# HG changeset patch
# User wenzelm
# Date 1646912042 -3600
# Node ID 5a15a2ceafdfdf9c98f0e022cb171297e42f9c62
# Parent  f70b1a2c27832648c9b4b0064f6cc8a0429bd82e# Parent  fd44e4559adb16a91f435729adff31d4d4f84d2d
merged

diff -r fd44e4559adb -r 5a15a2ceafdf src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Thu Mar 10 12:28:20 2022 +0100
+++ b/src/HOL/Deriv.thy	Thu Mar 10 12:34:02 2022 +0100
@@ -803,9 +803,7 @@
 proof -
   have "((\<lambda>y. norm (f y - f x - D * (y - x)) / norm (y - x)) \<longlongrightarrow> 0) (at x within S) 
       = ((\<lambda>y. (f y - f x) / (y - x) - D) \<longlongrightarrow> 0) (at x within S)"
-    apply (subst tendsto_norm_zero_iff[symmetric], rule filterlim_cong)
-      apply (simp_all add: eventually_at_filter field_simps nonzero_norm_divide)
-    done
+    by (smt (verit, best) Lim_cong_within divide_diff_eq_iff norm_divide right_minus_eq tendsto_norm_zero_iff)
   then show ?thesis
     by (simp add: has_field_derivative_def has_derivative_iff_norm bounded_linear_mult_right LIM_zero_iff)
 qed
@@ -813,36 +811,19 @@
 lemma DERIV_def: "DERIV f x :> D \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow> D"
   unfolding field_has_derivative_at has_field_derivative_def has_field_derivative_iff ..
 
+text \<open>due to Christian Pardillo Laursen, replacing a proper epsilon-delta horror\<close>
 lemma field_derivative_lim_unique:
   assumes f: "(f has_field_derivative df) (at z)"
-      and s: "s \<longlonglongrightarrow> 0"  "\<And>n. s n \<noteq> 0" 
-      and a: "(\<lambda>n. (f (z + s n) - f z) / s n) \<longlonglongrightarrow> a"
-    shows "df = a"
-proof (rule ccontr)
-  assume "df \<noteq> a"
-  obtain q where qpos: "\<And>\<epsilon>. \<epsilon> > 0 \<Longrightarrow> q \<epsilon> > 0" 
-             and q: "\<And>\<epsilon> y. \<lbrakk>\<epsilon> > 0; y \<noteq> z; dist y z < q \<epsilon>\<rbrakk> \<Longrightarrow> dist ((f y - f z) / (y - z)) df < \<epsilon>"
-    using f unfolding LIM_def has_field_derivative_iff by metis
-  obtain NA where NA: "\<And>\<epsilon> n. \<lbrakk>\<epsilon> > 0; n \<ge> NA \<epsilon>\<rbrakk> \<Longrightarrow> dist ((f (z + s n) - f z) / s n) a < \<epsilon>" 
-    using a unfolding LIMSEQ_def by metis
-  obtain NB where NB: "\<And>\<epsilon> n. \<lbrakk>\<epsilon> > 0; n \<ge> NB \<epsilon>\<rbrakk> \<Longrightarrow> norm (s n) < \<epsilon>" 
-    using s unfolding LIMSEQ_def by (metis norm_conv_dist)
-  have df: "\<And>\<epsilon> n. \<epsilon> > 0 \<Longrightarrow> \<lbrakk>0 < \<epsilon>; norm (s n) < q \<epsilon>\<rbrakk> \<Longrightarrow> dist ((f (z + s n) - f z) / s n) df < \<epsilon>"
-    using add_cancel_left_right add_diff_cancel_left' q s
-    by (metis add_diff_cancel_right' dist_diff(1))
-  define \<delta> where "\<delta> \<equiv> dist df a / 2"
-  with \<open>df \<noteq> a\<close> have "\<delta> > 0" and \<delta>: "\<delta>+\<delta> \<le> dist df a"
-    by auto
-  define N where "N \<equiv> max (NA \<delta>) (NB (q \<delta>))"
-  then have "norm (s N) < q \<delta>"
-    by (simp add: NB \<open>\<delta> > 0\<close> qpos)
-  then have "dist ((f (z + s N) - f z) / s N) df < \<delta>"
-    by (simp add: \<open>0 < \<delta>\<close> df)
-  moreover have "dist ((f (z + s N) - f z) / s N) a < \<delta>"
-    using NA N_def \<open>0 < \<delta>\<close> by force
-  ultimately have "dist df a < dist df a"
-    by (smt (verit, ccfv_SIG) \<delta> dist_commute dist_triangle)
-  then show False ..
+    and s: "s \<longlonglongrightarrow> 0"  "\<And>n. s n \<noteq> 0" 
+    and a: "(\<lambda>n. (f (z + s n) - f z) / s n) \<longlonglongrightarrow> a"
+  shows "df = a"
+proof -
+  have "((\<lambda>k. (f (z + k) - f z) / k) \<longlongrightarrow> df) (at 0)"
+    using f by (simp add: DERIV_def)
+  with s have "((\<lambda>n. (f (z + s n) - f z) / s n) \<longlonglongrightarrow> df)"
+    by (simp flip: LIMSEQ_SEQ_conv)
+  then show ?thesis
+    using a by (rule LIMSEQ_unique)
 qed
 
 lemma mult_commute_abs: "(\<lambda>x. x * c) = (*) c"
diff -r fd44e4559adb -r 5a15a2ceafdf src/HOL/Library/Lexord.thy
--- a/src/HOL/Library/Lexord.thy	Thu Mar 10 12:28:20 2022 +0100
+++ b/src/HOL/Library/Lexord.thy	Thu Mar 10 12:34:02 2022 +0100
@@ -189,10 +189,7 @@
 global_interpretation dvd: lex_preordering \<open>(dvd) :: 'a::comm_monoid_mult \<Rightarrow> 'a \<Rightarrow> bool\<close> dvd_strict
   defines lex_dvd = dvd.lex_less_eq
     and lex_dvd_strict = dvd.lex_less
-  apply (rule lex_preordering.intro)
-  apply standard
-    apply (auto simp add: dvd_strict_def)
-  done
+  by unfold_locales (auto simp add: dvd_strict_def)
 
 global_interpretation lex_dvd: preordering lex_dvd lex_dvd_strict
   by (fact dvd.preordering)
diff -r fd44e4559adb -r 5a15a2ceafdf src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Mar 10 12:28:20 2022 +0100
+++ b/src/HOL/List.thy	Thu Mar 10 12:34:02 2022 +0100
@@ -4277,6 +4277,8 @@
 
 subsubsection \<open>\<^const>\<open>count_list\<close>\<close>
 
+text \<open>This library is intentionally minimal. See the remark about multisets at the point above where @{const count_list} is defined.\<close>
+
 lemma count_list_append[simp]: "count_list (xs @ ys) x = count_list xs x + count_list ys x"
 by (induction xs) simp_all
 
@@ -4289,10 +4291,16 @@
 lemma count_le_length: "count_list xs x \<le> length xs"
 by (induction xs) auto
 
+lemma count_list_map_ge: "count_list xs x \<le> count_list (map f xs) (f x)"
+by (induction xs) auto
+
 lemma count_list_inj_map:
   "\<lbrakk> inj_on f (set xs); x \<in> set xs \<rbrakk> \<Longrightarrow> count_list (map f xs) (f x) = count_list xs x"
 by (induction xs) (simp, fastforce)
 
+lemma count_list_rev[simp]: "count_list (rev xs) x = count_list xs x"
+by (induction xs) auto
+
 lemma sum_count_set:
   "set xs \<subseteq> X \<Longrightarrow> finite X \<Longrightarrow> sum (count_list xs) X = length xs"
 proof (induction xs arbitrary: X)
diff -r fd44e4559adb -r 5a15a2ceafdf src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Thu Mar 10 12:28:20 2022 +0100
+++ b/src/HOL/Topological_Spaces.thy	Thu Mar 10 12:34:02 2022 +0100
@@ -1802,21 +1802,16 @@
   "(\<forall>f. (\<forall>n. f n \<noteq> a) \<and> f \<longlonglongrightarrow> a \<longrightarrow> eventually (\<lambda>n. P (f n)) sequentially) \<Longrightarrow> eventually P (at a)"
   using sequentially_imp_eventually_within [where s=UNIV] by simp
 
-lemma LIMSEQ_SEQ_conv1:
-  fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
-  assumes f: "f \<midarrow>a\<rightarrow> l"
-  shows "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S \<longlonglongrightarrow> a \<longrightarrow> (\<lambda>n. f (S n)) \<longlonglongrightarrow> l"
-  using tendsto_compose_eventually [OF f, where F=sequentially] by simp
-
-lemma LIMSEQ_SEQ_conv2:
-  fixes f :: "'a::first_countable_topology \<Rightarrow> 'b::topological_space"
-  assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S \<longlonglongrightarrow> a \<longrightarrow> (\<lambda>n. f (S n)) \<longlonglongrightarrow> l"
-  shows "f \<midarrow>a\<rightarrow> l"
-  using assms unfolding tendsto_def [where l=l] by (simp add: sequentially_imp_eventually_at)
-
-lemma LIMSEQ_SEQ_conv: "(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S \<longlonglongrightarrow> a \<longrightarrow> (\<lambda>n. X (S n)) \<longlonglongrightarrow> L) \<longleftrightarrow> X \<midarrow>a\<rightarrow> L"
+lemma LIMSEQ_SEQ_conv:
+  "(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S \<longlonglongrightarrow> a \<longrightarrow> (\<lambda>n. X (S n)) \<longlonglongrightarrow> L)  \<longleftrightarrow>  X \<midarrow>a\<rightarrow> L"  (is "?lhs=?rhs")
   for a :: "'a::first_countable_topology" and L :: "'b::topological_space"
-  using LIMSEQ_SEQ_conv2 LIMSEQ_SEQ_conv1 ..
+proof
+  assume ?lhs then show ?rhs
+    by (simp add: sequentially_imp_eventually_within tendsto_def) 
+next
+  assume ?rhs then show ?lhs
+    using tendsto_compose_eventually eventuallyI by blast
+qed    
 
 lemma sequentially_imp_eventually_at_left:
   fixes a :: "'a::{linorder_topology,first_countable_topology}"