author | nipkow |
Thu, 19 Aug 2004 12:35:45 +0200 | |
changeset 15149 | c5c4884634b7 |
parent 15093 | 49ede01e9ee6 |
child 15166 | 66f0584aa714 |
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) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
19 |
"(M::hypnat) hdvd N == |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
20 |
\<exists>X Y. X: Rep_hypnat(M) & Y: Rep_hypnat(N) & |
13957 | 21 |
{n::nat. X n dvd Y n} : FreeUltrafilterNat" |
22 |
||
23 |
constdefs |
|
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
24 |
starprime :: "hypnat set" |
13957 | 25 |
"starprime == ( *sNat* prime)" |
26 |
||
27 |
constdefs |
|
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
28 |
choicefun :: "'a set => 'a" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
29 |
"choicefun E == (@x. \<exists>X \<in> Pow(E) -{{}}. x : X)" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
30 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
31 |
consts injf_max :: "nat => ('a::{order} set) => 'a" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
32 |
primrec |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
33 |
injf_max_zero: "injf_max 0 E = choicefun E" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
34 |
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
|
35 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
36 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
37 |
text{*A "choice" theorem for ultrafilters, like almost everywhere |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
38 |
quantification*} |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
39 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
40 |
lemma UF_choice: "{n. \<exists>m. Q n m} : FreeUltrafilterNat |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
41 |
==> \<exists>f. {n. Q n (f n)} : FreeUltrafilterNat" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
42 |
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
|
43 |
apply (ultra, rule someI, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
44 |
done |
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 UF_if: "({n. P n} : FreeUltrafilterNat --> {n. Q n} : FreeUltrafilterNat) = |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
47 |
({n. P n --> Q n} : FreeUltrafilterNat)" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
48 |
apply auto |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
49 |
apply ultra+ |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
50 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
51 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
52 |
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
|
53 |
({n. P n & Q n} : FreeUltrafilterNat)" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
54 |
apply auto |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
55 |
apply ultra+ |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
56 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
57 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
58 |
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
|
59 |
({n. \<forall>m. Q n m} : FreeUltrafilterNat)" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
60 |
apply auto |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
61 |
prefer 2 apply ultra |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
62 |
apply (rule ccontr) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
63 |
apply (rule contrapos_np) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
64 |
apply (erule_tac [2] asm_rl) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
65 |
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
|
66 |
apply (rule UF_choice, ultra) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
67 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
68 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
69 |
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
|
70 |
apply (rule allI) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
71 |
apply (induct_tac "M", auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
72 |
apply (rule_tac x = "N * (Suc n) " in exI) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
73 |
apply (safe, force) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
74 |
apply (drule le_imp_less_or_eq, erule disjE) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
75 |
apply (force intro!: dvd_mult2) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
76 |
apply (force intro!: dvd_mult) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
77 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
78 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
79 |
lemmas dvd_by_all2 = dvd_by_all [THEN spec, standard] |
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 |
lemma lemma_hypnat_P_EX: "(\<exists>(x::hypnat). P x) = (\<exists>f. P (Abs_hypnat(hypnatrel `` {f})))" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
82 |
apply auto |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
83 |
apply (rule_tac z = x in eq_Abs_hypnat, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
84 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
85 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
86 |
lemma lemma_hypnat_P_ALL: "(\<forall>(x::hypnat). P x) = (\<forall>f. P (Abs_hypnat(hypnatrel `` {f})))" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
87 |
apply auto |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
88 |
apply (rule_tac z = x in eq_Abs_hypnat, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
89 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
90 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
91 |
lemma hdvd: |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
92 |
"(Abs_hypnat(hypnatrel``{%n. X n}) hdvd |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
93 |
Abs_hypnat(hypnatrel``{%n. Y n})) = |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
94 |
({n. X n dvd Y n} : FreeUltrafilterNat)" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
95 |
apply (unfold hdvd_def) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
96 |
apply (auto, ultra) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
97 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
98 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
99 |
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
|
100 |
by (subst hypnat_of_nat_zero [symmetric], auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
101 |
declare hypnat_of_nat_le_zero_iff [simp] |
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 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
104 |
(* Goldblatt: Exercise 5.11(2) - p. 57 *) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
105 |
lemma hdvd_by_all: "\<forall>M. \<exists>N. 0 < N & (\<forall>m. 0 < m & (m::hypnat) <= M --> m hdvd N)" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
106 |
apply safe |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
107 |
apply (rule_tac z = M in eq_Abs_hypnat) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
108 |
apply (auto simp add: lemma_hypnat_P_EX lemma_hypnat_P_ALL |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
109 |
hypnat_zero_def hypnat_le hypnat_less hdvd) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
110 |
apply (cut_tac dvd_by_all) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
111 |
apply (subgoal_tac " \<forall>(n::nat) . \<exists>N. 0 < N & (\<forall>m. 0 < (m::nat) & m <= (x n) --> m dvd N)") |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
112 |
prefer 2 apply blast |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
113 |
apply (erule thin_rl) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
114 |
apply (drule choice, safe) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
115 |
apply (rule_tac x = f in exI, auto, ultra) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
116 |
apply auto |
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 |
lemmas hdvd_by_all2 = hdvd_by_all [THEN spec, standard] |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
120 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
121 |
(* Goldblatt: Exercise 5.11(2) - p. 57 *) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
122 |
lemma hypnat_dvd_all_hypnat_of_nat: |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
123 |
"\<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
|
124 |
apply (cut_tac hdvd_by_all) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
125 |
apply (drule_tac x = whn in spec, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
126 |
apply (rule exI, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
127 |
apply (drule_tac x = "hypnat_of_nat n" in spec) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
128 |
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
|
129 |
done |
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 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
132 |
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
|
133 |
those hypernaturals exceeding 1 that have no nontrivial factors*} |
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 |
(* Goldblatt: Exercise 5.11(3a) - p 57 *) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
136 |
lemma starprime: |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
137 |
"starprime = {p. 1 < p & (\<forall>m. m hdvd p --> m = 1 | m = p)}" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
138 |
apply (unfold starprime_def prime_def) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
139 |
apply (auto simp add: Collect_conj_eq NatStar_Int) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
140 |
apply (rule_tac [!] z = x in eq_Abs_hypnat) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
141 |
apply (rule_tac [2] z = m in eq_Abs_hypnat) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
142 |
apply (auto simp add: hdvd hypnat_one_def hypnat_less lemma_hypnat_P_ALL starsetNat_def) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
143 |
apply (drule bspec, drule_tac [2] bspec, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
144 |
apply (ultra, ultra) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
145 |
apply (rule ccontr) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
146 |
apply (drule FreeUltrafilterNat_Compl_mem) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
147 |
apply (auto simp add: Collect_neg_eq [symmetric]) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
148 |
apply (drule UF_choice, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
149 |
apply (drule_tac x = f in spec, auto, ultra+) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
150 |
done |
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 |
lemma prime_two: "2 : prime" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
153 |
apply (unfold prime_def, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
154 |
apply (frule dvd_imp_le) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
155 |
apply (auto dest: dvd_0_left) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
156 |
(*????arith raises exception Match!!??*) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
157 |
apply (case_tac m, simp, arith) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
158 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
159 |
declare prime_two [simp] |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
160 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
161 |
(* proof uses course-of-value induction *) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
162 |
lemma prime_factor_exists [rule_format]: "Suc 0 < n --> (\<exists>k \<in> prime. k dvd n)" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
163 |
apply (rule_tac n = n in nat_less_induct, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
164 |
apply (case_tac "n \<in> prime") |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
165 |
apply (rule_tac x = n in bexI, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
166 |
apply (drule conjI [THEN not_prime_ex_mk], auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
167 |
apply (drule_tac x = m in spec, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
168 |
apply (rule_tac x = ka in bexI) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
169 |
apply (auto intro: dvd_mult2) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
170 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
171 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
172 |
(* Goldblatt Exercise 5.11(3b) - p 57 *) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
173 |
lemma hyperprime_factor_exists [rule_format]: "1 < n ==> (\<exists>k \<in> starprime. k hdvd n)" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
174 |
apply (rule_tac z = n in eq_Abs_hypnat) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
175 |
apply (auto simp add: hypnat_one_def hypnat_less starprime_def |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
176 |
lemma_hypnat_P_EX lemma_hypnat_P_ALL hdvd starsetNat_def Ball_def UF_if) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
177 |
apply (rule_tac x = "%n. @y. y \<in> prime & y dvd x n" in exI, auto, ultra) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
178 |
apply (drule sym, simp (no_asm_simp)) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
179 |
prefer 2 apply ultra |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
180 |
apply (rule_tac [!] someI2_ex) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
181 |
apply (auto dest!: prime_factor_exists) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
182 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
183 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
184 |
(* behaves as expected! *) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
185 |
lemma NatStar_insert: "( *sNat* insert x A) = insert (hypnat_of_nat x) ( *sNat* A)" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
186 |
apply (auto simp add: starsetNat_def hypnat_of_nat_eq) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
187 |
apply (rule_tac [!] z = xa in eq_Abs_hypnat, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
188 |
apply (drule_tac [!] bspec asm_rl, auto, ultra+) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
189 |
done |
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 |
(* Goldblatt Exercise 3.10(1) - p. 29 *) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
192 |
lemma NatStar_hypnat_of_nat: "finite A ==> *sNat* A = hypnat_of_nat ` A" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
193 |
apply (rule_tac P = "%x. *sNat* x = hypnat_of_nat ` x" in finite_induct) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
194 |
apply (auto simp add: NatStar_insert) |
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 |
(* proved elsewhere? *) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
198 |
lemma FreeUltrafilterNat_singleton_not_mem: "{x} \<notin> FreeUltrafilterNat" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
199 |
by (auto intro!: FreeUltrafilterNat_finite) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
200 |
declare FreeUltrafilterNat_singleton_not_mem [simp] |
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 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
203 |
subsection{*Another characterization of infinite set of natural numbers*} |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
204 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
205 |
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
|
206 |
apply (erule_tac F = N in finite_induct, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
207 |
apply (rule_tac x = "Suc n + x" in exI, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
208 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
209 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
210 |
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
|
211 |
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
|
212 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
213 |
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
|
214 |
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
|
215 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
216 |
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
|
217 |
apply (rule finite_subset) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
218 |
apply (rule_tac [2] finite_atMost, auto) |
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 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
|
222 |
apply (erule_tac F = N in finite_induct, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
223 |
apply (rule_tac x = "n + x" in exI, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
224 |
done |
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 |
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
|
227 |
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
|
228 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
229 |
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
|
230 |
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
|
231 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
232 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
233 |
subsection{*An injective function cannot define an embedded natural number*} |
13957 | 234 |
|
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
235 |
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
|
236 |
==> {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
|
237 |
apply auto |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
238 |
apply (drule_tac x = x in spec, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
239 |
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
|
240 |
apply auto |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
241 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
242 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
243 |
lemma inj_fun_not_hypnat_in_SHNat: "inj f ==> Abs_hypnat(hypnatrel `` {f}) \<notin> Nats" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
244 |
apply (auto simp add: SHNat_eq hypnat_of_nat_eq) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
245 |
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
|
246 |
apply (drule_tac [2] injD) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
247 |
prefer 2 apply assumption |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
248 |
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
|
249 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
250 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
251 |
lemma range_subset_mem_starsetNat: |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
252 |
"range f <= A ==> Abs_hypnat(hypnatrel `` {f}) \<in> *sNat* A" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
253 |
apply (unfold starsetNat_def, auto, ultra) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
254 |
apply (drule_tac c = "f x" in subsetD) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
255 |
apply (rule rangeI, auto) |
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 |
(*--------------------------------------------------------------------------------*) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
259 |
(* 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
|
260 |
(* 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
|
261 |
(* 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
|
262 |
(* 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
|
263 |
(* :-)) 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
|
264 |
(* dealing with nats as we have well-ordering property *) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
265 |
(*--------------------------------------------------------------------------------*) |
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 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
|
268 |
by auto |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
269 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
270 |
lemma choicefun_mem_set: "E \<noteq> {} ==> choicefun E \<in> E" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
271 |
apply (unfold choicefun_def) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
272 |
apply (rule lemmaPow3 [THEN someI2_ex], auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
273 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
274 |
declare choicefun_mem_set [simp] |
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 |
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
|
277 |
apply (induct_tac "n", force) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
278 |
apply (simp (no_asm) add: choicefun_def) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
279 |
apply (rule lemmaPow3 [THEN someI2_ex], auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
280 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
281 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
282 |
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
|
283 |
apply (simp (no_asm) add: choicefun_def) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
284 |
apply (rule lemmaPow3 [THEN someI2_ex], 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 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
287 |
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
|
288 |
==> \<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
|
289 |
apply (rule allI) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
290 |
apply (induct_tac "n", auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
291 |
apply (simp (no_asm) add: choicefun_def) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
292 |
apply (rule lemmaPow3 [THEN someI2_ex]) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
293 |
apply (auto simp add: less_Suc_eq) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
294 |
apply (drule_tac x = m in spec) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
295 |
apply (drule subsetD, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
296 |
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
|
297 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
298 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
299 |
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
|
300 |
apply (rule inj_onI) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
301 |
apply (rule ccontr, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
302 |
apply (drule injf_max_order_preserving2) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
303 |
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
|
304 |
apply (auto dest!: spec) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
305 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
306 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
307 |
lemma infinite_set_has_order_preserving_inj: |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
308 |
"[| (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
|
309 |
==> \<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
|
310 |
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
|
311 |
apply (rule injf_max_mem_set) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
312 |
apply (rule_tac [3] inj_injf_max) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
313 |
apply (rule_tac [4] injf_max_order_preserving, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
314 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
315 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
316 |
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
|
317 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
318 |
lemma hypnat_infinite_has_nonstandard: |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
319 |
"~ finite A ==> hypnat_of_nat ` A < ( *sNat* A)" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
320 |
apply auto |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
321 |
apply (rule subsetD) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
322 |
apply (rule NatStar_hypreal_of_real_image_subset, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
323 |
apply (subgoal_tac "A \<noteq> {}") |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
324 |
prefer 2 apply force |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
325 |
apply (drule infinite_set_has_order_preserving_inj) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
326 |
apply (erule not_finite_nat_set_iff2 [THEN iffD1], auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
327 |
apply (drule inj_fun_not_hypnat_in_SHNat) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
328 |
apply (drule range_subset_mem_starsetNat) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
329 |
apply (auto simp add: SHNat_eq) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
330 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
331 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
332 |
lemma starsetNat_eq_hypnat_of_nat_image_finite: "*sNat* A = hypnat_of_nat ` A ==> finite A" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
333 |
apply (rule ccontr) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
334 |
apply (auto dest: hypnat_infinite_has_nonstandard) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
335 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
336 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
337 |
lemma finite_starsetNat_iff: "( *sNat* A = hypnat_of_nat ` A) = (finite A)" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
338 |
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
|
339 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
340 |
lemma hypnat_infinite_has_nonstandard_iff: "(~ finite A) = (hypnat_of_nat ` A < *sNat* A)" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
341 |
apply (rule iffI) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
342 |
apply (blast intro!: hypnat_infinite_has_nonstandard) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
343 |
apply (auto simp add: finite_starsetNat_iff [symmetric]) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
344 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
345 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
346 |
subsection{*Existence of Infinitely Many Primes: a Nonstandard Proof*} |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
347 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
348 |
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
|
349 |
apply auto |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
350 |
apply (rule_tac x = 2 in bexI) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
351 |
apply (auto simp add: hypnat_of_nat_eq hypnat_one_def hdvd dvd_def) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
352 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
353 |
declare lemma_not_dvd_hypnat_one [simp] |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
354 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
355 |
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
|
356 |
apply (cut_tac lemma_not_dvd_hypnat_one) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
357 |
apply (auto simp del: lemma_not_dvd_hypnat_one) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
358 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
359 |
declare lemma_not_dvd_hypnat_one2 [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 |
(* not needed here *) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
362 |
lemma hypnat_gt_zero_gt_one: |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
363 |
"[| 0 < (N::hypnat); N \<noteq> 1 |] ==> 1 < N" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
364 |
apply (unfold hypnat_zero_def hypnat_one_def) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
365 |
apply (rule_tac z = N in eq_Abs_hypnat) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
366 |
apply (auto simp add: hypnat_less, ultra) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
367 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
368 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
369 |
lemma hypnat_add_one_gt_one: |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
370 |
"0 < N ==> 1 < (N::hypnat) + 1" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
371 |
apply (unfold hypnat_zero_def hypnat_one_def) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
372 |
apply (rule_tac z = N in eq_Abs_hypnat) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
373 |
apply (auto simp add: hypnat_less hypnat_add) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
374 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
375 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
376 |
lemma zero_not_prime: "0 \<notin> prime" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
377 |
apply safe |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
378 |
apply (drule prime_g_zero, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
379 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
380 |
declare zero_not_prime [simp] |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
381 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
382 |
lemma hypnat_of_nat_zero_not_prime: "hypnat_of_nat 0 \<notin> starprime" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
383 |
by (auto intro!: bexI simp add: starprime_def starsetNat_def hypnat_of_nat_eq) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
384 |
declare hypnat_of_nat_zero_not_prime [simp] |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
385 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
386 |
lemma hypnat_zero_not_prime: |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
387 |
"0 \<notin> starprime" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
388 |
apply (unfold starprime_def starsetNat_def hypnat_zero_def) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
389 |
apply (auto intro!: bexI) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
390 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
391 |
declare hypnat_zero_not_prime [simp] |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
392 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
393 |
lemma one_not_prime: "1 \<notin> prime" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
394 |
apply safe |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
395 |
apply (drule prime_g_one, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
396 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
397 |
declare one_not_prime [simp] |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
398 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
399 |
lemma one_not_prime2: "Suc 0 \<notin> prime" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
400 |
apply safe |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
401 |
apply (drule prime_g_one, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
402 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
403 |
declare one_not_prime2 [simp] |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
404 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
405 |
lemma hypnat_of_nat_one_not_prime: "hypnat_of_nat 1 \<notin> starprime" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
406 |
by (auto intro!: bexI simp add: starprime_def starsetNat_def hypnat_of_nat_eq) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
407 |
declare hypnat_of_nat_one_not_prime [simp] |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
408 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
409 |
lemma hypnat_one_not_prime: "1 \<notin> starprime" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
410 |
apply (unfold starprime_def starsetNat_def hypnat_one_def) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
411 |
apply (auto intro!: bexI) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
412 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
413 |
declare hypnat_one_not_prime [simp] |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
414 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
415 |
lemma hdvd_diff: "[| k hdvd m; k hdvd n |] ==> k hdvd (m - n)" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
416 |
apply (rule_tac z = k in eq_Abs_hypnat) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
417 |
apply (rule_tac z = m in eq_Abs_hypnat) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
418 |
apply (rule_tac z = n in eq_Abs_hypnat) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
419 |
apply (auto simp add: hdvd hypnat_minus, ultra) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
420 |
apply (blast intro: dvd_diff) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
421 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
422 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
423 |
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
|
424 |
by (unfold dvd_def, auto) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
425 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
426 |
lemma hdvd_one_eq_one: "x hdvd 1 ==> x = 1" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
427 |
apply (unfold hypnat_one_def) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
428 |
apply (rule_tac z = x in eq_Abs_hypnat) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
429 |
apply (auto simp add: hdvd) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
430 |
done |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
431 |
|
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
432 |
theorem not_finite_prime: "~ finite prime" |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
433 |
apply (rule hypnat_infinite_has_nonstandard_iff [THEN iffD2]) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
434 |
apply (cut_tac hypnat_dvd_all_hypnat_of_nat) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
435 |
apply (erule exE) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
436 |
apply (erule conjE) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
437 |
apply (subgoal_tac "1 < N + 1") |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
438 |
prefer 2 apply (blast intro: hypnat_add_one_gt_one) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
439 |
apply (drule hyperprime_factor_exists) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
440 |
apply (auto intro: NatStar_mem) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
441 |
apply (subgoal_tac "k \<notin> hypnat_of_nat ` prime") |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
442 |
apply (force simp add: starprime_def, safe) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
443 |
apply (drule_tac x = x in bspec) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
444 |
apply (rule ccontr, simp) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
445 |
apply (drule hdvd_diff, assumption) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
446 |
apply (auto dest: hdvd_one_eq_one) |
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
14051
diff
changeset
|
447 |
done |
13957 | 448 |
|
449 |
end |