author huffman Mon, 25 May 2009 22:14:59 -0700 changeset 31253 d54dc8956d48 parent 31252 5155117f9d66 child 31254 03a35fbc9dc6
use interval sets with gauge predicate
 src/HOL/Integration.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Integration.thy	Mon May 25 21:55:07 2009 -0700
+++ b/src/HOL/Integration.thy	Mon May 25 22:14:59 2009 -0700
@@ -32,8 +32,8 @@
--{*Gauges and gauge-fine divisions*}

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

definition
fine :: "[real => real, ((nat => real)*(nat => real))] => bool" where
@@ -50,13 +50,13 @@
definition
Integral :: "[(real*real),real=>real,real] => bool" where
[code del]: "Integral = (%(a,b) f k. \<forall>e > 0.
-                               (\<exists>g. gauge(%x. a \<le> x & x \<le> b) g &
+                               (\<exists>g. gauge {a..b} g &
(\<forall>D p. tpart(a,b) (D,p) & fine(g)(D,p) -->
\<bar>rsum(D,p) f - k\<bar> < e)))"

lemma Integral_def2:
-  "Integral = (%(a,b) f k. \<forall>e>0. (\<exists>g. gauge(%x. a \<le> x & x \<le> b) g &
+  "Integral = (%(a,b) f k. \<forall>e>0. (\<exists>g. gauge {a..b} g &
(\<forall>D p. tpart(a,b) (D,p) & fine(g)(D,p) -->
\<bar>rsum(D,p) f - k\<bar> \<le> e)))"
unfolding Integral_def
@@ -288,7 +288,7 @@
text{*We can always find a division that is fine wrt any gauge*}

lemma partition_exists:
-     "[| a \<le> b; gauge(%x. a \<le> x & x \<le> b) g |]
+     "[| a \<le> b; gauge {a..b} g |]
==> \<exists>D p. tpart(a,b) (D,p) & fine g (D,p)"
apply (cut_tac P = "%(u,v). a \<le> u & v \<le> b -->
(\<exists>D p. tpart (u,v) (D,p) & fine (g) (D,p))"
@@ -381,23 +381,13 @@

text{*"Straddle Lemma" : Swartz and Thompson: AMM 95(7) 1988 *}

-lemma choiceP: "\<forall>x. P(x) --> (\<exists>y. Q x y) ==> \<exists>f. (\<forall>x. P(x) --> Q x (f x))"
-by (insert bchoice [of "Collect P" Q], simp)
-
-(*UNUSED
-lemma choice2: "\<forall>x. (\<exists>y. R(y) & (\<exists>z. Q x y z)) ==>
-      \<exists>f fa. (\<forall>x. R(f x) & Q x (f x) (fa x))"
-*)
-
-
"\<lbrakk>\<forall>z::real. z \<noteq> x \<and> \<bar>z - x\<bar> < s \<longrightarrow>
\<bar>(f z - f x) / (z - x) - f' x\<bar> < e/2;
0 < s; 0 < e; a \<le> x; x \<le> b\<rbrakk>
\<Longrightarrow> \<forall>z. \<bar>z - x\<bar> < s -->\<bar>f z - f x - f' x * (z - x)\<bar> \<le> e/2 * \<bar>z - x\<bar>"
apply clarify
-apply (case_tac "0 < \<bar>z - x\<bar>")
- prefer 2 apply (simp add: zero_less_abs_iff)
+apply (case_tac "z = x", simp)
apply (drule_tac x = z in spec)
apply (rule_tac z1 = "\<bar>inverse (z - x)\<bar>"
in real_mult_le_cancel_iff2 [THEN iffD1])
@@ -415,14 +405,14 @@

assumes f': "\<forall>x. a \<le> x & x \<le> b --> DERIV f x :> f'(x)" and "0 < e"
-  shows "\<exists>g. gauge(%x. a \<le> x & x \<le> b) g &
+  shows "\<exists>g. gauge {a..b} g &
(\<forall>x u v. a \<le> u & u \<le> x & x \<le> v & v \<le> b & (v - u) < g(x)
--> \<bar>(f(v) - f(u)) - (f'(x) * (v - u))\<bar> \<le> e * (v - u))"
proof -
-  have "\<forall>x. a \<le> x & x \<le> b -->
+  have "\<forall>x\<in>{a..b}.
(\<exists>d > 0. \<forall>u v. u \<le> x & x \<le> v & (v - u) < d -->
\<bar>(f(v) - f(u)) - (f'(x) * (v - u))\<bar> \<le> e * (v - u))"
-  proof (clarify)
+  proof (clarsimp)
fix x :: real assume "a \<le> x" and "x \<le> b"
with f' have "DERIV f x :> f'(x)" by simp
then have "\<forall>r>0. \<exists>s>0. \<forall>z. z \<noteq> x \<and> \<bar>z - x\<bar> < s \<longrightarrow> \<bar>(f z - f x) / (z - x) - f' x\<bar> < r"
@@ -455,7 +445,7 @@
qed
qed
thus ?thesis
-    by (simp add: gauge_def) (drule choiceP, auto)
+    by (simp add: gauge_def) (drule bchoice, auto)
qed

lemma FTC1: "[|a \<le> b; \<forall>x. a \<le> x & x \<le> b --> DERIV f x :> f'(x) |]
@@ -724,7 +714,7 @@
done

lemma fine_left1:
-     "[| a \<le> D n; tpart (a, b) (D, p); gauge (%x. a \<le> x & x \<le> D n) g;
+     "[| a \<le> D n; tpart (a, b) (D, p); gauge {a..D n} g;
fine (%x. if x < D n then min (g x) ((D n - x)/ 2)
else if x = D n then min (g (D n)) (ga (D n))
else min (ga x) ((x - D n)/ 2)) (D, p) |]
@@ -746,7 +736,7 @@
done

lemma fine_right1:
-     "[| a \<le> D n; tpart (a, b) (D, p); gauge (%x. D n \<le> x & x \<le> b) ga;
+     "[| a \<le> D n; tpart (a, b) (D, p); gauge {D n..b} ga;
fine (%x. if x < D n then min (g x) ((D n - x)/ 2)
else if x = D n then min (g (D n)) (ga (D n))
else min (ga x) ((x - D n)/ 2)) (D, p) |]
@@ -842,7 +832,7 @@

lemma Integral_imp_Cauchy:
"(\<exists>k. Integral(a,b) f k) ==>
-      (\<forall>e > 0. \<exists>g. gauge (%x. a \<le> x & x \<le> b) g &
+      (\<forall>e > 0. \<exists>g. gauge {a..b} g &
(\<forall>D1 D2 p1 p2.
tpart(a,b) (D1, p1) & fine g (D1,p1) &
tpart(a,b) (D2, p2) & fine g (D2,p2) -->
@@ -871,7 +861,7 @@
done

lemma partition_exists2:
-     "[| a \<le> b; \<forall>n. gauge (%x. a \<le> x & x \<le> b) (fa n) |]
+     "[| a \<le> b; \<forall>n. gauge {a..b} (fa n) |]
==> \<forall>n. \<exists>D p. tpart (a, b) (D, p) & fine (fa n) (D, p)"
by (blast dest: partition_exists)
```