# HG changeset patch
# User huffman
# Date 1243314899 25200
# Node ID d54dc8956d486f67459e29c22f47a171e74509fc
# Parent  5155117f9d668740cc4b6742f44e8d8cc093b524
use interval sets with gauge predicate

diff -r 5155117f9d66 -r d54dc8956d48 src/HOL/Integration.thy
--- 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))"
-*)
-
-
 lemma strad1:
        "\<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 @@
 
 lemma lemma_straddle:
   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)