src/HOL/Probability/Measure_Space.thy
changeset 53374 a14d2a854c02
parent 51351 dd1dd470690b
child 54417 dbb8ecfe1337
     1.1 --- a/src/HOL/Probability/Measure_Space.thy	Tue Sep 03 00:51:08 2013 +0200
     1.2 +++ b/src/HOL/Probability/Measure_Space.thy	Tue Sep 03 01:12:40 2013 +0200
     1.3 @@ -158,7 +158,8 @@
     1.4        and A: "A`S \<subseteq> M"
     1.5        and disj: "disjoint_family_on A S"
     1.6    shows  "(\<Sum>i\<in>S. f (A i)) = f (\<Union>i\<in>S. A i)"
     1.7 -using `finite S` disj A proof induct
     1.8 +  using `finite S` disj A
     1.9 +proof induct
    1.10    case empty show ?case using f by (simp add: positive_def)
    1.11  next
    1.12    case (insert s S)
    1.13 @@ -168,7 +169,6 @@
    1.14    have "A s \<in> M" using insert by blast
    1.15    moreover have "(\<Union>i\<in>S. A i) \<in> M"
    1.16      using insert `finite S` by auto
    1.17 -  moreover
    1.18    ultimately have "f (A s \<union> (\<Union>i\<in>S. A i)) = f (A s) + f(\<Union>i\<in>S. A i)"
    1.19      using ad UNION_in_sets A by (auto simp add: additive_def)
    1.20    with insert show ?case using ad disjoint_family_on_mono[of S "insert s S" A]
    1.21 @@ -781,15 +781,15 @@
    1.22      using sets.sets_into_space by auto
    1.23    show "{} \<in> null_sets M"
    1.24      by auto
    1.25 -  fix A B assume sets: "A \<in> null_sets M" "B \<in> null_sets M"
    1.26 -  then have "A \<in> sets M" "B \<in> sets M"
    1.27 +  fix A B assume null_sets: "A \<in> null_sets M" "B \<in> null_sets M"
    1.28 +  then have sets: "A \<in> sets M" "B \<in> sets M"
    1.29      by auto
    1.30 -  moreover then have "emeasure M (A \<union> B) \<le> emeasure M A + emeasure M B"
    1.31 +  then have *: "emeasure M (A \<union> B) \<le> emeasure M A + emeasure M B"
    1.32      "emeasure M (A - B) \<le> emeasure M A"
    1.33      by (auto intro!: emeasure_subadditive emeasure_mono)
    1.34 -  moreover have "emeasure M B = 0" "emeasure M A = 0"
    1.35 -    using sets by auto
    1.36 -  ultimately show "A - B \<in> null_sets M" "A \<union> B \<in> null_sets M"
    1.37 +  then have "emeasure M B = 0" "emeasure M A = 0"
    1.38 +    using null_sets by auto
    1.39 +  with sets * show "A - B \<in> null_sets M" "A \<union> B \<in> null_sets M"
    1.40      by (auto intro!: antisym)
    1.41  qed
    1.42  
    1.43 @@ -1563,9 +1563,9 @@
    1.44          by (auto intro!: Lim_eventually eventually_sequentiallyI[where c=i])
    1.45      next
    1.46        assume "\<not> (\<exists>i. \<forall>j\<ge>i. F i = F j)"
    1.47 -      then obtain f where "\<And>i. i \<le> f i" "\<And>i. F i \<noteq> F (f i)" by metis
    1.48 -      moreover then have "\<And>i. F i \<subseteq> F (f i)" using `incseq F` by (auto simp: incseq_def)
    1.49 -      ultimately have *: "\<And>i. F i \<subset> F (f i)" by auto
    1.50 +      then obtain f where f: "\<And>i. i \<le> f i" "\<And>i. F i \<noteq> F (f i)" by metis
    1.51 +      then have "\<And>i. F i \<subseteq> F (f i)" using `incseq F` by (auto simp: incseq_def)
    1.52 +      with f have *: "\<And>i. F i \<subset> F (f i)" by auto
    1.53  
    1.54        have "incseq (\<lambda>i. ?M (F i))"
    1.55          using `incseq F` unfolding incseq_def by (auto simp: card_mono dest: finite_subset)