--- 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