equal
deleted
inserted
replaced
432 shows "(Bex (Respects R) f = Bex (Respects R) g)" |
432 shows "(Bex (Respects R) f = Bex (Respects R) g)" |
433 using a by (simp add: Bex_def in_respects) |
433 using a by (simp add: Bex_def in_respects) |
434 |
434 |
435 lemma bex1_rsp: |
435 lemma bex1_rsp: |
436 assumes a: "(R ===> (op =)) f g" |
436 assumes a: "(R ===> (op =)) f g" |
437 shows "(Bex1 (Respects R) f = Bex1 (Respects R) g)" |
437 shows "Ex1 (\<lambda>x. x \<in> Respects R \<and> f x) = Ex1 (\<lambda>x. x \<in> Respects R \<and> g x)" |
438 using a |
438 using a |
439 by (simp add: Ex1_def Bex1_def in_respects) auto |
439 by (simp add: Ex1_def in_respects) auto |
440 |
440 |
441 (* 3 lemmas needed for cleaning of quantifiers *) |
441 (* 3 lemmas needed for cleaning of quantifiers *) |
442 lemma all_prs: |
442 lemma all_prs: |
443 assumes a: "Quotient R absf repf" |
443 assumes a: "Quotient R absf repf" |
444 shows "Ball (Respects R) ((absf ---> id) f) = All f" |
444 shows "Ball (Respects R) ((absf ---> id) f) = All f" |
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> (Bex1_rel 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 Bex1_rel_def in_respects) |
539 apply (simp add: 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) |