# HG changeset patch
# User haftmann
# Date 1762110103 -3600
# Node ID 518a1464f1ac0a3353267707765026d6671feb25
# Parent  1cf4f1e930afef71ca0b61353a82754c489abd1f
more efficient naive prime test

diff -r 1cf4f1e930af -r 518a1464f1ac src/HOL/Computational_Algebra/Computation_Checks.thy
--- a/src/HOL/Computational_Algebra/Computation_Checks.thy	Sun Nov 02 19:47:30 2025 +0100
+++ b/src/HOL/Computational_Algebra/Computation_Checks.thy	Sun Nov 02 20:01:43 2025 +0100
@@ -13,11 +13,19 @@
 \<close>
 
 text \<open>
-  @{lemma \<open>prime (997 :: nat)\<close> by eval}
+  @{lemma \<open>prime (97 :: nat)\<close> by simp}
 \<close>
 
 text \<open>
-  @{lemma \<open>prime (997 :: int)\<close> by eval}
+  @{lemma \<open>prime (97 :: int)\<close> by simp}
+\<close>
+
+text \<open>
+  @{lemma \<open>prime (9973 :: nat)\<close> by eval}
+\<close>
+
+text \<open>
+  @{lemma \<open>prime (9973 :: int)\<close> by eval}
 \<close>
 
 text \<open>
diff -r 1cf4f1e930af -r 518a1464f1ac src/HOL/Computational_Algebra/Primes.thy
--- a/src/HOL/Computational_Algebra/Primes.thy	Sun Nov 02 19:47:30 2025 +0100
+++ b/src/HOL/Computational_Algebra/Primes.thy	Sun Nov 02 20:01:43 2025 +0100
@@ -226,6 +226,21 @@
     using prime_nat_naiveI [of n] by auto
 qed
 
+lemma prime_nat_iff':
+  "prime (p :: nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {2..<p}. \<not> n dvd p)"
+proof safe
+  assume "p > 1" and *: "\<forall>n\<in>{2..<p}. \<not>n dvd p"
+  show "prime p" unfolding prime_nat_iff
+  proof (intro conjI allI impI)
+    fix m assume "m dvd p"
+    with \<open>p > 1\<close> have "m \<noteq> 0" by (intro notI) auto
+    hence "m \<ge> 1" by simp
+    moreover from \<open>m dvd p\<close> and * have "m \<notin> {2..<p}" by blast
+    with \<open>m dvd p\<close> and \<open>p > 1\<close> have "m \<le> 1 \<or> m = p" by (auto dest: dvd_imp_le)
+    ultimately show "m = 1 \<or> m = p" by simp
+  qed fact+
+qed (auto simp: prime_nat_iff)
+
 lemma prime_int_iff:
   "prime (n::int) \<longleftrightarrow> (1 < n \<and> (\<forall>m. m \<ge> 0 \<and> m dvd n \<longrightarrow> m = 1 \<or> m = n))"
 proof (intro iffI conjI allI impI; (elim conjE)?)
@@ -256,6 +271,23 @@
     unfolding prime_int_nat_transfer prime_nat_iff by auto
 qed
 
+lemma prime_int_iff':
+  "prime (p :: int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {2..<p}. \<not> n dvd p)" (is "?P \<longleftrightarrow> ?Q")
+proof (cases "p \<ge> 0")
+  case True
+  have "?P \<longleftrightarrow> prime (nat p)"
+    by simp
+  also have "\<dots> \<longleftrightarrow> p > 1 \<and> (\<forall>n\<in>{2..<nat p}. \<not> n dvd nat \<bar>p\<bar>)"
+    using True by (simp add: prime_nat_iff')
+  also have "{2..<nat p} = nat ` {2..<p}"
+    using True int_eq_iff by fastforce
+  finally show "?P \<longleftrightarrow> ?Q" by simp
+next
+  case False
+  then show ?thesis
+    by (auto simp add: prime_ge_0_int)
+qed
+
 lemma prime_nat_not_dvd:
   assumes "prime p" "p > n" "n \<noteq> (1::nat)"
   shows   "\<not>n dvd p"
@@ -293,9 +325,119 @@
   using assms irreducible_altdef[of m]
   by (auto simp: prime_elem_iff_irreducible irreducible_altdef)
 
-    
+
+subsection \<open>Make prime naively executable\<close>
+
+lemma prime_int_numeral_eq [simp]:
+  "prime (numeral m :: int) \<longleftrightarrow> prime (numeral m :: nat)"
+  by (simp add: prime_int_nat_transfer)
+
+class check_prime_by_range = normalization_semidom + discrete_linordered_semidom +
+  assumes prime_iff: \<open>prime a \<longleftrightarrow> 1 < a \<and> (\<forall>d\<in>{2..a div 2}. \<not> d dvd a)\<close>
+begin
+
+lemma two_is_prime [simp]:
+  \<open>prime 2\<close>
+  by (simp add: prime_iff)
+
+end
+
+lemma divisor_less_eq_half_nat:
+  \<open>m \<le> n div 2\<close> if \<open>m dvd n\<close> \<open>m < n\<close> for m n :: nat
+  using that by (auto simp add: less_eq_div_iff_mult_less_eq)
+
+instance nat :: check_prime_by_range
+  apply standard
+  apply (auto simp add: prime_nat_iff)
+  apply (rule ccontr)
+  apply (auto simp add: neq_iff)
+  apply (metis One_nat_def Suc_1 Suc_leI atLeastAtMost_iff divisor_less_eq_half_nat)
+  done
+
+lemma two_is_prime_nat [simp]:
+  \<open>prime (2::nat)\<close>
+  by (fact two_is_prime)
+
+lemma divisor_less_eq_half_int:
+  \<open>k \<le> l div 2\<close> if \<open>k dvd l\<close> \<open>k < l\<close> \<open>l \<ge> 0\<close> \<open>k \<ge> 0\<close> for k l :: int
+proof -
+  define m n where \<open>m = nat \<bar>k\<bar>\<close> \<open>n = nat \<bar>l\<bar>\<close>
+  with \<open>l \<ge> 0\<close> \<open>k \<ge> 0\<close> have \<open>k = int m\<close> \<open>l = int n\<close>
+    by simp_all
+  with that show ?thesis
+    using divisor_less_eq_half_nat [of m n] by simp
+qed
+
+instance int :: check_prime_by_range
+  apply standard
+  apply (auto simp add: prime_int_iff)
+  apply (smt (verit) int_div_less_self)
+  apply (rule ccontr)
+  apply (auto simp add: neq_iff zdvd_not_zless)
+  apply (metis div_by_0 dvd_div_eq_0_iff less_le_not_le one_dvd order_le_less
+      zdvd_not_zless)
+  apply (metis atLeastAtMost_iff divisor_less_eq_half_int dvd_div_eq_0_iff
+      int_one_le_iff_zero_less nle_le one_add_one pos_imp_zdiv_nonneg_iff zdiv_eq_0_iff
+      zless_imp_add1_zle)
+  done
+
+lemma prime_nat_numeral_eq [simp]: \<comment> \<open>TODO Sieve Of Erathosthenes might speed this up\<close>
+  "prime (numeral m :: nat) \<longleftrightarrow>
+    (1::nat) < numeral m \<and>
+    (\<forall>n::nat \<in> set [2..<Suc (numeral m div 2)]. \<not> n dvd numeral m)"
+  using prime_iff [of \<open>numeral m :: nat\<close>]
+  by (simp only: set_upt atLeastLessThanSuc_atLeastAtMost)
+
+context check_prime_by_range
+begin
+
+definition check_divisors :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool\<close>
+  where \<open>check_divisors l u a \<longleftrightarrow> (\<forall>d\<in>{l..u}. \<not> d dvd a)\<close>
+
+lemma check_divisors_rec [code]:
+  \<open>check_divisors l u a \<longleftrightarrow> u < l \<or> (\<not> l dvd a \<and> check_divisors (l + 1) u a)\<close>
+  apply (auto simp add: check_divisors_def not_less)
+  apply (metis local.add_increasing2 local.atLeastAtMost_iff local.linear local.order_eq_iff
+      local.zero_le_one)
+  subgoal for d
+    apply (cases \<open>l + 1 \<le> d\<close>)
+     apply (auto simp add: not_le)
+    apply (metis local.dual_order.antisym local.less_eq_iff_succ_less)
+    done
+  done
+
+lemma prime_eq_check_divisors [code]:
+  \<open>prime a \<longleftrightarrow> a > 1 \<and> check_divisors 2 (a div 2) a\<close>
+  by (simp add: check_divisors_def prime_iff)
+
+end
+
+
 subsection \<open>Largest exponent of a prime factor\<close>
 
+lemma prime_factor_nat:
+  "n \<noteq> (1::nat) \<Longrightarrow> \<exists>p. prime p \<and> p dvd n"
+  using prime_divisor_exists[of n]
+  by (cases "n = 0") (auto intro: exI[of _ "2::nat"])
+
+lemma prime_factor_int:
+  fixes k :: int
+  assumes "\<bar>k\<bar> \<noteq> 1"
+  obtains p where "prime p" "p dvd k"
+proof (cases "k = 0")
+  case True
+  then have "prime (2::int)" and "2 dvd k"
+    by simp_all
+  with that show thesis
+    by blast
+next
+  case False
+  with assms prime_divisor_exists [of k] obtain p where "prime p" "p dvd k"
+    by auto
+  with that show thesis
+    by blast
+qed
+
 text\<open>Possibly duplicates other material, but avoid the complexities of multisets.\<close>
   
 lemma prime_power_cancel_less:
@@ -353,83 +495,6 @@
 qed
 
 
-subsubsection \<open>Make prime naively executable\<close>
-
-lemma prime_nat_iff':
-  "prime (p :: nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {2..<p}. \<not> n dvd p)"
-proof safe
-  assume "p > 1" and *: "\<forall>n\<in>{2..<p}. \<not>n dvd p"
-  show "prime p" unfolding prime_nat_iff
-  proof (intro conjI allI impI)
-    fix m assume "m dvd p"
-    with \<open>p > 1\<close> have "m \<noteq> 0" by (intro notI) auto
-    hence "m \<ge> 1" by simp
-    moreover from \<open>m dvd p\<close> and * have "m \<notin> {2..<p}" by blast
-    with \<open>m dvd p\<close> and \<open>p > 1\<close> have "m \<le> 1 \<or> m = p" by (auto dest: dvd_imp_le)
-    ultimately show "m = 1 \<or> m = p" by simp
-  qed fact+
-qed (auto simp: prime_nat_iff)
-
-lemma prime_int_iff':
-  "prime (p :: int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {2..<p}. \<not> n dvd p)" (is "?P \<longleftrightarrow> ?Q")
-proof (cases "p \<ge> 0")
-  case True
-  have "?P \<longleftrightarrow> prime (nat p)"
-    by simp
-  also have "\<dots> \<longleftrightarrow> p > 1 \<and> (\<forall>n\<in>{2..<nat p}. \<not> n dvd nat \<bar>p\<bar>)"
-    using True by (simp add: prime_nat_iff')
-  also have "{2..<nat p} = nat ` {2..<p}"
-    using True int_eq_iff by fastforce 
-  finally show "?P \<longleftrightarrow> ?Q" by simp
-next
-  case False
-  then show ?thesis
-    by (auto simp add: prime_ge_0_int) 
-qed
-
-lemma prime_int_numeral_eq [simp]:
-  "prime (numeral m :: int) \<longleftrightarrow> prime (numeral m :: nat)"
-  by (simp add: prime_int_nat_transfer)
-
-lemma two_is_prime_nat [simp]: "prime (2::nat)"
-  by (simp add: prime_nat_iff')
-
-lemma prime_nat_numeral_eq [simp]:
-  "prime (numeral m :: nat) \<longleftrightarrow>
-    (1::nat) < numeral m \<and>
-    (\<forall>n::nat \<in> set [2..<numeral m]. \<not> n dvd numeral m)"
-  by (simp only: prime_nat_iff' set_upt)  \<comment> \<open>TODO Sieve Of Erathosthenes might speed this up\<close>
-
-
-text\<open>A bit of regression testing:\<close>
-
-lemma "prime(97::nat)" by simp
-lemma "prime(97::int)" by simp
-
-lemma prime_factor_nat: 
-  "n \<noteq> (1::nat) \<Longrightarrow> \<exists>p. prime p \<and> p dvd n"
-  using prime_divisor_exists[of n]
-  by (cases "n = 0") (auto intro: exI[of _ "2::nat"])
-
-lemma prime_factor_int:
-  fixes k :: int
-  assumes "\<bar>k\<bar> \<noteq> 1"
-  obtains p where "prime p" "p dvd k"
-proof (cases "k = 0")
-  case True
-  then have "prime (2::int)" and "2 dvd k"
-    by simp_all
-  with that show thesis
-    by blast
-next
-  case False
-  with assms prime_divisor_exists [of k] obtain p where "prime p" "p dvd k"
-    by auto
-  with that show thesis
-    by blast
-qed
-
-
 subsection \<open>Infinitely many primes\<close>
 
 lemma next_prime_bound: "\<exists>p::nat. prime p \<and> n < p \<and> p \<le> fact n + 1"
@@ -1060,44 +1125,4 @@
 lemmas prime_divprod_pow_nat = prime_elem_divprod_pow[where ?'a = nat]
 lemmas prime_exp = prime_elem_power_iff[where ?'a = nat]
 
-text \<open>Code generation\<close>
-
-lemma divisor_less_eq_half_nat:
-  \<open>m \<le> n div 2\<close> if \<open>m dvd n\<close> \<open>m < n\<close> for m n :: nat
-  using that by (auto simp add: less_eq_div_iff_mult_less_eq)
-
-lemma divisor_less_eq_half_int:
-  \<open>k \<le> l div 2\<close> if \<open>k dvd l\<close> \<open>k < l\<close> \<open>l \<ge> 0\<close> \<open>k \<ge> 0\<close> for k l :: int
-proof -
-  define m n where \<open>m = nat \<bar>k\<bar>\<close> \<open>n = nat \<bar>l\<bar>\<close>
-  with \<open>l \<ge> 0\<close> \<open>k \<ge> 0\<close> have \<open>k = int m\<close> \<open>l = int n\<close>
-    by simp_all
-  with that show ?thesis
-    using divisor_less_eq_half_nat [of m n] by simp
-qed
-
-lemma
-  \<open>prime n \<longleftrightarrow> 1 < n \<and> (\<forall>n\<in>{1<..n div 2}. \<not> n dvd p)\<close>
-
-thm prime_nat_iff prime_int_iff [no_vars]
-
-context
-begin
-
-qualified definition prime_nat :: "nat \<Rightarrow> bool"
-  where [simp, code_abbrev]: "prime_nat = prime"
-
-lemma prime_nat_naive [code]:
-  "prime_nat p \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in>{1<..<p}. \<not> n dvd p)"
-  by (auto simp add: prime_nat_iff')
-
-qualified definition prime_int :: "int \<Rightarrow> bool"
-  where [simp, code_abbrev]: "prime_int = prime"
-
-lemma prime_int_naive [code]:
-  "prime_int p \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in>{1<..<p}. \<not> n dvd p)"
-  by (auto simp add: prime_int_iff')
-
 end
-
-end