Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Conflicting locales with a common signature


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

From: Michael Chan <mchan@inf.ed.ac.uk>
Hi all,

I have a question about proving theorems about conflicting locales which
share a common signature. Suppose the following:

locale sig_loc =
fixes f :: "real=>real"

locale loc1 = sig_loc +
assumes ax1: "ALL x. f x > 0"

locale loc2 = sig_loc +
assumes ax1: "ALL x. f x = 0"

locale locexp =
l1: loc1 f + l2: loc2 f'
for f f'

Clearly, loc1 and loc2 conflict with each other due to loc1.ax1 and
loc2.ax1. Since they both contain the constant 'f', could one come up
with a theorem stating that there exists a function 'func' and a real
number 'x' such that 'func x > 0' holds in one locale (loc1) and 'func x
= 0' holds in another (loc2)? Something in a similar shape as

lemma (in locexp) lem: "EX func x. func x > 0 & func x = 0"

but that's inconsistent. Are there ways to annotate the variables, e.g.,
"EX func x. l1.func x > 0 & l2.func x = 0", or something similar?

Thanks in advance.

Regards,
Michael

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

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Michael,

You just need to give both parameters the same name on import, e.g.:

locale A =
fixes f
assumes involutory: "f ∘ f = id"

locale B =
fixes g
assumes idempotency: "g ∘ g = g"

locale C = A h + B h for h
begin

lemma "h = id"
using involutory idempotency by simp

end

Note also that the concept of locale import has little to do with the
object-oriented concept of inheritance, so it is rarely helpful to think
in that category.

Hope this helps,
Florian
signature.asc

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

From: Peter Gammie <peteg42@gmail.com>
Michael,

Did you try this?

Try saying:

print_locale! locexp

to see what Isabelle thinks you are trying to say.

locexp is not inconsistent - loc1 is instantiated with f, and loc2 with f' - distinct parameters. The diamond dependency you're trying to exploit doesn't work the way you think it does (I think :-).

I'd also suggest making the prefixes l1 and l2 mandatory:

locale locexp =
l1!: loc1 f + l2!: loc2 f'
for f f'

Hope this helps.

cheers
peter


Last updated: Mar 29 2024 at 12:28 UTC