src/HOL/Library/Quotient_Product.thy
changeset 55932 68c5104d2204
parent 55414 eab03e9cee8a
child 55944 7ab8f003fe41
     1.1 --- a/src/HOL/Library/Quotient_Product.thy	Thu Mar 06 13:36:15 2014 +0100
     1.2 +++ b/src/HOL/Library/Quotient_Product.thy	Thu Mar 06 13:36:48 2014 +0100
     1.3 @@ -10,8 +10,8 @@
     1.4  
     1.5  subsection {* Rules for the Quotient package *}
     1.6  
     1.7 -lemma map_pair_id [id_simps]:
     1.8 -  shows "map_pair id id = id"
     1.9 +lemma map_prod_id [id_simps]:
    1.10 +  shows "map_prod id id = id"
    1.11    by (simp add: fun_eq_iff)
    1.12  
    1.13  lemma prod_rel_eq [id_simps]:
    1.14 @@ -27,9 +27,9 @@
    1.15  lemma prod_quotient [quot_thm]:
    1.16    assumes "Quotient3 R1 Abs1 Rep1"
    1.17    assumes "Quotient3 R2 Abs2 Rep2"
    1.18 -  shows "Quotient3 (prod_rel R1 R2) (map_pair Abs1 Abs2) (map_pair Rep1 Rep2)"
    1.19 +  shows "Quotient3 (prod_rel R1 R2) (map_prod Abs1 Abs2) (map_prod Rep1 Rep2)"
    1.20    apply (rule Quotient3I)
    1.21 -  apply (simp add: map_pair.compositionality comp_def map_pair.identity
    1.22 +  apply (simp add: map_prod.compositionality comp_def map_prod.identity
    1.23       Quotient3_abs_rep [OF assms(1)] Quotient3_abs_rep [OF assms(2)])
    1.24    apply (simp add: split_paired_all Quotient3_rel_rep [OF assms(1)] Quotient3_rel_rep [OF assms(2)])
    1.25    using Quotient3_rel [OF assms(1)] Quotient3_rel [OF assms(2)]
    1.26 @@ -47,7 +47,7 @@
    1.27  lemma Pair_prs [quot_preserve]:
    1.28    assumes q1: "Quotient3 R1 Abs1 Rep1"
    1.29    assumes q2: "Quotient3 R2 Abs2 Rep2"
    1.30 -  shows "(Rep1 ---> Rep2 ---> (map_pair Abs1 Abs2)) Pair = Pair"
    1.31 +  shows "(Rep1 ---> Rep2 ---> (map_prod Abs1 Abs2)) Pair = Pair"
    1.32    apply(simp add: fun_eq_iff)
    1.33    apply(simp add: Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2])
    1.34    done
    1.35 @@ -61,7 +61,7 @@
    1.36  lemma fst_prs [quot_preserve]:
    1.37    assumes q1: "Quotient3 R1 Abs1 Rep1"
    1.38    assumes q2: "Quotient3 R2 Abs2 Rep2"
    1.39 -  shows "(map_pair Rep1 Rep2 ---> Abs1) fst = fst"
    1.40 +  shows "(map_prod Rep1 Rep2 ---> Abs1) fst = fst"
    1.41    by (simp add: fun_eq_iff Quotient3_abs_rep[OF q1])
    1.42  
    1.43  lemma snd_rsp [quot_respect]:
    1.44 @@ -73,7 +73,7 @@
    1.45  lemma snd_prs [quot_preserve]:
    1.46    assumes q1: "Quotient3 R1 Abs1 Rep1"
    1.47    assumes q2: "Quotient3 R2 Abs2 Rep2"
    1.48 -  shows "(map_pair Rep1 Rep2 ---> Abs2) snd = snd"
    1.49 +  shows "(map_prod Rep1 Rep2 ---> Abs2) snd = snd"
    1.50    by (simp add: fun_eq_iff Quotient3_abs_rep[OF q2])
    1.51  
    1.52  lemma split_rsp [quot_respect]:
    1.53 @@ -83,7 +83,7 @@
    1.54  lemma split_prs [quot_preserve]:
    1.55    assumes q1: "Quotient3 R1 Abs1 Rep1"
    1.56    and     q2: "Quotient3 R2 Abs2 Rep2"
    1.57 -  shows "(((Abs1 ---> Abs2 ---> id) ---> map_pair Rep1 Rep2 ---> id) split) = split"
    1.58 +  shows "(((Abs1 ---> Abs2 ---> id) ---> map_prod Rep1 Rep2 ---> id) split) = split"
    1.59    by (simp add: fun_eq_iff Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2])
    1.60  
    1.61  lemma [quot_respect]:
    1.62 @@ -95,7 +95,7 @@
    1.63    assumes q1: "Quotient3 R1 abs1 rep1"
    1.64    and     q2: "Quotient3 R2 abs2 rep2"
    1.65    shows "((abs1 ---> abs1 ---> id) ---> (abs2 ---> abs2 ---> id) --->
    1.66 -  map_pair rep1 rep2 ---> map_pair rep1 rep2 ---> id) prod_rel = prod_rel"
    1.67 +  map_prod rep1 rep2 ---> map_prod rep1 rep2 ---> id) prod_rel = prod_rel"
    1.68    by (simp add: fun_eq_iff Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2])
    1.69  
    1.70  lemma [quot_preserve]: