src/HOL/Probability/Radon_Nikodym.thy
changeset 44890 22f665a2e91c
parent 44568 e6f291cb5810
child 44918 6a80fbc4e72c
     1.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Sun Sep 11 22:56:05 2011 +0200
     1.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Mon Sep 12 07:55:43 2011 +0200
     1.3 @@ -32,7 +32,7 @@
     1.4    show ?thesis
     1.5    proof (safe intro!: bexI[of _ ?h] del: notI)
     1.6      have "\<And>i. A i \<in> sets M"
     1.7 -      using range by fastsimp+
     1.8 +      using range by fastforce+
     1.9      then have "integral\<^isup>P M ?h = (\<Sum>i. n i * \<mu> (A i))" using pos
    1.10        by (simp add: positive_integral_suminf positive_integral_cmult_indicator)
    1.11      also have "\<dots> \<le> (\<Sum>i. (1 / 2)^Suc i)"
    1.12 @@ -640,7 +640,7 @@
    1.13    have Union: "(SUP i. \<mu> (?O i)) = \<mu> (\<Union>i. ?O i)"
    1.14    proof (rule continuity_from_below[of ?O])
    1.15      show "range ?O \<subseteq> sets M" using Q' by (auto intro!: finite_UN)
    1.16 -    show "incseq ?O" by (fastsimp intro!: incseq_SucI)
    1.17 +    show "incseq ?O" by (fastforce intro!: incseq_SucI)
    1.18    qed
    1.19    have Q'_sets: "\<And>i. Q' i \<in> sets M" using Q' by auto
    1.20    have O_sets: "\<And>i. ?O i \<in> sets M"
    1.21 @@ -654,7 +654,7 @@
    1.22      also have "\<dots> < \<infinity>" using Q' by (simp add: setsum_Pinfty)
    1.23      finally show "\<nu> (?O i) \<noteq> \<infinity>" by simp
    1.24    qed auto
    1.25 -  have O_mono: "\<And>n. ?O n \<subseteq> ?O (Suc n)" by fastsimp
    1.26 +  have O_mono: "\<And>n. ?O n \<subseteq> ?O (Suc n)" by fastforce
    1.27    have a_eq: "?a = \<mu> (\<Union>i. ?O i)" unfolding Union[symmetric]
    1.28    proof (rule antisym)
    1.29      show "?a \<le> (SUP i. \<mu> (?O i))" unfolding a_Lim
    1.30 @@ -676,7 +676,7 @@
    1.31    show ?thesis
    1.32    proof (intro bexI exI conjI ballI impI allI)
    1.33      show "disjoint_family Q"
    1.34 -      by (fastsimp simp: disjoint_family_on_def Q_def
    1.35 +      by (fastforce simp: disjoint_family_on_def Q_def
    1.36          split: nat.split_asm)
    1.37      show "range Q \<subseteq> sets M"
    1.38        using Q_sets by auto
    1.39 @@ -697,7 +697,7 @@
    1.40            proof (rule continuity_from_below[of "\<lambda>i. ?O i \<union> A", symmetric, simplified])
    1.41              show "range (\<lambda>i. ?O i \<union> A) \<subseteq> sets M"
    1.42                using `\<nu> A \<noteq> \<infinity>` O_sets A by auto
    1.43 -          qed (fastsimp intro!: incseq_SucI)
    1.44 +          qed (fastforce intro!: incseq_SucI)
    1.45            also have "\<dots> \<le> ?a"
    1.46            proof (safe intro!: SUP_leI)
    1.47              fix i have "?O i \<union> A \<in> ?Q"
    1.48 @@ -734,14 +734,14 @@
    1.49          case 0 then show ?case by (simp add: Q_def)
    1.50        next
    1.51          case (Suc j)
    1.52 -        have eq: "\<And>j. (\<Union>i\<le>j. ?O i) = (\<Union>i\<le>j. Q' i)" by fastsimp
    1.53 +        have eq: "\<And>j. (\<Union>i\<le>j. ?O i) = (\<Union>i\<le>j. Q' i)" by fastforce
    1.54          have "{..j} \<union> {..Suc j} = {..Suc j}" by auto
    1.55          then have "(\<Union>i\<le>Suc j. Q' i) = (\<Union>i\<le>j. Q' i) \<union> Q (Suc j)"
    1.56            by (simp add: UN_Un[symmetric] Q_def del: UN_Un)
    1.57          then show ?case using Suc by (auto simp add: eq atMost_Suc)
    1.58        qed }
    1.59      then have "(\<Union>j. (\<Union>i\<le>j. ?O i)) = (\<Union>j. (\<Union>i\<le>j. Q i))" by simp
    1.60 -    then show "space M - ?O_0 = space M - (\<Union>i. Q i)" by fastsimp
    1.61 +    then show "space M - ?O_0 = space M - (\<Union>i. Q i)" by fastforce
    1.62    qed
    1.63  qed
    1.64