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