Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] How to show that locale loop is finite?

Email Gateway (Aug 18 2022 at 16:46):

From: Tobias Nipkow <nipkow@in.tum.de>
Isabelle does not unfold definitions automatically, you need to do that
explicitly, eg by(simp add: fdef_def). However, when running your
theory, I get a different error, which has nothing to do with F:

*** Roundup bound exceeded (sublocale relation probably not terminating).
*** At command "locale"

If you did not get this, you were lucky.

Tobias

Victor Porton schrieb:

Email Gateway (Aug 18 2022 at 16:53):

From: Victor Porton <porton@narod.ru>
05.01.2011, 10:16, "Tobias Nipkow" <nipkow@in.tum.de>:

Isabelle does not unfold definitions automatically, you need to do that
explicitly, eg by(simp add: fdef_def). However, when running your
theory, I get a different error, which has nothing to do with F:

*** Roundup bound exceeded (sublocale relation probably not terminating).
*** At command "locale"

If you did not get this, you were lucky.

"Roundup bound exceeded" appears because Isabelle treats all expressions such as "F(F(F(F(x)))))" and does not understand that these are equal to "x". I could add by(simp add: fdef_def) as you recommend but don't know where to add it.

Victor Porton schrieb:

The following theory does not verify. Which additional lemmas it needs to make it to verify? Isabelle does not understand that F(x) = x. How to make it to understand?

theory test
   imports Main_ZF
 begin

definition fdef: "F(x) == x"

locale loc1 =
   fixes s1::i

locale loc2 =
   fixes s2::i

sublocale loc1 < p1: loc2 "F(s2)" .

sublocale loc2 < p2: loc1 "F(s1)" .

locale test = loc1 "0"

interpretation inter: loc1 "0"
 sorry

Email Gateway (Aug 18 2022 at 16:53):

From: Clemens Ballarin <ballarin@in.tum.de>
Quoting Victor Porton <porton@narod.ru>:

The following theory does not verify. Which additional lemmas it
needs to make it to verify? Isabelle does not understand that F(x) =
x. How to make it to understand?

Given the locales below,

sublocale loc1 < p1: loc2 "F(s1)"

instructs to add (and prove) instances of theorems from loc2, where s2
is substituted by F(s1). This is irrespective of relations between s1
and F(s1) that might be provable. If F(s1) = s1 you may consider the
declaration

sublocale loc1 < p1: loc2 s1

Likely this is not what you want, though. Section "Avoiding Infinite
Chains of Interpretations" in the locales tutorial might be worth
reading.

theory test
imports Main_ZF
begin

definition fdef: "F(x) == x"

locale loc1 =
fixes s1::i

locale loc2 =
fixes s2::i

sublocale loc1 < p1: loc2 "F(s2)" .

sublocale loc2 < p2: loc1 "F(s1)" .

locale test = loc1 "0"

interpretation inter: loc1 "0"
sorry

Email Gateway (Aug 18 2022 at 17:00):

From: Victor Porton <porton@narod.ru>
The following theory does not verify. Which additional lemmas it needs to make it to verify? Isabelle does not understand that F(x) = x. How to make it to understand?

theory test
imports Main_ZF
begin

definition fdef: "F(x) == x"

locale loc1 =
fixes s1::i

locale loc2 =
fixes s2::i

sublocale loc1 < p1: loc2 "F(s2)" .

sublocale loc2 < p2: loc1 "F(s1)" .

locale test = loc1 "0"

interpretation inter: loc1 "0"
sorry

Last updated: Apr 23 2024 at 04:18 UTC