|
1 (*:wrap=hard:maxLineLen=78:*) |
|
2 |
|
3 theory Manual |
|
4 imports Base "../Eisbach_Tools" |
|
5 begin |
|
6 |
|
7 chapter \<open>The method command\<close> |
|
8 |
|
9 text \<open> |
|
10 The @{command_def method} command provides the ability to write proof |
|
11 methods by combining existing ones with their usual syntax. Specifically it |
|
12 allows compound proof methods to be named, and to extend the name space of |
|
13 basic methods accordingly. Method definitions may abstract over parameters: |
|
14 terms, facts, or other methods. |
|
15 |
|
16 \medskip The syntax diagram below refers to some syntactic categories that |
|
17 are further defined in @{cite "isabelle-isar-ref"}. |
|
18 |
|
19 @{rail \<open> |
|
20 @@{command method} name args @'=' method |
|
21 ; |
|
22 args: term_args? method_args? \<newline> fact_args? decl_args? |
|
23 ; |
|
24 term_args: @'for' @{syntax "fixes"} |
|
25 ; |
|
26 method_args: @'methods' (name+) |
|
27 ; |
|
28 fact_args: @'uses' (name+) |
|
29 ; |
|
30 decl_args: @'declares' (name+) |
|
31 \<close>} |
|
32 \<close> |
|
33 |
|
34 |
|
35 section \<open>Basic method definitions\<close> |
|
36 |
|
37 text \<open> |
|
38 Consider the following proof that makes use of usual Isar method |
|
39 combinators. |
|
40 \<close> |
|
41 |
|
42 lemma "P \<and> Q \<longrightarrow> P" |
|
43 by ((rule impI, (erule conjE)?) | assumption)+ |
|
44 |
|
45 text \<open> |
|
46 It is clear that this compound method will be applicable in more cases than |
|
47 this proof alone. With the @{command method} command we can define a proof |
|
48 method that makes the above functionality available generally. |
|
49 \<close> |
|
50 |
|
51 method prop_solver\<^sub>1 = |
|
52 ((rule impI, (erule conjE)?) | assumption)+ |
|
53 |
|
54 lemma "P \<and> Q \<and> R \<longrightarrow> P" |
|
55 by prop_solver\<^sub>1 |
|
56 |
|
57 text \<open> |
|
58 In this example, the facts @{text impI} and @{text conjE} are static. They |
|
59 are evaluated once when the method is defined and cannot be changed later. |
|
60 This makes the method stable in the sense of \emph{static scoping}: naming |
|
61 another fact @{text impI} in a later context won't affect the behaviour of |
|
62 @{text "prop_solver\<^sub>1"}. |
|
63 \<close> |
|
64 |
|
65 |
|
66 section \<open>Term abstraction\<close> |
|
67 |
|
68 text \<open> |
|
69 Methods can also abstract over terms using the @{keyword_def "for"} keyword, |
|
70 optionally providing type constraints. For instance, the following proof |
|
71 method @{text intro_ex} takes a term @{term y} of any type, which it uses to |
|
72 instantiate the @{term x}-variable of @{text exI} (existential introduction) |
|
73 before applying the result as a rule. The instantiation is performed here by |
|
74 Isar's @{attribute_ref "where"} attribute. If the current subgoal is to find |
|
75 a witness for the given predicate @{term Q}, then this has the effect of |
|
76 committing to @{term y}. |
|
77 \<close> |
|
78 |
|
79 method intro_ex for Q :: "'a \<Rightarrow> bool" and y :: 'a = |
|
80 (rule exI ["where" P = Q and x = y]) |
|
81 |
|
82 |
|
83 text \<open> |
|
84 The term parameters @{term y} and @{term Q} can be used arbitrarily inside |
|
85 the method body, as part of attribute applications or arguments to other |
|
86 methods. The expression is type-checked as far as possible when the method |
|
87 is defined, however dynamic type errors can still occur when it is invoked |
|
88 (e.g.\ when terms are instantiated in a parameterized fact). Actual term |
|
89 arguments are supplied positionally, in the same order as in the method |
|
90 definition. |
|
91 \<close> |
|
92 |
|
93 lemma "P a \<Longrightarrow> \<exists>x. P x" |
|
94 by (intro_ex P a) |
|
95 |
|
96 |
|
97 section \<open>Fact abstraction\<close> |
|
98 |
|
99 subsection \<open>Named theorems\<close> |
|
100 |
|
101 text \<open> |
|
102 A @{text "named theorem"} is a fact whose contents are produced dynamically |
|
103 within the current proof context. The Isar command @{command_ref |
|
104 "named_theorems"} provides simple access to this concept: it declares a |
|
105 dynamic fact with corresponding \emph{attribute} |
|
106 (see \autoref{s:attributes}) for managing this particular data slot in the |
|
107 context. |
|
108 \<close> |
|
109 |
|
110 named_theorems intros |
|
111 |
|
112 text \<open> |
|
113 So far @{text "intros"} refers to the empty fact. Using the Isar command |
|
114 @{command_ref "declare"} we may apply declaration attributes to the context. |
|
115 Below we declare both @{text "conjI"} and @{text "impI"} as @{text |
|
116 "intros"}, adding them to the named theorem slot. |
|
117 \<close> |
|
118 |
|
119 declare conjI [intros] and impI [intros] |
|
120 |
|
121 text \<open> |
|
122 We can refer to named theorems as dynamic facts within a particular proof |
|
123 context, which are evaluated whenever the method is invoked. Instead of |
|
124 having facts hard-coded into the method, as in @{text prop_solver\<^sub>1}, we can |
|
125 instead refer to these named theorems. |
|
126 \<close> |
|
127 |
|
128 named_theorems elims |
|
129 declare conjE [elims] |
|
130 |
|
131 method prop_solver\<^sub>3 = |
|
132 ((rule intros, (erule elims)?) | assumption)+ |
|
133 |
|
134 lemma "P \<and> Q \<longrightarrow> P" |
|
135 by prop_solver\<^sub>3 |
|
136 |
|
137 text \<open> |
|
138 Often these named theorems need to be augmented on the spot, when a method |
|
139 is invoked. The @{keyword_def "declares"} keyword in the signature of |
|
140 @{command method} adds the common method syntax @{text "method decl: facts"} |
|
141 for each named theorem @{text decl}. |
|
142 \<close> |
|
143 |
|
144 method prop_solver\<^sub>4 declares intros elims = |
|
145 ((rule intros, (erule elims)?) | assumption)+ |
|
146 |
|
147 lemma "P \<and> (P \<longrightarrow> Q) \<longrightarrow> Q \<and> P" |
|
148 by (prop_solver\<^sub>4 elims: impE intros: conjI) |
|
149 |
|
150 |
|
151 subsection \<open>Simple fact abstraction\<close> |
|
152 |
|
153 text \<open> |
|
154 The @{keyword "declares"} keyword requires that a corresponding dynamic fact |
|
155 has been declared with @{command_ref named_theorems}. This is useful for |
|
156 managing collections of facts which are to be augmented with declarations, |
|
157 but is overkill if we simply want to pass a fact to a method. |
|
158 |
|
159 We may use the @{keyword_def "uses"} keyword in the method header to provide |
|
160 a simple fact parameter. In contrast to @{keyword "declares"}, these facts |
|
161 are always implicitly empty unless augmented when the method is invoked. |
|
162 \<close> |
|
163 |
|
164 method rule_twice uses my_rule = |
|
165 (rule my_rule, rule my_rule) |
|
166 |
|
167 lemma "P \<Longrightarrow> Q \<Longrightarrow> (P \<and> Q) \<and> Q" |
|
168 by (rule_twice my_rule: conjI) |
|
169 |
|
170 |
|
171 section \<open>Higher-order methods\<close> |
|
172 |
|
173 text \<open> |
|
174 The \emph{structured concatenation} combinator ``@{text "method\<^sub>1 ; |
|
175 method\<^sub>2"}'' was introduced in Isabelle2015, motivated by development of |
|
176 Eisbach. It is similar to ``@{text "method\<^sub>1, method\<^sub>2"}'', but @{text |
|
177 method\<^sub>2} is invoked on on \emph{all} subgoals that have newly emerged from |
|
178 @{text method\<^sub>1}. This is useful to handle cases where the number of |
|
179 subgoals produced by a method is determined dynamically at run-time. |
|
180 \<close> |
|
181 |
|
182 method conj_with uses rule = |
|
183 (intro conjI ; intro rule) |
|
184 |
|
185 lemma |
|
186 assumes A: "P" |
|
187 shows "P \<and> P \<and> P" |
|
188 by (conj_with rule: A) |
|
189 |
|
190 text \<open> |
|
191 Method definitions may take other methods as arguments, and thus implement |
|
192 method combinators with prefix syntax. For example, to more usefully exploit |
|
193 Isabelle's backtracking, the explicit requirement that a method solve all |
|
194 produced subgoals is frequently useful. This can easily be written as a |
|
195 \emph{higher-order method} using ``@{text ";"}''. The @{keyword "methods"} |
|
196 keyword denotes method parameters that are other proof methods to be invoked |
|
197 by the method being defined. |
|
198 \<close> |
|
199 |
|
200 method solve methods m = (m ; fail) |
|
201 |
|
202 text \<open> |
|
203 Given some method-argument @{text m}, @{text "solve \<open>m\<close>"} applies the |
|
204 method @{text m} and then fails whenever @{text m} produces any new unsolved |
|
205 subgoals --- i.e. when @{text m} fails to completely discharge the goal it |
|
206 was applied to. |
|
207 \<close> |
|
208 |
|
209 |
|
210 section \<open>Example\<close> |
|
211 |
|
212 text \<open> |
|
213 With these simple features we are ready to write our first non-trivial proof |
|
214 method. Returning to the first-order logic example, the following method |
|
215 definition applies various rules with their canonical methods. |
|
216 \<close> |
|
217 |
|
218 named_theorems subst |
|
219 |
|
220 method prop_solver declares intros elims subst = |
|
221 (assumption | |
|
222 (rule intros) | erule elims | |
|
223 subst subst | subst (asm) subst | |
|
224 (erule notE ; solve \<open>prop_solver\<close>))+ |
|
225 |
|
226 text \<open> |
|
227 The only non-trivial part above is the final alternative @{text "(erule notE |
|
228 ; solve \<open>prop_solver\<close>)"}. Here, in the case that all other alternatives |
|
229 fail, the method takes one of the assumptions @{term "\<not> P"} of the current |
|
230 goal and eliminates it with the rule @{text notE}, causing the goal to be |
|
231 proved to become @{term P}. The method then recursively invokes itself on |
|
232 the remaining goals. The job of the recursive call is to demonstrate that |
|
233 there is a contradiction in the original assumptions (i.e.\ that @{term P} |
|
234 can be derived from them). Note this recursive invocation is applied with |
|
235 the @{method solve} method combinator to ensure that a contradiction will |
|
236 indeed be shown. In the case where a contradiction cannot be found, |
|
237 backtracking will occur and a different assumption @{term "\<not> Q"} will be |
|
238 chosen for elimination. |
|
239 |
|
240 Note that the recursive call to @{method prop_solver} does not have any |
|
241 parameters passed to it. Recall that fact parameters, e.g.\ @{text |
|
242 "intros"}, @{text "elims"}, and @{text "subst"}, are managed by declarations |
|
243 in the current proof context. They will therefore be passed to any recursive |
|
244 call to @{method prop_solver} and, more generally, any invocation of a |
|
245 method which declares these named theorems. |
|
246 |
|
247 \medskip After declaring some standard rules to the context, the @{method |
|
248 prop_solver} becomes capable of solving non-trivial propositional |
|
249 tautologies.\<close> |
|
250 |
|
251 lemmas [intros] = |
|
252 conjI -- \<open>@{thm conjI}\<close> |
|
253 impI -- \<open>@{thm impI}\<close> |
|
254 disjCI -- \<open>@{thm disjCI}\<close> |
|
255 iffI -- \<open>@{thm iffI}\<close> |
|
256 notI -- \<open>@{thm notI}\<close> |
|
257 (*<*)TrueI(*>*) |
|
258 lemmas [elims] = |
|
259 impCE -- \<open>@{thm impCE}\<close> |
|
260 conjE -- \<open>@{thm conjE}\<close> |
|
261 disjE -- \<open>@{thm disjE}\<close> |
|
262 |
|
263 lemma "(A \<or> B) \<and> (A \<longrightarrow> C) \<and> (B \<longrightarrow> C) \<longrightarrow> C" |
|
264 by prop_solver |
|
265 |
|
266 |
|
267 chapter \<open>The match method \label{s:matching}\<close> |
|
268 |
|
269 text \<open> |
|
270 So far we have seen methods defined as simple combinations of other methods. |
|
271 Some familiar programming language concepts have been introduced (i.e.\ |
|
272 abstraction and recursion). The only control flow has been implicitly the |
|
273 result of backtracking. When designing more sophisticated proof methods this |
|
274 proves too restrictive and difficult to manage conceptually. |
|
275 |
|
276 To address this, we introduce the @{method_def "match"} method, which |
|
277 provides more direct access to the higher-order matching facility at the |
|
278 core of Isabelle. It is implemented as a separate proof method (in |
|
279 Isabelle/ML), and thus can be directly applied to proofs, however it is most |
|
280 useful when applied in the context of writing Eisbach method definitions. |
|
281 |
|
282 \medskip The syntax diagram below refers to some syntactic categories that |
|
283 are further defined in @{cite "isabelle-isar-ref"}. |
|
284 |
|
285 @{rail \<open> |
|
286 @@{method match} kind @'in' (pattern '\<Rightarrow>' cartouche + '\<bar>') |
|
287 ; |
|
288 kind: |
|
289 (@'conclusion' | @'premises' ('(' 'local' ')')? | |
|
290 '(' term ')' | @{syntax thmrefs}) |
|
291 ; |
|
292 pattern: fact_name? term args? \<newline> (@'for' fixes)? |
|
293 ; |
|
294 fact_name: @{syntax name} @{syntax attributes}? ':' |
|
295 ; |
|
296 args: '(' (('multi' | 'cut' nat?) + ',') ')' |
|
297 \<close>} |
|
298 |
|
299 Matching allows methods to introspect the goal state, and to implement more |
|
300 explicit control flow. In the basic case, a term or fact @{text ts} is given |
|
301 to match against as a \emph{match target}, along with a collection of |
|
302 pattern-method pairs @{text "(p, m)"}: roughly speaking, when the pattern |
|
303 @{text p} matches any member of @{text ts}, the \emph{inner} method @{text |
|
304 m} will be executed. |
|
305 \<close> |
|
306 |
|
307 lemma |
|
308 assumes X: |
|
309 "Q \<longrightarrow> P" |
|
310 "Q" |
|
311 shows P |
|
312 by (match X in I: "Q \<longrightarrow> P" and I': "Q" \<Rightarrow> \<open>insert mp [OF I I']\<close>) |
|
313 |
|
314 text \<open> |
|
315 In this example we have a structured Isar proof, with the named |
|
316 assumption @{text "X"} and a conclusion @{term "P"}. With the match method |
|
317 we can find the local facts @{term "Q \<longrightarrow> P"} and @{term "Q"}, binding them to |
|
318 separately as @{text "I"} and @{text "I'"}. We then specialize the |
|
319 modus-ponens rule @{thm mp [of Q P]} to these facts to solve the goal. |
|
320 \<close> |
|
321 |
|
322 |
|
323 section \<open>Subgoal focus\<close> |
|
324 |
|
325 text\<open> |
|
326 In the previous example we were able to match against an assumption out of |
|
327 the Isar proof state. In general, however, proof subgoals can be |
|
328 \emph{unstructured}, with goal parameters and premises arising from rule |
|
329 application. To address this, @{method match} uses \emph{subgoal focusing} |
|
330 (see also \autoref{s:design}) to produce structured goals out of |
|
331 unstructured ones. In place of fact or term, we may give the |
|
332 keyword @{keyword_def "premises"} as the match target. This causes a subgoal |
|
333 focus on the first subgoal, lifting local goal parameters to fixed term |
|
334 variables and premises into hypothetical theorems. The match is performed |
|
335 against these theorems, naming them and binding them as appropriate. |
|
336 Similarly giving the keyword @{keyword_def "conclusion"} matches against the |
|
337 conclusion of the first subgoal. |
|
338 |
|
339 An unstructured version of the previous example can then be similarly solved |
|
340 through focusing. |
|
341 \<close> |
|
342 |
|
343 lemma "Q \<longrightarrow> P \<Longrightarrow> Q \<Longrightarrow> P" |
|
344 by (match premises in |
|
345 I: "Q \<longrightarrow> P" and I': "Q" \<Rightarrow> \<open>insert mp [OF I I']\<close>) |
|
346 |
|
347 text \<open> |
|
348 Match variables may be specified by giving a list of @{keyword_ref |
|
349 "for"}-fixes after the pattern description. This marks those terms as bound |
|
350 variables, which may be used in the method body. |
|
351 \<close> |
|
352 |
|
353 lemma "Q \<longrightarrow> P \<Longrightarrow> Q \<Longrightarrow> P" |
|
354 by (match premises in I: "Q \<longrightarrow> A" and I': "Q" for A \<Rightarrow> |
|
355 \<open>match conclusion in A \<Rightarrow> \<open>insert mp [OF I I']\<close>\<close>) |
|
356 |
|
357 text \<open> |
|
358 In this example @{term A} is a match variable which is bound to @{term P} |
|
359 upon a successful match. The inner @{method match} then matches the |
|
360 now-bound @{term A} (bound to @{term P}) against the conclusion (also @{term |
|
361 P}), finally applying the specialized rule to solve the goal. |
|
362 |
|
363 Schematic terms like @{text "?P"} may also be used to specify match |
|
364 variables, but the result of the match is not bound, and thus cannot be used |
|
365 in the inner method body. |
|
366 |
|
367 \medskip In the following example we extract the predicate of an |
|
368 existentially quantified conclusion in the current subgoal and search the |
|
369 current premises for a matching fact. If both matches are successful, we |
|
370 then instantiate the existential introduction rule with both the witness and |
|
371 predicate, solving with the matched premise. |
|
372 \<close> |
|
373 |
|
374 method solve_ex = |
|
375 (match conclusion in "\<exists>x. Q x" for Q \<Rightarrow> |
|
376 \<open>match premises in U: "Q y" for y \<Rightarrow> |
|
377 \<open>rule exI [where P = Q and x = y, OF U]\<close>\<close>) |
|
378 |
|
379 text \<open> |
|
380 The first @{method match} matches the pattern @{term "\<exists>x. Q x"} against the |
|
381 current conclusion, binding the term @{term "Q"} in the inner match. Next |
|
382 the pattern @{text "Q y"} is matched against all premises of the current |
|
383 subgoal. In this case @{term "Q"} is fixed and @{term "y"} may be |
|
384 instantiated. Once a match is found, the local fact @{text U} is bound to |
|
385 the matching premise and the variable @{term "y"} is bound to the matching |
|
386 witness. The existential introduction rule @{text "exI:"}~@{thm exI} is then |
|
387 instantiated with @{term "y"} as the witness and @{term "Q"} as the |
|
388 predicate, with its proof obligation solved by the local fact U (using the |
|
389 Isar attribute @{attribute OF}). The following example is a trivial use of |
|
390 this method. |
|
391 \<close> |
|
392 |
|
393 lemma "halts p \<Longrightarrow> \<exists>x. halts x" |
|
394 by solve_ex |
|
395 |
|
396 |
|
397 subsubsection \<open>Operating within a focus\<close> |
|
398 |
|
399 text \<open> |
|
400 Subgoal focusing provides a structured form of a subgoal, allowing for more |
|
401 expressive introspection of the goal state. This requires some consideration |
|
402 in order to be used effectively. When the keyword @{keyword "premises"} is |
|
403 given as the match target, the premises of the subgoal are lifted into |
|
404 hypothetical theorems, which can be found and named via match patterns. |
|
405 Additionally these premises are stripped from the subgoal, leaving only the |
|
406 conclusion. This renders them inaccessible to standard proof methods which |
|
407 operate on the premises, such as @{method frule} or @{method erule}. Naive |
|
408 usage of these methods within a match will most likely not function as the |
|
409 method author intended. |
|
410 \<close> |
|
411 |
|
412 method my_allE_bad for y :: 'a = |
|
413 (match premises in I: "\<forall>x :: 'a. ?Q x" \<Rightarrow> |
|
414 \<open>erule allE [where x = y]\<close>) |
|
415 |
|
416 text \<open> |
|
417 Here we take a single parameter @{term y} and specialize the universal |
|
418 elimination rule (@{thm allE}) to it, then attempt to apply this specialized |
|
419 rule with @{method erule}. The method @{method erule} will attempt to unify |
|
420 with a universal quantifier in the premises that matches the type of @{term |
|
421 y}. Since @{keyword "premises"} causes a focus, however, there are no |
|
422 subgoal premises to be found and thus @{method my_allE_bad} will always |
|
423 fail. If focusing instead left the premises in place, using methods |
|
424 like @{method erule} would lead to unintended behaviour, specifically during |
|
425 backtracking. In our example, @{method erule} could choose an alternate |
|
426 premise while backtracking, while leaving @{text I} bound to the original |
|
427 match. In the case of more complex inner methods, where either @{text I} or |
|
428 bound terms are used, this would almost certainly not be the intended |
|
429 behaviour. |
|
430 |
|
431 An alternative implementation would be to specialize the elimination rule to |
|
432 the bound term and apply it directly. |
|
433 \<close> |
|
434 |
|
435 method my_allE_almost for y :: 'a = |
|
436 (match premises in I: "\<forall>x :: 'a. ?Q x" \<Rightarrow> |
|
437 \<open>rule allE [where x = y, OF I]\<close>) |
|
438 |
|
439 lemma "\<forall>x. P x \<Longrightarrow> P y" |
|
440 by (my_allE_almost y) |
|
441 |
|
442 text \<open> |
|
443 This method will insert a specialized duplicate of a universally quantified |
|
444 premise. Although this will successfully apply in the presence of such a |
|
445 premise, it is not likely the intended behaviour. Repeated application of |
|
446 this method will produce an infinite stream of duplicate specialized |
|
447 premises, due to the original premise never being removed. To address this, |
|
448 matched premises may be declared with the @{attribute "thin"} attribute. |
|
449 This will hide the premise from subsequent inner matches, and remove it from |
|
450 the list of premises when the inner method has finished and the subgoal is |
|
451 unfocused. It can be considered analogous to the existing @{text thin_tac}. |
|
452 |
|
453 To complete our example, the correct implementation of the method |
|
454 will @{attribute "thin"} the premise from the match and then apply it to the |
|
455 specialized elimination rule.\<close> |
|
456 |
|
457 method my_allE for y :: 'a = |
|
458 (match premises in I [thin]: "\<forall>x :: 'a. ?Q x" \<Rightarrow> |
|
459 \<open>rule allE [where x = y, OF I]\<close>) |
|
460 |
|
461 lemma "\<forall>x. P x \<Longrightarrow> \<forall>x. Q x \<Longrightarrow> P y \<and> Q y" |
|
462 by (my_allE y)+ (rule conjI) |
|
463 |
|
464 |
|
465 subsection \<open>Attributes\<close> |
|
466 |
|
467 text \<open> |
|
468 Attributes may throw errors when applied to a given fact. For example, rule |
|
469 instantiation will fail of there is a type mismatch or if a given variable |
|
470 doesn't exist. Within a match or a method definition, it isn't generally |
|
471 possible to guarantee that applied attributes won't fail. For example, in |
|
472 the following method there is no guarantee that the two provided facts will |
|
473 necessarily compose. |
|
474 \<close> |
|
475 |
|
476 method my_compose uses rule1 rule2 = |
|
477 (rule rule1[OF rule2]) |
|
478 |
|
479 text \<open> |
|
480 Some attributes (like @{attribute OF}) have been made partially |
|
481 Eisbach-aware. This means that they are able to form a closure despite not |
|
482 necessarily always being applicable. In the case of @{attribute OF}, it is |
|
483 up to the proof author to guard attribute application with an appropriate |
|
484 @{method match}, but there are still no static guarantees. |
|
485 |
|
486 In contrast to @{attribute OF}, the @{attribute "where"} and @{attribute of} |
|
487 attributes attempt to provide static guarantees that they will apply |
|
488 whenever possible. |
|
489 |
|
490 Within a match pattern for a fact, each outermost quantifier specifies the |
|
491 requirement that a matching fact must have a schematic variable at that |
|
492 point. This gives a corresponding name to this ``slot'' for the purposes of |
|
493 forming a static closure, allowing the @{attribute "where"} attribute to |
|
494 perform an instantiation at run-time. |
|
495 \<close> |
|
496 |
|
497 lemma |
|
498 assumes A: "Q \<Longrightarrow> False" |
|
499 shows "\<not> Q" |
|
500 by (match intros in X: "\<And>P. (P \<Longrightarrow> False) \<Longrightarrow> \<not> P" \<Rightarrow> |
|
501 \<open>rule X [where P = Q, OF A]\<close>) |
|
502 |
|
503 text \<open> |
|
504 Subgoal focusing converts the outermost quantifiers of premises into |
|
505 schematics when lifting them to hypothetical facts. This allows us to |
|
506 instantiate them with @{attribute "where"} when using an appropriate match |
|
507 pattern. |
|
508 \<close> |
|
509 |
|
510 lemma "(\<And>x :: 'a. A x \<Longrightarrow> B x) \<Longrightarrow> A y \<Longrightarrow> B y" |
|
511 by (match premises in I: "\<And>x :: 'a. ?P x \<Longrightarrow> ?Q x" \<Rightarrow> |
|
512 \<open>rule I [where x = y]\<close>) |
|
513 |
|
514 text \<open> |
|
515 The @{attribute of} attribute behaves similarly. It is worth noting, |
|
516 however, that the positional instantiation of @{attribute of} occurs against |
|
517 the position of the variables as they are declared \emph{in the match |
|
518 pattern}. |
|
519 \<close> |
|
520 |
|
521 lemma |
|
522 fixes A B and x :: 'a and y :: 'b |
|
523 assumes asm: "(\<And>x y. A y x \<Longrightarrow> B x y )" |
|
524 shows "A y x \<Longrightarrow> B x y" |
|
525 by (match asm in I: "\<And>(x :: 'a) (y :: 'b). ?P x y \<Longrightarrow> ?Q x y" \<Rightarrow> |
|
526 \<open>rule I [of x y]\<close>) |
|
527 |
|
528 text \<open> |
|
529 In this example, the order of schematics in @{text asm} is actually @{text |
|
530 "?y ?x"}, but we instantiate our matched rule in the opposite order. This is |
|
531 because the effective rule @{term I} was bound from the match, which |
|
532 declared the @{typ 'a} slot first and the @{typ 'b} slot second. |
|
533 |
|
534 To get the dynamic behaviour of @{attribute of} we can choose to invoke it |
|
535 \emph{unchecked}. This avoids trying to do any type inference for the |
|
536 provided parameters, instead storing them as their most general type and |
|
537 doing type matching at run-time. This, like @{attribute OF}, will throw |
|
538 errors if the expected slots don't exist or there is a type mismatch. |
|
539 \<close> |
|
540 |
|
541 lemma |
|
542 fixes A B and x :: 'a and y :: 'b |
|
543 assumes asm: "\<And>x y. A y x \<Longrightarrow> B x y" |
|
544 shows "A y x \<Longrightarrow> B x y" |
|
545 by (match asm in I: "PROP ?P" \<Rightarrow> \<open>rule I [of (unchecked) y x]\<close>) |
|
546 |
|
547 text \<open> |
|
548 Attributes may be applied to matched facts directly as they are matched. Any |
|
549 declarations will therefore be applied in the context of the inner method, |
|
550 as well as any transformations to the rule. |
|
551 \<close> |
|
552 |
|
553 lemma "(\<And>x :: 'a. A x \<Longrightarrow> B x) \<Longrightarrow> A y \<longrightarrow> B y" |
|
554 by (match premises in I[of y, intros]: "\<And>x :: 'a. ?P x \<Longrightarrow> ?Q x" \<Rightarrow> |
|
555 \<open>prop_solver\<close>) |
|
556 |
|
557 text \<open> |
|
558 In this example, the pattern @{text "\<And>x :: 'a. ?P x \<Longrightarrow> ?Q x"} matches against |
|
559 the only premise, giving an appropriately typed slot for @{term y}. After |
|
560 the match, the resulting rule is instantiated to @{term y} and then declared |
|
561 as an @{attribute intros} rule. This is then picked up by @{method |
|
562 prop_solver} to solve the goal. |
|
563 \<close> |
|
564 |
|
565 |
|
566 section \<open>Multi-match \label{sec:multi}\<close> |
|
567 |
|
568 text \<open> |
|
569 In all previous examples, @{method match} was only ever searching for a |
|
570 single rule or premise. Each local fact would therefore always have a length |
|
571 of exactly one. We may, however, wish to find \emph{all} matching results. |
|
572 To achieve this, we can simply mark a given pattern with the @{text |
|
573 "(multi)"} argument. |
|
574 \<close> |
|
575 |
|
576 lemma |
|
577 assumes asms: "A \<Longrightarrow> B" "A \<Longrightarrow> D" |
|
578 shows "(A \<longrightarrow> B) \<and> (A \<longrightarrow> D)" |
|
579 apply (match asms in I[intros]: "?P \<Longrightarrow> ?Q" \<Rightarrow> \<open>solves \<open>prop_solver\<close>\<close>)? |
|
580 by (match asms in I[intros]: "?P \<Longrightarrow> ?Q" (multi) \<Rightarrow> \<open>prop_solver\<close>) |
|
581 |
|
582 text \<open> |
|
583 In the first @{method match}, without the @{text "(multi)"} argument, @{term |
|
584 I} is only ever be bound to one of the members of @{text asms}. This |
|
585 backtracks over both possibilities (see next section), however neither |
|
586 assumption in isolation is sufficient to solve to goal. The use of the |
|
587 @{method solves} combinator ensures that @{method prop_solver} has no effect |
|
588 on the goal when it doesn't solve it, and so the first match leaves the goal |
|
589 unchanged. In the second @{method match}, @{text I} is bound to all of |
|
590 @{text asms}, declaring both results as @{text intros}. With these rules |
|
591 @{method prop_solver} is capable of solving the goal. |
|
592 |
|
593 Using for-fixed variables in patterns imposes additional constraints on the |
|
594 results. In all previous examples, the choice of using @{text ?P} or a |
|
595 for-fixed @{term P} only depended on whether or not @{term P} was mentioned |
|
596 in another pattern or the inner method. When using a multi-match, however, |
|
597 all for-fixed terms must agree in the results. |
|
598 \<close> |
|
599 |
|
600 lemma |
|
601 assumes asms: "A \<Longrightarrow> B" "A \<Longrightarrow> D" "D \<Longrightarrow> B" |
|
602 shows "(A \<longrightarrow> B) \<and> (A \<longrightarrow> D)" |
|
603 apply (match asms in I[intros]: "?P \<Longrightarrow> Q" (multi) for Q \<Rightarrow> |
|
604 \<open>solves \<open>prop_solver\<close>\<close>)? |
|
605 by (match asms in I[intros]: "P \<Longrightarrow> ?Q" (multi) for P \<Rightarrow> |
|
606 \<open>prop_solver\<close>) |
|
607 |
|
608 text \<open> |
|
609 Here we have two seemingly-equivalent applications of @{method match}, |
|
610 however only the second one is capable of solving the goal. The first |
|
611 @{method match} selects the first and third members of @{text asms} (those |
|
612 that agree on their conclusion), which is not sufficient. The second |
|
613 @{method match} selects the first and second members of @{text asms} (those |
|
614 that agree on their assumption), which is enough for @{method prop_solver} |
|
615 to solve the goal. |
|
616 \<close> |
|
617 |
|
618 |
|
619 section \<open>Dummy patterns\<close> |
|
620 |
|
621 text \<open> |
|
622 Dummy patterns may be given as placeholders for unique schematics in |
|
623 patterns. They implicitly receive all currently bound variables as |
|
624 arguments, and are coerced into the @{typ prop} type whenever possible. For |
|
625 example, the trivial dummy pattern @{text "_"} will match any proposition. |
|
626 In contrast, by default the pattern @{text "?P"} is considered to have type |
|
627 @{typ bool}. It will not bind anything with meta-logical connectives (e.g. |
|
628 @{text "_ \<Longrightarrow> _"} or @{text "_ &&& _"}). |
|
629 \<close> |
|
630 |
|
631 lemma |
|
632 assumes asms: "A &&& B \<Longrightarrow> D" |
|
633 shows "(A \<and> B \<longrightarrow> D)" |
|
634 by (match asms in I:_ \<Rightarrow> \<open>prop_solver intros: I conjunctionI\<close>) |
|
635 |
|
636 |
|
637 section \<open>Backtracking\<close> |
|
638 |
|
639 text \<open> |
|
640 Patterns are considered top-down, executing the inner method @{text m} of |
|
641 the first pattern which is satisfied by the current match target. By |
|
642 default, matching performs extensive backtracking by attempting all valid |
|
643 variable and fact bindings according to the given pattern. In particular, |
|
644 all unifiers for a given pattern will be explored, as well as each matching |
|
645 fact. The inner method @{text m} will be re-executed for each different |
|
646 variable/fact binding during backtracking. A successful match is considered |
|
647 a cut-point for backtracking. Specifically, once a match is made no other |
|
648 pattern-method pairs will be considered. |
|
649 |
|
650 The method @{text foo} below fails for all goals that are conjunctions. Any |
|
651 such goal will match the first pattern, causing the second pattern (that |
|
652 would otherwise match all goals) to never be considered. If multiple |
|
653 unifiers exist for the pattern @{text "?P \<and> ?Q"} against the current goal, |
|
654 then the failing method @{method fail} will be (uselessly) tried for all of |
|
655 them. |
|
656 \<close> |
|
657 |
|
658 method foo = |
|
659 (match conclusion in "?P \<and> ?Q" \<Rightarrow> \<open>fail\<close> \<bar> "?R" \<Rightarrow> \<open>prop_solver\<close>) |
|
660 |
|
661 text \<open> |
|
662 This behaviour is in direct contrast to the backtracking done by Coq's Ltac, |
|
663 which will attempt all patterns in a match before failing. This means that |
|
664 the failure of an inner method that is executed after a successful match |
|
665 does not, in Ltac, cause the entire match to fail, whereas it does in |
|
666 Eisbach. In Eisbach the distinction is important due to the pervasive use of |
|
667 backtracking. When a method is used in a combinator chain, its failure |
|
668 becomes significant because it signals previously applied methods to move to |
|
669 the next result. Therefore, it is necessary for @{method match} to not mask |
|
670 such failure. One can always rewrite a match using the combinators ``@{text |
|
671 "?"}'' and ``@{text "|"}'' to try subsequent patterns in the case of an |
|
672 inner-method failure. The following proof method, for example, always |
|
673 invokes @{method prop_solver} for all goals because its first alternative |
|
674 either never matches or (if it does match) always fails. |
|
675 \<close> |
|
676 |
|
677 method foo\<^sub>1 = |
|
678 (match conclusion in "?P \<and> ?Q" \<Rightarrow> \<open>fail\<close>) | |
|
679 (match conclusion in "?R" \<Rightarrow> \<open>prop_solver\<close>) |
|
680 |
|
681 |
|
682 subsection \<open>Cut\<close> |
|
683 |
|
684 text \<open> |
|
685 Backtracking may be controlled more precisely by marking individual patterns |
|
686 as \emph{cut}. This causes backtracking to not progress beyond this pattern: |
|
687 once a match is found no others will be considered. |
|
688 \<close> |
|
689 |
|
690 method foo\<^sub>2 = |
|
691 (match premises in I: "P \<and> Q" (cut) and I': "P \<longrightarrow> ?U" for P Q \<Rightarrow> |
|
692 \<open>rule mp [OF I' I [THEN conjunct1]]\<close>) |
|
693 |
|
694 text \<open> |
|
695 In this example, once a conjunction is found (@{term "P \<and> Q"}), all possible |
|
696 implications of @{term "P"} in the premises are considered, evaluating the |
|
697 inner @{method rule} with each consequent. No other conjunctions will be |
|
698 considered, with method failure occurring once all implications of the |
|
699 form @{text "P \<longrightarrow> ?U"} have been explored. Here the left-right processing of |
|
700 individual patterns is important, as all patterns after of the cut will |
|
701 maintain their usual backtracking behaviour. |
|
702 \<close> |
|
703 |
|
704 lemma "A \<and> B \<Longrightarrow> A \<longrightarrow> D \<Longrightarrow> A \<longrightarrow> C \<Longrightarrow> C" |
|
705 by foo\<^sub>2 |
|
706 |
|
707 lemma "C \<and> D \<Longrightarrow> A \<and> B \<Longrightarrow> A \<longrightarrow> C \<Longrightarrow> C" |
|
708 by (foo\<^sub>2 | prop_solver) |
|
709 |
|
710 text \<open> |
|
711 In this example, the first lemma is solved by @{text foo\<^sub>2}, by first |
|
712 picking @{term "A \<longrightarrow> D"} for @{text I'}, then backtracking and ultimately |
|
713 succeeding after picking @{term "A \<longrightarrow> C"}. In the second lemma, however, |
|
714 @{term "C \<and> D"} is matched first, the second pattern in the match cannot be |
|
715 found and so the method fails, falling through to @{method prop_solver}. |
|
716 \<close> |
|
717 |
|
718 |
|
719 subsection \<open>Multi-match revisited\<close> |
|
720 |
|
721 text \<open> |
|
722 A multi-match will produce a sequence of potential bindings for for-fixed |
|
723 variables, where each binding environment is the result of matching against |
|
724 at least one element from the match target. For each environment, the match |
|
725 result will be all elements of the match target which agree with the pattern |
|
726 under that environment. This can result in unexpected behaviour when giving |
|
727 very general patterns. |
|
728 \<close> |
|
729 |
|
730 lemma |
|
731 assumes asms: "\<And>x. A x \<and> B x" "\<And>y. A y \<and> C y" "\<And>z. B z \<and> C z" |
|
732 shows "A x \<and> C x" |
|
733 by (match asms in I: "\<And>x. P x \<and> ?Q x" (multi) for P \<Rightarrow> |
|
734 \<open>match (P) in "A" \<Rightarrow> \<open>fail\<close> |
|
735 \<bar> _ \<Rightarrow> \<open>match I in "\<And>x. A x \<and> B x" \<Rightarrow> \<open>fail\<close> |
|
736 \<bar> _ \<Rightarrow> \<open>rule I\<close>\<close>\<close>) |
|
737 |
|
738 text \<open> |
|
739 Intuitively it seems like this proof should fail to check. The first match |
|
740 result, which binds @{term I} to the first two members of @{text asms}, |
|
741 fails the second inner match due to binding @{term P} to @{term A}. |
|
742 Backtracking then attempts to bind @{term I} to the third member of @{text |
|
743 asms}. This passes all inner matches, but fails when @{method rule} cannot |
|
744 successfully apply this to the current goal. After this, a valid match that |
|
745 is produced by the unifier is one which binds @{term P} to simply @{text |
|
746 "\<lambda>a. A ?x"}. The first inner match succeeds because @{text "\<lambda>a. A ?x"} does |
|
747 not match @{term A}. The next inner match succeeds because @{term I} has |
|
748 only been bound to the first member of @{text asms}. This is due to @{method |
|
749 match} considering @{text "\<lambda>a. A ?x"} and @{text "\<lambda>a. A ?y"} as distinct |
|
750 terms. |
|
751 |
|
752 The simplest way to address this is to explicitly disallow term bindings |
|
753 which we would consider invalid. |
|
754 \<close> |
|
755 |
|
756 method abs_used for P = |
|
757 (match (P) in "\<lambda>a. ?P" \<Rightarrow> \<open>fail\<close> \<bar> _ \<Rightarrow> \<open>-\<close>) |
|
758 |
|
759 text \<open> |
|
760 This method has no effect on the goal state, but instead serves as a filter |
|
761 on the environment produced from match. |
|
762 \<close> |
|
763 |
|
764 |
|
765 section \<open>Uncurrying\<close> |
|
766 |
|
767 text \<open> |
|
768 The @{method match} method is not aware of the logical content of match |
|
769 targets. Each pattern is simply matched against the shallow structure of a |
|
770 fact or term. Most facts are in \emph{normal form}, which curries premises |
|
771 via meta-implication @{text "_ \<Longrightarrow> _"}. |
|
772 \<close> |
|
773 |
|
774 lemma |
|
775 assumes asms: "D \<Longrightarrow> B \<Longrightarrow> C" "D \<Longrightarrow> A" |
|
776 shows "D \<Longrightarrow> B \<Longrightarrow> C \<and> A" |
|
777 by (match asms in H:"D \<Longrightarrow> _" (multi) \<Rightarrow> \<open>prop_solver elims: H\<close>) |
|
778 |
|
779 text \<open> |
|
780 For the first member of @{text asms} the dummy pattern successfully matches |
|
781 against @{term "B \<Longrightarrow> C"} and so the proof is successful. |
|
782 \<close> |
|
783 |
|
784 lemma |
|
785 assumes asms: "A \<Longrightarrow> B \<Longrightarrow> C" "D \<Longrightarrow> C" |
|
786 shows "D \<or> (A \<and> B) \<Longrightarrow> C" |
|
787 apply (match asms in H:"_ \<Longrightarrow> C" (multi) \<Rightarrow> \<open>prop_solver elims: H\<close>)(*<*)? |
|
788 by (prop_solver elims: asms)(*>*) |
|
789 |
|
790 text \<open> |
|
791 This proof will fail to solve the goal. Our match pattern will only match |
|
792 rules which have a single premise, and conclusion @{term C}, so the first |
|
793 member of @{text asms} is not bound and thus the proof fails. Matching a |
|
794 pattern of the form @{term "P \<Longrightarrow> Q"} against this fact will bind @{term "P"} |
|
795 to @{term "A"} and @{term Q} to @{term "B \<Longrightarrow> C"}. Our pattern, with a |
|
796 concrete @{term "C"} in the conclusion, will fail to match this fact. |
|
797 |
|
798 To express our desired match, we may \emph{uncurry} our rules before |
|
799 matching against them. This forms a meta-conjunction of all premises in a |
|
800 fact, so that only one implication remains. For example the uncurried |
|
801 version of @{term "A \<Longrightarrow> B \<Longrightarrow> C"} is @{term "A &&& B \<Longrightarrow> C"}. This will now match |
|
802 our desired pattern @{text "_ \<Longrightarrow> C"}, and can be \emph{curried} after the |
|
803 match to put it back into normal form. |
|
804 \<close> |
|
805 |
|
806 lemma |
|
807 assumes asms: "A \<Longrightarrow> B \<Longrightarrow> C" "D \<Longrightarrow> C" |
|
808 shows "D \<or> (A \<and> B) \<Longrightarrow> C" |
|
809 by (match asms[uncurry] in H[curry]:"_ \<Longrightarrow> C" (multi) \<Rightarrow> |
|
810 \<open>prop_solver elims: H\<close>) |
|
811 |
|
812 |
|
813 section \<open>Reverse matching\<close> |
|
814 |
|
815 text \<open> |
|
816 The @{method match} method only attempts to perform matching of the pattern |
|
817 against the match target. Specifically this means that it will not |
|
818 instantiate schematic terms in the match target. |
|
819 \<close> |
|
820 |
|
821 lemma |
|
822 assumes asms: "\<And>x :: 'a. A x" |
|
823 shows "A y" |
|
824 apply (match asms in H:"A y" \<Rightarrow> \<open>rule H\<close>)? |
|
825 by (match asms in H:"P" for P \<Rightarrow> |
|
826 \<open>match ("A y") in "P" \<Rightarrow> \<open>rule H\<close>\<close>) |
|
827 |
|
828 text \<open> |
|
829 In the first @{method match} we attempt to find a member of @{text asms} |
|
830 which matches our goal precisely. This fails due to no such member existing. |
|
831 The second match reverses the role of the fact in the match, by first giving |
|
832 a general pattern @{term P}. This bound pattern is then matched against |
|
833 @{term "A y"}. In this case, @{term P} is bound to @{text "A ?x"} and so it |
|
834 successfully matches. |
|
835 \<close> |
|
836 |
|
837 |
|
838 section \<open>Type matching\<close> |
|
839 |
|
840 text \<open> |
|
841 The rule instantiation attributes @{attribute "where"} and @{attribute "of"} |
|
842 attempt to guarantee type-correctness wherever possible. This can require |
|
843 additional invocations of @{method match} in order to statically ensure that |
|
844 instantiation will succeed. |
|
845 \<close> |
|
846 |
|
847 lemma |
|
848 assumes asms: "\<And>x :: 'a. A x" |
|
849 shows "A y" |
|
850 by (match asms in H:"\<And>z :: 'b. P z" for P \<Rightarrow> |
|
851 \<open>match (y) in "y :: 'b" for y \<Rightarrow> \<open>rule H[where z=y]\<close>\<close>) |
|
852 |
|
853 text \<open> |
|
854 In this example the type @{text 'b} is matched to @{text 'a}, however |
|
855 statically they are formally distinct types. The first match binds @{text |
|
856 'b} while the inner match serves to coerce @{term y} into having the type |
|
857 @{text 'b}. This allows the rule instantiation to successfully apply. |
|
858 \<close> |
|
859 |
|
860 |
|
861 chapter \<open>Method development\<close> |
|
862 |
|
863 section \<open>Tracing methods\<close> |
|
864 |
|
865 text \<open> |
|
866 Method tracing is supported by auxiliary print methods provided by @{theory |
|
867 Eisbach_Tools}. These include @{method print_fact}, @{method print_term} and |
|
868 @{method print_type}. Whenever a print method is evaluated it leaves the |
|
869 goal unchanged and writes its argument as tracing output. |
|
870 |
|
871 Print methods can be combined with the @{method fail} method to investigate |
|
872 the backtracking behaviour of a method. |
|
873 \<close> |
|
874 |
|
875 lemma |
|
876 assumes asms: A B C D |
|
877 shows D |
|
878 apply (match asms in H:_ \<Rightarrow> \<open>print_fact H, fail\<close>)(*<*)? |
|
879 by (simp add: asms)(*>*) |
|
880 |
|
881 text \<open> |
|
882 This proof will fail, but the tracing output will show the order that the |
|
883 assumptions are attempted. |
|
884 \<close> |
|
885 |
|
886 |
|
887 section \<open>Integrating with Isabelle/ML\<close> |
|
888 |
|
889 subsection \<open>Attributes\<close> |
|
890 |
|
891 text \<open> |
|
892 A custom rule attribute is a simple way to extend the functionality of |
|
893 Eisbach methods. The dummy rule attribute notation (@{text "[[ _ ]]"}) |
|
894 invokes the given attribute against a dummy fact and evaluates to the result |
|
895 of that attribute. When used as a match target, this can serve as an |
|
896 effective auxiliary function. |
|
897 \<close> |
|
898 |
|
899 attribute_setup get_split_rule = |
|
900 \<open>Args.term >> (fn t => |
|
901 Thm.rule_attribute (fn context => fn _ => |
|
902 (case get_split_rule (Context.proof_of context) t of |
|
903 SOME thm => thm |
|
904 | NONE => Drule.dummy_thm)))\<close> |
|
905 |
|
906 text \<open> |
|
907 In this example, the new attribute @{attribute get_split_rule} lifts the ML |
|
908 function of the same name into an attribute. When applied to a cast |
|
909 distinction over a datatype, it retrieves its corresponding split rule. |
|
910 |
|
911 We can then integrate this intro a method that applies the split rule, fist |
|
912 matching to ensure that fetching the rule was successful. |
|
913 \<close> |
|
914 |
|
915 method splits = |
|
916 (match conclusion in "?P f" for f \<Rightarrow> |
|
917 \<open>match [[get_split_rule f]] in U: "(_ :: bool) = _" \<Rightarrow> |
|
918 \<open>rule U[THEN iffD2]\<close>\<close>) |
|
919 |
|
920 lemma "L \<noteq> [] \<Longrightarrow> case L of [] \<Rightarrow> False | _ \<Rightarrow> True" |
|
921 by (splits, prop_solver intros: allI) |
|
922 |
|
923 end |