--- a/src/HOL/Complex_Analysis/Complex_Singularities.thy Wed Mar 19 22:18:52 2025 +0000
+++ b/src/HOL/Complex_Analysis/Complex_Singularities.thy Fri Mar 21 10:45:56 2025 +0000
@@ -245,8 +245,10 @@
ultimately show False
using not_tendsto_and_filterlim_at_infinity trivial_limit_sequentially by blast
qed
-
- text \<open>The proposition
+
+subsection \<open>Isolated singularities\<close>
+
+text \<open>The proposition
\<^term>\<open>\<exists>x. ((f::complex\<Rightarrow>complex) \<longlongrightarrow> x) (at z) \<or> is_pole f z\<close>
can be interpreted as the complex function \<^term>\<open>f\<close> has a non-essential singularity at \<^term>\<open>z\<close>
(i.e. the singularity is either removable or a pole).\<close>
@@ -1059,6 +1061,47 @@
shows "isolated_singularity_at f z"
by (meson Diff_subset analytic_at assms holomorphic_on_subset isolated_singularity_at_holomorphic)
+lemma isolated_singularity_sum [singularity_intros]:
+ assumes "\<And>x. x \<in> A \<Longrightarrow> isolated_singularity_at (f x) z"
+ shows "isolated_singularity_at (\<lambda>w. \<Sum>x\<in>A. f x w) z"
+ using assms by (induction A rule: infinite_finite_induct) (auto intro!: singularity_intros)
+
+lemma isolated_singularity_prod [singularity_intros]:
+ assumes "\<And>x. x \<in> A \<Longrightarrow> isolated_singularity_at (f x) z"
+ shows "isolated_singularity_at (\<lambda>w. \<Prod>x\<in>A. f x w) z"
+ using assms by (induction A rule: infinite_finite_induct) (auto intro!: singularity_intros)
+
+lemma isolated_singularity_sum_list [singularity_intros]:
+ assumes "\<And>f. f \<in> set fs \<Longrightarrow> isolated_singularity_at f z"
+ shows "isolated_singularity_at (\<lambda>w. \<Sum>f\<leftarrow>fs. f w) z"
+ using assms by (induction fs) (auto intro!: singularity_intros)
+
+lemma isolated_singularity_prod_list [singularity_intros]:
+ assumes "\<And>f. f \<in> set fs \<Longrightarrow> isolated_singularity_at f z"
+ shows "isolated_singularity_at (\<lambda>w. \<Prod>f\<leftarrow>fs. f w) z"
+ using assms by (induction fs) (auto intro!: singularity_intros)
+
+lemma isolated_singularity_sum_mset [singularity_intros]:
+ assumes "\<And>f. f \<in># F \<Longrightarrow> isolated_singularity_at f z"
+ shows "isolated_singularity_at (\<lambda>w. \<Sum>f\<in>#F. f w) z"
+ using assms by (induction F) (auto intro!: singularity_intros)
+
+lemma isolated_singularity_prod_mset [singularity_intros]:
+ assumes "\<And>f. f \<in># F \<Longrightarrow> isolated_singularity_at f z"
+ shows "isolated_singularity_at (\<lambda>w. \<Prod>f\<in>#F. f w) z"
+ using assms by (induction F) (auto intro!: singularity_intros)
+
+lemma analytic_nhd_imp_isolated_singularity:
+ assumes "f analytic_on A - {x}" "x \<in> A" "open A"
+ shows "isolated_singularity_at f x"
+ unfolding isolated_singularity_at_def using assms
+ using analytic_imp_holomorphic isolated_singularity_at_def isolated_singularity_at_holomorphic by blast
+
+lemma isolated_singularity_at_iff_analytic_nhd:
+ "isolated_singularity_at f x \<longleftrightarrow> (\<exists>A. x \<in> A \<and> open A \<and> f analytic_on A - {x})"
+ by (meson open_ball analytic_nhd_imp_isolated_singularity
+ centre_in_ball isolated_singularity_at_def)
+
subsection \<open>The order of non-essential singularities (i.e. removable singularities or poles)\<close>
definition\<^marker>\<open>tag important\<close> zorder :: "(complex \<Rightarrow> complex) \<Rightarrow> complex \<Rightarrow> int" where
--- a/src/HOL/Complex_Analysis/Winding_Numbers.thy Wed Mar 19 22:18:52 2025 +0000
+++ b/src/HOL/Complex_Analysis/Winding_Numbers.thy Fri Mar 21 10:45:56 2025 +0000
@@ -281,6 +281,10 @@
by metis
qed
+lemma winding_number_offset_NO_MATCH:
+ "NO_MATCH 0 z \<Longrightarrow> winding_number p z = winding_number (\<lambda>w. p w - z) 0"
+ using winding_number_offset by metis
+
lemma winding_number_negatepath:
assumes \<gamma>: "valid_path \<gamma>" and 0: "0 \<notin> path_image \<gamma>"
shows "winding_number(uminus \<circ> \<gamma>) 0 = winding_number \<gamma> 0"
--- a/src/HOL/Euclidean_Rings.thy Wed Mar 19 22:18:52 2025 +0000
+++ b/src/HOL/Euclidean_Rings.thy Fri Mar 21 10:45:56 2025 +0000
@@ -2584,6 +2584,10 @@
by simp
qed
+lemma int_div_le_self:
+ \<open>x div k \<le> x\<close> if \<open>0 < x\<close> for x k :: int
+ by (metis div_by_1 int_div_less_self less_le_not_le nle_le nonneg1_imp_zdiv_pos_iff order.trans that)
+
subsubsection \<open>Computing \<open>div\<close> and \<open>mod\<close> by shifting\<close>
--- a/src/HOL/Library/Sublist.thy Wed Mar 19 22:18:52 2025 +0000
+++ b/src/HOL/Library/Sublist.thy Fri Mar 21 10:45:56 2025 +0000
@@ -1095,6 +1095,30 @@
lemma suffix_imp_subseq [intro]: "suffix xs ys \<Longrightarrow> subseq xs ys"
by (auto simp: suffix_def)
+text \<open>a subsequence of a sorted list\<close>
+lemma sorted_subset_imp_subseq:
+ fixes xs :: "'a::order list"
+ assumes "set xs \<subseteq> set ys" "sorted_wrt (<) xs" "sorted_wrt (\<le>) ys"
+ shows "subseq xs ys"
+ using assms
+proof (induction xs arbitrary: ys)
+ case Nil
+ then show ?case
+ by auto
+next
+ case (Cons x xs)
+ then have "x \<in> set ys"
+ by auto
+ then obtain us vs where \<section>: "ys = us @ [x] @ vs"
+ by (metis append.left_neutral append_eq_Cons_conv split_list)
+ moreover
+ have "set xs \<subseteq> set vs"
+ using Cons.prems by (fastforce simp: \<section> sorted_wrt_append)
+ with Cons have "subseq xs vs"
+ by (metis \<section> sorted_wrt.simps(2) sorted_wrt_append)
+ ultimately show ?case
+ by auto
+qed
subsection \<open>Appending elements\<close>
--- a/src/HOL/Rat.thy Wed Mar 19 22:18:52 2025 +0000
+++ b/src/HOL/Rat.thy Fri Mar 21 10:45:56 2025 +0000
@@ -928,6 +928,12 @@
lemma quotient_of_int [code abstract]: "quotient_of (Rat.of_int a) = (a, 1)"
by (simp add: of_int_def of_int_rat quotient_of_Fract)
+lemma quotient_of_rat_of_int [simp]: "quotient_of (rat_of_int i) = (i, 1)"
+ using Rat.of_int_def quotient_of_int by force
+
+lemma quotient_of_rat_of_nat [simp]: "quotient_of (rat_of_nat i) = (int i, 1)"
+ by (metis of_int_of_nat_eq quotient_of_rat_of_int)
+
lemma [code_unfold]: "numeral k = Rat.of_int (numeral k)"
by (simp add: Rat.of_int_def)