*To*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>, isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Attributes use wrong context in lemma statement*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Thu, 27 Feb 2014 13:31:02 +0100*In-reply-to*: <530F1393.1060502@informatik.tu-muenchen.de>*References*: <52E61A9F.6070201@inf.ethz.ch> <530F1393.1060502@informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.3.0

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" *) endI 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.

Andreas

**References**:**Re: [isabelle] Attributes use wrong context in lemma statement***From:*Florian Haftmann

- Previous by Date: Re: [isabelle] Attributes use wrong context in lemma statement
- Next by Date: [isabelle] CICM 2014: Extended Deadline March 14th, 2014
- Previous by Thread: Re: [isabelle] Attributes use wrong context in lemma statement
- Next by Thread: [isabelle] CICM 2014: Extended Deadline March 14th, 2014
- Cl-isabelle-users February 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list