--- a/CookBook/Tactical.thy Wed Feb 25 16:49:20 2009 +0000
+++ b/CookBook/Tactical.thy Wed Feb 25 21:55:08 2009 +0000
@@ -727,6 +727,8 @@
the first goal. To do this can result in quite messy code. In contrast,
the ``reverse application'' is easy to implement.
+ (FIXME: mention @{ML "CSUBGOAL"})
+
Of course, this example is contrived: there are much simpler methods available in
Isabelle for implementing a proof procedure analysing a goal according to its topmost
connective. These simpler methods use tactic combinators, which we will explain
@@ -1319,24 +1321,27 @@
text {*
- Conversions are a ``thin'' layer on top of Isabelle's inference kernel, and
+ Conversions are a thin layer on top of Isabelle's inference kernel, and
can be viewed be as a controllable, bare-bone version of Isabelle's simplifier.
- A difference is that conversions simplify @{ML_type cterm}s, while teh simplifier
- acts on theorems. The type for conversions is
+ 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.
+ However, we will also show in this section how conversions can be applied
+ to theorems via tactics. The type for conversions is
*}
ML{*type conv = Thm.cterm -> Thm.thm*}
text {*
- whereby the theorem is always a meta-equality. A simple conversion is
- the function @{ML "Conv.all_conv"}, which maps a @{ML_type cterm} to an instance of
- the (meta)reflexivity theorem. For example:
+ whereby the produced theorem is always a meta-equality. A simple conversion
+ is the function @{ML "Conv.all_conv"}, which maps a @{ML_type cterm} to an
+ instance of the (meta)reflexivity theorem. For example:
@{ML_response_fake [display,gray]
"Conv.all_conv @{cterm \"Foo \<or> Bar\"}"
"Foo \<or> Bar \<equiv> Foo \<or> Bar"}
- Another simple conversion is @{ML Conv.no_conv} which always raises the exception @{ML CTERM}
+ Another simple conversion is @{ML Conv.no_conv} which always raises the
+ exception @{ML CTERM}.
@{ML_response_fake [display,gray]
"Conv.no_conv @{cterm True}"
@@ -1355,16 +1360,31 @@
end"
"((\<lambda>x y. x + y) 2) 10 \<equiv> 2 + 10"}
- Note that the actual response in the example is @{term "2 + 10 \<equiv> 2 + (10::nat)"},
- since the pretty-printer of @{ML_type cterm}s already beta-normalises terms.
- However, we can by how we constructed the term (using the function
- @{ML Thm.capply}, which is the application @{ML $} for @{ML_type cterm})
- that the left-hand side must contain beta-redexes.
+ Note that the actual response in this example is @{term "2 + 10 \<equiv> 2 + (10::nat)"},
+ since the pretty printer for @{ML_type cterm}s already beta-normalises terms.
+ But by the way how we constructed the term (using the function
+ @{ML Thm.capply}, which is the application @{ML $} for @{ML_type cterm}s),
+ we can be sure the left-hand side must contain beta-redexes. Indeed
+ if we obtain the ``raw'' representation of the produced theorem, we
+ can see the difference:
+
+ @{ML_response [display,gray]
+"let
+ val add = @{cterm \"\<lambda>x y. x + (y::nat)\"}
+ val two = @{cterm \"2::nat\"}
+ val ten = @{cterm \"10::nat\"}
+in
+ #prop (rep_thm
+ (Thm.beta_conversion true (Thm.capply (Thm.capply add two) ten)))
+end"
+"Const (\"==\",\<dots>) $
+ (Abs (\"x\",\<dots>,Abs (\"y\",\<dots>,\<dots>)) $\<dots>$\<dots>) $
+ (Const (\"HOL.plus_class.plus\",\<dots>) $ \<dots> $ \<dots>)"}
The argument @{ML true} in @{ML Thm.beta_conversion} indicates that
- the right-hand side should be fully beta-normalised. If @{ML false} is
- given, then only a beta-reduction is performed on the outer-most level.
- For example
+ the right-hand side will be fully beta-normalised. If instead
+ @{ML false} is given, then only a single beta-reduction is performed
+ on the outer-most level. For example
@{ML_response_fake [display,gray]
"let
@@ -1376,18 +1396,19 @@
"((\<lambda>x y. x + y) 2) \<equiv> \<lambda>y. 2 + y"}
Again, we actually see as output only the fully normalised term
- @{term "\<lambda>y. 2 + y"}.
+ @{text "\<lambda>y. 2 + y"}.
- The main point of conversions is that they can be used for rewriting terms.
- For this you can use the function @{ML "Conv.rewr_conv"}. Suppose we want
- to rewrite a term according to the (meta)equation:
-
+ The main point of conversions is that they can be used for rewriting
+ @{ML_type cterm}s. To do this you can use the function @{ML
+ "Conv.rewr_conv"} which expects a meta-equation as an argument. Suppose we
+ want to rewrite a @{ML_type cterm} according to the (meta)equation:
*}
lemma true_conj1: "True \<and> P \<equiv> P" by simp
text {*
- then we can use it in order to rewrite @{term "True \<and> (Foo \<longrightarrow> Bar)"}:
+ You can see how this function works with the example
+ @{term "True \<and> (Foo \<longrightarrow> Bar)"}:
@{ML_response_fake [display,gray]
"let
@@ -1397,8 +1418,10 @@
end"
"True \<and> (Foo \<longrightarrow> Bar) \<equiv> Foo \<longrightarrow> Bar"}
- The function @{ML Conv.rewr_conv} only does rewriting on the outer-most
- level, otherwise it raises the exception @{ML CTERM}.
+ Note, however, that the function @{ML Conv.rewr_conv} only rewrites the
+ outer-most level of the @{ML_type cterm}. If the given @{ML_type cterm} does not match the
+ left-hand side of the theorem, then @{ML Conv.rewr_conv} raises
+ the exception @{ML CTERM}.
This very primitive way of rewriting can be made more powerful by
combining several conversions into one. For this you can use conversion
@@ -1407,38 +1430,42 @@
@{ML_response_fake [display,gray]
"let
- val conv1 = Thm.beta_conversion true
+ val conv1 = Thm.beta_conversion false
val conv2 = Conv.rewr_conv @{thm true_conj1}
- val ctrm = Thm.capply (@{cterm \"\<lambda>x. x \<and> False\"}) (@{cterm \"True\"})
+ val ctrm = Thm.capply @{cterm \"\<lambda>x. x \<and> False\"} @{cterm \"True\"}
in
(conv1 then_conv conv2) ctrm
end"
"(\<lambda>x. x \<and> False) True \<equiv> False"}
+ where we first beta-reduce the term and then rewrite according to
+ @{thm [source] true_conj1}.
+
The conversion combinator @{ML else_conv} tries out the
first one, and if it does not apply, tries the second. For example
@{ML_response_fake [display,gray]
"let
- val conv = Conv.rewr_conv @{thm true_conj1}
- else_conv Conv.all_conv
+ val conv = Conv.rewr_conv @{thm true_conj1} else_conv Conv.all_conv
val ctrm1 = @{cterm \"True \<and> Q\"}
val ctrm2 = @{cterm \"P \<or> (True \<and> Q)\"}
in
(conv ctrm1, conv ctrm2)
end"
-"(True \<and> Q \<equiv> Q,
- P \<or> True \<and> Q \<equiv> P \<or> True \<and> Q)"}
+"(True \<and> Q \<equiv> Q, P \<or> True \<and> Q \<equiv> P \<or> True \<and> Q)"}
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 because the combinator @{ML else_conv} will then
- try out @{ML Conv.all_conv}, which allways succeeds.
+ does not fail, however, because the combinator @{ML else_conv} will then
+ try out @{ML Conv.all_conv}, which always succeeds.
- The combinator @{ML Conv.arg_conv} will apply the conversion on
- the first argument, taht is the term must be of the form
- @{ML "t1 $ t2" for t1 t2} and the conversion is applied to @{text t2}.
- For example
+ Apart from the function @{ML beta_conversion in Thm}, which able to fully
+ beta-normalise a term, the restriction of conversions so far is that they
+ only apply to the outer-most level of a @{ML_type cterm}. In what follows we
+ will lift this restriction. The combinator @{ML Conv.arg_conv} will apply
+ the conversion on the first argument of an application, that is the term
+ must be of the form @{ML "t1 $ t2" for t1 t2} and the conversion is applied
+ to @{text t2}. For example
@{ML_response_fake [display,gray]
"let
@@ -1449,68 +1476,111 @@
end"
"P \<or> (True \<and> Q) \<equiv> P \<or> Q"}
- The reason for this behaviour is that @{text "(op \<or>)"} expects two arguments
- and so is of the form @{text "Const \<dots> $ t1 $ t2"}. The conversion is then
- applied to @{text "t2"} which stands for @{term "True \<and> Q"}.
+ The reason for this behaviour is that @{text "(op \<or>)"} expects two
+ arguments. So the term must be of the form @{text "Const \<dots> $ t1 $ t2"}. The
+ conversion is then applied to @{text "t2"} which in the example above
+ stands for @{term "True \<and> Q"}.
+
+ The function @{ML Conv.abs_conv} applies a conversion under an abstractions.
+ For example:
+ @{ML_response_fake [display,gray]
+"let
+ val conv = K (Conv.rewr_conv @{thm true_conj1})
+ val ctrm = @{cterm \"\<lambda>P. True \<and> P \<and> Foo\"}
+in
+ Conv.abs_conv conv @{context} ctrm
+end"
+ "\<lambda>P. True \<and> P \<and> Foo \<equiv> \<lambda>P. P \<and> Foo"}
+
+ The conversion that goes under an application is
+ @{ML Conv.combination_conv}. It expects two conversions, which each of them
+ is applied to the corresponding ``branch'' of the application.
+
+ We can now apply all these functions in a
+ conversion that recursively descends a term and applies a conversion in all
+ possible positions.
*}
-
-text {*
- To begin with, let us 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
+ML %linenosgray{*fun all_true1_conv ctxt ctrm =
+ case (Thm.term_of ctrm) of
@{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)*}
+ Conv.rewr_conv @{thm true_conj1}) ctrm
+ | _ $ _ => Conv.combination_conv
+ (all_true1_conv ctxt) (all_true1_conv ctxt) ctrm
+ | Abs _ => Conv.abs_conv (fn (_, ctxt) => all_true1_conv ctxt) ctxt ctrm
+ | _ => Conv.all_conv ctrm*}
text {*
- Here is this conversion in action:
+ This functions descends under applications (Line 6 and 7) and abstractions
+ (Line 8); and ``fires'' if the outer-most constant is an @{text "True \<and> \<dots>"}
+ (Lines 3-5); otherwise it leaves the term unchanged (Line 9). To see this
+ conversion in action, consider the following example.
- @{ML_response_fake [display,gray]
- "all_true1_conv @{context}
- @{cterm \"distinct [1, x] \<longrightarrow> True \<and> 1 \<noteq> x\"}"
+@{ML_response_fake [display,gray]
+"let
+ val ctxt = @{context}
+ val ctrm = @{cterm \"distinct [1, x] \<longrightarrow> True \<and> 1 \<noteq> x\"}
+in
+ all_true1_conv ctxt ctrm
+end"
"distinct [1, x] \<longrightarrow> True \<and> 1 \<noteq> x \<equiv> distinct [1, x] \<longrightarrow> 1 \<noteq> x"}
- Now, let us make the task a bit more complicated by rewriting according to the rule
- @{text true_conj1}, but only in the first arguments of @{term If}:
+ To see how much control you have about rewriting via conversions, let us
+ make the task a bit more complicated by rewriting according to the rule
+ @{text true_conj1}, but only in the first arguments of @{term If}s. The
+ the conversion should be as follows.
*}
-ML{*fun if_true1_conv ctxt ct =
- (case Thm.term_of ct of
+ML{*fun if_true1_conv ctxt ctrm =
+ case Thm.term_of ctrm 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)*}
+ Conv.arg_conv (all_true1_conv ctxt) ctrm
+ | _ $ _ => Conv.combination_conv
+ (if_true1_conv ctxt) (if_true1_conv ctxt) ctrm
+ | Abs _ => Conv.abs_conv (fn (_, ctxt) => if_true1_conv ctxt) ctxt ctrm
+ | _ => Conv.all_conv ctrm *}
text {*
Here is an application of this conversion:
@{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"}
+"let
+ val ctxt = @{context}
+ val ctrm =
+ @{cterm \"if P (True \<and> 1 \<noteq> 2) then True \<and> True else True \<and> False\"}
+in
+ if_true1_conv ctxt 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"}
*}
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}.
+ So far we only applied conversions to @{ML_type cterm}s. Conversions can, however,
+ also work on theorems using the function @{ML "Conv.fconv_rule"}. As an example,
+ consider @{ML all_true1_conv} and the lemma:
+*}
+
+lemma foo_test: "P \<or> (True \<and> \<not>P)" by simp
+
+text {*
+ Using the conversion you can transform this theorem into a new theorem
+ as follows
+
+ @{ML_response_fake [display,gray]
+ "Conv.fconv_rule (all_true1_conv @{context}) @{thm foo_test}"
+ "?P \<or> \<not> ?P"}
+
+ Finally, conversions can also be turned into tactics and then applied to
+ goal states. This can be done with the help of the function @{ML CONVERSION},
+ and also some predefined conversion combinator which traverse a goal
+ state. The combinators for the goal state are: @{ML Conv.params_conv} for
+ going under parameters (i.e.~where goals are of the form @{text "\<And>x. P \<Longrightarrow>
+ Q"}); the function @{ML Conv.prems_conv} for applying the conversion to all
+ premises of a goal, and @{ML Conv.concl_conv} for applying the conversion to
+ the conclusion of a goal.
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.
@@ -1518,36 +1588,38 @@
*}
ML{*val true1_tac = CSUBGOAL (fn (goal, i) =>
- let val ctxt = ProofContext.init (Thm.theory_of_cterm goal)
+ 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
+ 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) i
end)*}
text {*
- To demonstrate this tactic, consider the following example:
+ We call the conversions with the argument @{ML "~1"} in order to
+ analyse all parameters, premises and conclusions. If we call it with
+ a non-negative number, say @{text n}, then these conversions will
+ only be called on @{text n} premises (similar for parameters and
+ conclusions). To test the tactic, consider the proof
*}
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}
+txt {* where the tactic yields the goal state
+
+ \begin{minipage}{\textwidth}
@{subgoals [display]}
\end{minipage} *}
(*<*)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:
-
- @{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"}
+ To sum up this section, conversions are not as powerful as the simplifier
+ and simprocs; the advantage of conversions, however, is that you never have
+ to worry about non-termination.
\begin{readmore}
See @{ML_file "Pure/conv.ML"} for more information about conversion combinators.