Changed fact_Suc_nat back to fact_Suc
authoravigad
Fri Jul 17 13:12:18 2009 -0400 (2009-07-17)
changeset 32047c141f139ce26
parent 32045 efc5f4806cd5
child 32048 b3eaeb39da83
Changed fact_Suc_nat back to fact_Suc
src/HOL/Fact.thy
src/HOL/Library/Binomial.thy
src/HOL/Library/Formal_Power_Series.thy
src/HOL/MacLaurin.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Fact.thy	Fri Jul 17 10:07:15 2009 +0200
     1.2 +++ b/src/HOL/Fact.thy	Fri Jul 17 13:12:18 2009 -0400
     1.3 @@ -24,7 +24,7 @@
     1.4    fact_nat :: "nat \<Rightarrow> nat"
     1.5  where
     1.6    fact_0_nat: "fact_nat 0 = Suc 0"
     1.7 -| fact_Suc_nat: "fact_nat (Suc x) = Suc x * fact x"
     1.8 +| fact_Suc: "fact_nat (Suc x) = Suc x * fact x"
     1.9  
    1.10  instance proof qed
    1.11  
    1.12 @@ -100,7 +100,7 @@
    1.13  lemma fact_reduce_nat: "(n::nat) > 0 \<Longrightarrow> fact n = n * fact (n - 1)"
    1.14    apply (subgoal_tac "n = Suc (n - 1)")
    1.15    apply (erule ssubst)
    1.16 -  apply (subst fact_Suc_nat)
    1.17 +  apply (subst fact_Suc)
    1.18    apply simp_all
    1.19  done
    1.20  
    1.21 @@ -142,7 +142,7 @@
    1.22  lemma dvd_fact_nat [rule_format]: "1 <= m \<longrightarrow> m <= n \<longrightarrow> m dvd fact (n::nat)"
    1.23    apply (induct n)
    1.24    apply force
    1.25 -  apply (auto simp only: fact_Suc_nat)
    1.26 +  apply (auto simp only: fact_Suc)
    1.27    apply (subgoal_tac "m = Suc n")
    1.28    apply (erule ssubst)
    1.29    apply (rule dvd_triv_left)
    1.30 @@ -170,7 +170,7 @@
    1.31  lemma fact_altdef_nat: "fact (n::nat) = (PROD i:{1..n}. i)"
    1.32    apply (induct n)
    1.33    apply force
    1.34 -  apply (subst fact_Suc_nat)
    1.35 +  apply (subst fact_Suc)
    1.36    apply (subst interval_Suc)
    1.37    apply auto
    1.38  done
     2.1 --- a/src/HOL/Library/Binomial.thy	Fri Jul 17 10:07:15 2009 +0200
     2.2 +++ b/src/HOL/Library/Binomial.thy	Fri Jul 17 13:12:18 2009 -0400
     2.3 @@ -398,7 +398,7 @@
     2.4  proof-
     2.5    have "?r = ((- 1) ^n * pochhammer (- a) n / of_nat (fact n)) * (of_nat n - (- a + of_nat n))"
     2.6      unfolding gbinomial_pochhammer
     2.7 -    pochhammer_Suc fact_Suc_nat of_nat_mult right_diff_distrib power_Suc
     2.8 +    pochhammer_Suc fact_Suc of_nat_mult right_diff_distrib power_Suc
     2.9      by (simp add:  field_simps del: of_nat_Suc)
    2.10    also have "\<dots> = ?l" unfolding gbinomial_pochhammer
    2.11      by (simp add: ring_simps)
    2.12 @@ -414,7 +414,7 @@
    2.13  lemma gbinomial_mult_fact:
    2.14    "(of_nat (fact (Suc k)) :: 'a) * ((a::'a::field_char_0) gchoose (Suc k)) = (setprod (\<lambda>i. a - of_nat i) {0 .. k})"
    2.15    unfolding gbinomial_Suc
    2.16 -  by (simp_all add: field_simps del: fact_Suc_nat)
    2.17 +  by (simp_all add: field_simps del: fact_Suc)
    2.18  
    2.19  lemma gbinomial_mult_fact':
    2.20    "((a::'a::field_char_0) gchoose (Suc k)) * (of_nat (fact (Suc k)) :: 'a) = (setprod (\<lambda>i. a - of_nat i) {0 .. k})"
    2.21 @@ -432,9 +432,9 @@
    2.22  
    2.23      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)" 
    2.24        unfolding h
    2.25 -      apply (simp add: ring_simps del: fact_Suc_nat)
    2.26 +      apply (simp add: ring_simps del: fact_Suc)
    2.27        unfolding gbinomial_mult_fact'
    2.28 -      apply (subst fact_Suc_nat)
    2.29 +      apply (subst fact_Suc)
    2.30        unfolding of_nat_mult 
    2.31        apply (subst mult_commute)
    2.32        unfolding mult_assoc
    2.33 @@ -449,7 +449,7 @@
    2.34        by simp
    2.35      also have "\<dots> = of_nat (fact (Suc k)) * ((a + 1) gchoose (Suc k))"
    2.36        unfolding gbinomial_mult_fact ..
    2.37 -    finally have ?thesis by (simp del: fact_Suc_nat) }
    2.38 +    finally have ?thesis by (simp del: fact_Suc) }
    2.39    ultimately show ?thesis by (cases k, auto)
    2.40  qed
    2.41  
     3.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Fri Jul 17 10:07:15 2009 +0200
     3.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Fri Jul 17 13:12:18 2009 -0400
     3.3 @@ -2514,7 +2514,7 @@
     3.4  proof-
     3.5    {fix n
     3.6      have "?l$n = ?r $ n"
     3.7 -  apply (auto simp add: E_def field_simps power_Suc[symmetric]simp del: fact_Suc_nat of_nat_Suc power_Suc)
     3.8 +  apply (auto simp add: E_def field_simps power_Suc[symmetric]simp del: fact_Suc of_nat_Suc power_Suc)
     3.9    by (simp add: of_nat_mult ring_simps)}
    3.10  then show ?thesis by (simp add: fps_eq_iff)
    3.11  qed
    3.12 @@ -2531,7 +2531,7 @@
    3.13        apply simp
    3.14        unfolding th
    3.15        using fact_gt_zero_nat
    3.16 -      apply (simp add: field_simps del: of_nat_Suc fact_Suc_nat)
    3.17 +      apply (simp add: field_simps del: of_nat_Suc fact_Suc)
    3.18        apply (drule sym)
    3.19        by (simp add: ring_simps of_nat_mult power_Suc)}
    3.20    note th' = this
    3.21 @@ -2697,7 +2697,7 @@
    3.22        also have "\<dots> = of_nat (n+1) * ((- 1)^(n div 2) * c^Suc n / of_nat (fact (Suc n)))"
    3.23  	using en by (simp add: fps_sin_def)
    3.24        also have "\<dots> = (- 1)^(n div 2) * c^Suc n * (of_nat (n+1) / (of_nat (Suc n) * of_nat (fact n)))"
    3.25 -	unfolding fact_Suc_nat of_nat_mult
    3.26 +	unfolding fact_Suc of_nat_mult
    3.27  	by (simp add: field_simps del: of_nat_add of_nat_Suc)
    3.28        also have "\<dots> = (- 1)^(n div 2) *c^Suc n / of_nat (fact n)"
    3.29  	by (simp add: field_simps del: of_nat_add of_nat_Suc)
    3.30 @@ -2721,7 +2721,7 @@
    3.31        also have "\<dots> = of_nat (n+1) * ((- 1)^((n + 1) div 2) * c^Suc n / of_nat (fact (Suc n)))"
    3.32  	using en by (simp add: fps_cos_def)
    3.33        also have "\<dots> = (- 1)^((n + 1) div 2)*c^Suc n * (of_nat (n+1) / (of_nat (Suc n) * of_nat (fact n)))"
    3.34 -	unfolding fact_Suc_nat of_nat_mult
    3.35 +	unfolding fact_Suc of_nat_mult
    3.36  	by (simp add: field_simps del: of_nat_add of_nat_Suc)
    3.37        also have "\<dots> = (- 1)^((n + 1) div 2) * c^Suc n / of_nat (fact n)"
    3.38  	by (simp add: field_simps del: of_nat_add of_nat_Suc)
    3.39 @@ -2763,7 +2763,7 @@
    3.40    "fps_sin c $ (n + 2) = - (c * c * fps_sin c $ n / (of_nat(n+1) * of_nat(n+2)))"
    3.41  unfolding fps_sin_def
    3.42  apply (cases n, simp)
    3.43 -apply (simp add: divide_eq_iff eq_divide_iff del: of_nat_Suc fact_Suc_nat)
    3.44 +apply (simp add: divide_eq_iff eq_divide_iff del: of_nat_Suc fact_Suc)
    3.45  apply (simp add: of_nat_mult del: of_nat_Suc mult_Suc)
    3.46  done
    3.47  
    3.48 @@ -2776,7 +2776,7 @@
    3.49  lemma fps_cos_nth_add_2:
    3.50    "fps_cos c $ (n + 2) = - (c * c * fps_cos c $ n / (of_nat(n+1) * of_nat(n+2)))"
    3.51  unfolding fps_cos_def
    3.52 -apply (simp add: divide_eq_iff eq_divide_iff del: of_nat_Suc fact_Suc_nat)
    3.53 +apply (simp add: divide_eq_iff eq_divide_iff del: of_nat_Suc fact_Suc)
    3.54  apply (simp add: of_nat_mult del: of_nat_Suc mult_Suc)
    3.55  done
    3.56  
     4.1 --- a/src/HOL/MacLaurin.thy	Fri Jul 17 10:07:15 2009 +0200
     4.2 +++ b/src/HOL/MacLaurin.thy	Fri Jul 17 13:12:18 2009 -0400
     4.3 @@ -58,17 +58,17 @@
     4.4   apply (frule less_iff_Suc_add [THEN iffD1], clarify)
     4.5   apply (simp del: setsum_op_ivl_Suc)
     4.6   apply (insert sumr_offset4 [of "Suc 0"])
     4.7 - apply (simp del: setsum_op_ivl_Suc fact_Suc_nat power_Suc)
     4.8 + apply (simp del: setsum_op_ivl_Suc fact_Suc power_Suc)
     4.9   apply (rule lemma_DERIV_subst)
    4.10    apply (rule DERIV_add)
    4.11     apply (rule_tac [2] DERIV_const)
    4.12    apply (rule DERIV_sumr, clarify)
    4.13    prefer 2 apply simp
    4.14 - apply (simp (no_asm) add: divide_inverse mult_assoc del: fact_Suc_nat power_Suc)
    4.15 + apply (simp (no_asm) add: divide_inverse mult_assoc del: fact_Suc power_Suc)
    4.16   apply (rule DERIV_cmult)
    4.17   apply (rule lemma_DERIV_subst)
    4.18    apply (best intro!: DERIV_intros)
    4.19 - apply (subst fact_Suc_nat)
    4.20 + apply (subst fact_Suc)
    4.21   apply (subst real_of_nat_mult)
    4.22   apply (simp add: mult_ac)
    4.23  done
    4.24 @@ -120,7 +120,7 @@
    4.25      apply (frule less_iff_Suc_add [THEN iffD1], clarify)
    4.26      apply (simp del: setsum_op_ivl_Suc)
    4.27      apply (insert sumr_offset4 [of "Suc 0"])
    4.28 -    apply (simp del: setsum_op_ivl_Suc fact_Suc_nat)
    4.29 +    apply (simp del: setsum_op_ivl_Suc fact_Suc)
    4.30      done
    4.31  
    4.32    have isCont_difg: "\<And>m x. \<lbrakk>m < n; 0 \<le> x; x \<le> h\<rbrakk> \<Longrightarrow> isCont (difg m) x"
    4.33 @@ -180,7 +180,7 @@
    4.34        (\<Sum>m = 0..<n. diff m 0 / real (fact m) * h ^ m) +
    4.35        diff n t / real (fact n) * h ^ n"
    4.36        using `difg (Suc m) t = 0`
    4.37 -      by (simp add: m f_h difg_def del: fact_Suc_nat)
    4.38 +      by (simp add: m f_h difg_def del: fact_Suc)
    4.39    qed
    4.40  
    4.41  qed
     5.1 --- a/src/HOL/Transcendental.thy	Fri Jul 17 10:07:15 2009 +0200
     5.2 +++ b/src/HOL/Transcendental.thy	Fri Jul 17 13:12:18 2009 -0400
     5.3 @@ -1604,11 +1604,11 @@
     5.4  apply (rotate_tac 2)
     5.5  apply (drule sin_paired [THEN sums_unique, THEN ssubst])
     5.6  unfolding One_nat_def
     5.7 -apply (auto simp del: fact_Suc_nat)
     5.8 +apply (auto simp del: fact_Suc)
     5.9  apply (frule sums_unique)
    5.10 -apply (auto simp del: fact_Suc_nat)
    5.11 +apply (auto simp del: fact_Suc)
    5.12  apply (rule_tac n1 = 0 in series_pos_less [THEN [2] order_le_less_trans])
    5.13 -apply (auto simp del: fact_Suc_nat)
    5.14 +apply (auto simp del: fact_Suc)
    5.15  apply (erule sums_summable)
    5.16  apply (case_tac "m=0")
    5.17  apply (simp (no_asm_simp))
    5.18 @@ -1617,24 +1617,24 @@
    5.19  apply (simp (no_asm_simp) add: numeral_2_eq_2 [symmetric] mult_assoc [symmetric])
    5.20  apply (subgoal_tac "x*x < 2*3", simp) 
    5.21  apply (rule mult_strict_mono)
    5.22 -apply (auto simp add: real_0_less_add_iff real_of_nat_Suc simp del: fact_Suc_nat)
    5.23 -apply (subst fact_Suc_nat)
    5.24 -apply (subst fact_Suc_nat)
    5.25 -apply (subst fact_Suc_nat)
    5.26 -apply (subst fact_Suc_nat)
    5.27 +apply (auto simp add: real_0_less_add_iff real_of_nat_Suc simp del: fact_Suc)
    5.28 +apply (subst fact_Suc)
    5.29 +apply (subst fact_Suc)
    5.30 +apply (subst fact_Suc)
    5.31 +apply (subst fact_Suc)
    5.32  apply (subst real_of_nat_mult)
    5.33  apply (subst real_of_nat_mult)
    5.34  apply (subst real_of_nat_mult)
    5.35  apply (subst real_of_nat_mult)
    5.36 -apply (simp (no_asm) add: divide_inverse del: fact_Suc_nat)
    5.37 -apply (auto simp add: mult_assoc [symmetric] simp del: fact_Suc_nat)
    5.38 +apply (simp (no_asm) add: divide_inverse del: fact_Suc)
    5.39 +apply (auto simp add: mult_assoc [symmetric] simp del: fact_Suc)
    5.40  apply (rule_tac c="real (Suc (Suc (4*m)))" in mult_less_imp_less_right) 
    5.41 -apply (auto simp add: mult_assoc simp del: fact_Suc_nat)
    5.42 +apply (auto simp add: mult_assoc simp del: fact_Suc)
    5.43  apply (rule_tac c="real (Suc (Suc (Suc (4*m))))" in mult_less_imp_less_right) 
    5.44 -apply (auto simp add: mult_assoc mult_less_cancel_left simp del: fact_Suc_nat)
    5.45 +apply (auto simp add: mult_assoc mult_less_cancel_left simp del: fact_Suc)
    5.46  apply (subgoal_tac "x * (x * x ^ (4*m)) = (x ^ (4*m)) * (x * x)") 
    5.47  apply (erule ssubst)+
    5.48 -apply (auto simp del: fact_Suc_nat)
    5.49 +apply (auto simp del: fact_Suc)
    5.50  apply (subgoal_tac "0 < x ^ (4 * m) ")
    5.51   prefer 2 apply (simp only: zero_less_power) 
    5.52  apply (simp (no_asm_simp) add: mult_less_cancel_left)
    5.53 @@ -1670,18 +1670,18 @@
    5.54  apply (rule_tac y =
    5.55   "\<Sum>n=0..< Suc(Suc(Suc 0)). - (-1 ^ n / (real(fact (2*n))) * 2 ^ (2*n))"
    5.56         in order_less_trans)
    5.57 -apply (simp (no_asm) add: fact_num_eq_if_nat realpow_num_eq_if del: fact_Suc_nat)
    5.58 +apply (simp (no_asm) add: fact_num_eq_if_nat realpow_num_eq_if del: fact_Suc)
    5.59  apply (simp (no_asm) add: mult_assoc del: setsum_op_ivl_Suc)
    5.60  apply (rule sumr_pos_lt_pair)
    5.61  apply (erule sums_summable, safe)
    5.62  unfolding One_nat_def
    5.63  apply (simp (no_asm) add: divide_inverse real_0_less_add_iff mult_assoc [symmetric] 
    5.64 -            del: fact_Suc_nat)
    5.65 +            del: fact_Suc)
    5.66  apply (rule real_mult_inverse_cancel2)
    5.67  apply (rule real_of_nat_fact_gt_zero)+
    5.68 -apply (simp (no_asm) add: mult_assoc [symmetric] del: fact_Suc_nat)
    5.69 +apply (simp (no_asm) add: mult_assoc [symmetric] del: fact_Suc)
    5.70  apply (subst fact_lemma) 
    5.71 -apply (subst fact_Suc_nat [of "Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))"])
    5.72 +apply (subst fact_Suc [of "Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))"])
    5.73  apply (simp only: real_of_nat_mult)
    5.74  apply (rule mult_strict_mono, force)
    5.75    apply (rule_tac [3] real_of_nat_ge_zero)