src/HOL/Probability/Probability_Mass_Function.thy
 changeset 59667 651ea265d568 parent 59665 37adca7fd48f child 59670 dee043d19729 child 59730 b7c394c7a619
```     1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Tue Mar 10 11:56:32 2015 +0100
1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Tue Mar 10 15:20:40 2015 +0000
1.3 @@ -1,5 +1,5 @@
1.4  (*  Title:      HOL/Probability/Probability_Mass_Function.thy
1.5 -    Author:     Johannes Hölzl, TU München
1.6 +    Author:     Johannes Hölzl, TU München
1.7      Author:     Andreas Lochbihler, ETH Zurich
1.8  *)
1.9
1.10 @@ -8,7 +8,6 @@
1.11  theory Probability_Mass_Function
1.12  imports
1.14 -  "~~/src/HOL/Number_Theory/Binomial"
1.15    "~~/src/HOL/Library/Multiset"
1.16  begin
1.17
1.18 @@ -52,14 +51,14 @@
1.19      fix n assume "infinite {x. ?M / Suc n < ?m x}" (is "infinite ?X")
1.20      then obtain X where "finite X" "card X = Suc (Suc n)" "X \<subseteq> ?X"
1.21        by (metis infinite_arbitrarily_large)
1.22 -    from this(3) have *: "\<And>x. x \<in> X \<Longrightarrow> ?M / Suc n \<le> ?m x"
1.23 +    from this(3) have *: "\<And>x. x \<in> X \<Longrightarrow> ?M / Suc n \<le> ?m x"
1.24        by auto
1.25      { fix x assume "x \<in> X"
1.26        from `?M \<noteq> 0` *[OF this] have "?m x \<noteq> 0" by (auto simp: field_simps measure_le_0_iff)
1.27        then have "{x} \<in> sets M" by (auto dest: measure_notin_sets) }
1.28      note singleton_sets = this
1.29      have "?M < (\<Sum>x\<in>X. ?M / Suc n)"
1.30 -      using `?M \<noteq> 0`
1.31 +      using `?M \<noteq> 0`
1.32        by (simp add: `card X = Suc (Suc n)` real_eq_of_nat[symmetric] real_of_nat_Suc field_simps less_le measure_nonneg)
1.33      also have "\<dots> \<le> (\<Sum>x\<in>X. ?m x)"
1.34        by (rule setsum_mono) fact
1.35 @@ -82,7 +81,7 @@
1.36    assume "\<exists>S. countable S \<and> (AE x in M. x \<in> S)"
1.37    then obtain S where S[intro]: "countable S" and ae: "AE x in M. x \<in> S"
1.38      by auto
1.39 -  then have "emeasure M (\<Union>x\<in>{x\<in>S. emeasure M {x} \<noteq> 0}. {x}) =
1.40 +  then have "emeasure M (\<Union>x\<in>{x\<in>S. emeasure M {x} \<noteq> 0}. {x}) =
1.41      (\<integral>\<^sup>+ x. emeasure M {x} * indicator {x\<in>S. emeasure M {x} \<noteq> 0} x \<partial>count_space UNIV)"
1.42      by (subst emeasure_UN_countable)
1.43         (auto simp: disjoint_family_on_def nn_integral_restrict_space[symmetric] restrict_count_space)
1.44 @@ -136,7 +135,7 @@
1.45  interpretation pmf_as_measure .
1.46
1.47  lemma sets_measure_pmf[simp]: "sets (measure_pmf p) = UNIV"
1.48 -  by transfer blast
1.49 +  by transfer blast
1.50
1.51  lemma sets_measure_pmf_count_space[measurable_cong]:
1.52    "sets (measure_pmf M) = sets (count_space UNIV)"
1.53 @@ -353,10 +352,10 @@
1.54
1.55    have [measurable]: "g \<in> measurable f (subprob_algebra (count_space UNIV))"
1.56      by (auto simp: measurable_def space_subprob_algebra prob_space_imp_subprob_space g)
1.57 -
1.58 +
1.59    show "prob_space (f \<guillemotright>= g)"
1.60      using g by (intro f.prob_space_bind[where S="count_space UNIV"]) auto
1.61 -  then interpret fg: prob_space "f \<guillemotright>= g" .
1.62 +  then interpret fg: prob_space "f \<guillemotright>= g" .
1.63    show [simp]: "sets (f \<guillemotright>= g) = UNIV"
1.64      using sets_eq_imp_space_eq[OF s_f]
1.65      by (subst sets_bind[where N="count_space UNIV"]) auto
1.66 @@ -385,7 +384,7 @@
1.67    by transfer (simp add: bind_const' prob_space_imp_subprob_space)
1.68
1.69  lemma set_bind_pmf[simp]: "set_pmf (bind_pmf M N) = (\<Union>M\<in>set_pmf M. set_pmf (N M))"
1.70 -  unfolding set_pmf_eq ereal_eq_0(1)[symmetric] ereal_pmf_bind
1.71 +  unfolding set_pmf_eq ereal_eq_0(1)[symmetric] ereal_pmf_bind
1.72    by (auto simp add: nn_integral_0_iff_AE AE_measure_pmf_iff set_pmf_eq not_le less_le pmf_nonneg)
1.73
1.74  lemma bind_pmf_cong:
1.75 @@ -415,7 +414,7 @@
1.76    using measurable_measure_pmf[of N]
1.77    unfolding measure_pmf_bind
1.78    by (subst emeasure_bind[where N="count_space UNIV"]) auto
1.79 -
1.80 +
1.81  lift_definition return_pmf :: "'a \<Rightarrow> 'a pmf" is "return (count_space UNIV)"
1.82    by (auto intro!: prob_space_return simp: AE_return measure_return)
1.83
1.84 @@ -451,7 +450,7 @@
1.85  proof -
1.86    have "rel_fun op = (rel_fun pmf_as_measure.cr_pmf pmf_as_measure.cr_pmf)
1.87       (\<lambda>f M. M \<guillemotright>= (return (count_space UNIV) o f)) map_pmf"
1.88 -    unfolding map_pmf_def[abs_def] comp_def by transfer_prover
1.89 +    unfolding map_pmf_def[abs_def] comp_def by transfer_prover
1.90    then show ?thesis
1.91      by (force simp: rel_fun_def cr_pmf_def bind_return_distr)
1.92  qed
1.93 @@ -468,7 +467,7 @@
1.94    using map_pmf_id unfolding id_def .
1.95
1.96  lemma map_pmf_compose: "map_pmf (f \<circ> g) = map_pmf f \<circ> map_pmf g"
1.97 -  by (rule, transfer) (simp add: distr_distr[symmetric, where N="count_space UNIV"] measurable_def)
1.98 +  by (rule, transfer) (simp add: distr_distr[symmetric, where N="count_space UNIV"] measurable_def)
1.99
1.100  lemma map_pmf_comp: "map_pmf f (map_pmf g M) = map_pmf (\<lambda>x. f (g x)) M"
1.101    using map_pmf_compose[of f g] by (simp add: comp_def)
1.102 @@ -665,7 +664,7 @@
1.103    show "M = density (count_space UNIV) (\<lambda>x. ereal (measure M {x}))"
1.104    proof (rule measure_eqI)
1.105      fix A :: "'a set"
1.106 -    have "(\<integral>\<^sup>+ x. ereal (measure M {x}) * indicator A x \<partial>count_space UNIV) =
1.107 +    have "(\<integral>\<^sup>+ x. ereal (measure M {x}) * indicator A x \<partial>count_space UNIV) =
1.108        (\<integral>\<^sup>+ x. emeasure M {x} * indicator (A \<inter> {x. measure M {x} \<noteq> 0}) x \<partial>count_space UNIV)"
1.109        by (auto intro!: nn_integral_cong simp: emeasure_eq_measure split: split_indicator)
1.110      also have "\<dots> = (\<integral>\<^sup>+ x. emeasure M {x} \<partial>count_space (A \<inter> {x. measure M {x} \<noteq> 0}))"
1.111 @@ -706,9 +705,9 @@
1.112
1.113  setup_lifting td_pmf_embed_pmf
1.114
1.115 -lemma set_pmf_transfer[transfer_rule]:
1.116 +lemma set_pmf_transfer[transfer_rule]:
1.117    assumes "bi_total A"
1.118 -  shows "rel_fun (pcr_pmf A) (rel_set A) (\<lambda>f. {x. f x \<noteq> 0}) set_pmf"
1.119 +  shows "rel_fun (pcr_pmf A) (rel_set A) (\<lambda>f. {x. f x \<noteq> 0}) set_pmf"
1.120    using `bi_total A`
1.121    by (auto simp: pcr_pmf_def cr_pmf_def rel_fun_def rel_set_def bi_total_def Bex_def set_pmf_iff)
1.122       metis+
1.123 @@ -888,14 +887,14 @@
1.124  inductive rel_pmf :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a pmf \<Rightarrow> 'b pmf \<Rightarrow> bool"
1.125  for R p q
1.126  where
1.127 -  "\<lbrakk> \<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> R x y;
1.128 +  "\<lbrakk> \<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> R x y;
1.129       map_pmf fst pq = p; map_pmf snd pq = q \<rbrakk>
1.130    \<Longrightarrow> rel_pmf R p q"
1.131
1.132  bnf pmf: "'a pmf" map: map_pmf sets: set_pmf bd : "natLeq" rel: rel_pmf
1.133  proof -
1.134    show "map_pmf id = id" by (rule map_pmf_id)
1.135 -  show "\<And>f g. map_pmf (f \<circ> g) = map_pmf f \<circ> map_pmf g" by (rule map_pmf_compose)
1.136 +  show "\<And>f g. map_pmf (f \<circ> g) = map_pmf f \<circ> map_pmf g" by (rule map_pmf_compose)
1.137    show "\<And>f g::'a \<Rightarrow> 'b. \<And>p. (\<And>x. x \<in> set_pmf p \<Longrightarrow> f x = g x) \<Longrightarrow> map_pmf f p = map_pmf g p"
1.138      by (intro map_pmf_cong refl)
1.139
1.140 @@ -1042,7 +1041,7 @@
1.141                     map_pair)
1.142  qed
1.143
1.144 -lemma rel_pmf_reflI:
1.145 +lemma rel_pmf_reflI:
1.146    assumes "\<And>x. x \<in> set_pmf p \<Longrightarrow> P x x"
1.147    shows "rel_pmf P p p"
1.148    by (rule rel_pmf.intros[where pq="map_pmf (\<lambda>x. (x, x)) p"])
1.149 @@ -1089,7 +1088,7 @@
1.150      and q: "q = map_pmf snd pq"
1.151      and P: "\<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> rel_pmf P x y"
1.152      by cases auto
1.153 -  from P obtain PQ
1.154 +  from P obtain PQ
1.155      where PQ: "\<And>x y a b. \<lbrakk> (x, y) \<in> set_pmf pq; (a, b) \<in> set_pmf (PQ x y) \<rbrakk> \<Longrightarrow> P a b"
1.156      and x: "\<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> map_pmf fst (PQ x y) = x"
1.157      and y: "\<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> map_pmf snd (PQ x y) = y"
1.158 @@ -1112,12 +1111,12 @@
1.159
1.160  text {*
1.161    Proof that @{const rel_pmf} preserves orders.
1.162 -  Antisymmetry proof follows Thm. 1 in N. Saheb-Djahromi, Cpo's of measures for nondeterminism,
1.163 -  Theoretical Computer Science 12(1):19--37, 1980,
1.164 +  Antisymmetry proof follows Thm. 1 in N. Saheb-Djahromi, Cpo's of measures for nondeterminism,
1.165 +  Theoretical Computer Science 12(1):19--37, 1980,
1.166    @{url "http://dx.doi.org/10.1016/0304-3975(80)90003-1"}
1.167  *}
1.168
1.169 -lemma
1.170 +lemma
1.171    assumes *: "rel_pmf R p q"
1.172    and refl: "reflp R" and trans: "transp R"
1.173    shows measure_Ici: "measure p {y. R x y} \<le> measure q {y. R x y}" (is ?thesis1)
1.174 @@ -1174,7 +1173,7 @@
1.175      hence "measure (measure_pmf p) (?E x) \<noteq> 0"
1.176        by (auto simp add: measure_pmf.prob_eq_0 AE_measure_pmf_iff intro: reflpD[OF \<open>reflp R\<close>])
1.177      hence "measure (measure_pmf q) (?E x) \<noteq> 0" using eq by simp
1.178 -    hence "set_pmf q \<inter> {y. R x y \<and> R y x} \<noteq> {}"
1.179 +    hence "set_pmf q \<inter> {y. R x y \<and> R y x} \<noteq> {}"
1.180        by (auto simp add: measure_pmf.prob_eq_0 AE_measure_pmf_iff) }
1.181    ultimately show "inf R R\<inverse>\<inverse> x y"
1.182      by (auto simp add: pq_def)
1.183 @@ -1235,13 +1234,13 @@
1.184  lemma set_pmf_bernoulli: "0 < p \<Longrightarrow> p < 1 \<Longrightarrow> set_pmf (bernoulli_pmf p) = UNIV"
1.185    by (auto simp add: set_pmf_iff UNIV_bool)
1.186
1.187 -lemma nn_integral_bernoulli_pmf[simp]:
1.188 +lemma nn_integral_bernoulli_pmf[simp]:
1.189    assumes [simp]: "0 \<le> p" "p \<le> 1" "\<And>x. 0 \<le> f x"
1.190    shows "(\<integral>\<^sup>+x. f x \<partial>bernoulli_pmf p) = f True * p + f False * (1 - p)"
1.191    by (subst nn_integral_measure_pmf_support[of UNIV])
1.192       (auto simp: UNIV_bool field_simps)
1.193
1.194 -lemma integral_bernoulli_pmf[simp]:
1.195 +lemma integral_bernoulli_pmf[simp]:
1.196    assumes [simp]: "0 \<le> p" "p \<le> 1"
1.197    shows "(\<integral>x. f x \<partial>bernoulli_pmf p) = f True * p + f False * (1 - p)"
1.198    by (subst integral_measure_pmf[of UNIV]) (auto simp: UNIV_bool)
1.199 @@ -1277,7 +1276,7 @@
1.200
1.201  lift_definition pmf_of_multiset :: "'a pmf" is "\<lambda>x. count M x / size M"
1.202  proof
1.203 -  show "(\<integral>\<^sup>+ x. ereal (real (count M x) / real (size M)) \<partial>count_space UNIV) = 1"
1.204 +  show "(\<integral>\<^sup>+ x. ereal (real (count M x) / real (size M)) \<partial>count_space UNIV) = 1"
1.205      using M_not_empty
1.206      by (simp add: zero_less_divide_iff nn_integral_count_space nonempty_has_size
1.207                    setsum_divide_distrib[symmetric])
1.208 @@ -1300,7 +1299,7 @@
1.209
1.210  lift_definition pmf_of_set :: "'a pmf" is "\<lambda>x. indicator S x / card S"
1.211  proof
1.212 -  show "(\<integral>\<^sup>+ x. ereal (indicator S x / real (card S)) \<partial>count_space UNIV) = 1"
1.213 +  show "(\<integral>\<^sup>+ x. ereal (indicator S x / real (card S)) \<partial>count_space UNIV) = 1"
1.214      using S_not_empty S_finite by (subst nn_integral_count_space'[of S]) auto
1.215  qed simp
1.216
```