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

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: "xn (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  xn 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  xn 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]: "xn⇙⇗0= xn⇖"
  by (simp add:powsum_simps)
  
lemma powsum2: "xn⇙⇗Suc m= xn⇙⇗m+ xn+Suc m⇖"
proof-
  have "xn⇙⇗Suc m= sum ((^) x) {n..(Suc m)+n}"
    using powsum_def by blast
  also have "... = sum ((^) x) {n..m+n} +  xn+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]: "x0⇙⇗0= 1"
  by (simp add: powsum_def)

lemma powsum_01 [simp]: "x0⇙⇗1= 1 + x" 
  by (simp add: powsum2) 

lemma powsum_10 [simp]: "x1⇙⇗0= x"  
  by (simp add: powsum_simps) 

lemma powsum_split: "xm⇙⇗i+Suc n= xm⇙⇗i+ xm+Suc i⇙⇗n⇖"
  by (induct n, simp_all add:powsum_simps ac_simps)

lemma powsum_split_var1: "x0⇙⇗n+1= 1 + x1⇙⇗n⇖" 
proof -
  have "x0⇙⇗n + 1= x0⇙⇗0 + Suc n⇖"
    by simp
  also have "... = x0⇙⇗0+ x0 + Suc 0⇙⇗n⇖"
    by (subst powsum_split, rule refl)
  also have "... = 1 + x0 + Suc 0⇙⇗n⇖"
    by simp
  finally show ?thesis 
    by simp
qed

lemma powsum_split_var2 [simp]: "xm+ x0⇙⇗m= x0⇙⇗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: "x0⇙⇗m+Suc n= x0⇙⇗m+ x0+Suc m⇙⇗n⇖" 
  by (subst powsum_split, simp)

lemma powsum_split_var4 [simp]: "x0⇙⇗m+n+ xm⇙⇗n= x0⇙⇗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  "x0⇙⇗m + Suc n+ xm⇙⇗Suc n= x0⇙⇗m + n+ xSuc (m + n)+ (xm⇙⇗n+ xm + Suc n)"
      by (auto simp add: powsum2)  
    also have "... = (x0⇙⇗m + n+ xm⇙⇗n) + xSuc (m + n)+ xm + Suc n⇖"
      by (metis add.assoc add.left_commute)
    also have "... =  xSuc (m+n)+ x0⇙⇗m+n⇖"
      by (metis add_Suc_right add.assoc add.commute add_idem' hyp)
    also have "... = x0⇙⇗m + Suc n⇖"
      by (simp add: add_commute powsum2)
    finally show ?thesis .
  qed
qed

lemma powsum_split_var6: "x0⇙⇗(Suc k)+Suc n= x0⇙⇗Suc k+ x0+Suc (Suc k)⇙⇗n⇖"     
  by (metis powsum_split_var3) 

lemma powsum_ext: "x  x0⇙⇗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  x0⇙⇗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  xm⇙⇗n= xm+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: "xk xm⇙⇗n= xk+m⇙⇗n⇖" 
  by (induct k, simp_all, metis Suc_eq_plus1 mult.assoc powsum_shift1)

lemma powsum_prod_suc: "x0⇙⇗m x0⇙⇗Suc n= x0⇙⇗Suc (m+n)⇖"
proof (induct m)
  case 0 show ?case
    by simp
  case (Suc m) 
  note hyp = this
  show ?case
  proof -
    have "x0⇙⇗Suc m x0⇙⇗Suc n=  x0⇙⇗m x0⇙⇗Suc n+ xSuc m x0⇙⇗Suc n⇖"
      by (simp add: powsum2)
    also have "... = x0⇙⇗Suc (m + n)+ xSuc m x0⇙⇗Suc n⇖"
      by (simp add:hyp)
    also have "... = x0⇙⇗Suc (m + n)+ xSuc m⇙⇗Suc n⇖"
      by (subst powsum_shift, simp)
    also have "... = x0⇙⇗Suc (m + n)+ (xSuc m⇙⇗n+ xSuc m + Suc n)"
      by (simp add:powsum2)
    also have "... = x0⇙⇗Suc (m + n)+ xSuc m⇙⇗n+ xSuc (Suc (m + n))⇖"
      by (metis add_Suc_right add_Suc_shift add.assoc add.left_commute)
    also have "... = x0⇙⇗Suc (m + n)+ xSuc (Suc (m + n))⇖"
      by (simp only: add_Suc_right[THEN sym] add_Suc_shift[THEN sym] powsum_split_var4)
    also have "... = x0⇙⇗Suc (Suc m + n)⇖"
      by (simp add: powsum2)
    finally show ?thesis .
  qed
qed

lemma powsum_prod: "x0⇙⇗m x0⇙⇗n= x0⇙⇗m+n⇖"
  by (cases n, simp, simp add: powsum_prod_suc)

end

end