--- a/src/HOL/Library/Quotient_Sum.thy Thu Nov 18 17:01:16 2010 +0100
+++ b/src/HOL/Library/Quotient_Sum.thy Thu Nov 18 17:01:16 2010 +0100
@@ -16,12 +16,6 @@
| "sum_rel R1 R2 (Inr a2) (Inl b1) = False"
| "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"
-primrec
- sum_map :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd"
-where
- "sum_map f1 f2 (Inl a) = Inl (f1 a)"
-| "sum_map f1 f2 (Inr a) = Inr (f2 a)"
-
declare [[map sum = (sum_map, sum_rel)]]
--- a/src/HOL/Sum_Type.thy Thu Nov 18 17:01:16 2010 +0100
+++ b/src/HOL/Sum_Type.thy Thu Nov 18 17:01:16 2010 +0100
@@ -91,6 +91,20 @@
then show "P s" by (auto intro: sumE [of s])
qed (auto dest: Inl_inject Inr_inject simp add: Inl_not_Inr)
+primrec sum_map :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd" where
+ "sum_map f1 f2 (Inl a) = Inl (f1 a)"
+| "sum_map f1 f2 (Inr a) = Inr (f2 a)"
+
+type_mapper sum_map proof -
+ fix f g h i s
+ show "sum_map f g (sum_map h i s) = sum_map (\<lambda>x. f (h x)) (\<lambda>x. g (i x)) s"
+ by (cases s) simp_all
+next
+ fix s
+ show "sum_map (\<lambda>x. x) (\<lambda>x. x) s = s"
+ by (cases s) simp_all
+qed
+
subsection {* Projections *}