--- a/src/Provers/blast.ML Fri Dec 30 16:56:58 2005 +0100
+++ b/src/Provers/blast.ML Fri Dec 30 16:56:59 2005 +0100
@@ -1,6 +1,6 @@
-(* Title: Provers/blast.ML
+(* Title: Provers/blast.ML
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1997 University of Cambridge
Generic tableau prover with proof reconstruction
@@ -14,21 +14,20 @@
Blast_tac is often more powerful than fast_tac, but has some limitations.
Blast_tac...
- * ignores wrappers (addss, addbefore, addafter, addWrapper, ...);
+ * ignores wrappers (addss, addbefore, addafter, addWrapper, ...);
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
+ (conclusion must be a formula variable)
* rules must not require higher-order unification, e.g. apply_type in ZF
+ message "Function Var's argument not a bound variable" relates to this
* its proof strategy is more general but can actually be slower
Known problems:
"Recursive" chains of rules can sometimes exclude other unsafe formulae
- from expansion. This happens because newly-created formulae always
- have priority over existing ones. But obviously recursive rules
- such as transitivity are treated specially to prevent this. Sometimes
- the formulae get into the wrong order (see WRONG below).
+ from expansion. This happens because newly-created formulae always
+ have priority over existing ones. But obviously recursive rules
+ such as transitivity are treated specially to prevent this. Sometimes
+ the formulae get into the wrong order (see WRONG below).
With substition for equalities (hyp_subst_tac):
When substitution affects a haz formula or literal, it is moved
@@ -40,28 +39,24 @@
(*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 ="
- --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 equality_name: string
+ val not_name: string
+ val notE : thm (* [| ~P; P |] ==> R *)
+ val ccontr : thm
+ val contr_tac : int -> tactic
+ val dup_intr : thm -> thm
val hyp_subst_tac : bool ref -> int -> tactic
- val claset : unit -> claset
- val rep_cs : (* dependent on classical.ML *)
- claset -> {safeIs: thm list, safeEs: thm list,
- hazIs: thm list, hazEs: thm list,
- swrappers: (string * wrapper) list,
- uwrappers: (string * wrapper) list,
- safe0_netpair: netpair, safep_netpair: netpair,
- haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: ContextRules.netpair}
+ val claset : unit -> claset
+ val rep_cs : (* dependent on classical.ML *)
+ claset -> {safeIs: thm list, safeEs: thm list,
+ hazIs: thm list, hazEs: thm list,
+ swrappers: (string * wrapper) list,
+ uwrappers: (string * wrapper) list,
+ safe0_netpair: netpair, safep_netpair: netpair,
+ haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: ContextRules.netpair}
val cla_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
end;
@@ -69,9 +64,9 @@
signature BLAST =
sig
- type claset
+ type claset
exception TRANS of string (*reports translation errors*)
- datatype term =
+ datatype term =
Const of string * term list
| Skolem of string * term option ref list
| Free of string
@@ -80,32 +75,32 @@
| Abs of string*term
| $ of term*term;
type branch
- val depth_tac : claset -> int -> int -> tactic
+ val depth_tac : claset -> int -> int -> tactic
val depth_limit : int ref
- val blast_tac : claset -> int -> tactic
- val Blast_tac : int -> tactic
- val setup : (theory -> theory) list
+ val blast_tac : claset -> int -> tactic
+ val Blast_tac : int -> tactic
+ val setup : (theory -> theory) list
(*debugging tools*)
- val stats : bool ref
- val trace : bool ref
- val fullTrace : branch list list ref
- val fromType : (indexname * term) list ref -> Term.typ -> term
- val fromTerm : Term.term -> term
+ val stats : bool ref
+ val trace : bool ref
+ val fullTrace : branch list list ref
+ val fromType : (indexname * term) list ref -> Term.typ -> term
+ val fromTerm : Term.term -> term
val fromSubgoal : Term.term -> term
val instVars : term -> (unit -> unit)
- val toTerm : int -> term -> Term.term
- val readGoal : Sign.sg -> string -> term
- val tryInThy : theory -> int -> string ->
- (int->tactic) list * branch list list * (int*int*exn) list
- val trygl : claset -> int -> int ->
- (int->tactic) list * branch list list * (int*int*exn) list
- val Trygl : int -> int ->
+ val toTerm : int -> term -> Term.term
+ val readGoal : theory -> string -> term
+ val tryInThy : theory -> int -> string ->
(int->tactic) list * branch list list * (int*int*exn) list
- val normBr : branch -> branch
+ val trygl : claset -> int -> int ->
+ (int->tactic) list * branch list list * (int*int*exn) list
+ val Trygl : int -> int ->
+ (int->tactic) list * branch list list * (int*int*exn) list
+ val normBr : branch -> branch
end;
-functor BlastFun(Data: BLAST_DATA) : BLAST =
+functor BlastFun(Data: BLAST_DATA) : BLAST =
struct
type claset = Data.claset;
@@ -113,7 +108,7 @@
val trace = ref false
and stats = ref false; (*for runtime and search statistics*)
-datatype term =
+datatype term =
Const of string * term list (*typargs constant--as a terms!*)
| Skolem of string * term option ref list
| Free of string
@@ -136,9 +131,9 @@
val list_comb : term * term list -> term = Library.foldl (op $);
(* maps f(t1,...,tn) to (f, [t1,...,tn]) ; naturally tail-recursive*)
-fun strip_comb u : term * term list =
+fun strip_comb u : term * term list =
let fun stripc (f$t, ts) = stripc (f, t::ts)
- | stripc x = x
+ | stripc x = x
in stripc(u,[]) end;
(* maps f(t1,...,tn) to f , which is never a combination *)
@@ -148,12 +143,15 @@
(** Particular constants **)
-fun negate P = Const ("Not", []) $ P;
+fun negate P = Const (Data.not_name, []) $ P;
+
+fun isNot (Const (c, _) $ _) = c = Data.not_name
+ | isNot _ = false;
fun mkGoal P = Const ("*Goal*", []) $ P;
fun isGoal (Const ("*Goal*", _) $ _) = true
- | isGoal _ = false;
+ | isGoal _ = false;
val TruepropC = ObjectLogic.judgment_name (the_context ());
val TruepropT = Sign.the_const_type (the_context ()) TruepropC;
@@ -172,11 +170,11 @@
fun fromType alist (Term.Type(a,Ts)) = list_comb (Const (a, []), map (fromType alist) Ts)
| fromType alist (Term.TFree(a,_)) = Free a
| fromType alist (Term.TVar (ixn,_)) =
- (case (AList.lookup (op =) (!alist) ixn) of
- NONE => let val t' = Var(ref NONE)
- in alist := (ixn, t') :: !alist; t'
- end
- | SOME v => v)
+ (case (AList.lookup (op =) (!alist) ixn) of
+ NONE => let val t' = Var(ref NONE)
+ in alist := (ixn, t') :: !alist; t'
+ end
+ | SOME v => v)
(*refer to the theory in which blast is initialized*)
val typargs = ref (fn ((_, T): string * typ) => [T]);
@@ -191,7 +189,7 @@
| (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*)
+ | (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)
@@ -215,22 +213,22 @@
(** 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)
+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 (Const (_,ts), vars) = add_terms_vars(ts,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
+ | add_term_vars (Const (_,ts), vars) = add_terms_vars(ts,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 (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));
+ add_vars_vars (vs, ins_var (v, vars));
(*Chase assignments in "vars"; return a list of unassigned variables*)
@@ -241,7 +239,7 @@
(*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
+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;
@@ -252,23 +250,23 @@
(*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
+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 (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 =
+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
+ 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;
@@ -287,18 +285,18 @@
(*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)
+ 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))
+ 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
@@ -307,15 +305,15 @@
| _ => wkNormAux t;
-(*Does variable v occur in u? For unification.
+(*Does variable v occur in u? For unification.
Dangling bound vars are also forbidden.*)
-fun varOccur v =
- let fun occL lev [] = false (*same as (exists occ), but faster*)
- | occL lev (u::us) = occ lev u orelse occL lev us
- and occ lev (Var w) =
- v=w orelse
+fun varOccur v =
+ let fun occL lev [] = false (*same as (exists occ), but faster*)
+ | occL lev (u::us) = occ lev u orelse occL lev us
+ and occ lev (Var w) =
+ v=w orelse
(case !w of NONE => false
- | SOME u => occ lev u)
+ | SOME u => occ lev u)
| occ lev (Skolem(_,args)) = occL lev (map Var args)
(*ignore Const, since term variables can't occur in types (?) *)
| occ lev (Bound i) = lev <= i
@@ -333,36 +331,36 @@
(*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);
+ (hd(!trail) := NONE;
+ trail := tl (!trail);
+ ntrail := !ntrail - 1);
-(*First-order unification with bound variables.
+(*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)
+ 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)
- | (Const(a,ats), Const(b,bts)) => if a=b then unifysAux(ats,bts)
- 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
+ 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,ats), Const(b,bts)) => if a=b then unifysAux(ats,bts)
+ 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
and unifysAux ([], []) = ()
| unifysAux (t :: ts, u :: us) = (unifyAux (t, u); unifysAux (ts, us))
| unifysAux _ = raise UNIFY;
@@ -376,21 +374,21 @@
let val alistVar = ref []
and alistTVar = ref []
fun from (Term.Const aT) = fromConst alistTVar aT
- | from (Term.Free (a,_)) = Free a
- | from (Term.Bound i) = Bound i
- | from (Term.Var (ixn,T)) =
- (case (AList.lookup (op =) (!alistVar) ixn) of
- NONE => let val t' = Var(ref NONE)
- in alistVar := (ixn, t') :: !alistVar; t'
- end
- | SOME v => v)
- | from (Term.Abs (a,_,u)) =
- (case from u of
- u' as (f $ Bound 0) =>
- if (0 mem_int loose_bnos f) then Abs(a,u')
- else incr_boundvars ~1 f
- | u' => Abs(a,u'))
- | from (Term.$ (f,u)) = from f $ from u
+ | from (Term.Free (a,_)) = Free a
+ | from (Term.Bound i) = Bound i
+ | from (Term.Var (ixn,T)) =
+ (case (AList.lookup (op =) (!alistVar) ixn) of
+ NONE => let val t' = Var(ref NONE)
+ in alistVar := (ixn, t') :: !alistVar; t'
+ end
+ | SOME v => v)
+ | from (Term.Abs (a,_,u)) =
+ (case from u of
+ u' as (f $ Bound 0) =>
+ if (0 mem_int loose_bnos f) then Abs(a,u')
+ else incr_boundvars ~1 f
+ | u' => Abs(a,u'))
+ | from (Term.$ (f,u)) = from f $ from u
in from t end;
(*A debugging function: replaces all Vars by dummy Frees for visual inspection
@@ -399,12 +397,12 @@
let val name = ref "a"
val updated = ref []
fun inst (Const(a,ts)) = List.app inst ts
- | inst (Var(v as ref NONE)) = (updated := v :: (!updated);
- v := SOME (Free ("?" ^ !name));
- name := Symbol.bump_string (!name))
- | inst (Abs(a,t)) = inst t
- | inst (f $ u) = (inst f; inst u)
- | inst _ = ()
+ | inst (Var(v as ref NONE)) = (updated := v :: (!updated);
+ v := SOME (Free ("?" ^ !name));
+ name := Symbol.bump_string (!name))
+ | inst (Abs(a,t)) = inst t
+ | inst (f $ u) = (inst f; inst u)
+ | inst _ = ()
fun revert() = List.app (fn v => v:=NONE) (!updated)
in inst t; revert end;
@@ -424,20 +422,21 @@
exception ElimBadConcl and ElimBadPrem;
(*The conclusion becomes the goal/negated assumption *False*: delete it!
- If we don't find it then the premise is ill-formed and could cause
+ If we don't find it then the premise is ill-formed and could cause
PROOF FAILED*)
fun delete_concl [] = raise ElimBadPrem
- | delete_concl (Const ("*Goal*", _) $ (Var (ref (SOME (Const ("*False*", _))))) :: Ps) =
- Ps
- | delete_concl (Const ("Not", _) $ (Var (ref (SOME (Const ("*False*", _))))) :: Ps) =
- Ps
- | delete_concl (P::Ps) = P :: delete_concl Ps;
+ | delete_concl (P :: Ps) =
+ (case P of
+ Const (c, _) $ Var (ref (SOME (Const ("*False*", _)))) =>
+ if c = "*Goal*" orelse c = Data.not_name then Ps
+ else P :: delete_concl Ps
+ | _ => P :: delete_concl Ps);
fun skoPrem vars (Const ("all", _) $ Abs (_, P)) =
skoPrem vars (subst_bound (Skolem (gensym "S_", vars), P))
| skoPrem vars P = P;
-fun convertPrem t =
+fun convertPrem t =
delete_concl (mkGoal (strip_imp_concl t) :: strip_imp_prems t);
(*Expects elimination rules to have a formula variable as conclusion*)
@@ -445,7 +444,7 @@
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)
+ (P, map (convertPrem o skoPrem vars) Ps)
end
handle Bind => raise ElimBadConcl;
@@ -466,7 +465,7 @@
| rot_tac (k::ks) i st = rot_tac ks (i+1) (rotate_rule (~k) i st);
in
fun rot_subgoals_tac (rot, rl) =
- rot_tac (if rot then map nNewHyps rl else [])
+ rot_tac (if rot then map nNewHyps rl else [])
end;
@@ -477,24 +476,24 @@
fun emtac upd rl = TRACE rl (if upd then etac rl else ematch_tac [rl]);
fun rmtac upd rl = TRACE rl (if upd then rtac rl else match_tac [rl]);
-(*Tableau rule from elimination rule.
+(*Tableau rule from elimination rule.
Flag "upd" says that the inference updated the branch.
Flag "dup" requests duplication of the affected formula.*)
-fun fromRule vars rl =
+fun fromRule vars rl =
let val trl = rl |> rep_thm |> #prop |> fromTerm |> convertRule vars
- fun tac (upd, dup,rot) i =
- emtac upd (if dup then rev_dup_elim rl else rl) i
- THEN
- rot_subgoals_tac (rot, #2 trl) i
+ fun tac (upd, dup,rot) i =
+ emtac upd (if dup then rev_dup_elim rl else rl) i
+ THEN
+ rot_subgoals_tac (rot, #2 trl) i
in Option.SOME (trl, tac) end
handle ElimBadPrem => (*reject: prems don't preserve conclusion*)
- (warning("Ignoring weak elimination rule\n" ^ string_of_thm rl);
- Option.NONE)
+ (warning("Ignoring weak elimination rule\n" ^ string_of_thm rl);
+ Option.NONE)
| ElimBadConcl => (*ignore: conclusion is not just a variable*)
- (if !trace then (warning("Ignoring ill-formed elimination rule:\n" ^
- "conclusion should be a variable\n" ^ string_of_thm rl))
- else ();
- Option.NONE);
+ (if !trace then (warning("Ignoring ill-formed elimination rule:\n" ^
+ "conclusion should be a variable\n" ^ string_of_thm rl))
+ else ();
+ Option.NONE);
(*** Conversion of Introduction Rules ***)
@@ -504,20 +503,20 @@
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)
+ in (mkGoal P, map (convertIntrPrem o skoPrem vars) Ps)
end;
-(*Tableau rule from introduction rule.
+(*Tableau rule from introduction rule.
Flag "upd" says that the inference updated the branch.
Flag "dup" requests duplication of the affected formula.
Since haz rules are now delayed, "dup" is always FALSE for
introduction rules.*)
-fun fromIntrRule vars rl =
+fun fromIntrRule vars rl =
let val trl = rl |> rep_thm |> #prop |> fromTerm |> convertIntrRule vars
- fun tac (upd,dup,rot) i =
- rmtac upd (if dup then Data.dup_intr rl else rl) i
- THEN
- rot_subgoals_tac (rot, #2 trl) i
+ fun tac (upd,dup,rot) i =
+ rmtac upd (if dup then Data.dup_intr rl else rl) i
+ THEN
+ rot_subgoals_tac (rot, #2 trl) i
in (trl, tac) end;
@@ -538,22 +537,22 @@
fun netMkRules P vars (nps: netpair list) =
case P of
(Const ("*Goal*", _) $ G) =>
- let val pG = mk_Trueprop (toTerm 2 G)
- val intrs = List.concat
- (map (fn (inet,_) => Net.unify_term inet pG)
- nps)
- in map (fromIntrRule vars o #2) (Tactic.orderlist intrs) end
+ let val pG = mk_Trueprop (toTerm 2 G)
+ val intrs = List.concat
+ (map (fn (inet,_) => Net.unify_term inet pG)
+ nps)
+ in map (fromIntrRule vars o #2) (Tactic.orderlist intrs) end
| _ =>
- let val pP = mk_Trueprop (toTerm 3 P)
- val elims = List.concat
- (map (fn (_,enet) => Net.unify_term enet pP)
- nps)
- in List.mapPartial (fromRule vars o #2) (Tactic.orderlist elims) end;
+ let val pP = mk_Trueprop (toTerm 3 P)
+ val elims = List.concat
+ (map (fn (_,enet) => Net.unify_term enet pP)
+ nps)
+ in List.mapPartial (fromRule vars o #2) (Tactic.orderlist elims) end;
(*Pending formulae carry md (may duplicate) flags*)
-type branch =
- {pairs: ((term*bool) list * (*safe formulae on this level*)
+type branch =
+ {pairs: ((term*bool) list * (*safe formulae on this level*)
(term*bool) list) list, (*haz formulae on this level*)
lits: term list, (*literals: irreducible formulae*)
vars: term option ref list, (*variables occurring in branch*)
@@ -567,9 +566,9 @@
fun normLev (Gs,Hs) = (map norm2 Gs, map norm2 Hs);
fun normBr {pairs, lits, vars, lim} =
- {pairs = map normLev pairs,
- lits = map norm lits,
- vars = vars,
+ {pairs = map normLev pairs,
+ lits = map norm lits,
+ vars = vars,
lim = lim};
@@ -581,8 +580,8 @@
| showType (Var _) = dummyTVar
| showType t =
(case strip_comb t of
- (Const (a, _), us) => Term.Type(a, map showType us)
- | _ => dummyT);
+ (Const (a, _), us) => Term.Type(a, map showType us)
+ | _ => dummyT);
(*Display top-level overloading if any*)
fun topType thy (Const (c, ts)) = SOME (Sign.const_instance thy (c, map showType ts))
@@ -599,33 +598,33 @@
| showTerm d (Var(ref(SOME u))) = showTerm d u
| showTerm d (Var(ref NONE)) = dummyVar2
| showTerm d (Abs(a,t)) = if d=0 then dummyVar
- else Term.Abs(a, dummyT, showTerm (d-1) t)
+ else Term.Abs(a, dummyT, showTerm (d-1) t)
| showTerm d (f $ u) = if d=0 then dummyVar
- else Term.$ (showTerm d f, showTerm (d-1) u);
+ else Term.$ (showTerm d f, showTerm (d-1) u);
fun string_of sign d t = Sign.string_of_term sign (showTerm d t);
-fun traceTerm sign t =
+fun traceTerm sign t =
let val t' = norm t
val stm = string_of sign 8 t'
- in
+ in
case topType sign t' of
- NONE => stm (*no type to attach*)
- | SOME T => stm ^ "\t:: " ^ Sign.string_of_typ sign T
+ NONE => stm (*no type to attach*)
+ | SOME T => stm ^ "\t:: " ^ Sign.string_of_typ sign T
end;
(*Print tracing information at each iteration of prover*)
-fun tracing sign brs =
+fun tracing sign brs =
let fun printPairs (((G,_)::_,_)::_) = immediate_output(traceTerm sign G)
- | printPairs (([],(H,_)::_)::_) = immediate_output(traceTerm sign H ^ "\t (Unsafe)")
- | printPairs _ = ()
+ | printPairs (([],(H,_)::_)::_) = immediate_output(traceTerm sign H ^ "\t (Unsafe)")
+ | printPairs _ = ()
fun printBrs (brs0 as {pairs, lits, lim, ...} :: brs) =
- (fullTrace := brs0 :: !fullTrace;
- List.app (fn _ => immediate_output "+") brs;
- immediate_output (" [" ^ Int.toString lim ^ "] ");
- printPairs pairs;
- writeln"")
+ (fullTrace := brs0 :: !fullTrace;
+ List.app (fn _ => immediate_output "+") brs;
+ immediate_output (" [" ^ Int.toString lim ^ "] ");
+ printPairs pairs;
+ writeln"")
in if !trace then printBrs (map normBr brs) else ()
end;
@@ -633,11 +632,11 @@
(*Tracing: variables updated in the last branch operation?*)
fun traceVars sign ntrl =
- if !trace then
+ if !trace then
(case !ntrail-ntrl of
- 0 => ()
- | 1 => immediate_output"\t1 variable UPDATED:"
- | n => immediate_output("\t" ^ Int.toString n ^ " variables UPDATED:");
+ 0 => ()
+ | 1 => immediate_output"\t1 variable UPDATED:"
+ | n => immediate_output("\t" ^ Int.toString n ^ " variables UPDATED:");
(*display the instantiations themselves, though no variable names*)
List.app (fn v => immediate_output(" " ^ string_of sign 4 (valOf (!v))))
(List.take(!trail, !ntrail-ntrl));
@@ -646,30 +645,30 @@
(*Tracing: how many new branches are created?*)
fun traceNew prems =
- if !trace then
+ if !trace then
case length prems of
- 0 => immediate_output"branch closed by rule"
- | 1 => immediate_output"branch extended (1 new subgoal)"
- | n => immediate_output("branch split: "^ Int.toString n ^ " new subgoals")
+ 0 => immediate_output"branch closed by rule"
+ | 1 => immediate_output"branch extended (1 new subgoal)"
+ | n => immediate_output("branch split: "^ Int.toString n ^ " new subgoals")
else ();
(*** Code for handling equality: naive substitution, like hyp_subst_tac ***)
-(*Replace the ATOMIC term "old" by "new" in t*)
+(*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
+ | 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)) =
+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)
+ else eta_contract_atom (incr_boundvars ~1 f)
| _ => t0)
| eta_contract_atom t = t
and eta_contract2 (f$t) = f $ eta_contract_atom t
@@ -683,21 +682,21 @@
Prefer to eliminate Bound variables if possible.
Result: true = use as is, false = reorient first *)
-(*Can t occur in u? For substitution.
+(*Can t occur in u? For substitution.
Does NOT examine the args of Skolem terms: substitution does not affect them.
REFLEXIVE because hyp_subst_tac fails on x=x.*)
-fun substOccur t =
- let (*NO vars are permitted in u except the arguments of t, if it is
+fun substOccur t =
+ let (*NO vars are permitted in u except the arguments of t, if it is
a Skolem term. This ensures that no equations are deleted that could
be instantiated to a cycle. For example, x=?a is rejected because ?a
- could be instantiated to Suc(x).*)
+ could be instantiated to Suc(x).*)
val vars = case t of
Skolem(_,vars) => vars
- | _ => []
+ | _ => []
fun occEq u = (t aconv u) orelse occ u
and occ (Var(ref(SOME u))) = occEq u
| occ (Var v) = not (mem_var (v, vars))
- | occ (Abs(_,u)) = occEq u
+ | occ (Abs(_,u)) = occEq u
| occ (f$u) = occEq u orelse occEq f
| occ (_) = false;
in occEq end;
@@ -705,54 +704,55 @@
exception DEST_EQ;
(*Take apart an equality. NO constant Trueprop*)
-fun dest_eq (Const ("op =", _) $ t $ u) =
- (eta_contract_atom t, eta_contract_atom u)
- | dest_eq _ = raise DEST_EQ;
+fun dest_eq (Const (c, _) $ t $ u) =
+ if c = Data.equality_name then (eta_contract_atom t, eta_contract_atom u)
+ else raise DEST_EQ
+ | dest_eq _ = raise DEST_EQ;
(*Reject the equality if u occurs in (or equals!) t*)
fun check (t,u,v) = if substOccur t u then raise DEST_EQ else v;
-(*IF the goal is an equality with a substitutable variable
+(*IF the goal is an equality with a substitutable variable
THEN orient that equality ELSE raise exception DEST_EQ*)
fun orientGoal (t,u) = case (t,u) of
- (Skolem _, _) => check(t,u,(t,u)) (*eliminates t*)
- | (_, Skolem _) => check(u,t,(u,t)) (*eliminates u*)
- | (Free _, _) => check(t,u,(t,u)) (*eliminates t*)
- | (_, Free _) => check(u,t,(u,t)) (*eliminates u*)
+ (Skolem _, _) => check(t,u,(t,u)) (*eliminates t*)
+ | (_, Skolem _) => check(u,t,(u,t)) (*eliminates u*)
+ | (Free _, _) => check(t,u,(t,u)) (*eliminates t*)
+ | (_, Free _) => check(u,t,(u,t)) (*eliminates u*)
| _ => raise DEST_EQ;
(*Substitute through the branch if an equality goal (else raise DEST_EQ).
Moves affected literals back into the branch, but it is not clear where
they should go: this could make proofs fail.*)
-fun equalSubst sign (G, {pairs, lits, vars, lim}) =
+fun equalSubst sign (G, {pairs, lits, vars, lim}) =
let val (t,u) = orientGoal(dest_eq G)
val subst = subst_atomic (t,u)
fun subst2(G,md) = (subst G, md)
(*substitute throughout list; extract affected formulae*)
fun subForm ((G,md), (changed, pairs)) =
- let val nG = subst G
- in if nG aconv G then (changed, (G,md)::pairs)
- else ((nG,md)::changed, pairs)
+ let val nG = subst G
+ in if nG aconv G then (changed, (G,md)::pairs)
+ else ((nG,md)::changed, pairs)
end
(*substitute throughout "stack frame"; extract affected formulae*)
fun subFrame ((Gs,Hs), (changed, frames)) =
- let val (changed', Gs') = foldr subForm (changed, []) Gs
+ let val (changed', Gs') = foldr subForm (changed, []) Gs
val (changed'', Hs') = foldr subForm (changed', []) Hs
in (changed'', (Gs',Hs')::frames) end
(*substitute throughout literals; extract affected ones*)
fun subLit (lit, (changed, nlits)) =
- let val nlit = subst lit
- in if nlit aconv lit then (changed, nlit::nlits)
- else ((nlit,true)::changed, nlits)
+ let val nlit = subst lit
+ in if nlit aconv lit then (changed, nlit::nlits)
+ else ((nlit,true)::changed, nlits)
end
val (changed, lits') = foldr subLit ([], []) lits
val (changed', pairs') = foldr subFrame (changed, []) pairs
in if !trace then writeln ("Substituting " ^ traceTerm sign u ^
- " for " ^ traceTerm sign t ^ " in branch" )
+ " for " ^ traceTerm sign t ^ " in branch" )
else ();
- {pairs = (changed',[])::pairs', (*affected formulas, and others*)
- lits = lits', (*unaffected literals*)
- vars = vars,
+ {pairs = (changed',[])::pairs', (*affected formulas, and others*)
+ lits = lits', (*unaffected literals*)
+ vars = vars,
lim = lim}
end;
@@ -762,27 +762,28 @@
exception PROVE;
(*Trying eq_contr_tac first INCREASES the effort, slowing reconstruction*)
-val contr_tac = ematch_tac [Data.notE] THEN'
+val contr_tac = ematch_tac [Data.notE] THEN'
(eq_assume_tac ORELSE' assume_tac);
val eContr_tac = TRACE Data.notE contr_tac;
val eAssume_tac = TRACE asm_rl (eq_assume_tac ORELSE' assume_tac);
-(*Try to unify complementary literals and return the corresponding tactic. *)
-fun tryClose (Const ("*Goal*", _) $ G, L) =
- if unify([],G,L) then SOME eAssume_tac else NONE
- | tryClose (G, Const ("*Goal*", _) $ L) =
- if unify([],G,L) then SOME eAssume_tac else NONE
- | tryClose (Const ("Not", _) $ G, L) =
- if unify([],G,L) then SOME eContr_tac else NONE
- | tryClose (G, Const ("Not", _) $ L) =
- if unify([],G,L) then SOME eContr_tac else NONE
- | tryClose _ = NONE;
-
+(*Try to unify complementary literals and return the corresponding tactic. *)
+fun tryClose (G, L) =
+ let
+ fun close t u tac = if unify ([], t, u) then SOME tac else NONE;
+ fun arg (_ $ t) = t;
+ in
+ if isGoal G then close (arg G) L eAssume_tac
+ else if isGoal L then close G (arg L) eAssume_tac
+ else if isNot G then close (arg G) L eContr_tac
+ else if isNot L then close G (arg L) eContr_tac
+ else NONE
+ end;
(*Were there Skolem terms in the premise? Must NOT chase Vars*)
fun hasSkolem (Skolem _) = true
- | hasSkolem (Abs (_,body)) = hasSkolem body
+ | hasSkolem (Abs (_,body)) = hasSkolem body
| hasSkolem (f$t) = hasSkolem f orelse hasSkolem t
| hasSkolem _ = false;
@@ -815,63 +816,64 @@
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)
+ | 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*)
+fun prune (1, nxtVars, choices) = choices (*DON'T prune at very end: allow
+ backtracking over bad proofs*)
| prune (nbrs: int, nxtVars, choices) =
let fun traceIt last =
- let val ll = length last
- and lc = length choices
- in if !trace andalso ll<lc then
- (writeln("Pruning " ^ Int.toString(lc-ll) ^ " levels");
- last)
- else last
- end
- fun pruneAux (last, _, _, []) = last
- | pruneAux (last, ntrl, trl, (ntrl',nbrs',exn) :: choices) =
- if nbrs' < nbrs
- then last (*don't backtrack beyond first solution of goal*)
- else if nbrs' > nbrs then pruneAux (last, ntrl, trl, choices)
- else (* nbrs'=nbrs *)
- if clashVar nxtVars (ntrl-ntrl', trl) then last
- else (*no clashes: can go back at least this far!*)
- pruneAux(choices, ntrl', List.drop(trl, ntrl-ntrl'),
- choices)
+ let val ll = length last
+ and lc = length choices
+ in if !trace andalso ll<lc then
+ (writeln("Pruning " ^ Int.toString(lc-ll) ^ " levels");
+ last)
+ else last
+ end
+ fun pruneAux (last, _, _, []) = last
+ | pruneAux (last, ntrl, trl, (ntrl',nbrs',exn) :: choices) =
+ if nbrs' < nbrs
+ then last (*don't backtrack beyond first solution of goal*)
+ else if nbrs' > nbrs then pruneAux (last, ntrl, trl, choices)
+ else (* nbrs'=nbrs *)
+ if clashVar nxtVars (ntrl-ntrl', trl) then last
+ else (*no clashes: can go back at least this far!*)
+ pruneAux(choices, ntrl', List.drop(trl, ntrl-ntrl'),
+ choices)
in traceIt (pruneAux (choices, !ntrail, !trail, choices)) end;
fun nextVars ({pairs, lits, vars, lim} :: _) = map Var vars
| nextVars [] = [];
-fun backtrack (choices as (ntrl, nbrs, exn)::_) =
- (if !trace then (writeln ("Backtracking; now there are " ^
- Int.toString nbrs ^ " branches"))
- else ();
+fun backtrack (choices as (ntrl, nbrs, exn)::_) =
+ (if !trace then (writeln ("Backtracking; now there are " ^
+ Int.toString nbrs ^ " branches"))
+ else ();
raise exn)
| backtrack _ = raise PROVE;
(*Add the literal G, handling *Goal* and detecting duplicates.*)
-fun addLit (Const ("*Goal*", _) $ G, lits) =
+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
+ | bad (Const (c, _) $ G') = c = Data.not_name andalso G aconv G'
+ | bad _ = false;
+ fun change [] = []
+ | change (lit :: lits) =
+ (case lit of
+ Const (c, _) $ G' =>
+ if c = "*Goal*" orelse c = Data.not_name then
+ if G aconv G' then change lits
+ else negate G' :: change lits
+ else lit :: change lits
+ | _ => lit :: change lits)
in
- Const ("*Goal*", []) $ G :: (if exists bad lits then change lits else lits)
+ Const ("*Goal*", []) $ G :: (if exists bad lits then change lits else lits)
end
| addLit (G,lits) = ins_term(G, lits)
@@ -884,9 +886,10 @@
(*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,tas)) (Const (b,tbs)) = a=b andalso matchs tas tbs
+ | match (Const (a,tas)) (Const (b,tbs)) =
+ a = "*Goal*" andalso b = Data.not_name orelse
+ a = Data.not_name andalso b = "*Goal*" orelse
+ a = b andalso matchs tas tbs
| match (Free a) (Free b) = (a=b)
| match (Bound i) (Bound j) = (i=j)
| match (Abs(_,t)) (Abs(_,u)) = match t u
@@ -903,15 +906,15 @@
fun printStats (b, start, tacs) =
if b then
- writeln (endTiming start ^ " for search. Closed: "
- ^ Int.toString (!nclosed) ^
+ writeln (endTiming start ^ " for search. Closed: "
+ ^ Int.toString (!nclosed) ^
" tried: " ^ Int.toString (!ntried) ^
" tactics: " ^ Int.toString (length tacs))
else ();
-(*Tableau prover based on leanTaP. Argument is a list of branches. Each
- branch contains a list of unexpanded formulae, a list of literals, and a
+(*Tableau prover based on leanTaP. Argument is a list of branches. Each
+ branch contains a list of unexpanded formulae, a list of literals, and a
bound on unsafe expansions.
"start" is CPU time at start, for printing search time
*)
@@ -919,259 +922,259 @@
let val {safe0_netpair, safep_netpair, haz_netpair, ...} = Data.rep_cs cs
val safeList = [safe0_netpair, safep_netpair]
and hazList = [haz_netpair]
- fun prv (tacs, trs, choices, []) =
- (printStats (!trace orelse !stats, start, tacs);
- cont (tacs, trs, choices)) (*all branches closed!*)
- | prv (tacs, trs, choices,
- brs0 as {pairs = ((G,md)::br, haz)::pairs,
- lits, vars, lim} :: brs) =
- (*apply a safe rule only (possibly allowing instantiation);
+ fun prv (tacs, trs, choices, []) =
+ (printStats (!trace orelse !stats, start, tacs);
+ cont (tacs, trs, choices)) (*all branches closed!*)
+ | prv (tacs, trs, choices,
+ brs0 as {pairs = ((G,md)::br, haz)::pairs,
+ lits, vars, lim} :: brs) =
+ (*apply a safe rule only (possibly allowing instantiation);
defer any haz formulae*)
- let exception PRV (*backtrack to precisely this recursion!*)
- val ntrl = !ntrail
- val nbrs = length brs0
+ 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 {pairs = ((joinMd md prem, []) ::
- negOfGoals ((br, haz)::pairs)),
- lits = map negOfGoal lits,
- vars = vars',
- lim = lim'}
- else {pairs = ((joinMd md prem, []) ::
- (br, haz) :: pairs),
- lits = lits,
- vars = vars',
- lim = lim'})
- prems @
- brs
- (*Seek a matching rule. If unifiable then add new premises
+ 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 {pairs = ((joinMd md prem, []) ::
+ negOfGoals ((br, haz)::pairs)),
+ lits = map negOfGoal lits,
+ vars = vars',
+ lim = lim'}
+ else {pairs = ((joinMd md prem, []) ::
+ (br, haz) :: pairs),
+ lits = lits,
+ vars = vars',
+ lim = lim'})
+ prems @
+ brs
+ (*Seek a matching rule. If unifiable then add new premises
to branch.*)
- fun deeper [] = raise NEWBRANCHES
- | deeper (((P,prems),tac)::grls) =
- if unify(add_term_vars(P,[]), P, G)
- then (*P comes from the rule; G comes from the branch.*)
- let val updated = ntrl < !ntrail (*branch updated*)
- val lim' = if updated
- then lim - (1+log(length rules))
- else lim (*discourage branching updates*)
- val vars = vars_in_vars vars
- val vars' = foldr add_terms_vars vars prems
- val choices' = (ntrl, nbrs, PRV) :: choices
- val tacs' = (tac(updated,false,true))
+ fun deeper [] = raise NEWBRANCHES
+ | deeper (((P,prems),tac)::grls) =
+ if unify(add_term_vars(P,[]), P, G)
+ then (*P comes from the rule; G comes from the branch.*)
+ let val updated = ntrl < !ntrail (*branch updated*)
+ val lim' = if updated
+ then lim - (1+log(length rules))
+ else lim (*discourage branching updates*)
+ val vars = vars_in_vars vars
+ val vars' = foldr add_terms_vars vars prems
+ val choices' = (ntrl, nbrs, PRV) :: choices
+ val tacs' = (tac(updated,false,true))
:: tacs (*no duplication; rotate*)
- in
- traceNew prems; traceVars sign ntrl;
- (if null prems then (*closed the branch: prune!*)
- (nclosed := !nclosed + 1;
- prv(tacs', brs0::trs,
- prune (nbrs, nxtVars, choices'),
- brs))
- else (*prems non-null*)
- if lim'<0 (*faster to kill ALL the alternatives*)
- then (traceMsg"Excessive branching: KILLED";
- clearTo ntrl; raise NEWBRANCHES)
- else
- (ntried := !ntried + length prems - 1;
- prv(tacs', brs0::trs, choices',
- newBr (vars',lim') prems)))
- handle PRV =>
- if updated then
- (*Backtrack at this level.
- Reset Vars and try another rule*)
- (clearTo ntrl; deeper grls)
- else (*backtrack to previous level*)
- backtrack choices
- end
- else deeper grls
- (*Try to close branch by unifying with head goal*)
- fun closeF [] = raise CLOSEF
- | closeF (L::Ls) =
- case tryClose(G,L) of
- NONE => closeF Ls
- | SOME tac =>
- let val choices' =
- (if !trace then (immediate_output"branch closed";
- traceVars sign ntrl)
- else ();
- prune (nbrs, nxtVars,
- (ntrl, nbrs, PRV) :: choices))
- in nclosed := !nclosed + 1;
- prv (tac::tacs, brs0::trs, choices', brs)
- handle PRV =>
- (*reset Vars and try another literal
- [this handler is pruned if possible!]*)
- (clearTo ntrl; closeF Ls)
- end
- (*Try to unify a queued formula (safe or haz) with head goal*)
- fun closeFl [] = raise CLOSEF
- | closeFl ((br, haz)::pairs) =
- closeF (map fst br)
- handle CLOSEF => closeF (map fst haz)
- handle CLOSEF => closeFl pairs
- in tracing sign brs0;
- if lim<0 then (traceMsg "Limit reached. "; backtrack choices)
- else
- prv (Data.hyp_subst_tac trace :: tacs,
- brs0::trs, choices,
- equalSubst sign
- (G, {pairs = (br,haz)::pairs,
- lits = lits, vars = vars, lim = lim})
- :: brs)
- handle DEST_EQ => closeF lits
- handle CLOSEF => closeFl ((br,haz)::pairs)
- handle CLOSEF => deeper rules
- handle NEWBRANCHES =>
- (case netMkRules G vars hazList of
- [] => (*there are no plausible haz rules*)
- (traceMsg "moving formula to literals";
- prv (tacs, brs0::trs, choices,
- {pairs = (br,haz)::pairs,
- lits = addLit(G,lits),
- vars = vars,
- lim = lim} :: brs))
- | _ => (*G admits some haz rules: try later*)
- (traceMsg "moving formula to haz list";
- prv (if isGoal G then negOfGoal_tac :: tacs
- else tacs,
- brs0::trs,
- choices,
- {pairs = (br, haz@[(negOfGoal G, md)])::pairs,
- lits = lits,
- vars = vars,
- lim = lim} :: brs)))
- end
- | prv (tacs, trs, choices,
- {pairs = ([],haz)::(Gs,haz')::pairs, lits, vars, lim} :: brs) =
- (*no more "safe" formulae: transfer haz down a level*)
- prv (tacs, trs, choices,
- {pairs = (Gs,haz@haz')::pairs,
- lits = lits,
- vars = vars,
- lim = lim} :: brs)
- | prv (tacs, trs, choices,
- brs0 as {pairs = [([], (H,md)::Hs)],
- lits, vars, lim} :: brs) =
- (*no safe steps possible at any level: apply a haz rule*)
- let exception PRV (*backtrack to precisely this recursion!*)
- val H = norm H
- val ntrl = !ntrail
- val rules = netMkRules H vars hazList
- (*new premises of haz rules may NOT be duplicated*)
- fun newPrem (vars,P,dup,lim') prem =
- let val Gs' = map (fn Q => (Q,false)) prem
- and Hs' = if dup then Hs @ [(negOfGoal H, md)] else Hs
- and lits' = if (exists isGoal prem)
- then map negOfGoal lits
- else lits
- in {pairs = if exists (match P) prem then [(Gs',Hs')]
- (*Recursive in this premise. Don't make new
- "stack frame". New haz premises will end up
- at the BACK of the queue, preventing
- exclusion of others*)
- else [(Gs',[]), ([],Hs')],
- lits = lits',
- vars = vars,
- lim = lim'}
- end
- fun newBr x prems = map (newPrem x) prems @ brs
- (*Seek a matching rule. If unifiable then add new premises
+ in
+ traceNew prems; traceVars sign ntrl;
+ (if null prems then (*closed the branch: prune!*)
+ (nclosed := !nclosed + 1;
+ prv(tacs', brs0::trs,
+ prune (nbrs, nxtVars, choices'),
+ brs))
+ else (*prems non-null*)
+ if lim'<0 (*faster to kill ALL the alternatives*)
+ then (traceMsg"Excessive branching: KILLED";
+ clearTo ntrl; raise NEWBRANCHES)
+ else
+ (ntried := !ntried + length prems - 1;
+ prv(tacs', brs0::trs, choices',
+ newBr (vars',lim') prems)))
+ handle PRV =>
+ if updated then
+ (*Backtrack at this level.
+ Reset Vars and try another rule*)
+ (clearTo ntrl; deeper grls)
+ else (*backtrack to previous level*)
+ backtrack choices
+ end
+ else deeper grls
+ (*Try to close branch by unifying with head goal*)
+ fun closeF [] = raise CLOSEF
+ | closeF (L::Ls) =
+ case tryClose(G,L) of
+ NONE => closeF Ls
+ | SOME tac =>
+ let val choices' =
+ (if !trace then (immediate_output"branch closed";
+ traceVars sign ntrl)
+ else ();
+ prune (nbrs, nxtVars,
+ (ntrl, nbrs, PRV) :: choices))
+ in nclosed := !nclosed + 1;
+ prv (tac::tacs, brs0::trs, choices', brs)
+ handle PRV =>
+ (*reset Vars and try another literal
+ [this handler is pruned if possible!]*)
+ (clearTo ntrl; closeF Ls)
+ end
+ (*Try to unify a queued formula (safe or haz) with head goal*)
+ fun closeFl [] = raise CLOSEF
+ | closeFl ((br, haz)::pairs) =
+ closeF (map fst br)
+ handle CLOSEF => closeF (map fst haz)
+ handle CLOSEF => closeFl pairs
+ in tracing sign brs0;
+ if lim<0 then (traceMsg "Limit reached. "; backtrack choices)
+ else
+ prv (Data.hyp_subst_tac trace :: tacs,
+ brs0::trs, choices,
+ equalSubst sign
+ (G, {pairs = (br,haz)::pairs,
+ lits = lits, vars = vars, lim = lim})
+ :: brs)
+ handle DEST_EQ => closeF lits
+ handle CLOSEF => closeFl ((br,haz)::pairs)
+ handle CLOSEF => deeper rules
+ handle NEWBRANCHES =>
+ (case netMkRules G vars hazList of
+ [] => (*there are no plausible haz rules*)
+ (traceMsg "moving formula to literals";
+ prv (tacs, brs0::trs, choices,
+ {pairs = (br,haz)::pairs,
+ lits = addLit(G,lits),
+ vars = vars,
+ lim = lim} :: brs))
+ | _ => (*G admits some haz rules: try later*)
+ (traceMsg "moving formula to haz list";
+ prv (if isGoal G then negOfGoal_tac :: tacs
+ else tacs,
+ brs0::trs,
+ choices,
+ {pairs = (br, haz@[(negOfGoal G, md)])::pairs,
+ lits = lits,
+ vars = vars,
+ lim = lim} :: brs)))
+ end
+ | prv (tacs, trs, choices,
+ {pairs = ([],haz)::(Gs,haz')::pairs, lits, vars, lim} :: brs) =
+ (*no more "safe" formulae: transfer haz down a level*)
+ prv (tacs, trs, choices,
+ {pairs = (Gs,haz@haz')::pairs,
+ lits = lits,
+ vars = vars,
+ lim = lim} :: brs)
+ | prv (tacs, trs, choices,
+ brs0 as {pairs = [([], (H,md)::Hs)],
+ lits, vars, lim} :: brs) =
+ (*no safe steps possible at any level: apply a haz rule*)
+ let exception PRV (*backtrack to precisely this recursion!*)
+ val H = norm H
+ val ntrl = !ntrail
+ val rules = netMkRules H vars hazList
+ (*new premises of haz rules may NOT be duplicated*)
+ fun newPrem (vars,P,dup,lim') prem =
+ let val Gs' = map (fn Q => (Q,false)) prem
+ and Hs' = if dup then Hs @ [(negOfGoal H, md)] else Hs
+ and lits' = if (exists isGoal prem)
+ then map negOfGoal lits
+ else lits
+ in {pairs = if exists (match P) prem then [(Gs',Hs')]
+ (*Recursive in this premise. Don't make new
+ "stack frame". New haz premises will end up
+ at the BACK of the queue, preventing
+ exclusion of others*)
+ else [(Gs',[]), ([],Hs')],
+ lits = lits',
+ vars = vars,
+ lim = 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) =
- if unify(add_term_vars(P,[]), P, H)
- then
- let val updated = ntrl < !ntrail (*branch updated*)
- val vars = vars_in_vars vars
- val vars' = foldr add_terms_vars vars prems
- (*duplicate H if md permits*)
- val dup = md (*earlier had "andalso vars' <> vars":
+ fun deeper [] = raise NEWBRANCHES
+ | deeper (((P,prems),tac)::grls) =
+ if unify(add_term_vars(P,[]), P, H)
+ then
+ let val updated = ntrl < !ntrail (*branch updated*)
+ val vars = vars_in_vars vars
+ val vars' = foldr add_terms_vars vars prems
+ (*duplicate H if md permits*)
+ val dup = md (*earlier had "andalso vars' <> vars":
duplicate only if the subgoal has new vars*)
- (*any instances of P in the subgoals?
- NB: boolean "recur" affects tracing only!*)
- and recur = exists (exists (match P)) prems
- val lim' = (*Decrement "lim" extra if updates occur*)
- if updated then lim - (1+log(length rules))
- else lim-1
- (*It is tempting to leave "lim" UNCHANGED if
- both dup and recur are false. Proofs are
- found at shallower depths, but looping
- occurs too often...*)
- val mayUndo =
- (*Allowing backtracking from a rule application
- if other matching rules exist, if the rule
- updated variables, or if the rule did not
- introduce new variables. This latter condition
- means it is not a standard "gamma-rule" but
- some other form of unsafe rule. Aim is to
- emulate Fast_tac, which allows all unsafe steps
- to be undone.*)
- not(null grls) (*other rules to try?*)
- orelse updated
- orelse vars=vars' (*no new Vars?*)
- val tac' = tac(updated, dup, true)
- (*if recur then perhaps shouldn't call rotate_tac: new
+ (*any instances of P in the subgoals?
+ NB: boolean "recur" affects tracing only!*)
+ and recur = exists (exists (match P)) prems
+ val lim' = (*Decrement "lim" extra if updates occur*)
+ if updated then lim - (1+log(length rules))
+ else lim-1
+ (*It is tempting to leave "lim" UNCHANGED if
+ both dup and recur are false. Proofs are
+ found at shallower depths, but looping
+ occurs too often...*)
+ val mayUndo =
+ (*Allowing backtracking from a rule application
+ if other matching rules exist, if the rule
+ updated variables, or if the rule did not
+ introduce new variables. This latter condition
+ means it is not a standard "gamma-rule" but
+ some other form of unsafe rule. Aim is to
+ emulate Fast_tac, which allows all unsafe steps
+ to be undone.*)
+ not(null grls) (*other rules to try?*)
+ orelse updated
+ orelse vars=vars' (*no new Vars?*)
+ val tac' = tac(updated, dup, true)
+ (*if recur then perhaps shouldn't call rotate_tac: new
formulae should be last, but that's WRONG if the new
formulae are Goals, since they remain in the first
position*)
- in
- if lim'<0 andalso not (null prems)
- then (*it's faster to kill ALL the alternatives*)
- (traceMsg"Excessive branching: KILLED";
- clearTo ntrl; raise NEWBRANCHES)
- else
- traceNew prems;
- if !trace andalso dup then immediate_output" (duplicating)"
- else ();
- if !trace andalso recur then immediate_output" (recursive)"
- else ();
- traceVars sign ntrl;
- if null prems then nclosed := !nclosed + 1
- else ntried := !ntried + length prems - 1;
- prv(tac' :: tacs,
- brs0::trs,
- (ntrl, length brs0, PRV) :: choices,
- newBr (vars', P, dup, lim') prems)
- handle PRV =>
- if mayUndo
- then (*reset Vars and try another rule*)
- (clearTo ntrl; deeper grls)
- else (*backtrack to previous level*)
- backtrack choices
- end
- else deeper grls
- in tracing sign brs0;
- if lim<1 then (traceMsg "Limit reached. "; backtrack choices)
- else deeper rules
- handle NEWBRANCHES =>
- (*cannot close branch: move H to literals*)
- prv (tacs, brs0::trs, choices,
- {pairs = [([], Hs)],
- lits = H::lits,
- vars = vars,
- lim = lim} :: brs)
- end
+ in
+ if lim'<0 andalso not (null prems)
+ then (*it's faster to kill ALL the alternatives*)
+ (traceMsg"Excessive branching: KILLED";
+ clearTo ntrl; raise NEWBRANCHES)
+ else
+ traceNew prems;
+ if !trace andalso dup then immediate_output" (duplicating)"
+ else ();
+ if !trace andalso recur then immediate_output" (recursive)"
+ else ();
+ traceVars sign ntrl;
+ if null prems then nclosed := !nclosed + 1
+ else ntried := !ntried + length prems - 1;
+ prv(tac' :: tacs,
+ brs0::trs,
+ (ntrl, length brs0, PRV) :: choices,
+ newBr (vars', P, dup, lim') prems)
+ handle PRV =>
+ if mayUndo
+ then (*reset Vars and try another rule*)
+ (clearTo ntrl; deeper grls)
+ else (*backtrack to previous level*)
+ backtrack choices
+ end
+ else deeper grls
+ in tracing sign brs0;
+ if lim<1 then (traceMsg "Limit reached. "; backtrack choices)
+ else deeper rules
+ handle NEWBRANCHES =>
+ (*cannot close branch: move H to literals*)
+ prv (tacs, brs0::trs, choices,
+ {pairs = [([], Hs)],
+ lits = H::lits,
+ vars = vars,
+ lim = 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) =
+fun initBranch (ts,lim) =
{pairs = [(map (fn t => (t,true)) ts, [])],
- lits = [],
- vars = add_terms_vars (ts,[]),
+ lits = [],
+ vars = add_terms_vars (ts,[]),
lim = lim};
(*** Conversion & Skolemization of the Isabelle proof state ***)
(*Make a list of all the parameters in a subgoal, even if nested*)
-local open Term
+local open Term
in
fun discard_foralls (Const("all",_)$Abs(a,T,t)) = discard_foralls t
| discard_foralls t = t;
@@ -1180,8 +1183,8 @@
(*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;
+ if i mem is then getVars alist i
+ else v :: getVars alist i;
exception TRANS of string;
@@ -1191,77 +1194,77 @@
and alistTVar = ref []
fun hdvar ((ix,(v,is))::_) = v
fun from lev t =
- let val (ht,ts) = Term.strip_comb t
- fun apply u = list_comb (u, map (from lev) ts)
- fun bounds [] = []
- | bounds (Term.Bound i::ts) =
- if i<lev then raise TRANS
- "Function unknown's argument not a parameter"
- else i-lev :: bounds ts
- | bounds ts = raise TRANS
- "Function unknown's argument not a bound variable"
+ let val (ht,ts) = Term.strip_comb t
+ fun apply u = list_comb (u, map (from lev) ts)
+ fun bounds [] = []
+ | bounds (Term.Bound i::ts) =
+ if i<lev then raise TRANS
+ "Function unknown's argument not a parameter"
+ else i-lev :: bounds ts
+ | bounds ts = raise TRANS
+ "Function unknown's argument not a bound variable"
in
- case ht of
- Term.Const aT => apply (fromConst alistTVar aT)
- | Term.Free (a,_) => apply (Free a)
- | Term.Bound i => apply (Bound i)
- | Term.Var (ix,_) =>
- (case (AList.lookup (op =) (!alistVar) ix) of
- NONE => (alistVar := (ix, (ref NONE, bounds ts))
- :: !alistVar;
- Var (hdvar(!alistVar)))
- | SOME(v,is) => if is=bounds ts then Var v
- else raise TRANS
- ("Discrepancy among occurrences of "
- ^ Syntax.string_of_vname ix))
- | Term.Abs (a,_,body) =>
- if null ts then Abs(a, from (lev+1) body)
- else raise TRANS "argument not in normal form"
+ case ht of
+ Term.Const aT => apply (fromConst alistTVar aT)
+ | Term.Free (a,_) => apply (Free a)
+ | Term.Bound i => apply (Bound i)
+ | Term.Var (ix,_) =>
+ (case (AList.lookup (op =) (!alistVar) ix) of
+ NONE => (alistVar := (ix, (ref NONE, bounds ts))
+ :: !alistVar;
+ Var (hdvar(!alistVar)))
+ | SOME(v,is) => if is=bounds ts then Var v
+ else raise TRANS
+ ("Discrepancy among occurrences of "
+ ^ Syntax.string_of_vname ix))
+ | Term.Abs (a,_,body) =>
+ if null ts then Abs(a, from (lev+1) body)
+ else raise TRANS "argument not in normal form"
end
val npars = length (Logic.strip_params t)
(*Skolemize a subgoal from a proof state*)
fun skoSubgoal i t =
- if i<npars then
- skoSubgoal (i+1)
- (subst_bound (Skolem (gensym "T_", getVars (!alistVar) i),
- t))
- else t
+ if i<npars then
+ skoSubgoal (i+1)
+ (subst_bound (Skolem (gensym "T_", getVars (!alistVar) i),
+ t))
+ else t
in skoSubgoal 0 (from 0 (discard_foralls t)) end;
-fun initialize thy =
+fun initialize thy =
(fullTrace:=[]; trail := []; ntrail := 0;
nclosed := 0; ntried := 1; typargs := Sign.const_typargs thy);
-(*Tactic using tableau engine and proof reconstruction.
+(*Tactic using tableau engine and proof reconstruction.
"start" is CPU time at start, for printing SEARCH time
- (also prints reconstruction time)
+ (also prints reconstruction time)
"lim" is depth limit.*)
-fun timing_depth_tac start cs lim i st0 =
+fun timing_depth_tac start cs lim i st0 =
let val st = (initialize (theory_of_thm st0); ObjectLogic.atomize_goal i st0);
val {sign,...} = rep_thm st
val skoprem = fromSubgoal (List.nth(prems_of st, i-1))
val hyps = strip_imp_prems skoprem
and concl = strip_imp_concl skoprem
- fun cont (tacs,_,choices) =
- let val start = startTiming()
- in
- case Seq.pull(EVERY' (rev tacs) i st) of
- NONE => (writeln ("PROOF FAILED for depth " ^
- Int.toString lim);
- if !trace then error "************************\n"
- else ();
- backtrack choices)
- | cell => (if (!trace orelse !stats)
- then writeln (endTiming start ^ " for reconstruction")
- else ();
- Seq.make(fn()=> cell))
+ fun cont (tacs,_,choices) =
+ let val start = startTiming()
+ in
+ case Seq.pull(EVERY' (rev tacs) i st) of
+ NONE => (writeln ("PROOF FAILED for depth " ^
+ Int.toString lim);
+ if !trace then error "************************\n"
+ else ();
+ backtrack choices)
+ | cell => (if (!trace orelse !stats)
+ then writeln (endTiming start ^ " for reconstruction")
+ else ();
+ Seq.make(fn()=> cell))
end
- in prove (sign, start, cs, [initBranch (mkGoal concl :: hyps, lim)], cont)
+ in prove (sign, start, cs, [initBranch (mkGoal concl :: hyps, lim)], cont)
end
handle PROVE => Seq.empty;
@@ -1270,58 +1273,61 @@
val depth_limit = ref 20;
-fun blast_tac cs i st =
- ((DEEPEN (1, !depth_limit) (timing_depth_tac (startTiming()) cs) 0) i
+fun blast_tac cs i st =
+ ((DEEPEN (1, !depth_limit) (timing_depth_tac (startTiming()) cs) 0) i
THEN flexflex_tac) st
handle TRANS s =>
- ((if !trace then warning ("blast: " ^ s) else ());
+ ((if !trace then warning ("blast: " ^ s) else ());
Seq.empty);
fun Blast_tac i = blast_tac (Data.claset()) i;
-(*** For debugging: these apply the prover to a subgoal and return
+(*** 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 =
- let val st = topthm()
- val {sign,...} = rep_thm st
- val skoprem = (initialize (theory_of_thm st);
- fromSubgoal (List.nth(prems_of st, i-1)))
- val hyps = strip_imp_prems skoprem
- and concl = strip_imp_concl skoprem
- in timeap prove (sign, startTiming(), cs,
- [initBranch (mkGoal concl :: hyps, lim)], I)
- end
- handle Subscript => error("There is no subgoal " ^ Int.toString i);
+fun trygl cs lim i =
+ let val st = topthm()
+ val {sign,...} = rep_thm st
+ val skoprem = (initialize (theory_of_thm st);
+ fromSubgoal (List.nth(prems_of st, i-1)))
+ val hyps = strip_imp_prems skoprem
+ and concl = strip_imp_concl skoprem
+ in timeap prove (sign, startTiming(), cs,
+ [initBranch (mkGoal concl :: hyps, lim)], I)
+ end
+ handle Subscript => error("There is no subgoal " ^ Int.toString i);
fun Trygl lim i = trygl (Data.claset()) lim i;
(*Read a string to make an initial, singleton branch*)
-fun readGoal sign s = read_cterm sign (s,propT) |>
- term_of |> fromTerm |> rand |> mkGoal;
+fun readGoal thy s = Sign.read_prop thy s |> fromTerm |> rand |> mkGoal;
-fun tryInThy thy lim s =
+fun tryInThy thy lim s =
(initialize thy;
- timeap prove (Theory.sign_of thy,
- startTiming(),
- Data.claset(),
- [initBranch ([readGoal (Theory.sign_of thy) s], lim)],
- I));
+ timeap prove (thy,
+ startTiming(),
+ Data.claset(),
+ [initBranch ([readGoal thy s], lim)],
+ I));
(** method setup **)
fun blast_args m =
- Method.bang_sectioned_args'
+ Method.bang_sectioned_args'
Data.cla_modifiers (Scan.lift (Scan.option Args.nat)) m;
fun blast_meth NONE = Data.cla_meth' blast_tac
| blast_meth (SOME lim) = Data.cla_meth' (fn cs => depth_tac cs lim);
-val setup = [Method.add_methods [("blast", blast_args blast_meth,
- "tableau prover")]];
+val setup =
+ [fn thy => thy
+ |> Sign.root_path
+ |> Theory.add_consts_i [("*Goal*", propT, NoSyn), ("*False*", propT, NoSyn)]
+ |> Sign.restore_naming thy,
+ Method.add_methods [("blast", blast_args blast_meth, "tableau prover")]];
end;