src/HOL/Probability/Borel_Space.thy
changeset 50244 de72bbe42190
parent 50104 de19856feb54
child 50245 dea9363887a6
     1.1 --- a/src/HOL/Probability/Borel_Space.thy	Thu Nov 22 10:09:54 2012 +0100
     1.2 +++ b/src/HOL/Probability/Borel_Space.thy	Tue Nov 27 11:29:47 2012 +0100
     1.3 @@ -53,7 +53,7 @@
     1.4  
     1.5  lemma borel_singleton[measurable]:
     1.6    "A \<in> sets borel \<Longrightarrow> insert x A \<in> sets (borel :: 'a::t1_space measure)"
     1.7 -  unfolding insert_def by (rule Un) auto
     1.8 +  unfolding insert_def by (rule sets.Un) auto
     1.9  
    1.10  lemma borel_comp[measurable]: "A \<in> sets borel \<Longrightarrow> - A \<in> sets borel"
    1.11    unfolding Compl_eq_Diff_UNIV by simp
    1.12 @@ -180,7 +180,7 @@
    1.13  
    1.14  lemma borel_sigma_sets_subset:
    1.15    "A \<subseteq> sets borel \<Longrightarrow> sigma_sets UNIV A \<subseteq> sets borel"
    1.16 -  using sigma_sets_subset[of A borel] by simp
    1.17 +  using sets.sigma_sets_subset[of A borel] by simp
    1.18  
    1.19  lemma borel_eq_sigmaI1:
    1.20    fixes F :: "'i \<Rightarrow> 'a::topological_space set" and X :: "'a::topological_space set set"
    1.21 @@ -276,7 +276,8 @@
    1.22      by blast
    1.23    show "S \<in> ?SIGMA"
    1.24      unfolding *
    1.25 -    by (safe intro!: countable_UN Int countable_INT) (auto intro!: halfspace_gt_in_halfspace)
    1.26 +    by (safe intro!: sets.countable_UN sets.Int sets.countable_INT)
    1.27 +      (auto intro!: halfspace_gt_in_halfspace)
    1.28  qed auto
    1.29  
    1.30  lemma borel_eq_halfspace_le:
    1.31 @@ -299,7 +300,7 @@
    1.32      finally show "x$$i < a" .
    1.33    qed
    1.34    show "{x. x$$i < a} \<in> ?SIGMA" unfolding *
    1.35 -    by (safe intro!: countable_UN) auto
    1.36 +    by (safe intro!: sets.countable_UN) auto
    1.37  qed auto
    1.38  
    1.39  lemma borel_eq_halfspace_ge:
    1.40 @@ -308,7 +309,7 @@
    1.41  proof (rule borel_eq_sigmaI2[OF borel_eq_halfspace_less])
    1.42    fix a i have *: "{x::'a. x$$i < a} = space ?SIGMA - {x::'a. a \<le> x$$i}" by auto
    1.43    show "{x. x$$i < a} \<in> ?SIGMA" unfolding *
    1.44 -      by (safe intro!: compl_sets) auto
    1.45 +      by (safe intro!: sets.compl_sets) auto
    1.46  qed auto
    1.47  
    1.48  lemma borel_eq_halfspace_greater:
    1.49 @@ -317,7 +318,7 @@
    1.50  proof (rule borel_eq_sigmaI2[OF borel_eq_halfspace_le])
    1.51    fix a i have *: "{x::'a. x$$i \<le> a} = space ?SIGMA - {x::'a. a < x$$i}" by auto
    1.52    show "{x. x$$i \<le> a} \<in> ?SIGMA" unfolding *
    1.53 -    by (safe intro!: compl_sets) auto
    1.54 +    by (safe intro!: sets.compl_sets) auto
    1.55  qed auto
    1.56  
    1.57  lemma borel_eq_atMost:
    1.58 @@ -337,7 +338,7 @@
    1.59          by (auto intro!: exI[of _ k])
    1.60      qed
    1.61      show "{x. x$$i \<le> a} \<in> ?SIGMA" unfolding *
    1.62 -      by (safe intro!: countable_UN) auto
    1.63 +      by (safe intro!: sets.countable_UN) auto
    1.64    qed (auto intro: sigma_sets_top sigma_sets.Empty)
    1.65  qed auto
    1.66  
    1.67 @@ -363,7 +364,7 @@
    1.68      qed
    1.69      finally show "{x. x$$i \<le> a} \<in> ?SIGMA"
    1.70        apply (simp only:)
    1.71 -      apply (safe intro!: countable_UN Diff)
    1.72 +      apply (safe intro!: sets.countable_UN sets.Diff)
    1.73        apply (auto intro: sigma_sets_top)
    1.74        done
    1.75    qed (auto intro: sigma_sets_top sigma_sets.Empty)
    1.76 @@ -391,7 +392,7 @@
    1.77      qed
    1.78      finally show "{x. a \<le> x$$i} \<in> ?SIGMA"
    1.79        apply (simp only:)
    1.80 -      apply (safe intro!: countable_UN Diff)
    1.81 +      apply (safe intro!: sets.countable_UN sets.Diff)
    1.82        apply (auto intro: sigma_sets_top)
    1.83        done
    1.84    qed (auto intro: sigma_sets_top sigma_sets.Empty)
    1.85 @@ -415,7 +416,7 @@
    1.86        by (auto intro!: exI[of _ k])
    1.87    qed
    1.88    show "{..a} \<in> ?SIGMA" unfolding *
    1.89 -    by (safe intro!: countable_UN)
    1.90 +    by (safe intro!: sets.countable_UN)
    1.91         (auto intro!: sigma_sets_top)
    1.92  qed auto
    1.93  
    1.94 @@ -427,7 +428,7 @@
    1.95    then have "open M" by simp
    1.96    show "M \<in> ?SIGMA"
    1.97      apply (subst open_UNION[OF `open M`])
    1.98 -    apply (safe intro!: countable_UN)
    1.99 +    apply (safe intro!: sets.countable_UN)
   1.100      apply auto
   1.101      done
   1.102  qed auto