diff -r 84d1392186d3 -r 253ea99c1441 CookBook/Tactical.thy --- a/CookBook/Tactical.thy Wed Feb 25 22:13:41 2009 +0000 +++ b/CookBook/Tactical.thy Thu Feb 26 12:16:24 2009 +0000 @@ -311,7 +311,7 @@ "(C)"}. Since the goal @{term C} can potentially be an implication, there is a ``protector'' wrapped around it (in from of an outermost constant @{text "Const (\"prop\", bool \ bool)"}; however this constant - is invisible in the figure). This prevents that premises of @{text C} are + is invisible in the figure). This wrapper prevents that premises of @{text C} are mis-interpreted as open subgoals. While tactics can operate on the subgoals (the @{text "A\<^isub>i"} above), they are expected to leave the conclusion @{term C} intact, with the exception of possibly instantiating schematic @@ -453,7 +453,7 @@ (*<*)oops(*>*) text {* - where the application of Rule @{text bspec} generates two subgoals involving the + where the application of rule @{text bspec} generates two subgoals involving the meta-variable @{text "?x"}. Now, if you are not careful, tactics applied to the first subgoal might instantiate this meta-variable in such a way that the second subgoal becomes unprovable. If it is clear what the @{text "?x"} @@ -576,7 +576,7 @@ \end{tabular} \end{quote} - Note in the actual output the brown colour of the variables @{term x} and + Notice in the actual output the brown colour of the variables @{term x} and @{term y}. Although they are parameters in the original goal, they are fixed inside the subproof. By convention these fixed variables are printed in brown colour. Similarly the schematic variable @{term z}. The assumption, or premise, @@ -727,12 +727,13 @@ the first goal. To do this can result in quite messy code. In contrast, the ``reverse application'' is easy to implement. - (FIXME: mention @{ML "CSUBGOAL"}) + The tactic @{ML "CSUBGOAL"} is similar to @{ML SUBGOAL} except that it takes + a @{ML_type cterm} instead of a @{ML_type term}. Of course, this example is + contrived: there are much simpler methods available in Isabelle for + implementing a proof procedure analysing a goal according to its topmost + connective. These simpler methods use tactic combinators, which we will + explain in the next section. - Of course, this example is contrived: there are much simpler methods available in - Isabelle for implementing a proof procedure analysing a goal according to its topmost - connective. These simpler methods use tactic combinators, which we will explain - in the next section. *} section {* Tactic Combinators *} @@ -1027,10 +1028,10 @@ text {* In Isabelle you can also implement custom simplification procedures, called - \emph{simprocs}. Simprocs can be triggered on a specified term-pattern and - rewrite a term according to a theorem. They are useful in cases where - a rewriting rule must be produced on ``demand'' or when rewriting by - simplification is too unpredictable and potentially loops. + \emph{simprocs}. Simprocs can be triggered by the simplifier on a specified + term-pattern and rewrite a term according to a theorem. They are useful in + cases where a rewriting rule must be produced on ``demand'' or when + rewriting by simplification is too unpredictable and potentially loops. To see how simprocs work, let us first write a simproc that just prints out the pattern which triggers it and otherwise does nothing. For this @@ -1052,7 +1053,7 @@ returns @{ML NONE} (standing for an optional @{ML_type thm}) since at the moment we are \emph{not} interested in actually rewriting anything. We want that the simproc is triggered by the pattern @{term "Suc n"}. This can be - done by adding the simproc to the current simproc as follows + done by adding the simproc to the current simpset as follows *} simproc_setup fail_sp ("Suc n") = {* K fail_sp_aux *} @@ -1114,7 +1115,8 @@ text {* Here the redex is given as a @{ML_type term}, instead of a @{ML_type cterm} (therefore we printing it out using the function @{ML string_of_term in Syntax}). - We can turn this function into a proper simproc using + We can turn this function into a proper simproc using the function + @{ML Simplifier.simproc_i}: *} @@ -1130,7 +1132,7 @@ Here the pattern is given as @{ML_type term} (instead of @{ML_type cterm}). The function also takes a list of patterns that can trigger the simproc. Now the simproc is set up and can be explicitly added using - {ML addsimprocs} to a simpset whenerver + @{ML addsimprocs} to a simpset whenerver needed. Simprocs are applied from inside to outside and from left to right. You can @@ -1138,7 +1140,7 @@ *} lemma shows "Suc (Suc 0) = (Suc 1)" - apply(tactic {* simp_tac (HOL_ss addsimprocs [fail_sp']) 1*}) + apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [fail_sp']) 1*}) (*<*)oops(*>*) text {* @@ -1190,7 +1192,7 @@ *} lemma shows "P (Suc (Suc (Suc 0))) (Suc 0)" - apply(tactic {* simp_tac (HOL_ss addsimprocs [plus_one_sp]) 1*}) + apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [plus_one_sp]) 1*}) txt{* where the simproc produces the goal state @@ -1208,7 +1210,6 @@ Next let us implement a simproc that replaces terms of the form @{term "Suc n"} with the number @{text n} increase by one. First we implement a function that takes a term and produces the corresponding integer value. - *} ML{*fun dest_suc_trm ((Const (@{const_name "Suc"}, _)) $ t) = 1 + dest_suc_trm t @@ -1412,7 +1413,7 @@ @{ML_response_fake [display,gray] "let - val ctrm = @{cterm \"True \ (Foo \ Bar)\"} + val ctrm = @{cterm \"True \ (Foo \ Bar)\"} in Conv.rewr_conv @{thm true_conj1} ctrm end" @@ -1439,7 +1440,8 @@ "(\x. x \ False) True \ False"} where we first beta-reduce the term and then rewrite according to - @{thm [source] true_conj1}. + @{thm [source] true_conj1}. (Recall the problem with the pretty-printer + normalising all terms.) The conversion combinator @{ML else_conv} tries out the first one, and if it does not apply, tries the second. For example @@ -1459,11 +1461,11 @@ does not fail, however, because the combinator @{ML else_conv} will then try out @{ML Conv.all_conv}, which always succeeds. - Apart from the function @{ML beta_conversion in Thm}, which able to fully - beta-normalise a term, the restriction of conversions so far is that they + Apart from the function @{ML beta_conversion in Thm}, which is able to fully + beta-normalise a term, the conversions so far are restricted in that they only apply to the outer-most level of a @{ML_type cterm}. In what follows we will lift this restriction. The combinator @{ML Conv.arg_conv} will apply - the conversion on the first argument of an application, that is the term + the conversion to the first argument of an application, that is the term must be of the form @{ML "t1 $ t2" for t1 t2} and the conversion is applied to @{text t2}. For example @@ -1477,7 +1479,7 @@ "P \ (True \ Q) \ P \ Q"} The reason for this behaviour is that @{text "(op \)"} expects two - arguments. So the term must be of the form @{text "Const \ $ t1 $ t2"}. The + arguments. So the term must be of the form @{text "(Const \ $ t1) $ t2"}. The conversion is then applied to @{text "t2"} which in the example above stands for @{term "True \ Q"}. @@ -1515,8 +1517,10 @@ text {* This functions descends under applications (Line 6 and 7) and abstractions (Line 8); and ``fires'' if the outer-most constant is an @{text "True \ \"} - (Lines 3-5); otherwise it leaves the term unchanged (Line 9). To see this - conversion in action, consider the following example. + (Lines 3-5); otherwise it leaves the term unchanged (Line 9). In Line 2 + we need to transform the @{ML_type cterm} into a @{ML_type term} in order + to be able to pattern-match the term. To see this + conversion in action, consider the following example @{ML_response_fake [display,gray] "let @@ -1527,9 +1531,11 @@ end" "distinct [1, x] \ True \ 1 \ x \ distinct [1, x] \ 1 \ x"} - To see how much control you have about rewriting via conversions, let us + where the conversion is applied ``deep'' inside the term. + + To see how much control you have about rewriting by using conversions, let us make the task a bit more complicated by rewriting according to the rule - @{text true_conj1}, but only in the first arguments of @{term If}s. The + @{text true_conj1}, but only in the first arguments of @{term If}s. Then the conversion should be as follows. *} @@ -1543,7 +1549,7 @@ | _ => Conv.all_conv ctrm *} text {* - Here is an application of this conversion: + Here is an example for this conversion: @{ML_response_fake [display,gray] "let @@ -1560,7 +1566,7 @@ text {* So far we only applied conversions to @{ML_type cterm}s. Conversions can, however, also work on theorems using the function @{ML "Conv.fconv_rule"}. As an example, - consider @{ML all_true1_conv} and the lemma: + consider the conversion @{ML all_true1_conv} and the lemma: *} lemma foo_test: "P \ (True \ \P)" by simp @@ -1583,7 +1589,7 @@ the conclusion of a goal. Assume we want to apply @{ML all_true1_conv} only in the conclusion - of the goal, and @{ML if_true1_conv} should only be applied in the premises. + of the goal, and @{ML if_true1_conv} should only be applied to the premises. Here is a tactic doing exactly that: *} @@ -1611,9 +1617,7 @@ apply(tactic {* true1_tac 1 *}) txt {* where the tactic yields the goal state - \begin{minipage}{\textwidth} - @{subgoals [display]} - \end{minipage} *} + @{subgoals [display]}*} (*<*)oops(*>*) text {*