# HG changeset patch
# User huffman
# Date 1235502778 28800
# Node ID 43c5b7bfc791e29d781e5c7ecd08613c6564268e
# Parent  46b9c8ae3897e1157f4a341cc836cc37ad68e7ad
make more proofs work whether or not One_nat_def is a simp rule

diff -r 46b9c8ae3897 -r 43c5b7bfc791 src/HOL/Fact.thy
--- a/src/HOL/Fact.thy	Tue Feb 24 11:10:05 2009 -0800
+++ b/src/HOL/Fact.thy	Tue Feb 24 11:12:58 2009 -0800
@@ -58,7 +58,7 @@
   "n < Suc m ==> fact (Suc m - n) = (Suc m - n) * fact (m - n)"
 apply (induct n arbitrary: m)
 apply auto
-apply (drule_tac x = "m - 1" in meta_spec, auto)
+apply (drule_tac x = "m - Suc 0" in meta_spec, auto)
 done
 
 lemma fact_num0: "fact 0 = 1"
diff -r 46b9c8ae3897 -r 43c5b7bfc791 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Tue Feb 24 11:10:05 2009 -0800
+++ b/src/HOL/GCD.thy	Tue Feb 24 11:12:58 2009 -0800
@@ -60,9 +60,12 @@
 lemma gcd_non_0: "n > 0 \<Longrightarrow> gcd m n = gcd n (m mod n)"
   by simp
 
-lemma gcd_1 [simp, algebra]: "gcd m (Suc 0) = 1"
+lemma gcd_1 [simp, algebra]: "gcd m (Suc 0) = Suc 0"
   by simp
 
+lemma nat_gcd_1_right [simp, algebra]: "gcd m 1 = 1"
+  unfolding One_nat_def by (rule gcd_1)
+
 declare gcd.simps [simp del]
 
 text {*
@@ -116,9 +119,12 @@
   apply (blast intro: dvd_trans)
   done
 
-lemma gcd_1_left [simp, algebra]: "gcd (Suc 0) m = 1"
+lemma gcd_1_left [simp, algebra]: "gcd (Suc 0) m = Suc 0"
   by (simp add: gcd_commute)
 
+lemma nat_gcd_1_left [simp, algebra]: "gcd 1 m = 1"
+  unfolding One_nat_def by (rule gcd_1_left)
+
 text {*
   \medskip Multiplication laws
 *}
diff -r 46b9c8ae3897 -r 43c5b7bfc791 src/HOL/Integration.thy
--- a/src/HOL/Integration.thy	Tue Feb 24 11:10:05 2009 -0800
+++ b/src/HOL/Integration.thy	Tue Feb 24 11:12:58 2009 -0800
@@ -134,7 +134,7 @@
 apply (frule partition [THEN iffD1], safe)
 apply (drule_tac x = "psize D" and P="%n. psize D \<le> n --> ?P n" in spec, safe)
 apply (case_tac "psize D = 0")
-apply (drule_tac [2] n = "psize D - 1" in partition_lt, auto)
+apply (drule_tac [2] n = "psize D - Suc 0" in partition_lt, auto)
 done
 
 lemma partition_gt: "[|partition(a,b) D; n < (psize D)|] ==> D(n) < D(psize D)"
@@ -145,7 +145,7 @@
 apply (rotate_tac 2)
 apply (drule_tac x = "psize D" in spec)
 apply (rule ccontr)
-apply (drule_tac n = "psize D - 1" in partition_lt)
+apply (drule_tac n = "psize D - Suc 0" in partition_lt)
 apply auto
 done
 
diff -r 46b9c8ae3897 -r 43c5b7bfc791 src/HOL/MacLaurin.thy
--- a/src/HOL/MacLaurin.thy	Tue Feb 24 11:10:05 2009 -0800
+++ b/src/HOL/MacLaurin.thy	Tue Feb 24 11:12:58 2009 -0800
@@ -81,7 +81,7 @@
   prefer 2 apply simp
  apply (frule less_iff_Suc_add [THEN iffD1], clarify)
  apply (simp del: setsum_op_ivl_Suc)
- apply (insert sumr_offset4 [of 1])
+ apply (insert sumr_offset4 [of "Suc 0"])
  apply (simp del: setsum_op_ivl_Suc fact_Suc realpow_Suc)
  apply (rule lemma_DERIV_subst)
   apply (rule DERIV_add)
@@ -124,7 +124,7 @@
 
   have g2: "g 0 = 0 & g h = 0"
     apply (simp add: m f_h g_def del: setsum_op_ivl_Suc)
-    apply (cut_tac n = m and k = 1 in sumr_offset2)
+    apply (cut_tac n = m and k = "Suc 0" in sumr_offset2)
     apply (simp add: eq_diff_eq' diff_0 del: setsum_op_ivl_Suc)
     done
 
@@ -144,7 +144,7 @@
     apply (simp add: m difg_def)
     apply (frule less_iff_Suc_add [THEN iffD1], clarify)
     apply (simp del: setsum_op_ivl_Suc)
-    apply (insert sumr_offset4 [of 1])
+    apply (insert sumr_offset4 [of "Suc 0"])
     apply (simp del: setsum_op_ivl_Suc fact_Suc realpow_Suc)
     done
 
@@ -552,6 +552,10 @@
     "[|x = y; abs u \<le> (v::real) |] ==> \<bar>(x + u) - y\<bar> \<le> v"
 by auto
 
+text {* TODO: move to Parity.thy *}
+lemma nat_odd_1 [simp]: "odd (1::nat)"
+  unfolding even_nat_def by simp
+
 lemma Maclaurin_sin_bound:
   "abs(sin x - (\<Sum>m=0..<n. (if even m then 0 else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
   x ^ m))  \<le> inverse(real (fact n)) * \<bar>x\<bar> ^ n"
diff -r 46b9c8ae3897 -r 43c5b7bfc791 src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Tue Feb 24 11:10:05 2009 -0800
+++ b/src/HOL/RealDef.thy	Tue Feb 24 11:12:58 2009 -0800
@@ -705,6 +705,9 @@
 lemma real_of_nat_zero [simp]: "real (0::nat) = 0"
 by (simp add: real_of_nat_def)
 
+lemma real_of_nat_1 [simp]: "real (1::nat) = 1"
+by (simp add: real_of_nat_def)
+
 lemma real_of_nat_one [simp]: "real (Suc 0) = (1::real)"
 by (simp add: real_of_nat_def)
 
diff -r 46b9c8ae3897 -r 43c5b7bfc791 src/HOL/RealPow.thy
--- a/src/HOL/RealPow.thy	Tue Feb 24 11:10:05 2009 -0800
+++ b/src/HOL/RealPow.thy	Tue Feb 24 11:12:58 2009 -0800
@@ -44,7 +44,8 @@
 by (insert power_decreasing [of 1 "Suc n" r], simp)
 
 lemma realpow_minus_mult [rule_format]:
-     "0 < n --> (x::real) ^ (n - 1) * x = x ^ n" 
+     "0 < n --> (x::real) ^ (n - 1) * x = x ^ n"
+unfolding One_nat_def
 apply (simp split add: nat_diff_split)
 done
 
diff -r 46b9c8ae3897 -r 43c5b7bfc791 src/HOL/SEQ.thy
--- a/src/HOL/SEQ.thy	Tue Feb 24 11:10:05 2009 -0800
+++ b/src/HOL/SEQ.thy	Tue Feb 24 11:12:58 2009 -0800
@@ -338,10 +338,10 @@
 done
 
 lemma LIMSEQ_Suc: "f ----> l \<Longrightarrow> (\<lambda>n. f (Suc n)) ----> l"
-by (drule_tac k="1" in LIMSEQ_ignore_initial_segment, simp)
+by (drule_tac k="Suc 0" in LIMSEQ_ignore_initial_segment, simp)
 
 lemma LIMSEQ_imp_Suc: "(\<lambda>n. f (Suc n)) ----> l \<Longrightarrow> f ----> l"
-by (rule_tac k="1" in LIMSEQ_offset, simp)
+by (rule_tac k="Suc 0" in LIMSEQ_offset, simp)
 
 lemma LIMSEQ_Suc_iff: "(\<lambda>n. f (Suc n)) ----> l = f ----> l"
 by (blast intro: LIMSEQ_imp_Suc LIMSEQ_Suc)
diff -r 46b9c8ae3897 -r 43c5b7bfc791 src/HOL/Series.thy
--- a/src/HOL/Series.thy	Tue Feb 24 11:10:05 2009 -0800
+++ b/src/HOL/Series.thy	Tue Feb 24 11:12:58 2009 -0800
@@ -312,6 +312,7 @@
   shows "\<lbrakk>summable f;
         \<forall>d. 0 < f (k + (Suc(Suc 0) * d)) + f (k + ((Suc(Suc 0) * d) + 1))\<rbrakk>
       \<Longrightarrow> setsum f {0..<k} < suminf f"
+unfolding One_nat_def
 apply (subst suminf_split_initial_segment [where k="k"])
 apply assumption
 apply simp
@@ -537,7 +538,7 @@
 apply (safe, subgoal_tac "\<forall>n. N < n --> f (n) = 0")
  prefer 2
  apply clarify
- apply(erule_tac x = "n - 1" in allE)
+ apply(erule_tac x = "n - Suc 0" in allE)
  apply (simp add:diff_Suc split:nat.splits)
  apply (blast intro: norm_ratiotest_lemma)
 apply (rule_tac x = "Suc N" in exI, clarify)
diff -r 46b9c8ae3897 -r 43c5b7bfc791 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Tue Feb 24 11:10:05 2009 -0800
+++ b/src/HOL/Transcendental.thy	Tue Feb 24 11:12:58 2009 -0800
@@ -120,7 +120,7 @@
   case (Suc n)
   have "(\<Sum> i = 0 ..< 2 * Suc n. if even i then f i else g i) = 
         (\<Sum> i = 0 ..< n. f (2 * i)) + (\<Sum> i = 0 ..< n. g (2 * i + 1)) + (f (2 * n) + g (2 * n + 1))"
-    using Suc.hyps by auto
+    using Suc.hyps unfolding One_nat_def by auto
   also have "\<dots> = (\<Sum> i = 0 ..< Suc n. f (2 * i)) + (\<Sum> i = 0 ..< Suc n. g (2 * i + 1))" by auto
   finally show ?case .
 qed auto
@@ -187,16 +187,18 @@
              ((\<forall>n. l \<le> (\<Sum>i=0..<2*n + 1. -1^i*a i)) \<and> (\<lambda> n. \<Sum>i=0..<2*n + 1. -1^i*a i) ----> l)"
   (is "\<exists>l. ((\<forall>n. ?f n \<le> l) \<and> _) \<and> ((\<forall>n. l \<le> ?g n) \<and> _)")
 proof -
-  have fg_diff: "\<And>n. ?f n - ?g n = - a (2 * n)" by auto
+  have fg_diff: "\<And>n. ?f n - ?g n = - a (2 * n)" unfolding One_nat_def by auto
 
   have "\<forall> n. ?f n \<le> ?f (Suc n)"
   proof fix n show "?f n \<le> ?f (Suc n)" using mono[of "2*n"] by auto qed
   moreover
   have "\<forall> n. ?g (Suc n) \<le> ?g n"
-  proof fix n show "?g (Suc n) \<le> ?g n" using mono[of "Suc (2*n)"] by auto qed
+  proof fix n show "?g (Suc n) \<le> ?g n" using mono[of "Suc (2*n)"]
+    unfolding One_nat_def by auto qed
   moreover
   have "\<forall> n. ?f n \<le> ?g n" 
-  proof fix n show "?f n \<le> ?g n" using fg_diff a_pos by auto qed
+  proof fix n show "?f n \<le> ?g n" using fg_diff a_pos
+    unfolding One_nat_def by auto qed
   moreover
   have "(\<lambda> n. ?f n - ?g n) ----> 0" unfolding fg_diff
   proof (rule LIMSEQ_I)
@@ -904,7 +906,7 @@
 proof -
   have "(\<Sum>n = 0..<1. f n * 0 ^ n) = (\<Sum>n. f n * 0 ^ n)"
     by (rule sums_unique [OF series_zero], simp add: power_0_left)
-  thus ?thesis by simp
+  thus ?thesis unfolding One_nat_def by simp
 qed
 
 lemma exp_zero [simp]: "exp 0 = 1"
@@ -1234,10 +1236,11 @@
       show "x - 1 \<in> {- 1<..<1}" and "(0 :: real) < 1" using `0 < x` `x < 2` by auto
       { fix x :: real assume "x \<in> {- 1<..<1}" hence "norm (-x) < 1" by auto
 	show "summable (\<lambda>n. -1 ^ n * (1 / real (n + 1)) * real (Suc n) * x ^ n)"
+          unfolding One_nat_def
 	  by (auto simp del: power_mult_distrib simp add: power_mult_distrib[symmetric] summable_geometric[OF `norm (-x) < 1`])
       }
     qed
-    hence "DERIV (\<lambda>x. suminf (?f x)) (x - 1) :> suminf (?f' x)" by auto
+    hence "DERIV (\<lambda>x. suminf (?f x)) (x - 1) :> suminf (?f' x)" unfolding One_nat_def by auto
     hence "DERIV (\<lambda>x. suminf (?f (x - 1))) x :> suminf (?f' x)" unfolding DERIV_iff repos .
     ultimately have "DERIV (\<lambda>x. ln x - suminf (?f (x - 1))) x :> (suminf (?f' x) - suminf (?f' x))"
       by (rule DERIV_diff)
@@ -1514,6 +1517,7 @@
 
 lemma DERIV_fun_pow: "DERIV g x :> m ==>  
       DERIV (%x. (g x) ^ n) x :> real n * (g x) ^ (n - 1) * m"
+unfolding One_nat_def
 apply (rule lemma_DERIV_subst)
 apply (rule_tac f = "(%x. x ^ n)" in DERIV_chain2)
 apply (rule DERIV_pow, auto)
@@ -1635,7 +1639,7 @@
 	sums sin x"
     unfolding sin_def
     by (rule sin_converges [THEN sums_summable, THEN sums_group], simp) 
-  thus ?thesis by (simp add: mult_ac)
+  thus ?thesis unfolding One_nat_def by (simp add: mult_ac)
 qed
 
 lemma sin_gt_zero: "[|0 < x; x < 2 |] ==> 0 < sin x"
@@ -1647,6 +1651,7 @@
  apply (rule sin_paired [THEN sums_summable, THEN sums_group], simp) 
 apply (rotate_tac 2)
 apply (drule sin_paired [THEN sums_unique, THEN ssubst])
+unfolding One_nat_def
 apply (auto simp del: fact_Suc realpow_Suc)
 apply (frule sums_unique)
 apply (auto simp del: fact_Suc realpow_Suc)
@@ -1720,6 +1725,7 @@
 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)
 apply (rule real_mult_inverse_cancel2)
@@ -2792,7 +2798,7 @@
 
 lemma monoseq_arctan_series: fixes x :: real
   assumes "\<bar>x\<bar> \<le> 1" shows "monoseq (\<lambda> n. 1 / real (n*2+1) * x^(n*2+1))" (is "monoseq ?a")
-proof (cases "x = 0") case True thus ?thesis unfolding monoseq_def by auto
+proof (cases "x = 0") case True thus ?thesis unfolding monoseq_def One_nat_def by auto
 next
   case False
   have "norm x \<le> 1" and "x \<le> 1" and "-1 \<le> x" using assms by auto
@@ -2823,7 +2829,7 @@
 
 lemma zeroseq_arctan_series: fixes x :: real
   assumes "\<bar>x\<bar> \<le> 1" shows "(\<lambda> n. 1 / real (n*2+1) * x^(n*2+1)) ----> 0" (is "?a ----> 0")
-proof (cases "x = 0") case True thus ?thesis by (auto simp add: LIMSEQ_const)
+proof (cases "x = 0") case True thus ?thesis unfolding One_nat_def by (auto simp add: LIMSEQ_const)
 next
   case False
   have "norm x \<le> 1" and "x \<le> 1" and "-1 \<le> x" using assms by auto
@@ -2831,12 +2837,14 @@
   proof (cases "\<bar>x\<bar> < 1")
     case True hence "norm x < 1" by auto
     from LIMSEQ_mult[OF LIMSEQ_inverse_real_of_nat LIMSEQ_power_zero[OF `norm x < 1`, THEN LIMSEQ_Suc]]
-    show ?thesis unfolding inverse_eq_divide Suc_plus1 using LIMSEQ_linear[OF _ pos2] by auto
+    have "(\<lambda>n. 1 / real (n + 1) * x ^ (n + 1)) ----> 0"
+      unfolding inverse_eq_divide Suc_plus1 by simp
+    then show ?thesis using pos2 by (rule LIMSEQ_linear)
   next
     case False hence "x = -1 \<or> x = 1" using `\<bar>x\<bar> \<le> 1` by auto
-    hence n_eq: "\<And> n. x ^ (n * 2 + 1) = x" by auto
+    hence n_eq: "\<And> n. x ^ (n * 2 + 1) = x" unfolding One_nat_def by auto
     from LIMSEQ_mult[OF LIMSEQ_inverse_real_of_nat[THEN LIMSEQ_linear, OF pos2, unfolded inverse_eq_divide] LIMSEQ_const[of x]]
-    show ?thesis unfolding n_eq by auto
+    show ?thesis unfolding n_eq Suc_plus1 by auto
   qed
 qed
 
@@ -2989,7 +2997,7 @@
 	  from `even n` obtain m where "2 * m = n" unfolding even_mult_two_ex by auto
 	  from bounds[of m, unfolded this atLeastAtMost_iff]
 	  have "\<bar>arctan x - (\<Sum>i = 0..<n. (?c x i))\<bar> \<le> (\<Sum>i = 0..<n + 1. (?c x i)) - (\<Sum>i = 0..<n. (?c x i))" by auto
-	  also have "\<dots> = ?c x n" by auto
+	  also have "\<dots> = ?c x n" unfolding One_nat_def by auto
 	  also have "\<dots> = ?a x n" unfolding sgn_pos a_pos by auto
 	  finally show ?thesis .
 	next
@@ -2998,7 +3006,7 @@
 	  hence m_plus: "2 * (m + 1) = n + 1" by auto
 	  from bounds[of "m + 1", unfolded this atLeastAtMost_iff, THEN conjunct1] bounds[of m, unfolded m_def atLeastAtMost_iff, THEN conjunct2]
 	  have "\<bar>arctan x - (\<Sum>i = 0..<n. (?c x i))\<bar> \<le> (\<Sum>i = 0..<n. (?c x i)) - (\<Sum>i = 0..<n+1. (?c x i))" by auto
-	  also have "\<dots> = - ?c x n" by auto
+	  also have "\<dots> = - ?c x n" unfolding One_nat_def by auto
 	  also have "\<dots> = ?a x n" unfolding sgn_neg a_pos by auto
 	  finally show ?thesis .
 	qed
@@ -3011,7 +3019,9 @@
       ultimately have "0 \<le> ?a 1 n - ?diff 1 n" by (rule LIM_less_bound)
       hence "?diff 1 n \<le> ?a 1 n" by auto
     }
-    have "?a 1 ----> 0" unfolding LIMSEQ_rabs_zero power_one divide_inverse by (auto intro!: LIMSEQ_mult LIMSEQ_linear LIMSEQ_inverse_real_of_nat)
+    have "?a 1 ----> 0"
+      unfolding LIMSEQ_rabs_zero power_one divide_inverse One_nat_def
+      by (auto intro!: LIMSEQ_mult LIMSEQ_linear LIMSEQ_inverse_real_of_nat)
     have "?diff 1 ----> 0"
     proof (rule LIMSEQ_I)
       fix r :: real assume "0 < r"
@@ -3031,7 +3041,7 @@
       have "- (pi / 2) < 0" using pi_gt_zero by auto
       have "- (2 * pi) < 0" using pi_gt_zero by auto
       
-      have c_minus_minus: "\<And> i. ?c (- 1) i = - ?c 1 i" by auto
+      have c_minus_minus: "\<And> i. ?c (- 1) i = - ?c 1 i" unfolding One_nat_def by auto
     
       have "arctan (- 1) = arctan (tan (-(pi / 4)))" unfolding tan_45 tan_minus ..
       also have "\<dots> = - (pi / 4)" by (rule arctan_tan, auto simp add: order_less_trans[OF `- (pi / 2) < 0` pi_gt_zero])
@@ -3179,4 +3189,4 @@
 apply (erule polar_ex2)
 done
 
-end 
+end