401 and a2: "(R1 ===> R2) g1 g2" |
401 and a2: "(R1 ===> R2) g1 g2" |
402 shows "(R1 ===> R3) (f1 o g1) (f2 o g2)" |
402 shows "(R1 ===> R3) (f1 o g1) (f2 o g2)" |
403 using a1 a2 unfolding o_def expand_fun_eq |
403 using a1 a2 unfolding o_def expand_fun_eq |
404 by (auto) |
404 by (auto) |
405 |
405 |
|
406 |
|
407 (* TODO: Put the following lemmas in proper places *) |
|
408 |
406 lemma equiv_res_forall: |
409 lemma equiv_res_forall: |
407 fixes P :: "'a \<Rightarrow> bool" |
410 fixes P :: "'a \<Rightarrow> bool" |
408 assumes a: "EQUIV E" |
411 assumes a: "EQUIV E" |
409 shows "Ball (Respects E) P = (All P)" |
412 shows "Ball (Respects E) P = (All P)" |
410 using a by (metis EQUIV_def IN_RESPECTS a) |
413 using a by (metis EQUIV_def IN_RESPECTS a) |
413 fixes P :: "'a \<Rightarrow> bool" |
416 fixes P :: "'a \<Rightarrow> bool" |
414 assumes a: "EQUIV E" |
417 assumes a: "EQUIV E" |
415 shows "Bex (Respects E) P = (Ex P)" |
418 shows "Bex (Respects E) P = (Ex P)" |
416 using a by (metis EQUIV_def IN_RESPECTS a) |
419 using a by (metis EQUIV_def IN_RESPECTS a) |
417 |
420 |
|
421 lemma FORALL_REGULAR: |
|
422 assumes a: "!x :: 'a. (P x --> Q x)" |
|
423 and b: "All P" |
|
424 shows "All Q" |
|
425 using a b by (metis) |
|
426 |
|
427 lemma EXISTS_REGULAR: |
|
428 assumes a: "!x :: 'a. (P x --> Q x)" |
|
429 and b: "Ex P" |
|
430 shows "Ex Q" |
|
431 using a b by (metis) |
|
432 |
|
433 lemma RES_FORALL_REGULAR: |
|
434 assumes a: "!x :: 'a. (R x --> P x --> Q x)" |
|
435 and b: "Ball R P" |
|
436 shows "Ball R Q" |
|
437 using a b by (metis COMBC_def Collect_def Collect_mem_eq) |
|
438 |
|
439 lemma RES_EXISTS_REGULAR: |
|
440 assumes a: "!x :: 'a. (R x --> P x --> Q x)" |
|
441 and b: "Bex R P" |
|
442 shows "Bex R Q" |
|
443 using a b by (metis COMBC_def Collect_def Collect_mem_eq) |
|
444 |
|
445 lemma LEFT_RES_FORALL_REGULAR: |
|
446 assumes a: "!x. (R x \<and> (Q x --> P x))" |
|
447 shows "Ball R Q ==> All P" |
|
448 using a |
|
449 apply (metis COMBC_def Collect_def Collect_mem_eq a) |
|
450 done |
|
451 |
|
452 lemma RIGHT_RES_FORALL_REGULAR: |
|
453 assumes a: "!x :: 'a. (R x --> P x --> Q x)" |
|
454 shows "All P ==> Ball R Q" |
|
455 using a |
|
456 apply (metis COMBC_def Collect_def Collect_mem_eq a) |
|
457 done |
|
458 |
|
459 lemma LEFT_RES_EXISTS_REGULAR: |
|
460 assumes a: "!x :: 'a. (R x --> Q x --> P x)" |
|
461 shows "Bex R Q ==> Ex P" |
|
462 using a by (metis COMBC_def Collect_def Collect_mem_eq) |
|
463 |
|
464 lemma RIGHT_RES_EXISTS_REGULAR: |
|
465 assumes a: "!x :: 'a. (R x \<and> (P x --> Q x))" |
|
466 shows "Ex P \<Longrightarrow> Bex R Q" |
|
467 using a by (metis COMBC_def Collect_def Collect_mem_eq) |
|
468 |
418 end |
469 end |
419 |
470 |