src/HOL/Library/Quotient_Product.thy
changeset 47634 091bcd569441
parent 47624 16d433895d2e
child 47635 ebb79474262c
     1.1 --- a/src/HOL/Library/Quotient_Product.thy	Fri Apr 20 15:49:45 2012 +0200
     1.2 +++ b/src/HOL/Library/Quotient_Product.thy	Fri Apr 20 18:29:21 2012 +0200
     1.3 @@ -93,6 +93,15 @@
     1.4  
     1.5  declare [[map prod = (prod_rel, Quotient_prod)]]
     1.6  
     1.7 +definition prod_pred :: "('a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
     1.8 +where "prod_pred R1 R2 = (\<lambda>(a, b). R1 a \<and> R2 b)"
     1.9 +
    1.10 +lemma prod_invariant_commute [invariant_commute]: 
    1.11 +  "prod_rel (Lifting.invariant P1) (Lifting.invariant P2) = Lifting.invariant (prod_pred P1 P2)"
    1.12 +  apply (simp add: fun_eq_iff prod_rel_def prod_pred_def Lifting.invariant_def) 
    1.13 +  apply blast
    1.14 +done
    1.15 +
    1.16  subsection {* Rules for quotient package *}
    1.17  
    1.18  lemma prod_quotient [quot_thm]: