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
> next
>   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:

lemma
  fixes xs :: "'a list"
  shows "P xs"
proof (induct xs)
  show "P Nil" sorry
next
  fix y ys
  assume "P ys"
  show "P (Cons y ys)" sorry
qed

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 
"is" patterns).


	Makarius






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