use AE_mp in AE_conjI proof
authorhoelzl
Fri Jan 21 11:39:26 2011 +0100 (2011-01-21)
changeset 416607795aaab6038
parent 41659 a5d1b2df5e97
child 41661 baf1964bc468
use AE_mp in AE_conjI proof
src/HOL/Probability/Measure.thy
     1.1 --- a/src/HOL/Probability/Measure.thy	Wed Jan 19 17:44:53 2011 +0100
     1.2 +++ b/src/HOL/Probability/Measure.thy	Fri Jan 21 11:39:26 2011 +0100
     1.3 @@ -803,23 +803,17 @@
     1.4  lemma (in measure_space) AE_conjI:
     1.5    assumes AE_P: "AE x. P x" and AE_Q: "AE x. Q x"
     1.6    shows "AE x. P x \<and> Q x"
     1.7 -proof -
     1.8 -  from AE_P obtain A where P: "{x\<in>space M. \<not> P x} \<subseteq> A"
     1.9 -    and A: "A \<in> sets M" "\<mu> A = 0"
    1.10 -    by (auto elim!: AE_E)
    1.11 -
    1.12 -  from AE_Q obtain B where Q: "{x\<in>space M. \<not> Q x} \<subseteq> B"
    1.13 -    and B: "B \<in> sets M" "\<mu> B = 0"
    1.14 -    by (auto elim!: AE_E)
    1.15 +  apply (rule AE_mp[OF AE_P])
    1.16 +  apply (rule AE_mp[OF AE_Q])
    1.17 +  by simp
    1.18  
    1.19 -  show ?thesis
    1.20 -  proof (intro AE_I)
    1.21 -    show "A \<union> B \<in> sets M" "\<mu> (A \<union> B) = 0" using A B
    1.22 -      using measure_subadditive[of A B] by auto
    1.23 -    show "{x\<in>space M. \<not> (P x \<and> Q x)} \<subseteq> A \<union> B"
    1.24 -      using P Q by auto
    1.25 -  qed
    1.26 -qed
    1.27 +lemma (in measure_space) AE_conj_iff[simp]:
    1.28 +  shows "(AE x. P x \<and> Q x) \<longleftrightarrow> (AE x. P x) \<and> (AE x. Q x)"
    1.29 +proof (intro conjI iffI AE_conjI)
    1.30 +  assume *: "AE x. P x \<and> Q x"
    1.31 +  from * show "AE x. P x" by (rule AE_mp) auto
    1.32 +  from * show "AE x. Q x" by (rule AE_mp) auto
    1.33 +qed auto
    1.34  
    1.35  lemma (in measure_space) AE_E2:
    1.36    assumes "AE x. P x" "{x\<in>space M. P x} \<in> sets M"
    1.37 @@ -845,14 +839,6 @@
    1.38      by (rule AE_mp[OF AE_space]) auto
    1.39  qed
    1.40  
    1.41 -lemma (in measure_space) AE_conj_iff[simp]:
    1.42 -  shows "(AE x. P x \<and> Q x) \<longleftrightarrow> (AE x. P x) \<and> (AE x. Q x)"
    1.43 -proof (intro conjI iffI AE_conjI)
    1.44 -  assume *: "AE x. P x \<and> Q x"
    1.45 -  from * show "AE x. P x" by (rule AE_mp) auto
    1.46 -  from * show "AE x. Q x" by (rule AE_mp) auto
    1.47 -qed auto
    1.48 -
    1.49  lemma (in measure_space) all_AE_countable:
    1.50    "(\<forall>i::'i::countable. AE x. P i x) \<longleftrightarrow> (AE x. \<forall>i. P i x)"
    1.51  proof