Repairs regarding new Fact.thy.
authoravigad
Tue Jul 14 20:58:53 2009 -0400 (2009-07-14)
changeset 32042df28ead1cf19
parent 32038 4127b89f48ab
child 32043 a4213e1b4cc7
Repairs regarding new Fact.thy.
src/HOL/Library/Binomial.thy
src/HOL/Library/Formal_Power_Series.thy
     1.1 --- a/src/HOL/Library/Binomial.thy	Fri Jul 10 12:55:06 2009 -0400
     1.2 +++ b/src/HOL/Library/Binomial.thy	Tue Jul 14 20:58:53 2009 -0400
     1.3 @@ -243,14 +243,8 @@
     1.4  ultimately show ?thesis by blast
     1.5  qed
     1.6  
     1.7 -lemma fact_setprod: "fact n = setprod id {1 .. n}"
     1.8 -  apply (induct n, simp)
     1.9 -  apply (simp only: fact_Suc atLeastAtMostSuc_conv)
    1.10 -  apply (subst setprod_insert)
    1.11 -  by simp_all
    1.12 -
    1.13  lemma pochhammer_fact: "of_nat (fact n) = pochhammer 1 n"
    1.14 -  unfolding fact_setprod
    1.15 +  unfolding fact_altdef_nat
    1.16    
    1.17    apply (cases n, simp_all add: of_nat_setprod pochhammer_Suc_setprod)
    1.18    apply (rule setprod_reindex_cong[where f=Suc])
    1.19 @@ -347,7 +341,7 @@
    1.20    assumes kn: "k \<le> n" 
    1.21    shows "(of_nat (n choose k) :: 'a::field_char_0) = of_nat (fact n) / (of_nat (fact k) * of_nat (fact (n - k)))"
    1.22    using binomial_fact_lemma[OF kn]
    1.23 -  by (simp add: field_simps fact_not_eq_zero of_nat_mult[symmetric])
    1.24 +  by (simp add: field_simps of_nat_mult[symmetric])
    1.25  
    1.26  lemma binomial_gbinomial: "of_nat (n choose k) = of_nat n gchoose k"
    1.27  proof-
    1.28 @@ -377,7 +371,7 @@
    1.29      have ?thesis using kn
    1.30        apply (simp add: binomial_fact[OF kn, where ?'a = 'a] 
    1.31  	gbinomial_pochhammer field_simps pochhammer_Suc_setprod)
    1.32 -      apply (simp add: pochhammer_Suc_setprod fact_setprod h of_nat_setprod setprod_timesf[symmetric] eq' del: One_nat_def power_Suc)
    1.33 +      apply (simp add: pochhammer_Suc_setprod fact_altdef_nat h of_nat_setprod setprod_timesf[symmetric] eq' del: One_nat_def power_Suc)
    1.34        unfolding setprod_Un_disjoint[OF th0, unfolded eq3, of "of_nat:: nat \<Rightarrow> 'a"] eq[unfolded h]
    1.35        unfolding mult_assoc[symmetric] 
    1.36        unfolding setprod_timesf[symmetric]
    1.37 @@ -404,7 +398,7 @@
    1.38  proof-
    1.39    have "?r = ((- 1) ^n * pochhammer (- a) n / of_nat (fact n)) * (of_nat n - (- a + of_nat n))"
    1.40      unfolding gbinomial_pochhammer
    1.41 -    pochhammer_Suc fact_Suc of_nat_mult right_diff_distrib power_Suc
    1.42 +    pochhammer_Suc fact_Suc_nat of_nat_mult right_diff_distrib power_Suc
    1.43      by (simp add:  field_simps del: of_nat_Suc)
    1.44    also have "\<dots> = ?l" unfolding gbinomial_pochhammer
    1.45      by (simp add: ring_simps)
    1.46 @@ -420,7 +414,7 @@
    1.47  lemma gbinomial_mult_fact:
    1.48    "(of_nat (fact (Suc k)) :: 'a) * ((a::'a::field_char_0) gchoose (Suc k)) = (setprod (\<lambda>i. a - of_nat i) {0 .. k})"
    1.49    unfolding gbinomial_Suc
    1.50 -  by (simp_all add: field_simps del: fact_Suc)
    1.51 +  by (simp_all add: field_simps del: fact_Suc_nat)
    1.52  
    1.53  lemma gbinomial_mult_fact':
    1.54    "((a::'a::field_char_0) gchoose (Suc k)) * (of_nat (fact (Suc k)) :: 'a) = (setprod (\<lambda>i. a - of_nat i) {0 .. k})"
    1.55 @@ -438,9 +432,9 @@
    1.56  
    1.57      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)" 
    1.58        unfolding h
    1.59 -      apply (simp add: ring_simps del: fact_Suc)
    1.60 +      apply (simp add: ring_simps del: fact_Suc_nat)
    1.61        unfolding gbinomial_mult_fact'
    1.62 -      apply (subst fact_Suc)
    1.63 +      apply (subst fact_Suc_nat)
    1.64        unfolding of_nat_mult 
    1.65        apply (subst mult_commute)
    1.66        unfolding mult_assoc
    1.67 @@ -455,7 +449,7 @@
    1.68        by simp
    1.69      also have "\<dots> = of_nat (fact (Suc k)) * ((a + 1) gchoose (Suc k))"
    1.70        unfolding gbinomial_mult_fact ..
    1.71 -    finally have ?thesis by (simp del: fact_Suc) }
    1.72 +    finally have ?thesis by (simp del: fact_Suc_nat) }
    1.73    ultimately show ?thesis by (cases k, auto)
    1.74  qed
    1.75  
     2.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Fri Jul 10 12:55:06 2009 -0400
     2.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Tue Jul 14 20:58:53 2009 -0400
     2.3 @@ -2514,7 +2514,7 @@
     2.4  proof-
     2.5    {fix n
     2.6      have "?l$n = ?r $ n"
     2.7 -  apply (auto simp add: E_def field_simps power_Suc[symmetric]simp del: fact_Suc of_nat_Suc power_Suc)
     2.8 +  apply (auto simp add: E_def field_simps power_Suc[symmetric]simp del: fact_Suc_nat of_nat_Suc power_Suc)
     2.9    by (simp add: of_nat_mult ring_simps)}
    2.10  then show ?thesis by (simp add: fps_eq_iff)
    2.11  qed
    2.12 @@ -2530,8 +2530,8 @@
    2.13        apply (induct n)
    2.14        apply simp
    2.15        unfolding th
    2.16 -      using fact_gt_zero
    2.17 -      apply (simp add: field_simps del: of_nat_Suc fact.simps)
    2.18 +      using fact_gt_zero_nat
    2.19 +      apply (simp add: field_simps del: of_nat_Suc fact_Suc_nat)
    2.20        apply (drule sym)
    2.21        by (simp add: ring_simps of_nat_mult power_Suc)}
    2.22    note th' = this
    2.23 @@ -2697,7 +2697,7 @@
    2.24        also have "\<dots> = of_nat (n+1) * ((- 1)^(n div 2) * c^Suc n / of_nat (fact (Suc n)))"
    2.25  	using en by (simp add: fps_sin_def)
    2.26        also have "\<dots> = (- 1)^(n div 2) * c^Suc n * (of_nat (n+1) / (of_nat (Suc n) * of_nat (fact n)))"
    2.27 -	unfolding fact_Suc of_nat_mult
    2.28 +	unfolding fact_Suc_nat of_nat_mult
    2.29  	by (simp add: field_simps del: of_nat_add of_nat_Suc)
    2.30        also have "\<dots> = (- 1)^(n div 2) *c^Suc n / of_nat (fact n)"
    2.31  	by (simp add: field_simps del: of_nat_add of_nat_Suc)
    2.32 @@ -2721,7 +2721,7 @@
    2.33        also have "\<dots> = of_nat (n+1) * ((- 1)^((n + 1) div 2) * c^Suc n / of_nat (fact (Suc n)))"
    2.34  	using en by (simp add: fps_cos_def)
    2.35        also have "\<dots> = (- 1)^((n + 1) div 2)*c^Suc n * (of_nat (n+1) / (of_nat (Suc n) * of_nat (fact n)))"
    2.36 -	unfolding fact_Suc of_nat_mult
    2.37 +	unfolding fact_Suc_nat of_nat_mult
    2.38  	by (simp add: field_simps del: of_nat_add of_nat_Suc)
    2.39        also have "\<dots> = (- 1)^((n + 1) div 2) * c^Suc n / of_nat (fact n)"
    2.40  	by (simp add: field_simps del: of_nat_add of_nat_Suc)
    2.41 @@ -2747,9 +2747,6 @@
    2.42    finally show ?thesis .
    2.43  qed
    2.44  
    2.45 -lemma fact_1 [simp]: "fact 1 = 1"
    2.46 -unfolding One_nat_def fact_Suc by simp
    2.47 -
    2.48  lemma divide_eq_iff: "a \<noteq> (0::'a::field) \<Longrightarrow> x / a = y \<longleftrightarrow> x = y * a"
    2.49  by auto
    2.50  
    2.51 @@ -2766,7 +2763,7 @@
    2.52    "fps_sin c $ (n + 2) = - (c * c * fps_sin c $ n / (of_nat(n+1) * of_nat(n+2)))"
    2.53  unfolding fps_sin_def
    2.54  apply (cases n, simp)
    2.55 -apply (simp add: divide_eq_iff eq_divide_iff del: of_nat_Suc fact_Suc)
    2.56 +apply (simp add: divide_eq_iff eq_divide_iff del: of_nat_Suc fact_Suc_nat)
    2.57  apply (simp add: of_nat_mult del: of_nat_Suc mult_Suc)
    2.58  done
    2.59  
    2.60 @@ -2779,7 +2776,7 @@
    2.61  lemma fps_cos_nth_add_2:
    2.62    "fps_cos c $ (n + 2) = - (c * c * fps_cos c $ n / (of_nat(n+1) * of_nat(n+2)))"
    2.63  unfolding fps_cos_def
    2.64 -apply (simp add: divide_eq_iff eq_divide_iff del: of_nat_Suc fact_Suc)
    2.65 +apply (simp add: divide_eq_iff eq_divide_iff del: of_nat_Suc fact_Suc_nat)
    2.66  apply (simp add: of_nat_mult del: of_nat_Suc mult_Suc)
    2.67  done
    2.68