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