Theory Kleene_Algebra.Conway
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⇧†"
oops
lemma "y ⋅ x⇧† = y + y ⋅ x ⋅ x⇧†"
oops
lemma "(x + y)⇧† = x⇧† ⋅ (y ⋅ x⇧†)⇧†"
oops
lemma "(x⇧†)⇧† = x⇧†"
oops
lemma "(1 + x)⇧⋆ = x⇧⋆"
oops
lemma "x⇧† ⋅ x = x ⋅ x⇧†"
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"
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"
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⇧†"
oops
lemma "(x⇧†)⇧† = x⇧†"
oops
lemma dagger_denest_var [simp]: "(x + y)⇧† = (x⇧† ⋅ y⇧†)⇧†"
oops
lemma star2 [simp]: "(1 + x)⇧† = x⇧†"
oops
end
end