# HG changeset patch
# User himmelma
# Date 1267520269 -3600
# Node ID 3d073a3e1c61e415dc0006588dd6e8632e74c3e3
# Parent  5f1ea533158cb7ab8983ebb584505e3b63df5c56
the ordering on real^1 is linear

diff -r 5f1ea533158c -r 3d073a3e1c61 src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Tue Mar 02 09:05:50 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Tue Mar 02 09:57:49 2010 +0100
@@ -100,6 +100,12 @@
   instance ..
 end
 
+instantiation cart :: (scaleR, finite) scaleR
+begin
+  definition vector_scaleR_def: "scaleR = (\<lambda> r x.  (\<chi> i. scaleR r (x$i)))"
+  instance ..
+end
+
 instantiation cart :: (ord,finite) ord
 begin
   definition vector_le_def:
@@ -108,12 +114,31 @@
   instance by (intro_classes)
 end
 
-instantiation cart :: (scaleR, finite) scaleR
+text{* The ordering on real^1 is linear. *}
+
+class cart_one = assumes UNIV_one: "card (UNIV \<Colon> 'a set) = Suc 0"
 begin
-  definition vector_scaleR_def: "scaleR = (\<lambda> r x.  (\<chi> i. scaleR r (x$i)))"
-  instance ..
+  subclass finite
+  proof from UNIV_one show "finite (UNIV :: 'a set)"
+      by (auto intro!: card_ge_0_finite) qed
 end
 
+instantiation num1 :: cart_one begin
+instance proof
+  show "CARD(1) = Suc 0" by auto
+qed end
+
+instantiation cart :: (linorder,cart_one) linorder begin
+instance proof
+  guess a B using UNIV_one[where 'a='b] unfolding card_Suc_eq apply- by(erule exE)+
+  hence *:"UNIV = {a}" by auto
+  have "\<And>P. (\<forall>i\<in>UNIV. P i) \<longleftrightarrow> P a" unfolding * by auto hence all:"\<And>P. (\<forall>i. P i) \<longleftrightarrow> P a" by auto
+  fix x y z::"'a^'b::cart_one" note * = vector_le_def vector_less_def all Cart_eq
+  show "x\<le>x" "(x < y) = (x \<le> y \<and> \<not> y \<le> x)" "x\<le>y \<or> y\<le>x" unfolding * by(auto simp only:field_simps)
+  { assume "x\<le>y" "y\<le>z" thus "x\<le>z" unfolding * by(auto simp only:field_simps) }
+  { assume "x\<le>y" "y\<le>x" thus "x=y" unfolding * by(auto simp only:field_simps) }
+qed end
+
 text{* Also the scalar-vector multiplication. *}
 
 definition vector_scalar_mult:: "'a::times \<Rightarrow> 'a ^ 'n \<Rightarrow> 'a ^ 'n" (infixl "*s" 70)
diff -r 5f1ea533158c -r 3d073a3e1c61 src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue Mar 02 09:05:50 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Tue Mar 02 09:57:49 2010 +0100
@@ -1310,9 +1310,12 @@
 lemma integral_empty[simp]: shows "integral {} f = 0"
   apply(rule integral_unique) using has_integral_empty .
 
-lemma has_integral_refl[intro]: shows "(f has_integral 0) {a..a}"
-  apply(rule has_integral_null) unfolding content_eq_0_interior
-  unfolding interior_closed_interval using interval_sing by auto
+lemma has_integral_refl[intro]: shows "(f has_integral 0) {a..a}" "(f has_integral 0) {a}"
+proof- have *:"{a} = {a..a}" apply(rule set_ext) unfolding mem_interval singleton_iff Cart_eq
+    apply safe prefer 3 apply(erule_tac x=i in allE) by(auto simp add: field_simps)
+  show "(f has_integral 0) {a..a}" "(f has_integral 0) {a}" unfolding *
+    apply(rule_tac[!] has_integral_null) unfolding content_eq_0_interior
+    unfolding interior_closed_interval using interval_sing by auto qed
 
 lemma integrable_on_refl[intro]: shows "f integrable_on {a..a}" unfolding integrable_on_def by auto
 
@@ -2811,6 +2814,9 @@
 
 subsection {* Special case of additivity we need for the FCT. *}
 
+lemma interval_bound_sing[simp]: "interval_upperbound {a} = a"  "interval_lowerbound {a} = a"
+  unfolding interval_upperbound_def interval_lowerbound_def unfolding Cart_eq by auto
+
 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"