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