Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Reasoning behind appearance of variables in is...

Email Gateway (Aug 18 2022 at 11:24):

From: Rafal Kolanski <rafalk@cse.unsw.edu.au>
Hello,

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.

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

Sincerely,

Rafal Kolanski.

Email Gateway (Aug 18 2022 at 11:24):

From: Makarius <makarius@sketis.net>
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

Last updated: Nov 21 2024 at 12:39 UTC