Theory NSPrimes

(*  Title       : NSPrimes.thy
    Author      : Jacques D. Fleuriot
    Copyright   : 2002 University of Edinburgh
    Conversion to Isar and new proofs by Lawrence C Paulson, 2004
*)

section ‹The Nonstandard Primes as an Extension of the Prime Numbers›

theory NSPrimes
  imports "HOL-Computational_Algebra.Primes" "HOL-Nonstandard_Analysis.Hyperreal"
begin

text ‹These can be used to derive an alternative proof of the infinitude of
primes by considering a property of nonstandard sets.›

definition starprime :: "hypnat set"
  where [transfer_unfold]: "starprime = *s* {p. prime p}"

definition choicefun :: "'a set ⇒ 'a"
  where "choicefun E = (SOME x. ∃X ∈ Pow E - {{}}. x ∈ X)"

primrec injf_max :: "nat ⇒ 'a::order set ⇒ 'a"
where
  injf_max_zero: "injf_max 0 E = choicefun E"
| injf_max_Suc: "injf_max (Suc n) E = choicefun ({e. e ∈ E ∧ injf_max n E < e})"

lemma dvd_by_all2: "∃N>0. ∀m. 0 < m ∧ m ≤ M ⟶ m dvd N"
  for M :: nat
  apply (induct M)
   apply auto
  apply (rule_tac x = "N * Suc M" in exI)
  apply auto
  apply (metis dvdI dvd_add_times_triv_left_iff dvd_add_triv_right_iff dvd_refl dvd_trans le_Suc_eq mult_Suc_right)
  done

lemma dvd_by_all: "∀M::nat. ∃N>0. ∀m. 0 < m ∧ m ≤ M ⟶ m dvd N"
  using dvd_by_all2 by blast

lemma hypnat_of_nat_le_zero_iff [simp]: "hypnat_of_nat n ≤ 0 ⟷ n = 0"
  by transfer simp

text ‹Goldblatt: Exercise 5.11(2) -- p. 57.›
lemma hdvd_by_all: "∀M. ∃N. 0 < N ∧ (∀m::hypnat. 0 < m ∧ m ≤ M ⟶ m dvd N)"
  by transfer (rule dvd_by_all)

lemmas hdvd_by_all2 = hdvd_by_all [THEN spec]

text ‹Goldblatt: Exercise 5.11(2) -- p. 57.›
lemma hypnat_dvd_all_hypnat_of_nat:
  "∃N::hypnat. 0 < N ∧ (∀n ∈ - {0::nat}. hypnat_of_nat n dvd N)"
  apply (cut_tac hdvd_by_all)
  apply (drule_tac x = whn in spec)
  apply auto
  apply (rule exI)
  apply auto
  apply (drule_tac x = "hypnat_of_nat n" in spec)
  apply (auto simp add: linorder_not_less)
  done


text ‹The nonstandard extension of the set prime numbers consists of precisely
  those hypernaturals exceeding 1 that have no nontrivial factors.›

text ‹Goldblatt: Exercise 5.11(3a) -- p 57.›
lemma starprime: "starprime = {p. 1 < p ∧ (∀m. m dvd p ⟶ m = 1 ∨ m = p)}"
  by transfer (auto simp add: prime_nat_iff)

text ‹Goldblatt Exercise 5.11(3b) -- p 57.›
lemma hyperprime_factor_exists: "⋀n. 1 < n ⟹ ∃k ∈ starprime. k dvd n"
  by transfer (simp add: prime_factor_nat)

text ‹Goldblatt Exercise 3.10(1) -- p. 29.›
lemma NatStar_hypnat_of_nat: "finite A ⟹ *s* A = hypnat_of_nat ` A"
  by (rule starset_finite)


subsection ‹Another characterization of infinite set of natural numbers›

lemma finite_nat_set_bounded: "finite N ⟹ ∃n::nat. ∀i ∈ N. i < n"
  apply (erule_tac F = N in finite_induct)
   apply auto
  apply (rule_tac x = "Suc n + x" in exI)
  apply auto
  done

lemma finite_nat_set_bounded_iff: "finite N ⟷ (∃n::nat. ∀i ∈ N. i < n)"
  by (blast intro: finite_nat_set_bounded bounded_nat_set_is_finite)

lemma not_finite_nat_set_iff: "¬ finite N ⟷ (∀n::nat. ∃i ∈ N. n ≤ i)"
  by (auto simp add: finite_nat_set_bounded_iff not_less)

lemma bounded_nat_set_is_finite2: "∀i::nat ∈ N. i ≤ n ⟹ finite N"
  apply (rule finite_subset)
   apply (rule_tac [2] finite_atMost)
  apply auto
  done

lemma finite_nat_set_bounded2: "finite N ⟹ ∃n::nat. ∀i ∈ N. i ≤ n"
  apply (erule_tac F = N in finite_induct)
   apply auto
  apply (rule_tac x = "n + x" in exI)
  apply auto
  done

lemma finite_nat_set_bounded_iff2: "finite N ⟷ (∃n::nat. ∀i ∈ N. i ≤ n)"
  by (blast intro: finite_nat_set_bounded2 bounded_nat_set_is_finite2)

lemma not_finite_nat_set_iff2: "¬ finite N ⟷ (∀n::nat. ∃i ∈ N. n < i)"
  by (auto simp add: finite_nat_set_bounded_iff2 not_le)


subsection ‹An injective function cannot define an embedded natural number›

lemma lemma_infinite_set_singleton:
  "∀m n. m ≠ n ⟶ f n ≠ f m ⟹ {n. f n = N} = {} ∨ (∃m. {n. f n = N} = {m})"
  apply auto
  apply (drule_tac x = x in spec, auto)
  apply (subgoal_tac "∀n. f n = f x ⟷ x = n")
   apply auto
  done

lemma inj_fun_not_hypnat_in_SHNat:
  fixes f :: "nat ⇒ nat"
  assumes inj_f: "inj f"
  shows "starfun f whn ∉ Nats"
proof
  from inj_f have inj_f': "inj (starfun f)"
    by (transfer inj_on_def Ball_def UNIV_def)
  assume "starfun f whn ∈ Nats"
  then obtain N where N: "starfun f whn = hypnat_of_nat N"
    by (auto simp: Nats_def)
  then have "∃n. starfun f n = hypnat_of_nat N" ..
  then have "∃n. f n = N" by transfer
  then obtain n where "f n = N" ..
  then have "starfun f (hypnat_of_nat n) = hypnat_of_nat N"
    by transfer
  with N have "starfun f whn = starfun f (hypnat_of_nat n)"
    by simp
  with inj_f' have "whn = hypnat_of_nat n"
    by (rule injD)
  then show False
    by (simp add: whn_neq_hypnat_of_nat)
qed

lemma range_subset_mem_starsetNat: "range f ⊆ A ⟹ starfun f whn ∈ *s* A"
  apply (rule_tac x="whn" in spec)
  apply transfer
  apply auto
  done

text ‹
  Gleason Proposition 11-5.5. pg 149, pg 155 (ex. 3) and pg. 360.

  Let ‹E› be a nonvoid ordered set with no maximal elements (note: effectively an
  infinite set if we take ‹E = N› (Nats)). Then there exists an order-preserving
  injection from ‹N› to ‹E›. Of course, (as some doofus will undoubtedly point out!
  :-)) can use notion of least element in proof (i.e. no need for choice) if
  dealing with nats as we have well-ordering property.
›

lemma lemmaPow3: "E ≠ {} ⟹ ∃x. ∃X ∈ Pow E - {{}}. x ∈ X"
  by auto

lemma choicefun_mem_set [simp]: "E ≠ {} ⟹ choicefun E ∈ E"
  apply (unfold choicefun_def)
  apply (rule lemmaPow3 [THEN someI2_ex], auto)
  done

lemma injf_max_mem_set: "E ≠{} ⟹ ∀x. ∃y ∈ E. x < y ⟹ injf_max n E ∈ E"
  apply (induct n)
   apply force
  apply (simp add: choicefun_def)
  apply (rule lemmaPow3 [THEN someI2_ex], auto)
  done

lemma injf_max_order_preserving: "∀x. ∃y ∈ E. x < y ⟹ injf_max n E < injf_max (Suc n) E"
  apply (simp add: choicefun_def)
  apply (rule lemmaPow3 [THEN someI2_ex])
   apply auto
  done

lemma injf_max_order_preserving2: "∀x. ∃y ∈ E. x < y ⟹ ∀n m. m < n ⟶ injf_max m E < injf_max n E"
  apply (rule allI)
  apply (induct_tac n)
   apply auto
  apply (simp add: choicefun_def)
  apply (rule lemmaPow3 [THEN someI2_ex])
   apply (auto simp add: less_Suc_eq)
  apply (drule_tac x = m in spec)
  apply (drule subsetD)
   apply auto
  done

lemma inj_injf_max: "∀x. ∃y ∈ E. x < y ⟹ inj (λn. injf_max n E)"
  apply (rule inj_onI)
  apply (rule ccontr)
  apply auto
  apply (drule injf_max_order_preserving2)
  apply (metis antisym_conv3 order_less_le)
  done

lemma infinite_set_has_order_preserving_inj:
  "E ≠ {} ⟹ ∀x. ∃y ∈ E. x < y ⟹ ∃f. range f ⊆ E ∧ inj f ∧ (∀m. f m < f (Suc m))"
  for E :: "'a::order set" and f :: "nat ⇒ 'a"
  apply (rule_tac x = "λn. injf_max n E" in exI)
  apply safe
    apply (rule injf_max_mem_set)
     apply (rule_tac [3] inj_injf_max)
     apply (rule_tac [4] injf_max_order_preserving)
     apply auto
  done


text ‹Only need the existence of an injective function from ‹N› to ‹A› for proof.›

lemma hypnat_infinite_has_nonstandard: "¬ finite A ⟹ hypnat_of_nat ` A < ( *s* A)"
  apply auto
  apply (subgoal_tac "A ≠ {}")
   prefer 2 apply force
  apply (drule infinite_set_has_order_preserving_inj)
   apply (erule not_finite_nat_set_iff2 [THEN iffD1])
  apply auto
  apply (drule inj_fun_not_hypnat_in_SHNat)
  apply (drule range_subset_mem_starsetNat)
  apply (auto simp add: SHNat_eq)
  done

lemma starsetNat_eq_hypnat_of_nat_image_finite: "*s* A =  hypnat_of_nat ` A ⟹ finite A"
  by (metis hypnat_infinite_has_nonstandard less_irrefl)

lemma finite_starsetNat_iff: "*s* A = hypnat_of_nat ` A ⟷ finite A"
  by (blast intro!: starsetNat_eq_hypnat_of_nat_image_finite NatStar_hypnat_of_nat)

lemma hypnat_infinite_has_nonstandard_iff: "¬ finite A ⟷ hypnat_of_nat ` A < *s* A"
  apply (rule iffI)
   apply (blast intro!: hypnat_infinite_has_nonstandard)
  apply (auto simp add: finite_starsetNat_iff [symmetric])
  done


subsection ‹Existence of Infinitely Many Primes: a Nonstandard Proof›

lemma lemma_not_dvd_hypnat_one [simp]: "¬ (∀n ∈ - {0}. hypnat_of_nat n dvd 1)"
  apply auto
  apply (rule_tac x = 2 in bexI)
   apply transfer
   apply auto
  done

lemma lemma_not_dvd_hypnat_one2 [simp]: "∃n ∈ - {0}. ¬ hypnat_of_nat n dvd 1"
  using lemma_not_dvd_hypnat_one by (auto simp del: lemma_not_dvd_hypnat_one)

lemma hypnat_add_one_gt_one: "⋀N::hypnat. 0 < N ⟹ 1 < N + 1"
  by transfer simp

lemma hypnat_of_nat_zero_not_prime [simp]: "hypnat_of_nat 0 ∉ starprime"
  by transfer simp

lemma hypnat_zero_not_prime [simp]: "0 ∉ starprime"
  using hypnat_of_nat_zero_not_prime by simp

lemma hypnat_of_nat_one_not_prime [simp]: "hypnat_of_nat 1 ∉ starprime"
  by transfer simp

lemma hypnat_one_not_prime [simp]: "1 ∉ starprime"
  using hypnat_of_nat_one_not_prime by simp

lemma hdvd_diff: "⋀k m n :: hypnat. k dvd m ⟹ k dvd n ⟹ k dvd (m - n)"
  by transfer (rule dvd_diff_nat)

lemma hdvd_one_eq_one: "⋀x::hypnat. is_unit x ⟹ x = 1"
  by transfer simp

text ‹Already proved as ‹primes_infinite›, but now using non-standard naturals.›
theorem not_finite_prime: "¬ finite {p::nat. prime p}"
  apply (rule hypnat_infinite_has_nonstandard_iff [THEN iffD2])
  using hypnat_dvd_all_hypnat_of_nat
  apply clarify
  apply (drule hypnat_add_one_gt_one)
  apply (drule hyperprime_factor_exists)
  apply clarify
  apply (subgoal_tac "k ∉ hypnat_of_nat ` {p. prime p}")
   apply (force simp: starprime_def)
  apply (metis Compl_iff add.commute dvd_add_left_iff empty_iff hdvd_one_eq_one hypnat_one_not_prime
      imageE insert_iff mem_Collect_eq not_prime_0)
  done

end