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