Theory Dioid_Power_Sum
section ‹Dioids, Powers and Finite Sums›
theory Dioid_Power_Sum
imports Kleene_Algebra.Dioid Kleene_Algebra.Finite_Suprema
begin
text ‹We add a few facts about powers and finite
sums---in fact, finite suprema---to an existing theory field for dioids.›
context dioid_one_zero
begin
lemma add_iso_r: "y ≤ z ⟹ x + y ≤ x + z"
using local.join.sup_mono by blast
notation power (‹_⇗_⇖› [101,50] 100)
lemma power_subdist: "x⇗n⇖ ≤ (x + y)⇗n⇖"
apply (induct n)
apply simp
using local.mult_isol_var local.power_Suc2 by auto
lemma power_inductl_var: "x ⋅ y ≤ y ⟹ x⇗n⇖ ⋅ y ≤ y"
apply (induct n)
apply simp
by (metis (no_types, lifting) local.dual_order.trans local.mult_isol local.power_Suc2 mult_assoc)
lemma power_inductr_var: "y ⋅ x ≤ y ⟹ y ⋅ x⇗n⇖ ≤ y"
by (induct n, metis eq_refl mult_oner power.simps(1), metis mult.assoc mult_isor order_refl order_trans power.simps(2) power_commutes)
definition powsum :: "'a ⇒ nat ⇒ nat ⇒ 'a" (‹_⇘_⇙⇗_⇖› [101,50,50] 100) where
"powsum x m n = sum ((^) x) {m..n + m}"
lemmas powsum_simps = powsum_def atLeastAtMostSuc_conv numerals
lemma powsum1 [simp]: "x⇘n⇙⇗0⇖ = x⇗n⇖"
by (simp add:powsum_simps)
lemma powsum2: "x⇘n⇙⇗Suc m⇖ = x⇘n⇙⇗m ⇖+ x⇗n+Suc m⇖"
proof-
have "x⇘n⇙⇗Suc m⇖ = sum ((^) x) {n..(Suc m)+n}"
using powsum_def by blast
also have "... = sum ((^) x) {n..m+n} + x⇗n+Suc m⇖"
by (simp add: ab_semigroup_add_class.add.commute atLeastAtMostSuc_conv local.join.sup_commute)
finally show ?thesis
by (simp add: powsum_def)
qed
lemma powsum_00 [simp]: "x⇘0⇙⇗0 ⇖= 1"
by (simp add: powsum_def)
lemma powsum_01 [simp]: "x⇘0⇙⇗1⇖ = 1 + x"
by (simp add: powsum2)
lemma powsum_10 [simp]: "x⇘1⇙⇗0⇖ = x"
by (simp add: powsum_simps)
lemma powsum_split: "x⇘m⇙⇗i+Suc n⇖ = x⇘m⇙⇗i⇖ + x⇘m+Suc i⇙⇗n⇖"
by (induct n, simp_all add:powsum_simps ac_simps)
lemma powsum_split_var1: "x⇘0⇙⇗n+1⇖ = 1 + x⇘1⇙⇗n⇖"
proof -
have "x⇘0⇙⇗n + 1⇖ = x⇘0⇙⇗0 + Suc n⇖"
by simp
also have "... = x⇘0⇙⇗0⇖ + x⇘0 + Suc 0⇙⇗n⇖"
by (subst powsum_split, rule refl)
also have "... = 1 + x⇘0 + Suc 0⇙⇗n⇖"
by simp
finally show ?thesis
by simp
qed
lemma powsum_split_var2 [simp]: "x⇗m⇖ + x⇘0⇙⇗m⇖ = x⇘0⇙⇗m⇖"
proof (induct m)
case 0 show ?case
by (metis add_idem' power_0 powsum_00)
case (Suc n) show ?case
by (simp add: add_commute powsum2)
qed
lemma powsum_split_var3: "x⇘0⇙⇗m+Suc n⇖ = x⇘0⇙⇗m ⇖+ x⇘0+Suc m⇙⇗n⇖"
by (subst powsum_split, simp)
lemma powsum_split_var4 [simp]: "x⇘0⇙⇗m+n⇖ + x⇘m⇙⇗n⇖ = x⇘0⇙⇗m+n⇖"
proof (induct n)
case 0 show ?case
by (metis add_0_iff add_comm powsum1 powsum_split_var2)
next
case (Suc n) note hyp = this
show ?case
proof -
have "x⇘0⇙⇗m + Suc n⇖ + x⇘m⇙⇗Suc n⇖ = x⇘0⇙⇗m + n⇖ + x⇗Suc (m + n)⇖ + (x⇘m⇙⇗n⇖ + x⇗m + Suc n⇖)"
by (auto simp add: powsum2)
also have "... = (x⇘0⇙⇗m + n ⇖+ x⇘m⇙⇗n⇖) + x⇗Suc (m + n)⇖ + x⇗m + Suc n⇖"
by (metis add.assoc add.left_commute)
also have "... = x⇗Suc (m+n)⇖ + x⇘0⇙⇗m+n⇖"
by (metis add_Suc_right add.assoc add.commute add_idem' hyp)
also have "... = x⇘0⇙⇗m + Suc n⇖"
by (simp add: add_commute powsum2)
finally show ?thesis .
qed
qed
lemma powsum_split_var6: "x⇘0⇙⇗(Suc k)+Suc n⇖ = x⇘0⇙⇗Suc k ⇖+ x⇘0+Suc (Suc k)⇙⇗n⇖"
by (metis powsum_split_var3)
lemma powsum_ext: "x ≤ x⇘0⇙⇗Suc n⇖"
proof (induct n)
case 0 show ?case
by (metis One_nat_def local.join.sup_ge2 powsum_01)
next
case (Suc n) thus ?case
by (auto simp add:less_eq_def powsum_simps, metis (lifting, no_types) add.left_commute)
qed
lemma powsum_one: "1 ≤ x⇘0⇙⇗Suc n⇖"
by (induct n, metis One_nat_def local.join.sup.cobounded1 powsum_01, metis (full_types) Suc_eq_plus1 local.join.sup.cobounded1 powsum_split_var1)
lemma powsum_shift1: "x ⋅ x⇘m⇙⇗n⇖ = x⇘m+1⇙⇗n⇖"
apply (induct n)
apply (simp_all add: powsum_simps)
apply (metis local.add_left_comm local.distrib_left powsum_def)
done
lemma powsum_shift: "x⇗k ⇖⋅ x⇘m⇙⇗n⇖ = x⇘k+m⇙⇗n⇖"
by (induct k, simp_all, metis Suc_eq_plus1 mult.assoc powsum_shift1)
lemma powsum_prod_suc: "x⇘0⇙⇗m ⇖⋅ x⇘0⇙⇗Suc n⇖ = x⇘0⇙⇗Suc (m+n)⇖"
proof (induct m)
case 0 show ?case
by simp
case (Suc m)
note hyp = this
show ?case
proof -
have "x⇘0⇙⇗Suc m ⇖⋅ x⇘0⇙⇗Suc n⇖ = x⇘0⇙⇗m⇖ ⋅ x⇘0⇙⇗Suc n⇖ + x⇗Suc m ⇖⋅ x⇘0⇙⇗Suc n⇖"
by (simp add: powsum2)
also have "... = x⇘0⇙⇗Suc (m + n)⇖ + x⇗Suc m ⇖⋅ x⇘0⇙⇗Suc n⇖"
by (simp add:hyp)
also have "... = x⇘0⇙⇗Suc (m + n)⇖ + x⇘Suc m⇙⇗Suc n⇖"
by (subst powsum_shift, simp)
also have "... = x⇘0⇙⇗Suc (m + n)⇖ + (x⇘Suc m⇙⇗n⇖ + x⇗Suc m + Suc n⇖)"
by (simp add:powsum2)
also have "... = x⇘0⇙⇗Suc (m + n)⇖ + x⇘Suc m⇙⇗n⇖ + x⇗Suc (Suc (m + n))⇖"
by (metis add_Suc_right add_Suc_shift add.assoc add.left_commute)
also have "... = x⇘0⇙⇗Suc (m + n)⇖ + x⇗Suc (Suc (m + n))⇖"
by (simp only: add_Suc_right[THEN sym] add_Suc_shift[THEN sym] powsum_split_var4)
also have "... = x⇘0⇙⇗Suc (Suc m + n)⇖"
by (simp add: powsum2)
finally show ?thesis .
qed
qed
lemma powsum_prod: "x⇘0⇙⇗m ⇖⋅ x⇘0⇙⇗n⇖ = x⇘0⇙⇗m+n⇖"
by (cases n, simp, simp add: powsum_prod_suc)
end
end