equal
deleted
inserted
replaced
533 apply rule+ |
533 apply rule+ |
534 using a unfolding Quotient_def in_respects |
534 using a unfolding Quotient_def in_respects |
535 apply metis |
535 apply metis |
536 done |
536 done |
537 |
537 |
|
538 lemma bex1_bexeq_reg: "(\<exists>!x\<in>Respects R. P x) \<longrightarrow> (Bexeq R (\<lambda>x. P x))" |
|
539 apply (simp add: Bex1_def Ex1_def Bexeq_def in_respects) |
|
540 apply clarify |
|
541 apply auto |
|
542 apply (rule bexI) |
|
543 apply assumption |
|
544 apply (simp add: in_respects) |
|
545 apply (simp add: in_respects) |
|
546 apply auto |
|
547 done |
|
548 |
538 section {* Various respects and preserve lemmas *} |
549 section {* Various respects and preserve lemmas *} |
539 |
550 |
540 lemma quot_rel_rsp: |
551 lemma quot_rel_rsp: |
541 assumes a: "Quotient R Abs Rep" |
552 assumes a: "Quotient R Abs Rep" |
542 shows "(R ===> R ===> op =) R R" |
553 shows "(R ===> R ===> op =) R R" |