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