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

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:
> 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

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