
diff -r 3d27d77c351f -r f8d020bbc2c0 ProgTutorial/Tactical.thy
--- a/ProgTutorial/Tactical.thy	Wed Nov 25 21:00:31 2009 +0100
+++ b/ProgTutorial/Tactical.thy	Tue Dec 01 12:25:34 2009 +0100
@@ -2077,10 +2077,10 @@
 text {*
   Conversions are a thin layer on top of Isabelle's inference kernel, and 
   can be viewed as a controllable, bare-bone version of Isabelle's simplifier.
-  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. 
+  One difference between a conversion and the simplifier is that the former
+  acts 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
+  to theorems and used as tactics. The type for conversions is
 *}
 
 ML{*type conv = cterm -> thm*}
@@ -2118,7 +2118,7 @@
   If you run this example, you will notice that the actual response is the 
   seemingly nonsensical @{term
   "2 + 10 \<equiv> 2 + (10::nat)"}. The reason is that the pretty-printer for
-  @{ML_type cterm}s eta-normalises terms and therefore produces this output.
+  @{ML_type cterm}s eta-normalises (sic) terms and therefore produces this output.
   If we get hold of the ``raw'' representation of the produced theorem, 
   we obtain the expected result.
 
@@ -2204,10 +2204,8 @@
   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, however, because the combinator @{ML else_conv in Conv} will then 
-  try out @{ML all_conv in Conv}, which always succeeds.
-
-  The conversion combinator @{ML_ind try_conv in Conv} constructs a conversion 
-  which is tried out on a term, but in case of failure just does nothing.
+  try out @{ML all_conv in Conv}, which always succeeds. The same
+  behaviour can also be achieved with conversion combinator @{ML_ind try_conv in Conv}.
   For example
   
   @{ML_response_fake [display,gray]
@@ -2219,6 +2217,10 @@
 end"
   "True \<or> P \<equiv> True \<or> P"}
 
+  Rewriting with more than one theorem can be done using the function 
+  @{ML_ind rewrs_conv in More_Conv} from the structure @{ML_struct More_Conv}.
+  
+
   Apart from the function @{ML beta_conversion in Thm}, which is able to fully
   beta-normalise a term, the conversions so far are restricted in that they
   only apply to the outer-most level of a @{ML_type cterm}. In what follows we
@@ -2269,13 +2271,13 @@
   in all possible positions.
 *}
 
-ML %linenosgray{*fun all_true1_conv ctxt ctrm =
+ML %linenosgray{*fun true_conj1_conv ctxt ctrm =
   case (Thm.term_of ctrm) of
     @{term "op \<and>"} $ @{term True} $ _ => 
-      (Conv.arg_conv (all_true1_conv ctxt) then_conv
+      (Conv.arg_conv (true_conj1_conv ctxt) then_conv
          Conv.rewr_conv @{thm true_conj1}) ctrm
-  | _ $ _ => Conv.comb_conv (all_true1_conv ctxt) ctrm
-  | Abs _ => Conv.abs_conv (fn (_, ctxt) => all_true1_conv ctxt) ctxt ctrm
+  | _ $ _ => Conv.comb_conv (true_conj1_conv ctxt) ctrm
+  | Abs _ => Conv.abs_conv (fn (_, ctxt) => true_conj1_conv ctxt) ctxt ctrm
   | _ => Conv.all_conv ctrm*}
 
 text {*
@@ -2288,12 +2290,57 @@
 
 @{ML_response_fake [display,gray]
 "let
-  val conv = all_true1_conv @{context}
-  val ctrm = @{cterm \"distinct [1, x] \<longrightarrow> True \<and> 1 \<noteq> x\"}
+  val conv = true_conj1_conv @{context}
+  val ctrm = @{cterm \"distinct [1::nat, x] \<longrightarrow> True \<and> 1 \<noteq> x\"}
 in
   conv ctrm
 end"
   "distinct [1, x] \<longrightarrow> True \<and> 1 \<noteq> x \<equiv> distinct [1, x] \<longrightarrow> 1 \<noteq> x"}
+*}
+
+text {*
+  Conversions that traverse terms, like @{ML true_conj1_conv} above, can be
+  implemented more succinctly with the combinators @{ML_ind bottom_conv in
+  More_Conv} and @{ML_ind top_conv in More_Conv}. For example:
+*}
+
+ML{*fun true_conj1_conv ctxt =
+let
+  val conv = Conv.try_conv (Conv.rewr_conv @{thm true_conj1})
+in
+  More_Conv.bottom_conv (K conv) ctxt
+end*}
+
+text {*
+  The function @{ML bottom_conv in More_Conv} traverses first the the term and
+  on the ``way down'' applies the conversion, whereas @{ML top_conv in
+  More_Conv} applies the on the ``way up''. To see the difference, 
+  assume the following two meta-equations.
+*}
+
+lemma conj_assoc:
+  fixes A B C::bool
+  shows "A \<and> (B \<and> C) \<equiv> (A \<and> B) \<and> C"
+  and   "(A \<and> B) \<and> C \<equiv> A \<and> (B \<and> C)"
+by simp_all
+
+text {*
+  and the @{ML_type cterm} @{text "(a \<and> (b \<and> c)) \<and> d"}. The reader should
+  pause for a moment to be convinced that rewriting top-down and bottom-up 
+  according to the lemma produces two results. 
+
+  @{ML_response_fake [display, gray]
+  "let
+  val ctxt = @{context}
+  val conv = Conv.try_conv (More_Conv.rewrs_conv @{thms conj_assoc})
+  val conv_top = More_Conv.top_conv (K conv) ctxt
+  val conv_bot = More_Conv.bottom_conv (K conv) ctxt
+  val ctrm = @{cterm \"(a \<and> (b \<and> c)) \<and> d\"}
+in
+  (conv_top ctrm, conv_bot ctrm)
+end"
+  "(\"(a \<and> (b \<and> c)) \<and> d \<equiv> a \<and> (b \<and> (c \<and> d))\",
+ \"(a \<and> (b \<and> c)) \<and> d \<equiv> (a \<and> b) \<and> (c \<and> d)\")"}
 
   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
@@ -2301,24 +2348,31 @@
   the conversion should be as follows.
 *}
 
-ML{*fun if_true1_conv ctxt ctrm =
+ML{*fun if_true1_simple_conv ctxt ctrm =
   case Thm.term_of ctrm of
     Const (@{const_name If}, _) $ _ =>
-      Conv.arg_conv (all_true1_conv ctxt) ctrm
-  | _ $ _ => Conv.comb_conv (if_true1_conv ctxt) ctrm
-  | Abs _ => Conv.abs_conv (fn (_, ctxt) => if_true1_conv ctxt) ctxt ctrm
-  | _ => Conv.all_conv ctrm *}
+      Conv.arg_conv (true_conj1_conv ctxt) ctrm
+  | _ => Conv.no_conv ctrm 
+
+val if_true1_conv = More_Conv.top_sweep_conv if_true1_simple_conv*}
 
 text {*
-  Here is an example for this conversion:
+  In the first function we only treat the top-most redex and also only the
+  success case and otherwise return @{ML no_conv in Conv}.  To apply this
+  conversion inside a term, we use in the last line the combinator @{ML_ind
+  top_sweep_conv in More_Conv}, which traverses the term starting from the
+  root and applies it to all the redexes on the way, but stops in a branch as
+  soon as it found one redex.\footnote{\bf Fixme: Check with Sascha whether
+  the conversion stops after a single success case, or stops in each branch
+  after a success case.} Here is an example for this conversion:
+
 
   @{ML_response_fake [display,gray]
 "let
-  val conv = if_true1_conv @{context}
-  val ctrm = 
-       @{cterm \"if P (True \<and> 1 \<noteq> 2) then True \<and> True else True \<and> False\"}
+  val ctrm = @{cterm \"if P (True \<and> 1 \<noteq> (2::nat)) 
+                        then True \<and> True else True \<and> False\"}
 in
-  conv ctrm
+  if_true1_conv @{context} 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"}
@@ -2327,19 +2381,19 @@
 text {*
   So far we only applied conversions to @{ML_type cterm}s. Conversions can, however, 
   also work on theorems using the function @{ML_ind  fconv_rule in Conv}. As an example, 
-  consider the conversion @{ML all_true1_conv} and the lemma:
+  consider the conversion @{ML true_conj1_conv} and the lemma:
 *}
 
 lemma foo_test: 
   shows "P \<or> (True \<and> \<not>P)" by simp
 
 text {*
-  Using the conversion @{ML all_true1_conv} you can transform this theorem into a 
+  Using the conversion @{ML true_conj1_conv} you can transform this theorem into a 
   new theorem as follows
 
   @{ML_response_fake [display,gray]
 "let
-  val conv = Conv.fconv_rule (all_true1_conv @{context}) 
+  val conv = Conv.fconv_rule (true_conj1_conv @{context}) 
   val thm = @{thm foo_test}
 in
   conv thm
@@ -2363,7 +2417,7 @@
   conclusion of a goal.
   \end{itemize}
 
-  Assume we want to apply @{ML all_true1_conv} only in the conclusion
+  Assume we want to apply @{ML true_conj1_conv} only in the conclusion
   of the goal, and @{ML if_true1_conv} should only apply to the premises.
   Here is a tactic doing exactly that:
 *}
@@ -2372,7 +2426,7 @@
   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)*}
+          Conv.concl_conv ~1 (true_conj1_conv ctxt))) ctxt)*}
 
 text {* 
   We call the conversions with the argument @{ML "~1"}. This is to 
@@ -2394,7 +2448,7 @@
 
 text {*
   As you can see, the premises are rewritten according to @{ML if_true1_conv}, while
-  the conclusion according to @{ML all_true1_conv}.
+  the conclusion according to @{ML true_conj1_conv}.
 
   Conversions can also be helpful for constructing meta-equality theorems.
   Such theorems are often definitions. As an example consider the following




