Theory N_Omega_Binary_Iterings

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

section ‹N-Omega Binary Iterings›

theory N_Omega_Binary_Iterings

imports N_Omega_Algebras Binary_Iterings_Strict

begin

sublocale extended_binary_itering < left_zero_conway_semiring where circ = "(λx . x ⋆ 1)"
  apply unfold_locales
  using while_left_unfold apply force
  apply (metis mult_1_right while_one_mult_below while_slide)
  by (simp add: while_one_while while_sumstar_2)

class binary_itering_apx = bounded_binary_itering + n_algebra_apx
begin

lemma C_while_import:
  "C (x ⋆ z) = C (C x ⋆ z)"
proof -
  have 1: "C x * (x ⋆ z) ≤ C x ⋆ (C x * z)"
    using C_mult_propagate while_simulate by force
  have "C (x ⋆ z) = C z ⊔ C x * (x ⋆ z)"
    by (metis inf_sup_distrib1 n_L_T_meet_mult while_left_unfold)
  also have "... ≤ C x ⋆ z"
    using 1 by (metis C_decreasing sup_mono while_right_unfold)
  finally have "C (x ⋆ z) ≤ C (C x ⋆ z)"
    by simp
  thus ?thesis
    by (metis order.antisym inf.boundedI inf.cobounded1 inf.coboundedI2 inf.sup_monoid.add_commute while_absorb_2 while_increasing)
qed

lemma C_while_preserve:
  "C (x ⋆ z) = C (x ⋆ C z)"
proof -
  have "C x * (x ⋆ z) ≤ C x ⋆ (C x * z)"
    using C_mult_propagate while_simulate by auto
  also have "... ≤ x ⋆ (x * C z)"
    using C_decreasing n_L_T_meet_mult_propagate while_isotone by blast
  finally have 1: "C x * (x ⋆ z) ≤ x ⋆ (x * C z)"
    .
  have "C (x ⋆ z) = C z ⊔ C x * (x ⋆ z)"
    by (metis inf_sup_distrib1 n_L_T_meet_mult while_left_unfold)
  also have "... ≤ x ⋆ C z"
    using 1 by (meson order.trans le_supI while_increasing while_right_plus_below)
  finally have "C (x ⋆ z) ≤ C (x ⋆ C z)"
    by simp
  thus ?thesis
    by (meson order.antisym inf.boundedI inf.cobounded1 inf.coboundedI2 inf.eq_refl while_isotone)
qed

lemma C_while_import_preserve:
  "C (x ⋆ z) = C (C x ⋆ C z)"
  using C_while_import C_while_preserve by auto

lemma while_L_L:
  "L ⋆ L = L"
  by (metis n_L_top_L while_mult_star_exchange while_right_top)

lemma while_L_below_sup:
  "L ⋆ x ≤ x ⊔ L"
  by (metis while_left_unfold sup_right_isotone n_L_below_L)

lemma while_L_split:
  "x ⋆ L ≤ (x ⋆ y) ⊔ L"
proof -
  have "x ⋆ L ≤ (x ⋆ bot) ⊔ L"
    by (metis sup_commute sup_bot_left mult_1_right n_L_split_L while_right_unfold while_simulate_left_plus while_zero)
  thus ?thesis
    by (metis sup_commute sup_right_isotone order_trans while_right_isotone bot_least)
qed

lemma while_n_while_top_split:
  "x ⋆ (n(x ⋆ y) * top) ≤ (x ⋆ bot) ⊔ n(x ⋆ y) * top"
proof -
  have "x * n(x ⋆ y) * top ≤ x * bot ⊔ n(x * (x ⋆ y)) * top"
    by (simp add: n_n_top_split_n_top)
  also have "... ≤ n(x ⋆ y) * top ⊔ x * bot"
    by (metis sup_commute sup_right_isotone mult_left_isotone n_isotone while_left_plus_below)
  finally have "x ⋆ (n(x ⋆ y) * top) ≤ n(x ⋆ y) * top ⊔ (x ⋆ (x * bot))"
    by (metis mult_assoc mult_1_right while_simulate_left mult_left_zero while_left_top)
  also have "... ≤ (x ⋆ bot) ⊔ n(x ⋆ y) * top"
    using sup_left_isotone while_right_plus_below by auto
  finally show ?thesis
    .
qed

lemma circ_apx_right_isotone:
  assumes "x ⊑ y"
    shows "z ⋆ x ⊑ z ⋆ y"
proof -
  have 1: "x ≤ y ⊔ L ∧ C y ≤ x ⊔ n(x) * top"
    using assms apx_def by auto
  hence "z ⋆ x ≤ (z ⋆ y) ⊔ (z ⋆ L)"
    by (metis while_left_dist_sup while_right_isotone)
  hence 2: "z ⋆ x ≤ (z ⋆ y) ⊔ L"
    by (meson le_supI order_lesseq_imp sup.cobounded1 while_L_split)
  have "z ⋆ (n(z ⋆ x) * top) ≤ (z ⋆ bot) ⊔ n(z ⋆ x) * top"
    by (simp add: while_n_while_top_split)
  also have "... ≤ (z ⋆ x) ⊔ n(z ⋆ x) * top"
    using sup_left_isotone while_right_isotone by force
  finally have 3: "z ⋆ (n(x) * top) ≤ (z ⋆ x) ⊔ n(z ⋆ x) * top"
    by (metis mult_left_isotone n_isotone order_trans while_increasing while_right_isotone)
  have "C (z ⋆ y) ≤ z ⋆ C y"
    by (metis C_while_preserve inf.cobounded2)
  also have "... ≤ (z ⋆ x) ⊔ (z ⋆ (n(x) * top))"
    using 1 by (metis while_left_dist_sup while_right_isotone)
  also have "... ≤ (z ⋆ x) ⊔ n(z ⋆ x) * top"
    using 3 by simp
  finally show ?thesis
    using 2 apx_def by auto
qed

end

class extended_binary_itering_apx = binary_itering_apx + bounded_extended_binary_itering +
  assumes n_below_while_zero: "n(x) ≤ n(x ⋆ bot)"
begin

lemma circ_apx_right_isotone:
  assumes "x ⊑ y"
    shows "x ⋆ z ⊑ y ⋆ z"
proof -
  have 1: "x ≤ y ⊔ L ∧ C y ≤ x ⊔ n(x) * top"
    using assms apx_def by auto
  hence "x ⋆ z ≤ ((y ⋆ 1) * L) ⋆ (y ⋆ z)"
    by (metis while_left_isotone while_sumstar_3)
  also have "... ≤ (y ⋆ z) ⊔ (y ⋆ 1) * L"
    by (metis while_productstar sup_right_isotone mult_right_isotone n_L_below_L while_slide)
  also have "... ≤ (y ⋆ z) ⊔ L"
    by (meson order.trans le_supI sup.cobounded1 while_L_split while_one_mult_below)
  finally have 2: "x ⋆ z ≤ (y ⋆ z) ⊔ L"
    .
  have "C (y ⋆ z) ≤ C y ⋆ z"
    by (metis C_while_import inf.sup_right_divisibility)
  also have "... ≤ ((x ⋆ 1) * n(x) * top) ⋆ (x ⋆ z)"
    using 1 by (metis while_left_isotone mult_assoc while_sumstar_3)
  also have "... ≤ (x ⋆ z) ⊔ (x ⋆ 1) * n(x) * top"
    by (metis while_productstar sup_left_top sup_right_isotone mult_assoc mult_left_sub_dist_sup_right while_slide)
  also have "... ≤ (x ⋆ z) ⊔ (x ⋆ (n(x) * top))"
    using sup_right_isotone while_one_mult_below mult_assoc by auto
  also have "... ≤ (x ⋆ z) ⊔ (x ⋆ (n(x ⋆ z) * top))"
    by (metis n_below_while_zero bot_least while_right_isotone n_isotone mult_left_isotone sup_right_isotone order_trans)
  also have "... ≤ (x ⋆ z) ⊔ n(x ⋆ z) * top"
    by (metis sup_assoc sup_right_isotone while_n_while_top_split sup_bot_right while_left_dist_sup)
  finally show ?thesis
    using 2 apx_def by auto
qed

proposition while_top: "top ⋆ x = L ⊔ top * x" oops
proposition while_one_top: "1 ⋆ x = L ⊔ x" oops
proposition while_unfold_below_1: "x = y * x ⟹ x ≤ y ⋆ 1" 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 while_mult_L: "(x * L) ⋆ z = z ⊔ x * L" oops
proposition tarski_top_omega_below_2: "x * L ≤ (x * L) ⋆ bot" oops
proposition tarski_top_omega_2: "x * L = (x * L) ⋆ bot" oops
proposition while_separate_right_plus: "y * x ≤ x * (x ⋆ (1 ⊔ y)) ⊔ 1 ⟹ y ⋆ (x ⋆ z) ≤ x ⋆ (y ⋆ z)" 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 n_omega_algebra_binary = n_omega_algebra + while +
  assumes while_def: "x ⋆ y = n(xω) * L ⊔ x⋆ * y"
begin

lemma while_omega_inf_L_star:
  "x ⋆ y = (xω ⊓ L) ⊔ x⋆ * y"
  by (metis loop_semantics_kappa_mu_nu loop_semantics_kappa_mu_nu_2 while_def)

lemma while_one_mult_while_below_1:
  "(y ⋆ 1) * (y ⋆ v) ≤ y ⋆ v"
proof -
  have "(y ⋆ 1) * (y ⋆ v) ≤ y ⋆ (y ⋆ v)"
    by (smt sup_left_isotone mult_assoc mult_right_dist_sup mult_right_isotone n_L_below_L while_def mult_left_one)
  also have "... = n(yω) * L ⊔ y⋆ * n(yω) * L ⊔ y⋆ * y⋆ * v"
    by (simp add: mult_left_dist_sup sup_assoc while_def mult_assoc)
  also have "... = n(yω) * L ⊔ (y⋆ * y⋆ * bot ⊔ y⋆ * n(yω) * L) ⊔ y⋆ * y⋆ * v"
    by (metis mult_left_dist_sup star.circ_transitive_equal sup_bot_left mult_assoc)
  also have "... = n(yω) * L ⊔ (y⋆ * y⋆ * bot ⊔ n(y⋆ * yω) * L) ⊔ y⋆ * y⋆ * v"
    by (simp add: n_mult_omega_L_star_zero)
  also have "... = n(yω) * L ⊔ n(y⋆ * yω) * L ⊔ y⋆ * y⋆ * v"
    by (smt (z3) mult_left_dist_sup sup.left_commute sup_bot_left sup_commute)
  finally show ?thesis
    by (simp add: star.circ_transitive_equal star_mult_omega while_def)
qed

lemma star_below_while:
  "x⋆ * y ≤ x ⋆ y"
  by (simp add: while_def)

subclass bounded_binary_itering
proof unfold_locales
  fix x y z
  have "z ⊔ x * ((y * x) ⋆ (y * z)) = x * (y * x)⋆ * y * z ⊔ x * n((y * x)ω) * L ⊔ z"
    using mult_left_dist_sup sup_commute while_def mult_assoc by auto
  also have "... = x * (y * x)⋆ * y * z ⊔ n(x * (y * x)ω) * L ⊔ z"
    by (metis mult_assoc mult_right_isotone bot_least n_mult_omega_L_star_zero sup_relative_same_increasing)
  also have "... = (x * y)⋆ * z ⊔ n(x * (y * x)ω) * L"
    by (smt sup_assoc sup_commute mult_assoc star.circ_loop_fixpoint star_slide)
  also have "... = (x * y) ⋆ z"
    by (simp add: omega_slide sup_monoid.add_commute while_def)
  finally show "(x * y) ⋆ z = z ⊔ x * ((y * x) ⋆ (y * z))"
    by simp
next
  fix x y z
  have "(x ⋆ y) ⋆ (x ⋆ z) = n((n(xω) * L ⊔ x⋆ * y)ω) * L ⊔ (n(xω) * L ⊔ x⋆ * y)⋆ * (x ⋆ z)"
    by (simp add: while_def)
  also have "... = n((x⋆ * y)ω ⊔ (x⋆ * y)⋆ * n(xω) * L) * L ⊔ ((x⋆ * y)⋆ ⊔ (x⋆ * y)⋆ * n(xω) * L) * (x ⋆ z)"
    using mult_L_sup_omega mult_L_sup_star by force
  also have "... = n((x⋆ * y)ω) * L ⊔ n((x⋆ * y)⋆ * n(xω) * L) * L ⊔ (x⋆ * y)⋆ * (x ⋆ z) ⊔ (x⋆ * y)⋆ * n(xω) * L * (x ⋆ z)"
    by (simp add: mult_right_dist_sup n_dist_omega_star sup_assoc mult_assoc)
  also have "... = n((x⋆ * y)ω) * L ⊔ n((x⋆ * y)⋆ * n(xω) * L) * L ⊔ (x⋆ * y)⋆ * bot ⊔ (x⋆ * y)⋆ * (x ⋆ z) ⊔ (x⋆ * y)⋆ * n(xω) * L * (x ⋆ z)"
    by (smt sup_assoc sup_bot_left mult_left_dist_sup)
  also have "... = n((x⋆ * y)ω) * L ⊔ ((x⋆ * y)⋆ * n(xω) * L * (x ⋆ z) ⊔ (x⋆ * y)⋆ * n(xω) * L ⊔ (x⋆ * y)⋆ * (x ⋆ z))"
    by (smt n_n_L_split_n_n_L_L sup_commute sup_assoc)
  also have "... = n((x⋆ * y)ω) * L ⊔ ((x⋆ * y)⋆ * n(xω) * L ⊔ (x⋆ * y)⋆ * (x ⋆ z))"
    by (smt mult_L_omega omega_sub_vector le_iff_sup)
  also have "... = n((x⋆ * y)ω) * L ⊔ (x⋆ * y)⋆ * (x ⋆ z)"
    using mult_left_sub_dist_sup_left sup_absorb2 while_def mult_assoc by auto
  also have "... = (x⋆ * y)⋆ * x⋆ * z ⊔ (x⋆ * y)⋆ * n(xω) * L ⊔ n((x⋆ * y)ω) * L"
    by (simp add: mult_left_dist_sup sup_commute while_def mult_assoc)
  also have "... = (x⋆ * y)⋆ * x⋆ * z ⊔ n((x⋆ * y)⋆ * xω) * L ⊔ n((x⋆ * y)ω) * L"
    by (metis sup_bot_right mult_left_dist_sup sup_assoc n_mult_omega_L_star_zero)
  also have "... = (x ⊔ y) ⋆ z"
    using n_dist_omega_star omega_decompose semiring.combine_common_factor star.circ_sup_9 sup_commute while_def by force
  finally show "(x ⊔ y) ⋆ z = (x ⋆ y) ⋆ (x ⋆ z)"
    by simp
next
  fix x y z
  show "x ⋆ (y ⊔ z) = (x ⋆ y) ⊔ (x ⋆ z)"
    using semiring.distrib_left sup_assoc sup_commute while_def by force
next
  fix x y z
  show "(x ⋆ y) * z ≤ x ⋆ (y * z)"
    by (smt sup_left_isotone mult_assoc mult_right_dist_sup mult_right_isotone n_L_below_L while_def)
next
  fix v w x y z
  show "x * z ≤ z * (y ⋆ 1) ⊔ w ⟶ x ⋆ (z * v) ≤ z * (y ⋆ v) ⊔ (x ⋆ (w * (y ⋆ v)))"
  proof
    assume 1: "x * z ≤ z * (y ⋆ 1) ⊔ w"
    have "z * v ⊔ x * (z * (y ⋆ v) ⊔ x⋆ * (w * (y ⋆ v))) ≤ z * v ⊔ x * z * (y ⋆ v) ⊔ x⋆ * (w * (y ⋆ v))"
      by (metis sup_assoc sup_right_isotone mult_assoc mult_left_dist_sup mult_left_isotone star.left_plus_below_circ)
    also have "... ≤ z * v ⊔ z * (y ⋆ 1) * (y ⋆ v) ⊔ w * (y ⋆ v) ⊔ x⋆ * (w * (y ⋆ v))"
      using 1 by (metis sup_assoc sup_left_isotone sup_right_isotone mult_left_isotone mult_right_dist_sup)
    also have "... ≤ z * v ⊔ z * (y ⋆ v) ⊔ x⋆ * (w * (y ⋆ v))"
      by (smt (verit, ccfv_threshold) sup_ge2 le_iff_sup mult_assoc mult_left_dist_sup star.circ_loop_fixpoint while_one_mult_while_below_1 le_supE le_supI)
    also have "... = z * (y ⋆ v) ⊔ x⋆ * (w * (y ⋆ v))"
      by (metis le_iff_sup le_supE mult_right_isotone star.circ_loop_fixpoint star_below_while)
    finally have "x⋆ * z * v ≤ z * (y ⋆ v) ⊔ x⋆ * (w * (y ⋆ v))"
      using star_left_induct mult_assoc by auto
    thus "x ⋆ (z * v) ≤ z * (y ⋆ v) ⊔ (x ⋆ (w * (y ⋆ v)))"
      by (smt sup_assoc sup_commute sup_right_isotone mult_assoc while_def)
  qed
next
  fix v w x y z
  show "z * x ≤ y * (y ⋆ z) ⊔ w ⟶ z * (x ⋆ v) ≤ y ⋆ (z * v ⊔ w * (x ⋆ v))"
  proof
    assume "z * x ≤ y * (y ⋆ z) ⊔ w"
    hence 1: "z * x ≤ y * y⋆ * z ⊔ (y * n(yω) * L ⊔ w)"
      by (simp add: mult_left_dist_sup sup.left_commute sup_commute while_def mult_assoc)
    hence "z * x⋆ ≤ y⋆ * (z ⊔ (y * n(yω) * L ⊔ w) * x⋆)"
      by (simp add: star_circ_simulate_right_plus)
    also have "... = y⋆ * z ⊔ y⋆ * y * n(yω) * L ⊔ y⋆ * w * x⋆"
      by (simp add: L_mult_star semiring.distrib_left semiring.distrib_right sup_left_commute sup_monoid.add_commute mult_assoc)
    also have "... = y⋆ * z ⊔ n(y⋆ * y * yω) * L ⊔ y⋆ * w * x⋆"
      by (metis sup_relative_same_increasing mult_isotone n_mult_omega_L_star_zero star.left_plus_below_circ star.right_plus_circ bot_least)
    also have "... = n(yω) * L ⊔ y⋆ * z ⊔ y⋆ * w * x⋆"
      using omega_unfold star_mult_omega sup_commute mult_assoc by force
    finally have "z * x⋆ * v ≤ n(yω) * L * v ⊔ y⋆ * z * v ⊔ y⋆ * w * x⋆ * v"
      by (smt le_iff_sup mult_right_dist_sup)
    also have "... ≤ n(yω) * L ⊔ y⋆ * (z * v ⊔ w * x⋆ * v)"
      by (metis n_L_below_L mult_assoc mult_right_isotone sup_left_isotone mult_left_dist_sup sup_assoc)
    also have "... ≤ n(yω) * L ⊔ y⋆ * (z * v ⊔ w * (x ⋆ v))"
      using mult_right_isotone semiring.add_left_mono mult_assoc star_below_while by auto
    finally have 2: "z * x⋆ * v ≤ y ⋆ (z * v ⊔ w * (x ⋆ v))"
      by (simp add: while_def)
    have 3: "y⋆ * y * y⋆ * bot ≤ y⋆ * w * xω"
      by (metis sup_commute sup_bot_left mult_assoc mult_left_sub_dist_sup_left star.circ_loop_fixpoint star.circ_transitive_equal)
    have "z * xω ≤ y * y⋆ * z * xω ⊔ (y * n(yω) * L ⊔ w) * xω"
      using 1 by (metis mult_assoc mult_left_isotone mult_right_dist_sup omega_unfold)
    hence "z * xω ≤ yω ⊔ y⋆ * y * n(yω) * L * xω ⊔ y⋆ * w * xω"
      by (smt sup_assoc sup_commute left_plus_omega mult_assoc mult_left_dist_sup mult_right_dist_sup omega_induct star.left_plus_circ)
    also have "... ≤ yω ⊔ y⋆ * y * n(yω) * L ⊔ y⋆ * w * xω"
      by (metis sup_left_isotone sup_right_isotone mult_assoc mult_right_isotone n_L_below_L)
    also have "... = yω ⊔ n(y⋆ * y * yω) * L ⊔ y⋆ * w * xω"
      using 3 by (smt sup_assoc sup_commute sup_relative_same_increasing n_mult_omega_L_star_zero)
    also have "... = yω ⊔ y⋆ * w * xω"
      by (metis mult_assoc omega_unfold star_mult_omega sup_commute le_iff_sup n_L_decreasing)
    finally have "n(z * xω) * L ≤ n(yω) * L ⊔ n(y⋆ * w * xω) * L"
      by (metis mult_assoc mult_left_isotone mult_right_dist_sup n_dist_omega_star n_isotone)
    also have "... ≤ n(yω) * L ⊔ y⋆ * (w * (n(xω) * L ⊔ x⋆ * bot))"
      by (smt sup_commute sup_right_isotone mult_assoc mult_left_dist_sup n_mult_omega_L_below_zero)
    also have "... ≤ n(yω) * L ⊔ y⋆ * (w * (n(xω) * L ⊔ x⋆ * v))"
      by (metis sup_right_isotone mult_right_isotone bot_least)
    also have "... ≤ n(yω) * L ⊔ y⋆ * (z * v ⊔ w * (n(xω) * L ⊔ x⋆ * v))"
      using mult_left_sub_dist_sup_right sup_right_isotone by auto
    finally have 4: "n(z * xω) * L ≤ y ⋆ (z * v ⊔ w * (x ⋆ v))"
      using while_def by auto
    have "z * (x ⋆ v) = z * n(xω) * L ⊔ z * x⋆ * v"
      by (simp add: mult_left_dist_sup while_def mult_assoc)
    also have "... = n(z * xω) * L ⊔ z * x⋆ * v"
      by (metis sup_commute sup_relative_same_increasing mult_right_isotone n_mult_omega_L_star_zero bot_least)
    finally show "z * (x ⋆ v) ≤ y ⋆ (z * v ⊔ w * (x ⋆ v))"
      using 2 4 by simp
  qed
qed

lemma while_top:
  "top ⋆ x = L ⊔ top * x"
  by (metis n_top_L star.circ_top star_omega_top while_def)

lemma while_one_top:
  "1 ⋆ x = L ⊔ x"
  by (smt mult_left_one n_top_L omega_one star_one while_def)

lemma while_finite_associative:
  "xω = bot ⟹ (x ⋆ y) * z = x ⋆ (y * z)"
  by (metis sup_bot_left mult_assoc n_zero_L_zero while_def)

lemma while_while_one:
  "y ⋆ (x ⋆ 1) = n(yω) * L ⊔ y⋆ * n(xω) * L ⊔ y⋆ * x⋆"
  by (simp add: mult_left_dist_sup sup_assoc while_def mult_assoc)

text ‹AACP Theorem 8.17›

subclass bounded_extended_binary_itering
proof unfold_locales
  fix w x y z
  have "w * (x ⋆ y * z) = n(w * n(xω) * L) * L ⊔ w * x⋆ * y * z"
    by (smt sup_assoc sup_commute sup_bot_left mult_assoc mult_left_dist_sup n_n_L_split_n_n_L_L while_def)
  also have "... ≤ n((w * n(xω) * L)ω) * L ⊔ w * x⋆ * y * z"
    by (simp add: mult_L_omega)
  also have "... ≤ n((w * (x ⋆ y))ω) * L ⊔ w * x⋆ * y * z"
    by (smt sup_left_isotone sup_ge1 mult_assoc mult_left_isotone mult_right_isotone n_isotone omega_isotone while_def)
  also have "... ≤ n((w * (x ⋆ y))ω) * L ⊔ w * (x ⋆ y) * z"
    by (metis star_below_while mult_assoc mult_left_isotone mult_right_isotone sup_right_isotone)
  also have "... ≤ n((w * (x ⋆ y))ω) * L ⊔ (w * (x ⋆ y))⋆ * (w * (x ⋆ y) * z)"
    using sup.boundedI sup.cobounded1 while_def while_increasing by auto
  finally show "w * (x ⋆ y * z) ≤ (w * (x ⋆ y)) ⋆ (w * (x ⋆ y) * z)"
    using while_def by auto
qed

subclass extended_binary_itering_apx
  apply unfold_locales
  by (metis n_below_n_omega n_left_upper_bound n_n_L order_trans while_def)

lemma while_simulate_4_plus:
  assumes "y * x ≤ x * (x ⋆ (1 ⊔ y))"
    shows "y * x * x⋆ ≤ x * (x ⋆ (1 ⊔ y))"
proof -
  have "x * (x ⋆ (1 ⊔ y)) = x * n(xω) * L ⊔ x * x⋆ * (1 ⊔ y)"
    by (simp add: mult_left_dist_sup while_def mult_assoc)
  also have "... = n(x * xω) * L ⊔ x * x⋆ * (1 ⊔ y)"
    by (smt n_mult_omega_L_star_zero sup_relative_same_increasing sup_commute sup_bot_right mult_left_sub_dist_sup_right)
  finally have 1: "x * (x ⋆ (1 ⊔ y)) = n(xω) * L ⊔ x * x⋆ ⊔ x * x⋆ * y"
    using mult_left_dist_sup omega_unfold sup_assoc by force
  hence "x * x⋆ * y * x ≤ x * x⋆ * n(xω) * L ⊔ x * x⋆ * x⋆ * x ⊔ x * x⋆ * x * x⋆ * y"
    by (metis assms mult_assoc mult_right_isotone mult_left_dist_sup star_plus)
  also have "... = n(x * x⋆ * xω) * L ⊔ x * x⋆ * x⋆ * x ⊔ x * x⋆ * x * x⋆ * y"
    by (smt (z3) sup_commute n_mult_omega_L_star omega_unfold semiring.distrib_left star_plus mult_assoc)
  also have "... = n(xω) * L ⊔ x * x⋆ * x ⊔ x * x * x⋆ * y"
    using omega_unfold star.circ_plus_same star.circ_transitive_equal star_mult_omega mult_assoc by auto
  also have "... ≤ n(xω) * L ⊔ x * x⋆ ⊔ x * x⋆ * y"
    by (smt sup_assoc sup_ge2 le_iff_sup mult_assoc mult_right_dist_sup star.circ_increasing star.circ_plus_same star.circ_transitive_equal)
  finally have 2: "x * x⋆ * y * x ≤ n(xω) * L ⊔ x * x⋆ ⊔ x * x⋆ * y"
    .
  have "(n(xω) * L ⊔ x * x⋆ ⊔ x * x⋆ * y) * x ≤ n(xω) * L ⊔ x * x⋆ * x ⊔ x * x⋆ * y * x"
    by (metis mult_right_dist_sup n_L_below_L mult_assoc mult_right_isotone sup_left_isotone)
  also have "... ≤ n(xω) * L ⊔ x * x⋆ ⊔ x * x⋆ * y * x"
    by (smt sup_commute sup_left_isotone mult_assoc mult_right_isotone star.left_plus_below_circ star_plus)
  also have "... ≤ n(xω) * L ⊔ x * x⋆ ⊔ x * x⋆ * y"
    using 2 by simp
  finally show ?thesis
    using 1 assms star_right_induct by force
qed

lemma while_simulate_4_omega:
  assumes "y * x ≤ x * (x ⋆ (1 ⊔ y))"
    shows "y * xω ≤ xω"
proof -
  have "x * (x ⋆ (1 ⊔ y)) = x * n(xω) * L ⊔ x * x⋆ * (1 ⊔ y)"
    using mult_left_dist_sup while_def mult_assoc by auto
  also have "... = n(x * xω) * L ⊔ x * x⋆ * (1 ⊔ y)"
    by (smt (z3) mult_1_right mult_left_sub_dist_sup_left n_mult_omega_L_star sup_commute sup_relative_same_increasing)
  finally have "x * (x ⋆ (1 ⊔ y)) = n(xω) * L ⊔ x * x⋆ ⊔ x * x⋆ * y"
    using mult_left_dist_sup omega_unfold sup_assoc by force
  hence "y * xω ≤ n(xω) * L * xω ⊔ x * x⋆ * xω ⊔ x * x⋆ * y * xω"
    by (smt assms le_iff_sup mult_assoc mult_right_dist_sup omega_unfold)
  also have "... ≤ x * x⋆ * (y * xω) ⊔ xω"
    by (metis sup_left_isotone mult_L_omega omega_sub_vector mult_assoc omega_unfold star_mult_omega n_L_decreasing le_iff_sup sup_commute)
  finally have "y * xω ≤ (x * x⋆)ω ⊔ (x * x⋆)⋆ * xω"
    by (simp add: omega_induct sup_monoid.add_commute)
  thus ?thesis
    by (metis sup_idem left_plus_omega star_mult_omega)
qed

lemma while_square_1:
  "x ⋆ 1 = (x * x) ⋆ (x ⊔ 1)"
  by (metis mult_1_right omega_square star_square_2 while_def)

lemma while_absorb_below_one:
  "y * x ≤ x ⟹ y ⋆ x ≤ 1 ⋆ x"
  by (metis star_left_induct_mult sup_mono n_galois n_sub_nL while_def while_one_top)

lemma while_mult_L:
  "(x * L) ⋆ z = z ⊔ x * L"
  by (metis sup_bot_right mult_left_zero while_denest_5 while_one_top while_productstar while_sumstar)

lemma tarski_top_omega_below_2:
  "x * L ≤ (x * L) ⋆ bot"
  by (simp add: while_mult_L)

lemma tarski_top_omega_2:
  "x * L = (x * L) ⋆ bot"
  by (simp add: while_mult_L)

proposition while_sub_mult_one: "x * (1 ⋆ y) ≤ 1 ⋆ x" nitpick [expect=genuine,card=3] oops
proposition while_unfold_below: "x = z ⊔ y * x ⟶ x ≤ y ⋆ z" nitpick [expect=genuine,card=2] oops
proposition while_loop_is_greatest_postfixpoint: "is_greatest_postfixpoint (λx . y * x ⊔ z) (y ⋆ z)" nitpick [expect=genuine,card=2] oops
proposition while_loop_is_greatest_fixpoint: "is_greatest_fixpoint (λx . y * x ⊔ z) (y ⋆ z)" nitpick [expect=genuine,card=2] oops
proposition while_denest_3: "(x ⋆ w) ⋆ xω = (x ⋆ w)ω" nitpick [expect=genuine,card=2] oops
proposition while_mult_top: "(x * top) ⋆ z = z ⊔ x * top" nitpick [expect=genuine,card=2] oops
proposition tarski_below_top_omega: "x ≤ (x * L)ω" nitpick [expect=genuine,card=2] oops
proposition tarski_mult_omega_omega: "(x * yω)ω = x * yω" nitpick [expect=genuine,card=3] oops
proposition tarski_below_top_omega_2: "x ≤ (x * L) ⋆ bot" nitpick [expect=genuine,card=2] oops
proposition "1 = (x * bot) ⋆ 1" nitpick [expect=genuine,card=3] oops
proposition tarski: "x = bot ∨ top * x * top = top" nitpick [expect=genuine,card=3] oops
proposition "(x ⊔ y) ⋆ z = ((x ⋆ 1) * y) ⋆ ((x ⋆ 1) * z)" nitpick [expect=genuine,card=2] oops
proposition while_top_2: "top ⋆ z = top * z" nitpick [expect=genuine,card=2] oops
proposition while_mult_top_2: "(x * top) ⋆ z = z ⊔ x * top * z" nitpick [expect=genuine,card=2] oops
proposition while_one_mult: "(x ⋆ 1) * x = x ⋆ x" nitpick [expect=genuine,card=4] oops
proposition "(x ⋆ 1) * y = x ⋆ y" nitpick [expect=genuine,card=2] oops
proposition while_associative: "(x ⋆ y) * z = x ⋆ (y * z)" nitpick [expect=genuine,card=2] oops
proposition while_back_loop_is_fixpoint: "is_fixpoint (λx . x * y ⊔ z) (z * (y ⋆ 1))" nitpick [expect=genuine,card=4] oops
proposition "1 ⊔ x * bot = x ⋆ 1" nitpick [expect=genuine,card=3] oops
proposition "x = x * (x ⋆ 1)" nitpick [expect=genuine,card=3] oops
proposition "x * (x ⋆ 1) = x ⋆ 1" nitpick [expect=genuine,card=2] oops
proposition "x ⋆ 1 = x ⋆ (1 ⋆ 1)" nitpick [expect=genuine,card=3] oops
proposition "(x ⊔ y) ⋆ 1 = (x ⋆ (y ⋆ 1)) ⋆ 1" nitpick [expect=genuine,card=3] oops
proposition "z ⊔ y * x = x ⟹ y ⋆ z ≤ x" nitpick [expect=genuine,card=2] oops
proposition "y * x = x ⟹ y ⋆ x ≤ x" nitpick [expect=genuine,card=2] oops
proposition "z ⊔ x * y = x ⟹ z * (y ⋆ 1) ≤ x" nitpick [expect=genuine,card=3] oops
proposition "x * y = x ⟹ x * (y ⋆ 1) ≤ x" nitpick [expect=genuine,card=3] oops
proposition "x * z = z * y ⟹ x ⋆ z ≤ z * (y ⋆ 1)" nitpick [expect=genuine,card=2] oops

proposition while_unfold_below_1: "x = y * x ⟹ x ≤ y ⋆ 1" nitpick [expect=genuine,card=3] oops
proposition "xω ≤ xω * xω" oops
proposition tarski_omega_idempotent: "xωω = xω" oops

end

class n_omega_algebra_binary_strict = n_omega_algebra_binary + circ +
  assumes L_left_zero: "L * x = L"
  assumes circ_def: "x∘ = n(xω) * L ⊔ x⋆"
begin

subclass strict_binary_itering
  apply unfold_locales
  apply (metis while_def mult_assoc L_left_zero mult_right_dist_sup)
  by (metis circ_def while_def mult_1_right)

end

end