1(* Title : NSPrimes.thy 2 Author : Jacques D. Fleuriot 3 Copyright : 2002 University of Edinburgh 4 Conversion to Isar and new proofs by Lawrence C Paulson, 2004 5*) 6 7section \<open>The Nonstandard Primes as an Extension of the Prime Numbers\<close> 8 9theory NSPrimes 10 imports "HOL-Computational_Algebra.Primes" "HOL-Nonstandard_Analysis.Hyperreal" 11begin 12 13text \<open>These can be used to derive an alternative proof of the infinitude of 14primes by considering a property of nonstandard sets.\<close> 15 16definition starprime :: "hypnat set" 17 where [transfer_unfold]: "starprime = *s* {p. prime p}" 18 19definition choicefun :: "'a set \<Rightarrow> 'a" 20 where "choicefun E = (SOME x. \<exists>X \<in> Pow E - {{}}. x \<in> X)" 21 22primrec injf_max :: "nat \<Rightarrow> 'a::order set \<Rightarrow> 'a" 23where 24 injf_max_zero: "injf_max 0 E = choicefun E" 25| injf_max_Suc: "injf_max (Suc n) E = choicefun ({e. e \<in> E \<and> injf_max n E < e})" 26 27lemma dvd_by_all2: "\<exists>N>0. \<forall>m. 0 < m \<and> m \<le> M \<longrightarrow> m dvd N" 28 for M :: nat 29 apply (induct M) 30 apply auto 31 apply (rule_tac x = "N * Suc M" in exI) 32 apply auto 33 apply (metis dvdI dvd_add_times_triv_left_iff dvd_add_triv_right_iff dvd_refl dvd_trans le_Suc_eq mult_Suc_right) 34 done 35 36lemma dvd_by_all: "\<forall>M::nat. \<exists>N>0. \<forall>m. 0 < m \<and> m \<le> M \<longrightarrow> m dvd N" 37 using dvd_by_all2 by blast 38 39lemma hypnat_of_nat_le_zero_iff [simp]: "hypnat_of_nat n \<le> 0 \<longleftrightarrow> n = 0" 40 by transfer simp 41 42text \<open>Goldblatt: Exercise 5.11(2) -- p. 57.\<close> 43lemma hdvd_by_all: "\<forall>M. \<exists>N. 0 < N \<and> (\<forall>m::hypnat. 0 < m \<and> m \<le> M \<longrightarrow> m dvd N)" 44 by transfer (rule dvd_by_all) 45 46lemmas hdvd_by_all2 = hdvd_by_all [THEN spec] 47 48text \<open>Goldblatt: Exercise 5.11(2) -- p. 57.\<close> 49lemma hypnat_dvd_all_hypnat_of_nat: 50 "\<exists>N::hypnat. 0 < N \<and> (\<forall>n \<in> - {0::nat}. hypnat_of_nat n dvd N)" 51 apply (cut_tac hdvd_by_all) 52 apply (drule_tac x = whn in spec) 53 apply auto 54 apply (rule exI) 55 apply auto 56 apply (drule_tac x = "hypnat_of_nat n" in spec) 57 apply (auto simp add: linorder_not_less) 58 done 59 60 61text \<open>The nonstandard extension of the set prime numbers consists of precisely 62 those hypernaturals exceeding 1 that have no nontrivial factors.\<close> 63 64text \<open>Goldblatt: Exercise 5.11(3a) -- p 57.\<close> 65lemma starprime: "starprime = {p. 1 < p \<and> (\<forall>m. m dvd p \<longrightarrow> m = 1 \<or> m = p)}" 66 by transfer (auto simp add: prime_nat_iff) 67 68text \<open>Goldblatt Exercise 5.11(3b) -- p 57.\<close> 69lemma hyperprime_factor_exists: "\<And>n. 1 < n \<Longrightarrow> \<exists>k \<in> starprime. k dvd n" 70 by transfer (simp add: prime_factor_nat) 71 72text \<open>Goldblatt Exercise 3.10(1) -- p. 29.\<close> 73lemma NatStar_hypnat_of_nat: "finite A \<Longrightarrow> *s* A = hypnat_of_nat ` A" 74 by (rule starset_finite) 75 76 77subsection \<open>Another characterization of infinite set of natural numbers\<close> 78 79lemma finite_nat_set_bounded: "finite N \<Longrightarrow> \<exists>n::nat. \<forall>i \<in> N. i < n" 80 apply (erule_tac F = N in finite_induct) 81 apply auto 82 apply (rule_tac x = "Suc n + x" in exI) 83 apply auto 84 done 85 86lemma finite_nat_set_bounded_iff: "finite N \<longleftrightarrow> (\<exists>n::nat. \<forall>i \<in> N. i < n)" 87 by (blast intro: finite_nat_set_bounded bounded_nat_set_is_finite) 88 89lemma not_finite_nat_set_iff: "\<not> finite N \<longleftrightarrow> (\<forall>n::nat. \<exists>i \<in> N. n \<le> i)" 90 by (auto simp add: finite_nat_set_bounded_iff not_less) 91 92lemma bounded_nat_set_is_finite2: "\<forall>i::nat \<in> N. i \<le> n \<Longrightarrow> finite N" 93 apply (rule finite_subset) 94 apply (rule_tac [2] finite_atMost) 95 apply auto 96 done 97 98lemma finite_nat_set_bounded2: "finite N \<Longrightarrow> \<exists>n::nat. \<forall>i \<in> N. i \<le> n" 99 apply (erule_tac F = N in finite_induct) 100 apply auto 101 apply (rule_tac x = "n + x" in exI) 102 apply auto 103 done 104 105lemma finite_nat_set_bounded_iff2: "finite N \<longleftrightarrow> (\<exists>n::nat. \<forall>i \<in> N. i \<le> n)" 106 by (blast intro: finite_nat_set_bounded2 bounded_nat_set_is_finite2) 107 108lemma not_finite_nat_set_iff2: "\<not> finite N \<longleftrightarrow> (\<forall>n::nat. \<exists>i \<in> N. n < i)" 109 by (auto simp add: finite_nat_set_bounded_iff2 not_le) 110 111 112subsection \<open>An injective function cannot define an embedded natural number\<close> 113 114lemma lemma_infinite_set_singleton: 115 "\<forall>m n. m \<noteq> n \<longrightarrow> f n \<noteq> f m \<Longrightarrow> {n. f n = N} = {} \<or> (\<exists>m. {n. f n = N} = {m})" 116 apply auto 117 apply (drule_tac x = x in spec, auto) 118 apply (subgoal_tac "\<forall>n. f n = f x \<longleftrightarrow> x = n") 119 apply auto 120 done 121 122lemma inj_fun_not_hypnat_in_SHNat: 123 fixes f :: "nat \<Rightarrow> nat" 124 assumes inj_f: "inj f" 125 shows "starfun f whn \<notin> Nats" 126proof 127 from inj_f have inj_f': "inj (starfun f)" 128 by (transfer inj_on_def Ball_def UNIV_def) 129 assume "starfun f whn \<in> Nats" 130 then obtain N where N: "starfun f whn = hypnat_of_nat N" 131 by (auto simp: Nats_def) 132 then have "\<exists>n. starfun f n = hypnat_of_nat N" .. 133 then have "\<exists>n. f n = N" by transfer 134 then obtain n where "f n = N" .. 135 then have "starfun f (hypnat_of_nat n) = hypnat_of_nat N" 136 by transfer 137 with N have "starfun f whn = starfun f (hypnat_of_nat n)" 138 by simp 139 with inj_f' have "whn = hypnat_of_nat n" 140 by (rule injD) 141 then show False 142 by (simp add: whn_neq_hypnat_of_nat) 143qed 144 145lemma range_subset_mem_starsetNat: "range f \<subseteq> A \<Longrightarrow> starfun f whn \<in> *s* A" 146 apply (rule_tac x="whn" in spec) 147 apply transfer 148 apply auto 149 done 150 151text \<open> 152 Gleason Proposition 11-5.5. pg 149, pg 155 (ex. 3) and pg. 360. 153 154 Let \<open>E\<close> be a nonvoid ordered set with no maximal elements (note: effectively an 155 infinite set if we take \<open>E = N\<close> (Nats)). Then there exists an order-preserving 156 injection from \<open>N\<close> to \<open>E\<close>. Of course, (as some doofus will undoubtedly point out! 157 :-)) can use notion of least element in proof (i.e. no need for choice) if 158 dealing with nats as we have well-ordering property. 159\<close> 160 161lemma lemmaPow3: "E \<noteq> {} \<Longrightarrow> \<exists>x. \<exists>X \<in> Pow E - {{}}. x \<in> X" 162 by auto 163 164lemma choicefun_mem_set [simp]: "E \<noteq> {} \<Longrightarrow> choicefun E \<in> E" 165 apply (unfold choicefun_def) 166 apply (rule lemmaPow3 [THEN someI2_ex], auto) 167 done 168 169lemma injf_max_mem_set: "E \<noteq>{} \<Longrightarrow> \<forall>x. \<exists>y \<in> E. x < y \<Longrightarrow> injf_max n E \<in> E" 170 apply (induct n) 171 apply force 172 apply (simp add: choicefun_def) 173 apply (rule lemmaPow3 [THEN someI2_ex], auto) 174 done 175 176lemma injf_max_order_preserving: "\<forall>x. \<exists>y \<in> E. x < y \<Longrightarrow> injf_max n E < injf_max (Suc n) E" 177 apply (simp add: choicefun_def) 178 apply (rule lemmaPow3 [THEN someI2_ex]) 179 apply auto 180 done 181 182lemma injf_max_order_preserving2: "\<forall>x. \<exists>y \<in> E. x < y \<Longrightarrow> \<forall>n m. m < n \<longrightarrow> injf_max m E < injf_max n E" 183 apply (rule allI) 184 apply (induct_tac n) 185 apply auto 186 apply (simp add: choicefun_def) 187 apply (rule lemmaPow3 [THEN someI2_ex]) 188 apply (auto simp add: less_Suc_eq) 189 apply (drule_tac x = m in spec) 190 apply (drule subsetD) 191 apply auto 192 apply (drule_tac x = "injf_max m E" in order_less_trans) 193 apply auto 194 done 195 196lemma inj_injf_max: "\<forall>x. \<exists>y \<in> E. x < y \<Longrightarrow> inj (\<lambda>n. injf_max n E)" 197 apply (rule inj_onI) 198 apply (rule ccontr) 199 apply auto 200 apply (drule injf_max_order_preserving2) 201 apply (metis antisym_conv3 order_less_le) 202 done 203 204lemma infinite_set_has_order_preserving_inj: 205 "E \<noteq> {} \<Longrightarrow> \<forall>x. \<exists>y \<in> E. x < y \<Longrightarrow> \<exists>f. range f \<subseteq> E \<and> inj f \<and> (\<forall>m. f m < f (Suc m))" 206 for E :: "'a::order set" and f :: "nat \<Rightarrow> 'a" 207 apply (rule_tac x = "\<lambda>n. injf_max n E" in exI) 208 apply safe 209 apply (rule injf_max_mem_set) 210 apply (rule_tac [3] inj_injf_max) 211 apply (rule_tac [4] injf_max_order_preserving) 212 apply auto 213 done 214 215 216text \<open>Only need the existence of an injective function from \<open>N\<close> to \<open>A\<close> for proof.\<close> 217 218lemma hypnat_infinite_has_nonstandard: "\<not> finite A \<Longrightarrow> hypnat_of_nat ` A < ( *s* A)" 219 apply auto 220 apply (subgoal_tac "A \<noteq> {}") 221 prefer 2 apply force 222 apply (drule infinite_set_has_order_preserving_inj) 223 apply (erule not_finite_nat_set_iff2 [THEN iffD1]) 224 apply auto 225 apply (drule inj_fun_not_hypnat_in_SHNat) 226 apply (drule range_subset_mem_starsetNat) 227 apply (auto simp add: SHNat_eq) 228 done 229 230lemma starsetNat_eq_hypnat_of_nat_image_finite: "*s* A = hypnat_of_nat ` A \<Longrightarrow> finite A" 231 by (metis hypnat_infinite_has_nonstandard less_irrefl) 232 233lemma finite_starsetNat_iff: "*s* A = hypnat_of_nat ` A \<longleftrightarrow> finite A" 234 by (blast intro!: starsetNat_eq_hypnat_of_nat_image_finite NatStar_hypnat_of_nat) 235 236lemma hypnat_infinite_has_nonstandard_iff: "\<not> finite A \<longleftrightarrow> hypnat_of_nat ` A < *s* A" 237 apply (rule iffI) 238 apply (blast intro!: hypnat_infinite_has_nonstandard) 239 apply (auto simp add: finite_starsetNat_iff [symmetric]) 240 done 241 242 243subsection \<open>Existence of Infinitely Many Primes: a Nonstandard Proof\<close> 244 245lemma lemma_not_dvd_hypnat_one [simp]: "\<not> (\<forall>n \<in> - {0}. hypnat_of_nat n dvd 1)" 246 apply auto 247 apply (rule_tac x = 2 in bexI) 248 apply transfer 249 apply auto 250 done 251 252lemma lemma_not_dvd_hypnat_one2 [simp]: "\<exists>n \<in> - {0}. \<not> hypnat_of_nat n dvd 1" 253 using lemma_not_dvd_hypnat_one by (auto simp del: lemma_not_dvd_hypnat_one) 254 255lemma hypnat_add_one_gt_one: "\<And>N::hypnat. 0 < N \<Longrightarrow> 1 < N + 1" 256 by transfer simp 257 258lemma hypnat_of_nat_zero_not_prime [simp]: "hypnat_of_nat 0 \<notin> starprime" 259 by transfer simp 260 261lemma hypnat_zero_not_prime [simp]: "0 \<notin> starprime" 262 using hypnat_of_nat_zero_not_prime by simp 263 264lemma hypnat_of_nat_one_not_prime [simp]: "hypnat_of_nat 1 \<notin> starprime" 265 by transfer simp 266 267lemma hypnat_one_not_prime [simp]: "1 \<notin> starprime" 268 using hypnat_of_nat_one_not_prime by simp 269 270lemma hdvd_diff: "\<And>k m n :: hypnat. k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m - n)" 271 by transfer (rule dvd_diff_nat) 272 273lemma hdvd_one_eq_one: "\<And>x::hypnat. is_unit x \<Longrightarrow> x = 1" 274 by transfer simp 275 276text \<open>Already proved as \<open>primes_infinite\<close>, but now using non-standard naturals.\<close> 277theorem not_finite_prime: "\<not> finite {p::nat. prime p}" 278 apply (rule hypnat_infinite_has_nonstandard_iff [THEN iffD2]) 279 using hypnat_dvd_all_hypnat_of_nat 280 apply clarify 281 apply (drule hypnat_add_one_gt_one) 282 apply (drule hyperprime_factor_exists) 283 apply clarify 284 apply (subgoal_tac "k \<notin> hypnat_of_nat ` {p. prime p}") 285 apply (force simp: starprime_def) 286 apply (metis Compl_iff add.commute dvd_add_left_iff empty_iff hdvd_one_eq_one hypnat_one_not_prime 287 imageE insert_iff mem_Collect_eq not_prime_0) 288 done 289 290end 291