--- a/src/Doc/Isar_Ref/Proof.thy Tue Oct 20 23:03:46 2015 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy Tue Oct 20 23:53:40 2015 +0200
@@ -11,17 +11,16 @@
facts, and open goals. Isar/VM transitions are typed according to
the following three different modes of operation:
- \<^descr> @{text "proof(prove)"} means that a new goal has just been
+ \<^descr> \<open>proof(prove)\<close> means that a new goal has just been
stated that is now to be \<^emph>\<open>proven\<close>; the next command may refine
it by some proof method, and enter a sub-proof to establish the
actual result.
- \<^descr> @{text "proof(state)"} is like a nested theory mode: the
+ \<^descr> \<open>proof(state)\<close> is like a nested theory mode: the
context may be augmented by \<^emph>\<open>stating\<close> additional assumptions,
intermediate results etc.
- \<^descr> @{text "proof(chain)"} is intermediate between @{text
- "proof(state)"} and @{text "proof(prove)"}: existing facts (i.e.\ the
+ \<^descr> \<open>proof(chain)\<close> is intermediate between \<open>proof(state)\<close> and \<open>proof(prove)\<close>: existing facts (i.e.\ the
contents of the special @{fact_ref this} register) have been just picked
up in order to be used when refining the goal claimed next.
@@ -46,7 +45,7 @@
text \<open>
\begin{matharray}{rcl}
- @{command_def "notepad"} & : & @{text "local_theory \<rightarrow> proof(state)"} \\
+ @{command_def "notepad"} & : & \<open>local_theory \<rightarrow> proof(state)\<close> \\
\end{matharray}
@{rail \<open>
@@ -65,9 +64,9 @@
text \<open>
\begin{matharray}{rcl}
- @{command_def "next"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
- @{command_def "{"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
- @{command_def "}"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
+ @{command_def "next"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
+ @{command_def "{"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
+ @{command_def "}"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
\end{matharray}
While Isar is inherently block-structured, opening and closing
@@ -103,7 +102,7 @@
text \<open>
\begin{matharray}{rcl}
- @{command_def "oops"} & : & @{text "proof \<rightarrow> local_theory | theory"} \\
+ @{command_def "oops"} & : & \<open>proof \<rightarrow> local_theory | theory\<close> \\
\end{matharray}
The @{command "oops"} command discontinues the current proof
@@ -121,7 +120,7 @@
preparation tools of Isabelle described in \chref{ch:document-prep}.
Thus partial or even wrong proof attempts can be discussed in a
logically sound manner. Note that the Isabelle {\LaTeX} macros can
- be easily adapted to print something like ``@{text "\<dots>"}'' instead of
+ be easily adapted to print something like ``\<open>\<dots>\<close>'' instead of
the keyword ``@{command "oops"}''.
\<close>
@@ -132,28 +131,28 @@
text \<open>
\begin{matharray}{rcl}
- @{command_def "fix"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
- @{command_def "assume"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
- @{command_def "presume"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
- @{command_def "def"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
+ @{command_def "fix"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
+ @{command_def "assume"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
+ @{command_def "presume"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
+ @{command_def "def"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
\end{matharray}
The logical proof context consists of fixed variables and
assumptions. The former closely correspond to Skolem constants, or
meta-level universal quantification as provided by the Isabelle/Pure
logical framework. Introducing some \<^emph>\<open>arbitrary, but fixed\<close>
- variable via ``@{command "fix"}~@{text x}'' results in a local value
+ variable via ``@{command "fix"}~\<open>x\<close>'' results in a local value
that may be used in the subsequent proof as any other variable or
- constant. Furthermore, any result @{text "\<turnstile> \<phi>[x]"} exported from
- the context will be universally closed wrt.\ @{text x} at the
- outermost level: @{text "\<turnstile> \<And>x. \<phi>[x]"} (this is expressed in normal
+ constant. Furthermore, any result \<open>\<turnstile> \<phi>[x]\<close> exported from
+ the context will be universally closed wrt.\ \<open>x\<close> at the
+ outermost level: \<open>\<turnstile> \<And>x. \<phi>[x]\<close> (this is expressed in normal
form using Isabelle's meta-variables).
- Similarly, introducing some assumption @{text \<chi>} has two effects.
+ Similarly, introducing some assumption \<open>\<chi>\<close> has two effects.
On the one hand, a local theorem is created that may be used as a
fact in subsequent proof steps. On the other hand, any result
- @{text "\<chi> \<turnstile> \<phi>"} exported from the context becomes conditional wrt.\
- the assumption: @{text "\<turnstile> \<chi> \<Longrightarrow> \<phi>"}. Thus, solving an enclosing goal
+ \<open>\<chi> \<turnstile> \<phi>\<close> exported from the context becomes conditional wrt.\
+ the assumption: \<open>\<turnstile> \<chi> \<Longrightarrow> \<phi>\<close>. Thus, solving an enclosing goal
using such a result would basically introduce a new subgoal stemming
from the assumption. How this situation is handled depends on the
version of assumption command used: while @{command "assume"}
@@ -161,12 +160,12 @@
the goal, @{command "presume"} leaves the subgoal unchanged in order
to be proved later by the user.
- Local definitions, introduced by ``@{command "def"}~@{text "x \<equiv>
- t"}'', are achieved by combining ``@{command "fix"}~@{text x}'' with
+ Local definitions, introduced by ``@{command "def"}~\<open>x \<equiv>
+ t\<close>'', are achieved by combining ``@{command "fix"}~\<open>x\<close>'' with
another version of assumption that causes any hypothetical equation
- @{text "x \<equiv> t"} to be eliminated by the reflexivity rule. Thus,
- exporting some result @{text "x \<equiv> t \<turnstile> \<phi>[x]"} yields @{text "\<turnstile>
- \<phi>[t]"}.
+ \<open>x \<equiv> t\<close> to be eliminated by the reflexivity rule. Thus,
+ exporting some result \<open>x \<equiv> t \<turnstile> \<phi>[x]\<close> yields \<open>\<turnstile>
+ \<phi>[t]\<close>.
@{rail \<open>
@@{command fix} @{syntax "fixes"}
@@ -179,28 +178,26 @@
@{syntax name} ('==' | '\<equiv>') @{syntax term} @{syntax term_pat}?
\<close>}
- \<^descr> @{command "fix"}~@{text x} introduces a local variable @{text
- x} that is \<^emph>\<open>arbitrary, but fixed\<close>.
+ \<^descr> @{command "fix"}~\<open>x\<close> introduces a local variable \<open>x\<close> that is \<^emph>\<open>arbitrary, but fixed\<close>.
- \<^descr> @{command "assume"}~@{text "a: \<phi>"} and @{command
- "presume"}~@{text "a: \<phi>"} introduce a local fact @{text "\<phi> \<turnstile> \<phi>"} by
+ \<^descr> @{command "assume"}~\<open>a: \<phi>\<close> and @{command
+ "presume"}~\<open>a: \<phi>\<close> introduce a local fact \<open>\<phi> \<turnstile> \<phi>\<close> by
assumption. Subsequent results applied to an enclosing goal (e.g.\
by @{command_ref "show"}) are handled as follows: @{command
"assume"} expects to be able to unify with existing premises in the
- goal, while @{command "presume"} leaves @{text \<phi>} as new subgoals.
+ goal, while @{command "presume"} leaves \<open>\<phi>\<close> as new subgoals.
Several lists of assumptions may be given (separated by
@{keyword_ref "and"}; the resulting list of current facts consists
of all of these concatenated.
- \<^descr> @{command "def"}~@{text "x \<equiv> t"} introduces a local
+ \<^descr> @{command "def"}~\<open>x \<equiv> t\<close> introduces a local
(non-polymorphic) definition. In results exported from the context,
- @{text x} is replaced by @{text t}. Basically, ``@{command
- "def"}~@{text "x \<equiv> t"}'' abbreviates ``@{command "fix"}~@{text
- x}~@{command "assume"}~@{text "x \<equiv> t"}'', with the resulting
+ \<open>x\<close> is replaced by \<open>t\<close>. Basically, ``@{command
+ "def"}~\<open>x \<equiv> t\<close>'' abbreviates ``@{command "fix"}~\<open>x\<close>~@{command "assume"}~\<open>x \<equiv> t\<close>'', with the resulting
hypothetical equation solved by reflexivity.
- The default name for the definitional equation is @{text x_def}.
+ The default name for the definitional equation is \<open>x_def\<close>.
Several simultaneous definitions may be given at the same time.
\<close>
@@ -209,16 +206,16 @@
text \<open>
\begin{matharray}{rcl}
- @{command_def "let"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
+ @{command_def "let"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
@{keyword_def "is"} & : & syntax \\
\end{matharray}
Abbreviations may be either bound by explicit @{command
- "let"}~@{text "p \<equiv> t"} statements, or by annotating assumptions or
- goal statements with a list of patterns ``@{text "(\<IS> p\<^sub>1 \<dots>
- p\<^sub>n)"}''. In both cases, higher-order matching is invoked to
+ "let"}~\<open>p \<equiv> t\<close> statements, or by annotating assumptions or
+ goal statements with a list of patterns ``\<open>(\<IS> p\<^sub>1 \<dots>
+ p\<^sub>n)\<close>''. In both cases, higher-order matching is invoked to
bind extra-logical term variables, which may be either named
- schematic variables of the form @{text ?x}, or nameless dummies
+ schematic variables of the form \<open>?x\<close>, or nameless dummies
``@{variable _}'' (underscore). Note that in the @{command "let"}
form the patterns occur on the left-hand side, while the @{keyword
"is"} patterns are in postfix position.
@@ -247,12 +244,12 @@
The syntax of @{keyword "is"} patterns follows @{syntax term_pat} or
@{syntax prop_pat} (see \secref{sec:term-decls}).
- \<^descr> @{command "let"}~@{text "p\<^sub>1 = t\<^sub>1 \<AND> \<dots> p\<^sub>n = t\<^sub>n"} binds any
- text variables in patterns @{text "p\<^sub>1, \<dots>, p\<^sub>n"} by simultaneous
- higher-order matching against terms @{text "t\<^sub>1, \<dots>, t\<^sub>n"}.
+ \<^descr> @{command "let"}~\<open>p\<^sub>1 = t\<^sub>1 \<AND> \<dots> p\<^sub>n = t\<^sub>n\<close> binds any
+ text variables in patterns \<open>p\<^sub>1, \<dots>, p\<^sub>n\<close> by simultaneous
+ higher-order matching against terms \<open>t\<^sub>1, \<dots>, t\<^sub>n\<close>.
- \<^descr> @{text "(\<IS> p\<^sub>1 \<dots> p\<^sub>n)"} resembles @{command "let"}, but
- matches @{text "p\<^sub>1, \<dots>, p\<^sub>n"} against the preceding statement. Also
+ \<^descr> \<open>(\<IS> p\<^sub>1 \<dots> p\<^sub>n)\<close> resembles @{command "let"}, but
+ matches \<open>p\<^sub>1, \<dots>, p\<^sub>n\<close> against the preceding statement. Also
note that @{keyword "is"} is not a separate command, but part of
others (such as @{command "assume"}, @{command "have"} etc.).
@@ -263,8 +260,8 @@
abstracted over any meta-level parameters (if present). Likewise,
@{variable_ref this} is bound for fact statements resulting from
assumptions or finished goals. In case @{variable this} refers to
- an object-logic statement that is an application @{text "f t"}, then
- @{text t} is bound to the special text variable ``@{variable "\<dots>"}''
+ an object-logic statement that is an application \<open>f t\<close>, then
+ \<open>t\<close> is bound to the special text variable ``@{variable "\<dots>"}''
(three dots). The canonical application of this convenience are
calculational proofs (see \secref{sec:calculation}).
\<close>
@@ -274,12 +271,12 @@
text \<open>
\begin{matharray}{rcl}
- @{command_def "note"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
- @{command_def "then"} & : & @{text "proof(state) \<rightarrow> proof(chain)"} \\
- @{command_def "from"} & : & @{text "proof(state) \<rightarrow> proof(chain)"} \\
- @{command_def "with"} & : & @{text "proof(state) \<rightarrow> proof(chain)"} \\
- @{command_def "using"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\
- @{command_def "unfolding"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\
+ @{command_def "note"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
+ @{command_def "then"} & : & \<open>proof(state) \<rightarrow> proof(chain)\<close> \\
+ @{command_def "from"} & : & \<open>proof(state) \<rightarrow> proof(chain)\<close> \\
+ @{command_def "with"} & : & \<open>proof(state) \<rightarrow> proof(chain)\<close> \\
+ @{command_def "using"} & : & \<open>proof(prove) \<rightarrow> proof(prove)\<close> \\
+ @{command_def "unfolding"} & : & \<open>proof(prove) \<rightarrow> proof(prove)\<close> \\
\end{matharray}
New facts are established either by assumption or proof of local
@@ -300,8 +297,8 @@
(@{syntax thmrefs} + @'and')
\<close>}
- \<^descr> @{command "note"}~@{text "a = b\<^sub>1 \<dots> b\<^sub>n"} recalls existing facts
- @{text "b\<^sub>1, \<dots>, b\<^sub>n"}, binding the result as @{text a}. Note that
+ \<^descr> @{command "note"}~\<open>a = b\<^sub>1 \<dots> b\<^sub>n\<close> recalls existing facts
+ \<open>b\<^sub>1, \<dots>, b\<^sub>n\<close>, binding the result as \<open>a\<close>. Note that
attributes may be involved as well, both on the left and right hand
sides.
@@ -315,34 +312,34 @@
facts into the goal state before operation. This provides a simple
scheme to control relevance of facts in automated proof search.
- \<^descr> @{command "from"}~@{text b} abbreviates ``@{command
- "note"}~@{text b}~@{command "then"}''; thus @{command "then"} is
- equivalent to ``@{command "from"}~@{text this}''.
+ \<^descr> @{command "from"}~\<open>b\<close> abbreviates ``@{command
+ "note"}~\<open>b\<close>~@{command "then"}''; thus @{command "then"} is
+ equivalent to ``@{command "from"}~\<open>this\<close>''.
- \<^descr> @{command "with"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"} abbreviates ``@{command
- "from"}~@{text "b\<^sub>1 \<dots> b\<^sub>n \<AND> this"}''; thus the forward chaining
+ \<^descr> @{command "with"}~\<open>b\<^sub>1 \<dots> b\<^sub>n\<close> abbreviates ``@{command
+ "from"}~\<open>b\<^sub>1 \<dots> b\<^sub>n \<AND> this\<close>''; thus the forward chaining
is from earlier facts together with the current ones.
- \<^descr> @{command "using"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"} augments the facts being
+ \<^descr> @{command "using"}~\<open>b\<^sub>1 \<dots> b\<^sub>n\<close> augments the facts being
currently indicated for use by a subsequent refinement step (such as
@{command_ref "apply"} or @{command_ref "proof"}).
- \<^descr> @{command "unfolding"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"} is structurally
+ \<^descr> @{command "unfolding"}~\<open>b\<^sub>1 \<dots> b\<^sub>n\<close> is structurally
similar to @{command "using"}, but unfolds definitional equations
- @{text "b\<^sub>1, \<dots> b\<^sub>n"} throughout the goal state and facts.
+ \<open>b\<^sub>1, \<dots> b\<^sub>n\<close> throughout the goal state and facts.
Forward chaining with an empty list of theorems is the same as not
- chaining at all. Thus ``@{command "from"}~@{text nothing}'' has no
- effect apart from entering @{text "prove(chain)"} mode, since
+ chaining at all. Thus ``@{command "from"}~\<open>nothing\<close>'' has no
+ effect apart from entering \<open>prove(chain)\<close> mode, since
@{fact_ref nothing} is bound to the empty list of theorems.
Basic proof methods (such as @{method_ref (Pure) rule}) expect multiple
facts to be given in their proper order, corresponding to a prefix
of the premises of the rule involved. Note that positions may be
- easily skipped using something like @{command "from"}~@{text "_
- \<AND> a \<AND> b"}, for example. This involves the trivial rule
- @{text "PROP \<psi> \<Longrightarrow> PROP \<psi>"}, which is bound in Isabelle/Pure as
+ easily skipped using something like @{command "from"}~\<open>_
+ \<AND> a \<AND> b\<close>, for example. This involves the trivial rule
+ \<open>PROP \<psi> \<Longrightarrow> PROP \<psi>\<close>, which is bound in Isabelle/Pure as
``@{fact_ref "_"}'' (underscore).
Automated methods (such as @{method simp} or @{method auto}) just
@@ -356,16 +353,16 @@
text \<open>
\begin{matharray}{rcl}
- @{command_def "lemma"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
- @{command_def "theorem"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
- @{command_def "corollary"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
- @{command_def "proposition"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
- @{command_def "schematic_goal"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
- @{command_def "have"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\
- @{command_def "show"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\
- @{command_def "hence"} & : & @{text "proof(state) \<rightarrow> proof(prove)"} \\
- @{command_def "thus"} & : & @{text "proof(state) \<rightarrow> proof(prove)"} \\
- @{command_def "print_statement"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
+ @{command_def "lemma"} & : & \<open>local_theory \<rightarrow> proof(prove)\<close> \\
+ @{command_def "theorem"} & : & \<open>local_theory \<rightarrow> proof(prove)\<close> \\
+ @{command_def "corollary"} & : & \<open>local_theory \<rightarrow> proof(prove)\<close> \\
+ @{command_def "proposition"} & : & \<open>local_theory \<rightarrow> proof(prove)\<close> \\
+ @{command_def "schematic_goal"} & : & \<open>local_theory \<rightarrow> proof(prove)\<close> \\
+ @{command_def "have"} & : & \<open>proof(state) | proof(chain) \<rightarrow> proof(prove)\<close> \\
+ @{command_def "show"} & : & \<open>proof(state) | proof(chain) \<rightarrow> proof(prove)\<close> \\
+ @{command_def "hence"} & : & \<open>proof(state) \<rightarrow> proof(prove)\<close> \\
+ @{command_def "thus"} & : & \<open>proof(state) \<rightarrow> proof(prove)\<close> \\
+ @{command_def "print_statement"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
\end{matharray}
From a theory context, proof mode is entered by an initial goal command
@@ -375,7 +372,7 @@
Goals may consist of multiple statements, resulting in a list of
facts eventually. A pending multi-goal is internally represented as
- a meta-level conjunction (@{text "&&&"}), which is usually
+ a meta-level conjunction (\<open>&&&\<close>), which is usually
split into the corresponding number of sub-goals prior to an initial
method application, via @{command_ref "proof"}
(\secref{sec:proof-steps}) or @{command_ref "apply"}
@@ -422,9 +419,9 @@
(@{syntax thmdecl}? (@{syntax prop}+) + @'and')
\<close>}
- \<^descr> @{command "lemma"}~@{text "a: \<phi>"} enters proof mode with
- @{text \<phi>} as main goal, eventually resulting in some fact @{text "\<turnstile>
- \<phi>"} to be put back into the target context. An additional @{syntax
+ \<^descr> @{command "lemma"}~\<open>a: \<phi>\<close> enters proof mode with
+ \<open>\<phi>\<close> as main goal, eventually resulting in some fact \<open>\<turnstile>
+ \<phi>\<close> to be put back into the target context. An additional @{syntax
context} specification may build up an initial proof context for the
subsequent claim; this includes local definitions and syntax as
well, see also @{syntax "includes"} in \secref{sec:bundle} and
@@ -444,15 +441,15 @@
proofs is lost, which also impacts performance, because proof
checking is forced into sequential mode.
- \<^descr> @{command "have"}~@{text "a: \<phi>"} claims a local goal,
+ \<^descr> @{command "have"}~\<open>a: \<phi>\<close> claims a local goal,
eventually resulting in a fact within the current logical context.
This operation is completely independent of any pending sub-goals of
an enclosing goal statements, so @{command "have"} may be freely
used for experimental exploration of potential results within a
proof body.
- \<^descr> @{command "show"}~@{text "a: \<phi>"} is like @{command
- "have"}~@{text "a: \<phi>"} plus a second stage to refine some pending
+ \<^descr> @{command "show"}~\<open>a: \<phi>\<close> is like @{command
+ "have"}~\<open>a: \<phi>\<close> plus a second stage to refine some pending
sub-goal for each one of the finished result, after having been
exported into the corresponding context (at the head of the
sub-proof of this @{command "show"} command).
@@ -467,13 +464,13 @@
\<^descr> @{command "hence"} abbreviates ``@{command "then"}~@{command
"have"}'', i.e.\ claims a local goal to be proven by forward
chaining the current facts. Note that @{command "hence"} is also
- equivalent to ``@{command "from"}~@{text this}~@{command "have"}''.
+ equivalent to ``@{command "from"}~\<open>this\<close>~@{command "have"}''.
\<^descr> @{command "thus"} abbreviates ``@{command "then"}~@{command
"show"}''. Note that @{command "thus"} is also equivalent to
- ``@{command "from"}~@{text this}~@{command "show"}''.
+ ``@{command "from"}~\<open>this\<close>~@{command "show"}''.
- \<^descr> @{command "print_statement"}~@{text a} prints facts from the
+ \<^descr> @{command "print_statement"}~\<open>a\<close> prints facts from the
current theory or proof context in long statement form, according to
the syntax for @{command "lemma"} given above.
@@ -493,19 +490,19 @@
text \<open>
\begin{matharray}{rcl}
- @{command_def "also"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
- @{command_def "finally"} & : & @{text "proof(state) \<rightarrow> proof(chain)"} \\
- @{command_def "moreover"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
- @{command_def "ultimately"} & : & @{text "proof(state) \<rightarrow> proof(chain)"} \\
- @{command_def "print_trans_rules"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
- @{attribute trans} & : & @{text attribute} \\
- @{attribute sym} & : & @{text attribute} \\
- @{attribute symmetric} & : & @{text attribute} \\
+ @{command_def "also"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
+ @{command_def "finally"} & : & \<open>proof(state) \<rightarrow> proof(chain)\<close> \\
+ @{command_def "moreover"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
+ @{command_def "ultimately"} & : & \<open>proof(state) \<rightarrow> proof(chain)\<close> \\
+ @{command_def "print_trans_rules"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
+ @{attribute trans} & : & \<open>attribute\<close> \\
+ @{attribute sym} & : & \<open>attribute\<close> \\
+ @{attribute symmetric} & : & \<open>attribute\<close> \\
\end{matharray}
Calculational proof is forward reasoning with implicit application
- of transitivity rules (such those of @{text "="}, @{text "\<le>"},
- @{text "<"}). Isabelle/Isar maintains an auxiliary fact register
+ of transitivity rules (such those of \<open>=\<close>, \<open>\<le>\<close>,
+ \<open><\<close>). Isabelle/Isar maintains an auxiliary fact register
@{fact_ref calculation} for accumulating results obtained by
transitivity composed with the current result. Command @{command
"also"} updates @{fact calculation} involving @{fact this}, while
@@ -519,7 +516,7 @@
but only collect further results in @{fact calculation} without
applying any rules yet.
- Also note that the implicit term abbreviation ``@{text "\<dots>"}'' has
+ Also note that the implicit term abbreviation ``\<open>\<dots>\<close>'' has
its canonical application with calculational proofs. It refers to
the argument of the preceding statement. (The argument of a curried
infix expression happens to be its right-hand side.)
@@ -537,11 +534,11 @@
handling of block-structure.}
\begin{matharray}{rcl}
- @{command "also"}@{text "\<^sub>0"} & \equiv & @{command "note"}~@{text "calculation = this"} \\
- @{command "also"}@{text "\<^sub>n+1"} & \equiv & @{command "note"}~@{text "calculation = trans [OF calculation this]"} \\[0.5ex]
- @{command "finally"} & \equiv & @{command "also"}~@{command "from"}~@{text calculation} \\[0.5ex]
- @{command "moreover"} & \equiv & @{command "note"}~@{text "calculation = calculation this"} \\
- @{command "ultimately"} & \equiv & @{command "moreover"}~@{command "from"}~@{text calculation} \\
+ @{command "also"}\<open>\<^sub>0\<close> & \equiv & @{command "note"}~\<open>calculation = this\<close> \\
+ @{command "also"}\<open>\<^sub>n+1\<close> & \equiv & @{command "note"}~\<open>calculation = trans [OF calculation this]\<close> \\[0.5ex]
+ @{command "finally"} & \equiv & @{command "also"}~@{command "from"}~\<open>calculation\<close> \\[0.5ex]
+ @{command "moreover"} & \equiv & @{command "note"}~\<open>calculation = calculation this\<close> \\
+ @{command "ultimately"} & \equiv & @{command "moreover"}~@{command "from"}~\<open>calculation\<close> \\
\end{matharray}
@{rail \<open>
@@ -550,7 +547,7 @@
@@{attribute trans} (() | 'add' | 'del')
\<close>}
- \<^descr> @{command "also"}~@{text "(a\<^sub>1 \<dots> a\<^sub>n)"} maintains the auxiliary
+ \<^descr> @{command "also"}~\<open>(a\<^sub>1 \<dots> a\<^sub>n)\<close> maintains the auxiliary
@{fact calculation} register as follows. The first occurrence of
@{command "also"} in some calculational thread initializes @{fact
calculation} by @{fact this}. Any subsequent @{command "also"} on
@@ -560,15 +557,15 @@
current context, unless alternative rules are given as explicit
arguments.
- \<^descr> @{command "finally"}~@{text "(a\<^sub>1 \<dots> a\<^sub>n)"} maintaining @{fact
+ \<^descr> @{command "finally"}~\<open>(a\<^sub>1 \<dots> a\<^sub>n)\<close> maintaining @{fact
calculation} in the same way as @{command "also"}, and concludes the
current calculational thread. The final result is exhibited as fact
for forward chaining towards the next goal. Basically, @{command
"finally"} just abbreviates @{command "also"}~@{command
"from"}~@{fact calculation}. Typical idioms for concluding
calculational proofs are ``@{command "finally"}~@{command
- "show"}~@{text ?thesis}~@{command "."}'' and ``@{command
- "finally"}~@{command "have"}~@{text \<phi>}~@{command "."}''.
+ "show"}~\<open>?thesis\<close>~@{command "."}'' and ``@{command
+ "finally"}~@{command "have"}~\<open>\<phi>\<close>~@{command "."}''.
\<^descr> @{command "moreover"} and @{command "ultimately"} are
analogous to @{command "also"} and @{command "finally"}, but collect
@@ -583,17 +580,16 @@
\<^descr> @{attribute trans} declares theorems as transitivity rules.
\<^descr> @{attribute sym} declares symmetry rules, as well as
- @{attribute "Pure.elim"}@{text "?"} rules.
+ @{attribute "Pure.elim"}\<open>?\<close> rules.
\<^descr> @{attribute symmetric} resolves a theorem with some rule
declared as @{attribute sym} in the current context. For example,
- ``@{command "assume"}~@{text "[symmetric]: x = y"}'' produces a
+ ``@{command "assume"}~\<open>[symmetric]: x = y\<close>'' produces a
swapped fact derived from that assumption.
In structured proof texts it is often more appropriate to use an
explicit single-step elimination proof, such as ``@{command
- "assume"}~@{text "x = y"}~@{command "then"}~@{command "have"}~@{text
- "y = x"}~@{command ".."}''.
+ "assume"}~\<open>x = y\<close>~@{command "then"}~@{command "have"}~\<open>y = x\<close>~@{command ".."}''.
\<close>
@@ -605,8 +601,8 @@
methods via ``@{verbatim ","}'' (sequential composition), ``@{verbatim
";"}'' (structural composition), ``@{verbatim "|"}'' (alternative
choices), ``@{verbatim "?"}'' (try), ``@{verbatim "+"}'' (repeat at least
- once), ``@{verbatim "["}@{text n}@{verbatim "]"}'' (restriction to first
- @{text n} subgoals). In practice, proof methods are usually just a comma
+ once), ``@{verbatim "["}\<open>n\<close>@{verbatim "]"}'' (restriction to first
+ \<open>n\<close> subgoals). In practice, proof methods are usually just a comma
separated list of @{syntax nameref}~@{syntax args} specifications. Note
that parentheses may be dropped for single method specifications (with no
arguments). The syntactic precedence of method combinators is @{verbatim
@@ -631,26 +627,24 @@
elsewhere. Thus a proof method has no other chance than to operate on the
subgoals that are presently exposed.
- Structural composition ``@{text m\<^sub>1}@{verbatim ";"}~@{text m\<^sub>2}'' means
- that method @{text m\<^sub>1} is applied with restriction to the first subgoal,
- then @{text m\<^sub>2} is applied consecutively with restriction to each subgoal
- that has newly emerged due to @{text m\<^sub>1}. This is analogous to the tactic
+ Structural composition ``\<open>m\<^sub>1\<close>@{verbatim ";"}~\<open>m\<^sub>2\<close>'' means
+ that method \<open>m\<^sub>1\<close> is applied with restriction to the first subgoal,
+ then \<open>m\<^sub>2\<close> is applied consecutively with restriction to each subgoal
+ that has newly emerged due to \<open>m\<^sub>1\<close>. This is analogous to the tactic
combinator @{ML_op THEN_ALL_NEW} in Isabelle/ML, see also @{cite
- "isabelle-implementation"}. For example, @{text "(rule r; blast)"} applies
- rule @{text "r"} and then solves all new subgoals by @{text blast}.
+ "isabelle-implementation"}. For example, \<open>(rule r; blast)\<close> applies
+ rule \<open>r\<close> and then solves all new subgoals by \<open>blast\<close>.
- Moreover, the explicit goal restriction operator ``@{text "[n]"}'' exposes
- only the first @{text n} subgoals (which need to exist), with default
- @{text "n = 1"}. For example, the method expression ``@{text
- "simp_all[3]"}'' simplifies the first three subgoals, while ``@{text
- "(rule r, simp_all)[]"}'' simplifies all new goals that emerge from
- applying rule @{text "r"} to the originally first one.
+ Moreover, the explicit goal restriction operator ``\<open>[n]\<close>'' exposes
+ only the first \<open>n\<close> subgoals (which need to exist), with default
+ \<open>n = 1\<close>. For example, the method expression ``\<open>simp_all[3]\<close>'' simplifies the first three subgoals, while ``\<open>(rule r, simp_all)[]\<close>'' simplifies all new goals that emerge from
+ applying rule \<open>r\<close> to the originally first one.
\<^medskip>
Improper methods, notably tactic emulations, offer low-level goal
addressing as explicit argument to the individual tactic being involved.
- Here ``@{text "[!]"}'' refers to all goals, and ``@{text "[n-]"}'' to all
- goals starting from @{text "n"}.
+ Here ``\<open>[!]\<close>'' refers to all goals, and ``\<open>[n-]\<close>'' to all
+ goals starting from \<open>n\<close>.
@{rail \<open>
@{syntax_def goal_spec}:
@@ -663,13 +657,13 @@
text \<open>
\begin{matharray}{rcl}
- @{command_def "proof"} & : & @{text "proof(prove) \<rightarrow> proof(state)"} \\
- @{command_def "qed"} & : & @{text "proof(state) \<rightarrow> proof(state) | local_theory | theory"} \\
- @{command_def "by"} & : & @{text "proof(prove) \<rightarrow> proof(state) | local_theory | theory"} \\
- @{command_def ".."} & : & @{text "proof(prove) \<rightarrow> proof(state) | local_theory | theory"} \\
- @{command_def "."} & : & @{text "proof(prove) \<rightarrow> proof(state) | local_theory | theory"} \\
- @{command_def "sorry"} & : & @{text "proof(prove) \<rightarrow> proof(state) | local_theory | theory"} \\
- @{method_def standard} & : & @{text method} \\
+ @{command_def "proof"} & : & \<open>proof(prove) \<rightarrow> proof(state)\<close> \\
+ @{command_def "qed"} & : & \<open>proof(state) \<rightarrow> proof(state) | local_theory | theory\<close> \\
+ @{command_def "by"} & : & \<open>proof(prove) \<rightarrow> proof(state) | local_theory | theory\<close> \\
+ @{command_def ".."} & : & \<open>proof(prove) \<rightarrow> proof(state) | local_theory | theory\<close> \\
+ @{command_def "."} & : & \<open>proof(prove) \<rightarrow> proof(state) | local_theory | theory\<close> \\
+ @{command_def "sorry"} & : & \<open>proof(prove) \<rightarrow> proof(state) | local_theory | theory\<close> \\
+ @{method_def standard} & : & \<open>method\<close> \\
\end{matharray}
Arbitrary goal refinement via tactics is considered harmful.
@@ -677,14 +671,12 @@
invoked in two places only.
\<^enum> An \<^emph>\<open>initial\<close> refinement step @{command_ref
- "proof"}~@{text "m\<^sub>1"} reduces a newly stated goal to a number
+ "proof"}~\<open>m\<^sub>1\<close> reduces a newly stated goal to a number
of sub-goals that are to be solved later. Facts are passed to
- @{text "m\<^sub>1"} for forward chaining, if so indicated by @{text
- "proof(chain)"} mode.
+ \<open>m\<^sub>1\<close> for forward chaining, if so indicated by \<open>proof(chain)\<close> mode.
- \<^enum> A \<^emph>\<open>terminal\<close> conclusion step @{command_ref "qed"}~@{text
- "m\<^sub>2"} is intended to solve remaining goals. No facts are
- passed to @{text "m\<^sub>2"}.
+ \<^enum> A \<^emph>\<open>terminal\<close> conclusion step @{command_ref "qed"}~\<open>m\<^sub>2\<close> is intended to solve remaining goals. No facts are
+ passed to \<open>m\<^sub>2\<close>.
The only other (proper) way to affect pending goals in a proof body
@@ -718,16 +710,15 @@
(@@{command "."} | @@{command ".."} | @@{command sorry})
\<close>}
- \<^descr> @{command "proof"}~@{text "m\<^sub>1"} refines the goal by proof
- method @{text "m\<^sub>1"}; facts for forward chaining are passed if so
- indicated by @{text "proof(chain)"} mode.
+ \<^descr> @{command "proof"}~\<open>m\<^sub>1\<close> refines the goal by proof
+ method \<open>m\<^sub>1\<close>; facts for forward chaining are passed if so
+ indicated by \<open>proof(chain)\<close> mode.
- \<^descr> @{command "qed"}~@{text "m\<^sub>2"} refines any remaining goals by
- proof method @{text "m\<^sub>2"} and concludes the sub-proof by assumption.
- If the goal had been @{text "show"} (or @{text "thus"}), some
+ \<^descr> @{command "qed"}~\<open>m\<^sub>2\<close> refines any remaining goals by
+ proof method \<open>m\<^sub>2\<close> and concludes the sub-proof by assumption.
+ If the goal had been \<open>show\<close> (or \<open>thus\<close>), some
pending sub-goal is solved as well by the rule resulting from the
- result \<^emph>\<open>exported\<close> into the enclosing goal context. Thus @{text
- "qed"} may fail for two reasons: either @{text "m\<^sub>2"} fails, or the
+ result \<^emph>\<open>exported\<close> into the enclosing goal context. Thus \<open>qed\<close> may fail for two reasons: either \<open>m\<^sub>2\<close> fails, or the
resulting rule does not fit to any pending goal\footnote{This
includes any additional ``strong'' assumptions as introduced by
@{command "assume"}.} of the enclosing context. Debugging such a
@@ -735,22 +726,20 @@
@{command "have"}, or weakening the local context by replacing
occurrences of @{command "assume"} by @{command "presume"}.
- \<^descr> @{command "by"}~@{text "m\<^sub>1 m\<^sub>2"} is a \<^emph>\<open>terminal
+ \<^descr> @{command "by"}~\<open>m\<^sub>1 m\<^sub>2\<close> is a \<^emph>\<open>terminal
proof\<close>\index{proof!terminal}; it abbreviates @{command
- "proof"}~@{text "m\<^sub>1"}~@{command "qed"}~@{text "m\<^sub>2"}, but with
+ "proof"}~\<open>m\<^sub>1\<close>~@{command "qed"}~\<open>m\<^sub>2\<close>, but with
backtracking across both methods. Debugging an unsuccessful
- @{command "by"}~@{text "m\<^sub>1 m\<^sub>2"} command can be done by expanding its
- definition; in many cases @{command "proof"}~@{text "m\<^sub>1"} (or even
- @{text "apply"}~@{text "m\<^sub>1"}) is already sufficient to see the
+ @{command "by"}~\<open>m\<^sub>1 m\<^sub>2\<close> command can be done by expanding its
+ definition; in many cases @{command "proof"}~\<open>m\<^sub>1\<close> (or even
+ \<open>apply\<close>~\<open>m\<^sub>1\<close>) is already sufficient to see the
problem.
\<^descr> ``@{command ".."}'' is a \<^emph>\<open>standard
- proof\<close>\index{proof!standard}; it abbreviates @{command "by"}~@{text
- "standard"}.
+ proof\<close>\index{proof!standard}; it abbreviates @{command "by"}~\<open>standard\<close>.
\<^descr> ``@{command "."}'' is a \<^emph>\<open>trivial
- proof\<close>\index{proof!trivial}; it abbreviates @{command "by"}~@{text
- "this"}.
+ proof\<close>\index{proof!trivial}; it abbreviates @{command "by"}~\<open>this\<close>.
\<^descr> @{command "sorry"} is a \<^emph>\<open>fake proof\<close>\index{proof!fake}
pretending to solve the pending claim without further ado. This
@@ -787,20 +776,20 @@
\chref{ch:gen-tools} and \partref{part:hol}).
\begin{matharray}{rcl}
- @{command_def "print_rules"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\[0.5ex]
- @{method_def "-"} & : & @{text method} \\
- @{method_def "goal_cases"} & : & @{text method} \\
- @{method_def "fact"} & : & @{text method} \\
- @{method_def "assumption"} & : & @{text method} \\
- @{method_def "this"} & : & @{text method} \\
- @{method_def (Pure) "rule"} & : & @{text method} \\
- @{attribute_def (Pure) "intro"} & : & @{text attribute} \\
- @{attribute_def (Pure) "elim"} & : & @{text attribute} \\
- @{attribute_def (Pure) "dest"} & : & @{text attribute} \\
- @{attribute_def (Pure) "rule"} & : & @{text attribute} \\[0.5ex]
- @{attribute_def "OF"} & : & @{text attribute} \\
- @{attribute_def "of"} & : & @{text attribute} \\
- @{attribute_def "where"} & : & @{text attribute} \\
+ @{command_def "print_rules"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\[0.5ex]
+ @{method_def "-"} & : & \<open>method\<close> \\
+ @{method_def "goal_cases"} & : & \<open>method\<close> \\
+ @{method_def "fact"} & : & \<open>method\<close> \\
+ @{method_def "assumption"} & : & \<open>method\<close> \\
+ @{method_def "this"} & : & \<open>method\<close> \\
+ @{method_def (Pure) "rule"} & : & \<open>method\<close> \\
+ @{attribute_def (Pure) "intro"} & : & \<open>attribute\<close> \\
+ @{attribute_def (Pure) "elim"} & : & \<open>attribute\<close> \\
+ @{attribute_def (Pure) "dest"} & : & \<open>attribute\<close> \\
+ @{attribute_def (Pure) "rule"} & : & \<open>attribute\<close> \\[0.5ex]
+ @{attribute_def "OF"} & : & \<open>attribute\<close> \\
+ @{attribute_def "of"} & : & \<open>attribute\<close> \\
+ @{attribute_def "where"} & : & \<open>attribute\<close> \\
\end{matharray}
@{rail \<open>
@@ -839,9 +828,9 @@
Note that command @{command_ref "proof"} without any method actually
performs a single reduction step using the @{method_ref (Pure) rule}
method; thus a plain \<^emph>\<open>do-nothing\<close> proof step would be ``@{command
- "proof"}~@{text "-"}'' rather than @{command "proof"} alone.
+ "proof"}~\<open>-\<close>'' rather than @{command "proof"} alone.
- \<^descr> @{method "goal_cases"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} turns the current subgoals
+ \<^descr> @{method "goal_cases"}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> turns the current subgoals
into cases within the context (see also \secref{sec:cases-induct}). The
specified case names are used if present; otherwise cases are numbered
starting from 1.
@@ -851,15 +840,14 @@
premises, and @{command let} variable @{variable_ref ?case} refer to the
conclusion.
- \<^descr> @{method "fact"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} composes some fact from
- @{text "a\<^sub>1, \<dots>, a\<^sub>n"} (or implicitly from the current proof context)
+ \<^descr> @{method "fact"}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> composes some fact from
+ \<open>a\<^sub>1, \<dots>, a\<^sub>n\<close> (or implicitly from the current proof context)
modulo unification of schematic type and term variables. The rule
structure is not taken into account, i.e.\ meta-level implication is
considered atomic. This is the same principle underlying literal
- facts (cf.\ \secref{sec:syn-att}): ``@{command "have"}~@{text
- "\<phi>"}~@{command "by"}~@{text fact}'' is equivalent to ``@{command
- "note"}~@{verbatim "`"}@{text \<phi>}@{verbatim "`"}'' provided that
- @{text "\<turnstile> \<phi>"} is an instance of some known @{text "\<turnstile> \<phi>"} in the
+ facts (cf.\ \secref{sec:syn-att}): ``@{command "have"}~\<open>\<phi>\<close>~@{command "by"}~\<open>fact\<close>'' is equivalent to ``@{command
+ "note"}~@{verbatim "`"}\<open>\<phi>\<close>@{verbatim "`"}'' provided that
+ \<open>\<turnstile> \<phi>\<close> is an instance of some known \<open>\<turnstile> \<phi>\<close> in the
proof context.
\<^descr> @{method assumption} solves some goal by a single assumption
@@ -872,9 +860,9 @@
\<^descr> @{method this} applies all of the current facts directly as
rules. Recall that ``@{command "."}'' (dot) abbreviates ``@{command
- "by"}~@{text this}''.
+ "by"}~\<open>this\<close>''.
- \<^descr> @{method (Pure) rule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} applies some rule given as
+ \<^descr> @{method (Pure) rule}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> applies some rule given as
argument in backward manner; facts are used to reduce the rule
before applying it to the goal. Thus @{method (Pure) rule} without facts
is plain introduction, while with facts it becomes elimination.
@@ -890,48 +878,48 @@
@{attribute (Pure) dest} declare introduction, elimination, and
destruct rules, to be used with method @{method (Pure) rule}, and similar
tools. Note that the latter will ignore rules declared with
- ``@{text "?"}'', while ``@{text "!"}'' are used most aggressively.
+ ``\<open>?\<close>'', while ``\<open>!\<close>'' are used most aggressively.
The classical reasoner (see \secref{sec:classical}) introduces its
own variants of these attributes; use qualified names to access the
present versions of Isabelle/Pure, i.e.\ @{attribute (Pure)
"Pure.intro"}.
- \<^descr> @{attribute (Pure) rule}~@{text del} undeclares introduction,
+ \<^descr> @{attribute (Pure) rule}~\<open>del\<close> undeclares introduction,
elimination, or destruct rules.
- \<^descr> @{attribute OF}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} applies some theorem to all
- of the given rules @{text "a\<^sub>1, \<dots>, a\<^sub>n"} in canonical right-to-left
- order, which means that premises stemming from the @{text "a\<^sub>i"}
+ \<^descr> @{attribute OF}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> applies some theorem to all
+ of the given rules \<open>a\<^sub>1, \<dots>, a\<^sub>n\<close> in canonical right-to-left
+ order, which means that premises stemming from the \<open>a\<^sub>i\<close>
emerge in parallel in the result, without interfering with each
- other. In many practical situations, the @{text "a\<^sub>i"} do not have
- premises themselves, so @{text "rule [OF a\<^sub>1 \<dots> a\<^sub>n]"} can be actually
+ other. In many practical situations, the \<open>a\<^sub>i\<close> do not have
+ premises themselves, so \<open>rule [OF a\<^sub>1 \<dots> a\<^sub>n]\<close> can be actually
read as functional application (modulo unification).
- Argument positions may be effectively skipped by using ``@{text _}''
+ Argument positions may be effectively skipped by using ``\<open>_\<close>''
(underscore), which refers to the propositional identity rule in the
Pure theory.
- \<^descr> @{attribute of}~@{text "t\<^sub>1 \<dots> t\<^sub>n"} performs positional
- instantiation of term variables. The terms @{text "t\<^sub>1, \<dots>, t\<^sub>n"} are
+ \<^descr> @{attribute of}~\<open>t\<^sub>1 \<dots> t\<^sub>n\<close> performs positional
+ instantiation of term variables. The terms \<open>t\<^sub>1, \<dots>, t\<^sub>n\<close> are
substituted for any schematic variables occurring in a theorem from
- left to right; ``@{text _}'' (underscore) indicates to skip a
- position. Arguments following a ``@{text "concl:"}'' specification
+ left to right; ``\<open>_\<close>'' (underscore) indicates to skip a
+ position. Arguments following a ``\<open>concl:\<close>'' specification
refer to positions of the conclusion of a rule.
- An optional context of local variables @{text "\<FOR> x\<^sub>1 \<dots> x\<^sub>m"} may
+ An optional context of local variables \<open>\<FOR> x\<^sub>1 \<dots> x\<^sub>m\<close> may
be specified: the instantiated theorem is exported, and these
variables become schematic (usually with some shifting of indices).
- \<^descr> @{attribute "where"}~@{text "x\<^sub>1 = t\<^sub>1 \<AND> \<dots> x\<^sub>n = t\<^sub>n"}
+ \<^descr> @{attribute "where"}~\<open>x\<^sub>1 = t\<^sub>1 \<AND> \<dots> x\<^sub>n = t\<^sub>n\<close>
performs named instantiation of schematic type and term variables
occurring in a theorem. Schematic variables have to be specified on
- the left-hand side (e.g.\ @{text "?x1.3"}). The question mark may
+ the left-hand side (e.g.\ \<open>?x1.3\<close>). The question mark may
be omitted if the variable name is a plain identifier without index.
As type instantiations are inferred from term instantiations,
explicit type instantiations are seldom necessary.
- An optional context of local variables @{text "\<FOR> x\<^sub>1 \<dots> x\<^sub>m"} may
+ An optional context of local variables \<open>\<FOR> x\<^sub>1 \<dots> x\<^sub>m\<close> may
be specified as for @{attribute "of"} above.
\<close>
@@ -940,16 +928,15 @@
text \<open>
\begin{matharray}{rcl}
- @{command_def "method_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
+ @{command_def "method_setup"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
\end{matharray}
@{rail \<open>
@@{command method_setup} @{syntax name} '=' @{syntax text} @{syntax text}?
\<close>}
- \<^descr> @{command "method_setup"}~@{text "name = text description"}
- defines a proof method in the current context. The given @{text
- "text"} has to be an ML expression of type
+ \<^descr> @{command "method_setup"}~\<open>name = text description\<close>
+ defines a proof method in the current context. The given \<open>text\<close> has to be an ML expression of type
@{ML_type "(Proof.context -> Proof.method) context_parser"}, cf.\
basic parsers defined in structure @{ML_structure Args} and @{ML_structure
Attrib}. There are also combinators like @{ML METHOD} and @{ML
@@ -983,12 +970,12 @@
text \<open>
\begin{matharray}{rcl}
- @{command_def "case"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
- @{command_def "print_cases"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
- @{attribute_def case_names} & : & @{text attribute} \\
- @{attribute_def case_conclusion} & : & @{text attribute} \\
- @{attribute_def params} & : & @{text attribute} \\
- @{attribute_def consumes} & : & @{text attribute} \\
+ @{command_def "case"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
+ @{command_def "print_cases"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
+ @{attribute_def case_names} & : & \<open>attribute\<close> \\
+ @{attribute_def case_conclusion} & : & \<open>attribute\<close> \\
+ @{attribute_def params} & : & \<open>attribute\<close> \\
+ @{attribute_def consumes} & : & \<open>attribute\<close> \\
\end{matharray}
The puristic way to build up Isar proof contexts is by explicit
@@ -1000,27 +987,26 @@
The @{command "case"} command provides a shorthand to refer to a
local context symbolically: certain proof methods provide an
- environment of named ``cases'' of the form @{text "c: x\<^sub>1, \<dots>,
- x\<^sub>m, \<phi>\<^sub>1, \<dots>, \<phi>\<^sub>n"}; the effect of ``@{command
- "case"}~@{text c}'' is then equivalent to ``@{command "fix"}~@{text
- "x\<^sub>1 \<dots> x\<^sub>m"}~@{command "assume"}~@{text "c: \<phi>\<^sub>1 \<dots>
- \<phi>\<^sub>n"}''. Term bindings may be covered as well, notably
+ environment of named ``cases'' of the form \<open>c: x\<^sub>1, \<dots>,
+ x\<^sub>m, \<phi>\<^sub>1, \<dots>, \<phi>\<^sub>n\<close>; the effect of ``@{command
+ "case"}~\<open>c\<close>'' is then equivalent to ``@{command "fix"}~\<open>x\<^sub>1 \<dots> x\<^sub>m\<close>~@{command "assume"}~\<open>c: \<phi>\<^sub>1 \<dots>
+ \<phi>\<^sub>n\<close>''. Term bindings may be covered as well, notably
@{variable ?case} for the main conclusion.
- By default, the ``terminology'' @{text "x\<^sub>1, \<dots>, x\<^sub>m"} of
+ By default, the ``terminology'' \<open>x\<^sub>1, \<dots>, x\<^sub>m\<close> of
a case value is marked as hidden, i.e.\ there is no way to refer to
such parameters in the subsequent proof text. After all, original
rule parameters stem from somewhere outside of the current proof
- text. By using the explicit form ``@{command "case"}~@{text "(c
- y\<^sub>1 \<dots> y\<^sub>m)"}'' instead, the proof author is able to
+ text. By using the explicit form ``@{command "case"}~\<open>(c
+ y\<^sub>1 \<dots> y\<^sub>m)\<close>'' instead, the proof author is able to
chose local names that fit nicely into the current context.
\<^medskip>
It is important to note that proper use of @{command
"case"} does not provide means to peek at the current goal state,
which is not directly observable in Isar! Nonetheless, goal
- refinement commands do provide named cases @{text "goal\<^sub>i"}
- for each subgoal @{text "i = 1, \<dots>, n"} of the resulting goal state.
+ refinement commands do provide named cases \<open>goal\<^sub>i\<close>
+ for each subgoal \<open>i = 1, \<dots>, n\<close> of the resulting goal state.
Using this extra feature requires great care, because some bits of
the internal tactical machinery intrude the proof text. In
particular, parameter names stemming from the left-over of automated
@@ -1051,57 +1037,56 @@
@@{attribute consumes} @{syntax int}?
\<close>}
- \<^descr> @{command "case"}~@{text "a: (c x\<^sub>1 \<dots> x\<^sub>m)"} invokes a named local
- context @{text "c: x\<^sub>1, \<dots>, x\<^sub>m, \<phi>\<^sub>1, \<dots>, \<phi>\<^sub>m"}, as provided by an
+ \<^descr> @{command "case"}~\<open>a: (c x\<^sub>1 \<dots> x\<^sub>m)\<close> invokes a named local
+ context \<open>c: x\<^sub>1, \<dots>, x\<^sub>m, \<phi>\<^sub>1, \<dots>, \<phi>\<^sub>m\<close>, as provided by an
appropriate proof method (such as @{method_ref cases} and @{method_ref
- induct}). The command ``@{command "case"}~@{text "a: (c x\<^sub>1 \<dots> x\<^sub>m)"}''
- abbreviates ``@{command "fix"}~@{text "x\<^sub>1 \<dots> x\<^sub>m"}~@{command
- "assume"}~@{text "a.c: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"}''. Each local fact is qualified by the
- prefix @{text "a"}, and all such facts are collectively bound to the name
- @{text a}.
+ induct}). The command ``@{command "case"}~\<open>a: (c x\<^sub>1 \<dots> x\<^sub>m)\<close>''
+ abbreviates ``@{command "fix"}~\<open>x\<^sub>1 \<dots> x\<^sub>m\<close>~@{command
+ "assume"}~\<open>a.c: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close>''. Each local fact is qualified by the
+ prefix \<open>a\<close>, and all such facts are collectively bound to the name
+ \<open>a\<close>.
- The fact name is specification @{text a} is optional, the default is to
- re-use @{text c}. So @{command "case"}~@{text "(c x\<^sub>1 \<dots> x\<^sub>m)"} is the same
- as @{command "case"}~@{text "c: (c x\<^sub>1 \<dots> x\<^sub>m)"}.
+ The fact name is specification \<open>a\<close> is optional, the default is to
+ re-use \<open>c\<close>. So @{command "case"}~\<open>(c x\<^sub>1 \<dots> x\<^sub>m)\<close> is the same
+ as @{command "case"}~\<open>c: (c x\<^sub>1 \<dots> x\<^sub>m)\<close>.
\<^descr> @{command "print_cases"} prints all local contexts of the
current state, using Isar proof language notation.
- \<^descr> @{attribute case_names}~@{text "c\<^sub>1 \<dots> c\<^sub>k"} declares names for
- the local contexts of premises of a theorem; @{text "c\<^sub>1, \<dots>, c\<^sub>k"}
+ \<^descr> @{attribute case_names}~\<open>c\<^sub>1 \<dots> c\<^sub>k\<close> declares names for
+ the local contexts of premises of a theorem; \<open>c\<^sub>1, \<dots>, c\<^sub>k\<close>
refers to the \<^emph>\<open>prefix\<close> of the list of premises. Each of the
- cases @{text "c\<^sub>i"} can be of the form @{text "c[h\<^sub>1 \<dots> h\<^sub>n]"} where
- the @{text "h\<^sub>1 \<dots> h\<^sub>n"} are the names of the hypotheses in case @{text "c\<^sub>i"}
+ cases \<open>c\<^sub>i\<close> can be of the form \<open>c[h\<^sub>1 \<dots> h\<^sub>n]\<close> where
+ the \<open>h\<^sub>1 \<dots> h\<^sub>n\<close> are the names of the hypotheses in case \<open>c\<^sub>i\<close>
from left to right.
- \<^descr> @{attribute case_conclusion}~@{text "c d\<^sub>1 \<dots> d\<^sub>k"} declares
- names for the conclusions of a named premise @{text c}; here @{text
- "d\<^sub>1, \<dots>, d\<^sub>k"} refers to the prefix of arguments of a logical formula
- built by nesting a binary connective (e.g.\ @{text "\<or>"}).
+ \<^descr> @{attribute case_conclusion}~\<open>c d\<^sub>1 \<dots> d\<^sub>k\<close> declares
+ names for the conclusions of a named premise \<open>c\<close>; here \<open>d\<^sub>1, \<dots>, d\<^sub>k\<close> refers to the prefix of arguments of a logical formula
+ built by nesting a binary connective (e.g.\ \<open>\<or>\<close>).
Note that proof methods such as @{method induct} and @{method
coinduct} already provide a default name for the conclusion as a
whole. The need to name subformulas only arises with cases that
split into several sub-cases, as in common co-induction rules.
- \<^descr> @{attribute params}~@{text "p\<^sub>1 \<dots> p\<^sub>m \<AND> \<dots> q\<^sub>1 \<dots> q\<^sub>n"} renames
- the innermost parameters of premises @{text "1, \<dots>, n"} of some
+ \<^descr> @{attribute params}~\<open>p\<^sub>1 \<dots> p\<^sub>m \<AND> \<dots> q\<^sub>1 \<dots> q\<^sub>n\<close> renames
+ the innermost parameters of premises \<open>1, \<dots>, n\<close> of some
theorem. An empty list of names may be given to skip positions,
leaving the present parameters unchanged.
Note that the default usage of case rules does \<^emph>\<open>not\<close> directly
expose parameters to the proof context.
- \<^descr> @{attribute consumes}~@{text n} declares the number of ``major
+ \<^descr> @{attribute consumes}~\<open>n\<close> declares the number of ``major
premises'' of a rule, i.e.\ the number of facts to be consumed when
it is applied by an appropriate proof method. The default value of
- @{attribute consumes} is @{text "n = 1"}, which is appropriate for
+ @{attribute consumes} is \<open>n = 1\<close>, which is appropriate for
the usual kind of cases and induction rules for inductive sets (cf.\
\secref{sec:hol-inductive}). Rules without any @{attribute
consumes} declaration given are treated as if @{attribute
- consumes}~@{text 0} had been specified.
+ consumes}~\<open>0\<close> had been specified.
- A negative @{text n} is interpreted relatively to the total number
+ A negative \<open>n\<close> is interpreted relatively to the total number
of premises of the rule in the target context. Thus its absolute
value specifies the remaining number of premises, after subtracting
the prefix of major premises as indicated above. This form of
@@ -1120,10 +1105,10 @@
text \<open>
\begin{matharray}{rcl}
- @{method_def cases} & : & @{text method} \\
- @{method_def induct} & : & @{text method} \\
- @{method_def induction} & : & @{text method} \\
- @{method_def coinduct} & : & @{text method} \\
+ @{method_def cases} & : & \<open>method\<close> \\
+ @{method_def induct} & : & \<open>method\<close> \\
+ @{method_def induction} & : & \<open>method\<close> \\
+ @{method_def coinduct} & : & \<open>method\<close> \\
\end{matharray}
The @{method cases}, @{method induct}, @{method induction},
@@ -1167,9 +1152,9 @@
taking: 'taking' ':' @{syntax insts}
\<close>}
- \<^descr> @{method cases}~@{text "insts R"} applies method @{method
+ \<^descr> @{method cases}~\<open>insts R\<close> applies method @{method
rule} with an appropriate case distinction theorem, instantiated to
- the subjects @{text insts}. Symbolic case names are bound according
+ the subjects \<open>insts\<close>. Symbolic case names are bound according
to the rule's local contexts.
The rule is determined as follows, according to the facts and
@@ -1178,11 +1163,11 @@
\<^medskip>
\begin{tabular}{llll}
facts & & arguments & rule \\\hline
- @{text "\<turnstile> R"} & @{method cases} & & implicit rule @{text R} \\
+ \<open>\<turnstile> R\<close> & @{method cases} & & implicit rule \<open>R\<close> \\
& @{method cases} & & classical case split \\
- & @{method cases} & @{text t} & datatype exhaustion (type of @{text t}) \\
- @{text "\<turnstile> A t"} & @{method cases} & @{text "\<dots>"} & inductive predicate/set elimination (of @{text A}) \\
- @{text "\<dots>"} & @{method cases} & @{text "\<dots> rule: R"} & explicit rule @{text R} \\
+ & @{method cases} & \<open>t\<close> & datatype exhaustion (type of \<open>t\<close>) \\
+ \<open>\<turnstile> A t\<close> & @{method cases} & \<open>\<dots>\<close> & inductive predicate/set elimination (of \<open>A\<close>) \\
+ \<open>\<dots>\<close> & @{method cases} & \<open>\<dots> rule: R\<close> & explicit rule \<open>R\<close> \\
\end{tabular}
\<^medskip>
@@ -1190,91 +1175,89 @@
of premises of the case rule; within each premise, the \<^emph>\<open>prefix\<close>
of variables is instantiated. In most situations, only a single
term needs to be specified; this refers to the first variable of the
- last premise (it is usually the same for all cases). The @{text
- "(no_simp)"} option can be used to disable pre-simplification of
+ last premise (it is usually the same for all cases). The \<open>(no_simp)\<close> option can be used to disable pre-simplification of
cases (see the description of @{method induct} below for details).
- \<^descr> @{method induct}~@{text "insts R"} and
- @{method induction}~@{text "insts R"} are analogous to the
+ \<^descr> @{method induct}~\<open>insts R\<close> and
+ @{method induction}~\<open>insts R\<close> are analogous to the
@{method cases} method, but refer to induction rules, which are
determined as follows:
\<^medskip>
\begin{tabular}{llll}
facts & & arguments & rule \\\hline
- & @{method induct} & @{text "P x"} & datatype induction (type of @{text x}) \\
- @{text "\<turnstile> A x"} & @{method induct} & @{text "\<dots>"} & predicate/set induction (of @{text A}) \\
- @{text "\<dots>"} & @{method induct} & @{text "\<dots> rule: R"} & explicit rule @{text R} \\
+ & @{method induct} & \<open>P x\<close> & datatype induction (type of \<open>x\<close>) \\
+ \<open>\<turnstile> A x\<close> & @{method induct} & \<open>\<dots>\<close> & predicate/set induction (of \<open>A\<close>) \\
+ \<open>\<dots>\<close> & @{method induct} & \<open>\<dots> rule: R\<close> & explicit rule \<open>R\<close> \\
\end{tabular}
\<^medskip>
Several instantiations may be given, each referring to some part of
a mutual inductive definition or datatype --- only related partial
induction rules may be used together, though. Any of the lists of
- terms @{text "P, x, \<dots>"} refers to the \<^emph>\<open>suffix\<close> of variables
+ terms \<open>P, x, \<dots>\<close> refers to the \<^emph>\<open>suffix\<close> of variables
present in the induction rule. This enables the writer to specify
only induction variables, or both predicates and variables, for
example.
- Instantiations may be definitional: equations @{text "x \<equiv> t"}
+ Instantiations may be definitional: equations \<open>x \<equiv> t\<close>
introduce local definitions, which are inserted into the claim and
discharged after applying the induction rule. Equalities reappear
in the inductive cases, but have been transformed according to the
induction principle being involved here. In order to achieve
practically useful induction hypotheses, some variables occurring in
- @{text t} need to be fixed (see below). Instantiations of the form
- @{text t}, where @{text t} is not a variable, are taken as a
- shorthand for \mbox{@{text "x \<equiv> t"}}, where @{text x} is a fresh
- variable. If this is not intended, @{text t} has to be enclosed in
+ \<open>t\<close> need to be fixed (see below). Instantiations of the form
+ \<open>t\<close>, where \<open>t\<close> is not a variable, are taken as a
+ shorthand for \mbox{\<open>x \<equiv> t\<close>}, where \<open>x\<close> is a fresh
+ variable. If this is not intended, \<open>t\<close> has to be enclosed in
parentheses. By default, the equalities generated by definitional
instantiations are pre-simplified using a specific set of rules,
usually consisting of distinctness and injectivity theorems for
datatypes. This pre-simplification may cause some of the parameters
of an inductive case to disappear, or may even completely delete
some of the inductive cases, if one of the equalities occurring in
- their premises can be simplified to @{text False}. The @{text
- "(no_simp)"} option can be used to disable pre-simplification.
+ their premises can be simplified to \<open>False\<close>. The \<open>(no_simp)\<close> option can be used to disable pre-simplification.
Additional rules to be used in pre-simplification can be declared
using the @{attribute_def induct_simp} attribute.
- The optional ``@{text "arbitrary: x\<^sub>1 \<dots> x\<^sub>m"}''
- specification generalizes variables @{text "x\<^sub>1, \<dots>,
- x\<^sub>m"} of the original goal before applying induction. One can
- separate variables by ``@{text "and"}'' to generalize them in other
+ The optional ``\<open>arbitrary: x\<^sub>1 \<dots> x\<^sub>m\<close>''
+ specification generalizes variables \<open>x\<^sub>1, \<dots>,
+ x\<^sub>m\<close> of the original goal before applying induction. One can
+ separate variables by ``\<open>and\<close>'' to generalize them in other
goals then the first. Thus induction hypotheses may become
sufficiently general to get the proof through. Together with
definitional instantiations, one may effectively perform induction
over expressions of a certain structure.
- The optional ``@{text "taking: t\<^sub>1 \<dots> t\<^sub>n"}''
+ The optional ``\<open>taking: t\<^sub>1 \<dots> t\<^sub>n\<close>''
specification provides additional instantiations of a prefix of
pending variables in the rule. Such schematic induction rules
rarely occur in practice, though.
- \<^descr> @{method coinduct}~@{text "inst R"} is analogous to the
+ \<^descr> @{method coinduct}~\<open>inst R\<close> is analogous to the
@{method induct} method, but refers to coinduction rules, which are
determined as follows:
\<^medskip>
\begin{tabular}{llll}
goal & & arguments & rule \\\hline
- & @{method coinduct} & @{text x} & type coinduction (type of @{text x}) \\
- @{text "A x"} & @{method coinduct} & @{text "\<dots>"} & predicate/set coinduction (of @{text A}) \\
- @{text "\<dots>"} & @{method coinduct} & @{text "\<dots> rule: R"} & explicit rule @{text R} \\
+ & @{method coinduct} & \<open>x\<close> & type coinduction (type of \<open>x\<close>) \\
+ \<open>A x\<close> & @{method coinduct} & \<open>\<dots>\<close> & predicate/set coinduction (of \<open>A\<close>) \\
+ \<open>\<dots>\<close> & @{method coinduct} & \<open>\<dots> rule: R\<close> & explicit rule \<open>R\<close> \\
\end{tabular}
\<^medskip>
Coinduction is the dual of induction. Induction essentially
- eliminates @{text "A x"} towards a generic result @{text "P x"},
- while coinduction introduces @{text "A x"} starting with @{text "B
- x"}, for a suitable ``bisimulation'' @{text B}. The cases of a
+ eliminates \<open>A x\<close> towards a generic result \<open>P x\<close>,
+ while coinduction introduces \<open>A x\<close> starting with \<open>B
+ x\<close>, for a suitable ``bisimulation'' \<open>B\<close>. The cases of a
coinduct rule are typically named after the predicates or sets being
covered, while the conclusions consist of several alternatives being
named after the individual destructor patterns.
The given instantiation refers to the \<^emph>\<open>suffix\<close> of variables
occurring in the rule's major premise, or conclusion if unavailable.
- An additional ``@{text "taking: t\<^sub>1 \<dots> t\<^sub>n"}''
+ An additional ``\<open>taking: t\<^sub>1 \<dots> t\<^sub>n\<close>''
specification may be required in order to specify the bisimulation
to be used in the coinduction step.
@@ -1295,8 +1278,7 @@
Despite the additional infrastructure, both @{method cases}
and @{method coinduct} merely apply a certain rule, after
instantiation, while conforming due to the usual way of monotonic
- natural deduction: the context of a structured statement @{text
- "\<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> \<dots>"}
+ natural deduction: the context of a structured statement \<open>\<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> \<dots>\<close>
reappears unchanged after the case split.
The @{method induct} method is fundamentally different in this
@@ -1309,17 +1291,16 @@
of the original statement.
In @{method induct} proofs, local assumptions introduced by cases are split
- into two different kinds: @{text hyps} stemming from the rule and
- @{text prems} from the goal statement. This is reflected in the
- extracted cases accordingly, so invoking ``@{command "case"}~@{text
- c}'' will provide separate facts @{text c.hyps} and @{text c.prems},
- as well as fact @{text c} to hold the all-inclusive list.
+ into two different kinds: \<open>hyps\<close> stemming from the rule and
+ \<open>prems\<close> from the goal statement. This is reflected in the
+ extracted cases accordingly, so invoking ``@{command "case"}~\<open>c\<close>'' will provide separate facts \<open>c.hyps\<close> and \<open>c.prems\<close>,
+ as well as fact \<open>c\<close> to hold the all-inclusive list.
In @{method induction} proofs, local assumptions introduced by cases are
- split into three different kinds: @{text IH}, the induction hypotheses,
- @{text hyps}, the remaining hypotheses stemming from the rule, and
- @{text prems}, the assumptions from the goal statement. The names are
- @{text c.IH}, @{text c.hyps} and @{text c.prems}, as above.
+ split into three different kinds: \<open>IH\<close>, the induction hypotheses,
+ \<open>hyps\<close>, the remaining hypotheses stemming from the rule, and
+ \<open>prems\<close>, the assumptions from the goal statement. The names are
+ \<open>c.IH\<close>, \<open>c.hyps\<close> and \<open>c.prems\<close>, as above.
\<^medskip>
@@ -1328,7 +1309,7 @@
usually 0 for plain cases and induction rules of datatypes etc.\ and
1 for rules of inductive predicates or sets and the like. The
remaining facts are inserted into the goal verbatim before the
- actual @{text cases}, @{text induct}, or @{text coinduct} rule is
+ actual \<open>cases\<close>, \<open>induct\<close>, or \<open>coinduct\<close> rule is
applied.
\<close>
@@ -1337,10 +1318,10 @@
text \<open>
\begin{matharray}{rcl}
- @{command_def "print_induct_rules"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
- @{attribute_def cases} & : & @{text attribute} \\
- @{attribute_def induct} & : & @{text attribute} \\
- @{attribute_def coinduct} & : & @{text attribute} \\
+ @{command_def "print_induct_rules"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
+ @{attribute_def cases} & : & \<open>attribute\<close> \\
+ @{attribute_def induct} & : & \<open>attribute\<close> \\
+ @{attribute_def coinduct} & : & \<open>attribute\<close> \\
\end{matharray}
@{rail \<open>
@@ -1364,18 +1345,18 @@
packages of object-logics usually declare emerging cases and
induction rules as expected, so users rarely need to intervene.
- Rules may be deleted via the @{text "del"} specification, which
- covers all of the @{text "type"}/@{text "pred"}/@{text "set"}
+ Rules may be deleted via the \<open>del\<close> specification, which
+ covers all of the \<open>type\<close>/\<open>pred\<close>/\<open>set\<close>
sub-categories simultaneously. For example, @{attribute
- cases}~@{text del} removes any @{attribute cases} rules declared for
+ cases}~\<open>del\<close> removes any @{attribute cases} rules declared for
some type, predicate, or set.
Manual rule declarations usually refer to the @{attribute
case_names} and @{attribute params} attributes to adjust names of
cases and parameters of a rule; the @{attribute consumes}
declaration is taken care of automatically: @{attribute
- consumes}~@{text 0} is specified for ``type'' rules and @{attribute
- consumes}~@{text 1} for ``predicate'' / ``set'' rules.
+ consumes}~\<open>0\<close> is specified for ``type'' rules and @{attribute
+ consumes}~\<open>1\<close> for ``predicate'' / ``set'' rules.
\<close>
@@ -1383,9 +1364,9 @@
text \<open>
\begin{matharray}{rcl}
- @{command_def "consider"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\
- @{command_def "obtain"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\
- @{command_def "guess"}@{text "\<^sup>*"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\
+ @{command_def "consider"} & : & \<open>proof(state) | proof(chain) \<rightarrow> proof(prove)\<close> \\
+ @{command_def "obtain"} & : & \<open>proof(state) | proof(chain) \<rightarrow> proof(prove)\<close> \\
+ @{command_def "guess"}\<open>\<^sup>*\<close> & : & \<open>proof(state) | proof(chain) \<rightarrow> proof(prove)\<close> \\
\end{matharray}
Generalized elimination means that hypothetical parameters and premises
@@ -1396,9 +1377,9 @@
\<^medskip>
\begin{tabular}{ll}
- @{text "\<exists>x. B x \<Longrightarrow> (\<And>x. B x \<Longrightarrow> thesis) \<Longrightarrow> thesis"} \\
- @{text "A \<and> B \<Longrightarrow> (A \<Longrightarrow> B \<Longrightarrow> thesis) \<Longrightarrow> thesis"} \\
- @{text "A \<or> B \<Longrightarrow> (A \<Longrightarrow> thesis) \<Longrightarrow> (B \<Longrightarrow> thesis) \<Longrightarrow> thesis"} \\
+ \<open>\<exists>x. B x \<Longrightarrow> (\<And>x. B x \<Longrightarrow> thesis) \<Longrightarrow> thesis\<close> \\
+ \<open>A \<and> B \<Longrightarrow> (A \<Longrightarrow> B \<Longrightarrow> thesis) \<Longrightarrow> thesis\<close> \\
+ \<open>A \<or> B \<Longrightarrow> (A \<Longrightarrow> thesis) \<Longrightarrow> (B \<Longrightarrow> thesis) \<Longrightarrow> thesis\<close> \\
\end{tabular}
\<^medskip>
@@ -1416,8 +1397,8 @@
@@{command guess} (@{syntax "fixes"} + @'and')
\<close>}
- \<^descr> @{command consider}~@{text "(a) \<^vec>x \<WHERE> \<^vec>A \<^vec>x
- | (b) \<^vec>y \<WHERE> \<^vec>B \<^vec>y | \<dots> "} states a rule for case
+ \<^descr> @{command consider}~\<open>(a) \<^vec>x \<WHERE> \<^vec>A \<^vec>x
+ | (b) \<^vec>y \<WHERE> \<^vec>B \<^vec>y | \<dots> \<close> states a rule for case
splitting into separate subgoals, such that each case involves new
parameters and premises. After the proof is finished, the resulting rule
may be used directly with the @{method cases} proof method
@@ -1433,24 +1414,24 @@
Isar language element as follows:
\begin{matharray}{l}
- @{command "consider"}~@{text "(a) \<^vec>x \<WHERE> \<^vec>A \<^vec>x | (b) \<^vec>y \<WHERE> \<^vec>B \<^vec>y | \<dots> \<equiv>"} \\[1ex]
- \quad @{command "have"}~@{text "[case_names a b \<dots>]: thesis"} \\
- \qquad @{text "\<IF> a [Pure.intro?]: \<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis"} \\
- \qquad @{text "\<AND> b [Pure.intro?]: \<And>\<^vec>y. \<^vec>B \<^vec>y \<Longrightarrow> thesis"} \\
- \qquad @{text "\<AND> \<dots>"} \\
- \qquad @{text "\<FOR> thesis"} \\
- \qquad @{command "apply"}~@{text "(insert a b \<dots>)"} \\
+ @{command "consider"}~\<open>(a) \<^vec>x \<WHERE> \<^vec>A \<^vec>x | (b) \<^vec>y \<WHERE> \<^vec>B \<^vec>y | \<dots> \<equiv>\<close> \\[1ex]
+ \quad @{command "have"}~\<open>[case_names a b \<dots>]: thesis\<close> \\
+ \qquad \<open>\<IF> a [Pure.intro?]: \<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis\<close> \\
+ \qquad \<open>\<AND> b [Pure.intro?]: \<And>\<^vec>y. \<^vec>B \<^vec>y \<Longrightarrow> thesis\<close> \\
+ \qquad \<open>\<AND> \<dots>\<close> \\
+ \qquad \<open>\<FOR> thesis\<close> \\
+ \qquad @{command "apply"}~\<open>(insert a b \<dots>)\<close> \\
\end{matharray}
See also \secref{sec:goals} for @{keyword "obtains"} in toplevel goal
statements, as well as @{command print_statement} to print existing rules
in a similar format.
- \<^descr> @{command obtain}~@{text "\<^vec>x \<WHERE> \<^vec>A \<^vec>x"}
+ \<^descr> @{command obtain}~\<open>\<^vec>x \<WHERE> \<^vec>A \<^vec>x\<close>
states a generalized elimination rule with exactly one case. After the
proof is finished, it is activated for the subsequent proof text: the
- context is augmented via @{command fix}~@{text "\<^vec>x"} @{command
- assume}~@{text "\<^vec>A \<^vec>x"}, with special provisions to export
+ context is augmented via @{command fix}~\<open>\<^vec>x\<close> @{command
+ assume}~\<open>\<^vec>A \<^vec>x\<close>, with special provisions to export
later results by discharging these assumptions again.
Note that according to the parameter scopes within the elimination rule,
@@ -1464,13 +1445,13 @@
@{command assume}:
\begin{matharray}{l}
- @{command "obtain"}~@{text "\<^vec>x \<WHERE> a: \<^vec>A \<^vec>x \<langle>proof\<rangle> \<equiv>"} \\[1ex]
- \quad @{command "have"}~@{text "thesis"} \\
- \qquad @{text "\<IF> that [Pure.intro?]: \<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis"} \\
- \qquad @{text "\<FOR> thesis"} \\
- \qquad @{command "apply"}~@{text "(insert that)"} \\
- \qquad @{text "\<langle>proof\<rangle>"} \\
- \quad @{command "fix"}~@{text "\<^vec>x"}~@{command "assume"}@{text "\<^sup>* a: \<^vec>A \<^vec>x"} \\
+ @{command "obtain"}~\<open>\<^vec>x \<WHERE> a: \<^vec>A \<^vec>x \<langle>proof\<rangle> \<equiv>\<close> \\[1ex]
+ \quad @{command "have"}~\<open>thesis\<close> \\
+ \qquad \<open>\<IF> that [Pure.intro?]: \<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis\<close> \\
+ \qquad \<open>\<FOR> thesis\<close> \\
+ \qquad @{command "apply"}~\<open>(insert that)\<close> \\
+ \qquad \<open>\<langle>proof\<rangle>\<close> \\
+ \quad @{command "fix"}~\<open>\<^vec>x\<close>~@{command "assume"}\<open>\<^sup>* a: \<^vec>A \<^vec>x\<close> \\
\end{matharray}
\<^descr> @{command guess} is similar to @{command obtain}, but it derives the
@@ -1478,11 +1459,10 @@
proof. Thus it can considerably obscure the proof: it is classified as
\<^emph>\<open>improper\<close>.
- A proof with @{command guess} starts with a fixed goal @{text thesis}. The
- subsequent refinement steps may turn this to anything of the form @{text
- "\<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis"}, but without splitting into new
+ A proof with @{command guess} starts with a fixed goal \<open>thesis\<close>. The
+ subsequent refinement steps may turn this to anything of the form \<open>\<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis\<close>, but without splitting into new
subgoals. The final goal state is then used as reduction rule for the
- obtain pattern described above. Obtained parameters @{text "\<^vec>x"} are
+ obtain pattern described above. Obtained parameters \<open>\<^vec>x\<close> are
marked as internal by default, and thus inaccessible in the proof text.
The variable names and type constraints given as arguments for @{command
"guess"} specify a prefix of accessible parameters.