src/HOL/Probability/Borel_Space.thy

   unfolding borel_def by auto
 
 lemma pred_Collect_borel[measurable (raw)]: "Sigma_Algebra.pred borel P \<Longrightarrow> {x. P x} \<in> sets borel"
   unfolding borel_def pred_def by auto
 
-lemma borel_open[simp, measurable (raw generic)]:
+lemma borel_open[measurable (raw generic)]:
   assumes "open A" shows "A \<in> sets borel"
 proof -
   have "A \<in> {S. open S}" unfolding mem_Collect_eq using assms .
   thus ?thesis unfolding borel_def by auto
 qed
 
-lemma borel_closed[simp, measurable (raw generic)]:
+lemma borel_closed[measurable (raw generic)]:
   assumes "closed A" shows "A \<in> sets borel"
 proof -
   have "space borel - (- A) \<in> sets borel"
     using assms unfolding closed_def by (blast intro: borel_open)
   thus ?thesis by simp
 qed
 
-lemma borel_insert[measurable]:
-  "A \<in> sets borel \<Longrightarrow> insert x A \<in> sets (borel :: 'a::t2_space measure)"
+lemma borel_singleton[measurable]:
+  "A \<in> sets borel \<Longrightarrow> insert x A \<in> sets (borel :: 'a::t1_space measure)"
   unfolding insert_def by (rule Un) auto
 
-lemma borel_comp[intro, simp, measurable]: "A \<in> sets borel \<Longrightarrow> - A \<in> sets borel"
+lemma borel_comp[measurable]: "A \<in> sets borel \<Longrightarrow> - A \<in> sets borel"
   unfolding Compl_eq_Diff_UNIV by simp
 
 lemma borel_measurable_vimage:
   fixes f :: "'a \<Rightarrow> 'x::t2_space"
   assumes borel[measurable]: "f \<in> borel_measurable M"

 proof (rule measurable_measure_of, simp_all)
   fix S :: "'x set" assume "open S" thus "f -` S \<inter> space M \<in> sets M"
     using assms[of S] by simp
 qed
 
-lemma borel_singleton[simp, intro]:
-  fixes x :: "'a::t1_space"
-  shows "A \<in> sets borel \<Longrightarrow> insert x A \<in> sets borel"
-  proof (rule insert_in_sets)
-    show "{x} \<in> sets borel"
-      using closed_singleton[of x] by (rule borel_closed)
-  qed simp
-
-lemma borel_measurable_const[simp, intro, measurable (raw)]:
+lemma borel_measurable_const[measurable (raw)]:
   "(\<lambda>x. c) \<in> borel_measurable M"
   by auto
 
-lemma borel_measurable_indicator[simp, intro!]:
+lemma borel_measurable_indicator:
   assumes A: "A \<in> sets M"
   shows "indicator A \<in> borel_measurable M"
   unfolding indicator_def [abs_def] using A
   by (auto intro!: measurable_If_set)
 

 
 lemma borel_measurable_euclidean_component:
   "(f :: 'a \<Rightarrow> 'b::euclidean_space) \<in> borel_measurable M \<Longrightarrow>(\<lambda>x. f x $$ i) \<in> borel_measurable M"
   by simp
 
-lemma [simp, intro, measurable]:
+lemma [measurable]:
   fixes a b :: "'a\<Colon>ordered_euclidean_space"
   shows lessThan_borel: "{..< a} \<in> sets borel"
     and greaterThan_borel: "{a <..} \<in> sets borel"
     and greaterThanLessThan_borel: "{a<..<b} \<in> sets borel"
     and atMost_borel: "{..a} \<in> sets borel"

     and atLeastLessThan_borel: "{a..<b} \<in> sets borel"
   unfolding greaterThanAtMost_def atLeastLessThan_def
   by (blast intro: borel_open borel_closed)+
 
 lemma 
-  shows hafspace_less_borel[simp, intro]: "{x::'a::euclidean_space. a < x $$ i} \<in> sets borel"
-    and hafspace_greater_borel[simp, intro]: "{x::'a::euclidean_space. x $$ i < a} \<in> sets borel"
-    and hafspace_less_eq_borel[simp, intro]: "{x::'a::euclidean_space. a \<le> x $$ i} \<in> sets borel"
-    and hafspace_greater_eq_borel[simp, intro]: "{x::'a::euclidean_space. x $$ i \<le> a} \<in> sets borel"
+  shows hafspace_less_borel: "{x::'a::euclidean_space. a < x $$ i} \<in> sets borel"
+    and hafspace_greater_borel: "{x::'a::euclidean_space. x $$ i < a} \<in> sets borel"
+    and hafspace_less_eq_borel: "{x::'a::euclidean_space. a \<le> x $$ i} \<in> sets borel"
+    and hafspace_greater_eq_borel: "{x::'a::euclidean_space. x $$ i \<le> a} \<in> sets borel"
   by simp_all
 
-lemma borel_measurable_less[simp, intro, measurable]:
+lemma borel_measurable_less[measurable]:
   fixes f :: "'a \<Rightarrow> real"
   assumes f: "f \<in> borel_measurable M"
   assumes g: "g \<in> borel_measurable M"
   shows "{w \<in> space M. f w < g w} \<in> sets M"
 proof -

     using Rats_dense_in_real by (auto simp add: Rats_def)
   with f g show ?thesis
     by simp
 qed
 
-lemma [simp, intro]:
+lemma
   fixes f :: "'a \<Rightarrow> real"
   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"
     and borel_measurable_eq[measurable]: "{w \<in> space M. f w = g w} \<in> sets M"

   assumes g: "g \<in> borel_measurable M"
   shows "(\<lambda>x. if g x \<in> A then f (g x) else c) \<in> borel_measurable M"
   using measurable_comp[OF g borel_measurable_continuous_on_open'[OF cont], of c]
   by (simp add: comp_def)
 
-lemma borel_measurable_uminus[simp, intro, measurable (raw)]:
+lemma borel_measurable_uminus[measurable (raw)]:
   fixes g :: "'a \<Rightarrow> real"
   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)
 
 lemma euclidean_component_prod:
   fixes x :: "'a :: euclidean_space \<times> 'b :: euclidean_space"
   shows "x $$ i = (if i < DIM('a) then fst x $$ i else snd x $$ (i - DIM('a)))"
   unfolding euclidean_component_def basis_prod_def inner_prod_def by auto
 
-lemma borel_measurable_Pair[simp, intro, measurable (raw)]:
+lemma borel_measurable_Pair[measurable (raw)]:
   fixes f :: "'a \<Rightarrow> 'b::ordered_euclidean_space" and g :: "'a \<Rightarrow> 'c::ordered_euclidean_space"
   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"
 proof (intro borel_measurable_iff_halfspace_le[THEN iffD2] allI impI)

     by (auto simp: continuous_on_closed closed_closedin vimage_def)
 qed
 
 lemma borel_measurable_continuous_Pair:
   fixes f :: "'a \<Rightarrow> 'b::ordered_euclidean_space" and g :: "'a \<Rightarrow> 'c::ordered_euclidean_space"
-  assumes [simp]: "f \<in> borel_measurable M"
-  assumes [simp]: "g \<in> borel_measurable M"
+  assumes [measurable]: "f \<in> borel_measurable M"
+  assumes [measurable]: "g \<in> borel_measurable M"
   assumes H: "continuous_on UNIV (\<lambda>x. H (fst x) (snd x))"
   shows "(\<lambda>x. H (f x) (g x)) \<in> borel_measurable M"
 proof -
   have eq: "(\<lambda>x. H (f x) (g x)) = (\<lambda>x. (\<lambda>x. H (fst x) (snd x)) (f x, g x))" by auto
   show ?thesis
     unfolding eq by (rule borel_measurable_continuous_on[OF H]) auto
 qed
 
-lemma borel_measurable_add[simp, intro, measurable (raw)]:
+lemma borel_measurable_add[measurable (raw)]:
   fixes f g :: "'a \<Rightarrow> 'c::ordered_euclidean_space"
   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)
 
-lemma borel_measurable_setsum[simp, intro, measurable (raw)]:
+lemma borel_measurable_setsum[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. \<Sum>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_diff[simp, intro, measurable (raw)]:
+lemma borel_measurable_diff[measurable (raw)]:
   fixes f :: "'a \<Rightarrow> real"
   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 fast
-
-lemma borel_measurable_times[simp, intro, measurable (raw)]:
+  unfolding diff_minus using assms by simp
+
+lemma borel_measurable_times[measurable (raw)]:
   fixes f :: "'a \<Rightarrow> real"
   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

 lemma continuous_on_dist:
   fixes f :: "'a :: t2_space \<Rightarrow> 'b :: metric_space"
   shows "continuous_on A f \<Longrightarrow> continuous_on A g \<Longrightarrow> continuous_on A (\<lambda>x. dist (f x) (g x))"
   unfolding continuous_on_eq_continuous_within by (auto simp: continuous_dist)
 
-lemma borel_measurable_dist[simp, intro, measurable (raw)]:
+lemma borel_measurable_dist[measurable (raw)]:
   fixes g f :: "'a \<Rightarrow> 'b::ordered_euclidean_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

 
 lemma borel_measurable_const_add[measurable (raw)]:
   "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[simp, intro, measurable (raw)]:
+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[simp, intro, measurable (raw)]:
+lemma borel_measurable_inverse[measurable (raw)]:
   fixes f :: "'a \<Rightarrow> real"
   assumes f: "f \<in> borel_measurable M"
   shows "(\<lambda>x. inverse (f x)) \<in> borel_measurable M"
 proof -
-  have *: "\<And>x::real. inverse x = (if x \<in> UNIV - {0} then inverse x else 0)" by auto
-  show ?thesis
-    apply (subst *)
-    apply (rule borel_measurable_continuous_on_open)
-    apply (auto intro!: f continuous_on_inverse continuous_on_id)
-    done
-qed
-
-lemma borel_measurable_divide[simp, intro, measurable (raw)]:
-  fixes f :: "'a \<Rightarrow> real"
-  assumes "f \<in> borel_measurable M"
-  and "g \<in> borel_measurable M"
-  shows "(\<lambda>x. f x / g x) \<in> borel_measurable M"
-  unfolding field_divide_inverse
-  by (rule borel_measurable_inverse borel_measurable_times assms)+
-
-lemma borel_measurable_max[intro, simp, measurable (raw)]:
-  fixes f g :: "'a \<Rightarrow> real"
-  assumes "f \<in> borel_measurable M"
-  assumes "g \<in> borel_measurable M"
-  shows "(\<lambda>x. max (g x) (f x)) \<in> borel_measurable M"
-  unfolding max_def by (auto intro!: assms measurable_If)
-
-lemma borel_measurable_min[intro, simp, measurable (raw)]:
-  fixes f g :: "'a \<Rightarrow> real"
-  assumes "f \<in> borel_measurable M"
-  assumes "g \<in> borel_measurable M"
-  shows "(\<lambda>x. min (g x) (f x)) \<in> borel_measurable M"
-  unfolding min_def by (auto intro!: assms measurable_If)
-
-lemma borel_measurable_abs[simp, intro, measurable (raw)]:
-  assumes "f \<in> borel_measurable M"
-  shows "(\<lambda>x. \<bar>f x :: real\<bar>) \<in> borel_measurable M"
-proof -
-  have *: "\<And>x. \<bar>f x\<bar> = max 0 (f x) + max 0 (- f x)" by (simp add: max_def)
-  show ?thesis unfolding * using assms by auto
-qed
-
-lemma borel_measurable_nth[simp, intro, measurable (raw)]:
+  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
+  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"
+  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"
+  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"
+  by (simp add: min_def)
+
+lemma borel_measurable_abs[measurable (raw)]:
+  "f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. \<bar>f x :: real\<bar>) \<in> borel_measurable M"
+  unfolding abs_real_def by simp
+
+lemma borel_measurable_nth[measurable (raw)]:
   "(\<lambda>x::real^'n. x $ i) \<in> borel_measurable borel"
-  using borel_measurable_euclidean_component'
-  unfolding nth_conv_component by auto
+  by (simp add: nth_conv_component)
 
 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"

   also have "?qX \<longleftrightarrow> (\<lambda>x. q (X x)) \<in> borel_measurable M"
     using X by (intro measurable_cong) auto
   finally show ?thesis .
 qed
 
-lemma borel_measurable_ln[simp, intro, measurable (raw)]:
+lemma borel_measurable_ln[measurable (raw)]:
   assumes f: "f \<in> borel_measurable M"
   shows "(\<lambda>x. ln (f x)) \<in> borel_measurable M"
 proof -
   { fix x :: real assume x: "x \<le> 0"
     { fix x::real assume "x \<le> 0" then have "\<And>u. exp u = x \<longleftrightarrow> False" by auto }

   also have "(\<lambda>x. if x \<in> {0<..} then ln x else ln 0) = ln"
     by (simp add: fun_eq_iff not_less ln_imp)
   finally show ?thesis .
 qed
 
-lemma borel_measurable_log[simp, intro, measurable (raw)]:
+lemma borel_measurable_log[measurable (raw)]:
   "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. log (g x) (f x)) \<in> borel_measurable M"
   unfolding log_def by auto
 
 lemma measurable_count_space_eq2_countable:
   fixes f :: "'a => 'c::countable"

   unfolding ceiling_def[abs_def] by simp
 
 lemma borel_measurable_real_floor: "(\<lambda>x::real. real \<lfloor>x\<rfloor>) \<in> borel_measurable borel"
   by simp
 
-lemma borel_measurable_real_natfloor[intro, simp]:
+lemma borel_measurable_real_natfloor:
   "f \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. real (natfloor (f x))) \<in> borel_measurable M"
   by simp
 
 subsection "Borel space on the extended reals"
 
-lemma borel_measurable_ereal[simp, intro, measurable (raw)]:
+lemma borel_measurable_ereal[measurable (raw)]:
   assumes f: "f \<in> borel_measurable M" shows "(\<lambda>x. ereal (f x)) \<in> borel_measurable M"
   using continuous_on_ereal f by (rule borel_measurable_continuous_on)
 
-lemma borel_measurable_real_of_ereal[simp, intro, measurable (raw)]:
+lemma borel_measurable_real_of_ereal[measurable (raw)]:
   fixes f :: "'a \<Rightarrow> ereal" 
   assumes f: "f \<in> borel_measurable M"
   shows "(\<lambda>x. real (f x)) \<in> borel_measurable M"
 proof -
   have "(\<lambda>x. if f x \<in> UNIV - { \<infinity>, - \<infinity> } then real (f x) else 0) \<in> borel_measurable M"

   { fix x have "H (f x) = ?F x" by (cases "f x") auto }
   with f H show ?thesis by simp
 qed
 
 lemma
-  fixes f :: "'a \<Rightarrow> ereal" assumes f[simp]: "f \<in> borel_measurable M"
-  shows borel_measurable_ereal_abs[intro, simp, measurable(raw)]: "(\<lambda>x. \<bar>f x\<bar>) \<in> borel_measurable M"
-    and borel_measurable_ereal_inverse[simp, intro, measurable(raw)]: "(\<lambda>x. inverse (f x) :: ereal) \<in> borel_measurable M"
-    and borel_measurable_uminus_ereal[intro, measurable(raw)]: "(\<lambda>x. - f x :: ereal) \<in> borel_measurable M"
+  fixes f :: "'a \<Rightarrow> ereal" assumes f[measurable]: "f \<in> borel_measurable M"
+  shows borel_measurable_ereal_abs[measurable(raw)]: "(\<lambda>x. \<bar>f x\<bar>) \<in> borel_measurable M"
+    and borel_measurable_ereal_inverse[measurable(raw)]: "(\<lambda>x. inverse (f x) :: ereal) \<in> borel_measurable M"
+    and borel_measurable_uminus_ereal[measurable(raw)]: "(\<lambda>x. - f x :: ereal) \<in> borel_measurable M"
   by (auto simp del: abs_real_of_ereal simp: borel_measurable_ereal_cases[OF f] measurable_If)
 
 lemma borel_measurable_uminus_eq_ereal[simp]:
   "(\<lambda>x. - f x :: ereal) \<in> borel_measurable M \<longleftrightarrow> f \<in> borel_measurable M" (is "?l = ?r")
 proof

   note * = this
   from assms show ?thesis
     by (subst *) (simp del: space_borel split del: split_if)
 qed
 
-lemma
+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[intro,simp,measurable(raw)]: "{x \<in> space M. f x \<le> g x} \<in> sets M"
-    and borel_measurable_ereal_less[intro,simp,measurable(raw)]: "{x \<in> space M. f x < g x} \<in> sets M"
-    and borel_measurable_ereal_eq[intro,simp,measurable(raw)]: "{w \<in> space M. f w = g w} \<in> sets M"
-    and borel_measurable_ereal_neq[intro,simp]: "{w \<in> space M. f w \<noteq> g w} \<in> sets M"
-  using f g by (auto simp: f g set_Collect_ereal2[OF f g] intro!: sets_Collect_neg)
+  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
   assume "(\<lambda>x. ereal (f x)) \<in> borel_measurable M"

   fixes f :: "'a \<Rightarrow> ereal" assumes f: "f \<in> borel_measurable M"
   shows borel_measurable_ereal_eq_const: "{x\<in>space M. f x = c} \<in> sets M"
     and borel_measurable_ereal_neq_const: "{x\<in>space M. f x \<noteq> c} \<in> sets M"
   using f by auto
 
-lemma [intro, simp, measurable(raw)]:
+lemma [measurable(raw)]:
   fixes f :: "'a \<Rightarrow> ereal"
-  assumes [simp]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
+  assumes [measurable]: "f \<in> borel_measurable M" "g \<in> borel_measurable M"
   shows borel_measurable_ereal_add: "(\<lambda>x. f x + g x) \<in> borel_measurable M"
     and borel_measurable_ereal_times: "(\<lambda>x. f x * g x) \<in> borel_measurable M"
     and borel_measurable_ereal_min: "(\<lambda>x. min (g x) (f x)) \<in> borel_measurable M"
     and borel_measurable_ereal_max: "(\<lambda>x. max (g x) (f x)) \<in> borel_measurable M"
-  by (auto simp add: borel_measurable_ereal2 measurable_If min_def max_def)
-
-lemma [simp, intro, measurable(raw)]:
+  by (simp_all add: borel_measurable_ereal2 min_def max_def)
+
+lemma [measurable(raw)]:
   fixes f g :: "'a \<Rightarrow> ereal"
   assumes "f \<in> borel_measurable M"
   assumes "g \<in> borel_measurable M"
   shows borel_measurable_ereal_diff: "(\<lambda>x. f x - g x) \<in> borel_measurable M"
     and borel_measurable_ereal_divide: "(\<lambda>x. f x / g x) \<in> borel_measurable M"
-  unfolding minus_ereal_def divide_ereal_def using assms by auto
-
-lemma borel_measurable_ereal_setsum[simp, intro,measurable (raw)]:
+  using assms by (simp_all add: minus_ereal_def divide_ereal_def)
+
+lemma borel_measurable_ereal_setsum[measurable (raw)]:
   fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> ereal"
   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
   assume "finite S"
   thus ?thesis using assms
     by induct auto
 qed simp
 
-lemma borel_measurable_ereal_setprod[simp, intro,measurable (raw)]:
+lemma borel_measurable_ereal_setprod[measurable (raw)]:
   fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> ereal"
   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_SUP[simp, intro,measurable (raw)]:
+lemma borel_measurable_SUP[measurable (raw)]:
   fixes f :: "'d\<Colon>countable \<Rightarrow> 'a \<Rightarrow> ereal"
   assumes "\<And>i. i \<in> A \<Longrightarrow> f i \<in> borel_measurable M"
   shows "(\<lambda>x. SUP i : A. f i x) \<in> borel_measurable M" (is "?sup \<in> borel_measurable M")
   unfolding borel_measurable_ereal_iff_ge
 proof

     by (auto simp: less_SUP_iff)
   then show "?sup -` {a<..} \<inter> space M \<in> sets M"
     using assms by auto
 qed
 
-lemma borel_measurable_INF[simp, intro,measurable (raw)]:
+lemma borel_measurable_INF[measurable (raw)]:
   fixes f :: "'d :: countable \<Rightarrow> 'a \<Rightarrow> ereal"
   assumes "\<And>i. i \<in> A \<Longrightarrow> f i \<in> borel_measurable M"
   shows "(\<lambda>x. INF i : A. f i x) \<in> borel_measurable M" (is "?inf \<in> borel_measurable M")
   unfolding borel_measurable_ereal_iff_less
 proof

     by (auto simp: INF_less_iff)
   then show "?inf -` {..<a} \<inter> space M \<in> sets M"
     using assms by auto
 qed
 
-lemma [simp, intro, measurable (raw)]:
+lemma [measurable (raw)]:
   fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
   assumes "\<And>i. f i \<in> borel_measurable M"
   shows borel_measurable_liminf: "(\<lambda>x. liminf (\<lambda>i. f i x)) \<in> borel_measurable M"
     and borel_measurable_limsup: "(\<lambda>x. limsup (\<lambda>i. f i x)) \<in> borel_measurable M"
   unfolding liminf_SUPR_INFI limsup_INFI_SUPR using assms by auto
 
+lemma sets_Collect_eventually_sequientially[measurable]:
+  "(\<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 convergent_ereal:
+  fixes X :: "nat \<Rightarrow> ereal"
+  shows "convergent X \<longleftrightarrow> limsup X = liminf X"
+  using ereal_Liminf_eq_Limsup_iff[of sequentially]
+  by (auto simp: convergent_def)
+
+lemma convergent_ereal_limsup:
+  fixes X :: "nat \<Rightarrow> ereal"
+  shows "convergent X \<Longrightarrow> limsup X = lim X"
+  by (auto simp: convergent_def limI lim_imp_Limsup)
+
+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"
+  unfolding convergent_ereal by auto
+
+lemma borel_measurable_extreal_lim[measurable (raw)]:
+  fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
+  assumes [measurable]: "\<And>i. f i \<in> borel_measurable M"
+  shows "(\<lambda>x. lim (\<lambda>i. f i x)) \<in> borel_measurable M"
+proof -
+  have "\<And>x. lim (\<lambda>i. f i x) = (if convergent (\<lambda>i. f i x) then limsup (\<lambda>i. f i x) else (THE i. False))"
+    using convergent_ereal_limsup by (simp add: lim_def convergent_def)
+  then show ?thesis
+    by simp
+qed
+
 lemma borel_measurable_ereal_LIMSEQ:
   fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
   assumes u': "\<And>x. x \<in> space M \<Longrightarrow> (\<lambda>i. u i x) ----> u' x"
   and u: "\<And>i. u i \<in> borel_measurable M"
   shows "u' \<in> borel_measurable M"
 proof -
   have "\<And>x. x \<in> space M \<Longrightarrow> u' x = liminf (\<lambda>n. u n x)"
     using u' by (simp add: lim_imp_Liminf[symmetric])
-  then show ?thesis by (simp add: u cong: measurable_cong)
-qed
-
-lemma borel_measurable_psuminf[simp, intro, measurable (raw)]:
+  with u show ?thesis by (simp cong: measurable_cong)
+qed
+
+lemma borel_measurable_extreal_suminf[measurable (raw)]:
   fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> ereal"
-  assumes "\<And>i. f i \<in> borel_measurable M" and pos: "\<And>i x. x \<in> space M \<Longrightarrow> 0 \<le> f i x"
+  assumes [measurable]: "\<And>i. f i \<in> borel_measurable M"
   shows "(\<lambda>x. (\<Sum>i. f i x)) \<in> borel_measurable M"
-  apply (subst measurable_cong)
-  apply (subst suminf_ereal_eq_SUPR)
-  apply (rule pos)
-  using assms by auto
+  unfolding suminf_def sums_def[abs_def] lim_def[symmetric] by simp
 
 section "LIMSEQ is borel measurable"
 
 lemma borel_measurable_LIMSEQ:
   fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> real"