Repairs regarding new Fact.thy.
--- a/src/HOL/Library/Binomial.thy Fri Jul 10 12:55:06 2009 -0400
+++ b/src/HOL/Library/Binomial.thy Tue Jul 14 20:58:53 2009 -0400
@@ -243,14 +243,8 @@
ultimately show ?thesis by blast
qed
-lemma fact_setprod: "fact n = setprod id {1 .. n}"
- apply (induct n, simp)
- apply (simp only: fact_Suc atLeastAtMostSuc_conv)
- apply (subst setprod_insert)
- by simp_all
-
lemma pochhammer_fact: "of_nat (fact n) = pochhammer 1 n"
- unfolding fact_setprod
+ unfolding fact_altdef_nat
apply (cases n, simp_all add: of_nat_setprod pochhammer_Suc_setprod)
apply (rule setprod_reindex_cong[where f=Suc])
@@ -347,7 +341,7 @@
assumes kn: "k \<le> n"
shows "(of_nat (n choose k) :: 'a::field_char_0) = of_nat (fact n) / (of_nat (fact k) * of_nat (fact (n - k)))"
using binomial_fact_lemma[OF kn]
- by (simp add: field_simps fact_not_eq_zero of_nat_mult[symmetric])
+ by (simp add: field_simps of_nat_mult[symmetric])
lemma binomial_gbinomial: "of_nat (n choose k) = of_nat n gchoose k"
proof-
@@ -377,7 +371,7 @@
have ?thesis using kn
apply (simp add: binomial_fact[OF kn, where ?'a = 'a]
gbinomial_pochhammer field_simps pochhammer_Suc_setprod)
- apply (simp add: pochhammer_Suc_setprod fact_setprod h of_nat_setprod setprod_timesf[symmetric] eq' del: One_nat_def power_Suc)
+ apply (simp add: pochhammer_Suc_setprod fact_altdef_nat h of_nat_setprod setprod_timesf[symmetric] eq' del: One_nat_def power_Suc)
unfolding setprod_Un_disjoint[OF th0, unfolded eq3, of "of_nat:: nat \<Rightarrow> 'a"] eq[unfolded h]
unfolding mult_assoc[symmetric]
unfolding setprod_timesf[symmetric]
@@ -404,7 +398,7 @@
proof-
have "?r = ((- 1) ^n * pochhammer (- a) n / of_nat (fact n)) * (of_nat n - (- a + of_nat n))"
unfolding gbinomial_pochhammer
- pochhammer_Suc fact_Suc of_nat_mult right_diff_distrib power_Suc
+ pochhammer_Suc fact_Suc_nat of_nat_mult right_diff_distrib power_Suc
by (simp add: field_simps del: of_nat_Suc)
also have "\<dots> = ?l" unfolding gbinomial_pochhammer
by (simp add: ring_simps)
@@ -420,7 +414,7 @@
lemma gbinomial_mult_fact:
"(of_nat (fact (Suc k)) :: 'a) * ((a::'a::field_char_0) gchoose (Suc k)) = (setprod (\<lambda>i. a - of_nat i) {0 .. k})"
unfolding gbinomial_Suc
- by (simp_all add: field_simps del: fact_Suc)
+ by (simp_all add: field_simps del: fact_Suc_nat)
lemma gbinomial_mult_fact':
"((a::'a::field_char_0) gchoose (Suc k)) * (of_nat (fact (Suc k)) :: 'a) = (setprod (\<lambda>i. a - of_nat i) {0 .. k})"
@@ -438,9 +432,9 @@
have "of_nat (fact (Suc k)) * (a gchoose k + (a gchoose (Suc k))) = ((a gchoose Suc h) * of_nat (fact (Suc h)) * of_nat (Suc k)) + (\<Prod>i\<in>{0\<Colon>nat..Suc h}. a - of_nat i)"
unfolding h
- apply (simp add: ring_simps del: fact_Suc)
+ apply (simp add: ring_simps del: fact_Suc_nat)
unfolding gbinomial_mult_fact'
- apply (subst fact_Suc)
+ apply (subst fact_Suc_nat)
unfolding of_nat_mult
apply (subst mult_commute)
unfolding mult_assoc
@@ -455,7 +449,7 @@
by simp
also have "\<dots> = of_nat (fact (Suc k)) * ((a + 1) gchoose (Suc k))"
unfolding gbinomial_mult_fact ..
- finally have ?thesis by (simp del: fact_Suc) }
+ finally have ?thesis by (simp del: fact_Suc_nat) }
ultimately show ?thesis by (cases k, auto)
qed
--- a/src/HOL/Library/Formal_Power_Series.thy Fri Jul 10 12:55:06 2009 -0400
+++ b/src/HOL/Library/Formal_Power_Series.thy Tue Jul 14 20:58:53 2009 -0400
@@ -2514,7 +2514,7 @@
proof-
{fix n
have "?l$n = ?r $ n"
- apply (auto simp add: E_def field_simps power_Suc[symmetric]simp del: fact_Suc of_nat_Suc power_Suc)
+ apply (auto simp add: E_def field_simps power_Suc[symmetric]simp del: fact_Suc_nat of_nat_Suc power_Suc)
by (simp add: of_nat_mult ring_simps)}
then show ?thesis by (simp add: fps_eq_iff)
qed
@@ -2530,8 +2530,8 @@
apply (induct n)
apply simp
unfolding th
- using fact_gt_zero
- apply (simp add: field_simps del: of_nat_Suc fact.simps)
+ using fact_gt_zero_nat
+ apply (simp add: field_simps del: of_nat_Suc fact_Suc_nat)
apply (drule sym)
by (simp add: ring_simps of_nat_mult power_Suc)}
note th' = this
@@ -2697,7 +2697,7 @@
also have "\<dots> = of_nat (n+1) * ((- 1)^(n div 2) * c^Suc n / of_nat (fact (Suc n)))"
using en by (simp add: fps_sin_def)
also have "\<dots> = (- 1)^(n div 2) * c^Suc n * (of_nat (n+1) / (of_nat (Suc n) * of_nat (fact n)))"
- unfolding fact_Suc of_nat_mult
+ unfolding fact_Suc_nat of_nat_mult
by (simp add: field_simps del: of_nat_add of_nat_Suc)
also have "\<dots> = (- 1)^(n div 2) *c^Suc n / of_nat (fact n)"
by (simp add: field_simps del: of_nat_add of_nat_Suc)
@@ -2721,7 +2721,7 @@
also have "\<dots> = of_nat (n+1) * ((- 1)^((n + 1) div 2) * c^Suc n / of_nat (fact (Suc n)))"
using en by (simp add: fps_cos_def)
also have "\<dots> = (- 1)^((n + 1) div 2)*c^Suc n * (of_nat (n+1) / (of_nat (Suc n) * of_nat (fact n)))"
- unfolding fact_Suc of_nat_mult
+ unfolding fact_Suc_nat of_nat_mult
by (simp add: field_simps del: of_nat_add of_nat_Suc)
also have "\<dots> = (- 1)^((n + 1) div 2) * c^Suc n / of_nat (fact n)"
by (simp add: field_simps del: of_nat_add of_nat_Suc)
@@ -2747,9 +2747,6 @@
finally show ?thesis .
qed
-lemma fact_1 [simp]: "fact 1 = 1"
-unfolding One_nat_def fact_Suc by simp
-
lemma divide_eq_iff: "a \<noteq> (0::'a::field) \<Longrightarrow> x / a = y \<longleftrightarrow> x = y * a"
by auto
@@ -2766,7 +2763,7 @@
"fps_sin c $ (n + 2) = - (c * c * fps_sin c $ n / (of_nat(n+1) * of_nat(n+2)))"
unfolding fps_sin_def
apply (cases n, simp)
-apply (simp add: divide_eq_iff eq_divide_iff del: of_nat_Suc fact_Suc)
+apply (simp add: divide_eq_iff eq_divide_iff del: of_nat_Suc fact_Suc_nat)
apply (simp add: of_nat_mult del: of_nat_Suc mult_Suc)
done
@@ -2779,7 +2776,7 @@
lemma fps_cos_nth_add_2:
"fps_cos c $ (n + 2) = - (c * c * fps_cos c $ n / (of_nat(n+1) * of_nat(n+2)))"
unfolding fps_cos_def
-apply (simp add: divide_eq_iff eq_divide_iff del: of_nat_Suc fact_Suc)
+apply (simp add: divide_eq_iff eq_divide_iff del: of_nat_Suc fact_Suc_nat)
apply (simp add: of_nat_mult del: of_nat_Suc mult_Suc)
done