src/HOL/BNF_Def.thy

--- a/src/HOL/BNF_Def.thy	Wed Aug 06 10:20:50 2014 +0200
+++ b/src/HOL/BNF_Def.thy	Wed Aug 06 16:00:11 2014 +0200
@@ -159,6 +159,11 @@
 "case_sum f g \<circ> Inr = g"
 by auto
 
+lemma map_sum_o_inj:
+"map_sum f g o Inl = Inl o f"
+"map_sum f g o Inr = Inr o g"
+by auto
+
 lemma card_order_csum_cone_cexp_def:
   "card_order r \<Longrightarrow> ( |A1| +c cone) ^c r = |Func UNIV (Inl ` A1 \<union> {Inr ()})|"
   unfolding cexp_def cone_def Field_csum Field_card_of by (auto dest: Field_card_order)