Re: [isabelle] Locale expression and contradiction
On Wed, Jun 2, 2010 at 10:54 AM, John Munroe <munddr at gmail.com> wrote:
> 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'
> lemma (in LocB) lem: "EX f s. f s = F' s"
> by auto
> 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
"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"
>, 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"
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and