# HG changeset patch # User avigad # Date 1247619533 14400 # Node ID df28ead1cf19146afe851e8be1230495018adca7 # Parent 4127b89f48abfc6014996857f94c237e62de6b57 Repairs regarding new Fact.thy. diff -r 4127b89f48ab -r df28ead1cf19 src/HOL/Library/Binomial.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 \ 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 \ '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 "\ = ?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 (\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 (\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)) + (\i\{0\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 "\ = 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 diff -r 4127b89f48ab -r df28ead1cf19 src/HOL/Library/Formal_Power_Series.thy --- 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 "\ = 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 "\ = (- 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 "\ = (- 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 "\ = 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 "\ = (- 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 "\ = (- 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 \ (0::'a::field) \ x / a = y \ 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