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.


	Makarius





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