Re: [isabelle] How to show that locale loop is finite?
Quoting Victor Porton <porton at narod.ru>:
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?
Given the locales below,
sublocale loc1 < p1: loc2 "F(s1)"
instructs to add (and prove) instances of theorems from loc2, where s2
is substituted by F(s1). This is irrespective of relations between s1
and F(s1) that might be provable. If F(s1) = s1 you may consider the
sublocale loc1 < p1: loc2 s1
Likely this is not what you want, though. Section "Avoiding Infinite
Chains of Interpretations" in the locales tutorial might be worth
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