Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Locale parameters

Email Gateway (Aug 18 2022 at 18:25):

From: John Munroe <munddr@gmail.com>
Hi,

Suppose I have two locales L1 and L2:

locale L1 =
fixes c :: nat
assumes ax: "c = 0"

locale L2 =
fixes c :: nat
assumes ax: "c = 1"

and I want to prove a lemma stating that the constant 'c' in L1 does
not have the same value as the constant 'c' in L2:

lemma lem1: "ALL a b. L1 c --> c = a & L2 c --> c = b & a ~= b"
using L1.ax L2.ax
by auto

(hopefully the formulation matches my intended meaning.)

Now, if I change the parametrisation slightly:

lemma lem2: "ALL a b. L1 c --> c = a & L2 d --> d = b & a ~= b"
using L1.ax L2.ax
by auto

The proof fails. Aren't the occurrences of 'c' in lem1 distinct
instances? Which lemma actually matches my intended meaning, if any?

Any help will be appreciated. Thanks.

John

Email Gateway (Aug 18 2022 at 18:26):

From: "Tim (McKenzie) Makarios" <tjm1983@gmail.com>
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

On 27/09/11 05:57, John Munroe wrote:

Hi,

Suppose I have two locales L1 and L2:

locale L1 =
fixes c :: nat
assumes ax: "c = 0"

locale L2 =
fixes c :: nat
assumes ax: "c = 1"

and I want to prove a lemma stating that the constant 'c' in L1 does
not have the same value as the constant 'c' in L2:

lemma lem1: "ALL a b. L1 c --> c = a & L2 c --> c = b & a ~= b"
using L1.ax L2.ax
by auto

(hopefully the formulation matches my intended meaning.)

By turning on "Show Brackets", you can see that lem1 means
"ALL a b. L1 c --> ((c = a & L2 c) --> (c = b & a ~= b))"
(after you've removed other superfluous brackets). I don't think this
is what you meant. Perhaps you want something like this:

lemma lem3:
assumes "L1 c"
shows "~ L2 c"
using assms and L1.ax and L2.ax
by auto

or:

lemma lem4:
assumes "L1 c" and "L2 d"
shows "c ? d"
using assms and L1.ax and L2.ax
by auto

Now, if I change the parametrisation slightly:

lemma lem2: "ALL a b. L1 c --> c = a & L2 d --> d = b & a ~= b"
using L1.ax L2.ax
by auto

The proof fails. Aren't the occurrences of 'c' in lem1 distinct
instances?

No, I don't think so. They're not quantified separately; what would
make them distinct?

Which lemma actually matches my intended meaning, if any?

Any help will be appreciated. Thanks.

John

Tim
<><
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.10 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/

iEYEARECAAYFAk6A3kIACgkQ/cBxZIxl6rmuUQCgt2h/AVlrDZ3jAC3FJb5w+ve6
8DUAn2dfzBPNVW6uy9oOkppPApI3HcOW
=k9B2
-----END PGP SIGNATURE-----

Email Gateway (Aug 18 2022 at 18:26):

From: Clemens Ballarin <ballarin@in.tum.de>
Hi John,

Your question is actually not directly related to locales. Have a
look at Isabelle/HOL's term syntax (which should be explained in the
Isabelle/HOL tutorial).

All occurrences of c denote the same variable, which is implicitly
universally quantified at the outer most level. Also note that -->
binds less tightly than & and is right associative. That is, lem1
amounts to this:

!!c. ALL a b. (L1 c --> ((c = a & L2 c) --> (c = b & a ~= b)))

What you want is a lemma like this:

L1 a & L2 b --> a ~= b

Clemens

Last updated: Apr 19 2024 at 04:17 UTC