# 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.*