author ballarin Mon, 09 Nov 2009 21:45:24 +0100 changeset 33542 f2d7d4e67447 parent 33541 e716c6ad381b (current diff) parent 33537 06c87d2c5b5a (diff) child 33543 a4dbf0f92d96
Merged.
```--- a/src/HOL/Probability/Borel.thy	Mon Nov 09 21:33:22 2009 +0100
+++ b/src/HOL/Probability/Borel.thy	Mon Nov 09 21:45:24 2009 +0100
@@ -17,8 +17,8 @@

definition mono_convergent where
"mono_convergent u f s \<equiv>
-	(\<forall>x m n. m \<le> n \<and> x \<in> s \<longrightarrow> u m x \<le> u n x) \<and>
-	(\<forall>x \<in> s. (\<lambda>i. u i x) ----> f x)"
+        (\<forall>x m n. m \<le> n \<and> x \<in> s \<longrightarrow> u m x \<le> u n x) \<and>
+        (\<forall>x \<in> s. (\<lambda>i. u i x) ----> f x)"

lemma in_borel_measurable:
"f \<in> borel_measurable M \<longleftrightarrow>
@@ -222,7 +222,7 @@
shows "{w \<in> space M. f w < g w} \<in> sets M"
proof -
have "{w \<in> space M. f w < g w} =
-	(\<Union>r\<in>\<rat>. {w \<in> space M. f w < r} \<inter> {w \<in> space M. r < g w })"
+        (\<Union>r\<in>\<rat>. {w \<in> space M. f w < r} \<inter> {w \<in> space M. r < g w })"
thus ?thesis using f g
by (simp add: borel_measurable_less_iff [of f]
@@ -247,7 +247,7 @@
shows "{w \<in> space M. f w = g w} \<in> sets M"
proof -
have "{w \<in> space M. f w = g w} =
-	{w \<in> space M. f w \<le> g w} \<inter> {w \<in> space M. g w \<le> f w}"
+        {w \<in> space M. f w \<le> g w} \<inter> {w \<in> space M. g w \<le> f w}"
by auto
thus ?thesis using f g
by (simp add: borel_measurable_leq_borel_measurable Int) ```
```--- a/src/HOL/Probability/Caratheodory.thy	Mon Nov 09 21:33:22 2009 +0100
+++ b/src/HOL/Probability/Caratheodory.thy	Mon Nov 09 21:45:24 2009 +0100
@@ -2,7 +2,6 @@

theory Caratheodory
imports Sigma_Algebra SupInf SeriesPlus
-
begin

text{*From the Hurd/Coble measure theory development, translated by Lawrence Paulson.*}
@@ -136,7 +135,7 @@
proof
fix n
show "(\<Sum>i\<Colon>nat = 0\<Colon>nat..<Suc (Suc n). f (binaryset A B i)) = f A + f B"
-	by (induct n)  (auto simp add: binaryset_def f)
+        by (induct n)  (auto simp add: binaryset_def f)
qed
moreover
have "... ----> f A + f B" by (rule LIMSEQ_const)
@@ -198,30 +197,30 @@
proof -
from xl yl show ?thesis
proof (auto simp add: positive_def lambda_system_eq Int)
-	fix u
-	assume x: "x \<in> sets M" and y: "y \<in> sets M" and u: "u \<in> sets M"
+        fix u
+        assume x: "x \<in> sets M" and y: "y \<in> sets M" and u: "u \<in> sets M"
and fx: "\<forall>z\<in>sets M. f (z \<inter> x) + f (z - x) = f z"
and fy: "\<forall>z\<in>sets M. f (z \<inter> y) + f (z - y) = f z"
-	have "u - x \<inter> y \<in> sets M"
-	  by (metis Diff Diff_Int Un u x y)
-	moreover
-	have "(u - (x \<inter> y)) \<inter> y = u \<inter> y - x" by blast
-	moreover
-	have "u - x \<inter> y - y = u - y" by blast
-	ultimately
-	have ey: "f (u - x \<inter> y) = f (u \<inter> y - x) + f (u - y)" using fy
-	  by force
-	have "f (u \<inter> (x \<inter> y)) + f (u - x \<inter> y)
+        have "u - x \<inter> y \<in> sets M"
+          by (metis Diff Diff_Int Un u x y)
+        moreover
+        have "(u - (x \<inter> y)) \<inter> y = u \<inter> y - x" by blast
+        moreover
+        have "u - x \<inter> y - y = u - y" by blast
+        ultimately
+        have ey: "f (u - x \<inter> y) = f (u \<inter> y - x) + f (u - y)" using fy
+          by force
+        have "f (u \<inter> (x \<inter> y)) + f (u - x \<inter> y)
= (f (u \<inter> (x \<inter> y)) + f (u \<inter> y - x)) + f (u - y)"
-	also have "... =  (f ((u \<inter> y) \<inter> x) + f (u \<inter> y - x)) + f (u - y)"
-	also have "... = f (u \<inter> y) + f (u - y)"
-	  using fx [THEN bspec, of "u \<inter> y"] Int y u
-	  by force
-	also have "... = f u"
-	  by (metis fy u)
-	finally show "f (u \<inter> (x \<inter> y)) + f (u - x \<inter> y) = f u" .
+        also have "... =  (f ((u \<inter> y) \<inter> x) + f (u \<inter> y - x)) + f (u - y)"
+        also have "... = f (u \<inter> y) + f (u - y)"
+          using fx [THEN bspec, of "u \<inter> y"] Int y u
+          by force
+        also have "... = f u"
+          by (metis fy u)
+        finally show "f (u \<inter> (x \<inter> y)) + f (u - x \<inter> y) = f u" .
qed
qed

@@ -478,11 +477,11 @@
have U_eq: "f (\<Union>i. A i) = suminf (f o A)"
proof (rule antisym)
show "f (\<Union>i. A i) \<le> suminf (f \<circ> A)"
-	by (rule countably_subadditiveD [OF csa A'' disj U_in sumfA])
+        by (rule countably_subadditiveD [OF csa A'' disj U_in sumfA])
show "suminf (f \<circ> A) \<le> f (\<Union>i. A i)"
-	by (rule suminf_le [OF sumfA])
+        by (rule suminf_le [OF sumfA])
(metis algebra.additive_sum [OF alg_ls] pos disj UN_Un Un_UNIV_right
subset_Un_eq increasingD [OF inc] A' A'' UNION_in_sets U_in)
qed
{
@@ -491,58 +490,58 @@
have "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) = f a"
proof -
have summ: "summable (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A)" using pos A''
-	apply -
-	apply (rule summable_comparison_test [OF _ sumfA])
-	apply (rule_tac x="0" in exI)
-	apply (auto simp add: )
-	apply (subst abs_of_nonneg)
-	apply (metis A'' Int UNIV_I a image_subset_iff)
-	apply (blast intro:  increasingD [OF inc] a)
-	done
+        apply -
+        apply (rule summable_comparison_test [OF _ sumfA])
+        apply (rule_tac x="0" in exI)
+        apply (auto simp add: )
+        apply (subst abs_of_nonneg)
+        apply (metis A'' Int UNIV_I a image_subset_iff)
+        apply (blast intro:  increasingD [OF inc] a)
+        done
show ?thesis
proof (rule antisym)
-	have "range (\<lambda>i. a \<inter> A i) \<subseteq> sets M" using A''
-	  by blast
-	moreover
-	have "disjoint_family (\<lambda>i. a \<inter> A i)" using disj
-	  by (auto simp add: disjoint_family_def)
-	moreover
-	have "a \<inter> (\<Union>i. A i) \<in> sets M"
-	  by (metis Int U_in a)
-	ultimately
-	have "f (a \<inter> (\<Union>i. A i)) \<le> suminf (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A)"
-	  using countably_subadditiveD [OF csa, of "(\<lambda>i. a \<inter> A i)"] summ
-	moreover
-	have "suminf (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A)  \<le> f a - f (a - (\<Union>i. A i))"
-	  proof (rule suminf_le [OF summ])
-	    fix n
-	    have UNION_in: "(\<Union>i\<in>{0..<n}. A i) \<in> sets M"
-	      by (metis A'' UNION_in_sets)
-	    have le_fa: "f (UNION {0..<n} A \<inter> a) \<le> f a" using A''
-	      by (blast intro: increasingD [OF inc] A'' Int UNION_in_sets a)
-	    have ls: "(\<Union>i\<in>{0..<n}. A i) \<in> lambda_system M f"
-	      using algebra.UNION_in_sets [OF lambda_system_algebra [OF pos]]
-	    hence eq_fa: "f (a \<inter> (\<Union>i\<in>{0..<n}. A i)) + f (a - (\<Union>i\<in>{0..<n}. A i)) = f a"
-	      by (simp add: lambda_system_eq UNION_in Diff_Compl a)
-	    have "f (a - (\<Union>i. A i)) \<le> f (a - (\<Union>i\<in>{0..<n}. A i))"
-	      by (blast intro: increasingD [OF inc] Diff UNION_eq_Union_image
+        have "range (\<lambda>i. a \<inter> A i) \<subseteq> sets M" using A''
+          by blast
+        moreover
+        have "disjoint_family (\<lambda>i. a \<inter> A i)" using disj
+          by (auto simp add: disjoint_family_def)
+        moreover
+        have "a \<inter> (\<Union>i. A i) \<in> sets M"
+          by (metis Int U_in a)
+        ultimately
+        have "f (a \<inter> (\<Union>i. A i)) \<le> suminf (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A)"
+          using countably_subadditiveD [OF csa, of "(\<lambda>i. a \<inter> A i)"] summ
+        moreover
+        have "suminf (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A)  \<le> f a - f (a - (\<Union>i. A i))"
+          proof (rule suminf_le [OF summ])
+            fix n
+            have UNION_in: "(\<Union>i\<in>{0..<n}. A i) \<in> sets M"
+              by (metis A'' UNION_in_sets)
+            have le_fa: "f (UNION {0..<n} A \<inter> a) \<le> f a" using A''
+              by (blast intro: increasingD [OF inc] A'' Int UNION_in_sets a)
+            have ls: "(\<Union>i\<in>{0..<n}. A i) \<in> lambda_system M f"
+              using algebra.UNION_in_sets [OF lambda_system_algebra [OF pos]]
+            hence eq_fa: "f (a \<inter> (\<Union>i\<in>{0..<n}. A i)) + f (a - (\<Union>i\<in>{0..<n}. A i)) = f a"
+              by (simp add: lambda_system_eq UNION_in Diff_Compl a)
+            have "f (a - (\<Union>i. A i)) \<le> f (a - (\<Union>i\<in>{0..<n}. A i))"
+              by (blast intro: increasingD [OF inc] Diff UNION_eq_Union_image
UNION_in U_in a)
-	    thus "setsum (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A) {0..<n} \<le> f a - f (a - (\<Union>i. A i))"
-	      using eq_fa
-	      by (simp add: suminf_le [OF summ] lambda_system_strong_sum pos
+            thus "setsum (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A) {0..<n} \<le> f a - f (a - (\<Union>i. A i))"
+              using eq_fa
+              by (simp add: suminf_le [OF summ] lambda_system_strong_sum pos
a A disj)
-	  qed
-	ultimately show "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) \<le> f a"
-	  by arith
+          qed
+        ultimately show "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) \<le> f a"
+          by arith
next
-	have "f a \<le> f (a \<inter> (\<Union>i. A i) \<union> (a - (\<Union>i. A i)))"
-	  by (blast intro:  increasingD [OF inc] a U_in)
-	also have "... \<le>  f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))"
-	  by (blast intro: subadditiveD [OF sa] Int Diff U_in)
-	finally show "f a \<le> f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))" .
+        have "f a \<le> f (a \<inter> (\<Union>i. A i) \<union> (a - (\<Union>i. A i)))"
+          by (blast intro:  increasingD [OF inc] a U_in)
+        also have "... \<le>  f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))"
+          by (blast intro: subadditiveD [OF sa] Int Diff U_in)
+        finally show "f a \<le> f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))" .
qed
qed
}
@@ -654,20 +653,20 @@
have sums: "(\<lambda>i. f (A i \<inter> s)) sums f (\<Union>i. A i \<inter> s)"
show "range (\<lambda>n. A n \<inter> s) \<subseteq> sets M" using A s
-	by blast
+        by blast
show "disjoint_family (\<lambda>n. A n \<inter> s)" using disj
-	by (auto simp add: disjoint_family_def)
+        by (auto simp add: disjoint_family_def)
show "(\<Union>i. A i \<inter> s) \<in> sets M" using A s
-	by (metis UN_extend_simps(4) s seq)
+        by (metis UN_extend_simps(4) s seq)
qed
hence "f s = suminf (\<lambda>i. f (A i \<inter> s))"
by (metis Int_commute UN_simps(4) seq sums_iff)
also have "... \<le> suminf (f \<circ> A)"
proof (rule summable_le [OF _ _ sm])
show "\<forall>n. f (A n \<inter> s) \<le> (f \<circ> A) n" using A s
-	by (force intro: increasingD [OF inc])
+        by (force intro: increasingD [OF inc])
show "summable (\<lambda>i. f (A i \<inter> s))" using sums
qed
also have "... = z" by (rule si)
finally show "f s \<le> z" .
@@ -722,9 +721,9 @@
proof (auto)
fix n
have "\<bar>f (disjointed A n)\<bar> = f (disjointed A n)" using posf dA
-	by (auto simp add: positive_def image_subset_iff)
+        by (auto simp add: positive_def image_subset_iff)
also have "... \<le> f (A n)"
-	by (metis increasingD [OF inc] UNIV_I dA image_subset_iff disjointed_subset A)
+        by (metis increasingD [OF inc] UNIV_I dA image_subset_iff disjointed_subset A)
finally show "\<bar>f (disjointed A n)\<bar> \<le> f (A n)" .
qed
from Series.summable_le2 [OF this sm]
@@ -787,32 +786,32 @@
and ll: "!!n. ll n \<le> Inf (measure_set M f (A n)) + e * (1/2)^(Suc n)"
by auto blast
have llpos: "!!n. 0 \<le> ll n"
-	by (metis BBsums sums_iff o_apply posf positive_imp_pos suminf_ge_zero
+        by (metis BBsums sums_iff o_apply posf positive_imp_pos suminf_ge_zero
range_subsetD BB)
have sll: "summable ll &
suminf ll \<le> suminf (\<lambda>n. Inf (measure_set M f (A n))) + e"
proof -
-	have "(\<lambda>n. e * (1/2)^(Suc n)) sums (e*1)"
-	  by (rule sums_mult [OF power_half_series])
-	hence sum0: "summable (\<lambda>n. e * (1 / 2) ^ Suc n)"
-	  and eqe:  "(\<Sum>n. e * (1 / 2) ^ n / 2) = e"
-	  by (auto simp add: sums_iff)
-	have 0: "suminf (\<lambda>n. Inf (measure_set M f (A n))) +
+        have "(\<lambda>n. e * (1/2)^(Suc n)) sums (e*1)"
+          by (rule sums_mult [OF power_half_series])
+        hence sum0: "summable (\<lambda>n. e * (1 / 2) ^ Suc n)"
+          and eqe:  "(\<Sum>n. e * (1 / 2) ^ n / 2) = e"
+          by (auto simp add: sums_iff)
+        have 0: "suminf (\<lambda>n. Inf (measure_set M f (A n))) +
suminf (\<lambda>n. e * (1/2)^(Suc n)) =
suminf (\<lambda>n. Inf (measure_set M f (A n)) + e * (1/2)^(Suc n))"
-	  by (rule suminf_add [OF sum1 sum0])
-	have 1: "\<forall>n. \<bar>ll n\<bar> \<le> Inf (measure_set M f (A n)) + e * (1/2) ^ Suc n"
-	  by (metis ll llpos abs_of_nonneg)
-	have 2: "summable (\<lambda>n. Inf (measure_set M f (A n)) + e*(1/2)^(Suc n))"
-	  by (rule summable_add [OF sum1 sum0])
-	have "suminf ll \<le> (\<Sum>n. Inf (measure_set M f (A n)) + e*(1/2) ^ Suc n)"
-	  using Series.summable_le2 [OF 1 2] by auto
-	also have "... = (\<Sum>n. Inf (measure_set M f (A n))) +
+          by (rule suminf_add [OF sum1 sum0])
+        have 1: "\<forall>n. \<bar>ll n\<bar> \<le> Inf (measure_set M f (A n)) + e * (1/2) ^ Suc n"
+          by (metis ll llpos abs_of_nonneg)
+        have 2: "summable (\<lambda>n. Inf (measure_set M f (A n)) + e*(1/2)^(Suc n))"
+          by (rule summable_add [OF sum1 sum0])
+        have "suminf ll \<le> (\<Sum>n. Inf (measure_set M f (A n)) + e*(1/2) ^ Suc n)"
+          using Series.summable_le2 [OF 1 2] by auto
+        also have "... = (\<Sum>n. Inf (measure_set M f (A n))) +
(\<Sum>n. e * (1 / 2) ^ Suc n)"
-	  by (metis 0)
-	also have "... = (\<Sum>n. Inf (measure_set M f (A n))) + e"
-	finally show ?thesis using  Series.summable_le2 [OF 1 2] by auto
+          by (metis 0)
+        also have "... = (\<Sum>n. Inf (measure_set M f (A n))) + e"
+        finally show ?thesis using  Series.summable_le2 [OF 1 2] by auto
qed
def C \<equiv> "(split BB) o nat_to_nat2"
have C: "!!n. C n \<in> sets M"
@@ -822,24 +821,24 @@
done
have sbC: "(\<Union>i. A i) \<subseteq> (\<Union>i. C i)"
-	fix x i
-	assume x: "x \<in> A i"
-	with sbBB [of i] obtain j where "x \<in> BB i j"
-	  by blast
-	thus "\<exists>i. x \<in> split BB (nat_to_nat2 i)"
-	  by (metis nat_to_nat2_surj internal_split_def prod.cases
+        fix x i
+        assume x: "x \<in> A i"
+        with sbBB [of i] obtain j where "x \<in> BB i j"
+          by blast
+        thus "\<exists>i. x \<in> split BB (nat_to_nat2 i)"
+          by (metis nat_to_nat2_surj internal_split_def prod.cases
prod_case_split surj_f_inv_f)
qed
have "(f \<circ> C) = (f \<circ> (\<lambda>(x, y). BB x y)) \<circ> nat_to_nat2"
by (rule ext)  (auto simp add: C_def)
also have "... sums suminf ll"
proof (rule suminf_2dimen)
-	show "\<And>m n. 0 \<le> (f \<circ> (\<lambda>(x, y). BB x y)) (m, n)" using posf BB
-	  by (force simp add: positive_def)
-	show "\<And>m. (\<lambda>n. (f \<circ> (\<lambda>(x, y). BB x y)) (m, n)) sums ll m"using BBsums BB
-	  by (force simp add: o_def)
-	show "summable ll" using sll
-	  by auto
+        show "\<And>m n. 0 \<le> (f \<circ> (\<lambda>(x, y). BB x y)) (m, n)" using posf BB
+          by (force simp add: positive_def)
+        show "\<And>m. (\<lambda>n. (f \<circ> (\<lambda>(x, y). BB x y)) (m, n)) sums ll m"using BBsums BB
+          by (force simp add: o_def)
+        show "summable ll" using sll
+          by auto
qed
finally have Csums: "(f \<circ> C) sums suminf ll" .
have "Inf (measure_set M f (\<Union>i. A i)) \<le> suminf ll"
@@ -882,24 +881,24 @@
from inf_measure_close [OF posf e s]
obtain A l where A: "range A \<subseteq> sets M" and disj: "disjoint_family A"
and sUN: "s \<subseteq> (\<Union>i. A i)" and fsums: "(f \<circ> A) sums l"
-	           and l: "l \<le> Inf (measure_set M f s) + e"
-	by auto
+                   and l: "l \<le> Inf (measure_set M f s) + e"
+        by auto
have [simp]: "!!x. x \<in> sets M \<Longrightarrow>
(f o (\<lambda>z. z \<inter> (space M - x)) o A) = (f o (\<lambda>z. z - x) o A)"
-	by (rule ext, simp, metis A Int_Diff Int_space_eq2 range_subsetD)
+        by (rule ext, simp, metis A Int_Diff Int_space_eq2 range_subsetD)
have  [simp]: "!!n. f (A n \<inter> x) + f (A n - x) = f (A n)"
- 	   (auto simp add: x range_subsetD [OF A] Int_Diff_Un Int_Diff_disjoint)
+           (auto simp add: x range_subsetD [OF A] Int_Diff_Un Int_Diff_disjoint)
have fsumb: "summable (f \<circ> A)"
-	by (metis fsums sums_iff)
+        by (metis fsums sums_iff)
{ fix u
-	assume u: "u \<in> sets M"
-	have [simp]: "\<And>n. \<bar>f (A n \<inter> u)\<bar> \<le> f (A n)"
-	  by (simp add: positive_imp_pos [OF posf]  increasingD [OF inc]
+        assume u: "u \<in> sets M"
+        have [simp]: "\<And>n. \<bar>f (A n \<inter> u)\<bar> \<le> f (A n)"
+          by (simp add: positive_imp_pos [OF posf]  increasingD [OF inc]
u Int  range_subsetD [OF A])
-	have 1: "summable (f o (\<lambda>z. z\<inter>u) o A)"
+        have 1: "summable (f o (\<lambda>z. z\<inter>u) o A)"
by (rule summable_comparison_test [OF _ fsumb]) simp
-	have 2: "Inf (measure_set M f (s\<inter>u)) \<le> suminf (f o (\<lambda>z. z\<inter>u) o A)"
+        have 2: "Inf (measure_set M f (s\<inter>u)) \<le> suminf (f o (\<lambda>z. z\<inter>u) o A)"
proof (rule Inf_lower)
show "suminf (f \<circ> (\<lambda>z. z \<inter> u) \<circ> A) \<in> measure_set M f (s \<inter> u)"
@@ -920,14 +919,14 @@
and sum2: "summable (f o (\<lambda>z. z \<inter> (space M - x)) o A)"
and inf2: "Inf (measure_set M f (s \<inter> (space M - x)))
\<le> suminf (f o (\<lambda>z. z \<inter> (space M - x)) o A)"
-	by (metis Diff lesum top x)+
+        by (metis Diff lesum top x)+
hence "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
\<le> suminf (f o (\<lambda>s. s\<inter>x) o A) + suminf (f o (\<lambda>s. s-x) o A)"
also have "... \<le> suminf (f o A)" using suminf_add [OF sum1 sum2]
also have "... \<le> Inf (measure_set M f s) + e"
-	by (metis fsums l sums_unique)
+        by (metis fsums l sums_unique)
finally show "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
\<le> Inf (measure_set M f s) + e" .
qed
@@ -940,7 +939,7 @@
also have "... \<le> Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))"
apply (auto simp add: subsetD [OF s])
done
finally show ?thesis .```
```--- a/src/HOL/Probability/Measure.thy	Mon Nov 09 21:33:22 2009 +0100
+++ b/src/HOL/Probability/Measure.thy	Mon Nov 09 21:45:24 2009 +0100
@@ -46,8 +46,8 @@
definition
measurable  where
"measurable a b = {f . sigma_algebra a & sigma_algebra b &
-			 f \<in> (space a -> space b) &
-			 (\<forall>y \<in> sets b. (f -` y) \<inter> (space a) \<in> sets a)}"
+                         f \<in> (space a -> space b) &
+                         (\<forall>y \<in> sets b. (f -` y) \<inter> (space a) \<in> sets a)}"

definition
measure_preserving  where
@@ -258,23 +258,23 @@
fix x
assume x: "x \<in> smallest_ccdi_sets M"
thus "x \<in> C"
-	proof (induct rule: smallest_ccdi_sets.induct)
-	  case (Basic x)
-	  thus ?case
-	    by (metis Basic subsetD sbC)
-	next
-	  case (Compl x)
-	  thus ?case
-	    by (blast intro: closed_cdi_Compl [OF ccdi, simplified])
- 	next
-	  case (Inc A)
-	  thus ?case
-	       by (auto intro: closed_cdi_Inc [OF ccdi, simplified])
-	next
-	  case (Disj A)
-	  thus ?case
-	       by (auto intro: closed_cdi_Disj [OF ccdi, simplified])
-	qed
+        proof (induct rule: smallest_ccdi_sets.induct)
+          case (Basic x)
+          thus ?case
+            by (metis Basic subsetD sbC)
+        next
+          case (Compl x)
+          thus ?case
+            by (blast intro: closed_cdi_Compl [OF ccdi, simplified])
+        next
+          case (Inc A)
+          thus ?case
+               by (auto intro: closed_cdi_Inc [OF ccdi, simplified])
+        next
+          case (Disj A)
+          thus ?case
+               by (auto intro: closed_cdi_Disj [OF ccdi, simplified])
+        qed
qed
finally show ?thesis .
qed
@@ -292,12 +292,12 @@
have "sigma_sets (space M) (sets M) \<subseteq> C \<inter> sigma_sets (space M) (sets M)"
proof (rule sigma_property_disjoint_lemma)
show "sets M \<subseteq> C \<inter> sigma_sets (space M) (sets M)"
-	by (metis Int_greatest Set.subsetI sbC sigma_sets.Basic)
+        by (metis Int_greatest Set.subsetI sbC sigma_sets.Basic)
next
show "closed_cdi \<lparr>space = space M, sets = C \<inter> sigma_sets (space M) (sets M)\<rparr>"
-	by (simp add: closed_cdi_def compl inc disj)
+        by (simp add: closed_cdi_def compl inc disj)
(metis PowI Set.subsetI le_infI2 sigma_sets_into_sp space_closed
-	     IntE sigma_sets.Compl range_subsetD sigma_sets.Union)
+             IntE sigma_sets.Compl range_subsetD sigma_sets.Union)
qed
thus ?thesis
by blast
@@ -349,7 +349,7 @@
case 0 show ?case by simp
next
case (Suc m) thus ?case
qed
}
hence "!!m n. m < n \<Longrightarrow> A m \<subseteq> A n"
@@ -371,17 +371,17 @@
have "(measure M \<circ> A) n =
setsum (measure M \<circ> (\<lambda>i. A (Suc i) - A i)) {0..<n}"
proof (induct n)
-	case 0 thus ?case by (auto simp add: A0 empty_measure)
+        case 0 thus ?case by (auto simp add: A0 empty_measure)
next
-	case (Suc m)
-	have "A (Suc m) = A m \<union> (A (Suc m) - A m)"
-	  by (metis ASuc Un_Diff_cancel Un_absorb1)
-	hence "measure M (A (Suc m)) =
+        case (Suc m)
+        have "A (Suc m) = A m \<union> (A (Suc m) - A m)"
+          by (metis ASuc Un_Diff_cancel Un_absorb1)
+        hence "measure M (A (Suc m)) =
measure M (A m) + measure M (A (Suc m) - A m)"
-	with Suc show ?case
-	  by simp
+        with Suc show ?case
+          by simp
qed
}
hence Meq: "measure M o A = (\<lambda>n. setsum (measure M o (\<lambda>i. A(Suc i) - A i)) {0..<n})"
@@ -390,13 +390,13 @@
proof (rule UN_finite2_eq [where k=1], simp)
fix i
show "(\<Union>i\<in>{0..<i}. A (Suc i) - A i) = (\<Union>i\<in>{0..<Suc i}. A i)"
-	proof (induct i)
-	  case 0 thus ?case by (simp add: A0)
-	next
-	  case (Suc i)
-	  thus ?case
-	    by (auto simp add: atLeastLessThanSuc intro: subsetD [OF ASuc])
-	qed
+        proof (induct i)
+          case 0 thus ?case by (simp add: A0)
+        next
+          case (Suc i)
+          thus ?case
+            by (auto simp add: atLeastLessThanSuc intro: subsetD [OF ASuc])
+        qed
qed
have A1: "\<And>i. A (Suc i) - A i \<in> sets M"
by (metis A Diff range_subsetD)
@@ -461,23 +461,23 @@
assume A: "range A \<subseteq> (vimage f) ` (sets b)"
have  "(\<Union>i. A i) \<in> (vimage f) ` (sets b)"
proof -
-	def B \<equiv> "\<lambda>i. @v. v \<in> sets b \<and> f -` v = A i"
-	{
-	  fix i
-	  have "A i \<in> (vimage f) ` (sets b)" using A
-	    by blast
-	  hence "\<exists>v. v \<in> sets b \<and> f -` v = A i"
-	    by blast
-	  hence "B i \<in> sets b \<and> f -` B i = A i"
-	    by (simp add: B_def) (erule someI_ex)
-	} note B = this
-	show ?thesis
-	  proof
-	    show "(\<Union>i. A i) = f -` (\<Union>i. B i)"
-	      by (simp add: vimage_UN B)
-	   show "(\<Union>i. B i) \<in> sets b" using B
-	     by (auto intro: sigma_algebra.countable_UN [OF b])
-	  qed
+        def B \<equiv> "\<lambda>i. @v. v \<in> sets b \<and> f -` v = A i"
+        {
+          fix i
+          have "A i \<in> (vimage f) ` (sets b)" using A
+            by blast
+          hence "\<exists>v. v \<in> sets b \<and> f -` v = A i"
+            by blast
+          hence "B i \<in> sets b \<and> f -` B i = A i"
+            by (simp add: B_def) (erule someI_ex)
+        } note B = this
+        show ?thesis
+          proof
+            show "(\<Union>i. A i) = f -` (\<Union>i. B i)"
+              by (simp add: vimage_UN B)
+           show "(\<Union>i. B i) \<in> sets b" using B
+             by (auto intro: sigma_algebra.countable_UN [OF b])
+          qed
qed
}
thus "\<forall>A::nat \<Rightarrow> 'a set.
@@ -496,26 +496,26 @@
fix x
assume "x \<in> sigma_sets X B"
thus "f -` x \<inter> space M \<in> sets M \<and> x \<subseteq> X"
-	proof induct
-	  case (Basic a)
-	  thus ?case
-	    by (auto simp add: ba) (metis B subsetD PowD)
+        proof induct
+          case (Basic a)
+          thus ?case
+            by (auto simp add: ba) (metis B subsetD PowD)
next
-	  case Empty
-	  thus ?case
-	    by auto
+          case Empty
+          thus ?case
+            by auto
next
-	  case (Compl a)
-	  have [simp]: "f -` X \<inter> space M = space M"
-	    by (auto simp add: funcset_mem [OF f])
-	  thus ?case
-	    by (auto simp add: vimage_Diff Diff_Int_distrib2 compl_sets Compl)
-	next
-	  case (Union a)
-	  thus ?case
-	    by (simp add: vimage_UN, simp only: UN_extend_simps(4))
-	       (blast intro: countable_UN)
-	qed
+          case (Compl a)
+          have [simp]: "f -` X \<inter> space M = space M"
+            by (auto simp add: funcset_mem [OF f])
+          thus ?case
+            by (auto simp add: vimage_Diff Diff_Int_distrib2 compl_sets Compl)
+        next
+          case (Union a)
+          thus ?case
+            by (simp add: vimage_UN, simp only: UN_extend_simps(4))
+               (blast intro: countable_UN)
+        qed
qed
thus ?thesis
by (simp add: measurable_def sigma_algebra_axioms sigma_algebra_sigma B f)
@@ -553,122 +553,122 @@
show ?thesis using fmp
proof (clarsimp simp add: measure_preserving_def m1 m2)
assume fm: "f \<in> measurable m1 (m a)"
-	 and mam: "measure_space (m a)"
-	 and meq: "\<forall>y\<in>a. measure m1 (f -` y \<inter> space m1) = measure m2 y"
+         and mam: "measure_space (m a)"
+         and meq: "\<forall>y\<in>a. measure m1 (f -` y \<inter> space m1) = measure m2 y"
have "f \<in> measurable m1 (sigma (space (m a)) (sets (m a)))"
-	by (rule subsetD [OF measurable_subset fm])
+        by (rule subsetD [OF measurable_subset fm])
also have "... = measurable m1 m2"
-	by (rule measurable_eqI) (simp_all add: m_def setsm2 sigma_def)
+        by (rule measurable_eqI) (simp_all add: m_def setsm2 sigma_def)
finally have f12: "f \<in> measurable m1 m2" .
hence ffn: "f \<in> space m1 \<rightarrow> space m2"
have "space m1 \<subseteq> f -` (space m2)"
-	by auto (metis PiE ffn)
+        by auto (metis PiE ffn)
hence fveq [simp]: "(f -` (space m2)) \<inter> space m1 = space m1"
-	by blast
+        by blast
{
-	fix y
-	assume y: "y \<in> sets m2"
-	have ama: "algebra (m a)"  using mam
-	  by (simp add: measure_space_def sigma_algebra_iff)
-	have spa: "space m2 \<in> a" using algebra.top [OF ama]
-	have "sigma_sets (space m2) a = sigma_sets (space (m a)) (sets (m a))"
-	also have "... \<subseteq> {s . measure m1 ((f -` s) \<inter> space m1) = measure m2 s}"
-	  proof (rule algebra.sigma_property_disjoint, auto simp add: ama)
-	    fix x
-	    assume x: "x \<in> a"
-	    thus "measure m1 (f -` x \<inter> space m1) = measure m2 x"
-	  next
-	    fix s
-	    assume eq: "measure m1 (f -` s \<inter> space m1) = measure m2 s"
-	       and s: "s \<in> sigma_sets (space m2) a"
-	    hence s2: "s \<in> sets m2"
-	    thus "measure m1 (f -` (space m2 - s) \<inter> space m1) =
+        fix y
+        assume y: "y \<in> sets m2"
+        have ama: "algebra (m a)"  using mam
+          by (simp add: measure_space_def sigma_algebra_iff)
+        have spa: "space m2 \<in> a" using algebra.top [OF ama]
+        have "sigma_sets (space m2) a = sigma_sets (space (m a)) (sets (m a))"
+        also have "... \<subseteq> {s . measure m1 ((f -` s) \<inter> space m1) = measure m2 s}"
+          proof (rule algebra.sigma_property_disjoint, auto simp add: ama)
+            fix x
+            assume x: "x \<in> a"
+            thus "measure m1 (f -` x \<inter> space m1) = measure m2 x"
+          next
+            fix s
+            assume eq: "measure m1 (f -` s \<inter> space m1) = measure m2 s"
+               and s: "s \<in> sigma_sets (space m2) a"
+            hence s2: "s \<in> sets m2"
+            thus "measure m1 (f -` (space m2 - s) \<inter> space m1) =
measure m2 (space m2 - s)" using f12
-	      by (simp add: vimage_Diff Diff_Int_distrib2 eq m1 m2
-		    measure_space.measure_compl measurable_def)
-	         (metis fveq meq spa)
-	  next
-	    fix A
-	      assume A0: "A 0 = {}"
-	 	 and ASuc: "!!n.  A n \<subseteq> A (Suc n)"
-		 and rA1: "range A \<subseteq>
-		           {s. measure m1 (f -` s \<inter> space m1) = measure m2 s}"
-		 and "range A \<subseteq> sigma_sets (space m2) a"
-	      hence rA2: "range A \<subseteq> sets m2" by (metis setsm2)
-	      have eq1: "!!i. measure m1 (f -` A i \<inter> space m1) = measure m2 (A i)"
-		using rA1 by blast
-	      have "(measure m2 \<circ> A) = measure m1 o (\<lambda>i. (f -` A i \<inter> space m1))"
-		by (simp add: o_def eq1)
-	      also have "... ----> measure m1 (\<Union>i. f -` A i \<inter> space m1)"
-		proof (rule measure_space.measure_countable_increasing [OF m1])
-		  show "range (\<lambda>i. f -` A i \<inter> space m1) \<subseteq> sets m1"
-		    using f12 rA2 by (auto simp add: measurable_def)
-		  show "f -` A 0 \<inter> space m1 = {}" using A0
-		    by blast
-		  show "\<And>n. f -` A n \<inter> space m1 \<subseteq> f -` A (Suc n) \<inter> space m1"
-		    using ASuc by auto
-		qed
-	      also have "... = measure m1 (f -` (\<Union>i. A i) \<inter> space m1)"
-	      finally have "(measure m2 \<circ> A) ----> measure m1 (f -` (\<Union>i. A i) \<inter> space m1)" .
-	      moreover
-	      have "(measure m2 \<circ> A) ----> measure m2 (\<Union>i. A i)"
-		by (rule measure_space.measure_countable_increasing
-		          [OF m2 rA2, OF A0 ASuc])
-	      ultimately
-	      show "measure m1 (f -` (\<Union>i. A i) \<inter> space m1) =
+              by (simp add: vimage_Diff Diff_Int_distrib2 eq m1 m2
+                    measure_space.measure_compl measurable_def)
+                 (metis fveq meq spa)
+          next
+            fix A
+              assume A0: "A 0 = {}"
+                 and ASuc: "!!n.  A n \<subseteq> A (Suc n)"
+                 and rA1: "range A \<subseteq>
+                           {s. measure m1 (f -` s \<inter> space m1) = measure m2 s}"
+                 and "range A \<subseteq> sigma_sets (space m2) a"
+              hence rA2: "range A \<subseteq> sets m2" by (metis setsm2)
+              have eq1: "!!i. measure m1 (f -` A i \<inter> space m1) = measure m2 (A i)"
+                using rA1 by blast
+              have "(measure m2 \<circ> A) = measure m1 o (\<lambda>i. (f -` A i \<inter> space m1))"
+                by (simp add: o_def eq1)
+              also have "... ----> measure m1 (\<Union>i. f -` A i \<inter> space m1)"
+                proof (rule measure_space.measure_countable_increasing [OF m1])
+                  show "range (\<lambda>i. f -` A i \<inter> space m1) \<subseteq> sets m1"
+                    using f12 rA2 by (auto simp add: measurable_def)
+                  show "f -` A 0 \<inter> space m1 = {}" using A0
+                    by blast
+                  show "\<And>n. f -` A n \<inter> space m1 \<subseteq> f -` A (Suc n) \<inter> space m1"
+                    using ASuc by auto
+                qed
+              also have "... = measure m1 (f -` (\<Union>i. A i) \<inter> space m1)"
+              finally have "(measure m2 \<circ> A) ----> measure m1 (f -` (\<Union>i. A i) \<inter> space m1)" .
+              moreover
+              have "(measure m2 \<circ> A) ----> measure m2 (\<Union>i. A i)"
+                by (rule measure_space.measure_countable_increasing
+                          [OF m2 rA2, OF A0 ASuc])
+              ultimately
+              show "measure m1 (f -` (\<Union>i. A i) \<inter> space m1) =
measure m2 (\<Union>i. A i)"
-		by (rule LIMSEQ_unique)
-	  next
-	    fix A :: "nat => 'a2 set"
-	      assume dA: "disjoint_family A"
-		 and rA1: "range A \<subseteq>
-		           {s. measure m1 (f -` s \<inter> space m1) = measure m2 s}"
-		 and "range A \<subseteq> sigma_sets (space m2) a"
-	      hence rA2: "range A \<subseteq> sets m2" by (metis setsm2)
-	      hence Um2: "(\<Union>i. A i) \<in> sets m2"
-		by (metis range_subsetD setsm2 sigma_sets.Union)
-	      have "!!i. measure m1 (f -` A i \<inter> space m1) = measure m2 (A i)"
-		using rA1 by blast
-	      hence "measure m2 o A = measure m1 o (\<lambda>i. f -` A i \<inter> space m1)"
-	      also have "... sums measure m1 (\<Union>i. f -` A i \<inter> space m1)"
-		proof (rule measure_space.measure_countably_additive [OF m1] )
-		  show "range (\<lambda>i. f -` A i \<inter> space m1) \<subseteq> sets m1"
-		    using f12 rA2 by (auto simp add: measurable_def)
-		  show "disjoint_family (\<lambda>i. f -` A i \<inter> space m1)" using dA
-		    by (auto simp add: disjoint_family_def)
-		  show "(\<Union>i. f -` A i \<inter> space m1) \<in> sets m1"
-		    proof (rule sigma_algebra.countable_UN [OF sa1])
-		      show "range (\<lambda>i. f -` A i \<inter> space m1) \<subseteq> sets m1" using f12 rA2
-			by (auto simp add: measurable_def)
-		    qed
- 		qed
-	      finally have "(measure m2 o A) sums measure m1 (\<Union>i. f -` A i \<inter> space m1)" .
-	      with measure_space.measure_countably_additive [OF m2 rA2 dA Um2]
-	      have "measure m1 (\<Union>i. f -` A i \<inter> space m1) = measure m2 (\<Union>i. A i)"
-		by (metis sums_unique)
+                by (rule LIMSEQ_unique)
+          next
+            fix A :: "nat => 'a2 set"
+              assume dA: "disjoint_family A"
+                 and rA1: "range A \<subseteq>
+                           {s. measure m1 (f -` s \<inter> space m1) = measure m2 s}"
+                 and "range A \<subseteq> sigma_sets (space m2) a"
+              hence rA2: "range A \<subseteq> sets m2" by (metis setsm2)
+              hence Um2: "(\<Union>i. A i) \<in> sets m2"
+                by (metis range_subsetD setsm2 sigma_sets.Union)
+              have "!!i. measure m1 (f -` A i \<inter> space m1) = measure m2 (A i)"
+                using rA1 by blast
+              hence "measure m2 o A = measure m1 o (\<lambda>i. f -` A i \<inter> space m1)"
+              also have "... sums measure m1 (\<Union>i. f -` A i \<inter> space m1)"
+                proof (rule measure_space.measure_countably_additive [OF m1] )
+                  show "range (\<lambda>i. f -` A i \<inter> space m1) \<subseteq> sets m1"
+                    using f12 rA2 by (auto simp add: measurable_def)
+                  show "disjoint_family (\<lambda>i. f -` A i \<inter> space m1)" using dA
+                    by (auto simp add: disjoint_family_def)
+                  show "(\<Union>i. f -` A i \<inter> space m1) \<in> sets m1"
+                    proof (rule sigma_algebra.countable_UN [OF sa1])
+                      show "range (\<lambda>i. f -` A i \<inter> space m1) \<subseteq> sets m1" using f12 rA2
+                        by (auto simp add: measurable_def)
+                    qed
+                qed
+              finally have "(measure m2 o A) sums measure m1 (\<Union>i. f -` A i \<inter> space m1)" .
+              with measure_space.measure_countably_additive [OF m2 rA2 dA Um2]
+              have "measure m1 (\<Union>i. f -` A i \<inter> space m1) = measure m2 (\<Union>i. A i)"
+                by (metis sums_unique)

-	      moreover have "measure m1 (f -` (\<Union>i. A i) \<inter> space m1) = measure m1 (\<Union>i. f -` A i \<inter> space m1)"
-	      ultimately show "measure m1 (f -` (\<Union>i. A i) \<inter> space m1) =
+              moreover have "measure m1 (f -` (\<Union>i. A i) \<inter> space m1) = measure m1 (\<Union>i. f -` A i \<inter> space m1)"
+              ultimately show "measure m1 (f -` (\<Union>i. A i) \<inter> space m1) =
measure m2 (\<Union>i. A i)"
-		by metis
-	  qed
-	finally have "sigma_sets (space m2) a
+                by metis
+          qed
+        finally have "sigma_sets (space m2) a
\<subseteq> {s . measure m1 ((f -` s) \<inter> space m1) = measure m2 s}" .
-	hence "measure m1 (f -` y \<inter> space m1) = measure m2 y" using y
-	  by (force simp add: setsm2)
+        hence "measure m1 (f -` y \<inter> space m1) = measure m2 y" using y
+          by (force simp add: setsm2)
}
thus "f \<in> measurable m1 m2 \<and>
(\<forall>y\<in>sets m2.
measure m1 (f -` y \<inter> space m1) = measure m2 y)"
-	by (blast intro: f12)
+        by (blast intro: f12)
qed
qed
```
```--- a/src/HOL/Probability/Probability.thy	Mon Nov 09 21:33:22 2009 +0100
+++ b/src/HOL/Probability/Probability.thy	Mon Nov 09 21:45:24 2009 +0100
@@ -1,5 +1,5 @@
-theory Probability imports
-	Measure
+theory Probability
+imports Measure
begin

end```
```--- a/src/HOL/Probability/ROOT.ML	Mon Nov 09 21:33:22 2009 +0100
+++ b/src/HOL/Probability/ROOT.ML	Mon Nov 09 21:45:24 2009 +0100
@@ -1,6 +1,1 @@
-(*
-  no_document use_thy "ThisTheory";
-  use_thy "ThatTheory";
-*)
-
use_thy "Probability";```
```--- a/src/HOL/Probability/SeriesPlus.thy	Mon Nov 09 21:33:22 2009 +0100
+++ b/src/HOL/Probability/SeriesPlus.thy	Mon Nov 09 21:45:24 2009 +0100
@@ -1,6 +1,5 @@
theory SeriesPlus
imports Complex_Main Nat_Int_Bij
-
begin

text{*From the Hurd/Coble measure theory development, translated by Lawrence Paulson.*}
@@ -28,9 +27,9 @@
proof -
fix m
have "0 \<le> suminf (\<lambda>n. f (m,n))"
-	by (rule suminf_0_le, simp add: f_nneg, metis fsums sums_iff)
+        by (rule suminf_0_le, simp add: f_nneg, metis fsums sums_iff)
thus "0 \<le> g m" using fsums [of m]
-	by (auto simp add: sums_iff)
+        by (auto simp add: sums_iff)
qed
show "(\<lambda>n. \<Sum>x = 0..<n. f (nat_to_nat2 x)) ----> suminf g"
proof (rule increasing_LIMSEQ, simp add: f_nneg)
@@ -48,14 +47,14 @@
by (rule setsum_mono2) (auto simp add: ij)
also have "... = setsum (\<lambda>m. setsum (\<lambda>n. f (m,n)) {0..j}) {0..<Suc i}"
by (metis atLeast0AtMost atLeast0LessThan lessThan_Suc_atMost
-	        setsum_cartesian_product split_eta)
+                setsum_cartesian_product split_eta)
also have "... \<le> setsum g {0..<Suc i}"
proof (rule setsum_mono, simp add: less_Suc_eq_le)
-	fix m
-	assume m: "m \<le> i"
-	thus " (\<Sum>n = 0..j. f (m, n)) \<le> g m" using fsums [of m]
-	  by (auto simp add: sums_iff)
-	   (metis atLeastLessThanSuc_atLeastAtMost f_nneg series_pos_le f_nneg)
+        fix m
+        assume m: "m \<le> i"
+        thus " (\<Sum>n = 0..j. f (m, n)) \<le> g m" using fsums [of m]
+          by (auto simp add: sums_iff)
+           (metis atLeastLessThanSuc_atLeastAtMost f_nneg series_pos_le f_nneg)
qed
finally have  "(\<Sum>x = 0..<n. f (nat_to_nat2 x)) \<le> setsum g {0..<Suc i}" .
also have "... \<le> suminf g"
@@ -73,13 +72,13 @@
{ fix m
assume m: "m<N"
hence enneg: "0 < e / (2 * real N)" using e
hence  "\<exists>j. \<bar>(\<Sum>n = 0..<j. f (m, n)) - g m\<bar> < e/(2 * real N)"
-	using fsums [of m] m
+        using fsums [of m] m
by (force simp add: sums_def LIMSEQ_def dist_real_def)
hence "\<exists>j. g m < setsum (\<lambda>n. f (m,n)) {0..<j} + e/(2 * real N)"
-	using fsums [of m]
-	by (auto simp add: sums_iff)
+        using fsums [of m]
+        by (auto simp add: sums_iff)
}
hence "\<exists>jj. \<forall>m. m<N \<longrightarrow> g m < (\<Sum>n = 0..<jj m. f (m, n)) + e/(2 * real N)"
@@ -103,13 +102,13 @@
def NIJ \<equiv> "Max (nat_to_nat2 -` IJ)"
have IJsb: "IJ \<subseteq> nat_to_nat2 ` {0..NIJ}"
-	fix i j
-	assume ij:"(i,j) \<in> IJ"
-	hence "(i,j) = nat_to_nat2 (inv nat_to_nat2 (i,j))"
-	  by (metis nat_to_nat2_surj surj_f_inv_f)
-	thus "(i,j) \<in> nat_to_nat2 ` {0..Max (nat_to_nat2 -` IJ)}"
-	  by (rule image_eqI)
-	     (simp add: ij finite_vimageI [OF finite_IJ nat_to_nat2_inj]
+        fix i j
+        assume ij:"(i,j) \<in> IJ"
+        hence "(i,j) = nat_to_nat2 (inv nat_to_nat2 (i,j))"
+          by (metis nat_to_nat2_surj surj_f_inv_f)
+        thus "(i,j) \<in> nat_to_nat2 ` {0..Max (nat_to_nat2 -` IJ)}"
+          by (rule image_eqI)
+             (simp add: ij finite_vimageI [OF finite_IJ nat_to_nat2_inj]
nat_to_nat2_surj surj_f_inv_f)
qed
have "setsum f IJ \<le> setsum f (nat_to_nat2 `{0..NIJ})"```
```--- a/src/HOL/Probability/Sigma_Algebra.thy	Mon Nov 09 21:33:22 2009 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Mon Nov 09 21:45:24 2009 +0100
@@ -235,4 +235,3 @@

end
-```
```--- a/src/HOL/Series.thy	Mon Nov 09 21:33:22 2009 +0100
+++ b/src/HOL/Series.thy	Mon Nov 09 21:45:24 2009 +0100
@@ -293,11 +293,11 @@
have "convergent (\<lambda>n. setsum f {0..<n})"
proof (rule Bseq_mono_convergent)
show "Bseq (\<lambda>n. setsum f {0..<n})"
-	by (rule f_inc_g_dec_Beq_f [of "(\<lambda>n. setsum f {0..<n})" "\<lambda>n. x"])
+        by (rule f_inc_g_dec_Beq_f [of "(\<lambda>n. setsum f {0..<n})" "\<lambda>n. x"])
next
show "\<forall>m n. m \<le> n \<longrightarrow> setsum f {0..<m} \<le> setsum f {0..<n}"
-	by (auto intro: setsum_mono2 pos)
+        by (auto intro: setsum_mono2 pos)
qed
then obtain L where "(%n. setsum f {0..<n}) ----> L"
by (blast dest: convergentD)```
```--- a/src/Pure/Isar/proof_context.ML	Mon Nov 09 21:33:22 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML	Mon Nov 09 21:45:24 2009 +0100
@@ -1032,7 +1032,10 @@
(Local_Syntax.update_modesyntax (theory_of ctxt) add mode (map_filter (const_syntax ctxt) args));

fun target_notation add mode args phi =
-  let val args' = filter (fn (t, _) => Type.similar_types (t, Morphism.term phi t)) args;
+  let
+    val args' = args |> map_filter (fn (t, mx) =>
+      let val t' = Morphism.term phi t
+      in if Term.aconv_untyped (t, t') then SOME (t', mx) else NONE end);

end;```
```--- a/src/Pure/Isar/theory_target.ML	Mon Nov 09 21:33:22 2009 +0100
+++ b/src/Pure/Isar/theory_target.ML	Mon Nov 09 21:45:24 2009 +0100
@@ -190,9 +190,7 @@
val b' = Morphism.binding phi b;
val rhs' = Morphism.term phi rhs;
val arg = (b', Term.close_schematic_term rhs');
-(*    val similar_body = Type.similar_types (rhs, rhs'); *)
-    val same_shape = op aconv o pairself (Term.map_types (fn _ => Term.dummyT));
-    val similar_body = same_shape (rhs, rhs');
+    val same_shape = Term.aconv_untyped (rhs, rhs');
(* FIXME workaround based on educated guess *)
val prefix' = Binding.prefix_of b';
val class_global =
@@ -200,12 +198,12 @@
not (null prefix') andalso
fst (snd (split_last prefix')) = Class_Target.class_prefix target;
in
-    not (is_class andalso (similar_body orelse class_global)) ?
+    not (is_class andalso (same_shape orelse class_global)) ?
(Context.mapping_result
#-> (fn (lhs' as Const (d, _), _) =>
-          similar_body ?
+          same_shape ?
(Context.mapping (Sign.revert_abbrev mode d) (ProofContext.revert_abbrev mode d) #>
Morphism.form (ProofContext.target_notation true prmode [(lhs', mx)]))))
end;```
```--- a/src/Pure/term.ML	Mon Nov 09 21:33:22 2009 +0100
+++ b/src/Pure/term.ML	Mon Nov 09 21:45:24 2009 +0100
@@ -146,6 +146,7 @@
val eq_ix: indexname * indexname -> bool
val eq_tvar: (indexname * sort) * (indexname * sort) -> bool
val eq_var: (indexname * typ) * (indexname * typ) -> bool
+  val aconv_untyped: term * term -> bool
val could_unify: term * term -> bool
val strip_abs_eta: int -> term -> (string * typ) list * term
val match_bvars: (term * term) * (string * string) list -> (string * string) list
@@ -524,6 +525,17 @@
| (Abs (_, T1, t1), Abs (_, T2, t2)) => t1 aconv t2 andalso T1 = T2
| (a1, a2) => a1 = a2);

+fun aconv_untyped (tm1, tm2) =
+  pointer_eq (tm1, tm2) orelse
+    (case (tm1, tm2) of
+      (t1 \$ u1, t2 \$ u2) => aconv_untyped (t1, t2) andalso aconv_untyped (u1, u2)
+    | (Abs (_, _, t1), Abs (_, _, t2)) => aconv_untyped (t1, t2)
+    | (Const (a, _), Const (b, _)) => a = b
+    | (Free (x, _), Free (y, _)) => x = y
+    | (Var (xi, _), Var (yj, _)) => xi = yj
+    | (Bound i, Bound j) => i = j
+    | _ => false);
+

(*A fast unification filter: true unless the two terms cannot be unified.
Terms must be NORMAL.  Treats all Vars as distinct. *)```
```--- a/src/Pure/type.ML	Mon Nov 09 21:33:22 2009 +0100
+++ b/src/Pure/type.ML	Mon Nov 09 21:45:24 2009 +0100
@@ -42,7 +42,6 @@

(*special treatment of type vars*)
val strip_sorts: typ -> typ
-  val similar_types: term * term -> bool
val no_tvars: typ -> typ
val varify: (string * sort) list -> term -> ((string * sort) * indexname) list * term
val freeze_thaw_type: typ -> typ * (typ -> typ)
@@ -236,23 +235,6 @@
| strip_sorts (TVar (xi, _)) = TVar (xi, []);

-(* equivalence up to renaming of atomic types *)
-
-local
-
-fun standard_types t =
-  let
-    val Ts = fold_types (fold_atyps (insert (op =))) t [];
-    val Ts' = map (fn a => TFree (a, [])) (Name.invents Name.context Name.aT (length Ts));
-  in map_types (map_atyps (perhaps (AList.lookup (op =) (Ts ~~ Ts')))) t end;
-
-in
-
-val similar_types = op aconv o pairself (Term.map_types strip_sorts o standard_types);
-
-end;
-
-
(* no_tvars *)

fun no_tvars T =```