Theory Binary_Iterings_Nonstrict

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

section ‹Nonstrict Binary Iterings›

theory Binary_Iterings_Nonstrict

imports Omega_Algebras Binary_Iterings

begin

class nonstrict_itering = bounded_left_zero_omega_algebra + while +
  assumes while_def: "x ⋆ y = x⇧^ω ⊔ x⇧^⋆ * y"
begin

text ‹Theorem 8.2›

subclass bounded_binary_itering
proof (unfold_locales)
  fix x y z
  show "(x * y) ⋆ z = z ⊔ x * ((y * x) ⋆ (y * z))"
    by (metis sup_commute mult_assoc mult_left_dist_sup omega_loop_fixpoint omega_slide star.circ_slide while_def)
next
  fix x y z
  show "(x ⊔ y) ⋆ z = (x ⋆ y) ⋆ (x ⋆ z)"
  proof -
    have 1: "(x ⊔ y) ⋆ z = (x⇧^⋆ * y)⇧^ω ⊔ (x⇧^⋆ * y)⇧^⋆ * (x⇧^ω ⊔ x⇧^⋆ * z)"
      using mult_left_dist_sup omega_decompose star.circ_sup_9 sup_assoc while_def mult_assoc by auto
    hence 2: "(x ⊔ y) ⋆ z ≤ (x ⋆ y) ⋆ (x ⋆ z)"
      by (smt (z3) sup_mono sup_ge2 le_iff_sup mult_left_isotone omega_sub_dist star.circ_sub_dist while_def)
    let ?rhs = "x⇧^⋆ * y * ((x⇧^ω ⊔ x⇧^⋆ * y)⇧^ω ⊔ (x⇧^ω ⊔ x⇧^⋆ * y)⇧^⋆ * (x⇧^ω ⊔ x⇧^⋆ * z)) ⊔ (x⇧^ω ⊔ x⇧^⋆ * z)"
    have "x⇧^ω * (x⇧^ω ⊔ x⇧^⋆ * y)⇧^ω ≤ x⇧^ω"
      by (simp add: omega_sub_vector)
    hence "x⇧^ω * (x⇧^ω ⊔ x⇧^⋆ * y)⇧^ω ⊔ x⇧^⋆ * y * (x⇧^ω ⊔ x⇧^⋆ * y)⇧^ω ≤ ?rhs"
      by (smt (z3) sup_commute sup_mono sup_ge1 mult_left_dist_sup order_trans)
    hence 3: "(x⇧^ω ⊔ x⇧^⋆ * y)⇧^ω ≤ ?rhs"
      by (metis mult_right_dist_sup omega_unfold)
    have "x⇧^ω * (x⇧^ω ⊔ x⇧^⋆ * y)⇧^⋆ * (x⇧^ω ⊔ x⇧^⋆ * z) ≤ x⇧^ω"
      by (simp add: omega_mult_star_2 omega_sub_vector)
    hence "x⇧^ω * (x⇧^ω ⊔ x⇧^⋆ * y)⇧^⋆ * (x⇧^ω ⊔ x⇧^⋆ * z) ⊔ x⇧^⋆ * y * (x⇧^ω ⊔ x⇧^⋆ * y)⇧^⋆ * (x⇧^ω ⊔ x⇧^⋆ * z) ≤ ?rhs"
      by (smt (z3) sup_commute sup_mono sup_ge2 mult_assoc mult_left_dist_sup order_trans)
    hence "(x⇧^ω ⊔ x⇧^⋆ * y)⇧^⋆ * (x⇧^ω ⊔ x⇧^⋆ * z) ≤ ?rhs"
      by (smt (z3) sup_assoc sup_ge2 le_iff_sup mult_assoc mult_right_dist_sup star.circ_loop_fixpoint)
    hence "(x⇧^ω ⊔ x⇧^⋆ * y)⇧^ω ⊔ (x⇧^ω ⊔ x⇧^⋆ * y)⇧^⋆ * (x⇧^ω ⊔ x⇧^⋆ * z) ≤ ?rhs"
      using 3 by simp
    hence "(x⇧^ω ⊔ x⇧^⋆ * y)⇧^ω ⊔ (x⇧^ω ⊔ x⇧^⋆ * y)⇧^⋆ * (x⇧^ω ⊔ x⇧^⋆ * z) ≤ (x⇧^⋆ * y)⇧^ω ⊔ (x⇧^⋆ * y)⇧^⋆ * (x⇧^ω ⊔ x⇧^⋆ * z)"
      by (metis sup_commute omega_induct)
    thus ?thesis
      using 1 2 order.antisym while_def by force
  qed
next
  fix x y z
  show "x ⋆ (y ⊔ z) = (x ⋆ y) ⊔ (x ⋆ z)"
    using mult_left_dist_sup sup_assoc sup_commute while_def by auto
next
  fix x y z
  show "(x ⋆ y) * z ≤ x ⋆ (y * z)"
    using mult_semi_associative omega_sub_vector semiring.add_mono semiring.distrib_right while_def by fastforce
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 "x * z ≤ z * (y ⋆ 1) ⊔ w"
    hence 1: "x * z ≤ z * y⇧^ω ⊔ z * y⇧^⋆ ⊔ w"
      by (metis mult_left_dist_sup mult_1_right while_def)
    let ?rhs = "z * (y⇧^ω ⊔ y⇧^⋆ * v) ⊔ x⇧^ω ⊔ x⇧^⋆ * w * (y⇧^ω ⊔ y⇧^⋆ * v)"
    have 2: "z * v ≤ ?rhs"
      by (metis le_supI1 mult_left_sub_dist_sup_right omega_loop_fixpoint)
    have "x * z * (y⇧^ω ⊔ y⇧^⋆ * v) ≤ ?rhs"
    proof -
      have "x * z * (y⇧^ω ⊔ y⇧^⋆ * v) ≤ (z * y⇧^ω ⊔ z * y⇧^⋆ ⊔ w) * (y⇧^ω ⊔ y⇧^⋆ * v)"
        using 1 mult_left_isotone by auto
      also have "... = z * (y⇧^ω * (y⇧^ω ⊔ y⇧^⋆ * v) ⊔ y⇧^⋆ * (y⇧^ω ⊔ y⇧^⋆ * v)) ⊔ w * (y⇧^ω ⊔ y⇧^⋆ * v)"
        by (smt (z3) mult_assoc mult_left_dist_sup mult_right_dist_sup)
      also have "... = z * (y⇧^ω * (y⇧^ω ⊔ y⇧^⋆ * v) ⊔ y⇧^ω ⊔ y⇧^⋆ * v) ⊔ w * (y⇧^ω ⊔ y⇧^⋆ * v)"
        by (smt (z3) sup_assoc mult_assoc mult_left_dist_sup star.circ_transitive_equal star_mult_omega)
      also have "... ≤ z * (y⇧^ω ⊔ y⇧^⋆ * v) ⊔ x⇧^⋆ * w * (y⇧^ω ⊔ y⇧^⋆ * v)"
        by (smt (z3) sup_commute sup_mono sup_left_top mult_left_dist_sup mult_left_one mult_right_dist_sup mult_right_sub_dist_sup_left omega_vector order_refl star.circ_plus_one)
      finally show ?thesis
        by (smt (z3) sup_assoc sup_commute le_iff_sup)
    qed
    hence "x * ?rhs ≤ ?rhs"
      by (smt (z3) sup_assoc sup_commute sup_ge1 le_iff_sup mult_assoc mult_left_dist_sup mult_right_dist_sup omega_unfold star.circ_increasing star.circ_transitive_equal)
    hence "z * v ⊔ x * ?rhs ≤ ?rhs"
      using 2 le_supI by blast
    hence "x⇧^⋆ * z * v ≤ ?rhs"
      by (simp add: star_left_induct mult_assoc)
    hence "x⇧^ω ⊔ x⇧^⋆ * z * v ≤ ?rhs"
      by (meson order_trans sup_ge1 sup_ge2 sup_least)
    thus "x ⋆ (z * v) ≤ z * (y ⋆ v) ⊔ (x ⋆ (w * (y ⋆ v)))"
      by (simp add: sup_assoc while_def mult_assoc)
  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 "z * x ≤ y * (y⇧^ω ⊔ y⇧^⋆ * z) ⊔ w"
      by (simp add: while_def)
    hence 1: "z * x ≤ y⇧^ω ⊔ y * y⇧^⋆ * z ⊔ w"
      using mult_left_dist_sup omega_unfold mult_assoc by auto
    let ?rhs = "y⇧^ω ⊔ y⇧^⋆ * z * v ⊔ y⇧^⋆ * w * (x⇧^ω ⊔ x⇧^⋆ * v)"
    have 2: "z * x⇧^ω ≤ ?rhs"
    proof -
      have "z * x⇧^ω ≤ y * y⇧^⋆ * z * x⇧^ω ⊔ y⇧^ω * x⇧^ω ⊔ w * x⇧^ω"
        using 1 by (smt (z3) sup_commute le_iff_sup mult_assoc mult_right_dist_sup omega_unfold)
      also have "... ≤ y * y⇧^⋆ * z * x⇧^ω ⊔ y⇧^ω ⊔ w * x⇧^ω"
        using omega_sub_vector semiring.add_mono by blast
      also have "... = y * y⇧^⋆ * (z * x⇧^ω) ⊔ (y⇧^ω ⊔ w * x⇧^ω)"
        by (simp add: sup_assoc mult_assoc)
      finally have "z * x⇧^ω ≤ (y * y⇧^⋆)⇧^ω ⊔ (y * y⇧^⋆)⇧^⋆ * (y⇧^ω ⊔ w * x⇧^ω)"
        by (simp add: omega_induct sup_commute)
      also have "... = y⇧^ω ⊔ y⇧^⋆ * w * x⇧^ω"
        by (simp add: left_plus_omega semiring.distrib_left star.left_plus_circ star_mult_omega mult_assoc)
      also have "... ≤ ?rhs"
        using mult_left_sub_dist_sup_left sup.mono sup_ge1 by blast
      finally show ?thesis
        .
    qed
    let ?rhs2 = "y⇧^ω ⊔ y⇧^⋆ * z ⊔ y⇧^⋆ * w * (x⇧^ω ⊔ x⇧^⋆)"
    have "?rhs2 * x ≤ ?rhs2"
    proof -
      have 3: "y⇧^ω * x ≤ ?rhs2"
        by (simp add: le_supI1 omega_sub_vector)
      have "y⇧^⋆ * z * x ≤ y⇧^⋆ * (y⇧^ω ⊔ y * y⇧^⋆ * z ⊔ w)"
        using 1 mult_right_isotone mult_assoc by auto
      also have "... = y⇧^ω ⊔ y⇧^⋆ * y * y⇧^⋆ * z ⊔ y⇧^⋆ * w"
        by (simp add: semiring.distrib_left star_mult_omega mult_assoc)
      also have "... = y⇧^ω ⊔ y * y⇧^⋆ * z ⊔ y⇧^⋆ * w"
        by (simp add: star.circ_plus_same star.circ_transitive_equal mult_assoc)
      also have "... ≤ y⇧^ω ⊔ y⇧^⋆ * z ⊔ y⇧^⋆ * w"
        by (metis sup_left_isotone sup_right_isotone mult_left_isotone star.left_plus_below_circ)
      also have "... ≤ y⇧^ω ⊔ y⇧^⋆ * z ⊔ y⇧^⋆ * w * x⇧^⋆"
        using semiring.add_left_mono star.circ_back_loop_prefixpoint by auto
      finally have 4: "y⇧^⋆ * z * x ≤ ?rhs2"
        using mult_left_sub_dist_sup_right order_lesseq_imp semiring.add_left_mono by blast
      have "(x⇧^ω ⊔ x⇧^⋆) * x ≤ x⇧^ω ⊔ x⇧^⋆"
        using omega_sub_vector semiring.distrib_right star.left_plus_below_circ star_plus sup_mono by fastforce
      hence "y⇧^⋆ * w * (x⇧^ω ⊔ x⇧^⋆) * x ≤ ?rhs2"
        by (simp add: le_supI2 mult_right_isotone mult_assoc)
      thus ?thesis
        using 3 4 mult_right_dist_sup by force
    qed
    hence "z ⊔ ?rhs2 * x ≤ ?rhs2"
      by (metis omega_loop_fixpoint sup.boundedE sup_ge1 sup_least)
    hence 5: "z * x⇧^⋆ ≤ ?rhs2"
      using star_right_induct by blast
    have "z * x⇧^⋆ * v ≤ ?rhs"
    proof -
      have "z * x⇧^⋆ * v ≤ ?rhs2 * v"
        using 5 mult_left_isotone by auto
      also have "... = y⇧^ω * v ⊔ y⇧^⋆ * z * v ⊔ y⇧^⋆ * w * (x⇧^ω * v ⊔ x⇧^⋆ * v)"
        using mult_right_dist_sup mult_assoc by auto
      also have "... ≤ y⇧^ω ⊔ y⇧^⋆ * z * v ⊔ y⇧^⋆ * w * (x⇧^ω * v ⊔ x⇧^⋆ * v)"
        using omega_sub_vector semiring.add_right_mono by blast
      also have "... ≤ ?rhs"
        using mult_right_isotone omega_sub_vector semiring.add_left_mono semiring.add_right_mono by auto
      finally show ?thesis
        .
    qed
    hence "z * (x⇧^ω ⊔ x⇧^⋆ * v) ≤ ?rhs"
      using 2 semiring.distrib_left mult_assoc by force
    thus "z * (x ⋆ v) ≤ y ⋆ (z * v ⊔ w * (x ⋆ v))"
      by (simp add: semiring.distrib_left sup_assoc while_def mult_assoc)
  qed
qed

text ‹Theorem 13.8›

lemma while_top:
  "top ⋆ x = top"
  by (metis sup_left_top star.circ_top star_omega_top while_def)

text ‹Theorem 13.7›

lemma while_one_top:
  "1 ⋆ x = top"
  by (simp add: omega_one while_def)

lemma while_finite_associative:
  "x⇧^ω = bot ⟹ (x ⋆ y) * z = x ⋆ (y * z)"
  by (simp add: while_def mult_assoc)

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

text ‹Theorem 13.9›

lemma while_sub_mult_one:
  "x * (1 ⋆ y) ≤ 1 ⋆ x"
  by (simp add: omega_one while_def)

lemma while_while_one:
  "y ⋆ (x ⋆ 1) = y⇧^ω ⊔ y⇧^⋆ * x⇧^ω ⊔ y⇧^⋆ * x⇧^⋆"
  using mult_left_dist_sup sup_assoc while_def by auto

lemma while_simulate_4_plus:
  assumes "y * x ≤ x * (x ⋆ (1 ⊔ y))"
    shows "y * x * x⇧^⋆ ≤ x * (x ⋆ (1 ⊔ y))"
proof -
  have 1: "x * (x ⋆ (1 ⊔ y)) = x⇧^ω ⊔ x * x⇧^⋆ ⊔ x * x⇧^⋆ * y"
    using mult_left_dist_sup omega_unfold sup_assoc while_def mult_assoc by force
  hence "y * x * x⇧^⋆ ≤ (x⇧^ω ⊔ x * x⇧^⋆ ⊔ x * x⇧^⋆ * y) * x⇧^⋆"
    using assms mult_left_isotone by auto
  also have "... = x⇧^ω * x⇧^⋆ ⊔ x * x⇧^⋆ * x⇧^⋆ ⊔ x * x⇧^⋆ * y * x⇧^⋆"
    using mult_right_dist_sup by force
  also have "... = x * x⇧^⋆ * (y * x * x⇧^⋆) ⊔ x⇧^ω ⊔ x * x⇧^⋆ ⊔ x * x⇧^⋆ * y"
    by (smt (z3) sup_assoc sup_commute mult_assoc omega_mult_star_2 star.circ_back_loop_fixpoint star.circ_plus_same star.circ_transitive_equal)
  finally have "y * x * x⇧^⋆ ≤ x * x⇧^⋆ * (y * x * x⇧^⋆) ⊔ (x⇧^ω ⊔ x * x⇧^⋆ ⊔ x * x⇧^⋆ * y)"
    using sup_assoc by force
  hence "y * x * x⇧^⋆ ≤ (x * x⇧^⋆)⇧^ω ⊔ (x * x⇧^⋆)⇧^⋆ * (x⇧^ω ⊔ x * x⇧^⋆ ⊔ x * x⇧^⋆ * y)"
    by (simp add: omega_induct sup_monoid.add_commute)
  also have "... = x⇧^ω ⊔ x⇧^⋆ * (x⇧^ω ⊔ x * x⇧^⋆ ⊔ x * x⇧^⋆ * y)"
    by (simp add: left_plus_omega star.left_plus_circ)
  finally show ?thesis
    using 1 by (metis while_def while_mult_star_exchange while_transitive)
qed

lemma while_simulate_4_omega:
  assumes "y * x ≤ x * (x ⋆ (1 ⊔ y))"
    shows "y * x⇧^ω ≤ x⇧^ω"
proof -
  have "x * (x ⋆ (1 ⊔ y)) = x⇧^ω ⊔ x * x⇧^⋆ ⊔ x * x⇧^⋆ * y"
    using mult_1_right mult_left_dist_sup omega_unfold sup_assoc while_def mult_assoc by auto
  hence "y * x⇧^ω ≤ (x⇧^ω ⊔ x * x⇧^⋆ ⊔ x * x⇧^⋆ * y) * x⇧^ω"
    by (smt (z3) assms le_iff_sup mult_assoc mult_right_dist_sup omega_unfold)
  also have "... = x⇧^ω * x⇧^ω ⊔ x * x⇧^⋆ * x⇧^ω ⊔ x * x⇧^⋆ * y * x⇧^ω"
    using semiring.distrib_right by auto
  also have "... = x * x⇧^⋆ * (y * x⇧^ω) ⊔ x⇧^ω"
    by (metis sup_commute le_iff_sup mult_assoc omega_sub_vector omega_unfold star_mult_omega)
  finally have "y * x⇧^ω ≤ x * x⇧^⋆ * (y * x⇧^ω) ⊔ x⇧^ω"
    .
  hence "y * x⇧^ω ≤ (x * x⇧^⋆)⇧^ω ⊔ (x * x⇧^⋆)⇧^⋆ * x⇧^ω"
    by (simp add: omega_induct sup_commute)
  thus ?thesis
    by (metis sup_idem left_plus_omega star_mult_omega)
qed

text ‹Theorem 13.11›

lemma while_unfold_below:
  "x = z ⊔ y * x ⟹ x ≤ y ⋆ z"
  by (simp add: omega_induct while_def)

text ‹Theorem 13.12›

lemma while_unfold_below_sub:
  "x ≤ z ⊔ y * x ⟹ x ≤ y ⋆ z"
  by (simp add: omega_induct while_def)

text ‹Theorem 13.10›

lemma while_unfold_below_1:
  "x = y * x ⟹ x ≤ y ⋆ 1"
  by (simp add: while_unfold_below_sub)

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 (simp add: while_unfold_below_sub)

lemma while_loop_is_greatest_postfixpoint:
  "is_greatest_postfixpoint (λx . y * x ⊔ z) (y ⋆ z)"
proof -
  have "(y ⋆ z) ≤ (λx . y * x ⊔ z) (y ⋆ z)"
    using sup_commute while_left_unfold by force
  thus ?thesis
    by (simp add: is_greatest_postfixpoint_def sup_commute while_unfold_below_sub)
qed

lemma while_loop_is_greatest_fixpoint:
  "is_greatest_fixpoint (λx . y * x ⊔ z) (y ⋆ z)"
  by (simp add: omega_loop_is_greatest_fixpoint while_def)

proposition while_sumstar_4_below: "(x ⋆ y) ⋆ ((x ⋆ 1) * z) ≤ x ⋆ ((y * (x ⋆ 1)) ⋆ z)" nitpick [expect=genuine,card=6] oops
proposition while_sumstar_2: "(x ⊔ y) ⋆ z = x ⋆ ((y * (x ⋆ 1)) ⋆ z)" nitpick [expect=genuine,card=6] 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)" nitpick [expect=genuine,card=6] 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 "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

proposition while_mult_sub_while_while: "x ⋆ (y * z) ≤ (x ⋆ y) ⋆ z" oops
proposition while_zero_zero: "(x ⋆ bot) ⋆ bot = x ⋆ bot" oops
proposition while_denest_3: "(x ⋆ w) ⋆ (x ⋆ bot) = (x ⋆ w) ⋆ bot" oops
proposition while_02: "x ⋆ ((x ⋆ w) ⋆ ((x ⋆ y) * z)) = (x ⋆ w) ⋆ ((x ⋆ y) * z)" oops
proposition while_sumstar_3_below: "(x ⋆ y) ⋆ (x ⋆ z) ≤ (x ⋆ y) ⋆ ((x ⋆ 1) * z)" oops
proposition while_sumstar_1: "(x ⊔ y) ⋆ z = (x ⋆ y) ⋆ ((x ⋆ 1) * z)" oops
proposition while_denest_4: "(x ⋆ w) ⋆ (x ⋆ (y * z)) = (x ⋆ w) ⋆ ((x ⋆ y) * z)" oops

end

class nonstrict_itering_zero = nonstrict_itering +
  assumes mult_right_zero: "x * bot = bot"
begin

lemma while_finite_associative_2:
  "x ⋆ bot = bot ⟹ (x ⋆ y) * z = x ⋆ (y * z)"
  by (metis sup_bot_left sup_bot_right mult_assoc mult_right_zero while_def)

text ‹Theorem 13 counterexamples›

proposition while_mult_top: "(x * top) ⋆ z = z ⊔ x * top" nitpick [expect=genuine,card=3] oops
proposition tarski_mult_top_idempotent: "x * top = x * top * x * top" nitpick [expect=genuine,card=3] oops

proposition while_denest_0: "w * (x ⋆ (y * z)) ≤ (w * (x ⋆ y)) ⋆ (w * (x ⋆ y) * z)" nitpick [expect=genuine,card=3] oops
proposition while_denest_1: "w * (x ⋆ (y * z)) ≤ (w * (x ⋆ y)) ⋆ z" nitpick [expect=genuine,card=3] oops
proposition while_mult_zero_zero: "(x * (y ⋆ bot)) ⋆ bot = x * (y ⋆ bot)" nitpick [expect=genuine,card=3] oops
proposition while_denest_2: "w * ((x ⋆ (y * w)) ⋆ z) = w * (((x ⋆ y) * w) ⋆ z)" nitpick [expect=genuine,card=3] oops
proposition while_denest_5: "w * ((x ⋆ (y * w)) ⋆ (x ⋆ (y * z))) = w * (((x ⋆ y) * w) ⋆ ((x ⋆ y) * z))" nitpick [expect=genuine,card=3] oops
proposition while_denest_6: "(w * (x ⋆ y)) ⋆ z = z ⊔ w * ((x ⊔ y * w) ⋆ (y * z))" nitpick [expect=genuine,card=3] oops
proposition while_sum_below_one: "y * ((x ⊔ y) ⋆ z) ≤ (y * (x ⋆ 1)) ⋆ z" nitpick [expect=genuine,card=3] oops
proposition while_separate_unfold: "(y * (x ⋆ 1)) ⋆ z = (y ⋆ z) ⊔ (y ⋆ (y * x * (x ⋆ ((y * (x ⋆ 1)) ⋆ z))))" nitpick [expect=genuine,card=3] oops

proposition while_sub_while_zero: "x ⋆ z ≤ (x ⋆ y) ⋆ z" nitpick [expect=genuine,card=4] oops
proposition while_while_sub_associative: "x ⋆ (y ⋆ z) ≤ (x ⋆ y) ⋆ z" nitpick [expect=genuine,card=4] oops
proposition tarski: "x ≤ x * top * x * top" nitpick [expect=genuine,card=3] oops
proposition tarski_top_omega_below: "x * top ≤ (x * top)⇧^ω" nitpick [expect=genuine,card=3] oops
proposition tarski_top_omega: "x * top = (x * top)⇧^ω" nitpick [expect=genuine,card=3] oops
proposition tarski_below_top_omega: "x ≤ (x * top)⇧^ω" nitpick [expect=genuine,card=3] oops
proposition tarski_mult_omega_omega: "(x * y⇧^ω)⇧^ω = x * y⇧^ω" nitpick [expect=genuine,card=3] oops
proposition tarski_mult_omega_omega: "(∀z . z⇧^ω⇧^ω = z⇧^ω) ⟹ (x * y⇧^ω)⇧^ω = x * y⇧^ω" nitpick [expect=genuine,card=3] oops
proposition tarski: "x = bot ∨ top * x * top = top" nitpick [expect=genuine,card=3] oops

end

class nonstrict_itering_tarski = nonstrict_itering +
  assumes tarski: "x ≤ x * top * x * top"
begin

text ‹Theorem 13.14›

lemma tarski_mult_top_idempotent:
  "x * top = x * top * x * top"
  by (metis sup_commute le_iff_sup mult_assoc star.circ_back_loop_fixpoint star.circ_left_top tarski top_mult_top)

lemma tarski_top_omega_below:
  "x * top ≤ (x * top)⇧^ω"
  using omega_induct_mult order.refl mult_assoc tarski_mult_top_idempotent by auto

lemma tarski_top_omega:
  "x * top = (x * top)⇧^ω"
  by (simp add: order.eq_iff mult_top_omega tarski_top_omega_below)

lemma tarski_below_top_omega:
  "x ≤ (x * top)⇧^ω"
  using top_right_mult_increasing tarski_top_omega by auto

lemma tarski_mult_omega_omega:
  "(x * y⇧^ω)⇧^ω = x * y⇧^ω"
  by (metis mult_assoc omega_vector tarski_top_omega)

lemma tarski_omega_idempotent:
  "x⇧^ω⇧^ω = x⇧^ω"
  by (metis omega_vector tarski_top_omega)

lemma while_denest_2a:
  "w * ((x ⋆ (y * w)) ⋆ z) = w * (((x ⋆ y) * w) ⋆ z)"
proof -
  have "(x⇧^ω ⊔ x⇧^⋆ * y * w)⇧^ω = (x⇧^⋆ * y * w)⇧^⋆ * x⇧^ω * (((x⇧^⋆ * y * w)⇧^⋆ * x⇧^ω)⇧^ω ⊔ ((x⇧^⋆ * y * w)⇧^⋆ * x⇧^ω)⇧^⋆ * (x⇧^⋆ * y * w)⇧^ω) ⊔ (x⇧^⋆ * y * w)⇧^ω"
    by (metis sup_commute omega_decompose omega_loop_fixpoint)
  also have "... ≤ (x⇧^⋆ * y * w)⇧^⋆ * x⇧^ω ⊔ (x⇧^⋆ * y * w)⇧^ω"
    by (metis sup_left_isotone mult_assoc mult_right_isotone omega_sub_vector)
  finally have 1: "w * (x⇧^ω ⊔ x⇧^⋆ * y * w)⇧^ω ≤ (w * x⇧^⋆ * y)⇧^⋆ * w * x⇧^ω ⊔ (w * x⇧^⋆ * y)⇧^ω"
    by (smt (z3) sup_commute le_iff_sup mult_assoc mult_left_dist_sup while_def while_slide)
  have "(x⇧^ω ⊔ x⇧^⋆ * y * w)⇧^⋆ * z = (x⇧^⋆ * y * w)⇧^⋆ * x⇧^ω * ((x⇧^⋆ * y * w)⇧^⋆ * x⇧^ω)⇧^⋆ * (x⇧^⋆ * y * w)⇧^⋆ * z ⊔ (x⇧^⋆ * y * w)⇧^⋆ * z"
    by (smt (z3) sup_commute mult_assoc star.circ_sup star.circ_loop_fixpoint)
  also have "... ≤ (x⇧^⋆ * y * w)⇧^⋆ * x⇧^ω ⊔ (x⇧^⋆ * y * w)⇧^⋆ * z"
    by (smt (z3) sup_commute sup_right_isotone mult_assoc mult_right_isotone omega_sub_vector)
  finally have "w * (x⇧^ω ⊔ x⇧^⋆ * y * w)⇧^⋆ * z ≤ (w * x⇧^⋆ * y)⇧^⋆ * w * x⇧^ω ⊔ (w * x⇧^⋆ * y)⇧^⋆ * w * z"
    by (metis mult_assoc mult_left_dist_sup mult_right_isotone star.circ_slide)
  hence "w * (x⇧^ω ⊔ x⇧^⋆ * y * w)⇧^ω ⊔ w * (x⇧^ω ⊔ x⇧^⋆ * y * w)⇧^⋆ * z ≤ (w * x⇧^⋆ * y)⇧^⋆ * (w * x⇧^ω)⇧^ω ⊔ (w * x⇧^⋆ * y)⇧^ω ⊔ (w * x⇧^⋆ * y)⇧^⋆ * w * z"
    using 1 by (smt (z3) sup_assoc sup_commute le_iff_sup mult_assoc tarski_mult_omega_omega)
  also have "... ≤ (w * x⇧^ω ⊔ w * x⇧^⋆ * y)⇧^⋆ * (w * x⇧^ω ⊔ w * x⇧^⋆ * y)⇧^ω ⊔ (w * x⇧^ω ⊔ w * x⇧^⋆ * y)⇧^ω ⊔ (w * x⇧^ω ⊔ w * x⇧^⋆ * y)⇧^⋆ * w * z"
    by (metis sup_mono sup_ge1 sup_ge2 mult_isotone mult_left_isotone omega_isotone star.circ_isotone)
  also have "... = (w * x⇧^ω ⊔ w * x⇧^⋆ * y)⇧^ω ⊔ (w * x⇧^ω ⊔ w * x⇧^⋆ * y)⇧^⋆ * w * z"
    by (simp add: star_mult_omega)
  finally have "w * ((x⇧^ω ⊔ x⇧^⋆ * y * w)⇧^ω ⊔ (x⇧^ω ⊔ x⇧^⋆ * y * w)⇧^⋆ * z) ≤ w * ((x⇧^ω ⊔ x⇧^⋆ * y) * w)⇧^ω ⊔ w * ((x⇧^ω ⊔ x⇧^⋆ * y) * w)⇧^⋆ * z"
    by (smt (z3) mult_assoc mult_left_dist_sup omega_slide star.circ_slide)
  hence 2: "w * ((x ⋆ (y * w)) ⋆ z) ≤ w * (((x ⋆ y) * w) ⋆ z)"
    by (simp add: mult_left_dist_sup while_def mult_assoc)
  have "w * (((x ⋆ y) * w) ⋆ z) ≤ w * ((x ⋆ (y * w)) ⋆ z)"
    by (simp add: mult_right_isotone while_left_isotone while_sub_associative)
  thus ?thesis
    using 2 order.antisym by auto
qed

lemma while_denest_3:
  "(x ⋆ w) ⋆ x⇧^ω = (x ⋆ w)⇧^ω"
proof -
  have 1: "(x ⋆ w) ⋆ x⇧^ω = (x ⋆ w)⇧^ω ⊔ (x ⋆ w)⇧^⋆ * x⇧^ω⇧^ω"
    by (simp add: while_def tarski_omega_idempotent)
  also have "... ≤ (x ⋆ w)⇧^ω ⊔ (x ⋆ w)⇧^⋆ * (x⇧^ω ⊔ x⇧^⋆ * w)⇧^ω"
    using mult_right_isotone omega_sub_dist semiring.add_left_mono by blast
  also have "... = (x ⋆ w)⇧^ω"
    by (simp add: star_mult_omega while_def)
  finally show ?thesis
    using 1 by (simp add: sup.order_iff)
qed

lemma while_denest_4a:
  "(x ⋆ w) ⋆ (x ⋆ (y * z)) = (x ⋆ w) ⋆ ((x ⋆ y) * z)"
proof -
  have "(x ⋆ w) ⋆ (x ⋆ (y * z)) = (x ⋆ w)⇧^ω ⊔ ((x ⋆ w) ⋆ (x⇧^⋆ * y * z))"
    using while_def while_denest_3 while_left_dist_sup mult_assoc by auto
  also have "... ≤ (x ⋆ w)⇧^ω ⊔ ((x ⋆ w) ⋆ ((x ⋆ y) * z))"
    using mult_right_sub_dist_sup_right order.refl semiring.add_mono while_def while_right_isotone by auto
  finally have 1: "(x ⋆ w) ⋆ (x ⋆ (y * z)) ≤ (x ⋆ w) ⋆ ((x ⋆ y) * z)"
    by (simp add: while_def)
  have "(x ⋆ w) ⋆ ((x ⋆ y) * z) ≤ (x ⋆ w) ⋆ (x ⋆ (y * z))"
    by (simp add: while_right_isotone while_sub_associative)
  thus ?thesis
    using 1 order.antisym by auto
qed

text ‹Theorem 8.3›

subclass bounded_extended_binary_itering
  apply unfold_locales
  by (smt (z3) mult_assoc while_denest_2a while_denest_4a while_increasing while_slide)

text ‹Theorem 13.13›

lemma while_mult_top:
  "(x * top) ⋆ z = z ⊔ x * top"
proof -
  have 1: "z ⊔ x * top ≤ (x * top) ⋆ z"
    by (metis le_supI sup_ge1 while_def while_increasing tarski_top_omega)
  have "(x * top) ⋆ z = z ⊔ x * top * ((x * top) ⋆ z)"
    using while_left_unfold by auto
  also have "... ≤ z ⊔ x * top"
    using mult_right_isotone sup_right_isotone top_greatest mult_assoc by auto
  finally show ?thesis
    using 1 order.antisym by auto
qed

lemma tarski_top_omega_below_2:
  "x * top ≤ (x * top) ⋆ bot"
  by (simp add: while_mult_top)

lemma tarski_top_omega_2:
  "x * top = (x * top) ⋆ bot"
  by (simp add: while_mult_top)

lemma tarski_below_top_omega_2:
  "x ≤ (x * top) ⋆ bot"
  using top_right_mult_increasing tarski_top_omega_2 by auto

proposition "1 = (x * bot) ⋆ 1" nitpick [expect=genuine,card=3] oops

end

class nonstrict_itering_tarski_zero = nonstrict_itering_tarski + nonstrict_itering_zero
begin

lemma while_bot_1:
  "1 = (x * bot) ⋆ 1"
  by (simp add: mult_right_zero while_zero)

text ‹Theorem 13 counterexamples›

proposition while_associative: "(x ⋆ y) * z = x ⋆ (y * z)" nitpick [expect=genuine,card=2] oops
proposition "(x ⋆ 1) * y = x ⋆ y" nitpick [expect=genuine,card=2] oops
proposition while_one_mult: "(x ⋆ 1) * x = x ⋆ x" nitpick [expect=genuine,card=4] oops
proposition "(x ⊔ y) ⋆ z = ((x ⋆ 1) * y) ⋆ ((x ⋆ 1) * 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_top_2: "top ⋆ z = top * z" nitpick [expect=genuine,card=2] oops

proposition tarski: "x = bot ∨ top * x * top = top" nitpick [expect=genuine,card=3] 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 tarski: "x = bot ∨ top * x * top = top" nitpick [expect=genuine,card=3] oops
proposition tarski_case: assumes t1: "x = bot ⟶ P x" and t2: "top * x * top = top ⟶ P x" shows "P x" nitpick [expect=genuine,card=3] oops

end

end