make more proofs work whether or not One_nat_def is a simp rule
authorhuffman
Tue Feb 24 11:12:58 2009 -0800 (2009-02-24)
changeset 3008243c5b7bfc791
parent 30081 46b9c8ae3897
child 30084 776de457f214
child 30093 ecb557b021b2
make more proofs work whether or not One_nat_def is a simp rule
src/HOL/Fact.thy
src/HOL/GCD.thy
src/HOL/Integration.thy
src/HOL/MacLaurin.thy
src/HOL/RealDef.thy
src/HOL/RealPow.thy
src/HOL/SEQ.thy
src/HOL/Series.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Fact.thy	Tue Feb 24 11:10:05 2009 -0800
     1.2 +++ b/src/HOL/Fact.thy	Tue Feb 24 11:12:58 2009 -0800
     1.3 @@ -58,7 +58,7 @@
     1.4    "n < Suc m ==> fact (Suc m - n) = (Suc m - n) * fact (m - n)"
     1.5  apply (induct n arbitrary: m)
     1.6  apply auto
     1.7 -apply (drule_tac x = "m - 1" in meta_spec, auto)
     1.8 +apply (drule_tac x = "m - Suc 0" in meta_spec, auto)
     1.9  done
    1.10  
    1.11  lemma fact_num0: "fact 0 = 1"
     2.1 --- a/src/HOL/GCD.thy	Tue Feb 24 11:10:05 2009 -0800
     2.2 +++ b/src/HOL/GCD.thy	Tue Feb 24 11:12:58 2009 -0800
     2.3 @@ -60,9 +60,12 @@
     2.4  lemma gcd_non_0: "n > 0 \<Longrightarrow> gcd m n = gcd n (m mod n)"
     2.5    by simp
     2.6  
     2.7 -lemma gcd_1 [simp, algebra]: "gcd m (Suc 0) = 1"
     2.8 +lemma gcd_1 [simp, algebra]: "gcd m (Suc 0) = Suc 0"
     2.9    by simp
    2.10  
    2.11 +lemma nat_gcd_1_right [simp, algebra]: "gcd m 1 = 1"
    2.12 +  unfolding One_nat_def by (rule gcd_1)
    2.13 +
    2.14  declare gcd.simps [simp del]
    2.15  
    2.16  text {*
    2.17 @@ -116,9 +119,12 @@
    2.18    apply (blast intro: dvd_trans)
    2.19    done
    2.20  
    2.21 -lemma gcd_1_left [simp, algebra]: "gcd (Suc 0) m = 1"
    2.22 +lemma gcd_1_left [simp, algebra]: "gcd (Suc 0) m = Suc 0"
    2.23    by (simp add: gcd_commute)
    2.24  
    2.25 +lemma nat_gcd_1_left [simp, algebra]: "gcd 1 m = 1"
    2.26 +  unfolding One_nat_def by (rule gcd_1_left)
    2.27 +
    2.28  text {*
    2.29    \medskip Multiplication laws
    2.30  *}
     3.1 --- a/src/HOL/Integration.thy	Tue Feb 24 11:10:05 2009 -0800
     3.2 +++ b/src/HOL/Integration.thy	Tue Feb 24 11:12:58 2009 -0800
     3.3 @@ -134,7 +134,7 @@
     3.4  apply (frule partition [THEN iffD1], safe)
     3.5  apply (drule_tac x = "psize D" and P="%n. psize D \<le> n --> ?P n" in spec, safe)
     3.6  apply (case_tac "psize D = 0")
     3.7 -apply (drule_tac [2] n = "psize D - 1" in partition_lt, auto)
     3.8 +apply (drule_tac [2] n = "psize D - Suc 0" in partition_lt, auto)
     3.9  done
    3.10  
    3.11  lemma partition_gt: "[|partition(a,b) D; n < (psize D)|] ==> D(n) < D(psize D)"
    3.12 @@ -145,7 +145,7 @@
    3.13  apply (rotate_tac 2)
    3.14  apply (drule_tac x = "psize D" in spec)
    3.15  apply (rule ccontr)
    3.16 -apply (drule_tac n = "psize D - 1" in partition_lt)
    3.17 +apply (drule_tac n = "psize D - Suc 0" in partition_lt)
    3.18  apply auto
    3.19  done
    3.20  
     4.1 --- a/src/HOL/MacLaurin.thy	Tue Feb 24 11:10:05 2009 -0800
     4.2 +++ b/src/HOL/MacLaurin.thy	Tue Feb 24 11:12:58 2009 -0800
     4.3 @@ -81,7 +81,7 @@
     4.4    prefer 2 apply simp
     4.5   apply (frule less_iff_Suc_add [THEN iffD1], clarify)
     4.6   apply (simp del: setsum_op_ivl_Suc)
     4.7 - apply (insert sumr_offset4 [of 1])
     4.8 + apply (insert sumr_offset4 [of "Suc 0"])
     4.9   apply (simp del: setsum_op_ivl_Suc fact_Suc realpow_Suc)
    4.10   apply (rule lemma_DERIV_subst)
    4.11    apply (rule DERIV_add)
    4.12 @@ -124,7 +124,7 @@
    4.13  
    4.14    have g2: "g 0 = 0 & g h = 0"
    4.15      apply (simp add: m f_h g_def del: setsum_op_ivl_Suc)
    4.16 -    apply (cut_tac n = m and k = 1 in sumr_offset2)
    4.17 +    apply (cut_tac n = m and k = "Suc 0" in sumr_offset2)
    4.18      apply (simp add: eq_diff_eq' diff_0 del: setsum_op_ivl_Suc)
    4.19      done
    4.20  
    4.21 @@ -144,7 +144,7 @@
    4.22      apply (simp add: m difg_def)
    4.23      apply (frule less_iff_Suc_add [THEN iffD1], clarify)
    4.24      apply (simp del: setsum_op_ivl_Suc)
    4.25 -    apply (insert sumr_offset4 [of 1])
    4.26 +    apply (insert sumr_offset4 [of "Suc 0"])
    4.27      apply (simp del: setsum_op_ivl_Suc fact_Suc realpow_Suc)
    4.28      done
    4.29  
    4.30 @@ -552,6 +552,10 @@
    4.31      "[|x = y; abs u \<le> (v::real) |] ==> \<bar>(x + u) - y\<bar> \<le> v"
    4.32  by auto
    4.33  
    4.34 +text {* TODO: move to Parity.thy *}
    4.35 +lemma nat_odd_1 [simp]: "odd (1::nat)"
    4.36 +  unfolding even_nat_def by simp
    4.37 +
    4.38  lemma Maclaurin_sin_bound:
    4.39    "abs(sin x - (\<Sum>m=0..<n. (if even m then 0 else (-1 ^ ((m - Suc 0) div 2)) / real (fact m)) *
    4.40    x ^ m))  \<le> inverse(real (fact n)) * \<bar>x\<bar> ^ n"
     5.1 --- a/src/HOL/RealDef.thy	Tue Feb 24 11:10:05 2009 -0800
     5.2 +++ b/src/HOL/RealDef.thy	Tue Feb 24 11:12:58 2009 -0800
     5.3 @@ -705,6 +705,9 @@
     5.4  lemma real_of_nat_zero [simp]: "real (0::nat) = 0"
     5.5  by (simp add: real_of_nat_def)
     5.6  
     5.7 +lemma real_of_nat_1 [simp]: "real (1::nat) = 1"
     5.8 +by (simp add: real_of_nat_def)
     5.9 +
    5.10  lemma real_of_nat_one [simp]: "real (Suc 0) = (1::real)"
    5.11  by (simp add: real_of_nat_def)
    5.12  
     6.1 --- a/src/HOL/RealPow.thy	Tue Feb 24 11:10:05 2009 -0800
     6.2 +++ b/src/HOL/RealPow.thy	Tue Feb 24 11:12:58 2009 -0800
     6.3 @@ -44,7 +44,8 @@
     6.4  by (insert power_decreasing [of 1 "Suc n" r], simp)
     6.5  
     6.6  lemma realpow_minus_mult [rule_format]:
     6.7 -     "0 < n --> (x::real) ^ (n - 1) * x = x ^ n" 
     6.8 +     "0 < n --> (x::real) ^ (n - 1) * x = x ^ n"
     6.9 +unfolding One_nat_def
    6.10  apply (simp split add: nat_diff_split)
    6.11  done
    6.12  
     7.1 --- a/src/HOL/SEQ.thy	Tue Feb 24 11:10:05 2009 -0800
     7.2 +++ b/src/HOL/SEQ.thy	Tue Feb 24 11:12:58 2009 -0800
     7.3 @@ -338,10 +338,10 @@
     7.4  done
     7.5  
     7.6  lemma LIMSEQ_Suc: "f ----> l \<Longrightarrow> (\<lambda>n. f (Suc n)) ----> l"
     7.7 -by (drule_tac k="1" in LIMSEQ_ignore_initial_segment, simp)
     7.8 +by (drule_tac k="Suc 0" in LIMSEQ_ignore_initial_segment, simp)
     7.9  
    7.10  lemma LIMSEQ_imp_Suc: "(\<lambda>n. f (Suc n)) ----> l \<Longrightarrow> f ----> l"
    7.11 -by (rule_tac k="1" in LIMSEQ_offset, simp)
    7.12 +by (rule_tac k="Suc 0" in LIMSEQ_offset, simp)
    7.13  
    7.14  lemma LIMSEQ_Suc_iff: "(\<lambda>n. f (Suc n)) ----> l = f ----> l"
    7.15  by (blast intro: LIMSEQ_imp_Suc LIMSEQ_Suc)
     8.1 --- a/src/HOL/Series.thy	Tue Feb 24 11:10:05 2009 -0800
     8.2 +++ b/src/HOL/Series.thy	Tue Feb 24 11:12:58 2009 -0800
     8.3 @@ -312,6 +312,7 @@
     8.4    shows "\<lbrakk>summable f;
     8.5          \<forall>d. 0 < f (k + (Suc(Suc 0) * d)) + f (k + ((Suc(Suc 0) * d) + 1))\<rbrakk>
     8.6        \<Longrightarrow> setsum f {0..<k} < suminf f"
     8.7 +unfolding One_nat_def
     8.8  apply (subst suminf_split_initial_segment [where k="k"])
     8.9  apply assumption
    8.10  apply simp
    8.11 @@ -537,7 +538,7 @@
    8.12  apply (safe, subgoal_tac "\<forall>n. N < n --> f (n) = 0")
    8.13   prefer 2
    8.14   apply clarify
    8.15 - apply(erule_tac x = "n - 1" in allE)
    8.16 + apply(erule_tac x = "n - Suc 0" in allE)
    8.17   apply (simp add:diff_Suc split:nat.splits)
    8.18   apply (blast intro: norm_ratiotest_lemma)
    8.19  apply (rule_tac x = "Suc N" in exI, clarify)
     9.1 --- a/src/HOL/Transcendental.thy	Tue Feb 24 11:10:05 2009 -0800
     9.2 +++ b/src/HOL/Transcendental.thy	Tue Feb 24 11:12:58 2009 -0800
     9.3 @@ -120,7 +120,7 @@
     9.4    case (Suc n)
     9.5    have "(\<Sum> i = 0 ..< 2 * Suc n. if even i then f i else g i) = 
     9.6          (\<Sum> i = 0 ..< n. f (2 * i)) + (\<Sum> i = 0 ..< n. g (2 * i + 1)) + (f (2 * n) + g (2 * n + 1))"
     9.7 -    using Suc.hyps by auto
     9.8 +    using Suc.hyps unfolding One_nat_def by auto
     9.9    also have "\<dots> = (\<Sum> i = 0 ..< Suc n. f (2 * i)) + (\<Sum> i = 0 ..< Suc n. g (2 * i + 1))" by auto
    9.10    finally show ?case .
    9.11  qed auto
    9.12 @@ -187,16 +187,18 @@
    9.13               ((\<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)"
    9.14    (is "\<exists>l. ((\<forall>n. ?f n \<le> l) \<and> _) \<and> ((\<forall>n. l \<le> ?g n) \<and> _)")
    9.15  proof -
    9.16 -  have fg_diff: "\<And>n. ?f n - ?g n = - a (2 * n)" by auto
    9.17 +  have fg_diff: "\<And>n. ?f n - ?g n = - a (2 * n)" unfolding One_nat_def by auto
    9.18  
    9.19    have "\<forall> n. ?f n \<le> ?f (Suc n)"
    9.20    proof fix n show "?f n \<le> ?f (Suc n)" using mono[of "2*n"] by auto qed
    9.21    moreover
    9.22    have "\<forall> n. ?g (Suc n) \<le> ?g n"
    9.23 -  proof fix n show "?g (Suc n) \<le> ?g n" using mono[of "Suc (2*n)"] by auto qed
    9.24 +  proof fix n show "?g (Suc n) \<le> ?g n" using mono[of "Suc (2*n)"]
    9.25 +    unfolding One_nat_def by auto qed
    9.26    moreover
    9.27    have "\<forall> n. ?f n \<le> ?g n" 
    9.28 -  proof fix n show "?f n \<le> ?g n" using fg_diff a_pos by auto qed
    9.29 +  proof fix n show "?f n \<le> ?g n" using fg_diff a_pos
    9.30 +    unfolding One_nat_def by auto qed
    9.31    moreover
    9.32    have "(\<lambda> n. ?f n - ?g n) ----> 0" unfolding fg_diff
    9.33    proof (rule LIMSEQ_I)
    9.34 @@ -904,7 +906,7 @@
    9.35  proof -
    9.36    have "(\<Sum>n = 0..<1. f n * 0 ^ n) = (\<Sum>n. f n * 0 ^ n)"
    9.37      by (rule sums_unique [OF series_zero], simp add: power_0_left)
    9.38 -  thus ?thesis by simp
    9.39 +  thus ?thesis unfolding One_nat_def by simp
    9.40  qed
    9.41  
    9.42  lemma exp_zero [simp]: "exp 0 = 1"
    9.43 @@ -1234,10 +1236,11 @@
    9.44        show "x - 1 \<in> {- 1<..<1}" and "(0 :: real) < 1" using `0 < x` `x < 2` by auto
    9.45        { fix x :: real assume "x \<in> {- 1<..<1}" hence "norm (-x) < 1" by auto
    9.46  	show "summable (\<lambda>n. -1 ^ n * (1 / real (n + 1)) * real (Suc n) * x ^ n)"
    9.47 +          unfolding One_nat_def
    9.48  	  by (auto simp del: power_mult_distrib simp add: power_mult_distrib[symmetric] summable_geometric[OF `norm (-x) < 1`])
    9.49        }
    9.50      qed
    9.51 -    hence "DERIV (\<lambda>x. suminf (?f x)) (x - 1) :> suminf (?f' x)" by auto
    9.52 +    hence "DERIV (\<lambda>x. suminf (?f x)) (x - 1) :> suminf (?f' x)" unfolding One_nat_def by auto
    9.53      hence "DERIV (\<lambda>x. suminf (?f (x - 1))) x :> suminf (?f' x)" unfolding DERIV_iff repos .
    9.54      ultimately have "DERIV (\<lambda>x. ln x - suminf (?f (x - 1))) x :> (suminf (?f' x) - suminf (?f' x))"
    9.55        by (rule DERIV_diff)
    9.56 @@ -1514,6 +1517,7 @@
    9.57  
    9.58  lemma DERIV_fun_pow: "DERIV g x :> m ==>  
    9.59        DERIV (%x. (g x) ^ n) x :> real n * (g x) ^ (n - 1) * m"
    9.60 +unfolding One_nat_def
    9.61  apply (rule lemma_DERIV_subst)
    9.62  apply (rule_tac f = "(%x. x ^ n)" in DERIV_chain2)
    9.63  apply (rule DERIV_pow, auto)
    9.64 @@ -1635,7 +1639,7 @@
    9.65  	sums sin x"
    9.66      unfolding sin_def
    9.67      by (rule sin_converges [THEN sums_summable, THEN sums_group], simp) 
    9.68 -  thus ?thesis by (simp add: mult_ac)
    9.69 +  thus ?thesis unfolding One_nat_def by (simp add: mult_ac)
    9.70  qed
    9.71  
    9.72  lemma sin_gt_zero: "[|0 < x; x < 2 |] ==> 0 < sin x"
    9.73 @@ -1647,6 +1651,7 @@
    9.74   apply (rule sin_paired [THEN sums_summable, THEN sums_group], simp) 
    9.75  apply (rotate_tac 2)
    9.76  apply (drule sin_paired [THEN sums_unique, THEN ssubst])
    9.77 +unfolding One_nat_def
    9.78  apply (auto simp del: fact_Suc realpow_Suc)
    9.79  apply (frule sums_unique)
    9.80  apply (auto simp del: fact_Suc realpow_Suc)
    9.81 @@ -1720,6 +1725,7 @@
    9.82  apply (simp (no_asm) add: mult_assoc del: setsum_op_ivl_Suc)
    9.83  apply (rule sumr_pos_lt_pair)
    9.84  apply (erule sums_summable, safe)
    9.85 +unfolding One_nat_def
    9.86  apply (simp (no_asm) add: divide_inverse real_0_less_add_iff mult_assoc [symmetric] 
    9.87              del: fact_Suc)
    9.88  apply (rule real_mult_inverse_cancel2)
    9.89 @@ -2792,7 +2798,7 @@
    9.90  
    9.91  lemma monoseq_arctan_series: fixes x :: real
    9.92    assumes "\<bar>x\<bar> \<le> 1" shows "monoseq (\<lambda> n. 1 / real (n*2+1) * x^(n*2+1))" (is "monoseq ?a")
    9.93 -proof (cases "x = 0") case True thus ?thesis unfolding monoseq_def by auto
    9.94 +proof (cases "x = 0") case True thus ?thesis unfolding monoseq_def One_nat_def by auto
    9.95  next
    9.96    case False
    9.97    have "norm x \<le> 1" and "x \<le> 1" and "-1 \<le> x" using assms by auto
    9.98 @@ -2823,7 +2829,7 @@
    9.99  
   9.100  lemma zeroseq_arctan_series: fixes x :: real
   9.101    assumes "\<bar>x\<bar> \<le> 1" shows "(\<lambda> n. 1 / real (n*2+1) * x^(n*2+1)) ----> 0" (is "?a ----> 0")
   9.102 -proof (cases "x = 0") case True thus ?thesis by (auto simp add: LIMSEQ_const)
   9.103 +proof (cases "x = 0") case True thus ?thesis unfolding One_nat_def by (auto simp add: LIMSEQ_const)
   9.104  next
   9.105    case False
   9.106    have "norm x \<le> 1" and "x \<le> 1" and "-1 \<le> x" using assms by auto
   9.107 @@ -2831,12 +2837,14 @@
   9.108    proof (cases "\<bar>x\<bar> < 1")
   9.109      case True hence "norm x < 1" by auto
   9.110      from LIMSEQ_mult[OF LIMSEQ_inverse_real_of_nat LIMSEQ_power_zero[OF `norm x < 1`, THEN LIMSEQ_Suc]]
   9.111 -    show ?thesis unfolding inverse_eq_divide Suc_plus1 using LIMSEQ_linear[OF _ pos2] by auto
   9.112 +    have "(\<lambda>n. 1 / real (n + 1) * x ^ (n + 1)) ----> 0"
   9.113 +      unfolding inverse_eq_divide Suc_plus1 by simp
   9.114 +    then show ?thesis using pos2 by (rule LIMSEQ_linear)
   9.115    next
   9.116      case False hence "x = -1 \<or> x = 1" using `\<bar>x\<bar> \<le> 1` by auto
   9.117 -    hence n_eq: "\<And> n. x ^ (n * 2 + 1) = x" by auto
   9.118 +    hence n_eq: "\<And> n. x ^ (n * 2 + 1) = x" unfolding One_nat_def by auto
   9.119      from LIMSEQ_mult[OF LIMSEQ_inverse_real_of_nat[THEN LIMSEQ_linear, OF pos2, unfolded inverse_eq_divide] LIMSEQ_const[of x]]
   9.120 -    show ?thesis unfolding n_eq by auto
   9.121 +    show ?thesis unfolding n_eq Suc_plus1 by auto
   9.122    qed
   9.123  qed
   9.124  
   9.125 @@ -2989,7 +2997,7 @@
   9.126  	  from `even n` obtain m where "2 * m = n" unfolding even_mult_two_ex by auto
   9.127  	  from bounds[of m, unfolded this atLeastAtMost_iff]
   9.128  	  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
   9.129 -	  also have "\<dots> = ?c x n" by auto
   9.130 +	  also have "\<dots> = ?c x n" unfolding One_nat_def by auto
   9.131  	  also have "\<dots> = ?a x n" unfolding sgn_pos a_pos by auto
   9.132  	  finally show ?thesis .
   9.133  	next
   9.134 @@ -2998,7 +3006,7 @@
   9.135  	  hence m_plus: "2 * (m + 1) = n + 1" by auto
   9.136  	  from bounds[of "m + 1", unfolded this atLeastAtMost_iff, THEN conjunct1] bounds[of m, unfolded m_def atLeastAtMost_iff, THEN conjunct2]
   9.137  	  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
   9.138 -	  also have "\<dots> = - ?c x n" by auto
   9.139 +	  also have "\<dots> = - ?c x n" unfolding One_nat_def by auto
   9.140  	  also have "\<dots> = ?a x n" unfolding sgn_neg a_pos by auto
   9.141  	  finally show ?thesis .
   9.142  	qed
   9.143 @@ -3011,7 +3019,9 @@
   9.144        ultimately have "0 \<le> ?a 1 n - ?diff 1 n" by (rule LIM_less_bound)
   9.145        hence "?diff 1 n \<le> ?a 1 n" by auto
   9.146      }
   9.147 -    have "?a 1 ----> 0" unfolding LIMSEQ_rabs_zero power_one divide_inverse by (auto intro!: LIMSEQ_mult LIMSEQ_linear LIMSEQ_inverse_real_of_nat)
   9.148 +    have "?a 1 ----> 0"
   9.149 +      unfolding LIMSEQ_rabs_zero power_one divide_inverse One_nat_def
   9.150 +      by (auto intro!: LIMSEQ_mult LIMSEQ_linear LIMSEQ_inverse_real_of_nat)
   9.151      have "?diff 1 ----> 0"
   9.152      proof (rule LIMSEQ_I)
   9.153        fix r :: real assume "0 < r"
   9.154 @@ -3031,7 +3041,7 @@
   9.155        have "- (pi / 2) < 0" using pi_gt_zero by auto
   9.156        have "- (2 * pi) < 0" using pi_gt_zero by auto
   9.157        
   9.158 -      have c_minus_minus: "\<And> i. ?c (- 1) i = - ?c 1 i" by auto
   9.159 +      have c_minus_minus: "\<And> i. ?c (- 1) i = - ?c 1 i" unfolding One_nat_def by auto
   9.160      
   9.161        have "arctan (- 1) = arctan (tan (-(pi / 4)))" unfolding tan_45 tan_minus ..
   9.162        also have "\<dots> = - (pi / 4)" by (rule arctan_tan, auto simp add: order_less_trans[OF `- (pi / 2) < 0` pi_gt_zero])
   9.163 @@ -3179,4 +3189,4 @@
   9.164  apply (erule polar_ex2)
   9.165  done
   9.166  
   9.167 -end 
   9.168 +end