Re: [isabelle] No such variable



Ah, I'd forgotten about no_vars. Thanks.

John

-----Original Message-----
From: Makarius [mailto:makarius at sketis.net] 
Sent: Wednesday, February 15, 2012 3:06 AM
To: Matthews, John R
Cc: isabelle-users at cl.cam.ac.uk
Subject: Re: [isabelle] No such variable

On Mon, 30 Jan 2012, Matthews, John R wrote:

> I have a small feature request: I have a large list of theorems that 
> I'm giving to blast. To simplify blast's search space, I want to fix 
> all of the variables in my theorem list. However, some of the theorems 
> contain only a proper subset of the variables I'm fixing. This causes 
> Isabelle to report a "no such variable" error, even though all of the 
> variables I'm fixing occur in at least one of the theorems.
>
>
> Below is a simplified example of the error I'm hitting:

> lemma L1: "x = x" by auto
> lemma L2: "y = y" by auto
>
> lemmas both = L1 L2
>
> thm both[where x=x and y=y] -- {* reports "no such variable" error *}
>

> Could this behavior be changed such that the error is reported only 
> when a variable occurs in none of the theorems?

Unfortunately not.  The fact notation with attribute application is structurally decomposed such that each attribute sees only a single thm as its argument.  This was done consciously many years ago to keep things as simple as possible (which was only partly successful, because attributes turned out quite complex nonetheless).


>From the above explanation it is not fully clear what you are trying to do.  Seen in isolation, the "fixing" of schematic variables can be done as in the "no_vars" attribute, see also
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2011-1/src/Pure/Isar/attrib.ML#l288

Note that no_vars is a bit odd in introducing locally fixed variables, without propagating the extended context.  This results in undeclared frees occurring in the resulting theorem.  The Prover IDE (even Proof
General) prints those with a warning color markup, but the main use of no_vars is for LaTeX documents.


You can easily make your own attribute along the same lines.  But I can't say on the spot what happens when you do propagate the extended context with the new fixes declared.  In all these years the question was left open if attributes are allowed to change the "axiomatic basis" 
(fixes/assumes) of the context; some advanced locale interpretation stuff might fail if that is done.


 	Makarius





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