# HG changeset patch # User paulson # Date 982326547 -3600 # Node ID 32d002362005d63728c24ca68da14a39f339fbe5 # Parent 4042eb2fde2f1f65a5a70fcc5c80dbea1c38ba40 Blast bug fix: now always duplicates when applying a haz rule, whether or not new variables are added. Can now prove theorems such as these: val prems = Goal "[|P==>Q; P==>~Q|] ==> ~P"; by (blast_tac (claset() addDs prems) 1); val prems = Goal "[|Q==>P; ~Q==>P|] ==> P"; by (blast_tac (claset() addIs prems) 1); diff -r 4042eb2fde2f -r 32d002362005 src/Provers/blast.ML --- a/src/Provers/blast.ML Fri Feb 16 13:27:56 2001 +0100 +++ b/src/Provers/blast.ML Fri Feb 16 13:29:07 2001 +0100 @@ -575,10 +575,6 @@ nps) in List.mapPartial (fromRule vars o #2) (orderlist elims) end; -(** -end; -**) - (*Pending formulae carry md (may duplicate) flags*) type branch = @@ -1042,6 +1038,7 @@ [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) @@ -1122,10 +1119,11 @@ let val updated = ntrl < !ntrail (*branch updated*) val vars = vars_in_vars vars val vars' = foldr add_terms_vars (prems, vars) - (*duplicate H if md and the subgoal has new vars*) - val dup = md andalso vars' <> vars + (*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: this boolean affects tracing only!*) + 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)) @@ -1159,6 +1157,8 @@ clearTo ntrl; raise NEWBRANCHES) else traceNew prems; + if !trace andalso dup then prs" (duplicating)" + else (); if !trace andalso recur then prs" (recursive)" else (); traceVars sign ntrl; @@ -1345,12 +1345,14 @@ (** method setup **) fun blast_args m = - Method.bang_sectioned_args' Data.cla_modifiers (Scan.lift (Scan.option Args.nat)) m; + 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 = [Method.add_methods [("blast", blast_args blast_meth, + "tableau prover")]]; end;