src/HOL/Probability/Borel_Space.thy
changeset 40869 251df82c0088
parent 40859 de0b30e6c2d2
child 40870 94427db32392
     1.1 --- a/src/HOL/Probability/Borel_Space.thy	Wed Dec 01 19:42:09 2010 +0100
     1.2 +++ b/src/HOL/Probability/Borel_Space.thy	Wed Dec 01 20:09:41 2010 +0100
     1.3 @@ -6,12 +6,6 @@
     1.4    imports Sigma_Algebra Positive_Infinite_Real Multivariate_Analysis
     1.5  begin
     1.6  
     1.7 -lemma (in sigma_algebra) sets_sigma_subset:
     1.8 -  assumes "space N = space M"
     1.9 -  assumes "sets N \<subseteq> sets M"
    1.10 -  shows "sets (sigma N) \<subseteq> sets M"
    1.11 -  by (unfold assms sets_sigma, rule sigma_sets_subset, rule assms)
    1.12 -
    1.13  lemma LIMSEQ_max:
    1.14    "u ----> (x::real) \<Longrightarrow> (\<lambda>i. max (u i) 0) ----> max x 0"
    1.15    by (fastsimp intro!: LIMSEQ_I dest!: LIMSEQ_D)
    1.16 @@ -612,13 +606,10 @@
    1.17    then show ?thesis by (intro sets_sigma_subset) auto
    1.18  qed
    1.19  
    1.20 -lemma algebra_eqI: assumes "sets A = sets (B::'a algebra)" "space A = space B"
    1.21 -  shows "A = B" using assms by auto
    1.22 -
    1.23  lemma borel_eq_atMost:
    1.24    "borel = (sigma \<lparr>space=UNIV, sets=range (\<lambda> a. {.. a::'a\<Colon>ordered_euclidean_space})\<rparr>)"
    1.25      (is "_ = ?SIGMA")
    1.26 -proof (rule algebra_eqI, rule antisym)
    1.27 +proof (intro algebra.equality antisym)
    1.28    show "sets borel \<subseteq> sets ?SIGMA"
    1.29      using halfspace_le_span_atMost halfspace_span_halfspace_le open_span_halfspace
    1.30      by auto
    1.31 @@ -629,7 +620,7 @@
    1.32  lemma borel_eq_atLeastAtMost:
    1.33    "borel = (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a :: 'a\<Colon>ordered_euclidean_space, b). {a .. b})\<rparr>)"
    1.34     (is "_ = ?SIGMA")
    1.35 -proof (rule algebra_eqI, rule antisym)
    1.36 +proof (intro algebra.equality antisym)
    1.37    show "sets borel \<subseteq> sets ?SIGMA"
    1.38      using atMost_span_atLeastAtMost halfspace_le_span_atMost
    1.39        halfspace_span_halfspace_le open_span_halfspace
    1.40 @@ -641,7 +632,7 @@
    1.41  lemma borel_eq_greaterThan:
    1.42    "borel = (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a :: 'a\<Colon>ordered_euclidean_space). {a <..})\<rparr>)"
    1.43     (is "_ = ?SIGMA")
    1.44 -proof (rule algebra_eqI, rule antisym)
    1.45 +proof (intro algebra.equality antisym)
    1.46    show "sets borel \<subseteq> sets ?SIGMA"
    1.47      using halfspace_le_span_greaterThan
    1.48        halfspace_span_halfspace_le open_span_halfspace
    1.49 @@ -653,7 +644,7 @@
    1.50  lemma borel_eq_lessThan:
    1.51    "borel = (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a :: 'a\<Colon>ordered_euclidean_space). {..< a})\<rparr>)"
    1.52     (is "_ = ?SIGMA")
    1.53 -proof (rule algebra_eqI, rule antisym)
    1.54 +proof (intro algebra.equality antisym)
    1.55    show "sets borel \<subseteq> sets ?SIGMA"
    1.56      using halfspace_le_span_lessThan
    1.57        halfspace_span_halfspace_ge open_span_halfspace
    1.58 @@ -665,7 +656,7 @@
    1.59  lemma borel_eq_greaterThanLessThan:
    1.60    "borel = (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, b). {a <..< (b :: 'a \<Colon> ordered_euclidean_space)})\<rparr>)"
    1.61      (is "_ = ?SIGMA")
    1.62 -proof (rule algebra_eqI, rule antisym)
    1.63 +proof (intro algebra.equality antisym)
    1.64    show "sets ?SIGMA \<subseteq> sets borel"
    1.65      by (rule borel.sets_sigma_subset) auto
    1.66    show "sets borel \<subseteq> sets ?SIGMA"
    1.67 @@ -686,7 +677,7 @@
    1.68  lemma borel_eq_halfspace_le:
    1.69    "borel = (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x::'a::ordered_euclidean_space. x$$i \<le> a})\<rparr>)"
    1.70     (is "_ = ?SIGMA")
    1.71 -proof (rule algebra_eqI, rule antisym)
    1.72 +proof (intro algebra.equality antisym)
    1.73    show "sets borel \<subseteq> sets ?SIGMA"
    1.74      using open_span_halfspace halfspace_span_halfspace_le by auto
    1.75    show "sets ?SIGMA \<subseteq> sets borel"
    1.76 @@ -696,7 +687,7 @@
    1.77  lemma borel_eq_halfspace_less:
    1.78    "borel = (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x::'a::ordered_euclidean_space. x$$i < a})\<rparr>)"
    1.79     (is "_ = ?SIGMA")
    1.80 -proof (rule algebra_eqI, rule antisym)
    1.81 +proof (intro algebra.equality antisym)
    1.82    show "sets borel \<subseteq> sets ?SIGMA"
    1.83      using open_span_halfspace .
    1.84    show "sets ?SIGMA \<subseteq> sets borel"
    1.85 @@ -706,7 +697,7 @@
    1.86  lemma borel_eq_halfspace_gt:
    1.87    "borel = (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x::'a::ordered_euclidean_space. a < x$$i})\<rparr>)"
    1.88     (is "_ = ?SIGMA")
    1.89 -proof (rule algebra_eqI, rule antisym)
    1.90 +proof (intro algebra.equality antisym)
    1.91    show "sets borel \<subseteq> sets ?SIGMA"
    1.92      using halfspace_le_span_halfspace_gt open_span_halfspace halfspace_span_halfspace_le by auto
    1.93    show "sets ?SIGMA \<subseteq> sets borel"
    1.94 @@ -716,7 +707,7 @@
    1.95  lemma borel_eq_halfspace_ge:
    1.96    "borel = (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x::'a::ordered_euclidean_space. a \<le> x$$i})\<rparr>)"
    1.97     (is "_ = ?SIGMA")
    1.98 -proof (rule algebra_eqI, rule antisym)
    1.99 +proof (intro algebra.equality antisym)
   1.100    show "sets borel \<subseteq> sets ?SIGMA"
   1.101      using halfspace_span_halfspace_ge open_span_halfspace by auto
   1.102    show "sets ?SIGMA \<subseteq> sets borel"