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)"
|
|
86 |
apply (erule def_induct [OF nat_def nat_bnd_mono], blast)
|
|
87 |
done
|
|
88 |
|
|
89 |
lemma natE:
|
|
90 |
"[| n: nat; n=0 ==> P; !!x. [| x: nat; n=succ(x) |] ==> P |] ==> P"
|
|
91 |
apply (erule nat_unfold [THEN equalityD1, THEN subsetD, THEN UnE], auto)
|
|
92 |
done
|
|
93 |
|
|
94 |
lemma nat_into_Ord [simp]: "n: nat ==> Ord(n)"
|
|
95 |
by (erule nat_induct, auto)
|
|
96 |
|
|
97 |
(* i: nat ==> 0 le i; same thing as 0<succ(i) *)
|
|
98 |
lemmas nat_0_le = nat_into_Ord [THEN Ord_0_le, standard]
|
|
99 |
|
|
100 |
(* i: nat ==> i le i; same thing as i<succ(i) *)
|
|
101 |
lemmas nat_le_refl = nat_into_Ord [THEN le_refl, standard]
|
|
102 |
|
|
103 |
lemma Ord_nat [iff]: "Ord(nat)"
|
|
104 |
apply (rule OrdI)
|
|
105 |
apply (erule_tac [2] nat_into_Ord [THEN Ord_is_Transset])
|
|
106 |
apply (unfold Transset_def)
|
|
107 |
apply (rule ballI)
|
|
108 |
apply (erule nat_induct, auto)
|
|
109 |
done
|
|
110 |
|
|
111 |
lemma Limit_nat [iff]: "Limit(nat)"
|
|
112 |
apply (unfold Limit_def)
|
|
113 |
apply (safe intro!: ltI Ord_nat)
|
|
114 |
apply (erule ltD)
|
|
115 |
done
|
|
116 |
|
|
117 |
lemma succ_natD [dest!]: "succ(i): nat ==> i: nat"
|
|
118 |
by (rule Ord_trans [OF succI1], auto)
|
|
119 |
|
|
120 |
lemma nat_succ_iff [iff]: "succ(n): nat <-> n: nat"
|
|
121 |
by blast
|
|
122 |
|
|
123 |
lemma nat_le_Limit: "Limit(i) ==> nat le i"
|
|
124 |
apply (rule subset_imp_le)
|
|
125 |
apply (simp_all add: Limit_is_Ord)
|
|
126 |
apply (rule subsetI)
|
|
127 |
apply (erule nat_induct)
|
|
128 |
apply (erule Limit_has_0 [THEN ltD])
|
|
129 |
apply (blast intro: Limit_has_succ [THEN ltD] ltI Limit_is_Ord)
|
|
130 |
done
|
|
131 |
|
|
132 |
(* [| succ(i): k; k: nat |] ==> i: k *)
|
|
133 |
lemmas succ_in_naturalD = Ord_trans [OF succI1 _ nat_into_Ord]
|
|
134 |
|
|
135 |
lemma lt_nat_in_nat: "[| m<n; n: nat |] ==> m: nat"
|
|
136 |
apply (erule ltE)
|
|
137 |
apply (erule Ord_trans, assumption)
|
|
138 |
apply simp
|
|
139 |
done
|
|
140 |
|
|
141 |
lemma le_in_nat: "[| m le n; n:nat |] ==> m:nat"
|
|
142 |
by (blast dest!: lt_nat_in_nat)
|
|
143 |
|
|
144 |
|
|
145 |
(** Variations on mathematical induction **)
|
|
146 |
|
|
147 |
(*complete induction*)
|
|
148 |
lemmas complete_induct = Ord_induct [OF _ Ord_nat]
|
|
149 |
|
|
150 |
lemma nat_induct_from_lemma [rule_format]:
|
|
151 |
"[| n: nat; m: nat;
|
|
152 |
!!x. [| x: nat; m le x; P(x) |] ==> P(succ(x)) |]
|
|
153 |
==> m le n --> P(m) --> P(n)"
|
|
154 |
apply (erule nat_induct)
|
|
155 |
apply (simp_all add: distrib_simps le0_iff le_succ_iff)
|
|
156 |
done
|
|
157 |
|
|
158 |
(*Induction starting from m rather than 0*)
|
|
159 |
lemma nat_induct_from:
|
|
160 |
"[| m le n; m: nat; n: nat;
|
|
161 |
P(m);
|
|
162 |
!!x. [| x: nat; m le x; P(x) |] ==> P(succ(x)) |]
|
|
163 |
==> P(n)"
|
|
164 |
apply (blast intro: nat_induct_from_lemma)
|
|
165 |
done
|
|
166 |
|
|
167 |
(*Induction suitable for subtraction and less-than*)
|
|
168 |
lemma diff_induct:
|
|
169 |
"[| m: nat; n: nat;
|
|
170 |
!!x. x: nat ==> P(x,0);
|
|
171 |
!!y. y: nat ==> P(0,succ(y));
|
|
172 |
!!x y. [| x: nat; y: nat; P(x,y) |] ==> P(succ(x),succ(y)) |]
|
|
173 |
==> P(m,n)"
|
|
174 |
apply (erule_tac x = "m" in rev_bspec)
|
|
175 |
apply (erule nat_induct, simp)
|
|
176 |
apply (rule ballI)
|
|
177 |
apply (rename_tac i j)
|
|
178 |
apply (erule_tac n=j in nat_induct, auto)
|
|
179 |
done
|
|
180 |
|
|
181 |
(** Induction principle analogous to trancl_induct **)
|
|
182 |
|
|
183 |
lemma succ_lt_induct_lemma [rule_format]:
|
|
184 |
"m: nat ==> P(m,succ(m)) --> (ALL x: nat. P(m,x) --> P(m,succ(x))) -->
|
|
185 |
(ALL n:nat. m<n --> P(m,n))"
|
|
186 |
apply (erule nat_induct)
|
|
187 |
apply (intro impI, rule nat_induct [THEN ballI])
|
|
188 |
prefer 4 apply (intro impI, rule nat_induct [THEN ballI])
|
|
189 |
apply (auto simp add: le_iff)
|
|
190 |
done
|
|
191 |
|
|
192 |
lemma succ_lt_induct:
|
|
193 |
"[| m<n; n: nat;
|
|
194 |
P(m,succ(m));
|
|
195 |
!!x. [| x: nat; P(m,x) |] ==> P(m,succ(x)) |]
|
|
196 |
==> P(m,n)"
|
|
197 |
by (blast intro: succ_lt_induct_lemma lt_nat_in_nat)
|
|
198 |
|
|
199 |
(** nat_case **)
|
|
200 |
|
|
201 |
lemma nat_case_0 [simp]: "nat_case(a,b,0) = a"
|
13174
|
202 |
by (simp add: nat_case_def)
|
13173
|
203 |
|
|
204 |
lemma nat_case_succ [simp]: "nat_case(a,b,succ(n)) = b(n)"
|
13174
|
205 |
by (simp add: nat_case_def)
|
13171
|
206 |
|
13173
|
207 |
lemma nat_case_type [TC]:
|
|
208 |
"[| n: nat; a: C(0); !!m. m: nat ==> b(m): C(succ(m)) |]
|
|
209 |
==> nat_case(a,b,n) : C(n)";
|
|
210 |
by (erule nat_induct, auto)
|
|
211 |
|
|
212 |
(** nat_case3 **)
|
|
213 |
|
|
214 |
lemma nat_case3_0 [simp]: "nat_case3(a,b,0) = a"
|
13174
|
215 |
by (simp add: nat_case3_def)
|
13173
|
216 |
|
|
217 |
lemma nat_case3_succ [simp]: "n\<in>nat \<Longrightarrow> nat_case3(a,b,succ(n)) = b(n)"
|
13174
|
218 |
by (simp add: nat_case3_def)
|
13171
|
219 |
|
13173
|
220 |
lemma non_nat_case3: "x\<notin>nat \<Longrightarrow> nat_case3(a,b,x) = 0"
|
|
221 |
apply (simp add: nat_case3_def)
|
|
222 |
apply (blast intro: the_0)
|
13171
|
223 |
done
|
|
224 |
|
13173
|
225 |
lemma split_nat_case3:
|
|
226 |
"P(nat_case3(a,b,k)) <->
|
|
227 |
((k=0 --> P(a)) & (\<forall>x\<in>nat. k=succ(x) --> P(b(x))) & (k \<notin> nat \<longrightarrow> P(0)))"
|
|
228 |
apply (rule_tac P="k\<in>nat" in case_split_thm)
|
|
229 |
(*case_tac method not available yet; needs "inductive"*)
|
|
230 |
apply (erule natE)
|
|
231 |
apply (auto simp add: non_nat_case3)
|
|
232 |
done
|
|
233 |
|
|
234 |
lemma nat_case3_type [TC]:
|
|
235 |
"[| n: nat; a: C(0); !!m. m: nat ==> b(m): C(succ(m)) |]
|
|
236 |
==> nat_case3(a,b,n) : C(n)";
|
|
237 |
by (erule nat_induct, auto)
|
|
238 |
|
13171
|
239 |
|
|
240 |
(** nat_rec -- used to define eclose and transrec, then obsolete
|
|
241 |
rec, from arith.ML, has fewer typing conditions **)
|
|
242 |
|
|
243 |
lemma nat_rec_0: "nat_rec(0,a,b) = a"
|
|
244 |
apply (rule nat_rec_def [THEN def_wfrec, THEN trans])
|
|
245 |
apply (rule wf_Memrel)
|
|
246 |
apply (rule nat_case_0)
|
|
247 |
done
|
|
248 |
|
|
249 |
lemma nat_rec_succ: "m: nat ==> nat_rec(succ(m),a,b) = b(m, nat_rec(m,a,b))"
|
|
250 |
apply (rule nat_rec_def [THEN def_wfrec, THEN trans])
|
|
251 |
apply (rule wf_Memrel)
|
|
252 |
apply (simp add: vimage_singleton_iff)
|
|
253 |
done
|
|
254 |
|
|
255 |
(** The union of two natural numbers is a natural number -- their maximum **)
|
|
256 |
|
13173
|
257 |
lemma Un_nat_type [TC]: "[| i: nat; j: nat |] ==> i Un j: nat"
|
13171
|
258 |
apply (rule Un_least_lt [THEN ltD])
|
|
259 |
apply (simp_all add: lt_def)
|
|
260 |
done
|
|
261 |
|
13173
|
262 |
lemma Int_nat_type [TC]: "[| i: nat; j: nat |] ==> i Int j: nat"
|
13171
|
263 |
apply (rule Int_greatest_lt [THEN ltD])
|
|
264 |
apply (simp_all add: lt_def)
|
|
265 |
done
|
|
266 |
|
|
267 |
(*needed to simplify unions over nat*)
|
|
268 |
lemma nat_nonempty [simp]: "nat ~= 0"
|
|
269 |
by blast
|
|
270 |
|
|
271 |
ML
|
|
272 |
{*
|
|
273 |
val Le_def = thm "Le_def";
|
|
274 |
val Lt_def = thm "Lt_def";
|
|
275 |
val Ge_def = thm "Ge_def";
|
|
276 |
val Gt_def = thm "Gt_def";
|
|
277 |
val less_than_def = thm "less_than_def";
|
|
278 |
val greater_than_def = thm "greater_than_def";
|
|
279 |
|
|
280 |
val nat_bnd_mono = thm "nat_bnd_mono";
|
|
281 |
val nat_unfold = thm "nat_unfold";
|
|
282 |
val nat_0I = thm "nat_0I";
|
|
283 |
val nat_succI = thm "nat_succI";
|
|
284 |
val nat_1I = thm "nat_1I";
|
|
285 |
val nat_2I = thm "nat_2I";
|
|
286 |
val bool_subset_nat = thm "bool_subset_nat";
|
|
287 |
val bool_into_nat = thm "bool_into_nat";
|
|
288 |
val nat_induct = thm "nat_induct";
|
|
289 |
val natE = thm "natE";
|
|
290 |
val nat_into_Ord = thm "nat_into_Ord";
|
|
291 |
val nat_0_le = thm "nat_0_le";
|
|
292 |
val nat_le_refl = thm "nat_le_refl";
|
|
293 |
val Ord_nat = thm "Ord_nat";
|
|
294 |
val Limit_nat = thm "Limit_nat";
|
|
295 |
val succ_natD = thm "succ_natD";
|
|
296 |
val nat_succ_iff = thm "nat_succ_iff";
|
|
297 |
val nat_le_Limit = thm "nat_le_Limit";
|
|
298 |
val succ_in_naturalD = thm "succ_in_naturalD";
|
|
299 |
val lt_nat_in_nat = thm "lt_nat_in_nat";
|
|
300 |
val le_in_nat = thm "le_in_nat";
|
|
301 |
val complete_induct = thm "complete_induct";
|
|
302 |
val nat_induct_from_lemma = thm "nat_induct_from_lemma";
|
|
303 |
val nat_induct_from = thm "nat_induct_from";
|
|
304 |
val diff_induct = thm "diff_induct";
|
|
305 |
val succ_lt_induct_lemma = thm "succ_lt_induct_lemma";
|
|
306 |
val succ_lt_induct = thm "succ_lt_induct";
|
|
307 |
val nat_case_0 = thm "nat_case_0";
|
|
308 |
val nat_case_succ = thm "nat_case_succ";
|
|
309 |
val nat_case_type = thm "nat_case_type";
|
|
310 |
val nat_rec_0 = thm "nat_rec_0";
|
|
311 |
val nat_rec_succ = thm "nat_rec_succ";
|
|
312 |
val Un_nat_type = thm "Un_nat_type";
|
|
313 |
val Int_nat_type = thm "Int_nat_type";
|
|
314 |
val nat_nonempty = thm "nat_nonempty";
|
|
315 |
*}
|
|
316 |
|
0
|
317 |
end
|