
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




