Theory Euclid

theory Euclid
imports Primes Util Old_Datatype Code_Target_Numeral
```(*  Title:      HOL/Proofs/Extraction/Euclid.thy
Author:     Markus Wenzel, TU Muenchen
Author:     Freek Wiedijk, Radboud University Nijmegen
Author:     Stefan Berghofer, TU Muenchen
*)

section ‹Euclid's theorem›

theory Euclid
imports
"HOL-Computational_Algebra.Primes"
Util
"HOL-Library.Old_Datatype"
"HOL-Library.Code_Target_Numeral"
begin

text ‹
A constructive version of the proof of Euclid's theorem by
Markus Wenzel and Freek Wiedijk @{cite "Wenzel-Wiedijk-JAR2002"}.
›

lemma factor_greater_one1: "n = m * k ⟹ m < n ⟹ k < n ⟹ Suc 0 < m"
by (induct m) auto

lemma factor_greater_one2: "n = m * k ⟹ m < n ⟹ k < n ⟹ Suc 0 < k"
by (induct k) auto

lemma prod_mn_less_k: "0 < n ⟹ 0 < k ⟹ Suc 0 < m ⟹ m * n = k ⟹ n < k"
by (induct m) auto

lemma prime_eq: "prime (p::nat) ⟷ 1 < p ∧ (∀m. m dvd p ⟶ 1 < m ⟶ m = p)"
apply (rule iffI)
apply blast
apply (erule conjE)
apply (rule conjI)
apply assumption
apply (rule allI impI)+
apply (erule allE)
apply (erule impE)
apply assumption
apply (case_tac "m = 0")
apply simp
apply (case_tac "m = Suc 0")
apply simp
apply simp
done

lemma prime_eq': "prime (p::nat) ⟷ 1 < p ∧ (∀m k. p = m * k ⟶ 1 < m ⟶ m = p)"
by (simp add: prime_eq dvd_def HOL.all_simps [symmetric] del: HOL.all_simps)

lemma not_prime_ex_mk:
assumes n: "Suc 0 < n"
shows "(∃m k. Suc 0 < m ∧ Suc 0 < k ∧ m < n ∧ k < n ∧ n = m * k) ∨ prime n"
proof -
from nat_eq_dec have "(∃m<n. n = m * k) ∨ ¬ (∃m<n. n = m * k)" for k
by (rule search)
then have "(∃k<n. ∃m<n. n = m * k) ∨ ¬ (∃k<n. ∃m<n. n = m * k)"
by (rule search)
then show ?thesis
proof
assume "∃k<n. ∃m<n. n = m * k"
then obtain k m where k: "k<n" and m: "m<n" and nmk: "n = m * k"
by iprover
from nmk m k have "Suc 0 < m" by (rule factor_greater_one1)
moreover from nmk m k have "Suc 0 < k" by (rule factor_greater_one2)
ultimately show ?thesis using k m nmk by iprover
next
assume "¬ (∃k<n. ∃m<n. n = m * k)"
then have A: "∀k<n. ∀m<n. n ≠ m * k" by iprover
have "∀m k. n = m * k ⟶ Suc 0 < m ⟶ m = n"
proof (intro allI impI)
fix m k
assume nmk: "n = m * k"
assume m: "Suc 0 < m"
from n m nmk have k: "0 < k"
by (cases k) auto
moreover from n have n: "0 < n" by simp
moreover note m
moreover from nmk have "m * k = n" by simp
ultimately have kn: "k < n" by (rule prod_mn_less_k)
show "m = n"
proof (cases "k = Suc 0")
case True
with nmk show ?thesis by (simp only: mult_Suc_right)
next
case False
from m have "0 < m" by simp
moreover note n
moreover from False n nmk k have "Suc 0 < k" by auto
moreover from nmk have "k * m = n" by (simp only: ac_simps)
ultimately have mn: "m < n" by (rule prod_mn_less_k)
with kn A nmk show ?thesis by iprover
qed
qed
with n have "prime n"
by (simp only: prime_eq' One_nat_def simp_thms)
then show ?thesis ..
qed
qed

lemma dvd_factorial: "0 < m ⟹ m ≤ n ⟹ m dvd fact n"
proof (induct n rule: nat_induct)
case 0
then show ?case by simp
next
case (Suc n)
from ‹m ≤ Suc n› show ?case
proof (rule le_SucE)
assume "m ≤ n"
with ‹0 < m› have "m dvd fact n" by (rule Suc)
then have "m dvd (fact n * Suc n)" by (rule dvd_mult2)
then show ?thesis by (simp add: mult.commute)
next
assume "m = Suc n"
then have "m dvd (fact n * Suc n)"
by (auto intro: dvdI simp: ac_simps)
then show ?thesis by (simp add: mult.commute)
qed
qed

lemma dvd_prod [iff]: "n dvd (∏m::nat ∈# mset (n # ns). m)"

definition all_prime :: "nat list ⇒ bool"
where "all_prime ps ⟷ (∀p∈set ps. prime p)"

lemma all_prime_simps:
"all_prime []"
"all_prime (p # ps) ⟷ prime p ∧ all_prime ps"

lemma all_prime_append: "all_prime (ps @ qs) ⟷ all_prime ps ∧ all_prime qs"

lemma split_all_prime:
assumes "all_prime ms" and "all_prime ns"
shows "∃qs. all_prime qs ∧
(∏m::nat ∈# mset qs. m) = (∏m::nat ∈# mset ms. m) * (∏m::nat ∈# mset ns. m)"
(is "∃qs. ?P qs ∧ ?Q qs")
proof -
from assms have "all_prime (ms @ ns)"
moreover
have "(∏m::nat ∈# mset (ms @ ns). m) = (∏m::nat ∈# mset ms. m) * (∏m::nat ∈# mset ns. m)"
using assms by (simp add: prod_mset_Un)
ultimately have "?P (ms @ ns) ∧ ?Q (ms @ ns)" ..
then show ?thesis ..
qed

lemma all_prime_nempty_g_one:
assumes "all_prime ps" and "ps ≠ []"
shows "Suc 0 < (∏m::nat ∈# mset ps. m)"
using ‹ps ≠ []› ‹all_prime ps›
unfolding One_nat_def [symmetric]
by (induct ps rule: list_nonempty_induct)
(simp_all add: all_prime_simps prod_mset_Un prime_gt_1_nat less_1_mult del: One_nat_def)

lemma factor_exists: "Suc 0 < n ⟹ (∃ps. all_prime ps ∧ (∏m::nat ∈# mset ps. m) = n)"
proof (induct n rule: nat_wf_ind)
case (1 n)
from ‹Suc 0 < n›
have "(∃m k. Suc 0 < m ∧ Suc 0 < k ∧ m < n ∧ k < n ∧ n = m * k) ∨ prime n"
by (rule not_prime_ex_mk)
then show ?case
proof
assume "∃m k. Suc 0 < m ∧ Suc 0 < k ∧ m < n ∧ k < n ∧ n = m * k"
then obtain m k where m: "Suc 0 < m" and k: "Suc 0 < k" and mn: "m < n"
and kn: "k < n" and nmk: "n = m * k"
by iprover
from mn and m have "∃ps. all_prime ps ∧ (∏m::nat ∈# mset ps. m) = m"
by (rule 1)
then obtain ps1 where "all_prime ps1" and prod_ps1_m: "(∏m::nat ∈# mset ps1. m) = m"
by iprover
from kn and k have "∃ps. all_prime ps ∧ (∏m::nat ∈# mset ps. m) = k"
by (rule 1)
then obtain ps2 where "all_prime ps2" and prod_ps2_k: "(∏m::nat ∈# mset ps2. m) = k"
by iprover
from ‹all_prime ps1› ‹all_prime ps2›
have "∃ps. all_prime ps ∧ (∏m::nat ∈# mset ps. m) =
(∏m::nat ∈# mset ps1. m) * (∏m::nat ∈# mset ps2. m)"
by (rule split_all_prime)
with prod_ps1_m prod_ps2_k nmk show ?thesis by simp
next
assume "prime n" then have "all_prime [n]" by (simp add: all_prime_simps)
moreover have "(∏m::nat ∈# mset [n]. m) = n" by (simp)
ultimately have "all_prime [n] ∧ (∏m::nat ∈# mset [n]. m) = n" ..
then show ?thesis ..
qed
qed

lemma prime_factor_exists:
assumes N: "(1::nat) < n"
shows "∃p. prime p ∧ p dvd n"
proof -
from N obtain ps where "all_prime ps" and prod_ps: "n = (∏m::nat ∈# mset ps. m)"
using factor_exists by simp iprover
with N have "ps ≠ []"
then obtain p qs where ps: "ps = p # qs"
by (cases ps) simp
with ‹all_prime ps› have "prime p"
moreover from ‹all_prime ps› ps prod_ps have "p dvd n"
by (simp only: dvd_prod)
ultimately show ?thesis by iprover
qed

text ‹Euclid's theorem: there are infinitely many primes.›

lemma Euclid: "∃p::nat. prime p ∧ n < p"
proof -
let ?k = "fact n + (1::nat)"
have "1 < ?k" by simp
then obtain p where prime: "prime p" and dvd: "p dvd ?k"
using prime_factor_exists by iprover
have "n < p"
proof -
have "¬ p ≤ n"
proof
assume pn: "p ≤ n"
from ‹prime p› have "0 < p" by (rule prime_gt_0_nat)
then have "p dvd fact n" using pn by (rule dvd_factorial)
with dvd have "p dvd ?k - fact n" by (rule dvd_diff_nat)
then have "p dvd 1" by simp
with prime show False by auto
qed
then show ?thesis by simp
qed
with prime show ?thesis by iprover
qed

extract Euclid

text ‹
The program extracted from the proof of Euclid's theorem looks as follows.
@{thm [display] Euclid_def}
The program corresponding to the proof of the factorization theorem is
@{thm [display] factor_exists_def}
›

instantiation nat :: default
begin

definition "default = (0::nat)"

instance ..

end

instantiation list :: (type) default
begin

definition "default = []"

instance ..

end

primrec iterate :: "nat ⇒ ('a ⇒ 'a) ⇒ 'a ⇒ 'a list"
where
"iterate 0 f x = []"
| "iterate (Suc n) f x = (let y = f x in y # iterate n f y)"

lemma "factor_exists 1007 = [53, 19]" by eval
lemma "factor_exists 567 = [7, 3, 3, 3, 3]" by eval
lemma "factor_exists 345 = [23, 5, 3]" by eval
lemma "factor_exists 999 = [37, 3, 3, 3]" by eval
lemma "factor_exists 876 = [73, 3, 2, 2]" by eval

lemma "iterate 4 Euclid 0 = [2, 3, 7, 71]" by eval

end
```