Theory Conway

(* Title:      Conway Algebra
   Author:     Alasdair Armstrong, Victor B. F. Gomes, Georg Struth
   Maintainer: Georg Struth <g.struth at sheffield.ac.uk>
               Tjark Weber <tjark.weber at it.uu.se>
*)

section ‹Conway Algebras›

theory Conway
  imports Dioid
begin

text ‹
  We define a weak regular algebra which can serve as a common basis for Kleene algebra and demonic reginement algebra.
  It is closely related to an axiomatisation given by Conway~cite"conway71regular". 
›

class dagger_op =
  fixes dagger :: "'a  'a" ("_" [101] 100)

subsection‹Near Conway Algebras›

class near_conway_base = near_dioid_one + dagger_op +
  assumes dagger_denest: "(x + y) = (x  y)  x"
  and dagger_prod_unfold [simp]: "1 + x  (y  x)  y = (x  y)"

begin

lemma dagger_unfoldl_eq [simp]: "1 + x  x = x"
  by (metis dagger_prod_unfold mult_1_left mult_1_right)

lemma dagger_unfoldl: "1 + x  x  x"
  by auto

lemma dagger_unfoldr_eq [simp]: "1 + x  x = x"
  by (metis dagger_prod_unfold mult_1_right mult_1_left)

lemma dagger_unfoldr: "1 + x  x  x"
  by auto

lemma dagger_unfoldl_distr [simp]: "y + x  x  y = x  y"
  by (metis distrib_right' mult_1_left dagger_unfoldl_eq)

lemma dagger_unfoldr_distr [simp]: "y + x  x  y = x  y"
  by (metis dagger_unfoldr_eq distrib_right' mult_1_left mult.assoc)

lemma dagger_refl: "1  x"
  using dagger_unfoldl local.join.sup.bounded_iff by blast

lemma dagger_plus_one [simp]: "1 + x = x"
  by (simp add: dagger_refl local.join.sup_absorb2)

lemma star_1l: "x  x  x"
  using dagger_unfoldl local.join.sup.bounded_iff by blast

lemma star_1r: "x  x  x"
  using dagger_unfoldr local.join.sup.bounded_iff by blast

lemma dagger_ext: "x  x"
  by (metis dagger_unfoldl_distr local.join.sup.boundedE star_1r)

lemma dagger_trans_eq [simp]: "x  x = x"
  by (metis dagger_unfoldr_eq local.dagger_denest local.join.sup.idem mult_assoc)

lemma dagger_subdist:  "x  (x + y)"
  by (metis dagger_unfoldr_distr local.dagger_denest local.order_prop)

lemma dagger_subdist_var:  "x + y  (x + y)"
  using dagger_subdist local.join.sup_commute by fastforce

lemma dagger_iso [intro]: "x  y  x  y"
  by (metis less_eq_def dagger_subdist)

lemma star_square: "(x  x)  x"
  by (metis dagger_plus_one dagger_subdist dagger_trans_eq dagger_unfoldr_distr dagger_denest
    distrib_right' order.eq_iff join.sup_commute less_eq_def mult_onel mult_assoc)

lemma dagger_rtc1_eq [simp]: "1 + x + x  x = x"
  by (simp add: local.dagger_ext local.dagger_refl local.join.sup_absorb2)

text ‹Nitpick refutes the next lemmas.›

lemma " y + y  x  x = y  x"
(*nitpick [expect=genuine]*)
  oops

lemma "y  x = y + y  x  x"
(*nitpick [expect=genuine]*)
  oops

lemma "(x + y) = x  (y  x)"
(*nitpick [expect=genuine]*)
  oops

lemma "(x) = x"
(*nitpick [expect=genuine]*)
oops

lemma "(1 + x) = x"
(*nitpick [expect = genuine]*)
oops

lemma "x  x = x  x"
(*nitpick [expect=genuine]*)
oops

end

subsection‹Pre-Conway Algebras›

class pre_conway_base = near_conway_base + pre_dioid_one

begin

lemma dagger_subdist_var_3: "x  y  (x + y)"
  using local.dagger_subdist_var local.mult_isol_var by fastforce

lemma dagger_subdist_var_2: "x  y  (x + y)"
  by (meson dagger_subdist_var_3 local.dagger_ext local.mult_isol_var local.order.trans)

lemma dagger_sum_unfold [simp]: "x + x  y  (x + y) = (x + y)"
  by (metis local.dagger_denest local.dagger_unfoldl_distr mult_assoc)

end

subsection ‹Conway Algebras›

class conway_base = pre_conway_base + dioid_one

begin

lemma troeger: "(x + y)  z = x  (y  (x + y)  z + z)"
proof -
  have "(x + y)  z = x  z + x  y  (x + y)  z"
    by (metis dagger_sum_unfold local.distrib_right')
  thus ?thesis
   by (metis add_commute local.distrib_left mult_assoc)
qed

lemma dagger_slide_var1: "x  x  x  x"
  by (metis local.dagger_unfoldl_distr local.dagger_unfoldr_eq local.distrib_left order.eq_iff local.mult_1_right mult_assoc)

lemma dagger_slide_var1_eq: "x  x = x  x"
  by (metis local.dagger_unfoldl_distr local.dagger_unfoldr_eq local.distrib_left local.mult_1_right mult_assoc)

lemma dagger_slide_eq: "(x  y)  x = x  (y  x)"
proof -
  have "(x  y)  x = x + x  (y  x)  y  x"
    by (metis local.dagger_prod_unfold local.distrib_right' local.mult_onel)
  also have "... = x  (1 + (y  x)  y  x)"
    using local.distrib_left local.mult_1_right mult_assoc by presburger
  finally show ?thesis
    by (simp add: mult_assoc)
qed

end

subsection ‹Conway Algebras with  Zero›

class near_conway_base_zerol = near_conway_base + near_dioid_one_zerol

begin

lemma dagger_annil [simp]: "1 + x  0 = (x  0)"
  by (metis annil dagger_unfoldl_eq mult.assoc)

lemma zero_dagger [simp]: "0 = 1"
  by (metis add_0_right annil dagger_annil)

end

class pre_conway_base_zerol = near_conway_base_zerol + pre_dioid

class conway_base_zerol = pre_conway_base_zerol + dioid

subclass (in pre_conway_base_zerol) pre_conway_base ..

subclass (in conway_base_zerol) conway_base ..

context conway_base_zerol
begin

lemma "z  x  y  z  z  x  y  z"
(*nitpick [expect=genuine]*)
oops 

end

subsection ‹Conway Algebras with Simulation›

class near_conway = near_conway_base +
  assumes dagger_simr: "z  x  y  z  z  x  y  z"

begin

lemma dagger_slide_var: "x  (y  x)  (x  y)  x"
  by (metis eq_refl dagger_simr mult.assoc)

text ‹Nitpick refutes the next lemma.›

lemma dagger_slide: "x  (y  x) = (x  y)  x"
(*nitpick [expect=genuine]*)
  oops

text ‹
  We say that $y$ preserves $x$ if $x \cdot y \cdot x = x \cdot y$ and $!x \cdot y \cdot !x = !x \cdot y$. This definition is taken
  from Solin~cite"Solin11". It is useful for program transformation.
›
  
lemma preservation1: "x  y  x  y  x  x  y  (x  y + z)  x"
proof -
  assume "x  y  x  y  x"
  hence "x  y  (x  y + z)  x"
    by (simp add: local.join.le_supI1)
  thus ?thesis
    by (simp add: local.dagger_simr)
qed

end

class near_conway_zerol = near_conway + near_dioid_one_zerol

class pre_conway = near_conway + pre_dioid_one

begin

subclass pre_conway_base ..

lemma dagger_slide: "x  (y  x) = (x  y)  x"
  by (metis add.commute dagger_prod_unfold join.sup_least mult_1_right mult.assoc subdistl dagger_slide_var dagger_unfoldl_distr order.antisym)

lemma dagger_denest2: "(x + y) = x  (y  x)"
  by (metis dagger_denest dagger_slide)

lemma preservation2: "y  x  y  (x  y)  x  x  y"
  by (metis dagger_slide local.dagger_iso local.mult_isol)

lemma preservation1_eq: "x  y  x  y  x  y  x  y  (x  y)  x = x  y"
  by (simp add: local.dagger_simr order.eq_iff preservation2)

end

class pre_conway_zerol = near_conway_zerol + pre_dioid_one_zerol

begin

subclass pre_conway ..

end

class conway = pre_conway + dioid_one

class conway_zerol = pre_conway + dioid_one_zerol

begin

subclass conway_base ..

text ‹Nitpick refutes the next lemmas.›

lemma "1 = 1"
(*nitpick [expect=genuine]*)
oops

lemma "(x) = x"
(*nitpick [expect=genuine]*)
oops

lemma dagger_denest_var [simp]: "(x + y) = (x  y)"
(* nitpick [expect=genuine]*)
oops

lemma star2 [simp]: "(1 + x) = x"
(*nitpick [expect=genuine]*)
oops

end

end