--- a/ProgTutorial/Tactical.thy Tue Dec 01 12:25:34 2009 +0100
+++ b/ProgTutorial/Tactical.thy Wed Dec 02 02:34:09 2009 +0100
@@ -2075,12 +2075,11 @@
section {* Conversions\label{sec:conversion} *}
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 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 and used as tactics. The type for conversions is
+ 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.
+ The purpose of conversions is to manipulate on @{ML_type cterm}s. However,
+ we will also show in this section how conversions can be applied to theorems
+ and used as tactics. The type of conversions is
*}
ML{*type conv = cterm -> thm*}
@@ -2201,7 +2200,7 @@
end"
"(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
+ Here the conversion @{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 same
@@ -2281,9 +2280,9 @@
| _ => Conv.all_conv ctrm*}
text {*
- This function ``fires'' if the terms is of the form @{text "(True \<and> \<dots>)"}.
- It descends under applications (Line 6 and 7) and abstractions
- (Line 8); otherwise it leaves the term unchanged (Line 9). In Line 2
+ This function ``fires'' if the term is of the form @{text "(True \<and> \<dots>)"}.
+ It descends under applications (Line 6) and abstractions
+ (Line 7); otherwise it leaves the term unchanged (Line 8). In Line 2
we need to transform the @{ML_type cterm} into a @{ML_type term} in order
to be able to pattern-match the term. To see this
conversion in action, consider the following example:
@@ -2314,7 +2313,7 @@
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,
+ More_Conv} applies the conversion on the ``way up''. To see the difference,
assume the following two meta-equations.
*}
@@ -2327,7 +2326,7 @@
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.
+ according to the two meta-equations produces two results.
@{ML_response_fake [display, gray]
"let
@@ -2361,10 +2360,8 @@
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:
+ root and applies it to all the redexes on the way, but stops in each branch as
+ soon as it found one redex. Here is an example for this conversion:
@{ML_response_fake [display,gray]
@@ -2429,11 +2426,13 @@
Conv.concl_conv ~1 (true_conj1_conv ctxt))) ctxt)*}
text {*
- We call the conversions with the argument @{ML "~1"}. This is to
- analyse all parameters, premises and conclusions. If we call them 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
+ We call the conversions with the argument @{ML "~1"}. By this we
+ analyse all parameters, all premises and the conclusion of a goal
+ state. If we call @{ML concl_conv in Conv} with
+ a non-negative number, say @{text n}, then this conversions will
+ skip the first @{text n} premises and applies the conversion to the
+ ``rest'' (similar for parameters and conclusions). To test the
+ tactic, consider the proof
*}
lemma
@@ -2473,8 +2472,8 @@
"Drule.abs_def @{thm id1_def}"
"id1 \<equiv> \<lambda>x. x"}
- Unfortunately, Isabelle has no build-in function that transforms the
- theorems in the other direction. We can conveniently implement one using
+ Unfortunately, Isabelle has no built-in function that transforms the
+ theorems in the other direction. We can implement one using
conversions. The feature of conversions we are using is that if we apply a
@{ML_type cterm} to a conversion we obtain a meta-equality theorem (recall
that the type of conversions is an abbreviation for
@@ -2505,7 +2504,7 @@
abstraction. We compute the possibly empty list of abstracted variables in
Line 4 using the function @{ML_ind strip_abs_vars in Term}. For this we have to
transform the @{ML_type cterm} into a @{ML_type term}. In Line 5 we
- importing these variables into the context @{ML_text ctxt'}, in order to
+ import these variables into the context @{text "ctxt'"}, in order to
export them again in Line 15. In Line 8 we certify the list of variables,
which in turn we apply to the @{ML_text lhs} of the definition using the
function @{ML_ind list_comb in Drule}. In Line 11 and 12 we generate the
@@ -2515,8 +2514,8 @@
conversion with @{ML_ind fun_conv in Conv}. Now in Line 14 we only have to
apply the new left-hand side to the generated conversion and obtain the the
theorem we want to construct. As mentioned above, in Line 15 we only have to
- export the context @{ML_text ctxt'} in order to produce meta-variables for
- the theorem. An example is as follows.
+ export the context @{text "ctxt'"} back to @{text "ctxt"} in order to
+ produce meta-variables for the theorem. An example is as follows.
@{ML_response_fake [display, gray]
"unabs_def @{context} @{thm id2_def}"
@@ -2527,7 +2526,7 @@
To sum up this section, conversions are more general than the simplifier
or simprocs, but you have to do more work yourself. Also conversions are
often much less efficient than the simplifier. The advantage of conversions,
- however, that they provide much less room for non-termination.
+ however, is that they provide much less room for non-termination.
\begin{exercise}\label{ex:addconversion}
Write a tactic that does the same as the simproc in exercise