|
1 theory Generic |
|
2 imports Base Main |
|
3 begin |
|
4 |
|
5 chapter {* Generic tools and packages \label{ch:gen-tools} *} |
|
6 |
|
7 section {* Configuration options \label{sec:config} *} |
|
8 |
|
9 text {* Isabelle/Pure maintains a record of named configuration |
|
10 options within the theory or proof context, with values of type |
|
11 @{ML_type bool}, @{ML_type int}, @{ML_type real}, or @{ML_type |
|
12 string}. Tools may declare options in ML, and then refer to these |
|
13 values (relative to the context). Thus global reference variables |
|
14 are easily avoided. The user may change the value of a |
|
15 configuration option by means of an associated attribute of the same |
|
16 name. This form of context declaration works particularly well with |
|
17 commands such as @{command "declare"} or @{command "using"} like |
|
18 this: |
|
19 *} |
|
20 |
|
21 declare [[show_main_goal = false]] |
|
22 |
|
23 notepad |
|
24 begin |
|
25 note [[show_main_goal = true]] |
|
26 end |
|
27 |
|
28 text {* For historical reasons, some tools cannot take the full proof |
|
29 context into account and merely refer to the background theory. |
|
30 This is accommodated by configuration options being declared as |
|
31 ``global'', which may not be changed within a local context. |
|
32 |
|
33 \begin{matharray}{rcll} |
|
34 @{command_def "print_configs"} & : & @{text "context \<rightarrow>"} \\ |
|
35 \end{matharray} |
|
36 |
|
37 @{rail " |
|
38 @{syntax name} ('=' ('true' | 'false' | @{syntax int} | @{syntax float} | @{syntax name}))? |
|
39 "} |
|
40 |
|
41 \begin{description} |
|
42 |
|
43 \item @{command "print_configs"} prints the available configuration |
|
44 options, with names, types, and current values. |
|
45 |
|
46 \item @{text "name = value"} as an attribute expression modifies the |
|
47 named option, with the syntax of the value depending on the option's |
|
48 type. For @{ML_type bool} the default value is @{text true}. Any |
|
49 attempt to change a global option in a local context is ignored. |
|
50 |
|
51 \end{description} |
|
52 *} |
|
53 |
|
54 |
|
55 section {* Basic proof tools *} |
|
56 |
|
57 subsection {* Miscellaneous methods and attributes \label{sec:misc-meth-att} *} |
|
58 |
|
59 text {* |
|
60 \begin{matharray}{rcl} |
|
61 @{method_def unfold} & : & @{text method} \\ |
|
62 @{method_def fold} & : & @{text method} \\ |
|
63 @{method_def insert} & : & @{text method} \\[0.5ex] |
|
64 @{method_def erule}@{text "\<^sup>*"} & : & @{text method} \\ |
|
65 @{method_def drule}@{text "\<^sup>*"} & : & @{text method} \\ |
|
66 @{method_def frule}@{text "\<^sup>*"} & : & @{text method} \\ |
|
67 @{method_def intro} & : & @{text method} \\ |
|
68 @{method_def elim} & : & @{text method} \\ |
|
69 @{method_def succeed} & : & @{text method} \\ |
|
70 @{method_def fail} & : & @{text method} \\ |
|
71 \end{matharray} |
|
72 |
|
73 @{rail " |
|
74 (@@{method fold} | @@{method unfold} | @@{method insert}) @{syntax thmrefs} |
|
75 ; |
|
76 (@@{method erule} | @@{method drule} | @@{method frule}) |
|
77 ('(' @{syntax nat} ')')? @{syntax thmrefs} |
|
78 ; |
|
79 (@@{method intro} | @@{method elim}) @{syntax thmrefs}? |
|
80 "} |
|
81 |
|
82 \begin{description} |
|
83 |
|
84 \item @{method unfold}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} and @{method fold}~@{text |
|
85 "a\<^sub>1 \<dots> a\<^sub>n"} expand (or fold back) the given definitions throughout |
|
86 all goals; any chained facts provided are inserted into the goal and |
|
87 subject to rewriting as well. |
|
88 |
|
89 \item @{method insert}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} inserts theorems as facts |
|
90 into all goals of the proof state. Note that current facts |
|
91 indicated for forward chaining are ignored. |
|
92 |
|
93 \item @{method erule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}, @{method |
|
94 drule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}, and @{method frule}~@{text |
|
95 "a\<^sub>1 \<dots> a\<^sub>n"} are similar to the basic @{method rule} |
|
96 method (see \secref{sec:pure-meth-att}), but apply rules by |
|
97 elim-resolution, destruct-resolution, and forward-resolution, |
|
98 respectively \cite{isabelle-implementation}. The optional natural |
|
99 number argument (default 0) specifies additional assumption steps to |
|
100 be performed here. |
|
101 |
|
102 Note that these methods are improper ones, mainly serving for |
|
103 experimentation and tactic script emulation. Different modes of |
|
104 basic rule application are usually expressed in Isar at the proof |
|
105 language level, rather than via implicit proof state manipulations. |
|
106 For example, a proper single-step elimination would be done using |
|
107 the plain @{method rule} method, with forward chaining of current |
|
108 facts. |
|
109 |
|
110 \item @{method intro} and @{method elim} repeatedly refine some goal |
|
111 by intro- or elim-resolution, after having inserted any chained |
|
112 facts. Exactly the rules given as arguments are taken into account; |
|
113 this allows fine-tuned decomposition of a proof problem, in contrast |
|
114 to common automated tools. |
|
115 |
|
116 \item @{method succeed} yields a single (unchanged) result; it is |
|
117 the identity of the ``@{text ","}'' method combinator (cf.\ |
|
118 \secref{sec:proof-meth}). |
|
119 |
|
120 \item @{method fail} yields an empty result sequence; it is the |
|
121 identity of the ``@{text "|"}'' method combinator (cf.\ |
|
122 \secref{sec:proof-meth}). |
|
123 |
|
124 \end{description} |
|
125 |
|
126 \begin{matharray}{rcl} |
|
127 @{attribute_def tagged} & : & @{text attribute} \\ |
|
128 @{attribute_def untagged} & : & @{text attribute} \\[0.5ex] |
|
129 @{attribute_def THEN} & : & @{text attribute} \\ |
|
130 @{attribute_def unfolded} & : & @{text attribute} \\ |
|
131 @{attribute_def folded} & : & @{text attribute} \\ |
|
132 @{attribute_def abs_def} & : & @{text attribute} \\[0.5ex] |
|
133 @{attribute_def rotated} & : & @{text attribute} \\ |
|
134 @{attribute_def (Pure) elim_format} & : & @{text attribute} \\ |
|
135 @{attribute_def standard}@{text "\<^sup>*"} & : & @{text attribute} \\ |
|
136 @{attribute_def no_vars}@{text "\<^sup>*"} & : & @{text attribute} \\ |
|
137 \end{matharray} |
|
138 |
|
139 @{rail " |
|
140 @@{attribute tagged} @{syntax name} @{syntax name} |
|
141 ; |
|
142 @@{attribute untagged} @{syntax name} |
|
143 ; |
|
144 @@{attribute THEN} ('[' @{syntax nat} ']')? @{syntax thmref} |
|
145 ; |
|
146 (@@{attribute unfolded} | @@{attribute folded}) @{syntax thmrefs} |
|
147 ; |
|
148 @@{attribute rotated} @{syntax int}? |
|
149 "} |
|
150 |
|
151 \begin{description} |
|
152 |
|
153 \item @{attribute tagged}~@{text "name value"} and @{attribute |
|
154 untagged}~@{text name} add and remove \emph{tags} of some theorem. |
|
155 Tags may be any list of string pairs that serve as formal comment. |
|
156 The first string is considered the tag name, the second its value. |
|
157 Note that @{attribute untagged} removes any tags of the same name. |
|
158 |
|
159 \item @{attribute THEN}~@{text a} composes rules by resolution; it |
|
160 resolves with the first premise of @{text a} (an alternative |
|
161 position may be also specified). See also @{ML_op "RS"} in |
|
162 \cite{isabelle-implementation}. |
|
163 |
|
164 \item @{attribute unfolded}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} and @{attribute |
|
165 folded}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} expand and fold back again the given |
|
166 definitions throughout a rule. |
|
167 |
|
168 \item @{attribute abs_def} turns an equation of the form @{prop "f x |
|
169 y \<equiv> t"} into @{prop "f \<equiv> \<lambda>x y. t"}, which ensures that @{method |
|
170 simp} or @{method unfold} steps always expand it. This also works |
|
171 for object-logic equality. |
|
172 |
|
173 \item @{attribute rotated}~@{text n} rotate the premises of a |
|
174 theorem by @{text n} (default 1). |
|
175 |
|
176 \item @{attribute (Pure) elim_format} turns a destruction rule into |
|
177 elimination rule format, by resolving with the rule @{prop "PROP A \<Longrightarrow> |
|
178 (PROP A \<Longrightarrow> PROP B) \<Longrightarrow> PROP B"}. |
|
179 |
|
180 Note that the Classical Reasoner (\secref{sec:classical}) provides |
|
181 its own version of this operation. |
|
182 |
|
183 \item @{attribute standard} puts a theorem into the standard form of |
|
184 object-rules at the outermost theory level. Note that this |
|
185 operation violates the local proof context (including active |
|
186 locales). |
|
187 |
|
188 \item @{attribute no_vars} replaces schematic variables by free |
|
189 ones; this is mainly for tuning output of pretty printed theorems. |
|
190 |
|
191 \end{description} |
|
192 *} |
|
193 |
|
194 |
|
195 subsection {* Low-level equational reasoning *} |
|
196 |
|
197 text {* |
|
198 \begin{matharray}{rcl} |
|
199 @{method_def subst} & : & @{text method} \\ |
|
200 @{method_def hypsubst} & : & @{text method} \\ |
|
201 @{method_def split} & : & @{text method} \\ |
|
202 \end{matharray} |
|
203 |
|
204 @{rail " |
|
205 @@{method subst} ('(' 'asm' ')')? \\ ('(' (@{syntax nat}+) ')')? @{syntax thmref} |
|
206 ; |
|
207 @@{method split} @{syntax thmrefs} |
|
208 "} |
|
209 |
|
210 These methods provide low-level facilities for equational reasoning |
|
211 that are intended for specialized applications only. Normally, |
|
212 single step calculations would be performed in a structured text |
|
213 (see also \secref{sec:calculation}), while the Simplifier methods |
|
214 provide the canonical way for automated normalization (see |
|
215 \secref{sec:simplifier}). |
|
216 |
|
217 \begin{description} |
|
218 |
|
219 \item @{method subst}~@{text eq} performs a single substitution step |
|
220 using rule @{text eq}, which may be either a meta or object |
|
221 equality. |
|
222 |
|
223 \item @{method subst}~@{text "(asm) eq"} substitutes in an |
|
224 assumption. |
|
225 |
|
226 \item @{method subst}~@{text "(i \<dots> j) eq"} performs several |
|
227 substitutions in the conclusion. The numbers @{text i} to @{text j} |
|
228 indicate the positions to substitute at. Positions are ordered from |
|
229 the top of the term tree moving down from left to right. For |
|
230 example, in @{text "(a + b) + (c + d)"} there are three positions |
|
231 where commutativity of @{text "+"} is applicable: 1 refers to @{text |
|
232 "a + b"}, 2 to the whole term, and 3 to @{text "c + d"}. |
|
233 |
|
234 If the positions in the list @{text "(i \<dots> j)"} are non-overlapping |
|
235 (e.g.\ @{text "(2 3)"} in @{text "(a + b) + (c + d)"}) you may |
|
236 assume all substitutions are performed simultaneously. Otherwise |
|
237 the behaviour of @{text subst} is not specified. |
|
238 |
|
239 \item @{method subst}~@{text "(asm) (i \<dots> j) eq"} performs the |
|
240 substitutions in the assumptions. The positions refer to the |
|
241 assumptions in order from left to right. For example, given in a |
|
242 goal of the form @{text "P (a + b) \<Longrightarrow> P (c + d) \<Longrightarrow> \<dots>"}, position 1 of |
|
243 commutativity of @{text "+"} is the subterm @{text "a + b"} and |
|
244 position 2 is the subterm @{text "c + d"}. |
|
245 |
|
246 \item @{method hypsubst} performs substitution using some |
|
247 assumption; this only works for equations of the form @{text "x = |
|
248 t"} where @{text x} is a free or bound variable. |
|
249 |
|
250 \item @{method split}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} performs single-step case |
|
251 splitting using the given rules. Splitting is performed in the |
|
252 conclusion or some assumption of the subgoal, depending of the |
|
253 structure of the rule. |
|
254 |
|
255 Note that the @{method simp} method already involves repeated |
|
256 application of split rules as declared in the current context, using |
|
257 @{attribute split}, for example. |
|
258 |
|
259 \end{description} |
|
260 *} |
|
261 |
|
262 |
|
263 subsection {* Further tactic emulations \label{sec:tactics} *} |
|
264 |
|
265 text {* |
|
266 The following improper proof methods emulate traditional tactics. |
|
267 These admit direct access to the goal state, which is normally |
|
268 considered harmful! In particular, this may involve both numbered |
|
269 goal addressing (default 1), and dynamic instantiation within the |
|
270 scope of some subgoal. |
|
271 |
|
272 \begin{warn} |
|
273 Dynamic instantiations refer to universally quantified parameters |
|
274 of a subgoal (the dynamic context) rather than fixed variables and |
|
275 term abbreviations of a (static) Isar context. |
|
276 \end{warn} |
|
277 |
|
278 Tactic emulation methods, unlike their ML counterparts, admit |
|
279 simultaneous instantiation from both dynamic and static contexts. |
|
280 If names occur in both contexts goal parameters hide locally fixed |
|
281 variables. Likewise, schematic variables refer to term |
|
282 abbreviations, if present in the static context. Otherwise the |
|
283 schematic variable is interpreted as a schematic variable and left |
|
284 to be solved by unification with certain parts of the subgoal. |
|
285 |
|
286 Note that the tactic emulation proof methods in Isabelle/Isar are |
|
287 consistently named @{text foo_tac}. Note also that variable names |
|
288 occurring on left hand sides of instantiations must be preceded by a |
|
289 question mark if they coincide with a keyword or contain dots. This |
|
290 is consistent with the attribute @{attribute "where"} (see |
|
291 \secref{sec:pure-meth-att}). |
|
292 |
|
293 \begin{matharray}{rcl} |
|
294 @{method_def rule_tac}@{text "\<^sup>*"} & : & @{text method} \\ |
|
295 @{method_def erule_tac}@{text "\<^sup>*"} & : & @{text method} \\ |
|
296 @{method_def drule_tac}@{text "\<^sup>*"} & : & @{text method} \\ |
|
297 @{method_def frule_tac}@{text "\<^sup>*"} & : & @{text method} \\ |
|
298 @{method_def cut_tac}@{text "\<^sup>*"} & : & @{text method} \\ |
|
299 @{method_def thin_tac}@{text "\<^sup>*"} & : & @{text method} \\ |
|
300 @{method_def subgoal_tac}@{text "\<^sup>*"} & : & @{text method} \\ |
|
301 @{method_def rename_tac}@{text "\<^sup>*"} & : & @{text method} \\ |
|
302 @{method_def rotate_tac}@{text "\<^sup>*"} & : & @{text method} \\ |
|
303 @{method_def tactic}@{text "\<^sup>*"} & : & @{text method} \\ |
|
304 @{method_def raw_tactic}@{text "\<^sup>*"} & : & @{text method} \\ |
|
305 \end{matharray} |
|
306 |
|
307 @{rail " |
|
308 (@@{method rule_tac} | @@{method erule_tac} | @@{method drule_tac} | |
|
309 @@{method frule_tac} | @@{method cut_tac} | @@{method thin_tac}) @{syntax goal_spec}? \\ |
|
310 ( dynamic_insts @'in' @{syntax thmref} | @{syntax thmrefs} ) |
|
311 ; |
|
312 @@{method subgoal_tac} @{syntax goal_spec}? (@{syntax prop} +) |
|
313 ; |
|
314 @@{method rename_tac} @{syntax goal_spec}? (@{syntax name} +) |
|
315 ; |
|
316 @@{method rotate_tac} @{syntax goal_spec}? @{syntax int}? |
|
317 ; |
|
318 (@@{method tactic} | @@{method raw_tactic}) @{syntax text} |
|
319 ; |
|
320 |
|
321 dynamic_insts: ((@{syntax name} '=' @{syntax term}) + @'and') |
|
322 "} |
|
323 |
|
324 \begin{description} |
|
325 |
|
326 \item @{method rule_tac} etc. do resolution of rules with explicit |
|
327 instantiation. This works the same way as the ML tactics @{ML |
|
328 res_inst_tac} etc. (see \cite{isabelle-implementation}) |
|
329 |
|
330 Multiple rules may be only given if there is no instantiation; then |
|
331 @{method rule_tac} is the same as @{ML resolve_tac} in ML (see |
|
332 \cite{isabelle-implementation}). |
|
333 |
|
334 \item @{method cut_tac} inserts facts into the proof state as |
|
335 assumption of a subgoal; instantiations may be given as well. Note |
|
336 that the scope of schematic variables is spread over the main goal |
|
337 statement and rule premises are turned into new subgoals. This is |
|
338 in contrast to the regular method @{method insert} which inserts |
|
339 closed rule statements. |
|
340 |
|
341 \item @{method thin_tac}~@{text \<phi>} deletes the specified premise |
|
342 from a subgoal. Note that @{text \<phi>} may contain schematic |
|
343 variables, to abbreviate the intended proposition; the first |
|
344 matching subgoal premise will be deleted. Removing useless premises |
|
345 from a subgoal increases its readability and can make search tactics |
|
346 run faster. |
|
347 |
|
348 \item @{method subgoal_tac}~@{text "\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} adds the propositions |
|
349 @{text "\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} as local premises to a subgoal, and poses the same |
|
350 as new subgoals (in the original context). |
|
351 |
|
352 \item @{method rename_tac}~@{text "x\<^sub>1 \<dots> x\<^sub>n"} renames parameters of a |
|
353 goal according to the list @{text "x\<^sub>1, \<dots>, x\<^sub>n"}, which refers to the |
|
354 \emph{suffix} of variables. |
|
355 |
|
356 \item @{method rotate_tac}~@{text n} rotates the premises of a |
|
357 subgoal by @{text n} positions: from right to left if @{text n} is |
|
358 positive, and from left to right if @{text n} is negative; the |
|
359 default value is 1. |
|
360 |
|
361 \item @{method tactic}~@{text "text"} produces a proof method from |
|
362 any ML text of type @{ML_type tactic}. Apart from the usual ML |
|
363 environment and the current proof context, the ML code may refer to |
|
364 the locally bound values @{ML_text facts}, which indicates any |
|
365 current facts used for forward-chaining. |
|
366 |
|
367 \item @{method raw_tactic} is similar to @{method tactic}, but |
|
368 presents the goal state in its raw internal form, where simultaneous |
|
369 subgoals appear as conjunction of the logical framework instead of |
|
370 the usual split into several subgoals. While feature this is useful |
|
371 for debugging of complex method definitions, it should not never |
|
372 appear in production theories. |
|
373 |
|
374 \end{description} |
|
375 *} |
|
376 |
|
377 |
|
378 section {* The Simplifier \label{sec:simplifier} *} |
|
379 |
|
380 subsection {* Simplification methods *} |
|
381 |
|
382 text {* |
|
383 \begin{matharray}{rcl} |
|
384 @{method_def simp} & : & @{text method} \\ |
|
385 @{method_def simp_all} & : & @{text method} \\ |
|
386 \end{matharray} |
|
387 |
|
388 @{rail " |
|
389 (@@{method simp} | @@{method simp_all}) opt? (@{syntax simpmod} * ) |
|
390 ; |
|
391 |
|
392 opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use' | 'asm_lr' ) ')' |
|
393 ; |
|
394 @{syntax_def simpmod}: ('add' | 'del' | 'only' | 'cong' (() | 'add' | 'del') | |
|
395 'split' (() | 'add' | 'del')) ':' @{syntax thmrefs} |
|
396 "} |
|
397 |
|
398 \begin{description} |
|
399 |
|
400 \item @{method simp} invokes the Simplifier, after declaring |
|
401 additional rules according to the arguments given. Note that the |
|
402 @{text only} modifier first removes all other rewrite rules, |
|
403 congruences, and looper tactics (including splits), and then behaves |
|
404 like @{text add}. |
|
405 |
|
406 \medskip The @{text cong} modifiers add or delete Simplifier |
|
407 congruence rules (see also \secref{sec:simp-cong}), the default is |
|
408 to add. |
|
409 |
|
410 \medskip The @{text split} modifiers add or delete rules for the |
|
411 Splitter (see also \cite{isabelle-ref}), the default is to add. |
|
412 This works only if the Simplifier method has been properly setup to |
|
413 include the Splitter (all major object logics such HOL, HOLCF, FOL, |
|
414 ZF do this already). |
|
415 |
|
416 \item @{method simp_all} is similar to @{method simp}, but acts on |
|
417 all goals (backwards from the last to the first one). |
|
418 |
|
419 \end{description} |
|
420 |
|
421 By default the Simplifier methods take local assumptions fully into |
|
422 account, using equational assumptions in the subsequent |
|
423 normalization process, or simplifying assumptions themselves (cf.\ |
|
424 @{ML asm_full_simp_tac} in \cite{isabelle-ref}). In structured |
|
425 proofs this is usually quite well behaved in practice: just the |
|
426 local premises of the actual goal are involved, additional facts may |
|
427 be inserted via explicit forward-chaining (via @{command "then"}, |
|
428 @{command "from"}, @{command "using"} etc.). |
|
429 |
|
430 Additional Simplifier options may be specified to tune the behavior |
|
431 further (mostly for unstructured scripts with many accidental local |
|
432 facts): ``@{text "(no_asm)"}'' means assumptions are ignored |
|
433 completely (cf.\ @{ML simp_tac}), ``@{text "(no_asm_simp)"}'' means |
|
434 assumptions are used in the simplification of the conclusion but are |
|
435 not themselves simplified (cf.\ @{ML asm_simp_tac}), and ``@{text |
|
436 "(no_asm_use)"}'' means assumptions are simplified but are not used |
|
437 in the simplification of each other or the conclusion (cf.\ @{ML |
|
438 full_simp_tac}). For compatibility reasons, there is also an option |
|
439 ``@{text "(asm_lr)"}'', which means that an assumption is only used |
|
440 for simplifying assumptions which are to the right of it (cf.\ @{ML |
|
441 asm_lr_simp_tac}). |
|
442 |
|
443 The configuration option @{text "depth_limit"} limits the number of |
|
444 recursive invocations of the simplifier during conditional |
|
445 rewriting. |
|
446 |
|
447 \medskip The Splitter package is usually configured to work as part |
|
448 of the Simplifier. The effect of repeatedly applying @{ML |
|
449 split_tac} can be simulated by ``@{text "(simp only: split: |
|
450 a\<^sub>1 \<dots> a\<^sub>n)"}''. There is also a separate @{text split} |
|
451 method available for single-step case splitting. |
|
452 *} |
|
453 |
|
454 |
|
455 subsection {* Declaring rules *} |
|
456 |
|
457 text {* |
|
458 \begin{matharray}{rcl} |
|
459 @{command_def "print_simpset"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
|
460 @{attribute_def simp} & : & @{text attribute} \\ |
|
461 @{attribute_def split} & : & @{text attribute} \\ |
|
462 \end{matharray} |
|
463 |
|
464 @{rail " |
|
465 (@@{attribute simp} | @@{attribute split}) (() | 'add' | 'del') |
|
466 "} |
|
467 |
|
468 \begin{description} |
|
469 |
|
470 \item @{command "print_simpset"} prints the collection of rules |
|
471 declared to the Simplifier, which is also known as ``simpset'' |
|
472 internally \cite{isabelle-ref}. |
|
473 |
|
474 \item @{attribute simp} declares simplification rules. |
|
475 |
|
476 \item @{attribute split} declares case split rules. |
|
477 |
|
478 \end{description} |
|
479 *} |
|
480 |
|
481 |
|
482 subsection {* Congruence rules\label{sec:simp-cong} *} |
|
483 |
|
484 text {* |
|
485 \begin{matharray}{rcl} |
|
486 @{attribute_def cong} & : & @{text attribute} \\ |
|
487 \end{matharray} |
|
488 |
|
489 @{rail " |
|
490 @@{attribute cong} (() | 'add' | 'del') |
|
491 "} |
|
492 |
|
493 \begin{description} |
|
494 |
|
495 \item @{attribute cong} declares congruence rules to the Simplifier |
|
496 context. |
|
497 |
|
498 \end{description} |
|
499 |
|
500 Congruence rules are equalities of the form @{text [display] |
|
501 "\<dots> \<Longrightarrow> f ?x\<^sub>1 \<dots> ?x\<^sub>n = f ?y\<^sub>1 \<dots> ?y\<^sub>n"} |
|
502 |
|
503 This controls the simplification of the arguments of @{text f}. For |
|
504 example, some arguments can be simplified under additional |
|
505 assumptions: @{text [display] "?P\<^sub>1 \<longleftrightarrow> ?Q\<^sub>1 \<Longrightarrow> (?Q\<^sub>1 \<Longrightarrow> ?P\<^sub>2 \<longleftrightarrow> ?Q\<^sub>2) \<Longrightarrow> |
|
506 (?P\<^sub>1 \<longrightarrow> ?P\<^sub>2) \<longleftrightarrow> (?Q\<^sub>1 \<longrightarrow> ?Q\<^sub>2)"} |
|
507 |
|
508 Given this rule, the simplifier assumes @{text "?Q\<^sub>1"} and extracts |
|
509 rewrite rules from it when simplifying @{text "?P\<^sub>2"}. Such local |
|
510 assumptions are effective for rewriting formulae such as @{text "x = |
|
511 0 \<longrightarrow> y + x = y"}. |
|
512 |
|
513 %FIXME |
|
514 %The local assumptions are also provided as theorems to the solver; |
|
515 %see \secref{sec:simp-solver} below. |
|
516 |
|
517 \medskip The following congruence rule for bounded quantifiers also |
|
518 supplies contextual information --- about the bound variable: |
|
519 @{text [display] "(?A = ?B) \<Longrightarrow> (\<And>x. x \<in> ?B \<Longrightarrow> ?P x \<longleftrightarrow> ?Q x) \<Longrightarrow> |
|
520 (\<forall>x \<in> ?A. ?P x) \<longleftrightarrow> (\<forall>x \<in> ?B. ?Q x)"} |
|
521 |
|
522 \medskip This congruence rule for conditional expressions can |
|
523 supply contextual information for simplifying the arms: |
|
524 @{text [display] "?p = ?q \<Longrightarrow> (?q \<Longrightarrow> ?a = ?c) \<Longrightarrow> (\<not> ?q \<Longrightarrow> ?b = ?d) \<Longrightarrow> |
|
525 (if ?p then ?a else ?b) = (if ?q then ?c else ?d)"} |
|
526 |
|
527 A congruence rule can also \emph{prevent} simplification of some |
|
528 arguments. Here is an alternative congruence rule for conditional |
|
529 expressions that conforms to non-strict functional evaluation: |
|
530 @{text [display] "?p = ?q \<Longrightarrow> (if ?p then ?a else ?b) = (if ?q then ?a else ?b)"} |
|
531 |
|
532 Only the first argument is simplified; the others remain unchanged. |
|
533 This can make simplification much faster, but may require an extra |
|
534 case split over the condition @{text "?q"} to prove the goal. |
|
535 *} |
|
536 |
|
537 |
|
538 subsection {* Simplification procedures *} |
|
539 |
|
540 text {* Simplification procedures are ML functions that produce proven |
|
541 rewrite rules on demand. They are associated with higher-order |
|
542 patterns that approximate the left-hand sides of equations. The |
|
543 Simplifier first matches the current redex against one of the LHS |
|
544 patterns; if this succeeds, the corresponding ML function is |
|
545 invoked, passing the Simplifier context and redex term. Thus rules |
|
546 may be specifically fashioned for particular situations, resulting |
|
547 in a more powerful mechanism than term rewriting by a fixed set of |
|
548 rules. |
|
549 |
|
550 Any successful result needs to be a (possibly conditional) rewrite |
|
551 rule @{text "t \<equiv> u"} that is applicable to the current redex. The |
|
552 rule will be applied just as any ordinary rewrite rule. It is |
|
553 expected to be already in \emph{internal form}, bypassing the |
|
554 automatic preprocessing of object-level equivalences. |
|
555 |
|
556 \begin{matharray}{rcl} |
|
557 @{command_def "simproc_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ |
|
558 simproc & : & @{text attribute} \\ |
|
559 \end{matharray} |
|
560 |
|
561 @{rail " |
|
562 @@{command simproc_setup} @{syntax name} '(' (@{syntax term} + '|') ')' '=' |
|
563 @{syntax text} \\ (@'identifier' (@{syntax nameref}+))? |
|
564 ; |
|
565 |
|
566 @@{attribute simproc} (('add' ':')? | 'del' ':') (@{syntax name}+) |
|
567 "} |
|
568 |
|
569 \begin{description} |
|
570 |
|
571 \item @{command "simproc_setup"} defines a named simplification |
|
572 procedure that is invoked by the Simplifier whenever any of the |
|
573 given term patterns match the current redex. The implementation, |
|
574 which is provided as ML source text, needs to be of type @{ML_type |
|
575 "morphism -> simpset -> cterm -> thm option"}, where the @{ML_type |
|
576 cterm} represents the current redex @{text r} and the result is |
|
577 supposed to be some proven rewrite rule @{text "r \<equiv> r'"} (or a |
|
578 generalized version), or @{ML NONE} to indicate failure. The |
|
579 @{ML_type simpset} argument holds the full context of the current |
|
580 Simplifier invocation, including the actual Isar proof context. The |
|
581 @{ML_type morphism} informs about the difference of the original |
|
582 compilation context wrt.\ the one of the actual application later |
|
583 on. The optional @{keyword "identifier"} specifies theorems that |
|
584 represent the logical content of the abstract theory of this |
|
585 simproc. |
|
586 |
|
587 Morphisms and identifiers are only relevant for simprocs that are |
|
588 defined within a local target context, e.g.\ in a locale. |
|
589 |
|
590 \item @{text "simproc add: name"} and @{text "simproc del: name"} |
|
591 add or delete named simprocs to the current Simplifier context. The |
|
592 default is to add a simproc. Note that @{command "simproc_setup"} |
|
593 already adds the new simproc to the subsequent context. |
|
594 |
|
595 \end{description} |
|
596 *} |
|
597 |
|
598 |
|
599 subsubsection {* Example *} |
|
600 |
|
601 text {* The following simplification procedure for @{thm |
|
602 [source=false, show_types] unit_eq} in HOL performs fine-grained |
|
603 control over rule application, beyond higher-order pattern matching. |
|
604 Declaring @{thm unit_eq} as @{attribute simp} directly would make |
|
605 the simplifier loop! Note that a version of this simplification |
|
606 procedure is already active in Isabelle/HOL. *} |
|
607 |
|
608 simproc_setup unit ("x::unit") = {* |
|
609 fn _ => fn _ => fn ct => |
|
610 if HOLogic.is_unit (term_of ct) then NONE |
|
611 else SOME (mk_meta_eq @{thm unit_eq}) |
|
612 *} |
|
613 |
|
614 text {* Since the Simplifier applies simplification procedures |
|
615 frequently, it is important to make the failure check in ML |
|
616 reasonably fast. *} |
|
617 |
|
618 |
|
619 subsection {* Forward simplification *} |
|
620 |
|
621 text {* |
|
622 \begin{matharray}{rcl} |
|
623 @{attribute_def simplified} & : & @{text attribute} \\ |
|
624 \end{matharray} |
|
625 |
|
626 @{rail " |
|
627 @@{attribute simplified} opt? @{syntax thmrefs}? |
|
628 ; |
|
629 |
|
630 opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use') ')' |
|
631 "} |
|
632 |
|
633 \begin{description} |
|
634 |
|
635 \item @{attribute simplified}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} causes a theorem to |
|
636 be simplified, either by exactly the specified rules @{text "a\<^sub>1, \<dots>, |
|
637 a\<^sub>n"}, or the implicit Simplifier context if no arguments are given. |
|
638 The result is fully simplified by default, including assumptions and |
|
639 conclusion; the options @{text no_asm} etc.\ tune the Simplifier in |
|
640 the same way as the for the @{text simp} method. |
|
641 |
|
642 Note that forward simplification restricts the simplifier to its |
|
643 most basic operation of term rewriting; solver and looper tactics |
|
644 \cite{isabelle-ref} are \emph{not} involved here. The @{text |
|
645 simplified} attribute should be only rarely required under normal |
|
646 circumstances. |
|
647 |
|
648 \end{description} |
|
649 *} |
|
650 |
|
651 |
|
652 section {* The Classical Reasoner \label{sec:classical} *} |
|
653 |
|
654 subsection {* Basic concepts *} |
|
655 |
|
656 text {* Although Isabelle is generic, many users will be working in |
|
657 some extension of classical first-order logic. Isabelle/ZF is built |
|
658 upon theory FOL, while Isabelle/HOL conceptually contains |
|
659 first-order logic as a fragment. Theorem-proving in predicate logic |
|
660 is undecidable, but many automated strategies have been developed to |
|
661 assist in this task. |
|
662 |
|
663 Isabelle's classical reasoner is a generic package that accepts |
|
664 certain information about a logic and delivers a suite of automatic |
|
665 proof tools, based on rules that are classified and declared in the |
|
666 context. These proof procedures are slow and simplistic compared |
|
667 with high-end automated theorem provers, but they can save |
|
668 considerable time and effort in practice. They can prove theorems |
|
669 such as Pelletier's \cite{pelletier86} problems 40 and 41 in a few |
|
670 milliseconds (including full proof reconstruction): *} |
|
671 |
|
672 lemma "(\<exists>y. \<forall>x. F x y \<longleftrightarrow> F x x) \<longrightarrow> \<not> (\<forall>x. \<exists>y. \<forall>z. F z y \<longleftrightarrow> \<not> F z x)" |
|
673 by blast |
|
674 |
|
675 lemma "(\<forall>z. \<exists>y. \<forall>x. f x y \<longleftrightarrow> f x z \<and> \<not> f x x) \<longrightarrow> \<not> (\<exists>z. \<forall>x. f x z)" |
|
676 by blast |
|
677 |
|
678 text {* The proof tools are generic. They are not restricted to |
|
679 first-order logic, and have been heavily used in the development of |
|
680 the Isabelle/HOL library and applications. The tactics can be |
|
681 traced, and their components can be called directly; in this manner, |
|
682 any proof can be viewed interactively. *} |
|
683 |
|
684 |
|
685 subsubsection {* The sequent calculus *} |
|
686 |
|
687 text {* Isabelle supports natural deduction, which is easy to use for |
|
688 interactive proof. But natural deduction does not easily lend |
|
689 itself to automation, and has a bias towards intuitionism. For |
|
690 certain proofs in classical logic, it can not be called natural. |
|
691 The \emph{sequent calculus}, a generalization of natural deduction, |
|
692 is easier to automate. |
|
693 |
|
694 A \textbf{sequent} has the form @{text "\<Gamma> \<turnstile> \<Delta>"}, where @{text "\<Gamma>"} |
|
695 and @{text "\<Delta>"} are sets of formulae.\footnote{For first-order |
|
696 logic, sequents can equivalently be made from lists or multisets of |
|
697 formulae.} The sequent @{text "P\<^sub>1, \<dots>, P\<^sub>m \<turnstile> Q\<^sub>1, \<dots>, Q\<^sub>n"} is |
|
698 \textbf{valid} if @{text "P\<^sub>1 \<and> \<dots> \<and> P\<^sub>m"} implies @{text "Q\<^sub>1 \<or> \<dots> \<or> |
|
699 Q\<^sub>n"}. Thus @{text "P\<^sub>1, \<dots>, P\<^sub>m"} represent assumptions, each of which |
|
700 is true, while @{text "Q\<^sub>1, \<dots>, Q\<^sub>n"} represent alternative goals. A |
|
701 sequent is \textbf{basic} if its left and right sides have a common |
|
702 formula, as in @{text "P, Q \<turnstile> Q, R"}; basic sequents are trivially |
|
703 valid. |
|
704 |
|
705 Sequent rules are classified as \textbf{right} or \textbf{left}, |
|
706 indicating which side of the @{text "\<turnstile>"} symbol they operate on. |
|
707 Rules that operate on the right side are analogous to natural |
|
708 deduction's introduction rules, and left rules are analogous to |
|
709 elimination rules. The sequent calculus analogue of @{text "(\<longrightarrow>I)"} |
|
710 is the rule |
|
711 \[ |
|
712 \infer[@{text "(\<longrightarrow>R)"}]{@{text "\<Gamma> \<turnstile> \<Delta>, P \<longrightarrow> Q"}}{@{text "P, \<Gamma> \<turnstile> \<Delta>, Q"}} |
|
713 \] |
|
714 Applying the rule backwards, this breaks down some implication on |
|
715 the right side of a sequent; @{text "\<Gamma>"} and @{text "\<Delta>"} stand for |
|
716 the sets of formulae that are unaffected by the inference. The |
|
717 analogue of the pair @{text "(\<or>I1)"} and @{text "(\<or>I2)"} is the |
|
718 single rule |
|
719 \[ |
|
720 \infer[@{text "(\<or>R)"}]{@{text "\<Gamma> \<turnstile> \<Delta>, P \<or> Q"}}{@{text "\<Gamma> \<turnstile> \<Delta>, P, Q"}} |
|
721 \] |
|
722 This breaks down some disjunction on the right side, replacing it by |
|
723 both disjuncts. Thus, the sequent calculus is a kind of |
|
724 multiple-conclusion logic. |
|
725 |
|
726 To illustrate the use of multiple formulae on the right, let us |
|
727 prove the classical theorem @{text "(P \<longrightarrow> Q) \<or> (Q \<longrightarrow> P)"}. Working |
|
728 backwards, we reduce this formula to a basic sequent: |
|
729 \[ |
|
730 \infer[@{text "(\<or>R)"}]{@{text "\<turnstile> (P \<longrightarrow> Q) \<or> (Q \<longrightarrow> P)"}} |
|
731 {\infer[@{text "(\<longrightarrow>R)"}]{@{text "\<turnstile> (P \<longrightarrow> Q), (Q \<longrightarrow> P)"}} |
|
732 {\infer[@{text "(\<longrightarrow>R)"}]{@{text "P \<turnstile> Q, (Q \<longrightarrow> P)"}} |
|
733 {@{text "P, Q \<turnstile> Q, P"}}}} |
|
734 \] |
|
735 |
|
736 This example is typical of the sequent calculus: start with the |
|
737 desired theorem and apply rules backwards in a fairly arbitrary |
|
738 manner. This yields a surprisingly effective proof procedure. |
|
739 Quantifiers add only few complications, since Isabelle handles |
|
740 parameters and schematic variables. See \cite[Chapter |
|
741 10]{paulson-ml2} for further discussion. *} |
|
742 |
|
743 |
|
744 subsubsection {* Simulating sequents by natural deduction *} |
|
745 |
|
746 text {* Isabelle can represent sequents directly, as in the |
|
747 object-logic LK. But natural deduction is easier to work with, and |
|
748 most object-logics employ it. Fortunately, we can simulate the |
|
749 sequent @{text "P\<^sub>1, \<dots>, P\<^sub>m \<turnstile> Q\<^sub>1, \<dots>, Q\<^sub>n"} by the Isabelle formula |
|
750 @{text "P\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> P\<^sub>m \<Longrightarrow> \<not> Q\<^sub>2 \<Longrightarrow> ... \<Longrightarrow> \<not> Q\<^sub>n \<Longrightarrow> Q\<^sub>1"} where the order of |
|
751 the assumptions and the choice of @{text "Q\<^sub>1"} are arbitrary. |
|
752 Elim-resolution plays a key role in simulating sequent proofs. |
|
753 |
|
754 We can easily handle reasoning on the left. Elim-resolution with |
|
755 the rules @{text "(\<or>E)"}, @{text "(\<bottom>E)"} and @{text "(\<exists>E)"} achieves |
|
756 a similar effect as the corresponding sequent rules. For the other |
|
757 connectives, we use sequent-style elimination rules instead of |
|
758 destruction rules such as @{text "(\<and>E1, 2)"} and @{text "(\<forall>E)"}. |
|
759 But note that the rule @{text "(\<not>L)"} has no effect under our |
|
760 representation of sequents! |
|
761 \[ |
|
762 \infer[@{text "(\<not>L)"}]{@{text "\<not> P, \<Gamma> \<turnstile> \<Delta>"}}{@{text "\<Gamma> \<turnstile> \<Delta>, P"}} |
|
763 \] |
|
764 |
|
765 What about reasoning on the right? Introduction rules can only |
|
766 affect the formula in the conclusion, namely @{text "Q\<^sub>1"}. The |
|
767 other right-side formulae are represented as negated assumptions, |
|
768 @{text "\<not> Q\<^sub>2, \<dots>, \<not> Q\<^sub>n"}. In order to operate on one of these, it |
|
769 must first be exchanged with @{text "Q\<^sub>1"}. Elim-resolution with the |
|
770 @{text swap} rule has this effect: @{text "\<not> P \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> R"} |
|
771 |
|
772 To ensure that swaps occur only when necessary, each introduction |
|
773 rule is converted into a swapped form: it is resolved with the |
|
774 second premise of @{text "(swap)"}. The swapped form of @{text |
|
775 "(\<and>I)"}, which might be called @{text "(\<not>\<and>E)"}, is |
|
776 @{text [display] "\<not> (P \<and> Q) \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> (\<not> R \<Longrightarrow> Q) \<Longrightarrow> R"} |
|
777 |
|
778 Similarly, the swapped form of @{text "(\<longrightarrow>I)"} is |
|
779 @{text [display] "\<not> (P \<longrightarrow> Q) \<Longrightarrow> (\<not> R \<Longrightarrow> P \<Longrightarrow> Q) \<Longrightarrow> R"} |
|
780 |
|
781 Swapped introduction rules are applied using elim-resolution, which |
|
782 deletes the negated formula. Our representation of sequents also |
|
783 requires the use of ordinary introduction rules. If we had no |
|
784 regard for readability of intermediate goal states, we could treat |
|
785 the right side more uniformly by representing sequents as @{text |
|
786 [display] "P\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> P\<^sub>m \<Longrightarrow> \<not> Q\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> \<not> Q\<^sub>n \<Longrightarrow> \<bottom>"} |
|
787 *} |
|
788 |
|
789 |
|
790 subsubsection {* Extra rules for the sequent calculus *} |
|
791 |
|
792 text {* As mentioned, destruction rules such as @{text "(\<and>E1, 2)"} and |
|
793 @{text "(\<forall>E)"} must be replaced by sequent-style elimination rules. |
|
794 In addition, we need rules to embody the classical equivalence |
|
795 between @{text "P \<longrightarrow> Q"} and @{text "\<not> P \<or> Q"}. The introduction |
|
796 rules @{text "(\<or>I1, 2)"} are replaced by a rule that simulates |
|
797 @{text "(\<or>R)"}: @{text [display] "(\<not> Q \<Longrightarrow> P) \<Longrightarrow> P \<or> Q"} |
|
798 |
|
799 The destruction rule @{text "(\<longrightarrow>E)"} is replaced by @{text [display] |
|
800 "(P \<longrightarrow> Q) \<Longrightarrow> (\<not> P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"} |
|
801 |
|
802 Quantifier replication also requires special rules. In classical |
|
803 logic, @{text "\<exists>x. P x"} is equivalent to @{text "\<not> (\<forall>x. \<not> P x)"}; |
|
804 the rules @{text "(\<exists>R)"} and @{text "(\<forall>L)"} are dual: |
|
805 \[ |
|
806 \infer[@{text "(\<exists>R)"}]{@{text "\<Gamma> \<turnstile> \<Delta>, \<exists>x. P x"}}{@{text "\<Gamma> \<turnstile> \<Delta>, \<exists>x. P x, P t"}} |
|
807 \qquad |
|
808 \infer[@{text "(\<forall>L)"}]{@{text "\<forall>x. P x, \<Gamma> \<turnstile> \<Delta>"}}{@{text "P t, \<forall>x. P x, \<Gamma> \<turnstile> \<Delta>"}} |
|
809 \] |
|
810 Thus both kinds of quantifier may be replicated. Theorems requiring |
|
811 multiple uses of a universal formula are easy to invent; consider |
|
812 @{text [display] "(\<forall>x. P x \<longrightarrow> P (f x)) \<and> P a \<longrightarrow> P (f\<^sup>n a)"} for any |
|
813 @{text "n > 1"}. Natural examples of the multiple use of an |
|
814 existential formula are rare; a standard one is @{text "\<exists>x. \<forall>y. P x |
|
815 \<longrightarrow> P y"}. |
|
816 |
|
817 Forgoing quantifier replication loses completeness, but gains |
|
818 decidability, since the search space becomes finite. Many useful |
|
819 theorems can be proved without replication, and the search generally |
|
820 delivers its verdict in a reasonable time. To adopt this approach, |
|
821 represent the sequent rules @{text "(\<exists>R)"}, @{text "(\<exists>L)"} and |
|
822 @{text "(\<forall>R)"} by @{text "(\<exists>I)"}, @{text "(\<exists>E)"} and @{text "(\<forall>I)"}, |
|
823 respectively, and put @{text "(\<forall>E)"} into elimination form: @{text |
|
824 [display] "\<forall>x. P x \<Longrightarrow> (P t \<Longrightarrow> Q) \<Longrightarrow> Q"} |
|
825 |
|
826 Elim-resolution with this rule will delete the universal formula |
|
827 after a single use. To replicate universal quantifiers, replace the |
|
828 rule by @{text [display] "\<forall>x. P x \<Longrightarrow> (P t \<Longrightarrow> \<forall>x. P x \<Longrightarrow> Q) \<Longrightarrow> Q"} |
|
829 |
|
830 To replicate existential quantifiers, replace @{text "(\<exists>I)"} by |
|
831 @{text [display] "(\<not> (\<exists>x. P x) \<Longrightarrow> P t) \<Longrightarrow> \<exists>x. P x"} |
|
832 |
|
833 All introduction rules mentioned above are also useful in swapped |
|
834 form. |
|
835 |
|
836 Replication makes the search space infinite; we must apply the rules |
|
837 with care. The classical reasoner distinguishes between safe and |
|
838 unsafe rules, applying the latter only when there is no alternative. |
|
839 Depth-first search may well go down a blind alley; best-first search |
|
840 is better behaved in an infinite search space. However, quantifier |
|
841 replication is too expensive to prove any but the simplest theorems. |
|
842 *} |
|
843 |
|
844 |
|
845 subsection {* Rule declarations *} |
|
846 |
|
847 text {* The proof tools of the Classical Reasoner depend on |
|
848 collections of rules declared in the context, which are classified |
|
849 as introduction, elimination or destruction and as \emph{safe} or |
|
850 \emph{unsafe}. In general, safe rules can be attempted blindly, |
|
851 while unsafe rules must be used with care. A safe rule must never |
|
852 reduce a provable goal to an unprovable set of subgoals. |
|
853 |
|
854 The rule @{text "P \<Longrightarrow> P \<or> Q"} is unsafe because it reduces @{text "P |
|
855 \<or> Q"} to @{text "P"}, which might turn out as premature choice of an |
|
856 unprovable subgoal. Any rule is unsafe whose premises contain new |
|
857 unknowns. The elimination rule @{text "\<forall>x. P x \<Longrightarrow> (P t \<Longrightarrow> Q) \<Longrightarrow> Q"} is |
|
858 unsafe, since it is applied via elim-resolution, which discards the |
|
859 assumption @{text "\<forall>x. P x"} and replaces it by the weaker |
|
860 assumption @{text "P t"}. The rule @{text "P t \<Longrightarrow> \<exists>x. P x"} is |
|
861 unsafe for similar reasons. The quantifier duplication rule @{text |
|
862 "\<forall>x. P x \<Longrightarrow> (P t \<Longrightarrow> \<forall>x. P x \<Longrightarrow> Q) \<Longrightarrow> Q"} is unsafe in a different sense: |
|
863 since it keeps the assumption @{text "\<forall>x. P x"}, it is prone to |
|
864 looping. In classical first-order logic, all rules are safe except |
|
865 those mentioned above. |
|
866 |
|
867 The safe~/ unsafe distinction is vague, and may be regarded merely |
|
868 as a way of giving some rules priority over others. One could argue |
|
869 that @{text "(\<or>E)"} is unsafe, because repeated application of it |
|
870 could generate exponentially many subgoals. Induction rules are |
|
871 unsafe because inductive proofs are difficult to set up |
|
872 automatically. Any inference is unsafe that instantiates an unknown |
|
873 in the proof state --- thus matching must be used, rather than |
|
874 unification. Even proof by assumption is unsafe if it instantiates |
|
875 unknowns shared with other subgoals. |
|
876 |
|
877 \begin{matharray}{rcl} |
|
878 @{command_def "print_claset"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
|
879 @{attribute_def intro} & : & @{text attribute} \\ |
|
880 @{attribute_def elim} & : & @{text attribute} \\ |
|
881 @{attribute_def dest} & : & @{text attribute} \\ |
|
882 @{attribute_def rule} & : & @{text attribute} \\ |
|
883 @{attribute_def iff} & : & @{text attribute} \\ |
|
884 @{attribute_def swapped} & : & @{text attribute} \\ |
|
885 \end{matharray} |
|
886 |
|
887 @{rail " |
|
888 (@@{attribute intro} | @@{attribute elim} | @@{attribute dest}) ('!' | () | '?') @{syntax nat}? |
|
889 ; |
|
890 @@{attribute rule} 'del' |
|
891 ; |
|
892 @@{attribute iff} (((() | 'add') '?'?) | 'del') |
|
893 "} |
|
894 |
|
895 \begin{description} |
|
896 |
|
897 \item @{command "print_claset"} prints the collection of rules |
|
898 declared to the Classical Reasoner, i.e.\ the @{ML_type claset} |
|
899 within the context. |
|
900 |
|
901 \item @{attribute intro}, @{attribute elim}, and @{attribute dest} |
|
902 declare introduction, elimination, and destruction rules, |
|
903 respectively. By default, rules are considered as \emph{unsafe} |
|
904 (i.e.\ not applied blindly without backtracking), while ``@{text |
|
905 "!"}'' classifies as \emph{safe}. Rule declarations marked by |
|
906 ``@{text "?"}'' coincide with those of Isabelle/Pure, cf.\ |
|
907 \secref{sec:pure-meth-att} (i.e.\ are only applied in single steps |
|
908 of the @{method rule} method). The optional natural number |
|
909 specifies an explicit weight argument, which is ignored by the |
|
910 automated reasoning tools, but determines the search order of single |
|
911 rule steps. |
|
912 |
|
913 Introduction rules are those that can be applied using ordinary |
|
914 resolution. Their swapped forms are generated internally, which |
|
915 will be applied using elim-resolution. Elimination rules are |
|
916 applied using elim-resolution. Rules are sorted by the number of |
|
917 new subgoals they will yield; rules that generate the fewest |
|
918 subgoals will be tried first. Otherwise, later declarations take |
|
919 precedence over earlier ones. |
|
920 |
|
921 Rules already present in the context with the same classification |
|
922 are ignored. A warning is printed if the rule has already been |
|
923 added with some other classification, but the rule is added anyway |
|
924 as requested. |
|
925 |
|
926 \item @{attribute rule}~@{text del} deletes all occurrences of a |
|
927 rule from the classical context, regardless of its classification as |
|
928 introduction~/ elimination~/ destruction and safe~/ unsafe. |
|
929 |
|
930 \item @{attribute iff} declares logical equivalences to the |
|
931 Simplifier and the Classical reasoner at the same time. |
|
932 Non-conditional rules result in a safe introduction and elimination |
|
933 pair; conditional ones are considered unsafe. Rules with negative |
|
934 conclusion are automatically inverted (using @{text "\<not>"}-elimination |
|
935 internally). |
|
936 |
|
937 The ``@{text "?"}'' version of @{attribute iff} declares rules to |
|
938 the Isabelle/Pure context only, and omits the Simplifier |
|
939 declaration. |
|
940 |
|
941 \item @{attribute swapped} turns an introduction rule into an |
|
942 elimination, by resolving with the classical swap principle @{text |
|
943 "\<not> P \<Longrightarrow> (\<not> R \<Longrightarrow> P) \<Longrightarrow> R"} in the second position. This is mainly for |
|
944 illustrative purposes: the Classical Reasoner already swaps rules |
|
945 internally as explained above. |
|
946 |
|
947 \end{description} |
|
948 *} |
|
949 |
|
950 |
|
951 subsection {* Structured methods *} |
|
952 |
|
953 text {* |
|
954 \begin{matharray}{rcl} |
|
955 @{method_def rule} & : & @{text method} \\ |
|
956 @{method_def contradiction} & : & @{text method} \\ |
|
957 \end{matharray} |
|
958 |
|
959 @{rail " |
|
960 @@{method rule} @{syntax thmrefs}? |
|
961 "} |
|
962 |
|
963 \begin{description} |
|
964 |
|
965 \item @{method rule} as offered by the Classical Reasoner is a |
|
966 refinement over the Pure one (see \secref{sec:pure-meth-att}). Both |
|
967 versions work the same, but the classical version observes the |
|
968 classical rule context in addition to that of Isabelle/Pure. |
|
969 |
|
970 Common object logics (HOL, ZF, etc.) declare a rich collection of |
|
971 classical rules (even if these would qualify as intuitionistic |
|
972 ones), but only few declarations to the rule context of |
|
973 Isabelle/Pure (\secref{sec:pure-meth-att}). |
|
974 |
|
975 \item @{method contradiction} solves some goal by contradiction, |
|
976 deriving any result from both @{text "\<not> A"} and @{text A}. Chained |
|
977 facts, which are guaranteed to participate, may appear in either |
|
978 order. |
|
979 |
|
980 \end{description} |
|
981 *} |
|
982 |
|
983 |
|
984 subsection {* Automated methods *} |
|
985 |
|
986 text {* |
|
987 \begin{matharray}{rcl} |
|
988 @{method_def blast} & : & @{text method} \\ |
|
989 @{method_def auto} & : & @{text method} \\ |
|
990 @{method_def force} & : & @{text method} \\ |
|
991 @{method_def fast} & : & @{text method} \\ |
|
992 @{method_def slow} & : & @{text method} \\ |
|
993 @{method_def best} & : & @{text method} \\ |
|
994 @{method_def fastforce} & : & @{text method} \\ |
|
995 @{method_def slowsimp} & : & @{text method} \\ |
|
996 @{method_def bestsimp} & : & @{text method} \\ |
|
997 @{method_def deepen} & : & @{text method} \\ |
|
998 \end{matharray} |
|
999 |
|
1000 @{rail " |
|
1001 @@{method blast} @{syntax nat}? (@{syntax clamod} * ) |
|
1002 ; |
|
1003 @@{method auto} (@{syntax nat} @{syntax nat})? (@{syntax clasimpmod} * ) |
|
1004 ; |
|
1005 @@{method force} (@{syntax clasimpmod} * ) |
|
1006 ; |
|
1007 (@@{method fast} | @@{method slow} | @@{method best}) (@{syntax clamod} * ) |
|
1008 ; |
|
1009 (@@{method fastforce} | @@{method slowsimp} | @@{method bestsimp}) |
|
1010 (@{syntax clasimpmod} * ) |
|
1011 ; |
|
1012 @@{method deepen} (@{syntax nat} ?) (@{syntax clamod} * ) |
|
1013 ; |
|
1014 @{syntax_def clamod}: |
|
1015 (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' @{syntax thmrefs} |
|
1016 ; |
|
1017 @{syntax_def clasimpmod}: ('simp' (() | 'add' | 'del' | 'only') | |
|
1018 ('cong' | 'split') (() | 'add' | 'del') | |
|
1019 'iff' (((() | 'add') '?'?) | 'del') | |
|
1020 (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del')) ':' @{syntax thmrefs} |
|
1021 "} |
|
1022 |
|
1023 \begin{description} |
|
1024 |
|
1025 \item @{method blast} is a separate classical tableau prover that |
|
1026 uses the same classical rule declarations as explained before. |
|
1027 |
|
1028 Proof search is coded directly in ML using special data structures. |
|
1029 A successful proof is then reconstructed using regular Isabelle |
|
1030 inferences. It is faster and more powerful than the other classical |
|
1031 reasoning tools, but has major limitations too. |
|
1032 |
|
1033 \begin{itemize} |
|
1034 |
|
1035 \item It does not use the classical wrapper tacticals, such as the |
|
1036 integration with the Simplifier of @{method fastforce}. |
|
1037 |
|
1038 \item It does not perform higher-order unification, as needed by the |
|
1039 rule @{thm [source=false] rangeI} in HOL. There are often |
|
1040 alternatives to such rules, for example @{thm [source=false] |
|
1041 range_eqI}. |
|
1042 |
|
1043 \item Function variables may only be applied to parameters of the |
|
1044 subgoal. (This restriction arises because the prover does not use |
|
1045 higher-order unification.) If other function variables are present |
|
1046 then the prover will fail with the message \texttt{Function Var's |
|
1047 argument not a bound variable}. |
|
1048 |
|
1049 \item Its proof strategy is more general than @{method fast} but can |
|
1050 be slower. If @{method blast} fails or seems to be running forever, |
|
1051 try @{method fast} and the other proof tools described below. |
|
1052 |
|
1053 \end{itemize} |
|
1054 |
|
1055 The optional integer argument specifies a bound for the number of |
|
1056 unsafe steps used in a proof. By default, @{method blast} starts |
|
1057 with a bound of 0 and increases it successively to 20. In contrast, |
|
1058 @{text "(blast lim)"} tries to prove the goal using a search bound |
|
1059 of @{text "lim"}. Sometimes a slow proof using @{method blast} can |
|
1060 be made much faster by supplying the successful search bound to this |
|
1061 proof method instead. |
|
1062 |
|
1063 \item @{method auto} combines classical reasoning with |
|
1064 simplification. It is intended for situations where there are a lot |
|
1065 of mostly trivial subgoals; it proves all the easy ones, leaving the |
|
1066 ones it cannot prove. Occasionally, attempting to prove the hard |
|
1067 ones may take a long time. |
|
1068 |
|
1069 The optional depth arguments in @{text "(auto m n)"} refer to its |
|
1070 builtin classical reasoning procedures: @{text m} (default 4) is for |
|
1071 @{method blast}, which is tried first, and @{text n} (default 2) is |
|
1072 for a slower but more general alternative that also takes wrappers |
|
1073 into account. |
|
1074 |
|
1075 \item @{method force} is intended to prove the first subgoal |
|
1076 completely, using many fancy proof tools and performing a rather |
|
1077 exhaustive search. As a result, proof attempts may take rather long |
|
1078 or diverge easily. |
|
1079 |
|
1080 \item @{method fast}, @{method best}, @{method slow} attempt to |
|
1081 prove the first subgoal using sequent-style reasoning as explained |
|
1082 before. Unlike @{method blast}, they construct proofs directly in |
|
1083 Isabelle. |
|
1084 |
|
1085 There is a difference in search strategy and back-tracking: @{method |
|
1086 fast} uses depth-first search and @{method best} uses best-first |
|
1087 search (guided by a heuristic function: normally the total size of |
|
1088 the proof state). |
|
1089 |
|
1090 Method @{method slow} is like @{method fast}, but conducts a broader |
|
1091 search: it may, when backtracking from a failed proof attempt, undo |
|
1092 even the step of proving a subgoal by assumption. |
|
1093 |
|
1094 \item @{method fastforce}, @{method slowsimp}, @{method bestsimp} |
|
1095 are like @{method fast}, @{method slow}, @{method best}, |
|
1096 respectively, but use the Simplifier as additional wrapper. The name |
|
1097 @{method fastforce}, reflects the behaviour of this popular method |
|
1098 better without requiring an understanding of its implementation. |
|
1099 |
|
1100 \item @{method deepen} works by exhaustive search up to a certain |
|
1101 depth. The start depth is 4 (unless specified explicitly), and the |
|
1102 depth is increased iteratively up to 10. Unsafe rules are modified |
|
1103 to preserve the formula they act on, so that it be used repeatedly. |
|
1104 This method can prove more goals than @{method fast}, but is much |
|
1105 slower, for example if the assumptions have many universal |
|
1106 quantifiers. |
|
1107 |
|
1108 \end{description} |
|
1109 |
|
1110 Any of the above methods support additional modifiers of the context |
|
1111 of classical (and simplifier) rules, but the ones related to the |
|
1112 Simplifier are explicitly prefixed by @{text simp} here. The |
|
1113 semantics of these ad-hoc rule declarations is analogous to the |
|
1114 attributes given before. Facts provided by forward chaining are |
|
1115 inserted into the goal before commencing proof search. |
|
1116 *} |
|
1117 |
|
1118 |
|
1119 subsection {* Semi-automated methods *} |
|
1120 |
|
1121 text {* These proof methods may help in situations when the |
|
1122 fully-automated tools fail. The result is a simpler subgoal that |
|
1123 can be tackled by other means, such as by manual instantiation of |
|
1124 quantifiers. |
|
1125 |
|
1126 \begin{matharray}{rcl} |
|
1127 @{method_def safe} & : & @{text method} \\ |
|
1128 @{method_def clarify} & : & @{text method} \\ |
|
1129 @{method_def clarsimp} & : & @{text method} \\ |
|
1130 \end{matharray} |
|
1131 |
|
1132 @{rail " |
|
1133 (@@{method safe} | @@{method clarify}) (@{syntax clamod} * ) |
|
1134 ; |
|
1135 @@{method clarsimp} (@{syntax clasimpmod} * ) |
|
1136 "} |
|
1137 |
|
1138 \begin{description} |
|
1139 |
|
1140 \item @{method safe} repeatedly performs safe steps on all subgoals. |
|
1141 It is deterministic, with at most one outcome. |
|
1142 |
|
1143 \item @{method clarify} performs a series of safe steps without |
|
1144 splitting subgoals; see also @{ML clarify_step_tac}. |
|
1145 |
|
1146 \item @{method clarsimp} acts like @{method clarify}, but also does |
|
1147 simplification. Note that if the Simplifier context includes a |
|
1148 splitter for the premises, the subgoal may still be split. |
|
1149 |
|
1150 \end{description} |
|
1151 *} |
|
1152 |
|
1153 |
|
1154 subsection {* Single-step tactics *} |
|
1155 |
|
1156 text {* |
|
1157 \begin{matharray}{rcl} |
|
1158 @{index_ML safe_step_tac: "Proof.context -> int -> tactic"} \\ |
|
1159 @{index_ML inst_step_tac: "Proof.context -> int -> tactic"} \\ |
|
1160 @{index_ML step_tac: "Proof.context -> int -> tactic"} \\ |
|
1161 @{index_ML slow_step_tac: "Proof.context -> int -> tactic"} \\ |
|
1162 @{index_ML clarify_step_tac: "Proof.context -> int -> tactic"} \\ |
|
1163 \end{matharray} |
|
1164 |
|
1165 These are the primitive tactics behind the (semi)automated proof |
|
1166 methods of the Classical Reasoner. By calling them yourself, you |
|
1167 can execute these procedures one step at a time. |
|
1168 |
|
1169 \begin{description} |
|
1170 |
|
1171 \item @{ML safe_step_tac}~@{text "ctxt i"} performs a safe step on |
|
1172 subgoal @{text i}. The safe wrapper tacticals are applied to a |
|
1173 tactic that may include proof by assumption or Modus Ponens (taking |
|
1174 care not to instantiate unknowns), or substitution. |
|
1175 |
|
1176 \item @{ML inst_step_tac} is like @{ML safe_step_tac}, but allows |
|
1177 unknowns to be instantiated. |
|
1178 |
|
1179 \item @{ML step_tac}~@{text "ctxt i"} is the basic step of the proof |
|
1180 procedure. The unsafe wrapper tacticals are applied to a tactic |
|
1181 that tries @{ML safe_tac}, @{ML inst_step_tac}, or applies an unsafe |
|
1182 rule from the context. |
|
1183 |
|
1184 \item @{ML slow_step_tac} resembles @{ML step_tac}, but allows |
|
1185 backtracking between using safe rules with instantiation (@{ML |
|
1186 inst_step_tac}) and using unsafe rules. The resulting search space |
|
1187 is larger. |
|
1188 |
|
1189 \item @{ML clarify_step_tac}~@{text "ctxt i"} performs a safe step |
|
1190 on subgoal @{text i}. No splitting step is applied; for example, |
|
1191 the subgoal @{text "A \<and> B"} is left as a conjunction. Proof by |
|
1192 assumption, Modus Ponens, etc., may be performed provided they do |
|
1193 not instantiate unknowns. Assumptions of the form @{text "x = t"} |
|
1194 may be eliminated. The safe wrapper tactical is applied. |
|
1195 |
|
1196 \end{description} |
|
1197 *} |
|
1198 |
|
1199 |
|
1200 section {* Object-logic setup \label{sec:object-logic} *} |
|
1201 |
|
1202 text {* |
|
1203 \begin{matharray}{rcl} |
|
1204 @{command_def "judgment"} & : & @{text "theory \<rightarrow> theory"} \\ |
|
1205 @{method_def atomize} & : & @{text method} \\ |
|
1206 @{attribute_def atomize} & : & @{text attribute} \\ |
|
1207 @{attribute_def rule_format} & : & @{text attribute} \\ |
|
1208 @{attribute_def rulify} & : & @{text attribute} \\ |
|
1209 \end{matharray} |
|
1210 |
|
1211 The very starting point for any Isabelle object-logic is a ``truth |
|
1212 judgment'' that links object-level statements to the meta-logic |
|
1213 (with its minimal language of @{text prop} that covers universal |
|
1214 quantification @{text "\<And>"} and implication @{text "\<Longrightarrow>"}). |
|
1215 |
|
1216 Common object-logics are sufficiently expressive to internalize rule |
|
1217 statements over @{text "\<And>"} and @{text "\<Longrightarrow>"} within their own |
|
1218 language. This is useful in certain situations where a rule needs |
|
1219 to be viewed as an atomic statement from the meta-level perspective, |
|
1220 e.g.\ @{text "\<And>x. x \<in> A \<Longrightarrow> P x"} versus @{text "\<forall>x \<in> A. P x"}. |
|
1221 |
|
1222 From the following language elements, only the @{method atomize} |
|
1223 method and @{attribute rule_format} attribute are occasionally |
|
1224 required by end-users, the rest is for those who need to setup their |
|
1225 own object-logic. In the latter case existing formulations of |
|
1226 Isabelle/FOL or Isabelle/HOL may be taken as realistic examples. |
|
1227 |
|
1228 Generic tools may refer to the information provided by object-logic |
|
1229 declarations internally. |
|
1230 |
|
1231 @{rail " |
|
1232 @@{command judgment} @{syntax name} '::' @{syntax type} @{syntax mixfix}? |
|
1233 ; |
|
1234 @@{attribute atomize} ('(' 'full' ')')? |
|
1235 ; |
|
1236 @@{attribute rule_format} ('(' 'noasm' ')')? |
|
1237 "} |
|
1238 |
|
1239 \begin{description} |
|
1240 |
|
1241 \item @{command "judgment"}~@{text "c :: \<sigma> (mx)"} declares constant |
|
1242 @{text c} as the truth judgment of the current object-logic. Its |
|
1243 type @{text \<sigma>} should specify a coercion of the category of |
|
1244 object-level propositions to @{text prop} of the Pure meta-logic; |
|
1245 the mixfix annotation @{text "(mx)"} would typically just link the |
|
1246 object language (internally of syntactic category @{text logic}) |
|
1247 with that of @{text prop}. Only one @{command "judgment"} |
|
1248 declaration may be given in any theory development. |
|
1249 |
|
1250 \item @{method atomize} (as a method) rewrites any non-atomic |
|
1251 premises of a sub-goal, using the meta-level equations declared via |
|
1252 @{attribute atomize} (as an attribute) beforehand. As a result, |
|
1253 heavily nested goals become amenable to fundamental operations such |
|
1254 as resolution (cf.\ the @{method (Pure) rule} method). Giving the ``@{text |
|
1255 "(full)"}'' option here means to turn the whole subgoal into an |
|
1256 object-statement (if possible), including the outermost parameters |
|
1257 and assumptions as well. |
|
1258 |
|
1259 A typical collection of @{attribute atomize} rules for a particular |
|
1260 object-logic would provide an internalization for each of the |
|
1261 connectives of @{text "\<And>"}, @{text "\<Longrightarrow>"}, and @{text "\<equiv>"}. |
|
1262 Meta-level conjunction should be covered as well (this is |
|
1263 particularly important for locales, see \secref{sec:locale}). |
|
1264 |
|
1265 \item @{attribute rule_format} rewrites a theorem by the equalities |
|
1266 declared as @{attribute rulify} rules in the current object-logic. |
|
1267 By default, the result is fully normalized, including assumptions |
|
1268 and conclusions at any depth. The @{text "(no_asm)"} option |
|
1269 restricts the transformation to the conclusion of a rule. |
|
1270 |
|
1271 In common object-logics (HOL, FOL, ZF), the effect of @{attribute |
|
1272 rule_format} is to replace (bounded) universal quantification |
|
1273 (@{text "\<forall>"}) and implication (@{text "\<longrightarrow>"}) by the corresponding |
|
1274 rule statements over @{text "\<And>"} and @{text "\<Longrightarrow>"}. |
|
1275 |
|
1276 \end{description} |
|
1277 *} |
|
1278 |
|
1279 end |