Theory Kleene_Algebra.Signatures

(* Title:      Signatures for Kleene Algebra
   Author:     Alasdair Armstrong, Georg Struth, Tjark Weber
   Maintainer: Georg Struth <g.struth at sheffield.ac.uk>
               Tjark Weber <tjark.weber at it.uu.se>
*)

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)

(*
class residual_r_op =
  fixes residual_r :: "'a ⇒ 'a ⇒ 'a" (infixr "→" 60)

class residual_l_op =
  fixes residual_l :: "'a ⇒ 'a ⇒ 'a" (infixl "←" 60)
*)

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