Stream: General

Topic: Circularity and infinite chains in the locale hierarchy

Gergely Buday (Sep 15 2025 at 10:54):

Section 5.7.3 Locale interpretation in the Isar Reference Manual says:

Circular sublocale declarations are allowed as long as they do not lead to infinite chains.

How a circular, sublocale A < B, sublocale B < A declaration does not lead to an infinite chain?

And, what declarations do lead to an infinite chain?

This works:

locale partial_order =
  fixes le :: "'a ⇒ 'a ⇒ bool" (infixl "⊑" 50)
  assumes reflexivity [intro, simp]: "x ⊑ x"
      and antisymmetry [intro]: "x ⊑ y ⟹ y ⊑ x ⟹ x = y"
      and transitivity [trans]: "x ⊑ y ⟹ y ⊑ z ⟹ x ⊑ z"
begin end

locale po = partial_order

sublocale po < partial_order ..

sublocale partial_order < po sledgehammer
  using partial_order_axioms po_def by blast

Mathias Fleury (Sep 15 2025 at 16:07):

You have to be careful, some locale errors only happens when you instantiate them

Mathias Fleury (Sep 15 2025 at 16:08):

because it is only at the instantiation time, that the theorems are generated

Manuel Eberl (Sep 17 2025 at 11:38):

I think if you reach the exact same locale interpretation again in the chain that you already have then that's fine; it just terminates at that point. That's how e.g. the "dual" sublocales in the order locales work. But all the term parameters have to be exactly the same terms for that to work. I'm sure that's documented somewhere...

Last updated: Oct 09 2025 at 01:37 UTC