equal
deleted
inserted
replaced
845 and q2: "Quotient R2 abs2 rep2" |
845 and q2: "Quotient R2 abs2 rep2" |
846 shows "((abs1 ---> id) ---> (abs2 ---> id) ---> prod_fun rep1 rep2 ---> id) prod_fv = prod_fv" |
846 shows "((abs1 ---> id) ---> (abs2 ---> id) ---> prod_fun rep1 rep2 ---> id) prod_fv = prod_fv" |
847 by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) |
847 by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]) |
848 |
848 |
849 lemma [mono]: |
849 lemma [mono]: |
850 shows "A <= B \<Longrightarrow> C <= D ==> prod_rel A C <= prod_rel B D" |
850 shows "A <= B \<Longrightarrow> C <= D ==> prod_alpha A C <= prod_alpha B D" |
|
851 unfolding prod_alpha_def |
851 by auto |
852 by auto |
852 |
853 |
853 lemma [eqvt]: |
854 lemma [eqvt]: |
854 shows "p \<bullet> prod_alpha A B x y = prod_alpha (p \<bullet> A) (p \<bullet> B) (p \<bullet> x) (p \<bullet> y)" |
855 shows "p \<bullet> prod_alpha A B x y = prod_alpha (p \<bullet> A) (p \<bullet> B) (p \<bullet> x) (p \<bullet> y)" |
855 unfolding prod_alpha_def |
856 unfolding prod_alpha_def |
859 lemma [eqvt]: |
860 lemma [eqvt]: |
860 shows "p \<bullet> prod_fv A B (x, y) = prod_fv (p \<bullet> A) (p \<bullet> B) (p \<bullet> x, p \<bullet> y)" |
861 shows "p \<bullet> prod_fv A B (x, y) = prod_fv (p \<bullet> A) (p \<bullet> B) (p \<bullet> x, p \<bullet> y)" |
861 unfolding prod_fv.simps |
862 unfolding prod_fv.simps |
862 by (perm_simp) (rule refl) |
863 by (perm_simp) (rule refl) |
863 |
864 |
|
865 |
864 end |
866 end |
865 |
867 |