Theory Extended_Designs

(* Title:      Extended Designs
   Author:     Walter Guttmann
   Maintainer: Walter Guttmann <walter.guttmann at canterbury.ac.nz>
*)

section Extended Designs

theory Extended_Designs

imports Omega_Algebras Domain

begin

class domain_semiring_L_below = left_zero_domain_semiring + L +
  assumes L_left_zero_below: "L * x  L"
  assumes mult_L_split: "x * L = x * bot  d(x) * L"
begin

lemma d_zero_mult_L:
  "d(x * bot) * L  x"
  by (metis le_sup_iff mult_L_split mult_assoc mult_left_zero zero_right_mult_decreasing)

lemma mult_L:
  "x * L  x * bot  L"
  by (metis sup_right_isotone d_mult_below mult_L_split)

lemma d_mult_L:
  "d(x) * L  x * L"
  by (metis sup_right_divisibility mult_L_split)

lemma d_L_split:
  "x * d(y) * L = x * bot  d(x * y) * L"
  by (metis d_commutative d_mult_d d_zero mult_L_split mult_assoc mult_left_zero)

lemma d_mult_mult_L:
  "d(x * y) * L  x * d(y) * L"
  using d_L_split by auto

lemma L_L:
  "L * L = L"
  by (metis d_restrict_equals le_iff_sup mult_L_split zero_right_mult_decreasing)

end

class antidomain_semiring_L = left_zero_antidomain_semiring + L +
  assumes d_zero_mult_L: "d(x * bot) * L  x"
  assumes d_L_zero     : "d(L * bot) = 1"
  assumes mult_L       : "x * L  x * bot  L"
begin

lemma L_left_zero:
  "L * x = L"
  by (metis order.antisym d_L_zero d_zero_mult_L mult_assoc mult_left_one mult_left_zero zero_right_mult_decreasing)

subclass domain_semiring_L_below
  apply unfold_locales
  apply (simp add: L_left_zero)
  apply (rule order.antisym)
  apply (smt d_restrict_equals le_iff_sup mult_L mult_assoc mult_left_dist_sup)
  by (metis le_sup_iff d_L_zero d_mult_d d_zero_mult_L mult_assoc mult_right_isotone mult_1_right bot_least)

end

class ed_below = bounded_left_zero_omega_algebra + domain_semiring_L_below + Omega +
  assumes Omega_def: "xΩ = d(xω) * L  x"
begin

lemma Omega_isotone:
  "x  y  xΩ  yΩ"
  by (metis Omega_def sup_mono d_isotone mult_left_isotone omega_isotone star.circ_isotone)

lemma star_below_Omega:
  "x  xΩ"
  using Omega_def by auto

lemma one_below_Omega:
  "1  xΩ"
  using order_trans star.circ_reflexive star_below_Omega by blast

lemma L_left_zero_star:
  "L * x = L"
  by (meson L_left_zero_below order.antisym star.circ_back_loop_prefixpoint sup.boundedE)

lemma L_left_zero_Omega:
  "L * xΩ = L"
  using L_left_zero_star L_left_zero_below Omega_def mult_left_dist_sup sup.order_iff sup_monoid.add_commute by auto

lemma mult_L_star:
  "(x * L) = 1  x * L"
  by (metis L_left_zero_star mult_assoc star.circ_left_unfold)

lemma mult_L_omega_below:
  "(x * L)ω  x * L"
  by (metis L_left_zero_below mult_right_isotone omega_slide)

lemma mult_L_sup_star:
  "(x * L  y) = y  y * x * L"
  by (metis L_left_zero_star sup_commute mult_assoc star.circ_unfold_sum)

lemma mult_L_sup_omega_below:
  "(x * L  y)ω  yω  y * x * L"
proof -
  have "(x * L  y)ω = (y * x * L)ω  (y * x * L) * yω"
    by (simp add: ils.il_inf_associative omega_decompose sup_commute)
  also have "...  y * x * L  (y * x * L) * yω"
    using sup_left_isotone mult_L_omega_below by auto
  also have "... = y * x * L  y * x * L * yω  yω"
    by (smt L_left_zero_star sup_assoc sup_commute mult_assoc star.circ_loop_fixpoint)
  also have "...  yω  y * x * L"
    by (metis L_left_zero_star sup_commute eq_refl mult_assoc star.circ_back_loop_fixpoint)
  finally show ?thesis
    .
qed

lemma mult_L_sup_circ:
  "(x * L  y)Ω = d(yω) * L  y  y * x * L"
proof -
  have "(x * L  y)Ω = d((x * L  y)ω) * L  (x * L  y)"
    by (simp add: Omega_def)
  also have "...  d(yω  y * x * L) * L  (x * L  y)"
    by (metis sup_left_isotone d_isotone mult_L_sup_omega_below mult_left_isotone)
  also have "... = d(yω) * L  d(y * x * L) * L  (x * L  y)"
    by (simp add: d_dist_sup mult_right_dist_sup)
  also have "...  d(yω) * L  y * x * L * L  (x * L  y)"
    by (meson d_mult_L order.refl sup.mono)
  also have "... = d(yω) * L  y  y * x * L"
    by (smt L_L sup_assoc sup_commute le_iff_sup mult_L_sup_star mult_assoc order_refl)
  finally have 1: "(x * L  y)Ω  d(yω) * L  y  y * x * L"
    .
  have 2: "d(yω) * L  (x * L  y)Ω"
    using Omega_isotone Omega_def by force
  have "y  y * x * L  (x * L  y)Ω"
    by (metis Omega_def sup_ge2 mult_L_sup_star)
  hence "d(yω) * L  y  y * x * L  (x * L  y)Ω"
    using 2 by simp
  thus ?thesis
    using 1 by (simp add: order.antisym)
qed

lemma circ_sup_d:
  "(xΩ * y)Ω * xΩ = d((x * y)ω) * L  ((x * y) * x  (x * y) * d(xω) * L)"
proof -
  have "(xΩ * y)Ω * xΩ = ((d(xω) * L  x) * y)Ω * xΩ"
    by (simp add: Omega_def)
  also have "... = (d(xω) * L * y  x * y)Ω * xΩ"
    by (simp add: mult_right_dist_sup)
  also have "...  (d(xω) * L  x * y)Ω * xΩ"
    by (metis L_left_zero_below Omega_isotone sup_left_isotone mult_assoc mult_left_isotone mult_right_isotone)
  also have "... = (d((x * y)ω) * L  (x * y)  (x * y) * d(xω) * L) * xΩ"
    by (simp add: mult_L_sup_circ)
  also have "... = d((x * y)ω) * L * xΩ  (x * y) * xΩ  (x * y) * d(xω) * L * xΩ"
    using mult_right_dist_sup by auto
  also have "... = d((x * y)ω) * L  (x * y) * xΩ  (x * y) * d(xω) * L"
    by (simp add: L_left_zero_Omega mult.assoc)
  also have "... = d((x * y)ω) * L  ((x * y) * x  (x * y) * d(xω) * L)"
    by (simp add: Omega_def ils.il_inf_associative semiring.distrib_left sup_left_commute sup_monoid.add_commute)
  finally have 1: "(xΩ * y)Ω * xΩ  d((x * y)ω) * L  ((x * y) * x  (x * y) * d(xω) * L)"
    .
  have "d((x * y)ω) * L  (xΩ * y)Ω"
    using Omega_isotone Omega_def mult_left_isotone by auto
  also have "...  (xΩ * y)Ω * xΩ"
    by (metis mult_right_isotone mult_1_right one_below_Omega)
  finally have 2: "d((x * y)ω) * L  (xΩ * y)Ω * xΩ"
    .
  have 3: "(x * y) * x  (xΩ * y)Ω * xΩ"
    by (meson Omega_isotone order.trans mult_left_isotone mult_right_isotone star_below_Omega)
  have "(x * y) * d(xω) * L  (x * y) * xΩ"
    by (metis Omega_def sup_commute mult_assoc mult_left_sub_dist_sup_right)
  also have "...  (xΩ * y)Ω * xΩ"
    using Omega_isotone Omega_def mult_left_isotone by force
  finally have "d((x * y)ω) * L  ((x * y) * x  (x * y) * d(xω) * L)  (xΩ * y)Ω * xΩ"
    using 2 3 by (simp add: sup_assoc)
  thus ?thesis
    using 1 by (simp add: order.antisym)
qed

proposition mult_L_omega: "(x * L)ω = x * L" nitpick [expect=genuine,card=5] oops
proposition mult_L_sup_omega: "(x * L  y)ω = yω  y * x * L" nitpick [expect=genuine,card=5] oops
proposition d_Omega_circ_simulate_right_plus: "z * x  y * yΩ * z  w  z * xΩ  yΩ * (z  w * xΩ)" nitpick [expect=genuine,card=4] oops
proposition d_Omega_circ_simulate_left_plus: "x * z  z * yΩ  w  xΩ * z  (z  xΩ * w) * yΩ" nitpick [expect=genuine,card=3] oops

end

class ed = ed_below +
  assumes L_left_zero: "L * x = L"
begin

lemma mult_L_omega:
  "(x * L)ω = x * L"
  by (metis L_left_zero omega_slide)

lemma mult_L_sup_omega:
  "(x * L  y)ω = yω  y * x * L"
  by (metis L_left_zero ils.il_inf_associative mult_bot_add_omega sup_commute)

lemma d_Omega_circ_simulate_right_plus:
  assumes "z * x  y * yΩ * z  w"
    shows "z * xΩ  yΩ * (z  w * xΩ)"
proof -
  have "z * x  y * d(yω) * L * z  y * y * z  w"
    using assms Omega_def ils.il_inf_associative mult_right_dist_sup semiring.distrib_left by auto
  also have "...  y * d(yω) * L  y * y * z  w"
    by (metis L_left_zero_below sup_commute sup_right_isotone mult_assoc mult_right_isotone)
  also have "... = y * bot  d(y * yω) * L  y * y * z  w"
    by (simp add: d_L_split)
  also have "... = d(yω) * L  y * y * z  w"
    by (smt sup_assoc sup_commute sup_bot_left mult_assoc mult_left_dist_sup omega_unfold)
  finally have 1: "z * x  d(yω) * L  y * y * z  w"
    .
  have "(d(yω) * L  y * z  y * w * d(xω) * L  y * w * x) * x = d(yω) * L * x  y * z * x  y * w * d(xω) * L * x  y * w * x * x"
    using mult_right_dist_sup by fastforce
  also have "...  d(yω) * L  y * z * x  y * w * d(xω) * L * x  y * w * x * x"
    by (metis L_left_zero_below sup_left_isotone mult_assoc mult_right_isotone)
  also have "...  d(yω) * L  y * z * x  y * w * d(xω) * L  y * w * x * x"
    by (metis L_left_zero_below sup_commute sup_left_isotone mult_assoc mult_right_isotone)
  also have "...  d(yω) * L  y * z * x  y * w * d(xω) * L  y * w * x"
    by (meson star.circ_back_loop_prefixpoint sup.boundedE sup_right_isotone)
  also have "...  d(yω) * L  y * (d(yω) * L  y * y * z  w)  y * w * d(xω) * L  y * w * x"
    using 1 by (smt sup_left_isotone sup_right_isotone le_iff_sup mult_assoc mult_left_dist_sup)
  also have "... = d(yω) * L  y * y * y * z  y * w * d(xω) * L  y * w * x"
    by (smt sup_assoc sup_commute sup_idem mult_assoc mult_left_dist_sup d_L_split star.circ_back_loop_fixpoint star_mult_omega)
  also have "...  d(yω) * L  y * z  y * w * d(xω) * L  y * w * x"
    using mult_isotone order_refl semiring.add_right_mono star.circ_mult_upper_bound star.right_plus_below_circ sup_right_isotone by auto
  finally have 2: "z * x  d(yω) * L  y * z  y * w * d(xω) * L  y * w * x"
    by (smt le_sup_iff sup_ge1 star.circ_loop_fixpoint star_right_induct)
  have "z * x * xω  y * y * z * xω  d(yω) * L * xω  w * xω"
    using 1 by (metis sup_commute mult_left_isotone mult_right_dist_sup)
  also have "...  y * y * z * xω  d(yω) * L  w * xω"
    by (metis L_left_zero eq_refl ils.il_inf_associative)
  finally have "z * xω  yω  y * d(yω) * L  y * w * xω"
    by (smt sup_assoc sup_commute left_plus_omega mult_assoc mult_left_dist_sup omega_induct omega_unfold star.left_plus_circ)
  hence "z * xω  yω  y * w * xω"
    by (metis sup_commute d_mult_L le_iff_sup mult_assoc mult_right_isotone omega_sub_vector order_trans star_mult_omega)
  hence "d(z * xω) * L  d(yω) * L  y * w * d(xω) * L"
    by (smt sup_assoc sup_commute d_L_split d_dist_sup le_iff_sup mult_right_dist_sup)
  hence "z * d(xω) * L  z * bot  d(yω) * L  y * w * d(xω) * L"
    using d_L_split sup_assoc sup_right_isotone by force
  also have "...  y * z  d(yω) * L  y * w * d(xω) * L"
    by (smt sup_commute sup_left_isotone sup_ge1 order_trans star.circ_loop_fixpoint zero_right_mult_decreasing)
  finally have "z * d(xω) * L  d(yω) * L  y * z  y * w * d(xω) * L  y * w * x"
    by (simp add: le_supI2 sup_commute)
  thus ?thesis
    using 2 by (smt L_left_zero Omega_def sup_assoc le_iff_sup mult_assoc mult_left_dist_sup mult_right_dist_sup)
qed

lemma d_Omega_circ_simulate_left_plus:
  assumes "x * z  z * yΩ  w"
    shows "xΩ * z  (z  xΩ * w) * yΩ"
proof -
  have "x * (z * d(yω) * L  z * y  d(xω) * L  x * w * d(yω) * L  x * w * y) = x * z * d(yω) * L  x * z * y  d(xω) * L  x * x * w * d(yω) * L  x * x * w * y"
    by (smt sup_assoc sup_commute mult_assoc mult_left_dist_sup d_L_split omega_unfold)
  also have "...  (z * d(yω) * L  z * y  w) * d(yω) * L  (z * d(yω) * L  z * y  w) * y  d(xω) * L  x * w * d(yω) * L  x * w * y"
    by (smt assms Omega_def sup_assoc sup_ge2 le_iff_sup mult_assoc mult_left_dist_sup mult_right_dist_sup star.circ_loop_fixpoint)
  also have "... = z * d(yω) * L  z * y * d(yω) * L  w * d(yω) * L  z * y  w * y  d(xω) * L  x * w * d(yω) * L  x * w * y"
    by (smt L_left_zero sup_assoc sup_commute sup_idem mult_assoc mult_right_dist_sup star.circ_transitive_equal)
  also have "... = z * d(yω) * L  w * d(yω) * L  z * y  w * y  d(xω) * L  x * w * d(yω) * L  x * w * y"
    by (smt sup_assoc sup_commute sup_idem le_iff_sup mult_assoc d_L_split star_mult_omega zero_right_mult_decreasing)
  finally have "x * (z * d(yω) * L  z * y  d(xω) * L  x * w * d(yω) * L  x * w * y)  z * d(yω) * L  z * y  d(xω) * L  x * w * d(yω) * L  x * w * y"
    by (smt sup_assoc sup_commute sup_idem mult_assoc star.circ_loop_fixpoint)
  thus ?thesis
    by (smt (verit, del_insts) L_left_zero Omega_def sup_assoc le_sup_iff sup_ge1 mult_assoc mult_left_dist_sup mult_right_dist_sup star.circ_back_loop_fixpoint star_left_induct)
qed

end

text Theorem 2.5 and Theorem 50.4

sublocale ed < ed_omega: itering where circ = Omega
  apply unfold_locales
  apply (smt sup_assoc sup_commute sup_bot_left circ_sup_d Omega_def mult_left_dist_sup mult_right_dist_sup d_L_split d_dist_sup omega_decompose star.circ_sup_1 star.circ_slide)
  apply (smt L_left_zero sup_assoc sup_commute sup_bot_left Omega_def mult_assoc mult_left_dist_sup mult_right_dist_sup d_L_split omega_slide star.circ_mult)
  using d_Omega_circ_simulate_right_plus apply blast
  by (simp add: d_Omega_circ_simulate_left_plus)

sublocale ed < ed_star: itering where circ = star ..

class ed_2 = ed_below + antidomain_semiring_L + Omega
begin

subclass ed
  apply unfold_locales
  by (rule L_left_zero)

end

end