531 definition 

   531 definition 

   532   prod_alpha :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool)"

   532   prod_alpha :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool)"

   533 where

   533 where

   534  "prod_alpha = prod_rel"

   534  "prod_alpha = prod_rel"

   535 

   535 

   537 lemma [quot_respect]:

   536 lemma [quot_respect]:

   538   shows "((R1 ===> op =) ===> (R2 ===> op =) ===> prod_rel R1 R2 ===> op =) prod_fv prod_fv"

   537   shows "((R1 ===> op =) ===> (R2 ===> op =) ===> prod_rel R1 R2 ===> op =) prod_fv prod_fv"

   539   by auto

   538   by auto

   540 

   539 

   541 lemma [quot_preserve]:

   540 lemma [quot_preserve]:

   557 

   556 

   558 lemma [eqvt]: 

   557 lemma [eqvt]: 

   559   shows "p \<bullet> prod_fv A B (x, y) = prod_fv (p \<bullet> A) (p \<bullet> B) (p \<bullet> x, p \<bullet> y)"

   558   shows "p \<bullet> prod_fv A B (x, y) = prod_fv (p \<bullet> A) (p \<bullet> B) (p \<bullet> x, p \<bullet> y)"

   560   unfolding prod_fv.simps

   559   unfolding prod_fv.simps

   561   by (perm_simp) (rule refl)

   560   by (perm_simp) (rule refl)

   570 

   561 

   571 

   562 

   572 

   563 

   573 

   564 

   574 section {* BELOW is stuff that may or may not be needed *}

   565 section {* BELOW is stuff that may or may not be needed *}