src/Provers/blast.ML
author nipkow
Fri May 17 11:25:07 2002 +0200 (2002-05-17 ago)
changeset 13157 4a4599f78f18
parent 12902 a23dc0b7566f
child 13550 5a176b8dda84
permissions -rw-r--r--
allowed more general split rules to cope with div/mod 2
     1 (*  Title: 	Provers/blast.ML
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1997  University of Cambridge
     5 
     6 Generic tableau prover with proof reconstruction
     7 
     8   SKOLEMIZES ReplaceI WRONGLY: allow new vars in prems, or forbid such rules??
     9   Needs explicit instantiation of assumptions?
    10 
    11 
    12 Blast_tac is often more powerful than fast_tac, but has some limitations.
    13 Blast_tac...
    14   * ignores wrappers (addss, addbefore, addafter, addWrapper, ...); 
    15     this restriction is intrinsic
    16   * ignores elimination rules that don't have the correct format
    17 	(conclusion must be a formula variable)
    18   * ignores types, which can make HOL proofs fail
    19   * rules must not require higher-order unification, e.g. apply_type in ZF
    20     + message "Function Var's argument not a bound variable" relates to this
    21   * its proof strategy is more general but can actually be slower
    22 
    23 Known problems:
    24   "Recursive" chains of rules can sometimes exclude other unsafe formulae
    25 	from expansion.  This happens because newly-created formulae always
    26 	have priority over existing ones.  But obviously recursive rules 
    27 	such as transitivity are treated specially to prevent this.  Sometimes
    28 	the formulae get into the wrong order (see WRONG below).
    29 
    30   With overloading:
    31         Calls to Blast.overloaded (see HOL/Set.ML for examples) are needed
    32 	to tell Blast_tac when to retain some type information.  Make sure
    33 	you know the constant's internal name, which might be "op <=" or 
    34 	"Relation.op ^^".
    35 
    36   With substition for equalities (hyp_subst_tac):
    37         When substitution affects a haz formula or literal, it is moved
    38         back to the list of safe formulae.
    39         But there's no way of putting it in the right place.  A "moved" or
    40         "no DETERM" flag would prevent proofs failing here.
    41 *)
    42 
    43 (*Should be a type abbreviation?*)
    44 type netpair = (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net;
    45 
    46 
    47 (*Assumptions about constants:
    48   --The negation symbol is "Not"
    49   --The equality symbol is "op ="
    50   --The is-true judgement symbol is "Trueprop"
    51   --There are no constants named "*Goal* or "*False*"
    52 *)
    53 signature BLAST_DATA =
    54   sig
    55   type claset
    56   val notE		: thm		(* [| ~P;  P |] ==> R *)
    57   val ccontr		: thm		
    58   val contr_tac 	: int -> tactic
    59   val dup_intr		: thm -> thm
    60   val hyp_subst_tac     : bool ref -> int -> tactic
    61   val claset		: unit -> claset
    62   val rep_cs	: (* dependent on classical.ML *)
    63       claset -> {safeIs: thm list, safeEs: thm list, 
    64 		 hazIs: thm list, hazEs: thm list,
    65 		 swrappers: (string * wrapper) list, 
    66 		 uwrappers: (string * wrapper) list,
    67 		 safe0_netpair: netpair, safep_netpair: netpair,
    68 		 haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: ContextRules.netpair}
    69   val cla_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
    70   val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
    71   end;
    72 
    73 
    74 signature BLAST =
    75   sig
    76   type claset 
    77   exception TRANS of string    (*reports translation errors*)
    78   datatype term = 
    79       Const of string
    80     | TConst of string * term
    81     | Skolem of string * term option ref list
    82     | Free  of string
    83     | Var   of term option ref
    84     | Bound of int
    85     | Abs   of string*term
    86     | $  of term*term;
    87   type branch
    88   val depth_tac 	: claset -> int -> int -> tactic
    89   val blast_tac 	: claset -> int -> tactic
    90   val Blast_tac 	: int -> tactic
    91   val overloaded 	: string * (Term.typ -> Term.typ) -> unit
    92   val get_overloads	: unit -> (string * (Term.typ -> Term.typ)) list
    93   val setup		: (theory -> theory) list
    94   (*debugging tools*)
    95   val stats	        : bool ref
    96   val trace	        : bool ref
    97   val fullTrace	        : branch list list ref
    98   val fromType	        : (indexname * term) list ref -> Term.typ -> term
    99   val fromTerm	        : Term.term -> term
   100   val fromSubgoal       : Term.term -> term
   101   val instVars          : term -> (unit -> unit)
   102   val toTerm	        : int -> term -> Term.term
   103   val readGoal          : Sign.sg -> string -> term
   104   val tryInThy		: theory -> int -> string ->
   105 		  (int->tactic) list * branch list list * (int*int*exn) list
   106   val trygl		: claset -> int -> int ->
   107 		  (int->tactic) list * branch list list * (int*int*exn) list
   108   val Trygl		: int -> int -> 
   109                   (int->tactic) list * branch list list * (int*int*exn) list
   110   val normBr		: branch -> branch
   111   end;
   112 
   113 
   114 functor BlastFun(Data: BLAST_DATA) : BLAST = 
   115 struct
   116 
   117 type claset = Data.claset;
   118 
   119 val trace = ref false
   120 and stats = ref false;   (*for runtime and search statistics*)
   121 
   122 datatype term = 
   123     Const  of string
   124   | TConst of string * term    (*type of overloaded constant--as a term!*)
   125   | Skolem of string * term option ref list
   126   | Free   of string
   127   | Var    of term option ref
   128   | Bound  of int
   129   | Abs    of string*term
   130   | op $   of term*term;
   131 
   132 
   133 (** Basic syntactic operations **)
   134 
   135 fun is_Var (Var _) = true
   136   | is_Var _ = false;
   137 
   138 fun dest_Var (Var x) =  x;
   139 
   140 
   141 fun rand (f$x) = x;
   142 
   143 (* maps   (f, [t1,...,tn])  to  f(t1,...,tn) *)
   144 val list_comb : term * term list -> term = foldl (op $);
   145 
   146 
   147 (* maps   f(t1,...,tn)  to  (f, [t1,...,tn]) ; naturally tail-recursive*)
   148 fun strip_comb u : term * term list = 
   149     let fun stripc (f$t, ts) = stripc (f, t::ts)
   150         |   stripc  x =  x 
   151     in  stripc(u,[])  end;
   152 
   153 
   154 (* maps   f(t1,...,tn)  to  f , which is never a combination *)
   155 fun head_of (f$t) = head_of f
   156   | head_of u = u;
   157 
   158 
   159 (** Particular constants **)
   160 
   161 fun negate P = Const"Not" $ P;
   162 
   163 fun mkGoal P = Const"*Goal*" $ P;
   164 
   165 fun isGoal (Const"*Goal*" $ _) = true
   166   | isGoal _                   = false;
   167 
   168 val Trueprop = Term.Const("Trueprop", Type("o",[])-->propT);
   169 fun mk_tprop P = Term.$ (Trueprop, P);
   170 
   171 fun isTrueprop (Term.Const("Trueprop",_)) = true
   172   | isTrueprop _                          = false;
   173 
   174 
   175 (*** Dealing with overloaded constants ***)
   176 
   177 (*alist is a map from TVar names to Vars.  We need to unify the TVars
   178   faithfully in order to track overloading*)
   179 fun fromType alist (Term.Type(a,Ts)) = list_comb (Const a, 
   180 						  map (fromType alist) Ts)
   181   | fromType alist (Term.TFree(a,_)) = Free a
   182   | fromType alist (Term.TVar (ixn,_)) =
   183 	      (case (assoc_string_int(!alist,ixn)) of
   184 		   None => let val t' = Var(ref None)
   185 		           in  alist := (ixn, t') :: !alist;  t'
   186 			   end
   187 		 | Some v => v)
   188 
   189 local
   190 val overloads = ref ([]: (string * (Term.typ -> Term.typ)) list)
   191 in
   192 
   193 fun overloaded arg = (overloads := arg :: (!overloads));
   194 
   195 fun get_overloads() = !overloads;
   196 
   197 (*Convert a possibly overloaded Term.Const to a Blast.Const or Blast.TConst,
   198   converting its type to a Blast.term in the latter case.*)
   199 fun fromConst alist (a,T) =
   200   case assoc_string (!overloads, a) of
   201       None   => Const a		(*not overloaded*)
   202     | Some f => 
   203 	let val T' = f T
   204 		     handle Match => error
   205                 ("Blast_tac: unexpected type for overloaded constant " ^ a)
   206         in  TConst(a, fromType alist T')  end;
   207 
   208 end;
   209 
   210 
   211 (*Tests whether 2 terms are alpha-convertible; chases instantiations*)
   212 fun (Const a)      aconv (Const b)      = a=b
   213   | (TConst (a,ta)) aconv (TConst (b,tb)) = a=b andalso ta aconv tb
   214   | (Skolem (a,_)) aconv (Skolem (b,_)) = a=b  (*arglists must then be equal*)
   215   | (Free a)       aconv (Free b)       = a=b
   216   | (Var(ref(Some t))) aconv u          = t aconv u
   217   | t          aconv (Var(ref(Some u))) = t aconv u
   218   | (Var v)        aconv (Var w)        = v=w	(*both Vars are un-assigned*)
   219   | (Bound i)      aconv (Bound j)      = i=j
   220   | (Abs(_,t))     aconv (Abs(_,u))     = t aconv u
   221   | (f$t)          aconv (g$u)          = (f aconv g) andalso (t aconv u)
   222   | _ aconv _  =  false;
   223 
   224 
   225 fun mem_term (_, [])     = false
   226   | mem_term (t, t'::ts) = t aconv t' orelse mem_term(t,ts);
   227 
   228 fun ins_term(t,ts) = if mem_term(t,ts) then ts else t :: ts;
   229 
   230 fun mem_var (v: term option ref, []) = false
   231   | mem_var (v, v'::vs)              = v=v' orelse mem_var(v,vs);
   232 
   233 fun ins_var(v,vs) = if mem_var(v,vs) then vs else v :: vs;
   234 
   235 
   236 (** Vars **)
   237 
   238 (*Accumulates the Vars in the term, suppressing duplicates*)
   239 fun add_term_vars (Skolem(a,args),	vars) = add_vars_vars(args,vars)
   240   | add_term_vars (Var (v as ref None),	vars) = ins_var (v, vars)
   241   | add_term_vars (Var (ref (Some u)), vars)  = add_term_vars(u,vars)
   242   | add_term_vars (TConst (_,t),	vars) = add_term_vars(t,vars)
   243   | add_term_vars (Abs (_,body),	vars) = add_term_vars(body,vars)
   244   | add_term_vars (f$t,	vars) =  add_term_vars (f, add_term_vars(t, vars))
   245   | add_term_vars (_,	vars) = vars
   246 (*Term list version.  [The fold functionals are slow]*)
   247 and add_terms_vars ([],    vars) = vars
   248   | add_terms_vars (t::ts, vars) = add_terms_vars (ts, add_term_vars(t,vars))
   249 (*Var list version.*)
   250 and add_vars_vars ([],    vars) = vars
   251   | add_vars_vars (ref (Some u) :: vs, vars) = 
   252 	add_vars_vars (vs, add_term_vars(u,vars))
   253   | add_vars_vars (v::vs, vars) =   (*v must be a ref None*)
   254 	add_vars_vars (vs, ins_var (v, vars));
   255 
   256 
   257 (*Chase assignments in "vars"; return a list of unassigned variables*)
   258 fun vars_in_vars vars = add_vars_vars(vars,[]);
   259 
   260 
   261 
   262 (*increment a term's non-local bound variables
   263      inc is  increment for bound variables
   264      lev is  level at which a bound variable is considered 'loose'*)
   265 fun incr_bv (inc, lev, u as Bound i) = if i>=lev then Bound(i+inc) else u 
   266   | incr_bv (inc, lev, Abs(a,body)) = Abs(a, incr_bv(inc,lev+1,body))
   267   | incr_bv (inc, lev, f$t) = incr_bv(inc,lev,f) $ incr_bv(inc,lev,t)
   268   | incr_bv (inc, lev, u) = u;
   269 
   270 fun incr_boundvars  0  t = t
   271   | incr_boundvars inc t = incr_bv(inc,0,t);
   272 
   273 
   274 (*Accumulate all 'loose' bound vars referring to level 'lev' or beyond.
   275    (Bound 0) is loose at level 0 *)
   276 fun add_loose_bnos (Bound i, lev, js)   = if i<lev then js  
   277 					  else  (i-lev) ins_int js
   278   | add_loose_bnos (Abs (_,t), lev, js) = add_loose_bnos (t, lev+1, js)
   279   | add_loose_bnos (f$t, lev, js)       =
   280 	        add_loose_bnos (f, lev, add_loose_bnos (t, lev, js)) 
   281   | add_loose_bnos (_, _, js)           = js;
   282 
   283 fun loose_bnos t = add_loose_bnos (t, 0, []);
   284 
   285 fun subst_bound (arg, t) : term = 
   286   let fun subst (t as Bound i, lev) =
   287  	    if i<lev then  t    (*var is locally bound*)
   288 	    else  if i=lev then incr_boundvars lev arg
   289 		           else Bound(i-1)  (*loose: change it*)
   290 	| subst (Abs(a,body), lev) = Abs(a, subst(body,lev+1))
   291 	| subst (f$t, lev) =  subst(f,lev)  $  subst(t,lev)
   292 	| subst (t,lev)    = t
   293   in  subst (t,0)  end;
   294 
   295 
   296 (*Normalize...but not the bodies of ABSTRACTIONS*)
   297 fun norm t = case t of
   298     Skolem (a,args)      => Skolem(a, vars_in_vars args)
   299   | TConst(a,aT)         => TConst(a, norm aT)
   300   | (Var (ref None))     => t
   301   | (Var (ref (Some u))) => norm u
   302   | (f $ u) => (case norm f of
   303                     Abs(_,body) => norm (subst_bound (u, body))
   304                   | nf => nf $ norm u)
   305   | _ => t;
   306 
   307 
   308 (*Weak (one-level) normalize for use in unification*)
   309 fun wkNormAux t = case t of
   310     (Var v) => (case !v of
   311 		    Some u => wkNorm u
   312 		  | None   => t)
   313   | (f $ u) => (case wkNormAux f of
   314 		    Abs(_,body) => wkNorm (subst_bound (u, body))
   315 		  | nf          => nf $ u)
   316   | Abs (a,body) =>	(*eta-contract if possible*)
   317 	(case wkNormAux body of
   318 	     nb as (f $ t) => 
   319 		 if (0 mem_int loose_bnos f) orelse wkNorm t <> Bound 0
   320 		 then Abs(a,nb)
   321 		 else wkNorm (incr_boundvars ~1 f)
   322 	   | nb => Abs (a,nb))
   323   | _ => t
   324 and wkNorm t = case head_of t of
   325     Const _        => t
   326   | TConst _       => t
   327   | Skolem(a,args) => t
   328   | Free _         => t
   329   | _              => wkNormAux t;
   330 
   331 
   332 (*Does variable v occur in u?  For unification.  
   333   Dangling bound vars are also forbidden.*)
   334 fun varOccur v = 
   335   let fun occL lev [] = false	(*same as (exists occ), but faster*)
   336 	| occL lev (u::us) = occ lev u orelse occL lev us
   337       and occ lev (Var w) = 
   338 	      v=w orelse
   339               (case !w of None   => false
   340 	                | Some u => occ lev u)
   341         | occ lev (Skolem(_,args)) = occL lev (map Var args)
   342             (*ignore TConst, since term variables can't occur in types (?) *)
   343         | occ lev (Bound i)  = lev <= i
   344         | occ lev (Abs(_,u)) = occ (lev+1) u
   345         | occ lev (f$u)      = occ lev u  orelse  occ lev f
   346         | occ lev _          = false;
   347   in  occ 0  end;
   348 
   349 exception UNIFY;
   350 
   351 val trail = ref [] : term option ref list ref;
   352 val ntrail = ref 0;
   353 
   354 
   355 (*Restore the trail to some previous state: for backtracking*)
   356 fun clearTo n =
   357     while !ntrail<>n do
   358 	(hd(!trail) := None;
   359 	 trail := tl (!trail);
   360 	 ntrail := !ntrail - 1);
   361 
   362 
   363 (*First-order unification with bound variables.  
   364   "vars" is a list of variables local to the rule and NOT to be put
   365 	on the trail (no point in doing so)
   366 *)
   367 fun unify(vars,t,u) =
   368     let val n = !ntrail 
   369 	fun update (t as Var v, u) =
   370 	    if t aconv u then ()
   371 	    else if varOccur v u then raise UNIFY 
   372 	    else if mem_var(v, vars) then v := Some u
   373 		 else (*avoid updating Vars in the branch if possible!*)
   374 		      if is_Var u andalso mem_var(dest_Var u, vars)
   375 		      then dest_Var u := Some t
   376 		      else (v := Some u;
   377 			    trail := v :: !trail;  ntrail := !ntrail + 1)
   378 	fun unifyAux (t,u) = 
   379 	    case (wkNorm t,  wkNorm u) of
   380 		(nt as Var v,  nu) => update(nt,nu)
   381 	      | (nu,  nt as Var v) => update(nt,nu)
   382 	      | (TConst(a,at), TConst(b,bt)) => if a=b then unifyAux(at,bt)
   383 		                                else raise UNIFY
   384 	      | (Abs(_,t'),  Abs(_,u')) => unifyAux(t',u')
   385 		    (*NB: can yield unifiers having dangling Bound vars!*)
   386 	      | (f$t',  g$u') => (unifyAux(f,g); unifyAux(t',u'))
   387 	      | (nt,  nu)    => if nt aconv nu then () else raise UNIFY
   388     in  (unifyAux(t,u); true) handle UNIFY => (clearTo n; false)
   389     end;
   390 
   391 
   392 (*Convert from "real" terms to prototerms; eta-contract
   393   Code is duplicated with fromSubgoal.  Correct this?*)
   394 fun fromTerm t =
   395   let val alistVar = ref []
   396       and alistTVar = ref []
   397       fun from (Term.Const aT) = fromConst alistTVar aT
   398 	| from (Term.Free  (a,_)) = Free a
   399 	| from (Term.Bound i)     = Bound i
   400 	| from (Term.Var (ixn,T)) = 
   401 	      (case (assoc_string_int(!alistVar,ixn)) of
   402 		   None => let val t' = Var(ref None)
   403 		           in  alistVar := (ixn, t') :: !alistVar;  t'
   404 			   end
   405 		 | Some v => v)
   406 	| from (Term.Abs (a,_,u)) = 
   407 	      (case  from u  of
   408 		u' as (f $ Bound 0) => 
   409 		  if (0 mem_int loose_bnos f) then Abs(a,u')
   410 		  else incr_boundvars ~1 f 
   411 	      | u' => Abs(a,u'))
   412 	| from (Term.$ (f,u)) = from f $ from u
   413   in  from t  end;
   414 
   415 (*A debugging function: replaces all Vars by dummy Frees for visual inspection
   416   of whether they are distinct.  Function revert undoes the assignments.*)
   417 fun instVars t =
   418   let val name = ref "a"
   419       val updated = ref []
   420       fun inst (TConst(a,t)) = inst t
   421 	| inst (Var(v as ref None)) = (updated := v :: (!updated);
   422 				       v       := Some (Free ("?" ^ !name)); 
   423 				       name    := Symbol.bump_string (!name))
   424 	| inst (Abs(a,t))    = inst t
   425 	| inst (f $ u)       = (inst f; inst u)
   426 	| inst _             = ()
   427       fun revert() = seq (fn v => v:=None) (!updated)
   428   in  inst t; revert  end;
   429 
   430 
   431 (* A1==>...An==>B  goes to  [A1,...,An], where B is not an implication *)
   432 fun strip_imp_prems (Const"==>" $ (Const"Trueprop" $ A) $ B) = 
   433            A :: strip_imp_prems B
   434   | strip_imp_prems (Const"==>" $ A $ B) = A :: strip_imp_prems B
   435   | strip_imp_prems _ = [];
   436 
   437 (* A1==>...An==>B  goes to B, where B is not an implication *)
   438 fun strip_imp_concl (Const"==>" $ A $ B) = strip_imp_concl B
   439   | strip_imp_concl (Const"Trueprop" $ A) = A
   440   | strip_imp_concl A = A : term;
   441 
   442 
   443 (*** Conversion of Elimination Rules to Tableau Operations ***)
   444 
   445 exception ElimBadConcl and ElimBadPrem;
   446 
   447 (*The conclusion becomes the goal/negated assumption *False*: delete it!
   448   If we don't find it then the premise is ill-formed and could cause 
   449   PROOF FAILED*)
   450 fun delete_concl [] = raise ElimBadPrem
   451   | delete_concl (Const "*Goal*" $ (Var (ref (Some (Const"*False*")))) :: Ps) =
   452 	Ps
   453   | delete_concl (Const "Not" $ (Var (ref (Some (Const"*False*")))) :: Ps) =
   454 	Ps
   455   | delete_concl (P::Ps) = P :: delete_concl Ps;
   456 
   457 fun skoPrem vars (Const "all" $ Abs (_, P)) =
   458         skoPrem vars (subst_bound (Skolem (gensym "S_", vars), P))
   459   | skoPrem vars P = P;
   460 
   461 fun convertPrem t = 
   462     delete_concl (mkGoal (strip_imp_concl t) :: strip_imp_prems t);
   463 
   464 (*Expects elimination rules to have a formula variable as conclusion*)
   465 fun convertRule vars t =
   466   let val (P::Ps) = strip_imp_prems t
   467       val Var v   = strip_imp_concl t
   468   in  v := Some (Const"*False*");
   469       (P, map (convertPrem o skoPrem vars) Ps) 
   470   end
   471   handle Bind => raise ElimBadConcl;
   472 
   473 
   474 (*Like dup_elim, but puts the duplicated major premise FIRST*)
   475 fun rev_dup_elim th = th RSN (2, revcut_rl) |> assumption 2 |> Seq.hd;
   476 
   477 
   478 (*Rotate the assumptions in all new subgoals for the LIFO discipline*)
   479 local
   480   (*Count new hyps so that they can be rotated*)
   481   fun nNewHyps []                         = 0
   482     | nNewHyps (Const "*Goal*" $ _ :: Ps) = nNewHyps Ps
   483     | nNewHyps (P::Ps)                    = 1 + nNewHyps Ps;
   484 
   485   fun rot_tac [] i st      = Seq.single st
   486     | rot_tac (0::ks) i st = rot_tac ks (i+1) st
   487     | rot_tac (k::ks) i st = rot_tac ks (i+1) (rotate_rule (~k) i st);
   488 in
   489 fun rot_subgoals_tac (rot, rl) =
   490      rot_tac (if rot then map nNewHyps rl else []) 
   491 end;
   492 
   493 
   494 fun TRACE rl tac st i = if !trace then (prth rl; tac st i) else tac st i;
   495 
   496 (*Resolution/matching tactics: if upd then the proof state may be updated.
   497   Matching makes the tactics more deterministic in the presence of Vars.*)
   498 fun emtac upd rl = TRACE rl (if upd then etac rl else ematch_tac [rl]);
   499 fun rmtac upd rl = TRACE rl (if upd then rtac rl else match_tac [rl]);
   500 
   501 (*Tableau rule from elimination rule.  
   502   Flag "upd" says that the inference updated the branch.
   503   Flag "dup" requests duplication of the affected formula.*)
   504 fun fromRule vars rl = 
   505   let val trl = rl |> rep_thm |> #prop |> fromTerm |> convertRule vars
   506       fun tac (upd, dup,rot) i = 
   507 	emtac upd (if dup then rev_dup_elim rl else rl) i
   508 	THEN
   509 	rot_subgoals_tac (rot, #2 trl) i
   510   in Option.SOME (trl, tac) end
   511   handle ElimBadPrem => (*reject: prems don't preserve conclusion*)
   512 	    (warning("Ignoring weak elimination rule\n" ^ string_of_thm rl);
   513 	     Option.NONE)
   514        | ElimBadConcl => (*ignore: conclusion is not just a variable*)
   515 	   (if !trace then (warning("Ignoring ill-formed elimination rule:\n" ^
   516        	               "conclusion should be a variable\n" ^ string_of_thm rl))
   517 	    else ();
   518 	    Option.NONE);
   519 
   520 
   521 (*** Conversion of Introduction Rules ***)
   522 
   523 fun convertIntrPrem t = mkGoal (strip_imp_concl t) :: strip_imp_prems t;
   524 
   525 fun convertIntrRule vars t =
   526   let val Ps = strip_imp_prems t
   527       val P  = strip_imp_concl t
   528   in  (mkGoal P, map (convertIntrPrem o skoPrem vars) Ps) 
   529   end;
   530 
   531 (*Tableau rule from introduction rule.  
   532   Flag "upd" says that the inference updated the branch.
   533   Flag "dup" requests duplication of the affected formula.
   534   Since haz rules are now delayed, "dup" is always FALSE for
   535   introduction rules.*)
   536 fun fromIntrRule vars rl = 
   537   let val trl = rl |> rep_thm |> #prop |> fromTerm |> convertIntrRule vars
   538       fun tac (upd,dup,rot) i = 
   539 	 rmtac upd (if dup then Data.dup_intr rl else rl) i
   540 	 THEN
   541 	 rot_subgoals_tac (rot, #2 trl) i
   542   in (trl, tac) end;
   543 
   544 
   545 val dummyVar = Term.Var (("etc",0), dummyT);
   546 
   547 (*Convert from prototerms to ordinary terms with dummy types
   548   Ignore abstractions; identify all Vars; STOP at given depth*)
   549 fun toTerm 0 _             = dummyVar
   550   | toTerm d (Const a)     = Term.Const (a,dummyT)
   551   | toTerm d (TConst(a,_)) = Term.Const (a,dummyT)  (*no need to convert type*)
   552   | toTerm d (Skolem(a,_)) = Term.Const (a,dummyT)
   553   | toTerm d (Free a)      = Term.Free  (a,dummyT)
   554   | toTerm d (Bound i)     = Term.Bound i
   555   | toTerm d (Var _)       = dummyVar
   556   | toTerm d (Abs(a,_))    = dummyVar
   557   | toTerm d (f $ u)       = Term.$ (toTerm d f, toTerm (d-1) u);
   558 
   559 
   560 fun netMkRules P vars (nps: netpair list) =
   561   case P of
   562       (Const "*Goal*" $ G) =>
   563 	let val pG = mk_tprop (toTerm 2 G)
   564 	    val intrs = List.concat 
   565 		             (map (fn (inet,_) => Net.unify_term inet pG) 
   566 			      nps)
   567 	in  map (fromIntrRule vars o #2) (Tactic.orderlist intrs)  end
   568     | _ =>
   569 	let val pP = mk_tprop (toTerm 3 P)
   570 	    val elims = List.concat 
   571 		             (map (fn (_,enet) => Net.unify_term enet pP) 
   572 			      nps)
   573 	in  List.mapPartial (fromRule vars o #2) (Tactic.orderlist elims)  end;
   574 
   575 
   576 (*Pending formulae carry md (may duplicate) flags*)
   577 type branch = 
   578     {pairs: ((term*bool) list *	(*safe formulae on this level*)
   579                (term*bool) list) list,  (*haz formulae  on this level*)
   580      lits:   term list,                 (*literals: irreducible formulae*)
   581      vars:   term option ref list,      (*variables occurring in branch*)
   582      lim:    int};                      (*resource limit*)
   583 
   584 val fullTrace = ref[] : branch list list ref;
   585 
   586 (*Normalize a branch--for tracing*)
   587 fun norm2 (G,md) = (norm G, md);
   588 
   589 fun normLev (Gs,Hs) = (map norm2 Gs, map norm2 Hs);
   590 
   591 fun normBr {pairs, lits, vars, lim} =
   592      {pairs = map normLev pairs, 
   593       lits  = map norm lits, 
   594       vars  = vars, 
   595       lim   = lim};
   596 
   597 
   598 val dummyTVar = Term.TVar(("a",0), []);
   599 val dummyVar2 = Term.Var(("var",0), dummyT);
   600 
   601 (*convert Blast_tac's type representation to real types for tracing*)
   602 fun showType (Free a)  = Term.TFree (a,[])
   603   | showType (Var _)   = dummyTVar
   604   | showType t         =
   605       (case strip_comb t of
   606 	   (Const a, us) => Term.Type(a, map showType us)
   607 	 | _ => dummyT);
   608 
   609 (*Display top-level overloading if any*)
   610 fun topType (TConst(a,t)) = Some (showType t)
   611   | topType (Abs(a,t))    = topType t
   612   | topType (f $ u)       = (case topType f of
   613 				 None => topType u
   614 			       | some => some)
   615   | topType _             = None;
   616 
   617 
   618 (*Convert from prototerms to ordinary terms with dummy types for tracing*)
   619 fun showTerm d (Const a)     = Term.Const (a,dummyT)
   620   | showTerm d (TConst(a,_)) = Term.Const (a,dummyT)
   621   | showTerm d (Skolem(a,_)) = Term.Const (a,dummyT)
   622   | showTerm d (Free a)      = Term.Free  (a,dummyT)
   623   | showTerm d (Bound i)     = Term.Bound i
   624   | showTerm d (Var(ref(Some u))) = showTerm d u
   625   | showTerm d (Var(ref None))    = dummyVar2
   626   | showTerm d (Abs(a,t))    = if d=0 then dummyVar
   627 			       else Term.Abs(a, dummyT, showTerm (d-1) t)
   628   | showTerm d (f $ u)       = if d=0 then dummyVar
   629 			       else Term.$ (showTerm d f, showTerm (d-1) u);
   630 
   631 fun string_of sign d t = Sign.string_of_term sign (showTerm d t);
   632 
   633 fun traceTerm sign t = 
   634   let val t' = norm t
   635       val stm = string_of sign 8 t'
   636   in  
   637       case topType t' of
   638 	  None   => stm   (*no type to attach*)
   639 	| Some T => stm ^ "\t:: " ^ Sign.string_of_typ sign T
   640   end;
   641 
   642 
   643 val prs = std_output;
   644 
   645 (*Print tracing information at each iteration of prover*)
   646 fun tracing sign brs = 
   647   let fun printPairs (((G,_)::_,_)::_)  = prs(traceTerm sign G)
   648 	| printPairs (([],(H,_)::_)::_) = prs(traceTerm sign H ^ "\t (Unsafe)")
   649 	| printPairs _                 = ()
   650       fun printBrs (brs0 as {pairs, lits, lim, ...} :: brs) =
   651 	    (fullTrace := brs0 :: !fullTrace;
   652 	     seq (fn _ => prs "+") brs;
   653 	     prs (" [" ^ Int.toString lim ^ "] ");
   654 	     printPairs pairs;
   655 	     writeln"")
   656   in if !trace then printBrs (map normBr brs) else ()
   657   end;
   658 
   659 fun traceMsg s = if !trace then writeln s else ();
   660 
   661 (*Tracing: variables updated in the last branch operation?*)
   662 fun traceVars sign ntrl =
   663   if !trace then 
   664       (case !ntrail-ntrl of
   665 	    0 => ()
   666 	  | 1 => prs"\t1 variable UPDATED:"
   667 	  | n => prs("\t" ^ Int.toString n ^ " variables UPDATED:");
   668        (*display the instantiations themselves, though no variable names*)
   669        seq (fn v => prs("   " ^ string_of sign 4 (the (!v))))
   670            (List.take(!trail, !ntrail-ntrl));
   671        writeln"")
   672     else ();
   673 
   674 (*Tracing: how many new branches are created?*)
   675 fun traceNew prems =
   676     if !trace then 
   677         case length prems of
   678 	    0 => prs"branch closed by rule"
   679 	  | 1 => prs"branch extended (1 new subgoal)"
   680 	  | n => prs("branch split: "^ Int.toString n ^ " new subgoals")
   681     else ();
   682 
   683 
   684 
   685 (*** Code for handling equality: naive substitution, like hyp_subst_tac ***)
   686 
   687 (*Replace the ATOMIC term "old" by "new" in t*)  
   688 fun subst_atomic (old,new) t =
   689     let fun subst (Var(ref(Some u))) = subst u
   690 	  | subst (Abs(a,body))      = Abs(a, subst body)
   691 	  | subst (f$t)              = subst f $ subst t
   692 	  | subst t                  = if t aconv old then new else t
   693     in  subst t  end;
   694 
   695 (*Eta-contract a term from outside: just enough to reduce it to an atom*)
   696 fun eta_contract_atom (t0 as Abs(a, body)) = 
   697       (case  eta_contract2 body  of
   698         f $ Bound 0 => if (0 mem_int loose_bnos f) then t0
   699 		       else eta_contract_atom (incr_boundvars ~1 f)
   700       | _ => t0)
   701   | eta_contract_atom t = t
   702 and eta_contract2 (f$t) = f $ eta_contract_atom t
   703   | eta_contract2 t     = eta_contract_atom t;
   704 
   705 
   706 (*When can we safely delete the equality?
   707     Not if it equates two constants; consider 0=1.
   708     Not if it resembles x=t[x], since substitution does not eliminate x.
   709     Not if it resembles ?x=0; another goal could instantiate ?x to Suc(i)
   710   Prefer to eliminate Bound variables if possible.
   711   Result:  true = use as is,  false = reorient first *)
   712 
   713 (*Can t occur in u?  For substitution.  
   714   Does NOT examine the args of Skolem terms: substitution does not affect them.
   715   REFLEXIVE because hyp_subst_tac fails on x=x.*)
   716 fun substOccur t = 
   717   let (*NO vars are permitted in u except the arguments of t, if it is 
   718         a Skolem term.  This ensures that no equations are deleted that could
   719         be instantiated to a cycle.  For example, x=?a is rejected because ?a
   720 	could be instantiated to Suc(x).*)
   721       val vars = case t of
   722                      Skolem(_,vars) => vars
   723 		   | _ => []
   724       fun occEq u = (t aconv u) orelse occ u
   725       and occ (Var(ref(Some u))) = occEq u
   726         | occ (Var v)            = not (mem_var (v, vars))
   727 	| occ (Abs(_,u))         = occEq u
   728         | occ (f$u)              = occEq u  orelse  occEq f
   729         | occ (_)                = false;
   730   in  occEq  end;
   731 
   732 exception DEST_EQ;
   733 
   734 (*Take apart an equality (plain or overloaded).  NO constant Trueprop*)
   735 fun dest_eq (Const  "op ="     $ t $ u) = 
   736 		(eta_contract_atom t, eta_contract_atom u)
   737   | dest_eq (TConst("op =",_)  $ t $ u) = 
   738 		(eta_contract_atom t, eta_contract_atom u)
   739   | dest_eq _                           = raise DEST_EQ;
   740 
   741 (*Reject the equality if u occurs in (or equals!) t*)
   742 fun check (t,u,v) = if substOccur t u then raise DEST_EQ else v;
   743 
   744 (*IF the goal is an equality with a substitutable variable 
   745   THEN orient that equality ELSE raise exception DEST_EQ*)
   746 fun orientGoal (t,u) = case (t,u) of
   747        (Skolem _, _) => check(t,u,(t,u))	(*eliminates t*)
   748      | (_, Skolem _) => check(u,t,(u,t))	(*eliminates u*)
   749      | (Free _, _)   => check(t,u,(t,u))	(*eliminates t*)
   750      | (_, Free _)   => check(u,t,(u,t))	(*eliminates u*)
   751      | _             => raise DEST_EQ;
   752 
   753 (*Substitute through the branch if an equality goal (else raise DEST_EQ).
   754   Moves affected literals back into the branch, but it is not clear where
   755   they should go: this could make proofs fail.*)
   756 fun equalSubst sign (G, {pairs, lits, vars, lim}) = 
   757   let val (t,u) = orientGoal(dest_eq G)
   758       val subst = subst_atomic (t,u)
   759       fun subst2(G,md) = (subst G, md)
   760       (*substitute throughout list; extract affected formulae*)
   761       fun subForm ((G,md), (changed, pairs)) =
   762 	    let val nG = subst G
   763 	    in  if nG aconv G then (changed, (G,md)::pairs)
   764 		              else ((nG,md)::changed, pairs)
   765             end
   766       (*substitute throughout "stack frame"; extract affected formulae*)
   767       fun subFrame ((Gs,Hs), (changed, frames)) =
   768 	    let val (changed', Gs') = foldr subForm (Gs, (changed, []))
   769                 val (changed'', Hs') = foldr subForm (Hs, (changed', []))
   770             in  (changed'', (Gs',Hs')::frames)  end
   771       (*substitute throughout literals; extract affected ones*)
   772       fun subLit (lit, (changed, nlits)) =
   773 	    let val nlit = subst lit
   774 	    in  if nlit aconv lit then (changed, nlit::nlits)
   775 		                  else ((nlit,true)::changed, nlits)
   776             end
   777       val (changed, lits') = foldr subLit (lits, ([], []))
   778       val (changed', pairs') = foldr subFrame (pairs, (changed, []))
   779   in  if !trace then writeln ("Substituting " ^ traceTerm sign u ^
   780 			      " for " ^ traceTerm sign t ^ " in branch" )
   781       else ();
   782       {pairs = (changed',[])::pairs',	(*affected formulas, and others*)
   783        lits  = lits',			(*unaffected literals*)
   784        vars  = vars, 
   785        lim   = lim}
   786   end;
   787 
   788 
   789 exception NEWBRANCHES and CLOSEF;
   790 
   791 exception PROVE;
   792 
   793 (*Trying eq_contr_tac first INCREASES the effort, slowing reconstruction*)
   794 val contr_tac = ematch_tac [Data.notE] THEN' 
   795                 (eq_assume_tac ORELSE' assume_tac);
   796 
   797 val eContr_tac  = TRACE Data.notE contr_tac;
   798 val eAssume_tac = TRACE asm_rl   (eq_assume_tac ORELSE' assume_tac);
   799 
   800 (*Try to unify complementary literals and return the corresponding tactic. *) 
   801 fun tryClose (Const"*Goal*" $ G,  L) = 
   802 	if unify([],G,L) then Some eAssume_tac else None
   803   | tryClose (G,  Const"*Goal*" $ L) = 
   804 	if unify([],G,L) then Some eAssume_tac else None
   805   | tryClose (Const"Not" $ G,  L)    = 
   806 	if unify([],G,L) then Some eContr_tac else None
   807   | tryClose (G,  Const"Not" $ L)    = 
   808 	if unify([],G,L) then Some eContr_tac else None
   809   | tryClose _                       = None;
   810 
   811 
   812 (*Were there Skolem terms in the premise?  Must NOT chase Vars*)
   813 fun hasSkolem (Skolem _)     = true
   814   | hasSkolem (Abs (_,body)) = hasSkolem body 
   815   | hasSkolem (f$t)          =  hasSkolem f orelse hasSkolem t
   816   | hasSkolem _              = false;
   817 
   818 (*Attach the right "may duplicate" flag to new formulae: if they contain
   819   Skolem terms then allow duplication.*)
   820 fun joinMd md [] = []
   821   | joinMd md (G::Gs) = (G, hasSkolem G orelse md) :: joinMd md Gs;
   822 
   823 (*Convert a Goal to an ordinary Not.  Used also in dup_intr, where a goal like
   824   Ex(P) is duplicated as the assumption ~Ex(P). *)
   825 fun negOfGoal (Const"*Goal*" $ G) = negate G
   826   | negOfGoal G                   = G;
   827 
   828 fun negOfGoal2 (G,md) = (negOfGoal G, md);
   829 
   830 (*Converts all Goals to Nots in the safe parts of a branch.  They could
   831   have been moved there from the literals list after substitution (equalSubst).
   832   There can be at most one--this function could be made more efficient.*)
   833 fun negOfGoals pairs = map (fn (Gs,haz) => (map negOfGoal2 Gs, haz)) pairs;
   834 
   835 (*Tactic.  Convert *Goal* to negated assumption in FIRST position*)
   836 fun negOfGoal_tac i = TRACE Data.ccontr (rtac Data.ccontr) i THEN
   837                       rotate_tac ~1 i;
   838 
   839 
   840 (** Backtracking and Pruning **)
   841 
   842 (*clashVar vars (n,trail) determines whether any of the last n elements
   843   of "trail" occur in "vars" OR in their instantiations*)
   844 fun clashVar [] = (fn _ => false)
   845   | clashVar vars =
   846       let fun clash (0, _)     = false
   847 	    | clash (_, [])    = false
   848 	    | clash (n, v::vs) = exists (varOccur v) vars orelse clash(n-1,vs)
   849       in  clash  end;
   850 
   851 
   852 (*nbrs = # of branches just prior to closing this one.  Delete choice points
   853   for goals proved by the latest inference, provided NO variables in the
   854   next branch have been updated.*)
   855 fun prune (1, nxtVars, choices) = choices  (*DON'T prune at very end: allow 
   856 					     backtracking over bad proofs*)
   857   | prune (nbrs, nxtVars, choices) =
   858       let fun traceIt last =
   859 		let val ll = length last
   860 		    and lc = length choices
   861 		in if !trace andalso ll<lc then
   862 		    (writeln("Pruning " ^ Int.toString(lc-ll) ^ " levels"); 
   863 		     last)
   864 		   else last
   865 		end
   866 	  fun pruneAux (last, _, _, []) = last
   867 	    | pruneAux (last, ntrl, trl, (ntrl',nbrs',exn) :: choices) =
   868 		if nbrs' < nbrs 
   869 		then last  (*don't backtrack beyond first solution of goal*)
   870 		else if nbrs' > nbrs then pruneAux (last, ntrl, trl, choices)
   871 		else (* nbrs'=nbrs *)
   872 		     if clashVar nxtVars (ntrl-ntrl', trl) then last
   873 		     else (*no clashes: can go back at least this far!*)
   874 			  pruneAux(choices, ntrl', List.drop(trl, ntrl-ntrl'), 
   875 				   choices)
   876   in  traceIt (pruneAux (choices, !ntrail, !trail, choices))  end;
   877 
   878 fun nextVars ({pairs, lits, vars, lim} :: _) = map Var vars
   879   | nextVars []                              = [];
   880 
   881 fun backtrack (choices as (ntrl, nbrs, exn)::_) = 
   882       (if !trace then (writeln ("Backtracking; now there are " ^ 
   883 				Int.toString nbrs ^ " branches"))
   884                  else (); 
   885        raise exn)
   886   | backtrack _ = raise PROVE;
   887 
   888 (*Add the literal G, handling *Goal* and detecting duplicates.*)
   889 fun addLit (Const "*Goal*" $ G, lits) = 
   890       (*New literal is a *Goal*, so change all other Goals to Nots*)
   891       let fun bad (Const"*Goal*" $ _) = true
   892 	    | bad (Const"Not" $ G')   = G aconv G'
   893 	    | bad _                   = false;
   894 	  fun change [] = []
   895 	    | change (Const"*Goal*" $ G' :: lits) = 
   896 		  if G aconv G' then change lits
   897 		  else Const"Not" $ G' :: change lits
   898 	    | change (Const"Not" $ G' :: lits)    = 
   899 		  if G aconv G' then change lits
   900 		  else Const"Not" $ G' :: change lits
   901 	    | change (lit::lits) = lit :: change lits
   902       in
   903 	Const "*Goal*" $ G :: (if exists bad lits then change lits else lits)
   904       end
   905   | addLit (G,lits) = ins_term(G, lits)
   906 
   907 
   908 (*For calculating the "penalty" to assess on a branching factor of n
   909   log2 seems a little too severe*)
   910 fun log n = if n<4 then 0 else 1 + log(n div 4);
   911 
   912 
   913 (*match(t,u) says whether the term u might be an instance of the pattern t
   914   Used to detect "recursive" rules such as transitivity*)
   915 fun match (Var _) u   = true
   916   | match (Const"*Goal*") (Const"Not")    = true
   917   | match (Const"Not")    (Const"*Goal*") = true
   918   | match (Const a)       (Const b)       = (a=b)
   919   | match (TConst (a,ta)) (TConst (b,tb)) = a=b andalso match ta tb
   920   | match (Free a)        (Free b)        = (a=b)
   921   | match (Bound i)       (Bound j)       = (i=j)
   922   | match (Abs(_,t))      (Abs(_,u))      = match t u
   923   | match (f$t)           (g$u)           = match f g andalso match t u
   924   | match t               u   = false;
   925 
   926 
   927 (*Branches closed: number of branches closed during the search
   928   Branches tried:  number of branches created by splitting (counting from 1)*)
   929 val nclosed = ref 0
   930 and ntried  = ref 1;
   931 
   932 fun printStats (b, start, tacs) =
   933   if b then
   934     writeln (endTiming start ^ " for search.  Closed: " 
   935 	     ^ Int.toString (!nclosed) ^
   936              " tried: " ^ Int.toString (!ntried) ^
   937              " tactics: " ^ Int.toString (length tacs))
   938   else ();
   939 
   940 
   941 (*Tableau prover based on leanTaP.  Argument is a list of branches.  Each 
   942   branch contains a list of unexpanded formulae, a list of literals, and a 
   943   bound on unsafe expansions.
   944  "start" is CPU time at start, for printing search time
   945 *)
   946 fun prove (sign, start, cs, brs, cont) =
   947  let val {safe0_netpair, safep_netpair, haz_netpair, ...} = Data.rep_cs cs
   948      val safeList = [safe0_netpair, safep_netpair]
   949      and hazList  = [haz_netpair]
   950      fun prv (tacs, trs, choices, []) = 
   951 	        (printStats (!trace orelse !stats, start, tacs); 
   952 		 cont (tacs, trs, choices))   (*all branches closed!*)
   953        | prv (tacs, trs, choices, 
   954 	      brs0 as {pairs = ((G,md)::br, haz)::pairs, 
   955 		       lits, vars, lim} :: brs) =
   956    	     (*apply a safe rule only (possibly allowing instantiation);
   957                defer any haz formulae*)
   958 	  let exception PRV (*backtrack to precisely this recursion!*)
   959 	      val ntrl = !ntrail 
   960 	      val nbrs = length brs0
   961               val nxtVars = nextVars brs
   962 	      val G = norm G
   963 	      val rules = netMkRules G vars safeList
   964 	      (*Make a new branch, decrementing "lim" if instantiations occur*)
   965 	      fun newBr (vars',lim') prems =
   966 		  map (fn prem => 
   967 		       if (exists isGoal prem) 
   968 		       then {pairs = ((joinMd md prem, []) :: 
   969 				      negOfGoals ((br, haz)::pairs)),
   970 			     lits  = map negOfGoal lits, 
   971 			     vars  = vars', 
   972 			     lim   = lim'}
   973 		       else {pairs = ((joinMd md prem, []) :: 
   974 				      (br, haz) :: pairs),
   975 			     lits = lits, 
   976 			     vars = vars', 
   977 			     lim  = lim'})
   978 		  prems @
   979 		  brs		  
   980 	      (*Seek a matching rule.  If unifiable then add new premises
   981                 to branch.*)
   982 	      fun deeper [] = raise NEWBRANCHES
   983 		| deeper (((P,prems),tac)::grls) =
   984 		    if unify(add_term_vars(P,[]), P, G) 
   985 		    then  (*P comes from the rule; G comes from the branch.*)
   986 		     let val updated = ntrl < !ntrail (*branch updated*)
   987 			 val lim' = if updated
   988 				    then lim - (1+log(length rules))
   989 				    else lim   (*discourage branching updates*)
   990 			 val vars  = vars_in_vars vars
   991 			 val vars' = foldr add_terms_vars (prems, vars)
   992 			 val choices' = (ntrl, nbrs, PRV) :: choices
   993 			 val tacs' = (tac(updated,false,true)) 
   994                                      :: tacs  (*no duplication; rotate*)
   995 		     in
   996 			 traceNew prems;  traceVars sign ntrl;
   997 			 (if null prems then (*closed the branch: prune!*)
   998 			    (nclosed := !nclosed + 1;
   999 			     prv(tacs',  brs0::trs, 
  1000 				 prune (nbrs, nxtVars, choices'),
  1001 				 brs))
  1002 			  else (*prems non-null*)
  1003 			  if lim'<0 (*faster to kill ALL the alternatives*)
  1004 			  then (traceMsg"Excessive branching: KILLED";
  1005 			        clearTo ntrl;  raise NEWBRANCHES)
  1006 			  else
  1007 			    (ntried := !ntried + length prems - 1;
  1008 			     prv(tacs',  brs0::trs, choices',
  1009 				 newBr (vars',lim') prems)))
  1010                          handle PRV => 
  1011 			   if updated then
  1012 				(*Backtrack at this level.
  1013 				  Reset Vars and try another rule*)
  1014 				(clearTo ntrl;  deeper grls)
  1015 			   else (*backtrack to previous level*)
  1016 				backtrack choices
  1017 		     end
  1018 		    else deeper grls
  1019 	      (*Try to close branch by unifying with head goal*)
  1020 	      fun closeF [] = raise CLOSEF
  1021 		| closeF (L::Ls) = 
  1022 		    case tryClose(G,L) of
  1023 			None     => closeF Ls
  1024 		      | Some tac => 
  1025 			    let val choices' = 
  1026 				    (if !trace then (prs"branch closed";
  1027 						     traceVars sign ntrl)
  1028 				               else ();
  1029 				     prune (nbrs, nxtVars, 
  1030 					    (ntrl, nbrs, PRV) :: choices))
  1031 			    in  nclosed := !nclosed + 1;
  1032 				prv (tac::tacs, brs0::trs, choices', brs)  
  1033 				handle PRV => 
  1034 				    (*reset Vars and try another literal
  1035 				      [this handler is pruned if possible!]*)
  1036 				 (clearTo ntrl;  closeF Ls)
  1037 			    end
  1038 	      (*Try to unify a queued formula (safe or haz) with head goal*)
  1039 	      fun closeFl [] = raise CLOSEF
  1040 		| closeFl ((br, haz)::pairs) =
  1041 		    closeF (map fst br)
  1042 		      handle CLOSEF => closeF (map fst haz)
  1043 			handle CLOSEF => closeFl pairs
  1044 	  in tracing sign brs0; 
  1045 	     if lim<0 then (traceMsg "Limit reached.  "; backtrack choices)
  1046 	     else
  1047 	     prv (Data.hyp_subst_tac trace :: tacs, 
  1048 		  brs0::trs,  choices,
  1049 		  equalSubst sign
  1050 		    (G, {pairs = (br,haz)::pairs, 
  1051 			 lits  = lits, vars  = vars, lim   = lim}) 
  1052 		    :: brs)
  1053 	     handle DEST_EQ =>   closeF lits
  1054 	      handle CLOSEF =>   closeFl ((br,haz)::pairs)
  1055 	        handle CLOSEF => deeper rules
  1056 		  handle NEWBRANCHES => 
  1057 		   (case netMkRules G vars hazList of
  1058 		       [] => (*there are no plausible haz rules*)
  1059 			     (traceMsg "moving formula to literals";
  1060 			      prv (tacs, brs0::trs, choices,
  1061 				   {pairs = (br,haz)::pairs, 
  1062 				    lits  = addLit(G,lits), 
  1063 				    vars  = vars, 
  1064 				    lim   = lim}  :: brs))
  1065 		    | _ => (*G admits some haz rules: try later*)
  1066 			   (traceMsg "moving formula to haz list";
  1067 			    prv (if isGoal G then negOfGoal_tac :: tacs
  1068 				             else tacs, 
  1069 				 brs0::trs,  
  1070 				 choices,
  1071 				 {pairs = (br, haz@[(negOfGoal G, md)])::pairs,
  1072 				  lits  = lits,
  1073 				  vars  = vars, 
  1074 				  lim   = lim}  :: brs)))
  1075 	  end
  1076        | prv (tacs, trs, choices, 
  1077 	      {pairs = ([],haz)::(Gs,haz')::pairs, lits, vars, lim} :: brs) =
  1078 	     (*no more "safe" formulae: transfer haz down a level*)
  1079 	   prv (tacs, trs, choices, 
  1080 		{pairs = (Gs,haz@haz')::pairs, 
  1081 		 lits  = lits, 
  1082 		 vars  = vars, 
  1083 		 lim    = lim} :: brs)
  1084        | prv (tacs, trs, choices, 
  1085 	      brs0 as {pairs = [([], (H,md)::Hs)],
  1086 		       lits, vars, lim} :: brs) =
  1087    	     (*no safe steps possible at any level: apply a haz rule*)
  1088 	  let exception PRV (*backtrack to precisely this recursion!*)
  1089 	      val H = norm H
  1090 	      val ntrl = !ntrail
  1091 	      val rules = netMkRules H vars hazList
  1092 	      (*new premises of haz rules may NOT be duplicated*)
  1093 	      fun newPrem (vars,P,dup,lim') prem = 
  1094 		  let val Gs' = map (fn Q => (Q,false)) prem
  1095 		      and Hs' = if dup then Hs @ [(negOfGoal H, md)] else Hs
  1096 		      and lits' = if (exists isGoal prem) 
  1097 			          then map negOfGoal lits
  1098 				  else lits
  1099                   in  {pairs = if exists (match P) prem then [(Gs',Hs')] 
  1100 			       (*Recursive in this premise.  Don't make new
  1101 				 "stack frame".  New haz premises will end up
  1102 				 at the BACK of the queue, preventing
  1103 				 exclusion of others*)
  1104 			    else [(Gs',[]), ([],Hs')], 
  1105 		       lits = lits', 
  1106 		       vars = vars, 
  1107 		       lim  = lim'}
  1108 		  end
  1109 	      fun newBr x prems = map (newPrem x) prems  @  brs
  1110 	      (*Seek a matching rule.  If unifiable then add new premises
  1111                 to branch.*)
  1112 	      fun deeper [] = raise NEWBRANCHES
  1113 		| deeper (((P,prems),tac)::grls) =
  1114 		    if unify(add_term_vars(P,[]), P, H)
  1115 		    then
  1116 		     let val updated = ntrl < !ntrail (*branch updated*)
  1117 			 val vars  = vars_in_vars vars
  1118 			 val vars' = foldr add_terms_vars (prems, vars)
  1119 			    (*duplicate H if md permits*)
  1120 			 val dup = md (*earlier had "andalso vars' <> vars":
  1121                                   duplicate only if the subgoal has new vars*)
  1122 			     (*any instances of P in the subgoals?
  1123 			       NB: boolean "recur" affects tracing only!*)
  1124 			 and recur = exists (exists (match P)) prems
  1125 			 val lim' = (*Decrement "lim" extra if updates occur*)
  1126 			     if updated then lim - (1+log(length rules))
  1127 			     else lim-1 
  1128 				 (*It is tempting to leave "lim" UNCHANGED if
  1129 				   both dup and recur are false.  Proofs are
  1130 				   found at shallower depths, but looping
  1131 				   occurs too often...*)
  1132 			 val mayUndo = 
  1133 			     (*Allowing backtracking from a rule application
  1134 			       if other matching rules exist, if the rule
  1135 			       updated variables, or if the rule did not
  1136 			       introduce new variables.  This latter condition
  1137 			       means it is not a standard "gamma-rule" but
  1138 			       some other form of unsafe rule.  Aim is to
  1139 			       emulate Fast_tac, which allows all unsafe steps
  1140 			       to be undone.*)
  1141 			     not(null grls)   (*other rules to try?*)
  1142 			     orelse updated
  1143 			     orelse vars=vars'   (*no new Vars?*)
  1144 			 val tac' = tac(updated, dup, true)
  1145 		       (*if recur then perhaps shouldn't call rotate_tac: new
  1146                          formulae should be last, but that's WRONG if the new
  1147                          formulae are Goals, since they remain in the first
  1148                          position*)
  1149 
  1150 		     in
  1151 		       if lim'<0 andalso not (null prems)
  1152 		       then (*it's faster to kill ALL the alternatives*)
  1153 			   (traceMsg"Excessive branching: KILLED";
  1154 			    clearTo ntrl;  raise NEWBRANCHES)
  1155 		       else 
  1156 			 traceNew prems;  
  1157 			 if !trace andalso dup then prs" (duplicating)"
  1158 					         else ();
  1159 			 if !trace andalso recur then prs" (recursive)"
  1160 					         else ();
  1161 			 traceVars sign ntrl;
  1162 			 if null prems then nclosed := !nclosed + 1
  1163 			 else ntried := !ntried + length prems - 1;
  1164 			 prv(tac' :: tacs, 
  1165 			     brs0::trs, 
  1166 			     (ntrl, length brs0, PRV) :: choices, 
  1167 			     newBr (vars', P, dup, lim') prems)
  1168 			  handle PRV => 
  1169 			      if mayUndo
  1170 			      then (*reset Vars and try another rule*)
  1171 				   (clearTo ntrl;  deeper grls)
  1172 			      else (*backtrack to previous level*)
  1173 				   backtrack choices
  1174 		     end
  1175 		    else deeper grls
  1176 	  in tracing sign brs0; 
  1177 	     if lim<1 then (traceMsg "Limit reached.  "; backtrack choices)
  1178 	     else deeper rules
  1179 	     handle NEWBRANCHES => 
  1180 		 (*cannot close branch: move H to literals*)
  1181 		 prv (tacs,  brs0::trs,  choices,
  1182 		      {pairs = [([], Hs)], 
  1183 		       lits  = H::lits, 
  1184 		       vars  = vars, 
  1185 		       lim   = lim}  :: brs)
  1186 	  end
  1187        | prv (tacs, trs, choices, _ :: brs) = backtrack choices
  1188  in prv ([], [], [(!ntrail, length brs, PROVE)], brs) end;
  1189 
  1190 
  1191 (*Construct an initial branch.*)
  1192 fun initBranch (ts,lim) = 
  1193     {pairs = [(map (fn t => (t,true)) ts, [])],
  1194      lits  = [], 
  1195      vars  = add_terms_vars (ts,[]), 
  1196      lim   = lim};
  1197 
  1198 
  1199 (*** Conversion & Skolemization of the Isabelle proof state ***)
  1200 
  1201 (*Make a list of all the parameters in a subgoal, even if nested*)
  1202 local open Term 
  1203 in
  1204 fun discard_foralls (Const("all",_)$Abs(a,T,t)) = discard_foralls t
  1205   | discard_foralls t = t;
  1206 end;
  1207 
  1208 
  1209 (*List of variables not appearing as arguments to the given parameter*)
  1210 fun getVars []                  i = []
  1211   | getVars ((_,(v,is))::alist) i =
  1212 	if i mem is then getVars alist i
  1213 	else v :: getVars alist i;
  1214 
  1215 exception TRANS of string;
  1216 
  1217 (*Translation of a subgoal: Skolemize all parameters*)
  1218 fun fromSubgoal t =
  1219   let val alistVar = ref []
  1220       and alistTVar = ref []
  1221       fun hdvar ((ix,(v,is))::_) = v
  1222       fun from lev t =
  1223 	let val (ht,ts) = Term.strip_comb t
  1224 	    fun apply u = list_comb (u, map (from lev) ts)
  1225 	    fun bounds [] = []
  1226 	      | bounds (Term.Bound i::ts) = 
  1227 		  if i<lev then raise TRANS
  1228 		      "Function unknown's argument not a parameter"
  1229 		  else i-lev :: bounds ts
  1230 	      | bounds ts = raise TRANS
  1231 		      "Function unknown's argument not a bound variable"
  1232         in
  1233 	  case ht of 
  1234 	      Term.Const aT    => apply (fromConst alistTVar aT)
  1235 	    | Term.Free  (a,_) => apply (Free a)
  1236 	    | Term.Bound i     => apply (Bound i)
  1237 	    | Term.Var (ix,_) => 
  1238 		  (case (assoc_string_int(!alistVar,ix)) of
  1239 		       None => (alistVar := (ix, (ref None, bounds ts))
  1240 					  :: !alistVar;
  1241 				Var (hdvar(!alistVar)))
  1242 		     | Some(v,is) => if is=bounds ts then Var v
  1243 			    else raise TRANS
  1244 				("Discrepancy among occurrences of "
  1245 				 ^ Syntax.string_of_vname ix))
  1246 	    | Term.Abs (a,_,body) => 
  1247 		  if null ts then Abs(a, from (lev+1) body)
  1248 		  else raise TRANS "argument not in normal form"
  1249         end
  1250 
  1251       val npars = length (Logic.strip_params t)
  1252 
  1253       (*Skolemize a subgoal from a proof state*)
  1254       fun skoSubgoal i t =
  1255 	  if i<npars then 
  1256 	      skoSubgoal (i+1)
  1257 		(subst_bound (Skolem (gensym "T_", getVars (!alistVar) i), 
  1258 			      t))
  1259 	  else t
  1260 
  1261   in  skoSubgoal 0 (from 0 (discard_foralls t))  end;
  1262 
  1263 
  1264 fun initialize() = 
  1265     (fullTrace:=[];  trail := [];  ntrail := 0;
  1266      nclosed := 0;  ntried := 1);
  1267 
  1268 
  1269 (*Tactic using tableau engine and proof reconstruction.  
  1270  "start" is CPU time at start, for printing SEARCH time
  1271 	(also prints reconstruction time)
  1272  "lim" is depth limit.*)
  1273 fun timing_depth_tac start cs lim i st0 = 
  1274  (initialize();
  1275   let val st = ObjectLogic.atomize_goal i st0;
  1276       val {sign,...} = rep_thm st
  1277       val skoprem = fromSubgoal (List.nth(prems_of st, i-1))
  1278       val hyps  = strip_imp_prems skoprem
  1279       and concl = strip_imp_concl skoprem
  1280       fun cont (tacs,_,choices) = 
  1281 	  let val start = startTiming()
  1282 	  in
  1283 	  case Seq.pull(EVERY' (rev tacs) i st) of
  1284 	      None => (writeln ("PROOF FAILED for depth " ^
  1285 				Int.toString lim);
  1286 		       if !trace then writeln "************************\n"
  1287 		       else ();
  1288 		       backtrack choices)
  1289 	    | cell => (if (!trace orelse !stats)
  1290 		       then writeln (endTiming start ^ " for reconstruction")
  1291 		       else ();
  1292 		       Seq.make(fn()=> cell))
  1293           end
  1294   in prove (sign, start, cs, [initBranch (mkGoal concl :: hyps, lim)], cont) 
  1295   end
  1296   handle PROVE     => Seq.empty);
  1297 
  1298 (*Public version with fixed depth*)
  1299 fun depth_tac cs lim i st = timing_depth_tac (startTiming()) cs lim i st;
  1300 
  1301 fun blast_tac cs i st = 
  1302     ((DEEPEN (1,20) (timing_depth_tac (startTiming()) cs) 0) i 
  1303      THEN flexflex_tac) st
  1304     handle TRANS s => (warning ("Blast_tac: " ^ s); Seq.empty);
  1305 
  1306 fun Blast_tac i = blast_tac (Data.claset()) i;
  1307 
  1308 
  1309 (*** For debugging: these apply the prover to a subgoal and return 
  1310      the resulting tactics, trace, etc.                            ***)
  1311 
  1312 (*Translate subgoal i from a proof state*)
  1313 fun trygl cs lim i = 
  1314     (initialize();
  1315      let val st = topthm()
  1316          val {sign,...} = rep_thm st
  1317 	 val skoprem = fromSubgoal (List.nth(prems_of st, i-1))
  1318          val hyps  = strip_imp_prems skoprem
  1319          and concl = strip_imp_concl skoprem
  1320      in timeap prove (sign, startTiming(), cs, 
  1321 		      [initBranch (mkGoal concl :: hyps, lim)], I)
  1322      end
  1323      handle Subscript => error("There is no subgoal " ^ Int.toString i));
  1324 
  1325 fun Trygl lim i = trygl (Data.claset()) lim i;
  1326 
  1327 (*Read a string to make an initial, singleton branch*)
  1328 fun readGoal sign s = read_cterm sign (s,propT) |>
  1329                       term_of |> fromTerm |> rand |> mkGoal;
  1330 
  1331 fun tryInThy thy lim s = 
  1332     (initialize();
  1333      timeap prove (Theory.sign_of thy, 
  1334 		   startTiming(), 
  1335 		   Data.claset(), 
  1336 		   [initBranch ([readGoal (Theory.sign_of thy) s], lim)], 
  1337 		   I));
  1338 
  1339 
  1340 (** method setup **)
  1341 
  1342 fun blast_args m =
  1343   Method.bang_sectioned_args' 
  1344       Data.cla_modifiers (Scan.lift (Scan.option Args.nat)) m;
  1345 
  1346 fun blast_meth None = Data.cla_meth' blast_tac
  1347   | blast_meth (Some lim) = Data.cla_meth' (fn cs => depth_tac cs lim);
  1348 
  1349 val setup = [Method.add_methods [("blast", blast_args blast_meth, 
  1350 				  "tableau prover")]];
  1351 
  1352 
  1353 end;