# HG changeset patch
# User huffman
# Date 1274415578 25200
# Node ID 58a0757031dd6e62768ee7ada1afb2fa4e0099a2
# Parent  21010d2b41e72ca211cd3d203b4f43e17e919d97
speed up some proofs and fix some warnings

diff -r 21010d2b41e7 -r 58a0757031dd src/HOL/Probability/Borel.thy
--- 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]
diff -r 21010d2b41e7 -r 58a0757031dd src/HOL/Probability/Caratheodory.thy
--- 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:
diff -r 21010d2b41e7 -r 58a0757031dd src/HOL/Probability/Lebesgue.thy
--- 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
diff -r 21010d2b41e7 -r 58a0757031dd src/HOL/Probability/Measure.thy
--- 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) 
diff -r 21010d2b41e7 -r 58a0757031dd src/HOL/Probability/Sigma_Algebra.thy
--- 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: