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.


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.