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? _______________________________________________ Isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
