src/HOL/Sum_Type.thy
changeset 41372 551eb49a6e91
parent 40968 a6fcd305f7dc
child 41505 6d19301074cf
     1.1 --- a/src/HOL/Sum_Type.thy	Tue Dec 21 16:14:46 2010 +0100
     1.2 +++ b/src/HOL/Sum_Type.thy	Tue Dec 21 17:52:23 2010 +0100
     1.3 @@ -95,14 +95,22 @@
     1.4    "sum_map f1 f2 (Inl a) = Inl (f1 a)"
     1.5  | "sum_map f1 f2 (Inr a) = Inr (f2 a)"
     1.6  
     1.7 -type_lifting sum_map proof -
     1.8 -  fix f g h i s
     1.9 -  show "sum_map f g (sum_map h i s) = sum_map (\<lambda>x. f (h x)) (\<lambda>x. g (i x)) s"
    1.10 -    by (cases s) simp_all
    1.11 +type_lifting sum_map: sum_map proof -
    1.12 +  fix f g h i
    1.13 +  show "sum_map f g \<circ> sum_map h i = sum_map (f \<circ> h) (g \<circ> i)"
    1.14 +  proof
    1.15 +    fix s
    1.16 +    show "(sum_map f g \<circ> sum_map h i) s = sum_map (f \<circ> h) (g \<circ> i) s"
    1.17 +      by (cases s) simp_all
    1.18 +  qed
    1.19  next
    1.20    fix s
    1.21 -  show "sum_map (\<lambda>x. x) (\<lambda>x. x) s = s"
    1.22 -    by (cases s) simp_all
    1.23 +  show "sum_map id id = id"
    1.24 +  proof
    1.25 +    fix s
    1.26 +    show "sum_map id id s = id s" 
    1.27 +      by (cases s) simp_all
    1.28 +  qed
    1.29  qed
    1.30  
    1.31