Theory KAD.Range_Semiring

(* Title:      Range and Antirange Semirings
   Author:     Victor B. F. Gomes, Walter Guttmann, Peter Höfner, Georg Struth, Tjark Weber
   Maintainer: Walter Guttmann <walter.guttman at canterbury.ac.nz>
               Georg Struth <g.struth at sheffield.ac.uk>
               Tjark Weber <tjark.weber at it.uu.se>
*)

section ‹Range and Antirange Semirings›

theory Range_Semiring
imports Antidomain_Semiring
begin

subsection ‹Range Semirings›

text ‹We set up the duality between domain and antidomain semirings on the one hand and range and antirange semirings on the other hand.›

class range_op =
  fixes range_op :: "'a ⇒ 'a" (‹r›)

class range_semiring = semiring_one_zero + plus_ord + range_op +
  assumes rsr1 [simp]: "x + (x ⋅ r x) = x ⋅ r x"
  and rsr2 [simp]: "r (r x ⋅ y) = r(x ⋅ y)"
  and rsr3 [simp]: "r x + 1 = 1"
  and rsr4 [simp]: "r 0 = 0"
  and rsr5 [simp]: "r (x + y) = r x + r y"

begin

definition bd :: "'a ⇒ 'a ⇒ 'a" (‹⟨_| _› [61,81] 82) where
  "⟨x| y = r (y ⋅ x)"

no_notation range_op (‹r›)

end

sublocale range_semiring ⊆ rdual: domain_semiring "(+)" "λx y. y ⋅ x" 1 0 range_op "(≤)" "(<)"
  rewrites "rdual.fd x y = ⟨x| y"
proof -
  show "class.domain_semiring (+) (λx y. y ⋅ x) 1 0 range_op (≤) (<)"
    by (standard, auto simp: mult_assoc distrib_left)
  then interpret rdual: domain_semiring "(+)" "λx y. y ⋅ x" 1 0 range_op "(≤)" "(<)" .
  show "rdual.fd x y = ⟨x| y"
    unfolding rdual.fd_def bd_def by auto
qed

sublocale domain_semiring ⊆ ddual: range_semiring "(+)" "λx y. y ⋅ x" 1 0 domain_op "(≤)" "(<)"
  rewrites "ddual.bd x y = domain_semiringl_class.fd x y"
proof -
  show "class.range_semiring (+) (λx y. y ⋅ x) 1 0 domain_op (≤) (<)"
    by (standard, auto simp: mult_assoc distrib_left)
  then interpret ddual: range_semiring "(+)" "λx y. y ⋅ x" 1 0 domain_op "(≤)" "(<)" .
  show "ddual.bd x y = domain_semiringl_class.fd x y"
    unfolding ddual.bd_def fd_def by auto
qed

subsection ‹Antirange Semirings›

class antirange_op =
  fixes antirange_op :: "'a ⇒ 'a" (‹ar _› [999] 1000)

class antirange_semiring = semiring_one_zero + plus_ord + antirange_op +
  assumes ars1 [simp]: "x ⋅ ar x = 0"
  and ars2 [simp]: "ar (x ⋅ y) + ar (ar ar x ⋅ y) = ar (ar ar x ⋅ y)"
  and ars3 [simp]: "ar ar x + ar x = 1"

begin

no_notation bd (‹⟨_| _› [61,81] 82)

definition ars_r :: "'a ⇒ 'a" (‹r›) where
  "r x = ar (ar x)"

definition bdia :: "'a ⇒ 'a ⇒ 'a" (‹⟨_| _› [61,81] 82) where
  "⟨x| y = ar ar (y ⋅ x)"

definition bbox :: "'a ⇒ 'a ⇒ 'a" (‹[_| _› [61,81] 82) where
  "[x| y = ar (ar y ⋅ x)"

end

sublocale antirange_semiring ⊆ ardual: antidomain_semiring antirange_op "(+)" "λx y. y ⋅ x" 1 0 "(≤)" "(<)"
  rewrites "ardual.ads_d x = r x"
  and "ardual.fdia x y = ⟨x| y"
  and "ardual.fbox x y = [x| y"
proof -
  show "class.antidomain_semiring antirange_op (+) (λx y. y ⋅ x) 1 0 (≤) (<)"
    by (standard, auto simp: mult_assoc distrib_left)
  then interpret ardual: antidomain_semiring antirange_op "(+)" "λx y. y ⋅ x" 1 0 "(≤)" "(<)" .
  show "ardual.ads_d x = r x"
    by (simp add: ardual.ads_d_def local.ars_r_def)
  show "ardual.fdia x y = ⟨x| y"
    unfolding ardual.fdia_def bdia_def by auto
  show "ardual.fbox x y = [x| y"
    unfolding ardual.fbox_def bbox_def by auto
qed

context antirange_semiring

begin

sublocale rs: range_semiring "(+)" "(⋅)" 1 0 "λx. ar ar x" "(≤)" "(<)"
  by unfold_locales

end

sublocale antidomain_semiring ⊆ addual: antirange_semiring "(+)" "λx y. y ⋅ x" 1 0 antidomain_op "(≤)" "(<)"
  rewrites "addual.ars_r x = d x"
  and "addual.bdia x y = |x⟩ y"
  and "addual.bbox x y = |x] y"
proof -
  show "class.antirange_semiring (+) (λx y. y ⋅ x) 1 0 antidomain_op (≤) (<)"
    by (standard, auto simp: mult_assoc distrib_left)
  then interpret addual: antirange_semiring "(+)" "λx y. y ⋅ x" 1 0 antidomain_op "(≤)" "(<)" .
  show "addual.ars_r x = d x"
    by (simp add: addual.ars_r_def local.ads_d_def)
  show "addual.bdia x y = |x⟩ y"
    unfolding addual.bdia_def fdia_def by auto
  show "addual.bbox x y = |x] y"
    unfolding addual.bbox_def fbox_def by auto
qed

subsection ‹Antirange Kleene Algebras›

class antirange_kleene_algebra = antirange_semiring + kleene_algebra

sublocale antirange_kleene_algebra ⊆ dual: antidomain_kleene_algebra antirange_op "(+)" "λx y. y ⋅ x" 1 0 "(≤)" "(<)" "star"
  by (standard, auto simp: local.star_inductr' local.star_inductl)


sublocale antidomain_kleene_algebra ⊆ dual: antirange_kleene_algebra "(+)" "λx y. y ⋅ x" 1 0 "(≤)" "(<)" "star" antidomain_op
  by (standard, simp_all add: star_inductr star_inductl)

text ‹Hence all range theorems have been derived by duality in a generic way.›

end