Email Gateway (Aug 18 2022 at 19:03): Email Gateway (Aug 18 2022 at 19:03):From: "Matthews, John R" <john.r.matthews@intel.com>
Hi,
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:
theory NoSuchVar
imports Main
begin
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 *}
end
Could this behavior be changed such that the error is reported only when a variable occurs in none of the theorems?
I'm using Isabelle2011-1.
Thanks,
John
Email Gateway (Aug 18 2022 at 19:08):From: Makarius <makarius@sketis.net>
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 autolemmas 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
Email Gateway (Aug 18 2022 at 19:10):From: "Matthews, John R" <john.r.matthews@intel.com>
Ah, I'd forgotten about no_vars. Thanks.
John
-----Original Message-----
From: Makarius [mailto:makarius@sketis.net]
Sent: Wednesday, February 15, 2012 3:06 AM
To: Matthews, John R
Cc: isabelle-users@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 autolemmas 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
Last updated: Apr 23 2024 at 04:18 UTC