
diff -r 4aa8a80e37ff -r 6dafb0815ae6 CookBook/Tactical.thy
--- a/CookBook/Tactical.thy	Wed Feb 25 16:49:20 2009 +0000
+++ b/CookBook/Tactical.thy	Wed Feb 25 21:55:08 2009 +0000
@@ -727,6 +727,8 @@
   the first goal. To do this can result in quite messy code. In contrast, 
   the ``reverse application'' is easy to implement.
 
+  (FIXME: mention @{ML "CSUBGOAL"})
+
   Of course, this example is contrived: there are much simpler methods available in 
   Isabelle for implementing a proof procedure analysing a goal according to its topmost
   connective. These simpler methods use tactic combinators, which we will explain 
@@ -1319,24 +1321,27 @@
 
 text {*
 
-  Conversions are a ``thin'' layer on top of Isabelle's inference kernel, and 
+  Conversions are a thin layer on top of Isabelle's inference kernel, and 
   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
+  One difference between conversions and the simplifier is that the former
+  act on @{ML_type cterm}s while the latter acts on @{ML_type thm}s. 
+  However, we will also show in this section how conversions can be applied
+  to theorems via tactics. The type for conversions is
 *}
 
 ML{*type conv = Thm.cterm -> Thm.thm*}
 
 text {*
-  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:
+  whereby the produced 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 \"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}
+  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}" 
@@ -1355,16 +1360,31 @@
 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.
+  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.
+  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
+  #prop (rep_thm 
+          (Thm.beta_conversion true (Thm.capply (Thm.capply add two) ten)))
+end"
+"Const (\"==\",\<dots>) $ 
+  (Abs (\"x\",\<dots>,Abs (\"y\",\<dots>,\<dots>)) $\<dots>$\<dots>) $ 
+    (Const (\"HOL.plus_class.plus\",\<dots>) $ \<dots> $ \<dots>)"} 
 
   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
+  the right-hand side will be fully beta-normalised. If instead 
+  @{ML false} is given, then only a single beta-reduction is performed 
+  on the outer-most level. For example
 
   @{ML_response_fake [display,gray]
   "let
@@ -1376,18 +1396,19 @@
   "((\<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"}.
+  @{text "\<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:
-
+  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:
 *}
 
 lemma true_conj1: "True \<and> P \<equiv> P" by simp
 
 text {* 
-  then we can use it in order to rewrite @{term "True \<and> (Foo \<longrightarrow> Bar)"}:
+  You can see how this function works with the example 
+  @{term "True \<and> (Foo \<longrightarrow> Bar)"}:
 
   @{ML_response_fake [display,gray]
 "let 
@@ -1397,8 +1418,10 @@
 end"
   "True \<and> (Foo \<longrightarrow> Bar) \<equiv> Foo \<longrightarrow> Bar"}
 
-  The function @{ML Conv.rewr_conv} only does rewriting on the outer-most
-  level, otherwise it raises the exception @{ML CTERM}.
+  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 
+  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
@@ -1407,38 +1430,42 @@
 
   @{ML_response_fake [display,gray]
 "let
-  val conv1 = Thm.beta_conversion true
+  val conv1 = Thm.beta_conversion false
   val conv2 = Conv.rewr_conv @{thm true_conj1}
-  val ctrm = Thm.capply (@{cterm \"\<lambda>x. x \<and> False\"}) (@{cterm \"True\"})
+  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"}
 
+  where we first beta-reduce the term and then rewrite according to
+  @{thm [source] true_conj1}. 
+
   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]
 "let
-  val conv = Conv.rewr_conv @{thm true_conj1} 
-             else_conv Conv.all_conv
+  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)"}
+"(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.
+  does not fail, however, because the combinator @{ML else_conv} will then 
+  try out @{ML Conv.all_conv}, which always 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
+  Apart from the function @{ML beta_conversion in Thm}, which able to fully
+  beta-normalise a term, the restriction of conversions so far is that they
+  only apply to the outer-most level of a @{ML_type cterm}. In what follows we
+  will lift this restriction. The combinator @{ML Conv.arg_conv} will apply
+  the conversion on the first argument of an application, that 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]
 "let 
@@ -1449,68 +1476,111 @@
 end"
 "P \<or> (True \<and> Q) \<equiv> P \<or> Q"}
 
-  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"}.
+  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
+  conversion is then applied to @{text "t2"} which in the example above
+  stands for @{term "True \<and> Q"}.
+
+  The function @{ML Conv.abs_conv} applies a conversion under an abstractions.
+  For example:
 
+  @{ML_response_fake [display,gray]
+"let 
+  val conv = K (Conv.rewr_conv @{thm true_conj1}) 
+  val ctrm = @{cterm \"\<lambda>P. True \<and> P \<and> Foo\"}
+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
+  @{ML Conv.combination_conv}. It expects two conversions, which each of them
+  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.
 *}
 
-
-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
+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}) ct
-  | _ $ _ => Conv.combination_conv (all_true1_conv ctxt)
-      (all_true1_conv ctxt) ct
-  | Abs _ => Conv.abs_conv (fn (_, cx) => all_true1_conv cx) ctxt ct
-  | _ => Conv.all_conv ct)*}
+         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 {*
-  Here is this conversion in action:
+  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). To see this 
+  conversion in action, consider the following example.
 
-  @{ML_response_fake [display,gray]
-  "all_true1_conv @{context}
-  @{cterm \"distinct [1, x] \<longrightarrow> True \<and> 1 \<noteq> x\"}"
+@{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"}
 
-  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}:
+  To see how much control you have about rewriting via 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. The 
+  the conversion should be as follows.
 *}
 
-ML{*fun if_true1_conv ctxt ct =
-  (case Thm.term_of ct of
+ML{*fun if_true1_conv ctxt ctrm =
+  case Thm.term_of ctrm of
     Const (@{const_name If}, _) $ _ =>
-      Conv.arg_conv (all_true1_conv ctxt) ct
-  | _ $ _ => Conv.combination_conv (if_true1_conv ctxt)
-      (if_true1_conv ctxt) ct
-  | Abs _ => Conv.abs_conv (fn (_, cx) => if_true1_conv cx) ctxt ct
-  | _ => Conv.all_conv ct)*}
+      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 application of this conversion:
 
   @{ML_response_fake [display,gray]
-  "if_true1_conv @{context}
-  @{cterm \"if P (True \<and> 1 \<noteq> 2) then True \<and> True else True \<and> False\"}"
-  "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"}
+"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"}
 *}
 
 text {*
-  Conversions can also be turned into a tactic with the @{ML CONVERSION}
-  tactical, and there are predefined conversionals to traverse a goal state.
-  Given a state @{term "\<And>x. P \<Longrightarrow> Q"},  the conversional
-  @{ML Conv.params_conv} applies a conversion to @{term "P \<Longrightarrow> Q"};
-  given a state @{term "\<lbrakk> P1; P2 \<rbrakk> \<Longrightarrow> Q"},
-  the conversional @{ML Conv.prems_conv} applies a conversion to the premises
-  @{term P1} and @{term P2}, and @{ML Conv.concl_conv} applies a conversion to
-  the conclusion @{term Q}.
+  So far we only applied conversions to @{ML_type cterm}s. Conversions can, however, 
+  also work on theorems using the function @{ML "Conv.fconv_rule"}. As an example, 
+  consider @{ML all_true1_conv} and the lemma:
+*}
+
+lemma foo_test: "P \<or> (True \<and> \<not>P)" by simp
+
+text {*
+  Using the conversion you can transform this theorem into a new theorem
+  as follows
+
+  @{ML_response_fake [display,gray]
+  "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
+  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
+  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 in the premises.
@@ -1518,36 +1588,38 @@
 *}
 
 ML{*val true1_tac = CSUBGOAL (fn (goal, i) =>
-  let val ctxt = ProofContext.init (Thm.theory_of_cterm goal)
+  let 
+    val ctxt = ProofContext.init (Thm.theory_of_cterm goal)
   in
-    CONVERSION (
-      Conv.params_conv ~1 (fn cx =>
-        (Conv.prems_conv ~1 (if_true1_conv cx)) then_conv
-          Conv.concl_conv ~1 (all_true1_conv cx)) ctxt) i
+    CONVERSION 
+      (Conv.params_conv ~1 (fn ctxt =>
+        (Conv.prems_conv ~1 (if_true1_conv ctxt)) then_conv
+          Conv.concl_conv ~1 (all_true1_conv ctxt)) ctxt) i
   end)*}
 
 text {* 
-  To demonstrate this tactic, consider the following example:
+  We call the conversions with the argument @{ML "~1"} in order to 
+  analyse all parameters, premises and conclusions. If we call it with 
+  a non-negative number, say @{text n}, then these conversions will 
+  only be called on @{text n} premises (similar for parameters and
+  conclusions). To test the tactic, consider the proof
 *}
 
 lemma
   "if True \<and> P then P else True \<and> False \<Longrightarrow>
   (if True \<and> Q then Q else P) \<longrightarrow> True \<and> (True \<and> Q)"
 apply(tactic {* true1_tac 1 *})
-txt {* \begin{minipage}{\textwidth}
+txt {* where the tactic yields the goal state
+
+       \begin{minipage}{\textwidth}
        @{subgoals [display]} 
        \end{minipage} *}
 (*<*)oops(*>*)
 
 text {*
-  Conversions are not restricted to work on certified terms only, they can also
-  be lifted to theorem transformers, i.e. functions mapping a theorem to a
-  theorem, by the help of @{ML Conv.fconv_rule}. As an example, consider the
-  conversion @{ML all_true1_conv} again:
-
-  @{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"}
+  To sum up this section, conversions are not as powerful as the simplifier
+  and simprocs; the advantage of conversions, however, is that you never have
+  to worry about non-termination.
 
   \begin{readmore}
   See @{ML_file "Pure/conv.ML"} for more information about conversion combinators. 




