--- a/CookBook/Tactical.thy Wed Feb 25 10:14:42 2009 +0100
+++ b/CookBook/Tactical.thy Wed Feb 25 11:07:43 2009 +0100
@@ -1,5 +1,6 @@
theory Tactical
imports Base FirstSteps
+uses "infix_conv.ML"
begin
chapter {* Tactical Reasoning\label{chp:tactical} *}
@@ -1317,40 +1318,55 @@
section {* Conversions\label{sec:conversion} *}
text {*
-Conversions are meta-equalities depending on some input term. There type is
+Conversions are meta-equalities depending on some input term. Their type is
as follows:
*}
ML {*type conv = Thm.cterm -> Thm.thm*}
text {*
-The simplest two conversions are @{ML "Conv.all_conv"} and @{ML "Conv.no_conv"}:
+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"}
-Further basic conversions are, for example, @{ML "Thm.beta_conversion"} and
- @{ML "Conv.rewr_conv"}:
+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"}
+
+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 {*
-@{ML_response_fake "Thm.beta_conversion true @{cterm \"(\<lambda>x. x \<or> False) True\"}"
-"(\<lambda>x. x \<or> False) True \<equiv> True \<or> False"}
+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"}
+*}
+text {*
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
+"(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"}
-@{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.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)"}
-@{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"}
+@{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
@@ -1362,70 +1378,86 @@
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:
+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 =
(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
+ @{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)*}
text {*
-Here is the new conversion in action:
+Here is this 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"}
+@{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}:
+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}:
*}
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
+ 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)*}
text {*
-Here is an application of this new conversion:
+Here is an application of this 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"}
+@{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 {*
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"}.
+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:
*}
-ML {*local open Conv
-in
-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 (
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*}
+ Conv.concl_conv ~1 (all_true1_conv cx)) ctxt) i
+ end)*}
+
+text {*
+To demonstrate this tactic, consider the following example:
+*}
-text {* FIXME: give example, show that the conditional rewriting works *}
-
+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}
+ @{subgoals [display]}
+ \end{minipage} *}
+(*<*)oops(*>*)
text {*
Conversions are not restricted to work on certified terms only, they can also
@@ -1433,7 +1465,9 @@
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
+"Conv.fconv_rule (all_true1_conv @{context})
+ @{lemma \"P \<or> (True \<and> \<not>P)\" by simp}" "P \<or> \<not>P"}
*}