--- 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