# HG changeset patch # User Christian Urban # Date 1259717649 -3600 # Node ID f399b6855546af4368785032b0f3f40f2e23070f # Parent f8d020bbc2c0749ca0ade5646e163654c59c8f8f implemented suggestion from Sascha diff -r f8d020bbc2c0 -r f399b6855546 ProgTutorial/Tactical.thy --- 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 \ Q \ Q, P \ True \ Q \ P \ True \ 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 \ \)"}. - 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 \ \)"}. + 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 \ (b \ c)) \ 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 \ \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 diff -r f8d020bbc2c0 -r f399b6855546 progtutorial.pdf Binary file progtutorial.pdf has changed