Theory N_Omega_Algebras

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

section N-Omega-Algebras

theory N_Omega_Algebras

imports Omega_Algebras Recursion

begin

class itering_apx = bounded_itering + n_algebra_apx
begin

lemma circ_L:
  "L = L  1"
  by (metis sup_commute mult_top_circ n_L_top_L)

lemma C_circ_import:
  "C (x)  (C x)"
proof -
  have 1: "C x * x  (C x) * C x"
    using C_mult_propagate circ_simulate order.eq_iff by blast
  have "C (x) = C (1  x * x)"
    by (simp add: circ_left_unfold)
  also have "... = C 1  C (x * x)"
    by (simp add: inf_sup_distrib1)
  also have "...  1  C (x * x)"
    using sup_left_isotone by auto
  also have "... = 1  C x * x"
    by (simp add: n_L_T_meet_mult)
  also have "...  (C x)"
    using 1 by (meson circ_reflexive order.trans le_supI right_plus_below_circ)
  finally show ?thesis
    .
qed

text AACP Theorem 4.3 and Theorem 4.4

lemma circ_apx_isotone:
  assumes "x  y"
  shows "x  y"
proof -
  have 1: "x  y  L  C y  x  n(x) * top"
    using assms apx_def by auto
  have "C (y)  (C y)"
    by (simp add: C_circ_import)
  also have "...  x  x * n(x) * top"
    using 1 by (metis circ_isotone circ_left_top circ_unfold_sum mult_assoc)
  also have "...  x  (x * bot  n(x * x) * top)"
    using n_n_top_split_n_top sup_right_isotone by blast
  also have "...  x  (x * bot  n(x) * top)"
    using circ_plus_same left_plus_below_circ mult_left_isotone n_isotone sup_right_isotone by auto
  also have "... = x  n(x) * top"
    by (meson sup.left_idem sup_relative_same_increasing zero_right_mult_decreasing)
  finally have 2: "C (y)  x  n(x) * top"
    .
  have "x  y * L"
    using 1 by (metis circ_sup_1 circ_back_loop_fixpoint circ_isotone n_L_below_L le_iff_sup mult_assoc)
  also have "... = y  y * L"
    using circ_L mult_left_dist_sup sup_commute by auto
  also have "...  y  y * bot  L"
    using n_L_split_L semiring.add_left_mono sup_assoc by auto
  finally have "x  y  L"
    using sup.absorb1 zero_right_mult_decreasing by force
  thus "x  y"
    using 2 by (simp add: apx_def)
qed

end

class n_omega_algebra_1 = bounded_left_zero_omega_algebra + n_algebra_apx + Omega +
  assumes Omega_def: "xΩ = n(xω) * L  x"
begin

text AACP Theorem 8.13

lemma C_omega_export:
  "C (xω) = (C x)ω"
proof -
  have "C (xω) = C x * C (xω)"
    by (metis C_mult_propagate n_L_T_meet_mult omega_unfold)
  hence 1: "C (xω)  (C x)ω"
    using eq_refl omega_induct_mult by auto
  have "(C x)ω = C (x * (C x)ω)"
    using n_L_T_meet_mult omega_unfold by auto
  also have "...  C (xω)"
    by (metis calculation C_decreasing inf_le1 le_infI omega_induct_mult)
  finally show ?thesis
    using 1 order.antisym by blast
qed  

text AACP Theorem 8.2

lemma L_mult_star:
  "L * x = L"
  by (metis n_L_top_L star.circ_left_top mult_assoc)

text AACP Theorem 8.3

lemma mult_L_star:
  "(x * L) = 1  x * L"
  by (metis L_mult_star star.circ_mult_1 mult_assoc)

lemma mult_L_omega_below:
  "(x * L)ω  x * L"
  by (metis mult_right_isotone n_L_below_L omega_slide)

text AACP Theorem 8.5

lemma mult_L_sup_star:
  "(x * L  y) = y  y * x * L"
  using L_mult_star mult_1_right mult_left_dist_sup star_sup_1 sup_commute mult_L_star mult_assoc by auto

lemma mult_L_sup_omega_below:
  "(x * L  y)ω  yω  y * x * L"
proof -
  have "(x * L  y)ω  y * x * L  (y * x * L) * yω"
    by (metis sup_commute mult_assoc omega_decompose sup_left_isotone mult_L_omega_below)
  also have "...  yω  y * x * L"
    by (smt (z3) le_iff_sup le_supI mult_left_dist_sup n_L_below_L star_left_induct sup.cobounded2 sup.left_idem sup.orderE sup_assoc sup_commute mult_assoc)
  finally show ?thesis
    .
qed

lemma n_Omega_isotone:
  "x  y  xΩ  yΩ"
  by (metis Omega_def sup_mono mult_left_isotone n_isotone omega_isotone star_isotone)

lemma n_star_below_Omega:
  "x  xΩ"
  by (simp add: Omega_def)

lemma mult_L_star_mult_below:
  "(x * L) * y  y  x * L"
  by (metis sup_right_isotone mult_assoc mult_right_isotone n_L_below_L star_left_induct)

end

sublocale n_omega_algebra_1 < star: itering_apx where circ = star ..

class n_omega_algebra = n_omega_algebra_1 + n_algebra_apx +
  assumes n_split_omega_mult: "C (xω)  x * n(xω) * top"
  assumes tarski: "x * L  x * L * x * L"
begin

text AACP Theorem 8.4

lemma mult_L_omega:
  "(x * L)ω = x * L"
  apply (rule order.antisym)
  apply (rule mult_L_omega_below)
  using omega_induct_mult tarski mult_assoc by auto

text AACP Theorem 8.6

lemma mult_L_sup_omega:
  "(x * L  y)ω = yω  y * x * L"
  apply (rule order.antisym)
  apply (rule mult_L_sup_omega_below)
  by (metis le_supI omega_isotone omega_sub_dist_2 sup.cobounded2 sup_commute mult_L_omega mult_assoc)

text AACP Theorem 8.1

lemma tarski_mult_top_idempotent:
  "x * L = x * L * x * L"
  by (metis omega_unfold mult_L_omega mult_assoc)

text AACP Theorem 8.7

lemma n_below_n_omega:
  "n(x)  n(xω)"
proof -
  have "n(x) * L  n(x) * L * n(x) * L"
    by (simp add: tarski)
  also have "...  x * n(x) * L"
    by (simp add: mult_isotone n_L_decreasing)
  finally have "n(x) * L  xω"
    by (simp add: omega_induct_mult mult_assoc)
  thus ?thesis
    by (simp add: n_galois)
qed

text AACP Theorem 8.14

lemma n_split_omega_sup_zero:
  "C (xω)  x * bot  n(xω) * top"
proof -
  have "n(xω) * top  x * (x * bot  n(xω) * top) = n(xω) * top  x * x * bot  x * n(xω) * top"
    by (simp add: mult_left_dist_sup sup_assoc mult_assoc)
  also have "...  n(xω) * top  x * x * bot  x * bot  n(xω) * top"
    by (metis sup_assoc sup_right_isotone n_n_top_split_n_top omega_unfold)
  also have "... = x * x * bot  n(xω) * top"
    by (smt sup_assoc sup_commute sup_left_top sup_bot_right mult_assoc mult_left_dist_sup)
  also have "...  x * bot  n(xω) * top"
    by (metis sup_left_isotone mult_left_isotone star.left_plus_below_circ)
  finally have "x * n(xω) * top  x * bot  n(xω) * top"
    using star_left_induct mult_assoc by auto
  thus ?thesis
    using n_split_omega_mult order_trans by blast
qed

lemma n_split_omega_sup:
  "C (xω)  x  n(xω) * top"
  by (metis sup_left_isotone n_split_omega_sup_zero order_trans zero_right_mult_decreasing)

text AACP Theorem 8.12

lemma n_dist_omega_star:
  "n(yω  y * z) = n(yω)  n(y * z)"
proof -
  have "n(yω  y * z) = n(C (yω)  C (y * z))"
    by (metis inf_sup_distrib1 n_C)
  also have "...  n(C (yω)  y * z)"
    using n_isotone semiring.add_right_mono sup_commute by auto
  also have "...  n(y * bot  n(yω) * top  y * z)"
    using n_isotone semiring.add_right_mono n_split_omega_sup_zero by blast
  also have "... = n(yω)  n(y * z)"
    by (smt sup_assoc sup_commute sup_bot_right mult_left_dist_sup n_dist_n_add)
  finally show ?thesis
    by (simp add: order.antisym n_isotone)
qed

lemma mult_L_sup_circ_below:
  "(x * L  y)Ω  n(yω) * L  y  y * x * L"
proof -
  have "(x * L  y)Ω  n(yω  y * x * L) * L  (x * L  y)"
    by (simp add: Omega_def mult_L_sup_omega)
  also have "... = n(yω) * L  n(y * x * L) * L  (x * L  y)"
    by (simp add: semiring.distrib_right mult_assoc n_dist_omega_star)
  also have "...  n(yω) * L  y  y * x * L"
    by (smt (z3) le_supI sup.cobounded1 sup_assoc sup_commute sup_idem sup_right_isotone mult_L_sup_star n_L_decreasing)
  finally show ?thesis
    .
qed

lemma n_mult_omega_L_below_zero:
  "n(y * xω) * L  y * x * bot  y * n(xω) * L"
proof -
  have "n(y * xω) * L  C (y * xω)  L"
    by (metis n_C n_L_decreasing_meet_L)
  also have "...  y * C (xω)  L"
    using inf.sup_left_isotone n_L_T_meet_mult n_L_T_meet_mult_propagate by auto
  also have "...  y * (x * bot  n(xω) * top)  L"
    using inf.sup_left_isotone mult_right_isotone n_split_omega_sup_zero by auto
  also have "... = (y * x * bot  L)  (y * n(xω) * top  L)"
    using inf_sup_distrib2 mult_left_dist_sup mult_assoc by auto
  also have "...  (y * x * bot  L)  y * n(xω) * L"
    using n_vector_meet_L sup_right_isotone by auto
  also have "...  y * x * bot  y * n(xω) * L"
    using sup_left_isotone by auto
  finally show ?thesis
    .
qed

text AACP Theorem 8.10

lemma n_mult_omega_L_star_zero:
  "y * x * bot  n(y * xω) * L = y * x * bot  y * n(xω) * L"
  apply (rule order.antisym)
  apply (simp add: n_mult_omega_L_below_zero)
  by (smt sup_assoc sup_commute sup_bot_left sup_right_isotone mult_assoc mult_left_dist_sup n_n_L_split_n_L)

text AACP Theorem 8.11

lemma n_mult_omega_L_star:
  "y * x  n(y * xω) * L = y * x  y * n(xω) * L"
  by (metis zero_right_mult_decreasing n_mult_omega_L_star_zero sup_relative_same_increasing)

lemma n_mult_omega_L_below:
  "n(y * xω) * L  y * x  y * n(xω) * L"
  using sup_right_divisibility n_mult_omega_L_star by blast

lemma n_omega_L_below_zero:
  "n(xω) * L  x * x * bot  x * n(xω) * L"
  by (metis omega_unfold n_mult_omega_L_below_zero)

lemma n_omega_L_below:
  "n(xω) * L  x  x * n(xω) * L"
  by (metis omega_unfold n_mult_omega_L_below sup_left_isotone star.left_plus_below_circ order_trans)

lemma n_omega_L_star_zero:
  "x * x * bot  n(xω) * L = x * x * bot  x * n(xω) * L"
  by (metis n_mult_omega_L_star_zero omega_unfold)

text AACP Theorem 8.8

lemma n_omega_L_star:
  "x  n(xω) * L = x  x * n(xω) * L"
  by (metis star.circ_mult_upper_bound star.left_plus_below_circ bot_least n_omega_L_star_zero sup_relative_same_increasing)

text AACP Theorem 8.9

lemma n_omega_L_star_zero_star:
  "x * bot  n(xω) * L = x * bot  x * n(xω) * L"
  by (metis n_mult_omega_L_star_zero star_mult_omega mult_assoc star.circ_transitive_equal)

text AACP Theorem 8.8

lemma n_omega_L_star_star:
  "x  n(xω) * L = x  x * n(xω) * L"
  by (metis zero_right_mult_decreasing n_omega_L_star_zero_star sup_relative_same_increasing)

lemma n_Omega_left_unfold:
  "1  x * xΩ = xΩ"
  by (smt Omega_def sup_assoc sup_commute mult_assoc mult_left_dist_sup n_omega_L_star star.circ_left_unfold)

lemma n_Omega_left_slide:
  "(x * y)Ω * x  x * (y * x)Ω"
proof -
  have "(x * y)Ω * x  x * y * n((x * y)ω) * L  (x * y) * x"
    by (smt Omega_def sup_commute sup_left_isotone mult_assoc mult_right_dist_sup mult_right_isotone n_L_below_L n_omega_L_star)
  also have "...  x * (y * bot  n(y * (x * y)ω) * L)  (x * y) * x"
    by (metis mult_right_isotone n_n_L_split_n_L sup_commute sup_right_isotone mult_assoc)
  also have "... = x * (y * x)Ω"
    by (smt (verit, del_insts) le_supI1 star_slide Omega_def sup_assoc sup_commute le_iff_sup mult_assoc mult_isotone mult_left_dist_sup omega_slide star.circ_increasing star.circ_slide bot_least)
  finally show ?thesis
    .
qed

lemma n_Omega_sup_1:
  "(x  y)Ω = xΩ * (y * xΩ)Ω"
proof -
  have 1: "(x  y)Ω = n((x * y)ω) * L  n((x * y) * xω) * L  (x * y) * x"
    by (simp add: Omega_def omega_decompose semiring.distrib_right star.circ_sup_9 n_dist_omega_star)
  have "n((x * y)ω) * L  (x * y)  x * (y * n((x * y)ω) * L)"
    by (metis n_omega_L_below mult_assoc)
  also have "...  (x * y)  x * y * bot  x * n((y * x)ω) * L"
    by (smt sup_assoc sup_right_isotone mult_assoc mult_left_dist_sup mult_right_isotone n_n_L_split_n_L omega_slide)
  also have "... = (x * y)  x * n((y * x)ω) * L"
    by (metis sup_commute le_iff_sup star.circ_sub_dist_1 zero_right_mult_decreasing)
  also have "...  x * (y * x)  x * n((y * x)ω) * L"
    by (metis star_outer_increasing star_slide star_star_absorb sup_left_isotone)
  also have "...  x * (y * xΩ)Ω"
    by (metis Omega_def sup_commute mult_assoc mult_left_dist_sup mult_right_isotone n_Omega_isotone n_star_below_Omega)
  also have "...  xΩ * (y * xΩ)Ω"
    by (simp add: mult_left_isotone n_star_below_Omega)
  finally have 2: "n((x * y)ω) * L  xΩ * (y * xΩ)Ω"
    .
  have "n((x * y) * xω) * L  n(xω) * L  x * (y * x)  x * (y * x) * y * n(xω) * L"
    by (smt sup_assoc sup_commute mult_left_one mult_right_dist_sup n_mult_omega_L_below star.circ_mult star.circ_slide)
  also have "... = n(xω) * L * (y * xΩ)  x * (y * xΩ)"
    by (smt Omega_def sup_assoc mult_L_sup_star mult_assoc mult_left_dist_sup L_mult_star)
  also have "...  xΩ * (y * xΩ)Ω"
    by (simp add: Omega_def mult_isotone)
  finally have 3: "n((x * y) * xω) * L  xΩ * (y * xΩ)Ω"
    .
  have "(x * y) * x  xΩ * (y * xΩ)Ω"
    by (metis star_slide mult_isotone mult_right_isotone n_star_below_Omega order_trans star_isotone)
  hence 4: "(x  y)Ω  xΩ * (y * xΩ)Ω"
    using 1 2 3 by simp
  have 5: "xΩ * (y * xΩ)Ω  n(xω) * L  x * n((y * xΩ)ω) * L  x * (y * xΩ)"
    by (smt Omega_def sup_assoc sup_left_isotone mult_assoc mult_left_dist_sup mult_right_dist_sup mult_right_isotone n_L_below_L)
  have "n(xω) * L  n((x * y) * xω) * L"
    by (metis sup_commute sup_ge1 mult_left_isotone n_isotone star.circ_loop_fixpoint)
  hence 6: "n(xω) * L  (x  y)Ω"
    using 1 order_lesseq_imp by fastforce
  have "x * n((y * xΩ)ω) * L  x * n((y * x)ω  (y * x) * y * n(xω) * L) * L"
    by (metis Omega_def mult_L_sup_omega_below mult_assoc mult_left_dist_sup mult_left_isotone mult_right_isotone n_isotone)
  also have "...  x * bot  n(x * ((y * x)ω  (y * x) * y * n(xω) * L)) * L"
    by (simp add: n_n_L_split_n_L)
  also have "...  x  n((x * y)ω  x * (y * x) * y * n(xω) * L) * L"
    using omega_slide semiring.distrib_left sup_mono zero_right_mult_decreasing mult_assoc by fastforce
  also have "...  x  n((x * y)ω  (x * y) * n(xω) * L) * L"
    by (smt sup_right_divisibility sup_right_isotone mult_left_isotone n_isotone star.circ_mult)
  also have "...  x  n((x  y)ω) * L"
    by (metis sup_right_isotone mult_assoc mult_left_isotone mult_right_isotone n_L_decreasing n_isotone omega_decompose)
  also have "...  (x  y)Ω"
    by (simp add: Omega_def le_supI1 star_isotone sup_commute)
  finally have 7: "x * n((y * xΩ)ω) * L  (x  y)Ω"
    .
  have "x * (y * xΩ)  (x * y) * x  (x * y) * n(xω) * L"
    by (smt Omega_def sup_right_isotone mult_L_sup_star mult_assoc mult_left_dist_sup mult_left_isotone star.left_plus_below_circ star_slide)
  also have "...  (x * y) * x  n((x * y) * xω) * L"
    by (simp add: n_mult_omega_L_star)
  also have "...  (x  y)Ω"
    by (smt Omega_def sup_commute sup_right_isotone mult_left_isotone n_right_upper_bound omega_decompose star.circ_sup)
  finally have "n(xω) * L  x * n((y * xΩ)ω) * L  x * (y * xΩ)  (x  y)Ω"
    using 6 7 by simp
  hence "xΩ * (y * xΩ)Ω  (x  y)Ω"
    using 5 order.trans by blast
  thus ?thesis
    using 4 order.antisym by blast
qed

end

sublocale n_omega_algebra < nL_omega: left_zero_conway_semiring where circ = Omega
  apply unfold_locales
  apply (simp add: n_Omega_left_unfold)
  apply (simp add: n_Omega_left_slide)
  by (simp add: n_Omega_sup_1)

(* circ_plus_same does not hold in the non-strict model using Omega *)

context n_omega_algebra
begin

text AACP Theorem 8.16

lemma omega_apx_isotone:
  assumes "x  y"
    shows "xω  yω"
proof -
  have 1: "x  y  L  C y  x  n(x) * top"
    using assms apx_def by auto
  have "n(x) * top  x * (xω  n(xω) * top)  n(x) * top  xω  n(xω) * top"
    by (metis le_supI n_split_top sup.cobounded1 sup_assoc mult_assoc mult_left_dist_sup sup_right_isotone omega_unfold)
  also have "...  xω  n(xω) * top"
    by (metis sup_commute sup_right_isotone mult_left_isotone n_below_n_omega sup_assoc sup_idem)
  finally have 2: "x * n(x) * top  xω  n(xω) * top"
    using star_left_induct mult_assoc by auto
  have "C (yω) = (C y)ω"
    by (simp add: C_omega_export)
  also have "...  (x  n(x) * top)ω"
    using 1 omega_isotone by blast
  also have "... = (x * n(x) * top)ω  (x * n(x) * top) * xω"
    by (simp add: omega_decompose mult_assoc)
  also have "...  x * n(x) * top  (x * n(x) * top) * xω"
    using mult_top_omega sup_left_isotone by blast
  also have "... = x * n(x) * top  (1  x * n(x) * top * (x * n(x) * top)) * xω"
    by (simp add: star_left_unfold_equal)
  also have "...  xω  x * n(x) * top"
    by (smt sup_mono sup_least mult_assoc mult_left_one mult_right_dist_sup mult_right_isotone order_refl top_greatest sup.cobounded2)
  also have "...  xω  n(xω) * top"
    using 2 by simp
  finally have 3: "C (yω)  xω  n(xω) * top"
    .
  have "xω  (y  L)ω"
    using 1 omega_isotone by simp
  also have "... = (y * L)ω  (y * L) * yω"
    by (simp add: omega_decompose)
  also have "... = y * L * (y * L)ω  (y * L) * yω"
    using omega_unfold by auto
  also have "...  y * L  (y * L) * yω"
    by (metis sup_left_isotone n_L_below_L mult_assoc mult_right_isotone)
  also have "... = y * L  (1  y * L * (y * L)) * yω"
    by (simp add: star_left_unfold_equal)
  also have "...  y * L  yω"
    by (simp add: mult_L_star_mult_below star_left_unfold_equal sup_commute)
  also have "...  y * bot  L  yω"
    using n_L_split_L sup_left_isotone by auto
  finally have "xω  yω  L"
    by (simp add: star_bot_below_omega sup.absorb1 sup.left_commute sup_commute)
  thus "xω  yω"
    using 3 by (simp add: apx_def)
qed

lemma combined_apx_left_isotone:
  "x  y  n(xω) * L  x * z  n(yω) * L  y * z"
  by (simp add: mult_apx_isotone n_L_apx_isotone star.circ_apx_isotone sup_apx_isotone omega_apx_isotone)

lemma combined_apx_left_isotone_2:
  "x  y  (xω  L)  x * z  (yω  L)  y * z"
  by (metis sup_apx_isotone mult_apx_left_isotone omega_apx_isotone star.circ_apx_isotone meet_L_apx_isotone)

lemma combined_apx_right_isotone:
  "y  z  n(xω) * L  x * y  n(xω) * L  x * z"
  by (simp add: mult_apx_isotone sup_apx_left_isotone sup_commute)

lemma combined_apx_right_isotone_2:
  "y  z  (xω  L)  x * y  (xω  L)  x * z"
  by (simp add: mult_apx_right_isotone sup_apx_right_isotone)

lemma combined_apx_isotone:
  "x  y  w  z  n(xω) * L  x * w  n(yω) * L  y * z"
  by (simp add: mult_apx_isotone n_L_apx_isotone star.circ_apx_isotone sup_apx_isotone omega_apx_isotone)

lemma combined_apx_isotone_2:
  "x  y  w  z  (xω  L)  x * w  (yω  L)  y * z"
  by (meson combined_apx_left_isotone_2 combined_apx_right_isotone_2 apx.order.trans)

lemma n_split_nu_mu:
  "C (yω  y * z)  y * z  n(yω  y * z) * top"
proof -
  have "C (yω  y * z)  C (yω)  y * z"
    by (simp add: inf_sup_distrib1 le_supI1 sup_commute)
  also have "...  y * bot  n(yω) * top  y * z"
    using n_split_omega_sup_zero sup_left_isotone by blast
  also have "...  y * z  n(yω  y * z) * top"
    using le_supI1 mult_left_isotone mult_right_isotone n_left_upper_bound sup_right_isotone by force
  finally show ?thesis
    .
qed

lemma n_split_nu_mu_2:
  "C (yω  y * z)  y * z  ((yω  y * z)  L)  n(yω  y * z) * top"
proof -
  have "C (yω  y * z)  C (yω)  y * z"
    using inf.sup_left_isotone sup_inf_distrib2 by auto
  also have "...  y * bot  n(yω) * top  y * z"
    using n_split_omega_sup_zero sup_left_isotone by blast
  also have "...  y * z  n(yω  y * z) * top"
    using le_supI1 mult_left_isotone mult_right_isotone n_left_upper_bound semiring.add_left_mono by auto
  finally show ?thesis
    using order_lesseq_imp semiring.add_right_mono sup.cobounded1 by blast
qed

lemma loop_exists:
  "C (ν (λx . y * x  z))  μ (λx . y * x  z)  n(ν (λx . y * x  z)) * top"
  using omega_loop_nu star_loop_mu n_split_nu_mu by auto

lemma loop_exists_2:
  "C (ν (λx . y * x  z))  μ (λx . y * x  z)  (ν (λx . y * x  z)  L)  n(ν (λx . y * x  z)) * top"
  by (simp add: omega_loop_nu star_loop_mu n_split_nu_mu_2)

lemma loop_apx_least_fixpoint:
  "apx.is_least_fixpoint (λx . y * x  z) (μ (λx . y * x  z)  n(ν (λx . y * x  z)) * L)"
proof -
  have "kappa_mu_nu_L (λx . y * x  z)"
    by (metis affine_apx_isotone loop_exists affine_has_greatest_fixpoint affine_has_least_fixpoint affine_isotone nu_below_mu_nu_L_def nu_below_mu_nu_L_kappa_mu_nu_L)
  thus ?thesis
    using apx.least_fixpoint_char kappa_mu_nu_L_def by force
qed

lemma loop_apx_least_fixpoint_2:
  "apx.is_least_fixpoint (λx . y * x  z) (μ (λx . y * x  z)  (ν (λx . y * x  z)  L))"
proof -
  have "kappa_mu_nu (λx . y * x  z)"
    by (metis affine_apx_isotone affine_has_greatest_fixpoint affine_has_least_fixpoint affine_isotone loop_exists_2 nu_below_mu_nu_def nu_below_mu_nu_kappa_mu_nu)
  thus ?thesis
    using apx.least_fixpoint_char kappa_mu_nu_def by force
qed

lemma loop_has_apx_least_fixpoint:
  "apx.has_least_fixpoint (λx . y * x  z)"
  using apx.least_fixpoint_char loop_apx_least_fixpoint by blast

lemma loop_semantics:
  "κ (λx . y * x  z) = μ (λx . y * x  z)  n(ν (λx . y * x  z)) * L"
  using apx.least_fixpoint_char loop_apx_least_fixpoint by force

lemma loop_semantics_2:
  "κ (λx . y * x  z) = μ (λx . y * x  z)  (ν (λx . y * x  z)  L)"
  using apx.least_fixpoint_char loop_apx_least_fixpoint_2 by force

text AACP Theorem 8.15

lemma loop_semantics_kappa_mu_nu:
  "κ (λx . y * x  z) = n(yω) * L  y * z"
proof -
  have "κ (λx . y * x  z) = y * z  n(yω  y * z) * L"
    using apx.least_fixpoint_char omega_loop_nu star_loop_mu loop_apx_least_fixpoint by auto
  thus ?thesis
    by (smt n_dist_omega_star sup_assoc mult_right_dist_sup sup_commute le_iff_sup n_L_decreasing)
qed

text AACP Theorem 8.15

lemma loop_semantics_kappa_mu_nu_2:
  "κ (λx . y * x  z) = (yω  L)  y * z"
proof -
  have "κ (λx . y * x  z) = y * z  ((yω  y * z)  L)"
    using apx.least_fixpoint_char omega_loop_nu star_loop_mu loop_apx_least_fixpoint_2 by auto
  thus ?thesis
    by (metis sup_absorb2 sup_ge2 sup_inf_distrib1 sup_monoid.add_commute)
qed

text AACP Theorem 8.16

lemma loop_semantics_apx_left_isotone:
  "w  y  κ (λx . w * x  z)  κ (λx . y * x  z)"
  by (metis loop_semantics_kappa_mu_nu_2 combined_apx_left_isotone_2)

text AACP Theorem 8.16

lemma loop_semantics_apx_right_isotone:
  "w  z  κ (λx . y * x  w)  κ (λx . y * x  z)"
  by (metis loop_semantics_kappa_mu_nu_2 combined_apx_right_isotone_2)

lemma loop_semantics_apx_isotone:
  "v  y  w  z  κ (λx . v * x  w)  κ (λx . y * x  z)"
  using apx_transitive_2 loop_semantics_apx_left_isotone loop_semantics_apx_right_isotone by blast

end

end