author  nipkow 
Sun, 21 Oct 2007 14:53:44 +0200  
changeset 25134  3d4953e88449 
parent 25112  98824cc791c0 
child 25162  ad4d5365d9d8 
permissions  rwrr 
15944  1 
(* ID : $Id$ 
12224  2 
Author : Jacques D. Fleuriot 
3 
Copyright : 2001 University of Edinburgh 

15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

4 
Conversion to Isar and new proofs by Lawrence C Paulson, 2004 
12224  5 
*) 
6 

15944  7 
header{*MacLaurin Series*} 
8 

15131  9 
theory MacLaurin 
22983  10 
imports Transcendental 
15131  11 
begin 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

12 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

13 
subsection{*Maclaurin's Theorem with Lagrange Form of Remainder*} 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

14 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

15 
text{*This is a very long, messy proof even now that it's been broken down 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

16 
into lemmas.*} 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

17 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

18 
lemma Maclaurin_lemma: 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

19 
"0 < h ==> 
15539  20 
\<exists>B. f h = (\<Sum>m=0..<n. (j m / real (fact m)) * (h^m)) + 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

21 
(B * ((h^n) / real(fact n)))" 
15539  22 
apply (rule_tac x = "(f h  (\<Sum>m=0..<n. (j m / real (fact m)) * h^m)) * 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

23 
real(fact n) / (h^n)" 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

24 
in exI) 
15539  25 
apply (simp) 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

26 
done 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

27 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

28 
lemma eq_diff_eq': "(x = y  z) = (y = x + (z::real))" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

29 
by arith 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

30 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

31 
text{*A crude tactic to differentiate by proof.*} 
24180  32 

33 
lemmas deriv_rulesI = 

34 
DERIV_ident DERIV_const DERIV_cos DERIV_cmult 

35 
DERIV_sin DERIV_exp DERIV_inverse DERIV_pow 

36 
DERIV_add DERIV_diff DERIV_mult DERIV_minus 

37 
DERIV_inverse_fun DERIV_quotient DERIV_fun_pow 

38 
DERIV_fun_exp DERIV_fun_sin DERIV_fun_cos 

39 
DERIV_ident DERIV_const DERIV_cos 

40 

15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

41 
ML 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

42 
{* 
19765  43 
local 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

44 
exception DERIV_name; 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

45 
fun get_fun_name (_ $ (Const ("Lim.deriv",_) $ Abs(_,_, Const (f,_) $ _) $ _ $ _)) = f 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

46 
 get_fun_name (_ $ (_ $ (Const ("Lim.deriv",_) $ Abs(_,_, Const (f,_) $ _) $ _ $ _))) = f 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

47 
 get_fun_name _ = raise DERIV_name; 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

48 

24180  49 
in 
50 

15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

51 
val deriv_tac = 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

52 
SUBGOAL (fn (prem,i) => 
24180  53 
(resolve_tac @{thms deriv_rulesI} i) ORELSE 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

54 
((rtac (read_instantiate [("f",get_fun_name prem)] 
24180  55 
@{thm DERIV_chain2}) i) handle DERIV_name => no_tac));; 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

56 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

57 
val DERIV_tac = ALLGOALS(fn i => REPEAT(deriv_tac i)); 
19765  58 

59 
end 

15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

60 
*} 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

61 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

62 
lemma Maclaurin_lemma2: 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

63 
"[ \<forall>m t. m < n \<and> 0\<le>t \<and> t\<le>h \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t; 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

64 
n = Suc k; 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

65 
difg = 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

66 
(\<lambda>m t. diff m t  
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

67 
((\<Sum>p = 0..<n  m. diff (m + p) 0 / real (fact p) * t ^ p) + 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

68 
B * (t ^ (n  m) / real (fact (n  m)))))] ==> 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

69 
\<forall>m t. m < n & 0 \<le> t & t \<le> h > 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

70 
DERIV (difg m) t :> difg (Suc m) t" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

71 
apply clarify 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

72 
apply (rule DERIV_diff) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

73 
apply (simp (no_asm_simp)) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

74 
apply (tactic DERIV_tac) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

75 
apply (tactic DERIV_tac) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

76 
apply (rule_tac [2] lemma_DERIV_subst) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

77 
apply (rule_tac [2] DERIV_quotient) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

78 
apply (rule_tac [3] DERIV_const) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

79 
apply (rule_tac [2] DERIV_pow) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

80 
prefer 3 apply (simp add: fact_diff_Suc) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

81 
prefer 2 apply simp 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

82 
apply (frule_tac m = m in less_add_one, clarify) 
15561  83 
apply (simp del: setsum_op_ivl_Suc) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

84 
apply (insert sumr_offset4 [of 1]) 
15561  85 
apply (simp del: setsum_op_ivl_Suc fact_Suc realpow_Suc) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

86 
apply (rule lemma_DERIV_subst) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

87 
apply (rule DERIV_add) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

88 
apply (rule_tac [2] DERIV_const) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

89 
apply (rule DERIV_sumr, clarify) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

90 
prefer 2 apply simp 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

91 
apply (simp (no_asm) add: divide_inverse mult_assoc del: fact_Suc realpow_Suc) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

92 
apply (rule DERIV_cmult) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

93 
apply (rule lemma_DERIV_subst) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

94 
apply (best intro: DERIV_chain2 intro!: DERIV_intros) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

95 
apply (subst fact_Suc) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

96 
apply (subst real_of_nat_mult) 
15539  97 
apply (simp add: mult_ac) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

98 
done 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

99 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

100 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

101 
lemma Maclaurin_lemma3: 
20792  102 
fixes difg :: "nat => real => real" shows 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

103 
"[\<forall>k t. k < Suc m \<and> 0\<le>t & t\<le>h \<longrightarrow> DERIV (difg k) t :> difg (Suc k) t; 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

104 
\<forall>k<Suc m. difg k 0 = 0; DERIV (difg n) t :> 0; n < m; 0 < t; 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

105 
t < h] 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

106 
==> \<exists>ta. 0 < ta & ta < t & DERIV (difg (Suc n)) ta :> 0" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

107 
apply (rule Rolle, assumption, simp) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

108 
apply (drule_tac x = n and P="%k. k<Suc m > difg k 0 = 0" in spec) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

109 
apply (rule DERIV_unique) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

110 
prefer 2 apply assumption 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

111 
apply force 
24998  112 
apply (metis DERIV_isCont dlo_simps(4) dlo_simps(9) less_trans_Suc nat_less_le not_less_eq real_le_trans) 
113 
apply (metis Suc_less_eq differentiableI dlo_simps(7) dlo_simps(8) dlo_simps(9) real_le_trans xt1(8)) 

15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

114 
done 
14738  115 

15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

116 
lemma Maclaurin: 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

117 
"[ 0 < h; n \<noteq> 0; diff 0 = f; 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

118 
\<forall>m t. m < n & 0 \<le> t & t \<le> h > DERIV (diff m) t :> diff (Suc m) t ] 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

119 
==> \<exists>t. 0 < t & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

120 
t < h & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

121 
f h = 
15539  122 
setsum (%m. (diff m 0 / real (fact m)) * h ^ m) {0..<n} + 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

123 
(diff n t / real (fact n)) * h ^ n" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

124 
apply (case_tac "n = 0", force) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

125 
apply (drule not0_implies_Suc) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

126 
apply (erule exE) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

127 
apply (frule_tac f=f and n=n and j="%m. diff m 0" in Maclaurin_lemma) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

128 
apply (erule exE) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

129 
apply (subgoal_tac "\<exists>g. 
15539  130 
g = (%t. f t  (setsum (%m. (diff m 0 / real(fact m)) * t^m) {0..<n} + (B * (t^n / real(fact n)))))") 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

131 
prefer 2 apply blast 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

132 
apply (erule exE) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

133 
apply (subgoal_tac "g 0 = 0 & g h =0") 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

134 
prefer 2 
15561  135 
apply (simp del: setsum_op_ivl_Suc) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

136 
apply (cut_tac n = m and k = 1 in sumr_offset2) 
15561  137 
apply (simp add: eq_diff_eq' del: setsum_op_ivl_Suc) 
15539  138 
apply (subgoal_tac "\<exists>difg. difg = (%m t. diff m t  (setsum (%p. (diff (m + p) 0 / real (fact p)) * (t ^ p)) {0..<nm} + (B * ((t ^ (n  m)) / real (fact (n  m))))))") 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

139 
prefer 2 apply blast 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

140 
apply (erule exE) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

141 
apply (subgoal_tac "difg 0 = g") 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

142 
prefer 2 apply simp 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

143 
apply (frule Maclaurin_lemma2, assumption+) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

144 
apply (subgoal_tac "\<forall>ma. ma < n > (\<exists>t. 0 < t & t < h & difg (Suc ma) t = 0) ") 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

145 
apply (drule_tac x = m and P="%m. m<n > (\<exists>t. ?QQ m t)" in spec) 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

146 
apply (erule impE) 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

147 
apply (simp (no_asm_simp)) 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

148 
apply (erule exE) 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

149 
apply (rule_tac x = t in exI) 
15539  150 
apply (simp del: realpow_Suc fact_Suc) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

151 
apply (subgoal_tac "\<forall>m. m < n > difg m 0 = 0") 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

152 
prefer 2 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

153 
apply clarify 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

154 
apply simp 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

155 
apply (frule_tac m = ma in less_add_one, clarify) 
15561  156 
apply (simp del: setsum_op_ivl_Suc) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

157 
apply (insert sumr_offset4 [of 1]) 
15561  158 
apply (simp del: setsum_op_ivl_Suc fact_Suc realpow_Suc) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

159 
apply (subgoal_tac "\<forall>m. m < n > (\<exists>t. 0 < t & t < h & DERIV (difg m) t :> 0) ") 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

160 
apply (rule allI, rule impI) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

161 
apply (drule_tac x = ma and P="%m. m<n > (\<exists>t. ?QQ m t)" in spec) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

162 
apply (erule impE, assumption) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

163 
apply (erule exE) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

164 
apply (rule_tac x = t in exI) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

165 
(* do some tidying up *) 
15539  166 
apply (erule_tac [!] V= "difg = (%m t. diff m t  (setsum (%p. diff (m + p) 0 / real (fact p) * t ^ p) {0..<nm} + B * (t ^ (n  m) / real (fact (n  m)))))" 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

167 
in thin_rl) 
15539  168 
apply (erule_tac [!] V="g = (%t. f t  (setsum (%m. diff m 0 / real (fact m) * t ^ m) {0..<n} + B * (t ^ n / real (fact n))))" 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

169 
in thin_rl) 
15539  170 
apply (erule_tac [!] V="f h = setsum (%m. diff m 0 / real (fact m) * h ^ m) {0..<n} + B * (h ^ n / real (fact n))" 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

171 
in thin_rl) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

172 
(* back to business *) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

173 
apply (simp (no_asm_simp)) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

174 
apply (rule DERIV_unique) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

175 
prefer 2 apply blast 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

176 
apply force 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

177 
apply (rule allI, induct_tac "ma") 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

178 
apply (rule impI, rule Rolle, assumption, simp, simp) 
24998  179 
apply (metis DERIV_isCont zero_less_Suc) 
180 
apply (metis One_nat_def differentiableI dlo_simps(7)) 

15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

181 
apply safe 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

182 
apply force 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

183 
apply (frule Maclaurin_lemma3, assumption+, safe) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

184 
apply (rule_tac x = ta in exI, force) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

185 
done 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

186 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

187 
lemma Maclaurin_objl: 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

188 
"0 < h & n\<noteq>0 & diff 0 = f & 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

189 
(\<forall>m t. m < n & 0 \<le> t & t \<le> h > DERIV (diff m) t :> diff (Suc m) t) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

190 
> (\<exists>t. 0 < t & t < h & 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

191 
f h = (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) + 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

192 
diff n t / real (fact n) * h ^ n)" 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

193 
by (blast intro: Maclaurin) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

194 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

195 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

196 
lemma Maclaurin2: 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

197 
"[ 0 < h; diff 0 = f; 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

198 
\<forall>m t. 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

199 
m < n & 0 \<le> t & t \<le> h > DERIV (diff m) t :> diff (Suc m) t ] 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

200 
==> \<exists>t. 0 < t & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

201 
t \<le> h & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

202 
f h = 
15539  203 
(\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) + 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

204 
diff n t / real (fact n) * h ^ n" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

205 
apply (case_tac "n", auto) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

206 
apply (drule Maclaurin, auto) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

207 
done 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

208 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

209 
lemma Maclaurin2_objl: 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

210 
"0 < h & diff 0 = f & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

211 
(\<forall>m t. 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

212 
m < n & 0 \<le> t & t \<le> h > DERIV (diff m) t :> diff (Suc m) t) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

213 
> (\<exists>t. 0 < t & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

214 
t \<le> h & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

215 
f h = 
15539  216 
(\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) + 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

217 
diff n t / real (fact n) * h ^ n)" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

218 
by (blast intro: Maclaurin2) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

219 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

220 
lemma Maclaurin_minus: 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

221 
"[ h < 0; n \<noteq> 0; diff 0 = f; 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

222 
\<forall>m t. m < n & h \<le> t & t \<le> 0 > DERIV (diff m) t :> diff (Suc m) t ] 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

223 
==> \<exists>t. h < t & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

224 
t < 0 & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

225 
f h = 
15539  226 
(\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) + 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

227 
diff n t / real (fact n) * h ^ n" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

228 
apply (cut_tac f = "%x. f (x)" 
23177  229 
and diff = "%n x. (1 ^ n) * diff n (x)" 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

230 
and h = "h" and n = n in Maclaurin_objl) 
15539  231 
apply (simp) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

232 
apply safe 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

233 
apply (subst minus_mult_right) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

234 
apply (rule DERIV_cmult) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

235 
apply (rule lemma_DERIV_subst) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

236 
apply (rule DERIV_chain2 [where g=uminus]) 
23069
cdfff0241c12
rename lemmas LIM_ident, isCont_ident, DERIV_ident
huffman
parents:
22985
diff
changeset

237 
apply (rule_tac [2] DERIV_minus, rule_tac [2] DERIV_ident) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

238 
prefer 2 apply force 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

239 
apply force 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

240 
apply (rule_tac x = "t" in exI, auto) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

241 
apply (subgoal_tac "(\<Sum>m = 0..<n. 1 ^ m * diff m 0 * (h)^m / real(fact m)) = 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

242 
(\<Sum>m = 0..<n. diff m 0 * h ^ m / real(fact m))") 
15536  243 
apply (rule_tac [2] setsum_cong[OF refl]) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

244 
apply (auto simp add: divide_inverse power_mult_distrib [symmetric]) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

245 
done 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

246 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

247 
lemma Maclaurin_minus_objl: 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

248 
"(h < 0 & n \<noteq> 0 & diff 0 = f & 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

249 
(\<forall>m t. 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

250 
m < n & h \<le> t & t \<le> 0 > DERIV (diff m) t :> diff (Suc m) t)) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

251 
> (\<exists>t. h < t & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

252 
t < 0 & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

253 
f h = 
15539  254 
(\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) + 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

255 
diff n t / real (fact n) * h ^ n)" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

256 
by (blast intro: Maclaurin_minus) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

257 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

258 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

259 
subsection{*More Convenient "Bidirectional" Version.*} 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

260 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

261 
(* not good for PVS sin_approx, cos_approx *) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

262 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

263 
lemma Maclaurin_bi_le_lemma [rule_format]: 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

264 
"n\<noteq>0 \<longrightarrow> 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

265 
diff 0 0 = 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

266 
(\<Sum>m = 0..<n. diff m 0 * 0 ^ m / real (fact m)) + 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

267 
diff n 0 * 0 ^ n / real (fact n)" 
15251  268 
by (induct "n", auto) 
14738  269 

15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

270 
lemma Maclaurin_bi_le: 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

271 
"[ diff 0 = f; 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

272 
\<forall>m t. m < n & abs t \<le> abs x > DERIV (diff m) t :> diff (Suc m) t ] 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

273 
==> \<exists>t. abs t \<le> abs x & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

274 
f x = 
15539  275 
(\<Sum>m=0..<n. diff m 0 / real (fact m) * x ^ m) + 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

276 
diff n t / real (fact n) * x ^ n" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

277 
apply (case_tac "n = 0", force) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

278 
apply (case_tac "x = 0") 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

279 
apply (rule_tac x = 0 in exI) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

280 
apply (force simp add: Maclaurin_bi_le_lemma) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

281 
apply (cut_tac x = x and y = 0 in linorder_less_linear, auto) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

282 
txt{*Case 1, where @{term "x < 0"}*} 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

283 
apply (cut_tac f = "diff 0" and diff = diff and h = x and n = n in Maclaurin_minus_objl, safe) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

284 
apply (simp add: abs_if) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

285 
apply (rule_tac x = t in exI) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

286 
apply (simp add: abs_if) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

287 
txt{*Case 2, where @{term "0 < x"}*} 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

288 
apply (cut_tac f = "diff 0" and diff = diff and h = x and n = n in Maclaurin_objl, safe) 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

289 
apply (simp add: abs_if) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

290 
apply (rule_tac x = t in exI) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

291 
apply (simp add: abs_if) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

292 
done 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

293 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

294 
lemma Maclaurin_all_lt: 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

295 
"[ diff 0 = f; 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

296 
\<forall>m x. DERIV (diff m) x :> diff(Suc m) x; 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

297 
x ~= 0; n \<noteq> 0 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

298 
] ==> \<exists>t. 0 < abs t & abs t < abs x & 
15539  299 
f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) + 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

300 
(diff n t / real (fact n)) * x ^ n" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

301 
apply (rule_tac x = x and y = 0 in linorder_cases) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

302 
prefer 2 apply blast 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

303 
apply (drule_tac [2] diff=diff in Maclaurin) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

304 
apply (drule_tac diff=diff in Maclaurin_minus, simp_all, safe) 
15229  305 
apply (rule_tac [!] x = t in exI, auto) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

306 
done 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

307 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

308 
lemma Maclaurin_all_lt_objl: 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

309 
"diff 0 = f & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

310 
(\<forall>m x. DERIV (diff m) x :> diff(Suc m) x) & 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

311 
x ~= 0 & n \<noteq> 0 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

312 
> (\<exists>t. 0 < abs t & abs t < abs x & 
15539  313 
f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) + 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

314 
(diff n t / real (fact n)) * x ^ n)" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

315 
by (blast intro: Maclaurin_all_lt) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

316 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

317 
lemma Maclaurin_zero [rule_format]: 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

318 
"x = (0::real) 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

319 
==> n \<noteq> 0 > 
15539  320 
(\<Sum>m=0..<n. (diff m (0::real) / real (fact m)) * x ^ m) = 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

321 
diff 0 0" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

322 
by (induct n, auto) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

323 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

324 
lemma Maclaurin_all_le: "[ diff 0 = f; 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

325 
\<forall>m x. DERIV (diff m) x :> diff (Suc m) x 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

326 
] ==> \<exists>t. abs t \<le> abs x & 
15539  327 
f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) + 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

328 
(diff n t / real (fact n)) * x ^ n" 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

329 
apply(cases "n=0") 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

330 
apply (force) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

331 
apply (case_tac "x = 0") 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

332 
apply (frule_tac diff = diff and n = n in Maclaurin_zero, assumption) 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

333 
apply (drule not0_implies_Suc) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

334 
apply (rule_tac x = 0 in exI, force) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

335 
apply (frule_tac diff = diff and n = n in Maclaurin_all_lt, auto) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

336 
apply (rule_tac x = t in exI, auto) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

337 
done 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

338 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

339 
lemma Maclaurin_all_le_objl: "diff 0 = f & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

340 
(\<forall>m x. DERIV (diff m) x :> diff (Suc m) x) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

341 
> (\<exists>t. abs t \<le> abs x & 
15539  342 
f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) + 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

343 
(diff n t / real (fact n)) * x ^ n)" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

344 
by (blast intro: Maclaurin_all_le) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

345 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

346 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

347 
subsection{*Version for Exponential Function*} 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

348 

25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

349 
lemma Maclaurin_exp_lt: "[ x ~= 0; n \<noteq> 0 ] 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

350 
==> (\<exists>t. 0 < abs t & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

351 
abs t < abs x & 
15539  352 
exp x = (\<Sum>m=0..<n. (x ^ m) / real (fact m)) + 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

353 
(exp t / real (fact n)) * x ^ n)" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

354 
by (cut_tac diff = "%n. exp" and f = exp and x = x and n = n in Maclaurin_all_lt_objl, auto) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

355 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

356 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

357 
lemma Maclaurin_exp_le: 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

358 
"\<exists>t. abs t \<le> abs x & 
15539  359 
exp x = (\<Sum>m=0..<n. (x ^ m) / real (fact m)) + 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

360 
(exp t / real (fact n)) * x ^ n" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

361 
by (cut_tac diff = "%n. exp" and f = exp and x = x and n = n in Maclaurin_all_le_objl, auto) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

362 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

363 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

364 
subsection{*Version for Sine Function*} 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

365 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

366 
lemma MVT2: 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

367 
"[ a < b; \<forall>x. a \<le> x & x \<le> b > DERIV f x :> f'(x) ] 
21782  368 
==> \<exists>z::real. a < z & z < b & (f b  f a = (b  a) * f'(z))" 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

369 
apply (drule MVT) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

370 
apply (blast intro: DERIV_isCont) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

371 
apply (force dest: order_less_imp_le simp add: differentiable_def) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

372 
apply (blast dest: DERIV_unique order_less_imp_le) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

373 
done 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

374 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

375 
lemma mod_exhaust_less_4: 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

376 
"m mod 4 = 0  m mod 4 = 1  m mod 4 = 2  m mod 4 = (3::nat)" 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19765
diff
changeset

377 
by auto 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

378 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

379 
lemma Suc_Suc_mult_two_diff_two [rule_format, simp]: 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

380 
"n\<noteq>0 > Suc (Suc (2 * n  2)) = 2*n" 
15251  381 
by (induct "n", auto) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

382 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

383 
lemma lemma_Suc_Suc_4n_diff_2 [rule_format, simp]: 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

384 
"n\<noteq>0 > Suc (Suc (4*n  2)) = 4*n" 
15251  385 
by (induct "n", auto) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

386 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

387 
lemma Suc_mult_two_diff_one [rule_format, simp]: 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

388 
"n\<noteq>0 > Suc (2 * n  1) = 2*n" 
15251  389 
by (induct "n", auto) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

390 

15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

391 

ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

392 
text{*It is unclear why so many variant results are needed.*} 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

393 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

394 
lemma Maclaurin_sin_expansion2: 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

395 
"\<exists>t. abs t \<le> abs x & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

396 
sin x = 
15539  397 
(\<Sum>m=0..<n. (if even m then 0 
23177  398 
else (1 ^ ((m  Suc 0) div 2)) / real (fact m)) * 
15539  399 
x ^ m) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

400 
+ ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

401 
apply (cut_tac f = sin and n = n and x = x 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

402 
and diff = "%n x. sin (x + 1/2*real n * pi)" in Maclaurin_all_lt_objl) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

403 
apply safe 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

404 
apply (simp (no_asm)) 
15539  405 
apply (simp (no_asm)) 
23242  406 
apply (case_tac "n", clarify, simp, simp add: lemma_STAR_sin) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

407 
apply (rule ccontr, simp) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

408 
apply (drule_tac x = x in spec, simp) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

409 
apply (erule ssubst) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

410 
apply (rule_tac x = t in exI, simp) 
15536  411 
apply (rule setsum_cong[OF refl]) 
15539  412 
apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

413 
done 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

414 

15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

415 
lemma Maclaurin_sin_expansion: 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

416 
"\<exists>t. sin x = 
15539  417 
(\<Sum>m=0..<n. (if even m then 0 
23177  418 
else (1 ^ ((m  Suc 0) div 2)) / real (fact m)) * 
15539  419 
x ^ m) 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

420 
+ ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)" 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

421 
apply (insert Maclaurin_sin_expansion2 [of x n]) 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

422 
apply (blast intro: elim:); 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

423 
done 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

424 

ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

425 

ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

426 

15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

427 
lemma Maclaurin_sin_expansion3: 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

428 
"[ n \<noteq> 0; 0 < x ] ==> 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

429 
\<exists>t. 0 < t & t < x & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

430 
sin x = 
15539  431 
(\<Sum>m=0..<n. (if even m then 0 
23177  432 
else (1 ^ ((m  Suc 0) div 2)) / real (fact m)) * 
15539  433 
x ^ m) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

434 
+ ((sin(t + 1/2 * real(n) *pi) / real (fact n)) * x ^ n)" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

435 
apply (cut_tac f = sin and n = n and h = x and diff = "%n x. sin (x + 1/2*real (n) *pi)" in Maclaurin_objl) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

436 
apply safe 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

437 
apply simp 
15539  438 
apply (simp (no_asm)) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

439 
apply (erule ssubst) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

440 
apply (rule_tac x = t in exI, simp) 
15536  441 
apply (rule setsum_cong[OF refl]) 
15539  442 
apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

443 
done 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

444 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

445 
lemma Maclaurin_sin_expansion4: 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

446 
"0 < x ==> 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

447 
\<exists>t. 0 < t & t \<le> x & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

448 
sin x = 
15539  449 
(\<Sum>m=0..<n. (if even m then 0 
23177  450 
else (1 ^ ((m  Suc 0) div 2)) / real (fact m)) * 
15539  451 
x ^ m) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

452 
+ ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

453 
apply (cut_tac f = sin and n = n and h = x and diff = "%n x. sin (x + 1/2*real (n) *pi)" in Maclaurin2_objl) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

454 
apply safe 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

455 
apply simp 
15539  456 
apply (simp (no_asm)) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

457 
apply (erule ssubst) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

458 
apply (rule_tac x = t in exI, simp) 
15536  459 
apply (rule setsum_cong[OF refl]) 
15539  460 
apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

461 
done 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

462 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

463 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

464 
subsection{*Maclaurin Expansion for Cosine Function*} 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

465 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

466 
lemma sumr_cos_zero_one [simp]: 
15539  467 
"(\<Sum>m=0..<(Suc n). 
23177  468 
(if even m then 1 ^ (m div 2)/(real (fact m)) else 0) * 0 ^ m) = 1" 
15251  469 
by (induct "n", auto) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

470 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

471 
lemma Maclaurin_cos_expansion: 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

472 
"\<exists>t. abs t \<le> abs x & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

473 
cos x = 
15539  474 
(\<Sum>m=0..<n. (if even m 
23177  475 
then 1 ^ (m div 2)/(real (fact m)) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

476 
else 0) * 
15539  477 
x ^ m) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

478 
+ ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

479 
apply (cut_tac f = cos and n = n and x = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_all_lt_objl) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

480 
apply safe 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

481 
apply (simp (no_asm)) 
15539  482 
apply (simp (no_asm)) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

483 
apply (case_tac "n", simp) 
15561  484 
apply (simp del: setsum_op_ivl_Suc) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

485 
apply (rule ccontr, simp) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

486 
apply (drule_tac x = x in spec, simp) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

487 
apply (erule ssubst) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

488 
apply (rule_tac x = t in exI, simp) 
15536  489 
apply (rule setsum_cong[OF refl]) 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

490 
apply (auto simp add: cos_zero_iff even_mult_two_ex) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

491 
done 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

492 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

493 
lemma Maclaurin_cos_expansion2: 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

494 
"[ 0 < x; n \<noteq> 0 ] ==> 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

495 
\<exists>t. 0 < t & t < x & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

496 
cos x = 
15539  497 
(\<Sum>m=0..<n. (if even m 
23177  498 
then 1 ^ (m div 2)/(real (fact m)) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

499 
else 0) * 
15539  500 
x ^ m) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

501 
+ ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

502 
apply (cut_tac f = cos and n = n and h = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_objl) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

503 
apply safe 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

504 
apply simp 
15539  505 
apply (simp (no_asm)) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

506 
apply (erule ssubst) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

507 
apply (rule_tac x = t in exI, simp) 
15536  508 
apply (rule setsum_cong[OF refl]) 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

509 
apply (auto simp add: cos_zero_iff even_mult_two_ex) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

510 
done 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

511 

15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

512 
lemma Maclaurin_minus_cos_expansion: 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

513 
"[ x < 0; n \<noteq> 0 ] ==> 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

514 
\<exists>t. x < t & t < 0 & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

515 
cos x = 
15539  516 
(\<Sum>m=0..<n. (if even m 
23177  517 
then 1 ^ (m div 2)/(real (fact m)) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

518 
else 0) * 
15539  519 
x ^ m) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

520 
+ ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

521 
apply (cut_tac f = cos and n = n and h = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_minus_objl) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

522 
apply safe 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

523 
apply simp 
15539  524 
apply (simp (no_asm)) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

525 
apply (erule ssubst) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

526 
apply (rule_tac x = t in exI, simp) 
15536  527 
apply (rule setsum_cong[OF refl]) 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

528 
apply (auto simp add: cos_zero_iff even_mult_two_ex) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

529 
done 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

530 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

531 
(*  *) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

532 
(* Version for ln(1 +/ x). Where is it?? *) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

533 
(*  *) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

534 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

535 
lemma sin_bound_lemma: 
15081  536 
"[x = y; abs u \<le> (v::real) ] ==> \<bar>(x + u)  y\<bar> \<le> v" 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

537 
by auto 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

538 

2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

539 
lemma Maclaurin_sin_bound: 
23177  540 
"abs(sin x  (\<Sum>m=0..<n. (if even m then 0 else (1 ^ ((m  Suc 0) div 2)) / real (fact m)) * 
15081  541 
x ^ m)) \<le> inverse(real (fact n)) * \<bar>x\<bar> ^ n" 
14738  542 
proof  
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

543 
have "!! x (y::real). x \<le> 1 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x * y \<le> 1 * y" 
14738  544 
by (rule_tac mult_right_mono,simp_all) 
545 
note est = this[simplified] 

22985  546 
let ?diff = "\<lambda>(n::nat) x. if n mod 4 = 0 then sin(x) else if n mod 4 = 1 then cos(x) else if n mod 4 = 2 then sin(x) else cos(x)" 
547 
have diff_0: "?diff 0 = sin" by simp 

548 
have DERIV_diff: "\<forall>m x. DERIV (?diff m) x :> ?diff (Suc m) x" 

549 
apply (clarify) 

550 
apply (subst (1 2 3) mod_Suc_eq_Suc_mod) 

551 
apply (cut_tac m=m in mod_exhaust_less_4) 

552 
apply (safe, simp_all) 

553 
apply (rule DERIV_minus, simp) 

554 
apply (rule lemma_DERIV_subst, rule DERIV_minus, rule DERIV_cos, simp) 

555 
done 

556 
from Maclaurin_all_le [OF diff_0 DERIV_diff] 

557 
obtain t where t1: "\<bar>t\<bar> \<le> \<bar>x\<bar>" and 

558 
t2: "sin x = (\<Sum>m = 0..<n. ?diff m 0 / real (fact m) * x ^ m) + 

559 
?diff n t / real (fact n) * x ^ n" by fast 

560 
have diff_m_0: 

561 
"\<And>m. ?diff m 0 = (if even m then 0 

23177  562 
else 1 ^ ((m  Suc 0) div 2))" 
22985  563 
apply (subst even_even_mod_4_iff) 
564 
apply (cut_tac m=m in mod_exhaust_less_4) 

565 
apply (elim disjE, simp_all) 

566 
apply (safe dest!: mod_eqD, simp_all) 

567 
done 

14738  568 
show ?thesis 
22985  569 
apply (subst t2) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

570 
apply (rule sin_bound_lemma) 
15536  571 
apply (rule setsum_cong[OF refl]) 
22985  572 
apply (subst diff_m_0, simp) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

573 
apply (auto intro: mult_right_mono [where b=1, simplified] mult_right_mono 
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
15944
diff
changeset

574 
simp add: est mult_nonneg_nonneg mult_ac divide_inverse 
16924  575 
power_abs [symmetric] abs_mult) 
14738  576 
done 
577 
qed 

578 

15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

579 
end 