[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?
definition fdef: "F(x) == x"
locale loc1 =
locale loc2 =
sublocale loc1 < p1: loc2 "F(s2)" .
sublocale loc2 < p2: loc1 "F(s1)" .
locale test = loc1 "0"
interpretation inter: loc1 "0"
This archive was generated by a fusion of
Pipermail (Mailman edition) and