828 fun

   829   prod_fv :: "('a \<Rightarrow> atom set) \<Rightarrow> ('b \<Rightarrow> atom set) \<Rightarrow> ('a \<times> 'b) \<Rightarrow> atom set"

   830 where

   831   "prod_fv fvx fvy (x, y) = (fvx x \<union> fvy y)"

   832 

   833 lemma [quot_respect]:

   834   "((R1 ===> op =) ===> (R2 ===> op =) ===> prod_rel R1 R2 ===> op =) prod_fv prod_fv"

   835   by auto

   836 

   837 lemma [quot_preserve]:

   838   assumes q1: "Quotient R1 abs1 rep1"

   839   and     q2: "Quotient R2 abs2 rep2"

   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])