# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1475078461 -3600
# Node ID 354808e9f44b4a06852d867e07a7c46b94dc8573
# Parent  cdc1e59aa51378fbf210999cf7d546fe89faeac2
new material connected with HOL Light measure theory, plus more rationalisation

diff -r cdc1e59aa513 -r 354808e9f44b src/HOL/Analysis/Borel_Space.thy
--- a/src/HOL/Analysis/Borel_Space.thy	Mon Sep 26 07:56:54 2016 +0200
+++ b/src/HOL/Analysis/Borel_Space.thy	Wed Sep 28 17:01:01 2016 +0100
@@ -101,7 +101,7 @@
   assumes mono: "mono_on f A" and deriv: "(f has_real_derivative D) (at x)"
   assumes "x \<in> interior A"
   shows "D \<ge> 0"
-proof (rule tendsto_le_const)
+proof (rule tendsto_lowerbound)
   let ?A' = "(\<lambda>y. y - x) ` interior A"
   from deriv show "((\<lambda>h. (f (x + h) - f x) / h) \<longlongrightarrow> D) (at 0)"
       by (simp add: field_has_derivative_at has_field_derivative_def)
diff -r cdc1e59aa513 -r 354808e9f44b src/HOL/Analysis/Bounded_Linear_Function.thy
--- a/src/HOL/Analysis/Bounded_Linear_Function.thy	Mon Sep 26 07:56:54 2016 +0200
+++ b/src/HOL/Analysis/Bounded_Linear_Function.thy	Wed Sep 28 17:01:01 2016 +0100
@@ -328,7 +328,7 @@
         have tendsto_v: "(\<lambda>m. norm (X n x - X m x)) \<longlonglongrightarrow> norm (X n x - Blinfun v x)"
           by (auto intro!: tendsto_intros Bv)
         show "norm ((X n - Blinfun v) x) \<le> r' * norm x"
-          by (auto intro!: tendsto_ge_const tendsto_v ev_le simp: blinfun.bilinear_simps)
+          by (auto intro!: tendsto_upperbound tendsto_v ev_le simp: blinfun.bilinear_simps)
       qed (simp add: \<open>0 < r'\<close> less_imp_le)
       thus "norm (X n - Blinfun v) < r"
         by (metis \<open>r' < r\<close> le_less_trans)
diff -r cdc1e59aa513 -r 354808e9f44b src/HOL/Analysis/Derivative.thy
--- a/src/HOL/Analysis/Derivative.thy	Mon Sep 26 07:56:54 2016 +0200
+++ b/src/HOL/Analysis/Derivative.thy	Wed Sep 28 17:01:01 2016 +0100
@@ -1998,7 +1998,7 @@
           by (auto simp add: algebra_simps)
       qed
       ultimately show "norm (f n x - f n y - (g x - g y)) \<le> e * norm (x - y)"
-        by (rule tendsto_ge_const[OF trivial_limit_sequentially])
+        by (simp add: tendsto_upperbound)
     qed
   qed
   have "\<forall>x\<in>s. ((\<lambda>n. f n x) \<longlongrightarrow> g x) sequentially \<and> (g has_derivative g' x) (at x within s)"
@@ -2667,7 +2667,7 @@
   qed
   hence "eventually (\<lambda>y. (f y - f c) / (y - c) \<le> (f x - f c) / (x - c)) (at c within ?A')"
     by (blast intro: filter_leD at_le)
-  ultimately have "f' \<le> (f x - f c) / (x - c)" by (rule tendsto_ge_const)
+  ultimately have "f' \<le> (f x - f c) / (x - c)" by (simp add: tendsto_upperbound)
   thus ?thesis using xc by (simp add: field_simps)
 next
   assume xc: "x < c"
@@ -2691,7 +2691,7 @@
   qed
   hence "eventually (\<lambda>y. (f y - f c) / (y - c) \<ge> (f x - f c) / (x - c)) (at c within ?A')"
     by (blast intro: filter_leD at_le)
-  ultimately have "f' \<ge> (f x - f c) / (x - c)" by (rule tendsto_le_const)
+  ultimately have "f' \<ge> (f x - f c) / (x - c)" by (simp add: tendsto_lowerbound)
   thus ?thesis using xc by (simp add: field_simps)
 qed simp_all
 
diff -r cdc1e59aa513 -r 354808e9f44b src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Mon Sep 26 07:56:54 2016 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Wed Sep 28 17:01:01 2016 +0100
@@ -1870,7 +1870,7 @@
   have F_mono: "a \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> F x \<le> F y" for x y
     using f nonneg by (intro DERIV_nonneg_imp_nondecreasing[of x y F]) (auto intro: order_trans)
   then have F_le_T: "a \<le> x \<Longrightarrow> F x \<le> T" for x
-    by (intro tendsto_le_const[OF _ lim])
+    by (intro tendsto_lowerbound[OF lim])
        (auto simp: trivial_limit_at_top_linorder eventually_at_top_linorder)
 
   have "(SUP i::nat. ?f i x) = ?fR x" for x
diff -r cdc1e59aa513 -r 354808e9f44b src/HOL/Analysis/Euclidean_Space.thy
--- a/src/HOL/Analysis/Euclidean_Space.thy	Mon Sep 26 07:56:54 2016 +0200
+++ b/src/HOL/Analysis/Euclidean_Space.thy	Wed Sep 28 17:01:01 2016 +0100
@@ -93,6 +93,11 @@
     by (auto intro!: exI[of _ "\<Sum>i\<in>Basis. f i *\<^sub>R i"])
 qed auto
 
+lemma (in euclidean_space) bchoice_Basis_iff:
+  fixes P :: "'a \<Rightarrow> real \<Rightarrow> bool"
+  shows "(\<forall>i\<in>Basis. \<exists>x\<in>A. P i x) \<longleftrightarrow> (\<exists>x. \<forall>i\<in>Basis. inner x i \<in> A \<and> P i (inner x i))"
+by (simp add: choice_Basis_iff Bex_def)
+
 lemma (in euclidean_space) euclidean_representation_setsum_fun:
     "(\<lambda>x. \<Sum>b\<in>Basis. inner (f x) b *\<^sub>R b) = f"
   by (rule ext) (simp add: euclidean_representation_setsum)
diff -r cdc1e59aa513 -r 354808e9f44b src/HOL/Analysis/Gamma_Function.thy
--- a/src/HOL/Analysis/Gamma_Function.thy	Mon Sep 26 07:56:54 2016 +0200
+++ b/src/HOL/Analysis/Gamma_Function.thy	Wed Sep 28 17:01:01 2016 +0100
@@ -1812,13 +1812,13 @@
   shows   "G x = Gamma x"
 proof (rule antisym)
   show "G x \<ge> Gamma x"
-  proof (rule tendsto_ge_const)
+  proof (rule tendsto_upperbound)
     from G_lower[of x] show "eventually (\<lambda>n. Gamma_series x n \<le> G x) sequentially"
       using eventually_ge_at_top[of "1::nat"] x by (auto elim!: eventually_mono)
   qed (simp_all add: Gamma_series_LIMSEQ)
 next
   show "G x \<le> Gamma x"
-  proof (rule tendsto_le_const)
+  proof (rule tendsto_lowerbound)
     have "(\<lambda>n. Gamma_series x n * (1 + x / real n)) \<longlonglongrightarrow> Gamma x * (1 + 0)"
       by (rule tendsto_intros real_tendsto_divide_at_top 
                Gamma_series_LIMSEQ filterlim_real_sequentially)+
diff -r cdc1e59aa513 -r 354808e9f44b src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Mon Sep 26 07:56:54 2016 +0200
+++ b/src/HOL/Deriv.thy	Wed Sep 28 17:01:01 2016 +0100
@@ -1563,12 +1563,12 @@
     and lim: "(f \<longlongrightarrow> flim) at_bot"
   shows "flim < f b"
 proof -
-  have "flim \<le> f (b - 1)"
-    apply (rule tendsto_ge_const [OF _ lim])
-     apply (auto simp: trivial_limit_at_bot_linorder eventually_at_bot_linorder)
+  have "\<exists>N. \<forall>n\<le>N. f n \<le> f (b - 1)"
     apply (rule_tac x="b - 2" in exI)
     apply (force intro: order.strict_implies_order DERIV_pos_imp_increasing [where f=f] assms)
     done
+  then have "flim \<le> f (b - 1)"
+     by (auto simp: trivial_limit_at_bot_linorder eventually_at_bot_linorder tendsto_upperbound [OF lim])
   also have "\<dots> < f b"
     by (force intro: DERIV_pos_imp_increasing [where f=f] assms)
   finally show ?thesis .
diff -r cdc1e59aa513 -r 354808e9f44b src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Mon Sep 26 07:56:54 2016 +0200
+++ b/src/HOL/Fields.thy	Wed Sep 28 17:01:01 2016 +0100
@@ -1192,6 +1192,20 @@
   finally show ?thesis .
 qed
 
+text\<open>For creating values between @{term u} and @{term v}.\<close>
+lemma scaling_mono:
+  assumes "u \<le> v" "0 \<le> r" "r \<le> s"
+    shows "u + r * (v - u) / s \<le> v"
+proof -
+  have "r/s \<le> 1" using assms
+    using divide_le_eq_1 by fastforce
+  then have "(r/s) * (v - u) \<le> 1 * (v - u)"
+    apply (rule mult_right_mono)
+    using assms by simp
+  then show ?thesis
+    by (simp add: field_simps)
+qed
+
 end
 
 text \<open>Min/max Simplification Rules\<close>
diff -r cdc1e59aa513 -r 354808e9f44b src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Mon Sep 26 07:56:54 2016 +0200
+++ b/src/HOL/Groups_Big.thy	Wed Sep 28 17:01:01 2016 +0100
@@ -47,6 +47,9 @@
 lemma insert_remove: "finite A \<Longrightarrow> F g (insert x A) = g x \<^bold>* F g (A - {x})"
   by (cases "x \<in> A") (simp_all add: remove insert_absorb)
 
+lemma insert_if: "finite A \<Longrightarrow> F g (insert x A) = (if x \<in> A then F g A else g x \<^bold>* F g A)"
+  by (cases "x \<in> A") (simp_all add: insert_absorb)
+
 lemma neutral: "\<forall>x\<in>A. g x = \<^bold>1 \<Longrightarrow> F g A = \<^bold>1"
   by (induct A rule: infinite_finite_induct) simp_all
 
@@ -1288,4 +1291,22 @@
   qed
 qed
 
+lemma setsum_image_le:
+  fixes g :: "'a \<Rightarrow> 'b::ordered_ab_group_add"
+  assumes "finite I" "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> g(f i)"
+    shows "setsum g (f ` I) \<le> setsum (g \<circ> f) I"
+  using assms
+proof induction
+  case empty
+  then show ?case by auto
+next
+  case (insert x F) then
+  have "setsum g (f ` insert x F) = setsum g (insert (f x) (f ` F))" by simp
+  also have "\<dots> \<le> g (f x) + setsum g (f ` F)"
+    by (simp add: insert setsum.insert_if)
+  also have "\<dots>  \<le> setsum (g \<circ> f) (insert x F)"
+    using insert by auto
+  finally show ?case .
+qed
+ 
 end
diff -r cdc1e59aa513 -r 354808e9f44b src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Mon Sep 26 07:56:54 2016 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Wed Sep 28 17:01:01 2016 +0100
@@ -3856,7 +3856,7 @@
   assumes "eventually (\<lambda>x. f x \<ge> 0) F"
   shows   "((\<lambda>x. inverse (f x)) \<longlongrightarrow> inverse c) F"
   by (cases "F = bot")
-     (auto intro!: tendsto_le_const[of F] assms
+     (auto intro!: tendsto_lowerbound assms
                    continuous_on_tendsto_compose[OF continuous_on_inverse_ereal])
 
 
diff -r cdc1e59aa513 -r 354808e9f44b src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Mon Sep 26 07:56:54 2016 +0200
+++ b/src/HOL/Limits.thy	Wed Sep 28 17:01:01 2016 +0100
@@ -2368,7 +2368,7 @@
   fixes f :: "real \<Rightarrow> real"
   assumes ev: "b < x" "\<forall> x' \<in> { b <..< x}. 0 \<le> f x'" and "isCont f x"
   shows "0 \<le> f x"
-proof (rule tendsto_le_const)
+proof (rule tendsto_lowerbound)
   show "(f \<longlongrightarrow> f x) (at_left x)"
     using \<open>isCont f x\<close> by (simp add: filterlim_at_split isCont_def)
   show "eventually (\<lambda>x. 0 \<le> f x) (at_left x)"
diff -r cdc1e59aa513 -r 354808e9f44b src/HOL/Order_Relation.thy
--- a/src/HOL/Order_Relation.thy	Mon Sep 26 07:56:54 2016 +0200
+++ b/src/HOL/Order_Relation.thy	Wed Sep 28 17:01:01 2016 +0100
@@ -397,6 +397,18 @@
   ultimately show ?thesis unfolding R_def by blast
 qed
 
+text\<open>A transitive relation is well-founded if all initial segments are finite.\<close>
+corollary wf_finite_segments:
+  assumes "irrefl r" and "trans r" and "\<And>x. finite {y. (y, x) \<in> r}"
+  shows "wf (r)"
+proof (clarsimp simp: trans_wf_iff wf_iff_acyclic_if_finite converse_def assms)
+  fix a
+  have "trans (r \<inter> ({x. (x, a) \<in> r} \<times> {x. (x, a) \<in> r}))"
+    using assms unfolding trans_def Field_def by blast
+  then show "acyclic (r \<inter> {x. (x, a) \<in> r} \<times> {x. (x, a) \<in> r})"
+    using assms acyclic_def assms irrefl_def by fastforce
+qed
+
 text \<open>The next lemma is a variation of \<open>wf_eq_minimal\<close> from Wellfounded,
   allowing one to assume the set included in the field.\<close>
 
diff -r cdc1e59aa513 -r 354808e9f44b src/HOL/Probability/Helly_Selection.thy
--- a/src/HOL/Probability/Helly_Selection.thy	Mon Sep 26 07:56:54 2016 +0200
+++ b/src/HOL/Probability/Helly_Selection.thy	Wed Sep 28 17:01:01 2016 +0100
@@ -108,7 +108,7 @@
   moreover have "(\<lambda>n. f (d n) x) \<longlonglongrightarrow> F x" if cts: "continuous (at x) F" for x
   proof (rule limsup_le_liminf_real)
     show "limsup (\<lambda>n. f (d n) x) \<le> F x"
-    proof (rule tendsto_le_const)
+    proof (rule tendsto_lowerbound)
       show "(F \<longlongrightarrow> ereal (F x)) (at_right x)"
         using cts unfolding continuous_at_split by (auto simp: continuous_within)
       show "\<forall>\<^sub>F i in at_right x. limsup (\<lambda>n. f (d n) x) \<le> F i"
@@ -128,7 +128,7 @@
       qed
     qed simp
     show "F x \<le> liminf (\<lambda>n. f (d n) x)"
-    proof (rule tendsto_ge_const)
+    proof (rule tendsto_upperbound)
       show "(F \<longlongrightarrow> ereal (F x)) (at_left x)"
         using cts unfolding continuous_at_split by (auto simp: continuous_within)
       show "\<forall>\<^sub>F i in at_left x. F i \<le> liminf (\<lambda>n. f (d n) x)"
@@ -214,7 +214,7 @@
     have "(\<lambda>k. ?\<mu> k {..b}) \<longlonglongrightarrow> F b"
       using b(2) lim_F unfolding f_def cdf_def o_def by auto
     then have "1 - \<epsilon> \<le> F b"
-    proof (rule tendsto_le_const[OF sequentially_bot], intro always_eventually allI)
+    proof (rule tendsto_lowerbound, intro always_eventually allI)
       fix k
       have "1 - \<epsilon> < ?\<mu> k {a<..b}"
         using ab by auto
@@ -222,20 +222,20 @@
         by (auto intro!: \<mu>.finite_measure_mono)
       finally show "1 - \<epsilon> \<le> ?\<mu> k {..b}"
         by (rule less_imp_le)
-    qed
+    qed (rule sequentially_bot)
     then show "\<exists>b. \<forall>x\<ge>b. 1 - \<epsilon> \<le> F x"
       using F unfolding mono_def by (metis order.trans)
 
     have "(\<lambda>k. ?\<mu> k {..a}) \<longlonglongrightarrow> F a"
       using a(2) lim_F unfolding f_def cdf_def o_def by auto
     then have Fa: "F a \<le> \<epsilon>"
-    proof (rule tendsto_ge_const[OF sequentially_bot], intro always_eventually allI)
+    proof (rule tendsto_upperbound, intro always_eventually allI)
       fix k
       have "?\<mu> k {..a} + ?\<mu> k {a<..b} \<le> 1"
         by (subst \<mu>.finite_measure_Union[symmetric]) auto
       then show "?\<mu> k {..a} \<le> \<epsilon>"
         using ab[of k] by simp
-    qed
+    qed (rule sequentially_bot)
     then show "\<exists>a. \<forall>x\<le>a. F x \<le> \<epsilon>"
       using F unfolding mono_def by (metis order.trans)
   qed
diff -r cdc1e59aa513 -r 354808e9f44b src/HOL/Probability/Weak_Convergence.thy
--- a/src/HOL/Probability/Weak_Convergence.thy	Mon Sep 26 07:56:54 2016 +0200
+++ b/src/HOL/Probability/Weak_Convergence.thy	Wed Sep 28 17:01:01 2016 +0100
@@ -200,7 +200,7 @@
       using \<omega>(2) by (auto intro: tendsto_within_subset simp: continuous_at)
     show "limsup (\<lambda>n. \<mu>.I n \<omega>) \<le> M.I \<omega>"
       using \<omega>
-      by (intro tendsto_le_const[OF trivial_limit_at_right_real **])
+      by (intro tendsto_lowerbound[OF **])
          (auto intro!: exI[of _ 1] * simp: eventually_at_right[of _ 1])
   qed
 
@@ -391,12 +391,12 @@
   } note ** = this
 
   have "limsup (\<lambda>n. cdf (M_seq n) x) \<le> cdf M x"
-  proof (rule tendsto_le_const)
+  proof (rule tendsto_lowerbound)
     show "\<forall>\<^sub>F i in at_right x. limsup (\<lambda>xa. ereal (cdf (M_seq xa) x)) \<le> ereal (cdf M i)"
       by (subst eventually_at_right[of _ "x + 1"]) (auto simp: * intro: exI [of _ "x+1"])
   qed (insert cdf_is_right_cont, auto simp: continuous_within)
   moreover have "cdf M x \<le> liminf (\<lambda>n. cdf (M_seq n) x)"
-  proof (rule tendsto_ge_const)
+  proof (rule tendsto_upperbound)
     show "\<forall>\<^sub>F i in at_left x. ereal (cdf M i) \<le> liminf (\<lambda>xa. ereal (cdf (M_seq xa) x))"
       by (subst eventually_at_left[of "x - 1"]) (auto simp: ** intro: exI [of _ "x-1"])
   qed (insert left_cont, auto simp: continuous_within)
diff -r cdc1e59aa513 -r 354808e9f44b src/HOL/Series.thy
--- a/src/HOL/Series.thy	Mon Sep 26 07:56:54 2016 +0200
+++ b/src/HOL/Series.thy	Wed Sep 28 17:01:01 2016 +0100
@@ -26,12 +26,16 @@
     (binder "\<Sum>" 10)
   where "suminf f = (THE s. f sums s)"
 
+text\<open>Variants of the definition\<close>
 lemma sums_def': "f sums s \<longleftrightarrow> (\<lambda>n. \<Sum>i = 0..n. f i) \<longlonglongrightarrow> s"
   apply (simp add: sums_def)
   apply (subst LIMSEQ_Suc_iff [symmetric])
   apply (simp only: lessThan_Suc_atMost atLeast0AtMost)
   done
 
+lemma sums_def_le: "f sums s \<longleftrightarrow> (\<lambda>n. \<Sum>i\<le>n. f i) \<longlonglongrightarrow> s"
+  by (simp add: sums_def' atMost_atLeast0)
+
 
 subsection \<open>Infinite summability on topological monoids\<close>
 
diff -r cdc1e59aa513 -r 354808e9f44b src/HOL/Set.thy
--- a/src/HOL/Set.thy	Mon Sep 26 07:56:54 2016 +0200
+++ b/src/HOL/Set.thy	Wed Sep 28 17:01:01 2016 +0100
@@ -1858,6 +1858,9 @@
 definition disjnt :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
   where "disjnt A B \<longleftrightarrow> A \<inter> B = {}"
 
+lemma disjnt_self_iff_empty [simp]: "disjnt S S \<longleftrightarrow> S = {}"
+  by (auto simp: disjnt_def)
+
 lemma disjnt_iff: "disjnt A B \<longleftrightarrow> (\<forall>x. \<not> (x \<in> A \<and> x \<in> B))"
   by (force simp: disjnt_def)
 
diff -r cdc1e59aa513 -r 354808e9f44b src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Mon Sep 26 07:56:54 2016 +0200
+++ b/src/HOL/Topological_Spaces.thy	Wed Sep 28 17:01:01 2016 +0100
@@ -884,19 +884,19 @@
     by (simp add: eventually_False)
 qed
 
-lemma tendsto_le_const:
+lemma tendsto_lowerbound:
   fixes f :: "'a \<Rightarrow> 'b::linorder_topology"
-  assumes F: "\<not> trivial_limit F"
-    and x: "(f \<longlongrightarrow> x) F"
-    and ev: "eventually (\<lambda>i. a \<le> f i) F"
+  assumes x: "(f \<longlongrightarrow> x) F"
+      and ev: "eventually (\<lambda>i. a \<le> f i) F"
+      and F: "\<not> trivial_limit F"
   shows "a \<le> x"
   using F x tendsto_const ev by (rule tendsto_le)
 
-lemma tendsto_ge_const:
+lemma tendsto_upperbound:
   fixes f :: "'a \<Rightarrow> 'b::linorder_topology"
-  assumes F: "\<not> trivial_limit F"
-    and x: "(f \<longlongrightarrow> x) F"
-    and ev: "eventually (\<lambda>i. a \<ge> f i) F"
+  assumes x: "(f \<longlongrightarrow> x) F"
+      and ev: "eventually (\<lambda>i. a \<ge> f i) F"
+      and F: "\<not> trivial_limit F"
   shows "a \<ge> x"
   by (rule tendsto_le [OF F tendsto_const x ev])
 
@@ -1256,7 +1256,7 @@
 
 lemma LIMSEQ_le_const: "X \<longlonglongrightarrow> x \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. a \<le> X n \<Longrightarrow> a \<le> x"
   for a x :: "'a::linorder_topology"
-  using tendsto_le_const[of sequentially X x a] by (simp add: eventually_sequentially)
+  by (simp add: eventually_at_top_linorder tendsto_lowerbound)
 
 lemma LIMSEQ_le: "X \<longlonglongrightarrow> x \<Longrightarrow> Y \<longlonglongrightarrow> y \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. X n \<le> Y n \<Longrightarrow> x \<le> y"
   for x y :: "'a::linorder_topology"