src/HOL/Complex/NSInduct.ML

HOL-Real -> HOL-Complex

(*  Title:       NSInduct.ML
    Author:      Jacques D. Fleuriot
    Copyright:   2001  University of Edinburgh
    Description: Nonstandard characterization of induction etc.
*)

Goalw [starPNat_def]
"(( *pNat* P) (Abs_hypnat(hypnatrel``{%n. X n}))) = \
\     ({n. P (X n)} : FreeUltrafilterNat)";
by (Auto_tac);
by (Ultra_tac 1);
qed "starPNat";

Goalw [hypnat_of_nat_def] "( *pNat* P) (hypnat_of_nat n) = P n";
by (auto_tac (claset(),simpset() addsimps [starPNat]));
qed "starPNat_hypnat_of_nat";
Addsimps [starPNat_hypnat_of_nat];

Goalw [hypnat_zero_def,hypnat_one_def]
    "!!P. (( *pNat* P) 0 &   \
\           (ALL n. ( *pNat* P)(n) --> ( *pNat* P)(n + 1))) \
\      --> ( *pNat* P)(n)";
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
by (auto_tac (claset(),simpset() addsimps [starPNat]));
by (Ultra_tac 1);
by (etac nat_induct 1);
by (dres_inst_tac [("x","hypnat_of_nat n")] spec 1);
by (rtac ccontr 1);
by (auto_tac (claset(),simpset() addsimps [starPNat,
    hypnat_of_nat_def,hypnat_add]));
qed "hypnat_induct_obj";

Goal
  "!!P. [| ( *pNat* P) 0;   \
\        !!n. ( *pNat* P)(n) ==> ( *pNat* P)(n + 1)|] \
\    ==> ( *pNat* P)(n)";
by (cut_inst_tac [("P","P"),("n","n")] hypnat_induct_obj 1);
by (Auto_tac);
qed "hypnat_induct";

fun hypnat_ind_tac a i = 
  res_inst_tac [("n",a)] hypnat_induct i  THEN  rename_last_tac a [""] (i+1);

Goalw [starPNat2_def]
"(( *pNat2* P) (Abs_hypnat(hypnatrel``{%n. X n})) \
\            (Abs_hypnat(hypnatrel``{%n. Y n}))) = \
\     ({n. P (X n) (Y n)} : FreeUltrafilterNat)";
by (Auto_tac);
by (Ultra_tac 1);
qed "starPNat2";

Goalw [starPNat2_def] "( *pNat2* (op =)) = (op =)";
by (rtac ext 1);
by (rtac ext 1);
by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
by (res_inst_tac [("z","y")] eq_Abs_hypnat 1);
by (Auto_tac THEN Ultra_tac 1);
qed "starPNat2_eq_iff";

Goal "( *pNat2* (%x y. x = y)) X Y = (X = Y)";
by (simp_tac (simpset() addsimps [starPNat2_eq_iff]) 1);
qed "starPNat2_eq_iff2";

Goal "(EX h. P(h::hypnat)) = (EX x. P(Abs_hypnat(hypnatrel `` {x})))";
by (Auto_tac);
by (res_inst_tac [("z","h")] eq_Abs_hypnat 1);
by (Auto_tac);
val lemma_hyp = result();

Goal "(EX (v::nat=>nat). ALL (x::nat). P (g v) (f x)) = \
\     (EX (v::nat=>nat). ALL x. EX f': Rep_hypnat(f x). P (g v) (Abs_hypnat(hypnatrel `` {f'})))"; 
by (Auto_tac);
by (ALLGOALS(res_inst_tac [("x","v")] exI));
by (Step_tac 1);
by (ALLGOALS(res_inst_tac [("z","f x")] eq_Abs_hypnat));
by (Auto_tac);
by (rtac bexI 1);
by (dres_inst_tac [("x","x")] spec 3);
by (dtac sym 1);
by (Auto_tac);
by (subgoal_tac 
    "Abs_hypnat (hypnatrel `` {X}) = Abs_hypnat (hypnatrel `` {Y})" 1);
by (Asm_simp_tac 1);
by (Auto_tac);
val lemma_hyp2 = result();

Goalw [hSuc_def] "hSuc m ~= 0";
by Auto_tac;
qed "hSuc_not_zero";

bind_thm ("zero_not_hSuc", hSuc_not_zero RS not_sym);

Goalw [hSuc_def,hypnat_one_def] 
      "(hSuc m = hSuc n) = (m = n)";
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 [hypnat_add]));
qed "hSuc_hSuc_eq";

AddIffs [hSuc_not_zero,zero_not_hSuc,hSuc_hSuc_eq];

Goalw [hypnat_le_def] "m <= (n::hypnat) | n <= m";
by (auto_tac (claset() addDs [hypnat_less_trans],simpset()));
qed "hypnat_le_linear";

val hypnat_less_le = hypnat_less_imp_le;

Goal "c : (S :: nat set) ==> (LEAST n. n : S) : S";
by (etac LeastI 1);
qed "nonempty_nat_set_Least_mem";

Goalw [InternalNatSets_def,starsetNat_n_def]
    "[| S : InternalNatSets; S ~= {} |] ==> EX n: S. ALL m: S. n <= m";
by (auto_tac (claset(),simpset() addsimps [lemma_hyp]));
by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
by (auto_tac (claset() addSDs [bspec],simpset() addsimps [hypnat_le]));
by (dres_inst_tac [("x","%m. LEAST n. n : As m")] spec 1);
by Auto_tac;
by (ultra_tac (claset() addDs [nonempty_nat_set_Least_mem],simpset()) 1);
by (dres_inst_tac [("x","x")] bspec 1 THEN Auto_tac);
by (ultra_tac (claset() addIs [Least_le],simpset()) 1);
qed "nonempty_InternalNatSet_has_least";

(* Goldblatt p 129 Thm 11.3.2 *)
Goal "[| X : InternalNatSets; 0 : X; ALL n. n : X --> n + 1 : X |] \
\     ==> X = (UNIV:: hypnat set)";
by (rtac ccontr 1);
by (ftac InternalNatSets_Compl 1);
by (dres_inst_tac [("S","- X")] nonempty_InternalNatSet_has_least 1);
by Auto_tac;
by (subgoal_tac "1 <= n" 1);
by (dres_inst_tac [("x","n - 1")] bspec 1);
by (Step_tac 1);
by (dres_inst_tac [("x","n - 1")] spec 1);
by (dres_inst_tac [("x","1"),("q1.0","n")] hypnat_add_le_mono1 2);
by (auto_tac (claset(),simpset() addsimps [hypnat_le_def]));
qed "internal_induct";