106 The tactic @{ML foo_tac} is just a sequence of simple tactics stringed |
106 The tactic @{ML foo_tac} is just a sequence of simple tactics stringed |
107 together by @{ML THEN}. As can be seen, each simple tactic in @{ML foo_tac} |
107 together by @{ML THEN}. As can be seen, each simple tactic in @{ML foo_tac} |
108 has a hard-coded number that stands for the subgoal analysed by the |
108 has a hard-coded number that stands for the subgoal analysed by the |
109 tactic (@{text "1"} stands for the first, or top-most, subgoal). This hard-coding |
109 tactic (@{text "1"} stands for the first, or top-most, subgoal). This hard-coding |
110 of goals is sometimes wanted, but usually it is not. To avoid the explicit numbering, |
110 of goals is sometimes wanted, but usually it is not. To avoid the explicit numbering, |
111 you can write\label{tac:footacprime} |
111 you can write |
112 *} |
112 *} |
113 |
113 |
114 ML{*val foo_tac' = |
114 ML{*val foo_tac' = |
115 (etac @{thm disjE} |
115 (etac @{thm disjE} |
116 THEN' rtac @{thm disjI2} |
116 THEN' rtac @{thm disjI2} |
117 THEN' atac |
117 THEN' atac |
118 THEN' rtac @{thm disjI1} |
118 THEN' rtac @{thm disjI1} |
119 THEN' atac)*} |
119 THEN' atac)*}text_raw{*\label{tac:footacprime}*} |
120 |
120 |
121 text {* |
121 text {* |
122 where @{ML THEN'} is used instead of @{ML THEN}. With @{ML foo_tac'} you can give |
122 where @{ML THEN'} is used instead of @{ML THEN}. With @{ML foo_tac'} you can give |
123 the number for the subgoal explicitly when the tactic is |
123 the number for the subgoal explicitly when the tactic is |
124 called. So in the next proof you can first discharge the second subgoal, and |
124 called. So in the next proof you can first discharge the second subgoal, and |
406 expects a list of theorems as arguments. From this list it will apply the |
406 expects a list of theorems as arguments. From this list it will apply the |
407 first applicable theorem (later theorems that are also applicable can be |
407 first applicable theorem (later theorems that are also applicable can be |
408 explored via the lazy sequences mechanism). Given the code |
408 explored via the lazy sequences mechanism). Given the code |
409 *} |
409 *} |
410 |
410 |
411 ML{*val resolve_tac_xmp = resolve_tac [@{thm impI}, @{thm conjI}]*} |
411 ML{*val resolve_xmp_tac = resolve_tac [@{thm impI}, @{thm conjI}]*} |
412 |
412 |
413 text {* |
413 text {* |
414 an example for @{ML resolve_tac} is the following proof where first an outermost |
414 an example for @{ML resolve_tac} is the following proof where first an outermost |
415 implication is analysed and then an outermost conjunction. |
415 implication is analysed and then an outermost conjunction. |
416 *} |
416 *} |
417 |
417 |
418 lemma shows "C \<longrightarrow> (A \<and> B)" and "(A \<longrightarrow> B) \<and> C" |
418 lemma shows "C \<longrightarrow> (A \<and> B)" and "(A \<longrightarrow> B) \<and> C" |
419 apply(tactic {* resolve_tac_xmp 1 *}) |
419 apply(tactic {* resolve_xmp_tac 1 *}) |
420 apply(tactic {* resolve_tac_xmp 2 *}) |
420 apply(tactic {* resolve_xmp_tac 2 *}) |
421 txt{*\begin{minipage}{\textwidth} |
421 txt{*\begin{minipage}{\textwidth} |
422 @{subgoals [display]} |
422 @{subgoals [display]} |
423 \end{minipage}*} |
423 \end{minipage}*} |
424 (*<*)oops(*>*) |
424 (*<*)oops(*>*) |
425 |
425 |
661 and @{ML CSUBGOAL}. They allow you to inspect a given subgoal (the former |
661 and @{ML CSUBGOAL}. They allow you to inspect a given subgoal (the former |
662 presents the subgoal as a @{ML_type term}, while the latter as a @{ML_type |
662 presents the subgoal as a @{ML_type term}, while the latter as a @{ML_type |
663 cterm}). With this you can implement a tactic that applies a rule according |
663 cterm}). With this you can implement a tactic that applies a rule according |
664 to the topmost logic connective in the subgoal (to illustrate this we only |
664 to the topmost logic connective in the subgoal (to illustrate this we only |
665 analyse a few connectives). The code of the tactic is as |
665 analyse a few connectives). The code of the tactic is as |
666 follows.\label{tac:selecttac} |
666 follows. |
667 |
|
668 *} |
667 *} |
669 |
668 |
670 ML %linenosgray{*fun select_tac (t, i) = |
669 ML %linenosgray{*fun select_tac (t, i) = |
671 case t of |
670 case t of |
672 @{term "Trueprop"} $ t' => select_tac (t', i) |
671 @{term "Trueprop"} $ t' => select_tac (t', i) |
673 | @{term "op \<Longrightarrow>"} $ _ $ t' => select_tac (t', i) |
672 | @{term "op \<Longrightarrow>"} $ _ $ t' => select_tac (t', i) |
674 | @{term "op \<and>"} $ _ $ _ => rtac @{thm conjI} i |
673 | @{term "op \<and>"} $ _ $ _ => rtac @{thm conjI} i |
675 | @{term "op \<longrightarrow>"} $ _ $ _ => rtac @{thm impI} i |
674 | @{term "op \<longrightarrow>"} $ _ $ _ => rtac @{thm impI} i |
676 | @{term "Not"} $ _ => rtac @{thm notI} i |
675 | @{term "Not"} $ _ => rtac @{thm notI} i |
677 | Const (@{const_name "All"}, _) $ _ => rtac @{thm allI} i |
676 | Const (@{const_name "All"}, _) $ _ => rtac @{thm allI} i |
678 | _ => all_tac*} |
677 | _ => all_tac*}text_raw{*\label{tac:selecttac}*} |
679 |
678 |
680 text {* |
679 text {* |
681 The input of the function is a term representing the subgoal and a number |
680 The input of the function is a term representing the subgoal and a number |
682 specifying the subgoal of interest. In Line 3 you need to descend under the |
681 specifying the subgoal of interest. In Line 3 you need to descend under the |
683 outermost @{term "Trueprop"} in order to get to the connective you like to |
682 outermost @{term "Trueprop"} in order to get to the connective you like to |
798 then you can use the combinator @{ML ORELSE'} for two tactics, and @{ML |
797 then you can use the combinator @{ML ORELSE'} for two tactics, and @{ML |
799 FIRST'} (or @{ML FIRST1}) for a list of tactics. For example, the tactic |
798 FIRST'} (or @{ML FIRST1}) for a list of tactics. For example, the tactic |
800 |
799 |
801 *} |
800 *} |
802 |
801 |
803 ML{*val orelse_xmp = rtac @{thm disjI1} ORELSE' rtac @{thm conjI}*} |
802 ML{*val orelse_xmp_tac = rtac @{thm disjI1} ORELSE' rtac @{thm conjI}*} |
804 |
803 |
805 text {* |
804 text {* |
806 will first try out whether rule @{text disjI} applies and after that |
805 will first try out whether rule @{text disjI} applies and after that |
807 @{text conjI}. To see this consider the proof |
806 @{text conjI}. To see this consider the proof |
808 *} |
807 *} |
809 |
808 |
810 lemma shows "True \<and> False" and "Foo \<or> Bar" |
809 lemma shows "True \<and> False" and "Foo \<or> Bar" |
811 apply(tactic {* orelse_xmp 2 *}) |
810 apply(tactic {* orelse_xmp_tac 2 *}) |
812 apply(tactic {* orelse_xmp 1 *}) |
811 apply(tactic {* orelse_xmp_tac 1 *}) |
813 txt {* which results in the goal state |
812 txt {* which results in the goal state |
814 |
813 |
815 \begin{minipage}{\textwidth} |
814 \begin{minipage}{\textwidth} |
816 @{subgoals [display]} |
815 @{subgoals [display]} |
817 \end{minipage} |
816 \end{minipage} |
823 Using @{ML FIRST'} we can simplify our @{ML select_tac} from Page~\pageref{tac:selecttac} |
822 Using @{ML FIRST'} we can simplify our @{ML select_tac} from Page~\pageref{tac:selecttac} |
824 as follows: |
823 as follows: |
825 *} |
824 *} |
826 |
825 |
827 ML{*val select_tac' = FIRST' [rtac @{thm conjI}, rtac @{thm impI}, |
826 ML{*val select_tac' = FIRST' [rtac @{thm conjI}, rtac @{thm impI}, |
828 rtac @{thm notI}, rtac @{thm allI}, K all_tac]*} |
827 rtac @{thm notI}, rtac @{thm allI}, K all_tac]*}text_raw{*\label{tac:selectprime}*} |
829 |
828 |
830 text {* |
829 text {* |
831 Since we like to mimic the behaviour of @{ML select_tac} as closely as possible, |
830 Since we like to mimic the behaviour of @{ML select_tac} as closely as possible, |
832 we must include @{ML all_tac} at the end of the list, otherwise the tactic will |
831 we must include @{ML all_tac} at the end of the list, otherwise the tactic will |
833 fail if no rule applies (we also have to wrap @{ML all_tac} using the |
832 fail if no rule applies (we also have to wrap @{ML all_tac} using the |
900 connective, but also to the ones immediately ``underneath'', i.e.~analyse the goal |
899 connective, but also to the ones immediately ``underneath'', i.e.~analyse the goal |
901 completely. For this you can use the tactic combinator @{ML REPEAT}. As an example |
900 completely. For this you can use the tactic combinator @{ML REPEAT}. As an example |
902 suppose the following tactic |
901 suppose the following tactic |
903 *} |
902 *} |
904 |
903 |
905 ML{*val repeat_xmp = REPEAT (CHANGED (select_tac' 1)) *} |
904 ML{*val repeat_xmp_tac = REPEAT (CHANGED (select_tac' 1)) *} |
906 |
905 |
907 text {* which applied to the proof *} |
906 text {* which applied to the proof *} |
908 |
907 |
909 lemma shows "((\<not>A) \<and> (\<forall>x. B x)) \<and> (C \<longrightarrow> D)" |
908 lemma shows "((\<not>A) \<and> (\<forall>x. B x)) \<and> (C \<longrightarrow> D)" |
910 apply(tactic {* repeat_xmp *}) |
909 apply(tactic {* repeat_xmp_tac *}) |
911 txt{* produces |
910 txt{* produces |
912 |
911 |
913 \begin{minipage}{\textwidth} |
912 \begin{minipage}{\textwidth} |
914 @{subgoals [display]} |
913 @{subgoals [display]} |
915 \end{minipage} *} |
914 \end{minipage} *} |
920 because otherwise @{ML REPEAT} runs into an infinite loop (it applies the |
919 because otherwise @{ML REPEAT} runs into an infinite loop (it applies the |
921 tactic as long as it succeeds). The function |
920 tactic as long as it succeeds). The function |
922 @{ML REPEAT1} is similar, but runs the tactic at least once (failing if |
921 @{ML REPEAT1} is similar, but runs the tactic at least once (failing if |
923 this is not possible). |
922 this is not possible). |
924 |
923 |
925 If you are after the ``primed'' version of @{ML repeat_xmp}, then you |
924 If you are after the ``primed'' version of @{ML repeat_xmp_tac}, then you |
926 need to implement it as |
925 need to implement it as |
927 *} |
926 *} |
928 |
927 |
929 ML{*val repeat_xmp' = REPEAT o CHANGED o select_tac'*} |
928 ML{*val repeat_xmp_tac' = REPEAT o CHANGED o select_tac'*} |
930 |
929 |
931 text {* |
930 text {* |
932 since there are no ``primed'' versions of @{ML REPEAT} and @{ML CHANGED}. |
931 since there are no ``primed'' versions of @{ML REPEAT} and @{ML CHANGED}. |
933 |
932 |
934 If you look closely at the goal state above, the tactics @{ML repeat_xmp} |
933 If you look closely at the goal state above, the tactics @{ML repeat_xmp_tac} |
935 and @{ML repeat_xmp'} are not yet quite what we are after: the problem is |
934 and @{ML repeat_xmp_tac'} are not yet quite what we are after: the problem is |
936 that goals 2 and 3 are not analysed. This is because the tactic |
935 that goals 2 and 3 are not analysed. This is because the tactic |
937 is applied repeatedly only to the first subgoal. To analyse also all |
936 is applied repeatedly only to the first subgoal. To analyse also all |
938 resulting subgoals, you can use the tactic combinator @{ML REPEAT_ALL_NEW}. |
937 resulting subgoals, you can use the tactic combinator @{ML REPEAT_ALL_NEW}. |
939 Suppose the tactic |
938 Suppose the tactic |
940 *} |
939 *} |
941 |
940 |
942 ML{*val repeat_all_new_xmp = REPEAT_ALL_NEW (CHANGED o select_tac')*} |
941 ML{*val repeat_all_new_xmp_tac = REPEAT_ALL_NEW (CHANGED o select_tac')*} |
943 |
942 |
944 text {* |
943 text {* |
945 you see that the following goal |
944 you see that the following goal |
946 *} |
945 *} |
947 |
946 |
948 lemma shows "((\<not>A) \<and> (\<forall>x. B x)) \<and> (C \<longrightarrow> D)" |
947 lemma shows "((\<not>A) \<and> (\<forall>x. B x)) \<and> (C \<longrightarrow> D)" |
949 apply(tactic {* repeat_all_new_xmp 1 *}) |
948 apply(tactic {* repeat_all_new_xmp_tac 1 *}) |
950 txt{* \begin{minipage}{\textwidth} |
949 txt{* \begin{minipage}{\textwidth} |
951 @{subgoals [display]} |
950 @{subgoals [display]} |
952 \end{minipage} *} |
951 \end{minipage} *} |
953 (*<*)oops(*>*) |
952 (*<*)oops(*>*) |
954 |
953 |
1005 \begin{isabelle} |
1004 \begin{isabelle} |
1006 @{text "*** back: no alternatives"}\\ |
1005 @{text "*** back: no alternatives"}\\ |
1007 @{text "*** At command \"back\"."} |
1006 @{text "*** At command \"back\"."} |
1008 \end{isabelle} |
1007 \end{isabelle} |
1009 |
1008 |
|
1009 Recall that we implemented @{ML select_tac'} on Page~\pageref{tac:selectprime} specifically |
|
1010 so that it always succeeds. We achieved this by adding at the end the tactic @{ML all_tac}. |
|
1011 We can achieve this also by using the combinator @{ML TRY}. Suppose, for example the |
|
1012 tactic |
|
1013 *} |
|
1014 |
|
1015 ML{*val select_tac'' = FIRST' [rtac @{thm conjI}, rtac @{thm impI}, |
|
1016 rtac @{thm notI}, rtac @{thm allI}]*} |
|
1017 |
|
1018 text {* |
|
1019 which will fail if none of the rules applies. However, if you prefix it as follows |
|
1020 *} |
|
1021 |
|
1022 ML{*val select_tac''' = TRY o select_tac''*} |
|
1023 |
|
1024 text {* |
|
1025 then the tactic @{ML select_tac''} will be tried out and any failure is harnessed. |
|
1026 We again have to use the construction with \mbox{@{text "TRY o ..."}} since there is |
|
1027 no primed version of @{ML TRY}. The tactic combinator @{ML TRYALL} will try out |
|
1028 a tactic on all subgoals. For example the tactic |
|
1029 *} |
|
1030 |
|
1031 ML{*val triv_tac = TRYALL (rtac @{thm TrueI} ORELSE' etac @{thm FalseE})*} |
|
1032 |
|
1033 text {* |
|
1034 will solve all trivial subgoals involving @{term True} or @{term "False"}. |
|
1035 |
|
1036 (FIXME: say something about @{ML COND} and COND') |
|
1037 |
1010 \begin{readmore} |
1038 \begin{readmore} |
1011 Most tactic combinators described in this section are defined in @{ML_file "Pure/tctical.ML"}. |
1039 Most tactic combinators described in this section are defined in @{ML_file "Pure/tctical.ML"}. |
|
1040 Some combinators for the purpose of proof search are implemented in @{ML_file "Pure/search.ML"}. |
1012 \end{readmore} |
1041 \end{readmore} |
1013 |
1042 |
1014 *} |
1043 *} |
1015 |
1044 |
1016 section {* Simplifier Tactics *} |
1045 section {* Simplifier Tactics *} |