Theory Signatures
section ‹Signatures›
theory Signatures
imports Main
begin
text ‹
Default notation in Isabelle/HOL is occasionally different from
established notation in the relation/algebra community. We use the
latter where possible.
›
notation
times (infixl "⋅" 70)
text ‹
Some classes in our algebraic hierarchy are most naturally defined as
subclasses of two (or more) superclasses that impose different
restrictions on the same parameter(s).
Alas, in Isabelle/HOL, a class cannot have multiple superclasses that
independently declare the same parameter(s). One workaround, which
motivated the following syntactic classes, is to shift the parameter
declaration to a common superclass.
›
class star_op =
fixes star :: "'a ⇒ 'a" ("_⇧⋆" [101] 100)
class omega_op =
fixes omega :: "'a ⇒ 'a" ("_⇧ω" [101] 100)
text ‹
We define a type class that combines addition and the definition of
order in, e.g., semilattices. This class makes the definition of
various other type classes more slick.
›
class plus_ord = plus + ord +
assumes less_eq_def: "x ≤ y ⟷ x + y = y"
and less_def: "x < y ⟷ x ≤ y ∧ x ≠ y"
end