--- 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"
--- 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
*}
--- 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
--- 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"
--- 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)
--- 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
--- 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)
--- 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)
--- 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