John Hughes (Apr 01 2025 at 13:48): John Hughes (Apr 01 2025 at 13:48):In HOL-Algebra.Group, early on we have
record 'a monoid = "'a partial_object" +
mult :: "['a, 'a] ⇒ 'a" (infixl ‹⊗ı› 70)
one :: 'a (‹𝟭ı›)
definition m_inv :: "('a, 'b) monoid_scheme => 'a => 'a"
where "m_inv G x = (THE y. y ∈ carrier G ∧ x ⊗⇘G⇙ y = 𝟭⇘G⇙ ∧ y ⊗⇘G⇙ x = 𝟭⇘G⇙)"
Cmd-clicking on monoid_scheme jumps to the record definition a few lines above. I figured it might be something automatically generated when the record was created, so I made a Scratch file containing this:
theory Scratch
imports Main "HOL-Algebra.Congruence" "HOL-Library.FuncSet"
begin
record 'a zonoid = "'a partial_object" +
mult :: "['a, 'a] ⇒ 'a" (infixl ‹⊗ı› 70)
one :: 'a (‹𝟭ı›)
end
A query with name: zonoid then yielded many many things, but not zonoid_scheme. I also grepped through the HOL sources for monoid_scheme and saw it used a lot, but nothing that looked like a definition.
As I'm trying to define a notion of isomorphism for affine and projective planes (locales that I've definied), I was hoping to mimic the definition of hom from the Algebra theories, but go stuck here. Can someone tell me where monoid_scheme came from, and what it means?
Mathias Fleury (Apr 01 2025 at 14:25):monoid is a record and monoid_scheme is the definition generated by the record package
John Hughes (Apr 01 2025 at 15:28):So why, in my scratch example, does "zonoid_scheme" not show up in the search?
Mathias Fleury (Apr 01 2025 at 15:36):It is a type, not a term
typ ‹('a, 'b) zonoid_scheme›
You can search for ‹_ :: (_, _) zonoid_scheme› however
Last updated: Apr 18 2025 at 20:21 UTC