# HG changeset patch
# User boehmes
# Date 1235553023 -3600
# Node ID ed1eb9cb2533a0a91d846fb702bab1945c36cd5d
# Parent  8c31b729a5df436705b7b91de8d8934f3d5ad647
Improved conversion subsection.

diff -r 8c31b729a5df -r ed1eb9cb2533 CookBook/Tactical.thy
--- a/CookBook/Tactical.thy	Tue Feb 24 14:35:07 2009 +0100
+++ b/CookBook/Tactical.thy	Wed Feb 25 10:10:23 2009 +0100
@@ -1317,97 +1317,125 @@
 section {* Conversions *}
 
 text {*
-conversions: core of the simplifier
-
-see: Pure/conv.ML
+Conversions are meta-equalities depending on some input term. There type is
+as follows:
 *}
 
-ML {* type conv = Thm.cterm -> Thm.thm *}
+ML {*type conv = Thm.cterm -> Thm.thm*}
 
 text {*
-simple example:
-*}
+The simplest two conversions are @{ML "Conv.all_conv"} and @{ML "Conv.no_conv"}:
 
-lemma true_conj_1: "True \<and> P \<equiv> P" by simp
+@{ML_response_fake "Conv.all_conv @{cterm True}" "True \<equiv> True"}
 
-ML {*
-val true1_conv = Conv.rewr_conv @{thm true_conj_1}
-*}
+@{ML_response_fake "Conv.no_conv @{cterm True}" "*** Exception- CTERM (\"no conversion\", []) raised"}
 
-ML {*
-true1_conv @{cterm "True \<and> False"}
+Further basic conversions are, for example, @{ML "Thm.beta_conversion"} and
+ @{ML "Conv.rewr_conv"}:
 *}
 
-text {*
-@{ML_response_fake "true1_conv @{cterm \"True \<and> False\"}"
-  "True \<and> False \<equiv> False"}
-*}
+lemma true_conj1: "True \<and> P \<equiv> P" by simp
 
 text {*
-how to extend rewriting to more complex cases? e.g.:
+@{ML_response_fake "Thm.beta_conversion true @{cterm \"(\<lambda>x. x \<or> False) True\"}"
+"(\<lambda>x. x \<or> False) True \<equiv> True \<or> False"}
+
+@{ML_response_fake "Conv.rewr_conv @{thm true_conj1} @{cterm \"True \<or> False\"}"
+ "True \<and> False \<equiv> False"}
+
+Basic conversions can be combined with a number of conversionals, i.e.
+conversion combinators:
+
+@{ML_response_fake "Conv.then_conv (Thm.beta_conversion true, Conv.rewr_conv @{thm true_conj1}) @{cterm \"(\<lambda>x. x \<and> False) True\"}" "(\<lambda>x. x \<and> False) True \<equiv> False"}
+
+@{ML_response_fake "Conv.else_conv (Conv.rewr_conv @{thm true_conj1}, Conv.all_conv) @{cterm \"P \<or> (True \<and> Q)\"}" "P \<or> (True \<and> Q) \<equiv> P \<or> (True \<and> Q)"}
+
+@{ML_response_fake "Conv.arg_conv (Conv.rewr_conv @{thm true_conj1}) @{cterm \"P \<or> (True \<and> Q)\"}" "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}
+
+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. We
+will demonstrate this feature in the following example.
+
+For the moment, let's assumes we want to simplify according to the rewrite rule
+@{thm true_conj1}. As a conversion, this may look as follows:
 *}
 
-ML {*
-val complex = @{cterm "distinct [1, x] \<longrightarrow> True \<and> 1 \<noteq> (x::int)"}
+ML {*fun all_true1_conv ctxt ct =
+  (case Thm.term_of ct of
+    @{term "op \<and>"} $ @{term True} $ _ => 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)*}
+
+text {*
+Here is the new conversion in action:
+
+@{ML_response_fake "all_true1_conv @{context} @{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's complicate the task: Rewrite according to the rule
+@{thm true_conj1}, but only in the first arguments of @{term If}:
 *}
 
-text {* conversionals: basically a count-down version of MetaSimplifier.rewrite *}
+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
+  | _ => Conv.all_conv ct)*}
 
-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 {*
+Here is an application of this new conversion:
+
+@{ML_response_fake "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"}
 *}
 
 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"}
+Conversions can also be turned into a tactic with the @{ML CONVERSION}
+tactical, and there are predefined conversionals to traverse a goal state
+
+@{term "\<And>x. P \<Longrightarrow> Q"}: 
+
+The conversional
+@{ML Conv.params_conv} applies a conversion to @{term "P \<Longrightarrow> Q"},
+@{ML Conv.prems_conv} applies a conversion to all premises in @{term "P \<Longrightarrow> Q"}, and
+@{ML Conv.concl_conv} applies a conversion to the conclusion @{term Q} in @{term "P \<Longrightarrow> Q"}.
+
+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.
+Here is a tactic doing exactly that:
 *}
 
+ML {*local open Conv 
+in
+val true1_tac = CSUBGOAL (fn (goal, i) =>
+  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
+  end)
+end*}
+
+text {* FIXME: give example, show that the conditional rewriting works *}
+
 
 text {*
-transforming theorems: @{ML "Conv.fconv_rule"} (give type)
-
-example:
-*}
-
-lemma foo: "True \<and> (P \<or> \<not>P)" by simp
+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:
 
-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)
+@{ML_response_fake "Conv.fconv_rule (all_true1_conv @{context}) @{lemma \"P \<or> (True \<and> \<not>P)\" by simp}" "P \<or> \<not>P"}
 *}
 
-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 *}
-
 
 
 
@@ -1453,4 +1481,4 @@
 
 
 
-end
\ No newline at end of file
+end
diff -r 8c31b729a5df -r ed1eb9cb2533 cookbook.pdf
Binary file cookbook.pdf has changed