src/HOL/Probability/ex/Dining_Cryptographers.thy
changeset 39099 5c714fd55b1e
parent 38656 d5d342611edb
child 40859 de0b30e6c2d2
equal deleted inserted replaced
39098:21e9bd6cf0a8 39099:5c714fd55b1e
    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)"