Quelle  Conway.thy

(* 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)^\<dagger> = (x^\<dagger> ⋅ y)^\<dagger> ⋅ x^\<dagger>"
  and dagger_prod_unfold [simp]: "1 + x ⋅ (y ⋅ x)^\<dagger> ⋅ y = (x ⋅ y)^\<dagger>"

begin

lemma dagger_unfoldl_eq [simp]: "1 + x ⋅ x^\<dagger> = x^\<dagger>"
  by (metis dagger_prod_unfold mult_1_left mult_1_right)

lemma dagger_unfoldl: "1 + x ⋅ x^\<dagger> ≤ x^\<dagger>"
  by auto

lemma dagger_unfoldr_eq [simp]: "1 + x^\<dagger> ⋅ x = x^\<dagger>"
  by (metis dagger_prod_unfold mult_1_right mult_1_left)

lemma dagger_unfoldr: "1 + x^\<dagger> ⋅ x ≤ x^\<dagger>"
  by auto

lemma dagger_unfoldl_distr [simp]: "y + x ⋅ x^\<dagger> ⋅ y = x^\<dagger> ⋅ y"
  by (metis distrib_right' mult_1_left dagger_unfoldl_eq)

lemma dagger_unfoldr_distr [simp]: "y + x^\<dagger> ⋅ x ⋅ y = x^\<dagger> ⋅ y"
  by (metis dagger_unfoldr_eq distrib_right' mult_1_left mult.assoc)

lemma dagger_refl: "1 ≤ x^\<dagger>"
  using dagger_unfoldl local.join.sup.bounded_iff by blast

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

lemma star_1l: "x ⋅ x^\<dagger> ≤ x^\<dagger>"
  using dagger_unfoldl local.join.sup.bounded_iff by blast

lemma star_1r: "x^\<dagger> ⋅ x ≤ x^\<dagger>"
  using dagger_unfoldr local.join.sup.bounded_iff by blast

lemma dagger_ext: "x ≤ x^\<dagger>"
  by (metis dagger_unfoldl_distr local.join.sup.boundedE star_1r)

lemma dagger_trans_eq [simp]: "x^\<dagger> ⋅ x^\<dagger> = x^\<dagger>"
  by (metis dagger_unfoldr_eq local.dagger_denest local.join.sup.idem mult_assoc)

lemma dagger_subdist:  "x^\<dagger> ≤ (x + y)^\<dagger>"
  by (metis dagger_unfoldr_distr local.dagger_denest local.order_prop)

lemma dagger_subdist_var:  "x^\<dagger> + y^\<dagger> ≤ (x + y)^\<dagger>"
  using dagger_subdist local.join.sup_commute by fastforce

lemma dagger_iso [intro]: "x ≤ y ==> x^\<dagger> ≤ y^\<dagger>"
  by (metis less_eq_def dagger_subdist)

lemma star_square: "(x ⋅ x)^\<dagger> ≤ x^\<dagger>"
  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^\<dagger> ⋅ x^\<dagger> = x^\<dagger>"
  by (simp add: local.dagger_ext local.dagger_refl local.join.sup_absorb2)

text ‹Nitpick refutes the next lemmas.›

lemma " y + y ⋅ x^\<dagger> ⋅ x = y ⋅ x^\<dagger>"
(*nitpick [expect=genuine]*)
  oops

lemma "y ⋅ x^\<dagger> = y + y ⋅ x ⋅ x^\<dagger>"
(*nitpick [expect=genuine]*)
  oops

lemma "(x + y)^\<dagger> = x^\<dagger> ⋅ (y ⋅ x^\<dagger>)^\<dagger>"
(*nitpick [expect=genuine]*)
  oops

lemma "(x^\<dagger>)^\<dagger> = x^\<dagger>"
(*nitpick [expect=genuine]*)
oops

lemma "(1 + x)^\<star> = x^\<star>"
(*nitpick [expect = genuine]*)
oops

lemma "x^\<dagger> ⋅ x = x ⋅ x^\<dagger>"
(*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^\<dagger> ⋅ y^\<dagger> ≤ (x + y)^\<dagger>"
  using local.dagger_subdist_var local.mult_isol_var by fastforce

lemma dagger_subdist_var_2: "x ⋅ y ≤ (x + y)^\<dagger>"
  by (meson dagger_subdist_var_3 local.dagger_ext local.mult_isol_var local.order.trans)

lemma dagger_sum_unfold [simp]: "x^\<dagger> + x^\<dagger> ⋅ y ⋅ (x + y)^\<dagger> = (x + y)^\<dagger>"
  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)^\<dagger> ⋅ z = x^\<dagger> ⋅ (y ⋅ (x + y)^\<dagger> ⋅ z + z)"
proof -
  have "(x + y)^\<dagger> ⋅ z = x^\<dagger> ⋅ z + x^\<dagger> ⋅ y ⋅ (x + y)^\<dagger> ⋅ 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^\<dagger> ⋅ x ≤ x ⋅ x^\<dagger>"
  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^\<dagger> ⋅ x = x ⋅ x^\<dagger>"
  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)^\<dagger> ⋅ x = x ⋅ (y ⋅ x)^\<dagger>"
proof -
  have "(x ⋅ y)^\<dagger> ⋅ x = x + x ⋅ (y ⋅ x)^\<dagger> ⋅ y ⋅ x"
    by (metis local.dagger_prod_unfold local.distrib_right' local.mult_onel)
  also have "... = x ⋅ (1 + (y ⋅ x)^\<dagger> ⋅ 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)^\<dagger>"
  by (metis annil dagger_unfoldl_eq mult.assoc)

lemma zero_dagger [simp]: "0^\<dagger> = 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^\<dagger> ≤ y^\<dagger> ⋅ 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^\<dagger> ≤ y^\<dagger> ⋅ z"

begin

lemma dagger_slide_var: "x ⋅ (y ⋅ x)^\<dagger> ≤ (x ⋅ y)^\<dagger> ⋅ x"
  by (metis eq_refl dagger_simr mult.assoc)

text ‹Nitpick refutes the next lemma.›

lemma dagger_slide: "x ⋅ (y ⋅ x)^\<dagger> = (x ⋅ y)^\<dagger> ⋅ 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^\<dagger> ≤ (x ⋅ y + z)^\<dagger> ⋅ 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)^\<dagger> = (x ⋅ y)^\<dagger> ⋅ 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)^\<dagger> = x^\<dagger> ⋅ (y ⋅ x^\<dagger>)^\<dagger>"
  by (metis dagger_denest dagger_slide)

lemma preservation2: "y ⋅ x ≤ y ==> (x ⋅ y)^\<dagger> ⋅ x ≤ x ⋅ y^\<dagger>"
  by (metis dagger_slide local.dagger_iso local.mult_isol)

lemma preservation1_eq: "x ⋅ y ≤ x ⋅ y ⋅ x ==> y ⋅ x ≤ y ==> (x ⋅ y)^\<dagger> ⋅ x = x ⋅ y^\<dagger>"
  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^\<dagger>"
(*nitpick [expect=genuine]*)
oops

lemma "(x^\<dagger>)^\<dagger> = x^\<dagger>"
(*nitpick [expect=genuine]*)
oops

lemma dagger_denest_var [simp]: "(x + y)^\<dagger> = (x^\<dagger> ⋅ y^\<dagger>)^\<dagger>"
(* nitpick [expect=genuine]*)
oops

lemma star2 [simp]: "(1 + x)^\<dagger> = x^\<dagger>"
(*nitpick [expect=genuine]*)
oops

end

end