# Theory Dioid_Power_Sum

```(* Title:      Regular Algebras
Author:     Simon Foster, Georg Struth
Maintainer: Simon Foster <s.foster at york.ac.uk>
Georg Struth <g.struth at sheffield.ac.uk>
*)

section ‹Dioids, Powers and Finite Sums›

theory Dioid_Power_Sum
imports Kleene_Algebra.Dioid Kleene_Algebra.Finite_Suprema

begin

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⇖"

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⇖"
finally show ?thesis
qed

lemma powsum_00 [simp]: "x⇘0⇙⇗0 ⇖= 1"

lemma powsum_01 [simp]: "x⇘0⇙⇗1⇖ = 1 + x"

lemma powsum_10 [simp]: "x⇘1⇙⇗0⇖ = x"

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
case (Suc n) show ?case
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
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⇖)"
also have "... = (x⇘0⇙⇗m + n ⇖+ x⇘m⇙⇗n⇖) + x⇗Suc (m + n)⇖ + x⇗m + Suc n⇖"
also have "... =  x⇗Suc (m+n)⇖ + x⇘0⇙⇗m+n⇖"
also have "... = x⇘0⇙⇗m + Suc n⇖"
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
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)
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⇖"
also have "... = x⇘0⇙⇗Suc (m + n)⇖ + x⇗Suc m ⇖⋅ x⇘0⇙⇗Suc n⇖"
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⇖)"
also have "... = x⇘0⇙⇗Suc (m + n)⇖ + x⇘Suc m⇙⇗n⇖ + x⇗Suc (Suc (m + n))⇖"
also have "... = x⇘0⇙⇗Suc (m + n)⇖ + x⇗Suc (Suc (m + n))⇖"