# HG changeset patch
# User hoelzl
# Date 1295606366 -3600
# Node ID 7795aaab603875be8f097d4bfbd34c6627d8961a
# Parent  a5d1b2df5e9760bee5e0975f0f3b8b70f302154c
use AE_mp in AE_conjI proof

diff -r a5d1b2df5e97 -r 7795aaab6038 src/HOL/Probability/Measure.thy
--- 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