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)
  by (simp add: capped_omega_induct sup_commute)

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"
    by (simp add: capped_omega_induct)
  also have "... = 1⇧ω⇩v"
    by (simp add: star_one)
  finally show ?thesis
    by (simp add: capped_omega_below order.antisym)
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)"
    by (simp add: inf_sup_distrib2)
  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)"
  by (simp add: capped_fix is_fixpoint_def)

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"
    by (simp add: star_left_induct_mult)
  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"
  by (simp add: star_loop_least_fixpoint unfold_capped_omega)

lemma capped_omega_induct_meet_zero:
  "x ≤ y * x ⊓ v ⟹ x ≤ y⇧ω⇩v ⊔ y⇧⋆ * bot"
  by (simp add: capped_omega_induct)

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"
  by (simp add: capped_omega_isotone)

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