src/HOL/Library/Quotient_Product.thy
changeset 47308 9caab698dbe4
parent 47301 ca743eafa1dd
child 47455 26315a545e26
     1.1 --- a/src/HOL/Library/Quotient_Product.thy	Tue Apr 03 14:09:37 2012 +0200
     1.2 +++ b/src/HOL/Library/Quotient_Product.thy	Tue Apr 03 16:26:48 2012 +0200
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:      HOL/Library/Quotient_Product.thy
     1.5 +(*  Title:      HOL/Library/Quotient3_Product.thy
     1.6      Author:     Cezary Kaliszyk and Christian Urban
     1.7  *)
     1.8  
     1.9 @@ -32,56 +32,56 @@
    1.10    using assms by (auto intro!: equivpI reflpI sympI transpI elim!: equivpE elim: reflpE sympE transpE)
    1.11  
    1.12  lemma prod_quotient [quot_thm]:
    1.13 -  assumes "Quotient R1 Abs1 Rep1"
    1.14 -  assumes "Quotient R2 Abs2 Rep2"
    1.15 -  shows "Quotient (prod_rel R1 R2) (map_pair Abs1 Abs2) (map_pair Rep1 Rep2)"
    1.16 -  apply (rule QuotientI)
    1.17 +  assumes "Quotient3 R1 Abs1 Rep1"
    1.18 +  assumes "Quotient3 R2 Abs2 Rep2"
    1.19 +  shows "Quotient3 (prod_rel R1 R2) (map_pair Abs1 Abs2) (map_pair Rep1 Rep2)"
    1.20 +  apply (rule Quotient3I)
    1.21    apply (simp add: map_pair.compositionality comp_def map_pair.identity
    1.22 -     Quotient_abs_rep [OF assms(1)] Quotient_abs_rep [OF assms(2)])
    1.23 -  apply (simp add: split_paired_all Quotient_rel_rep [OF assms(1)] Quotient_rel_rep [OF assms(2)])
    1.24 -  using Quotient_rel [OF assms(1)] Quotient_rel [OF assms(2)]
    1.25 +     Quotient3_abs_rep [OF assms(1)] Quotient3_abs_rep [OF assms(2)])
    1.26 +  apply (simp add: split_paired_all Quotient3_rel_rep [OF assms(1)] Quotient3_rel_rep [OF assms(2)])
    1.27 +  using Quotient3_rel [OF assms(1)] Quotient3_rel [OF assms(2)]
    1.28    apply (auto simp add: split_paired_all)
    1.29    done
    1.30  
    1.31 -declare [[map prod = (prod_rel, prod_quotient)]]
    1.32 +declare [[mapQ3 prod = (prod_rel, prod_quotient)]]
    1.33  
    1.34  lemma Pair_rsp [quot_respect]:
    1.35 -  assumes q1: "Quotient R1 Abs1 Rep1"
    1.36 -  assumes q2: "Quotient R2 Abs2 Rep2"
    1.37 +  assumes q1: "Quotient3 R1 Abs1 Rep1"
    1.38 +  assumes q2: "Quotient3 R2 Abs2 Rep2"
    1.39    shows "(R1 ===> R2 ===> prod_rel R1 R2) Pair Pair"
    1.40    by (auto simp add: prod_rel_def)
    1.41  
    1.42  lemma Pair_prs [quot_preserve]:
    1.43 -  assumes q1: "Quotient R1 Abs1 Rep1"
    1.44 -  assumes q2: "Quotient R2 Abs2 Rep2"
    1.45 +  assumes q1: "Quotient3 R1 Abs1 Rep1"
    1.46 +  assumes q2: "Quotient3 R2 Abs2 Rep2"
    1.47    shows "(Rep1 ---> Rep2 ---> (map_pair Abs1 Abs2)) Pair = Pair"
    1.48    apply(simp add: fun_eq_iff)
    1.49 -  apply(simp add: Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
    1.50 +  apply(simp add: Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2])
    1.51    done
    1.52  
    1.53  lemma fst_rsp [quot_respect]:
    1.54 -  assumes "Quotient R1 Abs1 Rep1"
    1.55 -  assumes "Quotient R2 Abs2 Rep2"
    1.56 +  assumes "Quotient3 R1 Abs1 Rep1"
    1.57 +  assumes "Quotient3 R2 Abs2 Rep2"
    1.58    shows "(prod_rel R1 R2 ===> R1) fst fst"
    1.59    by auto
    1.60  
    1.61  lemma fst_prs [quot_preserve]:
    1.62 -  assumes q1: "Quotient R1 Abs1 Rep1"
    1.63 -  assumes q2: "Quotient R2 Abs2 Rep2"
    1.64 +  assumes q1: "Quotient3 R1 Abs1 Rep1"
    1.65 +  assumes q2: "Quotient3 R2 Abs2 Rep2"
    1.66    shows "(map_pair Rep1 Rep2 ---> Abs1) fst = fst"
    1.67 -  by (simp add: fun_eq_iff Quotient_abs_rep[OF q1])
    1.68 +  by (simp add: fun_eq_iff Quotient3_abs_rep[OF q1])
    1.69  
    1.70  lemma snd_rsp [quot_respect]:
    1.71 -  assumes "Quotient R1 Abs1 Rep1"
    1.72 -  assumes "Quotient R2 Abs2 Rep2"
    1.73 +  assumes "Quotient3 R1 Abs1 Rep1"
    1.74 +  assumes "Quotient3 R2 Abs2 Rep2"
    1.75    shows "(prod_rel R1 R2 ===> R2) snd snd"
    1.76    by auto
    1.77  
    1.78  lemma snd_prs [quot_preserve]:
    1.79 -  assumes q1: "Quotient R1 Abs1 Rep1"
    1.80 -  assumes q2: "Quotient R2 Abs2 Rep2"
    1.81 +  assumes q1: "Quotient3 R1 Abs1 Rep1"
    1.82 +  assumes q2: "Quotient3 R2 Abs2 Rep2"
    1.83    shows "(map_pair Rep1 Rep2 ---> Abs2) snd = snd"
    1.84 -  by (simp add: fun_eq_iff Quotient_abs_rep[OF q2])
    1.85 +  by (simp add: fun_eq_iff Quotient3_abs_rep[OF q2])
    1.86  
    1.87  lemma split_rsp [quot_respect]:
    1.88    shows "((R1 ===> R2 ===> (op =)) ===> (prod_rel R1 R2) ===> (op =)) split split"
    1.89 @@ -89,10 +89,10 @@
    1.90    by auto
    1.91  
    1.92  lemma split_prs [quot_preserve]:
    1.93 -  assumes q1: "Quotient R1 Abs1 Rep1"
    1.94 -  and     q2: "Quotient R2 Abs2 Rep2"
    1.95 +  assumes q1: "Quotient3 R1 Abs1 Rep1"
    1.96 +  and     q2: "Quotient3 R2 Abs2 Rep2"
    1.97    shows "(((Abs1 ---> Abs2 ---> id) ---> map_pair Rep1 Rep2 ---> id) split) = split"
    1.98 -  by (simp add: fun_eq_iff Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
    1.99 +  by (simp add: fun_eq_iff Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2])
   1.100  
   1.101  lemma [quot_respect]:
   1.102    shows "((R2 ===> R2 ===> op =) ===> (R1 ===> R1 ===> op =) ===>
   1.103 @@ -100,11 +100,11 @@
   1.104    by (auto simp add: fun_rel_def)
   1.105  
   1.106  lemma [quot_preserve]:
   1.107 -  assumes q1: "Quotient R1 abs1 rep1"
   1.108 -  and     q2: "Quotient R2 abs2 rep2"
   1.109 +  assumes q1: "Quotient3 R1 abs1 rep1"
   1.110 +  and     q2: "Quotient3 R2 abs2 rep2"
   1.111    shows "((abs1 ---> abs1 ---> id) ---> (abs2 ---> abs2 ---> id) --->
   1.112    map_pair rep1 rep2 ---> map_pair rep1 rep2 ---> id) prod_rel = prod_rel"
   1.113 -  by (simp add: fun_eq_iff Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
   1.114 +  by (simp add: fun_eq_iff Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2])
   1.115  
   1.116  lemma [quot_preserve]:
   1.117    shows"(prod_rel ((rep1 ---> rep1 ---> id) R1) ((rep2 ---> rep2 ---> id) R2)