--- a/ProgTutorial/Essential.thy Wed Nov 25 21:00:31 2009 +0100
+++ b/ProgTutorial/Essential.thy Tue Dec 01 12:25:34 2009 +0100
@@ -1685,7 +1685,7 @@
Theorems can also be produced from terms by giving an explicit proof.
One way to achieve this is by using the function @{ML_ind prove in Goal}
in the structure @{ML_struct Goal}. For example below we use this function
- to prove the term @{term "P \<Longrightarrow> P"}.
+ to prove the term @{term "P \<Longrightarrow> P"}.\footnote{\bf FIXME: What about @{ML_ind prove_internal in Goal}?}
@{ML_response_fake [display,gray]
"let
--- a/ProgTutorial/Solutions.thy Wed Nov 25 21:00:31 2009 +0100
+++ b/ProgTutorial/Solutions.thy Tue Dec 01 12:25:34 2009 +0100
@@ -225,7 +225,7 @@
text {* and a test case is the lemma *}
-lemma "P (Suc (99 + 1)) ((0 + 0)::nat) (Suc (3 + 3 + 3)) (4 + 1)"
+lemma "P (Suc (99 + 1)) ((0 + 0)::nat) (Suc (3 + 3 + 3)) ((4 + 1)::nat)"
apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [@{simproc add_sp}]) 1 *})
txt {*
where the simproc produces the goal state
@@ -242,33 +242,28 @@
exercise.
*}
-ML{*fun add_simple_conv ctxt ctrm =
+ML {*fun add_simple_conv ctxt ctrm =
let
- val trm = Thm.term_of ctrm
-in
- get_sum_thm ctxt trm (dest_sum trm)
+ val trm = Thm.term_of ctrm
+in
+ case trm of
+ @{term "(op +)::nat \<Rightarrow> nat \<Rightarrow> nat"} $ _ $ _ =>
+ get_sum_thm ctxt trm (dest_sum trm)
+ | _ => Conv.all_conv ctrm
end
-fun add_conv ctxt ctrm =
- (case Thm.term_of ctrm of
- @{term "(op +)::nat \<Rightarrow> nat \<Rightarrow> nat"} $ _ $ _ =>
- (Conv.binop_conv (add_conv ctxt)
- then_conv (Conv.try_conv (add_simple_conv ctxt))) ctrm
- | _ $ _ => Conv.comb_conv (add_conv ctxt) ctrm
- | Abs _ => Conv.abs_conv (fn (_, ctxt) => add_conv ctxt) ctxt ctrm
- | _ => Conv.all_conv ctrm)
+val add_conv = More_Conv.bottom_conv add_simple_conv
-fun add_tac ctxt = CSUBGOAL (fn (goal, i) =>
- CONVERSION
+fun add_tac ctxt = CONVERSION
(Conv.params_conv ~1 (fn ctxt =>
(Conv.prems_conv ~1 (add_conv ctxt) then_conv
- Conv.concl_conv ~1 (add_conv ctxt))) ctxt) i)*}
+ Conv.concl_conv ~1 (add_conv ctxt))) ctxt)*}
text {*
A test case for this conversion is as follows
*}
-lemma "P (Suc (99 + 1)) ((0 + 0)::nat) (Suc (3 + 3 + 3)) (4 + 1)"
+lemma "P (Suc (99 + 1)) ((0 + 0)::nat) (Suc (3 + 3 + 3)) ((4 + 1)::nat)"
apply(tactic {* add_tac @{context} 1 *})?
txt {*
where it produces the goal state
--- a/ProgTutorial/Tactical.thy Wed Nov 25 21:00:31 2009 +0100
+++ b/ProgTutorial/Tactical.thy Tue Dec 01 12:25:34 2009 +0100
@@ -2077,10 +2077,10 @@
text {*
Conversions are a thin layer on top of Isabelle's inference kernel, and
can be viewed as a controllable, bare-bone version of Isabelle's simplifier.
- 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.
+ One difference between a conversion and the simplifier is that the former
+ acts 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
+ to theorems and used as tactics. The type for conversions is
*}
ML{*type conv = cterm -> thm*}
@@ -2118,7 +2118,7 @@
If you run this example, you will notice that the actual response is the
seemingly nonsensical @{term
"2 + 10 \<equiv> 2 + (10::nat)"}. The reason is that the pretty-printer for
- @{ML_type cterm}s eta-normalises terms and therefore produces this output.
+ @{ML_type cterm}s eta-normalises (sic) terms and therefore produces this output.
If we get hold of the ``raw'' representation of the produced theorem,
we obtain the expected result.
@@ -2204,10 +2204,8 @@
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, however, because the combinator @{ML else_conv in Conv} will then
- try out @{ML all_conv in Conv}, which always succeeds.
-
- The conversion combinator @{ML_ind try_conv in Conv} constructs a conversion
- which is tried out on a term, but in case of failure just does nothing.
+ try out @{ML all_conv in Conv}, which always succeeds. The same
+ behaviour can also be achieved with conversion combinator @{ML_ind try_conv in Conv}.
For example
@{ML_response_fake [display,gray]
@@ -2219,6 +2217,10 @@
end"
"True \<or> P \<equiv> True \<or> P"}
+ Rewriting with more than one theorem can be done using the function
+ @{ML_ind rewrs_conv in More_Conv} from the structure @{ML_struct More_Conv}.
+
+
Apart from the function @{ML beta_conversion in Thm}, which is able to fully
beta-normalise a term, the conversions so far are restricted in that they
only apply to the outer-most level of a @{ML_type cterm}. In what follows we
@@ -2269,13 +2271,13 @@
in all possible positions.
*}
-ML %linenosgray{*fun all_true1_conv ctxt ctrm =
+ML %linenosgray{*fun true_conj1_conv ctxt ctrm =
case (Thm.term_of ctrm) of
@{term "op \<and>"} $ @{term True} $ _ =>
- (Conv.arg_conv (all_true1_conv ctxt) then_conv
+ (Conv.arg_conv (true_conj1_conv ctxt) then_conv
Conv.rewr_conv @{thm true_conj1}) ctrm
- | _ $ _ => Conv.comb_conv (all_true1_conv ctxt) ctrm
- | Abs _ => Conv.abs_conv (fn (_, ctxt) => all_true1_conv ctxt) ctxt ctrm
+ | _ $ _ => Conv.comb_conv (true_conj1_conv ctxt) ctrm
+ | Abs _ => Conv.abs_conv (fn (_, ctxt) => true_conj1_conv ctxt) ctxt ctrm
| _ => Conv.all_conv ctrm*}
text {*
@@ -2288,12 +2290,57 @@
@{ML_response_fake [display,gray]
"let
- val conv = all_true1_conv @{context}
- val ctrm = @{cterm \"distinct [1, x] \<longrightarrow> True \<and> 1 \<noteq> x\"}
+ val conv = true_conj1_conv @{context}
+ val ctrm = @{cterm \"distinct [1::nat, x] \<longrightarrow> True \<and> 1 \<noteq> x\"}
in
conv ctrm
end"
"distinct [1, x] \<longrightarrow> True \<and> 1 \<noteq> x \<equiv> distinct [1, x] \<longrightarrow> 1 \<noteq> x"}
+*}
+
+text {*
+ Conversions that traverse terms, like @{ML true_conj1_conv} above, can be
+ implemented more succinctly with the combinators @{ML_ind bottom_conv in
+ More_Conv} and @{ML_ind top_conv in More_Conv}. For example:
+*}
+
+ML{*fun true_conj1_conv ctxt =
+let
+ val conv = Conv.try_conv (Conv.rewr_conv @{thm true_conj1})
+in
+ More_Conv.bottom_conv (K conv) ctxt
+end*}
+
+text {*
+ The function @{ML bottom_conv in More_Conv} traverses first the the term and
+ on the ``way down'' applies the conversion, whereas @{ML top_conv in
+ More_Conv} applies the on the ``way up''. To see the difference,
+ assume the following two meta-equations.
+*}
+
+lemma conj_assoc:
+ fixes A B C::bool
+ shows "A \<and> (B \<and> C) \<equiv> (A \<and> B) \<and> C"
+ and "(A \<and> B) \<and> C \<equiv> A \<and> (B \<and> C)"
+by simp_all
+
+text {*
+ and the @{ML_type cterm} @{text "(a \<and> (b \<and> c)) \<and> d"}. The reader should
+ pause for a moment to be convinced that rewriting top-down and bottom-up
+ according to the lemma produces two results.
+
+ @{ML_response_fake [display, gray]
+ "let
+ val ctxt = @{context}
+ val conv = Conv.try_conv (More_Conv.rewrs_conv @{thms conj_assoc})
+ val conv_top = More_Conv.top_conv (K conv) ctxt
+ val conv_bot = More_Conv.bottom_conv (K conv) ctxt
+ val ctrm = @{cterm \"(a \<and> (b \<and> c)) \<and> d\"}
+in
+ (conv_top ctrm, conv_bot ctrm)
+end"
+ "(\"(a \<and> (b \<and> c)) \<and> d \<equiv> a \<and> (b \<and> (c \<and> d))\",
+ \"(a \<and> (b \<and> c)) \<and> d \<equiv> (a \<and> b) \<and> (c \<and> d)\")"}
To see how much control you have about rewriting by using conversions, let us
make the task a bit more complicated by rewriting according to the rule
@@ -2301,24 +2348,31 @@
the conversion should be as follows.
*}
-ML{*fun if_true1_conv ctxt ctrm =
+ML{*fun if_true1_simple_conv ctxt ctrm =
case Thm.term_of ctrm of
Const (@{const_name If}, _) $ _ =>
- Conv.arg_conv (all_true1_conv ctxt) ctrm
- | _ $ _ => Conv.comb_conv (if_true1_conv ctxt) ctrm
- | Abs _ => Conv.abs_conv (fn (_, ctxt) => if_true1_conv ctxt) ctxt ctrm
- | _ => Conv.all_conv ctrm *}
+ Conv.arg_conv (true_conj1_conv ctxt) ctrm
+ | _ => Conv.no_conv ctrm
+
+val if_true1_conv = More_Conv.top_sweep_conv if_true1_simple_conv*}
text {*
- Here is an example for this conversion:
+ In the first function we only treat the top-most redex and also only the
+ success case and otherwise return @{ML no_conv in Conv}. To apply this
+ conversion inside a term, we use in the last line the combinator @{ML_ind
+ top_sweep_conv in More_Conv}, which traverses the term starting from the
+ root and applies it to all the redexes on the way, but stops in a branch as
+ soon as it found one redex.\footnote{\bf Fixme: Check with Sascha whether
+ the conversion stops after a single success case, or stops in each branch
+ after a success case.} Here is an example for this conversion:
+
@{ML_response_fake [display,gray]
"let
- val conv = if_true1_conv @{context}
- val ctrm =
- @{cterm \"if P (True \<and> 1 \<noteq> 2) then True \<and> True else True \<and> False\"}
+ val ctrm = @{cterm \"if P (True \<and> 1 \<noteq> (2::nat))
+ then True \<and> True else True \<and> False\"}
in
- conv ctrm
+ if_true1_conv @{context} 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"}
@@ -2327,19 +2381,19 @@
text {*
So far we only applied conversions to @{ML_type cterm}s. Conversions can, however,
also work on theorems using the function @{ML_ind fconv_rule in Conv}. As an example,
- consider the conversion @{ML all_true1_conv} and the lemma:
+ consider the conversion @{ML true_conj1_conv} and the lemma:
*}
lemma foo_test:
shows "P \<or> (True \<and> \<not>P)" by simp
text {*
- Using the conversion @{ML all_true1_conv} you can transform this theorem into a
+ Using the conversion @{ML true_conj1_conv} you can transform this theorem into a
new theorem as follows
@{ML_response_fake [display,gray]
"let
- val conv = Conv.fconv_rule (all_true1_conv @{context})
+ val conv = Conv.fconv_rule (true_conj1_conv @{context})
val thm = @{thm foo_test}
in
conv thm
@@ -2363,7 +2417,7 @@
conclusion of a goal.
\end{itemize}
- Assume we want to apply @{ML all_true1_conv} only in the conclusion
+ Assume we want to apply @{ML true_conj1_conv} only in the conclusion
of the goal, and @{ML if_true1_conv} should only apply to the premises.
Here is a tactic doing exactly that:
*}
@@ -2372,7 +2426,7 @@
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)*}
+ Conv.concl_conv ~1 (true_conj1_conv ctxt))) ctxt)*}
text {*
We call the conversions with the argument @{ML "~1"}. This is to
@@ -2394,7 +2448,7 @@
text {*
As you can see, the premises are rewritten according to @{ML if_true1_conv}, while
- the conclusion according to @{ML all_true1_conv}.
+ the conclusion according to @{ML true_conj1_conv}.
Conversions can also be helpful for constructing meta-equality theorems.
Such theorems are often definitions. As an example consider the following
Binary file progtutorial.pdf has changed