src/Provers/classical.ML
author paulson
Tue Jun 18 16:36:04 1996 +0200 (1996-06-18)
changeset 1814 89f8d4a88cca
parent 1807 3ff66483a8d4
child 1927 6f97cb16e453
permissions -rw-r--r--
Addition of Safe_step_tac
     1 (*  Title: 	Provers/classical
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1992  University of Cambridge
     5 
     6 Theorem prover for classical reasoning, including predicate calculus, set
     7 theory, etc.
     8 
     9 Rules must be classified as intr, elim, safe, hazardous.
    10 
    11 A rule is unsafe unless it can be applied blindly without harmful results.
    12 For a rule to be safe, its premises and conclusion should be logically
    13 equivalent.  There should be no variables in the premises that are not in
    14 the conclusion.
    15 *)
    16 
    17 infix 1 THEN_MAYBE;
    18 
    19 signature CLASSICAL_DATA =
    20   sig
    21   val mp	: thm    	(* [| P-->Q;  P |] ==> Q *)
    22   val not_elim	: thm		(* [| ~P;  P |] ==> R *)
    23   val classical	: thm		(* (~P ==> P) ==> P *)
    24   val sizef 	: thm -> int	(* size function for BEST_FIRST *)
    25   val hyp_subst_tacs: (int -> tactic) list
    26   end;
    27 
    28 (*Higher precedence than := facilitates use of references*)
    29 infix 4 addSIs addSEs addSDs addIs addEs addDs delrules
    30         setwrapper compwrapper addbefore addafter;
    31 
    32 
    33 signature CLASSICAL =
    34   sig
    35   type claset
    36   type netpair
    37   val empty_cs		: claset
    38   val merge_cs		: claset * claset -> claset
    39   val addDs 		: claset * thm list -> claset
    40   val addEs 		: claset * thm list -> claset
    41   val addIs 		: claset * thm list -> claset
    42   val addSDs		: claset * thm list -> claset
    43   val addSEs		: claset * thm list -> claset
    44   val addSIs		: claset * thm list -> claset
    45   val delrules		: claset * thm list -> claset
    46   val setwrapper 	: claset * (tactic->tactic) -> claset
    47   val compwrapper 	: claset * (tactic->tactic) -> claset
    48   val addbefore 	: claset * tactic -> claset
    49   val addafter 		: claset * tactic -> claset
    50 
    51   val print_cs		: claset -> unit
    52   val rep_claset	: 
    53       claset -> {safeIs: thm list, safeEs: thm list, 
    54 		 hazIs: thm list, hazEs: thm list,
    55 		 wrapper: tactic -> tactic,
    56 		 safe0_netpair: netpair, safep_netpair: netpair,
    57 		 haz_netpair: netpair, dup_netpair: netpair}
    58   val getwrapper	: claset -> tactic -> tactic
    59   val THEN_MAYBE	: tactic * tactic -> tactic
    60 
    61   val fast_tac 		: claset -> int -> tactic
    62   val slow_tac 		: claset -> int -> tactic
    63   val weight_ASTAR	: int ref
    64   val astar_tac		: claset -> int -> tactic
    65   val slow_astar_tac 	: claset -> int -> tactic
    66   val best_tac 		: claset -> int -> tactic
    67   val slow_best_tac 	: claset -> int -> tactic
    68   val depth_tac		: claset -> int -> int -> tactic
    69   val deepen_tac	: claset -> int -> int -> tactic
    70 
    71   val contr_tac 	: int -> tactic
    72   val dup_elim		: thm -> thm
    73   val dup_intr		: thm -> thm
    74   val dup_step_tac	: claset -> int -> tactic
    75   val eq_mp_tac		: int -> tactic
    76   val haz_step_tac 	: claset -> int -> tactic
    77   val joinrules 	: thm list * thm list -> (bool * thm) list
    78   val mp_tac		: int -> tactic
    79   val safe_tac 		: claset -> tactic
    80   val safe_step_tac 	: claset -> int -> tactic
    81   val step_tac 		: claset -> int -> tactic
    82   val swap		: thm                 (* ~P ==> (~Q ==> P) ==> Q *)
    83   val swapify 		: thm list -> thm list
    84   val swap_res_tac 	: thm list -> int -> tactic
    85   val inst_step_tac 	: claset -> int -> tactic
    86   val inst0_step_tac 	: claset -> int -> tactic
    87   val instp_step_tac 	: claset -> int -> tactic
    88 
    89   val claset : claset ref
    90   val AddDs 		: thm list -> unit
    91   val AddEs 		: thm list -> unit
    92   val AddIs 		: thm list -> unit
    93   val AddSDs		: thm list -> unit
    94   val AddSEs		: thm list -> unit
    95   val AddSIs		: thm list -> unit
    96   val Delrules		: thm list -> unit
    97   val Safe_step_tac	: int -> tactic
    98   val Step_tac 		: int -> tactic
    99   val Fast_tac 		: int -> tactic
   100   val Best_tac 		: int -> tactic
   101   val Deepen_tac	: int -> int -> tactic
   102 
   103   end;
   104 
   105 
   106 functor ClassicalFun(Data: CLASSICAL_DATA): CLASSICAL = 
   107 struct
   108 
   109 local open Data in
   110 
   111 (*** Useful tactics for classical reasoning ***)
   112 
   113 val imp_elim = (*cannot use bind_thm within a structure!*)
   114   store_thm ("imp_elim", make_elim mp);
   115 
   116 (*Solve goal that assumes both P and ~P. *)
   117 val contr_tac = eresolve_tac [not_elim]  THEN'  assume_tac;
   118 
   119 (*Finds P-->Q and P in the assumptions, replaces implication by Q.
   120   Could do the same thing for P<->Q and P... *)
   121 fun mp_tac i = eresolve_tac [not_elim, imp_elim] i  THEN  assume_tac i;
   122 
   123 (*Like mp_tac but instantiates no variables*)
   124 fun eq_mp_tac i = ematch_tac [not_elim, imp_elim] i  THEN  eq_assume_tac i;
   125 
   126 val swap =
   127   store_thm ("swap", rule_by_tactic (etac thin_rl 1) (not_elim RS classical));
   128 
   129 (*Creates rules to eliminate ~A, from rules to introduce A*)
   130 fun swapify intrs = intrs RLN (2, [swap]);
   131 
   132 (*Uses introduction rules in the normal way, or on negated assumptions,
   133   trying rules in order. *)
   134 fun swap_res_tac rls = 
   135     let fun addrl (rl,brls) = (false, rl) :: (true, rl RSN (2,swap)) :: brls
   136     in  assume_tac 	ORELSE' 
   137 	contr_tac 	ORELSE' 
   138         biresolve_tac (foldr addrl (rls,[]))
   139     end;
   140 
   141 (*Duplication of hazardous rules, for complete provers*)
   142 fun dup_intr th = standard (th RS classical);
   143 
   144 fun dup_elim th = th RSN (2, revcut_rl) |> assumption 2 |> Sequence.hd |> 
   145                   rule_by_tactic (TRYALL (etac revcut_rl));
   146 
   147 
   148 (**** Classical rule sets ****)
   149 
   150 type netpair = (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net;
   151 
   152 datatype claset =
   153   CS of {safeIs		: thm list,		(*safe introduction rules*)
   154 	 safeEs		: thm list,		(*safe elimination rules*)
   155 	 hazIs		: thm list,		(*unsafe introduction rules*)
   156 	 hazEs		: thm list,		(*unsafe elimination rules*)
   157 	 wrapper	: tactic->tactic,	(*for transforming step_tac*)
   158 	 safe0_netpair	: netpair,		(*nets for trivial cases*)
   159 	 safep_netpair	: netpair,		(*nets for >0 subgoals*)
   160 	 haz_netpair  	: netpair,		(*nets for unsafe rules*)
   161 	 dup_netpair	: netpair};		(*nets for duplication*)
   162 
   163 (*Desired invariants are
   164 	safe0_netpair = build safe0_brls,
   165 	safep_netpair = build safep_brls,
   166 	haz_netpair = build (joinrules(hazIs, hazEs)),
   167 	dup_netpair = build (joinrules(map dup_intr hazIs, 
   168 				       map dup_elim hazEs))}
   169 
   170 where build = build_netpair(Net.empty,Net.empty), 
   171       safe0_brls contains all brules that solve the subgoal, and
   172       safep_brls contains all brules that generate 1 or more new subgoals.
   173 The theorem lists are largely comments, though they are used in merge_cs.
   174 Nets must be built incrementally, to save space and time.
   175 *)
   176 
   177 val empty_cs = 
   178   CS{safeIs	= [],
   179      safeEs	= [],
   180      hazIs	= [],
   181      hazEs	= [],
   182      wrapper 	= I,
   183      safe0_netpair = (Net.empty,Net.empty),
   184      safep_netpair = (Net.empty,Net.empty),
   185      haz_netpair   = (Net.empty,Net.empty),
   186      dup_netpair   = (Net.empty,Net.empty)};
   187 
   188 fun print_cs (CS{safeIs,safeEs,hazIs,hazEs,...}) =
   189  (writeln"Introduction rules";  	prths hazIs;
   190   writeln"Safe introduction rules";  	prths safeIs;
   191   writeln"Elimination rules";  		prths hazEs;
   192   writeln"Safe elimination rules";  	prths safeEs;
   193   ());
   194 
   195 fun rep_claset (CS args) = args;
   196 
   197 fun getwrapper (CS{wrapper,...}) = wrapper;
   198 
   199 
   200 (*** Adding (un)safe introduction or elimination rules.
   201 
   202     In case of overlap, new rules are tried BEFORE old ones!!
   203 ***)
   204 
   205 (*For use with biresolve_tac.  Combines intr rules with swap to handle negated
   206   assumptions.  Pairs elim rules with true. *)
   207 fun joinrules (intrs,elims) =  
   208     (map (pair true) (elims @ swapify intrs)  @
   209      map (pair false) intrs);
   210 
   211 (*Priority: prefer rules with fewest subgoals, 
   212   then rules added most recently (preferring the head of the list).*)
   213 fun tag_brls k [] = []
   214   | tag_brls k (brl::brls) =
   215       (1000000*subgoals_of_brl brl + k, brl) :: 
   216       tag_brls (k+1) brls;
   217 
   218 fun insert_tagged_list kbrls netpr = foldr insert_tagged_brl (kbrls, netpr);
   219 
   220 (*Insert into netpair that already has nI intr rules and nE elim rules.
   221   Count the intr rules double (to account for swapify).  Negate to give the
   222   new insertions the lowest priority.*)
   223 fun insert (nI,nE) = insert_tagged_list o (tag_brls (~(2*nI+nE))) o joinrules;
   224 
   225 fun delete_tagged_list brls netpr = foldr delete_tagged_brl (brls, netpr);
   226 
   227 val delete = delete_tagged_list o joinrules;
   228 
   229 (*** Safe rules ***)
   230 
   231 fun (CS{safeIs, safeEs, hazIs, hazEs, wrapper, 
   232 	safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) 
   233     addSIs  ths  =
   234   let val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
   235           partition (fn rl => nprems_of rl=0) ths
   236       val nI = length safeIs + length ths
   237       and nE = length safeEs
   238   in CS{safeIs	= ths@safeIs,
   239         safe0_netpair = insert (nI,nE) (safe0_rls, []) safe0_netpair,
   240 	safep_netpair = insert (nI,nE) (safep_rls, []) safep_netpair,
   241 	safeEs	= safeEs,
   242 	hazIs	= hazIs,
   243 	hazEs	= hazEs,
   244 	wrapper = wrapper,
   245 	haz_netpair = haz_netpair,
   246 	dup_netpair = dup_netpair}
   247   end;
   248 
   249 fun (CS{safeIs, safeEs, hazIs, hazEs, wrapper, 
   250 	safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) 
   251     addSEs  ths  =
   252   let val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
   253           partition (fn rl => nprems_of rl=1) ths
   254       val nI = length safeIs
   255       and nE = length safeEs + length ths
   256   in 
   257      CS{safeEs	= ths@safeEs,
   258         safe0_netpair = insert (nI,nE) ([], safe0_rls) safe0_netpair,
   259 	safep_netpair = insert (nI,nE) ([], safep_rls) safep_netpair,
   260 	safeIs	= safeIs,
   261 	hazIs	= hazIs,
   262 	hazEs	= hazEs,
   263 	wrapper = wrapper,
   264 	haz_netpair = haz_netpair,
   265 	dup_netpair = dup_netpair}
   266   end;
   267 
   268 fun cs addSDs ths = cs addSEs (map make_elim ths);
   269 
   270 
   271 (*** Hazardous (unsafe) rules ***)
   272 
   273 fun (CS{safeIs, safeEs, hazIs, hazEs, wrapper, 
   274 	safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) 
   275     addIs  ths  =
   276   let val nI = length hazIs + length ths
   277       and nE = length hazEs
   278   in 
   279      CS{hazIs	= ths@hazIs,
   280 	haz_netpair = insert (nI,nE) (ths, []) haz_netpair,
   281 	dup_netpair = insert (nI,nE) (map dup_intr ths, []) dup_netpair,
   282 	safeIs 	= safeIs, 
   283 	safeEs	= safeEs,
   284 	hazEs	= hazEs,
   285 	wrapper 	= wrapper,
   286 	safe0_netpair = safe0_netpair,
   287 	safep_netpair = safep_netpair}
   288   end;
   289 
   290 fun (CS{safeIs, safeEs, hazIs, hazEs, wrapper, 
   291 	safe0_netpair, safep_netpair, haz_netpair, dup_netpair}) 
   292     addEs  ths  =
   293   let val nI = length hazIs 
   294       and nE = length hazEs + length ths
   295   in 
   296      CS{hazEs	= ths@hazEs,
   297 	haz_netpair = insert (nI,nE) ([], ths) haz_netpair,
   298 	dup_netpair = insert (nI,nE) ([], map dup_elim ths) dup_netpair,
   299 	safeIs	= safeIs, 
   300 	safeEs	= safeEs,
   301 	hazIs	= hazIs,
   302 	wrapper	= wrapper,
   303 	safe0_netpair = safe0_netpair,
   304 	safep_netpair = safep_netpair}
   305   end;
   306 
   307 fun cs addDs ths = cs addEs (map make_elim ths);
   308 
   309 
   310 (*** Deletion of rules 
   311      Working out what to delete, requires repeating much of the code used
   312 	to insert.
   313      Separate functions delSIs, etc., are not exported; instead delrules
   314         searches in all the lists and chooses the relevant delXX function.
   315 ***)
   316 
   317 fun delSIs (CS{safeIs, safeEs, hazIs, hazEs, wrapper, 
   318                safe0_netpair, safep_netpair, haz_netpair, dup_netpair},
   319             th) =
   320   let val (safe0_rls, safep_rls) = partition (fn rl => nprems_of rl=0) [th]
   321   in CS{safeIs	= gen_rem eq_thm (safeIs,th),
   322         safe0_netpair = delete (safe0_rls, []) safe0_netpair,
   323 	safep_netpair = delete (safep_rls, []) safep_netpair,
   324 	safeEs	= safeEs,
   325 	hazIs	= hazIs,
   326 	hazEs	= hazEs,
   327 	wrapper = wrapper,
   328 	haz_netpair = haz_netpair,
   329 	dup_netpair = dup_netpair}
   330   end;
   331 
   332 fun delSEs (CS{safeIs, safeEs, hazIs, hazEs, wrapper, 
   333 	       safe0_netpair, safep_netpair, haz_netpair, dup_netpair},
   334             th) =
   335   let val (safe0_rls, safep_rls) = partition (fn rl => nprems_of rl=1) [th]
   336   in CS{safeEs	= gen_rem eq_thm (safeEs,th),
   337         safe0_netpair = delete ([], safe0_rls) safe0_netpair,
   338 	safep_netpair = delete ([], safep_rls) safep_netpair,
   339 	safeIs	= safeIs,
   340 	hazIs	= hazIs,
   341 	hazEs	= hazEs,
   342 	wrapper = wrapper,
   343 	haz_netpair = haz_netpair,
   344 	dup_netpair = dup_netpair}
   345   end;
   346 
   347 
   348 fun delIs (CS{safeIs, safeEs, hazIs, hazEs, wrapper, 
   349 	      safe0_netpair, safep_netpair, haz_netpair, dup_netpair},
   350 	   th) =
   351      CS{hazIs	= gen_rem eq_thm (hazIs,th),
   352 	haz_netpair = delete ([th], []) haz_netpair,
   353 	dup_netpair = delete ([dup_intr th], []) dup_netpair,
   354 	safeIs 	= safeIs, 
   355 	safeEs	= safeEs,
   356 	hazEs	= hazEs,
   357 	wrapper 	= wrapper,
   358 	safe0_netpair = safe0_netpair,
   359 	safep_netpair = safep_netpair};
   360 
   361 fun delEs (CS{safeIs, safeEs, hazIs, hazEs, wrapper, 
   362 	      safe0_netpair, safep_netpair, haz_netpair, dup_netpair},
   363 	   th) =
   364      CS{hazEs	= gen_rem eq_thm (hazEs,th),
   365 	haz_netpair = delete ([], [th]) haz_netpair,
   366 	dup_netpair = delete ([], [dup_elim th]) dup_netpair,
   367 	safeIs	= safeIs, 
   368 	safeEs	= safeEs,
   369 	hazIs	= hazIs,
   370 	wrapper	= wrapper,
   371 	safe0_netpair = safe0_netpair,
   372 	safep_netpair = safep_netpair};
   373 
   374 fun delrule (cs as CS{safeIs, safeEs, hazIs, hazEs, ...}, th) =
   375        if gen_mem eq_thm (th, safeIs) then delSIs(cs,th)
   376   else if gen_mem eq_thm (th, safeEs) then delSEs(cs,th)
   377   else if gen_mem eq_thm (th, hazIs) then delIs(cs,th)
   378   else if gen_mem eq_thm (th, hazEs) then delEs(cs,th)
   379   else (warning ("rule not in claset\n" ^ (string_of_thm th)); 
   380 	cs);
   381 
   382 val op delrules = foldl delrule;
   383 
   384 
   385 (*** Setting or modifying the wrapper tactical ***)
   386 
   387 (*Set a new wrapper*)
   388 fun (CS{safeIs, safeEs, hazIs, hazEs, 
   389 	safe0_netpair, safep_netpair, haz_netpair, dup_netpair, ...}) 
   390     setwrapper new_wrapper  =
   391   CS{wrapper 	= new_wrapper,
   392      safeIs	= safeIs,
   393      safeEs	= safeEs,
   394      hazIs	= hazIs,
   395      hazEs	= hazEs,
   396      safe0_netpair = safe0_netpair,
   397      safep_netpair = safep_netpair,
   398      haz_netpair = haz_netpair,
   399      dup_netpair = dup_netpair};
   400 
   401 (*Compose a tactical with the existing wrapper*)
   402 fun cs compwrapper wrapper' = cs setwrapper (wrapper' o getwrapper cs);
   403 
   404 (*Execute tac1, but only execute tac2 if there are at least as many subgoals
   405   as before.  This ensures that tac2 is only applied to an outcome of tac1.*)
   406 fun tac1 THEN_MAYBE tac2 = 
   407   STATE (fn state =>
   408 	 tac1  THEN  
   409 	 COND (has_fewer_prems (nprems_of state)) all_tac tac2);
   410 
   411 (*Cause a tactic to be executed before/after the step tactic*)
   412 fun cs addbefore tac2 = cs compwrapper (fn tac1 => tac2 THEN_MAYBE tac1);
   413 fun cs addafter tac2  = cs compwrapper (fn tac1 => tac1 THEN_MAYBE tac2);
   414 
   415 
   416 (*Merge works by adding all new rules of the 2nd claset into the 1st claset.
   417   Merging the term nets may look more efficient, but the rather delicate
   418   treatment of priority might get muddled up.*)
   419 fun merge_cs
   420     (cs as CS{safeIs, safeEs, hazIs, hazEs, wrapper, ...},
   421      CS{safeIs=safeIs2, safeEs=safeEs2, hazIs=hazIs2, hazEs=hazEs2,...}) =
   422   let val safeIs' = gen_rems eq_thm (safeIs2,safeIs)
   423       val safeEs' = gen_rems eq_thm (safeEs2,safeEs)
   424       val hazIs' = gen_rems eq_thm (hazIs2,hazIs)
   425       val hazEs' = gen_rems eq_thm (hazEs2,hazEs)
   426   in cs addSIs safeIs'
   427         addSEs safeEs'
   428         addIs  hazIs'
   429         addEs  hazEs'
   430   end;
   431 
   432 
   433 (**** Simple tactics for theorem proving ****)
   434 
   435 (*Attack subgoals using safe inferences -- matching, not resolution*)
   436 fun safe_step_tac (CS{safe0_netpair,safep_netpair,...}) = 
   437   FIRST' [eq_assume_tac,
   438 	  eq_mp_tac,
   439 	  bimatch_from_nets_tac safe0_netpair,
   440 	  FIRST' hyp_subst_tacs,
   441 	  bimatch_from_nets_tac safep_netpair] ;
   442 
   443 (*Repeatedly attack subgoals using safe inferences -- it's deterministic!*)
   444 fun safe_tac cs = REPEAT_DETERM_FIRST (safe_step_tac cs);
   445 
   446 (*But these unsafe steps at least solve a subgoal!*)
   447 fun inst0_step_tac (CS{safe0_netpair,safep_netpair,...}) =
   448   assume_tac 			  APPEND' 
   449   contr_tac 			  APPEND' 
   450   biresolve_from_nets_tac safe0_netpair;
   451 
   452 (*These are much worse since they could generate more and more subgoals*)
   453 fun instp_step_tac (CS{safep_netpair,...}) =
   454   biresolve_from_nets_tac safep_netpair;
   455 
   456 (*These steps could instantiate variables and are therefore unsafe.*)
   457 fun inst_step_tac cs = inst0_step_tac cs APPEND' instp_step_tac cs;
   458 
   459 fun haz_step_tac (CS{haz_netpair,...}) = 
   460   biresolve_from_nets_tac haz_netpair;
   461 
   462 (*Single step for the prover.  FAILS unless it makes progress. *)
   463 fun step_tac cs i = 
   464   getwrapper cs 
   465     (FIRST [safe_tac cs, inst_step_tac cs i, haz_step_tac cs i]);
   466 
   467 (*Using a "safe" rule to instantiate variables is unsafe.  This tactic
   468   allows backtracking from "safe" rules to "unsafe" rules here.*)
   469 fun slow_step_tac cs i = 
   470   getwrapper cs 
   471     (safe_tac cs ORELSE (inst_step_tac cs i APPEND haz_step_tac cs i));
   472 
   473 (**** The following tactics all fail unless they solve one goal ****)
   474 
   475 (*Dumb but fast*)
   476 fun fast_tac cs = SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1));
   477 
   478 (*Slower but smarter than fast_tac*)
   479 fun best_tac cs = 
   480   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac cs 1));
   481 
   482 fun slow_tac cs = SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1));
   483 
   484 fun slow_best_tac cs = 
   485   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (slow_step_tac cs 1));
   486 
   487 
   488 (***ASTAR with weight weight_ASTAR, by Norbert Voelker*) 
   489 val weight_ASTAR = ref 5; 
   490 
   491 fun astar_tac cs = 
   492   SELECT_GOAL ( ASTAR (has_fewer_prems 1
   493 	      , fn level =>(fn thm =>size_of_thm thm + !weight_ASTAR *level)) 
   494 	      (step_tac cs 1));
   495 
   496 fun slow_astar_tac cs = 
   497   SELECT_GOAL ( ASTAR (has_fewer_prems 1
   498 	      , fn level =>(fn thm =>size_of_thm thm + !weight_ASTAR *level)) 
   499 	      (slow_step_tac cs 1));
   500 
   501 (**** Complete tactic, loosely based upon LeanTaP.  This tactic is the outcome
   502   of much experimentation!  Changing APPEND to ORELSE below would prove
   503   easy theorems faster, but loses completeness -- and many of the harder
   504   theorems such as 43. ****)
   505 
   506 (*Non-deterministic!  Could always expand the first unsafe connective.
   507   That's hard to implement and did not perform better in experiments, due to
   508   greater search depth required.*)
   509 fun dup_step_tac (cs as (CS{dup_netpair,...})) = 
   510   biresolve_from_nets_tac dup_netpair;
   511 
   512 (*Searching to depth m.*)
   513 fun depth_tac cs m i = STATE(fn state => 
   514   SELECT_GOAL 
   515     (REPEAT_DETERM1 (safe_step_tac cs 1) THEN_ELSE
   516      (DEPTH_SOLVE (depth_tac cs m 1),
   517       inst0_step_tac cs 1  APPEND
   518       COND (K(m=0)) no_tac
   519         ((instp_step_tac cs 1 APPEND dup_step_tac cs 1)
   520 	 THEN DEPTH_SOLVE (depth_tac cs (m-1) 1))))
   521   i);
   522 
   523 (*Iterative deepening tactical.  Allows us to "deepen" any search tactic*)
   524 fun DEEPEN tacf m i = STATE(fn state => 
   525    if has_fewer_prems i state then no_tac
   526    else (writeln ("Depth = " ^ string_of_int m);
   527 	 tacf m i  ORELSE  DEEPEN tacf (m+2) i));
   528 
   529 fun safe_depth_tac cs m = 
   530   SUBGOAL 
   531     (fn (prem,i) =>
   532       let val deti =
   533 	  (*No Vars in the goal?  No need to backtrack between goals.*)
   534 	  case term_vars prem of
   535 	      []	=> DETERM 
   536 	    | _::_	=> I
   537       in  SELECT_GOAL (TRY (safe_tac cs) THEN 
   538 		       DEPTH_SOLVE (deti (depth_tac cs m 1))) i
   539       end);
   540 
   541 fun deepen_tac cs = DEEPEN (safe_depth_tac cs);
   542 
   543 val claset = ref empty_cs;
   544 
   545 fun AddDs ts = (claset := !claset addDs ts);
   546 
   547 fun AddEs ts = (claset := !claset addEs ts);
   548 
   549 fun AddIs ts = (claset := !claset addIs ts);
   550 
   551 fun AddSDs ts = (claset := !claset addSDs ts);
   552 
   553 fun AddSEs ts = (claset := !claset addSEs ts);
   554 
   555 fun AddSIs ts = (claset := !claset addSIs ts);
   556 
   557 fun Delrules ts = (claset := !claset delrules ts);
   558 
   559 (*Cannot have Safe_tac, as it takes no arguments; must delay dereferencing!*)
   560 
   561 fun Safe_step_tac i = safe_step_tac (!claset) i; 
   562 
   563 fun Step_tac i = step_tac (!claset) i; 
   564 
   565 fun Fast_tac i = fast_tac (!claset) i; 
   566 
   567 fun Best_tac i = best_tac (!claset) i; 
   568 
   569 fun Deepen_tac m = deepen_tac (!claset) m; 
   570 
   571 end; 
   572 end;