the integral is 0 when otherwise it would be undefined (also for contour integrals)

--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Fri Feb 26 15:49:35 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Mon Feb 29 11:42:15 2016 +0000
@@ -642,10 +642,14 @@
   where "f contour_integrable_on g \<equiv> \<exists>i. (f has_contour_integral i) g"
 
 definition contour_integral
-  where "contour_integral g f \<equiv> @i. (f has_contour_integral i) g"
-
-lemma contour_integral_unique: "(f has_contour_integral i)  g \<Longrightarrow> contour_integral g f = i"
-  by (auto simp: contour_integral_def has_contour_integral_def integral_def [symmetric])
+  where "contour_integral g f \<equiv> @i. (f has_contour_integral i) g \<or> ~ f contour_integrable_on g \<and> i=0"
+
+lemma not_integrable_contour_integral: "~ f contour_integrable_on g \<Longrightarrow> contour_integral g f = 0"
+  unfolding contour_integrable_on_def contour_integral_def by blast 
+
+lemma contour_integral_unique: "(f has_contour_integral i) g \<Longrightarrow> contour_integral g f = i"
+  apply (simp add: contour_integral_def has_contour_integral_def contour_integrable_on_def)
+  using has_integral_unique by blast
 
 corollary has_contour_integral_eqpath:
      "\<lbrakk>(f has_contour_integral y) p; f contour_integrable_on \<gamma>;
@@ -769,8 +773,16 @@
   using contour_integrable_reversepath valid_path_reversepath by fastforce
 
 lemma contour_integral_reversepath:
-    "\<lbrakk>valid_path g; f contour_integrable_on g\<rbrakk> \<Longrightarrow> contour_integral (reversepath g) f = -(contour_integral g f)"
-  using has_contour_integral_reversepath contour_integrable_on_def contour_integral_unique by blast
+  assumes "valid_path g"
+    shows "contour_integral (reversepath g) f = - (contour_integral g f)"
+proof (cases "f contour_integrable_on g")
+  case True then show ?thesis
+    by (simp add: assms contour_integral_unique has_contour_integral_integral has_contour_integral_reversepath)
+next
+  case False then have "~ f contour_integrable_on (reversepath g)"
+    by (simp add: assms contour_integrable_reversepath_eq)
+  with False show ?thesis by (simp add: not_integrable_contour_integral)
+qed
 
 
 subsection\<open>Joining two paths together\<close>
@@ -1093,10 +1105,16 @@
     shows "(f has_contour_integral i) (shiftpath a g) \<longleftrightarrow> (f has_contour_integral i) g"
   using assms has_contour_integral_shiftpath has_contour_integral_shiftpath_D by blast
 
+lemma contour_integrable_on_shiftpath_eq:
+  assumes "valid_path g" "pathfinish g = pathstart g" "a \<in> {0..1}"
+    shows "f contour_integrable_on (shiftpath a g) \<longleftrightarrow> f contour_integrable_on g"
+using assms contour_integrable_on_def has_contour_integral_shiftpath_eq by auto
+
 lemma contour_integral_shiftpath:
   assumes "valid_path g" "pathfinish g = pathstart g" "a \<in> {0..1}"
     shows "contour_integral (shiftpath a g) f = contour_integral g f"
-   using assms by (simp add: contour_integral_def has_contour_integral_shiftpath_eq)
+   using assms   
+   by (simp add: contour_integral_def contour_integrable_on_def has_contour_integral_shiftpath_eq)
 
 
 subsection\<open>More about straight-line paths\<close>
@@ -1325,8 +1343,8 @@
 qed
 
 lemma contour_integral_integral:
-  shows "contour_integral g f = integral {0..1} (\<lambda>x. f (g x) * vector_derivative g (at x))"
-  by (simp add: contour_integral_def integral_def has_contour_integral)
+     "contour_integral g f = integral {0..1} (\<lambda>x. f (g x) * vector_derivative g (at x))"
+  by (simp add: contour_integral_def integral_def has_contour_integral contour_integrable_on)
 
 
 subsection\<open>Segments via convex hulls\<close>
@@ -1577,7 +1595,9 @@
 
 lemma contour_integral_eq:
     "(\<And>x. x \<in> path_image p \<Longrightarrow> f x = g x) \<Longrightarrow> contour_integral p f = contour_integral p g"
-  by (simp add: contour_integral_def) (metis has_contour_integral_eq)
+  apply (simp add: contour_integral_def)
+  using has_contour_integral_eq
+  by (metis contour_integral_unique has_contour_integral_integrable has_contour_integral_integral)
 
 lemma contour_integral_eq_0:
     "(\<And>z. z \<in> path_image g \<Longrightarrow> f z = 0) \<Longrightarrow> contour_integral g f = 0"
@@ -1877,16 +1897,16 @@
     done
   also have "... = integral {0..1}
                      (\<lambda>y. contour_integral g (\<lambda>x. f x (h y) * vector_derivative h (at y)))"
-    apply (simp add: contour_integral_integral)
+    apply (simp only: contour_integral_integral)
     apply (subst integral_swap_continuous [where 'a = real and 'b = real, of 0 0 1 1, simplified])
-    apply (rule fgh gvcon' hvcon' continuous_intros | simp add: split_def)+
-    apply (simp add: algebra_simps)
+     apply (rule fgh gvcon' hvcon' continuous_intros | simp add: split_def)+
+    unfolding integral_mult_left [symmetric]
+    apply (simp only: mult_ac)
     done
   also have "... = contour_integral h (\<lambda>z. contour_integral g (\<lambda>w. f w z))"
     apply (simp add: contour_integral_integral)
     apply (rule integral_cong)
-    apply (subst integral_mult_left [symmetric])
-    apply (blast intro: vdg)
+    unfolding integral_mult_left [symmetric]
     apply (simp add: algebra_simps)
     done
   finally show ?thesis

--- a/src/HOL/Multivariate_Analysis/Conformal_Mappings.thy	Fri Feb 26 15:49:35 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Conformal_Mappings.thy	Mon Feb 29 11:42:15 2016 +0000
@@ -1521,10 +1521,7 @@
   then have 2: "contour_integral (linepath b c) f =
                 contour_integral (linepath b a') f + contour_integral (linepath a' c) f"
     by (rule contour_integral_split_linepath [OF _ a'])
-  have "f contour_integrable_on linepath b' a'"
-    by (meson a'b' contf continuous_on_subset contour_integrable_continuous_linepath
-              convex_contains_segment \<open>convex S\<close>)
-  then have 3: "contour_integral (reversepath (linepath b' a')) f =
+  have 3: "contour_integral (reversepath (linepath b' a')) f =
                 - contour_integral (linepath b' a') f"
     by (rule contour_integral_reversepath [OF valid_path_linepath])
   have fcd_le: "f complex_differentiable at x"

--- a/src/HOL/Multivariate_Analysis/Integration.thy	Fri Feb 26 15:49:35 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Mon Feb 29 11:42:15 2016 +0000
@@ -1806,10 +1806,13 @@
 definition integrable_on (infixr "integrable'_on" 46)
   where "f integrable_on i \<longleftrightarrow> (\<exists>y. (f has_integral y) i)"
 
-definition "integral i f = (SOME y. (f has_integral y) i)"
+definition "integral i f = (SOME y. (f has_integral y) i \<or> ~ f integrable_on i \<and> y=0)"
 
 lemma integrable_integral[dest]: "f integrable_on i \<Longrightarrow> (f has_integral (integral i f)) i"
-  unfolding integrable_on_def integral_def by (rule someI_ex)
+  unfolding integrable_on_def integral_def by (metis (mono_tags, lifting) someI_ex)
+
+lemma not_integrable_integral: "~ f integrable_on i \<Longrightarrow> integral i f = 0"
+  unfolding integrable_on_def integral_def by blast 
 
 lemma has_integral_integrable[intro]: "(f has_integral i) s \<Longrightarrow> f integrable_on s"
   unfolding integrable_on_def by auto
@@ -2328,6 +2331,12 @@
   unfolding integral_def
   by (rule some_equality) (auto intro: has_integral_unique)
 
+lemma eq_integralD: "integral k f = y \<Longrightarrow> (f has_integral y) k \<or> ~ f integrable_on k \<and> y=0"
+  unfolding integral_def integrable_on_def
+  apply (erule subst)
+  apply (rule someI_ex)
+  by blast
+
 lemma has_integral_is_0:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::real_normed_vector"
   assumes "\<forall>x\<in>s. f x = 0"
@@ -2468,14 +2477,29 @@
   using has_integral_linear[OF _ bounded_linear_scaleR_left] by (simp add: comp_def)
 
 lemma has_integral_mult_left:
-  fixes c :: "_ :: {real_normed_algebra}"
+  fixes c :: "_ :: real_normed_algebra"
   shows "(f has_integral y) s \<Longrightarrow> ((\<lambda>x. f x * c) has_integral (y * c)) s"
   using has_integral_linear[OF _ bounded_linear_mult_left] by (simp add: comp_def)
 
-corollary integral_mult_left:
-  fixes c:: "'a::real_normed_algebra"
-  shows "f integrable_on s \<Longrightarrow> integral s (\<lambda>x. f x * c) = integral s f * c"
-  by (blast intro:  has_integral_mult_left)
+text\<open>The case analysis eliminates the condition @{term "f integrable_on s"} at the cost
+     of the type class constraint @{text"division_ring"}\<close>
+corollary integral_mult_left [simp]:
+  fixes c:: "'a::{real_normed_algebra,division_ring}"
+  shows "integral s (\<lambda>x. f x * c) = integral s f * c"
+proof (cases "f integrable_on s \<or> c = 0")
+  case True then show ?thesis
+    by (force intro: has_integral_mult_left)
+next
+  case False then have "~ (\<lambda>x. f x * c) integrable_on s"
+    using has_integral_mult_left [of "(\<lambda>x. f x * c)" _ s "inverse c"]
+    by (force simp add: mult.assoc)
+  with False show ?thesis by (simp add: not_integrable_integral)
+qed
+
+corollary integral_mult_right [simp]:
+  fixes c:: "'a::{real_normed_field}"
+  shows "integral s (\<lambda>x. c * f x) = c * integral s f"
+by (simp add: mult.commute [of c])
 
 lemma has_integral_mult_right:
   fixes c :: "'a :: real_normed_algebra"
@@ -2499,7 +2523,7 @@
     unfolding real_scaleR_def .
 qed
 
-lemma has_integral_neg: "(f has_integral k) s \<Longrightarrow> ((\<lambda>x. -(f x)) has_integral (-k)) s"
+lemma has_integral_neg: "(f has_integral k) s \<Longrightarrow> ((\<lambda>x. -(f x)) has_integral -k) s"
   by (drule_tac c="-1" in has_integral_cmul) auto
 
 lemma has_integral_add:
@@ -2608,7 +2632,7 @@
   unfolding algebra_simps
   by auto
 
-lemma integral_0:
+lemma integral_0 [simp]:
   "integral s (\<lambda>x::'n::euclidean_space. 0::'m::real_normed_vector) = 0"
   by (rule integral_unique has_integral_0)+
 
@@ -2616,11 +2640,26 @@
     integral s (\<lambda>x. f x + g x) = integral s f + integral s g"
   by (rule integral_unique) (metis integrable_integral has_integral_add)
 
-lemma integral_cmul: "f integrable_on s \<Longrightarrow> integral s (\<lambda>x. c *\<^sub>R f x) = c *\<^sub>R integral s f"
-  by (rule integral_unique) (metis integrable_integral has_integral_cmul)
-
-lemma integral_neg: "f integrable_on s \<Longrightarrow> integral s (\<lambda>x. - f x) = - integral s f"
-  by (rule integral_unique) (metis integrable_integral has_integral_neg)
+lemma integral_cmul [simp]: "integral s (\<lambda>x. c *\<^sub>R f x) = c *\<^sub>R integral s f"
+proof (cases "f integrable_on s \<or> c = 0")
+  case True with has_integral_cmul show ?thesis by force
+next
+  case False then have "~ (\<lambda>x. c *\<^sub>R f x) integrable_on s"
+    using has_integral_cmul [of "(\<lambda>x. c *\<^sub>R f x)" _ s "inverse c"]
+    by force
+  with False show ?thesis by (simp add: not_integrable_integral)
+qed
+
+lemma integral_neg [simp]: "integral s (\<lambda>x. - f x) = - integral s f"
+proof (cases "f integrable_on s")
+  case True then show ?thesis
+    by (simp add: has_integral_neg integrable_integral integral_unique)
+next
+  case False then have "~ (\<lambda>x. - f x) integrable_on s"
+    using has_integral_neg [of "(\<lambda>x. - f x)" _ s ]
+    by force
+  with False show ?thesis by (simp add: not_integrable_integral)
+qed
 
 lemma integral_diff: "f integrable_on s \<Longrightarrow> g integrable_on s \<Longrightarrow>
     integral s (\<lambda>x. f x - g x) = integral s f - integral s g"
@@ -2715,7 +2754,7 @@
   assumes "\<And>x. x \<in> s \<Longrightarrow> f x = g x"
   shows "integral s f = integral s g"
   unfolding integral_def
-  by (metis assms has_integral_cong)
+by (metis (full_types, hide_lams) assms has_integral_cong integrable_eq)
 
 lemma has_integral_null [intro]:
   assumes "content(cbox a b) = 0"
@@ -4427,12 +4466,17 @@
 lemma integral_component_nonneg:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes "k \<in> Basis"
-    and "f integrable_on s" "\<forall>x\<in>s. 0 \<le> (f x)\<bullet>k"
+    and  "\<forall>x\<in>s. 0 \<le> (f x)\<bullet>k"
   shows "0 \<le> (integral s f)\<bullet>k"
-  apply (rule has_integral_component_nonneg)
-  using assms
-  apply auto
-  done
+proof (cases "f integrable_on s")
+  case True show ?thesis
+    apply (rule has_integral_component_nonneg)
+    using assms True
+    apply auto
+    done
+next
+  case False then show ?thesis by (simp add: not_integrable_integral)
+qed
 
 lemma has_integral_component_neg:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
@@ -5345,9 +5389,7 @@
   assumes "negligible s"
     and "\<forall>x\<in>(t - s). g x = f x"
   shows "integral t f = integral t g"
-  unfolding integral_def
-  using has_integral_spike_eq[OF assms]
-  by auto
+  using has_integral_spike_eq[OF assms] by (simp add: integral_def integrable_on_def)
 
 
 subsection \<open>Some other trivialities about negligible sets.\<close>
@@ -8146,10 +8188,7 @@
     using p by auto
   have **: "g integrable_on cbox c d"
     apply (rule integrable_spike_interior[where f=f])
-    unfolding g_def
-    defer
-    apply (rule has_integral_integrable)
-    using assms(1)
+    unfolding g_def  using assms(1)
     apply auto
     done
   moreover
@@ -9426,12 +9465,7 @@
     note kl = tagged_division_ofD(3,4)[OF qq[THEN conjunct1]]
     from this(2)[OF as(4,1)] guess u v by (elim exE) note uv=this
     have *: "interior (k \<inter> l) = {}"
-      unfolding interior_Int
-      apply (rule q')
-      using as
-      unfolding r_def
-      apply auto
-      done
+      by (metis DiffE \<open>T1 = qq k\<close> \<open>T1 \<noteq> T2\<close> \<open>T2 = qq l\<close> as(4) as(5) interior_Int q'(5) r_def)
     have "interior m = {}"
       unfolding subset_empty[symmetric]
       unfolding *[symmetric]
@@ -10234,7 +10268,6 @@
     apply (rule_tac x="integral s (f k)" in bexI)
     prefer 3
     apply (rule_tac x=k in exI)
-    unfolding integral_neg[OF assm(1)]
     apply auto
     done
   have "(\<lambda>x. - g x) integrable_on s \<and>
@@ -10254,14 +10287,8 @@
     done
   note * = conjunctD2[OF this]
   show ?thesis
-    apply rule
-    using integrable_neg[OF *(1)]
-    defer
-    using tendsto_minus[OF *(2)]
-    unfolding integral_neg[OF assm(1)]
-    unfolding integral_neg[OF *(1),symmetric]
-    apply auto
-    done
+    using integrable_neg[OF *(1)] tendsto_minus[OF *(2)]
+    by auto
 qed
 
 
@@ -11402,11 +11429,9 @@
         unfolding inner_minus_left[symmetric]
         defer
         apply (subst integral_neg[symmetric])
-        defer
         apply (rule_tac[1-2] integral_component_le[OF i])
-        apply (rule integrable_neg)
         using integrable_on_subcbox[OF assms(1),of a b]
-          integrable_on_subcbox[OF assms(2),of a b] i
+          integrable_on_subcbox[OF assms(2),of a b] i  integrable_neg
         unfolding ab
         apply auto
         done