author  paulson 
Sat, 31 Jul 2004 20:54:23 +0200  
changeset 15094  a7d1a3fdc30d 
parent 15093  49ede01e9ee6 
child 15105  e194d4d265fb 
permissions  rwrr 
13958  1 
(* Title : Integration.thy 
2 
Author : Jacques D. Fleuriot 

3 
Copyright : 2000 University of Edinburgh 

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

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

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

7 
header{*Theory of Integration*} 
13958  8 

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

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

10 

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

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

13 
constdefs 

14 

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

15 
{*Partitions and tagged partitions etc.*} 
13958  16 

17 
partition :: "[(real*real),nat => real] => bool" 

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

18 
"partition == %(a,b) D. ((D 0 = a) & 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

19 
(\<exists>N. ((\<forall>n. n < N > D(n) < D(Suc n)) & 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

20 
(\<forall>n. N \<le> n > (D(n) = b)))))" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

21 

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

22 
psize :: "(nat => real) => nat" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

23 
"psize D == @N. (\<forall>n. n < N > D(n) < D(Suc n)) & 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

24 
(\<forall>n. N \<le> n > (D(n) = D(N)))" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

25 

13958  26 
tpart :: "[(real*real),((nat => real)*(nat =>real))] => bool" 
27 
"tpart == %(a,b) (D,p). partition(a,b) D & 

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

28 
(\<forall>n. D(n) \<le> p(n) & p(n) \<le> D(Suc n))" 
13958  29 

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

30 
{*Gauges and gaugefine divisions*} 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

31 

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

32 
gauge :: "[real => bool, real => real] => bool" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

33 
"gauge E g == \<forall>x. E x > 0 < g(x)" 
13958  34 

35 
fine :: "[real => real, ((nat => real)*(nat => real))] => bool" 

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

36 
"fine == % g (D,p). \<forall>n. n < (psize D) > D(Suc n)  D(n) < g(p n)" 
13958  37 

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

38 
{*Riemann sum*} 
13958  39 

40 
rsum :: "[((nat=>real)*(nat=>real)),real=>real] => real" 

41 
"rsum == %(D,p) f. sumr 0 (psize(D)) (%n. f(p n) * (D(Suc n)  D(n)))" 

42 

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

43 
{*Gauge integrability (definite)*} 
13958  44 

45 
Integral :: "[(real*real),real=>real,real] => bool" 

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

46 
"Integral == %(a,b) f k. \<forall>e. 0 < e > 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

47 
(\<exists>g. gauge(%x. a \<le> x & x \<le> b) g & 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

48 
(\<forall>D p. tpart(a,b) (D,p) & fine(g)(D,p) > 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

50 

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

51 

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

52 
lemma partition_zero [simp]: "a = b ==> psize (%n. if n = 0 then a else b) = 0" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

54 

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

55 
lemma partition_one [simp]: "a < b ==> psize (%n. if n = 0 then a else b) = 1" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

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

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

60 

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

61 
lemma partition_single [simp]: 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

62 
"a \<le> b ==> partition(a,b)(%n. if n = 0 then a else b)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

63 
by (auto simp add: partition_def order_le_less) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

64 

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

65 
lemma partition_lhs: "partition(a,b) D ==> (D(0) = a)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

67 

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

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

69 
"(partition(a,b) D) = 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

70 
((D 0 = a) & 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

71 
(\<forall>n. n < (psize D) > D n < D(Suc n)) & 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

72 
(\<forall>n. (psize D) \<le> n > (D n = b)))" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

74 
apply (subgoal_tac [!] "psize D = N", auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

75 
apply (simp_all (no_asm) add: psize_def) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

76 
apply (rule_tac [!] some_equality, blast) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

77 
prefer 2 apply blast 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

78 
apply (rule_tac [!] ccontr) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

79 
apply (simp_all add: linorder_neq_iff, safe) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

82 
apply (drule_tac x = "Suc Na" in spec, simp) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

85 
apply (drule_tac x = Na in spec) 
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
15093
diff
changeset

86 
apply (drule_tac x = "Suc Na" and P = "%n. Na\<le>n \<longrightarrow> D n = D Na" in spec, auto) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

88 

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

89 
lemma partition_rhs: "partition(a,b) D ==> (D(psize D) = b)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

91 

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

92 
lemma partition_rhs2: "[partition(a,b) D; psize D \<le> n ] ==> (D n = b)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

94 

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

95 
lemma lemma_partition_lt_gen [rule_format]: 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

96 
"partition(a,b) D & m + Suc d \<le> n & n \<le> (psize D) > D(m) < D(m + Suc d)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

97 
apply (induct_tac "d", auto simp add: partition) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

98 
apply (blast dest: Suc_le_lessD intro: less_le_trans order_less_trans) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

100 

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

101 
lemma less_eq_add_Suc: "m < n ==> \<exists>d. n = m + Suc d" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

103 

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

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

105 
"[partition(a,b) D; m < n; n \<le> (psize D)] ==> D(m) < D(n)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

106 
by (auto dest: less_eq_add_Suc intro: lemma_partition_lt_gen) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

107 

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

108 
lemma partition_lt: "partition(a,b) D ==> n < (psize D) ==> D(0) < D(Suc n)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

109 
apply (induct "n") 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

112 

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

113 
lemma partition_le: "partition(a,b) D ==> a \<le> b" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

114 
apply (frule partition [THEN iffD1], safe) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

116 
apply (drule_tac x = "psize D" in spec, safe) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

117 
apply (rule ccontr) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

118 
apply (case_tac "psize D = 0", safe) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

119 
apply (drule_tac [2] n = "psize D  1" in partition_lt, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

121 

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

122 
lemma partition_gt: "[partition(a,b) D; n < (psize D)] ==> D(n) < D(psize D)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

123 
by (auto intro: partition_lt_gen) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

124 

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

125 
lemma partition_eq: "partition(a,b) D ==> ((a = b) = (psize D = 0))" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

126 
apply (frule partition [THEN iffD1], safe) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

129 
apply (rule ccontr) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

130 
apply (drule_tac n = "psize D  1" in partition_lt) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

131 
prefer 3 apply (blast, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

133 

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

134 
lemma partition_lb: "partition(a,b) D ==> a \<le> D(r)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

135 
apply (frule partition [THEN iffD1], safe) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

136 
apply (induct_tac "r") 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

137 
apply (cut_tac [2] y = "Suc n" and x = "psize D" in linorder_le_less_linear, safe) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

138 
apply (blast intro: order_trans partition_le) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

140 
apply (best intro: order_less_trans order_trans order_less_imp_le) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

142 

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

143 
lemma partition_lb_lt: "[ partition(a,b) D; psize D ~= 0 ] ==> a < D(Suc n)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

144 
apply (rule_tac t = a in partition_lhs [THEN subst], assumption) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

145 
apply (cut_tac x = "Suc n" and y = "psize D" in linorder_le_less_linear) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

146 
apply (frule partition [THEN iffD1], safe) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

147 
apply (blast intro: partition_lt less_le_trans) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

150 
apply (erule impE) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

151 
apply (erule less_imp_le) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

152 
apply (frule partition_rhs) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

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

156 

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

157 
lemma partition_ub: "partition(a,b) D ==> D(r) \<le> b" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

158 
apply (frule partition [THEN iffD1]) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

159 
apply (cut_tac x = "psize D" and y = r in linorder_le_less_linear, safe, blast) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

160 
apply (subgoal_tac "\<forall>x. D ((psize D)  x) \<le> b") 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

162 
apply (drule_tac x = "psize D  r" in spec) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

163 
apply (subgoal_tac "psize D  (psize D  r) = r") 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

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

167 
apply (induct_tac "x") 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

168 
apply (simp (no_asm), blast) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

169 
apply (case_tac "psize D  Suc n = 0") 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

170 
apply (erule_tac V = "\<forall>n. psize D \<le> n > D n = b" in thin_rl) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

172 
apply (rule order_trans) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

173 
prefer 2 apply assumption 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

174 
apply (subgoal_tac "psize D  n = Suc (psize D  Suc n)") 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

176 
apply (drule_tac x = "psize D  Suc n" in spec) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

177 
apply (erule_tac V = "\<forall>n. psize D \<le> n > D n = b" in thin_rl, simp) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

179 

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

180 
lemma partition_ub_lt: "[ partition(a,b) D; n < psize D ] ==> D(n) < b" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

181 
by (blast intro: partition_rhs [THEN subst] partition_gt) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

182 

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

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

184 
"[ partition (a, b) D1; partition (b, c) D2 ] 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

185 
==> (\<forall>n. 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

186 
n < psize D1 + psize D2 > 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

187 
(if n < psize D1 then D1 n else D2 (n  psize D1)) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

188 
< (if Suc n < psize D1 then D1 (Suc n) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

189 
else D2 (Suc n  psize D1))) & 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

190 
(\<forall>n. 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

191 
psize D1 + psize D2 \<le> n > 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

192 
(if n < psize D1 then D1 n else D2 (n  psize D1)) = 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

193 
(if psize D1 + psize D2 < psize D1 then D1 (psize D1 + psize D2) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

194 
else D2 (psize D1 + psize D2  psize D1)))" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

196 
apply (auto intro: partition_lt_gen) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

197 
apply (subgoal_tac "psize D1 = Suc n") 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

198 
apply (auto intro!: partition_lt_gen simp add: partition_lhs partition_ub_lt) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

199 
apply (auto intro!: partition_rhs2 simp add: partition_rhs 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

202 

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

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

204 
"[ partition (a, b) D1; partition (b, c) D2; N < psize D1 ] 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

205 
==> D1(N) < D2 (psize D2)" 
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
15093
diff
changeset

206 
apply (rule_tac y = "D1 (psize D1)" in order_less_le_trans) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

207 
apply (erule partition_gt, assumption) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

208 
apply (auto simp add: partition_rhs partition_le) 
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 lemma_partition_append2: 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

212 
"[ partition (a, b) D1; partition (b, c) D2 ] 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

213 
==> psize (%n. if n < psize D1 then D1 n else D2 (n  psize D1)) = 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

214 
psize D1 + psize D2" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

215 
apply (rule_tac D2 = "%n. if n < psize D1 then D1 n else D2 (n  psize D1) " 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

216 
in psize_def [THEN meta_eq_to_obj_eq, THEN ssubst]) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

217 
apply (rule some1_equality) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

218 
prefer 2 apply (blast intro!: lemma_partition_append1) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

220 
apply (rule ccontr) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

221 
apply (simp add: linorder_neq_iff, safe) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

223 
apply (drule_tac x = "psize D1 + psize D2" in spec, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

224 
apply (case_tac "N < psize D1") 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

225 
apply (auto dest: lemma_psize1) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

226 
apply (subgoal_tac "N  psize D1 < psize D2") 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

228 
apply (drule_tac a = b and b = c in partition_gt, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

229 
apply (drule_tac x = "psize D1 + psize D2" in spec) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

232 

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

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

234 
"[psize D = 0; tpart(a,b) (D,p)] ==> a = b" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

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

238 

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

239 
lemma tpart_partition: "tpart(a,b) (D,p) ==> partition(a,b) D" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

241 

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

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

243 
"[ tpart(a,b) (D1,p1); fine(g) (D1,p1); 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

244 
tpart(b,c) (D2,p2); fine(g) (D2,p2) ] 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

245 
==> \<exists>D p. tpart(a,c) (D,p) & fine(g) (D,p)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

246 
apply (rule_tac x = "%n. if n < psize D1 then D1 n else D2 (n  psize D1)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

248 
apply (rule_tac x = "%n. if n < psize D1 then p1 n else p2 (n  psize D1)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

250 
apply (case_tac "psize D1 = 0") 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

251 
apply (auto dest: tpart_eq_lhs_rhs) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

254 
lemma_partition_append2 [OF tpart_partition tpart_partition]) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

255 
{*But must not expand @{term fine} in other subgoals*} 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

257 
apply (subgoal_tac "psize D1 = Suc n") 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

259 
apply (drule tpart_partition [THEN partition_rhs]) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

260 
apply (drule tpart_partition [THEN partition_lhs]) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

261 
apply (auto split: nat_diff_split) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

264 
apply (subgoal_tac "psize D1 = Suc n") 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

267 
apply (drule partition_lhs, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

268 
apply (simp split: nat_diff_split) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

271 
apply (rule_tac [3] conjI) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

272 
apply (drule_tac [4] lemma_partition_append1) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

275 

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

276 
text{*We can always find a division which is fine wrt any gauge*} 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

277 

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

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

279 
"[ a \<le> b; gauge(%x. a \<le> x & x \<le> b) g ] 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

280 
==> \<exists>D p. tpart(a,b) (D,p) & fine g (D,p)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

281 
apply (cut_tac P = "%(u,v). a \<le> u & v \<le> b > 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

282 
(\<exists>D p. tpart (u,v) (D,p) & fine (g) (D,p))" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

285 
apply (blast intro: real_le_trans)+ 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

286 
apply (auto intro: partition_append) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

287 
apply (case_tac "a \<le> x & x \<le> b") 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

288 
apply (rule_tac [2] x = 1 in exI, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

289 
apply (rule_tac x = "g x" in exI) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

291 
apply (rule_tac x = "%n. if n = 0 then aa else ba" in exI) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

292 
apply (rule_tac x = "%n. if n = 0 then x else ba" in exI) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

295 

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

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

297 

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

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

299 
"[ gauge(E) g1; gauge(E) g2 ] 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

300 
==> gauge(E) (%x. if g1(x) < g2(x) then g1(x) else g2(x))" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

302 

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

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

304 
"fine (%x. if g1(x) < g2(x) then g1(x) else g2(x)) (D,p) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

305 
==> fine(g1) (D,p) & fine(g2) (D,p)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

306 
by (auto simp add: fine_def split: split_if_asm) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

307 

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

308 

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

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

310 

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

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

312 
"[ 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

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

314 
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

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

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

317 
apply (drule_tac g = "%x. if g x < ga x then g x else ga x" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

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

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

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

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

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

325 
apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric] 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

326 
mult_less_cancel_right, arith) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

328 

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

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

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

331 
apply (rule_tac x = "%x. 1" in exI) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

334 

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

335 
lemma sumr_partition_eq_diff_bounds [simp]: 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

336 
"sumr 0 m (%n. D (Suc n)  D n) = D(m)  D 0" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

337 
by (induct_tac "m", auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

338 

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

339 
lemma Integral_eq_diff_bounds: "a \<le> b ==> Integral(a,b) (%x. 1) (b  a)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

340 
apply (drule real_le_imp_less_or_eq, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

342 
apply (rule_tac x = "%x. b  a" in exI) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

343 
apply (auto simp add: gauge_def abs_interval_iff tpart_def partition) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

345 

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

346 
lemma Integral_mult_const: "a \<le> b ==> Integral(a,b) (%x. c) (c*(b  a))" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

349 
apply (rule_tac x = "%x. b  a" in exI) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

350 
apply (auto simp add: sumr_mult [symmetric] gauge_def abs_interval_iff 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

351 
right_diff_distrib [symmetric] partition tpart_def) 
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 

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

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

355 
"[ a \<le> b; Integral(a,b) f k ] ==> Integral(a,b) (%x. c * f x) (c * k)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

357 
apply (auto dest: Integral_unique [OF real_le_refl Integral_zero]) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

358 
apply (auto simp add: rsum_def Integral_def sumr_mult [symmetric] real_mult_assoc) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

359 
apply (rule_tac a2 = c in abs_ge_zero [THEN real_le_imp_less_or_eq, THEN disjE]) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

360 
prefer 2 apply force 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

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

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

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

366 
apply (rule_tac z1 = "inverse (abs c)" in real_mult_less_iff1 [THEN iffD1]) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

367 
apply (auto simp add: divide_inverse [symmetric] right_diff_distrib [symmetric]) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

369 

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

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

371 

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

372 
text{*"Straddle Lemma" : Swartz & Thompson: AMM 95(7) 1988 *} 
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 choiceP: "\<forall>x. P(x) > (\<exists>y. Q x y) ==> \<exists>f. (\<forall>x. P(x) > Q x (f x))" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

376 

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

377 
lemma choiceP2: "\<forall>x. P(x) > (\<exists>y. R(y) & (\<exists>z. Q x y z)) ==> 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

378 
\<exists>f fa. (\<forall>x. P(x) > R(f x) & Q x (f x) (fa x))" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

380 

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

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

382 
lemma choice2: "\<forall>x. (\<exists>y. R(y) & (\<exists>z. Q x y z)) ==> 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

383 
\<exists>f fa. (\<forall>x. R(f x) & Q x (f x) (fa x))" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

385 

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

386 

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

387 
(* new simplifications e.g. (y < x/n) = (y * n < x) are a real nuisance 
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
15093
diff
changeset

388 
they break the original proofs and make new proofs longer!*) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

390 
"\<lbrakk>\<forall>xa::real. xa \<noteq> x \<and> \<bar>xa +  x\<bar> < s \<longrightarrow> 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

391 
\<bar>(f xa  f x) / (xa  x) +  f' x\<bar> * 2 < e; 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

392 
0 < e; a \<le> x; x \<le> b; 0 < s\<rbrakk> 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

393 
\<Longrightarrow> \<forall>z. \<bar>z  x\<bar> < s >\<bar>f z  f x  f' x * (z  x)\<bar> * 2 \<le> e * \<bar>z  x\<bar>" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

395 
apply (case_tac "0 < \<bar>z  x\<bar>") 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

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

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

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

401 
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

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

403 
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

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

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

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

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

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

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

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

411 

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

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

413 
"[ \<forall>x. a \<le> x & x \<le> b > DERIV f x :> f'(x); 0 < e ] 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

414 
==> \<exists>g. gauge(%x. a \<le> x & x \<le> b) g & 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

416 
> \<bar>(f(v)  f(u))  (f'(x) * (v  u))\<bar> \<le> e * (v  u))" 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

418 
apply (subgoal_tac "\<forall>x. a \<le> x & x \<le> b > 
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
15093
diff
changeset

419 
(\<exists>d. 0 < d & 
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
15093
diff
changeset

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

421 
\<bar>(f (v)  f (u))  (f' (x) * (v  u))\<bar> \<le> e * (v  u)))") 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

422 
apply (drule choiceP, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

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

426 
apply (frule strad1, assumption+) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

427 
apply (rule_tac x = s in exI, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

428 
apply (rule_tac x = u and y = v in linorder_cases, auto) 
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
15093
diff
changeset

429 
apply (rule_tac j = "\<bar>(f (v)  f (x))  (f' (x) * (v  x))\<bar> + 
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
15093
diff
changeset

430 
\<bar>(f (x)  f (u))  (f' (x) * (x  u))\<bar>" 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

432 
apply (rule abs_triangle_ineq [THEN [2] real_le_trans]) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

433 
apply (simp add: right_diff_distrib, arith) 
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
15093
diff
changeset

434 
apply (rule_tac t = "e* (v  u)" in real_sum_of_halves [THEN subst]) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

435 
apply (rule add_mono) 
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
15093
diff
changeset

436 
apply (rule_tac j = " (e / 2) * \<bar>v  x\<bar>" in real_le_trans) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

437 
prefer 2 apply simp apply arith 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

438 
apply (erule_tac [!] 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

439 
V= "\<forall>xa. xa ~= x & \<bar>xa +  x\<bar> < s > \<bar>(f xa  f x) / (xa  x) +  f' x\<bar> * 2 < e" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

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

443 
apply (subgoal_tac "\<bar>f u  f x  f' x * (u  x)\<bar> = \<bar>f x  f u  f' x * (x  u)\<bar>") 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

444 
apply (rule order_trans) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

446 
apply (simp add: right_diff_distrib, arith) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

448 

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

449 
lemma FTC1: "[a \<le> b; \<forall>x. a \<le> x & x \<le> b > DERIV f x :> f'(x) ] 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

450 
==> Integral(a,b) f' (f(b)  f(a))" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

451 
apply (drule real_le_imp_less_or_eq, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

453 
apply (rule ccontr) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

454 
apply (subgoal_tac "\<forall>e. 0 < e > (\<exists>g. gauge (%x. a \<le> x & x \<le> b) g & (\<forall>D p. tpart (a, b) (D, p) & fine g (D, p) > \<bar>rsum (D, p) f'  (f b  f a)\<bar> \<le> e))") 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

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

458 
apply ((drule spec)+, auto) 
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
15093
diff
changeset

459 
apply (drule_tac e = "ea/ (b  a)" in lemma_straddle) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

462 
apply (auto simp add: tpart_def rsum_def) 
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
15093
diff
changeset

463 
apply (subgoal_tac "sumr 0 (psize D) (%n. f(D(Suc n))  f(D n)) = f b  f a") 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

465 
apply (cut_tac D = "%n. f (D n)" and m = "psize D" 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

468 
apply (drule sym, simp) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

470 
apply (rule sumr_rabs [THEN real_le_trans]) 
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
15093
diff
changeset

471 
apply (subgoal_tac "ea = sumr 0 (psize D) (%n. (ea / (b  a)) * (D (Suc n)  (D n)))") 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

473 
apply (rule_tac t = ea in ssubst, assumption) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

474 
apply (rule sumr_le2) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

475 
apply (rule_tac [2] sumr_mult [THEN subst]) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

476 
apply (auto simp add: partition_rhs partition_lhs partition_lb partition_ub 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

478 
done 
13958  479 

480 

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

481 
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

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

483 

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

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

485 
"[ 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

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

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

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

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

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

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

492 
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

493 
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

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

495 

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

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

497 
"partition(a,b) D ==> psize D = (LEAST n. D(n) = b)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

498 
apply (auto intro!: Least_equality [symmetric] partition_rhs) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

499 
apply (rule ccontr) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

501 
apply (auto simp add: linorder_not_less [symmetric]) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

503 

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

504 
lemma lemma_partition_bounded: "partition (a, c) D ==> ~ (\<exists>n. c < D(n))" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

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

508 

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

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

510 
"partition (a, c) D ==> D = (%n. if D n < c then D n else c)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

512 
apply (auto dest!: lemma_partition_bounded) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

515 

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

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

517 
"partition (a, c) D ==> D = (%n. if D n \<le> c then D n else c)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

519 
apply (auto dest!: lemma_partition_bounded) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

522 

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

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

524 
"[ partition(a,b) D; n < psize D ] ==> D n < D (Suc n)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

526 

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

527 
lemma tpart_tag_eq: "tpart(a,c) (D,p) ==> p = (%n. if D n < c then p n else c)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

528 
apply (rule ext) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

530 
apply (drule linorder_not_less [THEN iffD1]) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

531 
apply (drule_tac r = "Suc n" in partition_ub) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

534 

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

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

536 

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

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

538 
"[ a \<le> D n; D n < b; partition(a,b) D ] ==> n < psize D" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

539 
by (auto simp add: partition linorder_not_less [symmetric]) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

540 

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

541 
lemma lemma_additivity2: "[ a \<le> D n; partition(a,D n) D ] ==> psize D \<le> n" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

542 
apply (rule ccontr, drule not_leE) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

543 
apply (frule partition [THEN iffD1], safe) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

544 
apply (frule_tac r = "Suc n" in partition_ub) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

545 
apply (auto dest!: spec) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

547 

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

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

549 
"[ partition(a,b) D; psize D < m ] ==> D(m) = D(psize D)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

551 

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

552 
lemma partition_ub2: "[ partition(a,b) D; psize D < m ] ==> D(r) \<le> D(m)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

554 

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

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

556 
"[ tpart(a,b) (D,p); psize D \<le> m ] ==> p(m) = D(m)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

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

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

561 

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

562 
lemma partition_lt_cancel: "[ partition(a,b) D; D m < D n ] ==> m < n" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

563 
apply (cut_tac m = n and n = "psize D" in less_linear, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

564 
apply (rule ccontr, drule leI, drule le_imp_less_or_eq) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

565 
apply (cut_tac m = m and n = "psize D" in less_linear) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

566 
apply (auto dest: partition_gt) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

568 
apply (frule partition_eq_bound) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

569 
apply (drule_tac [2] partition_gt, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

570 
apply (rule ccontr, drule leI, drule le_imp_less_or_eq) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

571 
apply (auto dest: partition_eq_bound) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

572 
apply (rule ccontr, drule leI, drule le_imp_less_or_eq) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

573 
apply (frule partition_eq_bound, assumption) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

576 

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

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

578 
"[ a \<le> D n; D n < b; partition (a, b) D ] 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

579 
==> psize (%x. if D x < D n then D(x) else D n) = n" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

580 
apply (unfold psize_def) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

581 
apply (frule lemma_additivity1) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

583 
apply (rule some_equality) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

584 
apply (auto intro: partition_lt_Suc) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

585 
apply (drule_tac n = n in partition_lt_gen) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

587 
apply (cut_tac m = na and n = "psize D" in less_linear) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

588 
apply (auto dest: partition_lt_cancel) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

589 
apply (rule_tac x=N and y=n in linorder_cases) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

590 
apply (drule_tac x = n and P="%m. N \<le> m > ?f m = ?g m" in spec, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

593 
apply (simp split: split_if_asm) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

595 

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

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

597 
"partition (a, b) D 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

598 
==> psize (%x. if D x < D n then D(x) else D n) \<le> psize D" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

599 
apply (frule_tac r = n in partition_ub) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

600 
apply (drule_tac x = "D n" in real_le_imp_less_or_eq) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

601 
apply (auto simp add: lemma_partition_eq [symmetric]) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

602 
apply (frule_tac r = n in partition_lb) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

604 
apply (rule_tac [3] ccontr, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

605 
apply (frule_tac not_leE [THEN [2] partition_eq_bound]) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

608 

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

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

610 
"[ partition(a,b) D; na < psize (%x. if D x < D n then D(x) else D n) ] 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

611 
==> na < psize D" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

612 
apply (erule_tac lemma_psize_left_less_psize [THEN [2] less_le_trans], assumption) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

614 

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

615 

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

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

617 
"[ partition(a,b) D; D na < D n; D n < D (Suc na); 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

618 
n < psize D ] 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

619 
==> False" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

620 
apply (cut_tac m = n and n = "Suc na" in less_linear, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

621 
apply (drule_tac [2] n = n in partition_lt_gen, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

622 
apply (cut_tac m = "psize D" and n = na in less_linear) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

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

626 

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

627 
lemma psize_const [simp]: "psize (%x. k) = 0" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

628 
by (simp add: psize_def, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

629 

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

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

631 
"[ partition(a,b) D; D na < D n; D n < D (Suc na); 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

632 
na < psize D ] 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

633 
==> False" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

634 
apply (frule_tac m = n in partition_lt_cancel) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

635 
apply (auto intro: lemma_additivity3) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

637 

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

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

639 
"[ partition(a,b) D; D n < b ] ==> psize (%x. D (x + n)) \<le> psize D  n" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

640 
apply (simp add: psize_def [of "(%x. D (x + n))"]); 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

641 
apply (rule_tac a = "psize D  n" in someI2, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

644 
apply (case_tac "psize D \<le> n") 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

647 
apply (rule ccontr, drule not_leE) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

649 
apply (frule partition_rhs, safe) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

650 
apply (frule partition_lt_cancel, assumption) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

651 
apply (drule partition [THEN iffD1], safe) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

652 
apply (subgoal_tac "~ D (psize D  n + n) < D (Suc (psize D  n + n))") 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

654 
apply (drule_tac x = "Suc (psize D)" and P="%n. ?P n \<longrightarrow> D n = D (psize D)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

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

658 

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

659 
lemma psize_le_n: "partition (a, D n) D ==> psize D \<le> n" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

660 
apply (rule ccontr, drule not_leE) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

661 
apply (frule partition_lt_Suc, assumption) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

662 
apply (frule_tac r = "Suc n" in partition_ub, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

664 

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

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

666 
"partition(a,D n) D ==> psize (%x. D (x + n)) \<le> psize D  n" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

667 
apply (simp add: psize_def [of "(%x. D (x + n))"]); 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

668 
apply (rule_tac a = "psize D  n" in someI2, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

671 
apply (case_tac "psize D \<le> n") 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

672 
apply (force intro: partition_rhs2) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

674 
apply (rule ccontr, drule not_leE) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

675 
apply (frule psize_le_n) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

676 
apply (drule_tac x = "psize D  n" in spec, simp) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

677 
apply (drule partition [THEN iffD1], safe) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

678 
apply (drule_tac x = "Suc n" and P="%na. psize D \<le> na \<longrightarrow> D na = D n" in spec, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

680 

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

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

682 
"partition(a,b) D ==> psize (%x. D (x + n)) \<le> psize D  n" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

683 
apply (frule_tac r1 = n in partition_ub [THEN real_le_imp_less_or_eq]) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

684 
apply (blast intro: better_lemma_psize_right_eq1a better_lemma_psize_right_eq1) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

686 

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

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

688 
"[ partition(a,b) D; D n < b ] ==> psize (%x. D (x + n)) \<le> psize D" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

689 
apply (simp add: psize_def [of "(%x. D (x + n))"]); 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

690 
apply (rule_tac a = "psize D  n" in someI2, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

692 
apply (subgoal_tac "n \<le> psize D") 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

694 
apply (rule ccontr, drule not_leE) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

695 
apply (drule_tac less_imp_le [THEN [2] partition_rhs2], auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

696 
apply (rule ccontr, drule not_leE) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

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

700 

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

701 
(* should be combined with previous theorem; also proof has redundancy *) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

703 
"partition(a,D n) D ==> psize (%x. D (x + n)) \<le> psize D" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

704 
apply (simp add: psize_def [of "(%x. D (x + n))"]); 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

705 
apply (rule_tac a = "psize D  n" in someI2, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

707 
apply (case_tac "psize D \<le> n") 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

708 
apply (force intro: partition_rhs2 simp add: le_diff_conv) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

710 
apply (rule ccontr, drule not_leE) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

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

714 

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

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

716 
"[ partition(a,b) D ] ==> psize (%x. D (x + n)) \<le> psize D" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

717 
apply (frule_tac r1 = n in partition_ub [THEN real_le_imp_less_or_eq]) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

718 
apply (blast intro: lemma_psize_right_eq1a lemma_psize_right_eq1) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

720 

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

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

722 
"[ a \<le> D n; tpart (a, b) (D, p) ] 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

723 
==> tpart(a, D n) (%x. if D x < D n then D(x) else D n, 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

724 
%x. if D x < D n then p(x) else D n)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

725 
apply (frule_tac r = n in tpart_partition [THEN partition_ub]) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

726 
apply (drule_tac x = "D n" in real_le_imp_less_or_eq) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

727 
apply (auto simp add: tpart_partition [THEN lemma_partition_eq, symmetric] tpart_tag_eq [symmetric]) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

728 
apply (frule_tac tpart_partition [THEN [3] lemma_additivity1]) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

730 
apply (drule_tac [2] linorder_not_less [THEN iffD1, THEN real_le_imp_less_or_eq], auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

732 
apply (drule linorder_not_less [THEN iffD1]) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

734 
prefer 2 apply (blast dest: lemma_additivity3) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

735 
apply (frule lemma_additivity4_psize_eq) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

737 
apply (rule partition [THEN iffD2]) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

738 
apply (frule partition [THEN iffD1]) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

739 
apply (auto intro: partition_lt_gen) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

740 
apply (drule_tac n = n in partition_lt_gen) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

741 
apply (assumption, arith, blast) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

742 
apply (drule partition_lt_cancel, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

744 

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

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

746 
"[ a \<le> D n; tpart (a, b) (D, p); gauge (%x. a \<le> x & x \<le> D n) g; 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

747 
fine (%x. if x < D n then min (g x) ((D n  x)/ 2) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

748 
else if x = D n then min (g (D n)) (ga (D n)) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

749 
else min (ga x) ((x  D n)/ 2)) (D, p) ] 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

750 
==> fine g 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

751 
(%x. if D x < D n then D(x) else D n, 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

752 
%x. if D x < D n then p(x) else D n)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

753 
apply (auto simp add: fine_def tpart_def gauge_def) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

754 
apply (frule_tac [!] na=na in lemma_psize_left_less_psize2) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

757 
apply (auto dest: lemma_additivity3a simp add: split_if_asm) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

759 

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

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

761 
"[ a \<le> D n; tpart (a, b) (D, p) ] 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

762 
==> tpart(D n, b) (%x. D(x + n),%x. p(x + n))" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

763 
apply (simp add: tpart_def partition_def, safe) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

764 
apply (rule_tac x = "N  n" in exI, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

766 
apply (drule_tac x = "na + n" in spec) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

768 
apply (drule_tac [2] x = "na + n" in spec, arith+) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

770 

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

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

772 
"[ a \<le> D n; tpart (a, b) (D, p); gauge (%x. D n \<le> x & x \<le> b) ga; 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

773 
fine (%x. if x < D n then min (g x) ((D n  x)/ 2) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

774 
else if x = D n then min (g (D n)) (ga (D n)) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

775 
else min (ga x) ((x  D n)/ 2)) (D, p) ] 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

776 
==> fine ga (%x. D(x + n),%x. p(x + n))" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

778 
apply (drule_tac x = "na + n" in spec) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

779 
apply (frule_tac n = n in tpart_partition [THEN better_lemma_psize_right_eq], auto, arith) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

780 
apply (simp add: tpart_def, safe) 
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
15093
diff
changeset

781 
apply (subgoal_tac "D n \<le> p (na + n)") 
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
15093
diff
changeset

782 
apply (drule_tac y = "p (na + n)" in real_le_imp_less_or_eq) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

784 
apply (simp split: split_if_asm, simp) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

787 
apply (drule_tac x = "na + n" in spec, safe) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

788 
apply (rule_tac y="D (na + n)" in order_trans) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

789 
apply (case_tac "na = 0", auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

790 
apply (erule partition_lt_gen [THEN order_less_imp_le], arith+) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

792 

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

793 
lemma rsum_add: "rsum (D, p) (%x. f x + g x) = rsum (D, p) f + rsum(D, p) g" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

794 
by (simp add: rsum_def sumr_add left_distrib) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

795 

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

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

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

798 
"[ 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

799 
==> Integral(a,b) (%x. f x + g x) (k1 + k2)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

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

803 
apply (drule gauge_min, assumption) 
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
15093
diff
changeset

804 
apply (rule_tac x = " (%x. if ga x < gaa x then ga x else gaa x)" in exI) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

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

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

809 
apply (auto simp only: rsum_add left_distrib [symmetric] 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

812 

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

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

814 
"[ partition(a,b) D; r < psize D ] ==> 0 < D (Suc r)  D r" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

816 

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

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

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

819 
tpart(a,b) (D,p) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

820 
] ==> \<forall>n. n \<le> psize D > f (p n) \<le> g (p n)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

822 
apply (auto, frule partition [THEN iffD1], auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

824 
apply (case_tac "n = 0", simp) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

825 
apply (rule partition_lt_gen [THEN order_less_le_trans, THEN order_less_imp_le], auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

826 
apply (drule le_imp_less_or_eq, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

827 
apply (drule_tac [2] x = "psize D" in spec, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

828 
apply (drule_tac r = "Suc n" in partition_ub) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

831 

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

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

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

834 
tpart(a,b) (D,p) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

835 
] ==> rsum(D,p) f \<le> rsum(D,p) g" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

837 
apply (auto intro!: sumr_le2 dest: tpart_partition [THEN partition_lt_gen2] 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

838 
dest!: lemma_Integral_le) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

840 

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

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

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

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

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

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

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

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

848 
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

849 
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

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

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

852 
apply (drule_tac g = "%x. if ga x < gaa x then ga x else gaa x" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

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

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

857 
apply (frule lemma_Integral_rsum_le, assumption) 
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
15093
diff
changeset

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

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

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

861 
apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric] 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

862 
real_mult_less_iff1, arith) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

864 

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

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

866 
"(\<exists>k. Integral(a,b) f k) ==> 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

867 
(\<forall>e. 0 < e > 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

868 
(\<exists>g. gauge (%x. a \<le> x & x \<le> b) g & 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

869 
(\<forall>D1 D2 p1 p2. 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

870 
tpart(a,b) (D1, p1) & fine g (D1,p1) & 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

871 
tpart(a,b) (D2, p2) & fine g (D2,p2) > 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

872 
\<bar>rsum(D1,p1) f  rsum(D2,p2) f\<bar> < e)))" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

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

876 
apply (frule_tac x = D1 in spec) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

877 
apply (frule_tac x = D2 in spec) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

879 
apply (erule_tac V = "0 < e" in thin_rl) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

881 
apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric] 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

882 
real_mult_less_iff1, arith) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

884 

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

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

886 
"Cauchy X = 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

887 
(\<forall>j. (\<exists>M. \<forall>m n. M \<le> m & M \<le> n > 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

888 
\<bar>X m +  X n\<bar> < inverse(real (Suc j))))" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

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

892 
apply (rule_tac x = M in exI, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

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

896 

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

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

898 
"[ a \<le> b; \<forall>n. gauge (%x. a \<le> x & x \<le> b) (fa n) ] 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

899 
==> \<forall>n. \<exists>D p. tpart (a, b) (D, p) & fine (fa n) (D, p)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

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

903 

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

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

905 
"[ 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

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

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

908 
apply (rule Integral_le, assumption) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

909 
apply (rule_tac [2] FTC1) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

910 
apply (rule_tac [4] FTC1, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

912 

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

913 
end 