Re: [isabelle] Locale expression and contradiction



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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.