272 using a by blast |
272 using a by blast |
273 |
273 |
274 lemma LAMBDA_PRS: |
274 lemma LAMBDA_PRS: |
275 assumes q1: "QUOTIENT R1 Abs1 Rep1" |
275 assumes q1: "QUOTIENT R1 Abs1 Rep1" |
276 and q2: "QUOTIENT R2 Abs2 Rep2" |
276 and q2: "QUOTIENT R2 Abs2 Rep2" |
277 shows "(\<lambda>x. f x) = (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x)))" |
277 shows "(Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) = (\<lambda>x. f x)" |
278 unfolding expand_fun_eq |
278 unfolding expand_fun_eq |
279 using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2] |
279 using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2] |
280 by simp |
280 by simp |
281 |
281 |
282 lemma LAMBDA_PRS1: |
282 lemma LAMBDA_PRS1: |
283 assumes q1: "QUOTIENT R1 Abs1 Rep1" |
283 assumes q1: "QUOTIENT R1 Abs1 Rep1" |
284 and q2: "QUOTIENT R2 Abs2 Rep2" |
284 and q2: "QUOTIENT R2 Abs2 Rep2" |
285 shows "(\<lambda>x. f x) = (Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x)" |
285 shows "(\<lambda>x. f x) = (Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x)" |
286 unfolding expand_fun_eq |
286 unfolding expand_fun_eq |
287 by (subst LAMBDA_PRS[OF q1 q2]) (simp) |
287 using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2] |
|
288 by (simp) |
|
289 |
|
290 lemma APP_PRS: |
|
291 assumes q1: "QUOTIENT R1 abs1 rep1" |
|
292 and q2: "QUOTIENT R2 abs2 rep2" |
|
293 shows "abs2 ((abs1 ---> rep2) f (rep1 x)) = f x" |
|
294 unfolding expand_fun_eq |
|
295 using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2] |
|
296 by simp |
288 |
297 |
289 (* Ask Peter: assumption q1 and q2 not used and lemma is the 'identity' *) |
298 (* Ask Peter: assumption q1 and q2 not used and lemma is the 'identity' *) |
290 lemma LAMBDA_RSP: |
299 lemma LAMBDA_RSP: |
291 assumes q1: "QUOTIENT R1 Abs1 Rep1" |
300 assumes q1: "QUOTIENT R1 Abs1 Rep1" |
292 and q2: "QUOTIENT R2 Abs2 Rep2" |
301 and q2: "QUOTIENT R2 Abs2 Rep2" |