54 (that is @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"} in the proof at hand) under the |
54 (that is @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"} in the proof at hand) under the |
55 assumptions @{text As} (happens to be empty) with the variables |
55 assumptions @{text As} (happens to be empty) with the variables |
56 @{text xs} that will be generalised once the goal is proved (in our case |
56 @{text xs} that will be generalised once the goal is proved (in our case |
57 @{text P} and @{text Q}). The @{text "tac"} is the tactic that proves the goal; |
57 @{text P} and @{text Q}). The @{text "tac"} is the tactic that proves the goal; |
58 it can make use of the local assumptions (there are none in this example). |
58 it can make use of the local assumptions (there are none in this example). |
59 The functions @{ML etac}, @{ML rtac} and @{ML atac} in the code above correspond to |
59 The tactics @{ML etac}, @{ML rtac} and @{ML atac} in the code above correspond |
60 @{text erule}, @{text rule} and @{text assumption}, respectively. |
60 roughly to @{text erule}, @{text rule} and @{text assumption}, respectively. |
61 The operator @{ML THEN} strings the tactics together. |
61 The operator @{ML THEN} strings the tactics together. |
62 |
62 |
63 \begin{readmore} |
63 \begin{readmore} |
64 To learn more about the function @{ML Goal.prove} see \isccite{sec:results} |
64 To learn more about the function @{ML Goal.prove} see \isccite{sec:results} |
65 and the file @{ML_file "Pure/goal.ML"}. See @{ML_file |
65 and the file @{ML_file "Pure/goal.ML"}. See @{ML_file |
143 \begin{isabelle} |
143 \begin{isabelle} |
144 @{text "*** empty result sequence -- proof command failed"}\\ |
144 @{text "*** empty result sequence -- proof command failed"}\\ |
145 @{text "*** At command \"apply\"."} |
145 @{text "*** At command \"apply\"."} |
146 \end{isabelle} |
146 \end{isabelle} |
147 |
147 |
148 This means they failed. The reason for this error message is that tactics |
148 This means they failed.\footnote{To be precise tactics do not produce this error |
|
149 message, the it originates from the \isacommand{apply} wrapper.} The reason for this |
|
150 error message is that tactics |
149 are functions mapping a goal state to a (lazy) sequence of successor states. |
151 are functions mapping a goal state to a (lazy) sequence of successor states. |
150 Hence the type of a tactic is: |
152 Hence the type of a tactic is: |
151 *} |
153 *} |
152 |
154 |
153 ML{*type tactic = thm -> thm Seq.seq*} |
155 ML{*type tactic = thm -> thm Seq.seq*} |
308 @{text[display] "A\<^isub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^isub>n \<Longrightarrow> (C)"} |
310 @{text[display] "A\<^isub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^isub>n \<Longrightarrow> (C)"} |
309 |
311 |
310 where @{term C} is the goal to be proved and the @{term "A\<^isub>i"} are |
312 where @{term C} is the goal to be proved and the @{term "A\<^isub>i"} are |
311 the subgoals. So after setting up the lemma, the goal state is always of the |
313 the subgoals. So after setting up the lemma, the goal state is always of the |
312 form @{text "C \<Longrightarrow> (C)"}; when the proof is finished we are left with @{text |
314 form @{text "C \<Longrightarrow> (C)"}; when the proof is finished we are left with @{text |
313 "(C)"}. Since the goal @{term C} can potentially be an implication, there is |
315 "(C)"}.\footnote{This only applies to single statements. If the lemma |
314 a ``protector'' wrapped around it (the wrapper is the outermost constant @{text |
316 contains more than one statement, then one has more such implications.} |
315 "Const (\"prop\", bool \<Rightarrow> bool)"}; however this constant |
317 Since the goal @{term C} can potentially be an implication, there is a |
316 is invisible in the figure). This wrapper prevents that premises of @{text C} are |
318 ``protector'' wrapped around it (the wrapper is the outermost constant |
|
319 @{text "Const (\"prop\", bool \<Rightarrow> bool)"}; however this constant is invisible |
|
320 in the figure). This wrapper prevents that premises of @{text C} are |
317 misinterpreted as open subgoals. While tactics can operate on the subgoals |
321 misinterpreted as open subgoals. While tactics can operate on the subgoals |
318 (the @{text "A\<^isub>i"} above), they are expected to leave the conclusion |
322 (the @{text "A\<^isub>i"} above), they are expected to leave the conclusion |
319 @{term C} intact, with the exception of possibly instantiating schematic |
323 @{term C} intact, with the exception of possibly instantiating schematic |
320 variables. If you use the predefined tactics, which we describe in the next |
324 variables. If you use the predefined tactics, which we describe in the next |
321 section, this will always be the case. |
325 section, this will always be the case. |
360 @{subgoals [display]} |
364 @{subgoals [display]} |
361 \end{minipage}*} |
365 \end{minipage}*} |
362 (*<*)oops(*>*) |
366 (*<*)oops(*>*) |
363 |
367 |
364 text {* |
368 text {* |
|
369 This tactic works however only if the quick-and-dirty mode of Isabelle |
|
370 is switched on. |
|
371 |
365 Another simple tactic is the function @{ML atac}, which, as shown in the previous |
372 Another simple tactic is the function @{ML atac}, which, as shown in the previous |
366 section, corresponds to the assumption command. |
373 section, corresponds to the assumption command. |
367 *} |
374 *} |
368 |
375 |
369 lemma shows "P \<Longrightarrow> P" |
376 lemma shows "P \<Longrightarrow> P" |
372 @{subgoals [display]} |
379 @{subgoals [display]} |
373 \end{minipage}*} |
380 \end{minipage}*} |
374 (*<*)oops(*>*) |
381 (*<*)oops(*>*) |
375 |
382 |
376 text {* |
383 text {* |
377 Similarly, @{ML rtac}, @{ML dtac}, @{ML etac} and @{ML ftac} correspond |
384 Similarly, @{ML rtac}, @{ML dtac}, @{ML etac} and @{ML ftac} correspond (roughly) |
378 to @{text rule}, @{text drule}, @{text erule} and @{text frule}, |
385 to @{text rule}, @{text drule}, @{text erule} and @{text frule}, |
379 respectively. Each of them take a theorem as argument and attempt to |
386 respectively. Each of them take a theorem as argument and attempt to |
380 apply it to a goal. Below are three self-explanatory examples. |
387 apply it to a goal. Below are three self-explanatory examples. |
381 *} |
388 *} |
382 |
389 |
459 where the application of rule @{text bspec} generates two subgoals involving the |
466 where the application of rule @{text bspec} generates two subgoals involving the |
460 meta-variable @{text "?x"}. Now, if you are not careful, tactics |
467 meta-variable @{text "?x"}. Now, if you are not careful, tactics |
461 applied to the first subgoal might instantiate this meta-variable in such a |
468 applied to the first subgoal might instantiate this meta-variable in such a |
462 way that the second subgoal becomes unprovable. If it is clear what the @{text "?x"} |
469 way that the second subgoal becomes unprovable. If it is clear what the @{text "?x"} |
463 should be, then this situation can be avoided by introducing a more |
470 should be, then this situation can be avoided by introducing a more |
464 constraint version of the @{text bspec}-rule. Such constraints can be given by |
471 constrained version of the @{text bspec}-rule. Such constraints can be given by |
465 pre-instantiating theorems with other theorems. One function to do this is |
472 pre-instantiating theorems with other theorems. One function to do this is |
466 @{ML RS} |
473 @{ML RS} |
467 |
474 |
468 @{ML_response_fake [display,gray] |
475 @{ML_response_fake [display,gray] |
469 "@{thm disjI1} RS @{thm conjI}" "\<lbrakk>?P1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q"} |
476 "@{thm disjI1} RS @{thm conjI}" "\<lbrakk>?P1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q"} |
514 \end{readmore} |
521 \end{readmore} |
515 |
522 |
516 Often proofs on the ML-level involve elaborate operations on assumptions and |
523 Often proofs on the ML-level involve elaborate operations on assumptions and |
517 @{text "\<And>"}-quantified variables. To do such operations using the basic tactics |
524 @{text "\<And>"}-quantified variables. To do such operations using the basic tactics |
518 shown so far is very unwieldy and brittle. Some convenience and |
525 shown so far is very unwieldy and brittle. Some convenience and |
519 safety is provided by the tactic @{ML SUBPROOF}. This tactic fixes the parameters |
526 safety is provided by @{ML SUBPROOF}. This tactic fixes the parameters |
520 and binds the various components of a goal state to a record. |
527 and binds the various components of a goal state to a record. |
521 To see what happens, assume the function defined in Figure~\ref{fig:sptac}, which |
528 To see what happens, assume the function defined in Figure~\ref{fig:sptac}, which |
522 takes a record and just prints out the content of this record (using the |
529 takes a record and just prints out the content of this record (using the |
523 string transformation functions from in Section~\ref{sec:printing}). Consider |
530 string transformation functions from in Section~\ref{sec:printing}). Consider |
524 now the proof: |
531 now the proof: |
627 txt{* it will produce |
634 txt{* it will produce |
628 @{subgoals [display]} *} |
635 @{subgoals [display]} *} |
629 (*<*)oops(*>*) |
636 (*<*)oops(*>*) |
630 |
637 |
631 text {* |
638 text {* |
632 The restriction in this tactic which is not present in @{ML atac} is |
639 The restriction in this tactic which is not present in @{ML atac} is that it |
633 that it cannot instantiate any |
640 cannot instantiate any schematic variables. This might be seen as a defect, |
634 schematic variable. This might be seen as a defect, but it is actually |
641 but it is actually an advantage in the situations for which @{ML SUBPROOF} |
635 an advantage in the situations for which @{ML SUBPROOF} was designed: |
642 was designed: the reason is that, as mentioned before, instantiation of |
636 the reason is that, as mentioned before, instantiation of schematic variables can affect |
643 schematic variables can affect several goals and can render them |
637 several goals and can render them unprovable. @{ML SUBPROOF} is meant |
644 unprovable. @{ML SUBPROOF} is meant to avoid this. |
638 to avoid this. |
645 |
639 |
646 Notice that @{ML atac'} inside @{ML SUBPROOF} calls @{ML resolve_tac} with |
640 Notice that @{ML atac'} inside @{ML SUBPROOF} calls @{ML resolve_tac} with |
647 the subgoal number @{text "1"} and also the outer call to @{ML SUBPROOF} in |
641 the subgoal number @{text "1"} and also the outer call to @{ML SUBPROOF} in |
648 the \isacommand{apply}-step uses @{text "1"}. This is another advantage of |
642 the \isacommand{apply}-step uses @{text "1"}. This is another advantage |
649 @{ML SUBPROOF}: the addressing inside it is completely local to the tactic |
643 of @{ML SUBPROOF}: the addressing inside it is completely |
650 inside the subproof. It is therefore possible to also apply @{ML atac'} to |
644 local to the tactic inside the subproof. It is therefore possible to also apply |
651 the second goal by just writing: |
645 @{ML atac'} to the second goal by just writing: |
|
646 *} |
652 *} |
647 |
653 |
648 lemma shows "True" and "\<lbrakk>B x y; A x y; C x y\<rbrakk> \<Longrightarrow> A x y" |
654 lemma shows "True" and "\<lbrakk>B x y; A x y; C x y\<rbrakk> \<Longrightarrow> A x y" |
649 apply(tactic {* atac' @{context} 2 *}) |
655 apply(tactic {* atac' @{context} 2 *}) |
650 apply(rule TrueI) |
656 apply(rule TrueI) |