Theory Lattice_Syntax

(* Author: Florian Haftmann, TU Muenchen *)

section ‹Pretty syntax for lattice operations›

theory Lattice_Syntax
imports Complete_Lattices
begin

notation
  bot ("⊥") and
  top ("⊤") and
  inf  (infixl "⊓" 70) and
  sup  (infixl "⊔" 65) and
  Inf  ("⨅_" [900] 900) and
  Sup  ("⨆_" [900] 900)

syntax
  "_INF1"     :: "pttrns ⇒ 'b ⇒ 'b"           ("(3⨅_./ _)" [0, 10] 10)
  "_INF"      :: "pttrn ⇒ 'a set ⇒ 'b ⇒ 'b"  ("(3⨅_∈_./ _)" [0, 0, 10] 10)
  "_SUP1"     :: "pttrns ⇒ 'b ⇒ 'b"           ("(3⨆_./ _)" [0, 10] 10)
  "_SUP"      :: "pttrn ⇒ 'a set ⇒ 'b ⇒ 'b"  ("(3⨆_∈_./ _)" [0, 0, 10] 10)

end