Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Simplification in locales

Email Gateway (Aug 18 2022 at 12:06):

From: John Matthews <matthews@galois.com>
I'm running into some behavior of locales that seems to violate
"locality". I'm using Isabelle2008. If I define the following locale

locale l =
fixes x :: nat
begin

definition
f :: "nat => nat" where
"f y = x + y"

end

and then try to simplify the following (unprovable) lemma using the
definition of f:

lemma (in l)
"f y = 2 * y"
apply (simp add: f_def)

then I get the subgoal "x = y", as expected. If, however, I add a
hypothesis about x to the lemma and try to simplify it again:

lemma (in l)
"x = y ==> f y = 2 * y"
apply (simp add: f_def)

then I'd expect the lemma to be provable, but instead I get the
following subgoal:

1. x = y ==> l.f y y = 2 * y

Eliminating the locale l and replacing "fixes x :: nat" with "consts
x :: nat" causes the lemma to be provable, so it seems that the
abstraction of a locale as a local theory is being violated somehow.

Thanks,
-john

Email Gateway (Aug 18 2022 at 12:06):

From: Brian Huffman <brianh@cs.pdx.edu>
Quoting John Matthews <matthews@galois.com>:

I'm running into some behavior of locales that seems to violate
"locality". I'm using Isabelle2008. If I define the following locale

locale l =
fixes x :: nat
begin

definition
f :: "nat => nat" where
"f y = x + y"

end
...
If, however, I add a
hypothesis about x to the lemma and try to simplify it again:

lemma (in l)
"x = y ==> f y = 2 * y"
apply (simp add: f_def)

then I'd expect the lemma to be provable, but instead I get the
following subgoal:

1. x = y ==> l.f y y = 2 * y

I think I understand what is going on here. When you define the
constant f inside the locale l, it defines a global constant named
"l.f", which has extra parameters corresponding to the locale fixes.

Within the context of locale l, when you write "f", this is really
just an abbreviation for "l.f x". So your lemma is really equivalent to:

lemma (in l) "x = y ==> l.f x y = 2 * y"

The simplifier then happily rewrites x to y in the conclusion:

1. x = y ==> l.f y y = 2 * y

Eliminating the locale l and replacing "fixes x :: nat" with "consts x
:: nat" causes the lemma to be provable, so it seems that the
abstraction of a locale as a local theory is being violated somehow.

I agree that the locale abstraction is being violated in this case.
Even if locale-defined constants are implemented as abbreviations,
this should not be apparent to the user. Here's my idea for a possible
remedy: Within the locale, the simplifier should use a congruence rule
that prevents the implicit parameters from being rewritten:

lemma f_cong [cong]: "y = z ==> l.f x y = l.f x z"

• Brian

Last updated: Nov 21 2024 at 12:39 UTC