--- a/CookBook/Tactical.thy Wed Feb 25 12:08:32 2009 +0000
+++ b/CookBook/Tactical.thy Wed Feb 25 16:49:20 2009 +0000
@@ -1117,12 +1117,12 @@
ML{*val fail_sp' =
- let
- val thy = @{theory}
- val pat = [@{term "Suc n"}]
- in
- Simplifier.simproc_i thy "fail_sp'" pat (K fail_sp_aux')
- end*}
+let
+ val thy = @{theory}
+ val pat = [@{term "Suc n"}]
+in
+ Simplifier.simproc_i thy "fail_sp'" pat (K fail_sp_aux')
+end*}
text {*
Here the pattern is given as @{ML_type term} (instead of @{ML_type cterm}).
@@ -1173,12 +1173,12 @@
*}
ML{*val plus_one_sp =
- let
- val thy = @{theory}
- val pat = [@{term "Suc n"}]
- in
- Simplifier.simproc_i thy "sproc +1" pat (K plus_one_sp_aux)
- end*}
+let
+ val thy = @{theory}
+ val pat = [@{term "Suc n"}]
+in
+ Simplifier.simproc_i thy "sproc +1" pat (K plus_one_sp_aux)
+end*}
text {*
Now the simproc is set up so that it is triggered by terms
@@ -1320,76 +1320,148 @@
text {*
Conversions are a ``thin'' layer on top of Isabelle's inference kernel, and
- may be seen as a controllable, bare-bone version of Isabelle's simplifier.
- They are meta-equalities depending on some input term. Their type is
- as follows:
+ 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
*}
ML{*type conv = Thm.cterm -> Thm.thm*}
text {*
- The simplest two conversions are @{ML "Conv.all_conv"}, which maps a
- term to an instance of the reflexivity theorem, and
- @{ML "Conv.no_conv"}, which always fails:
+ 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:
@{ML_response_fake [display,gray]
- "Conv.all_conv @{cterm True}" "True \<equiv> True"}
+ "Conv.all_conv @{cterm \"Foo \<or> Bar\"}"
+ "Foo \<or> Bar \<equiv> Foo \<or> Bar"}
+
+ 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}"
"*** Exception- CTERM (\"no conversion\", []) raised"}
- A further basic conversion is, for example, @{ML "Thm.beta_conversion"}:
+ 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
@{ML_response_fake [display,gray]
- "Thm.beta_conversion true @{cterm \"(\<lambda>x. x \<or> False) True\"}"
- "(\<lambda>x. x \<or> False) True \<equiv> True \<or> False"}
+ "let
+ val add = @{cterm \"\<lambda>x y. x + (y::nat)\"}
+ val two = @{cterm \"2::nat\"}
+ val ten = @{cterm \"10::nat\"}
+in
+ 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 the example is @{term "2 + 10 \<equiv> 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.
- User-defined rewrite rules can be applied by the conversion
- @{ML "Conv.rewr_conv"}. Consider, for example, the following rule:
+ 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
+
+ @{ML_response_fake [display,gray]
+ "let
+ val add = @{cterm \"\<lambda>x y. x + (y::nat)\"}
+ val two = @{cterm \"2::nat\"}
+in
+ Thm.beta_conversion false (Thm.capply add two)
+end"
+ "((\<lambda>x y. x + y) 2) \<equiv> \<lambda>y. 2 + y"}
+
+ Again, we actually see as output only the fully normalised term
+ @{term "\<lambda>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:
+
*}
lemma true_conj1: "True \<and> P \<equiv> P" by simp
-text {*
- Here is how this rule can be used for rewriting:
+text {*
+ then we can use it in order to rewrite @{term "True \<and> (Foo \<longrightarrow> Bar)"}:
@{ML_response_fake [display,gray]
- "Conv.rewr_conv @{thm true_conj1} @{cterm \"True \<or> False\"}"
- "True \<and> False \<equiv> False"}
-*}
+"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"}
-text {*
- Basic conversions can be combined with a number of conversionals, i.e.
- conversion combinators:
+ The function @{ML Conv.rewr_conv} only does rewriting on the outer-most
+ level, otherwise it 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
+ combinators. The simplest conversion combinator is @{ML then_conv},
+ which applies one conversion after another. For example
@{ML_response_fake [display,gray]
- "(Thm.beta_conversion true then_conv Conv.rewr_conv @{thm true_conj1})
- @{cterm \"(\<lambda>x. x \<and> False) True\"}"
+"let
+ val conv1 = Thm.beta_conversion true
+ val conv2 = Conv.rewr_conv @{thm true_conj1}
+ val ctrm = Thm.capply (@{cterm \"\<lambda>x. x \<and> False\"}) (@{cterm \"True\"})
+in
+ (conv1 then_conv conv2) ctrm
+end"
"(\<lambda>x. x \<and> False) True \<equiv> False"}
+ 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]
- "(Conv.rewr_conv @{thm true_conj1} else_conv Conv.all_conv)
- @{cterm \"P \<or> (True \<and> Q)\"}"
- "P \<or> (True \<and> Q) \<equiv> P \<or> (True \<and> Q)"}
+"let
+ val conv = Conv.rewr_conv @{thm true_conj1}
+ else_conv Conv.all_conv
+ val ctrm1 = @{cterm \"True \<and> Q\"}
+ val ctrm2 = @{cterm \"P \<or> (True \<and> Q)\"}
+in
+ (conv ctrm1, conv ctrm2)
+end"
+"(True \<and> Q \<equiv> Q,
+ P \<or> True \<and> Q \<equiv> P \<or> True \<and> 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.
+
+ 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
@{ML_response_fake [display,gray]
- "Conv.arg_conv (Conv.rewr_conv @{thm true_conj1})
- @{cterm \"P \<or> (True \<and> Q)\"}"
- "P \<or> (True \<and> Q) \<equiv> P \<or> Q"}
+"let
+ val conv = Conv.rewr_conv @{thm true_conj1}
+ val ctrm = @{cterm \"P \<or> (True \<and> Q)\"}
+in
+ Conv.arg_conv conv ctrm
+end"
+"P \<or> (True \<and> Q) \<equiv> P \<or> Q"}
- \begin{readmore}
- See @{ML_file "Pure/conv.ML"} for more conversionals. Further basic conversions
- can be found in, for example, @{ML_file "Pure/thm.ML"},
- @{ML_file "Pure/drule.ML"}, and @{ML_file "Pure/meta_simplifier.ML"}.
- \end{readmore}
+ The reason for this behaviour is that @{text "(op \<or>)"} expects two arguments
+ and so is of the form @{text "Const \<dots> $ t1 $ t2"}. The conversion is then
+ applied to @{text "t2"} which stands for @{term "True \<and> Q"}.
- We will demonstrate this feature in the following example.
+*}
+
- To begin with, let's assumes we want to simplify with the rewrite rule
+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
@{term "op \<and>"} $ @{term True} $ _ =>
@@ -1408,7 +1480,7 @@
@{cterm \"distinct [1, x] \<longrightarrow> True \<and> 1 \<noteq> x\"}"
"distinct [1, x] \<longrightarrow> True \<and> 1 \<noteq> x \<equiv> distinct [1, x] \<longrightarrow> 1 \<noteq> x"}
- Now, let make the task a bit more complicated by rewrite according to the rule
+ 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}:
*}
@@ -1476,6 +1548,12 @@
@{ML_response_fake [display,gray]
"Conv.fconv_rule (all_true1_conv @{context}) @{lemma \"P \<or> (True \<and> \<not>P)\" by simp}"
"P \<or> \<not>P"}
+
+ \begin{readmore}
+ See @{ML_file "Pure/conv.ML"} for more information about conversion combinators.
+ Further conversions are defined in @{ML_file "Pure/thm.ML"},
+ @{ML_file "Pure/drule.ML"} and @{ML_file "Pure/meta_simplifier.ML"}.
+ \end{readmore}
*}