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