Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Locale expression and contradiction

view this post on Zulip Email Gateway (Aug 18 2022 at 15:24):

From: Brian Huffman <brianh@cs.pdx.edu>
On Wed, Jun 2, 2010 at 10:54 AM, John Munroe <munddr@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.

view this post on Zulip Email Gateway (Aug 18 2022 at 15:26):

From: John Munroe <munddr@gmail.com>
On Thu, Jun 3, 2010 at 3:46 PM, Brian Huffman <brianh@cs.pdx.edu> wrote:

On Wed, Jun 2, 2010 at 10:54 AM, John Munroe <munddr@gmail.com> wrote:

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

What I actually wanted to prove is that whether there's a function in
LocB such that it'd return the same value as that returned by a
function in LocC for the same argument. Would I need to parameterise F
and G in locB and F in locC?

Thanks again.
John

, 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.

view this post on Zulip Email Gateway (Aug 18 2022 at 15:33):

From: John Munroe <munddr@gmail.com>
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? Is the lemma what I think it is, 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?

Thanks
John

Last updated: Nov 21 2024 at 12:39 UTC