src/HOL/Probability/Probability_Mass_Function.thy
 changeset 58606 9c66f7c541fb parent 58587 5484f6079bcd child 58730 b3fd0628f849
```     1.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Mon Oct 06 21:21:46 2014 +0200
1.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Tue Oct 07 10:34:24 2014 +0200
1.3 @@ -1,20 +1,10 @@
1.4 +(*  Title:      HOL/Probability/Probability_Mass_Function.thy
1.5 +    Author:     Johannes Hölzl, TU München *)
1.6 +
1.7  theory Probability_Mass_Function
1.8    imports Probability_Measure
1.9  begin
1.10
1.11 -lemma sets_Pair: "{x} \<in> sets M1 \<Longrightarrow> {y} \<in> sets M2 \<Longrightarrow> {(x, y)} \<in> sets (M1 \<Otimes>\<^sub>M M2)"
1.12 -  using pair_measureI[of "{x}" M1 "{y}" M2] by simp
1.13 -
1.14 -lemma finite_subset_card:
1.15 -  assumes X: "infinite X" shows "\<exists>A\<subseteq>X. finite A \<and> card A = n"
1.16 -proof (induct n)
1.17 -  case (Suc n) then guess A .. note A = this
1.18 -  with X obtain x where "x \<in> X" "x \<notin> A"
1.19 -    by (metis subset_antisym subset_eq)
1.20 -  with A show ?case
1.21 -    by (intro exI[of _ "insert x A"]) auto
1.22 -qed (simp cong: conj_cong)
1.23 -
1.24  lemma (in prob_space) countable_support:
1.25    "countable {x. measure M {x} \<noteq> 0}"
1.26  proof -
1.27 @@ -25,7 +15,7 @@
1.28    proof (rule ccontr)
1.29      fix n assume "infinite {x. inverse (Suc n) < ?m x}" (is "infinite ?X")
1.30      then obtain X where "finite X" "card X = Suc (Suc n)" "X \<subseteq> ?X"
1.31 -      by (metis finite_subset_card)
1.32 +      by (metis infinite_arbitrarily_large)
1.33      from this(3) have *: "\<And>x. x \<in> X \<Longrightarrow> 1 / Suc n \<le> ?m x"
1.34        by (auto simp: inverse_eq_divide)
1.35      { fix x assume "x \<in> X"
1.36 @@ -46,17 +36,10 @@
1.37      unfolding * by (intro countable_UN countableI_type countable_finite[OF **])
1.38  qed
1.39
1.40 -lemma measure_count_space: "measure (count_space A) X = (if X \<subseteq> A then card X else 0)"
1.41 -  unfolding measure_def
1.42 -  by (cases "finite X") (simp_all add: emeasure_notin_sets)
1.43 -
1.44  typedef 'a pmf = "{M :: 'a measure. prob_space M \<and> sets M = UNIV \<and> (AE x in M. measure M {x} \<noteq> 0)}"
1.45    morphisms measure_pmf Abs_pmf
1.46 -  apply (intro exI[of _ "uniform_measure (count_space UNIV) {undefined}"])
1.47 -  apply (auto intro!: prob_space_uniform_measure simp: measure_count_space)
1.48 -  apply (subst uniform_measure_def)
1.49 -  apply (simp add: AE_density AE_count_space split: split_indicator)
1.50 -  done
1.51 +  by (intro exI[of _ "uniform_measure (count_space UNIV) {undefined}"])
1.52 +     (auto intro!: prob_space_uniform_measure AE_uniform_measureI)
1.53
1.54  declare [[coercion measure_pmf]]
1.55
```