Quelle  NSPrimes.thy   Sprache: Isabelle

(*  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
proof (induct M)
  case 0
  then show ?case 
    by auto
next
  case (Suc M)
  then obtain N where "N>0" and "\m. 0 < m \ m \ M \ m dvd N"
    by metis
  then show ?case
    by (metis nat_0_less_mult_iff zero_less_Suc dvd_mult dvd_mult2 dvd_refl le_Suc_eq)
qed

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 [rule_format]: "\M. \N. 0 < N \ (\m::hypnat. 0 < m \ m \ M \ m dvd N)"
  by transfer (rule dvd_by_all)

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)"
  by (metis Compl_iff gr0I hdvd_by_all hypnat_of_nat_le_whn singletonI star_of_0_less)


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 ‹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})"
  by (metis (mono_tags) is_singletonI' is_singleton_the_elem mem_Collect_eq)

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"
  by (metis STAR_subset_closed UNIV_I image_eqI starset_UNIV starset_image)

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"
  unfolding choicefun_def
  by (force intro: lemmaPow3 [THEN someI2_ex])

lemma injf_max_mem_set: "E \{} \ \x. \y \ E. x < y \ injf_max n E \ E"
proof (induct n)
  case 0
  then show ?case by force
next
  case (Suc n)
  then show ?case
    apply (simp add: choicefun_def)
    apply (rule lemmaPow3 [THEN someI2_ex], auto)
    done
qed

lemma injf_max_order_preserving: "\x. \y \ E. x < y \ injf_max n E < injf_max (Suc n) E"
  by (metis (no_types, lifting) choicefun_mem_set empty_iff injf_max.simps(2) mem_Collect_eq)

lemma injf_max_order_preserving2: 
  assumes "m < n" and E: "\x. \y \ E. x < y"
  shows  "injf_max m E < injf_max n E"
  using ‹m < n›
proof (induction n arbitrary: m)
  case 0 then show ?case by auto
next
  case (Suc n)
  then show ?case
    by (metis E injf_max_order_preserving less_Suc_eq order_less_trans)
qed


lemma inj_injf_max: "\x. \y \ E. x < y \ inj (\n. injf_max n E)"
  by (metis injf_max_order_preserving2 linorder_injI order_less_irrefl)

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"
  by (metis image_subsetI inj_injf_max injf_max_mem_set injf_max_order_preserving)


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

lemma hypnat_infinite_has_nonstandard:
  assumes "infinite A"
  shows "hypnat_of_nat ` A < ( *s* A)"
  by (metis assms IntE NatStar_hypreal_of_real_Int STAR_star_of_image_subset psubsetI
      infinite_iff_countable_subset inj_fun_not_hypnat_in_SHNat range_subset_mem_starsetNat)

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: "infinite A \ hypnat_of_nat ` A < *s* A"
  by (metis finite_starsetNat_iff hypnat_infinite_has_nonstandard nless_le)


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

lemma lemma_not_dvd_hypnat_one [simp]: "\n \ - {0}. \ hypnat_of_nat n dvd 1"
proof -
  have "\ hypnat_of_nat 2 dvd 1"
    by transfer auto
  then show ?thesis
    by (metis ComplI singletonD zero_neq_numeral)
qed

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: "infinite {p::nat. prime p}"
proof -
  obtain N k where N: "\n\- {0}. hypnat_of_nat n dvd N" "k\starprime" "k dvd N + 1"
    by (meson hyperprime_factor_exists hypnat_add_one_gt_one hypnat_dvd_all_hypnat_of_nat)
  then have "k \ 1"
    using ‹k ∈ starprime› by force
  then have "k \ hypnat_of_nat ` {p. prime p}"
    using N dvd_add_right_iff hdvd_one_eq_one not_prime_0 by blast
  then show ?thesis
    by (metis ‹k ∈ starprime› finite_starsetNat_iff starprime_def)
qed

end