# HG changeset patch # User paulson # Date 859972546 -7200 # Node ID f03b1652fc6a49ac69bd098ada4eec84d111aa30 # Parent f7e4109e17258f8e814fcbe05680b9f550e3369a Implementation of blast_tac: fast tableau prover diff -r f7e4109e1725 -r f03b1652fc6a src/Provers/blast.ML --- /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 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 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 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 (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; +