equal
deleted
inserted
replaced
983 unfolding fun_rel_def |
983 unfolding fun_rel_def |
984 unfolding prod_rel_def |
984 unfolding prod_rel_def |
985 by auto |
985 by auto |
986 |
986 |
987 lemma [quot_preserve]: |
987 lemma [quot_preserve]: |
988 assumes q1: "Quotient R1 abs1 rep1" |
988 assumes q1: "Quotient3 R1 abs1 rep1" |
989 and q2: "Quotient R2 abs2 rep2" |
989 and q2: "Quotient3 R2 abs2 rep2" |
990 shows "((abs1 ---> id) ---> (abs2 ---> id) ---> map_pair rep1 rep2 ---> id) prod_fv = prod_fv" |
990 shows "((abs1 ---> id) ---> (abs2 ---> id) ---> map_pair rep1 rep2 ---> id) prod_fv = prod_fv" |
991 by (simp add: fun_eq_iff Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) |
991 by (simp add: fun_eq_iff Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2]) |
992 |
992 |
993 lemma [mono]: |
993 lemma [mono]: |
994 shows "A <= B \<Longrightarrow> C <= D ==> prod_alpha A C <= prod_alpha B D" |
994 shows "A <= B \<Longrightarrow> C <= D ==> prod_alpha A C <= prod_alpha B D" |
995 unfolding prod_alpha_def |
995 unfolding prod_alpha_def |
996 by auto |
996 by auto |