# HG changeset patch # User Christian Urban # Date 1259666734 -3600 # Node ID f8d020bbc2c0749ca0ade5646e163654c59c8f8f # Parent 3d27d77c351f3c2bd5685965382434ebc68d3b24 improved section on conversions diff -r 3d27d77c351f -r f8d020bbc2c0 ProgTutorial/Essential.thy --- 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 \ P"}. + to prove the term @{term "P \ P"}.\footnote{\bf FIXME: What about @{ML_ind prove_internal in Goal}?} @{ML_response_fake [display,gray] "let diff -r 3d27d77c351f -r f8d020bbc2c0 ProgTutorial/Solutions.thy --- 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 \ nat \ 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 \ nat \ 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 diff -r 3d27d77c351f -r f8d020bbc2c0 ProgTutorial/Tactical.thy --- 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 \ 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 \ P \ True \ 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 \"} $ @{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] \ True \ 1 \ x\"} + val conv = true_conj1_conv @{context} + val ctrm = @{cterm \"distinct [1::nat, x] \ True \ 1 \ x\"} in conv ctrm end" "distinct [1, x] \ True \ 1 \ x \ distinct [1, x] \ 1 \ 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 \ (B \ C) \ (A \ B) \ C" + and "(A \ B) \ C \ A \ (B \ C)" +by simp_all + +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. + + @{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 \ (b \ c)) \ d\"} +in + (conv_top ctrm, conv_bot ctrm) +end" + "(\"(a \ (b \ c)) \ d \ a \ (b \ (c \ d))\", + \"(a \ (b \ c)) \ d \ (a \ b) \ (c \ 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 \ 1 \ 2) then True \ True else True \ False\"} + val ctrm = @{cterm \"if P (True \ 1 \ (2::nat)) + then True \ True else True \ False\"} in - conv ctrm + if_true1_conv @{context} ctrm end" "if P (True \ 1 \ 2) then True \ True else True \ False \ if P (1 \ 2) then True \ True else True \ 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 \ (True \ \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 diff -r 3d27d77c351f -r f8d020bbc2c0 progtutorial.pdf Binary file progtutorial.pdf has changed