ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order

--- a/src/HOL/Library/Product_Order.thy	Mon Dec 16 17:08:22 2013 +0100
+++ b/src/HOL/Library/Product_Order.thy	Mon Dec 16 17:08:22 2013 +0100
@@ -5,7 +5,7 @@
 header {* Pointwise order on product types *}
 
 theory Product_Order
-imports Product_plus
+imports Product_plus Conditionally_Complete_Lattices
 begin
 
 subsection {* Pointwise ordering *}
@@ -54,7 +54,7 @@
 
 subsection {* Binary infimum and supremum *}
 
-instantiation prod :: (semilattice_inf, semilattice_inf) semilattice_inf
+instantiation prod :: (inf, inf) inf
 begin
 
 definition
@@ -69,12 +69,14 @@
 lemma snd_inf [simp]: "snd (inf x y) = inf (snd x) (snd y)"
   unfolding inf_prod_def by simp
 
-instance
+instance proof qed
+end
+
+instance prod :: (semilattice_inf, semilattice_inf) semilattice_inf
   by default auto
 
-end
 
-instantiation prod :: (semilattice_sup, semilattice_sup) semilattice_sup
+instantiation prod :: (sup, sup) sup
 begin
 
 definition
@@ -89,11 +91,12 @@
 lemma snd_sup [simp]: "snd (sup x y) = sup (snd x) (snd y)"
   unfolding sup_prod_def by simp
 
-instance
+instance proof qed
+end
+
+instance prod :: (semilattice_sup, semilattice_sup) semilattice_sup
   by default auto
 
-end
-
 instance prod :: (lattice, lattice) lattice ..
 
 instance prod :: (distrib_lattice, distrib_lattice) distrib_lattice
@@ -154,21 +157,33 @@
 
 subsection {* Complete lattice operations *}
 
-instantiation prod :: (complete_lattice, complete_lattice) complete_lattice
+instantiation prod :: (Inf, Inf) Inf
+begin
+
+definition
+  "Inf A = (INF x:A. fst x, INF x:A. snd x)"
+
+instance proof qed
+end
+
+instantiation prod :: (Sup, Sup) Sup
 begin
 
 definition
   "Sup A = (SUP x:A. fst x, SUP x:A. snd x)"
 
-definition
-  "Inf A = (INF x:A. fst x, INF x:A. snd x)"
+instance proof qed
+end
 
-instance
+instance prod :: (conditionally_complete_lattice, conditionally_complete_lattice)
+    conditionally_complete_lattice
+  by default (force simp: less_eq_prod_def Inf_prod_def Sup_prod_def bdd_below_def bdd_above_def
+    INF_def SUP_def intro!: cInf_lower cSup_upper cInf_greatest cSup_least)+
+
+instance prod :: (complete_lattice, complete_lattice) complete_lattice
   by default (simp_all add: less_eq_prod_def Inf_prod_def Sup_prod_def
     INF_lower SUP_upper le_INF_iff SUP_le_iff bot_prod_def top_prod_def)
 
-end
-
 lemma fst_Sup: "fst (Sup A) = (SUP x:A. fst x)"
   unfolding Sup_prod_def by simp
 

--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Mon Dec 16 17:08:22 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Mon Dec 16 17:08:22 2013 +0100
@@ -58,7 +58,7 @@
 begin
 
 definition "x \<le> y \<longleftrightarrow> (\<forall>i. x$i \<le> y$i)"
-definition "x < y \<longleftrightarrow> (\<forall>i. x$i < y$i)"
+definition "x < (y::'a^'b) \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
 instance ..
 
 end
@@ -77,10 +77,11 @@
 
 end
 
-instantiation vec :: (linorder, cart_one) linorder
-begin
+instance vec:: (order, finite) order
+  by default (auto simp: less_eq_vec_def less_vec_def vec_eq_iff
+      intro: order.trans order.antisym order.strict_implies_order)
 
-instance
+instance vec :: (linorder, cart_one) linorder
 proof
   obtain a :: 'b where all: "\<And>P. (\<forall>i. P i) \<longleftrightarrow> P a"
   proof -
@@ -89,17 +90,12 @@
     then have "\<And>P. (\<forall>i\<in>UNIV. P i) \<longleftrightarrow> P b" by auto
     then show thesis by (auto intro: that)
   qed
-
+  fix x y :: "'a^'b::cart_one"
   note [simp] = less_eq_vec_def less_vec_def all vec_eq_iff field_simps
-  fix x y z :: "'a^'b::cart_one"
-  show "x \<le> x" "(x < y) = (x \<le> y \<and> \<not> y \<le> x)" "x \<le> y \<or> y \<le> x" by auto
-  { assume "x\<le>y" "y\<le>z" then show "x\<le>z" by auto }
-  { assume "x\<le>y" "y\<le>x" then show "x=y" by auto }
+  show "x \<le> y \<or> y \<le> x" by auto
 qed
 
-end
-
-text{* Constant Vectors *} 
+text{* Constant Vectors *}
 
 definition "vec x = (\<chi> i. x)"
 
@@ -332,14 +328,24 @@
   using setsum_norm_allsubsets_bound[OF assms]
   by (simp add: DIM_cart Basis_real_def)
 
-instance vec :: (ordered_euclidean_space, finite) ordered_euclidean_space
-proof
-  fix x y::"'a^'b"
-  show "(x \<le> y) = (\<forall>i\<in>Basis. x \<bullet> i \<le> y \<bullet> i)"
-    unfolding less_eq_vec_def apply(subst eucl_le) by (simp add: Basis_vec_def inner_axis)
-  show"(x < y) = (\<forall>i\<in>Basis. x \<bullet> i < y \<bullet> i)"
-    unfolding less_vec_def apply(subst eucl_less) by (simp add: Basis_vec_def inner_axis)
-qed
+instantiation vec :: (ordered_euclidean_space, finite) ordered_euclidean_space
+begin
+
+definition "inf x y = (\<chi> i. inf (x $ i) (y $ i))"
+definition "sup x y = (\<chi> i. sup (x $ i) (y $ i))"
+definition "Inf X = (\<chi> i. (INF x:X. x $ i))"
+definition "Sup X = (\<chi> i. (SUP x:X. x $ i))"
+definition "abs x = (\<chi> i. abs (x $ i))"
+
+instance
+  apply default
+  unfolding euclidean_representation_setsum'
+  apply (auto simp: less_eq_vec_def inf_vec_def sup_vec_def Inf_vec_def Sup_vec_def inner_axis
+    Basis_vec_def inner_Basis_inf_left inner_Basis_sup_left inner_Basis_INF_left
+    inner_Basis_SUP_left eucl_le[where 'a='a] less_le_not_le abs_vec_def abs_inner)
+  done
+
+end
 
 subsection {* Matrix operations *}
 
@@ -970,8 +976,6 @@
   fixes a :: "'a::linorder^'n"
   shows "{a .. a} = {a} \<and> {a<..<a} = {}"
   apply (auto simp add: set_eq_iff less_vec_def less_eq_vec_def vec_eq_iff)
-  apply (simp add: order_eq_iff)
-  apply (auto simp add: not_less less_imp_le)
   done
 
 lemma interval_open_subset_closed_cart:

--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Mon Dec 16 17:08:22 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Mon Dec 16 17:08:22 2013 +0100
@@ -75,6 +75,10 @@
   "(\<Sum>i\<in>Basis. f i *\<^sub>R i) = b \<longleftrightarrow> (\<forall>i\<in>Basis. f i = inner b i)"
   by (subst euclidean_eq_iff) simp
 
+lemma (in euclidean_space) euclidean_representation_setsum':
+  "b = (\<Sum>i\<in>Basis. f i *\<^sub>R i) \<longleftrightarrow> (\<forall>i\<in>Basis. f i = inner b i)"
+  by (auto simp add: euclidean_representation_setsum[symmetric])
+
 lemma (in euclidean_space) euclidean_representation: "(\<Sum>b\<in>Basis. inner x b *\<^sub>R b) = x"
   unfolding euclidean_representation_setsum by simp
 

--- a/src/HOL/Multivariate_Analysis/Integration.thy	Mon Dec 16 17:08:22 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Mon Dec 16 17:08:22 2013 +0100
@@ -220,8 +220,7 @@
   where "One \<equiv> \<Sum>Basis"
 
 lemma empty_as_interval: "{} = {One..(0::'a::ordered_euclidean_space)}"
-  apply (auto simp: eucl_le[where 'a='a])
-  by (metis (mono_tags) eucl_less eucl_less_not_refl order.strict_trans2 zero_less_one)
+  by (auto simp: eucl_le[where 'a='a])
 
 lemma interior_subset_union_intervals:
   assumes "i = {a..b::'a::ordered_euclidean_space}"
@@ -1030,14 +1029,14 @@
       then show "\<exists>a b. k = {a..b}"
         by auto
       have "k \<subseteq> {a..b} \<and> k \<noteq> {}"
-      proof (simp add: k interval_eq_empty subset_interval not_less, safe)
+      proof (simp add: k interval_eq_empty subset_interval not_less eucl_le[where 'a='a], safe)
         fix i :: 'a
         assume i: "i \<in> Basis"
         with f have "f i = (a, c) \<or> f i = (c, d) \<or> f i = (d, b)"
           by (auto simp: PiE_iff)
         with i ord[of i]
         show "a \<bullet> i \<le> fst (f i) \<bullet> i" "snd (f i) \<bullet> i \<le> b \<bullet> i" "fst (f i) \<bullet> i \<le> snd (f i) \<bullet> i"
-          by (auto simp: subset_iff eucl_le[where 'a='a])
+          by auto
       qed
       then show "k \<noteq> {}" "k \<subseteq> {a .. b}"
         by auto
@@ -1116,7 +1115,7 @@
       using p(4)[OF goal1] by blast
     have *: "{c..d} \<subseteq> {a..b}" "{c..d} \<noteq> {}"
       using p(2,3)[OF goal1, unfolded k] using assms(2)
-        by auto
+      by (blast intro: order.trans)+
     obtain q where "q division_of {a..b}" "{c..d} \<in> q"
       by (rule partial_division_extend_1[OF *])
     then show ?case
@@ -2025,9 +2024,9 @@
     and "\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> c\<bullet>i \<le> d\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i \<and> 2 * (d\<bullet>i - c\<bullet>i) \<le> b\<bullet>i - a\<bullet>i"
 proof -
   have "{a..b} \<noteq> {}"
-    using assms(1,3) by auto
+    using assms(1,3) by metis
   then have ab: "\<And>i. i\<in>Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
-    by (auto simp: interval_eq_empty not_le)
+    by (auto simp: eucl_le[where 'a='a])
   {
     fix f
     have "finite f \<Longrightarrow>
@@ -2346,15 +2345,8 @@
     qed simp
   } note ABsubset = this
   have "\<exists>a. \<forall>n. a\<in>{A n..B n}"
-    apply (rule decreasing_closed_nest[rule_format,OF closed_interval _ ABsubset interv])
-  proof -
-    fix n
-    show "{A n..B n} \<noteq> {}"
-      apply (cases "0 < n")
-      using AB(3)[of "n - 1"] assms(1,3) AB(1-2)
-      apply auto
-      done
-  qed auto
+    by (rule decreasing_closed_nest[rule_format,OF closed_interval _ ABsubset interv])
+      (metis nat.exhaust AB(1-3) assms(1,3))
   then obtain x0 where x0: "\<And>n. x0 \<in> {A n..B n}"
     by blast
   show thesis
@@ -3723,7 +3715,7 @@
     apply (rule tagged_division_union[OF assms(1-2)])
     unfolding interval_split[OF k] interior_closed_interval
     using k
-    apply (auto simp add: eucl_less[where 'a='a] interval elim!: ballE[where x=k])
+    apply (auto simp add: interval elim!: ballE[where x=k])
     done
 qed
 
@@ -8787,8 +8779,7 @@
     proof -
       case goal1
       then have *: "box c d = {}"
-        using interval_open_subset_closed
-        by auto
+        by (metis bot.extremum_uniqueI interval_open_subset_closed)
       show ?thesis
         using assms(1)
         unfolding *

--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Mon Dec 16 17:08:22 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Mon Dec 16 17:08:22 2013 +0100
@@ -8,6 +8,7 @@
 imports
   Euclidean_Space
   "~~/src/HOL/Library/Infinite_Set"
+  "~~/src/HOL/Library/Product_Order"
 begin
 
 lemma cond_application_beta: "(if b then f else g) x = (if b then f x else g x)"
@@ -2881,9 +2882,9 @@
 lemma infnorm_le_norm: "infnorm x \<le> norm x"
   by (simp add: Basis_le_norm infnorm_Max)
 
-lemma euclidean_inner: "inner x y = (\<Sum>b\<in>Basis. (x \<bullet> b) * (y \<bullet> b))"
-  by (subst (1 2) euclidean_representation[symmetric, where 'a='a])
-     (simp add: inner_setsum_left inner_setsum_right setsum_cases inner_Basis ac_simps if_distrib)
+lemma (in euclidean_space) euclidean_inner: "inner x y = (\<Sum>b\<in>Basis. (x \<bullet> b) * (y \<bullet> b))"
+  by (subst (1 2) euclidean_representation[symmetric])
+    (simp add: inner_setsum_left inner_setsum_right setsum_cases inner_Basis ac_simps if_distrib)
 
 lemma norm_le_infnorm:
   fixes x :: "'a::euclidean_space"
@@ -3111,39 +3112,104 @@
 
 subsection {* An ordering on euclidean spaces that will allow us to talk about intervals *}
 
-class ordered_euclidean_space = ord + euclidean_space +
+class ordered_euclidean_space = ord + inf + sup + abs + Inf + Sup + euclidean_space +
   assumes eucl_le: "x \<le> y \<longleftrightarrow> (\<forall>i\<in>Basis. x \<bullet> i \<le> y \<bullet> i)"
-    and eucl_less: "x < y \<longleftrightarrow> (\<forall>i\<in>Basis. x \<bullet> i < y \<bullet> i)"
-
-lemma eucl_less_not_refl[simp, intro!]: "\<not> x < (x::'a::ordered_euclidean_space)"
-  unfolding eucl_less[where 'a='a] by auto
-
-lemma euclidean_trans[trans]:
-  fixes x y z :: "'a::ordered_euclidean_space"
-  shows "x < y \<Longrightarrow> y < z \<Longrightarrow> x < z"
-    and "x \<le> y \<Longrightarrow> y < z \<Longrightarrow> x < z"
-    and "x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z"
-  unfolding eucl_less[where 'a='a] eucl_le[where 'a='a]
-  by (fast intro: less_trans, fast intro: le_less_trans,
-    fast intro: order_trans)
-
-lemma atLeastAtMost_singleton_euclidean[simp]:
-  fixes a :: "'a::ordered_euclidean_space"
-  shows "{a .. a} = {a}"
-  by (force simp: eucl_le[where 'a='a] euclidean_eq_iff[where 'a='a])
+  assumes eucl_less_le_not_le: "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
+  assumes eucl_inf: "inf x y = (\<Sum>i\<in>Basis. inf (x \<bullet> i) (y \<bullet> i) *\<^sub>R i)"
+  assumes eucl_sup: "sup x y = (\<Sum>i\<in>Basis. sup (x \<bullet> i) (y \<bullet> i) *\<^sub>R i)"
+  assumes eucl_Inf: "Inf X = (\<Sum>i\<in>Basis. (INF x:X. x \<bullet> i) *\<^sub>R i)"
+  assumes eucl_Sup: "Sup X = (\<Sum>i\<in>Basis. (SUP x:X. x \<bullet> i) *\<^sub>R i)"
+  assumes eucl_abs: "abs x = (\<Sum>i\<in>Basis. abs (x \<bullet> i) *\<^sub>R i)"
+begin
+
+subclass order
+  by default
+    (auto simp: eucl_le eucl_less_le_not_le intro!: euclidean_eqI antisym intro: order.trans)
+
+subclass ordered_ab_group_add_abs
+  by default (auto simp: eucl_le inner_add_left eucl_abs abs_leI)
+
+subclass lattice
+  by default (auto simp: eucl_inf eucl_sup eucl_le)
+
+subclass distrib_lattice
+  by default (auto simp: eucl_inf eucl_sup sup_inf_distrib1 intro!: euclidean_eqI)
+
+subclass conditionally_complete_lattice
+proof
+  fix z::'a and X::"'a set"
+  assume "X \<noteq> {}"
+  hence "\<And>i. (\<lambda>x. x \<bullet> i) ` X \<noteq> {}" by simp
+  thus "(\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> z \<le> Inf X" "(\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup X \<le> z"
+    by (auto simp: eucl_Inf eucl_Sup eucl_le Inf_class.INF_def Sup_class.SUP_def
+      intro!: cInf_greatest cSup_least)
+qed (force intro!: cInf_lower cSup_upper
+      simp: bdd_below_def bdd_above_def preorder_class.bdd_below_def preorder_class.bdd_above_def
+        eucl_Inf eucl_Sup eucl_le Inf_class.INF_def Sup_class.SUP_def)+
+
+lemma inner_Basis_inf_left: "i \<in> Basis \<Longrightarrow> inf x y \<bullet> i = inf (x \<bullet> i) (y \<bullet> i)"
+  and inner_Basis_sup_left: "i \<in> Basis \<Longrightarrow> sup x y \<bullet> i = sup (x \<bullet> i) (y \<bullet> i)"
+  by (simp_all add: eucl_inf eucl_sup inner_setsum_left inner_Basis if_distrib setsum_delta
+      cong: if_cong)
+
+lemma inner_Basis_INF_left: "i \<in> Basis \<Longrightarrow> (INF x:X. f x) \<bullet> i = (INF x:X. f x \<bullet> i)"
+  and inner_Basis_SUP_left: "i \<in> Basis \<Longrightarrow> (SUP x:X. f x) \<bullet> i = (SUP x:X. f x \<bullet> i)"
+  by (simp_all add: INF_def SUP_def eucl_Sup eucl_Inf)
+
+lemma abs_inner: "i \<in> Basis \<Longrightarrow> abs x \<bullet> i = abs (x \<bullet> i)"
+  by (auto simp: eucl_abs)
+
+lemma
+  abs_scaleR: "\<bar>a *\<^sub>R b\<bar> = \<bar>a\<bar> *\<^sub>R \<bar>b\<bar>"
+  by (auto simp: eucl_abs abs_mult intro!: euclidean_eqI)
+
+lemma interval_inner_leI:
+  assumes "x \<in> {a .. b}" "0 \<le> i"
+  shows "a\<bullet>i \<le> x\<bullet>i" "x\<bullet>i \<le> b\<bullet>i"
+  using assms
+  unfolding euclidean_inner[of a i] euclidean_inner[of x i] euclidean_inner[of b i]
+  by (auto intro!: setsum_mono mult_right_mono simp: eucl_le)
+
+lemma inner_nonneg_nonneg:
+  shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a \<bullet> b"
+  using interval_inner_leI[of a 0 a b]
+  by auto
+
+lemma inner_Basis_mono:
+  shows "a \<le> b \<Longrightarrow> c \<in> Basis  \<Longrightarrow> a \<bullet> c \<le> b \<bullet> c"
+  by (simp add: eucl_le)
+
+lemma Basis_nonneg[intro, simp]: "i \<in> Basis \<Longrightarrow> 0 \<le> i"
+  by (auto simp: eucl_le inner_Basis)
+
+end
+
+lemma (in order) atLeastatMost_empty'[simp]:
+  "(~ a <= b) \<Longrightarrow> {a..b} = {}"
+  by (auto)
 
 instance real :: ordered_euclidean_space
-  by default auto
-
-instantiation prod :: (ordered_euclidean_space, ordered_euclidean_space) ordered_euclidean_space
+  by default (auto simp: INF_def SUP_def)
+
+lemma in_Basis_prod_iff:
+  fixes i::"'a::euclidean_space*'b::euclidean_space"
+  shows "i \<in> Basis \<longleftrightarrow> fst i = 0 \<and> snd i \<in> Basis \<or> snd i = 0 \<and> fst i \<in> Basis"
+  by (cases i) (auto simp: Basis_prod_def)
+
+instantiation prod::(abs, abs) abs
 begin
 
-definition "x \<le> (y::('a\<times>'b)) \<longleftrightarrow> (\<forall>i\<in>Basis. x \<bullet> i \<le> y \<bullet> i)"
-definition "x < (y::('a\<times>'b)) \<longleftrightarrow> (\<forall>i\<in>Basis. x \<bullet> i < y \<bullet> i)"
-
-instance
-  by default (auto simp: less_prod_def less_eq_prod_def)
+definition "abs x = (abs (fst x), abs (snd x))"
+
+instance proof qed
+end
+
+instance prod :: (ordered_euclidean_space, ordered_euclidean_space) ordered_euclidean_space
+  by default
+    (auto intro!: add_mono simp add: euclidean_representation_setsum'  Ball_def inner_prod_def
+      in_Basis_prod_iff inner_Basis_inf_left inner_Basis_sup_left inner_Basis_INF_left Inf_prod_def
+      inner_Basis_SUP_left Sup_prod_def less_prod_def less_eq_prod_def eucl_le[where 'a='a]
+      eucl_le[where 'a='b] abs_prod_def abs_inner)
 
 end
 
-end

--- a/src/HOL/Probability/Radon_Nikodym.thy	Mon Dec 16 17:08:22 2013 +0100
+++ b/src/HOL/Probability/Radon_Nikodym.thy	Mon Dec 16 17:08:22 2013 +0100
@@ -686,7 +686,7 @@
   from choice[OF this[unfolded Bex_def]]
   obtain f where borel: "\<And>i. f i \<in> borel_measurable M" "\<And>i x. 0 \<le> f i x"
     and f_density: "\<And>i. density (?M i) (f i) = ?N i"
-    by auto
+    by force
   { fix A i assume A: "A \<in> sets M"
     with Q borel have "(\<integral>\<^sup>+x. f i x * indicator (Q i \<inter> A) x \<partial>M) = emeasure (density (?M i) (f i)) A"
       by (auto simp add: emeasure_density positive_integral_density subset_eq