Theory Domain_Iterings

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

section Domain Iterings

theory Domain_Iterings

imports Domain Lattice_Ordered_Semirings Omega_Algebras

begin

class domain_semiring_lattice = left_zero_domain_semiring + lattice_ordered_pre_left_semiring
begin

subclass bounded_idempotent_left_zero_semiring ..

lemma d_top:
  "d(top) = 1"
  by (metis sup_left_top d_dist_sup d_one d_plus_one)

lemma mult_domain_top:
  "x * d(y) * top  d(x * y) * top"
  by (smt d_mult_d d_restrict_equals mult_assoc mult_right_isotone top_greatest)

lemma domain_meet_domain:
  "d(x  d(y) * z)  d(y)"
  by (metis d_export d_isotone d_mult_greatest_lower_bound inf.cobounded2)

lemma meet_domain:
  "x  d(y) * z = d(y) * (x  z)"
  apply (rule order.antisym)
  apply (metis domain_meet_domain d_mult_below d_restrict_equals inf_mono mult_isotone)
  by (meson d_mult_below le_inf_iff mult_left_sub_dist_inf_right)

lemma meet_intro_domain:
  "x  y = d(y) * x  y"
  by (metis d_restrict_equals inf_commute meet_domain)

lemma meet_domain_top:
  "x  d(y) * top = d(y) * x"
  by (simp add: meet_domain)

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

lemma d_galois:
  "d(x)  d(y)  x  d(y) * top"
  by (metis d_export d_isotone d_mult_left_absorb_sup d_plus_one d_restrict_equals d_top mult_isotone top.extremum)

lemma vector_meet:
  "x * top  y  d(x) * y"
  by (metis d_galois d_mult_sub inf.sup_monoid.add_commute inf.sup_right_isotone meet_domain_top)

end

class domain_semiring_lattice_L = domain_semiring_lattice + L +
  assumes l1: "x * L = x * bot  d(x) * L"
  assumes l2: "d(L) * x  x * d(L)"
  assumes l3: "d(L) * top  L  d(L * bot) * top"
  assumes l4: "L * top  L"
  assumes l5: "x * bot  L  (x  L) * bot"
begin

lemma l8:
  "(x  L) * bot  x * bot  L"
  by (meson inf.boundedE inf.boundedI mult_right_sub_dist_inf_left zero_right_mult_decreasing)

lemma l9:
  "x * bot  L  d(x * bot) * L"
  by (metis vector_meet vector_mult_closed zero_vector)

lemma l10:
  "L * L = L"
  by (metis d_restrict_equals l1 le_iff_sup zero_right_mult_decreasing)

lemma l11:
  "d(x) * L  x * L"
  by (metis l1 sup.cobounded2)

lemma l12:
  "d(x * bot) * L  x * bot"
  by (metis sup_right_divisibility l1 mult_assoc mult_left_zero)

lemma l13:
  "d(x * bot) * L  x"
  using l12 order_trans zero_right_mult_decreasing by blast

lemma l14:
  "x * L  x * bot  L"
  by (metis d_mult_below l1 sup_right_isotone)

lemma l15:
  "x * d(y) * L = x * bot  d(x * y) * L"
  by (metis d_commutative d_mult_d d_zero l1 mult_assoc mult_left_zero)

lemma l16:
  "x * top  L  x * L"
  using inf.order_lesseq_imp l11 vector_meet by blast

lemma l17:
  "d(x) * L  d(x * L) * L"
  by (metis d_mult_below l11 le_infE le_infI meet_intro_domain)

lemma l18:
  "d(x) * L = d(x * L) * L"
  by (simp add: order.antisym d_mult_sub l17 mult_left_isotone)

lemma l19:
  "d(x * top * bot) * L  d(x * L) * L"
  by (metis d_mult_sub l18 mult_assoc mult_left_isotone)

lemma l20:
  "x  y  x  y  L  x  y  d(y * bot) * top"
  apply (rule iffI)
  apply (simp add: le_supI1)
  by (smt sup_commute sup_inf_distrib1 l13 le_iff_sup meet_domain_top)

lemma l21:
  "d(x * bot) * L  x * bot  L"
  by (simp add: d_mult_below l12)

lemma l22:
  "x * bot  L = d(x * bot) * L"
  using l21 order.antisym l9 by auto

lemma l23:
  "x * top  L = d(x) * L"
  apply (rule order.antisym)
  apply (simp add: vector_meet)
  by (metis d_mult_below inf.le_sup_iff inf_top.left_neutral l1 le_supE mult_left_sub_dist_inf_left)

lemma l29:
  "L * d(L) = L"
  by (metis d_preserves_equation d_restrict_equals l2)

lemma l30:
  "d(L) * x  (x  L)  d(L * bot) * x"
  by (metis inf.sup_right_divisibility inf_left_commute inf_sup_distrib1 l3 meet_domain_top)

lemma l31:
  "d(L) * x = (x  L)  d(L * bot) * x"
  by (smt (z3) l30 d_dist_sup le_iff_sup meet_intro_domain semiring.combine_common_factor sup_commute sup_inf_absorb zero_right_mult_decreasing)

lemma l40:
  "L * x  L"
  by (meson bot_least inf.order_trans l4 semiring.mult_left_mono top.extremum)

lemma l41:
  "L * top = L"
  by (simp add: l40 order.antisym top_right_mult_increasing)

lemma l50:
  "x * bot  L = (x  L) * bot"
  using order.antisym l5 l8 by force

lemma l51:
  "d(x * bot) * L = (x  L) * bot"
  using l22 l50 by auto

lemma l90:
  "L * top * L = L"
  by (simp add: l41 l10)

lemma l91:
  assumes "x = x * top"
    shows "d(L * bot) * x  d(x * bot) * top"
proof -
  have "d(L * bot) * x  d(d(L * bot) * x) * top"
    using d_galois by blast
  also have "... = d(d(L * bot) * d(x)) * top"
    using d_mult_d by auto
  also have "... = d(d(x) * L * bot) * top"
    using d_commutative d_mult_d ils.il_inf_associative by auto
  also have "...  d(x * L * bot) * top"
    by (metis d_isotone l11 mult_left_isotone)
  also have "...  d(x * top * bot) * top"
    by (simp add: d_isotone mult_left_isotone mult_right_isotone)
  finally show ?thesis
    using assms by auto
qed

lemma l92:
  assumes "x = x * top"
    shows "d(L * bot) * x  d((x  L) * bot) * top"
proof -
  have "d(L * bot) * x = d(L) * d(L * bot) * x"
    using d_commutative d_mult_sub d_order by auto
  also have "...  d(L) * d(x * bot) * top"
    by (metis assms order.eq_iff l91 mult_assoc mult_isotone)
  also have "... = d(d(x * bot) * L) * top"
    by (simp add: d_commutative d_export)
  also have "...  d((x  L) * bot) * top"
    by (simp add: l51)
  finally show ?thesis
    .
qed

end

class domain_itering_lattice_L = bounded_itering + domain_semiring_lattice_L
begin

lemma mult_L_circ:
  "(x * L) = 1  x * L"
  by (metis circ_back_loop_fixpoint circ_mult l40 le_iff_sup mult_assoc)

lemma mult_L_circ_mult_below:
  "(x * L) * y  y  x * L"
  by (smt sup_right_isotone l40 mult_L_circ mult_assoc mult_left_one mult_right_dist_sup mult_right_isotone)

lemma circ_L:
  "L = L  1"
  by (metis sup_commute l10 mult_L_circ)

lemma circ_d0_L:
  "x * d(x * bot) * L = x * bot"
  by (metis sup_bot_right circ_loop_fixpoint circ_plus_same d_zero l15 mult_assoc mult_left_zero)

lemma d0_circ_left_unfold:
  "d(x * bot) = d(x * x * bot)"
  by (metis sup_commute sup_bot_left circ_loop_fixpoint mult_assoc)

lemma d_circ_import:
  "d(y) * x  x * d(y)  d(y) * x = d(y) * (d(y) * x)"
  apply (rule order.antisym)
  apply (simp add: circ_import d_idempotent d_plus_one le_iff_sup)
  using circ_isotone d_mult_below mult_right_isotone by auto

end

class domain_omega_algebra_lattice_L = bounded_left_zero_omega_algebra + domain_semiring_lattice_L
begin

lemma mult_L_star:
  "(x * L) = 1  x * L"
  by (metis l40 le_iff_sup mult_assoc star.circ_back_loop_fixpoint star.circ_mult)

lemma mult_L_omega:
  "(x * L)ω  x * L"
  by (metis l40 mult_right_isotone omega_slide)

lemma mult_L_sup_star:
  "(x * L  y) = y  y * x * L"
proof (rule order.antisym)
  have "(x * L  y) * (y  y * x * L) = x * L * (y  y * x * L)  y * (y  y * x * L)"
    by (simp add: mult_right_dist_sup)
  also have "...  x * L  y * (y  y * x * L)"
    by (metis sup_left_isotone l40 mult_assoc mult_right_isotone)
  also have "...  x * L  y * y  y * x * L"
    by (smt sup_assoc sup_commute sup_ge2 mult_assoc mult_left_dist_sup star.circ_loop_fixpoint)
  also have "...  x * L  y  y * x * L"
    by (meson order_refl star.left_plus_below_circ sup_mono)
  also have "... = y  y * x * L"
    by (metis sup_assoc sup_commute mult_assoc star.circ_loop_fixpoint star.circ_reflexive star.circ_sup_one_right_unfold star_involutive)
  finally have "1  (x * L  y) * (y  y * x * L)  y  y * x * L"
    by (meson le_supI le_supI1 star.circ_reflexive)
  thus "(x * L  y)  y  y * x * L"
    using star_left_induct by fastforce
next
  show "y  y * x * L  (x * L  y)"
    by (metis sup_commute le_sup_iff mult_assoc star.circ_increasing star.circ_mult_upper_bound star.circ_sub_dist)
qed

lemma mult_L_sup_omega:
  "(x * L  y)ω  yω  y * x * L"
proof -
  have 1: "(y * x * L)ω  yω  y * x * L"
    by (simp add: le_supI2 mult_L_omega)
  have "(y * x * L) * yω  yω  y * x * L"
    by (metis sup_right_isotone l40 mult_assoc mult_right_isotone star_left_induct)
  thus ?thesis
    using 1 by (simp add: ils.il_inf_associative omega_decompose sup_monoid.add_commute)
qed

end

sublocale domain_omega_algebra_lattice_L < dL_star: itering where circ = star ..

sublocale domain_omega_algebra_lattice_L < dL_star: domain_itering_lattice_L where circ = star ..

context domain_omega_algebra_lattice_L
begin

lemma d0_star_below_d0_omega:
  "d(x * bot)  d(xω * bot)"
  by (simp add: d_isotone star_bot_below_omega_bot)

lemma d0_below_d0_omega:
  "d(x * bot)  d(xω * bot)"
  by (metis d0_star_below_d0_omega d_isotone mult_left_isotone order_trans star.circ_increasing)

lemma star_L_split:
  assumes "y  z"
      and "x * z * L  x * bot  z * L"
    shows "x * y * L  x * bot  z * L"
proof -
  have "x * (x * bot  z * L)  x * bot  x * z * L"
    by (metis sup_bot_right order.eq_iff mult_assoc mult_left_dist_sup star.circ_loop_fixpoint)
  also have "...  x * bot  x * bot  z * L"
    using assms(2) semiring.add_left_mono sup_monoid.add_assoc by auto
  also have "... = x * bot  z * L"
    using mult_isotone star.circ_increasing sup.absorb_iff1 by force
  finally have "y * L  x * (x * bot  z * L)  x * bot  z * L"
    by (simp add: assms(1) le_supI1 mult_left_isotone sup_monoid.add_commute)
  thus ?thesis
    by (simp add: star_left_induct mult.assoc)
qed

lemma star_L_split_same:
  "x * y * L  x * bot  y * L  x * y * L = x * bot  y * L"
  apply (rule order.antisym)
  using star_L_split apply blast
  by (metis bot_least ils.il_inf_associative le_supI mult_isotone mult_left_one order_refl star.circ_reflexive)

lemma star_d_L_split_equal:
  "d(x * y)  d(y)  x * d(y) * L = x * bot  d(y) * L"
  by (metis sup_right_isotone l15 le_iff_sup mult_right_sub_dist_sup_left star_L_split_same)

lemma d0_omega_mult:
  "d(xω * y * bot) = d(xω * bot)"
  apply (rule order.antisym)
  apply (simp add: d_isotone mult_isotone omega_sub_vector)
  by (metis d_isotone mult_assoc mult_right_isotone bot_least)

lemma d_omega_export:
  "d(y) * x  x * d(y)  d(y) * xω = (d(y) * x)ω"
  apply (rule order.antisym)
  apply (simp add: d_preserves_equation omega_simulation)
  by (smt le_iff_sup mult_left_dist_sup omega_simulation_2 omega_slide)

lemma d_omega_import:
  "d(y) * x  x * d(y)  d(y) * xω = d(y) * (d(y) * x)ω"
  using d_idempotent omega_import order.refl by auto

lemma star_d_omega_top:
  "x * d(xω) * top = x * bot  d(xω) * top"
  apply (rule order.antisym)
  apply (metis le_supI2 mult_domain_top star_mult_omega)
  by (metis ils.il_inf_associative le_supI mult_left_one mult_left_sub_dist_sup_right mult_right_sub_dist_sup_left star.circ_right_unfold_1 sup_monoid.add_0_right)

lemma omega_meet_L:
  "xω  L = d(xω) * L"
  by (metis l23 omega_vector)

proposition d_star_mult: "d(x * y)  d(y)  d(x * y) = d(x * bot)  d(y)" oops
proposition d0_split_omega_omega: "xω  xω * bot  d(xω  L) * top" nitpick [expect=genuine,card=2] oops

end

end