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