# HG changeset patch
# User hoelzl
# Date 1309767826 -7200
# Node ID 0d96ec6ec33b6248f5d6d58210b4830aca38725d
# Parent  537ea3846f649a02e32506865cc7b3f35639e768
the borel probability measure is easier to handle with {0 ..< 1} (coverable by disjoint intervals {_ ..< _})

diff -r 537ea3846f64 -r 0d96ec6ec33b src/HOL/Probability/Probability_Measure.thy
--- a/src/HOL/Probability/Probability_Measure.thy	Mon Jul 04 10:15:49 2011 +0200
+++ b/src/HOL/Probability/Probability_Measure.thy	Mon Jul 04 10:23:46 2011 +0200
@@ -1107,43 +1107,44 @@
     by (simp add: distribution_def prob_space vimage_Times comp_def measure_space_1)
 qed
 
-subsection "Borel Measure on {0 .. 1}"
+subsection "Borel Measure on {0 ..< 1}"
 
 definition pborel :: "real measure_space" where
-  "pborel = lborel.restricted_space {0 .. 1}"
+  "pborel = lborel.restricted_space {0 ..< 1}"
 
 lemma space_pborel[simp]:
-  "space pborel = {0 .. 1}"
+  "space pborel = {0 ..< 1}"
   unfolding pborel_def by auto
 
 lemma sets_pborel:
-  "A \<in> sets pborel \<longleftrightarrow> A \<in> sets borel \<and> A \<subseteq> { 0 .. 1}"
+  "A \<in> sets pborel \<longleftrightarrow> A \<in> sets borel \<and> A \<subseteq> { 0 ..< 1}"
   unfolding pborel_def by auto
 
 lemma in_pborel[intro, simp]:
-  "A \<subseteq> {0 .. 1} \<Longrightarrow> A \<in> sets borel \<Longrightarrow> A \<in> sets pborel"
+  "A \<subseteq> {0 ..< 1} \<Longrightarrow> A \<in> sets borel \<Longrightarrow> A \<in> sets pborel"
   unfolding pborel_def by auto
 
 interpretation pborel: measure_space pborel
-  using lborel.restricted_measure_space[of "{0 .. 1}"]
+  using lborel.restricted_measure_space[of "{0 ..< 1}"]
   by (simp add: pborel_def)
 
 interpretation pborel: prob_space pborel
   by default (simp add: one_extreal_def pborel_def)
 
-lemma pborel_prob: "pborel.prob A = (if A \<in> sets borel \<and> A \<subseteq> {0 .. 1} then real (lborel.\<mu> A) else 0)"
+lemma pborel_prob: "pborel.prob A = (if A \<in> sets borel \<and> A \<subseteq> {0 ..< 1} then real (lborel.\<mu> A) else 0)"
   unfolding pborel.\<mu>'_def by (auto simp: pborel_def)
 
 lemma pborel_singelton[simp]: "pborel.prob {a} = 0"
   by (auto simp: pborel_prob)
 
 lemma
-  shows pborel_atLeastAtMost[simp]: "pborel.\<mu>' {a .. b} = (if 0 \<le> a \<and> a \<le> b \<and> b \<le> 1 then b - a else 0)"
+  shows pborel_atLeastAtMost[simp]: "pborel.\<mu>' {a .. b} = (if 0 \<le> a \<and> a \<le> b \<and> b < 1 then b - a else 0)"
     and pborel_atLeastLessThan[simp]: "pborel.\<mu>' {a ..< b} = (if 0 \<le> a \<and> a \<le> b \<and> b \<le> 1 then b - a else 0)"
-    and pborel_greaterThanAtMost[simp]: "pborel.\<mu>' {a <.. b} = (if 0 \<le> a \<and> a \<le> b \<and> b \<le> 1 then b - a else 0)"
+    and pborel_greaterThanAtMost[simp]: "pborel.\<mu>' {a <.. b} = (if 0 \<le> a \<and> a \<le> b \<and> b < 1 then b - a else 0)"
     and pborel_greaterThanLessThan[simp]: "pborel.\<mu>' {a <..< b} = (if 0 \<le> a \<and> a \<le> b \<and> b \<le> 1 then b - a else 0)"
-  unfolding pborel_prob by (auto simp: atLeastLessThan_subseteq_atLeastAtMost_iff
-    greaterThanAtMost_subseteq_atLeastAtMost_iff greaterThanLessThan_subseteq_atLeastAtMost_iff)
+  unfolding pborel_prob
+  by (auto simp: atLeastAtMost_subseteq_atLeastLessThan_iff
+    greaterThanAtMost_subseteq_atLeastLessThan_iff greaterThanLessThan_subseteq_atLeastLessThan_iff)
 
 lemma pborel_lebesgue_measure:
   "A \<in> sets pborel \<Longrightarrow> pborel.prob A = real (measure lebesgue A)"
@@ -1151,16 +1152,16 @@
 
 lemma pborel_alt:
   "pborel = sigma \<lparr>
-    space = {0..1},
-    sets = range (\<lambda>(x,y). {x..y} \<inter> {0..1}),
+    space = {0..<1},
+    sets = range (\<lambda>(x,y). {x..<y} \<inter> {0..<1}),
     measure = measure lborel \<rparr>" (is "_ = ?R")
 proof -
-  have *: "{0..1::real} \<in> sets borel" by auto
-  have **: "op \<inter> {0..1::real} ` range (\<lambda>(x, y). {x..y}) = range (\<lambda>(x,y). {x..y} \<inter> {0..1})"
+  have *: "{0..<1::real} \<in> sets borel" by auto
+  have **: "op \<inter> {0..<1::real} ` range (\<lambda>(x, y). {x..<y}) = range (\<lambda>(x,y). {x..<y} \<inter> {0..<1})"
     unfolding image_image by (intro arg_cong[where f=range]) auto
-  have "pborel = algebra.restricted_space (sigma \<lparr>space=UNIV, sets=range (\<lambda>(a, b). {a .. b :: real}),
-    measure = measure pborel\<rparr>) {0 .. 1}"
-    by (simp add: sigma_def lebesgue_def pborel_def borel_eq_atLeastAtMost lborel_def)
+  have "pborel = algebra.restricted_space (sigma \<lparr>space=UNIV, sets=range (\<lambda>(a, b). {a ..< b :: real}),
+    measure = measure pborel\<rparr>) {0 ..< 1}"
+    by (simp add: sigma_def lebesgue_def pborel_def borel_eq_atLeastLessThan lborel_def)
   also have "\<dots> = ?R"
     by (subst restricted_sigma)
        (simp_all add: sets_sigma sigma_sets.Basic ** pborel_def image_eqI[of _ _ "(0,1)"])