# HG changeset patch
# User eberlm <eberlm@in.tum.de>
# Date 1502974376 -7200
# Node ID a1f5c5c26fa676b2f7e8bb9f3def7f459830b9ec
# Parent  407de076812651abf429562f3bbf8e434927d64c
Replaced subseq with strict_mono

diff -r 407de0768126 -r a1f5c5c26fa6 src/HOL/Analysis/Bochner_Integration.thy
--- a/src/HOL/Analysis/Bochner_Integration.thy	Thu Aug 17 14:40:42 2017 +0200
+++ b/src/HOL/Analysis/Bochner_Integration.thy	Thu Aug 17 14:52:56 2017 +0200
@@ -2128,7 +2128,7 @@
   fixes u :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::{banach, second_countable_topology}"
   assumes [measurable]: "\<And>n. integrable M (u n)"
       and "(\<lambda>n. (\<integral>x. norm(u n x) \<partial>M)) \<longlonglongrightarrow> 0"
-  shows "\<exists>r. subseq r \<and> (AE x in M. (\<lambda>n. u (r n) x) \<longlonglongrightarrow> 0)"
+  shows "\<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (AE x in M. (\<lambda>n. u (r n) x) \<longlonglongrightarrow> 0)"
 proof -
   {
     fix k
@@ -2140,13 +2140,13 @@
   }
   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))"
     by (intro dependent_nat_choice, auto)
-  then obtain r0 where r0: "subseq r0" "\<And>n. (\<integral>x. norm(u (r0 (Suc n)) x) \<partial>M) < (1/2)^(r0 n)"
-    by (auto simp: subseq_Suc_iff)
+  then obtain r0 where r0: "strict_mono r0" "\<And>n. (\<integral>x. norm(u (r0 (Suc n)) x) \<partial>M) < (1/2)^(r0 n)"
+    by (auto simp: strict_mono_Suc_iff)
   define r where "r = (\<lambda>n. r0(n+1))"
-  have "subseq r" unfolding r_def using r0(1) by (simp add: subseq_Suc_iff)
+  have "strict_mono r" unfolding r_def using r0(1) by (simp add: strict_mono_Suc_iff)
   have I: "(\<integral>\<^sup>+x. norm(u (r n) x) \<partial>M) < ennreal((1/2)^n)" for n
   proof -
-    have "r0 n \<ge> n" using \<open>subseq r0\<close> by (simp add: seq_suble)
+    have "r0 n \<ge> n" using \<open>strict_mono r0\<close> by (simp add: seq_suble)
     have "(1/2::real)^(r0 n) \<le> (1/2)^n" by (rule power_decreasing[OF \<open>r0 n \<ge> n\<close>], auto)
     then have "(\<integral>x. norm(u (r0 (Suc n)) x) \<partial>M) < (1/2)^n" using r0(2) less_le_trans by auto
     then have "(\<integral>x. norm(u (r n) x) \<partial>M) < (1/2)^n" unfolding r_def by auto
@@ -2219,7 +2219,7 @@
       by (simp add: tendsto_norm_zero_iff)
   }
   ultimately have "AE x in M. (\<lambda>n. u (r n) x) \<longlonglongrightarrow> 0" by auto
-  then show ?thesis using \<open>subseq r\<close> by auto
+  then show ?thesis using \<open>strict_mono r\<close> by auto
 qed
 
 subsection \<open>Restricted measure spaces\<close>
diff -r 407de0768126 -r a1f5c5c26fa6 src/HOL/Analysis/Bounded_Linear_Function.thy
--- a/src/HOL/Analysis/Bounded_Linear_Function.thy	Thu Aug 17 14:40:42 2017 +0200
+++ b/src/HOL/Analysis/Bounded_Linear_Function.thy	Thu Aug 17 14:52:56 2017 +0200
@@ -476,8 +476,8 @@
 lemma compact_blinfun_lemma:
   fixes f :: "nat \<Rightarrow> 'a::euclidean_space \<Rightarrow>\<^sub>L 'b::euclidean_space"
   assumes "bounded (range f)"
-  shows "\<forall>d\<subseteq>Basis. \<exists>l::'a \<Rightarrow>\<^sub>L 'b. \<exists> r.
-    subseq r \<and> (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) i) (l i) < e) sequentially)"
+  shows "\<forall>d\<subseteq>Basis. \<exists>l::'a \<Rightarrow>\<^sub>L 'b. \<exists> r::nat\<Rightarrow>nat.
+    strict_mono r \<and> (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) i) (l i) < e) sequentially)"
   by (rule compact_lemma_general[where unproj = "\<lambda>e. blinfun_of_matrix (\<lambda>i j. e j \<bullet> i)"])
    (auto intro!: euclidean_eqI[where 'a='b] bounded_linear_image assms
     simp: blinfun_of_matrix_works blinfun_of_matrix_apply inner_Basis mult_if_delta sum.delta'
@@ -501,7 +501,7 @@
 proof
   fix f :: "nat \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
   assume f: "bounded (range f)"
-  then obtain l::"'a \<Rightarrow>\<^sub>L 'b" and r where r: "subseq r"
+  then obtain l::"'a \<Rightarrow>\<^sub>L 'b" and r where r: "strict_mono r"
     and l: "\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>Basis. dist (f (r n) i) (l i) < e) sequentially"
     using compact_blinfun_lemma [OF f] by blast
   {
@@ -545,7 +545,7 @@
   }
   then have *: "((f \<circ> r) \<longlongrightarrow> l) sequentially"
     unfolding o_def tendsto_iff by simp
-  with r show "\<exists>l r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
+  with r show "\<exists>l r. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
     by auto
 qed
 
diff -r 407de0768126 -r a1f5c5c26fa6 src/HOL/Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Thu Aug 17 14:40:42 2017 +0200
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Thu Aug 17 14:52:56 2017 +0200
@@ -957,7 +957,7 @@
 lemma compact_lemma_cart:
   fixes f :: "nat \<Rightarrow> 'a::heine_borel ^ 'n"
   assumes f: "bounded (range f)"
-  shows "\<exists>l r. subseq r \<and>
+  shows "\<exists>l r. strict_mono r \<and>
         (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) $ i) (l $ i) < e) sequentially)"
     (is "?th d")
 proof -
@@ -971,7 +971,7 @@
 proof
   fix f :: "nat \<Rightarrow> 'a ^ 'b"
   assume f: "bounded (range f)"
-  then obtain l r where r: "subseq r"
+  then obtain l r where r: "strict_mono r"
       and l: "\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>UNIV. dist (f (r n) $ i) (l $ i) < e) sequentially"
     using compact_lemma_cart [OF f] by blast
   let ?d = "UNIV::'b set"
@@ -993,7 +993,7 @@
       by (rule eventually_mono)
   }
   hence "((f \<circ> r) \<longlongrightarrow> l) sequentially" unfolding o_def tendsto_iff by simp
-  with r show "\<exists>l r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially" by auto
+  with r show "\<exists>l r. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially" by auto
 qed
 
 lemma interval_cart:
diff -r 407de0768126 -r a1f5c5c26fa6 src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Thu Aug 17 14:40:42 2017 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Thu Aug 17 14:52:56 2017 +0200
@@ -2420,7 +2420,7 @@
                intro!: mult_pos_pos divide_pos_pos always_eventually)
     thus "summable (\<lambda>n. g n * u^n)"
       by (subst summable_mono_reindex[of "\<lambda>n. 2*n+1", symmetric])
-         (auto simp: power_mult subseq_def g_def h_def elim!: oddE)
+         (auto simp: power_mult strict_mono_def g_def h_def elim!: oddE)
   qed (simp add: h_def)
 
   have "\<exists>c. \<forall>u\<in>ball 0 1. Arctan u - G u = c"
@@ -2436,7 +2436,7 @@
       by (intro ext) (simp_all del: of_nat_Suc add: g_def diffs_def power_mult_distrib)
     also have "suminf \<dots> = (\<Sum>n. (-(u^2))^n)"
       by (subst suminf_mono_reindex[of "\<lambda>n. 2*n", symmetric])
-         (auto elim!: evenE simp: subseq_def power_mult power_mult_distrib)
+         (auto elim!: evenE simp: strict_mono_def power_mult power_mult_distrib)
     also from u have "norm u^2 < 1^2" by (intro power_strict_mono) simp_all
     hence "(\<Sum>n. (-(u^2))^n) = inverse (1 + u^2)"
       by (subst suminf_geometric) (simp_all add: norm_power inverse_eq_divide)
@@ -2450,7 +2450,7 @@
   with c z have "Arctan z = G z" by simp
   with summable[OF z] show "(\<lambda>n. g n * z^n) sums Arctan z" unfolding G_def by (simp add: sums_iff)
   thus "h z sums Arctan z" by (subst (asm) sums_mono_reindex[of "\<lambda>n. 2*n+1", symmetric])
-                              (auto elim!: oddE simp: subseq_def power_mult g_def h_def)
+                              (auto elim!: oddE simp: strict_mono_def power_mult g_def h_def)
 qed
 
 text \<open>A quickly-converging series for the logarithm, based on the arctangent.\<close>
diff -r 407de0768126 -r a1f5c5c26fa6 src/HOL/Analysis/Gamma_Function.thy
--- a/src/HOL/Analysis/Gamma_Function.thy	Thu Aug 17 14:40:42 2017 +0200
+++ b/src/HOL/Analysis/Gamma_Function.thy	Thu Aug 17 14:52:56 2017 +0200
@@ -101,7 +101,7 @@
   also have "(\<lambda>n. sin_coeff n *\<^sub>R z^n) sums sin z \<longleftrightarrow>
                  (\<lambda>n. ((-1)^n / fact (2*n+1)) *\<^sub>R z^(2*n+1)) sums sin z"
     by (subst sums_mono_reindex[of "\<lambda>n. 2*n+1", symmetric])
-       (auto simp: sin_coeff_def subseq_def ac_simps elim!: oddE)
+       (auto simp: sin_coeff_def strict_mono_def ac_simps elim!: oddE)
   finally show ?thesis .
 qed
 
@@ -111,7 +111,7 @@
   also have "(\<lambda>n. cos_coeff n *\<^sub>R z^n) sums cos z \<longleftrightarrow>
                  (\<lambda>n. ((-1)^n / fact (2*n)) *\<^sub>R z^(2*n)) sums cos z"
     by (subst sums_mono_reindex[of "\<lambda>n. 2*n", symmetric])
-       (auto simp: cos_coeff_def subseq_def ac_simps elim!: evenE)
+       (auto simp: cos_coeff_def strict_mono_def ac_simps elim!: evenE)
   finally show ?thesis .
 qed
 
@@ -2038,7 +2038,7 @@
     hence "?g \<longlonglongrightarrow> ?powr 2 (2*z) * Gamma z * Gamma (z+1/2) / Gamma (2*z)"
       using LIMSEQ_subseq_LIMSEQ[OF Gamma_series'_LIMSEQ, of "op*2" "2*z"]
       by (intro tendsto_intros Gamma_series'_LIMSEQ)
-         (simp_all add: o_def subseq_def Gamma_eq_zero_iff)
+         (simp_all add: o_def strict_mono_def Gamma_eq_zero_iff)
     ultimately have "?h \<longlonglongrightarrow> ?powr 2 (2*z) * Gamma z * Gamma (z+1/2) / Gamma (2*z)"
       by (rule Lim_transform_eventually)
   } note lim = this
diff -r 407de0768126 -r a1f5c5c26fa6 src/HOL/Analysis/Great_Picard.thy
--- a/src/HOL/Analysis/Great_Picard.thy	Thu Aug 17 14:40:42 2017 +0200
+++ b/src/HOL/Analysis/Great_Picard.thy	Thu Aug 17 14:52:56 2017 +0200
@@ -618,22 +618,22 @@
 
 lemma subsequence_diagonalization_lemma:
   fixes P :: "nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> bool"
-  assumes sub: "\<And>i r. \<exists>k. subseq k \<and> P i (r \<circ> k)"
+  assumes sub: "\<And>i r. \<exists>k. strict_mono (k :: nat \<Rightarrow> nat) \<and> P i (r \<circ> k)"
       and P_P:  "\<And>i r::nat \<Rightarrow> 'a. \<And>k1 k2 N.
                    \<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)"
-   obtains k where "subseq k" "\<And>i. P i (r \<circ> k)"
+   obtains k where "strict_mono (k :: nat \<Rightarrow> nat)" "\<And>i. P i (r \<circ> k)"
 proof -
-  obtain kk where "\<And>i r. subseq (kk i r) \<and> P i (r \<circ> (kk i r))"
+  obtain kk where "\<And>i r. strict_mono (kk i r :: nat \<Rightarrow> nat) \<and> P i (r \<circ> (kk i r))"
     using sub by metis
-  then have sub_kk: "\<And>i r. subseq (kk i r)" and P_kk: "\<And>i r. P i (r \<circ> (kk i r))"
+  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))"
     by auto
   define rr where "rr \<equiv> rec_nat (kk 0 r) (\<lambda>n x. x \<circ> kk (Suc n) (r \<circ> x))"
   then have [simp]: "rr 0 = kk 0 r" "\<And>n. rr(Suc n) = rr n \<circ> kk (Suc n) (r \<circ> rr n)"
     by auto
   show thesis
   proof
-    have sub_rr: "subseq (rr i)" for i
-      using sub_kk  by (induction i) (auto simp: subseq_def o_def)
+    have sub_rr: "strict_mono (rr i)" for i
+      using sub_kk  by (induction i) (auto simp: strict_mono_def o_def)
     have P_rr: "P i (r \<circ> rr i)" for i
       using P_kk  by (induction i) (auto simp: o_def)
     have "i \<le> i+d \<Longrightarrow> rr i n \<le> rr (i+d) n" for d i n
@@ -643,13 +643,13 @@
     next
       case (Suc d) then show ?case
         apply simp
-          using seq_suble [OF sub_kk] order_trans subseq_le_mono [OF sub_rr] by blast
+          using seq_suble [OF sub_kk] order_trans strict_mono_less_eq [OF sub_rr] by blast
     qed
     then have "\<And>i j n. i \<le> j \<Longrightarrow> rr i n \<le> rr j n"
       by (metis le_iff_add)
-    show "subseq (\<lambda>n. rr n n)"
-      apply (simp add: subseq_Suc_iff)
-      by (meson Suc_le_eq seq_suble sub_kk sub_rr subseq_mono)
+    show "strict_mono (\<lambda>n. rr n n)"
+      apply (simp add: strict_mono_Suc_iff)
+      by (meson lessI less_le_trans seq_suble strict_monoD sub_kk sub_rr)
     have "\<exists>j. i \<le> j \<and> rr (n+d) i = rr n j" for d n i
       apply (induction d arbitrary: i, auto)
       by (meson order_trans seq_suble sub_kk)
@@ -663,19 +663,19 @@
 lemma function_convergent_subsequence:
   fixes f :: "[nat,'a] \<Rightarrow> 'b::{real_normed_vector,heine_borel}"
   assumes "countable S" and M: "\<And>n::nat. \<And>x. x \<in> S \<Longrightarrow> norm(f n x) \<le> M"
-   obtains k where "subseq k" "\<And>x. x \<in> S \<Longrightarrow> \<exists>l. (\<lambda>n. f (k n) x) \<longlonglongrightarrow> l"
+   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"
 proof (cases "S = {}")
   case True
   then show ?thesis
-    using subseq_id that by fastforce
+    using strict_mono_id that by fastforce
 next
   case False
   with \<open>countable S\<close> obtain \<sigma> :: "nat \<Rightarrow> 'a" where \<sigma>: "S = range \<sigma>"
     using uncountable_def by blast
-  obtain k where "subseq k" and k: "\<And>i. \<exists>l. (\<lambda>n. (f \<circ> k) n (\<sigma> i)) \<longlonglongrightarrow> l"
+  obtain k where "strict_mono k" and k: "\<And>i. \<exists>l. (\<lambda>n. (f \<circ> k) n (\<sigma> i)) \<longlonglongrightarrow> l"
   proof (rule subsequence_diagonalization_lemma
       [of "\<lambda>i r. \<exists>l. ((\<lambda>n. (f \<circ> r) n (\<sigma> i)) \<longlongrightarrow> l) sequentially" id])
-    show "\<exists>k. subseq k \<and> (\<exists>l. (\<lambda>n. (f \<circ> (r \<circ> k)) n (\<sigma> i)) \<longlonglongrightarrow> l)" for i r
+    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
     proof -
       have "f (r n) (\<sigma> i) \<in> cball 0 M" for n
         by (simp add: \<sigma> M)
@@ -705,7 +705,7 @@
       and equicont:
           "\<And>x e. \<lbrakk>x \<in> S; 0 < e\<rbrakk>
                  \<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)"
-  obtains g k where "continuous_on S g" "subseq k"
+  obtains g k where "continuous_on S g" "strict_mono (k :: nat \<Rightarrow> nat)"
                     "\<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"
 proof -
   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)"
@@ -727,7 +727,7 @@
   moreover
   obtain R where "countable R" "R \<subseteq> S" and SR: "S \<subseteq> closure R"
     by (metis separable that)
-  obtain k where "subseq k" and k: "\<And>x. x \<in> R \<Longrightarrow> \<exists>l. (\<lambda>n. \<F> (k n) x) \<longlonglongrightarrow> l"
+  obtain k where "strict_mono k" and k: "\<And>x. x \<in> R \<Longrightarrow> \<exists>l. (\<lambda>n. \<F> (k n) x) \<longlonglongrightarrow> l"
     apply (rule function_convergent_subsequence [OF \<open>countable R\<close> M])
     using \<open>R \<subseteq> S\<close> apply force+
     done
@@ -783,7 +783,7 @@
     apply (simp add: o_def dist_norm)
     by meson
   ultimately show thesis
-    by (metis that \<open>subseq k\<close>)
+    by (metis that \<open>strict_mono k\<close>)
 qed
 
 
@@ -802,7 +802,7 @@
       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"
       and rng_f: "range \<F> \<subseteq> \<H>"
   obtains g r
-    where "g holomorphic_on S" "subseq r"
+    where "g holomorphic_on S" "strict_mono (r :: nat \<Rightarrow> nat)"
           "\<And>x. x \<in> S \<Longrightarrow> ((\<lambda>n. \<F> (r n) x) \<longlongrightarrow> g x) sequentially"
           "\<And>K. \<lbrakk>compact K; K \<subseteq> S\<rbrakk> \<Longrightarrow> uniform_limit K (\<F> \<circ> r) g sequentially"        
 proof -
@@ -813,10 +813,10 @@
     by (simp add: bounded)
   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"
     by metis
-  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)"
+  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)"
         if "\<And>n. \<F> n \<in> \<H>" for \<F> i
   proof -
-    obtain g k where "continuous_on (K i) g" "subseq k"
+    obtain g k where "continuous_on (K i) g" "strict_mono (k::nat\<Rightarrow>nat)"
                     "\<And>e. 0 < e \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. \<forall>x \<in> K i. norm(\<F>(k n) x - g x) < e"
     proof (rule Arzela_Ascoli [of "K i" "\<F>" "B i"])
       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"
@@ -925,13 +925,13 @@
     then show ?thesis
       by fastforce
   qed
-  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)"
+  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)"
          for i r
     apply (rule *)
     using rng_f by auto
-  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)"
+  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)"
     by (force simp: o_assoc)
-  obtain k where "subseq k"
+  obtain k :: "nat \<Rightarrow> nat" where "strict_mono k"
              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"
     apply (rule subsequence_diagonalization_lemma [OF **, of id])
      apply (erule ex_forward all_forward imp_forward)+
@@ -988,7 +988,7 @@
         with d show ?thesis by blast
       qed
     qed
-  qed (auto simp: \<open>subseq k\<close>)
+  qed (auto simp: \<open>strict_mono k\<close>)
 qed
 
 
@@ -1332,7 +1332,7 @@
         using hol\<G> \<G>not0 \<G>not1 \<G>_le1 by (force simp: W_def)+
       then obtain e where "e > 0" and e: "ball v e \<subseteq> Z"
         by (meson open_contains_ball)
-      obtain h j where holh: "h holomorphic_on ball v e" and "subseq j"
+      obtain h j where holh: "h holomorphic_on ball v e" and "strict_mono j"
                    and lim:  "\<And>x. x \<in> ball v e \<Longrightarrow> (\<lambda>n. \<G> (j n) x) \<longlonglongrightarrow> h x"
                    and ulim: "\<And>K. \<lbrakk>compact K; K \<subseteq> ball v e\<rbrakk>
                                   \<Longrightarrow> uniform_limit K (\<G> \<circ> j) h sequentially"
@@ -1347,7 +1347,7 @@
         show "(\<lambda>n. \<G> (j n) v) \<longlonglongrightarrow> h v"
           using \<open>e > 0\<close> lim by simp
         have lt_Fj: "real x \<le> cmod (\<F> (j x) v)" for x
-          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)
+          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)
         show "(\<lambda>n. \<G> (j n) v) \<longlonglongrightarrow> 0"
         proof (rule Lim_null_comparison [OF eventually_sequentiallyI seq_harmonic])
           show "cmod (\<G> (j x) v) \<le> inverse (real x)" if "1 \<le> x" for x
@@ -1428,8 +1428,8 @@
   qed
   with that show ?thesis by metis
 qed
-    
-  
+
+
 lemma GPicard4:
   assumes "0 < k" and holf: "f holomorphic_on (ball 0 k - {0})" 
       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)"
@@ -1500,7 +1500,8 @@
   then show ?thesis
   proof cases
     case 1
-    with infinite_enumerate obtain r where "subseq r" and r: "\<And>n. r n \<in> {n. norm(h n w) \<le> 1}"
+    with infinite_enumerate obtain r :: "nat \<Rightarrow> nat" 
+      where "strict_mono r" and r: "\<And>n. r n \<in> {n. norm(h n w) \<le> 1}"
       by blast
     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"
     proof (rule GPicard3 [OF _ _ w, where K = "sphere 0 (1/2)"])  
@@ -1529,7 +1530,7 @@
       obtain n where "(1/e - 2) / 2 < real n"
         using reals_Archimedean2 by blast
       also have "... \<le> r n"
-        using \<open>subseq r\<close> by (simp add: seq_suble)
+        using \<open>strict_mono r\<close> by (simp add: seq_suble)
       finally have "(1/e - 2) / 2 < real (r n)" .
       with \<open>0 < e\<close> have e: "e > 1 / (2 + 2 * real (r n))"
         by (simp add: field_simps)
@@ -1546,7 +1547,8 @@
       using \<epsilon> by auto 
   next
     case 2
-    with infinite_enumerate obtain r where "subseq r" and r: "\<And>n. r n \<in> {n. norm(h n w) \<ge> 1}"
+    with infinite_enumerate obtain r :: "nat \<Rightarrow> nat" 
+      where "strict_mono r" and r: "\<And>n. r n \<in> {n. norm(h n w) \<ge> 1}"
       by blast
     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"
     proof (rule GPicard3 [OF _ _ w, where K = "sphere 0 (1/2)"])  
@@ -1579,7 +1581,7 @@
       obtain n where "(1/e - 2) / 2 < real n"
         using reals_Archimedean2 by blast
       also have "... \<le> r n"
-        using \<open>subseq r\<close> by (simp add: seq_suble)
+        using \<open>strict_mono r\<close> by (simp add: seq_suble)
       finally have "(1/e - 2) / 2 < real (r n)" .
       with \<open>0 < e\<close> have e: "e > 1 / (2 + 2 * real (r n))"
         by (simp add: field_simps)
diff -r 407de0768126 -r a1f5c5c26fa6 src/HOL/Analysis/Harmonic_Numbers.thy
--- a/src/HOL/Analysis/Harmonic_Numbers.thy	Thu Aug 17 14:40:42 2017 +0200
+++ b/src/HOL/Analysis/Harmonic_Numbers.thy	Thu Aug 17 14:52:56 2017 +0200
@@ -215,7 +215,7 @@
   moreover have "(\<lambda>n. ?em (2*n) - ?em n + ln (2::real))
                      \<longlonglongrightarrow> euler_mascheroni - euler_mascheroni + ln 2"
     by (intro tendsto_intros euler_mascheroni_LIMSEQ filterlim_compose[OF euler_mascheroni_LIMSEQ]
-              filterlim_subseq) (auto simp: subseq_def)
+              filterlim_subseq) (auto simp: strict_mono_def)
   hence "(\<lambda>n. ?em (2*n) - ?em n + ln (2::real)) \<longlonglongrightarrow> ln 2" by simp
   ultimately have "(\<lambda>n. (\<Sum>k<2*n. (-1)^k / real_of_nat (Suc k))) \<longlonglongrightarrow> ln 2"
     by (rule Lim_transform_eventually)
@@ -227,7 +227,7 @@
     by (simp add: summable_sums_iff divide_inverse sums_def)
   from filterlim_compose[OF this filterlim_subseq[of "op * (2::nat)"]]
     have "(\<lambda>n. \<Sum>k<2*n. (-1)^k / real_of_nat (Suc k)) \<longlonglongrightarrow> (\<Sum>k. (-1)^k / real_of_nat (Suc k))"
-    by (simp add: subseq_def)
+    by (simp add: strict_mono_def)
   ultimately have "(\<Sum>k. (- 1) ^ k / real_of_nat (Suc k)) = ln 2" by (intro LIMSEQ_unique)
   with A show ?thesis by (simp add: sums_def)
 qed
diff -r 407de0768126 -r a1f5c5c26fa6 src/HOL/Analysis/Linear_Algebra.thy
--- a/src/HOL/Analysis/Linear_Algebra.thy	Thu Aug 17 14:40:42 2017 +0200
+++ b/src/HOL/Analysis/Linear_Algebra.thy	Thu Aug 17 14:52:56 2017 +0200
@@ -1757,8 +1757,8 @@
 
 lemma infinite_enumerate:
   assumes fS: "infinite S"
-  shows "\<exists>r. subseq r \<and> (\<forall>n. r n \<in> S)"
-  unfolding subseq_def
+  shows "\<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (\<forall>n. r n \<in> S)"
+  unfolding strict_mono_def
   using enumerate_in_set[OF fS] enumerate_mono[of _ _ S] fS by auto
 
 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)"
diff -r 407de0768126 -r a1f5c5c26fa6 src/HOL/Analysis/Path_Connected.thy
--- a/src/HOL/Analysis/Path_Connected.thy	Thu Aug 17 14:40:42 2017 +0200
+++ b/src/HOL/Analysis/Path_Connected.thy	Thu Aug 17 14:52:56 2017 +0200
@@ -3305,7 +3305,8 @@
     then have "\<And>n. \<exists>x \<in> S. \<xi> n = f x" by force
     then obtain z where zs: "\<And>n. z n \<in> S" and fz: "\<And>n. \<xi> n = f (z n)"
       by metis
-    then obtain y K where y: "y \<in> closure S" and "subseq K" and Klim: "(z \<circ> K) \<longlonglongrightarrow> y"
+    then obtain y K where y: "y \<in> closure S" and "strict_mono (K :: nat \<Rightarrow> nat)" 
+                      and Klim: "(z \<circ> K) \<longlonglongrightarrow> y"
       using \<open>bounded S\<close>
       apply (simp add: compact_closure [symmetric] compact_def)
       apply (drule_tac x=z in spec)
diff -r 407de0768126 -r a1f5c5c26fa6 src/HOL/Analysis/Set_Integral.thy
--- a/src/HOL/Analysis/Set_Integral.thy	Thu Aug 17 14:40:42 2017 +0200
+++ b/src/HOL/Analysis/Set_Integral.thy	Thu Aug 17 14:52:56 2017 +0200
@@ -193,22 +193,22 @@
 
 lemma limsup_subseq_lim:
   fixes u::"nat \<Rightarrow> 'a :: {complete_linorder, linorder_topology}"
-  shows "\<exists>r. subseq r \<and> (u o r) \<longlonglongrightarrow> limsup u"
+  shows "\<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (u o r) \<longlonglongrightarrow> limsup u"
 proof (cases)
   assume "\<forall>n. \<exists>p>n. \<forall>m\<ge>p. u m \<le> u p"
   then have "\<exists>r. \<forall>n. (\<forall>m\<ge>r n. u m \<le> u (r n)) \<and> r n < r (Suc n)"
     by (intro dependent_nat_choice) (auto simp: conj_commute)
-  then obtain r where "subseq r" and mono: "\<And>n m. r n \<le> m \<Longrightarrow> u m \<le> u (r n)"
-    by (auto simp: subseq_Suc_iff)
+  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)"
+    by (auto simp: strict_mono_Suc_iff)
   define umax where "umax = (\<lambda>n. (SUP m:{n..}. u m))"
   have "decseq umax" unfolding umax_def by (simp add: SUP_subset_mono antimono_def)
   then have "umax \<longlonglongrightarrow> limsup u" unfolding umax_def by (metis LIMSEQ_INF limsup_INF_SUP)
-  then have *: "(umax o r) \<longlonglongrightarrow> limsup u" by (simp add: LIMSEQ_subseq_LIMSEQ \<open>subseq r\<close>)
+  then have *: "(umax o r) \<longlonglongrightarrow> limsup u" by (simp add: LIMSEQ_subseq_LIMSEQ \<open>strict_mono r\<close>)
   have "\<And>n. umax(r n) = u(r n)" unfolding umax_def using mono
     by (metis SUP_le_iff antisym atLeast_def mem_Collect_eq order_refl)
   then have "umax o r = u o r" unfolding o_def by simp
   then have "(u o r) \<longlonglongrightarrow> limsup u" using * by simp
-  then show ?thesis using \<open>subseq r\<close> by blast
+  then show ?thesis using \<open>strict_mono r\<close> by blast
 next
   assume "\<not> (\<forall>n. \<exists>p>n. (\<forall>m\<ge>p. u m \<le> u p))"
   then obtain N where N: "\<And>p. p > N \<Longrightarrow> \<exists>m>p. u p < u m" by (force simp: not_le le_less)
@@ -262,16 +262,16 @@
     then show "\<exists>y>N. x < y \<and> (\<forall>i\<in>{N<..y}. u i \<le> u y)" by auto
   qed (auto)
   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
-  have "subseq r" using r by (auto simp: subseq_Suc_iff)
+  have "strict_mono r" using r by (auto simp: strict_mono_Suc_iff)
   have "incseq (u o r)" unfolding o_def using r by (simp add: incseq_SucI order.strict_implies_order)
   then have "(u o r) \<longlonglongrightarrow> (SUP n. (u o r) n)" using LIMSEQ_SUP by blast
   then have "limsup (u o r) = (SUP n. (u o r) n)" by (simp add: lim_imp_Limsup)
-  moreover have "limsup (u o r) \<le> limsup u" using \<open>subseq r\<close> by (simp add: limsup_subseq_mono)
+  moreover have "limsup (u o r) \<le> limsup u" using \<open>strict_mono r\<close> by (simp add: limsup_subseq_mono)
   ultimately have "(SUP n. (u o r) n) \<le> limsup u" by simp
 
   {
     fix i assume i: "i \<in> {N<..}"
-    obtain n where "i < r (Suc n)" using \<open>subseq r\<close> using Suc_le_eq seq_suble by blast
+    obtain n where "i < r (Suc n)" using \<open>strict_mono r\<close> using Suc_le_eq seq_suble by blast
     then have "i \<in> {N<..r(Suc n)}" using i by simp
     then have "u i \<le> u (r(Suc n))" using r by simp
     then have "u i \<le> (SUP n. (u o r) n)" unfolding o_def by (meson SUP_upper2 UNIV_I)
@@ -281,27 +281,27 @@
     by (metis (mono_tags, lifting) INF_lower2 atLeast_Suc_greaterThan atLeast_def eventually_ge_at_top mem_Collect_eq)
   then have "limsup u = (SUP n. (u o r) n)" using \<open>(SUP n. (u o r) n) \<le> limsup u\<close> by simp
   then have "(u o r) \<longlonglongrightarrow> limsup u" using \<open>(u o r) \<longlonglongrightarrow> (SUP n. (u o r) n)\<close> by simp
-  then show ?thesis using \<open>subseq r\<close> by auto
+  then show ?thesis using \<open>strict_mono r\<close> by auto
 qed
 
 lemma liminf_subseq_lim:
   fixes u::"nat \<Rightarrow> 'a :: {complete_linorder, linorder_topology}"
-  shows "\<exists>r. subseq r \<and> (u o r) \<longlonglongrightarrow> liminf u"
+  shows "\<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (u o r) \<longlonglongrightarrow> liminf u"
 proof (cases)
   assume "\<forall>n. \<exists>p>n. \<forall>m\<ge>p. u m \<ge> u p"
   then have "\<exists>r. \<forall>n. (\<forall>m\<ge>r n. u m \<ge> u (r n)) \<and> r n < r (Suc n)"
     by (intro dependent_nat_choice) (auto simp: conj_commute)
-  then obtain r where "subseq r" and mono: "\<And>n m. r n \<le> m \<Longrightarrow> u m \<ge> u (r n)"
-    by (auto simp: subseq_Suc_iff)
+  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)"
+    by (auto simp: strict_mono_Suc_iff)
   define umin where "umin = (\<lambda>n. (INF m:{n..}. u m))"
   have "incseq umin" unfolding umin_def by (simp add: INF_superset_mono incseq_def)
   then have "umin \<longlonglongrightarrow> liminf u" unfolding umin_def by (metis LIMSEQ_SUP liminf_SUP_INF)
-  then have *: "(umin o r) \<longlonglongrightarrow> liminf u" by (simp add: LIMSEQ_subseq_LIMSEQ \<open>subseq r\<close>)
+  then have *: "(umin o r) \<longlonglongrightarrow> liminf u" by (simp add: LIMSEQ_subseq_LIMSEQ \<open>strict_mono r\<close>)
   have "\<And>n. umin(r n) = u(r n)" unfolding umin_def using mono
     by (metis le_INF_iff antisym atLeast_def mem_Collect_eq order_refl)
   then have "umin o r = u o r" unfolding o_def by simp
   then have "(u o r) \<longlonglongrightarrow> liminf u" using * by simp
-  then show ?thesis using \<open>subseq r\<close> by blast
+  then show ?thesis using \<open>strict_mono r\<close> by blast
 next
   assume "\<not> (\<forall>n. \<exists>p>n. (\<forall>m\<ge>p. u m \<ge> u p))"
   then obtain N where N: "\<And>p. p > N \<Longrightarrow> \<exists>m>p. u p > u m" by (force simp: not_le le_less)
@@ -354,17 +354,18 @@
     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
     then show "\<exists>y>N. x < y \<and> (\<forall>i\<in>{N<..y}. u i \<ge> u y)" by auto
   qed (auto)
-  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
-  have "subseq r" using r by (auto simp: subseq_Suc_iff)
+  then obtain r :: "nat \<Rightarrow> nat" 
+    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
+  have "strict_mono r" using r by (auto simp: strict_mono_Suc_iff)
   have "decseq (u o r)" unfolding o_def using r by (simp add: decseq_SucI order.strict_implies_order)
   then have "(u o r) \<longlonglongrightarrow> (INF n. (u o r) n)" using LIMSEQ_INF by blast
   then have "liminf (u o r) = (INF n. (u o r) n)" by (simp add: lim_imp_Liminf)
-  moreover have "liminf (u o r) \<ge> liminf u" using \<open>subseq r\<close> by (simp add: liminf_subseq_mono)
+  moreover have "liminf (u o r) \<ge> liminf u" using \<open>strict_mono r\<close> by (simp add: liminf_subseq_mono)
   ultimately have "(INF n. (u o r) n) \<ge> liminf u" by simp
 
   {
     fix i assume i: "i \<in> {N<..}"
-    obtain n where "i < r (Suc n)" using \<open>subseq r\<close> using Suc_le_eq seq_suble by blast
+    obtain n where "i < r (Suc n)" using \<open>strict_mono r\<close> using Suc_le_eq seq_suble by blast
     then have "i \<in> {N<..r(Suc n)}" using i by simp
     then have "u i \<ge> u (r(Suc n))" using r by simp
     then have "u i \<ge> (INF n. (u o r) n)" unfolding o_def by (meson INF_lower2 UNIV_I)
@@ -374,7 +375,7 @@
     by (metis (mono_tags, lifting) SUP_upper2 atLeast_Suc_greaterThan atLeast_def eventually_ge_at_top mem_Collect_eq)
   then have "liminf u = (INF n. (u o r) n)" using \<open>(INF n. (u o r) n) \<ge> liminf u\<close> by simp
   then have "(u o r) \<longlonglongrightarrow> liminf u" using \<open>(u o r) \<longlonglongrightarrow> (INF n. (u o r) n)\<close> by simp
-  then show ?thesis using \<open>subseq r\<close> by auto
+  then show ?thesis using \<open>strict_mono r\<close> by auto
 qed
 
 
@@ -1076,12 +1077,12 @@
   then have "limsup u < \<infinity>" "limsup v < \<infinity>" by auto
 
   define w where "w = (\<lambda>n. u n + v n)"
-  obtain r where r: "subseq r" "(w o r) \<longlonglongrightarrow> limsup w" using limsup_subseq_lim by auto
-  obtain s where s: "subseq s" "(u o r o s) \<longlonglongrightarrow> limsup (u o r)" using limsup_subseq_lim by auto
-  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
+  obtain r where r: "strict_mono r" "(w o r) \<longlonglongrightarrow> limsup w" using limsup_subseq_lim by auto
+  obtain s where s: "strict_mono s" "(u o r o s) \<longlonglongrightarrow> limsup (u o r)" using limsup_subseq_lim by auto
+  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
 
   define a where "a = r o s o t"
-  have "subseq a" using r s t by (simp add: a_def subseq_o)
+  have "strict_mono a" using r s t by (simp add: a_def strict_mono_o)
   have l:"(w o a) \<longlonglongrightarrow> limsup w"
          "(u o a) \<longlonglongrightarrow> limsup (u o r)"
          "(v o a) \<longlonglongrightarrow> limsup (v o r o s)"
@@ -1092,7 +1093,8 @@
 
   have "limsup (u o r) \<le> limsup u" by (simp add: limsup_subseq_mono r(1))
   then have a: "limsup (u o r) \<noteq> \<infinity>" using \<open>limsup u < \<infinity>\<close> by auto
-  have "limsup (v o r o s) \<le> limsup v" by (simp add: comp_assoc limsup_subseq_mono r(1) s(1) subseq_o)
+  have "limsup (v o r o s) \<le> limsup v" 
+    by (simp add: comp_assoc limsup_subseq_mono r(1) s(1) strict_mono_o)
   then have b: "limsup (v o r o s) \<noteq> \<infinity>" using \<open>limsup v < \<infinity>\<close> by auto
 
   have "(\<lambda>n. (u o a) n + (v o a) n) \<longlonglongrightarrow> limsup (u o r) + limsup (v o r o s)"
@@ -1122,12 +1124,12 @@
   then have "liminf u > -\<infinity>" "liminf v > -\<infinity>" by auto
 
   define w where "w = (\<lambda>n. u n + v n)"
-  obtain r where r: "subseq r" "(w o r) \<longlonglongrightarrow> liminf w" using liminf_subseq_lim by auto
-  obtain s where s: "subseq s" "(u o r o s) \<longlonglongrightarrow> liminf (u o r)" using liminf_subseq_lim by auto
-  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
+  obtain r where r: "strict_mono r" "(w o r) \<longlonglongrightarrow> liminf w" using liminf_subseq_lim by auto
+  obtain s where s: "strict_mono s" "(u o r o s) \<longlonglongrightarrow> liminf (u o r)" using liminf_subseq_lim by auto
+  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
 
   define a where "a = r o s o t"
-  have "subseq a" using r s t by (simp add: a_def subseq_o)
+  have "strict_mono a" using r s t by (simp add: a_def strict_mono_o)
   have l:"(w o a) \<longlonglongrightarrow> liminf w"
          "(u o a) \<longlonglongrightarrow> liminf (u o r)"
          "(v o a) \<longlonglongrightarrow> liminf (v o r o s)"
@@ -1138,7 +1140,8 @@
 
   have "liminf (u o r) \<ge> liminf u" by (simp add: liminf_subseq_mono r(1))
   then have a: "liminf (u o r) \<noteq> -\<infinity>" using \<open>liminf u > -\<infinity>\<close> by auto
-  have "liminf (v o r o s) \<ge> liminf v" by (simp add: comp_assoc liminf_subseq_mono r(1) s(1) subseq_o)
+  have "liminf (v o r o s) \<ge> liminf v" 
+    by (simp add: comp_assoc liminf_subseq_mono r(1) s(1) strict_mono_o)
   then have b: "liminf (v o r o s) \<noteq> -\<infinity>" using \<open>liminf v > -\<infinity>\<close> by auto
 
   have "(\<lambda>n. (u o a) n + (v o a) n) \<longlonglongrightarrow> liminf (u o r) + liminf (v o r o s)"
@@ -1188,7 +1191,7 @@
   shows "limsup (\<lambda>n. u n * v n) = a * limsup v"
 proof -
   define w where "w = (\<lambda>n. u n * v n)"
-  obtain r where r: "subseq r" "(v o r) \<longlonglongrightarrow> limsup v" using limsup_subseq_lim by auto
+  obtain r where r: "strict_mono r" "(v o r) \<longlonglongrightarrow> limsup v" using limsup_subseq_lim by auto
   have "(u o r) \<longlonglongrightarrow> a" using assms(1) LIMSEQ_subseq_LIMSEQ r by auto
   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
   moreover have "\<And>n. (w o r) n = (u o r) n * (v o r) n" unfolding w_def by auto
@@ -1196,7 +1199,7 @@
   then have "limsup (w o r) = a * limsup v" by (simp add: tendsto_iff_Liminf_eq_Limsup)
   then have I: "limsup w \<ge> a * limsup v" by (metis limsup_subseq_mono r(1))
 
-  obtain s where s: "subseq s" "(w o s) \<longlonglongrightarrow> limsup w" using limsup_subseq_lim by auto
+  obtain s where s: "strict_mono s" "(w o s) \<longlonglongrightarrow> limsup w" using limsup_subseq_lim by auto
   have *: "(u o s) \<longlonglongrightarrow> a" using assms(1) LIMSEQ_subseq_LIMSEQ s by auto
   have "eventually (\<lambda>n. (u o s) n > 0) sequentially" using assms(2) * order_tendsto_iff by blast
   moreover have "eventually (\<lambda>n. (u o s) n < \<infinity>) sequentially" using assms(3) * order_tendsto_iff by blast
@@ -1218,7 +1221,7 @@
   shows "liminf (\<lambda>n. u n * v n) = a * liminf v"
 proof -
   define w where "w = (\<lambda>n. u n * v n)"
-  obtain r where r: "subseq r" "(v o r) \<longlonglongrightarrow> liminf v" using liminf_subseq_lim by auto
+  obtain r where r: "strict_mono r" "(v o r) \<longlonglongrightarrow> liminf v" using liminf_subseq_lim by auto
   have "(u o r) \<longlonglongrightarrow> a" using assms(1) LIMSEQ_subseq_LIMSEQ r by auto
   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
   moreover have "\<And>n. (w o r) n = (u o r) n * (v o r) n" unfolding w_def by auto
@@ -1226,7 +1229,7 @@
   then have "liminf (w o r) = a * liminf v" by (simp add: tendsto_iff_Liminf_eq_Limsup)
   then have I: "liminf w \<le> a * liminf v" by (metis liminf_subseq_mono r(1))
 
-  obtain s where s: "subseq s" "(w o s) \<longlonglongrightarrow> liminf w" using liminf_subseq_lim by auto
+  obtain s where s: "strict_mono s" "(w o s) \<longlonglongrightarrow> liminf w" using liminf_subseq_lim by auto
   have *: "(u o s) \<longlonglongrightarrow> a" using assms(1) LIMSEQ_subseq_LIMSEQ s by auto
   have "eventually (\<lambda>n. (u o s) n > 0) sequentially" using assms(2) * order_tendsto_iff by blast
   moreover have "eventually (\<lambda>n. (u o s) n < \<infinity>) sequentially" using assms(3) * order_tendsto_iff by blast
@@ -1286,12 +1289,12 @@
   then have "limsup v < \<infinity>" "liminf u < \<infinity>" by auto
 
   define w where "w = (\<lambda>n. u n + v n)"
-  obtain r where r: "subseq r" "(u o r) \<longlonglongrightarrow> liminf u" using liminf_subseq_lim by auto
-  obtain s where s: "subseq s" "(w o r o s) \<longlonglongrightarrow> liminf (w o r)" using liminf_subseq_lim by auto
-  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
+  obtain r where r: "strict_mono r" "(u o r) \<longlonglongrightarrow> liminf u" using liminf_subseq_lim by auto
+  obtain s where s: "strict_mono s" "(w o r o s) \<longlonglongrightarrow> liminf (w o r)" using liminf_subseq_lim by auto
+  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
 
   define a where "a = r o s o t"
-  have "subseq a" using r s t by (simp add: a_def subseq_o)
+  have "strict_mono a" using r s t by (simp add: a_def strict_mono_o)
   have l:"(u o a) \<longlonglongrightarrow> liminf u"
          "(w o a) \<longlonglongrightarrow> liminf (w o r)"
          "(v o a) \<longlonglongrightarrow> limsup (v o r o s)"
@@ -1301,7 +1304,8 @@
   done
 
   have "liminf (w o r) \<ge> liminf w" by (simp add: liminf_subseq_mono r(1))
-  have "limsup (v o r o s) \<le> limsup v" by (simp add: comp_assoc limsup_subseq_mono r(1) s(1) subseq_o)
+  have "limsup (v o r o s) \<le> limsup v" 
+    by (simp add: comp_assoc limsup_subseq_mono r(1) s(1) strict_mono_o)
   then have b: "limsup (v o r o s) < \<infinity>" using \<open>limsup v < \<infinity>\<close> by auto
 
   have "(\<lambda>n. (u o a) n + (v o a) n) \<longlonglongrightarrow> liminf u + limsup (v o r o s)"
diff -r 407de0768126 -r a1f5c5c26fa6 src/HOL/Analysis/Summation_Tests.thy
--- a/src/HOL/Analysis/Summation_Tests.thy	Thu Aug 17 14:40:42 2017 +0200
+++ b/src/HOL/Analysis/Summation_Tests.thy	Thu Aug 17 14:52:56 2017 +0200
@@ -189,7 +189,7 @@
   also have "\<dots> \<longleftrightarrow> Bseq (\<lambda>n. \<Sum>k=1..<n. f k)" unfolding f'_def by simp
   also have "\<dots> \<longleftrightarrow> Bseq (\<lambda>n. \<Sum>k=1..<2^n. f k)"
     by (rule nonneg_incseq_Bseq_subseq_iff[symmetric])
-       (auto intro!: sum_nonneg incseq_SucI nonneg simp: subseq_def)
+       (auto intro!: sum_nonneg incseq_SucI nonneg simp: strict_mono_def)
   also have "\<dots> \<longleftrightarrow> Bseq (\<lambda>n. \<Sum>k<n. 2^k * f (2^k))"
   proof (intro iffI)
     assume A: "Bseq (\<lambda>n. \<Sum>k=1..<2^n. f k)"
diff -r 407de0768126 -r a1f5c5c26fa6 src/HOL/Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Thu Aug 17 14:40:42 2017 +0200
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Thu Aug 17 14:52:56 2017 +0200
@@ -4468,7 +4468,7 @@
 lemma acc_point_range_imp_convergent_subsequence:
   fixes l :: "'a :: first_countable_topology"
   assumes l: "\<forall>U. l\<in>U \<longrightarrow> open U \<longrightarrow> infinite (U \<inter> range f)"
-  shows "\<exists>r. subseq r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
+  shows "\<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
 proof -
   from countable_basis_at_decseq[of l]
   obtain A where A:
@@ -4492,8 +4492,8 @@
   }
   note s = this
   define r where "r = rec_nat (s 0 0) s"
-  have "subseq r"
-    by (auto simp: r_def s subseq_Suc_iff)
+  have "strict_mono r"
+    by (auto simp: r_def s strict_mono_Suc_iff)
   moreover
   have "(\<lambda>n. f (r n)) \<longlonglongrightarrow> l"
   proof (rule topological_tendstoI)
@@ -4513,7 +4513,7 @@
     ultimately show "eventually (\<lambda>i. f (r i) \<in> S) sequentially"
       by eventually_elim auto
   qed
-  ultimately show "\<exists>r. subseq r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
+  ultimately show "\<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
     by (auto simp: convergent_def comp_def)
 qed
 
@@ -4616,7 +4616,7 @@
 lemma islimpt_range_imp_convergent_subsequence:
   fixes l :: "'a :: {t1_space, first_countable_topology}"
   assumes l: "l islimpt (range f)"
-  shows "\<exists>r. subseq r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
+  shows "\<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
   using l unfolding islimpt_eq_acc_point
   by (rule acc_point_range_imp_convergent_subsequence)
 
@@ -4949,16 +4949,16 @@
 
 definition seq_compact :: "'a::topological_space set \<Rightarrow> bool"
   where "seq_compact S \<longleftrightarrow>
-    (\<forall>f. (\<forall>n. f n \<in> S) \<longrightarrow> (\<exists>l\<in>S. \<exists>r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially))"
+    (\<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))"
 
 lemma seq_compactI:
-  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"
+  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"
   shows "seq_compact S"
   unfolding seq_compact_def using assms by fast
 
 lemma seq_compactE:
   assumes "seq_compact S" "\<forall>n. f n \<in> S"
-  obtains l r where "l \<in> S" "subseq r" "((f \<circ> r) \<longlongrightarrow> l) sequentially"
+  obtains l r where "l \<in> S" "strict_mono (r :: nat \<Rightarrow> nat)" "((f \<circ> r) \<longlongrightarrow> l) sequentially"
   using assms unfolding seq_compact_def by fast
 
 lemma closed_sequentially: (* TODO: move upwards *)
@@ -4980,13 +4980,13 @@
   hence "\<forall>n. f n \<in> s" and "\<forall>n. f n \<in> t"
     by simp_all
   from \<open>seq_compact s\<close> and \<open>\<forall>n. f n \<in> s\<close>
-  obtain l r where "l \<in> s" and r: "subseq r" and l: "(f \<circ> r) \<longlonglongrightarrow> l"
+  obtain l r where "l \<in> s" and r: "strict_mono r" and l: "(f \<circ> r) \<longlonglongrightarrow> l"
     by (rule seq_compactE)
   from \<open>\<forall>n. f n \<in> t\<close> have "\<forall>n. (f \<circ> r) n \<in> t"
     by simp
   from \<open>closed t\<close> and this and l have "l \<in> t"
     by (rule closed_sequentially)
-  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"
+  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"
     by fast
 qed
 
@@ -5002,7 +5002,7 @@
 proof (safe intro!: countably_compactI)
   fix A
   assume A: "\<forall>a\<in>A. open a" "U \<subseteq> \<Union>A" "countable A"
-  have subseq: "\<And>X. range X \<subseteq> U \<Longrightarrow> \<exists>r x. x \<in> U \<and> subseq r \<and> (X \<circ> r) \<longlonglongrightarrow> x"
+  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"
     using \<open>seq_compact U\<close> by (fastforce simp: seq_compact_def subset_eq)
   show "\<exists>T\<subseteq>A. finite T \<and> U \<subseteq> \<Union>T"
   proof cases
@@ -5023,7 +5023,7 @@
         using \<open>A \<noteq> {}\<close> unfolding X_def by (intro T) (auto intro: from_nat_into)
       then have "range X \<subseteq> U"
         by auto
-      with subseq[of X] obtain r x where "x \<in> U" and r: "subseq r" "(X \<circ> r) \<longlonglongrightarrow> x"
+      with subseq[of X] obtain r x where "x \<in> U" and r: "strict_mono r" "(X \<circ> r) \<longlonglongrightarrow> x"
         by auto
       from \<open>x\<in>U\<close> \<open>U \<subseteq> \<Union>A\<close> from_nat_into_surj[OF \<open>countable A\<close>]
       obtain n where "x \<in> from_nat_into A n" by auto
@@ -5034,7 +5034,7 @@
         by (auto simp: eventually_sequentially)
       moreover from X have "\<And>i. n \<le> r i \<Longrightarrow> X (r i) \<notin> from_nat_into A n"
         by auto
-      moreover from \<open>subseq r\<close>[THEN seq_suble, of "max n N"] have "\<exists>i. n \<le> r i \<and> N \<le> i"
+      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"
         by (auto intro!: exI[of _ "max n N"])
       ultimately show False
         by auto
@@ -5087,8 +5087,8 @@
   }
   note s = this
   define r where "r = rec_nat (s 0 0) s"
-  have "subseq r"
-    by (auto simp: r_def s subseq_Suc_iff)
+  have "strict_mono r"
+    by (auto simp: r_def s strict_mono_Suc_iff)
   moreover
   have "(\<lambda>n. X (r n)) \<longlonglongrightarrow> x"
   proof (rule topological_tendstoI)
@@ -5108,7 +5108,7 @@
     ultimately show "eventually (\<lambda>i. X (r i) \<in> S) sequentially"
       by eventually_elim auto
   qed
-  ultimately show "\<exists>x \<in> U. \<exists>r. subseq r \<and> (X \<circ> r) \<longlonglongrightarrow> x"
+  ultimately show "\<exists>x \<in> U. \<exists>r. strict_mono r \<and> (X \<circ> r) \<longlonglongrightarrow> x"
     using \<open>x \<in> U\<close> by (auto simp: convergent_def comp_def)
 qed
 
@@ -5159,25 +5159,25 @@
   {
     fix f :: "nat \<Rightarrow> 'a"
     assume f: "\<forall>n. f n \<in> s"
-    have "\<exists>l\<in>s. \<exists>r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
+    have "\<exists>l\<in>s. \<exists>r. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
     proof (cases "finite (range f)")
       case True
       obtain l where "infinite {n. f n = f l}"
         using pigeonhole_infinite[OF _ True] by auto
-      then obtain r where "subseq r" and fr: "\<forall>n. f (r n) = f l"
+      then obtain r :: "nat \<Rightarrow> nat" where "strict_mono  r" and fr: "\<forall>n. f (r n) = f l"
         using infinite_enumerate by blast
-      then have "subseq r \<and> (f \<circ> r) \<longlonglongrightarrow> f l"
+      then have "strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> f l"
         by (simp add: fr o_def)
-      with f show "\<exists>l\<in>s. \<exists>r. subseq r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
+      with f show "\<exists>l\<in>s. \<exists>r. strict_mono  r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
         by auto
     next
       case False
       with f assms have "\<exists>x\<in>s. \<forall>U. x\<in>U \<and> open U \<longrightarrow> infinite (U \<inter> range f)"
         by auto
       then obtain l where "l \<in> s" "\<forall>U. l\<in>U \<and> open U \<longrightarrow> infinite (U \<inter> range f)" ..
-      from this(2) have "\<exists>r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
+      from this(2) have "\<exists>r. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
         using acc_point_range_imp_convergent_subsequence[of l f] by auto
-      with \<open>l \<in> s\<close> show "\<exists>l\<in>s. \<exists>r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially" ..
+      with \<open>l \<in> s\<close> show "\<exists>l\<in>s. \<exists>r. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially" ..
     qed
   }
   then show ?thesis
@@ -5237,14 +5237,14 @@
     qed simp
     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)"
       by blast
-    then obtain l r where "l \<in> s" and r:"subseq r" and "((x \<circ> r) \<longlongrightarrow> l) sequentially"
+    then obtain l r where "l \<in> s" and r:"strict_mono  r" and "((x \<circ> r) \<longlongrightarrow> l) sequentially"
       using assms by (metis seq_compact_def)
     from this(3) have "Cauchy (x \<circ> r)"
       using LIMSEQ_imp_Cauchy by auto
     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"
       unfolding cauchy_def using \<open>e > 0\<close> by blast
     then have False
-      using x[of "r N" "r (N+1)"] r by (auto simp: subseq_def) }
+      using x[of "r N" "r (N+1)"] r by (auto simp: strict_mono_def) }
   then show ?thesis
     by metis
 qed
@@ -5302,7 +5302,7 @@
 
 lemma compact_def: \<comment>\<open>this is the definition of compactness in HOL Light\<close>
   "compact (S :: 'a::metric_space set) \<longleftrightarrow>
-   (\<forall>f. (\<forall>n. f n \<in> S) \<longrightarrow> (\<exists>l\<in>S. \<exists>r. subseq r \<and> (f \<circ> r) \<longlonglongrightarrow> l))"
+   (\<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))"
   unfolding compact_eq_seq_compact_metric seq_compact_def by auto
 
 subsubsection \<open>Complete the chain of compactness variants\<close>
@@ -5335,7 +5335,7 @@
 
 class heine_borel = metric_space +
   assumes bounded_imp_convergent_subsequence:
-    "bounded (range f) \<Longrightarrow> \<exists>l r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
+    "bounded (range f) \<Longrightarrow> \<exists>l r. strict_mono (r::nat\<Rightarrow>nat) \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
 
 lemma bounded_closed_imp_seq_compact:
   fixes s::"'a::heine_borel set"
@@ -5347,13 +5347,13 @@
   assume f: "\<forall>n. f n \<in> s"
   with \<open>bounded s\<close> have "bounded (range f)"
     by (auto intro: bounded_subset)
-  obtain l r where r: "subseq r" and l: "((f \<circ> r) \<longlongrightarrow> l) sequentially"
+  obtain l r where r: "strict_mono (r :: nat \<Rightarrow> nat)" and l: "((f \<circ> r) \<longlongrightarrow> l) sequentially"
     using bounded_imp_convergent_subsequence [OF \<open>bounded (range f)\<close>] by auto
   from f have fr: "\<forall>n. (f \<circ> r) n \<in> s"
     by simp
   have "l \<in> s" using \<open>closed s\<close> fr l
     by (rule closed_sequentially)
-  show "\<exists>l\<in>s. \<exists>r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
+  show "\<exists>l\<in>s. \<exists>r. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
     using \<open>l \<in> s\<close> r l by blast
 qed
 
@@ -5393,11 +5393,11 @@
 proof
   fix f :: "nat \<Rightarrow> real"
   assume f: "bounded (range f)"
-  obtain r where r: "subseq r" "monoseq (f \<circ> r)"
+  obtain r :: "nat \<Rightarrow> nat" where r: "strict_mono r" "monoseq (f \<circ> r)"
     unfolding comp_def by (metis seq_monosub)
   then have "Bseq (f \<circ> r)"
     unfolding Bseq_eq_bounded using f by (force intro: bounded_subset)
-  with r show "\<exists>l r. subseq r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
+  with r show "\<exists>l r. strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
     using Bseq_monoseq_convergent[of "f \<circ> r"] by (auto simp: convergent_def)
 qed
 
@@ -5409,19 +5409,19 @@
   assumes bounded_proj: "\<And>k. k \<in> basis \<Longrightarrow> bounded ((\<lambda>x. x proj k) ` range f)"
   assumes proj_unproj: "\<And>e k. k \<in> basis \<Longrightarrow> (unproj e) proj k = e k"
   assumes unproj_proj: "\<And>x. unproj (\<lambda>k. x proj k) = x"
-  shows "\<forall>d\<subseteq>basis. \<exists>l::'a. \<exists> r.
-    subseq r \<and> (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) proj i) (l proj i) < e) sequentially)"
+  shows "\<forall>d\<subseteq>basis. \<exists>l::'a. \<exists> r::nat\<Rightarrow>nat.
+    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)"
 proof safe
   fix d :: "'b set"
   assume d: "d \<subseteq> basis"
   with finite_basis have "finite d"
     by (blast intro: finite_subset)
-  from this d show "\<exists>l::'a. \<exists>r. subseq r \<and>
+  from this d show "\<exists>l::'a. \<exists>r::nat\<Rightarrow>nat. 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)"
   proof (induct d)
     case empty
     then show ?case
-      unfolding subseq_def by auto
+      unfolding strict_mono_def by auto
   next
     case (insert k d)
     have k[intro]: "k \<in> basis"
@@ -5429,19 +5429,19 @@
     have s': "bounded ((\<lambda>x. x proj k) ` range f)"
       using k
       by (rule bounded_proj)
-    obtain l1::"'a" and r1 where r1: "subseq r1"
+    obtain l1::"'a" and r1 where r1: "strict_mono r1"
       and lr1: "\<forall>e > 0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) proj i) (l1 proj i) < e) sequentially"
       using insert(3) using insert(4) by auto
     have f': "\<forall>n. f (r1 n) proj k \<in> (\<lambda>x. x proj k) ` range f"
       by simp
     have "bounded (range (\<lambda>i. f (r1 i) proj k))"
       by (metis (lifting) bounded_subset f' image_subsetI s')
-    then obtain l2 r2 where r2:"subseq r2" and lr2:"((\<lambda>i. f (r1 (r2 i)) proj k) \<longlongrightarrow> l2) sequentially"
+    then obtain l2 r2 where r2:"strict_mono r2" and lr2:"((\<lambda>i. f (r1 (r2 i)) proj k) \<longlongrightarrow> l2) sequentially"
       using bounded_imp_convergent_subsequence[of "\<lambda>i. f (r1 i) proj k"]
       by (auto simp: o_def)
     define r where "r = r1 \<circ> r2"
-    have r:"subseq r"
-      using r1 and r2 unfolding r_def o_def subseq_def by auto
+    have r:"strict_mono r"
+      using r1 and r2 unfolding r_def o_def strict_mono_def by auto
     moreover
     define l where "l = unproj (\<lambda>i. if i = k then l2 else l1 proj i)"
     {
@@ -5465,7 +5465,7 @@
   fixes f :: "nat \<Rightarrow> 'a::euclidean_space"
   assumes "bounded (range f)"
   shows "\<forall>d\<subseteq>Basis. \<exists>l::'a. \<exists> r.
-    subseq r \<and> (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially)"
+    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)"
   by (rule compact_lemma_general[where unproj="\<lambda>e. \<Sum>i\<in>Basis. e i *\<^sub>R i"])
      (auto intro!: assms bounded_linear_inner_left bounded_linear_image
        simp: euclidean_representation)
@@ -5474,7 +5474,7 @@
 proof
   fix f :: "nat \<Rightarrow> 'a"
   assume f: "bounded (range f)"
-  then obtain l::'a and r where r: "subseq r"
+  then obtain l::'a and r where r: "strict_mono r"
     and l: "\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially"
     using compact_lemma [OF f] by blast
   {
@@ -5505,7 +5505,7 @@
   }
   then have *: "((f \<circ> r) \<longlongrightarrow> l) sequentially"
     unfolding o_def tendsto_iff by simp
-  with r show "\<exists>l r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
+  with r show "\<exists>l r. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
     by auto
 qed
 
@@ -5525,20 +5525,20 @@
     by (rule bounded_fst)
   then have s1: "bounded (range (fst \<circ> f))"
     by (simp add: image_comp)
-  obtain l1 r1 where r1: "subseq r1" and l1: "(\<lambda>n. fst (f (r1 n))) \<longlonglongrightarrow> l1"
+  obtain l1 r1 where r1: "strict_mono r1" and l1: "(\<lambda>n. fst (f (r1 n))) \<longlonglongrightarrow> l1"
     using bounded_imp_convergent_subsequence [OF s1] unfolding o_def by fast
   from f have s2: "bounded (range (snd \<circ> f \<circ> r1))"
     by (auto simp add: image_comp intro: bounded_snd bounded_subset)
-  obtain l2 r2 where r2: "subseq r2" and l2: "((\<lambda>n. snd (f (r1 (r2 n)))) \<longlongrightarrow> l2) sequentially"
+  obtain l2 r2 where r2: "strict_mono r2" and l2: "((\<lambda>n. snd (f (r1 (r2 n)))) \<longlongrightarrow> l2) sequentially"
     using bounded_imp_convergent_subsequence [OF s2]
     unfolding o_def by fast
   have l1': "((\<lambda>n. fst (f (r1 (r2 n)))) \<longlongrightarrow> l1) sequentially"
     using LIMSEQ_subseq_LIMSEQ [OF l1 r2] unfolding o_def .
   have l: "((f \<circ> (r1 \<circ> r2)) \<longlongrightarrow> (l1, l2)) sequentially"
     using tendsto_Pair [OF l1' l2] unfolding o_def by simp
-  have r: "subseq (r1 \<circ> r2)"
-    using r1 r2 unfolding subseq_def by simp
-  show "\<exists>l r. subseq r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
+  have r: "strict_mono (r1 \<circ> r2)"
+    using r1 r2 unfolding strict_mono_def by simp
+  show "\<exists>l r. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
     using l r by fast
 qed
 
@@ -5641,7 +5641,7 @@
   {
     fix f
     assume as: "(\<forall>n::nat. f n \<in> s)" "Cauchy f"
-    from as(1) obtain l r where lr: "l\<in>s" "subseq r" "(f \<circ> r) \<longlonglongrightarrow> l"
+    from as(1) obtain l r where lr: "l\<in>s" "strict_mono r" "(f \<circ> r) \<longlonglongrightarrow> l"
       using assms unfolding compact_def by blast
 
     note lr' = seq_suble [OF lr(2)]
@@ -5752,8 +5752,8 @@
       qed
 
       define t where "t = rec_nat (sel 0 0) (\<lambda>n i. sel (Suc n) i)"
-      have "subseq t"
-        unfolding subseq_Suc_iff by (simp add: t_def sel)
+      have "strict_mono t"
+        unfolding strict_mono_Suc_iff by (simp add: t_def sel)
       moreover have "\<forall>i. (f \<circ> t) i \<in> s"
         using f by auto
       moreover
@@ -5777,7 +5777,7 @@
           by (simp add: dist_commute)
       qed
 
-      ultimately show "\<exists>l\<in>s. \<exists>r. subseq r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
+      ultimately show "\<exists>l\<in>s. \<exists>r. strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
         using assms unfolding complete_def by blast
     qed
   qed
@@ -5974,7 +5974,7 @@
     using choice[of "\<lambda>n x. x \<in> s n"] by auto
   from assms(4,1) have "seq_compact (s 0)"
     by (simp add: bounded_closed_imp_seq_compact)
-  then obtain l r where lr: "l \<in> s 0" "subseq r" "(x \<circ> r) \<longlonglongrightarrow> l"
+  then obtain l r where lr: "l \<in> s 0" "strict_mono r" "(x \<circ> r) \<longlonglongrightarrow> l"
     using x and assms(3) unfolding seq_compact_def by blast
   have "\<forall>n. l \<in> s n"
   proof
@@ -7670,7 +7670,7 @@
       using neg by simp
     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"
       by metis
-    then obtain l r where "l \<in> S" "subseq r" and to_l: "(f \<circ> r) \<longlonglongrightarrow> l"
+    then obtain l r where "l \<in> S" "strict_mono r" and to_l: "(f \<circ> r) \<longlonglongrightarrow> l"
       using \<open>compact S\<close> compact_def that by metis
     then obtain G where "l \<in> G" "G \<in> \<G>"
       using Ssub by auto
@@ -7687,7 +7687,7 @@
       by simp
     also have "... \<le> 1 / real (Suc (max N1 N2))"
       apply (simp add: divide_simps del: max.bounded_iff)
-      using \<open>subseq r\<close> seq_suble by blast
+      using \<open>strict_mono r\<close> seq_suble by blast
     also have "... \<le> 1 / real (Suc N2)"
       by (simp add: field_simps)
     also have "... < e/2"
@@ -7851,7 +7851,7 @@
   apply (clarify, rename_tac l2 r2)
   apply (rule_tac x="(l1, l2)" in rev_bexI, simp)
   apply (rule_tac x="r1 \<circ> r2" in exI)
-  apply (rule conjI, simp add: subseq_def)
+  apply (rule conjI, simp add: strict_mono_def)
   apply (drule_tac f=r2 in LIMSEQ_subseq_LIMSEQ, assumption)
   apply (drule (1) tendsto_Pair) back
   apply (simp add: o_def)
@@ -8287,7 +8287,7 @@
     assume as: "\<forall>n. x n \<in> ?S"  "(x \<longlongrightarrow> l) sequentially"
     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"
       using choice[of "\<lambda>n y. x n = (fst y) + (snd y) \<and> fst y \<in> S \<and> snd y \<in> T"] by auto
-    obtain l' r where "l'\<in>S" and r: "subseq r" and lr: "(((\<lambda>n. fst (f n)) \<circ> r) \<longlongrightarrow> l') sequentially"
+    obtain l' r where "l'\<in>S" and r: "strict_mono r" and lr: "(((\<lambda>n. fst (f n)) \<circ> r) \<longlongrightarrow> l') sequentially"
       using assms(1)[unfolded compact_def, THEN spec[where x="\<lambda> n. fst (f n)"]] using f(2) by auto
     have "((\<lambda>n. snd (f (r n))) \<longlongrightarrow> l - l') sequentially"
       using tendsto_diff[OF LIMSEQ_subseq_LIMSEQ[OF as(2) r] lr] and f(1)
diff -r 407de0768126 -r a1f5c5c26fa6 src/HOL/Computational_Algebra/Fundamental_Theorem_Algebra.thy
--- a/src/HOL/Computational_Algebra/Fundamental_Theorem_Algebra.thy	Thu Aug 17 14:40:42 2017 +0200
+++ b/src/HOL/Computational_Algebra/Fundamental_Theorem_Algebra.thy	Thu Aug 17 14:52:56 2017 +0200
@@ -236,13 +236,13 @@
 
 lemma bolzano_weierstrass_complex_disc:
   assumes r: "\<forall>n. cmod (s n) \<le> r"
-  shows "\<exists>f z. subseq f \<and> (\<forall>e >0. \<exists>N. \<forall>n \<ge> N. cmod (s (f n) - z) < e)"
+  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)"
 proof -
   from seq_monosub[of "Re \<circ> s"]
-  obtain f where f: "subseq f" "monoseq (\<lambda>n. Re (s (f n)))"
+  obtain f where f: "strict_mono f" "monoseq (\<lambda>n. Re (s (f n)))"
     unfolding o_def by blast
   from seq_monosub[of "Im \<circ> s \<circ> f"]
-  obtain g where g: "subseq g" "monoseq (\<lambda>n. Im (s (f (g n))))"
+  obtain g where g: "strict_mono g" "monoseq (\<lambda>n. Im (s (f (g n))))"
     unfolding o_def by blast
   let ?h = "f \<circ> g"
   from r[rule_format, of 0] have rp: "r \<ge> 0"
@@ -284,8 +284,8 @@
   then have y: "\<forall>r>0. \<exists>n0. \<forall>n\<ge>n0. \<bar>Im (s (f (g n))) - y\<bar> < r"
     unfolding LIMSEQ_iff real_norm_def .
   let ?w = "Complex x y"
-  from f(1) g(1) have hs: "subseq ?h"
-    unfolding subseq_def by auto
+  from f(1) g(1) have hs: "strict_mono ?h"
+    unfolding strict_mono_def by auto
   have "\<exists>N. \<forall>n\<ge>N. cmod (s (?h n) - ?w) < e" if "e > 0" for e
   proof -
     from that have e2: "e/2 > 0"
@@ -400,7 +400,7 @@
         g: "\<forall>n. cmod (g n) \<le> r" "\<forall>n. cmod (poly p (g n)) <?m + 1 /real(Suc n)"
       by blast
     from bolzano_weierstrass_complex_disc[OF g(1)]
-    obtain f z where fz: "subseq f" "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. cmod (g (f n) - z) < e"
+    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"
       by blast
     {
       fix w
diff -r 407de0768126 -r a1f5c5c26fa6 src/HOL/Library/Diagonal_Subsequence.thy
--- a/src/HOL/Library/Diagonal_Subsequence.thy	Thu Aug 17 14:40:42 2017 +0200
+++ b/src/HOL/Library/Diagonal_Subsequence.thy	Thu Aug 17 14:52:56 2017 +0200
@@ -8,28 +8,28 @@
 
 locale subseqs =
   fixes P::"nat\<Rightarrow>(nat\<Rightarrow>nat)\<Rightarrow>bool"
-  assumes ex_subseq: "\<And>n s. subseq s \<Longrightarrow> \<exists>r'. subseq r' \<and> P n (s o r')"
+  assumes ex_subseq: "\<And>n s. strict_mono (s::nat\<Rightarrow>nat) \<Longrightarrow> \<exists>r'. strict_mono r' \<and> P n (s o r')"
 begin
 
-definition reduce where "reduce s n = (SOME r'. subseq r' \<and> P n (s o r'))"
+definition reduce where "reduce s n = (SOME r'::nat\<Rightarrow>nat. strict_mono r' \<and> P n (s o r'))"
 
 lemma subseq_reduce[intro, simp]:
-  "subseq s \<Longrightarrow> subseq (reduce s n)"
+  "strict_mono s \<Longrightarrow> strict_mono (reduce s n)"
   unfolding reduce_def by (rule someI2_ex[OF ex_subseq]) auto
 
 lemma reduce_holds:
-  "subseq s \<Longrightarrow> P n (s o reduce s n)"
+  "strict_mono s \<Longrightarrow> P n (s o reduce s n)"
   unfolding reduce_def by (rule someI2_ex[OF ex_subseq]) (auto simp: o_def)
 
-primrec seqseq where
+primrec seqseq :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
   "seqseq 0 = id"
 | "seqseq (Suc n) = seqseq n o reduce (seqseq n) n"
 
-lemma subseq_seqseq[intro, simp]: "subseq (seqseq n)"
+lemma subseq_seqseq[intro, simp]: "strict_mono (seqseq n)"
 proof (induct n)
-  case 0 thus ?case by (simp add: subseq_def)
+  case 0 thus ?case by (simp add: strict_mono_def)
 next
-  case (Suc n) thus ?case by (subst seqseq.simps) (auto intro!: subseq_o)
+  case (Suc n) thus ?case by (subst seqseq.simps) (auto intro!: strict_mono_o)
 qed
 
 lemma seqseq_holds:
@@ -40,35 +40,29 @@
   thus ?thesis by simp
 qed
 
-definition diagseq where "diagseq i = seqseq i i"
-
-lemma subseq_mono: "subseq f \<Longrightarrow> a \<le> b \<Longrightarrow> f a \<le> f b"
-  by (metis le_eq_less_or_eq subseq_mono)
-
-lemma subseq_strict_mono: "subseq f \<Longrightarrow> a < b \<Longrightarrow> f a < f b"
-  by (simp add: subseq_def)
+definition diagseq :: "nat \<Rightarrow> nat" where "diagseq i = seqseq i i"
 
 lemma diagseq_mono: "diagseq n < diagseq (Suc n)"
 proof -
   have "diagseq n < seqseq n (Suc n)"
-    using subseq_seqseq[of n] by (simp add: diagseq_def subseq_def)
+    using subseq_seqseq[of n] by (simp add: diagseq_def strict_mono_def)
   also have "\<dots> \<le> seqseq n (reduce (seqseq n) n (Suc n))"
-    by (auto intro: subseq_mono seq_suble)
+    using strict_mono_less_eq seq_suble by blast
   also have "\<dots> = diagseq (Suc n)" by (simp add: diagseq_def)
   finally show ?thesis .
 qed
 
-lemma subseq_diagseq: "subseq diagseq"
-  using diagseq_mono by (simp add: subseq_Suc_iff diagseq_def)
+lemma subseq_diagseq: "strict_mono diagseq"
+  using diagseq_mono by (simp add: strict_mono_Suc_iff diagseq_def)
 
 primrec fold_reduce where
   "fold_reduce n 0 = id"
 | "fold_reduce n (Suc k) = fold_reduce n k o reduce (seqseq (n + k)) (n + k)"
 
-lemma subseq_fold_reduce[intro, simp]: "subseq (fold_reduce n k)"
+lemma subseq_fold_reduce[intro, simp]: "strict_mono (fold_reduce n k)"
 proof (induct k)
-  case (Suc k) from subseq_o[OF this subseq_reduce] show ?case by (simp add: o_def)
-qed (simp add: subseq_def)
+  case (Suc k) from strict_mono_o[OF this subseq_reduce] show ?case by (simp add: o_def)
+qed (simp add: strict_mono_def)
 
 lemma ex_subseq_reduce_index: "seqseq (n + k) = seqseq n o fold_reduce n k"
   by (induct k) simp_all
@@ -95,14 +89,14 @@
   assumes "m \<le> n" shows "diagseq n = (seqseq m o (fold_reduce m (n - m))) n"
   using diagseq_add[of m "n - m"] assms by simp
 
-lemma subseq_diagonal_rest: "subseq (\<lambda>x. fold_reduce k x (k + x))"
-  unfolding subseq_Suc_iff fold_reduce.simps o_def
+lemma subseq_diagonal_rest: "strict_mono (\<lambda>x. fold_reduce k x (k + x))"
+  unfolding strict_mono_Suc_iff fold_reduce.simps o_def
 proof
   fix n
   have "fold_reduce k n (k + n) < fold_reduce k n (k + Suc n)" (is "?lhs < _")
-    by (auto intro: subseq_strict_mono)
+    by (auto intro: strict_monoD)
   also have "\<dots> \<le> fold_reduce k n (reduce (seqseq (k + n)) (k + n) (k + Suc n))"
-    by (rule subseq_mono) (auto intro!: seq_suble subseq_mono)
+    by (auto intro: less_mono_imp_le_mono seq_suble strict_monoD)
   finally show "?lhs < \<dots>" .
 qed
 
@@ -110,7 +104,7 @@
   by (auto simp: o_def diagseq_add)
 
 lemma diagseq_holds:
-  assumes subseq_stable: "\<And>r s n. subseq r \<Longrightarrow> P n s \<Longrightarrow> P n (s o r)"
+  assumes subseq_stable: "\<And>r s n. strict_mono r \<Longrightarrow> P n s \<Longrightarrow> P n (s o r)"
   shows "P k (diagseq o (op + (Suc k)))"
   unfolding diagseq_seqseq by (intro subseq_stable subseq_diagonal_rest seqseq_holds)
 
diff -r 407de0768126 -r a1f5c5c26fa6 src/HOL/Library/Liminf_Limsup.thy
--- a/src/HOL/Library/Liminf_Limsup.thy	Thu Aug 17 14:40:42 2017 +0200
+++ b/src/HOL/Library/Liminf_Limsup.thy	Thu Aug 17 14:52:56 2017 +0200
@@ -379,20 +379,20 @@
 
 lemma liminf_subseq_mono:
   fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
-  assumes "subseq r"
+  assumes "strict_mono r"
   shows "liminf X \<le> liminf (X \<circ> r) "
 proof-
   have "\<And>n. (INF m:{n..}. X m) \<le> (INF m:{n..}. (X \<circ> r) m)"
   proof (safe intro!: INF_mono)
     fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. X ma \<le> (X \<circ> r) m"
-      using seq_suble[OF \<open>subseq r\<close>, of m] by (intro bexI[of _ "r m"]) auto
+      using seq_suble[OF \<open>strict_mono r\<close>, of m] by (intro bexI[of _ "r m"]) auto
   qed
   then show ?thesis by (auto intro!: SUP_mono simp: liminf_SUP_INF comp_def)
 qed
 
 lemma limsup_subseq_mono:
   fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
-  assumes "subseq r"
+  assumes "strict_mono r"
   shows "limsup (X \<circ> r) \<le> limsup X"
 proof-
   have "(SUP m:{n..}. (X \<circ> r) m) \<le> (SUP m:{n..}. X m)" for n
@@ -400,7 +400,7 @@
     fix m :: nat
     assume "n \<le> m"
     then show "\<exists>ma\<in>{n..}. (X \<circ> r) m \<le> X ma"
-      using seq_suble[OF \<open>subseq r\<close>, of m] by (intro bexI[of _ "r m"]) auto
+      using seq_suble[OF \<open>strict_mono r\<close>, of m] by (intro bexI[of _ "r m"]) auto
   qed
   then show ?thesis
     by (auto intro!: INF_mono simp: limsup_INF_SUP comp_def)
@@ -587,9 +587,9 @@
 
 lemma compact_complete_linorder:
   fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
-  shows "\<exists>l r. subseq r \<and> (X \<circ> r) \<longlonglongrightarrow> l"
+  shows "\<exists>l r. strict_mono r \<and> (X \<circ> r) \<longlonglongrightarrow> l"
 proof -
-  obtain r where "subseq r" and mono: "monoseq (X \<circ> r)"
+  obtain r where "strict_mono r" and mono: "monoseq (X \<circ> r)"
     using seq_monosub[of X]
     unfolding comp_def
     by auto
@@ -599,7 +599,7 @@
      using lim_increasing_cl[of "X \<circ> r"] lim_decreasing_cl[of "X \<circ> r"]
      by auto
   then show ?thesis
-    using \<open>subseq r\<close> by auto
+    using \<open>strict_mono r\<close> by auto
 qed
 
 lemma tendsto_Limsup:
diff -r 407de0768126 -r a1f5c5c26fa6 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Thu Aug 17 14:40:42 2017 +0200
+++ b/src/HOL/Limits.thy	Thu Aug 17 14:52:56 2017 +0200
@@ -325,7 +325,7 @@
   using Bseq_offset[of f 1] by (auto intro: Bseq_subseq)
 
 lemma increasing_Bseq_subseq_iff:
-  assumes "\<And>x y. x \<le> y \<Longrightarrow> norm (f x :: 'a::real_normed_vector) \<le> norm (f y)" "subseq g"
+  assumes "\<And>x y. x \<le> y \<Longrightarrow> norm (f x :: 'a::real_normed_vector) \<le> norm (f y)" "strict_mono g"
   shows "Bseq (\<lambda>x. f (g x)) \<longleftrightarrow> Bseq f"
 proof
   assume "Bseq (\<lambda>x. f (g x))"
@@ -346,7 +346,7 @@
 lemma nonneg_incseq_Bseq_subseq_iff:
   fixes f :: "nat \<Rightarrow> real"
     and g :: "nat \<Rightarrow> nat"
-  assumes "\<And>x. f x \<ge> 0" "incseq f" "subseq g"
+  assumes "\<And>x. f x \<ge> 0" "incseq f" "strict_mono g"
   shows "Bseq (\<lambda>x. f (g x)) \<longleftrightarrow> Bseq f"
   using assms by (intro increasing_Bseq_subseq_iff) (auto simp: incseq_def)
 
@@ -1398,11 +1398,11 @@
 
 lemma mult_nat_left_at_top: "c > 0 \<Longrightarrow> filterlim (\<lambda>x. c * x) at_top sequentially"
   for c :: nat
-  by (rule filterlim_subseq) (auto simp: subseq_def)
+  by (rule filterlim_subseq) (auto simp: strict_mono_def)
 
 lemma mult_nat_right_at_top: "c > 0 \<Longrightarrow> filterlim (\<lambda>x. x * c) at_top sequentially"
   for c :: nat
-  by (rule filterlim_subseq) (auto simp: subseq_def)
+  by (rule filterlim_subseq) (auto simp: strict_mono_def)
 
 lemma at_to_infinity: "(at (0::'a::{real_normed_field,field})) = filtermap inverse at_infinity"
 proof (rule antisym)
diff -r 407de0768126 -r a1f5c5c26fa6 src/HOL/Probability/Helly_Selection.thy
--- a/src/HOL/Probability/Helly_Selection.thy	Thu Aug 17 14:40:42 2017 +0200
+++ b/src/HOL/Probability/Helly_Selection.thy	Thu Aug 17 14:52:56 2017 +0200
@@ -19,7 +19,7 @@
   assumes rcont: "\<And>n x. continuous (at_right x) (f n)"
   assumes mono: "\<And>n. mono (f n)"
   assumes bdd: "\<And>n x. \<bar>f n x\<bar> \<le> M"
-  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>
+  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>
     (\<forall>x. continuous (at x) F \<longrightarrow> (\<lambda>n. f (s n) x) \<longlonglongrightarrow> F x))"
 proof -
   obtain m :: "real \<Rightarrow> nat" where "bij_betw m \<rat> UNIV"
@@ -33,18 +33,18 @@
   let ?P = "\<lambda>n. \<lambda>s. convergent (\<lambda>k. f (s k) (r n))"
   interpret nat: subseqs ?P
   proof (unfold convergent_def, unfold subseqs_def, auto)
-    fix n :: nat and s :: "nat \<Rightarrow> nat" assume s: "subseq s"
+    fix n :: nat and s :: "nat \<Rightarrow> nat" assume s: "strict_mono s"
     have "bounded {-M..M}"
       using bounded_closed_interval by auto
     moreover have "\<And>k. f (s k) (r n) \<in> {-M..M}"
       using bdd by (simp add: abs_le_iff minus_le_iff)
-    ultimately have "\<exists>l s'. subseq s' \<and> ((\<lambda>k. f (s k) (r n)) \<circ> s') \<longlonglongrightarrow> l"
+    ultimately have "\<exists>l s'. strict_mono s' \<and> ((\<lambda>k. f (s k) (r n)) \<circ> s') \<longlonglongrightarrow> l"
       using compact_Icc compact_imp_seq_compact seq_compactE by metis
-    thus "\<exists>s'. subseq s' \<and> (\<exists>l. (\<lambda>k. f (s (s' k)) (r n)) \<longlonglongrightarrow> l)"
+    thus "\<exists>s'. strict_mono (s'::nat\<Rightarrow>nat) \<and> (\<exists>l. (\<lambda>k. f (s (s' k)) (r n)) \<longlonglongrightarrow> l)"
       by (auto simp: comp_def)
   qed
   define d where "d = nat.diagseq"
-  have subseq: "subseq d"
+  have subseq: "strict_mono d"
     unfolding d_def using nat.subseq_diagseq by auto
   have rat_cnv: "?P n d" for n
   proof -
@@ -157,8 +157,8 @@
 
 (* Can strengthen to equivalence. *)
 theorem tight_imp_convergent_subsubsequence:
-  assumes \<mu>: "tight \<mu>" "subseq s"
-  shows "\<exists>r M. subseq r \<and> real_distribution M \<and> weak_conv_m (\<mu> \<circ> s \<circ> r) M"
+  assumes \<mu>: "tight \<mu>" "strict_mono s"
+  shows "\<exists>r M. strict_mono (r :: nat \<Rightarrow> nat) \<and> real_distribution M \<and> weak_conv_m (\<mu> \<circ> s \<circ> r) M"
 proof -
   define f where "f k = cdf (\<mu> (s k))" for k
   interpret \<mu>: real_distribution "\<mu> k" for k
@@ -174,7 +174,7 @@
     by (auto simp add: abs_le_iff minus_le_iff f_def \<mu>.cdf_nonneg \<mu>.cdf_bounded_prob)
 
   from Helly_selection[OF rcont mono bdd, of "\<lambda>x. x"] obtain r F
-    where F: "subseq r" "\<And>x. continuous (at_right x) F" "mono F" "\<And>x. \<bar>F x\<bar> \<le> 1"
+    where F: "strict_mono r" "\<And>x. continuous (at_right x) F" "mono F" "\<And>x. \<bar>F x\<bar> \<le> 1"
     and lim_F: "\<And>x. continuous (at x) F \<Longrightarrow> (\<lambda>n. f (r n) x) \<longlonglongrightarrow> F x"
     by blast
 
@@ -265,14 +265,14 @@
     using F by (auto intro!: real_distribution_interval_measure cdf_interval_measure simp: mono_def)
   with lim_F LIMSEQ_subseq_LIMSEQ M have "weak_conv_m (\<mu> \<circ> s \<circ> r) (interval_measure F)"
     by (auto simp: weak_conv_def weak_conv_m_def f_def comp_def)
-  then show "\<exists>r M. subseq r \<and> (real_distribution M \<and> weak_conv_m (\<mu> \<circ> s \<circ> r) M)"
+  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)"
     using F M by auto
 qed
 
 corollary tight_subseq_weak_converge:
   fixes \<mu> :: "nat \<Rightarrow> real measure" and M :: "real measure"
   assumes "\<And>n. real_distribution (\<mu> n)" "real_distribution M" and tight: "tight \<mu>" and
-    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"
+    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"
   shows "weak_conv_m \<mu> M"
 proof (rule ccontr)
   define f where "f n = cdf (\<mu> n)" for n
@@ -283,12 +283,12 @@
     by (auto simp: weak_conv_m_def weak_conv_def f_def F_def)
   then obtain \<epsilon> where "\<epsilon> > 0" and "infinite {n. \<not> dist (f n x) (F x) < \<epsilon>}"
     by (auto simp: tendsto_iff not_eventually INFM_iff_infinite cofinite_eq_sequentially[symmetric])
-  then obtain s where s: "\<And>n. \<not> dist (f (s n) x) (F x) < \<epsilon>" and "subseq s"
-    using enumerate_in_set enumerate_mono by (fastforce simp: subseq_def)
-  then obtain r \<nu> where r: "subseq r" "real_distribution \<nu>" "weak_conv_m (\<mu> \<circ> s \<circ> r) \<nu>"
+  then obtain s :: "nat \<Rightarrow> nat" where s: "\<And>n. \<not> dist (f (s n) x) (F x) < \<epsilon>" and "strict_mono s"
+    using enumerate_in_set enumerate_mono by (fastforce simp: strict_mono_def)
+  then obtain r \<nu> where r: "strict_mono r" "real_distribution \<nu>" "weak_conv_m (\<mu> \<circ> s \<circ> r) \<nu>"
     using tight_imp_convergent_subsubsequence[OF tight] by blast
   then have "weak_conv_m (\<mu> \<circ> (s \<circ> r)) M"
-    using \<open>subseq s\<close> r by (intro subseq subseq_o) (auto simp: comp_assoc)
+    using \<open>strict_mono s\<close> r by (intro subseq strict_mono_o) (auto simp: comp_assoc)
   then have "(\<lambda>n. f (s (r n)) x) \<longlonglongrightarrow> F x"
     using x by (auto simp: weak_conv_m_def weak_conv_def F_def f_def)
   then show False
diff -r 407de0768126 -r a1f5c5c26fa6 src/HOL/Probability/Levy.thy
--- a/src/HOL/Probability/Levy.thy	Thu Aug 17 14:40:42 2017 +0200
+++ b/src/HOL/Probability/Levy.thy	Thu Aug 17 14:52:56 2017 +0200
@@ -500,7 +500,7 @@
   show ?thesis
   proof (rule tight_subseq_weak_converge [OF real_distr_M real_distr_M' tight])
     fix s \<nu>
-    assume s: "subseq s"
+    assume s: "strict_mono (s :: nat \<Rightarrow> nat)"
     assume nu: "weak_conv_m (M \<circ> s) \<nu>"
     assume *: "real_distribution \<nu>"
     have 2: "\<And>n. real_distribution ((M \<circ> s) n)" unfolding comp_def by (rule assms)
diff -r 407de0768126 -r a1f5c5c26fa6 src/HOL/Probability/Projective_Limit.thy
--- a/src/HOL/Probability/Projective_Limit.thy	Thu Aug 17 14:40:42 2017 +0200
+++ b/src/HOL/Probability/Projective_Limit.thy	Thu Aug 17 14:52:56 2017 +0200
@@ -45,20 +45,20 @@
 lemma compactE':
   fixes S :: "'a :: metric_space set"
   assumes "compact S" "\<forall>n\<ge>m. f n \<in> S"
-  obtains l r where "l \<in> S" "subseq r" "((f \<circ> r) \<longlongrightarrow> l) sequentially"
+  obtains l r where "l \<in> S" "strict_mono (r::nat\<Rightarrow>nat)" "((f \<circ> r) \<longlongrightarrow> l) sequentially"
 proof atomize_elim
-  have "subseq (op + m)" by (simp add: subseq_def)
+  have "strict_mono (op + m)" by (simp add: strict_mono_def)
   have "\<forall>n. (f o (\<lambda>i. m + i)) n \<in> S" using assms by auto
   from seq_compactE[OF \<open>compact S\<close>[unfolded compact_eq_seq_compact_metric] this] guess l r .
-  hence "l \<in> S" "subseq ((\<lambda>i. m + i) o r) \<and> (f \<circ> ((\<lambda>i. m + i) o r)) \<longlonglongrightarrow> l"
-    using subseq_o[OF \<open>subseq (op + m)\<close> \<open>subseq r\<close>] by (auto simp: o_def)
-  thus "\<exists>l r. l \<in> S \<and> subseq r \<and> (f \<circ> r) \<longlonglongrightarrow> l" by blast
+  hence "l \<in> S" "strict_mono ((\<lambda>i. m + i) o r) \<and> (f \<circ> ((\<lambda>i. m + i) o r)) \<longlonglongrightarrow> l"
+    using strict_mono_o[OF \<open>strict_mono (op + m)\<close> \<open>strict_mono r\<close>] by (auto simp: o_def)
+  thus "\<exists>l r. l \<in> S \<and> strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> l" by blast
 qed
 
 sublocale finmap_seqs_into_compact \<subseteq> subseqs "\<lambda>n s. (\<exists>l. (\<lambda>i. ((f o s) i)\<^sub>F n) \<longlonglongrightarrow> l)"
 proof
-  fix n s
-  assume "subseq s"
+  fix n and s :: "nat \<Rightarrow> nat"
+  assume "strict_mono s"
   from proj_in_KE[of n] guess n0 . note n0 = this
   have "\<forall>i \<ge> n0. ((f \<circ> s) i)\<^sub>F n \<in> (\<lambda>k. (k)\<^sub>F n) ` K n0"
   proof safe
@@ -69,7 +69,7 @@
       by auto
   qed
   from compactE'[OF compact_projset this] guess ls rs .
-  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)
+  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)
 qed
 
 lemma (in finmap_seqs_into_compact) diagonal_tendsto: "\<exists>l. (\<lambda>i. (f (diagseq i))\<^sub>F n) \<longlonglongrightarrow> l"
@@ -77,11 +77,11 @@
   obtain l where "(\<lambda>i. ((f o (diagseq o op + (Suc n))) i)\<^sub>F n) \<longlonglongrightarrow> l"
   proof (atomize_elim, rule diagseq_holds)
     fix r s n
-    assume "subseq r"
+    assume "strict_mono (r :: nat \<Rightarrow> nat)"
     assume "\<exists>l. (\<lambda>i. ((f \<circ> s) i)\<^sub>F n) \<longlonglongrightarrow> l"
     then obtain l where "((\<lambda>i. (f i)\<^sub>F n) o s) \<longlonglongrightarrow> l"
       by (auto simp: o_def)
-    hence "((\<lambda>i. (f i)\<^sub>F n) o s o r) \<longlonglongrightarrow> l" using \<open>subseq r\<close>
+    hence "((\<lambda>i. (f i)\<^sub>F n) o s o r) \<longlonglongrightarrow> l" using \<open>strict_mono r\<close>
       by (rule LIMSEQ_subseq_LIMSEQ)
     thus "\<exists>l. (\<lambda>i. ((f \<circ> (s \<circ> r)) i)\<^sub>F n) \<longlonglongrightarrow> l" by (auto simp add: o_def)
   qed
@@ -406,7 +406,7 @@
     have "(\<lambda>i. fm n (y (Suc (diagseq i)))) \<longlonglongrightarrow> finmap_of (Utn ` J n) z"
       by (rule tendsto_finmap)
     hence "((\<lambda>i. fm n (y (Suc (diagseq i)))) o (\<lambda>i. i + n)) \<longlonglongrightarrow> finmap_of (Utn ` J n) z"
-      by (rule LIMSEQ_subseq_LIMSEQ) (simp add: subseq_def)
+      by (rule LIMSEQ_subseq_LIMSEQ) (simp add: strict_mono_def)
     moreover
     have "(\<forall>i. ((\<lambda>i. fm n (y (Suc (diagseq i)))) o (\<lambda>i. i + n)) i \<in> K' n)"
       apply (auto simp add: o_def intro!: fm_in_K' \<open>1 \<le> n\<close> le_SucI)
diff -r 407de0768126 -r a1f5c5c26fa6 src/HOL/Series.thy
--- a/src/HOL/Series.thy	Thu Aug 17 14:40:42 2017 +0200
+++ b/src/HOL/Series.thy	Thu Aug 17 14:52:56 2017 +0200
@@ -1107,7 +1107,7 @@
 qed
 
 lemma sums_mono_reindex:
-  assumes subseq: "subseq g"
+  assumes subseq: "strict_mono g"
     and zero: "\<And>n. n \<notin> range g \<Longrightarrow> f n = 0"
   shows "(\<lambda>n. f (g n)) sums c \<longleftrightarrow> f sums c"
   unfolding sums_def
@@ -1117,10 +1117,10 @@
   proof
     fix n :: nat
     from subseq have "(\<Sum>k<n. f (g k)) = (\<Sum>k\<in>g`{..<n}. f k)"
-      by (subst sum.reindex) (auto intro: subseq_imp_inj_on)
+      by (subst sum.reindex) (auto intro: strict_mono_imp_inj_on)
     also from subseq have "\<dots> = (\<Sum>k<g n. f k)"
       by (intro sum.mono_neutral_left ballI zero)
-        (auto dest: subseq_strict_mono simp: strict_mono_less strict_mono_less_eq)
+        (auto simp: strict_mono_less strict_mono_less_eq)
     finally show "(\<Sum>k<n. f (g k)) = (\<Sum>k<g n. f k)" .
   qed
   also from LIMSEQ_subseq_LIMSEQ[OF lim subseq] have "\<dots> \<longlonglongrightarrow> c"
@@ -1150,7 +1150,7 @@
         have "g l < g (g_inv n)"
           by (rule less_le_trans[OF _ g_inv]) (use k l in simp_all)
         with subseq have "l < g_inv n"
-          by (simp add: subseq_strict_mono strict_mono_less)
+          by (simp add: strict_mono_less)
         with k l show False
           by simp
       qed
@@ -1160,7 +1160,7 @@
     with g_inv_least' g_inv have "(\<Sum>k<n. f k) = (\<Sum>k\<in>g`{..<g_inv n}. f k)"
       by (intro sum.mono_neutral_right) auto
     also from subseq have "\<dots> = (\<Sum>k<g_inv n. f (g k))"
-      using subseq_imp_inj_on by (subst sum.reindex) simp_all
+      using strict_mono_imp_inj_on by (subst sum.reindex) simp_all
     finally show "(\<Sum>k<n. f k) = (\<Sum>k<g_inv n. f (g k))" .
   qed
   also {
@@ -1169,7 +1169,7 @@
     also have "n \<le> g (g_inv n)"
       by (rule g_inv)
     finally have "K \<le> g_inv n"
-      using subseq by (simp add: strict_mono_less_eq subseq_strict_mono)
+      using subseq by (simp add: strict_mono_less_eq)
   }
   then have "filterlim g_inv at_top sequentially"
     by (auto simp: filterlim_at_top eventually_at_top_linorder)
@@ -1179,14 +1179,14 @@
 qed
 
 lemma summable_mono_reindex:
-  assumes subseq: "subseq g"
+  assumes subseq: "strict_mono g"
     and zero: "\<And>n. n \<notin> range g \<Longrightarrow> f n = 0"
   shows "summable (\<lambda>n. f (g n)) \<longleftrightarrow> summable f"
   using sums_mono_reindex[of g f, OF assms] by (simp add: summable_def)
 
 lemma suminf_mono_reindex:
   fixes f :: "nat \<Rightarrow> 'a::{t2_space,comm_monoid_add}"
-  assumes "subseq g" "\<And>n. n \<notin> range g \<Longrightarrow> f n = 0"
+  assumes "strict_mono g" "\<And>n. n \<notin> range g \<Longrightarrow> f n = 0"
   shows   "suminf (\<lambda>n. f (g n)) = suminf f"
 proof (cases "summable f")
   case True
diff -r 407de0768126 -r a1f5c5c26fa6 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Thu Aug 17 14:40:42 2017 +0200
+++ b/src/HOL/Topological_Spaces.thy	Thu Aug 17 14:52:56 2017 +0200
@@ -1069,14 +1069,13 @@
   unfolding antimono_def ..
 
 text \<open>Definition of subsequence.\<close>
-definition subseq :: "(nat \<Rightarrow> nat) \<Rightarrow> bool"
-  where "subseq f \<longleftrightarrow> (\<forall>m. \<forall>n>m. f m < f n)"
-
-lemma subseq_le_mono: "subseq r \<Longrightarrow> m \<le> n \<Longrightarrow> r m \<le> r n"
-  by (simp add: less_mono_imp_le_mono subseq_def)
-
-lemma subseq_id: "subseq id"
-  by (simp add: subseq_def)
+
+(* For compatibility with the old "subseq" *)
+lemma strict_mono_leD: "strict_mono r \<Longrightarrow> m \<le> n \<Longrightarrow> r m \<le> r n"
+  by (erule (1) monoD [OF strict_mono_mono])
+
+lemma strict_mono_id: "strict_mono id"
+  by (simp add: strict_mono_def)
 
 lemma incseq_SucI: "(\<And>n. X n \<le> X (Suc n)) \<Longrightarrow> incseq X"
   using lift_Suc_mono_le[of X] by (auto simp: incseq_def)
@@ -1144,28 +1143,30 @@
 
 text \<open>Subsequence (alternative definition, (e.g. Hoskins)\<close>
 
-lemma subseq_Suc_iff: "subseq f \<longleftrightarrow> (\<forall>n. f n < f (Suc n))"
-  apply (simp add: subseq_def)
-  apply (auto dest!: less_imp_Suc_add)
-  apply (induct_tac k)
-   apply (auto intro: less_trans)
-  done
-
-lemma subseq_add: "subseq (\<lambda>n. n + k)"
-  by (auto simp: subseq_Suc_iff)
+lemma strict_mono_Suc_iff: "strict_mono f \<longleftrightarrow> (\<forall>n. f n < f (Suc n))"
+proof (intro iffI strict_monoI)
+  assume *: "\<forall>n. f n < f (Suc n)"
+  fix m n :: nat assume "m < n"
+  thus "f m < f n"
+    by (induction rule: less_Suc_induct) (use * in auto)
+qed (auto simp: strict_mono_def)
+
+lemma strict_mono_add: "strict_mono (\<lambda>n::'a::linordered_semidom. n + k)"
+  by (auto simp: strict_mono_def)
 
 text \<open>For any sequence, there is a monotonic subsequence.\<close>
 lemma seq_monosub:
   fixes s :: "nat \<Rightarrow> 'a::linorder"
-  shows "\<exists>f. subseq f \<and> monoseq (\<lambda>n. (s (f n)))"
+  shows "\<exists>f. strict_mono f \<and> monoseq (\<lambda>n. (s (f n)))"
 proof (cases "\<forall>n. \<exists>p>n. \<forall>m\<ge>p. s m \<le> s p")
   case True
   then have "\<exists>f. \<forall>n. (\<forall>m\<ge>f n. s m \<le> s (f n)) \<and> f n < f (Suc n)"
     by (intro dependent_nat_choice) (auto simp: conj_commute)
-  then obtain f where f: "subseq f" and mono: "\<And>n m. f n \<le> m \<Longrightarrow> s m \<le> s (f n)"
-    by (auto simp: subseq_Suc_iff)
+  then obtain f :: "nat \<Rightarrow> nat" 
+    where f: "strict_mono f" and mono: "\<And>n m. f n \<le> m \<Longrightarrow> s m \<le> s (f n)"
+    by (auto simp: strict_mono_Suc_iff)
   then have "incseq f"
-    unfolding subseq_Suc_iff incseq_Suc_iff by (auto intro: less_imp_le)
+    unfolding strict_mono_Suc_iff incseq_Suc_iff by (auto intro: less_imp_le)
   then have "monoseq (\<lambda>n. s (f n))"
     by (auto simp add: incseq_def intro!: mono monoI2)
   with f show ?thesis
@@ -1182,29 +1183,29 @@
       by (auto intro: less_trans)
   qed auto
   then show ?thesis
-    by (auto simp: monoseq_iff incseq_Suc_iff subseq_Suc_iff)
+    by (auto simp: monoseq_iff incseq_Suc_iff strict_mono_Suc_iff)
 qed
 
 lemma seq_suble:
-  assumes sf: "subseq f"
+  assumes sf: "strict_mono (f :: nat \<Rightarrow> nat)"
   shows "n \<le> f n"
 proof (induct n)
   case 0
   show ?case by simp
 next
   case (Suc n)
-  with sf [unfolded subseq_Suc_iff, rule_format, of n] have "n < f (Suc n)"
+  with sf [unfolded strict_mono_Suc_iff, rule_format, of n] have "n < f (Suc n)"
      by arith
   then show ?case by arith
 qed
 
 lemma eventually_subseq:
-  "subseq r \<Longrightarrow> eventually P sequentially \<Longrightarrow> eventually (\<lambda>n. P (r n)) sequentially"
+  "strict_mono r \<Longrightarrow> eventually P sequentially \<Longrightarrow> eventually (\<lambda>n. P (r n)) sequentially"
   unfolding eventually_sequentially by (metis seq_suble le_trans)
 
 lemma not_eventually_sequentiallyD:
   assumes "\<not> eventually P sequentially"
-  shows "\<exists>r. subseq r \<and> (\<forall>n. \<not> P (r n))"
+  shows "\<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (\<forall>n. \<not> P (r n))"
 proof -
   from assms have "\<forall>n. \<exists>m\<ge>n. \<not> P m"
     unfolding eventually_sequentially by (simp add: not_less)
@@ -1212,29 +1213,14 @@
     by (auto simp: choice_iff)
   then show ?thesis
     by (auto intro!: exI[of _ "\<lambda>n. r (((Suc \<circ> r) ^^ Suc n) 0)"]
-             simp: less_eq_Suc_le subseq_Suc_iff)
+             simp: less_eq_Suc_le strict_mono_Suc_iff)
 qed
 
-lemma filterlim_subseq: "subseq f \<Longrightarrow> filterlim f sequentially sequentially"
+lemma filterlim_subseq: "strict_mono f \<Longrightarrow> filterlim f sequentially sequentially"
   unfolding filterlim_iff by (metis eventually_subseq)
 
-lemma subseq_o: "subseq r \<Longrightarrow> subseq s \<Longrightarrow> subseq (r \<circ> s)"
-  unfolding subseq_def by simp
-
-lemma subseq_mono: "subseq r \<Longrightarrow> m < n \<Longrightarrow> r m < r n"
-  by (auto simp: subseq_def)
-
-lemma subseq_imp_inj_on: "subseq g \<Longrightarrow> inj_on g A"
-proof (rule inj_onI)
-  assume g: "subseq g"
-  fix x y
-  assume "g x = g y"
-  with subseq_mono[OF g, of x y] subseq_mono[OF g, of y x] show "x = y"
-    by (cases x y rule: linorder_cases) simp_all
-qed
-
-lemma subseq_strict_mono: "subseq g \<Longrightarrow> strict_mono g"
-  by (intro strict_monoI subseq_mono[of g])
+lemma strict_mono_o: "strict_mono r \<Longrightarrow> strict_mono s \<Longrightarrow> strict_mono (r \<circ> s)"
+  unfolding strict_mono_def by simp
 
 lemma incseq_imp_monoseq:  "incseq X \<Longrightarrow> monoseq X"
   by (simp add: incseq_def monoseq_def)
@@ -1324,10 +1310,10 @@
   for x :: "'a::linorder_topology"
   by (metis LIMSEQ_le_const LIMSEQ_le_const2 decseq_def incseq_def monoseq_iff)
 
-lemma LIMSEQ_subseq_LIMSEQ: "X \<longlonglongrightarrow> L \<Longrightarrow> subseq f \<Longrightarrow> (X \<circ> f) \<longlonglongrightarrow> L"
+lemma LIMSEQ_subseq_LIMSEQ: "X \<longlonglongrightarrow> L \<Longrightarrow> strict_mono f \<Longrightarrow> (X \<circ> f) \<longlonglongrightarrow> L"
   unfolding comp_def by (rule filterlim_compose [of X, OF _ filterlim_subseq])
 
-lemma convergent_subseq_convergent: "convergent X \<Longrightarrow> subseq f \<Longrightarrow> convergent (X \<circ> f)"
+lemma convergent_subseq_convergent: "convergent X \<Longrightarrow> strict_mono f \<Longrightarrow> convergent (X \<circ> f)"
   by (auto simp: convergent_def intro: LIMSEQ_subseq_LIMSEQ)
 
 lemma limI: "X \<longlonglongrightarrow> L \<Longrightarrow> lim X = L"
@@ -1651,7 +1637,7 @@
       and "(\<lambda>n. X (s n)) \<longlonglongrightarrow> a"
       and "\<not> P (X (s n))"
       for n
-      by (auto simp: subseq_Suc_iff Suc_le_eq incseq_Suc_iff
+      by (auto simp: strict_mono_Suc_iff Suc_le_eq incseq_Suc_iff
           intro!: LIMSEQ_subseq_LIMSEQ[OF \<open>X \<longlonglongrightarrow> a\<close>, unfolded comp_def])
     from *[OF this(1,2,3,4)] this(5) show False
       by auto
@@ -1700,7 +1686,7 @@
       and "(\<lambda>n. X (s n)) \<longlonglongrightarrow> a"
       and "\<not> P (X (s n))"
       for n
-      by (auto simp: subseq_Suc_iff Suc_le_eq decseq_Suc_iff
+      by (auto simp: strict_mono_Suc_iff Suc_le_eq decseq_Suc_iff
           intro!: LIMSEQ_subseq_LIMSEQ[OF \<open>X \<longlonglongrightarrow> a\<close>, unfolded comp_def])
     from *[OF this(1,2,3,4)] this(5) show False
       by auto
@@ -3143,11 +3129,11 @@
   unfolding Cauchy_uniform filterlim_def by (intro nhds_imp_cauchy_filter)
 
 lemma Cauchy_subseq_Cauchy:
-  assumes "Cauchy X" "subseq f"
+  assumes "Cauchy X" "strict_mono f"
   shows "Cauchy (X \<circ> f)"
   unfolding Cauchy_uniform comp_def filtermap_filtermap[symmetric] cauchy_filter_def
   by (rule order_trans[OF _ \<open>Cauchy X\<close>[unfolded Cauchy_uniform cauchy_filter_def]])
-     (intro prod_filter_mono filtermap_mono filterlim_subseq[OF \<open>subseq f\<close>, unfolded filterlim_def])
+     (intro prod_filter_mono filtermap_mono filterlim_subseq[OF \<open>strict_mono f\<close>, unfolded filterlim_def])
 
 lemma convergent_Cauchy: "convergent X \<Longrightarrow> Cauchy X"
   unfolding convergent_def by (erule exE, erule LIMSEQ_imp_Cauchy)