removed dependency on Dense_Linear_Order
authorboehmes
Mon Feb 28 22:10:57 2011 +0100 (2011-02-28)
changeset 41863e5104b436ea1
parent 41855 c3b6e69da386
child 41864 41b9acc0114d
removed dependency on Dense_Linear_Order
src/HOL/Multivariate_Analysis/Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
     1.1 --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sat Feb 26 20:40:45 2011 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Mon Feb 28 22:10:57 2011 +0100
     1.3 @@ -7,7 +7,6 @@
     1.4  theory Euclidean_Space
     1.5  imports
     1.6    Complex_Main
     1.7 -  "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
     1.8    "~~/src/HOL/Library/Infinite_Set"
     1.9    "~~/src/HOL/Library/Inner_Product"
    1.10    L2_Norm
    1.11 @@ -48,7 +47,8 @@
    1.12      by (metis linorder_linear not_le)
    1.13      have th1: "\<And>z x e d :: real. z <= x + e \<Longrightarrow> e < d ==> z < x \<or> abs(z - x) < d" by arith
    1.14      have th2: "\<And>e x:: real. 0 < e ==> ~(x + e <= x)" by arith
    1.15 -    have th3: "\<And>d::real. d > 0 \<Longrightarrow> \<exists>e > 0. e < d" by dlo
    1.16 +    have "\<And>d::real. 0 < d \<Longrightarrow> 0 < d/2 \<and> d/2 < d" by simp
    1.17 +    then have th3: "\<And>d::real. d > 0 \<Longrightarrow> \<exists>e > 0. e < d" by blast
    1.18      {assume le2: "f l \<in> e2"
    1.19        from le2 fa fb e12 alb have la: "l \<noteq> a" by metis
    1.20        hence lap: "l - a > 0" using alb by arith
    1.21 @@ -56,8 +56,10 @@
    1.22          e: "e > 0" "\<forall>y. dist y (f l) < e \<longrightarrow> y \<in> e2" by metis
    1.23        from dst[OF alb e(1)] obtain d where
    1.24          d: "d > 0" "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> dist (f y) (f l) < e" by metis
    1.25 -      have "\<exists>d'. d' < d \<and> d' >0 \<and> l - d' > a" using lap d(1)
    1.26 -        apply ferrack by arith
    1.27 +      let ?d' = "min (d/2) ((l - a)/2)"
    1.28 +      have "?d' < d \<and> 0 < ?d' \<and> ?d' < l - a" using lap d(1)
    1.29 +        by (simp add: min_max.less_infI2)
    1.30 +      then have "\<exists>d'. d' < d \<and> d' >0 \<and> l - d' > a" by auto
    1.31        then obtain d' where d': "d' > 0" "d' < d" "l - d' > a" by metis
    1.32        from d e have th0: "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> f y \<in> e2" by metis
    1.33        from th0[rule_format, of "l - d'"] d' have "f (l - d') \<in> e2" by auto
    1.34 @@ -72,7 +74,8 @@
    1.35          e: "e > 0" "\<forall>y. dist y (f l) < e \<longrightarrow> y \<in> e1" by metis
    1.36        from dst[OF alb e(1)] obtain d where
    1.37          d: "d > 0" "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> dist (f y) (f l) < e" by metis
    1.38 -      have "\<exists>d'. d' < d \<and> d' >0" using d(1) by dlo
    1.39 +      have "\<And>d::real. 0 < d \<Longrightarrow> d/2 < d \<and> 0 < d/2" by simp
    1.40 +      then have "\<exists>d'. d' < d \<and> d' >0" using d(1) by blast
    1.41        then obtain d' where d': "d' > 0" "d' < d" by metis
    1.42        from d e have th0: "\<forall>y. \<bar>y - l\<bar> < d \<longrightarrow> f y \<in> e1" by auto
    1.43        hence "\<forall>y. l \<le> y \<and> y \<le> l + d' \<longrightarrow> f y \<in> e1" using d' by auto
    1.44 @@ -1995,7 +1998,7 @@
    1.45          by (simp add: mult_less_0_iff)
    1.46        with B[rule_format, of "(\<chi>\<chi> i. 1)::'a"] norm_ge_zero[of "f ((\<chi>\<chi> i. 1)::'a)"] have False by simp
    1.47      }
    1.48 -    then have Bp: "B \<ge> 0" by ferrack
    1.49 +    then have Bp: "B \<ge> 0" by (metis not_leE)
    1.50      {fix x::"'a"
    1.51        have "norm (f x) \<le> ?K *  norm x"
    1.52        using B[rule_format, of x] norm_ge_zero[of x] norm_ge_zero[of "f x"] Bp
     2.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Sat Feb 26 20:40:45 2011 +0100
     2.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Mon Feb 28 22:10:57 2011 +0100
     2.3 @@ -6,7 +6,6 @@
     2.4  theory Integration
     2.5  imports
     2.6    Derivative
     2.7 -  "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
     2.8    "~~/src/HOL/Library/Indicator_Function"
     2.9  begin
    2.10  
    2.11 @@ -14,8 +13,6 @@
    2.12  declare [[smt_fixed=true]]
    2.13  declare [[smt_oracle=false]]
    2.14  
    2.15 -setup {* Arith_Data.add_tactic "Ferrante-Rackoff" (K FerranteRackoff.dlo_tac) *}
    2.16 -
    2.17  (*declare not_less[simp] not_le[simp]*)
    2.18  
    2.19  lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib
    2.20 @@ -2879,7 +2876,7 @@
    2.21  lemma operative_1_lt: assumes "monoidal opp"
    2.22    shows "operative opp f \<longleftrightarrow> ((\<forall>a b. b \<le> a \<longrightarrow> f {a..b::real} = neutral opp) \<and>
    2.23                  (\<forall>a b c. a < c \<and> c < b \<longrightarrow> opp (f{a..c})(f{c..b}) = f {a..b}))"
    2.24 -  unfolding operative_def content_eq_0 DIM_real less_one dnf_simps(39,41) Eucl_real_simps
    2.25 +  unfolding operative_def content_eq_0 DIM_real less_one simp_thms(39,41) Eucl_real_simps
    2.26      (* The dnf_simps simplify "\<exists> x. x= _ \<and> _" and "\<forall>k. k = _ \<longrightarrow> _" *)
    2.27  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}))
    2.28      (f ({a..b} \<inter> {x. c \<le> x}))" "a < c" "c < b"
    2.29 @@ -4354,7 +4351,7 @@
    2.30    "(\<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)"
    2.31    and p:"p tagged_partial_division_of {a..b}" "d fine p"
    2.32    shows "norm(setsum (\<lambda>(x,k). content k *\<^sub>R f x - integral k f) p) \<le> e" (is "?x \<le> e")
    2.33 -proof-  { presume "\<And>k. 0<k \<Longrightarrow> ?x \<le> e + k" thus ?thesis by arith }
    2.34 +proof-  { presume "\<And>k. 0<k \<Longrightarrow> ?x \<le> e + k" thus ?thesis by (blast intro: field_le_epsilon) }
    2.35    fix k::real assume k:"k>0" note p' = tagged_partial_division_ofD[OF p(1)]
    2.36    have "\<Union>snd ` p \<subseteq> {a..b}" using p'(3) by fastsimp
    2.37    note partial_division_of_tagged_division[OF p(1)] this
     3.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sat Feb 26 20:40:45 2011 +0100
     3.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Feb 28 22:10:57 2011 +0100
     3.3 @@ -589,7 +589,7 @@
     3.4    fixes a :: "'a::metric_space"
     3.5    assumes fS: "finite S" shows  "\<exists>d>0. \<forall>x\<in>S. x \<noteq> a \<longrightarrow> d <= dist a x"
     3.6  proof(induct rule: finite_induct[OF fS])
     3.7 -  case 1 thus ?case apply auto by ferrack
     3.8 +  case 1 thus ?case by (auto intro: zero_less_one)
     3.9  next
    3.10    case (2 x F)
    3.11    from 2 obtain d where d: "d >0" "\<forall>x\<in>F. x\<noteq>a \<longrightarrow> d \<le> dist a x" by blast
    3.12 @@ -5767,7 +5767,10 @@
    3.13      hence "\<exists>N. \<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (z m) (z n) < e"
    3.14      proof(cases "d = 0")
    3.15        case True
    3.16 -      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`])
    3.17 +      have *: "\<And>x. ((1 - c) * x \<le> 0) = (x \<le> 0)" using `1 - c > 0`
    3.18 +        by (metis mult_zero_left real_mult_commute real_mult_le_cancel_iff1)
    3.19 +      from True have "\<And>n. z n = z0" using cf_z2[of 0] and c unfolding z_def
    3.20 +        by (simp add: *)
    3.21        thus ?thesis using `e>0` by auto
    3.22      next
    3.23        case False hence "d>0" unfolding d_def using zero_le_dist[of "z 0" "z 1"]