
diff -r eaba1442c516 -r f1ba430a5e7d CookBook/Tactical.thy
--- a/CookBook/Tactical.thy	Wed Feb 25 11:28:41 2009 +0000
+++ b/CookBook/Tactical.thy	Wed Feb 25 12:08:32 2009 +0000
@@ -1318,71 +1318,79 @@
 section {* Conversions\label{sec:conversion} *}
 
 text {*
-Conversions are meta-equalities depending on some input term. Their type is
-as follows:
+
+  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:
 *}
 
-ML {*type conv = Thm.cterm -> Thm.thm*}
+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:
+  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:
 
-@{ML_response_fake "Conv.all_conv @{cterm True}" "True \<equiv> True"}
-
-@{ML_response_fake "Conv.no_conv @{cterm True}" "*** Exception- CTERM (\"no conversion\", []) raised"}
+  @{ML_response_fake [display,gray]
+  "Conv.all_conv @{cterm True}" "True \<equiv> True"}
 
-A further basic conversion is, for example, @{ML "Thm.beta_conversion"}:
+  @{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"}:
 
-@{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 [display,gray]
+  "Thm.beta_conversion true @{cterm \"(\<lambda>x. x \<or> False) True\"}"
+  "(\<lambda>x. x \<or> False) True \<equiv> True \<or> False"}
 
-User-defined rewrite rules can be applied by the conversion
-@{ML "Conv.rewr_conv"}. Consider, for example, the following rule:
+  User-defined rewrite rules can be applied by the conversion
+  @{ML "Conv.rewr_conv"}. Consider, for example, the following rule:
 *}
 
 lemma true_conj1: "True \<and> P \<equiv> P" by simp
 
 text {*
-Here is how this rule can be used for rewriting:
+  Here is how this rule can be used for rewriting:
 
-@{ML_response_fake "Conv.rewr_conv @{thm true_conj1} @{cterm \"True \<or> False\"}"
- "True \<and> False \<equiv> False"}
+  @{ML_response_fake [display,gray]
+  "Conv.rewr_conv @{thm true_conj1} @{cterm \"True \<or> False\"}"
+  "True \<and> False \<equiv> False"}
 *}
 
 text {*
-Basic conversions can be combined with a number of conversionals, i.e.
-conversion combinators:
+  Basic conversions can be combined with a number of conversionals, i.e.
+  conversion combinators:
 
-@{ML_response_fake
-"(Thm.beta_conversion true then_conv Conv.rewr_conv @{thm true_conj1})
+  @{ML_response_fake [display,gray]
+  "(Thm.beta_conversion true then_conv Conv.rewr_conv @{thm true_conj1})
   @{cterm \"(\<lambda>x. x \<and> False) True\"}"
-"(\<lambda>x. x \<and> False) True \<equiv> False"}
+  "(\<lambda>x. x \<and> False) True \<equiv> False"}
 
-@{ML_response_fake
-"(Conv.rewr_conv @{thm true_conj1} else_conv Conv.all_conv)
+  @{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)"}
+  "P \<or> (True \<and> Q) \<equiv> P \<or> (True \<and> Q)"}
 
-@{ML_response_fake
-"Conv.arg_conv (Conv.rewr_conv @{thm true_conj1})
+  @{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"}
+  "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}
+  \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.
+  We will demonstrate this feature in the following example.
 
-To begin with, let's assumes we want to simplify with the rewrite rule
-@{text true_conj1}. As a conversion, this may look as follows:
+  To begin with, let's 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 =
+ML{*fun all_true1_conv ctxt ct =
   (case Thm.term_of ct of
     @{term "op \<and>"} $ @{term True} $ _ => 
       (Conv.arg_conv (all_true1_conv ctxt) then_conv
@@ -1393,18 +1401,18 @@
   | _ => Conv.all_conv ct)*}
 
 text {*
-Here is this conversion in action:
+  Here is this conversion in action:
 
-@{ML_response_fake
-"all_true1_conv @{context}
+  @{ML_response_fake [display,gray]
+  "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"}
+  "distinct [1, x] \<longrightarrow> True \<and> 1 \<noteq> x \<equiv> distinct [1, x] \<longrightarrow> 1 \<noteq> x"}
 
-Now, let's complicate the task a bit: Rewrite according to the rule
-@{text true_conj1}, but only in the first arguments of @{term If}:
+  Now, let make the task a bit more  complicated by rewrite according to the rule
+  @{text true_conj1}, but only in the first arguments of @{term If}:
 *}
 
-ML {*fun if_true1_conv ctxt ct =
+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
@@ -1414,30 +1422,30 @@
   | _ => Conv.all_conv ct)*}
 
 text {*
-Here is an application of this conversion:
+  Here is an application of this conversion:
 
-@{ML_response_fake
-"if_true1_conv @{context}
+  @{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"}
+  "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}.
+  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}.
 
-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:
+  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 {*val true1_tac = CSUBGOAL (fn (goal, i) =>
+ML{*val true1_tac = CSUBGOAL (fn (goal, i) =>
   let val ctxt = ProofContext.init (Thm.theory_of_cterm goal)
   in
     CONVERSION (
@@ -1447,7 +1455,7 @@
   end)*}
 
 text {* 
-To demonstrate this tactic, consider the following example:
+  To demonstrate this tactic, consider the following example:
 *}
 
 lemma
@@ -1460,20 +1468,18 @@
 (*<*)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:
+  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
-"Conv.fconv_rule (all_true1_conv @{context})
-  @{lemma \"P \<or> (True \<and> \<not>P)\" by simp}" "P \<or> \<not>P"}
+  @{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"}
 *}
 
 
 
-
-
 section {* Structured Proofs *}
 
 text {* TBD *}




