src/HOL/Library/Quotient_Product.thy
changeset 47982 7aa35601ff65
parent 47936 756f30eac792
child 51377 7da251a6c16e
     1.1 --- a/src/HOL/Library/Quotient_Product.thy	Thu May 24 13:56:21 2012 +0200
     1.2 +++ b/src/HOL/Library/Quotient_Product.thy	Thu May 24 14:20:23 2012 +0200
     1.3 @@ -27,12 +27,18 @@
     1.4    shows "prod_rel (op =) (op =) = (op =)"
     1.5    by (simp add: fun_eq_iff)
     1.6  
     1.7 -lemma prod_reflp [reflp_preserve]:
     1.8 +lemma prod_reflp [reflexivity_rule]:
     1.9    assumes "reflp R1"
    1.10    assumes "reflp R2"
    1.11    shows "reflp (prod_rel R1 R2)"
    1.12  using assms by (auto intro!: reflpI elim: reflpE)
    1.13  
    1.14 +lemma prod_left_total [reflexivity_rule]:
    1.15 +  assumes "left_total R1"
    1.16 +  assumes "left_total R2"
    1.17 +  shows "left_total (prod_rel R1 R2)"
    1.18 +using assms by (auto intro!: left_totalI elim!: left_totalE)
    1.19 +
    1.20  lemma prod_equivp [quot_equiv]:
    1.21    assumes "equivp R1"
    1.22    assumes "equivp R2"