theory LocalesModuleSystem

imports Main

begin

locale partial_order =
  fixes S and le (infixl "⊑" 50)
  assumes refl: "x∈S ⟹ x⊑x"
      and antisym: "⟦ x⊑y; y⊑x; x ∈ S; y ∈ S ⟧ ⟹ x = y"
      and transitive: "⟦x⊑y; y⊑z; x∈S; y∈S; z∈S⟧ ⟹ x⊑z"

context partial_order begin
definition is_inf where "is_inf x y w ⟷
  w⊑x ∧ w⊑y ∧ (∀z∈S. z⊑x ∧ z⊑y ⟶ z⊑w) ∧ x∈S ∧ y∈S ∧ w∈S"
end

locale semilattice = partial_order "S" "le" for S and le (infixl "⊑" 50) +
  assumes existence: "⟦x∈S; y∈S⟧ ⟹ ∃inf. is_inf x y inf"

context semilattice begin
definition meet (infixl "⊓" 70)
  where "meet = (λx∈S . λy∈S . THE inf. is_inf x y inf)"