wenzelm@18525: (* Title: Provers/blast.ML wenzelm@18525: Author: Lawrence C Paulson, Cambridge University Computer Laboratory paulson@3083: Copyright 1997 University of Cambridge paulson@2894: paulson@2894: Generic tableau prover with proof reconstruction paulson@2894: paulson@2854: SKOLEMIZES ReplaceI WRONGLY: allow new vars in prems, or forbid such rules?? paulson@2894: Needs explicit instantiation of assumptions? paulson@2894: paulson@18171: Given the typeargs system, constructor Const could be eliminated, with paulson@18171: TConst replaced by a constructor that takes the typargs list as an argument. paulson@18171: However, Const is heavily used for logical connectives. paulson@2894: paulson@2924: Blast_tac is often more powerful than fast_tac, but has some limitations. paulson@2924: Blast_tac... wenzelm@18525: * ignores wrappers (addss, addbefore, addafter, addWrapper, ...); oheimb@4651: this restriction is intrinsic paulson@2894: * ignores elimination rules that don't have the correct format wenzelm@18525: (conclusion must be a formula variable) paulson@2924: * rules must not require higher-order unification, e.g. apply_type in ZF paulson@2924: + message "Function Var's argument not a bound variable" relates to this paulson@2924: * its proof strategy is more general but can actually be slower paulson@2894: paulson@2894: Known problems: paulson@3092: "Recursive" chains of rules can sometimes exclude other unsafe formulae wenzelm@18525: from expansion. This happens because newly-created formulae always wenzelm@18525: have priority over existing ones. But obviously recursive rules wenzelm@18525: such as transitivity are treated specially to prevent this. Sometimes wenzelm@18525: the formulae get into the wrong order (see WRONG below). paulson@3021: paulson@2924: With substition for equalities (hyp_subst_tac): paulson@3092: When substitution affects a haz formula or literal, it is moved paulson@2924: back to the list of safe formulae. paulson@2924: But there's no way of putting it in the right place. A "moved" or paulson@2924: "no DETERM" flag would prevent proofs failing here. paulson@2854: *) paulson@2854: paulson@2854: (*Should be a type abbreviation?*) paulson@2854: type netpair = (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net; paulson@2854: paulson@2854: signature BLAST_DATA = paulson@2854: sig paulson@2854: type claset wenzelm@18525: val equality_name: string wenzelm@18525: val not_name: string wenzelm@18525: val notE : thm (* [| ~P; P |] ==> R *) wenzelm@18525: val ccontr : thm wenzelm@18525: val contr_tac : int -> tactic wenzelm@18525: val dup_intr : thm -> thm wenzelm@23908: val hyp_subst_tac : bool -> int -> tactic wenzelm@18525: val claset : unit -> claset wenzelm@18525: val rep_cs : (* dependent on classical.ML *) wenzelm@18525: claset -> {safeIs: thm list, safeEs: thm list, wenzelm@18525: hazIs: thm list, hazEs: thm list, wenzelm@18525: swrappers: (string * wrapper) list, wenzelm@18525: uwrappers: (string * wrapper) list, wenzelm@18525: safe0_netpair: netpair, safep_netpair: netpair, wenzelm@18525: haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: ContextRules.netpair} wenzelm@7272: val cla_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list wenzelm@7559: val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method paulson@2854: end; paulson@2854: paulson@2854: paulson@2854: signature BLAST = paulson@2854: sig wenzelm@18525: type claset paulson@4233: exception TRANS of string (*reports translation errors*) wenzelm@18525: datatype term = wenzelm@18177: Const of string * term list paulson@2924: | Skolem of string * term option ref list paulson@2924: | Free of string paulson@2924: | Var of term option ref paulson@2924: | Bound of int paulson@2924: | Abs of string*term wenzelm@17795: | $ of term*term; paulson@2924: type branch wenzelm@18525: val depth_tac : claset -> int -> int -> tactic wenzelm@24112: val depth_limit : int Config.T wenzelm@18525: val blast_tac : claset -> int -> tactic wenzelm@18525: val Blast_tac : int -> tactic wenzelm@18708: val setup : theory -> theory paulson@2924: (*debugging tools*) wenzelm@18525: val stats : bool ref wenzelm@18525: val trace : bool ref wenzelm@18525: val fullTrace : branch list list ref wenzelm@18525: val fromType : (indexname * term) list ref -> Term.typ -> term wenzelm@24062: val fromTerm : theory -> Term.term -> term wenzelm@24062: val fromSubgoal : theory -> Term.term -> term paulson@4065: val instVars : term -> (unit -> unit) wenzelm@18525: val toTerm : int -> term -> Term.term wenzelm@18525: val readGoal : theory -> string -> term wenzelm@18525: val tryInThy : theory -> int -> string -> paulson@3083: (int->tactic) list * branch list list * (int*int*exn) list wenzelm@18525: val normBr : branch -> branch paulson@2854: end; paulson@2854: paulson@2854: wenzelm@18525: functor BlastFun(Data: BLAST_DATA) : BLAST = paulson@2854: struct paulson@2854: paulson@2854: type claset = Data.claset; paulson@2854: paulson@4323: val trace = ref false paulson@4323: and stats = ref false; (*for runtime and search statistics*) paulson@2854: wenzelm@18525: datatype term = wenzelm@18177: Const of string * term list (*typargs constant--as a terms!*) paulson@2854: | Skolem of string * term option ref list paulson@5343: | Free of string paulson@5343: | Var of term option ref paulson@5343: | Bound of int paulson@5343: | Abs of string*term paulson@5613: | op $ of term*term; paulson@2854: wenzelm@24062: (*Pending formulae carry md (may duplicate) flags*) wenzelm@24062: type branch = wenzelm@24062: {pairs: ((term*bool) list * (*safe formulae on this level*) wenzelm@24062: (term*bool) list) list, (*haz formulae on this level*) wenzelm@24062: lits: term list, (*literals: irreducible formulae*) wenzelm@24062: vars: term option ref list, (*variables occurring in branch*) wenzelm@24062: lim: int}; (*resource limit*) wenzelm@24062: wenzelm@24062: wenzelm@24062: (* global state information *) wenzelm@24062: wenzelm@24062: datatype state = State of wenzelm@24062: {thy: theory, wenzelm@24062: fullTrace: branch list list ref, wenzelm@24062: trail: term option ref list ref, wenzelm@24062: ntrail: int ref, wenzelm@24062: nclosed: int ref, wenzelm@24062: ntried: int ref} wenzelm@24062: wenzelm@24062: fun reject_const thy c = wenzelm@24062: is_some (Sign.const_type thy c) andalso wenzelm@24062: error ("blast: theory contains illegal constant " ^ quote c); wenzelm@24062: wenzelm@24062: fun initialize thy = wenzelm@24062: (reject_const thy "*Goal*"; wenzelm@24062: reject_const thy "*False*"; wenzelm@24062: State wenzelm@24062: {thy = thy, wenzelm@24062: fullTrace = ref [], wenzelm@24062: trail = ref [], wenzelm@24062: ntrail = ref 0, wenzelm@24062: nclosed = ref 0, (*branches closed: number of branches closed during the search*) wenzelm@24062: ntried = ref 1}); (*branches tried: number of branches created by splitting (counting from 1)*) wenzelm@24062: wenzelm@24062: paulson@2854: paulson@2854: (** Basic syntactic operations **) paulson@2854: paulson@2854: fun is_Var (Var _) = true paulson@2854: | is_Var _ = false; paulson@2854: paulson@2854: fun dest_Var (Var x) = x; paulson@2854: paulson@2854: fun rand (f$x) = x; paulson@2854: paulson@2854: (* maps (f, [t1,...,tn]) to f(t1,...,tn) *) skalberg@15570: val list_comb : term * term list -> term = Library.foldl (op $); paulson@2854: paulson@2854: (* maps f(t1,...,tn) to (f, [t1,...,tn]) ; naturally tail-recursive*) wenzelm@18525: fun strip_comb u : term * term list = paulson@2854: let fun stripc (f$t, ts) = stripc (f, t::ts) wenzelm@18525: | stripc x = x paulson@2854: in stripc(u,[]) end; paulson@2854: paulson@2854: (* maps f(t1,...,tn) to f , which is never a combination *) paulson@2854: fun head_of (f$t) = head_of f paulson@2854: | head_of u = u; paulson@2854: paulson@2854: paulson@2854: (** Particular constants **) paulson@2854: wenzelm@18525: fun negate P = Const (Data.not_name, []) $ P; wenzelm@18525: wenzelm@18525: fun isNot (Const (c, _) $ _) = c = Data.not_name wenzelm@18525: | isNot _ = false; paulson@2854: wenzelm@18177: fun mkGoal P = Const ("*Goal*", []) $ P; paulson@2854: wenzelm@18177: fun isGoal (Const ("*Goal*", _) $ _) = true wenzelm@18525: | isGoal _ = false; paulson@2854: wenzelm@18177: val TruepropC = ObjectLogic.judgment_name (the_context ()); wenzelm@18177: val TruepropT = Sign.the_const_type (the_context ()) TruepropC; paulson@18171: wenzelm@18177: fun mk_Trueprop t = Term.$ (Term.Const (TruepropC, TruepropT), t); paulson@2854: wenzelm@18177: fun strip_Trueprop (tm as Const (c, _) $ t) = if c = TruepropC then t else tm wenzelm@18177: | strip_Trueprop tm = tm; wenzelm@18177: paulson@2854: paulson@2854: paulson@4065: (*** Dealing with overloaded constants ***) paulson@2854: paulson@4065: (*alist is a map from TVar names to Vars. We need to unify the TVars paulson@4065: faithfully in order to track overloading*) wenzelm@18177: fun fromType alist (Term.Type(a,Ts)) = list_comb (Const (a, []), map (fromType alist) Ts) paulson@4065: | fromType alist (Term.TFree(a,_)) = Free a paulson@4065: | fromType alist (Term.TVar (ixn,_)) = wenzelm@18525: (case (AList.lookup (op =) (!alist) ixn) of wenzelm@18525: NONE => let val t' = Var(ref NONE) wenzelm@18525: in alist := (ixn, t') :: !alist; t' wenzelm@18525: end wenzelm@18525: | SOME v => v) paulson@2854: wenzelm@24062: fun fromConst thy alist (a, T) = wenzelm@24062: Const (a, map (fromType alist) (Sign.const_typargs thy (a, T))); paulson@2854: paulson@2854: paulson@2854: (*Tests whether 2 terms are alpha-convertible; chases instantiations*) wenzelm@18177: fun (Const (a, ts)) aconv (Const (b, us)) = a=b andalso aconvs (ts, us) paulson@2854: | (Skolem (a,_)) aconv (Skolem (b,_)) = a=b (*arglists must then be equal*) paulson@2854: | (Free a) aconv (Free b) = a=b skalberg@15531: | (Var(ref(SOME t))) aconv u = t aconv u skalberg@15531: | t aconv (Var(ref(SOME u))) = t aconv u wenzelm@18525: | (Var v) aconv (Var w) = v=w (*both Vars are un-assigned*) paulson@2854: | (Bound i) aconv (Bound j) = i=j paulson@2854: | (Abs(_,t)) aconv (Abs(_,u)) = t aconv u paulson@2854: | (f$t) aconv (g$u) = (f aconv g) andalso (t aconv u) wenzelm@18177: | _ aconv _ = false wenzelm@18177: and aconvs ([], []) = true wenzelm@18177: | aconvs (t :: ts, u :: us) = t aconv u andalso aconvs (ts, us) wenzelm@18177: | aconvs _ = false; paulson@2854: paulson@2854: paulson@2854: fun mem_term (_, []) = false paulson@2854: | mem_term (t, t'::ts) = t aconv t' orelse mem_term(t,ts); paulson@2854: paulson@2854: fun ins_term(t,ts) = if mem_term(t,ts) then ts else t :: ts; paulson@2854: paulson@2854: fun mem_var (v: term option ref, []) = false paulson@2854: | mem_var (v, v'::vs) = v=v' orelse mem_var(v,vs); paulson@2854: paulson@2854: fun ins_var(v,vs) = if mem_var(v,vs) then vs else v :: vs; paulson@2854: paulson@2854: paulson@2854: (** Vars **) paulson@2854: paulson@2854: (*Accumulates the Vars in the term, suppressing duplicates*) wenzelm@18525: fun add_term_vars (Skolem(a,args), vars) = add_vars_vars(args,vars) wenzelm@18525: | add_term_vars (Var (v as ref NONE), vars) = ins_var (v, vars) skalberg@15531: | add_term_vars (Var (ref (SOME u)), vars) = add_term_vars(u,vars) wenzelm@18525: | add_term_vars (Const (_,ts), vars) = add_terms_vars(ts,vars) wenzelm@18525: | add_term_vars (Abs (_,body), vars) = add_term_vars(body,vars) wenzelm@18525: | add_term_vars (f$t, vars) = add_term_vars (f, add_term_vars(t, vars)) wenzelm@18525: | add_term_vars (_, vars) = vars paulson@2854: (*Term list version. [The fold functionals are slow]*) paulson@2854: and add_terms_vars ([], vars) = vars paulson@2854: | add_terms_vars (t::ts, vars) = add_terms_vars (ts, add_term_vars(t,vars)) paulson@2854: (*Var list version.*) paulson@2854: and add_vars_vars ([], vars) = vars wenzelm@18525: | add_vars_vars (ref (SOME u) :: vs, vars) = wenzelm@18525: add_vars_vars (vs, add_term_vars(u,vars)) skalberg@15531: | add_vars_vars (v::vs, vars) = (*v must be a ref NONE*) wenzelm@18525: add_vars_vars (vs, ins_var (v, vars)); paulson@2854: paulson@2854: paulson@2854: (*Chase assignments in "vars"; return a list of unassigned variables*) paulson@2854: fun vars_in_vars vars = add_vars_vars(vars,[]); paulson@2854: paulson@2854: paulson@2854: paulson@2854: (*increment a term's non-local bound variables paulson@2854: inc is increment for bound variables paulson@2854: lev is level at which a bound variable is considered 'loose'*) wenzelm@18525: fun incr_bv (inc, lev, u as Bound i) = if i>=lev then Bound(i+inc) else u paulson@2854: | incr_bv (inc, lev, Abs(a,body)) = Abs(a, incr_bv(inc,lev+1,body)) paulson@2854: | incr_bv (inc, lev, f$t) = incr_bv(inc,lev,f) $ incr_bv(inc,lev,t) paulson@2854: | incr_bv (inc, lev, u) = u; paulson@2854: paulson@2854: fun incr_boundvars 0 t = t paulson@2854: | incr_boundvars inc t = incr_bv(inc,0,t); paulson@2854: paulson@2854: paulson@2854: (*Accumulate all 'loose' bound vars referring to level 'lev' or beyond. paulson@2854: (Bound 0) is loose at level 0 *) wenzelm@18525: fun add_loose_bnos (Bound i, lev, js) = if i Skolem(a, vars_in_vars args) wenzelm@18177: | Const(a,ts) => Const(a, map norm ts) skalberg@15531: | (Var (ref NONE)) => t skalberg@15531: | (Var (ref (SOME u))) => norm u paulson@2854: | (f $ u) => (case norm f of paulson@3101: Abs(_,body) => norm (subst_bound (u, body)) paulson@3101: | nf => nf $ norm u) paulson@2854: | _ => t; paulson@2854: paulson@2854: paulson@2854: (*Weak (one-level) normalize for use in unification*) paulson@2854: fun wkNormAux t = case t of paulson@2854: (Var v) => (case !v of wenzelm@18525: SOME u => wkNorm u wenzelm@18525: | NONE => t) paulson@2854: | (f $ u) => (case wkNormAux f of wenzelm@18525: Abs(_,body) => wkNorm (subst_bound (u, body)) wenzelm@18525: | nf => nf $ u) wenzelm@18525: | Abs (a,body) => (*eta-contract if possible*) wenzelm@18525: (case wkNormAux body of wenzelm@18525: nb as (f $ t) => wenzelm@20664: if member (op =) (loose_bnos f) 0 orelse wkNorm t <> Bound 0 wenzelm@18525: then Abs(a,nb) wenzelm@18525: else wkNorm (incr_boundvars ~1 f) wenzelm@18525: | nb => Abs (a,nb)) paulson@2854: | _ => t paulson@2854: and wkNorm t = case head_of t of paulson@2854: Const _ => t paulson@2854: | Skolem(a,args) => t paulson@2854: | Free _ => t paulson@2854: | _ => wkNormAux t; paulson@2854: paulson@2854: wenzelm@18525: (*Does variable v occur in u? For unification. paulson@5734: Dangling bound vars are also forbidden.*) wenzelm@18525: fun varOccur v = wenzelm@18525: let fun occL lev [] = false (*same as (exists occ), but faster*) wenzelm@18525: | occL lev (u::us) = occ lev u orelse occL lev us wenzelm@18525: and occ lev (Var w) = wenzelm@18525: v=w orelse skalberg@15531: (case !w of NONE => false wenzelm@18525: | SOME u => occ lev u) paulson@5734: | occ lev (Skolem(_,args)) = occL lev (map Var args) wenzelm@18177: (*ignore Const, since term variables can't occur in types (?) *) paulson@5734: | occ lev (Bound i) = lev <= i paulson@5734: | occ lev (Abs(_,u)) = occ (lev+1) u paulson@5734: | occ lev (f$u) = occ lev u orelse occ lev f paulson@5734: | occ lev _ = false; paulson@5734: in occ 0 end; paulson@2854: paulson@2854: exception UNIFY; paulson@2854: paulson@2854: paulson@2854: (*Restore the trail to some previous state: for backtracking*) wenzelm@24062: fun clearTo (State {ntrail, trail, ...}) n = paulson@3083: while !ntrail<>n do wenzelm@18525: (hd(!trail) := NONE; wenzelm@18525: trail := tl (!trail); wenzelm@18525: ntrail := !ntrail - 1); paulson@2854: paulson@2854: wenzelm@18525: (*First-order unification with bound variables. paulson@2854: "vars" is a list of variables local to the rule and NOT to be put wenzelm@18525: on the trail (no point in doing so) paulson@2854: *) wenzelm@24062: fun unify state (vars,t,u) = wenzelm@24062: let val State {ntrail, trail, ...} = state wenzelm@24062: val n = !ntrail wenzelm@18525: fun update (t as Var v, u) = wenzelm@18525: if t aconv u then () wenzelm@18525: else if varOccur v u then raise UNIFY wenzelm@18525: else if mem_var(v, vars) then v := SOME u wenzelm@18525: else (*avoid updating Vars in the branch if possible!*) wenzelm@18525: if is_Var u andalso mem_var(dest_Var u, vars) wenzelm@18525: then dest_Var u := SOME t wenzelm@18525: else (v := SOME u; wenzelm@18525: trail := v :: !trail; ntrail := !ntrail + 1) wenzelm@18525: fun unifyAux (t,u) = wenzelm@18525: case (wkNorm t, wkNorm u) of wenzelm@18525: (nt as Var v, nu) => update(nt,nu) wenzelm@18525: | (nu, nt as Var v) => update(nt,nu) wenzelm@18525: | (Const(a,ats), Const(b,bts)) => if a=b then unifysAux(ats,bts) wenzelm@18525: else raise UNIFY wenzelm@18525: | (Abs(_,t'), Abs(_,u')) => unifyAux(t',u') wenzelm@18525: (*NB: can yield unifiers having dangling Bound vars!*) wenzelm@18525: | (f$t', g$u') => (unifyAux(f,g); unifyAux(t',u')) wenzelm@18525: | (nt, nu) => if nt aconv nu then () else raise UNIFY wenzelm@18177: and unifysAux ([], []) = () wenzelm@18177: | unifysAux (t :: ts, u :: us) = (unifyAux (t, u); unifysAux (ts, us)) wenzelm@18177: | unifysAux _ = raise UNIFY; wenzelm@24062: in (unifyAux(t,u); true) handle UNIFY => (clearTo state n; false) paulson@2854: end; paulson@2854: paulson@2854: paulson@16774: (*Convert from "real" terms to prototerms; eta-contract. paulson@16774: Code is similar to fromSubgoal.*) wenzelm@24062: fun fromTerm thy t = paulson@4065: let val alistVar = ref [] paulson@4065: and alistTVar = ref [] wenzelm@24062: fun from (Term.Const aT) = fromConst thy alistTVar aT wenzelm@18525: | from (Term.Free (a,_)) = Free a wenzelm@18525: | from (Term.Bound i) = Bound i wenzelm@18525: | from (Term.Var (ixn,T)) = wenzelm@18525: (case (AList.lookup (op =) (!alistVar) ixn) of wenzelm@18525: NONE => let val t' = Var(ref NONE) wenzelm@18525: in alistVar := (ixn, t') :: !alistVar; t' wenzelm@18525: end wenzelm@18525: | SOME v => v) wenzelm@18525: | from (Term.Abs (a,_,u)) = wenzelm@18525: (case from u of wenzelm@18525: u' as (f $ Bound 0) => wenzelm@20664: if member (op =) (loose_bnos f) 0 then Abs(a,u') wenzelm@18525: else incr_boundvars ~1 f wenzelm@18525: | u' => Abs(a,u')) wenzelm@18525: | from (Term.$ (f,u)) = from f $ from u paulson@2854: in from t end; paulson@2854: paulson@4065: (*A debugging function: replaces all Vars by dummy Frees for visual inspection paulson@4065: of whether they are distinct. Function revert undoes the assignments.*) paulson@4065: fun instVars t = wenzelm@12902: let val name = ref "a" paulson@4065: val updated = ref [] wenzelm@18177: fun inst (Const(a,ts)) = List.app inst ts wenzelm@18525: | inst (Var(v as ref NONE)) = (updated := v :: (!updated); wenzelm@18525: v := SOME (Free ("?" ^ !name)); wenzelm@18525: name := Symbol.bump_string (!name)) wenzelm@18525: | inst (Abs(a,t)) = inst t wenzelm@18525: | inst (f $ u) = (inst f; inst u) wenzelm@18525: | inst _ = () skalberg@15570: fun revert() = List.app (fn v => v:=NONE) (!updated) paulson@4065: in inst t; revert end; paulson@4065: paulson@4065: paulson@2854: (* A1==>...An==>B goes to [A1,...,An], where B is not an implication *) wenzelm@18177: fun strip_imp_prems (Const ("==>", _) $ A $ B) = strip_Trueprop A :: strip_imp_prems B paulson@2854: | strip_imp_prems _ = []; paulson@2854: paulson@2854: (* A1==>...An==>B goes to B, where B is not an implication *) wenzelm@18177: fun strip_imp_concl (Const ("==>", _) $ A $ B) = strip_imp_concl B wenzelm@18177: | strip_imp_concl A = strip_Trueprop A; wenzelm@18177: paulson@2854: paulson@2854: paulson@2854: (*** Conversion of Elimination Rules to Tableau Operations ***) paulson@2854: paulson@9170: exception ElimBadConcl and ElimBadPrem; paulson@9170: paulson@9170: (*The conclusion becomes the goal/negated assumption *False*: delete it! wenzelm@18525: If we don't find it then the premise is ill-formed and could cause paulson@9170: PROOF FAILED*) paulson@9170: fun delete_concl [] = raise ElimBadPrem wenzelm@18525: | delete_concl (P :: Ps) = wenzelm@18525: (case P of wenzelm@18525: Const (c, _) $ Var (ref (SOME (Const ("*False*", _)))) => wenzelm@18525: if c = "*Goal*" orelse c = Data.not_name then Ps wenzelm@18525: else P :: delete_concl Ps wenzelm@18525: | _ => P :: delete_concl Ps); paulson@2854: wenzelm@18177: fun skoPrem vars (Const ("all", _) $ Abs (_, P)) = paulson@2854: skoPrem vars (subst_bound (Skolem (gensym "S_", vars), P)) paulson@2854: | skoPrem vars P = P; paulson@2854: wenzelm@18525: fun convertPrem t = paulson@9170: delete_concl (mkGoal (strip_imp_concl t) :: strip_imp_prems t); paulson@2854: paulson@2854: (*Expects elimination rules to have a formula variable as conclusion*) paulson@2854: fun convertRule vars t = paulson@2854: let val (P::Ps) = strip_imp_prems t paulson@2854: val Var v = strip_imp_concl t wenzelm@18177: in v := SOME (Const ("*False*", [])); wenzelm@18525: (P, map (convertPrem o skoPrem vars) Ps) paulson@9170: end paulson@9170: handle Bind => raise ElimBadConcl; paulson@2854: paulson@2854: paulson@2854: (*Like dup_elim, but puts the duplicated major premise FIRST*) haftmann@17257: fun rev_dup_elim th = (th RSN (2, revcut_rl)) |> assumption 2 |> Seq.hd; paulson@2854: paulson@2854: paulson@4391: (*Rotate the assumptions in all new subgoals for the LIFO discipline*) paulson@4391: local paulson@4391: (*Count new hyps so that they can be rotated*) paulson@4391: fun nNewHyps [] = 0 wenzelm@18177: | nNewHyps (Const ("*Goal*", _) $ _ :: Ps) = nNewHyps Ps paulson@4391: | nNewHyps (P::Ps) = 1 + nNewHyps Ps; paulson@2854: paulson@5463: fun rot_tac [] i st = Seq.single st paulson@4391: | rot_tac (0::ks) i st = rot_tac ks (i+1) st paulson@4391: | rot_tac (k::ks) i st = rot_tac ks (i+1) (rotate_rule (~k) i st); paulson@4391: in paulson@4391: fun rot_subgoals_tac (rot, rl) = wenzelm@18525: rot_tac (if rot then map nNewHyps rl else []) paulson@4391: end; paulson@4391: paulson@2854: wenzelm@26928: fun TRACE rl tac st i = if !trace then (Display.prth rl; tac st i) else tac st i; paulson@2854: paulson@5343: (*Resolution/matching tactics: if upd then the proof state may be updated. paulson@5343: Matching makes the tactics more deterministic in the presence of Vars.*) paulson@5343: fun emtac upd rl = TRACE rl (if upd then etac rl else ematch_tac [rl]); paulson@5343: fun rmtac upd rl = TRACE rl (if upd then rtac rl else match_tac [rl]); paulson@5343: wenzelm@18525: (*Tableau rule from elimination rule. paulson@5343: Flag "upd" says that the inference updated the branch. paulson@5343: Flag "dup" requests duplication of the affected formula.*) wenzelm@24062: fun fromRule thy vars rl = wenzelm@24062: let val trl = rl |> Thm.prop_of |> fromTerm thy |> convertRule vars wenzelm@18525: fun tac (upd, dup,rot) i = wenzelm@18525: emtac upd (if dup then rev_dup_elim rl else rl) i wenzelm@18525: THEN wenzelm@18525: rot_subgoals_tac (rot, #2 trl) i paulson@3244: in Option.SOME (trl, tac) end paulson@9170: handle ElimBadPrem => (*reject: prems don't preserve conclusion*) wenzelm@26928: (warning("Ignoring weak elimination rule\n" ^ Display.string_of_thm rl); wenzelm@18525: Option.NONE) paulson@9170: | ElimBadConcl => (*ignore: conclusion is not just a variable*) wenzelm@18525: (if !trace then (warning("Ignoring ill-formed elimination rule:\n" ^ wenzelm@26928: "conclusion should be a variable\n" ^ Display.string_of_thm rl)) wenzelm@18525: else (); wenzelm@18525: Option.NONE); paulson@2854: paulson@2854: paulson@3101: (*** Conversion of Introduction Rules ***) paulson@2854: paulson@2854: fun convertIntrPrem t = mkGoal (strip_imp_concl t) :: strip_imp_prems t; paulson@2854: paulson@2854: fun convertIntrRule vars t = paulson@2854: let val Ps = strip_imp_prems t paulson@2854: val P = strip_imp_concl t wenzelm@18525: in (mkGoal P, map (convertIntrPrem o skoPrem vars) Ps) paulson@2854: end; paulson@2854: wenzelm@18525: (*Tableau rule from introduction rule. paulson@5343: Flag "upd" says that the inference updated the branch. paulson@5343: Flag "dup" requests duplication of the affected formula. paulson@5343: Since haz rules are now delayed, "dup" is always FALSE for paulson@5343: introduction rules.*) wenzelm@24062: fun fromIntrRule thy vars rl = wenzelm@24062: let val trl = rl |> Thm.prop_of |> fromTerm thy |> convertIntrRule vars wenzelm@18525: fun tac (upd,dup,rot) i = wenzelm@18525: rmtac upd (if dup then Data.dup_intr rl else rl) i wenzelm@18525: THEN wenzelm@18525: rot_subgoals_tac (rot, #2 trl) i paulson@2854: in (trl, tac) end; paulson@2854: paulson@2854: paulson@3030: val dummyVar = Term.Var (("etc",0), dummyT); paulson@2854: paulson@2854: (*Convert from prototerms to ordinary terms with dummy types paulson@2924: Ignore abstractions; identify all Vars; STOP at given depth*) paulson@2924: fun toTerm 0 _ = dummyVar wenzelm@18177: | toTerm d (Const(a,_)) = Term.Const (a,dummyT) (*no need to convert typargs*) paulson@2924: | toTerm d (Skolem(a,_)) = Term.Const (a,dummyT) paulson@2924: | toTerm d (Free a) = Term.Free (a,dummyT) paulson@2924: | toTerm d (Bound i) = Term.Bound i paulson@2924: | toTerm d (Var _) = dummyVar paulson@2924: | toTerm d (Abs(a,_)) = dummyVar paulson@2924: | toTerm d (f $ u) = Term.$ (toTerm d f, toTerm (d-1) u); paulson@2854: paulson@2854: wenzelm@24062: fun netMkRules thy P vars (nps: netpair list) = paulson@2854: case P of wenzelm@18177: (Const ("*Goal*", _) $ G) => wenzelm@18525: let val pG = mk_Trueprop (toTerm 2 G) wenzelm@19482: val intrs = maps (fn (inet,_) => Net.unify_term inet pG) nps wenzelm@24062: in map (fromIntrRule thy vars o #2) (Tactic.orderlist intrs) end paulson@2854: | _ => wenzelm@18525: let val pP = mk_Trueprop (toTerm 3 P) wenzelm@19482: val elims = maps (fn (_,enet) => Net.unify_term enet pP) nps wenzelm@24062: in map_filter (fromRule thy vars o #2) (Tactic.orderlist elims) end; paulson@2854: paulson@3092: paulson@3092: (*Normalize a branch--for tracing*) paulson@3092: fun norm2 (G,md) = (norm G, md); paulson@3092: paulson@3092: fun normLev (Gs,Hs) = (map norm2 Gs, map norm2 Hs); paulson@3092: paulson@5463: fun normBr {pairs, lits, vars, lim} = wenzelm@18525: {pairs = map normLev pairs, wenzelm@18525: lits = map norm lits, wenzelm@18525: vars = vars, paulson@5463: lim = lim}; paulson@3092: paulson@3092: paulson@4065: val dummyTVar = Term.TVar(("a",0), []); paulson@3092: val dummyVar2 = Term.Var(("var",0), dummyT); paulson@3092: wenzelm@26938: (*convert blast_tac's type representation to real types for tracing*) paulson@4065: fun showType (Free a) = Term.TFree (a,[]) paulson@4065: | showType (Var _) = dummyTVar paulson@4065: | showType t = paulson@4065: (case strip_comb t of wenzelm@18525: (Const (a, _), us) => Term.Type(a, map showType us) wenzelm@18525: | _ => dummyT); paulson@4065: paulson@4065: (*Display top-level overloading if any*) wenzelm@18177: fun topType thy (Const (c, ts)) = SOME (Sign.const_instance thy (c, map showType ts)) wenzelm@18177: | topType thy (Abs(a,t)) = topType thy t wenzelm@18177: | topType thy (f $ u) = (case topType thy f of NONE => topType thy u | some => some) wenzelm@18177: | topType _ _ = NONE; paulson@4065: paulson@4065: paulson@3092: (*Convert from prototerms to ordinary terms with dummy types for tracing*) wenzelm@18177: fun showTerm d (Const (a,_)) = Term.Const (a,dummyT) paulson@3092: | showTerm d (Skolem(a,_)) = Term.Const (a,dummyT) paulson@3092: | showTerm d (Free a) = Term.Free (a,dummyT) paulson@3092: | showTerm d (Bound i) = Term.Bound i skalberg@15531: | showTerm d (Var(ref(SOME u))) = showTerm d u skalberg@15531: | showTerm d (Var(ref NONE)) = dummyVar2 paulson@3092: | showTerm d (Abs(a,t)) = if d=0 then dummyVar wenzelm@18525: else Term.Abs(a, dummyT, showTerm (d-1) t) paulson@3092: | showTerm d (f $ u) = if d=0 then dummyVar wenzelm@18525: else Term.$ (showTerm d f, showTerm (d-1) u); paulson@3092: wenzelm@26939: fun string_of thy d t = Syntax.string_of_term_global thy (showTerm d t); paulson@3092: paulson@19037: (*Convert a Goal to an ordinary Not. Used also in dup_intr, where a goal like paulson@19037: Ex(P) is duplicated as the assumption ~Ex(P). *) paulson@19037: fun negOfGoal (Const ("*Goal*", _) $ G) = negate G paulson@19037: | negOfGoal G = G; paulson@19037: paulson@19037: fun negOfGoal2 (G,md) = (negOfGoal G, md); paulson@19037: paulson@19037: (*Converts all Goals to Nots in the safe parts of a branch. They could paulson@19037: have been moved there from the literals list after substitution (equalSubst). paulson@19037: There can be at most one--this function could be made more efficient.*) paulson@19037: fun negOfGoals pairs = map (fn (Gs,haz) => (map negOfGoal2 Gs, haz)) pairs; paulson@19037: paulson@19037: (*Tactic. Convert *Goal* to negated assumption in FIRST position*) paulson@19037: fun negOfGoal_tac i = TRACE Data.ccontr (rtac Data.ccontr) i THEN paulson@19037: rotate_tac ~1 i; paulson@19037: wenzelm@24062: fun traceTerm thy t = paulson@19037: let val t' = norm (negOfGoal t) wenzelm@24062: val stm = string_of thy 8 t' wenzelm@18525: in wenzelm@24062: case topType thy t' of wenzelm@18525: NONE => stm (*no type to attach*) wenzelm@26939: | SOME T => stm ^ "\t:: " ^ Syntax.string_of_typ_global thy T paulson@4065: end; paulson@3092: paulson@3092: paulson@3092: (*Print tracing information at each iteration of prover*) wenzelm@24062: fun tracing (State {thy, fullTrace, ...}) brs = wenzelm@24062: let fun printPairs (((G,_)::_,_)::_) = Output.immediate_output(traceTerm thy G) wenzelm@24062: | printPairs (([],(H,_)::_)::_) = Output.immediate_output(traceTerm thy H ^ "\t (Unsafe)") wenzelm@18525: | printPairs _ = () paulson@5463: fun printBrs (brs0 as {pairs, lits, lim, ...} :: brs) = wenzelm@18525: (fullTrace := brs0 :: !fullTrace; wenzelm@22580: List.app (fn _ => Output.immediate_output "+") brs; wenzelm@22580: Output.immediate_output (" [" ^ Int.toString lim ^ "] "); wenzelm@18525: printPairs pairs; wenzelm@18525: writeln"") paulson@3092: in if !trace then printBrs (map normBr brs) else () paulson@3092: end; paulson@3092: paulson@5343: fun traceMsg s = if !trace then writeln s else (); paulson@4065: paulson@3092: (*Tracing: variables updated in the last branch operation?*) wenzelm@24062: fun traceVars (State {thy, ntrail, trail, ...}) ntrl = wenzelm@18525: if !trace then paulson@4065: (case !ntrail-ntrl of wenzelm@18525: 0 => () wenzelm@22580: | 1 => Output.immediate_output"\t1 variable UPDATED:" wenzelm@22580: | n => Output.immediate_output("\t" ^ Int.toString n ^ " variables UPDATED:"); paulson@4065: (*display the instantiations themselves, though no variable names*) wenzelm@24062: List.app (fn v => Output.immediate_output(" " ^ string_of thy 4 (the (!v)))) paulson@4065: (List.take(!trail, !ntrail-ntrl)); paulson@4065: writeln"") paulson@3092: else (); paulson@3092: paulson@3092: (*Tracing: how many new branches are created?*) paulson@3092: fun traceNew prems = wenzelm@18525: if !trace then paulson@3092: case length prems of wenzelm@22580: 0 => Output.immediate_output"branch closed by rule" wenzelm@22580: | 1 => Output.immediate_output"branch extended (1 new subgoal)" wenzelm@22580: | n => Output.immediate_output("branch split: "^ Int.toString n ^ " new subgoals") paulson@3092: else (); paulson@3092: paulson@3092: paulson@3092: paulson@2854: (*** Code for handling equality: naive substitution, like hyp_subst_tac ***) paulson@2854: wenzelm@18525: (*Replace the ATOMIC term "old" by "new" in t*) paulson@2854: fun subst_atomic (old,new) t = skalberg@15531: let fun subst (Var(ref(SOME u))) = subst u wenzelm@18525: | subst (Abs(a,body)) = Abs(a, subst body) wenzelm@18525: | subst (f$t) = subst f $ subst t wenzelm@18525: | subst t = if t aconv old then new else t paulson@2854: in subst t end; paulson@2854: paulson@2854: (*Eta-contract a term from outside: just enough to reduce it to an atom*) wenzelm@18525: fun eta_contract_atom (t0 as Abs(a, body)) = paulson@2854: (case eta_contract2 body of wenzelm@20664: f $ Bound 0 => if member (op =) (loose_bnos f) 0 then t0 wenzelm@18525: else eta_contract_atom (incr_boundvars ~1 f) paulson@2854: | _ => t0) paulson@2854: | eta_contract_atom t = t paulson@2854: and eta_contract2 (f$t) = f $ eta_contract_atom t paulson@2854: | eta_contract2 t = eta_contract_atom t; paulson@2854: paulson@2854: paulson@2854: (*When can we safely delete the equality? paulson@2854: Not if it equates two constants; consider 0=1. paulson@2854: Not if it resembles x=t[x], since substitution does not eliminate x. paulson@2854: Not if it resembles ?x=0; another goal could instantiate ?x to Suc(i) paulson@2854: Prefer to eliminate Bound variables if possible. paulson@2854: Result: true = use as is, false = reorient first *) paulson@2854: wenzelm@18525: (*Can t occur in u? For substitution. paulson@4354: Does NOT examine the args of Skolem terms: substitution does not affect them. paulson@4196: REFLEXIVE because hyp_subst_tac fails on x=x.*) wenzelm@18525: fun substOccur t = wenzelm@18525: let (*NO vars are permitted in u except the arguments of t, if it is paulson@4354: a Skolem term. This ensures that no equations are deleted that could paulson@4354: be instantiated to a cycle. For example, x=?a is rejected because ?a wenzelm@18525: could be instantiated to Suc(x).*) paulson@4354: val vars = case t of paulson@4354: Skolem(_,vars) => vars wenzelm@18525: | _ => [] paulson@4354: fun occEq u = (t aconv u) orelse occ u skalberg@15531: and occ (Var(ref(SOME u))) = occEq u paulson@4354: | occ (Var v) = not (mem_var (v, vars)) wenzelm@18525: | occ (Abs(_,u)) = occEq u paulson@2854: | occ (f$u) = occEq u orelse occEq f paulson@2854: | occ (_) = false; paulson@2854: in occEq end; paulson@2854: paulson@3092: exception DEST_EQ; paulson@3092: wenzelm@18177: (*Take apart an equality. NO constant Trueprop*) wenzelm@18525: fun dest_eq (Const (c, _) $ t $ u) = wenzelm@18525: if c = Data.equality_name then (eta_contract_atom t, eta_contract_atom u) wenzelm@18525: else raise DEST_EQ wenzelm@18525: | dest_eq _ = raise DEST_EQ; paulson@3092: paulson@4196: (*Reject the equality if u occurs in (or equals!) t*) paulson@2854: fun check (t,u,v) = if substOccur t u then raise DEST_EQ else v; paulson@2854: wenzelm@18525: (*IF the goal is an equality with a substitutable variable paulson@2854: THEN orient that equality ELSE raise exception DEST_EQ*) paulson@3092: fun orientGoal (t,u) = case (t,u) of wenzelm@18525: (Skolem _, _) => check(t,u,(t,u)) (*eliminates t*) wenzelm@18525: | (_, Skolem _) => check(u,t,(u,t)) (*eliminates u*) wenzelm@18525: | (Free _, _) => check(t,u,(t,u)) (*eliminates t*) wenzelm@18525: | (_, Free _) => check(u,t,(u,t)) (*eliminates u*) paulson@2854: | _ => raise DEST_EQ; paulson@2854: paulson@2894: (*Substitute through the branch if an equality goal (else raise DEST_EQ). paulson@2894: Moves affected literals back into the branch, but it is not clear where paulson@4391: they should go: this could make proofs fail.*) wenzelm@24062: fun equalSubst thy (G, {pairs, lits, vars, lim}) = paulson@3092: let val (t,u) = orientGoal(dest_eq G) paulson@3092: val subst = subst_atomic (t,u) paulson@2854: fun subst2(G,md) = (subst G, md) paulson@4466: (*substitute throughout list; extract affected formulae*) paulson@4466: fun subForm ((G,md), (changed, pairs)) = wenzelm@18525: let val nG = subst G wenzelm@18525: in if nG aconv G then (changed, (G,md)::pairs) wenzelm@18525: else ((nG,md)::changed, pairs) paulson@2924: end paulson@4466: (*substitute throughout "stack frame"; extract affected formulae*) paulson@4466: fun subFrame ((Gs,Hs), (changed, frames)) = wenzelm@30193: let val (changed', Gs') = List.foldr subForm (changed, []) Gs wenzelm@30193: val (changed'', Hs') = List.foldr subForm (changed', []) Hs paulson@4466: in (changed'', (Gs',Hs')::frames) end paulson@4466: (*substitute throughout literals; extract affected ones*) paulson@4466: fun subLit (lit, (changed, nlits)) = wenzelm@18525: let val nlit = subst lit wenzelm@18525: in if nlit aconv lit then (changed, nlit::nlits) wenzelm@18525: else ((nlit,true)::changed, nlits) paulson@2854: end wenzelm@30193: val (changed, lits') = List.foldr subLit ([], []) lits wenzelm@30193: val (changed', pairs') = List.foldr subFrame (changed, []) pairs wenzelm@24062: in if !trace then writeln ("Substituting " ^ traceTerm thy u ^ wenzelm@24062: " for " ^ traceTerm thy t ^ " in branch" ) paulson@3092: else (); wenzelm@18525: {pairs = (changed',[])::pairs', (*affected formulas, and others*) wenzelm@18525: lits = lits', (*unaffected literals*) wenzelm@18525: vars = vars, paulson@5463: lim = lim} paulson@2854: end; paulson@2854: paulson@2854: paulson@2854: exception NEWBRANCHES and CLOSEF; paulson@2854: paulson@2854: exception PROVE; paulson@2854: paulson@4391: (*Trying eq_contr_tac first INCREASES the effort, slowing reconstruction*) wenzelm@18525: val contr_tac = ematch_tac [Data.notE] THEN' paulson@4391: (eq_assume_tac ORELSE' assume_tac); paulson@2854: paulson@4391: val eContr_tac = TRACE Data.notE contr_tac; paulson@2854: val eAssume_tac = TRACE asm_rl (eq_assume_tac ORELSE' assume_tac); paulson@2854: wenzelm@18525: (*Try to unify complementary literals and return the corresponding tactic. *) wenzelm@24062: fun tryClose state (G, L) = wenzelm@18525: let wenzelm@24062: fun close t u tac = if unify state ([], t, u) then SOME tac else NONE; wenzelm@18525: fun arg (_ $ t) = t; wenzelm@18525: in wenzelm@18525: if isGoal G then close (arg G) L eAssume_tac wenzelm@18525: else if isGoal L then close G (arg L) eAssume_tac wenzelm@18525: else if isNot G then close (arg G) L eContr_tac wenzelm@18525: else if isNot L then close G (arg L) eContr_tac wenzelm@18525: else NONE wenzelm@18525: end; paulson@2854: paulson@2854: (*Were there Skolem terms in the premise? Must NOT chase Vars*) paulson@2854: fun hasSkolem (Skolem _) = true wenzelm@18525: | hasSkolem (Abs (_,body)) = hasSkolem body paulson@2854: | hasSkolem (f$t) = hasSkolem f orelse hasSkolem t paulson@2854: | hasSkolem _ = false; paulson@2854: paulson@2854: (*Attach the right "may duplicate" flag to new formulae: if they contain paulson@2854: Skolem terms then allow duplication.*) paulson@2854: fun joinMd md [] = [] paulson@2854: | joinMd md (G::Gs) = (G, hasSkolem G orelse md) :: joinMd md Gs; paulson@2854: paulson@2854: paulson@2854: (** Backtracking and Pruning **) paulson@2854: paulson@2854: (*clashVar vars (n,trail) determines whether any of the last n elements paulson@2854: of "trail" occur in "vars" OR in their instantiations*) paulson@2854: fun clashVar [] = (fn _ => false) paulson@2854: | clashVar vars = paulson@2854: let fun clash (0, _) = false wenzelm@18525: | clash (_, []) = false wenzelm@18525: | clash (n, v::vs) = exists (varOccur v) vars orelse clash(n-1,vs) paulson@2854: in clash end; paulson@2854: paulson@2854: paulson@2854: (*nbrs = # of branches just prior to closing this one. Delete choice points paulson@2854: for goals proved by the latest inference, provided NO variables in the paulson@2854: next branch have been updated.*) wenzelm@24062: fun prune _ (1, nxtVars, choices) = choices (*DON'T prune at very end: allow wenzelm@18525: backtracking over bad proofs*) wenzelm@24062: | prune (State {ntrail, trail, ...}) (nbrs: int, nxtVars, choices) = paulson@2854: let fun traceIt last = wenzelm@18525: let val ll = length last wenzelm@18525: and lc = length choices wenzelm@18525: in if !trace andalso ll nbrs then pruneAux (last, ntrl, trl, choices) wenzelm@18525: else (* nbrs'=nbrs *) wenzelm@18525: if clashVar nxtVars (ntrl-ntrl', trl) then last wenzelm@18525: else (*no clashes: can go back at least this far!*) wenzelm@18525: pruneAux(choices, ntrl', List.drop(trl, ntrl-ntrl'), wenzelm@18525: choices) paulson@2854: in traceIt (pruneAux (choices, !ntrail, !trail, choices)) end; paulson@2854: paulson@5463: fun nextVars ({pairs, lits, vars, lim} :: _) = map Var vars paulson@5463: | nextVars [] = []; paulson@2854: wenzelm@18525: fun backtrack (choices as (ntrl, nbrs, exn)::_) = wenzelm@18525: (if !trace then (writeln ("Backtracking; now there are " ^ wenzelm@18525: Int.toString nbrs ^ " branches")) wenzelm@18525: else (); paulson@3083: raise exn) paulson@3083: | backtrack _ = raise PROVE; paulson@2854: paulson@2894: (*Add the literal G, handling *Goal* and detecting duplicates.*) wenzelm@18525: fun addLit (Const ("*Goal*", _) $ G, lits) = paulson@2894: (*New literal is a *Goal*, so change all other Goals to Nots*) wenzelm@18177: let fun bad (Const ("*Goal*", _) $ _) = true wenzelm@18525: | bad (Const (c, _) $ G') = c = Data.not_name andalso G aconv G' wenzelm@18525: | bad _ = false; wenzelm@18525: fun change [] = [] wenzelm@18525: | change (lit :: lits) = wenzelm@18525: (case lit of wenzelm@18525: Const (c, _) $ G' => wenzelm@18525: if c = "*Goal*" orelse c = Data.not_name then wenzelm@18525: if G aconv G' then change lits wenzelm@18525: else negate G' :: change lits wenzelm@18525: else lit :: change lits wenzelm@18525: | _ => lit :: change lits) paulson@2854: in wenzelm@18525: Const ("*Goal*", []) $ G :: (if exists bad lits then change lits else lits) paulson@2854: end paulson@2854: | addLit (G,lits) = ins_term(G, lits) paulson@2854: paulson@2854: paulson@2952: (*For calculating the "penalty" to assess on a branching factor of n paulson@2952: log2 seems a little too severe*) paulson@3083: fun log n = if n<4 then 0 else 1 + log(n div 4); paulson@2924: paulson@2924: paulson@3021: (*match(t,u) says whether the term u might be an instance of the pattern t paulson@3021: Used to detect "recursive" rules such as transitivity*) paulson@3021: fun match (Var _) u = true wenzelm@18525: | match (Const (a,tas)) (Const (b,tbs)) = wenzelm@18525: a = "*Goal*" andalso b = Data.not_name orelse wenzelm@18525: a = Data.not_name andalso b = "*Goal*" orelse wenzelm@18525: a = b andalso matchs tas tbs paulson@4065: | match (Free a) (Free b) = (a=b) paulson@4065: | match (Bound i) (Bound j) = (i=j) paulson@4065: | match (Abs(_,t)) (Abs(_,u)) = match t u paulson@4065: | match (f$t) (g$u) = match f g andalso match t u wenzelm@18177: | match t u = false wenzelm@18177: and matchs [] [] = true wenzelm@18177: | matchs (t :: ts) (u :: us) = match t u andalso matchs ts us; paulson@3021: paulson@3021: wenzelm@24062: fun printStats (State {ntried, nclosed, ...}) (b, start, tacs) = paulson@4323: if b then wenzelm@30187: writeln (#message (end_timing start) ^ " for search. Closed: " wenzelm@18525: ^ Int.toString (!nclosed) ^ paulson@4391: " tried: " ^ Int.toString (!ntried) ^ paulson@4391: " tactics: " ^ Int.toString (length tacs)) paulson@4323: else (); paulson@4323: paulson@4323: wenzelm@18525: (*Tableau prover based on leanTaP. Argument is a list of branches. Each wenzelm@18525: branch contains a list of unexpanded formulae, a list of literals, and a paulson@4391: bound on unsafe expansions. paulson@4391: "start" is CPU time at start, for printing search time paulson@4391: *) wenzelm@24062: fun prove (state, start, cs, brs, cont) = wenzelm@24062: let val State {thy, ntrail, nclosed, ntried, ...} = state; wenzelm@24062: val {safe0_netpair, safep_netpair, haz_netpair, ...} = Data.rep_cs cs paulson@2854: val safeList = [safe0_netpair, safep_netpair] paulson@2854: and hazList = [haz_netpair] wenzelm@18525: fun prv (tacs, trs, choices, []) = wenzelm@24062: (printStats state (!trace orelse !stats, start, tacs); wenzelm@18525: cont (tacs, trs, choices)) (*all branches closed!*) wenzelm@18525: | prv (tacs, trs, choices, wenzelm@18525: brs0 as {pairs = ((G,md)::br, haz)::pairs, wenzelm@18525: lits, vars, lim} :: brs) = wenzelm@18525: (*apply a safe rule only (possibly allowing instantiation); paulson@3917: defer any haz formulae*) wenzelm@18525: let exception PRV (*backtrack to precisely this recursion!*) wenzelm@18525: val ntrl = !ntrail wenzelm@18525: val nbrs = length brs0 paulson@2854: val nxtVars = nextVars brs wenzelm@18525: val G = norm G wenzelm@24062: val rules = netMkRules thy G vars safeList wenzelm@18525: (*Make a new branch, decrementing "lim" if instantiations occur*) wenzelm@18525: fun newBr (vars',lim') prems = wenzelm@18525: map (fn prem => wenzelm@18525: if (exists isGoal prem) wenzelm@18525: then {pairs = ((joinMd md prem, []) :: wenzelm@18525: negOfGoals ((br, haz)::pairs)), wenzelm@18525: lits = map negOfGoal lits, wenzelm@18525: vars = vars', wenzelm@18525: lim = lim'} wenzelm@18525: else {pairs = ((joinMd md prem, []) :: wenzelm@18525: (br, haz) :: pairs), wenzelm@18525: lits = lits, wenzelm@18525: vars = vars', wenzelm@18525: lim = lim'}) wenzelm@18525: prems @ wenzelm@18525: brs wenzelm@18525: (*Seek a matching rule. If unifiable then add new premises paulson@2854: to branch.*) wenzelm@18525: fun deeper [] = raise NEWBRANCHES wenzelm@18525: | deeper (((P,prems),tac)::grls) = wenzelm@24062: if unify state (add_term_vars(P,[]), P, G) wenzelm@18525: then (*P comes from the rule; G comes from the branch.*) wenzelm@18525: let val updated = ntrl < !ntrail (*branch updated*) wenzelm@18525: val lim' = if updated wenzelm@18525: then lim - (1+log(length rules)) wenzelm@18525: else lim (*discourage branching updates*) wenzelm@18525: val vars = vars_in_vars vars wenzelm@30193: val vars' = List.foldr add_terms_vars vars prems wenzelm@18525: val choices' = (ntrl, nbrs, PRV) :: choices wenzelm@18525: val tacs' = (tac(updated,false,true)) paulson@5343: :: tacs (*no duplication; rotate*) wenzelm@18525: in wenzelm@24062: traceNew prems; traceVars state ntrl; wenzelm@18525: (if null prems then (*closed the branch: prune!*) wenzelm@18525: (nclosed := !nclosed + 1; wenzelm@18525: prv(tacs', brs0::trs, wenzelm@24062: prune state (nbrs, nxtVars, choices'), wenzelm@18525: brs)) wenzelm@18525: else (*prems non-null*) wenzelm@18525: if lim'<0 (*faster to kill ALL the alternatives*) wenzelm@18525: then (traceMsg"Excessive branching: KILLED"; wenzelm@24062: clearTo state ntrl; raise NEWBRANCHES) wenzelm@18525: else wenzelm@18525: (ntried := !ntried + length prems - 1; wenzelm@18525: prv(tacs', brs0::trs, choices', wenzelm@18525: newBr (vars',lim') prems))) wenzelm@18525: handle PRV => wenzelm@18525: if updated then wenzelm@18525: (*Backtrack at this level. wenzelm@18525: Reset Vars and try another rule*) wenzelm@24062: (clearTo state ntrl; deeper grls) wenzelm@18525: else (*backtrack to previous level*) wenzelm@18525: backtrack choices wenzelm@18525: end wenzelm@18525: else deeper grls wenzelm@18525: (*Try to close branch by unifying with head goal*) wenzelm@18525: fun closeF [] = raise CLOSEF wenzelm@18525: | closeF (L::Ls) = wenzelm@24062: case tryClose state (G,L) of wenzelm@18525: NONE => closeF Ls wenzelm@18525: | SOME tac => wenzelm@18525: let val choices' = wenzelm@22580: (if !trace then (Output.immediate_output"branch closed"; wenzelm@24062: traceVars state ntrl) wenzelm@18525: else (); wenzelm@24062: prune state (nbrs, nxtVars, wenzelm@18525: (ntrl, nbrs, PRV) :: choices)) wenzelm@18525: in nclosed := !nclosed + 1; wenzelm@18525: prv (tac::tacs, brs0::trs, choices', brs) wenzelm@18525: handle PRV => wenzelm@18525: (*reset Vars and try another literal wenzelm@18525: [this handler is pruned if possible!]*) wenzelm@24062: (clearTo state ntrl; closeF Ls) wenzelm@18525: end wenzelm@18525: (*Try to unify a queued formula (safe or haz) with head goal*) wenzelm@18525: fun closeFl [] = raise CLOSEF wenzelm@18525: | closeFl ((br, haz)::pairs) = wenzelm@18525: closeF (map fst br) wenzelm@18525: handle CLOSEF => closeF (map fst haz) wenzelm@18525: handle CLOSEF => closeFl pairs wenzelm@24062: in tracing state brs0; wenzelm@18525: if lim<0 then (traceMsg "Limit reached. "; backtrack choices) wenzelm@18525: else wenzelm@23908: prv (Data.hyp_subst_tac (!trace) :: tacs, wenzelm@18525: brs0::trs, choices, wenzelm@24062: equalSubst thy wenzelm@18525: (G, {pairs = (br,haz)::pairs, wenzelm@18525: lits = lits, vars = vars, lim = lim}) wenzelm@18525: :: brs) wenzelm@18525: handle DEST_EQ => closeF lits wenzelm@18525: handle CLOSEF => closeFl ((br,haz)::pairs) wenzelm@18525: handle CLOSEF => deeper rules wenzelm@18525: handle NEWBRANCHES => wenzelm@24062: (case netMkRules thy G vars hazList of wenzelm@18525: [] => (*there are no plausible haz rules*) wenzelm@18525: (traceMsg "moving formula to literals"; wenzelm@18525: prv (tacs, brs0::trs, choices, wenzelm@18525: {pairs = (br,haz)::pairs, wenzelm@18525: lits = addLit(G,lits), wenzelm@18525: vars = vars, wenzelm@18525: lim = lim} :: brs)) wenzelm@18525: | _ => (*G admits some haz rules: try later*) wenzelm@18525: (traceMsg "moving formula to haz list"; wenzelm@18525: prv (if isGoal G then negOfGoal_tac :: tacs wenzelm@18525: else tacs, wenzelm@18525: brs0::trs, wenzelm@18525: choices, wenzelm@18525: {pairs = (br, haz@[(negOfGoal G, md)])::pairs, wenzelm@18525: lits = lits, wenzelm@18525: vars = vars, wenzelm@18525: lim = lim} :: brs))) wenzelm@18525: end wenzelm@18525: | prv (tacs, trs, choices, wenzelm@18525: {pairs = ([],haz)::(Gs,haz')::pairs, lits, vars, lim} :: brs) = wenzelm@18525: (*no more "safe" formulae: transfer haz down a level*) wenzelm@18525: prv (tacs, trs, choices, wenzelm@18525: {pairs = (Gs,haz@haz')::pairs, wenzelm@18525: lits = lits, wenzelm@18525: vars = vars, wenzelm@18525: lim = lim} :: brs) wenzelm@18525: | prv (tacs, trs, choices, wenzelm@18525: brs0 as {pairs = [([], (H,md)::Hs)], wenzelm@18525: lits, vars, lim} :: brs) = wenzelm@18525: (*no safe steps possible at any level: apply a haz rule*) wenzelm@18525: let exception PRV (*backtrack to precisely this recursion!*) wenzelm@18525: val H = norm H wenzelm@18525: val ntrl = !ntrail wenzelm@24062: val rules = netMkRules thy H vars hazList wenzelm@18525: (*new premises of haz rules may NOT be duplicated*) wenzelm@18525: fun newPrem (vars,P,dup,lim') prem = wenzelm@18525: let val Gs' = map (fn Q => (Q,false)) prem wenzelm@18525: and Hs' = if dup then Hs @ [(negOfGoal H, md)] else Hs wenzelm@18525: and lits' = if (exists isGoal prem) wenzelm@18525: then map negOfGoal lits wenzelm@18525: else lits wenzelm@18525: in {pairs = if exists (match P) prem then [(Gs',Hs')] wenzelm@18525: (*Recursive in this premise. Don't make new wenzelm@18525: "stack frame". New haz premises will end up wenzelm@18525: at the BACK of the queue, preventing wenzelm@18525: exclusion of others*) wenzelm@18525: else [(Gs',[]), ([],Hs')], wenzelm@18525: lits = lits', wenzelm@18525: vars = vars, wenzelm@18525: lim = lim'} wenzelm@18525: end wenzelm@18525: fun newBr x prems = map (newPrem x) prems @ brs wenzelm@18525: (*Seek a matching rule. If unifiable then add new premises paulson@2854: to branch.*) wenzelm@18525: fun deeper [] = raise NEWBRANCHES wenzelm@18525: | deeper (((P,prems),tac)::grls) = wenzelm@24062: if unify state (add_term_vars(P,[]), P, H) wenzelm@18525: then wenzelm@18525: let val updated = ntrl < !ntrail (*branch updated*) wenzelm@18525: val vars = vars_in_vars vars wenzelm@30193: val vars' = List.foldr add_terms_vars vars prems wenzelm@18525: (*duplicate H if md permits*) wenzelm@18525: val dup = md (*earlier had "andalso vars' <> vars": paulson@11152: duplicate only if the subgoal has new vars*) wenzelm@18525: (*any instances of P in the subgoals? wenzelm@18525: NB: boolean "recur" affects tracing only!*) wenzelm@18525: and recur = exists (exists (match P)) prems wenzelm@18525: val lim' = (*Decrement "lim" extra if updates occur*) wenzelm@18525: if updated then lim - (1+log(length rules)) wenzelm@18525: else lim-1 wenzelm@18525: (*It is tempting to leave "lim" UNCHANGED if wenzelm@18525: both dup and recur are false. Proofs are wenzelm@18525: found at shallower depths, but looping wenzelm@18525: occurs too often...*) wenzelm@18525: val mayUndo = wenzelm@18525: (*Allowing backtracking from a rule application wenzelm@18525: if other matching rules exist, if the rule wenzelm@18525: updated variables, or if the rule did not wenzelm@18525: introduce new variables. This latter condition wenzelm@18525: means it is not a standard "gamma-rule" but wenzelm@18525: some other form of unsafe rule. Aim is to wenzelm@18525: emulate Fast_tac, which allows all unsafe steps wenzelm@18525: to be undone.*) wenzelm@18525: not(null grls) (*other rules to try?*) wenzelm@18525: orelse updated wenzelm@18525: orelse vars=vars' (*no new Vars?*) wenzelm@18525: val tac' = tac(updated, dup, true) wenzelm@18525: (*if recur then perhaps shouldn't call rotate_tac: new paulson@5463: formulae should be last, but that's WRONG if the new paulson@5463: formulae are Goals, since they remain in the first paulson@5463: position*) paulson@5463: wenzelm@18525: in wenzelm@18525: if lim'<0 andalso not (null prems) wenzelm@18525: then (*it's faster to kill ALL the alternatives*) wenzelm@18525: (traceMsg"Excessive branching: KILLED"; wenzelm@24062: clearTo state ntrl; raise NEWBRANCHES) wenzelm@18525: else wenzelm@18525: traceNew prems; wenzelm@22580: if !trace andalso dup then Output.immediate_output" (duplicating)" wenzelm@18525: else (); wenzelm@22580: if !trace andalso recur then Output.immediate_output" (recursive)" wenzelm@18525: else (); wenzelm@24062: traceVars state ntrl; wenzelm@18525: if null prems then nclosed := !nclosed + 1 wenzelm@18525: else ntried := !ntried + length prems - 1; wenzelm@18525: prv(tac' :: tacs, wenzelm@18525: brs0::trs, wenzelm@18525: (ntrl, length brs0, PRV) :: choices, wenzelm@18525: newBr (vars', P, dup, lim') prems) wenzelm@18525: handle PRV => wenzelm@18525: if mayUndo wenzelm@18525: then (*reset Vars and try another rule*) wenzelm@24062: (clearTo state ntrl; deeper grls) wenzelm@18525: else (*backtrack to previous level*) wenzelm@18525: backtrack choices wenzelm@18525: end wenzelm@18525: else deeper grls wenzelm@24062: in tracing state brs0; wenzelm@18525: if lim<1 then (traceMsg "Limit reached. "; backtrack choices) wenzelm@18525: else deeper rules wenzelm@18525: handle NEWBRANCHES => wenzelm@18525: (*cannot close branch: move H to literals*) wenzelm@18525: prv (tacs, brs0::trs, choices, wenzelm@18525: {pairs = [([], Hs)], wenzelm@18525: lits = H::lits, wenzelm@18525: vars = vars, wenzelm@18525: lim = lim} :: brs) wenzelm@18525: end paulson@2854: | prv (tacs, trs, choices, _ :: brs) = backtrack choices wenzelm@12346: in prv ([], [], [(!ntrail, length brs, PROVE)], brs) end; paulson@2854: paulson@2854: paulson@2883: (*Construct an initial branch.*) wenzelm@18525: fun initBranch (ts,lim) = paulson@5463: {pairs = [(map (fn t => (t,true)) ts, [])], wenzelm@18525: lits = [], wenzelm@18525: vars = add_terms_vars (ts,[]), paulson@5463: lim = lim}; paulson@2854: paulson@2854: paulson@2854: (*** Conversion & Skolemization of the Isabelle proof state ***) paulson@2854: paulson@2854: (*Make a list of all the parameters in a subgoal, even if nested*) wenzelm@18525: local open Term paulson@2854: in paulson@2854: fun discard_foralls (Const("all",_)$Abs(a,T,t)) = discard_foralls t paulson@2854: | discard_foralls t = t; paulson@2854: end; paulson@2854: paulson@2854: (*List of variables not appearing as arguments to the given parameter*) paulson@2854: fun getVars [] i = [] wenzelm@20664: | getVars ((_,(v,is))::alist) (i: int) = wenzelm@20664: if member (op =) is i then getVars alist i wenzelm@18525: else v :: getVars alist i; paulson@2854: paulson@4233: exception TRANS of string; paulson@2854: paulson@4233: (*Translation of a subgoal: Skolemize all parameters*) wenzelm@24062: fun fromSubgoal thy t = paulson@4065: let val alistVar = ref [] paulson@4065: and alistTVar = ref [] paulson@2854: fun hdvar ((ix,(v,is))::_) = v paulson@2854: fun from lev t = wenzelm@18525: let val (ht,ts) = Term.strip_comb t wenzelm@18525: fun apply u = list_comb (u, map (from lev) ts) wenzelm@18525: fun bounds [] = [] wenzelm@18525: | bounds (Term.Bound i::ts) = wenzelm@18525: if i apply (fromConst thy alistTVar aT) wenzelm@18525: | Term.Free (a,_) => apply (Free a) wenzelm@18525: | Term.Bound i => apply (Bound i) wenzelm@18525: | Term.Var (ix,_) => wenzelm@18525: (case (AList.lookup (op =) (!alistVar) ix) of wenzelm@18525: NONE => (alistVar := (ix, (ref NONE, bounds ts)) wenzelm@18525: :: !alistVar; wenzelm@18525: Var (hdvar(!alistVar))) wenzelm@18525: | SOME(v,is) => if is=bounds ts then Var v wenzelm@18525: else raise TRANS wenzelm@18525: ("Discrepancy among occurrences of " wenzelm@22678: ^ Term.string_of_vname ix)) wenzelm@18525: | Term.Abs (a,_,body) => wenzelm@18525: if null ts then Abs(a, from (lev+1) body) wenzelm@18525: else raise TRANS "argument not in normal form" paulson@2854: end paulson@2854: paulson@2854: val npars = length (Logic.strip_params t) paulson@2854: paulson@2854: (*Skolemize a subgoal from a proof state*) paulson@2854: fun skoSubgoal i t = wenzelm@18525: if i (writeln ("PROOF FAILED for depth " ^ wenzelm@18525: Int.toString lim); wenzelm@18525: if !trace then error "************************\n" wenzelm@18525: else (); wenzelm@18525: backtrack choices) wenzelm@18525: | cell => (if (!trace orelse !stats) wenzelm@30187: then writeln (#message (end_timing start) ^ " for reconstruction") wenzelm@18525: else (); wenzelm@18525: Seq.make(fn()=> cell)) paulson@4323: end wenzelm@24062: in prove (state, start, cs, [initBranch (mkGoal concl :: hyps, lim)], cont) end wenzelm@24062: handle PROVE => Seq.empty paulson@2854: paulson@4391: (*Public version with fixed depth*) wenzelm@21295: fun depth_tac cs lim i st = timing_depth_tac (start_timing ()) cs lim i st; paulson@4391: wenzelm@24112: val (depth_limit, setup_depth_limit) = Attrib.config_int_global "blast_depth_limit" 20; webertj@15162: wenzelm@18525: fun blast_tac cs i st = wenzelm@24112: ((DEEPEN (1, Config.get_thy (Thm.theory_of_thm st) depth_limit) wenzelm@24099: (timing_depth_tac (start_timing ()) cs) 0) i paulson@5463: THEN flexflex_tac) st paulson@14466: handle TRANS s => wenzelm@18525: ((if !trace then warning ("blast: " ^ s) else ()); paulson@14466: Seq.empty); paulson@2854: wenzelm@4078: fun Blast_tac i = blast_tac (Data.claset()) i; paulson@2854: paulson@2924: wenzelm@18525: (*** For debugging: these apply the prover to a subgoal and return paulson@2924: the resulting tactics, trace, etc. ***) paulson@2924: wenzelm@24062: val fullTrace = ref ([]: branch list list); paulson@2924: paulson@2924: (*Read a string to make an initial, singleton branch*) wenzelm@25365: fun readGoal thy s = Syntax.read_prop_global thy s |> fromTerm thy |> rand |> mkGoal; paulson@2924: wenzelm@18525: fun tryInThy thy lim s = wenzelm@24062: let wenzelm@24062: val state as State {fullTrace = ft, ...} = initialize thy; wenzelm@24062: val res = timeap prove wenzelm@24062: (state, start_timing(), Data.claset(), [initBranch ([readGoal thy s], lim)], I); wenzelm@24062: val _ = fullTrace := !ft; wenzelm@24062: in res end; paulson@2924: paulson@2924: wenzelm@5926: (** method setup **) wenzelm@5926: wenzelm@24099: val blast_method = wenzelm@27809: Method.bang_sectioned_args' Data.cla_modifiers (Scan.lift (Scan.option OuterParse.nat)) wenzelm@24099: (fn NONE => Data.cla_meth' blast_tac wenzelm@24099: | SOME lim => Data.cla_meth' (fn cs => depth_tac cs lim)); wenzelm@7155: wenzelm@18525: val setup = wenzelm@24099: setup_depth_limit #> wenzelm@24099: Method.add_methods [("blast", blast_method, "tableau prover")]; wenzelm@5926: paulson@2854: end;