author hoelzl Fri, 16 Nov 2012 14:46:23 +0100 changeset 50098 98abff4a775b parent 50097 32973da2d4f7 child 50099 a58bb401af80
rules for AE and prob
```--- a/src/HOL/Probability/Probability_Measure.thy	Fri Nov 16 14:46:23 2012 +0100
+++ b/src/HOL/Probability/Probability_Measure.thy	Fri Nov 16 14:46:23 2012 +0100
@@ -219,6 +219,17 @@
with AE_in_set_eq_1 assms show ?thesis by simp
qed

+lemma (in prob_space) AE_const[simp]: "(AE x in M. P) \<longleftrightarrow> P"
+  by (cases P) (auto simp: AE_False)
+
+lemma (in prob_space) AE_contr:
+  assumes ae: "AE \<omega> in M. P \<omega>" "AE \<omega> in M. \<not> P \<omega>"
+  shows False
+proof -
+  from ae have "AE \<omega> in M. False" by eventually_elim auto
+  then show False by auto
+qed
+
lemma (in finite_measure) prob_space_increasing: "increasing M (measure M)"
by (auto intro!: finite_measure_mono simp: increasing_def)

@@ -438,6 +449,23 @@
then show ?thesis by simp

+lemma (in prob_space) prob_Collect_eq_0:
+  "{x \<in> space M. P x} \<in> sets M \<Longrightarrow> \<P>(x in M. P x) = 0 \<longleftrightarrow> (AE x in M. \<not> P x)"
+  using AE_iff_measurable[OF _ refl, of M "\<lambda>x. \<not> P x"] by (simp add: emeasure_eq_measure)
+
+lemma (in prob_space) prob_Collect_eq_1:
+  "{x \<in> space M. P x} \<in> sets M \<Longrightarrow> \<P>(x in M. P x) = 1 \<longleftrightarrow> (AE x in M. P x)"
+  using AE_in_set_eq_1[of "{x\<in>space M. P x}"] by simp
+
+lemma (in prob_space) prob_eq_0:
+  "A \<in> sets M \<Longrightarrow> prob A = 0 \<longleftrightarrow> (AE x in M. x \<notin> A)"
+  using AE_iff_measurable[OF _ refl, of M "\<lambda>x. x \<notin> A"]
+  by (auto simp add: emeasure_eq_measure Int_def[symmetric])
+
+lemma (in prob_space) prob_eq_1:
+  "A \<in> sets M \<Longrightarrow> prob A = 1 \<longleftrightarrow> (AE x in M. x \<in> A)"
+  using AE_in_set_eq_1[of A] by simp
+
lemma (in prob_space) prob_sums:
assumes P: "\<And>n. {x\<in>space M. P n x} \<in> events"
assumes Q: "{x\<in>space M. Q x} \<in> events"```