--- a/src/HOL/Probability/Borel.thy Thu May 20 23:22:37 2010 +0200
+++ b/src/HOL/Probability/Borel.thy Thu May 20 21:19:38 2010 -0700
@@ -397,8 +397,7 @@
{ fix w
from `0 < a` have "a \<le> inverse (f w) \<longleftrightarrow> 0 < f w \<and> f w \<le> 1 / a"
by (metis inverse_eq_divide inverse_inverse_eq le_imp_inverse_le
- linorder_not_le order_refl order_trans less_le
- xt1(7) zero_less_divide_1_iff) }
+ less_le_trans zero_less_divide_1_iff) }
hence "{w \<in> space M. a \<le> inverse (f w)} =
{w \<in> space M. 0 < f w} \<inter> {w \<in> space M. f w \<le> 1 / a}" by auto
with Int assms[unfolded borel_measurable_gr_iff]
--- a/src/HOL/Probability/Caratheodory.thy Thu May 20 23:22:37 2010 +0200
+++ b/src/HOL/Probability/Caratheodory.thy Thu May 20 21:19:38 2010 -0700
@@ -167,9 +167,9 @@
{l. l \<in> sets M & (\<forall>x \<in> sets M. f (x \<inter> l) + f (x - l) = f x)}"
proof -
have [simp]: "!!l x. l \<in> sets M \<Longrightarrow> x \<in> sets M \<Longrightarrow> (space M - l) \<inter> x = x - l"
- by (metis Diff_eq Int_Diff Int_absorb1 Int_commute sets_into_space)
+ by (metis Int_Diff Int_absorb1 Int_commute sets_into_space)
show ?thesis
- by (auto simp add: lambda_system_def) (metis Diff_Compl Int_commute)+
+ by (auto simp add: lambda_system_def) (metis Int_commute)+
qed
lemma (in algebra) lambda_system_empty:
@@ -352,7 +352,7 @@
proof (auto simp add: disjointed_def)
fix n
show "A n - (\<Union>i\<in>{0..<n}. A i) \<in> sets M" using UNION_in_sets
- by (metis A Diff UNIV_I disjointed_def image_subset_iff)
+ by (metis A Diff UNIV_I image_subset_iff)
qed
lemma sigma_algebra_disjoint_iff:
@@ -476,7 +476,7 @@
lambda_system_positive lambda_system_additive lambda_system_increasing
A' oms outer_measure_space_def disj)
have U_in: "(\<Union>i. A i) \<in> sets M"
- by (metis A countable_UN image_subset_iff lambda_system_sets)
+ by (metis A'' countable_UN)
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)"
@@ -500,7 +500,7 @@
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)
+ apply (blast intro: increasingD [OF inc])
done
show ?thesis
proof (rule antisym)
@@ -523,15 +523,15 @@
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)
+ by (blast intro: increasingD [OF inc] A'' UNION_in_sets)
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]]
by (simp add: A)
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)
+ by (simp add: lambda_system_eq UNION_in)
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)
+ by (blast intro: increasingD [OF inc] UNION_eq_Union_image
+ UNION_in U_in)
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
@@ -541,9 +541,9 @@
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)
+ by (blast intro: increasingD [OF inc] 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)
+ by (blast intro: subadditiveD [OF sa] U_in)
finally show "f a \<le> f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))" .
qed
qed
@@ -610,11 +610,11 @@
fix x y
assume xy: "x \<in> sets M" "y \<in> sets M" "x \<subseteq> y"
have "f x \<le> f x + f (y-x)" using posf
- by (simp add: positive_def) (metis Diff xy)
+ by (simp add: positive_def) (metis Diff xy(1,2))
also have "... = f (x \<union> (y-x))" using addf
- by (auto simp add: additive_def) (metis Diff_disjoint Un_Diff_cancel Diff xy)
+ by (auto simp add: additive_def) (metis Diff_disjoint Un_Diff_cancel Diff xy(1,2))
also have "... = f y"
- by (metis Un_Diff_cancel Un_absorb1 xy)
+ by (metis Un_Diff_cancel Un_absorb1 xy(3))
finally show "f x \<le> f y" .
qed
@@ -663,7 +663,7 @@
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)
+ using seq [symmetric] by (simp add: 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
@@ -704,7 +704,7 @@
apply (auto simp add: increasing_def)
apply (rule Inf_greatest, metis emptyE inf_measure_nonempty top posf)
apply (rule Inf_lower)
-apply (clarsimp simp add: measure_set_def, blast)
+apply (clarsimp simp add: measure_set_def, rule_tac x=A in exI, blast)
apply (blast intro: inf_measure_pos0 posf)
done
@@ -743,7 +743,7 @@
apply (simp add: disjoint_family_disjointed UN_disjointed_eq ss dA)
done
show ?thesis
- by (blast intro: Inf_lower y order_trans [OF _ ley] inf_measure_pos0 posf)
+ by (blast intro: y order_trans [OF _ ley] inf_measure_pos0 posf)
qed
lemma (in algebra) inf_measure_close:
--- a/src/HOL/Probability/Lebesgue.thy Thu May 20 23:22:37 2010 +0200
+++ b/src/HOL/Probability/Lebesgue.thy Thu May 20 21:19:38 2010 -0700
@@ -76,15 +76,14 @@
pos_part f \<in> borel_measurable M \<and> neg_part f \<in> borel_measurable M"
proof -
{ fix x
- have "f x = pos_part f x - neg_part f x"
+ have "pos_part f x - neg_part f x = f x"
unfolding pos_part_def neg_part_def unfolding max_def min_def
by auto }
- hence "(\<lambda> x. f x) = (\<lambda> x. pos_part f x - neg_part f x)" by auto
- hence "f = (\<lambda> x. pos_part f x - neg_part f x)" by blast
+ hence "(\<lambda> x. pos_part f x - neg_part f x) = (\<lambda>x. f x)" by auto
+ hence f: "(\<lambda> x. pos_part f x - neg_part f x) = f" by blast
from pos_part_borel_measurable[of f] neg_part_borel_measurable[of f]
borel_measurable_diff_borel_measurable[of "pos_part f" "neg_part f"]
- this
- show ?thesis by auto
+ show ?thesis unfolding f by fast
qed
context measure_space
--- a/src/HOL/Probability/Measure.thy Thu May 20 23:22:37 2010 +0200
+++ b/src/HOL/Probability/Measure.thy Thu May 20 21:19:38 2010 -0700
@@ -143,7 +143,7 @@
shows "A \<union> B \<in> smallest_ccdi_sets M"
proof -
have ra: "range (binaryset A B) \<in> Pow (smallest_ccdi_sets M)"
- by (simp add: range_binaryset_eq A B empty_sets smallest_ccdi_sets.Basic)
+ by (simp add: range_binaryset_eq A B smallest_ccdi_sets.Basic)
have di: "disjoint_family (binaryset A B)" using disj
by (simp add: disjoint_family_on_def binaryset_def Int_commute)
from Disj [OF ra di]
@@ -277,9 +277,8 @@
apply (blast intro: smallest_ccdi_sets.Disj)
done
hence "sigma_sets (space M) (sets M) \<subseteq> smallest_ccdi_sets M"
- by auto
- (metis sigma_algebra.sigma_sets_subset algebra.simps(1)
- algebra.simps(2) subsetD)
+ by clarsimp
+ (drule sigma_algebra.sigma_sets_subset [where a="sets M"], auto)
also have "... \<subseteq> C"
proof
fix x
@@ -344,7 +343,7 @@
show "algebra M"
by (blast intro: sigma_algebra.axioms local.sigma_algebra_axioms)
show "positive M (measure M)"
- by (simp add: positive_def empty_measure positive)
+ by (simp add: positive_def positive)
qed
lemma (in measure_space) measure_additive:
@@ -410,7 +409,7 @@
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)
next
case (Suc m)
have "A (Suc m) = A m \<union> (A (Suc m) - A m)"
@@ -440,7 +439,7 @@
have A1: "\<And>i. A (Suc i) - A i \<in> sets M"
by (metis A Diff range_subsetD)
have A2: "(\<Union>i. A (Suc i) - A i) \<in> sets M"
- by (blast intro: countable_UN range_subsetD [OF A])
+ by (blast intro: range_subsetD [OF A])
have "(measure M o (\<lambda>i. A (Suc i) - A i)) sums measure M (\<Union>i. A (Suc i) - A i)"
by (rule measure_countably_additive)
(auto simp add: disjoint_family_Suc ASuc A1 A2)
@@ -486,7 +485,8 @@
assume y: "y \<in> sets b"
with a b f
have "space a - f -` y = f -` (space b - y)"
- by (auto simp add: sigma_algebra_iff2) (blast intro: ba)
+ by (auto, clarsimp simp add: sigma_algebra_iff2)
+ (drule ba, blast intro: ba)
hence "space a - (f -` y) \<in> (vimage f) ` sets b"
by auto
(metis b y subsetD equalityE imageI sigma_algebra.sigma_sets_eq
@@ -788,7 +788,7 @@
show ?thesis
proof (rule measurable_sigma)
show "prod_sets (sets a1) (sets a2) \<subseteq> Pow (space a1 \<times> space a2)" using sa1 sa2
- by (force simp add: prod_sets_def sigma_algebra_iff algebra_def)
+ by (auto simp add: prod_sets_def sigma_algebra_iff dest: algebra.space_closed)
next
show "f \<in> space M \<rightarrow> space a1 \<times> space a2"
by (rule prod_final [OF fn1 fn2])
@@ -843,13 +843,13 @@
next
case (insert x t)
hence x: "x \<in> s" and t: "t \<subseteq> s"
- by (simp_all add: insert_subset)
+ by simp_all
hence ts: "t \<in> sets M" using insert
by (metis Diff_insert_absorb Diff ssets)
have "measure M (insert x t) = measure M ({x} \<union> t)"
by simp
also have "... = measure M {x} + measure M t"
- by (simp add: measure_additive insert insert_disjoint ssets x ts
+ by (simp add: measure_additive insert ssets x ts
del: Un_insert_left)
also have "... = (\<Sum>x\<in>insert x t. measure M {x})"
by (simp add: x t ts insert)
--- a/src/HOL/Probability/Sigma_Algebra.thy Thu May 20 23:22:37 2010 +0200
+++ b/src/HOL/Probability/Sigma_Algebra.thy Thu May 20 21:19:38 2010 -0700
@@ -75,8 +75,8 @@
assumes a: "range a \<subseteq> sets M"
shows "(\<Inter>i::nat. a i) \<in> sets M"
proof -
- have "space M - (\<Union>i. space M - a i) \<in> sets M" using a
- by (blast intro: countable_UN compl_sets a)
+ from a have "\<forall>i. a i \<in> sets M" by fast
+ hence "space M - (\<Union>i. space M - a i) \<in> sets M" by blast
moreover
have "(\<Inter>i. a i) = space M - (\<Union>i. space M - a i)" using space_closed a
by blast
@@ -161,7 +161,7 @@
lemma sigma_sets_Un:
"a \<in> sigma_sets sp A \<Longrightarrow> b \<in> sigma_sets sp A \<Longrightarrow> a \<union> b \<in> sigma_sets sp A"
apply (simp add: Un_range_binary range_binary_eq)
-apply (metis Union COMBK_def binary_def fun_upd_apply)
+apply (rule Union, simp add: binary_def COMBK_def fun_upd_apply)
done
lemma sigma_sets_Inter:
@@ -210,7 +210,7 @@
"sigma_sets (space M) (sets M) = sets M"
proof
show "sets M \<subseteq> sigma_sets (space M) (sets M)"
- by (metis Set.subsetI sigma_sets.Basic space_closed)
+ by (metis Set.subsetI sigma_sets.Basic)
next
show "sigma_sets (space M) (sets M) \<subseteq> sets M"
by (metis sigma_sets_subset subset_refl)
@@ -221,7 +221,7 @@
apply (auto simp add: sigma_algebra_def sigma_algebra_axioms_def
algebra_def sigma_sets.Empty sigma_sets.Compl sigma_sets_Un)
apply (blast dest: sigma_sets_into_sp)
- apply (blast intro: sigma_sets.intros)
+ apply (rule sigma_sets.Union, fast)
done
lemma sigma_algebra_sigma: