# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1742553956 0
# Node ID 41f5266e5595662b9980b2a60f93f43c2652a7c0
# Parent  3529946fca19c7409cfb26781da7eaf10b8c1e70
New theorems, mostly from the number theory project

diff -r 3529946fca19 -r 41f5266e5595 src/HOL/Complex_Analysis/Complex_Singularities.thy
--- 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
diff -r 3529946fca19 -r 41f5266e5595 src/HOL/Complex_Analysis/Winding_Numbers.thy
--- 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"
diff -r 3529946fca19 -r 41f5266e5595 src/HOL/Euclidean_Rings.thy
--- 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>
 
diff -r 3529946fca19 -r 41f5266e5595 src/HOL/Library/Sublist.thy
--- 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>
 
diff -r 3529946fca19 -r 41f5266e5595 src/HOL/Rat.thy
--- 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)