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



Hi Andreas,

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

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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