isabelle-cookbook: comparison CookBook/Tactical.thy

equal deleted inserted replaced

-:64fa844064fa
+:cc9359bfacf4
 and @{ML_file "Pure/simplifier.ML"}. The simplifier for HOL is set up in
 @{ML_file "HOL/Tools/simpdata.ML"}. Generic splitters are implemented in
 @{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}
 \begin{tabular}{ll}
 @{ML addsimps}   & @{ML delsimps}\\
 @{ML_response_fake [display,gray]
 "Conv.no_conv @{cterm True}"
 "*** 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
 val add = @{cterm \"\<lambda>x y. x + (y::nat)\"}
 val two = @{cterm \"2::nat\"}
 Thm.beta_conversion true (Thm.capply (Thm.capply add two) ten)
 end"
 "((\<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
 if we obtain the ``raw'' representation of the produced theorem, we
 can see the difference:
 @{ML_response [display,gray]
 "let
 val add = @{cterm \"\<lambda>x y. x + (y::nat)\"}
 val two = @{cterm \"2::nat\"}
 val ten = @{cterm \"10::nat\"}
-in
+val thm = Thm.beta_conversion true (Thm.capply (Thm.capply add two) ten)
-#prop (rep_thm
+in
-(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>) $
 (Const (\"HOL.plus_class.plus\",\<dots>) $ \<dots> $ \<dots>)"}
 Again, we actually see as output only the fully normalised term
 @{text "\<lambda>y. 2 + y"}.
 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
+"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:
+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
+You can see how this function works in the example rewriting
-@{term "True \<and> (Foo \<longrightarrow> Bar)"}:
+the @{ML_type cterm} @{term "True \<and> (Foo \<longrightarrow> Bar)"} to @{term "Foo \<longrightarrow> Bar"}.
 @{ML_response_fake [display,gray]
 "let
 val ctrm = @{cterm \"True \<and> (Foo \<longrightarrow> Bar)\"}
 in
 Conv.rewr_conv @{thm true_conj1} ctrm
 end"
 "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}.
 This very primitive way of rewriting can be made more powerful by
 combining several conversions into one. For this you can use conversion
 Conv.arg_conv conv ctrm
 end"
 "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.
 The function @{ML Conv.abs_conv} applies a conversion under an abstractions.
 in
 Conv.abs_conv conv @{context} ctrm
 end"
 "\<lambda>P. True \<and> P \<and> Foo \<equiv> \<lambda>P. P \<and> Foo"}
-The conversion that goes under an application is
+Note that this conversion needs a context as an argument. The conversion that
-@{ML Conv.combination_conv}. It expects two conversions as arguments,
+goes under an application is @{ML Conv.combination_conv}. It expects two conversions
-each of which is applied to the corresponding ``branch'' of the application.
+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
+We can now apply all these functions in a conversion that recursively
-possible positions.
+descends a term and applies a ``@{thm [source] true_conj1}''-conversion
+in all possible positions.
 *}
 ML %linenosgray{*fun all_true1_conv ctxt ctrm =
 case (Thm.term_of ctrm) of
 @{term "op \<and>"} $ @{term True} $ _ =>
 (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
 | 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
+This function ``fires'' if the terms is of the form @{text "True \<and> \<dots>"};
-(Line 8); and ``fires'' if the outer-most constant is an @{text "True \<and> \<dots>"}
+it descends under applications (Line 6 and 7) and abstractions
-(Lines 3-5); otherwise it leaves the term unchanged (Line 9). In Line 2
+(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
 val ctxt = @{context}
 val ctrm = @{cterm \"distinct [1, x] \<longrightarrow> True \<and> 1 \<noteq> x\"}
 in
 all_true1_conv ctxt ctrm
 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
 the conversion should be as follows.
 ML{*fun if_true1_conv ctxt ctrm =
 case Thm.term_of ctrm of
 Const (@{const_name If}, _) $ _ =>
 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 example for this conversion:
 @{ML_response_fake [display,gray]
 "let
 val ctxt = @{context}
 val ctrm =
 @{cterm \"if P (True \<and> 1 \<noteq> 2) then True \<and> True else True \<and> False\"}
 in
 if_true1_conv ctxt ctrm
 end"
 "if P (True \<and> 1 \<noteq> 2) then True \<and> True else True \<and> False
 \<equiv> if P (1 \<noteq> 2) then True \<and> True else True \<and> False"}
 "Conv.fconv_rule (all_true1_conv @{context}) @{thm foo_test}"
 "?P \<or> \<not> ?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
+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>
+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 the conversion to all
+Q"}); the function @{ML Conv.prems_conv} for applying a conversion to all
-premises of a goal, and @{ML Conv.concl_conv} for applying the conversion to
+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:
 *}
 ML{*val true1_tac = CSUBGOAL (fn (goal, i) =>
 let
 the same assumptions as in \ref{ex:addsimproc}. FIXME: the current solution
 requires some additional functions.
 \end{exercise}
 \begin{exercise}
-Compare which way of rewriting such terms is more efficient. For this
+Compare which way (either Exercise ~\ref{addsimproc} or \ref{ex:addconversion}) of
-you might have to construct quite large terms.
+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}
 See @{ML_file "Pure/conv.ML"} for more information about conversion combinators.
 Further conversions are defined in  @{ML_file "Pure/thm.ML"},

changeset 160	cc9359bfacf4
parent 158	d7944bdf7b3f
child 161	83f36a1c62f2