paulson@13957
|
1 |
(* Title: NSInduct.ML
|
paulson@13957
|
2 |
Author: Jacques D. Fleuriot
|
paulson@13957
|
3 |
Copyright: 2001 University of Edinburgh
|
paulson@13957
|
4 |
Description: Nonstandard characterization of induction etc.
|
paulson@13957
|
5 |
*)
|
paulson@13957
|
6 |
|
paulson@13957
|
7 |
Goalw [starPNat_def]
|
paulson@13957
|
8 |
"(( *pNat* P) (Abs_hypnat(hypnatrel``{%n. X n}))) = \
|
paulson@13957
|
9 |
\ ({n. P (X n)} : FreeUltrafilterNat)";
|
paulson@13957
|
10 |
by (Auto_tac);
|
paulson@13957
|
11 |
by (Ultra_tac 1);
|
paulson@13957
|
12 |
qed "starPNat";
|
paulson@13957
|
13 |
|
paulson@14378
|
14 |
Goal "( *pNat* P) (hypnat_of_nat n) = P n";
|
paulson@14378
|
15 |
by (auto_tac (claset(),simpset() addsimps [starPNat, hypnat_of_nat_eq]));
|
paulson@13957
|
16 |
qed "starPNat_hypnat_of_nat";
|
paulson@13957
|
17 |
Addsimps [starPNat_hypnat_of_nat];
|
paulson@13957
|
18 |
|
paulson@13957
|
19 |
Goalw [hypnat_zero_def,hypnat_one_def]
|
paulson@13957
|
20 |
"!!P. (( *pNat* P) 0 & \
|
paulson@13957
|
21 |
\ (ALL n. ( *pNat* P)(n) --> ( *pNat* P)(n + 1))) \
|
paulson@13957
|
22 |
\ --> ( *pNat* P)(n)";
|
paulson@13957
|
23 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
|
paulson@13957
|
24 |
by (auto_tac (claset(),simpset() addsimps [starPNat]));
|
paulson@13957
|
25 |
by (Ultra_tac 1);
|
paulson@13957
|
26 |
by (etac nat_induct 1);
|
paulson@13957
|
27 |
by (dres_inst_tac [("x","hypnat_of_nat n")] spec 1);
|
paulson@13957
|
28 |
by (rtac ccontr 1);
|
paulson@13957
|
29 |
by (auto_tac (claset(),simpset() addsimps [starPNat,
|
paulson@14378
|
30 |
hypnat_of_nat_eq,hypnat_add]));
|
paulson@13957
|
31 |
qed "hypnat_induct_obj";
|
paulson@13957
|
32 |
|
paulson@13957
|
33 |
Goal
|
paulson@13957
|
34 |
"!!P. [| ( *pNat* P) 0; \
|
paulson@13957
|
35 |
\ !!n. ( *pNat* P)(n) ==> ( *pNat* P)(n + 1)|] \
|
paulson@13957
|
36 |
\ ==> ( *pNat* P)(n)";
|
paulson@13957
|
37 |
by (cut_inst_tac [("P","P"),("n","n")] hypnat_induct_obj 1);
|
paulson@13957
|
38 |
by (Auto_tac);
|
paulson@13957
|
39 |
qed "hypnat_induct";
|
paulson@13957
|
40 |
|
paulson@13957
|
41 |
fun hypnat_ind_tac a i =
|
paulson@13957
|
42 |
res_inst_tac [("n",a)] hypnat_induct i THEN rename_last_tac a [""] (i+1);
|
paulson@13957
|
43 |
|
paulson@13957
|
44 |
Goalw [starPNat2_def]
|
paulson@13957
|
45 |
"(( *pNat2* P) (Abs_hypnat(hypnatrel``{%n. X n})) \
|
paulson@13957
|
46 |
\ (Abs_hypnat(hypnatrel``{%n. Y n}))) = \
|
paulson@13957
|
47 |
\ ({n. P (X n) (Y n)} : FreeUltrafilterNat)";
|
paulson@13957
|
48 |
by (Auto_tac);
|
paulson@13957
|
49 |
by (Ultra_tac 1);
|
paulson@13957
|
50 |
qed "starPNat2";
|
paulson@13957
|
51 |
|
paulson@13957
|
52 |
Goalw [starPNat2_def] "( *pNat2* (op =)) = (op =)";
|
paulson@13957
|
53 |
by (rtac ext 1);
|
paulson@13957
|
54 |
by (rtac ext 1);
|
paulson@13957
|
55 |
by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
|
paulson@13957
|
56 |
by (res_inst_tac [("z","y")] eq_Abs_hypnat 1);
|
paulson@13957
|
57 |
by (Auto_tac THEN Ultra_tac 1);
|
paulson@13957
|
58 |
qed "starPNat2_eq_iff";
|
paulson@13957
|
59 |
|
paulson@13957
|
60 |
Goal "( *pNat2* (%x y. x = y)) X Y = (X = Y)";
|
paulson@13957
|
61 |
by (simp_tac (simpset() addsimps [starPNat2_eq_iff]) 1);
|
paulson@13957
|
62 |
qed "starPNat2_eq_iff2";
|
paulson@13957
|
63 |
|
paulson@13957
|
64 |
Goal "(EX h. P(h::hypnat)) = (EX x. P(Abs_hypnat(hypnatrel `` {x})))";
|
paulson@13957
|
65 |
by (Auto_tac);
|
paulson@13957
|
66 |
by (res_inst_tac [("z","h")] eq_Abs_hypnat 1);
|
paulson@13957
|
67 |
by (Auto_tac);
|
paulson@13957
|
68 |
val lemma_hyp = result();
|
paulson@13957
|
69 |
|
paulson@13957
|
70 |
Goalw [hSuc_def] "hSuc m ~= 0";
|
paulson@13957
|
71 |
by Auto_tac;
|
paulson@13957
|
72 |
qed "hSuc_not_zero";
|
paulson@13957
|
73 |
|
paulson@13957
|
74 |
bind_thm ("zero_not_hSuc", hSuc_not_zero RS not_sym);
|
paulson@13957
|
75 |
|
paulson@13957
|
76 |
Goalw [hSuc_def,hypnat_one_def]
|
paulson@13957
|
77 |
"(hSuc m = hSuc n) = (m = n)";
|
paulson@13957
|
78 |
by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
|
paulson@13957
|
79 |
by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
|
paulson@13957
|
80 |
by (auto_tac (claset(),simpset() addsimps [hypnat_add]));
|
paulson@13957
|
81 |
qed "hSuc_hSuc_eq";
|
paulson@13957
|
82 |
|
paulson@13957
|
83 |
AddIffs [hSuc_not_zero,zero_not_hSuc,hSuc_hSuc_eq];
|
paulson@13957
|
84 |
|
paulson@13957
|
85 |
Goal "c : (S :: nat set) ==> (LEAST n. n : S) : S";
|
paulson@13957
|
86 |
by (etac LeastI 1);
|
paulson@13957
|
87 |
qed "nonempty_nat_set_Least_mem";
|
paulson@13957
|
88 |
|
paulson@13957
|
89 |
Goalw [InternalNatSets_def,starsetNat_n_def]
|
paulson@13957
|
90 |
"[| S : InternalNatSets; S ~= {} |] ==> EX n: S. ALL m: S. n <= m";
|
paulson@13957
|
91 |
by (auto_tac (claset(),simpset() addsimps [lemma_hyp]));
|
paulson@13957
|
92 |
by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
|
paulson@13957
|
93 |
by (auto_tac (claset() addSDs [bspec],simpset() addsimps [hypnat_le]));
|
paulson@13957
|
94 |
by (dres_inst_tac [("x","%m. LEAST n. n : As m")] spec 1);
|
paulson@13957
|
95 |
by Auto_tac;
|
paulson@13957
|
96 |
by (ultra_tac (claset() addDs [nonempty_nat_set_Least_mem],simpset()) 1);
|
paulson@13957
|
97 |
by (dres_inst_tac [("x","x")] bspec 1 THEN Auto_tac);
|
paulson@13957
|
98 |
by (ultra_tac (claset() addIs [Least_le],simpset()) 1);
|
paulson@13957
|
99 |
qed "nonempty_InternalNatSet_has_least";
|
paulson@13957
|
100 |
|
paulson@13957
|
101 |
(* Goldblatt p 129 Thm 11.3.2 *)
|
paulson@13957
|
102 |
Goal "[| X : InternalNatSets; 0 : X; ALL n. n : X --> n + 1 : X |] \
|
paulson@13957
|
103 |
\ ==> X = (UNIV:: hypnat set)";
|
paulson@13957
|
104 |
by (rtac ccontr 1);
|
paulson@13957
|
105 |
by (ftac InternalNatSets_Compl 1);
|
paulson@13957
|
106 |
by (dres_inst_tac [("S","- X")] nonempty_InternalNatSet_has_least 1);
|
paulson@13957
|
107 |
by Auto_tac;
|
paulson@13957
|
108 |
by (subgoal_tac "1 <= n" 1);
|
paulson@13957
|
109 |
by (dres_inst_tac [("x","n - 1")] bspec 1);
|
paulson@13957
|
110 |
by (Step_tac 1);
|
paulson@13957
|
111 |
by (dres_inst_tac [("x","n - 1")] spec 1);
|
paulson@14371
|
112 |
by (dres_inst_tac [("c","1"),("a","n")] add_right_mono 2);
|
paulson@14371
|
113 |
by (auto_tac ((claset(),simpset() addsimps [linorder_not_less RS sym])
|
paulson@14371
|
114 |
delIffs [hypnat_neq0_conv]));
|
paulson@13957
|
115 |
qed "internal_induct";
|
paulson@13957
|
116 |
|