diff -r 340df9f3491f -r 22f665a2e91c src/HOL/Probability/Radon_Nikodym.thy --- a/src/HOL/Probability/Radon_Nikodym.thy Sun Sep 11 22:56:05 2011 +0200 +++ b/src/HOL/Probability/Radon_Nikodym.thy Mon Sep 12 07:55:43 2011 +0200 @@ -32,7 +32,7 @@ show ?thesis proof (safe intro!: bexI[of _ ?h] del: notI) have "\i. A i \ sets M" - using range by fastsimp+ + using range by fastforce+ then have "integral\<^isup>P M ?h = (\i. n i * \ (A i))" using pos by (simp add: positive_integral_suminf positive_integral_cmult_indicator) also have "\ \ (\i. (1 / 2)^Suc i)" @@ -640,7 +640,7 @@ have Union: "(SUP i. \ (?O i)) = \ (\i. ?O i)" proof (rule continuity_from_below[of ?O]) show "range ?O \ sets M" using Q' by (auto intro!: finite_UN) - show "incseq ?O" by (fastsimp intro!: incseq_SucI) + show "incseq ?O" by (fastforce intro!: incseq_SucI) qed have Q'_sets: "\i. Q' i \ sets M" using Q' by auto have O_sets: "\i. ?O i \ sets M" @@ -654,7 +654,7 @@ also have "\ < \" using Q' by (simp add: setsum_Pinfty) finally show "\ (?O i) \ \" by simp qed auto - have O_mono: "\n. ?O n \ ?O (Suc n)" by fastsimp + have O_mono: "\n. ?O n \ ?O (Suc n)" by fastforce have a_eq: "?a = \ (\i. ?O i)" unfolding Union[symmetric] proof (rule antisym) show "?a \ (SUP i. \ (?O i))" unfolding a_Lim @@ -676,7 +676,7 @@ show ?thesis proof (intro bexI exI conjI ballI impI allI) show "disjoint_family Q" - by (fastsimp simp: disjoint_family_on_def Q_def + by (fastforce simp: disjoint_family_on_def Q_def split: nat.split_asm) show "range Q \ sets M" using Q_sets by auto @@ -697,7 +697,7 @@ proof (rule continuity_from_below[of "\i. ?O i \ A", symmetric, simplified]) show "range (\i. ?O i \ A) \ sets M" using `\ A \ \` O_sets A by auto - qed (fastsimp intro!: incseq_SucI) + qed (fastforce intro!: incseq_SucI) also have "\ \ ?a" proof (safe intro!: SUP_leI) fix i have "?O i \ A \ ?Q" @@ -734,14 +734,14 @@ case 0 then show ?case by (simp add: Q_def) next case (Suc j) - have eq: "\j. (\i\j. ?O i) = (\i\j. Q' i)" by fastsimp + have eq: "\j. (\i\j. ?O i) = (\i\j. Q' i)" by fastforce have "{..j} \ {..Suc j} = {..Suc j}" by auto then have "(\i\Suc j. Q' i) = (\i\j. Q' i) \ Q (Suc j)" by (simp add: UN_Un[symmetric] Q_def del: UN_Un) then show ?case using Suc by (auto simp add: eq atMost_Suc) qed } then have "(\j. (\i\j. ?O i)) = (\j. (\i\j. Q i))" by simp - then show "space M - ?O_0 = space M - (\i. Q i)" by fastsimp + then show "space M - ?O_0 = space M - (\i. Q i)" by fastforce qed qed