src/Provers/classical.ML
changeset 42793 88bee9f6eec7
parent 42792 85fb70b0c5e8
child 42798 02c88bdabe75
     1.1 --- a/src/Provers/classical.ML	Fri May 13 16:03:03 2011 +0200
     1.2 +++ b/src/Provers/classical.ML	Fri May 13 22:55:00 2011 +0200
     1.3 @@ -37,30 +37,29 @@
     1.4  sig
     1.5    type claset
     1.6    val empty_cs: claset
     1.7 -  val print_cs: Proof.context -> claset -> unit
     1.8    val rep_cs: claset ->
     1.9     {safeIs: thm list,
    1.10      safeEs: thm list,
    1.11      hazIs: thm list,
    1.12      hazEs: thm list,
    1.13 -    swrappers: (string * wrapper) list,
    1.14 -    uwrappers: (string * wrapper) list,
    1.15 +    swrappers: (string * (Proof.context -> wrapper)) list,
    1.16 +    uwrappers: (string * (Proof.context -> wrapper)) list,
    1.17      safe0_netpair: netpair,
    1.18      safep_netpair: netpair,
    1.19      haz_netpair: netpair,
    1.20      dup_netpair: netpair,
    1.21      xtra_netpair: Context_Rules.netpair}
    1.22 -  val merge_cs: claset * claset -> claset
    1.23 -  val addDs: claset * thm list -> claset
    1.24 -  val addEs: claset * thm list -> claset
    1.25 -  val addIs: claset * thm list -> claset
    1.26 -  val addSDs: claset * thm list -> claset
    1.27 -  val addSEs: claset * thm list -> claset
    1.28 -  val addSIs: claset * thm list -> claset
    1.29 -  val delrules: claset * thm list -> claset
    1.30 -  val addSWrapper: claset * (string * wrapper) -> claset
    1.31 +  val print_claset: Proof.context -> unit
    1.32 +  val addDs: Proof.context * thm list -> Proof.context
    1.33 +  val addEs: Proof.context * thm list -> Proof.context
    1.34 +  val addIs: Proof.context * thm list -> Proof.context
    1.35 +  val addSDs: Proof.context * thm list -> Proof.context
    1.36 +  val addSEs: Proof.context * thm list -> Proof.context
    1.37 +  val addSIs: Proof.context * thm list -> Proof.context
    1.38 +  val delrules: Proof.context * thm list -> Proof.context
    1.39 +  val addSWrapper: claset * (string * (Proof.context -> wrapper)) -> claset
    1.40    val delSWrapper: claset *  string -> claset
    1.41 -  val addWrapper: claset * (string * wrapper) -> claset
    1.42 +  val addWrapper: claset * (string * (Proof.context -> wrapper)) -> claset
    1.43    val delWrapper: claset *  string -> claset
    1.44    val addSbefore: claset * (string * (int -> tactic)) -> claset
    1.45    val addSafter: claset * (string * (int -> tactic)) -> claset
    1.46 @@ -70,54 +69,50 @@
    1.47    val addE2: claset * (string * thm) -> claset
    1.48    val addSD2: claset * (string * thm) -> claset
    1.49    val addSE2: claset * (string * thm) -> claset
    1.50 -  val appSWrappers: claset -> wrapper
    1.51 -  val appWrappers: claset -> wrapper
    1.52 +  val appSWrappers: Proof.context -> wrapper
    1.53 +  val appWrappers: Proof.context -> wrapper
    1.54  
    1.55    val global_claset_of: theory -> claset
    1.56    val claset_of: Proof.context -> claset
    1.57 +  val map_claset: (claset -> claset) -> Proof.context -> Proof.context
    1.58 +  val put_claset: claset -> Proof.context -> Proof.context
    1.59  
    1.60 -  val fast_tac: claset -> int -> tactic
    1.61 -  val slow_tac: claset -> int -> tactic
    1.62 -  val astar_tac: claset -> int -> tactic
    1.63 -  val slow_astar_tac: claset -> int -> tactic
    1.64 -  val best_tac: claset -> int -> tactic
    1.65 -  val first_best_tac: claset -> int -> tactic
    1.66 -  val slow_best_tac: claset -> int -> tactic
    1.67 -  val depth_tac: claset -> int -> int -> tactic
    1.68 -  val deepen_tac: claset -> int -> int -> tactic
    1.69 +  val fast_tac: Proof.context -> int -> tactic
    1.70 +  val slow_tac: Proof.context -> int -> tactic
    1.71 +  val astar_tac: Proof.context -> int -> tactic
    1.72 +  val slow_astar_tac: Proof.context -> int -> tactic
    1.73 +  val best_tac: Proof.context -> int -> tactic
    1.74 +  val first_best_tac: Proof.context -> int -> tactic
    1.75 +  val slow_best_tac: Proof.context -> int -> tactic
    1.76 +  val depth_tac: Proof.context -> int -> int -> tactic
    1.77 +  val deepen_tac: Proof.context -> int -> int -> tactic
    1.78  
    1.79    val contr_tac: int -> tactic
    1.80    val dup_elim: thm -> thm
    1.81    val dup_intr: thm -> thm
    1.82 -  val dup_step_tac: claset -> int -> tactic
    1.83 +  val dup_step_tac: Proof.context -> int -> tactic
    1.84    val eq_mp_tac: int -> tactic
    1.85 -  val haz_step_tac: claset -> int -> tactic
    1.86 +  val haz_step_tac: Proof.context -> int -> tactic
    1.87    val joinrules: thm list * thm list -> (bool * thm) list
    1.88    val mp_tac: int -> tactic
    1.89 -  val safe_tac: claset -> tactic
    1.90 -  val safe_steps_tac: claset -> int -> tactic
    1.91 -  val safe_step_tac: claset -> int -> tactic
    1.92 -  val clarify_tac: claset -> int -> tactic
    1.93 -  val clarify_step_tac: claset -> int -> tactic
    1.94 -  val step_tac: claset -> int -> tactic
    1.95 -  val slow_step_tac: claset -> int -> tactic
    1.96 +  val safe_tac: Proof.context -> tactic
    1.97 +  val safe_steps_tac: Proof.context -> int -> tactic
    1.98 +  val safe_step_tac: Proof.context -> int -> tactic
    1.99 +  val clarify_tac: Proof.context -> int -> tactic
   1.100 +  val clarify_step_tac: Proof.context -> int -> tactic
   1.101 +  val step_tac: Proof.context -> int -> tactic
   1.102 +  val slow_step_tac: Proof.context -> int -> tactic
   1.103    val swapify: thm list -> thm list
   1.104    val swap_res_tac: thm list -> int -> tactic
   1.105 -  val inst_step_tac: claset -> int -> tactic
   1.106 -  val inst0_step_tac: claset -> int -> tactic
   1.107 -  val instp_step_tac: claset -> int -> tactic
   1.108 +  val inst_step_tac: Proof.context -> int -> tactic
   1.109 +  val inst0_step_tac: Proof.context -> int -> tactic
   1.110 +  val instp_step_tac: Proof.context -> int -> tactic
   1.111  end;
   1.112  
   1.113  signature CLASSICAL =
   1.114  sig
   1.115    include BASIC_CLASSICAL
   1.116    val classical_rule: thm -> thm
   1.117 -  val add_context_safe_wrapper: string * (Proof.context -> wrapper) -> theory -> theory
   1.118 -  val del_context_safe_wrapper: string -> theory -> theory
   1.119 -  val add_context_unsafe_wrapper: string * (Proof.context -> wrapper) -> theory -> theory
   1.120 -  val del_context_unsafe_wrapper: string -> theory -> theory
   1.121 -  val get_claset: Proof.context -> claset
   1.122 -  val put_claset: claset -> Proof.context -> Proof.context
   1.123    val get_cs: Context.generic -> claset
   1.124    val map_cs: (claset -> claset) -> Context.generic -> Context.generic
   1.125    val safe_dest: int option -> attribute
   1.126 @@ -128,10 +123,10 @@
   1.127    val haz_intro: int option -> attribute
   1.128    val rule_del: attribute
   1.129    val cla_modifiers: Method.modifier parser list
   1.130 -  val cla_meth: (claset -> tactic) -> Proof.context -> Proof.method
   1.131 -  val cla_meth': (claset -> int -> tactic) -> Proof.context -> Proof.method
   1.132 -  val cla_method: (claset -> tactic) -> (Proof.context -> Proof.method) context_parser
   1.133 -  val cla_method': (claset -> int -> tactic) -> (Proof.context -> Proof.method) context_parser
   1.134 +  val cla_method:
   1.135 +    (Proof.context -> tactic) -> (Proof.context -> Proof.method) context_parser
   1.136 +  val cla_method':
   1.137 +    (Proof.context -> int -> tactic) -> (Proof.context -> Proof.method) context_parser
   1.138    val setup: theory -> theory
   1.139  end;
   1.140  
   1.141 @@ -208,7 +203,7 @@
   1.142  (*Duplication of hazardous rules, for complete provers*)
   1.143  fun dup_intr th = zero_var_indexes (th RS Data.classical);
   1.144  
   1.145 -fun dup_elim th =
   1.146 +fun dup_elim th =  (* FIXME proper context!? *)
   1.147    let
   1.148      val rl = (th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd;
   1.149      val ctxt = Proof_Context.init_global (Thm.theory_of_thm rl);
   1.150 @@ -218,17 +213,18 @@
   1.151  (**** Classical rule sets ****)
   1.152  
   1.153  datatype claset =
   1.154 -  CS of {safeIs         : thm list,                (*safe introduction rules*)
   1.155 -         safeEs         : thm list,                (*safe elimination rules*)
   1.156 -         hazIs          : thm list,                (*unsafe introduction rules*)
   1.157 -         hazEs          : thm list,                (*unsafe elimination rules*)
   1.158 -         swrappers      : (string * wrapper) list, (*for transforming safe_step_tac*)
   1.159 -         uwrappers      : (string * wrapper) list, (*for transforming step_tac*)
   1.160 -         safe0_netpair  : netpair,                 (*nets for trivial cases*)
   1.161 -         safep_netpair  : netpair,                 (*nets for >0 subgoals*)
   1.162 -         haz_netpair    : netpair,                 (*nets for unsafe rules*)
   1.163 -         dup_netpair    : netpair,                 (*nets for duplication*)
   1.164 -         xtra_netpair   : Context_Rules.netpair};  (*nets for extra rules*)
   1.165 +  CS of
   1.166 +   {safeIs         : thm list,                (*safe introduction rules*)
   1.167 +    safeEs         : thm list,                (*safe elimination rules*)
   1.168 +    hazIs          : thm list,                (*unsafe introduction rules*)
   1.169 +    hazEs          : thm list,                (*unsafe elimination rules*)
   1.170 +    swrappers      : (string * (Proof.context -> wrapper)) list, (*for transforming safe_step_tac*)
   1.171 +    uwrappers      : (string * (Proof.context -> wrapper)) list, (*for transforming step_tac*)
   1.172 +    safe0_netpair  : netpair,                 (*nets for trivial cases*)
   1.173 +    safep_netpair  : netpair,                 (*nets for >0 subgoals*)
   1.174 +    haz_netpair    : netpair,                 (*nets for unsafe rules*)
   1.175 +    dup_netpair    : netpair,                 (*nets for duplication*)
   1.176 +    xtra_netpair   : Context_Rules.netpair};  (*nets for extra rules*)
   1.177  
   1.178  (*Desired invariants are
   1.179          safe0_netpair = build safe0_brls,
   1.180 @@ -247,34 +243,21 @@
   1.181  val empty_netpair = (Net.empty, Net.empty);
   1.182  
   1.183  val empty_cs =
   1.184 -  CS{safeIs     = [],
   1.185 -     safeEs     = [],
   1.186 -     hazIs      = [],
   1.187 -     hazEs      = [],
   1.188 -     swrappers  = [],
   1.189 -     uwrappers  = [],
   1.190 -     safe0_netpair = empty_netpair,
   1.191 -     safep_netpair = empty_netpair,
   1.192 -     haz_netpair   = empty_netpair,
   1.193 -     dup_netpair   = empty_netpair,
   1.194 -     xtra_netpair  = empty_netpair};
   1.195 -
   1.196 -fun print_cs ctxt (CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, ...}) =
   1.197 -  let val pretty_thms = map (Display.pretty_thm ctxt) in
   1.198 -    [Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs),
   1.199 -      Pretty.big_list "introduction rules (intro):" (pretty_thms hazIs),
   1.200 -      Pretty.big_list "safe elimination rules (elim!):" (pretty_thms safeEs),
   1.201 -      Pretty.big_list "elimination rules (elim):" (pretty_thms hazEs),
   1.202 -      Pretty.strs ("safe wrappers:" :: map #1 swrappers),
   1.203 -      Pretty.strs ("unsafe wrappers:" :: map #1 uwrappers)]
   1.204 -    |> Pretty.chunks |> Pretty.writeln
   1.205 -  end;
   1.206 +  CS
   1.207 +   {safeIs = [],
   1.208 +    safeEs = [],
   1.209 +    hazIs = [],
   1.210 +    hazEs = [],
   1.211 +    swrappers = [],
   1.212 +    uwrappers = [],
   1.213 +    safe0_netpair = empty_netpair,
   1.214 +    safep_netpair = empty_netpair,
   1.215 +    haz_netpair = empty_netpair,
   1.216 +    dup_netpair = empty_netpair,
   1.217 +    xtra_netpair = empty_netpair};
   1.218  
   1.219  fun rep_cs (CS args) = args;
   1.220  
   1.221 -fun appSWrappers (CS {swrappers, ...}) = fold snd swrappers;
   1.222 -fun appWrappers  (CS {uwrappers, ...}) = fold snd uwrappers;
   1.223 -
   1.224  
   1.225  (*** Adding (un)safe introduction or elimination rules.
   1.226  
   1.227 @@ -314,22 +297,31 @@
   1.228  val mem_thm = member Thm.eq_thm_prop
   1.229  and rem_thm = remove Thm.eq_thm_prop;
   1.230  
   1.231 -fun warn msg rules th =
   1.232 -  mem_thm rules th andalso (warning (msg ^ Display.string_of_thm_without_context th); true);
   1.233 +fun string_of_thm NONE = Display.string_of_thm_without_context
   1.234 +  | string_of_thm (SOME context) =
   1.235 +      Display.string_of_thm (Context.cases Syntax.init_pretty_global I context);
   1.236 +
   1.237 +fun make_elim context th =
   1.238 +  if has_fewer_prems 1 th then
   1.239 +    error ("Ill-formed destruction rule\n" ^ string_of_thm context th)
   1.240 +  else Tactic.make_elim th;
   1.241  
   1.242 -fun warn_other th (CS{safeIs, safeEs, hazIs, hazEs, ...}) =
   1.243 -  warn "Rule already declared as safe introduction (intro!)\n" safeIs th orelse
   1.244 -  warn "Rule already declared as safe elimination (elim!)\n" safeEs th orelse
   1.245 -  warn "Rule already declared as introduction (intro)\n" hazIs th orelse
   1.246 -  warn "Rule already declared as elimination (elim)\n" hazEs th;
   1.247 +fun warn context msg rules th =
   1.248 +  mem_thm rules th andalso (warning (msg ^ string_of_thm context th); true);
   1.249 +
   1.250 +fun warn_other context th (CS{safeIs, safeEs, hazIs, hazEs, ...}) =
   1.251 +  warn context "Rule already declared as safe introduction (intro!)\n" safeIs th orelse
   1.252 +  warn context "Rule already declared as safe elimination (elim!)\n" safeEs th orelse
   1.253 +  warn context "Rule already declared as introduction (intro)\n" hazIs th orelse
   1.254 +  warn context "Rule already declared as elimination (elim)\n" hazEs th;
   1.255  
   1.256  
   1.257  (*** Safe rules ***)
   1.258  
   1.259 -fun addSI w th
   1.260 +fun addSI w context th
   1.261      (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   1.262        safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   1.263 -  if warn "Ignoring duplicate safe introduction (intro!)\n" safeIs th then cs
   1.264 +  if warn context "Ignoring duplicate safe introduction (intro!)\n" safeIs th then cs
   1.265    else
   1.266      let
   1.267        val th' = flat_rule th;
   1.268 @@ -337,7 +329,7 @@
   1.269          List.partition Thm.no_prems [th'];
   1.270        val nI = length safeIs + 1;
   1.271        val nE = length safeEs;
   1.272 -      val _ = warn_other th cs;
   1.273 +      val _ = warn_other context th cs;
   1.274      in
   1.275        CS
   1.276         {safeIs  = th::safeIs,
   1.277 @@ -353,12 +345,12 @@
   1.278          xtra_netpair = insert' (the_default 0 w) (nI,nE) ([th], []) xtra_netpair}
   1.279      end;
   1.280  
   1.281 -fun addSE w th
   1.282 +fun addSE w context th
   1.283      (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   1.284        safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   1.285 -  if warn "Ignoring duplicate safe elimination (elim!)\n" safeEs th then cs
   1.286 +  if warn context "Ignoring duplicate safe elimination (elim!)\n" safeEs th then cs
   1.287    else if has_fewer_prems 1 th then
   1.288 -    error ("Ill-formed elimination rule\n" ^ Display.string_of_thm_without_context th)
   1.289 +    error ("Ill-formed elimination rule\n" ^ string_of_thm context th)
   1.290    else
   1.291      let
   1.292        val th' = classical_rule (flat_rule th);
   1.293 @@ -366,7 +358,7 @@
   1.294          List.partition (fn rl => nprems_of rl=1) [th'];
   1.295        val nI = length safeIs;
   1.296        val nE = length safeEs + 1;
   1.297 -      val _ = warn_other th cs;
   1.298 +      val _ = warn_other context th cs;
   1.299      in
   1.300        CS
   1.301         {safeEs  = th::safeEs,
   1.302 @@ -382,19 +374,21 @@
   1.303          xtra_netpair = insert' (the_default 0 w) (nI,nE) ([], [th]) xtra_netpair}
   1.304      end;
   1.305  
   1.306 +fun addSD w context th = addSE w context (make_elim context th);
   1.307 +
   1.308  
   1.309  (*** Hazardous (unsafe) rules ***)
   1.310  
   1.311 -fun addI w th
   1.312 +fun addI w context th
   1.313      (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   1.314        safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   1.315 -  if warn "Ignoring duplicate introduction (intro)\n" hazIs th then cs
   1.316 +  if warn context "Ignoring duplicate introduction (intro)\n" hazIs th then cs
   1.317    else
   1.318      let
   1.319        val th' = flat_rule th;
   1.320        val nI = length hazIs + 1;
   1.321        val nE = length hazEs;
   1.322 -      val _ = warn_other th cs;
   1.323 +      val _ = warn_other context th cs;
   1.324      in
   1.325        CS
   1.326         {hazIs = th :: hazIs,
   1.327 @@ -410,20 +404,20 @@
   1.328          xtra_netpair = insert' (the_default 1 w) (nI, nE) ([th], []) xtra_netpair}
   1.329      end
   1.330      handle THM ("RSN: no unifiers", _, _) => (*from dup_intr*)  (* FIXME !? *)
   1.331 -      error ("Ill-formed introduction rule\n" ^ Display.string_of_thm_without_context th);
   1.332 +      error ("Ill-formed introduction rule\n" ^ string_of_thm context th);
   1.333  
   1.334 -fun addE w th
   1.335 +fun addE w context th
   1.336      (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   1.337        safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   1.338 -  if warn "Ignoring duplicate elimination (elim)\n" hazEs th then cs
   1.339 +  if warn context "Ignoring duplicate elimination (elim)\n" hazEs th then cs
   1.340    else if has_fewer_prems 1 th then
   1.341 -    error ("Ill-formed elimination rule\n" ^ Display.string_of_thm_without_context th)
   1.342 +    error ("Ill-formed elimination rule\n" ^ string_of_thm context th)
   1.343    else
   1.344      let
   1.345        val th' = classical_rule (flat_rule th);
   1.346        val nI = length hazIs;
   1.347        val nE = length hazEs + 1;
   1.348 -      val _ = warn_other th cs;
   1.349 +      val _ = warn_other context th cs;
   1.350      in
   1.351        CS
   1.352         {hazEs = th :: hazEs,
   1.353 @@ -439,6 +433,8 @@
   1.354          xtra_netpair = insert' (the_default 1 w) (nI, nE) ([], [th]) xtra_netpair}
   1.355      end;
   1.356  
   1.357 +fun addD w context th = addE w context (make_elim context th);
   1.358 +
   1.359  
   1.360  
   1.361  (*** Deletion of rules
   1.362 @@ -492,7 +488,7 @@
   1.363      end
   1.364    else cs;
   1.365  
   1.366 -fun delI th
   1.367 +fun delI context th
   1.368      (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   1.369        safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   1.370    if mem_thm hazIs th then
   1.371 @@ -512,7 +508,7 @@
   1.372      end
   1.373    else cs
   1.374    handle THM ("RSN: no unifiers", _, _) => (*from dup_intr*)  (* FIXME !? *)
   1.375 -    error ("Ill-formed introduction rule\n" ^ Display.string_of_thm_without_context th);
   1.376 +    error ("Ill-formed introduction rule\n" ^ string_of_thm context th);
   1.377  
   1.378  fun delE th
   1.379      (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   1.380 @@ -535,32 +531,21 @@
   1.381    else cs;
   1.382  
   1.383  (*Delete ALL occurrences of "th" in the claset (perhaps from several lists)*)
   1.384 -fun delrule th (cs as CS {safeIs, safeEs, hazIs, hazEs, ...}) =
   1.385 -  let val th' = Tactic.make_elim th (* FIXME classical make_elim!? *) in
   1.386 +fun delrule context th (cs as CS {safeIs, safeEs, hazIs, hazEs, ...}) =
   1.387 +  let val th' = Tactic.make_elim th in
   1.388      if mem_thm safeIs th orelse mem_thm safeEs th orelse
   1.389        mem_thm hazIs th orelse mem_thm hazEs th orelse
   1.390        mem_thm safeEs th' orelse mem_thm hazEs th'
   1.391 -    then delSI th (delSE th (delI th (delE th (delSE th' (delE th' cs)))))
   1.392 -    else (warning ("Undeclared classical rule\n" ^ Display.string_of_thm_without_context th); cs)
   1.393 +    then delSI th (delSE th (delI context th (delE th (delSE th' (delE th' cs)))))
   1.394 +    else (warning ("Undeclared classical rule\n" ^ string_of_thm context th); cs)
   1.395    end;
   1.396  
   1.397 -fun cs delrules ths = fold delrule ths cs;
   1.398 -
   1.399  
   1.400 -fun make_elim th =
   1.401 -  if has_fewer_prems 1 th then
   1.402 -    error ("Ill-formed destruction rule\n" ^ Display.string_of_thm_without_context th)
   1.403 -  else Tactic.make_elim th;
   1.404 +
   1.405 +(** claset data **)
   1.406  
   1.407 -fun cs addSIs ths = fold_rev (addSI NONE) ths cs;
   1.408 -fun cs addSEs ths = fold_rev (addSE NONE) ths cs;
   1.409 -fun cs addSDs ths = cs addSEs (map make_elim ths);
   1.410 -fun cs addIs ths = fold_rev (addI NONE) ths cs;
   1.411 -fun cs addEs ths = fold_rev (addE NONE) ths cs;
   1.412 -fun cs addDs ths = cs addEs (map make_elim ths);
   1.413 +(* wrappers *)
   1.414  
   1.415 -
   1.416 -(*** Modifying the wrapper tacticals ***)
   1.417  fun map_swrappers f
   1.418    (CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   1.419      safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   1.420 @@ -570,48 +555,15 @@
   1.421      haz_netpair = haz_netpair, dup_netpair = dup_netpair, xtra_netpair = xtra_netpair};
   1.422  
   1.423  fun map_uwrappers f
   1.424 -  (CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   1.425 +  (CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
   1.426      safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   1.427    CS {safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs,
   1.428      swrappers = swrappers, uwrappers = f uwrappers,
   1.429      safe0_netpair = safe0_netpair, safep_netpair = safep_netpair,
   1.430      haz_netpair = haz_netpair, dup_netpair = dup_netpair, xtra_netpair = xtra_netpair};
   1.431  
   1.432 -fun update_warn msg (p as (key : string, _)) xs =
   1.433 -  (if AList.defined (op =) xs key then warning msg else (); AList.update (op =) p xs);
   1.434  
   1.435 -fun delete_warn msg (key : string) xs =
   1.436 -  if AList.defined (op =) xs key then AList.delete (op =) key xs
   1.437 -  else (warning msg; xs);
   1.438 -
   1.439 -(*Add/replace a safe wrapper*)
   1.440 -fun cs addSWrapper new_swrapper = map_swrappers
   1.441 -  (update_warn ("Overwriting safe wrapper " ^ fst new_swrapper) new_swrapper) cs;
   1.442 -
   1.443 -(*Add/replace an unsafe wrapper*)
   1.444 -fun cs addWrapper new_uwrapper = map_uwrappers
   1.445 -  (update_warn ("Overwriting unsafe wrapper " ^ fst new_uwrapper) new_uwrapper) cs;
   1.446 -
   1.447 -(*Remove a safe wrapper*)
   1.448 -fun cs delSWrapper name = map_swrappers
   1.449 -  (delete_warn ("No such safe wrapper in claset: " ^ name) name) cs;
   1.450 -
   1.451 -(*Remove an unsafe wrapper*)
   1.452 -fun cs delWrapper name = map_uwrappers
   1.453 -  (delete_warn ("No such unsafe wrapper in claset: " ^ name) name) cs;
   1.454 -
   1.455 -(* compose a safe tactic alternatively before/after safe_step_tac *)
   1.456 -fun cs addSbefore (name, tac1) = cs addSWrapper (name, fn tac2 => tac1 ORELSE' tac2);
   1.457 -fun cs addSafter (name, tac2) = cs addSWrapper (name, fn tac1 => tac1 ORELSE' tac2);
   1.458 -
   1.459 -(*compose a tactic alternatively before/after the step tactic *)
   1.460 -fun cs addbefore (name, tac1) = cs addWrapper (name, fn tac2 => tac1 APPEND' tac2);
   1.461 -fun cs addafter (name, tac2) = cs addWrapper (name, fn tac1 => tac1 APPEND' tac2);
   1.462 -
   1.463 -fun cs addD2 (name, thm) = cs addafter (name, datac thm 1);
   1.464 -fun cs addE2 (name, thm) = cs addafter (name, eatac thm 1);
   1.465 -fun cs addSD2 (name, thm) = cs addSafter (name, dmatch_tac [thm] THEN' eq_assume_tac);
   1.466 -fun cs addSE2 (name, thm) = cs addSafter (name, ematch_tac [thm] THEN' eq_assume_tac);
   1.467 +(* merge_cs *)
   1.468  
   1.469  (*Merge works by adding all new rules of the 2nd claset into the 1st claset.
   1.470    Merging the term nets may look more efficient, but the rather delicate
   1.471 @@ -626,29 +578,129 @@
   1.472        val safeEs' = fold rem_thm safeEs safeEs2;
   1.473        val hazIs' = fold rem_thm hazIs hazIs2;
   1.474        val hazEs' = fold rem_thm hazEs hazEs2;
   1.475 -      val cs1 = cs addSIs safeIs' addSEs safeEs' addIs hazIs' addEs hazEs';
   1.476 -      val cs2 = map_swrappers (fn ws => AList.merge (op =) (K true) (ws, swrappers)) cs1;
   1.477 -      val cs3 = map_uwrappers (fn ws => AList.merge (op =) (K true) (ws, uwrappers)) cs2;
   1.478 -    in cs3 end;
   1.479 +    in
   1.480 +      cs
   1.481 +      |> fold_rev (addSI NONE NONE) safeIs'
   1.482 +      |> fold_rev (addSE NONE NONE) safeEs'
   1.483 +      |> fold_rev (addI NONE NONE) hazIs'
   1.484 +      |> fold_rev (addE NONE NONE) hazEs'
   1.485 +      |> map_swrappers (fn ws => AList.merge (op =) (K true) (ws, swrappers))
   1.486 +      |> map_uwrappers (fn ws => AList.merge (op =) (K true) (ws, uwrappers))
   1.487 +    end;
   1.488 +
   1.489 +
   1.490 +(* data *)
   1.491 +
   1.492 +structure Claset = Generic_Data
   1.493 +(
   1.494 +  type T = claset;
   1.495 +  val empty = empty_cs;
   1.496 +  val extend = I;
   1.497 +  val merge = merge_cs;
   1.498 +);
   1.499 +
   1.500 +val global_claset_of = Claset.get o Context.Theory;
   1.501 +val claset_of = Claset.get o Context.Proof;
   1.502 +val rep_claset_of = rep_cs o claset_of;
   1.503 +
   1.504 +val get_cs = Claset.get;
   1.505 +val map_cs = Claset.map;
   1.506 +
   1.507 +fun map_claset f = Context.proof_map (map_cs f);
   1.508 +fun put_claset cs = map_claset (K cs);
   1.509 +
   1.510 +fun print_claset ctxt =
   1.511 +  let
   1.512 +    val {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, ...} = rep_claset_of ctxt;
   1.513 +    val pretty_thms = map (Display.pretty_thm ctxt);
   1.514 +  in
   1.515 +    [Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs),
   1.516 +      Pretty.big_list "introduction rules (intro):" (pretty_thms hazIs),
   1.517 +      Pretty.big_list "safe elimination rules (elim!):" (pretty_thms safeEs),
   1.518 +      Pretty.big_list "elimination rules (elim):" (pretty_thms hazEs),
   1.519 +      Pretty.strs ("safe wrappers:" :: map #1 swrappers),
   1.520 +      Pretty.strs ("unsafe wrappers:" :: map #1 uwrappers)]
   1.521 +    |> Pretty.chunks |> Pretty.writeln
   1.522 +  end;
   1.523 +
   1.524 +
   1.525 +(* old-style declarations *)
   1.526 +
   1.527 +fun decl f (ctxt, ths) = map_claset (fold_rev (f (SOME (Context.Proof ctxt))) ths) ctxt;
   1.528 +
   1.529 +val op addSIs = decl (addSI NONE);
   1.530 +val op addSEs = decl (addSE NONE);
   1.531 +val op addSDs = decl (addSD NONE);
   1.532 +val op addIs = decl (addI NONE);
   1.533 +val op addEs = decl (addE NONE);
   1.534 +val op addDs = decl (addD NONE);
   1.535 +val op delrules = decl delrule;
   1.536 +
   1.537 +
   1.538 +
   1.539 +(*** Modifying the wrapper tacticals ***)
   1.540 +
   1.541 +fun appSWrappers ctxt = fold (fn (_, w) => w ctxt) (#swrappers (rep_claset_of ctxt));
   1.542 +fun appWrappers ctxt = fold (fn (_, w) => w ctxt) (#uwrappers (rep_claset_of ctxt));
   1.543 +
   1.544 +fun update_warn msg (p as (key : string, _)) xs =
   1.545 +  (if AList.defined (op =) xs key then warning msg else (); AList.update (op =) p xs);
   1.546 +
   1.547 +fun delete_warn msg (key : string) xs =
   1.548 +  if AList.defined (op =) xs key then AList.delete (op =) key xs
   1.549 +  else (warning msg; xs);
   1.550 +
   1.551 +(*Add/replace a safe wrapper*)
   1.552 +fun cs addSWrapper new_swrapper =
   1.553 +  map_swrappers (update_warn ("Overwriting safe wrapper " ^ fst new_swrapper) new_swrapper) cs;
   1.554 +
   1.555 +(*Add/replace an unsafe wrapper*)
   1.556 +fun cs addWrapper new_uwrapper =
   1.557 +  map_uwrappers (update_warn ("Overwriting unsafe wrapper " ^ fst new_uwrapper) new_uwrapper) cs;
   1.558 +
   1.559 +(*Remove a safe wrapper*)
   1.560 +fun cs delSWrapper name =
   1.561 +  map_swrappers (delete_warn ("No such safe wrapper in claset: " ^ name) name) cs;
   1.562 +
   1.563 +(*Remove an unsafe wrapper*)
   1.564 +fun cs delWrapper name =
   1.565 +  map_uwrappers (delete_warn ("No such unsafe wrapper in claset: " ^ name) name) cs;
   1.566 +
   1.567 +(* compose a safe tactic alternatively before/after safe_step_tac *)
   1.568 +fun cs addSbefore (name, tac1) = cs addSWrapper (name, fn _ => fn tac2 => tac1 ORELSE' tac2);
   1.569 +fun cs addSafter (name, tac2) = cs addSWrapper (name, fn _ => fn tac1 => tac1 ORELSE' tac2);
   1.570 +
   1.571 +(*compose a tactic alternatively before/after the step tactic *)
   1.572 +fun cs addbefore (name, tac1) = cs addWrapper (name, fn _ => fn tac2 => tac1 APPEND' tac2);
   1.573 +fun cs addafter (name, tac2) = cs addWrapper (name, fn _ => fn tac1 => tac1 APPEND' tac2);
   1.574 +
   1.575 +fun cs addD2 (name, thm) = cs addafter (name, datac thm 1);
   1.576 +fun cs addE2 (name, thm) = cs addafter (name, eatac thm 1);
   1.577 +fun cs addSD2 (name, thm) = cs addSafter (name, dmatch_tac [thm] THEN' eq_assume_tac);
   1.578 +fun cs addSE2 (name, thm) = cs addSafter (name, ematch_tac [thm] THEN' eq_assume_tac);
   1.579 +
   1.580  
   1.581  
   1.582  (**** Simple tactics for theorem proving ****)
   1.583  
   1.584  (*Attack subgoals using safe inferences -- matching, not resolution*)
   1.585 -fun safe_step_tac (cs as CS {safe0_netpair, safep_netpair, ...}) =
   1.586 -  appSWrappers cs (FIRST' [
   1.587 -        eq_assume_tac,
   1.588 +fun safe_step_tac ctxt =
   1.589 +  let val {safe0_netpair, safep_netpair, ...} = rep_claset_of ctxt in
   1.590 +    appSWrappers ctxt
   1.591 +      (FIRST'
   1.592 +       [eq_assume_tac,
   1.593          eq_mp_tac,
   1.594          bimatch_from_nets_tac safe0_netpair,
   1.595          FIRST' Data.hyp_subst_tacs,
   1.596 -        bimatch_from_nets_tac safep_netpair]);
   1.597 +        bimatch_from_nets_tac safep_netpair])
   1.598 +  end;
   1.599  
   1.600  (*Repeatedly attack a subgoal using safe inferences -- it's deterministic!*)
   1.601 -fun safe_steps_tac cs =
   1.602 -  REPEAT_DETERM1 o (fn i => COND (has_fewer_prems i) no_tac (safe_step_tac cs i));
   1.603 +fun safe_steps_tac ctxt =
   1.604 +  REPEAT_DETERM1 o (fn i => COND (has_fewer_prems i) no_tac (safe_step_tac ctxt i));
   1.605  
   1.606  (*Repeatedly attack subgoals using safe inferences -- it's deterministic!*)
   1.607 -fun safe_tac cs = REPEAT_DETERM1 (FIRSTGOAL (safe_steps_tac cs));
   1.608 +fun safe_tac ctxt = REPEAT_DETERM1 (FIRSTGOAL (safe_steps_tac ctxt));
   1.609  
   1.610  
   1.611  (*** Clarify_tac: do safe steps without causing branching ***)
   1.612 @@ -669,86 +721,89 @@
   1.613    (eq_assume_contr_tac i ORELSE eq_assume_contr_tac (i + 1));
   1.614  
   1.615  (*Attack subgoals using safe inferences -- matching, not resolution*)
   1.616 -fun clarify_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) =
   1.617 -  appSWrappers cs (FIRST' [
   1.618 -        eq_assume_contr_tac,
   1.619 +fun clarify_step_tac ctxt =
   1.620 +  let val {safe0_netpair, safep_netpair, ...} = rep_claset_of ctxt in
   1.621 +    appSWrappers ctxt
   1.622 +     (FIRST'
   1.623 +       [eq_assume_contr_tac,
   1.624          bimatch_from_nets_tac safe0_netpair,
   1.625          FIRST' Data.hyp_subst_tacs,
   1.626          n_bimatch_from_nets_tac 1 safep_netpair,
   1.627 -        bimatch2_tac safep_netpair]);
   1.628 +        bimatch2_tac safep_netpair])
   1.629 +  end;
   1.630  
   1.631 -fun clarify_tac cs = SELECT_GOAL (REPEAT_DETERM (clarify_step_tac cs 1));
   1.632 +fun clarify_tac ctxt = SELECT_GOAL (REPEAT_DETERM (clarify_step_tac ctxt 1));
   1.633  
   1.634  
   1.635  (*** Unsafe steps instantiate variables or lose information ***)
   1.636  
   1.637  (*Backtracking is allowed among the various these unsafe ways of
   1.638    proving a subgoal.  *)
   1.639 -fun inst0_step_tac (CS {safe0_netpair, ...}) =
   1.640 +fun inst0_step_tac ctxt =
   1.641    assume_tac APPEND'
   1.642    contr_tac APPEND'
   1.643 -  biresolve_from_nets_tac safe0_netpair;
   1.644 +  biresolve_from_nets_tac (#safe0_netpair (rep_claset_of ctxt));
   1.645  
   1.646  (*These unsafe steps could generate more subgoals.*)
   1.647 -fun instp_step_tac (CS {safep_netpair, ...}) =
   1.648 -  biresolve_from_nets_tac safep_netpair;
   1.649 +fun instp_step_tac ctxt =
   1.650 +  biresolve_from_nets_tac (#safep_netpair (rep_claset_of ctxt));
   1.651  
   1.652  (*These steps could instantiate variables and are therefore unsafe.*)
   1.653 -fun inst_step_tac cs = inst0_step_tac cs APPEND' instp_step_tac cs;
   1.654 +fun inst_step_tac ctxt = inst0_step_tac ctxt APPEND' instp_step_tac ctxt;
   1.655  
   1.656 -fun haz_step_tac (CS{haz_netpair,...}) =
   1.657 -  biresolve_from_nets_tac haz_netpair;
   1.658 +fun haz_step_tac ctxt =
   1.659 +  biresolve_from_nets_tac (#haz_netpair (rep_claset_of ctxt));
   1.660  
   1.661  (*Single step for the prover.  FAILS unless it makes progress. *)
   1.662 -fun step_tac cs i =
   1.663 -  safe_tac cs ORELSE appWrappers cs (inst_step_tac cs ORELSE' haz_step_tac cs) i;
   1.664 +fun step_tac ctxt i =
   1.665 +  safe_tac ctxt ORELSE appWrappers ctxt (inst_step_tac ctxt ORELSE' haz_step_tac ctxt) i;
   1.666  
   1.667  (*Using a "safe" rule to instantiate variables is unsafe.  This tactic
   1.668    allows backtracking from "safe" rules to "unsafe" rules here.*)
   1.669 -fun slow_step_tac cs i =
   1.670 -  safe_tac cs ORELSE appWrappers cs (inst_step_tac cs APPEND' haz_step_tac cs) i;
   1.671 +fun slow_step_tac ctxt i =
   1.672 +  safe_tac ctxt ORELSE appWrappers ctxt (inst_step_tac ctxt APPEND' haz_step_tac ctxt) i;
   1.673  
   1.674  
   1.675  (**** The following tactics all fail unless they solve one goal ****)
   1.676  
   1.677  (*Dumb but fast*)
   1.678 -fun fast_tac cs =
   1.679 -  Object_Logic.atomize_prems_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1));
   1.680 +fun fast_tac ctxt =
   1.681 +  Object_Logic.atomize_prems_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt 1));
   1.682  
   1.683  (*Slower but smarter than fast_tac*)
   1.684 -fun best_tac cs =
   1.685 +fun best_tac ctxt =
   1.686    Object_Logic.atomize_prems_tac THEN'
   1.687 -  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (step_tac cs 1));
   1.688 +  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (step_tac ctxt 1));
   1.689  
   1.690  (*even a bit smarter than best_tac*)
   1.691 -fun first_best_tac cs =
   1.692 +fun first_best_tac ctxt =
   1.693    Object_Logic.atomize_prems_tac THEN'
   1.694 -  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (FIRSTGOAL (step_tac cs)));
   1.695 +  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (FIRSTGOAL (step_tac ctxt)));
   1.696  
   1.697 -fun slow_tac cs =
   1.698 +fun slow_tac ctxt =
   1.699    Object_Logic.atomize_prems_tac THEN'
   1.700 -  SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1));
   1.701 +  SELECT_GOAL (DEPTH_SOLVE (slow_step_tac ctxt 1));
   1.702  
   1.703 -fun slow_best_tac cs =
   1.704 +fun slow_best_tac ctxt =
   1.705    Object_Logic.atomize_prems_tac THEN'
   1.706 -  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (slow_step_tac cs 1));
   1.707 +  SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, Data.sizef) (slow_step_tac ctxt 1));
   1.708  
   1.709  
   1.710  (***ASTAR with weight weight_ASTAR, by Norbert Voelker*)
   1.711  
   1.712  val weight_ASTAR = 5;
   1.713  
   1.714 -fun astar_tac cs =
   1.715 +fun astar_tac ctxt =
   1.716    Object_Logic.atomize_prems_tac THEN'
   1.717    SELECT_GOAL
   1.718      (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + weight_ASTAR * lev)
   1.719 -      (step_tac cs 1));
   1.720 +      (step_tac ctxt 1));
   1.721  
   1.722 -fun slow_astar_tac cs =
   1.723 +fun slow_astar_tac ctxt =
   1.724    Object_Logic.atomize_prems_tac THEN'
   1.725    SELECT_GOAL
   1.726      (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + weight_ASTAR * lev)
   1.727 -      (slow_step_tac cs 1));
   1.728 +      (slow_step_tac ctxt 1));
   1.729  
   1.730  
   1.731  (**** Complete tactic, loosely based upon LeanTaP.  This tactic is the outcome
   1.732 @@ -759,132 +814,44 @@
   1.733  (*Non-deterministic!  Could always expand the first unsafe connective.
   1.734    That's hard to implement and did not perform better in experiments, due to
   1.735    greater search depth required.*)
   1.736 -fun dup_step_tac (CS {dup_netpair, ...}) =
   1.737 -  biresolve_from_nets_tac dup_netpair;
   1.738 +fun dup_step_tac ctxt =
   1.739 +  biresolve_from_nets_tac (#dup_netpair (rep_claset_of ctxt));
   1.740  
   1.741  (*Searching to depth m. A variant called nodup_depth_tac appears in clasimp.ML*)
   1.742  local
   1.743 -  fun slow_step_tac' cs = appWrappers cs (instp_step_tac cs APPEND' dup_step_tac cs);
   1.744 +  fun slow_step_tac' ctxt = appWrappers ctxt (instp_step_tac ctxt APPEND' dup_step_tac ctxt);
   1.745  in
   1.746 -  fun depth_tac cs m i state = SELECT_GOAL
   1.747 -    (safe_steps_tac cs 1 THEN_ELSE
   1.748 -      (DEPTH_SOLVE (depth_tac cs m 1),
   1.749 -        inst0_step_tac cs 1 APPEND COND (K (m = 0)) no_tac
   1.750 -          (slow_step_tac' cs 1 THEN DEPTH_SOLVE (depth_tac cs (m - 1) 1)))) i state;
   1.751 +  fun depth_tac ctxt m i state = SELECT_GOAL
   1.752 +    (safe_steps_tac ctxt 1 THEN_ELSE
   1.753 +      (DEPTH_SOLVE (depth_tac ctxt m 1),
   1.754 +        inst0_step_tac ctxt 1 APPEND COND (K (m = 0)) no_tac
   1.755 +          (slow_step_tac' ctxt 1 THEN DEPTH_SOLVE (depth_tac ctxt (m - 1) 1)))) i state;
   1.756  end;
   1.757  
   1.758  (*Search, with depth bound m.
   1.759    This is the "entry point", which does safe inferences first.*)
   1.760 -fun safe_depth_tac cs m = SUBGOAL (fn (prem,i) =>
   1.761 -  let val deti =
   1.762 -      (*No Vars in the goal?  No need to backtrack between goals.*)
   1.763 -    if exists_subterm (fn Var _ => true | _ => false) prem then DETERM else I
   1.764 +fun safe_depth_tac ctxt m = SUBGOAL (fn (prem, i) =>
   1.765 +  let
   1.766 +    val deti = (*No Vars in the goal?  No need to backtrack between goals.*)
   1.767 +      if exists_subterm (fn Var _ => true | _ => false) prem then DETERM else I;
   1.768    in
   1.769 -    SELECT_GOAL (TRY (safe_tac cs) THEN DEPTH_SOLVE (deti (depth_tac cs m 1))) i
   1.770 +    SELECT_GOAL (TRY (safe_tac ctxt) THEN DEPTH_SOLVE (deti (depth_tac ctxt m 1))) i
   1.771    end);
   1.772  
   1.773 -fun deepen_tac cs = DEEPEN (2, 10) (safe_depth_tac cs);
   1.774 -
   1.775 -
   1.776 -
   1.777 -(** context dependent claset components **)
   1.778 -
   1.779 -datatype context_cs = ContextCS of
   1.780 - {swrappers: (string * (Proof.context -> wrapper)) list,
   1.781 -  uwrappers: (string * (Proof.context -> wrapper)) list};
   1.782 -
   1.783 -fun context_cs ctxt cs (ContextCS {swrappers, uwrappers}) =
   1.784 -  let
   1.785 -    fun add_wrapper add (name, f) claset = add (claset, (name, f ctxt));
   1.786 -  in
   1.787 -    cs
   1.788 -    |> fold_rev (add_wrapper (op addSWrapper)) swrappers
   1.789 -    |> fold_rev (add_wrapper (op addWrapper)) uwrappers
   1.790 -  end;
   1.791 -
   1.792 -fun make_context_cs (swrappers, uwrappers) =
   1.793 -  ContextCS {swrappers = swrappers, uwrappers = uwrappers};
   1.794 -
   1.795 -val empty_context_cs = make_context_cs ([], []);
   1.796 -
   1.797 -fun merge_context_cs (ctxt_cs1, ctxt_cs2) =
   1.798 -  if pointer_eq (ctxt_cs1, ctxt_cs2) then ctxt_cs1
   1.799 -  else
   1.800 -    let
   1.801 -      val ContextCS {swrappers = swrappers1, uwrappers = uwrappers1} = ctxt_cs1;
   1.802 -      val ContextCS {swrappers = swrappers2, uwrappers = uwrappers2} = ctxt_cs2;
   1.803 -      val swrappers' = AList.merge (op =) (K true) (swrappers1, swrappers2);
   1.804 -      val uwrappers' = AList.merge (op =) (K true) (uwrappers1, uwrappers2);
   1.805 -    in make_context_cs (swrappers', uwrappers') end;
   1.806 -
   1.807 -
   1.808 -
   1.809 -(** claset data **)
   1.810 -
   1.811 -(* global clasets *)
   1.812 -
   1.813 -structure GlobalClaset = Theory_Data
   1.814 -(
   1.815 -  type T = claset * context_cs;
   1.816 -  val empty = (empty_cs, empty_context_cs);
   1.817 -  val extend = I;
   1.818 -  fun merge ((cs1, ctxt_cs1), (cs2, ctxt_cs2)) =
   1.819 -    (merge_cs (cs1, cs2), merge_context_cs (ctxt_cs1, ctxt_cs2));
   1.820 -);
   1.821 -
   1.822 -val get_global_claset = #1 o GlobalClaset.get;
   1.823 -val map_global_claset = GlobalClaset.map o apfst;
   1.824 -
   1.825 -val get_context_cs = #2 o GlobalClaset.get o Proof_Context.theory_of;
   1.826 -fun map_context_cs f = GlobalClaset.map (apsnd
   1.827 -  (fn ContextCS {swrappers, uwrappers} => make_context_cs (f (swrappers, uwrappers))));
   1.828 -
   1.829 -fun global_claset_of thy =
   1.830 -  let val (cs, ctxt_cs) = GlobalClaset.get thy
   1.831 -  in context_cs (Proof_Context.init_global thy) cs (ctxt_cs) end;
   1.832 -
   1.833 -
   1.834 -(* context dependent components *)
   1.835 -
   1.836 -fun add_context_safe_wrapper wrapper = map_context_cs (apfst ((AList.update (op =) wrapper)));
   1.837 -fun del_context_safe_wrapper name = map_context_cs (apfst ((AList.delete (op =) name)));
   1.838 -
   1.839 -fun add_context_unsafe_wrapper wrapper = map_context_cs (apsnd ((AList.update (op =) wrapper)));
   1.840 -fun del_context_unsafe_wrapper name = map_context_cs (apsnd ((AList.delete (op =) name)));
   1.841 -
   1.842 -
   1.843 -(* local clasets *)
   1.844 -
   1.845 -structure LocalClaset = Proof_Data
   1.846 -(
   1.847 -  type T = claset;
   1.848 -  val init = get_global_claset;
   1.849 -);
   1.850 -
   1.851 -val get_claset = LocalClaset.get;
   1.852 -val put_claset = LocalClaset.put;
   1.853 -
   1.854 -fun claset_of ctxt =
   1.855 -  context_cs ctxt (LocalClaset.get ctxt) (get_context_cs ctxt);
   1.856 -
   1.857 -
   1.858 -(* generic clasets *)
   1.859 -
   1.860 -val get_cs = Context.cases global_claset_of claset_of;
   1.861 -fun map_cs f = Context.mapping (map_global_claset f) (LocalClaset.map f);
   1.862 +fun deepen_tac ctxt = DEEPEN (2, 10) (safe_depth_tac ctxt);
   1.863  
   1.864  
   1.865  (* attributes *)
   1.866  
   1.867 -fun attrib f = Thm.declaration_attribute (fn th =>
   1.868 -  Context.mapping (map_global_claset (f th)) (LocalClaset.map (f th)));
   1.869 +fun attrib f =
   1.870 +  Thm.declaration_attribute (fn th => fn context => map_cs (f (SOME context) th) context);
   1.871  
   1.872 -fun safe_dest w = attrib (addSE w o make_elim);
   1.873  val safe_elim = attrib o addSE;
   1.874  val safe_intro = attrib o addSI;
   1.875 -fun haz_dest w = attrib (addE w o make_elim);
   1.876 +val safe_dest = attrib o addSD;
   1.877  val haz_elim = attrib o addE;
   1.878  val haz_intro = attrib o addI;
   1.879 +val haz_dest = attrib o addD;
   1.880  val rule_del = attrib delrule o Context_Rules.rule_del;
   1.881  
   1.882  
   1.883 @@ -916,7 +883,7 @@
   1.884  fun some_rule_tac ctxt facts = SUBGOAL (fn (goal, i) =>
   1.885    let
   1.886      val [rules1, rules2, rules4] = Context_Rules.find_rules false facts goal ctxt;
   1.887 -    val CS {xtra_netpair, ...} = claset_of ctxt;
   1.888 +    val {xtra_netpair, ...} = rep_claset_of ctxt;
   1.889      val rules3 = Context_Rules.find_rules_netpair true facts goal xtra_netpair;
   1.890      val rules = rules1 @ rules2 @ rules3 @ rules4;
   1.891      val ruleq = Drule.multi_resolves facts rules;
   1.892 @@ -954,14 +921,8 @@
   1.893    Args.$$$ introN -- Args.colon >> K (I, haz_intro NONE),
   1.894    Args.del -- Args.colon >> K (I, rule_del)];
   1.895  
   1.896 -fun cla_meth tac ctxt = METHOD (fn facts =>
   1.897 -  ALLGOALS (Method.insert_tac facts) THEN tac (claset_of ctxt));
   1.898 -
   1.899 -fun cla_meth' tac ctxt = METHOD (fn facts =>
   1.900 -  HEADGOAL (Method.insert_tac facts THEN' tac (claset_of ctxt)));
   1.901 -
   1.902 -fun cla_method tac = Method.sections cla_modifiers >> K (cla_meth tac);
   1.903 -fun cla_method' tac = Method.sections cla_modifiers >> K (cla_meth' tac);
   1.904 +fun cla_method tac = Method.sections cla_modifiers >> K (SIMPLE_METHOD o tac);
   1.905 +fun cla_method' tac = Method.sections cla_modifiers >> K (SIMPLE_METHOD' o tac);
   1.906  
   1.907  
   1.908  
   1.909 @@ -981,7 +942,7 @@
   1.910    Method.setup @{binding fast} (cla_method' fast_tac) "classical prover (depth-first)" #>
   1.911    Method.setup @{binding slow} (cla_method' slow_tac) "classical prover (slow depth-first)" #>
   1.912    Method.setup @{binding best} (cla_method' best_tac) "classical prover (best-first)" #>
   1.913 -  Method.setup @{binding deepen} (cla_method' (fn cs => deepen_tac cs 4))
   1.914 +  Method.setup @{binding deepen} (cla_method' (fn ctxt => deepen_tac ctxt 4))
   1.915      "classical prover (iterative deepening)" #>
   1.916    Method.setup @{binding safe} (cla_method (CHANGED_PROP o safe_tac))
   1.917      "classical prover (apply safe rules)";
   1.918 @@ -1002,6 +963,6 @@
   1.919      (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
   1.920        Toplevel.keep (fn state =>
   1.921          let val ctxt = Toplevel.context_of state
   1.922 -        in print_cs ctxt (claset_of ctxt) end)));
   1.923 +        in print_claset ctxt end)));
   1.924  
   1.925  end;