828 fun |
828 fun |
829 prod_fv :: "('a \<Rightarrow> atom set) \<Rightarrow> ('b \<Rightarrow> atom set) \<Rightarrow> ('a \<times> 'b) \<Rightarrow> atom set" |
829 prod_fv :: "('a \<Rightarrow> atom set) \<Rightarrow> ('b \<Rightarrow> atom set) \<Rightarrow> ('a \<times> 'b) \<Rightarrow> atom set" |
830 where |
830 where |
831 "prod_fv fvx fvy (x, y) = (fvx x \<union> fvy y)" |
831 "prod_fv fvx fvy (x, y) = (fvx x \<union> fvy y)" |
832 |
832 |
|
833 definition |
|
834 prod_alpha :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool)" |
|
835 where |
|
836 "prod_alpha = prod_rel" |
|
837 |
|
838 |
833 lemma [quot_respect]: |
839 lemma [quot_respect]: |
834 "((R1 ===> op =) ===> (R2 ===> op =) ===> prod_rel R1 R2 ===> op =) prod_fv prod_fv" |
840 shows "((R1 ===> op =) ===> (R2 ===> op =) ===> prod_rel R1 R2 ===> op =) prod_fv prod_fv" |
835 by auto |
841 by auto |
836 |
842 |
837 lemma [quot_preserve]: |
843 lemma [quot_preserve]: |
838 assumes q1: "Quotient R1 abs1 rep1" |
844 assumes q1: "Quotient R1 abs1 rep1" |
839 and q2: "Quotient R2 abs2 rep2" |
845 and q2: "Quotient R2 abs2 rep2" |
840 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" |
841 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]) |
842 |
848 |
843 lemma [mono]: "A <= B \<Longrightarrow> C <= D ==> prod_rel A C <= prod_rel B D" |
849 lemma [mono]: |
|
850 shows "A <= B \<Longrightarrow> C <= D ==> prod_rel A C <= prod_rel B D" |
844 by auto |
851 by auto |
845 |
852 |
846 lemma [eqvt]: |
853 lemma [eqvt]: |
847 shows "p \<bullet> prod_rel A B x y = prod_rel (p \<bullet> A) (p \<bullet> B) (p \<bullet> x) (p \<bullet> y)" |
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 unfolding prod_alpha_def |
848 unfolding prod_rel.simps |
856 unfolding prod_rel.simps |
849 by (perm_simp) (rule refl) |
857 by (perm_simp) (rule refl) |
850 |
858 |
851 lemma [eqvt]: |
859 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)" |
860 shows "p \<bullet> prod_fv A B (x, y) = prod_fv (p \<bullet> A) (p \<bullet> B) (p \<bullet> x, p \<bullet> y)" |