src/HOL/Library/Quotient_Product.thy
changeset 40607 30d512bf47a7
parent 40541 7850b4cc1507
child 40820 fd9c98ead9a9
     1.1 --- a/src/HOL/Library/Quotient_Product.thy	Thu Nov 18 17:01:16 2010 +0100
     1.2 +++ b/src/HOL/Library/Quotient_Product.thy	Thu Nov 18 17:01:16 2010 +0100
     1.3 @@ -13,7 +13,7 @@
     1.4  where
     1.5    "prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
     1.6  
     1.7 -declare [[map prod = (prod_fun, prod_rel)]]
     1.8 +declare [[map prod = (map_pair, prod_rel)]]
     1.9  
    1.10  lemma prod_rel_apply [simp]:
    1.11    "prod_rel R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
    1.12 @@ -34,7 +34,7 @@
    1.13  lemma prod_quotient[quot_thm]:
    1.14    assumes q1: "Quotient R1 Abs1 Rep1"
    1.15    assumes q2: "Quotient R2 Abs2 Rep2"
    1.16 -  shows "Quotient (prod_rel R1 R2) (prod_fun Abs1 Abs2) (prod_fun Rep1 Rep2)"
    1.17 +  shows "Quotient (prod_rel R1 R2) (map_pair Abs1 Abs2) (map_pair Rep1 Rep2)"
    1.18    unfolding Quotient_def
    1.19    apply(simp add: split_paired_all)
    1.20    apply(simp add: Quotient_abs_rep[OF q1] Quotient_rel_rep[OF q1])
    1.21 @@ -53,7 +53,7 @@
    1.22  lemma Pair_prs[quot_preserve]:
    1.23    assumes q1: "Quotient R1 Abs1 Rep1"
    1.24    assumes q2: "Quotient R2 Abs2 Rep2"
    1.25 -  shows "(Rep1 ---> Rep2 ---> (prod_fun Abs1 Abs2)) Pair = Pair"
    1.26 +  shows "(Rep1 ---> Rep2 ---> (map_pair Abs1 Abs2)) Pair = Pair"
    1.27    apply(simp add: fun_eq_iff)
    1.28    apply(simp add: Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
    1.29    done
    1.30 @@ -67,7 +67,7 @@
    1.31  lemma fst_prs[quot_preserve]:
    1.32    assumes q1: "Quotient R1 Abs1 Rep1"
    1.33    assumes q2: "Quotient R2 Abs2 Rep2"
    1.34 -  shows "(prod_fun Rep1 Rep2 ---> Abs1) fst = fst"
    1.35 +  shows "(map_pair Rep1 Rep2 ---> Abs1) fst = fst"
    1.36    by (simp add: fun_eq_iff Quotient_abs_rep[OF q1])
    1.37  
    1.38  lemma snd_rsp[quot_respect]:
    1.39 @@ -79,7 +79,7 @@
    1.40  lemma snd_prs[quot_preserve]:
    1.41    assumes q1: "Quotient R1 Abs1 Rep1"
    1.42    assumes q2: "Quotient R2 Abs2 Rep2"
    1.43 -  shows "(prod_fun Rep1 Rep2 ---> Abs2) snd = snd"
    1.44 +  shows "(map_pair Rep1 Rep2 ---> Abs2) snd = snd"
    1.45    by (simp add: fun_eq_iff Quotient_abs_rep[OF q2])
    1.46  
    1.47  lemma split_rsp[quot_respect]:
    1.48 @@ -89,7 +89,7 @@
    1.49  lemma split_prs[quot_preserve]:
    1.50    assumes q1: "Quotient R1 Abs1 Rep1"
    1.51    and     q2: "Quotient R2 Abs2 Rep2"
    1.52 -  shows "(((Abs1 ---> Abs2 ---> id) ---> prod_fun Rep1 Rep2 ---> id) split) = split"
    1.53 +  shows "(((Abs1 ---> Abs2 ---> id) ---> map_pair Rep1 Rep2 ---> id) split) = split"
    1.54    by (simp add: fun_eq_iff Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
    1.55  
    1.56  lemma [quot_respect]:
    1.57 @@ -101,7 +101,7 @@
    1.58    assumes q1: "Quotient R1 abs1 rep1"
    1.59    and     q2: "Quotient R2 abs2 rep2"
    1.60    shows "((abs1 ---> abs1 ---> id) ---> (abs2 ---> abs2 ---> id) --->
    1.61 -  prod_fun rep1 rep2 ---> prod_fun rep1 rep2 ---> id) prod_rel = prod_rel"
    1.62 +  map_pair rep1 rep2 ---> map_pair rep1 rep2 ---> id) prod_rel = prod_rel"
    1.63    by (simp add: fun_eq_iff Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
    1.64  
    1.65  lemma [quot_preserve]:
    1.66 @@ -111,8 +111,8 @@
    1.67  
    1.68  declare Pair_eq[quot_preserve]
    1.69  
    1.70 -lemma prod_fun_id[id_simps]:
    1.71 -  shows "prod_fun id id = id"
    1.72 +lemma map_pair_id[id_simps]:
    1.73 +  shows "map_pair id id = id"
    1.74    by (simp add: fun_eq_iff)
    1.75  
    1.76  lemma prod_rel_eq[id_simps]: