Stream: Beginner Questions

Topic: local theorems get pulled from locale instead of class

Alex Mobius (May 05 2026 at 16:31):

following code:

theory Scratch imports HOLCF begin

class works = pcpo begin
typ 'a (* 'a::type *)
thm is_ubI (*(⋀x. x ∈ ?S ⟹ x ⊑ ?u) ⟹ ?S <| ?u*)
end

class weird = profinite begin
typ 'a (* 'a::cpo *)
thm is_ubI (*(⋀x. x ∈ ?S ⟹ below x ?u) ⟹ po.is_ub below ?S ?u*)
end

end

So in "profinite" context, the definitions from parent contexts have the locale form instead of class form which means they cannot be applied to normal definitions (po.is_ub and po_class.is_ub are distinct entities).

Not sure what to make of it, seems like some sort of a bug, especially the fact that it happens with profinite/bifinite/domain but not with cpo/pcpo. Not sure what to make of it, please help.

Alex Mobius (May 05 2026 at 16:35):

Ah, I figure this is likely because bifinite and profinite definition is defined on approx_chain which is limited to sort cpo, so context setup chokes on that in some way...

Kevin Kappelmann (May 06 2026 at 07:22):

I don't quite get it. I think if you could minimise it to a self-contained theory not using HOLCF, it would be easier to help.

Alex Mobius (May 06 2026 at 14:27):

Weirdly, I can only reproduce this with HOLCF:

theory Repro imports HOLCF begin
default_sort type

(* the trick works with a HOLCF class *)
class holcf = pcpo + assumes "∃(a::(nat⇒'a::cpo)). chain a"
begin
typ 'a (* 'a::cpo *)
(*theorem borked*)
thm is_ubI (*(⋀x. x ∈ ?S ⟹ below x ?u) ⟹ po.is_ub below ?S ?u*)
end

(*but doesn't work with a HOL class *)

class hol = linorder +
  assumes "∃(a :: (nat⇒'a::order)). mono a"
(*error "Sort constraint order inconsistent with default type for type variable "'a"*)

end

So, no luck reproducing without. But it's part of standard distribution and not very big, like HOL-Analysis...

Last updated: May 17 2026 at 06:46 UTC