local_cla/simpset_of;
authorwenzelm
Sun Jul 11 20:33:22 2004 +0200 (2004-07-11)
changeset 1503202aed07e01bf
parent 15031 726dc9146bb1
child 15033 255bc508a756
local_cla/simpset_of;
src/HOL/Auth/Message.thy
src/HOL/Auth/Public.thy
src/HOL/Auth/Shared.thy
src/HOL/Hoare/Hoare.thy
src/HOL/Hoare/HoareAbort.thy
src/HOL/Hyperreal/HyperDef.thy
src/HOL/SET-Protocol/MessageSET.thy
src/HOL/SET-Protocol/PublicSET.thy
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/meson.ML
src/HOL/Tools/recdef_package.ML
src/HOL/UNITY/Simple/NSP_Bad.thy
src/HOL/UNITY/UNITY_Main.thy
src/Provers/clasimp.ML
src/ZF/Tools/ind_cases.ML
src/ZF/UNITY/ClientImpl.thy
     1.1 --- a/src/HOL/Auth/Message.thy	Fri Jul 09 16:33:20 2004 +0200
     1.2 +++ b/src/HOL/Auth/Message.thy	Sun Jul 11 20:33:22 2004 +0200
     1.3 @@ -932,21 +932,19 @@
     1.4  method_setup spy_analz = {*
     1.5      Method.ctxt_args (fn ctxt =>
     1.6          Method.METHOD (fn facts => 
     1.7 -            gen_spy_analz_tac (Classical.get_local_claset ctxt,
     1.8 -                               Simplifier.get_local_simpset ctxt) 1)) *}
     1.9 +            gen_spy_analz_tac (local_clasimpset_of ctxt) 1)) *}
    1.10      "for proving the Fake case when analz is involved"
    1.11  
    1.12  method_setup atomic_spy_analz = {*
    1.13      Method.ctxt_args (fn ctxt =>
    1.14          Method.METHOD (fn facts => 
    1.15 -            atomic_spy_analz_tac (Classical.get_local_claset ctxt,
    1.16 -                                  Simplifier.get_local_simpset ctxt) 1)) *}
    1.17 +            atomic_spy_analz_tac (local_clasimpset_of ctxt) 1)) *}
    1.18      "for debugging spy_analz"
    1.19  
    1.20  method_setup Fake_insert_simp = {*
    1.21      Method.ctxt_args (fn ctxt =>
    1.22          Method.METHOD (fn facts =>
    1.23 -            Fake_insert_simp_tac (Simplifier.get_local_simpset ctxt) 1)) *}
    1.24 +            Fake_insert_simp_tac (local_simpset_of ctxt) 1)) *}
    1.25      "for debugging spy_analz"
    1.26  
    1.27  
     2.1 --- a/src/HOL/Auth/Public.thy	Fri Jul 09 16:33:20 2004 +0200
     2.2 +++ b/src/HOL/Auth/Public.thy	Sun Jul 11 20:33:22 2004 +0200
     2.3 @@ -435,7 +435,7 @@
     2.4  method_setup possibility = {*
     2.5      Method.ctxt_args (fn ctxt =>
     2.6          Method.METHOD (fn facts =>
     2.7 -            gen_possibility_tac (Simplifier.get_local_simpset ctxt))) *}
     2.8 +            gen_possibility_tac (local_simpset_of ctxt))) *}
     2.9      "for proving possibility theorems"
    2.10  
    2.11  end
     3.1 --- a/src/HOL/Auth/Shared.thy	Fri Jul 09 16:33:20 2004 +0200
     3.2 +++ b/src/HOL/Auth/Shared.thy	Sun Jul 11 20:33:22 2004 +0200
     3.3 @@ -272,7 +272,7 @@
     3.4  method_setup possibility = {*
     3.5      Method.ctxt_args (fn ctxt =>
     3.6          Method.METHOD (fn facts =>
     3.7 -            gen_possibility_tac (Simplifier.get_local_simpset ctxt))) *}
     3.8 +            gen_possibility_tac (local_simpset_of ctxt))) *}
     3.9      "for proving possibility theorems"
    3.10  
    3.11  lemma knows_subset_knows_Cons: "knows A evs <= knows A (e # evs)"
     4.1 --- a/src/HOL/Hoare/Hoare.thy	Fri Jul 09 16:33:20 2004 +0200
     4.2 +++ b/src/HOL/Hoare/Hoare.thy	Sun Jul 11 20:33:22 2004 +0200
     4.3 @@ -235,7 +235,7 @@
     4.4  method_setup vcg_simp = {*
     4.5    Method.ctxt_args (fn ctxt =>
     4.6      Method.METHOD (fn facts => 
     4.7 -      hoare_tac (asm_full_simp_tac (Simplifier.get_local_simpset ctxt))1)) *}
     4.8 +      hoare_tac (asm_full_simp_tac (local_simpset_of ctxt))1)) *}
     4.9    "verification condition generator plus simplification"
    4.10  
    4.11  end
     5.1 --- a/src/HOL/Hoare/HoareAbort.thy	Fri Jul 09 16:33:20 2004 +0200
     5.2 +++ b/src/HOL/Hoare/HoareAbort.thy	Sun Jul 11 20:33:22 2004 +0200
     5.3 @@ -245,7 +245,7 @@
     5.4  method_setup vcg_simp = {*
     5.5    Method.ctxt_args (fn ctxt =>
     5.6      Method.METHOD (fn facts => 
     5.7 -      hoare_tac (asm_full_simp_tac (Simplifier.get_local_simpset ctxt))1)) *}
     5.8 +      hoare_tac (asm_full_simp_tac (local_simpset_of ctxt))1)) *}
     5.9    "verification condition generator plus simplification"
    5.10  
    5.11  (* Special syntax for guarded statements and guarded array updates: *)
     6.1 --- a/src/HOL/Hyperreal/HyperDef.thy	Fri Jul 09 16:33:20 2004 +0200
     6.2 +++ b/src/HOL/Hyperreal/HyperDef.thy	Sun Jul 11 20:33:22 2004 +0200
     6.3 @@ -208,15 +208,13 @@
     6.4  method_setup fuf = {*
     6.5      Method.ctxt_args (fn ctxt =>
     6.6          Method.METHOD (fn facts =>
     6.7 -            fuf_tac (Classical.get_local_claset ctxt,
     6.8 -                     Simplifier.get_local_simpset ctxt) 1)) *}
     6.9 +            fuf_tac (local_clasimpset_of ctxt) 1)) *}
    6.10      "free ultrafilter tactic"
    6.11  
    6.12  method_setup ultra = {*
    6.13      Method.ctxt_args (fn ctxt =>
    6.14          Method.METHOD (fn facts =>
    6.15 -            ultra_tac (Classical.get_local_claset ctxt,
    6.16 -                       Simplifier.get_local_simpset ctxt) 1)) *}
    6.17 +            ultra_tac (local_clasimpset_of ctxt) 1)) *}
    6.18      "ultrafilter tactic"
    6.19  
    6.20  
     7.1 --- a/src/HOL/SET-Protocol/MessageSET.thy	Fri Jul 09 16:33:20 2004 +0200
     7.2 +++ b/src/HOL/SET-Protocol/MessageSET.thy	Sun Jul 11 20:33:22 2004 +0200
     7.3 @@ -936,21 +936,19 @@
     7.4  method_setup spy_analz = {*
     7.5      Method.ctxt_args (fn ctxt =>
     7.6          Method.METHOD (fn facts =>
     7.7 -            gen_spy_analz_tac (Classical.get_local_claset ctxt,
     7.8 -                               Simplifier.get_local_simpset ctxt) 1))*}
     7.9 +            gen_spy_analz_tac (local_clasimpset_of ctxt) 1))*}
    7.10      "for proving the Fake case when analz is involved"
    7.11  
    7.12  method_setup atomic_spy_analz = {*
    7.13      Method.ctxt_args (fn ctxt =>
    7.14          Method.METHOD (fn facts =>
    7.15 -            atomic_spy_analz_tac (Classical.get_local_claset ctxt,
    7.16 -                                  Simplifier.get_local_simpset ctxt) 1))*}
    7.17 +            atomic_spy_analz_tac (local_clasimpset_of ctxt) 1))*}
    7.18      "for debugging spy_analz"
    7.19  
    7.20  method_setup Fake_insert_simp = {*
    7.21      Method.ctxt_args (fn ctxt =>
    7.22          Method.METHOD (fn facts =>
    7.23 -            Fake_insert_simp_tac (Simplifier.get_local_simpset ctxt) 1))*}
    7.24 +            Fake_insert_simp_tac (local_simpset_of ctxt) 1))*}
    7.25      "for debugging spy_analz"
    7.26  
    7.27  
     8.1 --- a/src/HOL/SET-Protocol/PublicSET.thy	Fri Jul 09 16:33:20 2004 +0200
     8.2 +++ b/src/HOL/SET-Protocol/PublicSET.thy	Sun Jul 11 20:33:22 2004 +0200
     8.3 @@ -374,7 +374,7 @@
     8.4  method_setup possibility = {*
     8.5      Method.ctxt_args (fn ctxt =>
     8.6          Method.METHOD (fn facts =>
     8.7 -            gen_possibility_tac (Simplifier.get_local_simpset ctxt))) *}
     8.8 +            gen_possibility_tac (local_simpset_of ctxt))) *}
     8.9      "for proving possibility theorems"
    8.10  
    8.11  
     9.1 --- a/src/HOL/Tools/inductive_package.ML	Fri Jul 09 16:33:20 2004 +0200
     9.2 +++ b/src/HOL/Tools/inductive_package.ML	Sun Jul 11 20:33:22 2004 +0200
     9.3 @@ -600,7 +600,7 @@
     9.4  fun mk_cases_meth (ctxt, raw_props) =
     9.5    let
     9.6      val thy = ProofContext.theory_of ctxt;
     9.7 -    val ss = Simplifier.get_local_simpset ctxt;
     9.8 +    val ss = local_simpset_of ctxt;
     9.9      val cprops = map (Thm.cterm_of (Theory.sign_of thy) o ProofContext.read_prop ctxt) raw_props;
    9.10    in Method.erule 0 (map (smart_mk_cases thy ss) cprops) end;
    9.11  
    10.1 --- a/src/HOL/Tools/meson.ML	Fri Jul 09 16:33:20 2004 +0200
    10.2 +++ b/src/HOL/Tools/meson.ML	Sun Jul 11 20:33:22 2004 +0200
    10.3 @@ -419,7 +419,7 @@
    10.4  
    10.5  fun meson_meth ctxt =
    10.6    Method.SIMPLE_METHOD' HEADGOAL
    10.7 -    (CHANGED_PROP o meson_claset_tac (Classical.get_local_claset ctxt));
    10.8 +    (CHANGED_PROP o meson_claset_tac (local_claset_of ctxt));
    10.9  
   10.10  val skolemize_meth =
   10.11    Method.SIMPLE_METHOD' HEADGOAL
    11.1 --- a/src/HOL/Tools/recdef_package.ML	Fri Jul 09 16:33:20 2004 +0200
    11.2 +++ b/src/HOL/Tools/recdef_package.ML	Sun Jul 11 20:33:22 2004 +0200
    11.3 @@ -213,13 +213,15 @@
    11.4          None => ctxt0
    11.5        | Some src => Method.only_sectioned_args recdef_modifiers I src ctxt0);
    11.6      val {simps, congs, wfs} = get_local_hints ctxt;
    11.7 -    val cs = Classical.get_local_claset ctxt;
    11.8 -    val ss = Simplifier.get_local_simpset ctxt addsimps simps;
    11.9 +    val cs = local_claset_of ctxt;
   11.10 +    val ss = local_simpset_of ctxt addsimps simps;
   11.11    in (cs, ss, map #2 congs, wfs) end;
   11.12  
   11.13  fun prepare_hints_i thy () =
   11.14 -  let val {simps, congs, wfs} = get_global_hints thy
   11.15 -  in (Classical.claset_of thy, Simplifier.simpset_of thy addsimps simps, map #2 congs, wfs) end;
   11.16 +  let
   11.17 +    val ctxt0 = ProofContext.init thy;
   11.18 +    val {simps, congs, wfs} = get_global_hints thy;
   11.19 +  in (local_claset_of ctxt0, local_simpset_of ctxt0 addsimps simps, map #2 congs, wfs) end;
   11.20  
   11.21  
   11.22  
    12.1 --- a/src/HOL/UNITY/Simple/NSP_Bad.thy	Fri Jul 09 16:33:20 2004 +0200
    12.2 +++ b/src/HOL/UNITY/Simple/NSP_Bad.thy	Sun Jul 11 20:33:22 2004 +0200
    12.3 @@ -130,8 +130,7 @@
    12.4  method_setup ns_induct = {*
    12.5      Method.ctxt_args (fn ctxt =>
    12.6          Method.METHOD (fn facts =>
    12.7 -            ns_induct_tac (Classical.get_local_claset ctxt,
    12.8 -                               Simplifier.get_local_simpset ctxt) 1)) *}
    12.9 +            ns_induct_tac (local_clasimpset_of ctxt) 1)) *}
   12.10      "for inductive reasoning about the Needham-Schroeder protocol"
   12.11  
   12.12  text{*Converts invariants into statements about reachable states*}
    13.1 --- a/src/HOL/UNITY/UNITY_Main.thy	Fri Jul 09 16:33:20 2004 +0200
    13.2 +++ b/src/HOL/UNITY/UNITY_Main.thy	Sun Jul 11 20:33:22 2004 +0200
    13.3 @@ -12,15 +12,13 @@
    13.4  method_setup constrains = {*
    13.5      Method.ctxt_args (fn ctxt =>
    13.6          Method.METHOD (fn facts => 
    13.7 -            gen_constrains_tac (Classical.get_local_claset ctxt,
    13.8 -                               Simplifier.get_local_simpset ctxt) 1)) *}
    13.9 +            gen_constrains_tac (local_clasimpset_of ctxt) 1)) *}
   13.10      "for proving safety properties"
   13.11  
   13.12  method_setup ensures_tac = {*
   13.13      fn args => fn ctxt =>
   13.14          Method.goal_args' (Scan.lift Args.name) 
   13.15 -           (gen_ensures_tac (Classical.get_local_claset ctxt,
   13.16 -                               Simplifier.get_local_simpset ctxt))
   13.17 +           (gen_ensures_tac (local_clasimpset_of ctxt))
   13.18             args ctxt *}
   13.19      "for proving progress properties"
   13.20  
    14.1 --- a/src/Provers/clasimp.ML	Fri Jul 09 16:33:20 2004 +0200
    14.2 +++ b/src/Provers/clasimp.ML	Sun Jul 11 20:33:22 2004 +0200
    14.3 @@ -61,6 +61,7 @@
    14.4    val change_global_css: (clasimpset * thm list -> clasimpset) -> theory attribute
    14.5    val change_local_css: (clasimpset * thm list -> clasimpset) -> Proof.context attribute
    14.6    val get_local_clasimpset: Proof.context -> clasimpset
    14.7 +  val local_clasimpset_of: Proof.context -> clasimpset
    14.8    val iff_add_global: theory attribute
    14.9    val iff_add_global': theory attribute
   14.10    val iff_del_global: theory attribute
   14.11 @@ -276,6 +277,9 @@
   14.12  fun get_local_clasimpset ctxt =
   14.13    (Classical.get_local_claset ctxt, Simplifier.get_local_simpset ctxt);
   14.14  
   14.15 +fun local_clasimpset_of ctxt =
   14.16 +  (Classical.local_claset_of ctxt, Simplifier.local_simpset_of ctxt);
   14.17 +
   14.18  
   14.19  (* attributes *)
   14.20  
   14.21 @@ -315,10 +319,10 @@
   14.22  (* methods *)
   14.23  
   14.24  fun clasimp_meth tac prems ctxt = Method.METHOD (fn facts =>
   14.25 -  ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (get_local_clasimpset ctxt));
   14.26 +  ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (local_clasimpset_of ctxt));
   14.27  
   14.28  fun clasimp_meth' tac prems ctxt = Method.METHOD (fn facts =>
   14.29 -  HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_clasimpset ctxt)));
   14.30 +  HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (local_clasimpset_of ctxt)));
   14.31  
   14.32  val clasimp_method = Method.bang_sectioned_args clasimp_modifiers o clasimp_meth;
   14.33  val clasimp_method' = Method.bang_sectioned_args clasimp_modifiers o clasimp_meth';
    15.1 --- a/src/ZF/Tools/ind_cases.ML	Fri Jul 09 16:33:20 2004 +0200
    15.2 +++ b/src/ZF/Tools/ind_cases.ML	Sun Jul 11 20:33:22 2004 +0200
    15.3 @@ -63,7 +63,7 @@
    15.4  
    15.5  fun mk_cases_meth (ctxt, props) =
    15.6    props
    15.7 -  |> map (smart_cases (ProofContext.theory_of ctxt) (Simplifier.get_local_simpset ctxt)
    15.8 +  |> map (smart_cases (ProofContext.theory_of ctxt) (local_simpset_of ctxt)
    15.9      (ProofContext.read_prop ctxt))
   15.10    |> Method.erule 0;
   15.11  
    16.1 --- a/src/ZF/UNITY/ClientImpl.thy	Fri Jul 09 16:33:20 2004 +0200
    16.2 +++ b/src/ZF/UNITY/ClientImpl.thy	Sun Jul 11 20:33:22 2004 +0200
    16.3 @@ -13,8 +13,7 @@
    16.4  method_setup constrains = {*
    16.5      Method.ctxt_args (fn ctxt =>
    16.6          Method.METHOD (fn facts =>
    16.7 -            gen_constrains_tac (Classical.get_local_claset ctxt,
    16.8 -                               Simplifier.get_local_simpset ctxt) 1)) *}
    16.9 +            gen_constrains_tac (local_clasimpset_of ctxt) 1)) *}
   16.10      "for proving safety properties"
   16.11  
   16.12  consts