*To*: Viorel Preoteasa <viorel.preoteasa at abo.fi>*Subject*: Re: [isabelle] using global theorems in locale context*From*: Brian Huffman <huffman at in.tum.de>*Date*: Sat, 7 Apr 2012 16:40:21 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <4F8045B0.7020409@abo.fi>*References*: <CAAPnxw3pRenDhpMqcPrWWvYW8O1tYE6rbAtwBv3OpHLKvCAcPw@mail.gmail.com> <4F8045B0.7020409@abo.fi>

On Sat, Apr 7, 2012 at 3:48 PM, Viorel Preoteasa <viorel.preoteasa at abo.fi> wrote: > Hello, > > I have the following theorem > > lemma small_fusion: "h : Disjunctive ==> mono f ==> mono g ==> h o f = g o h > ==> h (lfp f) = lfp g" > > which is proved as a global theorem. > > However I would like to use it in a context of a complete lattice > > context complete_lattice > begin > lemma ... > apply (cut_tac ... in small_fusion) > > The main reason I have small_fusion as a global theorem is because I use > lfp_ordinal_induct to prove it. If I want to prove small_fusion in the > context > of a complete lattice, then I would have to build everything about lfp > in the local context. The reason that lfp_ordinal_induct is not proved in the locale context is because it refers to the constant "mono". The constant "mono :: ('a::order => 'b::order) => bool" is not defined within the "order" locale context because its type mentions not one order, but two different orders. If you want to have lfp_ordinal_induct inside the complete_lattice locale context, the only way I can think of is to define a more restricted "mono' :: ('a => 'a) => bool" in the locale context, and then reprove the lfp lemmas in terms of that. (There are only 5 or 6 easy lemmas necessary to prove lfp_ordinal_induct; you could just copy the proof scripts from Inductive.thy.) The inability of the class-based locales to handle constants like "mono" is very unfortunate. Perhaps some of the other developers have more to add about this; I hope that the situation can be improved in the future! - Brian

**Follow-Ups**:**Re: [isabelle] using global theorems in locale context***From:*Viorel Preoteasa

**References**:**[isabelle] Isabelle2011-1 with PG crashes***From:*Alfio Martini

**[isabelle] using global theorems in locale context***From:*Viorel Preoteasa

- Previous by Date: [isabelle] using global theorems in locale context
- Next by Date: [isabelle] LSFA 2012: Call For Papers
- Previous by Thread: [isabelle] using global theorems in locale context
- Next by Thread: Re: [isabelle] using global theorems in locale context
- Cl-isabelle-users April 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