# HG changeset patch
# User hoelzl
# Date 1322744637 -3600
# Node ID 852597248663e4f9326aa9615c1a5842edfc21c9
# Parent  a2c32e196d49d507b817431f6a8176cab1bb5fd4
moved theorems about distribution to the definition; removed oopsed-lemma

diff -r a2c32e196d49 -r 852597248663 src/HOL/Probability/Information.thy
--- a/src/HOL/Probability/Information.thy	Thu Dec 01 14:03:57 2011 +0100
+++ b/src/HOL/Probability/Information.thy	Thu Dec 01 14:03:57 2011 +0100
@@ -1009,17 +1009,6 @@
     by (simp add: setsum_cartesian_product' distribution_remove_const)
 qed
 
-lemma (in prob_space) distribution_unit[simp]: "distribution (\<lambda>x. ()) {()} = 1"
-  unfolding distribution_def using prob_space by auto
-
-lemma (in prob_space) joint_distribution_unit[simp]: "distribution (\<lambda>x. (X x, ())) {(a, ())} = distribution X {a}"
-  unfolding distribution_def by (auto intro!: arg_cong[where f=\<mu>'])
-
-lemma (in prob_space) setsum_distribution:
-  assumes X: "finite_random_variable MX X" shows "(\<Sum>a\<in>space MX. distribution X {a}) = 1"
-  using setsum_joint_distribution[OF assms, of "\<lparr> space = UNIV, sets = Pow UNIV \<rparr>" "\<lambda>x. ()" "{()}"]
-  using sigma_algebra_Pow[of "UNIV::unit set" "()"] by simp
-
 lemma (in information_space) conditional_mutual_information_generic_positive:
   assumes X: "finite_random_variable MX X" and Y: "finite_random_variable MY Y" and Z: "finite_random_variable MZ Z"
   shows "0 \<le> conditional_mutual_information b MX MY MZ X Y Z"
diff -r a2c32e196d49 -r 852597248663 src/HOL/Probability/Probability_Measure.thy
--- a/src/HOL/Probability/Probability_Measure.thy	Thu Dec 01 14:03:57 2011 +0100
+++ b/src/HOL/Probability/Probability_Measure.thy	Thu Dec 01 14:03:57 2011 +0100
@@ -70,6 +70,12 @@
     "joint_distribution X X {(x, x)} = distribution X {x}"
   unfolding distribution_def by (auto intro!: arg_cong[where f=\<mu>'])
 
+lemma (in prob_space) distribution_unit[simp]: "distribution (\<lambda>x. ()) {()} = 1"
+  unfolding distribution_def using prob_space by auto
+
+lemma (in prob_space) joint_distribution_unit[simp]: "distribution (\<lambda>x. (X x, ())) {(a, ())} = distribution X {a}"
+  unfolding distribution_def by (auto intro!: arg_cong[where f=\<mu>'])
+
 lemma (in prob_space) not_empty: "space M \<noteq> {}"
   using prob_space empty_measure' by auto
 
@@ -743,6 +749,11 @@
     finite_random_variableD[OF Y(1)]
     finite_random_variable_imp_sets[OF Y]] by simp
 
+lemma (in prob_space) setsum_distribution:
+  assumes X: "finite_random_variable MX X" shows "(\<Sum>a\<in>space MX. distribution X {a}) = 1"
+  using setsum_joint_distribution[OF assms, of "\<lparr> space = UNIV, sets = Pow UNIV \<rparr>" "\<lambda>x. ()" "{()}"]
+  using sigma_algebra_Pow[of "UNIV::unit set" "()"] by simp
+
 locale pair_finite_prob_space = M1: finite_prob_space M1 + M2: finite_prob_space M2 for M1 M2
 
 sublocale pair_finite_prob_space \<subseteq> pair_prob_space M1 M2 by default
diff -r a2c32e196d49 -r 852597248663 src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy
--- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Thu Dec 01 14:03:57 2011 +0100
+++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy	Thu Dec 01 14:03:57 2011 +0100
@@ -75,13 +75,6 @@
   qed
 qed
 
-lemma (in prob_space)
-  assumes "finite (X`space M)"
-  shows "bij_betw (ordered_variable_partition X) {0..<card (X`space M)} (X`space M)"
-  and "\<And>i j. \<lbrakk> i < card (X`space M) ; j < card (X`space M) ; i \<le> j \<rbrakk> \<Longrightarrow>
-    distribution X {ordered_variable_partition X i} \<le> distribution X {ordered_variable_partition X j}"
-  oops
-
 definition (in prob_space)
   "order_distribution X i = real (distribution X {ordered_variable_partition X i})"