30 |
31 |
31 measure :: "[i, i\<Rightarrow>i] \<Rightarrow> i" |
32 measure :: "[i, i\<Rightarrow>i] \<Rightarrow> i" |
32 "measure(A,f) == {<x,y>: A*A. f(x) < f(y)}" |
33 "measure(A,f) == {<x,y>: A*A. f(x) < f(y)}" |
33 |
34 |
34 |
35 |
35 (**** Addition of relations -- disjoint sum ****) |
36 subsection{*Addition of Relations -- Disjoint Sum*} |
36 |
37 |
37 (** Rewrite rules. Can be used to obtain introduction rules **) |
38 (** Rewrite rules. Can be used to obtain introduction rules **) |
38 |
39 |
39 lemma radd_Inl_Inr_iff [iff]: |
40 lemma radd_Inl_Inr_iff [iff]: |
40 "<Inl(a), Inr(b)> : radd(A,r,B,s) <-> a:A & b:B" |
41 "<Inl(a), Inr(b)> : radd(A,r,B,s) <-> a:A & b:B" |
41 apply (unfold radd_def, blast) |
42 by (unfold radd_def, blast) |
42 done |
|
43 |
43 |
44 lemma radd_Inl_iff [iff]: |
44 lemma radd_Inl_iff [iff]: |
45 "<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" |
46 apply (unfold radd_def, blast) |
46 by (unfold radd_def, blast) |
47 done |
|
48 |
47 |
49 lemma radd_Inr_iff [iff]: |
48 lemma radd_Inr_iff [iff]: |
50 "<Inr(b'), Inr(b)> : radd(A,r,B,s) <-> b':B & b:B & <b',b>:s" |
49 "<Inr(b'), Inr(b)> : radd(A,r,B,s) <-> b':B & b:B & <b',b>:s" |
51 apply (unfold radd_def, blast) |
50 by (unfold radd_def, blast) |
52 done |
|
53 |
51 |
54 lemma radd_Inr_Inl_iff [iff]: |
52 lemma radd_Inr_Inl_iff [iff]: |
55 "<Inr(b), Inl(a)> : radd(A,r,B,s) <-> False" |
53 "<Inr(b), Inl(a)> : radd(A,r,B,s) <-> False" |
56 apply (unfold radd_def, blast) |
54 by (unfold radd_def, blast) |
57 done |
|
58 |
55 |
59 (** Elimination Rule **) |
56 (** Elimination Rule **) |
60 |
57 |
61 lemma raddE: |
58 lemma raddE: |
62 "[| <p',p> : radd(A,r,B,s); |
59 "[| <p',p> : radd(A,r,B,s); |
63 !!x y. [| p'=Inl(x); x:A; p=Inr(y); y:B |] ==> Q; |
60 !!x y. [| p'=Inl(x); x:A; p=Inr(y); y:B |] ==> Q; |
64 !!x' x. [| p'=Inl(x'); p=Inl(x); <x',x>: r; x':A; x:A |] ==> Q; |
61 !!x' x. [| p'=Inl(x'); p=Inl(x); <x',x>: r; x':A; x:A |] ==> Q; |
65 !!y' y. [| p'=Inr(y'); p=Inr(y); <y',y>: s; y':B; y:B |] ==> Q |
62 !!y' y. [| p'=Inr(y'); p=Inr(y); <y',y>: s; y':B; y:B |] ==> Q |
66 |] ==> Q" |
63 |] ==> Q" |
67 apply (unfold radd_def, blast) |
64 by (unfold radd_def, blast) |
68 done |
|
69 |
65 |
70 (** Type checking **) |
66 (** Type checking **) |
71 |
67 |
72 lemma radd_type: "radd(A,r,B,s) <= (A+B) * (A+B)" |
68 lemma radd_type: "radd(A,r,B,s) <= (A+B) * (A+B)" |
73 apply (unfold radd_def) |
69 apply (unfold radd_def) |
154 |
150 |
155 lemma sum_assoc_ord_iso: |
151 lemma sum_assoc_ord_iso: |
156 "(lam z:(A+B)+C. case(case(Inl, %y. Inr(Inl(y))), %y. Inr(Inr(y)), z)) |
152 "(lam z:(A+B)+C. case(case(Inl, %y. Inr(Inl(y))), %y. Inr(Inr(y)), z)) |
157 : ord_iso((A+B)+C, radd(A+B, radd(A,r,B,s), C, t), |
153 : ord_iso((A+B)+C, radd(A+B, radd(A,r,B,s), C, t), |
158 A+(B+C), radd(A, r, B+C, radd(B,s,C,t)))" |
154 A+(B+C), radd(A, r, B+C, radd(B,s,C,t)))" |
159 apply (rule sum_assoc_bij [THEN ord_isoI], auto) |
155 by (rule sum_assoc_bij [THEN ord_isoI], auto) |
160 done |
156 |
161 |
157 |
162 |
158 subsection{*Multiplication of Relations -- Lexicographic Product*} |
163 (**** Multiplication of relations -- lexicographic product ****) |
|
164 |
159 |
165 (** Rewrite rule. Can be used to obtain introduction rules **) |
160 (** Rewrite rule. Can be used to obtain introduction rules **) |
166 |
161 |
167 lemma rmult_iff [iff]: |
162 lemma rmult_iff [iff]: |
168 "<<a',b'>, <a,b>> : rmult(A,r,B,s) <-> |
163 "<<a',b'>, <a,b>> : rmult(A,r,B,s) <-> |
169 (<a',a>: r & a':A & a:A & b': B & b: B) | |
164 (<a',a>: r & a':A & a:A & b': B & b: B) | |
170 (<b',b>: s & a'=a & a:A & b': B & b: B)" |
165 (<b',b>: s & a'=a & a:A & b': B & b: B)" |
171 |
166 |
172 apply (unfold rmult_def, blast) |
167 by (unfold rmult_def, blast) |
173 done |
|
174 |
168 |
175 lemma rmultE: |
169 lemma rmultE: |
176 "[| <<a',b'>, <a,b>> : rmult(A,r,B,s); |
170 "[| <<a',b'>, <a,b>> : rmult(A,r,B,s); |
177 [| <a',a>: r; a':A; a:A; b':B; b:B |] ==> Q; |
171 [| <a',a>: r; a':A; a:A; b':B; b:B |] ==> Q; |
178 [| <b',b>: s; a:A; a'=a; b':B; b:B |] ==> Q |
172 [| <b',b>: s; a:A; a'=a; b':B; b:B |] ==> Q |
179 |] ==> Q" |
173 |] ==> Q" |
180 apply blast |
174 by blast |
181 done |
|
182 |
175 |
183 (** Type checking **) |
176 (** Type checking **) |
184 |
177 |
185 lemma rmult_type: "rmult(A,r,B,s) <= (A*B) * (A*B)" |
178 lemma rmult_type: "rmult(A,r,B,s) <= (A*B) * (A*B)" |
186 apply (unfold rmult_def) |
179 by (unfold rmult_def, rule Collect_subset) |
187 apply (rule Collect_subset) |
|
188 done |
|
189 |
180 |
190 lemmas field_rmult = rmult_type [THEN field_rel_subset] |
181 lemmas field_rmult = rmult_type [THEN field_rel_subset] |
191 |
182 |
192 (** Linearity **) |
183 (** Linearity **) |
193 |
184 |
194 lemma linear_rmult: |
185 lemma linear_rmult: |
195 "[| linear(A,r); linear(B,s) |] ==> linear(A*B,rmult(A,r,B,s))" |
186 "[| linear(A,r); linear(B,s) |] ==> linear(A*B,rmult(A,r,B,s))" |
196 apply (simp add: linear_def, blast) |
187 by (simp add: linear_def, blast) |
197 done |
|
198 |
188 |
199 (** Well-foundedness **) |
189 (** Well-foundedness **) |
200 |
190 |
201 lemma wf_on_rmult: "[| wf[A](r); wf[B](s) |] ==> wf[A*B](rmult(A,r,B,s))" |
191 lemma wf_on_rmult: "[| wf[A](r); wf[B](s) |] ==> wf[A*B](rmult(A,r,B,s))" |
202 apply (rule wf_onI2) |
192 apply (rule wf_onI2) |
287 (** Distributive law **) |
277 (** Distributive law **) |
288 |
278 |
289 lemma sum_prod_distrib_bij: |
279 lemma sum_prod_distrib_bij: |
290 "(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x)) |
280 "(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x)) |
291 : bij((A+B)*C, (A*C)+(B*C))" |
281 : bij((A+B)*C, (A*C)+(B*C))" |
292 apply (rule_tac d = "case (%<x,y>.<Inl (x),y>, %<x,y>.<Inr (x),y>) " |
282 by (rule_tac d = "case (%<x,y>.<Inl (x),y>, %<x,y>.<Inr (x),y>) " |
293 in lam_bijective) |
283 in lam_bijective, auto) |
294 apply auto |
|
295 done |
|
296 |
284 |
297 lemma sum_prod_distrib_ord_iso: |
285 lemma sum_prod_distrib_ord_iso: |
298 "(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x)) |
286 "(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x)) |
299 : ord_iso((A+B)*C, rmult(A+B, radd(A,r,B,s), C, t), |
287 : ord_iso((A+B)*C, rmult(A+B, radd(A,r,B,s), C, t), |
300 (A*C)+(B*C), radd(A*C, rmult(A,r,C,t), B*C, rmult(B,s,C,t)))" |
288 (A*C)+(B*C), radd(A*C, rmult(A,r,C,t), B*C, rmult(B,s,C,t)))" |
301 apply (rule sum_prod_distrib_bij [THEN ord_isoI], auto) |
289 by (rule sum_prod_distrib_bij [THEN ord_isoI], auto) |
302 done |
|
303 |
290 |
304 (** Associativity **) |
291 (** Associativity **) |
305 |
292 |
306 lemma prod_assoc_bij: |
293 lemma prod_assoc_bij: |
307 "(lam <<x,y>, z>:(A*B)*C. <x,<y,z>>) : bij((A*B)*C, A*(B*C))" |
294 "(lam <<x,y>, z>:(A*B)*C. <x,<y,z>>) : bij((A*B)*C, A*(B*C))" |
308 apply (rule_tac d = "%<x, <y,z>>. <<x,y>, z>" in lam_bijective, auto) |
295 by (rule_tac d = "%<x, <y,z>>. <<x,y>, z>" in lam_bijective, auto) |
309 done |
|
310 |
296 |
311 lemma prod_assoc_ord_iso: |
297 lemma prod_assoc_ord_iso: |
312 "(lam <<x,y>, z>:(A*B)*C. <x,<y,z>>) |
298 "(lam <<x,y>, z>:(A*B)*C. <x,<y,z>>) |
313 : ord_iso((A*B)*C, rmult(A*B, rmult(A,r,B,s), C, t), |
299 : ord_iso((A*B)*C, rmult(A*B, rmult(A,r,B,s), C, t), |
314 A*(B*C), rmult(A, r, B*C, rmult(B,s,C,t)))" |
300 A*(B*C), rmult(A, r, B*C, rmult(B,s,C,t)))" |
315 apply (rule prod_assoc_bij [THEN ord_isoI], auto) |
301 by (rule prod_assoc_bij [THEN ord_isoI], auto) |
316 done |
302 |
317 |
303 subsection{*Inverse Image of a Relation*} |
318 (**** Inverse image of a relation ****) |
|
319 |
304 |
320 (** Rewrite rule **) |
305 (** Rewrite rule **) |
321 |
306 |
322 lemma rvimage_iff: "<a,b> : rvimage(A,f,r) <-> <f`a,f`b>: r & a:A & b:A" |
307 lemma rvimage_iff: "<a,b> : rvimage(A,f,r) <-> <f`a,f`b>: r & a:A & b:A" |
323 by (unfold rvimage_def, blast) |
308 by (unfold rvimage_def, blast) |
324 |
309 |
325 (** Type checking **) |
310 (** Type checking **) |
326 |
311 |
327 lemma rvimage_type: "rvimage(A,f,r) <= A*A" |
312 lemma rvimage_type: "rvimage(A,f,r) <= A*A" |
328 apply (unfold rvimage_def) |
313 apply (unfold rvimage_def, rule Collect_subset) |
329 apply (rule Collect_subset) |
|
330 done |
314 done |
331 |
315 |
332 lemmas field_rvimage = rvimage_type [THEN field_rel_subset] |
316 lemmas field_rvimage = rvimage_type [THEN field_rel_subset] |
333 |
317 |
334 lemma rvimage_converse: "rvimage(A,f, converse(r)) = converse(rvimage(A,f,r))" |
318 lemma rvimage_converse: "rvimage(A,f, converse(r)) = converse(rvimage(A,f,r))" |