isabelle-cookbook: comparison ProgTutorial/Tactical.thy

equal deleted inserted replaced

-:f8d020bbc2c0
+:f399b6855546
 *}
 section {* Conversions\label{sec:conversion} *}
 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
-can be viewed as a controllable, bare-bone version of Isabelle's simplifier.
+be viewed as a controllable, bare-bone version of Isabelle's simplifier.
-One difference between a conversion and the simplifier is that the former
+The purpose of conversions is to manipulate on @{ML_type cterm}s. However,
-acts on @{ML_type cterm}s while the latter acts on @{ML_type thm}s.
+we will also show in this section how conversions can be applied to theorems
-However, we will also show in this section how conversions can be applied
+and used as tactics. The type of conversions is
-to theorems and used as tactics. The type for conversions is
 *}
 ML{*type conv = cterm -> thm*}
 text {*
 in
 (conv ctrm1, conv ctrm2)
 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
 behaviour can also be achieved with conversion combinator @{ML_ind try_conv in Conv}.
 For example
 | _ $ _ => 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 {*
-This function ``fires'' if the terms is of the form @{text "(True \<and> \<dots>)"}.
+This function ``fires'' if the term is of the form @{text "(True \<and> \<dots>)"}.
-It descends under applications (Line 6 and 7) and abstractions
+It descends under applications (Line 6) and abstractions
-(Line 8); otherwise it leaves the term unchanged (Line 9). In Line 2
+(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:
 @{ML_response_fake [display,gray]
 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,
+More_Conv} applies the conversion on the ``way up''. To see the difference,
 assume the following two meta-equations.
 *}
 lemma conj_assoc:
 fixes A B C::bool
 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.
+according to the two meta-equations produces two results.
 @{ML_response_fake [display, gray]
 "let
 val ctxt = @{context}
 val conv = Conv.try_conv (More_Conv.rewrs_conv @{thms conj_assoc})
 text {*
 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
+root and applies it to all the redexes on the way, but stops in each branch as
-soon as it found one redex.\footnote{\bf Fixme: Check with Sascha whether
+soon as it found one redex. Here is an example for this conversion:
-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 ctrm = @{cterm \"if P (True \<and> 1 \<noteq> (2::nat))
 (Conv.params_conv ~1 (fn ctxt =>
 (Conv.prems_conv ~1 (if_true1_conv ctxt) then_conv
 Conv.concl_conv ~1 (true_conj1_conv ctxt))) ctxt)*}
 text {*
-We call the conversions with the argument @{ML "~1"}. This is to
+We call the conversions with the argument @{ML "~1"}. By this we
-analyse all parameters, premises and conclusions. If we call them with
+analyse all parameters, all premises and the conclusion of a goal
-a non-negative number, say @{text n}, then these conversions will
+state. If we call @{ML concl_conv in Conv} with
-only be called on @{text n} premises (similar for parameters and
+a non-negative number, say @{text n}, then this conversions will
-conclusions). To test the tactic, consider the proof
+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
 "if True \<and> P then P else True \<and> False \<Longrightarrow>
 (if True \<and> Q then True \<and> Q else P) \<longrightarrow> True \<and> (True \<and> Q)"
 @{ML_response_fake [display,gray]
 "Drule.abs_def @{thm id1_def}"
 "id1 \<equiv> \<lambda>x. x"}
-Unfortunately, Isabelle has no build-in function that transforms the
+Unfortunately, Isabelle has no built-in function that transforms the
-theorems in the other direction. We can conveniently implement one using
+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
 @{ML_type "cterm -> thm"}). The code of the transformation is below.
 *}
 corresponding to the left-hand and right-hand side of the meta-equality. The
 assumption in @{ML unabs_def} is that the right-hand side is an
 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
 conversion according to the length of the list of (abstracted) variables. If
 there are none, then we just return the conversion corresponding to the
 original definition. If there are variables, then we have to prefix this
 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
+export the context @{text "ctxt'"} back to @{text "ctxt"} in order to
-the theorem.  An example is as follows.
+produce meta-variables for the theorem.  An example is as follows.
 @{ML_response_fake [display, gray]
 "unabs_def @{context} @{thm id2_def}"
 "id2 ?x1 \<equiv> ?x1"}
 *}
 text {*
 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
 \ref{ex:addsimproc}, but is based on conversions. You can make
 the same assumptions as in \ref{ex:addsimproc}.

changeset 406	f399b6855546
parent 405	f8d020bbc2c0
child 408	ef048892d0f0