On 08/23/2010 12:30 PM, Thomas Sewell wrote:
Hello again isabelle-dev.
I should clear up some confusion that may have been caused by my mail. I was
trying to avoid repeating all that had been said on this issue, and it seems I
left out some that hadn't been said as well.
This approach avoids ever deleting an equality on a Free variable during a
'safe' reasoning step. It will substitute with that equality but keep it in
place. This is a significant change to the intermediate state of some tactic
scripts, thus the incompatibilities, especially on induction. It is somewhat
surprising there aren't more such incompatibilities. There's no truly safe way
to delete an equality on a Free variable without inspecting the whole context.
Naive questions:
* why is inspecting the whole context infeasible?
* why can't we just collect (and cache?) the Frees occuring in
assumptions managed
by assumption.ML and never delete equalities involving them?
Since equalities are not deleted, care must be taken to avoid an infinite loop
in which a substitution is repeatedly attempted. This is the reason for the
uniqueness check - if x appears only in 'x = expr' then there is no more
substitution to be done. Some subtleties were discovered experimentally:
- 'x = y' should not be substituted if either x or y is unique, or else we enter a
loop substituting x -> y -> x
- 'expr = x' needs to be reoriented when it is substituted, or else hypsubst
and simp will loop doing opposite substitutions.
- 'x = y' is OK to substitute if y is a unique free and x is a non-unique
Bound.
This is what is meant by a 'useful' substitution in the comment. Other
equalities, which would cause a no-effect or cyclic substitution, are referred
to as trivial (abbreviated triv) in this code. The language should probably be
cleanup up to use a consistent set of names.
Sounds complicated, but cool.
You adapted blast_hyp_subst_tac in that way too, right?
The subtlety here is that blast tries to approximate the effect of that
tactic
in the search and has accuracy problems even now. The more complicated
the substitution criterion, the more weirdness is induced here.
With the current situation before the patch, the accuracy problems can be
fully repaired it seems; what works best for blast is a simple criterion of
substitutability which is decidable from the hyp (and possibly
information that
stays constant in the whole search) only.
Let me address Alex's detailed comments:
1. In the HOL sources the algebra method is used to solve two problems about
parity essentially by accident. No Groebner bases were involved, but the
surrouding logic, which appeals to clarify_tac and a custom simpset, happened
to solve the goal. With this change the simplified goal had an extra quantifier
in it. Note that with this change terminal tactics operating in 'unsafe' mode -
fast, best, etc - will call thin_triv_tac via Context_Rules and behave
similarly to before. It is terminal tactics which take safe steps - like
algebra - that are most likely to break.
2. Yes, count vars is a bit strange, as it will consider "(%f. f) (%x. x)" to
contain two copies of Bound -1. The point is to count loose Bounds in the hypotheses as
returned by Logic.strip_assums_hyp, which it gets right.
Yours,
Thomas.
_______________________________________________
Isabelle-dev mailing list
Isabelle-dev@mailbroy.informatik.tu-muenchen.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
