# 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

```