src/Provers/blast.ML
 author paulson Sat, 10 Jan 1998 17:59:32 +0100 changeset 4552 bb8ff763c93d parent 4511 93a84eb6c522 child 4651 70dd492a1698 permissions -rw-r--r--
Simplified proofs by omitting PA = {|XA, ...|} from RA2
```
(*  Title: 	Provers/blast.ML
ID:         \$Id\$
Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory

Generic tableau prover with proof reconstruction

SKOLEMIZES ReplaceI WRONGLY: allow new vars in prems, or forbid such rules??
Needs explicit instantiation of assumptions?

Blast_tac is often more powerful than fast_tac, but has some limitations.
Blast_tac...
* ignores elimination rules that don't have the correct format
(conclusion must be a formula variable)
* ignores types, which can make HOL proofs fail
* rules must not require higher-order unification, e.g. apply_type in ZF
+ message "Function Var's argument not a bound variable" relates to this
* its proof strategy is more general but can actually be slower

Known problems:
"Recursive" chains of rules can sometimes exclude other unsafe formulae
from expansion.  This happens because newly-created formulae always
have priority over existing ones.  But obviously recursive rules
such as transitivity are treated specially to prevent this.

prove "In1 x ~: Part A In0" because PartE introducees the polymorphic
equality In1 x = In0 y, when the corresponding rule uses the (distinct)
set equality.  Workaround: supply a type instance of the rule that
creates new equalities (e.g. PartE in HOL/ex/Simult)
==> affects freeness reasoning about Sexp constants (since they have
type ... set)

With substition for equalities (hyp_subst_tac):
When substitution affects a haz formula or literal, it is moved
back to the list of safe formulae.
But there's no way of putting it in the right place.  A "moved" or
"no DETERM" flag would prevent proofs failing here.
*)

(*Should be a type abbreviation?*)
type netpair = (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net;

--The negation symbol is "Not"
--The equality symbol is "op ="
--The is-true judgement symbol is "Trueprop"
--There are no constants named "*Goal* or "*False*"
*)
signature BLAST_DATA =
sig
type claset
val notE		: thm		(* [| ~P;  P |] ==> R *)
val ccontr		: thm
val contr_tac 	: int -> tactic
val dup_intr		: thm -> thm
val hyp_subst_tac     : bool ref -> int -> tactic
val claset		: unit -> claset
val rep_claset	:
claset -> {safeIs: thm list, safeEs: thm list,
hazIs: thm list, hazEs: thm list,
uwrapper: (int -> tactic) -> (int -> tactic),
swrapper: (int -> tactic) -> (int -> tactic),
safe0_netpair: netpair, safep_netpair: netpair,
haz_netpair: netpair, dup_netpair: netpair}
end;

signature BLAST =
sig
type claset
exception TRANS of string    (*reports translation errors*)
datatype term =
Const of string
| TConst of string * term
| Skolem of string * term option ref list
| Free  of string
| Var   of term option ref
| Bound of int
| Abs   of string*term
| \$  of term*term;
type branch
val depth_tac 	: claset -> int -> int -> tactic
val blast_tac 	: claset -> int -> tactic
val Blast_tac 	: int -> tactic
val overloaded 	: string * (Term.typ -> Term.typ) -> unit
(*debugging tools*)
val stats	        : bool ref
val trace	        : bool ref
val fullTrace	        : branch list list ref
val fromType	        : (indexname * term) list ref -> Term.typ -> term
val fromTerm	        : Term.term -> term
val fromSubgoal       : Term.term -> term
val instVars          : term -> (unit -> unit)
val toTerm	        : int -> term -> Term.term
val readGoal          : Sign.sg -> string -> term
val tryInThy		: theory -> int -> string ->
(int->tactic) list * branch list list * (int*int*exn) list
val trygl		: claset -> int -> int ->
(int->tactic) list * branch list list * (int*int*exn) list
val Trygl		: int -> int ->
(int->tactic) list * branch list list * (int*int*exn) list
val normBr		: branch -> branch
end;

functor BlastFun(Data: BLAST_DATA) : BLAST =
struct

type claset = Data.claset;

val trace = ref false
and stats = ref false;   (*for runtime and search statistics*)

datatype term =
Const of string
| TConst of string * term    (*type of overloaded constant--as a term!*)
| Skolem of string * term option ref list
| Free  of string
| Var   of term option ref
| Bound of int
| Abs   of string*term
| op \$  of term*term;

(** Basic syntactic operations **)

fun is_Var (Var _) = true
| is_Var _ = false;

fun dest_Var (Var x) =  x;

fun rand (f\$x) = x;

(* maps   (f, [t1,...,tn])  to  f(t1,...,tn) *)
val list_comb : term * term list -> term = foldl (op \$);

(* maps   f(t1,...,tn)  to  (f, [t1,...,tn]) ; naturally tail-recursive*)
fun strip_comb u : term * term list =
let fun stripc (f\$t, ts) = stripc (f, t::ts)
|   stripc  x =  x
in  stripc(u,[])  end;

(* maps   f(t1,...,tn)  to  f , which is never a combination *)

(** Particular constants **)

fun negate P = Const"Not" \$ P;

fun mkGoal P = Const"*Goal*" \$ P;

fun isGoal (Const"*Goal*" \$ _) = true
| isGoal _                   = false;

val Trueprop = Term.Const("Trueprop", Type("o",[])-->propT);
fun mk_tprop P = Term.\$ (Trueprop, P);

fun isTrueprop (Term.Const("Trueprop",_)) = true
| isTrueprop _                          = false;

(*** Dealing with overloaded constants ***)

(*alist is a map from TVar names to Vars.  We need to unify the TVars
fun fromType alist (Term.Type(a,Ts)) = list_comb (Const a,
map (fromType alist) Ts)
| fromType alist (Term.TFree(a,_)) = Free a
| fromType alist (Term.TVar (ixn,_)) =
(case (assoc_string_int(!alist,ixn)) of
None => let val t' = Var(ref None)
in  alist := (ixn, t') :: !alist;  t'
end
| Some v => v)

local
val overloads = ref ([]: (string * (Term.typ -> Term.typ)) list)
in

(*Convert a possibly overloaded Term.Const to a Blast.Const or Blast.TConst,
converting its type to a Blast.term in the latter case.*)
fun fromConst alist (a,T) =
None   => Const a		(*not overloaded*)
| Some f =>
let val T' = f T
handle Match => error
("Blast_tac: unexpected type for overloaded constant " ^ a)
in  TConst(a, fromType alist T')  end;

end;

(*Tests whether 2 terms are alpha-convertible; chases instantiations*)
fun (Const a)      aconv (Const b)      = a=b
| (TConst (a,ta)) aconv (TConst (b,tb)) = a=b andalso ta aconv tb
| (Skolem (a,_)) aconv (Skolem (b,_)) = a=b  (*arglists must then be equal*)
| (Free a)       aconv (Free b)       = a=b
| (Var(ref(Some t))) aconv u          = t aconv u
| t          aconv (Var(ref(Some u))) = t aconv u
| (Var v)        aconv (Var w)        = v=w	(*both Vars are un-assigned*)
| (Bound i)      aconv (Bound j)      = i=j
| (Abs(_,t))     aconv (Abs(_,u))     = t aconv u
| (f\$t)          aconv (g\$u)          = (f aconv g) andalso (t aconv u)
| _ aconv _  =  false;

fun mem_term (_, [])     = false
| mem_term (t, t'::ts) = t aconv t' orelse mem_term(t,ts);

fun ins_term(t,ts) = if mem_term(t,ts) then ts else t :: ts;

fun mem_var (v: term option ref, []) = false
| mem_var (v, v'::vs)              = v=v' orelse mem_var(v,vs);

fun ins_var(v,vs) = if mem_var(v,vs) then vs else v :: vs;

(** Vars **)

(*Accumulates the Vars in the term, suppressing duplicates*)
| add_term_vars (Var (v as ref None),	vars) = ins_var (v, vars)
| add_term_vars (_,	vars) = vars
(*Term list version.  [The fold functionals are slow]*)
and add_terms_vars ([],    vars) = vars
(*Var list version.*)
and add_vars_vars ([],    vars) = vars
| add_vars_vars (ref (Some u) :: vs, vars) =
| add_vars_vars (v::vs, vars) =   (*v must be a ref None*)

(*Chase assignments in "vars"; return a list of unassigned variables*)

(*increment a term's non-local bound variables
inc is  increment for bound variables
lev is  level at which a bound variable is considered 'loose'*)
fun incr_bv (inc, lev, u as Bound i) = if i>=lev then Bound(i+inc) else u
| incr_bv (inc, lev, Abs(a,body)) = Abs(a, incr_bv(inc,lev+1,body))
| incr_bv (inc, lev, f\$t) = incr_bv(inc,lev,f) \$ incr_bv(inc,lev,t)
| incr_bv (inc, lev, u) = u;

fun incr_boundvars  0  t = t
| incr_boundvars inc t = incr_bv(inc,0,t);

(*Accumulate all 'loose' bound vars referring to level 'lev' or beyond.
(Bound 0) is loose at level 0 *)
fun add_loose_bnos (Bound i, lev, js)   = if i<lev then js
else  (i-lev) ins_int js
| add_loose_bnos (f\$t, lev, js)       =
| add_loose_bnos (_, _, js)           = js;

fun loose_bnos t = add_loose_bnos (t, 0, []);

fun subst_bound (arg, t) : term =
let fun subst (t as Bound i, lev) =
if i<lev then  t    (*var is locally bound*)
else  if i=lev then incr_boundvars lev arg
else Bound(i-1)  (*loose: change it*)
| subst (Abs(a,body), lev) = Abs(a, subst(body,lev+1))
| subst (f\$t, lev) =  subst(f,lev)  \$  subst(t,lev)
| subst (t,lev)    = t
in  subst (t,0)  end;

(*Normalize...but not the bodies of ABSTRACTIONS*)
fun norm t = case t of
Skolem (a,args)      => Skolem(a, vars_in_vars args)
| TConst(a,aT)         => TConst(a, norm aT)
| (Var (ref None))     => t
| (Var (ref (Some u))) => norm u
| (f \$ u) => (case norm f of
Abs(_,body) => norm (subst_bound (u, body))
| nf => nf \$ norm u)
| _ => t;

(*Weak (one-level) normalize for use in unification*)
fun wkNormAux t = case t of
(Var v) => (case !v of
Some u => wkNorm u
| None   => t)
| (f \$ u) => (case wkNormAux f of
Abs(_,body) => wkNorm (subst_bound (u, body))
| nf          => nf \$ u)
| Abs (a,body) =>	(*eta-contract if possible*)
(case wkNormAux body of
nb as (f \$ t) =>
if (0 mem_int loose_bnos f) orelse wkNorm t <> Bound 0
then Abs(a,nb)
else wkNorm (incr_boundvars ~1 f)
| nb => Abs (a,nb))
| _ => t
and wkNorm t = case head_of t of
Const _        => t
| TConst _       => t
| Skolem(a,args) => t
| Free _         => t
| _              => wkNormAux t;

(*Does variable v occur in u?  For unification.*)
fun varOccur v =
let fun occL [] = false	(*same as (exists occ), but faster*)
| occL (u::us) = occ u orelse occL us
and occ (Var w) =
v=w orelse
(case !w of None   => false
| Some u => occ u)
| occ (Skolem(_,args)) = occL (map Var args)
| occ (TConst(_,u)) = occ u
| occ (Abs(_,u)) = occ u
| occ (f\$u)      = occ u  orelse  occ f
| occ (_)        = false;
in  occ  end;

exception UNIFY;

val trail = ref [] : term option ref list ref;
val ntrail = ref 0;

(*Restore the trail to some previous state: for backtracking*)
fun clearTo n =
while !ntrail<>n do
(hd(!trail) := None;
trail := tl (!trail);
ntrail := !ntrail - 1);

(*First-order unification with bound variables.
"vars" is a list of variables local to the rule and NOT to be put
on the trail (no point in doing so)
*)
fun unify(vars,t,u) =
let val n = !ntrail
fun update (t as Var v, u) =
if t aconv u then ()
else if varOccur v u then raise UNIFY
else if mem_var(v, vars) then v := Some u
else (*avoid updating Vars in the branch if possible!*)
if is_Var u andalso mem_var(dest_Var u, vars)
then dest_Var u := Some t
else (v := Some u;
trail := v :: !trail;  ntrail := !ntrail + 1)
fun unifyAux (t,u) =
case (wkNorm t,  wkNorm u) of
(nt as Var v,  nu) => update(nt,nu)
| (nu,  nt as Var v) => update(nt,nu)
| (TConst(a,at), TConst(b,bt)) => if a=b then unifyAux(at,bt)
else raise UNIFY
| (Abs(_,t'),  Abs(_,u')) => unifyAux(t',u')
(*NB: can yield unifiers having dangling Bound vars!*)
| (f\$t',  g\$u') => (unifyAux(f,g); unifyAux(t',u'))
| (nt,  nu)    => if nt aconv nu then () else raise UNIFY
in  (unifyAux(t,u); true) handle UNIFY => (clearTo n; false)
end;

(*Convert from "real" terms to prototerms; eta-contract
Code is duplicated with fromSubgoal.  Correct this?*)
fun fromTerm t =
let val alistVar = ref []
and alistTVar = ref []
fun from (Term.Const aT) = fromConst alistTVar aT
| from (Term.Free  (a,_)) = Free a
| from (Term.Bound i)     = Bound i
| from (Term.Var (ixn,T)) =
(case (assoc_string_int(!alistVar,ixn)) of
None => let val t' = Var(ref None)
in  alistVar := (ixn, t') :: !alistVar;  t'
end
| Some v => v)
| from (Term.Abs (a,_,u)) =
(case  from u  of
u' as (f \$ Bound 0) =>
if (0 mem_int loose_bnos f) then Abs(a,u')
else incr_boundvars ~1 f
| u' => Abs(a,u'))
| from (Term.\$ (f,u)) = from f \$ from u
in  from t  end;

(*A debugging function: replaces all Vars by dummy Frees for visual inspection
of whether they are distinct.  Function revert undoes the assignments.*)
fun instVars t =
let val name = ref "A"
val updated = ref []
fun inst (TConst(a,t)) = inst t
| inst (Var(v as ref None)) = (updated := v :: (!updated);
v       := Some (Free ("?" ^ !name));
name    := bump_string (!name))
| inst (Abs(a,t))    = inst t
| inst (f \$ u)       = (inst f; inst u)
| inst _             = ()
fun revert() = seq (fn v => v:=None) (!updated)
in  inst t; revert  end;

(* A1==>...An==>B  goes to  [A1,...,An], where B is not an implication *)
fun strip_imp_prems (Const"==>" \$ (Const"Trueprop" \$ A) \$ B) =
A :: strip_imp_prems B
| strip_imp_prems (Const"==>" \$ A \$ B) = A :: strip_imp_prems B
| strip_imp_prems _ = [];

(* A1==>...An==>B  goes to B, where B is not an implication *)
fun strip_imp_concl (Const"==>" \$ A \$ B) = strip_imp_concl B
| strip_imp_concl (Const"Trueprop" \$ A) = A
| strip_imp_concl A = A : term;

(*** Conversion of Elimination Rules to Tableau Operations ***)

(*The conclusion becomes the goal/negated assumption *False*: delete it!*)
fun squash_nots [] = []
| squash_nots (Const "*Goal*" \$ (Var (ref (Some (Const"*False*")))) :: Ps) =
squash_nots Ps
| squash_nots (Const "Not" \$ (Var (ref (Some (Const"*False*")))) :: Ps) =
squash_nots Ps
| squash_nots (P::Ps) = P :: squash_nots Ps;

fun skoPrem vars (Const "all" \$ Abs (_, P)) =
skoPrem vars (subst_bound (Skolem (gensym "S_", vars), P))
| skoPrem vars P = P;

fun convertPrem t =
squash_nots (mkGoal (strip_imp_concl t) :: strip_imp_prems t);

(*Expects elimination rules to have a formula variable as conclusion*)
fun convertRule vars t =
let val (P::Ps) = strip_imp_prems t
val Var v   = strip_imp_concl t
in  v := Some (Const"*False*");
(P, map (convertPrem o skoPrem vars) Ps)
end;

(*Like dup_elim, but puts the duplicated major premise FIRST*)
fun rev_dup_elim th = th RSN (2, revcut_rl) |> assumption 2 |> Seq.hd;

(*Rotate the assumptions in all new subgoals for the LIFO discipline*)
local
(*Count new hyps so that they can be rotated*)
fun nNewHyps []                         = 0
| nNewHyps (Const "*Goal*" \$ _ :: Ps) = nNewHyps Ps
| nNewHyps (P::Ps)                    = 1 + nNewHyps Ps;

fun rot_tac [] i st      = Seq.single (Seq.hd (flexflex_rule st))
| rot_tac (0::ks) i st = rot_tac ks (i+1) st
| rot_tac (k::ks) i st = rot_tac ks (i+1) (rotate_rule (~k) i st);
in
fun rot_subgoals_tac (rot, rl) =
rot_tac (if rot then map nNewHyps rl else [])
end;

fun TRACE rl tac st i = if !trace then (prth rl; tac st i) else tac st i;

(*Tableau rule from elimination rule.  Flag "dup" requests duplication of the
affected formula.*)
fun fromRule vars rl =
let val trl = rl |> rep_thm |> #prop |> fromTerm |> convertRule vars
fun tac (dup,rot) i =
TRACE rl (etac (if dup then rev_dup_elim rl else rl)) i
THEN
rot_subgoals_tac (rot, #2 trl) i
in Option.SOME (trl, tac) end
handle Bind => (*reject: conclusion is not just a variable*)
(if !trace then (warning ("ignoring ill-formed elimination rule\n" ^
string_of_thm rl))
else ();
Option.NONE);

(*** Conversion of Introduction Rules ***)

fun convertIntrPrem t = mkGoal (strip_imp_concl t) :: strip_imp_prems t;

fun convertIntrRule vars t =
let val Ps = strip_imp_prems t
val P  = strip_imp_concl t
in  (mkGoal P, map (convertIntrPrem o skoPrem vars) Ps)
end;

(*Tableau rule from introduction rule.  Since haz rules are now delayed,
"dup" is always FALSE for introduction rules.*)
fun fromIntrRule vars rl =
let val trl = rl |> rep_thm |> #prop |> fromTerm |> convertIntrRule vars
fun tac (dup,rot) i =
TRACE rl (rtac (if dup then Data.dup_intr rl else rl)) i
THEN
rot_subgoals_tac (rot, #2 trl) i
in (trl, tac) end;

val dummyVar = Term.Var (("etc",0), dummyT);

(*Convert from prototerms to ordinary terms with dummy types
Ignore abstractions; identify all Vars; STOP at given depth*)
fun toTerm 0 _             = dummyVar
| toTerm d (Const a)     = Term.Const (a,dummyT)
| toTerm d (TConst(a,_)) = Term.Const (a,dummyT)  (*no need to convert type*)
| toTerm d (Skolem(a,_)) = Term.Const (a,dummyT)
| toTerm d (Free a)      = Term.Free  (a,dummyT)
| toTerm d (Bound i)     = Term.Bound i
| toTerm d (Var _)       = dummyVar
| toTerm d (Abs(a,_))    = dummyVar
| toTerm d (f \$ u)       = Term.\$ (toTerm d f, toTerm (d-1) u);

fun netMkRules P vars (nps: netpair list) =
case P of
(Const "*Goal*" \$ G) =>
let val pG = mk_tprop (toTerm 2 G)
val intrs = List.concat
(map (fn (inet,_) => Net.unify_term inet pG)
nps)
in  map (fromIntrRule vars o #2) (orderlist intrs)  end
| _ =>
let val pP = mk_tprop (toTerm 3 P)
val elims = List.concat
(map (fn (_,enet) => Net.unify_term enet pP)
nps)
in  List.mapPartial (fromRule vars o #2) (orderlist elims)  end;

(**
end;
**)

(*Pending formulae carry md (may duplicate) flags*)
type branch = ((term*bool) list *	(*safe formulae on this level*)
(term*bool) list) list * (*haz formulae  on this level*)
term list *               (*literals: irreducible formulae*)
term option ref list *    (*variables occurring in branch*)
int;                      (*resource limit*)

val fullTrace = ref[] : branch list list ref;

(*Normalize a branch--for tracing*)
fun norm2 (G,md) = (norm G, md);

fun normLev (Gs,Hs) = (map norm2 Gs, map norm2 Hs);

fun normBr (br, lits, vars, lim) =
(map normLev br, map norm lits, vars, lim);

val dummyTVar = Term.TVar(("a",0), []);
val dummyVar2 = Term.Var(("var",0), dummyT);

(*convert Blast_tac's type representation to real types for tracing*)
fun showType (Free a)  = Term.TFree (a,[])
| showType (Var _)   = dummyTVar
| showType t         =
(case strip_comb t of
(Const a, us) => Term.Type(a, map showType us)
| _ => dummyT);

fun topType (TConst(a,t)) = Some (showType t)
| topType (Abs(a,t))    = topType t
| topType (f \$ u)       = (case topType f of
None => topType u
| some => some)
| topType _             = None;

(*Convert from prototerms to ordinary terms with dummy types for tracing*)
fun showTerm d (Const a)     = Term.Const (a,dummyT)
| showTerm d (TConst(a,_)) = Term.Const (a,dummyT)
| showTerm d (Skolem(a,_)) = Term.Const (a,dummyT)
| showTerm d (Free a)      = Term.Free  (a,dummyT)
| showTerm d (Bound i)     = Term.Bound i
| showTerm d (Var(ref(Some u))) = showTerm d u
| showTerm d (Var(ref None))    = dummyVar2
| showTerm d (Abs(a,t))    = if d=0 then dummyVar
else Term.Abs(a, dummyT, showTerm (d-1) t)
| showTerm d (f \$ u)       = if d=0 then dummyVar
else Term.\$ (showTerm d f, showTerm (d-1) u);

fun string_of sign d t = Sign.string_of_term sign (showTerm d t);

fun traceTerm sign t =
let val t' = norm t
val stm = string_of sign 8 t'
in
case topType t' of
None   => stm   (*no type to attach*)
| Some T => stm ^ "\t:: " ^ Sign.string_of_typ sign T
end;

(*Print tracing information at each iteration of prover*)
fun tracing sign brs =
let fun printPairs (((G,_)::_,_)::_)  = prs(traceTerm sign G)
| printPairs (([],(H,_)::_)::_) = prs(traceTerm sign H ^ "\t (Unsafe)")
| printPairs _                 = ()
fun printBrs (brs0 as (pairs, lits, _, lim) :: brs) =
(fullTrace := brs0 :: !fullTrace;
seq (fn _ => prs "+") brs;
prs (" [" ^ Int.toString lim ^ "] ");
printPairs pairs;
writeln"")
in if !trace then printBrs (map normBr brs) else ()
end;

fun traceMsg s = if !trace then prs s else ();

(*Tracing: variables updated in the last branch operation?*)
fun traceVars sign ntrl =
if !trace then
(case !ntrail-ntrl of
0 => ()
| 1 => prs"\t1 variable UPDATED:"
| n => prs("\t" ^ Int.toString n ^ " variables UPDATED:");
(*display the instantiations themselves, though no variable names*)
seq (fn v => prs("   " ^ string_of sign 4 (the (!v))))
(List.take(!trail, !ntrail-ntrl));
writeln"")
else ();

(*Tracing: how many new branches are created?*)
fun traceNew prems =
if !trace then
case length prems of
0 => prs"branch closed by rule"
| 1 => prs"branch extended (1 new subgoal)"
| n => prs("branch split: "^ Int.toString n ^ " new subgoals")
else ();

(*** Code for handling equality: naive substitution, like hyp_subst_tac ***)

(*Replace the ATOMIC term "old" by "new" in t*)
fun subst_atomic (old,new) t =
let fun subst (Var(ref(Some u))) = subst u
| subst (Abs(a,body))      = Abs(a, subst body)
| subst (f\$t)              = subst f \$ subst t
| subst t                  = if t aconv old then new else t
in  subst t  end;

(*Eta-contract a term from outside: just enough to reduce it to an atom*)
fun eta_contract_atom (t0 as Abs(a, body)) =
(case  eta_contract2 body  of
f \$ Bound 0 => if (0 mem_int loose_bnos f) then t0
else eta_contract_atom (incr_boundvars ~1 f)
| _ => t0)
| eta_contract_atom t = t
and eta_contract2 (f\$t) = f \$ eta_contract_atom t
| eta_contract2 t     = eta_contract_atom t;

(*When can we safely delete the equality?
Not if it equates two constants; consider 0=1.
Not if it resembles x=t[x], since substitution does not eliminate x.
Not if it resembles ?x=0; another goal could instantiate ?x to Suc(i)
Prefer to eliminate Bound variables if possible.
Result:  true = use as is,  false = reorient first *)

(*Can t occur in u?  For substitution.
Does NOT examine the args of Skolem terms: substitution does not affect them.
REFLEXIVE because hyp_subst_tac fails on x=x.*)
fun substOccur t =
let (*NO vars are permitted in u except the arguments of t, if it is
a Skolem term.  This ensures that no equations are deleted that could
be instantiated to a cycle.  For example, x=?a is rejected because ?a
could be instantiated to Suc(x).*)
val vars = case t of
Skolem(_,vars) => vars
| _ => []
fun occEq u = (t aconv u) orelse occ u
and occ (Var(ref(Some u))) = occEq u
| occ (Var v)            = not (mem_var (v, vars))
| occ (Abs(_,u))         = occEq u
| occ (f\$u)              = occEq u  orelse  occEq f
| occ (_)                = false;
in  occEq  end;

exception DEST_EQ;

(*Take apart an equality (plain or overloaded).  NO constant Trueprop*)
fun dest_eq (Const  "op ="     \$ t \$ u) =
(eta_contract_atom t, eta_contract_atom u)
| dest_eq (TConst("op =",_)  \$ t \$ u) =
(eta_contract_atom t, eta_contract_atom u)
| dest_eq _                           = raise DEST_EQ;

(*Reject the equality if u occurs in (or equals!) t*)
fun check (t,u,v) = if substOccur t u then raise DEST_EQ else v;

(*IF the goal is an equality with a substitutable variable
THEN orient that equality ELSE raise exception DEST_EQ*)
fun orientGoal (t,u) = case (t,u) of
(Skolem _, _) => check(t,u,(t,u))	(*eliminates t*)
| (_, Skolem _) => check(u,t,(u,t))	(*eliminates u*)
| (Free _, _)   => check(t,u,(t,u))	(*eliminates t*)
| (_, Free _)   => check(u,t,(u,t))	(*eliminates u*)
| _             => raise DEST_EQ;

(*Substitute through the branch if an equality goal (else raise DEST_EQ).
Moves affected literals back into the branch, but it is not clear where
they should go: this could make proofs fail.*)
fun equalSubst sign (G, pairs, lits, vars, lim) =
let val (t,u) = orientGoal(dest_eq G)
val subst = subst_atomic (t,u)
fun subst2(G,md) = (subst G, md)
(*substitute throughout list; extract affected formulae*)
fun subForm ((G,md), (changed, pairs)) =
let val nG = subst G
in  if nG aconv G then (changed, (G,md)::pairs)
else ((nG,md)::changed, pairs)
end
(*substitute throughout "stack frame"; extract affected formulae*)
fun subFrame ((Gs,Hs), (changed, frames)) =
let val (changed', Gs') = foldr subForm (Gs, (changed, []))
val (changed'', Hs') = foldr subForm (Hs, (changed', []))
in  (changed'', (Gs',Hs')::frames)  end
(*substitute throughout literals; extract affected ones*)
fun subLit (lit, (changed, nlits)) =
let val nlit = subst lit
in  if nlit aconv lit then (changed, nlit::nlits)
else ((nlit,true)::changed, nlits)
end
val (changed, lits') = foldr subLit (lits, ([], []))
val (changed', pairs') = foldr subFrame (pairs, (changed, []))
in  if !trace then writeln ("Substituting " ^ traceTerm sign u ^
" for " ^ traceTerm sign t ^ " in branch" )
else ();
((changed',[])::pairs',	(*affected formulas, and others*)
lits',			(*unaffected literals*)
vars, lim)
end;

exception NEWBRANCHES and CLOSEF;

exception PROVE;

(*Trying eq_contr_tac first INCREASES the effort, slowing reconstruction*)
val contr_tac = ematch_tac [Data.notE] THEN'
(eq_assume_tac ORELSE' assume_tac);

val eContr_tac  = TRACE Data.notE contr_tac;
val eAssume_tac = TRACE asm_rl   (eq_assume_tac ORELSE' assume_tac);

(*Try to unify complementary literals and return the corresponding tactic. *)
fun tryClose (Const"*Goal*" \$ G,  L) =
if unify([],G,L) then Some eAssume_tac else None
| tryClose (G,  Const"*Goal*" \$ L) =
if unify([],G,L) then Some eAssume_tac else None
| tryClose (Const"Not" \$ G,  L)    =
if unify([],G,L) then Some eContr_tac else None
| tryClose (G,  Const"Not" \$ L)    =
if unify([],G,L) then Some eContr_tac else None
| tryClose _                       = None;

(*Were there Skolem terms in the premise?  Must NOT chase Vars*)
fun hasSkolem (Skolem _)     = true
| hasSkolem (Abs (_,body)) = hasSkolem body
| hasSkolem (f\$t)          =  hasSkolem f orelse hasSkolem t
| hasSkolem _              = false;

(*Attach the right "may duplicate" flag to new formulae: if they contain
Skolem terms then allow duplication.*)
fun joinMd md [] = []
| joinMd md (G::Gs) = (G, hasSkolem G orelse md) :: joinMd md Gs;

(*Convert a Goal to an ordinary Not.  Used also in dup_intr, where a goal like
Ex(P) is duplicated as the assumption ~Ex(P). *)
fun negOfGoal (Const"*Goal*" \$ G) = negate G
| negOfGoal G                   = G;

fun negOfGoal2 (G,md) = (negOfGoal G, md);

(*Converts all Goals to Nots in the safe parts of a branch.  They could
have been moved there from the literals list after substitution (equalSubst).
There can be at most one--this function could be made more efficient.*)
fun negOfGoals pairs = map (fn (Gs,haz) => (map negOfGoal2 Gs, haz)) pairs;

(*Tactic.  Convert *Goal* to negated assumption in FIRST position*)
fun negOfGoal_tac i = TRACE Data.ccontr (rtac Data.ccontr) i THEN
rotate_tac ~1 i;

(** Backtracking and Pruning **)

(*clashVar vars (n,trail) determines whether any of the last n elements
of "trail" occur in "vars" OR in their instantiations*)
fun clashVar [] = (fn _ => false)
| clashVar vars =
let fun clash (0, _)     = false
| clash (_, [])    = false
| clash (n, v::vs) = exists (varOccur v) vars orelse clash(n-1,vs)
in  clash  end;

(*nbrs = # of branches just prior to closing this one.  Delete choice points
for goals proved by the latest inference, provided NO variables in the
next branch have been updated.*)
fun prune (1, nxtVars, choices) = choices  (*DON'T prune at very end: allow
| prune (nbrs, nxtVars, choices) =
let fun traceIt last =
let val ll = length last
and lc = length choices
in if !trace andalso ll<lc then
(writeln("Pruning " ^ Int.toString(lc-ll) ^ " levels");
last)
else last
end
fun pruneAux (last, _, _, []) = last
| pruneAux (last, ntrl, trl, (ntrl',nbrs',exn) :: choices) =
if nbrs' < nbrs
then last  (*don't backtrack beyond first solution of goal*)
else if nbrs' > nbrs then pruneAux (last, ntrl, trl, choices)
else (* nbrs'=nbrs *)
if clashVar nxtVars (ntrl-ntrl', trl) then last
else (*no clashes: can go back at least this far!*)
pruneAux(choices, ntrl', List.drop(trl, ntrl-ntrl'),
choices)
in  traceIt (pruneAux (choices, !ntrail, !trail, choices))  end;

fun nextVars ((br, lits, vars, lim) :: _) = map Var vars
| nextVars []                           = [];

fun backtrack (choices as (ntrl, nbrs, exn)::_) =
(if !trace then (writeln ("Backtracking; now there are " ^
Int.toString nbrs ^ " branches"))
else ();
raise exn)
| backtrack _ = raise PROVE;

(*Add the literal G, handling *Goal* and detecting duplicates.*)
fun addLit (Const "*Goal*" \$ G, lits) =
(*New literal is a *Goal*, so change all other Goals to Nots*)
let fun bad (Const"*Goal*" \$ _) = true
| bad (Const"Not" \$ G')   = G aconv G'
fun change [] = []
| change (Const"*Goal*" \$ G' :: lits) =
if G aconv G' then change lits
else Const"Not" \$ G' :: change lits
| change (Const"Not" \$ G' :: lits)    =
if G aconv G' then change lits
else Const"Not" \$ G' :: change lits
| change (lit::lits) = lit :: change lits
in
Const "*Goal*" \$ G :: (if exists bad lits then change lits else lits)
end
| addLit (G,lits) = ins_term(G, lits)

(*For calculating the "penalty" to assess on a branching factor of n
log2 seems a little too severe*)
fun log n = if n<4 then 0 else 1 + log(n div 4);

(*match(t,u) says whether the term u might be an instance of the pattern t
Used to detect "recursive" rules such as transitivity*)
fun match (Var _) u   = true
| match (Const"*Goal*") (Const"Not")    = true
| match (Const"Not")    (Const"*Goal*") = true
| match (Const a)       (Const b)       = (a=b)
| match (TConst (a,ta)) (TConst (b,tb)) = a=b andalso match ta tb
| match (Free a)        (Free b)        = (a=b)
| match (Bound i)       (Bound j)       = (i=j)
| match (Abs(_,t))      (Abs(_,u))      = match t u
| match (f\$t)           (g\$u)           = match f g andalso match t u
| match t               u   = false;

(*Branches closed: number of branches closed during the search
Branches tried:  number of branches created by splitting (counting from 1)*)
val nclosed = ref 0
and ntried  = ref 1;

fun printStats (b, start, tacs) =
if b then
writeln (endTiming start ^ " for search.  Closed: "
^ Int.toString (!nclosed) ^
" tried: " ^ Int.toString (!ntried) ^
" tactics: " ^ Int.toString (length tacs))
else ();

(*Tableau prover based on leanTaP.  Argument is a list of branches.  Each
branch contains a list of unexpanded formulae, a list of literals, and a
bound on unsafe expansions.
"start" is CPU time at start, for printing search time
*)
fun prove (sign, start, cs, brs, cont) =
let val {safe0_netpair, safep_netpair, haz_netpair, ...} = Data.rep_claset cs
val safeList = [safe0_netpair, safep_netpair]
and hazList  = [haz_netpair]
fun prv (tacs, trs, choices, []) =
(printStats (!trace orelse !stats, start, tacs);
cont (tacs, trs, choices))   (*all branches closed!*)
| prv (tacs, trs, choices,
brs0 as (((G,md)::br, haz)::pairs, lits, vars, lim) :: brs) =
(*apply a safe rule only (possibly allowing instantiation);
defer any haz formulae*)
let exception PRV (*backtrack to precisely this recursion!*)
val ntrl = !ntrail
val nbrs = length brs0
val nxtVars = nextVars brs
val G = norm G
val rules = netMkRules G vars safeList
(*Make a new branch, decrementing "lim" if instantiations occur*)
fun newBr (vars',lim') prems =
map (fn prem =>
if (exists isGoal prem)
then (((joinMd md prem, []) ::
negOfGoals ((br, haz)::pairs)),
map negOfGoal lits,
vars', lim')
else (((joinMd md prem, []) :: (br, haz) :: pairs),
lits, vars', lim'))
prems @
brs
(*Seek a matching rule.  If unifiable then add new premises
to branch.*)
fun deeper [] = raise NEWBRANCHES
| deeper (((P,prems),tac)::grls) =
then  (*P comes from the rule; G comes from the branch.*)
let val ntrl' = !ntrail
val lim' = if ntrl < !ntrail
then lim - (1+log(length rules))
val vars  = vars_in_vars vars
val vars' = foldr add_terms_vars (prems, vars)
val choices' = (ntrl, nbrs, PRV) :: choices
val tacs' = (DETERM o tac(false,true)) :: tacs
(*no duplication; rotate*)
in
traceNew prems;  traceVars sign ntrl;
(if null prems then (*closed the branch: prune!*)
(nclosed := !nclosed + 1;
prv(tacs',  brs0::trs,
prune (nbrs, nxtVars, choices'),
brs))
else (*prems non-null*)
if lim'<0 (*faster to kill ALL the alternatives*)
then (traceMsg"Excessive branching: KILLED\n";
clearTo ntrl;  raise NEWBRANCHES)
else
(ntried := !ntried + length prems - 1;
prv(tacs',  brs0::trs, choices',
newBr (vars',lim') prems)))
handle PRV =>
if ntrl < ntrl' (*Vars have been updated*)
then
(*Backtrack at this level.
Reset Vars and try another rule*)
(clearTo ntrl;  deeper grls)
else (*backtrack to previous level*)
backtrack choices
end
else deeper grls
(*Try to close branch by unifying with head goal*)
fun closeF [] = raise CLOSEF
| closeF (L::Ls) =
case tryClose(G,L) of
None     => closeF Ls
| Some tac =>
let val choices' =
(if !trace then (prs"branch closed";
traceVars sign ntrl)
else ();
prune (nbrs, nxtVars,
(ntrl, nbrs, PRV) :: choices))
in  nclosed := !nclosed + 1;
prv (tac::tacs, brs0::trs, choices', brs)
handle PRV =>
(*reset Vars and try another literal
[this handler is pruned if possible!]*)
(clearTo ntrl;  closeF Ls)
end
fun closeFl [] = raise CLOSEF
| closeFl ((br, haz)::pairs) =
closeF (map fst br)
handle CLOSEF => closeF (map fst haz)
handle CLOSEF => closeFl pairs
in tracing sign brs0;
if lim<0 then (traceMsg "Limit reached.  "; backtrack choices)
else
prv (Data.hyp_subst_tac trace :: tacs,
brs0::trs,  choices,
equalSubst sign (G, (br,haz)::pairs, lits, vars, lim) :: brs)
handle DEST_EQ =>   closeF lits
handle CLOSEF =>   closeFl ((br,haz)::pairs)
handle CLOSEF => deeper rules
handle NEWBRANCHES =>
(case netMkRules G vars hazList of
[] => (*there are no plausible haz rules*)
(traceMsg "moving goal to literals";
prv (tacs, brs0::trs, choices,
::brs))
| _ => (*G admits some haz rules: try later*)
(traceMsg "moving goal to haz list";
prv (if isGoal G then negOfGoal_tac :: tacs
else tacs,
brs0::trs,  choices,
((br, haz@[(negOfGoal G, md)])::pairs,
lits, vars, lim)  ::  brs)))
end
| prv (tacs, trs, choices,
(([],haz)::(Gs,haz')::pairs, lits, vars, lim) :: brs) =
(*no more "safe" formulae: transfer haz down a level*)
prv (tacs, trs, choices,
((Gs,haz@haz')::pairs, lits, vars, lim) :: brs)
| prv (tacs, trs, choices,
brs0 as ([([], (H,md)::Hs)], lits, vars, lim) :: brs) =
(*no safe steps possible at any level: apply a haz rule*)
let exception PRV (*backtrack to precisely this recursion!*)
val H = norm H
val ntrl = !ntrail
val rules = netMkRules H vars hazList
(*new premises of haz rules may NOT be duplicated*)
fun newPrem (vars,P,dup,lim') prem =
let val Gs' = map (fn Q => (Q,false)) prem
and Hs' = if dup then Hs @ [(negOfGoal H, md)] else Hs
and lits' = if (exists isGoal prem)
then map negOfGoal lits
else lits
in  (if exists (match P) prem
then (*Recursive in this premise.
Don't make new "stack frame".
New haz premises will end up at the BACK of the
queue, preventing exclusion of others*)
[(Gs',Hs')]
else [(Gs',[]), ([],Hs')],
lits', vars, lim')
end
fun newBr x prems = map (newPrem x) prems  @  brs
(*Seek a matching rule.  If unifiable then add new premises
to branch.*)
fun deeper [] = raise NEWBRANCHES
| deeper (((P,prems),tac)::grls) =
then
let val ntrl' = !ntrail
val vars  = vars_in_vars vars
val vars' = foldr add_terms_vars (prems, vars)
(*duplicate H if md and the subgoal has new vars*)
val dup = md andalso vars' <> vars
(*any instances of P in the subgoals?*)
and recur = exists (exists (match P)) prems
val lim' = (*Decrement "lim" extra if updates occur*)
if ntrl < !ntrail then lim - (1+log(length rules))
else lim-1
(*It is tempting to leave "lim" UNCHANGED if
both dup and recur are false.  Proofs are
found at shallower depths, but looping
occurs too often...*)
val mayUndo =
(*Allowing backtracking from a rule application
if other matching rules exist, if the rule
updated variables, or if the rule did not
introduce new variables.  This latter condition
means it is not a standard "gamma-rule" but
some other form of unsafe rule.  Aim is to
emulate Fast_tac, which allows all unsafe steps
to be undone.*)
not(null grls)   (*other rules to try?*)
orelse ntrl < ntrl' (*variables updated?*)
orelse vars=vars'   (*no new Vars?*)
val tac' = if mayUndo then tac(dup, true)
else   DETERM o tac(dup, true)
(*if recur then doesn't call rotate_tac:
new formulae should be last*)
in
if lim'<0 andalso not (null prems)
then (*it's faster to kill ALL the alternatives*)
(traceMsg"Excessive branching: KILLED\n";
clearTo ntrl;  raise NEWBRANCHES)
else
traceNew prems;
if !trace andalso recur then prs" (recursive)"
else ();
traceVars sign ntrl;
if null prems then nclosed := !nclosed + 1
else ntried := !ntried + length prems - 1;
prv(tac' :: tacs,
brs0::trs,
(ntrl, length brs0, PRV) :: choices,
newBr (vars', P, dup, lim') prems)
handle PRV =>
if mayUndo
then (*reset Vars and try another rule*)
(clearTo ntrl;  deeper grls)
else (*backtrack to previous level*)
backtrack choices
end
else deeper grls
in tracing sign brs0;
if lim<1 then (traceMsg "Limit reached.  "; backtrack choices)
else deeper rules
handle NEWBRANCHES =>
(*cannot close branch: move H to literals*)
prv (tacs,  brs0::trs,  choices,
([([], Hs)], H::lits, vars, lim)::brs)
end
| prv (tacs, trs, choices, _ :: brs) = backtrack choices
in init_gensym();
prv ([], [], [(!ntrail, length brs, PROVE)], brs)
end;

(*Construct an initial branch.*)
fun initBranch (ts,lim) =
([(map (fn t => (t,true)) ts, [])],

(*** Conversion & Skolemization of the Isabelle proof state ***)

(*Make a list of all the parameters in a subgoal, even if nested*)
local open Term
in
end;

(*List of variables not appearing as arguments to the given parameter*)
fun getVars []                  i = []
| getVars ((_,(v,is))::alist) i =
if i mem is then getVars alist i
else v :: getVars alist i;

exception TRANS of string;

(*Translation of a subgoal: Skolemize all parameters*)
fun fromSubgoal t =
let val alistVar = ref []
and alistTVar = ref []
fun hdvar ((ix,(v,is))::_) = v
fun from lev t =
let val (ht,ts) = Term.strip_comb t
fun apply u = list_comb (u, map (from lev) ts)
fun bounds [] = []
| bounds (Term.Bound i::ts) =
if i<lev then raise TRANS
"Function unknown's argument not a parameter"
else i-lev :: bounds ts
| bounds ts = raise TRANS
"Function unknown's argument not a bound variable"
in
case ht of
Term.Const aT    => apply (fromConst alistTVar aT)
| Term.Free  (a,_) => apply (Free a)
| Term.Bound i     => apply (Bound i)
| Term.Var (ix,_) =>
(case (assoc_string_int(!alistVar,ix)) of
None => (alistVar := (ix, (ref None, bounds ts))
:: !alistVar;
Var (hdvar(!alistVar)))
| Some(v,is) => if is=bounds ts then Var v
else raise TRANS
("Discrepancy among occurrences of ?"
^ Syntax.string_of_vname ix))
| Term.Abs (a,_,body) =>
if null ts then Abs(a, from (lev+1) body)
else raise TRANS "argument not in normal form"
end

val npars = length (Logic.strip_params t)

(*Skolemize a subgoal from a proof state*)
fun skoSubgoal i t =
if i<npars then
skoSubgoal (i+1)
(subst_bound (Skolem (gensym "T_", getVars (!alistVar) i),
t))
else t

in  skoSubgoal 0 (from 0 (discard_foralls t))  end;

fun initialize() =
(fullTrace:=[];  trail := [];  ntrail := 0;
nclosed := 0;  ntried := 1);

(*Tactic using tableau engine and proof reconstruction.
"start" is CPU time at start, for printing SEARCH time
(also prints reconstruction time)
"lim" is depth limit.*)
fun timing_depth_tac start cs lim i st =
(initialize();
let val {sign,...} = rep_thm st
val skoprem = fromSubgoal (List.nth(prems_of st, i-1))
val hyps  = strip_imp_prems skoprem
and concl = strip_imp_concl skoprem
fun cont (tacs,_,choices) =
let val start = startTiming()
in
case Seq.pull(EVERY' (rev tacs) i st) of
None => (writeln ("PROOF FAILED for depth " ^
Int.toString lim);
backtrack choices)
| cell => (if (!trace orelse !stats)
then writeln (endTiming start ^ " for reconstruction")
else ();
Seq.make(fn()=> cell))
end
in prove (sign, start, cs, [initBranch (mkGoal concl :: hyps, lim)], cont)
end
handle PROVE     => Seq.empty);

(*Public version with fixed depth*)
fun depth_tac cs lim i st = timing_depth_tac (startTiming()) cs lim i st;

fun blast_tac cs i st =
(DEEPEN (1,20) (timing_depth_tac (startTiming()) cs) 0) i st
handle TRANS s => (warning ("Blast_tac: " ^ s); Seq.empty);

fun Blast_tac i = blast_tac (Data.claset()) i;

(*** For debugging: these apply the prover to a subgoal and return
the resulting tactics, trace, etc.                            ***)

(*Translate subgoal i from a proof state*)
fun trygl cs lim i =
(initialize();
let val st = topthm()
val {sign,...} = rep_thm st
val skoprem = fromSubgoal (List.nth(prems_of st, i-1))
val hyps  = strip_imp_prems skoprem
and concl = strip_imp_concl skoprem
in timeap prove (sign, startTiming(), cs,
[initBranch (mkGoal concl :: hyps, lim)], I)
end
handle Subscript => error("There is no subgoal " ^ Int.toString i));

fun Trygl lim i = trygl (Data.claset()) lim i;

(*Read a string to make an initial, singleton branch*)
term_of |> fromTerm |> rand |> mkGoal;

fun tryInThy thy lim s =
(initialize();
timeap prove (sign_of thy,
startTiming(),
Data.claset(),
[initBranch ([readGoal (sign_of thy) s], lim)],
I));

end;

```