equal
deleted
inserted
replaced
449 assumes a: "Quotient R absf repf" |
449 assumes a: "Quotient R absf repf" |
450 shows "Bex (Respects R) ((absf ---> id) f) = Ex f" |
450 shows "Bex (Respects R) ((absf ---> id) f) = Ex f" |
451 using a unfolding Quotient_def Bex_def in_respects fun_map_def id_apply |
451 using a unfolding Quotient_def Bex_def in_respects fun_map_def id_apply |
452 by metis |
452 by metis |
453 |
453 |
454 section {* Bexeq quantifier *} |
454 section {* Bex1_rel quantifier *} |
455 |
455 |
456 definition |
456 definition |
457 Bexeq :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" |
457 Bex1_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" |
458 where |
458 where |
459 "Bexeq R P \<equiv> (\<exists>x \<in> Respects R. P x) \<and> (\<forall>x \<in> Respects R. \<forall>y \<in> Respects R. ((P x \<and> P y) \<longrightarrow> (R x y)))" |
459 "Bex1_rel R P \<equiv> (\<exists>x \<in> Respects R. P x) \<and> (\<forall>x \<in> Respects R. \<forall>y \<in> Respects R. ((P x \<and> P y) \<longrightarrow> (R x y)))" |
460 |
460 |
461 (* TODO/FIXME: simplify the repetitions in this proof *) |
461 (* TODO/FIXME: simplify the repetitions in this proof *) |
462 lemma bexeq_rsp: |
462 lemma bexeq_rsp: |
463 assumes a: "Quotient R absf repf" |
463 assumes a: "Quotient R absf repf" |
464 shows "((R ===> op =) ===> op =) (Bexeq R) (Bexeq R)" |
464 shows "((R ===> op =) ===> op =) (Bex1_rel R) (Bex1_rel R)" |
465 apply simp |
465 apply simp |
466 unfolding Bexeq_def |
466 unfolding Bex1_rel_def |
467 apply rule |
467 apply rule |
468 apply rule |
468 apply rule |
469 apply rule |
469 apply rule |
470 apply rule |
470 apply rule |
471 apply (erule conjE)+ |
471 apply (erule conjE)+ |
498 apply (metis in_respects) |
498 apply (metis in_respects) |
499 done |
499 done |
500 |
500 |
501 lemma ex1_prs: |
501 lemma ex1_prs: |
502 assumes a: "Quotient R absf repf" |
502 assumes a: "Quotient R absf repf" |
503 shows "((absf ---> id) ---> id) (Bexeq R) f = Ex1 f" |
503 shows "((absf ---> id) ---> id) (Bex1_rel R) f = Ex1 f" |
504 apply simp |
504 apply simp |
505 apply (subst Bexeq_def) |
505 apply (subst Bex1_rel_def) |
506 apply (subst Bex_def) |
506 apply (subst Bex_def) |
507 apply (subst Ex1_def) |
507 apply (subst Ex1_def) |
508 apply simp |
508 apply simp |
509 apply rule |
509 apply rule |
510 apply (erule conjE)+ |
510 apply (erule conjE)+ |
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))" |
538 lemma bex1_bexeq_reg: "(\<exists>!x\<in>Respects R. P x) \<longrightarrow> (Bex1_rel R (\<lambda>x. P x))" |
539 apply (simp add: Bex1_def Ex1_def Bexeq_def in_respects) |
539 apply (simp add: Bex1_def Ex1_def Bex1_rel_def in_respects) |
540 apply clarify |
540 apply clarify |
541 apply auto |
541 apply auto |
542 apply (rule bexI) |
542 apply (rule bexI) |
543 apply assumption |
543 apply assumption |
544 apply (simp add: in_respects) |
544 apply (simp add: in_respects) |