Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Attributes use wrong context in lemma statement

Email Gateway (Aug 19 2022 at 13:21):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear experts of contexts,

I would like to report the following annoying behaviour (bug?) in Isabelle2013-2 and a
recent version of repository (761e40ce91bc). When I use the THEN attribute to transform a
proved lemma in an auxiliary context, I cannot refer to theorems imported by local
interpretations. My guess is that attributes in lemma statements somehow use a wrong context.

Below is a minimal example with THEN, but the same error also occurs for other attributes
like unfolded. In my use case, I prove a statement in a simple form and then automatically
transform it into a usable form by composing it with a lemma that I get from a local
interpretation. It would be great if I could do this directly at the lemma statement.

theory Scratch imports Main begin

locale l begin
lemma foo: "A ==> A" .
end

context begin
interpretation e!: l .

thm e.foo (* works *)
thm TrueI[THEN e.foo] (* works *)

lemmas bar1 = TrueI[THEN e.foo] (* works *)
lemmas bar2[THEN e.foo] = TrueI (* works *)

lemma bar [THEN e.foo]: "True" by simp (* does not work: Unknown fact "e.foo" *)
end

end

Best,
Andreas

Email Gateway (Aug 19 2022 at 13:41):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Andreas,

I guess there is a conceptual problem here: since attribute ingredients
must all be subject to morphism application, it is not possible to
reference facts which are only present in the hypothetical context since
these have no counterpart in the deeper layers of the target context stack.

This would definitely deserve hints in the documentation.

Cheers,
Florian
signature.asc

Email Gateway (Aug 19 2022 at 13:41):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Florian,

Thanks for the explanation, but I am afraid that I don't see the point you are trying to
make. If attribute ingredients are to work under morphisms, I would expect that the same
restrictions apply for using attribute with lemmas and with lemma. However, it works with
lemmas, but not with lemma. What makes the difference?

Andreas

Email Gateway (Aug 19 2022 at 14:00):

From: Makarius <makarius@sketis.net>
On Mon, 27 Jan 2014, Andreas Lochbihler wrote:

I would like to report the following annoying behaviour (bug?) in
Isabelle2013-2 and a recent version of repository (761e40ce91bc). When I
use the THEN attribute to transform a proved lemma in an auxiliary
context, I cannot refer to theorems imported by local interpretations.
My guess is that attributes in lemma statements somehow use a wrong
context.

This got delayed due my initial filtering for meaningless words like
"bug". I did not feel like giving again a lecture about that non-sense,
with the majority of people having no clue what it is about.

theory Scratch imports Main begin

locale l begin
lemma foo: "A ==> A" .
end

context begin
interpretation e!: l .

thm e.foo (* works *)
thm TrueI[THEN e.foo] (* works *)

lemmas bar1 = TrueI[THEN e.foo] (* works *)
lemmas bar2[THEN e.foo] = TrueI (* works *)

lemma bar [THEN e.foo]: "True" by simp (* does not work: Unknown fact "e.foo"
*)
end

end

What you see in lemma bar [THEN e.foo] above is the classic dynamic
scoping of fact expressions (so-called "notes") that was the standard
behaviour until about 2 years ago. It was known from the outset (around
1999) that dynamic scoping is generally a bad thing --- even though
classic LISP dialects still do it --- but I initially considered it
infeasible to implement proper static scoping for attributes and proof
methods.

I came back to statically applied attributes only much later, see the NEWS
of Isabelle2012 (May 2012):

* Rule attributes in local theory declarations (e.g. locale or class)
are now statically evaluated: the resulting theorem is stored instead
of the original expression. INCOMPATIBILITY in rare situations, where
the historic accident of dynamic re-evaluation in interpretations
etc. was exploited.

Here the wording is the result of spending a long time with old
applications (from AFP etc.) to get them updated to a better world. As
usual there are both accidental and intentional uses of such "features" in
corner cases that make reforms always a challenge.

I can't say on the spot if there were reasons of not making the situation
above statically scoped as well in 2012. Just a few days ago, I passed by
that part of the sources and was wondering about it. A quick try now
immediately produces obscure failure elsewhere, but I might come back to
it before the Isabelle2014 release this summer. (Major renovations in the
management of facts and attribute expressions are in the pipeline.)

Makarius

Last updated: Apr 29 2024 at 20:15 UTC