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

Last updated: Sep 16 2025 at 12:42 UTC