1 (* Title: HOL/Univ |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1991 University of Cambridge |
|
5 *) |
|
6 |
|
7 (** apfst -- can be used in similar type definitions **) |
|
8 |
|
9 Goalw [apfst_def] "apfst f (a,b) = (f(a),b)"; |
|
10 by (rtac split 1); |
|
11 qed "apfst_conv"; |
|
12 |
|
13 val [major,minor] = Goal |
|
14 "[| q = apfst f p; !!x y. [| p = (x,y); q = (f(x),y) |] ==> R \ |
|
15 \ |] ==> R"; |
|
16 by (rtac PairE 1); |
|
17 by (rtac minor 1); |
|
18 by (assume_tac 1); |
|
19 by (rtac (major RS trans) 1); |
|
20 by (etac ssubst 1); |
|
21 by (rtac apfst_conv 1); |
|
22 qed "apfst_convE"; |
|
23 |
|
24 (** Push -- an injection, analogous to Cons on lists **) |
|
25 |
|
26 Goalw [Push_def] "Push i f = Push j g ==> i=j"; |
|
27 by (etac (fun_cong RS box_equals) 1); |
|
28 by (rtac nat_case_0 1); |
|
29 by (rtac nat_case_0 1); |
|
30 qed "Push_inject1"; |
|
31 |
|
32 Goalw [Push_def] "Push i f = Push j g ==> f=g"; |
|
33 by (rtac (ext RS box_equals) 1); |
|
34 by (etac fun_cong 1); |
|
35 by (rtac (nat_case_Suc RS ext) 1); |
|
36 by (rtac (nat_case_Suc RS ext) 1); |
|
37 qed "Push_inject2"; |
|
38 |
|
39 val [major,minor] = Goal |
|
40 "[| Push i f =Push j g; [| i=j; f=g |] ==> P \ |
|
41 \ |] ==> P"; |
|
42 by (rtac ((major RS Push_inject2) RS ((major RS Push_inject1) RS minor)) 1); |
|
43 qed "Push_inject"; |
|
44 |
|
45 Goalw [Push_def] "Push (Inr (Suc k)) f = (%z. Inr 0) ==> P"; |
|
46 by (rtac Suc_neq_Zero 1); |
|
47 by (etac (fun_cong RS box_equals RS Inr_inject) 1); |
|
48 by (rtac nat_case_0 1); |
|
49 by (rtac refl 1); |
|
50 qed "Push_neq_K0"; |
|
51 |
|
52 (*** Isomorphisms ***) |
|
53 |
|
54 Goal "inj(Rep_Node)"; |
|
55 by (rtac inj_inverseI 1); (*cannot combine by RS: multiple unifiers*) |
|
56 by (rtac Rep_Node_inverse 1); |
|
57 qed "inj_Rep_Node"; |
|
58 |
|
59 Goal "inj_on Abs_Node Node"; |
|
60 by (rtac inj_on_inverseI 1); |
|
61 by (etac Abs_Node_inverse 1); |
|
62 qed "inj_on_Abs_Node"; |
|
63 |
|
64 bind_thm ("Abs_Node_inject", inj_on_Abs_Node RS inj_onD); |
|
65 |
|
66 |
|
67 (*** Introduction rules for Node ***) |
|
68 |
|
69 Goalw [Node_def] "(%k. Inr 0, a) : Node"; |
|
70 by (Blast_tac 1); |
|
71 qed "Node_K0_I"; |
|
72 |
|
73 Goalw [Node_def,Push_def] |
|
74 "p: Node ==> apfst (Push i) p : Node"; |
|
75 by (fast_tac (claset() addSIs [apfst_conv, nat_case_Suc RS trans]) 1); |
|
76 qed "Node_Push_I"; |
|
77 |
|
78 |
|
79 (*** Distinctness of constructors ***) |
|
80 |
|
81 (** Scons vs Atom **) |
|
82 |
|
83 Goalw [Atom_def,Scons_def,Push_Node_def] "Scons M N ~= Atom(a)"; |
|
84 by (rtac notI 1); |
|
85 by (etac (equalityD2 RS subsetD RS UnE) 1); |
|
86 by (rtac singletonI 1); |
|
87 by (REPEAT (eresolve_tac [imageE, Abs_Node_inject RS apfst_convE, |
|
88 Pair_inject, sym RS Push_neq_K0] 1 |
|
89 ORELSE resolve_tac [Node_K0_I, Rep_Node RS Node_Push_I] 1)); |
|
90 qed "Scons_not_Atom"; |
|
91 bind_thm ("Atom_not_Scons", Scons_not_Atom RS not_sym); |
|
92 |
|
93 |
|
94 (*** Injectiveness ***) |
|
95 |
|
96 (** Atomic nodes **) |
|
97 |
|
98 Goalw [Atom_def] "inj(Atom)"; |
|
99 by (blast_tac (claset() addSIs [injI, Node_K0_I] addSDs [Abs_Node_inject]) 1); |
|
100 qed "inj_Atom"; |
|
101 bind_thm ("Atom_inject", inj_Atom RS injD); |
|
102 |
|
103 Goal "(Atom(a)=Atom(b)) = (a=b)"; |
|
104 by (blast_tac (claset() addSDs [Atom_inject]) 1); |
|
105 qed "Atom_Atom_eq"; |
|
106 AddIffs [Atom_Atom_eq]; |
|
107 |
|
108 Goalw [Leaf_def,o_def] "inj(Leaf)"; |
|
109 by (rtac injI 1); |
|
110 by (etac (Atom_inject RS Inl_inject) 1); |
|
111 qed "inj_Leaf"; |
|
112 |
|
113 bind_thm ("Leaf_inject", inj_Leaf RS injD); |
|
114 AddSDs [Leaf_inject]; |
|
115 |
|
116 Goalw [Numb_def,o_def] "inj(Numb)"; |
|
117 by (rtac injI 1); |
|
118 by (etac (Atom_inject RS Inr_inject) 1); |
|
119 qed "inj_Numb"; |
|
120 |
|
121 bind_thm ("Numb_inject", inj_Numb RS injD); |
|
122 AddSDs [Numb_inject]; |
|
123 |
|
124 (** Injectiveness of Push_Node **) |
|
125 |
|
126 val [major,minor] = Goalw [Push_Node_def] |
|
127 "[| Push_Node i m =Push_Node j n; [| i=j; m=n |] ==> P \ |
|
128 \ |] ==> P"; |
|
129 by (rtac (major RS Abs_Node_inject RS apfst_convE) 1); |
|
130 by (REPEAT (resolve_tac [Rep_Node RS Node_Push_I] 1)); |
|
131 by (etac (sym RS apfst_convE) 1); |
|
132 by (rtac minor 1); |
|
133 by (etac Pair_inject 1); |
|
134 by (etac (Push_inject1 RS sym) 1); |
|
135 by (rtac (inj_Rep_Node RS injD) 1); |
|
136 by (etac trans 1); |
|
137 by (safe_tac (claset() addSEs [Push_inject,sym])); |
|
138 qed "Push_Node_inject"; |
|
139 |
|
140 |
|
141 (** Injectiveness of Scons **) |
|
142 |
|
143 Goalw [Scons_def] "Scons M N <= Scons M' N' ==> M<=M'"; |
|
144 by (blast_tac (claset() addSDs [Push_Node_inject]) 1); |
|
145 qed "Scons_inject_lemma1"; |
|
146 |
|
147 Goalw [Scons_def] "Scons M N <= Scons M' N' ==> N<=N'"; |
|
148 by (blast_tac (claset() addSDs [Push_Node_inject]) 1); |
|
149 qed "Scons_inject_lemma2"; |
|
150 |
|
151 Goal "Scons M N = Scons M' N' ==> M=M'"; |
|
152 by (etac equalityE 1); |
|
153 by (REPEAT (ares_tac [equalityI, Scons_inject_lemma1] 1)); |
|
154 qed "Scons_inject1"; |
|
155 |
|
156 Goal "Scons M N = Scons M' N' ==> N=N'"; |
|
157 by (etac equalityE 1); |
|
158 by (REPEAT (ares_tac [equalityI, Scons_inject_lemma2] 1)); |
|
159 qed "Scons_inject2"; |
|
160 |
|
161 val [major,minor] = Goal |
|
162 "[| Scons M N = Scons M' N'; [| M=M'; N=N' |] ==> P \ |
|
163 \ |] ==> P"; |
|
164 by (rtac ((major RS Scons_inject2) RS ((major RS Scons_inject1) RS minor)) 1); |
|
165 qed "Scons_inject"; |
|
166 |
|
167 Goal "(Scons M N = Scons M' N') = (M=M' & N=N')"; |
|
168 by (blast_tac (claset() addSEs [Scons_inject]) 1); |
|
169 qed "Scons_Scons_eq"; |
|
170 |
|
171 (*** Distinctness involving Leaf and Numb ***) |
|
172 |
|
173 (** Scons vs Leaf **) |
|
174 |
|
175 Goalw [Leaf_def,o_def] "Scons M N ~= Leaf(a)"; |
|
176 by (rtac Scons_not_Atom 1); |
|
177 qed "Scons_not_Leaf"; |
|
178 bind_thm ("Leaf_not_Scons", Scons_not_Leaf RS not_sym); |
|
179 |
|
180 AddIffs [Scons_not_Leaf, Leaf_not_Scons]; |
|
181 |
|
182 |
|
183 (** Scons vs Numb **) |
|
184 |
|
185 Goalw [Numb_def,o_def] "Scons M N ~= Numb(k)"; |
|
186 by (rtac Scons_not_Atom 1); |
|
187 qed "Scons_not_Numb"; |
|
188 bind_thm ("Numb_not_Scons", Scons_not_Numb RS not_sym); |
|
189 |
|
190 AddIffs [Scons_not_Numb, Numb_not_Scons]; |
|
191 |
|
192 |
|
193 (** Leaf vs Numb **) |
|
194 |
|
195 Goalw [Leaf_def,Numb_def] "Leaf(a) ~= Numb(k)"; |
|
196 by (simp_tac (simpset() addsimps [Inl_not_Inr]) 1); |
|
197 qed "Leaf_not_Numb"; |
|
198 bind_thm ("Numb_not_Leaf", Leaf_not_Numb RS not_sym); |
|
199 |
|
200 AddIffs [Leaf_not_Numb, Numb_not_Leaf]; |
|
201 |
|
202 |
|
203 (*** ndepth -- the depth of a node ***) |
|
204 |
|
205 Addsimps [apfst_conv]; |
|
206 AddIffs [Scons_not_Atom, Atom_not_Scons, Scons_Scons_eq]; |
|
207 |
|
208 |
|
209 Goalw [ndepth_def] "ndepth (Abs_Node(%k. Inr 0, x)) = 0"; |
|
210 by (EVERY1[stac (Node_K0_I RS Abs_Node_inverse), stac split]); |
|
211 by (rtac Least_equality 1); |
|
212 by (rtac refl 1); |
|
213 by (etac less_zeroE 1); |
|
214 qed "ndepth_K0"; |
|
215 |
|
216 Goal "k < Suc(LEAST x. f x = Inr 0) --> nat_case (Inr (Suc i)) f k ~= Inr 0"; |
|
217 by (induct_tac "k" 1); |
|
218 by (ALLGOALS Simp_tac); |
|
219 by (rtac impI 1); |
|
220 by (etac not_less_Least 1); |
|
221 val lemma = result(); |
|
222 |
|
223 Goalw [ndepth_def,Push_Node_def] |
|
224 "ndepth (Push_Node (Inr (Suc i)) n) = Suc(ndepth(n))"; |
|
225 by (stac (Rep_Node RS Node_Push_I RS Abs_Node_inverse) 1); |
|
226 by (cut_facts_tac [rewrite_rule [Node_def] Rep_Node] 1); |
|
227 by Safe_tac; |
|
228 by (etac ssubst 1); (*instantiates type variables!*) |
|
229 by (Simp_tac 1); |
|
230 by (rtac Least_equality 1); |
|
231 by (rewtac Push_def); |
|
232 by (rtac (nat_case_Suc RS trans) 1); |
|
233 by (etac LeastI 1); |
|
234 by (asm_simp_tac (simpset() addsimps [lemma]) 1); |
|
235 qed "ndepth_Push_Node"; |
|
236 |
|
237 |
|
238 (*** ntrunc applied to the various node sets ***) |
|
239 |
|
240 Goalw [ntrunc_def] "ntrunc 0 M = {}"; |
|
241 by (Blast_tac 1); |
|
242 qed "ntrunc_0"; |
|
243 |
|
244 Goalw [Atom_def,ntrunc_def] "ntrunc (Suc k) (Atom a) = Atom(a)"; |
|
245 by (fast_tac (claset() addss (simpset() addsimps [ndepth_K0])) 1); |
|
246 qed "ntrunc_Atom"; |
|
247 |
|
248 Goalw [Leaf_def,o_def] "ntrunc (Suc k) (Leaf a) = Leaf(a)"; |
|
249 by (rtac ntrunc_Atom 1); |
|
250 qed "ntrunc_Leaf"; |
|
251 |
|
252 Goalw [Numb_def,o_def] "ntrunc (Suc k) (Numb i) = Numb(i)"; |
|
253 by (rtac ntrunc_Atom 1); |
|
254 qed "ntrunc_Numb"; |
|
255 |
|
256 Goalw [Scons_def,ntrunc_def] |
|
257 "ntrunc (Suc k) (Scons M N) = Scons (ntrunc k M) (ntrunc k N)"; |
|
258 by (safe_tac (claset() addSIs [imageI])); |
|
259 by (REPEAT (stac ndepth_Push_Node 3 THEN etac Suc_mono 3)); |
|
260 by (REPEAT (rtac Suc_less_SucD 1 THEN |
|
261 rtac (ndepth_Push_Node RS subst) 1 THEN |
|
262 assume_tac 1)); |
|
263 qed "ntrunc_Scons"; |
|
264 |
|
265 Addsimps [ntrunc_0, ntrunc_Atom, ntrunc_Leaf, ntrunc_Numb, ntrunc_Scons]; |
|
266 |
|
267 |
|
268 (** Injection nodes **) |
|
269 |
|
270 Goalw [In0_def] "ntrunc 1 (In0 M) = {}"; |
|
271 by (Simp_tac 1); |
|
272 by (rewtac Scons_def); |
|
273 by (Blast_tac 1); |
|
274 qed "ntrunc_one_In0"; |
|
275 |
|
276 Goalw [In0_def] |
|
277 "ntrunc (Suc (Suc k)) (In0 M) = In0 (ntrunc (Suc k) M)"; |
|
278 by (Simp_tac 1); |
|
279 qed "ntrunc_In0"; |
|
280 |
|
281 Goalw [In1_def] "ntrunc 1 (In1 M) = {}"; |
|
282 by (Simp_tac 1); |
|
283 by (rewtac Scons_def); |
|
284 by (Blast_tac 1); |
|
285 qed "ntrunc_one_In1"; |
|
286 |
|
287 Goalw [In1_def] |
|
288 "ntrunc (Suc (Suc k)) (In1 M) = In1 (ntrunc (Suc k) M)"; |
|
289 by (Simp_tac 1); |
|
290 qed "ntrunc_In1"; |
|
291 |
|
292 Addsimps [ntrunc_one_In0, ntrunc_In0, ntrunc_one_In1, ntrunc_In1]; |
|
293 |
|
294 |
|
295 (*** Cartesian Product ***) |
|
296 |
|
297 Goalw [uprod_def] "[| M:A; N:B |] ==> Scons M N : uprod A B"; |
|
298 by (REPEAT (ares_tac [singletonI,UN_I] 1)); |
|
299 qed "uprodI"; |
|
300 |
|
301 (*The general elimination rule*) |
|
302 val major::prems = Goalw [uprod_def] |
|
303 "[| c : uprod A B; \ |
|
304 \ !!x y. [| x:A; y:B; c = Scons x y |] ==> P \ |
|
305 \ |] ==> P"; |
|
306 by (cut_facts_tac [major] 1); |
|
307 by (REPEAT (eresolve_tac [asm_rl,singletonE,UN_E] 1 |
|
308 ORELSE resolve_tac prems 1)); |
|
309 qed "uprodE"; |
|
310 |
|
311 (*Elimination of a pair -- introduces no eigenvariables*) |
|
312 val prems = Goal |
|
313 "[| Scons M N : uprod A B; [| M:A; N:B |] ==> P \ |
|
314 \ |] ==> P"; |
|
315 by (rtac uprodE 1); |
|
316 by (REPEAT (ares_tac prems 1 ORELSE eresolve_tac [Scons_inject,ssubst] 1)); |
|
317 qed "uprodE2"; |
|
318 |
|
319 |
|
320 (*** Disjoint Sum ***) |
|
321 |
|
322 Goalw [usum_def] "M:A ==> In0(M) : usum A B"; |
|
323 by (Blast_tac 1); |
|
324 qed "usum_In0I"; |
|
325 |
|
326 Goalw [usum_def] "N:B ==> In1(N) : usum A B"; |
|
327 by (Blast_tac 1); |
|
328 qed "usum_In1I"; |
|
329 |
|
330 val major::prems = Goalw [usum_def] |
|
331 "[| u : usum A B; \ |
|
332 \ !!x. [| x:A; u=In0(x) |] ==> P; \ |
|
333 \ !!y. [| y:B; u=In1(y) |] ==> P \ |
|
334 \ |] ==> P"; |
|
335 by (rtac (major RS UnE) 1); |
|
336 by (REPEAT (rtac refl 1 |
|
337 ORELSE eresolve_tac (prems@[imageE,ssubst]) 1)); |
|
338 qed "usumE"; |
|
339 |
|
340 |
|
341 (** Injection **) |
|
342 |
|
343 Goalw [In0_def,In1_def] "In0(M) ~= In1(N)"; |
|
344 by (rtac notI 1); |
|
345 by (etac (Scons_inject1 RS Numb_inject RS Zero_neq_Suc) 1); |
|
346 qed "In0_not_In1"; |
|
347 |
|
348 bind_thm ("In1_not_In0", In0_not_In1 RS not_sym); |
|
349 |
|
350 AddIffs [In0_not_In1, In1_not_In0]; |
|
351 |
|
352 Goalw [In0_def] "In0(M) = In0(N) ==> M=N"; |
|
353 by (etac (Scons_inject2) 1); |
|
354 qed "In0_inject"; |
|
355 |
|
356 Goalw [In1_def] "In1(M) = In1(N) ==> M=N"; |
|
357 by (etac (Scons_inject2) 1); |
|
358 qed "In1_inject"; |
|
359 |
|
360 Goal "(In0 M = In0 N) = (M=N)"; |
|
361 by (blast_tac (claset() addSDs [In0_inject]) 1); |
|
362 qed "In0_eq"; |
|
363 |
|
364 Goal "(In1 M = In1 N) = (M=N)"; |
|
365 by (blast_tac (claset() addSDs [In1_inject]) 1); |
|
366 qed "In1_eq"; |
|
367 |
|
368 AddIffs [In0_eq, In1_eq]; |
|
369 |
|
370 Goal "inj In0"; |
|
371 by (blast_tac (claset() addSIs [injI]) 1); |
|
372 qed "inj_In0"; |
|
373 |
|
374 Goal "inj In1"; |
|
375 by (blast_tac (claset() addSIs [injI]) 1); |
|
376 qed "inj_In1"; |
|
377 |
|
378 |
|
379 (*** Function spaces ***) |
|
380 |
|
381 Goalw [Lim_def] "Lim f = Lim g ==> f = g"; |
|
382 by (rtac ext 1); |
|
383 by (blast_tac (claset() addSEs [Push_Node_inject]) 1); |
|
384 qed "Lim_inject"; |
|
385 |
|
386 Goalw [Funs_def] "S <= T ==> Funs S <= Funs T"; |
|
387 by (Blast_tac 1); |
|
388 qed "Funs_mono"; |
|
389 |
|
390 val [prem] = Goalw [Funs_def] "(!!x. f x : S) ==> f : Funs S"; |
|
391 by (blast_tac (claset() addIs [prem]) 1); |
|
392 qed "FunsI"; |
|
393 |
|
394 Goalw [Funs_def] "f : Funs S ==> f x : S"; |
|
395 by (etac CollectE 1); |
|
396 by (etac subsetD 1); |
|
397 by (rtac rangeI 1); |
|
398 qed "FunsD"; |
|
399 |
|
400 val [p1, p2] = Goalw [o_def] |
|
401 "[| f : Funs R; !!x. x : R ==> r (a x) = x |] ==> r o (a o f) = f"; |
|
402 by (rtac (p2 RS ext) 1); |
|
403 by (rtac (p1 RS FunsD) 1); |
|
404 qed "Funs_inv"; |
|
405 |
|
406 val [p1, p2] = Goalw [o_def] |
|
407 "[| f : Funs (range g); !!h. f = g o h ==> P |] ==> P"; |
|
408 by (res_inst_tac [("h", "%x. @y. (f::'a=>'b) x = g y")] p2 1); |
|
409 by (rtac ext 1); |
|
410 by (rtac (p1 RS FunsD RS rangeE) 1); |
|
411 by (etac (exI RS (some_eq_ex RS iffD2)) 1); |
|
412 qed "Funs_rangeE"; |
|
413 |
|
414 Goal "a : S ==> (%x. a) : Funs S"; |
|
415 by (rtac FunsI 1); |
|
416 by (assume_tac 1); |
|
417 qed "Funs_nonempty"; |
|
418 |
|
419 |
|
420 (*** proving equality of sets and functions using ntrunc ***) |
|
421 |
|
422 Goalw [ntrunc_def] "ntrunc k M <= M"; |
|
423 by (Blast_tac 1); |
|
424 qed "ntrunc_subsetI"; |
|
425 |
|
426 val [major] = Goalw [ntrunc_def] "(!!k. ntrunc k M <= N) ==> M<=N"; |
|
427 by (blast_tac (claset() addIs [less_add_Suc1, less_add_Suc2, |
|
428 major RS subsetD]) 1); |
|
429 qed "ntrunc_subsetD"; |
|
430 |
|
431 (*A generalized form of the take-lemma*) |
|
432 val [major] = Goal "(!!k. ntrunc k M = ntrunc k N) ==> M=N"; |
|
433 by (rtac equalityI 1); |
|
434 by (ALLGOALS (rtac ntrunc_subsetD)); |
|
435 by (ALLGOALS (rtac (ntrunc_subsetI RSN (2, subset_trans)))); |
|
436 by (rtac (major RS equalityD1) 1); |
|
437 by (rtac (major RS equalityD2) 1); |
|
438 qed "ntrunc_equality"; |
|
439 |
|
440 val [major] = Goalw [o_def] |
|
441 "[| !!k. (ntrunc(k) o h1) = (ntrunc(k) o h2) |] ==> h1=h2"; |
|
442 by (rtac (ntrunc_equality RS ext) 1); |
|
443 by (rtac (major RS fun_cong) 1); |
|
444 qed "ntrunc_o_equality"; |
|
445 |
|
446 (*** Monotonicity ***) |
|
447 |
|
448 Goalw [uprod_def] "[| A<=A'; B<=B' |] ==> uprod A B <= uprod A' B'"; |
|
449 by (Blast_tac 1); |
|
450 qed "uprod_mono"; |
|
451 |
|
452 Goalw [usum_def] "[| A<=A'; B<=B' |] ==> usum A B <= usum A' B'"; |
|
453 by (Blast_tac 1); |
|
454 qed "usum_mono"; |
|
455 |
|
456 Goalw [Scons_def] "[| M<=M'; N<=N' |] ==> Scons M N <= Scons M' N'"; |
|
457 by (Blast_tac 1); |
|
458 qed "Scons_mono"; |
|
459 |
|
460 Goalw [In0_def] "M<=N ==> In0(M) <= In0(N)"; |
|
461 by (REPEAT (ares_tac [subset_refl,Scons_mono] 1)); |
|
462 qed "In0_mono"; |
|
463 |
|
464 Goalw [In1_def] "M<=N ==> In1(M) <= In1(N)"; |
|
465 by (REPEAT (ares_tac [subset_refl,Scons_mono] 1)); |
|
466 qed "In1_mono"; |
|
467 |
|
468 |
|
469 (*** Split and Case ***) |
|
470 |
|
471 Goalw [Split_def] "Split c (Scons M N) = c M N"; |
|
472 by (Blast_tac 1); |
|
473 qed "Split"; |
|
474 |
|
475 Goalw [Case_def] "Case c d (In0 M) = c(M)"; |
|
476 by (Blast_tac 1); |
|
477 qed "Case_In0"; |
|
478 |
|
479 Goalw [Case_def] "Case c d (In1 N) = d(N)"; |
|
480 by (Blast_tac 1); |
|
481 qed "Case_In1"; |
|
482 |
|
483 Addsimps [Split, Case_In0, Case_In1]; |
|
484 |
|
485 |
|
486 (**** UN x. B(x) rules ****) |
|
487 |
|
488 Goalw [ntrunc_def] "ntrunc k (UN x. f(x)) = (UN x. ntrunc k (f x))"; |
|
489 by (Blast_tac 1); |
|
490 qed "ntrunc_UN1"; |
|
491 |
|
492 Goalw [Scons_def] "Scons (UN x. f x) M = (UN x. Scons (f x) M)"; |
|
493 by (Blast_tac 1); |
|
494 qed "Scons_UN1_x"; |
|
495 |
|
496 Goalw [Scons_def] "Scons M (UN x. f x) = (UN x. Scons M (f x))"; |
|
497 by (Blast_tac 1); |
|
498 qed "Scons_UN1_y"; |
|
499 |
|
500 Goalw [In0_def] "In0(UN x. f(x)) = (UN x. In0(f(x)))"; |
|
501 by (rtac Scons_UN1_y 1); |
|
502 qed "In0_UN1"; |
|
503 |
|
504 Goalw [In1_def] "In1(UN x. f(x)) = (UN x. In1(f(x)))"; |
|
505 by (rtac Scons_UN1_y 1); |
|
506 qed "In1_UN1"; |
|
507 |
|
508 |
|
509 (*** Equality for Cartesian Product ***) |
|
510 |
|
511 Goalw [dprod_def] |
|
512 "[| (M,M'):r; (N,N'):s |] ==> (Scons M N, Scons M' N') : dprod r s"; |
|
513 by (Blast_tac 1); |
|
514 qed "dprodI"; |
|
515 |
|
516 (*The general elimination rule*) |
|
517 val major::prems = Goalw [dprod_def] |
|
518 "[| c : dprod r s; \ |
|
519 \ !!x y x' y'. [| (x,x') : r; (y,y') : s; c = (Scons x y, Scons x' y') |] ==> P \ |
|
520 \ |] ==> P"; |
|
521 by (cut_facts_tac [major] 1); |
|
522 by (REPEAT_FIRST (eresolve_tac [asm_rl, UN_E, mem_splitE, singletonE])); |
|
523 by (REPEAT (ares_tac prems 1 ORELSE hyp_subst_tac 1)); |
|
524 qed "dprodE"; |
|
525 |
|
526 |
|
527 (*** Equality for Disjoint Sum ***) |
|
528 |
|
529 Goalw [dsum_def] "(M,M'):r ==> (In0(M), In0(M')) : dsum r s"; |
|
530 by (Blast_tac 1); |
|
531 qed "dsum_In0I"; |
|
532 |
|
533 Goalw [dsum_def] "(N,N'):s ==> (In1(N), In1(N')) : dsum r s"; |
|
534 by (Blast_tac 1); |
|
535 qed "dsum_In1I"; |
|
536 |
|
537 val major::prems = Goalw [dsum_def] |
|
538 "[| w : dsum r s; \ |
|
539 \ !!x x'. [| (x,x') : r; w = (In0(x), In0(x')) |] ==> P; \ |
|
540 \ !!y y'. [| (y,y') : s; w = (In1(y), In1(y')) |] ==> P \ |
|
541 \ |] ==> P"; |
|
542 by (cut_facts_tac [major] 1); |
|
543 by (REPEAT_FIRST (eresolve_tac [asm_rl, UN_E, UnE, mem_splitE, singletonE])); |
|
544 by (DEPTH_SOLVE (ares_tac prems 1 ORELSE hyp_subst_tac 1)); |
|
545 qed "dsumE"; |
|
546 |
|
547 AddSIs [uprodI, dprodI]; |
|
548 AddIs [usum_In0I, usum_In1I, dsum_In0I, dsum_In1I]; |
|
549 AddSEs [uprodE, dprodE, usumE, dsumE]; |
|
550 |
|
551 |
|
552 (*** Monotonicity ***) |
|
553 |
|
554 Goal "[| r<=r'; s<=s' |] ==> dprod r s <= dprod r' s'"; |
|
555 by (Blast_tac 1); |
|
556 qed "dprod_mono"; |
|
557 |
|
558 Goal "[| r<=r'; s<=s' |] ==> dsum r s <= dsum r' s'"; |
|
559 by (Blast_tac 1); |
|
560 qed "dsum_mono"; |
|
561 |
|
562 |
|
563 (*** Bounding theorems ***) |
|
564 |
|
565 Goal "(dprod (A <*> B) (C <*> D)) <= (uprod A C) <*> (uprod B D)"; |
|
566 by (Blast_tac 1); |
|
567 qed "dprod_Sigma"; |
|
568 |
|
569 bind_thm ("dprod_subset_Sigma", [dprod_mono, dprod_Sigma] MRS subset_trans |> standard); |
|
570 |
|
571 (*Dependent version*) |
|
572 Goal "(dprod (Sigma A B) (Sigma C D)) <= Sigma (uprod A C) (Split (%x y. uprod (B x) (D y)))"; |
|
573 by Safe_tac; |
|
574 by (stac Split 1); |
|
575 by (Blast_tac 1); |
|
576 qed "dprod_subset_Sigma2"; |
|
577 |
|
578 Goal "(dsum (A <*> B) (C <*> D)) <= (usum A C) <*> (usum B D)"; |
|
579 by (Blast_tac 1); |
|
580 qed "dsum_Sigma"; |
|
581 |
|
582 bind_thm ("dsum_subset_Sigma", [dsum_mono, dsum_Sigma] MRS subset_trans |> standard); |
|
583 |
|
584 |
|
585 (*** Domain ***) |
|
586 |
|
587 Goal "Domain (dprod r s) = uprod (Domain r) (Domain s)"; |
|
588 by Auto_tac; |
|
589 qed "Domain_dprod"; |
|
590 |
|
591 Goal "Domain (dsum r s) = usum (Domain r) (Domain s)"; |
|
592 by Auto_tac; |
|
593 qed "Domain_dsum"; |
|
594 |
|
595 Addsimps [Domain_dprod, Domain_dsum]; |
|