author | haftmann |
Fri, 15 Feb 2008 16:09:12 +0100 | |
changeset 26072 | f65a7fa2da6c |
parent 24742 | 73b8b42a36b6 |
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 |
|
19736 | 16 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20744
diff
changeset
|
17 |
hdvd :: "[hypnat, hypnat] => bool" (infixl "hdvd" 50) where |
19736 | 18 |
[transfer_unfold]: "(M::hypnat) hdvd N = ( *p2* (op dvd)) M N" |
17331 | 19 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20744
diff
changeset
|
20 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20744
diff
changeset
|
21 |
starprime :: "hypnat set" where |
19736 | 22 |
[transfer_unfold]: "starprime = ( *s* {p. prime p})" |
13957 | 23 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20744
diff
changeset
|
24 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20744
diff
changeset
|
25 |
choicefun :: "'a set => 'a" where |
19736 | 26 |
"choicefun E = (@x. \<exists>X \<in> Pow(E) -{{}}. x : X)" |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
27 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
28 |
consts injf_max :: "nat => ('a::{order} set) => 'a" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
29 |
primrec |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
30 |
injf_max_zero: "injf_max 0 E = choicefun E" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
31 |
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
|
32 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
33 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
34 |
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
|
35 |
apply (rule allI) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
36 |
apply (induct_tac "M", auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
37 |
apply (rule_tac x = "N * (Suc n) " in exI) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
38 |
apply (safe, force) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
39 |
apply (drule le_imp_less_or_eq, erule disjE) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
40 |
apply (force intro!: dvd_mult2) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
41 |
apply (force intro!: dvd_mult) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
42 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
43 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
44 |
lemmas dvd_by_all2 = dvd_by_all [THEN spec, standard] |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
45 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
46 |
lemma hypnat_of_nat_le_zero_iff: "(hypnat_of_nat n <= 0) = (n = 0)" |
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17331
diff
changeset
|
47 |
by (transfer, simp) |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
48 |
declare hypnat_of_nat_le_zero_iff [simp] |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
49 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
50 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
51 |
(* Goldblatt: Exercise 5.11(2) - p. 57 *) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
52 |
lemma hdvd_by_all: "\<forall>M. \<exists>N. 0 < N & (\<forall>m. 0 < m & (m::hypnat) <= M --> m hdvd N)" |
17331 | 53 |
by (transfer, rule dvd_by_all) |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
54 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
55 |
lemmas hdvd_by_all2 = hdvd_by_all [THEN spec, standard] |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
56 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
57 |
(* Goldblatt: Exercise 5.11(2) - p. 57 *) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
58 |
lemma hypnat_dvd_all_hypnat_of_nat: |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
59 |
"\<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
|
60 |
apply (cut_tac hdvd_by_all) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
61 |
apply (drule_tac x = whn in spec, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
62 |
apply (rule exI, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
63 |
apply (drule_tac x = "hypnat_of_nat n" in spec) |
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
17331
diff
changeset
|
64 |
apply (auto simp add: linorder_not_less star_of_eq_0) |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
65 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
66 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
67 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
68 |
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
|
69 |
those hypernaturals exceeding 1 that have no nontrivial factors*} |
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 |
(* Goldblatt: Exercise 5.11(3a) - p 57 *) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
72 |
lemma starprime: |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
73 |
"starprime = {p. 1 < p & (\<forall>m. m hdvd p --> m = 1 | m = p)}" |
17331 | 74 |
by (transfer, auto simp add: prime_def) |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
75 |
|
16663 | 76 |
lemma prime_two: "prime 2" |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
77 |
apply (unfold prime_def, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
78 |
apply (frule dvd_imp_le) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
79 |
apply (auto dest: dvd_0_left) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
80 |
apply (case_tac m, simp, arith) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
81 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
82 |
declare prime_two [simp] |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
83 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
84 |
(* proof uses course-of-value induction *) |
16663 | 85 |
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
|
86 |
apply (rule_tac n = n in nat_less_induct, auto) |
16663 | 87 |
apply (case_tac "prime n") |
88 |
apply (rule_tac x = n in exI, auto) |
|
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
89 |
apply (drule conjI [THEN not_prime_ex_mk], auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
90 |
apply (drule_tac x = m in spec, auto) |
16663 | 91 |
apply (rule_tac x = ka in exI) |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
92 |
apply (auto intro: dvd_mult2) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
93 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
94 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
95 |
(* Goldblatt Exercise 5.11(3b) - p 57 *) |
17319 | 96 |
lemma hyperprime_factor_exists [rule_format]: |
97 |
"!!n. 1 < n ==> (\<exists>k \<in> starprime. k hdvd n)" |
|
17331 | 98 |
by (transfer, simp add: prime_factor_exists) |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
99 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
100 |
(* Goldblatt Exercise 3.10(1) - p. 29 *) |
17319 | 101 |
lemma NatStar_hypnat_of_nat: "finite A ==> *s* A = hypnat_of_nat ` A" |
20744
d05d90c8291f
removed all references to star_n and FreeUltrafilterNat
huffman
parents:
20733
diff
changeset
|
102 |
by (rule starset_finite) |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
103 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
104 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
105 |
subsection{*Another characterization of infinite set of natural numbers*} |
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 |
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
|
108 |
apply (erule_tac F = N in finite_induct, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
109 |
apply (rule_tac x = "Suc n + x" in exI, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
110 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
111 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
112 |
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
|
113 |
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
|
114 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
115 |
lemma not_finite_nat_set_iff: "(~ finite N) = (\<forall>n. \<exists>i \<in> N. n <= (i::nat))" |
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
24742
diff
changeset
|
116 |
by (auto simp add: finite_nat_set_bounded_iff not_less) |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
117 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
118 |
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
|
119 |
apply (rule finite_subset) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
120 |
apply (rule_tac [2] finite_atMost, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
121 |
done |
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 |
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
|
124 |
apply (erule_tac F = N in finite_induct, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
125 |
apply (rule_tac x = "n + x" in exI, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
126 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
127 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
128 |
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
|
129 |
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
|
130 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
131 |
lemma not_finite_nat_set_iff2: "(~ finite N) = (\<forall>n. \<exists>i \<in> N. n < (i::nat))" |
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
24742
diff
changeset
|
132 |
by (auto simp add: finite_nat_set_bounded_iff2 not_le) |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
133 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
134 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
135 |
subsection{*An injective function cannot define an embedded natural number*} |
13957 | 136 |
|
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
137 |
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
|
138 |
==> {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
|
139 |
apply auto |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
140 |
apply (drule_tac x = x in spec, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
141 |
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
|
142 |
apply auto |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
143 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
144 |
|
20744
d05d90c8291f
removed all references to star_n and FreeUltrafilterNat
huffman
parents:
20733
diff
changeset
|
145 |
lemma inj_fun_not_hypnat_in_SHNat: |
d05d90c8291f
removed all references to star_n and FreeUltrafilterNat
huffman
parents:
20733
diff
changeset
|
146 |
assumes inj_f: "inj (f::nat=>nat)" |
d05d90c8291f
removed all references to star_n and FreeUltrafilterNat
huffman
parents:
20733
diff
changeset
|
147 |
shows "starfun f whn \<notin> Nats" |
d05d90c8291f
removed all references to star_n and FreeUltrafilterNat
huffman
parents:
20733
diff
changeset
|
148 |
proof |
d05d90c8291f
removed all references to star_n and FreeUltrafilterNat
huffman
parents:
20733
diff
changeset
|
149 |
from inj_f have inj_f': "inj (starfun f)" |
d05d90c8291f
removed all references to star_n and FreeUltrafilterNat
huffman
parents:
20733
diff
changeset
|
150 |
by (transfer inj_on_def Ball_def UNIV_def) |
d05d90c8291f
removed all references to star_n and FreeUltrafilterNat
huffman
parents:
20733
diff
changeset
|
151 |
assume "starfun f whn \<in> Nats" |
d05d90c8291f
removed all references to star_n and FreeUltrafilterNat
huffman
parents:
20733
diff
changeset
|
152 |
then obtain N where N: "starfun f whn = hypnat_of_nat N" |
d05d90c8291f
removed all references to star_n and FreeUltrafilterNat
huffman
parents:
20733
diff
changeset
|
153 |
by (auto simp add: Nats_def) |
d05d90c8291f
removed all references to star_n and FreeUltrafilterNat
huffman
parents:
20733
diff
changeset
|
154 |
hence "\<exists>n. starfun f n = hypnat_of_nat N" .. |
d05d90c8291f
removed all references to star_n and FreeUltrafilterNat
huffman
parents:
20733
diff
changeset
|
155 |
hence "\<exists>n. f n = N" by transfer |
d05d90c8291f
removed all references to star_n and FreeUltrafilterNat
huffman
parents:
20733
diff
changeset
|
156 |
then obtain n where n: "f n = N" .. |
d05d90c8291f
removed all references to star_n and FreeUltrafilterNat
huffman
parents:
20733
diff
changeset
|
157 |
hence "starfun f (hypnat_of_nat n) = hypnat_of_nat N" |
d05d90c8291f
removed all references to star_n and FreeUltrafilterNat
huffman
parents:
20733
diff
changeset
|
158 |
by transfer |
d05d90c8291f
removed all references to star_n and FreeUltrafilterNat
huffman
parents:
20733
diff
changeset
|
159 |
with N have "starfun f whn = starfun f (hypnat_of_nat n)" |
d05d90c8291f
removed all references to star_n and FreeUltrafilterNat
huffman
parents:
20733
diff
changeset
|
160 |
by simp |
d05d90c8291f
removed all references to star_n and FreeUltrafilterNat
huffman
parents:
20733
diff
changeset
|
161 |
with inj_f' have "whn = hypnat_of_nat n" |
d05d90c8291f
removed all references to star_n and FreeUltrafilterNat
huffman
parents:
20733
diff
changeset
|
162 |
by (rule injD) |
d05d90c8291f
removed all references to star_n and FreeUltrafilterNat
huffman
parents:
20733
diff
changeset
|
163 |
thus "False" |
d05d90c8291f
removed all references to star_n and FreeUltrafilterNat
huffman
parents:
20733
diff
changeset
|
164 |
by (simp add: whn_neq_hypnat_of_nat) |
d05d90c8291f
removed all references to star_n and FreeUltrafilterNat
huffman
parents:
20733
diff
changeset
|
165 |
qed |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
166 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
167 |
lemma range_subset_mem_starsetNat: |
20744
d05d90c8291f
removed all references to star_n and FreeUltrafilterNat
huffman
parents:
20733
diff
changeset
|
168 |
"range f <= A ==> starfun f whn \<in> *s* A" |
d05d90c8291f
removed all references to star_n and FreeUltrafilterNat
huffman
parents:
20733
diff
changeset
|
169 |
apply (rule_tac x="whn" in spec) |
d05d90c8291f
removed all references to star_n and FreeUltrafilterNat
huffman
parents:
20733
diff
changeset
|
170 |
apply (transfer, auto) |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
171 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
172 |
|
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 |
(* 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
|
175 |
(* 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
|
176 |
(* 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
|
177 |
(* 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
|
178 |
(* :-)) 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
|
179 |
(* dealing with nats as we have well-ordering property *) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
180 |
(*--------------------------------------------------------------------------------*) |
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 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
|
183 |
by auto |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
184 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
185 |
lemma choicefun_mem_set: "E \<noteq> {} ==> choicefun E \<in> E" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
186 |
apply (unfold choicefun_def) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
187 |
apply (rule lemmaPow3 [THEN someI2_ex], auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
188 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
189 |
declare choicefun_mem_set [simp] |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
190 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
191 |
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
|
192 |
apply (induct_tac "n", force) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
193 |
apply (simp (no_asm) add: choicefun_def) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
194 |
apply (rule lemmaPow3 [THEN someI2_ex], auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
195 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
196 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
197 |
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
|
198 |
apply (simp (no_asm) add: choicefun_def) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
199 |
apply (rule lemmaPow3 [THEN someI2_ex], auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
200 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
201 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
202 |
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
|
203 |
==> \<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
|
204 |
apply (rule allI) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
205 |
apply (induct_tac "n", auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
206 |
apply (simp (no_asm) add: choicefun_def) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
207 |
apply (rule lemmaPow3 [THEN someI2_ex]) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
208 |
apply (auto simp add: less_Suc_eq) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
209 |
apply (drule_tac x = m in spec) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
210 |
apply (drule subsetD, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
211 |
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
|
212 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
213 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
214 |
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
|
215 |
apply (rule inj_onI) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
216 |
apply (rule ccontr, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
217 |
apply (drule injf_max_order_preserving2) |
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
paulson
parents:
21404
diff
changeset
|
218 |
apply (metis linorder_antisym_conv3 order_less_le) |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
219 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
220 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
221 |
lemma infinite_set_has_order_preserving_inj: |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
222 |
"[| (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
|
223 |
==> \<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
|
224 |
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
|
225 |
apply (rule injf_max_mem_set) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
226 |
apply (rule_tac [3] inj_injf_max) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
227 |
apply (rule_tac [4] injf_max_order_preserving, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
228 |
done |
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 |
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
|
231 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
232 |
lemma hypnat_infinite_has_nonstandard: |
17319 | 233 |
"~ finite A ==> hypnat_of_nat ` A < ( *s* A)" |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
234 |
apply auto |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
235 |
apply (subgoal_tac "A \<noteq> {}") |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
236 |
prefer 2 apply force |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
237 |
apply (drule infinite_set_has_order_preserving_inj) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
238 |
apply (erule not_finite_nat_set_iff2 [THEN iffD1], auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
239 |
apply (drule inj_fun_not_hypnat_in_SHNat) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
240 |
apply (drule range_subset_mem_starsetNat) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
241 |
apply (auto simp add: SHNat_eq) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
242 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
243 |
|
17319 | 244 |
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
|
245 |
apply (rule ccontr) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
246 |
apply (auto dest: hypnat_infinite_has_nonstandard) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
247 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
248 |
|
17319 | 249 |
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
|
250 |
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
|
251 |
|
17319 | 252 |
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
|
253 |
apply (rule iffI) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
254 |
apply (blast intro!: hypnat_infinite_has_nonstandard) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
255 |
apply (auto simp add: finite_starsetNat_iff [symmetric]) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
256 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
257 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
258 |
subsection{*Existence of Infinitely Many Primes: a Nonstandard Proof*} |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
259 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
260 |
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
|
261 |
apply auto |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
262 |
apply (rule_tac x = 2 in bexI) |
17331 | 263 |
apply (transfer, auto) |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
264 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
265 |
declare lemma_not_dvd_hypnat_one [simp] |
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 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
|
268 |
apply (cut_tac lemma_not_dvd_hypnat_one) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
269 |
apply (auto simp del: lemma_not_dvd_hypnat_one) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
270 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
271 |
declare lemma_not_dvd_hypnat_one2 [simp] |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
272 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
273 |
(* not needed here *) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
274 |
lemma hypnat_gt_zero_gt_one: |
17319 | 275 |
"!!N. [| 0 < (N::hypnat); N \<noteq> 1 |] ==> 1 < N" |
276 |
by (transfer, simp) |
|
15093
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_add_one_gt_one: |
17319 | 279 |
"!!N. 0 < N ==> 1 < (N::hypnat) + 1" |
280 |
by (transfer, simp) |
|
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
281 |
|
16663 | 282 |
lemma zero_not_prime: "\<not> prime 0" |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
283 |
apply safe |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
284 |
apply (drule prime_g_zero, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
285 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
286 |
declare zero_not_prime [simp] |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
287 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
288 |
lemma hypnat_of_nat_zero_not_prime: "hypnat_of_nat 0 \<notin> starprime" |
17331 | 289 |
by (transfer, simp) |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
290 |
declare hypnat_of_nat_zero_not_prime [simp] |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
291 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
292 |
lemma hypnat_zero_not_prime: |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
293 |
"0 \<notin> starprime" |
17319 | 294 |
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
|
295 |
declare hypnat_zero_not_prime [simp] |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
296 |
|
16663 | 297 |
lemma one_not_prime: "\<not> prime 1" |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
298 |
apply safe |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
299 |
apply (drule prime_g_one, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
300 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
301 |
declare one_not_prime [simp] |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
302 |
|
16663 | 303 |
lemma one_not_prime2: "\<not> prime(Suc 0)" |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
304 |
apply safe |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
305 |
apply (drule prime_g_one, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
306 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
307 |
declare one_not_prime2 [simp] |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
308 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
309 |
lemma hypnat_of_nat_one_not_prime: "hypnat_of_nat 1 \<notin> starprime" |
17331 | 310 |
by (transfer, simp) |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
311 |
declare hypnat_of_nat_one_not_prime [simp] |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
312 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
313 |
lemma hypnat_one_not_prime: "1 \<notin> starprime" |
17319 | 314 |
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
|
315 |
declare hypnat_one_not_prime [simp] |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
316 |
|
17319 | 317 |
lemma hdvd_diff: "!!k m n. [| k hdvd m; k hdvd n |] ==> k hdvd (m - n)" |
17331 | 318 |
by (transfer, rule dvd_diff) |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
319 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
320 |
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
|
321 |
by (unfold dvd_def, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
322 |
|
17319 | 323 |
lemma hdvd_one_eq_one: "!!x. x hdvd 1 ==> x = 1" |
17331 | 324 |
by (transfer, rule dvd_one_eq_one) |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
325 |
|
16663 | 326 |
theorem not_finite_prime: "~ finite {p. prime p}" |
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
327 |
apply (rule hypnat_infinite_has_nonstandard_iff [THEN iffD2]) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
328 |
apply (cut_tac hypnat_dvd_all_hypnat_of_nat) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
329 |
apply (erule exE) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
330 |
apply (erule conjE) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
331 |
apply (subgoal_tac "1 < N + 1") |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
332 |
prefer 2 apply (blast intro: hypnat_add_one_gt_one) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
333 |
apply (drule hyperprime_factor_exists) |
20733 | 334 |
apply auto |
16663 | 335 |
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
|
336 |
apply (force simp add: starprime_def, safe) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
337 |
apply (drule_tac x = x in bspec) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
338 |
apply (rule ccontr, simp) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
339 |
apply (drule hdvd_diff, assumption) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
340 |
apply (auto dest: hdvd_one_eq_one) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
341 |
done |
13957 | 342 |
|
343 |
end |