--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Sat Feb 26 20:40:45 2011 +0100
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Mon Feb 28 22:10:57 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
--- a/src/HOL/Multivariate_Analysis/Integration.thy Sat Feb 26 20:40:45 2011 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Mon Feb 28 22:10:57 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
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Sat Feb 26 20:40:45 2011 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Feb 28 22:10:57 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"]