diff -r bdaa1582dc8b -r baefa3b461c2 src/HOL/Probability/Borel_Space.thy
--- a/src/HOL/Probability/Borel_Space.thy	Wed Apr 10 17:49:16 2013 +0200
+++ b/src/HOL/Probability/Borel_Space.thy	Wed Apr 10 18:51:21 2013 +0200
@@ -136,13 +136,8 @@
   interpret countable_basis using assms by unfold_locales
   fix X::"'a set" assume "open X"
   from open_countable_basisE[OF this] guess B' . note B' = this
-  show "X \<in> sigma_sets UNIV B"
-  proof cases
-    assume "B' \<noteq> {}"
-    thus "X \<in> sigma_sets UNIV B" using assms B'
-      by (metis from_nat_into Union_image_eq countable_subset range_from_nat_into
-        in_mono sigma_sets.Basic sigma_sets.Union)
-  qed (simp add: sigma_sets.Empty B')
+  then show "X \<in> sigma_sets UNIV B"
+    by (blast intro: sigma_sets_UNION `countable B` countable_subset)
 next
   fix b assume "b \<in> B"
   hence "open b" by (rule topological_basis_open[OF assms(2)])
@@ -206,22 +201,6 @@
   using measurable_comp[OF g borel_measurable_continuous_on_open'[OF cont], of c]
   by (simp add: comp_def)
 
-lemma continuous_on_fst: "continuous_on UNIV fst"
-proof -
-  have [simp]: "range fst = UNIV" by (auto simp: image_iff)
-  show ?thesis
-    using closed_vimage_fst
-    by (auto simp: continuous_on_closed closed_closedin vimage_def)
-qed
-
-lemma continuous_on_snd: "continuous_on UNIV snd"
-proof -
-  have [simp]: "range snd = UNIV" by (auto simp: image_iff)
-  show ?thesis
-    using closed_vimage_snd
-    by (auto simp: continuous_on_closed closed_closedin vimage_def)
-qed
-
 lemma borel_measurable_continuous_Pair:
   fixes f :: "'a \<Rightarrow> 'b::second_countable_topology" and g :: "'a \<Rightarrow> 'c::second_countable_topology"
   assumes [measurable]: "f \<in> borel_measurable M"
@@ -242,11 +221,10 @@
   assumes "g \<in> borel_measurable M"
   shows "(\<lambda>x. f x \<bullet> g x) \<in> borel_measurable M"
   using assms
-  by (rule borel_measurable_continuous_Pair)
-     (intro continuous_on_inner continuous_on_snd continuous_on_fst)
+  by (rule borel_measurable_continuous_Pair) (intro continuous_on_intros)
 
 lemma [measurable]:
-  fixes a b :: "'a\<Colon>ordered_euclidean_space"
+  fixes a b :: "'a\<Colon>linorder_topology"
   shows lessThan_borel: "{..< a} \<in> sets borel"
     and greaterThan_borel: "{a <..} \<in> sets borel"
     and greaterThanLessThan_borel: "{a<..<b} \<in> sets borel"
@@ -256,22 +234,58 @@
     and greaterThanAtMost_borel: "{a<..b} \<in> sets borel"
     and atLeastLessThan_borel: "{a..<b} \<in> sets borel"
   unfolding greaterThanAtMost_def atLeastLessThan_def
+  by (blast intro: borel_open borel_closed open_lessThan open_greaterThan open_greaterThanLessThan
+                   closed_atMost closed_atLeast closed_atLeastAtMost)+
+
+lemma eucl_ivals[measurable]:
+  fixes a b :: "'a\<Colon>ordered_euclidean_space"
+  shows "{..< a} \<in> sets borel"
+    and "{a <..} \<in> sets borel"
+    and "{a<..<b} \<in> sets borel"
+    and "{..a} \<in> sets borel"
+    and "{a..} \<in> sets borel"
+    and "{a..b} \<in> sets borel"
+    and  "{a<..b} \<in> sets borel"
+    and "{a..<b} \<in> sets borel"
+  unfolding greaterThanAtMost_def atLeastLessThan_def
   by (blast intro: borel_open borel_closed)+
 
+lemma open_Collect_less:
+  fixes f g :: "'i::topological_space \<Rightarrow> 'a :: {inner_dense_linorder, linorder_topology}"
+  assumes "continuous_on UNIV f"
+  assumes "continuous_on UNIV g"
+  shows "open {x. f x < g x}"
+proof -
+  have "open (\<Union>y. {x \<in> UNIV. f x \<in> {..< y}} \<inter> {x \<in> UNIV. g x \<in> {y <..}})" (is "open ?X")
+    by (intro open_UN ballI open_Int continuous_open_preimage assms) auto
+  also have "?X = {x. f x < g x}"
+    by (auto intro: dense)
+  finally show ?thesis .
+qed
+
+lemma closed_Collect_le:
+  fixes f g :: "'i::topological_space \<Rightarrow> 'a :: {inner_dense_linorder, linorder_topology}"
+  assumes f: "continuous_on UNIV f"
+  assumes g: "continuous_on UNIV g"
+  shows "closed {x. f x \<le> g x}"
+  using open_Collect_less[OF g f] unfolding not_less[symmetric] Collect_neg_eq open_closed .
+
 lemma borel_measurable_less[measurable]:
-  fixes f :: "'a \<Rightarrow> real"
-  assumes f: "f \<in> borel_measurable M"
-  assumes g: "g \<in> borel_measurable M"
+  fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, inner_dense_linorder, linorder_topology}"
+  assumes "f \<in> borel_measurable M"
+  assumes "g \<in> borel_measurable M"
   shows "{w \<in> space M. f w < g w} \<in> sets M"
 proof -
-  have "{w \<in> space M. f w < g w} = {x \<in> space M. \<exists>r. f x < of_rat r \<and> of_rat r < g x}"
-    using Rats_dense_in_real by (auto simp add: Rats_def)
-  with f g show ?thesis
-    by simp
+  have "{w \<in> space M. f w < g w} = (\<lambda>x. (f x, g x)) -` {x. fst x < snd x} \<inter> space M"
+    by auto
+  also have "\<dots> \<in> sets M"
+    by (intro measurable_sets[OF borel_measurable_Pair borel_open, OF assms open_Collect_less]
+              continuous_on_intros)
+  finally show ?thesis .
 qed
 
 lemma
-  fixes f :: "'a \<Rightarrow> real"
+  fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, inner_dense_linorder, linorder_topology}"
   assumes f[measurable]: "f \<in> borel_measurable M"
   assumes g[measurable]: "g \<in> borel_measurable M"
   shows borel_measurable_le[measurable]: "{w \<in> space M. f w \<le> g w} \<in> sets M"
@@ -281,10 +295,11 @@
   by measurable
 
 lemma 
-  shows hafspace_less_borel: "{x::'a::euclidean_space. a < x \<bullet> i} \<in> sets borel"
-    and hafspace_greater_borel: "{x::'a::euclidean_space. x \<bullet> i < a} \<in> sets borel"
-    and hafspace_less_eq_borel: "{x::'a::euclidean_space. a \<le> x \<bullet> i} \<in> sets borel"
-    and hafspace_greater_eq_borel: "{x::'a::euclidean_space. x \<bullet> i \<le> a} \<in> sets borel"
+  fixes i :: "'a::{second_countable_topology, real_inner}"
+  shows hafspace_less_borel: "{x. a < x \<bullet> i} \<in> sets borel"
+    and hafspace_greater_borel: "{x. x \<bullet> i < a} \<in> sets borel"
+    and hafspace_less_eq_borel: "{x. a \<le> x \<bullet> i} \<in> sets borel"
+    and hafspace_greater_eq_borel: "{x. x \<bullet> i \<le> a} \<in> sets borel"
   by simp_all
 
 subsection "Borel space equals sigma algebras over intervals"
@@ -636,22 +651,20 @@
 subsection "Borel measurable operators"
 
 lemma borel_measurable_uminus[measurable (raw)]:
-  fixes g :: "'a \<Rightarrow> real"
+  fixes g :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_vector}"
   assumes g: "g \<in> borel_measurable M"
   shows "(\<lambda>x. - g x) \<in> borel_measurable M"
-  by (rule borel_measurable_continuous_on[OF _ g]) (auto intro: continuous_on_minus continuous_on_id)
+  by (rule borel_measurable_continuous_on[OF _ g]) (intro continuous_on_intros)
 
 lemma borel_measurable_add[measurable (raw)]:
-  fixes f g :: "'a \<Rightarrow> 'c::ordered_euclidean_space"
+  fixes f g :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_vector}"
   assumes f: "f \<in> borel_measurable M"
   assumes g: "g \<in> borel_measurable M"
   shows "(\<lambda>x. f x + g x) \<in> borel_measurable M"
-  using f g
-  by (rule borel_measurable_continuous_Pair)
-     (auto intro: continuous_on_fst continuous_on_snd continuous_on_add)
+  using f g by (rule borel_measurable_continuous_Pair) (intro continuous_on_intros)
 
 lemma borel_measurable_setsum[measurable (raw)]:
-  fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> real"
+  fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> 'b::{second_countable_topology, real_normed_vector}"
   assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
   shows "(\<lambda>x. \<Sum>i\<in>S. f i x) \<in> borel_measurable M"
 proof cases
@@ -660,37 +673,41 @@
 qed simp
 
 lemma borel_measurable_diff[measurable (raw)]:
-  fixes f :: "'a \<Rightarrow> real"
+  fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_vector}"
   assumes f: "f \<in> borel_measurable M"
   assumes g: "g \<in> borel_measurable M"
   shows "(\<lambda>x. f x - g x) \<in> borel_measurable M"
   unfolding diff_minus using assms by simp
 
 lemma borel_measurable_times[measurable (raw)]:
-  fixes f :: "'a \<Rightarrow> real"
+  fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_algebra}"
   assumes f: "f \<in> borel_measurable M"
   assumes g: "g \<in> borel_measurable M"
   shows "(\<lambda>x. f x * g x) \<in> borel_measurable M"
-  using f g
-  by (rule borel_measurable_continuous_Pair)
-     (auto intro: continuous_on_fst continuous_on_snd continuous_on_mult)
+  using f g by (rule borel_measurable_continuous_Pair) (intro continuous_on_intros)
+
+lemma borel_measurable_setprod[measurable (raw)]:
+  fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> 'b::{second_countable_topology, real_normed_field}"
+  assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
+  shows "(\<lambda>x. \<Prod>i\<in>S. f i x) \<in> borel_measurable M"
+proof cases
+  assume "finite S"
+  thus ?thesis using assms by induct auto
+qed simp
 
 lemma borel_measurable_dist[measurable (raw)]:
-  fixes g f :: "'a \<Rightarrow> 'b::ordered_euclidean_space"
+  fixes g f :: "'a \<Rightarrow> 'b::{second_countable_topology, metric_space}"
   assumes f: "f \<in> borel_measurable M"
   assumes g: "g \<in> borel_measurable M"
   shows "(\<lambda>x. dist (f x) (g x)) \<in> borel_measurable M"
-  using f g
-  by (rule borel_measurable_continuous_Pair)
-     (intro continuous_on_dist continuous_on_fst continuous_on_snd)
+  using f g by (rule borel_measurable_continuous_Pair) (intro continuous_on_intros)
   
 lemma borel_measurable_scaleR[measurable (raw)]:
-  fixes g :: "'a \<Rightarrow> 'b::ordered_euclidean_space"
+  fixes g :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_vector}"
   assumes f: "f \<in> borel_measurable M"
   assumes g: "g \<in> borel_measurable M"
   shows "(\<lambda>x. f x *\<^sub>R g x) \<in> borel_measurable M"
-  by (rule borel_measurable_continuous_Pair[OF f g])
-     (auto intro!: continuous_on_scaleR continuous_on_fst continuous_on_snd)
+  using f g by (rule borel_measurable_continuous_Pair) (intro continuous_on_intros)
 
 lemma affine_borel_measurable_vector:
   fixes f :: "'a \<Rightarrow> 'x::real_normed_vector"
@@ -720,36 +737,29 @@
   "f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. a + f x ::'a::real_normed_vector) \<in> borel_measurable M"
   using affine_borel_measurable_vector[of f M a 1] by simp
 
-lemma borel_measurable_setprod[measurable (raw)]:
-  fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> real"
-  assumes "\<And>i. i \<in> S \<Longrightarrow> f i \<in> borel_measurable M"
-  shows "(\<lambda>x. \<Prod>i\<in>S. f i x) \<in> borel_measurable M"
-proof cases
-  assume "finite S"
-  thus ?thesis using assms by induct auto
-qed simp
-
 lemma borel_measurable_inverse[measurable (raw)]:
-  fixes f :: "'a \<Rightarrow> real"
+  fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_div_algebra}"
   assumes f: "f \<in> borel_measurable M"
   shows "(\<lambda>x. inverse (f x)) \<in> borel_measurable M"
 proof -
-  have "(\<lambda>x::real. if x \<in> UNIV - {0} then inverse x else 0) \<in> borel_measurable borel"
-    by (intro borel_measurable_continuous_on_open' continuous_on_inverse continuous_on_id) auto
-  also have "(\<lambda>x::real. if x \<in> UNIV - {0} then inverse x else 0) = inverse" by (intro ext) auto
+  have "(\<lambda>x::'b. if x \<in> UNIV - {0} then inverse x else inverse 0) \<in> borel_measurable borel"
+    by (intro borel_measurable_continuous_on_open' continuous_on_intros) auto
+  also have "(\<lambda>x::'b. if x \<in> UNIV - {0} then inverse x else inverse 0) = inverse"
+    by (intro ext) auto
   finally show ?thesis using f by simp
 qed
 
 lemma borel_measurable_divide[measurable (raw)]:
-  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. f x / g x::real) \<in> borel_measurable M"
+  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow>
+    (\<lambda>x. f x / g x::'b::{second_countable_topology, real_normed_field}) \<in> borel_measurable M"
   by (simp add: field_divide_inverse)
 
 lemma borel_measurable_max[measurable (raw)]:
-  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. max (g x) (f x) :: real) \<in> borel_measurable M"
+  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. max (g x) (f x) :: 'b::{second_countable_topology, inner_dense_linorder, linorder_topology}) \<in> borel_measurable M"
   by (simp add: max_def)
 
 lemma borel_measurable_min[measurable (raw)]:
-  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. min (g x) (f x) :: real) \<in> borel_measurable M"
+  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. min (g x) (f x) :: 'b::{second_countable_topology, inner_dense_linorder, linorder_topology}) \<in> borel_measurable M"
   by (simp add: min_def)
 
 lemma borel_measurable_abs[measurable (raw)]:
@@ -761,15 +771,15 @@
   by (simp add: cart_eq_inner_axis)
 
 lemma convex_measurable:
-  fixes a b :: real
-  assumes X: "X \<in> borel_measurable M" "X ` space M \<subseteq> { a <..< b}"
-  assumes q: "convex_on { a <..< b} q"
+  fixes A :: "'a :: ordered_euclidean_space set"
+  assumes X: "X \<in> borel_measurable M" "X ` space M \<subseteq> A" "open A"
+  assumes q: "convex_on A q"
   shows "(\<lambda>x. q (X x)) \<in> borel_measurable M"
 proof -
-  have "(\<lambda>x. if X x \<in> {a <..< b} then q (X x) else 0) \<in> borel_measurable M" (is "?qX")
+  have "(\<lambda>x. if X x \<in> A then q (X x) else 0) \<in> borel_measurable M" (is "?qX")
   proof (rule borel_measurable_continuous_on_open[OF _ _ X(1)])
-    show "open {a<..<b}" by auto
-    from this q show "continuous_on {a<..<b} q"
+    show "open A" by fact
+    from this q show "continuous_on A q"
       by (rule convex_on_continuous)
   qed
   also have "?qX \<longleftrightarrow> (\<lambda>x. q (X x)) \<in> borel_measurable M"
@@ -904,19 +914,6 @@
     by (subst *) (simp del: space_borel split del: split_if)
 qed
 
-lemma [measurable]:
-  fixes f g :: "'a \<Rightarrow> ereal"
-  assumes f: "f \<in> borel_measurable M"
-  assumes g: "g \<in> borel_measurable M"
-  shows borel_measurable_ereal_le: "{x \<in> space M. f x \<le> g x} \<in> sets M"
-    and borel_measurable_ereal_less: "{x \<in> space M. f x < g x} \<in> sets M"
-    and borel_measurable_ereal_eq: "{w \<in> space M. f w = g w} \<in> sets M"
-  using f g by (simp_all add: set_Collect_ereal2)
-
-lemma borel_measurable_ereal_neq:
-  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> {w \<in> space M. f w \<noteq> (g w :: ereal)} \<in> sets M"
-  by simp
-
 lemma borel_measurable_ereal_iff:
   shows "(\<lambda>x. ereal (f x)) \<in> borel_measurable M \<longleftrightarrow> f \<in> borel_measurable M"
 proof
@@ -1197,4 +1194,4 @@
   shows "(\<lambda>x. suminf (\<lambda>i. f i x)) \<in> borel_measurable M"
   unfolding suminf_def sums_def[abs_def] lim_def[symmetric] by simp
 
-end 
+end