author | paulson |
Tue, 18 Jun 2002 10:52:08 +0200 | |
changeset 13218 | 3732064ccbd1 |
parent 13203 | fac77a839aa2 |
child 13269 | 3ba9be497c33 |
permissions | -rw-r--r-- |
1478 | 1 |
(* Title: ZF/Nat.thy |
0 | 2 |
ID: $Id$ |
1478 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
435 | 4 |
Copyright 1994 University of Cambridge |
0 | 5 |
|
6 |
Natural numbers in Zermelo-Fraenkel Set Theory |
|
7 |
*) |
|
8 |
||
13171 | 9 |
theory Nat = OrdQuant + Bool + mono: |
0 | 10 |
|
12789 | 11 |
constdefs |
12 |
nat :: i |
|
13 |
"nat == lfp(Inf, %X. {0} Un {succ(i). i:X})" |
|
0 | 14 |
|
13173 | 15 |
(*Has an unconditional succ case, which is used in "recursor" below.*) |
12789 | 16 |
nat_case :: "[i, i=>i, i]=>i" |
17 |
"nat_case(a,b,k) == THE y. k=0 & y=a | (EX x. k=succ(x) & y=b(x))" |
|
0 | 18 |
|
13173 | 19 |
(*Slightly different from the version above. Requires k to be a |
20 |
natural number, but it has a splitting rule.*) |
|
21 |
nat_case3 :: "[i, i=>i, i]=>i" |
|
22 |
"nat_case3(a,b,k) == THE y. k=0 & y=a | (EX x:nat. k=succ(x) & y=b(x))" |
|
23 |
||
12789 | 24 |
nat_rec :: "[i, i, [i,i]=>i]=>i" |
25 |
"nat_rec(k,a,b) == |
|
1478 | 26 |
wfrec(Memrel(nat), k, %n f. nat_case(a, %m. b(m, f`m), n))" |
0 | 27 |
|
12789 | 28 |
(*Internalized relations on the naturals*) |
29 |
||
30 |
Le :: i |
|
31 |
"Le == {<x,y>:nat*nat. x le y}" |
|
32 |
||
33 |
Lt :: i |
|
34 |
"Lt == {<x, y>:nat*nat. x < y}" |
|
35 |
||
36 |
Ge :: i |
|
37 |
"Ge == {<x,y>:nat*nat. y le x}" |
|
38 |
||
39 |
Gt :: i |
|
40 |
"Gt == {<x,y>:nat*nat. y < x}" |
|
41 |
||
13171 | 42 |
less_than :: "i=>i" |
12789 | 43 |
"less_than(n) == {i:nat. i<n}" |
44 |
||
13171 | 45 |
greater_than :: "i=>i" |
12789 | 46 |
"greater_than(n) == {i:nat. n < i}" |
47 |
||
13171 | 48 |
lemma nat_bnd_mono: "bnd_mono(Inf, %X. {0} Un {succ(i). i:X})" |
49 |
apply (rule bnd_monoI) |
|
50 |
apply (cut_tac infinity, blast) |
|
51 |
apply blast |
|
52 |
done |
|
53 |
||
54 |
(* nat = {0} Un {succ(x). x:nat} *) |
|
55 |
lemmas nat_unfold = nat_bnd_mono [THEN nat_def [THEN def_lfp_unfold], standard] |
|
56 |
||
57 |
(** Type checking of 0 and successor **) |
|
58 |
||
59 |
lemma nat_0I [iff,TC]: "0 : nat" |
|
60 |
apply (subst nat_unfold) |
|
61 |
apply (rule singletonI [THEN UnI1]) |
|
62 |
done |
|
63 |
||
64 |
lemma nat_succI [intro!,TC]: "n : nat ==> succ(n) : nat" |
|
65 |
apply (subst nat_unfold) |
|
66 |
apply (erule RepFunI [THEN UnI2]) |
|
67 |
done |
|
68 |
||
69 |
lemma nat_1I [iff,TC]: "1 : nat" |
|
70 |
by (rule nat_0I [THEN nat_succI]) |
|
71 |
||
72 |
lemma nat_2I [iff,TC]: "2 : nat" |
|
73 |
by (rule nat_1I [THEN nat_succI]) |
|
74 |
||
75 |
lemma bool_subset_nat: "bool <= nat" |
|
76 |
by (blast elim!: boolE) |
|
77 |
||
78 |
lemmas bool_into_nat = bool_subset_nat [THEN subsetD, standard] |
|
79 |
||
80 |
||
81 |
(** Injectivity properties and induction **) |
|
82 |
||
83 |
(*Mathematical induction*) |
|
84 |
lemma nat_induct: |
|
85 |
"[| n: nat; P(0); !!x. [| x: nat; P(x) |] ==> P(succ(x)) |] ==> P(n)" |
|
13203
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset
|
86 |
by (erule def_induct [OF nat_def nat_bnd_mono], blast) |
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset
|
87 |
|
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset
|
88 |
(*fixed up for induct method*) |
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset
|
89 |
lemmas nat_induct = nat_induct [case_names 0 succ, induct set: nat] |
13171 | 90 |
|
91 |
lemma natE: |
|
92 |
"[| n: nat; n=0 ==> P; !!x. [| x: nat; n=succ(x) |] ==> P |] ==> P" |
|
13203
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset
|
93 |
by (erule nat_unfold [THEN equalityD1, THEN subsetD, THEN UnE], auto) |
13171 | 94 |
|
95 |
lemma nat_into_Ord [simp]: "n: nat ==> Ord(n)" |
|
96 |
by (erule nat_induct, auto) |
|
97 |
||
98 |
(* i: nat ==> 0 le i; same thing as 0<succ(i) *) |
|
99 |
lemmas nat_0_le = nat_into_Ord [THEN Ord_0_le, standard] |
|
100 |
||
101 |
(* i: nat ==> i le i; same thing as i<succ(i) *) |
|
102 |
lemmas nat_le_refl = nat_into_Ord [THEN le_refl, standard] |
|
103 |
||
104 |
lemma Ord_nat [iff]: "Ord(nat)" |
|
105 |
apply (rule OrdI) |
|
106 |
apply (erule_tac [2] nat_into_Ord [THEN Ord_is_Transset]) |
|
107 |
apply (unfold Transset_def) |
|
108 |
apply (rule ballI) |
|
109 |
apply (erule nat_induct, auto) |
|
110 |
done |
|
111 |
||
112 |
lemma Limit_nat [iff]: "Limit(nat)" |
|
113 |
apply (unfold Limit_def) |
|
114 |
apply (safe intro!: ltI Ord_nat) |
|
115 |
apply (erule ltD) |
|
116 |
done |
|
117 |
||
118 |
lemma succ_natD [dest!]: "succ(i): nat ==> i: nat" |
|
119 |
by (rule Ord_trans [OF succI1], auto) |
|
120 |
||
121 |
lemma nat_succ_iff [iff]: "succ(n): nat <-> n: nat" |
|
122 |
by blast |
|
123 |
||
124 |
lemma nat_le_Limit: "Limit(i) ==> nat le i" |
|
125 |
apply (rule subset_imp_le) |
|
126 |
apply (simp_all add: Limit_is_Ord) |
|
127 |
apply (rule subsetI) |
|
128 |
apply (erule nat_induct) |
|
129 |
apply (erule Limit_has_0 [THEN ltD]) |
|
130 |
apply (blast intro: Limit_has_succ [THEN ltD] ltI Limit_is_Ord) |
|
131 |
done |
|
132 |
||
133 |
(* [| succ(i): k; k: nat |] ==> i: k *) |
|
134 |
lemmas succ_in_naturalD = Ord_trans [OF succI1 _ nat_into_Ord] |
|
135 |
||
136 |
lemma lt_nat_in_nat: "[| m<n; n: nat |] ==> m: nat" |
|
137 |
apply (erule ltE) |
|
138 |
apply (erule Ord_trans, assumption) |
|
139 |
apply simp |
|
140 |
done |
|
141 |
||
142 |
lemma le_in_nat: "[| m le n; n:nat |] ==> m:nat" |
|
143 |
by (blast dest!: lt_nat_in_nat) |
|
144 |
||
145 |
||
146 |
(** Variations on mathematical induction **) |
|
147 |
||
148 |
(*complete induction*) |
|
13203
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset
|
149 |
|
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset
|
150 |
lemmas complete_induct = Ord_induct [OF _ Ord_nat, case_names less, consumes 1] |
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset
|
151 |
|
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset
|
152 |
lemmas complete_induct_rule = |
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset
|
153 |
complete_induct [rule_format, case_names less, consumes 1] |
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset
|
154 |
|
13171 | 155 |
|
156 |
lemma nat_induct_from_lemma [rule_format]: |
|
157 |
"[| n: nat; m: nat; |
|
158 |
!!x. [| x: nat; m le x; P(x) |] ==> P(succ(x)) |] |
|
159 |
==> m le n --> P(m) --> P(n)" |
|
160 |
apply (erule nat_induct) |
|
161 |
apply (simp_all add: distrib_simps le0_iff le_succ_iff) |
|
162 |
done |
|
163 |
||
164 |
(*Induction starting from m rather than 0*) |
|
165 |
lemma nat_induct_from: |
|
166 |
"[| m le n; m: nat; n: nat; |
|
167 |
P(m); |
|
168 |
!!x. [| x: nat; m le x; P(x) |] ==> P(succ(x)) |] |
|
169 |
==> P(n)" |
|
170 |
apply (blast intro: nat_induct_from_lemma) |
|
171 |
done |
|
172 |
||
173 |
(*Induction suitable for subtraction and less-than*) |
|
174 |
lemma diff_induct: |
|
175 |
"[| m: nat; n: nat; |
|
176 |
!!x. x: nat ==> P(x,0); |
|
177 |
!!y. y: nat ==> P(0,succ(y)); |
|
178 |
!!x y. [| x: nat; y: nat; P(x,y) |] ==> P(succ(x),succ(y)) |] |
|
179 |
==> P(m,n)" |
|
180 |
apply (erule_tac x = "m" in rev_bspec) |
|
181 |
apply (erule nat_induct, simp) |
|
182 |
apply (rule ballI) |
|
183 |
apply (rename_tac i j) |
|
184 |
apply (erule_tac n=j in nat_induct, auto) |
|
185 |
done |
|
186 |
||
13203
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset
|
187 |
(*fixed up for induct method*) |
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset
|
188 |
lemmas diff_induct = diff_induct [case_names 0 0_succ succ_succ, consumes 2] |
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset
|
189 |
|
13171 | 190 |
(** Induction principle analogous to trancl_induct **) |
191 |
||
192 |
lemma succ_lt_induct_lemma [rule_format]: |
|
193 |
"m: nat ==> P(m,succ(m)) --> (ALL x: nat. P(m,x) --> P(m,succ(x))) --> |
|
194 |
(ALL n:nat. m<n --> P(m,n))" |
|
195 |
apply (erule nat_induct) |
|
196 |
apply (intro impI, rule nat_induct [THEN ballI]) |
|
197 |
prefer 4 apply (intro impI, rule nat_induct [THEN ballI]) |
|
198 |
apply (auto simp add: le_iff) |
|
199 |
done |
|
200 |
||
201 |
lemma succ_lt_induct: |
|
202 |
"[| m<n; n: nat; |
|
203 |
P(m,succ(m)); |
|
204 |
!!x. [| x: nat; P(m,x) |] ==> P(m,succ(x)) |] |
|
205 |
==> P(m,n)" |
|
206 |
by (blast intro: succ_lt_induct_lemma lt_nat_in_nat) |
|
207 |
||
208 |
(** nat_case **) |
|
209 |
||
210 |
lemma nat_case_0 [simp]: "nat_case(a,b,0) = a" |
|
13174 | 211 |
by (simp add: nat_case_def) |
13173 | 212 |
|
213 |
lemma nat_case_succ [simp]: "nat_case(a,b,succ(n)) = b(n)" |
|
13174 | 214 |
by (simp add: nat_case_def) |
13171 | 215 |
|
13173 | 216 |
lemma nat_case_type [TC]: |
217 |
"[| n: nat; a: C(0); !!m. m: nat ==> b(m): C(succ(m)) |] |
|
218 |
==> nat_case(a,b,n) : C(n)"; |
|
219 |
by (erule nat_induct, auto) |
|
220 |
||
221 |
(** nat_case3 **) |
|
222 |
||
223 |
lemma nat_case3_0 [simp]: "nat_case3(a,b,0) = a" |
|
13174 | 224 |
by (simp add: nat_case3_def) |
13173 | 225 |
|
226 |
lemma nat_case3_succ [simp]: "n\<in>nat \<Longrightarrow> nat_case3(a,b,succ(n)) = b(n)" |
|
13174 | 227 |
by (simp add: nat_case3_def) |
13171 | 228 |
|
13173 | 229 |
lemma non_nat_case3: "x\<notin>nat \<Longrightarrow> nat_case3(a,b,x) = 0" |
230 |
apply (simp add: nat_case3_def) |
|
231 |
apply (blast intro: the_0) |
|
13171 | 232 |
done |
233 |
||
13173 | 234 |
lemma split_nat_case3: |
235 |
"P(nat_case3(a,b,k)) <-> |
|
236 |
((k=0 --> P(a)) & (\<forall>x\<in>nat. k=succ(x) --> P(b(x))) & (k \<notin> nat \<longrightarrow> P(0)))" |
|
237 |
apply (rule_tac P="k\<in>nat" in case_split_thm) |
|
238 |
(*case_tac method not available yet; needs "inductive"*) |
|
239 |
apply (erule natE) |
|
240 |
apply (auto simp add: non_nat_case3) |
|
241 |
done |
|
242 |
||
243 |
lemma nat_case3_type [TC]: |
|
244 |
"[| n: nat; a: C(0); !!m. m: nat ==> b(m): C(succ(m)) |] |
|
245 |
==> nat_case3(a,b,n) : C(n)"; |
|
246 |
by (erule nat_induct, auto) |
|
247 |
||
13171 | 248 |
|
249 |
(** nat_rec -- used to define eclose and transrec, then obsolete |
|
250 |
rec, from arith.ML, has fewer typing conditions **) |
|
251 |
||
252 |
lemma nat_rec_0: "nat_rec(0,a,b) = a" |
|
253 |
apply (rule nat_rec_def [THEN def_wfrec, THEN trans]) |
|
254 |
apply (rule wf_Memrel) |
|
255 |
apply (rule nat_case_0) |
|
256 |
done |
|
257 |
||
258 |
lemma nat_rec_succ: "m: nat ==> nat_rec(succ(m),a,b) = b(m, nat_rec(m,a,b))" |
|
259 |
apply (rule nat_rec_def [THEN def_wfrec, THEN trans]) |
|
260 |
apply (rule wf_Memrel) |
|
261 |
apply (simp add: vimage_singleton_iff) |
|
262 |
done |
|
263 |
||
264 |
(** The union of two natural numbers is a natural number -- their maximum **) |
|
265 |
||
13173 | 266 |
lemma Un_nat_type [TC]: "[| i: nat; j: nat |] ==> i Un j: nat" |
13171 | 267 |
apply (rule Un_least_lt [THEN ltD]) |
268 |
apply (simp_all add: lt_def) |
|
269 |
done |
|
270 |
||
13173 | 271 |
lemma Int_nat_type [TC]: "[| i: nat; j: nat |] ==> i Int j: nat" |
13171 | 272 |
apply (rule Int_greatest_lt [THEN ltD]) |
273 |
apply (simp_all add: lt_def) |
|
274 |
done |
|
275 |
||
276 |
(*needed to simplify unions over nat*) |
|
277 |
lemma nat_nonempty [simp]: "nat ~= 0" |
|
278 |
by blast |
|
279 |
||
13203
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13185
diff
changeset
|
280 |
|
13171 | 281 |
ML |
282 |
{* |
|
283 |
val Le_def = thm "Le_def"; |
|
284 |
val Lt_def = thm "Lt_def"; |
|
285 |
val Ge_def = thm "Ge_def"; |
|
286 |
val Gt_def = thm "Gt_def"; |
|
287 |
val less_than_def = thm "less_than_def"; |
|
288 |
val greater_than_def = thm "greater_than_def"; |
|
289 |
||
290 |
val nat_bnd_mono = thm "nat_bnd_mono"; |
|
291 |
val nat_unfold = thm "nat_unfold"; |
|
292 |
val nat_0I = thm "nat_0I"; |
|
293 |
val nat_succI = thm "nat_succI"; |
|
294 |
val nat_1I = thm "nat_1I"; |
|
295 |
val nat_2I = thm "nat_2I"; |
|
296 |
val bool_subset_nat = thm "bool_subset_nat"; |
|
297 |
val bool_into_nat = thm "bool_into_nat"; |
|
298 |
val nat_induct = thm "nat_induct"; |
|
299 |
val natE = thm "natE"; |
|
300 |
val nat_into_Ord = thm "nat_into_Ord"; |
|
301 |
val nat_0_le = thm "nat_0_le"; |
|
302 |
val nat_le_refl = thm "nat_le_refl"; |
|
303 |
val Ord_nat = thm "Ord_nat"; |
|
304 |
val Limit_nat = thm "Limit_nat"; |
|
305 |
val succ_natD = thm "succ_natD"; |
|
306 |
val nat_succ_iff = thm "nat_succ_iff"; |
|
307 |
val nat_le_Limit = thm "nat_le_Limit"; |
|
308 |
val succ_in_naturalD = thm "succ_in_naturalD"; |
|
309 |
val lt_nat_in_nat = thm "lt_nat_in_nat"; |
|
310 |
val le_in_nat = thm "le_in_nat"; |
|
311 |
val complete_induct = thm "complete_induct"; |
|
312 |
val nat_induct_from = thm "nat_induct_from"; |
|
313 |
val diff_induct = thm "diff_induct"; |
|
314 |
val succ_lt_induct = thm "succ_lt_induct"; |
|
315 |
val nat_case_0 = thm "nat_case_0"; |
|
316 |
val nat_case_succ = thm "nat_case_succ"; |
|
317 |
val nat_case_type = thm "nat_case_type"; |
|
318 |
val nat_rec_0 = thm "nat_rec_0"; |
|
319 |
val nat_rec_succ = thm "nat_rec_succ"; |
|
320 |
val Un_nat_type = thm "Un_nat_type"; |
|
321 |
val Int_nat_type = thm "Int_nat_type"; |
|
322 |
val nat_nonempty = thm "nat_nonempty"; |
|
323 |
*} |
|
324 |
||
0 | 325 |
end |