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

Quoting Victor Porton <porton at 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

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