Theory Omega_Kleene_Algebra
section ‹$\omega$-Kleene algebras›
theory "Omega_Kleene_Algebra"
imports Quantales_Converse.Modal_Kleene_Algebra_Var
begin
text ‹Here we develop $\omega$-semigroups and $\omega$-Kleene algebras.›
subsection ‹Copies for i-structures›
class icomp_op =
fixes icomp :: "'a ⇒ nat ⇒ 'a ⇒ 'a" ("_ ⋅⇘_⇙ _" [70,70,70]70)
class iid_op =
fixes un :: "nat ⇒ 'a"
class istar_op =
fixes star :: "nat ⇒ 'a ⇒ 'a"
class idom_op =
fixes do :: "nat ⇒ 'a ⇒ 'a"
class icod_op =
fixes cd :: "nat ⇒ 'a ⇒ 'a"
class imonoid_mult = icomp_op + iid_op +
assumes assoc: "x ⋅⇘i⇙ (y ⋅⇘i⇙ z) = (x ⋅⇘i⇙ y) ⋅⇘i⇙ z"
and comp_unl: "un i ⋅⇘i⇙ x = x"
and comp_unr: "x ⋅⇘i⇙ un i = x"
class idioid = imonoid_mult + join_semilattice_zero +
assumes distl: "x ⋅⇘i⇙ (y + z) = x ⋅⇘i⇙ y + x ⋅⇘i⇙ z"
and distr: "(x + y) ⋅⇘i⇙ z = x ⋅⇘i⇙ z + y ⋅⇘i⇙ z"
and annil: "0 ⋅⇘i⇙ x = 0"
and annir: "x ⋅⇘i⇙ 0 = 0"
class ikleene_algebra = idioid + istar_op +
assumes star_unfoldl: "un i + x ⋅⇘i⇙ star i x ≤ star i x"
and star_unfoldr: "un i + star i x ⋅⇘i⇙ x ≤ star i x"
and star_inductl: "z + x ⋅⇘i⇙ y ≤ y ⟹ star i x ⋅⇘i⇙ z ≤ y"
and star_inductr: "z + y ⋅⇘i⇙ x ≤ y ⟹ z ⋅⇘i⇙ star i x ≤ y"
class idomain_semiring = idioid + idom_op +
assumes do_absorb: "x ≤ do i x ⋅⇘i⇙ x"
and do_local: "do i (x ⋅⇘i⇙ do i y) = do i (x ⋅⇘i⇙ y)"
and do_add: "do i (x + y) = do i x + do i y"
and do_subid: "do i x ≤ un i"
and do_zero: "do i 0 = 0"
class icodomain_semiring = idioid + icod_op +
assumes cd_absorb: "x ≤ x ⋅⇘i⇙ cd i x"
and cd_local: "cd i (cd i x ⋅⇘i⇙ y) = cd i (x ⋅⇘i⇙ y)"
and cd_add: "cd i (x + y) = cd i x + cd i y"
and cd_subid: "cd i x ≤ un i"
and cd_zero: "cd i 0 = 0"
class imodal_semiring = idomain_semiring + icodomain_semiring +
assumes dc_compat: "do i (cd i x) = cd i x"
and cd_compat: "cd i (do i x) = do i x"
class imodal_kleene_algebra = imodal_semiring + ikleene_algebra
sublocale imonoid_mult ⊆ mm: monoid_mult "un i" "λx y. x ⋅⇘i⇙ y"
by (unfold_locales, simp_all add: local.assoc local.comp_unl local.comp_unr)
sublocale idioid ⊆ di: dioid_one_zero _ "λx y. x ⋅⇘i⇙ y" "un i" _ _ _
by (unfold_locales, simp_all add: local.distl local.distr annil annir)
sublocale idioid ⊆ ddi: idioid _ _ _ _"λx i y. icomp y i x" _
by unfold_locales (simp_all add: local.mm.mult_assoc local.distl)