Email Gateway (Jun 04 2026 at 11:21): Email Gateway (Jun 04 2026 at 11:21):From: Alex Mobius <cl-isabelle-users@lists.cam.ac.uk>
As I've previously written, assigning a sort to type variable 'a in locale axioms triggers surprising behaviour: it sometimes succeeds and sometimes fails, and the locale context ends up with a copy of theorems that refer to (normally inaccessible) locale fixes, instead of class polymorphic constants. I stumbled upon this in HOLCF, but this can crop up up any time you use a symbol in assumptions that fixes the sort of one of its typevars and wasn't defined in the class context.
I managed to create a reproduction that does not use HOLCF, and demonstrates the quirks rather minimally. Text included and attached for convenience.
theory Repro2 imports Main begin
(* this sort assignment fails (ord incompatible with default sort type), I am not sure why *)
class order_chain = order +
assumes "∃x::(nat⇒'a::ord). ∀i. x i ≤ x (Suc i)"
(* However if we make local copies of type classes, the same thing succeeds *)
class ord2 =
fixes less_eq2 :: "'a ⇒ 'a ⇒ bool"
and less2 :: "'a ⇒ 'a ⇒ bool"
begin
notation
less_eq2 (‹'(≤2')›) and
less_eq2 (‹(‹notation=‹infix ≤››_/ ≤2 _)› [51, 51] 50) and
less2 (‹'(<2')›) and
less2 (‹(‹notation=‹infix <››_/ <2 _)› [51, 51] 50)
end
class preorder2 = ord2 +
assumes less_le2_not_le2: "x <2 y ⟷ x ≤2 y ∧ ¬ (y ≤2 x)"
and order2_refl [iff]: "x ≤2 x"
and order2_trans: "x ≤2 y ⟹ y ≤2 z ⟹ x ≤2 z"
begin
lemma order2_le_trans: "x <2 y ⟹ y <2 z ⟹ x <2 z"
unfolding less_le2_not_le2
using order2_trans by blast
end
class order2 = preorder2 +
assumes order2_antisym: "x ≤2 y ⟹ y ≤2 x ⟹ x = y"
class order2_chain = order2 +
assumes "∃x::(nat⇒'a::preorder2). ∀i. x i ≤2 x (Suc i)"
begin
(* We have succeeded, but the local context is weird: local facts now refer to e.g.
locale fixed variable less_eq2, which is distinct from polymorphic constant less_eq2 *)
lemma "x ≤2 y ⟹ y ≤2 z ⟹ x ≤2 z" by (fact order2_trans) (* fails *)
lemma "x ≤2 y ⟹ y ≤2 z ⟹ x ≤2 z" by (fact preorder2_class.order2_trans) (succeeds)
end
(* Weirdly this works with base classes but with superclass ord (because it has no axioms maybe?)
*)
class order_chain_higher_sort = ord +
assumes "∃x::(nat⇒'a::order). ∀i. x i ≤ x (Suc i)"
end
Last updated: Jun 12 2026 at 04:13 UTC