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