264 lemma EQUALS_PRS: |
264 lemma EQUALS_PRS: |
265 assumes q: "QUOTIENT R Abs Rep" |
265 assumes q: "QUOTIENT R Abs Rep" |
266 shows "(x = y) = R (Rep x) (Rep y)" |
266 shows "(x = y) = R (Rep x) (Rep y)" |
267 by (rule QUOTIENT_REL_REP[OF q, symmetric]) |
267 by (rule QUOTIENT_REL_REP[OF q, symmetric]) |
268 |
268 |
269 lemma EQUALS_RSP: |
269 lemma equals_rsp: |
270 assumes q: "QUOTIENT R Abs Rep" |
270 assumes q: "QUOTIENT R Abs Rep" |
271 and a: "R xa xb" "R ya yb" |
271 and a: "R xa xb" "R ya yb" |
272 shows "R xa ya = R xb yb" |
272 shows "R xa ya = R xb yb" |
273 using QUOTIENT_SYM[OF q] QUOTIENT_TRANS[OF q] unfolding SYM_def TRANS_def |
273 using QUOTIENT_SYM[OF q] QUOTIENT_TRANS[OF q] unfolding SYM_def TRANS_def |
274 using a by blast |
274 using a by blast |
275 |
275 |
276 lemma LAMBDA_PRS: |
276 lemma lambda_prs: |
277 assumes q1: "QUOTIENT R1 Abs1 Rep1" |
277 assumes q1: "QUOTIENT R1 Abs1 Rep1" |
278 and q2: "QUOTIENT R2 Abs2 Rep2" |
278 and q2: "QUOTIENT R2 Abs2 Rep2" |
279 shows "(Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) = (\<lambda>x. f x)" |
279 shows "(Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) = (\<lambda>x. f x)" |
280 unfolding expand_fun_eq |
280 unfolding expand_fun_eq |
281 using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2] |
281 using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2] |
282 by simp |
282 by simp |
283 |
283 |
284 lemma LAMBDA_PRS1: |
284 lemma lambda_prs1: |
285 assumes q1: "QUOTIENT R1 Abs1 Rep1" |
285 assumes q1: "QUOTIENT R1 Abs1 Rep1" |
286 and q2: "QUOTIENT R2 Abs2 Rep2" |
286 and q2: "QUOTIENT R2 Abs2 Rep2" |
287 shows "(\<lambda>x. f x) = (Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x)" |
287 shows "(Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x) = (\<lambda>x. f x)" |
288 unfolding expand_fun_eq |
288 unfolding expand_fun_eq |
289 using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2] |
289 using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2] |
290 by simp |
290 by simp |
291 |
291 |
292 (* Not used since applic_prs proves a version for an arbitrary number of arguments *) |
292 (* Not used since applic_prs proves a version for an arbitrary number of arguments *) |
332 shows "R x1 (Rep (Abs x2))" |
332 shows "R x1 (Rep (Abs x2))" |
333 using q a by (metis QUOTIENT_REL[OF q] QUOTIENT_ABS_REP[OF q] QUOTIENT_REP_REFL[OF q]) |
333 using q a by (metis QUOTIENT_REL[OF q] QUOTIENT_ABS_REP[OF q] QUOTIENT_REP_REFL[OF q]) |
334 |
334 |
335 (* ----------------------------------------------------- *) |
335 (* ----------------------------------------------------- *) |
336 (* Quantifiers: FORALL, EXISTS, EXISTS_UNIQUE, *) |
336 (* Quantifiers: FORALL, EXISTS, EXISTS_UNIQUE, *) |
337 (* RES_FORALL, RES_EXISTS, RES_EXISTS_EQUIV *) |
337 (* Ball, Bex, RES_EXISTS_EQUIV *) |
338 (* ----------------------------------------------------- *) |
338 (* ----------------------------------------------------- *) |
339 |
339 |
340 (* bool theory: COND, LET *) |
340 (* bool theory: COND, LET *) |
341 |
341 |
342 lemma IF_PRS: |
342 lemma IF_PRS: |
372 (* literal_case_RSP *) |
372 (* literal_case_RSP *) |
373 |
373 |
374 |
374 |
375 (* FUNCTION APPLICATION *) |
375 (* FUNCTION APPLICATION *) |
376 |
376 |
|
377 (* Not used *) |
377 lemma APPLY_PRS: |
378 lemma APPLY_PRS: |
378 assumes q1: "QUOTIENT R1 Abs1 Rep1" |
379 assumes q1: "QUOTIENT R1 Abs1 Rep1" |
379 and q2: "QUOTIENT R2 Abs2 Rep2" |
380 and q2: "QUOTIENT R2 Abs2 Rep2" |
380 shows "f x = Abs2 (((Abs1 ---> Rep2) f) (Rep1 x))" |
381 shows "f x = Abs2 (((Abs1 ---> Rep2) f) (Rep1 x))" |
381 using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2] by auto |
382 using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2] by auto |
382 |
383 |
383 (* ask peter: no use of q1 q2 *) |
384 (* In the following theorem R1 can be instantiated with anything, |
384 (* Cez: I can answer, |
|
385 In the following theorem R2 can be instantiated with anything, |
|
386 but we know some of the types of the Rep and Abs functions; |
385 but we know some of the types of the Rep and Abs functions; |
387 so by solving QUOTIENT assumptions we can get a unique R2 that |
386 so by solving QUOTIENT assumptions we can get a unique R2 that |
388 will be provable; which is why we need to use APPLY_RSP1 *) |
387 will be provable; which is why we need to use APPLY_RSP *) |
389 lemma APPLY_RSP: |
388 lemma apply_rsp: |
390 assumes q1: "QUOTIENT R1 Abs1 Rep1" |
|
391 and q2: "QUOTIENT R2 Abs2 Rep2" |
|
392 and a: "(R1 ===> R2) f g" "R1 x y" |
|
393 shows "R2 (f x) (g y)" |
|
394 using a by (rule FUN_REL_IMP) |
|
395 |
|
396 lemma APPLY_RSP1: |
|
397 assumes q: "QUOTIENT R1 Abs1 Rep1" |
389 assumes q: "QUOTIENT R1 Abs1 Rep1" |
398 and a: "(R1 ===> R2) f g" "R1 x y" |
390 and a: "(R1 ===> R2) f g" "R1 x y" |
399 shows "R2 ((f::'a\<Rightarrow>'c) x) ((g::'a\<Rightarrow>'c) y)" |
391 shows "R2 ((f::'a\<Rightarrow>'c) x) ((g::'a\<Rightarrow>'c) y)" |
400 using a by (rule FUN_REL_IMP) |
392 using a by (rule FUN_REL_IMP) |
401 |
393 |
402 lemma APPLY_RSP2: |
394 lemma apply_rsp': |
403 assumes a: "(R1 ===> R2) f g" "R1 x y" |
395 assumes a: "(R1 ===> R2) f g" "R1 x y" |
404 shows "R2 (f x) (g y)" |
396 shows "R2 (f x) (g y)" |
405 using a by (rule FUN_REL_IMP) |
397 using a by (rule FUN_REL_IMP) |
406 |
398 |
407 |
399 |