summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Wed, 03 Dec 1997 11:42:45 +0100 | |

changeset 4354 | 7f4da01bdf0e |

parent 4353 | d565d2197a5f |

child 4355 | 68c7c544570c |

Fixed the treatment of substitution for equations, restricting occurrences of
variables on the RHS. Improves performance in many cases, though a few old
proofs fail

--- a/src/Provers/blast.ML Wed Dec 03 11:00:24 1997 +0100 +++ b/src/Provers/blast.ML Wed Dec 03 11:42:45 1997 +0100 @@ -678,14 +678,21 @@ Prefer to eliminate Bound variables if possible. Result: true = use as is, false = reorient first *) -(*Does t occur in u? For substitution. - Does NOT check args of Skolem terms: substitution does not affect them. +(*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 fun occEq u = (t aconv u) orelse occ u - and occ (Var(ref None)) = false - | occ (Var(ref(Some u))) = occEq u - | occ (Abs(_,u)) = occEq u + 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).*) + 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 (f$u) = occEq u orelse occEq f | occ (_) = false; in occEq end; @@ -989,10 +996,7 @@ in tracing sign brs0; if lim<0 then (traceMsg "Limit reached. "; backtrack choices) else - prv ((TRY o Data.vars_gen_hyp_subst_tac false) :: tacs, - (*The TRY above allows the substitution to fail, e.g. if - the real version is z = f(?x z). Rest of proof might - still succeed!*) + prv (Data.vars_gen_hyp_subst_tac false :: tacs, brs0::trs, choices, equalSubst sign (G, (br,haz)::pairs, lits, vars, lim) :: brs) handle DEST_EQ => closeF lits