# HG changeset patch # User paulson # Date 860146108 -7200 # Node ID d2ffee4f811bc9fa29525c2fc2668b941f4f66e1 # Parent 2ee005e46d6d248cff19fbbe5be489934bb180bd Re-organization of the order of haz rules diff -r 2ee005e46d6d -r d2ffee4f811b src/Provers/blast.ML --- a/src/Provers/blast.ML Fri Apr 04 11:27:02 1997 +0200 +++ b/src/Provers/blast.ML Fri Apr 04 11:28:28 1997 +0200 @@ -1,16 +1,32 @@ -(* ID: $Id$ -use "/homes/lcp/Isa/new/blast.ML"; +(* Title: Provers/blast + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1992 University of Cambridge + +Generic tableau prover with proof reconstruction + SKOLEMIZES ReplaceI WRONGLY: allow new vars in prems, or forbid such rules?? - Needs explicit instantiation of assumptions? (#55 takes 32s) + Needs explicit instantiation of assumptions? + + +Limitations compared with fast_tac: + * ignores addss, addbefore, addafter; this restriction is intrinsic + * seems to loop given transitivity and similar rules + * ignores elimination rules that don't have the correct format + (conclusion must be a formula variable) + * ignores types, which can make HOL proofs fail + +Known problems: + With hyp_subst_tac: + 1. Sometimes hyp_subst_tac will fail due to occurrence of the parameter + as the argument of a function variable + 2. When a literal is affected, it is moved back to the active formulae. + But there's no way of putting it in the right place. + 3. Affected haz formulae should also be moved, but they are not. *) -proof_timing:=true; -print_depth 20; - -structure List = List_; - (*Should be a type abbreviation?*) type netpair = (int*(bool*thm)) Net.net * (int*(bool*thm)) Net.net; @@ -533,30 +549,30 @@ | _ => raise DEST_EQ; -(*Convert a Goal to an ordinary Not. Used also in dup_intr, where a goal like - Ex(P) is duplicated as the assumption ~Ex(P). *) -fun negOfGoal (Const"*Goal*" $ G, md) = (negate G, md) - | negOfGoal G = G; - -(*Substitute through the branch if an equality goal (else raise DEST_EQ)*) -fun equalSubst (G, br, hazs, lits, vars, lim) = +(*Substitute through the branch if an equality goal (else raise DEST_EQ). + Moves affected literals back into the branch, but it is not clear where + they should go: this could make proofs fail. ??? *) +fun equalSubst (G, pairs, lits, vars, lim) = let val subst = subst_atomic (orientGoal(dest_eq G)) fun subst2(G,md) = (subst G, md) - fun subLits ([], br, nlits) = - (br, map (map subst2) hazs, nlits, vars, lim) - | subLits (lit::lits, br, nlits) = + val pairs' = map (fn(Gs,Hs) => (map subst2 Gs, map subst2 Hs)) pairs + (*substitute throughout literals and note those affected*) + fun subLits ([], [], nlits) = (pairs', nlits, vars, lim) + | subLits ([], Gs, nlits) = ((Gs,[])::pairs', nlits, vars, lim) + | subLits (lit::lits, Gs, nlits) = let val nlit = subst lit - in if nlit aconv lit then subLits (lits, br, nlit::nlits) - else subLits (lits, (nlit,true)::br, nlits) + in if nlit aconv lit then subLits (lits, Gs, nlit::nlits) + else subLits (lits, (nlit,true)::Gs, nlits) end - in subLits (rev lits, map subst2 br, []) + in subLits (rev lits, [], []) end; exception NEWBRANCHES and CLOSEF; -type branch = (term*bool) list * (*pending formulae with md flags*) - (term*bool) list list * (*stack of haz formulae*) +(*Pending formulae carry md (may duplicate) flags*) +type branch = ((term*bool) list * (*safe formulae on this level*) + (term*bool) list) list * (*haz formulae on this level*) term list * (*literals: irreducible formulae*) term option ref list * (*variables occurring in branch*) int; (*resource limit*) @@ -578,20 +594,6 @@ | tryClose _ = raise UNIFY; -(*hazs is a list of lists of unsafe formulae. This "stack" keeps them - in the right relative order: they must go after *all* safe formulae, - with newly introduced ones coming before older ones.*) - -(*Add an empty "stack frame" unless there's already one there*) -fun nilHaz hazs = - case hazs of []::_ => hazs - | _ => []::hazs; - -fun addHaz (G, haz::hazs) = (haz@[negOfGoal G]) :: hazs; - -(*Convert *Goal* to negated assumption in FIRST position*) -val negOfGoal_tac = rtac Data.ccontr THEN' rotate_tac ~1; - (*Were there Skolem terms in the premise? Must NOT chase Vars*) fun hasSkolem (Skolem _) = true | hasSkolem (Abs (_,body)) = hasSkolem body @@ -603,10 +605,21 @@ fun joinMd md [] = [] | joinMd md (G::Gs) = (G, hasSkolem G orelse md) :: joinMd md Gs; -(*Join new formulae to a branch.*) -fun appendBr md (ts,us) = - if (exists isGoal ts) then joinMd md ts @ map negOfGoal us - else joinMd md ts @ us; +(*Convert a Goal to an ordinary Not. Used also in dup_intr, where a goal like + Ex(P) is duplicated as the assumption ~Ex(P). *) +fun negOfGoal (Const"*Goal*" $ G) = negate G + | negOfGoal G = G; + +fun negOfGoal2 (G,md) = (negOfGoal G, md); + +(*Converts all Goals to Nots in the safe parts of a branch. They could + have been moved there from the literals list after substitution (equalSubst). + There can be at most one--this function could be made more efficient.*) +fun negOfGoals pairs = map (fn (Gs,haz) => (map negOfGoal2 Gs, haz)) pairs; + +(*Tactic. Convert *Goal* to negated assumption in FIRST position*) +val negOfGoal_tac = rtac Data.ccontr THEN' rotate_tac ~1; + (** Backtracking and Pruning **) @@ -646,14 +659,15 @@ choices) in traceIt (pruneAux (choices, !ntrail, !trail, choices)) end; -fun nextVars ((br, hazs, lits, vars, lim) :: _) = map Var vars +fun nextVars ((br, lits, vars, lim) :: _) = map Var vars | nextVars [] = []; fun backtrack ((_, _, exn)::_) = raise exn | backtrack _ = raise PROVE; -(*Change all *Goal* literals to Not. Also delete all those identical to G.*) -fun addLit (Const "*Goal*" $ G,lits) = +(*Add the literal G, handling *Goal* and detecting duplicates.*) +fun addLit (Const "*Goal*" $ G, lits) = + (*New literal is a *Goal*, so change all other Goals to Nots*) let fun bad (Const"*Goal*" $ _) = true | bad (Const"Not" $ G') = G aconv G' | bad _ = false; @@ -680,18 +694,22 @@ and hazList = [haz_netpair] fun prv (tacs, trs, choices, []) = (cont (trs,choices,tacs)) | prv (tacs, trs, choices, - brs0 as ((G,md)::br, hazs, lits, vars, lim) :: brs) = + brs0 as (((G,md)::br, haz)::pairs, lits, vars, lim) :: brs) = let exception PRV (*backtrack to precisely this recursion!*) val ntrl = !ntrail val nbrs = length brs0 val nxtVars = nextVars brs val G = norm G (*Make a new branch, decrementing "lim" if instantiations occur*) - fun newBr vars prems = - map (fn prem => (appendBr md (prem, br), - nilHaz hazs, lits, - add_terms_vars (prem,vars), - if ntrl < !ntrail then lim-3 else lim)) + fun newBr (vars',lim') prems = + map (fn prem => + if (exists isGoal prem) + then (((joinMd md prem, []) :: + negOfGoals ((br, haz)::pairs)), + map negOfGoal lits, + vars', lim') + else (((joinMd md prem, []) :: (br, haz) :: pairs), + lits, vars', lim')) prems @ brs (*Seek a matching rule. If unifiable then add new premises @@ -701,6 +719,9 @@ let val dummy = unify(add_term_vars(P,[]), P, G) (*P comes from the rule; G comes from the branch.*) val ntrl' = !ntrail + val lim' = if ntrl < !ntrail then lim-3 else lim + val vars = vars_in_vars vars + val vars' = foldr add_terms_vars (prems, vars) val choices' = (ntrl, nbrs, PRV) :: choices in if null prems then (*closed the branch: prune!*) @@ -714,7 +735,7 @@ else prv(tac false :: tacs, (*no duplication*) brs0::trs, choices', - newBr (vars_in_vars vars) prems) + newBr (vars',lim') prems) handle PRV => if ntrl < ntrl' then (*Vars have been updated: must backtrack @@ -738,42 +759,48 @@ (clearTo ntrl; closeF Ls) end handle UNIFY => closeF Ls + fun closeFl [] = raise CLOSEF + | closeFl ((br, haz)::pairs) = + closeF (map fst br) + handle CLOSEF => closeF (map fst haz) + handle CLOSEF => closeFl pairs in if !trace then fullTrace := brs0 :: !fullTrace else (); if lim<0 then backtrack choices else prv (Data.vars_gen_hyp_subst_tac false :: tacs, brs0::trs, choices, - equalSubst (G, br, hazs, lits, vars, lim) :: brs) + equalSubst (G, (br,haz)::pairs, lits, vars, lim) :: brs) handle DEST_EQ => closeF lits - handle CLOSEF => closeF (map #1 br) - handle CLOSEF => closeF (map #1 (List.concat hazs)) + handle CLOSEF => closeFl ((br,haz)::pairs) handle CLOSEF => - (deeper (netMkRules G vars safeList) - handle NEWBRANCHES => - (case netMkRules G vars hazList of - [] => (*no plausible rules: move G to literals*) - prv (tacs, brs0::trs, choices, - (br, hazs, addLit(G,lits), vars, lim)::brs) - | _ => (*G admits some haz rules: try later*) - prv (if isGoal G then negOfGoal_tac :: tacs - else tacs, - brs0::trs, choices, - (br, addHaz((G,md),hazs), lits, vars, lim) - ::brs))) + deeper (netMkRules G vars safeList) + handle NEWBRANCHES => + (case netMkRules G vars hazList of + [] => (*no plausible rules: move G to literals*) + prv (tacs, brs0::trs, choices, + ((br,haz)::pairs, addLit(G,lits), vars, lim) + ::brs) + | _ => (*G admits some haz rules: try later*) + prv (if isGoal G then negOfGoal_tac :: tacs + else tacs, + brs0::trs, choices, + ((br, haz@[(negOfGoal G, md)])::pairs, + lits, vars, lim) :: brs)) end - | prv (tacs, trs, choices, ([], []::hazs, lits, vars, lim) :: brs) = - (*removal of empty list from hazs*) - prv (tacs, trs, choices, ([], hazs, lits, vars, lim) :: brs) + | prv (tacs, trs, choices, (([],haz)::(Gs,haz')::pairs, + lits, vars, lim) :: brs) = + (*no more "safe" formulae: transfer haz down a level*) + prv (tacs, trs, choices, ((Gs,haz@haz')::pairs, lits, vars, lim) + :: brs) | prv (tacs, trs, choices, - brs0 as ([], ((G,md)::Gs)::hazs, lits, vars, lim) :: brs) = - (*application of haz rule*) + brs0 as ([([], (H,md)::Hs)], lits, vars, lim) :: brs) = + (*no safe steps possible at any level: apply a haz rule*) let exception PRV (*backtrack to precisely this recursion!*) - val G = norm G + val H = norm H val ntrl = !ntrail fun newPrem (vars,dup) prem = - (map (fn P => (P,false)) prem, - nilHaz (if dup then Gs :: hazs @ [[negOfGoal (G,md)]] - else Gs :: hazs), + ([(map (fn P => (P,false)) prem, []), (*may NOT duplicate*) + ([], if dup then Hs @ [(negOfGoal H, md)] else Hs)], lits, vars, (*Decrement "lim" if instantiations occur or the @@ -785,12 +812,12 @@ to branch.*) fun deeper [] = raise NEWBRANCHES | deeper (((P,prems),tac)::grls) = - let val dummy = unify(add_term_vars(P,[]), P, G) + let val dummy = unify(add_term_vars(P,[]), P, H) val ntrl' = !ntrail val vars = vars_in_vars vars val vars' = foldr add_terms_vars (prems, vars) val dup = md andalso vars' <> vars - (*duplicate G only if md and the premise has new vars*) + (*duplicate H only if md and the premise has new vars*) in prv(tac dup :: tacs, brs0::trs, @@ -808,11 +835,11 @@ in if !trace then fullTrace := brs0 :: !fullTrace else (); if lim<1 then backtrack choices else - deeper (netMkRules G vars hazList) + deeper (netMkRules H vars hazList) handle NEWBRANCHES => - (*cannot close branch: move G to literals*) + (*cannot close branch: move H to literals*) prv (tacs, brs0::trs, choices, - ([], Gs::hazs, G::lits, vars, lim)::brs) + ([([], Hs)], H::lits, vars, lim)::brs) end | prv (tacs, trs, choices, _ :: brs) = backtrack choices in prv ([], [], [(!ntrail, length brs, PROVE)], brs) end; @@ -820,8 +847,8 @@ (*Construct an initial branch.*) fun initBranch (ts,lim) = - (map (fn t => (t,true)) ts, - [[]], [], add_terms_vars (ts,[]), lim); + ([(map (fn t => (t,true)) ts, [])], + [], add_terms_vars (ts,[]), lim); (*** Conversion & Skolemization of the Isabelle proof state ***)