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



Hi Florian,

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

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




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