diff -r 4aa8a80e37ff -r 6dafb0815ae6 CookBook/Tactical.thy --- a/CookBook/Tactical.thy Wed Feb 25 16:49:20 2009 +0000 +++ b/CookBook/Tactical.thy Wed Feb 25 21:55:08 2009 +0000 @@ -727,6 +727,8 @@ 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"}) + 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 @@ -1319,24 +1321,27 @@ text {* - Conversions are a ``thin'' layer on top of Isabelle's inference kernel, and + Conversions are a thin layer on top of Isabelle's inference kernel, and can be viewed be as a controllable, bare-bone version of Isabelle's simplifier. - A difference is that conversions simplify @{ML_type cterm}s, while teh simplifier - acts on theorems. The type for conversions is + One difference between conversions and the simplifier is that the former + act on @{ML_type cterm}s while the latter acts on @{ML_type thm}s. + However, we will also show in this section how conversions can be applied + to theorems via tactics. The type for conversions is *} ML{*type conv = Thm.cterm -> Thm.thm*} text {* - whereby the theorem is always a meta-equality. A simple conversion is - the function @{ML "Conv.all_conv"}, which maps a @{ML_type cterm} to an instance of - the (meta)reflexivity theorem. For example: + whereby the produced theorem is always a meta-equality. A simple conversion + is the function @{ML "Conv.all_conv"}, which maps a @{ML_type cterm} to an + instance of the (meta)reflexivity theorem. For example: @{ML_response_fake [display,gray] "Conv.all_conv @{cterm \"Foo \ Bar\"}" "Foo \ Bar \ Foo \ Bar"} - Another simple conversion is @{ML Conv.no_conv} which always raises the exception @{ML CTERM} + Another simple conversion is @{ML Conv.no_conv} which always raises the + exception @{ML CTERM}. @{ML_response_fake [display,gray] "Conv.no_conv @{cterm True}" @@ -1355,16 +1360,31 @@ end" "((\x y. x + y) 2) 10 \ 2 + 10"} - Note that the actual response in the example is @{term "2 + 10 \ 2 + (10::nat)"}, - since the pretty-printer of @{ML_type cterm}s already beta-normalises terms. - However, we can by how we constructed the term (using the function - @{ML Thm.capply}, which is the application @{ML $} for @{ML_type cterm}) - that the left-hand side must contain beta-redexes. + Note that the actual response in this example is @{term "2 + 10 \ 2 + (10::nat)"}, + since the pretty printer for @{ML_type cterm}s already beta-normalises terms. + But by the way how we constructed the term (using the function + @{ML Thm.capply}, which is the application @{ML $} for @{ML_type cterm}s), + we can be sure the left-hand side must contain beta-redexes. Indeed + if we obtain the ``raw'' representation of the produced theorem, we + can see the difference: + + @{ML_response [display,gray] +"let + val add = @{cterm \"\x y. x + (y::nat)\"} + val two = @{cterm \"2::nat\"} + val ten = @{cterm \"10::nat\"} +in + #prop (rep_thm + (Thm.beta_conversion true (Thm.capply (Thm.capply add two) ten))) +end" +"Const (\"==\",\) $ + (Abs (\"x\",\,Abs (\"y\",\,\)) $\$\) $ + (Const (\"HOL.plus_class.plus\",\) $ \ $ \)"} The argument @{ML true} in @{ML Thm.beta_conversion} indicates that - the right-hand side should be fully beta-normalised. If @{ML false} is - given, then only a beta-reduction is performed on the outer-most level. - For example + the right-hand side will be fully beta-normalised. If instead + @{ML false} is given, then only a single beta-reduction is performed + on the outer-most level. For example @{ML_response_fake [display,gray] "let @@ -1376,18 +1396,19 @@ "((\x y. x + y) 2) \ \y. 2 + y"} Again, we actually see as output only the fully normalised term - @{term "\y. 2 + y"}. + @{text "\y. 2 + y"}. - The main point of conversions is that they can be used for rewriting terms. - For this you can use the function @{ML "Conv.rewr_conv"}. Suppose we want - to rewrite a term according to the (meta)equation: - + The main point of conversions is that they can be used for rewriting + @{ML_type cterm}s. To do this you can use the function @{ML + "Conv.rewr_conv"} which expects a meta-equation as an argument. Suppose we + want to rewrite a @{ML_type cterm} according to the (meta)equation: *} lemma true_conj1: "True \ P \ P" by simp text {* - then we can use it in order to rewrite @{term "True \ (Foo \ Bar)"}: + You can see how this function works with the example + @{term "True \ (Foo \ Bar)"}: @{ML_response_fake [display,gray] "let @@ -1397,8 +1418,10 @@ end" "True \ (Foo \ Bar) \ Foo \ Bar"} - The function @{ML Conv.rewr_conv} only does rewriting on the outer-most - level, otherwise it raises the exception @{ML CTERM}. + Note, however, that the function @{ML Conv.rewr_conv} only rewrites the + outer-most level of the @{ML_type cterm}. If the given @{ML_type cterm} does not match the + left-hand side of the theorem, then @{ML Conv.rewr_conv} raises + the exception @{ML CTERM}. This very primitive way of rewriting can be made more powerful by combining several conversions into one. For this you can use conversion @@ -1407,38 +1430,42 @@ @{ML_response_fake [display,gray] "let - val conv1 = Thm.beta_conversion true + val conv1 = Thm.beta_conversion false val conv2 = Conv.rewr_conv @{thm true_conj1} - val ctrm = Thm.capply (@{cterm \"\x. x \ False\"}) (@{cterm \"True\"}) + val ctrm = Thm.capply @{cterm \"\x. x \ False\"} @{cterm \"True\"} in (conv1 then_conv conv2) ctrm end" "(\x. x \ False) True \ False"} + where we first beta-reduce the term and then rewrite according to + @{thm [source] true_conj1}. + The conversion combinator @{ML else_conv} tries out the first one, and if it does not apply, tries the second. For example @{ML_response_fake [display,gray] "let - val conv = Conv.rewr_conv @{thm true_conj1} - else_conv Conv.all_conv + val conv = Conv.rewr_conv @{thm true_conj1} else_conv Conv.all_conv val ctrm1 = @{cterm \"True \ Q\"} val ctrm2 = @{cterm \"P \ (True \ Q)\"} in (conv ctrm1, conv ctrm2) end" -"(True \ Q \ Q, - P \ True \ Q \ P \ True \ Q)"} +"(True \ Q \ Q, P \ True \ Q \ P \ True \ Q)"} Here the conversion of @{thm [source] true_conj1} only applies in the first case, but fails in the second. The whole conversion - does not fail because the combinator @{ML else_conv} will then - try out @{ML Conv.all_conv}, which allways succeeds. + does not fail, however, because the combinator @{ML else_conv} will then + try out @{ML Conv.all_conv}, which always succeeds. - The combinator @{ML Conv.arg_conv} will apply the conversion on - the first argument, taht is the term must be of the form - @{ML "t1 $ t2" for t1 t2} and the conversion is applied to @{text t2}. - For example + 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 + 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 + must be of the form @{ML "t1 $ t2" for t1 t2} and the conversion is applied + to @{text t2}. For example @{ML_response_fake [display,gray] "let @@ -1449,68 +1476,111 @@ end" "P \ (True \ Q) \ P \ Q"} - The reason for this behaviour is that @{text "(op \)"} expects two arguments - and so is of the form @{text "Const \ $ t1 $ t2"}. The conversion is then - applied to @{text "t2"} which stands for @{term "True \ 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 + conversion is then applied to @{text "t2"} which in the example above + stands for @{term "True \ Q"}. + + The function @{ML Conv.abs_conv} applies a conversion under an abstractions. + For example: + @{ML_response_fake [display,gray] +"let + val conv = K (Conv.rewr_conv @{thm true_conj1}) + val ctrm = @{cterm \"\P. True \ P \ Foo\"} +in + Conv.abs_conv conv @{context} ctrm +end" + "\P. True \ P \ Foo \ \P. P \ Foo"} + + The conversion that goes under an application is + @{ML Conv.combination_conv}. It expects two conversions, which each of them + is applied to the corresponding ``branch'' of the application. + + We can now apply all these functions in a + conversion that recursively descends a term and applies a conversion in all + possible positions. *} - -text {* - To begin with, let us assumes we want to simplify with the rewrite rule - @{text true_conj1}. As a conversion, this may look as follows: -*} - - -ML{*fun all_true1_conv ctxt ct = - (case Thm.term_of ct of +ML %linenosgray{*fun all_true1_conv ctxt ctrm = + case (Thm.term_of ctrm) of @{term "op \"} $ @{term True} $ _ => (Conv.arg_conv (all_true1_conv ctxt) then_conv - Conv.rewr_conv @{thm true_conj1}) ct - | _ $ _ => Conv.combination_conv (all_true1_conv ctxt) - (all_true1_conv ctxt) ct - | Abs _ => Conv.abs_conv (fn (_, cx) => all_true1_conv cx) ctxt ct - | _ => Conv.all_conv ct)*} + Conv.rewr_conv @{thm true_conj1}) ctrm + | _ $ _ => Conv.combination_conv + (all_true1_conv ctxt) (all_true1_conv ctxt) ctrm + | Abs _ => Conv.abs_conv (fn (_, ctxt) => all_true1_conv ctxt) ctxt ctrm + | _ => Conv.all_conv ctrm*} text {* - Here is this conversion in action: + 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. - @{ML_response_fake [display,gray] - "all_true1_conv @{context} - @{cterm \"distinct [1, x] \ True \ 1 \ x\"}" +@{ML_response_fake [display,gray] +"let + val ctxt = @{context} + val ctrm = @{cterm \"distinct [1, x] \ True \ 1 \ x\"} +in + all_true1_conv ctxt ctrm +end" "distinct [1, x] \ True \ 1 \ x \ distinct [1, x] \ 1 \ x"} - Now, 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}: + To see how much control you have about rewriting via 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 + the conversion should be as follows. *} -ML{*fun if_true1_conv ctxt ct = - (case Thm.term_of ct of +ML{*fun if_true1_conv ctxt ctrm = + case Thm.term_of ctrm of Const (@{const_name If}, _) $ _ => - Conv.arg_conv (all_true1_conv ctxt) ct - | _ $ _ => Conv.combination_conv (if_true1_conv ctxt) - (if_true1_conv ctxt) ct - | Abs _ => Conv.abs_conv (fn (_, cx) => if_true1_conv cx) ctxt ct - | _ => Conv.all_conv ct)*} + Conv.arg_conv (all_true1_conv ctxt) ctrm + | _ $ _ => Conv.combination_conv + (if_true1_conv ctxt) (if_true1_conv ctxt) ctrm + | Abs _ => Conv.abs_conv (fn (_, ctxt) => if_true1_conv ctxt) ctxt ctrm + | _ => Conv.all_conv ctrm *} text {* Here is an application of this conversion: @{ML_response_fake [display,gray] - "if_true1_conv @{context} - @{cterm \"if P (True \ 1 \ 2) then True \ True else True \ False\"}" - "if P (True \ 1 \ 2) then True \ True else True \ False \ if P (1 \ 2) then True \ True else True \ False"} +"let + val ctxt = @{context} + val ctrm = + @{cterm \"if P (True \ 1 \ 2) then True \ True else True \ False\"} +in + if_true1_conv ctxt ctrm +end" +"if P (True \ 1 \ 2) then True \ True else True \ False +\ if P (1 \ 2) then True \ True else True \ False"} *} text {* - Conversions can also be turned into a tactic with the @{ML CONVERSION} - tactical, and there are predefined conversionals to traverse a goal state. - Given a state @{term "\x. P \ Q"}, the conversional - @{ML Conv.params_conv} applies a conversion to @{term "P \ Q"}; - given a state @{term "\ P1; P2 \ \ Q"}, - the conversional @{ML Conv.prems_conv} applies a conversion to the premises - @{term P1} and @{term P2}, and @{ML Conv.concl_conv} applies a conversion to - the conclusion @{term Q}. + 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: +*} + +lemma foo_test: "P \ (True \ \P)" by simp + +text {* + Using the conversion you can transform this theorem into a new theorem + as follows + + @{ML_response_fake [display,gray] + "Conv.fconv_rule (all_true1_conv @{context}) @{thm foo_test}" + "?P \ \ ?P"} + + Finally, conversions can also be turned into tactics and then applied to + goal states. This can be done with the help of the function @{ML CONVERSION}, + and also some predefined conversion combinator which traverse a goal + state. The combinators for the goal state are: @{ML Conv.params_conv} for + going under parameters (i.e.~where goals are of the form @{text "\x. P \ + Q"}); the function @{ML Conv.prems_conv} for applying the conversion to all + premises of a goal, and @{ML Conv.concl_conv} for applying the conversion to + 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. @@ -1518,36 +1588,38 @@ *} ML{*val true1_tac = CSUBGOAL (fn (goal, i) => - let val ctxt = ProofContext.init (Thm.theory_of_cterm goal) + let + val ctxt = ProofContext.init (Thm.theory_of_cterm goal) in - CONVERSION ( - Conv.params_conv ~1 (fn cx => - (Conv.prems_conv ~1 (if_true1_conv cx)) then_conv - Conv.concl_conv ~1 (all_true1_conv cx)) ctxt) i + CONVERSION + (Conv.params_conv ~1 (fn ctxt => + (Conv.prems_conv ~1 (if_true1_conv ctxt)) then_conv + Conv.concl_conv ~1 (all_true1_conv ctxt)) ctxt) i end)*} text {* - To demonstrate this tactic, consider the following example: + We call the conversions with the argument @{ML "~1"} in order to + analyse all parameters, premises and conclusions. If we call it with + a non-negative number, say @{text n}, then these conversions will + only be called on @{text n} premises (similar for parameters and + conclusions). To test the tactic, consider the proof *} lemma "if True \ P then P else True \ False \ (if True \ Q then Q else P) \ True \ (True \ Q)" apply(tactic {* true1_tac 1 *}) -txt {* \begin{minipage}{\textwidth} +txt {* where the tactic yields the goal state + + \begin{minipage}{\textwidth} @{subgoals [display]} \end{minipage} *} (*<*)oops(*>*) text {* - Conversions are not restricted to work on certified terms only, they can also - be lifted to theorem transformers, i.e. functions mapping a theorem to a - theorem, by the help of @{ML Conv.fconv_rule}. As an example, consider the - conversion @{ML all_true1_conv} again: - - @{ML_response_fake [display,gray] - "Conv.fconv_rule (all_true1_conv @{context}) @{lemma \"P \ (True \ \P)\" by simp}" - "P \ \P"} + To sum up this section, conversions are not as powerful as the simplifier + and simprocs; the advantage of conversions, however, is that you never have + to worry about non-termination. \begin{readmore} See @{ML_file "Pure/conv.ML"} for more information about conversion combinators.