# Theory General_Refinement_Algebras

```(* Title:      General Refinement Algebras
Author:     Walter Guttmann
Maintainer: Walter Guttmann <walter.guttmann at canterbury.ac.nz>
*)

section ‹General Refinement Algebras›

theory General_Refinement_Algebras

imports Omega_Algebras

begin

class general_refinement_algebra = left_kleene_algebra + Omega +
assumes Omega_unfold: "y⇧Ω ≤ 1 ⊔ y * y⇧Ω"
assumes Omega_induct: "x ≤ z ⊔ y * x ⟶ x ≤ y⇧Ω * z"
begin

lemma Omega_unfold_equal:
"y⇧Ω = 1 ⊔ y * y⇧Ω"
by (smt Omega_induct Omega_unfold sup_right_isotone order.antisym mult_right_isotone mult_1_right)

lemma Omega_sup_1:
"(x ⊔ y)⇧Ω = x⇧Ω * (y * x⇧Ω)⇧Ω"
apply (rule order.antisym)
apply (smt Omega_induct Omega_unfold_equal sup_assoc sup_commute sup_right_isotone mult_assoc mult_right_dist_sup mult_right_isotone mult_1_right order_refl)
by (smt Omega_induct Omega_unfold_equal sup_assoc sup_commute mult_assoc mult_left_one mult_right_dist_sup mult_1_right order_refl)

lemma Omega_left_slide:
"(x * y)⇧Ω * x ≤ x * (y * x)⇧Ω"
proof -
have "1 ⊔ y * (x * y)⇧Ω * x ≤ 1 ⊔ y * x * (1 ⊔ (y * (x * y)⇧Ω) * x)"
by (smt Omega_unfold_equal sup_right_isotone mult_assoc mult_left_one mult_left_sub_dist_sup mult_right_dist_sup mult_right_isotone mult_1_right)
thus ?thesis
by (smt Omega_induct Omega_unfold_equal le_sup_iff mult_assoc mult_left_one mult_right_dist_sup mult_right_isotone mult_1_right)
qed

end

text ‹Theorem 50.3›

sublocale general_refinement_algebra < Omega: left_conway_semiring where circ = Omega
apply unfold_locales
using Omega_unfold_equal apply simp

context general_refinement_algebra
begin

lemma star_below_Omega:
"x⇧⋆ ≤ x⇧Ω"
by (metis Omega_induct mult_1_right order_refl star.circ_left_unfold)

lemma star_mult_Omega:
"x⇧Ω = x⇧⋆ * x⇧Ω"
by (metis Omega.left_plus_below_circ sup_commute sup_ge1 order.eq_iff star.circ_loop_fixpoint star_left_induct_mult_iff)

lemma Omega_one_greatest:
"x ≤ 1⇧Ω"
by (metis Omega_induct sup_bot_left mult_left_one order_refl order_trans zero_right_mult_decreasing)

lemma greatest_left_zero:
"1⇧Ω * x = 1⇧Ω"
by (simp add: Omega_one_greatest Omega_induct order.antisym)

proposition circ_right_unfold: "1 ⊔ x⇧Ω * x = x⇧Ω" nitpick [expect=genuine,card=8] oops
proposition circ_slide: "(x * y)⇧Ω * x = x * (y * x)⇧Ω" nitpick [expect=genuine,card=6] oops
proposition circ_simulate: "z * x ≤ y * z ⟹ z * x⇧Ω ≤ y⇧Ω * z" nitpick [expect=genuine,card=6] oops
proposition circ_simulate_right: "z * x ≤ y * z ⊔ w ⟹ z * x⇧Ω ≤ y⇧Ω * (z ⊔ w * x⇧Ω)" nitpick [expect=genuine,card=6] oops
proposition circ_simulate_right_1: "z * x ≤ y * z ⟹ z * x⇧Ω ≤ y⇧Ω * z" nitpick [expect=genuine,card=6] oops
proposition circ_simulate_right_plus: "z * x ≤ y * y⇧Ω * z ⊔ w ⟹ z * x⇧Ω ≤ y⇧Ω * (z ⊔ w * x⇧Ω)" nitpick [expect=genuine,card=6] oops
proposition circ_simulate_right_plus_1: "z * x ≤ y * y⇧Ω * z ⟹ z * x⇧Ω ≤ y⇧Ω * z" nitpick [expect=genuine,card=6] oops
proposition circ_simulate_left_1: "x * z ≤ z * y ⟹ x⇧Ω * z ≤ z * y⇧Ω ⊔ x⇧Ω * bot" oops (* holds in LKA, counterexample exists in GRA *)
proposition circ_simulate_left_plus_1: "x * z ≤ z * y⇧Ω ⟹ x⇧Ω * z ≤ z * y⇧Ω ⊔ x⇧Ω * bot" oops (* holds in LKA, counterexample exists in GRA *)
proposition circ_simulate_absorb: "y * x ≤ x ⟹ y⇧Ω * x ≤ x ⊔ y⇧Ω * bot" nitpick [expect=genuine,card=8] oops (* holds in LKA, counterexample exists in GRA *)

end

class bounded_general_refinement_algebra = general_refinement_algebra + bounded_left_kleene_algebra
begin

lemma Omega_one:
"1⇧Ω = top"

lemma top_left_zero:
"top * x = top"
using Omega_one greatest_left_zero by blast

end

sublocale bounded_general_refinement_algebra < Omega: bounded_left_conway_semiring where circ = Omega ..

class left_demonic_refinement_algebra = general_refinement_algebra +
assumes Omega_isolate: "y⇧Ω ≤ y⇧Ω * bot ⊔ y⇧⋆"
begin

lemma Omega_isolate_equal:
"y⇧Ω = y⇧Ω * bot ⊔ y⇧⋆"
using Omega_isolate order.antisym le_sup_iff star_below_Omega zero_right_mult_decreasing by auto

proposition Omega_sum_unfold_1: "(x ⊔ y)⇧Ω = y⇧Ω ⊔ y⇧⋆ * x * (x ⊔ y)⇧Ω" oops
proposition Omega_sup_3: "(x ⊔ y)⇧Ω = (x⇧⋆ * y)⇧Ω * x⇧Ω" oops

end

class bounded_left_demonic_refinement_algebra = left_demonic_refinement_algebra + bounded_left_kleene_algebra
begin

proposition Omega_mult: "(x * y)⇧Ω = 1 ⊔ x * (y * x)⇧Ω * y" oops
proposition Omega_sup: "(x ⊔ y)⇧Ω = (x⇧Ω * y)⇧Ω * x⇧Ω" oops
proposition Omega_simulate: "z * x ≤ y * z ⟹ z * x⇧Ω ≤ y⇧Ω * z" nitpick [expect=genuine,card=6] oops
proposition Omega_separate_2: "y * x ≤ x * (x ⊔ y) ⟹ (x ⊔ y)⇧Ω = x⇧Ω * y⇧Ω" oops
proposition Omega_circ_simulate_right_plus: "z * x ≤ y * y⇧Ω * z ⊔ w ⟹ z * x⇧Ω ≤ y⇧Ω * (z ⊔ w * x⇧Ω)" nitpick [expect=genuine,card=6] oops
proposition Omega_circ_simulate_left_plus: "x * z ≤ z * y⇧Ω ⊔ w ⟹ x⇧Ω * z ≤ (z ⊔ x⇧Ω * w) * y⇧Ω" oops

end

sublocale bounded_left_demonic_refinement_algebra < Omega: bounded_left_conway_semiring where circ = Omega ..

class demonic_refinement_algebra = left_zero_kleene_algebra + left_demonic_refinement_algebra
begin

lemma Omega_mult:
"(x * y)⇧Ω = 1 ⊔ x * (y * x)⇧Ω * y"
by (smt (verit, del_insts) Omega.circ_left_slide Omega_induct Omega_unfold_equal order.eq_iff mult_assoc mult_left_dist_sup mult_1_right)

lemma Omega_sup:
"(x ⊔ y)⇧Ω = (x⇧Ω * y)⇧Ω * x⇧Ω"
by (smt Omega_sup_1 Omega_mult mult_assoc mult_left_dist_sup mult_left_one mult_right_dist_sup mult_1_right)

lemma Omega_simulate:
"z * x ≤ y * z ⟹ z * x⇧Ω ≤ y⇧Ω * z"
by (smt Omega_induct Omega_unfold_equal sup_right_isotone mult_assoc mult_left_dist_sup mult_left_isotone mult_1_right)

end

text ‹Theorem 2.4›

sublocale demonic_refinement_algebra < Omega1: itering_1 where circ = Omega
apply unfold_locales

sublocale demonic_refinement_algebra < Omega1: left_zero_conway_semiring_1 where circ = Omega ..

context demonic_refinement_algebra
begin

lemma Omega_sum_unfold_1:
"(x ⊔ y)⇧Ω = y⇧Ω ⊔ y⇧⋆ * x * (x ⊔ y)⇧Ω"
by (smt Omega1.circ_sup_9 Omega.circ_loop_fixpoint Omega_isolate_equal sup_assoc sup_commute mult_assoc mult_left_zero mult_right_dist_sup)

lemma Omega_sup_3:
"(x ⊔ y)⇧Ω = (x⇧⋆ * y)⇧Ω * x⇧Ω"
apply (rule order.antisym)
apply (metis Omega_sum_unfold_1 Omega_induct eq_refl sup_commute)
by (simp add: Omega.circ_isotone Omega_sup mult_left_isotone star_below_Omega)

lemma Omega_separate_2:
"y * x ≤ x * (x ⊔ y) ⟹ (x ⊔ y)⇧Ω = x⇧Ω * y⇧Ω"
apply (rule order.antisym)
apply (smt (verit, del_insts) Omega_induct Omega_sum_unfold_1 sup_right_isotone mult_assoc mult_left_isotone star_mult_Omega star_simulation_left)

lemma Omega_circ_simulate_right_plus:
assumes "z * x ≤ y * y⇧Ω * z ⊔ w"
shows "z * x⇧Ω ≤ y⇧Ω * (z ⊔ w * x⇧Ω)"
proof -
have "z * x⇧Ω = z ⊔ z * x * x⇧Ω"
using Omega1.circ_back_loop_fixpoint Omega1.circ_plus_same sup_commute mult_assoc by auto
also have "... ≤ y * y⇧Ω * z * x⇧Ω ⊔ z ⊔ w * x⇧Ω"
by (smt assms sup_assoc sup_commute sup_right_isotone le_iff_sup mult_right_dist_sup)
finally have "z * x⇧Ω ≤ (y * y⇧Ω)⇧Ω * (z ⊔ w * x⇧Ω)"
by (smt Omega_induct sup_assoc sup_commute mult_assoc)
thus ?thesis
qed

lemma Omega_circ_simulate_left_plus:
assumes "x * z ≤ z * y⇧Ω ⊔ w"
shows "x⇧Ω * z ≤ (z ⊔ x⇧Ω * w) * y⇧Ω"
proof -
have "x * ((z ⊔ x⇧Ω * w) * y⇧Ω) ≤ (z * y⇧Ω ⊔ w ⊔ x * x⇧Ω * w) * y⇧Ω"
by (smt assms mult_assoc mult_left_dist_sup sup_left_isotone mult_left_isotone)
also have "... ≤ z * y⇧Ω * y⇧Ω ⊔ w * y⇧Ω ⊔ x⇧Ω * w * y⇧Ω"
by (smt Omega.left_plus_below_circ sup_right_isotone mult_left_isotone mult_right_dist_sup)
finally have 1: "x * ((z ⊔ x⇧Ω * w) * y⇧Ω) ≤ (z ⊔ x⇧Ω * w) * y⇧Ω"
by (metis Omega.circ_transitive_equal mult_assoc Omega.circ_reflexive sup_assoc le_iff_sup mult_left_one mult_right_dist_sup)
have "x⇧Ω * z  = x⇧Ω * bot ⊔ x⇧⋆ * z"
by (metis Omega_isolate_equal mult_assoc mult_left_zero mult_right_dist_sup)
also have "... ≤ x⇧Ω * w * y⇧Ω ⊔ x⇧⋆ * (z ⊔ x⇧Ω * w) * y⇧Ω"
by (metis Omega1.circ_back_loop_fixpoint bot_least idempotent_bot_closed le_supI2 mult_isotone mult_left_sub_dist_sup_left semiring.add_mono zero_right_mult_decreasing mult_assoc)
also have "... ≤ (z ⊔ x⇧Ω * w) * y⇧Ω"
using 1 by (metis le_supI mult_right_sub_dist_sup_right star_left_induct_mult mult_assoc)
finally show ?thesis
.
qed

lemma Omega_circ_simulate_right:
assumes "z * x ≤ y * z ⊔ w"
shows "z * x⇧Ω ≤ y⇧Ω * (z ⊔ w * x⇧Ω)"
proof -
have "y * z ⊔ w ≤ y * y⇧Ω * z ⊔ w"
using Omega.circ_mult_increasing mult_left_isotone sup_left_isotone by auto
thus ?thesis
using Omega_circ_simulate_right_plus assms order.trans by blast
qed

end

sublocale demonic_refinement_algebra < Omega: itering where circ = Omega
apply unfold_locales
using Omega_mult apply blast
using Omega_circ_simulate_left_plus by auto

class bounded_demonic_refinement_algebra = demonic_refinement_algebra + bounded_left_zero_kleene_algebra
begin

lemma Omega_one:
"1⇧Ω = top"

lemma top_left_zero:
"top * x = top"
using Omega_one greatest_left_zero by auto

end

sublocale bounded_demonic_refinement_algebra < Omega: bounded_itering where circ = Omega ..

class general_refinement_algebra_omega = left_omega_algebra + Omega +
assumes omega_left_zero: "x⇧ω ≤ x⇧ω * y"
assumes Omega_def: "x⇧Ω = x⇧ω ⊔ x⇧⋆"
begin

lemma omega_left_zero_equal:
"x⇧ω * y = x⇧ω"
by (simp add: order.antisym omega_left_zero omega_sub_vector)

subclass left_demonic_refinement_algebra
apply unfold_locales
apply (metis Omega_def sup_commute eq_refl mult_1_right omega_loop_fixpoint)
apply (metis Omega_def mult_right_dist_sup omega_induct omega_left_zero_equal)
by (metis Omega_def mult_right_sub_dist_sup_right sup_commute sup_right_isotone omega_left_zero_equal)

end

class left_demonic_refinement_algebra_omega = bounded_left_omega_algebra + Omega +
assumes top_left_zero: "top * x = top"
assumes Omega_def: "x⇧Ω = x⇧ω ⊔ x⇧⋆"
begin

subclass general_refinement_algebra_omega
apply unfold_locales
apply (metis mult_assoc omega_vector order_refl top_left_zero)
by (rule Omega_def)

end

class demonic_refinement_algebra_omega = left_demonic_refinement_algebra_omega + bounded_left_zero_omega_algebra
begin

lemma Omega_mult:
"(x * y)⇧Ω = 1 ⊔ x * (y * x)⇧Ω * y"
by (metis Omega_def comb1.circ_mult_1 omega_left_zero_equal omega_translate)

lemma Omega_sup:
"(x ⊔ y)⇧Ω = (x⇧Ω * y)⇧Ω * x⇧Ω"
proof -
have "(x⇧Ω * y)⇧Ω * x⇧Ω = (x⇧⋆ * y)⇧⋆ * x⇧ω ⊔ (x⇧⋆ * y)⇧ω ⊔ (x⇧⋆ * y)⇧⋆ * x⇧ω⇧⋆ * x⇧Ω"
by (smt sup_commute Omega_def mult_assoc mult_right_dist_sup mult_bot_add_omega omega_left_zero_equal star.circ_sup_1)
thus ?thesis
using Omega_def Omega_sup_1 comb2.circ_slide_1 omega_left_zero_equal by auto
qed

lemma Omega_simulate:
"z * x ≤ y * z ⟹ z * x⇧Ω ≤ y⇧Ω * z"
using Omega_def comb2.circ_simulate omega_left_zero_equal by auto

subclass demonic_refinement_algebra ..

end

(* hold in GRA and LKA *)
proposition circ_circ_mult: "1⇧Ω * x⇧Ω = x⇧Ω⇧Ω" oops
proposition sub_mult_one_circ: "x * 1⇧Ω ≤ 1⇧Ω * x" oops
proposition circ_circ_mult_1: "x⇧Ω * 1⇧Ω = x⇧Ω⇧Ω" oops
proposition "y * x ≤ x ⟹ y⇧∘ * x ≤ 1⇧∘ * x" oops

(* unknown *)
proposition circ_simulate_2: "y * x⇧Ω ≤ x⇧Ω * y⇧Ω ⟷ y⇧Ω * x⇧Ω ≤ x⇧Ω * y⇧Ω" oops (* holds in LKA *)
proposition circ_simulate_3: "y * x⇧Ω ≤ x⇧Ω ⟹ y⇧Ω * x⇧Ω ≤ x⇧Ω * y⇧Ω" oops (* holds in LKA *)
proposition circ_separate_mult_1: "y * x ≤ x * y ⟹ (x * y)⇧Ω ≤ x⇧Ω * y⇧Ω" oops
proposition "x⇧∘ = (x * x)⇧∘ * (x ⊔ 1)" oops
proposition "y⇧∘ * x⇧∘ ≤ x⇧∘ * y⇧∘ ⟹ (x ⊔ y)⇧∘ = x⇧∘ * y⇧∘" oops
proposition "y * x ≤ (1 ⊔ x) * y⇧∘ ⟹ (x ⊔ y)⇧∘ = x⇧∘ * y⇧∘" oops

end

```