67 val prems = goal Nat.thy "n: nat ==> Ord(n)"; |
67 val prems = goal Nat.thy "n: nat ==> Ord(n)"; |
68 by (nat_ind_tac "n" prems 1); |
68 by (nat_ind_tac "n" prems 1); |
69 by (REPEAT (ares_tac [Ord_0, Ord_succ] 1)); |
69 by (REPEAT (ares_tac [Ord_0, Ord_succ] 1)); |
70 val naturals_are_ordinals = result(); |
70 val naturals_are_ordinals = result(); |
71 |
71 |
72 (* i: nat ==> 0: succ(i) *) |
72 (* i: nat ==> 0 le i *) |
73 val nat_0_in_succ = naturals_are_ordinals RS Ord_0_in_succ; |
73 val nat_0_le = naturals_are_ordinals RS Ord_0_le; |
74 |
74 |
75 goal Nat.thy "!!n. n: nat ==> n=0 | 0:n"; |
75 goal Nat.thy "!!n. n: nat ==> n=0 | 0:n"; |
76 by (etac nat_induct 1); |
76 by (etac nat_induct 1); |
77 by (fast_tac ZF_cs 1); |
77 by (fast_tac ZF_cs 1); |
78 by (fast_tac (ZF_cs addIs [nat_0_in_succ]) 1); |
78 by (fast_tac (ZF_cs addIs [nat_0_le]) 1); |
79 val natE0 = result(); |
79 val natE0 = result(); |
80 |
80 |
81 goal Nat.thy "Ord(nat)"; |
81 goal Nat.thy "Ord(nat)"; |
82 by (rtac OrdI 1); |
82 by (rtac OrdI 1); |
83 by (etac (naturals_are_ordinals RS Ord_is_Transset) 2); |
83 by (etac (naturals_are_ordinals RS Ord_is_Transset) 2); |
91 val succ_natD = [succI1, asm_rl, Ord_nat] MRS Ord_trans; |
91 val succ_natD = [succI1, asm_rl, Ord_nat] MRS Ord_trans; |
92 |
92 |
93 (* [| succ(i): k; k: nat |] ==> i: k *) |
93 (* [| succ(i): k; k: nat |] ==> i: k *) |
94 val succ_in_naturalD = [succI1, asm_rl, naturals_are_ordinals] MRS Ord_trans; |
94 val succ_in_naturalD = [succI1, asm_rl, naturals_are_ordinals] MRS Ord_trans; |
95 |
95 |
|
96 goal Nat.thy "!!m n. [| m<n; n: nat |] ==> m: nat"; |
|
97 by (etac ltE 1); |
|
98 by (etac (Ord_nat RSN (3,Ord_trans)) 1); |
|
99 by (assume_tac 1); |
|
100 val lt_nat_in_nat = result(); |
|
101 |
|
102 |
96 (** Variations on mathematical induction **) |
103 (** Variations on mathematical induction **) |
97 |
104 |
98 (*complete induction*) |
105 (*complete induction*) |
99 val complete_induct = Ord_nat RSN (2, Ord_induct); |
106 val complete_induct = Ord_nat RSN (2, Ord_induct); |
100 |
107 |
101 val prems = goal Nat.thy |
108 val prems = goal Nat.thy |
102 "[| m: nat; n: nat; \ |
109 "[| m: nat; n: nat; \ |
103 \ !!x. [| x: nat; m<=x; P(x) |] ==> P(succ(x)) \ |
110 \ !!x. [| x: nat; m le x; P(x) |] ==> P(succ(x)) \ |
104 \ |] ==> m <= n --> P(m) --> P(n)"; |
111 \ |] ==> m le n --> P(m) --> P(n)"; |
105 by (nat_ind_tac "n" prems 1); |
112 by (nat_ind_tac "n" prems 1); |
106 by (ALLGOALS |
113 by (ALLGOALS |
107 (asm_simp_tac |
114 (asm_simp_tac |
108 (ZF_ss addsimps (prems@distrib_rews@[subset_empty_iff, subset_succ_iff, |
115 (ZF_ss addsimps (prems@distrib_rews@[le0_iff, le_succ_iff])))); |
109 naturals_are_ordinals])))); |
|
110 val nat_induct_from_lemma = result(); |
116 val nat_induct_from_lemma = result(); |
111 |
117 |
112 (*Induction starting from m rather than 0*) |
118 (*Induction starting from m rather than 0*) |
113 val prems = goal Nat.thy |
119 val prems = goal Nat.thy |
114 "[| m <= n; m: nat; n: nat; \ |
120 "[| m le n; m: nat; n: nat; \ |
115 \ P(m); \ |
121 \ P(m); \ |
116 \ !!x. [| x: nat; m<=x; P(x) |] ==> P(succ(x)) \ |
122 \ !!x. [| x: nat; m le x; P(x) |] ==> P(succ(x)) \ |
117 \ |] ==> P(n)"; |
123 \ |] ==> P(n)"; |
118 by (rtac (nat_induct_from_lemma RS mp RS mp) 1); |
124 by (rtac (nat_induct_from_lemma RS mp RS mp) 1); |
119 by (REPEAT (ares_tac prems 1)); |
125 by (REPEAT (ares_tac prems 1)); |
120 val nat_induct_from = result(); |
126 val nat_induct_from = result(); |
121 |
127 |
122 (*Induction suitable for subtraction and less-than*) |
128 (*Induction suitable for subtraction and less-than*) |
123 val prems = goal Nat.thy |
129 val prems = goal Nat.thy |
124 "[| m: nat; n: nat; \ |
130 "[| m: nat; n: nat; \ |
125 \ !!x. [| x: nat |] ==> P(x,0); \ |
131 \ !!x. x: nat ==> P(x,0); \ |
126 \ !!y. [| y: nat |] ==> P(0,succ(y)); \ |
132 \ !!y. y: nat ==> P(0,succ(y)); \ |
127 \ !!x y. [| x: nat; y: nat; P(x,y) |] ==> P(succ(x),succ(y)) \ |
133 \ !!x y. [| x: nat; y: nat; P(x,y) |] ==> P(succ(x),succ(y)) \ |
128 \ |] ==> P(m,n)"; |
134 \ |] ==> P(m,n)"; |
129 by (res_inst_tac [("x","m")] bspec 1); |
135 by (res_inst_tac [("x","m")] bspec 1); |
130 by (resolve_tac prems 2); |
136 by (resolve_tac prems 2); |
131 by (nat_ind_tac "n" prems 1); |
137 by (nat_ind_tac "n" prems 1); |
136 |
142 |
137 (** Induction principle analogous to trancl_induct **) |
143 (** Induction principle analogous to trancl_induct **) |
138 |
144 |
139 goal Nat.thy |
145 goal Nat.thy |
140 "!!m. m: nat ==> P(m,succ(m)) --> (ALL x: nat. P(m,x) --> P(m,succ(x))) --> \ |
146 "!!m. m: nat ==> P(m,succ(m)) --> (ALL x: nat. P(m,x) --> P(m,succ(x))) --> \ |
141 \ (ALL n:nat. m:n --> P(m,n))"; |
147 \ (ALL n:nat. m<n --> P(m,n))"; |
142 by (etac nat_induct 1); |
148 by (etac nat_induct 1); |
143 by (ALLGOALS |
149 by (ALLGOALS |
144 (EVERY' [rtac (impI RS impI), rtac (nat_induct RS ballI), assume_tac, |
150 (EVERY' [rtac (impI RS impI), rtac (nat_induct RS ballI), assume_tac, |
145 fast_tac ZF_cs, fast_tac ZF_cs])); |
151 fast_tac lt_cs, fast_tac lt_cs])); |
146 val succ_less_induct_lemma = result(); |
152 val succ_lt_induct_lemma = result(); |
147 |
153 |
148 val prems = goal Nat.thy |
154 val prems = goal Nat.thy |
149 "[| m: n; n: nat; \ |
155 "[| m<n; n: nat; \ |
150 \ P(m,succ(m)); \ |
156 \ P(m,succ(m)); \ |
151 \ !!x. [| x: nat; P(m,x) |] ==> P(m,succ(x)) \ |
157 \ !!x. [| x: nat; P(m,x) |] ==> P(m,succ(x)) \ |
152 \ |] ==> P(m,n)"; |
158 \ |] ==> P(m,n)"; |
153 by (res_inst_tac [("P4","P")] |
159 by (res_inst_tac [("P4","P")] |
154 (succ_less_induct_lemma RS mp RS mp RS bspec RS mp) 1); |
160 (succ_lt_induct_lemma RS mp RS mp RS bspec RS mp) 1); |
155 by (rtac (Ord_nat RSN (3,Ord_trans)) 1); |
161 by (REPEAT (ares_tac (prems @ [ballI, impI, lt_nat_in_nat]) 1)); |
156 by (REPEAT (ares_tac (prems @ [ballI,impI]) 1)); |
162 val succ_lt_induct = result(); |
157 val succ_less_induct = result(); |
|
158 |
163 |
159 (** nat_case **) |
164 (** nat_case **) |
160 |
165 |
161 goalw Nat.thy [nat_case_def] "nat_case(a,b,0) = a"; |
166 goalw Nat.thy [nat_case_def] "nat_case(a,b,0) = a"; |
162 by (fast_tac (ZF_cs addIs [the_equality]) 1); |
167 by (fast_tac (ZF_cs addIs [the_equality]) 1); |
168 |
173 |
169 val major::prems = goal Nat.thy |
174 val major::prems = goal Nat.thy |
170 "[| n: nat; a: C(0); !!m. m: nat ==> b(m): C(succ(m)) \ |
175 "[| n: nat; a: C(0); !!m. m: nat ==> b(m): C(succ(m)) \ |
171 \ |] ==> nat_case(a,b,n) : C(n)"; |
176 \ |] ==> nat_case(a,b,n) : C(n)"; |
172 by (rtac (major RS nat_induct) 1); |
177 by (rtac (major RS nat_induct) 1); |
173 by (REPEAT (resolve_tac [nat_case_0 RS ssubst, |
178 by (ALLGOALS |
174 nat_case_succ RS ssubst] 1 |
179 (asm_simp_tac (ZF_ss addsimps (prems @ [nat_case_0, nat_case_succ])))); |
175 THEN resolve_tac prems 1)); |
|
176 by (assume_tac 1); |
|
177 val nat_case_type = result(); |
180 val nat_case_type = result(); |
178 |
181 |
179 |
182 |
180 (** nat_rec -- used to define eclose and transrec, then obsolete **) |
183 (** nat_rec -- used to define eclose and transrec, then obsolete; |
|
184 rec, from arith.ML, has fewer typing conditions **) |
181 |
185 |
182 val nat_rec_trans = wf_Memrel RS (nat_rec_def RS def_wfrec RS trans); |
186 val nat_rec_trans = wf_Memrel RS (nat_rec_def RS def_wfrec RS trans); |
183 |
187 |
184 goal Nat.thy "nat_rec(0,a,b) = a"; |
188 goal Nat.thy "nat_rec(0,a,b) = a"; |
185 by (rtac nat_rec_trans 1); |
189 by (rtac nat_rec_trans 1); |
193 vimage_singleton_iff]) 1); |
197 vimage_singleton_iff]) 1); |
194 val nat_rec_succ = result(); |
198 val nat_rec_succ = result(); |
195 |
199 |
196 (** The union of two natural numbers is a natural number -- their maximum **) |
200 (** The union of two natural numbers is a natural number -- their maximum **) |
197 |
201 |
198 (* [| i : nat; j : nat |] ==> i Un j : nat *) |
202 goal Nat.thy "!!i j. [| i: nat; j: nat |] ==> i Un j: nat"; |
199 val Un_nat_type = standard (Ord_nat RSN (3,Ord_member_UnI)); |
203 by (rtac (Un_least_lt RS ltD) 1); |
200 |
204 by (REPEAT (ares_tac [ltI, Ord_nat] 1)); |
201 (* [| i : nat; j : nat |] ==> i Int j : nat *) |
205 val Un_nat_type = result(); |
202 val Int_nat_type = standard (Ord_nat RSN (3,Ord_member_IntI)); |
206 |
203 |
207 goal Nat.thy "!!i j. [| i: nat; j: nat |] ==> i Int j: nat"; |
|
208 by (rtac (Int_greatest_lt RS ltD) 1); |
|
209 by (REPEAT (ares_tac [ltI, Ord_nat] 1)); |
|
210 val Int_nat_type = result(); |