Euclid.thy

theory Euclid
  imports Main "HOL-Library.Disjoint_Sets"
begin

fun prime :: "nat ⇒ bool" where
  "prime n ⟷ n ≥ 2 ∧ (∀k ≤ n. k dvd n ⟶ k = 1 ∨ k = n)"

lemma "prime 5"
  by code_simp

definition primes :: "nat set" where
  "primes = {p. prime p}"

lemma dvd_not1_geq_2:
  fixes k n :: nat
  assumes "k dvd n"
    "k ≠ 1"
    "n ≥ 2"
  shows "k ≥ 2"
  by (metis One_nat_def add.commute assms(1) assms(2) assms(3) dvd_add_triv_right_iff dvd_antisym
      dvd_refl less_2_cases_iff linorder_not_less nat_arith.rule0)

lemma dvd_prime: "n ≥ 2 ⟹ ∃p ≤ n. prime p ∧ p dvd n"
proof (induction n rule: nat_less_induct)
  case (1 n)
  then show ?case
  proof (cases "prime n")
    case True
    then show ?thesis by auto
  next
    case False
    then have "∃k ≤ n. k dvd n ∧ k ≠ 1 ∧ k ≠ n"
      by (simp add: "1.prems")
    then obtain k where
      "k ≤ n"
      "k dvd n"
      "k ≠ 1"
      "k ≠ n"
      by auto
    moreover have "k ≥ 2"
      using "1.prems" calculation(2) calculation(3) dvd_not1_geq_2 by auto
    moreover have "k < n"
      by (simp add: calculation(1) calculation(4) le_neq_implies_less)
    moreover have "∃p ≤ k. prime p ∧ p dvd k"
      using "1.IH" calculation(5) calculation(6) by blast
    moreover obtain p where
      "p ≤ k"
      "prime p"
      "p dvd k"
      using calculation(7) by blast
    ultimately show ?thesis
      by (meson gcd_nat.trans order_trans)
  qed
qed

(* Euclid's proof *)
context
begin

lemma prod_plus1_mod:
  fixes A :: "nat set"
  assumes "finite A"
    "k ≥ 1"
    "p = k * ∏A + 1"
    "∀a ∈ A. a ≥ 2"
  shows "∀a ∈ A. p mod a = 1"
using assms proof (induction A arbitrary: p k rule: finite_induct)
  case empty
  then show ?case by simp
next
  case (insert a' A')
  moreover have "∏(insert a' A') = a' * ∏A'"
    by (simp add: insert.hyps(1) insert.hyps(2))
  moreover have "p = k * a' * ∏A' + 1"
    by (simp add: calculation(7) insert.prems(2))
  moreover have "p mod a' = 1"
    by (metis Groups.mult_ac(3) One_nat_def Suc_1 Suc_times_mod_eq add.right_neutral add_Suc_right 
        calculation(7) insertCI le_simps(3) local.insert(5) local.insert(6))
  ultimately show ?case by simp
qed

lemma primes_prod_plus1_mod:
  assumes "finite primes"
    "p' = ∏primes + 1"
  shows "∀p ∈ primes. p' mod p = 1"
  using assms primes_def prod_plus1_mod by fastforce

theorem "infinite primes"
proof
  assume prem: "finite primes"
  obtain p' where
    "p' = ∏primes + 1"
    by simp
  moreover have "p' ≥ 2"
    by (metis CollectD Suc_1 Suc_leD add_mono_thms_linordered_semiring(1) calculation
        le_numeral_extra(4) one_add_one prime.elims(2) primes_def prod_ge_1)
  moreover have "∀p ∈ primes. p' mod p = 1"
    using calculation(1) prem primes_prod_plus1_mod by blast
  moreover have "∃p ≤ p'. prime p ∧ p dvd p'"
    using calculation(2) dvd_prime by blast
  moreover obtain p where
    "p ∈ primes"
    "p dvd p'"
    using calculation(4) primes_def by auto
  ultimately have "p' mod p = 1 ∧ p' mod p = 0" by auto
  then show False by auto
qed
end

(* Saidak's proof *)
context
begin

fun prime_factor :: "nat ⇒ nat ⇒ bool" where
  "prime_factor n p ⟷ prime p ∧ p dvd n"

fun prime_factors :: "nat ⇒ nat set" where
  "prime_factors n = {p. prime_factor n p}"

lemma saidak_lemma':
  fixes n m :: nat
  assumes "coprime n m"
    "n ≥ 2"
    "m ≥ 2"
  shows "∃p ∈ prime_factors m. p ∉ prime_factors n"
proof (rule contrapos_pp[OF assms(1)])
  assume "¬(∃p ∈ prime_factors m. p ∉ prime_factors n)"
  then have "∀p ∈ prime_factors m. p ∈ prime_factors n" by blast
  then have "∀p. prime p ∧ p dvd m ⟶ p dvd n" by simp
  moreover have "∃p. prime p ∧ p dvd m" using assms dvd_prime by auto
  ultimately have "∃p. prime p ∧ p dvd m ∧ p dvd n" by auto
  then show "¬coprime n m" by fastforce
qed

lemma saidak_lemma:
  fixes n m :: nat
  assumes "coprime n m"
    "n ≥ 2"
    "m ≥ 2"
  shows "∃p. p ∉ prime_factors n ∧ p ∈ prime_factors m"
  using saidak_lemma' assms(1) assms(2) assms(3) by blast

lemma "coprime n (Suc n)" by auto

fun saidak :: "nat ⇒ nat ⇒ nat" where
  "saidak 0 n = n * Suc n" |
  "saidak (Suc k) n = saidak k n * Suc (saidak k n)"

lemma saidak_geq_2:
  assumes "n ≥ 2"
  shows "saidak k n ≥ 2"
proof (induction k)
  case 0
  then show ?case using assms by auto
next
  case (Suc k)
  then show ?case by simp
qed

lemma prod_prime_factor:
  assumes "prime_factor n p"
  shows "prime_factor (m * n) p"
  using assms by auto

lemma prod_prime_factors:
  assumes "p ∈ prime_factors n"
  shows "p ∈ prime_factors (m * n)"
  using assms prod_prime_factor by auto

lemma prime_factors_saidak:
  assumes "p ∈ prime_factors (Suc (saidak k n))"
  shows "p ∈ prime_factors (saidak (Suc k) n)"
  using assms prod_prime_factors saidak.simps(2) by presburger

lemma saidak_ascending: "n ≥ 2 ⟹ prime_factors (saidak k n) ⊂ prime_factors (saidak (Suc k) n)"
proof
  show "prime_factors (saidak k n) ⊆ prime_factors (saidak (Suc k) n)"
  proof
    fix p
    assume "p ∈ prime_factors (saidak k n)"
    then show "p ∈ prime_factors (saidak (Suc k) n)" by auto
  qed
next
  assume "n ≥ 2"
  then have "saidak k n ≥ 2 ∧ Suc (saidak k n) ≥ 2"
    by (simp add: le_Suc_eq saidak_geq_2)
  moreover have "coprime (saidak k n) (Suc (saidak k n))" by auto
  ultimately have "∃p. p ∉ prime_factors (saidak k n) ∧ p ∈ prime_factors (Suc (saidak k n))"
    using saidak_lemma by blast
  then obtain p where
    "p ∉ prime_factors (saidak k n)"
    "p ∈ prime_factors (Suc (saidak k n))"
    by auto
  moreover have "p ∈ prime_factors (saidak (Suc k) n)"
    using calculation(2) prime_factors_saidak by blast
  ultimately show "prime_factors (saidak k n) ≠ prime_factors (saidak (Suc k) n)"
    by auto
qed

fun saidak2 :: "nat ⇒ nat set" where
  "saidak2 k = prime_factors (saidak k 2)"

lemma mono_saidak2: "mono saidak2"
  unfolding saidak2.simps
  using saidak_ascending mono_iff_le_Suc by blast

definition saidak_disjointed :: "nat ⇒ nat set" where
  "saidak_disjointed = disjointed saidak2"

lemma saidak_disjointed_nonempty:
  "saidak_disjointed k ≠ {}"
proof (cases k)
  have obv: "prime_factors 6 = {2, 3}" sorry

  case 0
  then have "saidak_disjointed k = prime_factors (saidak 0 2)"
    by (simp add: saidak_disjointed_def)
  then have "saidak_disjointed k = prime_factors 6" by simp
  then have "saidak_disjointed k = {2, 3}" using obv by simp
  then show ?thesis by simp
next
  case (Suc k)
  have "saidak_disjointed (Suc k) = saidak2 (Suc k) - saidak2 k"
    by (simp add: disjointed_mono mono_saidak2 saidak_disjointed_def)
  then have "saidak_disjointed (Suc k) ≠ {}"
    using saidak_ascending by auto
  then show ?thesis by (simp add: Suc)
qed

lemma
  "infinite (⋃ (saidak_disjointed ` UNIV))"
  apply (rule infinite_disjoint_family_imp_infinite_UNION)
    apply simp
   prefer 2
   apply (simp add: disjoint_family_disjointed saidak_disjointed_def)
  using saidak_disjointed_nonempty by auto

end

end