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