author | wenzelm |
Mon, 29 Dec 2008 15:16:01 +0100 | |
changeset 29192 | 082ee2a01a6d |
parent 28952 | 15a4b2cf8c34 |
child 29352 | 165e959721c2 |
permissions | -rw-r--r-- |
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28562
diff
changeset
|
1 |
(* Author : Jacques D. Fleuriot |
13958 | 2 |
Copyright : 2000 University of Edinburgh |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
3 |
Conversion to Isar and new proofs by Lawrence C Paulson, 2004 |
13958 | 4 |
*) |
5 |
||
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
6 |
header{*Theory of Integration*} |
13958 | 7 |
|
15131 | 8 |
theory Integration |
15140 | 9 |
imports MacLaurin |
15131 | 10 |
begin |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
11 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
12 |
text{*We follow John Harrison in formalizing the Gauge integral.*} |
13958 | 13 |
|
19765 | 14 |
definition |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
15 |
--{*Partitions and tagged partitions etc.*} |
13958 | 16 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20792
diff
changeset
|
17 |
partition :: "[(real*real),nat => real] => bool" where |
28562 | 18 |
[code del]: "partition = (%(a,b) D. D 0 = a & |
15360 | 19 |
(\<exists>N. (\<forall>n < N. D(n) < D(Suc n)) & |
19765 | 20 |
(\<forall>n \<ge> N. D(n) = b)))" |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
21 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20792
diff
changeset
|
22 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20792
diff
changeset
|
23 |
psize :: "(nat => real) => nat" where |
28562 | 24 |
[code del]:"psize D = (SOME N. (\<forall>n < N. D(n) < D(Suc n)) & |
19765 | 25 |
(\<forall>n \<ge> N. D(n) = D(N)))" |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
26 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20792
diff
changeset
|
27 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20792
diff
changeset
|
28 |
tpart :: "[(real*real),((nat => real)*(nat =>real))] => bool" where |
28562 | 29 |
[code del]:"tpart = (%(a,b) (D,p). partition(a,b) D & |
19765 | 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 gauge-fine divisions*} |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
33 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20792
diff
changeset
|
34 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20792
diff
changeset
|
35 |
gauge :: "[real => bool, real => real] => bool" where |
28562 | 36 |
[code del]:"gauge E g = (\<forall>x. E x --> 0 < g(x))" |
13958 | 37 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20792
diff
changeset
|
38 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20792
diff
changeset
|
39 |
fine :: "[real => real, ((nat => real)*(nat => real))] => bool" where |
28562 | 40 |
[code del]:"fine = (%g (D,p). \<forall>n. n < (psize D) --> D(Suc n) - D(n) < g(p n))" |
13958 | 41 |
|
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
42 |
--{*Riemann sum*} |
13958 | 43 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20792
diff
changeset
|
44 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20792
diff
changeset
|
45 |
rsum :: "[((nat=>real)*(nat=>real)),real=>real] => real" where |
19765 | 46 |
"rsum = (%(D,p) f. \<Sum>n=0..<psize(D). f(p n) * (D(Suc n) - D(n)))" |
13958 | 47 |
|
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
48 |
--{*Gauge integrability (definite)*} |
13958 | 49 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20792
diff
changeset
|
50 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20792
diff
changeset
|
51 |
Integral :: "[(real*real),real=>real,real] => bool" where |
28562 | 52 |
[code del]: "Integral = (%(a,b) f k. \<forall>e > 0. |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
53 |
(\<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
|
54 |
(\<forall>D p. tpart(a,b) (D,p) & fine(g)(D,p) --> |
19765 | 55 |
\<bar>rsum(D,p) f - k\<bar> < e)))" |
15093
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 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
58 |
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
|
59 |
by (auto simp add: psize_def) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
60 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
61 |
lemma partition_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
|
62 |
apply (simp add: psize_def) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
63 |
apply (rule some_equality, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
64 |
apply (drule_tac x = 1 in spec, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
65 |
done |
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_single [simp]: |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
68 |
"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
|
69 |
by (auto simp add: partition_def order_le_less) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
70 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
71 |
lemma partition_lhs: "partition(a,b) D ==> (D(0) = a)" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
72 |
by (simp add: partition_def) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
73 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
74 |
lemma partition: |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
75 |
"(partition(a,b) D) = |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
76 |
((D 0 = a) & |
15360 | 77 |
(\<forall>n < psize D. D n < D(Suc n)) & |
78 |
(\<forall>n \<ge> psize D. D n = b))" |
|
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
79 |
apply (simp add: partition_def, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
80 |
apply (subgoal_tac [!] "psize D = N", auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
81 |
apply (simp_all (no_asm) add: psize_def) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
82 |
apply (rule_tac [!] some_equality, blast) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
83 |
prefer 2 apply blast |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
84 |
apply (rule_tac [!] ccontr) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
85 |
apply (simp_all add: linorder_neq_iff, safe) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
86 |
apply (drule_tac x = Na in spec) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
87 |
apply (rotate_tac 3) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
88 |
apply (drule_tac x = "Suc Na" in spec, simp) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
89 |
apply (rotate_tac 2) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
90 |
apply (drule_tac x = N in spec, simp) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
91 |
apply (drule_tac x = Na in spec) |
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
15093
diff
changeset
|
92 |
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
|
93 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
94 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
95 |
lemma partition_rhs: "partition(a,b) D ==> (D(psize D) = b)" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
96 |
by (simp add: partition) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
97 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
98 |
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
|
99 |
by (simp add: partition) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
100 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
101 |
lemma lemma_partition_lt_gen [rule_format]: |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
102 |
"partition(a,b) D & m + Suc d \<le> n & n \<le> (psize D) --> D(m) < D(m + Suc d)" |
15251 | 103 |
apply (induct "d", auto simp add: partition) |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
104 |
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
|
105 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
106 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
107 |
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
|
108 |
by (auto simp add: less_iff_Suc_add) |
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_gen: |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
111 |
"[|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
|
112 |
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
|
113 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
114 |
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
|
115 |
apply (induct "n") |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
116 |
apply (auto simp add: partition) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
117 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
118 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
119 |
lemma partition_le: "partition(a,b) D ==> a \<le> b" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
120 |
apply (frule partition [THEN iffD1], safe) |
15219 | 121 |
apply (drule_tac x = "psize D" and P="%n. psize D \<le> n --> ?P n" in spec, safe) |
122 |
apply (case_tac "psize D = 0") |
|
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
123 |
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
|
124 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
125 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
126 |
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
|
127 |
by (auto intro: partition_lt_gen) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
128 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
129 |
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
|
130 |
apply (frule partition [THEN iffD1], safe) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
131 |
apply (rotate_tac 2) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
132 |
apply (drule_tac x = "psize D" in spec) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
133 |
apply (rule ccontr) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
134 |
apply (drule_tac n = "psize D - 1" in partition_lt) |
15219 | 135 |
apply auto |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
136 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
137 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
138 |
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
|
139 |
apply (frule partition [THEN iffD1], safe) |
15251 | 140 |
apply (induct "r") |
141 |
apply (cut_tac [2] y = "Suc r" and x = "psize D" in linorder_le_less_linear) |
|
142 |
apply (auto intro: partition_le) |
|
143 |
apply (drule_tac x = r in spec) |
|
144 |
apply arith; |
|
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
145 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
146 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
147 |
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
|
148 |
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
|
149 |
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
|
150 |
apply (frule partition [THEN iffD1], safe) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
151 |
apply (blast intro: partition_lt less_le_trans) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
152 |
apply (rotate_tac 3) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
153 |
apply (drule_tac x = "Suc n" in spec) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
154 |
apply (erule impE) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
155 |
apply (erule less_imp_le) |
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset
|
156 |
apply (frule partition_rhs) |
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset
|
157 |
apply (drule partition_gt[of _ _ _ 0], arith) |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
158 |
apply (simp (no_asm_simp)) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
159 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
160 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
161 |
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
|
162 |
apply (frule partition [THEN iffD1]) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
163 |
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
|
164 |
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
|
165 |
apply (rotate_tac 4) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
166 |
apply (drule_tac x = "psize D - r" in spec) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
167 |
apply (subgoal_tac "psize D - (psize D - r) = r") |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
168 |
apply simp |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
169 |
apply arith |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
170 |
apply safe |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
171 |
apply (induct_tac "x") |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
172 |
apply (simp (no_asm), blast) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
173 |
apply (case_tac "psize D - Suc n = 0") |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
174 |
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
|
175 |
apply (simp (no_asm_simp) add: partition_le) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
176 |
apply (rule order_trans) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
177 |
prefer 2 apply assumption |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
178 |
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
|
179 |
prefer 2 apply arith |
20432
07ec57376051
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20256
diff
changeset
|
180 |
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
|
181 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
182 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
183 |
lemma 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
|
184 |
by (blast intro: partition_rhs [THEN subst] partition_gt) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
185 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
186 |
lemma lemma_partition_append1: |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
187 |
"[| partition (a, b) D1; partition (b, c) D2 |] |
15360 | 188 |
==> (\<forall>n < psize D1 + psize D2. |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
189 |
(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
|
190 |
< (if Suc n < psize D1 then D1 (Suc n) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
191 |
else D2 (Suc n - psize D1))) & |
15360 | 192 |
(\<forall>n \<ge> psize D1 + psize D2. |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
193 |
(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
|
194 |
(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
|
195 |
else D2 (psize D1 + psize D2 - psize D1)))" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
196 |
apply (auto intro: partition_lt_gen) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
197 |
apply (subgoal_tac "psize D1 = Suc n") |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
198 |
apply (auto intro!: partition_lt_gen simp add: partition_lhs partition_ub_lt) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
199 |
apply (auto intro!: partition_rhs2 simp add: partition_rhs |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
200 |
split: nat_diff_split) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
201 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
202 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
203 |
lemma lemma_psize1: |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
204 |
"[| partition (a, b) D1; partition (b, c) D2; N < psize D1 |] |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
205 |
==> D1(N) < D2 (psize D2)" |
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
15093
diff
changeset
|
206 |
apply (rule_tac y = "D1 (psize D1)" in order_less_le_trans) |
15219 | 207 |
apply (erule partition_gt) |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
208 |
apply (auto simp add: partition_rhs partition_le) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
209 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
210 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
211 |
lemma lemma_partition_append2: |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
212 |
"[| partition (a, b) D1; partition (b, c) D2 |] |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
213 |
==> psize (%n. if n < psize D1 then D1 n else D2 (n - psize D1)) = |
15219 | 214 |
psize D1 + psize D2" |
215 |
apply (unfold psize_def |
|
216 |
[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
|
217 |
apply (rule some1_equality) |
15219 | 218 |
prefer 2 apply (blast intro!: lemma_partition_append1) |
219 |
apply (rule ex1I, rule lemma_partition_append1) |
|
220 |
apply (simp_all split: split_if_asm) |
|
221 |
txt{*The case @{term "N < psize D1"}*} |
|
222 |
apply (drule_tac x = "psize D1 + psize D2" and P="%n. ?P n & ?Q n" in spec) |
|
223 |
apply (force dest: lemma_psize1) |
|
224 |
apply (rule order_antisym); |
|
225 |
txt{*The case @{term "psize D1 \<le> N"}: |
|
226 |
proving @{term "N \<le> psize D1 + psize D2"}*} |
|
227 |
apply (drule_tac x = "psize D1 + psize D2" in spec) |
|
228 |
apply (simp add: partition_rhs2) |
|
229 |
apply (case_tac "N - psize D1 < psize D2") |
|
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
230 |
prefer 2 apply arith |
15219 | 231 |
txt{*Proving @{term "psize D1 + psize D2 \<le> N"}*} |
232 |
apply (drule_tac x = "psize D1 + psize D2" and P="%n. N\<le>n --> ?P n" in spec, simp) |
|
233 |
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
|
234 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
235 |
|
15219 | 236 |
lemma tpart_eq_lhs_rhs: "[|psize D = 0; tpart(a,b) (D,p)|] ==> a = b" |
237 |
by (auto simp add: tpart_def partition_eq) |
|
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
238 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
239 |
lemma tpart_partition: "tpart(a,b) (D,p) ==> partition(a,b) D" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
240 |
by (simp add: tpart_def) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
241 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
242 |
lemma partition_append: |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
243 |
"[| tpart(a,b) (D1,p1); fine(g) (D1,p1); |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
244 |
tpart(b,c) (D2,p2); fine(g) (D2,p2) |] |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
245 |
==> \<exists>D p. tpart(a,c) (D,p) & fine(g) (D,p)" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
246 |
apply (rule_tac x = "%n. if n < psize D1 then D1 n else D2 (n - psize D1)" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
247 |
in exI) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
248 |
apply (rule_tac x = "%n. if n < psize D1 then p1 n else p2 (n - psize D1)" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
249 |
in exI) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
250 |
apply (case_tac "psize D1 = 0") |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
251 |
apply (auto dest: tpart_eq_lhs_rhs) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
252 |
prefer 2 |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
253 |
apply (simp add: fine_def |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
254 |
lemma_partition_append2 [OF tpart_partition tpart_partition]) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
255 |
--{*But must not expand @{term fine} in other subgoals*} |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
256 |
apply auto |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
257 |
apply (subgoal_tac "psize D1 = Suc n") |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
258 |
prefer 2 apply arith |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
259 |
apply (drule tpart_partition [THEN partition_rhs]) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
260 |
apply (drule tpart_partition [THEN partition_lhs]) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
261 |
apply (auto split: nat_diff_split) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
262 |
apply (auto simp add: tpart_def) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
263 |
defer 1 |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
264 |
apply (subgoal_tac "psize D1 = Suc n") |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
265 |
prefer 2 apply arith |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
266 |
apply (drule partition_rhs) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
267 |
apply (drule partition_lhs, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
268 |
apply (simp split: nat_diff_split) |
15944 | 269 |
apply (subst partition) |
270 |
apply (subst (1 2) lemma_partition_append2, assumption+) |
|
271 |
apply (rule conjI) |
|
272 |
apply (simp add: partition_lhs) |
|
273 |
apply (drule lemma_partition_append1) |
|
274 |
apply assumption; |
|
275 |
apply (simp add: partition_rhs) |
|
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
276 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
277 |
|
15481 | 278 |
|
15219 | 279 |
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
|
280 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
281 |
lemma partition_exists: |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
282 |
"[| 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
|
283 |
==> \<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
|
284 |
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
|
285 |
(\<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
|
286 |
in lemma_BOLZANO2) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
287 |
apply safe |
15219 | 288 |
apply (blast intro: order_trans)+ |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
289 |
apply (auto intro: partition_append) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
290 |
apply (case_tac "a \<le> x & x \<le> b") |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
291 |
apply (rule_tac [2] x = 1 in exI, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
292 |
apply (rule_tac x = "g x" in exI) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
293 |
apply (auto simp add: gauge_def) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
294 |
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
|
295 |
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
|
296 |
apply (auto simp add: tpart_def fine_def) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
297 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
298 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
299 |
text{*Lemmas about combining gauges*} |
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 gauge_min: |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
302 |
"[| gauge(E) g1; gauge(E) g2 |] |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
303 |
==> 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
|
304 |
by (simp add: gauge_def) |
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 |
lemma fine_min: |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
307 |
"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
|
308 |
==> fine(g1) (D,p) & fine(g2) (D,p)" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
309 |
by (auto simp add: fine_def split: split_if_asm) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
310 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
311 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
312 |
text{*The integral is unique if it exists*} |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
313 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
314 |
lemma Integral_unique: |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
315 |
"[| 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
|
316 |
apply (simp add: Integral_def) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
317 |
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
|
318 |
apply auto |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
319 |
apply (drule gauge_min, assumption) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
320 |
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
|
321 |
in partition_exists, assumption, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
322 |
apply (drule fine_min) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
323 |
apply (drule spec)+ |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
324 |
apply auto |
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
15093
diff
changeset
|
325 |
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
|
326 |
apply arith |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
327 |
apply (drule add_strict_mono, assumption) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
328 |
apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric] |
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
16924
diff
changeset
|
329 |
mult_less_cancel_right) |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
330 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
331 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
332 |
lemma Integral_zero [simp]: "Integral(a,a) f 0" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
333 |
apply (auto simp add: Integral_def) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
334 |
apply (rule_tac x = "%x. 1" in exI) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
335 |
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
|
336 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
337 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
338 |
lemma sumr_partition_eq_diff_bounds [simp]: |
15539 | 339 |
"(\<Sum>n=0..<m. D (Suc n) - D n::real) = D(m) - D 0" |
15251 | 340 |
by (induct "m", auto) |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
341 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
342 |
lemma Integral_eq_diff_bounds: "a \<le> b ==> Integral(a,b) (%x. 1) (b - a)" |
15219 | 343 |
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
|
344 |
apply (rule_tac x = "%x. b - a" in exI) |
22998 | 345 |
apply (auto simp add: gauge_def abs_less_iff tpart_def partition) |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
346 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
347 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
348 |
lemma Integral_mult_const: "a \<le> b ==> Integral(a,b) (%x. c) (c*(b - a))" |
15219 | 349 |
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
|
350 |
apply (rule_tac x = "%x. b - a" in exI) |
22998 | 351 |
apply (auto simp add: setsum_right_distrib [symmetric] gauge_def abs_less_iff |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
352 |
right_diff_distrib [symmetric] partition tpart_def) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
353 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
354 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
355 |
lemma Integral_mult: |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
356 |
"[| a \<le> b; Integral(a,b) f k |] ==> Integral(a,b) (%x. c * f x) (c * k)" |
15221 | 357 |
apply (auto simp add: order_le_less |
358 |
dest: Integral_unique [OF order_refl Integral_zero]) |
|
19279 | 359 |
apply (auto simp add: rsum_def Integral_def setsum_right_distrib[symmetric] mult_assoc) |
22998 | 360 |
apply (rule_tac a2 = c in abs_ge_zero [THEN order_le_imp_less_or_eq, THEN disjE]) |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
361 |
prefer 2 apply force |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
362 |
apply (drule_tac x = "e/abs c" in spec, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
363 |
apply (simp add: zero_less_mult_iff divide_inverse) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
364 |
apply (rule exI, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
365 |
apply (drule spec)+ |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
366 |
apply auto |
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
15093
diff
changeset
|
367 |
apply (rule_tac z1 = "inverse (abs c)" in real_mult_less_iff1 [THEN iffD1]) |
16924 | 368 |
apply (auto simp add: abs_mult divide_inverse [symmetric] right_diff_distrib [symmetric]) |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
369 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
370 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
371 |
text{*Fundamental theorem of calculus (Part I)*} |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
372 |
|
15105 | 373 |
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
|
374 |
|
16588 | 375 |
lemma choiceP: "\<forall>x. P(x) --> (\<exists>y. Q x y) ==> \<exists>f. (\<forall>x. P(x) --> Q x (f x))" |
376 |
by (insert bchoice [of "Collect P" Q], simp) |
|
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
377 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
378 |
(*UNUSED |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
379 |
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
|
380 |
\<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
|
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 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
384 |
(* 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
|
385 |
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
|
386 |
lemma strad1: |
20563 | 387 |
"\<lbrakk>\<forall>xa::real. xa \<noteq> x \<and> \<bar>xa - x\<bar> < s \<longrightarrow> |
388 |
\<bar>(f xa - f x) / (xa - x) - f' x\<bar> * 2 < e; |
|
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
389 |
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
|
390 |
\<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
|
391 |
apply auto |
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
15093
diff
changeset
|
392 |
apply (case_tac "0 < \<bar>z - x\<bar>") |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
393 |
prefer 2 apply (simp add: zero_less_abs_iff) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
394 |
apply (drule_tac x = z in spec) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
395 |
apply (rule_tac z1 = "\<bar>inverse (z - x)\<bar>" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
396 |
in real_mult_le_cancel_iff2 [THEN iffD1]) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
397 |
apply simp |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
398 |
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
|
399 |
mult_assoc [symmetric]) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
400 |
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
|
401 |
= (f z - f x) / (z - x) - f' x") |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
402 |
apply (simp add: abs_mult [symmetric] mult_ac diff_minus) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
403 |
apply (subst mult_commute) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
404 |
apply (simp add: left_distrib diff_minus) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
405 |
apply (simp add: mult_assoc divide_inverse) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
406 |
apply (simp add: left_distrib) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
407 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
408 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
409 |
lemma lemma_straddle: |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
410 |
"[| \<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
|
411 |
==> \<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
|
412 |
(\<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
|
413 |
--> \<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
|
414 |
apply (simp add: gauge_def) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
415 |
apply (subgoal_tac "\<forall>x. a \<le> x & x \<le> b --> |
15360 | 416 |
(\<exists>d > 0. \<forall>u v. u \<le> x & x \<le> v & (v - u) < d --> |
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]) |
|
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19765
diff
changeset
|
429 |
apply (simp add: right_diff_distrib) |
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 |
20563 | 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) |
16775
c1b87ef4a1c3
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
avigad
parents:
16588
diff
changeset
|
436 |
apply (drule_tac x = u in spec, auto) |
15093
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) |
22998 | 439 |
apply (auto simp add: abs_le_iff) |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19765
diff
changeset
|
440 |
apply (simp add: right_diff_distrib) |
15093
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) |
15360 | 448 |
apply (subgoal_tac "\<forall>e > 0. \<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)") |
15093
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) |
15539 | 457 |
apply (subgoal_tac "(\<Sum>n=0..<psize D. 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) |
15536 | 463 |
apply (simp (no_asm) add: setsum_subtractf[symmetric]) |
464 |
apply (rule setsum_abs [THEN order_trans]) |
|
15539 | 465 |
apply (subgoal_tac "ea = (\<Sum>n=0..<psize D. (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) |
15539 | 468 |
apply (rule setsum_mono) |
19279 | 469 |
apply (rule_tac [2] setsum_right_distrib [THEN subst]) |
15093
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" |
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
23315
diff
changeset
|
555 |
apply (cut_tac less_linear [of n "psize D"], auto) |
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
23315
diff
changeset
|
556 |
apply (cut_tac less_linear [of m n]) |
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
23315
diff
changeset
|
557 |
apply (cut_tac less_linear [of m "psize D"]) |
15093
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) |
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25134
diff
changeset
|
562 |
apply (metis dense_linear_order_class.dlo_simps(8) not_less partition_rhs partition_rhs2) |
26316
9e9e67e33557
removed redundant less_trans, less_linear, le_imp_less_or_eq, le_less_trans, less_le_trans (cf. Orderings.thy);
wenzelm
parents:
26072
diff
changeset
|
563 |
apply (metis le_less_trans dense_linear_order_class.dlo_simps(8) nat_le_linear partition_eq_bound partition_rhs2) |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
564 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
565 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
566 |
lemma lemma_additivity4_psize_eq: |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
567 |
"[| 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
|
568 |
==> 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
|
569 |
apply (unfold psize_def) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
570 |
apply (frule lemma_additivity1) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
571 |
apply (assumption, assumption) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
572 |
apply (rule some_equality) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
573 |
apply (auto intro: partition_lt_Suc) |
15219 | 574 |
apply (drule_tac n = n in partition_lt_gen, assumption) |
575 |
apply (arith, arith) |
|
26316
9e9e67e33557
removed redundant less_trans, less_linear, le_imp_less_or_eq, le_less_trans, less_le_trans (cf. Orderings.thy);
wenzelm
parents:
26072
diff
changeset
|
576 |
apply (cut_tac x = na and y = "psize D" in less_linear) |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
577 |
apply (auto dest: partition_lt_cancel) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
578 |
apply (rule_tac x=N and y=n in linorder_cases) |
15219 | 579 |
apply (drule_tac x = n and P="%m. N \<le> m --> ?f m = ?g m" in spec, simp) |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19765
diff
changeset
|
580 |
apply (drule_tac n = n in partition_lt_gen, auto) |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
581 |
apply (drule_tac x = n in spec) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
582 |
apply (simp split: split_if_asm) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
583 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
584 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
585 |
lemma lemma_psize_left_less_psize: |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
586 |
"partition (a, b) D |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
587 |
==> 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
|
588 |
apply (frule_tac r = n in partition_ub) |
15219 | 589 |
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
|
590 |
apply (auto simp add: lemma_partition_eq [symmetric]) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
591 |
apply (frule_tac r = n in partition_lb) |
15219 | 592 |
apply (drule (2) lemma_additivity4_psize_eq) |
593 |
apply (rule ccontr, auto) |
|
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
594 |
apply (frule_tac not_leE [THEN [2] partition_eq_bound]) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
595 |
apply (auto simp add: partition_rhs) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
596 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
597 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
598 |
lemma lemma_psize_left_less_psize2: |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
599 |
"[| 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
|
600 |
==> na < psize D" |
15219 | 601 |
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
|
602 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
603 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
604 |
lemma lemma_additivity3: |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
605 |
"[| 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
|
606 |
n < psize D |] |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
607 |
==> False" |
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
23315
diff
changeset
|
608 |
by (metis not_less_eq partition_lt_cancel real_of_nat_less_iff) |
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
23315
diff
changeset
|
609 |
|
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
610 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
611 |
lemma psize_const [simp]: "psize (%x. k) = 0" |
15219 | 612 |
by (auto simp add: psize_def) |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
613 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
614 |
lemma lemma_additivity3a: |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
615 |
"[| 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
|
616 |
na < psize D |] |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
617 |
==> False" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
618 |
apply (frule_tac m = n in partition_lt_cancel) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
619 |
apply (auto intro: lemma_additivity3) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
620 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
621 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
622 |
lemma better_lemma_psize_right_eq1: |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
623 |
"[| 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
|
624 |
apply (simp add: psize_def [of "(%x. D (x + n))"]); |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
625 |
apply (rule_tac a = "psize D - n" in someI2, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
626 |
apply (simp add: partition less_diff_conv) |
15219 | 627 |
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
|
628 |
apply (drule_tac x = "psize D - n" in spec, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
629 |
apply (frule partition_rhs, safe) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
630 |
apply (frule partition_lt_cancel, assumption) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
631 |
apply (drule partition [THEN iffD1], safe) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
632 |
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
|
633 |
apply blast |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
634 |
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
|
635 |
in spec) |
15219 | 636 |
apply simp |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
637 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
638 |
|
15219 | 639 |
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
|
640 |
apply (rule ccontr, drule not_leE) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
641 |
apply (frule partition_lt_Suc, assumption) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
642 |
apply (frule_tac r = "Suc n" in partition_ub, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
643 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
644 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
645 |
lemma better_lemma_psize_right_eq1a: |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
646 |
"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
|
647 |
apply (simp add: psize_def [of "(%x. D (x + n))"]); |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
648 |
apply (rule_tac a = "psize D - n" in someI2, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
649 |
apply (simp add: partition less_diff_conv) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
650 |
apply (simp add: le_diff_conv) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
651 |
apply (case_tac "psize D \<le> n") |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
652 |
apply (force intro: partition_rhs2) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
653 |
apply (simp add: partition linorder_not_le) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
654 |
apply (rule ccontr, drule not_leE) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
655 |
apply (frule psize_le_n) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
656 |
apply (drule_tac x = "psize D - n" in spec, simp) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
657 |
apply (drule partition [THEN iffD1], safe) |
15219 | 658 |
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
|
659 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
660 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
661 |
lemma better_lemma_psize_right_eq: |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
662 |
"partition(a,b) D ==> psize (%x. D (x + n)) \<le> psize D - n" |
15219 | 663 |
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
|
664 |
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
|
665 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
666 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
667 |
lemma lemma_psize_right_eq1: |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
668 |
"[| partition(a,b) D; D n < b |] ==> psize (%x. D (x + n)) \<le> psize D" |
15219 | 669 |
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
|
670 |
apply (rule_tac a = "psize D - n" in someI2, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
671 |
apply (simp add: partition less_diff_conv) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
672 |
apply (subgoal_tac "n \<le> psize D") |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
673 |
apply (simp add: partition le_diff_conv) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
674 |
apply (rule ccontr, drule not_leE) |
15219 | 675 |
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
|
676 |
apply (drule_tac x = "psize D" in spec) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
677 |
apply (simp add: partition) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
678 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
679 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
680 |
(* should be combined with previous theorem; also proof has redundancy *) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
681 |
lemma lemma_psize_right_eq1a: |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
682 |
"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
|
683 |
apply (simp add: psize_def [of "(%x. D (x + n))"]); |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
684 |
apply (rule_tac a = "psize D - n" in someI2, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
685 |
apply (simp add: partition less_diff_conv) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
686 |
apply (case_tac "psize D \<le> n") |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
687 |
apply (force intro: partition_rhs2 simp add: le_diff_conv) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
688 |
apply (simp add: partition le_diff_conv) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
689 |
apply (rule ccontr, drule not_leE) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
690 |
apply (drule_tac x = "psize D" in spec) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
691 |
apply (simp add: partition) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
692 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
693 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
694 |
lemma lemma_psize_right_eq: |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
695 |
"[| partition(a,b) D |] ==> psize (%x. D (x + n)) \<le> psize D" |
15219 | 696 |
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
|
697 |
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
|
698 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
699 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
700 |
lemma tpart_left1: |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
701 |
"[| a \<le> D n; tpart (a, b) (D, p) |] |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
702 |
==> 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
|
703 |
%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
|
704 |
apply (frule_tac r = n in tpart_partition [THEN partition_ub]) |
15219 | 705 |
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
|
706 |
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
|
707 |
apply (frule_tac tpart_partition [THEN [3] lemma_additivity1]) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
708 |
apply (auto simp add: tpart_def) |
15219 | 709 |
apply (drule_tac [2] linorder_not_less [THEN iffD1, THEN order_le_imp_less_or_eq], auto) |
710 |
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
|
711 |
prefer 2 apply (blast dest: lemma_additivity3) |
15219 | 712 |
apply (frule (2) lemma_additivity4_psize_eq) |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
713 |
apply (rule partition [THEN iffD2]) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
714 |
apply (frule partition [THEN iffD1]) |
15219 | 715 |
apply safe |
716 |
apply (auto simp add: partition_lt_gen) |
|
15197 | 717 |
apply (drule (1) partition_lt_cancel, arith) |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
718 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
719 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
720 |
lemma fine_left1: |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
721 |
"[| 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
|
722 |
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
|
723 |
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
|
724 |
else min (ga x) ((x - D n)/ 2)) (D, p) |] |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
725 |
==> fine g |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
726 |
(%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
|
727 |
%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
|
728 |
apply (auto simp add: fine_def tpart_def gauge_def) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
729 |
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
|
730 |
apply (drule_tac [!] x = na in spec, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
731 |
apply (drule_tac [!] x = na in spec, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
732 |
apply (auto dest: lemma_additivity3a simp add: split_if_asm) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
733 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
734 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
735 |
lemma tpart_right1: |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
736 |
"[| a \<le> D n; tpart (a, b) (D, p) |] |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
737 |
==> 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
|
738 |
apply (simp add: tpart_def partition_def, safe) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
739 |
apply (rule_tac x = "N - n" in exI, auto) |
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 fine_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); gauge (%x. D n \<le> x & x \<le> b) ga; |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
744 |
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
|
745 |
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
|
746 |
else min (ga x) ((x - D n)/ 2)) (D, p) |] |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
747 |
==> fine ga (%x. D(x + n),%x. p(x + n))" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
748 |
apply (auto simp add: fine_def gauge_def) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
749 |
apply (drule_tac x = "na + n" in spec) |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19765
diff
changeset
|
750 |
apply (frule_tac n = n in tpart_partition [THEN better_lemma_psize_right_eq], auto) |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
751 |
apply (simp add: tpart_def, safe) |
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
15093
diff
changeset
|
752 |
apply (subgoal_tac "D n \<le> p (na + n)") |
15219 | 753 |
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
|
754 |
apply safe |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
755 |
apply (simp split: split_if_asm, simp) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
756 |
apply (drule less_le_trans, assumption) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
757 |
apply (rotate_tac 5) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
758 |
apply (drule_tac x = "na + n" in spec, safe) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
759 |
apply (rule_tac y="D (na + n)" in order_trans) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
760 |
apply (case_tac "na = 0", auto) |
23315 | 761 |
apply (erule partition_lt_gen [THEN order_less_imp_le]) |
762 |
apply arith |
|
763 |
apply arith |
|
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
764 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
765 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
766 |
lemma rsum_add: "rsum (D, p) (%x. f x + g x) = rsum (D, p) f + rsum(D, p) g" |
15536 | 767 |
by (simp add: rsum_def setsum_addf left_distrib) |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
768 |
|
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
15093
diff
changeset
|
769 |
text{* Bartle/Sherbert: Theorem 10.1.5 p. 278 *} |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
770 |
lemma Integral_add_fun: |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
771 |
"[| 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
|
772 |
==> Integral(a,b) (%x. f x + g x) (k1 + k2)" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
773 |
apply (simp add: Integral_def, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
774 |
apply ((drule_tac x = "e/2" in spec)+) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
775 |
apply auto |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
776 |
apply (drule gauge_min, assumption) |
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
15093
diff
changeset
|
777 |
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
|
778 |
apply auto |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
779 |
apply (drule fine_min) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
780 |
apply ((drule spec)+, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
781 |
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
|
782 |
apply (auto simp only: rsum_add left_distrib [symmetric] |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19765
diff
changeset
|
783 |
mult_2_right [symmetric] real_mult_less_iff1) |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
784 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
785 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
786 |
lemma partition_lt_gen2: |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
787 |
"[| 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
|
788 |
by (auto simp add: partition) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
789 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
790 |
lemma lemma_Integral_le: |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
791 |
"[| \<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
|
792 |
tpart(a,b) (D,p) |
15360 | 793 |
|] ==> \<forall>n \<le> psize D. f (p n) \<le> g (p n)" |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
794 |
apply (simp add: tpart_def) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
795 |
apply (auto, frule partition [THEN iffD1], auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
796 |
apply (drule_tac x = "p n" in spec, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
797 |
apply (case_tac "n = 0", simp) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
798 |
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
|
799 |
apply (drule le_imp_less_or_eq, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
800 |
apply (drule_tac [2] x = "psize D" in spec, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
801 |
apply (drule_tac r = "Suc n" in partition_ub) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
802 |
apply (drule_tac x = n in spec, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
803 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
804 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
805 |
lemma lemma_Integral_rsum_le: |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
806 |
"[| \<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
|
807 |
tpart(a,b) (D,p) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
808 |
|] ==> rsum(D,p) f \<le> rsum(D,p) g" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
809 |
apply (simp add: rsum_def) |
15539 | 810 |
apply (auto intro!: setsum_mono dest: tpart_partition [THEN partition_lt_gen2] |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
811 |
dest!: lemma_Integral_le) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
812 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
813 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
814 |
lemma Integral_le: |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
815 |
"[| a \<le> b; |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
816 |
\<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
|
817 |
Integral(a,b) f k1; Integral(a,b) g k2 |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
818 |
|] ==> k1 \<le> k2" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
819 |
apply (simp add: Integral_def) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
820 |
apply (rotate_tac 2) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
821 |
apply (drule_tac x = "\<bar>k1 - k2\<bar> /2" in spec) |
15221 | 822 |
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
|
823 |
apply (drule gauge_min, assumption) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
824 |
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
|
825 |
in partition_exists, assumption, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
826 |
apply (drule fine_min) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
827 |
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
|
828 |
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
|
829 |
apply (frule lemma_Integral_rsum_le, assumption) |
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
15093
diff
changeset
|
830 |
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
|
831 |
apply arith |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
832 |
apply (drule add_strict_mono, assumption) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
833 |
apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric] |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19765
diff
changeset
|
834 |
real_mult_less_iff1) |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
835 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
836 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
837 |
lemma Integral_imp_Cauchy: |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
838 |
"(\<exists>k. Integral(a,b) f k) ==> |
15360 | 839 |
(\<forall>e > 0. \<exists>g. gauge (%x. a \<le> x & x \<le> b) g & |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
840 |
(\<forall>D1 D2 p1 p2. |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
841 |
tpart(a,b) (D1, p1) & fine g (D1,p1) & |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
842 |
tpart(a,b) (D2, p2) & fine g (D2,p2) --> |
15360 | 843 |
\<bar>rsum(D1,p1) f - rsum(D2,p2) f\<bar> < e))" |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
844 |
apply (simp add: Integral_def, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
845 |
apply (drule_tac x = "e/2" in spec, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
846 |
apply (rule exI, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
847 |
apply (frule_tac x = D1 in spec) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
848 |
apply (frule_tac x = D2 in spec) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
849 |
apply ((drule spec)+, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
850 |
apply (erule_tac V = "0 < e" in thin_rl) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
851 |
apply (drule add_strict_mono, assumption) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
852 |
apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric] |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19765
diff
changeset
|
853 |
real_mult_less_iff1) |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
854 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
855 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
856 |
lemma Cauchy_iff2: |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
857 |
"Cauchy X = |
20563 | 858 |
(\<forall>j. (\<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. \<bar>X m - X n\<bar> < inverse(real (Suc j))))" |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
859 |
apply (simp add: Cauchy_def, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
860 |
apply (drule reals_Archimedean, safe) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
861 |
apply (drule_tac x = n in spec, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
862 |
apply (rule_tac x = M in exI, auto) |
15360 | 863 |
apply (drule_tac x = m in spec, simp) |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
864 |
apply (drule_tac x = na in spec, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
865 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
866 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
867 |
lemma partition_exists2: |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
868 |
"[| 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
|
869 |
==> \<forall>n. \<exists>D p. tpart (a, b) (D, p) & fine (fa n) (D, p)" |
15219 | 870 |
by (blast dest: partition_exists) |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
871 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
872 |
lemma monotonic_anti_derivative: |
20792 | 873 |
fixes f g :: "real => real" shows |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
874 |
"[| 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
|
875 |
\<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
|
876 |
==> f b - f a \<le> g b - g a" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
877 |
apply (rule Integral_le, assumption) |
15219 | 878 |
apply (auto intro: FTC1) |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
879 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
880 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset
|
881 |
end |