Re: [isabelle] case command and internal names
On Wed, 5 Mar 2014, Lars Noschinski wrote:
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?
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and