[isabelle] Attributes use wrong context in lemma statement



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




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