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  (λ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 "(λ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_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