Re: [isabelle] Reasoning behind appearance of variables in isar cases?
On Wed, 20 Feb 2008, Rafal Kolanski wrote:
> 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.
First of all note that the induction proof really needs to refer to
locally fresh variables in the body. Your proof can be spelled out more
explicitly as follows:
fixes xs :: "'a list"
shows "P xs"
proof (induct xs)
show "P Nil" sorry
fix y ys
assume "P ys"
show "P (Cons y ys)" sorry
The choice of names is up to you, it is convenient to re-use some names
from the original statement, but the internal logic is still the same.
In particular, using x and xs here makes the system invent an internal
(brown) xsa, to avoid a clash with the initial (fixed) xs.
For historical reasons, goal display uses the internal names of the raw
logic, not the terminology of the Isar text. This makes it indeed hard to
paste text from the goal state back into the source. (At some later
stage, the print layer might get smart enough to perform the trick.)
To avoid such inconveniences right now you can either use completely
different bound names (as y and ys above), or try to avoid pasting from
low-level goal state in the first place. This can be achieved to some
degree by referring to symbolic facts and goals produced by the ``cases''
infrastructure (see also the print_cases command), maybe also with some
additional term abbreviation derived from the original statement (using
This archive was generated by a fusion of
Pipermail (Mailman edition) and