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_mult_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_mult_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