31 "Ge == {<x,y>:nat*nat. y le x}" |
31 "Ge == {<x,y>:nat*nat. y le x}" |
32 |
32 |
33 Gt :: i |
33 Gt :: i |
34 "Gt == {<x,y>:nat*nat. y < x}" |
34 "Gt == {<x,y>:nat*nat. y < x}" |
35 |
35 |
36 less_than :: i=>i |
36 less_than :: "i=>i" |
37 "less_than(n) == {i:nat. i<n}" |
37 "less_than(n) == {i:nat. i<n}" |
38 |
38 |
39 greater_than :: i=>i |
39 greater_than :: "i=>i" |
40 "greater_than(n) == {i:nat. n < i}" |
40 "greater_than(n) == {i:nat. n < i}" |
41 |
41 |
|
42 lemma nat_bnd_mono: "bnd_mono(Inf, %X. {0} Un {succ(i). i:X})" |
|
43 apply (rule bnd_monoI) |
|
44 apply (cut_tac infinity, blast) |
|
45 apply blast |
|
46 done |
|
47 |
|
48 (* nat = {0} Un {succ(x). x:nat} *) |
|
49 lemmas nat_unfold = nat_bnd_mono [THEN nat_def [THEN def_lfp_unfold], standard] |
|
50 |
|
51 (** Type checking of 0 and successor **) |
|
52 |
|
53 lemma nat_0I [iff,TC]: "0 : nat" |
|
54 apply (subst nat_unfold) |
|
55 apply (rule singletonI [THEN UnI1]) |
|
56 done |
|
57 |
|
58 lemma nat_succI [intro!,TC]: "n : nat ==> succ(n) : nat" |
|
59 apply (subst nat_unfold) |
|
60 apply (erule RepFunI [THEN UnI2]) |
|
61 done |
|
62 |
|
63 lemma nat_1I [iff,TC]: "1 : nat" |
|
64 by (rule nat_0I [THEN nat_succI]) |
|
65 |
|
66 lemma nat_2I [iff,TC]: "2 : nat" |
|
67 by (rule nat_1I [THEN nat_succI]) |
|
68 |
|
69 lemma bool_subset_nat: "bool <= nat" |
|
70 by (blast elim!: boolE) |
|
71 |
|
72 lemmas bool_into_nat = bool_subset_nat [THEN subsetD, standard] |
|
73 |
|
74 |
|
75 (** Injectivity properties and induction **) |
|
76 |
|
77 (*Mathematical induction*) |
|
78 lemma nat_induct: |
|
79 "[| n: nat; P(0); !!x. [| x: nat; P(x) |] ==> P(succ(x)) |] ==> P(n)" |
|
80 apply (erule def_induct [OF nat_def nat_bnd_mono], blast) |
|
81 done |
|
82 |
|
83 lemma natE: |
|
84 "[| n: nat; n=0 ==> P; !!x. [| x: nat; n=succ(x) |] ==> P |] ==> P" |
|
85 apply (erule nat_unfold [THEN equalityD1, THEN subsetD, THEN UnE], auto) |
|
86 done |
|
87 |
|
88 lemma nat_into_Ord [simp]: "n: nat ==> Ord(n)" |
|
89 by (erule nat_induct, auto) |
|
90 |
|
91 (* i: nat ==> 0 le i; same thing as 0<succ(i) *) |
|
92 lemmas nat_0_le = nat_into_Ord [THEN Ord_0_le, standard] |
|
93 |
|
94 (* i: nat ==> i le i; same thing as i<succ(i) *) |
|
95 lemmas nat_le_refl = nat_into_Ord [THEN le_refl, standard] |
|
96 |
|
97 lemma Ord_nat [iff]: "Ord(nat)" |
|
98 apply (rule OrdI) |
|
99 apply (erule_tac [2] nat_into_Ord [THEN Ord_is_Transset]) |
|
100 apply (unfold Transset_def) |
|
101 apply (rule ballI) |
|
102 apply (erule nat_induct, auto) |
|
103 done |
|
104 |
|
105 lemma Limit_nat [iff]: "Limit(nat)" |
|
106 apply (unfold Limit_def) |
|
107 apply (safe intro!: ltI Ord_nat) |
|
108 apply (erule ltD) |
|
109 done |
|
110 |
|
111 lemma succ_natD [dest!]: "succ(i): nat ==> i: nat" |
|
112 by (rule Ord_trans [OF succI1], auto) |
|
113 |
|
114 lemma nat_succ_iff [iff]: "succ(n): nat <-> n: nat" |
|
115 by blast |
|
116 |
|
117 lemma nat_le_Limit: "Limit(i) ==> nat le i" |
|
118 apply (rule subset_imp_le) |
|
119 apply (simp_all add: Limit_is_Ord) |
|
120 apply (rule subsetI) |
|
121 apply (erule nat_induct) |
|
122 apply (erule Limit_has_0 [THEN ltD]) |
|
123 apply (blast intro: Limit_has_succ [THEN ltD] ltI Limit_is_Ord) |
|
124 done |
|
125 |
|
126 (* [| succ(i): k; k: nat |] ==> i: k *) |
|
127 lemmas succ_in_naturalD = Ord_trans [OF succI1 _ nat_into_Ord] |
|
128 |
|
129 lemma lt_nat_in_nat: "[| m<n; n: nat |] ==> m: nat" |
|
130 apply (erule ltE) |
|
131 apply (erule Ord_trans, assumption) |
|
132 apply simp |
|
133 done |
|
134 |
|
135 lemma le_in_nat: "[| m le n; n:nat |] ==> m:nat" |
|
136 by (blast dest!: lt_nat_in_nat) |
|
137 |
|
138 |
|
139 (** Variations on mathematical induction **) |
|
140 |
|
141 (*complete induction*) |
|
142 lemmas complete_induct = Ord_induct [OF _ Ord_nat] |
|
143 |
|
144 lemma nat_induct_from_lemma [rule_format]: |
|
145 "[| n: nat; m: nat; |
|
146 !!x. [| x: nat; m le x; P(x) |] ==> P(succ(x)) |] |
|
147 ==> m le n --> P(m) --> P(n)" |
|
148 apply (erule nat_induct) |
|
149 apply (simp_all add: distrib_simps le0_iff le_succ_iff) |
|
150 done |
|
151 |
|
152 (*Induction starting from m rather than 0*) |
|
153 lemma nat_induct_from: |
|
154 "[| m le n; m: nat; n: nat; |
|
155 P(m); |
|
156 !!x. [| x: nat; m le x; P(x) |] ==> P(succ(x)) |] |
|
157 ==> P(n)" |
|
158 apply (blast intro: nat_induct_from_lemma) |
|
159 done |
|
160 |
|
161 (*Induction suitable for subtraction and less-than*) |
|
162 lemma diff_induct: |
|
163 "[| m: nat; n: nat; |
|
164 !!x. x: nat ==> P(x,0); |
|
165 !!y. y: nat ==> P(0,succ(y)); |
|
166 !!x y. [| x: nat; y: nat; P(x,y) |] ==> P(succ(x),succ(y)) |] |
|
167 ==> P(m,n)" |
|
168 apply (erule_tac x = "m" in rev_bspec) |
|
169 apply (erule nat_induct, simp) |
|
170 apply (rule ballI) |
|
171 apply (rename_tac i j) |
|
172 apply (erule_tac n=j in nat_induct, auto) |
|
173 done |
|
174 |
|
175 (** Induction principle analogous to trancl_induct **) |
|
176 |
|
177 lemma succ_lt_induct_lemma [rule_format]: |
|
178 "m: nat ==> P(m,succ(m)) --> (ALL x: nat. P(m,x) --> P(m,succ(x))) --> |
|
179 (ALL n:nat. m<n --> P(m,n))" |
|
180 apply (erule nat_induct) |
|
181 apply (intro impI, rule nat_induct [THEN ballI]) |
|
182 prefer 4 apply (intro impI, rule nat_induct [THEN ballI]) |
|
183 apply (auto simp add: le_iff) |
|
184 done |
|
185 |
|
186 lemma succ_lt_induct: |
|
187 "[| m<n; n: nat; |
|
188 P(m,succ(m)); |
|
189 !!x. [| x: nat; P(m,x) |] ==> P(m,succ(x)) |] |
|
190 ==> P(m,n)" |
|
191 by (blast intro: succ_lt_induct_lemma lt_nat_in_nat) |
|
192 |
|
193 (** nat_case **) |
|
194 |
|
195 lemma nat_case_0 [simp]: "nat_case(a,b,0) = a" |
|
196 by (unfold nat_case_def, blast) |
|
197 |
|
198 lemma nat_case_succ [simp]: "nat_case(a,b,succ(m)) = b(m)" |
|
199 by (unfold nat_case_def, blast) |
|
200 |
|
201 lemma nat_case_type: |
|
202 "[| n: nat; a: C(0); !!m. m: nat ==> b(m): C(succ(m)) |] |
|
203 ==> nat_case(a,b,n) : C(n)" |
|
204 apply (erule nat_induct, auto) |
|
205 done |
|
206 |
|
207 |
|
208 (** nat_rec -- used to define eclose and transrec, then obsolete |
|
209 rec, from arith.ML, has fewer typing conditions **) |
|
210 |
|
211 lemma nat_rec_0: "nat_rec(0,a,b) = a" |
|
212 apply (rule nat_rec_def [THEN def_wfrec, THEN trans]) |
|
213 apply (rule wf_Memrel) |
|
214 apply (rule nat_case_0) |
|
215 done |
|
216 |
|
217 lemma nat_rec_succ: "m: nat ==> nat_rec(succ(m),a,b) = b(m, nat_rec(m,a,b))" |
|
218 apply (rule nat_rec_def [THEN def_wfrec, THEN trans]) |
|
219 apply (rule wf_Memrel) |
|
220 apply (simp add: vimage_singleton_iff) |
|
221 done |
|
222 |
|
223 (** The union of two natural numbers is a natural number -- their maximum **) |
|
224 |
|
225 lemma Un_nat_type: "[| i: nat; j: nat |] ==> i Un j: nat" |
|
226 apply (rule Un_least_lt [THEN ltD]) |
|
227 apply (simp_all add: lt_def) |
|
228 done |
|
229 |
|
230 lemma Int_nat_type: "[| i: nat; j: nat |] ==> i Int j: nat" |
|
231 apply (rule Int_greatest_lt [THEN ltD]) |
|
232 apply (simp_all add: lt_def) |
|
233 done |
|
234 |
|
235 (*needed to simplify unions over nat*) |
|
236 lemma nat_nonempty [simp]: "nat ~= 0" |
|
237 by blast |
|
238 |
|
239 ML |
|
240 {* |
|
241 val Le_def = thm "Le_def"; |
|
242 val Lt_def = thm "Lt_def"; |
|
243 val Ge_def = thm "Ge_def"; |
|
244 val Gt_def = thm "Gt_def"; |
|
245 val less_than_def = thm "less_than_def"; |
|
246 val greater_than_def = thm "greater_than_def"; |
|
247 |
|
248 val nat_bnd_mono = thm "nat_bnd_mono"; |
|
249 val nat_unfold = thm "nat_unfold"; |
|
250 val nat_0I = thm "nat_0I"; |
|
251 val nat_succI = thm "nat_succI"; |
|
252 val nat_1I = thm "nat_1I"; |
|
253 val nat_2I = thm "nat_2I"; |
|
254 val bool_subset_nat = thm "bool_subset_nat"; |
|
255 val bool_into_nat = thm "bool_into_nat"; |
|
256 val nat_induct = thm "nat_induct"; |
|
257 val natE = thm "natE"; |
|
258 val nat_into_Ord = thm "nat_into_Ord"; |
|
259 val nat_0_le = thm "nat_0_le"; |
|
260 val nat_le_refl = thm "nat_le_refl"; |
|
261 val Ord_nat = thm "Ord_nat"; |
|
262 val Limit_nat = thm "Limit_nat"; |
|
263 val succ_natD = thm "succ_natD"; |
|
264 val nat_succ_iff = thm "nat_succ_iff"; |
|
265 val nat_le_Limit = thm "nat_le_Limit"; |
|
266 val succ_in_naturalD = thm "succ_in_naturalD"; |
|
267 val lt_nat_in_nat = thm "lt_nat_in_nat"; |
|
268 val le_in_nat = thm "le_in_nat"; |
|
269 val complete_induct = thm "complete_induct"; |
|
270 val nat_induct_from_lemma = thm "nat_induct_from_lemma"; |
|
271 val nat_induct_from = thm "nat_induct_from"; |
|
272 val diff_induct = thm "diff_induct"; |
|
273 val succ_lt_induct_lemma = thm "succ_lt_induct_lemma"; |
|
274 val succ_lt_induct = thm "succ_lt_induct"; |
|
275 val nat_case_0 = thm "nat_case_0"; |
|
276 val nat_case_succ = thm "nat_case_succ"; |
|
277 val nat_case_type = thm "nat_case_type"; |
|
278 val nat_rec_0 = thm "nat_rec_0"; |
|
279 val nat_rec_succ = thm "nat_rec_succ"; |
|
280 val Un_nat_type = thm "Un_nat_type"; |
|
281 val Int_nat_type = thm "Int_nat_type"; |
|
282 val nat_nonempty = thm "nat_nonempty"; |
|
283 *} |
|
284 |
42 end |
285 end |