changed wrapper mechanism of classical reasoner
authoroheimb
Wed Feb 25 15:51:24 1998 +0100 (1998-02-25)
changeset 465170dd492a1698
parent 4650 91af1ef45d68
child 4652 d24cca140eeb
changed wrapper mechanism of classical reasoner
src/HOL/Auth/Message.ML
src/HOL/IMP/Transition.ML
src/HOL/IOA/Solve.ML
src/HOL/TLA/TLA.ML
src/HOL/TLA/cladata.ML
src/HOL/simpdata.ML
src/Provers/blast.ML
src/Provers/classical.ML
     1.1 --- a/src/HOL/Auth/Message.ML	Wed Feb 25 15:48:04 1998 +0100
     1.2 +++ b/src/HOL/Auth/Message.ML	Wed Feb 25 15:51:24 1998 +0100
     1.3 @@ -316,7 +316,7 @@
     1.4  by (blast_tac (claset() addSEs [add_leE]) 2);
     1.5  (*Nonce case*)
     1.6  by (res_inst_tac [("x","N + Suc nat")] exI 1);
     1.7 -by (fast_tac (claset() addSEs [add_leE] addaltern trans_tac) 1);
     1.8 +by (fast_tac (claset() addSEs [add_leE] addaltern ("trans_tac",trans_tac)) 1);
     1.9  qed "msg_Nonce_supply";
    1.10  
    1.11  
     2.1 --- a/src/HOL/IMP/Transition.ML	Wed Feb 25 15:48:04 1998 +0100
     2.2 +++ b/src/HOL/IMP/Transition.ML	Wed Feb 25 15:51:24 1998 +0100
     2.3 @@ -200,7 +200,7 @@
     2.4    "(c,s) -*-> (c',s') ==> <c',s'> -c-> t --> <c,s> -c-> t";
     2.5  by (rtac (major RS rtrancl_induct2) 1);
     2.6  by (Fast_tac 1);
     2.7 -by (fast_tac (claset() addIs [FB_lemma3] addbefore split_all_tac) 1);
     2.8 +by (fast_tac (claset() addIs [FB_lemma3]) 1);
     2.9  qed_spec_mp "FB_lemma2";
    2.10  
    2.11  goal Transition.thy "!!c. (c,s) -*-> (SKIP,t) ==> <c,s> -c-> t";
     3.1 --- a/src/HOL/IOA/Solve.ML	Wed Feb 25 15:48:04 1998 +0100
     3.2 +++ b/src/HOL/IOA/Solve.ML	Wed Feb 25 15:51:24 1998 +0100
     3.3 @@ -73,7 +73,7 @@
     3.4  \    %i. fst (snd ex i))")]  bexI 1);
     3.5  (* fst(s) is in projected execution *)
     3.6   by (Simp_tac 1);
     3.7 - by (Fast_tac 1);
     3.8 + by (fast_tac (claset() delWrapper "split_all_tac") 1);
     3.9  (* projected execution is indeed an execution *)
    3.10  by (asm_full_simp_tac
    3.11        (simpset() addsimps [executions_def,is_execution_fragment_def,
    3.12 @@ -93,7 +93,7 @@
    3.13  \    %i. snd (snd ex i))")]  bexI 1);
    3.14  (* fst(s) is in projected execution *)
    3.15   by (Simp_tac 1);
    3.16 - by (Fast_tac 1);
    3.17 + by (fast_tac (claset() delWrapper "split_all_tac") 1);
    3.18  (* projected execution is indeed an execution *)
    3.19  by (asm_full_simp_tac
    3.20        (simpset() addsimps [executions_def,is_execution_fragment_def,
     4.1 --- a/src/HOL/TLA/TLA.ML	Wed Feb 25 15:48:04 1998 +0100
     4.2 +++ b/src/HOL/TLA/TLA.ML	Wed Feb 25 15:51:24 1998 +0100
     4.3 @@ -46,8 +46,8 @@
     4.4  AddSIs [tempI];
     4.5  AddDs [tempD];
     4.6  
     4.7 -val temp_cs = action_cs addSIs [tempI] addDs [tempD];
     4.8 -val temp_css = (temp_cs,simpset());
     4.9 +val temp_css = action_css addSIs2 [tempI] addDs2 [tempD];
    4.10 +val temp_cs = op addss temp_css;
    4.11  
    4.12  (* ========================================================================= *)
    4.13  section "Init";
    4.14 @@ -340,7 +340,7 @@
    4.15  (* Make these rewrites active by default *)
    4.16  Addsimps temp_simps;
    4.17  val temp_css = temp_css addsimps2 temp_simps;
    4.18 -val temp_cs = temp_cs addss (empty_ss addsimps temp_simps);
    4.19 +val temp_cs = op addss temp_css;
    4.20  
    4.21  
    4.22  (* ------------------------ Further rewrites ----------------------------------------- *)
     5.1 --- a/src/HOL/TLA/cladata.ML	Wed Feb 25 15:48:04 1998 +0100
     5.2 +++ b/src/HOL/TLA/cladata.ML	Wed Feb 25 15:51:24 1998 +0100
     5.3 @@ -42,10 +42,11 @@
     5.4    Add the new hyp_subst_tac to the wrapper (also for the default claset).
     5.5  **)
     5.6  
     5.7 -val action_cs = (HOL_cs addSIs [actionI,intI] addSEs [exE_prop] addDs [actionD,intD] 
     5.8 -                        addss simpset()) 
     5.9 -                addSaltern action_hyp_subst_tac;
    5.10 -val action_css = (action_cs, simpset());
    5.11 +val action_css = (HOL_cs addSIs [actionI,intI] addSEs [exE_prop] 
    5.12 +		  addDs  [actionD,intD] 
    5.13 +		  addSaltern ("action_hyp_subst_tac", action_hyp_subst_tac),
    5.14 +		 simpset());
    5.15 +val action_cs = op addss action_css;
    5.16  
    5.17  
    5.18  AddSIs [actionI,intI];
     6.1 --- a/src/HOL/simpdata.ML	Wed Feb 25 15:48:04 1998 +0100
     6.2 +++ b/src/HOL/simpdata.ML	Wed Feb 25 15:51:24 1998 +0100
     6.3 @@ -447,8 +447,9 @@
     6.4  
     6.5  (*Add a simpset to a classical set!*)
     6.6  infix 4 addSss addss;
     6.7 -fun cs addSss ss = cs addSaltern (CHANGED o (safe_asm_more_full_simp_tac ss));
     6.8 -fun cs addss  ss = cs addbefore                        asm_full_simp_tac ss;
     6.9 +fun cs addSss ss = cs addSaltern ("safe_asm_more_full_simp_tac",
    6.10 +				  CHANGED o (safe_asm_more_full_simp_tac ss));
    6.11 +fun cs addss  ss = cs addbefore  ("asm_full_simp_tac", asm_full_simp_tac ss);
    6.12  
    6.13  fun Addss ss = (claset_ref() := claset() addss ss);
    6.14  
    6.15 @@ -485,7 +486,7 @@
    6.16  	   with dup_step_tac when they are combined by auto_tac *)
    6.17  	fun nodup_depth_tac cs m i state = 
    6.18  	  SELECT_GOAL 
    6.19 -	   (getWrapper cs
    6.20 +	   (appWrappers cs
    6.21  	    (fn i => REPEAT_DETERM1 (COND (has_fewer_prems i) no_tac
    6.22  				     (safe_step_tac cs i)) THEN_ELSE
    6.23  	     (DEPTH_SOLVE (nodup_depth_tac cs m i),
     7.1 --- a/src/Provers/blast.ML	Wed Feb 25 15:48:04 1998 +0100
     7.2 +++ b/src/Provers/blast.ML	Wed Feb 25 15:51:24 1998 +0100
     7.3 @@ -11,7 +11,8 @@
     7.4  
     7.5  Blast_tac is often more powerful than fast_tac, but has some limitations.
     7.6  Blast_tac...
     7.7 -  * ignores addss, addbefore, addafter; this restriction is intrinsic
     7.8 +  * ignores wrappers (addss, addbefore, addafter, addWrapper, ...); 
     7.9 +    this restriction is intrinsic
    7.10    * ignores elimination rules that don't have the correct format
    7.11  	(conclusion must be a formula variable)
    7.12    * ignores types, which can make HOL proofs fail
    7.13 @@ -60,11 +61,11 @@
    7.14    val dup_intr		: thm -> thm
    7.15    val hyp_subst_tac     : bool ref -> int -> tactic
    7.16    val claset		: unit -> claset
    7.17 -  val rep_claset	: 
    7.18 +  val rep_claset	: (* dependent on classical.ML *)
    7.19        claset -> {safeIs: thm list, safeEs: thm list, 
    7.20  		 hazIs: thm list, hazEs: thm list,
    7.21 -		 uwrapper: (int -> tactic) -> (int -> tactic),
    7.22 -		 swrapper: (int -> tactic) -> (int -> tactic),
    7.23 +		 swrappers: (string * wrapper) list, 
    7.24 +		 uwrappers: (string * wrapper) list,
    7.25  		 safe0_netpair: netpair, safep_netpair: netpair,
    7.26  		 haz_netpair: netpair, dup_netpair: netpair}
    7.27    end;
     8.1 --- a/src/Provers/classical.ML	Wed Feb 25 15:48:04 1998 +0100
     8.2 +++ b/src/Provers/classical.ML	Wed Feb 25 15:51:24 1998 +0100
     8.3 @@ -16,12 +16,13 @@
     8.4  
     8.5  (*higher precedence than := facilitates use of references*)
     8.6  infix 4 addSIs addSEs addSDs addIs addEs addDs delrules
     8.7 -  setSWrapper compSWrapper setWrapper compWrapper
     8.8 +  addSWrapper delSWrapper addWrapper delWrapper
     8.9    addSbefore addSaltern addbefore addaltern;
    8.10  
    8.11  
    8.12  (*should be a type abbreviation in signature CLASSICAL*)
    8.13  type netpair = (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net;
    8.14 +type wrapper = (int -> tactic) -> (int -> tactic);
    8.15  
    8.16  signature CLASET_THY_DATA =
    8.17  sig
    8.18 @@ -48,11 +49,11 @@
    8.19    val empty_cs: claset
    8.20    val print_cs: claset -> unit
    8.21    val print_claset: theory -> unit
    8.22 -  val rep_claset:
    8.23 +  val rep_claset: (* BLAST_DATA in blast.ML dependent on this *)
    8.24      claset -> {safeIs: thm list, safeEs: thm list,
    8.25  		 hazIs: thm list, hazEs: thm list,
    8.26 -		 uwrapper: (int -> tactic) -> (int -> tactic),
    8.27 -		 swrapper: (int -> tactic) -> (int -> tactic),
    8.28 +		 swrappers: (string * wrapper) list, 
    8.29 +		 uwrappers: (string * wrapper) list,
    8.30  		 safe0_netpair: netpair, safep_netpair: netpair,
    8.31  		 haz_netpair: netpair, dup_netpair: netpair}
    8.32    val merge_cs		: claset * claset -> claset
    8.33 @@ -63,16 +64,16 @@
    8.34    val addSEs		: claset * thm list -> claset
    8.35    val addSIs		: claset * thm list -> claset
    8.36    val delrules		: claset * thm list -> claset
    8.37 -  val setSWrapper 	: claset * ((int -> tactic) -> (int -> tactic)) ->claset
    8.38 -  val compSWrapper 	: claset * ((int -> tactic) -> (int -> tactic)) ->claset
    8.39 -  val setWrapper 	: claset * ((int -> tactic) -> (int -> tactic)) ->claset
    8.40 -  val compWrapper 	: claset * ((int -> tactic) -> (int -> tactic)) ->claset
    8.41 -  val addSbefore 	: claset * (int -> tactic) -> claset
    8.42 -  val addSaltern 	: claset * (int -> tactic) -> claset
    8.43 -  val addbefore 	: claset * (int -> tactic) -> claset
    8.44 -  val addaltern	 	: claset * (int -> tactic) -> claset
    8.45 -  val getWrapper	: claset -> (int -> tactic) -> (int -> tactic)
    8.46 -  val getSWrapper	: claset -> (int -> tactic) -> (int -> tactic)
    8.47 +  val addSWrapper 	: claset * (string * wrapper) -> claset
    8.48 +  val delSWrapper 	: claset *  string            -> claset
    8.49 +  val addWrapper 	: claset * (string * wrapper) -> claset
    8.50 +  val delWrapper 	: claset *  string            -> claset
    8.51 +  val addSbefore 	: claset * (string * (int -> tactic)) -> claset
    8.52 +  val addSaltern 	: claset * (string * (int -> tactic)) -> claset
    8.53 +  val addbefore 	: claset * (string * (int -> tactic)) -> claset
    8.54 +  val addaltern	 	: claset * (string * (int -> tactic)) -> claset
    8.55 +  val appWrappers	: claset -> wrapper
    8.56 +  val appSWrappers	: claset -> wrapper
    8.57  
    8.58    val claset_ref_of_sg: Sign.sg -> claset ref
    8.59    val claset_ref_of: theory -> claset ref
    8.60 @@ -218,10 +219,8 @@
    8.61  	 safeEs		: thm list,		(*safe elimination rules*)
    8.62  	 hazIs		: thm list,		(*unsafe introduction rules*)
    8.63  	 hazEs		: thm list,		(*unsafe elimination rules*)
    8.64 -	 uwrapper	: (int -> tactic) ->
    8.65 -			  (int -> tactic),	(*for transforming step_tac*)
    8.66 -	 swrapper	: (int -> tactic) ->
    8.67 -			  (int -> tactic),	(*for safe_step_tac*)
    8.68 +	 swrappers	: (string * wrapper) list, (*for transf. safe_step_tac*)
    8.69 +	 uwrappers	: (string * wrapper) list, (*for transforming step_tac*)
    8.70  	 safe0_netpair	: netpair,		(*nets for trivial cases*)
    8.71  	 safep_netpair	: netpair,		(*nets for >0 subgoals*)
    8.72  	 haz_netpair  	: netpair,		(*nets for unsafe rules*)
    8.73 @@ -246,8 +245,8 @@
    8.74       safeEs	= [],
    8.75       hazIs	= [],
    8.76       hazEs	= [],
    8.77 -     uwrapper   = I,
    8.78 -     swrapper   = I,
    8.79 +     swrappers  = [],
    8.80 +     uwrappers  = [],
    8.81       safe0_netpair = (Net.empty,Net.empty),
    8.82       safep_netpair = (Net.empty,Net.empty),
    8.83       haz_netpair   = (Net.empty,Net.empty),
    8.84 @@ -263,11 +262,12 @@
    8.85  
    8.86  fun rep_claset (CS args) = args;
    8.87  
    8.88 -
    8.89 -fun getWrapper  (CS{uwrapper,...}) = uwrapper;
    8.90 -
    8.91 -fun getSWrapper (CS{swrapper,...}) = swrapper;
    8.92 -
    8.93 +local 
    8.94 +  fun calc_wrap l tac = foldr (fn ((name,tacf),w) => tacf w) (l, tac);
    8.95 +in 
    8.96 +  fun appSWrappers (CS{swrappers,...}) = calc_wrap swrappers;
    8.97 +  fun appWrappers  (CS{uwrappers,...}) = calc_wrap uwrappers;
    8.98 +end;
    8.99  
   8.100  
   8.101  (*** Adding (un)safe introduction or elimination rules.
   8.102 @@ -317,7 +317,7 @@
   8.103  
   8.104  (*** Safe rules ***)
   8.105  
   8.106 -fun addSI (cs as CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, 
   8.107 +fun addSI (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
   8.108  	      safe0_netpair, safep_netpair, haz_netpair, dup_netpair},
   8.109  	   th)  =
   8.110    if mem_thm (th, safeIs) then 
   8.111 @@ -335,13 +335,13 @@
   8.112  	safeEs	= safeEs,
   8.113  	hazIs	= hazIs,
   8.114  	hazEs	= hazEs,
   8.115 -	uwrapper     = uwrapper,
   8.116 -	swrapper     = swrapper,
   8.117 +	swrappers    = swrappers,
   8.118 +	uwrappers    = uwrappers,
   8.119  	haz_netpair  = haz_netpair,
   8.120  	dup_netpair  = dup_netpair}
   8.121    end;
   8.122  
   8.123 -fun addSE (cs as CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, 
   8.124 +fun addSE (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
   8.125  		    safe0_netpair, safep_netpair, haz_netpair, dup_netpair},
   8.126  	   th)  =
   8.127    if mem_thm (th, safeEs) then 
   8.128 @@ -359,8 +359,8 @@
   8.129  	safeIs	= safeIs,
   8.130  	hazIs	= hazIs,
   8.131  	hazEs	= hazEs,
   8.132 -	uwrapper     = uwrapper,
   8.133 -	swrapper     = swrapper,
   8.134 +	swrappers    = swrappers,
   8.135 +	uwrappers    = uwrappers,
   8.136  	haz_netpair  = haz_netpair,
   8.137  	dup_netpair  = dup_netpair}
   8.138    end;
   8.139 @@ -375,7 +375,7 @@
   8.140  
   8.141  (*** Hazardous (unsafe) rules ***)
   8.142  
   8.143 -fun addI (cs as CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, 
   8.144 +fun addI (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
   8.145  		   safe0_netpair, safep_netpair, haz_netpair, dup_netpair},
   8.146  	  th)=
   8.147    if mem_thm (th, hazIs) then 
   8.148 @@ -391,13 +391,13 @@
   8.149  	safeIs 	= safeIs, 
   8.150  	safeEs	= safeEs,
   8.151  	hazEs	= hazEs,
   8.152 -	uwrapper      = uwrapper,
   8.153 -	swrapper      = swrapper,
   8.154 +	swrappers     = swrappers,
   8.155 +	uwrappers     = uwrappers,
   8.156  	safe0_netpair = safe0_netpair,
   8.157  	safep_netpair = safep_netpair}
   8.158    end;
   8.159  
   8.160 -fun addE (cs as CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, 
   8.161 +fun addE (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
   8.162  		   safe0_netpair, safep_netpair, haz_netpair, dup_netpair},
   8.163  	  th) =
   8.164    if mem_thm (th, hazEs) then 
   8.165 @@ -413,8 +413,8 @@
   8.166  	safeIs	= safeIs, 
   8.167  	safeEs	= safeEs,
   8.168  	hazIs	= hazIs,
   8.169 -	uwrapper      = uwrapper,
   8.170 -	swrapper      = swrapper,
   8.171 +	swrappers     = swrappers,
   8.172 +	uwrappers     = uwrappers,
   8.173  	safe0_netpair = safe0_netpair,
   8.174  	safep_netpair = safep_netpair}
   8.175    end;
   8.176 @@ -433,7 +433,7 @@
   8.177  ***)
   8.178  
   8.179  fun delSI th 
   8.180 -          (cs as CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, 
   8.181 +          (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
   8.182  		    safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) =
   8.183   if mem_thm (th, safeIs) then
   8.184     let val (safe0_rls, safep_rls) = partition (fn rl => nprems_of rl=0) [th]
   8.185 @@ -443,15 +443,15 @@
   8.186  	 safeEs	= safeEs,
   8.187  	 hazIs	= hazIs,
   8.188  	 hazEs	= hazEs,
   8.189 -	 uwrapper     = uwrapper,
   8.190 -	 swrapper     = swrapper,
   8.191 +	 swrappers    = swrappers,
   8.192 +	 uwrappers    = uwrappers,
   8.193  	 haz_netpair  = haz_netpair,
   8.194  	 dup_netpair  = dup_netpair}
   8.195     end
   8.196   else cs;
   8.197  
   8.198  fun delSE th
   8.199 -          (cs as CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, 
   8.200 +          (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
   8.201  	            safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) =
   8.202   if mem_thm (th, safeEs) then
   8.203     let val (safe0_rls, safep_rls) = partition (fn rl => nprems_of rl=1) [th]
   8.204 @@ -461,8 +461,8 @@
   8.205  	 safeEs	= rem_thm (safeEs,th),
   8.206  	 hazIs	= hazIs,
   8.207  	 hazEs	= hazEs,
   8.208 -	 uwrapper     = uwrapper,
   8.209 -	 swrapper     = swrapper,
   8.210 +	 swrappers    = swrappers,
   8.211 +	 uwrappers    = uwrappers,
   8.212  	 haz_netpair  = haz_netpair,
   8.213  	 dup_netpair  = dup_netpair}
   8.214     end
   8.215 @@ -470,7 +470,7 @@
   8.216  
   8.217  
   8.218  fun delI th
   8.219 -         (cs as CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, 
   8.220 +         (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
   8.221  	           safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) =
   8.222   if mem_thm (th, hazIs) then
   8.223       CS{haz_netpair = delete ([th], []) haz_netpair,
   8.224 @@ -479,14 +479,14 @@
   8.225  	safeEs	= safeEs,
   8.226  	hazIs	= rem_thm (hazIs,th),
   8.227  	hazEs	= hazEs,
   8.228 -	uwrapper      = uwrapper,
   8.229 -	swrapper      = swrapper,
   8.230 +	swrappers     = swrappers,
   8.231 +	uwrappers     = uwrappers,
   8.232  	safe0_netpair = safe0_netpair,
   8.233  	safep_netpair = safep_netpair}
   8.234   else cs;
   8.235  
   8.236  fun delE th
   8.237 -	 (cs as CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper, 
   8.238 +	 (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
   8.239  	           safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) =
   8.240   if mem_thm (th, hazEs) then
   8.241       CS{haz_netpair = delete ([], [th]) haz_netpair,
   8.242 @@ -495,8 +495,8 @@
   8.243  	safeEs	= safeEs,
   8.244  	hazIs	= hazIs,
   8.245  	hazEs	= rem_thm (hazEs,th),
   8.246 -	uwrapper      = uwrapper,
   8.247 -	swrapper      = swrapper,
   8.248 +	swrappers     = swrappers,
   8.249 +	uwrappers     = uwrappers,
   8.250  	safe0_netpair = safe0_netpair,
   8.251  	safep_netpair = safep_netpair}
   8.252   else cs;
   8.253 @@ -514,49 +514,85 @@
   8.254  
   8.255  (*** Setting or modifying the wrapper tacticals ***)
   8.256  
   8.257 -(*Set a new uwrapper*)
   8.258 -fun (CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper,
   8.259 +(*Add/replace a safe wrapper*)
   8.260 +fun (CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
   8.261  	safe0_netpair, safep_netpair, haz_netpair, dup_netpair, ...}) 
   8.262 -    setWrapper new_uwrapper  =
   8.263 +    addSWrapper new_swrapper  =
   8.264    CS{safeIs	= safeIs,
   8.265       safeEs	= safeEs,
   8.266       hazIs	= hazIs,
   8.267       hazEs	= hazEs,
   8.268 -     uwrapper 	= new_uwrapper,
   8.269 -     swrapper   = swrapper,
   8.270 +     swrappers 	= (case assoc_string (swrappers,(fst new_swrapper)) of None =>()
   8.271 +	   | Some x => warning("overwriting safe wrapper "^fst new_swrapper); 
   8.272 +		   overwrite (swrappers, new_swrapper)),
   8.273 +     uwrappers  = uwrappers,
   8.274 +     safe0_netpair = safe0_netpair,
   8.275 +     safep_netpair = safep_netpair,
   8.276 +     haz_netpair = haz_netpair,
   8.277 +     dup_netpair = dup_netpair};
   8.278 +
   8.279 +(*Add/replace an unsafe wrapper*)
   8.280 +fun (CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
   8.281 +	safe0_netpair, safep_netpair, haz_netpair, dup_netpair, ...}) 
   8.282 +    addWrapper new_uwrapper =
   8.283 +  CS{safeIs	= safeIs,
   8.284 +     safeEs	= safeEs,
   8.285 +     hazIs	= hazIs,
   8.286 +     hazEs	= hazEs,
   8.287 +     swrappers   = swrappers,
   8.288 +     uwrappers 	= (case assoc_string (uwrappers,(fst new_uwrapper)) of None =>()
   8.289 +	   | Some x => warning ("overwriting unsafe wrapper "^fst new_uwrapper);
   8.290 +		   overwrite (uwrappers, new_uwrapper)),
   8.291       safe0_netpair = safe0_netpair,
   8.292       safep_netpair = safep_netpair,
   8.293       haz_netpair = haz_netpair,
   8.294       dup_netpair = dup_netpair};
   8.295  
   8.296 -(*Set a new swrapper*)
   8.297 -fun (CS{safeIs, safeEs, hazIs, hazEs, uwrapper, swrapper,
   8.298 +(*Remove a safe wrapper*)
   8.299 +fun (CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
   8.300  	safe0_netpair, safep_netpair, haz_netpair, dup_netpair, ...}) 
   8.301 -    setSWrapper new_swrapper  =
   8.302 +    delSWrapper name =
   8.303    CS{safeIs	= safeIs,
   8.304       safeEs	= safeEs,
   8.305       hazIs	= hazIs,
   8.306       hazEs	= hazEs,
   8.307 -     uwrapper   = uwrapper,
   8.308 -     swrapper   = new_swrapper,
   8.309 +     swrappers 	= (case assoc_string (swrappers, name) of None =>
   8.310 +	   warning("safe wrapper "^ name ^" not in claset") | Some x => (); 
   8.311 +		   filter_out (fn (n,f) => n = name) swrappers),
   8.312 +     uwrappers  = uwrappers,
   8.313       safe0_netpair = safe0_netpair,
   8.314       safep_netpair = safep_netpair,
   8.315       haz_netpair = haz_netpair,
   8.316       dup_netpair = dup_netpair};
   8.317  
   8.318 -(*Compose a tactical with the existing uwrapper*)
   8.319 -fun cs compWrapper  uwrapper' = cs setWrapper  (uwrapper' o getWrapper cs);
   8.320 -
   8.321 -(*Compose a tactical with the existing swrapper*)
   8.322 -fun cs compSWrapper swrapper' = cs setSWrapper (swrapper' o getSWrapper cs);
   8.323 +(*Remove an unsafe wrapper*)
   8.324 +fun (CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, 
   8.325 +	safe0_netpair, safep_netpair, haz_netpair, dup_netpair, ...}) 
   8.326 +    delWrapper name =
   8.327 +  CS{safeIs	= safeIs,
   8.328 +     safeEs	= safeEs,
   8.329 +     hazIs	= hazIs,
   8.330 +     hazEs	= hazEs,
   8.331 +     swrappers  = swrappers,
   8.332 +     uwrappers 	= (case assoc_string (uwrappers, name) of None =>
   8.333 +	   warning("unsafe wrapper "^ name ^" not in claset") | Some x => (); 
   8.334 +		   filter_out (fn (n,f) => n = name) uwrappers),
   8.335 +     safe0_netpair = safe0_netpair,
   8.336 +     safep_netpair = safep_netpair,
   8.337 +     haz_netpair = haz_netpair,
   8.338 +     dup_netpair = dup_netpair};
   8.339  
   8.340  (*compose a safe tactic sequentially before/alternatively after safe_step_tac*)
   8.341 -fun cs addSbefore tac1 = cs compSWrapper (fn tac2 => tac1 THEN_MAYBE' tac2);
   8.342 -fun cs addSaltern tac2 = cs compSWrapper (fn tac1 => tac1 ORELSE'     tac2);
   8.343 +fun cs addSbefore (name,tac1) = cs addSWrapper (name, 
   8.344 +					fn tac2 => tac1 THEN_MAYBE' tac2);
   8.345 +fun cs addSaltern (name,tac2) = cs addSWrapper (name,
   8.346 +					fn tac1 => tac1 ORELSE'     tac2);
   8.347  
   8.348  (*compose a tactic sequentially before/alternatively after the step tactic*)
   8.349 -fun cs addbefore  tac1 = cs compWrapper  (fn tac2 => tac1 THEN_MAYBE' tac2);
   8.350 -fun cs addaltern  tac2 = cs compWrapper  (fn tac1 => tac1 APPEND'     tac2);
   8.351 +fun cs addbefore  (name,tac1) = cs addWrapper  (name,
   8.352 +					fn tac2 => tac1 THEN_MAYBE' tac2);
   8.353 +fun cs addaltern  (name,tac2) = cs addWrapper  (name,
   8.354 +					fn tac1 => tac1 APPEND'     tac2);
   8.355  
   8.356  (*Merge works by adding all new rules of the 2nd claset into the 1st claset.
   8.357    Merging the term nets may look more efficient, but the rather delicate
   8.358 @@ -579,7 +615,7 @@
   8.359  
   8.360  (*Attack subgoals using safe inferences -- matching, not resolution*)
   8.361  fun safe_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) = 
   8.362 -  getSWrapper cs (FIRST' [
   8.363 +  appSWrappers cs (FIRST' [
   8.364  	eq_assume_tac,
   8.365  	eq_mp_tac,
   8.366  	bimatch_from_nets_tac safe0_netpair,
   8.367 @@ -610,7 +646,7 @@
   8.368  
   8.369  (*Attack subgoals using safe inferences -- matching, not resolution*)
   8.370  fun clarify_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) = 
   8.371 -  getSWrapper cs (FIRST' [
   8.372 +  appSWrappers cs (FIRST' [
   8.373  	eq_assume_contr_tac,
   8.374  	bimatch_from_nets_tac safe0_netpair,
   8.375  	FIRST' hyp_subst_tacs,
   8.376 @@ -640,12 +676,12 @@
   8.377    biresolve_from_nets_tac haz_netpair;
   8.378  
   8.379  (*Single step for the prover.  FAILS unless it makes progress. *)
   8.380 -fun step_tac cs i = getWrapper cs 
   8.381 +fun step_tac cs i = appWrappers cs 
   8.382  	(K (safe_tac cs) ORELSE' (inst_step_tac cs ORELSE' haz_step_tac cs)) i;
   8.383  
   8.384  (*Using a "safe" rule to instantiate variables is unsafe.  This tactic
   8.385    allows backtracking from "safe" rules to "unsafe" rules here.*)
   8.386 -fun slow_step_tac cs i = getWrapper cs 
   8.387 +fun slow_step_tac cs i = appWrappers cs 
   8.388  	(K (safe_tac cs) ORELSE' (inst_step_tac cs APPEND' haz_step_tac cs)) i;
   8.389  
   8.390  (**** The following tactics all fail unless they solve one goal ****)
   8.391 @@ -690,7 +726,7 @@
   8.392  (*Searching to depth m.*)
   8.393  fun depth_tac cs m i state = 
   8.394    SELECT_GOAL 
   8.395 -   (getWrapper cs
   8.396 +   (appWrappers cs
   8.397      (fn i => REPEAT_DETERM1 (COND (has_fewer_prems i) no_tac
   8.398  			     (safe_step_tac cs i)) THEN_ELSE
   8.399       (DEPTH_SOLVE (depth_tac cs m i),