26 consts injf_max :: "nat => ('a::{order} set) => 'a" |
26 consts injf_max :: "nat => ('a::{order} set) => 'a" |
27 primrec |
27 primrec |
28 injf_max_zero: "injf_max 0 E = choicefun E" |
28 injf_max_zero: "injf_max 0 E = choicefun E" |
29 injf_max_Suc: "injf_max (Suc n) E = choicefun({e. e:E & injf_max n E < e})" |
29 injf_max_Suc: "injf_max (Suc n) E = choicefun({e. e:E & injf_max n E < e})" |
30 |
30 |
31 |
|
32 text{*A "choice" theorem for ultrafilters, like almost everywhere |
|
33 quantification*} |
|
34 |
|
35 lemma UF_choice: "{n. \<exists>m. Q n m} : FreeUltrafilterNat |
|
36 ==> \<exists>f. {n. Q n (f n)} : FreeUltrafilterNat" |
|
37 apply (rule_tac x = "%n. (@x. Q n x) " in exI) |
|
38 apply (ultra, rule someI, auto) |
|
39 done |
|
40 |
|
41 lemma UF_if: "({n. P n} : FreeUltrafilterNat --> {n. Q n} : FreeUltrafilterNat) = |
|
42 ({n. P n --> Q n} : FreeUltrafilterNat)" |
|
43 apply auto |
|
44 apply ultra+ |
|
45 done |
|
46 |
|
47 lemma UF_conj: "({n. P n} : FreeUltrafilterNat & {n. Q n} : FreeUltrafilterNat) = |
|
48 ({n. P n & Q n} : FreeUltrafilterNat)" |
|
49 apply auto |
|
50 apply ultra+ |
|
51 done |
|
52 |
|
53 lemma UF_choice_ccontr: "(\<forall>f. {n. Q n (f n)} : FreeUltrafilterNat) = |
|
54 ({n. \<forall>m. Q n m} : FreeUltrafilterNat)" |
|
55 apply auto |
|
56 prefer 2 apply ultra |
|
57 apply (rule ccontr) |
|
58 apply (rule contrapos_np) |
|
59 apply (erule_tac [2] asm_rl) |
|
60 apply (simp (no_asm) add: FreeUltrafilterNat_Compl_iff1 Collect_neg_eq [symmetric]) |
|
61 apply (rule UF_choice, ultra) |
|
62 done |
|
63 |
31 |
64 lemma dvd_by_all: "\<forall>M. \<exists>N. 0 < N & (\<forall>m. 0 < m & (m::nat) <= M --> m dvd N)" |
32 lemma dvd_by_all: "\<forall>M. \<exists>N. 0 < N & (\<forall>m. 0 < m & (m::nat) <= M --> m dvd N)" |
65 apply (rule allI) |
33 apply (rule allI) |
66 apply (induct_tac "M", auto) |
34 apply (induct_tac "M", auto) |
67 apply (rule_tac x = "N * (Suc n) " in exI) |
35 apply (rule_tac x = "N * (Suc n) " in exI) |
70 apply (force intro!: dvd_mult2) |
38 apply (force intro!: dvd_mult2) |
71 apply (force intro!: dvd_mult) |
39 apply (force intro!: dvd_mult) |
72 done |
40 done |
73 |
41 |
74 lemmas dvd_by_all2 = dvd_by_all [THEN spec, standard] |
42 lemmas dvd_by_all2 = dvd_by_all [THEN spec, standard] |
75 |
|
76 lemma lemma_hypnat_P_EX: "(\<exists>(x::hypnat). P x) = (\<exists>f. P (star_n f))" |
|
77 apply auto |
|
78 apply (rule_tac x = x in star_cases, auto) |
|
79 done |
|
80 |
|
81 lemma lemma_hypnat_P_ALL: "(\<forall>(x::hypnat). P x) = (\<forall>f. P (star_n f))" |
|
82 apply auto |
|
83 apply (rule_tac x = x in star_cases, auto) |
|
84 done |
|
85 |
|
86 lemma hdvd: |
|
87 "(star_n X hdvd star_n Y) = |
|
88 ({n. X n dvd Y n} : FreeUltrafilterNat)" |
|
89 by (simp add: hdvd_def starP2) |
|
90 |
43 |
91 lemma hypnat_of_nat_le_zero_iff: "(hypnat_of_nat n <= 0) = (n = 0)" |
44 lemma hypnat_of_nat_le_zero_iff: "(hypnat_of_nat n <= 0) = (n = 0)" |
92 by (transfer, simp) |
45 by (transfer, simp) |
93 declare hypnat_of_nat_le_zero_iff [simp] |
46 declare hypnat_of_nat_le_zero_iff [simp] |
94 |
47 |
142 "!!n. 1 < n ==> (\<exists>k \<in> starprime. k hdvd n)" |
95 "!!n. 1 < n ==> (\<exists>k \<in> starprime. k hdvd n)" |
143 by (transfer, simp add: prime_factor_exists) |
96 by (transfer, simp add: prime_factor_exists) |
144 |
97 |
145 (* Goldblatt Exercise 3.10(1) - p. 29 *) |
98 (* Goldblatt Exercise 3.10(1) - p. 29 *) |
146 lemma NatStar_hypnat_of_nat: "finite A ==> *s* A = hypnat_of_nat ` A" |
99 lemma NatStar_hypnat_of_nat: "finite A ==> *s* A = hypnat_of_nat ` A" |
147 apply (rule_tac P = "%x. *s* x = hypnat_of_nat ` x" in finite_induct) |
100 by (rule starset_finite) |
148 apply auto |
|
149 done |
|
150 |
|
151 (* proved elsewhere? *) |
|
152 lemma FreeUltrafilterNat_singleton_not_mem: "{x} \<notin> FreeUltrafilterNat" |
|
153 by (auto intro!: FreeUltrafilterNat_finite) |
|
154 declare FreeUltrafilterNat_singleton_not_mem [simp] |
|
155 |
101 |
156 |
102 |
157 subsection{*Another characterization of infinite set of natural numbers*} |
103 subsection{*Another characterization of infinite set of natural numbers*} |
158 |
104 |
159 lemma finite_nat_set_bounded: "finite N ==> \<exists>n. (\<forall>i \<in> N. i<(n::nat))" |
105 lemma finite_nat_set_bounded: "finite N ==> \<exists>n. (\<forall>i \<in> N. i<(n::nat))" |
192 apply (drule_tac x = x in spec, auto) |
138 apply (drule_tac x = x in spec, auto) |
193 apply (subgoal_tac "\<forall>n. (f n = f x) = (x = n) ") |
139 apply (subgoal_tac "\<forall>n. (f n = f x) = (x = n) ") |
194 apply auto |
140 apply auto |
195 done |
141 done |
196 |
142 |
197 lemma inj_fun_not_hypnat_in_SHNat: "inj (f::nat=>nat) ==> star_n f \<notin> Nats" |
143 lemma inj_fun_not_hypnat_in_SHNat: |
198 apply (auto simp add: SHNat_eq hypnat_of_nat_eq star_n_eq_iff) |
144 assumes inj_f: "inj (f::nat=>nat)" |
199 apply (subgoal_tac "\<forall>m n. m \<noteq> n --> f n \<noteq> f m", auto) |
145 shows "starfun f whn \<notin> Nats" |
200 apply (drule_tac [2] injD) |
146 proof |
201 prefer 2 apply assumption |
147 from inj_f have inj_f': "inj (starfun f)" |
202 apply (drule_tac N = N in lemma_infinite_set_singleton, auto) |
148 by (transfer inj_on_def Ball_def UNIV_def) |
203 done |
149 assume "starfun f whn \<in> Nats" |
|
150 then obtain N where N: "starfun f whn = hypnat_of_nat N" |
|
151 by (auto simp add: Nats_def) |
|
152 hence "\<exists>n. starfun f n = hypnat_of_nat N" .. |
|
153 hence "\<exists>n. f n = N" by transfer |
|
154 then obtain n where n: "f n = N" .. |
|
155 hence "starfun f (hypnat_of_nat n) = hypnat_of_nat N" |
|
156 by transfer |
|
157 with N have "starfun f whn = starfun f (hypnat_of_nat n)" |
|
158 by simp |
|
159 with inj_f' have "whn = hypnat_of_nat n" |
|
160 by (rule injD) |
|
161 thus "False" |
|
162 by (simp add: whn_neq_hypnat_of_nat) |
|
163 qed |
204 |
164 |
205 lemma range_subset_mem_starsetNat: |
165 lemma range_subset_mem_starsetNat: |
206 "range f <= A ==> star_n f \<in> *s* A" |
166 "range f <= A ==> starfun f whn \<in> *s* A" |
207 apply (simp add: starset_def star_of_def Iset_star_n) |
167 apply (rule_tac x="whn" in spec) |
208 apply (subgoal_tac "\<forall>n. f n \<in> A", auto) |
168 apply (transfer, auto) |
209 done |
169 done |
210 |
170 |
211 (*--------------------------------------------------------------------------------*) |
171 (*--------------------------------------------------------------------------------*) |
212 (* Gleason Proposition 11-5.5. pg 149, pg 155 (ex. 3) and pg. 360 *) |
172 (* Gleason Proposition 11-5.5. pg 149, pg 155 (ex. 3) and pg. 360 *) |
213 (* Let E be a nonvoid ordered set with no maximal elements (note: effectively an *) |
173 (* Let E be a nonvoid ordered set with no maximal elements (note: effectively an *) |