[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" .
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" *)
This archive was generated by a fusion of
Pipermail (Mailman edition) and