77 tactics and tactic combinators; see also Chapters 3 and 4 in the old |
79 tactics and tactic combinators; see also Chapters 3 and 4 in the old |
78 Isabelle Reference Manual, and Chapter 3 in the Isabelle/Isar Implementation |
80 Isabelle Reference Manual, and Chapter 3 in the Isabelle/Isar Implementation |
79 Manual. |
81 Manual. |
80 \end{readmore} |
82 \end{readmore} |
81 |
83 |
82 Note that in the code above we use antiquotations for referencing the |
|
83 theorems. We could also just have written @{ML "etac disjE 1"} because |
|
84 many of the basic theorems have a corresponding ML-binding: |
|
85 |
|
86 @{ML_response_fake [gray,display] |
|
87 "disjE" |
|
88 "\<lbrakk>?P \<or> ?Q; ?P \<Longrightarrow> ?R; ?Q \<Longrightarrow> ?R\<rbrakk> \<Longrightarrow> ?R"} |
|
89 |
|
90 In case where no ML-binding exists, theorems can also be looked up dynamically |
|
91 using the function @{ML thm} and the (string) name of the theorem. For example: |
|
92 |
|
93 @{ML_response_fake [gray,display] |
|
94 "thm \"disjE\"" |
|
95 "\<lbrakk>?P \<or> ?Q; ?P \<Longrightarrow> ?R; ?Q \<Longrightarrow> ?R\<rbrakk> \<Longrightarrow> ?R"} |
|
96 |
|
97 Both ways however are considered \emph{bad} style! The reason is that the binding |
|
98 for @{ML disjE} can be re-assigned and thus one does not have |
|
99 complete control over which theorem is actually applied. Similarly with the |
|
100 lookup of @{text [quotes] "disjE"}. Although theorems must have a unique name |
|
101 in the theorem database, the string can stand for a dynamically updatable |
|
102 theorem list. Also in this case we cannot be sure which theorem is applied. |
|
103 These problems can be nicely prevented by using antiquotations |
|
104 |
|
105 @{ML_response_fake [gray,display] |
|
106 "@{thm \"disjE\"}" |
|
107 "\<lbrakk>?P \<or> ?Q; ?P \<Longrightarrow> ?R; ?Q \<Longrightarrow> ?R\<rbrakk> \<Longrightarrow> ?R"} |
|
108 |
|
109 because then the theorems are fixed statically at compile-time. |
|
110 |
84 |
111 \index{tactic@ {\tt\slshape{}tactic}} |
85 \index{tactic@ {\tt\slshape{}tactic}} |
112 \index{raw\_tactic@ {\tt\slshape{}raw\_tactic}} |
86 \index{raw\_tactic@ {\tt\slshape{}raw\_tactic}} |
113 During the development of automatic proof procedures, you will often find it |
87 During the development of automatic proof procedures, you will often find it |
114 necessary to test a tactic on examples. This can be conveniently done with |
88 necessary to test a tactic on examples. This can be conveniently done with |
662 and "\<lbrakk>B x y; A x y; C x y\<rbrakk> \<Longrightarrow> A x y" |
636 and "\<lbrakk>B x y; A x y; C x y\<rbrakk> \<Longrightarrow> A x y" |
663 apply(tactic {* atac' @{context} 2 *}) |
637 apply(tactic {* atac' @{context} 2 *}) |
664 apply(rule TrueI) |
638 apply(rule TrueI) |
665 done |
639 done |
666 |
640 |
667 |
641 text {* |
668 text {* |
642 To sum up, both @{ML FOCUS in Subgoal} and @{ML SUBPROOF} are rather |
669 There is one peculiarity about @{ML FOCUS in Subgoal} and @{ML SUBPROOF}. |
|
670 If we apply @{text "rtac @{thm allI}"} in the proof below |
|
671 *} |
|
672 |
|
673 lemma |
|
674 shows "B \<Longrightarrow> \<forall>x. A x" |
|
675 apply(tactic {* rtac @{thm allI} 1 *}) |
|
676 txt{* it will produce the expected goal state |
|
677 @{subgoals [display]} *} |
|
678 (*<*)oops(*>*) |
|
679 |
|
680 text {* But if we apply the same tactic inside @{ML FOCUS in Subgoal} |
|
681 we obtain |
|
682 *} |
|
683 |
|
684 lemma |
|
685 shows "B \<Longrightarrow> \<forall>x. A x" |
|
686 apply(tactic {* Subgoal.FOCUS (fn _ => rtac @{thm allI} 1) @{context} 1 *}) |
|
687 txt{* it will produce the goal state |
|
688 @{subgoals [display]} |
|
689 |
|
690 If we want to imitate the behaviour of the ``plain'' tactic, then we |
|
691 can apply the tactic @{ML norm_hhf_tac in Goal}. This gives |
|
692 *} |
|
693 apply(tactic {* Goal.norm_hhf_tac 1 *}) |
|
694 txt{*@{subgoals [display]}*} |
|
695 (*<*)oops(*>*) |
|
696 |
|
697 text {* |
|
698 This tactic transforms the goal state into a \emph{hereditary Harrop normal |
|
699 form}. To sum up, both @{ML FOCUS in Subgoal} and @{ML SUBPROOF} are rather |
|
700 convenient, but can impose a considerable run-time penalty in automatic |
643 convenient, but can impose a considerable run-time penalty in automatic |
701 proofs. If speed is of the essence, then maybe the two lower level combinators |
644 proofs. If speed is of the essence, then maybe the two lower level combinators |
702 described next are more appropriate. |
645 described next are more appropriate. |
703 |
646 |
704 |
647 |