equal
deleted
inserted
replaced
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" |
843 lemma [mono]: "A <= B \<Longrightarrow> C <= D ==> prod_rel A C <= prod_rel B D" |
844 by auto |
844 by auto |
845 |
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)" |
846 lemma [eqvt]: |
847 by (simp, perm_simp) (rule refl) |
847 shows "p \<bullet> prod_rel A B x y = prod_rel (p \<bullet> A) (p \<bullet> B) (p \<bullet> x) (p \<bullet> y)" |
848 |
848 unfolding prod_rel.simps |
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)" |
849 by (perm_simp) (rule refl) |
850 by (simp, perm_simp) (rule refl) |
850 |
|
851 lemma [eqvt]: |
|
852 shows "p \<bullet> prod_fv A B (x, y) = prod_fv (p \<bullet> A) (p \<bullet> B) (p \<bullet> x, p \<bullet> y)" |
|
853 unfolding prod_fv.simps |
|
854 by (perm_simp) (rule refl) |
851 |
855 |
852 end |
856 end |
853 |
857 |