# Theory Capped_Omega_Algebras

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

section ‹Capped Omega Algebras›

theory Capped_Omega_Algebras

imports Omega_Algebras

begin

class capped_omega =
fixes capped_omega :: "'a ⇒ 'a ⇒ 'a" ("_⇧ω⇩_" [100,100] 100)

class capped_omega_algebra = bounded_left_zero_kleene_algebra + bounded_distrib_lattice + capped_omega +
assumes capped_omega_unfold: "y⇧ω⇩v = y * y⇧ω⇩v ⊓ v"
assumes capped_omega_induct: "x ≤ (y * x ⊔ z) ⊓ v ⟶ x ≤ y⇧ω⇩v ⊔ y⇧⋆ * z"

text ‹AACP Theorem 6.1›

notation
top ("⊤")

sublocale capped_omega_algebra < capped: bounded_left_zero_omega_algebra where omega = "(λy . y⇧ω⇩⊤)"
apply unfold_locales
apply (metis capped_omega_unfold inf_top_right)

context capped_omega_algebra
begin

text ‹AACP Theorem 6.2›

lemma capped_omega_below_omega:
"y⇧ω⇩v ≤ y⇧ω⇩⊤"
using capped.omega_induct_mult capped_omega_unfold order.eq_iff by force

text ‹AACP Theorem 6.3›

lemma capped_omega_below:
"y⇧ω⇩v ≤ v"
using capped_omega_unfold order.eq_iff by force

text ‹AACP Theorem 6.4›

lemma capped_omega_one:
"1⇧ω⇩v = v"
proof -
have "v ≤ (1 * v ⊔ bot) ⊓ v"
by simp
hence "v ≤ 1⇧ω⇩v ⊔ 1⇧⋆ * bot"
also have "... = 1⇧ω⇩v"
finally show ?thesis
qed

text ‹AACP Theorem 6.5›

lemma capped_omega_zero:
"bot⇧ω⇩v = bot"
by (metis capped_omega_below_omega bot_unique capped.omega_bot)

lemma star_below_cap:
"y ≤ u ⟹ z ≤ v ⟹ u * v ≤ v ⟹ y⇧⋆ * z ≤ v"
by (metis le_sup_iff order.trans mult_left_isotone star_left_induct)

lemma capped_fix:
assumes "y ≤ u"
and "z ≤ v"
and "u * v ≤ v"
shows "(y * (y⇧ω⇩v ⊔ y⇧⋆ * z) ⊔ z) ⊓ v = y⇧ω⇩v ⊔ y⇧⋆ * z"
proof -
have "(y * (y⇧ω⇩v ⊔ y⇧⋆ * z) ⊔ z) ⊓ v = (y * y⇧ω⇩v ⊔ y⇧⋆ * z) ⊓ v"
by (simp add: mult_left_dist_sup star.circ_loop_fixpoint sup_assoc)
also have "... = (y * y⇧ω⇩v ⊓ v) ⊔ (y⇧⋆ * z ⊓ v)"
also have "... = y⇧ω⇩v ⊔ y⇧⋆ * z"
using assms capped_omega_unfold le_iff_inf star_below_cap by auto
finally show ?thesis
.
qed

lemma capped_fixpoint:
"y ≤ u ⟹ z ≤ v ⟹ u * v ≤ v ⟹ is_fixpoint (λx . (y * x ⊔ z) ⊓ v) (y⇧ω⇩v ⊔ y⇧⋆ * z)"

lemma capped_greatest_fixpoint:
"y ≤ u ⟹ z ≤ v ⟹ u * v ≤ v ⟹ is_greatest_fixpoint (λx . (y * x ⊔ z) ⊓ v) (y⇧ω⇩v ⊔ y⇧⋆ * z)"
by (smt capped_fix order_refl capped_omega_induct is_greatest_fixpoint_def)

lemma capped_postfixpoint:
"y ≤ u ⟹ z ≤ v ⟹ u * v ≤ v ⟹ is_postfixpoint (λx . (y * x ⊔ z) ⊓ v) (y⇧ω⇩v ⊔ y⇧⋆ * z)"
using capped_fix inf.eq_refl is_postfixpoint_def by auto

lemma capped_greatest_postfixpoint:
"y ≤ u ⟹ z ≤ v ⟹ u * v ≤ v ⟹ is_greatest_postfixpoint (λx . (y * x ⊔ z) ⊓ v) (y⇧ω⇩v ⊔ y⇧⋆ * z)"
by (smt capped_fix order_refl capped_omega_induct is_greatest_postfixpoint_def)

text ‹AACP Theorem 6.6›

lemma capped_nu:
"y ≤ u ⟹ z ≤ v ⟹ u * v ≤ v ⟹ ν(λx . (y * x ⊔ z) ⊓ v) = y⇧ω⇩v ⊔ y⇧⋆ * z"
by (metis capped_greatest_fixpoint greatest_fixpoint_same)

lemma capped_pnu:
"y ≤ u ⟹ z ≤ v ⟹ u * v ≤ v ⟹ pν(λx . (y * x ⊔ z) ⊓ v) = y⇧ω⇩v ⊔ y⇧⋆ * z"
by (metis capped_greatest_postfixpoint greatest_postfixpoint_same)

text ‹AACP Theorem 6.7›

lemma unfold_capped_omega:
"y ≤ u ⟹ u * v ≤ v ⟹ y * y⇧ω⇩v = y⇧ω⇩v"
by (smt (verit, ccfv_SIG) capped_omega_below capped_omega_unfold inf.order_lesseq_imp le_iff_inf mult_isotone)

text ‹AACP Theorem 6.8›

lemma star_mult_capped_omega:
assumes "y ≤ u"
and "u * v ≤ v"
shows "y⇧⋆ * y⇧ω⇩v = y⇧ω⇩v"
proof -
have "y * y⇧ω⇩v = y⇧ω⇩v"
using assms unfold_capped_omega by auto
hence "y⇧⋆ * y⇧ω⇩v ≤ y⇧ω⇩v"
thus ?thesis
by (metis sup_ge2 order.antisym star.circ_loop_fixpoint)
qed

text ‹AACP Theorem 6.9›

lemma star_zero_below_capped_omega_zero:
assumes "y ≤ u"
and "u * v ≤ v"
shows "y⇧⋆ * bot ≤ y⇧ω⇩v * bot"
proof -
have "y * y⇧ω⇩v ≤ v"
using assms capped_omega_below unfold_capped_omega by auto
hence "y * y⇧ω⇩v = y⇧ω⇩v"
using assms unfold_capped_omega by auto
thus ?thesis
by (metis bot_least eq_refl mult_assoc star_below_cap)
qed

lemma star_zero_below_capped_omega:
"y ≤ u ⟹ u * v ≤ v ⟹ y⇧⋆ * bot ≤ y⇧ω⇩v"

lemma capped_omega_induct_meet_zero:
"x ≤ y * x ⊓ v ⟹ x ≤ y⇧ω⇩v ⊔ y⇧⋆ * bot"

text ‹AACP Theorem 6.10›

lemma capped_omega_induct_meet:
"y ≤ u ⟹ u * v ≤ v ⟹ x ≤ y * x ⊓ v ⟹ x ≤ y⇧ω⇩v"
by (metis capped_omega_induct_meet_zero sup_commute le_iff_sup star_zero_below_capped_omega)

lemma capped_omega_induct_equal:
"x = (y * x ⊔ z) ⊓ v ⟹ x ≤ y⇧ω⇩v ⊔ y⇧⋆ * z"
using capped_omega_induct inf.le_iff_sup by auto

text ‹AACP Theorem 6.11›

lemma capped_meet_nu:
assumes "y ≤ u"
and "u * v ≤ v"
shows "ν(λx . y * x ⊓ v) = y⇧ω⇩v"
proof -
have "y⇧ω⇩v ⊔ y⇧⋆ * bot = y⇧ω⇩v"
by (smt assms star_zero_below_capped_omega le_iff_sup sup_commute)
hence "ν(λx . (y * x ⊔ bot) ⊓ v) = y⇧ω⇩v"
by (metis assms capped_nu bot_least)
thus ?thesis
by simp
qed

lemma capped_meet_pnu:
assumes "y ≤ u"
and "u * v ≤ v"
shows "pν(λx . y * x ⊓ v) = y⇧ω⇩v"
proof -
have "y⇧ω⇩v ⊔ y⇧⋆ * bot = y⇧ω⇩v"
by (smt assms star_zero_below_capped_omega le_iff_sup sup_commute)
hence "pν(λx . (y * x ⊔ bot) ⊓ v) = y⇧ω⇩v"
by (metis assms capped_pnu bot_least)
thus ?thesis
by simp
qed

text ‹AACP Theorem 6.12›

lemma capped_omega_isotone:
"y ≤ u ⟹ u * v ≤ v ⟹ t ≤ y ⟹ t⇧ω⇩v ≤ y⇧ω⇩v"
by (metis capped_omega_induct_meet capped_omega_unfold le_iff_sup inf.sup_left_isotone mult_right_sub_dist_sup_left)

text ‹AACP Theorem 6.13›

lemma capped_omega_simulation:
assumes "y ≤ u"
and "s ≤ u"
and "u * v ≤ v"
and "s * t ≤ y * s"
shows "s * t⇧ω⇩v ≤ y⇧ω⇩v"
proof -
have "s * t⇧ω⇩v ≤ s * t * t⇧ω⇩v ⊓ s * v"
by (metis capped_omega_below capped_omega_unfold inf.boundedI inf.cobounded1 mult_right_isotone mult_assoc)
also have "... ≤ s * t * t⇧ω⇩v ⊓ v"
using assms(2,3) inf.order_lesseq_imp inf.sup_right_isotone mult_left_isotone by blast
also have "... ≤ y * s * t⇧ω⇩v ⊓ v"
using assms(4) inf.sup_left_isotone mult_left_isotone by auto
finally show ?thesis
using assms(1,3) capped_omega_induct_meet mult_assoc by auto
qed

lemma capped_omega_slide_sub:
assumes "s ≤ u"
and "y ≤ u"
and "u * u ≤ u"
and "u * v ≤ v"
shows "s * (y * s)⇧ω⇩v ≤ (s * y)⇧ω⇩v"
proof -
have "s * y ≤ u"
by (meson assms(1-3) mult_isotone order_trans)
thus ?thesis
using assms(1,4) capped_omega_simulation mult_assoc by auto
qed

text ‹AACP Theorem 6.14›

lemma capped_omega_slide:
"s ≤ u ⟹ y ≤ u ⟹ u * u ≤ u ⟹ u * v ≤ v ⟹ s * (y * s)⇧ω⇩v = (s * y)⇧ω⇩v"
by (smt (verit) order.antisym mult_assoc mult_right_isotone capped_omega_unfold capped_omega_slide_sub inf.sup_ge1 order_trans)

lemma capped_omega_sub_dist:
"s ≤ u ⟹ y ≤ u ⟹ u * v ≤ v ⟹ s⇧ω⇩v ≤ (s ⊔ y)⇧ω⇩v"

text ‹AACP Theorem 6.15›

lemma capped_omega_simulation_2:
assumes "s ≤ u"
and "y ≤ u"
and "u * u ≤ u"
and "u * v ≤ v"
and "y * s ≤ s * y"
shows "(s * y)⇧ω⇩v ≤ s⇧ω⇩v"
proof -
have 1: "s * y ≤ u"
using assms(1-3) inf.order_lesseq_imp mult_isotone by blast
have 2: "s * (s * y)⇧ω⇩v ≤ v"
by (meson assms(1,4) capped_omega_below order.trans mult_isotone)
have "(s * y)⇧ω⇩v = s * (y * s)⇧ω⇩v"
using assms(1-4) capped_omega_slide by auto
also have "... ≤ s * (s * y)⇧ω⇩v"
using 1 assms(4,5) capped_omega_isotone mult_right_isotone by blast
also have "... = s * (s * y)⇧ω⇩v ⊓ v"
using 2 inf.order_iff by auto
finally show ?thesis
using assms(1,4) capped_omega_induct_meet by blast
qed

text ‹AACP Theorem 6.16›

lemma left_plus_capped_omega:
assumes "y ≤ u"
and "u * u ≤ u"
and "u * v ≤ v"
shows "(y * y⇧⋆)⇧ω⇩v = y⇧ω⇩v"
proof -
have 1: "y * y⇧⋆ ≤ u"
by (metis assms(1,2) star_plus star_below_cap)
hence "y * y⇧⋆ * (y * y⇧⋆)⇧ω⇩v ≤ v"
using assms(3) capped_omega_below unfold_capped_omega by auto
hence "y * y⇧⋆ * (y * y⇧⋆)⇧ω⇩v = (y * y⇧⋆)⇧ω⇩v"
using 1 assms(3) unfold_capped_omega by blast
hence "(y * y⇧⋆)⇧ω⇩v ≤ y⇧ω⇩v"
using 1 by (smt assms(1,3) capped_omega_simulation mult_assoc mult_semi_associative star.circ_transitive_equal star_simulation_right_equal)
thus ?thesis
using 1 by (meson assms(3) capped_omega_isotone order.antisym star.circ_mult_increasing)
qed

text ‹AACP Theorem 6.17›

lemma capped_omega_sub_vector:
assumes "z ≤ v"
and "y ≤ u"
and "u * v ≤ v"
shows "y⇧ω⇩u * z ≤ y⇧ω⇩v"
proof -
have "y⇧ω⇩u * z ≤ y * y⇧ω⇩u * z ⊓ u * z"
by (metis capped_omega_below capped_omega_unfold eq_refl inf.boundedI inf.cobounded1 mult_isotone)
also have "... ≤ y * y⇧ω⇩u * z ⊓ v"
by (metis assms(1,3) inf.sup_left_isotone inf_commute mult_right_isotone order_trans)
finally show ?thesis
using assms(2,3) capped_omega_induct_meet mult_assoc by auto
qed

text ‹AACP Theorem 6.18›

lemma capped_omega_omega:
"y ≤ u ⟹ u * v ≤ v ⟹ (y⇧ω⇩u)⇧ω⇩v ≤ y⇧ω⇩v"
by (metis capped_omega_below capped_omega_sub_vector unfold_capped_omega)

end

end

```