src/HOL/Complex/ex/NSPrimes.ML

generic of_nat and of_int functions, and generalization of iszero
and neg

(*  Title       : NSPrimes.ML
    Author      : Jacques D. Fleuriot
    Copyright   : 2002 University of Edinburgh
    Description : The nonstandard primes as an extension of 
                  the prime numbers
*)

(*--------------------------------------------------------------*) 
(* A "choice" theorem for ultrafilters cf. almost everywhere    *)
(* quantification                                               *)
(*--------------------------------------------------------------*) 
    
Goal "{n. EX m. Q n m} : FreeUltrafilterNat \
\     ==> EX f. {n. Q n (f n)} : FreeUltrafilterNat";
by (res_inst_tac [("x","%n. (@x. Q n x)")] exI 1);
by (Ultra_tac 1 THEN rtac someI 1 THEN Auto_tac);
qed "UF_choice";

Goal "({n. P n} : FreeUltrafilterNat --> {n. Q n} : FreeUltrafilterNat) = \
\     ({n. P n --> Q n} : FreeUltrafilterNat)";
by Auto_tac;
by (ALLGOALS(Ultra_tac));
qed "UF_if";

Goal "({n. P n} : FreeUltrafilterNat & {n. Q n} : FreeUltrafilterNat) = \
\     ({n. P n & Q n} : FreeUltrafilterNat)";
by Auto_tac;
by (ALLGOALS(Ultra_tac));
qed "UF_conj";

Goal "(ALL f. {n. Q n (f n)} : FreeUltrafilterNat) = \
\     ({n. ALL m. Q n m} : FreeUltrafilterNat)";
by Auto_tac;
by (Ultra_tac 2);
by (rtac ccontr 1);
by (rtac swap 1 THEN assume_tac 2);
by (simp_tac (simpset() addsimps [FreeUltrafilterNat_Compl_iff1,
    CLAIM "-{n. Q n} = {n. ~ Q n}"]) 1);
by (rtac UF_choice 1);
by (Ultra_tac 1 THEN Auto_tac);
qed "UF_choice_ccontr";

Goal "ALL M. EX N. 0 < N & (ALL m. 0 < m & (m::nat) <= M --> m dvd N)";
by (rtac allI 1);
by (induct_tac "M" 1);
by Auto_tac;
by (res_inst_tac [("x","N * (Suc n)")] exI 1);
by (Step_tac 1 THEN Force_tac 1);
by (dtac le_imp_less_or_eq 1 THEN etac disjE 1);
by (force_tac (claset() addSIs [dvd_mult2],simpset()) 1);
by (force_tac (claset() addSIs [dvd_mult],simpset()) 1);
qed "dvd_by_all";

bind_thm ("dvd_by_all2",dvd_by_all RS spec);

Goal "(EX (x::hypnat). P x) = (EX f. P (Abs_hypnat(hypnatrel `` {f})))";
by Auto_tac;
by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
by Auto_tac;
qed "lemma_hypnat_P_EX";

Goal "(ALL (x::hypnat). P x) = (ALL f. P (Abs_hypnat(hypnatrel `` {f})))";
by Auto_tac;
by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
by Auto_tac;
qed "lemma_hypnat_P_ALL";

Goalw [hdvd_def]
      "(Abs_hypnat(hypnatrel``{%n. X n}) hdvd \
\           Abs_hypnat(hypnatrel``{%n. Y n})) = \
\      ({n. X n dvd Y n} : FreeUltrafilterNat)";
by (Auto_tac THEN Ultra_tac 1);
qed "hdvd";

Goal "(hypnat_of_nat n <= 0) = (n = 0)";
by (stac (hypnat_of_nat_zero RS sym) 1);
by Auto_tac;
qed "hypnat_of_nat_le_zero_iff";
Addsimps [hypnat_of_nat_le_zero_iff];


(* Goldblatt: Exercise 5.11(2) - p. 57 *)
Goal "ALL M. EX N. 0 < N & (ALL m. 0 < m & (m::hypnat) <= M --> m hdvd N)";
by (Step_tac 1);
by (res_inst_tac [("z","M")] eq_Abs_hypnat 1);
by (auto_tac (claset(),simpset() addsimps [lemma_hypnat_P_EX,
    lemma_hypnat_P_ALL,hypnat_zero_def,hypnat_le,hypnat_less,hdvd]));
by (cut_facts_tac [dvd_by_all] 1);
by (dtac (CLAIM "(ALL (M::nat). EX N. 0 < N & (ALL m. 0 < m & m <= M \
\                               --> m dvd N)) \
\                ==> ALL (n::nat). EX N. 0 < N & (ALL m. 0 < (m::nat) & m <= (x n) \
\                                  --> m dvd N)") 1);
by (dtac choice 1);
by (Step_tac 1);
by (res_inst_tac [("x","f")] exI 1);
by Auto_tac;
by (ALLGOALS(Ultra_tac));
by Auto_tac;
qed "hdvd_by_all";

bind_thm ("hdvd_by_all2",hdvd_by_all RS spec);

(* Goldblatt: Exercise 5.11(2) - p. 57 *)
Goal "EX (N::hypnat). 0 < N & (ALL n : - {0::nat}. hypnat_of_nat(n) hdvd N)"; 
by (cut_facts_tac [hdvd_by_all] 1);
by (dres_inst_tac [("x","whn")] spec 1);
by Auto_tac;
by (rtac exI 1 THEN Auto_tac);
by (dres_inst_tac [("x","hypnat_of_nat n")] spec 1);
by (auto_tac (claset(),
     simpset() addsimps [linorder_not_less, hypnat_of_nat_zero_iff]));
qed "hypnat_dvd_all_hypnat_of_nat";


(*--------------------------------------------------------------*)
(* the nonstandard extension of the set prime numbers consists  *)
(* of precisely those hypernaturals > 1 that have no nontrivial *)
(* factors                                                      *)
(*--------------------------------------------------------------*) 

(* Goldblatt: Exercise 5.11(3a) - p 57  *)
Goalw [starprime_def,thm "prime_def"]
  "starprime = {p. 1 < p & (ALL m. m hdvd p --> m = 1 | m = p)}";
by (auto_tac (claset(),simpset() addsimps 
    [CLAIM "{p. Q(p) & R(p)} = {p. Q(p)} Int {p. R(p)}",NatStar_Int]));
by (ALLGOALS(res_inst_tac [("z","x")] eq_Abs_hypnat));
by (res_inst_tac [("z","m")] eq_Abs_hypnat 2);
by (auto_tac (claset(),simpset() addsimps [hdvd,hypnat_one_def,hypnat_less,
    lemma_hypnat_P_ALL,starsetNat_def]));
by (dtac bspec 1 THEN dtac bspec 2 THEN Auto_tac);
by (Ultra_tac 1 THEN Ultra_tac 1); 
by (rtac ccontr 1);
by (dtac FreeUltrafilterNat_Compl_mem 1);
by (auto_tac (claset(),simpset() addsimps [CLAIM "- {p. Q p} = {p. ~ Q p}"]));
by (dtac UF_choice 1 THEN Auto_tac);
by (dres_inst_tac [("x","f")] spec 1 THEN Auto_tac);
by (ALLGOALS(Ultra_tac));
qed "starprime";

Goalw [thm "prime_def"] "2 : prime";
by Auto_tac;
by (ftac dvd_imp_le 1);
by (auto_tac (claset() addDs [dvd_0_left],simpset() addsimps 
    [ARITH_PROVE "(m <= (2::nat)) = (m = 0 | m = 1 | m = 2)"]));
qed "prime_two";
Addsimps [prime_two];

(* proof uses course-of-value induction *)
Goal "Suc 0 < n --> (EX k : prime. k dvd n)";
by (res_inst_tac [("n","n")] nat_less_induct 1);
by Auto_tac;
by (case_tac "n : prime" 1);
by (res_inst_tac [("x","n")] bexI 1 THEN Auto_tac);
by (dtac (conjI RS (thm "not_prime_ex_mk")) 1 THEN Auto_tac);
by (dres_inst_tac [("x","m")] spec 1 THEN Auto_tac);
by (res_inst_tac [("x","ka")] bexI 1);
by (auto_tac (claset() addIs [dvd_mult2],simpset()));
qed_spec_mp "prime_factor_exists";

(* Goldblatt Exercise 5.11(3b) - p 57  *)
Goal "1 < n ==> (EX k : starprime. k hdvd n)";
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
by (auto_tac (claset(),simpset() addsimps [hypnat_one_def,
    hypnat_less,starprime_def,lemma_hypnat_P_EX,lemma_hypnat_P_ALL,
    hdvd,starsetNat_def,CLAIM "(ALL X: S. P X) = (ALL X. X : S --> P X)",
    UF_if]));
by (res_inst_tac [("x","%n. @y. y : prime & y dvd x n")] exI 1);
by Auto_tac;
by (ALLGOALS (Ultra_tac));
by (dtac sym 1 THEN Asm_simp_tac 1);
by (ALLGOALS(rtac someI2_ex));
by (auto_tac (claset() addSDs [prime_factor_exists],simpset()));
qed_spec_mp "hyperprime_factor_exists";

(* behaves as expected! *)
Goal "( *sNat* insert x A) = insert (hypnat_of_nat x) ( *sNat* A)";
by (auto_tac (claset(),simpset() addsimps [starsetNat_def,
    hypnat_of_nat_eq]));
by (ALLGOALS(res_inst_tac [("z","xa")] eq_Abs_hypnat));
by Auto_tac;
by (TRYALL(dtac bspec));
by Auto_tac;
by (ALLGOALS(Ultra_tac));
qed "NatStar_insert";

(* Goldblatt Exercise 3.10(1) - p. 29 *)
Goal "finite A ==> *sNat* A = hypnat_of_nat ` A";
by (res_inst_tac [("P","%x. *sNat* x = hypnat_of_nat ` x")] finite_induct 1);
by (auto_tac (claset(),simpset() addsimps [NatStar_insert]));
qed "NatStar_hypnat_of_nat";

(* proved elsewhere? *)
Goal "{x} ~: FreeUltrafilterNat";
by (auto_tac (claset() addSIs [FreeUltrafilterNat_finite],simpset()));
qed "FreeUltrafilterNat_singleton_not_mem";
Addsimps [FreeUltrafilterNat_singleton_not_mem];

(*-------------------------------------------------------------------------------*)
(* Another characterization of infinite set of natural numbers                   *)
(*-------------------------------------------------------------------------------*)

Goal "finite N ==> EX n. (ALL i:N. i<(n::nat))";
by (eres_inst_tac [("F","N")] finite_induct 1);
by Auto_tac;
by (res_inst_tac [("x","Suc n + x")] exI 1);
by Auto_tac;
qed "finite_nat_set_bounded";

Goal "finite N = (EX n. (ALL i:N. i<(n::nat)))";
by (blast_tac (claset() addIs [finite_nat_set_bounded,
    bounded_nat_set_is_finite]) 1);
qed "finite_nat_set_bounded_iff";

Goal "(~ finite N) = (ALL n. EX i:N. n <= (i::nat))";
by (auto_tac (claset(),simpset() addsimps [finite_nat_set_bounded_iff,
    le_def]));
qed "not_finite_nat_set_iff";

Goal "(ALL i:N. i<=(n::nat)) ==> finite N";
by (rtac finite_subset 1);
 by (rtac finite_atMost 2);
by Auto_tac;
qed "bounded_nat_set_is_finite2";

Goal "finite N ==> EX n. (ALL i:N. i<=(n::nat))";
by (eres_inst_tac [("F","N")] finite_induct 1);
by Auto_tac;
by (res_inst_tac [("x","n + x")] exI 1);
by Auto_tac;
qed "finite_nat_set_bounded2";

Goal "finite N = (EX n. (ALL i:N. i<=(n::nat)))";
by (blast_tac (claset() addIs [finite_nat_set_bounded2,
    bounded_nat_set_is_finite2]) 1);
qed "finite_nat_set_bounded_iff2";

Goal "(~ finite N) = (ALL n. EX i:N. n < (i::nat))";
by (auto_tac (claset(),simpset() addsimps [finite_nat_set_bounded_iff2,
    le_def]));
qed "not_finite_nat_set_iff2";

(*-------------------------------------------------------------------------------*)
(* An injective function cannot define an embedded natural number                *)
(*-------------------------------------------------------------------------------*)

Goal "ALL m n. m ~= n --> f n ~= f m \
\     ==>  {n. f n = N} = {} |  (EX m. {n. f n = N} = {m})";
by Auto_tac;
by (dres_inst_tac [("x","x")] spec 1 THEN Auto_tac); 
by (subgoal_tac "ALL n. (f n = f x) = (x = n)" 1);
by Auto_tac;
qed "lemma_infinite_set_singleton";

Goal "inj f ==> Abs_hypnat(hypnatrel `` {f}) ~: Nats";
by (auto_tac (claset(), simpset() addsimps [SHNat_eq,hypnat_of_nat_eq])); 
by (subgoal_tac "ALL m n. m ~= n --> f n ~= f m" 1);
by Auto_tac;
by (dtac injD 2);
by (assume_tac 2 THEN Force_tac 2);
by (dres_inst_tac[("N","N")] lemma_infinite_set_singleton 1);
by Auto_tac;
qed "inj_fun_not_hypnat_in_SHNat";

Goalw [starsetNat_def] 
   "range f <= A ==> Abs_hypnat(hypnatrel `` {f}) : *sNat* A";
by Auto_tac;
by (Ultra_tac 1);
by (dres_inst_tac [("c","f x")] subsetD 1);
by (rtac rangeI 1);
by Auto_tac;
qed "range_subset_mem_starsetNat";

(*--------------------------------------------------------------------------------*)
(* Gleason Proposition 11-5.5. pg 149, pg 155 (ex. 3) and pg. 360                 *)
(* Let E be a nonvoid ordered set with no maximal elements (note: effectively an  *) 
(* infinite set if we take E = N (Nats)). Then there exists an order-preserving   *) 
(* injection from N to E. Of course, (as some doofus will undoubtedly point out!  *)
(* :-)) can use notion of least element in proof (i.e. no need for choice) if     *)
(* dealing with nats as we have well-ordering property                            *) 
(*--------------------------------------------------------------------------------*)

Goal "E ~= {} ==> EX x. EX X : (Pow E - {{}}). x: X";
by Auto_tac;
val lemmaPow3 = result();

Goalw [choicefun_def] "E ~= {} ==> choicefun E : E";
by (rtac (lemmaPow3 RS someI2_ex) 1);
by Auto_tac;
qed "choicefun_mem_set";
Addsimps [choicefun_mem_set];

Goal "[| E ~={}; ALL x. EX y: E. x < y |] ==> injf_max n E : E";
by (induct_tac "n" 1);
by (Force_tac 1);
by (simp_tac (simpset() addsimps [choicefun_def]) 1);
by (rtac (lemmaPow3 RS someI2_ex) 1);
by Auto_tac;
qed "injf_max_mem_set";

Goal "ALL x. EX y: E. x < y ==> injf_max n E < injf_max (Suc n) E";
by (simp_tac (simpset() addsimps [choicefun_def]) 1);
by (rtac (lemmaPow3 RS someI2_ex) 1);
by Auto_tac;
qed "injf_max_order_preserving";

Goal "ALL x. EX y: E. x < y \
\     ==> ALL n m. m < n --> injf_max m E < injf_max n E";
by (rtac allI 1);
by (induct_tac "n" 1);
by Auto_tac;
by (simp_tac (simpset() addsimps [choicefun_def]) 1);
by (rtac (lemmaPow3 RS someI2_ex) 1);
by Auto_tac;
by (dtac (CLAIM "m < Suc n ==> m = n | m < n") 1);
by Auto_tac;
by (dres_inst_tac [("x","m")] spec 1);
by Auto_tac;
by (dtac subsetD 1 THEN Auto_tac);
by (dres_inst_tac [("x","injf_max m E")] order_less_trans 1);
by Auto_tac;
qed "injf_max_order_preserving2";

Goal "ALL x. EX y: E. x < y ==> inj (%n. injf_max n E)";
by (rtac injI 1);
by (rtac ccontr 1);
by Auto_tac;
by (dtac injf_max_order_preserving2 1);
by (cut_inst_tac [("m","x"),("n","y")] less_linear 1);
by Auto_tac;
by (auto_tac (claset() addSDs [spec],simpset()));
qed "inj_injf_max";

Goal "[| (E::('a::{order} set)) ~= {}; ALL x. EX y: E. x < y |] \
\     ==> EX f. range f <= E & inj (f::nat => 'a) & (ALL m. f m < f(Suc m))";
by (res_inst_tac [("x","%n. injf_max n E")] exI 1);
by (Step_tac 1);
by (rtac injf_max_mem_set 1);
by (rtac inj_injf_max 3);
by (rtac injf_max_order_preserving 4);
by Auto_tac;
qed "infinite_set_has_order_preserving_inj";

(*-------------------------------------------------------------------------------*)
(* Only need fact that we can have an injective function from N to A for proof   *)
(*-------------------------------------------------------------------------------*)

Goal "~ finite A ==> hypnat_of_nat ` A < ( *sNat* A)";
by Auto_tac;
by (rtac subsetD 1);
by (rtac NatStar_hypreal_of_real_image_subset 1);
by Auto_tac;
by (subgoal_tac "A ~= {}" 1);
by (Force_tac 2);
by (dtac infinite_set_has_order_preserving_inj 1);
by (etac (not_finite_nat_set_iff2 RS iffD1) 1);
by Auto_tac;
by (dtac inj_fun_not_hypnat_in_SHNat 1);
by (dtac range_subset_mem_starsetNat 1);
by (auto_tac (claset(),simpset() addsimps [SHNat_eq]));
qed "hypnat_infinite_has_nonstandard";

Goal "*sNat* A =  hypnat_of_nat ` A ==> finite A";
by (rtac ccontr 1);
by (auto_tac (claset() addDs [hypnat_infinite_has_nonstandard],
    simpset()));
qed "starsetNat_eq_hypnat_of_nat_image_finite";

Goal "( *sNat* A = hypnat_of_nat ` A) = (finite A)";
by (blast_tac (claset() addSIs [starsetNat_eq_hypnat_of_nat_image_finite,
    NatStar_hypnat_of_nat]) 1);
qed "finite_starsetNat_iff";

Goal "(~ finite A) = (hypnat_of_nat ` A < *sNat* A)";
by (rtac iffI 1);
by (blast_tac (claset() addSIs [hypnat_infinite_has_nonstandard]) 1);
by (auto_tac (claset(),simpset() addsimps [finite_starsetNat_iff RS sym]));
qed "hypnat_infinite_has_nonstandard_iff";


(*-------------------------------------------------------------------------------*)
(* Existence of infinitely many primes: a nonstandard proof                      *)
(*-------------------------------------------------------------------------------*)

Goal "~ (ALL n:- {0}. hypnat_of_nat n hdvd 1)";
by Auto_tac;
by (res_inst_tac [("x","2")] bexI 1);
by (auto_tac (claset(),simpset() addsimps [hypnat_of_nat_eq,
    hypnat_one_def,hdvd,dvd_def]));
val lemma_not_dvd_hypnat_one = result();
Addsimps [lemma_not_dvd_hypnat_one];

Goal "EX n:- {0}. ~ hypnat_of_nat n hdvd 1";
by (cut_facts_tac [lemma_not_dvd_hypnat_one] 1);
by (auto_tac (claset(),simpset() delsimps [lemma_not_dvd_hypnat_one]));
val lemma_not_dvd_hypnat_one2 = result();
Addsimps [lemma_not_dvd_hypnat_one2];

(* not needed here *)
Goalw [hypnat_zero_def,hypnat_one_def] 
  "[| 0 < (N::hypnat); N ~= 1 |] ==> 1 < N";
by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
by (auto_tac (claset(),simpset() addsimps [hypnat_less]));
by (Ultra_tac 1);
qed "hypnat_gt_zero_gt_one";

Goalw [hypnat_zero_def,hypnat_one_def]
    "0 < N ==> 1 < (N::hypnat) + 1";
by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
by (auto_tac (claset(),simpset() addsimps [hypnat_less,hypnat_add]));
qed "hypnat_add_one_gt_one";

Goal "0 ~: prime";
by (Step_tac 1);
by (dtac (thm "prime_g_zero") 1);
by Auto_tac;
qed "zero_not_prime";
Addsimps [zero_not_prime];

Goal "hypnat_of_nat 0 ~: starprime";
by (auto_tac (claset() addSIs [bexI],
      simpset() addsimps [starprime_def,starsetNat_def,hypnat_of_nat_eq]));
qed "hypnat_of_nat_zero_not_prime";
Addsimps [hypnat_of_nat_zero_not_prime];

Goalw [starprime_def,starsetNat_def,hypnat_zero_def]
   "0 ~: starprime";
by (auto_tac (claset() addSIs [bexI],simpset()));
qed "hypnat_zero_not_prime";
Addsimps [hypnat_zero_not_prime];

Goal "1 ~: prime";
by (Step_tac 1);
by (dtac (thm "prime_g_one") 1);
by Auto_tac;
qed "one_not_prime";
Addsimps [one_not_prime];

Goal "Suc 0 ~: prime";
by (Step_tac 1);
by (dtac (thm "prime_g_one") 1);
by Auto_tac;
qed "one_not_prime2";
Addsimps [one_not_prime2];

Goal "hypnat_of_nat 1 ~: starprime";
by (auto_tac (claset() addSIs [bexI],
     simpset() addsimps [starprime_def,starsetNat_def,hypnat_of_nat_eq]));
qed "hypnat_of_nat_one_not_prime";
Addsimps [hypnat_of_nat_one_not_prime];

Goalw [starprime_def,starsetNat_def,hypnat_one_def]
   "1 ~: starprime";
by (auto_tac (claset() addSIs [bexI],simpset()));
qed "hypnat_one_not_prime";
Addsimps [hypnat_one_not_prime];

Goal "[| k hdvd m; k hdvd n |] ==> k hdvd (m - n)";
by (res_inst_tac [("z","k")] eq_Abs_hypnat 1);
by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
by (auto_tac (claset(),simpset() addsimps [hdvd,hypnat_minus]));
by (Ultra_tac 1);
by (blast_tac (claset() addIs [dvd_diff]) 1);
qed "hdvd_diff";

Goalw [dvd_def] "x dvd (1::nat) ==> x = 1";
by Auto_tac;
qed "dvd_one_eq_one";

Goalw [hypnat_one_def] "x hdvd 1 ==> x = 1";
by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
by (auto_tac (claset(),simpset() addsimps [hdvd]));
qed "hdvd_one_eq_one";

Goal "~ finite prime";
by (rtac (hypnat_infinite_has_nonstandard_iff RS iffD2) 1);
by (cut_facts_tac [hypnat_dvd_all_hypnat_of_nat] 1);
by (etac exE 1);
by (etac conjE 1);
by (subgoal_tac "1 < N + 1" 1);
by (blast_tac (claset() addIs [hypnat_add_one_gt_one]) 2);
by (dtac hyperprime_factor_exists 1);
by (auto_tac (claset() addIs [NatStar_mem],simpset()));
by (subgoal_tac "k ~: hypnat_of_nat ` prime" 1);
by (force_tac (claset(),simpset() addsimps [starprime_def]) 1);
by (Step_tac 1);
by (dres_inst_tac [("x","x")] bspec 1);
by (rtac ccontr 1 THEN Asm_full_simp_tac 1);
by (dtac hdvd_diff 1 THEN assume_tac 1);
by (auto_tac (claset() addDs [hdvd_one_eq_one],simpset()));
qed "not_finite_prime";