1.1 --- a/doc-src/IsarRef/Thy/Generic.thy Fri May 09 23:35:57 2008 +0200
1.2 +++ b/doc-src/IsarRef/Thy/Generic.thy Sat May 10 00:14:00 2008 +0200
1.3 @@ -786,200 +786,6 @@
1.4 *}
1.5
1.6
1.7 -section {* Derived proof schemes *}
1.8 -
1.9 -subsection {* Generalized elimination \label{sec:obtain} *}
1.10 -
1.11 -text {*
1.12 - \begin{matharray}{rcl}
1.13 - @{command_def "obtain"} & : & \isartrans{proof(state)}{proof(prove)} \\
1.14 - @{command_def "guess"}@{text "\<^sup>*"} & : & \isartrans{proof(state)}{proof(prove)} \\
1.15 - \end{matharray}
1.16 -
1.17 - Generalized elimination means that additional elements with certain
1.18 - properties may be introduced in the current context, by virtue of a
1.19 - locally proven ``soundness statement''. Technically speaking, the
1.20 - @{command "obtain"} language element is like a declaration of
1.21 - @{command "fix"} and @{command "assume"} (see also see
1.22 - \secref{sec:proof-context}), together with a soundness proof of its
1.23 - additional claim. According to the nature of existential reasoning,
1.24 - assumptions get eliminated from any result exported from the context
1.25 - later, provided that the corresponding parameters do \emph{not}
1.26 - occur in the conclusion.
1.27 -
1.28 - \begin{rail}
1.29 - 'obtain' parname? (vars + 'and') 'where' (props + 'and')
1.30 - ;
1.31 - 'guess' (vars + 'and')
1.32 - ;
1.33 - \end{rail}
1.34 -
1.35 - The derived Isar command @{command "obtain"} is defined as follows
1.36 - (where @{text "b\<^sub>1, \<dots>, b\<^sub>k"} shall refer to (optional)
1.37 - facts indicated for forward chaining).
1.38 - \begin{matharray}{l}
1.39 - @{text "\<langle>using b\<^sub>1 \<dots> b\<^sub>k\<rangle>"}~~@{command "obtain"}~@{text "x\<^sub>1 \<dots> x\<^sub>m \<WHERE> a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n \<langle>proof\<rangle> \<equiv>"} \\[1ex]
1.40 - \quad @{command "have"}~@{text "\<And>thesis. (\<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> thesis) \<Longrightarrow> thesis"} \\
1.41 - \quad @{command "proof"}~@{text succeed} \\
1.42 - \qquad @{command "fix"}~@{text thesis} \\
1.43 - \qquad @{command "assume"}~@{text "that [Pure.intro?]: \<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> thesis"} \\
1.44 - \qquad @{command "then"}~@{command "show"}~@{text thesis} \\
1.45 - \quad\qquad @{command "apply"}~@{text -} \\
1.46 - \quad\qquad @{command "using"}~@{text "b\<^sub>1 \<dots> b\<^sub>k \<langle>proof\<rangle>"} \\
1.47 - \quad @{command "qed"} \\
1.48 - \quad @{command "fix"}~@{text "x\<^sub>1 \<dots> x\<^sub>m"}~@{command "assume"}@{text "\<^sup>* a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} \\
1.49 - \end{matharray}
1.50 -
1.51 - Typically, the soundness proof is relatively straight-forward, often
1.52 - just by canonical automated tools such as ``@{command "by"}~@{text
1.53 - simp}'' or ``@{command "by"}~@{text blast}''. Accordingly, the
1.54 - ``@{text that}'' reduction above is declared as simplification and
1.55 - introduction rule.
1.56 -
1.57 - In a sense, @{command "obtain"} represents at the level of Isar
1.58 - proofs what would be meta-logical existential quantifiers and
1.59 - conjunctions. This concept has a broad range of useful
1.60 - applications, ranging from plain elimination (or introduction) of
1.61 - object-level existential and conjunctions, to elimination over
1.62 - results of symbolic evaluation of recursive definitions, for
1.63 - example. Also note that @{command "obtain"} without parameters acts
1.64 - much like @{command "have"}, where the result is treated as a
1.65 - genuine assumption.
1.66 -
1.67 - An alternative name to be used instead of ``@{text that}'' above may
1.68 - be given in parentheses.
1.69 -
1.70 - \medskip The improper variant @{command "guess"} is similar to
1.71 - @{command "obtain"}, but derives the obtained statement from the
1.72 - course of reasoning! The proof starts with a fixed goal @{text
1.73 - thesis}. The subsequent proof may refine this to anything of the
1.74 - form like @{text "\<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots>
1.75 - \<phi>\<^sub>n \<Longrightarrow> thesis"}, but must not introduce new subgoals. The
1.76 - final goal state is then used as reduction rule for the obtain
1.77 - scheme described above. Obtained parameters @{text "x\<^sub>1, \<dots>,
1.78 - x\<^sub>m"} are marked as internal by default, which prevents the
1.79 - proof context from being polluted by ad-hoc variables. The variable
1.80 - names and type constraints given as arguments for @{command "guess"}
1.81 - specify a prefix of obtained parameters explicitly in the text.
1.82 -
1.83 - It is important to note that the facts introduced by @{command
1.84 - "obtain"} and @{command "guess"} may not be polymorphic: any
1.85 - type-variables occurring here are fixed in the present context!
1.86 -*}
1.87 -
1.88 -
1.89 -subsection {* Calculational reasoning \label{sec:calculation} *}
1.90 -
1.91 -text {*
1.92 - \begin{matharray}{rcl}
1.93 - @{command_def "also"} & : & \isartrans{proof(state)}{proof(state)} \\
1.94 - @{command_def "finally"} & : & \isartrans{proof(state)}{proof(chain)} \\
1.95 - @{command_def "moreover"} & : & \isartrans{proof(state)}{proof(state)} \\
1.96 - @{command_def "ultimately"} & : & \isartrans{proof(state)}{proof(chain)} \\
1.97 - @{command_def "print_trans_rules"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
1.98 - @{attribute trans} & : & \isaratt \\
1.99 - @{attribute sym} & : & \isaratt \\
1.100 - @{attribute symmetric} & : & \isaratt \\
1.101 - \end{matharray}
1.102 -
1.103 - Calculational proof is forward reasoning with implicit application
1.104 - of transitivity rules (such those of @{text "="}, @{text "\<le>"},
1.105 - @{text "<"}). Isabelle/Isar maintains an auxiliary fact register
1.106 - @{fact_ref calculation} for accumulating results obtained by
1.107 - transitivity composed with the current result. Command @{command
1.108 - "also"} updates @{fact calculation} involving @{fact this}, while
1.109 - @{command "finally"} exhibits the final @{fact calculation} by
1.110 - forward chaining towards the next goal statement. Both commands
1.111 - require valid current facts, i.e.\ may occur only after commands
1.112 - that produce theorems such as @{command "assume"}, @{command
1.113 - "note"}, or some finished proof of @{command "have"}, @{command
1.114 - "show"} etc. The @{command "moreover"} and @{command "ultimately"}
1.115 - commands are similar to @{command "also"} and @{command "finally"},
1.116 - but only collect further results in @{fact calculation} without
1.117 - applying any rules yet.
1.118 -
1.119 - Also note that the implicit term abbreviation ``@{text "\<dots>"}'' has
1.120 - its canonical application with calculational proofs. It refers to
1.121 - the argument of the preceding statement. (The argument of a curried
1.122 - infix expression happens to be its right-hand side.)
1.123 -
1.124 - Isabelle/Isar calculations are implicitly subject to block structure
1.125 - in the sense that new threads of calculational reasoning are
1.126 - commenced for any new block (as opened by a local goal, for
1.127 - example). This means that, apart from being able to nest
1.128 - calculations, there is no separate \emph{begin-calculation} command
1.129 - required.
1.130 -
1.131 - \medskip The Isar calculation proof commands may be defined as
1.132 - follows:\footnote{We suppress internal bookkeeping such as proper
1.133 - handling of block-structure.}
1.134 -
1.135 - \begin{matharray}{rcl}
1.136 - @{command "also"}@{text "\<^sub>0"} & \equiv & @{command "note"}~@{text "calculation = this"} \\
1.137 - @{command "also"}@{text "\<^sub>n\<^sub>+\<^sub>1"} & \equiv & @{command "note"}~@{text "calculation = trans [OF calculation this]"} \\[0.5ex]
1.138 - @{command "finally"} & \equiv & @{command "also"}~@{command "from"}~@{text calculation} \\[0.5ex]
1.139 - @{command "moreover"} & \equiv & @{command "note"}~@{text "calculation = calculation this"} \\
1.140 - @{command "ultimately"} & \equiv & @{command "moreover"}~@{command "from"}~@{text calculation} \\
1.141 - \end{matharray}
1.142 -
1.143 - \begin{rail}
1.144 - ('also' | 'finally') ('(' thmrefs ')')?
1.145 - ;
1.146 - 'trans' (() | 'add' | 'del')
1.147 - ;
1.148 - \end{rail}
1.149 -
1.150 - \begin{descr}
1.151 -
1.152 - \item [@{command "also"}~@{text "(a\<^sub>1 \<dots> a\<^sub>n)"}]
1.153 - maintains the auxiliary @{fact calculation} register as follows.
1.154 - The first occurrence of @{command "also"} in some calculational
1.155 - thread initializes @{fact calculation} by @{fact this}. Any
1.156 - subsequent @{command "also"} on the same level of block-structure
1.157 - updates @{fact calculation} by some transitivity rule applied to
1.158 - @{fact calculation} and @{fact this} (in that order). Transitivity
1.159 - rules are picked from the current context, unless alternative rules
1.160 - are given as explicit arguments.
1.161 -
1.162 - \item [@{command "finally"}~@{text "(a\<^sub>1 \<dots> a\<^sub>n)"}]
1.163 - maintaining @{fact calculation} in the same way as @{command
1.164 - "also"}, and concludes the current calculational thread. The final
1.165 - result is exhibited as fact for forward chaining towards the next
1.166 - goal. Basically, @{command "finally"} just abbreviates @{command
1.167 - "also"}~@{command "from"}~@{fact calculation}. Typical idioms for
1.168 - concluding calculational proofs are ``@{command "finally"}~@{command
1.169 - "show"}~@{text ?thesis}~@{command "."}'' and ``@{command
1.170 - "finally"}~@{command "have"}~@{text \<phi>}~@{command "."}''.
1.171 -
1.172 - \item [@{command "moreover"} and @{command "ultimately"}] are
1.173 - analogous to @{command "also"} and @{command "finally"}, but collect
1.174 - results only, without applying rules.
1.175 -
1.176 - \item [@{command "print_trans_rules"}] prints the list of
1.177 - transitivity rules (for calculational commands @{command "also"} and
1.178 - @{command "finally"}) and symmetry rules (for the @{attribute
1.179 - symmetric} operation and single step elimination patters) of the
1.180 - current context.
1.181 -
1.182 - \item [@{attribute trans}] declares theorems as transitivity rules.
1.183 -
1.184 - \item [@{attribute sym}] declares symmetry rules, as well as
1.185 - @{attribute "Pure.elim?"} rules.
1.186 -
1.187 - \item [@{attribute symmetric}] resolves a theorem with some rule
1.188 - declared as @{attribute sym} in the current context. For example,
1.189 - ``@{command "assume"}~@{text "[symmetric]: x = y"}'' produces a
1.190 - swapped fact derived from that assumption.
1.191 -
1.192 - In structured proof texts it is often more appropriate to use an
1.193 - explicit single-step elimination proof, such as ``@{command
1.194 - "assume"}~@{text "x = y"}~@{command "then"}~@{command "have"}~@{text
1.195 - "y = x"}~@{command ".."}''.
1.196 -
1.197 - \end{descr}
1.198 -*}
1.199 -
1.200 -
1.201 section {* Proof tools *}
1.202
1.203 subsection {* Miscellaneous methods and attributes \label{sec:misc-meth-att} *}
2.1 --- a/doc-src/IsarRef/Thy/Proof.thy Fri May 09 23:35:57 2008 +0200
2.2 +++ b/doc-src/IsarRef/Thy/Proof.thy Sat May 10 00:14:00 2008 +0200
2.3 @@ -6,4 +6,1033 @@
2.4
2.5 chapter {* Proofs *}
2.6
2.7 +text {*
2.8 + Proof commands perform transitions of Isar/VM machine
2.9 + configurations, which are block-structured, consisting of a stack of
2.10 + nodes with three main components: logical proof context, current
2.11 + facts, and open goals. Isar/VM transitions are \emph{typed}
2.12 + according to the following three different modes of operation:
2.13 +
2.14 + \begin{descr}
2.15 +
2.16 + \item [@{text "proof(prove)"}] means that a new goal has just been
2.17 + stated that is now to be \emph{proven}; the next command may refine
2.18 + it by some proof method, and enter a sub-proof to establish the
2.19 + actual result.
2.20 +
2.21 + \item [@{text "proof(state)"}] is like a nested theory mode: the
2.22 + context may be augmented by \emph{stating} additional assumptions,
2.23 + intermediate results etc.
2.24 +
2.25 + \item [@{text "proof(chain)"}] is intermediate between @{text
2.26 + "proof(state)"} and @{text "proof(prove)"}: existing facts (i.e.\
2.27 + the contents of the special ``@{fact_ref this}'' register) have been
2.28 + just picked up in order to be used when refining the goal claimed
2.29 + next.
2.30 +
2.31 + \end{descr}
2.32 +
2.33 + The proof mode indicator may be read as a verb telling the writer
2.34 + what kind of operation may be performed next. The corresponding
2.35 + typings of proof commands restricts the shape of well-formed proof
2.36 + texts to particular command sequences. So dynamic arrangements of
2.37 + commands eventually turn out as static texts of a certain structure.
2.38 + \Appref{ap:refcard} gives a simplified grammar of the overall
2.39 + (extensible) language emerging that way.
2.40 +*}
2.41 +
2.42 +
2.43 +section {* Context elements \label{sec:proof-context} *}
2.44 +
2.45 +text {*
2.46 + \begin{matharray}{rcl}
2.47 + @{command_def "fix"} & : & \isartrans{proof(state)}{proof(state)} \\
2.48 + @{command_def "assume"} & : & \isartrans{proof(state)}{proof(state)} \\
2.49 + @{command_def "presume"} & : & \isartrans{proof(state)}{proof(state)} \\
2.50 + @{command_def "def"} & : & \isartrans{proof(state)}{proof(state)} \\
2.51 + \end{matharray}
2.52 +
2.53 + The logical proof context consists of fixed variables and
2.54 + assumptions. The former closely correspond to Skolem constants, or
2.55 + meta-level universal quantification as provided by the Isabelle/Pure
2.56 + logical framework. Introducing some \emph{arbitrary, but fixed}
2.57 + variable via ``@{command "fix"}~@{text x}'' results in a local value
2.58 + that may be used in the subsequent proof as any other variable or
2.59 + constant. Furthermore, any result @{text "\<turnstile> \<phi>[x]"} exported from
2.60 + the context will be universally closed wrt.\ @{text x} at the
2.61 + outermost level: @{text "\<turnstile> \<And>x. \<phi>[x]"} (this is expressed in normal
2.62 + form using Isabelle's meta-variables).
2.63 +
2.64 + Similarly, introducing some assumption @{text \<chi>} has two effects.
2.65 + On the one hand, a local theorem is created that may be used as a
2.66 + fact in subsequent proof steps. On the other hand, any result
2.67 + @{text "\<chi> \<turnstile> \<phi>"} exported from the context becomes conditional wrt.\
2.68 + the assumption: @{text "\<turnstile> \<chi> \<Longrightarrow> \<phi>"}. Thus, solving an enclosing goal
2.69 + using such a result would basically introduce a new subgoal stemming
2.70 + from the assumption. How this situation is handled depends on the
2.71 + version of assumption command used: while @{command "assume"}
2.72 + insists on solving the subgoal by unification with some premise of
2.73 + the goal, @{command "presume"} leaves the subgoal unchanged in order
2.74 + to be proved later by the user.
2.75 +
2.76 + Local definitions, introduced by ``@{command "def"}~@{text "x \<equiv>
2.77 + t"}'', are achieved by combining ``@{command "fix"}~@{text x}'' with
2.78 + another version of assumption that causes any hypothetical equation
2.79 + @{text "x \<equiv> t"} to be eliminated by the reflexivity rule. Thus,
2.80 + exporting some result @{text "x \<equiv> t \<turnstile> \<phi>[x]"} yields @{text "\<turnstile>
2.81 + \<phi>[t]"}.
2.82 +
2.83 + \begin{rail}
2.84 + 'fix' (vars + 'and')
2.85 + ;
2.86 + ('assume' | 'presume') (props + 'and')
2.87 + ;
2.88 + 'def' (def + 'and')
2.89 + ;
2.90 + def: thmdecl? \\ name ('==' | equiv) term termpat?
2.91 + ;
2.92 + \end{rail}
2.93 +
2.94 + \begin{descr}
2.95 +
2.96 + \item [@{command "fix"}~@{text x}] introduces a local variable
2.97 + @{text x} that is \emph{arbitrary, but fixed.}
2.98 +
2.99 + \item [@{command "assume"}~@{text "a: \<phi>"} and @{command
2.100 + "presume"}~@{text "a: \<phi>"}] introduce a local fact @{text "\<phi> \<turnstile> \<phi>"} by
2.101 + assumption. Subsequent results applied to an enclosing goal (e.g.\
2.102 + by @{command_ref "show"}) are handled as follows: @{command
2.103 + "assume"} expects to be able to unify with existing premises in the
2.104 + goal, while @{command "presume"} leaves @{text \<phi>} as new subgoals.
2.105 +
2.106 + Several lists of assumptions may be given (separated by
2.107 + @{keyword_ref "and"}; the resulting list of current facts consists
2.108 + of all of these concatenated.
2.109 +
2.110 + \item [@{command "def"}~@{text "x \<equiv> t"}] introduces a local
2.111 + (non-polymorphic) definition. In results exported from the context,
2.112 + @{text x} is replaced by @{text t}. Basically, ``@{command
2.113 + "def"}~@{text "x \<equiv> t"}'' abbreviates ``@{command "fix"}~@{text
2.114 + x}~@{command "assume"}~@{text "x \<equiv> t"}'', with the resulting
2.115 + hypothetical equation solved by reflexivity.
2.116 +
2.117 + The default name for the definitional equation is @{text x_def}.
2.118 + Several simultaneous definitions may be given at the same time.
2.119 +
2.120 + \end{descr}
2.121 +
2.122 + The special name @{fact_ref prems} refers to all assumptions of the
2.123 + current context as a list of theorems. This feature should be used
2.124 + with great care! It is better avoided in final proof texts.
2.125 +*}
2.126 +
2.127 +
2.128 +section {* Facts and forward chaining *}
2.129 +
2.130 +text {*
2.131 + \begin{matharray}{rcl}
2.132 + @{command_def "note"} & : & \isartrans{proof(state)}{proof(state)} \\
2.133 + @{command_def "then"} & : & \isartrans{proof(state)}{proof(chain)} \\
2.134 + @{command_def "from"} & : & \isartrans{proof(state)}{proof(chain)} \\
2.135 + @{command_def "with"} & : & \isartrans{proof(state)}{proof(chain)} \\
2.136 + @{command_def "using"} & : & \isartrans{proof(prove)}{proof(prove)} \\
2.137 + @{command_def "unfolding"} & : & \isartrans{proof(prove)}{proof(prove)} \\
2.138 + \end{matharray}
2.139 +
2.140 + New facts are established either by assumption or proof of local
2.141 + statements. Any fact will usually be involved in further proofs,
2.142 + either as explicit arguments of proof methods, or when forward
2.143 + chaining towards the next goal via @{command "then"} (and variants);
2.144 + @{command "from"} and @{command "with"} are composite forms
2.145 + involving @{command "note"}. The @{command "using"} elements
2.146 + augments the collection of used facts \emph{after} a goal has been
2.147 + stated. Note that the special theorem name @{fact_ref this} refers
2.148 + to the most recently established facts, but only \emph{before}
2.149 + issuing a follow-up claim.
2.150 +
2.151 + \begin{rail}
2.152 + 'note' (thmdef? thmrefs + 'and')
2.153 + ;
2.154 + ('from' | 'with' | 'using' | 'unfolding') (thmrefs + 'and')
2.155 + ;
2.156 + \end{rail}
2.157 +
2.158 + \begin{descr}
2.159 +
2.160 + \item [@{command "note"}~@{text "a = b\<^sub>1 \<dots> b\<^sub>n"}]
2.161 + recalls existing facts @{text "b\<^sub>1, \<dots>, b\<^sub>n"}, binding
2.162 + the result as @{text a}. Note that attributes may be involved as
2.163 + well, both on the left and right hand sides.
2.164 +
2.165 + \item [@{command "then"}] indicates forward chaining by the current
2.166 + facts in order to establish the goal to be claimed next. The
2.167 + initial proof method invoked to refine that will be offered the
2.168 + facts to do ``anything appropriate'' (see also
2.169 + \secref{sec:proof-steps}). For example, method @{method_ref rule}
2.170 + (see \secref{sec:pure-meth-att}) would typically do an elimination
2.171 + rather than an introduction. Automatic methods usually insert the
2.172 + facts into the goal state before operation. This provides a simple
2.173 + scheme to control relevance of facts in automated proof search.
2.174 +
2.175 + \item [@{command "from"}~@{text b}] abbreviates ``@{command
2.176 + "note"}~@{text b}~@{command "then"}''; thus @{command "then"} is
2.177 + equivalent to ``@{command "from"}~@{text this}''.
2.178 +
2.179 + \item [@{command "with"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"}]
2.180 + abbreviates ``@{command "from"}~@{text "b\<^sub>1 \<dots> b\<^sub>n \<AND>
2.181 + this"}''; thus the forward chaining is from earlier facts together
2.182 + with the current ones.
2.183 +
2.184 + \item [@{command "using"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"}] augments
2.185 + the facts being currently indicated for use by a subsequent
2.186 + refinement step (such as @{command_ref "apply"} or @{command_ref
2.187 + "proof"}).
2.188 +
2.189 + \item [@{command "unfolding"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"}] is
2.190 + structurally similar to @{command "using"}, but unfolds definitional
2.191 + equations @{text "b\<^sub>1, \<dots> b\<^sub>n"} throughout the goal state
2.192 + and facts.
2.193 +
2.194 + \end{descr}
2.195 +
2.196 + Forward chaining with an empty list of theorems is the same as not
2.197 + chaining at all. Thus ``@{command "from"}~@{text nothing}'' has no
2.198 + effect apart from entering @{text "prove(chain)"} mode, since
2.199 + @{fact_ref nothing} is bound to the empty list of theorems.
2.200 +
2.201 + Basic proof methods (such as @{method_ref rule}) expect multiple
2.202 + facts to be given in their proper order, corresponding to a prefix
2.203 + of the premises of the rule involved. Note that positions may be
2.204 + easily skipped using something like @{command "from"}~@{text "_
2.205 + \<AND> a \<AND> b"}, for example. This involves the trivial rule
2.206 + @{text "PROP \<psi> \<Longrightarrow> PROP \<psi>"}, which is bound in Isabelle/Pure as
2.207 + ``@{fact_ref "_"}'' (underscore).
2.208 +
2.209 + Automated methods (such as @{method simp} or @{method auto}) just
2.210 + insert any given facts before their usual operation. Depending on
2.211 + the kind of procedure involved, the order of facts is less
2.212 + significant here.
2.213 +*}
2.214 +
2.215 +
2.216 +section {* Goal statements \label{sec:goals} *}
2.217 +
2.218 +text {*
2.219 + \begin{matharray}{rcl}
2.220 + @{command_def "lemma"} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
2.221 + @{command_def "theorem"} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
2.222 + @{command_def "corollary"} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
2.223 + @{command_def "have"} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
2.224 + @{command_def "show"} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
2.225 + @{command_def "hence"} & : & \isartrans{proof(state)}{proof(prove)} \\
2.226 + @{command_def "thus"} & : & \isartrans{proof(state)}{proof(prove)} \\
2.227 + @{command_def "print_statement"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
2.228 + \end{matharray}
2.229 +
2.230 + From a theory context, proof mode is entered by an initial goal
2.231 + command such as @{command "lemma"}, @{command "theorem"}, or
2.232 + @{command "corollary"}. Within a proof, new claims may be
2.233 + introduced locally as well; four variants are available here to
2.234 + indicate whether forward chaining of facts should be performed
2.235 + initially (via @{command_ref "then"}), and whether the final result
2.236 + is meant to solve some pending goal.
2.237 +
2.238 + Goals may consist of multiple statements, resulting in a list of
2.239 + facts eventually. A pending multi-goal is internally represented as
2.240 + a meta-level conjunction (printed as @{text "&&"}), which is usually
2.241 + split into the corresponding number of sub-goals prior to an initial
2.242 + method application, via @{command_ref "proof"}
2.243 + (\secref{sec:proof-steps}) or @{command_ref "apply"}
2.244 + (\secref{sec:tactic-commands}). The @{method_ref induct} method
2.245 + covered in \secref{sec:cases-induct} acts on multiple claims
2.246 + simultaneously.
2.247 +
2.248 + Claims at the theory level may be either in short or long form. A
2.249 + short goal merely consists of several simultaneous propositions
2.250 + (often just one). A long goal includes an explicit context
2.251 + specification for the subsequent conclusion, involving local
2.252 + parameters and assumptions. Here the role of each part of the
2.253 + statement is explicitly marked by separate keywords (see also
2.254 + \secref{sec:locale}); the local assumptions being introduced here
2.255 + are available as @{fact_ref assms} in the proof. Moreover, there
2.256 + are two kinds of conclusions: @{element_def "shows"} states several
2.257 + simultaneous propositions (essentially a big conjunction), while
2.258 + @{element_def "obtains"} claims several simultaneous simultaneous
2.259 + contexts of (essentially a big disjunction of eliminated parameters
2.260 + and assumptions, cf.\ \secref{sec:obtain}).
2.261 +
2.262 + \begin{rail}
2.263 + ('lemma' | 'theorem' | 'corollary') target? (goal | longgoal)
2.264 + ;
2.265 + ('have' | 'show' | 'hence' | 'thus') goal
2.266 + ;
2.267 + 'print\_statement' modes? thmrefs
2.268 + ;
2.269 +
2.270 + goal: (props + 'and')
2.271 + ;
2.272 + longgoal: thmdecl? (contextelem *) conclusion
2.273 + ;
2.274 + conclusion: 'shows' goal | 'obtains' (parname? case + '|')
2.275 + ;
2.276 + case: (vars + 'and') 'where' (props + 'and')
2.277 + ;
2.278 + \end{rail}
2.279 +
2.280 + \begin{descr}
2.281 +
2.282 + \item [@{command "lemma"}~@{text "a: \<phi>"}] enters proof mode with
2.283 + @{text \<phi>} as main goal, eventually resulting in some fact @{text "\<turnstile>
2.284 + \<phi>"} to be put back into the target context. An additional
2.285 + \railnonterm{context} specification may build up an initial proof
2.286 + context for the subsequent claim; this includes local definitions
2.287 + and syntax as well, see the definition of @{syntax contextelem} in
2.288 + \secref{sec:locale}.
2.289 +
2.290 + \item [@{command "theorem"}~@{text "a: \<phi>"} and @{command
2.291 + "corollary"}~@{text "a: \<phi>"}] are essentially the same as @{command
2.292 + "lemma"}~@{text "a: \<phi>"}, but the facts are internally marked as
2.293 + being of a different kind. This discrimination acts like a formal
2.294 + comment.
2.295 +
2.296 + \item [@{command "have"}~@{text "a: \<phi>"}] claims a local goal,
2.297 + eventually resulting in a fact within the current logical context.
2.298 + This operation is completely independent of any pending sub-goals of
2.299 + an enclosing goal statements, so @{command "have"} may be freely
2.300 + used for experimental exploration of potential results within a
2.301 + proof body.
2.302 +
2.303 + \item [@{command "show"}~@{text "a: \<phi>"}] is like @{command
2.304 + "have"}~@{text "a: \<phi>"} plus a second stage to refine some pending
2.305 + sub-goal for each one of the finished result, after having been
2.306 + exported into the corresponding context (at the head of the
2.307 + sub-proof of this @{command "show"} command).
2.308 +
2.309 + To accommodate interactive debugging, resulting rules are printed
2.310 + before being applied internally. Even more, interactive execution
2.311 + of @{command "show"} predicts potential failure and displays the
2.312 + resulting error as a warning beforehand. Watch out for the
2.313 + following message:
2.314 +
2.315 + %FIXME proper antiquitation
2.316 + \begin{ttbox}
2.317 + Problem! Local statement will fail to solve any pending goal
2.318 + \end{ttbox}
2.319 +
2.320 + \item [@{command "hence"}] abbreviates ``@{command "then"}~@{command
2.321 + "have"}'', i.e.\ claims a local goal to be proven by forward
2.322 + chaining the current facts. Note that @{command "hence"} is also
2.323 + equivalent to ``@{command "from"}~@{text this}~@{command "have"}''.
2.324 +
2.325 + \item [@{command "thus"}] abbreviates ``@{command "then"}~@{command
2.326 + "show"}''. Note that @{command "thus"} is also equivalent to
2.327 + ``@{command "from"}~@{text this}~@{command "show"}''.
2.328 +
2.329 + \item [@{command "print_statement"}~@{text a}] prints facts from the
2.330 + current theory or proof context in long statement form, according to
2.331 + the syntax for @{command "lemma"} given above.
2.332 +
2.333 + \end{descr}
2.334 +
2.335 + Any goal statement causes some term abbreviations (such as
2.336 + @{variable_ref "?thesis"}) to be bound automatically, see also
2.337 + \secref{sec:term-abbrev}. Furthermore, the local context of a
2.338 + (non-atomic) goal is provided via the @{case_ref rule_context} case.
2.339 +
2.340 + The optional case names of @{element_ref "obtains"} have a twofold
2.341 + meaning: (1) during the of this claim they refer to the the local
2.342 + context introductions, (2) the resulting rule is annotated
2.343 + accordingly to support symbolic case splits when used with the
2.344 + @{method_ref cases} method (cf. \secref{sec:cases-induct}).
2.345 +
2.346 + \medskip
2.347 +
2.348 + \begin{warn}
2.349 + Isabelle/Isar suffers theory-level goal statements to contain
2.350 + \emph{unbound schematic variables}, although this does not conform
2.351 + to the aim of human-readable proof documents! The main problem
2.352 + with schematic goals is that the actual outcome is usually hard to
2.353 + predict, depending on the behavior of the proof methods applied
2.354 + during the course of reasoning. Note that most semi-automated
2.355 + methods heavily depend on several kinds of implicit rule
2.356 + declarations within the current theory context. As this would
2.357 + also result in non-compositional checking of sub-proofs,
2.358 + \emph{local goals} are not allowed to be schematic at all.
2.359 + Nevertheless, schematic goals do have their use in Prolog-style
2.360 + interactive synthesis of proven results, usually by stepwise
2.361 + refinement via emulation of traditional Isabelle tactic scripts
2.362 + (see also \secref{sec:tactic-commands}). In any case, users
2.363 + should know what they are doing.
2.364 + \end{warn}
2.365 +*}
2.366 +
2.367 +
2.368 +section {* Initial and terminal proof steps \label{sec:proof-steps} *}
2.369 +
2.370 +text {*
2.371 + \begin{matharray}{rcl}
2.372 + @{command_def "proof"} & : & \isartrans{proof(prove)}{proof(state)} \\
2.373 + @{command_def "qed"} & : & \isartrans{proof(state)}{proof(state) ~|~ theory} \\
2.374 + @{command_def "by"} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
2.375 + @{command_def ".."} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
2.376 + @{command_def "."} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
2.377 + @{command_def "sorry"} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
2.378 + \end{matharray}
2.379 +
2.380 + Arbitrary goal refinement via tactics is considered harmful.
2.381 + Structured proof composition in Isar admits proof methods to be
2.382 + invoked in two places only.
2.383 +
2.384 + \begin{enumerate}
2.385 +
2.386 + \item An \emph{initial} refinement step @{command_ref
2.387 + "proof"}~@{text "m\<^sub>1"} reduces a newly stated goal to a number
2.388 + of sub-goals that are to be solved later. Facts are passed to
2.389 + @{text "m\<^sub>1"} for forward chaining, if so indicated by @{text
2.390 + "proof(chain)"} mode.
2.391 +
2.392 + \item A \emph{terminal} conclusion step @{command_ref "qed"}~@{text
2.393 + "m\<^sub>2"} is intended to solve remaining goals. No facts are
2.394 + passed to @{text "m\<^sub>2"}.
2.395 +
2.396 + \end{enumerate}
2.397 +
2.398 + The only other (proper) way to affect pending goals in a proof body
2.399 + is by @{command_ref "show"}, which involves an explicit statement of
2.400 + what is to be solved eventually. Thus we avoid the fundamental
2.401 + problem of unstructured tactic scripts that consist of numerous
2.402 + consecutive goal transformations, with invisible effects.
2.403 +
2.404 + \medskip As a general rule of thumb for good proof style, initial
2.405 + proof methods should either solve the goal completely, or constitute
2.406 + some well-understood reduction to new sub-goals. Arbitrary
2.407 + automatic proof tools that are prone leave a large number of badly
2.408 + structured sub-goals are no help in continuing the proof document in
2.409 + an intelligible manner.
2.410 +
2.411 + Unless given explicitly by the user, the default initial method is
2.412 + ``@{method_ref rule}'', which applies a single standard elimination
2.413 + or introduction rule according to the topmost symbol involved.
2.414 + There is no separate default terminal method. Any remaining goals
2.415 + are always solved by assumption in the very last step.
2.416 +
2.417 + \begin{rail}
2.418 + 'proof' method?
2.419 + ;
2.420 + 'qed' method?
2.421 + ;
2.422 + 'by' method method?
2.423 + ;
2.424 + ('.' | '..' | 'sorry')
2.425 + ;
2.426 + \end{rail}
2.427 +
2.428 + \begin{descr}
2.429 +
2.430 + \item [@{command "proof"}~@{text "m\<^sub>1"}] refines the goal by
2.431 + proof method @{text "m\<^sub>1"}; facts for forward chaining are
2.432 + passed if so indicated by @{text "proof(chain)"} mode.
2.433 +
2.434 + \item [@{command "qed"}~@{text "m\<^sub>2"}] refines any remaining
2.435 + goals by proof method @{text "m\<^sub>2"} and concludes the
2.436 + sub-proof by assumption. If the goal had been @{text "show"} (or
2.437 + @{text "thus"}), some pending sub-goal is solved as well by the rule
2.438 + resulting from the result \emph{exported} into the enclosing goal
2.439 + context. Thus @{text "qed"} may fail for two reasons: either @{text
2.440 + "m\<^sub>2"} fails, or the resulting rule does not fit to any
2.441 + pending goal\footnote{This includes any additional ``strong''
2.442 + assumptions as introduced by @{command "assume"}.} of the enclosing
2.443 + context. Debugging such a situation might involve temporarily
2.444 + changing @{command "show"} into @{command "have"}, or weakening the
2.445 + local context by replacing occurrences of @{command "assume"} by
2.446 + @{command "presume"}.
2.447 +
2.448 + \item [@{command "by"}~@{text "m\<^sub>1 m\<^sub>2"}] is a
2.449 + \emph{terminal proof}\index{proof!terminal}; it abbreviates
2.450 + @{command "proof"}~@{text "m\<^sub>1"}~@{text "qed"}~@{text
2.451 + "m\<^sub>2"}, but with backtracking across both methods. Debugging
2.452 + an unsuccessful @{command "by"}~@{text "m\<^sub>1 m\<^sub>2"}
2.453 + command can be done by expanding its definition; in many cases
2.454 + @{command "proof"}~@{text "m\<^sub>1"} (or even @{text
2.455 + "apply"}~@{text "m\<^sub>1"}) is already sufficient to see the
2.456 + problem.
2.457 +
2.458 + \item [``@{command ".."}''] is a \emph{default
2.459 + proof}\index{proof!default}; it abbreviates @{command "by"}~@{text
2.460 + "rule"}.
2.461 +
2.462 + \item [``@{command "."}''] is a \emph{trivial
2.463 + proof}\index{proof!trivial}; it abbreviates @{command "by"}~@{text
2.464 + "this"}.
2.465 +
2.466 + \item [@{command "sorry"}] is a \emph{fake proof}\index{proof!fake}
2.467 + pretending to solve the pending claim without further ado. This
2.468 + only works in interactive development, or if the @{ML
2.469 + quick_and_dirty} flag is enabled (in ML). Facts emerging from fake
2.470 + proofs are not the real thing. Internally, each theorem container
2.471 + is tainted by an oracle invocation, which is indicated as ``@{text
2.472 + "[!]"}'' in the printed result.
2.473 +
2.474 + The most important application of @{command "sorry"} is to support
2.475 + experimentation and top-down proof development.
2.476 +
2.477 + \end{descr}
2.478 +*}
2.479 +
2.480 +
2.481 +section {* Fundamental methods and attributes \label{sec:pure-meth-att} *}
2.482 +
2.483 +text {*
2.484 + The following proof methods and attributes refer to basic logical
2.485 + operations of Isar. Further methods and attributes are provided by
2.486 + several generic and object-logic specific tools and packages (see
2.487 + \chref{ch:gen-tools} and \chref{ch:hol}).
2.488 +
2.489 + \begin{matharray}{rcl}
2.490 + @{method_def "-"} & : & \isarmeth \\
2.491 + @{method_def "fact"} & : & \isarmeth \\
2.492 + @{method_def "assumption"} & : & \isarmeth \\
2.493 + @{method_def "this"} & : & \isarmeth \\
2.494 + @{method_def "rule"} & : & \isarmeth \\
2.495 + @{method_def "iprover"} & : & \isarmeth \\[0.5ex]
2.496 + @{attribute_def "intro"} & : & \isaratt \\
2.497 + @{attribute_def "elim"} & : & \isaratt \\
2.498 + @{attribute_def "dest"} & : & \isaratt \\
2.499 + @{attribute_def "rule"} & : & \isaratt \\[0.5ex]
2.500 + @{attribute_def "OF"} & : & \isaratt \\
2.501 + @{attribute_def "of"} & : & \isaratt \\
2.502 + @{attribute_def "where"} & : & \isaratt \\
2.503 + \end{matharray}
2.504 +
2.505 + \begin{rail}
2.506 + 'fact' thmrefs?
2.507 + ;
2.508 + 'rule' thmrefs?
2.509 + ;
2.510 + 'iprover' ('!' ?) (rulemod *)
2.511 + ;
2.512 + rulemod: ('intro' | 'elim' | 'dest') ((('!' | () | '?') nat?) | 'del') ':' thmrefs
2.513 + ;
2.514 + ('intro' | 'elim' | 'dest') ('!' | () | '?') nat?
2.515 + ;
2.516 + 'rule' 'del'
2.517 + ;
2.518 + 'OF' thmrefs
2.519 + ;
2.520 + 'of' insts ('concl' ':' insts)?
2.521 + ;
2.522 + 'where' ((name | var | typefree | typevar) '=' (type | term) * 'and')
2.523 + ;
2.524 + \end{rail}
2.525 +
2.526 + \begin{descr}
2.527 +
2.528 + \item [``@{method "-"}'' (minus)] does nothing but insert the
2.529 + forward chaining facts as premises into the goal. Note that command
2.530 + @{command_ref "proof"} without any method actually performs a single
2.531 + reduction step using the @{method_ref rule} method; thus a plain
2.532 + \emph{do-nothing} proof step would be ``@{command "proof"}~@{text
2.533 + "-"}'' rather than @{command "proof"} alone.
2.534 +
2.535 + \item [@{method "fact"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}] composes
2.536 + some fact from @{text "a\<^sub>1, \<dots>, a\<^sub>n"} (or implicitly from
2.537 + the current proof context) modulo unification of schematic type and
2.538 + term variables. The rule structure is not taken into account, i.e.\
2.539 + meta-level implication is considered atomic. This is the same
2.540 + principle underlying literal facts (cf.\ \secref{sec:syn-att}):
2.541 + ``@{command "have"}~@{text "\<phi>"}~@{command "by"}~@{text fact}'' is
2.542 + equivalent to ``@{command "note"}~@{verbatim "`"}@{text \<phi>}@{verbatim
2.543 + "`"}'' provided that @{text "\<turnstile> \<phi>"} is an instance of some known
2.544 + @{text "\<turnstile> \<phi>"} in the proof context.
2.545 +
2.546 + \item [@{method assumption}] solves some goal by a single assumption
2.547 + step. All given facts are guaranteed to participate in the
2.548 + refinement; this means there may be only 0 or 1 in the first place.
2.549 + Recall that @{command "qed"} (\secref{sec:proof-steps}) already
2.550 + concludes any remaining sub-goals by assumption, so structured
2.551 + proofs usually need not quote the @{method assumption} method at
2.552 + all.
2.553 +
2.554 + \item [@{method this}] applies all of the current facts directly as
2.555 + rules. Recall that ``@{command "."}'' (dot) abbreviates ``@{command
2.556 + "by"}~@{text this}''.
2.557 +
2.558 + \item [@{method rule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}] applies some
2.559 + rule given as argument in backward manner; facts are used to reduce
2.560 + the rule before applying it to the goal. Thus @{method rule}
2.561 + without facts is plain introduction, while with facts it becomes
2.562 + elimination.
2.563 +
2.564 + When no arguments are given, the @{method rule} method tries to pick
2.565 + appropriate rules automatically, as declared in the current context
2.566 + using the @{attribute intro}, @{attribute elim}, @{attribute dest}
2.567 + attributes (see below). This is the default behavior of @{command
2.568 + "proof"} and ``@{command ".."}'' (double-dot) steps (see
2.569 + \secref{sec:proof-steps}).
2.570 +
2.571 + \item [@{method iprover}] performs intuitionistic proof search,
2.572 + depending on specifically declared rules from the context, or given
2.573 + as explicit arguments. Chained facts are inserted into the goal
2.574 + before commencing proof search; ``@{method iprover}@{text "!"}''
2.575 + means to include the current @{fact prems} as well.
2.576 +
2.577 + Rules need to be classified as @{attribute intro}, @{attribute
2.578 + elim}, or @{attribute dest}; here the ``@{text "!"}'' indicator
2.579 + refers to ``safe'' rules, which may be applied aggressively (without
2.580 + considering back-tracking later). Rules declared with ``@{text
2.581 + "?"}'' are ignored in proof search (the single-step @{method rule}
2.582 + method still observes these). An explicit weight annotation may be
2.583 + given as well; otherwise the number of rule premises will be taken
2.584 + into account here.
2.585 +
2.586 + \item [@{attribute intro}, @{attribute elim}, and @{attribute dest}]
2.587 + declare introduction, elimination, and destruct rules, to be used
2.588 + with the @{method rule} and @{method iprover} methods. Note that
2.589 + the latter will ignore rules declared with ``@{text "?"}'', while
2.590 + ``@{text "!"}'' are used most aggressively.
2.591 +
2.592 + The classical reasoner (see \secref{sec:classical}) introduces its
2.593 + own variants of these attributes; use qualified names to access the
2.594 + present versions of Isabelle/Pure, i.e.\ @{attribute "Pure.intro"}.
2.595 +
2.596 + \item [@{attribute rule}~@{text del}] undeclares introduction,
2.597 + elimination, or destruct rules.
2.598 +
2.599 + \item [@{attribute OF}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}] applies some
2.600 + theorem to all of the given rules @{text "a\<^sub>1, \<dots>, a\<^sub>n"}
2.601 + (in parallel). This corresponds to the @{ML "op MRS"} operation in
2.602 + ML, but note the reversed order. Positions may be effectively
2.603 + skipped by including ``@{text _}'' (underscore) as argument.
2.604 +
2.605 + \item [@{attribute of}~@{text "t\<^sub>1 \<dots> t\<^sub>n"}] performs
2.606 + positional instantiation of term variables. The terms @{text
2.607 + "t\<^sub>1, \<dots>, t\<^sub>n"} are substituted for any schematic
2.608 + variables occurring in a theorem from left to right; ``@{text
2.609 + _}'' (underscore) indicates to skip a position. Arguments following
2.610 + a ``@{keyword "concl"}@{text ":"}'' specification refer to positions
2.611 + of the conclusion of a rule.
2.612 +
2.613 + \item [@{attribute "where"}~@{text "x\<^sub>1 = t\<^sub>1 \<AND> \<dots>
2.614 + x\<^sub>n = t\<^sub>n"}] performs named instantiation of schematic
2.615 + type and term variables occurring in a theorem. Schematic variables
2.616 + have to be specified on the left-hand side (e.g.\ @{text "?x1.3"}).
2.617 + The question mark may be omitted if the variable name is a plain
2.618 + identifier without index. As type instantiations are inferred from
2.619 + term instantiations, explicit type instantiations are seldom
2.620 + necessary.
2.621 +
2.622 + \end{descr}
2.623 +*}
2.624 +
2.625 +
2.626 +section {* Term abbreviations \label{sec:term-abbrev} *}
2.627 +
2.628 +text {*
2.629 + \begin{matharray}{rcl}
2.630 + @{command_def "let"} & : & \isartrans{proof(state)}{proof(state)} \\
2.631 + @{keyword_def "is"} & : & syntax \\
2.632 + \end{matharray}
2.633 +
2.634 + Abbreviations may be either bound by explicit @{command
2.635 + "let"}~@{text "p \<equiv> t"} statements, or by annotating assumptions or
2.636 + goal statements with a list of patterns ``@{text "(\<IS> p\<^sub>1 \<dots>
2.637 + p\<^sub>n)"}''. In both cases, higher-order matching is invoked to
2.638 + bind extra-logical term variables, which may be either named
2.639 + schematic variables of the form @{text ?x}, or nameless dummies
2.640 + ``@{variable _}'' (underscore). Note that in the @{command "let"}
2.641 + form the patterns occur on the left-hand side, while the @{keyword
2.642 + "is"} patterns are in postfix position.
2.643 +
2.644 + Polymorphism of term bindings is handled in Hindley-Milner style,
2.645 + similar to ML. Type variables referring to local assumptions or
2.646 + open goal statements are \emph{fixed}, while those of finished
2.647 + results or bound by @{command "let"} may occur in \emph{arbitrary}
2.648 + instances later. Even though actual polymorphism should be rarely
2.649 + used in practice, this mechanism is essential to achieve proper
2.650 + incremental type-inference, as the user proceeds to build up the
2.651 + Isar proof text from left to right.
2.652 +
2.653 + \medskip Term abbreviations are quite different from local
2.654 + definitions as introduced via @{command "def"} (see
2.655 + \secref{sec:proof-context}). The latter are visible within the
2.656 + logic as actual equations, while abbreviations disappear during the
2.657 + input process just after type checking. Also note that @{command
2.658 + "def"} does not support polymorphism.
2.659 +
2.660 + \begin{rail}
2.661 + 'let' ((term + 'and') '=' term + 'and')
2.662 + ;
2.663 + \end{rail}
2.664 +
2.665 + The syntax of @{keyword "is"} patterns follows \railnonterm{termpat}
2.666 + or \railnonterm{proppat} (see \secref{sec:term-decls}).
2.667 +
2.668 + \begin{descr}
2.669 +
2.670 + \item [@{command "let"}~@{text "p\<^sub>1 = t\<^sub>1 \<AND> \<dots>
2.671 + p\<^sub>n = t\<^sub>n"}] binds any text variables in patterns @{text
2.672 + "p\<^sub>1, \<dots>, p\<^sub>n"} by simultaneous higher-order matching
2.673 + against terms @{text "t\<^sub>1, \<dots>, t\<^sub>n"}.
2.674 +
2.675 + \item [@{text "(\<IS> p\<^sub>1 \<dots> p\<^sub>n)"}] resembles @{command
2.676 + "let"}, but matches @{text "p\<^sub>1, \<dots>, p\<^sub>n"} against the
2.677 + preceding statement. Also note that @{keyword "is"} is not a
2.678 + separate command, but part of others (such as @{command "assume"},
2.679 + @{command "have"} etc.).
2.680 +
2.681 + \end{descr}
2.682 +
2.683 + Some \emph{implicit} term abbreviations\index{term abbreviations}
2.684 + for goals and facts are available as well. For any open goal,
2.685 + @{variable_ref thesis} refers to its object-level statement,
2.686 + abstracted over any meta-level parameters (if present). Likewise,
2.687 + @{variable_ref this} is bound for fact statements resulting from
2.688 + assumptions or finished goals. In case @{variable this} refers to
2.689 + an object-logic statement that is an application @{text "f t"}, then
2.690 + @{text t} is bound to the special text variable ``@{variable "\<dots>"}''
2.691 + (three dots). The canonical application of this convenience are
2.692 + calculational proofs (see \secref{sec:calculation}).
2.693 +*}
2.694 +
2.695 +
2.696 +section {* Block structure *}
2.697 +
2.698 +text {*
2.699 + \begin{matharray}{rcl}
2.700 + @{command_def "next"} & : & \isartrans{proof(state)}{proof(state)} \\
2.701 + @{command_def "{"} & : & \isartrans{proof(state)}{proof(state)} \\
2.702 + @{command_def "}"} & : & \isartrans{proof(state)}{proof(state)} \\
2.703 + \end{matharray}
2.704 +
2.705 + While Isar is inherently block-structured, opening and closing
2.706 + blocks is mostly handled rather casually, with little explicit
2.707 + user-intervention. Any local goal statement automatically opens
2.708 + \emph{two} internal blocks, which are closed again when concluding
2.709 + the sub-proof (by @{command "qed"} etc.). Sections of different
2.710 + context within a sub-proof may be switched via @{command "next"},
2.711 + which is just a single block-close followed by block-open again.
2.712 + The effect of @{command "next"} is to reset the local proof context;
2.713 + there is no goal focus involved here!
2.714 +
2.715 + For slightly more advanced applications, there are explicit block
2.716 + parentheses as well. These typically achieve a stronger forward
2.717 + style of reasoning.
2.718 +
2.719 + \begin{descr}
2.720 +
2.721 + \item [@{command "next"}] switches to a fresh block within a
2.722 + sub-proof, resetting the local context to the initial one.
2.723 +
2.724 + \item [@{command "{"} and @{command "}"}] explicitly open and close
2.725 + blocks. Any current facts pass through ``@{command "{"}''
2.726 + unchanged, while ``@{command "}"}'' causes any result to be
2.727 + \emph{exported} into the enclosing context. Thus fixed variables
2.728 + are generalized, assumptions discharged, and local definitions
2.729 + unfolded (cf.\ \secref{sec:proof-context}). There is no difference
2.730 + of @{command "assume"} and @{command "presume"} in this mode of
2.731 + forward reasoning --- in contrast to plain backward reasoning with
2.732 + the result exported at @{command "show"} time.
2.733 +
2.734 + \end{descr}
2.735 +*}
2.736 +
2.737 +
2.738 +section {* Emulating tactic scripts \label{sec:tactic-commands} *}
2.739 +
2.740 +text {*
2.741 + The Isar provides separate commands to accommodate tactic-style
2.742 + proof scripts within the same system. While being outside the
2.743 + orthodox Isar proof language, these might come in handy for
2.744 + interactive exploration and debugging, or even actual tactical proof
2.745 + within new-style theories (to benefit from document preparation, for
2.746 + example). See also \secref{sec:tactics} for actual tactics, that
2.747 + have been encapsulated as proof methods. Proper proof methods may
2.748 + be used in scripts, too.
2.749 +
2.750 + \begin{matharray}{rcl}
2.751 + @{command_def "apply"}@{text "\<^sup>*"} & : & \isartrans{proof(prove)}{proof(prove)} \\
2.752 + @{command_def "apply_end"}@{text "\<^sup>*"} & : & \isartrans{proof(state)}{proof(state)} \\
2.753 + @{command_def "done"}@{text "\<^sup>*"} & : & \isartrans{proof(prove)}{proof(state)} \\
2.754 + @{command_def "defer"}@{text "\<^sup>*"} & : & \isartrans{proof}{proof} \\
2.755 + @{command_def "prefer"}@{text "\<^sup>*"} & : & \isartrans{proof}{proof} \\
2.756 + @{command_def "back"}@{text "\<^sup>*"} & : & \isartrans{proof}{proof} \\
2.757 + \end{matharray}
2.758 +
2.759 + \begin{rail}
2.760 + ( 'apply' | 'apply\_end' ) method
2.761 + ;
2.762 + 'defer' nat?
2.763 + ;
2.764 + 'prefer' nat
2.765 + ;
2.766 + \end{rail}
2.767 +
2.768 + \begin{descr}
2.769 +
2.770 + \item [@{command "apply"}~@{text m}] applies proof method @{text m}
2.771 + in initial position, but unlike @{command "proof"} it retains
2.772 + ``@{text "proof(prove)"}'' mode. Thus consecutive method
2.773 + applications may be given just as in tactic scripts.
2.774 +
2.775 + Facts are passed to @{text m} as indicated by the goal's
2.776 + forward-chain mode, and are \emph{consumed} afterwards. Thus any
2.777 + further @{command "apply"} command would always work in a purely
2.778 + backward manner.
2.779 +
2.780 + \item [@{command "apply_end"}~@{text "m"}] applies proof method
2.781 + @{text m} as if in terminal position. Basically, this simulates a
2.782 + multi-step tactic script for @{command "qed"}, but may be given
2.783 + anywhere within the proof body.
2.784 +
2.785 + No facts are passed to @{method m} here. Furthermore, the static
2.786 + context is that of the enclosing goal (as for actual @{command
2.787 + "qed"}). Thus the proof method may not refer to any assumptions
2.788 + introduced in the current body, for example.
2.789 +
2.790 + \item [@{command "done"}] completes a proof script, provided that
2.791 + the current goal state is solved completely. Note that actual
2.792 + structured proof commands (e.g.\ ``@{command "."}'' or @{command
2.793 + "sorry"}) may be used to conclude proof scripts as well.
2.794 +
2.795 + \item [@{command "defer"}~@{text n} and @{command "prefer"}~@{text
2.796 + n}] shuffle the list of pending goals: @{command "defer"} puts off
2.797 + sub-goal @{text n} to the end of the list (@{text "n = 1"} by
2.798 + default), while @{command "prefer"} brings sub-goal @{text n} to the
2.799 + front.
2.800 +
2.801 + \item [@{command "back"}] does back-tracking over the result
2.802 + sequence of the latest proof command. Basically, any proof command
2.803 + may return multiple results.
2.804 +
2.805 + \end{descr}
2.806 +
2.807 + Any proper Isar proof method may be used with tactic script commands
2.808 + such as @{command "apply"}. A few additional emulations of actual
2.809 + tactics are provided as well; these would be never used in actual
2.810 + structured proofs, of course.
2.811 +*}
2.812 +
2.813 +
2.814 +section {* Omitting proofs *}
2.815 +
2.816 +text {*
2.817 + \begin{matharray}{rcl}
2.818 + @{command_def "oops"} & : & \isartrans{proof}{theory} \\
2.819 + \end{matharray}
2.820 +
2.821 + The @{command "oops"} command discontinues the current proof
2.822 + attempt, while considering the partial proof text as properly
2.823 + processed. This is conceptually quite different from ``faking''
2.824 + actual proofs via @{command_ref "sorry"} (see
2.825 + \secref{sec:proof-steps}): @{command "oops"} does not observe the
2.826 + proof structure at all, but goes back right to the theory level.
2.827 + Furthermore, @{command "oops"} does not produce any result theorem
2.828 + --- there is no intended claim to be able to complete the proof
2.829 + anyhow.
2.830 +
2.831 + A typical application of @{command "oops"} is to explain Isar proofs
2.832 + \emph{within} the system itself, in conjunction with the document
2.833 + preparation tools of Isabelle described in \cite{isabelle-sys}.
2.834 + Thus partial or even wrong proof attempts can be discussed in a
2.835 + logically sound manner. Note that the Isabelle {\LaTeX} macros can
2.836 + be easily adapted to print something like ``@{text "\<dots>"}'' instead of
2.837 + the keyword ``@{command "oops"}''.
2.838 +
2.839 + \medskip The @{command "oops"} command is undo-able, unlike
2.840 + @{command_ref "kill"} (see \secref{sec:history}). The effect is to
2.841 + get back to the theory just before the opening of the proof.
2.842 +*}
2.843 +
2.844 +
2.845 +section {* Generalized elimination \label{sec:obtain} *}
2.846 +
2.847 +text {*
2.848 + \begin{matharray}{rcl}
2.849 + @{command_def "obtain"} & : & \isartrans{proof(state)}{proof(prove)} \\
2.850 + @{command_def "guess"}@{text "\<^sup>*"} & : & \isartrans{proof(state)}{proof(prove)} \\
2.851 + \end{matharray}
2.852 +
2.853 + Generalized elimination means that additional elements with certain
2.854 + properties may be introduced in the current context, by virtue of a
2.855 + locally proven ``soundness statement''. Technically speaking, the
2.856 + @{command "obtain"} language element is like a declaration of
2.857 + @{command "fix"} and @{command "assume"} (see also see
2.858 + \secref{sec:proof-context}), together with a soundness proof of its
2.859 + additional claim. According to the nature of existential reasoning,
2.860 + assumptions get eliminated from any result exported from the context
2.861 + later, provided that the corresponding parameters do \emph{not}
2.862 + occur in the conclusion.
2.863 +
2.864 + \begin{rail}
2.865 + 'obtain' parname? (vars + 'and') 'where' (props + 'and')
2.866 + ;
2.867 + 'guess' (vars + 'and')
2.868 + ;
2.869 + \end{rail}
2.870 +
2.871 + The derived Isar command @{command "obtain"} is defined as follows
2.872 + (where @{text "b\<^sub>1, \<dots>, b\<^sub>k"} shall refer to (optional)
2.873 + facts indicated for forward chaining).
2.874 + \begin{matharray}{l}
2.875 + @{text "\<langle>using b\<^sub>1 \<dots> b\<^sub>k\<rangle>"}~~@{command "obtain"}~@{text "x\<^sub>1 \<dots> x\<^sub>m \<WHERE> a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n \<langle>proof\<rangle> \<equiv>"} \\[1ex]
2.876 + \quad @{command "have"}~@{text "\<And>thesis. (\<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> thesis) \<Longrightarrow> thesis"} \\
2.877 + \quad @{command "proof"}~@{text succeed} \\
2.878 + \qquad @{command "fix"}~@{text thesis} \\
2.879 + \qquad @{command "assume"}~@{text "that [Pure.intro?]: \<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> thesis"} \\
2.880 + \qquad @{command "then"}~@{command "show"}~@{text thesis} \\
2.881 + \quad\qquad @{command "apply"}~@{text -} \\
2.882 + \quad\qquad @{command "using"}~@{text "b\<^sub>1 \<dots> b\<^sub>k \<langle>proof\<rangle>"} \\
2.883 + \quad @{command "qed"} \\
2.884 + \quad @{command "fix"}~@{text "x\<^sub>1 \<dots> x\<^sub>m"}~@{command "assume"}@{text "\<^sup>* a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} \\
2.885 + \end{matharray}
2.886 +
2.887 + Typically, the soundness proof is relatively straight-forward, often
2.888 + just by canonical automated tools such as ``@{command "by"}~@{text
2.889 + simp}'' or ``@{command "by"}~@{text blast}''. Accordingly, the
2.890 + ``@{text that}'' reduction above is declared as simplification and
2.891 + introduction rule.
2.892 +
2.893 + In a sense, @{command "obtain"} represents at the level of Isar
2.894 + proofs what would be meta-logical existential quantifiers and
2.895 + conjunctions. This concept has a broad range of useful
2.896 + applications, ranging from plain elimination (or introduction) of
2.897 + object-level existential and conjunctions, to elimination over
2.898 + results of symbolic evaluation of recursive definitions, for
2.899 + example. Also note that @{command "obtain"} without parameters acts
2.900 + much like @{command "have"}, where the result is treated as a
2.901 + genuine assumption.
2.902 +
2.903 + An alternative name to be used instead of ``@{text that}'' above may
2.904 + be given in parentheses.
2.905 +
2.906 + \medskip The improper variant @{command "guess"} is similar to
2.907 + @{command "obtain"}, but derives the obtained statement from the
2.908 + course of reasoning! The proof starts with a fixed goal @{text
2.909 + thesis}. The subsequent proof may refine this to anything of the
2.910 + form like @{text "\<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots>
2.911 + \<phi>\<^sub>n \<Longrightarrow> thesis"}, but must not introduce new subgoals. The
2.912 + final goal state is then used as reduction rule for the obtain
2.913 + scheme described above. Obtained parameters @{text "x\<^sub>1, \<dots>,
2.914 + x\<^sub>m"} are marked as internal by default, which prevents the
2.915 + proof context from being polluted by ad-hoc variables. The variable
2.916 + names and type constraints given as arguments for @{command "guess"}
2.917 + specify a prefix of obtained parameters explicitly in the text.
2.918 +
2.919 + It is important to note that the facts introduced by @{command
2.920 + "obtain"} and @{command "guess"} may not be polymorphic: any
2.921 + type-variables occurring here are fixed in the present context!
2.922 +*}
2.923 +
2.924 +
2.925 +section {* Calculational reasoning \label{sec:calculation} *}
2.926 +
2.927 +text {*
2.928 + \begin{matharray}{rcl}
2.929 + @{command_def "also"} & : & \isartrans{proof(state)}{proof(state)} \\
2.930 + @{command_def "finally"} & : & \isartrans{proof(state)}{proof(chain)} \\
2.931 + @{command_def "moreover"} & : & \isartrans{proof(state)}{proof(state)} \\
2.932 + @{command_def "ultimately"} & : & \isartrans{proof(state)}{proof(chain)} \\
2.933 + @{command_def "print_trans_rules"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
2.934 + @{attribute trans} & : & \isaratt \\
2.935 + @{attribute sym} & : & \isaratt \\
2.936 + @{attribute symmetric} & : & \isaratt \\
2.937 + \end{matharray}
2.938 +
2.939 + Calculational proof is forward reasoning with implicit application
2.940 + of transitivity rules (such those of @{text "="}, @{text "\<le>"},
2.941 + @{text "<"}). Isabelle/Isar maintains an auxiliary fact register
2.942 + @{fact_ref calculation} for accumulating results obtained by
2.943 + transitivity composed with the current result. Command @{command
2.944 + "also"} updates @{fact calculation} involving @{fact this}, while
2.945 + @{command "finally"} exhibits the final @{fact calculation} by
2.946 + forward chaining towards the next goal statement. Both commands
2.947 + require valid current facts, i.e.\ may occur only after commands
2.948 + that produce theorems such as @{command "assume"}, @{command
2.949 + "note"}, or some finished proof of @{command "have"}, @{command
2.950 + "show"} etc. The @{command "moreover"} and @{command "ultimately"}
2.951 + commands are similar to @{command "also"} and @{command "finally"},
2.952 + but only collect further results in @{fact calculation} without
2.953 + applying any rules yet.
2.954 +
2.955 + Also note that the implicit term abbreviation ``@{text "\<dots>"}'' has
2.956 + its canonical application with calculational proofs. It refers to
2.957 + the argument of the preceding statement. (The argument of a curried
2.958 + infix expression happens to be its right-hand side.)
2.959 +
2.960 + Isabelle/Isar calculations are implicitly subject to block structure
2.961 + in the sense that new threads of calculational reasoning are
2.962 + commenced for any new block (as opened by a local goal, for
2.963 + example). This means that, apart from being able to nest
2.964 + calculations, there is no separate \emph{begin-calculation} command
2.965 + required.
2.966 +
2.967 + \medskip The Isar calculation proof commands may be defined as
2.968 + follows:\footnote{We suppress internal bookkeeping such as proper
2.969 + handling of block-structure.}
2.970 +
2.971 + \begin{matharray}{rcl}
2.972 + @{command "also"}@{text "\<^sub>0"} & \equiv & @{command "note"}~@{text "calculation = this"} \\
2.973 + @{command "also"}@{text "\<^sub>n\<^sub>+\<^sub>1"} & \equiv & @{command "note"}~@{text "calculation = trans [OF calculation this]"} \\[0.5ex]
2.974 + @{command "finally"} & \equiv & @{command "also"}~@{command "from"}~@{text calculation} \\[0.5ex]
2.975 + @{command "moreover"} & \equiv & @{command "note"}~@{text "calculation = calculation this"} \\
2.976 + @{command "ultimately"} & \equiv & @{command "moreover"}~@{command "from"}~@{text calculation} \\
2.977 + \end{matharray}
2.978 +
2.979 + \begin{rail}
2.980 + ('also' | 'finally') ('(' thmrefs ')')?
2.981 + ;
2.982 + 'trans' (() | 'add' | 'del')
2.983 + ;
2.984 + \end{rail}
2.985 +
2.986 + \begin{descr}
2.987 +
2.988 + \item [@{command "also"}~@{text "(a\<^sub>1 \<dots> a\<^sub>n)"}]
2.989 + maintains the auxiliary @{fact calculation} register as follows.
2.990 + The first occurrence of @{command "also"} in some calculational
2.991 + thread initializes @{fact calculation} by @{fact this}. Any
2.992 + subsequent @{command "also"} on the same level of block-structure
2.993 + updates @{fact calculation} by some transitivity rule applied to
2.994 + @{fact calculation} and @{fact this} (in that order). Transitivity
2.995 + rules are picked from the current context, unless alternative rules
2.996 + are given as explicit arguments.
2.997 +
2.998 + \item [@{command "finally"}~@{text "(a\<^sub>1 \<dots> a\<^sub>n)"}]
2.999 + maintaining @{fact calculation} in the same way as @{command
2.1000 + "also"}, and concludes the current calculational thread. The final
2.1001 + result is exhibited as fact for forward chaining towards the next
2.1002 + goal. Basically, @{command "finally"} just abbreviates @{command
2.1003 + "also"}~@{command "from"}~@{fact calculation}. Typical idioms for
2.1004 + concluding calculational proofs are ``@{command "finally"}~@{command
2.1005 + "show"}~@{text ?thesis}~@{command "."}'' and ``@{command
2.1006 + "finally"}~@{command "have"}~@{text \<phi>}~@{command "."}''.
2.1007 +
2.1008 + \item [@{command "moreover"} and @{command "ultimately"}] are
2.1009 + analogous to @{command "also"} and @{command "finally"}, but collect
2.1010 + results only, without applying rules.
2.1011 +
2.1012 + \item [@{command "print_trans_rules"}] prints the list of
2.1013 + transitivity rules (for calculational commands @{command "also"} and
2.1014 + @{command "finally"}) and symmetry rules (for the @{attribute
2.1015 + symmetric} operation and single step elimination patters) of the
2.1016 + current context.
2.1017 +
2.1018 + \item [@{attribute trans}] declares theorems as transitivity rules.
2.1019 +
2.1020 + \item [@{attribute sym}] declares symmetry rules, as well as
2.1021 + @{attribute "Pure.elim?"} rules.
2.1022 +
2.1023 + \item [@{attribute symmetric}] resolves a theorem with some rule
2.1024 + declared as @{attribute sym} in the current context. For example,
2.1025 + ``@{command "assume"}~@{text "[symmetric]: x = y"}'' produces a
2.1026 + swapped fact derived from that assumption.
2.1027 +
2.1028 + In structured proof texts it is often more appropriate to use an
2.1029 + explicit single-step elimination proof, such as ``@{command
2.1030 + "assume"}~@{text "x = y"}~@{command "then"}~@{command "have"}~@{text
2.1031 + "y = x"}~@{command ".."}''.
2.1032 +
2.1033 + \end{descr}
2.1034 +*}
2.1035 +
2.1036 end
3.1 --- a/doc-src/IsarRef/Thy/Spec.thy Fri May 09 23:35:57 2008 +0200
3.2 +++ b/doc-src/IsarRef/Thy/Spec.thy Sat May 10 00:14:00 2008 +0200
3.3 @@ -6,4 +6,69 @@
3.4
3.5 chapter {* Specifications *}
3.6
3.7 +section {* Defining theories \label{sec:begin-thy} *}
3.8 +
3.9 +text {*
3.10 + \begin{matharray}{rcl}
3.11 + @{command_def "header"} & : & \isarkeep{toplevel} \\
3.12 + @{command_def "theory"} & : & \isartrans{toplevel}{theory} \\
3.13 + @{command_def "end"} & : & \isartrans{theory}{toplevel} \\
3.14 + \end{matharray}
3.15 +
3.16 + Isabelle/Isar theories are defined via theory, which contain both
3.17 + specifications and proofs; occasionally definitional mechanisms also
3.18 + require some explicit proof.
3.19 +
3.20 + The first ``real'' command of any theory has to be @{command
3.21 + "theory"}, which starts a new theory based on the merge of existing
3.22 + ones. Just preceding the @{command "theory"} keyword, there may be
3.23 + an optional @{command "header"} declaration, which is relevant to
3.24 + document preparation only; it acts very much like a special
3.25 + pre-theory markup command (cf.\ \secref{sec:markup-thy} and
3.26 + \secref{sec:markup-thy}). The @{command "end"} command concludes a
3.27 + theory development; it has to be the very last command of any theory
3.28 + file loaded in batch-mode.
3.29 +
3.30 + \begin{rail}
3.31 + 'header' text
3.32 + ;
3.33 + 'theory' name 'imports' (name +) uses? 'begin'
3.34 + ;
3.35 +
3.36 + uses: 'uses' ((name | parname) +);
3.37 + \end{rail}
3.38 +
3.39 + \begin{descr}
3.40 +
3.41 + \item [@{command "header"}~@{text "text"}] provides plain text
3.42 + markup just preceding the formal beginning of a theory. In actual
3.43 + document preparation the corresponding {\LaTeX} macro @{verbatim
3.44 + "\\isamarkupheader"} may be redefined to produce chapter or section
3.45 + headings. See also \secref{sec:markup-thy} and
3.46 + \secref{sec:markup-prf} for further markup commands.
3.47 +
3.48 + \item [@{command "theory"}~@{text "A \<IMPORTS> B\<^sub>1 \<dots>
3.49 + B\<^sub>n \<BEGIN>"}] starts a new theory @{text A} based on the
3.50 + merge of existing theories @{text "B\<^sub>1 \<dots> B\<^sub>n"}.
3.51 +
3.52 + Due to inclusion of several ancestors, the overall theory structure
3.53 + emerging in an Isabelle session forms a directed acyclic graph
3.54 + (DAG). Isabelle's theory loader ensures that the sources
3.55 + contributing to the development graph are always up-to-date.
3.56 + Changed files are automatically reloaded when processing theory
3.57 + headers.
3.58 +
3.59 + The optional @{keyword_def "uses"} specification declares additional
3.60 + dependencies on extra files (usually ML sources). Files will be
3.61 + loaded immediately (as ML), unless the name is put in parentheses,
3.62 + which merely documents the dependency to be resolved later in the
3.63 + text (typically via explicit @{command_ref "use"} in the body text,
3.64 + see \secref{sec:ML}).
3.65 +
3.66 + \item [@{command "end"}] concludes the current theory definition or
3.67 + context switch.
3.68 +
3.69 + \end{descr}
3.70 +*}
3.71 +
3.72 end
4.1 --- a/doc-src/IsarRef/Thy/document/Generic.tex Fri May 09 23:35:57 2008 +0200
4.2 +++ b/doc-src/IsarRef/Thy/document/Generic.tex Sat May 10 00:14:00 2008 +0200
4.3 @@ -790,191 +790,6 @@
4.4 \end{isamarkuptext}%
4.5 \isamarkuptrue%
4.6 %
4.7 -\isamarkupsection{Derived proof schemes%
4.8 -}
4.9 -\isamarkuptrue%
4.10 -%
4.11 -\isamarkupsubsection{Generalized elimination \label{sec:obtain}%
4.12 -}
4.13 -\isamarkuptrue%
4.14 -%
4.15 -\begin{isamarkuptext}%
4.16 -\begin{matharray}{rcl}
4.17 - \indexdef{}{command}{obtain}\mbox{\isa{\isacommand{obtain}}} & : & \isartrans{proof(state)}{proof(prove)} \\
4.18 - \indexdef{}{command}{guess}\mbox{\isa{\isacommand{guess}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isartrans{proof(state)}{proof(prove)} \\
4.19 - \end{matharray}
4.20 -
4.21 - Generalized elimination means that additional elements with certain
4.22 - properties may be introduced in the current context, by virtue of a
4.23 - locally proven ``soundness statement''. Technically speaking, the
4.24 - \mbox{\isa{\isacommand{obtain}}} language element is like a declaration of
4.25 - \mbox{\isa{\isacommand{fix}}} and \mbox{\isa{\isacommand{assume}}} (see also see
4.26 - \secref{sec:proof-context}), together with a soundness proof of its
4.27 - additional claim. According to the nature of existential reasoning,
4.28 - assumptions get eliminated from any result exported from the context
4.29 - later, provided that the corresponding parameters do \emph{not}
4.30 - occur in the conclusion.
4.31 -
4.32 - \begin{rail}
4.33 - 'obtain' parname? (vars + 'and') 'where' (props + 'and')
4.34 - ;
4.35 - 'guess' (vars + 'and')
4.36 - ;
4.37 - \end{rail}
4.38 -
4.39 - The derived Isar command \mbox{\isa{\isacommand{obtain}}} is defined as follows
4.40 - (where \isa{{\isachardoublequote}b\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub k{\isachardoublequote}} shall refer to (optional)
4.41 - facts indicated for forward chaining).
4.42 - \begin{matharray}{l}
4.43 - \isa{{\isachardoublequote}{\isasymlangle}using\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub k{\isasymrangle}{\isachardoublequote}}~~\mbox{\isa{\isacommand{obtain}}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m\ {\isasymWHERE}\ a{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n\ \ {\isasymlangle}proof{\isasymrangle}\ {\isasymequiv}{\isachardoublequote}} \\[1ex]
4.44 - \quad \mbox{\isa{\isacommand{have}}}~\isa{{\isachardoublequote}{\isasymAnd}thesis{\isachardot}\ {\isacharparenleft}{\isasymAnd}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardot}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymphi}\isactrlsub n\ {\isasymLongrightarrow}\ thesis{\isacharparenright}\ {\isasymLongrightarrow}\ thesis{\isachardoublequote}} \\
4.45 - \quad \mbox{\isa{\isacommand{proof}}}~\isa{succeed} \\
4.46 - \qquad \mbox{\isa{\isacommand{fix}}}~\isa{thesis} \\
4.47 - \qquad \mbox{\isa{\isacommand{assume}}}~\isa{{\isachardoublequote}that\ {\isacharbrackleft}Pure{\isachardot}intro{\isacharquery}{\isacharbrackright}{\isacharcolon}\ {\isasymAnd}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardot}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymphi}\isactrlsub n\ {\isasymLongrightarrow}\ thesis{\isachardoublequote}} \\
4.48 - \qquad \mbox{\isa{\isacommand{then}}}~\mbox{\isa{\isacommand{show}}}~\isa{thesis} \\
4.49 - \quad\qquad \mbox{\isa{\isacommand{apply}}}~\isa{{\isacharminus}} \\
4.50 - \quad\qquad \mbox{\isa{\isacommand{using}}}~\isa{{\isachardoublequote}b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub k\ \ {\isasymlangle}proof{\isasymrangle}{\isachardoublequote}} \\
4.51 - \quad \mbox{\isa{\isacommand{qed}}} \\
4.52 - \quad \mbox{\isa{\isacommand{fix}}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardoublequote}}~\mbox{\isa{\isacommand{assume}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}\ a{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}} \\
4.53 - \end{matharray}
4.54 -
4.55 - Typically, the soundness proof is relatively straight-forward, often
4.56 - just by canonical automated tools such as ``\mbox{\isa{\isacommand{by}}}~\isa{simp}'' or ``\mbox{\isa{\isacommand{by}}}~\isa{blast}''. Accordingly, the
4.57 - ``\isa{that}'' reduction above is declared as simplification and
4.58 - introduction rule.
4.59 -
4.60 - In a sense, \mbox{\isa{\isacommand{obtain}}} represents at the level of Isar
4.61 - proofs what would be meta-logical existential quantifiers and
4.62 - conjunctions. This concept has a broad range of useful
4.63 - applications, ranging from plain elimination (or introduction) of
4.64 - object-level existential and conjunctions, to elimination over
4.65 - results of symbolic evaluation of recursive definitions, for
4.66 - example. Also note that \mbox{\isa{\isacommand{obtain}}} without parameters acts
4.67 - much like \mbox{\isa{\isacommand{have}}}, where the result is treated as a
4.68 - genuine assumption.
4.69 -
4.70 - An alternative name to be used instead of ``\isa{that}'' above may
4.71 - be given in parentheses.
4.72 -
4.73 - \medskip The improper variant \mbox{\isa{\isacommand{guess}}} is similar to
4.74 - \mbox{\isa{\isacommand{obtain}}}, but derives the obtained statement from the
4.75 - course of reasoning! The proof starts with a fixed goal \isa{thesis}. The subsequent proof may refine this to anything of the
4.76 - form like \isa{{\isachardoublequote}{\isasymAnd}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardot}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymphi}\isactrlsub n\ {\isasymLongrightarrow}\ thesis{\isachardoublequote}}, but must not introduce new subgoals. The
4.77 - final goal state is then used as reduction rule for the obtain
4.78 - scheme described above. Obtained parameters \isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub m{\isachardoublequote}} are marked as internal by default, which prevents the
4.79 - proof context from being polluted by ad-hoc variables. The variable
4.80 - names and type constraints given as arguments for \mbox{\isa{\isacommand{guess}}}
4.81 - specify a prefix of obtained parameters explicitly in the text.
4.82 -
4.83 - It is important to note that the facts introduced by \mbox{\isa{\isacommand{obtain}}} and \mbox{\isa{\isacommand{guess}}} may not be polymorphic: any
4.84 - type-variables occurring here are fixed in the present context!%
4.85 -\end{isamarkuptext}%
4.86 -\isamarkuptrue%
4.87 -%
4.88 -\isamarkupsubsection{Calculational reasoning \label{sec:calculation}%
4.89 -}
4.90 -\isamarkuptrue%
4.91 -%
4.92 -\begin{isamarkuptext}%
4.93 -\begin{matharray}{rcl}
4.94 - \indexdef{}{command}{also}\mbox{\isa{\isacommand{also}}} & : & \isartrans{proof(state)}{proof(state)} \\
4.95 - \indexdef{}{command}{finally}\mbox{\isa{\isacommand{finally}}} & : & \isartrans{proof(state)}{proof(chain)} \\
4.96 - \indexdef{}{command}{moreover}\mbox{\isa{\isacommand{moreover}}} & : & \isartrans{proof(state)}{proof(state)} \\
4.97 - \indexdef{}{command}{ultimately}\mbox{\isa{\isacommand{ultimately}}} & : & \isartrans{proof(state)}{proof(chain)} \\
4.98 - \indexdef{}{command}{print\_trans\_rules}\mbox{\isa{\isacommand{print{\isacharunderscore}trans{\isacharunderscore}rules}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
4.99 - \mbox{\isa{trans}} & : & \isaratt \\
4.100 - \mbox{\isa{sym}} & : & \isaratt \\
4.101 - \mbox{\isa{symmetric}} & : & \isaratt \\
4.102 - \end{matharray}
4.103 -
4.104 - Calculational proof is forward reasoning with implicit application
4.105 - of transitivity rules (such those of \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}}, \isa{{\isachardoublequote}{\isasymle}{\isachardoublequote}},
4.106 - \isa{{\isachardoublequote}{\isacharless}{\isachardoublequote}}). Isabelle/Isar maintains an auxiliary fact register
4.107 - \indexref{}{fact}{calculation}\mbox{\isa{calculation}} for accumulating results obtained by
4.108 - transitivity composed with the current result. Command \mbox{\isa{\isacommand{also}}} updates \mbox{\isa{calculation}} involving \mbox{\isa{this}}, while
4.109 - \mbox{\isa{\isacommand{finally}}} exhibits the final \mbox{\isa{calculation}} by
4.110 - forward chaining towards the next goal statement. Both commands
4.111 - require valid current facts, i.e.\ may occur only after commands
4.112 - that produce theorems such as \mbox{\isa{\isacommand{assume}}}, \mbox{\isa{\isacommand{note}}}, or some finished proof of \mbox{\isa{\isacommand{have}}}, \mbox{\isa{\isacommand{show}}} etc. The \mbox{\isa{\isacommand{moreover}}} and \mbox{\isa{\isacommand{ultimately}}}
4.113 - commands are similar to \mbox{\isa{\isacommand{also}}} and \mbox{\isa{\isacommand{finally}}},
4.114 - but only collect further results in \mbox{\isa{calculation}} without
4.115 - applying any rules yet.
4.116 -
4.117 - Also note that the implicit term abbreviation ``\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}'' has
4.118 - its canonical application with calculational proofs. It refers to
4.119 - the argument of the preceding statement. (The argument of a curried
4.120 - infix expression happens to be its right-hand side.)
4.121 -
4.122 - Isabelle/Isar calculations are implicitly subject to block structure
4.123 - in the sense that new threads of calculational reasoning are
4.124 - commenced for any new block (as opened by a local goal, for
4.125 - example). This means that, apart from being able to nest
4.126 - calculations, there is no separate \emph{begin-calculation} command
4.127 - required.
4.128 -
4.129 - \medskip The Isar calculation proof commands may be defined as
4.130 - follows:\footnote{We suppress internal bookkeeping such as proper
4.131 - handling of block-structure.}
4.132 -
4.133 - \begin{matharray}{rcl}
4.134 - \mbox{\isa{\isacommand{also}}}\isa{{\isachardoublequote}\isactrlsub {\isadigit{0}}{\isachardoublequote}} & \equiv & \mbox{\isa{\isacommand{note}}}~\isa{{\isachardoublequote}calculation\ {\isacharequal}\ this{\isachardoublequote}} \\
4.135 - \mbox{\isa{\isacommand{also}}}\isa{{\isachardoublequote}\isactrlsub n\isactrlsub {\isacharplus}\isactrlsub {\isadigit{1}}{\isachardoublequote}} & \equiv & \mbox{\isa{\isacommand{note}}}~\isa{{\isachardoublequote}calculation\ {\isacharequal}\ trans\ {\isacharbrackleft}OF\ calculation\ this{\isacharbrackright}{\isachardoublequote}} \\[0.5ex]
4.136 - \mbox{\isa{\isacommand{finally}}} & \equiv & \mbox{\isa{\isacommand{also}}}~\mbox{\isa{\isacommand{from}}}~\isa{calculation} \\[0.5ex]
4.137 - \mbox{\isa{\isacommand{moreover}}} & \equiv & \mbox{\isa{\isacommand{note}}}~\isa{{\isachardoublequote}calculation\ {\isacharequal}\ calculation\ this{\isachardoublequote}} \\
4.138 - \mbox{\isa{\isacommand{ultimately}}} & \equiv & \mbox{\isa{\isacommand{moreover}}}~\mbox{\isa{\isacommand{from}}}~\isa{calculation} \\
4.139 - \end{matharray}
4.140 -
4.141 - \begin{rail}
4.142 - ('also' | 'finally') ('(' thmrefs ')')?
4.143 - ;
4.144 - 'trans' (() | 'add' | 'del')
4.145 - ;
4.146 - \end{rail}
4.147 -
4.148 - \begin{descr}
4.149 -
4.150 - \item [\mbox{\isa{\isacommand{also}}}~\isa{{\isachardoublequote}{\isacharparenleft}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharparenright}{\isachardoublequote}}]
4.151 - maintains the auxiliary \mbox{\isa{calculation}} register as follows.
4.152 - The first occurrence of \mbox{\isa{\isacommand{also}}} in some calculational
4.153 - thread initializes \mbox{\isa{calculation}} by \mbox{\isa{this}}. Any
4.154 - subsequent \mbox{\isa{\isacommand{also}}} on the same level of block-structure
4.155 - updates \mbox{\isa{calculation}} by some transitivity rule applied to
4.156 - \mbox{\isa{calculation}} and \mbox{\isa{this}} (in that order). Transitivity
4.157 - rules are picked from the current context, unless alternative rules
4.158 - are given as explicit arguments.
4.159 -
4.160 - \item [\mbox{\isa{\isacommand{finally}}}~\isa{{\isachardoublequote}{\isacharparenleft}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharparenright}{\isachardoublequote}}]
4.161 - maintaining \mbox{\isa{calculation}} in the same way as \mbox{\isa{\isacommand{also}}}, and concludes the current calculational thread. The final
4.162 - result is exhibited as fact for forward chaining towards the next
4.163 - goal. Basically, \mbox{\isa{\isacommand{finally}}} just abbreviates \mbox{\isa{\isacommand{also}}}~\mbox{\isa{\isacommand{from}}}~\mbox{\isa{calculation}}. Typical idioms for
4.164 - concluding calculational proofs are ``\mbox{\isa{\isacommand{finally}}}~\mbox{\isa{\isacommand{show}}}~\isa{{\isacharquery}thesis}~\mbox{\isa{\isacommand{{\isachardot}}}}'' and ``\mbox{\isa{\isacommand{finally}}}~\mbox{\isa{\isacommand{have}}}~\isa{{\isasymphi}}~\mbox{\isa{\isacommand{{\isachardot}}}}''.
4.165 -
4.166 - \item [\mbox{\isa{\isacommand{moreover}}} and \mbox{\isa{\isacommand{ultimately}}}] are
4.167 - analogous to \mbox{\isa{\isacommand{also}}} and \mbox{\isa{\isacommand{finally}}}, but collect
4.168 - results only, without applying rules.
4.169 -
4.170 - \item [\mbox{\isa{\isacommand{print{\isacharunderscore}trans{\isacharunderscore}rules}}}] prints the list of
4.171 - transitivity rules (for calculational commands \mbox{\isa{\isacommand{also}}} and
4.172 - \mbox{\isa{\isacommand{finally}}}) and symmetry rules (for the \mbox{\isa{symmetric}} operation and single step elimination patters) of the
4.173 - current context.
4.174 -
4.175 - \item [\mbox{\isa{trans}}] declares theorems as transitivity rules.
4.176 -
4.177 - \item [\mbox{\isa{sym}}] declares symmetry rules, as well as
4.178 - \mbox{\isa{Pure{\isachardot}elim{\isacharquery}}} rules.
4.179 -
4.180 - \item [\mbox{\isa{symmetric}}] resolves a theorem with some rule
4.181 - declared as \mbox{\isa{sym}} in the current context. For example,
4.182 - ``\mbox{\isa{\isacommand{assume}}}~\isa{{\isachardoublequote}{\isacharbrackleft}symmetric{\isacharbrackright}{\isacharcolon}\ x\ {\isacharequal}\ y{\isachardoublequote}}'' produces a
4.183 - swapped fact derived from that assumption.
4.184 -
4.185 - In structured proof texts it is often more appropriate to use an
4.186 - explicit single-step elimination proof, such as ``\mbox{\isa{\isacommand{assume}}}~\isa{{\isachardoublequote}x\ {\isacharequal}\ y{\isachardoublequote}}~\mbox{\isa{\isacommand{then}}}~\mbox{\isa{\isacommand{have}}}~\isa{{\isachardoublequote}y\ {\isacharequal}\ x{\isachardoublequote}}~\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}''.
4.187 -
4.188 - \end{descr}%
4.189 -\end{isamarkuptext}%
4.190 -\isamarkuptrue%
4.191 -%
4.192 \isamarkupsection{Proof tools%
4.193 }
4.194 \isamarkuptrue%
5.1 --- a/doc-src/IsarRef/Thy/document/Proof.tex Fri May 09 23:35:57 2008 +0200
5.2 +++ b/doc-src/IsarRef/Thy/document/Proof.tex Sat May 10 00:14:00 2008 +0200
5.3 @@ -24,6 +24,997 @@
5.4 }
5.5 \isamarkuptrue%
5.6 %
5.7 +\begin{isamarkuptext}%
5.8 +Proof commands perform transitions of Isar/VM machine
5.9 + configurations, which are block-structured, consisting of a stack of
5.10 + nodes with three main components: logical proof context, current
5.11 + facts, and open goals. Isar/VM transitions are \emph{typed}
5.12 + according to the following three different modes of operation:
5.13 +
5.14 + \begin{descr}
5.15 +
5.16 + \item [\isa{{\isachardoublequote}proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}}] means that a new goal has just been
5.17 + stated that is now to be \emph{proven}; the next command may refine
5.18 + it by some proof method, and enter a sub-proof to establish the
5.19 + actual result.
5.20 +
5.21 + \item [\isa{{\isachardoublequote}proof{\isacharparenleft}state{\isacharparenright}{\isachardoublequote}}] is like a nested theory mode: the
5.22 + context may be augmented by \emph{stating} additional assumptions,
5.23 + intermediate results etc.
5.24 +
5.25 + \item [\isa{{\isachardoublequote}proof{\isacharparenleft}chain{\isacharparenright}{\isachardoublequote}}] is intermediate between \isa{{\isachardoublequote}proof{\isacharparenleft}state{\isacharparenright}{\isachardoublequote}} and \isa{{\isachardoublequote}proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}}: existing facts (i.e.\
5.26 + the contents of the special ``\indexref{}{fact}{this}\mbox{\isa{this}}'' register) have been
5.27 + just picked up in order to be used when refining the goal claimed
5.28 + next.
5.29 +
5.30 + \end{descr}
5.31 +
5.32 + The proof mode indicator may be read as a verb telling the writer
5.33 + what kind of operation may be performed next. The corresponding
5.34 + typings of proof commands restricts the shape of well-formed proof
5.35 + texts to particular command sequences. So dynamic arrangements of
5.36 + commands eventually turn out as static texts of a certain structure.
5.37 + \Appref{ap:refcard} gives a simplified grammar of the overall
5.38 + (extensible) language emerging that way.%
5.39 +\end{isamarkuptext}%
5.40 +\isamarkuptrue%
5.41 +%
5.42 +\isamarkupsection{Context elements \label{sec:proof-context}%
5.43 +}
5.44 +\isamarkuptrue%
5.45 +%
5.46 +\begin{isamarkuptext}%
5.47 +\begin{matharray}{rcl}
5.48 + \indexdef{}{command}{fix}\mbox{\isa{\isacommand{fix}}} & : & \isartrans{proof(state)}{proof(state)} \\
5.49 + \indexdef{}{command}{assume}\mbox{\isa{\isacommand{assume}}} & : & \isartrans{proof(state)}{proof(state)} \\
5.50 + \indexdef{}{command}{presume}\mbox{\isa{\isacommand{presume}}} & : & \isartrans{proof(state)}{proof(state)} \\
5.51 + \indexdef{}{command}{def}\mbox{\isa{\isacommand{def}}} & : & \isartrans{proof(state)}{proof(state)} \\
5.52 + \end{matharray}
5.53 +
5.54 + The logical proof context consists of fixed variables and
5.55 + assumptions. The former closely correspond to Skolem constants, or
5.56 + meta-level universal quantification as provided by the Isabelle/Pure
5.57 + logical framework. Introducing some \emph{arbitrary, but fixed}
5.58 + variable via ``\mbox{\isa{\isacommand{fix}}}~\isa{x}'' results in a local value
5.59 + that may be used in the subsequent proof as any other variable or
5.60 + constant. Furthermore, any result \isa{{\isachardoublequote}{\isasymturnstile}\ {\isasymphi}{\isacharbrackleft}x{\isacharbrackright}{\isachardoublequote}} exported from
5.61 + the context will be universally closed wrt.\ \isa{x} at the
5.62 + outermost level: \isa{{\isachardoublequote}{\isasymturnstile}\ {\isasymAnd}x{\isachardot}\ {\isasymphi}{\isacharbrackleft}x{\isacharbrackright}{\isachardoublequote}} (this is expressed in normal
5.63 + form using Isabelle's meta-variables).
5.64 +
5.65 + Similarly, introducing some assumption \isa{{\isasymchi}} has two effects.
5.66 + On the one hand, a local theorem is created that may be used as a
5.67 + fact in subsequent proof steps. On the other hand, any result
5.68 + \isa{{\isachardoublequote}{\isasymchi}\ {\isasymturnstile}\ {\isasymphi}{\isachardoublequote}} exported from the context becomes conditional wrt.\
5.69 + the assumption: \isa{{\isachardoublequote}{\isasymturnstile}\ {\isasymchi}\ {\isasymLongrightarrow}\ {\isasymphi}{\isachardoublequote}}. Thus, solving an enclosing goal
5.70 + using such a result would basically introduce a new subgoal stemming
5.71 + from the assumption. How this situation is handled depends on the
5.72 + version of assumption command used: while \mbox{\isa{\isacommand{assume}}}
5.73 + insists on solving the subgoal by unification with some premise of
5.74 + the goal, \mbox{\isa{\isacommand{presume}}} leaves the subgoal unchanged in order
5.75 + to be proved later by the user.
5.76 +
5.77 + Local definitions, introduced by ``\mbox{\isa{\isacommand{def}}}~\isa{{\isachardoublequote}x\ {\isasymequiv}\ t{\isachardoublequote}}'', are achieved by combining ``\mbox{\isa{\isacommand{fix}}}~\isa{x}'' with
5.78 + another version of assumption that causes any hypothetical equation
5.79 + \isa{{\isachardoublequote}x\ {\isasymequiv}\ t{\isachardoublequote}} to be eliminated by the reflexivity rule. Thus,
5.80 + exporting some result \isa{{\isachardoublequote}x\ {\isasymequiv}\ t\ {\isasymturnstile}\ {\isasymphi}{\isacharbrackleft}x{\isacharbrackright}{\isachardoublequote}} yields \isa{{\isachardoublequote}{\isasymturnstile}\ {\isasymphi}{\isacharbrackleft}t{\isacharbrackright}{\isachardoublequote}}.
5.81 +
5.82 + \begin{rail}
5.83 + 'fix' (vars + 'and')
5.84 + ;
5.85 + ('assume' | 'presume') (props + 'and')
5.86 + ;
5.87 + 'def' (def + 'and')
5.88 + ;
5.89 + def: thmdecl? \\ name ('==' | equiv) term termpat?
5.90 + ;
5.91 + \end{rail}
5.92 +
5.93 + \begin{descr}
5.94 +
5.95 + \item [\mbox{\isa{\isacommand{fix}}}~\isa{x}] introduces a local variable
5.96 + \isa{x} that is \emph{arbitrary, but fixed.}
5.97 +
5.98 + \item [\mbox{\isa{\isacommand{assume}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} and \mbox{\isa{\isacommand{presume}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}}] introduce a local fact \isa{{\isachardoublequote}{\isasymphi}\ {\isasymturnstile}\ {\isasymphi}{\isachardoublequote}} by
5.99 + assumption. Subsequent results applied to an enclosing goal (e.g.\
5.100 + by \indexref{}{command}{show}\mbox{\isa{\isacommand{show}}}) are handled as follows: \mbox{\isa{\isacommand{assume}}} expects to be able to unify with existing premises in the
5.101 + goal, while \mbox{\isa{\isacommand{presume}}} leaves \isa{{\isasymphi}} as new subgoals.
5.102 +
5.103 + Several lists of assumptions may be given (separated by
5.104 + \indexref{}{keyword}{and}\mbox{\isa{\isakeyword{and}}}; the resulting list of current facts consists
5.105 + of all of these concatenated.
5.106 +
5.107 + \item [\mbox{\isa{\isacommand{def}}}~\isa{{\isachardoublequote}x\ {\isasymequiv}\ t{\isachardoublequote}}] introduces a local
5.108 + (non-polymorphic) definition. In results exported from the context,
5.109 + \isa{x} is replaced by \isa{t}. Basically, ``\mbox{\isa{\isacommand{def}}}~\isa{{\isachardoublequote}x\ {\isasymequiv}\ t{\isachardoublequote}}'' abbreviates ``\mbox{\isa{\isacommand{fix}}}~\isa{x}~\mbox{\isa{\isacommand{assume}}}~\isa{{\isachardoublequote}x\ {\isasymequiv}\ t{\isachardoublequote}}'', with the resulting
5.110 + hypothetical equation solved by reflexivity.
5.111 +
5.112 + The default name for the definitional equation is \isa{x{\isacharunderscore}def}.
5.113 + Several simultaneous definitions may be given at the same time.
5.114 +
5.115 + \end{descr}
5.116 +
5.117 + The special name \indexref{}{fact}{prems}\mbox{\isa{prems}} refers to all assumptions of the
5.118 + current context as a list of theorems. This feature should be used
5.119 + with great care! It is better avoided in final proof texts.%
5.120 +\end{isamarkuptext}%
5.121 +\isamarkuptrue%
5.122 +%
5.123 +\isamarkupsection{Facts and forward chaining%
5.124 +}
5.125 +\isamarkuptrue%
5.126 +%
5.127 +\begin{isamarkuptext}%
5.128 +\begin{matharray}{rcl}
5.129 + \indexdef{}{command}{note}\mbox{\isa{\isacommand{note}}} & : & \isartrans{proof(state)}{proof(state)} \\
5.130 + \indexdef{}{command}{then}\mbox{\isa{\isacommand{then}}} & : & \isartrans{proof(state)}{proof(chain)} \\
5.131 + \indexdef{}{command}{from}\mbox{\isa{\isacommand{from}}} & : & \isartrans{proof(state)}{proof(chain)} \\
5.132 + \indexdef{}{command}{with}\mbox{\isa{\isacommand{with}}} & : & \isartrans{proof(state)}{proof(chain)} \\
5.133 + \indexdef{}{command}{using}\mbox{\isa{\isacommand{using}}} & : & \isartrans{proof(prove)}{proof(prove)} \\
5.134 + \indexdef{}{command}{unfolding}\mbox{\isa{\isacommand{unfolding}}} & : & \isartrans{proof(prove)}{proof(prove)} \\
5.135 + \end{matharray}
5.136 +
5.137 + New facts are established either by assumption or proof of local
5.138 + statements. Any fact will usually be involved in further proofs,
5.139 + either as explicit arguments of proof methods, or when forward
5.140 + chaining towards the next goal via \mbox{\isa{\isacommand{then}}} (and variants);
5.141 + \mbox{\isa{\isacommand{from}}} and \mbox{\isa{\isacommand{with}}} are composite forms
5.142 + involving \mbox{\isa{\isacommand{note}}}. The \mbox{\isa{\isacommand{using}}} elements
5.143 + augments the collection of used facts \emph{after} a goal has been
5.144 + stated. Note that the special theorem name \indexref{}{fact}{this}\mbox{\isa{this}} refers
5.145 + to the most recently established facts, but only \emph{before}
5.146 + issuing a follow-up claim.
5.147 +
5.148 + \begin{rail}
5.149 + 'note' (thmdef? thmrefs + 'and')
5.150 + ;
5.151 + ('from' | 'with' | 'using' | 'unfolding') (thmrefs + 'and')
5.152 + ;
5.153 + \end{rail}
5.154 +
5.155 + \begin{descr}
5.156 +
5.157 + \item [\mbox{\isa{\isacommand{note}}}~\isa{{\isachardoublequote}a\ {\isacharequal}\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}}]
5.158 + recalls existing facts \isa{{\isachardoublequote}b\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub n{\isachardoublequote}}, binding
5.159 + the result as \isa{a}. Note that attributes may be involved as
5.160 + well, both on the left and right hand sides.
5.161 +
5.162 + \item [\mbox{\isa{\isacommand{then}}}] indicates forward chaining by the current
5.163 + facts in order to establish the goal to be claimed next. The
5.164 + initial proof method invoked to refine that will be offered the
5.165 + facts to do ``anything appropriate'' (see also
5.166 + \secref{sec:proof-steps}). For example, method \indexref{}{method}{rule}\mbox{\isa{rule}}
5.167 + (see \secref{sec:pure-meth-att}) would typically do an elimination
5.168 + rather than an introduction. Automatic methods usually insert the
5.169 + facts into the goal state before operation. This provides a simple
5.170 + scheme to control relevance of facts in automated proof search.
5.171 +
5.172 + \item [\mbox{\isa{\isacommand{from}}}~\isa{b}] abbreviates ``\mbox{\isa{\isacommand{note}}}~\isa{b}~\mbox{\isa{\isacommand{then}}}''; thus \mbox{\isa{\isacommand{then}}} is
5.173 + equivalent to ``\mbox{\isa{\isacommand{from}}}~\isa{this}''.
5.174 +
5.175 + \item [\mbox{\isa{\isacommand{with}}}~\isa{{\isachardoublequote}b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}}]
5.176 + abbreviates ``\mbox{\isa{\isacommand{from}}}~\isa{{\isachardoublequote}b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n\ {\isasymAND}\ this{\isachardoublequote}}''; thus the forward chaining is from earlier facts together
5.177 + with the current ones.
5.178 +
5.179 + \item [\mbox{\isa{\isacommand{using}}}~\isa{{\isachardoublequote}b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}}] augments
5.180 + the facts being currently indicated for use by a subsequent
5.181 + refinement step (such as \indexref{}{command}{apply}\mbox{\isa{\isacommand{apply}}} or \indexref{}{command}{proof}\mbox{\isa{\isacommand{proof}}}).
5.182 +
5.183 + \item [\mbox{\isa{\isacommand{unfolding}}}~\isa{{\isachardoublequote}b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}}] is
5.184 + structurally similar to \mbox{\isa{\isacommand{using}}}, but unfolds definitional
5.185 + equations \isa{{\isachardoublequote}b\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}} throughout the goal state
5.186 + and facts.
5.187 +
5.188 + \end{descr}
5.189 +
5.190 + Forward chaining with an empty list of theorems is the same as not
5.191 + chaining at all. Thus ``\mbox{\isa{\isacommand{from}}}~\isa{nothing}'' has no
5.192 + effect apart from entering \isa{{\isachardoublequote}prove{\isacharparenleft}chain{\isacharparenright}{\isachardoublequote}} mode, since
5.193 + \indexref{}{fact}{nothing}\mbox{\isa{nothing}} is bound to the empty list of theorems.
5.194 +
5.195 + Basic proof methods (such as \indexref{}{method}{rule}\mbox{\isa{rule}}) expect multiple
5.196 + facts to be given in their proper order, corresponding to a prefix
5.197 + of the premises of the rule involved. Note that positions may be
5.198 + easily skipped using something like \mbox{\isa{\isacommand{from}}}~\isa{{\isachardoublequote}{\isacharunderscore}\ {\isasymAND}\ a\ {\isasymAND}\ b{\isachardoublequote}}, for example. This involves the trivial rule
5.199 + \isa{{\isachardoublequote}PROP\ {\isasympsi}\ {\isasymLongrightarrow}\ PROP\ {\isasympsi}{\isachardoublequote}}, which is bound in Isabelle/Pure as
5.200 + ``\indexref{}{fact}{\_}\mbox{\isa{{\isacharunderscore}}}'' (underscore).
5.201 +
5.202 + Automated methods (such as \mbox{\isa{simp}} or \mbox{\isa{auto}}) just
5.203 + insert any given facts before their usual operation. Depending on
5.204 + the kind of procedure involved, the order of facts is less
5.205 + significant here.%
5.206 +\end{isamarkuptext}%
5.207 +\isamarkuptrue%
5.208 +%
5.209 +\isamarkupsection{Goal statements \label{sec:goals}%
5.210 +}
5.211 +\isamarkuptrue%
5.212 +%
5.213 +\begin{isamarkuptext}%
5.214 +\begin{matharray}{rcl}
5.215 + \indexdef{}{command}{lemma}\mbox{\isa{\isacommand{lemma}}} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
5.216 + \indexdef{}{command}{theorem}\mbox{\isa{\isacommand{theorem}}} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
5.217 + \indexdef{}{command}{corollary}\mbox{\isa{\isacommand{corollary}}} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
5.218 + \indexdef{}{command}{have}\mbox{\isa{\isacommand{have}}} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
5.219 + \indexdef{}{command}{show}\mbox{\isa{\isacommand{show}}} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
5.220 + \indexdef{}{command}{hence}\mbox{\isa{\isacommand{hence}}} & : & \isartrans{proof(state)}{proof(prove)} \\
5.221 + \indexdef{}{command}{thus}\mbox{\isa{\isacommand{thus}}} & : & \isartrans{proof(state)}{proof(prove)} \\
5.222 + \indexdef{}{command}{print\_statement}\mbox{\isa{\isacommand{print{\isacharunderscore}statement}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
5.223 + \end{matharray}
5.224 +
5.225 + From a theory context, proof mode is entered by an initial goal
5.226 + command such as \mbox{\isa{\isacommand{lemma}}}, \mbox{\isa{\isacommand{theorem}}}, or
5.227 + \mbox{\isa{\isacommand{corollary}}}. Within a proof, new claims may be
5.228 + introduced locally as well; four variants are available here to
5.229 + indicate whether forward chaining of facts should be performed
5.230 + initially (via \indexref{}{command}{then}\mbox{\isa{\isacommand{then}}}), and whether the final result
5.231 + is meant to solve some pending goal.
5.232 +
5.233 + Goals may consist of multiple statements, resulting in a list of
5.234 + facts eventually. A pending multi-goal is internally represented as
5.235 + a meta-level conjunction (printed as \isa{{\isachardoublequote}{\isacharampersand}{\isacharampersand}{\isachardoublequote}}), which is usually
5.236 + split into the corresponding number of sub-goals prior to an initial
5.237 + method application, via \indexref{}{command}{proof}\mbox{\isa{\isacommand{proof}}}
5.238 + (\secref{sec:proof-steps}) or \indexref{}{command}{apply}\mbox{\isa{\isacommand{apply}}}
5.239 + (\secref{sec:tactic-commands}). The \indexref{}{method}{induct}\mbox{\isa{induct}} method
5.240 + covered in \secref{sec:cases-induct} acts on multiple claims
5.241 + simultaneously.
5.242 +
5.243 + Claims at the theory level may be either in short or long form. A
5.244 + short goal merely consists of several simultaneous propositions
5.245 + (often just one). A long goal includes an explicit context
5.246 + specification for the subsequent conclusion, involving local
5.247 + parameters and assumptions. Here the role of each part of the
5.248 + statement is explicitly marked by separate keywords (see also
5.249 + \secref{sec:locale}); the local assumptions being introduced here
5.250 + are available as \indexref{}{fact}{assms}\mbox{\isa{assms}} in the proof. Moreover, there
5.251 + are two kinds of conclusions: \indexdef{}{element}{shows}\mbox{\isa{\isakeyword{shows}}} states several
5.252 + simultaneous propositions (essentially a big conjunction), while
5.253 + \indexdef{}{element}{obtains}\mbox{\isa{\isakeyword{obtains}}} claims several simultaneous simultaneous
5.254 + contexts of (essentially a big disjunction of eliminated parameters
5.255 + and assumptions, cf.\ \secref{sec:obtain}).
5.256 +
5.257 + \begin{rail}
5.258 + ('lemma' | 'theorem' | 'corollary') target? (goal | longgoal)
5.259 + ;
5.260 + ('have' | 'show' | 'hence' | 'thus') goal
5.261 + ;
5.262 + 'print\_statement' modes? thmrefs
5.263 + ;
5.264 +
5.265 + goal: (props + 'and')
5.266 + ;
5.267 + longgoal: thmdecl? (contextelem *) conclusion
5.268 + ;
5.269 + conclusion: 'shows' goal | 'obtains' (parname? case + '|')
5.270 + ;
5.271 + case: (vars + 'and') 'where' (props + 'and')
5.272 + ;
5.273 + \end{rail}
5.274 +
5.275 + \begin{descr}
5.276 +
5.277 + \item [\mbox{\isa{\isacommand{lemma}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}}] enters proof mode with
5.278 + \isa{{\isasymphi}} as main goal, eventually resulting in some fact \isa{{\isachardoublequote}{\isasymturnstile}\ {\isasymphi}{\isachardoublequote}} to be put back into the target context. An additional
5.279 + \railnonterm{context} specification may build up an initial proof
5.280 + context for the subsequent claim; this includes local definitions
5.281 + and syntax as well, see the definition of \mbox{\isa{contextelem}} in
5.282 + \secref{sec:locale}.
5.283 +
5.284 + \item [\mbox{\isa{\isacommand{theorem}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} and \mbox{\isa{\isacommand{corollary}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}}] are essentially the same as \mbox{\isa{\isacommand{lemma}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}}, but the facts are internally marked as
5.285 + being of a different kind. This discrimination acts like a formal
5.286 + comment.
5.287 +
5.288 + \item [\mbox{\isa{\isacommand{have}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}}] claims a local goal,
5.289 + eventually resulting in a fact within the current logical context.
5.290 + This operation is completely independent of any pending sub-goals of
5.291 + an enclosing goal statements, so \mbox{\isa{\isacommand{have}}} may be freely
5.292 + used for experimental exploration of potential results within a
5.293 + proof body.
5.294 +
5.295 + \item [\mbox{\isa{\isacommand{show}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}}] is like \mbox{\isa{\isacommand{have}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} plus a second stage to refine some pending
5.296 + sub-goal for each one of the finished result, after having been
5.297 + exported into the corresponding context (at the head of the
5.298 + sub-proof of this \mbox{\isa{\isacommand{show}}} command).
5.299 +
5.300 + To accommodate interactive debugging, resulting rules are printed
5.301 + before being applied internally. Even more, interactive execution
5.302 + of \mbox{\isa{\isacommand{show}}} predicts potential failure and displays the
5.303 + resulting error as a warning beforehand. Watch out for the
5.304 + following message:
5.305 +
5.306 + %FIXME proper antiquitation
5.307 + \begin{ttbox}
5.308 + Problem! Local statement will fail to solve any pending goal
5.309 + \end{ttbox}
5.310 +
5.311 + \item [\mbox{\isa{\isacommand{hence}}}] abbreviates ``\mbox{\isa{\isacommand{then}}}~\mbox{\isa{\isacommand{have}}}'', i.e.\ claims a local goal to be proven by forward
5.312 + chaining the current facts. Note that \mbox{\isa{\isacommand{hence}}} is also
5.313 + equivalent to ``\mbox{\isa{\isacommand{from}}}~\isa{this}~\mbox{\isa{\isacommand{have}}}''.
5.314 +
5.315 + \item [\mbox{\isa{\isacommand{thus}}}] abbreviates ``\mbox{\isa{\isacommand{then}}}~\mbox{\isa{\isacommand{show}}}''. Note that \mbox{\isa{\isacommand{thus}}} is also equivalent to
5.316 + ``\mbox{\isa{\isacommand{from}}}~\isa{this}~\mbox{\isa{\isacommand{show}}}''.
5.317 +
5.318 + \item [\mbox{\isa{\isacommand{print{\isacharunderscore}statement}}}~\isa{a}] prints facts from the
5.319 + current theory or proof context in long statement form, according to
5.320 + the syntax for \mbox{\isa{\isacommand{lemma}}} given above.
5.321 +
5.322 + \end{descr}
5.323 +
5.324 + Any goal statement causes some term abbreviations (such as
5.325 + \indexref{}{variable}{?thesis}\mbox{\isa{{\isacharquery}thesis}}) to be bound automatically, see also
5.326 + \secref{sec:term-abbrev}. Furthermore, the local context of a
5.327 + (non-atomic) goal is provided via the \indexref{}{case}{rule\_context}\mbox{\isa{rule{\isacharunderscore}context}} case.
5.328 +
5.329 + The optional case names of \indexref{}{element}{obtains}\mbox{\isa{\isakeyword{obtains}}} have a twofold
5.330 + meaning: (1) during the of this claim they refer to the the local
5.331 + context introductions, (2) the resulting rule is annotated
5.332 + accordingly to support symbolic case splits when used with the
5.333 + \indexref{}{method}{cases}\mbox{\isa{cases}} method (cf. \secref{sec:cases-induct}).
5.334 +
5.335 + \medskip
5.336 +
5.337 + \begin{warn}
5.338 + Isabelle/Isar suffers theory-level goal statements to contain
5.339 + \emph{unbound schematic variables}, although this does not conform
5.340 + to the aim of human-readable proof documents! The main problem
5.341 + with schematic goals is that the actual outcome is usually hard to
5.342 + predict, depending on the behavior of the proof methods applied
5.343 + during the course of reasoning. Note that most semi-automated
5.344 + methods heavily depend on several kinds of implicit rule
5.345 + declarations within the current theory context. As this would
5.346 + also result in non-compositional checking of sub-proofs,
5.347 + \emph{local goals} are not allowed to be schematic at all.
5.348 + Nevertheless, schematic goals do have their use in Prolog-style
5.349 + interactive synthesis of proven results, usually by stepwise
5.350 + refinement via emulation of traditional Isabelle tactic scripts
5.351 + (see also \secref{sec:tactic-commands}). In any case, users
5.352 + should know what they are doing.
5.353 + \end{warn}%
5.354 +\end{isamarkuptext}%
5.355 +\isamarkuptrue%
5.356 +%
5.357 +\isamarkupsection{Initial and terminal proof steps \label{sec:proof-steps}%
5.358 +}
5.359 +\isamarkuptrue%
5.360 +%
5.361 +\begin{isamarkuptext}%
5.362 +\begin{matharray}{rcl}
5.363 + \indexdef{}{command}{proof}\mbox{\isa{\isacommand{proof}}} & : & \isartrans{proof(prove)}{proof(state)} \\
5.364 + \indexdef{}{command}{qed}\mbox{\isa{\isacommand{qed}}} & : & \isartrans{proof(state)}{proof(state) ~|~ theory} \\
5.365 + \indexdef{}{command}{by}\mbox{\isa{\isacommand{by}}} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
5.366 + \indexdef{}{command}{..}\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
5.367 + \indexdef{}{command}{.}\mbox{\isa{\isacommand{{\isachardot}}}} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
5.368 + \indexdef{}{command}{sorry}\mbox{\isa{\isacommand{sorry}}} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
5.369 + \end{matharray}
5.370 +
5.371 + Arbitrary goal refinement via tactics is considered harmful.
5.372 + Structured proof composition in Isar admits proof methods to be
5.373 + invoked in two places only.
5.374 +
5.375 + \begin{enumerate}
5.376 +
5.377 + \item An \emph{initial} refinement step \indexref{}{command}{proof}\mbox{\isa{\isacommand{proof}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}{\isachardoublequote}} reduces a newly stated goal to a number
5.378 + of sub-goals that are to be solved later. Facts are passed to
5.379 + \isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}{\isachardoublequote}} for forward chaining, if so indicated by \isa{{\isachardoublequote}proof{\isacharparenleft}chain{\isacharparenright}{\isachardoublequote}} mode.
5.380 +
5.381 + \item A \emph{terminal} conclusion step \indexref{}{command}{qed}\mbox{\isa{\isacommand{qed}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{2}}{\isachardoublequote}} is intended to solve remaining goals. No facts are
5.382 + passed to \isa{{\isachardoublequote}m\isactrlsub {\isadigit{2}}{\isachardoublequote}}.
5.383 +
5.384 + \end{enumerate}
5.385 +
5.386 + The only other (proper) way to affect pending goals in a proof body
5.387 + is by \indexref{}{command}{show}\mbox{\isa{\isacommand{show}}}, which involves an explicit statement of
5.388 + what is to be solved eventually. Thus we avoid the fundamental
5.389 + problem of unstructured tactic scripts that consist of numerous
5.390 + consecutive goal transformations, with invisible effects.
5.391 +
5.392 + \medskip As a general rule of thumb for good proof style, initial
5.393 + proof methods should either solve the goal completely, or constitute
5.394 + some well-understood reduction to new sub-goals. Arbitrary
5.395 + automatic proof tools that are prone leave a large number of badly
5.396 + structured sub-goals are no help in continuing the proof document in
5.397 + an intelligible manner.
5.398 +
5.399 + Unless given explicitly by the user, the default initial method is
5.400 + ``\indexref{}{method}{rule}\mbox{\isa{rule}}'', which applies a single standard elimination
5.401 + or introduction rule according to the topmost symbol involved.
5.402 + There is no separate default terminal method. Any remaining goals
5.403 + are always solved by assumption in the very last step.
5.404 +
5.405 + \begin{rail}
5.406 + 'proof' method?
5.407 + ;
5.408 + 'qed' method?
5.409 + ;
5.410 + 'by' method method?
5.411 + ;
5.412 + ('.' | '..' | 'sorry')
5.413 + ;
5.414 + \end{rail}
5.415 +
5.416 + \begin{descr}
5.417 +
5.418 + \item [\mbox{\isa{\isacommand{proof}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}{\isachardoublequote}}] refines the goal by
5.419 + proof method \isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}{\isachardoublequote}}; facts for forward chaining are
5.420 + passed if so indicated by \isa{{\isachardoublequote}proof{\isacharparenleft}chain{\isacharparenright}{\isachardoublequote}} mode.
5.421 +
5.422 + \item [\mbox{\isa{\isacommand{qed}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{2}}{\isachardoublequote}}] refines any remaining
5.423 + goals by proof method \isa{{\isachardoublequote}m\isactrlsub {\isadigit{2}}{\isachardoublequote}} and concludes the
5.424 + sub-proof by assumption. If the goal had been \isa{{\isachardoublequote}show{\isachardoublequote}} (or
5.425 + \isa{{\isachardoublequote}thus{\isachardoublequote}}), some pending sub-goal is solved as well by the rule
5.426 + resulting from the result \emph{exported} into the enclosing goal
5.427 + context. Thus \isa{{\isachardoublequote}qed{\isachardoublequote}} may fail for two reasons: either \isa{{\isachardoublequote}m\isactrlsub {\isadigit{2}}{\isachardoublequote}} fails, or the resulting rule does not fit to any
5.428 + pending goal\footnote{This includes any additional ``strong''
5.429 + assumptions as introduced by \mbox{\isa{\isacommand{assume}}}.} of the enclosing
5.430 + context. Debugging such a situation might involve temporarily
5.431 + changing \mbox{\isa{\isacommand{show}}} into \mbox{\isa{\isacommand{have}}}, or weakening the
5.432 + local context by replacing occurrences of \mbox{\isa{\isacommand{assume}}} by
5.433 + \mbox{\isa{\isacommand{presume}}}.
5.434 +
5.435 + \item [\mbox{\isa{\isacommand{by}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}\ m\isactrlsub {\isadigit{2}}{\isachardoublequote}}] is a
5.436 + \emph{terminal proof}\index{proof!terminal}; it abbreviates
5.437 + \mbox{\isa{\isacommand{proof}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}{\isachardoublequote}}~\isa{{\isachardoublequote}qed{\isachardoublequote}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{2}}{\isachardoublequote}}, but with backtracking across both methods. Debugging
5.438 + an unsuccessful \mbox{\isa{\isacommand{by}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}\ m\isactrlsub {\isadigit{2}}{\isachardoublequote}}
5.439 + command can be done by expanding its definition; in many cases
5.440 + \mbox{\isa{\isacommand{proof}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}{\isachardoublequote}} (or even \isa{{\isachardoublequote}apply{\isachardoublequote}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}{\isachardoublequote}}) is already sufficient to see the
5.441 + problem.
5.442 +
5.443 + \item [``\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}''] is a \emph{default
5.444 + proof}\index{proof!default}; it abbreviates \mbox{\isa{\isacommand{by}}}~\isa{{\isachardoublequote}rule{\isachardoublequote}}.
5.445 +
5.446 + \item [``\mbox{\isa{\isacommand{{\isachardot}}}}''] is a \emph{trivial
5.447 + proof}\index{proof!trivial}; it abbreviates \mbox{\isa{\isacommand{by}}}~\isa{{\isachardoublequote}this{\isachardoublequote}}.
5.448 +
5.449 + \item [\mbox{\isa{\isacommand{sorry}}}] is a \emph{fake proof}\index{proof!fake}
5.450 + pretending to solve the pending claim without further ado. This
5.451 + only works in interactive development, or if the \verb|quick_and_dirty| flag is enabled (in ML). Facts emerging from fake
5.452 + proofs are not the real thing. Internally, each theorem container
5.453 + is tainted by an oracle invocation, which is indicated as ``\isa{{\isachardoublequote}{\isacharbrackleft}{\isacharbang}{\isacharbrackright}{\isachardoublequote}}'' in the printed result.
5.454 +
5.455 + The most important application of \mbox{\isa{\isacommand{sorry}}} is to support
5.456 + experimentation and top-down proof development.
5.457 +
5.458 + \end{descr}%
5.459 +\end{isamarkuptext}%
5.460 +\isamarkuptrue%
5.461 +%
5.462 +\isamarkupsection{Fundamental methods and attributes \label{sec:pure-meth-att}%
5.463 +}
5.464 +\isamarkuptrue%
5.465 +%
5.466 +\begin{isamarkuptext}%
5.467 +The following proof methods and attributes refer to basic logical
5.468 + operations of Isar. Further methods and attributes are provided by
5.469 + several generic and object-logic specific tools and packages (see
5.470 + \chref{ch:gen-tools} and \chref{ch:hol}).
5.471 +
5.472 + \begin{matharray}{rcl}
5.473 + \indexdef{}{method}{-}\mbox{\isa{{\isacharminus}}} & : & \isarmeth \\
5.474 + \indexdef{}{method}{fact}\mbox{\isa{fact}} & : & \isarmeth \\
5.475 + \indexdef{}{method}{assumption}\mbox{\isa{assumption}} & : & \isarmeth \\
5.476 + \indexdef{}{method}{this}\mbox{\isa{this}} & : & \isarmeth \\
5.477 + \indexdef{}{method}{rule}\mbox{\isa{rule}} & : & \isarmeth \\
5.478 + \indexdef{}{method}{iprover}\mbox{\isa{iprover}} & : & \isarmeth \\[0.5ex]
5.479 + \indexdef{}{attribute}{intro}\mbox{\isa{intro}} & : & \isaratt \\
5.480 + \indexdef{}{attribute}{elim}\mbox{\isa{elim}} & : & \isaratt \\
5.481 + \indexdef{}{attribute}{dest}\mbox{\isa{dest}} & : & \isaratt \\
5.482 + \indexdef{}{attribute}{rule}\mbox{\isa{rule}} & : & \isaratt \\[0.5ex]
5.483 + \indexdef{}{attribute}{OF}\mbox{\isa{OF}} & : & \isaratt \\
5.484 + \indexdef{}{attribute}{of}\mbox{\isa{of}} & : & \isaratt \\
5.485 + \indexdef{}{attribute}{where}\mbox{\isa{where}} & : & \isaratt \\
5.486 + \end{matharray}
5.487 +
5.488 + \begin{rail}
5.489 + 'fact' thmrefs?
5.490 + ;
5.491 + 'rule' thmrefs?
5.492 + ;
5.493 + 'iprover' ('!' ?) (rulemod *)
5.494 + ;
5.495 + rulemod: ('intro' | 'elim' | 'dest') ((('!' | () | '?') nat?) | 'del') ':' thmrefs
5.496 + ;
5.497 + ('intro' | 'elim' | 'dest') ('!' | () | '?') nat?
5.498 + ;
5.499 + 'rule' 'del'
5.500 + ;
5.501 + 'OF' thmrefs
5.502 + ;
5.503 + 'of' insts ('concl' ':' insts)?
5.504 + ;
5.505 + 'where' ((name | var | typefree | typevar) '=' (type | term) * 'and')
5.506 + ;
5.507 + \end{rail}
5.508 +
5.509 + \begin{descr}
5.510 +
5.511 + \item [``\mbox{\isa{{\isacharminus}}}'' (minus)] does nothing but insert the
5.512 + forward chaining facts as premises into the goal. Note that command
5.513 + \indexref{}{command}{proof}\mbox{\isa{\isacommand{proof}}} without any method actually performs a single
5.514 + reduction step using the \indexref{}{method}{rule}\mbox{\isa{rule}} method; thus a plain
5.515 + \emph{do-nothing} proof step would be ``\mbox{\isa{\isacommand{proof}}}~\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' rather than \mbox{\isa{\isacommand{proof}}} alone.
5.516 +
5.517 + \item [\mbox{\isa{fact}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}] composes
5.518 + some fact from \isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ a\isactrlsub n{\isachardoublequote}} (or implicitly from
5.519 + the current proof context) modulo unification of schematic type and
5.520 + term variables. The rule structure is not taken into account, i.e.\
5.521 + meta-level implication is considered atomic. This is the same
5.522 + principle underlying literal facts (cf.\ \secref{sec:syn-att}):
5.523 + ``\mbox{\isa{\isacommand{have}}}~\isa{{\isachardoublequote}{\isasymphi}{\isachardoublequote}}~\mbox{\isa{\isacommand{by}}}~\isa{fact}'' is
5.524 + equivalent to ``\mbox{\isa{\isacommand{note}}}~\verb|`|\isa{{\isasymphi}}\verb|`|'' provided that \isa{{\isachardoublequote}{\isasymturnstile}\ {\isasymphi}{\isachardoublequote}} is an instance of some known
5.525 + \isa{{\isachardoublequote}{\isasymturnstile}\ {\isasymphi}{\isachardoublequote}} in the proof context.
5.526 +
5.527 + \item [\mbox{\isa{assumption}}] solves some goal by a single assumption
5.528 + step. All given facts are guaranteed to participate in the
5.529 + refinement; this means there may be only 0 or 1 in the first place.
5.530 + Recall that \mbox{\isa{\isacommand{qed}}} (\secref{sec:proof-steps}) already
5.531 + concludes any remaining sub-goals by assumption, so structured
5.532 + proofs usually need not quote the \mbox{\isa{assumption}} method at
5.533 + all.
5.534 +
5.535 + \item [\mbox{\isa{this}}] applies all of the current facts directly as
5.536 + rules. Recall that ``\mbox{\isa{\isacommand{{\isachardot}}}}'' (dot) abbreviates ``\mbox{\isa{\isacommand{by}}}~\isa{this}''.
5.537 +
5.538 + \item [\mbox{\isa{rule}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}] applies some
5.539 + rule given as argument in backward manner; facts are used to reduce
5.540 + the rule before applying it to the goal. Thus \mbox{\isa{rule}}
5.541 + without facts is plain introduction, while with facts it becomes
5.542 + elimination.
5.543 +
5.544 + When no arguments are given, the \mbox{\isa{rule}} method tries to pick
5.545 + appropriate rules automatically, as declared in the current context
5.546 + using the \mbox{\isa{intro}}, \mbox{\isa{elim}}, \mbox{\isa{dest}}
5.547 + attributes (see below). This is the default behavior of \mbox{\isa{\isacommand{proof}}} and ``\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}'' (double-dot) steps (see
5.548 + \secref{sec:proof-steps}).
5.549 +
5.550 + \item [\mbox{\isa{iprover}}] performs intuitionistic proof search,
5.551 + depending on specifically declared rules from the context, or given
5.552 + as explicit arguments. Chained facts are inserted into the goal
5.553 + before commencing proof search; ``\mbox{\isa{iprover}}\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}''
5.554 + means to include the current \mbox{\isa{prems}} as well.
5.555 +
5.556 + Rules need to be classified as \mbox{\isa{intro}}, \mbox{\isa{elim}}, or \mbox{\isa{dest}}; here the ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' indicator
5.557 + refers to ``safe'' rules, which may be applied aggressively (without
5.558 + considering back-tracking later). Rules declared with ``\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}'' are ignored in proof search (the single-step \mbox{\isa{rule}}
5.559 + method still observes these). An explicit weight annotation may be
5.560 + given as well; otherwise the number of rule premises will be taken
5.561 + into account here.
5.562 +
5.563 + \item [\mbox{\isa{intro}}, \mbox{\isa{elim}}, and \mbox{\isa{dest}}]
5.564 + declare introduction, elimination, and destruct rules, to be used
5.565 + with the \mbox{\isa{rule}} and \mbox{\isa{iprover}} methods. Note that
5.566 + the latter will ignore rules declared with ``\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}'', while
5.567 + ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' are used most aggressively.
5.568 +
5.569 + The classical reasoner (see \secref{sec:classical}) introduces its
5.570 + own variants of these attributes; use qualified names to access the
5.571 + present versions of Isabelle/Pure, i.e.\ \mbox{\isa{Pure{\isachardot}intro}}.
5.572 +
5.573 + \item [\mbox{\isa{rule}}~\isa{del}] undeclares introduction,
5.574 + elimination, or destruct rules.
5.575 +
5.576 + \item [\mbox{\isa{OF}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}] applies some
5.577 + theorem to all of the given rules \isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ a\isactrlsub n{\isachardoublequote}}
5.578 + (in parallel). This corresponds to the \verb|"op MRS"| operation in
5.579 + ML, but note the reversed order. Positions may be effectively
5.580 + skipped by including ``\isa{{\isacharunderscore}}'' (underscore) as argument.
5.581 +
5.582 + \item [\mbox{\isa{of}}~\isa{{\isachardoublequote}t\isactrlsub {\isadigit{1}}\ {\isasymdots}\ t\isactrlsub n{\isachardoublequote}}] performs
5.583 + positional instantiation of term variables. The terms \isa{{\isachardoublequote}t\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ t\isactrlsub n{\isachardoublequote}} are substituted for any schematic
5.584 + variables occurring in a theorem from left to right; ``\isa{{\isacharunderscore}}'' (underscore) indicates to skip a position. Arguments following
5.585 + a ``\mbox{\isa{\isakeyword{concl}}}\isa{{\isachardoublequote}{\isacharcolon}{\isachardoublequote}}'' specification refer to positions
5.586 + of the conclusion of a rule.
5.587 +
5.588 + \item [\mbox{\isa{where}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isacharequal}\ t\isactrlsub {\isadigit{1}}\ {\isasymAND}\ {\isasymdots}\ x\isactrlsub n\ {\isacharequal}\ t\isactrlsub n{\isachardoublequote}}] performs named instantiation of schematic
5.589 + type and term variables occurring in a theorem. Schematic variables
5.590 + have to be specified on the left-hand side (e.g.\ \isa{{\isachardoublequote}{\isacharquery}x{\isadigit{1}}{\isachardot}{\isadigit{3}}{\isachardoublequote}}).
5.591 + The question mark may be omitted if the variable name is a plain
5.592 + identifier without index. As type instantiations are inferred from
5.593 + term instantiations, explicit type instantiations are seldom
5.594 + necessary.
5.595 +
5.596 + \end{descr}%
5.597 +\end{isamarkuptext}%
5.598 +\isamarkuptrue%
5.599 +%
5.600 +\isamarkupsection{Term abbreviations \label{sec:term-abbrev}%
5.601 +}
5.602 +\isamarkuptrue%
5.603 +%
5.604 +\begin{isamarkuptext}%
5.605 +\begin{matharray}{rcl}
5.606 + \indexdef{}{command}{let}\mbox{\isa{\isacommand{let}}} & : & \isartrans{proof(state)}{proof(state)} \\
5.607 + \indexdef{}{keyword}{is}\mbox{\isa{\isakeyword{is}}} & : & syntax \\
5.608 + \end{matharray}
5.609 +
5.610 + Abbreviations may be either bound by explicit \mbox{\isa{\isacommand{let}}}~\isa{{\isachardoublequote}p\ {\isasymequiv}\ t{\isachardoublequote}} statements, or by annotating assumptions or
5.611 + goal statements with a list of patterns ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIS}\ p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub n{\isacharparenright}{\isachardoublequote}}''. In both cases, higher-order matching is invoked to
5.612 + bind extra-logical term variables, which may be either named
5.613 + schematic variables of the form \isa{{\isacharquery}x}, or nameless dummies
5.614 + ``\mbox{\isa{{\isacharunderscore}}}'' (underscore). Note that in the \mbox{\isa{\isacommand{let}}}
5.615 + form the patterns occur on the left-hand side, while the \mbox{\isa{\isakeyword{is}}} patterns are in postfix position.
5.616 +
5.617 + Polymorphism of term bindings is handled in Hindley-Milner style,
5.618 + similar to ML. Type variables referring to local assumptions or
5.619 + open goal statements are \emph{fixed}, while those of finished
5.620 + results or bound by \mbox{\isa{\isacommand{let}}} may occur in \emph{arbitrary}
5.621 + instances later. Even though actual polymorphism should be rarely
5.622 + used in practice, this mechanism is essential to achieve proper
5.623 + incremental type-inference, as the user proceeds to build up the
5.624 + Isar proof text from left to right.
5.625 +
5.626 + \medskip Term abbreviations are quite different from local
5.627 + definitions as introduced via \mbox{\isa{\isacommand{def}}} (see
5.628 + \secref{sec:proof-context}). The latter are visible within the
5.629 + logic as actual equations, while abbreviations disappear during the
5.630 + input process just after type checking. Also note that \mbox{\isa{\isacommand{def}}} does not support polymorphism.
5.631 +
5.632 + \begin{rail}
5.633 + 'let' ((term + 'and') '=' term + 'and')
5.634 + ;
5.635 + \end{rail}
5.636 +
5.637 + The syntax of \mbox{\isa{\isakeyword{is}}} patterns follows \railnonterm{termpat}
5.638 + or \railnonterm{proppat} (see \secref{sec:term-decls}).
5.639 +
5.640 + \begin{descr}
5.641 +
5.642 + \item [\mbox{\isa{\isacommand{let}}}~\isa{{\isachardoublequote}p\isactrlsub {\isadigit{1}}\ {\isacharequal}\ t\isactrlsub {\isadigit{1}}\ {\isasymAND}\ {\isasymdots}\ p\isactrlsub n\ {\isacharequal}\ t\isactrlsub n{\isachardoublequote}}] binds any text variables in patterns \isa{{\isachardoublequote}p\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ p\isactrlsub n{\isachardoublequote}} by simultaneous higher-order matching
5.643 + against terms \isa{{\isachardoublequote}t\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ t\isactrlsub n{\isachardoublequote}}.
5.644 +
5.645 + \item [\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIS}\ p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub n{\isacharparenright}{\isachardoublequote}}] resembles \mbox{\isa{\isacommand{let}}}, but matches \isa{{\isachardoublequote}p\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ p\isactrlsub n{\isachardoublequote}} against the
5.646 + preceding statement. Also note that \mbox{\isa{\isakeyword{is}}} is not a
5.647 + separate command, but part of others (such as \mbox{\isa{\isacommand{assume}}},
5.648 + \mbox{\isa{\isacommand{have}}} etc.).
5.649 +
5.650 + \end{descr}
5.651 +
5.652 + Some \emph{implicit} term abbreviations\index{term abbreviations}
5.653 + for goals and facts are available as well. For any open goal,
5.654 + \indexref{}{variable}{thesis}\mbox{\isa{thesis}} refers to its object-level statement,
5.655 + abstracted over any meta-level parameters (if present). Likewise,
5.656 + \indexref{}{variable}{this}\mbox{\isa{this}} is bound for fact statements resulting from
5.657 + assumptions or finished goals. In case \mbox{\isa{this}} refers to
5.658 + an object-logic statement that is an application \isa{{\isachardoublequote}f\ t{\isachardoublequote}}, then
5.659 + \isa{t} is bound to the special text variable ``\mbox{\isa{{\isasymdots}}}''
5.660 + (three dots). The canonical application of this convenience are
5.661 + calculational proofs (see \secref{sec:calculation}).%
5.662 +\end{isamarkuptext}%
5.663 +\isamarkuptrue%
5.664 +%
5.665 +\isamarkupsection{Block structure%
5.666 +}
5.667 +\isamarkuptrue%
5.668 +%
5.669 +\begin{isamarkuptext}%
5.670 +\begin{matharray}{rcl}
5.671 + \indexdef{}{command}{next}\mbox{\isa{\isacommand{next}}} & : & \isartrans{proof(state)}{proof(state)} \\
5.672 + \indexdef{}{command}{\{}\mbox{\isa{\isacommand{{\isacharbraceleft}}}} & : & \isartrans{proof(state)}{proof(state)} \\
5.673 + \indexdef{}{command}{\}}\mbox{\isa{\isacommand{{\isacharbraceright}}}} & : & \isartrans{proof(state)}{proof(state)} \\
5.674 + \end{matharray}
5.675 +
5.676 + While Isar is inherently block-structured, opening and closing
5.677 + blocks is mostly handled rather casually, with little explicit
5.678 + user-intervention. Any local goal statement automatically opens
5.679 + \emph{two} internal blocks, which are closed again when concluding
5.680 + the sub-proof (by \mbox{\isa{\isacommand{qed}}} etc.). Sections of different
5.681 + context within a sub-proof may be switched via \mbox{\isa{\isacommand{next}}},
5.682 + which is just a single block-close followed by block-open again.
5.683 + The effect of \mbox{\isa{\isacommand{next}}} is to reset the local proof context;
5.684 + there is no goal focus involved here!
5.685 +
5.686 + For slightly more advanced applications, there are explicit block
5.687 + parentheses as well. These typically achieve a stronger forward
5.688 + style of reasoning.
5.689 +
5.690 + \begin{descr}
5.691 +
5.692 + \item [\mbox{\isa{\isacommand{next}}}] switches to a fresh block within a
5.693 + sub-proof, resetting the local context to the initial one.
5.694 +
5.695 + \item [\mbox{\isa{\isacommand{{\isacharbraceleft}}}} and \mbox{\isa{\isacommand{{\isacharbraceright}}}}] explicitly open and close
5.696 + blocks. Any current facts pass through ``\mbox{\isa{\isacommand{{\isacharbraceleft}}}}''
5.697 + unchanged, while ``\mbox{\isa{\isacommand{{\isacharbraceright}}}}'' causes any result to be
5.698 + \emph{exported} into the enclosing context. Thus fixed variables
5.699 + are generalized, assumptions discharged, and local definitions
5.700 + unfolded (cf.\ \secref{sec:proof-context}). There is no difference
5.701 + of \mbox{\isa{\isacommand{assume}}} and \mbox{\isa{\isacommand{presume}}} in this mode of
5.702 + forward reasoning --- in contrast to plain backward reasoning with
5.703 + the result exported at \mbox{\isa{\isacommand{show}}} time.
5.704 +
5.705 + \end{descr}%
5.706 +\end{isamarkuptext}%
5.707 +\isamarkuptrue%
5.708 +%
5.709 +\isamarkupsection{Emulating tactic scripts \label{sec:tactic-commands}%
5.710 +}
5.711 +\isamarkuptrue%
5.712 +%
5.713 +\begin{isamarkuptext}%
5.714 +The Isar provides separate commands to accommodate tactic-style
5.715 + proof scripts within the same system. While being outside the
5.716 + orthodox Isar proof language, these might come in handy for
5.717 + interactive exploration and debugging, or even actual tactical proof
5.718 + within new-style theories (to benefit from document preparation, for
5.719 + example). See also \secref{sec:tactics} for actual tactics, that
5.720 + have been encapsulated as proof methods. Proper proof methods may
5.721 + be used in scripts, too.
5.722 +
5.723 + \begin{matharray}{rcl}
5.724 + \indexdef{}{command}{apply}\mbox{\isa{\isacommand{apply}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isartrans{proof(prove)}{proof(prove)} \\
5.725 + \indexdef{}{command}{apply\_end}\mbox{\isa{\isacommand{apply{\isacharunderscore}end}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isartrans{proof(state)}{proof(state)} \\
5.726 + \indexdef{}{command}{done}\mbox{\isa{\isacommand{done}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isartrans{proof(prove)}{proof(state)} \\
5.727 + \indexdef{}{command}{defer}\mbox{\isa{\isacommand{defer}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isartrans{proof}{proof} \\
5.728 + \indexdef{}{command}{prefer}\mbox{\isa{\isacommand{prefer}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isartrans{proof}{proof} \\
5.729 + \indexdef{}{command}{back}\mbox{\isa{\isacommand{back}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isartrans{proof}{proof} \\
5.730 + \end{matharray}
5.731 +
5.732 + \begin{rail}
5.733 + ( 'apply' | 'apply\_end' ) method
5.734 + ;
5.735 + 'defer' nat?
5.736 + ;
5.737 + 'prefer' nat
5.738 + ;
5.739 + \end{rail}
5.740 +
5.741 + \begin{descr}
5.742 +
5.743 + \item [\mbox{\isa{\isacommand{apply}}}~\isa{m}] applies proof method \isa{m}
5.744 + in initial position, but unlike \mbox{\isa{\isacommand{proof}}} it retains
5.745 + ``\isa{{\isachardoublequote}proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}}'' mode. Thus consecutive method
5.746 + applications may be given just as in tactic scripts.
5.747 +
5.748 + Facts are passed to \isa{m} as indicated by the goal's
5.749 + forward-chain mode, and are \emph{consumed} afterwards. Thus any
5.750 + further \mbox{\isa{\isacommand{apply}}} command would always work in a purely
5.751 + backward manner.
5.752 +
5.753 + \item [\mbox{\isa{\isacommand{apply{\isacharunderscore}end}}}~\isa{{\isachardoublequote}m{\isachardoublequote}}] applies proof method
5.754 + \isa{m} as if in terminal position. Basically, this simulates a
5.755 + multi-step tactic script for \mbox{\isa{\isacommand{qed}}}, but may be given
5.756 + anywhere within the proof body.
5.757 +
5.758 + No facts are passed to \mbox{\isa{m}} here. Furthermore, the static
5.759 + context is that of the enclosing goal (as for actual \mbox{\isa{\isacommand{qed}}}). Thus the proof method may not refer to any assumptions
5.760 + introduced in the current body, for example.
5.761 +
5.762 + \item [\mbox{\isa{\isacommand{done}}}] completes a proof script, provided that
5.763 + the current goal state is solved completely. Note that actual
5.764 + structured proof commands (e.g.\ ``\mbox{\isa{\isacommand{{\isachardot}}}}'' or \mbox{\isa{\isacommand{sorry}}}) may be used to conclude proof scripts as well.
5.765 +
5.766 + \item [\mbox{\isa{\isacommand{defer}}}~\isa{n} and \mbox{\isa{\isacommand{prefer}}}~\isa{n}] shuffle the list of pending goals: \mbox{\isa{\isacommand{defer}}} puts off
5.767 + sub-goal \isa{n} to the end of the list (\isa{{\isachardoublequote}n\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequote}} by
5.768 + default), while \mbox{\isa{\isacommand{prefer}}} brings sub-goal \isa{n} to the
5.769 + front.
5.770 +
5.771 + \item [\mbox{\isa{\isacommand{back}}}] does back-tracking over the result
5.772 + sequence of the latest proof command. Basically, any proof command
5.773 + may return multiple results.
5.774 +
5.775 + \end{descr}
5.776 +
5.777 + Any proper Isar proof method may be used with tactic script commands
5.778 + such as \mbox{\isa{\isacommand{apply}}}. A few additional emulations of actual
5.779 + tactics are provided as well; these would be never used in actual
5.780 + structured proofs, of course.%
5.781 +\end{isamarkuptext}%
5.782 +\isamarkuptrue%
5.783 +%
5.784 +\isamarkupsection{Omitting proofs%
5.785 +}
5.786 +\isamarkuptrue%
5.787 +%
5.788 +\begin{isamarkuptext}%
5.789 +\begin{matharray}{rcl}
5.790 + \indexdef{}{command}{oops}\mbox{\isa{\isacommand{oops}}} & : & \isartrans{proof}{theory} \\
5.791 + \end{matharray}
5.792 +
5.793 + The \mbox{\isa{\isacommand{oops}}} command discontinues the current proof
5.794 + attempt, while considering the partial proof text as properly
5.795 + processed. This is conceptually quite different from ``faking''
5.796 + actual proofs via \indexref{}{command}{sorry}\mbox{\isa{\isacommand{sorry}}} (see
5.797 + \secref{sec:proof-steps}): \mbox{\isa{\isacommand{oops}}} does not observe the
5.798 + proof structure at all, but goes back right to the theory level.
5.799 + Furthermore, \mbox{\isa{\isacommand{oops}}} does not produce any result theorem
5.800 + --- there is no intended claim to be able to complete the proof
5.801 + anyhow.
5.802 +
5.803 + A typical application of \mbox{\isa{\isacommand{oops}}} is to explain Isar proofs
5.804 + \emph{within} the system itself, in conjunction with the document
5.805 + preparation tools of Isabelle described in \cite{isabelle-sys}.
5.806 + Thus partial or even wrong proof attempts can be discussed in a
5.807 + logically sound manner. Note that the Isabelle {\LaTeX} macros can
5.808 + be easily adapted to print something like ``\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}'' instead of
5.809 + the keyword ``\mbox{\isa{\isacommand{oops}}}''.
5.810 +
5.811 + \medskip The \mbox{\isa{\isacommand{oops}}} command is undo-able, unlike
5.812 + \indexref{}{command}{kill}\mbox{\isa{\isacommand{kill}}} (see \secref{sec:history}). The effect is to
5.813 + get back to the theory just before the opening of the proof.%
5.814 +\end{isamarkuptext}%
5.815 +\isamarkuptrue%
5.816 +%
5.817 +\isamarkupsection{Generalized elimination \label{sec:obtain}%
5.818 +}
5.819 +\isamarkuptrue%
5.820 +%
5.821 +\begin{isamarkuptext}%
5.822 +\begin{matharray}{rcl}
5.823 + \indexdef{}{command}{obtain}\mbox{\isa{\isacommand{obtain}}} & : & \isartrans{proof(state)}{proof(prove)} \\
5.824 + \indexdef{}{command}{guess}\mbox{\isa{\isacommand{guess}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isartrans{proof(state)}{proof(prove)} \\
5.825 + \end{matharray}
5.826 +
5.827 + Generalized elimination means that additional elements with certain
5.828 + properties may be introduced in the current context, by virtue of a
5.829 + locally proven ``soundness statement''. Technically speaking, the
5.830 + \mbox{\isa{\isacommand{obtain}}} language element is like a declaration of
5.831 + \mbox{\isa{\isacommand{fix}}} and \mbox{\isa{\isacommand{assume}}} (see also see
5.832 + \secref{sec:proof-context}), together with a soundness proof of its
5.833 + additional claim. According to the nature of existential reasoning,
5.834 + assumptions get eliminated from any result exported from the context
5.835 + later, provided that the corresponding parameters do \emph{not}
5.836 + occur in the conclusion.
5.837 +
5.838 + \begin{rail}
5.839 + 'obtain' parname? (vars + 'and') 'where' (props + 'and')
5.840 + ;
5.841 + 'guess' (vars + 'and')
5.842 + ;
5.843 + \end{rail}
5.844 +
5.845 + The derived Isar command \mbox{\isa{\isacommand{obtain}}} is defined as follows
5.846 + (where \isa{{\isachardoublequote}b\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub k{\isachardoublequote}} shall refer to (optional)
5.847 + facts indicated for forward chaining).
5.848 + \begin{matharray}{l}
5.849 + \isa{{\isachardoublequote}{\isasymlangle}using\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub k{\isasymrangle}{\isachardoublequote}}~~\mbox{\isa{\isacommand{obtain}}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m\ {\isasymWHERE}\ a{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n\ \ {\isasymlangle}proof{\isasymrangle}\ {\isasymequiv}{\isachardoublequote}} \\[1ex]
5.850 + \quad \mbox{\isa{\isacommand{have}}}~\isa{{\isachardoublequote}{\isasymAnd}thesis{\isachardot}\ {\isacharparenleft}{\isasymAnd}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardot}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymphi}\isactrlsub n\ {\isasymLongrightarrow}\ thesis{\isacharparenright}\ {\isasymLongrightarrow}\ thesis{\isachardoublequote}} \\
5.851 + \quad \mbox{\isa{\isacommand{proof}}}~\isa{succeed} \\
5.852 + \qquad \mbox{\isa{\isacommand{fix}}}~\isa{thesis} \\
5.853 + \qquad \mbox{\isa{\isacommand{assume}}}~\isa{{\isachardoublequote}that\ {\isacharbrackleft}Pure{\isachardot}intro{\isacharquery}{\isacharbrackright}{\isacharcolon}\ {\isasymAnd}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardot}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymphi}\isactrlsub n\ {\isasymLongrightarrow}\ thesis{\isachardoublequote}} \\
5.854 + \qquad \mbox{\isa{\isacommand{then}}}~\mbox{\isa{\isacommand{show}}}~\isa{thesis} \\
5.855 + \quad\qquad \mbox{\isa{\isacommand{apply}}}~\isa{{\isacharminus}} \\
5.856 + \quad\qquad \mbox{\isa{\isacommand{using}}}~\isa{{\isachardoublequote}b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub k\ \ {\isasymlangle}proof{\isasymrangle}{\isachardoublequote}} \\
5.857 + \quad \mbox{\isa{\isacommand{qed}}} \\
5.858 + \quad \mbox{\isa{\isacommand{fix}}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardoublequote}}~\mbox{\isa{\isacommand{assume}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}\ a{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}} \\
5.859 + \end{matharray}
5.860 +
5.861 + Typically, the soundness proof is relatively straight-forward, often
5.862 + just by canonical automated tools such as ``\mbox{\isa{\isacommand{by}}}~\isa{simp}'' or ``\mbox{\isa{\isacommand{by}}}~\isa{blast}''. Accordingly, the
5.863 + ``\isa{that}'' reduction above is declared as simplification and
5.864 + introduction rule.
5.865 +
5.866 + In a sense, \mbox{\isa{\isacommand{obtain}}} represents at the level of Isar
5.867 + proofs what would be meta-logical existential quantifiers and
5.868 + conjunctions. This concept has a broad range of useful
5.869 + applications, ranging from plain elimination (or introduction) of
5.870 + object-level existential and conjunctions, to elimination over
5.871 + results of symbolic evaluation of recursive definitions, for
5.872 + example. Also note that \mbox{\isa{\isacommand{obtain}}} without parameters acts
5.873 + much like \mbox{\isa{\isacommand{have}}}, where the result is treated as a
5.874 + genuine assumption.
5.875 +
5.876 + An alternative name to be used instead of ``\isa{that}'' above may
5.877 + be given in parentheses.
5.878 +
5.879 + \medskip The improper variant \mbox{\isa{\isacommand{guess}}} is similar to
5.880 + \mbox{\isa{\isacommand{obtain}}}, but derives the obtained statement from the
5.881 + course of reasoning! The proof starts with a fixed goal \isa{thesis}. The subsequent proof may refine this to anything of the
5.882 + form like \isa{{\isachardoublequote}{\isasymAnd}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardot}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymphi}\isactrlsub n\ {\isasymLongrightarrow}\ thesis{\isachardoublequote}}, but must not introduce new subgoals. The
5.883 + final goal state is then used as reduction rule for the obtain
5.884 + scheme described above. Obtained parameters \isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub m{\isachardoublequote}} are marked as internal by default, which prevents the
5.885 + proof context from being polluted by ad-hoc variables. The variable
5.886 + names and type constraints given as arguments for \mbox{\isa{\isacommand{guess}}}
5.887 + specify a prefix of obtained parameters explicitly in the text.
5.888 +
5.889 + It is important to note that the facts introduced by \mbox{\isa{\isacommand{obtain}}} and \mbox{\isa{\isacommand{guess}}} may not be polymorphic: any
5.890 + type-variables occurring here are fixed in the present context!%
5.891 +\end{isamarkuptext}%
5.892 +\isamarkuptrue%
5.893 +%
5.894 +\isamarkupsection{Calculational reasoning \label{sec:calculation}%
5.895 +}
5.896 +\isamarkuptrue%
5.897 +%
5.898 +\begin{isamarkuptext}%
5.899 +\begin{matharray}{rcl}
5.900 + \indexdef{}{command}{also}\mbox{\isa{\isacommand{also}}} & : & \isartrans{proof(state)}{proof(state)} \\
5.901 + \indexdef{}{command}{finally}\mbox{\isa{\isacommand{finally}}} & : & \isartrans{proof(state)}{proof(chain)} \\
5.902 + \indexdef{}{command}{moreover}\mbox{\isa{\isacommand{moreover}}} & : & \isartrans{proof(state)}{proof(state)} \\
5.903 + \indexdef{}{command}{ultimately}\mbox{\isa{\isacommand{ultimately}}} & : & \isartrans{proof(state)}{proof(chain)} \\
5.904 + \indexdef{}{command}{print\_trans\_rules}\mbox{\isa{\isacommand{print{\isacharunderscore}trans{\isacharunderscore}rules}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
5.905 + \mbox{\isa{trans}} & : & \isaratt \\
5.906 + \mbox{\isa{sym}} & : & \isaratt \\
5.907 + \mbox{\isa{symmetric}} & : & \isaratt \\
5.908 + \end{matharray}
5.909 +
5.910 + Calculational proof is forward reasoning with implicit application
5.911 + of transitivity rules (such those of \isa{{\isachardoublequote}{\isacharequal}{\isachardoublequote}}, \isa{{\isachardoublequote}{\isasymle}{\isachardoublequote}},
5.912 + \isa{{\isachardoublequote}{\isacharless}{\isachardoublequote}}). Isabelle/Isar maintains an auxiliary fact register
5.913 + \indexref{}{fact}{calculation}\mbox{\isa{calculation}} for accumulating results obtained by
5.914 + transitivity composed with the current result. Command \mbox{\isa{\isacommand{also}}} updates \mbox{\isa{calculation}} involving \mbox{\isa{this}}, while
5.915 + \mbox{\isa{\isacommand{finally}}} exhibits the final \mbox{\isa{calculation}} by
5.916 + forward chaining towards the next goal statement. Both commands
5.917 + require valid current facts, i.e.\ may occur only after commands
5.918 + that produce theorems such as \mbox{\isa{\isacommand{assume}}}, \mbox{\isa{\isacommand{note}}}, or some finished proof of \mbox{\isa{\isacommand{have}}}, \mbox{\isa{\isacommand{show}}} etc. The \mbox{\isa{\isacommand{moreover}}} and \mbox{\isa{\isacommand{ultimately}}}
5.919 + commands are similar to \mbox{\isa{\isacommand{also}}} and \mbox{\isa{\isacommand{finally}}},
5.920 + but only collect further results in \mbox{\isa{calculation}} without
5.921 + applying any rules yet.
5.922 +
5.923 + Also note that the implicit term abbreviation ``\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}'' has
5.924 + its canonical application with calculational proofs. It refers to
5.925 + the argument of the preceding statement. (The argument of a curried
5.926 + infix expression happens to be its right-hand side.)
5.927 +
5.928 + Isabelle/Isar calculations are implicitly subject to block structure
5.929 + in the sense that new threads of calculational reasoning are
5.930 + commenced for any new block (as opened by a local goal, for
5.931 + example). This means that, apart from being able to nest
5.932 + calculations, there is no separate \emph{begin-calculation} command
5.933 + required.
5.934 +
5.935 + \medskip The Isar calculation proof commands may be defined as
5.936 + follows:\footnote{We suppress internal bookkeeping such as proper
5.937 + handling of block-structure.}
5.938 +
5.939 + \begin{matharray}{rcl}
5.940 + \mbox{\isa{\isacommand{also}}}\isa{{\isachardoublequote}\isactrlsub {\isadigit{0}}{\isachardoublequote}} & \equiv & \mbox{\isa{\isacommand{note}}}~\isa{{\isachardoublequote}calculation\ {\isacharequal}\ this{\isachardoublequote}} \\
5.941 + \mbox{\isa{\isacommand{also}}}\isa{{\isachardoublequote}\isactrlsub n\isactrlsub {\isacharplus}\isactrlsub {\isadigit{1}}{\isachardoublequote}} & \equiv & \mbox{\isa{\isacommand{note}}}~\isa{{\isachardoublequote}calculation\ {\isacharequal}\ trans\ {\isacharbrackleft}OF\ calculation\ this{\isacharbrackright}{\isachardoublequote}} \\[0.5ex]
5.942 + \mbox{\isa{\isacommand{finally}}} & \equiv & \mbox{\isa{\isacommand{also}}}~\mbox{\isa{\isacommand{from}}}~\isa{calculation} \\[0.5ex]
5.943 + \mbox{\isa{\isacommand{moreover}}} & \equiv & \mbox{\isa{\isacommand{note}}}~\isa{{\isachardoublequote}calculation\ {\isacharequal}\ calculation\ this{\isachardoublequote}} \\
5.944 + \mbox{\isa{\isacommand{ultimately}}} & \equiv & \mbox{\isa{\isacommand{moreover}}}~\mbox{\isa{\isacommand{from}}}~\isa{calculation} \\
5.945 + \end{matharray}
5.946 +
5.947 + \begin{rail}
5.948 + ('also' | 'finally') ('(' thmrefs ')')?
5.949 + ;
5.950 + 'trans' (() | 'add' | 'del')
5.951 + ;
5.952 + \end{rail}
5.953 +
5.954 + \begin{descr}
5.955 +
5.956 + \item [\mbox{\isa{\isacommand{also}}}~\isa{{\isachardoublequote}{\isacharparenleft}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharparenright}{\isachardoublequote}}]
5.957 + maintains the auxiliary \mbox{\isa{calculation}} register as follows.
5.958 + The first occurrence of \mbox{\isa{\isacommand{also}}} in some calculational
5.959 + thread initializes \mbox{\isa{calculation}} by \mbox{\isa{this}}. Any
5.960 + subsequent \mbox{\isa{\isacommand{also}}} on the same level of block-structure
5.961 + updates \mbox{\isa{calculation}} by some transitivity rule applied to
5.962 + \mbox{\isa{calculation}} and \mbox{\isa{this}} (in that order). Transitivity
5.963 + rules are picked from the current context, unless alternative rules
5.964 + are given as explicit arguments.
5.965 +
5.966 + \item [\mbox{\isa{\isacommand{finally}}}~\isa{{\isachardoublequote}{\isacharparenleft}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isacharparenright}{\isachardoublequote}}]
5.967 + maintaining \mbox{\isa{calculation}} in the same way as \mbox{\isa{\isacommand{also}}}, and concludes the current calculational thread. The final
5.968 + result is exhibited as fact for forward chaining towards the next
5.969 + goal. Basically, \mbox{\isa{\isacommand{finally}}} just abbreviates \mbox{\isa{\isacommand{also}}}~\mbox{\isa{\isacommand{from}}}~\mbox{\isa{calculation}}. Typical idioms for
5.970 + concluding calculational proofs are ``\mbox{\isa{\isacommand{finally}}}~\mbox{\isa{\isacommand{show}}}~\isa{{\isacharquery}thesis}~\mbox{\isa{\isacommand{{\isachardot}}}}'' and ``\mbox{\isa{\isacommand{finally}}}~\mbox{\isa{\isacommand{have}}}~\isa{{\isasymphi}}~\mbox{\isa{\isacommand{{\isachardot}}}}''.
5.971 +
5.972 + \item [\mbox{\isa{\isacommand{moreover}}} and \mbox{\isa{\isacommand{ultimately}}}] are
5.973 + analogous to \mbox{\isa{\isacommand{also}}} and \mbox{\isa{\isacommand{finally}}}, but collect
5.974 + results only, without applying rules.
5.975 +
5.976 + \item [\mbox{\isa{\isacommand{print{\isacharunderscore}trans{\isacharunderscore}rules}}}] prints the list of
5.977 + transitivity rules (for calculational commands \mbox{\isa{\isacommand{also}}} and
5.978 + \mbox{\isa{\isacommand{finally}}}) and symmetry rules (for the \mbox{\isa{symmetric}} operation and single step elimination patters) of the
5.979 + current context.
5.980 +
5.981 + \item [\mbox{\isa{trans}}] declares theorems as transitivity rules.
5.982 +
5.983 + \item [\mbox{\isa{sym}}] declares symmetry rules, as well as
5.984 + \mbox{\isa{Pure{\isachardot}elim{\isacharquery}}} rules.
5.985 +
5.986 + \item [\mbox{\isa{symmetric}}] resolves a theorem with some rule
5.987 + declared as \mbox{\isa{sym}} in the current context. For example,
5.988 + ``\mbox{\isa{\isacommand{assume}}}~\isa{{\isachardoublequote}{\isacharbrackleft}symmetric{\isacharbrackright}{\isacharcolon}\ x\ {\isacharequal}\ y{\isachardoublequote}}'' produces a
5.989 + swapped fact derived from that assumption.
5.990 +
5.991 + In structured proof texts it is often more appropriate to use an
5.992 + explicit single-step elimination proof, such as ``\mbox{\isa{\isacommand{assume}}}~\isa{{\isachardoublequote}x\ {\isacharequal}\ y{\isachardoublequote}}~\mbox{\isa{\isacommand{then}}}~\mbox{\isa{\isacommand{have}}}~\isa{{\isachardoublequote}y\ {\isacharequal}\ x{\isachardoublequote}}~\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}''.
5.993 +
5.994 + \end{descr}%
5.995 +\end{isamarkuptext}%
5.996 +\isamarkuptrue%
5.997 +%
5.998 \isadelimtheory
5.999 %
5.1000 \endisadelimtheory
6.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex Fri May 09 23:35:57 2008 +0200
6.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex Sat May 10 00:14:00 2008 +0200
6.3 @@ -24,6 +24,71 @@
6.4 }
6.5 \isamarkuptrue%
6.6 %
6.7 +\isamarkupsection{Defining theories \label{sec:begin-thy}%
6.8 +}
6.9 +\isamarkuptrue%
6.10 +%
6.11 +\begin{isamarkuptext}%
6.12 +\begin{matharray}{rcl}
6.13 + \indexdef{}{command}{header}\mbox{\isa{\isacommand{header}}} & : & \isarkeep{toplevel} \\
6.14 + \indexdef{}{command}{theory}\mbox{\isa{\isacommand{theory}}} & : & \isartrans{toplevel}{theory} \\
6.15 + \indexdef{}{command}{end}\mbox{\isa{\isacommand{end}}} & : & \isartrans{theory}{toplevel} \\
6.16 + \end{matharray}
6.17 +
6.18 + Isabelle/Isar theories are defined via theory, which contain both
6.19 + specifications and proofs; occasionally definitional mechanisms also
6.20 + require some explicit proof.
6.21 +
6.22 + The first ``real'' command of any theory has to be \mbox{\isa{\isacommand{theory}}}, which starts a new theory based on the merge of existing
6.23 + ones. Just preceding the \mbox{\isa{\isacommand{theory}}} keyword, there may be
6.24 + an optional \mbox{\isa{\isacommand{header}}} declaration, which is relevant to
6.25 + document preparation only; it acts very much like a special
6.26 + pre-theory markup command (cf.\ \secref{sec:markup-thy} and
6.27 + \secref{sec:markup-thy}). The \mbox{\isa{\isacommand{end}}} command concludes a
6.28 + theory development; it has to be the very last command of any theory
6.29 + file loaded in batch-mode.
6.30 +
6.31 + \begin{rail}
6.32 + 'header' text
6.33 + ;
6.34 + 'theory' name 'imports' (name +) uses? 'begin'
6.35 + ;
6.36 +
6.37 + uses: 'uses' ((name | parname) +);
6.38 + \end{rail}
6.39 +
6.40 + \begin{descr}
6.41 +
6.42 + \item [\mbox{\isa{\isacommand{header}}}~\isa{{\isachardoublequote}text{\isachardoublequote}}] provides plain text
6.43 + markup just preceding the formal beginning of a theory. In actual
6.44 + document preparation the corresponding {\LaTeX} macro \verb|\isamarkupheader| may be redefined to produce chapter or section
6.45 + headings. See also \secref{sec:markup-thy} and
6.46 + \secref{sec:markup-prf} for further markup commands.
6.47 +
6.48 + \item [\mbox{\isa{\isacommand{theory}}}~\isa{{\isachardoublequote}A\ {\isasymIMPORTS}\ B\isactrlsub {\isadigit{1}}\ {\isasymdots}\ B\isactrlsub n\ {\isasymBEGIN}{\isachardoublequote}}] starts a new theory \isa{A} based on the
6.49 + merge of existing theories \isa{{\isachardoublequote}B\isactrlsub {\isadigit{1}}\ {\isasymdots}\ B\isactrlsub n{\isachardoublequote}}.
6.50 +
6.51 + Due to inclusion of several ancestors, the overall theory structure
6.52 + emerging in an Isabelle session forms a directed acyclic graph
6.53 + (DAG). Isabelle's theory loader ensures that the sources
6.54 + contributing to the development graph are always up-to-date.
6.55 + Changed files are automatically reloaded when processing theory
6.56 + headers.
6.57 +
6.58 + The optional \indexdef{}{keyword}{uses}\mbox{\isa{\isakeyword{uses}}} specification declares additional
6.59 + dependencies on extra files (usually ML sources). Files will be
6.60 + loaded immediately (as ML), unless the name is put in parentheses,
6.61 + which merely documents the dependency to be resolved later in the
6.62 + text (typically via explicit \indexref{}{command}{use}\mbox{\isa{\isacommand{use}}} in the body text,
6.63 + see \secref{sec:ML}).
6.64 +
6.65 + \item [\mbox{\isa{\isacommand{end}}}] concludes the current theory definition or
6.66 + context switch.
6.67 +
6.68 + \end{descr}%
6.69 +\end{isamarkuptext}%
6.70 +\isamarkuptrue%
6.71 +%
6.72 \isadelimtheory
6.73 %
6.74 \endisadelimtheory
7.1 --- a/doc-src/IsarRef/Thy/document/pure.tex Fri May 09 23:35:57 2008 +0200
7.2 +++ b/doc-src/IsarRef/Thy/document/pure.tex Sat May 10 00:14:00 2008 +0200
7.3 @@ -52,71 +52,6 @@
7.4 }
7.5 \isamarkuptrue%
7.6 %
7.7 -\isamarkupsubsection{Defining theories \label{sec:begin-thy}%
7.8 -}
7.9 -\isamarkuptrue%
7.10 -%
7.11 -\begin{isamarkuptext}%
7.12 -\begin{matharray}{rcl}
7.13 - \indexdef{}{command}{header}\mbox{\isa{\isacommand{header}}} & : & \isarkeep{toplevel} \\
7.14 - \indexdef{}{command}{theory}\mbox{\isa{\isacommand{theory}}} & : & \isartrans{toplevel}{theory} \\
7.15 - \indexdef{}{command}{end}\mbox{\isa{\isacommand{end}}} & : & \isartrans{theory}{toplevel} \\
7.16 - \end{matharray}
7.17 -
7.18 - Isabelle/Isar theories are defined via theory, which contain both
7.19 - specifications and proofs; occasionally definitional mechanisms also
7.20 - require some explicit proof.
7.21 -
7.22 - The first ``real'' command of any theory has to be \mbox{\isa{\isacommand{theory}}}, which starts a new theory based on the merge of existing
7.23 - ones. Just preceding the \mbox{\isa{\isacommand{theory}}} keyword, there may be
7.24 - an optional \mbox{\isa{\isacommand{header}}} declaration, which is relevant to
7.25 - document preparation only; it acts very much like a special
7.26 - pre-theory markup command (cf.\ \secref{sec:markup-thy} and
7.27 - \secref{sec:markup-thy}). The \mbox{\isa{\isacommand{end}}} command concludes a
7.28 - theory development; it has to be the very last command of any theory
7.29 - file loaded in batch-mode.
7.30 -
7.31 - \begin{rail}
7.32 - 'header' text
7.33 - ;
7.34 - 'theory' name 'imports' (name +) uses? 'begin'
7.35 - ;
7.36 -
7.37 - uses: 'uses' ((name | parname) +);
7.38 - \end{rail}
7.39 -
7.40 - \begin{descr}
7.41 -
7.42 - \item [\mbox{\isa{\isacommand{header}}}~\isa{{\isachardoublequote}text{\isachardoublequote}}] provides plain text
7.43 - markup just preceding the formal beginning of a theory. In actual
7.44 - document preparation the corresponding {\LaTeX} macro \verb|\isamarkupheader| may be redefined to produce chapter or section
7.45 - headings. See also \secref{sec:markup-thy} and
7.46 - \secref{sec:markup-prf} for further markup commands.
7.47 -
7.48 - \item [\mbox{\isa{\isacommand{theory}}}~\isa{{\isachardoublequote}A\ {\isasymIMPORTS}\ B\isactrlsub {\isadigit{1}}\ {\isasymdots}\ B\isactrlsub n\ {\isasymBEGIN}{\isachardoublequote}}] starts a new theory \isa{A} based on the
7.49 - merge of existing theories \isa{{\isachardoublequote}B\isactrlsub {\isadigit{1}}\ {\isasymdots}\ B\isactrlsub n{\isachardoublequote}}.
7.50 -
7.51 - Due to inclusion of several ancestors, the overall theory structure
7.52 - emerging in an Isabelle session forms a directed acyclic graph
7.53 - (DAG). Isabelle's theory loader ensures that the sources
7.54 - contributing to the development graph are always up-to-date.
7.55 - Changed files are automatically reloaded when processing theory
7.56 - headers.
7.57 -
7.58 - The optional \indexdef{}{keyword}{uses}\mbox{\isa{\isakeyword{uses}}} specification declares additional
7.59 - dependencies on extra files (usually ML sources). Files will be
7.60 - loaded immediately (as ML), unless the name is put in parentheses,
7.61 - which merely documents the dependency to be resolved later in the
7.62 - text (typically via explicit \indexref{}{command}{use}\mbox{\isa{\isacommand{use}}} in the body text,
7.63 - see \secref{sec:ML}).
7.64 -
7.65 - \item [\mbox{\isa{\isacommand{end}}}] concludes the current theory definition or
7.66 - context switch.
7.67 -
7.68 - \end{descr}%
7.69 -\end{isamarkuptext}%
7.70 -\isamarkuptrue%
7.71 -%
7.72 \isamarkupsubsection{Markup commands \label{sec:markup-thy}%
7.73 }
7.74 \isamarkuptrue%
7.75 @@ -689,41 +624,6 @@
7.76 }
7.77 \isamarkuptrue%
7.78 %
7.79 -\begin{isamarkuptext}%
7.80 -Proof commands perform transitions of Isar/VM machine
7.81 - configurations, which are block-structured, consisting of a stack of
7.82 - nodes with three main components: logical proof context, current
7.83 - facts, and open goals. Isar/VM transitions are \emph{typed}
7.84 - according to the following three different modes of operation:
7.85 -
7.86 - \begin{descr}
7.87 -
7.88 - \item [\isa{{\isachardoublequote}proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}}] means that a new goal has just been
7.89 - stated that is now to be \emph{proven}; the next command may refine
7.90 - it by some proof method, and enter a sub-proof to establish the
7.91 - actual result.
7.92 -
7.93 - \item [\isa{{\isachardoublequote}proof{\isacharparenleft}state{\isacharparenright}{\isachardoublequote}}] is like a nested theory mode: the
7.94 - context may be augmented by \emph{stating} additional assumptions,
7.95 - intermediate results etc.
7.96 -
7.97 - \item [\isa{{\isachardoublequote}proof{\isacharparenleft}chain{\isacharparenright}{\isachardoublequote}}] is intermediate between \isa{{\isachardoublequote}proof{\isacharparenleft}state{\isacharparenright}{\isachardoublequote}} and \isa{{\isachardoublequote}proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}}: existing facts (i.e.\
7.98 - the contents of the special ``\indexref{}{fact}{this}\mbox{\isa{this}}'' register) have been
7.99 - just picked up in order to be used when refining the goal claimed
7.100 - next.
7.101 -
7.102 - \end{descr}
7.103 -
7.104 - The proof mode indicator may be read as a verb telling the writer
7.105 - what kind of operation may be performed next. The corresponding
7.106 - typings of proof commands restricts the shape of well-formed proof
7.107 - texts to particular command sequences. So dynamic arrangements of
7.108 - commands eventually turn out as static texts of a certain structure.
7.109 - \Appref{ap:refcard} gives a simplified grammar of the overall
7.110 - (extensible) language emerging that way.%
7.111 -\end{isamarkuptext}%
7.112 -\isamarkuptrue%
7.113 -%
7.114 \isamarkupsubsection{Markup commands \label{sec:markup-prf}%
7.115 }
7.116 \isamarkuptrue%
7.117 @@ -747,781 +647,6 @@
7.118 \end{isamarkuptext}%
7.119 \isamarkuptrue%
7.120 %
7.121 -\isamarkupsubsection{Context elements \label{sec:proof-context}%
7.122 -}
7.123 -\isamarkuptrue%
7.124 -%
7.125 -\begin{isamarkuptext}%
7.126 -\begin{matharray}{rcl}
7.127 - \indexdef{}{command}{fix}\mbox{\isa{\isacommand{fix}}} & : & \isartrans{proof(state)}{proof(state)} \\
7.128 - \indexdef{}{command}{assume}\mbox{\isa{\isacommand{assume}}} & : & \isartrans{proof(state)}{proof(state)} \\
7.129 - \indexdef{}{command}{presume}\mbox{\isa{\isacommand{presume}}} & : & \isartrans{proof(state)}{proof(state)} \\
7.130 - \indexdef{}{command}{def}\mbox{\isa{\isacommand{def}}} & : & \isartrans{proof(state)}{proof(state)} \\
7.131 - \end{matharray}
7.132 -
7.133 - The logical proof context consists of fixed variables and
7.134 - assumptions. The former closely correspond to Skolem constants, or
7.135 - meta-level universal quantification as provided by the Isabelle/Pure
7.136 - logical framework. Introducing some \emph{arbitrary, but fixed}
7.137 - variable via ``\mbox{\isa{\isacommand{fix}}}~\isa{x}'' results in a local value
7.138 - that may be used in the subsequent proof as any other variable or
7.139 - constant. Furthermore, any result \isa{{\isachardoublequote}{\isasymturnstile}\ {\isasymphi}{\isacharbrackleft}x{\isacharbrackright}{\isachardoublequote}} exported from
7.140 - the context will be universally closed wrt.\ \isa{x} at the
7.141 - outermost level: \isa{{\isachardoublequote}{\isasymturnstile}\ {\isasymAnd}x{\isachardot}\ {\isasymphi}{\isacharbrackleft}x{\isacharbrackright}{\isachardoublequote}} (this is expressed in normal
7.142 - form using Isabelle's meta-variables).
7.143 -
7.144 - Similarly, introducing some assumption \isa{{\isasymchi}} has two effects.
7.145 - On the one hand, a local theorem is created that may be used as a
7.146 - fact in subsequent proof steps. On the other hand, any result
7.147 - \isa{{\isachardoublequote}{\isasymchi}\ {\isasymturnstile}\ {\isasymphi}{\isachardoublequote}} exported from the context becomes conditional wrt.\
7.148 - the assumption: \isa{{\isachardoublequote}{\isasymturnstile}\ {\isasymchi}\ {\isasymLongrightarrow}\ {\isasymphi}{\isachardoublequote}}. Thus, solving an enclosing goal
7.149 - using such a result would basically introduce a new subgoal stemming
7.150 - from the assumption. How this situation is handled depends on the
7.151 - version of assumption command used: while \mbox{\isa{\isacommand{assume}}}
7.152 - insists on solving the subgoal by unification with some premise of
7.153 - the goal, \mbox{\isa{\isacommand{presume}}} leaves the subgoal unchanged in order
7.154 - to be proved later by the user.
7.155 -
7.156 - Local definitions, introduced by ``\mbox{\isa{\isacommand{def}}}~\isa{{\isachardoublequote}x\ {\isasymequiv}\ t{\isachardoublequote}}'', are achieved by combining ``\mbox{\isa{\isacommand{fix}}}~\isa{x}'' with
7.157 - another version of assumption that causes any hypothetical equation
7.158 - \isa{{\isachardoublequote}x\ {\isasymequiv}\ t{\isachardoublequote}} to be eliminated by the reflexivity rule. Thus,
7.159 - exporting some result \isa{{\isachardoublequote}x\ {\isasymequiv}\ t\ {\isasymturnstile}\ {\isasymphi}{\isacharbrackleft}x{\isacharbrackright}{\isachardoublequote}} yields \isa{{\isachardoublequote}{\isasymturnstile}\ {\isasymphi}{\isacharbrackleft}t{\isacharbrackright}{\isachardoublequote}}.
7.160 -
7.161 - \begin{rail}
7.162 - 'fix' (vars + 'and')
7.163 - ;
7.164 - ('assume' | 'presume') (props + 'and')
7.165 - ;
7.166 - 'def' (def + 'and')
7.167 - ;
7.168 - def: thmdecl? \\ name ('==' | equiv) term termpat?
7.169 - ;
7.170 - \end{rail}
7.171 -
7.172 - \begin{descr}
7.173 -
7.174 - \item [\mbox{\isa{\isacommand{fix}}}~\isa{x}] introduces a local variable
7.175 - \isa{x} that is \emph{arbitrary, but fixed.}
7.176 -
7.177 - \item [\mbox{\isa{\isacommand{assume}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} and \mbox{\isa{\isacommand{presume}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}}] introduce a local fact \isa{{\isachardoublequote}{\isasymphi}\ {\isasymturnstile}\ {\isasymphi}{\isachardoublequote}} by
7.178 - assumption. Subsequent results applied to an enclosing goal (e.g.\
7.179 - by \indexref{}{command}{show}\mbox{\isa{\isacommand{show}}}) are handled as follows: \mbox{\isa{\isacommand{assume}}} expects to be able to unify with existing premises in the
7.180 - goal, while \mbox{\isa{\isacommand{presume}}} leaves \isa{{\isasymphi}} as new subgoals.
7.181 -
7.182 - Several lists of assumptions may be given (separated by
7.183 - \indexref{}{keyword}{and}\mbox{\isa{\isakeyword{and}}}; the resulting list of current facts consists
7.184 - of all of these concatenated.
7.185 -
7.186 - \item [\mbox{\isa{\isacommand{def}}}~\isa{{\isachardoublequote}x\ {\isasymequiv}\ t{\isachardoublequote}}] introduces a local
7.187 - (non-polymorphic) definition. In results exported from the context,
7.188 - \isa{x} is replaced by \isa{t}. Basically, ``\mbox{\isa{\isacommand{def}}}~\isa{{\isachardoublequote}x\ {\isasymequiv}\ t{\isachardoublequote}}'' abbreviates ``\mbox{\isa{\isacommand{fix}}}~\isa{x}~\mbox{\isa{\isacommand{assume}}}~\isa{{\isachardoublequote}x\ {\isasymequiv}\ t{\isachardoublequote}}'', with the resulting
7.189 - hypothetical equation solved by reflexivity.
7.190 -
7.191 - The default name for the definitional equation is \isa{x{\isacharunderscore}def}.
7.192 - Several simultaneous definitions may be given at the same time.
7.193 -
7.194 - \end{descr}
7.195 -
7.196 - The special name \indexref{}{fact}{prems}\mbox{\isa{prems}} refers to all assumptions of the
7.197 - current context as a list of theorems. This feature should be used
7.198 - with great care! It is better avoided in final proof texts.%
7.199 -\end{isamarkuptext}%
7.200 -\isamarkuptrue%
7.201 -%
7.202 -\isamarkupsubsection{Facts and forward chaining%
7.203 -}
7.204 -\isamarkuptrue%
7.205 -%
7.206 -\begin{isamarkuptext}%
7.207 -\begin{matharray}{rcl}
7.208 - \indexdef{}{command}{note}\mbox{\isa{\isacommand{note}}} & : & \isartrans{proof(state)}{proof(state)} \\
7.209 - \indexdef{}{command}{then}\mbox{\isa{\isacommand{then}}} & : & \isartrans{proof(state)}{proof(chain)} \\
7.210 - \indexdef{}{command}{from}\mbox{\isa{\isacommand{from}}} & : & \isartrans{proof(state)}{proof(chain)} \\
7.211 - \indexdef{}{command}{with}\mbox{\isa{\isacommand{with}}} & : & \isartrans{proof(state)}{proof(chain)} \\
7.212 - \indexdef{}{command}{using}\mbox{\isa{\isacommand{using}}} & : & \isartrans{proof(prove)}{proof(prove)} \\
7.213 - \indexdef{}{command}{unfolding}\mbox{\isa{\isacommand{unfolding}}} & : & \isartrans{proof(prove)}{proof(prove)} \\
7.214 - \end{matharray}
7.215 -
7.216 - New facts are established either by assumption or proof of local
7.217 - statements. Any fact will usually be involved in further proofs,
7.218 - either as explicit arguments of proof methods, or when forward
7.219 - chaining towards the next goal via \mbox{\isa{\isacommand{then}}} (and variants);
7.220 - \mbox{\isa{\isacommand{from}}} and \mbox{\isa{\isacommand{with}}} are composite forms
7.221 - involving \mbox{\isa{\isacommand{note}}}. The \mbox{\isa{\isacommand{using}}} elements
7.222 - augments the collection of used facts \emph{after} a goal has been
7.223 - stated. Note that the special theorem name \indexref{}{fact}{this}\mbox{\isa{this}} refers
7.224 - to the most recently established facts, but only \emph{before}
7.225 - issuing a follow-up claim.
7.226 -
7.227 - \begin{rail}
7.228 - 'note' (thmdef? thmrefs + 'and')
7.229 - ;
7.230 - ('from' | 'with' | 'using' | 'unfolding') (thmrefs + 'and')
7.231 - ;
7.232 - \end{rail}
7.233 -
7.234 - \begin{descr}
7.235 -
7.236 - \item [\mbox{\isa{\isacommand{note}}}~\isa{{\isachardoublequote}a\ {\isacharequal}\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}}]
7.237 - recalls existing facts \isa{{\isachardoublequote}b\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub n{\isachardoublequote}}, binding
7.238 - the result as \isa{a}. Note that attributes may be involved as
7.239 - well, both on the left and right hand sides.
7.240 -
7.241 - \item [\mbox{\isa{\isacommand{then}}}] indicates forward chaining by the current
7.242 - facts in order to establish the goal to be claimed next. The
7.243 - initial proof method invoked to refine that will be offered the
7.244 - facts to do ``anything appropriate'' (see also
7.245 - \secref{sec:proof-steps}). For example, method \indexref{}{method}{rule}\mbox{\isa{rule}}
7.246 - (see \secref{sec:pure-meth-att}) would typically do an elimination
7.247 - rather than an introduction. Automatic methods usually insert the
7.248 - facts into the goal state before operation. This provides a simple
7.249 - scheme to control relevance of facts in automated proof search.
7.250 -
7.251 - \item [\mbox{\isa{\isacommand{from}}}~\isa{b}] abbreviates ``\mbox{\isa{\isacommand{note}}}~\isa{b}~\mbox{\isa{\isacommand{then}}}''; thus \mbox{\isa{\isacommand{then}}} is
7.252 - equivalent to ``\mbox{\isa{\isacommand{from}}}~\isa{this}''.
7.253 -
7.254 - \item [\mbox{\isa{\isacommand{with}}}~\isa{{\isachardoublequote}b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}}]
7.255 - abbreviates ``\mbox{\isa{\isacommand{from}}}~\isa{{\isachardoublequote}b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n\ {\isasymAND}\ this{\isachardoublequote}}''; thus the forward chaining is from earlier facts together
7.256 - with the current ones.
7.257 -
7.258 - \item [\mbox{\isa{\isacommand{using}}}~\isa{{\isachardoublequote}b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}}] augments
7.259 - the facts being currently indicated for use by a subsequent
7.260 - refinement step (such as \indexref{}{command}{apply}\mbox{\isa{\isacommand{apply}}} or \indexref{}{command}{proof}\mbox{\isa{\isacommand{proof}}}).
7.261 -
7.262 - \item [\mbox{\isa{\isacommand{unfolding}}}~\isa{{\isachardoublequote}b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}}] is
7.263 - structurally similar to \mbox{\isa{\isacommand{using}}}, but unfolds definitional
7.264 - equations \isa{{\isachardoublequote}b\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}\ b\isactrlsub n{\isachardoublequote}} throughout the goal state
7.265 - and facts.
7.266 -
7.267 - \end{descr}
7.268 -
7.269 - Forward chaining with an empty list of theorems is the same as not
7.270 - chaining at all. Thus ``\mbox{\isa{\isacommand{from}}}~\isa{nothing}'' has no
7.271 - effect apart from entering \isa{{\isachardoublequote}prove{\isacharparenleft}chain{\isacharparenright}{\isachardoublequote}} mode, since
7.272 - \indexref{}{fact}{nothing}\mbox{\isa{nothing}} is bound to the empty list of theorems.
7.273 -
7.274 - Basic proof methods (such as \indexref{}{method}{rule}\mbox{\isa{rule}}) expect multiple
7.275 - facts to be given in their proper order, corresponding to a prefix
7.276 - of the premises of the rule involved. Note that positions may be
7.277 - easily skipped using something like \mbox{\isa{\isacommand{from}}}~\isa{{\isachardoublequote}{\isacharunderscore}\ {\isasymAND}\ a\ {\isasymAND}\ b{\isachardoublequote}}, for example. This involves the trivial rule
7.278 - \isa{{\isachardoublequote}PROP\ {\isasympsi}\ {\isasymLongrightarrow}\ PROP\ {\isasympsi}{\isachardoublequote}}, which is bound in Isabelle/Pure as
7.279 - ``\indexref{}{fact}{\_}\mbox{\isa{{\isacharunderscore}}}'' (underscore).
7.280 -
7.281 - Automated methods (such as \mbox{\isa{simp}} or \mbox{\isa{auto}}) just
7.282 - insert any given facts before their usual operation. Depending on
7.283 - the kind of procedure involved, the order of facts is less
7.284 - significant here.%
7.285 -\end{isamarkuptext}%
7.286 -\isamarkuptrue%
7.287 -%
7.288 -\isamarkupsubsection{Goal statements \label{sec:goals}%
7.289 -}
7.290 -\isamarkuptrue%
7.291 -%
7.292 -\begin{isamarkuptext}%
7.293 -\begin{matharray}{rcl}
7.294 - \indexdef{}{command}{lemma}\mbox{\isa{\isacommand{lemma}}} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
7.295 - \indexdef{}{command}{theorem}\mbox{\isa{\isacommand{theorem}}} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
7.296 - \indexdef{}{command}{corollary}\mbox{\isa{\isacommand{corollary}}} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
7.297 - \indexdef{}{command}{have}\mbox{\isa{\isacommand{have}}} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
7.298 - \indexdef{}{command}{show}\mbox{\isa{\isacommand{show}}} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
7.299 - \indexdef{}{command}{hence}\mbox{\isa{\isacommand{hence}}} & : & \isartrans{proof(state)}{proof(prove)} \\
7.300 - \indexdef{}{command}{thus}\mbox{\isa{\isacommand{thus}}} & : & \isartrans{proof(state)}{proof(prove)} \\
7.301 - \indexdef{}{command}{print\_statement}\mbox{\isa{\isacommand{print{\isacharunderscore}statement}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
7.302 - \end{matharray}
7.303 -
7.304 - From a theory context, proof mode is entered by an initial goal
7.305 - command such as \mbox{\isa{\isacommand{lemma}}}, \mbox{\isa{\isacommand{theorem}}}, or
7.306 - \mbox{\isa{\isacommand{corollary}}}. Within a proof, new claims may be
7.307 - introduced locally as well; four variants are available here to
7.308 - indicate whether forward chaining of facts should be performed
7.309 - initially (via \indexref{}{command}{then}\mbox{\isa{\isacommand{then}}}), and whether the final result
7.310 - is meant to solve some pending goal.
7.311 -
7.312 - Goals may consist of multiple statements, resulting in a list of
7.313 - facts eventually. A pending multi-goal is internally represented as
7.314 - a meta-level conjunction (printed as \isa{{\isachardoublequote}{\isacharampersand}{\isacharampersand}{\isachardoublequote}}), which is usually
7.315 - split into the corresponding number of sub-goals prior to an initial
7.316 - method application, via \indexref{}{command}{proof}\mbox{\isa{\isacommand{proof}}}
7.317 - (\secref{sec:proof-steps}) or \indexref{}{command}{apply}\mbox{\isa{\isacommand{apply}}}
7.318 - (\secref{sec:tactic-commands}). The \indexref{}{method}{induct}\mbox{\isa{induct}} method
7.319 - covered in \secref{sec:cases-induct} acts on multiple claims
7.320 - simultaneously.
7.321 -
7.322 - Claims at the theory level may be either in short or long form. A
7.323 - short goal merely consists of several simultaneous propositions
7.324 - (often just one). A long goal includes an explicit context
7.325 - specification for the subsequent conclusion, involving local
7.326 - parameters and assumptions. Here the role of each part of the
7.327 - statement is explicitly marked by separate keywords (see also
7.328 - \secref{sec:locale}); the local assumptions being introduced here
7.329 - are available as \indexref{}{fact}{assms}\mbox{\isa{assms}} in the proof. Moreover, there
7.330 - are two kinds of conclusions: \indexdef{}{element}{shows}\mbox{\isa{\isakeyword{shows}}} states several
7.331 - simultaneous propositions (essentially a big conjunction), while
7.332 - \indexdef{}{element}{obtains}\mbox{\isa{\isakeyword{obtains}}} claims several simultaneous simultaneous
7.333 - contexts of (essentially a big disjunction of eliminated parameters
7.334 - and assumptions, cf.\ \secref{sec:obtain}).
7.335 -
7.336 - \begin{rail}
7.337 - ('lemma' | 'theorem' | 'corollary') target? (goal | longgoal)
7.338 - ;
7.339 - ('have' | 'show' | 'hence' | 'thus') goal
7.340 - ;
7.341 - 'print\_statement' modes? thmrefs
7.342 - ;
7.343 -
7.344 - goal: (props + 'and')
7.345 - ;
7.346 - longgoal: thmdecl? (contextelem *) conclusion
7.347 - ;
7.348 - conclusion: 'shows' goal | 'obtains' (parname? case + '|')
7.349 - ;
7.350 - case: (vars + 'and') 'where' (props + 'and')
7.351 - ;
7.352 - \end{rail}
7.353 -
7.354 - \begin{descr}
7.355 -
7.356 - \item [\mbox{\isa{\isacommand{lemma}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}}] enters proof mode with
7.357 - \isa{{\isasymphi}} as main goal, eventually resulting in some fact \isa{{\isachardoublequote}{\isasymturnstile}\ {\isasymphi}{\isachardoublequote}} to be put back into the target context. An additional
7.358 - \railnonterm{context} specification may build up an initial proof
7.359 - context for the subsequent claim; this includes local definitions
7.360 - and syntax as well, see the definition of \mbox{\isa{contextelem}} in
7.361 - \secref{sec:locale}.
7.362 -
7.363 - \item [\mbox{\isa{\isacommand{theorem}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} and \mbox{\isa{\isacommand{corollary}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}}] are essentially the same as \mbox{\isa{\isacommand{lemma}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}}, but the facts are internally marked as
7.364 - being of a different kind. This discrimination acts like a formal
7.365 - comment.
7.366 -
7.367 - \item [\mbox{\isa{\isacommand{have}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}}] claims a local goal,
7.368 - eventually resulting in a fact within the current logical context.
7.369 - This operation is completely independent of any pending sub-goals of
7.370 - an enclosing goal statements, so \mbox{\isa{\isacommand{have}}} may be freely
7.371 - used for experimental exploration of potential results within a
7.372 - proof body.
7.373 -
7.374 - \item [\mbox{\isa{\isacommand{show}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}}] is like \mbox{\isa{\isacommand{have}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} plus a second stage to refine some pending
7.375 - sub-goal for each one of the finished result, after having been
7.376 - exported into the corresponding context (at the head of the
7.377 - sub-proof of this \mbox{\isa{\isacommand{show}}} command).
7.378 -
7.379 - To accommodate interactive debugging, resulting rules are printed
7.380 - before being applied internally. Even more, interactive execution
7.381 - of \mbox{\isa{\isacommand{show}}} predicts potential failure and displays the
7.382 - resulting error as a warning beforehand. Watch out for the
7.383 - following message:
7.384 -
7.385 - %FIXME proper antiquitation
7.386 - \begin{ttbox}
7.387 - Problem! Local statement will fail to solve any pending goal
7.388 - \end{ttbox}
7.389 -
7.390 - \item [\mbox{\isa{\isacommand{hence}}}] abbreviates ``\mbox{\isa{\isacommand{then}}}~\mbox{\isa{\isacommand{have}}}'', i.e.\ claims a local goal to be proven by forward
7.391 - chaining the current facts. Note that \mbox{\isa{\isacommand{hence}}} is also
7.392 - equivalent to ``\mbox{\isa{\isacommand{from}}}~\isa{this}~\mbox{\isa{\isacommand{have}}}''.
7.393 -
7.394 - \item [\mbox{\isa{\isacommand{thus}}}] abbreviates ``\mbox{\isa{\isacommand{then}}}~\mbox{\isa{\isacommand{show}}}''. Note that \mbox{\isa{\isacommand{thus}}} is also equivalent to
7.395 - ``\mbox{\isa{\isacommand{from}}}~\isa{this}~\mbox{\isa{\isacommand{show}}}''.
7.396 -
7.397 - \item [\mbox{\isa{\isacommand{print{\isacharunderscore}statement}}}~\isa{a}] prints facts from the
7.398 - current theory or proof context in long statement form, according to
7.399 - the syntax for \mbox{\isa{\isacommand{lemma}}} given above.
7.400 -
7.401 - \end{descr}
7.402 -
7.403 - Any goal statement causes some term abbreviations (such as
7.404 - \indexref{}{variable}{?thesis}\mbox{\isa{{\isacharquery}thesis}}) to be bound automatically, see also
7.405 - \secref{sec:term-abbrev}. Furthermore, the local context of a
7.406 - (non-atomic) goal is provided via the \indexref{}{case}{rule\_context}\mbox{\isa{rule{\isacharunderscore}context}} case.
7.407 -
7.408 - The optional case names of \indexref{}{element}{obtains}\mbox{\isa{\isakeyword{obtains}}} have a twofold
7.409 - meaning: (1) during the of this claim they refer to the the local
7.410 - context introductions, (2) the resulting rule is annotated
7.411 - accordingly to support symbolic case splits when used with the
7.412 - \indexref{}{method}{cases}\mbox{\isa{cases}} method (cf. \secref{sec:cases-induct}).
7.413 -
7.414 - \medskip
7.415 -
7.416 - \begin{warn}
7.417 - Isabelle/Isar suffers theory-level goal statements to contain
7.418 - \emph{unbound schematic variables}, although this does not conform
7.419 - to the aim of human-readable proof documents! The main problem
7.420 - with schematic goals is that the actual outcome is usually hard to
7.421 - predict, depending on the behavior of the proof methods applied
7.422 - during the course of reasoning. Note that most semi-automated
7.423 - methods heavily depend on several kinds of implicit rule
7.424 - declarations within the current theory context. As this would
7.425 - also result in non-compositional checking of sub-proofs,
7.426 - \emph{local goals} are not allowed to be schematic at all.
7.427 - Nevertheless, schematic goals do have their use in Prolog-style
7.428 - interactive synthesis of proven results, usually by stepwise
7.429 - refinement via emulation of traditional Isabelle tactic scripts
7.430 - (see also \secref{sec:tactic-commands}). In any case, users
7.431 - should know what they are doing.
7.432 - \end{warn}%
7.433 -\end{isamarkuptext}%
7.434 -\isamarkuptrue%
7.435 -%
7.436 -\isamarkupsubsection{Initial and terminal proof steps \label{sec:proof-steps}%
7.437 -}
7.438 -\isamarkuptrue%
7.439 -%
7.440 -\begin{isamarkuptext}%
7.441 -\begin{matharray}{rcl}
7.442 - \indexdef{}{command}{proof}\mbox{\isa{\isacommand{proof}}} & : & \isartrans{proof(prove)}{proof(state)} \\
7.443 - \indexdef{}{command}{qed}\mbox{\isa{\isacommand{qed}}} & : & \isartrans{proof(state)}{proof(state) ~|~ theory} \\
7.444 - \indexdef{}{command}{by}\mbox{\isa{\isacommand{by}}} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
7.445 - \indexdef{}{command}{..}\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
7.446 - \indexdef{}{command}{.}\mbox{\isa{\isacommand{{\isachardot}}}} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
7.447 - \indexdef{}{command}{sorry}\mbox{\isa{\isacommand{sorry}}} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
7.448 - \end{matharray}
7.449 -
7.450 - Arbitrary goal refinement via tactics is considered harmful.
7.451 - Structured proof composition in Isar admits proof methods to be
7.452 - invoked in two places only.
7.453 -
7.454 - \begin{enumerate}
7.455 -
7.456 - \item An \emph{initial} refinement step \indexref{}{command}{proof}\mbox{\isa{\isacommand{proof}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}{\isachardoublequote}} reduces a newly stated goal to a number
7.457 - of sub-goals that are to be solved later. Facts are passed to
7.458 - \isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}{\isachardoublequote}} for forward chaining, if so indicated by \isa{{\isachardoublequote}proof{\isacharparenleft}chain{\isacharparenright}{\isachardoublequote}} mode.
7.459 -
7.460 - \item A \emph{terminal} conclusion step \indexref{}{command}{qed}\mbox{\isa{\isacommand{qed}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{2}}{\isachardoublequote}} is intended to solve remaining goals. No facts are
7.461 - passed to \isa{{\isachardoublequote}m\isactrlsub {\isadigit{2}}{\isachardoublequote}}.
7.462 -
7.463 - \end{enumerate}
7.464 -
7.465 - The only other (proper) way to affect pending goals in a proof body
7.466 - is by \indexref{}{command}{show}\mbox{\isa{\isacommand{show}}}, which involves an explicit statement of
7.467 - what is to be solved eventually. Thus we avoid the fundamental
7.468 - problem of unstructured tactic scripts that consist of numerous
7.469 - consecutive goal transformations, with invisible effects.
7.470 -
7.471 - \medskip As a general rule of thumb for good proof style, initial
7.472 - proof methods should either solve the goal completely, or constitute
7.473 - some well-understood reduction to new sub-goals. Arbitrary
7.474 - automatic proof tools that are prone leave a large number of badly
7.475 - structured sub-goals are no help in continuing the proof document in
7.476 - an intelligible manner.
7.477 -
7.478 - Unless given explicitly by the user, the default initial method is
7.479 - ``\indexref{}{method}{rule}\mbox{\isa{rule}}'', which applies a single standard elimination
7.480 - or introduction rule according to the topmost symbol involved.
7.481 - There is no separate default terminal method. Any remaining goals
7.482 - are always solved by assumption in the very last step.
7.483 -
7.484 - \begin{rail}
7.485 - 'proof' method?
7.486 - ;
7.487 - 'qed' method?
7.488 - ;
7.489 - 'by' method method?
7.490 - ;
7.491 - ('.' | '..' | 'sorry')
7.492 - ;
7.493 - \end{rail}
7.494 -
7.495 - \begin{descr}
7.496 -
7.497 - \item [\mbox{\isa{\isacommand{proof}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}{\isachardoublequote}}] refines the goal by
7.498 - proof method \isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}{\isachardoublequote}}; facts for forward chaining are
7.499 - passed if so indicated by \isa{{\isachardoublequote}proof{\isacharparenleft}chain{\isacharparenright}{\isachardoublequote}} mode.
7.500 -
7.501 - \item [\mbox{\isa{\isacommand{qed}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{2}}{\isachardoublequote}}] refines any remaining
7.502 - goals by proof method \isa{{\isachardoublequote}m\isactrlsub {\isadigit{2}}{\isachardoublequote}} and concludes the
7.503 - sub-proof by assumption. If the goal had been \isa{{\isachardoublequote}show{\isachardoublequote}} (or
7.504 - \isa{{\isachardoublequote}thus{\isachardoublequote}}), some pending sub-goal is solved as well by the rule
7.505 - resulting from the result \emph{exported} into the enclosing goal
7.506 - context. Thus \isa{{\isachardoublequote}qed{\isachardoublequote}} may fail for two reasons: either \isa{{\isachardoublequote}m\isactrlsub {\isadigit{2}}{\isachardoublequote}} fails, or the resulting rule does not fit to any
7.507 - pending goal\footnote{This includes any additional ``strong''
7.508 - assumptions as introduced by \mbox{\isa{\isacommand{assume}}}.} of the enclosing
7.509 - context. Debugging such a situation might involve temporarily
7.510 - changing \mbox{\isa{\isacommand{show}}} into \mbox{\isa{\isacommand{have}}}, or weakening the
7.511 - local context by replacing occurrences of \mbox{\isa{\isacommand{assume}}} by
7.512 - \mbox{\isa{\isacommand{presume}}}.
7.513 -
7.514 - \item [\mbox{\isa{\isacommand{by}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}\ m\isactrlsub {\isadigit{2}}{\isachardoublequote}}] is a
7.515 - \emph{terminal proof}\index{proof!terminal}; it abbreviates
7.516 - \mbox{\isa{\isacommand{proof}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}{\isachardoublequote}}~\isa{{\isachardoublequote}qed{\isachardoublequote}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{2}}{\isachardoublequote}}, but with backtracking across both methods. Debugging
7.517 - an unsuccessful \mbox{\isa{\isacommand{by}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}\ m\isactrlsub {\isadigit{2}}{\isachardoublequote}}
7.518 - command can be done by expanding its definition; in many cases
7.519 - \mbox{\isa{\isacommand{proof}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}{\isachardoublequote}} (or even \isa{{\isachardoublequote}apply{\isachardoublequote}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}{\isachardoublequote}}) is already sufficient to see the
7.520 - problem.
7.521 -
7.522 - \item [``\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}''] is a \emph{default
7.523 - proof}\index{proof!default}; it abbreviates \mbox{\isa{\isacommand{by}}}~\isa{{\isachardoublequote}rule{\isachardoublequote}}.
7.524 -
7.525 - \item [``\mbox{\isa{\isacommand{{\isachardot}}}}''] is a \emph{trivial
7.526 - proof}\index{proof!trivial}; it abbreviates \mbox{\isa{\isacommand{by}}}~\isa{{\isachardoublequote}this{\isachardoublequote}}.
7.527 -
7.528 - \item [\mbox{\isa{\isacommand{sorry}}}] is a \emph{fake proof}\index{proof!fake}
7.529 - pretending to solve the pending claim without further ado. This
7.530 - only works in interactive development, or if the \verb|quick_and_dirty| flag is enabled (in ML). Facts emerging from fake
7.531 - proofs are not the real thing. Internally, each theorem container
7.532 - is tainted by an oracle invocation, which is indicated as ``\isa{{\isachardoublequote}{\isacharbrackleft}{\isacharbang}{\isacharbrackright}{\isachardoublequote}}'' in the printed result.
7.533 -
7.534 - The most important application of \mbox{\isa{\isacommand{sorry}}} is to support
7.535 - experimentation and top-down proof development.
7.536 -
7.537 - \end{descr}%
7.538 -\end{isamarkuptext}%
7.539 -\isamarkuptrue%
7.540 -%
7.541 -\isamarkupsubsection{Fundamental methods and attributes \label{sec:pure-meth-att}%
7.542 -}
7.543 -\isamarkuptrue%
7.544 -%
7.545 -\begin{isamarkuptext}%
7.546 -The following proof methods and attributes refer to basic logical
7.547 - operations of Isar. Further methods and attributes are provided by
7.548 - several generic and object-logic specific tools and packages (see
7.549 - \chref{ch:gen-tools} and \chref{ch:hol}).
7.550 -
7.551 - \begin{matharray}{rcl}
7.552 - \indexdef{}{method}{-}\mbox{\isa{{\isacharminus}}} & : & \isarmeth \\
7.553 - \indexdef{}{method}{fact}\mbox{\isa{fact}} & : & \isarmeth \\
7.554 - \indexdef{}{method}{assumption}\mbox{\isa{assumption}} & : & \isarmeth \\
7.555 - \indexdef{}{method}{this}\mbox{\isa{this}} & : & \isarmeth \\
7.556 - \indexdef{}{method}{rule}\mbox{\isa{rule}} & : & \isarmeth \\
7.557 - \indexdef{}{method}{iprover}\mbox{\isa{iprover}} & : & \isarmeth \\[0.5ex]
7.558 - \indexdef{}{attribute}{intro}\mbox{\isa{intro}} & : & \isaratt \\
7.559 - \indexdef{}{attribute}{elim}\mbox{\isa{elim}} & : & \isaratt \\
7.560 - \indexdef{}{attribute}{dest}\mbox{\isa{dest}} & : & \isaratt \\
7.561 - \indexdef{}{attribute}{rule}\mbox{\isa{rule}} & : & \isaratt \\[0.5ex]
7.562 - \indexdef{}{attribute}{OF}\mbox{\isa{OF}} & : & \isaratt \\
7.563 - \indexdef{}{attribute}{of}\mbox{\isa{of}} & : & \isaratt \\
7.564 - \indexdef{}{attribute}{where}\mbox{\isa{where}} & : & \isaratt \\
7.565 - \end{matharray}
7.566 -
7.567 - \begin{rail}
7.568 - 'fact' thmrefs?
7.569 - ;
7.570 - 'rule' thmrefs?
7.571 - ;
7.572 - 'iprover' ('!' ?) (rulemod *)
7.573 - ;
7.574 - rulemod: ('intro' | 'elim' | 'dest') ((('!' | () | '?') nat?) | 'del') ':' thmrefs
7.575 - ;
7.576 - ('intro' | 'elim' | 'dest') ('!' | () | '?') nat?
7.577 - ;
7.578 - 'rule' 'del'
7.579 - ;
7.580 - 'OF' thmrefs
7.581 - ;
7.582 - 'of' insts ('concl' ':' insts)?
7.583 - ;
7.584 - 'where' ((name | var | typefree | typevar) '=' (type | term) * 'and')
7.585 - ;
7.586 - \end{rail}
7.587 -
7.588 - \begin{descr}
7.589 -
7.590 - \item [``\mbox{\isa{{\isacharminus}}}'' (minus)] does nothing but insert the
7.591 - forward chaining facts as premises into the goal. Note that command
7.592 - \indexref{}{command}{proof}\mbox{\isa{\isacommand{proof}}} without any method actually performs a single
7.593 - reduction step using the \indexref{}{method}{rule}\mbox{\isa{rule}} method; thus a plain
7.594 - \emph{do-nothing} proof step would be ``\mbox{\isa{\isacommand{proof}}}~\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' rather than \mbox{\isa{\isacommand{proof}}} alone.
7.595 -
7.596 - \item [\mbox{\isa{fact}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}] composes
7.597 - some fact from \isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ a\isactrlsub n{\isachardoublequote}} (or implicitly from
7.598 - the current proof context) modulo unification of schematic type and
7.599 - term variables. The rule structure is not taken into account, i.e.\
7.600 - meta-level implication is considered atomic. This is the same
7.601 - principle underlying literal facts (cf.\ \secref{sec:syn-att}):
7.602 - ``\mbox{\isa{\isacommand{have}}}~\isa{{\isachardoublequote}{\isasymphi}{\isachardoublequote}}~\mbox{\isa{\isacommand{by}}}~\isa{fact}'' is
7.603 - equivalent to ``\mbox{\isa{\isacommand{note}}}~\verb|`|\isa{{\isasymphi}}\verb|`|'' provided that \isa{{\isachardoublequote}{\isasymturnstile}\ {\isasymphi}{\isachardoublequote}} is an instance of some known
7.604 - \isa{{\isachardoublequote}{\isasymturnstile}\ {\isasymphi}{\isachardoublequote}} in the proof context.
7.605 -
7.606 - \item [\mbox{\isa{assumption}}] solves some goal by a single assumption
7.607 - step. All given facts are guaranteed to participate in the
7.608 - refinement; this means there may be only 0 or 1 in the first place.
7.609 - Recall that \mbox{\isa{\isacommand{qed}}} (\secref{sec:proof-steps}) already
7.610 - concludes any remaining sub-goals by assumption, so structured
7.611 - proofs usually need not quote the \mbox{\isa{assumption}} method at
7.612 - all.
7.613 -
7.614 - \item [\mbox{\isa{this}}] applies all of the current facts directly as
7.615 - rules. Recall that ``\mbox{\isa{\isacommand{{\isachardot}}}}'' (dot) abbreviates ``\mbox{\isa{\isacommand{by}}}~\isa{this}''.
7.616 -
7.617 - \item [\mbox{\isa{rule}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}] applies some
7.618 - rule given as argument in backward manner; facts are used to reduce
7.619 - the rule before applying it to the goal. Thus \mbox{\isa{rule}}
7.620 - without facts is plain introduction, while with facts it becomes
7.621 - elimination.
7.622 -
7.623 - When no arguments are given, the \mbox{\isa{rule}} method tries to pick
7.624 - appropriate rules automatically, as declared in the current context
7.625 - using the \mbox{\isa{intro}}, \mbox{\isa{elim}}, \mbox{\isa{dest}}
7.626 - attributes (see below). This is the default behavior of \mbox{\isa{\isacommand{proof}}} and ``\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}'' (double-dot) steps (see
7.627 - \secref{sec:proof-steps}).
7.628 -
7.629 - \item [\mbox{\isa{iprover}}] performs intuitionistic proof search,
7.630 - depending on specifically declared rules from the context, or given
7.631 - as explicit arguments. Chained facts are inserted into the goal
7.632 - before commencing proof search; ``\mbox{\isa{iprover}}\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}''
7.633 - means to include the current \mbox{\isa{prems}} as well.
7.634 -
7.635 - Rules need to be classified as \mbox{\isa{intro}}, \mbox{\isa{elim}}, or \mbox{\isa{dest}}; here the ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' indicator
7.636 - refers to ``safe'' rules, which may be applied aggressively (without
7.637 - considering back-tracking later). Rules declared with ``\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}'' are ignored in proof search (the single-step \mbox{\isa{rule}}
7.638 - method still observes these). An explicit weight annotation may be
7.639 - given as well; otherwise the number of rule premises will be taken
7.640 - into account here.
7.641 -
7.642 - \item [\mbox{\isa{intro}}, \mbox{\isa{elim}}, and \mbox{\isa{dest}}]
7.643 - declare introduction, elimination, and destruct rules, to be used
7.644 - with the \mbox{\isa{rule}} and \mbox{\isa{iprover}} methods. Note that
7.645 - the latter will ignore rules declared with ``\isa{{\isachardoublequote}{\isacharquery}{\isachardoublequote}}'', while
7.646 - ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' are used most aggressively.
7.647 -
7.648 - The classical reasoner (see \secref{sec:classical}) introduces its
7.649 - own variants of these attributes; use qualified names to access the
7.650 - present versions of Isabelle/Pure, i.e.\ \mbox{\isa{Pure{\isachardot}intro}}.
7.651 -
7.652 - \item [\mbox{\isa{rule}}~\isa{del}] undeclares introduction,
7.653 - elimination, or destruct rules.
7.654 -
7.655 - \item [\mbox{\isa{OF}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}] applies some
7.656 - theorem to all of the given rules \isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ a\isactrlsub n{\isachardoublequote}}
7.657 - (in parallel). This corresponds to the \verb|"op MRS"| operation in
7.658 - ML, but note the reversed order. Positions may be effectively
7.659 - skipped by including ``\isa{{\isacharunderscore}}'' (underscore) as argument.
7.660 -
7.661 - \item [\mbox{\isa{of}}~\isa{{\isachardoublequote}t\isactrlsub {\isadigit{1}}\ {\isasymdots}\ t\isactrlsub n{\isachardoublequote}}] performs
7.662 - positional instantiation of term variables. The terms \isa{{\isachardoublequote}t\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ t\isactrlsub n{\isachardoublequote}} are substituted for any schematic
7.663 - variables occurring in a theorem from left to right; ``\isa{{\isacharunderscore}}'' (underscore) indicates to skip a position. Arguments following
7.664 - a ``\mbox{\isa{\isakeyword{concl}}}\isa{{\isachardoublequote}{\isacharcolon}{\isachardoublequote}}'' specification refer to positions
7.665 - of the conclusion of a rule.
7.666 -
7.667 - \item [\mbox{\isa{where}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isacharequal}\ t\isactrlsub {\isadigit{1}}\ {\isasymAND}\ {\isasymdots}\ x\isactrlsub n\ {\isacharequal}\ t\isactrlsub n{\isachardoublequote}}] performs named instantiation of schematic
7.668 - type and term variables occurring in a theorem. Schematic variables
7.669 - have to be specified on the left-hand side (e.g.\ \isa{{\isachardoublequote}{\isacharquery}x{\isadigit{1}}{\isachardot}{\isadigit{3}}{\isachardoublequote}}).
7.670 - The question mark may be omitted if the variable name is a plain
7.671 - identifier without index. As type instantiations are inferred from
7.672 - term instantiations, explicit type instantiations are seldom
7.673 - necessary.
7.674 -
7.675 - \end{descr}%
7.676 -\end{isamarkuptext}%
7.677 -\isamarkuptrue%
7.678 -%
7.679 -\isamarkupsubsection{Term abbreviations \label{sec:term-abbrev}%
7.680 -}
7.681 -\isamarkuptrue%
7.682 -%
7.683 -\begin{isamarkuptext}%
7.684 -\begin{matharray}{rcl}
7.685 - \indexdef{}{command}{let}\mbox{\isa{\isacommand{let}}} & : & \isartrans{proof(state)}{proof(state)} \\
7.686 - \indexdef{}{keyword}{is}\mbox{\isa{\isakeyword{is}}} & : & syntax \\
7.687 - \end{matharray}
7.688 -
7.689 - Abbreviations may be either bound by explicit \mbox{\isa{\isacommand{let}}}~\isa{{\isachardoublequote}p\ {\isasymequiv}\ t{\isachardoublequote}} statements, or by annotating assumptions or
7.690 - goal statements with a list of patterns ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIS}\ p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub n{\isacharparenright}{\isachardoublequote}}''. In both cases, higher-order matching is invoked to
7.691 - bind extra-logical term variables, which may be either named
7.692 - schematic variables of the form \isa{{\isacharquery}x}, or nameless dummies
7.693 - ``\mbox{\isa{{\isacharunderscore}}}'' (underscore). Note that in the \mbox{\isa{\isacommand{let}}}
7.694 - form the patterns occur on the left-hand side, while the \mbox{\isa{\isakeyword{is}}} patterns are in postfix position.
7.695 -
7.696 - Polymorphism of term bindings is handled in Hindley-Milner style,
7.697 - similar to ML. Type variables referring to local assumptions or
7.698 - open goal statements are \emph{fixed}, while those of finished
7.699 - results or bound by \mbox{\isa{\isacommand{let}}} may occur in \emph{arbitrary}
7.700 - instances later. Even though actual polymorphism should be rarely
7.701 - used in practice, this mechanism is essential to achieve proper
7.702 - incremental type-inference, as the user proceeds to build up the
7.703 - Isar proof text from left to right.
7.704 -
7.705 - \medskip Term abbreviations are quite different from local
7.706 - definitions as introduced via \mbox{\isa{\isacommand{def}}} (see
7.707 - \secref{sec:proof-context}). The latter are visible within the
7.708 - logic as actual equations, while abbreviations disappear during the
7.709 - input process just after type checking. Also note that \mbox{\isa{\isacommand{def}}} does not support polymorphism.
7.710 -
7.711 - \begin{rail}
7.712 - 'let' ((term + 'and') '=' term + 'and')
7.713 - ;
7.714 - \end{rail}
7.715 -
7.716 - The syntax of \mbox{\isa{\isakeyword{is}}} patterns follows \railnonterm{termpat}
7.717 - or \railnonterm{proppat} (see \secref{sec:term-decls}).
7.718 -
7.719 - \begin{descr}
7.720 -
7.721 - \item [\mbox{\isa{\isacommand{let}}}~\isa{{\isachardoublequote}p\isactrlsub {\isadigit{1}}\ {\isacharequal}\ t\isactrlsub {\isadigit{1}}\ {\isasymAND}\ {\isasymdots}\ p\isactrlsub n\ {\isacharequal}\ t\isactrlsub n{\isachardoublequote}}] binds any text variables in patterns \isa{{\isachardoublequote}p\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ p\isactrlsub n{\isachardoublequote}} by simultaneous higher-order matching
7.722 - against terms \isa{{\isachardoublequote}t\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ t\isactrlsub n{\isachardoublequote}}.
7.723 -
7.724 - \item [\isa{{\isachardoublequote}{\isacharparenleft}{\isasymIS}\ p\isactrlsub {\isadigit{1}}\ {\isasymdots}\ p\isactrlsub n{\isacharparenright}{\isachardoublequote}}] resembles \mbox{\isa{\isacommand{let}}}, but matches \isa{{\isachardoublequote}p\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ p\isactrlsub n{\isachardoublequote}} against the
7.725 - preceding statement. Also note that \mbox{\isa{\isakeyword{is}}} is not a
7.726 - separate command, but part of others (such as \mbox{\isa{\isacommand{assume}}},
7.727 - \mbox{\isa{\isacommand{have}}} etc.).
7.728 -
7.729 - \end{descr}
7.730 -
7.731 - Some \emph{implicit} term abbreviations\index{term abbreviations}
7.732 - for goals and facts are available as well. For any open goal,
7.733 - \indexref{}{variable}{thesis}\mbox{\isa{thesis}} refers to its object-level statement,
7.734 - abstracted over any meta-level parameters (if present). Likewise,
7.735 - \indexref{}{variable}{this}\mbox{\isa{this}} is bound for fact statements resulting from
7.736 - assumptions or finished goals. In case \mbox{\isa{this}} refers to
7.737 - an object-logic statement that is an application \isa{{\isachardoublequote}f\ t{\isachardoublequote}}, then
7.738 - \isa{t} is bound to the special text variable ``\mbox{\isa{{\isasymdots}}}''
7.739 - (three dots). The canonical application of this convenience are
7.740 - calculational proofs (see \secref{sec:calculation}).%
7.741 -\end{isamarkuptext}%
7.742 -\isamarkuptrue%
7.743 -%
7.744 -\isamarkupsubsection{Block structure%
7.745 -}
7.746 -\isamarkuptrue%
7.747 -%
7.748 -\begin{isamarkuptext}%
7.749 -\begin{matharray}{rcl}
7.750 - \indexdef{}{command}{next}\mbox{\isa{\isacommand{next}}} & : & \isartrans{proof(state)}{proof(state)} \\
7.751 - \indexdef{}{command}{\{}\mbox{\isa{\isacommand{{\isacharbraceleft}}}} & : & \isartrans{proof(state)}{proof(state)} \\
7.752 - \indexdef{}{command}{\}}\mbox{\isa{\isacommand{{\isacharbraceright}}}} & : & \isartrans{proof(state)}{proof(state)} \\
7.753 - \end{matharray}
7.754 -
7.755 - While Isar is inherently block-structured, opening and closing
7.756 - blocks is mostly handled rather casually, with little explicit
7.757 - user-intervention. Any local goal statement automatically opens
7.758 - \emph{two} internal blocks, which are closed again when concluding
7.759 - the sub-proof (by \mbox{\isa{\isacommand{qed}}} etc.). Sections of different
7.760 - context within a sub-proof may be switched via \mbox{\isa{\isacommand{next}}},
7.761 - which is just a single block-close followed by block-open again.
7.762 - The effect of \mbox{\isa{\isacommand{next}}} is to reset the local proof context;
7.763 - there is no goal focus involved here!
7.764 -
7.765 - For slightly more advanced applications, there are explicit block
7.766 - parentheses as well. These typically achieve a stronger forward
7.767 - style of reasoning.
7.768 -
7.769 - \begin{descr}
7.770 -
7.771 - \item [\mbox{\isa{\isacommand{next}}}] switches to a fresh block within a
7.772 - sub-proof, resetting the local context to the initial one.
7.773 -
7.774 - \item [\mbox{\isa{\isacommand{{\isacharbraceleft}}}} and \mbox{\isa{\isacommand{{\isacharbraceright}}}}] explicitly open and close
7.775 - blocks. Any current facts pass through ``\mbox{\isa{\isacommand{{\isacharbraceleft}}}}''
7.776 - unchanged, while ``\mbox{\isa{\isacommand{{\isacharbraceright}}}}'' causes any result to be
7.777 - \emph{exported} into the enclosing context. Thus fixed variables
7.778 - are generalized, assumptions discharged, and local definitions
7.779 - unfolded (cf.\ \secref{sec:proof-context}). There is no difference
7.780 - of \mbox{\isa{\isacommand{assume}}} and \mbox{\isa{\isacommand{presume}}} in this mode of
7.781 - forward reasoning --- in contrast to plain backward reasoning with
7.782 - the result exported at \mbox{\isa{\isacommand{show}}} time.
7.783 -
7.784 - \end{descr}%
7.785 -\end{isamarkuptext}%
7.786 -\isamarkuptrue%
7.787 -%
7.788 -\isamarkupsubsection{Emulating tactic scripts \label{sec:tactic-commands}%
7.789 -}
7.790 -\isamarkuptrue%
7.791 -%
7.792 -\begin{isamarkuptext}%
7.793 -The Isar provides separate commands to accommodate tactic-style
7.794 - proof scripts within the same system. While being outside the
7.795 - orthodox Isar proof language, these might come in handy for
7.796 - interactive exploration and debugging, or even actual tactical proof
7.797 - within new-style theories (to benefit from document preparation, for
7.798 - example). See also \secref{sec:tactics} for actual tactics, that
7.799 - have been encapsulated as proof methods. Proper proof methods may
7.800 - be used in scripts, too.
7.801 -
7.802 - \begin{matharray}{rcl}
7.803 - \indexdef{}{command}{apply}\mbox{\isa{\isacommand{apply}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isartrans{proof(prove)}{proof(prove)} \\
7.804 - \indexdef{}{command}{apply\_end}\mbox{\isa{\isacommand{apply{\isacharunderscore}end}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isartrans{proof(state)}{proof(state)} \\
7.805 - \indexdef{}{command}{done}\mbox{\isa{\isacommand{done}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isartrans{proof(prove)}{proof(state)} \\
7.806 - \indexdef{}{command}{defer}\mbox{\isa{\isacommand{defer}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isartrans{proof}{proof} \\
7.807 - \indexdef{}{command}{prefer}\mbox{\isa{\isacommand{prefer}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isartrans{proof}{proof} \\
7.808 - \indexdef{}{command}{back}\mbox{\isa{\isacommand{back}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isartrans{proof}{proof} \\
7.809 - \end{matharray}
7.810 -
7.811 - \begin{rail}
7.812 - ( 'apply' | 'apply\_end' ) method
7.813 - ;
7.814 - 'defer' nat?
7.815 - ;
7.816 - 'prefer' nat
7.817 - ;
7.818 - \end{rail}
7.819 -
7.820 - \begin{descr}
7.821 -
7.822 - \item [\mbox{\isa{\isacommand{apply}}}~\isa{m}] applies proof method \isa{m}
7.823 - in initial position, but unlike \mbox{\isa{\isacommand{proof}}} it retains
7.824 - ``\isa{{\isachardoublequote}proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}}'' mode. Thus consecutive method
7.825 - applications may be given just as in tactic scripts.
7.826 -
7.827 - Facts are passed to \isa{m} as indicated by the goal's
7.828 - forward-chain mode, and are \emph{consumed} afterwards. Thus any
7.829 - further \mbox{\isa{\isacommand{apply}}} command would always work in a purely
7.830 - backward manner.
7.831 -
7.832 - \item [\mbox{\isa{\isacommand{apply{\isacharunderscore}end}}}~\isa{{\isachardoublequote}m{\isachardoublequote}}] applies proof method
7.833 - \isa{m} as if in terminal position. Basically, this simulates a
7.834 - multi-step tactic script for \mbox{\isa{\isacommand{qed}}}, but may be given
7.835 - anywhere within the proof body.
7.836 -
7.837 - No facts are passed to \mbox{\isa{m}} here. Furthermore, the static
7.838 - context is that of the enclosing goal (as for actual \mbox{\isa{\isacommand{qed}}}). Thus the proof method may not refer to any assumptions
7.839 - introduced in the current body, for example.
7.840 -
7.841 - \item [\mbox{\isa{\isacommand{done}}}] completes a proof script, provided that
7.842 - the current goal state is solved completely. Note that actual
7.843 - structured proof commands (e.g.\ ``\mbox{\isa{\isacommand{{\isachardot}}}}'' or \mbox{\isa{\isacommand{sorry}}}) may be used to conclude proof scripts as well.
7.844 -
7.845 - \item [\mbox{\isa{\isacommand{defer}}}~\isa{n} and \mbox{\isa{\isacommand{prefer}}}~\isa{n}] shuffle the list of pending goals: \mbox{\isa{\isacommand{defer}}} puts off
7.846 - sub-goal \isa{n} to the end of the list (\isa{{\isachardoublequote}n\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequote}} by
7.847 - default), while \mbox{\isa{\isacommand{prefer}}} brings sub-goal \isa{n} to the
7.848 - front.
7.849 -
7.850 - \item [\mbox{\isa{\isacommand{back}}}] does back-tracking over the result
7.851 - sequence of the latest proof command. Basically, any proof command
7.852 - may return multiple results.
7.853 -
7.854 - \end{descr}
7.855 -
7.856 - Any proper Isar proof method may be used with tactic script commands
7.857 - such as \mbox{\isa{\isacommand{apply}}}. A few additional emulations of actual
7.858 - tactics are provided as well; these would be never used in actual
7.859 - structured proofs, of course.%
7.860 -\end{isamarkuptext}%
7.861 -\isamarkuptrue%
7.862 -%
7.863 -\isamarkupsubsection{Meta-linguistic features%
7.864 -}
7.865 -\isamarkuptrue%
7.866 -%
7.867 -\begin{isamarkuptext}%
7.868 -\begin{matharray}{rcl}
7.869 - \indexdef{}{command}{oops}\mbox{\isa{\isacommand{oops}}} & : & \isartrans{proof}{theory} \\
7.870 - \end{matharray}
7.871 -
7.872 - The \mbox{\isa{\isacommand{oops}}} command discontinues the current proof
7.873 - attempt, while considering the partial proof text as properly
7.874 - processed. This is conceptually quite different from ``faking''
7.875 - actual proofs via \indexref{}{command}{sorry}\mbox{\isa{\isacommand{sorry}}} (see
7.876 - \secref{sec:proof-steps}): \mbox{\isa{\isacommand{oops}}} does not observe the
7.877 - proof structure at all, but goes back right to the theory level.
7.878 - Furthermore, \mbox{\isa{\isacommand{oops}}} does not produce any result theorem
7.879 - --- there is no intended claim to be able to complete the proof
7.880 - anyhow.
7.881 -
7.882 - A typical application of \mbox{\isa{\isacommand{oops}}} is to explain Isar proofs
7.883 - \emph{within} the system itself, in conjunction with the document
7.884 - preparation tools of Isabelle described in \cite{isabelle-sys}.
7.885 - Thus partial or even wrong proof attempts can be discussed in a
7.886 - logically sound manner. Note that the Isabelle {\LaTeX} macros can
7.887 - be easily adapted to print something like ``\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}'' instead of
7.888 - the keyword ``\mbox{\isa{\isacommand{oops}}}''.
7.889 -
7.890 - \medskip The \mbox{\isa{\isacommand{oops}}} command is undo-able, unlike
7.891 - \indexref{}{command}{kill}\mbox{\isa{\isacommand{kill}}} (see \secref{sec:history}). The effect is to
7.892 - get back to the theory just before the opening of the proof.%
7.893 -\end{isamarkuptext}%
7.894 -\isamarkuptrue%
7.895 -%
7.896 \isamarkupsection{Other commands%
7.897 }
7.898 \isamarkuptrue%
8.1 --- a/doc-src/IsarRef/Thy/pure.thy Fri May 09 23:35:57 2008 +0200
8.2 +++ b/doc-src/IsarRef/Thy/pure.thy Sat May 10 00:14:00 2008 +0200
8.3 @@ -32,72 +32,6 @@
8.4
8.5 section {* Theory commands *}
8.6
8.7 -subsection {* Defining theories \label{sec:begin-thy} *}
8.8 -
8.9 -text {*
8.10 - \begin{matharray}{rcl}
8.11 - @{command_def "header"} & : & \isarkeep{toplevel} \\
8.12 - @{command_def "theory"} & : & \isartrans{toplevel}{theory} \\
8.13 - @{command_def "end"} & : & \isartrans{theory}{toplevel} \\
8.14 - \end{matharray}
8.15 -
8.16 - Isabelle/Isar theories are defined via theory, which contain both
8.17 - specifications and proofs; occasionally definitional mechanisms also
8.18 - require some explicit proof.
8.19 -
8.20 - The first ``real'' command of any theory has to be @{command
8.21 - "theory"}, which starts a new theory based on the merge of existing
8.22 - ones. Just preceding the @{command "theory"} keyword, there may be
8.23 - an optional @{command "header"} declaration, which is relevant to
8.24 - document preparation only; it acts very much like a special
8.25 - pre-theory markup command (cf.\ \secref{sec:markup-thy} and
8.26 - \secref{sec:markup-thy}). The @{command "end"} command concludes a
8.27 - theory development; it has to be the very last command of any theory
8.28 - file loaded in batch-mode.
8.29 -
8.30 - \begin{rail}
8.31 - 'header' text
8.32 - ;
8.33 - 'theory' name 'imports' (name +) uses? 'begin'
8.34 - ;
8.35 -
8.36 - uses: 'uses' ((name | parname) +);
8.37 - \end{rail}
8.38 -
8.39 - \begin{descr}
8.40 -
8.41 - \item [@{command "header"}~@{text "text"}] provides plain text
8.42 - markup just preceding the formal beginning of a theory. In actual
8.43 - document preparation the corresponding {\LaTeX} macro @{verbatim
8.44 - "\\isamarkupheader"} may be redefined to produce chapter or section
8.45 - headings. See also \secref{sec:markup-thy} and
8.46 - \secref{sec:markup-prf} for further markup commands.
8.47 -
8.48 - \item [@{command "theory"}~@{text "A \<IMPORTS> B\<^sub>1 \<dots>
8.49 - B\<^sub>n \<BEGIN>"}] starts a new theory @{text A} based on the
8.50 - merge of existing theories @{text "B\<^sub>1 \<dots> B\<^sub>n"}.
8.51 -
8.52 - Due to inclusion of several ancestors, the overall theory structure
8.53 - emerging in an Isabelle session forms a directed acyclic graph
8.54 - (DAG). Isabelle's theory loader ensures that the sources
8.55 - contributing to the development graph are always up-to-date.
8.56 - Changed files are automatically reloaded when processing theory
8.57 - headers.
8.58 -
8.59 - The optional @{keyword_def "uses"} specification declares additional
8.60 - dependencies on extra files (usually ML sources). Files will be
8.61 - loaded immediately (as ML), unless the name is put in parentheses,
8.62 - which merely documents the dependency to be resolved later in the
8.63 - text (typically via explicit @{command_ref "use"} in the body text,
8.64 - see \secref{sec:ML}).
8.65 -
8.66 - \item [@{command "end"}] concludes the current theory definition or
8.67 - context switch.
8.68 -
8.69 - \end{descr}
8.70 -*}
8.71 -
8.72 -
8.73 subsection {* Markup commands \label{sec:markup-thy} *}
8.74
8.75 text {*
8.76 @@ -674,42 +608,6 @@
8.77
8.78 section {* Proof commands *}
8.79
8.80 -text {*
8.81 - Proof commands perform transitions of Isar/VM machine
8.82 - configurations, which are block-structured, consisting of a stack of
8.83 - nodes with three main components: logical proof context, current
8.84 - facts, and open goals. Isar/VM transitions are \emph{typed}
8.85 - according to the following three different modes of operation:
8.86 -
8.87 - \begin{descr}
8.88 -
8.89 - \item [@{text "proof(prove)"}] means that a new goal has just been
8.90 - stated that is now to be \emph{proven}; the next command may refine
8.91 - it by some proof method, and enter a sub-proof to establish the
8.92 - actual result.
8.93 -
8.94 - \item [@{text "proof(state)"}] is like a nested theory mode: the
8.95 - context may be augmented by \emph{stating} additional assumptions,
8.96 - intermediate results etc.
8.97 -
8.98 - \item [@{text "proof(chain)"}] is intermediate between @{text
8.99 - "proof(state)"} and @{text "proof(prove)"}: existing facts (i.e.\
8.100 - the contents of the special ``@{fact_ref this}'' register) have been
8.101 - just picked up in order to be used when refining the goal claimed
8.102 - next.
8.103 -
8.104 - \end{descr}
8.105 -
8.106 - The proof mode indicator may be read as a verb telling the writer
8.107 - what kind of operation may be performed next. The corresponding
8.108 - typings of proof commands restricts the shape of well-formed proof
8.109 - texts to particular command sequences. So dynamic arrangements of
8.110 - commands eventually turn out as static texts of a certain structure.
8.111 - \Appref{ap:refcard} gives a simplified grammar of the overall
8.112 - (extensible) language emerging that way.
8.113 -*}
8.114 -
8.115 -
8.116 subsection {* Markup commands \label{sec:markup-prf} *}
8.117
8.118 text {*
8.119 @@ -731,808 +629,6 @@
8.120 *}
8.121
8.122
8.123 -subsection {* Context elements \label{sec:proof-context} *}
8.124 -
8.125 -text {*
8.126 - \begin{matharray}{rcl}
8.127 - @{command_def "fix"} & : & \isartrans{proof(state)}{proof(state)} \\
8.128 - @{command_def "assume"} & : & \isartrans{proof(state)}{proof(state)} \\
8.129 - @{command_def "presume"} & : & \isartrans{proof(state)}{proof(state)} \\
8.130 - @{command_def "def"} & : & \isartrans{proof(state)}{proof(state)} \\
8.131 - \end{matharray}
8.132 -
8.133 - The logical proof context consists of fixed variables and
8.134 - assumptions. The former closely correspond to Skolem constants, or
8.135 - meta-level universal quantification as provided by the Isabelle/Pure
8.136 - logical framework. Introducing some \emph{arbitrary, but fixed}
8.137 - variable via ``@{command "fix"}~@{text x}'' results in a local value
8.138 - that may be used in the subsequent proof as any other variable or
8.139 - constant. Furthermore, any result @{text "\<turnstile> \<phi>[x]"} exported from
8.140 - the context will be universally closed wrt.\ @{text x} at the
8.141 - outermost level: @{text "\<turnstile> \<And>x. \<phi>[x]"} (this is expressed in normal
8.142 - form using Isabelle's meta-variables).
8.143 -
8.144 - Similarly, introducing some assumption @{text \<chi>} has two effects.
8.145 - On the one hand, a local theorem is created that may be used as a
8.146 - fact in subsequent proof steps. On the other hand, any result
8.147 - @{text "\<chi> \<turnstile> \<phi>"} exported from the context becomes conditional wrt.\
8.148 - the assumption: @{text "\<turnstile> \<chi> \<Longrightarrow> \<phi>"}. Thus, solving an enclosing goal
8.149 - using such a result would basically introduce a new subgoal stemming
8.150 - from the assumption. How this situation is handled depends on the
8.151 - version of assumption command used: while @{command "assume"}
8.152 - insists on solving the subgoal by unification with some premise of
8.153 - the goal, @{command "presume"} leaves the subgoal unchanged in order
8.154 - to be proved later by the user.
8.155 -
8.156 - Local definitions, introduced by ``@{command "def"}~@{text "x \<equiv>
8.157 - t"}'', are achieved by combining ``@{command "fix"}~@{text x}'' with
8.158 - another version of assumption that causes any hypothetical equation
8.159 - @{text "x \<equiv> t"} to be eliminated by the reflexivity rule. Thus,
8.160 - exporting some result @{text "x \<equiv> t \<turnstile> \<phi>[x]"} yields @{text "\<turnstile>
8.161 - \<phi>[t]"}.
8.162 -
8.163 - \begin{rail}
8.164 - 'fix' (vars + 'and')
8.165 - ;
8.166 - ('assume' | 'presume') (props + 'and')
8.167 - ;
8.168 - 'def' (def + 'and')
8.169 - ;
8.170 - def: thmdecl? \\ name ('==' | equiv) term termpat?
8.171 - ;
8.172 - \end{rail}
8.173 -
8.174 - \begin{descr}
8.175 -
8.176 - \item [@{command "fix"}~@{text x}] introduces a local variable
8.177 - @{text x} that is \emph{arbitrary, but fixed.}
8.178 -
8.179 - \item [@{command "assume"}~@{text "a: \<phi>"} and @{command
8.180 - "presume"}~@{text "a: \<phi>"}] introduce a local fact @{text "\<phi> \<turnstile> \<phi>"} by
8.181 - assumption. Subsequent results applied to an enclosing goal (e.g.\
8.182 - by @{command_ref "show"}) are handled as follows: @{command
8.183 - "assume"} expects to be able to unify with existing premises in the
8.184 - goal, while @{command "presume"} leaves @{text \<phi>} as new subgoals.
8.185 -
8.186 - Several lists of assumptions may be given (separated by
8.187 - @{keyword_ref "and"}; the resulting list of current facts consists
8.188 - of all of these concatenated.
8.189 -
8.190 - \item [@{command "def"}~@{text "x \<equiv> t"}] introduces a local
8.191 - (non-polymorphic) definition. In results exported from the context,
8.192 - @{text x} is replaced by @{text t}. Basically, ``@{command
8.193 - "def"}~@{text "x \<equiv> t"}'' abbreviates ``@{command "fix"}~@{text
8.194 - x}~@{command "assume"}~@{text "x \<equiv> t"}'', with the resulting
8.195 - hypothetical equation solved by reflexivity.
8.196 -
8.197 - The default name for the definitional equation is @{text x_def}.
8.198 - Several simultaneous definitions may be given at the same time.
8.199 -
8.200 - \end{descr}
8.201 -
8.202 - The special name @{fact_ref prems} refers to all assumptions of the
8.203 - current context as a list of theorems. This feature should be used
8.204 - with great care! It is better avoided in final proof texts.
8.205 -*}
8.206 -
8.207 -
8.208 -subsection {* Facts and forward chaining *}
8.209 -
8.210 -text {*
8.211 - \begin{matharray}{rcl}
8.212 - @{command_def "note"} & : & \isartrans{proof(state)}{proof(state)} \\
8.213 - @{command_def "then"} & : & \isartrans{proof(state)}{proof(chain)} \\
8.214 - @{command_def "from"} & : & \isartrans{proof(state)}{proof(chain)} \\
8.215 - @{command_def "with"} & : & \isartrans{proof(state)}{proof(chain)} \\
8.216 - @{command_def "using"} & : & \isartrans{proof(prove)}{proof(prove)} \\
8.217 - @{command_def "unfolding"} & : & \isartrans{proof(prove)}{proof(prove)} \\
8.218 - \end{matharray}
8.219 -
8.220 - New facts are established either by assumption or proof of local
8.221 - statements. Any fact will usually be involved in further proofs,
8.222 - either as explicit arguments of proof methods, or when forward
8.223 - chaining towards the next goal via @{command "then"} (and variants);
8.224 - @{command "from"} and @{command "with"} are composite forms
8.225 - involving @{command "note"}. The @{command "using"} elements
8.226 - augments the collection of used facts \emph{after} a goal has been
8.227 - stated. Note that the special theorem name @{fact_ref this} refers
8.228 - to the most recently established facts, but only \emph{before}
8.229 - issuing a follow-up claim.
8.230 -
8.231 - \begin{rail}
8.232 - 'note' (thmdef? thmrefs + 'and')
8.233 - ;
8.234 - ('from' | 'with' | 'using' | 'unfolding') (thmrefs + 'and')
8.235 - ;
8.236 - \end{rail}
8.237 -
8.238 - \begin{descr}
8.239 -
8.240 - \item [@{command "note"}~@{text "a = b\<^sub>1 \<dots> b\<^sub>n"}]
8.241 - recalls existing facts @{text "b\<^sub>1, \<dots>, b\<^sub>n"}, binding
8.242 - the result as @{text a}. Note that attributes may be involved as
8.243 - well, both on the left and right hand sides.
8.244 -
8.245 - \item [@{command "then"}] indicates forward chaining by the current
8.246 - facts in order to establish the goal to be claimed next. The
8.247 - initial proof method invoked to refine that will be offered the
8.248 - facts to do ``anything appropriate'' (see also
8.249 - \secref{sec:proof-steps}). For example, method @{method_ref rule}
8.250 - (see \secref{sec:pure-meth-att}) would typically do an elimination
8.251 - rather than an introduction. Automatic methods usually insert the
8.252 - facts into the goal state before operation. This provides a simple
8.253 - scheme to control relevance of facts in automated proof search.
8.254 -
8.255 - \item [@{command "from"}~@{text b}] abbreviates ``@{command
8.256 - "note"}~@{text b}~@{command "then"}''; thus @{command "then"} is
8.257 - equivalent to ``@{command "from"}~@{text this}''.
8.258 -
8.259 - \item [@{command "with"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"}]
8.260 - abbreviates ``@{command "from"}~@{text "b\<^sub>1 \<dots> b\<^sub>n \<AND>
8.261 - this"}''; thus the forward chaining is from earlier facts together
8.262 - with the current ones.
8.263 -
8.264 - \item [@{command "using"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"}] augments
8.265 - the facts being currently indicated for use by a subsequent
8.266 - refinement step (such as @{command_ref "apply"} or @{command_ref
8.267 - "proof"}).
8.268 -
8.269 - \item [@{command "unfolding"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"}] is
8.270 - structurally similar to @{command "using"}, but unfolds definitional
8.271 - equations @{text "b\<^sub>1, \<dots> b\<^sub>n"} throughout the goal state
8.272 - and facts.
8.273 -
8.274 - \end{descr}
8.275 -
8.276 - Forward chaining with an empty list of theorems is the same as not
8.277 - chaining at all. Thus ``@{command "from"}~@{text nothing}'' has no
8.278 - effect apart from entering @{text "prove(chain)"} mode, since
8.279 - @{fact_ref nothing} is bound to the empty list of theorems.
8.280 -
8.281 - Basic proof methods (such as @{method_ref rule}) expect multiple
8.282 - facts to be given in their proper order, corresponding to a prefix
8.283 - of the premises of the rule involved. Note that positions may be
8.284 - easily skipped using something like @{command "from"}~@{text "_
8.285 - \<AND> a \<AND> b"}, for example. This involves the trivial rule
8.286 - @{text "PROP \<psi> \<Longrightarrow> PROP \<psi>"}, which is bound in Isabelle/Pure as
8.287 - ``@{fact_ref "_"}'' (underscore).
8.288 -
8.289 - Automated methods (such as @{method simp} or @{method auto}) just
8.290 - insert any given facts before their usual operation. Depending on
8.291 - the kind of procedure involved, the order of facts is less
8.292 - significant here.
8.293 -*}
8.294 -
8.295 -
8.296 -subsection {* Goal statements \label{sec:goals} *}
8.297 -
8.298 -text {*
8.299 - \begin{matharray}{rcl}
8.300 - @{command_def "lemma"} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
8.301 - @{command_def "theorem"} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
8.302 - @{command_def "corollary"} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
8.303 - @{command_def "have"} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
8.304 - @{command_def "show"} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
8.305 - @{command_def "hence"} & : & \isartrans{proof(state)}{proof(prove)} \\
8.306 - @{command_def "thus"} & : & \isartrans{proof(state)}{proof(prove)} \\
8.307 - @{command_def "print_statement"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
8.308 - \end{matharray}
8.309 -
8.310 - From a theory context, proof mode is entered by an initial goal
8.311 - command such as @{command "lemma"}, @{command "theorem"}, or
8.312 - @{command "corollary"}. Within a proof, new claims may be
8.313 - introduced locally as well; four variants are available here to
8.314 - indicate whether forward chaining of facts should be performed
8.315 - initially (via @{command_ref "then"}), and whether the final result
8.316 - is meant to solve some pending goal.
8.317 -
8.318 - Goals may consist of multiple statements, resulting in a list of
8.319 - facts eventually. A pending multi-goal is internally represented as
8.320 - a meta-level conjunction (printed as @{text "&&"}), which is usually
8.321 - split into the corresponding number of sub-goals prior to an initial
8.322 - method application, via @{command_ref "proof"}
8.323 - (\secref{sec:proof-steps}) or @{command_ref "apply"}
8.324 - (\secref{sec:tactic-commands}). The @{method_ref induct} method
8.325 - covered in \secref{sec:cases-induct} acts on multiple claims
8.326 - simultaneously.
8.327 -
8.328 - Claims at the theory level may be either in short or long form. A
8.329 - short goal merely consists of several simultaneous propositions
8.330 - (often just one). A long goal includes an explicit context
8.331 - specification for the subsequent conclusion, involving local
8.332 - parameters and assumptions. Here the role of each part of the
8.333 - statement is explicitly marked by separate keywords (see also
8.334 - \secref{sec:locale}); the local assumptions being introduced here
8.335 - are available as @{fact_ref assms} in the proof. Moreover, there
8.336 - are two kinds of conclusions: @{element_def "shows"} states several
8.337 - simultaneous propositions (essentially a big conjunction), while
8.338 - @{element_def "obtains"} claims several simultaneous simultaneous
8.339 - contexts of (essentially a big disjunction of eliminated parameters
8.340 - and assumptions, cf.\ \secref{sec:obtain}).
8.341 -
8.342 - \begin{rail}
8.343 - ('lemma' | 'theorem' | 'corollary') target? (goal | longgoal)
8.344 - ;
8.345 - ('have' | 'show' | 'hence' | 'thus') goal
8.346 - ;
8.347 - 'print\_statement' modes? thmrefs
8.348 - ;
8.349 -
8.350 - goal: (props + 'and')
8.351 - ;
8.352 - longgoal: thmdecl? (contextelem *) conclusion
8.353 - ;
8.354 - conclusion: 'shows' goal | 'obtains' (parname? case + '|')
8.355 - ;
8.356 - case: (vars + 'and') 'where' (props + 'and')
8.357 - ;
8.358 - \end{rail}
8.359 -
8.360 - \begin{descr}
8.361 -
8.362 - \item [@{command "lemma"}~@{text "a: \<phi>"}] enters proof mode with
8.363 - @{text \<phi>} as main goal, eventually resulting in some fact @{text "\<turnstile>
8.364 - \<phi>"} to be put back into the target context. An additional
8.365 - \railnonterm{context} specification may build up an initial proof
8.366 - context for the subsequent claim; this includes local definitions
8.367 - and syntax as well, see the definition of @{syntax contextelem} in
8.368 - \secref{sec:locale}.
8.369 -
8.370 - \item [@{command "theorem"}~@{text "a: \<phi>"} and @{command
8.371 - "corollary"}~@{text "a: \<phi>"}] are essentially the same as @{command
8.372 - "lemma"}~@{text "a: \<phi>"}, but the facts are internally marked as
8.373 - being of a different kind. This discrimination acts like a formal
8.374 - comment.
8.375 -
8.376 - \item [@{command "have"}~@{text "a: \<phi>"}] claims a local goal,
8.377 - eventually resulting in a fact within the current logical context.
8.378 - This operation is completely independent of any pending sub-goals of
8.379 - an enclosing goal statements, so @{command "have"} may be freely
8.380 - used for experimental exploration of potential results within a
8.381 - proof body.
8.382 -
8.383 - \item [@{command "show"}~@{text "a: \<phi>"}] is like @{command
8.384 - "have"}~@{text "a: \<phi>"} plus a second stage to refine some pending
8.385 - sub-goal for each one of the finished result, after having been
8.386 - exported into the corresponding context (at the head of the
8.387 - sub-proof of this @{command "show"} command).
8.388 -
8.389 - To accommodate interactive debugging, resulting rules are printed
8.390 - before being applied internally. Even more, interactive execution
8.391 - of @{command "show"} predicts potential failure and displays the
8.392 - resulting error as a warning beforehand. Watch out for the
8.393 - following message:
8.394 -
8.395 - %FIXME proper antiquitation
8.396 - \begin{ttbox}
8.397 - Problem! Local statement will fail to solve any pending goal
8.398 - \end{ttbox}
8.399 -
8.400 - \item [@{command "hence"}] abbreviates ``@{command "then"}~@{command
8.401 - "have"}'', i.e.\ claims a local goal to be proven by forward
8.402 - chaining the current facts. Note that @{command "hence"} is also
8.403 - equivalent to ``@{command "from"}~@{text this}~@{command "have"}''.
8.404 -
8.405 - \item [@{command "thus"}] abbreviates ``@{command "then"}~@{command
8.406 - "show"}''. Note that @{command "thus"} is also equivalent to
8.407 - ``@{command "from"}~@{text this}~@{command "show"}''.
8.408 -
8.409 - \item [@{command "print_statement"}~@{text a}] prints facts from the
8.410 - current theory or proof context in long statement form, according to
8.411 - the syntax for @{command "lemma"} given above.
8.412 -
8.413 - \end{descr}
8.414 -
8.415 - Any goal statement causes some term abbreviations (such as
8.416 - @{variable_ref "?thesis"}) to be bound automatically, see also
8.417 - \secref{sec:term-abbrev}. Furthermore, the local context of a
8.418 - (non-atomic) goal is provided via the @{case_ref rule_context} case.
8.419 -
8.420 - The optional case names of @{element_ref "obtains"} have a twofold
8.421 - meaning: (1) during the of this claim they refer to the the local
8.422 - context introductions, (2) the resulting rule is annotated
8.423 - accordingly to support symbolic case splits when used with the
8.424 - @{method_ref cases} method (cf. \secref{sec:cases-induct}).
8.425 -
8.426 - \medskip
8.427 -
8.428 - \begin{warn}
8.429 - Isabelle/Isar suffers theory-level goal statements to contain
8.430 - \emph{unbound schematic variables}, although this does not conform
8.431 - to the aim of human-readable proof documents! The main problem
8.432 - with schematic goals is that the actual outcome is usually hard to
8.433 - predict, depending on the behavior of the proof methods applied
8.434 - during the course of reasoning. Note that most semi-automated
8.435 - methods heavily depend on several kinds of implicit rule
8.436 - declarations within the current theory context. As this would
8.437 - also result in non-compositional checking of sub-proofs,
8.438 - \emph{local goals} are not allowed to be schematic at all.
8.439 - Nevertheless, schematic goals do have their use in Prolog-style
8.440 - interactive synthesis of proven results, usually by stepwise
8.441 - refinement via emulation of traditional Isabelle tactic scripts
8.442 - (see also \secref{sec:tactic-commands}). In any case, users
8.443 - should know what they are doing.
8.444 - \end{warn}
8.445 -*}
8.446 -
8.447 -
8.448 -subsection {* Initial and terminal proof steps \label{sec:proof-steps} *}
8.449 -
8.450 -text {*
8.451 - \begin{matharray}{rcl}
8.452 - @{command_def "proof"} & : & \isartrans{proof(prove)}{proof(state)} \\
8.453 - @{command_def "qed"} & : & \isartrans{proof(state)}{proof(state) ~|~ theory} \\
8.454 - @{command_def "by"} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
8.455 - @{command_def ".."} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
8.456 - @{command_def "."} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
8.457 - @{command_def "sorry"} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
8.458 - \end{matharray}
8.459 -
8.460 - Arbitrary goal refinement via tactics is considered harmful.
8.461 - Structured proof composition in Isar admits proof methods to be
8.462 - invoked in two places only.
8.463 -
8.464 - \begin{enumerate}
8.465 -
8.466 - \item An \emph{initial} refinement step @{command_ref
8.467 - "proof"}~@{text "m\<^sub>1"} reduces a newly stated goal to a number
8.468 - of sub-goals that are to be solved later. Facts are passed to
8.469 - @{text "m\<^sub>1"} for forward chaining, if so indicated by @{text
8.470 - "proof(chain)"} mode.
8.471 -
8.472 - \item A \emph{terminal} conclusion step @{command_ref "qed"}~@{text
8.473 - "m\<^sub>2"} is intended to solve remaining goals. No facts are
8.474 - passed to @{text "m\<^sub>2"}.
8.475 -
8.476 - \end{enumerate}
8.477 -
8.478 - The only other (proper) way to affect pending goals in a proof body
8.479 - is by @{command_ref "show"}, which involves an explicit statement of
8.480 - what is to be solved eventually. Thus we avoid the fundamental
8.481 - problem of unstructured tactic scripts that consist of numerous
8.482 - consecutive goal transformations, with invisible effects.
8.483 -
8.484 - \medskip As a general rule of thumb for good proof style, initial
8.485 - proof methods should either solve the goal completely, or constitute
8.486 - some well-understood reduction to new sub-goals. Arbitrary
8.487 - automatic proof tools that are prone leave a large number of badly
8.488 - structured sub-goals are no help in continuing the proof document in
8.489 - an intelligible manner.
8.490 -
8.491 - Unless given explicitly by the user, the default initial method is
8.492 - ``@{method_ref rule}'', which applies a single standard elimination
8.493 - or introduction rule according to the topmost symbol involved.
8.494 - There is no separate default terminal method. Any remaining goals
8.495 - are always solved by assumption in the very last step.
8.496 -
8.497 - \begin{rail}
8.498 - 'proof' method?
8.499 - ;
8.500 - 'qed' method?
8.501 - ;
8.502 - 'by' method method?
8.503 - ;
8.504 - ('.' | '..' | 'sorry')
8.505 - ;
8.506 - \end{rail}
8.507 -
8.508 - \begin{descr}
8.509 -
8.510 - \item [@{command "proof"}~@{text "m\<^sub>1"}] refines the goal by
8.511 - proof method @{text "m\<^sub>1"}; facts for forward chaining are
8.512 - passed if so indicated by @{text "proof(chain)"} mode.
8.513 -
8.514 - \item [@{command "qed"}~@{text "m\<^sub>2"}] refines any remaining
8.515 - goals by proof method @{text "m\<^sub>2"} and concludes the
8.516 - sub-proof by assumption. If the goal had been @{text "show"} (or
8.517 - @{text "thus"}), some pending sub-goal is solved as well by the rule
8.518 - resulting from the result \emph{exported} into the enclosing goal
8.519 - context. Thus @{text "qed"} may fail for two reasons: either @{text
8.520 - "m\<^sub>2"} fails, or the resulting rule does not fit to any
8.521 - pending goal\footnote{This includes any additional ``strong''
8.522 - assumptions as introduced by @{command "assume"}.} of the enclosing
8.523 - context. Debugging such a situation might involve temporarily
8.524 - changing @{command "show"} into @{command "have"}, or weakening the
8.525 - local context by replacing occurrences of @{command "assume"} by
8.526 - @{command "presume"}.
8.527 -
8.528 - \item [@{command "by"}~@{text "m\<^sub>1 m\<^sub>2"}] is a
8.529 - \emph{terminal proof}\index{proof!terminal}; it abbreviates
8.530 - @{command "proof"}~@{text "m\<^sub>1"}~@{text "qed"}~@{text
8.531 - "m\<^sub>2"}, but with backtracking across both methods. Debugging
8.532 - an unsuccessful @{command "by"}~@{text "m\<^sub>1 m\<^sub>2"}
8.533 - command can be done by expanding its definition; in many cases
8.534 - @{command "proof"}~@{text "m\<^sub>1"} (or even @{text
8.535 - "apply"}~@{text "m\<^sub>1"}) is already sufficient to see the
8.536 - problem.
8.537 -
8.538 - \item [``@{command ".."}''] is a \emph{default
8.539 - proof}\index{proof!default}; it abbreviates @{command "by"}~@{text
8.540 - "rule"}.
8.541 -
8.542 - \item [``@{command "."}''] is a \emph{trivial
8.543 - proof}\index{proof!trivial}; it abbreviates @{command "by"}~@{text
8.544 - "this"}.
8.545 -
8.546 - \item [@{command "sorry"}] is a \emph{fake proof}\index{proof!fake}
8.547 - pretending to solve the pending claim without further ado. This
8.548 - only works in interactive development, or if the @{ML
8.549 - quick_and_dirty} flag is enabled (in ML). Facts emerging from fake
8.550 - proofs are not the real thing. Internally, each theorem container
8.551 - is tainted by an oracle invocation, which is indicated as ``@{text
8.552 - "[!]"}'' in the printed result.
8.553 -
8.554 - The most important application of @{command "sorry"} is to support
8.555 - experimentation and top-down proof development.
8.556 -
8.557 - \end{descr}
8.558 -*}
8.559 -
8.560 -
8.561 -subsection {* Fundamental methods and attributes \label{sec:pure-meth-att} *}
8.562 -
8.563 -text {*
8.564 - The following proof methods and attributes refer to basic logical
8.565 - operations of Isar. Further methods and attributes are provided by
8.566 - several generic and object-logic specific tools and packages (see
8.567 - \chref{ch:gen-tools} and \chref{ch:hol}).
8.568 -
8.569 - \begin{matharray}{rcl}
8.570 - @{method_def "-"} & : & \isarmeth \\
8.571 - @{method_def "fact"} & : & \isarmeth \\
8.572 - @{method_def "assumption"} & : & \isarmeth \\
8.573 - @{method_def "this"} & : & \isarmeth \\
8.574 - @{method_def "rule"} & : & \isarmeth \\
8.575 - @{method_def "iprover"} & : & \isarmeth \\[0.5ex]
8.576 - @{attribute_def "intro"} & : & \isaratt \\
8.577 - @{attribute_def "elim"} & : & \isaratt \\
8.578 - @{attribute_def "dest"} & : & \isaratt \\
8.579 - @{attribute_def "rule"} & : & \isaratt \\[0.5ex]
8.580 - @{attribute_def "OF"} & : & \isaratt \\
8.581 - @{attribute_def "of"} & : & \isaratt \\
8.582 - @{attribute_def "where"} & : & \isaratt \\
8.583 - \end{matharray}
8.584 -
8.585 - \begin{rail}
8.586 - 'fact' thmrefs?
8.587 - ;
8.588 - 'rule' thmrefs?
8.589 - ;
8.590 - 'iprover' ('!' ?) (rulemod *)
8.591 - ;
8.592 - rulemod: ('intro' | 'elim' | 'dest') ((('!' | () | '?') nat?) | 'del') ':' thmrefs
8.593 - ;
8.594 - ('intro' | 'elim' | 'dest') ('!' | () | '?') nat?
8.595 - ;
8.596 - 'rule' 'del'
8.597 - ;
8.598 - 'OF' thmrefs
8.599 - ;
8.600 - 'of' insts ('concl' ':' insts)?
8.601 - ;
8.602 - 'where' ((name | var | typefree | typevar) '=' (type | term) * 'and')
8.603 - ;
8.604 - \end{rail}
8.605 -
8.606 - \begin{descr}
8.607 -
8.608 - \item [``@{method "-"}'' (minus)] does nothing but insert the
8.609 - forward chaining facts as premises into the goal. Note that command
8.610 - @{command_ref "proof"} without any method actually performs a single
8.611 - reduction step using the @{method_ref rule} method; thus a plain
8.612 - \emph{do-nothing} proof step would be ``@{command "proof"}~@{text
8.613 - "-"}'' rather than @{command "proof"} alone.
8.614 -
8.615 - \item [@{method "fact"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}] composes
8.616 - some fact from @{text "a\<^sub>1, \<dots>, a\<^sub>n"} (or implicitly from
8.617 - the current proof context) modulo unification of schematic type and
8.618 - term variables. The rule structure is not taken into account, i.e.\
8.619 - meta-level implication is considered atomic. This is the same
8.620 - principle underlying literal facts (cf.\ \secref{sec:syn-att}):
8.621 - ``@{command "have"}~@{text "\<phi>"}~@{command "by"}~@{text fact}'' is
8.622 - equivalent to ``@{command "note"}~@{verbatim "`"}@{text \<phi>}@{verbatim
8.623 - "`"}'' provided that @{text "\<turnstile> \<phi>"} is an instance of some known
8.624 - @{text "\<turnstile> \<phi>"} in the proof context.
8.625 -
8.626 - \item [@{method assumption}] solves some goal by a single assumption
8.627 - step. All given facts are guaranteed to participate in the
8.628 - refinement; this means there may be only 0 or 1 in the first place.
8.629 - Recall that @{command "qed"} (\secref{sec:proof-steps}) already
8.630 - concludes any remaining sub-goals by assumption, so structured
8.631 - proofs usually need not quote the @{method assumption} method at
8.632 - all.
8.633 -
8.634 - \item [@{method this}] applies all of the current facts directly as
8.635 - rules. Recall that ``@{command "."}'' (dot) abbreviates ``@{command
8.636 - "by"}~@{text this}''.
8.637 -
8.638 - \item [@{method rule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}] applies some
8.639 - rule given as argument in backward manner; facts are used to reduce
8.640 - the rule before applying it to the goal. Thus @{method rule}
8.641 - without facts is plain introduction, while with facts it becomes
8.642 - elimination.
8.643 -
8.644 - When no arguments are given, the @{method rule} method tries to pick
8.645 - appropriate rules automatically, as declared in the current context
8.646 - using the @{attribute intro}, @{attribute elim}, @{attribute dest}
8.647 - attributes (see below). This is the default behavior of @{command
8.648 - "proof"} and ``@{command ".."}'' (double-dot) steps (see
8.649 - \secref{sec:proof-steps}).
8.650 -
8.651 - \item [@{method iprover}] performs intuitionistic proof search,
8.652 - depending on specifically declared rules from the context, or given
8.653 - as explicit arguments. Chained facts are inserted into the goal
8.654 - before commencing proof search; ``@{method iprover}@{text "!"}''
8.655 - means to include the current @{fact prems} as well.
8.656 -
8.657 - Rules need to be classified as @{attribute intro}, @{attribute
8.658 - elim}, or @{attribute dest}; here the ``@{text "!"}'' indicator
8.659 - refers to ``safe'' rules, which may be applied aggressively (without
8.660 - considering back-tracking later). Rules declared with ``@{text
8.661 - "?"}'' are ignored in proof search (the single-step @{method rule}
8.662 - method still observes these). An explicit weight annotation may be
8.663 - given as well; otherwise the number of rule premises will be taken
8.664 - into account here.
8.665 -
8.666 - \item [@{attribute intro}, @{attribute elim}, and @{attribute dest}]
8.667 - declare introduction, elimination, and destruct rules, to be used
8.668 - with the @{method rule} and @{method iprover} methods. Note that
8.669 - the latter will ignore rules declared with ``@{text "?"}'', while
8.670 - ``@{text "!"}'' are used most aggressively.
8.671 -
8.672 - The classical reasoner (see \secref{sec:classical}) introduces its
8.673 - own variants of these attributes; use qualified names to access the
8.674 - present versions of Isabelle/Pure, i.e.\ @{attribute "Pure.intro"}.
8.675 -
8.676 - \item [@{attribute rule}~@{text del}] undeclares introduction,
8.677 - elimination, or destruct rules.
8.678 -
8.679 - \item [@{attribute OF}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}] applies some
8.680 - theorem to all of the given rules @{text "a\<^sub>1, \<dots>, a\<^sub>n"}
8.681 - (in parallel). This corresponds to the @{ML "op MRS"} operation in
8.682 - ML, but note the reversed order. Positions may be effectively
8.683 - skipped by including ``@{text _}'' (underscore) as argument.
8.684 -
8.685 - \item [@{attribute of}~@{text "t\<^sub>1 \<dots> t\<^sub>n"}] performs
8.686 - positional instantiation of term variables. The terms @{text
8.687 - "t\<^sub>1, \<dots>, t\<^sub>n"} are substituted for any schematic
8.688 - variables occurring in a theorem from left to right; ``@{text
8.689 - _}'' (underscore) indicates to skip a position. Arguments following
8.690 - a ``@{keyword "concl"}@{text ":"}'' specification refer to positions
8.691 - of the conclusion of a rule.
8.692 -
8.693 - \item [@{attribute "where"}~@{text "x\<^sub>1 = t\<^sub>1 \<AND> \<dots>
8.694 - x\<^sub>n = t\<^sub>n"}] performs named instantiation of schematic
8.695 - type and term variables occurring in a theorem. Schematic variables
8.696 - have to be specified on the left-hand side (e.g.\ @{text "?x1.3"}).
8.697 - The question mark may be omitted if the variable name is a plain
8.698 - identifier without index. As type instantiations are inferred from
8.699 - term instantiations, explicit type instantiations are seldom
8.700 - necessary.
8.701 -
8.702 - \end{descr}
8.703 -*}
8.704 -
8.705 -
8.706 -subsection {* Term abbreviations \label{sec:term-abbrev} *}
8.707 -
8.708 -text {*
8.709 - \begin{matharray}{rcl}
8.710 - @{command_def "let"} & : & \isartrans{proof(state)}{proof(state)} \\
8.711 - @{keyword_def "is"} & : & syntax \\
8.712 - \end{matharray}
8.713 -
8.714 - Abbreviations may be either bound by explicit @{command
8.715 - "let"}~@{text "p \<equiv> t"} statements, or by annotating assumptions or
8.716 - goal statements with a list of patterns ``@{text "(\<IS> p\<^sub>1 \<dots>
8.717 - p\<^sub>n)"}''. In both cases, higher-order matching is invoked to
8.718 - bind extra-logical term variables, which may be either named
8.719 - schematic variables of the form @{text ?x}, or nameless dummies
8.720 - ``@{variable _}'' (underscore). Note that in the @{command "let"}
8.721 - form the patterns occur on the left-hand side, while the @{keyword
8.722 - "is"} patterns are in postfix position.
8.723 -
8.724 - Polymorphism of term bindings is handled in Hindley-Milner style,
8.725 - similar to ML. Type variables referring to local assumptions or
8.726 - open goal statements are \emph{fixed}, while those of finished
8.727 - results or bound by @{command "let"} may occur in \emph{arbitrary}
8.728 - instances later. Even though actual polymorphism should be rarely
8.729 - used in practice, this mechanism is essential to achieve proper
8.730 - incremental type-inference, as the user proceeds to build up the
8.731 - Isar proof text from left to right.
8.732 -
8.733 - \medskip Term abbreviations are quite different from local
8.734 - definitions as introduced via @{command "def"} (see
8.735 - \secref{sec:proof-context}). The latter are visible within the
8.736 - logic as actual equations, while abbreviations disappear during the
8.737 - input process just after type checking. Also note that @{command
8.738 - "def"} does not support polymorphism.
8.739 -
8.740 - \begin{rail}
8.741 - 'let' ((term + 'and') '=' term + 'and')
8.742 - ;
8.743 - \end{rail}
8.744 -
8.745 - The syntax of @{keyword "is"} patterns follows \railnonterm{termpat}
8.746 - or \railnonterm{proppat} (see \secref{sec:term-decls}).
8.747 -
8.748 - \begin{descr}
8.749 -
8.750 - \item [@{command "let"}~@{text "p\<^sub>1 = t\<^sub>1 \<AND> \<dots>
8.751 - p\<^sub>n = t\<^sub>n"}] binds any text variables in patterns @{text
8.752 - "p\<^sub>1, \<dots>, p\<^sub>n"} by simultaneous higher-order matching
8.753 - against terms @{text "t\<^sub>1, \<dots>, t\<^sub>n"}.
8.754 -
8.755 - \item [@{text "(\<IS> p\<^sub>1 \<dots> p\<^sub>n)"}] resembles @{command
8.756 - "let"}, but matches @{text "p\<^sub>1, \<dots>, p\<^sub>n"} against the
8.757 - preceding statement. Also note that @{keyword "is"} is not a
8.758 - separate command, but part of others (such as @{command "assume"},
8.759 - @{command "have"} etc.).
8.760 -
8.761 - \end{descr}
8.762 -
8.763 - Some \emph{implicit} term abbreviations\index{term abbreviations}
8.764 - for goals and facts are available as well. For any open goal,
8.765 - @{variable_ref thesis} refers to its object-level statement,
8.766 - abstracted over any meta-level parameters (if present). Likewise,
8.767 - @{variable_ref this} is bound for fact statements resulting from
8.768 - assumptions or finished goals. In case @{variable this} refers to
8.769 - an object-logic statement that is an application @{text "f t"}, then
8.770 - @{text t} is bound to the special text variable ``@{variable "\<dots>"}''
8.771 - (three dots). The canonical application of this convenience are
8.772 - calculational proofs (see \secref{sec:calculation}).
8.773 -*}
8.774 -
8.775 -
8.776 -subsection {* Block structure *}
8.777 -
8.778 -text {*
8.779 - \begin{matharray}{rcl}
8.780 - @{command_def "next"} & : & \isartrans{proof(state)}{proof(state)} \\
8.781 - @{command_def "{"} & : & \isartrans{proof(state)}{proof(state)} \\
8.782 - @{command_def "}"} & : & \isartrans{proof(state)}{proof(state)} \\
8.783 - \end{matharray}
8.784 -
8.785 - While Isar is inherently block-structured, opening and closing
8.786 - blocks is mostly handled rather casually, with little explicit
8.787 - user-intervention. Any local goal statement automatically opens
8.788 - \emph{two} internal blocks, which are closed again when concluding
8.789 - the sub-proof (by @{command "qed"} etc.). Sections of different
8.790 - context within a sub-proof may be switched via @{command "next"},
8.791 - which is just a single block-close followed by block-open again.
8.792 - The effect of @{command "next"} is to reset the local proof context;
8.793 - there is no goal focus involved here!
8.794 -
8.795 - For slightly more advanced applications, there are explicit block
8.796 - parentheses as well. These typically achieve a stronger forward
8.797 - style of reasoning.
8.798 -
8.799 - \begin{descr}
8.800 -
8.801 - \item [@{command "next"}] switches to a fresh block within a
8.802 - sub-proof, resetting the local context to the initial one.
8.803 -
8.804 - \item [@{command "{"} and @{command "}"}] explicitly open and close
8.805 - blocks. Any current facts pass through ``@{command "{"}''
8.806 - unchanged, while ``@{command "}"}'' causes any result to be
8.807 - \emph{exported} into the enclosing context. Thus fixed variables
8.808 - are generalized, assumptions discharged, and local definitions
8.809 - unfolded (cf.\ \secref{sec:proof-context}). There is no difference
8.810 - of @{command "assume"} and @{command "presume"} in this mode of
8.811 - forward reasoning --- in contrast to plain backward reasoning with
8.812 - the result exported at @{command "show"} time.
8.813 -
8.814 - \end{descr}
8.815 -*}
8.816 -
8.817 -
8.818 -subsection {* Emulating tactic scripts \label{sec:tactic-commands} *}
8.819 -
8.820 -text {*
8.821 - The Isar provides separate commands to accommodate tactic-style
8.822 - proof scripts within the same system. While being outside the
8.823 - orthodox Isar proof language, these might come in handy for
8.824 - interactive exploration and debugging, or even actual tactical proof
8.825 - within new-style theories (to benefit from document preparation, for
8.826 - example). See also \secref{sec:tactics} for actual tactics, that
8.827 - have been encapsulated as proof methods. Proper proof methods may
8.828 - be used in scripts, too.
8.829 -
8.830 - \begin{matharray}{rcl}
8.831 - @{command_def "apply"}@{text "\<^sup>*"} & : & \isartrans{proof(prove)}{proof(prove)} \\
8.832 - @{command_def "apply_end"}@{text "\<^sup>*"} & : & \isartrans{proof(state)}{proof(state)} \\
8.833 - @{command_def "done"}@{text "\<^sup>*"} & : & \isartrans{proof(prove)}{proof(state)} \\
8.834 - @{command_def "defer"}@{text "\<^sup>*"} & : & \isartrans{proof}{proof} \\
8.835 - @{command_def "prefer"}@{text "\<^sup>*"} & : & \isartrans{proof}{proof} \\
8.836 - @{command_def "back"}@{text "\<^sup>*"} & : & \isartrans{proof}{proof} \\
8.837 - \end{matharray}
8.838 -
8.839 - \begin{rail}
8.840 - ( 'apply' | 'apply\_end' ) method
8.841 - ;
8.842 - 'defer' nat?
8.843 - ;
8.844 - 'prefer' nat
8.845 - ;
8.846 - \end{rail}
8.847 -
8.848 - \begin{descr}
8.849 -
8.850 - \item [@{command "apply"}~@{text m}] applies proof method @{text m}
8.851 - in initial position, but unlike @{command "proof"} it retains
8.852 - ``@{text "proof(prove)"}'' mode. Thus consecutive method
8.853 - applications may be given just as in tactic scripts.
8.854 -
8.855 - Facts are passed to @{text m} as indicated by the goal's
8.856 - forward-chain mode, and are \emph{consumed} afterwards. Thus any
8.857 - further @{command "apply"} command would always work in a purely
8.858 - backward manner.
8.859 -
8.860 - \item [@{command "apply_end"}~@{text "m"}] applies proof method
8.861 - @{text m} as if in terminal position. Basically, this simulates a
8.862 - multi-step tactic script for @{command "qed"}, but may be given
8.863 - anywhere within the proof body.
8.864 -
8.865 - No facts are passed to @{method m} here. Furthermore, the static
8.866 - context is that of the enclosing goal (as for actual @{command
8.867 - "qed"}). Thus the proof method may not refer to any assumptions
8.868 - introduced in the current body, for example.
8.869 -
8.870 - \item [@{command "done"}] completes a proof script, provided that
8.871 - the current goal state is solved completely. Note that actual
8.872 - structured proof commands (e.g.\ ``@{command "."}'' or @{command
8.873 - "sorry"}) may be used to conclude proof scripts as well.
8.874 -
8.875 - \item [@{command "defer"}~@{text n} and @{command "prefer"}~@{text
8.876 - n}] shuffle the list of pending goals: @{command "defer"} puts off
8.877 - sub-goal @{text n} to the end of the list (@{text "n = 1"} by
8.878 - default), while @{command "prefer"} brings sub-goal @{text n} to the
8.879 - front.
8.880 -
8.881 - \item [@{command "back"}] does back-tracking over the result
8.882 - sequence of the latest proof command. Basically, any proof command
8.883 - may return multiple results.
8.884 -
8.885 - \end{descr}
8.886 -
8.887 - Any proper Isar proof method may be used with tactic script commands
8.888 - such as @{command "apply"}. A few additional emulations of actual
8.889 - tactics are provided as well; these would be never used in actual
8.890 - structured proofs, of course.
8.891 -*}
8.892 -
8.893 -
8.894 -subsection {* Meta-linguistic features *}
8.895 -
8.896 -text {*
8.897 - \begin{matharray}{rcl}
8.898 - @{command_def "oops"} & : & \isartrans{proof}{theory} \\
8.899 - \end{matharray}
8.900 -
8.901 - The @{command "oops"} command discontinues the current proof
8.902 - attempt, while considering the partial proof text as properly
8.903 - processed. This is conceptually quite different from ``faking''
8.904 - actual proofs via @{command_ref "sorry"} (see
8.905 - \secref{sec:proof-steps}): @{command "oops"} does not observe the
8.906 - proof structure at all, but goes back right to the theory level.
8.907 - Furthermore, @{command "oops"} does not produce any result theorem
8.908 - --- there is no intended claim to be able to complete the proof
8.909 - anyhow.
8.910 -
8.911 - A typical application of @{command "oops"} is to explain Isar proofs
8.912 - \emph{within} the system itself, in conjunction with the document
8.913 - preparation tools of Isabelle described in \cite{isabelle-sys}.
8.914 - Thus partial or even wrong proof attempts can be discussed in a
8.915 - logically sound manner. Note that the Isabelle {\LaTeX} macros can
8.916 - be easily adapted to print something like ``@{text "\<dots>"}'' instead of
8.917 - the keyword ``@{command "oops"}''.
8.918 -
8.919 - \medskip The @{command "oops"} command is undo-able, unlike
8.920 - @{command_ref "kill"} (see \secref{sec:history}). The effect is to
8.921 - get back to the theory just before the opening of the proof.
8.922 -*}
8.923 -
8.924 -
8.925 section {* Other commands *}
8.926
8.927 subsection {* Diagnostics *}
9.1 --- a/doc-src/IsarRef/isar-ref.tex Fri May 09 23:35:57 2008 +0200
9.2 +++ b/doc-src/IsarRef/isar-ref.tex Sat May 10 00:14:00 2008 +0200
9.3 @@ -15,7 +15,18 @@
9.4
9.5 \isadroptag{theory}
9.6 \title{\includegraphics[scale=0.5]{isabelle_isar} \\[4ex] The Isabelle/Isar Reference Manual}
9.7 -\author{\emph{Markus Wenzel} \\ TU M\"unchen}
9.8 +\author{\emph{Makarius Wenzel} \\[3ex]
9.9 + With Contributions by
9.10 + Clemens Ballarin,
9.11 + Stefan Berghofer, \\
9.12 + Florian Haftmann,
9.13 + Gerwin Klein,
9.14 + Alexander Krauss, \\
9.15 + Tobias Nipkow,
9.16 + David von Oheimb,
9.17 + Larry Paulson, \\
9.18 + and Sebastian Skalberg
9.19 +}
9.20
9.21 \makeindex
9.22