Re: [isabelle] auto and safe with defined variables in locales



At the moment, any assumption like []=X is deleted after replacing X by []. As you've noticed, that isn't helpful if constrained by a locale. We could investigate whether anything can be done about it.

Larry


On 26 Feb 2007, at 09:28, Peter Lammich wrote:

The subgoal presented to me is: False.
I expected something like:  [] = X ==> False, but I get just False.
The same is with auto. The reason seems to be the defined variable X of
the locale.
In some more complex proofs, this forces me to very often fold/unfold
symbol definitions in my locales (to prevent auto or safe making such
transformations), and this makes the proof scripts more confusing.
Is this behaviour of safe and auto the intended one ?
Is there any workaround to use a defined variable like X, but prevent
safe/auto from making such steps ?






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.