Email Gateway (Aug 19 2022 at 13:58): Email Gateway (Aug 19 2022 at 13:58):From: Lars Noschinski <noschinl@in.tum.de>
Hi everyone,
I just noticed that the "case" command allows the user to give internal
names to variables, i.e.
lemma "P (n :: nat)"
proof (induct n)
case (Suc m_)
does not give an error. As the similar "fix m_" fails with
Illegal reference to internal variable: "m_"
I wonder whether this is just an oversight?
-- Lars
Email Gateway (Aug 19 2022 at 14:54):From: Makarius <makarius@sketis.net>
It is an oversight from a very long time ago. When I discovered that
about 10 years ago, there were some proofs exploiting that omission of the
check, and for some odd reasons the variables could not just be renamed
without breaking the proofs.
I've checked the situation again just today: no such oddities are left in
the visible universe of Isabelle applications: the main repository + AFP.
So the coming release will have a proper check for 'case', just like for
'fix', 'fixes' or similar.
Makarius
Last updated: Apr 19 2024 at 16:20 UTC