# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1749231389 -3600
# Node ID cccbfa567117415ab061d2e2ca866606831e2395
# Parent  817f97d8cd26ae1d375ac52856cb4526c67528be
Sylvestre's correction to ex_least_nat_le and other tidying

diff -r 817f97d8cd26 -r cccbfa567117 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Fri Jun 06 16:18:44 2025 +0100
+++ b/src/HOL/Nat.thy	Fri Jun 06 18:36:29 2025 +0100
@@ -1004,7 +1004,7 @@
 
 lemma ex_least_nat_le:
   fixes P :: "nat \<Rightarrow> bool"
-  assumes "P n" "\<not> P 0" 
+  assumes "P n"
   shows "\<exists>k\<le>n. (\<forall>i<k. \<not> P i) \<and> P k"
 proof (cases n)
   case (Suc m)
@@ -1019,7 +1019,7 @@
 proof (cases n)
   case (Suc m)
   then obtain k where k: "k \<le> n" "\<forall>i<k. \<not> P i" "P k"
-    using ex_least_nat_le [OF assms] by blast
+    using ex_least_nat_le \<open>P n\<close> by blast
   show ?thesis 
     by (cases k) (use assms k less_eq_Suc_le in auto)
 qed (use assms in auto)
diff -r 817f97d8cd26 -r cccbfa567117 src/HOL/Number_Theory/Pocklington.thy
--- a/src/HOL/Number_Theory/Pocklington.thy	Fri Jun 06 16:18:44 2025 +0100
+++ b/src/HOL/Number_Theory/Pocklington.thy	Fri Jun 06 18:36:29 2025 +0100
@@ -11,11 +11,14 @@
 subsection \<open>Lemmas about previously defined terms\<close>
 
 lemma prime_nat_iff'': "prime (p::nat) \<longleftrightarrow> p \<noteq> 0 \<and> p \<noteq> 1 \<and> (\<forall>m. 0 < m \<and> m < p \<longrightarrow> coprime p m)"
-  apply (auto simp add: prime_nat_iff)
-   apply (rule coprimeI)
-   apply (auto dest: nat_dvd_not_less simp add: ac_simps)
-  apply (metis One_nat_def dvd_1_iff_1 dvd_pos_nat gcd_nat.order_iff is_unit_gcd linorder_neqE_nat nat_dvd_not_less)
-  done
+proof -
+have \<section>: "\<And>m. \<lbrakk>0 < p; \<forall>m. 0 < m \<and> m < p \<longrightarrow> coprime p m; m dvd p; m \<noteq> p\<rbrakk>
+         \<Longrightarrow> m = Suc 0"
+  by (metis One_nat_def coprime_absorb_right dvd_1_iff_1 dvd_nat_bounds
+      nless_le)
+  show ?thesis
+    by (auto simp: nat_dvd_not_less prime_imp_coprime_nat prime_nat_iff elim!: \<section>)
+qed
 
 lemma finite_number_segment: "card { m. 0 < m \<and> m < n } = n - 1"
 proof -
@@ -38,7 +41,7 @@
   case False
   from bezout_add_strong_nat [OF this]
   obtain d x y where dxy: "d dvd a" "d dvd n" "a * x = n * y + d" by blast
-  from dxy(1,2) have d1: "d = 1"
+  then have d1: "d = 1"
     using assms coprime_common_divisor [of a n d] by simp
   with dxy(3) have "a * x * b = (n * y + 1) * b"
     by simp
@@ -181,25 +184,6 @@
   qed
 qed (use n in auto)
 
-lemma nat_exists_least_iff: "(\<exists>(n::nat). P n) \<longleftrightarrow> (\<exists>n. P n \<and> (\<forall>m < n. \<not> P m))"
-  by (metis ex_least_nat_le not_less0)
-
-lemma nat_exists_least_iff': "(\<exists>(n::nat). P n) \<longleftrightarrow> P (Least P) \<and> (\<forall>m < (Least P). \<not> P m)"
-  (is "?lhs \<longleftrightarrow> ?rhs")
-proof
-  show ?lhs if ?rhs
-    using that by blast
-  show ?rhs if ?lhs
-  proof -
-    from \<open>?lhs\<close> obtain n where n: "P n" by blast
-    let ?x = "Least P"
-    have "\<not> P m" if "m < ?x" for m
-      by (rule not_less_Least[OF that])
-    with LeastI_ex[OF \<open>?lhs\<close>] show ?thesis
-      by blast
-  qed
-qed
-
 theorem lucas:
   assumes n2: "n \<ge> 2" and an1: "[a^(n - 1) = 1] (mod n)"
     and pn: "\<forall>p. prime p \<and> p dvd n - 1 \<longrightarrow> [a^((n - 1) div p) \<noteq> 1] (mod n)"
@@ -214,7 +198,7 @@
     using \<open>n \<ge> 2\<close> by simp_all
   have False if H0: "\<exists>m. 0 < m \<and> m < n - 1 \<and> [a ^ m = 1] (mod n)" (is "\<exists>m. ?P m")
   proof -
-    from H0[unfolded nat_exists_least_iff[of ?P]] obtain m where
+    from H0[unfolded exists_least_iff[of ?P]] obtain m where
       m: "0 < m" "m < n - 1" "[a ^ m = 1] (mod n)" "\<forall>k <m. \<not>?P k"
       by blast
     have False if nm1: "(n - 1) mod m > 0"
@@ -302,7 +286,7 @@
     with assms show ?thesis
       by auto
   qed
-  from nat_exists_least_iff'[of ?P] ex assms show ?thesis
+  from exists_least_iff'[of ?P] ex assms show ?thesis
     unfolding o[symmetric] by auto
 qed
 
diff -r 817f97d8cd26 -r cccbfa567117 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Fri Jun 06 16:18:44 2025 +0100
+++ b/src/HOL/Orderings.thy	Fri Jun 06 18:36:29 2025 +0100
@@ -1392,6 +1392,10 @@
   with LeastI_ex[OF H] show ?rhs by blast
 qed
 
+lemma exists_least_iff': 
+  shows "(\<exists>n. P n) \<longleftrightarrow> P (Least P) \<and> (\<forall>m < (Least P). \<not> P m)"
+  using LeastI_ex not_less_Least by auto
+
 end