[isabelle-dev] [isabelle] safe for boolean equality

[Lawrence Paulson]

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.
Larry

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:
> 
> lemma
>  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?