equal
deleted
inserted
replaced
88 fix P |
88 fix P |
89 fix s :: "'a + 'b" |
89 fix s :: "'a + 'b" |
90 assume x: "\<And>x\<Colon>'a. P (Inl x)" and y: "\<And>y\<Colon>'b. P (Inr y)" |
90 assume x: "\<And>x\<Colon>'a. P (Inl x)" and y: "\<And>y\<Colon>'b. P (Inr y)" |
91 then show "P s" by (auto intro: sumE [of s]) |
91 then show "P s" by (auto intro: sumE [of s]) |
92 qed (auto dest: Inl_inject Inr_inject simp add: Inl_not_Inr) |
92 qed (auto dest: Inl_inject Inr_inject simp add: Inl_not_Inr) |
|
93 |
|
94 primrec sum_map :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd" where |
|
95 "sum_map f1 f2 (Inl a) = Inl (f1 a)" |
|
96 | "sum_map f1 f2 (Inr a) = Inr (f2 a)" |
|
97 |
|
98 type_mapper sum_map proof - |
|
99 fix f g h i s |
|
100 show "sum_map f g (sum_map h i s) = sum_map (\<lambda>x. f (h x)) (\<lambda>x. g (i x)) s" |
|
101 by (cases s) simp_all |
|
102 next |
|
103 fix s |
|
104 show "sum_map (\<lambda>x. x) (\<lambda>x. x) s = s" |
|
105 by (cases s) simp_all |
|
106 qed |
93 |
107 |
94 |
108 |
95 subsection {* Projections *} |
109 subsection {* Projections *} |
96 |
110 |
97 lemma sum_case_KK [simp]: "sum_case (\<lambda>x. a) (\<lambda>x. a) = (\<lambda>x. a)" |
111 lemma sum_case_KK [simp]: "sum_case (\<lambda>x. a) (\<lambda>x. a) = (\<lambda>x. a)" |