36 |
36 |
37 (** Rewrite rules. Can be used to obtain introduction rules **) |
37 (** Rewrite rules. Can be used to obtain introduction rules **) |
38 |
38 |
39 lemma radd_Inl_Inr_iff [iff]: |
39 lemma radd_Inl_Inr_iff [iff]: |
40 "<Inl(a), Inr(b)> : radd(A,r,B,s) <-> a:A & b:B" |
40 "<Inl(a), Inr(b)> : radd(A,r,B,s) <-> a:A & b:B" |
41 apply (unfold radd_def) |
41 apply (unfold radd_def, blast) |
42 apply blast |
|
43 done |
42 done |
44 |
43 |
45 lemma radd_Inl_iff [iff]: |
44 lemma radd_Inl_iff [iff]: |
46 "<Inl(a'), Inl(a)> : radd(A,r,B,s) <-> a':A & a:A & <a',a>:r" |
45 "<Inl(a'), Inl(a)> : radd(A,r,B,s) <-> a':A & a:A & <a',a>:r" |
47 apply (unfold radd_def) |
46 apply (unfold radd_def, blast) |
48 apply blast |
|
49 done |
47 done |
50 |
48 |
51 lemma radd_Inr_iff [iff]: |
49 lemma radd_Inr_iff [iff]: |
52 "<Inr(b'), Inr(b)> : radd(A,r,B,s) <-> b':B & b:B & <b',b>:s" |
50 "<Inr(b'), Inr(b)> : radd(A,r,B,s) <-> b':B & b:B & <b',b>:s" |
53 apply (unfold radd_def) |
51 apply (unfold radd_def, blast) |
54 apply blast |
|
55 done |
52 done |
56 |
53 |
57 lemma radd_Inr_Inl_iff [iff]: |
54 lemma radd_Inr_Inl_iff [iff]: |
58 "<Inr(b), Inl(a)> : radd(A,r,B,s) <-> False" |
55 "<Inr(b), Inl(a)> : radd(A,r,B,s) <-> False" |
59 apply (unfold radd_def) |
56 apply (unfold radd_def, blast) |
60 apply blast |
|
61 done |
57 done |
62 |
58 |
63 (** Elimination Rule **) |
59 (** Elimination Rule **) |
64 |
60 |
65 lemma raddE: |
61 lemma raddE: |
66 "[| <p',p> : radd(A,r,B,s); |
62 "[| <p',p> : radd(A,r,B,s); |
67 !!x y. [| p'=Inl(x); x:A; p=Inr(y); y:B |] ==> Q; |
63 !!x y. [| p'=Inl(x); x:A; p=Inr(y); y:B |] ==> Q; |
68 !!x' x. [| p'=Inl(x'); p=Inl(x); <x',x>: r; x':A; x:A |] ==> Q; |
64 !!x' x. [| p'=Inl(x'); p=Inl(x); <x',x>: r; x':A; x:A |] ==> Q; |
69 !!y' y. [| p'=Inr(y'); p=Inr(y); <y',y>: s; y':B; y:B |] ==> Q |
65 !!y' y. [| p'=Inr(y'); p=Inr(y); <y',y>: s; y':B; y:B |] ==> Q |
70 |] ==> Q" |
66 |] ==> Q" |
71 apply (unfold radd_def) |
67 apply (unfold radd_def, blast) |
72 apply (blast intro: elim:); |
|
73 done |
68 done |
74 |
69 |
75 (** Type checking **) |
70 (** Type checking **) |
76 |
71 |
77 lemma radd_type: "radd(A,r,B,s) <= (A+B) * (A+B)" |
72 lemma radd_type: "radd(A,r,B,s) <= (A+B) * (A+B)" |
98 (*Proving the lemma, which is needed twice!*) |
92 (*Proving the lemma, which is needed twice!*) |
99 prefer 2 |
93 prefer 2 |
100 apply (erule_tac V = "y : A + B" in thin_rl) |
94 apply (erule_tac V = "y : A + B" in thin_rl) |
101 apply (rule_tac ballI) |
95 apply (rule_tac ballI) |
102 apply (erule_tac r = "r" and a = "x" in wf_on_induct, assumption) |
96 apply (erule_tac r = "r" and a = "x" in wf_on_induct, assumption) |
103 apply (blast intro: elim:); |
97 apply blast |
104 (*Returning to main part of proof*) |
98 (*Returning to main part of proof*) |
105 apply safe |
99 apply safe |
106 apply blast |
100 apply blast |
107 apply (erule_tac r = "s" and a = "ya" in wf_on_induct , assumption) |
101 apply (erule_tac r = "s" and a = "ya" in wf_on_induct, assumption, blast) |
108 apply (blast intro: elim:); |
|
109 done |
102 done |
110 |
103 |
111 lemma wf_radd: "[| wf(r); wf(s) |] ==> wf(radd(field(r),r,field(s),s))" |
104 lemma wf_radd: "[| wf(r); wf(s) |] ==> wf(radd(field(r),r,field(s),s))" |
112 apply (simp add: wf_iff_wf_on_field) |
105 apply (simp add: wf_iff_wf_on_field) |
113 apply (rule wf_on_subset_A [OF _ field_radd]) |
106 apply (rule wf_on_subset_A [OF _ field_radd]) |
161 |
154 |
162 lemma sum_assoc_ord_iso: |
155 lemma sum_assoc_ord_iso: |
163 "(lam z:(A+B)+C. case(case(Inl, %y. Inr(Inl(y))), %y. Inr(Inr(y)), z)) |
156 "(lam z:(A+B)+C. case(case(Inl, %y. Inr(Inl(y))), %y. Inr(Inr(y)), z)) |
164 : ord_iso((A+B)+C, radd(A+B, radd(A,r,B,s), C, t), |
157 : ord_iso((A+B)+C, radd(A+B, radd(A,r,B,s), C, t), |
165 A+(B+C), radd(A, r, B+C, radd(B,s,C,t)))" |
158 A+(B+C), radd(A, r, B+C, radd(B,s,C,t)))" |
166 apply (rule sum_assoc_bij [THEN ord_isoI]) |
159 apply (rule sum_assoc_bij [THEN ord_isoI], auto) |
167 apply auto |
|
168 done |
160 done |
169 |
161 |
170 |
162 |
171 (**** Multiplication of relations -- lexicographic product ****) |
163 (**** Multiplication of relations -- lexicographic product ****) |
172 |
164 |
175 lemma rmult_iff [iff]: |
167 lemma rmult_iff [iff]: |
176 "<<a',b'>, <a,b>> : rmult(A,r,B,s) <-> |
168 "<<a',b'>, <a,b>> : rmult(A,r,B,s) <-> |
177 (<a',a>: r & a':A & a:A & b': B & b: B) | |
169 (<a',a>: r & a':A & a:A & b': B & b: B) | |
178 (<b',b>: s & a'=a & a:A & b': B & b: B)" |
170 (<b',b>: s & a'=a & a:A & b': B & b: B)" |
179 |
171 |
180 apply (unfold rmult_def) |
172 apply (unfold rmult_def, blast) |
181 apply blast |
|
182 done |
173 done |
183 |
174 |
184 lemma rmultE: |
175 lemma rmultE: |
185 "[| <<a',b'>, <a,b>> : rmult(A,r,B,s); |
176 "[| <<a',b'>, <a,b>> : rmult(A,r,B,s); |
186 [| <a',a>: r; a':A; a:A; b':B; b:B |] ==> Q; |
177 [| <a',a>: r; a':A; a:A; b':B; b:B |] ==> Q; |
187 [| <b',b>: s; a:A; a'=a; b':B; b:B |] ==> Q |
178 [| <b',b>: s; a:A; a'=a; b':B; b:B |] ==> Q |
188 |] ==> Q" |
179 |] ==> Q" |
189 apply (blast intro: elim:); |
180 apply blast |
190 done |
181 done |
191 |
182 |
192 (** Type checking **) |
183 (** Type checking **) |
193 |
184 |
194 lemma rmult_type: "rmult(A,r,B,s) <= (A*B) * (A*B)" |
185 lemma rmult_type: "rmult(A,r,B,s) <= (A*B) * (A*B)" |
200 |
191 |
201 (** Linearity **) |
192 (** Linearity **) |
202 |
193 |
203 lemma linear_rmult: |
194 lemma linear_rmult: |
204 "[| linear(A,r); linear(B,s) |] ==> linear(A*B,rmult(A,r,B,s))" |
195 "[| linear(A,r); linear(B,s) |] ==> linear(A*B,rmult(A,r,B,s))" |
205 apply (simp add: linear_def); |
196 apply (simp add: linear_def, blast) |
206 apply (blast intro: elim:); |
|
207 done |
197 done |
208 |
198 |
209 (** Well-foundedness **) |
199 (** Well-foundedness **) |
210 |
200 |
211 lemma wf_on_rmult: "[| wf[A](r); wf[B](s) |] ==> wf[A*B](rmult(A,r,B,s))" |
201 lemma wf_on_rmult: "[| wf[A](r); wf[B](s) |] ==> wf[A*B](rmult(A,r,B,s))" |
212 apply (rule wf_onI2) |
202 apply (rule wf_onI2) |
213 apply (erule SigmaE) |
203 apply (erule SigmaE) |
214 apply (erule ssubst) |
204 apply (erule ssubst) |
215 apply (subgoal_tac "ALL b:B. <x,b>: Ba") |
205 apply (subgoal_tac "ALL b:B. <x,b>: Ba", blast) |
216 apply blast |
206 apply (erule_tac a = "x" in wf_on_induct, assumption) |
217 apply (erule_tac a = "x" in wf_on_induct , assumption) |
|
218 apply (rule ballI) |
207 apply (rule ballI) |
219 apply (erule_tac a = "b" in wf_on_induct , assumption) |
208 apply (erule_tac a = "b" in wf_on_induct, assumption) |
220 apply (best elim!: rmultE bspec [THEN mp]) |
209 apply (best elim!: rmultE bspec [THEN mp]) |
221 done |
210 done |
222 |
211 |
223 |
212 |
224 lemma wf_rmult: "[| wf(r); wf(s) |] ==> wf(rmult(field(r),r,field(s),s))" |
213 lemma wf_rmult: "[| wf(r); wf(s) |] ==> wf(rmult(field(r),r,field(s),s))" |
255 apply (simp_all add: bij_is_fun [THEN apply_type]) |
244 apply (simp_all add: bij_is_fun [THEN apply_type]) |
256 apply (blast intro: bij_is_inj [THEN inj_apply_equality]) |
245 apply (blast intro: bij_is_inj [THEN inj_apply_equality]) |
257 done |
246 done |
258 |
247 |
259 lemma singleton_prod_bij: "(lam z:A. <x,z>) : bij(A, {x}*A)" |
248 lemma singleton_prod_bij: "(lam z:A. <x,z>) : bij(A, {x}*A)" |
260 apply (rule_tac d = "snd" in lam_bijective) |
249 by (rule_tac d = "snd" in lam_bijective, auto) |
261 apply auto |
|
262 done |
|
263 |
250 |
264 (*Used??*) |
251 (*Used??*) |
265 lemma singleton_prod_ord_iso: |
252 lemma singleton_prod_ord_iso: |
266 "well_ord({x},xr) ==> |
253 "well_ord({x},xr) ==> |
267 (lam z:A. <x,z>) : ord_iso(A, r, {x}*A, rmult({x}, xr, A, r))" |
254 (lam z:A. <x,z>) : ord_iso(A, r, {x}*A, rmult({x}, xr, A, r))" |
277 (lam x:C*B + D. case(%x. x, %y.<a,y>, x)) |
264 (lam x:C*B + D. case(%x. x, %y.<a,y>, x)) |
278 : bij(C*B + D, C*B Un {a}*D)" |
265 : bij(C*B + D, C*B Un {a}*D)" |
279 apply (rule subst_elem) |
266 apply (rule subst_elem) |
280 apply (rule id_bij [THEN sum_bij, THEN comp_bij]) |
267 apply (rule id_bij [THEN sum_bij, THEN comp_bij]) |
281 apply (rule singleton_prod_bij) |
268 apply (rule singleton_prod_bij) |
282 apply (rule sum_disjoint_bij) |
269 apply (rule sum_disjoint_bij, blast) |
283 apply blast |
|
284 apply (simp (no_asm_simp) cong add: case_cong) |
270 apply (simp (no_asm_simp) cong add: case_cong) |
285 apply (rule comp_lam [THEN trans, symmetric]) |
271 apply (rule comp_lam [THEN trans, symmetric]) |
286 apply (fast elim!: case_type) |
272 apply (fast elim!: case_type) |
287 apply (simp (no_asm_simp) add: case_case) |
273 apply (simp (no_asm_simp) add: case_case) |
288 done |
274 done |
301 (** Distributive law **) |
287 (** Distributive law **) |
302 |
288 |
303 lemma sum_prod_distrib_bij: |
289 lemma sum_prod_distrib_bij: |
304 "(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x)) |
290 "(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x)) |
305 : bij((A+B)*C, (A*C)+(B*C))" |
291 : bij((A+B)*C, (A*C)+(B*C))" |
306 apply (rule_tac d = "case (%<x,y>.<Inl (x) ,y>, %<x,y>.<Inr (x) ,y>) " |
292 apply (rule_tac d = "case (%<x,y>.<Inl (x),y>, %<x,y>.<Inr (x),y>) " |
307 in lam_bijective) |
293 in lam_bijective) |
308 apply auto |
294 apply auto |
309 done |
295 done |
310 |
296 |
311 lemma sum_prod_distrib_ord_iso: |
297 lemma sum_prod_distrib_ord_iso: |
312 "(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x)) |
298 "(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x)) |
313 : ord_iso((A+B)*C, rmult(A+B, radd(A,r,B,s), C, t), |
299 : ord_iso((A+B)*C, rmult(A+B, radd(A,r,B,s), C, t), |
314 (A*C)+(B*C), radd(A*C, rmult(A,r,C,t), B*C, rmult(B,s,C,t)))" |
300 (A*C)+(B*C), radd(A*C, rmult(A,r,C,t), B*C, rmult(B,s,C,t)))" |
315 apply (rule sum_prod_distrib_bij [THEN ord_isoI]) |
301 apply (rule sum_prod_distrib_bij [THEN ord_isoI], auto) |
316 apply auto |
|
317 done |
302 done |
318 |
303 |
319 (** Associativity **) |
304 (** Associativity **) |
320 |
305 |
321 lemma prod_assoc_bij: |
306 lemma prod_assoc_bij: |
322 "(lam <<x,y>, z>:(A*B)*C. <x,<y,z>>) : bij((A*B)*C, A*(B*C))" |
307 "(lam <<x,y>, z>:(A*B)*C. <x,<y,z>>) : bij((A*B)*C, A*(B*C))" |
323 apply (rule_tac d = "%<x, <y,z>>. <<x,y>, z>" in lam_bijective) |
308 apply (rule_tac d = "%<x, <y,z>>. <<x,y>, z>" in lam_bijective, auto) |
324 apply auto |
|
325 done |
309 done |
326 |
310 |
327 lemma prod_assoc_ord_iso: |
311 lemma prod_assoc_ord_iso: |
328 "(lam <<x,y>, z>:(A*B)*C. <x,<y,z>>) |
312 "(lam <<x,y>, z>:(A*B)*C. <x,<y,z>>) |
329 : ord_iso((A*B)*C, rmult(A*B, rmult(A,r,B,s), C, t), |
313 : ord_iso((A*B)*C, rmult(A*B, rmult(A,r,B,s), C, t), |
330 A*(B*C), rmult(A, r, B*C, rmult(B,s,C,t)))" |
314 A*(B*C), rmult(A, r, B*C, rmult(B,s,C,t)))" |
331 apply (rule prod_assoc_bij [THEN ord_isoI]) |
315 apply (rule prod_assoc_bij [THEN ord_isoI], auto) |
332 apply auto |
|
333 done |
316 done |
334 |
317 |
335 (**** Inverse image of a relation ****) |
318 (**** Inverse image of a relation ****) |
336 |
319 |
337 (** Rewrite rule **) |
320 (** Rewrite rule **) |
338 |
321 |
339 lemma rvimage_iff: "<a,b> : rvimage(A,f,r) <-> <f`a,f`b>: r & a:A & b:A" |
322 lemma rvimage_iff: "<a,b> : rvimage(A,f,r) <-> <f`a,f`b>: r & a:A & b:A" |
340 apply (unfold rvimage_def) |
323 by (unfold rvimage_def, blast) |
341 apply blast |
|
342 done |
|
343 |
324 |
344 (** Type checking **) |
325 (** Type checking **) |
345 |
326 |
346 lemma rvimage_type: "rvimage(A,f,r) <= A*A" |
327 lemma rvimage_type: "rvimage(A,f,r) <= A*A" |
347 apply (unfold rvimage_def) |
328 apply (unfold rvimage_def) |
379 (** Linearity **) |
358 (** Linearity **) |
380 |
359 |
381 lemma linear_rvimage: |
360 lemma linear_rvimage: |
382 "[| f: inj(A,B); linear(B,r) |] ==> linear(A,rvimage(A,f,r))" |
361 "[| f: inj(A,B); linear(B,r) |] ==> linear(A,rvimage(A,f,r))" |
383 apply (simp add: inj_def linear_def rvimage_iff) |
362 apply (simp add: inj_def linear_def rvimage_iff) |
384 apply (blast intro: apply_funtype); |
363 apply (blast intro: apply_funtype) |
385 done |
364 done |
386 |
365 |
387 lemma tot_ord_rvimage: |
366 lemma tot_ord_rvimage: |
388 "[| f: inj(A,B); tot_ord(B,r) |] ==> tot_ord(A, rvimage(A,f,r))" |
367 "[| f: inj(A,B); tot_ord(B,r) |] ==> tot_ord(A, rvimage(A,f,r))" |
389 apply (unfold tot_ord_def) |
368 apply (unfold tot_ord_def) |
429 apply (simp add: rvimage_iff) |
408 apply (simp add: rvimage_iff) |
430 done |
409 done |
431 |
410 |
432 lemma ord_iso_rvimage_eq: |
411 lemma ord_iso_rvimage_eq: |
433 "f: ord_iso(A,r, B,s) ==> rvimage(A,f,s) = r Int A*A" |
412 "f: ord_iso(A,r, B,s) ==> rvimage(A,f,s) = r Int A*A" |
434 apply (unfold ord_iso_def rvimage_def) |
413 apply (unfold ord_iso_def rvimage_def, blast) |
435 apply blast |
|
436 done |
414 done |
437 |
415 |
438 |
416 |
439 (** The "measure" relation is useful with wfrec **) |
417 (** The "measure" relation is useful with wfrec **) |
440 |
418 |
441 lemma measure_eq_rvimage_Memrel: |
419 lemma measure_eq_rvimage_Memrel: |
442 "measure(A,f) = rvimage(A,Lambda(A,f),Memrel(Collect(RepFun(A,f),Ord)))" |
420 "measure(A,f) = rvimage(A,Lambda(A,f),Memrel(Collect(RepFun(A,f),Ord)))" |
443 apply (simp (no_asm) add: measure_def rvimage_def Memrel_iff) |
421 apply (simp (no_asm) add: measure_def rvimage_def Memrel_iff) |
444 apply (rule equalityI) |
422 apply (rule equalityI, auto) |
445 apply auto |
|
446 apply (auto intro: Ord_in_Ord simp add: lt_def) |
423 apply (auto intro: Ord_in_Ord simp add: lt_def) |
447 done |
424 done |
448 |
425 |
449 lemma wf_measure [iff]: "wf(measure(A,f))" |
426 lemma wf_measure [iff]: "wf(measure(A,f))" |
450 apply (simp (no_asm) add: measure_eq_rvimage_Memrel wf_Memrel wf_rvimage) |
427 apply (simp (no_asm) add: measure_eq_rvimage_Memrel wf_Memrel wf_rvimage) |