# HG changeset patch
# User wenzelm
# Date 1305929358 -7200
# Node ID 4b127cc20aac3ce6454e066cdc2e2a4e9d755cdc
# Parent  4a26abd3d57bea234c55e3b9219b7082aca13a4d# Parent  4aedcff42de6450e65aa04e98551aa3bbec79fdf
merged

diff -r 4a26abd3d57b -r 4b127cc20aac src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Sat May 21 00:01:15 2011 +0200
+++ b/src/HOL/Fields.thy	Sat May 21 00:09:18 2011 +0200
@@ -831,6 +831,39 @@
   apply (auto simp add: mult_commute)
 done
 
+lemma inverse_le_iff:
+  "inverse a \<le> inverse b \<longleftrightarrow> (0 < a * b \<longrightarrow> b \<le> a) \<and> (a * b \<le> 0 \<longrightarrow> a \<le> b)"
+proof -
+  { assume "a < 0"
+    then have "inverse a < 0" by simp
+    moreover assume "0 < b"
+    then have "0 < inverse b" by simp
+    ultimately have "inverse a < inverse b" by (rule less_trans)
+    then have "inverse a \<le> inverse b" by simp }
+  moreover
+  { assume "b < 0"
+    then have "inverse b < 0" by simp
+    moreover assume "0 < a"
+    then have "0 < inverse a" by simp
+    ultimately have "inverse b < inverse a" by (rule less_trans)
+    then have "\<not> inverse a \<le> inverse b" by simp }
+  ultimately show ?thesis
+    by (cases a 0 b 0 rule: linorder_cases[case_product linorder_cases])
+       (auto simp: not_less zero_less_mult_iff mult_le_0_iff)
+qed
+
+lemma inverse_less_iff:
+  "inverse a < inverse b \<longleftrightarrow> (0 < a * b \<longrightarrow> b < a) \<and> (a * b \<le> 0 \<longrightarrow> a < b)"
+  by (subst less_le) (auto simp: inverse_le_iff)
+
+lemma divide_le_cancel:
+  "a / c \<le> b / c \<longleftrightarrow> (0 < c \<longrightarrow> a \<le> b) \<and> (c < 0 \<longrightarrow> b \<le> a)"
+  by (simp add: divide_inverse mult_le_cancel_right)
+
+lemma divide_less_cancel:
+  "a / c < b / c \<longleftrightarrow> (0 < c \<longrightarrow> a < b) \<and> (c < 0 \<longrightarrow> b < a) \<and> c \<noteq> 0"
+  by (auto simp add: divide_inverse mult_less_cancel_right)
+
 text{*Simplify quotients that are compared with the value 1.*}
 
 lemma le_divide_eq_1 [no_atp]:
diff -r 4a26abd3d57b -r 4b127cc20aac src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Sat May 21 00:01:15 2011 +0200
+++ b/src/HOL/Fun.thy	Sat May 21 00:09:18 2011 +0200
@@ -478,6 +478,11 @@
 lemma surj_image_vimage_eq: "surj f ==> f ` (f -` A) = A"
 by simp
 
+lemma surj_vimage_empty:
+  assumes "surj f" shows "f -` A = {} \<longleftrightarrow> A = {}"
+  using surj_image_vimage_eq[OF `surj f`, of A]
+  by (intro iffI) fastsimp+
+
 lemma inj_vimage_image_eq: "inj f ==> f -` (f ` A) = A"
 by (simp add: inj_on_def, blast)
 
diff -r 4a26abd3d57b -r 4b127cc20aac src/HOL/Probability/Probability.thy
--- a/src/HOL/Probability/Probability.thy	Sat May 21 00:01:15 2011 +0200
+++ b/src/HOL/Probability/Probability.thy	Sat May 21 00:09:18 2011 +0200
@@ -1,7 +1,6 @@
 theory Probability
 imports
   Complete_Measure
-  Lebesgue_Measure
   Probability_Measure
   Infinite_Product_Measure
   Independent_Family
diff -r 4a26abd3d57b -r 4b127cc20aac src/HOL/Probability/Probability_Measure.thy
--- a/src/HOL/Probability/Probability_Measure.thy	Sat May 21 00:01:15 2011 +0200
+++ b/src/HOL/Probability/Probability_Measure.thy	Sat May 21 00:09:18 2011 +0200
@@ -6,7 +6,7 @@
 header {*Probability measure*}
 
 theory Probability_Measure
-imports Lebesgue_Integration Radon_Nikodym Finite_Product_Measure
+imports Lebesgue_Integration Radon_Nikodym Finite_Product_Measure Lebesgue_Measure
 begin
 
 lemma real_of_extreal_inverse[simp]:
@@ -1061,6 +1061,66 @@
   qed
 qed
 
+subsection "Borel Measure on {0 .. 1}"
+
+definition pborel :: "real measure_space" where
+  "pborel = lborel.restricted_space {0 .. 1}"
+
+lemma space_pborel[simp]:
+  "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}"
+  unfolding pborel_def by auto
+
+lemma in_pborel[intro, simp]:
+  "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}"]
+  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)"
+  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)"
+    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_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)
+
+lemma pborel_lebesgue_measure:
+  "A \<in> sets pborel \<Longrightarrow> pborel.prob A = real (measure lebesgue A)"
+  by (simp add: sets_pborel pborel_prob)
+
+lemma pborel_alt:
+  "pborel = sigma \<lparr>
+    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})"
+    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)
+  also have "\<dots> = ?R"
+    by (subst restricted_sigma)
+       (simp_all add: sets_sigma sigma_sets.Basic ** pborel_def image_eqI[of _ _ "(0,1)"])
+  finally show ?thesis .
+qed
+
 subsection "Bernoulli space"
 
 definition "bernoulli_space p = \<lparr> space = UNIV, sets = UNIV,
diff -r 4a26abd3d57b -r 4b127cc20aac src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Sat May 21 00:01:15 2011 +0200
+++ b/src/HOL/SetInterval.thy	Sat May 21 00:09:18 2011 +0200
@@ -269,6 +269,21 @@
   "{} = { a <..< b } \<longleftrightarrow> b \<le> a"
   using dense[of a b] by (cases "a < b") auto
 
+lemma atLeastLessThan_subseteq_atLeastAtMost_iff:
+  "{a ..< b} \<subseteq> { c .. d } \<longleftrightarrow> (a < b \<longrightarrow> c \<le> a \<and> b \<le> d)"
+  using dense[of "max a d" "b"]
+  by (force simp: subset_eq Ball_def not_less[symmetric])
+
+lemma greaterThanAtMost_subseteq_atLeastAtMost_iff:
+  "{a <.. b} \<subseteq> { c .. d } \<longleftrightarrow> (a < b \<longrightarrow> c \<le> a \<and> b \<le> d)"
+  using dense[of "a" "min c b"]
+  by (force simp: subset_eq Ball_def not_less[symmetric])
+
+lemma greaterThanLessThan_subseteq_atLeastAtMost_iff:
+  "{a <..< b} \<subseteq> { c .. d } \<longleftrightarrow> (a < b \<longrightarrow> c \<le> a \<and> b \<le> d)"
+  using dense[of "a" "min c b"] dense[of "max a d" "b"]
+  by (force simp: subset_eq Ball_def not_less[symmetric])
+
 end
 
 lemma (in linorder) atLeastLessThan_subset_iff: