Stream: Beginner Questions

Topic: Oddity with records and locales

John Hughes (Jul 28 2025 at 17:30):

Hoping to duplicate the structure of HOL/Algebra for using records as part of defining locales for algebraic objects (see also #Beginner Questions > Should I always bundle the data in a locale into a record? ), I've copied and slightly simplified the setup for a monoid:

record 'a monoid =
  carrier :: "'a set"
  mult    :: "['a, 'a] ⇒ 'a" (infixl ‹⊗ı› 70)
  one     :: 'a (‹𝟭ı›)

locale monoid =
  fixes G (structure)
  assumes m_closed [intro, simp]:
         "⟦x ∈ carrier G; y ∈ carrier G⟧ ⟹ x ⊗ y ∈ carrier G"
      and m_assoc:
         "⟦x ∈ carrier G; y ∈ carrier G; z ∈ carrier G⟧
          ⟹ (x ⊗ y) ⊗ z = x ⊗ (y ⊗ z)"
      and one_closed [intro, simp]: "𝟭 ∈ carrier G"
      and l_one [simp]: "x ∈ carrier G ⟹ 𝟭 ⊗ x = x"
      and r_one [simp]: "x ∈ carrier G ⟹ x ⊗ 𝟭 = x"
begin
end

Here the simplification was simply folding the "partial object" record into the monoid record. When I look at this in jEdit, the G in fixes G (structure) is shown in blue:
image.png

When I try to replicate that approach, albeit with different names, like this:

record ('p, 'l) affine_plane_r =
  Points :: "'p set"
  Lines :: "'l set"
  incid :: "'p ⇒ 'l ⇒ bool" (infix "⊲" 60)

locale affine_plane_data =
  fixes AP (structure)
  assumes contains:
    "⟦ k ∈ Lines AP ; P ∈ Points AP⟧ ⟹ (P ⊲ k)"
(*  fixes join:: "'p ⇒ 'p ⇒ 'l"
  fixes find_parallel:: "'l ⇒ 'p ⇒ 'l" *)
begin
end

the fixes AP (Structure) shows AP in black instead:
image.png

It also seems unhappy about my use of ⊲ as an infix operator, even though in the monoid example, the use of ⊗ as an infix operator works fine.

I suppose that my problem could be that I have two types, 'p and 'l, while monoids have only 'a, but I'm hoping it's something simpler/stupider, and that I've made some sort of copy-paste error that'll be obvious to a trained eye.

Can anyone explain what's going on here?

John Hughes (Jul 28 2025 at 17:50):

...wait. I think I've partly answered my own question. When I simplify to this:

locale affine_plane_data =
  fixes AP (structure)
  assumes nonempty: "Lines AP ≠ {}"
begin
end

then the AP turns blue. So perhaps the black vs blue problem is a symptom of the second problem: the fact my my contains assumption is generating a syntax error is causing the color problem as well.

I'm still puzzled, however, about the problem with ⊲, and why it doesn't work the way that multiplication seems to for monoids.

Christian Pardillo Laursen (Jul 28 2025 at 17:51):

Adding the ı character to the infix definition seems to do the trick, though I'm not entirely sure why that might be - perhaps it hints at an implicit argument?

record ('p, 'l) affine_plane_r =
  Points :: "'p set"
  Lines :: "'l set"
  incid :: "'p ⇒ 'l ⇒ bool" (infix ‹◃ı› 60)

locale affine_plane_data =
  fixes AP (structure)
  assumes contains:
    "⟦ k ∈ Lines AP ; P ∈ Points AP⟧ ⟹ (k ◃ P)"
(*  fixes join:: "'p ⇒ 'p ⇒ 'l"
  fixes find_parallel:: "'l ⇒ 'p ⇒ 'l" *)

The original works if we pass AP as an argument to ◃:

record ('p, 'l) affine_plane_r =
  Points :: "'p set"
  Lines :: "'l set"
  incid :: "'p ⇒ 'l ⇒ bool" (infix ‹◃› 60)

locale affine_plane_data =
  fixes AP (structure)
  assumes contains:
    "⟦ k ∈ Lines AP ; P ∈ Points AP⟧ ⟹ ((◃) AP k P)"

In both cases AP returns to blue - that only happens because of the error

John Hughes (Jul 28 2025 at 17:56):

Wow. I have no idea what that character means, and figured it had something to do with writing a subscript of G on later uses of ⊗, which I didn't need. As usual, I guess (a) that this takes me past this stumbling block, but (b) I've got more reading to do.

Thanks!

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

FYI some people consider the HOL-Algebra approach a bit old fashioned and prefer something like Ballarin's approach to algebra in the AFP. Also uses locales, but without records. Frankly I'm not convinced; to me it seems more like they both have their advantages and disadvantages.

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

And yes, that weird character is basically a placeholder for the structure parameter. The syntax with the HOL-Algebra approach can get a bit clunky. That's one disadvantage over Ballarin's approach. Some better tool support could go a long way here...

John Hughes (Sep 20 2025 at 15:28):

Thanks, Manuel. At this point I'm pretty much committed to the HOL-Algebra approach because with two types and a couple of functions, putting them all in a record just shortens all my "have" and "show" claims. :) I agree that a bit more tool support would be a nice thing.

Last updated: Oct 12 2025 at 20:20 UTC