*To*: Rafal Kolanski <rafalk at cse.unsw.edu.au>*Subject*: Re: [isabelle] Reasoning behind appearance of variables in isar cases?*From*: Makarius <makarius at sketis.net>*Date*: Wed, 20 Feb 2008 17:26:57 +0100 (CET)*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <47BBC1FF.9020306@cse.unsw.edu.au>*References*: <47BBC1FF.9020306@cse.unsw.edu.au>

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

**References**:**[isabelle] Reasoning behind appearance of variables in isar cases?***From:*Rafal Kolanski

- Previous by Date: [isabelle] LSFA 2008 - First call for papers
- Next by Date: Re: [isabelle] antiquotations
- Previous by Thread: [isabelle] Reasoning behind appearance of variables in isar cases?
- Next by Thread: [isabelle] LSFA 2008 - First call for papers
- Cl-isabelle-users February 2008 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list