author  huffman 
Thu, 17 May 2007 00:45:27 +0200  
changeset 22985  501e6dfe4e5a 
parent 22983  3314057c3b57 
child 23069  cdfff0241c12 
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.*} 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

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

33 
{* 
19765  34 
local 
35 
val deriv_rulesI = 

36 
[thm "DERIV_Id", thm "DERIV_const", thm "DERIV_cos", thm "DERIV_cmult", 

37 
thm "DERIV_sin", thm "DERIV_exp", thm "DERIV_inverse", thm "DERIV_pow", 

38 
thm "DERIV_add", thm "DERIV_diff", thm "DERIV_mult", thm "DERIV_minus", 

39 
thm "DERIV_inverse_fun", thm "DERIV_quotient", thm "DERIV_fun_pow", 

40 
thm "DERIV_fun_exp", thm "DERIV_fun_sin", thm "DERIV_fun_cos", 

41 
thm "DERIV_Id", thm "DERIV_const", thm "DERIV_cos"]; 

42 

43 
val DERIV_chain2 = thm "DERIV_chain2"; 

44 

45 
in 

46 

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

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

48 
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

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

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

51 

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

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

53 
SUBGOAL (fn (prem,i) => 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

54 
(resolve_tac deriv_rulesI i) ORELSE 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

55 
((rtac (read_instantiate [("f",get_fun_name prem)] 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

56 
DERIV_chain2) i) handle DERIV_name => no_tac));; 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

57 

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

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

60 
end 

15079
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 

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

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

64 
"[ \<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

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

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

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

68 
((\<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

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

70 
\<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

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

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

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

74 
apply (simp (no_asm_simp)) 
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 (tactic DERIV_tac) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

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

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

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

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

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

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

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

85 
apply (insert sumr_offset4 [of 1]) 
15561  86 
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

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

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

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

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

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

92 
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

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

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

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

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

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

99 
done 
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 

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

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

104 
"[\<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

105 
\<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

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

107 
==> \<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

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

109 
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

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

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

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

113 
apply (subgoal_tac "\<forall>ta. 0 \<le> ta & ta \<le> t > (difg (Suc n)) differentiable ta") 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

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

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

116 
apply (simp add: differentiable_def, clarify) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

117 
apply (rule_tac x = "difg (Suc (Suc n)) ta" in exI) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

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

119 
apply (simp add: differentiable_def, clarify) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

120 
apply (rule_tac x = "difg (Suc (Suc n)) x" in exI) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

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

122 
done 
14738  123 

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

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

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

126 
\<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

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

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

129 
f h = 
15539  130 
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

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

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

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

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

135 
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

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

137 
apply (subgoal_tac "\<exists>g. 
15539  138 
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

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 "g 0 = 0 & g h =0") 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

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

144 
apply (cut_tac n = m and k = 1 in sumr_offset2) 
15561  145 
apply (simp add: eq_diff_eq' del: setsum_op_ivl_Suc) 
15539  146 
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

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

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

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

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

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

152 
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

153 
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

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

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

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

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

159 
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

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

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

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

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

165 
apply (insert sumr_offset4 [of 1]) 
15561  166 
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

167 
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

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

169 
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

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

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

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

173 
(* do some tidying up *) 
15539  174 
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

175 
in thin_rl) 
15539  176 
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

177 
in thin_rl) 
15539  178 
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

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

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

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

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

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

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

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

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

187 
apply (subgoal_tac "\<forall>t. 0 \<le> t & t \<le> h > g differentiable t") 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

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

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

190 
apply (simp add: differentiable_def, clarify) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

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

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

193 
apply (simp add: differentiable_def, clarify) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

194 
apply (rule_tac x = "difg (Suc 0) x" in exI) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

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

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

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

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

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

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

201 

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

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

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

204 
(\<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

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

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

207 
f h = 
15539  208 
(\<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

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

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

211 

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

212 

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

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

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

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

216 
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

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

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

219 
f h = 
15539  220 
(\<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

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

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

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

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

225 

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

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

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

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

229 
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

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

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

232 
f h = 
15539  233 
(\<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

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

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

236 

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

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

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

239 
\<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

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

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

242 
f h = 
15539  243 
(\<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

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

245 
apply (cut_tac f = "%x. f (x)" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

246 
and diff = "%n x. (( 1) ^ n) * diff n (x)" 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

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

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

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

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

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

253 
apply (rule DERIV_chain2 [where g=uminus]) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

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

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

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

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

258 
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

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

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

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

263 

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

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

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

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

267 
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

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

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

270 
f h = 
15539  271 
(\<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

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

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

274 

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

275 

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

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

277 

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

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

279 

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

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

281 
"0 < n \<longrightarrow> 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

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

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

284 
diff n 0 * 0 ^ n / real (fact n)" 
15251  285 
by (induct "n", auto) 
14738  286 

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

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

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

289 
\<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

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

291 
f x = 
15539  292 
(\<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

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

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

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

296 
apply (rule_tac x = 0 in exI) 
15539  297 
apply (force simp add: Maclaurin_bi_le_lemma) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

298 
apply (cut_tac x = x and y = 0 in linorder_less_linear, auto) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

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

300 
apply (cut_tac f = "diff 0" and diff = diff and h = x and n = n in Maclaurin_minus_objl, safe) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

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

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

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

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

305 
apply (cut_tac f = "diff 0" and diff = diff and h = x and n = n in Maclaurin_objl, safe) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

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

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

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

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

310 

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

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

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

313 
\<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

314 
x ~= 0; 0 < n 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

315 
] ==> \<exists>t. 0 < abs t & abs t < abs x & 
15539  316 
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

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

318 
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

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

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

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

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

324 

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

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

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

327 
(\<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

328 
x ~= 0 & 0 < n 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

329 
> (\<exists>t. 0 < abs t & abs t < abs x & 
15539  330 
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

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

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

333 

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

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

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

336 
==> 0 < n > 
15539  337 
(\<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

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

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

340 

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

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

342 
\<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

343 
] ==> \<exists>t. abs t \<le> abs x & 
15539  344 
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

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

346 
apply (insert linorder_le_less_linear [of n 0]) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

347 
apply (erule disjE, force) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

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

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

350 
apply (drule gr_implies_not0 [THEN not0_implies_Suc]) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

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

352 
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

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

354 
done 
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 
lemma Maclaurin_all_le_objl: "diff 0 = f & 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

357 
(\<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

358 
> (\<exists>t. abs t \<le> abs x & 
15539  359 
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

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

361 
by (blast intro: Maclaurin_all_le) 
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 Exponential 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 Maclaurin_exp_lt: "[ x ~= 0; 0 < n ] 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

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

368 
abs t < abs x & 
15539  369 
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

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

371 
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

372 

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

373 

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

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

375 
"\<exists>t. abs t \<le> abs x & 
15539  376 
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

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

378 
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

379 

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

380 

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

381 
subsection{*Version for Sine Function*} 
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 MVT2: 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

384 
"[ a < b; \<forall>x. a \<le> x & x \<le> b > DERIV f x :> f'(x) ] 
21782  385 
==> \<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

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

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

388 
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

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

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

391 

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

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

393 
"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

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

395 

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

396 
lemma Suc_Suc_mult_two_diff_two [rule_format, simp]: 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

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

399 

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

400 
lemma lemma_Suc_Suc_4n_diff_2 [rule_format, simp]: 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

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

403 

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

404 
lemma Suc_mult_two_diff_one [rule_format, simp]: 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

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

407 

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

408 

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

409 
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

410 

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

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

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

413 
sin x = 
15539  414 
(\<Sum>m=0..<n. (if even m then 0 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

415 
else (( 1) ^ ((m  (Suc 0)) div 2)) / real (fact m)) * 
15539  416 
x ^ m) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

417 
+ ((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

418 
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

419 
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

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

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

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

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

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

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

427 
apply (rule_tac x = t in exI, simp) 
15536  428 
apply (rule setsum_cong[OF refl]) 
15539  429 
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

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

431 

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

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

433 
"\<exists>t. sin x = 
15539  434 
(\<Sum>m=0..<n. (if even m then 0 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

435 
else (( 1) ^ ((m  (Suc 0)) div 2)) / real (fact m)) * 
15539  436 
x ^ m) 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

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

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

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

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

441 

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

442 

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

443 

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

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

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

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

447 
sin x = 
15539  448 
(\<Sum>m=0..<n. (if even m then 0 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

449 
else (( 1) ^ ((m  (Suc 0)) div 2)) / real (fact m)) * 
15539  450 
x ^ m) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

451 
+ ((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

452 
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

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

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

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

457 
apply (rule_tac x = t in exI, simp) 
15536  458 
apply (rule setsum_cong[OF refl]) 
15539  459 
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

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

461 

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

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

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

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

465 
sin x = 
15539  466 
(\<Sum>m=0..<n. (if even m then 0 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

467 
else (( 1) ^ ((m  (Suc 0)) div 2)) / real (fact m)) * 
15539  468 
x ^ m) 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

469 
+ ((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

470 
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

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

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

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

475 
apply (rule_tac x = t in exI, simp) 
15536  476 
apply (rule setsum_cong[OF refl]) 
15539  477 
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

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

479 

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

480 

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

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

482 

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

483 
lemma sumr_cos_zero_one [simp]: 
15539  484 
"(\<Sum>m=0..<(Suc n). 
485 
(if even m then ( 1) ^ (m div 2)/(real (fact m)) else 0) * 0 ^ m) = 1" 

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

487 

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

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

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

490 
cos x = 
15539  491 
(\<Sum>m=0..<n. (if even m 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

492 
then ( 1) ^ (m div 2)/(real (fact m)) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

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

495 
+ ((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

496 
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

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

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

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

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

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

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

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

507 
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

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

509 

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

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

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

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

513 
cos x = 
15539  514 
(\<Sum>m=0..<n. (if even m 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

515 
then ( 1) ^ (m div 2)/(real (fact m)) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

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

518 
+ ((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

519 
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

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

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

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

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

526 
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

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

528 

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

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

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

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

532 
cos x = 
15539  533 
(\<Sum>m=0..<n. (if even m 
15079
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

534 
then ( 1) ^ (m div 2)/(real (fact m)) 
2ef899e4526d
conversion of Hyperreal/MacLaurin_lemmas to Isar script
paulson
parents:
14738
diff
changeset

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

537 
+ ((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

538 
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

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

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

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

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

545 
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

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

547 

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

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

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

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

551 

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

552 
lemma sin_bound_lemma: 
15081  553 
"[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

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

555 

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

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

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

22985  563 
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)" 
564 
have diff_0: "?diff 0 = sin" by simp 

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

566 
apply (clarify) 

567 
apply (subst (1 2 3) mod_Suc_eq_Suc_mod) 

568 
apply (cut_tac m=m in mod_exhaust_less_4) 

569 
apply (safe, simp_all) 

570 
apply (rule DERIV_minus, simp) 

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

572 
done 

573 
from Maclaurin_all_le [OF diff_0 DERIV_diff] 

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

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

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

577 
have diff_m_0: 

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

579 
else ( 1) ^ ((m  Suc 0) div 2))" 

580 
apply (subst even_even_mod_4_iff) 

581 
apply (cut_tac m=m in mod_exhaust_less_4) 

582 
apply (elim disjE, simp_all) 

583 
apply (safe dest!: mod_eqD, simp_all) 

584 
done 

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

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

590 
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

591 
simp add: est mult_nonneg_nonneg mult_ac divide_inverse 
16924  592 
power_abs [symmetric] abs_mult) 
14738  593 
done 
594 
qed 

595 

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

596 
end 