author  paulson 
Tue, 19 Oct 2004 18:18:45 +0200  
changeset 15251  bb6f072c8d10 
parent 15234  ec91a90c604e 
child 15360  300e09825d8b 
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 

15131  9 
theory Integration 
15140  10 
imports MacLaurin 
15131  11 
begin 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

12 

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

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

15 
constdefs 

16 

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

17 
{*Partitions and tagged partitions etc.*} 
13958  18 

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

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

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

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

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

23 

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

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

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

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

27 

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

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

30 
(\<forall>n. D(n) \<le> p(n) & p(n) \<le> D(Suc n))" 
13958  31 

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

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

33 

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

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

35 
"gauge E g == \<forall>x. E x > 0 < g(x)" 
13958  36 

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

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

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

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

40 
{*Riemann sum*} 
13958  41 

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

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

44 

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

45 
{*Gauge integrability (definite)*} 
13958  46 

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

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

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

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

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

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

52 

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

53 

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

54 
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

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

56 

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

57 
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

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

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

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

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

62 

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

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

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

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

66 

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

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

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

69 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

88 
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

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

90 

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

91 
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

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

93 

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

94 
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

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

96 

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

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

98 
"partition(a,b) D & m + Suc d \<le> n & n \<le> (psize D) > D(m) < D(m + Suc d)" 
15251  99 
apply (induct "d", auto simp add: partition) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

100 
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

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

102 

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

103 
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

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

105 

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

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

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

108 
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

109 

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

110 
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

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

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

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

114 

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

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

116 
apply (frule partition [THEN iffD1], safe) 
15219  117 
apply (drule_tac x = "psize D" and P="%n. psize D \<le> n > ?P n" in spec, safe) 
118 
apply (case_tac "psize D = 0") 

15093
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) 
15219  131 
apply auto 
15093
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) 
15251  136 
apply (induct "r") 
137 
apply (cut_tac [2] y = "Suc r" and x = "psize D" in linorder_le_less_linear) 

138 
apply (auto intro: partition_le) 

139 
apply (drule_tac x = r in spec) 

140 
apply arith; 

15093
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 
15221  176 
apply (drule_tac x = "psize D  Suc n" in spec, simp) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

178 

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

179 
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

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

181 

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

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

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

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

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

186 
(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

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

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

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

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

191 
(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

192 
(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

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

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

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

196 
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

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

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

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

200 

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

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

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

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

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

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

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

208 

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

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

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

211 
==> psize (%n. if n < psize D1 then D1 n else D2 (n  psize D1)) = 
15219  212 
psize D1 + psize D2" 
213 
apply (unfold psize_def 

214 
[of "%n. if n < psize D1 then D1 n else D2 (n  psize D1)"]) 

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

215 
apply (rule some1_equality) 
15219  216 
prefer 2 apply (blast intro!: lemma_partition_append1) 
217 
apply (rule ex1I, rule lemma_partition_append1) 

218 
apply (simp_all split: split_if_asm) 

219 
txt{*The case @{term "N < psize D1"}*} 

220 
apply (drule_tac x = "psize D1 + psize D2" and P="%n. ?P n & ?Q n" in spec) 

221 
apply (force dest: lemma_psize1) 

222 
apply (rule order_antisym); 

223 
txt{*The case @{term "psize D1 \<le> N"}: 

224 
proving @{term "N \<le> psize D1 + psize D2"}*} 

225 
apply (drule_tac x = "psize D1 + psize D2" in spec) 

226 
apply (simp add: partition_rhs2) 

227 
apply (case_tac "N  psize D1 < psize D2") 

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

228 
prefer 2 apply arith 
15219  229 
txt{*Proving @{term "psize D1 + psize D2 \<le> N"}*} 
230 
apply (drule_tac x = "psize D1 + psize D2" and P="%n. N\<le>n > ?P n" in spec, simp) 

231 
apply (drule_tac a = b and b = c in partition_gt, assumption, simp) 

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

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

233 

15219  234 
lemma tpart_eq_lhs_rhs: "[psize D = 0; tpart(a,b) (D,p)] ==> a = b" 
235 
by (auto simp add: tpart_def partition_eq) 

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

236 

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

237 
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

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

239 

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

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

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

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

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

244 
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

245 
in exI) 
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 p1 n else p2 (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 (case_tac "psize D1 = 0") 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

267 
apply (subst partition) 
15221  268 
apply (subst lemma_partition_append2, assumption+) 
269 
apply (rule conjI) 

270 
apply (drule_tac [2] lemma_partition_append1) 

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

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

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

273 

15219  274 
text{*We can always find a division that is fine wrt any gauge*} 
15093
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 
lemma partition_exists: 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

279 
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

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

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

282 
apply safe 
15219  283 
apply (blast intro: order_trans)+ 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

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

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

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

289 
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

290 
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

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

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

293 

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

294 
text{*Lemmas about combining gauges*} 
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 
lemma gauge_min: 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

298 
==> 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

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

300 

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

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

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

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

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

305 

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

306 

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

307 
text{*The integral is unique if it exists*} 
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 
lemma Integral_unique: 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

312 
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

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

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

315 
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

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

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

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

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

320 
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

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

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

323 
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

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

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

326 

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

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

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

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

330 
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

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

332 

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

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

334 
"sumr 0 m (%n. D (Suc n)  D n) = D(m)  D 0" 
15251  335 
by (induct "m", auto) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

336 

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

337 
lemma Integral_eq_diff_bounds: "a \<le> b ==> Integral(a,b) (%x. 1) (b  a)" 
15219  338 
apply (auto simp add: order_le_less rsum_def Integral_def) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

340 
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

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

342 

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

343 
lemma Integral_mult_const: "a \<le> b ==> Integral(a,b) (%x. c) (c*(b  a))" 
15219  344 
apply (auto simp add: order_le_less rsum_def Integral_def) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

346 
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

347 
right_diff_distrib [symmetric] partition tpart_def) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

349 

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

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

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

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

355 
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

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

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

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

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

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

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

362 
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

363 
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

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

365 

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

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

367 

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

369 

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

370 
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

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

372 

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

373 
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

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

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 
(*UNUSED 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

378 
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

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

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

381 

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

382 

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

383 
(* 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

384 
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

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

386 
"\<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

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

388 
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

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

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

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

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

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

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

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

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

397 
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

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

399 
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

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

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

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

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

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

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

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

407 

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

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

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

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

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

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

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

414 
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

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

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

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

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

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

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

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

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

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

424 
apply (rule_tac x = u and y = v in linorder_cases, auto) 
15219  425 
apply (rule_tac y = "\<bar>(f (v)  f (x))  (f' (x) * (v  x))\<bar> + 
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
15093
diff
changeset

426 
\<bar>(f (x)  f (u))  (f' (x) * (x  u))\<bar>" 
15219  427 
in order_trans) 
428 
apply (rule abs_triangle_ineq [THEN [2] order_trans]) 

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

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

430 
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

431 
apply (rule add_mono) 
15219  432 
apply (rule_tac y = "(e/2) * \<bar>v  x\<bar>" in order_trans) 
15229  433 
prefer 2 apply simp 
15219  434 
apply (erule_tac [!] V= "\<forall>x'. x' ~= x & \<bar>x' +  x\<bar> < s > ?P x'" in thin_rl) 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15229
diff
changeset

435 
apply (drule_tac x = v in spec, simp add: times_divide_eq) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

437 
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

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

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

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

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

442 

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

443 
lemma FTC1: "[a \<le> b; \<forall>x. a \<le> x & x \<le> b > DERIV f x :> f'(x) ] 
15219  444 
==> Integral(a,b) f' (f(b)  f(a))" 
445 
apply (drule order_le_imp_less_or_eq, auto) 

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

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

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

448 
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

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

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

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

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

453 
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

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

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

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

457 
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

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

459 
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

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

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

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

463 
apply (simp (no_asm) add: sumr_diff) 
15219  464 
apply (rule sumr_rabs [THEN order_trans]) 
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
15093
diff
changeset

465 
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

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

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

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

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

470 
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

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

472 
done 
13958  473 

474 

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

475 
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

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

477 

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

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

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

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

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

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

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

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

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

486 
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

487 
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

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

489 

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

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

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

492 
apply (auto intro!: Least_equality [symmetric] partition_rhs) 
15219  493 
apply (auto dest: partition_ub_lt simp add: linorder_not_less [symmetric]) 
15093
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 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

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

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

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

500 

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

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

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

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

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

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

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

507 

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

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

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

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

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

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

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

514 

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

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

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

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

518 

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

519 
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

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

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

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

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

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

525 
done 
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 
subsection{*Lemmas for Additivity Theorem of Gauge Integral*} 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

528 

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

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

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

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

532 

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

533 
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

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

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

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

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

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

539 

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

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

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

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

543 

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

544 
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

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

546 

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

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

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

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

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

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

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

553 

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

554 
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

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

557 
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

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

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

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

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

562 
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

563 
apply (auto dest: partition_eq_bound) 
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 (frule partition_eq_bound, assumption) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

568 

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

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

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

571 
==> 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

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

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

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

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

576 
apply (auto intro: partition_lt_Suc) 
15219  577 
apply (drule_tac n = n in partition_lt_gen, assumption) 
578 
apply (arith, arith) 

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

579 
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

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

581 
apply (rule_tac x=N and y=n in linorder_cases) 
15219  582 
apply (drule_tac x = n and P="%m. N \<le> m > ?f m = ?g m" in spec, simp) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

583 
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

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

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

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

587 

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

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

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

590 
==> 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

591 
apply (frule_tac r = n in partition_ub) 
15219  592 
apply (drule_tac x = "D n" in order_le_imp_less_or_eq) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

594 
apply (frule_tac r = n in partition_lb) 
15219  595 
apply (drule (2) lemma_additivity4_psize_eq) 
596 
apply (rule ccontr, auto) 

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

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

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

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

600 

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

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

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

603 
==> na < psize D" 
15219  604 
by (erule lemma_psize_left_less_psize [THEN [2] less_le_trans]) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

605 

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

606 

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

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

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

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

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

611 
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

612 
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

613 
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

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

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

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

617 

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

618 
lemma psize_const [simp]: "psize (%x. k) = 0" 
15219  619 
by (auto simp add: psize_def) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

620 

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

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

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

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

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

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

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

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

628 

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

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

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

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

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

633 
apply (simp add: partition less_diff_conv) 
15219  634 
apply (simp add: le_diff_conv partition_rhs2 split: nat_diff_split) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

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

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

639 
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

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

641 
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

642 
in spec) 
15219  643 
apply simp 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

645 

15219  646 
lemma psize_le_n: "partition (a, D n) D ==> psize D \<le> n" 
15093
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 (frule partition_lt_Suc, assumption) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

651 

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

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

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

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

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

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

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

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

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

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

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

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

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

664 
apply (drule partition [THEN iffD1], safe) 
15219  665 
apply (drule_tac x = "Suc n" and P="%na. ?s \<le> na \<longrightarrow> D na = D n" in spec, auto) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

667 

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

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

669 
"partition(a,b) D ==> psize (%x. D (x + n)) \<le> psize D  n" 
15219  670 
apply (frule_tac r1 = n in partition_ub [THEN order_le_imp_less_or_eq]) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

671 
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

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

673 

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

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

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

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

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

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

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

681 
apply (rule ccontr, drule not_leE) 
15219  682 
apply (drule_tac less_imp_le [THEN [2] partition_rhs2], assumption, simp) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

684 
apply (simp add: partition) 
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 
(* should be combined with previous theorem; also proof has redundancy *) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

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

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

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

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

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

695 
apply (simp add: partition le_diff_conv) 
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 
lemma lemma_psize_right_eq: 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

702 
"[ partition(a,b) D ] ==> psize (%x. D (x + n)) \<le> psize D" 
15219  703 
apply (frule_tac r1 = n in partition_ub [THEN order_le_imp_less_or_eq]) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

704 
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

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

706 

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

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

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

709 
==> 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

710 
%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

711 
apply (frule_tac r = n in tpart_partition [THEN partition_ub]) 
15219  712 
apply (drule_tac x = "D n" in order_le_imp_less_or_eq) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

713 
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

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

715 
apply (auto simp add: tpart_def) 
15219  716 
apply (drule_tac [2] linorder_not_less [THEN iffD1, THEN order_le_imp_less_or_eq], auto) 
717 
prefer 3 apply (drule_tac x=na in spec, arith) 

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

718 
prefer 2 apply (blast dest: lemma_additivity3) 
15219  719 
apply (frule (2) lemma_additivity4_psize_eq) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

721 
apply (frule partition [THEN iffD1]) 
15219  722 
apply safe 
723 
apply (auto simp add: partition_lt_gen) 

15197  724 
apply (drule (1) partition_lt_cancel, arith) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

726 

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

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

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

729 
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

730 
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

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

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

733 
(%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

734 
%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

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

736 
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

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

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

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

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

741 

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

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

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

744 
==> 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

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

746 
apply (rule_tac x = "N  n" in exI, auto) 
15221  747 
apply (drule_tac x = "na + n" in spec, arith)+ 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

749 

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

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

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

752 
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

753 
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

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

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

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

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

758 
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

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

760 
apply (subgoal_tac "D n \<le> p (na + n)") 
15219  761 
apply (drule_tac y = "p (na + n)" in order_le_imp_less_or_eq) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

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

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

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

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

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

769 
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

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

771 

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

772 
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

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

774 

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

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

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

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

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

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

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

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

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

783 
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

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

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

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

787 
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

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

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

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

791 

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

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

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

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

795 

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

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

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

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

799 
] ==> \<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

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

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

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

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

804 
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

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

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

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

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

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

810 

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

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

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

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

814 
] ==> rsum(D,p) f \<le> rsum(D,p) g" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

816 
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

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

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

819 

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

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

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

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

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

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

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

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

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

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

830 
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

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

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

833 
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

834 
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

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

836 
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

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

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

839 
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

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

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

842 

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

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

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

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

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

847 
(\<forall>D1 D2 p1 p2. 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

849 
tpart(a,b) (D2, p2) & fine g (D2,p2) > 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

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

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

854 
apply (frule_tac x = D1 in spec) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

855 
apply (frule_tac x = D2 in spec) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

857 
apply (erule_tac V = "0 < e" in thin_rl) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

859 
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

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

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

862 

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

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

864 
"Cauchy X = 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

866 
\<bar>X m +  X n\<bar> < inverse(real (Suc j))))" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

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

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

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

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

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

874 

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

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

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

877 
==> \<forall>n. \<exists>D p. tpart (a, b) (D, p) & fine (fa n) (D, p)" 
15219  878 
by (blast dest: partition_exists) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

879 

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

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

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

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

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

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

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

887 

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

888 
end 