src/HOL/Probability/Information.thy
changeset 45777 c36637603821
parent 45712 852597248663
child 46731 5302e932d1e5
     1.1 --- a/src/HOL/Probability/Information.thy	Mon Dec 05 15:10:15 2011 +0100
     1.2 +++ b/src/HOL/Probability/Information.thy	Wed Dec 07 15:10:29 2011 +0100
     1.3 @@ -198,7 +198,7 @@
     1.4  proof -
     1.5    interpret \<nu>: prob_space "M\<lparr>measure := \<nu>\<rparr>" by fact
     1.6    have ms: "measure_space (M\<lparr>measure := \<nu>\<rparr>)" by default
     1.7 -  have fms: "finite_measure (M\<lparr>measure := \<nu>\<rparr>)" by default
     1.8 +  have fms: "finite_measure (M\<lparr>measure := \<nu>\<rparr>)" by unfold_locales
     1.9    note RN = RN_deriv[OF ms ac]
    1.10  
    1.11    from real_RN_deriv[OF fms ac] guess D . note D = this
    1.12 @@ -460,7 +460,7 @@
    1.13  proof -
    1.14    interpret information_space M by default fact
    1.15    interpret v: finite_prob_space "M\<lparr>measure := \<nu>\<rparr>" by fact
    1.16 -  have ps: "prob_space (M\<lparr>measure := \<nu>\<rparr>)" by default
    1.17 +  have ps: "prob_space (M\<lparr>measure := \<nu>\<rparr>)" by unfold_locales
    1.18    from KL_ge_0[OF this ac v.integral_finite_singleton(1)] show ?thesis .
    1.19  qed
    1.20  
    1.21 @@ -558,7 +558,7 @@
    1.22  
    1.23    have eq: "\<forall>A\<in>sets XY.P. (ereal \<circ> joint_distribution X Y) A = XY.\<mu> A"
    1.24    proof (rule XY.KL_eq_0_imp)
    1.25 -    show "prob_space ?J" by default
    1.26 +    show "prob_space ?J" by unfold_locales
    1.27      show "XY.absolutely_continuous (ereal\<circ>joint_distribution X Y)"
    1.28        using ac by (simp add: P_def)
    1.29      show "integrable ?J (entropy_density b XY.P (ereal\<circ>joint_distribution X Y))"
    1.30 @@ -624,7 +624,7 @@
    1.31      have "prob_space (P.P\<lparr> measure := ereal\<circ>joint_distribution X Y\<rparr>)"
    1.32        using X Y by (auto intro!: distribution_prob_space random_variable_pairI)
    1.33      then show "measure_space (P.P\<lparr> measure := ereal\<circ>joint_distribution X Y\<rparr>)"
    1.34 -      unfolding prob_space_def by simp
    1.35 +      unfolding prob_space_def finite_measure_def sigma_finite_measure_def by simp
    1.36    qed auto
    1.37  qed
    1.38  
    1.39 @@ -654,7 +654,7 @@
    1.40    note rv = assms[THEN finite_random_variableD]
    1.41    show "XY.absolutely_continuous (ereal\<circ>joint_distribution X Y)"
    1.42    proof (rule XY.absolutely_continuousI)
    1.43 -    show "finite_measure_space (XY.P\<lparr> measure := ereal\<circ>joint_distribution X Y\<rparr>)" by default
    1.44 +    show "finite_measure_space (XY.P\<lparr> measure := ereal\<circ>joint_distribution X Y\<rparr>)" by unfold_locales
    1.45      fix x assume "x \<in> space XY.P" and "XY.\<mu> {x} = 0"
    1.46      then obtain a b where "x = (a, b)"
    1.47        and "distribution X {a} = 0 \<or> distribution Y {b} = 0"
    1.48 @@ -684,8 +684,8 @@
    1.49    interpret P: finite_prob_space "XY.P\<lparr>measure := ereal\<circ>joint_distribution X Y\<rparr>"
    1.50      using assms by (auto intro!: joint_distribution_finite_prob_space)
    1.51  
    1.52 -  have P_ms: "finite_measure_space (XY.P\<lparr>measure := ereal\<circ>joint_distribution X Y\<rparr>)" by default
    1.53 -  have P_ps: "finite_prob_space (XY.P\<lparr>measure := ereal\<circ>joint_distribution X Y\<rparr>)" by default
    1.54 +  have P_ms: "finite_measure_space (XY.P\<lparr>measure := ereal\<circ>joint_distribution X Y\<rparr>)" by unfold_locales
    1.55 +  have P_ps: "finite_prob_space (XY.P\<lparr>measure := ereal\<circ>joint_distribution X Y\<rparr>)" by unfold_locales
    1.56  
    1.57    show ?sum
    1.58      unfolding Let_def mutual_information_def