*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Unexpected assumptions in nested contexts*From*: Lars Noschinski <noschinl at in.tum.de>*Date*: Wed, 13 Jun 2012 17:30:38 +0200*In-reply-to*: <jraa1j$2lm$1@dough.gmane.org>*References*: <jraa1j$2lm$1@dough.gmane.org>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:8.0) Gecko/20120104 Icedove/8.0

On 13.06.2012 17:02, Lars Hupel wrote:

Nesting two contexts, where the inner context makes assumptions about fixed variables from the outer context, results in unexpected all-quantified assumptions. Consider this minimal example: context fixes I :: "'a set" begin context assumes I: "finite I" begin lemma test: "something_about I" sorry end end Looking at the fact `test` from outside both contexts with `thm test`, I get: (!!I. finite I) ==> ?something_about ?I [!] Obviously, this fact says something completely different.

This issue arises already after leaving the inner context: context fixes I :: "'a set" assumes nonempty: "I ≠ {}" begin context assumes I: "finite I" begin lemma card_neq_0: "card I ≠ 0" using I nonempty by auto end thm card_neq_0

But I don't have any idea how these contexts work or are supposed to work. -- Lars

**References**:**[isabelle] Unexpected assumptions in nested contexts***From:*Lars Hupel

- Previous by Date: Re: [isabelle] Unexpected assumptions in nested contexts
- Next by Date: Re: [isabelle] Formalisations of infinite streams
- Previous by Thread: Re: [isabelle] Unexpected assumptions in nested contexts
- Next by Thread: [isabelle] 3 new AFP entries available
- Cl-isabelle-users June 2012 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