# HG changeset patch
# User wenzelm
# Date 1247865237 -7200
# Node ID b3eaeb39da83fdedfaf490a987d31659a31e30fb
# Parent  c141f139ce26272b5b28396be7d4f2415e7de3ce# Parent  3b12e03e4178d710ba755a1a5ad7bc452daaa1e1
merged

diff -r 3b12e03e4178 -r b3eaeb39da83 src/HOL/Fact.thy
--- a/src/HOL/Fact.thy	Fri Jul 17 23:13:50 2009 +0200
+++ b/src/HOL/Fact.thy	Fri Jul 17 23:13:57 2009 +0200
@@ -24,7 +24,7 @@
   fact_nat :: "nat \<Rightarrow> nat"
 where
   fact_0_nat: "fact_nat 0 = Suc 0"
-| fact_Suc_nat: "fact_nat (Suc x) = Suc x * fact x"
+| fact_Suc: "fact_nat (Suc x) = Suc x * fact x"
 
 instance proof qed
 
@@ -100,7 +100,7 @@
 lemma fact_reduce_nat: "(n::nat) > 0 \<Longrightarrow> fact n = n * fact (n - 1)"
   apply (subgoal_tac "n = Suc (n - 1)")
   apply (erule ssubst)
-  apply (subst fact_Suc_nat)
+  apply (subst fact_Suc)
   apply simp_all
 done
 
@@ -142,7 +142,7 @@
 lemma dvd_fact_nat [rule_format]: "1 <= m \<longrightarrow> m <= n \<longrightarrow> m dvd fact (n::nat)"
   apply (induct n)
   apply force
-  apply (auto simp only: fact_Suc_nat)
+  apply (auto simp only: fact_Suc)
   apply (subgoal_tac "m = Suc n")
   apply (erule ssubst)
   apply (rule dvd_triv_left)
@@ -170,7 +170,7 @@
 lemma fact_altdef_nat: "fact (n::nat) = (PROD i:{1..n}. i)"
   apply (induct n)
   apply force
-  apply (subst fact_Suc_nat)
+  apply (subst fact_Suc)
   apply (subst interval_Suc)
   apply auto
 done
diff -r 3b12e03e4178 -r b3eaeb39da83 src/HOL/Library/Binomial.thy
--- a/src/HOL/Library/Binomial.thy	Fri Jul 17 23:13:50 2009 +0200
+++ b/src/HOL/Library/Binomial.thy	Fri Jul 17 23:13:57 2009 +0200
@@ -398,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_nat of_nat_mult right_diff_distrib power_Suc
+    pochhammer_Suc fact_Suc 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)
@@ -414,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_nat)
+  by (simp_all add: field_simps del: fact_Suc)
 
 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})"
@@ -432,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_nat)
+      apply (simp add: ring_simps del: fact_Suc)
       unfolding gbinomial_mult_fact'
-      apply (subst fact_Suc_nat)
+      apply (subst fact_Suc)
       unfolding of_nat_mult 
       apply (subst mult_commute)
       unfolding mult_assoc
@@ -449,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_nat) }
+    finally have ?thesis by (simp del: fact_Suc) }
   ultimately show ?thesis by (cases k, auto)
 qed
 
diff -r 3b12e03e4178 -r b3eaeb39da83 src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Fri Jul 17 23:13:50 2009 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy	Fri Jul 17 23:13:57 2009 +0200
@@ -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_nat of_nat_Suc power_Suc)
+  apply (auto simp add: E_def field_simps power_Suc[symmetric]simp del: fact_Suc of_nat_Suc power_Suc)
   by (simp add: of_nat_mult ring_simps)}
 then show ?thesis by (simp add: fps_eq_iff)
 qed
@@ -2531,7 +2531,7 @@
       apply simp
       unfolding th
       using fact_gt_zero_nat
-      apply (simp add: field_simps del: of_nat_Suc fact_Suc_nat)
+      apply (simp add: field_simps del: of_nat_Suc fact_Suc)
       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_nat of_nat_mult
+	unfolding fact_Suc 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_nat of_nat_mult
+	unfolding fact_Suc 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)
@@ -2763,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_nat)
+apply (simp add: divide_eq_iff eq_divide_iff del: of_nat_Suc fact_Suc)
 apply (simp add: of_nat_mult del: of_nat_Suc mult_Suc)
 done
 
@@ -2776,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_nat)
+apply (simp add: divide_eq_iff eq_divide_iff del: of_nat_Suc fact_Suc)
 apply (simp add: of_nat_mult del: of_nat_Suc mult_Suc)
 done
 
diff -r 3b12e03e4178 -r b3eaeb39da83 src/HOL/MacLaurin.thy
--- a/src/HOL/MacLaurin.thy	Fri Jul 17 23:13:50 2009 +0200
+++ b/src/HOL/MacLaurin.thy	Fri Jul 17 23:13:57 2009 +0200
@@ -58,17 +58,17 @@
  apply (frule less_iff_Suc_add [THEN iffD1], clarify)
  apply (simp del: setsum_op_ivl_Suc)
  apply (insert sumr_offset4 [of "Suc 0"])
- apply (simp del: setsum_op_ivl_Suc fact_Suc_nat power_Suc)
+ apply (simp del: setsum_op_ivl_Suc fact_Suc power_Suc)
  apply (rule lemma_DERIV_subst)
   apply (rule DERIV_add)
    apply (rule_tac [2] DERIV_const)
   apply (rule DERIV_sumr, clarify)
   prefer 2 apply simp
- apply (simp (no_asm) add: divide_inverse mult_assoc del: fact_Suc_nat power_Suc)
+ apply (simp (no_asm) add: divide_inverse mult_assoc del: fact_Suc power_Suc)
  apply (rule DERIV_cmult)
  apply (rule lemma_DERIV_subst)
   apply (best intro!: DERIV_intros)
- apply (subst fact_Suc_nat)
+ apply (subst fact_Suc)
  apply (subst real_of_nat_mult)
  apply (simp add: mult_ac)
 done
@@ -120,7 +120,7 @@
     apply (frule less_iff_Suc_add [THEN iffD1], clarify)
     apply (simp del: setsum_op_ivl_Suc)
     apply (insert sumr_offset4 [of "Suc 0"])
-    apply (simp del: setsum_op_ivl_Suc fact_Suc_nat)
+    apply (simp del: setsum_op_ivl_Suc fact_Suc)
     done
 
   have isCont_difg: "\<And>m x. \<lbrakk>m < n; 0 \<le> x; x \<le> h\<rbrakk> \<Longrightarrow> isCont (difg m) x"
@@ -180,7 +180,7 @@
       (\<Sum>m = 0..<n. diff m 0 / real (fact m) * h ^ m) +
       diff n t / real (fact n) * h ^ n"
       using `difg (Suc m) t = 0`
-      by (simp add: m f_h difg_def del: fact_Suc_nat)
+      by (simp add: m f_h difg_def del: fact_Suc)
   qed
 
 qed
diff -r 3b12e03e4178 -r b3eaeb39da83 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Fri Jul 17 23:13:50 2009 +0200
+++ b/src/HOL/Transcendental.thy	Fri Jul 17 23:13:57 2009 +0200
@@ -1604,11 +1604,11 @@
 apply (rotate_tac 2)
 apply (drule sin_paired [THEN sums_unique, THEN ssubst])
 unfolding One_nat_def
-apply (auto simp del: fact_Suc_nat)
+apply (auto simp del: fact_Suc)
 apply (frule sums_unique)
-apply (auto simp del: fact_Suc_nat)
+apply (auto simp del: fact_Suc)
 apply (rule_tac n1 = 0 in series_pos_less [THEN [2] order_le_less_trans])
-apply (auto simp del: fact_Suc_nat)
+apply (auto simp del: fact_Suc)
 apply (erule sums_summable)
 apply (case_tac "m=0")
 apply (simp (no_asm_simp))
@@ -1617,24 +1617,24 @@
 apply (simp (no_asm_simp) add: numeral_2_eq_2 [symmetric] mult_assoc [symmetric])
 apply (subgoal_tac "x*x < 2*3", simp) 
 apply (rule mult_strict_mono)
-apply (auto simp add: real_0_less_add_iff real_of_nat_Suc simp del: fact_Suc_nat)
-apply (subst fact_Suc_nat)
-apply (subst fact_Suc_nat)
-apply (subst fact_Suc_nat)
-apply (subst fact_Suc_nat)
+apply (auto simp add: real_0_less_add_iff real_of_nat_Suc simp del: fact_Suc)
+apply (subst fact_Suc)
+apply (subst fact_Suc)
+apply (subst fact_Suc)
+apply (subst fact_Suc)
 apply (subst real_of_nat_mult)
 apply (subst real_of_nat_mult)
 apply (subst real_of_nat_mult)
 apply (subst real_of_nat_mult)
-apply (simp (no_asm) add: divide_inverse del: fact_Suc_nat)
-apply (auto simp add: mult_assoc [symmetric] simp del: fact_Suc_nat)
+apply (simp (no_asm) add: divide_inverse del: fact_Suc)
+apply (auto simp add: mult_assoc [symmetric] simp del: fact_Suc)
 apply (rule_tac c="real (Suc (Suc (4*m)))" in mult_less_imp_less_right) 
-apply (auto simp add: mult_assoc simp del: fact_Suc_nat)
+apply (auto simp add: mult_assoc simp del: fact_Suc)
 apply (rule_tac c="real (Suc (Suc (Suc (4*m))))" in mult_less_imp_less_right) 
-apply (auto simp add: mult_assoc mult_less_cancel_left simp del: fact_Suc_nat)
+apply (auto simp add: mult_assoc mult_less_cancel_left simp del: fact_Suc)
 apply (subgoal_tac "x * (x * x ^ (4*m)) = (x ^ (4*m)) * (x * x)") 
 apply (erule ssubst)+
-apply (auto simp del: fact_Suc_nat)
+apply (auto simp del: fact_Suc)
 apply (subgoal_tac "0 < x ^ (4 * m) ")
  prefer 2 apply (simp only: zero_less_power) 
 apply (simp (no_asm_simp) add: mult_less_cancel_left)
@@ -1670,18 +1670,18 @@
 apply (rule_tac y =
  "\<Sum>n=0..< Suc(Suc(Suc 0)). - (-1 ^ n / (real(fact (2*n))) * 2 ^ (2*n))"
        in order_less_trans)
-apply (simp (no_asm) add: fact_num_eq_if_nat realpow_num_eq_if del: fact_Suc_nat)
+apply (simp (no_asm) add: fact_num_eq_if_nat realpow_num_eq_if del: fact_Suc)
 apply (simp (no_asm) add: mult_assoc del: setsum_op_ivl_Suc)
 apply (rule sumr_pos_lt_pair)
 apply (erule sums_summable, safe)
 unfolding One_nat_def
 apply (simp (no_asm) add: divide_inverse real_0_less_add_iff mult_assoc [symmetric] 
-            del: fact_Suc_nat)
+            del: fact_Suc)
 apply (rule real_mult_inverse_cancel2)
 apply (rule real_of_nat_fact_gt_zero)+
-apply (simp (no_asm) add: mult_assoc [symmetric] del: fact_Suc_nat)
+apply (simp (no_asm) add: mult_assoc [symmetric] del: fact_Suc)
 apply (subst fact_lemma) 
-apply (subst fact_Suc_nat [of "Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))"])
+apply (subst fact_Suc [of "Suc (Suc (Suc (Suc (Suc (Suc (Suc (4 * d)))))))"])
 apply (simp only: real_of_nat_mult)
 apply (rule mult_strict_mono, force)
   apply (rule_tac [3] real_of_nat_ge_zero)