--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Provers/blast.ML Wed Apr 02 11:15:46 1997 +0200
@@ -0,0 +1,906 @@
+(* ID: $Id$
+use "/homes/lcp/Isa/new/blast.ML";
+ SKOLEMIZES ReplaceI WRONGLY: allow new vars in prems, or forbid such rules??
+ Needs explicit instantiation of assumptions? (#55 takes 32s)
+
+*)
+
+
+proof_timing:=true;
+print_depth 20;
+
+structure List = List_;
+
+(*Should be a type abbreviation?*)
+type netpair = (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net;
+
+
+(*Assumptions about constants:
+ --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 vars_gen_hyp_subst_tac : bool -> int -> tactic
+ val claset : claset ref
+ 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
+ val depth_tac : claset -> int -> int -> tactic
+ val blast_tac : claset -> int -> tactic
+ val Blast_tac : int -> tactic
+ end;
+
+
+functor BlastFun(Data: BLAST_DATA): BLAST =
+struct
+
+type claset = Data.claset;
+
+val trace = ref false;
+
+datatype term =
+ Const of string
+ | OConst of string * int
+ | 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;
+
+
+exception DEST_EQ;
+
+ (*Take apart an equality (plain or overloaded). NO constant Trueprop*)
+ fun dest_eq (Const "op =" $ t $ u) = (t,u)
+ | dest_eq (OConst("op =",_) $ t $ u) = (t,u)
+ | dest_eq _ = raise DEST_EQ;
+
+(** 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 *)
+fun head_of (f$t) = head_of f
+ | head_of u = u;
+
+
+(** 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 **)
+
+(*Result is a symbol table, indexed by names of overloaded constants.
+ Each constant maps to a list of (pattern,Blast.Const) pairs.
+ Any Term.Const that matches a pattern gets replaced by the Blast.Const.
+*)
+fun addConsts (t as Term.Const(a,_), tab) =
+ (case Symtab.lookup (tab,a) of
+ None => tab (*ignore: not a constant that we are looking for*)
+ | Some patList =>
+ (case gen_assoc (op aconv) (patList, t) of
+ None => Symtab.update
+ ((a, (t, OConst (a, length patList)) :: patList),
+ tab)
+ | _ => tab))
+ | addConsts (Term.Abs(_,_,body), tab) = addConsts (body, tab)
+ | addConsts (Term.$ (t,u), tab) = addConsts (t, addConsts (u, tab))
+ | addConsts (_, tab) = tab (*ignore others*);
+
+
+fun addRules (rls,tab) = foldr addConsts (map (#prop o rep_thm) rls, tab);
+
+fun declConst (a,tab) = Symtab.update((a,[]), tab);
+
+(*maps the name of each overloaded constant to a list of archetypal constants,
+ which may be polymorphic.*)
+local
+val overLoadTab = ref (Symtab.null : (Term.term * term) list Symtab.table)
+ (*The alists in this table should only be increased*)
+in
+
+fun declConsts (names, rls) =
+ overLoadTab := addRules (rls, foldr declConst (names, !overLoadTab));
+
+
+(*Convert a possibly overloaded Term.Const to a Blast.Const*)
+fun fromConst tsig (t as Term.Const (a,_)) =
+ let fun find [] = Const a
+ | find ((pat,t')::patList) =
+ if Pattern.matches tsig (pat,t) then t'
+ else find patList
+ in case Symtab.lookup(!overLoadTab, a) of
+ None => Const a
+ | Some patList => find patList
+ end;
+end;
+
+
+(*Tests whether 2 terms are alpha-convertible; chases instantiations*)
+fun (Const a) aconv (Const b) = a=b
+ | (OConst ai) aconv (OConst bj) = ai=bj
+ | (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*)
+fun add_term_vars (Skolem(a,args), vars) = add_vars_vars(args,vars)
+ | add_term_vars (Var (v as ref None), vars) = ins_var (v, vars)
+ | add_term_vars (Var (ref (Some u)), vars) = add_term_vars(u,vars)
+ | add_term_vars (Abs (_,body), vars) = add_term_vars(body,vars)
+ | add_term_vars (f$t, vars) = add_term_vars (f, add_term_vars(t, vars))
+ | add_term_vars (_, vars) = vars
+(*Term list version. [The fold functionals are slow]*)
+and add_terms_vars ([], vars) = vars
+ | add_terms_vars (t::ts, vars) = add_terms_vars (ts, add_term_vars(t,vars))
+(*Var list version.*)
+and add_vars_vars ([], vars) = vars
+ | add_vars_vars (ref (Some u) :: vs, vars) =
+ add_vars_vars (vs, add_term_vars(u,vars))
+ | add_vars_vars (v::vs, vars) = (*v must be a ref None*)
+ add_vars_vars (vs, ins_var (v, vars));
+
+
+(*Chase assignments in "vars"; return a list of unassigned variables*)
+fun vars_in_vars vars = add_vars_vars(vars,[]);
+
+
+
+(*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 (Abs (_,t), lev, js) = add_loose_bnos (t, lev+1, js)
+ | add_loose_bnos (f$t, lev, js) =
+ add_loose_bnos (f, lev, add_loose_bnos (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)
+ | (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)
+ | _ => t
+and wkNorm t = case head_of t of
+ Const _ => t
+ | OConst _ => 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 (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)
+ | (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) handle UNIFY => (clearTo n; raise UNIFY)
+ end;
+
+
+(*Convert from "real" terms to prototerms; eta-contract*)
+fun fromTerm tsig t =
+ let val alist = ref []
+ fun from (t as Term.Const _) = fromConst tsig t
+ | from (Term.Free (a,_)) = Free a
+ | from (Term.Bound i) = Bound i
+ | from (Term.Var (ixn,T)) =
+ (case (assoc_string_int(!alist,ixn)) of
+ None => let val t' = Var(ref None)
+ in alist := (ixn, (t', T)) :: !alist; 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;
+
+(* 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 |> Sequence.hd;
+
+
+(*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_subgoals_tac [] i st = Sequence.single st
+ | rot_subgoals_tac (k::ks) i st =
+ rot_subgoals_tac ks (i+1) (Sequence.hd (rotate_tac (~k) i st))
+ handle OPTION _ => Sequence.null;
+
+fun TRACE rl tac st = if !trace then (prth rl; tac st) else tac st;
+
+(*Tableau rule from elimination rule. Flag "dup" requests duplication of the
+ affected formula.*)
+fun fromRule vars rl =
+ let val {tsig,...} = Sign.rep_sg (#sign (rep_thm rl))
+ val trl = rl |> rep_thm |> #prop |> fromTerm tsig |> convertRule vars
+ fun tac dup i =
+ TRACE rl
+ (DETERM (etac (if dup then rev_dup_elim rl else rl) i))
+ THEN rot_subgoals_tac (map nNewHyps (#2 trl)) i
+
+ in General.SOME (trl, tac) end
+ handle Bind => General.NONE (*reject: conclusion is not just a variable*);
+
+
+(*** Conversion of Introduction Rules (needed for efficiency in
+ proof reconstruction) ***)
+
+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 {tsig,...} = Sign.rep_sg (#sign (rep_thm rl))
+ val trl = rl |> rep_thm |> #prop |> fromTerm tsig |> convertIntrRule vars
+ fun tac dup i =
+ TRACE rl (DETERM (rtac (if dup then Data.dup_intr rl else rl) i))
+ THEN rot_subgoals_tac (map nNewHyps (#2 trl)) i
+ in (trl, tac) end;
+
+
+val dummyVar = Term.Var (("Doom",666), dummyT);
+
+(*Convert from prototerms to ordinary terms with dummy types
+ Ignore abstractions; identify all Vars*)
+fun dummyTerm 0 _ = dummyVar
+ | dummyTerm d (Const a) = Term.Const (a,dummyT)
+ | dummyTerm d (OConst(a,_)) = Term.Const (a,dummyT)
+ | dummyTerm d (Skolem(a,_)) = Term.Const (a,dummyT)
+ | dummyTerm d (Free a) = Term.Free (a,dummyT)
+ | dummyTerm d (Bound i) = Term.Bound i
+ | dummyTerm d (Var _) = dummyVar
+ | dummyTerm d (Abs(a,_)) = dummyVar
+ | dummyTerm d (f $ u) = Term.$ (dummyTerm d f, dummyTerm (d-1) u);
+
+
+fun netMkRules P vars (nps: netpair list) =
+ case P of
+ (Const "*Goal*" $ G) =>
+ let val pG = mk_tprop (dummyTerm 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 (dummyTerm 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;
+**)
+
+(*** 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 *)
+
+(*Does t occur in u? For substitution.
+ Does NOT check args of Skolem terms: substitution does not affect them.
+ NOT reflexive since hyp_subst_tac fails on x=x.*)
+fun substOccur t =
+ let fun occEq u = (t aconv u) orelse occ u
+ and occ (Var(ref None)) = false
+ | occ (Var(ref(Some u))) = occEq u
+ | occ (Abs(_,u)) = occEq u
+ | occ (f$u) = occEq u orelse occEq f
+ | occ (_) = false;
+ in occEq end;
+
+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 (eta_contract_atom t, eta_contract_atom 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;
+
+
+(*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, md) = (negate G, md)
+ | negOfGoal G = G;
+
+(*Substitute through the branch if an equality goal (else raise DEST_EQ)*)
+fun equalSubst (G, br, hazs, lits, vars, lim) =
+ let val subst = subst_atomic (orientGoal(dest_eq G))
+ fun subst2(G,md) = (subst G, md)
+ fun subLits ([], br, nlits) =
+ (br, map (map subst2) hazs, nlits, vars, lim)
+ | subLits (lit::lits, br, nlits) =
+ let val nlit = subst lit
+ in if nlit aconv lit then subLits (lits, br, nlit::nlits)
+ else subLits (lits, (nlit,true)::br, nlits)
+ end
+ in subLits (rev lits, map subst2 br, [])
+ end;
+
+
+exception NEWBRANCHES and CLOSEF;
+
+type branch = (term*bool) list * (*pending formulae with md flags*)
+ (term*bool) list list * (*stack of haz formulae*)
+ term list * (*literals: irreducible formulae*)
+ term option ref list * (*variables occurring in branch*)
+ int; (*resource limit*)
+
+val fullTrace = ref[] : branch list list ref;
+
+exception PROVE;
+
+val eq_contr_tac = eresolve_tac [Data.notE] THEN' eq_assume_tac;
+
+val eContr_tac = TRACE Data.notE (eq_contr_tac ORELSE' Data.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) = (unify([],G,L); eAssume_tac)
+ | tryClose (G, Const"*Goal*" $ L) = (unify([],G,L); eAssume_tac)
+ | tryClose (Const"Not" $ G, L) = (unify([],G,L); eContr_tac)
+ | tryClose (G, Const"Not" $ L) = (unify([],G,L); eContr_tac)
+ | tryClose _ = raise UNIFY;
+
+
+(*hazs is a list of lists of unsafe formulae. This "stack" keeps them
+ in the right relative order: they must go after *all* safe formulae,
+ with newly introduced ones coming before older ones.*)
+
+(*Add an empty "stack frame" unless there's already one there*)
+fun nilHaz hazs =
+ case hazs of []::_ => hazs
+ | _ => []::hazs;
+
+fun addHaz (G, haz::hazs) = (haz@[negOfGoal G]) :: hazs;
+
+(*Convert *Goal* to negated assumption in FIRST position*)
+val negOfGoal_tac = rtac Data.ccontr THEN' rotate_tac ~1;
+
+(*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;
+
+(*Join new formulae to a branch.*)
+fun appendBr md (ts,us) =
+ if (exists isGoal ts) then joinMd md ts @ map negOfGoal us
+ else joinMd md ts @ us;
+
+(** 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
+ backtracking over bad proofs*)
+ | 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, ch' as (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, hazs, lits, vars, lim) :: _) = map Var vars
+ | nextVars [] = [];
+
+fun backtrack ((_, _, exn)::_) = raise exn
+ | backtrack _ = raise PROVE;
+
+(*Change all *Goal* literals to Not. Also delete all those identical to G.*)
+fun addLit (Const "*Goal*" $ G,lits) =
+ let fun bad (Const"*Goal*" $ _) = true
+ | bad (Const"Not" $ G') = G aconv G'
+ | bad _ = false;
+ 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)
+
+
+(*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.*)
+fun prove (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, []) = (cont (trs,choices,tacs))
+ | prv (tacs, trs, choices,
+ brs0 as ((G,md)::br, hazs, lits, vars, lim) :: brs) =
+ let exception PRV (*backtrack to precisely this recursion!*)
+ val ntrl = !ntrail
+ val nbrs = length brs0
+ val nxtVars = nextVars brs
+ val G = norm G
+ (*Make a new branch, decrementing "lim" if instantiations occur*)
+ fun newBr vars prems =
+ map (fn prem => (appendBr md (prem, br),
+ nilHaz hazs, lits,
+ add_terms_vars (prem,vars),
+ if ntrl < !ntrail then lim-3 else lim))
+ prems @
+ brs
+ (*Seek a matching rule. If unifiable then add new premises
+ to branch.*)
+ fun deeper [] = raise NEWBRANCHES
+ | deeper (((P,prems),tac)::grls) =
+ let val dummy = unify(add_term_vars(P,[]), P, G)
+ (*P comes from the rule; G comes from the branch.*)
+ val ntrl' = !ntrail
+ val choices' = (ntrl, nbrs, PRV) :: choices
+ in
+ if null prems then (*closed the branch: prune!*)
+ prv(tac false :: tacs, (*no duplication*)
+ brs0::trs,
+ prune (nbrs, nxtVars, choices'),
+ brs)
+ handle PRV =>
+ (*reset Vars and try another rule*)
+ (clearTo ntrl; deeper grls)
+ else
+ prv(tac false :: tacs, (*no duplication*)
+ brs0::trs, choices',
+ newBr (vars_in_vars vars) prems)
+ handle PRV =>
+ if ntrl < ntrl' then
+ (*Vars have been updated: must backtrack
+ even if not mentioned in other goals!
+ Reset Vars and try another rule*)
+ (clearTo ntrl; deeper grls)
+ else (*backtrack to previous level*)
+ backtrack choices
+ end
+ handle UNIFY => deeper grls
+ (*Try to close branch by unifying with head goal*)
+ fun closeF [] = raise CLOSEF
+ | closeF (L::Ls) =
+ let val tacs' = tryClose(G,L)::tacs
+ val choices' = prune (nbrs, nxtVars,
+ (ntrl, nbrs, PRV) :: choices)
+ in prv (tacs', brs0::trs, choices', brs)
+ handle PRV =>
+ (*reset Vars and try another literal
+ [this handler is pruned if possible!]*)
+ (clearTo ntrl; closeF Ls)
+ end
+ handle UNIFY => closeF Ls
+ in if !trace then fullTrace := brs0 :: !fullTrace else ();
+ if lim<0 then backtrack choices
+ else
+ prv (Data.vars_gen_hyp_subst_tac false :: tacs,
+ brs0::trs, choices,
+ equalSubst (G, br, hazs, lits, vars, lim) :: brs)
+ handle DEST_EQ => closeF lits
+ handle CLOSEF => closeF (map #1 br)
+ handle CLOSEF => closeF (map #1 (List.concat hazs))
+ handle CLOSEF =>
+ (deeper (netMkRules G vars safeList)
+ handle NEWBRANCHES =>
+ (case netMkRules G vars hazList of
+ [] => (*no plausible rules: move G to literals*)
+ prv (tacs, trs, choices,
+ (br, hazs, addLit(G,lits), vars, lim)::brs)
+ | _ => (*G admits some haz rules: try later*)
+ prv (if isGoal G then negOfGoal_tac :: tacs
+ else tacs,
+ trs, choices,
+ (br, addHaz((G,md),hazs), lits, vars, lim)
+ ::brs)))
+ end
+ | prv (tacs, trs, choices, ([], []::hazs, lits, vars, lim) :: brs) =
+ (*removal of empty list from hazs*)
+ prv (tacs, trs, choices, ([], hazs, lits, vars, lim) :: brs)
+ | prv (tacs, trs, choices,
+ brs0 as ([], ((G,md)::Gs)::hazs, lits, vars, lim) :: brs) =
+ (*application of haz rule*)
+ let exception PRV (*backtrack to precisely this recursion!*)
+ val G = norm G
+ val ntrl = !ntrail
+ fun newPrem (vars,dup) prem =
+ (map (fn P => (P,false)) prem,
+ nilHaz (if dup then Gs :: hazs @ [[negOfGoal (G,md)]]
+ else Gs :: hazs),
+ lits,
+ vars,
+ (*Decrement "lim" if instantiations occur or the
+ formula is duplicated*)
+ if ntrl < !ntrail then lim-3
+ else if dup then lim-1 else lim)
+ 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) =
+ let val dummy = unify(add_term_vars(P,[]), P, G)
+ val ntrl' = !ntrail
+ val vars = vars_in_vars vars
+ val vars' = foldr add_terms_vars (prems, vars)
+ val dup = md andalso vars' <> vars
+ (*duplicate G only if md and the premise has new vars*)
+ in
+ prv(tac dup :: tacs,
+ brs0::trs,
+ (ntrl, length brs0, PRV) :: choices,
+ newBr (vars', dup) prems)
+ handle PRV =>
+ if ntrl < ntrl' (*variables updated?*)
+ orelse vars=vars' (*pseudo-unsafe: no new Vars?*)
+ then (*reset Vars and try another rule*)
+ (clearTo ntrl; deeper grls)
+ else (*backtrack to previous level*)
+ backtrack choices
+ end
+ handle UNIFY => deeper grls
+ in if !trace then fullTrace := brs0 :: !fullTrace else ();
+ if lim<1 then backtrack choices
+ else
+ deeper (netMkRules G vars hazList)
+ handle NEWBRANCHES =>
+ (*cannot close branch: move G to literals*)
+ prv (tacs, brs0::trs, choices,
+ ([], Gs::hazs, G::lits, vars, lim)::brs)
+ end
+ | prv (tacs, trs, choices, _ :: brs) = backtrack choices
+ in prv ([], [], [(!ntrail, length brs, PROVE)], brs) end;
+
+
+fun initBranch (ts,lim) =
+ (map (fn t => (t,true)) ts,
+ [[]], [], add_terms_vars (ts,[]), lim);
+
+
+(*** Conversion & Skolemization of the Isabelle proof state ***)
+
+(*Make a list of all the parameters in a subgoal, even if nested*)
+local open Term
+in
+fun discard_foralls (Const("all",_)$Abs(a,T,t)) = discard_foralls t
+ | discard_foralls t = t;
+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;
+
+
+(*Conversion of a subgoal: Skolemize all parameters*)
+fun fromSubgoal tsig t =
+ let val alist = 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 error"Function Var's argument not a parameter"
+ else i-lev :: bounds ts
+ | bounds ts = error"Function Var's argument not a bound variable"
+ in
+ case ht of
+ t as Term.Const _ => apply (fromConst tsig t)
+ | Term.Free (a,_) => apply (Free a)
+ | Term.Bound i => apply (Bound i)
+ | Term.Var (ix,_) =>
+ (case (assoc_string_int(!alist,ix)) of
+ None => (alist := (ix, (ref None, bounds ts))
+ :: !alist;
+ Var (hdvar(!alist)))
+ | Some(v,is) => if is=bounds ts then Var v
+ else error("Discrepancy among occurrences of ?"
+ ^ Syntax.string_of_vname ix))
+ | Term.Abs (a,_,body) =>
+ if null ts then Abs(a, from (lev+1) body)
+ else error "fromSubgoal: 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 "SG_", getVars (!alist) i),
+ t))
+ else t
+
+ in skoSubgoal 0 (from 0 (discard_foralls t)) end;
+
+
+(*Tactic using tableau engine and proof reconstruction.
+ "lim" is depth limit.*)
+fun depth_tac cs lim i st =
+ (fullTrace:=[]; trail := []; ntrail := 0;
+ let val {tsig,...} = Sign.rep_sg (#sign (rep_thm st))
+ val skoprem = fromSubgoal tsig (List.nth(prems_of st, i-1))
+ val hyps = strip_imp_prems skoprem
+ and concl = strip_imp_concl skoprem
+ fun cont (_,choices,tacs) =
+ (case Sequence.pull(EVERY' (rev tacs) i st) of
+ None => (writeln ("PROOF FAILED for depth " ^
+ Int.toString lim);
+ backtrack choices)
+ | cell => Sequence.seqof(fn()=> cell))
+ in prove (cs, [initBranch (mkGoal concl :: hyps, lim)], cont)
+ end
+ handle Subscript => Sequence.null
+ | PROVE => Sequence.null);
+
+fun blast_tac cs = (DEEPEN (1,20) (depth_tac cs) 0);
+
+fun Blast_tac i = blast_tac (!Data.claset) i;
+
+end;
+