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