tuned: use induction rule sigma_sets_induct_disjoint
authorhoelzl
Mon Nov 19 18:01:48 2012 +0100 (2012-11-19 ago)
changeset 501254319691be975
parent 50124 4161c834c2fd
child 50126 3dec88149176
tuned: use induction rule sigma_sets_induct_disjoint
src/HOL/Probability/Projective_Limit.thy
src/HOL/Probability/Regularity.thy
     1.1 --- a/src/HOL/Probability/Projective_Limit.thy	Mon Nov 19 16:09:11 2012 +0100
     1.2 +++ b/src/HOL/Probability/Projective_Limit.thy	Mon Nov 19 18:01:48 2012 +0100
     1.3 @@ -157,8 +157,7 @@
     1.4    thus "\<exists>r'. subseq r' \<and> (\<exists>l. (\<lambda>i. ((f \<circ> (s \<circ> r')) i)\<^isub>F n) ----> l)" by (auto simp: o_def)
     1.5  qed
     1.6  
     1.7 -lemma (in finmap_seqs_into_compact)
     1.8 -  diagonal_tendsto: "\<exists>l. (\<lambda>i. (f (diagseq i))\<^isub>F n) ----> l"
     1.9 +lemma (in finmap_seqs_into_compact) diagonal_tendsto: "\<exists>l. (\<lambda>i. (f (diagseq i))\<^isub>F n) ----> l"
    1.10  proof -
    1.11    have "\<And>i n0. (f o seqseq i) i = f (diagseq i)" unfolding diagseq_def by simp
    1.12    from reducer_reduces obtain l where l: "(\<lambda>i. ((f \<circ> seqseq (Suc n)) i)\<^isub>F n) ----> l"
    1.13 @@ -191,8 +190,7 @@
    1.14  
    1.15  abbreviation "lim\<^isub>B \<equiv> (\<lambda>J P. limP J (\<lambda>_. borel) P)"
    1.16  
    1.17 -lemma
    1.18 -  emeasure_limB_emb_not_empty:
    1.19 +lemma emeasure_limB_emb_not_empty:
    1.20    assumes "I \<noteq> {}"
    1.21    assumes X: "J \<noteq> {}" "J \<subseteq> I" "finite J" "\<forall>i\<in>J. B i \<in> sets borel"
    1.22    shows "emeasure (lim\<^isub>B I P) (emb I J (Pi\<^isub>E J B)) = emeasure (lim\<^isub>B J P) (Pi\<^isub>E J B)"
    1.23 @@ -691,8 +689,7 @@
    1.24  sublocale polish_product_prob_space \<subseteq> P: polish_projective I "\<lambda>J. PiM J (\<lambda>_. borel::('a) measure)"
    1.25  proof qed
    1.26  
    1.27 -lemma (in polish_product_prob_space)
    1.28 -  limP_eq_PiM:
    1.29 +lemma (in polish_product_prob_space) limP_eq_PiM:
    1.30    "I \<noteq> {} \<Longrightarrow> lim\<^isub>P I (\<lambda>_. borel) (\<lambda>J. PiM J (\<lambda>_. borel::('a) measure)) =
    1.31      PiM I (\<lambda>_. borel)"
    1.32    by (rule PiM_eq) (auto simp: emeasure_PiM emeasure_limB_emb)
     2.1 --- a/src/HOL/Probability/Regularity.thy	Mon Nov 19 16:09:11 2012 +0100
     2.2 +++ b/src/HOL/Probability/Regularity.thy	Mon Nov 19 18:01:48 2012 +0100
     2.3 @@ -210,11 +210,9 @@
     2.4      ultimately
     2.5      show "?thesis e " by (auto simp: sU)
     2.6    qed
     2.7 -  have closed_in_D: "\<And>A. closed A \<Longrightarrow> ?inner A \<and> ?outer A"
     2.8 -  proof
     2.9 -    fix A::"'a set" assume "closed A" hence "A \<in> sets borel" by (simp add: compact_imp_closed)
    2.10 +  { fix A::"'a set" assume "closed A" hence "A \<in> sets borel" by (simp add: compact_imp_closed)
    2.11      hence [simp]: "A \<in> sets M" by (simp add: sb)
    2.12 -    show "?inner A"
    2.13 +    have "?inner A"
    2.14      proof (rule approx_inner)
    2.15        fix e::real assume "e > 0"
    2.16        from approx_space[OF this] obtain K where
    2.17 @@ -237,7 +235,7 @@
    2.18        ultimately show "\<exists>K \<subseteq> A. compact K \<and> emeasure M A \<le> emeasure M K + ereal e"
    2.19          by blast
    2.20      qed simp
    2.21 -    show "?outer A"
    2.22 +    have "?outer A"
    2.23      proof cases
    2.24        assume "A \<noteq> {}"
    2.25        let ?G = "\<lambda>d. {x. infdist x A < d}"
    2.26 @@ -288,25 +286,25 @@
    2.27          by (rule INF_greatest) (auto intro!: emeasure_mono simp: sb)
    2.28        ultimately show ?thesis by simp
    2.29      qed (auto intro!: ereal_INFI)
    2.30 -  qed
    2.31 -  let ?D = "{B \<in> sets M. ?inner B \<and> ?outer B}"
    2.32 -  interpret dynkin: dynkin_system "space M" ?D
    2.33 -  proof (rule dynkin_systemI)
    2.34 -    have "{U::'a set. space M \<subseteq> U \<and> open U} = {space M}" by (auto simp add: sU)
    2.35 -    hence "?outer (space M)" by (simp add: min_def INF_def)
    2.36 -    moreover
    2.37 -    have "?inner (space M)"
    2.38 -    proof (rule ereal_approx_SUP)
    2.39 -      fix e::real assume "0 < e"
    2.40 -      thus "\<exists>K\<in>{K. K \<subseteq> space M \<and> compact K}. emeasure M (space M) \<le> emeasure M K + ereal e"
    2.41 -        by (rule approx_space)
    2.42 -    qed (auto intro: emeasure_mono simp: sU sb intro!: exI[where x="{}"])
    2.43 -    ultimately show "space M \<in> ?D" by (simp add: sU sb)
    2.44 +    note `?inner A` `?outer A` }
    2.45 +  note closed_in_D = this
    2.46 +  from `B \<in> sets borel`
    2.47 +  have "Int_stable (Collect closed)" "Collect closed \<subseteq> Pow UNIV" "B \<in> sigma_sets UNIV (Collect closed)" 
    2.48 +    by (auto simp: Int_stable_def borel_eq_closed)
    2.49 +  then show "?inner B" "?outer B"
    2.50 +  proof (induct B rule: sigma_sets_induct_disjoint)
    2.51 +    case empty
    2.52 +    { case 1 show ?case by (intro ereal_SUPI[symmetric]) auto }
    2.53 +    { case 2 show ?case by (intro ereal_INFI[symmetric]) (auto elim!: meta_allE[of _ "{}"]) }
    2.54    next
    2.55 -    fix B assume "B \<in> ?D" thus "B \<subseteq> space M" by (simp add: sU)
    2.56 -    from `B \<in> ?D` have [simp]: "B \<in> sets M" and "?inner B" "?outer B" by auto
    2.57 -    hence inner: "emeasure M B = (SUP K:{K. K \<subseteq> B \<and> compact K}. emeasure M K)"
    2.58 -      and outer: "emeasure M B = (INF U:{U. B \<subseteq> U \<and> open U}. emeasure M U)" by auto
    2.59 +    case (basic B)
    2.60 +    { case 1 from basic closed_in_D show ?case by auto }
    2.61 +    { case 2 from basic closed_in_D show ?case by auto }
    2.62 +  next
    2.63 +    case (compl B)
    2.64 +    note inner = compl(2) and outer = compl(3)
    2.65 +    from compl have [simp]: "B \<in> sets M" by (auto simp: sb borel_eq_closed)
    2.66 +    case 2
    2.67      have "M (space M - B) = M (space M) - emeasure M B" by (auto simp: emeasure_compl)
    2.68      also have "\<dots> = (INF K:{K. K \<subseteq> B \<and> compact K}. M (space M) -  M K)"
    2.69        unfolding inner by (subst INFI_ereal_cminus) force+
    2.70 @@ -315,7 +313,7 @@
    2.71      also have "\<dots> \<ge> (INF U:{U. U \<subseteq> B \<and> closed U}. M (space M - U))"
    2.72        by (rule INF_superset_mono) (auto simp add: compact_imp_closed)
    2.73      also have "(INF U:{U. U \<subseteq> B \<and> closed U}. M (space M - U)) =
    2.74 -      (INF U:{U. space M - B \<subseteq> U \<and> open U}. emeasure M U)"
    2.75 +        (INF U:{U. space M - B \<subseteq> U \<and> open U}. emeasure M U)"
    2.76        by (subst INF_image[of "\<lambda>u. space M - u", symmetric])
    2.77           (rule INF_cong, auto simp add: sU intro!: INF_cong)
    2.78      finally have
    2.79 @@ -323,41 +321,39 @@
    2.80      moreover have
    2.81        "(INF U:{U. space M - B \<subseteq> U \<and> open U}. emeasure M U) \<ge> emeasure M (space M - B)"
    2.82        by (auto simp: sb sU intro!: INF_greatest emeasure_mono)
    2.83 -    ultimately have "?outer (space M - B)" by simp
    2.84 -    moreover
    2.85 -    {
    2.86 -      have "M (space M - B) = M (space M) - emeasure M B" by (auto simp: emeasure_compl)
    2.87 -      also have "\<dots> = (SUP U: {U. B \<subseteq> U \<and> open U}. M (space M) -  M U)"
    2.88 -        unfolding outer by (subst SUPR_ereal_cminus) auto
    2.89 -      also have "\<dots> = (SUP U:{U. B \<subseteq> U \<and> open U}. M (space M - U))"
    2.90 -        by (rule SUP_cong) (auto simp add: emeasure_compl sb compact_imp_closed)
    2.91 -      also have "\<dots> = (SUP K:{K. K \<subseteq> space M - B \<and> closed K}. emeasure M K)"
    2.92 -        by (subst SUP_image[of "\<lambda>u. space M - u", symmetric])
    2.93 -           (rule SUP_cong, auto simp: sU)
    2.94 -      also have "\<dots> = (SUP K:{K. K \<subseteq> space M - B \<and> compact K}. emeasure M K)"
    2.95 -      proof (safe intro!: antisym SUP_least)
    2.96 -        fix K assume "closed K" "K \<subseteq> space M - B"
    2.97 -        from closed_in_D[OF `closed K`]
    2.98 -        have K_inner: "emeasure M K = (SUP K:{Ka. Ka \<subseteq> K \<and> compact Ka}. emeasure M K)" by simp
    2.99 -        show "emeasure M K \<le> (SUP K:{K. K \<subseteq> space M - B \<and> compact K}. emeasure M K)"
   2.100 -          unfolding K_inner using `K \<subseteq> space M - B`
   2.101 -          by (auto intro!: SUP_upper SUP_least)
   2.102 -      qed (fastforce intro!: SUP_least SUP_upper simp: compact_imp_closed)
   2.103 -      finally have "?inner (space M - B)" .
   2.104 -    } hence "?inner (space M - B)" .
   2.105 -    ultimately show "space M - B \<in> ?D" by auto
   2.106 +    ultimately show ?case by (auto intro!: antisym simp: sets_eq_imp_space_eq[OF sb])
   2.107 +
   2.108 +    case 1
   2.109 +    have "M (space M - B) = M (space M) - emeasure M B" by (auto simp: emeasure_compl)
   2.110 +    also have "\<dots> = (SUP U: {U. B \<subseteq> U \<and> open U}. M (space M) -  M U)"
   2.111 +      unfolding outer by (subst SUPR_ereal_cminus) auto
   2.112 +    also have "\<dots> = (SUP U:{U. B \<subseteq> U \<and> open U}. M (space M - U))"
   2.113 +      by (rule SUP_cong) (auto simp add: emeasure_compl sb compact_imp_closed)
   2.114 +    also have "\<dots> = (SUP K:{K. K \<subseteq> space M - B \<and> closed K}. emeasure M K)"
   2.115 +      by (subst SUP_image[of "\<lambda>u. space M - u", symmetric])
   2.116 +         (rule SUP_cong, auto simp: sU)
   2.117 +    also have "\<dots> = (SUP K:{K. K \<subseteq> space M - B \<and> compact K}. emeasure M K)"
   2.118 +    proof (safe intro!: antisym SUP_least)
   2.119 +      fix K assume "closed K" "K \<subseteq> space M - B"
   2.120 +      from closed_in_D[OF `closed K`]
   2.121 +      have K_inner: "emeasure M K = (SUP K:{Ka. Ka \<subseteq> K \<and> compact Ka}. emeasure M K)" by simp
   2.122 +      show "emeasure M K \<le> (SUP K:{K. K \<subseteq> space M - B \<and> compact K}. emeasure M K)"
   2.123 +        unfolding K_inner using `K \<subseteq> space M - B`
   2.124 +        by (auto intro!: SUP_upper SUP_least)
   2.125 +    qed (fastforce intro!: SUP_least SUP_upper simp: compact_imp_closed)
   2.126 +    finally show ?case by (auto intro!: antisym simp: sets_eq_imp_space_eq[OF sb])
   2.127    next
   2.128 -    fix D :: "nat \<Rightarrow> _"
   2.129 -    assume "range D \<subseteq> ?D" hence "range D \<subseteq> sets M" by auto
   2.130 -    moreover assume "disjoint_family D"
   2.131 -    ultimately have M[symmetric]: "(\<Sum>i. M (D i)) = M (\<Union>i. D i)" by (rule suminf_emeasure)
   2.132 +    case (union D)
   2.133 +    then have "range D \<subseteq> sets M" by (auto simp: sb borel_eq_closed)
   2.134 +    with union have M[symmetric]: "(\<Sum>i. M (D i)) = M (\<Union>i. D i)" by (intro suminf_emeasure)
   2.135      also have "(\<lambda>n. \<Sum>i\<in>{0..<n}. M (D i)) ----> (\<Sum>i. M (D i))"
   2.136        by (intro summable_sumr_LIMSEQ_suminf summable_ereal_pos emeasure_nonneg)
   2.137      finally have measure_LIMSEQ: "(\<lambda>n. \<Sum>i = 0..<n. measure M (D i)) ----> measure M (\<Union>i. D i)"
   2.138        by (simp add: emeasure_eq_measure)
   2.139      have "(\<Union>i. D i) \<in> sets M" using `range D \<subseteq> sets M` by auto
   2.140 -    moreover
   2.141 -    hence "?inner (\<Union>i. D i)"
   2.142 +    
   2.143 +    case 1
   2.144 +    show ?case
   2.145      proof (rule approx_inner)
   2.146        fix e::real assume "e > 0"
   2.147        with measure_LIMSEQ
   2.148 @@ -379,7 +375,7 @@
   2.149          fix i
   2.150          from `0 < e` have "0 < e/(2*Suc n0)" by (auto intro: divide_pos_pos)
   2.151          have "emeasure M (D i) = (SUP K:{K. K \<subseteq> (D i) \<and> compact K}. emeasure M K)"
   2.152 -          using `range D \<subseteq> ?D` by blast
   2.153 +          using union by blast
   2.154          from SUP_approx_ereal[OF `0 < e/(2*Suc n0)` this]
   2.155          show "\<exists>K. K \<subseteq> D i \<and> compact K \<and> emeasure M (D i) \<le> emeasure M K + e/(2*Suc n0)"
   2.156            by (auto simp: emeasure_eq_measure)
   2.157 @@ -410,8 +406,9 @@
   2.158        ultimately
   2.159        have "?K\<subseteq>(\<Union>i. D i) \<and> compact ?K \<and> emeasure M (\<Union>i. D i) \<le> emeasure M ?K + ereal e" by simp
   2.160        thus "\<exists>K\<subseteq>\<Union>i. D i. compact K \<and> emeasure M (\<Union>i. D i) \<le> emeasure M K + ereal e" ..
   2.161 -    qed
   2.162 -    moreover have "?outer (\<Union>i. D i)"
   2.163 +    qed fact
   2.164 +    case 2
   2.165 +    show ?case
   2.166      proof (rule approx_outer[OF `(\<Union>i. D i) \<in> sets M`])
   2.167        fix e::real assume "e > 0"
   2.168        have "\<forall>i::nat. \<exists>U. D i \<subseteq> U \<and> open U \<and> e/(2 powr Suc i) > emeasure M U - emeasure M (D i)"
   2.169 @@ -419,7 +416,7 @@
   2.170          fix i::nat
   2.171          from `0 < e` have "0 < e/(2 powr Suc i)" by (auto intro: divide_pos_pos)
   2.172          have "emeasure M (D i) = (INF U:{U. (D i) \<subseteq> U \<and> open U}. emeasure M U)"
   2.173 -          using `range D \<subseteq> ?D` by blast
   2.174 +          using union by blast
   2.175          from INF_approx_ereal[OF `0 < e/(2 powr Suc i)` this]
   2.176          show "\<exists>U. D i \<subseteq> U \<and> open U \<and> e/(2 powr Suc i) > emeasure M U - emeasure M (D i)"
   2.177            by (auto simp: emeasure_eq_measure)
   2.178 @@ -455,20 +452,7 @@
   2.179        have "(\<Union>i. D i) \<subseteq> ?U \<and> open ?U \<and> emeasure M ?U \<le> emeasure M (\<Union>i. D i) + ereal e" by simp
   2.180        thus "\<exists>B. (\<Union>i. D i) \<subseteq> B \<and> open B \<and> emeasure M B \<le> emeasure M (\<Union>i. D i) + ereal e" ..
   2.181      qed
   2.182 -    ultimately show "(\<Union>i. D i) \<in> ?D" by safe
   2.183    qed
   2.184 -  have "sets borel = sigma_sets (space M) (Collect closed)" by (simp add: borel_eq_closed sU)
   2.185 -  also have "\<dots> = dynkin (space M) (Collect closed)"
   2.186 -  proof (rule sigma_eq_dynkin)
   2.187 -    show "Collect closed \<subseteq> Pow (space M)" using Sigma_Algebra.sets_into_space by (auto simp: sU)
   2.188 -    show "Int_stable (Collect closed)" by (auto simp: Int_stable_def)
   2.189 -  qed
   2.190 -  also have "\<dots> \<subseteq> ?D" using closed_in_D
   2.191 -    by (intro dynkin.dynkin_subset) (auto simp add: compact_imp_closed sb)
   2.192 -  finally have "sets borel \<subseteq> ?D" .
   2.193 -  moreover have "?D \<subseteq> sets borel" by (auto simp: sb)
   2.194 -  ultimately have "sets borel = ?D" by simp
   2.195 -  with assms show "?inner B" and "?outer B" by auto
   2.196  qed
   2.197  
   2.198  end