11 goal Nat.thy "bnd_mono(Inf, %X. {0} Un {succ(i). i:X})"; |
11 goal Nat.thy "bnd_mono(Inf, %X. {0} Un {succ(i). i:X})"; |
12 by (rtac bnd_monoI 1); |
12 by (rtac bnd_monoI 1); |
13 by (REPEAT (ares_tac [subset_refl, RepFun_mono, Un_mono] 2)); |
13 by (REPEAT (ares_tac [subset_refl, RepFun_mono, Un_mono] 2)); |
14 by (cut_facts_tac [infinity] 1); |
14 by (cut_facts_tac [infinity] 1); |
15 by (fast_tac ZF_cs 1); |
15 by (fast_tac ZF_cs 1); |
16 val nat_bnd_mono = result(); |
16 qed "nat_bnd_mono"; |
17 |
17 |
18 (* nat = {0} Un {succ(x). x:nat} *) |
18 (* nat = {0} Un {succ(x). x:nat} *) |
19 val nat_unfold = nat_bnd_mono RS (nat_def RS def_lfp_Tarski); |
19 val nat_unfold = nat_bnd_mono RS (nat_def RS def_lfp_Tarski); |
20 |
20 |
21 (** Type checking of 0 and successor **) |
21 (** Type checking of 0 and successor **) |
22 |
22 |
23 goal Nat.thy "0 : nat"; |
23 goal Nat.thy "0 : nat"; |
24 by (rtac (nat_unfold RS ssubst) 1); |
24 by (rtac (nat_unfold RS ssubst) 1); |
25 by (rtac (singletonI RS UnI1) 1); |
25 by (rtac (singletonI RS UnI1) 1); |
26 val nat_0I = result(); |
26 qed "nat_0I"; |
27 |
27 |
28 val prems = goal Nat.thy "n : nat ==> succ(n) : nat"; |
28 val prems = goal Nat.thy "n : nat ==> succ(n) : nat"; |
29 by (rtac (nat_unfold RS ssubst) 1); |
29 by (rtac (nat_unfold RS ssubst) 1); |
30 by (rtac (RepFunI RS UnI2) 1); |
30 by (rtac (RepFunI RS UnI2) 1); |
31 by (resolve_tac prems 1); |
31 by (resolve_tac prems 1); |
32 val nat_succI = result(); |
32 qed "nat_succI"; |
33 |
33 |
34 goal Nat.thy "1 : nat"; |
34 goal Nat.thy "1 : nat"; |
35 by (rtac (nat_0I RS nat_succI) 1); |
35 by (rtac (nat_0I RS nat_succI) 1); |
36 val nat_1I = result(); |
36 qed "nat_1I"; |
37 |
37 |
38 goal Nat.thy "bool <= nat"; |
38 goal Nat.thy "bool <= nat"; |
39 by (REPEAT (ares_tac [subsetI,nat_0I,nat_1I] 1 |
39 by (REPEAT (ares_tac [subsetI,nat_0I,nat_1I] 1 |
40 ORELSE eresolve_tac [boolE,ssubst] 1)); |
40 ORELSE eresolve_tac [boolE,ssubst] 1)); |
41 val bool_subset_nat = result(); |
41 qed "bool_subset_nat"; |
42 |
42 |
43 val bool_into_nat = bool_subset_nat RS subsetD; |
43 val bool_into_nat = bool_subset_nat RS subsetD; |
44 |
44 |
45 |
45 |
46 (** Injectivity properties and induction **) |
46 (** Injectivity properties and induction **) |
61 val major::prems = goal Nat.thy |
61 val major::prems = goal Nat.thy |
62 "[| n: nat; n=0 ==> P; !!x. [| x: nat; n=succ(x) |] ==> P |] ==> P"; |
62 "[| n: nat; n=0 ==> P; !!x. [| x: nat; n=succ(x) |] ==> P |] ==> P"; |
63 by (rtac (major RS (nat_unfold RS equalityD1 RS subsetD) RS UnE) 1); |
63 by (rtac (major RS (nat_unfold RS equalityD1 RS subsetD) RS UnE) 1); |
64 by (DEPTH_SOLVE (eresolve_tac [singletonE,RepFunE] 1 |
64 by (DEPTH_SOLVE (eresolve_tac [singletonE,RepFunE] 1 |
65 ORELSE ares_tac prems 1)); |
65 ORELSE ares_tac prems 1)); |
66 val natE = result(); |
66 qed "natE"; |
67 |
67 |
68 val prems = goal Nat.thy "n: nat ==> Ord(n)"; |
68 val prems = goal Nat.thy "n: nat ==> Ord(n)"; |
69 by (nat_ind_tac "n" prems 1); |
69 by (nat_ind_tac "n" prems 1); |
70 by (REPEAT (ares_tac [Ord_0, Ord_succ] 1)); |
70 by (REPEAT (ares_tac [Ord_0, Ord_succ] 1)); |
71 val nat_into_Ord = result(); |
71 qed "nat_into_Ord"; |
72 |
72 |
73 (* i: nat ==> 0 le i *) |
73 (* i: nat ==> 0 le i *) |
74 val nat_0_le = nat_into_Ord RS Ord_0_le; |
74 val nat_0_le = nat_into_Ord RS Ord_0_le; |
75 |
75 |
76 val nat_le_refl = nat_into_Ord RS le_refl; |
76 val nat_le_refl = nat_into_Ord RS le_refl; |
77 |
77 |
78 goal Nat.thy "!!n. n: nat ==> n=0 | 0:n"; |
78 goal Nat.thy "!!n. n: nat ==> n=0 | 0:n"; |
79 by (etac nat_induct 1); |
79 by (etac nat_induct 1); |
80 by (fast_tac ZF_cs 1); |
80 by (fast_tac ZF_cs 1); |
81 by (fast_tac (ZF_cs addIs [nat_0_le]) 1); |
81 by (fast_tac (ZF_cs addIs [nat_0_le]) 1); |
82 val natE0 = result(); |
82 qed "natE0"; |
83 |
83 |
84 goal Nat.thy "Ord(nat)"; |
84 goal Nat.thy "Ord(nat)"; |
85 by (rtac OrdI 1); |
85 by (rtac OrdI 1); |
86 by (etac (nat_into_Ord RS Ord_is_Transset) 2); |
86 by (etac (nat_into_Ord RS Ord_is_Transset) 2); |
87 by (rewtac Transset_def); |
87 by (rewtac Transset_def); |
88 by (rtac ballI 1); |
88 by (rtac ballI 1); |
89 by (etac nat_induct 1); |
89 by (etac nat_induct 1); |
90 by (REPEAT (ares_tac [empty_subsetI,succ_subsetI] 1)); |
90 by (REPEAT (ares_tac [empty_subsetI,succ_subsetI] 1)); |
91 val Ord_nat = result(); |
91 qed "Ord_nat"; |
92 |
92 |
93 goalw Nat.thy [Limit_def] "Limit(nat)"; |
93 goalw Nat.thy [Limit_def] "Limit(nat)"; |
94 by (safe_tac (ZF_cs addSIs [ltI, nat_0I, nat_1I, nat_succI, Ord_nat])); |
94 by (safe_tac (ZF_cs addSIs [ltI, nat_0I, nat_1I, nat_succI, Ord_nat])); |
95 by (etac ltD 1); |
95 by (etac ltD 1); |
96 val Limit_nat = result(); |
96 qed "Limit_nat"; |
97 |
97 |
98 goal Nat.thy "!!i. Limit(i) ==> nat le i"; |
98 goal Nat.thy "!!i. Limit(i) ==> nat le i"; |
99 by (resolve_tac [subset_imp_le] 1); |
99 by (resolve_tac [subset_imp_le] 1); |
100 by (rtac subsetI 1); |
100 by (rtac subsetI 1); |
101 by (eresolve_tac [nat_induct] 1); |
101 by (eresolve_tac [nat_induct] 1); |
102 by (fast_tac (ZF_cs addIs [Limit_has_succ RS ltD, ltI, Limit_is_Ord]) 2); |
102 by (fast_tac (ZF_cs addIs [Limit_has_succ RS ltD, ltI, Limit_is_Ord]) 2); |
103 by (REPEAT (ares_tac [Limit_has_0 RS ltD, |
103 by (REPEAT (ares_tac [Limit_has_0 RS ltD, |
104 Ord_nat, Limit_is_Ord] 1)); |
104 Ord_nat, Limit_is_Ord] 1)); |
105 val nat_le_Limit = result(); |
105 qed "nat_le_Limit"; |
106 |
106 |
107 (* succ(i): nat ==> i: nat *) |
107 (* succ(i): nat ==> i: nat *) |
108 val succ_natD = [succI1, asm_rl, Ord_nat] MRS Ord_trans; |
108 val succ_natD = [succI1, asm_rl, Ord_nat] MRS Ord_trans; |
109 |
109 |
110 (* [| succ(i): k; k: nat |] ==> i: k *) |
110 (* [| succ(i): k; k: nat |] ==> i: k *) |
128 \ |] ==> m le n --> P(m) --> P(n)"; |
128 \ |] ==> m le n --> P(m) --> P(n)"; |
129 by (nat_ind_tac "n" prems 1); |
129 by (nat_ind_tac "n" prems 1); |
130 by (ALLGOALS |
130 by (ALLGOALS |
131 (asm_simp_tac |
131 (asm_simp_tac |
132 (ZF_ss addsimps (prems@distrib_rews@[le0_iff, le_succ_iff])))); |
132 (ZF_ss addsimps (prems@distrib_rews@[le0_iff, le_succ_iff])))); |
133 val nat_induct_from_lemma = result(); |
133 qed "nat_induct_from_lemma"; |
134 |
134 |
135 (*Induction starting from m rather than 0*) |
135 (*Induction starting from m rather than 0*) |
136 val prems = goal Nat.thy |
136 val prems = goal Nat.thy |
137 "[| m le n; m: nat; n: nat; \ |
137 "[| m le n; m: nat; n: nat; \ |
138 \ P(m); \ |
138 \ P(m); \ |
139 \ !!x. [| x: nat; m le x; P(x) |] ==> P(succ(x)) \ |
139 \ !!x. [| x: nat; m le x; P(x) |] ==> P(succ(x)) \ |
140 \ |] ==> P(n)"; |
140 \ |] ==> P(n)"; |
141 by (rtac (nat_induct_from_lemma RS mp RS mp) 1); |
141 by (rtac (nat_induct_from_lemma RS mp RS mp) 1); |
142 by (REPEAT (ares_tac prems 1)); |
142 by (REPEAT (ares_tac prems 1)); |
143 val nat_induct_from = result(); |
143 qed "nat_induct_from"; |
144 |
144 |
145 (*Induction suitable for subtraction and less-than*) |
145 (*Induction suitable for subtraction and less-than*) |
146 val prems = goal Nat.thy |
146 val prems = goal Nat.thy |
147 "[| m: nat; n: nat; \ |
147 "[| m: nat; n: nat; \ |
148 \ !!x. x: nat ==> P(x,0); \ |
148 \ !!x. x: nat ==> P(x,0); \ |
153 by (resolve_tac prems 2); |
153 by (resolve_tac prems 2); |
154 by (nat_ind_tac "n" prems 1); |
154 by (nat_ind_tac "n" prems 1); |
155 by (rtac ballI 2); |
155 by (rtac ballI 2); |
156 by (nat_ind_tac "x" [] 2); |
156 by (nat_ind_tac "x" [] 2); |
157 by (REPEAT (ares_tac (prems@[ballI]) 1 ORELSE etac bspec 1)); |
157 by (REPEAT (ares_tac (prems@[ballI]) 1 ORELSE etac bspec 1)); |
158 val diff_induct = result(); |
158 qed "diff_induct"; |
159 |
159 |
160 (** Induction principle analogous to trancl_induct **) |
160 (** Induction principle analogous to trancl_induct **) |
161 |
161 |
162 goal Nat.thy |
162 goal Nat.thy |
163 "!!m. m: nat ==> P(m,succ(m)) --> (ALL x: nat. P(m,x) --> P(m,succ(x))) --> \ |
163 "!!m. m: nat ==> P(m,succ(m)) --> (ALL x: nat. P(m,x) --> P(m,succ(x))) --> \ |
164 \ (ALL n:nat. m<n --> P(m,n))"; |
164 \ (ALL n:nat. m<n --> P(m,n))"; |
165 by (etac nat_induct 1); |
165 by (etac nat_induct 1); |
166 by (ALLGOALS |
166 by (ALLGOALS |
167 (EVERY' [rtac (impI RS impI), rtac (nat_induct RS ballI), assume_tac, |
167 (EVERY' [rtac (impI RS impI), rtac (nat_induct RS ballI), assume_tac, |
168 fast_tac lt_cs, fast_tac lt_cs])); |
168 fast_tac lt_cs, fast_tac lt_cs])); |
169 val succ_lt_induct_lemma = result(); |
169 qed "succ_lt_induct_lemma"; |
170 |
170 |
171 val prems = goal Nat.thy |
171 val prems = goal Nat.thy |
172 "[| m<n; n: nat; \ |
172 "[| m<n; n: nat; \ |
173 \ P(m,succ(m)); \ |
173 \ P(m,succ(m)); \ |
174 \ !!x. [| x: nat; P(m,x) |] ==> P(m,succ(x)) \ |
174 \ !!x. [| x: nat; P(m,x) |] ==> P(m,succ(x)) \ |
175 \ |] ==> P(m,n)"; |
175 \ |] ==> P(m,n)"; |
176 by (res_inst_tac [("P4","P")] |
176 by (res_inst_tac [("P4","P")] |
177 (succ_lt_induct_lemma RS mp RS mp RS bspec RS mp) 1); |
177 (succ_lt_induct_lemma RS mp RS mp RS bspec RS mp) 1); |
178 by (REPEAT (ares_tac (prems @ [ballI, impI, lt_nat_in_nat]) 1)); |
178 by (REPEAT (ares_tac (prems @ [ballI, impI, lt_nat_in_nat]) 1)); |
179 val succ_lt_induct = result(); |
179 qed "succ_lt_induct"; |
180 |
180 |
181 (** nat_case **) |
181 (** nat_case **) |
182 |
182 |
183 goalw Nat.thy [nat_case_def] "nat_case(a,b,0) = a"; |
183 goalw Nat.thy [nat_case_def] "nat_case(a,b,0) = a"; |
184 by (fast_tac (ZF_cs addIs [the_equality]) 1); |
184 by (fast_tac (ZF_cs addIs [the_equality]) 1); |
185 val nat_case_0 = result(); |
185 qed "nat_case_0"; |
186 |
186 |
187 goalw Nat.thy [nat_case_def] "nat_case(a,b,succ(m)) = b(m)"; |
187 goalw Nat.thy [nat_case_def] "nat_case(a,b,succ(m)) = b(m)"; |
188 by (fast_tac (ZF_cs addIs [the_equality]) 1); |
188 by (fast_tac (ZF_cs addIs [the_equality]) 1); |
189 val nat_case_succ = result(); |
189 qed "nat_case_succ"; |
190 |
190 |
191 val major::prems = goal Nat.thy |
191 val major::prems = goal Nat.thy |
192 "[| n: nat; a: C(0); !!m. m: nat ==> b(m): C(succ(m)) \ |
192 "[| n: nat; a: C(0); !!m. m: nat ==> b(m): C(succ(m)) \ |
193 \ |] ==> nat_case(a,b,n) : C(n)"; |
193 \ |] ==> nat_case(a,b,n) : C(n)"; |
194 by (rtac (major RS nat_induct) 1); |
194 by (rtac (major RS nat_induct) 1); |
195 by (ALLGOALS |
195 by (ALLGOALS |
196 (asm_simp_tac (ZF_ss addsimps (prems @ [nat_case_0, nat_case_succ])))); |
196 (asm_simp_tac (ZF_ss addsimps (prems @ [nat_case_0, nat_case_succ])))); |
197 val nat_case_type = result(); |
197 qed "nat_case_type"; |
198 |
198 |
199 |
199 |
200 (** nat_rec -- used to define eclose and transrec, then obsolete; |
200 (** nat_rec -- used to define eclose and transrec, then obsolete; |
201 rec, from arith.ML, has fewer typing conditions **) |
201 rec, from arith.ML, has fewer typing conditions **) |
202 |
202 |
203 val nat_rec_trans = wf_Memrel RS (nat_rec_def RS def_wfrec RS trans); |
203 val nat_rec_trans = wf_Memrel RS (nat_rec_def RS def_wfrec RS trans); |
204 |
204 |
205 goal Nat.thy "nat_rec(0,a,b) = a"; |
205 goal Nat.thy "nat_rec(0,a,b) = a"; |
206 by (rtac nat_rec_trans 1); |
206 by (rtac nat_rec_trans 1); |
207 by (rtac nat_case_0 1); |
207 by (rtac nat_case_0 1); |
208 val nat_rec_0 = result(); |
208 qed "nat_rec_0"; |
209 |
209 |
210 val [prem] = goal Nat.thy |
210 val [prem] = goal Nat.thy |
211 "m: nat ==> nat_rec(succ(m),a,b) = b(m, nat_rec(m,a,b))"; |
211 "m: nat ==> nat_rec(succ(m),a,b) = b(m, nat_rec(m,a,b))"; |
212 by (rtac nat_rec_trans 1); |
212 by (rtac nat_rec_trans 1); |
213 by (simp_tac (ZF_ss addsimps [prem, nat_case_succ, nat_succI, Memrel_iff, |
213 by (simp_tac (ZF_ss addsimps [prem, nat_case_succ, nat_succI, Memrel_iff, |
214 vimage_singleton_iff]) 1); |
214 vimage_singleton_iff]) 1); |
215 val nat_rec_succ = result(); |
215 qed "nat_rec_succ"; |
216 |
216 |
217 (** The union of two natural numbers is a natural number -- their maximum **) |
217 (** The union of two natural numbers is a natural number -- their maximum **) |
218 |
218 |
219 goal Nat.thy "!!i j. [| i: nat; j: nat |] ==> i Un j: nat"; |
219 goal Nat.thy "!!i j. [| i: nat; j: nat |] ==> i Un j: nat"; |
220 by (rtac (Un_least_lt RS ltD) 1); |
220 by (rtac (Un_least_lt RS ltD) 1); |
221 by (REPEAT (ares_tac [ltI, Ord_nat] 1)); |
221 by (REPEAT (ares_tac [ltI, Ord_nat] 1)); |
222 val Un_nat_type = result(); |
222 qed "Un_nat_type"; |
223 |
223 |
224 goal Nat.thy "!!i j. [| i: nat; j: nat |] ==> i Int j: nat"; |
224 goal Nat.thy "!!i j. [| i: nat; j: nat |] ==> i Int j: nat"; |
225 by (rtac (Int_greatest_lt RS ltD) 1); |
225 by (rtac (Int_greatest_lt RS ltD) 1); |
226 by (REPEAT (ares_tac [ltI, Ord_nat] 1)); |
226 by (REPEAT (ares_tac [ltI, Ord_nat] 1)); |
227 val Int_nat_type = result(); |
227 qed "Int_nat_type"; |