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

Brian Huffman brianh at cs.pdx.edu
Tue Jun 15 15:17:05 CEST 2010

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:

  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

More information about the isabelle-dev mailing list