# 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 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⇧ω"
hence "x⇧ω * (x⇧ω ⊔ x⇧⋆ * y)⇧ω ⊔ x⇧⋆ * y * (x⇧ω ⊔ x⇧⋆ * y)⇧ω ≤ ?rhs"
by (smt 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⇧ω"
hence "x⇧ω * (x⇧ω ⊔ x⇧⋆ * y)⇧⋆ * (x⇧ω ⊔ x⇧⋆ * z) ⊔ x⇧⋆ * y * (x⇧ω ⊔ x⇧⋆ * y)⇧⋆ * (x⇧ω ⊔ x⇧⋆ * z) ≤ ?rhs"
by (smt sup_commute sup_mono sup_ge2 mult_assoc mult_left_dist_sup order_trans)
hence "(x⇧ω ⊔ x⇧⋆ * y)⇧⋆ * (x⇧ω ⊔ x⇧⋆ * z) ≤ ?rhs"
by (smt 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 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 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 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 sup_assoc sup_commute le_iff_sup)
qed
hence "x * ?rhs ≤ ?rhs"
by (smt 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"
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"
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 sup_commute le_iff_sup mult_assoc mult_right_dist_sup omega_unfold)
also have "... ≤ y * y⇧⋆ * z * x⇧ω ⊔ y⇧ω ⊔ w * x⇧ω"
also have "... = y * y⇧⋆ * (z * x⇧ω) ⊔ (y⇧ω ⊔ w * x⇧ω)"
finally have "z * x⇧ω ≤ (y * y⇧⋆)⇧ω ⊔ (y * y⇧⋆)⇧⋆ * (y⇧ω ⊔ w * x⇧ω)"
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"
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⇧⋆"
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)"
also have "... ≤ ?rhs"
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"

lemma while_finite_associative:
"x⇧ω = bot ⟹ (x ⋆ y) * z = x ⋆ (y * z)"

lemma star_below_while:
"x⇧⋆ * y ≤ x ⋆ y"

text ‹Theorem 13.9›

lemma while_sub_mult_one:
"x * (1 ⋆ y) ≤ 1 ⋆ x"

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 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)"
also have "... = x⇧ω ⊔ x⇧⋆ * (x⇧ω ⊔ x * x⇧⋆ ⊔ x * x⇧⋆ * y)"
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 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⇧ω"
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"

text ‹Theorem 13.12›

lemma while_unfold_below_sub:
"x ≤ z ⊔ y * x ⟹ x ≤ y ⋆ z"

text ‹Theorem 13.10›

lemma while_unfold_below_1:
"x = y * x ⟹ x ≤ y ⋆ 1"

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"

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)"

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 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 sup_commute mult_assoc star.circ_sup star.circ_loop_fixpoint)
also have "... ≤ (x⇧⋆ * y * w)⇧⋆ * x⇧ω ⊔ (x⇧⋆ * y * w)⇧⋆ * z"
by (smt 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 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"
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 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⇧ω⇧ω"
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)⇧ω"
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)"
have "(x ⋆ w) ⋆ ((x ⋆ y) * z) ≤ (x ⋆ w) ⋆ (x ⋆ (y * z))"
thus ?thesis
using 1 order.antisym by auto
qed

text ‹Theorem 8.3›

subclass bounded_extended_binary_itering
apply unfold_locales
by (smt 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"

lemma tarski_top_omega_2:
"x * top = (x * top) ⋆ bot"

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"

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

```