author hoelzl Fri Jan 21 11:39:26 2011 +0100 (2011-01-21) changeset 41660 7795aaab6038 parent 41659 a5d1b2df5e97 child 41661 baf1964bc468
use AE_mp in AE_conjI proof
```     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
```