Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Conflicting locales with a common signature

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

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

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: Nov 21 2024 at 12:39 UTC