src/HOL/Library/Quotient_Sum.thy
changeset 47308 9caab698dbe4
parent 47094 1a7ad2601cb5
child 47455 26315a545e26
     1.1 --- a/src/HOL/Library/Quotient_Sum.thy	Tue Apr 03 14:09:37 2012 +0200
     1.2 +++ b/src/HOL/Library/Quotient_Sum.thy	Tue Apr 03 16:26:48 2012 +0200
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:      HOL/Library/Quotient_Sum.thy
     1.5 +(*  Title:      HOL/Library/Quotient3_Sum.thy
     1.6      Author:     Cezary Kaliszyk and Christian Urban
     1.7  *)
     1.8  
     1.9 @@ -55,44 +55,44 @@
    1.10    by (blast intro: equivpI sum_reflp sum_symp sum_transp elim: equivpE)
    1.11    
    1.12  lemma sum_quotient [quot_thm]:
    1.13 -  assumes q1: "Quotient R1 Abs1 Rep1"
    1.14 -  assumes q2: "Quotient R2 Abs2 Rep2"
    1.15 -  shows "Quotient (sum_rel R1 R2) (sum_map Abs1 Abs2) (sum_map Rep1 Rep2)"
    1.16 -  apply (rule QuotientI)
    1.17 +  assumes q1: "Quotient3 R1 Abs1 Rep1"
    1.18 +  assumes q2: "Quotient3 R2 Abs2 Rep2"
    1.19 +  shows "Quotient3 (sum_rel R1 R2) (sum_map Abs1 Abs2) (sum_map Rep1 Rep2)"
    1.20 +  apply (rule Quotient3I)
    1.21    apply (simp_all add: sum_map.compositionality comp_def sum_map.identity sum_rel_eq sum_rel_map1 sum_rel_map2
    1.22 -    Quotient_abs_rep [OF q1] Quotient_rel_rep [OF q1] Quotient_abs_rep [OF q2] Quotient_rel_rep [OF q2])
    1.23 -  using Quotient_rel [OF q1] Quotient_rel [OF q2]
    1.24 +    Quotient3_abs_rep [OF q1] Quotient3_rel_rep [OF q1] Quotient3_abs_rep [OF q2] Quotient3_rel_rep [OF q2])
    1.25 +  using Quotient3_rel [OF q1] Quotient3_rel [OF q2]
    1.26    apply (simp add: sum_rel_unfold comp_def split: sum.split)
    1.27    done
    1.28  
    1.29 -declare [[map sum = (sum_rel, sum_quotient)]]
    1.30 +declare [[mapQ3 sum = (sum_rel, sum_quotient)]]
    1.31  
    1.32  lemma sum_Inl_rsp [quot_respect]:
    1.33 -  assumes q1: "Quotient R1 Abs1 Rep1"
    1.34 -  assumes q2: "Quotient R2 Abs2 Rep2"
    1.35 +  assumes q1: "Quotient3 R1 Abs1 Rep1"
    1.36 +  assumes q2: "Quotient3 R2 Abs2 Rep2"
    1.37    shows "(R1 ===> sum_rel R1 R2) Inl Inl"
    1.38    by auto
    1.39  
    1.40  lemma sum_Inr_rsp [quot_respect]:
    1.41 -  assumes q1: "Quotient R1 Abs1 Rep1"
    1.42 -  assumes q2: "Quotient R2 Abs2 Rep2"
    1.43 +  assumes q1: "Quotient3 R1 Abs1 Rep1"
    1.44 +  assumes q2: "Quotient3 R2 Abs2 Rep2"
    1.45    shows "(R2 ===> sum_rel R1 R2) Inr Inr"
    1.46    by auto
    1.47  
    1.48  lemma sum_Inl_prs [quot_preserve]:
    1.49 -  assumes q1: "Quotient R1 Abs1 Rep1"
    1.50 -  assumes q2: "Quotient R2 Abs2 Rep2"
    1.51 +  assumes q1: "Quotient3 R1 Abs1 Rep1"
    1.52 +  assumes q2: "Quotient3 R2 Abs2 Rep2"
    1.53    shows "(Rep1 ---> sum_map Abs1 Abs2) Inl = Inl"
    1.54    apply(simp add: fun_eq_iff)
    1.55 -  apply(simp add: Quotient_abs_rep[OF q1])
    1.56 +  apply(simp add: Quotient3_abs_rep[OF q1])
    1.57    done
    1.58  
    1.59  lemma sum_Inr_prs [quot_preserve]:
    1.60 -  assumes q1: "Quotient R1 Abs1 Rep1"
    1.61 -  assumes q2: "Quotient R2 Abs2 Rep2"
    1.62 +  assumes q1: "Quotient3 R1 Abs1 Rep1"
    1.63 +  assumes q2: "Quotient3 R2 Abs2 Rep2"
    1.64    shows "(Rep2 ---> sum_map Abs1 Abs2) Inr = Inr"
    1.65    apply(simp add: fun_eq_iff)
    1.66 -  apply(simp add: Quotient_abs_rep[OF q2])
    1.67 +  apply(simp add: Quotient3_abs_rep[OF q2])
    1.68    done
    1.69  
    1.70  end