--- 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 @@
"((\<lambda>x y. x + y) 2) 10 \<equiv> 2 + 10"}
Note that the actual response in this example is @{term "2 + 10 \<equiv> 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 \"\<lambda>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 (\"==\",\<dots>) $
(Abs (\"x\",\<dots>,Abs (\"y\",\<dots>,\<dots>)) $\<dots>$\<dots>) $
@@ -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 \<and> P \<equiv> P" by simp
text {*
- You can see how this function works with the example
- @{term "True \<and> (Foo \<longrightarrow> Bar)"}:
+ You can see how this function works in the example rewriting
+ the @{ML_type cterm} @{term "True \<and> (Foo \<longrightarrow> Bar)"} to @{term "Foo \<longrightarrow> Bar"}.
@{ML_response_fake [display,gray]
"let
@@ -1782,7 +1787,8 @@
"True \<and> (Foo \<longrightarrow> Bar) \<equiv> Foo \<longrightarrow> 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 \<or> (True \<and> Q) \<equiv> P \<or> Q"}
The reason for this behaviour is that @{text "(op \<or>)"} expects two
- arguments. So the term must be of the form @{text "(Const \<dots> $ t1) $ t2"}. The
+ arguments. Therefore the term must be of the form @{text "(Const \<dots> $ t1) $ t2"}. The
conversion is then applied to @{text "t2"} which in the example above
stands for @{term "True \<and> Q"}. The function @{ML Conv.fun_conv} applies
the conversion to the first argument of an application.
@@ -1858,13 +1864,14 @@
end"
"\<lambda>P. True \<and> P \<and> Foo \<equiv> \<lambda>P. P \<and> 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 \<and> \<dots>"}
- (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 \<and> \<dots>"};
+ 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] \<longrightarrow> True \<and> 1 \<noteq> x \<equiv> distinct [1, x] \<longrightarrow> 1 \<noteq> 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 \<and> 1 \<noteq> 2) then True \<and> True else True \<and> False\"}
+ @{cterm \"if P (True \<and> 1 \<noteq> 2) then True \<and> True else True \<and> 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 "\<And>x. P \<Longrightarrow>
- 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 "\<And>x. P \<Longrightarrow>
+ 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}