src/HOL/Library/Quotient_Sum.thy
changeset 47094 1a7ad2601cb5
parent 45802 b16f976db515
child 47308 9caab698dbe4
     1.1 --- a/src/HOL/Library/Quotient_Sum.thy	Fri Mar 23 14:18:43 2012 +0100
     1.2 +++ b/src/HOL/Library/Quotient_Sum.thy	Fri Mar 23 14:20:09 2012 +0100
     1.3 @@ -16,8 +16,6 @@
     1.4  | "sum_rel R1 R2 (Inr a2) (Inl b1) = False"
     1.5  | "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"
     1.6  
     1.7 -declare [[map sum = sum_rel]]
     1.8 -
     1.9  lemma sum_rel_unfold:
    1.10    "sum_rel R1 R2 x y = (case (x, y) of (Inl x, Inl y) \<Rightarrow> R1 x y
    1.11      | (Inr x, Inr y) \<Rightarrow> R2 x y
    1.12 @@ -67,6 +65,8 @@
    1.13    apply (simp add: sum_rel_unfold comp_def split: sum.split)
    1.14    done
    1.15  
    1.16 +declare [[map sum = (sum_rel, sum_quotient)]]
    1.17 +
    1.18  lemma sum_Inl_rsp [quot_respect]:
    1.19    assumes q1: "Quotient R1 Abs1 Rep1"
    1.20    assumes q2: "Quotient R2 Abs2 Rep2"