# 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 \ inverse b \ (0 < a * b \ b \ a) \ (a * b \ 0 \ a \ 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 \ 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 "\ inverse a \ 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 \ (0 < a * b \ b < a) \ (a * b \ 0 \ a < b)" + by (subst less_le) (auto simp: inverse_le_iff) + +lemma divide_le_cancel: + "a / c \ b / c \ (0 < c \ a \ b) \ (c < 0 \ b \ a)" + by (simp add: divide_inverse mult_le_cancel_right) + +lemma divide_less_cancel: + "a / c < b / c \ (0 < c \ a < b) \ (c < 0 \ b < a) \ c \ 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 = {} \ 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 \ sets pborel \ A \ sets borel \ A \ { 0 .. 1}" + unfolding pborel_def by auto + +lemma in_pborel[intro, simp]: + "A \ {0 .. 1} \ A \ sets borel \ A \ 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 \ sets borel \ A \ {0 .. 1} then real (lborel.\ A) else 0)" + unfolding pborel.\'_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.\' {a .. b} = (if 0 \ a \ a \ b \ b \ 1 then b - a else 0)" + and pborel_atLeastLessThan[simp]: "pborel.\' {a ..< b} = (if 0 \ a \ a \ b \ b \ 1 then b - a else 0)" + and pborel_greaterThanAtMost[simp]: "pborel.\' {a <.. b} = (if 0 \ a \ a \ b \ b \ 1 then b - a else 0)" + and pborel_greaterThanLessThan[simp]: "pborel.\' {a <..< b} = (if 0 \ a \ a \ b \ b \ 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 \ sets pborel \ pborel.prob A = real (measure lebesgue A)" + by (simp add: sets_pborel pborel_prob) + +lemma pborel_alt: + "pborel = sigma \ + space = {0..1}, + sets = range (\(x,y). {x..y} \ {0..1}), + measure = measure lborel \" (is "_ = ?R") +proof - + have *: "{0..1::real} \ sets borel" by auto + have **: "op \ {0..1::real} ` range (\(x, y). {x..y}) = range (\(x,y). {x..y} \ {0..1})" + unfolding image_image by (intro arg_cong[where f=range]) auto + have "pborel = algebra.restricted_space (sigma \space=UNIV, sets=range (\(a, b). {a .. b :: real}), + measure = measure pborel\) {0 .. 1}" + by (simp add: sigma_def lebesgue_def pborel_def borel_eq_atLeastAtMost lborel_def) + also have "\ = ?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 = \ 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 } \ b \ a" using dense[of a b] by (cases "a < b") auto +lemma atLeastLessThan_subseteq_atLeastAtMost_iff: + "{a ..< b} \ { c .. d } \ (a < b \ c \ a \ b \ 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} \ { c .. d } \ (a < b \ c \ a \ b \ 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} \ { c .. d } \ (a < b \ c \ a \ b \ 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: