src/HOL/BNF_Examples/Derivation_Trees/Prelim.thy

 
 lemma fst_snd_convol_o[simp]: "<fst o s, snd o s> = s"
 apply(rule ext) by (simp add: convol_def)
 
 abbreviation sm_abbrev (infix "\<oplus>" 60)
-where "f \<oplus> g \<equiv> Sum_Type.sum_map f g"
+where "f \<oplus> g \<equiv> Sum_Type.map_sum f g"
 
-lemma sum_map_InlD: "(f \<oplus> g) z = Inl x \<Longrightarrow> \<exists>y. z = Inl y \<and> f y = x"
+lemma map_sum_InlD: "(f \<oplus> g) z = Inl x \<Longrightarrow> \<exists>y. z = Inl y \<and> f y = x"
 by (cases z) auto
 
-lemma sum_map_InrD: "(f \<oplus> g) z = Inr x \<Longrightarrow> \<exists>y. z = Inr y \<and> g y = x"
+lemma map_sum_InrD: "(f \<oplus> g) z = Inr x \<Longrightarrow> \<exists>y. z = Inr y \<and> g y = x"
 by (cases z) auto
 
 abbreviation case_sum_abbrev ("[[_,_]]" 800)
 where "[[f,g]] \<equiv> Sum_Type.case_sum f g"
 

 shows "Inl tr \<in> tns"
 using assms apply clarify by (case_tac x, auto)
 
 lemma Inl_oplus_iff[simp]: "Inl tr \<in> (id \<oplus> f) ` tns \<longleftrightarrow> Inl tr \<in> tns"
 using Inl_oplus_elim
-by (metis id_def image_iff sum_map.simps(1))
+by (metis id_def image_iff map_sum.simps(1))
 
 lemma Inl_m_oplus[simp]: "Inl -` (id \<oplus> f) ` tns = Inl -` tns"
 using Inl_oplus_iff unfolding vimage_def by auto
 
 lemma Inr_oplus_elim:

 
 lemma Inr_oplus_iff[simp]:
 "Inr tr \<in> (id \<oplus> f) ` tns \<longleftrightarrow> (\<exists> n. Inr n \<in> tns \<and> f n = tr)"
 apply (rule iffI)
  apply (metis Inr_oplus_elim)
-by (metis image_iff sum_map.simps(2))
+by (metis image_iff map_sum.simps(2))
 
 lemma Inr_m_oplus[simp]: "Inr -` (id \<oplus> f) ` tns = f ` (Inr -` tns)"
 using Inr_oplus_iff unfolding vimage_def by auto
 
 lemma Inl_Inr_image_cong: