Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] How to make these cyclic locales to work?

view this post on Zulip Email Gateway (Aug 18 2022 at 16:54):

From: Victor Porton <porton@narod.ru>
Please explain why the below theory does not verify and how to make it to verify.

I need this knowledge in order to develop order/lattices theory for IsarMathLib.

theory test
imports Main_ZF
begin

locale loc1 =
fixes s::i
assumes "0 ~: s"

locale loc2 =
fixes s::i
assumes "0 : s"

sublocale loc1 < loc2 "s Un {0}" sorry

sublocale loc2 < loc1 "s - {0}" sorry

interpretation inter: loc1 "0"
sorry

end

Last updated: Nov 21 2024 at 12:39 UTC