# HG changeset patch
# User hoelzl
# Date 1454997888 -3600
# Node ID 4fe872ff91bfa0d4b5026adb751703c8c3e128e5
# Parent  7c288c0c7300c14307e571dbe7638a3eecb98da2
Borel_Space.borel is now in the type class locale

diff -r 7c288c0c7300 -r 4fe872ff91bf src/HOL/Library/Countable_Set_Type.thy
--- a/src/HOL/Library/Countable_Set_Type.thy	Tue Feb 09 07:04:32 2016 +0100
+++ b/src/HOL/Library/Countable_Set_Type.thy	Tue Feb 09 07:04:48 2016 +0100
@@ -472,7 +472,8 @@
 
 lemma cUnion_parametric [transfer_rule]:
   "(rel_cset (rel_cset A) ===> rel_cset A) cUnion cUnion"
-  unfolding rel_fun_def by transfer(simp, fast dest: rel_setD1 rel_setD2 intro!: rel_setI)
+  unfolding rel_fun_def
+  by transfer (auto simp: rel_set_def, metis+)
 
 lemma cimage_parametric [transfer_rule]:
   "((A ===> B) ===> rel_cset A ===> rel_cset B) cimage cimage"
diff -r 7c288c0c7300 -r 4fe872ff91bf src/HOL/Probability/Borel_Space.thy
--- a/src/HOL/Probability/Borel_Space.thy	Tue Feb 09 07:04:32 2016 +0100
+++ b/src/HOL/Probability/Borel_Space.thy	Tue Feb 09 07:04:48 2016 +0100
@@ -19,7 +19,7 @@
   have "{A \<times> B :: ('a \<times> 'b) set | A B. open A \<and> open B} = ((\<lambda>(a, b). a \<times> b) ` ({A. open A} \<times> {A. open A}))"
     by auto
   then show ?thesis
-    by (auto intro: topological_basis_prod topological_basis_trivial topological_basis_imp_subbasis)  
+    by (auto intro: topological_basis_prod topological_basis_trivial topological_basis_imp_subbasis)
 qed
 
 definition "mono_on f A \<equiv> \<forall>r s. r \<in> A \<and> s \<in> A \<and> r \<le> s \<longrightarrow> f r \<le> f s"
@@ -76,7 +76,7 @@
   fix x y assume "x \<in> A" "y \<in> A" "f x = f y"
   thus "x = y"
     by (cases x y rule: linorder_cases)
-       (auto dest: strict_mono_onD[OF assms, of x y] strict_mono_onD[OF assms, of y x]) 
+       (auto dest: strict_mono_onD[OF assms, of x y] strict_mono_onD[OF assms, of y x])
 qed
 
 lemma strict_mono_on_leD:
@@ -121,7 +121,7 @@
   qed
 qed simp
 
-lemma strict_mono_on_imp_mono_on: 
+lemma strict_mono_on_imp_mono_on:
   "strict_mono_on (f :: (_ :: linorder) \<Rightarrow> _ :: preorder) A \<Longrightarrow> mono_on f A"
   by (rule mono_onI, rule strict_mono_on_leD)
 
@@ -153,7 +153,7 @@
           apply (auto simp add: dist_real_def not_less)
           apply (subgoal_tac "f x \<le> f xa")
           by (auto intro: mono)
-      qed 
+      qed
       thus ?thesis by auto
     next
       fix u assume "u > f a"
@@ -167,11 +167,11 @@
           apply (auto simp add: dist_real_def)
           apply (subgoal_tac "f x \<ge> f xa")
           by (auto intro: mono)
-      qed 
+      qed
       thus ?thesis by auto
     qed
   qed
-  hence "\<exists>g :: real \<Rightarrow> nat \<times> rat . \<forall>a \<in> {a\<in>A. \<not> continuous (at a within A) f}. 
+  hence "\<exists>g :: real \<Rightarrow> nat \<times> rat . \<forall>a \<in> {a\<in>A. \<not> continuous (at a within A) f}.
       (fst (g a) = 0 \<and> of_rat (snd (g a)) < f a \<and> (\<forall>x \<in> A. x < a \<longrightarrow> f x < of_rat (snd (g a)))) |
       (fst (g a) = 1 \<and> of_rat (snd (g a)) > f a \<and> (\<forall>x \<in> A. x > a \<longrightarrow> f x > of_rat (snd (g a))))"
     by (rule bchoice)
@@ -186,11 +186,11 @@
     assume 1: "w \<in> A" and 2: "\<not> continuous (at w within A) f" and
            3: "z \<in> A" and 4: "\<not> continuous (at z within A) f" and
            5: "g w = g z"
-    from g [OF 1 2 3] g [OF 3 4 1] 5 
+    from g [OF 1 2 3] g [OF 3 4 1] 5
     show "w = z" by auto
   qed
-  thus ?thesis 
-    by (rule countableI') 
+  thus ?thesis
+    by (rule countableI')
 qed
 
 lemma mono_on_ctble_discont_open:
@@ -226,7 +226,7 @@
   assumes "S \<noteq> {}" "bdd_above S"
   shows "Sup S \<in> closure S"
 proof-
-  have "Inf (uminus ` S) \<in> closure (uminus ` S)" 
+  have "Inf (uminus ` S) \<in> closure (uminus ` S)"
       using assms by (intro closure_contains_Inf) auto
   also have "Inf (uminus ` S) = -Sup S" by (simp add: Inf_real_def)
   also have "closure (uminus ` S) = uminus ` closure S"
@@ -247,7 +247,7 @@
 proof (cases "a < b")
   assume "a < b"
   from deriv have "\<forall>x. x \<ge> a \<and> x \<le> b \<longrightarrow> (g has_real_derivative g' x) (at x)" by simp
-  from MVT2[OF \<open>a < b\<close> this] and deriv 
+  from MVT2[OF \<open>a < b\<close> this] and deriv
     obtain \<xi> where \<xi>_ab: "\<xi> > a" "\<xi> < b" and g_ab: "g b - g a = (b - a) * g' \<xi>" by blast
   from \<xi>_ab ab nonneg have "(b - a) * g' \<xi> \<ge> 0" by simp
   with g_ab show ?thesis by simp
@@ -259,22 +259,22 @@
   obtains c' d' where "{a..b} \<inter> g -` {c..d} = {c'..d'}" "c' \<le> d'" "g c' = c" "g d' = d"
 proof-
     let ?A = "{a..b} \<inter> g -` {c..d}"
-    from IVT'[of g a c b, OF _ _ \<open>a \<le> b\<close> assms(1)] assms(4,5) 
+    from IVT'[of g a c b, OF _ _ \<open>a \<le> b\<close> assms(1)] assms(4,5)
          obtain c'' where c'': "c'' \<in> ?A" "g c'' = c" by auto
-    from IVT'[of g a d b, OF _ _ \<open>a \<le> b\<close> assms(1)] assms(4,5) 
+    from IVT'[of g a d b, OF _ _ \<open>a \<le> b\<close> assms(1)] assms(4,5)
          obtain d'' where d'': "d'' \<in> ?A" "g d'' = d" by auto
     hence [simp]: "?A \<noteq> {}" by blast
 
     def c' \<equiv> "Inf ?A" and d' \<equiv> "Sup ?A"
     have "?A \<subseteq> {c'..d'}" unfolding c'_def d'_def
         by (intro subsetI) (auto intro: cInf_lower cSup_upper)
-    moreover from assms have "closed ?A" 
+    moreover from assms have "closed ?A"
         using continuous_on_closed_vimage[of "{a..b}" g] by (subst Int_commute) simp
     hence c'd'_in_set: "c' \<in> ?A" "d' \<in> ?A" unfolding c'_def d'_def
         by ((intro closed_contains_Inf closed_contains_Sup, simp_all)[])+
-    hence "{c'..d'} \<subseteq> ?A" using assms 
+    hence "{c'..d'} \<subseteq> ?A" using assms
         by (intro subsetI)
-           (auto intro!: order_trans[of c "g c'" "g x" for x] order_trans[of "g x" "g d'" d for x] 
+           (auto intro!: order_trans[of c "g c'" "g x" for x] order_trans[of "g x" "g d'" d for x]
                  intro!: mono)
     moreover have "c' \<le> d'" using c'd'_in_set(2) unfolding c'_def by (intro cInf_lower) auto
     moreover have "g c' \<le> c" "g d' \<ge> d"
@@ -290,7 +290,7 @@
 
 subsection \<open>Generic Borel spaces\<close>
 
-definition borel :: "'a::topological_space measure" where
+definition (in topological_space) borel :: "'a measure" where
   "borel = sigma UNIV {S. open S}"
 
 abbreviation "borel_measurable M \<equiv> measurable M borel"
@@ -798,7 +798,7 @@
   unfolding eq_iff not_less[symmetric]
   by measurable
 
-lemma 
+lemma
   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"
@@ -881,7 +881,7 @@
 
 lemma halfspace_gt_in_halfspace:
   assumes i: "i \<in> A"
-  shows "{x::'a. a < x \<bullet> i} \<in> 
+  shows "{x::'a. a < x \<bullet> i} \<in>
     sigma_sets UNIV ((\<lambda> (a, i). {x::'a::euclidean_space. x \<bullet> i < a}) ` (UNIV \<times> A))"
   (is "?set \<in> ?SIGMA")
 proof -
@@ -1063,7 +1063,7 @@
   have "{..i} = (\<Union>j::nat. {-j <.. i})"
     by (auto simp: minus_less_iff reals_Archimedean2)
   also have "\<dots> \<in> sets (sigma UNIV (range (\<lambda>(i, j). {i<..j})))"
-    by (intro sets.countable_nat_UN) auto 
+    by (intro sets.countable_nat_UN) auto
   finally show "{..i} \<in> sets (sigma UNIV (range (\<lambda>(i, j). {i<..j})))" .
 qed simp
 
@@ -1100,7 +1100,7 @@
 lemma borel_measurable_halfspacesI:
   fixes f :: "'a \<Rightarrow> 'c::euclidean_space"
   assumes F: "borel = sigma UNIV (F ` (UNIV \<times> Basis))"
-  and S_eq: "\<And>a i. S a i = f -` F (a,i) \<inter> space M" 
+  and S_eq: "\<And>a i. S a i = f -` F (a,i) \<inter> space M"
   shows "f \<in> borel_measurable M = (\<forall>i\<in>Basis. \<forall>a::real. S a i \<in> sets M)"
 proof safe
   fix a :: real and i :: 'b assume i: "i \<in> Basis" and f: "f \<in> borel_measurable M"
@@ -1159,16 +1159,16 @@
 qed auto
 
 lemma borel_set_induct[consumes 1, case_names empty interval compl union]:
-  assumes "A \<in> sets borel" 
+  assumes "A \<in> sets borel"
   assumes empty: "P {}" and int: "\<And>a b. a \<le> b \<Longrightarrow> P {a..b}" and compl: "\<And>A. A \<in> sets borel \<Longrightarrow> P A \<Longrightarrow> P (-A)" and
           un: "\<And>f. disjoint_family f \<Longrightarrow> (\<And>i. f i \<in> sets borel) \<Longrightarrow>  (\<And>i. P (f i)) \<Longrightarrow> P (\<Union>i::nat. f i)"
   shows "P (A::real set)"
 proof-
   let ?G = "range (\<lambda>(a,b). {a..b::real})"
-  have "Int_stable ?G" "?G \<subseteq> Pow UNIV" "A \<in> sigma_sets UNIV ?G" 
+  have "Int_stable ?G" "?G \<subseteq> Pow UNIV" "A \<in> sigma_sets UNIV ?G"
       using assms(1) by (auto simp add: borel_eq_atLeastAtMost Int_stable_def)
   thus ?thesis
-  proof (induction rule: sigma_sets_induct_disjoint) 
+  proof (induction rule: sigma_sets_induct_disjoint)
     case (union f)
       from union.hyps(2) have "\<And>i. f i \<in> sets borel" by (auto simp: borel_eq_atLeastAtMost)
       with union show ?case by (auto intro: un)
@@ -1240,7 +1240,7 @@
   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_intros)
-  
+
 lemma borel_measurable_scaleR[measurable (raw)]:
   fixes g :: "'a \<Rightarrow> 'b::{second_countable_topology, real_normed_vector}"
   assumes f: "f \<in> borel_measurable M"
@@ -1323,7 +1323,7 @@
 
 lemma convex_measurable:
   fixes A :: "'a :: euclidean_space set"
-  shows "X \<in> borel_measurable M \<Longrightarrow> X ` space M \<subseteq> A \<Longrightarrow> open A \<Longrightarrow> convex_on A q \<Longrightarrow> 
+  shows "X \<in> borel_measurable M \<Longrightarrow> X ` space M \<subseteq> A \<Longrightarrow> open A \<Longrightarrow> convex_on A q \<Longrightarrow>
     (\<lambda>x. q (X x)) \<in> borel_measurable M"
   by (rule measurable_compose[where f=X and N="restrict_space borel A"])
      (auto intro!: borel_measurable_continuous_on_restrict convex_on_continuous measurable_restrict_space2)
@@ -1406,7 +1406,7 @@
   using continuous_on_ereal f by (rule borel_measurable_continuous_on) (rule continuous_on_id)
 
 lemma borel_measurable_real_of_ereal[measurable (raw)]:
-  fixes f :: "'a \<Rightarrow> ereal" 
+  fixes f :: "'a \<Rightarrow> ereal"
   assumes f: "f \<in> borel_measurable M"
   shows "(\<lambda>x. real_of_ereal (f x)) \<in> borel_measurable M"
   apply (rule measurable_compose[OF f])
@@ -1415,7 +1415,7 @@
   done
 
 lemma borel_measurable_ereal_cases:
-  fixes f :: "'a \<Rightarrow> ereal" 
+  fixes f :: "'a \<Rightarrow> ereal"
   assumes f: "f \<in> borel_measurable M"
   assumes H: "(\<lambda>x. H (ereal (real_of_ereal (f x)))) \<in> borel_measurable M"
   shows "(\<lambda>x. H (f x)) \<in> borel_measurable M"
@@ -1439,7 +1439,7 @@
 qed auto
 
 lemma set_Collect_ereal2:
-  fixes f g :: "'a \<Rightarrow> ereal" 
+  fixes f g :: "'a \<Rightarrow> ereal"
   assumes f: "f \<in> borel_measurable M"
   assumes g: "g \<in> borel_measurable M"
   assumes H: "{x \<in> space M. H (ereal (real_of_ereal (f x))) (ereal (real_of_ereal (g x)))} \<in> sets M"
@@ -1510,7 +1510,7 @@
   unfolding borel_measurable_ereal_iff_Iio vimage_sets_compl_iff[where A="{..< a}" for a] by simp
 
 lemma borel_measurable_ereal2:
-  fixes f g :: "'a \<Rightarrow> ereal" 
+  fixes f g :: "'a \<Rightarrow> ereal"
   assumes f: "f \<in> borel_measurable M"
   assumes g: "g \<in> borel_measurable M"
   assumes H: "(\<lambda>x. H (ereal (real_of_ereal (f x))) (ereal (real_of_ereal (g x)))) \<in> borel_measurable M"
@@ -1573,7 +1573,7 @@
   "(\<And>i. {x\<in>space M. P x i} \<in> sets M) \<Longrightarrow> {x\<in>space M. eventually (P x) sequentially} \<in> sets M"
   unfolding eventually_sequentially by simp
 
-lemma sets_Collect_ereal_convergent[measurable]: 
+lemma sets_Collect_ereal_convergent[measurable]:
   fixes f :: "nat \<Rightarrow> 'a => ereal"
   assumes f[measurable]: "\<And>i. f i \<in> borel_measurable M"
   shows "{x\<in>space M. convergent (\<lambda>i. f i x)} \<in> sets M"
@@ -1629,7 +1629,7 @@
   shows "g \<in> borel_measurable M"
   unfolding borel_eq_closed
 proof (safe intro!: measurable_measure_of)
-  fix A :: "'b set" assume "closed A" 
+  fix A :: "'b set" assume "closed A"
 
   have [measurable]: "(\<lambda>x. infdist (g x) A) \<in> borel_measurable M"
   proof (rule borel_measurable_LIMSEQ)
@@ -1653,7 +1653,7 @@
   qed simp
 qed auto
 
-lemma sets_Collect_Cauchy[measurable]: 
+lemma sets_Collect_Cauchy[measurable]:
   fixes f :: "nat \<Rightarrow> 'a => 'b::{metric_space, second_countable_topology}"
   assumes f[measurable]: "\<And>i. f i \<in> borel_measurable M"
   shows "{x\<in>space M. Cauchy (\<lambda>i. f i x)} \<in> sets M"
@@ -1674,7 +1674,7 @@
       by (cases "Cauchy (\<lambda>i. f i x)")
          (auto simp add: convergent_eq_cauchy[symmetric] convergent_def)
     then show "(\<lambda>i. if Cauchy (\<lambda>i. f i x) then f i x else 0) \<longlonglongrightarrow> u' x"
-      unfolding u'_def 
+      unfolding u'_def
       by (rule convergent_LIMSEQ_iff[THEN iffD1])
   qed measurable
   then show ?thesis
@@ -1731,7 +1731,7 @@
       from this[THEN spec, of "Suc n"]
       obtain j where j: "\<And>y z. dist x y < ?I j \<Longrightarrow> dist x z < ?I j \<Longrightarrow> dist (f y) (f z) \<le> ?I (Suc n)"
         by auto
-      
+
       show "\<exists>d>0. \<forall>y. dist y x < d \<longrightarrow> dist (f y) (f x) < e"
       proof (safe intro!: exI[of _ "?I j"])
         fix y assume "dist y x < ?I j"
@@ -1789,7 +1789,7 @@
   apply (rule measurable_restrict_countable[OF mono_on_ctble_discont[OF assms]])
   apply (auto intro!: image_eqI[where x="{x}" for x] simp: sets_restrict_space)
   apply (auto simp add: sets_restrict_restrict_space continuous_on_eq_continuous_within
-              cong: measurable_cong_sets 
+              cong: measurable_cong_sets
               intro!: borel_measurable_continuous_on_restrict intro: continuous_within_subset)
   done