--- 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]:
--- 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)
--- 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
--- 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,
--- 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: