diff -r fb6c29a90003 -r d8c376662bb4 ProgTutorial/Tactical.thy --- a/ProgTutorial/Tactical.thy Mon Apr 30 12:36:32 2012 +0100 +++ b/ProgTutorial/Tactical.thy Mon Apr 30 14:43:52 2012 +0100 @@ -2,14 +2,6 @@ imports Base First_Steps begin -(*<*) -setup{* -open_file_with_prelude - "Tactical_Code.thy" - ["theory Tactical", "imports Base First_Steps", "begin"] -*} -(*>*) - chapter {* Tactical Reasoning\label{chp:tactical} *} text {* @@ -104,7 +96,7 @@ *} -ML{*val foo_tac = +ML %grayML{*val foo_tac = (etac @{thm disjE} 1 THEN rtac @{thm disjI2} 1 THEN atac 1 @@ -133,7 +125,7 @@ you can write *} -ML{*val foo_tac' = +ML %grayML{*val foo_tac' = (etac @{thm disjE} THEN' rtac @{thm disjI2} THEN' atac @@ -177,7 +169,7 @@ states. Hence the type of a tactic is: *} -ML{*type tactic = thm -> thm Seq.seq*} +ML %grayML{*type tactic = thm -> thm Seq.seq*} text {* By convention, if a tactic fails, then it should return the empty sequence. @@ -190,14 +182,14 @@ is defined as *} -ML{*fun no_tac thm = Seq.empty*} +ML %grayML{*fun no_tac thm = Seq.empty*} text {* which means @{ML no_tac} always fails. The second returns the given theorem wrapped in a single member sequence; it is defined as *} -ML{*fun all_tac thm = Seq.single thm*} +ML %grayML{*fun all_tac thm = Seq.single thm*} text {* which means @{ML all_tac} always succeeds, but also does not make any progress @@ -237,7 +229,7 @@ tactic *} -ML{*fun my_print_tac ctxt thm = +ML %grayML{*fun my_print_tac ctxt thm = let val _ = tracing (Pretty.string_of (pretty_thm_no_vars ctxt thm)) in @@ -473,7 +465,7 @@ explored via the lazy sequences mechanism). Given the code *} -ML{*val resolve_xmp_tac = resolve_tac [@{thm impI}, @{thm conjI}]*} +ML %grayML{*val resolve_xmp_tac = resolve_tac [@{thm impI}, @{thm conjI}]*} text {* an example for @{ML resolve_tac} is the following proof where first an outermost @@ -529,7 +521,7 @@ \begin{isabelle} *} -ML{*fun foc_tac {prems, params, asms, concl, context, schematics} = +ML %grayML{*fun foc_tac {prems, params, asms, concl, context, schematics} = let fun assgn1 f1 f2 xs = Pretty.list "" "" (map (fn (x, y) => Pretty.enum ":=" "" "" [f1 x, f2 y]) xs) @@ -620,7 +612,7 @@ for example easily implement a tactic that behaves almost like @{ML atac}: *} -ML{*val atac' = Subgoal.FOCUS (fn {prems, ...} => resolve_tac prems 1)*} +ML %grayML{*val atac' = Subgoal.FOCUS (fn {prems, ...} => resolve_tac prems 1)*} text {* If you apply @{ML atac'} to the next lemma @@ -982,7 +974,7 @@ page~\pageref{tac:footacprime} can also be written as: *} -ML{*val foo_tac'' = EVERY' [etac @{thm disjE}, rtac @{thm disjI2}, +ML %grayML{*val foo_tac'' = EVERY' [etac @{thm disjE}, rtac @{thm disjI2}, atac, rtac @{thm disjI1}, atac]*} text {* @@ -993,7 +985,7 @@ you can also just write *} -ML{*val foo_tac1 = EVERY1 [etac @{thm disjE}, rtac @{thm disjI2}, +ML %grayML{*val foo_tac1 = EVERY1 [etac @{thm disjE}, rtac @{thm disjI2}, atac, rtac @{thm disjI1}, atac]*} text {* @@ -1007,7 +999,7 @@ *} -ML{*val orelse_xmp_tac = rtac @{thm disjI1} ORELSE' rtac @{thm conjI}*} +ML %grayML{*val orelse_xmp_tac = rtac @{thm disjI1} ORELSE' rtac @{thm conjI}*} text {* will first try out whether theorem @{text disjI} applies and in case of failure @@ -1031,7 +1023,7 @@ as follows: *} -ML{*val select_tac' = FIRST' [rtac @{thm conjI}, rtac @{thm impI}, +ML %grayML{*val select_tac' = FIRST' [rtac @{thm conjI}, rtac @{thm impI}, rtac @{thm notI}, rtac @{thm allI}, K all_tac]*}text_raw{*\label{tac:selectprime}*} text {* @@ -1074,7 +1066,7 @@ For example: *} -ML{*val select_tac'' = TRY o FIRST' [rtac @{thm conjI}, rtac @{thm impI}, +ML %grayML{*val select_tac'' = TRY o FIRST' [rtac @{thm conjI}, rtac @{thm impI}, rtac @{thm notI}, rtac @{thm allI}]*} text_raw{*\label{tac:selectprimeprime}*} @@ -1127,7 +1119,7 @@ suppose the following tactic *} -ML{*val repeat_xmp_tac = REPEAT (CHANGED (select_tac' 1)) *} +ML %grayML{*val repeat_xmp_tac = REPEAT (CHANGED (select_tac' 1)) *} text {* which applied to the proof *} @@ -1151,7 +1143,7 @@ can implement it as *} -ML{*val repeat_xmp_tac' = REPEAT o CHANGED o select_tac'*} +ML %grayML{*val repeat_xmp_tac' = REPEAT o CHANGED o select_tac'*} text {* since there are no ``primed'' versions of @{ML REPEAT} and @{ML CHANGED}. @@ -1164,7 +1156,7 @@ Supposing the tactic *} -ML{*val repeat_all_new_xmp_tac = REPEAT_ALL_NEW (CHANGED o select_tac')*} +ML %grayML{*val repeat_all_new_xmp_tac = REPEAT_ALL_NEW (CHANGED o select_tac')*} text {* you can see that the following goal @@ -1430,7 +1422,7 @@ \begin{figure}[t] \begin{minipage}{\textwidth} \begin{isabelle}*} -ML{*fun print_ss ctxt ss = +ML %grayML{*fun print_ss ctxt ss = let val {simps, congs, procs, ...} = Raw_Simplifier.dest_ss ss @@ -1471,7 +1463,7 @@ the simplification rule @{thm [source] Diff_Int} as follows: *} -ML{*val ss1 = empty_ss addsimps [@{thm Diff_Int} RS @{thm eq_reflection}] *} +ML %grayML{*val ss1 = empty_ss addsimps [@{thm Diff_Int} RS @{thm eq_reflection}] *} text {* Printing then out the components of the simpset gives: @@ -1488,7 +1480,7 @@ Adding also the congruence rule @{thm [source] UN_cong} *} -ML{*val ss2 = Simplifier.add_cong (@{thm UN_cong} RS @{thm eq_reflection}) ss1 *} +ML %grayML{*val ss2 = Simplifier.add_cong (@{thm UN_cong} RS @{thm eq_reflection}) ss1 *} text {* gives @@ -1847,7 +1839,7 @@ to *} -ML{*fun fail_simproc' simpset redex = +ML %grayML{*fun fail_simproc' simpset redex = let val ctxt = Simplifier.the_context simpset val _ = pwriteln (Pretty.block [Pretty.str "The redex:", pretty_term ctxt redex]) @@ -1863,7 +1855,7 @@ *} -ML{*val fail' = +ML %grayML{*val fail' = let val thy = @{theory} val pat = [@{term "Suc n"}] @@ -1911,7 +1903,7 @@ *} -ML{*fun plus_one_simproc ss redex = +ML %grayML{*fun plus_one_simproc ss redex = case redex of @{term "Suc 0"} => NONE | _ => SOME @{thm plus_one}*} @@ -1920,7 +1912,7 @@ and set up the simproc as follows. *} -ML{*val plus_one = +ML %grayML{*val plus_one = let val thy = @{theory} val pat = [@{term "Suc n"}] @@ -1958,7 +1950,7 @@ takes a term and produces the corresponding integer value. *} -ML{*fun dest_suc_trm ((Const (@{const_name "Suc"}, _)) $ t) = 1 + dest_suc_trm t +ML %grayML{*fun dest_suc_trm ((Const (@{const_name "Suc"}, _)) $ t) = 1 + dest_suc_trm t | dest_suc_trm t = snd (HOLogic.dest_number t)*} text {* @@ -1988,7 +1980,7 @@ want to prove here, the simpset @{text "num_ss"} should suffice. *} -ML{*fun get_thm_alt ctxt (t, n) = +ML %grayML{*fun get_thm_alt ctxt (t, n) = let val num = HOLogic.mk_number @{typ "nat"} n val goal = Logic.mk_equals (t, num) @@ -2012,7 +2004,7 @@ theorem for the simproc. *} -ML{*fun nat_number_simproc ss t = +ML %grayML{*fun nat_number_simproc ss t = let val ctxt = Simplifier.the_context ss in @@ -2027,7 +2019,7 @@ on an example, you can set it up as follows: *} -ML{*val nat_number = +ML %grayML{*val nat_number = let val thy = @{theory} val pat = [@{term "Suc n"}] @@ -2074,7 +2066,7 @@ and to goal states. The type of conversions is *} -ML{*type conv = cterm -> thm*} +ML %grayML{*type conv = cterm -> thm*} text {* whereby the produced theorem is always a meta-equality. A simple conversion @@ -2312,7 +2304,7 @@ Conv} and @{ML_ind top_conv in Conv}. For example: *} -ML{*fun true_conj1_conv ctxt = +ML %grayML{*fun true_conj1_conv ctxt = let val conv = Conv.try_conv (Conv.rewr_conv @{thm true_conj1}) in @@ -2358,7 +2350,7 @@ the conversion should be as follows. *} -ML{*fun if_true1_simple_conv ctxt ctrm = +ML %grayML{*fun if_true1_simple_conv ctxt ctrm = case Thm.term_of ctrm of Const (@{const_name If}, _) $ _ => Conv.arg_conv (true_conj1_conv ctxt) ctrm @@ -2430,7 +2422,7 @@ Here is a tactic doing exactly that: *} -ML{*fun true1_tac ctxt = +ML %grayML{*fun true1_tac ctxt = CONVERSION (Conv.params_conv ~1 (fn ctxt => (Conv.prems_conv ~1 (if_true1_conv ctxt) then_conv