equal
deleted
inserted
replaced
838 assumes q1: "Quotient R1 abs1 rep1" |
838 assumes q1: "Quotient R1 abs1 rep1" |
839 and q2: "Quotient R2 abs2 rep2" |
839 and q2: "Quotient R2 abs2 rep2" |
840 shows "((abs1 ---> id) ---> (abs2 ---> id) ---> prod_fun rep1 rep2 ---> id) prod_fv = prod_fv" |
840 shows "((abs1 ---> id) ---> (abs2 ---> id) ---> prod_fun rep1 rep2 ---> id) prod_fv = prod_fv" |
841 by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) |
841 by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) |
842 |
842 |
|
843 lemma [mono]: "A <= B \<Longrightarrow> C <= D ==> prod_rel A C <= prod_rel B D" |
|
844 by auto |
|
845 |
|
846 lemma [eqvt]: "(p \<bullet> prod_rel A B x y) = prod_rel (p \<bullet> A) (p \<bullet> B) (p \<bullet> x) (p \<bullet> y)" |
|
847 by (simp, perm_simp) (rule refl) |
|
848 |
|
849 lemma [eqvt]: "(p \<bullet> prod_fv A B (x, y)) = prod_fv (p \<bullet> A) (p \<bullet> B) (p \<bullet> x, p \<bullet> y)" |
|
850 by (simp, perm_simp) (rule refl) |
|
851 |
843 end |
852 end |
844 |
853 |