new version, more resistant to PROOF FAILED. Now it distinguishes between
inferences that update the branch (resolve_tac) and those that do not
(match_tac)
1.1 --- a/src/Provers/blast.ML Wed Aug 19 10:37:56 1998 +0200
1.2 +++ b/src/Provers/blast.ML Wed Aug 19 10:49:30 1998 +0200
1.3 @@ -24,16 +24,14 @@
1.4 "Recursive" chains of rules can sometimes exclude other unsafe formulae
1.5 from expansion. This happens because newly-created formulae always
1.6 have priority over existing ones. But obviously recursive rules
1.7 - such as transitivity are treated specially to prevent this.
1.8 + such as transitivity are treated specially to prevent this. Sometimes
1.9 + the formulae get into the wrong order (see WRONG below).
1.10
1.11 With overloading:
1.12 - Overloading can't follow all chains of type dependencies. Cannot
1.13 - prove "In1 x ~: Part A In0" because PartE introducees the polymorphic
1.14 - equality In1 x = In0 y, when the corresponding rule uses the (distinct)
1.15 - set equality. Workaround: supply a type instance of the rule that
1.16 - creates new equalities (e.g. PartE in HOL/ex/Simult)
1.17 - ==> affects freeness reasoning about Sexp constants (since they have
1.18 - type ... set)
1.19 + Calls to Blast.overloaded (see HOL/Set.ML for examples) are needed
1.20 + to tell Blast_tac when to retain some type information. Make sure
1.21 + you know the constant's internal name, which might be "op <=" or
1.22 + "Relation.op ^^".
1.23
1.24 With substition for equalities (hyp_subst_tac):
1.25 When substitution affects a haz formula or literal, it is moved
1.26 @@ -118,14 +116,14 @@
1.27 and stats = ref false; (*for runtime and search statistics*)
1.28
1.29 datatype term =
1.30 - Const of string
1.31 + Const of string
1.32 | TConst of string * term (*type of overloaded constant--as a term!*)
1.33 | Skolem of string * term option ref list
1.34 - | Free of string
1.35 - | Var of term option ref
1.36 - | Bound of int
1.37 - | Abs of string*term
1.38 - | op $ of term*term;
1.39 + | Free of string
1.40 + | Var of term option ref
1.41 + | Bound of int
1.42 + | Abs of string*term
1.43 + | $ of term*term;
1.44
1.45
1.46 (** Basic syntactic operations **)
1.47 @@ -482,12 +480,18 @@
1.48
1.49 fun TRACE rl tac st i = if !trace then (prth rl; tac st i) else tac st i;
1.50
1.51 -(*Tableau rule from elimination rule. Flag "dup" requests duplication of the
1.52 - affected formula.*)
1.53 +(*Resolution/matching tactics: if upd then the proof state may be updated.
1.54 + Matching makes the tactics more deterministic in the presence of Vars.*)
1.55 +fun emtac upd rl = TRACE rl (if upd then etac rl else ematch_tac [rl]);
1.56 +fun rmtac upd rl = TRACE rl (if upd then rtac rl else match_tac [rl]);
1.57 +
1.58 +(*Tableau rule from elimination rule.
1.59 + Flag "upd" says that the inference updated the branch.
1.60 + Flag "dup" requests duplication of the affected formula.*)
1.61 fun fromRule vars rl =
1.62 let val trl = rl |> rep_thm |> #prop |> fromTerm |> convertRule vars
1.63 - fun tac (dup,rot) i =
1.64 - TRACE rl (etac (if dup then rev_dup_elim rl else rl)) i
1.65 + fun tac (upd, dup,rot) i =
1.66 + emtac upd (if dup then rev_dup_elim rl else rl) i
1.67 THEN
1.68 rot_subgoals_tac (rot, #2 trl) i
1.69 in Option.SOME (trl, tac) end
1.70 @@ -508,12 +512,15 @@
1.71 in (mkGoal P, map (convertIntrPrem o skoPrem vars) Ps)
1.72 end;
1.73
1.74 -(*Tableau rule from introduction rule. Since haz rules are now delayed,
1.75 - "dup" is always FALSE for introduction rules.*)
1.76 +(*Tableau rule from introduction rule.
1.77 + Flag "upd" says that the inference updated the branch.
1.78 + Flag "dup" requests duplication of the affected formula.
1.79 + Since haz rules are now delayed, "dup" is always FALSE for
1.80 + introduction rules.*)
1.81 fun fromIntrRule vars rl =
1.82 let val trl = rl |> rep_thm |> #prop |> fromTerm |> convertIntrRule vars
1.83 - fun tac (dup,rot) i =
1.84 - TRACE rl (rtac (if dup then Data.dup_intr rl else rl)) i
1.85 + fun tac (upd,dup,rot) i =
1.86 + rmtac upd (if dup then Data.dup_intr rl else rl) i
1.87 THEN
1.88 rot_subgoals_tac (rot, #2 trl) i
1.89 in (trl, tac) end;
1.90 @@ -631,7 +638,7 @@
1.91 in if !trace then printBrs (map normBr brs) else ()
1.92 end;
1.93
1.94 -fun traceMsg s = if !trace then prs s else ();
1.95 +fun traceMsg s = if !trace then writeln s else ();
1.96
1.97 (*Tracing: variables updated in the last branch operation?*)
1.98 fun traceVars sign ntrl =
1.99 @@ -952,15 +959,15 @@
1.100 | deeper (((P,prems),tac)::grls) =
1.101 if unify(add_term_vars(P,[]), P, G)
1.102 then (*P comes from the rule; G comes from the branch.*)
1.103 - let val ntrl' = !ntrail
1.104 - val lim' = if ntrl < !ntrail
1.105 + let val updated = ntrl < !ntrail (*branch updated*)
1.106 + val lim' = if updated
1.107 then lim - (1+log(length rules))
1.108 else lim (*discourage branching updates*)
1.109 val vars = vars_in_vars vars
1.110 val vars' = foldr add_terms_vars (prems, vars)
1.111 val choices' = (ntrl, nbrs, PRV) :: choices
1.112 - val tacs' = (DETERM o tac(false,true)) :: tacs
1.113 - (*no duplication; rotate*)
1.114 + val tacs' = (DETERM o tac(updated,false,true))
1.115 + :: tacs (*no duplication; rotate*)
1.116 in
1.117 traceNew prems; traceVars sign ntrl;
1.118 (if null prems then (*closed the branch: prune!*)
1.119 @@ -970,15 +977,14 @@
1.120 brs))
1.121 else (*prems non-null*)
1.122 if lim'<0 (*faster to kill ALL the alternatives*)
1.123 - then (traceMsg"Excessive branching: KILLED\n";
1.124 + then (traceMsg"Excessive branching: KILLED";
1.125 clearTo ntrl; raise NEWBRANCHES)
1.126 else
1.127 (ntried := !ntried + length prems - 1;
1.128 prv(tacs', brs0::trs, choices',
1.129 newBr (vars',lim') prems)))
1.130 handle PRV =>
1.131 - if ntrl < ntrl' (*Vars have been updated*)
1.132 - then
1.133 + if updated then
1.134 (*Backtrack at this level.
1.135 Reset Vars and try another rule*)
1.136 (clearTo ntrl; deeper grls)
1.137 @@ -1069,7 +1075,7 @@
1.138 | deeper (((P,prems),tac)::grls) =
1.139 if unify(add_term_vars(P,[]), P, H)
1.140 then
1.141 - let val ntrl' = !ntrail
1.142 + let val updated = ntrl < !ntrail (*branch updated*)
1.143 val vars = vars_in_vars vars
1.144 val vars' = foldr add_terms_vars (prems, vars)
1.145 (*duplicate H if md and the subgoal has new vars*)
1.146 @@ -1077,7 +1083,7 @@
1.147 (*any instances of P in the subgoals?*)
1.148 and recur = exists (exists (match P)) prems
1.149 val lim' = (*Decrement "lim" extra if updates occur*)
1.150 - if ntrl < !ntrail then lim - (1+log(length rules))
1.151 + if updated then lim - (1+log(length rules))
1.152 else lim-1
1.153 (*It is tempting to leave "lim" UNCHANGED if
1.154 both dup and recur are false. Proofs are
1.155 @@ -1093,16 +1099,18 @@
1.156 emulate Fast_tac, which allows all unsafe steps
1.157 to be undone.*)
1.158 not(null grls) (*other rules to try?*)
1.159 - orelse ntrl < ntrl' (*variables updated?*)
1.160 + orelse updated
1.161 orelse vars=vars' (*no new Vars?*)
1.162 - val tac' = if mayUndo then tac(dup, true)
1.163 - else DETERM o tac(dup, true)
1.164 + val tac' = if mayUndo then tac(updated, dup, true)
1.165 + else DETERM o tac(updated, dup, true)
1.166 (*if recur then doesn't call rotate_tac:
1.167 - new formulae should be last*)
1.168 + new formulae should be last; WRONG
1.169 + if the new formulae are Goals, since
1.170 + they remain in the first position*)
1.171 in
1.172 if lim'<0 andalso not (null prems)
1.173 then (*it's faster to kill ALL the alternatives*)
1.174 - (traceMsg"Excessive branching: KILLED\n";
1.175 + (traceMsg"Excessive branching: KILLED";
1.176 clearTo ntrl; raise NEWBRANCHES)
1.177 else
1.178 traceNew prems;
1.179 @@ -1281,4 +1289,3 @@
1.180
1.181
1.182 end;
1.183 -