Theory Primes_Ex

(*
  File: Primes_Ex.thy
  Author: Bohua Zhan

  Elementary number theory of primes, up to the proof of infinitude
  of primes and the unique factorization theorem.

  Follows the development in HOL/Computational_Algebra/Primes.thy.
*)

section ‹Primes›

theory Primes_Ex
  imports Auto2_Main
begin

subsection ‹Basic definition›

definition prime :: "nat ⇒ bool" where [rewrite]:
  "prime p = (1 < p ∧ (∀m. m dvd p ⟶ m = 1 ∨ m = p))"

lemma primeD1 [forward]: "prime p ⟹ 1 < p" by auto2
lemma primeD2: "prime p ⟹ m dvd p ⟹ m = 1 ∨ m = p" by auto2
setup ‹add_forward_prfstep_cond @{thm primeD2} [with_cond "?m ≠ 1", with_cond "?m ≠ ?p"]›
setup ‹del_prfstep_thm_eqforward @{thm prime_def}›

(* Exists a prime p. *)
theorem exists_prime [resolve]: "∃p. prime p"
@proof @have "prime 2" @qed

lemma prime_odd_nat: "prime p ⟹ p > 2 ⟹ odd p" by auto2

lemma prime_imp_coprime_nat [backward2]: "prime p ⟹ ¬ p dvd n ⟹ coprime p n" by auto2

lemma prime_dvd_mult_nat: "prime p ⟹ p dvd m * n ⟹ p dvd m ∨ p dvd n" by auto2
setup ‹add_forward_prfstep_cond @{thm prime_dvd_mult_nat}
  (with_conds ["?m ≠ ?p", "?n ≠ ?p", "?m ≠ ?p * ?m'", "?n ≠ ?p * ?n'"])›

theorem prime_dvd_intro: "prime p ⟹ p * q = m * n ⟹ p dvd m ∨ p dvd n"
@proof @have "p dvd m * n" @qed
setup ‹add_forward_prfstep_cond @{thm prime_dvd_intro}
  (with_conds ["?m ≠ ?p", "?n ≠ ?p", "?m ≠ ?p * ?m'", "?n ≠ ?p * ?n'"])›

lemma prime_dvd_mult_eq_nat: "prime p ⟹ p dvd m * n = (p dvd m ∨ p dvd n)" by auto2

lemma not_prime_eq_prod_nat [backward1]: "n > 1 ⟹ ¬ prime n ⟹
    ∃m k. n = m * k ∧ 1 < m ∧ m < n ∧ 1 < k ∧ k < n"
@proof
  @obtain m where "m dvd n ∧ m ≠ 1 ∧ m ≠ n"
  @obtain k where "n = m * k" @have "m ≤ m * k" @have "k ≤ m * k"
@qed

lemma prime_dvd_power_nat: "prime p ⟹ p dvd x^n ⟹ p dvd x" by auto2
setup ‹add_forward_prfstep_cond @{thm prime_dvd_power_nat} [with_cond "?p ≠ ?x"]›

lemma prime_dvd_power_nat_iff: "prime p ⟹ n > 0 ⟹ p dvd x^n ⟷ p dvd x" by auto2

lemma prime_nat_code: "prime p = (1 < p ∧ (∀x. 1 < x ∧ x < p ⟶ ¬ x dvd p))" by auto2

lemma prime_factor_nat [backward]: "n ≠ 1 ⟹ ∃p. p dvd n ∧ prime p"
@proof
  @strong_induct n
  @case "prime n" @case "n = 0"
  @obtain k where "k ≠ 1" "k ≠ n" "k dvd n"
  @apply_induct_hyp k
@qed

lemma prime_divprod_pow_nat:
  "prime p ⟹ coprime a b ⟹ p^n dvd a * b ⟹ p^n dvd a ∨ p^n dvd b" by auto2

lemma prime_product [forward]: "prime (p * q) ⟹ p = 1 ∨ q = 1"
@proof @have "p dvd q * p" @qed

lemma prime_exp: "prime (p ^ n) ⟷ n = 1 ∧ prime p" by auto2

lemma prime_power_mult: "prime p ⟹ x * y = p ^ k ⟹ ∃i j. x = p ^ i ∧ y = p ^ j"
@proof
  @induct k arbitrary x y @with
    @subgoal "k = Suc k'"
      @case "p dvd x" @with
        @obtain x' where "x = p * x'" @have "x * y = p * (x' * y)"
        @obtain i j where "x' = p ^ i" "y = p ^ j" @have "x = p ^ Suc i" @end
      @case "p dvd y" @with
        @obtain y' where "y = p * y'" @have "x * y = p * (x * y')"
        @obtain i j where "x = p ^ i" "y' = p ^ j" @have "y = p ^ Suc j" @end
    @endgoal
  @end
@qed

subsection ‹Infinitude of primes›

theorem bigger_prime [resolve]: "∃p. prime p ∧ n < p"
@proof
  @obtain p where "prime p" "p dvd fact n + 1"
  @case "n ≥ p" @with @have "(p::nat) dvd fact n" @end
@qed

theorem primes_infinite: "¬ finite {p. prime p}"
@proof
  @obtain b where "prime b" "Max {p. prime p} < b"
@qed

subsection ‹Existence and uniqueness of prime factorization›

theorem factorization_exists: "n > 0 ⟹ ∃M. (∀p∈#M. prime p) ∧ n = (∏i∈#M. i)"
@proof
  @strong_induct n
  @case "n = 1" @with @have "n = (∏i∈# {#}. i)" @end
  @case "prime n" @with @have "n = (∏i∈# {#n#}. i)" @end
  @obtain m k where "n = m * k" "1 < m" "m < n" "1 < k" "k < n"
  @apply_induct_hyp m
  @obtain M where "(∀p∈#M. prime p)" "m = (∏i∈#M. i)"
  @apply_induct_hyp k
  @obtain K where "(∀p∈#K. prime p)" "k = (∏i∈#K. i)"
  @have "n = (∏i∈#(M+K). i)"
@qed

theorem prime_dvd_multiset [backward1]: "prime p ⟹ p dvd (∏i∈#M. i) ⟹ ∃n. n∈#M ∧ p dvd n"
@proof
  @strong_induct M
  @case "M = {#}"
  @obtain M' m where "M = M' + {#m#}"
  @contradiction @apply_induct_hyp M'
@qed

theorem factorization_unique_aux:
  "∀p∈#M. prime p ⟹ ∀p∈#N. prime p ⟹ (∏i∈#M. i) dvd (∏i∈#N. i) ⟹ M ⊆# N"
@proof
  @strong_induct M arbitrary N
  @case "M = {#}"
  @obtain M' m where "M = M' + {#m#}"
  @have "m dvd (∏i∈#M. i)"
  @obtain n where "n ∈# N" "m dvd n"
  @obtain N' where "N = N' + {#n#}"
  @have "m = n"
  @have "(∏i∈#M'. i) dvd (∏i∈#N'. i)"
  @apply_induct_hyp M' N'
@qed
setup ‹add_forward_prfstep_cond @{thm factorization_unique_aux} [with_cond "?M ≠ ?N"]›

theorem factorization_unique:
  "∀p∈#M. prime p ⟹ ∀p∈#N. prime p ⟹ (∏i∈#M. i) = (∏i∈#N. i) ⟹ M = N"
@proof @have "M ⊆# N" @qed
setup ‹del_prfstep_thm @{thm factorization_unique_aux}›

end