src/Provers/blast.ML
author wenzelm
Thu Jul 27 11:44:29 2000 +0200 (2000-07-27 ago)
changeset 9449 2f814053a6cc
parent 9170 0bfe5354d5e7
child 9486 2df511ebb956
permissions -rw-r--r--
intro_elim_tac: bimatch_from;
     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 		 xtraIs: thm list, xtraEs: thm list,
    66 		 swrappers: (string * wrapper) list, 
    67 		 uwrappers: (string * wrapper) list,
    68 		 safe0_netpair: netpair, safep_netpair: netpair,
    69 		 haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: netpair}
    70   val cla_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
    71   val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
    72   end;
    73 
    74 
    75 signature BLAST =
    76   sig
    77   type claset 
    78   exception TRANS of string    (*reports translation errors*)
    79   datatype term = 
    80       Const of string
    81     | TConst of string * term
    82     | Skolem of string * term option ref list
    83     | Free  of string
    84     | Var   of term option ref
    85     | Bound of int
    86     | Abs   of string*term
    87     | $  of term*term;
    88   type branch
    89   val depth_tac 	: claset -> int -> int -> tactic
    90   val blast_tac 	: claset -> int -> tactic
    91   val Blast_tac 	: int -> tactic
    92   val overloaded 	: string * (Term.typ -> Term.typ) -> unit
    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 (*Convert a possibly overloaded Term.Const to a Blast.Const or Blast.TConst,
   196   converting its type to a Blast.term in the latter case.*)
   197 fun fromConst alist (a,T) =
   198   case assoc_string (!overloads, a) of
   199       None   => Const a		(*not overloaded*)
   200     | Some f => 
   201 	let val T' = f T
   202 		     handle Match => error
   203                 ("Blast_tac: unexpected type for overloaded constant " ^ a)
   204         in  TConst(a, fromType alist T')  end;
   205 
   206 end;
   207 
   208 
   209 (*Tests whether 2 terms are alpha-convertible; chases instantiations*)
   210 fun (Const a)      aconv (Const b)      = a=b
   211   | (TConst (a,ta)) aconv (TConst (b,tb)) = a=b andalso ta aconv tb
   212   | (Skolem (a,_)) aconv (Skolem (b,_)) = a=b  (*arglists must then be equal*)
   213   | (Free a)       aconv (Free b)       = a=b
   214   | (Var(ref(Some t))) aconv u          = t aconv u
   215   | t          aconv (Var(ref(Some u))) = t aconv u
   216   | (Var v)        aconv (Var w)        = v=w	(*both Vars are un-assigned*)
   217   | (Bound i)      aconv (Bound j)      = i=j
   218   | (Abs(_,t))     aconv (Abs(_,u))     = t aconv u
   219   | (f$t)          aconv (g$u)          = (f aconv g) andalso (t aconv u)
   220   | _ aconv _  =  false;
   221 
   222 
   223 fun mem_term (_, [])     = false
   224   | mem_term (t, t'::ts) = t aconv t' orelse mem_term(t,ts);
   225 
   226 fun ins_term(t,ts) = if mem_term(t,ts) then ts else t :: ts;
   227 
   228 fun mem_var (v: term option ref, []) = false
   229   | mem_var (v, v'::vs)              = v=v' orelse mem_var(v,vs);
   230 
   231 fun ins_var(v,vs) = if mem_var(v,vs) then vs else v :: vs;
   232 
   233 
   234 (** Vars **)
   235 
   236 (*Accumulates the Vars in the term, suppressing duplicates*)
   237 fun add_term_vars (Skolem(a,args),	vars) = add_vars_vars(args,vars)
   238   | add_term_vars (Var (v as ref None),	vars) = ins_var (v, vars)
   239   | add_term_vars (Var (ref (Some u)), vars)  = add_term_vars(u,vars)
   240   | add_term_vars (TConst (_,t),	vars) = add_term_vars(t,vars)
   241   | add_term_vars (Abs (_,body),	vars) = add_term_vars(body,vars)
   242   | add_term_vars (f$t,	vars) =  add_term_vars (f, add_term_vars(t, vars))
   243   | add_term_vars (_,	vars) = vars
   244 (*Term list version.  [The fold functionals are slow]*)
   245 and add_terms_vars ([],    vars) = vars
   246   | add_terms_vars (t::ts, vars) = add_terms_vars (ts, add_term_vars(t,vars))
   247 (*Var list version.*)
   248 and add_vars_vars ([],    vars) = vars
   249   | add_vars_vars (ref (Some u) :: vs, vars) = 
   250 	add_vars_vars (vs, add_term_vars(u,vars))
   251   | add_vars_vars (v::vs, vars) =   (*v must be a ref None*)
   252 	add_vars_vars (vs, ins_var (v, vars));
   253 
   254 
   255 (*Chase assignments in "vars"; return a list of unassigned variables*)
   256 fun vars_in_vars vars = add_vars_vars(vars,[]);
   257 
   258 
   259 
   260 (*increment a term's non-local bound variables
   261      inc is  increment for bound variables
   262      lev is  level at which a bound variable is considered 'loose'*)
   263 fun incr_bv (inc, lev, u as Bound i) = if i>=lev then Bound(i+inc) else u 
   264   | incr_bv (inc, lev, Abs(a,body)) = Abs(a, incr_bv(inc,lev+1,body))
   265   | incr_bv (inc, lev, f$t) = incr_bv(inc,lev,f) $ incr_bv(inc,lev,t)
   266   | incr_bv (inc, lev, u) = u;
   267 
   268 fun incr_boundvars  0  t = t
   269   | incr_boundvars inc t = incr_bv(inc,0,t);
   270 
   271 
   272 (*Accumulate all 'loose' bound vars referring to level 'lev' or beyond.
   273    (Bound 0) is loose at level 0 *)
   274 fun add_loose_bnos (Bound i, lev, js)   = if i<lev then js  
   275 					  else  (i-lev) ins_int js
   276   | add_loose_bnos (Abs (_,t), lev, js) = add_loose_bnos (t, lev+1, js)
   277   | add_loose_bnos (f$t, lev, js)       =
   278 	        add_loose_bnos (f, lev, add_loose_bnos (t, lev, js)) 
   279   | add_loose_bnos (_, _, js)           = js;
   280 
   281 fun loose_bnos t = add_loose_bnos (t, 0, []);
   282 
   283 fun subst_bound (arg, t) : term = 
   284   let fun subst (t as Bound i, lev) =
   285  	    if i<lev then  t    (*var is locally bound*)
   286 	    else  if i=lev then incr_boundvars lev arg
   287 		           else Bound(i-1)  (*loose: change it*)
   288 	| subst (Abs(a,body), lev) = Abs(a, subst(body,lev+1))
   289 	| subst (f$t, lev) =  subst(f,lev)  $  subst(t,lev)
   290 	| subst (t,lev)    = t
   291   in  subst (t,0)  end;
   292 
   293 
   294 (*Normalize...but not the bodies of ABSTRACTIONS*)
   295 fun norm t = case t of
   296     Skolem (a,args)      => Skolem(a, vars_in_vars args)
   297   | TConst(a,aT)         => TConst(a, norm aT)
   298   | (Var (ref None))     => t
   299   | (Var (ref (Some u))) => norm u
   300   | (f $ u) => (case norm f of
   301                     Abs(_,body) => norm (subst_bound (u, body))
   302                   | nf => nf $ norm u)
   303   | _ => t;
   304 
   305 
   306 (*Weak (one-level) normalize for use in unification*)
   307 fun wkNormAux t = case t of
   308     (Var v) => (case !v of
   309 		    Some u => wkNorm u
   310 		  | None   => t)
   311   | (f $ u) => (case wkNormAux f of
   312 		    Abs(_,body) => wkNorm (subst_bound (u, body))
   313 		  | nf          => nf $ u)
   314   | Abs (a,body) =>	(*eta-contract if possible*)
   315 	(case wkNormAux body of
   316 	     nb as (f $ t) => 
   317 		 if (0 mem_int loose_bnos f) orelse wkNorm t <> Bound 0
   318 		 then Abs(a,nb)
   319 		 else wkNorm (incr_boundvars ~1 f)
   320 	   | nb => Abs (a,nb))
   321   | _ => t
   322 and wkNorm t = case head_of t of
   323     Const _        => t
   324   | TConst _       => t
   325   | Skolem(a,args) => t
   326   | Free _         => t
   327   | _              => wkNormAux t;
   328 
   329 
   330 (*Does variable v occur in u?  For unification.  
   331   Dangling bound vars are also forbidden.*)
   332 fun varOccur v = 
   333   let fun occL lev [] = false	(*same as (exists occ), but faster*)
   334 	| occL lev (u::us) = occ lev u orelse occL lev us
   335       and occ lev (Var w) = 
   336 	      v=w orelse
   337               (case !w of None   => false
   338 	                | Some u => occ lev u)
   339         | occ lev (Skolem(_,args)) = occL lev (map Var args)
   340             (*ignore TConst, since term variables can't occur in types (?) *)
   341         | occ lev (Bound i)  = lev <= i
   342         | occ lev (Abs(_,u)) = occ (lev+1) u
   343         | occ lev (f$u)      = occ lev u  orelse  occ lev f
   344         | occ lev _          = false;
   345   in  occ 0  end;
   346 
   347 exception UNIFY;
   348 
   349 val trail = ref [] : term option ref list ref;
   350 val ntrail = ref 0;
   351 
   352 
   353 (*Restore the trail to some previous state: for backtracking*)
   354 fun clearTo n =
   355     while !ntrail<>n do
   356 	(hd(!trail) := None;
   357 	 trail := tl (!trail);
   358 	 ntrail := !ntrail - 1);
   359 
   360 
   361 (*First-order unification with bound variables.  
   362   "vars" is a list of variables local to the rule and NOT to be put
   363 	on the trail (no point in doing so)
   364 *)
   365 fun unify(vars,t,u) =
   366     let val n = !ntrail 
   367 	fun update (t as Var v, u) =
   368 	    if t aconv u then ()
   369 	    else if varOccur v u then raise UNIFY 
   370 	    else if mem_var(v, vars) then v := Some u
   371 		 else (*avoid updating Vars in the branch if possible!*)
   372 		      if is_Var u andalso mem_var(dest_Var u, vars)
   373 		      then dest_Var u := Some t
   374 		      else (v := Some u;
   375 			    trail := v :: !trail;  ntrail := !ntrail + 1)
   376 	fun unifyAux (t,u) = 
   377 	    case (wkNorm t,  wkNorm u) of
   378 		(nt as Var v,  nu) => update(nt,nu)
   379 	      | (nu,  nt as Var v) => update(nt,nu)
   380 	      | (TConst(a,at), TConst(b,bt)) => if a=b then unifyAux(at,bt)
   381 		                                else raise UNIFY
   382 	      | (Abs(_,t'),  Abs(_,u')) => unifyAux(t',u')
   383 		    (*NB: can yield unifiers having dangling Bound vars!*)
   384 	      | (f$t',  g$u') => (unifyAux(f,g); unifyAux(t',u'))
   385 	      | (nt,  nu)    => if nt aconv nu then () else raise UNIFY
   386     in  (unifyAux(t,u); true) handle UNIFY => (clearTo n; false)
   387     end;
   388 
   389 
   390 (*Convert from "real" terms to prototerms; eta-contract
   391   Code is duplicated with fromSubgoal.  Correct this?*)
   392 fun fromTerm t =
   393   let val alistVar = ref []
   394       and alistTVar = ref []
   395       fun from (Term.Const aT) = fromConst alistTVar aT
   396 	| from (Term.Free  (a,_)) = Free a
   397 	| from (Term.Bound i)     = Bound i
   398 	| from (Term.Var (ixn,T)) = 
   399 	      (case (assoc_string_int(!alistVar,ixn)) of
   400 		   None => let val t' = Var(ref None)
   401 		           in  alistVar := (ixn, t') :: !alistVar;  t'
   402 			   end
   403 		 | Some v => v)
   404 	| from (Term.Abs (a,_,u)) = 
   405 	      (case  from u  of
   406 		u' as (f $ Bound 0) => 
   407 		  if (0 mem_int loose_bnos f) then Abs(a,u')
   408 		  else incr_boundvars ~1 f 
   409 	      | u' => Abs(a,u'))
   410 	| from (Term.$ (f,u)) = from f $ from u
   411   in  from t  end;
   412 
   413 (*A debugging function: replaces all Vars by dummy Frees for visual inspection
   414   of whether they are distinct.  Function revert undoes the assignments.*)
   415 fun instVars t =
   416   let val name = ref "A"
   417       val updated = ref []
   418       fun inst (TConst(a,t)) = inst t
   419 	| inst (Var(v as ref None)) = (updated := v :: (!updated);
   420 				       v       := Some (Free ("?" ^ !name)); 
   421 				       name    := bump_string (!name))
   422 	| inst (Abs(a,t))    = inst t
   423 	| inst (f $ u)       = (inst f; inst u)
   424 	| inst _             = ()
   425       fun revert() = seq (fn v => v:=None) (!updated)
   426   in  inst t; revert  end;
   427 
   428 
   429 (* A1==>...An==>B  goes to  [A1,...,An], where B is not an implication *)
   430 fun strip_imp_prems (Const"==>" $ (Const"Trueprop" $ A) $ B) = 
   431            A :: strip_imp_prems B
   432   | strip_imp_prems (Const"==>" $ A $ B) = A :: strip_imp_prems B
   433   | strip_imp_prems _ = [];
   434 
   435 (* A1==>...An==>B  goes to B, where B is not an implication *)
   436 fun strip_imp_concl (Const"==>" $ A $ B) = strip_imp_concl B
   437   | strip_imp_concl (Const"Trueprop" $ A) = A
   438   | strip_imp_concl A = A : term;
   439 
   440 
   441 (*** Conversion of Elimination Rules to Tableau Operations ***)
   442 
   443 exception ElimBadConcl and ElimBadPrem;
   444 
   445 (*The conclusion becomes the goal/negated assumption *False*: delete it!
   446   If we don't find it then the premise is ill-formed and could cause 
   447   PROOF FAILED*)
   448 fun delete_concl [] = raise ElimBadPrem
   449   | delete_concl (Const "*Goal*" $ (Var (ref (Some (Const"*False*")))) :: Ps) =
   450 	Ps
   451   | delete_concl (Const "Not" $ (Var (ref (Some (Const"*False*")))) :: Ps) =
   452 	Ps
   453   | delete_concl (P::Ps) = P :: delete_concl Ps;
   454 
   455 fun skoPrem vars (Const "all" $ Abs (_, P)) =
   456         skoPrem vars (subst_bound (Skolem (gensym "S_", vars), P))
   457   | skoPrem vars P = P;
   458 
   459 fun convertPrem t = 
   460     delete_concl (mkGoal (strip_imp_concl t) :: strip_imp_prems t);
   461 
   462 (*Expects elimination rules to have a formula variable as conclusion*)
   463 fun convertRule vars t =
   464   let val (P::Ps) = strip_imp_prems t
   465       val Var v   = strip_imp_concl t
   466   in  v := Some (Const"*False*");
   467       (P, map (convertPrem o skoPrem vars) Ps) 
   468   end
   469   handle Bind => raise ElimBadConcl;
   470 
   471 
   472 (*Like dup_elim, but puts the duplicated major premise FIRST*)
   473 fun rev_dup_elim th = th RSN (2, revcut_rl) |> assumption 2 |> Seq.hd;
   474 
   475 
   476 (*Rotate the assumptions in all new subgoals for the LIFO discipline*)
   477 local
   478   (*Count new hyps so that they can be rotated*)
   479   fun nNewHyps []                         = 0
   480     | nNewHyps (Const "*Goal*" $ _ :: Ps) = nNewHyps Ps
   481     | nNewHyps (P::Ps)                    = 1 + nNewHyps Ps;
   482 
   483   fun rot_tac [] i st      = Seq.single st
   484     | rot_tac (0::ks) i st = rot_tac ks (i+1) st
   485     | rot_tac (k::ks) i st = rot_tac ks (i+1) (rotate_rule (~k) i st);
   486 in
   487 fun rot_subgoals_tac (rot, rl) =
   488      rot_tac (if rot then map nNewHyps rl else []) 
   489 end;
   490 
   491 
   492 fun TRACE rl tac st i = if !trace then (prth rl; tac st i) else tac st i;
   493 
   494 (*Resolution/matching tactics: if upd then the proof state may be updated.
   495   Matching makes the tactics more deterministic in the presence of Vars.*)
   496 fun emtac upd rl = TRACE rl (if upd then etac rl else ematch_tac [rl]);
   497 fun rmtac upd rl = TRACE rl (if upd then rtac rl else match_tac [rl]);
   498 
   499 (*Tableau rule from elimination rule.  
   500   Flag "upd" says that the inference updated the branch.
   501   Flag "dup" requests duplication of the affected formula.*)
   502 fun fromRule vars rl = 
   503   let val trl = rl |> rep_thm |> #prop |> fromTerm |> convertRule vars
   504       fun tac (upd, dup,rot) i = 
   505 	emtac upd (if dup then rev_dup_elim rl else rl) i
   506 	THEN
   507 	rot_subgoals_tac (rot, #2 trl) i
   508   in Option.SOME (trl, tac) end
   509   handle ElimBadPrem => (*reject: prems don't preserve conclusion*)
   510 	    (warning("Ignoring weak elimination rule\n" ^ string_of_thm rl);
   511 	     Option.NONE)
   512        | ElimBadConcl => (*ignore: conclusion is not just a variable*)
   513 	   (if !trace then (warning("Ignoring ill-formed elimination rule:\n" ^
   514        	               "conclusion should be a variable\n" ^ string_of_thm rl))
   515 	    else ();
   516 	    Option.NONE);
   517 
   518 
   519 (*** Conversion of Introduction Rules ***)
   520 
   521 fun convertIntrPrem t = mkGoal (strip_imp_concl t) :: strip_imp_prems t;
   522 
   523 fun convertIntrRule vars t =
   524   let val Ps = strip_imp_prems t
   525       val P  = strip_imp_concl t
   526   in  (mkGoal P, map (convertIntrPrem o skoPrem vars) Ps) 
   527   end;
   528 
   529 (*Tableau rule from introduction rule.  
   530   Flag "upd" says that the inference updated the branch.
   531   Flag "dup" requests duplication of the affected formula.
   532   Since haz rules are now delayed, "dup" is always FALSE for
   533   introduction rules.*)
   534 fun fromIntrRule vars rl = 
   535   let val trl = rl |> rep_thm |> #prop |> fromTerm |> convertIntrRule vars
   536       fun tac (upd,dup,rot) i = 
   537 	 rmtac upd (if dup then Data.dup_intr rl else rl) i
   538 	 THEN
   539 	 rot_subgoals_tac (rot, #2 trl) i
   540   in (trl, tac) end;
   541 
   542 
   543 val dummyVar = Term.Var (("etc",0), dummyT);
   544 
   545 (*Convert from prototerms to ordinary terms with dummy types
   546   Ignore abstractions; identify all Vars; STOP at given depth*)
   547 fun toTerm 0 _             = dummyVar
   548   | toTerm d (Const a)     = Term.Const (a,dummyT)
   549   | toTerm d (TConst(a,_)) = Term.Const (a,dummyT)  (*no need to convert type*)
   550   | toTerm d (Skolem(a,_)) = Term.Const (a,dummyT)
   551   | toTerm d (Free a)      = Term.Free  (a,dummyT)
   552   | toTerm d (Bound i)     = Term.Bound i
   553   | toTerm d (Var _)       = dummyVar
   554   | toTerm d (Abs(a,_))    = dummyVar
   555   | toTerm d (f $ u)       = Term.$ (toTerm d f, toTerm (d-1) u);
   556 
   557 
   558 fun netMkRules P vars (nps: netpair list) =
   559   case P of
   560       (Const "*Goal*" $ G) =>
   561 	let val pG = mk_tprop (toTerm 2 G)
   562 	    val intrs = List.concat 
   563 		             (map (fn (inet,_) => Net.unify_term inet pG) 
   564 			      nps)
   565 	in  map (fromIntrRule vars o #2) (orderlist intrs)  end
   566     | _ =>
   567 	let val pP = mk_tprop (toTerm 3 P)
   568 	    val elims = List.concat 
   569 		             (map (fn (_,enet) => Net.unify_term enet pP) 
   570 			      nps)
   571 	in  List.mapPartial (fromRule vars o #2) (orderlist elims)  end;
   572 
   573 (**
   574 end;
   575 **)
   576 
   577 
   578 (*Pending formulae carry md (may duplicate) flags*)
   579 type branch = 
   580     {pairs: ((term*bool) list *	(*safe formulae on this level*)
   581                (term*bool) list) list,  (*haz formulae  on this level*)
   582      lits:   term list,                 (*literals: irreducible formulae*)
   583      vars:   term option ref list,      (*variables occurring in branch*)
   584      lim:    int};                      (*resource limit*)
   585 
   586 val fullTrace = ref[] : branch list list ref;
   587 
   588 (*Normalize a branch--for tracing*)
   589 fun norm2 (G,md) = (norm G, md);
   590 
   591 fun normLev (Gs,Hs) = (map norm2 Gs, map norm2 Hs);
   592 
   593 fun normBr {pairs, lits, vars, lim} =
   594      {pairs = map normLev pairs, 
   595       lits  = map norm lits, 
   596       vars  = vars, 
   597       lim   = lim};
   598 
   599 
   600 val dummyTVar = Term.TVar(("a",0), []);
   601 val dummyVar2 = Term.Var(("var",0), dummyT);
   602 
   603 (*convert Blast_tac's type representation to real types for tracing*)
   604 fun showType (Free a)  = Term.TFree (a,[])
   605   | showType (Var _)   = dummyTVar
   606   | showType t         =
   607       (case strip_comb t of
   608 	   (Const a, us) => Term.Type(a, map showType us)
   609 	 | _ => dummyT);
   610 
   611 (*Display top-level overloading if any*)
   612 fun topType (TConst(a,t)) = Some (showType t)
   613   | topType (Abs(a,t))    = topType t
   614   | topType (f $ u)       = (case topType f of
   615 				 None => topType u
   616 			       | some => some)
   617   | topType _             = None;
   618 
   619 
   620 (*Convert from prototerms to ordinary terms with dummy types for tracing*)
   621 fun showTerm d (Const a)     = Term.Const (a,dummyT)
   622   | showTerm d (TConst(a,_)) = Term.Const (a,dummyT)
   623   | showTerm d (Skolem(a,_)) = Term.Const (a,dummyT)
   624   | showTerm d (Free a)      = Term.Free  (a,dummyT)
   625   | showTerm d (Bound i)     = Term.Bound i
   626   | showTerm d (Var(ref(Some u))) = showTerm d u
   627   | showTerm d (Var(ref None))    = dummyVar2
   628   | showTerm d (Abs(a,t))    = if d=0 then dummyVar
   629 			       else Term.Abs(a, dummyT, showTerm (d-1) t)
   630   | showTerm d (f $ u)       = if d=0 then dummyVar
   631 			       else Term.$ (showTerm d f, showTerm (d-1) u);
   632 
   633 fun string_of sign d t = Sign.string_of_term sign (showTerm d t);
   634 
   635 fun traceTerm sign t = 
   636   let val t' = norm t
   637       val stm = string_of sign 8 t'
   638   in  
   639       case topType t' of
   640 	  None   => stm   (*no type to attach*)
   641 	| Some T => stm ^ "\t:: " ^ Sign.string_of_typ sign T
   642   end;
   643 
   644 
   645 val prs = std_output;
   646 
   647 (*Print tracing information at each iteration of prover*)
   648 fun tracing sign brs = 
   649   let fun printPairs (((G,_)::_,_)::_)  = prs(traceTerm sign G)
   650 	| printPairs (([],(H,_)::_)::_) = prs(traceTerm sign H ^ "\t (Unsafe)")
   651 	| printPairs _                 = ()
   652       fun printBrs (brs0 as {pairs, lits, lim, ...} :: brs) =
   653 	    (fullTrace := brs0 :: !fullTrace;
   654 	     seq (fn _ => prs "+") brs;
   655 	     prs (" [" ^ Int.toString lim ^ "] ");
   656 	     printPairs pairs;
   657 	     writeln"")
   658   in if !trace then printBrs (map normBr brs) else ()
   659   end;
   660 
   661 fun traceMsg s = if !trace then writeln s else ();
   662 
   663 (*Tracing: variables updated in the last branch operation?*)
   664 fun traceVars sign ntrl =
   665   if !trace then 
   666       (case !ntrail-ntrl of
   667 	    0 => ()
   668 	  | 1 => prs"\t1 variable UPDATED:"
   669 	  | n => prs("\t" ^ Int.toString n ^ " variables UPDATED:");
   670        (*display the instantiations themselves, though no variable names*)
   671        seq (fn v => prs("   " ^ string_of sign 4 (the (!v))))
   672            (List.take(!trail, !ntrail-ntrl));
   673        writeln"")
   674     else ();
   675 
   676 (*Tracing: how many new branches are created?*)
   677 fun traceNew prems =
   678     if !trace then 
   679         case length prems of
   680 	    0 => prs"branch closed by rule"
   681 	  | 1 => prs"branch extended (1 new subgoal)"
   682 	  | n => prs("branch split: "^ Int.toString n ^ " new subgoals")
   683     else ();
   684 
   685 
   686 
   687 (*** Code for handling equality: naive substitution, like hyp_subst_tac ***)
   688 
   689 (*Replace the ATOMIC term "old" by "new" in t*)  
   690 fun subst_atomic (old,new) t =
   691     let fun subst (Var(ref(Some u))) = subst u
   692 	  | subst (Abs(a,body))      = Abs(a, subst body)
   693 	  | subst (f$t)              = subst f $ subst t
   694 	  | subst t                  = if t aconv old then new else t
   695     in  subst t  end;
   696 
   697 (*Eta-contract a term from outside: just enough to reduce it to an atom*)
   698 fun eta_contract_atom (t0 as Abs(a, body)) = 
   699       (case  eta_contract2 body  of
   700         f $ Bound 0 => if (0 mem_int loose_bnos f) then t0
   701 		       else eta_contract_atom (incr_boundvars ~1 f)
   702       | _ => t0)
   703   | eta_contract_atom t = t
   704 and eta_contract2 (f$t) = f $ eta_contract_atom t
   705   | eta_contract2 t     = eta_contract_atom t;
   706 
   707 
   708 (*When can we safely delete the equality?
   709     Not if it equates two constants; consider 0=1.
   710     Not if it resembles x=t[x], since substitution does not eliminate x.
   711     Not if it resembles ?x=0; another goal could instantiate ?x to Suc(i)
   712   Prefer to eliminate Bound variables if possible.
   713   Result:  true = use as is,  false = reorient first *)
   714 
   715 (*Can t occur in u?  For substitution.  
   716   Does NOT examine the args of Skolem terms: substitution does not affect them.
   717   REFLEXIVE because hyp_subst_tac fails on x=x.*)
   718 fun substOccur t = 
   719   let (*NO vars are permitted in u except the arguments of t, if it is 
   720         a Skolem term.  This ensures that no equations are deleted that could
   721         be instantiated to a cycle.  For example, x=?a is rejected because ?a
   722 	could be instantiated to Suc(x).*)
   723       val vars = case t of
   724                      Skolem(_,vars) => vars
   725 		   | _ => []
   726       fun occEq u = (t aconv u) orelse occ u
   727       and occ (Var(ref(Some u))) = occEq u
   728         | occ (Var v)            = not (mem_var (v, vars))
   729 	| occ (Abs(_,u))         = occEq u
   730         | occ (f$u)              = occEq u  orelse  occEq f
   731         | occ (_)                = false;
   732   in  occEq  end;
   733 
   734 exception DEST_EQ;
   735 
   736 (*Take apart an equality (plain or overloaded).  NO constant Trueprop*)
   737 fun dest_eq (Const  "op ="     $ t $ u) = 
   738 		(eta_contract_atom t, eta_contract_atom u)
   739   | dest_eq (TConst("op =",_)  $ t $ u) = 
   740 		(eta_contract_atom t, eta_contract_atom u)
   741   | dest_eq _                           = raise DEST_EQ;
   742 
   743 (*Reject the equality if u occurs in (or equals!) t*)
   744 fun check (t,u,v) = if substOccur t u then raise DEST_EQ else v;
   745 
   746 (*IF the goal is an equality with a substitutable variable 
   747   THEN orient that equality ELSE raise exception DEST_EQ*)
   748 fun orientGoal (t,u) = case (t,u) of
   749        (Skolem _, _) => check(t,u,(t,u))	(*eliminates t*)
   750      | (_, Skolem _) => check(u,t,(u,t))	(*eliminates u*)
   751      | (Free _, _)   => check(t,u,(t,u))	(*eliminates t*)
   752      | (_, Free _)   => check(u,t,(u,t))	(*eliminates u*)
   753      | _             => raise DEST_EQ;
   754 
   755 (*Substitute through the branch if an equality goal (else raise DEST_EQ).
   756   Moves affected literals back into the branch, but it is not clear where
   757   they should go: this could make proofs fail.*)
   758 fun equalSubst sign (G, {pairs, lits, vars, lim}) = 
   759   let val (t,u) = orientGoal(dest_eq G)
   760       val subst = subst_atomic (t,u)
   761       fun subst2(G,md) = (subst G, md)
   762       (*substitute throughout list; extract affected formulae*)
   763       fun subForm ((G,md), (changed, pairs)) =
   764 	    let val nG = subst G
   765 	    in  if nG aconv G then (changed, (G,md)::pairs)
   766 		              else ((nG,md)::changed, pairs)
   767             end
   768       (*substitute throughout "stack frame"; extract affected formulae*)
   769       fun subFrame ((Gs,Hs), (changed, frames)) =
   770 	    let val (changed', Gs') = foldr subForm (Gs, (changed, []))
   771                 val (changed'', Hs') = foldr subForm (Hs, (changed', []))
   772             in  (changed'', (Gs',Hs')::frames)  end
   773       (*substitute throughout literals; extract affected ones*)
   774       fun subLit (lit, (changed, nlits)) =
   775 	    let val nlit = subst lit
   776 	    in  if nlit aconv lit then (changed, nlit::nlits)
   777 		                  else ((nlit,true)::changed, nlits)
   778             end
   779       val (changed, lits') = foldr subLit (lits, ([], []))
   780       val (changed', pairs') = foldr subFrame (pairs, (changed, []))
   781   in  if !trace then writeln ("Substituting " ^ traceTerm sign u ^
   782 			      " for " ^ traceTerm sign t ^ " in branch" )
   783       else ();
   784       {pairs = (changed',[])::pairs',	(*affected formulas, and others*)
   785        lits  = lits',			(*unaffected literals*)
   786        vars  = vars, 
   787        lim   = lim}
   788   end;
   789 
   790 
   791 exception NEWBRANCHES and CLOSEF;
   792 
   793 exception PROVE;
   794 
   795 (*Trying eq_contr_tac first INCREASES the effort, slowing reconstruction*)
   796 val contr_tac = ematch_tac [Data.notE] THEN' 
   797                 (eq_assume_tac ORELSE' assume_tac);
   798 
   799 val eContr_tac  = TRACE Data.notE contr_tac;
   800 val eAssume_tac = TRACE asm_rl   (eq_assume_tac ORELSE' assume_tac);
   801 
   802 (*Try to unify complementary literals and return the corresponding tactic. *) 
   803 fun tryClose (Const"*Goal*" $ G,  L) = 
   804 	if unify([],G,L) then Some eAssume_tac else None
   805   | tryClose (G,  Const"*Goal*" $ L) = 
   806 	if unify([],G,L) then Some eAssume_tac else None
   807   | tryClose (Const"Not" $ G,  L)    = 
   808 	if unify([],G,L) then Some eContr_tac else None
   809   | tryClose (G,  Const"Not" $ L)    = 
   810 	if unify([],G,L) then Some eContr_tac else None
   811   | tryClose _                       = None;
   812 
   813 
   814 (*Were there Skolem terms in the premise?  Must NOT chase Vars*)
   815 fun hasSkolem (Skolem _)     = true
   816   | hasSkolem (Abs (_,body)) = hasSkolem body 
   817   | hasSkolem (f$t)          =  hasSkolem f orelse hasSkolem t
   818   | hasSkolem _              = false;
   819 
   820 (*Attach the right "may duplicate" flag to new formulae: if they contain
   821   Skolem terms then allow duplication.*)
   822 fun joinMd md [] = []
   823   | joinMd md (G::Gs) = (G, hasSkolem G orelse md) :: joinMd md Gs;
   824 
   825 (*Convert a Goal to an ordinary Not.  Used also in dup_intr, where a goal like
   826   Ex(P) is duplicated as the assumption ~Ex(P). *)
   827 fun negOfGoal (Const"*Goal*" $ G) = negate G
   828   | negOfGoal G                   = G;
   829 
   830 fun negOfGoal2 (G,md) = (negOfGoal G, md);
   831 
   832 (*Converts all Goals to Nots in the safe parts of a branch.  They could
   833   have been moved there from the literals list after substitution (equalSubst).
   834   There can be at most one--this function could be made more efficient.*)
   835 fun negOfGoals pairs = map (fn (Gs,haz) => (map negOfGoal2 Gs, haz)) pairs;
   836 
   837 (*Tactic.  Convert *Goal* to negated assumption in FIRST position*)
   838 fun negOfGoal_tac i = TRACE Data.ccontr (rtac Data.ccontr) i THEN
   839                       rotate_tac ~1 i;
   840 
   841 
   842 (** Backtracking and Pruning **)
   843 
   844 (*clashVar vars (n,trail) determines whether any of the last n elements
   845   of "trail" occur in "vars" OR in their instantiations*)
   846 fun clashVar [] = (fn _ => false)
   847   | clashVar vars =
   848       let fun clash (0, _)     = false
   849 	    | clash (_, [])    = false
   850 	    | clash (n, v::vs) = exists (varOccur v) vars orelse clash(n-1,vs)
   851       in  clash  end;
   852 
   853 
   854 (*nbrs = # of branches just prior to closing this one.  Delete choice points
   855   for goals proved by the latest inference, provided NO variables in the
   856   next branch have been updated.*)
   857 fun prune (1, nxtVars, choices) = choices  (*DON'T prune at very end: allow 
   858 					     backtracking over bad proofs*)
   859   | prune (nbrs, nxtVars, choices) =
   860       let fun traceIt last =
   861 		let val ll = length last
   862 		    and lc = length choices
   863 		in if !trace andalso ll<lc then
   864 		    (writeln("Pruning " ^ Int.toString(lc-ll) ^ " levels"); 
   865 		     last)
   866 		   else last
   867 		end
   868 	  fun pruneAux (last, _, _, []) = last
   869 	    | pruneAux (last, ntrl, trl, (ntrl',nbrs',exn) :: choices) =
   870 		if nbrs' < nbrs 
   871 		then last  (*don't backtrack beyond first solution of goal*)
   872 		else if nbrs' > nbrs then pruneAux (last, ntrl, trl, choices)
   873 		else (* nbrs'=nbrs *)
   874 		     if clashVar nxtVars (ntrl-ntrl', trl) then last
   875 		     else (*no clashes: can go back at least this far!*)
   876 			  pruneAux(choices, ntrl', List.drop(trl, ntrl-ntrl'), 
   877 				   choices)
   878   in  traceIt (pruneAux (choices, !ntrail, !trail, choices))  end;
   879 
   880 fun nextVars ({pairs, lits, vars, lim} :: _) = map Var vars
   881   | nextVars []                              = [];
   882 
   883 fun backtrack (choices as (ntrl, nbrs, exn)::_) = 
   884       (if !trace then (writeln ("Backtracking; now there are " ^ 
   885 				Int.toString nbrs ^ " branches"))
   886                  else (); 
   887        raise exn)
   888   | backtrack _ = raise PROVE;
   889 
   890 (*Add the literal G, handling *Goal* and detecting duplicates.*)
   891 fun addLit (Const "*Goal*" $ G, lits) = 
   892       (*New literal is a *Goal*, so change all other Goals to Nots*)
   893       let fun bad (Const"*Goal*" $ _) = true
   894 	    | bad (Const"Not" $ G')   = G aconv G'
   895 	    | bad _                   = false;
   896 	  fun change [] = []
   897 	    | change (Const"*Goal*" $ G' :: lits) = 
   898 		  if G aconv G' then change lits
   899 		  else Const"Not" $ G' :: change lits
   900 	    | change (Const"Not" $ G' :: lits)    = 
   901 		  if G aconv G' then change lits
   902 		  else Const"Not" $ G' :: change lits
   903 	    | change (lit::lits) = lit :: change lits
   904       in
   905 	Const "*Goal*" $ G :: (if exists bad lits then change lits else lits)
   906       end
   907   | addLit (G,lits) = ins_term(G, lits)
   908 
   909 
   910 (*For calculating the "penalty" to assess on a branching factor of n
   911   log2 seems a little too severe*)
   912 fun log n = if n<4 then 0 else 1 + log(n div 4);
   913 
   914 
   915 (*match(t,u) says whether the term u might be an instance of the pattern t
   916   Used to detect "recursive" rules such as transitivity*)
   917 fun match (Var _) u   = true
   918   | match (Const"*Goal*") (Const"Not")    = true
   919   | match (Const"Not")    (Const"*Goal*") = true
   920   | match (Const a)       (Const b)       = (a=b)
   921   | match (TConst (a,ta)) (TConst (b,tb)) = a=b andalso match ta tb
   922   | match (Free a)        (Free b)        = (a=b)
   923   | match (Bound i)       (Bound j)       = (i=j)
   924   | match (Abs(_,t))      (Abs(_,u))      = match t u
   925   | match (f$t)           (g$u)           = match f g andalso match t u
   926   | match t               u   = false;
   927 
   928 
   929 (*Branches closed: number of branches closed during the search
   930   Branches tried:  number of branches created by splitting (counting from 1)*)
   931 val nclosed = ref 0
   932 and ntried  = ref 1;
   933 
   934 fun printStats (b, start, tacs) =
   935   if b then
   936     writeln (endTiming start ^ " for search.  Closed: " 
   937 	     ^ Int.toString (!nclosed) ^
   938              " tried: " ^ Int.toString (!ntried) ^
   939              " tactics: " ^ Int.toString (length tacs))
   940   else ();
   941 
   942 
   943 (*Tableau prover based on leanTaP.  Argument is a list of branches.  Each 
   944   branch contains a list of unexpanded formulae, a list of literals, and a 
   945   bound on unsafe expansions.
   946  "start" is CPU time at start, for printing search time
   947 *)
   948 fun prove (sign, start, cs, brs, cont) =
   949  let val {safe0_netpair, safep_netpair, haz_netpair, ...} = Data.rep_cs cs
   950      val safeList = [safe0_netpair, safep_netpair]
   951      and hazList  = [haz_netpair]
   952      fun prv (tacs, trs, choices, []) = 
   953 	        (printStats (!trace orelse !stats, start, tacs); 
   954 		 cont (tacs, trs, choices))   (*all branches closed!*)
   955        | prv (tacs, trs, choices, 
   956 	      brs0 as {pairs = ((G,md)::br, haz)::pairs, 
   957 		       lits, vars, lim} :: brs) =
   958    	     (*apply a safe rule only (possibly allowing instantiation);
   959                defer any haz formulae*)
   960 	  let exception PRV (*backtrack to precisely this recursion!*)
   961 	      val ntrl = !ntrail 
   962 	      val nbrs = length brs0
   963               val nxtVars = nextVars brs
   964 	      val G = norm G
   965 	      val rules = netMkRules G vars safeList
   966 	      (*Make a new branch, decrementing "lim" if instantiations occur*)
   967 	      fun newBr (vars',lim') prems =
   968 		  map (fn prem => 
   969 		       if (exists isGoal prem) 
   970 		       then {pairs = ((joinMd md prem, []) :: 
   971 				      negOfGoals ((br, haz)::pairs)),
   972 			     lits  = map negOfGoal lits, 
   973 			     vars  = vars', 
   974 			     lim   = lim'}
   975 		       else {pairs = ((joinMd md prem, []) :: 
   976 				      (br, haz) :: pairs),
   977 			     lits = lits, 
   978 			     vars = vars', 
   979 			     lim  = lim'})
   980 		  prems @
   981 		  brs		  
   982 	      (*Seek a matching rule.  If unifiable then add new premises
   983                 to branch.*)
   984 	      fun deeper [] = raise NEWBRANCHES
   985 		| deeper (((P,prems),tac)::grls) =
   986 		    if unify(add_term_vars(P,[]), P, G) 
   987 		    then  (*P comes from the rule; G comes from the branch.*)
   988 		     let val updated = ntrl < !ntrail (*branch updated*)
   989 			 val lim' = if updated
   990 				    then lim - (1+log(length rules))
   991 				    else lim   (*discourage branching updates*)
   992 			 val vars  = vars_in_vars vars
   993 			 val vars' = foldr add_terms_vars (prems, vars)
   994 			 val choices' = (ntrl, nbrs, PRV) :: choices
   995 			 val tacs' = (tac(updated,false,true)) 
   996                                      :: tacs  (*no duplication; rotate*)
   997 		     in
   998 			 traceNew prems;  traceVars sign ntrl;
   999 			 (if null prems then (*closed the branch: prune!*)
  1000 			    (nclosed := !nclosed + 1;
  1001 			     prv(tacs',  brs0::trs, 
  1002 				 prune (nbrs, nxtVars, choices'),
  1003 				 brs))
  1004 			  else (*prems non-null*)
  1005 			  if lim'<0 (*faster to kill ALL the alternatives*)
  1006 			  then (traceMsg"Excessive branching: KILLED";
  1007 			        clearTo ntrl;  raise NEWBRANCHES)
  1008 			  else
  1009 			    (ntried := !ntried + length prems - 1;
  1010 			     prv(tacs',  brs0::trs, choices',
  1011 				 newBr (vars',lim') prems)))
  1012                          handle PRV => 
  1013 			   if updated then
  1014 				(*Backtrack at this level.
  1015 				  Reset Vars and try another rule*)
  1016 				(clearTo ntrl;  deeper grls)
  1017 			   else (*backtrack to previous level*)
  1018 				backtrack choices
  1019 		     end
  1020 		    else deeper grls
  1021 	      (*Try to close branch by unifying with head goal*)
  1022 	      fun closeF [] = raise CLOSEF
  1023 		| closeF (L::Ls) = 
  1024 		    case tryClose(G,L) of
  1025 			None     => closeF Ls
  1026 		      | Some tac => 
  1027 			    let val choices' = 
  1028 				    (if !trace then (prs"branch closed";
  1029 						     traceVars sign ntrl)
  1030 				               else ();
  1031 				     prune (nbrs, nxtVars, 
  1032 					    (ntrl, nbrs, PRV) :: choices))
  1033 			    in  nclosed := !nclosed + 1;
  1034 				prv (tac::tacs, brs0::trs, choices', brs)  
  1035 				handle PRV => 
  1036 				    (*reset Vars and try another literal
  1037 				      [this handler is pruned if possible!]*)
  1038 				 (clearTo ntrl;  closeF Ls)
  1039 			    end
  1040 	      fun closeFl [] = raise CLOSEF
  1041 		| closeFl ((br, haz)::pairs) =
  1042 		    closeF (map fst br)
  1043 		      handle CLOSEF => closeF (map fst haz)
  1044 			handle CLOSEF => closeFl pairs
  1045 	  in tracing sign brs0; 
  1046 	     if lim<0 then (traceMsg "Limit reached.  "; backtrack choices)
  1047 	     else
  1048 	     prv (Data.hyp_subst_tac trace :: tacs, 
  1049 		  brs0::trs,  choices,
  1050 		  equalSubst sign
  1051 		    (G, {pairs = (br,haz)::pairs, 
  1052 			 lits  = lits, vars  = vars, lim   = lim}) 
  1053 		    :: brs)
  1054 	     handle DEST_EQ =>   closeF lits
  1055 	      handle CLOSEF =>   closeFl ((br,haz)::pairs)
  1056 	        handle CLOSEF => deeper rules
  1057 		  handle NEWBRANCHES => 
  1058 		   (case netMkRules G vars hazList of
  1059 		       [] => (*there are no plausible haz rules*)
  1060 			     (traceMsg "moving formula to literals";
  1061 			      prv (tacs, brs0::trs, choices,
  1062 				   {pairs = (br,haz)::pairs, 
  1063 				    lits  = addLit(G,lits), 
  1064 				    vars  = vars, 
  1065 				    lim   = lim}  :: brs))
  1066 		    | _ => (*G admits some haz rules: try later*)
  1067 			   (traceMsg "moving formula to haz list";
  1068 			    prv (if isGoal G then negOfGoal_tac :: tacs
  1069 				             else tacs, 
  1070 				 brs0::trs,  
  1071 				 choices,
  1072 				 {pairs = (br, haz@[(negOfGoal G, md)])::pairs,
  1073 				  lits  = lits,
  1074 				  vars  = vars, 
  1075 				  lim   = lim}  :: brs)))
  1076 	  end
  1077        | prv (tacs, trs, choices, 
  1078 	      {pairs = ([],haz)::(Gs,haz')::pairs, lits, vars, lim} :: brs) =
  1079 	     (*no more "safe" formulae: transfer haz down a level*)
  1080 	   prv (tacs, trs, choices, 
  1081 		{pairs = (Gs,haz@haz')::pairs, 
  1082 		 lits  = lits, 
  1083 		 vars  = vars, 
  1084 		 lim    = lim} :: brs)
  1085        | prv (tacs, trs, choices, 
  1086 	      brs0 as {pairs = [([], (H,md)::Hs)],
  1087 		       lits, vars, lim} :: brs) =
  1088    	     (*no safe steps possible at any level: apply a haz rule*)
  1089 	  let exception PRV (*backtrack to precisely this recursion!*)
  1090 	      val H = norm H
  1091 	      val ntrl = !ntrail
  1092 	      val rules = netMkRules H vars hazList
  1093 	      (*new premises of haz rules may NOT be duplicated*)
  1094 	      fun newPrem (vars,P,dup,lim') prem = 
  1095 		  let val Gs' = map (fn Q => (Q,false)) prem
  1096 		      and Hs' = if dup then Hs @ [(negOfGoal H, md)] else Hs
  1097 		      and lits' = if (exists isGoal prem) 
  1098 			          then map negOfGoal lits
  1099 				  else lits
  1100                   in  {pairs = if exists (match P) prem then [(Gs',Hs')] 
  1101 			       (*Recursive in this premise.  Don't make new
  1102 				 "stack frame".  New haz premises will end up
  1103 				 at the BACK of the queue, preventing
  1104 				 exclusion of others*)
  1105 			    else [(Gs',[]), ([],Hs')], 
  1106 		       lits = lits', 
  1107 		       vars = vars, 
  1108 		       lim  = lim'}
  1109 		  end
  1110 	      fun newBr x prems = map (newPrem x) prems  @  brs
  1111 	      (*Seek a matching rule.  If unifiable then add new premises
  1112                 to branch.*)
  1113 	      fun deeper [] = raise NEWBRANCHES
  1114 		| deeper (((P,prems),tac)::grls) =
  1115 		    if unify(add_term_vars(P,[]), P, H)
  1116 		    then
  1117 		     let val updated = ntrl < !ntrail (*branch updated*)
  1118 			 val vars  = vars_in_vars vars
  1119 			 val vars' = foldr add_terms_vars (prems, vars)
  1120 			    (*duplicate H if md and the subgoal has new vars*)
  1121 			 val dup = md andalso vars' <> vars
  1122 			     (*any instances of P in the subgoals?
  1123 			       NB: this boolean 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 recur then prs" (recursive)"
  1158 					         else ();
  1159 			 traceVars sign ntrl;
  1160 			 if null prems then nclosed := !nclosed + 1
  1161 			 else ntried := !ntried + length prems - 1;
  1162 			 prv(tac' :: tacs, 
  1163 			     brs0::trs, 
  1164 			     (ntrl, length brs0, PRV) :: choices, 
  1165 			     newBr (vars', P, dup, lim') prems)
  1166 			  handle PRV => 
  1167 			      if mayUndo
  1168 			      then (*reset Vars and try another rule*)
  1169 				   (clearTo ntrl;  deeper grls)
  1170 			      else (*backtrack to previous level*)
  1171 				   backtrack choices
  1172 		     end
  1173 		    else deeper grls
  1174 	  in tracing sign brs0; 
  1175 	     if lim<1 then (traceMsg "Limit reached.  "; backtrack choices)
  1176 	     else deeper rules
  1177 	     handle NEWBRANCHES => 
  1178 		 (*cannot close branch: move H to literals*)
  1179 		 prv (tacs,  brs0::trs,  choices,
  1180 		      {pairs = [([], Hs)], 
  1181 		       lits  = H::lits, 
  1182 		       vars  = vars, 
  1183 		       lim   = lim}  :: brs)
  1184 	  end
  1185        | prv (tacs, trs, choices, _ :: brs) = backtrack choices
  1186  in init_gensym();
  1187     prv ([], [], [(!ntrail, length brs, PROVE)], brs) 
  1188  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 st = 
  1274  (initialize();
  1275   let val {sign,...} = rep_thm st
  1276       val skoprem = fromSubgoal (List.nth(prems_of st, i-1))
  1277       val hyps  = strip_imp_prems skoprem
  1278       and concl = strip_imp_concl skoprem
  1279       fun cont (tacs,_,choices) = 
  1280 	  let val start = startTiming()
  1281 	  in
  1282 	  case Seq.pull(EVERY' (rev tacs) i st) of
  1283 	      None => (writeln ("PROOF FAILED for depth " ^
  1284 				Int.toString lim);
  1285 		       if !trace then writeln "************************\n"
  1286 		       else ();
  1287 		       backtrack choices)
  1288 	    | cell => (if (!trace orelse !stats)
  1289 		       then writeln (endTiming start ^ " for reconstruction")
  1290 		       else ();
  1291 		       Seq.make(fn()=> cell))
  1292           end
  1293   in prove (sign, start, cs, [initBranch (mkGoal concl :: hyps, lim)], cont) 
  1294   end
  1295   handle PROVE     => Seq.empty);
  1296 
  1297 (*Public version with fixed depth*)
  1298 fun depth_tac cs lim i st = timing_depth_tac (startTiming()) cs lim i st;
  1299 
  1300 fun blast_tac cs i st = 
  1301     ((DEEPEN (1,20) (timing_depth_tac (startTiming()) cs) 0) i 
  1302      THEN flexflex_tac) st
  1303     handle TRANS s => (warning ("Blast_tac: " ^ s); Seq.empty);
  1304 
  1305 fun Blast_tac i = blast_tac (Data.claset()) i;
  1306 
  1307 
  1308 (*** For debugging: these apply the prover to a subgoal and return 
  1309      the resulting tactics, trace, etc.                            ***)
  1310 
  1311 (*Translate subgoal i from a proof state*)
  1312 fun trygl cs lim i = 
  1313     (initialize();
  1314      let val st = topthm()
  1315          val {sign,...} = rep_thm st
  1316 	 val skoprem = fromSubgoal (List.nth(prems_of st, i-1))
  1317          val hyps  = strip_imp_prems skoprem
  1318          and concl = strip_imp_concl skoprem
  1319      in timeap prove (sign, startTiming(), cs, 
  1320 		      [initBranch (mkGoal concl :: hyps, lim)], I)
  1321      end
  1322      handle Subscript => error("There is no subgoal " ^ Int.toString i));
  1323 
  1324 fun Trygl lim i = trygl (Data.claset()) lim i;
  1325 
  1326 (*Read a string to make an initial, singleton branch*)
  1327 fun readGoal sign s = read_cterm sign (s,propT) |>
  1328                       term_of |> fromTerm |> rand |> mkGoal;
  1329 
  1330 fun tryInThy thy lim s = 
  1331     (initialize();
  1332      timeap prove (Theory.sign_of thy, 
  1333 		   startTiming(), 
  1334 		   Data.claset(), 
  1335 		   [initBranch ([readGoal (Theory.sign_of thy) s], lim)], 
  1336 		   I));
  1337 
  1338 
  1339 (** method setup **)
  1340 
  1341 fun blast_args m =
  1342   Method.sectioned_args (Args.bang_facts -- Scan.lift (Scan.option Args.nat)) Data.cla_modifiers m;
  1343 
  1344 fun blast_meth (prems, None) = Data.cla_meth' blast_tac prems
  1345   | blast_meth (prems, Some lim) = Data.cla_meth' (fn cs => depth_tac cs lim) prems;
  1346 
  1347 val setup = [Method.add_methods [("blast", blast_args blast_meth, "tableau prover")]];
  1348 
  1349 
  1350 end;