--- a/ProgTutorial/Tactical.thy Sat Apr 11 19:23:58 2009 +0000
+++ b/ProgTutorial/Tactical.thy Mon Apr 13 08:30:48 2009 +0000
@@ -108,7 +108,7 @@
has a hard-coded number that stands for the subgoal analysed by the
tactic (@{text "1"} stands for the first, or top-most, subgoal). This hard-coding
of goals is sometimes wanted, but usually it is not. To avoid the explicit numbering,
- you can write\label{tac:footacprime}
+ you can write
*}
ML{*val foo_tac' =
@@ -116,7 +116,7 @@
THEN' rtac @{thm disjI2}
THEN' atac
THEN' rtac @{thm disjI1}
- THEN' atac)*}
+ THEN' atac)*}text_raw{*\label{tac:footacprime}*}
text {*
where @{ML THEN'} is used instead of @{ML THEN}. With @{ML foo_tac'} you can give
@@ -408,7 +408,7 @@
explored via the lazy sequences mechanism). Given the code
*}
-ML{*val resolve_tac_xmp = resolve_tac [@{thm impI}, @{thm conjI}]*}
+ML{*val resolve_xmp_tac = resolve_tac [@{thm impI}, @{thm conjI}]*}
text {*
an example for @{ML resolve_tac} is the following proof where first an outermost
@@ -416,8 +416,8 @@
*}
lemma shows "C \<longrightarrow> (A \<and> B)" and "(A \<longrightarrow> B) \<and> C"
-apply(tactic {* resolve_tac_xmp 1 *})
-apply(tactic {* resolve_tac_xmp 2 *})
+apply(tactic {* resolve_xmp_tac 1 *})
+apply(tactic {* resolve_xmp_tac 2 *})
txt{*\begin{minipage}{\textwidth}
@{subgoals [display]}
\end{minipage}*}
@@ -663,8 +663,7 @@
cterm}). With this you can implement a tactic that applies a rule according
to the topmost logic connective in the subgoal (to illustrate this we only
analyse a few connectives). The code of the tactic is as
- follows.\label{tac:selecttac}
-
+ follows.
*}
ML %linenosgray{*fun select_tac (t, i) =
@@ -675,7 +674,7 @@
| @{term "op \<longrightarrow>"} $ _ $ _ => rtac @{thm impI} i
| @{term "Not"} $ _ => rtac @{thm notI} i
| Const (@{const_name "All"}, _) $ _ => rtac @{thm allI} i
- | _ => all_tac*}
+ | _ => all_tac*}text_raw{*\label{tac:selecttac}*}
text {*
The input of the function is a term representing the subgoal and a number
@@ -800,7 +799,7 @@
*}
-ML{*val orelse_xmp = rtac @{thm disjI1} ORELSE' rtac @{thm conjI}*}
+ML{*val orelse_xmp_tac = rtac @{thm disjI1} ORELSE' rtac @{thm conjI}*}
text {*
will first try out whether rule @{text disjI} applies and after that
@@ -808,8 +807,8 @@
*}
lemma shows "True \<and> False" and "Foo \<or> Bar"
-apply(tactic {* orelse_xmp 2 *})
-apply(tactic {* orelse_xmp 1 *})
+apply(tactic {* orelse_xmp_tac 2 *})
+apply(tactic {* orelse_xmp_tac 1 *})
txt {* which results in the goal state
\begin{minipage}{\textwidth}
@@ -825,7 +824,7 @@
*}
ML{*val select_tac' = FIRST' [rtac @{thm conjI}, rtac @{thm impI},
- rtac @{thm notI}, rtac @{thm allI}, K all_tac]*}
+ rtac @{thm notI}, rtac @{thm allI}, K all_tac]*}text_raw{*\label{tac:selectprime}*}
text {*
Since we like to mimic the behaviour of @{ML select_tac} as closely as possible,
@@ -902,12 +901,12 @@
suppose the following tactic
*}
-ML{*val repeat_xmp = REPEAT (CHANGED (select_tac' 1)) *}
+ML{*val repeat_xmp_tac = REPEAT (CHANGED (select_tac' 1)) *}
text {* which applied to the proof *}
lemma shows "((\<not>A) \<and> (\<forall>x. B x)) \<and> (C \<longrightarrow> D)"
-apply(tactic {* repeat_xmp *})
+apply(tactic {* repeat_xmp_tac *})
txt{* produces
\begin{minipage}{\textwidth}
@@ -922,31 +921,31 @@
@{ML REPEAT1} is similar, but runs the tactic at least once (failing if
this is not possible).
- If you are after the ``primed'' version of @{ML repeat_xmp}, then you
+ If you are after the ``primed'' version of @{ML repeat_xmp_tac}, then you
need to implement it as
*}
-ML{*val repeat_xmp' = REPEAT o CHANGED o select_tac'*}
+ML{*val repeat_xmp_tac' = REPEAT o CHANGED o select_tac'*}
text {*
since there are no ``primed'' versions of @{ML REPEAT} and @{ML CHANGED}.
- If you look closely at the goal state above, the tactics @{ML repeat_xmp}
- and @{ML repeat_xmp'} are not yet quite what we are after: the problem is
+ If you look closely at the goal state above, the tactics @{ML repeat_xmp_tac}
+ and @{ML repeat_xmp_tac'} are not yet quite what we are after: the problem is
that goals 2 and 3 are not analysed. This is because the tactic
is applied repeatedly only to the first subgoal. To analyse also all
resulting subgoals, you can use the tactic combinator @{ML REPEAT_ALL_NEW}.
Suppose the tactic
*}
-ML{*val repeat_all_new_xmp = REPEAT_ALL_NEW (CHANGED o select_tac')*}
+ML{*val repeat_all_new_xmp_tac = REPEAT_ALL_NEW (CHANGED o select_tac')*}
text {*
you see that the following goal
*}
lemma shows "((\<not>A) \<and> (\<forall>x. B x)) \<and> (C \<longrightarrow> D)"
-apply(tactic {* repeat_all_new_xmp 1 *})
+apply(tactic {* repeat_all_new_xmp_tac 1 *})
txt{* \begin{minipage}{\textwidth}
@{subgoals [display]}
\end{minipage} *}
@@ -1007,8 +1006,38 @@
@{text "*** At command \"back\"."}
\end{isabelle}
+ Recall that we implemented @{ML select_tac'} on Page~\pageref{tac:selectprime} specifically
+ so that it always succeeds. We achieved this by adding at the end the tactic @{ML all_tac}.
+ We can achieve this also by using the combinator @{ML TRY}. Suppose, for example the
+ tactic
+*}
+
+ML{*val select_tac'' = FIRST' [rtac @{thm conjI}, rtac @{thm impI},
+ rtac @{thm notI}, rtac @{thm allI}]*}
+
+text {*
+ which will fail if none of the rules applies. However, if you prefix it as follows
+*}
+
+ML{*val select_tac''' = TRY o select_tac''*}
+
+text {*
+ then the tactic @{ML select_tac''} will be tried out and any failure is harnessed.
+ We again have to use the construction with \mbox{@{text "TRY o ..."}} since there is
+ no primed version of @{ML TRY}. The tactic combinator @{ML TRYALL} will try out
+ a tactic on all subgoals. For example the tactic
+*}
+
+ML{*val triv_tac = TRYALL (rtac @{thm TrueI} ORELSE' etac @{thm FalseE})*}
+
+text {*
+ will solve all trivial subgoals involving @{term True} or @{term "False"}.
+
+ (FIXME: say something about @{ML COND} and COND')
+
\begin{readmore}
Most tactic combinators described in this section are defined in @{ML_file "Pure/tctical.ML"}.
+ Some combinators for the purpose of proof search are implemented in @{ML_file "Pure/search.ML"}.
\end{readmore}
*}