544 where

   544 where

   545  "prod_alpha = prod_rel"

   545  "prod_alpha = prod_rel"

   546 

   546 

   547 lemma [quot_respect]:

   547 lemma [quot_respect]:

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

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

   549   by auto

   551   by auto

   550 

   552 

   551 lemma [quot_preserve]:

   553 lemma [quot_preserve]:

   552   assumes q1: "Quotient R1 abs1 rep1"

   554   assumes q1: "Quotient R1 abs1 rep1"

   553   and     q2: "Quotient R2 abs2 rep2"

   555   and     q2: "Quotient R2 abs2 rep2"

   560   by auto

   562   by auto

   561 

   563 

   562 lemma [eqvt]: 

   564 lemma [eqvt]: 

   563   shows "p \<bullet> prod_alpha A B x y = prod_alpha (p \<bullet> A) (p \<bullet> B) (p \<bullet> x) (p \<bullet> y)"

   565   shows "p \<bullet> prod_alpha A B x y = prod_alpha (p \<bullet> A) (p \<bullet> B) (p \<bullet> x) (p \<bullet> y)"

   564   unfolding prod_alpha_def

   566   unfolding prod_alpha_def

   566   by (perm_simp) (rule refl)

   568   by (perm_simp) (rule refl)

   567 

   569 

   568 lemma [eqvt]: 

   570 lemma [eqvt]: 

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

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

   570   unfolding prod_fv.simps

   572   unfolding prod_fv.simps