# HG changeset patch # User Christian Urban # Date 1239611448 0 # Node ID 29787dcf7b2eedfae6bf2f6226429c6a19533e8c # Parent 0a8981f52045705fb78f1be923f3557c29a7b046 added something about TRY and TRYALL diff -r 0a8981f52045 -r 29787dcf7b2e ProgTutorial/Tactical.thy --- 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 \ (A \ B)" and "(A \ B) \ 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 \"} $ _ $ _ => 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 \ False" and "Foo \ 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 "((\A) \ (\x. B x)) \ (C \ 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 "((\A) \ (\x. B x)) \ (C \ 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} *} diff -r 0a8981f52045 -r 29787dcf7b2e progtutorial.pdf Binary file progtutorial.pdf has changed