|
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 |
|
7 header{*The Nonstandard Primes as an Extension of the Prime Numbers*} |
|
8 |
|
9 theory NSPrimes |
|
10 imports "~~/src/HOL/NumberTheory/Factorization" Hyperreal |
|
11 begin |
|
12 |
|
13 text{*These can be used to derive an alternative proof of the infinitude of |
|
14 primes by considering a property of nonstandard sets.*} |
|
15 |
|
16 definition |
|
17 hdvd :: "[hypnat, hypnat] => bool" (infixl "hdvd" 50) where |
|
18 [transfer_unfold]: "(M::hypnat) hdvd N = ( *p2* (op dvd)) M N" |
|
19 |
|
20 definition |
|
21 starprime :: "hypnat set" where |
|
22 [transfer_unfold]: "starprime = ( *s* {p. prime p})" |
|
23 |
|
24 definition |
|
25 choicefun :: "'a set => 'a" where |
|
26 "choicefun E = (@x. \<exists>X \<in> Pow(E) -{{}}. x : X)" |
|
27 |
|
28 consts injf_max :: "nat => ('a::{order} set) => 'a" |
|
29 primrec |
|
30 injf_max_zero: "injf_max 0 E = choicefun E" |
|
31 injf_max_Suc: "injf_max (Suc n) E = choicefun({e. e:E & injf_max n E < e})" |
|
32 |
|
33 |
|
34 lemma dvd_by_all: "\<forall>M. \<exists>N. 0 < N & (\<forall>m. 0 < m & (m::nat) <= M --> m dvd N)" |
|
35 apply (rule allI) |
|
36 apply (induct_tac "M", auto) |
|
37 apply (rule_tac x = "N * (Suc n) " in exI) |
|
38 apply (safe, force) |
|
39 apply (drule le_imp_less_or_eq, erule disjE) |
|
40 apply (force intro!: dvd_mult2) |
|
41 apply (force intro!: dvd_mult) |
|
42 done |
|
43 |
|
44 lemmas dvd_by_all2 = dvd_by_all [THEN spec, standard] |
|
45 |
|
46 lemma hypnat_of_nat_le_zero_iff: "(hypnat_of_nat n <= 0) = (n = 0)" |
|
47 by (transfer, simp) |
|
48 declare hypnat_of_nat_le_zero_iff [simp] |
|
49 |
|
50 |
|
51 (* Goldblatt: Exercise 5.11(2) - p. 57 *) |
|
52 lemma hdvd_by_all: "\<forall>M. \<exists>N. 0 < N & (\<forall>m. 0 < m & (m::hypnat) <= M --> m hdvd N)" |
|
53 by (transfer, rule dvd_by_all) |
|
54 |
|
55 lemmas hdvd_by_all2 = hdvd_by_all [THEN spec, standard] |
|
56 |
|
57 (* Goldblatt: Exercise 5.11(2) - p. 57 *) |
|
58 lemma hypnat_dvd_all_hypnat_of_nat: |
|
59 "\<exists>(N::hypnat). 0 < N & (\<forall>n \<in> -{0::nat}. hypnat_of_nat(n) hdvd N)" |
|
60 apply (cut_tac hdvd_by_all) |
|
61 apply (drule_tac x = whn in spec, auto) |
|
62 apply (rule exI, auto) |
|
63 apply (drule_tac x = "hypnat_of_nat n" in spec) |
|
64 apply (auto simp add: linorder_not_less star_of_eq_0) |
|
65 done |
|
66 |
|
67 |
|
68 text{*The nonstandard extension of the set prime numbers consists of precisely |
|
69 those hypernaturals exceeding 1 that have no nontrivial factors*} |
|
70 |
|
71 (* Goldblatt: Exercise 5.11(3a) - p 57 *) |
|
72 lemma starprime: |
|
73 "starprime = {p. 1 < p & (\<forall>m. m hdvd p --> m = 1 | m = p)}" |
|
74 by (transfer, auto simp add: prime_def) |
|
75 |
|
76 lemma prime_two: "prime 2" |
|
77 apply (unfold prime_def, auto) |
|
78 apply (frule dvd_imp_le) |
|
79 apply (auto dest: dvd_0_left) |
|
80 apply (case_tac m, simp, arith) |
|
81 done |
|
82 declare prime_two [simp] |
|
83 |
|
84 (* proof uses course-of-value induction *) |
|
85 lemma prime_factor_exists [rule_format]: "Suc 0 < n --> (\<exists>k. prime k & k dvd n)" |
|
86 apply (rule_tac n = n in nat_less_induct, auto) |
|
87 apply (case_tac "prime n") |
|
88 apply (rule_tac x = n in exI, auto) |
|
89 apply (drule conjI [THEN not_prime_ex_mk], auto) |
|
90 apply (drule_tac x = m in spec, auto) |
|
91 apply (rule_tac x = ka in exI) |
|
92 apply (auto intro: dvd_mult2) |
|
93 done |
|
94 |
|
95 (* Goldblatt Exercise 5.11(3b) - p 57 *) |
|
96 lemma hyperprime_factor_exists [rule_format]: |
|
97 "!!n. 1 < n ==> (\<exists>k \<in> starprime. k hdvd n)" |
|
98 by (transfer, simp add: prime_factor_exists) |
|
99 |
|
100 (* Goldblatt Exercise 3.10(1) - p. 29 *) |
|
101 lemma NatStar_hypnat_of_nat: "finite A ==> *s* A = hypnat_of_nat ` A" |
|
102 by (rule starset_finite) |
|
103 |
|
104 |
|
105 subsection{*Another characterization of infinite set of natural numbers*} |
|
106 |
|
107 lemma finite_nat_set_bounded: "finite N ==> \<exists>n. (\<forall>i \<in> N. i<(n::nat))" |
|
108 apply (erule_tac F = N in finite_induct, auto) |
|
109 apply (rule_tac x = "Suc n + x" in exI, auto) |
|
110 done |
|
111 |
|
112 lemma finite_nat_set_bounded_iff: "finite N = (\<exists>n. (\<forall>i \<in> N. i<(n::nat)))" |
|
113 by (blast intro: finite_nat_set_bounded bounded_nat_set_is_finite) |
|
114 |
|
115 lemma not_finite_nat_set_iff: "(~ finite N) = (\<forall>n. \<exists>i \<in> N. n <= (i::nat))" |
|
116 by (auto simp add: finite_nat_set_bounded_iff not_less) |
|
117 |
|
118 lemma bounded_nat_set_is_finite2: "(\<forall>i \<in> N. i<=(n::nat)) ==> finite N" |
|
119 apply (rule finite_subset) |
|
120 apply (rule_tac [2] finite_atMost, auto) |
|
121 done |
|
122 |
|
123 lemma finite_nat_set_bounded2: "finite N ==> \<exists>n. (\<forall>i \<in> N. i<=(n::nat))" |
|
124 apply (erule_tac F = N in finite_induct, auto) |
|
125 apply (rule_tac x = "n + x" in exI, auto) |
|
126 done |
|
127 |
|
128 lemma finite_nat_set_bounded_iff2: "finite N = (\<exists>n. (\<forall>i \<in> N. i<=(n::nat)))" |
|
129 by (blast intro: finite_nat_set_bounded2 bounded_nat_set_is_finite2) |
|
130 |
|
131 lemma not_finite_nat_set_iff2: "(~ finite N) = (\<forall>n. \<exists>i \<in> N. n < (i::nat))" |
|
132 by (auto simp add: finite_nat_set_bounded_iff2 not_le) |
|
133 |
|
134 |
|
135 subsection{*An injective function cannot define an embedded natural number*} |
|
136 |
|
137 lemma lemma_infinite_set_singleton: "\<forall>m n. m \<noteq> n --> f n \<noteq> f m |
|
138 ==> {n. f n = N} = {} | (\<exists>m. {n. f n = N} = {m})" |
|
139 apply auto |
|
140 apply (drule_tac x = x in spec, auto) |
|
141 apply (subgoal_tac "\<forall>n. (f n = f x) = (x = n) ") |
|
142 apply auto |
|
143 done |
|
144 |
|
145 lemma inj_fun_not_hypnat_in_SHNat: |
|
146 assumes inj_f: "inj (f::nat=>nat)" |
|
147 shows "starfun f whn \<notin> Nats" |
|
148 proof |
|
149 from inj_f have inj_f': "inj (starfun f)" |
|
150 by (transfer inj_on_def Ball_def UNIV_def) |
|
151 assume "starfun f whn \<in> Nats" |
|
152 then obtain N where N: "starfun f whn = hypnat_of_nat N" |
|
153 by (auto simp add: Nats_def) |
|
154 hence "\<exists>n. starfun f n = hypnat_of_nat N" .. |
|
155 hence "\<exists>n. f n = N" by transfer |
|
156 then obtain n where n: "f n = N" .. |
|
157 hence "starfun f (hypnat_of_nat n) = hypnat_of_nat N" |
|
158 by transfer |
|
159 with N have "starfun f whn = starfun f (hypnat_of_nat n)" |
|
160 by simp |
|
161 with inj_f' have "whn = hypnat_of_nat n" |
|
162 by (rule injD) |
|
163 thus "False" |
|
164 by (simp add: whn_neq_hypnat_of_nat) |
|
165 qed |
|
166 |
|
167 lemma range_subset_mem_starsetNat: |
|
168 "range f <= A ==> starfun f whn \<in> *s* A" |
|
169 apply (rule_tac x="whn" in spec) |
|
170 apply (transfer, auto) |
|
171 done |
|
172 |
|
173 (*--------------------------------------------------------------------------------*) |
|
174 (* Gleason Proposition 11-5.5. pg 149, pg 155 (ex. 3) and pg. 360 *) |
|
175 (* Let E be a nonvoid ordered set with no maximal elements (note: effectively an *) |
|
176 (* infinite set if we take E = N (Nats)). Then there exists an order-preserving *) |
|
177 (* injection from N to E. Of course, (as some doofus will undoubtedly point out! *) |
|
178 (* :-)) can use notion of least element in proof (i.e. no need for choice) if *) |
|
179 (* dealing with nats as we have well-ordering property *) |
|
180 (*--------------------------------------------------------------------------------*) |
|
181 |
|
182 lemma lemmaPow3: "E \<noteq> {} ==> \<exists>x. \<exists>X \<in> (Pow E - {{}}). x: X" |
|
183 by auto |
|
184 |
|
185 lemma choicefun_mem_set: "E \<noteq> {} ==> choicefun E \<in> E" |
|
186 apply (unfold choicefun_def) |
|
187 apply (rule lemmaPow3 [THEN someI2_ex], auto) |
|
188 done |
|
189 declare choicefun_mem_set [simp] |
|
190 |
|
191 lemma injf_max_mem_set: "[| E \<noteq>{}; \<forall>x. \<exists>y \<in> E. x < y |] ==> injf_max n E \<in> E" |
|
192 apply (induct_tac "n", force) |
|
193 apply (simp (no_asm) add: choicefun_def) |
|
194 apply (rule lemmaPow3 [THEN someI2_ex], auto) |
|
195 done |
|
196 |
|
197 lemma injf_max_order_preserving: "\<forall>x. \<exists>y \<in> E. x < y ==> injf_max n E < injf_max (Suc n) E" |
|
198 apply (simp (no_asm) add: choicefun_def) |
|
199 apply (rule lemmaPow3 [THEN someI2_ex], auto) |
|
200 done |
|
201 |
|
202 lemma injf_max_order_preserving2: "\<forall>x. \<exists>y \<in> E. x < y |
|
203 ==> \<forall>n m. m < n --> injf_max m E < injf_max n E" |
|
204 apply (rule allI) |
|
205 apply (induct_tac "n", auto) |
|
206 apply (simp (no_asm) add: choicefun_def) |
|
207 apply (rule lemmaPow3 [THEN someI2_ex]) |
|
208 apply (auto simp add: less_Suc_eq) |
|
209 apply (drule_tac x = m in spec) |
|
210 apply (drule subsetD, auto) |
|
211 apply (drule_tac x = "injf_max m E" in order_less_trans, auto) |
|
212 done |
|
213 |
|
214 lemma inj_injf_max: "\<forall>x. \<exists>y \<in> E. x < y ==> inj (%n. injf_max n E)" |
|
215 apply (rule inj_onI) |
|
216 apply (rule ccontr, auto) |
|
217 apply (drule injf_max_order_preserving2) |
|
218 apply (metis linorder_antisym_conv3 order_less_le) |
|
219 done |
|
220 |
|
221 lemma infinite_set_has_order_preserving_inj: |
|
222 "[| (E::('a::{order} set)) \<noteq> {}; \<forall>x. \<exists>y \<in> E. x < y |] |
|
223 ==> \<exists>f. range f <= E & inj (f::nat => 'a) & (\<forall>m. f m < f(Suc m))" |
|
224 apply (rule_tac x = "%n. injf_max n E" in exI, safe) |
|
225 apply (rule injf_max_mem_set) |
|
226 apply (rule_tac [3] inj_injf_max) |
|
227 apply (rule_tac [4] injf_max_order_preserving, auto) |
|
228 done |
|
229 |
|
230 text{*Only need the existence of an injective function from N to A for proof*} |
|
231 |
|
232 lemma hypnat_infinite_has_nonstandard: |
|
233 "~ finite A ==> hypnat_of_nat ` A < ( *s* A)" |
|
234 apply auto |
|
235 apply (subgoal_tac "A \<noteq> {}") |
|
236 prefer 2 apply force |
|
237 apply (drule infinite_set_has_order_preserving_inj) |
|
238 apply (erule not_finite_nat_set_iff2 [THEN iffD1], auto) |
|
239 apply (drule inj_fun_not_hypnat_in_SHNat) |
|
240 apply (drule range_subset_mem_starsetNat) |
|
241 apply (auto simp add: SHNat_eq) |
|
242 done |
|
243 |
|
244 lemma starsetNat_eq_hypnat_of_nat_image_finite: "*s* A = hypnat_of_nat ` A ==> finite A" |
|
245 apply (rule ccontr) |
|
246 apply (auto dest: hypnat_infinite_has_nonstandard) |
|
247 done |
|
248 |
|
249 lemma finite_starsetNat_iff: "( *s* A = hypnat_of_nat ` A) = (finite A)" |
|
250 by (blast intro!: starsetNat_eq_hypnat_of_nat_image_finite NatStar_hypnat_of_nat) |
|
251 |
|
252 lemma hypnat_infinite_has_nonstandard_iff: "(~ finite A) = (hypnat_of_nat ` A < *s* A)" |
|
253 apply (rule iffI) |
|
254 apply (blast intro!: hypnat_infinite_has_nonstandard) |
|
255 apply (auto simp add: finite_starsetNat_iff [symmetric]) |
|
256 done |
|
257 |
|
258 subsection{*Existence of Infinitely Many Primes: a Nonstandard Proof*} |
|
259 |
|
260 lemma lemma_not_dvd_hypnat_one: "~ (\<forall>n \<in> - {0}. hypnat_of_nat n hdvd 1)" |
|
261 apply auto |
|
262 apply (rule_tac x = 2 in bexI) |
|
263 apply (transfer, auto) |
|
264 done |
|
265 declare lemma_not_dvd_hypnat_one [simp] |
|
266 |
|
267 lemma lemma_not_dvd_hypnat_one2: "\<exists>n \<in> - {0}. ~ hypnat_of_nat n hdvd 1" |
|
268 apply (cut_tac lemma_not_dvd_hypnat_one) |
|
269 apply (auto simp del: lemma_not_dvd_hypnat_one) |
|
270 done |
|
271 declare lemma_not_dvd_hypnat_one2 [simp] |
|
272 |
|
273 (* not needed here *) |
|
274 lemma hypnat_gt_zero_gt_one: |
|
275 "!!N. [| 0 < (N::hypnat); N \<noteq> 1 |] ==> 1 < N" |
|
276 by (transfer, simp) |
|
277 |
|
278 lemma hypnat_add_one_gt_one: |
|
279 "!!N. 0 < N ==> 1 < (N::hypnat) + 1" |
|
280 by (transfer, simp) |
|
281 |
|
282 lemma zero_not_prime: "\<not> prime 0" |
|
283 apply safe |
|
284 apply (drule prime_g_zero, auto) |
|
285 done |
|
286 declare zero_not_prime [simp] |
|
287 |
|
288 lemma hypnat_of_nat_zero_not_prime: "hypnat_of_nat 0 \<notin> starprime" |
|
289 by (transfer, simp) |
|
290 declare hypnat_of_nat_zero_not_prime [simp] |
|
291 |
|
292 lemma hypnat_zero_not_prime: |
|
293 "0 \<notin> starprime" |
|
294 by (cut_tac hypnat_of_nat_zero_not_prime, simp) |
|
295 declare hypnat_zero_not_prime [simp] |
|
296 |
|
297 lemma one_not_prime: "\<not> prime 1" |
|
298 apply safe |
|
299 apply (drule prime_g_one, auto) |
|
300 done |
|
301 declare one_not_prime [simp] |
|
302 |
|
303 lemma one_not_prime2: "\<not> prime(Suc 0)" |
|
304 apply safe |
|
305 apply (drule prime_g_one, auto) |
|
306 done |
|
307 declare one_not_prime2 [simp] |
|
308 |
|
309 lemma hypnat_of_nat_one_not_prime: "hypnat_of_nat 1 \<notin> starprime" |
|
310 by (transfer, simp) |
|
311 declare hypnat_of_nat_one_not_prime [simp] |
|
312 |
|
313 lemma hypnat_one_not_prime: "1 \<notin> starprime" |
|
314 by (cut_tac hypnat_of_nat_one_not_prime, simp) |
|
315 declare hypnat_one_not_prime [simp] |
|
316 |
|
317 lemma hdvd_diff: "!!k m n. [| k hdvd m; k hdvd n |] ==> k hdvd (m - n)" |
|
318 by (transfer, rule dvd_diff) |
|
319 |
|
320 lemma dvd_one_eq_one: "x dvd (1::nat) ==> x = 1" |
|
321 by (unfold dvd_def, auto) |
|
322 |
|
323 lemma hdvd_one_eq_one: "!!x. x hdvd 1 ==> x = 1" |
|
324 by (transfer, rule dvd_one_eq_one) |
|
325 |
|
326 theorem not_finite_prime: "~ finite {p. prime p}" |
|
327 apply (rule hypnat_infinite_has_nonstandard_iff [THEN iffD2]) |
|
328 apply (cut_tac hypnat_dvd_all_hypnat_of_nat) |
|
329 apply (erule exE) |
|
330 apply (erule conjE) |
|
331 apply (subgoal_tac "1 < N + 1") |
|
332 prefer 2 apply (blast intro: hypnat_add_one_gt_one) |
|
333 apply (drule hyperprime_factor_exists) |
|
334 apply auto |
|
335 apply (subgoal_tac "k \<notin> hypnat_of_nat ` {p. prime p}") |
|
336 apply (force simp add: starprime_def, safe) |
|
337 apply (drule_tac x = x in bspec) |
|
338 apply (rule ccontr, simp) |
|
339 apply (drule hdvd_diff, assumption) |
|
340 apply (auto dest: hdvd_one_eq_one) |
|
341 done |
|
342 |
|
343 end |