--- a/src/HOL/Binomial.thy Sat Jul 02 15:02:24 2016 +0200
+++ b/src/HOL/Binomial.thy Sat Jul 02 20:22:25 2016 +0200
@@ -14,29 +14,38 @@
subsection \<open>Factorial\<close>
-fun (in semiring_char_0) fact :: "nat \<Rightarrow> 'a"
- where "fact 0 = 1" | "fact (Suc n) = of_nat (Suc n) * fact n"
+definition (in semiring_char_0) fact :: "nat \<Rightarrow> 'a"
+where
+ "fact n = of_nat (\<Prod>{1..n})"
+
+lemma fact_altdef': "fact n = of_nat (\<Prod>{1..n})"
+ by (fact fact_def)
-lemmas fact_Suc = fact.simps(2)
+lemma fact_altdef_nat: "fact n = \<Prod>{1..n}"
+ by (simp add: fact_def)
+
+lemma fact_altdef: "fact n = (\<Prod>i=1..n. of_nat i)"
+ by (simp add: fact_def)
+
+lemma fact_0 [simp]: "fact 0 = 1"
+ by (simp add: fact_def)
lemma fact_1 [simp]: "fact 1 = 1"
- by simp
+ by (simp add: fact_def)
lemma fact_Suc_0 [simp]: "fact (Suc 0) = Suc 0"
- by simp
+ by (simp add: fact_def)
+
+lemma fact_Suc [simp]: "fact (Suc n) = of_nat (Suc n) * fact n"
+ by (simp add: fact_def atLeastAtMostSuc_conv algebra_simps)
lemma of_nat_fact [simp]:
"of_nat (fact n) = fact n"
- by (induct n) (auto simp add: algebra_simps)
+ by (simp add: fact_def)
lemma of_int_fact [simp]:
"of_int (fact n) = fact n"
-proof -
- have "of_int (of_nat (fact n)) = fact n"
- unfolding of_int_of_nat_eq by simp
- then show ?thesis
- by simp
-qed
+ by (simp only: fact_def of_int_of_nat_eq)
lemma fact_reduce: "n > 0 \<Longrightarrow> fact n = of_nat n * fact (n - 1)"
by (cases n) auto
@@ -61,7 +70,7 @@
by (metis of_nat_fact of_nat_le_iff fact_mono_nat)
lemma fact_ge_1 [simp]: "fact n \<ge> (1 :: 'a)"
- by (metis le0 fact.simps(1) fact_mono)
+ by (metis le0 fact_0 fact_mono)
lemma fact_gt_zero [simp]: "fact n > (0 :: 'a)"
using fact_ge_1 less_le_trans zero_less_one by blast
@@ -107,15 +116,6 @@
lemma fact_ge_self: "fact n \<ge> n"
by (cases "n = 0") (simp_all add: dvd_imp_le dvd_fact)
-lemma fact_altdef_nat: "fact n = \<Prod>{1..n}"
- by (induct n) (auto simp: atLeastAtMostSuc_conv)
-
-lemma fact_altdef: "fact n = (\<Prod>i=1..n. of_nat i)"
- by (induct n) (auto simp: atLeastAtMostSuc_conv)
-
-lemma fact_altdef': "fact n = of_nat (\<Prod>{1..n})"
- by (subst fact_altdef_nat [symmetric]) simp
-
lemma fact_dvd: "n \<le> m \<Longrightarrow> fact n dvd (fact m :: 'a :: {semiring_div,linordered_semidom})"
by (induct m) (auto simp: le_Suc_eq)
@@ -164,7 +164,7 @@
lemma fact_numeral: \<comment>\<open>Evaluation for specific numerals\<close>
"fact (numeral k) = (numeral k) * (fact (pred_numeral k))"
- by (metis fact.simps(2) numeral_eq_Suc of_nat_numeral)
+ by (metis fact_Suc numeral_eq_Suc of_nat_numeral)
text \<open>This development is based on the work of Andy Gordon and
@@ -469,49 +469,44 @@
text \<open>See @{url "http://en.wikipedia.org/wiki/Pochhammer_symbol"}\<close>
-definition (in comm_semiring_1) "pochhammer (a :: 'a) n =
- (if n = 0 then 1 else setprod (\<lambda>n. a + of_nat n) {0 .. n - 1})"
+definition (in comm_semiring_1) pochhammer :: "'a \<Rightarrow> nat \<Rightarrow> 'a"
+where
+ "pochhammer (a :: 'a) n = setprod (\<lambda>n. a + of_nat n) {..<n}"
+lemma pochhammer_Suc_setprod:
+ "pochhammer a (Suc n) = setprod (\<lambda>n. a + of_nat n) {..n}"
+ by (simp add: pochhammer_def lessThan_Suc_atMost)
+
lemma pochhammer_0 [simp]: "pochhammer a 0 = 1"
by (simp add: pochhammer_def)
-
+
lemma pochhammer_1 [simp]: "pochhammer a 1 = a"
- by (simp add: pochhammer_def)
-
+ by (simp add: pochhammer_def lessThan_Suc)
+
lemma pochhammer_Suc0 [simp]: "pochhammer a (Suc 0) = a"
- by (simp add: pochhammer_def)
-
-lemma pochhammer_Suc_setprod: "pochhammer a (Suc n) = setprod (\<lambda>n. a + of_nat n) {0 .. n}"
- by (simp add: pochhammer_def)
-
+ by (simp add: pochhammer_def lessThan_Suc)
+
+lemma pochhammer_Suc: "pochhammer a (Suc n) = pochhammer a n * (a + of_nat n)"
+ by (simp add: pochhammer_def lessThan_Suc ac_simps)
+
lemma pochhammer_of_nat: "pochhammer (of_nat x) n = of_nat (pochhammer x n)"
by (simp add: pochhammer_def)
lemma pochhammer_of_int: "pochhammer (of_int x) n = of_int (pochhammer x n)"
by (simp add: pochhammer_def)
-lemma setprod_nat_ivl_Suc: "setprod f {0 .. Suc n} = setprod f {0..n} * f (Suc n)"
+lemma setprod_nat_ivl_Suc: "setprod f {.. Suc n} = setprod f {..n} * f (Suc n)"
proof -
- have "{0..Suc n} = {0..n} \<union> {Suc n}" by auto
+ have "{..Suc n} = {..n} \<union> {Suc n}" by auto
then show ?thesis by (simp add: field_simps)
qed
-lemma setprod_nat_ivl_1_Suc: "setprod f {0 .. Suc n} = f 0 * setprod f {1.. Suc n}"
+lemma setprod_nat_ivl_1_Suc: "setprod f {.. Suc n} = f 0 * setprod f {1.. Suc n}"
proof -
- have "{0..Suc n} = {0} \<union> {1 .. Suc n}" by auto
+ have "{..Suc n} = {0} \<union> {1 .. Suc n}" by auto
then show ?thesis by simp
qed
-
-lemma pochhammer_Suc: "pochhammer a (Suc n) = pochhammer a n * (a + of_nat n)"
-proof (cases n)
- case 0
- then show ?thesis by simp
-next
- case (Suc n)
- show ?thesis unfolding Suc pochhammer_Suc_setprod setprod_nat_ivl_Suc ..
-qed
-
lemma pochhammer_rec: "pochhammer a (Suc n) = a * pochhammer (a + 1) n"
proof (cases "n = 0")
case True
@@ -519,14 +514,14 @@
next
case False
have *: "finite {1 .. n}" "0 \<notin> {1 .. n}" by auto
- have eq: "insert 0 {1 .. n} = {0..n}" by auto
- have **: "(\<Prod>n\<in>{1::nat..n}. a + of_nat n) = (\<Prod>n\<in>{0::nat..n - 1}. a + 1 + of_nat n)"
+ have eq: "insert 0 {1 .. n} = {..n}" by auto
+ have **: "(\<Prod>n\<in>{1..n}. a + of_nat n) = (\<Prod>n\<in>{..<n}. a + 1 + of_nat n)"
apply (rule setprod.reindex_cong [where l = Suc])
using False
- apply (auto simp add: fun_eq_iff field_simps)
+ apply (auto simp add: fun_eq_iff field_simps image_Suc_lessThan)
done
show ?thesis
- apply (simp add: pochhammer_def)
+ apply (simp add: pochhammer_def lessThan_Suc_atMost)
unfolding setprod.insert [OF *, unfolded eq]
using ** apply (simp add: field_simps)
done
@@ -545,27 +540,15 @@
qed simp_all
lemma pochhammer_fact: "fact n = pochhammer 1 n"
- unfolding fact_altdef
- apply (cases n)
- apply (simp_all add: pochhammer_Suc_setprod)
+ apply (auto simp add: pochhammer_def fact_altdef)
apply (rule setprod.reindex_cong [where l = Suc])
- apply (auto simp add: fun_eq_iff)
+ apply (auto simp add: image_Suc_lessThan)
done
lemma pochhammer_of_nat_eq_0_lemma:
assumes "k > n"
shows "pochhammer (- (of_nat n :: 'a:: idom)) k = 0"
-proof (cases "n = 0")
- case True
- then show ?thesis
- using assms by (cases k) (simp_all add: pochhammer_rec)
-next
- case False
- from assms obtain h where "k = Suc h" by (cases k) auto
- then show ?thesis
- by (simp add: pochhammer_Suc_setprod)
- (metis Suc_leI Suc_le_mono assms atLeastAtMost_iff less_eq_nat.simps(1))
-qed
+ using assms by (auto simp add: pochhammer_def)
lemma pochhammer_of_nat_eq_0_lemma':
assumes kn: "k \<le> n"
@@ -589,11 +572,7 @@
by (auto simp add: not_le[symmetric])
lemma pochhammer_eq_0_iff: "pochhammer a n = (0::'a::field_char_0) \<longleftrightarrow> (\<exists>k < n. a = - of_nat k)"
- apply (auto simp add: pochhammer_of_nat_eq_0_iff)
- apply (cases n)
- apply (auto simp add: pochhammer_def algebra_simps group_add_class.eq_neg_iff_add_eq_0)
- apply (metis leD not_less_eq)
- done
+ by (auto simp add: pochhammer_def eq_neg_iff_add_eq_0)
lemma pochhammer_eq_0_mono:
"pochhammer a n = (0::'a::field_char_0) \<Longrightarrow> m \<ge> n \<Longrightarrow> pochhammer a m = 0"
@@ -610,8 +589,8 @@
then show ?thesis by simp
next
case (Suc h)
- have eq: "((- 1) ^ Suc h :: 'a) = (\<Prod>i=0..h. - 1)"
- using setprod_constant[where A="{0 .. h}" and y="- 1 :: 'a"]
+ have eq: "((- 1) ^ Suc h :: 'a) = (\<Prod>i\<le>h. - 1)"
+ using setprod_constant[where A="{.. h}" and y="- 1 :: 'a"]
by auto
show ?thesis
unfolding Suc pochhammer_Suc_setprod eq setprod.distrib[symmetric]
@@ -650,7 +629,7 @@
lemma pochhammer_times_pochhammer_half:
fixes z :: "'a :: field_char_0"
- shows "pochhammer z (Suc n) * pochhammer (z + 1/2) (Suc n) = (\<Prod>k=0..2*n+1. z + of_nat k / 2)"
+ shows "pochhammer z (Suc n) * pochhammer (z + 1/2) (Suc n) = (\<Prod>k\<le>2*n+1. z + of_nat k / 2)"
proof (induction n)
case (Suc n)
define n' where "n' = Suc n"
@@ -661,7 +640,7 @@
also have "?A = (z + of_nat (Suc (2 * n + 1)) / 2) * (z + of_nat (Suc (Suc (2 * n + 1))) / 2)"
(is "_ = ?A") by (simp add: field_simps n'_def)
also note Suc[folded n'_def]
- also have "(\<Prod>k = 0..2 * n + 1. z + of_nat k / 2) * ?A = (\<Prod>k = 0..2 * Suc n + 1. z + of_nat k / 2)"
+ also have "(\<Prod>k\<le>2 * n + 1. z + of_nat k / 2) * ?A = (\<Prod>k\<le>2 * Suc n + 1. z + of_nat k / 2)"
by (simp add: setprod_nat_ivl_Suc)
finally show ?case by (simp add: n'_def)
qed (simp add: setprod_nat_ivl_Suc)
@@ -699,8 +678,12 @@
subsection\<open>Generalized binomial coefficients\<close>
definition (in field_char_0) gbinomial :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixl "gchoose" 65)
- where "a gchoose n =
- (if n = 0 then 1 else (setprod (\<lambda>i. a - of_nat i) {0 .. n - 1}) / (fact n))"
+where
+ "a gchoose n = setprod (\<lambda>i. a - of_nat i) {..<n} / fact n"
+
+lemma gbinomial_Suc:
+ "a gchoose (Suc k) = setprod (\<lambda>i. a - of_nat i) {..k} / fact (Suc k)"
+ by (simp add: gbinomial_def lessThan_Suc_atMost)
lemma gbinomial_0 [simp]: "a gchoose 0 = 1" "0 gchoose (Suc n) = 0"
by (simp_all add: gbinomial_def)
@@ -711,7 +694,7 @@
then show ?thesis by simp
next
case False
- then have eq: "(- 1) ^ n = (\<Prod>i = 0..n - 1. - 1)"
+ then have eq: "(- 1) ^ n = (\<Prod>i<n. - 1)"
by (auto simp add: setprod_constant)
from False show ?thesis
by (simp add: pochhammer_def gbinomial_def field_simps
@@ -740,9 +723,9 @@
{ assume kn: "k \<le> n" and k0: "k\<noteq> 0"
from k0 obtain h where h: "k = Suc h" by (cases k) auto
from h
- have eq:"(- 1 :: 'a) ^ k = setprod (\<lambda>i. - 1) {0..h}"
+ have eq:"(- 1 :: 'a) ^ k = setprod (\<lambda>i. - 1) {..h}"
by (subst setprod_constant) auto
- have eq': "(\<Prod>i\<in>{0..h}. of_nat n + - (of_nat i :: 'a)) = (\<Prod>i\<in>{n - h..n}. of_nat i)"
+ have eq': "(\<Prod>i\<le>h. of_nat n + - (of_nat i :: 'a)) = (\<Prod>i\<in>{n - h..n}. of_nat i)"
using h kn
by (intro setprod.reindex_bij_witness[where i="op - n" and j="op - n"])
(auto simp: of_nat_diff)
@@ -770,10 +753,10 @@
qed
lemma gbinomial_1[simp]: "a gchoose 1 = a"
- by (simp add: gbinomial_def)
+ by (simp add: gbinomial_def lessThan_Suc)
lemma gbinomial_Suc0[simp]: "a gchoose (Suc 0) = a"
- by (simp add: gbinomial_def)
+ by (simp add: gbinomial_def lessThan_Suc)
lemma gbinomial_mult_1:
fixes a :: "'a :: field_char_0"
@@ -783,7 +766,7 @@
have "?r = ((- 1) ^n * pochhammer (- a) n / (fact n)) * (of_nat n - (- a + of_nat n))"
unfolding gbinomial_pochhammer
pochhammer_Suc right_diff_distrib power_Suc
- apply (simp del: of_nat_Suc fact.simps)
+ apply (simp del: of_nat_Suc fact_Suc)
apply (auto simp add: field_simps simp del: of_nat_Suc)
done
also have "\<dots> = ?l" unfolding gbinomial_pochhammer
@@ -796,20 +779,16 @@
shows "(a gchoose n) * a = of_nat n * (a gchoose n) + of_nat (Suc n) * (a gchoose (Suc n))"
by (simp add: mult.commute gbinomial_mult_1)
-lemma gbinomial_Suc:
- "a gchoose (Suc k) = (setprod (\<lambda>i. a - of_nat i) {0 .. k}) / (fact (Suc k))"
- by (simp add: gbinomial_def)
-
lemma gbinomial_mult_fact:
fixes a :: "'a::field_char_0"
shows
"fact (Suc k) * (a gchoose (Suc k)) =
- (setprod (\<lambda>i. a - of_nat i) {0 .. k})"
- by (simp_all add: gbinomial_Suc field_simps del: fact.simps)
+ (setprod (\<lambda>i. a - of_nat i) {.. k})"
+ by (simp_all add: gbinomial_Suc field_simps del: fact_Suc)
lemma gbinomial_mult_fact':
fixes a :: "'a::field_char_0"
- shows "(a gchoose (Suc k)) * fact (Suc k) = (setprod (\<lambda>i. a - of_nat i) {0 .. k})"
+ shows "(a gchoose (Suc k)) * fact (Suc k) = (setprod (\<lambda>i. a - of_nat i) {.. k})"
using gbinomial_mult_fact[of k a]
by (subst mult.commute)
@@ -821,36 +800,37 @@
then show ?thesis by simp
next
case (Suc h)
- have eq0: "(\<Prod>i\<in>{1..k}. (a + 1) - of_nat i) = (\<Prod>i\<in>{0..h}. a - of_nat i)"
+ have eq0: "(\<Prod>i\<in>{1..k}. (a + 1) - of_nat i) = (\<Prod>i\<in>{..h}. a - of_nat i)"
apply (rule setprod.reindex_cong [where l = Suc])
using Suc
- apply auto
+ apply (auto simp add: image_Suc_atMost)
done
have "fact (Suc k) * (a gchoose k + (a gchoose (Suc k))) =
(a gchoose Suc h) * (fact (Suc (Suc h))) +
(a gchoose Suc (Suc h)) * (fact (Suc (Suc h)))"
- by (simp add: Suc field_simps del: fact.simps)
+ by (simp add: Suc field_simps del: fact_Suc)
also have "... = (a gchoose Suc h) * of_nat (Suc (Suc h) * fact (Suc h)) +
- (\<Prod>i = 0..Suc h. a - of_nat i)"
- by (metis fact.simps(2) gbinomial_mult_fact' of_nat_fact of_nat_id)
+ (\<Prod>i\<le>Suc h. a - of_nat i)"
+ by (metis fact_Suc gbinomial_mult_fact' of_nat_fact of_nat_id)
also have "... = (fact (Suc h) * (a gchoose Suc h)) * of_nat (Suc (Suc h)) +
- (\<Prod>i = 0..Suc h. a - of_nat i)"
- by (simp only: fact.simps(2) mult.commute mult.left_commute of_nat_fact of_nat_id of_nat_mult)
- also have "... = of_nat (Suc (Suc h)) * (\<Prod>i = 0..h. a - of_nat i) +
- (\<Prod>i = 0..Suc h. a - of_nat i)"
+ (\<Prod>i\<le>Suc h. a - of_nat i)"
+ by (simp only: fact_Suc mult.commute mult.left_commute of_nat_fact of_nat_id of_nat_mult)
+ also have "... = of_nat (Suc (Suc h)) * (\<Prod>i\<le>h. a - of_nat i) +
+ (\<Prod>i\<le>Suc h. a - of_nat i)"
by (metis gbinomial_mult_fact mult.commute)
- also have "... = (\<Prod>i = 0..Suc h. a - of_nat i) +
- (of_nat h * (\<Prod>i = 0..h. a - of_nat i) + 2 * (\<Prod>i = 0..h. a - of_nat i))"
+ also have "... = (\<Prod>i\<le>Suc h. a - of_nat i) +
+ (of_nat h * (\<Prod>i\<le>h. a - of_nat i) + 2 * (\<Prod>i\<le>h. a - of_nat i))"
by (simp add: field_simps)
also have "... =
- ((a gchoose Suc h) * (fact (Suc h)) * of_nat (Suc k)) + (\<Prod>i\<in>{0::nat..Suc h}. a - of_nat i)"
+ ((a gchoose Suc h) * (fact (Suc h)) * of_nat (Suc k)) + (\<Prod>i\<in>{..Suc h}. a - of_nat i)"
unfolding gbinomial_mult_fact'
by (simp add: comm_semiring_class.distrib field_simps Suc)
- also have "\<dots> = (\<Prod>i\<in>{0..h}. a - of_nat i) * (a + 1)"
+ also have "\<dots> = (\<Prod>i\<in>{..h}. a - of_nat i) * (a + 1)"
unfolding gbinomial_mult_fact' setprod_nat_ivl_Suc
+ atMost_Suc
by (simp add: field_simps Suc)
- also have "\<dots> = (\<Prod>i\<in>{0..k}. (a + 1) - of_nat i)"
- using eq0
+ also have "\<dots> = (\<Prod>i\<in>{..k}. (a + 1) - of_nat i)"
+ using eq0 setprod_nat_ivl_1_Suc
by (simp add: Suc setprod_nat_ivl_1_Suc)
also have "\<dots> = (fact (Suc k)) * ((a + 1) gchoose (Suc k))"
unfolding gbinomial_mult_fact ..
@@ -1024,12 +1004,12 @@
proof (cases b)
case (Suc b)
hence "((a + 1) gchoose (Suc (Suc b))) =
- (\<Prod>i = 0..Suc b. a + (1 - of_nat i)) / fact (b + 2)"
- by (simp add: field_simps gbinomial_def)
- also have "(\<Prod>i = 0..Suc b. a + (1 - of_nat i)) = (a + 1) * (\<Prod>i = 0..b. a - of_nat i)"
- by (simp add: setprod_nat_ivl_1_Suc setprod_shift_bounds_cl_Suc_ivl)
+ (\<Prod>i\<le>Suc b. a + (1 - of_nat i)) / fact (b + 2)"
+ by (simp add: field_simps gbinomial_def lessThan_Suc_atMost)
+ also have "(\<Prod>i\<le>Suc b. a + (1 - of_nat i)) = (a + 1) * (\<Prod>i\<le>b. a - of_nat i)"
+ by (simp add: setprod_nat_ivl_1_Suc setprod_shift_bounds_cl_Suc_ivl atLeast0AtMost)
also have "... / fact (b + 2) = (a + 1) / of_nat (Suc (Suc b)) * (a gchoose Suc b)"
- by (simp_all add: gbinomial_def setprod_nat_ivl_1_Suc setprod_shift_bounds_cl_Suc_ivl)
+ by (simp_all add: gbinomial_def setprod_nat_ivl_1_Suc setprod_shift_bounds_cl_Suc_ivl lessThan_Suc_atMost)
finally show ?thesis by (simp add: Suc field_simps del: of_nat_Suc)
qed simp
@@ -1038,12 +1018,12 @@
proof (cases b)
case (Suc b)
hence "((a + 1) gchoose (Suc (Suc b))) =
- (\<Prod>i = 0..Suc b. a + (1 - of_nat i)) / fact (b + 2)"
- by (simp add: field_simps gbinomial_def)
- also have "(\<Prod>i = 0..Suc b. a + (1 - of_nat i)) = (a + 1) * (\<Prod>i = 0..b. a - of_nat i)"
+ (\<Prod>i\<le>Suc b. a + (1 - of_nat i)) / fact (b + 2)"
+ by (simp add: field_simps gbinomial_def lessThan_Suc_atMost)
+ also have "(\<Prod>i\<le>Suc b. a + (1 - of_nat i)) = (a + 1) * (\<Prod>i = 0..b. a - of_nat i)"
by (simp add: setprod_nat_ivl_1_Suc setprod_shift_bounds_cl_Suc_ivl)
also have "... / fact (b + 2) = (a + 1) / of_nat (Suc (Suc b)) * (a gchoose Suc b)"
- by (simp_all add: gbinomial_def setprod_nat_ivl_1_Suc setprod_shift_bounds_cl_Suc_ivl)
+ by (simp_all add: gbinomial_def setprod_nat_ivl_1_Suc setprod_shift_bounds_cl_Suc_ivl lessThan_Suc_atMost atLeast0AtMost)
finally show ?thesis by (simp add: Suc)
qed simp
@@ -1379,8 +1359,7 @@
apply (case_tac "k = 0")
apply auto
apply (case_tac "k = Suc n")
- apply auto
- apply (metis Suc_le_eq fact.cases le_Suc_eq le_eq_less_or_eq)
+ apply (auto simp add: le_Suc_eq elim: lessE)
done
lemma card_UNION:
@@ -1579,15 +1558,20 @@
finally show ?thesis .
qed
+lemma setprod_lessThan_fold_atLeastAtMost_nat:
+ "setprod f {..<Suc n} = fold_atLeastAtMost_nat (times \<circ> f) 0 n 1"
+ by (simp add: lessThan_Suc_atMost atLeast0AtMost [symmetric] setprod_atLeastAtMost_code comp_def)
+
+
lemma pochhammer_code [code]:
"pochhammer a n = (if n = 0 then 1 else
fold_atLeastAtMost_nat (\<lambda>n acc. (a + of_nat n) * acc) 0 (n - 1) 1)"
- by (simp add: setprod_atLeastAtMost_code pochhammer_def)
+ by (cases n) (simp_all add: pochhammer_def setprod_lessThan_fold_atLeastAtMost_nat comp_def)
lemma gbinomial_code [code]:
"a gchoose n = (if n = 0 then 1 else
fold_atLeastAtMost_nat (\<lambda>n acc. (a - of_nat n) * acc) 0 (n - 1) 1 / fact n)"
- by (simp add: setprod_atLeastAtMost_code gbinomial_def)
+ by (cases n) (simp_all add: gbinomial_def setprod_lessThan_fold_atLeastAtMost_nat comp_def)
(*TODO: This code equation breaks Scala code generation in HOL-Codegenerator_Test. We have to figure out why and how to prevent that. *)
--- a/src/HOL/Library/Formal_Power_Series.thy Sat Jul 02 15:02:24 2016 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy Sat Jul 02 20:22:25 2016 +0200
@@ -3700,7 +3700,7 @@
proof -
have "?l$n = ?r $ n" for n
apply (auto simp add: E_def field_simps power_Suc[symmetric]
- simp del: fact.simps of_nat_Suc power_Suc)
+ simp del: fact_Suc of_nat_Suc power_Suc)
apply (simp add: of_nat_mult field_simps)
done
then show ?thesis
@@ -4154,7 +4154,7 @@
case False
with kn have kn': "k < n"
by simp
- have m1nk: "?m1 n = setprod (\<lambda>i. - 1) {0..m}" "?m1 k = setprod (\<lambda>i. - 1) {0..h}"
+ have m1nk: "?m1 n = setprod (\<lambda>i. - 1) {..m}" "?m1 k = setprod (\<lambda>i. - 1) {0..h}"
by (simp_all add: setprod_constant m h)
have bnz0: "pochhammer (b - of_nat n + 1) k \<noteq> 0"
using bn0 kn
@@ -4163,27 +4163,19 @@
apply (erule_tac x= "n - ka - 1" in allE)
apply (auto simp add: algebra_simps of_nat_diff)
done
- have eq1: "setprod (\<lambda>k. (1::'a) + of_nat m - of_nat k) {0 .. h} =
+ have eq1: "setprod (\<lambda>k. (1::'a) + of_nat m - of_nat k) {..h} =
setprod of_nat {Suc (m - h) .. Suc m}"
using kn' h m
by (intro setprod.reindex_bij_witness[where i="\<lambda>k. Suc m - k" and j="\<lambda>k. Suc m - k"])
(auto simp: of_nat_diff)
-
have th1: "(?m1 k * ?p (of_nat n) k) / ?f n = 1 / of_nat(fact (n - k))"
unfolding m1nk
- unfolding m h pochhammer_Suc_setprod
- apply (simp add: field_simps del: fact_Suc)
- unfolding fact_altdef id_def
- unfolding of_nat_setprod
- unfolding setprod.distrib[symmetric]
- apply auto
- unfolding eq1
- apply (subst setprod.union_disjoint[symmetric])
- apply (auto)
- apply (rule setprod.cong)
- apply auto
+ apply (simp add: field_simps m h pochhammer_Suc_setprod del: fact_Suc)
+ apply (simp add: fact_altdef id_def atLeast0AtMost setprod.distrib [symmetric] eq1)
+ apply (subst setprod.union_disjoint [symmetric])
+ apply (auto intro!: setprod.cong)
done
- have th20: "?m1 n * ?p b n = setprod (\<lambda>i. b - of_nat i) {0..m}"
+ have th20: "?m1 n * ?p b n = setprod (\<lambda>i. b - of_nat i) {..m}"
unfolding m1nk
unfolding m h pochhammer_Suc_setprod
unfolding setprod.distrib[symmetric]
@@ -4216,7 +4208,10 @@
by (simp add: field_simps)
also have "\<dots> = b gchoose (n - k)"
unfolding th1 th2
- using kn' by (simp add: gbinomial_def)
+ using kn' apply (simp add: gbinomial_def atLeast0AtMost)
+ apply (rule setprod.cong)
+ apply auto
+ done
finally show ?thesis by simp
qed
qed
--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Sat Jul 02 15:02:24 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Sat Jul 02 20:22:25 2016 +0200
@@ -5906,7 +5906,7 @@
lemma bb: "Suc n choose k = (n choose k) + (if k = 0 then 0 else (n choose (k - 1)))"
- by (simp add: Binomial.binomial.simps)
+ by (cases k) simp_all
proposition higher_deriv_mult:
fixes z::complex
@@ -5924,7 +5924,7 @@
have sumeq: "(\<Sum>i = 0..n.
of_nat (n choose i) * (deriv ((deriv ^^ i) f) z * (deriv ^^ (n - i)) g z + deriv ((deriv ^^ (n - i)) g) z * (deriv ^^ i) f z)) =
g z * deriv ((deriv ^^ n) f) z + (\<Sum>i = 0..n. (deriv ^^ i) f z * (of_nat (Suc n choose i) * (deriv ^^ (Suc n - i)) g z))"
- apply (simp add: bb distrib_right algebra_simps setsum.distrib)
+ apply (simp add: bb algebra_simps setsum.distrib)
apply (subst (4) setsum_Suc_reindex)
apply (auto simp: algebra_simps Suc_diff_le intro: setsum.cong)
done
--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Sat Jul 02 15:02:24 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Sat Jul 02 20:22:25 2016 +0200
@@ -1106,19 +1106,19 @@
((fact(Suc n)) *(f(Suc n) u *(z-u) ^ n)) / (fact n) +
((fact(Suc n)) *(f(Suc(Suc n)) u *((z-u) *(z-u) ^ n)) / (fact(Suc n))) -
((fact(Suc n)) *(f(Suc n) u *(of_nat(Suc n) *(z-u) ^ n))) / (fact(Suc n))"
- by (simp add: algebra_simps del: fact.simps)
+ by (simp add: algebra_simps del: fact_Suc)
also have "... = ((fact (Suc n)) * (f (Suc n) u * (z-u) ^ n)) / (fact n) +
(f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n)) -
(f (Suc n) u * ((1 + of_nat n) * (z-u) ^ n))"
- by (simp del: fact.simps)
+ by (simp del: fact_Suc)
also have "... = (of_nat (Suc n) * (f (Suc n) u * (z-u) ^ n)) +
(f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n)) -
(f (Suc n) u * ((1 + of_nat n) * (z-u) ^ n))"
- by (simp only: fact.simps of_nat_mult ac_simps) simp
+ by (simp only: fact_Suc of_nat_mult ac_simps) simp
also have "... = f (Suc (Suc n)) u * ((z-u) * (z-u) ^ n)"
by (simp add: algebra_simps)
finally show ?thesis
- by (simp add: mult_left_cancel [where c = "(fact (Suc n))", THEN iffD1] del: fact.simps)
+ by (simp add: mult_left_cancel [where c = "(fact (Suc n))", THEN iffD1] del: fact_Suc)
qed
finally show ?case .
qed
--- a/src/HOL/Multivariate_Analysis/Gamma.thy Sat Jul 02 15:02:24 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Gamma.thy Sat Jul 02 20:22:25 2016 +0200
@@ -512,9 +512,10 @@
by (intro setprod.cong[OF refl], subst exp_Ln) (auto simp: field_simps plus_of_nat_eq_0_imp)
also have "... = (\<Prod>k=1..n. z + k) / fact n" unfolding fact_altdef
by (subst setprod_dividef [symmetric]) (simp_all add: field_simps)
- also from assms have "z * ... = (\<Prod>k=0..n. z + k) / fact n"
+ also from assms have "z * ... = (\<Prod>k\<le>n. z + k) / fact n"
by (cases n) (simp_all add: setprod_nat_ivl_1_Suc)
- also have "(\<Prod>k=0..n. z + k) = pochhammer z (Suc n)" unfolding pochhammer_def by simp
+ also have "(\<Prod>k\<le>n. z + k) = pochhammer z (Suc n)" unfolding pochhammer_def
+ by (simp add: lessThan_Suc_atMost)
also have "of_nat n powr z / (pochhammer z (Suc n) / fact n) = Gamma_series z n"
unfolding Gamma_series_def using assms by (simp add: divide_simps powr_def Ln_of_nat)
finally show ?thesis .
@@ -999,7 +1000,7 @@
hence "z \<noteq> - of_nat n" for n by auto
from rGamma_series_aux[OF this] show ?thesis
by (simp add: rGamma_series_def[abs_def] fact_altdef pochhammer_Suc_setprod
- exp_def of_real_def[symmetric] suminf_def sums_def[abs_def])
+ exp_def of_real_def[symmetric] suminf_def sums_def[abs_def] atLeast0AtMost)
qed (insert rGamma_eq_zero_iff[of z], simp_all add: rGamma_series_nonpos_Ints_LIMSEQ)
lemma Gamma_series_LIMSEQ [tendsto_intros]:
@@ -1364,7 +1365,7 @@
pochhammer' = \<lambda>a n. \<Prod>n = 0..n. a + of_nat n
in (\<lambda>n. pochhammer' z n / (fact' n * exp (z * ln (real_of_nat n) *\<^sub>R 1))) \<longlonglongrightarrow> rGamma z"
by (simp add: fact_altdef pochhammer_Suc_setprod rGamma_series_def [abs_def] exp_def
- of_real_def [symmetric] suminf_def sums_def [abs_def])
+ of_real_def [symmetric] suminf_def sums_def [abs_def] atLeast0AtMost)
qed
end
@@ -1497,7 +1498,7 @@
pochhammer' = \<lambda>a n. \<Prod>n = 0..n. a + of_nat n
in (\<lambda>n. pochhammer' x n / (fact' n * exp (x * ln (real_of_nat n) *\<^sub>R 1))) \<longlonglongrightarrow> rGamma x"
by (simp add: fact_altdef pochhammer_Suc_setprod rGamma_series_def [abs_def] exp_def
- of_real_def [symmetric] suminf_def sums_def [abs_def])
+ of_real_def [symmetric] suminf_def sums_def [abs_def] atLeast0AtMost)
qed
end
@@ -2424,7 +2425,7 @@
setprod_inversef[symmetric] divide_inverse)
also have "(\<Prod>k=1..n. (1 + z / of_nat k)) = pochhammer (z + 1) n / fact n"
by (cases n) (simp_all add: pochhammer_def fact_altdef setprod_shift_bounds_cl_Suc_ivl
- setprod_dividef[symmetric] divide_simps add_ac)
+ setprod_dividef[symmetric] divide_simps add_ac atLeast0AtMost lessThan_Suc_atMost)
also have "z * \<dots> = pochhammer z (Suc n) / fact n" by (simp add: pochhammer_rec)
finally show "?r n = Gamma_series_euler' z n / Gamma_series z n" by simp
qed
--- a/src/HOL/Multivariate_Analysis/Generalised_Binomial_Theorem.thy Sat Jul 02 15:02:24 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Generalised_Binomial_Theorem.thy Sat Jul 02 20:22:25 2016 +0200
@@ -27,11 +27,12 @@
show "eventually (\<lambda>n. ?f n = (a gchoose n) /(a gchoose Suc n)) sequentially"
proof eventually_elim
fix n :: nat assume n: "n > 0"
- let ?P = "\<Prod>i = 0..n - 1. a - of_nat i"
+ let ?P = "\<Prod>i<n. a - of_nat i"
from n have "(a gchoose n) / (a gchoose Suc n) = (of_nat (Suc n) :: 'a) *
- (?P / (\<Prod>i = 0..n. a - of_nat i))" by (simp add: gbinomial_def)
- also from n have "(\<Prod>i = 0..n. a - of_nat i) = ?P * (a - of_nat n)"
- by (cases n) (simp_all add: setprod_nat_ivl_Suc)
+ (?P / (\<Prod>i\<le>n. a - of_nat i))"
+ by (simp add: gbinomial_def lessThan_Suc_atMost)
+ also from n have "(\<Prod>i\<le>n. a - of_nat i) = ?P * (a - of_nat n)"
+ by (cases n) (simp_all add: setprod_nat_ivl_Suc lessThan_Suc_atMost)
also have "?P / \<dots> = (?P / ?P) / (a - of_nat n)" by (rule divide_divide_eq_left[symmetric])
also from assms have "?P / ?P = 1" by auto
also have "of_nat (Suc n) * (1 / (a - of_nat n)) =
--- a/src/HOL/NthRoot.thy Sat Jul 02 15:02:24 2016 +0200
+++ b/src/HOL/NthRoot.thy Sat Jul 02 20:22:25 2016 +0200
@@ -655,7 +655,7 @@
{ fix n :: nat assume "2 < n"
have "1 + (real (n - 1) * n) / 2 * x n^2 = 1 + of_nat (n choose 2) * x n^2"
using \<open>2 < n\<close> unfolding gbinomial_def binomial_gbinomial
- by (simp add: atLeast0AtMost atMost_Suc field_simps of_nat_diff numeral_2_eq_2)
+ by (simp add: atLeast0AtMost lessThan_Suc field_simps of_nat_diff numeral_2_eq_2)
also have "\<dots> \<le> (\<Sum>k\<in>{0, 2}. of_nat (n choose k) * x n^k)"
by (simp add: x_def)
also have "\<dots> \<le> (\<Sum>k=0..n. of_nat (n choose k) * x n^k)"
@@ -692,7 +692,8 @@
(simp_all add: at_infinity_eq_at_top_bot)
{ fix n :: nat assume "1 < n"
have "1 + x n * n = 1 + of_nat (n choose 1) * x n^1"
- using \<open>1 < n\<close> unfolding gbinomial_def binomial_gbinomial by simp
+ using \<open>1 < n\<close> unfolding gbinomial_def binomial_gbinomial
+ by (simp add: lessThan_Suc)
also have "\<dots> \<le> (\<Sum>k\<in>{0, 1}. of_nat (n choose k) * x n^k)"
by (simp add: x_def)
also have "\<dots> \<le> (\<Sum>k=0..n. of_nat (n choose k) * x n^k)"
--- a/src/HOL/Transcendental.thy Sat Jul 02 15:02:24 2016 +0200
+++ b/src/HOL/Transcendental.thy Sat Jul 02 20:22:25 2016 +0200
@@ -1758,7 +1758,7 @@
by (rule mult_mono)
(rule mult_mono, simp_all add: power_le_one a b)
hence "inverse (fact (n + 2)) * x ^ (n + 2) \<le> (x\<^sup>2/2) * ((1/2)^n)"
- unfolding power_add by (simp add: ac_simps del: fact.simps) }
+ unfolding power_add by (simp add: ac_simps del: fact_Suc) }
note aux1 = this
have "(\<lambda>n. x\<^sup>2 / 2 * (1 / 2) ^ n) sums (x\<^sup>2 / 2 * (1 / (1 - 1 / 2)))"
by (intro sums_mult geometric_sums, simp)
@@ -3319,7 +3319,7 @@
lemma cos_two_less_zero [simp]:
"cos 2 < (0::real)"
proof -
- note fact.simps(2) [simp del]
+ note fact_Suc [simp del]
from sums_minus [OF cos_paired]
have *: "(\<lambda>n. - ((- 1) ^ n * 2 ^ (2 * n) / fact (2 * n))) sums - cos (2::real)"
by simp
@@ -3335,7 +3335,7 @@
have "(4::real) * (fact (?six4d)) < (Suc (Suc (?six4d)) * fact (Suc (?six4d)))"
unfolding of_nat_mult by (rule mult_strict_mono) (simp_all add: fact_less_mono)
then have "(4::real) * (fact (?six4d)) < (fact (Suc (Suc (?six4d))))"
- by (simp only: fact.simps(2) [of "Suc (?six4d)"] of_nat_mult of_nat_fact)
+ by (simp only: fact_Suc [of "Suc (?six4d)"] of_nat_mult of_nat_fact)
then have "(4::real) * inverse (fact (Suc (Suc (?six4d)))) < inverse (fact (?six4d))"
by (simp add: inverse_eq_divide less_divide_eq)
}
--- a/src/HOL/ex/Sum_of_Powers.thy Sat Jul 02 15:02:24 2016 +0200
+++ b/src/HOL/ex/Sum_of_Powers.thy Sat Jul 02 20:22:25 2016 +0200
@@ -147,7 +147,7 @@
lemma binomial_unroll:
"n > 0 \<Longrightarrow> (n choose k) = (if k = 0 then 1 else (n - 1) choose (k - 1) + ((n - 1) choose k))"
-by (cases n) (auto simp add: binomial.simps(2))
+ by (auto simp add: gr0_conv_Suc)
lemma setsum_unroll:
"(\<Sum>k\<le>n::nat. f k) = (if n = 0 then f 0 else f n + (\<Sum>k\<le>n - 1. f k))"
@@ -157,7 +157,7 @@
"n > 0 \<Longrightarrow> bernoulli n = - 1 / (real n + 1) * (\<Sum>k\<le>n - 1. real (n + 1 choose k) * bernoulli k)"
by (cases n) (simp add: bernoulli.simps One_nat_def)+
-lemmas unroll = binomial.simps(1) binomial_unroll
+lemmas unroll = binomial_unroll
bernoulli.simps(1) bernoulli_unroll setsum_unroll bernpoly_def
lemma sum_of_squares: "(\<Sum>k\<le>n::nat. k ^ 2) = (2 * n ^ 3 + 3 * n ^ 2 + n) / 6"