src/HOL/Library/Quotient_Product.thy
changeset 55944 7ab8f003fe41
parent 55932 68c5104d2204
child 58881 b9556a055632
     1.1 --- a/src/HOL/Library/Quotient_Product.thy	Thu Mar 06 15:25:21 2014 +0100
     1.2 +++ b/src/HOL/Library/Quotient_Product.thy	Thu Mar 06 15:29:18 2014 +0100
     1.3 @@ -14,20 +14,20 @@
     1.4    shows "map_prod id id = id"
     1.5    by (simp add: fun_eq_iff)
     1.6  
     1.7 -lemma prod_rel_eq [id_simps]:
     1.8 -  shows "prod_rel (op =) (op =) = (op =)"
     1.9 +lemma rel_prod_eq [id_simps]:
    1.10 +  shows "rel_prod (op =) (op =) = (op =)"
    1.11    by (simp add: fun_eq_iff)
    1.12  
    1.13  lemma prod_equivp [quot_equiv]:
    1.14    assumes "equivp R1"
    1.15    assumes "equivp R2"
    1.16 -  shows "equivp (prod_rel R1 R2)"
    1.17 +  shows "equivp (rel_prod R1 R2)"
    1.18    using assms by (auto intro!: equivpI reflpI sympI transpI elim!: equivpE elim: reflpE sympE transpE)
    1.19  
    1.20  lemma prod_quotient [quot_thm]:
    1.21    assumes "Quotient3 R1 Abs1 Rep1"
    1.22    assumes "Quotient3 R2 Abs2 Rep2"
    1.23 -  shows "Quotient3 (prod_rel R1 R2) (map_prod Abs1 Abs2) (map_prod Rep1 Rep2)"
    1.24 +  shows "Quotient3 (rel_prod R1 R2) (map_prod Abs1 Abs2) (map_prod Rep1 Rep2)"
    1.25    apply (rule Quotient3I)
    1.26    apply (simp add: map_prod.compositionality comp_def map_prod.identity
    1.27       Quotient3_abs_rep [OF assms(1)] Quotient3_abs_rep [OF assms(2)])
    1.28 @@ -36,12 +36,12 @@
    1.29    apply (auto simp add: split_paired_all)
    1.30    done
    1.31  
    1.32 -declare [[mapQ3 prod = (prod_rel, prod_quotient)]]
    1.33 +declare [[mapQ3 prod = (rel_prod, prod_quotient)]]
    1.34  
    1.35  lemma Pair_rsp [quot_respect]:
    1.36    assumes q1: "Quotient3 R1 Abs1 Rep1"
    1.37    assumes q2: "Quotient3 R2 Abs2 Rep2"
    1.38 -  shows "(R1 ===> R2 ===> prod_rel R1 R2) Pair Pair"
    1.39 +  shows "(R1 ===> R2 ===> rel_prod R1 R2) Pair Pair"
    1.40    by (rule Pair_transfer)
    1.41  
    1.42  lemma Pair_prs [quot_preserve]:
    1.43 @@ -55,7 +55,7 @@
    1.44  lemma fst_rsp [quot_respect]:
    1.45    assumes "Quotient3 R1 Abs1 Rep1"
    1.46    assumes "Quotient3 R2 Abs2 Rep2"
    1.47 -  shows "(prod_rel R1 R2 ===> R1) fst fst"
    1.48 +  shows "(rel_prod R1 R2 ===> R1) fst fst"
    1.49    by auto
    1.50  
    1.51  lemma fst_prs [quot_preserve]:
    1.52 @@ -67,7 +67,7 @@
    1.53  lemma snd_rsp [quot_respect]:
    1.54    assumes "Quotient3 R1 Abs1 Rep1"
    1.55    assumes "Quotient3 R2 Abs2 Rep2"
    1.56 -  shows "(prod_rel R1 R2 ===> R2) snd snd"
    1.57 +  shows "(rel_prod R1 R2 ===> R2) snd snd"
    1.58    by auto
    1.59  
    1.60  lemma snd_prs [quot_preserve]:
    1.61 @@ -77,7 +77,7 @@
    1.62    by (simp add: fun_eq_iff Quotient3_abs_rep[OF q2])
    1.63  
    1.64  lemma split_rsp [quot_respect]:
    1.65 -  shows "((R1 ===> R2 ===> (op =)) ===> (prod_rel R1 R2) ===> (op =)) split split"
    1.66 +  shows "((R1 ===> R2 ===> (op =)) ===> (rel_prod R1 R2) ===> (op =)) split split"
    1.67    by (rule case_prod_transfer)
    1.68  
    1.69  lemma split_prs [quot_preserve]:
    1.70 @@ -88,18 +88,18 @@
    1.71  
    1.72  lemma [quot_respect]:
    1.73    shows "((R2 ===> R2 ===> op =) ===> (R1 ===> R1 ===> op =) ===>
    1.74 -  prod_rel R2 R1 ===> prod_rel R2 R1 ===> op =) prod_rel prod_rel"
    1.75 -  by (rule prod_rel_transfer)
    1.76 +  rel_prod R2 R1 ===> rel_prod R2 R1 ===> op =) rel_prod rel_prod"
    1.77 +  by (rule rel_prod_transfer)
    1.78  
    1.79  lemma [quot_preserve]:
    1.80    assumes q1: "Quotient3 R1 abs1 rep1"
    1.81    and     q2: "Quotient3 R2 abs2 rep2"
    1.82    shows "((abs1 ---> abs1 ---> id) ---> (abs2 ---> abs2 ---> id) --->
    1.83 -  map_prod rep1 rep2 ---> map_prod rep1 rep2 ---> id) prod_rel = prod_rel"
    1.84 +  map_prod rep1 rep2 ---> map_prod rep1 rep2 ---> id) rel_prod = rel_prod"
    1.85    by (simp add: fun_eq_iff Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2])
    1.86  
    1.87  lemma [quot_preserve]:
    1.88 -  shows"(prod_rel ((rep1 ---> rep1 ---> id) R1) ((rep2 ---> rep2 ---> id) R2)
    1.89 +  shows"(rel_prod ((rep1 ---> rep1 ---> id) R1) ((rep2 ---> rep2 ---> id) R2)
    1.90    (l1, l2) (r1, r2)) = (R1 (rep1 l1) (rep1 r1) \<and> R2 (rep2 l2) (rep2 r2))"
    1.91    by simp
    1.92