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
```