Stream: Archive Mirror: Isabelle Users Mailing List

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

Email Gateway (Aug 18 2022 at 10:15):

From: Peter Lammich <peter.lammich@uni-muenster.de>
In the following example:
locale A =
fixes X
defines "X==[1::nat]"

lemma (in A) test: "[] ~= X"
apply safe

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 ?

Thanks in advance for any help
-- Peter Lammich

Email Gateway (Aug 18 2022 at 10:15):

From: Lawrence Paulson <lp15@cam.ac.uk>
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

Last updated: Nov 21 2024 at 12:39 UTC