# HG changeset patch
# User haftmann
# Date 1290096076 -3600
# Node ID 70776ecfe324fc76494965daa3585576415dea12
# Parent  efb0d78785386b0e0c89998609284eea8327e0d3
mapper for sum type

diff -r efb0d7878538 -r 70776ecfe324 src/HOL/Library/Quotient_Sum.thy
--- 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)]]
 
 
diff -r efb0d7878538 -r 70776ecfe324 src/HOL/Sum_Type.thy
--- 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 *}