Replaced subseq with strict_mono
authoreberlm <eberlm@in.tum.de>
Thu Aug 17 14:52:56 2017 +0200 (21 months ago)
changeset 66447a1f5c5c26fa6
parent 66445 407de0768126
child 66448 97ad7a583457
Replaced subseq with strict_mono
src/HOL/Analysis/Bochner_Integration.thy
src/HOL/Analysis/Bounded_Linear_Function.thy
src/HOL/Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Analysis/Complex_Transcendental.thy
src/HOL/Analysis/Gamma_Function.thy
src/HOL/Analysis/Great_Picard.thy
src/HOL/Analysis/Harmonic_Numbers.thy
src/HOL/Analysis/Linear_Algebra.thy
src/HOL/Analysis/Path_Connected.thy
src/HOL/Analysis/Set_Integral.thy
src/HOL/Analysis/Summation_Tests.thy
src/HOL/Analysis/Topology_Euclidean_Space.thy
src/HOL/Computational_Algebra/Fundamental_Theorem_Algebra.thy
src/HOL/Library/Diagonal_Subsequence.thy
src/HOL/Library/Liminf_Limsup.thy
src/HOL/Limits.thy
src/HOL/Probability/Helly_Selection.thy
src/HOL/Probability/Levy.thy
src/HOL/Probability/Projective_Limit.thy
src/HOL/Series.thy
src/HOL/Topological_Spaces.thy
     1.1 --- a/src/HOL/Analysis/Bochner_Integration.thy	Thu Aug 17 14:40:42 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Bochner_Integration.thy	Thu Aug 17 14:52:56 2017 +0200
     1.3 @@ -2128,7 +2128,7 @@
     1.4    fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::{banach, second_countable_topology}"
     1.5    assumes [measurable]: "\<And>n. integrable M (u n)"
     1.6        and "(\<lambda>n. (\<integral>x. norm(u n x) \<partial>M)) \<longlonglongrightarrow> 0"
     1.7 -  shows "\<exists>r. subseq r \<and> (AE x in M. (\<lambda>n. u (r n) x) \<longlonglongrightarrow> 0)"
     1.8 +  shows "\<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (AE x in M. (\<lambda>n. u (r n) x) \<longlonglongrightarrow> 0)"
     1.9  proof -
    1.10    {
    1.11      fix k
    1.12 @@ -2140,13 +2140,13 @@
    1.13    }
    1.14    then have "\<exists>r. \<forall>n. True \<and> (r (Suc n) > r n \<and> (\<integral>x. norm(u (r (Suc n)) x) \<partial>M) < (1/2)^(r n))"
    1.15      by (intro dependent_nat_choice, auto)
    1.16 -  then obtain r0 where r0: "subseq r0" "\<And>n. (\<integral>x. norm(u (r0 (Suc n)) x) \<partial>M) < (1/2)^(r0 n)"
    1.17 -    by (auto simp: subseq_Suc_iff)
    1.18 +  then obtain r0 where r0: "strict_mono r0" "\<And>n. (\<integral>x. norm(u (r0 (Suc n)) x) \<partial>M) < (1/2)^(r0 n)"
    1.19 +    by (auto simp: strict_mono_Suc_iff)
    1.20    define r where "r = (\<lambda>n. r0(n+1))"
    1.21 -  have "subseq r" unfolding r_def using r0(1) by (simp add: subseq_Suc_iff)
    1.22 +  have "strict_mono r" unfolding r_def using r0(1) by (simp add: strict_mono_Suc_iff)
    1.23    have I: "(\<integral>\<^sup>+x. norm(u (r n) x) \<partial>M) < ennreal((1/2)^n)" for n
    1.24    proof -
    1.25 -    have "r0 n \<ge> n" using \<open>subseq r0\<close> by (simp add: seq_suble)
    1.26 +    have "r0 n \<ge> n" using \<open>strict_mono r0\<close> by (simp add: seq_suble)
    1.27      have "(1/2::real)^(r0 n) \<le> (1/2)^n" by (rule power_decreasing[OF \<open>r0 n \<ge> n\<close>], auto)
    1.28      then have "(\<integral>x. norm(u (r0 (Suc n)) x) \<partial>M) < (1/2)^n" using r0(2) less_le_trans by auto
    1.29      then have "(\<integral>x. norm(u (r n) x) \<partial>M) < (1/2)^n" unfolding r_def by auto
    1.30 @@ -2219,7 +2219,7 @@
    1.31        by (simp add: tendsto_norm_zero_iff)
    1.32    }
    1.33    ultimately have "AE x in M. (\<lambda>n. u (r n) x) \<longlonglongrightarrow> 0" by auto
    1.34 -  then show ?thesis using \<open>subseq r\<close> by auto
    1.35 +  then show ?thesis using \<open>strict_mono r\<close> by auto
    1.36  qed
    1.37  
    1.38  subsection \<open>Restricted measure spaces\<close>
     2.1 --- a/src/HOL/Analysis/Bounded_Linear_Function.thy	Thu Aug 17 14:40:42 2017 +0200
     2.2 +++ b/src/HOL/Analysis/Bounded_Linear_Function.thy	Thu Aug 17 14:52:56 2017 +0200
     2.3 @@ -476,8 +476,8 @@
     2.4  lemma compact_blinfun_lemma:
     2.5    fixes f :: "nat \<Rightarrow> 'a::euclidean_space \<Rightarrow>\<^sub>L 'b::euclidean_space"
     2.6    assumes "bounded (range f)"
     2.7 -  shows "\<forall>d\<subseteq>Basis. \<exists>l::'a \<Rightarrow>\<^sub>L 'b. \<exists> r.
     2.8 -    subseq r \<and> (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) i) (l i) < e) sequentially)"
     2.9 +  shows "\<forall>d\<subseteq>Basis. \<exists>l::'a \<Rightarrow>\<^sub>L 'b. \<exists> r::nat\<Rightarrow>nat.
    2.10 +    strict_mono r \<and> (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) i) (l i) < e) sequentially)"
    2.11    by (rule compact_lemma_general[where unproj = "\<lambda>e. blinfun_of_matrix (\<lambda>i j. e j \<bullet> i)"])
    2.12     (auto intro!: euclidean_eqI[where 'a='b] bounded_linear_image assms
    2.13      simp: blinfun_of_matrix_works blinfun_of_matrix_apply inner_Basis mult_if_delta sum.delta'
    2.14 @@ -501,7 +501,7 @@
    2.15  proof
    2.16    fix f :: "nat \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
    2.17    assume f: "bounded (range f)"
    2.18 -  then obtain l::"'a \<Rightarrow>\<^sub>L 'b" and r where r: "subseq r"
    2.19 +  then obtain l::"'a \<Rightarrow>\<^sub>L 'b" and r where r: "strict_mono r"
    2.20      and l: "\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>Basis. dist (f (r n) i) (l i) < e) sequentially"
    2.21      using compact_blinfun_lemma [OF f] by blast
    2.22    {
    2.23 @@ -545,7 +545,7 @@
    2.24    }
    2.25    then have *: "((f \<circ> r) \<longlongrightarrow> l) sequentially"
    2.26      unfolding o_def tendsto_iff by simp
    2.27 -  with r show "\<exists>l r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
    2.28 +  with r show "\<exists>l r. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
    2.29      by auto
    2.30  qed
    2.31  
     3.1 --- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Thu Aug 17 14:40:42 2017 +0200
     3.2 +++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Thu Aug 17 14:52:56 2017 +0200
     3.3 @@ -957,7 +957,7 @@
     3.4  lemma compact_lemma_cart:
     3.5    fixes f :: "nat \<Rightarrow> 'a::heine_borel ^ 'n"
     3.6    assumes f: "bounded (range f)"
     3.7 -  shows "\<exists>l r. subseq r \<and>
     3.8 +  shows "\<exists>l r. strict_mono r \<and>
     3.9          (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) $ i) (l $ i) < e) sequentially)"
    3.10      (is "?th d")
    3.11  proof -
    3.12 @@ -971,7 +971,7 @@
    3.13  proof
    3.14    fix f :: "nat \<Rightarrow> 'a ^ 'b"
    3.15    assume f: "bounded (range f)"
    3.16 -  then obtain l r where r: "subseq r"
    3.17 +  then obtain l r where r: "strict_mono r"
    3.18        and l: "\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>UNIV. dist (f (r n) $ i) (l $ i) < e) sequentially"
    3.19      using compact_lemma_cart [OF f] by blast
    3.20    let ?d = "UNIV::'b set"
    3.21 @@ -993,7 +993,7 @@
    3.22        by (rule eventually_mono)
    3.23    }
    3.24    hence "((f \<circ> r) \<longlongrightarrow> l) sequentially" unfolding o_def tendsto_iff by simp
    3.25 -  with r show "\<exists>l r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially" by auto
    3.26 +  with r show "\<exists>l r. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially" by auto
    3.27  qed
    3.28  
    3.29  lemma interval_cart:
     4.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Thu Aug 17 14:40:42 2017 +0200
     4.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Thu Aug 17 14:52:56 2017 +0200
     4.3 @@ -2420,7 +2420,7 @@
     4.4                 intro!: mult_pos_pos divide_pos_pos always_eventually)
     4.5      thus "summable (\<lambda>n. g n * u^n)"
     4.6        by (subst summable_mono_reindex[of "\<lambda>n. 2*n+1", symmetric])
     4.7 -         (auto simp: power_mult subseq_def g_def h_def elim!: oddE)
     4.8 +         (auto simp: power_mult strict_mono_def g_def h_def elim!: oddE)
     4.9    qed (simp add: h_def)
    4.10  
    4.11    have "\<exists>c. \<forall>u\<in>ball 0 1. Arctan u - G u = c"
    4.12 @@ -2436,7 +2436,7 @@
    4.13        by (intro ext) (simp_all del: of_nat_Suc add: g_def diffs_def power_mult_distrib)
    4.14      also have "suminf \<dots> = (\<Sum>n. (-(u^2))^n)"
    4.15        by (subst suminf_mono_reindex[of "\<lambda>n. 2*n", symmetric])
    4.16 -         (auto elim!: evenE simp: subseq_def power_mult power_mult_distrib)
    4.17 +         (auto elim!: evenE simp: strict_mono_def power_mult power_mult_distrib)
    4.18      also from u have "norm u^2 < 1^2" by (intro power_strict_mono) simp_all
    4.19      hence "(\<Sum>n. (-(u^2))^n) = inverse (1 + u^2)"
    4.20        by (subst suminf_geometric) (simp_all add: norm_power inverse_eq_divide)
    4.21 @@ -2450,7 +2450,7 @@
    4.22    with c z have "Arctan z = G z" by simp
    4.23    with summable[OF z] show "(\<lambda>n. g n * z^n) sums Arctan z" unfolding G_def by (simp add: sums_iff)
    4.24    thus "h z sums Arctan z" by (subst (asm) sums_mono_reindex[of "\<lambda>n. 2*n+1", symmetric])
    4.25 -                              (auto elim!: oddE simp: subseq_def power_mult g_def h_def)
    4.26 +                              (auto elim!: oddE simp: strict_mono_def power_mult g_def h_def)
    4.27  qed
    4.28  
    4.29  text \<open>A quickly-converging series for the logarithm, based on the arctangent.\<close>
     5.1 --- a/src/HOL/Analysis/Gamma_Function.thy	Thu Aug 17 14:40:42 2017 +0200
     5.2 +++ b/src/HOL/Analysis/Gamma_Function.thy	Thu Aug 17 14:52:56 2017 +0200
     5.3 @@ -101,7 +101,7 @@
     5.4    also have "(\<lambda>n. sin_coeff n *\<^sub>R z^n) sums sin z \<longleftrightarrow>
     5.5                   (\<lambda>n. ((-1)^n / fact (2*n+1)) *\<^sub>R z^(2*n+1)) sums sin z"
     5.6      by (subst sums_mono_reindex[of "\<lambda>n. 2*n+1", symmetric])
     5.7 -       (auto simp: sin_coeff_def subseq_def ac_simps elim!: oddE)
     5.8 +       (auto simp: sin_coeff_def strict_mono_def ac_simps elim!: oddE)
     5.9    finally show ?thesis .
    5.10  qed
    5.11  
    5.12 @@ -111,7 +111,7 @@
    5.13    also have "(\<lambda>n. cos_coeff n *\<^sub>R z^n) sums cos z \<longleftrightarrow>
    5.14                   (\<lambda>n. ((-1)^n / fact (2*n)) *\<^sub>R z^(2*n)) sums cos z"
    5.15      by (subst sums_mono_reindex[of "\<lambda>n. 2*n", symmetric])
    5.16 -       (auto simp: cos_coeff_def subseq_def ac_simps elim!: evenE)
    5.17 +       (auto simp: cos_coeff_def strict_mono_def ac_simps elim!: evenE)
    5.18    finally show ?thesis .
    5.19  qed
    5.20  
    5.21 @@ -2038,7 +2038,7 @@
    5.22      hence "?g \<longlonglongrightarrow> ?powr 2 (2*z) * Gamma z * Gamma (z+1/2) / Gamma (2*z)"
    5.23        using LIMSEQ_subseq_LIMSEQ[OF Gamma_series'_LIMSEQ, of "op*2" "2*z"]
    5.24        by (intro tendsto_intros Gamma_series'_LIMSEQ)
    5.25 -         (simp_all add: o_def subseq_def Gamma_eq_zero_iff)
    5.26 +         (simp_all add: o_def strict_mono_def Gamma_eq_zero_iff)
    5.27      ultimately have "?h \<longlonglongrightarrow> ?powr 2 (2*z) * Gamma z * Gamma (z+1/2) / Gamma (2*z)"
    5.28        by (rule Lim_transform_eventually)
    5.29    } note lim = this
     6.1 --- a/src/HOL/Analysis/Great_Picard.thy	Thu Aug 17 14:40:42 2017 +0200
     6.2 +++ b/src/HOL/Analysis/Great_Picard.thy	Thu Aug 17 14:52:56 2017 +0200
     6.3 @@ -618,22 +618,22 @@
     6.4  
     6.5  lemma subsequence_diagonalization_lemma:
     6.6    fixes P :: "nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> bool"
     6.7 -  assumes sub: "\<And>i r. \<exists>k. subseq k \<and> P i (r \<circ> k)"
     6.8 +  assumes sub: "\<And>i r. \<exists>k. strict_mono (k :: nat \<Rightarrow> nat) \<and> P i (r \<circ> k)"
     6.9        and P_P:  "\<And>i r::nat \<Rightarrow> 'a. \<And>k1 k2 N.
    6.10                     \<lbrakk>P i (r \<circ> k1); \<And>j. N \<le> j \<Longrightarrow> \<exists>j'. j \<le> j' \<and> k2 j = k1 j'\<rbrakk> \<Longrightarrow> P i (r \<circ> k2)"
    6.11 -   obtains k where "subseq k" "\<And>i. P i (r \<circ> k)"
    6.12 +   obtains k where "strict_mono (k :: nat \<Rightarrow> nat)" "\<And>i. P i (r \<circ> k)"
    6.13  proof -
    6.14 -  obtain kk where "\<And>i r. subseq (kk i r) \<and> P i (r \<circ> (kk i r))"
    6.15 +  obtain kk where "\<And>i r. strict_mono (kk i r :: nat \<Rightarrow> nat) \<and> P i (r \<circ> (kk i r))"
    6.16      using sub by metis
    6.17 -  then have sub_kk: "\<And>i r. subseq (kk i r)" and P_kk: "\<And>i r. P i (r \<circ> (kk i r))"
    6.18 +  then have sub_kk: "\<And>i r. strict_mono (kk i r)" and P_kk: "\<And>i r. P i (r \<circ> (kk i r))"
    6.19      by auto
    6.20    define rr where "rr \<equiv> rec_nat (kk 0 r) (\<lambda>n x. x \<circ> kk (Suc n) (r \<circ> x))"
    6.21    then have [simp]: "rr 0 = kk 0 r" "\<And>n. rr(Suc n) = rr n \<circ> kk (Suc n) (r \<circ> rr n)"
    6.22      by auto
    6.23    show thesis
    6.24    proof
    6.25 -    have sub_rr: "subseq (rr i)" for i
    6.26 -      using sub_kk  by (induction i) (auto simp: subseq_def o_def)
    6.27 +    have sub_rr: "strict_mono (rr i)" for i
    6.28 +      using sub_kk  by (induction i) (auto simp: strict_mono_def o_def)
    6.29      have P_rr: "P i (r \<circ> rr i)" for i
    6.30        using P_kk  by (induction i) (auto simp: o_def)
    6.31      have "i \<le> i+d \<Longrightarrow> rr i n \<le> rr (i+d) n" for d i n
    6.32 @@ -643,13 +643,13 @@
    6.33      next
    6.34        case (Suc d) then show ?case
    6.35          apply simp
    6.36 -          using seq_suble [OF sub_kk] order_trans subseq_le_mono [OF sub_rr] by blast
    6.37 +          using seq_suble [OF sub_kk] order_trans strict_mono_less_eq [OF sub_rr] by blast
    6.38      qed
    6.39      then have "\<And>i j n. i \<le> j \<Longrightarrow> rr i n \<le> rr j n"
    6.40        by (metis le_iff_add)
    6.41 -    show "subseq (\<lambda>n. rr n n)"
    6.42 -      apply (simp add: subseq_Suc_iff)
    6.43 -      by (meson Suc_le_eq seq_suble sub_kk sub_rr subseq_mono)
    6.44 +    show "strict_mono (\<lambda>n. rr n n)"
    6.45 +      apply (simp add: strict_mono_Suc_iff)
    6.46 +      by (meson lessI less_le_trans seq_suble strict_monoD sub_kk sub_rr)
    6.47      have "\<exists>j. i \<le> j \<and> rr (n+d) i = rr n j" for d n i
    6.48        apply (induction d arbitrary: i, auto)
    6.49        by (meson order_trans seq_suble sub_kk)
    6.50 @@ -663,19 +663,19 @@
    6.51  lemma function_convergent_subsequence:
    6.52    fixes f :: "[nat,'a] \<Rightarrow> 'b::{real_normed_vector,heine_borel}"
    6.53    assumes "countable S" and M: "\<And>n::nat. \<And>x. x \<in> S \<Longrightarrow> norm(f n x) \<le> M"
    6.54 -   obtains k where "subseq k" "\<And>x. x \<in> S \<Longrightarrow> \<exists>l. (\<lambda>n. f (k n) x) \<longlonglongrightarrow> l"
    6.55 +   obtains k where "strict_mono (k::nat\<Rightarrow>nat)" "\<And>x. x \<in> S \<Longrightarrow> \<exists>l. (\<lambda>n. f (k n) x) \<longlonglongrightarrow> l"
    6.56  proof (cases "S = {}")
    6.57    case True
    6.58    then show ?thesis
    6.59 -    using subseq_id that by fastforce
    6.60 +    using strict_mono_id that by fastforce
    6.61  next
    6.62    case False
    6.63    with \<open>countable S\<close> obtain \<sigma> :: "nat \<Rightarrow> 'a" where \<sigma>: "S = range \<sigma>"
    6.64      using uncountable_def by blast
    6.65 -  obtain k where "subseq k" and k: "\<And>i. \<exists>l. (\<lambda>n. (f \<circ> k) n (\<sigma> i)) \<longlonglongrightarrow> l"
    6.66 +  obtain k where "strict_mono k" and k: "\<And>i. \<exists>l. (\<lambda>n. (f \<circ> k) n (\<sigma> i)) \<longlonglongrightarrow> l"
    6.67    proof (rule subsequence_diagonalization_lemma
    6.68        [of "\<lambda>i r. \<exists>l. ((\<lambda>n. (f \<circ> r) n (\<sigma> i)) \<longlongrightarrow> l) sequentially" id])
    6.69 -    show "\<exists>k. subseq k \<and> (\<exists>l. (\<lambda>n. (f \<circ> (r \<circ> k)) n (\<sigma> i)) \<longlonglongrightarrow> l)" for i r
    6.70 +    show "\<exists>k::nat\<Rightarrow>nat. strict_mono k \<and> (\<exists>l. (\<lambda>n. (f \<circ> (r \<circ> k)) n (\<sigma> i)) \<longlonglongrightarrow> l)" for i r
    6.71      proof -
    6.72        have "f (r n) (\<sigma> i) \<in> cball 0 M" for n
    6.73          by (simp add: \<sigma> M)
    6.74 @@ -705,7 +705,7 @@
    6.75        and equicont:
    6.76            "\<And>x e. \<lbrakk>x \<in> S; 0 < e\<rbrakk>
    6.77                   \<Longrightarrow> \<exists>d. 0 < d \<and> (\<forall>n y. y \<in> S \<and> norm(x - y) < d \<longrightarrow> norm(\<F> n x - \<F> n y) < e)"
    6.78 -  obtains g k where "continuous_on S g" "subseq k"
    6.79 +  obtains g k where "continuous_on S g" "strict_mono (k :: nat \<Rightarrow> nat)"
    6.80                      "\<And>e. 0 < e \<Longrightarrow> \<exists>N. \<forall>n x. n \<ge> N \<and> x \<in> S \<longrightarrow> norm(\<F>(k n) x - g x) < e"
    6.81  proof -
    6.82    have UEQ: "\<And>e. 0 < e \<Longrightarrow> \<exists>d. 0 < d \<and> (\<forall>n. \<forall>x \<in> S. \<forall>x' \<in> S. dist x' x < d \<longrightarrow> dist (\<F> n x') (\<F> n x) < e)"
    6.83 @@ -727,7 +727,7 @@
    6.84    moreover
    6.85    obtain R where "countable R" "R \<subseteq> S" and SR: "S \<subseteq> closure R"
    6.86      by (metis separable that)
    6.87 -  obtain k where "subseq k" and k: "\<And>x. x \<in> R \<Longrightarrow> \<exists>l. (\<lambda>n. \<F> (k n) x) \<longlonglongrightarrow> l"
    6.88 +  obtain k where "strict_mono k" and k: "\<And>x. x \<in> R \<Longrightarrow> \<exists>l. (\<lambda>n. \<F> (k n) x) \<longlonglongrightarrow> l"
    6.89      apply (rule function_convergent_subsequence [OF \<open>countable R\<close> M])
    6.90      using \<open>R \<subseteq> S\<close> apply force+
    6.91      done
    6.92 @@ -783,7 +783,7 @@
    6.93      apply (simp add: o_def dist_norm)
    6.94      by meson
    6.95    ultimately show thesis
    6.96 -    by (metis that \<open>subseq k\<close>)
    6.97 +    by (metis that \<open>strict_mono k\<close>)
    6.98  qed
    6.99  
   6.100  
   6.101 @@ -802,7 +802,7 @@
   6.102        and bounded: "\<And>K. \<lbrakk>compact K; K \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>B. \<forall>h \<in> \<H>. \<forall> z \<in> K. norm(h z) \<le> B"
   6.103        and rng_f: "range \<F> \<subseteq> \<H>"
   6.104    obtains g r
   6.105 -    where "g holomorphic_on S" "subseq r"
   6.106 +    where "g holomorphic_on S" "strict_mono (r :: nat \<Rightarrow> nat)"
   6.107            "\<And>x. x \<in> S \<Longrightarrow> ((\<lambda>n. \<F> (r n) x) \<longlongrightarrow> g x) sequentially"
   6.108            "\<And>K. \<lbrakk>compact K; K \<subseteq> S\<rbrakk> \<Longrightarrow> uniform_limit K (\<F> \<circ> r) g sequentially"        
   6.109  proof -
   6.110 @@ -813,10 +813,10 @@
   6.111      by (simp add: bounded)
   6.112    then obtain B where B: "\<And>i h z. \<lbrakk>h \<in> \<H>; z \<in> K i\<rbrakk> \<Longrightarrow> norm(h z) \<le> B i"
   6.113      by metis
   6.114 -  have *: "\<exists>r g. subseq r \<and> (\<forall>e > 0. \<exists>N. \<forall>n\<ge>N. \<forall>x \<in> K i. norm((\<F> \<circ> r) n x - g x) < e)"
   6.115 +  have *: "\<exists>r g. strict_mono (r::nat\<Rightarrow>nat) \<and> (\<forall>e > 0. \<exists>N. \<forall>n\<ge>N. \<forall>x \<in> K i. norm((\<F> \<circ> r) n x - g x) < e)"
   6.116          if "\<And>n. \<F> n \<in> \<H>" for \<F> i
   6.117    proof -
   6.118 -    obtain g k where "continuous_on (K i) g" "subseq k"
   6.119 +    obtain g k where "continuous_on (K i) g" "strict_mono (k::nat\<Rightarrow>nat)"
   6.120                      "\<And>e. 0 < e \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. \<forall>x \<in> K i. norm(\<F>(k n) x - g x) < e"
   6.121      proof (rule Arzela_Ascoli [of "K i" "\<F>" "B i"])
   6.122        show "\<exists>d>0. \<forall>n y. y \<in> K i \<and> cmod (z - y) < d \<longrightarrow> cmod (\<F> n z - \<F> n y) < e"
   6.123 @@ -925,13 +925,13 @@
   6.124      then show ?thesis
   6.125        by fastforce
   6.126    qed
   6.127 -  have "\<exists>k g. subseq k \<and> (\<forall>e > 0. \<exists>N. \<forall>n\<ge>N. \<forall>x \<in> K i. norm((\<F> \<circ> r \<circ> k) n x - g x) < e)"
   6.128 +  have "\<exists>k g. strict_mono (k::nat\<Rightarrow>nat) \<and> (\<forall>e > 0. \<exists>N. \<forall>n\<ge>N. \<forall>x \<in> K i. norm((\<F> \<circ> r \<circ> k) n x - g x) < e)"
   6.129           for i r
   6.130      apply (rule *)
   6.131      using rng_f by auto
   6.132 -  then have **: "\<And>i r. \<exists>k. subseq k \<and> (\<exists>g. \<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x \<in> K i. norm((\<F> \<circ> (r \<circ> k)) n x - g x) < e)"
   6.133 +  then have **: "\<And>i r. \<exists>k. strict_mono (k::nat\<Rightarrow>nat) \<and> (\<exists>g. \<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x \<in> K i. norm((\<F> \<circ> (r \<circ> k)) n x - g x) < e)"
   6.134      by (force simp: o_assoc)
   6.135 -  obtain k where "subseq k"
   6.136 +  obtain k :: "nat \<Rightarrow> nat" where "strict_mono k"
   6.137               and "\<And>i. \<exists>g. \<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>K i. cmod ((\<F> \<circ> (id \<circ> k)) n x - g x) < e"
   6.138      apply (rule subsequence_diagonalization_lemma [OF **, of id])
   6.139       apply (erule ex_forward all_forward imp_forward)+
   6.140 @@ -988,7 +988,7 @@
   6.141          with d show ?thesis by blast
   6.142        qed
   6.143      qed
   6.144 -  qed (auto simp: \<open>subseq k\<close>)
   6.145 +  qed (auto simp: \<open>strict_mono k\<close>)
   6.146  qed
   6.147  
   6.148  
   6.149 @@ -1332,7 +1332,7 @@
   6.150          using hol\<G> \<G>not0 \<G>not1 \<G>_le1 by (force simp: W_def)+
   6.151        then obtain e where "e > 0" and e: "ball v e \<subseteq> Z"
   6.152          by (meson open_contains_ball)
   6.153 -      obtain h j where holh: "h holomorphic_on ball v e" and "subseq j"
   6.154 +      obtain h j where holh: "h holomorphic_on ball v e" and "strict_mono j"
   6.155                     and lim:  "\<And>x. x \<in> ball v e \<Longrightarrow> (\<lambda>n. \<G> (j n) x) \<longlonglongrightarrow> h x"
   6.156                     and ulim: "\<And>K. \<lbrakk>compact K; K \<subseteq> ball v e\<rbrakk>
   6.157                                    \<Longrightarrow> uniform_limit K (\<G> \<circ> j) h sequentially"
   6.158 @@ -1347,7 +1347,7 @@
   6.159          show "(\<lambda>n. \<G> (j n) v) \<longlonglongrightarrow> h v"
   6.160            using \<open>e > 0\<close> lim by simp
   6.161          have lt_Fj: "real x \<le> cmod (\<F> (j x) v)" for x
   6.162 -          by (metis of_nat_Suc ltF \<open>subseq j\<close> add.commute less_eq_real_def less_le_trans nat_le_real_less seq_suble)
   6.163 +          by (metis of_nat_Suc ltF \<open>strict_mono j\<close> add.commute less_eq_real_def less_le_trans nat_le_real_less seq_suble)
   6.164          show "(\<lambda>n. \<G> (j n) v) \<longlonglongrightarrow> 0"
   6.165          proof (rule Lim_null_comparison [OF eventually_sequentiallyI seq_harmonic])
   6.166            show "cmod (\<G> (j x) v) \<le> inverse (real x)" if "1 \<le> x" for x
   6.167 @@ -1428,8 +1428,8 @@
   6.168    qed
   6.169    with that show ?thesis by metis
   6.170  qed
   6.171 -    
   6.172 -  
   6.173 +
   6.174 +
   6.175  lemma GPicard4:
   6.176    assumes "0 < k" and holf: "f holomorphic_on (ball 0 k - {0})" 
   6.177        and AE: "\<And>e. \<lbrakk>0 < e; e < k\<rbrakk> \<Longrightarrow> \<exists>d. 0 < d \<and> d < e \<and> (\<forall>z \<in> sphere 0 d. norm(f z) \<le> B)"
   6.178 @@ -1500,7 +1500,8 @@
   6.179    then show ?thesis
   6.180    proof cases
   6.181      case 1
   6.182 -    with infinite_enumerate obtain r where "subseq r" and r: "\<And>n. r n \<in> {n. norm(h n w) \<le> 1}"
   6.183 +    with infinite_enumerate obtain r :: "nat \<Rightarrow> nat" 
   6.184 +      where "strict_mono r" and r: "\<And>n. r n \<in> {n. norm(h n w) \<le> 1}"
   6.185        by blast
   6.186      obtain B where B: "\<And>j z. \<lbrakk>norm z = 1/2; j \<in> range (h \<circ> r)\<rbrakk> \<Longrightarrow> norm(j z) \<le> B"
   6.187      proof (rule GPicard3 [OF _ _ w, where K = "sphere 0 (1/2)"])  
   6.188 @@ -1529,7 +1530,7 @@
   6.189        obtain n where "(1/e - 2) / 2 < real n"
   6.190          using reals_Archimedean2 by blast
   6.191        also have "... \<le> r n"
   6.192 -        using \<open>subseq r\<close> by (simp add: seq_suble)
   6.193 +        using \<open>strict_mono r\<close> by (simp add: seq_suble)
   6.194        finally have "(1/e - 2) / 2 < real (r n)" .
   6.195        with \<open>0 < e\<close> have e: "e > 1 / (2 + 2 * real (r n))"
   6.196          by (simp add: field_simps)
   6.197 @@ -1546,7 +1547,8 @@
   6.198        using \<epsilon> by auto 
   6.199    next
   6.200      case 2
   6.201 -    with infinite_enumerate obtain r where "subseq r" and r: "\<And>n. r n \<in> {n. norm(h n w) \<ge> 1}"
   6.202 +    with infinite_enumerate obtain r :: "nat \<Rightarrow> nat" 
   6.203 +      where "strict_mono r" and r: "\<And>n. r n \<in> {n. norm(h n w) \<ge> 1}"
   6.204        by blast
   6.205      obtain B where B: "\<And>j z. \<lbrakk>norm z = 1/2; j \<in> range (\<lambda>n. inverse \<circ> h (r n))\<rbrakk> \<Longrightarrow> norm(j z) \<le> B"
   6.206      proof (rule GPicard3 [OF _ _ w, where K = "sphere 0 (1/2)"])  
   6.207 @@ -1579,7 +1581,7 @@
   6.208        obtain n where "(1/e - 2) / 2 < real n"
   6.209          using reals_Archimedean2 by blast
   6.210        also have "... \<le> r n"
   6.211 -        using \<open>subseq r\<close> by (simp add: seq_suble)
   6.212 +        using \<open>strict_mono r\<close> by (simp add: seq_suble)
   6.213        finally have "(1/e - 2) / 2 < real (r n)" .
   6.214        with \<open>0 < e\<close> have e: "e > 1 / (2 + 2 * real (r n))"
   6.215          by (simp add: field_simps)
     7.1 --- a/src/HOL/Analysis/Harmonic_Numbers.thy	Thu Aug 17 14:40:42 2017 +0200
     7.2 +++ b/src/HOL/Analysis/Harmonic_Numbers.thy	Thu Aug 17 14:52:56 2017 +0200
     7.3 @@ -215,7 +215,7 @@
     7.4    moreover have "(\<lambda>n. ?em (2*n) - ?em n + ln (2::real))
     7.5                       \<longlonglongrightarrow> euler_mascheroni - euler_mascheroni + ln 2"
     7.6      by (intro tendsto_intros euler_mascheroni_LIMSEQ filterlim_compose[OF euler_mascheroni_LIMSEQ]
     7.7 -              filterlim_subseq) (auto simp: subseq_def)
     7.8 +              filterlim_subseq) (auto simp: strict_mono_def)
     7.9    hence "(\<lambda>n. ?em (2*n) - ?em n + ln (2::real)) \<longlonglongrightarrow> ln 2" by simp
    7.10    ultimately have "(\<lambda>n. (\<Sum>k<2*n. (-1)^k / real_of_nat (Suc k))) \<longlonglongrightarrow> ln 2"
    7.11      by (rule Lim_transform_eventually)
    7.12 @@ -227,7 +227,7 @@
    7.13      by (simp add: summable_sums_iff divide_inverse sums_def)
    7.14    from filterlim_compose[OF this filterlim_subseq[of "op * (2::nat)"]]
    7.15      have "(\<lambda>n. \<Sum>k<2*n. (-1)^k / real_of_nat (Suc k)) \<longlonglongrightarrow> (\<Sum>k. (-1)^k / real_of_nat (Suc k))"
    7.16 -    by (simp add: subseq_def)
    7.17 +    by (simp add: strict_mono_def)
    7.18    ultimately have "(\<Sum>k. (- 1) ^ k / real_of_nat (Suc k)) = ln 2" by (intro LIMSEQ_unique)
    7.19    with A show ?thesis by (simp add: sums_def)
    7.20  qed
     8.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Thu Aug 17 14:40:42 2017 +0200
     8.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Thu Aug 17 14:52:56 2017 +0200
     8.3 @@ -1757,8 +1757,8 @@
     8.4  
     8.5  lemma infinite_enumerate:
     8.6    assumes fS: "infinite S"
     8.7 -  shows "\<exists>r. subseq r \<and> (\<forall>n. r n \<in> S)"
     8.8 -  unfolding subseq_def
     8.9 +  shows "\<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (\<forall>n. r n \<in> S)"
    8.10 +  unfolding strict_mono_def
    8.11    using enumerate_in_set[OF fS] enumerate_mono[of _ _ S] fS by auto
    8.12  
    8.13  lemma approachable_lt_le: "(\<exists>(d::real) > 0. \<forall>x. f x < d \<longrightarrow> P x) \<longleftrightarrow> (\<exists>d>0. \<forall>x. f x \<le> d \<longrightarrow> P x)"
     9.1 --- a/src/HOL/Analysis/Path_Connected.thy	Thu Aug 17 14:40:42 2017 +0200
     9.2 +++ b/src/HOL/Analysis/Path_Connected.thy	Thu Aug 17 14:52:56 2017 +0200
     9.3 @@ -3305,7 +3305,8 @@
     9.4      then have "\<And>n. \<exists>x \<in> S. \<xi> n = f x" by force
     9.5      then obtain z where zs: "\<And>n. z n \<in> S" and fz: "\<And>n. \<xi> n = f (z n)"
     9.6        by metis
     9.7 -    then obtain y K where y: "y \<in> closure S" and "subseq K" and Klim: "(z \<circ> K) \<longlonglongrightarrow> y"
     9.8 +    then obtain y K where y: "y \<in> closure S" and "strict_mono (K :: nat \<Rightarrow> nat)" 
     9.9 +                      and Klim: "(z \<circ> K) \<longlonglongrightarrow> y"
    9.10        using \<open>bounded S\<close>
    9.11        apply (simp add: compact_closure [symmetric] compact_def)
    9.12        apply (drule_tac x=z in spec)
    10.1 --- a/src/HOL/Analysis/Set_Integral.thy	Thu Aug 17 14:40:42 2017 +0200
    10.2 +++ b/src/HOL/Analysis/Set_Integral.thy	Thu Aug 17 14:52:56 2017 +0200
    10.3 @@ -193,22 +193,22 @@
    10.4  
    10.5  lemma limsup_subseq_lim:
    10.6    fixes u::"nat \<Rightarrow> 'a :: {complete_linorder, linorder_topology}"
    10.7 -  shows "\<exists>r. subseq r \<and> (u o r) \<longlonglongrightarrow> limsup u"
    10.8 +  shows "\<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (u o r) \<longlonglongrightarrow> limsup u"
    10.9  proof (cases)
   10.10    assume "\<forall>n. \<exists>p>n. \<forall>m\<ge>p. u m \<le> u p"
   10.11    then have "\<exists>r. \<forall>n. (\<forall>m\<ge>r n. u m \<le> u (r n)) \<and> r n < r (Suc n)"
   10.12      by (intro dependent_nat_choice) (auto simp: conj_commute)
   10.13 -  then obtain r where "subseq r" and mono: "\<And>n m. r n \<le> m \<Longrightarrow> u m \<le> u (r n)"
   10.14 -    by (auto simp: subseq_Suc_iff)
   10.15 +  then obtain r :: "nat \<Rightarrow> nat" where "strict_mono r" and mono: "\<And>n m. r n \<le> m \<Longrightarrow> u m \<le> u (r n)"
   10.16 +    by (auto simp: strict_mono_Suc_iff)
   10.17    define umax where "umax = (\<lambda>n. (SUP m:{n..}. u m))"
   10.18    have "decseq umax" unfolding umax_def by (simp add: SUP_subset_mono antimono_def)
   10.19    then have "umax \<longlonglongrightarrow> limsup u" unfolding umax_def by (metis LIMSEQ_INF limsup_INF_SUP)
   10.20 -  then have *: "(umax o r) \<longlonglongrightarrow> limsup u" by (simp add: LIMSEQ_subseq_LIMSEQ \<open>subseq r\<close>)
   10.21 +  then have *: "(umax o r) \<longlonglongrightarrow> limsup u" by (simp add: LIMSEQ_subseq_LIMSEQ \<open>strict_mono r\<close>)
   10.22    have "\<And>n. umax(r n) = u(r n)" unfolding umax_def using mono
   10.23      by (metis SUP_le_iff antisym atLeast_def mem_Collect_eq order_refl)
   10.24    then have "umax o r = u o r" unfolding o_def by simp
   10.25    then have "(u o r) \<longlonglongrightarrow> limsup u" using * by simp
   10.26 -  then show ?thesis using \<open>subseq r\<close> by blast
   10.27 +  then show ?thesis using \<open>strict_mono r\<close> by blast
   10.28  next
   10.29    assume "\<not> (\<forall>n. \<exists>p>n. (\<forall>m\<ge>p. u m \<le> u p))"
   10.30    then obtain N where N: "\<And>p. p > N \<Longrightarrow> \<exists>m>p. u p < u m" by (force simp: not_le le_less)
   10.31 @@ -262,16 +262,16 @@
   10.32      then show "\<exists>y>N. x < y \<and> (\<forall>i\<in>{N<..y}. u i \<le> u y)" by auto
   10.33    qed (auto)
   10.34    then obtain r where r: "\<forall>n. N < r n \<and> r n < r (Suc n) \<and> (\<forall>i\<in> {N<..r (Suc n)}. u i \<le> u (r (Suc n)))" by auto
   10.35 -  have "subseq r" using r by (auto simp: subseq_Suc_iff)
   10.36 +  have "strict_mono r" using r by (auto simp: strict_mono_Suc_iff)
   10.37    have "incseq (u o r)" unfolding o_def using r by (simp add: incseq_SucI order.strict_implies_order)
   10.38    then have "(u o r) \<longlonglongrightarrow> (SUP n. (u o r) n)" using LIMSEQ_SUP by blast
   10.39    then have "limsup (u o r) = (SUP n. (u o r) n)" by (simp add: lim_imp_Limsup)
   10.40 -  moreover have "limsup (u o r) \<le> limsup u" using \<open>subseq r\<close> by (simp add: limsup_subseq_mono)
   10.41 +  moreover have "limsup (u o r) \<le> limsup u" using \<open>strict_mono r\<close> by (simp add: limsup_subseq_mono)
   10.42    ultimately have "(SUP n. (u o r) n) \<le> limsup u" by simp
   10.43  
   10.44    {
   10.45      fix i assume i: "i \<in> {N<..}"
   10.46 -    obtain n where "i < r (Suc n)" using \<open>subseq r\<close> using Suc_le_eq seq_suble by blast
   10.47 +    obtain n where "i < r (Suc n)" using \<open>strict_mono r\<close> using Suc_le_eq seq_suble by blast
   10.48      then have "i \<in> {N<..r(Suc n)}" using i by simp
   10.49      then have "u i \<le> u (r(Suc n))" using r by simp
   10.50      then have "u i \<le> (SUP n. (u o r) n)" unfolding o_def by (meson SUP_upper2 UNIV_I)
   10.51 @@ -281,27 +281,27 @@
   10.52      by (metis (mono_tags, lifting) INF_lower2 atLeast_Suc_greaterThan atLeast_def eventually_ge_at_top mem_Collect_eq)
   10.53    then have "limsup u = (SUP n. (u o r) n)" using \<open>(SUP n. (u o r) n) \<le> limsup u\<close> by simp
   10.54    then have "(u o r) \<longlonglongrightarrow> limsup u" using \<open>(u o r) \<longlonglongrightarrow> (SUP n. (u o r) n)\<close> by simp
   10.55 -  then show ?thesis using \<open>subseq r\<close> by auto
   10.56 +  then show ?thesis using \<open>strict_mono r\<close> by auto
   10.57  qed
   10.58  
   10.59  lemma liminf_subseq_lim:
   10.60    fixes u::"nat \<Rightarrow> 'a :: {complete_linorder, linorder_topology}"
   10.61 -  shows "\<exists>r. subseq r \<and> (u o r) \<longlonglongrightarrow> liminf u"
   10.62 +  shows "\<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (u o r) \<longlonglongrightarrow> liminf u"
   10.63  proof (cases)
   10.64    assume "\<forall>n. \<exists>p>n. \<forall>m\<ge>p. u m \<ge> u p"
   10.65    then have "\<exists>r. \<forall>n. (\<forall>m\<ge>r n. u m \<ge> u (r n)) \<and> r n < r (Suc n)"
   10.66      by (intro dependent_nat_choice) (auto simp: conj_commute)
   10.67 -  then obtain r where "subseq r" and mono: "\<And>n m. r n \<le> m \<Longrightarrow> u m \<ge> u (r n)"
   10.68 -    by (auto simp: subseq_Suc_iff)
   10.69 +  then obtain r :: "nat \<Rightarrow> nat" where "strict_mono r" and mono: "\<And>n m. r n \<le> m \<Longrightarrow> u m \<ge> u (r n)"
   10.70 +    by (auto simp: strict_mono_Suc_iff)
   10.71    define umin where "umin = (\<lambda>n. (INF m:{n..}. u m))"
   10.72    have "incseq umin" unfolding umin_def by (simp add: INF_superset_mono incseq_def)
   10.73    then have "umin \<longlonglongrightarrow> liminf u" unfolding umin_def by (metis LIMSEQ_SUP liminf_SUP_INF)
   10.74 -  then have *: "(umin o r) \<longlonglongrightarrow> liminf u" by (simp add: LIMSEQ_subseq_LIMSEQ \<open>subseq r\<close>)
   10.75 +  then have *: "(umin o r) \<longlonglongrightarrow> liminf u" by (simp add: LIMSEQ_subseq_LIMSEQ \<open>strict_mono r\<close>)
   10.76    have "\<And>n. umin(r n) = u(r n)" unfolding umin_def using mono
   10.77      by (metis le_INF_iff antisym atLeast_def mem_Collect_eq order_refl)
   10.78    then have "umin o r = u o r" unfolding o_def by simp
   10.79    then have "(u o r) \<longlonglongrightarrow> liminf u" using * by simp
   10.80 -  then show ?thesis using \<open>subseq r\<close> by blast
   10.81 +  then show ?thesis using \<open>strict_mono r\<close> by blast
   10.82  next
   10.83    assume "\<not> (\<forall>n. \<exists>p>n. (\<forall>m\<ge>p. u m \<ge> u p))"
   10.84    then obtain N where N: "\<And>p. p > N \<Longrightarrow> \<exists>m>p. u p > u m" by (force simp: not_le le_less)
   10.85 @@ -354,17 +354,18 @@
   10.86      then have "N < y \<and> x < y \<and> (\<forall>i\<in>{N<..y}. u i \<ge> u y)" using \<open>y > x\<close> \<open>y > N\<close> by auto
   10.87      then show "\<exists>y>N. x < y \<and> (\<forall>i\<in>{N<..y}. u i \<ge> u y)" by auto
   10.88    qed (auto)
   10.89 -  then obtain r where r: "\<forall>n. N < r n \<and> r n < r (Suc n) \<and> (\<forall>i\<in> {N<..r (Suc n)}. u i \<ge> u (r (Suc n)))" by auto
   10.90 -  have "subseq r" using r by (auto simp: subseq_Suc_iff)
   10.91 +  then obtain r :: "nat \<Rightarrow> nat" 
   10.92 +    where r: "\<forall>n. N < r n \<and> r n < r (Suc n) \<and> (\<forall>i\<in> {N<..r (Suc n)}. u i \<ge> u (r (Suc n)))" by auto
   10.93 +  have "strict_mono r" using r by (auto simp: strict_mono_Suc_iff)
   10.94    have "decseq (u o r)" unfolding o_def using r by (simp add: decseq_SucI order.strict_implies_order)
   10.95    then have "(u o r) \<longlonglongrightarrow> (INF n. (u o r) n)" using LIMSEQ_INF by blast
   10.96    then have "liminf (u o r) = (INF n. (u o r) n)" by (simp add: lim_imp_Liminf)
   10.97 -  moreover have "liminf (u o r) \<ge> liminf u" using \<open>subseq r\<close> by (simp add: liminf_subseq_mono)
   10.98 +  moreover have "liminf (u o r) \<ge> liminf u" using \<open>strict_mono r\<close> by (simp add: liminf_subseq_mono)
   10.99    ultimately have "(INF n. (u o r) n) \<ge> liminf u" by simp
  10.100  
  10.101    {
  10.102      fix i assume i: "i \<in> {N<..}"
  10.103 -    obtain n where "i < r (Suc n)" using \<open>subseq r\<close> using Suc_le_eq seq_suble by blast
  10.104 +    obtain n where "i < r (Suc n)" using \<open>strict_mono r\<close> using Suc_le_eq seq_suble by blast
  10.105      then have "i \<in> {N<..r(Suc n)}" using i by simp
  10.106      then have "u i \<ge> u (r(Suc n))" using r by simp
  10.107      then have "u i \<ge> (INF n. (u o r) n)" unfolding o_def by (meson INF_lower2 UNIV_I)
  10.108 @@ -374,7 +375,7 @@
  10.109      by (metis (mono_tags, lifting) SUP_upper2 atLeast_Suc_greaterThan atLeast_def eventually_ge_at_top mem_Collect_eq)
  10.110    then have "liminf u = (INF n. (u o r) n)" using \<open>(INF n. (u o r) n) \<ge> liminf u\<close> by simp
  10.111    then have "(u o r) \<longlonglongrightarrow> liminf u" using \<open>(u o r) \<longlonglongrightarrow> (INF n. (u o r) n)\<close> by simp
  10.112 -  then show ?thesis using \<open>subseq r\<close> by auto
  10.113 +  then show ?thesis using \<open>strict_mono r\<close> by auto
  10.114  qed
  10.115  
  10.116  
  10.117 @@ -1076,12 +1077,12 @@
  10.118    then have "limsup u < \<infinity>" "limsup v < \<infinity>" by auto
  10.119  
  10.120    define w where "w = (\<lambda>n. u n + v n)"
  10.121 -  obtain r where r: "subseq r" "(w o r) \<longlonglongrightarrow> limsup w" using limsup_subseq_lim by auto
  10.122 -  obtain s where s: "subseq s" "(u o r o s) \<longlonglongrightarrow> limsup (u o r)" using limsup_subseq_lim by auto
  10.123 -  obtain t where t: "subseq t" "(v o r o s o t) \<longlonglongrightarrow> limsup (v o r o s)" using limsup_subseq_lim by auto
  10.124 +  obtain r where r: "strict_mono r" "(w o r) \<longlonglongrightarrow> limsup w" using limsup_subseq_lim by auto
  10.125 +  obtain s where s: "strict_mono s" "(u o r o s) \<longlonglongrightarrow> limsup (u o r)" using limsup_subseq_lim by auto
  10.126 +  obtain t where t: "strict_mono t" "(v o r o s o t) \<longlonglongrightarrow> limsup (v o r o s)" using limsup_subseq_lim by auto
  10.127  
  10.128    define a where "a = r o s o t"
  10.129 -  have "subseq a" using r s t by (simp add: a_def subseq_o)
  10.130 +  have "strict_mono a" using r s t by (simp add: a_def strict_mono_o)
  10.131    have l:"(w o a) \<longlonglongrightarrow> limsup w"
  10.132           "(u o a) \<longlonglongrightarrow> limsup (u o r)"
  10.133           "(v o a) \<longlonglongrightarrow> limsup (v o r o s)"
  10.134 @@ -1092,7 +1093,8 @@
  10.135  
  10.136    have "limsup (u o r) \<le> limsup u" by (simp add: limsup_subseq_mono r(1))
  10.137    then have a: "limsup (u o r) \<noteq> \<infinity>" using \<open>limsup u < \<infinity>\<close> by auto
  10.138 -  have "limsup (v o r o s) \<le> limsup v" by (simp add: comp_assoc limsup_subseq_mono r(1) s(1) subseq_o)
  10.139 +  have "limsup (v o r o s) \<le> limsup v" 
  10.140 +    by (simp add: comp_assoc limsup_subseq_mono r(1) s(1) strict_mono_o)
  10.141    then have b: "limsup (v o r o s) \<noteq> \<infinity>" using \<open>limsup v < \<infinity>\<close> by auto
  10.142  
  10.143    have "(\<lambda>n. (u o a) n + (v o a) n) \<longlonglongrightarrow> limsup (u o r) + limsup (v o r o s)"
  10.144 @@ -1122,12 +1124,12 @@
  10.145    then have "liminf u > -\<infinity>" "liminf v > -\<infinity>" by auto
  10.146  
  10.147    define w where "w = (\<lambda>n. u n + v n)"
  10.148 -  obtain r where r: "subseq r" "(w o r) \<longlonglongrightarrow> liminf w" using liminf_subseq_lim by auto
  10.149 -  obtain s where s: "subseq s" "(u o r o s) \<longlonglongrightarrow> liminf (u o r)" using liminf_subseq_lim by auto
  10.150 -  obtain t where t: "subseq t" "(v o r o s o t) \<longlonglongrightarrow> liminf (v o r o s)" using liminf_subseq_lim by auto
  10.151 +  obtain r where r: "strict_mono r" "(w o r) \<longlonglongrightarrow> liminf w" using liminf_subseq_lim by auto
  10.152 +  obtain s where s: "strict_mono s" "(u o r o s) \<longlonglongrightarrow> liminf (u o r)" using liminf_subseq_lim by auto
  10.153 +  obtain t where t: "strict_mono t" "(v o r o s o t) \<longlonglongrightarrow> liminf (v o r o s)" using liminf_subseq_lim by auto
  10.154  
  10.155    define a where "a = r o s o t"
  10.156 -  have "subseq a" using r s t by (simp add: a_def subseq_o)
  10.157 +  have "strict_mono a" using r s t by (simp add: a_def strict_mono_o)
  10.158    have l:"(w o a) \<longlonglongrightarrow> liminf w"
  10.159           "(u o a) \<longlonglongrightarrow> liminf (u o r)"
  10.160           "(v o a) \<longlonglongrightarrow> liminf (v o r o s)"
  10.161 @@ -1138,7 +1140,8 @@
  10.162  
  10.163    have "liminf (u o r) \<ge> liminf u" by (simp add: liminf_subseq_mono r(1))
  10.164    then have a: "liminf (u o r) \<noteq> -\<infinity>" using \<open>liminf u > -\<infinity>\<close> by auto
  10.165 -  have "liminf (v o r o s) \<ge> liminf v" by (simp add: comp_assoc liminf_subseq_mono r(1) s(1) subseq_o)
  10.166 +  have "liminf (v o r o s) \<ge> liminf v" 
  10.167 +    by (simp add: comp_assoc liminf_subseq_mono r(1) s(1) strict_mono_o)
  10.168    then have b: "liminf (v o r o s) \<noteq> -\<infinity>" using \<open>liminf v > -\<infinity>\<close> by auto
  10.169  
  10.170    have "(\<lambda>n. (u o a) n + (v o a) n) \<longlonglongrightarrow> liminf (u o r) + liminf (v o r o s)"
  10.171 @@ -1188,7 +1191,7 @@
  10.172    shows "limsup (\<lambda>n. u n * v n) = a * limsup v"
  10.173  proof -
  10.174    define w where "w = (\<lambda>n. u n * v n)"
  10.175 -  obtain r where r: "subseq r" "(v o r) \<longlonglongrightarrow> limsup v" using limsup_subseq_lim by auto
  10.176 +  obtain r where r: "strict_mono r" "(v o r) \<longlonglongrightarrow> limsup v" using limsup_subseq_lim by auto
  10.177    have "(u o r) \<longlonglongrightarrow> a" using assms(1) LIMSEQ_subseq_LIMSEQ r by auto
  10.178    with tendsto_mult_ereal[OF this r(2)] have "(\<lambda>n. (u o r) n * (v o r) n) \<longlonglongrightarrow> a * limsup v" using assms(2) assms(3) by auto
  10.179    moreover have "\<And>n. (w o r) n = (u o r) n * (v o r) n" unfolding w_def by auto
  10.180 @@ -1196,7 +1199,7 @@
  10.181    then have "limsup (w o r) = a * limsup v" by (simp add: tendsto_iff_Liminf_eq_Limsup)
  10.182    then have I: "limsup w \<ge> a * limsup v" by (metis limsup_subseq_mono r(1))
  10.183  
  10.184 -  obtain s where s: "subseq s" "(w o s) \<longlonglongrightarrow> limsup w" using limsup_subseq_lim by auto
  10.185 +  obtain s where s: "strict_mono s" "(w o s) \<longlonglongrightarrow> limsup w" using limsup_subseq_lim by auto
  10.186    have *: "(u o s) \<longlonglongrightarrow> a" using assms(1) LIMSEQ_subseq_LIMSEQ s by auto
  10.187    have "eventually (\<lambda>n. (u o s) n > 0) sequentially" using assms(2) * order_tendsto_iff by blast
  10.188    moreover have "eventually (\<lambda>n. (u o s) n < \<infinity>) sequentially" using assms(3) * order_tendsto_iff by blast
  10.189 @@ -1218,7 +1221,7 @@
  10.190    shows "liminf (\<lambda>n. u n * v n) = a * liminf v"
  10.191  proof -
  10.192    define w where "w = (\<lambda>n. u n * v n)"
  10.193 -  obtain r where r: "subseq r" "(v o r) \<longlonglongrightarrow> liminf v" using liminf_subseq_lim by auto
  10.194 +  obtain r where r: "strict_mono r" "(v o r) \<longlonglongrightarrow> liminf v" using liminf_subseq_lim by auto
  10.195    have "(u o r) \<longlonglongrightarrow> a" using assms(1) LIMSEQ_subseq_LIMSEQ r by auto
  10.196    with tendsto_mult_ereal[OF this r(2)] have "(\<lambda>n. (u o r) n * (v o r) n) \<longlonglongrightarrow> a * liminf v" using assms(2) assms(3) by auto
  10.197    moreover have "\<And>n. (w o r) n = (u o r) n * (v o r) n" unfolding w_def by auto
  10.198 @@ -1226,7 +1229,7 @@
  10.199    then have "liminf (w o r) = a * liminf v" by (simp add: tendsto_iff_Liminf_eq_Limsup)
  10.200    then have I: "liminf w \<le> a * liminf v" by (metis liminf_subseq_mono r(1))
  10.201  
  10.202 -  obtain s where s: "subseq s" "(w o s) \<longlonglongrightarrow> liminf w" using liminf_subseq_lim by auto
  10.203 +  obtain s where s: "strict_mono s" "(w o s) \<longlonglongrightarrow> liminf w" using liminf_subseq_lim by auto
  10.204    have *: "(u o s) \<longlonglongrightarrow> a" using assms(1) LIMSEQ_subseq_LIMSEQ s by auto
  10.205    have "eventually (\<lambda>n. (u o s) n > 0) sequentially" using assms(2) * order_tendsto_iff by blast
  10.206    moreover have "eventually (\<lambda>n. (u o s) n < \<infinity>) sequentially" using assms(3) * order_tendsto_iff by blast
  10.207 @@ -1286,12 +1289,12 @@
  10.208    then have "limsup v < \<infinity>" "liminf u < \<infinity>" by auto
  10.209  
  10.210    define w where "w = (\<lambda>n. u n + v n)"
  10.211 -  obtain r where r: "subseq r" "(u o r) \<longlonglongrightarrow> liminf u" using liminf_subseq_lim by auto
  10.212 -  obtain s where s: "subseq s" "(w o r o s) \<longlonglongrightarrow> liminf (w o r)" using liminf_subseq_lim by auto
  10.213 -  obtain t where t: "subseq t" "(v o r o s o t) \<longlonglongrightarrow> limsup (v o r o s)" using limsup_subseq_lim by auto
  10.214 +  obtain r where r: "strict_mono r" "(u o r) \<longlonglongrightarrow> liminf u" using liminf_subseq_lim by auto
  10.215 +  obtain s where s: "strict_mono s" "(w o r o s) \<longlonglongrightarrow> liminf (w o r)" using liminf_subseq_lim by auto
  10.216 +  obtain t where t: "strict_mono t" "(v o r o s o t) \<longlonglongrightarrow> limsup (v o r o s)" using limsup_subseq_lim by auto
  10.217  
  10.218    define a where "a = r o s o t"
  10.219 -  have "subseq a" using r s t by (simp add: a_def subseq_o)
  10.220 +  have "strict_mono a" using r s t by (simp add: a_def strict_mono_o)
  10.221    have l:"(u o a) \<longlonglongrightarrow> liminf u"
  10.222           "(w o a) \<longlonglongrightarrow> liminf (w o r)"
  10.223           "(v o a) \<longlonglongrightarrow> limsup (v o r o s)"
  10.224 @@ -1301,7 +1304,8 @@
  10.225    done
  10.226  
  10.227    have "liminf (w o r) \<ge> liminf w" by (simp add: liminf_subseq_mono r(1))
  10.228 -  have "limsup (v o r o s) \<le> limsup v" by (simp add: comp_assoc limsup_subseq_mono r(1) s(1) subseq_o)
  10.229 +  have "limsup (v o r o s) \<le> limsup v" 
  10.230 +    by (simp add: comp_assoc limsup_subseq_mono r(1) s(1) strict_mono_o)
  10.231    then have b: "limsup (v o r o s) < \<infinity>" using \<open>limsup v < \<infinity>\<close> by auto
  10.232  
  10.233    have "(\<lambda>n. (u o a) n + (v o a) n) \<longlonglongrightarrow> liminf u + limsup (v o r o s)"
    11.1 --- a/src/HOL/Analysis/Summation_Tests.thy	Thu Aug 17 14:40:42 2017 +0200
    11.2 +++ b/src/HOL/Analysis/Summation_Tests.thy	Thu Aug 17 14:52:56 2017 +0200
    11.3 @@ -189,7 +189,7 @@
    11.4    also have "\<dots> \<longleftrightarrow> Bseq (\<lambda>n. \<Sum>k=1..<n. f k)" unfolding f'_def by simp
    11.5    also have "\<dots> \<longleftrightarrow> Bseq (\<lambda>n. \<Sum>k=1..<2^n. f k)"
    11.6      by (rule nonneg_incseq_Bseq_subseq_iff[symmetric])
    11.7 -       (auto intro!: sum_nonneg incseq_SucI nonneg simp: subseq_def)
    11.8 +       (auto intro!: sum_nonneg incseq_SucI nonneg simp: strict_mono_def)
    11.9    also have "\<dots> \<longleftrightarrow> Bseq (\<lambda>n. \<Sum>k<n. 2^k * f (2^k))"
   11.10    proof (intro iffI)
   11.11      assume A: "Bseq (\<lambda>n. \<Sum>k=1..<2^n. f k)"
    12.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Thu Aug 17 14:40:42 2017 +0200
    12.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Thu Aug 17 14:52:56 2017 +0200
    12.3 @@ -4468,7 +4468,7 @@
    12.4  lemma acc_point_range_imp_convergent_subsequence:
    12.5    fixes l :: "'a :: first_countable_topology"
    12.6    assumes l: "\<forall>U. l\<in>U \<longrightarrow> open U \<longrightarrow> infinite (U \<inter> range f)"
    12.7 -  shows "\<exists>r. subseq r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
    12.8 +  shows "\<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
    12.9  proof -
   12.10    from countable_basis_at_decseq[of l]
   12.11    obtain A where A:
   12.12 @@ -4492,8 +4492,8 @@
   12.13    }
   12.14    note s = this
   12.15    define r where "r = rec_nat (s 0 0) s"
   12.16 -  have "subseq r"
   12.17 -    by (auto simp: r_def s subseq_Suc_iff)
   12.18 +  have "strict_mono r"
   12.19 +    by (auto simp: r_def s strict_mono_Suc_iff)
   12.20    moreover
   12.21    have "(\<lambda>n. f (r n)) \<longlonglongrightarrow> l"
   12.22    proof (rule topological_tendstoI)
   12.23 @@ -4513,7 +4513,7 @@
   12.24      ultimately show "eventually (\<lambda>i. f (r i) \<in> S) sequentially"
   12.25        by eventually_elim auto
   12.26    qed
   12.27 -  ultimately show "\<exists>r. subseq r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
   12.28 +  ultimately show "\<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
   12.29      by (auto simp: convergent_def comp_def)
   12.30  qed
   12.31  
   12.32 @@ -4616,7 +4616,7 @@
   12.33  lemma islimpt_range_imp_convergent_subsequence:
   12.34    fixes l :: "'a :: {t1_space, first_countable_topology}"
   12.35    assumes l: "l islimpt (range f)"
   12.36 -  shows "\<exists>r. subseq r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
   12.37 +  shows "\<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
   12.38    using l unfolding islimpt_eq_acc_point
   12.39    by (rule acc_point_range_imp_convergent_subsequence)
   12.40  
   12.41 @@ -4949,16 +4949,16 @@
   12.42  
   12.43  definition seq_compact :: "'a::topological_space set \<Rightarrow> bool"
   12.44    where "seq_compact S \<longleftrightarrow>
   12.45 -    (\<forall>f. (\<forall>n. f n \<in> S) \<longrightarrow> (\<exists>l\<in>S. \<exists>r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially))"
   12.46 +    (\<forall>f. (\<forall>n. f n \<in> S) \<longrightarrow> (\<exists>l\<in>S. \<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially))"
   12.47  
   12.48  lemma seq_compactI:
   12.49 -  assumes "\<And>f. \<forall>n. f n \<in> S \<Longrightarrow> \<exists>l\<in>S. \<exists>r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
   12.50 +  assumes "\<And>f. \<forall>n. f n \<in> S \<Longrightarrow> \<exists>l\<in>S. \<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
   12.51    shows "seq_compact S"
   12.52    unfolding seq_compact_def using assms by fast
   12.53  
   12.54  lemma seq_compactE:
   12.55    assumes "seq_compact S" "\<forall>n. f n \<in> S"
   12.56 -  obtains l r where "l \<in> S" "subseq r" "((f \<circ> r) \<longlongrightarrow> l) sequentially"
   12.57 +  obtains l r where "l \<in> S" "strict_mono (r :: nat \<Rightarrow> nat)" "((f \<circ> r) \<longlongrightarrow> l) sequentially"
   12.58    using assms unfolding seq_compact_def by fast
   12.59  
   12.60  lemma closed_sequentially: (* TODO: move upwards *)
   12.61 @@ -4980,13 +4980,13 @@
   12.62    hence "\<forall>n. f n \<in> s" and "\<forall>n. f n \<in> t"
   12.63      by simp_all
   12.64    from \<open>seq_compact s\<close> and \<open>\<forall>n. f n \<in> s\<close>
   12.65 -  obtain l r where "l \<in> s" and r: "subseq r" and l: "(f \<circ> r) \<longlonglongrightarrow> l"
   12.66 +  obtain l r where "l \<in> s" and r: "strict_mono r" and l: "(f \<circ> r) \<longlonglongrightarrow> l"
   12.67      by (rule seq_compactE)
   12.68    from \<open>\<forall>n. f n \<in> t\<close> have "\<forall>n. (f \<circ> r) n \<in> t"
   12.69      by simp
   12.70    from \<open>closed t\<close> and this and l have "l \<in> t"
   12.71      by (rule closed_sequentially)
   12.72 -  with \<open>l \<in> s\<close> and r and l show "\<exists>l\<in>s \<inter> t. \<exists>r. subseq r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
   12.73 +  with \<open>l \<in> s\<close> and r and l show "\<exists>l\<in>s \<inter> t. \<exists>r. strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
   12.74      by fast
   12.75  qed
   12.76  
   12.77 @@ -5002,7 +5002,7 @@
   12.78  proof (safe intro!: countably_compactI)
   12.79    fix A
   12.80    assume A: "\<forall>a\<in>A. open a" "U \<subseteq> \<Union>A" "countable A"
   12.81 -  have subseq: "\<And>X. range X \<subseteq> U \<Longrightarrow> \<exists>r x. x \<in> U \<and> subseq r \<and> (X \<circ> r) \<longlonglongrightarrow> x"
   12.82 +  have subseq: "\<And>X. range X \<subseteq> U \<Longrightarrow> \<exists>r x. x \<in> U \<and> strict_mono (r :: nat \<Rightarrow> nat) \<and> (X \<circ> r) \<longlonglongrightarrow> x"
   12.83      using \<open>seq_compact U\<close> by (fastforce simp: seq_compact_def subset_eq)
   12.84    show "\<exists>T\<subseteq>A. finite T \<and> U \<subseteq> \<Union>T"
   12.85    proof cases
   12.86 @@ -5023,7 +5023,7 @@
   12.87          using \<open>A \<noteq> {}\<close> unfolding X_def by (intro T) (auto intro: from_nat_into)
   12.88        then have "range X \<subseteq> U"
   12.89          by auto
   12.90 -      with subseq[of X] obtain r x where "x \<in> U" and r: "subseq r" "(X \<circ> r) \<longlonglongrightarrow> x"
   12.91 +      with subseq[of X] obtain r x where "x \<in> U" and r: "strict_mono r" "(X \<circ> r) \<longlonglongrightarrow> x"
   12.92          by auto
   12.93        from \<open>x\<in>U\<close> \<open>U \<subseteq> \<Union>A\<close> from_nat_into_surj[OF \<open>countable A\<close>]
   12.94        obtain n where "x \<in> from_nat_into A n" by auto
   12.95 @@ -5034,7 +5034,7 @@
   12.96          by (auto simp: eventually_sequentially)
   12.97        moreover from X have "\<And>i. n \<le> r i \<Longrightarrow> X (r i) \<notin> from_nat_into A n"
   12.98          by auto
   12.99 -      moreover from \<open>subseq r\<close>[THEN seq_suble, of "max n N"] have "\<exists>i. n \<le> r i \<and> N \<le> i"
  12.100 +      moreover from \<open>strict_mono r\<close>[THEN seq_suble, of "max n N"] have "\<exists>i. n \<le> r i \<and> N \<le> i"
  12.101          by (auto intro!: exI[of _ "max n N"])
  12.102        ultimately show False
  12.103          by auto
  12.104 @@ -5087,8 +5087,8 @@
  12.105    }
  12.106    note s = this
  12.107    define r where "r = rec_nat (s 0 0) s"
  12.108 -  have "subseq r"
  12.109 -    by (auto simp: r_def s subseq_Suc_iff)
  12.110 +  have "strict_mono r"
  12.111 +    by (auto simp: r_def s strict_mono_Suc_iff)
  12.112    moreover
  12.113    have "(\<lambda>n. X (r n)) \<longlonglongrightarrow> x"
  12.114    proof (rule topological_tendstoI)
  12.115 @@ -5108,7 +5108,7 @@
  12.116      ultimately show "eventually (\<lambda>i. X (r i) \<in> S) sequentially"
  12.117        by eventually_elim auto
  12.118    qed
  12.119 -  ultimately show "\<exists>x \<in> U. \<exists>r. subseq r \<and> (X \<circ> r) \<longlonglongrightarrow> x"
  12.120 +  ultimately show "\<exists>x \<in> U. \<exists>r. strict_mono r \<and> (X \<circ> r) \<longlonglongrightarrow> x"
  12.121      using \<open>x \<in> U\<close> by (auto simp: convergent_def comp_def)
  12.122  qed
  12.123  
  12.124 @@ -5159,25 +5159,25 @@
  12.125    {
  12.126      fix f :: "nat \<Rightarrow> 'a"
  12.127      assume f: "\<forall>n. f n \<in> s"
  12.128 -    have "\<exists>l\<in>s. \<exists>r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
  12.129 +    have "\<exists>l\<in>s. \<exists>r. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
  12.130      proof (cases "finite (range f)")
  12.131        case True
  12.132        obtain l where "infinite {n. f n = f l}"
  12.133          using pigeonhole_infinite[OF _ True] by auto
  12.134 -      then obtain r where "subseq r" and fr: "\<forall>n. f (r n) = f l"
  12.135 +      then obtain r :: "nat \<Rightarrow> nat" where "strict_mono  r" and fr: "\<forall>n. f (r n) = f l"
  12.136          using infinite_enumerate by blast
  12.137 -      then have "subseq r \<and> (f \<circ> r) \<longlonglongrightarrow> f l"
  12.138 +      then have "strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> f l"
  12.139          by (simp add: fr o_def)
  12.140 -      with f show "\<exists>l\<in>s. \<exists>r. subseq r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
  12.141 +      with f show "\<exists>l\<in>s. \<exists>r. strict_mono  r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
  12.142          by auto
  12.143      next
  12.144        case False
  12.145        with f assms have "\<exists>x\<in>s. \<forall>U. x\<in>U \<and> open U \<longrightarrow> infinite (U \<inter> range f)"
  12.146          by auto
  12.147        then obtain l where "l \<in> s" "\<forall>U. l\<in>U \<and> open U \<longrightarrow> infinite (U \<inter> range f)" ..
  12.148 -      from this(2) have "\<exists>r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
  12.149 +      from this(2) have "\<exists>r. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
  12.150          using acc_point_range_imp_convergent_subsequence[of l f] by auto
  12.151 -      with \<open>l \<in> s\<close> show "\<exists>l\<in>s. \<exists>r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially" ..
  12.152 +      with \<open>l \<in> s\<close> show "\<exists>l\<in>s. \<exists>r. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially" ..
  12.153      qed
  12.154    }
  12.155    then show ?thesis
  12.156 @@ -5237,14 +5237,14 @@
  12.157      qed simp
  12.158      then obtain x where "\<forall>n::nat. x n \<in> s" and x:"\<And>n m. m < n \<Longrightarrow> \<not> (dist (x m) (x n) < e)"
  12.159        by blast
  12.160 -    then obtain l r where "l \<in> s" and r:"subseq r" and "((x \<circ> r) \<longlongrightarrow> l) sequentially"
  12.161 +    then obtain l r where "l \<in> s" and r:"strict_mono  r" and "((x \<circ> r) \<longlongrightarrow> l) sequentially"
  12.162        using assms by (metis seq_compact_def)
  12.163      from this(3) have "Cauchy (x \<circ> r)"
  12.164        using LIMSEQ_imp_Cauchy by auto
  12.165      then obtain N::nat where "\<And>m n. N \<le> m \<Longrightarrow> N \<le> n \<Longrightarrow> dist ((x \<circ> r) m) ((x \<circ> r) n) < e"
  12.166        unfolding cauchy_def using \<open>e > 0\<close> by blast
  12.167      then have False
  12.168 -      using x[of "r N" "r (N+1)"] r by (auto simp: subseq_def) }
  12.169 +      using x[of "r N" "r (N+1)"] r by (auto simp: strict_mono_def) }
  12.170    then show ?thesis
  12.171      by metis
  12.172  qed
  12.173 @@ -5302,7 +5302,7 @@
  12.174  
  12.175  lemma compact_def: \<comment>\<open>this is the definition of compactness in HOL Light\<close>
  12.176    "compact (S :: 'a::metric_space set) \<longleftrightarrow>
  12.177 -   (\<forall>f. (\<forall>n. f n \<in> S) \<longrightarrow> (\<exists>l\<in>S. \<exists>r. subseq r \<and> (f \<circ> r) \<longlonglongrightarrow> l))"
  12.178 +   (\<forall>f. (\<forall>n. f n \<in> S) \<longrightarrow> (\<exists>l\<in>S. \<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> l))"
  12.179    unfolding compact_eq_seq_compact_metric seq_compact_def by auto
  12.180  
  12.181  subsubsection \<open>Complete the chain of compactness variants\<close>
  12.182 @@ -5335,7 +5335,7 @@
  12.183  
  12.184  class heine_borel = metric_space +
  12.185    assumes bounded_imp_convergent_subsequence:
  12.186 -    "bounded (range f) \<Longrightarrow> \<exists>l r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
  12.187 +    "bounded (range f) \<Longrightarrow> \<exists>l r. strict_mono (r::nat\<Rightarrow>nat) \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
  12.188  
  12.189  lemma bounded_closed_imp_seq_compact:
  12.190    fixes s::"'a::heine_borel set"
  12.191 @@ -5347,13 +5347,13 @@
  12.192    assume f: "\<forall>n. f n \<in> s"
  12.193    with \<open>bounded s\<close> have "bounded (range f)"
  12.194      by (auto intro: bounded_subset)
  12.195 -  obtain l r where r: "subseq r" and l: "((f \<circ> r) \<longlongrightarrow> l) sequentially"
  12.196 +  obtain l r where r: "strict_mono (r :: nat \<Rightarrow> nat)" and l: "((f \<circ> r) \<longlongrightarrow> l) sequentially"
  12.197      using bounded_imp_convergent_subsequence [OF \<open>bounded (range f)\<close>] by auto
  12.198    from f have fr: "\<forall>n. (f \<circ> r) n \<in> s"
  12.199      by simp
  12.200    have "l \<in> s" using \<open>closed s\<close> fr l
  12.201      by (rule closed_sequentially)
  12.202 -  show "\<exists>l\<in>s. \<exists>r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
  12.203 +  show "\<exists>l\<in>s. \<exists>r. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
  12.204      using \<open>l \<in> s\<close> r l by blast
  12.205  qed
  12.206  
  12.207 @@ -5393,11 +5393,11 @@
  12.208  proof
  12.209    fix f :: "nat \<Rightarrow> real"
  12.210    assume f: "bounded (range f)"
  12.211 -  obtain r where r: "subseq r" "monoseq (f \<circ> r)"
  12.212 +  obtain r :: "nat \<Rightarrow> nat" where r: "strict_mono r" "monoseq (f \<circ> r)"
  12.213      unfolding comp_def by (metis seq_monosub)
  12.214    then have "Bseq (f \<circ> r)"
  12.215      unfolding Bseq_eq_bounded using f by (force intro: bounded_subset)
  12.216 -  with r show "\<exists>l r. subseq r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
  12.217 +  with r show "\<exists>l r. strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
  12.218      using Bseq_monoseq_convergent[of "f \<circ> r"] by (auto simp: convergent_def)
  12.219  qed
  12.220  
  12.221 @@ -5409,19 +5409,19 @@
  12.222    assumes bounded_proj: "\<And>k. k \<in> basis \<Longrightarrow> bounded ((\<lambda>x. x proj k) ` range f)"
  12.223    assumes proj_unproj: "\<And>e k. k \<in> basis \<Longrightarrow> (unproj e) proj k = e k"
  12.224    assumes unproj_proj: "\<And>x. unproj (\<lambda>k. x proj k) = x"
  12.225 -  shows "\<forall>d\<subseteq>basis. \<exists>l::'a. \<exists> r.
  12.226 -    subseq r \<and> (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) proj i) (l proj i) < e) sequentially)"
  12.227 +  shows "\<forall>d\<subseteq>basis. \<exists>l::'a. \<exists> r::nat\<Rightarrow>nat.
  12.228 +    strict_mono r \<and> (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) proj i) (l proj i) < e) sequentially)"
  12.229  proof safe
  12.230    fix d :: "'b set"
  12.231    assume d: "d \<subseteq> basis"
  12.232    with finite_basis have "finite d"
  12.233      by (blast intro: finite_subset)
  12.234 -  from this d show "\<exists>l::'a. \<exists>r. subseq r \<and>
  12.235 +  from this d show "\<exists>l::'a. \<exists>r::nat\<Rightarrow>nat. strict_mono r \<and>
  12.236      (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) proj i) (l proj i) < e) sequentially)"
  12.237    proof (induct d)
  12.238      case empty
  12.239      then show ?case
  12.240 -      unfolding subseq_def by auto
  12.241 +      unfolding strict_mono_def by auto
  12.242    next
  12.243      case (insert k d)
  12.244      have k[intro]: "k \<in> basis"
  12.245 @@ -5429,19 +5429,19 @@
  12.246      have s': "bounded ((\<lambda>x. x proj k) ` range f)"
  12.247        using k
  12.248        by (rule bounded_proj)
  12.249 -    obtain l1::"'a" and r1 where r1: "subseq r1"
  12.250 +    obtain l1::"'a" and r1 where r1: "strict_mono r1"
  12.251        and lr1: "\<forall>e > 0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) proj i) (l1 proj i) < e) sequentially"
  12.252        using insert(3) using insert(4) by auto
  12.253      have f': "\<forall>n. f (r1 n) proj k \<in> (\<lambda>x. x proj k) ` range f"
  12.254        by simp
  12.255      have "bounded (range (\<lambda>i. f (r1 i) proj k))"
  12.256        by (metis (lifting) bounded_subset f' image_subsetI s')
  12.257 -    then obtain l2 r2 where r2:"subseq r2" and lr2:"((\<lambda>i. f (r1 (r2 i)) proj k) \<longlongrightarrow> l2) sequentially"
  12.258 +    then obtain l2 r2 where r2:"strict_mono r2" and lr2:"((\<lambda>i. f (r1 (r2 i)) proj k) \<longlongrightarrow> l2) sequentially"
  12.259        using bounded_imp_convergent_subsequence[of "\<lambda>i. f (r1 i) proj k"]
  12.260        by (auto simp: o_def)
  12.261      define r where "r = r1 \<circ> r2"
  12.262 -    have r:"subseq r"
  12.263 -      using r1 and r2 unfolding r_def o_def subseq_def by auto
  12.264 +    have r:"strict_mono r"
  12.265 +      using r1 and r2 unfolding r_def o_def strict_mono_def by auto
  12.266      moreover
  12.267      define l where "l = unproj (\<lambda>i. if i = k then l2 else l1 proj i)"
  12.268      {
  12.269 @@ -5465,7 +5465,7 @@
  12.270    fixes f :: "nat \<Rightarrow> 'a::euclidean_space"
  12.271    assumes "bounded (range f)"
  12.272    shows "\<forall>d\<subseteq>Basis. \<exists>l::'a. \<exists> r.
  12.273 -    subseq r \<and> (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially)"
  12.274 +    strict_mono r \<and> (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially)"
  12.275    by (rule compact_lemma_general[where unproj="\<lambda>e. \<Sum>i\<in>Basis. e i *\<^sub>R i"])
  12.276       (auto intro!: assms bounded_linear_inner_left bounded_linear_image
  12.277         simp: euclidean_representation)
  12.278 @@ -5474,7 +5474,7 @@
  12.279  proof
  12.280    fix f :: "nat \<Rightarrow> 'a"
  12.281    assume f: "bounded (range f)"
  12.282 -  then obtain l::'a and r where r: "subseq r"
  12.283 +  then obtain l::'a and r where r: "strict_mono r"
  12.284      and l: "\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially"
  12.285      using compact_lemma [OF f] by blast
  12.286    {
  12.287 @@ -5505,7 +5505,7 @@
  12.288    }
  12.289    then have *: "((f \<circ> r) \<longlongrightarrow> l) sequentially"
  12.290      unfolding o_def tendsto_iff by simp
  12.291 -  with r show "\<exists>l r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
  12.292 +  with r show "\<exists>l r. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
  12.293      by auto
  12.294  qed
  12.295  
  12.296 @@ -5525,20 +5525,20 @@
  12.297      by (rule bounded_fst)
  12.298    then have s1: "bounded (range (fst \<circ> f))"
  12.299      by (simp add: image_comp)
  12.300 -  obtain l1 r1 where r1: "subseq r1" and l1: "(\<lambda>n. fst (f (r1 n))) \<longlonglongrightarrow> l1"
  12.301 +  obtain l1 r1 where r1: "strict_mono r1" and l1: "(\<lambda>n. fst (f (r1 n))) \<longlonglongrightarrow> l1"
  12.302      using bounded_imp_convergent_subsequence [OF s1] unfolding o_def by fast
  12.303    from f have s2: "bounded (range (snd \<circ> f \<circ> r1))"
  12.304      by (auto simp add: image_comp intro: bounded_snd bounded_subset)
  12.305 -  obtain l2 r2 where r2: "subseq r2" and l2: "((\<lambda>n. snd (f (r1 (r2 n)))) \<longlongrightarrow> l2) sequentially"
  12.306 +  obtain l2 r2 where r2: "strict_mono r2" and l2: "((\<lambda>n. snd (f (r1 (r2 n)))) \<longlongrightarrow> l2) sequentially"
  12.307      using bounded_imp_convergent_subsequence [OF s2]
  12.308      unfolding o_def by fast
  12.309    have l1': "((\<lambda>n. fst (f (r1 (r2 n)))) \<longlongrightarrow> l1) sequentially"
  12.310      using LIMSEQ_subseq_LIMSEQ [OF l1 r2] unfolding o_def .
  12.311    have l: "((f \<circ> (r1 \<circ> r2)) \<longlongrightarrow> (l1, l2)) sequentially"
  12.312      using tendsto_Pair [OF l1' l2] unfolding o_def by simp
  12.313 -  have r: "subseq (r1 \<circ> r2)"
  12.314 -    using r1 r2 unfolding subseq_def by simp
  12.315 -  show "\<exists>l r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
  12.316 +  have r: "strict_mono (r1 \<circ> r2)"
  12.317 +    using r1 r2 unfolding strict_mono_def by simp
  12.318 +  show "\<exists>l r. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
  12.319      using l r by fast
  12.320  qed
  12.321  
  12.322 @@ -5641,7 +5641,7 @@
  12.323    {
  12.324      fix f
  12.325      assume as: "(\<forall>n::nat. f n \<in> s)" "Cauchy f"
  12.326 -    from as(1) obtain l r where lr: "l\<in>s" "subseq r" "(f \<circ> r) \<longlonglongrightarrow> l"
  12.327 +    from as(1) obtain l r where lr: "l\<in>s" "strict_mono r" "(f \<circ> r) \<longlonglongrightarrow> l"
  12.328        using assms unfolding compact_def by blast
  12.329  
  12.330      note lr' = seq_suble [OF lr(2)]
  12.331 @@ -5752,8 +5752,8 @@
  12.332        qed
  12.333  
  12.334        define t where "t = rec_nat (sel 0 0) (\<lambda>n i. sel (Suc n) i)"
  12.335 -      have "subseq t"
  12.336 -        unfolding subseq_Suc_iff by (simp add: t_def sel)
  12.337 +      have "strict_mono t"
  12.338 +        unfolding strict_mono_Suc_iff by (simp add: t_def sel)
  12.339        moreover have "\<forall>i. (f \<circ> t) i \<in> s"
  12.340          using f by auto
  12.341        moreover
  12.342 @@ -5777,7 +5777,7 @@
  12.343            by (simp add: dist_commute)
  12.344        qed
  12.345  
  12.346 -      ultimately show "\<exists>l\<in>s. \<exists>r. subseq r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
  12.347 +      ultimately show "\<exists>l\<in>s. \<exists>r. strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
  12.348          using assms unfolding complete_def by blast
  12.349      qed
  12.350    qed
  12.351 @@ -5974,7 +5974,7 @@
  12.352      using choice[of "\<lambda>n x. x \<in> s n"] by auto
  12.353    from assms(4,1) have "seq_compact (s 0)"
  12.354      by (simp add: bounded_closed_imp_seq_compact)
  12.355 -  then obtain l r where lr: "l \<in> s 0" "subseq r" "(x \<circ> r) \<longlonglongrightarrow> l"
  12.356 +  then obtain l r where lr: "l \<in> s 0" "strict_mono r" "(x \<circ> r) \<longlonglongrightarrow> l"
  12.357      using x and assms(3) unfolding seq_compact_def by blast
  12.358    have "\<forall>n. l \<in> s n"
  12.359    proof
  12.360 @@ -7670,7 +7670,7 @@
  12.361        using neg by simp
  12.362      then obtain f where "\<And>n. f n \<in> S" and fG: "\<And>G n. G \<in> \<G> \<Longrightarrow> \<not> ball (f n) (1 / Suc n) \<subseteq> G"
  12.363        by metis
  12.364 -    then obtain l r where "l \<in> S" "subseq r" and to_l: "(f \<circ> r) \<longlonglongrightarrow> l"
  12.365 +    then obtain l r where "l \<in> S" "strict_mono r" and to_l: "(f \<circ> r) \<longlonglongrightarrow> l"
  12.366        using \<open>compact S\<close> compact_def that by metis
  12.367      then obtain G where "l \<in> G" "G \<in> \<G>"
  12.368        using Ssub by auto
  12.369 @@ -7687,7 +7687,7 @@
  12.370        by simp
  12.371      also have "... \<le> 1 / real (Suc (max N1 N2))"
  12.372        apply (simp add: divide_simps del: max.bounded_iff)
  12.373 -      using \<open>subseq r\<close> seq_suble by blast
  12.374 +      using \<open>strict_mono r\<close> seq_suble by blast
  12.375      also have "... \<le> 1 / real (Suc N2)"
  12.376        by (simp add: field_simps)
  12.377      also have "... < e/2"
  12.378 @@ -7851,7 +7851,7 @@
  12.379    apply (clarify, rename_tac l2 r2)
  12.380    apply (rule_tac x="(l1, l2)" in rev_bexI, simp)
  12.381    apply (rule_tac x="r1 \<circ> r2" in exI)
  12.382 -  apply (rule conjI, simp add: subseq_def)
  12.383 +  apply (rule conjI, simp add: strict_mono_def)
  12.384    apply (drule_tac f=r2 in LIMSEQ_subseq_LIMSEQ, assumption)
  12.385    apply (drule (1) tendsto_Pair) back
  12.386    apply (simp add: o_def)
  12.387 @@ -8287,7 +8287,7 @@
  12.388      assume as: "\<forall>n. x n \<in> ?S"  "(x \<longlongrightarrow> l) sequentially"
  12.389      from as(1) obtain f where f: "\<forall>n. x n = fst (f n) + snd (f n)"  "\<forall>n. fst (f n) \<in> S"  "\<forall>n. snd (f n) \<in> T"
  12.390        using choice[of "\<lambda>n y. x n = (fst y) + (snd y) \<and> fst y \<in> S \<and> snd y \<in> T"] by auto
  12.391 -    obtain l' r where "l'\<in>S" and r: "subseq r" and lr: "(((\<lambda>n. fst (f n)) \<circ> r) \<longlongrightarrow> l') sequentially"
  12.392 +    obtain l' r where "l'\<in>S" and r: "strict_mono r" and lr: "(((\<lambda>n. fst (f n)) \<circ> r) \<longlongrightarrow> l') sequentially"
  12.393        using assms(1)[unfolded compact_def, THEN spec[where x="\<lambda> n. fst (f n)"]] using f(2) by auto
  12.394      have "((\<lambda>n. snd (f (r n))) \<longlongrightarrow> l - l') sequentially"
  12.395        using tendsto_diff[OF LIMSEQ_subseq_LIMSEQ[OF as(2) r] lr] and f(1)
    13.1 --- a/src/HOL/Computational_Algebra/Fundamental_Theorem_Algebra.thy	Thu Aug 17 14:40:42 2017 +0200
    13.2 +++ b/src/HOL/Computational_Algebra/Fundamental_Theorem_Algebra.thy	Thu Aug 17 14:52:56 2017 +0200
    13.3 @@ -236,13 +236,13 @@
    13.4  
    13.5  lemma bolzano_weierstrass_complex_disc:
    13.6    assumes r: "\<forall>n. cmod (s n) \<le> r"
    13.7 -  shows "\<exists>f z. subseq f \<and> (\<forall>e >0. \<exists>N. \<forall>n \<ge> N. cmod (s (f n) - z) < e)"
    13.8 +  shows "\<exists>f z. strict_mono (f :: nat \<Rightarrow> nat) \<and> (\<forall>e >0. \<exists>N. \<forall>n \<ge> N. cmod (s (f n) - z) < e)"
    13.9  proof -
   13.10    from seq_monosub[of "Re \<circ> s"]
   13.11 -  obtain f where f: "subseq f" "monoseq (\<lambda>n. Re (s (f n)))"
   13.12 +  obtain f where f: "strict_mono f" "monoseq (\<lambda>n. Re (s (f n)))"
   13.13      unfolding o_def by blast
   13.14    from seq_monosub[of "Im \<circ> s \<circ> f"]
   13.15 -  obtain g where g: "subseq g" "monoseq (\<lambda>n. Im (s (f (g n))))"
   13.16 +  obtain g where g: "strict_mono g" "monoseq (\<lambda>n. Im (s (f (g n))))"
   13.17      unfolding o_def by blast
   13.18    let ?h = "f \<circ> g"
   13.19    from r[rule_format, of 0] have rp: "r \<ge> 0"
   13.20 @@ -284,8 +284,8 @@
   13.21    then have y: "\<forall>r>0. \<exists>n0. \<forall>n\<ge>n0. \<bar>Im (s (f (g n))) - y\<bar> < r"
   13.22      unfolding LIMSEQ_iff real_norm_def .
   13.23    let ?w = "Complex x y"
   13.24 -  from f(1) g(1) have hs: "subseq ?h"
   13.25 -    unfolding subseq_def by auto
   13.26 +  from f(1) g(1) have hs: "strict_mono ?h"
   13.27 +    unfolding strict_mono_def by auto
   13.28    have "\<exists>N. \<forall>n\<ge>N. cmod (s (?h n) - ?w) < e" if "e > 0" for e
   13.29    proof -
   13.30      from that have e2: "e/2 > 0"
   13.31 @@ -400,7 +400,7 @@
   13.32          g: "\<forall>n. cmod (g n) \<le> r" "\<forall>n. cmod (poly p (g n)) <?m + 1 /real(Suc n)"
   13.33        by blast
   13.34      from bolzano_weierstrass_complex_disc[OF g(1)]
   13.35 -    obtain f z where fz: "subseq f" "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. cmod (g (f n) - z) < e"
   13.36 +    obtain f z where fz: "strict_mono (f :: nat \<Rightarrow> nat)" "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. cmod (g (f n) - z) < e"
   13.37        by blast
   13.38      {
   13.39        fix w
    14.1 --- a/src/HOL/Library/Diagonal_Subsequence.thy	Thu Aug 17 14:40:42 2017 +0200
    14.2 +++ b/src/HOL/Library/Diagonal_Subsequence.thy	Thu Aug 17 14:52:56 2017 +0200
    14.3 @@ -8,28 +8,28 @@
    14.4  
    14.5  locale subseqs =
    14.6    fixes P::"nat\<Rightarrow>(nat\<Rightarrow>nat)\<Rightarrow>bool"
    14.7 -  assumes ex_subseq: "\<And>n s. subseq s \<Longrightarrow> \<exists>r'. subseq r' \<and> P n (s o r')"
    14.8 +  assumes ex_subseq: "\<And>n s. strict_mono (s::nat\<Rightarrow>nat) \<Longrightarrow> \<exists>r'. strict_mono r' \<and> P n (s o r')"
    14.9  begin
   14.10  
   14.11 -definition reduce where "reduce s n = (SOME r'. subseq r' \<and> P n (s o r'))"
   14.12 +definition reduce where "reduce s n = (SOME r'::nat\<Rightarrow>nat. strict_mono r' \<and> P n (s o r'))"
   14.13  
   14.14  lemma subseq_reduce[intro, simp]:
   14.15 -  "subseq s \<Longrightarrow> subseq (reduce s n)"
   14.16 +  "strict_mono s \<Longrightarrow> strict_mono (reduce s n)"
   14.17    unfolding reduce_def by (rule someI2_ex[OF ex_subseq]) auto
   14.18  
   14.19  lemma reduce_holds:
   14.20 -  "subseq s \<Longrightarrow> P n (s o reduce s n)"
   14.21 +  "strict_mono s \<Longrightarrow> P n (s o reduce s n)"
   14.22    unfolding reduce_def by (rule someI2_ex[OF ex_subseq]) (auto simp: o_def)
   14.23  
   14.24 -primrec seqseq where
   14.25 +primrec seqseq :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
   14.26    "seqseq 0 = id"
   14.27  | "seqseq (Suc n) = seqseq n o reduce (seqseq n) n"
   14.28  
   14.29 -lemma subseq_seqseq[intro, simp]: "subseq (seqseq n)"
   14.30 +lemma subseq_seqseq[intro, simp]: "strict_mono (seqseq n)"
   14.31  proof (induct n)
   14.32 -  case 0 thus ?case by (simp add: subseq_def)
   14.33 +  case 0 thus ?case by (simp add: strict_mono_def)
   14.34  next
   14.35 -  case (Suc n) thus ?case by (subst seqseq.simps) (auto intro!: subseq_o)
   14.36 +  case (Suc n) thus ?case by (subst seqseq.simps) (auto intro!: strict_mono_o)
   14.37  qed
   14.38  
   14.39  lemma seqseq_holds:
   14.40 @@ -40,35 +40,29 @@
   14.41    thus ?thesis by simp
   14.42  qed
   14.43  
   14.44 -definition diagseq where "diagseq i = seqseq i i"
   14.45 -
   14.46 -lemma subseq_mono: "subseq f \<Longrightarrow> a \<le> b \<Longrightarrow> f a \<le> f b"
   14.47 -  by (metis le_eq_less_or_eq subseq_mono)
   14.48 -
   14.49 -lemma subseq_strict_mono: "subseq f \<Longrightarrow> a < b \<Longrightarrow> f a < f b"
   14.50 -  by (simp add: subseq_def)
   14.51 +definition diagseq :: "nat \<Rightarrow> nat" where "diagseq i = seqseq i i"
   14.52  
   14.53  lemma diagseq_mono: "diagseq n < diagseq (Suc n)"
   14.54  proof -
   14.55    have "diagseq n < seqseq n (Suc n)"
   14.56 -    using subseq_seqseq[of n] by (simp add: diagseq_def subseq_def)
   14.57 +    using subseq_seqseq[of n] by (simp add: diagseq_def strict_mono_def)
   14.58    also have "\<dots> \<le> seqseq n (reduce (seqseq n) n (Suc n))"
   14.59 -    by (auto intro: subseq_mono seq_suble)
   14.60 +    using strict_mono_less_eq seq_suble by blast
   14.61    also have "\<dots> = diagseq (Suc n)" by (simp add: diagseq_def)
   14.62    finally show ?thesis .
   14.63  qed
   14.64  
   14.65 -lemma subseq_diagseq: "subseq diagseq"
   14.66 -  using diagseq_mono by (simp add: subseq_Suc_iff diagseq_def)
   14.67 +lemma subseq_diagseq: "strict_mono diagseq"
   14.68 +  using diagseq_mono by (simp add: strict_mono_Suc_iff diagseq_def)
   14.69  
   14.70  primrec fold_reduce where
   14.71    "fold_reduce n 0 = id"
   14.72  | "fold_reduce n (Suc k) = fold_reduce n k o reduce (seqseq (n + k)) (n + k)"
   14.73  
   14.74 -lemma subseq_fold_reduce[intro, simp]: "subseq (fold_reduce n k)"
   14.75 +lemma subseq_fold_reduce[intro, simp]: "strict_mono (fold_reduce n k)"
   14.76  proof (induct k)
   14.77 -  case (Suc k) from subseq_o[OF this subseq_reduce] show ?case by (simp add: o_def)
   14.78 -qed (simp add: subseq_def)
   14.79 +  case (Suc k) from strict_mono_o[OF this subseq_reduce] show ?case by (simp add: o_def)
   14.80 +qed (simp add: strict_mono_def)
   14.81  
   14.82  lemma ex_subseq_reduce_index: "seqseq (n + k) = seqseq n o fold_reduce n k"
   14.83    by (induct k) simp_all
   14.84 @@ -95,14 +89,14 @@
   14.85    assumes "m \<le> n" shows "diagseq n = (seqseq m o (fold_reduce m (n - m))) n"
   14.86    using diagseq_add[of m "n - m"] assms by simp
   14.87  
   14.88 -lemma subseq_diagonal_rest: "subseq (\<lambda>x. fold_reduce k x (k + x))"
   14.89 -  unfolding subseq_Suc_iff fold_reduce.simps o_def
   14.90 +lemma subseq_diagonal_rest: "strict_mono (\<lambda>x. fold_reduce k x (k + x))"
   14.91 +  unfolding strict_mono_Suc_iff fold_reduce.simps o_def
   14.92  proof
   14.93    fix n
   14.94    have "fold_reduce k n (k + n) < fold_reduce k n (k + Suc n)" (is "?lhs < _")
   14.95 -    by (auto intro: subseq_strict_mono)
   14.96 +    by (auto intro: strict_monoD)
   14.97    also have "\<dots> \<le> fold_reduce k n (reduce (seqseq (k + n)) (k + n) (k + Suc n))"
   14.98 -    by (rule subseq_mono) (auto intro!: seq_suble subseq_mono)
   14.99 +    by (auto intro: less_mono_imp_le_mono seq_suble strict_monoD)
  14.100    finally show "?lhs < \<dots>" .
  14.101  qed
  14.102  
  14.103 @@ -110,7 +104,7 @@
  14.104    by (auto simp: o_def diagseq_add)
  14.105  
  14.106  lemma diagseq_holds:
  14.107 -  assumes subseq_stable: "\<And>r s n. subseq r \<Longrightarrow> P n s \<Longrightarrow> P n (s o r)"
  14.108 +  assumes subseq_stable: "\<And>r s n. strict_mono r \<Longrightarrow> P n s \<Longrightarrow> P n (s o r)"
  14.109    shows "P k (diagseq o (op + (Suc k)))"
  14.110    unfolding diagseq_seqseq by (intro subseq_stable subseq_diagonal_rest seqseq_holds)
  14.111  
    15.1 --- a/src/HOL/Library/Liminf_Limsup.thy	Thu Aug 17 14:40:42 2017 +0200
    15.2 +++ b/src/HOL/Library/Liminf_Limsup.thy	Thu Aug 17 14:52:56 2017 +0200
    15.3 @@ -379,20 +379,20 @@
    15.4  
    15.5  lemma liminf_subseq_mono:
    15.6    fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
    15.7 -  assumes "subseq r"
    15.8 +  assumes "strict_mono r"
    15.9    shows "liminf X \<le> liminf (X \<circ> r) "
   15.10  proof-
   15.11    have "\<And>n. (INF m:{n..}. X m) \<le> (INF m:{n..}. (X \<circ> r) m)"
   15.12    proof (safe intro!: INF_mono)
   15.13      fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. X ma \<le> (X \<circ> r) m"
   15.14 -      using seq_suble[OF \<open>subseq r\<close>, of m] by (intro bexI[of _ "r m"]) auto
   15.15 +      using seq_suble[OF \<open>strict_mono r\<close>, of m] by (intro bexI[of _ "r m"]) auto
   15.16    qed
   15.17    then show ?thesis by (auto intro!: SUP_mono simp: liminf_SUP_INF comp_def)
   15.18  qed
   15.19  
   15.20  lemma limsup_subseq_mono:
   15.21    fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
   15.22 -  assumes "subseq r"
   15.23 +  assumes "strict_mono r"
   15.24    shows "limsup (X \<circ> r) \<le> limsup X"
   15.25  proof-
   15.26    have "(SUP m:{n..}. (X \<circ> r) m) \<le> (SUP m:{n..}. X m)" for n
   15.27 @@ -400,7 +400,7 @@
   15.28      fix m :: nat
   15.29      assume "n \<le> m"
   15.30      then show "\<exists>ma\<in>{n..}. (X \<circ> r) m \<le> X ma"
   15.31 -      using seq_suble[OF \<open>subseq r\<close>, of m] by (intro bexI[of _ "r m"]) auto
   15.32 +      using seq_suble[OF \<open>strict_mono r\<close>, of m] by (intro bexI[of _ "r m"]) auto
   15.33    qed
   15.34    then show ?thesis
   15.35      by (auto intro!: INF_mono simp: limsup_INF_SUP comp_def)
   15.36 @@ -587,9 +587,9 @@
   15.37  
   15.38  lemma compact_complete_linorder:
   15.39    fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
   15.40 -  shows "\<exists>l r. subseq r \<and> (X \<circ> r) \<longlonglongrightarrow> l"
   15.41 +  shows "\<exists>l r. strict_mono r \<and> (X \<circ> r) \<longlonglongrightarrow> l"
   15.42  proof -
   15.43 -  obtain r where "subseq r" and mono: "monoseq (X \<circ> r)"
   15.44 +  obtain r where "strict_mono r" and mono: "monoseq (X \<circ> r)"
   15.45      using seq_monosub[of X]
   15.46      unfolding comp_def
   15.47      by auto
   15.48 @@ -599,7 +599,7 @@
   15.49       using lim_increasing_cl[of "X \<circ> r"] lim_decreasing_cl[of "X \<circ> r"]
   15.50       by auto
   15.51    then show ?thesis
   15.52 -    using \<open>subseq r\<close> by auto
   15.53 +    using \<open>strict_mono r\<close> by auto
   15.54  qed
   15.55  
   15.56  lemma tendsto_Limsup:
    16.1 --- a/src/HOL/Limits.thy	Thu Aug 17 14:40:42 2017 +0200
    16.2 +++ b/src/HOL/Limits.thy	Thu Aug 17 14:52:56 2017 +0200
    16.3 @@ -325,7 +325,7 @@
    16.4    using Bseq_offset[of f 1] by (auto intro: Bseq_subseq)
    16.5  
    16.6  lemma increasing_Bseq_subseq_iff:
    16.7 -  assumes "\<And>x y. x \<le> y \<Longrightarrow> norm (f x :: 'a::real_normed_vector) \<le> norm (f y)" "subseq g"
    16.8 +  assumes "\<And>x y. x \<le> y \<Longrightarrow> norm (f x :: 'a::real_normed_vector) \<le> norm (f y)" "strict_mono g"
    16.9    shows "Bseq (\<lambda>x. f (g x)) \<longleftrightarrow> Bseq f"
   16.10  proof
   16.11    assume "Bseq (\<lambda>x. f (g x))"
   16.12 @@ -346,7 +346,7 @@
   16.13  lemma nonneg_incseq_Bseq_subseq_iff:
   16.14    fixes f :: "nat \<Rightarrow> real"
   16.15      and g :: "nat \<Rightarrow> nat"
   16.16 -  assumes "\<And>x. f x \<ge> 0" "incseq f" "subseq g"
   16.17 +  assumes "\<And>x. f x \<ge> 0" "incseq f" "strict_mono g"
   16.18    shows "Bseq (\<lambda>x. f (g x)) \<longleftrightarrow> Bseq f"
   16.19    using assms by (intro increasing_Bseq_subseq_iff) (auto simp: incseq_def)
   16.20  
   16.21 @@ -1398,11 +1398,11 @@
   16.22  
   16.23  lemma mult_nat_left_at_top: "c > 0 \<Longrightarrow> filterlim (\<lambda>x. c * x) at_top sequentially"
   16.24    for c :: nat
   16.25 -  by (rule filterlim_subseq) (auto simp: subseq_def)
   16.26 +  by (rule filterlim_subseq) (auto simp: strict_mono_def)
   16.27  
   16.28  lemma mult_nat_right_at_top: "c > 0 \<Longrightarrow> filterlim (\<lambda>x. x * c) at_top sequentially"
   16.29    for c :: nat
   16.30 -  by (rule filterlim_subseq) (auto simp: subseq_def)
   16.31 +  by (rule filterlim_subseq) (auto simp: strict_mono_def)
   16.32  
   16.33  lemma at_to_infinity: "(at (0::'a::{real_normed_field,field})) = filtermap inverse at_infinity"
   16.34  proof (rule antisym)
    17.1 --- a/src/HOL/Probability/Helly_Selection.thy	Thu Aug 17 14:40:42 2017 +0200
    17.2 +++ b/src/HOL/Probability/Helly_Selection.thy	Thu Aug 17 14:52:56 2017 +0200
    17.3 @@ -19,7 +19,7 @@
    17.4    assumes rcont: "\<And>n x. continuous (at_right x) (f n)"
    17.5    assumes mono: "\<And>n. mono (f n)"
    17.6    assumes bdd: "\<And>n x. \<bar>f n x\<bar> \<le> M"
    17.7 -  shows "\<exists>s. subseq s \<and> (\<exists>F. (\<forall>x. continuous (at_right x) F) \<and> mono F \<and> (\<forall>x. \<bar>F x\<bar> \<le> M) \<and>
    17.8 +  shows "\<exists>s. strict_mono (s::nat \<Rightarrow> nat) \<and> (\<exists>F. (\<forall>x. continuous (at_right x) F) \<and> mono F \<and> (\<forall>x. \<bar>F x\<bar> \<le> M) \<and>
    17.9      (\<forall>x. continuous (at x) F \<longrightarrow> (\<lambda>n. f (s n) x) \<longlonglongrightarrow> F x))"
   17.10  proof -
   17.11    obtain m :: "real \<Rightarrow> nat" where "bij_betw m \<rat> UNIV"
   17.12 @@ -33,18 +33,18 @@
   17.13    let ?P = "\<lambda>n. \<lambda>s. convergent (\<lambda>k. f (s k) (r n))"
   17.14    interpret nat: subseqs ?P
   17.15    proof (unfold convergent_def, unfold subseqs_def, auto)
   17.16 -    fix n :: nat and s :: "nat \<Rightarrow> nat" assume s: "subseq s"
   17.17 +    fix n :: nat and s :: "nat \<Rightarrow> nat" assume s: "strict_mono s"
   17.18      have "bounded {-M..M}"
   17.19        using bounded_closed_interval by auto
   17.20      moreover have "\<And>k. f (s k) (r n) \<in> {-M..M}"
   17.21        using bdd by (simp add: abs_le_iff minus_le_iff)
   17.22 -    ultimately have "\<exists>l s'. subseq s' \<and> ((\<lambda>k. f (s k) (r n)) \<circ> s') \<longlonglongrightarrow> l"
   17.23 +    ultimately have "\<exists>l s'. strict_mono s' \<and> ((\<lambda>k. f (s k) (r n)) \<circ> s') \<longlonglongrightarrow> l"
   17.24        using compact_Icc compact_imp_seq_compact seq_compactE by metis
   17.25 -    thus "\<exists>s'. subseq s' \<and> (\<exists>l. (\<lambda>k. f (s (s' k)) (r n)) \<longlonglongrightarrow> l)"
   17.26 +    thus "\<exists>s'. strict_mono (s'::nat\<Rightarrow>nat) \<and> (\<exists>l. (\<lambda>k. f (s (s' k)) (r n)) \<longlonglongrightarrow> l)"
   17.27        by (auto simp: comp_def)
   17.28    qed
   17.29    define d where "d = nat.diagseq"
   17.30 -  have subseq: "subseq d"
   17.31 +  have subseq: "strict_mono d"
   17.32      unfolding d_def using nat.subseq_diagseq by auto
   17.33    have rat_cnv: "?P n d" for n
   17.34    proof -
   17.35 @@ -157,8 +157,8 @@
   17.36  
   17.37  (* Can strengthen to equivalence. *)
   17.38  theorem tight_imp_convergent_subsubsequence:
   17.39 -  assumes \<mu>: "tight \<mu>" "subseq s"
   17.40 -  shows "\<exists>r M. subseq r \<and> real_distribution M \<and> weak_conv_m (\<mu> \<circ> s \<circ> r) M"
   17.41 +  assumes \<mu>: "tight \<mu>" "strict_mono s"
   17.42 +  shows "\<exists>r M. strict_mono (r :: nat \<Rightarrow> nat) \<and> real_distribution M \<and> weak_conv_m (\<mu> \<circ> s \<circ> r) M"
   17.43  proof -
   17.44    define f where "f k = cdf (\<mu> (s k))" for k
   17.45    interpret \<mu>: real_distribution "\<mu> k" for k
   17.46 @@ -174,7 +174,7 @@
   17.47      by (auto simp add: abs_le_iff minus_le_iff f_def \<mu>.cdf_nonneg \<mu>.cdf_bounded_prob)
   17.48  
   17.49    from Helly_selection[OF rcont mono bdd, of "\<lambda>x. x"] obtain r F
   17.50 -    where F: "subseq r" "\<And>x. continuous (at_right x) F" "mono F" "\<And>x. \<bar>F x\<bar> \<le> 1"
   17.51 +    where F: "strict_mono r" "\<And>x. continuous (at_right x) F" "mono F" "\<And>x. \<bar>F x\<bar> \<le> 1"
   17.52      and lim_F: "\<And>x. continuous (at x) F \<Longrightarrow> (\<lambda>n. f (r n) x) \<longlonglongrightarrow> F x"
   17.53      by blast
   17.54  
   17.55 @@ -265,14 +265,14 @@
   17.56      using F by (auto intro!: real_distribution_interval_measure cdf_interval_measure simp: mono_def)
   17.57    with lim_F LIMSEQ_subseq_LIMSEQ M have "weak_conv_m (\<mu> \<circ> s \<circ> r) (interval_measure F)"
   17.58      by (auto simp: weak_conv_def weak_conv_m_def f_def comp_def)
   17.59 -  then show "\<exists>r M. subseq r \<and> (real_distribution M \<and> weak_conv_m (\<mu> \<circ> s \<circ> r) M)"
   17.60 +  then show "\<exists>r M. strict_mono (r :: nat \<Rightarrow> nat) \<and> (real_distribution M \<and> weak_conv_m (\<mu> \<circ> s \<circ> r) M)"
   17.61      using F M by auto
   17.62  qed
   17.63  
   17.64  corollary tight_subseq_weak_converge:
   17.65    fixes \<mu> :: "nat \<Rightarrow> real measure" and M :: "real measure"
   17.66    assumes "\<And>n. real_distribution (\<mu> n)" "real_distribution M" and tight: "tight \<mu>" and
   17.67 -    subseq: "\<And>s \<nu>. subseq s \<Longrightarrow> real_distribution \<nu> \<Longrightarrow> weak_conv_m (\<mu> \<circ> s) \<nu> \<Longrightarrow> weak_conv_m (\<mu> \<circ> s) M"
   17.68 +    subseq: "\<And>s \<nu>. strict_mono s \<Longrightarrow> real_distribution \<nu> \<Longrightarrow> weak_conv_m (\<mu> \<circ> s) \<nu> \<Longrightarrow> weak_conv_m (\<mu> \<circ> s) M"
   17.69    shows "weak_conv_m \<mu> M"
   17.70  proof (rule ccontr)
   17.71    define f where "f n = cdf (\<mu> n)" for n
   17.72 @@ -283,12 +283,12 @@
   17.73      by (auto simp: weak_conv_m_def weak_conv_def f_def F_def)
   17.74    then obtain \<epsilon> where "\<epsilon> > 0" and "infinite {n. \<not> dist (f n x) (F x) < \<epsilon>}"
   17.75      by (auto simp: tendsto_iff not_eventually INFM_iff_infinite cofinite_eq_sequentially[symmetric])
   17.76 -  then obtain s where s: "\<And>n. \<not> dist (f (s n) x) (F x) < \<epsilon>" and "subseq s"
   17.77 -    using enumerate_in_set enumerate_mono by (fastforce simp: subseq_def)
   17.78 -  then obtain r \<nu> where r: "subseq r" "real_distribution \<nu>" "weak_conv_m (\<mu> \<circ> s \<circ> r) \<nu>"
   17.79 +  then obtain s :: "nat \<Rightarrow> nat" where s: "\<And>n. \<not> dist (f (s n) x) (F x) < \<epsilon>" and "strict_mono s"
   17.80 +    using enumerate_in_set enumerate_mono by (fastforce simp: strict_mono_def)
   17.81 +  then obtain r \<nu> where r: "strict_mono r" "real_distribution \<nu>" "weak_conv_m (\<mu> \<circ> s \<circ> r) \<nu>"
   17.82      using tight_imp_convergent_subsubsequence[OF tight] by blast
   17.83    then have "weak_conv_m (\<mu> \<circ> (s \<circ> r)) M"
   17.84 -    using \<open>subseq s\<close> r by (intro subseq subseq_o) (auto simp: comp_assoc)
   17.85 +    using \<open>strict_mono s\<close> r by (intro subseq strict_mono_o) (auto simp: comp_assoc)
   17.86    then have "(\<lambda>n. f (s (r n)) x) \<longlonglongrightarrow> F x"
   17.87      using x by (auto simp: weak_conv_m_def weak_conv_def F_def f_def)
   17.88    then show False
    18.1 --- a/src/HOL/Probability/Levy.thy	Thu Aug 17 14:40:42 2017 +0200
    18.2 +++ b/src/HOL/Probability/Levy.thy	Thu Aug 17 14:52:56 2017 +0200
    18.3 @@ -500,7 +500,7 @@
    18.4    show ?thesis
    18.5    proof (rule tight_subseq_weak_converge [OF real_distr_M real_distr_M' tight])
    18.6      fix s \<nu>
    18.7 -    assume s: "subseq s"
    18.8 +    assume s: "strict_mono (s :: nat \<Rightarrow> nat)"
    18.9      assume nu: "weak_conv_m (M \<circ> s) \<nu>"
   18.10      assume *: "real_distribution \<nu>"
   18.11      have 2: "\<And>n. real_distribution ((M \<circ> s) n)" unfolding comp_def by (rule assms)
    19.1 --- a/src/HOL/Probability/Projective_Limit.thy	Thu Aug 17 14:40:42 2017 +0200
    19.2 +++ b/src/HOL/Probability/Projective_Limit.thy	Thu Aug 17 14:52:56 2017 +0200
    19.3 @@ -45,20 +45,20 @@
    19.4  lemma compactE':
    19.5    fixes S :: "'a :: metric_space set"
    19.6    assumes "compact S" "\<forall>n\<ge>m. f n \<in> S"
    19.7 -  obtains l r where "l \<in> S" "subseq r" "((f \<circ> r) \<longlongrightarrow> l) sequentially"
    19.8 +  obtains l r where "l \<in> S" "strict_mono (r::nat\<Rightarrow>nat)" "((f \<circ> r) \<longlongrightarrow> l) sequentially"
    19.9  proof atomize_elim
   19.10 -  have "subseq (op + m)" by (simp add: subseq_def)
   19.11 +  have "strict_mono (op + m)" by (simp add: strict_mono_def)
   19.12    have "\<forall>n. (f o (\<lambda>i. m + i)) n \<in> S" using assms by auto
   19.13    from seq_compactE[OF \<open>compact S\<close>[unfolded compact_eq_seq_compact_metric] this] guess l r .
   19.14 -  hence "l \<in> S" "subseq ((\<lambda>i. m + i) o r) \<and> (f \<circ> ((\<lambda>i. m + i) o r)) \<longlonglongrightarrow> l"
   19.15 -    using subseq_o[OF \<open>subseq (op + m)\<close> \<open>subseq r\<close>] by (auto simp: o_def)
   19.16 -  thus "\<exists>l r. l \<in> S \<and> subseq r \<and> (f \<circ> r) \<longlonglongrightarrow> l" by blast
   19.17 +  hence "l \<in> S" "strict_mono ((\<lambda>i. m + i) o r) \<and> (f \<circ> ((\<lambda>i. m + i) o r)) \<longlonglongrightarrow> l"
   19.18 +    using strict_mono_o[OF \<open>strict_mono (op + m)\<close> \<open>strict_mono r\<close>] by (auto simp: o_def)
   19.19 +  thus "\<exists>l r. l \<in> S \<and> strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> l" by blast
   19.20  qed
   19.21  
   19.22  sublocale finmap_seqs_into_compact \<subseteq> subseqs "\<lambda>n s. (\<exists>l. (\<lambda>i. ((f o s) i)\<^sub>F n) \<longlonglongrightarrow> l)"
   19.23  proof
   19.24 -  fix n s
   19.25 -  assume "subseq s"
   19.26 +  fix n and s :: "nat \<Rightarrow> nat"
   19.27 +  assume "strict_mono s"
   19.28    from proj_in_KE[of n] guess n0 . note n0 = this
   19.29    have "\<forall>i \<ge> n0. ((f \<circ> s) i)\<^sub>F n \<in> (\<lambda>k. (k)\<^sub>F n) ` K n0"
   19.30    proof safe
   19.31 @@ -69,7 +69,7 @@
   19.32        by auto
   19.33    qed
   19.34    from compactE'[OF compact_projset this] guess ls rs .
   19.35 -  thus "\<exists>r'. subseq r' \<and> (\<exists>l. (\<lambda>i. ((f \<circ> (s \<circ> r')) i)\<^sub>F n) \<longlonglongrightarrow> l)" by (auto simp: o_def)
   19.36 +  thus "\<exists>r'. strict_mono r' \<and> (\<exists>l. (\<lambda>i. ((f \<circ> (s \<circ> r')) i)\<^sub>F n) \<longlonglongrightarrow> l)" by (auto simp: o_def)
   19.37  qed
   19.38  
   19.39  lemma (in finmap_seqs_into_compact) diagonal_tendsto: "\<exists>l. (\<lambda>i. (f (diagseq i))\<^sub>F n) \<longlonglongrightarrow> l"
   19.40 @@ -77,11 +77,11 @@
   19.41    obtain l where "(\<lambda>i. ((f o (diagseq o op + (Suc n))) i)\<^sub>F n) \<longlonglongrightarrow> l"
   19.42    proof (atomize_elim, rule diagseq_holds)
   19.43      fix r s n
   19.44 -    assume "subseq r"
   19.45 +    assume "strict_mono (r :: nat \<Rightarrow> nat)"
   19.46      assume "\<exists>l. (\<lambda>i. ((f \<circ> s) i)\<^sub>F n) \<longlonglongrightarrow> l"
   19.47      then obtain l where "((\<lambda>i. (f i)\<^sub>F n) o s) \<longlonglongrightarrow> l"
   19.48        by (auto simp: o_def)
   19.49 -    hence "((\<lambda>i. (f i)\<^sub>F n) o s o r) \<longlonglongrightarrow> l" using \<open>subseq r\<close>
   19.50 +    hence "((\<lambda>i. (f i)\<^sub>F n) o s o r) \<longlonglongrightarrow> l" using \<open>strict_mono r\<close>
   19.51        by (rule LIMSEQ_subseq_LIMSEQ)
   19.52      thus "\<exists>l. (\<lambda>i. ((f \<circ> (s \<circ> r)) i)\<^sub>F n) \<longlonglongrightarrow> l" by (auto simp add: o_def)
   19.53    qed
   19.54 @@ -406,7 +406,7 @@
   19.55      have "(\<lambda>i. fm n (y (Suc (diagseq i)))) \<longlonglongrightarrow> finmap_of (Utn ` J n) z"
   19.56        by (rule tendsto_finmap)
   19.57      hence "((\<lambda>i. fm n (y (Suc (diagseq i)))) o (\<lambda>i. i + n)) \<longlonglongrightarrow> finmap_of (Utn ` J n) z"
   19.58 -      by (rule LIMSEQ_subseq_LIMSEQ) (simp add: subseq_def)
   19.59 +      by (rule LIMSEQ_subseq_LIMSEQ) (simp add: strict_mono_def)
   19.60      moreover
   19.61      have "(\<forall>i. ((\<lambda>i. fm n (y (Suc (diagseq i)))) o (\<lambda>i. i + n)) i \<in> K' n)"
   19.62        apply (auto simp add: o_def intro!: fm_in_K' \<open>1 \<le> n\<close> le_SucI)
    20.1 --- a/src/HOL/Series.thy	Thu Aug 17 14:40:42 2017 +0200
    20.2 +++ b/src/HOL/Series.thy	Thu Aug 17 14:52:56 2017 +0200
    20.3 @@ -1107,7 +1107,7 @@
    20.4  qed
    20.5  
    20.6  lemma sums_mono_reindex:
    20.7 -  assumes subseq: "subseq g"
    20.8 +  assumes subseq: "strict_mono g"
    20.9      and zero: "\<And>n. n \<notin> range g \<Longrightarrow> f n = 0"
   20.10    shows "(\<lambda>n. f (g n)) sums c \<longleftrightarrow> f sums c"
   20.11    unfolding sums_def
   20.12 @@ -1117,10 +1117,10 @@
   20.13    proof
   20.14      fix n :: nat
   20.15      from subseq have "(\<Sum>k<n. f (g k)) = (\<Sum>k\<in>g`{..<n}. f k)"
   20.16 -      by (subst sum.reindex) (auto intro: subseq_imp_inj_on)
   20.17 +      by (subst sum.reindex) (auto intro: strict_mono_imp_inj_on)
   20.18      also from subseq have "\<dots> = (\<Sum>k<g n. f k)"
   20.19        by (intro sum.mono_neutral_left ballI zero)
   20.20 -        (auto dest: subseq_strict_mono simp: strict_mono_less strict_mono_less_eq)
   20.21 +        (auto simp: strict_mono_less strict_mono_less_eq)
   20.22      finally show "(\<Sum>k<n. f (g k)) = (\<Sum>k<g n. f k)" .
   20.23    qed
   20.24    also from LIMSEQ_subseq_LIMSEQ[OF lim subseq] have "\<dots> \<longlonglongrightarrow> c"
   20.25 @@ -1150,7 +1150,7 @@
   20.26          have "g l < g (g_inv n)"
   20.27            by (rule less_le_trans[OF _ g_inv]) (use k l in simp_all)
   20.28          with subseq have "l < g_inv n"
   20.29 -          by (simp add: subseq_strict_mono strict_mono_less)
   20.30 +          by (simp add: strict_mono_less)
   20.31          with k l show False
   20.32            by simp
   20.33        qed
   20.34 @@ -1160,7 +1160,7 @@
   20.35      with g_inv_least' g_inv have "(\<Sum>k<n. f k) = (\<Sum>k\<in>g`{..<g_inv n}. f k)"
   20.36        by (intro sum.mono_neutral_right) auto
   20.37      also from subseq have "\<dots> = (\<Sum>k<g_inv n. f (g k))"
   20.38 -      using subseq_imp_inj_on by (subst sum.reindex) simp_all
   20.39 +      using strict_mono_imp_inj_on by (subst sum.reindex) simp_all
   20.40      finally show "(\<Sum>k<n. f k) = (\<Sum>k<g_inv n. f (g k))" .
   20.41    qed
   20.42    also {
   20.43 @@ -1169,7 +1169,7 @@
   20.44      also have "n \<le> g (g_inv n)"
   20.45        by (rule g_inv)
   20.46      finally have "K \<le> g_inv n"
   20.47 -      using subseq by (simp add: strict_mono_less_eq subseq_strict_mono)
   20.48 +      using subseq by (simp add: strict_mono_less_eq)
   20.49    }
   20.50    then have "filterlim g_inv at_top sequentially"
   20.51      by (auto simp: filterlim_at_top eventually_at_top_linorder)
   20.52 @@ -1179,14 +1179,14 @@
   20.53  qed
   20.54  
   20.55  lemma summable_mono_reindex:
   20.56 -  assumes subseq: "subseq g"
   20.57 +  assumes subseq: "strict_mono g"
   20.58      and zero: "\<And>n. n \<notin> range g \<Longrightarrow> f n = 0"
   20.59    shows "summable (\<lambda>n. f (g n)) \<longleftrightarrow> summable f"
   20.60    using sums_mono_reindex[of g f, OF assms] by (simp add: summable_def)
   20.61  
   20.62  lemma suminf_mono_reindex:
   20.63    fixes f :: "nat \<Rightarrow> 'a::{t2_space,comm_monoid_add}"
   20.64 -  assumes "subseq g" "\<And>n. n \<notin> range g \<Longrightarrow> f n = 0"
   20.65 +  assumes "strict_mono g" "\<And>n. n \<notin> range g \<Longrightarrow> f n = 0"
   20.66    shows   "suminf (\<lambda>n. f (g n)) = suminf f"
   20.67  proof (cases "summable f")
   20.68    case True
    21.1 --- a/src/HOL/Topological_Spaces.thy	Thu Aug 17 14:40:42 2017 +0200
    21.2 +++ b/src/HOL/Topological_Spaces.thy	Thu Aug 17 14:52:56 2017 +0200
    21.3 @@ -1069,14 +1069,13 @@
    21.4    unfolding antimono_def ..
    21.5  
    21.6  text \<open>Definition of subsequence.\<close>
    21.7 -definition subseq :: "(nat \<Rightarrow> nat) \<Rightarrow> bool"
    21.8 -  where "subseq f \<longleftrightarrow> (\<forall>m. \<forall>n>m. f m < f n)"
    21.9 -
   21.10 -lemma subseq_le_mono: "subseq r \<Longrightarrow> m \<le> n \<Longrightarrow> r m \<le> r n"
   21.11 -  by (simp add: less_mono_imp_le_mono subseq_def)
   21.12 -
   21.13 -lemma subseq_id: "subseq id"
   21.14 -  by (simp add: subseq_def)
   21.15 +
   21.16 +(* For compatibility with the old "subseq" *)
   21.17 +lemma strict_mono_leD: "strict_mono r \<Longrightarrow> m \<le> n \<Longrightarrow> r m \<le> r n"
   21.18 +  by (erule (1) monoD [OF strict_mono_mono])
   21.19 +
   21.20 +lemma strict_mono_id: "strict_mono id"
   21.21 +  by (simp add: strict_mono_def)
   21.22  
   21.23  lemma incseq_SucI: "(\<And>n. X n \<le> X (Suc n)) \<Longrightarrow> incseq X"
   21.24    using lift_Suc_mono_le[of X] by (auto simp: incseq_def)
   21.25 @@ -1144,28 +1143,30 @@
   21.26  
   21.27  text \<open>Subsequence (alternative definition, (e.g. Hoskins)\<close>
   21.28  
   21.29 -lemma subseq_Suc_iff: "subseq f \<longleftrightarrow> (\<forall>n. f n < f (Suc n))"
   21.30 -  apply (simp add: subseq_def)
   21.31 -  apply (auto dest!: less_imp_Suc_add)
   21.32 -  apply (induct_tac k)
   21.33 -   apply (auto intro: less_trans)
   21.34 -  done
   21.35 -
   21.36 -lemma subseq_add: "subseq (\<lambda>n. n + k)"
   21.37 -  by (auto simp: subseq_Suc_iff)
   21.38 +lemma strict_mono_Suc_iff: "strict_mono f \<longleftrightarrow> (\<forall>n. f n < f (Suc n))"
   21.39 +proof (intro iffI strict_monoI)
   21.40 +  assume *: "\<forall>n. f n < f (Suc n)"
   21.41 +  fix m n :: nat assume "m < n"
   21.42 +  thus "f m < f n"
   21.43 +    by (induction rule: less_Suc_induct) (use * in auto)
   21.44 +qed (auto simp: strict_mono_def)
   21.45 +
   21.46 +lemma strict_mono_add: "strict_mono (\<lambda>n::'a::linordered_semidom. n + k)"
   21.47 +  by (auto simp: strict_mono_def)
   21.48  
   21.49  text \<open>For any sequence, there is a monotonic subsequence.\<close>
   21.50  lemma seq_monosub:
   21.51    fixes s :: "nat \<Rightarrow> 'a::linorder"
   21.52 -  shows "\<exists>f. subseq f \<and> monoseq (\<lambda>n. (s (f n)))"
   21.53 +  shows "\<exists>f. strict_mono f \<and> monoseq (\<lambda>n. (s (f n)))"
   21.54  proof (cases "\<forall>n. \<exists>p>n. \<forall>m\<ge>p. s m \<le> s p")
   21.55    case True
   21.56    then have "\<exists>f. \<forall>n. (\<forall>m\<ge>f n. s m \<le> s (f n)) \<and> f n < f (Suc n)"
   21.57      by (intro dependent_nat_choice) (auto simp: conj_commute)
   21.58 -  then obtain f where f: "subseq f" and mono: "\<And>n m. f n \<le> m \<Longrightarrow> s m \<le> s (f n)"
   21.59 -    by (auto simp: subseq_Suc_iff)
   21.60 +  then obtain f :: "nat \<Rightarrow> nat" 
   21.61 +    where f: "strict_mono f" and mono: "\<And>n m. f n \<le> m \<Longrightarrow> s m \<le> s (f n)"
   21.62 +    by (auto simp: strict_mono_Suc_iff)
   21.63    then have "incseq f"
   21.64 -    unfolding subseq_Suc_iff incseq_Suc_iff by (auto intro: less_imp_le)
   21.65 +    unfolding strict_mono_Suc_iff incseq_Suc_iff by (auto intro: less_imp_le)
   21.66    then have "monoseq (\<lambda>n. s (f n))"
   21.67      by (auto simp add: incseq_def intro!: mono monoI2)
   21.68    with f show ?thesis
   21.69 @@ -1182,29 +1183,29 @@
   21.70        by (auto intro: less_trans)
   21.71    qed auto
   21.72    then show ?thesis
   21.73 -    by (auto simp: monoseq_iff incseq_Suc_iff subseq_Suc_iff)
   21.74 +    by (auto simp: monoseq_iff incseq_Suc_iff strict_mono_Suc_iff)
   21.75  qed
   21.76  
   21.77  lemma seq_suble:
   21.78 -  assumes sf: "subseq f"
   21.79 +  assumes sf: "strict_mono (f :: nat \<Rightarrow> nat)"
   21.80    shows "n \<le> f n"
   21.81  proof (induct n)
   21.82    case 0
   21.83    show ?case by simp
   21.84  next
   21.85    case (Suc n)
   21.86 -  with sf [unfolded subseq_Suc_iff, rule_format, of n] have "n < f (Suc n)"
   21.87 +  with sf [unfolded strict_mono_Suc_iff, rule_format, of n] have "n < f (Suc n)"
   21.88       by arith
   21.89    then show ?case by arith
   21.90  qed
   21.91  
   21.92  lemma eventually_subseq:
   21.93 -  "subseq r \<Longrightarrow> eventually P sequentially \<Longrightarrow> eventually (\<lambda>n. P (r n)) sequentially"
   21.94 +  "strict_mono r \<Longrightarrow> eventually P sequentially \<Longrightarrow> eventually (\<lambda>n. P (r n)) sequentially"
   21.95    unfolding eventually_sequentially by (metis seq_suble le_trans)
   21.96  
   21.97  lemma not_eventually_sequentiallyD:
   21.98    assumes "\<not> eventually P sequentially"
   21.99 -  shows "\<exists>r. subseq r \<and> (\<forall>n. \<not> P (r n))"
  21.100 +  shows "\<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (\<forall>n. \<not> P (r n))"
  21.101  proof -
  21.102    from assms have "\<forall>n. \<exists>m\<ge>n. \<not> P m"
  21.103      unfolding eventually_sequentially by (simp add: not_less)
  21.104 @@ -1212,29 +1213,14 @@
  21.105      by (auto simp: choice_iff)
  21.106    then show ?thesis
  21.107      by (auto intro!: exI[of _ "\<lambda>n. r (((Suc \<circ> r) ^^ Suc n) 0)"]
  21.108 -             simp: less_eq_Suc_le subseq_Suc_iff)
  21.109 +             simp: less_eq_Suc_le strict_mono_Suc_iff)
  21.110  qed
  21.111  
  21.112 -lemma filterlim_subseq: "subseq f \<Longrightarrow> filterlim f sequentially sequentially"
  21.113 +lemma filterlim_subseq: "strict_mono f \<Longrightarrow> filterlim f sequentially sequentially"
  21.114    unfolding filterlim_iff by (metis eventually_subseq)
  21.115  
  21.116 -lemma subseq_o: "subseq r \<Longrightarrow> subseq s \<Longrightarrow> subseq (r \<circ> s)"
  21.117 -  unfolding subseq_def by simp
  21.118 -
  21.119 -lemma subseq_mono: "subseq r \<Longrightarrow> m < n \<Longrightarrow> r m < r n"
  21.120 -  by (auto simp: subseq_def)
  21.121 -
  21.122 -lemma subseq_imp_inj_on: "subseq g \<Longrightarrow> inj_on g A"
  21.123 -proof (rule inj_onI)
  21.124 -  assume g: "subseq g"
  21.125 -  fix x y
  21.126 -  assume "g x = g y"
  21.127 -  with subseq_mono[OF g, of x y] subseq_mono[OF g, of y x] show "x = y"
  21.128 -    by (cases x y rule: linorder_cases) simp_all
  21.129 -qed
  21.130 -
  21.131 -lemma subseq_strict_mono: "subseq g \<Longrightarrow> strict_mono g"
  21.132 -  by (intro strict_monoI subseq_mono[of g])
  21.133 +lemma strict_mono_o: "strict_mono r \<Longrightarrow> strict_mono s \<Longrightarrow> strict_mono (r \<circ> s)"
  21.134 +  unfolding strict_mono_def by simp
  21.135  
  21.136  lemma incseq_imp_monoseq:  "incseq X \<Longrightarrow> monoseq X"
  21.137    by (simp add: incseq_def monoseq_def)
  21.138 @@ -1324,10 +1310,10 @@
  21.139    for x :: "'a::linorder_topology"
  21.140    by (metis LIMSEQ_le_const LIMSEQ_le_const2 decseq_def incseq_def monoseq_iff)
  21.141  
  21.142 -lemma LIMSEQ_subseq_LIMSEQ: "X \<longlonglongrightarrow> L \<Longrightarrow> subseq f \<Longrightarrow> (X \<circ> f) \<longlonglongrightarrow> L"
  21.143 +lemma LIMSEQ_subseq_LIMSEQ: "X \<longlonglongrightarrow> L \<Longrightarrow> strict_mono f \<Longrightarrow> (X \<circ> f) \<longlonglongrightarrow> L"
  21.144    unfolding comp_def by (rule filterlim_compose [of X, OF _ filterlim_subseq])
  21.145  
  21.146 -lemma convergent_subseq_convergent: "convergent X \<Longrightarrow> subseq f \<Longrightarrow> convergent (X \<circ> f)"
  21.147 +lemma convergent_subseq_convergent: "convergent X \<Longrightarrow> strict_mono f \<Longrightarrow> convergent (X \<circ> f)"
  21.148    by (auto simp: convergent_def intro: LIMSEQ_subseq_LIMSEQ)
  21.149  
  21.150  lemma limI: "X \<longlonglongrightarrow> L \<Longrightarrow> lim X = L"
  21.151 @@ -1651,7 +1637,7 @@
  21.152        and "(\<lambda>n. X (s n)) \<longlonglongrightarrow> a"
  21.153        and "\<not> P (X (s n))"
  21.154        for n
  21.155 -      by (auto simp: subseq_Suc_iff Suc_le_eq incseq_Suc_iff
  21.156 +      by (auto simp: strict_mono_Suc_iff Suc_le_eq incseq_Suc_iff
  21.157            intro!: LIMSEQ_subseq_LIMSEQ[OF \<open>X \<longlonglongrightarrow> a\<close>, unfolded comp_def])
  21.158      from *[OF this(1,2,3,4)] this(5) show False
  21.159        by auto
  21.160 @@ -1700,7 +1686,7 @@
  21.161        and "(\<lambda>n. X (s n)) \<longlonglongrightarrow> a"
  21.162        and "\<not> P (X (s n))"
  21.163        for n
  21.164 -      by (auto simp: subseq_Suc_iff Suc_le_eq decseq_Suc_iff
  21.165 +      by (auto simp: strict_mono_Suc_iff Suc_le_eq decseq_Suc_iff
  21.166            intro!: LIMSEQ_subseq_LIMSEQ[OF \<open>X \<longlonglongrightarrow> a\<close>, unfolded comp_def])
  21.167      from *[OF this(1,2,3,4)] this(5) show False
  21.168        by auto
  21.169 @@ -3143,11 +3129,11 @@
  21.170    unfolding Cauchy_uniform filterlim_def by (intro nhds_imp_cauchy_filter)
  21.171  
  21.172  lemma Cauchy_subseq_Cauchy:
  21.173 -  assumes "Cauchy X" "subseq f"
  21.174 +  assumes "Cauchy X" "strict_mono f"
  21.175    shows "Cauchy (X \<circ> f)"
  21.176    unfolding Cauchy_uniform comp_def filtermap_filtermap[symmetric] cauchy_filter_def
  21.177    by (rule order_trans[OF _ \<open>Cauchy X\<close>[unfolded Cauchy_uniform cauchy_filter_def]])
  21.178 -     (intro prod_filter_mono filtermap_mono filterlim_subseq[OF \<open>subseq f\<close>, unfolded filterlim_def])
  21.179 +     (intro prod_filter_mono filtermap_mono filterlim_subseq[OF \<open>strict_mono f\<close>, unfolded filterlim_def])
  21.180  
  21.181  lemma convergent_Cauchy: "convergent X \<Longrightarrow> Cauchy X"
  21.182    unfolding convergent_def by (erule exE, erule LIMSEQ_imp_Cauchy)