src/Provers/blast.ML
author wenzelm
Wed Apr 04 23:29:33 2007 +0200 (2007-04-04)
changeset 22596 d0d2af4db18f
parent 22580 d91b4dd651d6
child 22678 23963361278c
permissions -rw-r--r--
rep_thm/cterm/ctyp: removed obsolete sign field;
     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 insert (op =) (i - lev) 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 member (op =) (loose_bnos f) 0 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 member (op =) (loose_bnos f) 0 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 |> Thm.prop_of |> 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 |> Thm.prop_of |> 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 = maps (fn (inet,_) => Net.unify_term inet pG) nps
   542         in  map (fromIntrRule vars o #2) (Tactic.orderlist intrs)  end
   543     | _ =>
   544         let val pP = mk_Trueprop (toTerm 3 P)
   545             val elims = maps (fn (_,enet) => Net.unify_term enet pP) nps
   546         in  map_filter (fromRule vars o #2) (Tactic.orderlist elims)  end;
   547 
   548 
   549 (*Pending formulae carry md (may duplicate) flags*)
   550 type branch =
   551     {pairs: ((term*bool) list * (*safe formulae on this level*)
   552                (term*bool) list) list,  (*haz formulae  on this level*)
   553      lits:   term list,                 (*literals: irreducible formulae*)
   554      vars:   term option ref list,      (*variables occurring in branch*)
   555      lim:    int};                      (*resource limit*)
   556 
   557 val fullTrace = ref[] : branch list list ref;
   558 
   559 (*Normalize a branch--for tracing*)
   560 fun norm2 (G,md) = (norm G, md);
   561 
   562 fun normLev (Gs,Hs) = (map norm2 Gs, map norm2 Hs);
   563 
   564 fun normBr {pairs, lits, vars, lim} =
   565      {pairs = map normLev pairs,
   566       lits  = map norm lits,
   567       vars  = vars,
   568       lim   = lim};
   569 
   570 
   571 val dummyTVar = Term.TVar(("a",0), []);
   572 val dummyVar2 = Term.Var(("var",0), dummyT);
   573 
   574 (*convert Blast_tac's type representation to real types for tracing*)
   575 fun showType (Free a)  = Term.TFree (a,[])
   576   | showType (Var _)   = dummyTVar
   577   | showType t         =
   578       (case strip_comb t of
   579            (Const (a, _), us) => Term.Type(a, map showType us)
   580          | _ => dummyT);
   581 
   582 (*Display top-level overloading if any*)
   583 fun topType thy (Const (c, ts)) = SOME (Sign.const_instance thy (c, map showType ts))
   584   | topType thy (Abs(a,t)) = topType thy t
   585   | topType thy (f $ u) = (case topType thy f of NONE => topType thy u | some => some)
   586   | topType _ _ = NONE;
   587 
   588 
   589 (*Convert from prototerms to ordinary terms with dummy types for tracing*)
   590 fun showTerm d (Const (a,_)) = Term.Const (a,dummyT)
   591   | showTerm d (Skolem(a,_)) = Term.Const (a,dummyT)
   592   | showTerm d (Free a)      = Term.Free  (a,dummyT)
   593   | showTerm d (Bound i)     = Term.Bound i
   594   | showTerm d (Var(ref(SOME u))) = showTerm d u
   595   | showTerm d (Var(ref NONE))    = dummyVar2
   596   | showTerm d (Abs(a,t))    = if d=0 then dummyVar
   597                                else Term.Abs(a, dummyT, showTerm (d-1) t)
   598   | showTerm d (f $ u)       = if d=0 then dummyVar
   599                                else Term.$ (showTerm d f, showTerm (d-1) u);
   600 
   601 fun string_of sign d t = Sign.string_of_term sign (showTerm d t);
   602 
   603 (*Convert a Goal to an ordinary Not.  Used also in dup_intr, where a goal like
   604   Ex(P) is duplicated as the assumption ~Ex(P). *)
   605 fun negOfGoal (Const ("*Goal*", _) $ G) = negate G
   606   | negOfGoal G = G;
   607 
   608 fun negOfGoal2 (G,md) = (negOfGoal G, md);
   609 
   610 (*Converts all Goals to Nots in the safe parts of a branch.  They could
   611   have been moved there from the literals list after substitution (equalSubst).
   612   There can be at most one--this function could be made more efficient.*)
   613 fun negOfGoals pairs = map (fn (Gs,haz) => (map negOfGoal2 Gs, haz)) pairs;
   614 
   615 (*Tactic.  Convert *Goal* to negated assumption in FIRST position*)
   616 fun negOfGoal_tac i = TRACE Data.ccontr (rtac Data.ccontr) i THEN
   617                       rotate_tac ~1 i;
   618 
   619 fun traceTerm sign t =
   620   let val t' = norm (negOfGoal t)
   621       val stm = string_of sign 8 t'
   622   in
   623       case topType sign t' of
   624           NONE   => stm   (*no type to attach*)
   625         | SOME T => stm ^ "\t:: " ^ Sign.string_of_typ sign T
   626   end;
   627 
   628 
   629 (*Print tracing information at each iteration of prover*)
   630 fun tracing sign brs =
   631   let fun printPairs (((G,_)::_,_)::_)  = Output.immediate_output(traceTerm sign G)
   632         | printPairs (([],(H,_)::_)::_) = Output.immediate_output(traceTerm sign H ^ "\t (Unsafe)")
   633         | printPairs _                 = ()
   634       fun printBrs (brs0 as {pairs, lits, lim, ...} :: brs) =
   635             (fullTrace := brs0 :: !fullTrace;
   636              List.app (fn _ => Output.immediate_output "+") brs;
   637              Output.immediate_output (" [" ^ Int.toString lim ^ "] ");
   638              printPairs pairs;
   639              writeln"")
   640   in if !trace then printBrs (map normBr brs) else ()
   641   end;
   642 
   643 fun traceMsg s = if !trace then writeln s else ();
   644 
   645 (*Tracing: variables updated in the last branch operation?*)
   646 fun traceVars sign ntrl =
   647   if !trace then
   648       (case !ntrail-ntrl of
   649             0 => ()
   650           | 1 => Output.immediate_output"\t1 variable UPDATED:"
   651           | n => Output.immediate_output("\t" ^ Int.toString n ^ " variables UPDATED:");
   652        (*display the instantiations themselves, though no variable names*)
   653        List.app (fn v => Output.immediate_output("   " ^ string_of sign 4 (the (!v))))
   654            (List.take(!trail, !ntrail-ntrl));
   655        writeln"")
   656     else ();
   657 
   658 (*Tracing: how many new branches are created?*)
   659 fun traceNew prems =
   660     if !trace then
   661         case length prems of
   662             0 => Output.immediate_output"branch closed by rule"
   663           | 1 => Output.immediate_output"branch extended (1 new subgoal)"
   664           | n => Output.immediate_output("branch split: "^ Int.toString n ^ " new subgoals")
   665     else ();
   666 
   667 
   668 
   669 (*** Code for handling equality: naive substitution, like hyp_subst_tac ***)
   670 
   671 (*Replace the ATOMIC term "old" by "new" in t*)
   672 fun subst_atomic (old,new) t =
   673     let fun subst (Var(ref(SOME u))) = subst u
   674           | subst (Abs(a,body))      = Abs(a, subst body)
   675           | subst (f$t)              = subst f $ subst t
   676           | subst t                  = if t aconv old then new else t
   677     in  subst t  end;
   678 
   679 (*Eta-contract a term from outside: just enough to reduce it to an atom*)
   680 fun eta_contract_atom (t0 as Abs(a, body)) =
   681       (case  eta_contract2 body  of
   682         f $ Bound 0 => if member (op =) (loose_bnos f) 0 then t0
   683                        else eta_contract_atom (incr_boundvars ~1 f)
   684       | _ => t0)
   685   | eta_contract_atom t = t
   686 and eta_contract2 (f$t) = f $ eta_contract_atom t
   687   | eta_contract2 t     = eta_contract_atom t;
   688 
   689 
   690 (*When can we safely delete the equality?
   691     Not if it equates two constants; consider 0=1.
   692     Not if it resembles x=t[x], since substitution does not eliminate x.
   693     Not if it resembles ?x=0; another goal could instantiate ?x to Suc(i)
   694   Prefer to eliminate Bound variables if possible.
   695   Result:  true = use as is,  false = reorient first *)
   696 
   697 (*Can t occur in u?  For substitution.
   698   Does NOT examine the args of Skolem terms: substitution does not affect them.
   699   REFLEXIVE because hyp_subst_tac fails on x=x.*)
   700 fun substOccur t =
   701   let (*NO vars are permitted in u except the arguments of t, if it is
   702         a Skolem term.  This ensures that no equations are deleted that could
   703         be instantiated to a cycle.  For example, x=?a is rejected because ?a
   704         could be instantiated to Suc(x).*)
   705       val vars = case t of
   706                      Skolem(_,vars) => vars
   707                    | _ => []
   708       fun occEq u = (t aconv u) orelse occ u
   709       and occ (Var(ref(SOME u))) = occEq u
   710         | occ (Var v)            = not (mem_var (v, vars))
   711         | occ (Abs(_,u))         = occEq u
   712         | occ (f$u)              = occEq u  orelse  occEq f
   713         | occ (_)                = false;
   714   in  occEq  end;
   715 
   716 exception DEST_EQ;
   717 
   718 (*Take apart an equality.  NO constant Trueprop*)
   719 fun dest_eq (Const (c, _) $ t $ u) =
   720       if c = Data.equality_name then (eta_contract_atom t, eta_contract_atom u)
   721       else raise DEST_EQ
   722   | dest_eq _ = raise DEST_EQ;
   723 
   724 (*Reject the equality if u occurs in (or equals!) t*)
   725 fun check (t,u,v) = if substOccur t u then raise DEST_EQ else v;
   726 
   727 (*IF the goal is an equality with a substitutable variable
   728   THEN orient that equality ELSE raise exception DEST_EQ*)
   729 fun orientGoal (t,u) = case (t,u) of
   730        (Skolem _, _) => check(t,u,(t,u))        (*eliminates t*)
   731      | (_, Skolem _) => check(u,t,(u,t))        (*eliminates u*)
   732      | (Free _, _)   => check(t,u,(t,u))        (*eliminates t*)
   733      | (_, Free _)   => check(u,t,(u,t))        (*eliminates u*)
   734      | _             => raise DEST_EQ;
   735 
   736 (*Substitute through the branch if an equality goal (else raise DEST_EQ).
   737   Moves affected literals back into the branch, but it is not clear where
   738   they should go: this could make proofs fail.*)
   739 fun equalSubst sign (G, {pairs, lits, vars, lim}) =
   740   let val (t,u) = orientGoal(dest_eq G)
   741       val subst = subst_atomic (t,u)
   742       fun subst2(G,md) = (subst G, md)
   743       (*substitute throughout list; extract affected formulae*)
   744       fun subForm ((G,md), (changed, pairs)) =
   745             let val nG = subst G
   746             in  if nG aconv G then (changed, (G,md)::pairs)
   747                               else ((nG,md)::changed, pairs)
   748             end
   749       (*substitute throughout "stack frame"; extract affected formulae*)
   750       fun subFrame ((Gs,Hs), (changed, frames)) =
   751             let val (changed', Gs') = foldr subForm (changed, []) Gs
   752                 val (changed'', Hs') = foldr subForm (changed', []) Hs
   753             in  (changed'', (Gs',Hs')::frames)  end
   754       (*substitute throughout literals; extract affected ones*)
   755       fun subLit (lit, (changed, nlits)) =
   756             let val nlit = subst lit
   757             in  if nlit aconv lit then (changed, nlit::nlits)
   758                                   else ((nlit,true)::changed, nlits)
   759             end
   760       val (changed, lits') = foldr subLit ([], []) lits
   761       val (changed', pairs') = foldr subFrame (changed, []) pairs
   762   in  if !trace then writeln ("Substituting " ^ traceTerm sign u ^
   763                               " for " ^ traceTerm sign t ^ " in branch" )
   764       else ();
   765       {pairs = (changed',[])::pairs',   (*affected formulas, and others*)
   766        lits  = lits',                   (*unaffected literals*)
   767        vars  = vars,
   768        lim   = lim}
   769   end;
   770 
   771 
   772 exception NEWBRANCHES and CLOSEF;
   773 
   774 exception PROVE;
   775 
   776 (*Trying eq_contr_tac first INCREASES the effort, slowing reconstruction*)
   777 val contr_tac = ematch_tac [Data.notE] THEN'
   778                 (eq_assume_tac ORELSE' assume_tac);
   779 
   780 val eContr_tac  = TRACE Data.notE contr_tac;
   781 val eAssume_tac = TRACE asm_rl   (eq_assume_tac ORELSE' assume_tac);
   782 
   783 (*Try to unify complementary literals and return the corresponding tactic. *)
   784 fun tryClose (G, L) =
   785   let
   786     fun close t u tac = if unify ([], t, u) then SOME tac else NONE;
   787     fun arg (_ $ t) = t;
   788   in
   789     if isGoal G then close (arg G) L eAssume_tac
   790     else if isGoal L then close G (arg L) eAssume_tac
   791     else if isNot G then close (arg G) L eContr_tac
   792     else if isNot L then close G (arg L) eContr_tac
   793     else NONE
   794   end;
   795 
   796 (*Were there Skolem terms in the premise?  Must NOT chase Vars*)
   797 fun hasSkolem (Skolem _)     = true
   798   | hasSkolem (Abs (_,body)) = hasSkolem body
   799   | hasSkolem (f$t)          =  hasSkolem f orelse hasSkolem t
   800   | hasSkolem _              = false;
   801 
   802 (*Attach the right "may duplicate" flag to new formulae: if they contain
   803   Skolem terms then allow duplication.*)
   804 fun joinMd md [] = []
   805   | joinMd md (G::Gs) = (G, hasSkolem G orelse md) :: joinMd md Gs;
   806 
   807 
   808 (** Backtracking and Pruning **)
   809 
   810 (*clashVar vars (n,trail) determines whether any of the last n elements
   811   of "trail" occur in "vars" OR in their instantiations*)
   812 fun clashVar [] = (fn _ => false)
   813   | clashVar vars =
   814       let fun clash (0, _)     = false
   815             | clash (_, [])    = false
   816             | clash (n, v::vs) = exists (varOccur v) vars orelse clash(n-1,vs)
   817       in  clash  end;
   818 
   819 
   820 (*nbrs = # of branches just prior to closing this one.  Delete choice points
   821   for goals proved by the latest inference, provided NO variables in the
   822   next branch have been updated.*)
   823 fun prune (1, nxtVars, choices) = choices  (*DON'T prune at very end: allow
   824                                              backtracking over bad proofs*)
   825   | prune (nbrs: int, nxtVars, choices) =
   826       let fun traceIt last =
   827                 let val ll = length last
   828                     and lc = length choices
   829                 in if !trace andalso ll<lc then
   830                     (writeln("Pruning " ^ Int.toString(lc-ll) ^ " levels");
   831                      last)
   832                    else last
   833                 end
   834           fun pruneAux (last, _, _, []) = last
   835             | pruneAux (last, ntrl, trl, (ntrl',nbrs',exn) :: choices) =
   836                 if nbrs' < nbrs
   837                 then last  (*don't backtrack beyond first solution of goal*)
   838                 else if nbrs' > nbrs then pruneAux (last, ntrl, trl, choices)
   839                 else (* nbrs'=nbrs *)
   840                      if clashVar nxtVars (ntrl-ntrl', trl) then last
   841                      else (*no clashes: can go back at least this far!*)
   842                           pruneAux(choices, ntrl', List.drop(trl, ntrl-ntrl'),
   843                                    choices)
   844   in  traceIt (pruneAux (choices, !ntrail, !trail, choices))  end;
   845 
   846 fun nextVars ({pairs, lits, vars, lim} :: _) = map Var vars
   847   | nextVars []                              = [];
   848 
   849 fun backtrack (choices as (ntrl, nbrs, exn)::_) =
   850       (if !trace then (writeln ("Backtracking; now there are " ^
   851                                 Int.toString nbrs ^ " branches"))
   852                  else ();
   853        raise exn)
   854   | backtrack _ = raise PROVE;
   855 
   856 (*Add the literal G, handling *Goal* and detecting duplicates.*)
   857 fun addLit (Const ("*Goal*", _) $ G, lits) =
   858       (*New literal is a *Goal*, so change all other Goals to Nots*)
   859       let fun bad (Const ("*Goal*", _) $ _) = true
   860             | bad (Const (c, _) $ G')   = c = Data.not_name andalso G aconv G'
   861             | bad _                   = false;
   862           fun change [] = []
   863             | change (lit :: lits) =
   864                 (case lit of
   865                   Const (c, _) $ G' =>
   866                     if c = "*Goal*" orelse c = Data.not_name then
   867                       if G aconv G' then change lits
   868                       else negate G' :: change lits
   869                     else lit :: change lits
   870                 | _ => lit :: change lits)
   871       in
   872         Const ("*Goal*", []) $ G :: (if exists bad lits then change lits else lits)
   873       end
   874   | addLit (G,lits) = ins_term(G, lits)
   875 
   876 
   877 (*For calculating the "penalty" to assess on a branching factor of n
   878   log2 seems a little too severe*)
   879 fun log n = if n<4 then 0 else 1 + log(n div 4);
   880 
   881 
   882 (*match(t,u) says whether the term u might be an instance of the pattern t
   883   Used to detect "recursive" rules such as transitivity*)
   884 fun match (Var _) u   = true
   885   | match (Const (a,tas)) (Const (b,tbs)) =
   886       a = "*Goal*" andalso b = Data.not_name orelse
   887       a = Data.not_name andalso b = "*Goal*" orelse
   888       a = b andalso matchs tas tbs
   889   | match (Free a)        (Free b)        = (a=b)
   890   | match (Bound i)       (Bound j)       = (i=j)
   891   | match (Abs(_,t))      (Abs(_,u))      = match t u
   892   | match (f$t)           (g$u)           = match f g andalso match t u
   893   | match t               u   = false
   894 and matchs [] [] = true
   895   | matchs (t :: ts) (u :: us) = match t u andalso matchs ts us;
   896 
   897 
   898 (*Branches closed: number of branches closed during the search
   899   Branches tried:  number of branches created by splitting (counting from 1)*)
   900 val nclosed = ref 0
   901 and ntried  = ref 1;
   902 
   903 fun printStats (b, start, tacs) =
   904   if b then
   905     writeln (end_timing start ^ " for search.  Closed: "
   906              ^ Int.toString (!nclosed) ^
   907              " tried: " ^ Int.toString (!ntried) ^
   908              " tactics: " ^ Int.toString (length tacs))
   909   else ();
   910 
   911 
   912 (*Tableau prover based on leanTaP.  Argument is a list of branches.  Each
   913   branch contains a list of unexpanded formulae, a list of literals, and a
   914   bound on unsafe expansions.
   915  "start" is CPU time at start, for printing search time
   916 *)
   917 fun prove (sign, start, cs, brs, cont) =
   918  let val {safe0_netpair, safep_netpair, haz_netpair, ...} = Data.rep_cs cs
   919      val safeList = [safe0_netpair, safep_netpair]
   920      and hazList  = [haz_netpair]
   921      fun prv (tacs, trs, choices, []) =
   922                 (printStats (!trace orelse !stats, start, tacs);
   923                  cont (tacs, trs, choices))   (*all branches closed!*)
   924        | prv (tacs, trs, choices,
   925               brs0 as {pairs = ((G,md)::br, haz)::pairs,
   926                        lits, vars, lim} :: brs) =
   927              (*apply a safe rule only (possibly allowing instantiation);
   928                defer any haz formulae*)
   929           let exception PRV (*backtrack to precisely this recursion!*)
   930               val ntrl = !ntrail
   931               val nbrs = length brs0
   932               val nxtVars = nextVars brs
   933               val G = norm G
   934               val rules = netMkRules G vars safeList
   935               (*Make a new branch, decrementing "lim" if instantiations occur*)
   936               fun newBr (vars',lim') prems =
   937                   map (fn prem =>
   938                        if (exists isGoal prem)
   939                        then {pairs = ((joinMd md prem, []) ::
   940                                       negOfGoals ((br, haz)::pairs)),
   941                              lits  = map negOfGoal lits,
   942                              vars  = vars',
   943                              lim   = lim'}
   944                        else {pairs = ((joinMd md prem, []) ::
   945                                       (br, haz) :: pairs),
   946                              lits = lits,
   947                              vars = vars',
   948                              lim  = lim'})
   949                   prems @
   950                   brs
   951               (*Seek a matching rule.  If unifiable then add new premises
   952                 to branch.*)
   953               fun deeper [] = raise NEWBRANCHES
   954                 | deeper (((P,prems),tac)::grls) =
   955                     if unify(add_term_vars(P,[]), P, G)
   956                     then  (*P comes from the rule; G comes from the branch.*)
   957                      let val updated = ntrl < !ntrail (*branch updated*)
   958                          val lim' = if updated
   959                                     then lim - (1+log(length rules))
   960                                     else lim   (*discourage branching updates*)
   961                          val vars  = vars_in_vars vars
   962                          val vars' = foldr add_terms_vars vars prems
   963                          val choices' = (ntrl, nbrs, PRV) :: choices
   964                          val tacs' = (tac(updated,false,true))
   965                                      :: tacs  (*no duplication; rotate*)
   966                      in
   967                          traceNew prems;  traceVars sign ntrl;
   968                          (if null prems then (*closed the branch: prune!*)
   969                             (nclosed := !nclosed + 1;
   970                              prv(tacs',  brs0::trs,
   971                                  prune (nbrs, nxtVars, choices'),
   972                                  brs))
   973                           else (*prems non-null*)
   974                           if lim'<0 (*faster to kill ALL the alternatives*)
   975                           then (traceMsg"Excessive branching: KILLED";
   976                                 clearTo ntrl;  raise NEWBRANCHES)
   977                           else
   978                             (ntried := !ntried + length prems - 1;
   979                              prv(tacs',  brs0::trs, choices',
   980                                  newBr (vars',lim') prems)))
   981                          handle PRV =>
   982                            if updated then
   983                                 (*Backtrack at this level.
   984                                   Reset Vars and try another rule*)
   985                                 (clearTo ntrl;  deeper grls)
   986                            else (*backtrack to previous level*)
   987                                 backtrack choices
   988                      end
   989                     else deeper grls
   990               (*Try to close branch by unifying with head goal*)
   991               fun closeF [] = raise CLOSEF
   992                 | closeF (L::Ls) =
   993                     case tryClose(G,L) of
   994                         NONE     => closeF Ls
   995                       | SOME tac =>
   996                             let val choices' =
   997                                     (if !trace then (Output.immediate_output"branch closed";
   998                                                      traceVars sign ntrl)
   999                                                else ();
  1000                                      prune (nbrs, nxtVars,
  1001                                             (ntrl, nbrs, PRV) :: choices))
  1002                             in  nclosed := !nclosed + 1;
  1003                                 prv (tac::tacs, brs0::trs, choices', brs)
  1004                                 handle PRV =>
  1005                                     (*reset Vars and try another literal
  1006                                       [this handler is pruned if possible!]*)
  1007                                  (clearTo ntrl;  closeF Ls)
  1008                             end
  1009               (*Try to unify a queued formula (safe or haz) with head goal*)
  1010               fun closeFl [] = raise CLOSEF
  1011                 | closeFl ((br, haz)::pairs) =
  1012                     closeF (map fst br)
  1013                       handle CLOSEF => closeF (map fst haz)
  1014                         handle CLOSEF => closeFl pairs
  1015           in tracing sign brs0;
  1016              if lim<0 then (traceMsg "Limit reached.  "; backtrack choices)
  1017              else
  1018              prv (Data.hyp_subst_tac trace :: tacs,
  1019                   brs0::trs,  choices,
  1020                   equalSubst sign
  1021                     (G, {pairs = (br,haz)::pairs,
  1022                          lits  = lits, vars  = vars, lim   = lim})
  1023                     :: brs)
  1024              handle DEST_EQ =>   closeF lits
  1025               handle CLOSEF =>   closeFl ((br,haz)::pairs)
  1026                 handle CLOSEF => deeper rules
  1027                   handle NEWBRANCHES =>
  1028                    (case netMkRules G vars hazList of
  1029                        [] => (*there are no plausible haz rules*)
  1030                              (traceMsg "moving formula to literals";
  1031                               prv (tacs, brs0::trs, choices,
  1032                                    {pairs = (br,haz)::pairs,
  1033                                     lits  = addLit(G,lits),
  1034                                     vars  = vars,
  1035                                     lim   = lim}  :: brs))
  1036                     | _ => (*G admits some haz rules: try later*)
  1037                            (traceMsg "moving formula to haz list";
  1038                             prv (if isGoal G then negOfGoal_tac :: tacs
  1039                                              else tacs,
  1040                                  brs0::trs,
  1041                                  choices,
  1042                                  {pairs = (br, haz@[(negOfGoal G, md)])::pairs,
  1043                                   lits  = lits,
  1044                                   vars  = vars,
  1045                                   lim   = lim}  :: brs)))
  1046           end
  1047        | prv (tacs, trs, choices,
  1048               {pairs = ([],haz)::(Gs,haz')::pairs, lits, vars, lim} :: brs) =
  1049              (*no more "safe" formulae: transfer haz down a level*)
  1050            prv (tacs, trs, choices,
  1051                 {pairs = (Gs,haz@haz')::pairs,
  1052                  lits  = lits,
  1053                  vars  = vars,
  1054                  lim    = lim} :: brs)
  1055        | prv (tacs, trs, choices,
  1056               brs0 as {pairs = [([], (H,md)::Hs)],
  1057                        lits, vars, lim} :: brs) =
  1058              (*no safe steps possible at any level: apply a haz rule*)
  1059           let exception PRV (*backtrack to precisely this recursion!*)
  1060               val H = norm H
  1061               val ntrl = !ntrail
  1062               val rules = netMkRules H vars hazList
  1063               (*new premises of haz rules may NOT be duplicated*)
  1064               fun newPrem (vars,P,dup,lim') prem =
  1065                   let val Gs' = map (fn Q => (Q,false)) prem
  1066                       and Hs' = if dup then Hs @ [(negOfGoal H, md)] else Hs
  1067                       and lits' = if (exists isGoal prem)
  1068                                   then map negOfGoal lits
  1069                                   else lits
  1070                   in  {pairs = if exists (match P) prem then [(Gs',Hs')]
  1071                                (*Recursive in this premise.  Don't make new
  1072                                  "stack frame".  New haz premises will end up
  1073                                  at the BACK of the queue, preventing
  1074                                  exclusion of others*)
  1075                             else [(Gs',[]), ([],Hs')],
  1076                        lits = lits',
  1077                        vars = vars,
  1078                        lim  = lim'}
  1079                   end
  1080               fun newBr x prems = map (newPrem x) prems  @  brs
  1081               (*Seek a matching rule.  If unifiable then add new premises
  1082                 to branch.*)
  1083               fun deeper [] = raise NEWBRANCHES
  1084                 | deeper (((P,prems),tac)::grls) =
  1085                     if unify(add_term_vars(P,[]), P, H)
  1086                     then
  1087                      let val updated = ntrl < !ntrail (*branch updated*)
  1088                          val vars  = vars_in_vars vars
  1089                          val vars' = foldr add_terms_vars vars prems
  1090                             (*duplicate H if md permits*)
  1091                          val dup = md (*earlier had "andalso vars' <> vars":
  1092                                   duplicate only if the subgoal has new vars*)
  1093                              (*any instances of P in the subgoals?
  1094                                NB: boolean "recur" affects tracing only!*)
  1095                          and recur = exists (exists (match P)) prems
  1096                          val lim' = (*Decrement "lim" extra if updates occur*)
  1097                              if updated then lim - (1+log(length rules))
  1098                              else lim-1
  1099                                  (*It is tempting to leave "lim" UNCHANGED if
  1100                                    both dup and recur are false.  Proofs are
  1101                                    found at shallower depths, but looping
  1102                                    occurs too often...*)
  1103                          val mayUndo =
  1104                              (*Allowing backtracking from a rule application
  1105                                if other matching rules exist, if the rule
  1106                                updated variables, or if the rule did not
  1107                                introduce new variables.  This latter condition
  1108                                means it is not a standard "gamma-rule" but
  1109                                some other form of unsafe rule.  Aim is to
  1110                                emulate Fast_tac, which allows all unsafe steps
  1111                                to be undone.*)
  1112                              not(null grls)   (*other rules to try?*)
  1113                              orelse updated
  1114                              orelse vars=vars'   (*no new Vars?*)
  1115                          val tac' = tac(updated, dup, true)
  1116                        (*if recur then perhaps shouldn't call rotate_tac: new
  1117                          formulae should be last, but that's WRONG if the new
  1118                          formulae are Goals, since they remain in the first
  1119                          position*)
  1120 
  1121                      in
  1122                        if lim'<0 andalso not (null prems)
  1123                        then (*it's faster to kill ALL the alternatives*)
  1124                            (traceMsg"Excessive branching: KILLED";
  1125                             clearTo ntrl;  raise NEWBRANCHES)
  1126                        else
  1127                          traceNew prems;
  1128                          if !trace andalso dup then Output.immediate_output" (duplicating)"
  1129                                                  else ();
  1130                          if !trace andalso recur then Output.immediate_output" (recursive)"
  1131                                                  else ();
  1132                          traceVars sign ntrl;
  1133                          if null prems then nclosed := !nclosed + 1
  1134                          else ntried := !ntried + length prems - 1;
  1135                          prv(tac' :: tacs,
  1136                              brs0::trs,
  1137                              (ntrl, length brs0, PRV) :: choices,
  1138                              newBr (vars', P, dup, lim') prems)
  1139                           handle PRV =>
  1140                               if mayUndo
  1141                               then (*reset Vars and try another rule*)
  1142                                    (clearTo ntrl;  deeper grls)
  1143                               else (*backtrack to previous level*)
  1144                                    backtrack choices
  1145                      end
  1146                     else deeper grls
  1147           in tracing sign brs0;
  1148              if lim<1 then (traceMsg "Limit reached.  "; backtrack choices)
  1149              else deeper rules
  1150              handle NEWBRANCHES =>
  1151                  (*cannot close branch: move H to literals*)
  1152                  prv (tacs,  brs0::trs,  choices,
  1153                       {pairs = [([], Hs)],
  1154                        lits  = H::lits,
  1155                        vars  = vars,
  1156                        lim   = lim}  :: brs)
  1157           end
  1158        | prv (tacs, trs, choices, _ :: brs) = backtrack choices
  1159  in prv ([], [], [(!ntrail, length brs, PROVE)], brs) end;
  1160 
  1161 
  1162 (*Construct an initial branch.*)
  1163 fun initBranch (ts,lim) =
  1164     {pairs = [(map (fn t => (t,true)) ts, [])],
  1165      lits  = [],
  1166      vars  = add_terms_vars (ts,[]),
  1167      lim   = lim};
  1168 
  1169 
  1170 (*** Conversion & Skolemization of the Isabelle proof state ***)
  1171 
  1172 (*Make a list of all the parameters in a subgoal, even if nested*)
  1173 local open Term
  1174 in
  1175 fun discard_foralls (Const("all",_)$Abs(a,T,t)) = discard_foralls t
  1176   | discard_foralls t = t;
  1177 end;
  1178 
  1179 (*List of variables not appearing as arguments to the given parameter*)
  1180 fun getVars []                  i = []
  1181   | getVars ((_,(v,is))::alist) (i: int) =
  1182         if member (op =) is i then getVars alist i
  1183         else v :: getVars alist i;
  1184 
  1185 exception TRANS of string;
  1186 
  1187 (*Translation of a subgoal: Skolemize all parameters*)
  1188 fun fromSubgoal t =
  1189   let val alistVar = ref []
  1190       and alistTVar = ref []
  1191       fun hdvar ((ix,(v,is))::_) = v
  1192       fun from lev t =
  1193         let val (ht,ts) = Term.strip_comb t
  1194             fun apply u = list_comb (u, map (from lev) ts)
  1195             fun bounds [] = []
  1196               | bounds (Term.Bound i::ts) =
  1197                   if i<lev then raise TRANS
  1198                       "Function unknown's argument not a parameter"
  1199                   else i-lev :: bounds ts
  1200               | bounds ts = raise TRANS
  1201                       "Function unknown's argument not a bound variable"
  1202         in
  1203           case ht of
  1204               Term.Const aT    => apply (fromConst alistTVar aT)
  1205             | Term.Free  (a,_) => apply (Free a)
  1206             | Term.Bound i     => apply (Bound i)
  1207             | Term.Var (ix,_) =>
  1208                   (case (AList.lookup (op =) (!alistVar) ix) of
  1209                        NONE => (alistVar := (ix, (ref NONE, bounds ts))
  1210                                           :: !alistVar;
  1211                                 Var (hdvar(!alistVar)))
  1212                      | SOME(v,is) => if is=bounds ts then Var v
  1213                             else raise TRANS
  1214                                 ("Discrepancy among occurrences of "
  1215                                  ^ Syntax.string_of_vname ix))
  1216             | Term.Abs (a,_,body) =>
  1217                   if null ts then Abs(a, from (lev+1) body)
  1218                   else raise TRANS "argument not in normal form"
  1219         end
  1220 
  1221       val npars = length (Logic.strip_params t)
  1222 
  1223       (*Skolemize a subgoal from a proof state*)
  1224       fun skoSubgoal i t =
  1225           if i<npars then
  1226               skoSubgoal (i+1)
  1227                 (subst_bound (Skolem (gensym "T_", getVars (!alistVar) i),
  1228                               t))
  1229           else t
  1230 
  1231   in  skoSubgoal 0 (from 0 (discard_foralls t))  end;
  1232 
  1233 
  1234 fun reject_const thy c =
  1235   if is_some (Sign.const_type thy c) then
  1236     error ("Blast: theory contains illegal constant " ^ quote c)
  1237   else ();
  1238 
  1239 fun initialize thy =
  1240  (fullTrace:=[];  trail := [];  ntrail := 0;
  1241   nclosed := 0;  ntried := 1;  typargs := Sign.const_typargs thy;
  1242   reject_const thy "*Goal*"; reject_const thy "*False*");
  1243 
  1244 
  1245 (*Tactic using tableau engine and proof reconstruction.
  1246  "start" is CPU time at start, for printing SEARCH time
  1247         (also prints reconstruction time)
  1248  "lim" is depth limit.*)
  1249 fun timing_depth_tac start cs lim i st0 =
  1250   let val st = (initialize (theory_of_thm st0); ObjectLogic.atomize_goal i st0);
  1251       val sign = Thm.theory_of_thm st
  1252       val skoprem = fromSubgoal (List.nth(prems_of st, i-1))
  1253       val hyps  = strip_imp_prems skoprem
  1254       and concl = strip_imp_concl skoprem
  1255       fun cont (tacs,_,choices) =
  1256           let val start = start_timing ()
  1257           in
  1258           case Seq.pull(EVERY' (rev tacs) i st) of
  1259               NONE => (writeln ("PROOF FAILED for depth " ^
  1260                                 Int.toString lim);
  1261                        if !trace then error "************************\n"
  1262                        else ();
  1263                        backtrack choices)
  1264             | cell => (if (!trace orelse !stats)
  1265                        then writeln (end_timing start ^ " for reconstruction")
  1266                        else ();
  1267                        Seq.make(fn()=> cell))
  1268           end
  1269   in prove (sign, start, cs, [initBranch (mkGoal concl :: hyps, lim)], cont)
  1270   end
  1271   handle PROVE     => Seq.empty;
  1272 
  1273 (*Public version with fixed depth*)
  1274 fun depth_tac cs lim i st = timing_depth_tac (start_timing ()) cs lim i st;
  1275 
  1276 val depth_limit = ref 20;
  1277 
  1278 fun blast_tac cs i st =
  1279     ((DEEPEN (1, !depth_limit) (timing_depth_tac (start_timing ()) cs) 0) i
  1280      THEN flexflex_tac) st
  1281     handle TRANS s =>
  1282       ((if !trace then warning ("blast: " ^ s) else ());
  1283        Seq.empty);
  1284 
  1285 fun Blast_tac i = blast_tac (Data.claset()) i;
  1286 
  1287 
  1288 (*** For debugging: these apply the prover to a subgoal and return
  1289      the resulting tactics, trace, etc.                            ***)
  1290 
  1291 (*Translate subgoal i from a proof state*)
  1292 fun trygl cs lim i =
  1293         let val st = topthm()
  1294                 val sign = Thm.theory_of_thm st
  1295                 val skoprem = (initialize (theory_of_thm st);
  1296                                fromSubgoal (List.nth(prems_of st, i-1)))
  1297                 val hyps  = strip_imp_prems skoprem
  1298                 and concl = strip_imp_concl skoprem
  1299         in timeap prove (sign, start_timing (), cs,
  1300                          [initBranch (mkGoal concl :: hyps, lim)], I)
  1301         end
  1302         handle Subscript => error("There is no subgoal " ^ Int.toString i);
  1303 
  1304 fun Trygl lim i = trygl (Data.claset()) lim i;
  1305 
  1306 (*Read a string to make an initial, singleton branch*)
  1307 fun readGoal thy s = Sign.read_prop thy s |> fromTerm |> rand |> mkGoal;
  1308 
  1309 fun tryInThy thy lim s =
  1310     (initialize thy;
  1311      timeap prove (thy,
  1312                    start_timing(),
  1313                    Data.claset(),
  1314                    [initBranch ([readGoal thy s], lim)],
  1315                    I));
  1316 
  1317 
  1318 (** method setup **)
  1319 
  1320 fun blast_args m =
  1321   Method.bang_sectioned_args'
  1322       Data.cla_modifiers (Scan.lift (Scan.option Args.nat)) m;
  1323 
  1324 fun blast_meth NONE = Data.cla_meth' blast_tac
  1325   | blast_meth (SOME lim) = Data.cla_meth' (fn cs => depth_tac cs lim);
  1326 
  1327 val setup =
  1328   Method.add_methods [("blast", blast_args blast_meth, "tableau prover")];
  1329 
  1330 
  1331 end;