src/Provers/classical.ML
changeset 9938 cb6a7572d0a1
parent 9899 5a9081c3b869
child 9941 fe05af7ec816
     1.1 --- a/src/Provers/classical.ML	Tue Sep 12 17:35:09 2000 +0200
     1.2 +++ b/src/Provers/classical.ML	Tue Sep 12 17:38:49 2000 +0200
     1.3 @@ -1,6 +1,6 @@
     1.4 -(*  Title: 	Provers/classical.ML
     1.5 +(*  Title:      Provers/classical.ML
     1.6      ID:         $Id$
     1.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.9      Copyright   1992  University of Cambridge
    1.10  
    1.11  Theorem prover for classical reasoning, including predicate calculus, set
    1.12 @@ -28,10 +28,10 @@
    1.13  signature CLASSICAL_DATA =
    1.14  sig
    1.15    val make_elim : thm -> thm    (* Tactic.make_elim or a classical version*)
    1.16 -  val mp	: thm    	(* [| P-->Q;  P |] ==> Q *)
    1.17 -  val not_elim	: thm		(* [| ~P;  P |] ==> R *)
    1.18 -  val classical	: thm		(* (~P ==> P) ==> P *)
    1.19 -  val sizef 	: thm -> int	(* size function for BEST_FIRST *)
    1.20 +  val mp        : thm           (* [| P-->Q;  P |] ==> Q *)
    1.21 +  val not_elim  : thm           (* [| ~P;  P |] ==> R *)
    1.22 +  val classical : thm           (* (~P ==> P) ==> P *)
    1.23 +  val sizef     : thm -> int    (* size function for BEST_FIRST *)
    1.24    val hyp_subst_tacs: (int -> tactic) list
    1.25  end;
    1.26  
    1.27 @@ -43,35 +43,35 @@
    1.28    val print_claset: theory -> unit
    1.29    val rep_cs: (* BLAST_DATA in blast.ML dependent on this *)
    1.30      claset -> {safeIs: thm list, safeEs: thm list,
    1.31 -		 hazIs: thm list, hazEs: thm list,
    1.32 -		 xtraIs: thm list, xtraEs: thm list,
    1.33 -		 swrappers: (string * wrapper) list, 
    1.34 -		 uwrappers: (string * wrapper) list,
    1.35 -		 safe0_netpair: netpair, safep_netpair: netpair,
    1.36 -		 haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: netpair}
    1.37 -  val merge_cs		: claset * claset -> claset
    1.38 -  val addDs 		: claset * thm list -> claset
    1.39 -  val addEs 		: claset * thm list -> claset
    1.40 -  val addIs 		: claset * thm list -> claset
    1.41 -  val addSDs		: claset * thm list -> claset
    1.42 -  val addSEs		: claset * thm list -> claset
    1.43 -  val addSIs		: claset * thm list -> claset
    1.44 -  val delrules		: claset * thm list -> claset
    1.45 -  val addSWrapper 	: claset * (string * wrapper) -> claset
    1.46 -  val delSWrapper 	: claset *  string            -> claset
    1.47 -  val addWrapper 	: claset * (string * wrapper) -> claset
    1.48 -  val delWrapper 	: claset *  string            -> claset
    1.49 -  val addSbefore 	: claset * (string * (int -> tactic)) -> claset
    1.50 -  val addSaltern 	: claset * (string * (int -> tactic)) -> claset
    1.51 -  val addbefore 	: claset * (string * (int -> tactic)) -> claset
    1.52 -  val addaltern	 	: claset * (string * (int -> tactic)) -> claset
    1.53 +                 hazIs: thm list, hazEs: thm list,
    1.54 +                 xtraIs: thm list, xtraEs: thm list,
    1.55 +                 swrappers: (string * wrapper) list, 
    1.56 +                 uwrappers: (string * wrapper) list,
    1.57 +                 safe0_netpair: netpair, safep_netpair: netpair,
    1.58 +                 haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: netpair}
    1.59 +  val merge_cs          : claset * claset -> claset
    1.60 +  val addDs             : claset * thm list -> claset
    1.61 +  val addEs             : claset * thm list -> claset
    1.62 +  val addIs             : claset * thm list -> claset
    1.63 +  val addSDs            : claset * thm list -> claset
    1.64 +  val addSEs            : claset * thm list -> claset
    1.65 +  val addSIs            : claset * thm list -> claset
    1.66 +  val delrules          : claset * thm list -> claset
    1.67 +  val addSWrapper       : claset * (string * wrapper) -> claset
    1.68 +  val delSWrapper       : claset *  string            -> claset
    1.69 +  val addWrapper        : claset * (string * wrapper) -> claset
    1.70 +  val delWrapper        : claset *  string            -> claset
    1.71 +  val addSbefore        : claset * (string * (int -> tactic)) -> claset
    1.72 +  val addSaltern        : claset * (string * (int -> tactic)) -> claset
    1.73 +  val addbefore         : claset * (string * (int -> tactic)) -> claset
    1.74 +  val addaltern         : claset * (string * (int -> tactic)) -> claset
    1.75    val addD2             : claset * (string * thm) -> claset
    1.76    val addE2             : claset * (string * thm) -> claset
    1.77    val addSD2            : claset * (string * thm) -> claset
    1.78    val addSE2            : claset * (string * thm) -> claset
    1.79 -  val appSWrappers	: claset -> wrapper
    1.80 -  val appWrappers	: claset -> wrapper
    1.81 -  val trace_rules	: bool ref
    1.82 +  val appSWrappers      : claset -> wrapper
    1.83 +  val appWrappers       : claset -> wrapper
    1.84 +  val trace_rules       : bool ref
    1.85  
    1.86    val claset_ref_of_sg: Sign.sg -> claset ref
    1.87    val claset_ref_of: theory -> claset ref
    1.88 @@ -82,59 +82,59 @@
    1.89    val claset: unit -> claset
    1.90    val claset_ref: unit -> claset ref
    1.91  
    1.92 -  val fast_tac 		: claset -> int -> tactic
    1.93 -  val slow_tac 		: claset -> int -> tactic
    1.94 -  val weight_ASTAR	: int ref
    1.95 -  val astar_tac		: claset -> int -> tactic
    1.96 -  val slow_astar_tac 	: claset -> int -> tactic
    1.97 -  val best_tac 		: claset -> int -> tactic
    1.98 -  val first_best_tac	: claset -> int -> tactic
    1.99 -  val slow_best_tac 	: claset -> int -> tactic
   1.100 -  val depth_tac		: claset -> int -> int -> tactic
   1.101 -  val deepen_tac	: claset -> int -> int -> tactic
   1.102 +  val fast_tac          : claset -> int -> tactic
   1.103 +  val slow_tac          : claset -> int -> tactic
   1.104 +  val weight_ASTAR      : int ref
   1.105 +  val astar_tac         : claset -> int -> tactic
   1.106 +  val slow_astar_tac    : claset -> int -> tactic
   1.107 +  val best_tac          : claset -> int -> tactic
   1.108 +  val first_best_tac    : claset -> int -> tactic
   1.109 +  val slow_best_tac     : claset -> int -> tactic
   1.110 +  val depth_tac         : claset -> int -> int -> tactic
   1.111 +  val deepen_tac        : claset -> int -> int -> tactic
   1.112  
   1.113 -  val contr_tac 	: int -> tactic
   1.114 -  val dup_elim		: thm -> thm
   1.115 -  val dup_intr		: thm -> thm
   1.116 -  val dup_step_tac	: claset -> int -> tactic
   1.117 -  val eq_mp_tac		: int -> tactic
   1.118 -  val haz_step_tac 	: claset -> int -> tactic
   1.119 -  val joinrules 	: thm list * thm list -> (bool * thm) list
   1.120 -  val mp_tac		: int -> tactic
   1.121 -  val safe_tac 		: claset -> tactic
   1.122 -  val safe_steps_tac 	: claset -> int -> tactic
   1.123 -  val safe_step_tac 	: claset -> int -> tactic
   1.124 -  val clarify_tac 	: claset -> int -> tactic
   1.125 -  val clarify_step_tac 	: claset -> int -> tactic
   1.126 -  val step_tac 		: claset -> int -> tactic
   1.127 -  val slow_step_tac	: claset -> int -> tactic
   1.128 -  val swap		: thm                 (* ~P ==> (~Q ==> P) ==> Q *)
   1.129 -  val swapify 		: thm list -> thm list
   1.130 -  val swap_res_tac 	: thm list -> int -> tactic
   1.131 -  val inst_step_tac 	: claset -> int -> tactic
   1.132 -  val inst0_step_tac 	: claset -> int -> tactic
   1.133 -  val instp_step_tac 	: claset -> int -> tactic
   1.134 +  val contr_tac         : int -> tactic
   1.135 +  val dup_elim          : thm -> thm
   1.136 +  val dup_intr          : thm -> thm
   1.137 +  val dup_step_tac      : claset -> int -> tactic
   1.138 +  val eq_mp_tac         : int -> tactic
   1.139 +  val haz_step_tac      : claset -> int -> tactic
   1.140 +  val joinrules         : thm list * thm list -> (bool * thm) list
   1.141 +  val mp_tac            : int -> tactic
   1.142 +  val safe_tac          : claset -> tactic
   1.143 +  val safe_steps_tac    : claset -> int -> tactic
   1.144 +  val safe_step_tac     : claset -> int -> tactic
   1.145 +  val clarify_tac       : claset -> int -> tactic
   1.146 +  val clarify_step_tac  : claset -> int -> tactic
   1.147 +  val step_tac          : claset -> int -> tactic
   1.148 +  val slow_step_tac     : claset -> int -> tactic
   1.149 +  val swap              : thm                 (* ~P ==> (~Q ==> P) ==> Q *)
   1.150 +  val swapify           : thm list -> thm list
   1.151 +  val swap_res_tac      : thm list -> int -> tactic
   1.152 +  val inst_step_tac     : claset -> int -> tactic
   1.153 +  val inst0_step_tac    : claset -> int -> tactic
   1.154 +  val instp_step_tac    : claset -> int -> tactic
   1.155  
   1.156 -  val AddDs 		: thm list -> unit
   1.157 -  val AddEs 		: thm list -> unit
   1.158 -  val AddIs 		: thm list -> unit
   1.159 -  val AddSDs		: thm list -> unit
   1.160 -  val AddSEs		: thm list -> unit
   1.161 -  val AddSIs		: thm list -> unit
   1.162 -  val AddXDs		: thm list -> unit
   1.163 -  val AddXEs		: thm list -> unit
   1.164 -  val AddXIs		: thm list -> unit
   1.165 -  val Delrules		: thm list -> unit
   1.166 -  val Safe_tac         	: tactic
   1.167 -  val Safe_step_tac	: int -> tactic
   1.168 -  val Clarify_tac 	: int -> tactic
   1.169 -  val Clarify_step_tac 	: int -> tactic
   1.170 -  val Step_tac 		: int -> tactic
   1.171 -  val Fast_tac 		: int -> tactic
   1.172 -  val Best_tac 		: int -> tactic
   1.173 -  val Slow_tac 		: int -> tactic
   1.174 +  val AddDs             : thm list -> unit
   1.175 +  val AddEs             : thm list -> unit
   1.176 +  val AddIs             : thm list -> unit
   1.177 +  val AddSDs            : thm list -> unit
   1.178 +  val AddSEs            : thm list -> unit
   1.179 +  val AddSIs            : thm list -> unit
   1.180 +  val AddXDs            : thm list -> unit
   1.181 +  val AddXEs            : thm list -> unit
   1.182 +  val AddXIs            : thm list -> unit
   1.183 +  val Delrules          : thm list -> unit
   1.184 +  val Safe_tac          : tactic
   1.185 +  val Safe_step_tac     : int -> tactic
   1.186 +  val Clarify_tac       : int -> tactic
   1.187 +  val Clarify_step_tac  : int -> tactic
   1.188 +  val Step_tac          : int -> tactic
   1.189 +  val Fast_tac          : int -> tactic
   1.190 +  val Best_tac          : int -> tactic
   1.191 +  val Slow_tac          : int -> tactic
   1.192    val Slow_best_tac     : int -> tactic
   1.193 -  val Deepen_tac	: int -> int -> tactic
   1.194 +  val Deepen_tac        : int -> int -> tactic
   1.195  end;
   1.196  
   1.197  signature CLASSICAL =
   1.198 @@ -152,7 +152,7 @@
   1.199    val xtra_dest_global: theory attribute
   1.200    val xtra_elim_global: theory attribute
   1.201    val xtra_intro_global: theory attribute
   1.202 -  val delrule_global: theory attribute
   1.203 +  val rule_del_global: theory attribute
   1.204    val safe_dest_local: Proof.context attribute
   1.205    val safe_elim_local: Proof.context attribute
   1.206    val safe_intro_local: Proof.context attribute
   1.207 @@ -162,7 +162,7 @@
   1.208    val xtra_dest_local: Proof.context attribute
   1.209    val xtra_elim_local: Proof.context attribute
   1.210    val xtra_intro_local: Proof.context attribute
   1.211 -  val delrule_local: Proof.context attribute
   1.212 +  val rule_del_local: Proof.context attribute
   1.213    val cla_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
   1.214    val cla_meth: (claset -> tactic) -> thm list -> Proof.context -> Proof.method
   1.215    val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
   1.216 @@ -180,7 +180,7 @@
   1.217  (*** Useful tactics for classical reasoning ***)
   1.218  
   1.219  val imp_elim = (*cannot use bind_thm within a structure!*)
   1.220 -  store_thm ("imp_elim", make_elim mp);
   1.221 +  store_thm ("imp_elim", Data.make_elim mp);
   1.222  
   1.223  (*Prove goal that assumes both P and ~P.  
   1.224    No backtracking if it finds an equal assumption.  Perhaps should call
   1.225 @@ -205,8 +205,8 @@
   1.226    trying rules in order. *)
   1.227  fun swap_res_tac rls = 
   1.228      let fun addrl (rl,brls) = (false, rl) :: (true, rl RSN (2,swap)) :: brls
   1.229 -    in  assume_tac 	ORELSE' 
   1.230 -	contr_tac 	ORELSE' 
   1.231 +    in  assume_tac      ORELSE' 
   1.232 +        contr_tac       ORELSE' 
   1.233          biresolve_tac (foldr addrl (rls,[]))
   1.234      end;
   1.235  
   1.236 @@ -224,27 +224,27 @@
   1.237  (**** Classical rule sets ****)
   1.238  
   1.239  datatype claset =
   1.240 -  CS of {safeIs		: thm list,		(*safe introduction rules*)
   1.241 -	 safeEs		: thm list,		(*safe elimination rules*)
   1.242 -	 hazIs		: thm list,		(*unsafe introduction rules*)
   1.243 -	 hazEs		: thm list,		(*unsafe elimination rules*)
   1.244 -	 xtraIs		: thm list,		(*extra introduction rules*)
   1.245 -	 xtraEs		: thm list,		(*extra elimination rules*)
   1.246 -	 swrappers	: (string * wrapper) list, (*for transf. safe_step_tac*)
   1.247 -	 uwrappers	: (string * wrapper) list, (*for transforming step_tac*)
   1.248 -	 safe0_netpair	: netpair,		(*nets for trivial cases*)
   1.249 -	 safep_netpair	: netpair,		(*nets for >0 subgoals*)
   1.250 -	 haz_netpair  	: netpair,		(*nets for unsafe rules*)
   1.251 -	 dup_netpair	: netpair,		(*nets for duplication*)
   1.252 -	 xtra_netpair	: netpair};		(*nets for extra rules*)
   1.253 +  CS of {safeIs         : thm list,             (*safe introduction rules*)
   1.254 +         safeEs         : thm list,             (*safe elimination rules*)
   1.255 +         hazIs          : thm list,             (*unsafe introduction rules*)
   1.256 +         hazEs          : thm list,             (*unsafe elimination rules*)
   1.257 +         xtraIs         : thm list,             (*extra introduction rules*)
   1.258 +         xtraEs         : thm list,             (*extra elimination rules*)
   1.259 +         swrappers      : (string * wrapper) list, (*for transf. safe_step_tac*)
   1.260 +         uwrappers      : (string * wrapper) list, (*for transforming step_tac*)
   1.261 +         safe0_netpair  : netpair,              (*nets for trivial cases*)
   1.262 +         safep_netpair  : netpair,              (*nets for >0 subgoals*)
   1.263 +         haz_netpair    : netpair,              (*nets for unsafe rules*)
   1.264 +         dup_netpair    : netpair,              (*nets for duplication*)
   1.265 +         xtra_netpair   : netpair};             (*nets for extra rules*)
   1.266  
   1.267  (*Desired invariants are
   1.268 -	safe0_netpair = build safe0_brls,
   1.269 -	safep_netpair = build safep_brls,
   1.270 -	haz_netpair = build (joinrules(hazIs, hazEs)),
   1.271 -	dup_netpair = build (joinrules(map dup_intr hazIs, 
   1.272 -				       map dup_elim hazEs)),
   1.273 -	xtra_netpair = build (joinrules(xtraIs, xtraEs))}
   1.274 +        safe0_netpair = build safe0_brls,
   1.275 +        safep_netpair = build safep_brls,
   1.276 +        haz_netpair = build (joinrules(hazIs, hazEs)),
   1.277 +        dup_netpair = build (joinrules(map dup_intr hazIs, 
   1.278 +                                       map dup_elim hazEs)),
   1.279 +        xtra_netpair = build (joinrules(xtraIs, xtraEs))}
   1.280  
   1.281  where build = build_netpair(Net.empty,Net.empty), 
   1.282        safe0_brls contains all brules that solve the subgoal, and
   1.283 @@ -256,12 +256,12 @@
   1.284  val empty_netpair = (Net.empty, Net.empty);
   1.285  
   1.286  val empty_cs = 
   1.287 -  CS{safeIs	= [],
   1.288 -     safeEs	= [],
   1.289 -     hazIs	= [],
   1.290 -     hazEs	= [],
   1.291 -     xtraIs	= [],
   1.292 -     xtraEs	= [],
   1.293 +  CS{safeIs     = [],
   1.294 +     safeEs     = [],
   1.295 +     hazIs      = [],
   1.296 +     hazEs      = [],
   1.297 +     xtraIs     = [],
   1.298 +     xtraEs     = [],
   1.299       swrappers  = [],
   1.300       uwrappers  = [],
   1.301       safe0_netpair = empty_netpair,
   1.302 @@ -327,7 +327,7 @@
   1.303    is still allowed.*)
   1.304  fun warn_dup th (CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, ...}) = 
   1.305         if mem_thm (th, safeIs) then 
   1.306 -	 warning ("Rule already declared as safe introduction (intro!)\n" ^ string_of_thm th)
   1.307 +         warning ("Rule already declared as safe introduction (intro!)\n" ^ string_of_thm th)
   1.308    else if mem_thm (th, safeEs) then
   1.309           warning ("Rule already declared as safe elimination (elim!)\n" ^ string_of_thm th)
   1.310    else if mem_thm (th, hazIs) then 
   1.311 @@ -343,57 +343,57 @@
   1.312  (*** Safe rules ***)
   1.313  
   1.314  fun addSI (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
   1.315 -	      safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair},
   1.316 -	   th)  =
   1.317 +              safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair},
   1.318 +           th)  =
   1.319    if mem_thm (th, safeIs) then 
   1.320 -	 (warning ("Ignoring duplicate safe introduction (intro!)\n" ^ string_of_thm th);
   1.321 -	  cs)
   1.322 +         (warning ("Ignoring duplicate safe introduction (intro!)\n" ^ string_of_thm th);
   1.323 +          cs)
   1.324    else
   1.325    let val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
   1.326            partition Thm.no_prems [th]
   1.327        val nI = length safeIs + 1
   1.328        and nE = length safeEs
   1.329    in warn_dup th cs;
   1.330 -     CS{safeIs	= th::safeIs,
   1.331 +     CS{safeIs  = th::safeIs,
   1.332          safe0_netpair = insert (nI,nE) (safe0_rls, []) safe0_netpair,
   1.333 -	safep_netpair = insert (nI,nE) (safep_rls, []) safep_netpair,
   1.334 -	safeEs	= safeEs,
   1.335 -	hazIs	= hazIs,
   1.336 -	hazEs	= hazEs,
   1.337 -	xtraIs	= xtraIs,
   1.338 -	xtraEs	= xtraEs,
   1.339 -	swrappers    = swrappers,
   1.340 -	uwrappers    = uwrappers,
   1.341 -	haz_netpair  = haz_netpair,
   1.342 -	dup_netpair  = dup_netpair,
   1.343 -	xtra_netpair = xtra_netpair}
   1.344 +        safep_netpair = insert (nI,nE) (safep_rls, []) safep_netpair,
   1.345 +        safeEs  = safeEs,
   1.346 +        hazIs   = hazIs,
   1.347 +        hazEs   = hazEs,
   1.348 +        xtraIs  = xtraIs,
   1.349 +        xtraEs  = xtraEs,
   1.350 +        swrappers    = swrappers,
   1.351 +        uwrappers    = uwrappers,
   1.352 +        haz_netpair  = haz_netpair,
   1.353 +        dup_netpair  = dup_netpair,
   1.354 +        xtra_netpair = xtra_netpair}
   1.355    end;
   1.356  
   1.357  fun addSE (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
   1.358 -		    safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair},
   1.359 -	   th)  =
   1.360 +                    safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair},
   1.361 +           th)  =
   1.362    if mem_thm (th, safeEs) then 
   1.363 -	 (warning ("Ignoring duplicate safe elimination (elim!)\n" ^ string_of_thm th);
   1.364 -	  cs)
   1.365 +         (warning ("Ignoring duplicate safe elimination (elim!)\n" ^ string_of_thm th);
   1.366 +          cs)
   1.367    else
   1.368    let val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
   1.369            partition (fn rl => nprems_of rl=1) [th]
   1.370        val nI = length safeIs
   1.371        and nE = length safeEs + 1
   1.372    in warn_dup th cs;
   1.373 -     CS{safeEs	= th::safeEs,
   1.374 +     CS{safeEs  = th::safeEs,
   1.375          safe0_netpair = insert (nI,nE) ([], safe0_rls) safe0_netpair,
   1.376 -	safep_netpair = insert (nI,nE) ([], safep_rls) safep_netpair,
   1.377 -	safeIs	= safeIs,
   1.378 -	hazIs	= hazIs,
   1.379 -	hazEs	= hazEs,
   1.380 -	xtraIs	= xtraIs,
   1.381 -	xtraEs	= xtraEs,
   1.382 -	swrappers    = swrappers,
   1.383 -	uwrappers    = uwrappers,
   1.384 -	haz_netpair  = haz_netpair,
   1.385 -	dup_netpair  = dup_netpair,
   1.386 -	xtra_netpair = xtra_netpair}
   1.387 +        safep_netpair = insert (nI,nE) ([], safep_rls) safep_netpair,
   1.388 +        safeIs  = safeIs,
   1.389 +        hazIs   = hazIs,
   1.390 +        hazEs   = hazEs,
   1.391 +        xtraIs  = xtraIs,
   1.392 +        xtraEs  = xtraEs,
   1.393 +        swrappers    = swrappers,
   1.394 +        uwrappers    = uwrappers,
   1.395 +        haz_netpair  = haz_netpair,
   1.396 +        dup_netpair  = dup_netpair,
   1.397 +        xtra_netpair = xtra_netpair}
   1.398    end;
   1.399  
   1.400  fun rev_foldl f (e, l) = foldl f (e, rev l);
   1.401 @@ -401,117 +401,117 @@
   1.402  val op addSIs = rev_foldl addSI;
   1.403  val op addSEs = rev_foldl addSE;
   1.404  
   1.405 -fun cs addSDs ths = cs addSEs (map make_elim ths);
   1.406 +fun cs addSDs ths = cs addSEs (map Data.make_elim ths);
   1.407  
   1.408  
   1.409  (*** Hazardous (unsafe) rules ***)
   1.410  
   1.411  fun addI (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
   1.412 -		   safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair},
   1.413 -	  th)=
   1.414 +                   safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair},
   1.415 +          th)=
   1.416    if mem_thm (th, hazIs) then 
   1.417 -	 (warning ("Ignoring duplicate introduction (intro)\n" ^ string_of_thm th);
   1.418 -	  cs)
   1.419 +         (warning ("Ignoring duplicate introduction (intro)\n" ^ string_of_thm th);
   1.420 +          cs)
   1.421    else
   1.422    let val nI = length hazIs + 1
   1.423        and nE = length hazEs
   1.424    in warn_dup th cs;
   1.425 -     CS{hazIs	= th::hazIs,
   1.426 -	haz_netpair = insert (nI,nE) ([th], []) haz_netpair,
   1.427 -	dup_netpair = insert (nI,nE) (map dup_intr [th], []) dup_netpair,
   1.428 -	safeIs 	= safeIs, 
   1.429 -	safeEs	= safeEs,
   1.430 -	hazEs	= hazEs,
   1.431 -	xtraIs	= xtraIs,
   1.432 -	xtraEs	= xtraEs,
   1.433 -	swrappers     = swrappers,
   1.434 -	uwrappers     = uwrappers,
   1.435 -	safe0_netpair = safe0_netpair,
   1.436 -	safep_netpair = safep_netpair,
   1.437 -	xtra_netpair = xtra_netpair}
   1.438 +     CS{hazIs   = th::hazIs,
   1.439 +        haz_netpair = insert (nI,nE) ([th], []) haz_netpair,
   1.440 +        dup_netpair = insert (nI,nE) (map dup_intr [th], []) dup_netpair,
   1.441 +        safeIs  = safeIs, 
   1.442 +        safeEs  = safeEs,
   1.443 +        hazEs   = hazEs,
   1.444 +        xtraIs  = xtraIs,
   1.445 +        xtraEs  = xtraEs,
   1.446 +        swrappers     = swrappers,
   1.447 +        uwrappers     = uwrappers,
   1.448 +        safe0_netpair = safe0_netpair,
   1.449 +        safep_netpair = safep_netpair,
   1.450 +        xtra_netpair = xtra_netpair}
   1.451    end;
   1.452  
   1.453  fun addE (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
   1.454 -		   safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair},
   1.455 -	  th) =
   1.456 +                   safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair},
   1.457 +          th) =
   1.458    if mem_thm (th, hazEs) then 
   1.459 -	 (warning ("Ignoring duplicate elimination (elim)\n" ^ string_of_thm th);
   1.460 -	  cs)
   1.461 +         (warning ("Ignoring duplicate elimination (elim)\n" ^ string_of_thm th);
   1.462 +          cs)
   1.463    else
   1.464    let val nI = length hazIs 
   1.465        and nE = length hazEs + 1
   1.466    in warn_dup th cs;
   1.467 -     CS{hazEs	= th::hazEs,
   1.468 -	haz_netpair = insert (nI,nE) ([], [th]) haz_netpair,
   1.469 -	dup_netpair = insert (nI,nE) ([], map dup_elim [th]) dup_netpair,
   1.470 -	safeIs	= safeIs, 
   1.471 -	safeEs	= safeEs,
   1.472 -	hazIs	= hazIs,
   1.473 -	xtraIs	= xtraIs,
   1.474 -	xtraEs	= xtraEs,
   1.475 -	swrappers     = swrappers,
   1.476 -	uwrappers     = uwrappers,
   1.477 -	safe0_netpair = safe0_netpair,
   1.478 -	safep_netpair = safep_netpair,
   1.479 -	xtra_netpair = xtra_netpair}
   1.480 +     CS{hazEs   = th::hazEs,
   1.481 +        haz_netpair = insert (nI,nE) ([], [th]) haz_netpair,
   1.482 +        dup_netpair = insert (nI,nE) ([], map dup_elim [th]) dup_netpair,
   1.483 +        safeIs  = safeIs, 
   1.484 +        safeEs  = safeEs,
   1.485 +        hazIs   = hazIs,
   1.486 +        xtraIs  = xtraIs,
   1.487 +        xtraEs  = xtraEs,
   1.488 +        swrappers     = swrappers,
   1.489 +        uwrappers     = uwrappers,
   1.490 +        safe0_netpair = safe0_netpair,
   1.491 +        safep_netpair = safep_netpair,
   1.492 +        xtra_netpair = xtra_netpair}
   1.493    end;
   1.494  
   1.495  val op addIs = rev_foldl addI;
   1.496  val op addEs = rev_foldl addE;
   1.497  
   1.498 -fun cs addDs ths = cs addEs (map make_elim ths);
   1.499 +fun cs addDs ths = cs addEs (map Data.make_elim ths);
   1.500  
   1.501  
   1.502  (*** Extra (single step) rules ***)
   1.503  
   1.504  fun addXI (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers,
   1.505 -		   safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair},
   1.506 -	  th)=
   1.507 +                   safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair},
   1.508 +          th)=
   1.509    if mem_thm (th, xtraIs) then 
   1.510 -	 (warning ("Ignoring duplicate extra introduction (intro?)\n" ^ string_of_thm th);
   1.511 -	  cs)
   1.512 +         (warning ("Ignoring duplicate extra introduction (intro?)\n" ^ string_of_thm th);
   1.513 +          cs)
   1.514    else
   1.515    let val nI = length xtraIs + 1
   1.516        and nE = length xtraEs
   1.517    in warn_dup th cs;
   1.518 -     CS{xtraIs	= th::xtraIs,
   1.519 -	xtra_netpair = insert (nI,nE) ([th], []) xtra_netpair,
   1.520 -	safeIs 	= safeIs, 
   1.521 -	safeEs	= safeEs,
   1.522 -	hazIs	= hazIs,
   1.523 -	hazEs	= hazEs,
   1.524 -	xtraEs	= xtraEs,
   1.525 -	swrappers     = swrappers,
   1.526 -	uwrappers     = uwrappers,
   1.527 -	safe0_netpair = safe0_netpair,
   1.528 -	safep_netpair = safep_netpair,
   1.529 -	haz_netpair  = haz_netpair,
   1.530 -	dup_netpair  = dup_netpair}
   1.531 +     CS{xtraIs  = th::xtraIs,
   1.532 +        xtra_netpair = insert (nI,nE) ([th], []) xtra_netpair,
   1.533 +        safeIs  = safeIs, 
   1.534 +        safeEs  = safeEs,
   1.535 +        hazIs   = hazIs,
   1.536 +        hazEs   = hazEs,
   1.537 +        xtraEs  = xtraEs,
   1.538 +        swrappers     = swrappers,
   1.539 +        uwrappers     = uwrappers,
   1.540 +        safe0_netpair = safe0_netpair,
   1.541 +        safep_netpair = safep_netpair,
   1.542 +        haz_netpair  = haz_netpair,
   1.543 +        dup_netpair  = dup_netpair}
   1.544    end;
   1.545  
   1.546  fun addXE (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
   1.547 -		   safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair},
   1.548 -	  th) =
   1.549 +                   safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair},
   1.550 +          th) =
   1.551    if mem_thm (th, xtraEs) then
   1.552 -	 (warning ("Ignoring duplicate extra elimination (elim?)\n" ^ string_of_thm th);
   1.553 -	  cs)
   1.554 +         (warning ("Ignoring duplicate extra elimination (elim?)\n" ^ string_of_thm th);
   1.555 +          cs)
   1.556    else
   1.557    let val nI = length xtraIs 
   1.558        and nE = length xtraEs + 1
   1.559    in warn_dup th cs;
   1.560 -     CS{xtraEs	= th::xtraEs,
   1.561 -	xtra_netpair = insert (nI,nE) ([], [th]) xtra_netpair,
   1.562 -	safeIs	= safeIs, 
   1.563 -	safeEs	= safeEs,
   1.564 -	hazIs	= hazIs,
   1.565 -	hazEs	= hazEs,
   1.566 -	xtraIs	= xtraIs,
   1.567 -	swrappers     = swrappers,
   1.568 -	uwrappers     = uwrappers,
   1.569 -	safe0_netpair = safe0_netpair,
   1.570 -	safep_netpair = safep_netpair,
   1.571 -	haz_netpair  = haz_netpair,
   1.572 -	dup_netpair  = dup_netpair}
   1.573 +     CS{xtraEs  = th::xtraEs,
   1.574 +        xtra_netpair = insert (nI,nE) ([], [th]) xtra_netpair,
   1.575 +        safeIs  = safeIs, 
   1.576 +        safeEs  = safeEs,
   1.577 +        hazIs   = hazIs,
   1.578 +        hazEs   = hazEs,
   1.579 +        xtraIs  = xtraIs,
   1.580 +        swrappers     = swrappers,
   1.581 +        uwrappers     = uwrappers,
   1.582 +        safe0_netpair = safe0_netpair,
   1.583 +        safep_netpair = safep_netpair,
   1.584 +        haz_netpair  = haz_netpair,
   1.585 +        dup_netpair  = dup_netpair}
   1.586    end;
   1.587  
   1.588  infix 4 addXIs addXEs addXDs;
   1.589 @@ -519,144 +519,147 @@
   1.590  val op addXIs = rev_foldl addXI;
   1.591  val op addXEs = rev_foldl addXE;
   1.592  
   1.593 -fun cs addXDs ths = cs addXEs (map make_elim ths);
   1.594 +fun cs addXDs ths = cs addXEs (map Data.make_elim ths);
   1.595  
   1.596  
   1.597  (*** Deletion of rules 
   1.598       Working out what to delete, requires repeating much of the code used
   1.599 -	to insert.
   1.600 +        to insert.
   1.601       Separate functions delSI, etc., are not exported; instead delrules
   1.602          searches in all the lists and chooses the relevant delXX functions.
   1.603  ***)
   1.604  
   1.605  fun delSI th 
   1.606            (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers,
   1.607 -		    safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   1.608 +                    safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   1.609   if mem_thm (th, safeIs) then
   1.610     let val (safe0_rls, safep_rls) = partition Thm.no_prems [th]
   1.611     in CS{safe0_netpair = delete (safe0_rls, []) safe0_netpair,
   1.612 -	 safep_netpair = delete (safep_rls, []) safep_netpair,
   1.613 -	 safeIs	= rem_thm (safeIs,th),
   1.614 -	 safeEs	= safeEs,
   1.615 -	 hazIs	= hazIs,
   1.616 -	 hazEs	= hazEs,
   1.617 -	 xtraIs	= xtraIs,
   1.618 -	 xtraEs	= xtraEs,
   1.619 -	 swrappers    = swrappers,
   1.620 -	 uwrappers    = uwrappers,
   1.621 -	 haz_netpair  = haz_netpair,
   1.622 -	 dup_netpair  = dup_netpair,
   1.623 -	 xtra_netpair = xtra_netpair}
   1.624 +         safep_netpair = delete (safep_rls, []) safep_netpair,
   1.625 +         safeIs = rem_thm (safeIs,th),
   1.626 +         safeEs = safeEs,
   1.627 +         hazIs  = hazIs,
   1.628 +         hazEs  = hazEs,
   1.629 +         xtraIs = xtraIs,
   1.630 +         xtraEs = xtraEs,
   1.631 +         swrappers    = swrappers,
   1.632 +         uwrappers    = uwrappers,
   1.633 +         haz_netpair  = haz_netpair,
   1.634 +         dup_netpair  = dup_netpair,
   1.635 +         xtra_netpair = xtra_netpair}
   1.636     end
   1.637   else cs;
   1.638  
   1.639  fun delSE th
   1.640            (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
   1.641 -	            safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   1.642 +                    safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   1.643   if mem_thm (th, safeEs) then
   1.644     let val (safe0_rls, safep_rls) = partition (fn rl => nprems_of rl=1) [th]
   1.645     in CS{safe0_netpair = delete ([], safe0_rls) safe0_netpair,
   1.646 -	 safep_netpair = delete ([], safep_rls) safep_netpair,
   1.647 -	 safeIs	= safeIs,
   1.648 -	 safeEs	= rem_thm (safeEs,th),
   1.649 -	 hazIs	= hazIs,
   1.650 -	 hazEs	= hazEs,
   1.651 -	 xtraIs	= xtraIs,
   1.652 -	 xtraEs	= xtraEs,
   1.653 -	 swrappers    = swrappers,
   1.654 -	 uwrappers    = uwrappers,
   1.655 -	 haz_netpair  = haz_netpair,
   1.656 -	 dup_netpair  = dup_netpair,
   1.657 -	 xtra_netpair = xtra_netpair}
   1.658 +         safep_netpair = delete ([], safep_rls) safep_netpair,
   1.659 +         safeIs = safeIs,
   1.660 +         safeEs = rem_thm (safeEs,th),
   1.661 +         hazIs  = hazIs,
   1.662 +         hazEs  = hazEs,
   1.663 +         xtraIs = xtraIs,
   1.664 +         xtraEs = xtraEs,
   1.665 +         swrappers    = swrappers,
   1.666 +         uwrappers    = uwrappers,
   1.667 +         haz_netpair  = haz_netpair,
   1.668 +         dup_netpair  = dup_netpair,
   1.669 +         xtra_netpair = xtra_netpair}
   1.670     end
   1.671   else cs;
   1.672  
   1.673  
   1.674  fun delI th
   1.675           (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
   1.676 -	           safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   1.677 +                   safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   1.678   if mem_thm (th, hazIs) then
   1.679       CS{haz_netpair = delete ([th], []) haz_netpair,
   1.680 -	dup_netpair = delete ([dup_intr th], []) dup_netpair,
   1.681 -	safeIs 	= safeIs, 
   1.682 -	safeEs	= safeEs,
   1.683 -	hazIs	= rem_thm (hazIs,th),
   1.684 -	hazEs	= hazEs,
   1.685 -	xtraIs	= xtraIs,
   1.686 -	xtraEs	= xtraEs,
   1.687 -	swrappers     = swrappers,
   1.688 -	uwrappers     = uwrappers,
   1.689 -	safe0_netpair = safe0_netpair,
   1.690 -	safep_netpair = safep_netpair,
   1.691 -	xtra_netpair = xtra_netpair}
   1.692 +        dup_netpair = delete ([dup_intr th], []) dup_netpair,
   1.693 +        safeIs  = safeIs, 
   1.694 +        safeEs  = safeEs,
   1.695 +        hazIs   = rem_thm (hazIs,th),
   1.696 +        hazEs   = hazEs,
   1.697 +        xtraIs  = xtraIs,
   1.698 +        xtraEs  = xtraEs,
   1.699 +        swrappers     = swrappers,
   1.700 +        uwrappers     = uwrappers,
   1.701 +        safe0_netpair = safe0_netpair,
   1.702 +        safep_netpair = safep_netpair,
   1.703 +        xtra_netpair = xtra_netpair}
   1.704   else cs;
   1.705  
   1.706  fun delE th
   1.707 -	 (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
   1.708 -	           safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   1.709 +         (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
   1.710 +                   safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   1.711   if mem_thm (th, hazEs) then
   1.712       CS{haz_netpair = delete ([], [th]) haz_netpair,
   1.713 -	dup_netpair = delete ([], [dup_elim th]) dup_netpair,
   1.714 -	safeIs	= safeIs, 
   1.715 -	safeEs	= safeEs,
   1.716 -	hazIs	= hazIs,
   1.717 -	hazEs	= rem_thm (hazEs,th),
   1.718 -	xtraIs	= xtraIs,
   1.719 -	xtraEs	= xtraEs,
   1.720 -	swrappers     = swrappers,
   1.721 -	uwrappers     = uwrappers,
   1.722 -	safe0_netpair = safe0_netpair,
   1.723 -	safep_netpair = safep_netpair,
   1.724 -	xtra_netpair = xtra_netpair}
   1.725 +        dup_netpair = delete ([], [dup_elim th]) dup_netpair,
   1.726 +        safeIs  = safeIs, 
   1.727 +        safeEs  = safeEs,
   1.728 +        hazIs   = hazIs,
   1.729 +        hazEs   = rem_thm (hazEs,th),
   1.730 +        xtraIs  = xtraIs,
   1.731 +        xtraEs  = xtraEs,
   1.732 +        swrappers     = swrappers,
   1.733 +        uwrappers     = uwrappers,
   1.734 +        safe0_netpair = safe0_netpair,
   1.735 +        safep_netpair = safep_netpair,
   1.736 +        xtra_netpair = xtra_netpair}
   1.737   else cs;
   1.738  
   1.739  
   1.740  fun delXI th
   1.741           (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
   1.742 -	           safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   1.743 +                   safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   1.744   if mem_thm (th, xtraIs) then
   1.745       CS{xtra_netpair = delete ([th], []) xtra_netpair,
   1.746 -	safeIs 	= safeIs, 
   1.747 -	safeEs	= safeEs,
   1.748 -	hazIs	= hazIs,
   1.749 -	hazEs	= hazEs,
   1.750 -	xtraIs	= rem_thm (xtraIs,th),
   1.751 -	xtraEs	= xtraEs,
   1.752 -	swrappers     = swrappers,
   1.753 -	uwrappers     = uwrappers,
   1.754 -	safe0_netpair = safe0_netpair,
   1.755 -	safep_netpair = safep_netpair,
   1.756 -	haz_netpair  = haz_netpair,
   1.757 -	dup_netpair  = dup_netpair}
   1.758 +        safeIs  = safeIs, 
   1.759 +        safeEs  = safeEs,
   1.760 +        hazIs   = hazIs,
   1.761 +        hazEs   = hazEs,
   1.762 +        xtraIs  = rem_thm (xtraIs,th),
   1.763 +        xtraEs  = xtraEs,
   1.764 +        swrappers     = swrappers,
   1.765 +        uwrappers     = uwrappers,
   1.766 +        safe0_netpair = safe0_netpair,
   1.767 +        safep_netpair = safep_netpair,
   1.768 +        haz_netpair  = haz_netpair,
   1.769 +        dup_netpair  = dup_netpair}
   1.770   else cs;
   1.771  
   1.772  fun delXE th
   1.773 -	 (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
   1.774 -	           safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   1.775 +         (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
   1.776 +                   safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   1.777   if mem_thm (th, xtraEs) then
   1.778       CS{xtra_netpair = delete ([], [th]) xtra_netpair,
   1.779 -	safeIs	= safeIs, 
   1.780 -	safeEs	= safeEs,
   1.781 -	hazIs	= hazIs,
   1.782 -	hazEs	= hazEs,
   1.783 -	xtraIs	= xtraIs,
   1.784 -	xtraEs	= rem_thm (xtraEs,th),
   1.785 -	swrappers     = swrappers,
   1.786 -	uwrappers     = uwrappers,
   1.787 -	safe0_netpair = safe0_netpair,
   1.788 -	safep_netpair = safep_netpair,
   1.789 -	haz_netpair  = haz_netpair,
   1.790 -	dup_netpair  = dup_netpair}
   1.791 +        safeIs  = safeIs, 
   1.792 +        safeEs  = safeEs,
   1.793 +        hazIs   = hazIs,
   1.794 +        hazEs   = hazEs,
   1.795 +        xtraIs  = xtraIs,
   1.796 +        xtraEs  = rem_thm (xtraEs,th),
   1.797 +        swrappers     = swrappers,
   1.798 +        uwrappers     = uwrappers,
   1.799 +        safe0_netpair = safe0_netpair,
   1.800 +        safep_netpair = safep_netpair,
   1.801 +        haz_netpair  = haz_netpair,
   1.802 +        dup_netpair  = dup_netpair}
   1.803   else cs;
   1.804  
   1.805  (*Delete ALL occurrences of "th" in the claset (perhaps from several lists)*)
   1.806  fun delrule (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, ...}, th) =
   1.807 -       if mem_thm (th, safeIs) orelse mem_thm (th, safeEs) orelse
   1.808 -	  mem_thm (th, hazIs)  orelse mem_thm (th, hazEs) orelse
   1.809 -          mem_thm (th, xtraIs)  orelse mem_thm (th, xtraEs) 
   1.810 -       then delSI th (delSE th (delI th (delE th (delXI th (delXE th cs)))))
   1.811 -       else (warning ("Undeclared classical rule\n" ^ (string_of_thm th)); 
   1.812 -	     cs);
   1.813 +  let val th' = Data.make_elim th in
   1.814 +    if mem_thm (th, safeIs) orelse mem_thm (th, safeEs) orelse
   1.815 +      mem_thm (th, hazIs)  orelse mem_thm (th, hazEs) orelse
   1.816 +      mem_thm (th, xtraIs)  orelse mem_thm (th, xtraEs) orelse
   1.817 +      mem_thm (th', safeEs) orelse mem_thm (th', hazEs) orelse mem_thm (th', xtraEs)
   1.818 +    then delSI th (delSE th (delI th (delE th (delXI th (delXE th
   1.819 +      (delSE th' (delE th' (delXE th' cs))))))))
   1.820 +    else (warning ("Undeclared classical rule\n" ^ (string_of_thm th)); cs)
   1.821 +  end;
   1.822  
   1.823  val op delrules = foldl delrule;
   1.824  
   1.825 @@ -689,13 +692,13 @@
   1.826  (*Add/replace an unsafe wrapper*)
   1.827  fun cs addWrapper new_uwrapper = update_uwrappers cs (fn uwrappers =>
   1.828      overwrite_warn (uwrappers, new_uwrapper)
   1.829 -	("Overwriting unsafe wrapper "^fst new_uwrapper));
   1.830 +        ("Overwriting unsafe wrapper "^fst new_uwrapper));
   1.831  
   1.832  (*Remove a safe wrapper*)
   1.833  fun cs delSWrapper name = update_swrappers cs (fn swrappers =>
   1.834      let val (del,rest) = partition (fn (n,_) => n=name) swrappers
   1.835      in if null del then (warning ("No such safe wrapper in claset: "^ name); 
   1.836 -			 swrappers) else rest end);
   1.837 +                         swrappers) else rest end);
   1.838  
   1.839  (*Remove an unsafe wrapper*)
   1.840  fun cs delWrapper name = update_uwrappers cs (fn uwrappers =>
   1.841 @@ -730,7 +733,7 @@
   1.842  fun merge_cs
   1.843      (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, ...},
   1.844       CS{safeIs=safeIs2, safeEs=safeEs2, hazIs=hazIs2, hazEs=hazEs2,
   1.845 -        xtraIs=xtraIs2, xtraEs=xtraEs2,	swrappers, uwrappers, ...}) =
   1.846 +        xtraIs=xtraIs2, xtraEs=xtraEs2, swrappers, uwrappers, ...}) =
   1.847    let val safeIs' = gen_rems eq_thm (safeIs2,safeIs)
   1.848        val safeEs' = gen_rems eq_thm (safeEs2,safeEs)
   1.849        val  hazIs' = gen_rems eq_thm ( hazIs2, hazIs)
   1.850 @@ -738,11 +741,11 @@
   1.851        val xtraIs' = gen_rems eq_thm (xtraIs2, xtraIs)
   1.852        val xtraEs' = gen_rems eq_thm (xtraEs2, xtraEs)
   1.853        val cs1   = cs addSIs safeIs'
   1.854 -		     addSEs safeEs'
   1.855 -		     addIs  hazIs'
   1.856 -		     addEs  hazEs'
   1.857 -		     addXIs xtraIs'
   1.858 -		     addXEs xtraEs'
   1.859 +                     addSEs safeEs'
   1.860 +                     addIs  hazIs'
   1.861 +                     addEs  hazEs'
   1.862 +                     addXIs xtraIs'
   1.863 +                     addXEs xtraEs'
   1.864        val cs2 = update_swrappers cs1 (fn ws => merge_alists ws swrappers);
   1.865        val cs3 = update_uwrappers cs2 (fn ws => merge_alists ws uwrappers);
   1.866    in cs3 
   1.867 @@ -754,15 +757,15 @@
   1.868  (*Attack subgoals using safe inferences -- matching, not resolution*)
   1.869  fun safe_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) = 
   1.870    appSWrappers cs (FIRST' [
   1.871 -	eq_assume_tac,
   1.872 -	eq_mp_tac,
   1.873 -	bimatch_from_nets_tac safe0_netpair,
   1.874 -	FIRST' hyp_subst_tacs,
   1.875 -	bimatch_from_nets_tac safep_netpair]);
   1.876 +        eq_assume_tac,
   1.877 +        eq_mp_tac,
   1.878 +        bimatch_from_nets_tac safe0_netpair,
   1.879 +        FIRST' hyp_subst_tacs,
   1.880 +        bimatch_from_nets_tac safep_netpair]);
   1.881  
   1.882  (*Repeatedly attack a subgoal using safe inferences -- it's deterministic!*)
   1.883  fun safe_steps_tac cs = REPEAT_DETERM1 o 
   1.884 -	(fn i => COND (has_fewer_prems i) no_tac (safe_step_tac cs i));
   1.885 +        (fn i => COND (has_fewer_prems i) no_tac (safe_step_tac cs i));
   1.886  
   1.887  (*Repeatedly attack subgoals using safe inferences -- it's deterministic!*)
   1.888  fun safe_tac cs = REPEAT_DETERM1 (FIRSTGOAL (safe_steps_tac cs));
   1.889 @@ -788,10 +791,10 @@
   1.890  (*Attack subgoals using safe inferences -- matching, not resolution*)
   1.891  fun clarify_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) = 
   1.892    appSWrappers cs (FIRST' [
   1.893 -	eq_assume_contr_tac,
   1.894 -	bimatch_from_nets_tac safe0_netpair,
   1.895 -	FIRST' hyp_subst_tacs,
   1.896 -	n_bimatch_from_nets_tac 1 safep_netpair,
   1.897 +        eq_assume_contr_tac,
   1.898 +        bimatch_from_nets_tac safe0_netpair,
   1.899 +        FIRST' hyp_subst_tacs,
   1.900 +        n_bimatch_from_nets_tac 1 safep_netpair,
   1.901          bimatch2_tac safep_netpair]);
   1.902  
   1.903  fun clarify_tac cs = SELECT_GOAL (REPEAT_DETERM (clarify_step_tac cs 1));
   1.904 @@ -802,8 +805,8 @@
   1.905  (*Backtracking is allowed among the various these unsafe ways of
   1.906    proving a subgoal.  *)
   1.907  fun inst0_step_tac (CS{safe0_netpair,safep_netpair,...}) =
   1.908 -  assume_tac 			  APPEND' 
   1.909 -  contr_tac 			  APPEND' 
   1.910 +  assume_tac                      APPEND' 
   1.911 +  contr_tac                       APPEND' 
   1.912    biresolve_from_nets_tac safe0_netpair;
   1.913  
   1.914  (*These unsafe steps could generate more subgoals.*)
   1.915 @@ -818,12 +821,12 @@
   1.916  
   1.917  (*Single step for the prover.  FAILS unless it makes progress. *)
   1.918  fun step_tac cs i = safe_tac cs ORELSE appWrappers cs 
   1.919 -	(inst_step_tac cs ORELSE' haz_step_tac cs) i;
   1.920 +        (inst_step_tac cs ORELSE' haz_step_tac cs) i;
   1.921  
   1.922  (*Using a "safe" rule to instantiate variables is unsafe.  This tactic
   1.923    allows backtracking from "safe" rules to "unsafe" rules here.*)
   1.924  fun slow_step_tac cs i = safe_tac cs ORELSE appWrappers cs 
   1.925 -	(inst_step_tac cs APPEND' haz_step_tac cs) i;
   1.926 +        (inst_step_tac cs APPEND' haz_step_tac cs) i;
   1.927  
   1.928  (**** The following tactics all fail unless they solve one goal ****)
   1.929  
   1.930 @@ -849,13 +852,13 @@
   1.931  
   1.932  fun astar_tac cs = 
   1.933    SELECT_GOAL ( ASTAR (has_fewer_prems 1
   1.934 -	      , fn level =>(fn thm =>size_of_thm thm + !weight_ASTAR *level)) 
   1.935 -	      (step_tac cs 1));
   1.936 +              , fn level =>(fn thm =>size_of_thm thm + !weight_ASTAR *level)) 
   1.937 +              (step_tac cs 1));
   1.938  
   1.939  fun slow_astar_tac cs = 
   1.940    SELECT_GOAL ( ASTAR (has_fewer_prems 1
   1.941 -	      , fn level =>(fn thm =>size_of_thm thm + !weight_ASTAR *level)) 
   1.942 -	      (slow_step_tac cs 1));
   1.943 +              , fn level =>(fn thm =>size_of_thm thm + !weight_ASTAR *level)) 
   1.944 +              (slow_step_tac cs 1));
   1.945  
   1.946  (**** Complete tactic, loosely based upon LeanTaP.  This tactic is the outcome
   1.947    of much experimentation!  Changing APPEND to ORELSE below would prove
   1.948 @@ -871,12 +874,12 @@
   1.949  (*Searching to depth m. A variant called nodup_depth_tac appears in clasimp.ML*)
   1.950  local
   1.951  fun slow_step_tac' cs = appWrappers cs 
   1.952 -	(instp_step_tac cs APPEND' dup_step_tac cs);
   1.953 +        (instp_step_tac cs APPEND' dup_step_tac cs);
   1.954  in fun depth_tac cs m i state = SELECT_GOAL 
   1.955     (safe_steps_tac cs 1 THEN_ELSE 
   1.956 -	(DEPTH_SOLVE (depth_tac cs m 1),
   1.957 -	 inst0_step_tac cs 1 APPEND COND (K (m=0)) no_tac
   1.958 -		(slow_step_tac' cs 1 THEN DEPTH_SOLVE (depth_tac cs (m-1) 1))
   1.959 +        (DEPTH_SOLVE (depth_tac cs m 1),
   1.960 +         inst0_step_tac cs 1 APPEND COND (K (m=0)) no_tac
   1.961 +                (slow_step_tac' cs 1 THEN DEPTH_SOLVE (depth_tac cs (m-1) 1))
   1.962          )) i state;
   1.963  end;
   1.964  
   1.965 @@ -886,12 +889,12 @@
   1.966    SUBGOAL 
   1.967      (fn (prem,i) =>
   1.968        let val deti =
   1.969 -	  (*No Vars in the goal?  No need to backtrack between goals.*)
   1.970 -	  case term_vars prem of
   1.971 -	      []	=> DETERM 
   1.972 -	    | _::_	=> I
   1.973 +          (*No Vars in the goal?  No need to backtrack between goals.*)
   1.974 +          case term_vars prem of
   1.975 +              []        => DETERM 
   1.976 +            | _::_      => I
   1.977        in  SELECT_GOAL (TRY (safe_tac cs) THEN 
   1.978 -		       DEPTH_SOLVE (deti (depth_tac cs m 1))) i
   1.979 +                       DEPTH_SOLVE (deti (depth_tac cs m 1))) i
   1.980        end);
   1.981  
   1.982  fun deepen_tac cs = DEEPEN (2,10) (safe_depth_tac cs);
   1.983 @@ -983,7 +986,7 @@
   1.984  val xtra_dest_global = change_global_cs (op addXDs);
   1.985  val xtra_elim_global = change_global_cs (op addXEs);
   1.986  val xtra_intro_global = change_global_cs (op addXIs);
   1.987 -val delrule_global = change_global_cs (op delrules);
   1.988 +val rule_del_global = change_global_cs (op delrules);
   1.989  
   1.990  val safe_dest_local = change_local_cs (op addSDs);
   1.991  val safe_elim_local = change_local_cs (op addSEs);
   1.992 @@ -994,22 +997,22 @@
   1.993  val xtra_dest_local = change_local_cs (op addXDs);
   1.994  val xtra_elim_local = change_local_cs (op addXEs);
   1.995  val xtra_intro_local = change_local_cs (op addXIs);
   1.996 -val delrule_local = change_local_cs (op delrules);
   1.997 +val rule_del_local = change_local_cs (op delrules);
   1.998  
   1.999  
  1.1000  (* tactics referring to the implicit claset *)
  1.1001  
  1.1002  (*the abstraction over the proof state delays the dereferencing*)
  1.1003 -fun Safe_tac st		  = safe_tac (claset()) st;
  1.1004 -fun Safe_step_tac i st	  = safe_step_tac (claset()) i st;
  1.1005 +fun Safe_tac st           = safe_tac (claset()) st;
  1.1006 +fun Safe_step_tac i st    = safe_step_tac (claset()) i st;
  1.1007  fun Clarify_step_tac i st = clarify_step_tac (claset()) i st;
  1.1008 -fun Clarify_tac i st	  = clarify_tac (claset()) i st;
  1.1009 -fun Step_tac i st	  = step_tac (claset()) i st;
  1.1010 -fun Fast_tac i st	  = fast_tac (claset()) i st;
  1.1011 -fun Best_tac i st	  = best_tac (claset()) i st;
  1.1012 -fun Slow_tac i st	  = slow_tac (claset()) i st;
  1.1013 -fun Slow_best_tac i st	  = slow_best_tac (claset()) i st;
  1.1014 -fun Deepen_tac m	  = deepen_tac (claset()) m;
  1.1015 +fun Clarify_tac i st      = clarify_tac (claset()) i st;
  1.1016 +fun Step_tac i st         = step_tac (claset()) i st;
  1.1017 +fun Fast_tac i st         = fast_tac (claset()) i st;
  1.1018 +fun Best_tac i st         = best_tac (claset()) i st;
  1.1019 +fun Slow_tac i st         = slow_tac (claset()) i st;
  1.1020 +fun Slow_best_tac i st    = slow_best_tac (claset()) i st;
  1.1021 +fun Deepen_tac m          = deepen_tac (claset()) m;
  1.1022  
  1.1023  
  1.1024  end; 
  1.1025 @@ -1023,8 +1026,8 @@
  1.1026  val introN = "intro";
  1.1027  val elimN = "elim";
  1.1028  val destN = "dest";
  1.1029 +val ruleN = "rule";
  1.1030  val delN = "del";
  1.1031 -val delruleN = "delrule";
  1.1032  
  1.1033  val colon = Args.$$$ ":";
  1.1034  val query = Args.$$$ "?";
  1.1035 @@ -1036,19 +1039,21 @@
  1.1036    (Scan.lift ((query >> K xtra || bang >> K safe || Scan.succeed haz) >> change));
  1.1037  
  1.1038  fun cla_attr f g h = (cla_att change_global_cs f g h, cla_att change_local_cs f g h);
  1.1039 -val del_attr = (Attrib.no_args delrule_global, Attrib.no_args delrule_local);
  1.1040 +
  1.1041 +fun del_args att = Attrib.syntax (Scan.lift (Args.$$$ delN) >> K att);
  1.1042 +val rule_del_attr = (del_args rule_del_global, del_args rule_del_local);
  1.1043  
  1.1044  
  1.1045  (* setup_attrs *)
  1.1046  
  1.1047 -fun elimified x = Attrib.no_args (Drule.rule_attribute (K make_elim)) x;
  1.1048 +fun elimified x = Attrib.no_args (Drule.rule_attribute (K Data.make_elim)) x;
  1.1049  
  1.1050  val setup_attrs = Attrib.add_attributes
  1.1051   [("elimified", (elimified, elimified), "destruct rule turned into elimination rule (classical)"),
  1.1052    (destN, cla_attr (op addXDs) (op addDs) (op addSDs), "declaration of destruction rule"),
  1.1053    (elimN, cla_attr (op addXEs) (op addEs) (op addSEs), "declaration of elimination rule"),
  1.1054    (introN, cla_attr (op addXIs) (op addIs) (op addSIs), "declaration of introduction rule"),
  1.1055 -  (delruleN, del_attr, "remove declaration of elim/intro rule")];
  1.1056 +  (ruleN, rule_del_attr, "remove declaration of intro/elim/dest rule")];
  1.1057  
  1.1058  
  1.1059  
  1.1060 @@ -1153,7 +1158,7 @@
  1.1061    Args.$$$ introN -- query_colon >> K (I, xtra_intro_local),
  1.1062    Args.$$$ introN -- bang_colon >> K (I, safe_intro_local),
  1.1063    Args.$$$ introN -- colon >> K (I, haz_intro_local),
  1.1064 -  Args.$$$ delN -- colon >> K (I, delrule_local)];
  1.1065 +  Args.$$$ delN -- colon >> K (I, rule_del_local)];
  1.1066  
  1.1067  fun cla_meth tac prems ctxt = Method.METHOD (fn facts =>
  1.1068    ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (get_local_claset ctxt));