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

Quoting Victor Porton <porton at>:

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

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"

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.