--- a/ProgTutorial/Tactical.thy Fri Mar 01 00:49:15 2013 +0000
+++ b/ProgTutorial/Tactical.thy Fri Apr 19 11:09:18 2013 +0100
@@ -407,7 +407,7 @@
lemma
shows "False" and "Goldbach_conjecture"
-apply(tactic {* Skip_Proof.cheat_tac @{theory} *})
+apply(tactic {* Skip_Proof.cheat_tac 1 *})
txt{*\begin{minipage}{\textwidth}
@{subgoals [display]}
\end{minipage}*}
@@ -1344,7 +1344,7 @@
lemma
shows "Suc (1 + 2) < 3 + 2"
-apply(tactic {* asm_full_simp_tac @{simpset} 1 *})
+apply(tactic {* asm_full_simp_tac @{context} 1 *})
done
text {*
@@ -1430,13 +1430,15 @@
let
val {simps, congs, procs, ...} = Raw_Simplifier.dest_ss ss
- fun name_thm (nm, thm) =
+ fun name_sthm (nm, thm) =
+ Pretty.enclose (nm ^ ": ") "" [pretty_thm_no_vars ctxt thm]
+ fun name_cthm ((_, nm), thm) =
Pretty.enclose (nm ^ ": ") "" [pretty_thm_no_vars ctxt thm]
fun name_ctrm (nm, ctrm) =
Pretty.enclose (nm ^ ": ") "" [pretty_cterms ctxt ctrm]
- val pps = [Pretty.big_list "Simplification rules:" (map name_thm simps),
- Pretty.big_list "Congruences rules:" (map name_thm congs),
+ val pps = [Pretty.big_list "Simplification rules:" (map name_sthm simps),
+ Pretty.big_list "Congruences rules:" (map name_cthm congs),
Pretty.big_list "Simproc patterns:" (map name_ctrm procs)]
in
pps |> Pretty.chunks
@@ -1467,13 +1469,13 @@
the simplification rule @{thm [source] Diff_Int} as follows:
*}
-ML %grayML{*val ss1 = empty_ss addsimps [@{thm Diff_Int} RS @{thm eq_reflection}] *}
+ML %grayML{*val ss1 = put_simpset empty_ss @{context} addsimps [@{thm Diff_Int} RS @{thm eq_reflection}] *}
text {*
Printing then out the components of the simpset gives:
@{ML_response_fake [display,gray]
- "print_ss @{context} ss1"
+ "print_ss @{context} (Raw_Simplifier.simpset_of ss1)"
"Simplification rules:
??.unknown: A - B \<inter> C \<equiv> A - B \<union> (A - C)
Congruences rules:
@@ -1484,13 +1486,13 @@
Adding also the congruence rule @{thm [source] UN_cong}
*}
-ML %grayML{*val ss2 = Simplifier.add_cong (@{thm UN_cong} RS @{thm eq_reflection}) ss1 *}
+ML %grayML{*val ss2 = ss1 |> Simplifier.add_cong (@{thm UN_cong} RS @{thm eq_reflection}) *}
text {*
gives
@{ML_response_fake [display,gray]
- "print_ss @{context} ss2"
+ "print_ss @{context} (Raw_Simplifier.simpset_of ss2)"
"Simplification rules:
??.unknown: A - B \<inter> C \<equiv> A - B \<union> (A - C)
Congruences rules:
@@ -1528,7 +1530,7 @@
and "t \<equiv> t"
and "False \<Longrightarrow> Foo"
and "\<lbrakk>A; B; C\<rbrakk> \<Longrightarrow> A"
-apply(tactic {* ALLGOALS (simp_tac HOL_basic_ss) *})
+apply(tactic {* ALLGOALS (simp_tac (put_simpset HOL_basic_ss @{context})) *})
done
text {*
@@ -1711,17 +1713,18 @@
the definition of the auxiliary constant.
*}
-ML %linenosgray{*val perm_simp_tac =
+ML %linenosgray{*fun perm_simp_tac ctxt =
let
val thms1 = [@{thm perm_aux_expand}]
val thms2 = [@{thm perm_append}, @{thm perm_bij}, @{thm perm_rev},
@{thm perm_compose_aux}] @ @{thms perm_prod.simps} @
@{thms perm_list.simps} @ @{thms perm_nat.simps}
val thms3 = [@{thm perm_aux_def}]
+ val ss = put_simpset HOL_basic_ss ctxt
in
- simp_tac (HOL_basic_ss addsimps thms1)
- THEN' simp_tac (HOL_basic_ss addsimps thms2)
- THEN' simp_tac (HOL_basic_ss addsimps thms3)
+ simp_tac (ss addsimps thms1)
+ THEN' simp_tac (ss addsimps thms2)
+ THEN' simp_tac (ss addsimps thms3)
end*}
text {*
@@ -1733,7 +1736,7 @@
lemma
fixes c d::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
shows "pi\<^isub>1\<bullet>(c, pi\<^isub>2\<bullet>((rev pi\<^isub>1)\<bullet>d)) = (pi\<^isub>1\<bullet>c, (pi\<^isub>1\<bullet>pi\<^isub>2)\<bullet>d)"
-apply(tactic {* perm_simp_tac 1 *})
+apply(tactic {* perm_simp_tac @{context} 1 *})
done
@@ -1749,8 +1752,6 @@
(FIXME: What are the second components of the congruence rules---something to
do with weak congruence constants?)
- (FIXME: Anything interesting to say about @{ML Simplifier.clear_ss}?)
-
(FIXME: what are @{ML mksimps_pairs}; used in Nominal.thy)
(FIXME: explain @{ML simplify} and @{ML "Simplifier.rewrite_rule"} etc.)
@@ -1771,9 +1772,8 @@
you can use the function:
*}
-ML %linenosgray{*fun fail_simproc simpset redex =
+ML %linenosgray{*fun fail_simproc ctxt redex =
let
- val ctxt = Simplifier.the_context simpset
val _ = pwriteln (Pretty.block
[Pretty.str "The redex: ", pretty_cterm ctxt redex])
in
@@ -1830,7 +1830,8 @@
lemma
shows "Suc 0 = 1"
-apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [@{simproc fail}]) 1*})
+apply(tactic {* simp_tac (put_simpset
+ HOL_basic_ss @{context} addsimprocs [@{simproc fail}]) 1*})
(*<*)oops(*>*)
text {*
@@ -1844,9 +1845,8 @@
to
*}
-ML %grayML{*fun fail_simproc' simpset redex =
+ML %grayML{*fun fail_simproc' ctxt redex =
let
- val ctxt = Simplifier.the_context simpset
val _ = pwriteln (Pretty.block
[Pretty.str "The redex:", pretty_term ctxt redex])
in
@@ -1861,12 +1861,12 @@
*}
-ML %grayML{*val fail' =
+ML %grayML{*fun fail' ctxt =
let
val thy = @{theory}
val pat = [@{term "Suc n"}]
in
- Simplifier.simproc_global_i thy "fail_simproc'" pat (K fail_simproc')
+ Simplifier.simproc_global_i thy "fail_simproc'" pat (K fail_simproc' ctxt)
end*}
text {*
@@ -1882,7 +1882,7 @@
lemma
shows "Suc (Suc 0) = (Suc 1)"
-apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [fail']) 1*})
+apply(tactic {* simp_tac ((put_simpset HOL_basic_ss @{context}) addsimprocs [fail' @{context}]) 1*})
(*<*)oops(*>*)
text {*
@@ -1909,7 +1909,7 @@
*}
-ML %grayML{*fun plus_one_simproc ss redex =
+ML %grayML{*fun plus_one_simproc ctxt redex =
case redex of
@{term "Suc 0"} => NONE
| _ => SOME @{thm plus_one}*}
@@ -1918,12 +1918,12 @@
and set up the simproc as follows.
*}
-ML %grayML{*val plus_one =
+ML %grayML{*fun plus_one ctxt =
let
val thy = @{theory}
val pat = [@{term "Suc n"}]
in
- Simplifier.simproc_global_i thy "sproc +1" pat (K plus_one_simproc)
+ Simplifier.simproc_global_i thy "sproc +1" pat (K plus_one_simproc ctxt)
end*}
text {*
@@ -1935,7 +1935,7 @@
lemma
shows "P (Suc (Suc (Suc 0))) (Suc 0)"
-apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [plus_one]) 1*})
+apply(tactic {* simp_tac (put_simpset HOL_basic_ss @{context} addsimprocs [plus_one @{context}]) 1*})
txt{*
where the simproc produces the goal state
\begin{isabelle}
@@ -1990,7 +1990,7 @@
let
val num = HOLogic.mk_number @{typ "nat"} n
val goal = Logic.mk_equals (t, num)
- val num_ss = HOL_ss addsimps @{thms semiring_norm}
+ val num_ss = put_simpset HOL_ss ctxt addsimps @{thms semiring_norm}
in
Goal.prove ctxt [] [] goal (K (simp_tac num_ss 1))
end*}
@@ -2010,13 +2010,9 @@
theorem for the simproc.
*}
-ML %grayML{*fun nat_number_simproc ss t =
-let
- val ctxt = Simplifier.the_context ss
-in
+ML %grayML{*fun nat_number_simproc ctxt t =
SOME (get_thm_alt ctxt (t, dest_suc_trm t))
- handle TERM _ => NONE
-end*}
+ handle TERM _ => NONE *}
text {*
This function uses the fact that @{ML dest_suc_trm} might raise an exception
@@ -2025,12 +2021,12 @@
on an example, you can set it up as follows:
*}
-ML %grayML{*val nat_number =
+ML %grayML{*fun nat_number ctxt =
let
val thy = @{theory}
val pat = [@{term "Suc n"}]
in
- Simplifier.simproc_global_i thy "nat_number" pat (K nat_number_simproc)
+ Simplifier.simproc_global_i thy "nat_number" pat (K nat_number_simproc ctxt)
end*}
text {*
@@ -2039,7 +2035,7 @@
lemma
shows "P (Suc (Suc 2)) (Suc 99) (0::nat) (Suc 4 + Suc 0) (Suc (0 + 0))"
-apply(tactic {* simp_tac (HOL_ss addsimprocs [nat_number]) 1*})
+apply(tactic {* simp_tac (put_simpset HOL_ss @{context} addsimprocs [nat_number @{context}]) 1*})
txt {*
you obtain the more legible goal state
\begin{isabelle}