# 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 \ 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 \ 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 \ (v::real) |] ==> \(x + u) - y\ \ 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 - (\m=0.. inverse(real (fact n)) * \x\ ^ 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 \ (\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: "(\n. f (Suc n)) ----> l \ 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: "(\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 "\summable f; \d. 0 < f (k + (Suc(Suc 0) * d)) + f (k + ((Suc(Suc 0) * d) + 1))\ \ setsum f {0..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 "(\ i = 0 ..< 2 * Suc n. if even i then f i else g i) = (\ i = 0 ..< n. f (2 * i)) + (\ 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 "\ = (\ i = 0 ..< Suc n. f (2 * i)) + (\ i = 0 ..< Suc n. g (2 * i + 1))" by auto finally show ?case . qed auto @@ -187,16 +187,18 @@ ((\n. l \ (\i=0..<2*n + 1. -1^i*a i)) \ (\ n. \i=0..<2*n + 1. -1^i*a i) ----> l)" (is "\l. ((\n. ?f n \ l) \ _) \ ((\n. l \ ?g n) \ _)") proof - - have fg_diff: "\n. ?f n - ?g n = - a (2 * n)" by auto + have fg_diff: "\n. ?f n - ?g n = - a (2 * n)" unfolding One_nat_def by auto have "\ n. ?f n \ ?f (Suc n)" proof fix n show "?f n \ ?f (Suc n)" using mono[of "2*n"] by auto qed moreover have "\ n. ?g (Suc n) \ ?g n" - proof fix n show "?g (Suc n) \ ?g n" using mono[of "Suc (2*n)"] by auto qed + proof fix n show "?g (Suc n) \ ?g n" using mono[of "Suc (2*n)"] + unfolding One_nat_def by auto qed moreover have "\ n. ?f n \ ?g n" - proof fix n show "?f n \ ?g n" using fg_diff a_pos by auto qed + proof fix n show "?f n \ ?g n" using fg_diff a_pos + unfolding One_nat_def by auto qed moreover have "(\ n. ?f n - ?g n) ----> 0" unfolding fg_diff proof (rule LIMSEQ_I) @@ -904,7 +906,7 @@ proof - have "(\n = 0..<1. f n * 0 ^ n) = (\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 \ {- 1<..<1}" and "(0 :: real) < 1" using `0 < x` `x < 2` by auto { fix x :: real assume "x \ {- 1<..<1}" hence "norm (-x) < 1" by auto show "summable (\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 (\x. suminf (?f x)) (x - 1) :> suminf (?f' x)" by auto + hence "DERIV (\x. suminf (?f x)) (x - 1) :> suminf (?f' x)" unfolding One_nat_def by auto hence "DERIV (\x. suminf (?f (x - 1))) x :> suminf (?f' x)" unfolding DERIV_iff repos . ultimately have "DERIV (\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 "\x\ \ 1" shows "monoseq (\ 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 \ 1" and "x \ 1" and "-1 \ x" using assms by auto @@ -2823,7 +2829,7 @@ lemma zeroseq_arctan_series: fixes x :: real assumes "\x\ \ 1" shows "(\ 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 \ 1" and "x \ 1" and "-1 \ x" using assms by auto @@ -2831,12 +2837,14 @@ proof (cases "\x\ < 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 "(\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 \ x = 1" using `\x\ \ 1` by auto - hence n_eq: "\ n. x ^ (n * 2 + 1) = x" by auto + hence n_eq: "\ 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 "\arctan x - (\i = 0.. \ (\i = 0..i = 0.. = ?c x n" by auto + also have "\ = ?c x n" unfolding One_nat_def by auto also have "\ = ?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 "\arctan x - (\i = 0.. \ (\i = 0..i = 0.. = - ?c x n" by auto + also have "\ = - ?c x n" unfolding One_nat_def by auto also have "\ = ?a x n" unfolding sgn_neg a_pos by auto finally show ?thesis . qed @@ -3011,7 +3019,9 @@ ultimately have "0 \ ?a 1 n - ?diff 1 n" by (rule LIM_less_bound) hence "?diff 1 n \ ?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: "\ i. ?c (- 1) i = - ?c 1 i" by auto + have c_minus_minus: "\ 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 "\ = - (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