src/HOL/Library/Quotient_Product.thy
changeset 61424 c3658c18b7bc
parent 60500 903bb1495239
child 62954 c5d0fdc260fa
     1.1 --- a/src/HOL/Library/Quotient_Product.thy	Tue Oct 13 09:21:14 2015 +0200
     1.2 +++ b/src/HOL/Library/Quotient_Product.thy	Tue Oct 13 09:21:15 2015 +0200
     1.3 @@ -76,14 +76,14 @@
     1.4    shows "(map_prod Rep1 Rep2 ---> Abs2) snd = snd"
     1.5    by (simp add: fun_eq_iff Quotient3_abs_rep[OF q2])
     1.6  
     1.7 -lemma split_rsp [quot_respect]:
     1.8 -  shows "((R1 ===> R2 ===> (op =)) ===> (rel_prod R1 R2) ===> (op =)) split split"
     1.9 +lemma case_prod_rsp [quot_respect]:
    1.10 +  shows "((R1 ===> R2 ===> (op =)) ===> (rel_prod R1 R2) ===> (op =)) case_prod case_prod"
    1.11    by (rule case_prod_transfer)
    1.12  
    1.13  lemma split_prs [quot_preserve]:
    1.14    assumes q1: "Quotient3 R1 Abs1 Rep1"
    1.15    and     q2: "Quotient3 R2 Abs2 Rep2"
    1.16 -  shows "(((Abs1 ---> Abs2 ---> id) ---> map_prod Rep1 Rep2 ---> id) split) = split"
    1.17 +  shows "(((Abs1 ---> Abs2 ---> id) ---> map_prod Rep1 Rep2 ---> id) case_prod) = case_prod"
    1.18    by (simp add: fun_eq_iff Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2])
    1.19  
    1.20  lemma [quot_respect]:
    1.21 @@ -103,6 +103,6 @@
    1.22    (l1, l2) (r1, r2)) = (R1 (rep1 l1) (rep1 r1) \<and> R2 (rep2 l2) (rep2 r2))"
    1.23    by simp
    1.24  
    1.25 -declare Pair_eq[quot_preserve]
    1.26 +declare prod.inject[quot_preserve]
    1.27  
    1.28  end