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

05.01.2011, 10:16, "Tobias Nipkow" <nipkow at 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
--
Victor Porton - http://portonvictor.org

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