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 (z3) 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 (z3) 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 (z3) 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 (z3) 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
  apply (simp add: Omega_left_slide)
  by (simp add: Omega_sup_1)

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"
  by (simp add: Omega_one_greatest order.antisym)

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 (z3) 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 (z3) 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
  apply (simp add: Omega_simulate mult_assoc)
  by (simp add: Omega_simulate)

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 (z3) 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)
  by (simp add: Omega.circ_sub_dist_3)

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 (z3) 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 (z3) Omega_induct sup_assoc sup_commute mult_assoc)
  thus ?thesis
    by (simp add: Omega.left_plus_circ)
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 (z3) 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 (z3) 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
  apply (simp add: Omega_sup)
  using Omega_mult apply blast
  apply (simp add: Omega_circ_simulate_right_plus)
  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"
  by (simp add: Omega_one_greatest order.antisym)

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 (z3) 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