[isabelle-dev] [isabelle] safe for boolean equality
lp15 at cam.ac.uk
Tue Jun 15 15:20:30 CEST 2010
If there is an easy way to identify free variables that are constrained externally, then such a change would be beneficial. Failing that, the particular case of locales is particularly necessary to handle correctly.
On 15 Jun 2010, at 14:17, Brian Huffman wrote:
> Note that testing whether a variable is a locale constant is not
> sufficient. The same problem occurs with structured Isar proofs, even
> without locales:
> assumes "xs = "
> shows "xs = ys ==> ys = "
> apply safe
> (* goal "ys = " is now unsolvable *)
> The real test for a free variable must be, "Does the proof context
> contain any assumptions involving this variable?" If the answer is no,
> then it is safe to eliminate the equality. If the answer is yes, then
> the equality must be kept in the assumptions. (It could be tried again
> with the opposite orientation, though; in my example above, unfolding
> "xs = ys" is unsafe, but unfolding "ys = xs" would be OK.)
> I'm not sure how to implement this test on the proof context, but I
> suspect that the code already exists -- doing a forall-introduction on
> a theorem involves the same kind of check, doesn't it?
More information about the isabelle-dev