# HG changeset patch
# User boehmes
# Date 1298927529 -3600
# Node ID 41b9acc0114dd31bc6d856fdf6948c4f1d25159c
# Parent  e5104b436ea145a19b6e8644eb4f81488eb29ad6# Parent  a38536bf273629abc0ae79cc0474e0fb6ff02249
merged

diff -r a38536bf2736 -r 41b9acc0114d src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Mon Feb 28 19:06:24 2011 +0100
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Mon Feb 28 22:12:09 2011 +0100
@@ -7,7 +7,6 @@
 theory Euclidean_Space
 imports
   Complex_Main
-  "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
   "~~/src/HOL/Library/Infinite_Set"
   "~~/src/HOL/Library/Inner_Product"
   L2_Norm
@@ -48,7 +47,8 @@
     by (metis linorder_linear not_le)
     have th1: "\<And>z x e d :: real. z <= x + e \<Longrightarrow> e < d ==> z < x \<or> abs(z - x) < d" by arith
     have th2: "\<And>e x:: real. 0 < e ==> ~(x + e <= x)" by arith
-    have th3: "\<And>d::real. d > 0 \<Longrightarrow> \<exists>e > 0. e < d" by dlo
+    have "\<And>d::real. 0 < d \<Longrightarrow> 0 < d/2 \<and> d/2 < d" by simp
+    then have th3: "\<And>d::real. d > 0 \<Longrightarrow> \<exists>e > 0. e < d" by blast
     {assume le2: "f l \<in> e2"
       from le2 fa fb e12 alb have la: "l \<noteq> a" by metis
       hence lap: "l - a > 0" using alb by arith
@@ -56,8 +56,10 @@
         e: "e > 0" "\<forall>y. dist y (f l) < e \<longrightarrow> y \<in> e2" by metis
       from dst[OF alb e(1)] obtain d where
         d: "d > 0" "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> dist (f y) (f l) < e" by metis
-      have "\<exists>d'. d' < d \<and> d' >0 \<and> l - d' > a" using lap d(1)
-        apply ferrack by arith
+      let ?d' = "min (d/2) ((l - a)/2)"
+      have "?d' < d \<and> 0 < ?d' \<and> ?d' < l - a" using lap d(1)
+        by (simp add: min_max.less_infI2)
+      then have "\<exists>d'. d' < d \<and> d' >0 \<and> l - d' > a" by auto
       then obtain d' where d': "d' > 0" "d' < d" "l - d' > a" by metis
       from d e have th0: "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> f y \<in> e2" by metis
       from th0[rule_format, of "l - d'"] d' have "f (l - d') \<in> e2" by auto
@@ -72,7 +74,8 @@
         e: "e > 0" "\<forall>y. dist y (f l) < e \<longrightarrow> y \<in> e1" by metis
       from dst[OF alb e(1)] obtain d where
         d: "d > 0" "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> dist (f y) (f l) < e" by metis
-      have "\<exists>d'. d' < d \<and> d' >0" using d(1) by dlo
+      have "\<And>d::real. 0 < d \<Longrightarrow> d/2 < d \<and> 0 < d/2" by simp
+      then have "\<exists>d'. d' < d \<and> d' >0" using d(1) by blast
       then obtain d' where d': "d' > 0" "d' < d" by metis
       from d e have th0: "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> f y \<in> e1" by auto
       hence "\<forall>y. l \<le> y \<and> y \<le> l + d' \<longrightarrow> f y \<in> e1" using d' by auto
@@ -1995,7 +1998,7 @@
         by (simp add: mult_less_0_iff)
       with B[rule_format, of "(\<chi>\<chi> i. 1)::'a"] norm_ge_zero[of "f ((\<chi>\<chi> i. 1)::'a)"] have False by simp
     }
-    then have Bp: "B \<ge> 0" by ferrack
+    then have Bp: "B \<ge> 0" by (metis not_leE)
     {fix x::"'a"
       have "norm (f x) \<le> ?K *  norm x"
       using B[rule_format, of x] norm_ge_zero[of x] norm_ge_zero[of "f x"] Bp
diff -r a38536bf2736 -r 41b9acc0114d src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Mon Feb 28 19:06:24 2011 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Mon Feb 28 22:12:09 2011 +0100
@@ -6,7 +6,6 @@
 theory Integration
 imports
   Derivative
-  "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
   "~~/src/HOL/Library/Indicator_Function"
 begin
 
@@ -14,8 +13,6 @@
 declare [[smt_fixed=true]]
 declare [[smt_oracle=false]]
 
-setup {* Arith_Data.add_tactic "Ferrante-Rackoff" (K FerranteRackoff.dlo_tac) *}
-
 (*declare not_less[simp] not_le[simp]*)
 
 lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib
@@ -2879,7 +2876,7 @@
 lemma operative_1_lt: assumes "monoidal opp"
   shows "operative opp f \<longleftrightarrow> ((\<forall>a b. b \<le> a \<longrightarrow> f {a..b::real} = neutral opp) \<and>
                 (\<forall>a b c. a < c \<and> c < b \<longrightarrow> opp (f{a..c})(f{c..b}) = f {a..b}))"
-  unfolding operative_def content_eq_0 DIM_real less_one dnf_simps(39,41) Eucl_real_simps
+  unfolding operative_def content_eq_0 DIM_real less_one simp_thms(39,41) Eucl_real_simps
     (* The dnf_simps simplify "\<exists> x. x= _ \<and> _" and "\<forall>k. k = _ \<longrightarrow> _" *)
 proof safe fix a b c::"real" assume as:"\<forall>a b c. f {a..b} = opp (f ({a..b} \<inter> {x. x \<le> c}))
     (f ({a..b} \<inter> {x. c \<le> x}))" "a < c" "c < b"
@@ -4354,7 +4351,7 @@
   "(\<forall>p. p tagged_division_of {a..b} \<and> d fine p \<longrightarrow> norm (setsum (\<lambda>(x,k). content k *\<^sub>R f x) p - integral({a..b}) f) < e)"
   and p:"p tagged_partial_division_of {a..b}" "d fine p"
   shows "norm(setsum (\<lambda>(x,k). content k *\<^sub>R f x - integral k f) p) \<le> e" (is "?x \<le> e")
-proof-  { presume "\<And>k. 0<k \<Longrightarrow> ?x \<le> e + k" thus ?thesis by arith }
+proof-  { presume "\<And>k. 0<k \<Longrightarrow> ?x \<le> e + k" thus ?thesis by (blast intro: field_le_epsilon) }
   fix k::real assume k:"k>0" note p' = tagged_partial_division_ofD[OF p(1)]
   have "\<Union>snd ` p \<subseteq> {a..b}" using p'(3) by fastsimp
   note partial_division_of_tagged_division[OF p(1)] this
diff -r a38536bf2736 -r 41b9acc0114d src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Feb 28 19:06:24 2011 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Feb 28 22:12:09 2011 +0100
@@ -589,7 +589,7 @@
   fixes a :: "'a::metric_space"
   assumes fS: "finite S" shows  "\<exists>d>0. \<forall>x\<in>S. x \<noteq> a \<longrightarrow> d <= dist a x"
 proof(induct rule: finite_induct[OF fS])
-  case 1 thus ?case apply auto by ferrack
+  case 1 thus ?case by (auto intro: zero_less_one)
 next
   case (2 x F)
   from 2 obtain d where d: "d >0" "\<forall>x\<in>F. x\<noteq>a \<longrightarrow> d \<le> dist a x" by blast
@@ -5767,7 +5767,10 @@
     hence "\<exists>N. \<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (z m) (z n) < e"
     proof(cases "d = 0")
       case True
-      hence "\<And>n. z n = z0" using cf_z2[of 0] and c unfolding z_def by (auto simp add: pos_prod_le[OF `1 - c > 0`])
+      have *: "\<And>x. ((1 - c) * x \<le> 0) = (x \<le> 0)" using `1 - c > 0`
+        by (metis mult_zero_left real_mult_commute real_mult_le_cancel_iff1)
+      from True have "\<And>n. z n = z0" using cf_z2[of 0] and c unfolding z_def
+        by (simp add: *)
       thus ?thesis using `e>0` by auto
     next
       case False hence "d>0" unfolding d_def using zero_le_dist[of "z 0" "z 1"]