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
```