[isabelle] Reasoning behind appearance of variables in isar cases?


I am confused as to why Isabelle displays different variables than their actual names in some cases. For instance:

lemma "P (xs::'a list)"
proof (induct xs)
  case Nil
  thus ?case sorry
  case (Cons x xs)
  hence "P xs" .

Note how I write "Cons x xs" and "P xs" but Isabelle keeps displaying xsa. With complicated induction proofs this makes it hard to keep track of what exactly the variables are called. It doesn't prevent shadowing because when I write "xs" I don't get the blue xs from the original statement. Also, when copying a subgoal or parts thereof to a new "have" or "lemma" statement to prove them separately, I have to go through and convert every "<var>a" to "<var>". This is cumbersome.

Why does this happen, and is there a way to turn this behaviour off?


Rafal Kolanski.

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