src/HOL/Library/Quotient_Product.thy
changeset 51377 7da251a6c16e
parent 47982 7aa35601ff65
child 51956 a4d81cdebf8b
     1.1 --- a/src/HOL/Library/Quotient_Product.thy	Fri Mar 08 13:21:45 2013 +0100
     1.2 +++ b/src/HOL/Library/Quotient_Product.thy	Fri Mar 08 13:21:52 2013 +0100
     1.3 @@ -27,6 +27,16 @@
     1.4    shows "prod_rel (op =) (op =) = (op =)"
     1.5    by (simp add: fun_eq_iff)
     1.6  
     1.7 +lemma prod_rel_mono[relator_mono]:
     1.8 +  assumes "A \<le> C"
     1.9 +  assumes "B \<le> D"
    1.10 +  shows "(prod_rel A B) \<le> (prod_rel C D)"
    1.11 +using assms by (auto simp: prod_rel_def)
    1.12 +
    1.13 +lemma prod_rel_OO[relator_distr]:
    1.14 +  "(prod_rel A B) OO (prod_rel C D) = prod_rel (A OO C) (B OO D)"
    1.15 +by (rule ext)+ (auto simp: prod_rel_def OO_def)
    1.16 +
    1.17  lemma prod_reflp [reflexivity_rule]:
    1.18    assumes "reflp R1"
    1.19    assumes "reflp R2"