Re: [isabelle] Attributes use wrong context in lemma statement
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?
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
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and