24 sublocale finite_space \<subseteq> finite_information_space M \<mu> 2 |
24 sublocale finite_space \<subseteq> finite_information_space M \<mu> 2 |
25 proof (rule finite_information_spaceI) |
25 proof (rule finite_information_spaceI) |
26 let ?measure = "\<lambda>s::'a set. real (card s) / real (card S)" |
26 let ?measure = "\<lambda>s::'a set. real (card s) / real (card S)" |
27 |
27 |
28 show "finite_measure_space M \<mu>" |
28 show "finite_measure_space M \<mu>" |
29 proof (rule finite_Pow_additivity_sufficient, simp_all) |
29 proof (rule finite_measure_spaceI) |
30 show "positive \<mu>" by (simp add: positive_def) |
30 fix A B :: "'a set" assume "A \<inter> B = {}" "A \<subseteq> space M" "B \<subseteq> space M" |
31 |
31 then show "\<mu> (A \<union> B) = \<mu> A + \<mu> B" |
32 show "additive M \<mu>" |
32 by (simp add: inverse_eq_divide field_simps Real_real |
33 by (simp add: additive_def inverse_eq_divide field_simps Real_real |
|
34 divide_le_0_iff zero_le_divide_iff |
33 divide_le_0_iff zero_le_divide_iff |
35 card_Un_disjoint finite_subset[OF _ finite]) |
34 card_Un_disjoint finite_subset[OF _ finite]) |
36 qed |
35 qed auto |
37 qed simp_all |
36 qed simp_all |
38 |
37 |
39 lemma set_of_list_extend: |
38 lemma set_of_list_extend: |
40 "{xs. length xs = Suc n \<and> (\<forall>x\<in>set xs. x \<in> A)} = |
39 "{xs. length xs = Suc n \<and> (\<forall>x\<in>set xs. x \<in> A)} = |
41 (\<lambda>(xs, n). n#xs) ` ({xs. length xs = n \<and> (\<forall>x\<in>set xs. x \<in> A)} \<times> A)" |
40 (\<lambda>(xs, n). n#xs) ` ({xs. length xs = n \<and> (\<forall>x\<in>set xs. x \<in> A)} \<times> A)" |