author  huffman 
Tue, 26 May 2009 11:02:59 0700  
changeset 31259  c1b981b71dba 
parent 31257  547bf9819d6c 
child 31336  e17f13cd1280 
permissions  rwrr 
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28562
diff
changeset

1 
(* Author : Jacques D. Fleuriot 
13958  2 
Copyright : 2000 University of Edinburgh 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

6 
header{*Theory of Integration*} 
13958  7 

15131  8 
theory Integration 
29469  9 
imports Deriv ATP_Linkup 
15131  10 
begin 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

11 

49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

12 
text{*We follow John Harrison in formalizing the Gauge integral.*} 
13958  13 

31259
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

14 
subsection {* Gauges *} 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

15 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20792
diff
changeset

16 
definition 
31253  17 
gauge :: "[real set, real => real] => bool" where 
18 
[code del]:"gauge E g = (\<forall>x\<in>E. 0 < g(x))" 

13958  19 

31259
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

20 

c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

21 
subsection {* Gaugefine divisions *} 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

22 

c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

23 
inductive 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

24 
fine :: "[real \<Rightarrow> real, real \<times> real, (real \<times> real \<times> real) list] \<Rightarrow> bool" 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

25 
for 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

26 
\<delta> :: "real \<Rightarrow> real" 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

27 
where 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

28 
fine_Nil: 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

29 
"fine \<delta> (a, a) []" 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

30 
 fine_Cons: 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

31 
"\<lbrakk>fine \<delta> (b, c) D; a < b; a \<le> x; x \<le> b; b  a < \<delta> x\<rbrakk> 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

32 
\<Longrightarrow> fine \<delta> (a, c) ((a, x, b) # D)" 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

33 

c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

34 
lemmas fine_induct [induct set: fine] = 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

35 
fine.induct [of "\<delta>" "(a,b)" "D" "split P", unfolded split_conv, standard] 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

36 

c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

37 
lemma fine_single: 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

38 
"\<lbrakk>a < b; a \<le> x; x \<le> b; b  a < \<delta> x\<rbrakk> \<Longrightarrow> fine \<delta> (a, b) [(a, x, b)]" 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

39 
by (rule fine_Cons [OF fine_Nil]) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

40 

c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

41 
lemma fine_append: 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

42 
"\<lbrakk>fine \<delta> (a, b) D; fine \<delta> (b, c) D'\<rbrakk> \<Longrightarrow> fine \<delta> (a, c) (D @ D')" 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

43 
by (induct set: fine, simp, simp add: fine_Cons) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

44 

c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

45 
lemma fine_imp_le: "fine \<delta> (a, b) D \<Longrightarrow> a \<le> b" 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

46 
by (induct set: fine, simp_all) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

47 

c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

48 
lemma nonempty_fine_imp_less: "\<lbrakk>fine \<delta> (a, b) D; D \<noteq> []\<rbrakk> \<Longrightarrow> a < b" 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

49 
apply (induct set: fine, simp) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

50 
apply (drule fine_imp_le, simp) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

51 
done 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

52 

c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

53 
lemma empty_fine_imp_eq: "\<lbrakk>fine \<delta> (a, b) D; D = []\<rbrakk> \<Longrightarrow> a = b" 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

54 
by (induct set: fine, simp_all) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

55 

c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

56 
lemma fine_eq: "fine \<delta> (a, b) D \<Longrightarrow> a = b \<longleftrightarrow> D = []" 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

57 
apply (cases "D = []") 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

58 
apply (drule (1) empty_fine_imp_eq, simp) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

59 
apply (drule (1) nonempty_fine_imp_less, simp) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

60 
done 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

61 

c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

62 
lemma mem_fine: 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

63 
"\<lbrakk>fine \<delta> (a, b) D; (u, x, v) \<in> set D\<rbrakk> \<Longrightarrow> u < v \<and> u \<le> x \<and> x \<le> v" 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

64 
by (induct set: fine, simp, force) 
13958  65 

31259
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

66 
lemma mem_fine2: "\<lbrakk>fine \<delta> (a, b) D; (u, z, v) \<in> set D\<rbrakk> \<Longrightarrow> a \<le> u \<and> v \<le> b" 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

67 
apply (induct arbitrary: z u v set: fine, auto) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

68 
apply (simp add: fine_imp_le) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

69 
apply (erule order_trans [OF less_imp_le], simp) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

70 
done 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

71 

c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

72 
lemma mem_fine3: "\<lbrakk>fine \<delta> (a, b) D; (u, z, v) \<in> set D\<rbrakk> \<Longrightarrow> v  u < \<delta> z" 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

73 
by (induct arbitrary: z u v set: fine) auto 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

74 

c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

75 
lemma BOLZANO: 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

76 
fixes P :: "real \<Rightarrow> real \<Rightarrow> bool" 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

77 
assumes 1: "a \<le> b" 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

78 
assumes 2: "\<And>a b c. \<lbrakk>P a b; P b c; a \<le> b; b \<le> c\<rbrakk> \<Longrightarrow> P a c" 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

79 
assumes 3: "\<And>x. \<exists>d>0. \<forall>a b. a \<le> x & x \<le> b & (ba) < d \<longrightarrow> P a b" 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

80 
shows "P a b" 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

81 
apply (subgoal_tac "split P (a,b)", simp) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

82 
apply (rule lemma_BOLZANO [OF _ _ 1]) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

83 
apply (clarify, erule (3) 2) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

84 
apply (clarify, rule 3) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

85 
done 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

86 

c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

87 
text{*We can always find a division that is fine wrt any gauge*} 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

88 

c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

89 
lemma fine_exists: 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

90 
assumes "a \<le> b" and "gauge {a..b} \<delta>" shows "\<exists>D. fine \<delta> (a, b) D" 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

91 
proof  
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

92 
{ 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

93 
fix u v :: real assume "u \<le> v" 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

94 
have "a \<le> u \<Longrightarrow> v \<le> b \<Longrightarrow> \<exists>D. fine \<delta> (u, v) D" 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

95 
apply (induct u v rule: BOLZANO, rule `u \<le> v`) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

96 
apply (simp, fast intro: fine_append) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

97 
apply (case_tac "a \<le> x \<and> x \<le> b") 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

98 
apply (rule_tac x="\<delta> x" in exI) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

99 
apply (rule conjI) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

100 
apply (simp add: `gauge {a..b} \<delta>` [unfolded gauge_def]) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

101 
apply (clarify, rename_tac u v) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

102 
apply (case_tac "u = v") 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

103 
apply (fast intro: fine_Nil) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

104 
apply (subgoal_tac "u < v", fast intro: fine_single, simp) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

105 
apply (rule_tac x="1" in exI, clarsimp) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

106 
done 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

107 
} 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

108 
with `a \<le> b` show ?thesis by auto 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

109 
qed 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

110 

c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

111 

c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

112 
subsection {* Riemann sum *} 
13958  113 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20792
diff
changeset

114 
definition 
31259
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

115 
rsum :: "[(real \<times> real \<times> real) list, real \<Rightarrow> real] \<Rightarrow> real" where 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

116 
"rsum D f = (\<Sum>(u, x, v)\<leftarrow>D. f x * (v  u))" 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

117 

c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

118 
lemma rsum_Nil [simp]: "rsum [] f = 0" 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

119 
unfolding rsum_def by simp 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

120 

c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

121 
lemma rsum_Cons [simp]: "rsum ((u, x, v) # D) f = f x * (v  u) + rsum D f" 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

122 
unfolding rsum_def by simp 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

123 

c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

124 
lemma rsum_zero [simp]: "rsum D (\<lambda>x. 0) = 0" 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

125 
by (induct D, auto) 
13958  126 

31259
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

127 
lemma rsum_left_distrib: "rsum D f * c = rsum D (\<lambda>x. f x * c)" 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

128 
by (induct D, auto simp add: algebra_simps) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

129 

c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

130 
lemma rsum_right_distrib: "c * rsum D f = rsum D (\<lambda>x. c * f x)" 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

131 
by (induct D, auto simp add: algebra_simps) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

132 

c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

133 
lemma rsum_add: "rsum D (\<lambda>x. f x + g x) = rsum D f + rsum D g" 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

134 
by (induct D, auto simp add: algebra_simps) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

135 

c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

136 

c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

137 
subsection {* Gauge integrability (definite) *} 
13958  138 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20792
diff
changeset

139 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20792
diff
changeset

140 
Integral :: "[(real*real),real=>real,real] => bool" where 
28562  141 
[code del]: "Integral = (%(a,b) f k. \<forall>e > 0. 
31259
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

142 
(\<exists>\<delta>. gauge {a .. b} \<delta> & 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

143 
(\<forall>D. fine \<delta> (a,b) D > 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

144 
\<bar>rsum D f  k\<bar> < e)))" 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

145 

31252  146 
lemma Integral_def2: 
31259
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

147 
"Integral = (%(a,b) f k. \<forall>e>0. (\<exists>\<delta>. gauge {a..b} \<delta> & 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

148 
(\<forall>D. fine \<delta> (a,b) D > 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

149 
\<bar>rsum D f  k\<bar> \<le> e)))" 
31252  150 
unfolding Integral_def 
151 
apply (safe intro!: ext) 

152 
apply (fast intro: less_imp_le) 

153 
apply (drule_tac x="e/2" in spec) 

154 
apply force 

155 
done 

156 

15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

157 
text{*Lemmas about combining gauges*} 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

158 

49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

159 
lemma gauge_min: 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

160 
"[ gauge(E) g1; gauge(E) g2 ] 
31259
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

161 
==> gauge(E) (%x. min (g1(x)) (g2(x)))" 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

162 
by (simp add: gauge_def) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

163 

49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

164 
lemma fine_min: 
31259
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

165 
"fine (%x. min (g1(x)) (g2(x))) (a,b) D 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

166 
==> fine(g1) (a,b) D & fine(g2) (a,b) D" 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

167 
apply (erule fine.induct) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

168 
apply (simp add: fine_Nil) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

169 
apply (simp add: fine_Cons) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

170 
done 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

171 

49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

172 
text{*The integral is unique if it exists*} 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

173 

49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

174 
lemma Integral_unique: 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

175 
"[ a \<le> b; Integral(a,b) f k1; Integral(a,b) f k2 ] ==> k1 = k2" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

176 
apply (simp add: Integral_def) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

177 
apply (drule_tac x = "\<bar>k1  k2\<bar> /2" in spec)+ 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

178 
apply auto 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

179 
apply (drule gauge_min, assumption) 
31259
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

180 
apply (drule_tac \<delta> = "%x. min (\<delta> x) (\<delta>' x)" 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

181 
in fine_exists, assumption, auto) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

182 
apply (drule fine_min) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

183 
apply (drule spec)+ 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

184 
apply auto 
31259
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

185 
apply (subgoal_tac "\<bar>(rsum D f  k2)  (rsum D f  k1)\<bar> < \<bar>k1  k2\<bar>") 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

186 
apply arith 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

187 
apply (drule add_strict_mono, assumption) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

188 
apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric] 
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
16924
diff
changeset

189 
mult_less_cancel_right) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

190 
done 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

191 

49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

192 
lemma Integral_zero [simp]: "Integral(a,a) f 0" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

193 
apply (auto simp add: Integral_def) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

194 
apply (rule_tac x = "%x. 1" in exI) 
31259
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

195 
apply (auto dest: fine_eq simp add: gauge_def rsum_def) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

196 
done 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

197 

31259
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

198 
lemma fine_rsum_const: "fine \<delta> (a,b) D \<Longrightarrow> rsum D (\<lambda>x. c) = (c * (b  a))" 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

199 
unfolding rsum_def 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

200 
by (induct set: fine, auto simp add: algebra_simps) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

201 

49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

202 
lemma Integral_eq_diff_bounds: "a \<le> b ==> Integral(a,b) (%x. 1) (b  a)" 
31259
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

203 
apply (cases "a = b", simp) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

204 
apply (simp add: Integral_def, clarify) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

205 
apply (rule_tac x = "%x. b  a" in exI) 
31259
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

206 
apply (rule conjI, simp add: gauge_def) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

207 
apply (clarify) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

208 
apply (subst fine_rsum_const, assumption, simp) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

209 
done 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

210 

49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

211 
lemma Integral_mult_const: "a \<le> b ==> Integral(a,b) (%x. c) (c*(b  a))" 
31259
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

212 
apply (cases "a = b", simp) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

213 
apply (simp add: Integral_def, clarify) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

214 
apply (rule_tac x = "%x. b  a" in exI) 
31259
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

215 
apply (rule conjI, simp add: gauge_def) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

216 
apply (clarify) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

217 
apply (subst fine_rsum_const, assumption, simp) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

218 
done 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

219 

49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

220 
lemma Integral_mult: 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

221 
"[ a \<le> b; Integral(a,b) f k ] ==> Integral(a,b) (%x. c * f x) (c * k)" 
15221  222 
apply (auto simp add: order_le_less 
223 
dest: Integral_unique [OF order_refl Integral_zero]) 

31257  224 
apply (auto simp add: Integral_def setsum_right_distrib[symmetric] mult_assoc) 
225 
apply (case_tac "c = 0", force) 

226 
apply (drule_tac x = "e/abs c" in spec) 

227 
apply (simp add: divide_pos_pos) 

228 
apply clarify 

31259
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

229 
apply (rule_tac x="\<delta>" in exI, clarify) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

230 
apply (drule_tac x="D" in spec, clarify) 
31257  231 
apply (simp add: pos_less_divide_eq abs_mult [symmetric] 
232 
algebra_simps rsum_right_distrib) 

15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

233 
done 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

234 

31259
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

235 

15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

236 
text{*Fundamental theorem of calculus (Part I)*} 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

237 

15105  238 
text{*"Straddle Lemma" : Swartz and Thompson: AMM 95(7) 1988 *} 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

239 

49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

240 
lemma strad1: 
31252  241 
"\<lbrakk>\<forall>z::real. z \<noteq> x \<and> \<bar>z  x\<bar> < s \<longrightarrow> 
242 
\<bar>(f z  f x) / (z  x)  f' x\<bar> < e/2; 

243 
0 < s; 0 < e; a \<le> x; x \<le> b\<rbrakk> 

244 
\<Longrightarrow> \<forall>z. \<bar>z  x\<bar> < s >\<bar>f z  f x  f' x * (z  x)\<bar> \<le> e/2 * \<bar>z  x\<bar>" 

245 
apply clarify 

31253  246 
apply (case_tac "z = x", simp) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

247 
apply (drule_tac x = z in spec) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

248 
apply (rule_tac z1 = "\<bar>inverse (z  x)\<bar>" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

249 
in real_mult_le_cancel_iff2 [THEN iffD1]) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

250 
apply simp 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

251 
apply (simp del: abs_inverse abs_mult add: abs_mult [symmetric] 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

252 
mult_assoc [symmetric]) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

253 
apply (subgoal_tac "inverse (z  x) * (f z  f x  f' x * (z  x)) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

254 
= (f z  f x) / (z  x)  f' x") 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

255 
apply (simp add: abs_mult [symmetric] mult_ac diff_minus) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

256 
apply (subst mult_commute) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

257 
apply (simp add: left_distrib diff_minus) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

258 
apply (simp add: mult_assoc divide_inverse) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

259 
apply (simp add: left_distrib) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

260 
done 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

261 

49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

262 
lemma lemma_straddle: 
31252  263 
assumes f': "\<forall>x. a \<le> x & x \<le> b > DERIV f x :> f'(x)" and "0 < e" 
31253  264 
shows "\<exists>g. gauge {a..b} g & 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

265 
(\<forall>x u v. a \<le> u & u \<le> x & x \<le> v & v \<le> b & (v  u) < g(x) 
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
15093
diff
changeset

266 
> \<bar>(f(v)  f(u))  (f'(x) * (v  u))\<bar> \<le> e * (v  u))" 
31252  267 
proof  
31253  268 
have "\<forall>x\<in>{a..b}. 
15360  269 
(\<exists>d > 0. \<forall>u v. u \<le> x & x \<le> v & (v  u) < d > 
31252  270 
\<bar>(f(v)  f(u))  (f'(x) * (v  u))\<bar> \<le> e * (v  u))" 
31253  271 
proof (clarsimp) 
31252  272 
fix x :: real assume "a \<le> x" and "x \<le> b" 
273 
with f' have "DERIV f x :> f'(x)" by simp 

274 
then have "\<forall>r>0. \<exists>s>0. \<forall>z. z \<noteq> x \<and> \<bar>z  x\<bar> < s \<longrightarrow> \<bar>(f z  f x) / (z  x)  f' x\<bar> < r" 

275 
by (simp add: DERIV_iff2 LIM_def) 

276 
with `0 < e` obtain s 

277 
where "\<forall>z. z \<noteq> x \<and> \<bar>z  x\<bar> < s \<longrightarrow> \<bar>(f z  f x) / (z  x)  f' x\<bar> < e/2" and "0 < s" 

278 
by (drule_tac x="e/2" in spec, auto) 

279 
then have strad [rule_format]: 

280 
"\<forall>z. \<bar>z  x\<bar> < s > \<bar>f z  f x  f' x * (z  x)\<bar> \<le> e/2 * \<bar>z  x\<bar>" 

281 
using `0 < e` `a \<le> x` `x \<le> b` by (rule strad1) 

282 
show "\<exists>d>0. \<forall>u v. u \<le> x \<and> x \<le> v \<and> v  u < d \<longrightarrow> \<bar>f v  f u  f' x * (v  u)\<bar> \<le> e * (v  u)" 

283 
proof (safe intro!: exI) 

284 
show "0 < s" by fact 

285 
next 

286 
fix u v :: real assume "u \<le> x" and "x \<le> v" and "v  u < s" 

287 
have "\<bar>f v  f u  f' x * (v  u)\<bar> = 

288 
\<bar>(f v  f x  f' x * (v  x)) + (f x  f u  f' x * (x  u))\<bar>" 

289 
by (simp add: right_diff_distrib) 

290 
also have "\<dots> \<le> \<bar>f v  f x  f' x * (v  x)\<bar> + \<bar>f x  f u  f' x * (x  u)\<bar>" 

291 
by (rule abs_triangle_ineq) 

292 
also have "\<dots> = \<bar>f v  f x  f' x * (v  x)\<bar> + \<bar>f u  f x  f' x * (u  x)\<bar>" 

293 
by (simp add: right_diff_distrib) 

294 
also have "\<dots> \<le> (e/2) * \<bar>v  x\<bar> + (e/2) * \<bar>u  x\<bar>" 

295 
using `u \<le> x` `x \<le> v` `v  u < s` by (intro add_mono strad, simp_all) 

296 
also have "\<dots> \<le> e * (v  u) / 2 + e * (v  u) / 2" 

297 
using `u \<le> x` `x \<le> v` `0 < e` by (intro add_mono, simp_all) 

298 
also have "\<dots> = e * (v  u)" 

299 
by simp 

300 
finally show "\<bar>f v  f u  f' x * (v  u)\<bar> \<le> e * (v  u)" . 

301 
qed 

302 
qed 

303 
thus ?thesis 

31253  304 
by (simp add: gauge_def) (drule bchoice, auto) 
31252  305 
qed 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

306 

31259
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

307 
lemma fine_listsum_eq_diff: 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

308 
fixes f :: "real \<Rightarrow> real" 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

309 
shows "fine \<delta> (a, b) D \<Longrightarrow> (\<Sum>(u, x, v)\<leftarrow>D. f v  f u) = f b  f a" 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

310 
by (induct set: fine) simp_all 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

311 

15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

312 
lemma FTC1: "[a \<le> b; \<forall>x. a \<le> x & x \<le> b > DERIV f x :> f'(x) ] 
15219  313 
==> Integral(a,b) f' (f(b)  f(a))" 
31252  314 
apply (drule order_le_imp_less_or_eq, auto) 
315 
apply (auto simp add: Integral_def2) 

316 
apply (drule_tac e = "e / (b  a)" in lemma_straddle) 

317 
apply (simp add: divide_pos_pos) 

318 
apply clarify 

319 
apply (rule_tac x="g" in exI, clarify) 

31259
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

320 
apply (clarsimp simp add: rsum_def) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

321 
apply (frule fine_listsum_eq_diff [where f=f]) 
31252  322 
apply (erule subst) 
31259
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

323 
apply (subst listsum_subtractf [symmetric]) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

324 
apply (rule listsum_abs [THEN order_trans]) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

325 
apply (subst map_compose [symmetric, unfolded o_def]) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

326 
apply (subgoal_tac "e = (\<Sum>(u, x, v)\<leftarrow>D. (e / (b  a)) * (v  u))") 
31252  327 
apply (erule ssubst) 
328 
apply (simp add: abs_minus_commute) 

31259
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

329 
apply (rule listsum_mono) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

330 
apply (clarify, rename_tac u x v) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

331 
apply ((drule spec)+, erule mp) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

332 
apply (simp add: mem_fine mem_fine2 mem_fine3) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

333 
apply (frule fine_listsum_eq_diff [where f="\<lambda>x. x"]) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

334 
apply (simp only: split_def) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

335 
apply (subst listsum_const_mult) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

336 
apply simp 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

337 
done 
13958  338 

15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

339 
lemma Integral_subst: "[ Integral(a,b) f k1; k2=k1 ] ==> Integral(a,b) f k2" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

340 
by simp 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

341 

49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

342 
lemma Integral_add: 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

343 
"[ a \<le> b; b \<le> c; Integral(a,b) f' k1; Integral(b,c) f' k2; 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

344 
\<forall>x. a \<le> x & x \<le> c > DERIV f x :> f' x ] 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

345 
==> Integral(a,c) f' (k1 + k2)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

346 
apply (rule FTC1 [THEN Integral_subst], auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

347 
apply (frule FTC1, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

348 
apply (frule_tac a = b in FTC1, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

349 
apply (drule_tac x = x in spec, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

350 
apply (drule_tac ?k2.0 = "f b  f a" in Integral_unique) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

351 
apply (drule_tac [3] ?k2.0 = "f c  f b" in Integral_unique, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

352 
done 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

353 

31259
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

354 
subsection {* Additivity Theorem of Gauge Integral *} 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

355 

15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
15093
diff
changeset

356 
text{* Bartle/Sherbert: Theorem 10.1.5 p. 278 *} 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

357 
lemma Integral_add_fun: 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

358 
"[ a \<le> b; Integral(a,b) f k1; Integral(a,b) g k2 ] 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

359 
==> Integral(a,b) (%x. f x + g x) (k1 + k2)" 
31259
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

360 
unfolding Integral_def 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

361 
apply clarify 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

362 
apply (drule_tac x = "e/2" in spec)+ 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

363 
apply clarsimp 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

364 
apply (rule_tac x = "\<lambda>x. min (\<delta> x) (\<delta>' x)" in exI) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

365 
apply (rule conjI, erule (1) gauge_min) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

366 
apply clarify 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

367 
apply (drule fine_min) 
31259
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

368 
apply (drule_tac x=D in spec, simp)+ 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

369 
apply (drule_tac a = "\<bar>rsum D f  k1\<bar> * 2" and c = "\<bar>rsum D g  k2\<bar> * 2" in add_strict_mono, assumption) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

370 
apply (auto simp only: rsum_add left_distrib [symmetric] 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19765
diff
changeset

371 
mult_2_right [symmetric] real_mult_less_iff1) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

372 
done 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

373 

49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

374 
lemma lemma_Integral_rsum_le: 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

375 
"[ \<forall>x. a \<le> x & x \<le> b > f x \<le> g x; 
31259
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

376 
fine \<delta> (a,b) D 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

377 
] ==> rsum D f \<le> rsum D g" 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

378 
unfolding rsum_def 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

379 
apply (rule listsum_mono) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

380 
apply clarify 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

381 
apply (rule mult_right_mono) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

382 
apply (drule spec, erule mp) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

383 
apply (frule (1) mem_fine) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

384 
apply (frule (1) mem_fine2) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

385 
apply simp 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

386 
apply (frule (1) mem_fine) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

387 
apply simp 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

388 
done 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

389 

49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

390 
lemma Integral_le: 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

391 
"[ a \<le> b; 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

392 
\<forall>x. a \<le> x & x \<le> b > f(x) \<le> g(x); 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

393 
Integral(a,b) f k1; Integral(a,b) g k2 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

394 
] ==> k1 \<le> k2" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

395 
apply (simp add: Integral_def) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

396 
apply (rotate_tac 2) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

397 
apply (drule_tac x = "\<bar>k1  k2\<bar> /2" in spec) 
15221  398 
apply (drule_tac x = "\<bar>k1  k2\<bar> /2" in spec, auto) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

399 
apply (drule gauge_min, assumption) 
31259
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

400 
apply (drule_tac \<delta> = "\<lambda>x. min (\<delta> x) (\<delta>' x)" in fine_exists, assumption, clarify) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

401 
apply (drule fine_min) 
31259
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

402 
apply (drule_tac x = D in spec, drule_tac x = D in spec, clarsimp) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

403 
apply (frule lemma_Integral_rsum_le, assumption) 
31259
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

404 
apply (subgoal_tac "\<bar>(rsum D f  k1)  (rsum D g  k2)\<bar> < \<bar>k1  k2\<bar>") 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

405 
apply arith 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

406 
apply (drule add_strict_mono, assumption) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

407 
apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric] 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19765
diff
changeset

408 
real_mult_less_iff1) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

409 
done 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

410 

49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

411 
lemma Integral_imp_Cauchy: 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

412 
"(\<exists>k. Integral(a,b) f k) ==> 
31259
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

413 
(\<forall>e > 0. \<exists>\<delta>. gauge {a..b} \<delta> & 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

414 
(\<forall>D1 D2. 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

415 
fine \<delta> (a,b) D1 & 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

416 
fine \<delta> (a,b) D2 > 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

417 
\<bar>rsum D1 f  rsum D2 f\<bar> < e))" 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

418 
apply (simp add: Integral_def, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

419 
apply (drule_tac x = "e/2" in spec, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

420 
apply (rule exI, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

421 
apply (frule_tac x = D1 in spec) 
31259
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

422 
apply (drule_tac x = D2 in spec) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

423 
apply simp 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

424 
apply (thin_tac "0 < e") 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

425 
apply (drule add_strict_mono, assumption) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

426 
apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric] 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19765
diff
changeset

427 
real_mult_less_iff1) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

428 
done 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

429 

49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

430 
lemma Cauchy_iff2: 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

431 
"Cauchy X = 
20563  432 
(\<forall>j. (\<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. \<bar>X m  X n\<bar> < inverse(real (Suc j))))" 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

433 
apply (simp add: Cauchy_def, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

434 
apply (drule reals_Archimedean, safe) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

435 
apply (drule_tac x = n in spec, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

436 
apply (rule_tac x = M in exI, auto) 
15360  437 
apply (drule_tac x = m in spec, simp) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

438 
apply (drule_tac x = na in spec, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

439 
done 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

440 

49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

441 
lemma monotonic_anti_derivative: 
20792  442 
fixes f g :: "real => real" shows 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

443 
"[ a \<le> b; \<forall>c. a \<le> c & c \<le> b > f' c \<le> g' c; 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

444 
\<forall>x. DERIV f x :> f' x; \<forall>x. DERIV g x :> g' x ] 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

445 
==> f b  f a \<le> g b  g a" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

446 
apply (rule Integral_le, assumption) 
15219  447 
apply (auto intro: FTC1) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

448 
done 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

449 

49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

450 
end 