*To*: Brian Huffman <huffman at in.tum.de>*Subject*: Re: [isabelle] using global theorems in locale context*From*: Viorel Preoteasa <viorel.preoteasa at abo.fi>*Date*: Sun, 08 Apr 2012 11:58:50 +0300*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <CAAMXsiYSbTXJkWopwiLja9F1suLL9v20N30a4NPU8GidBz2FCg@mail.gmail.com>*References*: <CAAPnxw3pRenDhpMqcPrWWvYW8O1tYE6rbAtwBv3OpHLKvCAcPw@mail.gmail.com> <4F8045B0.7020409@abo.fi> <CAAMXsiYSbTXJkWopwiLja9F1suLL9v20N30a4NPU8GidBz2FCg@mail.gmail.com>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.7; rv:11.0) Gecko/20120327 Thunderbird/11.0.1

Hello Brian, Than you for your answer. I understand the reasons. I was hopping that there is a mechanism such that you can use a global theorem in a local context. I think that I had this problem before, and I did not find a solution. I have two subclasses A and B of a complete lattice, and the fusion theorem would allow me to prove that B is a subclass of A. I have stated this property in this way: lemma "class.B (bot::'a::A) ..." which is satisfactory. Viorel On 4/7/12 5:40 PM, Brian Huffman wrote:

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

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

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

**Re: [isabelle] using global theorems in locale context***From:*Brian Huffman

- Previous by Date: [isabelle] LSFA 2012: Call For Papers
- Next by Date: [isabelle] UITP'12: Second Call for Papers
- Previous by Thread: Re: [isabelle] using global theorems in locale context
- Next by Thread: Re: [isabelle] Isabelle2011-1 with PG crashes
- 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