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.