diff -r 64fa844064fa -r cc9359bfacf4 CookBook/Tactical.thy --- a/CookBook/Tactical.thy Wed Mar 04 14:26:21 2009 +0000 +++ b/CookBook/Tactical.thy Thu Mar 05 16:46:43 2009 +0000 @@ -1094,6 +1094,11 @@ @{ML_file "Provers/splitter.ML"}. \end{readmore} + \begin{readmore} + FIXME: Find the right place Discrimination nets are implemented + in @{ML_file "Pure/net.ML"}. + \end{readmore} + The most common combinators to modify simpsets are \begin{isabelle} @@ -1711,7 +1716,7 @@ "*** Exception- CTERM (\"no conversion\", []) raised"} A more interesting conversion is the function @{ML "Thm.beta_conversion"}: it - produces an equation between a term and its beta-normal form. For example + produces a meta-equation between a term and its beta-normal form. For example @{ML_response_fake [display,gray] "let @@ -1724,7 +1729,7 @@ "((\x y. x + y) 2) 10 \ 2 + 10"} 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. + 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 @@ -1736,9 +1741,9 @@ val add = @{cterm \"\x y. x + (y::nat)\"} val two = @{cterm \"2::nat\"} val ten = @{cterm \"10::nat\"} + val thm = Thm.beta_conversion true (Thm.capply (Thm.capply add two) ten) in - #prop (rep_thm - (Thm.beta_conversion true (Thm.capply (Thm.capply add two) ten))) + #prop (rep_thm thm) end" "Const (\"==\",\) $ (Abs (\"x\",\,Abs (\"y\",\,\)) $\$\) $ @@ -1763,15 +1768,15 @@ 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: + "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 {* - You can see how this function works with the example - @{term "True \ (Foo \ Bar)"}: + You can see how this function works in the example rewriting + the @{ML_type cterm} @{term "True \ (Foo \ Bar)"} to @{term "Foo \ Bar"}. @{ML_response_fake [display,gray] "let @@ -1782,7 +1787,8 @@ "True \ (Foo \ Bar) \ Foo \ Bar"} 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 + outer-most level of the @{ML_type cterm}. If the given @{ML_type cterm} does not match + exactly the left-hand side of the theorem, then @{ML Conv.rewr_conv} raises the exception @{ML CTERM}. @@ -1841,7 +1847,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. Therefore 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.fun_conv} applies the conversion to the first argument of an application. @@ -1858,13 +1864,14 @@ end" "\P. True \ P \ Foo \ \P. P \ Foo"} - The conversion that goes under an application is - @{ML Conv.combination_conv}. It expects two conversions as arguments, - each of which is applied to the corresponding ``branch'' of the application. + Note that this conversion needs a context as an argument. The conversion that + goes under an application is @{ML Conv.combination_conv}. It expects two conversions + as arguments, each of which 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. + We can now apply all these functions in a conversion that recursively + descends a term and applies a ``@{thm [source] true_conj1}''-conversion + in all possible positions. *} ML %linenosgray{*fun all_true1_conv ctxt ctrm = @@ -1873,17 +1880,17 @@ (Conv.arg_conv (all_true1_conv ctxt) then_conv Conv.rewr_conv @{thm true_conj1}) ctrm | _ $ _ => Conv.combination_conv - (all_true1_conv ctxt) (all_true1_conv ctxt) ctrm + (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 {* - 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). In Line 2 + This function ``fires'' if the terms is of the form @{text "True \ \"}; + it descends under applications (Line 6 and 7) and abstractions + (Line 8); 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 + conversion in action, consider the following example: @{ML_response_fake [display,gray] "let @@ -1894,8 +1901,6 @@ end" "distinct [1, x] \ True \ 1 \ x \ distinct [1, x] \ 1 \ x"} - 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. Then @@ -1907,7 +1912,7 @@ Const (@{const_name If}, _) $ _ => Conv.arg_conv (all_true1_conv ctxt) ctrm | _ $ _ => Conv.combination_conv - (if_true1_conv ctxt) (if_true1_conv ctxt) ctrm + (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 *} @@ -1918,7 +1923,7 @@ "let val ctxt = @{context} val ctrm = - @{cterm \"if P (True \ 1 \ 2) then True \ True else True \ False\"} + @{cterm \"if P (True \ 1 \ 2) then True \ True else True \ False\"} in if_true1_conv ctxt ctrm end" @@ -1944,15 +1949,15 @@ 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 + and also some predefined conversion combinators that 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 + converting under parameters (i.e.~where goals are of the form @{text "\x. P \ + Q"}); the function @{ML Conv.prems_conv} for applying a conversion to all + premises of a goal, and @{ML Conv.concl_conv} for applying a 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 to the premises. + of the goal, and @{ML if_true1_conv} should only apply to the premises. Here is a tactic doing exactly that: *} @@ -2000,8 +2005,9 @@ \end{exercise} \begin{exercise} - Compare which way of rewriting such terms is more efficient. For this - you might have to construct quite large terms. + Compare which way (either Exercise ~\ref{addsimproc} or \ref{ex:addconversion}) of + rewriting such terms is faster. For this you might have to construct quite + large terms. Also see Recipe \ref{rec:timing} for information about timing. \end{exercise} \begin{readmore}