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