src/HOL/Multivariate_Analysis/Integration.thy

   by auto
 
 lemma has_integral_vec1: assumes "(f has_integral k) {a..b}"
   shows "((\<lambda>x. vec1 (f x)) has_integral (vec1 k)) {a..b}"
 proof- have *:"\<And>p. (\<Sum>(x, k)\<in>p. content k *\<^sub>R vec1 (f x)) - vec1 k = vec1 ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - k)"
-    unfolding vec_sub Cart_eq by(auto simp add:vec1_dest_vec1_simps split_beta)
+    unfolding vec_sub Cart_eq by(auto simp add: split_beta)
   show ?thesis using assms unfolding has_integral apply safe
     apply(erule_tac x=e in allE,safe) apply(rule_tac x=d in exI,safe)
     apply(erule_tac x=p in allE,safe) unfolding * norm_vector_1 by auto qed
 
 lemma setsum_content_null:

   shows "\<forall>x\<in>s. f x = g x \<Longrightarrow> f integrable_on s \<Longrightarrow> g integrable_on s"
   unfolding integrable_on_def using has_integral_eq[of s f g] by auto
 
 lemma has_integral_eq_eq:
   shows "\<forall>x\<in>s. f x = g x \<Longrightarrow> ((f has_integral k) s \<longleftrightarrow> (g has_integral k) s)"
-  using has_integral_eq[of s f g] has_integral_eq[of s g f] by auto 
+  using has_integral_eq[of s f g] has_integral_eq[of s g f] by rule auto
 
 lemma has_integral_null[dest]:
   assumes "content({a..b}) = 0" shows  "(f has_integral 0) ({a..b})"
   unfolding has_integral apply(rule,rule,rule_tac x="\<lambda>x. ball x 1" in exI,rule) defer
 proof(rule,rule,erule conjE) fix e::real assume e:"e>0" thus "gauge (\<lambda>x. ball x 1)" by auto

   assumes "p1 tagged_division_of ({a..b} \<inter> {x::real^'n. x$k \<le> (c::real)})"  "p2 tagged_division_of ({a..b} \<inter> {x. x$k \<ge> c})"
   shows "(p1 \<union> p2) tagged_division_of ({a..b})"
 proof- have *:"{a..b} = ({a..b} \<inter> {x. x$k \<le> c}) \<union> ({a..b} \<inter> {x. x$k \<ge> c})" by auto
   show ?thesis apply(subst *) apply(rule tagged_division_union[OF assms])
     unfolding interval_split interior_closed_interval
-    by(auto simp add: vector_less_def Cart_lambda_beta elim!:allE[where x=k]) qed
+    by(auto simp add: vector_less_def elim!:allE[where x=k]) qed
 
 lemma has_integral_separate_sides: fixes f::"real^'m \<Rightarrow> 'a::real_normed_vector"
   assumes "(f has_integral i) ({a..b})" "e>0"
   obtains d where "gauge d" "(\<forall>p1 p2. p1 tagged_division_of ({a..b} \<inter> {x. x$k \<le> c}) \<and> d fine p1 \<and>
                                 p2 tagged_division_of ({a..b} \<inter> {x. x$k \<ge> c}) \<and> d fine p2

   unfolding operative_def apply(rule property_empty_interval) by auto
 
 subsection {* Using additivity of lifted function to encode definedness. *}
 
 lemma forall_option: "(\<forall>x. P x) \<longleftrightarrow> P None \<and> (\<forall>x. P(Some x))"
-  by (metis map_of.simps option.nchotomy)
+  by (metis option.nchotomy)
 
 lemma exists_option:
  "(\<exists>x. P x) \<longleftrightarrow> P None \<or> (\<exists>x. P(Some x))" 
-  by (metis map_of.simps option.nchotomy)
+  by (metis option.nchotomy)
 
 fun lifted where 
   "lifted (opp::'a\<Rightarrow>'a\<Rightarrow>'b) (Some x) (Some y) = Some(opp x y)" |
   "lifted opp None _ = (None::'b option)" |
   "lifted opp _ None = None"

   apply(rule some_equality) defer apply(erule_tac x=0 in allE) by auto
 
 lemma operative_content[intro]: "operative (op +) content"
   unfolding operative_def content_split[THEN sym] neutral_add by auto
 
-lemma neutral_monoid[simp]: "neutral ((op +)::('a::comm_monoid_add) \<Rightarrow> 'a \<Rightarrow> 'a) = 0"
-  unfolding neutral_def apply(rule some_equality) defer
-  apply(erule_tac x=0 in allE) by auto
+lemma neutral_monoid: "neutral ((op +)::('a::comm_monoid_add) \<Rightarrow> 'a \<Rightarrow> 'a) = 0"
+  by (rule neutral_add) (* FIXME: duplicate *)
 
 lemma monoidal_monoid[intro]:
   shows "monoidal ((op +)::('a::comm_monoid_add) \<Rightarrow> 'a \<Rightarrow> 'a)"
   unfolding monoidal_def neutral_monoid by(auto simp add: group_simps) 
 

     unfolding l interval_bounds[OF uv(1)] using uv[rule_format,of k] ab by auto
   have "\<exists>x. x \<in> ?D - ?D1" using assms(2-) apply-apply(erule disjE)
     apply(rule_tac x="(k,(interval_lowerbound l)$k)" in exI) defer
     apply(rule_tac x="(k,(interval_upperbound l)$k)" in exI)
     unfolding division_points_def unfolding interval_bounds[OF ab]
-    apply (auto simp add:interval_bounds) unfolding * by auto
+    apply auto unfolding * by auto
   thus "?D1 \<subset> ?D" apply-apply(rule,rule division_points_subset[OF assms(1-4)]) by auto
 
   have *:"interval_lowerbound ({a..b} \<inter> {x. x $ k \<ge> interval_lowerbound l $ k}) $ k = interval_lowerbound l $ k"
          "interval_lowerbound ({a..b} \<inter> {x. x $ k \<ge> interval_upperbound l $ k}) $ k = interval_upperbound l $ k"
     unfolding interval_split apply(subst interval_bounds) prefer 3 apply(subst interval_bounds)
     unfolding l interval_bounds[OF uv(1)] using uv[rule_format,of k] ab by auto
   have "\<exists>x. x \<in> ?D - ?D2" using assms(2-) apply-apply(erule disjE)
     apply(rule_tac x="(k,(interval_lowerbound l)$k)" in exI) defer
     apply(rule_tac x="(k,(interval_upperbound l)$k)" in exI)
     unfolding division_points_def unfolding interval_bounds[OF ab]
-    apply (auto simp add:interval_bounds) unfolding * by auto
+    apply auto unfolding * by auto
   thus "?D2 \<subset> ?D" apply-apply(rule,rule division_points_subset[OF assms(1-4)]) by auto qed
 
 subsection {* Preservation by divisions and tagged divisions. *}
 
 lemma support_support[simp]:"support opp f (support opp f s) = support opp f s"

 
 lemma rsum_component_le: fixes f::"real^'n \<Rightarrow> real^'m"
   assumes "p tagged_division_of {a..b}"  "\<forall>x\<in>{a..b}. (f x)$i \<le> (g x)$i"
   shows "(setsum (\<lambda>(x,k). content k *\<^sub>R f x) p)$i \<le> (setsum (\<lambda>(x,k). content k *\<^sub>R g x) p)$i"
   unfolding setsum_component apply(rule setsum_mono)
-  apply(rule mp) defer apply assumption apply(induct_tac x,rule) unfolding split_conv
+  apply(rule mp) defer apply assumption unfolding split_paired_all apply rule unfolding split_conv
 proof- fix a b assume ab:"(a,b) \<in> p" note assm = tagged_division_ofD(2-4)[OF assms(1) ab]
   from this(3) guess u v apply-by(erule exE)+ note b=this
   show "(content b *\<^sub>R f a) $ i \<le> (content b *\<^sub>R g a) $ i" unfolding b
     unfolding Cart_nth.scaleR real_scaleR_def apply(rule mult_left_mono)
     defer apply(rule content_pos_le,rule assms(2)[rule_format]) using assm by auto qed

 lemma additive_tagged_division_1: fixes f::"real^1 \<Rightarrow> 'a::real_normed_vector"
   assumes "dest_vec1 a \<le> dest_vec1 b" "p tagged_division_of {a..b}"
   shows "setsum (\<lambda>(x,k). f(interval_upperbound k) - f(interval_lowerbound k)) p = f b - f a"
 proof- let ?f = "(\<lambda>k::(real^1) set. if k = {} then 0 else f(interval_upperbound k) - f(interval_lowerbound k))"
   have *:"operative op + ?f" unfolding operative_1_lt[OF monoidal_monoid] interval_eq_empty_1
-    by(auto simp add:not_less interval_bound_1 vector_less_def)
+    by(auto simp add:not_less vector_less_def)
   have **:"{a..b} \<noteq> {}" using assms(1) by auto note operative_tagged_division[OF monoidal_monoid * assms(2)]
   note * = this[unfolded if_not_P[OF **] interval_bound_1[OF assms(1)],THEN sym ]
   show ?thesis unfolding * apply(subst setsum_iterate[THEN sym]) defer
     apply(rule setsum_cong2) unfolding split_paired_all split_conv using assms(2) by auto qed
 

   assumes"a \<le> b" "continuous_on {a..b} f" "\<forall>x\<in>{a<..<b}. (f has_vector_derivative f'(x)) (at x)"
   shows "((f' o dest_vec1) has_integral (f b - f a)) {vec a..vec b}"
 proof- { presume *:"a < b \<Longrightarrow> ?thesis" 
     show ?thesis proof(cases,rule *,assumption)
       assume "\<not> a < b" hence "a = b" using assms(1) by auto
-      hence *:"{vec a .. vec b} = {vec b}" "f b - f a = 0" apply(auto simp add: Cart_simps) by smt
+      hence *:"{vec a .. vec b} = {vec b}" "f b - f a = 0" by(auto simp add: Cart_eq vector_le_def order_antisym)
       show ?thesis unfolding *(2) apply(rule has_integral_null) unfolding content_eq_0_1 using * `a=b` by auto
     qed } assume ab:"a < b"
   let ?P = "\<lambda>e. \<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of {vec1 a..vec1 b} \<and> d fine p \<longrightarrow>
                    norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R (f' \<circ> dest_vec1) x) - (f b - f a)) \<le> e * content {vec1 a..vec1 b})"
   { presume "\<And>e. e>0 \<Longrightarrow> ?P e" thus ?thesis unfolding has_integral_factor_content by auto }

           < norm (content k *\<^sub>R f' (dest_vec1 x) - (f (dest_vec1 (interval_upperbound k)) - f (dest_vec1 (interval_lowerbound k))))"
         from p(4)[OF this(1)] guess u v apply-by(erule exE)+ note k=this
         hence "\<forall>i. u$i \<le> v$i" and uv:"{u,v}\<subseteq>{u..v}" using p(2)[OF as(1)] by auto note this(1) this(1)[unfolded forall_1]
         note result = as(2)[unfolded k interval_bounds[OF this(1)] content_1[OF this(2)]]
 
-        assume as':"x \<noteq> vec1 a" "x \<noteq> vec1 b" hence "x$1 \<in> {a<..<b}" using p(2-3)[OF as(1)] by(auto simp add:Cart_simps) note  * = d(2)[OF this] 
+        assume as':"x \<noteq> vec1 a" "x \<noteq> vec1 b" hence "x$1 \<in> {a<..<b}" using p(2-3)[OF as(1)] by(auto simp add: Cart_eq) note  * = d(2)[OF this]
         have "norm ((v$1 - u$1) *\<^sub>R f' (x$1) - (f (v$1) - f (u$1))) =
           norm ((f (u$1) - f (x$1) - (u$1 - x$1) *\<^sub>R f' (x$1)) - (f (v$1) - f (x$1) - (v$1 - x$1) *\<^sub>R f' (x$1)))" 
           apply(rule arg_cong[of _ _ norm]) unfolding scaleR_left.diff by auto 
         also have "... \<le> e / 2 * norm (u$1 - x$1) + e / 2 * norm (v$1 - x$1)" apply(rule norm_triangle_le_sub)
           apply(rule add_mono) apply(rule_tac[!] *) using fineD[OF goal2(2) as(1)] as' unfolding k subset_eq

       unfolding `x=a` vector_dist_norm apply(rule d(2)[rule_format]) unfolding norm_real by auto
   next   assume "x=b" have "b \<le> b" by auto
     from indefinite_integral_continuous_left[OF assms(1) `a<b` this `e>0`] guess d . note d=this
     show ?thesis apply(rule,rule,rule d,safe) apply(subst dist_commute)
       unfolding `x=b` vector_dist_norm apply(rule d(2)[rule_format]) unfolding norm_real by auto
-  next assume "a<x \<and> x<b" hence xl:"a<x" "x\<le>b" and xr:"a\<le>x" "x<b" by(auto simp add:Cart_simps)
+  next assume "a<x \<and> x<b" hence xl:"a<x" "x\<le>b" and xr:"a\<le>x" "x<b" by(auto simp add: vector_less_def)
     from indefinite_integral_continuous_left [OF assms(1) xl `e>0`] guess d1 . note d1=this
     from indefinite_integral_continuous_right[OF assms(1) xr `e>0`] guess d2 . note d2=this
     show ?thesis apply(rule_tac x="min d1 d2" in exI)
     proof safe show "0 < min d1 d2" using d1 d2 by auto
       fix y assume "y\<in>{a..b}" "dist y x < min d1 d2"

   have "(f \<circ> (\<lambda>t. (1 - t) *\<^sub>R c + t *\<^sub>R x)) 1 = y"
     apply(rule has_derivative_zero_unique_strong_interval[OF as2 as1, of ])
     unfolding o_def using assms(5) defer apply-apply(rule)
   proof- fix t assume as:"t\<in>{0..1} - {t. (1 - t) *\<^sub>R c + t *\<^sub>R x \<in> k}"
     have *:"c - t *\<^sub>R c + t *\<^sub>R x \<in> s - k" apply safe apply(rule conv[unfolded scaleR_simps]) 
-      using `x\<in>s` `c\<in>s` as by(auto simp add:scaleR_simps)
+      using `x\<in>s` `c\<in>s` as by(auto simp add: algebra_simps)
     have "(f \<circ> (\<lambda>t. (1 - t) *\<^sub>R c + t *\<^sub>R x) has_derivative (\<lambda>x. 0) \<circ> (\<lambda>z. (0 - z *\<^sub>R c) + z *\<^sub>R x)) (at t within {0..1})"
       apply(rule diff_chain_within) apply(rule has_derivative_add)
       unfolding scaleR_simps apply(rule has_derivative_sub) apply(rule has_derivative_const)
       apply(rule has_derivative_vmul_within,rule has_derivative_id)+ 
       apply(rule has_derivative_within_subset,rule assms(6)[rule_format])

   proof safe case goal1 show ?case apply(rule has_integral_negligible[OF `?r`[rule_format,of a b]])
       unfolding indicator_def by auto qed qed auto
 
 lemma has_integral_spike_set_eq: fixes f::"real^'n \<Rightarrow> 'a::banach" 
   assumes "negligible((s - t) \<union> (t - s))" shows "((f has_integral y) s \<longleftrightarrow> (f has_integral y) t)"
-  unfolding has_integral_restrict_univ[THEN sym,of f] apply(rule has_integral_spike_eq[OF assms]) by auto
+  unfolding has_integral_restrict_univ[THEN sym,of f] apply(rule has_integral_spike_eq[OF assms]) by (safe, auto split: split_if_asm)
 
 lemma has_integral_spike_set[dest]: fixes f::"real^'n \<Rightarrow> 'a::banach"
   assumes "negligible((s - t) \<union> (t - s))" "(f has_integral y) s"
   shows "(f has_integral y) t"
   using assms has_integral_spike_set_eq by auto