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