--- a/CookBook/Tactical.thy	Tue Feb 24 11:15:41 2009 +0000
+++ b/CookBook/Tactical.thy	Tue Feb 24 14:35:07 2009 +0100
@@ -1316,6 +1316,101 @@
 
 section {* Conversions *}
 
+text {*
+conversions: core of the simplifier
+
+see: Pure/conv.ML
+*}
+
+ML {* type conv = Thm.cterm -> Thm.thm *}
+
+text {*
+simple example:
+*}
+
+lemma true_conj_1: "True \<and> P \<equiv> P" by simp
+
+ML {*
+val true1_conv = Conv.rewr_conv @{thm true_conj_1}
+*}
+
+ML {*
+true1_conv @{cterm "True \<and> False"}
+*}
+
+text {*
+@{ML_response_fake "true1_conv @{cterm \"True \<and> False\"}"
+  "True \<and> False \<equiv> False"}
+*}
+
+text {*
+how to extend rewriting to more complex cases? e.g.:
+*}
+
+ML {*
+val complex = @{cterm "distinct [1, x] \<longrightarrow> True \<and> 1 \<noteq> (x::int)"}
+*}
+
+text {* conversionals: basically a count-down version of MetaSimplifier.rewrite *}
+
+ML {*
+fun all_true1_conv ctxt ct =
+  (case Thm.term_of ct of
+    @{term "op \<and>"} $ @{term True} $ _ => true1_conv 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)
+*}
+
+text {*
+@{ML_response_fake "all_true1_conv @{context} complex"
+  "distinct [1, x] \<longrightarrow> True \<and> 1 \<noteq> x \<equiv> distinct [1, x] \<longrightarrow> 1 \<noteq> x"}
+*}
+
+
+text {*
+transforming theorems: @{ML "Conv.fconv_rule"} (give type)
+
+example:
+*}
+
+lemma foo: "True \<and> (P \<or> \<not>P)" by simp
+
+text {*
+@{ML_response_fake "Conv.fconv_rule (Conv.arg_conv (all_true1_conv @{context})) @{thm foo}" "P \<or> \<not>P"}
+*}
+
+text {* now, replace "True and P" with "P" if it occurs inside an If *}
+
+ML {*
+fun if_true1_conv ctxt ct =
+  (case Thm.term_of ct 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)
+*}
+
+text {* show example *}
+
+text {*
+conversions inside a tactic: replace "true" in conclusion, "if true" in assumptions
+*}
+
+ML {*
+local open Conv 
+in
+fun true1_tac ctxt =
+  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)
+end
+*}
+
+text {* give example, show that the conditional rewriting works *}
+
+
+
+
 
 section {* Structured Proofs *}