renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
--- a/doc-src/TutorialI/Protocol/Message.thy Thu Jul 23 18:44:08 2009 +0200
+++ b/doc-src/TutorialI/Protocol/Message.thy Thu Jul 23 18:44:09 2009 +0200
@@ -915,15 +915,15 @@
lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD]
method_setup spy_analz = {*
- Scan.succeed (SIMPLE_METHOD' o spy_analz_tac o local_clasimpset_of) *}
+ Scan.succeed (SIMPLE_METHOD' o spy_analz_tac o clasimpset_of) *}
"for proving the Fake case when analz is involved"
method_setup atomic_spy_analz = {*
- Scan.succeed (SIMPLE_METHOD' o atomic_spy_analz_tac o local_clasimpset_of) *}
+ Scan.succeed (SIMPLE_METHOD' o atomic_spy_analz_tac o clasimpset_of) *}
"for debugging spy_analz"
method_setup Fake_insert_simp = {*
- Scan.succeed (SIMPLE_METHOD' o Fake_insert_simp_tac o local_simpset_of) *}
+ Scan.succeed (SIMPLE_METHOD' o Fake_insert_simp_tac o simpset_of) *}
"for debugging spy_analz"
--- a/doc-src/TutorialI/Protocol/Public.thy Thu Jul 23 18:44:08 2009 +0200
+++ b/doc-src/TutorialI/Protocol/Public.thy Thu Jul 23 18:44:09 2009 +0200
@@ -154,7 +154,7 @@
ML {*
fun possibility_tac ctxt =
REPEAT (*omit used_Says so that Nonces start from different traces!*)
- (ALLGOALS (simp_tac (local_simpset_of ctxt delsimps [used_Says]))
+ (ALLGOALS (simp_tac (simpset_of ctxt delsimps [used_Says]))
THEN
REPEAT_FIRST (eq_assume_tac ORELSE'
resolve_tac [refl, conjI, @{thm Nonce_supply}]));
--- a/src/CCL/CCL.thy Thu Jul 23 18:44:08 2009 +0200
+++ b/src/CCL/CCL.thy Thu Jul 23 18:44:09 2009 +0200
@@ -257,9 +257,9 @@
(mk_dstnct_rls @{theory} ["bot","true","false","pair","lambda"]) end
fun mk_dstnct_thms thy defs inj_rls xs =
- let fun mk_dstnct_thm rls s = prove_goalw thy defs s
- (fn _ => [simp_tac (simpset_of thy addsimps (rls@inj_rls)) 1])
- in map (mk_dstnct_thm ccl_dstncts) (mk_dstnct_rls thy xs) end
+ let fun mk_dstnct_thm rls s = prove_goalw thy defs s
+ (fn _ => [simp_tac (global_simpset_of thy addsimps (rls@inj_rls)) 1])
+ in map (mk_dstnct_thm ccl_dstncts) (mk_dstnct_rls thy xs) end
fun mkall_dstnct_thms thy defs i_rls xss = List.concat (map (mk_dstnct_thms thy defs i_rls) xss)
--- a/src/CCL/Type.thy Thu Jul 23 18:44:08 2009 +0200
+++ b/src/CCL/Type.thy Thu Jul 23 18:44:09 2009 +0200
@@ -132,10 +132,10 @@
fun mk_ncanT_tac ctxt defs top_crls crls s = prove_goalw (ProofContext.theory_of ctxt) defs s
(fn major::prems => [(resolve_tac ([major] RL top_crls) 1),
(REPEAT_SOME (eresolve_tac (crls @ [exE,bexE,conjE,disjE]))),
- (ALLGOALS (asm_simp_tac (local_simpset_of ctxt))),
+ (ALLGOALS (asm_simp_tac (simpset_of ctxt))),
(ALLGOALS (ares_tac (prems RL [lemma]) ORELSE'
etac bspec )),
- (safe_tac (local_claset_of ctxt addSIs prems))])
+ (safe_tac (claset_of ctxt addSIs prems))])
end
*}
@@ -408,7 +408,7 @@
fun mk_genIs thy defs genXH gen_mono s = prove_goalw thy defs s
(fn prems => [rtac (genXH RS iffD2) 1,
- simp_tac (simpset_of thy) 1,
+ simp_tac (global_simpset_of thy) 1,
TRY (fast_tac (@{claset} addIs
([genXH RS iffD2,gen_mono RS coinduct3_mono_lemma RS lfpI]
@ prems)) 1)])
@@ -442,7 +442,7 @@
"[| <h,h'> : lfp(%x. POgen(x) Un R Un PO); <t,t'> : lfp(%x. POgen(x) Un R Un PO) |] ==> <h$t,h'$t'> : POgen(lfp(%x. POgen(x) Un R Un PO))"];
fun POgen_tac ctxt (rla,rlb) i =
- SELECT_GOAL (safe_tac (local_claset_of ctxt)) i THEN
+ SELECT_GOAL (safe_tac (claset_of ctxt)) i THEN
rtac (rlb RS (rla RS @{thm ssubst_pair})) i THEN
(REPEAT (resolve_tac (POgenIs @ [@{thm PO_refl} RS (@{thm POgen_mono} RS ci3_AI)] @
(POgenIs RL [@{thm POgen_mono} RS ci3_AgenI]) @ [@{thm POgen_mono} RS ci3_RI]) i));
@@ -481,9 +481,9 @@
fun EQgen_tac ctxt rews i =
SELECT_GOAL
- (TRY (safe_tac (local_claset_of ctxt)) THEN
+ (TRY (safe_tac (claset_of ctxt)) THEN
resolve_tac ((rews@[refl]) RL ((rews@[refl]) RL [@{thm ssubst_pair}])) i THEN
- ALLGOALS (simp_tac (local_simpset_of ctxt)) THEN
+ ALLGOALS (simp_tac (simpset_of ctxt)) THEN
ALLGOALS EQgen_raw_tac) i
*}
--- a/src/FOL/cladata.ML Thu Jul 23 18:44:08 2009 +0200
+++ b/src/FOL/cladata.ML Thu Jul 23 18:44:09 2009 +0200
@@ -19,7 +19,7 @@
structure Cla = ClassicalFun(Classical_Data);
structure BasicClassical: BASIC_CLASSICAL = Cla; open BasicClassical;
-ML_Antiquote.value "claset" (Scan.succeed "Cla.local_claset_of (ML_Context.the_local_context ())");
+ML_Antiquote.value "claset" (Scan.succeed "Cla.claset_of (ML_Context.the_local_context ())");
(*Propositional rules*)
--- a/src/FOL/simpdata.ML Thu Jul 23 18:44:08 2009 +0200
+++ b/src/FOL/simpdata.ML Thu Jul 23 18:44:09 2009 +0200
@@ -164,6 +164,6 @@
open Clasimp;
ML_Antiquote.value "clasimpset"
- (Scan.succeed "Clasimp.local_clasimpset_of (ML_Context.the_local_context ())");
+ (Scan.succeed "Clasimp.clasimpset_of (ML_Context.the_local_context ())");
val FOL_css = (FOL_cs, FOL_ss);
--- a/src/HOL/Auth/Message.thy Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOL/Auth/Message.thy Thu Jul 23 18:44:09 2009 +0200
@@ -939,15 +939,15 @@
lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD]
method_setup spy_analz = {*
- Scan.succeed (SIMPLE_METHOD' o Message.spy_analz_tac o local_clasimpset_of) *}
+ Scan.succeed (SIMPLE_METHOD' o Message.spy_analz_tac o clasimpset_of) *}
"for proving the Fake case when analz is involved"
method_setup atomic_spy_analz = {*
- Scan.succeed (SIMPLE_METHOD' o Message.atomic_spy_analz_tac o local_clasimpset_of) *}
+ Scan.succeed (SIMPLE_METHOD' o Message.atomic_spy_analz_tac o clasimpset_of) *}
"for debugging spy_analz"
method_setup Fake_insert_simp = {*
- Scan.succeed (SIMPLE_METHOD' o Message.Fake_insert_simp_tac o local_simpset_of) *}
+ Scan.succeed (SIMPLE_METHOD' o Message.Fake_insert_simp_tac o simpset_of) *}
"for debugging spy_analz"
end
--- a/src/HOL/Auth/Public.thy Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOL/Auth/Public.thy Thu Jul 23 18:44:09 2009 +0200
@@ -407,7 +407,7 @@
(*Tactic for possibility theorems*)
fun possibility_tac ctxt =
REPEAT (*omit used_Says so that Nonces start from different traces!*)
- (ALLGOALS (simp_tac (local_simpset_of ctxt delsimps [@{thm used_Says}]))
+ (ALLGOALS (simp_tac (simpset_of ctxt delsimps [@{thm used_Says}]))
THEN
REPEAT_FIRST (eq_assume_tac ORELSE'
resolve_tac [refl, conjI, @{thm Nonce_supply}]))
@@ -416,7 +416,7 @@
nonces and keys initially*)
fun basic_possibility_tac ctxt =
REPEAT
- (ALLGOALS (asm_simp_tac (local_simpset_of ctxt setSolver safe_solver))
+ (ALLGOALS (asm_simp_tac (simpset_of ctxt setSolver safe_solver))
THEN
REPEAT_FIRST (resolve_tac [refl, conjI]))
--- a/src/HOL/Auth/Shared.thy Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOL/Auth/Shared.thy Thu Jul 23 18:44:09 2009 +0200
@@ -204,7 +204,7 @@
such as Nonce ?N \<notin> used evs that match Nonce_supply*)
fun possibility_tac ctxt =
(REPEAT
- (ALLGOALS (simp_tac (local_simpset_of ctxt
+ (ALLGOALS (simp_tac (simpset_of ctxt
delsimps [@{thm used_Says}, @{thm used_Notes}, @{thm used_Gets}]
setSolver safe_solver))
THEN
@@ -215,7 +215,7 @@
nonces and keys initially*)
fun basic_possibility_tac ctxt =
REPEAT
- (ALLGOALS (asm_simp_tac (local_simpset_of ctxt setSolver safe_solver))
+ (ALLGOALS (asm_simp_tac (simpset_of ctxt setSolver safe_solver))
THEN
REPEAT_FIRST (resolve_tac [refl, conjI]))
--- a/src/HOL/Auth/Smartcard/ShoupRubin.thy Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOL/Auth/Smartcard/ShoupRubin.thy Thu Jul 23 18:44:09 2009 +0200
@@ -757,7 +757,7 @@
(*SR9*) dresolve_tac [@{thm Gets_imp_knows_Spy_parts_Snd}] 19 THEN
(*Oops1*) dresolve_tac [@{thm Outpts_B_Card_form_7}] 25 THEN
(*Oops2*) dresolve_tac [@{thm Outpts_A_Card_form_10}] 27 THEN
- (*Base*) (force_tac (local_clasimpset_of ctxt)) 1
+ (*Base*) (force_tac (clasimpset_of ctxt)) 1
val analz_prepare_tac =
prepare_tac THEN
--- a/src/HOL/Auth/Smartcard/ShoupRubinBella.thy Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOL/Auth/Smartcard/ShoupRubinBella.thy Thu Jul 23 18:44:09 2009 +0200
@@ -755,7 +755,7 @@
fun prepare_tac ctxt =
(*SR_U8*) forward_tac [@{thm Outpts_B_Card_form_7}] 14 THEN
- (*SR_U8*) clarify_tac (local_claset_of ctxt) 15 THEN
+ (*SR_U8*) clarify_tac (claset_of ctxt) 15 THEN
(*SR_U9*) forward_tac [@{thm Outpts_A_Card_form_4}] 16 THEN
(*SR_U11*) forward_tac [@{thm Outpts_A_Card_form_10}] 21
@@ -765,7 +765,7 @@
(*SR_U9*) dresolve_tac [@{thm Gets_imp_knows_Spy_parts_Snd}] 19 THEN
(*Oops1*) dresolve_tac [@{thm Outpts_B_Card_form_7}] 25 THEN
(*Oops2*) dresolve_tac [@{thm Outpts_A_Card_form_10}] 27 THEN
- (*Base*) (force_tac (local_clasimpset_of ctxt)) 1
+ (*Base*) (force_tac (clasimpset_of ctxt)) 1
fun analz_prepare_tac ctxt =
prepare_tac ctxt THEN
--- a/src/HOL/Auth/Smartcard/Smartcard.thy Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOL/Auth/Smartcard/Smartcard.thy Thu Jul 23 18:44:09 2009 +0200
@@ -375,7 +375,7 @@
such as Nonce ?N \<notin> used evs that match Nonce_supply*)
fun possibility_tac ctxt =
(REPEAT
- (ALLGOALS (simp_tac (local_simpset_of ctxt
+ (ALLGOALS (simp_tac (simpset_of ctxt
delsimps [@{thm used_Says}, @{thm used_Notes}, @{thm used_Gets},
@{thm used_Inputs}, @{thm used_C_Gets}, @{thm used_Outpts}, @{thm used_A_Gets}]
setSolver safe_solver))
@@ -387,7 +387,7 @@
nonces and keys initially*)
fun basic_possibility_tac ctxt =
REPEAT
- (ALLGOALS (asm_simp_tac (local_simpset_of ctxt setSolver safe_solver))
+ (ALLGOALS (asm_simp_tac (simpset_of ctxt setSolver safe_solver))
THEN
REPEAT_FIRST (resolve_tac [refl, conjI]))
--- a/src/HOL/Bali/Basis.thy Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOL/Bali/Basis.thy Thu Jul 23 18:44:09 2009 +0200
@@ -229,7 +229,7 @@
ML {*
fun sum3_instantiate ctxt thm = map (fn s =>
- simplify (Simplifier.local_simpset_of ctxt delsimps[@{thm not_None_eq}])
+ simplify (simpset_of ctxt delsimps[@{thm not_None_eq}])
(read_instantiate ctxt [(("t", 0), "In" ^ s ^ " ?x")] thm)) ["1l","2","3","1r"]
*}
(* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *)
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Thu Jul 23 18:44:09 2009 +0200
@@ -692,7 +692,7 @@
val clt = Thm.dest_fun2 ct
val cz = Thm.dest_arg ct
val neg = cr </ Rat.zero
- val cthp = Simplifier.rewrite (local_simpset_of ctxt)
+ val cthp = Simplifier.rewrite (simpset_of ctxt)
(Thm.capply @{cterm "Trueprop"}
(if neg then Thm.capply (Thm.capply clt c) cz
else Thm.capply (Thm.capply clt cz) c))
@@ -715,7 +715,7 @@
val clt = Thm.dest_fun2 ct
val cz = Thm.dest_arg ct
val neg = cr </ Rat.zero
- val cthp = Simplifier.rewrite (local_simpset_of ctxt)
+ val cthp = Simplifier.rewrite (simpset_of ctxt)
(Thm.capply @{cterm "Trueprop"}
(if neg then Thm.capply (Thm.capply clt c) cz
else Thm.capply (Thm.capply clt cz) c))
@@ -736,7 +736,7 @@
val clt = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "op <"}
val cz = Thm.dest_arg ct
val neg = cr </ Rat.zero
- val cthp = Simplifier.rewrite (local_simpset_of ctxt)
+ val cthp = Simplifier.rewrite (simpset_of ctxt)
(Thm.capply @{cterm "Trueprop"}
(if neg then Thm.capply (Thm.capply clt c) cz
else Thm.capply (Thm.capply clt cz) c))
@@ -760,7 +760,7 @@
val clt = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "op <"}
val cz = Thm.dest_arg ct
val neg = cr </ Rat.zero
- val cthp = Simplifier.rewrite (local_simpset_of ctxt)
+ val cthp = Simplifier.rewrite (simpset_of ctxt)
(Thm.capply @{cterm "Trueprop"}
(if neg then Thm.capply (Thm.capply clt c) cz
else Thm.capply (Thm.capply clt cz) c))
@@ -779,7 +779,7 @@
val cr = dest_frac c
val ceq = Thm.dest_fun2 ct
val cz = Thm.dest_arg ct
- val cthp = Simplifier.rewrite (local_simpset_of ctxt)
+ val cthp = Simplifier.rewrite (simpset_of ctxt)
(Thm.capply @{cterm "Trueprop"}
(Thm.capply @{cterm "Not"} (Thm.capply (Thm.capply ceq c) cz)))
val cth = equal_elim (symmetric cthp) TrueI
@@ -801,7 +801,7 @@
val cr = dest_frac c
val ceq = Thm.dest_fun2 ct
val cz = Thm.dest_arg ct
- val cthp = Simplifier.rewrite (local_simpset_of ctxt)
+ val cthp = Simplifier.rewrite (simpset_of ctxt)
(Thm.capply @{cterm "Trueprop"}
(Thm.capply @{cterm "Not"} (Thm.capply (Thm.capply ceq c) cz)))
val cth = equal_elim (symmetric cthp) TrueI
--- a/src/HOL/HOL.thy Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOL/HOL.thy Thu Jul 23 18:44:09 2009 +0200
@@ -833,7 +833,7 @@
open BasicClassical;
ML_Antiquote.value "claset"
- (Scan.succeed "Classical.local_claset_of (ML_Context.the_local_context ())");
+ (Scan.succeed "Classical.claset_of (ML_Context.the_local_context ())");
structure ResAtpset = Named_Thms
(val name = "atp" val description = "ATP rules");
--- a/src/HOL/Hoare/Hoare.thy Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOL/Hoare/Hoare.thy Thu Jul 23 18:44:09 2009 +0200
@@ -239,7 +239,7 @@
method_setup vcg_simp = {*
Scan.succeed (fn ctxt =>
- SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac (local_simpset_of ctxt)))) *}
+ SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac (simpset_of ctxt)))) *}
"verification condition generator plus simplification"
end
--- a/src/HOL/Hoare/HoareAbort.thy Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOL/Hoare/HoareAbort.thy Thu Jul 23 18:44:09 2009 +0200
@@ -251,7 +251,7 @@
method_setup vcg_simp = {*
Scan.succeed (fn ctxt =>
- SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac (local_simpset_of ctxt)))) *}
+ SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac (simpset_of ctxt)))) *}
"verification condition generator plus simplification"
(* Special syntax for guarded statements and guarded array updates: *)
--- a/src/HOL/Hoare/hoare_tac.ML Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOL/Hoare/hoare_tac.ML Thu Jul 23 18:44:09 2009 +0200
@@ -73,7 +73,7 @@
val MsetT = fastype_of big_Collect;
fun Mset_incl t = mk_Trueprop (inclt MsetT $ Free (Mset, MsetT) $ t);
val impl = Logic.mk_implies (Mset_incl big_Collect, Mset_incl small_Collect);
- val th = Goal.prove ctxt [Mset, P] [] impl (fn _ => blast_tac (local_claset_of ctxt) 1);
+ val th = Goal.prove ctxt [Mset, P] [] impl (fn _ => blast_tac (claset_of ctxt) 1);
in (vars, th) end;
end;
--- a/src/HOL/Library/comm_ring.ML Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOL/Library/comm_ring.ML Thu Jul 23 18:44:09 2009 +0200
@@ -89,7 +89,7 @@
fun comm_ring_tac ctxt = SUBGOAL (fn (g, i) =>
let
val thy = ProofContext.theory_of ctxt;
- val cring_ss = Simplifier.local_simpset_of ctxt (*FIXME really the full simpset!?*)
+ val cring_ss = Simplifier.simpset_of ctxt (*FIXME really the full simpset!?*)
addsimps cring_simps;
val (ca, cvs, clhs, crhs) = reif_eq thy (HOLogic.dest_Trueprop g)
val norm_eq_th =
--- a/src/HOL/Library/reflection.ML Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOL/Library/reflection.ML Thu Jul 23 18:44:09 2009 +0200
@@ -285,7 +285,7 @@
val th' = instantiate ([], cvs) th
val t' = (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) th'
val th'' = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, t')))
- (fn _ => simp_tac (local_simpset_of ctxt) 1)
+ (fn _ => simp_tac (simpset_of ctxt) 1)
in FWD trans [th'',th']
end
--- a/src/HOL/MicroJava/J/JTypeSafe.thy Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy Thu Jul 23 18:44:09 2009 +0200
@@ -204,7 +204,7 @@
apply( simp_all)
apply( tactic "ALLGOALS strip_tac")
apply( tactic {* ALLGOALS (eresolve_tac [thm "ty_expr.cases", thm "ty_exprs.cases", thm "wt_stmt.cases"]
- THEN_ALL_NEW (full_simp_tac (simpset_of @{theory Conform}))) *})
+ THEN_ALL_NEW (full_simp_tac (global_simpset_of @{theory Conform}))) *})
apply(tactic "ALLGOALS (EVERY' [REPEAT o (etac conjE), REPEAT o hyp_subst_tac])")
-- "Level 7"
--- a/src/HOL/Modelcheck/mucke_oracle.ML Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOL/Modelcheck/mucke_oracle.ML Thu Jul 23 18:44:09 2009 +0200
@@ -109,7 +109,7 @@
(
OldGoals.push_proof();
OldGoals.goalw_cterm [] (cterm_of sign trm);
-by (simp_tac (simpset_of sign) 1);
+by (simp_tac (global_simpset_of sign) 1);
let
val if_tmp_result = result()
in
--- a/src/HOL/Nominal/nominal_datatype.ML Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Thu Jul 23 18:44:09 2009 +0200
@@ -324,7 +324,7 @@
(perm_names_types ~~ perm_indnames))))
(fn _ => EVERY [indtac induction perm_indnames 1,
ALLGOALS (asm_full_simp_tac
- (simpset_of thy2 addsimps [perm_fun_def]))])),
+ (global_simpset_of thy2 addsimps [perm_fun_def]))])),
length new_type_names));
(**** prove [] \<bullet> t = t ****)
@@ -344,7 +344,7 @@
(perm_names ~~
map body_type perm_types ~~ perm_indnames)))))
(fn _ => EVERY [indtac induction perm_indnames 1,
- ALLGOALS (asm_full_simp_tac (simpset_of thy2))])),
+ ALLGOALS (asm_full_simp_tac (global_simpset_of thy2))])),
length new_type_names))
end)
atoms);
@@ -379,7 +379,7 @@
(perm_names ~~
map body_type perm_types ~~ perm_indnames)))))
(fn _ => EVERY [indtac induction perm_indnames 1,
- ALLGOALS (asm_full_simp_tac (simpset_of thy2 addsimps [pt2', pt2_ax]))]))),
+ ALLGOALS (asm_full_simp_tac (global_simpset_of thy2 addsimps [pt2', pt2_ax]))]))),
length new_type_names)
end) atoms);
@@ -415,7 +415,7 @@
(perm_names ~~
map body_type perm_types ~~ perm_indnames))))))
(fn _ => EVERY [indtac induction perm_indnames 1,
- ALLGOALS (asm_full_simp_tac (simpset_of thy2 addsimps [pt3', pt3_rev', pt3_ax]))]))),
+ ALLGOALS (asm_full_simp_tac (global_simpset_of thy2 addsimps [pt3', pt3_rev', pt3_ax]))]))),
length new_type_names)
end) atoms);
@@ -437,7 +437,7 @@
val permT2 = mk_permT (Type (name2, []));
val Ts = map body_type perm_types;
val cp_inst = cp_inst_of thy name1 name2;
- val simps = simpset_of thy addsimps (perm_fun_def ::
+ val simps = global_simpset_of thy addsimps (perm_fun_def ::
(if name1 <> name2 then
let val dj = dj_thm_of thy name2 name1
in [dj RS (cp_inst RS dj_cp), dj RS dj_perm_perm_forget] end
@@ -601,7 +601,7 @@
end) (rep_set_names'' ~~ recTs' ~~ perm_indnames')))))
(fn _ => EVERY
[indtac rep_induct [] 1,
- ALLGOALS (simp_tac (simpset_of thy4 addsimps
+ ALLGOALS (simp_tac (global_simpset_of thy4 addsimps
(symmetric perm_fun_def :: abs_perm))),
ALLGOALS (resolve_tac rep_intrs THEN_ALL_NEW assume_tac)])),
length new_type_names));
@@ -661,8 +661,8 @@
map (inter_sort thy sort o snd) tvs, [pt_class])
(EVERY [Class.intro_classes_tac [],
rewrite_goals_tac [perm_def],
- asm_full_simp_tac (simpset_of thy addsimps [Rep_inverse]) 1,
- asm_full_simp_tac (simpset_of thy addsimps
+ asm_full_simp_tac (global_simpset_of thy addsimps [Rep_inverse]) 1,
+ asm_full_simp_tac (global_simpset_of thy addsimps
[Rep RS perm_closed RS Abs_inverse]) 1,
asm_full_simp_tac (HOL_basic_ss addsimps [PureThy.get_thm thy
("pt_" ^ Long_Name.base_name atom ^ "3")]) 1]) thy
@@ -690,7 +690,7 @@
map (inter_sort thy sort o snd) tvs, [cp_class])
(EVERY [Class.intro_classes_tac [],
rewrite_goals_tac [perm_def],
- asm_full_simp_tac (simpset_of thy addsimps
+ asm_full_simp_tac (global_simpset_of thy addsimps
((Rep RS perm_closed1 RS Abs_inverse) ::
(if atom1 = atom2 then []
else [Rep RS perm_closed2 RS Abs_inverse]))) 1,
@@ -875,7 +875,7 @@
| prove_distinct_thms (p as (rep_thms, dist_lemma)) (k, t :: ts) =
let
val dist_thm = Goal.prove_global thy8 [] [] t (fn _ =>
- simp_tac (simpset_of thy8 addsimps (dist_lemma :: rep_thms)) 1)
+ simp_tac (global_simpset_of thy8 addsimps (dist_lemma :: rep_thms)) 1)
in dist_thm :: standard (dist_thm RS not_sym) ::
prove_distinct_thms p (k, ts)
end;
@@ -920,7 +920,7 @@
(HOLogic.mk_Trueprop (HOLogic.mk_eq
(perm (list_comb (c, l_args)), list_comb (c, r_args)))))
(fn _ => EVERY
- [simp_tac (simpset_of thy8 addsimps (constr_rep_thm :: perm_defs)) 1,
+ [simp_tac (global_simpset_of thy8 addsimps (constr_rep_thm :: perm_defs)) 1,
simp_tac (HOL_basic_ss addsimps (Rep_thms @ Abs_inverse_thms @
constr_defs @ perm_closed_thms)) 1,
TRY (simp_tac (HOL_basic_ss addsimps
@@ -973,7 +973,7 @@
(HOLogic.mk_eq (list_comb (c, args1), list_comb (c, args2)),
foldr1 HOLogic.mk_conj eqs))))
(fn _ => EVERY
- [asm_full_simp_tac (simpset_of thy8 addsimps (constr_rep_thm ::
+ [asm_full_simp_tac (global_simpset_of thy8 addsimps (constr_rep_thm ::
rep_inject_thms')) 1,
TRY (asm_full_simp_tac (HOL_basic_ss addsimps (fresh_def :: supp_def ::
alpha @ abs_perm @ abs_fresh @ rep_inject_thms @
@@ -1100,7 +1100,7 @@
(Const ("Nominal.supp", T --> HOLogic.mk_setT atomT) $ Free (s, T)))
(indnames ~~ recTs)))))
(fn _ => indtac dt_induct indnames 1 THEN
- ALLGOALS (asm_full_simp_tac (simpset_of thy8 addsimps
+ ALLGOALS (asm_full_simp_tac (global_simpset_of thy8 addsimps
(abs_supp @ supp_atm @
PureThy.get_thms thy8 ("fs_" ^ Long_Name.base_name atom ^ "1") @
List.concat supp_thms))))),
--- a/src/HOL/Nominal/nominal_fresh_fun.ML Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML Thu Jul 23 18:44:09 2009 +0200
@@ -143,7 +143,7 @@
let
val thy = theory_of_thm thm;
val ctx = Context.init_proof thy;
- val ss = simpset_of thy;
+ val ss = global_simpset_of thy;
val abs_fresh = PureThy.get_thms thy "abs_fresh";
val fresh_perm_app = PureThy.get_thms thy "fresh_perm_app";
val ss' = ss addsimps fresh_prod::abs_fresh;
--- a/src/HOL/Nominal/nominal_inductive.ML Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML Thu Jul 23 18:44:09 2009 +0200
@@ -403,7 +403,7 @@
cut_facts_tac [th] 1 THEN REPEAT (etac conjE 1) THEN
REPEAT (REPEAT (resolve_tac [conjI, impI] 1) THEN
etac impE 1 THEN atac 1 THEN REPEAT (etac @{thm allE_Nil} 1) THEN
- asm_full_simp_tac (simpset_of thy) 1)
+ asm_full_simp_tac (simpset_of ctxt) 1)
end) |> singleton (ProofContext.export ctxt' ctxt);
(** strong case analysis rule **)
--- a/src/HOL/Nominal/nominal_inductive2.ML Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML Thu Jul 23 18:44:09 2009 +0200
@@ -438,7 +438,7 @@
cut_facts_tac [th] 1 THEN REPEAT (etac conjE 1) THEN
REPEAT (REPEAT (resolve_tac [conjI, impI] 1) THEN
etac impE 1 THEN atac 1 THEN REPEAT (etac @{thm allE_Nil} 1) THEN
- asm_full_simp_tac (simpset_of thy) 1)
+ asm_full_simp_tac (simpset_of ctxt) 1)
end) |>
fresh_postprocess |>
singleton (ProofContext.export ctxt' ctxt);
--- a/src/HOL/Nominal/nominal_permeq.ML Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML Thu Jul 23 18:44:09 2009 +0200
@@ -404,19 +404,19 @@
Method.sections (Simplifier.simp_modifiers') >>
(fn (prems, tac) => fn ctxt => METHOD (fn facts =>
HEADGOAL (Method.insert_tac (prems @ facts) THEN'
- (CHANGED_PROP oo tac) (local_simpset_of ctxt))));
+ (CHANGED_PROP oo tac) (simpset_of ctxt))));
(* setup so that the simpset is used which is active at the moment when the tactic is called *)
fun local_simp_meth_setup tac =
Method.sections (Simplifier.simp_modifiers' @ Splitter.split_modifiers) >>
- (K (SIMPLE_METHOD' o tac o local_simpset_of));
+ (K (SIMPLE_METHOD' o tac o simpset_of));
(* uses HOL_basic_ss only and fails if the tactic does not solve the subgoal *)
fun basic_simp_meth_setup debug tac =
Scan.depend (fn ctxt => Scan.succeed (Simplifier.map_ss (fn _ => HOL_basic_ss) ctxt, ())) --
Method.sections (Simplifier.simp_modifiers' @ Splitter.split_modifiers) >>
- (K (SIMPLE_METHOD' o (fn ss => if debug then tac ss else SOLVEI (tac ss)) o local_simpset_of));
+ (K (SIMPLE_METHOD' o (fn ss => if debug then tac ss else SOLVEI (tac ss)) o simpset_of));
val perm_simp_meth_debug = local_simp_meth_setup dperm_simp_tac;
val perm_extend_simp_meth = local_simp_meth_setup perm_extend_simp_tac;
--- a/src/HOL/SET-Protocol/MessageSET.thy Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOL/SET-Protocol/MessageSET.thy Thu Jul 23 18:44:09 2009 +0200
@@ -939,17 +939,17 @@
method_setup spy_analz = {*
Scan.succeed (fn ctxt =>
- SIMPLE_METHOD' (MessageSET.spy_analz_tac (local_clasimpset_of ctxt))) *}
+ SIMPLE_METHOD' (MessageSET.spy_analz_tac (clasimpset_of ctxt))) *}
"for proving the Fake case when analz is involved"
method_setup atomic_spy_analz = {*
Scan.succeed (fn ctxt =>
- SIMPLE_METHOD' (MessageSET.atomic_spy_analz_tac (local_clasimpset_of ctxt))) *}
+ SIMPLE_METHOD' (MessageSET.atomic_spy_analz_tac (clasimpset_of ctxt))) *}
"for debugging spy_analz"
method_setup Fake_insert_simp = {*
Scan.succeed (fn ctxt =>
- SIMPLE_METHOD' (MessageSET.Fake_insert_simp_tac (local_simpset_of ctxt))) *}
+ SIMPLE_METHOD' (MessageSET.Fake_insert_simp_tac (simpset_of ctxt))) *}
"for debugging spy_analz"
end
--- a/src/HOL/SET-Protocol/PublicSET.thy Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOL/SET-Protocol/PublicSET.thy Thu Jul 23 18:44:09 2009 +0200
@@ -350,7 +350,7 @@
(*Tactic for possibility theorems*)
fun possibility_tac ctxt =
REPEAT (*omit used_Says so that Nonces start from different traces!*)
- (ALLGOALS (simp_tac (local_simpset_of ctxt delsimps [@{thm used_Says}, @{thm used_Notes}]))
+ (ALLGOALS (simp_tac (simpset_of ctxt delsimps [@{thm used_Says}, @{thm used_Notes}]))
THEN
REPEAT_FIRST (eq_assume_tac ORELSE'
resolve_tac [refl, conjI, @{thm Nonce_supply}]))
@@ -359,7 +359,7 @@
nonces and keys initially*)
fun basic_possibility_tac ctxt =
REPEAT
- (ALLGOALS (asm_simp_tac (local_simpset_of ctxt setSolver safe_solver))
+ (ALLGOALS (asm_simp_tac (simpset_of ctxt setSolver safe_solver))
THEN
REPEAT_FIRST (resolve_tac [refl, conjI]))
--- a/src/HOL/SizeChange/sct.ML Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOL/SizeChange/sct.ML Thu Jul 23 18:44:09 2009 +0200
@@ -184,7 +184,7 @@
fun setup_probe_goal ctxt domT Dtab Mtab (i, j) =
let
- val css = local_clasimpset_of ctxt
+ val css = clasimpset_of ctxt
val thy = ProofContext.theory_of ctxt
val RD1 = get_elem (Dtab i)
val RD2 = get_elem (Dtab j)
@@ -269,7 +269,7 @@
fun in_graph_tac ctxt =
simp_tac (HOL_basic_ss addsimps has_edge_simps) 1
- THEN (simp_tac (local_simpset_of ctxt) 1) (* FIXME reduce simpset *)
+ THEN (simp_tac (simpset_of ctxt) 1) (* FIXME reduce simpset *)
fun approx_tac _ (NoStep thm) = rtac disjI1 1 THEN rtac thm 1
| approx_tac ctxt (Graph (G, thm)) =
@@ -334,7 +334,7 @@
val sound_int_goal = HOLogic.mk_Trueprop (mk_sound_int ACG RDlist mfuns)
val tac =
- unfold_tac [sound_int_def, len_simp] (local_simpset_of ctxt)
+ unfold_tac [sound_int_def, len_simp] (simpset_of ctxt)
THEN all_less_tac (map (all_less_tac o map (approx_tac ctxt)) parts)
in
tac (instantiate' [] [SOME (cterm_of thy ACG), SOME (cterm_of thy mfuns)] st)
--- a/src/HOL/TLA/Memory/MemoryImplementation.thy Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy Thu Jul 23 18:44:09 2009 +0200
@@ -763,7 +763,7 @@
*)
ML {*
fun split_idle_tac ctxt simps i =
- let val ss = Simplifier.local_simpset_of ctxt in
+ let val ss = simpset_of ctxt in
TRY (rtac @{thm actionI} i) THEN
InductTacs.case_tac ctxt "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" i THEN
rewrite_goals_tac @{thms action_rews} THEN
--- a/src/HOL/Tools/Function/decompose.ML Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOL/Tools/Function/decompose.ML Thu Jul 23 18:44:09 2009 +0200
@@ -98,7 +98,7 @@
fun auto_decompose_tac ctxt =
Termination.TERMINATION ctxt
- (decompose_tac ctxt (auto_tac (local_clasimpset_of ctxt))
+ (decompose_tac ctxt (auto_tac (clasimpset_of ctxt))
(K (K all_tac)) (K (K no_tac)))
--- a/src/HOL/Tools/Function/fundef_core.ML Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOL/Tools/Function/fundef_core.ML Thu Jul 23 18:44:09 2009 +0200
@@ -702,7 +702,7 @@
Goal.init goal
|> (SINGLE (resolve_tac [accI] 1)) |> the
|> (SINGLE (eresolve_tac [Thm.forall_elim_vars 0 R_cases] 1)) |> the
- |> (SINGLE (auto_tac (local_clasimpset_of ctxt))) |> the
+ |> (SINGLE (auto_tac (clasimpset_of ctxt))) |> the
|> Goal.conclude
|> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
end
@@ -831,7 +831,7 @@
((rtac (G_induct OF [a]))
THEN_ALL_NEW (rtac accI)
THEN_ALL_NEW (etac R_cases)
- THEN_ALL_NEW (asm_full_simp_tac (local_simpset_of octxt))) 1)
+ THEN_ALL_NEW (asm_full_simp_tac (simpset_of octxt))) 1)
val default_thm = (forall_intr_vars graph_implies_dom) COMP (f_def COMP fundef_default_value)
@@ -849,9 +849,9 @@
(fn _ =>
rtac (instantiate' [] [SOME (cterm_of thy lhs_acc)] case_split) 1
THEN (rtac (Thm.forall_elim_vars 0 psimp) THEN_ALL_NEW assume_tac) 1
- THEN (simp_default_tac (local_simpset_of ctxt) 1)
+ THEN (simp_default_tac (simpset_of ctxt) 1)
THEN (etac not_acc_down 1)
- THEN ((etac R_cases) THEN_ALL_NEW (simp_default_tac (local_simpset_of ctxt))) 1)
+ THEN ((etac R_cases) THEN_ALL_NEW (simp_default_tac (simpset_of ctxt))) 1)
|> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
end
in
--- a/src/HOL/Tools/Function/lexicographic_order.ML Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOL/Tools/Function/lexicographic_order.ML Thu Jul 23 18:44:09 2009 +0200
@@ -217,7 +217,7 @@
fun lexicographic_order_tac ctxt =
TRY (FundefCommon.apply_termination_rule ctxt 1)
THEN lex_order_tac ctxt
- (auto_tac (local_clasimpset_of ctxt addsimps2 FundefCommon.Termination_Simps.get ctxt))
+ (auto_tac (clasimpset_of ctxt addsimps2 FundefCommon.Termination_Simps.get ctxt))
val lexicographic_order = SIMPLE_METHOD o lexicographic_order_tac
--- a/src/HOL/Tools/Function/mutual.ML Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOL/Tools/Function/mutual.ML Thu Jul 23 18:44:09 2009 +0200
@@ -206,7 +206,7 @@
(HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs))
(fn _ => (LocalDefs.unfold_tac ctxt all_orig_fdefs)
THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1
- THEN (simp_tac (local_simpset_of ctxt addsimps SumTree.proj_in_rules)) 1)
+ THEN (simp_tac (simpset_of ctxt addsimps SumTree.proj_in_rules)) 1)
|> restore_cond
|> export
end
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Thu Jul 23 18:44:09 2009 +0200
@@ -291,7 +291,7 @@
THEN (rtac @{thm rp_inv_image_rp} 1)
THEN (rtac (order_rpair ms_rp label) 1)
THEN PRIMITIVE (instantiate' [] [SOME level_mapping])
- THEN unfold_tac @{thms rp_inv_image_def} (local_simpset_of ctxt)
+ THEN unfold_tac @{thms rp_inv_image_def} (simpset_of ctxt)
THEN LocalDefs.unfold_tac ctxt
(@{thms split_conv} @ @{thms fst_conv} @ @{thms snd_conv})
THEN REPEAT (SOMEGOAL (resolve_tac [@{thm Un_least}, @{thm empty_subsetI}]))
@@ -406,7 +406,7 @@
fun decomp_scnp orders ctxt =
let
val extra_simps = FundefCommon.Termination_Simps.get ctxt
- val autom_tac = auto_tac (local_clasimpset_of ctxt addsimps2 extra_simps)
+ val autom_tac = auto_tac (clasimpset_of ctxt addsimps2 extra_simps)
in
SIMPLE_METHOD
(gen_sizechange_tac orders autom_tac ctxt (print_error ctxt))
--- a/src/HOL/Tools/Function/termination.ML Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOL/Tools/Function/termination.ML Thu Jul 23 18:44:09 2009 +0200
@@ -303,7 +303,7 @@
THEN' ((rtac @{thm refl}) (* unification instantiates all Vars *)
ORELSE' ((rtac @{thm conjI})
THEN' (rtac @{thm refl})
- THEN' (blast_tac (local_claset_of ctxt)))) (* Solve rest of context... not very elegant *)
+ THEN' (blast_tac (claset_of ctxt)))) (* Solve rest of context... not very elegant *)
) i
in
((PRIMITIVE (Drule.cterm_instantiate [(cert rel, cert relation)])
--- a/src/HOL/Tools/Qelim/ferrante_rackoff.ML Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOL/Tools/Qelim/ferrante_rackoff.ML Thu Jul 23 18:44:09 2009 +0200
@@ -228,6 +228,6 @@
ObjectLogic.full_atomize_tac i THEN
simp_tac (#simpset (snd instance)) i THEN (* FIXME already part of raw_ferrack_qe_conv? *)
CONVERSION (ObjectLogic.judgment_conv (raw_ferrack_qe_conv ctxt instance)) i THEN
- simp_tac (Simplifier.local_simpset_of ctxt) i)); (* FIXME really? *)
+ simp_tac (simpset_of ctxt) i)); (* FIXME really? *)
end;
--- a/src/HOL/Tools/inductive.ML Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOL/Tools/inductive.ML Thu Jul 23 18:44:09 2009 +0200
@@ -425,7 +425,7 @@
fun mk_cases ctxt prop =
let
val thy = ProofContext.theory_of ctxt;
- val ss = Simplifier.local_simpset_of ctxt;
+ val ss = simpset_of ctxt;
fun err msg =
error (Pretty.string_of (Pretty.block
--- a/src/HOL/Tools/recdef.ML Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOL/Tools/recdef.ML Thu Jul 23 18:44:09 2009 +0200
@@ -172,15 +172,15 @@
NONE => ctxt0
| SOME src => #2 (Method.syntax (Method.sections recdef_modifiers) src ctxt0));
val {simps, congs, wfs} = get_hints ctxt;
- val cs = local_claset_of ctxt;
- val ss = local_simpset_of ctxt addsimps simps;
+ val cs = claset_of ctxt;
+ val ss = simpset_of ctxt addsimps simps;
in (cs, ss, rev (map snd congs), wfs) end;
fun prepare_hints_i thy () =
let
val ctxt0 = ProofContext.init thy;
val {simps, congs, wfs} = get_global_hints thy;
- in (local_claset_of ctxt0, local_simpset_of ctxt0 addsimps simps, rev (map snd congs), wfs) end;
+ in (claset_of ctxt0, simpset_of ctxt0 addsimps simps, rev (map snd congs), wfs) end;
--- a/src/HOL/Tools/simpdata.ML Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOL/Tools/simpdata.ML Thu Jul 23 18:44:09 2009 +0200
@@ -158,7 +158,7 @@
open Clasimp;
val _ = ML_Antiquote.value "clasimpset"
- (Scan.succeed "Clasimp.local_clasimpset_of (ML_Context.the_local_context ())");
+ (Scan.succeed "Clasimp.clasimpset_of (ML_Context.the_local_context ())");
val mksimps_pairs =
[("op -->", [@{thm mp}]), ("op &", [@{thm conjunct1}, @{thm conjunct2}]),
--- a/src/HOL/UNITY/Comp/Alloc.thy Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOL/UNITY/Comp/Alloc.thy Thu Jul 23 18:44:09 2009 +0200
@@ -321,7 +321,7 @@
*}
method_setup record_auto = {*
- Scan.succeed (fn ctxt => SIMPLE_METHOD (record_auto_tac (local_clasimpset_of ctxt)))
+ Scan.succeed (fn ctxt => SIMPLE_METHOD (record_auto_tac (clasimpset_of ctxt)))
*} ""
lemma inj_sysOfAlloc [iff]: "inj sysOfAlloc"
@@ -714,7 +714,7 @@
method_setup rename_client_map = {*
Scan.succeed (fn ctxt =>
- SIMPLE_METHOD (rename_client_map_tac (local_simpset_of ctxt)))
+ SIMPLE_METHOD (rename_client_map_tac (simpset_of ctxt)))
*} ""
text{*Lifting @{text Client_Increasing} to @{term systemState}*}
--- a/src/HOL/UNITY/Simple/NSP_Bad.thy Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOL/UNITY/Simple/NSP_Bad.thy Thu Jul 23 18:44:09 2009 +0200
@@ -125,7 +125,7 @@
method_setup ns_induct = {*
Scan.succeed (fn ctxt =>
- SIMPLE_METHOD' (ns_induct_tac (local_clasimpset_of ctxt))) *}
+ SIMPLE_METHOD' (ns_induct_tac (clasimpset_of ctxt))) *}
"for inductive reasoning about the Needham-Schroeder protocol"
text{*Converts invariants into statements about reachable states*}
--- a/src/HOL/UNITY/UNITY_Main.thy Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOL/UNITY/UNITY_Main.thy Thu Jul 23 18:44:09 2009 +0200
@@ -11,12 +11,12 @@
method_setup safety = {*
Scan.succeed (fn ctxt =>
- SIMPLE_METHOD' (constrains_tac (local_clasimpset_of ctxt))) *}
+ SIMPLE_METHOD' (constrains_tac (clasimpset_of ctxt))) *}
"for proving safety properties"
method_setup ensures_tac = {*
Args.goal_spec -- Scan.lift Args.name_source >>
- (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac (local_clasimpset_of ctxt) s))
+ (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac (clasimpset_of ctxt) s))
*} "for proving progress properties"
end
--- a/src/HOL/Word/WordArith.thy Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOL/Word/WordArith.thy Thu Jul 23 18:44:09 2009 +0200
@@ -513,8 +513,8 @@
fun uint_arith_tacs ctxt =
let
fun arith_tac' n t = Arith_Data.verbose_arith_tac ctxt n t handle COOPER => Seq.empty;
- val cs = local_claset_of ctxt;
- val ss = local_simpset_of ctxt;
+ val cs = claset_of ctxt;
+ val ss = simpset_of ctxt;
in
[ clarify_tac cs 1,
full_simp_tac (uint_arith_ss_of ss) 1,
@@ -1075,8 +1075,8 @@
fun unat_arith_tacs ctxt =
let
fun arith_tac' n t = Arith_Data.verbose_arith_tac ctxt n t handle COOPER => Seq.empty;
- val cs = local_claset_of ctxt;
- val ss = local_simpset_of ctxt;
+ val cs = claset_of ctxt;
+ val ss = simpset_of ctxt;
in
[ clarify_tac cs 1,
full_simp_tac (unat_arith_ss_of ss) 1,
--- a/src/HOLCF/FOCUS/Buffer.thy Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOLCF/FOCUS/Buffer.thy Thu Jul 23 18:44:09 2009 +0200
@@ -101,7 +101,7 @@
fun B_prover s tac eqs =
let val thy = the_context () in
prove_goal thy s (fn prems => [cut_facts_tac prems 1,
- tac 1, auto_tac (claset_of thy, simpset_of thy addsimps eqs)])
+ tac 1, auto_tac (global_claset_of thy, global_simpset_of thy addsimps eqs)])
end;
fun prove_forw s thm = B_prover s (dtac (thm RS iffD1)) [];
--- a/src/HOLCF/IOA/Modelcheck/MuIOA.thy Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOLCF/IOA/Modelcheck/MuIOA.thy Thu Jul 23 18:44:09 2009 +0200
@@ -278,14 +278,14 @@
by (REPEAT (rtac impI 1));
by (REPEAT (dtac eq_reflection 1));
(* Bis hierher wird im Kapitel 4 erl"autert, ab hier im Kapitel 5 *)
-by (full_simp_tac ((simpset_of sign delcongs (if_weak_cong :: weak_case_congs)
+by (full_simp_tac ((global_simpset_of sign delcongs (if_weak_cong :: weak_case_congs)
delsimps [not_iff,split_part])
addsimps (thl @ comp_simps @ restrict_simps @ hide_simps @
rename_simps @ ioa_simps @ asig_simps)) 1);
by (full_simp_tac
(Mucke_ss delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) 1);
by (REPEAT (if_full_simp_tac
- (simpset_of sign delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) 1));
+ (global_simpset_of sign delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) 1));
by (call_mucke_tac 1);
(* Bis hierher wird im Kapitel 5 erl"autert, ab hier wieder im Kapitel 4 *)
by (atac 1);
--- a/src/HOLCF/IOA/meta_theory/Abstraction.thy Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOLCF/IOA/meta_theory/Abstraction.thy Thu Jul 23 18:44:09 2009 +0200
@@ -605,7 +605,7 @@
ML {*
fun abstraction_tac ctxt =
- let val (cs, ss) = local_clasimpset_of ctxt in
+ let val (cs, ss) = clasimpset_of ctxt in
SELECT_GOAL (auto_tac (cs addSIs @{thms weak_strength_lemmas},
ss addsimps [@{thm state_strengthening_def}, @{thm state_weakening_def}]))
end
--- a/src/HOLCF/IOA/meta_theory/CompoScheds.thy Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoScheds.thy Thu Jul 23 18:44:09 2009 +0200
@@ -299,10 +299,10 @@
in
fun mkex_induct_tac ctxt sch exA exB =
- let val ss = Simplifier.local_simpset_of ctxt in
+ let val ss = simpset_of ctxt in
EVERY1[Seq_induct_tac ctxt sch defs,
asm_full_simp_tac ss,
- SELECT_GOAL (safe_tac (claset_of @{theory Fun})),
+ SELECT_GOAL (safe_tac (global_claset_of @{theory Fun})),
Seq_case_simp_tac ctxt exA,
Seq_case_simp_tac ctxt exB,
asm_full_simp_tac ss,
--- a/src/HOLCF/IOA/meta_theory/Sequence.thy Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy Thu Jul 23 18:44:09 2009 +0200
@@ -1091,7 +1091,7 @@
(* on a>>s only simp_tac, as full_simp_tac is uncomplete and often causes errors *)
fun Seq_case_simp_tac ctxt s i =
- let val ss = Simplifier.local_simpset_of ctxt in
+ let val ss = simpset_of ctxt in
Seq_case_tac ctxt s i
THEN asm_simp_tac ss (i+2)
THEN asm_full_simp_tac ss (i+1)
@@ -1100,7 +1100,7 @@
(* rws are definitions to be unfolded for admissibility check *)
fun Seq_induct_tac ctxt s rws i =
- let val ss = Simplifier.local_simpset_of ctxt in
+ let val ss = simpset_of ctxt in
res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_induct} i
THEN (REPEAT_DETERM (CHANGED (asm_simp_tac ss (i+1))))
THEN simp_tac (ss addsimps rws) i
@@ -1108,15 +1108,15 @@
fun Seq_Finite_induct_tac ctxt i =
etac @{thm Seq_Finite_ind} i
- THEN (REPEAT_DETERM (CHANGED (asm_simp_tac (Simplifier.local_simpset_of ctxt) i)));
+ THEN (REPEAT_DETERM (CHANGED (asm_simp_tac (simpset_of ctxt) i)));
fun pair_tac ctxt s =
res_inst_tac ctxt [(("p", 0), s)] PairE
- THEN' hyp_subst_tac THEN' asm_full_simp_tac (Simplifier.local_simpset_of ctxt);
+ THEN' hyp_subst_tac THEN' asm_full_simp_tac (simpset_of ctxt);
(* induction on a sequence of pairs with pairsplitting and simplification *)
fun pair_induct_tac ctxt s rws i =
- let val ss = Simplifier.local_simpset_of ctxt in
+ let val ss = simpset_of ctxt in
res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_induct} i
THEN pair_tac ctxt "a" (i+3)
THEN (REPEAT_DETERM (CHANGED (simp_tac ss (i+1))))
--- a/src/HOLCF/Lift.thy Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOLCF/Lift.thy Thu Jul 23 18:44:09 2009 +0200
@@ -61,7 +61,7 @@
method_setup defined = {*
Scan.succeed (fn ctxt => SIMPLE_METHOD'
- (etac @{thm lift_definedE} THEN' asm_simp_tac (local_simpset_of ctxt)))
+ (etac @{thm lift_definedE} THEN' asm_simp_tac (simpset_of ctxt)))
*} ""
lemma DefE: "Def x = \<bottom> \<Longrightarrow> R"
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Thu Jul 23 18:44:09 2009 +0200
@@ -685,7 +685,7 @@
(* ----- theorems concerning finite approximation and finite induction ------ *)
local
- val iterate_Cprod_ss = simpset_of @{theory Fix};
+ val iterate_Cprod_ss = global_simpset_of @{theory Fix};
val copy_con_rews = copy_rews @ con_rews;
val copy_take_defs =
(if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def;
--- a/src/HOLCF/Tools/fixrec.ML Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOLCF/Tools/fixrec.ML Thu Jul 23 18:44:09 2009 +0200
@@ -158,13 +158,13 @@
val thy = ProofContext.theory_of lthy;
val names = map (Binding.name_of o fst o fst) fixes;
val all_names = space_implode "_" names;
- val (lhss,rhss) = ListPair.unzip (map (dest_eqs o snd) spec);
+ val (lhss, rhss) = ListPair.unzip (map (dest_eqs o snd) spec);
val functional = lambda_tuple lhss (mk_tuple rhss);
val fixpoint = mk_fix (mk_cabs functional);
val cont_thm =
Goal.prove lthy [] [] (mk_trp (mk_cont functional))
- (K (simp_tac (local_simpset_of lthy) 1));
+ (K (simp_tac (simpset_of lthy) 1));
fun one_def (l as Free(n,_)) r =
let val b = Long_Name.base_name n
@@ -311,12 +311,12 @@
(*************************************************************************)
(* proves a block of pattern matching equations as theorems, using unfold *)
-fun make_simps lthy (unfold_thm, eqns : (Attrib.binding * term) list) =
+fun make_simps ctxt (unfold_thm, eqns : (Attrib.binding * term) list) =
let
val tacs =
[rtac (unfold_thm RS @{thm ssubst_lhs}) 1,
- asm_simp_tac (local_simpset_of lthy) 1];
- fun prove_term t = Goal.prove lthy [] [] t (K (EVERY tacs));
+ asm_simp_tac (simpset_of ctxt) 1];
+ fun prove_term t = Goal.prove ctxt [] [] t (K (EVERY tacs));
fun prove_eqn (bind, eqn_t) = (bind, prove_term eqn_t);
in
map prove_eqn eqns
@@ -399,7 +399,7 @@
fixrec_err "function is not declared as constant in theory";
val unfold_thm = PureThy.get_thm thy (cname^"_unfold");
val simp = Goal.prove_global thy [] [] eq
- (fn _ => EVERY [stac unfold_thm 1, simp_tac (simpset_of thy) 1]);
+ (fn _ => EVERY [stac unfold_thm 1, simp_tac (global_simpset_of thy) 1]);
in simp end;
fun gen_add_fixpat prep_term prep_attrib ((name, srcs), strings) thy =
--- a/src/Pure/Isar/isar_cmd.ML Thu Jul 23 18:44:08 2009 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Thu Jul 23 18:44:09 2009 +0200
@@ -363,7 +363,7 @@
val print_simpset = Toplevel.unknown_context o
Toplevel.keep (fn state =>
let val ctxt = Toplevel.context_of state
- in Pretty.writeln (Simplifier.pretty_ss ctxt (Simplifier.local_simpset_of ctxt)) end);
+ in Pretty.writeln (Simplifier.pretty_ss ctxt (simpset_of ctxt)) end);
val print_rules = Toplevel.unknown_context o
Toplevel.keep (ContextRules.print_rules o Toplevel.context_of);
--- a/src/Pure/Tools/find_theorems.ML Thu Jul 23 18:44:08 2009 +0200
+++ b/src/Pure/Tools/find_theorems.ML Thu Jul 23 18:44:09 2009 +0200
@@ -207,7 +207,7 @@
fun filter_simp ctxt t (_, thm) =
let
- val mksimps = Simplifier.mksimps (Simplifier.local_simpset_of ctxt);
+ val mksimps = Simplifier.mksimps (simpset_of ctxt);
val extract_simp =
(map Thm.full_prop_of o mksimps, #1 o Logic.dest_equals o Logic.strip_imp_concl);
val ss = is_matching_thm false extract_simp ctxt false t thm;
--- a/src/Tools/eqsubst.ML Thu Jul 23 18:44:08 2009 +0200
+++ b/src/Tools/eqsubst.ML Thu Jul 23 18:44:09 2009 +0200
@@ -127,7 +127,7 @@
(* changes object "=" to meta "==" which prepares a given rewrite rule *)
fun prep_meta_eq ctxt =
- Simplifier.mksimps (Simplifier.local_simpset_of ctxt) #> map Drule.zero_var_indexes;
+ Simplifier.mksimps (simpset_of ctxt) #> map Drule.zero_var_indexes;
(* a type abriviation for match information *)
--- a/src/ZF/IntDiv_ZF.thy Thu Jul 23 18:44:08 2009 +0200
+++ b/src/ZF/IntDiv_ZF.thy Thu Jul 23 18:44:09 2009 +0200
@@ -1732,7 +1732,7 @@
(if ~b | #0 $<= integ_of w
then integ_of v zdiv (integ_of w)
else (integ_of v $+ #1) zdiv (integ_of w))"
- apply (simp_tac (simpset_of Int.thy add: zadd_assoc integ_of_BIT)
+ apply (simp_tac (global_simpset_of Int.thy add: zadd_assoc integ_of_BIT)
apply (simp (no_asm_simp) del: bin_arith_extra_simps@bin_rel_simps add: zdiv_zmult_zmult1 pos_zdiv_mult_2 lemma neg_zdiv_mult_2)
done
@@ -1778,7 +1778,7 @@
then #2 $* (integ_of v zmod integ_of w) $+ #1
else #2 $* ((integ_of v $+ #1) zmod integ_of w) - #1
else #2 $* (integ_of v zmod integ_of w))"
- apply (simp_tac (simpset_of Int.thy add: zadd_assoc integ_of_BIT)
+ apply (simp_tac (global_simpset_of Int.thy add: zadd_assoc integ_of_BIT)
apply (simp (no_asm_simp) del: bin_arith_extra_simps@bin_rel_simps add: zmod_zmult_zmult1 pos_zmod_mult_2 lemma neg_zmod_mult_2)
done
--- a/src/ZF/Tools/ind_cases.ML Thu Jul 23 18:44:08 2009 +0200
+++ b/src/ZF/Tools/ind_cases.ML Thu Jul 23 18:44:09 2009 +0200
@@ -47,8 +47,7 @@
fun inductive_cases args thy =
let
- val read_prop = Syntax.read_prop (ProofContext.init thy);
- val mk_cases = smart_cases thy (Simplifier.simpset_of thy) read_prop;
+ val mk_cases = smart_cases thy (global_simpset_of thy) (Syntax.read_prop_global thy);
val facts = args |> map (fn ((name, srcs), props) =>
((name, map (Attrib.attribute thy) srcs),
map (Thm.no_attributes o single o mk_cases) props));
@@ -62,7 +61,7 @@
(Scan.lift (Scan.repeat1 Args.name_source) >>
(fn props => fn ctxt =>
props
- |> map (smart_cases (ProofContext.theory_of ctxt) (local_simpset_of ctxt) (Syntax.read_prop ctxt))
+ |> map (smart_cases (ProofContext.theory_of ctxt) (simpset_of ctxt) (Syntax.read_prop ctxt))
|> Method.erule 0))
"dynamic case analysis on sets";
--- a/src/ZF/UNITY/Constrains.thy Thu Jul 23 18:44:08 2009 +0200
+++ b/src/ZF/UNITY/Constrains.thy Thu Jul 23 18:44:09 2009 +0200
@@ -471,7 +471,7 @@
(*proves "co" properties when the program is specified*)
fun constrains_tac ctxt =
- let val css as (cs, ss) = local_clasimpset_of ctxt in
+ let val css as (cs, ss) = clasimpset_of ctxt in
SELECT_GOAL
(EVERY [REPEAT (Always_Int_tac 1),
REPEAT (etac @{thm Always_ConstrainsI} 1
@@ -494,7 +494,7 @@
(*For proving invariants*)
fun always_tac ctxt i =
- rtac @{thm AlwaysI} i THEN force_tac (local_clasimpset_of ctxt) i THEN constrains_tac ctxt i;
+ rtac @{thm AlwaysI} i THEN force_tac (clasimpset_of ctxt) i THEN constrains_tac ctxt i;
*}
setup Program_Defs.setup
--- a/src/ZF/UNITY/SubstAx.thy Thu Jul 23 18:44:08 2009 +0200
+++ b/src/ZF/UNITY/SubstAx.thy Thu Jul 23 18:44:09 2009 +0200
@@ -351,7 +351,7 @@
ML {*
(*proves "ensures/leadsTo" properties when the program is specified*)
fun ensures_tac ctxt sact =
- let val css as (cs, ss) = local_clasimpset_of ctxt in
+ let val css as (cs, ss) = clasimpset_of ctxt in
SELECT_GOAL
(EVERY [REPEAT (Always_Int_tac 1),
etac @{thm Always_LeadsTo_Basis} 1
--- a/src/ZF/int_arith.ML Thu Jul 23 18:44:08 2009 +0200
+++ b/src/ZF/int_arith.ML Thu Jul 23 18:44:09 2009 +0200
@@ -145,7 +145,7 @@
val numeral_simp_ss = ZF_ss addsimps add_0s @ bin_simps @ tc_rules @ intifys
fun numeral_simp_tac ss =
ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
- THEN ALLGOALS (asm_simp_tac (local_simpset_of (Simplifier.the_context ss)))
+ THEN ALLGOALS (asm_simp_tac (simpset_of (Simplifier.the_context ss)))
val simplify_meta_eq = ArithData.simplify_meta_eq (add_0s @ mult_1s)
end;