author hoelzl Fri, 21 Jan 2011 11:39:26 +0100 changeset 41660 7795aaab6038 parent 41659 a5d1b2df5e97 child 41661 baf1964bc468
use AE_mp in AE_conjI proof
```--- a/src/HOL/Probability/Measure.thy	Wed Jan 19 17:44:53 2011 +0100
+++ b/src/HOL/Probability/Measure.thy	Fri Jan 21 11:39:26 2011 +0100
@@ -803,23 +803,17 @@
lemma (in measure_space) AE_conjI:
assumes AE_P: "AE x. P x" and AE_Q: "AE x. Q x"
shows "AE x. P x \<and> Q x"
-proof -
-  from AE_P obtain A where P: "{x\<in>space M. \<not> P x} \<subseteq> A"
-    and A: "A \<in> sets M" "\<mu> A = 0"
-    by (auto elim!: AE_E)
-
-  from AE_Q obtain B where Q: "{x\<in>space M. \<not> Q x} \<subseteq> B"
-    and B: "B \<in> sets M" "\<mu> B = 0"
-    by (auto elim!: AE_E)
+  apply (rule AE_mp[OF AE_P])
+  apply (rule AE_mp[OF AE_Q])
+  by simp

-  show ?thesis
-  proof (intro AE_I)
-    show "A \<union> B \<in> sets M" "\<mu> (A \<union> B) = 0" using A B
-      using measure_subadditive[of A B] by auto
-    show "{x\<in>space M. \<not> (P x \<and> Q x)} \<subseteq> A \<union> B"
-      using P Q by auto
-  qed
-qed
+lemma (in measure_space) AE_conj_iff[simp]:
+  shows "(AE x. P x \<and> Q x) \<longleftrightarrow> (AE x. P x) \<and> (AE x. Q x)"
+proof (intro conjI iffI AE_conjI)
+  assume *: "AE x. P x \<and> Q x"
+  from * show "AE x. P x" by (rule AE_mp) auto
+  from * show "AE x. Q x" by (rule AE_mp) auto
+qed auto

lemma (in measure_space) AE_E2:
assumes "AE x. P x" "{x\<in>space M. P x} \<in> sets M"
@@ -845,14 +839,6 @@
by (rule AE_mp[OF AE_space]) auto
qed

-lemma (in measure_space) AE_conj_iff[simp]:
-  shows "(AE x. P x \<and> Q x) \<longleftrightarrow> (AE x. P x) \<and> (AE x. Q x)"
-proof (intro conjI iffI AE_conjI)
-  assume *: "AE x. P x \<and> Q x"
-  from * show "AE x. P x" by (rule AE_mp) auto
-  from * show "AE x. Q x" by (rule AE_mp) auto
-qed auto
-
lemma (in measure_space) all_AE_countable:
"(\<forall>i::'i::countable. AE x. P i x) \<longleftrightarrow> (AE x. \<forall>i. P i x)"
proof```