692 assumes Rep1: "\<And>x y. R2 x y \<Longrightarrow> R2' (Rep1 x) (Rep1 y)" |
692 assumes Rep1: "\<And>x y. R2 x y \<Longrightarrow> R2' (Rep1 x) (Rep1 y)" |
693 shows "Quotient3 (R1 OO R2' OO R1) (Abs2 \<circ> Abs1) (Rep1 \<circ> Rep2)" |
693 shows "Quotient3 (R1 OO R2' OO R1) (Abs2 \<circ> Abs1) (Rep1 \<circ> Rep2)" |
694 apply (rule Quotient3I) |
694 apply (rule Quotient3I) |
695 apply (simp add: o_def Quotient3_abs_rep [OF R2] Quotient3_abs_rep [OF R1]) |
695 apply (simp add: o_def Quotient3_abs_rep [OF R2] Quotient3_abs_rep [OF R1]) |
696 apply simp |
696 apply simp |
697 apply (rule_tac b="Rep1 (Rep2 a)" in pred_compI) |
697 apply (rule_tac b="Rep1 (Rep2 a)" in relcomppI) |
698 apply (rule Quotient3_rep_reflp [OF R1]) |
698 apply (rule Quotient3_rep_reflp [OF R1]) |
699 apply (rule_tac b="Rep1 (Rep2 a)" in pred_compI [rotated]) |
699 apply (rule_tac b="Rep1 (Rep2 a)" in relcomppI [rotated]) |
700 apply (rule Quotient3_rep_reflp [OF R1]) |
700 apply (rule Quotient3_rep_reflp [OF R1]) |
701 apply (rule Rep1) |
701 apply (rule Rep1) |
702 apply (rule Quotient3_rep_reflp [OF R2]) |
702 apply (rule Quotient3_rep_reflp [OF R2]) |
703 apply safe |
703 apply safe |
704 apply (rename_tac x y) |
704 apply (rename_tac x y) |
705 apply (drule Abs1) |
705 apply (drule Abs1) |
706 apply (erule Quotient3_refl2 [OF R1]) |
706 apply (erule Quotient3_refl2 [OF R1]) |
707 apply (erule Quotient3_refl1 [OF R1]) |
707 apply (erule Quotient3_refl1 [OF R1]) |
708 apply (drule Quotient3_refl1 [OF R2], drule Rep1) |
708 apply (drule Quotient3_refl1 [OF R2], drule Rep1) |
709 apply (subgoal_tac "R1 r (Rep1 (Abs1 x))") |
709 apply (subgoal_tac "R1 r (Rep1 (Abs1 x))") |
710 apply (rule_tac b="Rep1 (Abs1 x)" in pred_compI, assumption) |
710 apply (rule_tac b="Rep1 (Abs1 x)" in relcomppI, assumption) |
711 apply (erule pred_compI) |
711 apply (erule relcomppI) |
712 apply (erule Quotient3_symp [OF R1, THEN sympD]) |
712 apply (erule Quotient3_symp [OF R1, THEN sympD]) |
713 apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2]) |
713 apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2]) |
714 apply (rule conjI, erule Quotient3_refl1 [OF R1]) |
714 apply (rule conjI, erule Quotient3_refl1 [OF R1]) |
715 apply (rule conjI, rule Quotient3_rep_reflp [OF R1]) |
715 apply (rule conjI, rule Quotient3_rep_reflp [OF R1]) |
716 apply (subst Quotient3_abs_rep [OF R1]) |
716 apply (subst Quotient3_abs_rep [OF R1]) |
719 apply (drule Abs1) |
719 apply (drule Abs1) |
720 apply (erule Quotient3_refl2 [OF R1]) |
720 apply (erule Quotient3_refl2 [OF R1]) |
721 apply (erule Quotient3_refl1 [OF R1]) |
721 apply (erule Quotient3_refl1 [OF R1]) |
722 apply (drule Quotient3_refl2 [OF R2], drule Rep1) |
722 apply (drule Quotient3_refl2 [OF R2], drule Rep1) |
723 apply (subgoal_tac "R1 s (Rep1 (Abs1 y))") |
723 apply (subgoal_tac "R1 s (Rep1 (Abs1 y))") |
724 apply (rule_tac b="Rep1 (Abs1 y)" in pred_compI, assumption) |
724 apply (rule_tac b="Rep1 (Abs1 y)" in relcomppI, assumption) |
725 apply (erule pred_compI) |
725 apply (erule relcomppI) |
726 apply (erule Quotient3_symp [OF R1, THEN sympD]) |
726 apply (erule Quotient3_symp [OF R1, THEN sympD]) |
727 apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2]) |
727 apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2]) |
728 apply (rule conjI, erule Quotient3_refl2 [OF R1]) |
728 apply (rule conjI, erule Quotient3_refl2 [OF R1]) |
729 apply (rule conjI, rule Quotient3_rep_reflp [OF R1]) |
729 apply (rule conjI, rule Quotient3_rep_reflp [OF R1]) |
730 apply (subst Quotient3_abs_rep [OF R1]) |
730 apply (subst Quotient3_abs_rep [OF R1]) |
736 apply (erule Abs1) |
736 apply (erule Abs1) |
737 apply (erule Quotient3_refl2 [OF R1]) |
737 apply (erule Quotient3_refl2 [OF R1]) |
738 apply (erule Quotient3_refl1 [OF R1]) |
738 apply (erule Quotient3_refl1 [OF R1]) |
739 apply (rename_tac a b c d) |
739 apply (rename_tac a b c d) |
740 apply simp |
740 apply simp |
741 apply (rule_tac b="Rep1 (Abs1 r)" in pred_compI) |
741 apply (rule_tac b="Rep1 (Abs1 r)" in relcomppI) |
742 apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2]) |
742 apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2]) |
743 apply (rule conjI, erule Quotient3_refl1 [OF R1]) |
743 apply (rule conjI, erule Quotient3_refl1 [OF R1]) |
744 apply (simp add: Quotient3_abs_rep [OF R1] Quotient3_rep_reflp [OF R1]) |
744 apply (simp add: Quotient3_abs_rep [OF R1] Quotient3_rep_reflp [OF R1]) |
745 apply (rule_tac b="Rep1 (Abs1 s)" in pred_compI [rotated]) |
745 apply (rule_tac b="Rep1 (Abs1 s)" in relcomppI [rotated]) |
746 apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2]) |
746 apply (rule Quotient3_rel[symmetric, OF R1, THEN iffD2]) |
747 apply (simp add: Quotient3_abs_rep [OF R1] Quotient3_rep_reflp [OF R1]) |
747 apply (simp add: Quotient3_abs_rep [OF R1] Quotient3_rep_reflp [OF R1]) |
748 apply (erule Quotient3_refl2 [OF R1]) |
748 apply (erule Quotient3_refl2 [OF R1]) |
749 apply (rule Rep1) |
749 apply (rule Rep1) |
750 apply (drule Abs1) |
750 apply (drule Abs1) |