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
  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 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
  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 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 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
    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 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
  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 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