# HG changeset patch
# User hoelzl
# Date 1305827887 -7200
# Node ID b02349e70d5a1f968f79685cde7765f799ad865c
# Parent  d9dfc733f25c7c4b1cef795d278c2d2917836a1f
add Bernoulli space

diff -r d9dfc733f25c -r b02349e70d5a src/HOL/Probability/Probability_Measure.thy
--- a/src/HOL/Probability/Probability_Measure.thy	Thu May 19 19:57:59 2011 +0200
+++ b/src/HOL/Probability/Probability_Measure.thy	Thu May 19 19:58:07 2011 +0200
@@ -1045,4 +1045,21 @@
   qed
 qed
 
+subsection "Bernoulli space"
+
+definition "bernoulli_space p = \<lparr> space = UNIV, sets = UNIV,
+  measure = extreal \<circ> setsum (\<lambda>b. if b then min 1 (max 0 p) else 1 - min 1 (max 0 p)) \<rparr>"
+
+interpretation bernoulli: finite_prob_space "bernoulli_space p" for p
+  by (rule finite_prob_spaceI)
+     (auto simp: bernoulli_space_def UNIV_bool one_extreal_def setsum_Un_disjoint intro!: setsum_nonneg)
+
+lemma bernoulli_measure:
+  "0 \<le> p \<Longrightarrow> p \<le> 1 \<Longrightarrow> bernoulli.prob p B = (\<Sum>b\<in>B. if b then p else 1 - p)"
+  unfolding bernoulli.\<mu>'_def unfolding bernoulli_space_def by (auto intro!: setsum_cong)
+
+lemma bernoulli_measure_True: "0 \<le> p \<Longrightarrow> p \<le> 1 \<Longrightarrow> bernoulli.prob p {True} = p"
+  and bernoulli_measure_False: "0 \<le> p \<Longrightarrow> p \<le> 1 \<Longrightarrow> bernoulli.prob p {False} = 1 - p"
+  unfolding bernoulli_measure by simp_all
+
 end