# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1438100101 -3600
# Node ID 9ede42599eeb047fb48253383771720da7613624
# Parent  457abb82fb9eb332b9b7ded07da77754cc28e1df
tweaks. Got rid of a really slow step

diff -r 457abb82fb9e -r 9ede42599eeb src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue Jul 28 16:16:13 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Tue Jul 28 17:15:01 2015 +0100
@@ -10,17 +10,18 @@
   "~~/src/HOL/Library/Indicator_Function"
 begin
 
-lemma cSup_abs_le: (* TODO: is this really needed? *)
+lemma cSup_abs_le: (* TODO: move to Conditionally_Complete_Lattices.thy? *)
   fixes S :: "real set"
-  shows "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Sup S\<bar> \<le> a"
+  shows "S \<noteq> {} \<Longrightarrow> (\<And>x. x\<in>S \<Longrightarrow> \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Sup S\<bar> \<le> a"
   by (auto simp add: abs_le_interval_iff intro: cSup_least) (metis cSup_upper2 bdd_aboveI)
 
-lemma cInf_abs_ge: (* TODO: is this really needed? *)
+lemma cInf_abs_ge: 
   fixes S :: "real set"
-  shows "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Inf S\<bar> \<le> a"
-  by (simp add: Inf_real_def) (insert cSup_abs_le [of "uminus ` S"], auto)
-
-lemma cSup_asclose: (* TODO: is this really needed? *)
+  shows "S \<noteq> {} \<Longrightarrow> (\<And>x. x\<in>S \<Longrightarrow> \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Inf S\<bar> \<le> a"
+  using cSup_abs_le [of "uminus ` S"]
+  by (fastforce simp add: Inf_real_def)
+
+lemma cSup_asclose:
   fixes S :: "real set"
   assumes S: "S \<noteq> {}"
     and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e"
@@ -34,7 +35,7 @@
     unfolding th by (auto intro!: cSup_upper2 cSup_least)
 qed
 
-lemma cInf_asclose: (* TODO: is this really needed? *)
+lemma cInf_asclose:
   fixes S :: "real set"
   assumes S: "S \<noteq> {}"
     and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e"
@@ -4931,11 +4932,10 @@
     from p(4)[unfolded xk, OF insertI1] guess u v by (elim exE) note uv=this
 
     have "finite {k. \<exists>x. (x, k) \<in> p}"
-      apply (rule finite_subset[of _ "snd ` p"],rule)
-      unfolding subset_eq image_iff mem_Collect_eq
-      apply (erule exE)
-      apply (rule_tac x="(xa,x)" in bexI)
+      apply (rule finite_subset[of _ "snd ` p"])
       using p
+      apply safe
+      apply (metis image_iff snd_conv)
       apply auto
       done
     then have int: "interior (cbox u v) \<inter> interior (\<Union>{k. \<exists>x. (x, k) \<in> p}) = {}"
@@ -4978,7 +4978,7 @@
         apply rule
         apply rule
         apply (erule insertE)
-        defer
+        apply (simp add: uv xk)
         apply (rule UnI2)
         apply (drule q1(3)[rule_format])
         unfolding xk uv
@@ -5002,7 +5002,7 @@
         apply rule
         apply (erule insertE)
         apply (rule UnI2)
-        defer
+        apply (simp add: False uv xk)
         apply (drule q1(3)[rule_format])
         using False
         unfolding xk uv
@@ -11771,7 +11771,9 @@
         prefer 5 unfolding real_norm_def
         apply rule
         apply (rule cSup_abs_le)
-        prefer 5
+        using assms
+        apply (force simp add: )
+        prefer 4
         apply rule
         apply (rule_tac g=h in absolutely_integrable_integrable_bound)
         using assms
diff -r 457abb82fb9e -r 9ede42599eeb src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Tue Jul 28 16:16:13 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Tue Jul 28 17:15:01 2015 +0100
@@ -1203,7 +1203,7 @@
     show ?lhs
       using i False
       apply (auto simp add: dependent_def)
-      by (metis in_span_insert insert_Diff insert_Diff_if insert_iff)
+      by (metis in_span_insert insert_Diff_if insert_Diff_single insert_absorb)
   qed
 qed