src/HOL/Multivariate_Analysis/Integration.thy

     Translation from HOL light: Robert Himmelmann, TU Muenchen *)
 
 theory Integration
 imports
   Derivative
-  "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
   "~~/src/HOL/Library/Indicator_Function"
 begin
 
 declare [[smt_certificates="Integration.certs"]]
 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
   scaleR_zero_right scaleR_minus_right scaleR_right_diff_distrib scaleR_eq_0_iff

 subsection {* Specialization of additivity to one dimension. *}
 
 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"
     from this(2-) have "{a..b} \<inter> {x. x \<le> c} = {a..c}" "{a..b} \<inter> {x. x \<ge> c} = {c..b}" by auto
     thus "opp (f {a..c}) (f {c..b}) = f {a..b}" unfolding as(1)[rule_format,of a b "c"] by auto

 lemma henstock_lemma_part1: fixes f::"'n::ordered_euclidean_space \<Rightarrow> 'a::banach"
   assumes "f integrable_on {a..b}" "0 < e" "gauge d"
   "(\<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
   from partial_division_extend_interval[OF this] guess q . note q=this and q' = division_ofD[OF this(2)]
   def r \<equiv> "q - snd ` p" have "snd ` p \<inter> r = {}" unfolding r_def by auto