equal
deleted
inserted
replaced
551 by auto |
551 by auto |
552 |
552 |
553 lemma [quot_preserve]: |
553 lemma [quot_preserve]: |
554 assumes q1: "Quotient R1 abs1 rep1" |
554 assumes q1: "Quotient R1 abs1 rep1" |
555 and q2: "Quotient R2 abs2 rep2" |
555 and q2: "Quotient R2 abs2 rep2" |
556 shows "((abs1 ---> id) ---> (abs2 ---> id) ---> prod_fun rep1 rep2 ---> id) prod_fv = prod_fv" |
556 shows "((abs1 ---> id) ---> (abs2 ---> id) ---> map_pair rep1 rep2 ---> id) prod_fv = prod_fv" |
557 by (simp add: fun_eq_iff Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) |
557 by (simp add: fun_eq_iff Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) |
558 |
558 |
559 lemma [mono]: |
559 lemma [mono]: |
560 shows "A <= B \<Longrightarrow> C <= D ==> prod_alpha A C <= prod_alpha B D" |
560 shows "A <= B \<Longrightarrow> C <= D ==> prod_alpha A C <= prod_alpha B D" |
561 unfolding prod_alpha_def |
561 unfolding prod_alpha_def |