author | wenzelm |
Tue, 20 Oct 2015 23:53:40 +0200 | |
changeset 61493 | 0debd22f0c0e |
parent 61477 | e467ae7aa808 |
child 61494 | 63b18f758874 |
permissions | -rw-r--r-- |
26869 | 1 |
theory Proof |
42651 | 2 |
imports Base Main |
26869 | 3 |
begin |
4 |
||
58618 | 5 |
chapter \<open>Proofs \label{ch:proofs}\<close> |
26869 | 6 |
|
58618 | 7 |
text \<open> |
26870 | 8 |
Proof commands perform transitions of Isar/VM machine |
9 |
configurations, which are block-structured, consisting of a stack of |
|
10 |
nodes with three main components: logical proof context, current |
|
29741 | 11 |
facts, and open goals. Isar/VM transitions are typed according to |
12 |
the following three different modes of operation: |
|
26870 | 13 |
|
61493 | 14 |
\<^descr> \<open>proof(prove)\<close> means that a new goal has just been |
61477 | 15 |
stated that is now to be \<^emph>\<open>proven\<close>; the next command may refine |
26870 | 16 |
it by some proof method, and enter a sub-proof to establish the |
17 |
actual result. |
|
18 |
||
61493 | 19 |
\<^descr> \<open>proof(state)\<close> is like a nested theory mode: the |
61477 | 20 |
context may be augmented by \<^emph>\<open>stating\<close> additional assumptions, |
26870 | 21 |
intermediate results etc. |
22 |
||
61493 | 23 |
\<^descr> \<open>proof(chain)\<close> is intermediate between \<open>proof(state)\<close> and \<open>proof(prove)\<close>: existing facts (i.e.\ the |
60480 | 24 |
contents of the special @{fact_ref this} register) have been just picked |
25 |
up in order to be used when refining the goal claimed next. |
|
26870 | 26 |
|
27 |
||
29741 | 28 |
The proof mode indicator may be understood as an instruction to the |
29 |
writer, telling what kind of operation may be performed next. The |
|
30 |
corresponding typings of proof commands restricts the shape of |
|
31 |
well-formed proof texts to particular command sequences. So dynamic |
|
32 |
arrangements of commands eventually turn out as static texts of a |
|
33 |
certain structure. |
|
34 |
||
35 |
\Appref{ap:refcard} gives a simplified grammar of the (extensible) |
|
36 |
language emerging that way from the different types of proof |
|
37 |
commands. The main ideas of the overall Isar framework are |
|
38 |
explained in \chref{ch:isar-framework}. |
|
58618 | 39 |
\<close> |
26870 | 40 |
|
41 |
||
58618 | 42 |
section \<open>Proof structure\<close> |
28755 | 43 |
|
58618 | 44 |
subsection \<open>Formal notepad\<close> |
36356
5ab0f8859f9f
command 'example_proof' opens an empty proof body;
wenzelm
parents:
36320
diff
changeset
|
45 |
|
58618 | 46 |
text \<open> |
36356
5ab0f8859f9f
command 'example_proof' opens an empty proof body;
wenzelm
parents:
36320
diff
changeset
|
47 |
\begin{matharray}{rcl} |
61493 | 48 |
@{command_def "notepad"} & : & \<open>local_theory \<rightarrow> proof(state)\<close> \\ |
36356
5ab0f8859f9f
command 'example_proof' opens an empty proof body;
wenzelm
parents:
36320
diff
changeset
|
49 |
\end{matharray} |
5ab0f8859f9f
command 'example_proof' opens an empty proof body;
wenzelm
parents:
36320
diff
changeset
|
50 |
|
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
51 |
@{rail \<open> |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40965
diff
changeset
|
52 |
@@{command notepad} @'begin' |
40965
54b6c9e1c157
command 'notepad' replaces former 'example_proof';
wenzelm
parents:
40255
diff
changeset
|
53 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40965
diff
changeset
|
54 |
@@{command end} |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
55 |
\<close>} |
40965
54b6c9e1c157
command 'notepad' replaces former 'example_proof';
wenzelm
parents:
40255
diff
changeset
|
56 |
|
61439 | 57 |
\<^descr> @{command "notepad"}~@{keyword "begin"} opens a proof state without |
60482 | 58 |
any goal statement. This allows to experiment with Isar, without producing |
59 |
any persistent result. The notepad is closed by @{command "end"}. |
|
58618 | 60 |
\<close> |
36356
5ab0f8859f9f
command 'example_proof' opens an empty proof body;
wenzelm
parents:
36320
diff
changeset
|
61 |
|
5ab0f8859f9f
command 'example_proof' opens an empty proof body;
wenzelm
parents:
36320
diff
changeset
|
62 |
|
58618 | 63 |
subsection \<open>Blocks\<close> |
28755 | 64 |
|
58618 | 65 |
text \<open> |
28755 | 66 |
\begin{matharray}{rcl} |
61493 | 67 |
@{command_def "next"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\ |
68 |
@{command_def "{"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\ |
|
69 |
@{command_def "}"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\ |
|
28755 | 70 |
\end{matharray} |
71 |
||
72 |
While Isar is inherently block-structured, opening and closing |
|
73 |
blocks is mostly handled rather casually, with little explicit |
|
74 |
user-intervention. Any local goal statement automatically opens |
|
61477 | 75 |
\<^emph>\<open>two\<close> internal blocks, which are closed again when concluding |
28755 | 76 |
the sub-proof (by @{command "qed"} etc.). Sections of different |
77 |
context within a sub-proof may be switched via @{command "next"}, |
|
78 |
which is just a single block-close followed by block-open again. |
|
79 |
The effect of @{command "next"} is to reset the local proof context; |
|
80 |
there is no goal focus involved here! |
|
81 |
||
82 |
For slightly more advanced applications, there are explicit block |
|
83 |
parentheses as well. These typically achieve a stronger forward |
|
84 |
style of reasoning. |
|
85 |
||
61439 | 86 |
\<^descr> @{command "next"} switches to a fresh block within a |
28755 | 87 |
sub-proof, resetting the local context to the initial one. |
88 |
||
61439 | 89 |
\<^descr> @{command "{"} and @{command "}"} explicitly open and close |
28755 | 90 |
blocks. Any current facts pass through ``@{command "{"}'' |
91 |
unchanged, while ``@{command "}"}'' causes any result to be |
|
61477 | 92 |
\<^emph>\<open>exported\<close> into the enclosing context. Thus fixed variables |
28755 | 93 |
are generalized, assumptions discharged, and local definitions |
94 |
unfolded (cf.\ \secref{sec:proof-context}). There is no difference |
|
95 |
of @{command "assume"} and @{command "presume"} in this mode of |
|
96 |
forward reasoning --- in contrast to plain backward reasoning with |
|
97 |
the result exported at @{command "show"} time. |
|
58618 | 98 |
\<close> |
28755 | 99 |
|
100 |
||
58618 | 101 |
subsection \<open>Omitting proofs\<close> |
28755 | 102 |
|
58618 | 103 |
text \<open> |
28755 | 104 |
\begin{matharray}{rcl} |
61493 | 105 |
@{command_def "oops"} & : & \<open>proof \<rightarrow> local_theory | theory\<close> \\ |
28755 | 106 |
\end{matharray} |
107 |
||
108 |
The @{command "oops"} command discontinues the current proof |
|
109 |
attempt, while considering the partial proof text as properly |
|
110 |
processed. This is conceptually quite different from ``faking'' |
|
111 |
actual proofs via @{command_ref "sorry"} (see |
|
112 |
\secref{sec:proof-steps}): @{command "oops"} does not observe the |
|
113 |
proof structure at all, but goes back right to the theory level. |
|
114 |
Furthermore, @{command "oops"} does not produce any result theorem |
|
115 |
--- there is no intended claim to be able to complete the proof |
|
45103 | 116 |
in any way. |
28755 | 117 |
|
118 |
A typical application of @{command "oops"} is to explain Isar proofs |
|
61477 | 119 |
\<^emph>\<open>within\<close> the system itself, in conjunction with the document |
28838
d5db6dfcb34a
moved table of standard Isabelle symbols to isar-ref manual;
wenzelm
parents:
28761
diff
changeset
|
120 |
preparation tools of Isabelle described in \chref{ch:document-prep}. |
28755 | 121 |
Thus partial or even wrong proof attempts can be discussed in a |
122 |
logically sound manner. Note that the Isabelle {\LaTeX} macros can |
|
61493 | 123 |
be easily adapted to print something like ``\<open>\<dots>\<close>'' instead of |
28755 | 124 |
the keyword ``@{command "oops"}''. |
58618 | 125 |
\<close> |
28755 | 126 |
|
127 |
||
58618 | 128 |
section \<open>Statements\<close> |
28754
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
27141
diff
changeset
|
129 |
|
58618 | 130 |
subsection \<open>Context elements \label{sec:proof-context}\<close> |
26870 | 131 |
|
58618 | 132 |
text \<open> |
26870 | 133 |
\begin{matharray}{rcl} |
61493 | 134 |
@{command_def "fix"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\ |
135 |
@{command_def "assume"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\ |
|
136 |
@{command_def "presume"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\ |
|
137 |
@{command_def "def"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\ |
|
26870 | 138 |
\end{matharray} |
139 |
||
140 |
The logical proof context consists of fixed variables and |
|
141 |
assumptions. The former closely correspond to Skolem constants, or |
|
142 |
meta-level universal quantification as provided by the Isabelle/Pure |
|
61477 | 143 |
logical framework. Introducing some \<^emph>\<open>arbitrary, but fixed\<close> |
61493 | 144 |
variable via ``@{command "fix"}~\<open>x\<close>'' results in a local value |
26870 | 145 |
that may be used in the subsequent proof as any other variable or |
61493 | 146 |
constant. Furthermore, any result \<open>\<turnstile> \<phi>[x]\<close> exported from |
147 |
the context will be universally closed wrt.\ \<open>x\<close> at the |
|
148 |
outermost level: \<open>\<turnstile> \<And>x. \<phi>[x]\<close> (this is expressed in normal |
|
26870 | 149 |
form using Isabelle's meta-variables). |
150 |
||
61493 | 151 |
Similarly, introducing some assumption \<open>\<chi>\<close> has two effects. |
26870 | 152 |
On the one hand, a local theorem is created that may be used as a |
153 |
fact in subsequent proof steps. On the other hand, any result |
|
61493 | 154 |
\<open>\<chi> \<turnstile> \<phi>\<close> exported from the context becomes conditional wrt.\ |
155 |
the assumption: \<open>\<turnstile> \<chi> \<Longrightarrow> \<phi>\<close>. Thus, solving an enclosing goal |
|
26870 | 156 |
using such a result would basically introduce a new subgoal stemming |
157 |
from the assumption. How this situation is handled depends on the |
|
158 |
version of assumption command used: while @{command "assume"} |
|
159 |
insists on solving the subgoal by unification with some premise of |
|
160 |
the goal, @{command "presume"} leaves the subgoal unchanged in order |
|
161 |
to be proved later by the user. |
|
162 |
||
61493 | 163 |
Local definitions, introduced by ``@{command "def"}~\<open>x \<equiv> |
164 |
t\<close>'', are achieved by combining ``@{command "fix"}~\<open>x\<close>'' with |
|
26870 | 165 |
another version of assumption that causes any hypothetical equation |
61493 | 166 |
\<open>x \<equiv> t\<close> to be eliminated by the reflexivity rule. Thus, |
167 |
exporting some result \<open>x \<equiv> t \<turnstile> \<phi>[x]\<close> yields \<open>\<turnstile> |
|
168 |
\<phi>[t]\<close>. |
|
26870 | 169 |
|
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
170 |
@{rail \<open> |
59785 | 171 |
@@{command fix} @{syntax "fixes"} |
26870 | 172 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40965
diff
changeset
|
173 |
(@@{command assume} | @@{command presume}) (@{syntax props} + @'and') |
26870 | 174 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40965
diff
changeset
|
175 |
@@{command def} (def + @'and') |
26870 | 176 |
; |
55029
61a6bf7d4b02
clarified @{rail} syntax: prefer explicit \<newline> symbol;
wenzelm
parents:
53377
diff
changeset
|
177 |
def: @{syntax thmdecl}? \<newline> |
61a6bf7d4b02
clarified @{rail} syntax: prefer explicit \<newline> symbol;
wenzelm
parents:
53377
diff
changeset
|
178 |
@{syntax name} ('==' | '\<equiv>') @{syntax term} @{syntax term_pat}? |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
179 |
\<close>} |
26870 | 180 |
|
61493 | 181 |
\<^descr> @{command "fix"}~\<open>x\<close> introduces a local variable \<open>x\<close> that is \<^emph>\<open>arbitrary, but fixed\<close>. |
60483 | 182 |
|
61493 | 183 |
\<^descr> @{command "assume"}~\<open>a: \<phi>\<close> and @{command |
184 |
"presume"}~\<open>a: \<phi>\<close> introduce a local fact \<open>\<phi> \<turnstile> \<phi>\<close> by |
|
26870 | 185 |
assumption. Subsequent results applied to an enclosing goal (e.g.\ |
186 |
by @{command_ref "show"}) are handled as follows: @{command |
|
187 |
"assume"} expects to be able to unify with existing premises in the |
|
61493 | 188 |
goal, while @{command "presume"} leaves \<open>\<phi>\<close> as new subgoals. |
60483 | 189 |
|
26870 | 190 |
Several lists of assumptions may be given (separated by |
191 |
@{keyword_ref "and"}; the resulting list of current facts consists |
|
192 |
of all of these concatenated. |
|
60483 | 193 |
|
61493 | 194 |
\<^descr> @{command "def"}~\<open>x \<equiv> t\<close> introduces a local |
26870 | 195 |
(non-polymorphic) definition. In results exported from the context, |
61493 | 196 |
\<open>x\<close> is replaced by \<open>t\<close>. Basically, ``@{command |
197 |
"def"}~\<open>x \<equiv> t\<close>'' abbreviates ``@{command "fix"}~\<open>x\<close>~@{command "assume"}~\<open>x \<equiv> t\<close>'', with the resulting |
|
26870 | 198 |
hypothetical equation solved by reflexivity. |
60483 | 199 |
|
61493 | 200 |
The default name for the definitional equation is \<open>x_def\<close>. |
26870 | 201 |
Several simultaneous definitions may be given at the same time. |
58618 | 202 |
\<close> |
26870 | 203 |
|
204 |
||
58618 | 205 |
subsection \<open>Term abbreviations \label{sec:term-abbrev}\<close> |
28754
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
27141
diff
changeset
|
206 |
|
58618 | 207 |
text \<open> |
28754
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
27141
diff
changeset
|
208 |
\begin{matharray}{rcl} |
61493 | 209 |
@{command_def "let"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\ |
28754
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
27141
diff
changeset
|
210 |
@{keyword_def "is"} & : & syntax \\ |
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
27141
diff
changeset
|
211 |
\end{matharray} |
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
27141
diff
changeset
|
212 |
|
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
27141
diff
changeset
|
213 |
Abbreviations may be either bound by explicit @{command |
61493 | 214 |
"let"}~\<open>p \<equiv> t\<close> statements, or by annotating assumptions or |
215 |
goal statements with a list of patterns ``\<open>(\<IS> p\<^sub>1 \<dots> |
|
216 |
p\<^sub>n)\<close>''. In both cases, higher-order matching is invoked to |
|
28754
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
27141
diff
changeset
|
217 |
bind extra-logical term variables, which may be either named |
61493 | 218 |
schematic variables of the form \<open>?x\<close>, or nameless dummies |
28754
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
27141
diff
changeset
|
219 |
``@{variable _}'' (underscore). Note that in the @{command "let"} |
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
27141
diff
changeset
|
220 |
form the patterns occur on the left-hand side, while the @{keyword |
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
27141
diff
changeset
|
221 |
"is"} patterns are in postfix position. |
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
27141
diff
changeset
|
222 |
|
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
27141
diff
changeset
|
223 |
Polymorphism of term bindings is handled in Hindley-Milner style, |
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
27141
diff
changeset
|
224 |
similar to ML. Type variables referring to local assumptions or |
61477 | 225 |
open goal statements are \<^emph>\<open>fixed\<close>, while those of finished |
226 |
results or bound by @{command "let"} may occur in \<^emph>\<open>arbitrary\<close> |
|
28754
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
27141
diff
changeset
|
227 |
instances later. Even though actual polymorphism should be rarely |
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
27141
diff
changeset
|
228 |
used in practice, this mechanism is essential to achieve proper |
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
27141
diff
changeset
|
229 |
incremental type-inference, as the user proceeds to build up the |
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
27141
diff
changeset
|
230 |
Isar proof text from left to right. |
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
27141
diff
changeset
|
231 |
|
61421 | 232 |
\<^medskip> |
233 |
Term abbreviations are quite different from local |
|
28754
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
27141
diff
changeset
|
234 |
definitions as introduced via @{command "def"} (see |
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
27141
diff
changeset
|
235 |
\secref{sec:proof-context}). The latter are visible within the |
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
27141
diff
changeset
|
236 |
logic as actual equations, while abbreviations disappear during the |
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
27141
diff
changeset
|
237 |
input process just after type checking. Also note that @{command |
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
27141
diff
changeset
|
238 |
"def"} does not support polymorphism. |
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
27141
diff
changeset
|
239 |
|
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
240 |
@{rail \<open> |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40965
diff
changeset
|
241 |
@@{command let} ((@{syntax term} + @'and') '=' @{syntax term} + @'and') |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
242 |
\<close>} |
28754
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
27141
diff
changeset
|
243 |
|
42705 | 244 |
The syntax of @{keyword "is"} patterns follows @{syntax term_pat} or |
245 |
@{syntax prop_pat} (see \secref{sec:term-decls}). |
|
28754
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
27141
diff
changeset
|
246 |
|
61493 | 247 |
\<^descr> @{command "let"}~\<open>p\<^sub>1 = t\<^sub>1 \<AND> \<dots> p\<^sub>n = t\<^sub>n\<close> binds any |
248 |
text variables in patterns \<open>p\<^sub>1, \<dots>, p\<^sub>n\<close> by simultaneous |
|
249 |
higher-order matching against terms \<open>t\<^sub>1, \<dots>, t\<^sub>n\<close>. |
|
28754
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
27141
diff
changeset
|
250 |
|
61493 | 251 |
\<^descr> \<open>(\<IS> p\<^sub>1 \<dots> p\<^sub>n)\<close> resembles @{command "let"}, but |
252 |
matches \<open>p\<^sub>1, \<dots>, p\<^sub>n\<close> against the preceding statement. Also |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28757
diff
changeset
|
253 |
note that @{keyword "is"} is not a separate command, but part of |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28757
diff
changeset
|
254 |
others (such as @{command "assume"}, @{command "have"} etc.). |
28754
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
27141
diff
changeset
|
255 |
|
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
27141
diff
changeset
|
256 |
|
61477 | 257 |
Some \<^emph>\<open>implicit\<close> term abbreviations\index{term abbreviations} |
28754
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
27141
diff
changeset
|
258 |
for goals and facts are available as well. For any open goal, |
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
27141
diff
changeset
|
259 |
@{variable_ref thesis} refers to its object-level statement, |
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
27141
diff
changeset
|
260 |
abstracted over any meta-level parameters (if present). Likewise, |
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
27141
diff
changeset
|
261 |
@{variable_ref this} is bound for fact statements resulting from |
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
27141
diff
changeset
|
262 |
assumptions or finished goals. In case @{variable this} refers to |
61493 | 263 |
an object-logic statement that is an application \<open>f t\<close>, then |
264 |
\<open>t\<close> is bound to the special text variable ``@{variable "\<dots>"}'' |
|
28754
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
27141
diff
changeset
|
265 |
(three dots). The canonical application of this convenience are |
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
27141
diff
changeset
|
266 |
calculational proofs (see \secref{sec:calculation}). |
58618 | 267 |
\<close> |
28754
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
27141
diff
changeset
|
268 |
|
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
27141
diff
changeset
|
269 |
|
58618 | 270 |
subsection \<open>Facts and forward chaining \label{sec:proof-facts}\<close> |
26870 | 271 |
|
58618 | 272 |
text \<open> |
26870 | 273 |
\begin{matharray}{rcl} |
61493 | 274 |
@{command_def "note"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\ |
275 |
@{command_def "then"} & : & \<open>proof(state) \<rightarrow> proof(chain)\<close> \\ |
|
276 |
@{command_def "from"} & : & \<open>proof(state) \<rightarrow> proof(chain)\<close> \\ |
|
277 |
@{command_def "with"} & : & \<open>proof(state) \<rightarrow> proof(chain)\<close> \\ |
|
278 |
@{command_def "using"} & : & \<open>proof(prove) \<rightarrow> proof(prove)\<close> \\ |
|
279 |
@{command_def "unfolding"} & : & \<open>proof(prove) \<rightarrow> proof(prove)\<close> \\ |
|
26870 | 280 |
\end{matharray} |
281 |
||
282 |
New facts are established either by assumption or proof of local |
|
283 |
statements. Any fact will usually be involved in further proofs, |
|
284 |
either as explicit arguments of proof methods, or when forward |
|
285 |
chaining towards the next goal via @{command "then"} (and variants); |
|
286 |
@{command "from"} and @{command "with"} are composite forms |
|
287 |
involving @{command "note"}. The @{command "using"} elements |
|
61477 | 288 |
augments the collection of used facts \<^emph>\<open>after\<close> a goal has been |
26870 | 289 |
stated. Note that the special theorem name @{fact_ref this} refers |
61477 | 290 |
to the most recently established facts, but only \<^emph>\<open>before\<close> |
26870 | 291 |
issuing a follow-up claim. |
292 |
||
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
293 |
@{rail \<open> |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40965
diff
changeset
|
294 |
@@{command note} (@{syntax thmdef}? @{syntax thmrefs} + @'and') |
26870 | 295 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40965
diff
changeset
|
296 |
(@@{command from} | @@{command with} | @@{command using} | @@{command unfolding}) |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40965
diff
changeset
|
297 |
(@{syntax thmrefs} + @'and') |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
298 |
\<close>} |
26870 | 299 |
|
61493 | 300 |
\<^descr> @{command "note"}~\<open>a = b\<^sub>1 \<dots> b\<^sub>n\<close> recalls existing facts |
301 |
\<open>b\<^sub>1, \<dots>, b\<^sub>n\<close>, binding the result as \<open>a\<close>. Note that |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28757
diff
changeset
|
302 |
attributes may be involved as well, both on the left and right hand |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28757
diff
changeset
|
303 |
sides. |
26870 | 304 |
|
61439 | 305 |
\<^descr> @{command "then"} indicates forward chaining by the current |
26870 | 306 |
facts in order to establish the goal to be claimed next. The |
307 |
initial proof method invoked to refine that will be offered the |
|
308 |
facts to do ``anything appropriate'' (see also |
|
42626 | 309 |
\secref{sec:proof-steps}). For example, method @{method (Pure) rule} |
26870 | 310 |
(see \secref{sec:pure-meth-att}) would typically do an elimination |
311 |
rather than an introduction. Automatic methods usually insert the |
|
312 |
facts into the goal state before operation. This provides a simple |
|
313 |
scheme to control relevance of facts in automated proof search. |
|
60483 | 314 |
|
61493 | 315 |
\<^descr> @{command "from"}~\<open>b\<close> abbreviates ``@{command |
316 |
"note"}~\<open>b\<close>~@{command "then"}''; thus @{command "then"} is |
|
317 |
equivalent to ``@{command "from"}~\<open>this\<close>''. |
|
60483 | 318 |
|
61493 | 319 |
\<^descr> @{command "with"}~\<open>b\<^sub>1 \<dots> b\<^sub>n\<close> abbreviates ``@{command |
320 |
"from"}~\<open>b\<^sub>1 \<dots> b\<^sub>n \<AND> this\<close>''; thus the forward chaining |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28757
diff
changeset
|
321 |
is from earlier facts together with the current ones. |
60483 | 322 |
|
61493 | 323 |
\<^descr> @{command "using"}~\<open>b\<^sub>1 \<dots> b\<^sub>n\<close> augments the facts being |
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28757
diff
changeset
|
324 |
currently indicated for use by a subsequent refinement step (such as |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28757
diff
changeset
|
325 |
@{command_ref "apply"} or @{command_ref "proof"}). |
60483 | 326 |
|
61493 | 327 |
\<^descr> @{command "unfolding"}~\<open>b\<^sub>1 \<dots> b\<^sub>n\<close> is structurally |
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28757
diff
changeset
|
328 |
similar to @{command "using"}, but unfolds definitional equations |
61493 | 329 |
\<open>b\<^sub>1, \<dots> b\<^sub>n\<close> throughout the goal state and facts. |
26870 | 330 |
|
331 |
||
332 |
Forward chaining with an empty list of theorems is the same as not |
|
61493 | 333 |
chaining at all. Thus ``@{command "from"}~\<open>nothing\<close>'' has no |
334 |
effect apart from entering \<open>prove(chain)\<close> mode, since |
|
26870 | 335 |
@{fact_ref nothing} is bound to the empty list of theorems. |
336 |
||
42626 | 337 |
Basic proof methods (such as @{method_ref (Pure) rule}) expect multiple |
26870 | 338 |
facts to be given in their proper order, corresponding to a prefix |
339 |
of the premises of the rule involved. Note that positions may be |
|
61493 | 340 |
easily skipped using something like @{command "from"}~\<open>_ |
341 |
\<AND> a \<AND> b\<close>, for example. This involves the trivial rule |
|
342 |
\<open>PROP \<psi> \<Longrightarrow> PROP \<psi>\<close>, which is bound in Isabelle/Pure as |
|
26870 | 343 |
``@{fact_ref "_"}'' (underscore). |
344 |
||
345 |
Automated methods (such as @{method simp} or @{method auto}) just |
|
346 |
insert any given facts before their usual operation. Depending on |
|
347 |
the kind of procedure involved, the order of facts is less |
|
348 |
significant here. |
|
58618 | 349 |
\<close> |
26870 | 350 |
|
351 |
||
58618 | 352 |
subsection \<open>Goals \label{sec:goals}\<close> |
26870 | 353 |
|
58618 | 354 |
text \<open> |
26870 | 355 |
\begin{matharray}{rcl} |
61493 | 356 |
@{command_def "lemma"} & : & \<open>local_theory \<rightarrow> proof(prove)\<close> \\ |
357 |
@{command_def "theorem"} & : & \<open>local_theory \<rightarrow> proof(prove)\<close> \\ |
|
358 |
@{command_def "corollary"} & : & \<open>local_theory \<rightarrow> proof(prove)\<close> \\ |
|
359 |
@{command_def "proposition"} & : & \<open>local_theory \<rightarrow> proof(prove)\<close> \\ |
|
360 |
@{command_def "schematic_goal"} & : & \<open>local_theory \<rightarrow> proof(prove)\<close> \\ |
|
361 |
@{command_def "have"} & : & \<open>proof(state) | proof(chain) \<rightarrow> proof(prove)\<close> \\ |
|
362 |
@{command_def "show"} & : & \<open>proof(state) | proof(chain) \<rightarrow> proof(prove)\<close> \\ |
|
363 |
@{command_def "hence"} & : & \<open>proof(state) \<rightarrow> proof(prove)\<close> \\ |
|
364 |
@{command_def "thus"} & : & \<open>proof(state) \<rightarrow> proof(prove)\<close> \\ |
|
365 |
@{command_def "print_statement"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\ |
|
26870 | 366 |
\end{matharray} |
367 |
||
61338 | 368 |
From a theory context, proof mode is entered by an initial goal command |
369 |
such as @{command "lemma"}. Within a proof context, new claims may be |
|
370 |
introduced locally; there are variants to interact with the overall proof |
|
371 |
structure specifically, such as @{command have} or @{command show}. |
|
26870 | 372 |
|
373 |
Goals may consist of multiple statements, resulting in a list of |
|
374 |
facts eventually. A pending multi-goal is internally represented as |
|
61493 | 375 |
a meta-level conjunction (\<open>&&&\<close>), which is usually |
26870 | 376 |
split into the corresponding number of sub-goals prior to an initial |
377 |
method application, via @{command_ref "proof"} |
|
378 |
(\secref{sec:proof-steps}) or @{command_ref "apply"} |
|
379 |
(\secref{sec:tactic-commands}). The @{method_ref induct} method |
|
380 |
covered in \secref{sec:cases-induct} acts on multiple claims |
|
381 |
simultaneously. |
|
382 |
||
383 |
Claims at the theory level may be either in short or long form. A |
|
384 |
short goal merely consists of several simultaneous propositions |
|
385 |
(often just one). A long goal includes an explicit context |
|
386 |
specification for the subsequent conclusion, involving local |
|
387 |
parameters and assumptions. Here the role of each part of the |
|
388 |
statement is explicitly marked by separate keywords (see also |
|
389 |
\secref{sec:locale}); the local assumptions being introduced here |
|
390 |
are available as @{fact_ref assms} in the proof. Moreover, there |
|
391 |
are two kinds of conclusions: @{element_def "shows"} states several |
|
392 |
simultaneous propositions (essentially a big conjunction), while |
|
393 |
@{element_def "obtains"} claims several simultaneous simultaneous |
|
394 |
contexts of (essentially a big disjunction of eliminated parameters |
|
395 |
and assumptions, cf.\ \secref{sec:obtain}). |
|
396 |
||
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
397 |
@{rail \<open> |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40965
diff
changeset
|
398 |
(@@{command lemma} | @@{command theorem} | @@{command corollary} | |
61338 | 399 |
@@{command proposition} | @@{command schematic_goal}) (stmt | statement) |
26870 | 400 |
; |
60406 | 401 |
(@@{command have} | @@{command show} | @@{command hence} | @@{command thus}) |
60555
51a6997b1384
support 'when' statement, which corresponds to 'presume';
wenzelm
parents:
60484
diff
changeset
|
402 |
stmt cond_stmt @{syntax for_fixes} |
26870 | 403 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40965
diff
changeset
|
404 |
@@{command print_statement} @{syntax modes}? @{syntax thmrefs} |
26870 | 405 |
; |
60483 | 406 |
|
60406 | 407 |
stmt: (@{syntax props} + @'and') |
26870 | 408 |
; |
60555
51a6997b1384
support 'when' statement, which corresponds to 'presume';
wenzelm
parents:
60484
diff
changeset
|
409 |
cond_stmt: ((@'if' | @'when') stmt)? |
51a6997b1384
support 'when' statement, which corresponds to 'presume';
wenzelm
parents:
60484
diff
changeset
|
410 |
; |
59786 | 411 |
statement: @{syntax thmdecl}? (@{syntax_ref "includes"}?) (@{syntax context_elem} *) \<newline> |
412 |
conclusion |
|
26870 | 413 |
; |
60459 | 414 |
conclusion: @'shows' stmt | @'obtains' @{syntax obtain_clauses} |
26870 | 415 |
; |
60459 | 416 |
@{syntax_def obtain_clauses}: (@{syntax par_name}? obtain_case + '|') |
417 |
; |
|
418 |
@{syntax_def obtain_case}: (@{syntax vars} + @'and') @'where' |
|
419 |
(@{syntax thmdecl}? (@{syntax prop}+) + @'and') |
|
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
420 |
\<close>} |
26870 | 421 |
|
61493 | 422 |
\<^descr> @{command "lemma"}~\<open>a: \<phi>\<close> enters proof mode with |
423 |
\<open>\<phi>\<close> as main goal, eventually resulting in some fact \<open>\<turnstile> |
|
424 |
\<phi>\<close> to be put back into the target context. An additional @{syntax |
|
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40965
diff
changeset
|
425 |
context} specification may build up an initial proof context for the |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40965
diff
changeset
|
426 |
subsequent claim; this includes local definitions and syntax as |
47484 | 427 |
well, see also @{syntax "includes"} in \secref{sec:bundle} and |
428 |
@{syntax context_elem} in \secref{sec:locale}. |
|
60483 | 429 |
|
61439 | 430 |
\<^descr> @{command "theorem"}, @{command "corollary"}, and @{command |
61338 | 431 |
"proposition"} are the same as @{command "lemma"}. The different command |
432 |
names merely serve as a formal comment in the theory source. |
|
36320 | 433 |
|
61439 | 434 |
\<^descr> @{command "schematic_goal"} is similar to @{command "theorem"}, |
61337 | 435 |
but allows the statement to contain unbound schematic variables. |
36320 | 436 |
|
437 |
Under normal circumstances, an Isar proof text needs to specify |
|
438 |
claims explicitly. Schematic goals are more like goals in Prolog, |
|
439 |
where certain results are synthesized in the course of reasoning. |
|
440 |
With schematic statements, the inherent compositionality of Isar |
|
441 |
proofs is lost, which also impacts performance, because proof |
|
442 |
checking is forced into sequential mode. |
|
60483 | 443 |
|
61493 | 444 |
\<^descr> @{command "have"}~\<open>a: \<phi>\<close> claims a local goal, |
26870 | 445 |
eventually resulting in a fact within the current logical context. |
446 |
This operation is completely independent of any pending sub-goals of |
|
447 |
an enclosing goal statements, so @{command "have"} may be freely |
|
448 |
used for experimental exploration of potential results within a |
|
449 |
proof body. |
|
60483 | 450 |
|
61493 | 451 |
\<^descr> @{command "show"}~\<open>a: \<phi>\<close> is like @{command |
452 |
"have"}~\<open>a: \<phi>\<close> plus a second stage to refine some pending |
|
26870 | 453 |
sub-goal for each one of the finished result, after having been |
454 |
exported into the corresponding context (at the head of the |
|
455 |
sub-proof of this @{command "show"} command). |
|
60483 | 456 |
|
26870 | 457 |
To accommodate interactive debugging, resulting rules are printed |
458 |
before being applied internally. Even more, interactive execution |
|
459 |
of @{command "show"} predicts potential failure and displays the |
|
460 |
resulting error as a warning beforehand. Watch out for the |
|
461 |
following message: |
|
61408
9020a3ba6c9a
@{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents:
61338
diff
changeset
|
462 |
@{verbatim [display] \<open>Local statement fails to refine any pending goal\<close>} |
60483 | 463 |
|
61439 | 464 |
\<^descr> @{command "hence"} abbreviates ``@{command "then"}~@{command |
26870 | 465 |
"have"}'', i.e.\ claims a local goal to be proven by forward |
466 |
chaining the current facts. Note that @{command "hence"} is also |
|
61493 | 467 |
equivalent to ``@{command "from"}~\<open>this\<close>~@{command "have"}''. |
60483 | 468 |
|
61439 | 469 |
\<^descr> @{command "thus"} abbreviates ``@{command "then"}~@{command |
26870 | 470 |
"show"}''. Note that @{command "thus"} is also equivalent to |
61493 | 471 |
``@{command "from"}~\<open>this\<close>~@{command "show"}''. |
60483 | 472 |
|
61493 | 473 |
\<^descr> @{command "print_statement"}~\<open>a\<close> prints facts from the |
26870 | 474 |
current theory or proof context in long statement form, according to |
475 |
the syntax for @{command "lemma"} given above. |
|
476 |
||
477 |
||
478 |
Any goal statement causes some term abbreviations (such as |
|
479 |
@{variable_ref "?thesis"}) to be bound automatically, see also |
|
26922 | 480 |
\secref{sec:term-abbrev}. |
26870 | 481 |
|
60555
51a6997b1384
support 'when' statement, which corresponds to 'presume';
wenzelm
parents:
60484
diff
changeset
|
482 |
Structured goal statements involving @{keyword_ref "if"} or @{keyword_ref |
51a6997b1384
support 'when' statement, which corresponds to 'presume';
wenzelm
parents:
60484
diff
changeset
|
483 |
"when"} define the special fact @{fact_ref that} to refer to these |
51a6997b1384
support 'when' statement, which corresponds to 'presume';
wenzelm
parents:
60484
diff
changeset
|
484 |
assumptions in the proof body. The user may provide separate names |
51a6997b1384
support 'when' statement, which corresponds to 'presume';
wenzelm
parents:
60484
diff
changeset
|
485 |
according to the syntax of the statement. |
58618 | 486 |
\<close> |
26870 | 487 |
|
488 |
||
60483 | 489 |
section \<open>Calculational reasoning \label{sec:calculation}\<close> |
490 |
||
491 |
text \<open> |
|
492 |
\begin{matharray}{rcl} |
|
61493 | 493 |
@{command_def "also"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\ |
494 |
@{command_def "finally"} & : & \<open>proof(state) \<rightarrow> proof(chain)\<close> \\ |
|
495 |
@{command_def "moreover"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\ |
|
496 |
@{command_def "ultimately"} & : & \<open>proof(state) \<rightarrow> proof(chain)\<close> \\ |
|
497 |
@{command_def "print_trans_rules"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\ |
|
498 |
@{attribute trans} & : & \<open>attribute\<close> \\ |
|
499 |
@{attribute sym} & : & \<open>attribute\<close> \\ |
|
500 |
@{attribute symmetric} & : & \<open>attribute\<close> \\ |
|
60483 | 501 |
\end{matharray} |
502 |
||
503 |
Calculational proof is forward reasoning with implicit application |
|
61493 | 504 |
of transitivity rules (such those of \<open>=\<close>, \<open>\<le>\<close>, |
505 |
\<open><\<close>). Isabelle/Isar maintains an auxiliary fact register |
|
60483 | 506 |
@{fact_ref calculation} for accumulating results obtained by |
507 |
transitivity composed with the current result. Command @{command |
|
508 |
"also"} updates @{fact calculation} involving @{fact this}, while |
|
509 |
@{command "finally"} exhibits the final @{fact calculation} by |
|
510 |
forward chaining towards the next goal statement. Both commands |
|
511 |
require valid current facts, i.e.\ may occur only after commands |
|
512 |
that produce theorems such as @{command "assume"}, @{command |
|
513 |
"note"}, or some finished proof of @{command "have"}, @{command |
|
514 |
"show"} etc. The @{command "moreover"} and @{command "ultimately"} |
|
515 |
commands are similar to @{command "also"} and @{command "finally"}, |
|
516 |
but only collect further results in @{fact calculation} without |
|
517 |
applying any rules yet. |
|
518 |
||
61493 | 519 |
Also note that the implicit term abbreviation ``\<open>\<dots>\<close>'' has |
60483 | 520 |
its canonical application with calculational proofs. It refers to |
521 |
the argument of the preceding statement. (The argument of a curried |
|
522 |
infix expression happens to be its right-hand side.) |
|
523 |
||
524 |
Isabelle/Isar calculations are implicitly subject to block structure |
|
525 |
in the sense that new threads of calculational reasoning are |
|
526 |
commenced for any new block (as opened by a local goal, for |
|
527 |
example). This means that, apart from being able to nest |
|
61477 | 528 |
calculations, there is no separate \<^emph>\<open>begin-calculation\<close> command |
60483 | 529 |
required. |
530 |
||
61421 | 531 |
\<^medskip> |
532 |
The Isar calculation proof commands may be defined as |
|
60483 | 533 |
follows:\footnote{We suppress internal bookkeeping such as proper |
534 |
handling of block-structure.} |
|
535 |
||
536 |
\begin{matharray}{rcl} |
|
61493 | 537 |
@{command "also"}\<open>\<^sub>0\<close> & \equiv & @{command "note"}~\<open>calculation = this\<close> \\ |
538 |
@{command "also"}\<open>\<^sub>n+1\<close> & \equiv & @{command "note"}~\<open>calculation = trans [OF calculation this]\<close> \\[0.5ex] |
|
539 |
@{command "finally"} & \equiv & @{command "also"}~@{command "from"}~\<open>calculation\<close> \\[0.5ex] |
|
540 |
@{command "moreover"} & \equiv & @{command "note"}~\<open>calculation = calculation this\<close> \\ |
|
541 |
@{command "ultimately"} & \equiv & @{command "moreover"}~@{command "from"}~\<open>calculation\<close> \\ |
|
60483 | 542 |
\end{matharray} |
543 |
||
544 |
@{rail \<open> |
|
545 |
(@@{command also} | @@{command finally}) ('(' @{syntax thmrefs} ')')? |
|
546 |
; |
|
547 |
@@{attribute trans} (() | 'add' | 'del') |
|
548 |
\<close>} |
|
549 |
||
61493 | 550 |
\<^descr> @{command "also"}~\<open>(a\<^sub>1 \<dots> a\<^sub>n)\<close> maintains the auxiliary |
60483 | 551 |
@{fact calculation} register as follows. The first occurrence of |
552 |
@{command "also"} in some calculational thread initializes @{fact |
|
553 |
calculation} by @{fact this}. Any subsequent @{command "also"} on |
|
554 |
the same level of block-structure updates @{fact calculation} by |
|
555 |
some transitivity rule applied to @{fact calculation} and @{fact |
|
556 |
this} (in that order). Transitivity rules are picked from the |
|
557 |
current context, unless alternative rules are given as explicit |
|
558 |
arguments. |
|
559 |
||
61493 | 560 |
\<^descr> @{command "finally"}~\<open>(a\<^sub>1 \<dots> a\<^sub>n)\<close> maintaining @{fact |
60483 | 561 |
calculation} in the same way as @{command "also"}, and concludes the |
562 |
current calculational thread. The final result is exhibited as fact |
|
563 |
for forward chaining towards the next goal. Basically, @{command |
|
564 |
"finally"} just abbreviates @{command "also"}~@{command |
|
565 |
"from"}~@{fact calculation}. Typical idioms for concluding |
|
566 |
calculational proofs are ``@{command "finally"}~@{command |
|
61493 | 567 |
"show"}~\<open>?thesis\<close>~@{command "."}'' and ``@{command |
568 |
"finally"}~@{command "have"}~\<open>\<phi>\<close>~@{command "."}''. |
|
60483 | 569 |
|
61439 | 570 |
\<^descr> @{command "moreover"} and @{command "ultimately"} are |
60483 | 571 |
analogous to @{command "also"} and @{command "finally"}, but collect |
572 |
results only, without applying rules. |
|
573 |
||
61439 | 574 |
\<^descr> @{command "print_trans_rules"} prints the list of transitivity |
60483 | 575 |
rules (for calculational commands @{command "also"} and @{command |
576 |
"finally"}) and symmetry rules (for the @{attribute symmetric} |
|
577 |
operation and single step elimination patters) of the current |
|
578 |
context. |
|
579 |
||
61439 | 580 |
\<^descr> @{attribute trans} declares theorems as transitivity rules. |
60483 | 581 |
|
61439 | 582 |
\<^descr> @{attribute sym} declares symmetry rules, as well as |
61493 | 583 |
@{attribute "Pure.elim"}\<open>?\<close> rules. |
60483 | 584 |
|
61439 | 585 |
\<^descr> @{attribute symmetric} resolves a theorem with some rule |
60483 | 586 |
declared as @{attribute sym} in the current context. For example, |
61493 | 587 |
``@{command "assume"}~\<open>[symmetric]: x = y\<close>'' produces a |
60483 | 588 |
swapped fact derived from that assumption. |
589 |
||
590 |
In structured proof texts it is often more appropriate to use an |
|
591 |
explicit single-step elimination proof, such as ``@{command |
|
61493 | 592 |
"assume"}~\<open>x = y\<close>~@{command "then"}~@{command "have"}~\<open>y = x\<close>~@{command ".."}''. |
60483 | 593 |
\<close> |
594 |
||
595 |
||
58618 | 596 |
section \<open>Refinement steps\<close> |
28754
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
27141
diff
changeset
|
597 |
|
58618 | 598 |
subsection \<open>Proof method expressions \label{sec:proof-meth}\<close> |
28754
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
27141
diff
changeset
|
599 |
|
59660
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
58619
diff
changeset
|
600 |
text \<open>Proof methods are either basic ones, or expressions composed of |
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
58619
diff
changeset
|
601 |
methods via ``@{verbatim ","}'' (sequential composition), ``@{verbatim |
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
58619
diff
changeset
|
602 |
";"}'' (structural composition), ``@{verbatim "|"}'' (alternative |
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
58619
diff
changeset
|
603 |
choices), ``@{verbatim "?"}'' (try), ``@{verbatim "+"}'' (repeat at least |
61493 | 604 |
once), ``@{verbatim "["}\<open>n\<close>@{verbatim "]"}'' (restriction to first |
605 |
\<open>n\<close> subgoals). In practice, proof methods are usually just a comma |
|
59660
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
58619
diff
changeset
|
606 |
separated list of @{syntax nameref}~@{syntax args} specifications. Note |
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
58619
diff
changeset
|
607 |
that parentheses may be dropped for single method specifications (with no |
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
58619
diff
changeset
|
608 |
arguments). The syntactic precedence of method combinators is @{verbatim |
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
58619
diff
changeset
|
609 |
"|"} @{verbatim ";"} @{verbatim ","} @{verbatim "[]"} @{verbatim "+"} |
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
58619
diff
changeset
|
610 |
@{verbatim "?"} (from low to high). |
28754
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
27141
diff
changeset
|
611 |
|
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
612 |
@{rail \<open> |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40965
diff
changeset
|
613 |
@{syntax_def method}: |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40965
diff
changeset
|
614 |
(@{syntax nameref} | '(' methods ')') (() | '?' | '+' | '[' @{syntax nat}? ']') |
28754
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
27141
diff
changeset
|
615 |
; |
59660
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
58619
diff
changeset
|
616 |
methods: (@{syntax nameref} @{syntax args} | @{syntax method}) + (',' | ';' | '|') |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
617 |
\<close>} |
28754
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
27141
diff
changeset
|
618 |
|
61477 | 619 |
Regular Isar proof methods do \<^emph>\<open>not\<close> admit direct goal addressing, but |
59660
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
58619
diff
changeset
|
620 |
refer to the first subgoal or to all subgoals uniformly. Nonetheless, |
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
58619
diff
changeset
|
621 |
the subsequent mechanisms allow to imitate the effect of subgoal |
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
58619
diff
changeset
|
622 |
addressing that is known from ML tactics. |
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
58619
diff
changeset
|
623 |
|
61421 | 624 |
\<^medskip> |
61477 | 625 |
Goal \<^emph>\<open>restriction\<close> means the proof state is wrapped-up in a |
59660
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
58619
diff
changeset
|
626 |
way that certain subgoals are exposed, and other subgoals are ``parked'' |
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
58619
diff
changeset
|
627 |
elsewhere. Thus a proof method has no other chance than to operate on the |
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
58619
diff
changeset
|
628 |
subgoals that are presently exposed. |
28754
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
27141
diff
changeset
|
629 |
|
61493 | 630 |
Structural composition ``\<open>m\<^sub>1\<close>@{verbatim ";"}~\<open>m\<^sub>2\<close>'' means |
631 |
that method \<open>m\<^sub>1\<close> is applied with restriction to the first subgoal, |
|
632 |
then \<open>m\<^sub>2\<close> is applied consecutively with restriction to each subgoal |
|
633 |
that has newly emerged due to \<open>m\<^sub>1\<close>. This is analogous to the tactic |
|
59992 | 634 |
combinator @{ML_op THEN_ALL_NEW} in Isabelle/ML, see also @{cite |
61493 | 635 |
"isabelle-implementation"}. For example, \<open>(rule r; blast)\<close> applies |
636 |
rule \<open>r\<close> and then solves all new subgoals by \<open>blast\<close>. |
|
59660
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
58619
diff
changeset
|
637 |
|
61493 | 638 |
Moreover, the explicit goal restriction operator ``\<open>[n]\<close>'' exposes |
639 |
only the first \<open>n\<close> subgoals (which need to exist), with default |
|
640 |
\<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 |
|
641 |
applying rule \<open>r\<close> to the originally first one. |
|
59660
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
58619
diff
changeset
|
642 |
|
61421 | 643 |
\<^medskip> |
644 |
Improper methods, notably tactic emulations, offer low-level goal |
|
59660
49e498cedd02
support structural composition (THEN_ALL_NEW) for proof methods;
wenzelm
parents:
58619
diff
changeset
|
645 |
addressing as explicit argument to the individual tactic being involved. |
61493 | 646 |
Here ``\<open>[!]\<close>'' refers to all goals, and ``\<open>[n-]\<close>'' to all |
647 |
goals starting from \<open>n\<close>. |
|
28754
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
27141
diff
changeset
|
648 |
|
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
649 |
@{rail \<open> |
42705 | 650 |
@{syntax_def goal_spec}: |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40965
diff
changeset
|
651 |
'[' (@{syntax nat} '-' @{syntax nat} | @{syntax nat} '-' | @{syntax nat} | '!' ) ']' |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
652 |
\<close>} |
58618 | 653 |
\<close> |
28754
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
27141
diff
changeset
|
654 |
|
6f2e67a3dfaa
moved section "Proof method expressions" to proof chapter;
wenzelm
parents:
27141
diff
changeset
|
655 |
|
58618 | 656 |
subsection \<open>Initial and terminal proof steps \label{sec:proof-steps}\<close> |
26870 | 657 |
|
58618 | 658 |
text \<open> |
26870 | 659 |
\begin{matharray}{rcl} |
61493 | 660 |
@{command_def "proof"} & : & \<open>proof(prove) \<rightarrow> proof(state)\<close> \\ |
661 |
@{command_def "qed"} & : & \<open>proof(state) \<rightarrow> proof(state) | local_theory | theory\<close> \\ |
|
662 |
@{command_def "by"} & : & \<open>proof(prove) \<rightarrow> proof(state) | local_theory | theory\<close> \\ |
|
663 |
@{command_def ".."} & : & \<open>proof(prove) \<rightarrow> proof(state) | local_theory | theory\<close> \\ |
|
664 |
@{command_def "."} & : & \<open>proof(prove) \<rightarrow> proof(state) | local_theory | theory\<close> \\ |
|
665 |
@{command_def "sorry"} & : & \<open>proof(prove) \<rightarrow> proof(state) | local_theory | theory\<close> \\ |
|
666 |
@{method_def standard} & : & \<open>method\<close> \\ |
|
26870 | 667 |
\end{matharray} |
668 |
||
669 |
Arbitrary goal refinement via tactics is considered harmful. |
|
670 |
Structured proof composition in Isar admits proof methods to be |
|
671 |
invoked in two places only. |
|
672 |
||
61477 | 673 |
\<^enum> An \<^emph>\<open>initial\<close> refinement step @{command_ref |
61493 | 674 |
"proof"}~\<open>m\<^sub>1\<close> reduces a newly stated goal to a number |
26870 | 675 |
of sub-goals that are to be solved later. Facts are passed to |
61493 | 676 |
\<open>m\<^sub>1\<close> for forward chaining, if so indicated by \<open>proof(chain)\<close> mode. |
60483 | 677 |
|
61493 | 678 |
\<^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 |
679 |
passed to \<open>m\<^sub>2\<close>. |
|
26870 | 680 |
|
681 |
||
682 |
The only other (proper) way to affect pending goals in a proof body |
|
683 |
is by @{command_ref "show"}, which involves an explicit statement of |
|
684 |
what is to be solved eventually. Thus we avoid the fundamental |
|
685 |
problem of unstructured tactic scripts that consist of numerous |
|
686 |
consecutive goal transformations, with invisible effects. |
|
687 |
||
61421 | 688 |
\<^medskip> |
689 |
As a general rule of thumb for good proof style, initial |
|
26870 | 690 |
proof methods should either solve the goal completely, or constitute |
691 |
some well-understood reduction to new sub-goals. Arbitrary |
|
692 |
automatic proof tools that are prone leave a large number of badly |
|
693 |
structured sub-goals are no help in continuing the proof document in |
|
694 |
an intelligible manner. |
|
695 |
||
696 |
Unless given explicitly by the user, the default initial method is |
|
60618
4c79543cc376
renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents:
60578
diff
changeset
|
697 |
@{method standard}, which subsumes at least @{method_ref (Pure) rule} or |
4c79543cc376
renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents:
60578
diff
changeset
|
698 |
its classical variant @{method_ref (HOL) rule}. These methods apply a |
4c79543cc376
renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents:
60578
diff
changeset
|
699 |
single standard elimination or introduction rule according to the topmost |
4c79543cc376
renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents:
60578
diff
changeset
|
700 |
logical connective involved. There is no separate default terminal method. |
4c79543cc376
renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents:
60578
diff
changeset
|
701 |
Any remaining goals are always solved by assumption in the very last step. |
26870 | 702 |
|
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
703 |
@{rail \<open> |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40965
diff
changeset
|
704 |
@@{command proof} method? |
26870 | 705 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40965
diff
changeset
|
706 |
@@{command qed} method? |
26870 | 707 |
; |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
708 |
@@{command "by"} method method? |
26870 | 709 |
; |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
710 |
(@@{command "."} | @@{command ".."} | @@{command sorry}) |
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
711 |
\<close>} |
26870 | 712 |
|
61493 | 713 |
\<^descr> @{command "proof"}~\<open>m\<^sub>1\<close> refines the goal by proof |
714 |
method \<open>m\<^sub>1\<close>; facts for forward chaining are passed if so |
|
715 |
indicated by \<open>proof(chain)\<close> mode. |
|
60483 | 716 |
|
61493 | 717 |
\<^descr> @{command "qed"}~\<open>m\<^sub>2\<close> refines any remaining goals by |
718 |
proof method \<open>m\<^sub>2\<close> and concludes the sub-proof by assumption. |
|
719 |
If the goal had been \<open>show\<close> (or \<open>thus\<close>), some |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28757
diff
changeset
|
720 |
pending sub-goal is solved as well by the rule resulting from the |
61493 | 721 |
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 |
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28757
diff
changeset
|
722 |
resulting rule does not fit to any pending goal\footnote{This |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28757
diff
changeset
|
723 |
includes any additional ``strong'' assumptions as introduced by |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28757
diff
changeset
|
724 |
@{command "assume"}.} of the enclosing context. Debugging such a |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28757
diff
changeset
|
725 |
situation might involve temporarily changing @{command "show"} into |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28757
diff
changeset
|
726 |
@{command "have"}, or weakening the local context by replacing |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28757
diff
changeset
|
727 |
occurrences of @{command "assume"} by @{command "presume"}. |
60483 | 728 |
|
61493 | 729 |
\<^descr> @{command "by"}~\<open>m\<^sub>1 m\<^sub>2\<close> is a \<^emph>\<open>terminal |
61477 | 730 |
proof\<close>\index{proof!terminal}; it abbreviates @{command |
61493 | 731 |
"proof"}~\<open>m\<^sub>1\<close>~@{command "qed"}~\<open>m\<^sub>2\<close>, but with |
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28757
diff
changeset
|
732 |
backtracking across both methods. Debugging an unsuccessful |
61493 | 733 |
@{command "by"}~\<open>m\<^sub>1 m\<^sub>2\<close> command can be done by expanding its |
734 |
definition; in many cases @{command "proof"}~\<open>m\<^sub>1\<close> (or even |
|
735 |
\<open>apply\<close>~\<open>m\<^sub>1\<close>) is already sufficient to see the |
|
26870 | 736 |
problem. |
737 |
||
61477 | 738 |
\<^descr> ``@{command ".."}'' is a \<^emph>\<open>standard |
61493 | 739 |
proof\<close>\index{proof!standard}; it abbreviates @{command "by"}~\<open>standard\<close>. |
26870 | 740 |
|
61477 | 741 |
\<^descr> ``@{command "."}'' is a \<^emph>\<open>trivial |
61493 | 742 |
proof\<close>\index{proof!trivial}; it abbreviates @{command "by"}~\<open>this\<close>. |
60483 | 743 |
|
61477 | 744 |
\<^descr> @{command "sorry"} is a \<^emph>\<open>fake proof\<close>\index{proof!fake} |
26870 | 745 |
pretending to solve the pending claim without further ado. This |
52059 | 746 |
only works in interactive development, or if the @{attribute |
747 |
quick_and_dirty} is enabled. Facts emerging from fake |
|
50126
3dec88149176
theorem status about oracles/futures is no longer printed by default;
wenzelm
parents:
50109
diff
changeset
|
748 |
proofs are not the real thing. Internally, the derivation object is |
3dec88149176
theorem status about oracles/futures is no longer printed by default;
wenzelm
parents:
50109
diff
changeset
|
749 |
tainted by an oracle invocation, which may be inspected via the |
58552 | 750 |
theorem status @{cite "isabelle-implementation"}. |
60483 | 751 |
|
26870 | 752 |
The most important application of @{command "sorry"} is to support |
753 |
experimentation and top-down proof development. |
|
754 |
||
61439 | 755 |
\<^descr> @{method standard} refers to the default refinement step of some |
60618
4c79543cc376
renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents:
60578
diff
changeset
|
756 |
Isar language elements (notably @{command proof} and ``@{command ".."}''). |
61477 | 757 |
It is \<^emph>\<open>dynamically scoped\<close>, so the behaviour depends on the |
60618
4c79543cc376
renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents:
60578
diff
changeset
|
758 |
application environment. |
4c79543cc376
renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents:
60578
diff
changeset
|
759 |
|
4c79543cc376
renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents:
60578
diff
changeset
|
760 |
In Isabelle/Pure, @{method standard} performs elementary introduction~/ |
4c79543cc376
renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents:
60578
diff
changeset
|
761 |
elimination steps (@{method_ref (Pure) rule}), introduction of type |
4c79543cc376
renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents:
60578
diff
changeset
|
762 |
classes (@{method_ref intro_classes}) and locales (@{method_ref |
4c79543cc376
renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents:
60578
diff
changeset
|
763 |
intro_locales}). |
4c79543cc376
renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents:
60578
diff
changeset
|
764 |
|
4c79543cc376
renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents:
60578
diff
changeset
|
765 |
In Isabelle/HOL, @{method standard} also takes classical rules into |
4c79543cc376
renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents:
60578
diff
changeset
|
766 |
account (cf.\ \secref{sec:classical}). |
58618 | 767 |
\<close> |
26870 | 768 |
|
769 |
||
58618 | 770 |
subsection \<open>Fundamental methods and attributes \label{sec:pure-meth-att}\<close> |
26870 | 771 |
|
58618 | 772 |
text \<open> |
26870 | 773 |
The following proof methods and attributes refer to basic logical |
774 |
operations of Isar. Further methods and attributes are provided by |
|
775 |
several generic and object-logic specific tools and packages (see |
|
50109 | 776 |
\chref{ch:gen-tools} and \partref{part:hol}). |
26870 | 777 |
|
778 |
\begin{matharray}{rcl} |
|
61493 | 779 |
@{command_def "print_rules"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\[0.5ex] |
780 |
@{method_def "-"} & : & \<open>method\<close> \\ |
|
781 |
@{method_def "goal_cases"} & : & \<open>method\<close> \\ |
|
782 |
@{method_def "fact"} & : & \<open>method\<close> \\ |
|
783 |
@{method_def "assumption"} & : & \<open>method\<close> \\ |
|
784 |
@{method_def "this"} & : & \<open>method\<close> \\ |
|
785 |
@{method_def (Pure) "rule"} & : & \<open>method\<close> \\ |
|
786 |
@{attribute_def (Pure) "intro"} & : & \<open>attribute\<close> \\ |
|
787 |
@{attribute_def (Pure) "elim"} & : & \<open>attribute\<close> \\ |
|
788 |
@{attribute_def (Pure) "dest"} & : & \<open>attribute\<close> \\ |
|
789 |
@{attribute_def (Pure) "rule"} & : & \<open>attribute\<close> \\[0.5ex] |
|
790 |
@{attribute_def "OF"} & : & \<open>attribute\<close> \\ |
|
791 |
@{attribute_def "of"} & : & \<open>attribute\<close> \\ |
|
792 |
@{attribute_def "where"} & : & \<open>attribute\<close> \\ |
|
26870 | 793 |
\end{matharray} |
794 |
||
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
795 |
@{rail \<open> |
61166
5976fe402824
renamed method "goals" to "goal_cases" to emphasize its meaning;
wenzelm
parents:
61164
diff
changeset
|
796 |
@@{method goal_cases} (@{syntax name}*) |
60578 | 797 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40965
diff
changeset
|
798 |
@@{method fact} @{syntax thmrefs}? |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40965
diff
changeset
|
799 |
; |
42626 | 800 |
@@{method (Pure) rule} @{syntax thmrefs}? |
26870 | 801 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40965
diff
changeset
|
802 |
rulemod: ('intro' | 'elim' | 'dest') |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40965
diff
changeset
|
803 |
((('!' | () | '?') @{syntax nat}?) | 'del') ':' @{syntax thmrefs} |
26870 | 804 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40965
diff
changeset
|
805 |
(@@{attribute intro} | @@{attribute elim} | @@{attribute dest}) |
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40965
diff
changeset
|
806 |
('!' | () | '?') @{syntax nat}? |
26870 | 807 |
; |
42626 | 808 |
@@{attribute (Pure) rule} 'del' |
26870 | 809 |
; |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40965
diff
changeset
|
810 |
@@{attribute OF} @{syntax thmrefs} |
26870 | 811 |
; |
59785 | 812 |
@@{attribute of} @{syntax insts} ('concl' ':' @{syntax insts})? @{syntax for_fixes} |
26870 | 813 |
; |
59853 | 814 |
@@{attribute "where"} @{syntax named_insts} @{syntax for_fixes} |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
815 |
\<close>} |
26870 | 816 |
|
61439 | 817 |
\<^descr> @{command "print_rules"} prints rules declared via attributes |
51077 | 818 |
@{attribute (Pure) intro}, @{attribute (Pure) elim}, @{attribute |
819 |
(Pure) dest} of Isabelle/Pure. |
|
820 |
||
821 |
See also the analogous @{command "print_claset"} command for similar |
|
822 |
rule declarations of the classical reasoner |
|
823 |
(\secref{sec:classical}). |
|
824 |
||
61439 | 825 |
\<^descr> ``@{method "-"}'' (minus) inserts the forward chaining facts as |
60578 | 826 |
premises into the goal, and nothing else. |
827 |
||
828 |
Note that command @{command_ref "proof"} without any method actually |
|
829 |
performs a single reduction step using the @{method_ref (Pure) rule} |
|
61477 | 830 |
method; thus a plain \<^emph>\<open>do-nothing\<close> proof step would be ``@{command |
61493 | 831 |
"proof"}~\<open>-\<close>'' rather than @{command "proof"} alone. |
60578 | 832 |
|
61493 | 833 |
\<^descr> @{method "goal_cases"}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> turns the current subgoals |
61164 | 834 |
into cases within the context (see also \secref{sec:cases-induct}). The |
835 |
specified case names are used if present; otherwise cases are numbered |
|
836 |
starting from 1. |
|
60578 | 837 |
|
838 |
Invoking cases in the subsequent proof body via the @{command_ref case} |
|
839 |
command will @{command fix} goal parameters, @{command assume} goal |
|
840 |
premises, and @{command let} variable @{variable_ref ?case} refer to the |
|
841 |
conclusion. |
|
60483 | 842 |
|
61493 | 843 |
\<^descr> @{method "fact"}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> composes some fact from |
844 |
\<open>a\<^sub>1, \<dots>, a\<^sub>n\<close> (or implicitly from the current proof context) |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28757
diff
changeset
|
845 |
modulo unification of schematic type and term variables. The rule |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28757
diff
changeset
|
846 |
structure is not taken into account, i.e.\ meta-level implication is |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28757
diff
changeset
|
847 |
considered atomic. This is the same principle underlying literal |
61493 | 848 |
facts (cf.\ \secref{sec:syn-att}): ``@{command "have"}~\<open>\<phi>\<close>~@{command "by"}~\<open>fact\<close>'' is equivalent to ``@{command |
849 |
"note"}~@{verbatim "`"}\<open>\<phi>\<close>@{verbatim "`"}'' provided that |
|
850 |
\<open>\<turnstile> \<phi>\<close> is an instance of some known \<open>\<turnstile> \<phi>\<close> in the |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28757
diff
changeset
|
851 |
proof context. |
60483 | 852 |
|
61439 | 853 |
\<^descr> @{method assumption} solves some goal by a single assumption |
26870 | 854 |
step. All given facts are guaranteed to participate in the |
855 |
refinement; this means there may be only 0 or 1 in the first place. |
|
856 |
Recall that @{command "qed"} (\secref{sec:proof-steps}) already |
|
857 |
concludes any remaining sub-goals by assumption, so structured |
|
858 |
proofs usually need not quote the @{method assumption} method at |
|
859 |
all. |
|
60483 | 860 |
|
61439 | 861 |
\<^descr> @{method this} applies all of the current facts directly as |
26870 | 862 |
rules. Recall that ``@{command "."}'' (dot) abbreviates ``@{command |
61493 | 863 |
"by"}~\<open>this\<close>''. |
60483 | 864 |
|
61493 | 865 |
\<^descr> @{method (Pure) rule}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> applies some rule given as |
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28757
diff
changeset
|
866 |
argument in backward manner; facts are used to reduce the rule |
42626 | 867 |
before applying it to the goal. Thus @{method (Pure) rule} without facts |
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28757
diff
changeset
|
868 |
is plain introduction, while with facts it becomes elimination. |
60483 | 869 |
|
60618
4c79543cc376
renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents:
60578
diff
changeset
|
870 |
When no arguments are given, the @{method (Pure) rule} method tries to |
4c79543cc376
renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents:
60578
diff
changeset
|
871 |
pick appropriate rules automatically, as declared in the current context |
4c79543cc376
renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents:
60578
diff
changeset
|
872 |
using the @{attribute (Pure) intro}, @{attribute (Pure) elim}, @{attribute |
4c79543cc376
renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents:
60578
diff
changeset
|
873 |
(Pure) dest} attributes (see below). This is included in the standard |
4c79543cc376
renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents:
60578
diff
changeset
|
874 |
behaviour of @{command "proof"} and ``@{command ".."}'' (double-dot) steps |
4c79543cc376
renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents:
60578
diff
changeset
|
875 |
(see \secref{sec:proof-steps}). |
60483 | 876 |
|
61439 | 877 |
\<^descr> @{attribute (Pure) intro}, @{attribute (Pure) elim}, and |
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28757
diff
changeset
|
878 |
@{attribute (Pure) dest} declare introduction, elimination, and |
42626 | 879 |
destruct rules, to be used with method @{method (Pure) rule}, and similar |
30169 | 880 |
tools. Note that the latter will ignore rules declared with |
61493 | 881 |
``\<open>?\<close>'', while ``\<open>!\<close>'' are used most aggressively. |
60483 | 882 |
|
26870 | 883 |
The classical reasoner (see \secref{sec:classical}) introduces its |
884 |
own variants of these attributes; use qualified names to access the |
|
26901 | 885 |
present versions of Isabelle/Pure, i.e.\ @{attribute (Pure) |
886 |
"Pure.intro"}. |
|
60483 | 887 |
|
61493 | 888 |
\<^descr> @{attribute (Pure) rule}~\<open>del\<close> undeclares introduction, |
26870 | 889 |
elimination, or destruct rules. |
51077 | 890 |
|
61493 | 891 |
\<^descr> @{attribute OF}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> applies some theorem to all |
892 |
of the given rules \<open>a\<^sub>1, \<dots>, a\<^sub>n\<close> in canonical right-to-left |
|
893 |
order, which means that premises stemming from the \<open>a\<^sub>i\<close> |
|
47498 | 894 |
emerge in parallel in the result, without interfering with each |
61493 | 895 |
other. In many practical situations, the \<open>a\<^sub>i\<close> do not have |
896 |
premises themselves, so \<open>rule [OF a\<^sub>1 \<dots> a\<^sub>n]\<close> can be actually |
|
47498 | 897 |
read as functional application (modulo unification). |
898 |
||
61493 | 899 |
Argument positions may be effectively skipped by using ``\<open>_\<close>'' |
47498 | 900 |
(underscore), which refers to the propositional identity rule in the |
901 |
Pure theory. |
|
60483 | 902 |
|
61493 | 903 |
\<^descr> @{attribute of}~\<open>t\<^sub>1 \<dots> t\<^sub>n\<close> performs positional |
904 |
instantiation of term variables. The terms \<open>t\<^sub>1, \<dots>, t\<^sub>n\<close> are |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28757
diff
changeset
|
905 |
substituted for any schematic variables occurring in a theorem from |
61493 | 906 |
left to right; ``\<open>_\<close>'' (underscore) indicates to skip a |
907 |
position. Arguments following a ``\<open>concl:\<close>'' specification |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28757
diff
changeset
|
908 |
refer to positions of the conclusion of a rule. |
55143
04448228381d
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
55112
diff
changeset
|
909 |
|
61493 | 910 |
An optional context of local variables \<open>\<FOR> x\<^sub>1 \<dots> x\<^sub>m\<close> may |
55143
04448228381d
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
55112
diff
changeset
|
911 |
be specified: the instantiated theorem is exported, and these |
04448228381d
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
55112
diff
changeset
|
912 |
variables become schematic (usually with some shifting of indices). |
60483 | 913 |
|
61493 | 914 |
\<^descr> @{attribute "where"}~\<open>x\<^sub>1 = t\<^sub>1 \<AND> \<dots> x\<^sub>n = t\<^sub>n\<close> |
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28757
diff
changeset
|
915 |
performs named instantiation of schematic type and term variables |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28757
diff
changeset
|
916 |
occurring in a theorem. Schematic variables have to be specified on |
61493 | 917 |
the left-hand side (e.g.\ \<open>?x1.3\<close>). The question mark may |
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28757
diff
changeset
|
918 |
be omitted if the variable name is a plain identifier without index. |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28757
diff
changeset
|
919 |
As type instantiations are inferred from term instantiations, |
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
28757
diff
changeset
|
920 |
explicit type instantiations are seldom necessary. |
26870 | 921 |
|
61493 | 922 |
An optional context of local variables \<open>\<FOR> x\<^sub>1 \<dots> x\<^sub>m\<close> may |
55143
04448228381d
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
55112
diff
changeset
|
923 |
be specified as for @{attribute "of"} above. |
58618 | 924 |
\<close> |
26870 | 925 |
|
926 |
||
58618 | 927 |
subsection \<open>Defining proof methods\<close> |
28757 | 928 |
|
58618 | 929 |
text \<open> |
28757 | 930 |
\begin{matharray}{rcl} |
61493 | 931 |
@{command_def "method_setup"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\ |
28757 | 932 |
\end{matharray} |
933 |
||
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
934 |
@{rail \<open> |
59783
00b62aa9f430
tuned syntax diagrams -- no duplication of "target";
wenzelm
parents:
59660
diff
changeset
|
935 |
@@{command method_setup} @{syntax name} '=' @{syntax text} @{syntax text}? |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
936 |
\<close>} |
28757 | 937 |
|
61493 | 938 |
\<^descr> @{command "method_setup"}~\<open>name = text description\<close> |
939 |
defines a proof method in the current context. The given \<open>text\<close> has to be an ML expression of type |
|
30547 | 940 |
@{ML_type "(Proof.context -> Proof.method) context_parser"}, cf.\ |
55837 | 941 |
basic parsers defined in structure @{ML_structure Args} and @{ML_structure |
30547 | 942 |
Attrib}. There are also combinators like @{ML METHOD} and @{ML |
943 |
SIMPLE_METHOD} to turn certain tactic forms into official proof |
|
944 |
methods; the primed versions refer to tactics with explicit goal |
|
945 |
addressing. |
|
28757 | 946 |
|
30547 | 947 |
Here are some example method definitions: |
58618 | 948 |
\<close> |
28757 | 949 |
|
59905 | 950 |
(*<*)experiment begin(*>*) |
58619 | 951 |
method_setup my_method1 = |
952 |
\<open>Scan.succeed (K (SIMPLE_METHOD' (fn i: int => no_tac)))\<close> |
|
953 |
"my first method (without any arguments)" |
|
30547 | 954 |
|
58619 | 955 |
method_setup my_method2 = |
956 |
\<open>Scan.succeed (fn ctxt: Proof.context => |
|
957 |
SIMPLE_METHOD' (fn i: int => no_tac))\<close> |
|
958 |
"my second method (with context)" |
|
30547 | 959 |
|
58619 | 960 |
method_setup my_method3 = |
961 |
\<open>Attrib.thms >> (fn thms: thm list => fn ctxt: Proof.context => |
|
962 |
SIMPLE_METHOD' (fn i: int => no_tac))\<close> |
|
963 |
"my third method (with theorem arguments and context)" |
|
59905 | 964 |
(*<*)end(*>*) |
30547 | 965 |
|
28757 | 966 |
|
60483 | 967 |
section \<open>Proof by cases and induction \label{sec:cases-induct}\<close> |
968 |
||
969 |
subsection \<open>Rule contexts\<close> |
|
970 |
||
971 |
text \<open> |
|
972 |
\begin{matharray}{rcl} |
|
61493 | 973 |
@{command_def "case"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\ |
974 |
@{command_def "print_cases"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\ |
|
975 |
@{attribute_def case_names} & : & \<open>attribute\<close> \\ |
|
976 |
@{attribute_def case_conclusion} & : & \<open>attribute\<close> \\ |
|
977 |
@{attribute_def params} & : & \<open>attribute\<close> \\ |
|
978 |
@{attribute_def consumes} & : & \<open>attribute\<close> \\ |
|
60483 | 979 |
\end{matharray} |
980 |
||
981 |
The puristic way to build up Isar proof contexts is by explicit |
|
982 |
language elements like @{command "fix"}, @{command "assume"}, |
|
983 |
@{command "let"} (see \secref{sec:proof-context}). This is adequate |
|
984 |
for plain natural deduction, but easily becomes unwieldy in concrete |
|
985 |
verification tasks, which typically involve big induction rules with |
|
986 |
several cases. |
|
987 |
||
988 |
The @{command "case"} command provides a shorthand to refer to a |
|
989 |
local context symbolically: certain proof methods provide an |
|
61493 | 990 |
environment of named ``cases'' of the form \<open>c: x\<^sub>1, \<dots>, |
991 |
x\<^sub>m, \<phi>\<^sub>1, \<dots>, \<phi>\<^sub>n\<close>; the effect of ``@{command |
|
992 |
"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> |
|
993 |
\<phi>\<^sub>n\<close>''. Term bindings may be covered as well, notably |
|
60483 | 994 |
@{variable ?case} for the main conclusion. |
995 |
||
61493 | 996 |
By default, the ``terminology'' \<open>x\<^sub>1, \<dots>, x\<^sub>m\<close> of |
60483 | 997 |
a case value is marked as hidden, i.e.\ there is no way to refer to |
998 |
such parameters in the subsequent proof text. After all, original |
|
999 |
rule parameters stem from somewhere outside of the current proof |
|
61493 | 1000 |
text. By using the explicit form ``@{command "case"}~\<open>(c |
1001 |
y\<^sub>1 \<dots> y\<^sub>m)\<close>'' instead, the proof author is able to |
|
60483 | 1002 |
chose local names that fit nicely into the current context. |
1003 |
||
61421 | 1004 |
\<^medskip> |
1005 |
It is important to note that proper use of @{command |
|
60483 | 1006 |
"case"} does not provide means to peek at the current goal state, |
1007 |
which is not directly observable in Isar! Nonetheless, goal |
|
61493 | 1008 |
refinement commands do provide named cases \<open>goal\<^sub>i\<close> |
1009 |
for each subgoal \<open>i = 1, \<dots>, n\<close> of the resulting goal state. |
|
60483 | 1010 |
Using this extra feature requires great care, because some bits of |
1011 |
the internal tactical machinery intrude the proof text. In |
|
1012 |
particular, parameter names stemming from the left-over of automated |
|
1013 |
reasoning tools are usually quite unpredictable. |
|
1014 |
||
1015 |
Under normal circumstances, the text of cases emerge from standard |
|
1016 |
elimination or induction rules, which in turn are derived from |
|
1017 |
previous theory specifications in a canonical way (say from |
|
1018 |
@{command "inductive"} definitions). |
|
1019 |
||
61421 | 1020 |
\<^medskip> |
1021 |
Proper cases are only available if both the proof method |
|
60483 | 1022 |
and the rules involved support this. By using appropriate |
1023 |
attributes, case names, conclusions, and parameters may be also |
|
1024 |
declared by hand. Thus variant versions of rules that have been |
|
1025 |
derived manually become ready to use in advanced case analysis |
|
1026 |
later. |
|
1027 |
||
1028 |
@{rail \<open> |
|
60565 | 1029 |
@@{command case} @{syntax thmdecl}? (nameref | '(' nameref (('_' | @{syntax name}) *) ')') |
60483 | 1030 |
; |
1031 |
@@{attribute case_names} ((@{syntax name} ( '[' (('_' | @{syntax name}) +) ']' ) ? ) +) |
|
1032 |
; |
|
1033 |
@@{attribute case_conclusion} @{syntax name} (@{syntax name} * ) |
|
1034 |
; |
|
1035 |
@@{attribute params} ((@{syntax name} * ) + @'and') |
|
1036 |
; |
|
1037 |
@@{attribute consumes} @{syntax int}? |
|
1038 |
\<close>} |
|
1039 |
||
61493 | 1040 |
\<^descr> @{command "case"}~\<open>a: (c x\<^sub>1 \<dots> x\<^sub>m)\<close> invokes a named local |
1041 |
context \<open>c: x\<^sub>1, \<dots>, x\<^sub>m, \<phi>\<^sub>1, \<dots>, \<phi>\<^sub>m\<close>, as provided by an |
|
60565 | 1042 |
appropriate proof method (such as @{method_ref cases} and @{method_ref |
61493 | 1043 |
induct}). The command ``@{command "case"}~\<open>a: (c x\<^sub>1 \<dots> x\<^sub>m)\<close>'' |
1044 |
abbreviates ``@{command "fix"}~\<open>x\<^sub>1 \<dots> x\<^sub>m\<close>~@{command |
|
1045 |
"assume"}~\<open>a.c: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close>''. Each local fact is qualified by the |
|
1046 |
prefix \<open>a\<close>, and all such facts are collectively bound to the name |
|
1047 |
\<open>a\<close>. |
|
60565 | 1048 |
|
61493 | 1049 |
The fact name is specification \<open>a\<close> is optional, the default is to |
1050 |
re-use \<open>c\<close>. So @{command "case"}~\<open>(c x\<^sub>1 \<dots> x\<^sub>m)\<close> is the same |
|
1051 |
as @{command "case"}~\<open>c: (c x\<^sub>1 \<dots> x\<^sub>m)\<close>. |
|
60483 | 1052 |
|
61439 | 1053 |
\<^descr> @{command "print_cases"} prints all local contexts of the |
60483 | 1054 |
current state, using Isar proof language notation. |
1055 |
||
61493 | 1056 |
\<^descr> @{attribute case_names}~\<open>c\<^sub>1 \<dots> c\<^sub>k\<close> declares names for |
1057 |
the local contexts of premises of a theorem; \<open>c\<^sub>1, \<dots>, c\<^sub>k\<close> |
|
61477 | 1058 |
refers to the \<^emph>\<open>prefix\<close> of the list of premises. Each of the |
61493 | 1059 |
cases \<open>c\<^sub>i\<close> can be of the form \<open>c[h\<^sub>1 \<dots> h\<^sub>n]\<close> where |
1060 |
the \<open>h\<^sub>1 \<dots> h\<^sub>n\<close> are the names of the hypotheses in case \<open>c\<^sub>i\<close> |
|
60483 | 1061 |
from left to right. |
1062 |
||
61493 | 1063 |
\<^descr> @{attribute case_conclusion}~\<open>c d\<^sub>1 \<dots> d\<^sub>k\<close> declares |
1064 |
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 |
|
1065 |
built by nesting a binary connective (e.g.\ \<open>\<or>\<close>). |
|
60483 | 1066 |
|
1067 |
Note that proof methods such as @{method induct} and @{method |
|
1068 |
coinduct} already provide a default name for the conclusion as a |
|
1069 |
whole. The need to name subformulas only arises with cases that |
|
1070 |
split into several sub-cases, as in common co-induction rules. |
|
1071 |
||
61493 | 1072 |
\<^descr> @{attribute params}~\<open>p\<^sub>1 \<dots> p\<^sub>m \<AND> \<dots> q\<^sub>1 \<dots> q\<^sub>n\<close> renames |
1073 |
the innermost parameters of premises \<open>1, \<dots>, n\<close> of some |
|
60483 | 1074 |
theorem. An empty list of names may be given to skip positions, |
1075 |
leaving the present parameters unchanged. |
|
1076 |
||
61477 | 1077 |
Note that the default usage of case rules does \<^emph>\<open>not\<close> directly |
60483 | 1078 |
expose parameters to the proof context. |
1079 |
||
61493 | 1080 |
\<^descr> @{attribute consumes}~\<open>n\<close> declares the number of ``major |
60483 | 1081 |
premises'' of a rule, i.e.\ the number of facts to be consumed when |
1082 |
it is applied by an appropriate proof method. The default value of |
|
61493 | 1083 |
@{attribute consumes} is \<open>n = 1\<close>, which is appropriate for |
60483 | 1084 |
the usual kind of cases and induction rules for inductive sets (cf.\ |
1085 |
\secref{sec:hol-inductive}). Rules without any @{attribute |
|
1086 |
consumes} declaration given are treated as if @{attribute |
|
61493 | 1087 |
consumes}~\<open>0\<close> had been specified. |
60483 | 1088 |
|
61493 | 1089 |
A negative \<open>n\<close> is interpreted relatively to the total number |
60483 | 1090 |
of premises of the rule in the target context. Thus its absolute |
1091 |
value specifies the remaining number of premises, after subtracting |
|
1092 |
the prefix of major premises as indicated above. This form of |
|
1093 |
declaration has the technical advantage of being stable under more |
|
1094 |
morphisms, notably those that export the result from a nested |
|
1095 |
@{command_ref context} with additional assumptions. |
|
1096 |
||
1097 |
Note that explicit @{attribute consumes} declarations are only |
|
1098 |
rarely needed; this is already taken care of automatically by the |
|
1099 |
higher-level @{attribute cases}, @{attribute induct}, and |
|
1100 |
@{attribute coinduct} declarations. |
|
1101 |
\<close> |
|
1102 |
||
1103 |
||
1104 |
subsection \<open>Proof methods\<close> |
|
1105 |
||
1106 |
text \<open> |
|
1107 |
\begin{matharray}{rcl} |
|
61493 | 1108 |
@{method_def cases} & : & \<open>method\<close> \\ |
1109 |
@{method_def induct} & : & \<open>method\<close> \\ |
|
1110 |
@{method_def induction} & : & \<open>method\<close> \\ |
|
1111 |
@{method_def coinduct} & : & \<open>method\<close> \\ |
|
60483 | 1112 |
\end{matharray} |
1113 |
||
1114 |
The @{method cases}, @{method induct}, @{method induction}, |
|
1115 |
and @{method coinduct} |
|
1116 |
methods provide a uniform interface to common proof techniques over |
|
1117 |
datatypes, inductive predicates (or sets), recursive functions etc. |
|
1118 |
The corresponding rules may be specified and instantiated in a |
|
1119 |
casual manner. Furthermore, these methods provide named local |
|
1120 |
contexts that may be invoked via the @{command "case"} proof command |
|
1121 |
within the subsequent proof text. This accommodates compact proof |
|
1122 |
texts even when reasoning about large specifications. |
|
1123 |
||
1124 |
The @{method induct} method also provides some additional |
|
1125 |
infrastructure in order to be applicable to structure statements |
|
1126 |
(either using explicit meta-level connectives, or including facts |
|
1127 |
and parameters separately). This avoids cumbersome encoding of |
|
1128 |
``strengthened'' inductive statements within the object-logic. |
|
1129 |
||
1130 |
Method @{method induction} differs from @{method induct} only in |
|
1131 |
the names of the facts in the local context invoked by the @{command "case"} |
|
1132 |
command. |
|
1133 |
||
1134 |
@{rail \<open> |
|
1135 |
@@{method cases} ('(' 'no_simp' ')')? \<newline> |
|
1136 |
(@{syntax insts} * @'and') rule? |
|
1137 |
; |
|
1138 |
(@@{method induct} | @@{method induction}) |
|
1139 |
('(' 'no_simp' ')')? (definsts * @'and') \<newline> arbitrary? taking? rule? |
|
1140 |
; |
|
1141 |
@@{method coinduct} @{syntax insts} taking rule? |
|
1142 |
; |
|
1143 |
||
1144 |
rule: ('type' | 'pred' | 'set') ':' (@{syntax nameref} +) | 'rule' ':' (@{syntax thmref} +) |
|
1145 |
; |
|
1146 |
definst: @{syntax name} ('==' | '\<equiv>') @{syntax term} | '(' @{syntax term} ')' | @{syntax inst} |
|
1147 |
; |
|
1148 |
definsts: ( definst * ) |
|
1149 |
; |
|
1150 |
arbitrary: 'arbitrary' ':' ((@{syntax term} * ) @'and' +) |
|
1151 |
; |
|
1152 |
taking: 'taking' ':' @{syntax insts} |
|
1153 |
\<close>} |
|
1154 |
||
61493 | 1155 |
\<^descr> @{method cases}~\<open>insts R\<close> applies method @{method |
60483 | 1156 |
rule} with an appropriate case distinction theorem, instantiated to |
61493 | 1157 |
the subjects \<open>insts\<close>. Symbolic case names are bound according |
60483 | 1158 |
to the rule's local contexts. |
1159 |
||
1160 |
The rule is determined as follows, according to the facts and |
|
1161 |
arguments passed to the @{method cases} method: |
|
1162 |
||
61421 | 1163 |
\<^medskip> |
60483 | 1164 |
\begin{tabular}{llll} |
1165 |
facts & & arguments & rule \\\hline |
|
61493 | 1166 |
\<open>\<turnstile> R\<close> & @{method cases} & & implicit rule \<open>R\<close> \\ |
60483 | 1167 |
& @{method cases} & & classical case split \\ |
61493 | 1168 |
& @{method cases} & \<open>t\<close> & datatype exhaustion (type of \<open>t\<close>) \\ |
1169 |
\<open>\<turnstile> A t\<close> & @{method cases} & \<open>\<dots>\<close> & inductive predicate/set elimination (of \<open>A\<close>) \\ |
|
1170 |
\<open>\<dots>\<close> & @{method cases} & \<open>\<dots> rule: R\<close> & explicit rule \<open>R\<close> \\ |
|
60483 | 1171 |
\end{tabular} |
61421 | 1172 |
\<^medskip> |
60483 | 1173 |
|
61477 | 1174 |
Several instantiations may be given, referring to the \<^emph>\<open>suffix\<close> |
1175 |
of premises of the case rule; within each premise, the \<^emph>\<open>prefix\<close> |
|
60483 | 1176 |
of variables is instantiated. In most situations, only a single |
1177 |
term needs to be specified; this refers to the first variable of the |
|
61493 | 1178 |
last premise (it is usually the same for all cases). The \<open>(no_simp)\<close> option can be used to disable pre-simplification of |
60483 | 1179 |
cases (see the description of @{method induct} below for details). |
1180 |
||
61493 | 1181 |
\<^descr> @{method induct}~\<open>insts R\<close> and |
1182 |
@{method induction}~\<open>insts R\<close> are analogous to the |
|
60483 | 1183 |
@{method cases} method, but refer to induction rules, which are |
1184 |
determined as follows: |
|
1185 |
||
61421 | 1186 |
\<^medskip> |
60483 | 1187 |
\begin{tabular}{llll} |
1188 |
facts & & arguments & rule \\\hline |
|
61493 | 1189 |
& @{method induct} & \<open>P x\<close> & datatype induction (type of \<open>x\<close>) \\ |
1190 |
\<open>\<turnstile> A x\<close> & @{method induct} & \<open>\<dots>\<close> & predicate/set induction (of \<open>A\<close>) \\ |
|
1191 |
\<open>\<dots>\<close> & @{method induct} & \<open>\<dots> rule: R\<close> & explicit rule \<open>R\<close> \\ |
|
60483 | 1192 |
\end{tabular} |
61421 | 1193 |
\<^medskip> |
60483 | 1194 |
|
1195 |
Several instantiations may be given, each referring to some part of |
|
1196 |
a mutual inductive definition or datatype --- only related partial |
|
1197 |
induction rules may be used together, though. Any of the lists of |
|
61493 | 1198 |
terms \<open>P, x, \<dots>\<close> refers to the \<^emph>\<open>suffix\<close> of variables |
60483 | 1199 |
present in the induction rule. This enables the writer to specify |
1200 |
only induction variables, or both predicates and variables, for |
|
1201 |
example. |
|
1202 |
||
61493 | 1203 |
Instantiations may be definitional: equations \<open>x \<equiv> t\<close> |
60483 | 1204 |
introduce local definitions, which are inserted into the claim and |
1205 |
discharged after applying the induction rule. Equalities reappear |
|
1206 |
in the inductive cases, but have been transformed according to the |
|
1207 |
induction principle being involved here. In order to achieve |
|
1208 |
practically useful induction hypotheses, some variables occurring in |
|
61493 | 1209 |
\<open>t\<close> need to be fixed (see below). Instantiations of the form |
1210 |
\<open>t\<close>, where \<open>t\<close> is not a variable, are taken as a |
|
1211 |
shorthand for \mbox{\<open>x \<equiv> t\<close>}, where \<open>x\<close> is a fresh |
|
1212 |
variable. If this is not intended, \<open>t\<close> has to be enclosed in |
|
60483 | 1213 |
parentheses. By default, the equalities generated by definitional |
1214 |
instantiations are pre-simplified using a specific set of rules, |
|
1215 |
usually consisting of distinctness and injectivity theorems for |
|
1216 |
datatypes. This pre-simplification may cause some of the parameters |
|
1217 |
of an inductive case to disappear, or may even completely delete |
|
1218 |
some of the inductive cases, if one of the equalities occurring in |
|
61493 | 1219 |
their premises can be simplified to \<open>False\<close>. The \<open>(no_simp)\<close> option can be used to disable pre-simplification. |
60483 | 1220 |
Additional rules to be used in pre-simplification can be declared |
1221 |
using the @{attribute_def induct_simp} attribute. |
|
1222 |
||
61493 | 1223 |
The optional ``\<open>arbitrary: x\<^sub>1 \<dots> x\<^sub>m\<close>'' |
1224 |
specification generalizes variables \<open>x\<^sub>1, \<dots>, |
|
1225 |
x\<^sub>m\<close> of the original goal before applying induction. One can |
|
1226 |
separate variables by ``\<open>and\<close>'' to generalize them in other |
|
60483 | 1227 |
goals then the first. Thus induction hypotheses may become |
1228 |
sufficiently general to get the proof through. Together with |
|
1229 |
definitional instantiations, one may effectively perform induction |
|
1230 |
over expressions of a certain structure. |
|
1231 |
||
61493 | 1232 |
The optional ``\<open>taking: t\<^sub>1 \<dots> t\<^sub>n\<close>'' |
60483 | 1233 |
specification provides additional instantiations of a prefix of |
1234 |
pending variables in the rule. Such schematic induction rules |
|
1235 |
rarely occur in practice, though. |
|
1236 |
||
61493 | 1237 |
\<^descr> @{method coinduct}~\<open>inst R\<close> is analogous to the |
60483 | 1238 |
@{method induct} method, but refers to coinduction rules, which are |
1239 |
determined as follows: |
|
1240 |
||
61421 | 1241 |
\<^medskip> |
60483 | 1242 |
\begin{tabular}{llll} |
1243 |
goal & & arguments & rule \\\hline |
|
61493 | 1244 |
& @{method coinduct} & \<open>x\<close> & type coinduction (type of \<open>x\<close>) \\ |
1245 |
\<open>A x\<close> & @{method coinduct} & \<open>\<dots>\<close> & predicate/set coinduction (of \<open>A\<close>) \\ |
|
1246 |
\<open>\<dots>\<close> & @{method coinduct} & \<open>\<dots> rule: R\<close> & explicit rule \<open>R\<close> \\ |
|
60483 | 1247 |
\end{tabular} |
61421 | 1248 |
\<^medskip> |
60483 | 1249 |
|
1250 |
Coinduction is the dual of induction. Induction essentially |
|
61493 | 1251 |
eliminates \<open>A x\<close> towards a generic result \<open>P x\<close>, |
1252 |
while coinduction introduces \<open>A x\<close> starting with \<open>B |
|
1253 |
x\<close>, for a suitable ``bisimulation'' \<open>B\<close>. The cases of a |
|
60483 | 1254 |
coinduct rule are typically named after the predicates or sets being |
1255 |
covered, while the conclusions consist of several alternatives being |
|
1256 |
named after the individual destructor patterns. |
|
1257 |
||
61477 | 1258 |
The given instantiation refers to the \<^emph>\<open>suffix\<close> of variables |
60483 | 1259 |
occurring in the rule's major premise, or conclusion if unavailable. |
61493 | 1260 |
An additional ``\<open>taking: t\<^sub>1 \<dots> t\<^sub>n\<close>'' |
60483 | 1261 |
specification may be required in order to specify the bisimulation |
1262 |
to be used in the coinduction step. |
|
1263 |
||
1264 |
||
1265 |
Above methods produce named local contexts, as determined by the |
|
1266 |
instantiated rule as given in the text. Beyond that, the @{method |
|
1267 |
induct} and @{method coinduct} methods guess further instantiations |
|
1268 |
from the goal specification itself. Any persisting unresolved |
|
1269 |
schematic variables of the resulting rule will render the the |
|
1270 |
corresponding case invalid. The term binding @{variable ?case} for |
|
1271 |
the conclusion will be provided with each case, provided that term |
|
1272 |
is fully specified. |
|
1273 |
||
1274 |
The @{command "print_cases"} command prints all named cases present |
|
1275 |
in the current proof state. |
|
1276 |
||
61421 | 1277 |
\<^medskip> |
1278 |
Despite the additional infrastructure, both @{method cases} |
|
60483 | 1279 |
and @{method coinduct} merely apply a certain rule, after |
1280 |
instantiation, while conforming due to the usual way of monotonic |
|
61493 | 1281 |
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> |
60483 | 1282 |
reappears unchanged after the case split. |
1283 |
||
1284 |
The @{method induct} method is fundamentally different in this |
|
1285 |
respect: the meta-level structure is passed through the |
|
1286 |
``recursive'' course involved in the induction. Thus the original |
|
1287 |
statement is basically replaced by separate copies, corresponding to |
|
1288 |
the induction hypotheses and conclusion; the original goal context |
|
1289 |
is no longer available. Thus local assumptions, fixed parameters |
|
1290 |
and definitions effectively participate in the inductive rephrasing |
|
1291 |
of the original statement. |
|
1292 |
||
1293 |
In @{method induct} proofs, local assumptions introduced by cases are split |
|
61493 | 1294 |
into two different kinds: \<open>hyps\<close> stemming from the rule and |
1295 |
\<open>prems\<close> from the goal statement. This is reflected in the |
|
1296 |
extracted cases accordingly, so invoking ``@{command "case"}~\<open>c\<close>'' will provide separate facts \<open>c.hyps\<close> and \<open>c.prems\<close>, |
|
1297 |
as well as fact \<open>c\<close> to hold the all-inclusive list. |
|
60483 | 1298 |
|
1299 |
In @{method induction} proofs, local assumptions introduced by cases are |
|
61493 | 1300 |
split into three different kinds: \<open>IH\<close>, the induction hypotheses, |
1301 |
\<open>hyps\<close>, the remaining hypotheses stemming from the rule, and |
|
1302 |
\<open>prems\<close>, the assumptions from the goal statement. The names are |
|
1303 |
\<open>c.IH\<close>, \<open>c.hyps\<close> and \<open>c.prems\<close>, as above. |
|
60483 | 1304 |
|
1305 |
||
61421 | 1306 |
\<^medskip> |
1307 |
Facts presented to either method are consumed according to |
|
60483 | 1308 |
the number of ``major premises'' of the rule involved, which is |
1309 |
usually 0 for plain cases and induction rules of datatypes etc.\ and |
|
1310 |
1 for rules of inductive predicates or sets and the like. The |
|
1311 |
remaining facts are inserted into the goal verbatim before the |
|
61493 | 1312 |
actual \<open>cases\<close>, \<open>induct\<close>, or \<open>coinduct\<close> rule is |
60483 | 1313 |
applied. |
1314 |
\<close> |
|
1315 |
||
1316 |
||
1317 |
subsection \<open>Declaring rules\<close> |
|
1318 |
||
1319 |
text \<open> |
|
1320 |
\begin{matharray}{rcl} |
|
61493 | 1321 |
@{command_def "print_induct_rules"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\ |
1322 |
@{attribute_def cases} & : & \<open>attribute\<close> \\ |
|
1323 |
@{attribute_def induct} & : & \<open>attribute\<close> \\ |
|
1324 |
@{attribute_def coinduct} & : & \<open>attribute\<close> \\ |
|
60483 | 1325 |
\end{matharray} |
1326 |
||
1327 |
@{rail \<open> |
|
1328 |
@@{attribute cases} spec |
|
1329 |
; |
|
1330 |
@@{attribute induct} spec |
|
1331 |
; |
|
1332 |
@@{attribute coinduct} spec |
|
1333 |
; |
|
1334 |
||
1335 |
spec: (('type' | 'pred' | 'set') ':' @{syntax nameref}) | 'del' |
|
1336 |
\<close>} |
|
1337 |
||
61439 | 1338 |
\<^descr> @{command "print_induct_rules"} prints cases and induct rules |
60483 | 1339 |
for predicates (or sets) and types of the current context. |
1340 |
||
61439 | 1341 |
\<^descr> @{attribute cases}, @{attribute induct}, and @{attribute |
60483 | 1342 |
coinduct} (as attributes) declare rules for reasoning about |
1343 |
(co)inductive predicates (or sets) and types, using the |
|
1344 |
corresponding methods of the same name. Certain definitional |
|
1345 |
packages of object-logics usually declare emerging cases and |
|
1346 |
induction rules as expected, so users rarely need to intervene. |
|
1347 |
||
61493 | 1348 |
Rules may be deleted via the \<open>del\<close> specification, which |
1349 |
covers all of the \<open>type\<close>/\<open>pred\<close>/\<open>set\<close> |
|
60483 | 1350 |
sub-categories simultaneously. For example, @{attribute |
61493 | 1351 |
cases}~\<open>del\<close> removes any @{attribute cases} rules declared for |
60483 | 1352 |
some type, predicate, or set. |
1353 |
||
1354 |
Manual rule declarations usually refer to the @{attribute |
|
1355 |
case_names} and @{attribute params} attributes to adjust names of |
|
1356 |
cases and parameters of a rule; the @{attribute consumes} |
|
1357 |
declaration is taken care of automatically: @{attribute |
|
61493 | 1358 |
consumes}~\<open>0\<close> is specified for ``type'' rules and @{attribute |
1359 |
consumes}~\<open>1\<close> for ``predicate'' / ``set'' rules. |
|
60483 | 1360 |
\<close> |
1361 |
||
1362 |
||
60459 | 1363 |
section \<open>Generalized elimination and case splitting \label{sec:obtain}\<close> |
26870 | 1364 |
|
58618 | 1365 |
text \<open> |
26870 | 1366 |
\begin{matharray}{rcl} |
61493 | 1367 |
@{command_def "consider"} & : & \<open>proof(state) | proof(chain) \<rightarrow> proof(prove)\<close> \\ |
1368 |
@{command_def "obtain"} & : & \<open>proof(state) | proof(chain) \<rightarrow> proof(prove)\<close> \\ |
|
1369 |
@{command_def "guess"}\<open>\<^sup>*\<close> & : & \<open>proof(state) | proof(chain) \<rightarrow> proof(prove)\<close> \\ |
|
26870 | 1370 |
\end{matharray} |
1371 |
||
60459 | 1372 |
Generalized elimination means that hypothetical parameters and premises |
1373 |
may be introduced in the current context, potentially with a split into |
|
1374 |
cases. This works by virtue of a locally proven rule that establishes the |
|
1375 |
soundness of this temporary context extension. As representative examples, |
|
1376 |
one may think of standard rules from Isabelle/HOL like this: |
|
1377 |
||
61421 | 1378 |
\<^medskip> |
60459 | 1379 |
\begin{tabular}{ll} |
61493 | 1380 |
\<open>\<exists>x. B x \<Longrightarrow> (\<And>x. B x \<Longrightarrow> thesis) \<Longrightarrow> thesis\<close> \\ |
1381 |
\<open>A \<and> B \<Longrightarrow> (A \<Longrightarrow> B \<Longrightarrow> thesis) \<Longrightarrow> thesis\<close> \\ |
|
1382 |
\<open>A \<or> B \<Longrightarrow> (A \<Longrightarrow> thesis) \<Longrightarrow> (B \<Longrightarrow> thesis) \<Longrightarrow> thesis\<close> \\ |
|
60459 | 1383 |
\end{tabular} |
61421 | 1384 |
\<^medskip> |
60459 | 1385 |
|
1386 |
In general, these particular rules and connectives need to get involved at |
|
1387 |
all: this concept works directly in Isabelle/Pure via Isar commands |
|
1388 |
defined below. In particular, the logic of elimination and case splitting |
|
1389 |
is delegated to an Isar proof, which often involves automated tools. |
|
26870 | 1390 |
|
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
1391 |
@{rail \<open> |
60459 | 1392 |
@@{command consider} @{syntax obtain_clauses} |
1393 |
; |
|
60448 | 1394 |
@@{command obtain} @{syntax par_name}? (@{syntax "fixes"} + @'and') |
42596
6c621a9d612a
modernized rail diagrams using @{rail} antiquotation;
wenzelm
parents:
40965
diff
changeset
|
1395 |
@'where' (@{syntax props} + @'and') |
26870 | 1396 |
; |
60459 | 1397 |
@@{command guess} (@{syntax "fixes"} + @'and') |
55112
b1a5d603fd12
prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents:
55029
diff
changeset
|
1398 |
\<close>} |
26870 | 1399 |
|
61493 | 1400 |
\<^descr> @{command consider}~\<open>(a) \<^vec>x \<WHERE> \<^vec>A \<^vec>x |
1401 |
| (b) \<^vec>y \<WHERE> \<^vec>B \<^vec>y | \<dots> \<close> states a rule for case |
|
60459 | 1402 |
splitting into separate subgoals, such that each case involves new |
1403 |
parameters and premises. After the proof is finished, the resulting rule |
|
1404 |
may be used directly with the @{method cases} proof method |
|
1405 |
(\secref{sec:cases-induct}), in order to perform actual case-splitting of |
|
1406 |
the proof text via @{command case} and @{command next} as usual. |
|
1407 |
||
1408 |
Optional names in round parentheses refer to case names: in the proof of |
|
1409 |
the rule this is a fact name, in the resulting rule it is used as |
|
1410 |
annotation with the @{attribute_ref case_names} attribute. |
|
1411 |
||
61421 | 1412 |
\<^medskip> |
1413 |
Formally, the command @{command consider} is defined as derived |
|
60459 | 1414 |
Isar language element as follows: |
1415 |
||
26870 | 1416 |
\begin{matharray}{l} |
61493 | 1417 |
@{command "consider"}~\<open>(a) \<^vec>x \<WHERE> \<^vec>A \<^vec>x | (b) \<^vec>y \<WHERE> \<^vec>B \<^vec>y | \<dots> \<equiv>\<close> \\[1ex] |
1418 |
\quad @{command "have"}~\<open>[case_names a b \<dots>]: thesis\<close> \\ |
|
1419 |
\qquad \<open>\<IF> a [Pure.intro?]: \<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis\<close> \\ |
|
1420 |
\qquad \<open>\<AND> b [Pure.intro?]: \<And>\<^vec>y. \<^vec>B \<^vec>y \<Longrightarrow> thesis\<close> \\ |
|
1421 |
\qquad \<open>\<AND> \<dots>\<close> \\ |
|
1422 |
\qquad \<open>\<FOR> thesis\<close> \\ |
|
1423 |
\qquad @{command "apply"}~\<open>(insert a b \<dots>)\<close> \\ |
|
26870 | 1424 |
\end{matharray} |
1425 |
||
60459 | 1426 |
See also \secref{sec:goals} for @{keyword "obtains"} in toplevel goal |
1427 |
statements, as well as @{command print_statement} to print existing rules |
|
1428 |
in a similar format. |
|
26870 | 1429 |
|
61493 | 1430 |
\<^descr> @{command obtain}~\<open>\<^vec>x \<WHERE> \<^vec>A \<^vec>x\<close> |
60459 | 1431 |
states a generalized elimination rule with exactly one case. After the |
1432 |
proof is finished, it is activated for the subsequent proof text: the |
|
61493 | 1433 |
context is augmented via @{command fix}~\<open>\<^vec>x\<close> @{command |
1434 |
assume}~\<open>\<^vec>A \<^vec>x\<close>, with special provisions to export |
|
60459 | 1435 |
later results by discharging these assumptions again. |
1436 |
||
1437 |
Note that according to the parameter scopes within the elimination rule, |
|
61477 | 1438 |
results \<^emph>\<open>must not\<close> refer to hypothetical parameters; otherwise the |
60459 | 1439 |
export will fail! This restriction conforms to the usual manner of |
1440 |
existential reasoning in Natural Deduction. |
|
1441 |
||
61421 | 1442 |
\<^medskip> |
1443 |
Formally, the command @{command obtain} is defined as derived |
|
60459 | 1444 |
Isar language element as follows, using an instrumented variant of |
1445 |
@{command assume}: |
|
26870 | 1446 |
|
60459 | 1447 |
\begin{matharray}{l} |
61493 | 1448 |
@{command "obtain"}~\<open>\<^vec>x \<WHERE> a: \<^vec>A \<^vec>x \<langle>proof\<rangle> \<equiv>\<close> \\[1ex] |
1449 |
\quad @{command "have"}~\<open>thesis\<close> \\ |
|
1450 |
\qquad \<open>\<IF> that [Pure.intro?]: \<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis\<close> \\ |
|
1451 |
\qquad \<open>\<FOR> thesis\<close> \\ |
|
1452 |
\qquad @{command "apply"}~\<open>(insert that)\<close> \\ |
|
1453 |
\qquad \<open>\<langle>proof\<rangle>\<close> \\ |
|
1454 |
\quad @{command "fix"}~\<open>\<^vec>x\<close>~@{command "assume"}\<open>\<^sup>* a: \<^vec>A \<^vec>x\<close> \\ |
|
60459 | 1455 |
\end{matharray} |
1456 |
||
61439 | 1457 |
\<^descr> @{command guess} is similar to @{command obtain}, but it derives the |
60459 | 1458 |
obtained context elements from the course of tactical reasoning in the |
1459 |
proof. Thus it can considerably obscure the proof: it is classified as |
|
61477 | 1460 |
\<^emph>\<open>improper\<close>. |
26870 | 1461 |
|
61493 | 1462 |
A proof with @{command guess} starts with a fixed goal \<open>thesis\<close>. The |
1463 |
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 |
|
60459 | 1464 |
subgoals. The final goal state is then used as reduction rule for the |
61493 | 1465 |
obtain pattern described above. Obtained parameters \<open>\<^vec>x\<close> are |
60459 | 1466 |
marked as internal by default, and thus inaccessible in the proof text. |
1467 |
The variable names and type constraints given as arguments for @{command |
|
1468 |
"guess"} specify a prefix of accessible parameters. |
|
26870 | 1469 |
|
60459 | 1470 |
|
1471 |
In the proof of @{command consider} and @{command obtain} the local |
|
60480 | 1472 |
premises are always bound to the fact name @{fact_ref that}, according to |
60459 | 1473 |
structured Isar statements involving @{keyword_ref "if"} |
1474 |
(\secref{sec:goals}). |
|
1475 |
||
1476 |
Facts that are established by @{command "obtain"} and @{command "guess"} |
|
1477 |
may not be polymorphic: any type-variables occurring here are fixed in the |
|
1478 |
present context. This is a natural consequence of the role of @{command |
|
1479 |
fix} and @{command assume} in these constructs. |
|
58618 | 1480 |
\<close> |
26870 | 1481 |
|
26869 | 1482 |
end |