250 |
250 |
251 lemma rep_abs_rsp: |
251 lemma rep_abs_rsp: |
252 assumes q: "Quotient R Abs Rep" |
252 assumes q: "Quotient R Abs Rep" |
253 and a: "R x1 x2" |
253 and a: "R x1 x2" |
254 shows "R x1 (Rep (Abs x2))" |
254 shows "R x1 (Rep (Abs x2))" |
255 using a |
255 using a |
256 by (metis Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q]) |
256 by (metis Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q]) |
257 |
257 |
258 lemma rep_abs_rsp_left: |
258 lemma rep_abs_rsp_left: |
259 assumes q: "Quotient R Abs Rep" |
259 assumes q: "Quotient R Abs Rep" |
260 and a: "R x1 x2" |
260 and a: "R x1 x2" |
261 shows "R (Rep (Abs x1)) x2" |
261 shows "R (Rep (Abs x1)) x2" |
262 using a |
262 using a |
263 by (metis Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q]) |
263 by (metis Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q]) |
264 |
264 |
265 (* In the following theorem R1 can be instantiated with anything, |
265 (* In the following theorem R1 can be instantiated with anything, |
266 but we know some of the types of the Rep and Abs functions; |
266 but we know some of the types of the Rep and Abs functions; |
267 so by solving Quotient assumptions we can get a unique R1 that |
267 so by solving Quotient assumptions we can get a unique R1 that |
268 will be provable; which is why we need to use apply_rsp and |
268 will be provable; which is why we need to use apply_rsp and |
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 "Ex1 (\<lambda>x. x \<in> Respects R \<and> f x) = Ex1 (\<lambda>x. x \<in> Respects R \<and> g x)" |
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 in_respects) auto |
439 by (simp add: Ex1_def in_respects) auto |
440 |
440 |
441 (* 3 lemmas needed for cleaning of quantifiers *) |
441 (* 2 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" |
445 using a unfolding Quotient_def Ball_def in_respects fun_map_def id_apply |
445 using a unfolding Quotient_def Ball_def in_respects fun_map_def id_apply |
446 by metis |
446 by metis |
447 |
447 |
448 lemma ex_prs: |
448 lemma ex_prs: |
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 |
456 definition |
456 definition |
457 Bex1_rel :: "('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 "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)))" |
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 lemma bex1_rel_aux: |
462 lemma bexeq_rsp: |
462 "\<lbrakk>\<forall>xa ya. R xa ya \<longrightarrow> x xa = y ya; Bex1_rel R x\<rbrakk> \<Longrightarrow> Bex1_rel R y" |
|
463 unfolding Bex1_rel_def |
|
464 apply (erule conjE)+ |
|
465 apply (erule bexE) |
|
466 apply rule |
|
467 apply (rule_tac x="xa" in bexI) |
|
468 apply metis |
|
469 apply metis |
|
470 apply rule+ |
|
471 apply (erule_tac x="xaa" in ballE) |
|
472 prefer 2 |
|
473 apply (metis) |
|
474 apply (erule_tac x="ya" in ballE) |
|
475 prefer 2 |
|
476 apply (metis) |
|
477 apply (metis in_respects) |
|
478 done |
|
479 |
|
480 lemma bex1_rel_aux2: |
|
481 "\<lbrakk>\<forall>xa ya. R xa ya \<longrightarrow> x xa = y ya; Bex1_rel R y\<rbrakk> \<Longrightarrow> Bex1_rel R x" |
|
482 unfolding Bex1_rel_def |
|
483 apply (erule conjE)+ |
|
484 apply (erule bexE) |
|
485 apply rule |
|
486 apply (rule_tac x="xa" in bexI) |
|
487 apply metis |
|
488 apply metis |
|
489 apply rule+ |
|
490 apply (erule_tac x="xaa" in ballE) |
|
491 prefer 2 |
|
492 apply (metis) |
|
493 apply (erule_tac x="ya" in ballE) |
|
494 prefer 2 |
|
495 apply (metis) |
|
496 apply (metis in_respects) |
|
497 done |
|
498 |
|
499 lemma bex1_rel_rsp: |
463 assumes a: "Quotient R absf repf" |
500 assumes a: "Quotient R absf repf" |
464 shows "((R ===> op =) ===> op =) (Bex1_rel R) (Bex1_rel R)" |
501 shows "((R ===> op =) ===> op =) (Bex1_rel R) (Bex1_rel R)" |
465 apply simp |
502 apply simp |
466 unfolding Bex1_rel_def |
503 apply clarify |
467 apply rule |
504 apply rule |
468 apply rule |
505 apply (simp_all add: bex1_rel_aux bex1_rel_aux2) |
469 apply rule |
506 apply (erule bex1_rel_aux2) |
470 apply rule |
507 apply assumption |
471 apply (erule conjE)+ |
508 done |
472 apply (erule bexE) |
509 |
473 apply rule |
|
474 apply (rule_tac x="xa" in bexI) |
|
475 apply metis |
|
476 apply metis |
|
477 apply rule+ |
|
478 apply (erule_tac x="xb" in ballE) |
|
479 prefer 2 |
|
480 apply (metis) |
|
481 apply (erule_tac x="ya" in ballE) |
|
482 prefer 2 |
|
483 apply (metis) |
|
484 apply (metis in_respects) |
|
485 apply (erule conjE)+ |
|
486 apply (erule bexE) |
|
487 apply rule |
|
488 apply (rule_tac x="xa" in bexI) |
|
489 apply metis |
|
490 apply metis |
|
491 apply rule+ |
|
492 apply (erule_tac x="xb" in ballE) |
|
493 prefer 2 |
|
494 apply (metis) |
|
495 apply (erule_tac x="ya" in ballE) |
|
496 prefer 2 |
|
497 apply (metis) |
|
498 apply (metis in_respects) |
|
499 done |
|
500 |
510 |
501 lemma ex1_prs: |
511 lemma ex1_prs: |
502 assumes a: "Quotient R absf repf" |
512 assumes a: "Quotient R absf repf" |
503 shows "((absf ---> id) ---> id) (Bex1_rel R) f = Ex1 f" |
513 shows "((absf ---> id) ---> id) (Bex1_rel R) f = Ex1 f" |
504 apply simp |
514 apply simp |
510 apply (erule conjE)+ |
520 apply (erule conjE)+ |
511 apply (erule_tac exE) |
521 apply (erule_tac exE) |
512 apply (erule conjE) |
522 apply (erule conjE) |
513 apply (subgoal_tac "\<forall>y. R y y \<longrightarrow> f (absf y) \<longrightarrow> R x y") |
523 apply (subgoal_tac "\<forall>y. R y y \<longrightarrow> f (absf y) \<longrightarrow> R x y") |
514 apply (rule_tac x="absf x" in exI) |
524 apply (rule_tac x="absf x" in exI) |
515 apply (thin_tac "\<forall>x\<in>Respects R. \<forall>y\<in>Respects R. f (absf x) \<and> f (absf y) \<longrightarrow> R x y") |
|
516 apply (simp) |
525 apply (simp) |
517 apply rule+ |
526 apply rule+ |
518 using a unfolding Quotient_def |
527 using a unfolding Quotient_def |
519 apply metis |
528 apply metis |
520 apply rule+ |
529 apply rule+ |
580 using a unfolding Quotient_def by auto |
589 using a unfolding Quotient_def by auto |
581 |
590 |
582 lemma if_prs: |
591 lemma if_prs: |
583 assumes q: "Quotient R Abs Rep" |
592 assumes q: "Quotient R Abs Rep" |
584 shows "Abs (If a (Rep b) (Rep c)) = If a b c" |
593 shows "Abs (If a (Rep b) (Rep c)) = If a b c" |
585 using Quotient_abs_rep[OF q] by auto |
594 using Quotient_abs_rep[OF q] by auto |
586 |
595 |
587 (* q not used *) |
596 (* q not used *) |
588 lemma if_rsp: |
597 lemma if_rsp: |
589 assumes q: "Quotient R Abs Rep" |
598 assumes q: "Quotient R Abs Rep" |
590 and a: "a1 = a2" "R b1 b2" "R c1 c2" |
599 and a: "a1 = a2" "R b1 b2" "R c1 c2" |
591 shows "R (If a1 b1 c1) (If a2 b2 c2)" |
600 shows "R (If a1 b1 c1) (If a2 b2 c2)" |
592 using a by auto |
601 using a by auto |
593 |
602 |
594 lemma let_prs: |
603 lemma let_prs: |
595 assumes q1: "Quotient R1 Abs1 Rep1" |
604 assumes q1: "Quotient R1 Abs1 Rep1" |
596 and q2: "Quotient R2 Abs2 Rep2" |
605 and q2: "Quotient R2 Abs2 Rep2" |
597 shows "Abs2 (Let (Rep1 x) ((Abs1 ---> Rep2) f)) = Let x f" |
606 shows "Abs2 (Let (Rep1 x) ((Abs1 ---> Rep2) f)) = Let x f" |
603 and a2: "R1 x y" |
612 and a2: "R1 x y" |
604 shows "R2 ((Let x f)::'c) ((Let y g)::'c)" |
613 shows "R2 ((Let x f)::'c) ((Let y g)::'c)" |
605 using apply_rsp[OF q1 a1] a2 by auto |
614 using apply_rsp[OF q1 a1] a2 by auto |
606 |
615 |
607 |
616 |
608 (******************************************) |
617 (*** REST OF THE FILE IS UNUSED (until now) ***) |
609 (* REST OF THE FILE IS UNUSED (until now) *) |
|
610 (******************************************) |
|
611 |
618 |
612 text {* |
619 text {* |
613 lemma in_fun: |
620 lemma in_fun: |
614 shows "x \<in> ((f ---> g) s) = g (f x \<in> s)" |
621 shows "x \<in> ((f ---> g) s) = g (f x \<in> s)" |
615 by (simp add: mem_def) |
622 by (simp add: mem_def) |
616 |
623 |
617 lemma respects_thm: |
624 lemma respects_thm: |
618 shows "Respects (R1 ===> R2) f = (\<forall>x y. R1 x y \<longrightarrow> R2 (f x) (f y))" |
625 shows "Respects (R1 ===> R2) f = (\<forall>x y. R1 x y \<longrightarrow> R2 (f x) (f y))" |
619 unfolding Respects_def |
626 unfolding Respects_def |
620 by (simp add: expand_fun_eq) |
627 by (simp add: expand_fun_eq) |
621 |
628 |
655 |
662 |
656 lemma fun_rel_equals: |
663 lemma fun_rel_equals: |
657 assumes q1: "Quotient R1 Abs1 Rep1" |
664 assumes q1: "Quotient R1 Abs1 Rep1" |
658 and q2: "Quotient R2 Abs2 Rep2" |
665 and q2: "Quotient R2 Abs2 Rep2" |
659 and r1: "Respects (R1 ===> R2) f" |
666 and r1: "Respects (R1 ===> R2) f" |
660 and r2: "Respects (R1 ===> R2) g" |
667 and r2: "Respects (R1 ===> R2) g" |
661 shows "((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g) = (\<forall>x y. R1 x y \<longrightarrow> R2 (f x) (g y))" |
668 shows "((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g) = (\<forall>x y. R1 x y \<longrightarrow> R2 (f x) (g y))" |
662 apply(rule_tac iffI) |
669 apply(rule_tac iffI) |
663 apply(rule)+ |
670 apply(rule)+ |
664 apply (rule apply_rsp'[of "R1" "R2"]) |
671 apply (rule apply_rsp'[of "R1" "R2"]) |
665 apply(subst Quotient_rel[OF fun_quotient[OF q1 q2]]) |
672 apply(subst Quotient_rel[OF fun_quotient[OF q1 q2]]) |
687 assumes r1: "\<And>r r'. R1 r r' \<Longrightarrow>R1 r (Rep1 (Abs1 r'))" |
694 assumes r1: "\<And>r r'. R1 r r' \<Longrightarrow>R1 r (Rep1 (Abs1 r'))" |
688 and r2: "\<And>r r'. R2 r r' \<Longrightarrow>R2 r (Rep2 (Abs2 r'))" |
695 and r2: "\<And>r r'. R2 r r' \<Longrightarrow>R2 r (Rep2 (Abs2 r'))" |
689 shows "(R1 ===> R2) f1 f2 \<Longrightarrow> (R1 ===> R2) f1 ((Abs1 ---> Rep2) ((Rep1 ---> Abs2) f2))" |
696 shows "(R1 ===> R2) f1 f2 \<Longrightarrow> (R1 ===> R2) f1 ((Abs1 ---> Rep2) ((Rep1 ---> Abs2) f2))" |
690 using r1 r2 by auto |
697 using r1 r2 by auto |
691 |
698 |
692 (* ask peter what are literal_case *) |
|
693 (* literal_case_PRS *) |
|
694 (* literal_case_RSP *) |
|
695 (* Cez: !f x. literal_case f x = f x *) |
|
696 |
|
697 (* We use id_simps which includes id_apply; so these 2 theorems can be removed *) |
699 (* We use id_simps which includes id_apply; so these 2 theorems can be removed *) |
698 lemma id_prs: |
700 lemma id_prs: |
699 assumes q: "Quotient R Abs Rep" |
701 assumes q: "Quotient R Abs Rep" |
700 shows "Abs (id (Rep e)) = id e" |
702 shows "Abs (id (Rep e)) = id e" |
701 using Quotient_abs_rep[OF q] by auto |
703 using Quotient_abs_rep[OF q] by auto |