src/Provers/classical.ML
changeset 42793 88bee9f6eec7
parent 42792 85fb70b0c5e8
child 42798 02c88bdabe75
--- a/src/Provers/classical.ML	Fri May 13 16:03:03 2011 +0200
+++ b/src/Provers/classical.ML	Fri May 13 22:55:00 2011 +0200
@@ -37,30 +37,29 @@
 sig
   type claset
   val empty_cs: claset
-  val print_cs: Proof.context -> claset -> unit
   val rep_cs: claset ->
    {safeIs: thm list,
     safeEs: thm list,
     hazIs: thm list,
     hazEs: thm list,
-    swrappers: (string * wrapper) list,
-    uwrappers: (string * wrapper) list,
+    swrappers: (string * (Proof.context -> wrapper)) list,
+    uwrappers: (string * (Proof.context -> wrapper)) list,
     safe0_netpair: netpair,
     safep_netpair: netpair,
     haz_netpair: netpair,
     dup_netpair: netpair,
     xtra_netpair: Context_Rules.netpair}
-  val merge_cs: claset * claset -> claset
-  val addDs: claset * thm list -> claset
-  val addEs: claset * thm list -> claset
-  val addIs: claset * thm list -> claset
-  val addSDs: claset * thm list -> claset
-  val addSEs: claset * thm list -> claset
-  val addSIs: claset * thm list -> claset
-  val delrules: claset * thm list -> claset
-  val addSWrapper: claset * (string * wrapper) -> claset
+  val print_claset: Proof.context -> unit
+  val addDs: Proof.context * thm list -> Proof.context
+  val addEs: Proof.context * thm list -> Proof.context
+  val addIs: Proof.context * thm list -> Proof.context
+  val addSDs: Proof.context * thm list -> Proof.context
+  val addSEs: Proof.context * thm list -> Proof.context
+  val addSIs: Proof.context * thm list -> Proof.context
+  val delrules: Proof.context * thm list -> Proof.context
+  val addSWrapper: claset * (string * (Proof.context -> wrapper)) -> claset
   val delSWrapper: claset *  string -> claset
-  val addWrapper: claset * (string * wrapper) -> claset
+  val addWrapper: claset * (string * (Proof.context -> wrapper)) -> claset
   val delWrapper: claset *  string -> claset
   val addSbefore: claset * (string * (int -> tactic)) -> claset
   val addSafter: claset * (string * (int -> tactic)) -> claset
@@ -70,54 +69,50 @@
   val addE2: claset * (string * thm) -> claset
   val addSD2: claset * (string * thm) -> claset
   val addSE2: claset * (string * thm) -> claset
-  val appSWrappers: claset -> wrapper
-  val appWrappers: claset -> wrapper
+  val appSWrappers: Proof.context -> wrapper
+  val appWrappers: Proof.context -> wrapper
 
   val global_claset_of: theory -> claset
   val claset_of: Proof.context -> claset
+  val map_claset: (claset -> claset) -> Proof.context -> Proof.context
+  val put_claset: claset -> Proof.context -> Proof.context
 
-  val fast_tac: claset -> int -> tactic
-  val slow_tac: claset -> int -> tactic
-  val astar_tac: claset -> int -> tactic
-  val slow_astar_tac: claset -> int -> tactic
-  val best_tac: claset -> int -> tactic
-  val first_best_tac: claset -> int -> tactic
-  val slow_best_tac: claset -> int -> tactic
-  val depth_tac: claset -> int -> int -> tactic
-  val deepen_tac: claset -> int -> int -> tactic
+  val fast_tac: Proof.context -> int -> tactic
+  val slow_tac: Proof.context -> int -> tactic
+  val astar_tac: Proof.context -> int -> tactic
+  val slow_astar_tac: Proof.context -> int -> tactic
+  val best_tac: Proof.context -> int -> tactic
+  val first_best_tac: Proof.context -> int -> tactic
+  val slow_best_tac: Proof.context -> int -> tactic
+  val depth_tac: Proof.context -> int -> int -> tactic
+  val deepen_tac: Proof.context -> int -> int -> tactic
 
   val contr_tac: int -> tactic
   val dup_elim: thm -> thm
   val dup_intr: thm -> thm
-  val dup_step_tac: claset -> int -> tactic
+  val dup_step_tac: Proof.context -> int -> tactic
   val eq_mp_tac: int -> tactic
-  val haz_step_tac: claset -> int -> tactic
+  val haz_step_tac: Proof.context -> int -> tactic
   val joinrules: thm list * thm list -> (bool * thm) list
   val mp_tac: int -> tactic
-  val safe_tac: claset -> tactic
-  val safe_steps_tac: claset -> int -> tactic
-  val safe_step_tac: claset -> int -> tactic
-  val clarify_tac: claset -> int -> tactic
-  val clarify_step_tac: claset -> int -> tactic
-  val step_tac: claset -> int -> tactic
-  val slow_step_tac: claset -> int -> tactic
+  val safe_tac: Proof.context -> tactic
+  val safe_steps_tac: Proof.context -> int -> tactic
+  val safe_step_tac: Proof.context -> int -> tactic
+  val clarify_tac: Proof.context -> int -> tactic
+  val clarify_step_tac: Proof.context -> int -> tactic
+  val step_tac: Proof.context -> int -> tactic
+  val slow_step_tac: Proof.context -> int -> tactic
   val swapify: thm list -> thm list
   val swap_res_tac: thm list -> int -> tactic
-  val inst_step_tac: claset -> int -> tactic
-  val inst0_step_tac: claset -> int -> tactic
-  val instp_step_tac: claset -> int -> tactic
+  val inst_step_tac: Proof.context -> int -> tactic
+  val inst0_step_tac: Proof.context -> int -> tactic
+  val instp_step_tac: Proof.context -> int -> tactic
 end;
 
 signature CLASSICAL =
 sig
   include BASIC_CLASSICAL
   val classical_rule: thm -> thm
-  val add_context_safe_wrapper: string * (Proof.context -> wrapper) -> theory -> theory
-  val del_context_safe_wrapper: string -> theory -> theory
-  val add_context_unsafe_wrapper: string * (Proof.context -> wrapper) -> theory -> theory
-  val del_context_unsafe_wrapper: string -> theory -> theory
-  val get_claset: Proof.context -> claset
-  val put_claset: claset -> Proof.context -> Proof.context
   val get_cs: Context.generic -> claset
   val map_cs: (claset -> claset) -> Context.generic -> Context.generic
   val safe_dest: int option -> attribute
@@ -128,10 +123,10 @@
   val haz_intro: int option -> attribute
   val rule_del: attribute
   val cla_modifiers: Method.modifier parser list
-  val cla_meth: (claset -> tactic) -> Proof.context -> Proof.method
-  val cla_meth': (claset -> int -> tactic) -> Proof.context -> Proof.method
-  val cla_method: (claset -> tactic) -> (Proof.context -> Proof.method) context_parser
-  val cla_method': (claset -> int -> tactic) -> (Proof.context -> Proof.method) context_parser
+  val cla_method:
+    (Proof.context -> tactic) -> (Proof.context -> Proof.method) context_parser
+  val cla_method':
+    (Proof.context -> int -> tactic) -> (Proof.context -> Proof.method) context_parser
   val setup: theory -> theory
 end;
 
@@ -208,7 +203,7 @@
 (*Duplication of hazardous rules, for complete provers*)
 fun dup_intr th = zero_var_indexes (th RS Data.classical);
 
-fun dup_elim th =
+fun dup_elim th =  (* FIXME proper context!? *)
   let
     val rl = (th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd;
     val ctxt = Proof_Context.init_global (Thm.theory_of_thm rl);
@@ -218,17 +213,18 @@
 (**** Classical rule sets ****)
 
 datatype claset =
-  CS of {safeIs         : thm list,                (*safe introduction rules*)
-         safeEs         : thm list,                (*safe elimination rules*)
-         hazIs          : thm list,                (*unsafe introduction rules*)
-         hazEs          : thm list,                (*unsafe elimination rules*)
-         swrappers      : (string * wrapper) list, (*for transforming safe_step_tac*)
-         uwrappers      : (string * wrapper) list, (*for transforming step_tac*)
-         safe0_netpair  : netpair,                 (*nets for trivial cases*)
-         safep_netpair  : netpair,                 (*nets for >0 subgoals*)
-         haz_netpair    : netpair,                 (*nets for unsafe rules*)
-         dup_netpair    : netpair,                 (*nets for duplication*)
-         xtra_netpair   : Context_Rules.netpair};  (*nets for extra rules*)
+  CS of
+   {safeIs         : thm list,                (*safe introduction rules*)
+    safeEs         : thm list,                (*safe elimination rules*)
+    hazIs          : thm list,                (*unsafe introduction rules*)
+    hazEs          : thm list,                (*unsafe elimination rules*)
+    swrappers      : (string * (Proof.context -> wrapper)) list, (*for transforming safe_step_tac*)
+    uwrappers      : (string * (Proof.context -> wrapper)) list, (*for transforming step_tac*)
+    safe0_netpair  : netpair,                 (*nets for trivial cases*)
+    safep_netpair  : netpair,                 (*nets for >0 subgoals*)
+    haz_netpair    : netpair,                 (*nets for unsafe rules*)
+    dup_netpair    : netpair,                 (*nets for duplication*)
+    xtra_netpair   : Context_Rules.netpair};  (*nets for extra rules*)
 
 (*Desired invariants are
         safe0_netpair = build safe0_brls,
@@ -247,34 +243,21 @@
 val empty_netpair = (Net.empty, Net.empty);
 
 val empty_cs =
-  CS{safeIs     = [],
-     safeEs     = [],
-     hazIs      = [],
-     hazEs      = [],
-     swrappers  = [],
-     uwrappers  = [],
-     safe0_netpair = empty_netpair,
-     safep_netpair = empty_netpair,
-     haz_netpair   = empty_netpair,
-     dup_netpair   = empty_netpair,
-     xtra_netpair  = empty_netpair};
-
-fun print_cs ctxt (CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, ...}) =
-  let val pretty_thms = map (Display.pretty_thm ctxt) in
-    [Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs),
-      Pretty.big_list "introduction rules (intro):" (pretty_thms hazIs),
-      Pretty.big_list "safe elimination rules (elim!):" (pretty_thms safeEs),
-      Pretty.big_list "elimination rules (elim):" (pretty_thms hazEs),
-      Pretty.strs ("safe wrappers:" :: map #1 swrappers),
-      Pretty.strs ("unsafe wrappers:" :: map #1 uwrappers)]
-    |> Pretty.chunks |> Pretty.writeln
-  end;
+  CS
+   {safeIs = [],
+    safeEs = [],
+    hazIs = [],
+    hazEs = [],
+    swrappers = [],
+    uwrappers = [],
+    safe0_netpair = empty_netpair,
+    safep_netpair = empty_netpair,
+    haz_netpair = empty_netpair,
+    dup_netpair = empty_netpair,
+    xtra_netpair = empty_netpair};
 
 fun rep_cs (CS args) = args;
 
-fun appSWrappers (CS {swrappers, ...}) = fold snd swrappers;
-fun appWrappers  (CS {uwrappers, ...}) = fold snd uwrappers;
-
 
 (*** Adding (un)safe introduction or elimination rules.
 
@@ -314,22 +297,31 @@
 val mem_thm = member Thm.eq_thm_prop
 and rem_thm = remove Thm.eq_thm_prop;
 
-fun warn msg rules th =
-  mem_thm rules th andalso (warning (msg ^ Display.string_of_thm_without_context th); true);
+fun string_of_thm NONE = Display.string_of_thm_without_context
+  | string_of_thm (SOME context) =
+      Display.string_of_thm (Context.cases Syntax.init_pretty_global I context);
+
+fun make_elim context th =
+  if has_fewer_prems 1 th then
+    error ("Ill-formed destruction rule\n" ^ string_of_thm context th)
+  else Tactic.make_elim th;
 
-fun warn_other th (CS{safeIs, safeEs, hazIs, hazEs, ...}) =
-  warn "Rule already declared as safe introduction (intro!)\n" safeIs th orelse
-  warn "Rule already declared as safe elimination (elim!)\n" safeEs th orelse
-  warn "Rule already declared as introduction (intro)\n" hazIs th orelse
-  warn "Rule already declared as elimination (elim)\n" hazEs th;
+fun warn context msg rules th =
+  mem_thm rules th andalso (warning (msg ^ string_of_thm context th); true);
+
+fun warn_other context th (CS{safeIs, safeEs, hazIs, hazEs, ...}) =
+  warn context "Rule already declared as safe introduction (intro!)\n" safeIs th orelse
+  warn context "Rule already declared as safe elimination (elim!)\n" safeEs th orelse
+  warn context "Rule already declared as introduction (intro)\n" hazIs th orelse
+  warn context "Rule already declared as elimination (elim)\n" hazEs th;
 
 
 (*** Safe rules ***)
 
-fun addSI w th
+fun addSI w context th
     (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
       safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
-  if warn "Ignoring duplicate safe introduction (intro!)\n" safeIs th then cs
+  if warn context "Ignoring duplicate safe introduction (intro!)\n" safeIs th then cs
   else
     let
       val th' = flat_rule th;
@@ -337,7 +329,7 @@
         List.partition Thm.no_prems [th'];
       val nI = length safeIs + 1;
       val nE = length safeEs;
-      val _ = warn_other th cs;
+      val _ = warn_other context th cs;
     in
       CS
        {safeIs  = th::safeIs,
@@ -353,12 +345,12 @@
         xtra_netpair = insert' (the_default 0 w) (nI,nE) ([th], []) xtra_netpair}
     end;
 
-fun addSE w th
+fun addSE w context th
     (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
       safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
-  if warn "Ignoring duplicate safe elimination (elim!)\n" safeEs th then cs
+  if warn context "Ignoring duplicate safe elimination (elim!)\n" safeEs th then cs
   else if has_fewer_prems 1 th then
-    error ("Ill-formed elimination rule\n" ^ Display.string_of_thm_without_context th)
+    error ("Ill-formed elimination rule\n" ^ string_of_thm context th)
   else
     let
       val th' = classical_rule (flat_rule th);
@@ -366,7 +358,7 @@
         List.partition (fn rl => nprems_of rl=1) [th'];
       val nI = length safeIs;
       val nE = length safeEs + 1;
-      val _ = warn_other th cs;
+      val _ = warn_other context th cs;
     in
       CS
        {safeEs  = th::safeEs,
@@ -382,19 +374,21 @@
         xtra_netpair = insert' (the_default 0 w) (nI,nE) ([], [th]) xtra_netpair}
     end;
 
+fun addSD w context th = addSE w context (make_elim context th);
+
 
 (*** Hazardous (unsafe) rules ***)
 
-fun addI w th
+fun addI w context th
     (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
       safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
-  if warn "Ignoring duplicate introduction (intro)\n" hazIs th then cs
+  if warn context "Ignoring duplicate introduction (intro)\n" hazIs th then cs
   else
     let
       val th' = flat_rule th;
       val nI = length hazIs + 1;
       val nE = length hazEs;
-      val _ = warn_other th cs;
+      val _ = warn_other context th cs;
     in
       CS
        {hazIs = th :: hazIs,
@@ -410,20 +404,20 @@
         xtra_netpair = insert' (the_default 1 w) (nI, nE) ([th], []) xtra_netpair}
     end
     handle THM ("RSN: no unifiers", _, _) => (*from dup_intr*)  (* FIXME !? *)
-      error ("Ill-formed introduction rule\n" ^ Display.string_of_thm_without_context th);
+      error ("Ill-formed introduction rule\n" ^ string_of_thm context th);
 
-fun addE w th
+fun addE w context th
     (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
       safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
-  if warn "Ignoring duplicate elimination (elim)\n" hazEs th then cs
+  if warn context "Ignoring duplicate elimination (elim)\n" hazEs th then cs
   else if has_fewer_prems 1 th then
-    error ("Ill-formed elimination rule\n" ^ Display.string_of_thm_without_context th)
+    error ("Ill-formed elimination rule\n" ^ string_of_thm context th)
   else
     let
       val th' = classical_rule (flat_rule th);
       val nI = length hazIs;
       val nE = length hazEs + 1;
-      val _ = warn_other th cs;
+      val _ = warn_other context th cs;
     in
       CS
        {hazEs = th :: hazEs,
@@ -439,6 +433,8 @@
         xtra_netpair = insert' (the_default 1 w) (nI, nE) ([], [th]) xtra_netpair}
     end;
 
+fun addD w context th = addE w context (make_elim context th);
+
 
 
 (*** Deletion of rules
@@ -492,7 +488,7 @@
     end
   else cs;
 
-fun delI th
+fun delI context th
     (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
       safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   if mem_thm hazIs th then
@@ -512,7 +508,7 @@
     end
   else cs
   handle THM ("RSN: no unifiers", _, _) => (*from dup_intr*)  (* FIXME !? *)
-    error ("Ill-formed introduction rule\n" ^ Display.string_of_thm_without_context th);
+    error ("Ill-formed introduction rule\n" ^ string_of_thm context th);
 
 fun delE th
     (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
@@ -535,32 +531,21 @@
   else cs;
 
 (*Delete ALL occurrences of "th" in the claset (perhaps from several lists)*)
-fun delrule th (cs as CS {safeIs, safeEs, hazIs, hazEs, ...}) =
-  let val th' = Tactic.make_elim th (* FIXME classical make_elim!? *) in
+fun delrule context th (cs as CS {safeIs, safeEs, hazIs, hazEs, ...}) =
+  let val th' = Tactic.make_elim th in
     if mem_thm safeIs th orelse mem_thm safeEs th orelse
       mem_thm hazIs th orelse mem_thm hazEs th orelse
       mem_thm safeEs th' orelse mem_thm hazEs th'
-    then delSI th (delSE th (delI th (delE th (delSE th' (delE th' cs)))))
-    else (warning ("Undeclared classical rule\n" ^ Display.string_of_thm_without_context th); cs)
+    then delSI th (delSE th (delI context th (delE th (delSE th' (delE th' cs)))))
+    else (warning ("Undeclared classical rule\n" ^ string_of_thm context th); cs)
   end;
 
-fun cs delrules ths = fold delrule ths cs;
-
 
-fun make_elim th =
-  if has_fewer_prems 1 th then
-    error ("Ill-formed destruction rule\n" ^ Display.string_of_thm_without_context th)
-  else Tactic.make_elim th;
+
+(** claset data **)
 
-fun cs addSIs ths = fold_rev (addSI NONE) ths cs;
-fun cs addSEs ths = fold_rev (addSE NONE) ths cs;
-fun cs addSDs ths = cs addSEs (map make_elim ths);
-fun cs addIs ths = fold_rev (addI NONE) ths cs;
-fun cs addEs ths = fold_rev (addE NONE) ths cs;
-fun cs addDs ths = cs addEs (map make_elim ths);
+(* wrappers *)
 
-
-(*** Modifying the wrapper tacticals ***)
 fun map_swrappers f
   (CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
     safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
@@ -570,48 +555,15 @@
     haz_netpair = haz_netpair, dup_netpair = dup_netpair, xtra_netpair = xtra_netpair};
 
 fun map_uwrappers f
-  (CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
+  (CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
     safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   CS {safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs,
     swrappers = swrappers, uwrappers = f uwrappers,
     safe0_netpair = safe0_netpair, safep_netpair = safep_netpair,
     haz_netpair = haz_netpair, dup_netpair = dup_netpair, xtra_netpair = xtra_netpair};
 
-fun update_warn msg (p as (key : string, _)) xs =
-  (if AList.defined (op =) xs key then warning msg else (); AList.update (op =) p xs);
 
-fun delete_warn msg (key : string) xs =
-  if AList.defined (op =) xs key then AList.delete (op =) key xs
-  else (warning msg; xs);
-
-(*Add/replace a safe wrapper*)
-fun cs addSWrapper new_swrapper = map_swrappers
-  (update_warn ("Overwriting safe wrapper " ^ fst new_swrapper) new_swrapper) cs;
-
-(*Add/replace an unsafe wrapper*)
-fun cs addWrapper new_uwrapper = map_uwrappers
-  (update_warn ("Overwriting unsafe wrapper " ^ fst new_uwrapper) new_uwrapper) cs;
-
-(*Remove a safe wrapper*)
-fun cs delSWrapper name = map_swrappers
-  (delete_warn ("No such safe wrapper in claset: " ^ name) name) cs;
-
-(*Remove an unsafe wrapper*)
-fun cs delWrapper name = map_uwrappers
-  (delete_warn ("No such unsafe wrapper in claset: " ^ name) name) cs;
-
-(* compose a safe tactic alternatively before/after safe_step_tac *)
-fun cs addSbefore (name, tac1) = cs addSWrapper (name, fn tac2 => tac1 ORELSE' tac2);
-fun cs addSafter (name, tac2) = cs addSWrapper (name, fn tac1 => tac1 ORELSE' tac2);
-
-(*compose a tactic alternatively before/after the step tactic *)
-fun cs addbefore (name, tac1) = cs addWrapper (name, fn tac2 => tac1 APPEND' tac2);
-fun cs addafter (name, tac2) = cs addWrapper (name, fn tac1 => tac1 APPEND' tac2);
-
-fun cs addD2 (name, thm) = cs addafter (name, datac thm 1);
-fun cs addE2 (name, thm) = cs addafter (name, eatac thm 1);
-fun cs addSD2 (name, thm) = cs addSafter (name, dmatch_tac [thm] THEN' eq_assume_tac);
-fun cs addSE2 (name, thm) = cs addSafter (name, ematch_tac [thm] THEN' eq_assume_tac);
+(* merge_cs *)
 
 (*Merge works by adding all new rules of the 2nd claset into the 1st claset.
   Merging the term nets may look more efficient, but the rather delicate
@@ -626,29 +578,129 @@
       val safeEs' = fold rem_thm safeEs safeEs2;
       val hazIs' = fold rem_thm hazIs hazIs2;
       val hazEs' = fold rem_thm hazEs hazEs2;
-      val cs1 = cs addSIs safeIs' addSEs safeEs' addIs hazIs' addEs hazEs';
-      val cs2 = map_swrappers (fn ws => AList.merge (op =) (K true) (ws, swrappers)) cs1;
-      val cs3 = map_uwrappers (fn ws => AList.merge (op =) (K true) (ws, uwrappers)) cs2;
-    in cs3 end;
+    in
+      cs
+      |> fold_rev (addSI NONE NONE) safeIs'
+      |> fold_rev (addSE NONE NONE) safeEs'
+      |> fold_rev (addI NONE NONE) hazIs'
+      |> fold_rev (addE NONE NONE) hazEs'
+      |> map_swrappers (fn ws => AList.merge (op =) (K true) (ws, swrappers))
+      |> map_uwrappers (fn ws => AList.merge (op =) (K true) (ws, uwrappers))
+    end;
+
+
+(* data *)
+
+structure Claset = Generic_Data
+(
+  type T = claset;
+  val empty = empty_cs;
+  val extend = I;
+  val merge = merge_cs;
+);
+
+val global_claset_of = Claset.get o Context.Theory;
+val claset_of = Claset.get o Context.Proof;
+val rep_claset_of = rep_cs o claset_of;
+
+val get_cs = Claset.get;
+val map_cs = Claset.map;
+
+fun map_claset f = Context.proof_map (map_cs f);
+fun put_claset cs = map_claset (K cs);
+
+fun print_claset ctxt =
+  let
+    val {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, ...} = rep_claset_of ctxt;
+    val pretty_thms = map (Display.pretty_thm ctxt);
+  in
+    [Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs),
+      Pretty.big_list "introduction rules (intro):" (pretty_thms hazIs),
+      Pretty.big_list "safe elimination rules (elim!):" (pretty_thms safeEs),
+      Pretty.big_list "elimination rules (elim):" (pretty_thms hazEs),
+      Pretty.strs ("safe wrappers:" :: map #1 swrappers),
+      Pretty.strs ("unsafe wrappers:" :: map #1 uwrappers)]
+    |> Pretty.chunks |> Pretty.writeln
+  end;
+
+
+(* old-style declarations *)
+
+fun decl f (ctxt, ths) = map_claset (fold_rev (f (SOME (Context.Proof ctxt))) ths) ctxt;
+
+val op addSIs = decl (addSI NONE);
+val op addSEs = decl (addSE NONE);
+val op addSDs = decl (addSD NONE);
+val op addIs = decl (addI NONE);
+val op addEs = decl (addE NONE);
+val op addDs = decl (addD NONE);
+val op delrules = decl delrule;
+
+
+
+(*** Modifying the wrapper tacticals ***)
+
+fun appSWrappers ctxt = fold (fn (_, w) => w ctxt) (#swrappers (rep_claset_of ctxt));
+fun appWrappers ctxt = fold (fn (_, w) => w ctxt) (#uwrappers (rep_claset_of ctxt));
+
+fun update_warn msg (p as (key : string, _)) xs =
+  (if AList.defined (op =) xs key then warning msg else (); AList.update (op =) p xs);
+
+fun delete_warn msg (key : string) xs =
+  if AList.defined (op =) xs key then AList.delete (op =) key xs
+  else (warning msg; xs);
+
+(*Add/replace a safe wrapper*)
+fun cs addSWrapper new_swrapper =
+  map_swrappers (update_warn ("Overwriting safe wrapper " ^ fst new_swrapper) new_swrapper) cs;
+
+(*Add/replace an unsafe wrapper*)
+fun cs addWrapper new_uwrapper =
+  map_uwrappers (update_warn ("Overwriting unsafe wrapper " ^ fst new_uwrapper) new_uwrapper) cs;
+
+(*Remove a safe wrapper*)
+fun cs delSWrapper name =
+  map_swrappers (delete_warn ("No such safe wrapper in claset: " ^ name) name) cs;
+
+(*Remove an unsafe wrapper*)
+fun cs delWrapper name =
+  map_uwrappers (delete_warn ("No such unsafe wrapper in claset: " ^ name) name) cs;
+
+(* compose a safe tactic alternatively before/after safe_step_tac *)
+fun cs addSbefore (name, tac1) = cs addSWrapper (name, fn _ => fn tac2 => tac1 ORELSE' tac2);
+fun cs addSafter (name, tac2) = cs addSWrapper (name, fn _ => fn tac1 => tac1 ORELSE' tac2);
+
+(*compose a tactic alternatively before/after the step tactic *)
+fun cs addbefore (name, tac1) = cs addWrapper (name, fn _ => fn tac2 => tac1 APPEND' tac2);
+fun cs addafter (name, tac2) = cs addWrapper (name, fn _ => fn tac1 => tac1 APPEND' tac2);
+
+fun cs addD2 (name, thm) = cs addafter (name, datac thm 1);
+fun cs addE2 (name, thm) = cs addafter (name, eatac thm 1);
+fun cs addSD2 (name, thm) = cs addSafter (name, dmatch_tac [thm] THEN' eq_assume_tac);
+fun cs addSE2 (name, thm) = cs addSafter (name, ematch_tac [thm] THEN' eq_assume_tac);
+
 
 
 (**** Simple tactics for theorem proving ****)
 
 (*Attack subgoals using safe inferences -- matching, not resolution*)
-fun safe_step_tac (cs as CS {safe0_netpair, safep_netpair, ...}) =
-  appSWrappers cs (FIRST' [
-        eq_assume_tac,
+fun safe_step_tac ctxt =
+  let val {safe0_netpair, safep_netpair, ...} = rep_claset_of ctxt in
+    appSWrappers ctxt
+      (FIRST'
+       [eq_assume_tac,
         eq_mp_tac,
         bimatch_from_nets_tac safe0_netpair,
         FIRST' Data.hyp_subst_tacs,
-        bimatch_from_nets_tac safep_netpair]);
+        bimatch_from_nets_tac safep_netpair])
+  end;
 
 (*Repeatedly attack a subgoal using safe inferences -- it's deterministic!*)
-fun safe_steps_tac cs =
-  REPEAT_DETERM1 o (fn i => COND (has_fewer_prems i) no_tac (safe_step_tac cs i));
+fun safe_steps_tac ctxt =
+  REPEAT_DETERM1 o (fn i => COND (has_fewer_prems i) no_tac (safe_step_tac ctxt i));
 
 (*Repeatedly attack subgoals using safe inferences -- it's deterministic!*)
-fun safe_tac cs = REPEAT_DETERM1 (FIRSTGOAL (safe_steps_tac cs));
+fun safe_tac ctxt = REPEAT_DETERM1 (FIRSTGOAL (safe_steps_tac ctxt));
 
 
 (*** Clarify_tac: do safe steps without causing branching ***)
@@ -669,86 +721,89 @@
   (eq_assume_contr_tac i ORELSE eq_assume_contr_tac (i + 1));
 
 (*Attack subgoals using safe inferences -- matching, not resolution*)
-fun clarify_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) =
-  appSWrappers cs (FIRST' [
-        eq_assume_contr_tac,
+fun clarify_step_tac ctxt =
+  let val {safe0_netpair, safep_netpair, ...} = rep_claset_of ctxt in
+    appSWrappers ctxt
+     (FIRST'
+       [eq_assume_contr_tac,
         bimatch_from_nets_tac safe0_netpair,
         FIRST' Data.hyp_subst_tacs,
         n_bimatch_from_nets_tac 1 safep_netpair,
-        bimatch2_tac safep_netpair]);
+        bimatch2_tac safep_netpair])
+  end;
 
-fun clarify_tac cs = SELECT_GOAL (REPEAT_DETERM (clarify_step_tac cs 1));
+fun clarify_tac ctxt = SELECT_GOAL (REPEAT_DETERM (clarify_step_tac ctxt 1));
 
 
 (*** Unsafe steps instantiate variables or lose information ***)
 
 (*Backtracking is allowed among the various these unsafe ways of
   proving a subgoal.  *)
-fun inst0_step_tac (CS {safe0_netpair, ...}) =
+fun inst0_step_tac ctxt =
   assume_tac APPEND'
   contr_tac APPEND'
-  biresolve_from_nets_tac safe0_netpair;
+  biresolve_from_nets_tac (#safe0_netpair (rep_claset_of ctxt));
 
 (*These unsafe steps could generate more subgoals.*)
-fun instp_step_tac (CS {safep_netpair, ...}) =
-  biresolve_from_nets_tac safep_netpair;
+fun instp_step_tac ctxt =
+  biresolve_from_nets_tac (#safep_netpair (rep_claset_of ctxt));
 
 (*These steps could instantiate variables and are therefore unsafe.*)
-fun inst_step_tac cs = inst0_step_tac cs APPEND' instp_step_tac cs;
+fun inst_step_tac ctxt = inst0_step_tac ctxt APPEND' instp_step_tac ctxt;
 
-fun haz_step_tac (CS{haz_netpair,...}) =
-  biresolve_from_nets_tac haz_netpair;
+fun haz_step_tac ctxt =
+  biresolve_from_nets_tac (#haz_netpair (rep_claset_of ctxt));
 
 (*Single step for the prover.  FAILS unless it makes progress. *)
-fun step_tac cs i =
-  safe_tac cs ORELSE appWrappers cs (inst_step_tac cs ORELSE' haz_step_tac cs) i;
+fun step_tac ctxt i =
+  safe_tac ctxt ORELSE appWrappers ctxt (inst_step_tac ctxt ORELSE' haz_step_tac ctxt) i;
 
 (*Using a "safe" rule to instantiate variables is unsafe.  This tactic
   allows backtracking from "safe" rules to "unsafe" rules here.*)
-fun slow_step_tac cs i =
-  safe_tac cs ORELSE appWrappers cs (inst_step_tac cs APPEND' haz_step_tac cs) i;
+fun slow_step_tac ctxt i =
+  safe_tac ctxt ORELSE appWrappers ctxt (inst_step_tac ctxt APPEND' haz_step_tac ctxt) i;
 
 
 (**** The following tactics all fail unless they solve one goal ****)
 
 (*Dumb but fast*)
-fun fast_tac cs =
-  Object_Logic.atomize_prems_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1));
+fun fast_tac ctxt =
+  Object_Logic.atomize_prems_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt 1));
 
 (*Slower but smarter than fast_tac*)
-fun best_tac cs =
+fun best_tac ctxt =
   Object_Logic.atomize_prems_tac THEN'
-  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (step_tac cs 1));
+  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (step_tac ctxt 1));
 
 (*even a bit smarter than best_tac*)
-fun first_best_tac cs =
+fun first_best_tac ctxt =
   Object_Logic.atomize_prems_tac THEN'
-  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (FIRSTGOAL (step_tac cs)));
+  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (FIRSTGOAL (step_tac ctxt)));
 
-fun slow_tac cs =
+fun slow_tac ctxt =
   Object_Logic.atomize_prems_tac THEN'
-  SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1));
+  SELECT_GOAL (DEPTH_SOLVE (slow_step_tac ctxt 1));
 
-fun slow_best_tac cs =
+fun slow_best_tac ctxt =
   Object_Logic.atomize_prems_tac THEN'
-  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (slow_step_tac cs 1));
+  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (slow_step_tac ctxt 1));
 
 
 (***ASTAR with weight weight_ASTAR, by Norbert Voelker*)
 
 val weight_ASTAR = 5;
 
-fun astar_tac cs =
+fun astar_tac ctxt =
   Object_Logic.atomize_prems_tac THEN'
   SELECT_GOAL
     (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + weight_ASTAR * lev)
-      (step_tac cs 1));
+      (step_tac ctxt 1));
 
-fun slow_astar_tac cs =
+fun slow_astar_tac ctxt =
   Object_Logic.atomize_prems_tac THEN'
   SELECT_GOAL
     (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + weight_ASTAR * lev)
-      (slow_step_tac cs 1));
+      (slow_step_tac ctxt 1));
 
 
 (**** Complete tactic, loosely based upon LeanTaP.  This tactic is the outcome
@@ -759,132 +814,44 @@
 (*Non-deterministic!  Could always expand the first unsafe connective.
   That's hard to implement and did not perform better in experiments, due to
   greater search depth required.*)
-fun dup_step_tac (CS {dup_netpair, ...}) =
-  biresolve_from_nets_tac dup_netpair;
+fun dup_step_tac ctxt =
+  biresolve_from_nets_tac (#dup_netpair (rep_claset_of ctxt));
 
 (*Searching to depth m. A variant called nodup_depth_tac appears in clasimp.ML*)
 local
-  fun slow_step_tac' cs = appWrappers cs (instp_step_tac cs APPEND' dup_step_tac cs);
+  fun slow_step_tac' ctxt = appWrappers ctxt (instp_step_tac ctxt APPEND' dup_step_tac ctxt);
 in
-  fun depth_tac cs m i state = SELECT_GOAL
-    (safe_steps_tac cs 1 THEN_ELSE
-      (DEPTH_SOLVE (depth_tac cs m 1),
-        inst0_step_tac cs 1 APPEND COND (K (m = 0)) no_tac
-          (slow_step_tac' cs 1 THEN DEPTH_SOLVE (depth_tac cs (m - 1) 1)))) i state;
+  fun depth_tac ctxt m i state = SELECT_GOAL
+    (safe_steps_tac ctxt 1 THEN_ELSE
+      (DEPTH_SOLVE (depth_tac ctxt m 1),
+        inst0_step_tac ctxt 1 APPEND COND (K (m = 0)) no_tac
+          (slow_step_tac' ctxt 1 THEN DEPTH_SOLVE (depth_tac ctxt (m - 1) 1)))) i state;
 end;
 
 (*Search, with depth bound m.
   This is the "entry point", which does safe inferences first.*)
-fun safe_depth_tac cs m = SUBGOAL (fn (prem,i) =>
-  let val deti =
-      (*No Vars in the goal?  No need to backtrack between goals.*)
-    if exists_subterm (fn Var _ => true | _ => false) prem then DETERM else I
+fun safe_depth_tac ctxt m = SUBGOAL (fn (prem, i) =>
+  let
+    val deti = (*No Vars in the goal?  No need to backtrack between goals.*)
+      if exists_subterm (fn Var _ => true | _ => false) prem then DETERM else I;
   in
-    SELECT_GOAL (TRY (safe_tac cs) THEN DEPTH_SOLVE (deti (depth_tac cs m 1))) i
+    SELECT_GOAL (TRY (safe_tac ctxt) THEN DEPTH_SOLVE (deti (depth_tac ctxt m 1))) i
   end);
 
-fun deepen_tac cs = DEEPEN (2, 10) (safe_depth_tac cs);
-
-
-
-(** context dependent claset components **)
-
-datatype context_cs = ContextCS of
- {swrappers: (string * (Proof.context -> wrapper)) list,
-  uwrappers: (string * (Proof.context -> wrapper)) list};
-
-fun context_cs ctxt cs (ContextCS {swrappers, uwrappers}) =
-  let
-    fun add_wrapper add (name, f) claset = add (claset, (name, f ctxt));
-  in
-    cs
-    |> fold_rev (add_wrapper (op addSWrapper)) swrappers
-    |> fold_rev (add_wrapper (op addWrapper)) uwrappers
-  end;
-
-fun make_context_cs (swrappers, uwrappers) =
-  ContextCS {swrappers = swrappers, uwrappers = uwrappers};
-
-val empty_context_cs = make_context_cs ([], []);
-
-fun merge_context_cs (ctxt_cs1, ctxt_cs2) =
-  if pointer_eq (ctxt_cs1, ctxt_cs2) then ctxt_cs1
-  else
-    let
-      val ContextCS {swrappers = swrappers1, uwrappers = uwrappers1} = ctxt_cs1;
-      val ContextCS {swrappers = swrappers2, uwrappers = uwrappers2} = ctxt_cs2;
-      val swrappers' = AList.merge (op =) (K true) (swrappers1, swrappers2);
-      val uwrappers' = AList.merge (op =) (K true) (uwrappers1, uwrappers2);
-    in make_context_cs (swrappers', uwrappers') end;
-
-
-
-(** claset data **)
-
-(* global clasets *)
-
-structure GlobalClaset = Theory_Data
-(
-  type T = claset * context_cs;
-  val empty = (empty_cs, empty_context_cs);
-  val extend = I;
-  fun merge ((cs1, ctxt_cs1), (cs2, ctxt_cs2)) =
-    (merge_cs (cs1, cs2), merge_context_cs (ctxt_cs1, ctxt_cs2));
-);
-
-val get_global_claset = #1 o GlobalClaset.get;
-val map_global_claset = GlobalClaset.map o apfst;
-
-val get_context_cs = #2 o GlobalClaset.get o Proof_Context.theory_of;
-fun map_context_cs f = GlobalClaset.map (apsnd
-  (fn ContextCS {swrappers, uwrappers} => make_context_cs (f (swrappers, uwrappers))));
-
-fun global_claset_of thy =
-  let val (cs, ctxt_cs) = GlobalClaset.get thy
-  in context_cs (Proof_Context.init_global thy) cs (ctxt_cs) end;
-
-
-(* context dependent components *)
-
-fun add_context_safe_wrapper wrapper = map_context_cs (apfst ((AList.update (op =) wrapper)));
-fun del_context_safe_wrapper name = map_context_cs (apfst ((AList.delete (op =) name)));
-
-fun add_context_unsafe_wrapper wrapper = map_context_cs (apsnd ((AList.update (op =) wrapper)));
-fun del_context_unsafe_wrapper name = map_context_cs (apsnd ((AList.delete (op =) name)));
-
-
-(* local clasets *)
-
-structure LocalClaset = Proof_Data
-(
-  type T = claset;
-  val init = get_global_claset;
-);
-
-val get_claset = LocalClaset.get;
-val put_claset = LocalClaset.put;
-
-fun claset_of ctxt =
-  context_cs ctxt (LocalClaset.get ctxt) (get_context_cs ctxt);
-
-
-(* generic clasets *)
-
-val get_cs = Context.cases global_claset_of claset_of;
-fun map_cs f = Context.mapping (map_global_claset f) (LocalClaset.map f);
+fun deepen_tac ctxt = DEEPEN (2, 10) (safe_depth_tac ctxt);
 
 
 (* attributes *)
 
-fun attrib f = Thm.declaration_attribute (fn th =>
-  Context.mapping (map_global_claset (f th)) (LocalClaset.map (f th)));
+fun attrib f =
+  Thm.declaration_attribute (fn th => fn context => map_cs (f (SOME context) th) context);
 
-fun safe_dest w = attrib (addSE w o make_elim);
 val safe_elim = attrib o addSE;
 val safe_intro = attrib o addSI;
-fun haz_dest w = attrib (addE w o make_elim);
+val safe_dest = attrib o addSD;
 val haz_elim = attrib o addE;
 val haz_intro = attrib o addI;
+val haz_dest = attrib o addD;
 val rule_del = attrib delrule o Context_Rules.rule_del;
 
 
@@ -916,7 +883,7 @@
 fun some_rule_tac ctxt facts = SUBGOAL (fn (goal, i) =>
   let
     val [rules1, rules2, rules4] = Context_Rules.find_rules false facts goal ctxt;
-    val CS {xtra_netpair, ...} = claset_of ctxt;
+    val {xtra_netpair, ...} = rep_claset_of ctxt;
     val rules3 = Context_Rules.find_rules_netpair true facts goal xtra_netpair;
     val rules = rules1 @ rules2 @ rules3 @ rules4;
     val ruleq = Drule.multi_resolves facts rules;
@@ -954,14 +921,8 @@
   Args.$$$ introN -- Args.colon >> K (I, haz_intro NONE),
   Args.del -- Args.colon >> K (I, rule_del)];
 
-fun cla_meth tac ctxt = METHOD (fn facts =>
-  ALLGOALS (Method.insert_tac facts) THEN tac (claset_of ctxt));
-
-fun cla_meth' tac ctxt = METHOD (fn facts =>
-  HEADGOAL (Method.insert_tac facts THEN' tac (claset_of ctxt)));
-
-fun cla_method tac = Method.sections cla_modifiers >> K (cla_meth tac);
-fun cla_method' tac = Method.sections cla_modifiers >> K (cla_meth' tac);
+fun cla_method tac = Method.sections cla_modifiers >> K (SIMPLE_METHOD o tac);
+fun cla_method' tac = Method.sections cla_modifiers >> K (SIMPLE_METHOD' o tac);
 
 
 
@@ -981,7 +942,7 @@
   Method.setup @{binding fast} (cla_method' fast_tac) "classical prover (depth-first)" #>
   Method.setup @{binding slow} (cla_method' slow_tac) "classical prover (slow depth-first)" #>
   Method.setup @{binding best} (cla_method' best_tac) "classical prover (best-first)" #>
-  Method.setup @{binding deepen} (cla_method' (fn cs => deepen_tac cs 4))
+  Method.setup @{binding deepen} (cla_method' (fn ctxt => deepen_tac ctxt 4))
     "classical prover (iterative deepening)" #>
   Method.setup @{binding safe} (cla_method (CHANGED_PROP o safe_tac))
     "classical prover (apply safe rules)";
@@ -1002,6 +963,6 @@
     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
       Toplevel.keep (fn state =>
         let val ctxt = Toplevel.context_of state
-        in print_cs ctxt (claset_of ctxt) end)));
+        in print_claset ctxt end)));
 
 end;