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



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.