src/HOL/Library/Quotient_Sum.thy
changeset 40465 2989f9f3aa10
parent 39302 d7728f65b353
child 40542 9a173a22771c
     1.1 --- a/src/HOL/Library/Quotient_Sum.thy	Tue Nov 09 14:02:12 2010 +0100
     1.2 +++ b/src/HOL/Library/Quotient_Sum.thy	Tue Nov 09 14:02:13 2010 +0100
     1.3 @@ -9,15 +9,15 @@
     1.4  begin
     1.5  
     1.6  fun
     1.7 -  sum_rel
     1.8 +  sum_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'a + 'b \<Rightarrow> bool"
     1.9  where
    1.10    "sum_rel R1 R2 (Inl a1) (Inl b1) = R1 a1 b1"
    1.11  | "sum_rel R1 R2 (Inl a1) (Inr b2) = False"
    1.12  | "sum_rel R1 R2 (Inr a2) (Inl b1) = False"
    1.13  | "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"
    1.14  
    1.15 -fun
    1.16 -  sum_map
    1.17 +primrec
    1.18 +  sum_map :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd"
    1.19  where
    1.20    "sum_map f1 f2 (Inl a) = Inl (f1 a)"
    1.21  | "sum_map f1 f2 (Inr a) = Inr (f2 a)"
    1.22 @@ -62,13 +62,13 @@
    1.23    assumes q1: "Quotient R1 Abs1 Rep1"
    1.24    assumes q2: "Quotient R2 Abs2 Rep2"
    1.25    shows "(R1 ===> sum_rel R1 R2) Inl Inl"
    1.26 -  by simp
    1.27 +  by auto
    1.28  
    1.29  lemma sum_Inr_rsp[quot_respect]:
    1.30    assumes q1: "Quotient R1 Abs1 Rep1"
    1.31    assumes q2: "Quotient R2 Abs2 Rep2"
    1.32    shows "(R2 ===> sum_rel R1 R2) Inr Inr"
    1.33 -  by simp
    1.34 +  by auto
    1.35  
    1.36  lemma sum_Inl_prs[quot_preserve]:
    1.37    assumes q1: "Quotient R1 Abs1 Rep1"