src/HOL/Quotient.thy
changeset 47434 b75ce48a93ee
parent 47105 e64ffc96a49f
child 47435 e1b761c216ac
equal deleted inserted replaced
47433:07f4bf913230 47434:b75ce48a93ee
   715   assumes Rep1: "\<And>x y. R2 x y \<Longrightarrow> R2' (Rep1 x) (Rep1 y)"
   715   assumes Rep1: "\<And>x y. R2 x y \<Longrightarrow> R2' (Rep1 x) (Rep1 y)"
   716   shows "Quotient (R1 OO R2' OO R1) (Abs2 \<circ> Abs1) (Rep1 \<circ> Rep2)"
   716   shows "Quotient (R1 OO R2' OO R1) (Abs2 \<circ> Abs1) (Rep1 \<circ> Rep2)"
   717 apply (rule QuotientI)
   717 apply (rule QuotientI)
   718    apply (simp add: o_def Quotient_abs_rep [OF R2] Quotient_abs_rep [OF R1])
   718    apply (simp add: o_def Quotient_abs_rep [OF R2] Quotient_abs_rep [OF R1])
   719   apply simp
   719   apply simp
   720   apply (rule_tac b="Rep1 (Rep2 a)" in pred_compI)
   720   apply (rule_tac b="Rep1 (Rep2 a)" in relcomppI)
   721    apply (rule Quotient_rep_reflp [OF R1])
   721    apply (rule Quotient_rep_reflp [OF R1])
   722   apply (rule_tac b="Rep1 (Rep2 a)" in pred_compI [rotated])
   722   apply (rule_tac b="Rep1 (Rep2 a)" in relcomppI [rotated])
   723    apply (rule Quotient_rep_reflp [OF R1])
   723    apply (rule Quotient_rep_reflp [OF R1])
   724   apply (rule Rep1)
   724   apply (rule Rep1)
   725   apply (rule Quotient_rep_reflp [OF R2])
   725   apply (rule Quotient_rep_reflp [OF R2])
   726  apply safe
   726  apply safe
   727     apply (rename_tac x y)
   727     apply (rename_tac x y)
   728     apply (drule Abs1)
   728     apply (drule Abs1)
   729       apply (erule Quotient_refl2 [OF R1])
   729       apply (erule Quotient_refl2 [OF R1])
   730      apply (erule Quotient_refl1 [OF R1])
   730      apply (erule Quotient_refl1 [OF R1])
   731     apply (drule Quotient_refl1 [OF R2], drule Rep1)
   731     apply (drule Quotient_refl1 [OF R2], drule Rep1)
   732     apply (subgoal_tac "R1 r (Rep1 (Abs1 x))")
   732     apply (subgoal_tac "R1 r (Rep1 (Abs1 x))")
   733      apply (rule_tac b="Rep1 (Abs1 x)" in pred_compI, assumption)
   733      apply (rule_tac b="Rep1 (Abs1 x)" in relcomppI, assumption)
   734      apply (erule pred_compI)
   734      apply (erule relcomppI)
   735      apply (erule Quotient_symp [OF R1, THEN sympD])
   735      apply (erule Quotient_symp [OF R1, THEN sympD])
   736     apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2])
   736     apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2])
   737     apply (rule conjI, erule Quotient_refl1 [OF R1])
   737     apply (rule conjI, erule Quotient_refl1 [OF R1])
   738     apply (rule conjI, rule Quotient_rep_reflp [OF R1])
   738     apply (rule conjI, rule Quotient_rep_reflp [OF R1])
   739     apply (subst Quotient_abs_rep [OF R1])
   739     apply (subst Quotient_abs_rep [OF R1])
   742    apply (drule Abs1)
   742    apply (drule Abs1)
   743      apply (erule Quotient_refl2 [OF R1])
   743      apply (erule Quotient_refl2 [OF R1])
   744     apply (erule Quotient_refl1 [OF R1])
   744     apply (erule Quotient_refl1 [OF R1])
   745    apply (drule Quotient_refl2 [OF R2], drule Rep1)
   745    apply (drule Quotient_refl2 [OF R2], drule Rep1)
   746    apply (subgoal_tac "R1 s (Rep1 (Abs1 y))")
   746    apply (subgoal_tac "R1 s (Rep1 (Abs1 y))")
   747     apply (rule_tac b="Rep1 (Abs1 y)" in pred_compI, assumption)
   747     apply (rule_tac b="Rep1 (Abs1 y)" in relcomppI, assumption)
   748     apply (erule pred_compI)
   748     apply (erule relcomppI)
   749     apply (erule Quotient_symp [OF R1, THEN sympD])
   749     apply (erule Quotient_symp [OF R1, THEN sympD])
   750    apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2])
   750    apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2])
   751    apply (rule conjI, erule Quotient_refl2 [OF R1])
   751    apply (rule conjI, erule Quotient_refl2 [OF R1])
   752    apply (rule conjI, rule Quotient_rep_reflp [OF R1])
   752    apply (rule conjI, rule Quotient_rep_reflp [OF R1])
   753    apply (subst Quotient_abs_rep [OF R1])
   753    apply (subst Quotient_abs_rep [OF R1])
   759   apply (erule Abs1)
   759   apply (erule Abs1)
   760    apply (erule Quotient_refl2 [OF R1])
   760    apply (erule Quotient_refl2 [OF R1])
   761   apply (erule Quotient_refl1 [OF R1])
   761   apply (erule Quotient_refl1 [OF R1])
   762  apply (rename_tac a b c d)
   762  apply (rename_tac a b c d)
   763  apply simp
   763  apply simp
   764  apply (rule_tac b="Rep1 (Abs1 r)" in pred_compI)
   764  apply (rule_tac b="Rep1 (Abs1 r)" in relcomppI)
   765   apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2])
   765   apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2])
   766   apply (rule conjI, erule Quotient_refl1 [OF R1])
   766   apply (rule conjI, erule Quotient_refl1 [OF R1])
   767   apply (simp add: Quotient_abs_rep [OF R1] Quotient_rep_reflp [OF R1])
   767   apply (simp add: Quotient_abs_rep [OF R1] Quotient_rep_reflp [OF R1])
   768  apply (rule_tac b="Rep1 (Abs1 s)" in pred_compI [rotated])
   768  apply (rule_tac b="Rep1 (Abs1 s)" in relcomppI [rotated])
   769   apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2])
   769   apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2])
   770   apply (simp add: Quotient_abs_rep [OF R1] Quotient_rep_reflp [OF R1])
   770   apply (simp add: Quotient_abs_rep [OF R1] Quotient_rep_reflp [OF R1])
   771   apply (erule Quotient_refl2 [OF R1])
   771   apply (erule Quotient_refl2 [OF R1])
   772  apply (rule Rep1)
   772  apply (rule Rep1)
   773  apply (drule Abs1)
   773  apply (drule Abs1)