*To*: John Munroe <munddr at gmail.com>*Subject*: Re: [isabelle] Locale expression and contradiction*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Thu, 3 Jun 2010 07:46:46 -0700*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <AANLkTinfV8IwPFVL-2_FLTliJUbIrlGIjNxZ7Kxd0iAe@mail.gmail.com>*References*: <AANLkTinfV8IwPFVL-2_FLTliJUbIrlGIjNxZ7Kxd0iAe@mail.gmail.com>*Sender*: huffman.brian.c at gmail.com

On Wed, Jun 2, 2010 at 10:54 AM, John Munroe <munddr at gmail.com> wrote: > Hi, > > I was wondering whether two locales that contradict with each other > can be combined in a local expression. For example: > > locale LocA = > fixes F :: "real => real" > > locale LocB = LocA + > assumes "F p = 0" > and "G p = 1" > > locale LocC = LocA + > assumes "F p = 1" > > locale LocExp = > LB: LocB F + LC: LocC F' > for F F' > > begin > lemma (in LocB) lem: "EX f s. f s = F' s" > by auto > end > > Is the reason why the lemma can be discharged that the locale LocExp > is inconsistent? Your locale LocExp is not inconsistent. Below are the assumptions of LocExp; there are three assumptions, and each is about a different function. "F p = 0" "G p = 1" "F' p = 1" By the way, unless you give names to your locale assumptions, you will have a hard time using them in later proofs. > Is the lemma what I think it is Your lemma is completely trivial, and its proof does not depend on any assumptions of any of your locales. LocB does not fix a variable F', so F' is considered as an ordinary free variable in lemma "lem". You could just as well prove it at the top level: lemma "EX f s. f s = F' s" by auto >, i.e. there exists > some function f and some argument s to f in the locale LocB such that > all values returned are same as those returned by F in LocC for the > same argument? How do you reconcile "there exists ... some argument s" with "all values returned"? Maybe you really meant this: lemma "EX f. ALL s. f s = F' s" by auto Either way, the lemma is trivially true, regardless of any locales. Whether or not any of your locales are inconsistent has no effect whatsoever on the proof. - Brian

**Follow-Ups**:**Re: [isabelle] Locale expression and contradiction***From:*John Munroe

**References**:**[isabelle] Locale expression and contradiction***From:*John Munroe

- Previous by Date: [isabelle] Implicit typing in lemma
- Next by Date: Re: [isabelle] Proofability of a simple existential statement
- Previous by Thread: [isabelle] Locale expression and contradiction
- Next by Thread: Re: [isabelle] Locale expression and contradiction
- Cl-isabelle-users June 2010 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