Theory Domain_Iterings
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