author | huffman |
Mon, 12 Sep 2005 23:13:46 +0200 | |
changeset 17331 | 6b8b27894133 |
parent 17319 | 14c6e073252f |
child 17429 | e8d6ed3aacfe |
permissions | -rw-r--r-- |
13957 | 1 |
(* Title : NSPrimes.thy |
2 |
Author : Jacques D. Fleuriot |
|
3 |
Copyright : 2002 University of Edinburgh |
|
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
4 |
Conversion to Isar and new proofs by Lawrence C Paulson, 2004 |
13957 | 5 |
*) |
6 |
||
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
7 |
header{*The Nonstandard Primes as an Extension of the Prime Numbers*} |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
8 |
|
15149 | 9 |
theory NSPrimes |
10 |
imports "~~/src/HOL/NumberTheory/Factorization" Complex_Main |
|
11 |
begin |
|
13957 | 12 |
|
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
13 |
text{*These can be used to derive an alternative proof of the infinitude of |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
14 |
primes by considering a property of nonstandard sets.*} |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
15 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
16 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
17 |
constdefs |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
18 |
hdvd :: "[hypnat, hypnat] => bool" (infixl "hdvd" 50) |
17319 | 19 |
"(M::hypnat) hdvd N == ( *p2* (op dvd)) M N" |
17331 | 20 |
|
21 |
declare hdvd_def [transfer_unfold] |
|
22 |
||
13957 | 23 |
constdefs |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
24 |
starprime :: "hypnat set" |
17319 | 25 |
"starprime == ( *s* {p. prime p})" |
13957 | 26 |
|
17331 | 27 |
declare starprime_def [transfer_unfold] |
28 |
||
13957 | 29 |
constdefs |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
30 |
choicefun :: "'a set => 'a" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
31 |
"choicefun E == (@x. \<exists>X \<in> Pow(E) -{{}}. x : X)" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
32 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
33 |
consts injf_max :: "nat => ('a::{order} set) => 'a" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
34 |
primrec |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
35 |
injf_max_zero: "injf_max 0 E = choicefun E" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
36 |
injf_max_Suc: "injf_max (Suc n) E = choicefun({e. e:E & injf_max n E < e})" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
37 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
38 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
39 |
text{*A "choice" theorem for ultrafilters, like almost everywhere |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
40 |
quantification*} |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
41 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
42 |
lemma UF_choice: "{n. \<exists>m. Q n m} : FreeUltrafilterNat |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
43 |
==> \<exists>f. {n. Q n (f n)} : FreeUltrafilterNat" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
44 |
apply (rule_tac x = "%n. (@x. Q n x) " in exI) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
45 |
apply (ultra, rule someI, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
46 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
47 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
48 |
lemma UF_if: "({n. P n} : FreeUltrafilterNat --> {n. Q n} : FreeUltrafilterNat) = |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
49 |
({n. P n --> Q n} : FreeUltrafilterNat)" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
50 |
apply auto |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
51 |
apply ultra+ |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
52 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
53 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
54 |
lemma UF_conj: "({n. P n} : FreeUltrafilterNat & {n. Q n} : FreeUltrafilterNat) = |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
55 |
({n. P n & Q n} : FreeUltrafilterNat)" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
56 |
apply auto |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
57 |
apply ultra+ |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
58 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
59 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
60 |
lemma UF_choice_ccontr: "(\<forall>f. {n. Q n (f n)} : FreeUltrafilterNat) = |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
61 |
({n. \<forall>m. Q n m} : FreeUltrafilterNat)" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
62 |
apply auto |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
63 |
prefer 2 apply ultra |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
64 |
apply (rule ccontr) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
65 |
apply (rule contrapos_np) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
66 |
apply (erule_tac [2] asm_rl) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
67 |
apply (simp (no_asm) add: FreeUltrafilterNat_Compl_iff1 Collect_neg_eq [symmetric]) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
68 |
apply (rule UF_choice, ultra) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
69 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
70 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
71 |
lemma dvd_by_all: "\<forall>M. \<exists>N. 0 < N & (\<forall>m. 0 < m & (m::nat) <= M --> m dvd N)" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
72 |
apply (rule allI) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
73 |
apply (induct_tac "M", auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
74 |
apply (rule_tac x = "N * (Suc n) " in exI) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
75 |
apply (safe, force) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
76 |
apply (drule le_imp_less_or_eq, erule disjE) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
77 |
apply (force intro!: dvd_mult2) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
78 |
apply (force intro!: dvd_mult) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
79 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
80 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
81 |
lemmas dvd_by_all2 = dvd_by_all [THEN spec, standard] |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
82 |
|
17319 | 83 |
lemma lemma_hypnat_P_EX: "(\<exists>(x::hypnat). P x) = (\<exists>f. P (star_n f))" |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
84 |
apply auto |
17319 | 85 |
apply (rule_tac x = x in star_cases, auto) |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
86 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
87 |
|
17319 | 88 |
lemma lemma_hypnat_P_ALL: "(\<forall>(x::hypnat). P x) = (\<forall>f. P (star_n f))" |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
89 |
apply auto |
17319 | 90 |
apply (rule_tac x = x in star_cases, auto) |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
91 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
92 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
93 |
lemma hdvd: |
17319 | 94 |
"(star_n X hdvd star_n Y) = |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
95 |
({n. X n dvd Y n} : FreeUltrafilterNat)" |
17319 | 96 |
by (simp add: hdvd_def starP2) |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
97 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
98 |
lemma hypnat_of_nat_le_zero_iff: "(hypnat_of_nat n <= 0) = (n = 0)" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
99 |
by (subst hypnat_of_nat_zero [symmetric], auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
100 |
declare hypnat_of_nat_le_zero_iff [simp] |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
101 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
102 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
103 |
(* Goldblatt: Exercise 5.11(2) - p. 57 *) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
104 |
lemma hdvd_by_all: "\<forall>M. \<exists>N. 0 < N & (\<forall>m. 0 < m & (m::hypnat) <= M --> m hdvd N)" |
17331 | 105 |
by (transfer, rule dvd_by_all) |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
106 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
107 |
lemmas hdvd_by_all2 = hdvd_by_all [THEN spec, standard] |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
108 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
109 |
(* Goldblatt: Exercise 5.11(2) - p. 57 *) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
110 |
lemma hypnat_dvd_all_hypnat_of_nat: |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
111 |
"\<exists>(N::hypnat). 0 < N & (\<forall>n \<in> -{0::nat}. hypnat_of_nat(n) hdvd N)" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
112 |
apply (cut_tac hdvd_by_all) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
113 |
apply (drule_tac x = whn in spec, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
114 |
apply (rule exI, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
115 |
apply (drule_tac x = "hypnat_of_nat n" in spec) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
116 |
apply (auto simp add: linorder_not_less hypnat_of_nat_zero_iff) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
117 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
118 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
119 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
120 |
text{*The nonstandard extension of the set prime numbers consists of precisely |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
121 |
those hypernaturals exceeding 1 that have no nontrivial factors*} |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
122 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
123 |
(* Goldblatt: Exercise 5.11(3a) - p 57 *) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
124 |
lemma starprime: |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
125 |
"starprime = {p. 1 < p & (\<forall>m. m hdvd p --> m = 1 | m = p)}" |
17331 | 126 |
by (transfer, auto simp add: prime_def) |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
127 |
|
16663 | 128 |
lemma prime_two: "prime 2" |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
129 |
apply (unfold prime_def, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
130 |
apply (frule dvd_imp_le) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
131 |
apply (auto dest: dvd_0_left) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
132 |
apply (case_tac m, simp, arith) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
133 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
134 |
declare prime_two [simp] |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
135 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
136 |
(* proof uses course-of-value induction *) |
16663 | 137 |
lemma prime_factor_exists [rule_format]: "Suc 0 < n --> (\<exists>k. prime k & k dvd n)" |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
138 |
apply (rule_tac n = n in nat_less_induct, auto) |
16663 | 139 |
apply (case_tac "prime n") |
140 |
apply (rule_tac x = n in exI, auto) |
|
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
141 |
apply (drule conjI [THEN not_prime_ex_mk], auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
142 |
apply (drule_tac x = m in spec, auto) |
16663 | 143 |
apply (rule_tac x = ka in exI) |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
144 |
apply (auto intro: dvd_mult2) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
145 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
146 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
147 |
(* Goldblatt Exercise 5.11(3b) - p 57 *) |
17319 | 148 |
lemma hyperprime_factor_exists [rule_format]: |
149 |
"!!n. 1 < n ==> (\<exists>k \<in> starprime. k hdvd n)" |
|
17331 | 150 |
by (transfer, simp add: prime_factor_exists) |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
151 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
152 |
(* Goldblatt Exercise 3.10(1) - p. 29 *) |
17319 | 153 |
lemma NatStar_hypnat_of_nat: "finite A ==> *s* A = hypnat_of_nat ` A" |
154 |
apply (rule_tac P = "%x. *s* x = hypnat_of_nat ` x" in finite_induct) |
|
155 |
apply auto |
|
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
156 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
157 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
158 |
(* proved elsewhere? *) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
159 |
lemma FreeUltrafilterNat_singleton_not_mem: "{x} \<notin> FreeUltrafilterNat" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
160 |
by (auto intro!: FreeUltrafilterNat_finite) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
161 |
declare FreeUltrafilterNat_singleton_not_mem [simp] |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
162 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
163 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
164 |
subsection{*Another characterization of infinite set of natural numbers*} |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
165 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
166 |
lemma finite_nat_set_bounded: "finite N ==> \<exists>n. (\<forall>i \<in> N. i<(n::nat))" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
167 |
apply (erule_tac F = N in finite_induct, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
168 |
apply (rule_tac x = "Suc n + x" in exI, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
169 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
170 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
171 |
lemma finite_nat_set_bounded_iff: "finite N = (\<exists>n. (\<forall>i \<in> N. i<(n::nat)))" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
172 |
by (blast intro: finite_nat_set_bounded bounded_nat_set_is_finite) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
173 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
174 |
lemma not_finite_nat_set_iff: "(~ finite N) = (\<forall>n. \<exists>i \<in> N. n <= (i::nat))" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
175 |
by (auto simp add: finite_nat_set_bounded_iff le_def) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
176 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
177 |
lemma bounded_nat_set_is_finite2: "(\<forall>i \<in> N. i<=(n::nat)) ==> finite N" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
178 |
apply (rule finite_subset) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
179 |
apply (rule_tac [2] finite_atMost, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
180 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
181 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
182 |
lemma finite_nat_set_bounded2: "finite N ==> \<exists>n. (\<forall>i \<in> N. i<=(n::nat))" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
183 |
apply (erule_tac F = N in finite_induct, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
184 |
apply (rule_tac x = "n + x" in exI, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
185 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
186 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
187 |
lemma finite_nat_set_bounded_iff2: "finite N = (\<exists>n. (\<forall>i \<in> N. i<=(n::nat)))" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
188 |
by (blast intro: finite_nat_set_bounded2 bounded_nat_set_is_finite2) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
189 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
190 |
lemma not_finite_nat_set_iff2: "(~ finite N) = (\<forall>n. \<exists>i \<in> N. n < (i::nat))" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
191 |
by (auto simp add: finite_nat_set_bounded_iff2 le_def) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
192 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
193 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
194 |
subsection{*An injective function cannot define an embedded natural number*} |
13957 | 195 |
|
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
196 |
lemma lemma_infinite_set_singleton: "\<forall>m n. m \<noteq> n --> f n \<noteq> f m |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
197 |
==> {n. f n = N} = {} | (\<exists>m. {n. f n = N} = {m})" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
198 |
apply auto |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
199 |
apply (drule_tac x = x in spec, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
200 |
apply (subgoal_tac "\<forall>n. (f n = f x) = (x = n) ") |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
201 |
apply auto |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
202 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
203 |
|
17319 | 204 |
lemma inj_fun_not_hypnat_in_SHNat: "inj (f::nat=>nat) ==> star_n f \<notin> Nats" |
205 |
apply (auto simp add: SHNat_eq hypnat_of_nat_eq star_n_eq_iff) |
|
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
206 |
apply (subgoal_tac "\<forall>m n. m \<noteq> n --> f n \<noteq> f m", auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
207 |
apply (drule_tac [2] injD) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
208 |
prefer 2 apply assumption |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
209 |
apply (drule_tac N = N in lemma_infinite_set_singleton, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
210 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
211 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
212 |
lemma range_subset_mem_starsetNat: |
17319 | 213 |
"range f <= A ==> star_n f \<in> *s* A" |
214 |
apply (simp add: Iset_of_def star_of_def Iset_star_n) |
|
215 |
apply (subgoal_tac "\<forall>n. f n \<in> A", auto) |
|
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
216 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
217 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
218 |
(*--------------------------------------------------------------------------------*) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
219 |
(* Gleason Proposition 11-5.5. pg 149, pg 155 (ex. 3) and pg. 360 *) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
220 |
(* Let E be a nonvoid ordered set with no maximal elements (note: effectively an *) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
221 |
(* infinite set if we take E = N (Nats)). Then there exists an order-preserving *) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
222 |
(* injection from N to E. Of course, (as some doofus will undoubtedly point out! *) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
223 |
(* :-)) can use notion of least element in proof (i.e. no need for choice) if *) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
224 |
(* dealing with nats as we have well-ordering property *) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
225 |
(*--------------------------------------------------------------------------------*) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
226 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
227 |
lemma lemmaPow3: "E \<noteq> {} ==> \<exists>x. \<exists>X \<in> (Pow E - {{}}). x: X" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
228 |
by auto |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
229 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
230 |
lemma choicefun_mem_set: "E \<noteq> {} ==> choicefun E \<in> E" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
231 |
apply (unfold choicefun_def) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
232 |
apply (rule lemmaPow3 [THEN someI2_ex], auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
233 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
234 |
declare choicefun_mem_set [simp] |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
235 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
236 |
lemma injf_max_mem_set: "[| E \<noteq>{}; \<forall>x. \<exists>y \<in> E. x < y |] ==> injf_max n E \<in> E" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
237 |
apply (induct_tac "n", force) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
238 |
apply (simp (no_asm) add: choicefun_def) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
239 |
apply (rule lemmaPow3 [THEN someI2_ex], auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
240 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
241 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
242 |
lemma injf_max_order_preserving: "\<forall>x. \<exists>y \<in> E. x < y ==> injf_max n E < injf_max (Suc n) E" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
243 |
apply (simp (no_asm) add: choicefun_def) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
244 |
apply (rule lemmaPow3 [THEN someI2_ex], auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
245 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
246 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
247 |
lemma injf_max_order_preserving2: "\<forall>x. \<exists>y \<in> E. x < y |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
248 |
==> \<forall>n m. m < n --> injf_max m E < injf_max n E" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
249 |
apply (rule allI) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
250 |
apply (induct_tac "n", auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
251 |
apply (simp (no_asm) add: choicefun_def) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
252 |
apply (rule lemmaPow3 [THEN someI2_ex]) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
253 |
apply (auto simp add: less_Suc_eq) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
254 |
apply (drule_tac x = m in spec) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
255 |
apply (drule subsetD, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
256 |
apply (drule_tac x = "injf_max m E" in order_less_trans, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
257 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
258 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
259 |
lemma inj_injf_max: "\<forall>x. \<exists>y \<in> E. x < y ==> inj (%n. injf_max n E)" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
260 |
apply (rule inj_onI) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
261 |
apply (rule ccontr, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
262 |
apply (drule injf_max_order_preserving2) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
263 |
apply (cut_tac m = x and n = y in less_linear, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
264 |
apply (auto dest!: spec) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
265 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
266 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
267 |
lemma infinite_set_has_order_preserving_inj: |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
268 |
"[| (E::('a::{order} set)) \<noteq> {}; \<forall>x. \<exists>y \<in> E. x < y |] |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
269 |
==> \<exists>f. range f <= E & inj (f::nat => 'a) & (\<forall>m. f m < f(Suc m))" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
270 |
apply (rule_tac x = "%n. injf_max n E" in exI, safe) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
271 |
apply (rule injf_max_mem_set) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
272 |
apply (rule_tac [3] inj_injf_max) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
273 |
apply (rule_tac [4] injf_max_order_preserving, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
274 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
275 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
276 |
text{*Only need the existence of an injective function from N to A for proof*} |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
277 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
278 |
lemma hypnat_infinite_has_nonstandard: |
17319 | 279 |
"~ finite A ==> hypnat_of_nat ` A < ( *s* A)" |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
280 |
apply auto |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
281 |
apply (rule subsetD) |
17319 | 282 |
apply (rule STAR_star_of_image_subset, auto) |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
283 |
apply (subgoal_tac "A \<noteq> {}") |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
284 |
prefer 2 apply force |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
285 |
apply (drule infinite_set_has_order_preserving_inj) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
286 |
apply (erule not_finite_nat_set_iff2 [THEN iffD1], auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
287 |
apply (drule inj_fun_not_hypnat_in_SHNat) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
288 |
apply (drule range_subset_mem_starsetNat) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
289 |
apply (auto simp add: SHNat_eq) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
290 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
291 |
|
17319 | 292 |
lemma starsetNat_eq_hypnat_of_nat_image_finite: "*s* A = hypnat_of_nat ` A ==> finite A" |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
293 |
apply (rule ccontr) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
294 |
apply (auto dest: hypnat_infinite_has_nonstandard) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
295 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
296 |
|
17319 | 297 |
lemma finite_starsetNat_iff: "( *s* A = hypnat_of_nat ` A) = (finite A)" |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
298 |
by (blast intro!: starsetNat_eq_hypnat_of_nat_image_finite NatStar_hypnat_of_nat) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
299 |
|
17319 | 300 |
lemma hypnat_infinite_has_nonstandard_iff: "(~ finite A) = (hypnat_of_nat ` A < *s* A)" |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
301 |
apply (rule iffI) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
302 |
apply (blast intro!: hypnat_infinite_has_nonstandard) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
303 |
apply (auto simp add: finite_starsetNat_iff [symmetric]) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
304 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
305 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
306 |
subsection{*Existence of Infinitely Many Primes: a Nonstandard Proof*} |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
307 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
308 |
lemma lemma_not_dvd_hypnat_one: "~ (\<forall>n \<in> - {0}. hypnat_of_nat n hdvd 1)" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
309 |
apply auto |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
310 |
apply (rule_tac x = 2 in bexI) |
17331 | 311 |
apply (transfer, auto) |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
312 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
313 |
declare lemma_not_dvd_hypnat_one [simp] |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
314 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
315 |
lemma lemma_not_dvd_hypnat_one2: "\<exists>n \<in> - {0}. ~ hypnat_of_nat n hdvd 1" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
316 |
apply (cut_tac lemma_not_dvd_hypnat_one) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
317 |
apply (auto simp del: lemma_not_dvd_hypnat_one) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
318 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
319 |
declare lemma_not_dvd_hypnat_one2 [simp] |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
320 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
321 |
(* not needed here *) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
322 |
lemma hypnat_gt_zero_gt_one: |
17319 | 323 |
"!!N. [| 0 < (N::hypnat); N \<noteq> 1 |] ==> 1 < N" |
324 |
by (transfer, simp) |
|
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
325 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
326 |
lemma hypnat_add_one_gt_one: |
17319 | 327 |
"!!N. 0 < N ==> 1 < (N::hypnat) + 1" |
328 |
by (transfer, simp) |
|
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
329 |
|
16663 | 330 |
lemma zero_not_prime: "\<not> prime 0" |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
331 |
apply safe |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
332 |
apply (drule prime_g_zero, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
333 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
334 |
declare zero_not_prime [simp] |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
335 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
336 |
lemma hypnat_of_nat_zero_not_prime: "hypnat_of_nat 0 \<notin> starprime" |
17331 | 337 |
by (transfer, simp) |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
338 |
declare hypnat_of_nat_zero_not_prime [simp] |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
339 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
340 |
lemma hypnat_zero_not_prime: |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
341 |
"0 \<notin> starprime" |
17319 | 342 |
by (cut_tac hypnat_of_nat_zero_not_prime, simp) |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
343 |
declare hypnat_zero_not_prime [simp] |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
344 |
|
16663 | 345 |
lemma one_not_prime: "\<not> prime 1" |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
346 |
apply safe |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
347 |
apply (drule prime_g_one, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
348 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
349 |
declare one_not_prime [simp] |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
350 |
|
16663 | 351 |
lemma one_not_prime2: "\<not> prime(Suc 0)" |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
352 |
apply safe |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
353 |
apply (drule prime_g_one, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
354 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
355 |
declare one_not_prime2 [simp] |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
356 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
357 |
lemma hypnat_of_nat_one_not_prime: "hypnat_of_nat 1 \<notin> starprime" |
17331 | 358 |
by (transfer, simp) |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
359 |
declare hypnat_of_nat_one_not_prime [simp] |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
360 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
361 |
lemma hypnat_one_not_prime: "1 \<notin> starprime" |
17319 | 362 |
by (cut_tac hypnat_of_nat_one_not_prime, simp) |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
363 |
declare hypnat_one_not_prime [simp] |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
364 |
|
17319 | 365 |
lemma hdvd_diff: "!!k m n. [| k hdvd m; k hdvd n |] ==> k hdvd (m - n)" |
17331 | 366 |
by (transfer, rule dvd_diff) |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
367 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
368 |
lemma dvd_one_eq_one: "x dvd (1::nat) ==> x = 1" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
369 |
by (unfold dvd_def, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
370 |
|
17319 | 371 |
lemma hdvd_one_eq_one: "!!x. x hdvd 1 ==> x = 1" |
17331 | 372 |
by (transfer, rule dvd_one_eq_one) |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
373 |
|
16663 | 374 |
theorem not_finite_prime: "~ finite {p. prime p}" |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
375 |
apply (rule hypnat_infinite_has_nonstandard_iff [THEN iffD2]) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
376 |
apply (cut_tac hypnat_dvd_all_hypnat_of_nat) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
377 |
apply (erule exE) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
378 |
apply (erule conjE) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
379 |
apply (subgoal_tac "1 < N + 1") |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
380 |
prefer 2 apply (blast intro: hypnat_add_one_gt_one) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
381 |
apply (drule hyperprime_factor_exists) |
17319 | 382 |
apply (auto intro: STAR_mem) |
16663 | 383 |
apply (subgoal_tac "k \<notin> hypnat_of_nat ` {p. prime p}") |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
384 |
apply (force simp add: starprime_def, safe) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
385 |
apply (drule_tac x = x in bspec) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
386 |
apply (rule ccontr, simp) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
387 |
apply (drule hdvd_diff, assumption) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
388 |
apply (auto dest: hdvd_one_eq_one) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
389 |
done |
13957 | 390 |
|
391 |
end |