# 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 "((\y. norm (f y - f x - D * (y - x)) / norm (y - x)) \ 0) (at x within S) = ((\y. (f y - f x) / (y - x) - D) \ 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 \ (\h. (f (x + h) - f x) / h) \0\ D" unfolding field_has_derivative_at has_field_derivative_def has_field_derivative_iff .. +text \due to Christian Pardillo Laursen, replacing a proper epsilon-delta horror\ lemma field_derivative_lim_unique: assumes f: "(f has_field_derivative df) (at z)" - and s: "s \ 0" "\n. s n \ 0" - and a: "(\n. (f (z + s n) - f z) / s n) \ a" - shows "df = a" -proof (rule ccontr) - assume "df \ a" - obtain q where qpos: "\\. \ > 0 \ q \ > 0" - and q: "\\ y. \\ > 0; y \ z; dist y z < q \\ \ dist ((f y - f z) / (y - z)) df < \" - using f unfolding LIM_def has_field_derivative_iff by metis - obtain NA where NA: "\\ n. \\ > 0; n \ NA \\ \ dist ((f (z + s n) - f z) / s n) a < \" - using a unfolding LIMSEQ_def by metis - obtain NB where NB: "\\ n. \\ > 0; n \ NB \\ \ norm (s n) < \" - using s unfolding LIMSEQ_def by (metis norm_conv_dist) - have df: "\\ n. \ > 0 \ \0 < \; norm (s n) < q \\ \ dist ((f (z + s n) - f z) / s n) df < \" - using add_cancel_left_right add_diff_cancel_left' q s - by (metis add_diff_cancel_right' dist_diff(1)) - define \ where "\ \ dist df a / 2" - with \df \ a\ have "\ > 0" and \: "\+\ \ dist df a" - by auto - define N where "N \ max (NA \) (NB (q \))" - then have "norm (s N) < q \" - by (simp add: NB \\ > 0\ qpos) - then have "dist ((f (z + s N) - f z) / s N) df < \" - by (simp add: \0 < \\ df) - moreover have "dist ((f (z + s N) - f z) / s N) a < \" - using NA N_def \0 < \\ by force - ultimately have "dist df a < dist df a" - by (smt (verit, ccfv_SIG) \ dist_commute dist_triangle) - then show False .. + and s: "s \ 0" "\n. s n \ 0" + and a: "(\n. (f (z + s n) - f z) / s n) \ a" + shows "df = a" +proof - + have "((\k. (f (z + k) - f z) / k) \ df) (at 0)" + using f by (simp add: DERIV_def) + with s have "((\n. (f (z + s n) - f z) / s n) \ df)" + by (simp flip: LIMSEQ_SEQ_conv) + then show ?thesis + using a by (rule LIMSEQ_unique) qed lemma mult_commute_abs: "(\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 \(dvd) :: 'a::comm_monoid_mult \ 'a \ bool\ 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 \\<^const>\count_list\\ +text \This library is intentionally minimal. See the remark about multisets at the point above where @{const count_list} is defined.\ + 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 \ length xs" by (induction xs) auto +lemma count_list_map_ge: "count_list xs x \ count_list (map f xs) (f x)" +by (induction xs) auto + lemma count_list_inj_map: "\ inj_on f (set xs); x \ set xs \ \ 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 \ X \ finite X \ 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 @@ "(\f. (\n. f n \ a) \ f \ a \ eventually (\n. P (f n)) sequentially) \ eventually P (at a)" using sequentially_imp_eventually_within [where s=UNIV] by simp -lemma LIMSEQ_SEQ_conv1: - fixes f :: "'a::topological_space \ 'b::topological_space" - assumes f: "f \a\ l" - shows "\S. (\n. S n \ a) \ S \ a \ (\n. f (S n)) \ l" - using tendsto_compose_eventually [OF f, where F=sequentially] by simp - -lemma LIMSEQ_SEQ_conv2: - fixes f :: "'a::first_countable_topology \ 'b::topological_space" - assumes "\S. (\n. S n \ a) \ S \ a \ (\n. f (S n)) \ l" - shows "f \a\ l" - using assms unfolding tendsto_def [where l=l] by (simp add: sequentially_imp_eventually_at) - -lemma LIMSEQ_SEQ_conv: "(\S. (\n. S n \ a) \ S \ a \ (\n. X (S n)) \ L) \ X \a\ L" +lemma LIMSEQ_SEQ_conv: + "(\S. (\n. S n \ a) \ S \ a \ (\n. X (S n)) \ L) \ X \a\ 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}"