# Theory Factorials

(* Authors: Amine Chaieb & Florian Haftmann, TU Muenchen with contributions by Lukas Bulwahn *)

section ‹Falling factorials›

theory Factorials
imports Complex_Main "HOL-Combinatorics.Stirling"
begin

lemma pochhammer_0 [simp]: ― ‹TODO move›
"pochhammer 0 n = (0::nat)" if "n > 0"
using that by (simp add: pochhammer_prod)

definition ffact :: "nat ⇒ 'a::comm_semiring_1_cancel ⇒ 'a"
where "ffact n a = pochhammer (a + 1 - of_nat n) n"

lemma ffact_0 [simp]:
"ffact 0 = (λx. 1)"

lemma ffact_Suc:
"ffact (Suc n) a = a * ffact n (a - 1)"
for a :: "'a :: comm_ring_1"
by (simp add: ffact_def pochhammer_prod prod.atLeast0_lessThan_Suc algebra_simps)

(* TODO: what's the right class here? *)
lemma ffact_Suc_rev:
"ffact (Suc n) m = (m - of_nat n) * ffact n m"
for m :: "'a :: {comm_semiring_1_cancel, ab_group_add}"

lemma ffact_nat_triv:
"ffact n m = 0" if "m < n"
using that by (simp add: ffact_def)

lemma ffact_Suc_nat:
"ffact (Suc n) m = m * ffact n (m - 1)"
for m :: nat
proof (cases "n ≤ m")
case True
then show ?thesis
by (simp add: ffact_def pochhammer_prod algebra_simps prod.atLeast0_lessThan_Suc)
next
case False
then have "m < n"
by simp
then show ?thesis
qed

lemma ffact_Suc_rev_nat:
"ffact (Suc n) m = (m - n) * ffact n m"
proof (cases "n ≤ m")
case True
then show ?thesis
by (simp add: ffact_def pochhammer_rec Suc_diff_le)
next
case False
then have "m < n" by simp
then show ?thesis by (simp add: ffact_nat_triv)
qed

lemma fact_div_fact_ffact:
"fact n div fact m = ffact (n - m) n" if "m ≤ n"
proof -
from that have "fact n = ffact (n - m) n * fact m"
by (simp add: ffact_def pochhammer_product pochhammer_fact)
moreover have "fact m dvd (fact n :: nat)"
using that by (rule fact_dvd)
ultimately show ?thesis
by simp
qed

lemma fact_div_fact_ffact_nat:
"fact n div fact (n - k) = ffact k n" if "k ≤ n"
using that by (simp add: fact_div_fact_ffact)

lemma ffact_fact:
"ffact n (of_nat n) = (of_nat (fact n) :: 'a :: comm_ring_1)"
by (induct n) (simp_all add: algebra_simps ffact_Suc)

"(a - of_nat n) * ffact n a + of_nat n * ffact n a = a * ffact n a"
for a :: "'a :: comm_ring_1"

lemma mult_ffact:
"a * ffact n a = ffact (Suc n) a + of_nat n * ffact n a"
for a :: "'a :: comm_ring_1"
proof -
have "ffact (Suc n) a + of_nat n * (ffact n a) = (a - of_nat n) * (ffact n a) + of_nat n * (ffact n a)"
using ffact_Suc_rev [of n] by auto
also have "… = a * ffact n a" using ffact_add_diff_assoc by (simp add: algebra_simps)
finally show ?thesis by simp
qed

(* TODO: what's the right class here? *)
lemma prod_ffact:
fixes m :: "'a :: {ord, ring_1, comm_monoid_mult, comm_semiring_1_cancel}"
shows "(∏i = 0..<n. m - of_nat i) = ffact n m"
proof -
have "inj_on (λj. j - 1) {1..n}"
by (force intro: inj_on_diff_nat)
moreover have "{0..<n} = (λj. j - 1)  {1..n}"
proof -
have "i ∈ (λj. j - 1)  {1..n}" if "i ∈ {0..<n}" for i
using that by (auto intro: image_eqI[where x="i + 1"])
from this show ?thesis by auto
qed
moreover have "m - of_nat (i - 1) = m + 1 - of_nat n + of_nat (n - i)" if "i ∈ {1..n}" for i
using that by (simp add: of_nat_diff)
ultimately have "(∏i = 0..<n. m - of_nat i) = (∏i = 1..n. m + 1 - of_nat n + of_nat (n - i))"
by (rule prod.reindex_cong)
from this show ?thesis
unfolding ffact_def by (simp only: pochhammer_prod_rev)
qed

lemma prod_ffact_nat:
fixes m :: nat
shows "(∏i = 0..<n. m - i) = ffact n m"
proof cases
assume "n ≤ m"
have "inj_on (λj. j - 1) {1..n}" by (force intro: inj_on_diff_nat)
moreover have "{0..<n} = (λj. j - 1)  {1..n}"
proof -
have "i ∈ (λj. j - 1)  {1..n}" if "i ∈ {0..<n}" for i
using that by (auto intro: image_eqI[where x="i + 1"])
from this show ?thesis by auto
qed
ultimately have "(∏i = 0..<n. m - i) = (∏i = 1..n. (m + 1) - i)"
by (auto intro: prod.reindex_cong[where l="λi. i - 1"])
from this ‹n ≤ m› show ?thesis
unfolding ffact_def by (simp add: pochhammer_prod_rev)
next
assume "¬ n ≤ m"
from this show ?thesis by (auto simp add: ffact_nat_triv)
qed

(* TODO: what's the right class here? *)
lemma prod_rev_ffact:
fixes m :: "'a :: {ord, ring_1, comm_monoid_mult, comm_semiring_1_cancel}"
shows "(∏i = 1..n. m - of_nat n + of_nat i) = ffact n m"
proof -
have "inj_on (λi. i + 1) {0..<n}" by simp
moreover have "{1..n} = (λi. i + 1)  {0..<n}" by auto
moreover have "m - of_nat n + of_nat (i + 1) = m + 1 - of_nat n + of_nat i" for i by simp
ultimately have "(∏i = 1..n. m - of_nat n + of_nat i) = (∏i = 0..<n. m + 1 - of_nat n + of_nat i)"
by (rule prod.reindex_cong[where l="λi. i + 1"])
from this show ?thesis
unfolding ffact_def by (simp only: pochhammer_prod)
qed

lemma prod_rev_ffact_nat:
fixes m :: nat
assumes "n ≤ m"
shows "(∏i = 1..n. m - n + i) = ffact n m"
proof -
have "inj_on (λi. i + 1) {0..<n}" by simp
moreover have "{1..n} = (λi. i + 1)  {0..<n}" by auto
moreover have "m - n + (i + 1) = m + 1 - n + i" for i
using  ‹n ≤ m› by auto
ultimately have "(∏i = 1..n. m - n + i) = (∏i = 0..<n. m + 1 - n + i)"
by (rule prod.reindex_cong)
from this show ?thesis
unfolding ffact_def by (simp only: pochhammer_prod of_nat_id)
qed

lemma prod_rev_ffact_nat':
fixes m :: nat
assumes "n ≤ m"
shows "∏{m - n + 1..m} = ffact n m"
proof -
have "inj_on (λi. m - n + i) {1::nat..n}" by (auto intro: inj_onI)
moreover have "{m - n + 1..m} = (λi. m - n + i)  {1::nat..n}"
proof -
have "i ∈ (λi. m + i - n)  {Suc 0..n}" if "i ∈ {m - n + 1..m}" for i
using that ‹n ≤ m› by (auto intro!: image_eqI[where x="i - (m - n)"])
with ‹n ≤ m› show ?thesis by auto
qed
moreover have "m - n + i = m - n + i" for i ..
ultimately have "∏{m - n + (1::nat)..m} = (∏i = 1..n. m - n + i)"
by (rule prod.reindex_cong)
from this show ?thesis
using ‹n ≤ m› by (simp only: prod_rev_ffact_nat)
qed

lemma ffact_eq_fact_mult_binomial:
"ffact k n = fact k * (n choose k)"
proof cases
assume "k ≤ n"
have "ffact k n = fact n div fact (n - k)"
using ‹k ≤ n› by (simp add: fact_div_fact_ffact_nat)
also have "… = fact k * (n choose k)"
using ‹k ≤ n› by (simp add: binomial_fact_lemma[symmetric])
finally show ?thesis .
next
assume "¬ k ≤ n"
from this ffact_nat_triv show ?thesis by force
qed

lemma of_nat_ffact:
"of_nat (ffact n m) = ffact n (of_nat m :: 'a :: comm_ring_1)"
proof (induct n arbitrary: m)
case 0
then show ?case
by simp
next
case (Suc n)
show ?case
proof (cases m)
case 0
then show ?thesis
next
case (Suc m)
with Suc.hyps show ?thesis
by (simp add: algebra_simps ffact_Suc_nat ffact_Suc)
qed
qed

lemma of_int_ffact:
"of_int (ffact n k) = ffact n (of_int k :: 'a :: comm_ring_1)"
proof (induct n arbitrary: k)
case 0 then show ?case by simp
next
case (Suc n k)
then have "of_int (ffact n (k - 1)) = ffact n (of_int (k - 1) :: 'a)" .
then show ?case
qed

lemma ffact_minus:
fixes x :: "'a :: comm_ring_1"
shows "ffact n (- x) = (- 1) ^ n * pochhammer x n"
proof -
have "ffact n (- x) = pochhammer (- x + 1 - of_nat n) n"
unfolding ffact_def ..
also have "… = pochhammer (- x - of_nat n + 1) n"
also have "… = (- 1) ^ n * pochhammer (- (- x)) n"
by (rule pochhammer_minus')
also have "… = (- 1) ^ n * pochhammer x n" by simp
finally show ?thesis .
qed

text ‹Conversion of natural potences into falling factorials and back›

lemma monomial_ffact:
"a ^ n = (∑k = 0..n. of_nat (Stirling n k) * ffact k a)"
for a :: "'a :: comm_ring_1"
proof (induct n)
case 0 then show ?case by simp
next
case (Suc n)
then have "a ^ Suc n = a * (∑k = 0..n. of_nat (Stirling n k) * ffact k a)"
by simp
also have "… = (∑k = 0..n. of_nat (Stirling n k) * (a * ffact k a))"
also have "… = (∑k = 0..n. of_nat (Stirling n k) * ffact (Suc k) a) +
(∑k = 0..n. of_nat (Stirling n k) * (of_nat k * ffact k a))"
by (simp add: sum.distrib algebra_simps mult_ffact)
also have "… = (∑k = 0.. Suc n. of_nat (Stirling n k) * ffact (Suc k) a) +
(∑k = 0..Suc n. of_nat ((Suc k) * (Stirling n (Suc k))) * (ffact (Suc k) a))"
proof -
have "(∑k = 0..n. of_nat (Stirling n k) * (of_nat k * ffact k a)) =
(∑k = 0..n+2. of_nat (Stirling n k) * (of_nat k * ffact k a))" by simp
also have "… = (∑k = Suc 0 .. Suc (Suc n). of_nat (Stirling n k) * (of_nat k * ffact k a)) "
by (simp only: sum.atLeast_Suc_atMost [of 0 "n + 2"]) simp
also have "… = (∑k = 0 .. Suc n. of_nat (Stirling n (Suc k)) * (of_nat (Suc k) * ffact (Suc k) a))"
by (simp only: image_Suc_atLeastAtMost sum.shift_bounds_cl_Suc_ivl)
also have "… = (∑k = 0 .. Suc n. of_nat ((Suc k) * Stirling n (Suc k)) * ffact (Suc k) a)"
by (simp only: of_nat_mult algebra_simps)
finally have "(∑k = 0..n. of_nat (Stirling n k) * (of_nat k * ffact k a)) =
(∑k = 0..Suc n. of_nat (Suc k * Stirling n (Suc k)) * ffact (Suc k) a)"
by simp
then show ?thesis by simp
qed
also have "… = (∑k = 0..n. of_nat (Stirling (Suc n) (Suc k)) * ffact (Suc k) a)"
also have "… = (∑k = Suc 0..Suc n. of_nat (Stirling (Suc n) k) * ffact k a)"
by (simp only: image_Suc_atLeastAtMost sum.shift_bounds_cl_Suc_ivl)
also have "… = (∑k = 0..Suc n. of_nat (Stirling (Suc n) k) * ffact k a)"
by (simp only: sum.atLeast_Suc_atMost [of "0" "Suc n"]) simp
finally show ?case by simp
qed

lemma ffact_monomial:
"ffact n a = (∑k = 0..n. (- 1) ^ (n - k) * of_nat (stirling n k) * a ^ k)"
for a :: "'a :: comm_ring_1"
proof (induct n)
case 0 show ?case by simp
next
case (Suc n)
then have "ffact (Suc n) a = (a - of_nat n) * (∑k = 0..n. (- 1) ^ (n - k) * of_nat (stirling n k) * a ^ k)"
also have "… = (∑k = 0..n. (- 1) ^ (n - k) * of_nat (stirling n k) * a ^ (Suc k)) +
(∑k = 0..n. (- 1) * (- 1) ^ (n - k) * of_nat (n * (stirling n k)) * a ^ k)"
also have "… = (∑k = 0..n. (- 1) ^ (Suc n - Suc k) * of_nat (stirling n k) * a ^ Suc k) +
(∑k = 0..n. (- 1) ^ (Suc n - Suc k) * of_nat (n * stirling n (Suc k)) * a ^ Suc k)"
proof -
have "(∑k = 0..n. (- 1) * (- 1) ^ (n - k) * of_nat (n * stirling n k) * a ^ k) =
(∑k = 0..n. (- 1) ^ (Suc n - k) * of_nat (n * stirling n k) * a ^ k)"
also have "… = (∑k = Suc 0..Suc n. (- 1) ^ (Suc n - k) * of_nat (n * stirling n k) * a ^ k)"
by (simp add: sum.atLeast_Suc_atMost) (cases n; simp)
also have "… = (∑k = 0..n. (- 1) ^ (Suc n - Suc k) * of_nat (n * stirling n (Suc k)) * a ^ Suc k)"
by (simp only: sum.shift_bounds_cl_Suc_ivl)
finally show ?thesis by simp
qed
also have "… = (∑k = 0..n. (- 1) ^ (Suc n - Suc k) * of_nat (n * stirling n (Suc k) + stirling n k) * a ^ Suc k)"
also have "… = (∑k = 0..n. (- 1) ^ (Suc n - Suc k) * of_nat (stirling (Suc n) (Suc k)) * a ^ Suc k)"
by (simp only: stirling.simps)
also have "… = (∑k = Suc 0..Suc n. (- 1) ^ (Suc n - k) * of_nat (stirling (Suc n) k) * a ^ k)"
by (simp only: sum.shift_bounds_cl_Suc_ivl)
also have "… = (∑k = 0..Suc n. (- 1) ^ (Suc n - k) * of_nat (stirling (Suc n) k) * a ^ k)"
finally show ?case .
qed

end


# Theory Discrete_Summation

(* Author: Florian Haftmann, TU Muenchen *)

section ‹Some basic facts about discrete summation›

theory Discrete_Summation
imports Main
begin

subsection ‹Auxiliary›

"sum f {k..<j} + sum f {l..<k} = sum f {l..<k} + sum f {k..<j}"

fixes j k l :: int
shows "j < k ⟹ k < l ⟹
sum f {j..<k} + sum f {k..<l} = sum f {j..<l}"
by (simp_all add: sum.union_inter [symmetric] ivl_disj_un)

subsection ‹The shift operator›

definition Δ :: "('b::ring_1 ⇒ 'a::ab_group_add) ⇒ int ⇒ 'a"
where
"Δ f k = f (of_int (k + 1)) - f (of_int k)"

lemma Δ_shift:
"Δ (λk. l + f k) = Δ f"

lemma Δ_same_shift:
assumes "Δ f = Δ g"
shows "∃l. plus l ∘ f ∘ of_int = g ∘ of_int"
proof -
let ?F = "λk. f (of_int k)"
let ?G = "λk. g (of_int k)"
from assms have "⋀k. Δ f (of_int k) = Δ g (of_int k)" by simp
then have k_incr: "⋀k. ?F (k + 1) - ?G (k + 1) = ?F k - ?G k"
then have "⋀k. ?F ((k - 1) + 1) - ?G ((k - 1) + 1) =
?F (k - 1) - ?G (k - 1)"
by blast
then have k_decr: "⋀k. ?F (k - 1) - ?G (k - 1) = ?F k - ?G k"
by simp
have "⋀k. ?F k - ?G k = ?F 0 - ?G 0"
proof -
fix k
show "?F k - ?G k = ?F 0 - ?G 0"
by (induct k rule: int_induct)
qed
then have "⋀k. (plus (?G 0 - ?F 0) ∘ ?F) k = ?G k"
then have "plus (?G 0 - ?F 0) ∘ ?F = ?G" ..
then have "plus (?G 0 - ?F 0) ∘ f ∘ of_int = g ∘ of_int"
by (simp only: comp_def)
then show ?thesis ..
qed

"Δ (λk. f k + g k) k = Δ f k + Δ g k"

lemma Δ_factor:
"Δ (λk. c * k) k = c"

subsection ‹The formal sum operator›

definition Σ :: "('b::ring_1 ⇒ 'a::ab_group_add) ⇒ int ⇒ int ⇒ 'a"
where
"Σ f j l = (if j < l then sum (f ∘ of_int) {j..<l}
else if j > l then - sum (f ∘ of_int) {l..<j}
else 0)"

lemma Σ_same [simp]:
"Σ f j j = 0"

lemma Σ_positive:
"j < l ⟹ Σ f j l = sum (f ∘ of_int) {j..<l}"

lemma Σ_negative:
"j > l ⟹ Σ f j l = - Σ f l j"

lemma Σ_comp_of_int:
"Σ (f ∘ of_int) = Σ f"

lemma Σ_const:
"Σ (λk. c) j l = of_int (l - j) * c"

"Σ (λk. f k + g k) j l = Σ f j l + Σ g j l"

lemma Σ_factor:
"Σ (λk. c * f k) j l = (c::'a::ring) * Σ (λk. f k) j l"

lemma Σ_concat:
"Σ f j k + Σ f k l = Σ f j l"
add_sum_orient [of "λk. f (of_int k)" j l k]

lemma Σ_incr_upper:
"Σ f j (l + 1) = Σ f j l + f (of_int l)"
proof -
have "{l..<l+1} = {l}" by auto
then have "Σ f l (l + 1) = f (of_int l)" by (simp add: Σ_def)
moreover have "Σ f j (l + 1) = Σ f j l + Σ f l (l + 1)" by (simp add: Σ_concat)
ultimately show ?thesis by simp
qed

subsection ‹Fundamental lemmas: The relation between @{term Δ} and @{term Σ}›

lemma Δ_Σ:
"Δ (Σ f j) = f"
proof
fix k
show "Δ (Σ f j) k = f k"
qed

lemma Σ_Δ:
"Σ (Δ f) j l = f (of_int l) - f (of_int j)"
proof -
from Δ_Σ have "Δ (Σ (Δ f) j) = Δ f" .
then obtain k where "plus k ∘ Σ (Δ f) j ∘ of_int = f ∘ of_int"
by (blast dest: Δ_same_shift)
then have "⋀q. f (of_int q) = k + Σ (Δ f) j q"
then show ?thesis by simp
qed

end



# Theory Summation_Conversion

(* Author: Florian Haftmann, TU Muenchen *)

section ‹A barebone conversion for discrete summation›

theory Summation_Conversion
imports Factorials Discrete_Summation
begin

text ‹Extensible theorem collection for solving summation problems›

named_theorems summation "rules for solving summation problems"

declare
Σ_factor [summation] monomial_ffact [summation]

lemma intervall_simps [summation]:
"(∑k::nat = 0..0. f k) = f 0"
"(∑k::nat = 0..Suc n. f k) = f (Suc n) + (∑k::nat = 0..n. f k)"

lemma Δ_ffact:
"Δ (ffact (Suc n)) k = of_nat (Suc n) * ffact n (of_int k :: 'a :: comm_ring_1)"
proof (induct n)
case 0 then show ?case
next
case (Suc n)
obtain m where "m = Suc n" by blast
have "Δ (ffact (Suc m)) k =
ffact (Suc m) (of_int (k + 1)) - ffact (Suc m) (of_int k :: 'a)"
also have "… = of_int (k + 1) * ffact m (of_int k)
- (ffact m (of_int k) * (of_int k - of_nat m))"
using ffact_Suc_rev [of m "(of_int k :: 'a :: comm_ring_1)"]
also have "… = (of_int k + 1 - of_int k + of_nat m) * ffact m (of_int k)"
also have "… = of_nat (Suc m) * ffact m (of_int k)" by simp
also have "… = of_nat (Suc m) * ffact (Suc m - 1) (of_int k)" by simp
finally show ?case by (simp only: ‹m = Suc n› diff_Suc_1)
qed

lemma Σ_ffact_divide [summation]:
"Σ (ffact n) j l =
(ffact (Suc n) (of_int l :: 'a :: {idom_divide, semiring_char_0}) - ffact (Suc n) (of_int j)) div of_nat (Suc n)"
proof -
have *: "(of_nat (Suc n) * Σ (ffact n) j l) div of_nat (Suc n) = (Σ (ffact n) j l :: 'a)"
using of_nat_neq_0 [where ?'a = 'a] by simp
have "ffact (Suc n) (of_int l :: 'a) - ffact (Suc n) (of_int j) =
Σ (λk. Δ (ffact (Suc n)) k) j l"
also have "… = Σ (λk. of_nat (Suc n) * ffact n (of_int k)) j l"
also have "… = of_nat (Suc n) * Σ (ffact n ∘ of_int) j l"
finally show ?thesis by (simp only: Σ_comp_of_int * of_nat_eq_0_iff)
qed

text ‹Various other rules›

lemma of_int_coeff:
"(of_int l :: 'a::comm_ring_1) * numeral k = of_int (l * numeral k)"
by simp

lemmas nat_simps =
mult_Suc mult_Suc_right mult_zero_left mult_zero_right
One_nat_def of_nat_simps

lemmas of_int_pull_out =
of_int_add [symmetric] of_int_diff [symmetric] of_int_mult [symmetric]
of_int_coeff

lemma of_nat_coeff:
"(of_nat n :: 'a::comm_semiring_1) * numeral m = of_nat (n * numeral m)"
by (induct n) simp_all

lemmas of_nat_pull_out =

lemmas nat_pull_in =

lemmas of_int_pull_in =
of_int_numeral of_int_neg_numeral times_divide_eq_left [symmetric]

text ‹Special for @{typ nat}›

definition lift_nat :: "(nat ⇒ nat) ⇒ int ⇒ int"
where
"lift_nat f = int ∘ f ∘ nat"

definition Σ_nat :: "(nat ⇒ nat) ⇒ nat ⇒ nat ⇒ nat" ("Σ⇩ℕ")
where
[summation]: "Σ⇩ℕ f m n = nat (Σ (lift_nat f) (int m) (int n))"

definition pos_id :: "int ⇒ int"
where
"pos_id k = (if k < 0 then 0 else k)"

lemma Σ_pos_id [summation]:
"0 ≤ k ⟹ 0 ≤ l ⟹ Σ (λr. f (pos_id r)) k l = Σ f k l"

lemma [summation]:
"(0::int) ≤ 0"
"(0::int) ≤ 1"
"(0::int) ≤ numeral m"
"(0::int) ≤ int n"
by simp_all

lemma [summation]:
"lift_nat (λn. m) = (λk. int m)"

lemma [summation]:
"lift_nat (λn. n) = pos_id"
by (simp add: lift_nat_def fun_eq_iff pos_id_def)

lemma [summation]:
"lift_nat (λn. f n + g n) = (λk. lift_nat f k + lift_nat g k)"

lemma [summation]:
"lift_nat (λn. m * f n) = (λk. int m * lift_nat f k)"

lemma [summation]:
"lift_nat (λn. f n * m) = (λk. lift_nat f k * int m)"

lemma [summation]:
"lift_nat (λn. f n ^ m) = (λk. lift_nat f k ^ m)"

text ‹Generic conversion›

ML ‹
signature SUMMATION =
sig
val conv: Proof.context -> conv
end

structure Summation : SUMMATION =
struct

val simps2 = @{thms Stirling.simps ffact_0 ffact_Suc nat_simps};
val simpset3 =
@{context}
|> Simplifier.simpset_of;
val simps4 = @{thms of_int_pull_out of_nat_pull_out nat_pull_in};
val simps6 = @{thms of_int_pull_in};

fun conv ctxt =
let
val ctxt1 =
ctxt
|> put_simpset HOL_basic_ss
|> fold Simplifier.add_simp (Named_Theorems.get ctxt @{named_theorems summation})
val ctxt2 =
ctxt
|> put_simpset HOL_basic_ss
val ctxt3 =
ctxt
|> put_simpset simpset3
val ctxt4 =
ctxt
|> put_simpset HOL_basic_ss
val semiring_conv_base = Semiring_Normalizer.semiring_normalize_conv ctxt
val semiring_conv = Conv.arg_conv (Conv.arg1_conv (Conv.arg_conv semiring_conv_base))
else_conv Conv.arg1_conv (Conv.arg_conv semiring_conv_base)
else_conv semiring_conv_base
val ctxt6 =
ctxt
|> put_simpset HOL_basic_ss
in
Simplifier.rewrite ctxt1
then_conv Simplifier.rewrite ctxt2
then_conv Simplifier.rewrite ctxt3
then_conv Simplifier.rewrite ctxt4
then_conv semiring_conv
then_conv Simplifier.rewrite ctxt6
end

end
›

hide_fact (open) nat_simps of_int_pull_out of_int_pull_in

end


# Theory Examples

(* Author: Florian Haftmann, TU Muenchen *)

section ‹Simple examples›

theory Examples
imports Summation_Conversion
begin

ML ‹
Summation.conv @{context}
@{cterm "Σ (λq::rat. q ^ Suc (Suc (Suc 0)) + 3) 0 j"}
›

ML ‹
Summation.conv @{context}
@{cterm "Σ (λx::real. x ^ Suc (Suc (Suc 0)) + 3) 0 j"}
›

ML ‹
Summation.conv @{context}
@{cterm "Σ (λk::int. k ^ Suc (Suc (Suc 0)) + 3) 0 j"}
›

ML ‹
Summation.conv @{context}
@{cterm "Σ⇩ℕ (λn::nat. n ^ Suc (Suc (Suc 0)) + 3) 0 m"}
›

end