Theory Binary_Iterings

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

section ‹Binary Iterings›

theory Binary_Iterings

imports Base

begin

class binary_itering = idempotent_left_zero_semiring + while +
  assumes while_productstar: "(x * y) ⋆ z = z ⊔ x * ((y * x) ⋆ (y * z))"
  assumes while_sumstar: "(x ⊔ y) ⋆ z = (x ⋆ y) ⋆ (x ⋆ z)"
  assumes while_left_dist_sup: "x ⋆ (y ⊔ z) = (x ⋆ y) ⊔ (x ⋆ z)"
  assumes while_sub_associative: "(x ⋆ y) * z ≤ x ⋆ (y * z)"
  assumes while_simulate_left_plus: "x * z ≤ z * (y ⋆ 1) ⊔ w ⟶ x ⋆ (z * v) ≤ z * (y ⋆ v) ⊔ (x ⋆ (w * (y ⋆ v)))"
  assumes while_simulate_right_plus: "z * x ≤ y * (y ⋆ z) ⊔ w ⟶ z * (x ⋆ v) ≤ y ⋆ (z * v ⊔ w * (x ⋆ v))"
begin

text ‹Theorem 9.1›

lemma while_zero:
  "bot ⋆ x = x"
  by (metis sup_bot_right mult_left_zero while_productstar)

text ‹Theorem 9.4›

lemma while_mult_increasing:
  "x * y ≤ x ⋆ y"
  by (metis le_supI2 mult.left_neutral mult_left_sub_dist_sup_left while_productstar)

text ‹Theorem 9.2›

lemma while_one_increasing:
  "x ≤ x ⋆ 1"
  by (metis mult.right_neutral while_mult_increasing)

text ‹Theorem 9.3›

lemma while_increasing:
  "y ≤ x ⋆ y"
  by (metis sup_left_divisibility mult_left_one while_productstar)

text ‹Theorem 9.42›

lemma while_right_isotone:
  "y ≤ z ⟹ x ⋆ y ≤ x ⋆ z"
  by (metis le_iff_sup while_left_dist_sup)

text ‹Theorem 9.41›

lemma while_left_isotone:
  "x ≤ y ⟹ x ⋆ z ≤ y ⋆ z"
  using sup_left_divisibility while_sumstar while_increasing by auto

lemma while_isotone:
  "w ≤ x ⟹ y ≤ z ⟹ w ⋆ y ≤ x ⋆ z"
  by (meson order_lesseq_imp while_left_isotone while_right_isotone)

text ‹Theorem 9.17›

lemma while_left_unfold:
  "x ⋆ y = y ⊔ x * (x ⋆ y)"
  by (metis mult_1_left mult_1_right while_productstar)

lemma while_simulate_left_plus_1:
  "x * z ≤ z * (y ⋆ 1) ⟹ x ⋆ (z * w) ≤ z * (y ⋆ w) ⊔ (x ⋆ bot)"
  by (metis sup_bot_right mult_left_zero while_simulate_left_plus)

text ‹Theorem 11.1›

lemma while_simulate_absorb:
  "y * x ≤ x ⟹ y ⋆ x ≤ x ⊔ (y ⋆ bot)"
  by (metis while_simulate_left_plus_1 while_zero mult_1_right)

text ‹Theorem 9.10›

lemma while_transitive:
  "x ⋆ (x ⋆ y) = x ⋆ y"
  by (metis order.eq_iff sup_bot_right sup_ge2 while_left_dist_sup while_increasing while_left_unfold while_simulate_absorb)

text ‹Theorem 9.25›

lemma while_slide:
  "(x * y) ⋆ (x * z) = x * ((y * x) ⋆ z)"
  by (metis mult_left_dist_sup while_productstar mult_assoc while_left_unfold)

text ‹Theorem 9.21›

lemma while_zero_2:
  "(x * bot) ⋆ y = x * bot ⊔ y"
  by (metis mult_left_zero sup_commute mult_assoc while_left_unfold)

text ‹Theorem 9.5›

lemma while_mult_star_exchange:
  "x * (x ⋆ y) = x ⋆ (x * y)"
  by (metis mult_left_one while_slide)

text ‹Theorem 9.18›

lemma while_right_unfold:
  "x ⋆ y = y ⊔ (x ⋆ (x * y))"
  by (metis while_left_unfold while_mult_star_exchange)

text ‹Theorem 9.7›

lemma while_one_mult_below:
  "(x ⋆ 1) * y ≤ x ⋆ y"
  by (metis mult_left_one while_sub_associative)

lemma while_plus_one:
  "x ⋆ y = y ⊔ (x ⋆ y)"
  by (simp add: sup.absorb2 while_increasing)

text ‹Theorem 9.19›

lemma while_rtc_2:
  "y ⊔ x * y ⊔ (x ⋆ (x ⋆ y)) = x ⋆ y"
  by (simp add: sup_absorb2 while_increasing while_mult_increasing while_transitive)

text ‹Theorem 9.6›

lemma while_left_plus_below:
  "x * (x ⋆ y) ≤ x ⋆ y"
  by (metis sup_right_divisibility while_left_unfold)

lemma while_right_plus_below:
  "x ⋆ (x * y) ≤ x ⋆ y"
  using while_left_plus_below while_mult_star_exchange by auto

lemma while_right_plus_below_2:
  "(x ⋆ x) * y ≤ x ⋆ y"
  by (smt order_trans while_right_plus_below while_sub_associative)

text ‹Theorem 9.47›

lemma while_mult_transitive:
  "x ≤ z ⋆ y ⟹ y ≤ z ⋆ w ⟹ x ≤ z ⋆ w"
  by (smt order_trans while_right_isotone while_transitive)

text ‹Theorem 9.48›

lemma while_mult_upper_bound:
  "x ≤ z ⋆ 1 ⟹ y ≤ z ⋆ w ⟹ x * y ≤ z ⋆ w"
  by (metis order.trans mult_isotone while_one_mult_below while_transitive)

lemma while_one_mult_while_below:
  "(y ⋆ 1) * (y ⋆ v) ≤ y ⋆ v"
  by (simp add: while_mult_upper_bound)

text ‹Theorem 9.34›

lemma while_sub_dist:
  "x ⋆ z ≤ (x ⊔ y) ⋆ z"
  by (simp add: while_left_isotone)

lemma while_sub_dist_1:
  "x * z ≤ (x ⊔ y) ⋆ z"
  using order.trans while_mult_increasing while_sub_dist by blast

lemma while_sub_dist_2:
  "x * y * z ≤ (x ⊔ y) ⋆ z"
  by (metis sup_commute mult_assoc while_mult_transitive while_sub_dist_1)

text ‹Theorem 9.36›

lemma while_sub_dist_3:
  "x ⋆ (y ⋆ z) ≤ (x ⊔ y) ⋆ z"
  by (metis sup_commute while_mult_transitive while_sub_dist)

text ‹Theorem 9.44›

lemma while_absorb_2:
  "x ≤ y ⟹ y ⋆ (x ⋆ z) = y ⋆ z"
  using sup_left_divisibility while_sumstar while_transitive by auto

lemma while_simulate_right_plus_1:
  "z * x ≤ y * (y ⋆ z) ⟹ z * (x ⋆ w) ≤ y ⋆ (z * w)"
  by (metis sup_bot_right mult_left_zero while_simulate_right_plus)

text ‹Theorem 9.39›

lemma while_sumstar_1_below:
  "x ⋆ ((y * (x ⋆ 1)) ⋆ z) ≤ ((x ⋆ 1) * y) ⋆ (x ⋆ z)"
proof -
  have 1: "x * (((x ⋆ 1) * y) ⋆ (x ⋆ z)) ≤ ((x ⋆ 1) * y) ⋆ (x ⋆ z)"
    by (smt sup_mono sup_ge2 mult_assoc mult_left_dist_sup mult_right_sub_dist_sup_right while_left_unfold)
  have "x ⋆ ((y * (x ⋆ 1)) ⋆ z) ≤ (x ⋆ z) ⊔ (x ⋆ (y * (((x ⋆ 1) * y) ⋆ ((x ⋆ 1) * z))))"
    by (metis eq_refl while_left_dist_sup while_productstar)
  also have "... ≤ (x ⋆ z) ⊔ (x ⋆ ((x ⋆ 1) * y * (((x ⋆ 1) * y) ⋆ ((x ⋆ 1) * z))))"
    by (metis sup_right_isotone mult_assoc mult_left_one mult_right_sub_dist_sup_left while_left_unfold while_right_isotone)
  also have "... ≤ (x ⋆ z) ⊔ (x ⋆ (((x ⋆ 1) * y) ⋆ ((x ⋆ 1) * z)))"
    using semiring.add_left_mono while_left_plus_below while_right_isotone by blast
  also have "... ≤ x ⋆ (((x ⋆ 1) * y) ⋆ (x ⋆ z))"
    by (meson order.trans le_supI while_increasing while_one_mult_below while_right_isotone)
  also have "... ≤ (((x ⋆ 1) * y) ⋆ (x ⋆ z)) ⊔ (x ⋆ bot)"
    using 1 while_simulate_absorb by auto
  also have "... = ((x ⋆ 1) * y) ⋆ (x ⋆ z)"
    by (smt sup_assoc sup_commute sup_bot_left while_left_dist_sup while_left_unfold)
  finally show ?thesis
    .
qed

lemma while_sumstar_2_below:
  "((x ⋆ 1) * y) ⋆ (x ⋆ z) ≤ (x ⋆ y) ⋆ (x ⋆ z)"
  by (simp add: while_left_isotone while_one_mult_below)

text ‹Theorem 9.38›

lemma while_sup_1_below:
  "x ⋆ ((y * (x ⋆ 1)) ⋆ z) ≤ (x ⊔ y) ⋆ z"
proof -
  have "((x ⋆ 1) * y) ⋆ ((x ⋆ 1) * z) ≤ (x ⊔ y) ⋆ z"
    using while_sumstar while_isotone while_one_mult_below by auto
  hence "(y * (x ⋆ 1)) ⋆ z ≤ z ⊔ y * ((x ⊔ y) ⋆ z)"
    by (metis sup_right_isotone mult_right_isotone while_productstar)
  also have "... ≤ (x ⊔ y) ⋆ z"
    by (metis sup_right_isotone sup_ge2 mult_left_isotone while_left_unfold)
  finally show ?thesis
    using while_mult_transitive while_sub_dist by blast
qed

text ‹Theorem 9.16›

lemma while_while_while:
  "((x ⋆ 1) ⋆ 1) ⋆ y = (x ⋆ 1) ⋆ y"
  by (smt (z3) sup.absorb1 while_sumstar while_absorb_2 while_increasing while_one_increasing)

lemma while_one:
  "(1 ⋆ 1) ⋆ y = 1 ⋆ y"
  by (metis while_while_while while_zero)

text ‹Theorem 9.22›

lemma while_sup_below:
  "x ⊔ y ≤ x ⋆ (y ⋆ 1)"
  by (metis le_supI le_supI1 while_left_dist_sup while_left_unfold while_one_increasing)

text ‹Theorem 9.32›

lemma while_sup_2:
  "(x ⊔ y) ⋆ z ≤ (x ⋆ (y ⋆ 1)) ⋆ z"
  using while_left_isotone while_sup_below by auto

text ‹Theorem 9.45›

lemma while_sup_one_left_unfold:
  "1 ≤ x ⟹ x * (x ⋆ y) = x ⋆ y"
  by (metis order.antisym mult_1_left mult_left_isotone while_left_plus_below)

lemma while_sup_one_right_unfold:
  "1 ≤ x ⟹ x ⋆ (x * y) = x ⋆ y"
  using while_mult_star_exchange while_sup_one_left_unfold by auto

text ‹Theorem 9.30›

lemma while_decompose_7:
  "(x ⊔ y) ⋆ z = x ⋆ (y ⋆ ((x ⊔ y) ⋆ z))"
  by (metis order.eq_iff order_trans while_increasing while_sub_dist_3 while_transitive)

text ‹Theorem 9.31›

lemma while_decompose_8:
  "(x ⊔ y) ⋆ z = (x ⊔ y) ⋆ (x ⋆ (y ⋆ z))"
  using while_absorb_2 by auto

text ‹Theorem 9.27›

lemma while_decompose_9:
  "(x ⋆ (y ⋆ 1)) ⋆ z = x ⋆ (y ⋆ ((x ⋆ (y ⋆ 1)) ⋆ z))"
  by (smt sup_commute le_iff_sup order_trans while_sup_below while_increasing while_sub_dist_3)

lemma while_decompose_10:
  "(x ⋆ (y ⋆ 1)) ⋆ z = (x ⋆ (y ⋆ 1)) ⋆ (x ⋆ (y ⋆ z))"
proof -
  have 1: "(x ⋆ (y ⋆ 1)) ⋆ z ≤ (x ⋆ (y ⋆ 1)) ⋆ (x ⋆ (y ⋆ z))"
    by (meson order.trans while_increasing while_right_isotone)
  have "x ⊔ (y ⋆ 1) ≤ x ⋆ (y ⋆ 1)"
    using while_increasing while_sup_below by auto
  hence "(x ⋆ (y ⋆ 1)) ⋆ (x ⋆ (y ⋆ z)) ≤ (x ⋆ (y ⋆ 1)) ⋆ z"
    using while_absorb_2 while_sup_below by force
  thus ?thesis
    using 1 order.antisym by blast
qed

lemma while_back_loop_fixpoint:
  "z * (y ⋆ (y * x)) ⊔ z * x = z * (y ⋆ x)"
  by (metis sup_commute mult_left_dist_sup while_right_unfold)

lemma while_back_loop_prefixpoint:
  "z * (y ⋆ 1) * y ⊔ z ≤ z * (y ⋆ 1)"
  by (metis le_supI le_supI2 mult_1_right mult_right_isotone mult_assoc while_increasing while_one_mult_below while_right_unfold)

text ‹Theorem 9›

lemma while_loop_is_fixpoint:
  "is_fixpoint (λx . y * x ⊔ z) (y ⋆ z)"
  using is_fixpoint_def sup_commute while_left_unfold by auto

text ‹Theorem 9›

lemma while_back_loop_is_prefixpoint:
  "is_prefixpoint (λx . x * y ⊔ z) (z * (y ⋆ 1))"
  using is_prefixpoint_def while_back_loop_prefixpoint by auto

text ‹Theorem 9.20›

lemma while_while_sup:
  "(1 ⊔ x) ⋆ y = (x ⋆ 1) ⋆ y"
  by (metis sup_commute while_decompose_10 while_sumstar while_zero)

lemma while_while_mult_sub:
  "x ⋆ (1 ⋆ y) ≤ (x ⋆ 1) ⋆ y"
  by (metis sup_commute while_sub_dist_3 while_while_sup)

text ‹Theorem 9.11›

lemma while_right_plus:
  "(x ⋆ x) ⋆ y = x ⋆ y"
  by (metis sup_idem while_plus_one while_sumstar while_transitive)

text ‹Theorem 9.12›

lemma while_left_plus:
  "(x * (x ⋆ 1)) ⋆ y = x ⋆ y"
  by (simp add: while_mult_star_exchange while_right_plus)

text ‹Theorem 9.9›

lemma while_below_while_one:
  "x ⋆ x ≤ x ⋆ 1"
  by (meson eq_refl while_mult_transitive while_one_increasing)

lemma while_below_while_one_mult:
  "x * (x ⋆ x) ≤ x * (x ⋆ 1)"
  by (simp add: mult_right_isotone while_below_while_one)

text ‹Theorem 9.23›

lemma while_sup_sub_sup_one:
  "x ⋆ (x ⊔ y) ≤ x ⋆ (1 ⊔ y)"
  using semiring.add_right_mono while_left_dist_sup while_below_while_one by auto

lemma while_sup_sub_sup_one_mult:
  "x * (x ⋆ (x ⊔ y)) ≤ x * (x ⋆ (1 ⊔ y))"
  by (simp add: mult_right_isotone while_sup_sub_sup_one)

lemma while_elimination:
  "x * y = bot ⟹ x * (y ⋆ z) = x * z"
  by (metis sup_bot_right mult_assoc mult_left_dist_sup mult_left_zero while_left_unfold)

text ‹Theorem 9.8›

lemma while_square:
  "(x * x) ⋆ y ≤ x ⋆ y"
  by (metis while_left_isotone while_mult_increasing while_right_plus)

text ‹Theorem 9.35›

lemma while_mult_sub_sup:
  "(x * y) ⋆ z ≤ (x ⊔ y) ⋆ z"
  by (metis while_increasing while_isotone while_mult_increasing while_sumstar)

text ‹Theorem 9.43›

lemma while_absorb_1:
  "x ≤ y ⟹ x ⋆ (y ⋆ z) = y ⋆ z"
  by (metis order.antisym le_iff_sup while_increasing while_sub_dist_3)

lemma while_absorb_3:
  "x ≤ y ⟹ x ⋆ (y ⋆ z) = y ⋆ (x ⋆ z)"
  by (simp add: while_absorb_1 while_absorb_2)

text ‹Theorem 9.24›

lemma while_square_2:
  "(x * x) ⋆ ((x ⊔ 1) * y) ≤ x ⋆ y"
  by (metis le_supI while_increasing while_mult_transitive while_mult_upper_bound while_one_increasing while_square)

lemma while_separate_unfold_below:
  "(y * (x ⋆ 1)) ⋆ z ≤ (y ⋆ z) ⊔ (y ⋆ (y * x * (x ⋆ ((y * (x ⋆ 1)) ⋆ z))))"
proof -
  have "(y * (x ⋆ 1)) ⋆ z = (y ⋆ (y * x * (x ⋆ 1))) ⋆ (y ⋆ z)"
    by (metis mult_assoc mult_left_dist_sup mult_1_right while_left_unfold while_sumstar)
  hence "(y * (x ⋆ 1)) ⋆ z = (y ⋆ z) ⊔ (y ⋆ (y * x * (x ⋆ 1))) * ((y * (x ⋆ 1)) ⋆ z)"
    using while_left_unfold by auto
  also have "... ≤ (y ⋆ z) ⊔ (y ⋆ (y * x * (x ⋆ 1)) * ((y * (x ⋆ 1)) ⋆ z))"
    using sup_right_isotone while_sub_associative by auto
  also have "... ≤ (y ⋆ z) ⊔ (y ⋆ (y * x * (x ⋆ ((y * (x ⋆ 1)) ⋆ z))))"
    by (smt sup_right_isotone mult_assoc mult_right_isotone while_one_mult_below while_right_isotone)
  finally show ?thesis
    .
qed

text ‹Theorem 9.33›

lemma while_mult_zero_sup:
  "(x ⊔ y * bot) ⋆ z = x ⋆ ((y * bot) ⋆ z)"
proof -
  have "(x ⊔ y * bot) ⋆ z = (x ⋆ (y * bot)) ⋆ (x ⋆ z)"
    by (simp add: while_sumstar)
  also have "... = (x ⋆ z) ⊔ (x ⋆ (y * bot)) * ((x ⋆ (y * bot)) ⋆ (x ⋆ z))"
    using while_left_unfold by auto
  also have "... ≤ (x ⋆ z) ⊔ (x ⋆ (y * bot))"
    by (metis sup_right_isotone mult_assoc mult_left_zero while_sub_associative)
  also have "... = x ⋆ ((y * bot) ⋆ z)"
    by (simp add: sup_commute while_left_dist_sup while_zero_2)
  finally show ?thesis
    by (simp add: order.antisym while_sub_dist_3)
qed

lemma while_sup_mult_zero:
  "(x ⊔ y * bot) ⋆ y = x ⋆ y"
  by (simp add: sup_absorb2 zero_right_mult_decreasing while_mult_zero_sup while_zero_2)

lemma while_mult_zero_sup_2:
  "(x ⊔ y * bot) ⋆ z = (x ⋆ z) ⊔ (x ⋆ (y * bot))"
  by (simp add: sup_commute while_left_dist_sup while_mult_zero_sup while_zero_2)

lemma while_sup_zero_star:
  "(x ⊔ y * bot) ⋆ z = x ⋆ (y * bot ⊔ z)"
  by (simp add: while_mult_zero_sup while_zero_2)

lemma while_unfold_sum:
  "(x ⊔ y) ⋆ z = (x ⋆ z) ⊔ (x ⋆ (y * ((x ⊔ y) ⋆ z)))"
  apply (rule order.antisym)
  apply (metis semiring.add_left_mono while_sub_associative while_sumstar while_left_unfold)
  by (metis le_supI while_decompose_7 while_mult_increasing while_right_isotone while_sub_dist)

lemma while_simulate_left:
  "x * z ≤ z * y ⊔ w ⟹ x ⋆ (z * v) ≤ z * (y ⋆ v) ⊔ (x ⋆ (w * (y ⋆ v)))"
  by (metis sup_left_isotone mult_right_isotone order_trans while_one_increasing while_simulate_left_plus)

lemma while_simulate_right:
  assumes "z * x ≤ y * z ⊔ w"
    shows "z * (x ⋆ v) ≤ y ⋆ (z * v ⊔ w * (x ⋆ v))"
proof -
  have "y * z ⊔ w ≤ y * (y ⋆ z) ⊔ w"
    using sup_left_isotone while_increasing while_mult_star_exchange by force
  thus ?thesis
    by (meson assms order.trans while_simulate_right_plus)
qed

lemma while_simulate:
  "z * x ≤ y * z ⟹ z * (x ⋆ v) ≤ y ⋆ (z * v)"
  by (metis sup_bot_right mult_left_zero while_simulate_right)

text ‹Theorem 9.14›

lemma while_while_mult:
  "1 ⋆ (x ⋆ y) = (x ⋆ 1) ⋆ y"
proof -
  have "(x ⋆ 1) ⋆ y ≤ (x ⋆ 1) * ((x ⋆ 1) ⋆ y)"
    by (simp add: while_increasing while_sup_one_left_unfold)
  also have "... ≤ 1 ⋆ ((x ⋆ 1) * y)"
    by (simp add: while_one_mult_while_below while_simulate)
  also have "... ≤ 1 ⋆ (x ⋆ y)"
    by (simp add: while_isotone while_one_mult_below)
  finally show ?thesis
    by (metis order.antisym while_sub_dist_3 while_while_sup)
qed

lemma while_simulate_left_1:
  "x * z ≤ z * y ⟹ x ⋆ (z * v) ≤ z * (y ⋆ v) ⊔ (x ⋆ bot)"
  by (meson order.trans mult_right_isotone while_one_increasing while_simulate_left_plus_1)

text ‹Theorem 9.46›

lemma while_associative_1:
  assumes "1 ≤ z"
  shows "x ⋆ (y * z) = (x ⋆ y) * z"
proof -
  have "x ⋆ (y * z) ≤ x ⋆ ((x ⋆ y) * z)"
    by (simp add: mult_isotone while_increasing while_right_isotone)
  also have "... ≤ (x ⋆ y) * (bot ⋆ z) ⊔ (x ⋆ bot)"
    by (metis mult_assoc mult_right_sub_dist_sup_right while_left_unfold while_simulate_absorb while_zero)
  also have "... ≤ (x ⋆ y) * z ⊔ (x ⋆ bot) * z"
    by (metis assms le_supI sup_ge1 sup_ge2 case_split_right while_plus_one while_zero)
  also have "... = (x ⋆ y) * z"
    by (metis sup_bot_right mult_right_dist_sup while_left_dist_sup)
  finally show ?thesis
    by (simp add: order.antisym while_sub_associative)
qed

text ‹Theorem 9.29›

lemma while_associative_while_1:
  "x ⋆ (y * (z ⋆ 1)) = (x ⋆ y) * (z ⋆ 1)"
  by (simp add: while_associative_1 while_increasing)

text ‹Theorem 9.13›

lemma while_one_while:
  "(x ⋆ 1) * (y ⋆ 1) = x ⋆ (y ⋆ 1)"
  by (metis mult_left_one while_associative_while_1)

lemma while_decompose_5_below:
  "(x ⋆ (y ⋆ 1)) ⋆ z ≤ (y ⋆ (x ⋆ 1)) ⋆ z"
  by (smt (z3) while_left_dist_sup while_sumstar while_absorb_2 while_one_increasing while_plus_one while_sub_dist)

text ‹Theorem 9.26›

lemma while_decompose_5:
  "(x ⋆ (y ⋆ 1)) ⋆ z = (y ⋆ (x ⋆ 1)) ⋆ z"
  by (simp add: order.antisym while_decompose_5_below)

lemma while_decompose_4:
  "(x ⋆ (y ⋆ 1)) ⋆ z = x ⋆ ((y ⋆ (x ⋆ 1)) ⋆ z)"
  using while_absorb_1 while_decompose_5 while_sup_below by auto

text ‹Theorem 11.7›

lemma while_simulate_2:
  "y * (x ⋆ 1) ≤ x ⋆ (y ⋆ 1) ⟷ y ⋆ (x ⋆ 1) ≤ x ⋆ (y ⋆ 1)"
proof
  assume "y * (x ⋆ 1) ≤ x ⋆ (y ⋆ 1)"
  hence "y * (x ⋆ 1) ≤ (x ⋆ 1) * (y ⋆ 1)"
    by (simp add: while_one_while)
  hence "y ⋆ ((x ⋆ 1) * 1) ≤ (x ⋆ 1) * (y ⋆ 1) ⊔ (y ⋆ bot)"
    using while_simulate_left_plus_1 by blast
  hence "y ⋆ (x ⋆ 1) ≤ (x ⋆ (y ⋆ 1)) ⊔ (y ⋆ bot)"
    by (simp add: while_one_while)
  also have "... = x ⋆ (y ⋆ 1)"
    by (metis sup_commute le_iff_sup order_trans while_increasing while_right_isotone bot_least)
  finally show "y ⋆ (x ⋆ 1) ≤ x ⋆ (y ⋆ 1)"
    .
next
  assume "y ⋆ (x ⋆ 1) ≤ x ⋆ (y ⋆ 1)"
  thus "y * (x ⋆ 1) ≤ x ⋆ (y ⋆ 1)"
    using order_trans while_mult_increasing by blast
qed

lemma while_simulate_1:
  "y * x ≤ x * y ⟹ y ⋆ (x ⋆ 1) ≤ x ⋆ (y ⋆ 1)"
  by (metis order_trans while_mult_increasing while_right_isotone while_simulate while_simulate_2)

lemma while_simulate_3:
  "y * (x ⋆ 1) ≤ x ⋆ 1 ⟹ y ⋆ (x ⋆ 1) ≤ x ⋆ (y ⋆ 1)"
  by (meson order.trans while_increasing while_right_isotone while_simulate_2)

text ‹Theorem 9.28›

lemma while_extra_while:
  "(y * (x ⋆ 1)) ⋆ z = (y * (y ⋆ (x ⋆ 1))) ⋆ z"
proof -
  have "y * (y ⋆ (x ⋆ 1)) ≤ y * (x ⋆ 1) * (y * (x ⋆ 1) ⋆ 1)"
    using while_back_loop_prefixpoint while_left_isotone while_mult_star_exchange by auto
  hence 1: "(y * (y ⋆ (x ⋆ 1))) ⋆ z ≤ (y * (x ⋆ 1)) ⋆ z"
    by (metis while_simulate_right_plus_1 mult_left_one)
  have "(y * (x ⋆ 1)) ⋆ z ≤ (y * (y ⋆ (x ⋆ 1))) ⋆ z"
    by (simp add: while_increasing while_left_isotone while_mult_star_exchange)
  thus ?thesis
    using 1 order.antisym by auto
qed

text ‹Theorem 11.6›

lemma while_separate_4:
  assumes "y * x ≤ x * (x ⋆ (1 ⊔ y))"
    shows "(x ⊔ y) ⋆ z = x ⋆ (y ⋆ z)"
proof -
  have "(1 ⊔ y) * x ≤ x * (x ⋆ (1 ⊔ y))"
    by (smt assms sup_assoc le_supI mult_left_one mult_left_sub_dist_sup_left mult_right_dist_sup mult_1_right while_left_unfold)
  hence 1: "(1 ⊔ y) * (x ⋆ 1) ≤ x ⋆ (1 ⊔ y)"
    by (metis mult_1_right while_simulate_right_plus_1)
  have "y * x * (x ⋆ 1) ≤ x * (x ⋆ ((1 ⊔ y) * (x ⋆ 1)))"
    by (smt assms le_iff_sup mult_assoc mult_right_dist_sup while_associative_1 while_increasing)
  also have "... ≤ x * (x ⋆ (1 ⊔ y))"
    using 1 mult_right_isotone while_mult_transitive by blast
  also have "... ≤ x * (x ⋆ 1) * (y ⋆ 1)"
    by (simp add: mult_right_isotone mult_assoc while_increasing while_one_increasing while_one_while while_right_isotone)
  finally have "y ⋆ (x * (x ⋆ 1)) ≤ x * (x ⋆ 1) * (y ⋆ 1) ⊔ (y ⋆ bot)"
    by (metis mult_assoc mult_1_right while_simulate_left_plus_1)
  hence "(y ⋆ 1) * (y ⋆ x) ≤ x * (x ⋆ y ⋆ 1) ⊔ (y ⋆ bot)"
    by (smt le_iff_sup mult_assoc mult_1_right order_refl order_trans while_absorb_2 while_left_dist_sup while_mult_star_exchange while_one_mult_below while_one_while while_plus_one)
  hence "(y ⋆ 1) * ((y ⋆ x) ⋆ (y ⋆ z)) ≤ x ⋆ ((y ⋆ 1) * (y ⋆ z) ⊔ (y ⋆ bot) * ((y ⋆ x) ⋆ (y ⋆ z)))"
    by (simp add: while_simulate_right_plus)
  also have "... ≤ x ⋆ ((y ⋆ z) ⊔ (y ⋆ bot))"
    by (metis sup_mono mult_left_zero order_refl while_absorb_2 while_one_mult_below while_right_isotone while_sub_associative)
  also have "... = x ⋆ y ⋆ z"
    using sup.absorb_iff1 while_right_isotone by auto
  finally show ?thesis
    by (smt sup_commute le_iff_sup mult_left_one mult_right_dist_sup while_plus_one while_sub_associative while_sumstar)
qed

lemma while_separate_5:
  "y * x ≤ x * (x ⋆ (x ⊔ y)) ⟹ (x ⊔ y) ⋆ z = x ⋆ (y ⋆ z)"
  using order_lesseq_imp while_separate_4 while_sup_sub_sup_one_mult by blast

lemma while_separate_6:
  "y * x ≤ x * (x ⊔ y) ⟹ (x ⊔ y) ⋆ z = x ⋆ (y ⋆ z)"
  by (smt order_trans while_increasing while_mult_star_exchange while_separate_5)

text ‹Theorem 11.4›

lemma while_separate_1:
  "y * x ≤ x * y ⟹ (x ⊔ y) ⋆ z = x ⋆ (y ⋆ z)"
  using mult_left_sub_dist_sup_right order_lesseq_imp while_separate_6 by blast

text ‹Theorem 11.2›

lemma while_separate_mult_1:
  "y * x ≤ x * y ⟹ (x * y) ⋆ z ≤ x ⋆ (y ⋆ z)"
  by (metis while_mult_sub_sup while_separate_1)

text ‹Theorem 11.5›

lemma separation:
  assumes "y * x ≤ x * (y ⋆ 1)"
    shows "(x ⊔ y) ⋆ z = x ⋆ (y ⋆ z)"
proof -
  have "y ⋆ x ≤ x * (y ⋆ 1) ⊔ (y ⋆ bot)"
    by (metis assms mult_1_right while_simulate_left_plus_1)
  also have "... ≤ x * (x ⋆ y ⋆ 1) ⊔ (y ⋆ bot)"
    using sup_left_isotone while_increasing while_mult_star_exchange by force
  finally have "(y ⋆ 1) * (y ⋆ x) ≤ x * (x ⋆ y ⋆ 1) ⊔ (y ⋆ bot)"
    using order.trans while_one_mult_while_below by blast
  hence "(y ⋆ 1) * ((y ⋆ x) ⋆ (y ⋆ z)) ≤ x ⋆ ((y ⋆ 1) * (y ⋆ z) ⊔ (y ⋆ bot) * ((y ⋆ x) ⋆ (y ⋆ z)))"
    by (simp add: while_simulate_right_plus)
  also have "... ≤ x ⋆ ((y ⋆ z) ⊔ (y ⋆ bot))"
    by (metis sup_mono mult_left_zero order_refl while_absorb_2 while_one_mult_below while_right_isotone while_sub_associative)
  also have "... = x ⋆ y ⋆ z"
    using sup.absorb_iff1 while_right_isotone by auto
  finally show ?thesis
    by (smt sup_commute le_iff_sup mult_left_one mult_right_dist_sup while_plus_one while_sub_associative while_sumstar)
qed

text ‹Theorem 11.5›

lemma while_separate_left:
  "y * x ≤ x * (y ⋆ 1) ⟹ y ⋆ (x ⋆ z) ≤ x ⋆ (y ⋆ z)"
  by (metis sup_commute separation while_sub_dist_3)

text ‹Theorem 11.6›

lemma while_simulate_4:
  "y * x ≤ x * (x ⋆ (1 ⊔ y)) ⟹ y ⋆ (x ⋆ z) ≤ x ⋆ (y ⋆ z)"
  by (metis sup_commute while_separate_4 while_sub_dist_3)

lemma while_simulate_5:
  "y * x ≤ x * (x ⋆ (x ⊔ y)) ⟹ y ⋆ (x ⋆ z) ≤ x ⋆ (y ⋆ z)"
  by (smt order_trans while_sup_sub_sup_one_mult while_simulate_4)

lemma while_simulate_6:
  "y * x ≤ x * (x ⊔ y) ⟹ y ⋆ (x ⋆ z) ≤ x ⋆ (y ⋆ z)"
  by (smt order_trans while_increasing while_mult_star_exchange while_simulate_5)

text ‹Theorem 11.3›

lemma while_simulate_7:
  "y * x ≤ x * y ⟹ y ⋆ (x ⋆ z) ≤ x ⋆ (y ⋆ z)"
  using mult_left_sub_dist_sup_right order_lesseq_imp while_simulate_6 by blast

lemma while_while_mult_1:
  "x ⋆ (1 ⋆ y) = 1 ⋆ (x ⋆ y)"
  by (metis sup_commute mult_left_one mult_1_right order_refl while_separate_1)

text ‹Theorem 9.15›

lemma while_while_mult_2:
  "x ⋆ (1 ⋆ y) = (x ⋆ 1) ⋆ y"
  by (simp add: while_while_mult while_while_mult_1)

text ‹Theorem 11.8›

lemma while_import:
  assumes "p ≤ p * p ∧ p ≤ 1 ∧ p * x ≤ x * p"
    shows "p * (x ⋆ y) = p * ((p * x) ⋆ y)"
proof -
  have "p * (x ⋆ y) ≤ (p * x) ⋆ (p * y)"
    using assms test_preserves_equation while_simulate by auto
  also have "... ≤ (p * x) ⋆ y"
    by (metis assms le_iff_sup mult_left_one mult_right_dist_sup while_right_isotone)
  finally have 2: "p * (x ⋆ y) ≤ p * ((p * x) ⋆ y)"
    by (smt assms sup_commute le_iff_sup mult_assoc mult_left_dist_sup mult_1_right)
  have "p * ((p * x) ⋆ y) ≤ p * (x ⋆ y)"
    by (metis assms mult_left_isotone mult_left_one mult_right_isotone while_left_isotone)
  thus ?thesis
    using 2 order.antisym by auto
qed

text ‹Theorem 11.8›

lemma while_preserve:
  assumes "p ≤ p * p"
      and "p ≤ 1"
      and "p * x ≤ x * p"
    shows "p * (x ⋆ y) = p * (x ⋆ (p * y))"
proof (rule order.antisym)
  show "p * (x ⋆ y) ≤ p * (x ⋆ (p * y))"
    by (metis assms order.antisym coreflexive_transitive mult_right_isotone mult_assoc while_simulate)
  show "p * (x ⋆ (p * y)) ≤ p * (x ⋆ y)"
    by (metis assms(2) mult_left_isotone mult_left_one mult_right_isotone while_right_isotone)
qed

lemma while_plus_below_while:
  "(x ⋆ 1) * x ≤ x ⋆ 1"
  by (simp add: while_mult_upper_bound while_one_increasing)

text ‹Theorem 9.40›

lemma while_01:
  "(w * (x ⋆ 1)) ⋆ (y * z) ≤ (x ⋆ w) ⋆ ((x ⋆ y) * z)"
proof -
  have "(w * (x ⋆ 1)) ⋆ (y * z) = y * z ⊔ w * (((x ⋆ 1) * w) ⋆ ((x ⋆ 1) * y * z))"
    by (metis mult_assoc while_productstar)
  also have "... ≤ y * z ⊔ w * ((x ⋆ w) ⋆ ((x ⋆ y) * z))"
    by (metis sup_right_isotone mult_left_isotone mult_right_isotone while_isotone while_one_mult_below)
  also have "... ≤ (x ⋆ y) * z ⊔ (x ⋆ w) * ((x ⋆ w) ⋆ ((x ⋆ y) * z))"
    by (meson mult_left_isotone semiring.add_mono while_increasing)
  finally show ?thesis
    using while_left_unfold by auto
qed

text ‹Theorem 9.37›

lemma while_while_sub_associative:
  "x ⋆ (y ⋆ z) ≤ ((x ⋆ y) ⋆ z) ⊔ (x ⋆ z)"
proof -
  have 1: "x * (x ⋆ 1) ≤ (x ⋆ 1) * ((x ⋆ y) ⋆ 1)"
    by (metis le_supE while_back_loop_prefixpoint while_mult_increasing while_mult_transitive while_one_while)
  have "x ⋆ (y ⋆ z) ≤ x ⋆ ((x ⋆ 1) * (y ⋆ z))"
    by (metis mult_left_isotone mult_left_one while_increasing while_right_isotone)
  also have "... ≤ (x ⋆ 1) * ((x ⋆ y) ⋆ (y ⋆ z)) ⊔ (x ⋆ bot)"
    using 1 while_simulate_left_plus_1 by auto
  also have "... ≤ (x ⋆ 1) * ((x ⋆ y) ⋆ z) ⊔ (x ⋆ z)"
    by (simp add: le_supI1 sup_commute while_absorb_2 while_increasing while_right_isotone)
  also have "... = (x ⋆ 1) * z ⊔ (x ⋆ 1) * (x ⋆ y) * ((x ⋆ y) ⋆ z) ⊔ (x ⋆ z)"
    by (metis mult_assoc mult_left_dist_sup while_left_unfold)
  also have "... = (x ⋆ y) * ((x ⋆ y) ⋆ z) ⊔ (x ⋆ z)"
    by (smt sup_assoc sup_commute le_iff_sup mult_left_one mult_right_dist_sup order_refl while_absorb_1 while_plus_one while_sub_associative)
  also have "... ≤ ((x ⋆ y) ⋆ z) ⊔ (x ⋆ z)"
    using sup_left_isotone while_left_plus_below by auto
  finally show ?thesis
    .
qed

lemma while_induct:
  "x * z ≤ z ∧ y ≤ z ∧ x ⋆ 1 ≤ z ⟹ x ⋆ y ≤ z"
  by (metis le_supI1 sup_commute sup_bot_left le_iff_sup while_right_isotone while_simulate_absorb)

proposition while_sumstar_4_below: "(x ⋆ y) ⋆ ((x ⋆ 1) * z) ≤ x ⋆ ((y * (x ⋆ 1)) ⋆ z)" oops
proposition while_sumstar_2: "(x ⊔ y) ⋆ z = x ⋆ ((y * (x ⋆ 1)) ⋆ z)" oops
proposition while_sumstar_3: "(x ⊔ y) ⋆ z = ((x ⋆ 1) * y) ⋆ (x ⋆ z)" oops
proposition while_decompose_6: "x ⋆ ((y * (x ⋆ 1)) ⋆ z) = y ⋆ ((x * (y ⋆ 1)) ⋆ z)" oops
proposition while_finite_associative: "x ⋆ bot = bot ⟹ (x ⋆ y) * z = x ⋆ (y * z)" oops
proposition atomicity_refinement: "s = s * q ⟹ x = q * x ⟹ q * b = bot ⟹ r * b ≤ b * r ⟹ r * l ≤ l * r ⟹ x * l ≤ l * x ⟹ b * l ≤ l * b ⟹ q * l ≤ l * q ⟹ r ⋆ q ≤ q * (r ⋆ 1) ⟹ q ≤ 1 ⟹ s * ((x ⊔ b ⊔ r ⊔ l) ⋆ (q * z)) ≤ s * ((x * (b ⋆ q) ⊔ r ⊔ l) ⋆ z)" oops

proposition while_separate_right_plus: "y * x ≤ x * (x ⋆ (1 ⊔ y)) ⊔ 1 ⟹ y ⋆ (x ⋆ z) ≤ x ⋆ (y ⋆ z)" oops
proposition while_square_1: "x ⋆ 1 = (x * x) ⋆ (x ⊔ 1)" oops
proposition while_absorb_below_one: "y * x ≤ x ⟹ y ⋆ x ≤ 1 ⋆ x" oops
proposition "y ⋆ (x ⋆ 1) ≤ x ⋆ (y ⋆ 1) ⟹ (x ⊔ y) ⋆ 1 = x ⋆ (y ⋆ 1)" oops
proposition "y * x ≤ (1 ⊔ x) * (y ⋆ 1) ⟹ (x ⊔ y) ⋆ 1 = x ⋆ (y ⋆ 1)" oops

end

class bounded_binary_itering = bounded_idempotent_left_zero_semiring + binary_itering
begin

text ‹Theorem 9›

lemma while_right_top:
  "x ⋆ top = top"
  by (metis sup_left_top while_left_unfold)

text ‹Theorem 9›

lemma while_left_top:
  "top * (x ⋆ 1) = top"
  by (meson order.antisym le_supE top_greatest while_back_loop_prefixpoint)

end

class extended_binary_itering = binary_itering +
  assumes while_denest_0: "w * (x ⋆ (y * z)) ≤ (w * (x ⋆ y)) ⋆ (w * (x ⋆ y) * z)"
begin

text ‹Theorem 10.2›

lemma while_denest_1:
  "w * (x ⋆ (y * z)) ≤ (w * (x ⋆ y)) ⋆ z"
  using while_denest_0 while_mult_increasing while_mult_transitive by blast

lemma while_mult_sub_while_while:
  "x ⋆ (y * z) ≤ (x ⋆ y) ⋆ z"
  by (metis mult_left_one while_denest_1)

lemma while_zero_zero:
  "(x ⋆ bot) ⋆ bot = x ⋆ bot"
  by (metis order.antisym mult_left_zero sup_bot_left while_left_unfold while_sub_associative while_mult_sub_while_while)

text ‹Theorem 10.11›

lemma while_mult_zero_zero:
  "(x * (y ⋆ bot)) ⋆ bot = x * (y ⋆ bot)"
  apply (rule order.antisym)
  apply (metis sup_bot_left while_left_unfold mult_assoc le_supI1 mult_left_zero mult_right_isotone while_left_dist_sup while_sub_associative)
  by (metis mult_left_zero while_denest_1)

text ‹Theorem 10.3›

lemma while_denest_2:
  "w * ((x ⋆ (y * w)) ⋆ z) = w * (((x ⋆ y) * w) ⋆ z)"
  apply (rule order.antisym)
  apply (metis mult_assoc while_denest_0 while_simulate_right_plus_1 while_slide)
  by (simp add: mult_isotone while_left_isotone while_sub_associative)

text ‹Theorem 10.12›

lemma while_denest_3:
  "(x ⋆ w) ⋆ (x ⋆ bot) = (x ⋆ w) ⋆ bot"
  by (metis while_absorb_2 while_right_isotone while_zero_zero bot_least)

text ‹Theorem 10.15›

lemma while_02:
  "x ⋆ ((x ⋆ w) ⋆ ((x ⋆ y) * z)) = (x ⋆ w) ⋆ ((x ⋆ y) * z)"
proof -
  have "x * ((x ⋆ w) ⋆ ((x ⋆ y) * z)) = x * (x ⋆ y) * z ⊔ x * (x ⋆ w) * ((x ⋆ w) ⋆ ((x ⋆ y) * z))"
    by (metis mult_assoc mult_left_dist_sup while_left_unfold)
  also have "... ≤ (x ⋆ w) ⋆ ((x ⋆ y) * z)"
    by (metis sup_mono mult_right_sub_dist_sup_right while_left_unfold)
  finally have "x ⋆ ((x ⋆ w) ⋆ ((x ⋆ y) * z)) ≤ ((x ⋆ w) ⋆ ((x ⋆ y) * z)) ⊔ (x ⋆ bot)"
    using while_simulate_absorb by auto
  also have "... = (x ⋆ w) ⋆ ((x ⋆ y) * z)"
    by (metis sup_commute le_iff_sup order_trans while_mult_sub_while_while while_right_isotone bot_least)
  finally show ?thesis
    by (simp add: order.antisym while_increasing)
qed

lemma while_sumstar_3_below:
  "(x ⋆ y) ⋆ (x ⋆ z) ≤ (x ⋆ y) ⋆ ((x ⋆ 1) * z)"
proof -
  have "(x ⋆ y) ⋆ (x ⋆ z) = (x ⋆ z) ⊔ ((x ⋆ y) ⋆ ((x ⋆ y) * (x ⋆ z)))"
    using while_right_unfold by blast
  also have "... ≤ (x ⋆ z) ⊔ ((x ⋆ y) ⋆ (x ⋆ (y * (x ⋆ z))))"
    by (meson sup_right_isotone while_right_isotone while_sub_associative)
  also have "... ≤ (x ⋆ z) ⊔ ((x ⋆ y) ⋆ (x ⋆ ((x ⋆ y) ⋆ (x ⋆ z))))"
    by (smt sup_right_isotone order_trans while_increasing while_mult_upper_bound while_one_increasing while_right_isotone)
  also have "... ≤ (x ⋆ z) ⊔ ((x ⋆ y) ⋆ (x ⋆ ((x ⋆ y) ⋆ ((x ⋆ 1) * z))))"
    by (metis sup_right_isotone mult_left_isotone mult_left_one order_trans while_increasing while_right_isotone while_sumstar while_transitive)
  also have "... = (x ⋆ z) ⊔ ((x ⋆ y) ⋆ ((x ⋆ 1) * z))"
    by (simp add: while_transitive while_02)
  also have "... = (x ⋆ y) ⋆ ((x ⋆ 1) * z)"
    by (smt sup_assoc mult_left_one mult_right_dist_sup while_02 while_left_dist_sup while_plus_one)
  finally show ?thesis
    .
qed

lemma while_sumstar_4_below:
  "(x ⋆ y) ⋆ ((x ⋆ 1) * z) ≤ x ⋆ ((y * (x ⋆ 1)) ⋆ z)"
proof -
  have "(x ⋆ y) ⋆ ((x ⋆ 1) * z) = (x ⋆ 1) * z ⊔ (x ⋆ y) * ((x ⋆ y) ⋆ ((x ⋆ 1) * z))"
    using while_left_unfold by auto
  also have "... ≤ (x ⋆ z) ⊔ (x ⋆ (y * ((x ⋆ y) ⋆ ((x ⋆ 1) * z))))"
    by (meson sup_mono while_one_mult_below while_sub_associative)
  also have "... = (x ⋆ z) ⊔ (x ⋆ (y * (((x ⋆ 1) * y) ⋆ ((x ⋆ 1) * z))))"
    by (metis mult_left_one while_denest_2)
  also have "... = x ⋆ ((y * (x ⋆ 1)) ⋆ z)"
    by (metis while_left_dist_sup while_productstar)
  finally show ?thesis
    .
qed

text ‹Theorem 10.10›

lemma while_sumstar_1:
  "(x ⊔ y) ⋆ z = (x ⋆ y) ⋆ ((x ⋆ 1) * z)"
  by (smt order.eq_iff order_trans while_sup_1_below while_sumstar while_sumstar_3_below while_sumstar_4_below)

text ‹Theorem 10.8›

lemma while_sumstar_2:
  "(x ⊔ y) ⋆ z = x ⋆ ((y * (x ⋆ 1)) ⋆ z)"
  using order.antisym while_sup_1_below while_sumstar_1 while_sumstar_4_below by auto

text ‹Theorem 10.9›

lemma while_sumstar_3:
  "(x ⊔ y) ⋆ z = ((x ⋆ 1) * y) ⋆ (x ⋆ z)"
  using order.antisym while_sumstar while_sumstar_1_below while_sumstar_2_below while_sumstar_2 by force

text ‹Theorem 10.6›

lemma while_decompose_6:
  "x ⋆ ((y * (x ⋆ 1)) ⋆ z) = y ⋆ ((x * (y ⋆ 1)) ⋆ z)"
  by (metis sup_commute while_sumstar_2)

text ‹Theorem 10.4›

lemma while_denest_4:
  "(x ⋆ w) ⋆ (x ⋆ (y * z)) = (x ⋆ w) ⋆ ((x ⋆ y) * z)"
proof -
  have "(x ⋆ w) ⋆ (x ⋆ (y * z)) = x ⋆ ((w * (x ⋆ 1)) ⋆ (y * z))"
    using while_sumstar while_sumstar_2 by force
  also have "... ≤ (x ⋆ w) ⋆ ((x ⋆ y) * z)"
    by (metis while_01 while_right_isotone while_02)
  finally show ?thesis
    using order.antisym while_right_isotone while_sub_associative by auto
qed

text ‹Theorem 10.13›

lemma while_denest_5:
  "w * ((x ⋆ (y * w)) ⋆ (x ⋆ (y * z))) = w * (((x ⋆ y) * w) ⋆ ((x ⋆ y) * z))"
  by (simp add: while_denest_2 while_denest_4)

text ‹Theorem 10.5›

lemma while_denest_6:
  "(w * (x ⋆ y)) ⋆ z = z ⊔ w * ((x ⊔ y * w) ⋆ (y * z))"
  by (metis while_denest_5 while_productstar while_sumstar)

text ‹Theorem 10.1›

lemma while_sum_below_one:
  "y * ((x ⊔ y) ⋆ z) ≤ (y * (x ⋆ 1)) ⋆ z"
  by (simp add: while_denest_6)

text ‹Theorem 10.14›

lemma while_separate_unfold:
  "(y * (x ⋆ 1)) ⋆ z = (y ⋆ z) ⊔ (y ⋆ (y * x * (x ⋆ ((y * (x ⋆ 1)) ⋆ z))))"
proof -
  have "y ⋆ (y * x * (x ⋆ ((y * (x ⋆ 1)) ⋆ z))) ≤ y ⋆ (y * ((x ⊔ y) ⋆ z))"
    using mult_right_isotone while_left_plus_below while_right_isotone mult_assoc while_sumstar_2 by auto
  also have "... ≤ (y * (x ⋆ 1)) ⋆ z"
    by (metis sup_commute sup_ge1 while_absorb_1 while_mult_star_exchange while_sum_below_one)
  finally have "(y ⋆ z) ⊔ (y ⋆ (y * x * (x ⋆ ((y * (x ⋆ 1)) ⋆ z)))) ≤ (y * (x ⋆ 1)) ⋆ z"
    using sup.bounded_iff while_back_loop_prefixpoint while_left_isotone by auto
  thus ?thesis
    by (simp add: order.antisym while_separate_unfold_below)
qed

text ‹Theorem 10.7›

lemma while_finite_associative:
  "x ⋆ bot = bot ⟹ (x ⋆ y) * z = x ⋆ (y * z)"
  by (metis while_denest_4 while_zero)

text ‹Theorem 12›

lemma atomicity_refinement:
  assumes "s = s * q"
      and "x = q * x"
      and "q * b = bot"
      and "r * b ≤ b * r"
      and "r * l ≤ l * r"
      and "x * l ≤ l * x"
      and "b * l ≤ l * b"
      and "q * l ≤ l * q"
      and "r ⋆ q ≤ q * (r ⋆ 1) ∧ q ≤ 1"
    shows "s * ((x ⊔ b ⊔ r ⊔ l) ⋆ (q * z)) ≤ s * ((x * (b ⋆ q) ⊔ r ⊔ l) ⋆ z)"
proof -
  have 1: "(x ⊔ b ⊔ r) * l ≤ l * (x ⊔ b ⊔ r)"
    by (smt assms(5-7) mult_left_dist_sup semiring.add_mono semiring.distrib_right)
  have "q * ((x * (b ⋆ r ⋆ 1) * q) ⋆ z) ≤ (x * (b ⋆ r ⋆ 1) * q) ⋆ z"
    using assms(9) order_lesseq_imp while_increasing while_mult_upper_bound by blast
  also have "... ≤ (x * (b ⋆ ((r ⋆ 1) * q))) ⋆ z"
    by (simp add: mult_right_isotone while_left_isotone while_sub_associative mult_assoc)
  also have "... ≤ (x * (b ⋆ r ⋆ q)) ⋆ z"
    by (simp add: mult_right_isotone while_left_isotone while_one_mult_below while_right_isotone)
  also have "... ≤ (x * (b ⋆ (q * (r ⋆ 1)))) ⋆ z"
    by (simp add: assms(9) mult_right_isotone while_left_isotone while_right_isotone)
  finally have 2: "q * ((x * (b ⋆ r ⋆ 1) * q) ⋆ z) ≤ (x * (b ⋆ q) * (r ⋆ 1)) ⋆ z"
    using while_associative_while_1 mult_assoc by auto
  have "s * ((x ⊔ b ⊔ r ⊔ l) ⋆ (q * z)) = s * (l ⋆ (x ⊔ b ⊔ r) ⋆ (q * z))"
    using 1 sup_commute while_separate_1 by fastforce
  also have "... = s * q * (l ⋆ b ⋆ r ⋆ (q * x * (b ⋆ r ⋆ 1)) ⋆ (q * z))"
    by (smt assms(1,2,4) sup_assoc sup_commute while_sumstar_2 while_separate_1)
  also have "... = s * q * (l ⋆ b ⋆ r ⋆ (q * ((x * (b ⋆ r ⋆ 1) * q) ⋆ z)))"
    by (simp add: while_slide mult_assoc)
  also have "... ≤ s * q * (l ⋆ b ⋆ r ⋆ (x * (b ⋆ q) * (r ⋆ 1)) ⋆ z)"
    using 2 by (meson mult_right_isotone while_right_isotone)
  also have "... ≤ s * (l ⋆ q * (b ⋆ r ⋆ (x * (b ⋆ q) * (r ⋆ 1)) ⋆ z))"
    by (simp add: assms(8) mult_right_isotone while_simulate mult_assoc)
  also have "... = s * (l ⋆ q * (r ⋆ (x * (b ⋆ q) * (r ⋆ 1)) ⋆ z))"
    using assms(3) while_elimination by auto
  also have "... ≤ s * (l ⋆ r ⋆ (x * (b ⋆ q) * (r ⋆ 1)) ⋆ z)"
    by (meson assms(9) order.trans mult_right_isotone order.refl while_increasing while_mult_upper_bound while_right_isotone)
  also have "... = s * (l ⋆ (r ⊔ x * (b ⋆ q)) ⋆ z)"
    by (simp add: while_sumstar_2)
  also have "... ≤ s * ((x * (b ⋆ q) ⊔ r ⊔ l) ⋆ z)"
    using mult_right_isotone sup_commute while_sub_dist_3 by auto
  finally show ?thesis
    .
qed

end

class bounded_extended_binary_itering = bounded_binary_itering + extended_binary_itering

end