# HG changeset patch
# User himmelma
# Date 1266865690 -3600
# Node ID ead7bfc30b26779f4d5b6dea319de22b0f12adb0
# Parent  3707f625314f801436f0e7ee916570b1f383d471
Support for one-dimensional integration in Multivariate-Analysis

diff -r 3707f625314f -r ead7bfc30b26 src/HOL/Multivariate_Analysis/Integration_MV.cert
--- 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
diff -r 3707f625314f -r ead7bfc30b26 src/HOL/Multivariate_Analysis/Integration_MV.thy
--- 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)"