# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1235580560 0
# Node ID 4aa8a80e37ff2ab3d2ddff28aebf7852955e3915
# Parent  f1ba430a5e7d27e26b39bd2cd0b42bf434c82042
some polishing about conversions

diff -r f1ba430a5e7d -r 4aa8a80e37ff CookBook/Tactical.thy
--- 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}
 *}
 
 
diff -r f1ba430a5e7d -r 4aa8a80e37ff cookbook.pdf
Binary file cookbook.pdf has changed