*To*: Steve W <s.wong.731 at googlemail.com>*Subject*: Re: [isabelle] Proving theorems bridging between two theories/locales*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Wed, 25 Nov 2009 08:07:48 -0800*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <12d162d00911240725p1f8540camd7f06e12844b2279@mail.gmail.com>*References*: <12d162d00911240725p1f8540camd7f06e12844b2279@mail.gmail.com>*Sender*: huffman.brian.c at gmail.com

On Tue, Nov 24, 2009 at 7:25 AM, Steve W <s.wong.731 at googlemail.com> wrote: > Hi, > > I'm reposting a question from earlier: > > I was wondering whether Isabelle can prove theorems bridging between two > theories or locales. For example, if I have A.thy and B.thy, can I prove > that there is a constant c in A that equals to v, while c in B that doesn't > equal to v? A and B can't be merged into one because together they'd be > inconsistent. Hi Steve, Certainly, if A.thy and B.thy each declare axioms, a merged theory might be inconsistent. But if each theory defines a constant called "c", then that doesn't prevent you from merging theories: The real constant names are qualified names like "A.c" and "B.c", so in a merged theory you might be able to prove something like "A.c ~= B.c". > Could locales be used here? It seems to me that: "locale C = A + B" would > merge A and B together to form C. That is exactly right. For example, if you want to show that the assumptions from locales A and B are inconsistent with each other, you can do something like this: locale C = A + B begin lemma A_B_inconsistent: "False" <proof using assumptions from locales A and B> end > Perhaps another operator could be used to > indicate that two locales are involved in the proof, but are not imported. If you don't want to define a new locale, you can combine locales within a single proof using the "interpret" command. This involves adding the locale predicates as assumptions of your lemma. Here is an example: locale A = fixes foo assumes ... locale B = fixes bar assumes ... lemma A_B_inconsistent: assumes "A foo" and "B bar" shows "False" proof - interpret A foo by fact interpret B bar by fact show "False" <proof using assumptions from locales A and B> qed > Is there a better way for proving bridging theorems? If not, would it > necessary for me to implement such an operator in ML? How much effort should > the implementation require? > > Thanks > Steve Hopefully one of the above methods will work for you. I don't think it should be necessary to implement anything at the ML level. - Brian

**References**:

- Previous by Date: [isabelle] Memocode 2010 First Call for Papers
- Next by Date: [isabelle] IJCAR 2010 - first call for papers
- Previous by Thread: [isabelle] Proving theorems bridging between two theories/locales
- Next by Thread: Re: [isabelle] Proving theorems bridging between two theories/locales
- Cl-isabelle-users November 2009 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