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