# HG changeset patch
# User wenzelm
# Date 1744231504 -7200
# Node ID 1fa80133027d0bd04e9f1490e57524a872d93215
# Parent  7bd2e917f4253f0adea84372401923a119ca7aee# Parent  40a609d67b3386ac73a89e9584531a5696ce549d
merged

diff -r 40a609d67b33 -r 1fa80133027d src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Wed Apr 09 22:37:58 2025 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Wed Apr 09 22:45:04 2025 +0200
@@ -2919,6 +2919,16 @@
   qed (use z in auto)
 qed
 
+lemma has_field_derivative_csqrt' [derivative_intros]:
+  assumes "(f has_field_derivative f') (at x within A)" "f x \<notin> \<real>\<^sub>\<le>\<^sub>0"
+  shows   "((\<lambda>x. csqrt (f x)) has_field_derivative (f' / (2 * csqrt (f x)))) (at x within A)"
+proof -
+  have "((csqrt \<circ> f) has_field_derivative (inverse (2 * csqrt (f x)) * f')) (at x within A)"
+    using has_field_derivative_csqrt assms(1) by (rule DERIV_chain) fact
+  thus ?thesis
+    by (simp add: o_def field_simps)
+qed
+
 lemma field_differentiable_at_csqrt:
     "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> csqrt field_differentiable at z"
   using field_differentiable_def has_field_derivative_csqrt by blast
diff -r 40a609d67b33 -r 1fa80133027d src/HOL/Analysis/Gamma_Function.thy
--- a/src/HOL/Analysis/Gamma_Function.thy	Wed Apr 09 22:37:58 2025 +0200
+++ b/src/HOL/Analysis/Gamma_Function.thy	Wed Apr 09 22:45:04 2025 +0200
@@ -35,66 +35,6 @@
   finally show ?thesis .
 qed
 
-lemma plus_one_in_nonpos_Ints_imp: "z + 1 \<in> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> z \<in> \<int>\<^sub>\<le>\<^sub>0"
-  using nonpos_Ints_diff_Nats[of "z+1" "1"] by simp_all
-
-lemma of_int_in_nonpos_Ints_iff:
-  "(of_int n :: 'a :: ring_char_0) \<in> \<int>\<^sub>\<le>\<^sub>0 \<longleftrightarrow> n \<le> 0"
-  by (auto simp: nonpos_Ints_def)
-
-lemma one_plus_of_int_in_nonpos_Ints_iff:
-  "(1 + of_int n :: 'a :: ring_char_0) \<in> \<int>\<^sub>\<le>\<^sub>0 \<longleftrightarrow> n \<le> -1"
-proof -
-  have "1 + of_int n = (of_int (n + 1) :: 'a)" by simp
-  also have "\<dots> \<in> \<int>\<^sub>\<le>\<^sub>0 \<longleftrightarrow> n + 1 \<le> 0" by (subst of_int_in_nonpos_Ints_iff) simp_all
-  also have "\<dots> \<longleftrightarrow> n \<le> -1" by presburger
-  finally show ?thesis .
-qed
-
-lemma one_minus_of_nat_in_nonpos_Ints_iff:
-  "(1 - of_nat n :: 'a :: ring_char_0) \<in> \<int>\<^sub>\<le>\<^sub>0 \<longleftrightarrow> n > 0"
-proof -
-  have "(1 - of_nat n :: 'a) = of_int (1 - int n)" by simp
-  also have "\<dots> \<in> \<int>\<^sub>\<le>\<^sub>0 \<longleftrightarrow> n > 0" by (subst of_int_in_nonpos_Ints_iff) presburger
-  finally show ?thesis .
-qed
-
-lemma fraction_not_in_ints:
-  assumes "\<not>(n dvd m)" "n \<noteq> 0"
-  shows   "of_int m / of_int n \<notin> (\<int> :: 'a :: {division_ring,ring_char_0} set)"
-proof
-  assume "of_int m / (of_int n :: 'a) \<in> \<int>"
-  then obtain k where "of_int m / of_int n = (of_int k :: 'a)" by (elim Ints_cases)
-  with assms have "of_int m = (of_int (k * n) :: 'a)" by (auto simp add: field_split_simps)
-  hence "m = k * n" by (subst (asm) of_int_eq_iff)
-  hence "n dvd m" by simp
-  with assms(1) show False by contradiction
-qed
-
-lemma fraction_not_in_nats:
-  assumes "\<not>n dvd m" "n \<noteq> 0"
-  shows   "of_int m / of_int n \<notin> (\<nat> :: 'a :: {division_ring,ring_char_0} set)"
-proof
-  assume "of_int m / of_int n \<in> (\<nat> :: 'a set)"
-  also note Nats_subset_Ints
-  finally have "of_int m / of_int n \<in> (\<int> :: 'a set)" .
-  moreover have "of_int m / of_int n \<notin> (\<int> :: 'a set)"
-    using assms by (intro fraction_not_in_ints)
-  ultimately show False by contradiction
-qed
-
-lemma not_in_Ints_imp_not_in_nonpos_Ints: "z \<notin> \<int> \<Longrightarrow> z \<notin> \<int>\<^sub>\<le>\<^sub>0"
-  by (auto simp: Ints_def nonpos_Ints_def)
-
-lemma double_in_nonpos_Ints_imp:
-  assumes "2 * (z :: 'a :: field_char_0) \<in> \<int>\<^sub>\<le>\<^sub>0"
-  shows   "z \<in> \<int>\<^sub>\<le>\<^sub>0 \<or> z + 1/2 \<in> \<int>\<^sub>\<le>\<^sub>0"
-proof-
-  from assms obtain k where k: "2 * z = - of_nat k" by (elim nonpos_Ints_cases')
-  thus ?thesis by (cases "even k") (auto elim!: evenE oddE simp: field_simps)
-qed
-
-
 lemma sin_series: "(\<lambda>n. ((-1)^n / fact (2*n+1)) *\<^sub>R z^(2*n+1)) sums sin z"
 proof -
   from sin_converges[of z] have "(\<lambda>n. sin_coeff n *\<^sub>R z^n) sums sin z" .
diff -r 40a609d67b33 -r 1fa80133027d src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy
--- a/src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy	Wed Apr 09 22:37:58 2025 +0200
+++ b/src/HOL/Complex_Analysis/Cauchy_Integral_Formula.thy	Wed Apr 09 22:45:04 2025 +0200
@@ -412,12 +412,88 @@
   finally show ?case by simp
 qed simp_all
 
+lemma higher_deriv_cmult':
+  assumes "f analytic_on {x}"
+  shows   "(deriv ^^ j) (\<lambda>x. c * f x) x = c * (deriv ^^ j) f x"
+  using assms higher_deriv_cmult[of f _ x j c] assms
+  using analytic_at_two by blast
+
+lemma deriv_cmult':
+  assumes "f analytic_on {x}"
+  shows   "deriv (\<lambda>x. c * f x) x = c * deriv f x"
+  using higher_deriv_cmult'[OF assms, of 1 c] by simp
+
+lemma analytic_derivI:
+  assumes "f analytic_on {z}"
+  shows   "(f has_field_derivative (deriv f z)) (at z within A)"
+  using assms holomorphic_derivI[of f _ z] analytic_at by blast
+
+lemma deriv_compose_analytic:
+  fixes f g :: "complex \<Rightarrow> complex"
+  assumes "f analytic_on {g z}" "g analytic_on {z}"
+  shows "deriv (\<lambda>x. f (g x)) z = deriv f (g z) * deriv g z"
+proof -
+  have "((f \<circ> g) has_field_derivative (deriv f (g z) * deriv g z)) (at z)"
+    by (intro DERIV_chain analytic_derivI assms)
+  thus ?thesis
+    by (auto intro!: DERIV_imp_deriv simp add: o_def)
+qed
+
 lemma valid_path_compose_holomorphic:
   assumes "valid_path g" "f holomorphic_on S" and "open S" "path_image g \<subseteq> S"
   shows "valid_path (f \<circ> g)"
   by (meson assms holomorphic_deriv holomorphic_on_imp_continuous_on holomorphic_on_imp_differentiable_at
       holomorphic_on_subset subsetD valid_path_compose)
 
+lemma valid_path_compose_analytic:
+  assumes "valid_path g" and holo:"f analytic_on S" and "path_image g \<subseteq> S"
+  shows "valid_path (f \<circ> g)"
+proof (rule valid_path_compose[OF \<open>valid_path g\<close>])
+  fix x assume "x \<in> path_image g"
+  then show "f field_differentiable at x"
+    using analytic_on_imp_differentiable_at analytic_on_open assms holo by blast
+next
+  show "continuous_on (path_image g) (deriv f)"
+    by (intro holomorphic_on_imp_continuous_on analytic_imp_holomorphic analytic_intros
+              analytic_on_subset[OF holo] assms)
+qed
+
+lemma analytic_on_deriv [analytic_intros]:
+  assumes "f analytic_on g ` A"
+  assumes "g analytic_on A"
+  shows   "(\<lambda>x. deriv f (g x)) analytic_on A"
+proof -
+  have "(deriv f \<circ> g) analytic_on A"
+    by (rule analytic_on_compose_gen[OF assms(2) analytic_deriv[OF assms(1)]]) auto
+  thus ?thesis
+    by (simp add: o_def)
+qed
+    
+lemma contour_integral_comp_analyticW:
+  assumes "f analytic_on s" "valid_path \<gamma>" "path_image \<gamma> \<subseteq> s"
+  shows "contour_integral (f \<circ> \<gamma>) g = contour_integral \<gamma> (\<lambda>w. deriv f w * g (f w))"
+proof -
+  obtain spikes where "finite spikes" and \<gamma>_diff: "\<gamma> C1_differentiable_on {0..1} - spikes"
+    using \<open>valid_path \<gamma>\<close> unfolding valid_path_def piecewise_C1_differentiable_on_def by auto  
+  show "contour_integral (f \<circ> \<gamma>) g 
+      = contour_integral \<gamma> (\<lambda>w. deriv f w * g (f w))"
+    unfolding contour_integral_integral
+  proof (rule integral_spike[rule_format,OF negligible_finite[OF \<open>finite spikes\<close>]])
+    fix t::real assume t:"t \<in> {0..1} - spikes"
+    then have "\<gamma> differentiable at t" 
+      using \<gamma>_diff unfolding C1_differentiable_on_eq by auto
+    moreover have "f field_differentiable at (\<gamma> t)" 
+    proof -
+      have "\<gamma> t \<in> s" using t assms unfolding path_image_def by auto 
+      thus ?thesis 
+        using \<open>f analytic_on s\<close>  analytic_on_imp_differentiable_at by blast
+    qed
+    ultimately show "deriv f (\<gamma> t) * g (f (\<gamma> t)) * vector_derivative \<gamma> (at t) =
+         g ((f \<circ> \<gamma>) t) * vector_derivative (f \<circ> \<gamma>) (at t)"
+      by (subst vector_derivative_chain_at_general) (simp_all add:field_simps)
+  qed
+qed
+
 subsection\<open>Morera's theorem\<close>
 
 lemma Morera_local_triangle_ball:
@@ -1097,6 +1173,99 @@
     by (fastforce simp add: holomorphic_on_open contg intro: that)
 qed
 
+lemma higher_deriv_complex_uniform_limit:
+  assumes ulim: "uniform_limit A f g F"
+      and f_holo: "eventually (\<lambda>n. f n holomorphic_on A) F"
+      and F: "F \<noteq> bot"
+      and A: "open A" "z \<in> A"
+    shows "((\<lambda>n. (deriv ^^ m) (f n) z) \<longlongrightarrow> (deriv ^^ m) g z) F"
+proof -
+  obtain r where r: "r > 0" "cball z r \<subseteq> A"
+    using A by (meson open_contains_cball)
+  have r': "ball z r \<subseteq> A"
+    using r by auto
+  define h where "h = (\<lambda>n z. f n z - g z)"
+  define c where "c = of_real (2*pi) * \<i> / fact m"
+  have [simp]: "c \<noteq> 0"
+    by (simp add: c_def)
+  have "g holomorphic_on ball z r \<and> continuous_on (cball z r) g"
+  proof (rule holomorphic_uniform_limit)
+    show "uniform_limit (cball z r) f g F"
+      by (rule uniform_limit_on_subset[OF ulim r(2)])
+    show "\<forall>\<^sub>F n in F. continuous_on (cball z r) (f n) \<and> f n holomorphic_on ball z r" using f_holo
+      by eventually_elim
+         (use holomorphic_on_subset[OF _ r(2)] holomorphic_on_subset[OF _ r'] 
+          in  \<open>auto intro!: holomorphic_on_imp_continuous_on\<close>)
+  qed (use F in auto)
+  hence g_holo: "g holomorphic_on ball z r" and g_cont: "continuous_on (cball z r) g"
+    by blast+
+
+  have ulim': "uniform_limit (sphere z r) (\<lambda>n x. h n x / (x - z) ^ (Suc m)) (\<lambda>_. 0) F"
+  proof -
+    have "uniform_limit (sphere z r) (\<lambda>n x. f n x / (x - z) ^ Suc m) (\<lambda>x. g x / (x - z) ^ Suc m) F"
+    proof (intro uniform_lim_divide uniform_limit_intros uniform_limit_on_subset[OF ulim])
+      have "compact (g ` sphere z r)"
+        by (intro compact_continuous_image continuous_on_subset[OF g_cont]) auto
+      thus "bounded (g ` sphere z r)"
+        by (rule compact_imp_bounded)
+      show "r ^ Suc m \<le> norm ((x - z) ^ Suc m)" if "x \<in> sphere z r" for x unfolding norm_power
+        by (intro power_mono) (use that r(1) in \<open>auto simp: dist_norm norm_minus_commute\<close>)
+    qed (use r in auto)
+    hence "uniform_limit (sphere z r) (\<lambda>n x. f n x / (x - z) ^ Suc m - g x / (x - z) ^ Suc m) 
+             (\<lambda>x. g x / (x - z) ^ Suc m - g x / (x - z) ^ Suc m) F"
+      by (intro uniform_limit_intros)
+    thus ?thesis
+      by (simp add: h_def diff_divide_distrib)
+  qed
+
+  have has_integral: "eventually (\<lambda>n. ((\<lambda>u. h n u / (u - z) ^ Suc m) has_contour_integral 
+                         c * (deriv ^^ m) (h n) z) (circlepath z r)) F"
+    using f_holo
+  proof eventually_elim
+    case (elim n)
+    show ?case
+      unfolding c_def
+    proof (rule Cauchy_has_contour_integral_higher_derivative_circlepath)
+      show "continuous_on (cball z r) (h n)" unfolding h_def 
+        by (intro continuous_intros g_cont holomorphic_on_imp_continuous_on
+                  holomorphic_on_subset[OF elim] r)
+      show "h n holomorphic_on ball z r"
+        unfolding h_def by (intro holomorphic_intros g_holo holomorphic_on_subset[OF elim] r')
+    qed (use r(1) in auto)
+  qed
+
+  have "((\<lambda>n. contour_integral (circlepath z r) (\<lambda>u. h n u / (u - z) ^ Suc m)) \<longlongrightarrow> 
+         contour_integral (circlepath z r) (\<lambda>u. 0 / (u - z) ^ Suc m)) F"
+  proof (rule contour_integral_uniform_limit_circlepath)
+    show "\<forall>\<^sub>F n in F. (\<lambda>u. h n u / (u - z) ^ Suc m) contour_integrable_on circlepath z r"
+      using has_integral by eventually_elim (blast intro: has_contour_integral_integrable)
+  qed (use r(1) \<open>F \<noteq> bot\<close> ulim' in simp_all)
+  hence "((\<lambda>n. contour_integral (circlepath z r) (\<lambda>u. h n u / (u - z) ^ Suc m)) \<longlongrightarrow> 0) F"
+    by simp
+  also have "?this \<longleftrightarrow> ((\<lambda>n. c * (deriv ^^ m) (h n) z) \<longlongrightarrow> 0) F"
+  proof (rule tendsto_cong)
+    show "\<forall>\<^sub>F x in F. contour_integral (circlepath z r) (\<lambda>u. h x u / (u - z) ^ Suc m) =
+                       c * (deriv ^^ m) (h x) z"
+      using has_integral by eventually_elim (simp add: contour_integral_unique)
+  qed
+  finally have "((\<lambda>n. (deriv ^^ m) g z + c * (deriv ^^ m) (h n) z / c) \<longlongrightarrow> 
+                  (deriv ^^ m) g z + 0 / c) F"
+    by (intro tendsto_intros) auto
+  also have "?this \<longleftrightarrow> ((\<lambda>n. (deriv ^^ m) (f n) z) \<longlongrightarrow> (deriv ^^ m) g z) F"
+  proof (intro filterlim_cong)
+    show "\<forall>\<^sub>F n in F. (deriv ^^ m) g z + c * (deriv ^^ m) (h n) z / c = (deriv ^^ m) (f n) z"
+      using f_holo
+    proof eventually_elim
+      case (elim n)
+      have "(deriv ^^ m) (h n) z = (deriv ^^ m) (f n) z - (deriv ^^ m) g z" unfolding h_def
+        by (rule higher_deriv_diff holomorphic_on_subset[OF elim r'] g_holo A)+ (use r(1) in auto)
+      thus ?case
+        by simp
+    qed
+  qed auto
+  finally show ?thesis .
+qed
+
 
 text\<open> Version showing that the limit is the limit of the derivatives.\<close>
 
diff -r 40a609d67b33 -r 1fa80133027d src/HOL/Complex_Analysis/Meromorphic.thy
--- a/src/HOL/Complex_Analysis/Meromorphic.thy	Wed Apr 09 22:37:58 2025 +0200
+++ b/src/HOL/Complex_Analysis/Meromorphic.thy	Wed Apr 09 22:45:04 2025 +0200
@@ -618,6 +618,11 @@
     by (auto simp: isCont_def)
 qed
   
+lemma analytic_on_imp_nicely_meromorphic_on:
+  "f analytic_on A \<Longrightarrow> f nicely_meromorphic_on A"
+  by (meson analytic_at_imp_isCont analytic_on_analytic_at
+            analytic_on_imp_meromorphic_on isContD nicely_meromorphic_on_def)
+
 lemma remove_sings_meromorphic [meromorphic_intros]:
   assumes "f meromorphic_on A"
   shows   "remove_sings f meromorphic_on A"
diff -r 40a609d67b33 -r 1fa80133027d src/HOL/Computational_Algebra/Nth_Powers.thy
--- a/src/HOL/Computational_Algebra/Nth_Powers.thy	Wed Apr 09 22:37:58 2025 +0200
+++ b/src/HOL/Computational_Algebra/Nth_Powers.thy	Wed Apr 09 22:45:04 2025 +0200
@@ -45,7 +45,7 @@
   by (auto simp: is_nth_power_def intro!: exI[of _ 1])
 
 lemma is_nth_power_Suc_0 [simp]: "is_nth_power n (Suc 0)"
-  by (simp add: One_nat_def [symmetric] del: One_nat_def)
+  by (metis One_nat_def is_nth_power_1)
 
 lemma is_nth_power_conv_multiplicity: 
   fixes x :: "'a :: {factorial_semiring, normalization_semidom_multiplicative}"
@@ -58,7 +58,7 @@
     fix y p :: 'a assume *: "normalize x = y ^ n" "prime p"
     with assms and False have [simp]: "y \<noteq> 0" by (auto simp: power_0_left)
     have "multiplicity p x = multiplicity p (y ^ n)"
-      by (subst *(1) [symmetric]) simp
+      by (metis "*"(1) multiplicity_normalize_right)
     with False and * and assms show "n dvd multiplicity p x"
       by (auto simp: prime_elem_multiplicity_power_distrib)
   next
@@ -88,11 +88,7 @@
 lemma is_nth_power_mult:
   assumes "is_nth_power n a" "is_nth_power n b"
   shows   "is_nth_power n (a * b :: 'a :: comm_monoid_mult)"
-proof -
-  from assms obtain a' b' where "a = a' ^ n" "b = b' ^ n" by (auto elim!: is_nth_powerE)
-  hence "a * b = (a' * b') ^ n" by (simp add: power_mult_distrib)
-  thus ?thesis by (rule is_nth_powerI)
-qed
+  by (metis assms is_nth_power_def power_mult_distrib)
     
 lemma is_nth_power_mult_coprime_natD:
   fixes a b :: nat
@@ -136,12 +132,7 @@
 lemma is_nth_power_nth_power': 
   assumes "n dvd n'"
   shows   "is_nth_power n (m ^ n')"
-proof -
-  from assms have "n' = n' div n * n" by simp
-  also have "m ^ \<dots> = (m ^ (n' div n)) ^ n" by (simp add: power_mult)
-  also have "is_nth_power n \<dots>" by simp
-  finally show ?thesis .
-qed
+  by (metis assms dvd_div_mult_self is_nth_power_def power_mult)
 
 definition is_nth_power_nat :: "nat \<Rightarrow> nat \<Rightarrow> bool"
   where [code_abbrev]: "is_nth_power_nat = is_nth_power"
@@ -154,6 +145,36 @@
       else (\<exists>k\<in>{1..m}. k ^ n = m))"
   by (auto simp: is_nth_power_nat_def is_nth_power_def power_eq_iff_eq_base self_le_power)
 
+lemma is_nth_power_mult_cancel_left:
+  fixes a b :: "'a :: semiring_gcd"
+  assumes "is_nth_power n a" "a \<noteq> 0"
+  shows   "is_nth_power n (a * b) \<longleftrightarrow> is_nth_power n b"
+proof (cases "n > 0")
+  case True
+  show ?thesis
+  proof
+    assume "is_nth_power n (a * b)"
+    then obtain x where x: "a * b = x ^ n"
+      by (elim is_nth_powerE)
+    obtain y where y: "a = y ^ n"
+      using assms by (elim is_nth_powerE)
+    have "y ^ n dvd x ^ n"
+      by (simp flip: x y)
+    hence "y dvd x"
+      using \<open>n > 0\<close> by simp
+    then obtain z where z: "x = y * z"
+      by (elim dvdE)
+    with \<open>a \<noteq> 0\<close> show "is_nth_power n b"
+      by (metis  is_nth_powerI mult_left_cancel power_mult_distrib x y)
+  qed (use assms in \<open>auto intro: is_nth_power_mult\<close>)
+qed (use assms in auto)
+
+lemma is_nth_power_mult_cancel_right:
+  fixes a b :: "'a :: semiring_gcd"
+  assumes "is_nth_power n b" "b \<noteq> 0"
+  shows   "is_nth_power n (a * b) \<longleftrightarrow> is_nth_power n a"
+  by (metis assms is_nth_power_mult_cancel_left mult.commute)
+
 
 (* TODO: Harmonise with Discrete_Functions.floor_sqrt *)
 
@@ -201,11 +222,8 @@
 lemma nth_root_nat_less: 
   assumes "k > 0" "x ^ k > n"
   shows   "nth_root_nat k n < x"
-proof -
-  from \<open>k > 0\<close> have "nth_root_nat k n ^ k \<le> n" by (rule nth_root_nat_power_le)
-  also have "n < x ^ k" by fact
-  finally show ?thesis by (rule power_less_imp_less_base) simp_all
-qed
+  by (meson assms nth_root_nat_power_le order.strict_trans1 power_less_imp_less_base
+      zero_le)
 
 lemma nth_root_nat_unique:
   assumes "m ^ k \<le> n" "(m + 1) ^ k > n"
@@ -219,11 +237,15 @@
   ultimately show ?thesis by (rule antisym)
 qed (insert assms, auto)
 
-lemma nth_root_nat_0 [simp]: "nth_root_nat k 0 = 0" by (simp add: nth_root_nat_def)
+lemma nth_root_nat_0 [simp]: "nth_root_nat k 0 = 0" 
+  by (simp add: nth_root_nat_def)
+
 lemma nth_root_nat_1 [simp]: "k > 0 \<Longrightarrow> nth_root_nat k 1 = 1"
   by (rule nth_root_nat_unique) (auto simp del: One_nat_def)
+
 lemma nth_root_nat_Suc_0 [simp]: "k > 0 \<Longrightarrow> nth_root_nat k (Suc 0) = Suc 0"
-  using nth_root_nat_1 by (simp del: nth_root_nat_1)
+  using One_nat_def is_nth_power_nat_def nth_root_nat_1
+  by presburger
 
 lemma first_root_nat [simp]: "nth_root_nat 1 n = n"
   by (intro nth_root_nat_unique) auto
@@ -265,7 +287,8 @@
   proof -
     note that
     also have "k < Suc k ^ 1" by simp
-    also from \<open>m > 0\<close> have "\<dots> \<le> Suc k ^ m" by (intro power_increasing) simp_all
+    also from \<open>m > 0\<close> have "\<dots> \<le> Suc k ^ m" 
+      by (intro power_increasing) simp_all
     finally show ?thesis .
   qed
   with 1 show ?case by (auto simp: Let_def)
@@ -274,7 +297,7 @@
 lemma nth_root_nat_aux_correct:
   assumes "k ^ m \<le> n" "m > 0"
   shows   "nth_root_nat_aux m k (k ^ m) n = nth_root_nat m n"
-  by (rule sym, intro nth_root_nat_unique nth_root_nat_aux_le nth_root_nat_aux_gt assms)
+  by (metis assms nth_root_nat_aux_gt nth_root_nat_aux_le nth_root_nat_unique)
 
 lemma nth_root_nat_naive_code [code]:
   "nth_root_nat m n = (if m = 0 \<or> n = 0 then 0 else if m = 1 \<or> n = 1 then n else
@@ -288,12 +311,7 @@
 lemma nth_root_nat_nth_power':
   assumes "k > 0" "k dvd m" 
   shows   "nth_root_nat k (n ^ m) = n ^ (m div k)"
-proof -
-  from assms have "m = (m div k) * k" by simp
-  also have "n ^ \<dots> = (n ^ (m div k)) ^ k" by (simp add: power_mult)
-  also from assms have "nth_root_nat k \<dots> = n ^ (m div k)" by simp
-  finally show ?thesis .
-qed
+  by (metis assms dvd_div_mult_self nth_root_nat_nth_power power_mult)
 
 lemma nth_root_nat_mono:
   assumes "m \<le> n"
diff -r 40a609d67b33 -r 1fa80133027d src/HOL/Library/Nonpos_Ints.thy
--- a/src/HOL/Library/Nonpos_Ints.thy	Wed Apr 09 22:37:58 2025 +0200
+++ b/src/HOL/Library/Nonpos_Ints.thy	Wed Apr 09 22:45:04 2025 +0200
@@ -305,4 +305,101 @@
 lemma ii_not_nonpos_Reals [iff]: "\<i> \<notin> \<real>\<^sub>\<le>\<^sub>0"
   by (simp add: complex_nonpos_Reals_iff)
 
+lemma plus_one_in_nonpos_Ints_imp: "z + 1 \<in> \<int>\<^sub>\<le>\<^sub>0 \<Longrightarrow> z \<in> \<int>\<^sub>\<le>\<^sub>0"
+  using nonpos_Ints_diff_Nats[of "z+1" "1"] by simp_all
+
+lemma of_int_in_nonpos_Ints_iff:
+  "(of_int n :: 'a :: ring_char_0) \<in> \<int>\<^sub>\<le>\<^sub>0 \<longleftrightarrow> n \<le> 0"
+  by (auto simp: nonpos_Ints_def)
+
+lemma one_plus_of_int_in_nonpos_Ints_iff:
+  "(1 + of_int n :: 'a :: ring_char_0) \<in> \<int>\<^sub>\<le>\<^sub>0 \<longleftrightarrow> n \<le> -1"
+proof -
+  have "1 + of_int n = (of_int (n + 1) :: 'a)" by simp
+  also have "\<dots> \<in> \<int>\<^sub>\<le>\<^sub>0 \<longleftrightarrow> n + 1 \<le> 0" by (subst of_int_in_nonpos_Ints_iff) simp_all
+  also have "\<dots> \<longleftrightarrow> n \<le> -1" by presburger
+  finally show ?thesis .
+qed
+
+lemma one_minus_of_nat_in_nonpos_Ints_iff:
+  "(1 - of_nat n :: 'a :: ring_char_0) \<in> \<int>\<^sub>\<le>\<^sub>0 \<longleftrightarrow> n > 0"
+proof -
+  have "(1 - of_nat n :: 'a) = of_int (1 - int n)" by simp
+  also have "\<dots> \<in> \<int>\<^sub>\<le>\<^sub>0 \<longleftrightarrow> n > 0" by (subst of_int_in_nonpos_Ints_iff) presburger
+  finally show ?thesis .
+qed
+
+lemma fraction_not_in_ints:
+  assumes "\<not>(n dvd m)" "n \<noteq> 0"
+  shows   "of_int m / of_int n \<notin> (\<int> :: 'a :: {division_ring,ring_char_0} set)"
+proof
+  assume "of_int m / (of_int n :: 'a) \<in> \<int>"
+  then obtain k where "of_int m / of_int n = (of_int k :: 'a)" by (elim Ints_cases)
+  with assms have "of_int m = (of_int (k * n) :: 'a)" by (auto simp add: field_split_simps)
+  hence "m = k * n" by (subst (asm) of_int_eq_iff)
+  hence "n dvd m" by simp
+  with assms(1) show False by contradiction
+qed
+
+lemma fraction_not_in_nats:
+  assumes "\<not>n dvd m" "n \<noteq> 0"
+  shows   "of_int m / of_int n \<notin> (\<nat> :: 'a :: {division_ring,ring_char_0} set)"
+proof
+  assume "of_int m / of_int n \<in> (\<nat> :: 'a set)"
+  also note Nats_subset_Ints
+  finally have "of_int m / of_int n \<in> (\<int> :: 'a set)" .
+  moreover have "of_int m / of_int n \<notin> (\<int> :: 'a set)"
+    using assms by (intro fraction_not_in_ints)
+  ultimately show False by contradiction
+qed
+
+lemma not_in_Ints_imp_not_in_nonpos_Ints: "z \<notin> \<int> \<Longrightarrow> z \<notin> \<int>\<^sub>\<le>\<^sub>0"
+  by (auto simp: Ints_def nonpos_Ints_def)
+
+lemma double_in_nonpos_Ints_imp:
+  assumes "2 * (z :: 'a :: field_char_0) \<in> \<int>\<^sub>\<le>\<^sub>0"
+  shows   "z \<in> \<int>\<^sub>\<le>\<^sub>0 \<or> z + 1/2 \<in> \<int>\<^sub>\<le>\<^sub>0"
+proof-
+  from assms obtain k where k: "2 * z = - of_nat k" by (elim nonpos_Ints_cases')
+  thus ?thesis by (cases "even k") (auto elim!: evenE oddE simp: field_simps)
+qed
+
+lemma fraction_numeral_Ints_iff [simp]:
+  "numeral a / numeral b \<in> (\<int> :: 'a :: {division_ring, ring_char_0} set)
+   \<longleftrightarrow> (numeral b :: int) dvd numeral a"  (is "?L=?R")
+proof
+  show "?L \<Longrightarrow> ?R"
+    by (metis fraction_not_in_ints of_int_numeral zero_neq_numeral)
+  assume ?R
+  then obtain k::int where "numeral a = numeral b * (of_int k :: 'a)"
+    unfolding dvd_def by (metis of_int_mult of_int_numeral)
+  then show ?L
+    by (metis Ints_of_int divide_eq_eq mult.commute of_int_mult of_int_numeral)
+qed
+
+lemma fraction_numeral_Ints_iff1 [simp]:
+  "1 / numeral b \<in> (\<int> :: 'a :: {division_ring, ring_char_0} set)
+   \<longleftrightarrow> b = Num.One"  (is "?L=?R")
+  using fraction_numeral_Ints_iff [of Num.One, where 'a='a] by simp
+
+lemma fraction_numeral_Nats_iff [simp]:
+  "numeral a / numeral b \<in> (\<nat> :: 'a :: {division_ring, ring_char_0} set)
+   \<longleftrightarrow> (numeral b :: int) dvd numeral a"  (is "?L=?R")
+proof
+  show "?L \<Longrightarrow> ?R"
+    using Nats_subset_Ints fraction_numeral_Ints_iff by blast
+  assume ?R
+  then obtain k::nat where "numeral a = numeral b * (of_nat k :: 'a)"
+    unfolding dvd_def
+    by (metis dvd_def int_dvd_int_iff of_nat_mult of_nat_numeral)
+  then show ?L
+    by (metis mult_of_nat_commute nonzero_divide_eq_eq of_nat_in_Nats
+        zero_neq_numeral)
+qed
+
+lemma fraction_numeral_Nats_iff1 [simp]:
+  "1 / numeral b \<in> (\<nat> :: 'a :: {division_ring, ring_char_0} set)
+   \<longleftrightarrow> b = Num.One"  (is "?L=?R")
+  using fraction_numeral_Nats_iff [of Num.One, where 'a='a] by simp
+
 end
diff -r 40a609d67b33 -r 1fa80133027d src/HOL/Try0_HOL.thy
--- a/src/HOL/Try0_HOL.thy	Wed Apr 09 22:37:58 2025 +0200
+++ b/src/HOL/Try0_HOL.thy	Wed Apr 09 22:45:04 2025 +0200
@@ -43,7 +43,6 @@
    ("force", (false, (false, full_attrs))),
    ("meson", (false, (false, metis_attrs))),
    ("satx", (false, (false, no_attrs))),
-   ("iprover", (false, (false, no_attrs))),
    ("order", (true, (false, no_attrs)))]
 
 in
@@ -64,7 +63,7 @@
 \<close>
 
 declare [[try0_schedule = "
-  satx iprover metis |
+  satx metis |
   order presburger linarith algebra argo |
   simp auto blast fast fastforce force meson
 "]]