(* Title: Provers/blast
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
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 addss, addbefore, addafter; this restriction is intrinsic
* 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" rules such as transitivity can exclude other unsafe formulae
from expansion. This happens because newly-created formulae always
have priority over existing ones.
With overloading:
Overloading can't follow all chains of type dependencies. Cannot
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):
1. Sometimes hyp_subst_tac will fail due to occurrence of the parameter
as the argument of a function variable
2. 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;
(*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
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
| $ of term*term;
type branch
val depth_tac : claset -> int -> int -> tactic
val blast_tac : claset -> int -> tactic
val Blast_tac : int -> tactic
val declConsts : string list * thm list -> unit
(*debugging tools*)
val trace : bool ref
val fullTrace : branch list list ref
val fromTerm : Type.type_sig -> Term.term -> term
val fromSubgoal : Type.type_sig -> Term.term -> term
val toTerm : int -> term -> Term.term
val readGoal : Sign.sg -> string -> term
val tryInThy : theory -> int -> string ->
branch list list * (int*int*exn) list * (int -> tactic) list
val trygl : claset -> int -> int ->
branch list list * (int*int*exn) list * (int -> tactic) list
val Trygl : int -> int ->
branch list list * (int*int*exn) list * (int -> tactic) list
val normBr : branch -> branch
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) =
case Symtab.lookup (tab,a) of
None => Symtab.update((a,[]), tab) (*create a brand new entry*)
| Some _ => tab (*preserve old entry*);
(*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)
| 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
| 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(allowClash,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)
| (Const a, OConst(b,_)) => if allowClash andalso a=b then ()
else raise UNIFY
| (OConst(a,_), Const b) => if allowClash andalso a=b then ()
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) 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 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 {tsig,...} = Sign.rep_sg (#sign (rep_thm rl))
val trl = rl |> rep_thm |> #prop |> fromTerm tsig |> convertRule vars
fun tac dup i =
TRACE rl (etac (if dup then rev_dup_elim rl else rl)) i
THEN rot_subgoals_tac (map nNewHyps (#2 trl)) i
in SOME (trl, tac) end
handle Bind => (*reject: conclusion is not just a variable*)
(if !trace then (writeln"Warning: ignoring ill-formed elimination rule";
print_thm rl)
else ();
NONE);
(*** 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 o (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 (("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 (OConst(a,_)) = Term.Const (a,dummyT)
| 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;
**)
(*** 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;
(*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 (G, pairs, lits, vars, lim) =
let val subst = subst_atomic (orientGoal(dest_eq G))
fun subst2(G,md) = (subst G, md)
(*substitute throughout Haz list; move affected ones to Safe part*)
fun subHazs ([], Gs, nHs) = (Gs,nHs)
| subHazs ((H,md)::Hs, Gs, nHs) =
let val nH = subst H
in if nH aconv H then subHazs (Hs, Gs, (H,md)::nHs)
else subHazs (Hs, (nH,md)::Gs, nHs)
end
val pairs' = map (fn(Gs,Hs) => subHazs(rev Hs, map subst2 Gs, [])) pairs
(*substitute throughout literals; move affected ones to Safe part*)
fun subLits ([], [], nlits) = (pairs', nlits, vars, lim)
| subLits ([], Gs, nlits) = ((Gs,[])::pairs', nlits, vars, lim)
| subLits (lit::lits, Gs, nlits) =
let val nlit = subst lit
in if nlit aconv lit then subLits (lits, Gs, nlit::nlits)
else subLits (lits, (nlit,true)::Gs, nlits)
end
in subLits (rev lits, [], [])
end;
exception NEWBRANCHES and CLOSEF;
(*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*)
local
fun norm2 (G,md) = (norm G, md);
fun normLev (Gs,Hs) = (map norm2 Gs, map norm2 Hs);
in
fun normBr (br, lits, vars, lim) =
(map normLev br, map norm lits, vars, lim);
(*Convert from prototerms to ordinary terms with dummy types for tracing*)
fun showTerm 0 _ = dummyVar
| showTerm d (Const a) = Term.Const (a,dummyT)
| showTerm d (OConst(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 _) = dummyVar
| showTerm d (Abs(a,t)) = Term.Abs(a, dummyT, showTerm (d-1) t)
| showTerm d (f $ u) = Term.$ (showTerm d f, showTerm (d-1) u);
fun tracing sign brs =
let fun pr t = prs (Sign.string_of_term sign (showTerm 5 t))
fun printPairs (((G,_)::_,_)::_) = pr G
| printPairs (([],(H,_)::_)::_) = (prs"Haz: "; pr H)
| 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;
end;
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(true,[],G,L); eAssume_tac)
| tryClose (G, Const"*Goal*" $ L) = (unify(true,[],G,L); eAssume_tac)
| tryClose (Const"Not" $ G, L) = (unify(true,[],G,L); eContr_tac)
| tryClose (G, Const"Not" $ L) = (unify(true,[],G,L); eContr_tac)
| tryClose _ = raise UNIFY;
(*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*)
val negOfGoal_tac = rtac Data.ccontr THEN' rotate_tac ~1;
(** 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, lits, vars, lim) :: _) = map Var vars
| nextVars [] = [];
fun backtrack ((_, _, exn)::_) = 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'
| 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)
(*For calculating the "penalty" to assess on a branching factor of n
log2 seems a little too severe*)
fun log4 n = if n<4 then 0 else 1 + log4(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 (OConst ai) (OConst bj) = (ai=bj)
| 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;
(*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 (sign, 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, haz)::pairs, 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
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) =
let val dummy = unify(false, add_term_vars(P,[]), P, G)
(*P comes from the rule; G comes from the branch.*)
val ntrl' = !ntrail
val lim' = if ntrl < !ntrail
then lim - (1+log4(length rules))
else lim (*discourage branching updates*)
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)) :: tacs
(*no duplication*)
in
if null prems then (*closed the branch: prune!*)
prv(tacs', brs0::trs,
prune (nbrs, nxtVars, choices'),
brs)
handle PRV => (*reset Vars and try another rule*)
(clearTo ntrl; deeper grls)
else
if lim'<0 (*it's faster to kill ALL the alternatives*)
then raise NEWBRANCHES
else
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
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
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 backtrack choices
else
prv (Data.vars_gen_hyp_subst_tac false :: tacs,
brs0::trs, choices,
equalSubst (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
[] => (*no plausible rules: move G to literals*)
prv (tacs, brs0::trs, choices,
((br,haz)::pairs, addLit(G,lits), vars, lim)
::brs)
| _ => (*G admits some haz rules: try later*)
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,recur,dup,lim') prem =
let val Gs' = map (fn P => (P,false)) prem
and Hs' = if dup then Hs @ [(negOfGoal H, md)] else Hs
in (if recur then [(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) =
let val dummy = unify(false, add_term_vars(P,[]), P, H)
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+log4(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 = 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
else DETERM o (tac dup)
in
if lim'<0 andalso not (null prems)
then (*it's faster to kill ALL the alternatives*)
raise NEWBRANCHES
else
prv(tac dup :: tacs,
brs0::trs,
(ntrl, length brs0, PRV) :: choices,
newBr (vars', recur, 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
handle UNIFY => deeper grls
in tracing sign brs0;
if lim<1 then 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 prv ([], [], [(!ntrail, length brs, PROVE)], brs) end;
(*Construct an initial branch.*)
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 {sign,...} = rep_thm st
val {tsig,...} = Sign.rep_sg sign
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 (sign, 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;
(*** 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 =
(fullTrace:=[]; trail := []; ntrail := 0;
let val st = topthm()
val {sign,...} = rep_thm st
val {tsig,...} = Sign.rep_sg sign
val skoprem = fromSubgoal tsig (List.nth(prems_of st, i-1))
val hyps = strip_imp_prems skoprem
and concl = strip_imp_concl skoprem
in timeap prove
(sign, 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*)
fun readGoal sign s = read_cterm sign (s,propT) |>
term_of |> fromTerm (#tsig(Sign.rep_sg sign)) |>
rand |> mkGoal;
fun tryInThy thy lim s =
(fullTrace:=[]; trail := []; ntrail := 0;
timeap prove (sign_of thy,
!Data.claset,
[initBranch ([readGoal (sign_of thy) s], lim)],
I));
end;