# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1497543743 -3600
# Node ID def95e0bc529e3c1693bc398eafe33e3ce4dfe60
# Parent  c9c9438cfc0f5bf1498e0ae4fec183ec1191bfd3
Some new material. SIMPRULE STATUS for sum/prod.delta rules!

diff -r c9c9438cfc0f -r def95e0bc529 src/HOL/Analysis/Bounded_Linear_Function.thy
--- a/src/HOL/Analysis/Bounded_Linear_Function.thy	Thu Jun 15 11:11:36 2017 +0200
+++ b/src/HOL/Analysis/Bounded_Linear_Function.thy	Thu Jun 15 17:22:23 2017 +0100
@@ -387,7 +387,7 @@
   have "(\<Sum>j\<in>Basis. \<Sum>i\<in>Basis. (x \<bullet> i * (f i \<bullet> j)) *\<^sub>R j) \<bullet> b
     = (\<Sum>j\<in>Basis. if j = b then (\<Sum>i\<in>Basis. (x \<bullet> i * (f i \<bullet> j))) else 0)"
     using b
-    by (auto simp add: algebra_simps inner_sum_left inner_Basis split: if_split intro!: sum.cong)
+    by (simp add: inner_sum_left inner_Basis if_distrib cong: if_cong) (simp add: sum.commute)
   also have "\<dots> = (\<Sum>i\<in>Basis. (x \<bullet> i * (f i \<bullet> b)))"
     using b by (simp add: sum.delta)
   also have "\<dots> = f x \<bullet> b"
diff -r c9c9438cfc0f -r def95e0bc529 src/HOL/Analysis/Complex_Analysis_Basics.thy
--- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Thu Jun 15 11:11:36 2017 +0200
+++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Thu Jun 15 17:22:23 2017 +0100
@@ -919,7 +919,6 @@
   apply (auto simp:  bounded_linear_mult_right)
   done
 
-(*Used only once, in Multivariate/cauchy.ml. *)
 lemma has_complex_derivative_inverse_strong:
   fixes f :: "complex \<Rightarrow> complex"
   shows "DERIV f x :> f' \<Longrightarrow>
diff -r c9c9438cfc0f -r def95e0bc529 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Jun 15 11:11:36 2017 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Jun 15 17:22:23 2017 +0100
@@ -55,7 +55,7 @@
 lemma content_unit[iff]: "content (cbox 0 (One::'a::euclidean_space)) = 1"
   by simp
 
-lemma content_pos_le[intro]: "0 \<le> content (cbox a b)"
+lemma content_pos_le [iff]: "0 \<le> content X"
   by simp
 
 corollary content_nonneg [simp]: "~ content (cbox a b) < 0"
@@ -157,20 +157,18 @@
 lemma sum_content_null:
   assumes "content (cbox a b) = 0"
     and "p tagged_division_of (cbox a b)"
-  shows "sum (\<lambda>(x,k). content k *\<^sub>R f x) p = (0::'a::real_normed_vector)"
+  shows "(\<Sum>(x,k)\<in>p. content k *\<^sub>R f x) = (0::'a::real_normed_vector)"
 proof (rule sum.neutral, rule)
   fix y
   assume y: "y \<in> p"
   obtain x k where xk: "y = (x, k)"
     using surj_pair[of y] by blast
-  note assm = tagged_division_ofD(3-4)[OF assms(2) y[unfolded xk]]
-  from this(2) obtain c d where k: "k = cbox c d" by blast
+  then obtain c d where k: "k = cbox c d" "k \<subseteq> cbox a b"
+    by (metis assms(2) tagged_division_ofD(3) tagged_division_ofD(4) y)
   have "(\<lambda>(x, k). content k *\<^sub>R f x) y = content k *\<^sub>R f x"
     unfolding xk by auto
   also have "\<dots> = 0"
-    using content_subset[OF assm(1)[unfolded k]] content_pos_le[of c d]
-    unfolding assms(1) k
-    by auto
+    using assms(1) content_0_subset k(2) by auto
   finally show "(\<lambda>(x, k). content k *\<^sub>R f x) y = 0" .
 qed
 
@@ -446,6 +444,11 @@
   "(f has_integral y) s \<Longrightarrow> ((\<lambda>x. f x *\<^sub>R c) has_integral (y *\<^sub>R c)) s"
   using has_integral_linear[OF _ bounded_linear_scaleR_left] by (simp add: comp_def)
 
+lemma integrable_on_scaleR_left:
+  assumes "f integrable_on A" 
+  shows "(\<lambda>x. f x *\<^sub>R y) integrable_on A" 
+  using assms has_integral_scaleR_left unfolding integrable_on_def by blast
+
 lemma has_integral_mult_left:
   fixes c :: "_ :: real_normed_algebra"
   shows "(f has_integral y) s \<Longrightarrow> ((\<lambda>x. f x * c) has_integral (y * c)) s"
@@ -670,12 +673,8 @@
   by (auto intro: has_integral_sum integrable_integral)
 
 lemma integrable_sum:
-  "\<lbrakk>finite t;  \<forall>a\<in>t. (f a) integrable_on s\<rbrakk> \<Longrightarrow> (\<lambda>x. sum (\<lambda>a. f a x) t) integrable_on s"
-  unfolding integrable_on_def
-  apply (drule bchoice)
-  using has_integral_sum[of t]
-  apply auto
-  done
+  "\<lbrakk>finite I;  \<And>a. a \<in> I \<Longrightarrow> f a integrable_on S\<rbrakk> \<Longrightarrow> (\<lambda>x. \<Sum>a\<in>I. f a x) integrable_on S"
+  unfolding integrable_on_def using has_integral_sum[of I] by metis
 
 lemma has_integral_eq:
   assumes "\<And>x. x \<in> s \<Longrightarrow> f x = g x"
@@ -5493,32 +5492,10 @@
       apply (rule_tac[!] sum_nonneg)
       apply safe
       unfolding real_scaleR_def right_diff_distrib[symmetric]
-      apply (rule_tac[!] mult_nonneg_nonneg)
-    proof -
-      fix a b
-      assume ab: "(a, b) \<in> p1"
-      show "0 \<le> content b"
-        using *(3)[OF ab]
-        apply safe
-        apply (rule content_pos_le)
+         apply (rule_tac[!] mult_nonneg_nonneg)
+        apply simp_all
+      using obt(4) prems(1) prems(4) apply (blast intro:  elim: dest!: bspec)+
         done
-      then show "0 \<le> content b" .
-      show "0 \<le> f a - g a" "0 \<le> h a - f a"
-        using *(1-2)[OF ab]
-        using obt(4)[rule_format,of a]
-        by auto
-    next
-      fix a b
-      assume ab: "(a, b) \<in> p2"
-      show "0 \<le> content b"
-        using *(6)[OF ab]
-        apply safe
-        apply (rule content_pos_le)
-        done
-      then show "0 \<le> content b" .
-      show "0 \<le> f a - g a" and "0 \<le> h a - f a"
-        using *(4-5)[OF ab] using obt(4)[rule_format,of a] by auto
-    qed
     then show ?case
       apply -
       unfolding real_norm_def
@@ -6317,7 +6294,7 @@
     proof (rule, goal_cases)
       case prems: (1 x)
       have "e / (4 * content (cbox a b)) > 0"
-        using \<open>e>0\<close> False content_pos_le[of a b] by (simp add: less_le)
+        by (simp add: False content_lt_nz e)
       from assms(3)[rule_format, OF prems, THEN LIMSEQ_D, OF this]
       guess n .. note n=this
       then show ?case
@@ -7094,9 +7071,10 @@
       also have "\<dots> = content (cbox a b) * e * norm (x - x0)"
         by simp
       also have "\<dots> < e' * norm (x - x0)"
-        using \<open>e' > 0\<close> content_pos_le[of a b]
-        by (intro mult_strict_right_mono[OF _ \<open>0 < norm (x - x0)\<close>])
-           (auto simp: divide_simps e_def simp del: measure_nonneg)
+        using \<open>e' > 0\<close>
+        apply (intro mult_strict_right_mono[OF _ \<open>0 < norm (x - x0)\<close>])  
+        apply  (auto simp: divide_simps e_def)
+        by (metis \<open>0 < e\<close> e_def order.asym zero_less_divide_iff)
       finally have "norm (?F x - ?F x0 - ?dF (x - x0)) < e' * norm (x - x0)" .
       then show ?case
         by (auto simp: divide_simps)
@@ -7207,8 +7185,7 @@
       define e' where "e' = e / 2"
       with \<open>e > 0\<close> have "e' > 0" by simp
       then have "\<forall>\<^sub>F n in F. \<forall>x\<in>cbox a b. norm (f n x - g x) < e' / content (cbox a b)"
-        using u content_nonzero content_pos_le[of a b]
-        by (auto simp: uniform_limit_iff dist_norm simp del: measure_nonneg)
+        using u content_nonzero by (auto simp: uniform_limit_iff dist_norm zero_less_measure_iff)
       then show "\<forall>\<^sub>F n in F. dist (I n) J < e"
       proof eventually_elim
         case (elim n)
diff -r c9c9438cfc0f -r def95e0bc529 src/HOL/Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Thu Jun 15 11:11:36 2017 +0200
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Thu Jun 15 17:22:23 2017 +0100
@@ -1665,8 +1665,8 @@
 definition "is_interval (s::('a::euclidean_space) set) \<longleftrightarrow>
   (\<forall>a\<in>s. \<forall>b\<in>s. \<forall>x. (\<forall>i\<in>Basis. ((a\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> b\<bullet>i) \<or> (b\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> a\<bullet>i))) \<longrightarrow> x \<in> s)"
 
-lemma is_interval_cbox: "is_interval (cbox a (b::'a::euclidean_space))" (is ?th1)
-  and is_interval_box: "is_interval (box a b)" (is ?th2)
+lemma is_interval_cbox [simp]: "is_interval (cbox a (b::'a::euclidean_space))" (is ?th1)
+  and is_interval_box [simp]: "is_interval (box a b)" (is ?th2)
   unfolding is_interval_def mem_box Ball_def atLeastAtMost_iff
   by (meson order_trans le_less_trans less_le_trans less_trans)+
 
@@ -1726,12 +1726,28 @@
   by (simp add: box_ne_empty inner_Basis inner_sum_left sum_nonneg)
 
 lemma box01_nonempty [simp]: "box 0 One \<noteq> {}"
-  by (simp add: box_ne_empty inner_Basis inner_sum_left) (simp add: sum.remove)
+  by (simp add: box_ne_empty inner_Basis inner_sum_left)
 
 lemma empty_as_interval: "{} = cbox One (0::'a::euclidean_space)"
   using nonempty_Basis box01_nonempty box_eq_empty(1) box_ne_empty(1) by blast
 
-
+lemma interval_subset_is_interval:
+  assumes "is_interval S"
+  shows "cbox a b \<subseteq> S \<longleftrightarrow> cbox a b = {} \<or> a \<in> S \<and> b \<in> S" (is "?lhs = ?rhs")
+proof
+  assume ?lhs
+  then show ?rhs  using box_ne_empty(1) mem_box(2) by fastforce
+next
+  assume ?rhs
+  have "cbox a b \<subseteq> S" if "a \<in> S" "b \<in> S"
+    using assms unfolding is_interval_def
+    apply (clarsimp simp add: mem_box)
+    using that by blast
+  with \<open>?rhs\<close> show ?lhs
+    by blast
+qed
+
+  
 subsection \<open>Connectedness\<close>
 
 lemma connected_local:
@@ -5641,35 +5657,6 @@
   qed
 qed (metis compact_imp_complete compact_imp_seq_compact seq_compact_imp_totally_bounded)
 
-lemma cauchy: "Cauchy s \<longleftrightarrow> (\<forall>e>0.\<exists> N::nat. \<forall>n\<ge>N. dist(s n)(s N) < e)" (is "?lhs = ?rhs")
-proof -
-  {
-    assume ?rhs
-    {
-      fix e::real
-      assume "e>0"
-      with \<open>?rhs\<close> obtain N where N:"\<forall>n\<ge>N. dist (s n) (s N) < e/2"
-        by (erule_tac x="e/2" in allE) auto
-      {
-        fix n m
-        assume nm:"N \<le> m \<and> N \<le> n"
-        then have "dist (s m) (s n) < e" using N
-          using dist_triangle_half_l[of "s m" "s N" "e" "s n"]
-          by blast
-      }
-      then have "\<exists>N. \<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (s m) (s n) < e"
-        by blast
-    }
-    then have ?lhs
-      unfolding cauchy_def
-      by blast
-  }
-  then show ?thesis
-    unfolding cauchy_def
-    using dist_triangle_half_l
-    by blast
-qed
-
 lemma cauchy_imp_bounded:
   assumes "Cauchy s"
   shows "bounded (range s)"
@@ -6978,6 +6965,11 @@
   ultimately show ?thesis ..
 qed
 
+lemma bounded_uniformly_continuous_image:
+  fixes f :: "'a :: heine_borel \<Rightarrow> 'b :: heine_borel"
+  assumes "uniformly_continuous_on S f" "bounded S"
+  shows "bounded(image f S)"
+  by (metis (no_types, lifting) assms bounded_closure_image compact_closure compact_continuous_image compact_eq_bounded_closed image_cong uniformly_continuous_imp_continuous uniformly_continuous_on_extension_on_closure)
 
 subsection\<open>Quotient maps\<close>
 
@@ -9521,7 +9513,7 @@
   have "\<exists>N. \<forall>n\<ge>N. norm (x n - x N) < d" if "d > 0" for d :: real
   proof -
     from that obtain N where N: "\<forall>n\<ge>N. norm (f (x n) - f (x N)) < e * d"
-      using cf[unfolded cauchy o_def dist_norm, THEN spec[where x="e*d"]] e
+      using cf[unfolded Cauchy_def o_def dist_norm, THEN spec[where x="e*d"]] e
       by auto
     have "norm (x n - x N) < d" if "n \<ge> N" for n
     proof -
@@ -9538,7 +9530,7 @@
     then show ?thesis by auto
   qed
   then show ?thesis
-    by (simp add: cauchy dist_norm)
+    by (simp add: Cauchy_altdef2 dist_norm)
 qed
 
 lemma complete_isometric_image:
diff -r c9c9438cfc0f -r def95e0bc529 src/HOL/Computational_Algebra/Formal_Power_Series.thy
--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Thu Jun 15 11:11:36 2017 +0200
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Thu Jun 15 17:22:23 2017 +0100
@@ -923,9 +923,7 @@
 
 lemma fps_sum_rep_nth: "(sum (\<lambda>i. fps_const(a$i)*X^i) {0..m})$n =
     (if n \<le> m then a$n else 0::'a::comm_ring_1)"
-  apply (auto simp add: fps_sum_nth cond_value_iff cong del: if_weak_cong)
-  apply (simp add: sum.delta')
-  done
+  by (auto simp add: fps_sum_nth cond_value_iff cong del: if_weak_cong)
 
 lemma fps_notation: "(\<lambda>n. sum (\<lambda>i. fps_const(a$i) * X^i) {0..n}) \<longlonglongrightarrow> a"
   (is "?s \<longlonglongrightarrow> a")
diff -r c9c9438cfc0f -r def95e0bc529 src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Thu Jun 15 11:11:36 2017 +0200
+++ b/src/HOL/Groups_Big.thy	Thu Jun 15 17:22:23 2017 +0100
@@ -332,7 +332,7 @@
     by (intro reindex_bij_betw_not_neutral[OF _ _ bij]) auto
 qed
 
-lemma delta:
+lemma delta [simp]:
   assumes fS: "finite S"
   shows "F (\<lambda>k. if k = a then b k else \<^bold>1) S = (if a \<in> S then b a else \<^bold>1)"
 proof -
@@ -355,7 +355,7 @@
   qed
 qed
 
-lemma delta':
+lemma delta' [simp]:
   assumes fin: "finite S"
   shows "F (\<lambda>k. if a = k then b k else \<^bold>1) S = (if a \<in> S then b a else \<^bold>1)"
   using delta [OF fin, of a b, symmetric] by (auto intro: cong)
diff -r c9c9438cfc0f -r def95e0bc529 src/HOL/Probability/Fin_Map.thy
--- a/src/HOL/Probability/Fin_Map.thy	Thu Jun 15 11:11:36 2017 +0200
+++ b/src/HOL/Probability/Fin_Map.thy	Thu Jun 15 17:22:23 2017 +0100
@@ -474,7 +474,7 @@
   fix P::"nat \<Rightarrow> 'a \<Rightarrow>\<^sub>F 'b"
   assume "Cauchy P"
   then obtain Nd where Nd: "\<And>n. n \<ge> Nd \<Longrightarrow> dist (P n) (P Nd) < 1"
-    by (force simp: cauchy)
+    by (force simp: Cauchy_altdef2)
   define d where "d = domain (P Nd)"
   with Nd have dim: "\<And>n. n \<ge> Nd \<Longrightarrow> domain (P n) = d" using dist_le_1_imp_domain_eq by auto
   have [simp]: "finite d" unfolding d_def by simp
@@ -484,11 +484,11 @@
   have q: "\<And>i. i \<in> d \<Longrightarrow> q i = Q i" by (auto simp add: Q_def Abs_fmap_inverse)
   {
     fix i assume "i \<in> d"
-    have "Cauchy (p i)" unfolding cauchy p_def
+    have "Cauchy (p i)" unfolding Cauchy_altdef2 p_def
     proof safe
       fix e::real assume "0 < e"
       with \<open>Cauchy P\<close> obtain N where N: "\<And>n. n\<ge>N \<Longrightarrow> dist (P n) (P N) < min e 1"
-        by (force simp: cauchy min_def)
+        by (force simp: Cauchy_altdef2 min_def)
       hence "\<And>n. n \<ge> N \<Longrightarrow> domain (P n) = domain (P N)" using dist_le_1_imp_domain_eq by auto
       with dim have dim: "\<And>n. n \<ge> N \<Longrightarrow> domain (P n) = d" by (metis nat_le_linear)
       show "\<exists>N. \<forall>n\<ge>N. dist ((P n) i) ((P N) i) < e"
diff -r c9c9438cfc0f -r def95e0bc529 src/HOL/Probability/Probability_Mass_Function.thy
--- a/src/HOL/Probability/Probability_Mass_Function.thy	Thu Jun 15 11:11:36 2017 +0200
+++ b/src/HOL/Probability/Probability_Mass_Function.thy	Thu Jun 15 17:22:23 2017 +0100
@@ -2111,7 +2111,7 @@
     by (rule sum.commute)
   also have "\<dots> = (\<Sum>xa = 0..<length xs. if fst (xs ! xa) \<in> A then
                      (\<Sum>x\<in>set (map fst xs). if x = fst (xs ! xa) then snd (xs ! xa) else 0) else 0)"
-    by (auto intro!: sum.cong sum.neutral)
+    by (auto intro!: sum.cong sum.neutral simp del: sum.delta)
   also have "\<dots> = (\<Sum>xa = 0..<length xs. if fst (xs ! xa) \<in> A then snd (xs ! xa) else 0)"
     by (intro sum.cong refl) (simp_all add: sum.delta)
   also have "\<dots> = sum_list (map snd (filter (\<lambda>x. fst x \<in> A) xs))"
diff -r c9c9438cfc0f -r def95e0bc529 src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Thu Jun 15 11:11:36 2017 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy	Thu Jun 15 17:22:23 2017 +0100
@@ -1949,6 +1949,33 @@
   qed
 qed
 
+lemma (in metric_space) Cauchy_altdef2: "Cauchy s \<longleftrightarrow> (\<forall>e>0. \<exists>N::nat. \<forall>n\<ge>N. dist(s n)(s N) < e)" (is "?lhs = ?rhs")
+proof 
+  assume "Cauchy s"
+  then show ?rhs by (force simp add: Cauchy_def)
+next
+    assume ?rhs
+    {
+      fix e::real
+      assume "e>0"
+      with \<open>?rhs\<close> obtain N where N: "\<forall>n\<ge>N. dist (s n) (s N) < e/2"
+        by (erule_tac x="e/2" in allE) auto
+      {
+        fix n m
+        assume nm: "N \<le> m \<and> N \<le> n"
+        then have "dist (s m) (s n) < e" using N
+          using dist_triangle_half_l[of "s m" "s N" "e" "s n"]
+          by blast
+      }
+      then have "\<exists>N. \<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (s m) (s n) < e"
+        by blast
+    }
+    then have ?lhs
+      unfolding Cauchy_def by blast
+  then show ?lhs
+    by blast
+qed
+
 lemma (in metric_space) metric_CauchyI:
   "(\<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e) \<Longrightarrow> Cauchy X"
   by (simp add: Cauchy_def)