--- a/src/HOL/Multivariate_Analysis/Integration_MV.cert Thu Feb 18 22:11:19 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration_MV.cert Mon Feb 22 20:08:10 2010 +0100
@@ -3268,3 +3268,29 @@
#269 := [quant-inst]: #268
[unit-resolution #269 #247 #274]: false
unsat
+vqiyJ/qjGXZ3iOg6xftiug 15 0
+uf_1 -> val!0
+uf_2 -> val!1
+uf_3 -> val!2
+uf_5 -> val!15
+uf_6 -> val!26
+uf_4 -> {
+ val!0 -> val!12
+ val!1 -> val!13
+ else -> val!13
+}
+uf_7 -> {
+ val!6 -> val!31
+ else -> val!31
+}
+sat
+mrZPJZyTokErrN6SYupisw 9 0
+uf_4 -> val!1
+uf_2 -> val!3
+uf_3 -> val!4
+uf_1 -> {
+ val!5 -> val!6
+ val!4 -> val!7
+ else -> val!7
+}
+sat
--- a/src/HOL/Multivariate_Analysis/Integration_MV.thy Thu Feb 18 22:11:19 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration_MV.thy Mon Feb 22 20:08:10 2010 +0100
@@ -853,6 +853,14 @@
lemma has_integral_integral:"f integrable_on s \<longleftrightarrow> (f has_integral (integral s f)) s"
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)
+ 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:
assumes "content({a..b}) = 0" "p tagged_division_of {a..b}"
shows "setsum (\<lambda>(x,k). content k *\<^sub>R f x) p = (0::'a::real_normed_vector)"