src/HOL/Complex/ex/NSPrimes.ML
author paulson
Thu Jul 01 12:29:53 2004 +0200 (2004-07-01)
changeset 15013 34264f5e4691
parent 14378 69c4d5997669
permissions -rw-r--r--
new treatment of binary numerals
paulson@13957
     1
(*  Title       : NSPrimes.ML
paulson@13957
     2
    Author      : Jacques D. Fleuriot
paulson@13957
     3
    Copyright   : 2002 University of Edinburgh
paulson@13957
     4
    Description : The nonstandard primes as an extension of 
paulson@13957
     5
                  the prime numbers
paulson@13957
     6
*)
paulson@13957
     7
paulson@13957
     8
(*--------------------------------------------------------------*) 
paulson@13957
     9
(* A "choice" theorem for ultrafilters cf. almost everywhere    *)
paulson@13957
    10
(* quantification                                               *)
paulson@13957
    11
(*--------------------------------------------------------------*) 
paulson@13957
    12
    
paulson@13957
    13
Goal "{n. EX m. Q n m} : FreeUltrafilterNat \
paulson@13957
    14
\     ==> EX f. {n. Q n (f n)} : FreeUltrafilterNat";
paulson@13957
    15
by (res_inst_tac [("x","%n. (@x. Q n x)")] exI 1);
paulson@13957
    16
by (Ultra_tac 1 THEN rtac someI 1 THEN Auto_tac);
paulson@13957
    17
qed "UF_choice";
paulson@13957
    18
paulson@13957
    19
Goal "({n. P n} : FreeUltrafilterNat --> {n. Q n} : FreeUltrafilterNat) = \
paulson@13957
    20
\     ({n. P n --> Q n} : FreeUltrafilterNat)";
paulson@13957
    21
by Auto_tac;
paulson@13957
    22
by (ALLGOALS(Ultra_tac));
paulson@13957
    23
qed "UF_if";
paulson@13957
    24
paulson@13957
    25
Goal "({n. P n} : FreeUltrafilterNat & {n. Q n} : FreeUltrafilterNat) = \
paulson@13957
    26
\     ({n. P n & Q n} : FreeUltrafilterNat)";
paulson@13957
    27
by Auto_tac;
paulson@13957
    28
by (ALLGOALS(Ultra_tac));
paulson@13957
    29
qed "UF_conj";
paulson@13957
    30
paulson@13957
    31
Goal "(ALL f. {n. Q n (f n)} : FreeUltrafilterNat) = \
paulson@13957
    32
\     ({n. ALL m. Q n m} : FreeUltrafilterNat)";
paulson@13957
    33
by Auto_tac;
paulson@13957
    34
by (Ultra_tac 2);
paulson@13957
    35
by (rtac ccontr 1);
paulson@13957
    36
by (rtac swap 1 THEN assume_tac 2);
paulson@13957
    37
by (simp_tac (simpset() addsimps [FreeUltrafilterNat_Compl_iff1,
paulson@13957
    38
    CLAIM "-{n. Q n} = {n. ~ Q n}"]) 1);
paulson@13957
    39
by (rtac UF_choice 1);
paulson@13957
    40
by (Ultra_tac 1 THEN Auto_tac);
paulson@13957
    41
qed "UF_choice_ccontr";
paulson@13957
    42
paulson@13957
    43
Goal "ALL M. EX N. 0 < N & (ALL m. 0 < m & (m::nat) <= M --> m dvd N)";
paulson@13957
    44
by (rtac allI 1);
paulson@13957
    45
by (induct_tac "M" 1);
paulson@13957
    46
by Auto_tac;
paulson@13957
    47
by (res_inst_tac [("x","N * (Suc n)")] exI 1);
paulson@13957
    48
by (Step_tac 1 THEN Force_tac 1);
paulson@13957
    49
by (dtac le_imp_less_or_eq 1 THEN etac disjE 1);
paulson@13957
    50
by (force_tac (claset() addSIs [dvd_mult2],simpset()) 1);
paulson@13957
    51
by (force_tac (claset() addSIs [dvd_mult],simpset()) 1);
paulson@13957
    52
qed "dvd_by_all";
paulson@13957
    53
paulson@13957
    54
bind_thm ("dvd_by_all2",dvd_by_all RS spec);
paulson@13957
    55
paulson@13957
    56
Goal "(EX (x::hypnat). P x) = (EX f. P (Abs_hypnat(hypnatrel `` {f})))";
paulson@13957
    57
by Auto_tac;
paulson@13957
    58
by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
paulson@13957
    59
by Auto_tac;
paulson@13957
    60
qed "lemma_hypnat_P_EX";
paulson@13957
    61
paulson@13957
    62
Goal "(ALL (x::hypnat). P x) = (ALL f. P (Abs_hypnat(hypnatrel `` {f})))";
paulson@13957
    63
by Auto_tac;
paulson@13957
    64
by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
paulson@13957
    65
by Auto_tac;
paulson@13957
    66
qed "lemma_hypnat_P_ALL";
paulson@13957
    67
paulson@13957
    68
Goalw [hdvd_def]
paulson@13957
    69
      "(Abs_hypnat(hypnatrel``{%n. X n}) hdvd \
paulson@13957
    70
\           Abs_hypnat(hypnatrel``{%n. Y n})) = \
paulson@13957
    71
\      ({n. X n dvd Y n} : FreeUltrafilterNat)";
paulson@13957
    72
by (Auto_tac THEN Ultra_tac 1);
paulson@13957
    73
qed "hdvd";
paulson@13957
    74
paulson@13957
    75
Goal "(hypnat_of_nat n <= 0) = (n = 0)";
paulson@13957
    76
by (stac (hypnat_of_nat_zero RS sym) 1);
paulson@14371
    77
by Auto_tac;
paulson@13957
    78
qed "hypnat_of_nat_le_zero_iff";
paulson@13957
    79
Addsimps [hypnat_of_nat_le_zero_iff];
paulson@13957
    80
paulson@13957
    81
paulson@13957
    82
(* Goldblatt: Exercise 5.11(2) - p. 57 *)
paulson@13957
    83
Goal "ALL M. EX N. 0 < N & (ALL m. 0 < m & (m::hypnat) <= M --> m hdvd N)";
paulson@13957
    84
by (Step_tac 1);
paulson@13957
    85
by (res_inst_tac [("z","M")] eq_Abs_hypnat 1);
paulson@13957
    86
by (auto_tac (claset(),simpset() addsimps [lemma_hypnat_P_EX,
paulson@13957
    87
    lemma_hypnat_P_ALL,hypnat_zero_def,hypnat_le,hypnat_less,hdvd]));
paulson@13957
    88
by (cut_facts_tac [dvd_by_all] 1);
paulson@13957
    89
by (dtac (CLAIM "(ALL (M::nat). EX N. 0 < N & (ALL m. 0 < m & m <= M \
paulson@13957
    90
\                               --> m dvd N)) \
paulson@13957
    91
\                ==> ALL (n::nat). EX N. 0 < N & (ALL m. 0 < (m::nat) & m <= (x n) \
paulson@13957
    92
\                                  --> m dvd N)") 1);
paulson@13957
    93
by (dtac choice 1);
paulson@13957
    94
by (Step_tac 1);
paulson@13957
    95
by (res_inst_tac [("x","f")] exI 1);
paulson@13957
    96
by Auto_tac;
paulson@13957
    97
by (ALLGOALS(Ultra_tac));
paulson@13957
    98
by Auto_tac;
paulson@13957
    99
qed "hdvd_by_all";
paulson@13957
   100
paulson@13957
   101
bind_thm ("hdvd_by_all2",hdvd_by_all RS spec);
paulson@13957
   102
paulson@13957
   103
(* Goldblatt: Exercise 5.11(2) - p. 57 *)
paulson@13957
   104
Goal "EX (N::hypnat). 0 < N & (ALL n : - {0::nat}. hypnat_of_nat(n) hdvd N)"; 
paulson@13957
   105
by (cut_facts_tac [hdvd_by_all] 1);
paulson@13957
   106
by (dres_inst_tac [("x","whn")] spec 1);
paulson@13957
   107
by Auto_tac;
paulson@13957
   108
by (rtac exI 1 THEN Auto_tac);
paulson@13957
   109
by (dres_inst_tac [("x","hypnat_of_nat n")] spec 1);
paulson@14371
   110
by (auto_tac (claset(),
paulson@14371
   111
     simpset() addsimps [linorder_not_less, hypnat_of_nat_zero_iff]));
paulson@13957
   112
qed "hypnat_dvd_all_hypnat_of_nat";
paulson@13957
   113
paulson@13957
   114
paulson@13957
   115
(*--------------------------------------------------------------*)
paulson@13957
   116
(* the nonstandard extension of the set prime numbers consists  *)
paulson@13957
   117
(* of precisely those hypernaturals > 1 that have no nontrivial *)
paulson@13957
   118
(* factors                                                      *)
paulson@13957
   119
(*--------------------------------------------------------------*) 
paulson@13957
   120
paulson@13957
   121
(* Goldblatt: Exercise 5.11(3a) - p 57  *)
paulson@13957
   122
Goalw [starprime_def,thm "prime_def"]
paulson@13957
   123
  "starprime = {p. 1 < p & (ALL m. m hdvd p --> m = 1 | m = p)}";
paulson@13957
   124
by (auto_tac (claset(),simpset() addsimps 
paulson@13957
   125
    [CLAIM "{p. Q(p) & R(p)} = {p. Q(p)} Int {p. R(p)}",NatStar_Int]));
paulson@13957
   126
by (ALLGOALS(res_inst_tac [("z","x")] eq_Abs_hypnat));
paulson@13957
   127
by (res_inst_tac [("z","m")] eq_Abs_hypnat 2);
paulson@13957
   128
by (auto_tac (claset(),simpset() addsimps [hdvd,hypnat_one_def,hypnat_less,
paulson@13957
   129
    lemma_hypnat_P_ALL,starsetNat_def]));
paulson@13957
   130
by (dtac bspec 1 THEN dtac bspec 2 THEN Auto_tac);
paulson@13957
   131
by (Ultra_tac 1 THEN Ultra_tac 1); 
paulson@13957
   132
by (rtac ccontr 1);
paulson@13957
   133
by (dtac FreeUltrafilterNat_Compl_mem 1);
paulson@13957
   134
by (auto_tac (claset(),simpset() addsimps [CLAIM "- {p. Q p} = {p. ~ Q p}"]));
paulson@13957
   135
by (dtac UF_choice 1 THEN Auto_tac);
paulson@13957
   136
by (dres_inst_tac [("x","f")] spec 1 THEN Auto_tac);
paulson@13957
   137
by (ALLGOALS(Ultra_tac));
paulson@13957
   138
qed "starprime";
paulson@13957
   139
paulson@13957
   140
Goalw [thm "prime_def"] "2 : prime";
paulson@13957
   141
by Auto_tac;
paulson@13957
   142
by (ftac dvd_imp_le 1);
paulson@13957
   143
by (auto_tac (claset() addDs [dvd_0_left],simpset() addsimps 
paulson@13957
   144
    [ARITH_PROVE "(m <= (2::nat)) = (m = 0 | m = 1 | m = 2)"]));
paulson@13957
   145
qed "prime_two";
paulson@13957
   146
Addsimps [prime_two];
paulson@13957
   147
paulson@13957
   148
(* proof uses course-of-value induction *)
paulson@13957
   149
Goal "Suc 0 < n --> (EX k : prime. k dvd n)";
paulson@13957
   150
by (res_inst_tac [("n","n")] nat_less_induct 1);
paulson@13957
   151
by Auto_tac;
paulson@13957
   152
by (case_tac "n : prime" 1);
paulson@13957
   153
by (res_inst_tac [("x","n")] bexI 1 THEN Auto_tac);
paulson@13957
   154
by (dtac (conjI RS (thm "not_prime_ex_mk")) 1 THEN Auto_tac);
paulson@13957
   155
by (dres_inst_tac [("x","m")] spec 1 THEN Auto_tac);
paulson@13957
   156
by (res_inst_tac [("x","ka")] bexI 1);
paulson@13957
   157
by (auto_tac (claset() addIs [dvd_mult2],simpset()));
paulson@13957
   158
qed_spec_mp "prime_factor_exists";
paulson@13957
   159
paulson@13957
   160
(* Goldblatt Exercise 5.11(3b) - p 57  *)
paulson@13957
   161
Goal "1 < n ==> (EX k : starprime. k hdvd n)";
paulson@13957
   162
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
paulson@13957
   163
by (auto_tac (claset(),simpset() addsimps [hypnat_one_def,
paulson@13957
   164
    hypnat_less,starprime_def,lemma_hypnat_P_EX,lemma_hypnat_P_ALL,
paulson@13957
   165
    hdvd,starsetNat_def,CLAIM "(ALL X: S. P X) = (ALL X. X : S --> P X)",
paulson@13957
   166
    UF_if]));
paulson@13957
   167
by (res_inst_tac [("x","%n. @y. y : prime & y dvd x n")] exI 1);
paulson@13957
   168
by Auto_tac;
paulson@13957
   169
by (ALLGOALS (Ultra_tac));
paulson@13957
   170
by (dtac sym 1 THEN Asm_simp_tac 1);
paulson@13957
   171
by (ALLGOALS(rtac someI2_ex));
paulson@13957
   172
by (auto_tac (claset() addSDs [prime_factor_exists],simpset()));
paulson@13957
   173
qed_spec_mp "hyperprime_factor_exists";
paulson@13957
   174
paulson@13957
   175
(* behaves as expected! *)
paulson@13957
   176
Goal "( *sNat* insert x A) = insert (hypnat_of_nat x) ( *sNat* A)";
paulson@13957
   177
by (auto_tac (claset(),simpset() addsimps [starsetNat_def,
paulson@14378
   178
    hypnat_of_nat_eq]));
paulson@13957
   179
by (ALLGOALS(res_inst_tac [("z","xa")] eq_Abs_hypnat));
paulson@13957
   180
by Auto_tac;
paulson@13957
   181
by (TRYALL(dtac bspec));
paulson@13957
   182
by Auto_tac;
paulson@13957
   183
by (ALLGOALS(Ultra_tac));
paulson@13957
   184
qed "NatStar_insert";
paulson@13957
   185
paulson@13957
   186
(* Goldblatt Exercise 3.10(1) - p. 29 *)
paulson@13957
   187
Goal "finite A ==> *sNat* A = hypnat_of_nat ` A";
paulson@13957
   188
by (res_inst_tac [("P","%x. *sNat* x = hypnat_of_nat ` x")] finite_induct 1);
paulson@13957
   189
by (auto_tac (claset(),simpset() addsimps [NatStar_insert]));
paulson@13957
   190
qed "NatStar_hypnat_of_nat";
paulson@13957
   191
paulson@13957
   192
(* proved elsewhere? *)
paulson@13957
   193
Goal "{x} ~: FreeUltrafilterNat";
paulson@13957
   194
by (auto_tac (claset() addSIs [FreeUltrafilterNat_finite],simpset()));
paulson@13957
   195
qed "FreeUltrafilterNat_singleton_not_mem";
paulson@13957
   196
Addsimps [FreeUltrafilterNat_singleton_not_mem];
paulson@13957
   197
paulson@13957
   198
(*-------------------------------------------------------------------------------*)
paulson@13957
   199
(* Another characterization of infinite set of natural numbers                   *)
paulson@13957
   200
(*-------------------------------------------------------------------------------*)
paulson@13957
   201
paulson@13957
   202
Goal "finite N ==> EX n. (ALL i:N. i<(n::nat))";
paulson@13957
   203
by (eres_inst_tac [("F","N")] finite_induct 1);
paulson@13957
   204
by Auto_tac;
paulson@13957
   205
by (res_inst_tac [("x","Suc n + x")] exI 1);
paulson@13957
   206
by Auto_tac;
paulson@13957
   207
qed "finite_nat_set_bounded";
paulson@13957
   208
paulson@13957
   209
Goal "finite N = (EX n. (ALL i:N. i<(n::nat)))";
paulson@13957
   210
by (blast_tac (claset() addIs [finite_nat_set_bounded,
paulson@13957
   211
    bounded_nat_set_is_finite]) 1);
paulson@13957
   212
qed "finite_nat_set_bounded_iff";
paulson@13957
   213
paulson@13957
   214
Goal "(~ finite N) = (ALL n. EX i:N. n <= (i::nat))";
paulson@13957
   215
by (auto_tac (claset(),simpset() addsimps [finite_nat_set_bounded_iff,
paulson@13957
   216
    le_def]));
paulson@13957
   217
qed "not_finite_nat_set_iff";
paulson@13957
   218
paulson@13957
   219
Goal "(ALL i:N. i<=(n::nat)) ==> finite N";
paulson@13957
   220
by (rtac finite_subset 1);
paulson@13957
   221
 by (rtac finite_atMost 2);
paulson@13957
   222
by Auto_tac;
paulson@13957
   223
qed "bounded_nat_set_is_finite2";
paulson@13957
   224
paulson@13957
   225
Goal "finite N ==> EX n. (ALL i:N. i<=(n::nat))";
paulson@13957
   226
by (eres_inst_tac [("F","N")] finite_induct 1);
paulson@13957
   227
by Auto_tac;
paulson@13957
   228
by (res_inst_tac [("x","n + x")] exI 1);
paulson@13957
   229
by Auto_tac;
paulson@13957
   230
qed "finite_nat_set_bounded2";
paulson@13957
   231
paulson@13957
   232
Goal "finite N = (EX n. (ALL i:N. i<=(n::nat)))";
paulson@13957
   233
by (blast_tac (claset() addIs [finite_nat_set_bounded2,
paulson@13957
   234
    bounded_nat_set_is_finite2]) 1);
paulson@13957
   235
qed "finite_nat_set_bounded_iff2";
paulson@13957
   236
paulson@13957
   237
Goal "(~ finite N) = (ALL n. EX i:N. n < (i::nat))";
paulson@13957
   238
by (auto_tac (claset(),simpset() addsimps [finite_nat_set_bounded_iff2,
paulson@13957
   239
    le_def]));
paulson@13957
   240
qed "not_finite_nat_set_iff2";
paulson@13957
   241
paulson@13957
   242
(*-------------------------------------------------------------------------------*)
paulson@13957
   243
(* An injective function cannot define an embedded natural number                *)
paulson@13957
   244
(*-------------------------------------------------------------------------------*)
paulson@13957
   245
paulson@13957
   246
Goal "ALL m n. m ~= n --> f n ~= f m \
paulson@13957
   247
\     ==>  {n. f n = N} = {} |  (EX m. {n. f n = N} = {m})";
paulson@13957
   248
by Auto_tac;
paulson@13957
   249
by (dres_inst_tac [("x","x")] spec 1 THEN Auto_tac); 
paulson@13957
   250
by (subgoal_tac "ALL n. (f n = f x) = (x = n)" 1);
paulson@13957
   251
by Auto_tac;
paulson@13957
   252
qed "lemma_infinite_set_singleton";
paulson@13957
   253
paulson@14378
   254
Goal "inj f ==> Abs_hypnat(hypnatrel `` {f}) ~: Nats";
paulson@14378
   255
by (auto_tac (claset(), simpset() addsimps [SHNat_eq,hypnat_of_nat_eq])); 
paulson@13957
   256
by (subgoal_tac "ALL m n. m ~= n --> f n ~= f m" 1);
paulson@13957
   257
by Auto_tac;
paulson@13957
   258
by (dtac injD 2);
paulson@13957
   259
by (assume_tac 2 THEN Force_tac 2);
paulson@13957
   260
by (dres_inst_tac[("N","N")] lemma_infinite_set_singleton 1);
paulson@13957
   261
by Auto_tac;
paulson@13957
   262
qed "inj_fun_not_hypnat_in_SHNat";
paulson@13957
   263
paulson@13957
   264
Goalw [starsetNat_def] 
paulson@13957
   265
   "range f <= A ==> Abs_hypnat(hypnatrel `` {f}) : *sNat* A";
paulson@13957
   266
by Auto_tac;
paulson@13957
   267
by (Ultra_tac 1);
paulson@13957
   268
by (dres_inst_tac [("c","f x")] subsetD 1);
paulson@13957
   269
by (rtac rangeI 1);
paulson@13957
   270
by Auto_tac;
paulson@13957
   271
qed "range_subset_mem_starsetNat";
paulson@13957
   272
paulson@13957
   273
(*--------------------------------------------------------------------------------*)
paulson@13957
   274
(* Gleason Proposition 11-5.5. pg 149, pg 155 (ex. 3) and pg. 360                 *)
paulson@13957
   275
(* Let E be a nonvoid ordered set with no maximal elements (note: effectively an  *) 
paulson@13957
   276
(* infinite set if we take E = N (Nats)). Then there exists an order-preserving   *) 
paulson@13957
   277
(* injection from N to E. Of course, (as some doofus will undoubtedly point out!  *)
paulson@13957
   278
(* :-)) can use notion of least element in proof (i.e. no need for choice) if     *)
paulson@13957
   279
(* dealing with nats as we have well-ordering property                            *) 
paulson@13957
   280
(*--------------------------------------------------------------------------------*)
paulson@13957
   281
paulson@13957
   282
Goal "E ~= {} ==> EX x. EX X : (Pow E - {{}}). x: X";
paulson@13957
   283
by Auto_tac;
paulson@13957
   284
val lemmaPow3 = result();
paulson@13957
   285
paulson@13957
   286
Goalw [choicefun_def] "E ~= {} ==> choicefun E : E";
paulson@13957
   287
by (rtac (lemmaPow3 RS someI2_ex) 1);
paulson@13957
   288
by Auto_tac;
paulson@13957
   289
qed "choicefun_mem_set";
paulson@13957
   290
Addsimps [choicefun_mem_set];
paulson@13957
   291
paulson@13957
   292
Goal "[| E ~={}; ALL x. EX y: E. x < y |] ==> injf_max n E : E";
paulson@13957
   293
by (induct_tac "n" 1);
paulson@13957
   294
by (Force_tac 1);
paulson@13957
   295
by (simp_tac (simpset() addsimps [choicefun_def]) 1);
paulson@13957
   296
by (rtac (lemmaPow3 RS someI2_ex) 1);
paulson@13957
   297
by Auto_tac;
paulson@13957
   298
qed "injf_max_mem_set";
paulson@13957
   299
paulson@13957
   300
Goal "ALL x. EX y: E. x < y ==> injf_max n E < injf_max (Suc n) E";
paulson@13957
   301
by (simp_tac (simpset() addsimps [choicefun_def]) 1);
paulson@13957
   302
by (rtac (lemmaPow3 RS someI2_ex) 1);
paulson@13957
   303
by Auto_tac;
paulson@13957
   304
qed "injf_max_order_preserving";
paulson@13957
   305
paulson@13957
   306
Goal "ALL x. EX y: E. x < y \
paulson@13957
   307
\     ==> ALL n m. m < n --> injf_max m E < injf_max n E";
paulson@13957
   308
by (rtac allI 1);
paulson@13957
   309
by (induct_tac "n" 1);
paulson@13957
   310
by Auto_tac;
paulson@13957
   311
by (simp_tac (simpset() addsimps [choicefun_def]) 1);
paulson@13957
   312
by (rtac (lemmaPow3 RS someI2_ex) 1);
paulson@13957
   313
by Auto_tac;
paulson@13957
   314
by (dtac (CLAIM "m < Suc n ==> m = n | m < n") 1);
paulson@13957
   315
by Auto_tac;
paulson@13957
   316
by (dres_inst_tac [("x","m")] spec 1);
paulson@13957
   317
by Auto_tac;
paulson@13957
   318
by (dtac subsetD 1 THEN Auto_tac);
paulson@13957
   319
by (dres_inst_tac [("x","injf_max m E")] order_less_trans 1);
paulson@13957
   320
by Auto_tac;
paulson@13957
   321
qed "injf_max_order_preserving2";
paulson@13957
   322
paulson@13957
   323
Goal "ALL x. EX y: E. x < y ==> inj (%n. injf_max n E)";
paulson@13957
   324
by (rtac injI 1);
paulson@13957
   325
by (rtac ccontr 1);
paulson@13957
   326
by Auto_tac;
paulson@13957
   327
by (dtac injf_max_order_preserving2 1);
paulson@13957
   328
by (cut_inst_tac [("m","x"),("n","y")] less_linear 1);
paulson@13957
   329
by Auto_tac;
paulson@13957
   330
by (auto_tac (claset() addSDs [spec],simpset()));
paulson@13957
   331
qed "inj_injf_max";
paulson@13957
   332
paulson@13957
   333
Goal "[| (E::('a::{order} set)) ~= {}; ALL x. EX y: E. x < y |] \
paulson@13957
   334
\     ==> EX f. range f <= E & inj (f::nat => 'a) & (ALL m. f m < f(Suc m))";
paulson@13957
   335
by (res_inst_tac [("x","%n. injf_max n E")] exI 1);
paulson@13957
   336
by (Step_tac 1);
paulson@13957
   337
by (rtac injf_max_mem_set 1);
paulson@13957
   338
by (rtac inj_injf_max 3);
paulson@13957
   339
by (rtac injf_max_order_preserving 4);
paulson@13957
   340
by Auto_tac;
paulson@13957
   341
qed "infinite_set_has_order_preserving_inj";
paulson@13957
   342
paulson@13957
   343
(*-------------------------------------------------------------------------------*)
paulson@13957
   344
(* Only need fact that we can have an injective function from N to A for proof   *)
paulson@13957
   345
(*-------------------------------------------------------------------------------*)
paulson@13957
   346
paulson@13957
   347
Goal "~ finite A ==> hypnat_of_nat ` A < ( *sNat* A)";
paulson@13957
   348
by Auto_tac;
paulson@13957
   349
by (rtac subsetD 1);
paulson@13957
   350
by (rtac NatStar_hypreal_of_real_image_subset 1);
paulson@13957
   351
by Auto_tac;
paulson@13957
   352
by (subgoal_tac "A ~= {}" 1);
paulson@13957
   353
by (Force_tac 2);
paulson@13957
   354
by (dtac infinite_set_has_order_preserving_inj 1);
paulson@13957
   355
by (etac (not_finite_nat_set_iff2 RS iffD1) 1);
paulson@13957
   356
by Auto_tac;
paulson@13957
   357
by (dtac inj_fun_not_hypnat_in_SHNat 1);
paulson@13957
   358
by (dtac range_subset_mem_starsetNat 1);
paulson@14378
   359
by (auto_tac (claset(),simpset() addsimps [SHNat_eq]));
paulson@13957
   360
qed "hypnat_infinite_has_nonstandard";
paulson@13957
   361
paulson@13957
   362
Goal "*sNat* A =  hypnat_of_nat ` A ==> finite A";
paulson@13957
   363
by (rtac ccontr 1);
paulson@13957
   364
by (auto_tac (claset() addDs [hypnat_infinite_has_nonstandard],
paulson@13957
   365
    simpset()));
paulson@13957
   366
qed "starsetNat_eq_hypnat_of_nat_image_finite";
paulson@13957
   367
paulson@13957
   368
Goal "( *sNat* A = hypnat_of_nat ` A) = (finite A)";
paulson@13957
   369
by (blast_tac (claset() addSIs [starsetNat_eq_hypnat_of_nat_image_finite,
paulson@13957
   370
    NatStar_hypnat_of_nat]) 1);
paulson@13957
   371
qed "finite_starsetNat_iff";
paulson@13957
   372
paulson@13957
   373
Goal "(~ finite A) = (hypnat_of_nat ` A < *sNat* A)";
paulson@13957
   374
by (rtac iffI 1);
paulson@13957
   375
by (blast_tac (claset() addSIs [hypnat_infinite_has_nonstandard]) 1);
paulson@13957
   376
by (auto_tac (claset(),simpset() addsimps [finite_starsetNat_iff RS sym]));
paulson@13957
   377
qed "hypnat_infinite_has_nonstandard_iff";
paulson@13957
   378
paulson@13957
   379
paulson@13957
   380
(*-------------------------------------------------------------------------------*)
paulson@13957
   381
(* Existence of infinitely many primes: a nonstandard proof                      *)
paulson@13957
   382
(*-------------------------------------------------------------------------------*)
paulson@13957
   383
paulson@13957
   384
Goal "~ (ALL n:- {0}. hypnat_of_nat n hdvd 1)";
paulson@13957
   385
by Auto_tac;
paulson@13957
   386
by (res_inst_tac [("x","2")] bexI 1);
paulson@14378
   387
by (auto_tac (claset(),simpset() addsimps [hypnat_of_nat_eq,
paulson@13957
   388
    hypnat_one_def,hdvd,dvd_def]));
paulson@13957
   389
val lemma_not_dvd_hypnat_one = result();
paulson@13957
   390
Addsimps [lemma_not_dvd_hypnat_one];
paulson@13957
   391
paulson@13957
   392
Goal "EX n:- {0}. ~ hypnat_of_nat n hdvd 1";
paulson@13957
   393
by (cut_facts_tac [lemma_not_dvd_hypnat_one] 1);
paulson@13957
   394
by (auto_tac (claset(),simpset() delsimps [lemma_not_dvd_hypnat_one]));
paulson@13957
   395
val lemma_not_dvd_hypnat_one2 = result();
paulson@13957
   396
Addsimps [lemma_not_dvd_hypnat_one2];
paulson@13957
   397
paulson@13957
   398
(* not needed here *)
paulson@13957
   399
Goalw [hypnat_zero_def,hypnat_one_def] 
paulson@13957
   400
  "[| 0 < (N::hypnat); N ~= 1 |] ==> 1 < N";
paulson@13957
   401
by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
paulson@13957
   402
by (auto_tac (claset(),simpset() addsimps [hypnat_less]));
paulson@13957
   403
by (Ultra_tac 1);
paulson@13957
   404
qed "hypnat_gt_zero_gt_one";
paulson@13957
   405
paulson@13957
   406
Goalw [hypnat_zero_def,hypnat_one_def]
paulson@13957
   407
    "0 < N ==> 1 < (N::hypnat) + 1";
paulson@13957
   408
by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
paulson@13957
   409
by (auto_tac (claset(),simpset() addsimps [hypnat_less,hypnat_add]));
paulson@13957
   410
qed "hypnat_add_one_gt_one";
paulson@13957
   411
paulson@13957
   412
Goal "0 ~: prime";
paulson@13957
   413
by (Step_tac 1);
paulson@13957
   414
by (dtac (thm "prime_g_zero") 1);
paulson@13957
   415
by Auto_tac;
paulson@13957
   416
qed "zero_not_prime";
paulson@13957
   417
Addsimps [zero_not_prime];
paulson@13957
   418
paulson@14378
   419
Goal "hypnat_of_nat 0 ~: starprime";
paulson@14378
   420
by (auto_tac (claset() addSIs [bexI],
paulson@14378
   421
      simpset() addsimps [starprime_def,starsetNat_def,hypnat_of_nat_eq]));
paulson@13957
   422
qed "hypnat_of_nat_zero_not_prime";
paulson@13957
   423
Addsimps [hypnat_of_nat_zero_not_prime];
paulson@13957
   424
paulson@13957
   425
Goalw [starprime_def,starsetNat_def,hypnat_zero_def]
paulson@13957
   426
   "0 ~: starprime";
paulson@13957
   427
by (auto_tac (claset() addSIs [bexI],simpset()));
paulson@13957
   428
qed "hypnat_zero_not_prime";
paulson@13957
   429
Addsimps [hypnat_zero_not_prime];
paulson@13957
   430
paulson@13957
   431
Goal "1 ~: prime";
paulson@13957
   432
by (Step_tac 1);
paulson@13957
   433
by (dtac (thm "prime_g_one") 1);
paulson@13957
   434
by Auto_tac;
paulson@13957
   435
qed "one_not_prime";
paulson@13957
   436
Addsimps [one_not_prime];
paulson@13957
   437
paulson@13957
   438
Goal "Suc 0 ~: prime";
paulson@13957
   439
by (Step_tac 1);
paulson@13957
   440
by (dtac (thm "prime_g_one") 1);
paulson@13957
   441
by Auto_tac;
paulson@13957
   442
qed "one_not_prime2";
paulson@13957
   443
Addsimps [one_not_prime2];
paulson@13957
   444
paulson@14378
   445
Goal "hypnat_of_nat 1 ~: starprime";
paulson@14378
   446
by (auto_tac (claset() addSIs [bexI],
paulson@14378
   447
     simpset() addsimps [starprime_def,starsetNat_def,hypnat_of_nat_eq]));
paulson@13957
   448
qed "hypnat_of_nat_one_not_prime";
paulson@13957
   449
Addsimps [hypnat_of_nat_one_not_prime];
paulson@13957
   450
paulson@13957
   451
Goalw [starprime_def,starsetNat_def,hypnat_one_def]
paulson@13957
   452
   "1 ~: starprime";
paulson@13957
   453
by (auto_tac (claset() addSIs [bexI],simpset()));
paulson@13957
   454
qed "hypnat_one_not_prime";
paulson@13957
   455
Addsimps [hypnat_one_not_prime];
paulson@13957
   456
paulson@13957
   457
Goal "[| k hdvd m; k hdvd n |] ==> k hdvd (m - n)";
paulson@13957
   458
by (res_inst_tac [("z","k")] eq_Abs_hypnat 1);
paulson@13957
   459
by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
paulson@13957
   460
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
paulson@13957
   461
by (auto_tac (claset(),simpset() addsimps [hdvd,hypnat_minus]));
paulson@13957
   462
by (Ultra_tac 1);
paulson@13957
   463
by (blast_tac (claset() addIs [dvd_diff]) 1);
paulson@13957
   464
qed "hdvd_diff";
paulson@13957
   465
paulson@13957
   466
Goalw [dvd_def] "x dvd (1::nat) ==> x = 1";
paulson@13957
   467
by Auto_tac;
paulson@13957
   468
qed "dvd_one_eq_one";
paulson@13957
   469
paulson@13957
   470
Goalw [hypnat_one_def] "x hdvd 1 ==> x = 1";
paulson@13957
   471
by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
paulson@13957
   472
by (auto_tac (claset(),simpset() addsimps [hdvd]));
paulson@13957
   473
qed "hdvd_one_eq_one";
paulson@13957
   474
paulson@13957
   475
Goal "~ finite prime";
paulson@13957
   476
by (rtac (hypnat_infinite_has_nonstandard_iff RS iffD2) 1);
paulson@13957
   477
by (cut_facts_tac [hypnat_dvd_all_hypnat_of_nat] 1);
paulson@13957
   478
by (etac exE 1);
paulson@13957
   479
by (etac conjE 1);
paulson@13957
   480
by (subgoal_tac "1 < N + 1" 1);
paulson@13957
   481
by (blast_tac (claset() addIs [hypnat_add_one_gt_one]) 2);
paulson@13957
   482
by (dtac hyperprime_factor_exists 1);
paulson@13957
   483
by (auto_tac (claset() addIs [NatStar_mem],simpset()));
paulson@13957
   484
by (subgoal_tac "k ~: hypnat_of_nat ` prime" 1);
paulson@13957
   485
by (force_tac (claset(),simpset() addsimps [starprime_def]) 1);
paulson@13957
   486
by (Step_tac 1);
paulson@13957
   487
by (dres_inst_tac [("x","x")] bspec 1);
paulson@13957
   488
by (rtac ccontr 1 THEN Asm_full_simp_tac 1);
paulson@13957
   489
by (dtac hdvd_diff 1 THEN assume_tac 1);
paulson@13957
   490
by (auto_tac (claset() addDs [hdvd_one_eq_one],simpset()));
paulson@13957
   491
qed "not_finite_prime";