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

[Brian Huffman]

On Tue, Jun 15, 2010 at 2:03 AM, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
> Altering the behaviour of the safe method on locale constants might be feasible, because it would affect only a few proofs. Can anybody tell me whether there is an easy way to identify whether a free variable is actually a locale constant?

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?

- Brian