renamed 'map_sum' to 'sum_map'
authorblanchet
Thu Mar 06 13:36:15 2014 +0100 (2014-03-06)
changeset 5593162156e694f3d
parent 55930 25a90cebbbe5
child 55932 68c5104d2204
renamed 'map_sum' to 'sum_map'
NEWS
src/HOL/BNF_Examples/Derivation_Trees/DTree.thy
src/HOL/BNF_Examples/Derivation_Trees/Gram_Lang.thy
src/HOL/BNF_Examples/Derivation_Trees/Prelim.thy
src/HOL/BNF_FP_Base.thy
src/HOL/Basic_BNFs.thy
src/HOL/Cardinals/Ordinal_Arithmetic.thy
src/HOL/HOLCF/Library/Option_Cpo.thy
src/HOL/HOLCF/Library/Sum_Cpo.thy
src/HOL/Library/Quotient_Sum.thy
src/HOL/Lifting_Sum.thy
src/HOL/Sum_Type.thy
src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
src/HOL/Tools/BNF/bnf_fp_n2m.ML
src/HOL/Tools/BNF/bnf_fp_util.ML
     1.1 --- a/NEWS	Thu Mar 06 12:17:26 2014 +0100
     1.2 +++ b/NEWS	Thu Mar 06 13:36:15 2014 +0100
     1.3 @@ -190,6 +190,9 @@
     1.4      the.simps ~> option.sel
     1.5    INCOMPATIBILITY.
     1.6  
     1.7 +* The following map function has been renamed:
     1.8 +    map_sum ~> sum_map
     1.9 +
    1.10  * New theory:
    1.11      Cardinals/Ordinal_Arithmetic.thy
    1.12  
     2.1 --- a/src/HOL/BNF_Examples/Derivation_Trees/DTree.thy	Thu Mar 06 12:17:26 2014 +0100
     2.2 +++ b/src/HOL/BNF_Examples/Derivation_Trees/DTree.thy	Thu Mar 06 13:36:15 2014 +0100
     2.3 @@ -20,7 +20,7 @@
     2.4  
     2.5  definition "Node n as \<equiv> NNode n (the_inv fset as)"
     2.6  definition "cont \<equiv> fset o ccont"
     2.7 -definition "unfold rt ct \<equiv> corec_dtree rt (the_inv fset o image (sum_map id Inr) o ct)"
     2.8 +definition "unfold rt ct \<equiv> corec_dtree rt (the_inv fset o image (map_sum id Inr) o ct)"
     2.9  definition "corec rt ct \<equiv> corec_dtree rt (the_inv fset o ct)"
    2.10  
    2.11  lemma finite_cont[simp]: "finite (cont tr)"
    2.12 @@ -75,10 +75,10 @@
    2.13  lemma unfold:
    2.14  "root (unfold rt ct b) = rt b"
    2.15  "finite (ct b) \<Longrightarrow> cont (unfold rt ct b) = image (id \<oplus> unfold rt ct) (ct b)"
    2.16 -using dtree.sel_corec[of rt "the_inv fset o image (sum_map id Inr) o ct" b] unfolding unfold_def
    2.17 +using dtree.sel_corec[of rt "the_inv fset o image (map_sum id Inr) o ct" b] unfolding unfold_def
    2.18  apply blast
    2.19  unfolding cont_def comp_def
    2.20 -by (simp add: case_sum_o_inj sum_map.compositionality image_image)
    2.21 +by (simp add: case_sum_o_inj map_sum.compositionality image_image)
    2.22  
    2.23  lemma corec:
    2.24  "root (corec rt ct b) = rt b"
     3.1 --- a/src/HOL/BNF_Examples/Derivation_Trees/Gram_Lang.thy	Thu Mar 06 12:17:26 2014 +0100
     3.2 +++ b/src/HOL/BNF_Examples/Derivation_Trees/Gram_Lang.thy	Thu Mar 06 13:36:15 2014 +0100
     3.3 @@ -334,13 +334,13 @@
     3.4    thus "t \<in> Inl -` cont tr" by(cases ttr, auto)
     3.5  next
     3.6    fix t assume "Inl t \<in> cont tr" thus "t \<in> Inl -` prodOf tr"
     3.7 -  by (metis (lifting) id_def image_iff sum_map.simps(1) vimageI2)
     3.8 +  by (metis (lifting) id_def image_iff map_sum.simps(1) vimageI2)
     3.9  qed
    3.10  
    3.11  lemma root_prodOf:
    3.12  assumes "Inr tr' \<in> cont tr"
    3.13  shows "Inr (root tr') \<in> prodOf tr"
    3.14 -by (metis (lifting) assms image_iff sum_map.simps(2))
    3.15 +by (metis (lifting) assms image_iff map_sum.simps(2))
    3.16  
    3.17  
    3.18  subsection{* Well-Formed Derivation Trees *}
    3.19 @@ -480,8 +480,8 @@
    3.20  proof-
    3.21    {fix tr assume "\<exists> n. tr = deftr n" hence "wf tr"
    3.22     apply(induct rule: wf_raw_coind) apply safe
    3.23 -   unfolding deftr_simps image_compose[symmetric] sum_map.comp id_comp
    3.24 -   root_o_deftr sum_map.id image_id id_apply apply(rule S_P)
    3.25 +   unfolding deftr_simps image_compose[symmetric] map_sum.comp id_comp
    3.26 +   root_o_deftr map_sum.id image_id id_apply apply(rule S_P)
    3.27     unfolding inj_on_def by auto
    3.28    }
    3.29    thus ?thesis by auto
    3.30 @@ -565,7 +565,7 @@
    3.31         show "(root (hsubst tr), prodOf (hsubst tr)) \<in> P"
    3.32         unfolding tr1 apply(cases "root tr = root tr0")
    3.33         using  wf_P[OF dtr] wf_P[OF tr0]
    3.34 -       by (auto simp add: image_compose[symmetric] sum_map.comp)
    3.35 +       by (auto simp add: image_compose[symmetric] map_sum.comp)
    3.36         show "inj_on root (Inr -` cont (hsubst tr))"
    3.37         apply(cases "root tr = root tr0") using wf_inj_on[OF dtr] wf_inj_on[OF tr0]
    3.38         unfolding inj_on_def by (auto, blast)
    3.39 @@ -958,7 +958,7 @@
    3.40  
    3.41  lemma cont_H[simp]:
    3.42  "cont (H n) = (id \<oplus> (H o root)) ` cont (pick n)"
    3.43 -apply(subst id_comp[symmetric, of id]) unfolding sum_map.comp[symmetric]
    3.44 +apply(subst id_comp[symmetric, of id]) unfolding map_sum.comp[symmetric]
    3.45  unfolding image_compose unfolding H_c_def[symmetric]
    3.46  using unfold(2)[of H_c n H_r, OF finite_H_c]
    3.47  unfolding H_def ..
    3.48 @@ -1001,9 +1001,9 @@
    3.49  assumes n: "inItr UNIV tr0 n" and t_tr: "t_tr \<in> cont (pick n)"
    3.50  shows "(id \<oplus> (root \<circ> H \<circ> root)) t_tr = (id \<oplus> root) t_tr"
    3.51  using assms apply(cases t_tr)
    3.52 -  apply (metis (lifting) sum_map.simps(1))
    3.53 +  apply (metis (lifting) map_sum.simps(1))
    3.54    using pick H_def H_r_def unfold(1)
    3.55 -      inItr.Base comp_apply subtr_StepL subtr_inItr sum_map.simps(2)
    3.56 +      inItr.Base comp_apply subtr_StepL subtr_inItr map_sum.simps(2)
    3.57    by (metis UNIV_I)
    3.58  
    3.59  lemma H_P:
    3.60 @@ -1011,7 +1011,7 @@
    3.61  shows "(n, (id \<oplus> root) ` cont (H n)) \<in> P" (is "?L \<in> P")
    3.62  proof-
    3.63    have "?L = (n, (id \<oplus> root) ` cont (pick n))"
    3.64 -  unfolding cont_H image_compose[symmetric] sum_map.comp id_comp comp_assoc[symmetric]
    3.65 +  unfolding cont_H image_compose[symmetric] map_sum.comp id_comp comp_assoc[symmetric]
    3.66    unfolding Pair_eq apply(rule conjI[OF refl]) apply(rule image_cong[OF refl])
    3.67    by (rule root_H_root[OF n])
    3.68    moreover have "... \<in> P" by (metis (lifting) wf_pick root_pick wf_P n tr0)
     4.1 --- a/src/HOL/BNF_Examples/Derivation_Trees/Prelim.thy	Thu Mar 06 12:17:26 2014 +0100
     4.2 +++ b/src/HOL/BNF_Examples/Derivation_Trees/Prelim.thy	Thu Mar 06 13:36:15 2014 +0100
     4.3 @@ -19,12 +19,12 @@
     4.4  apply(rule ext) by (simp add: convol_def)
     4.5  
     4.6  abbreviation sm_abbrev (infix "\<oplus>" 60)
     4.7 -where "f \<oplus> g \<equiv> Sum_Type.sum_map f g"
     4.8 +where "f \<oplus> g \<equiv> Sum_Type.map_sum f g"
     4.9  
    4.10 -lemma sum_map_InlD: "(f \<oplus> g) z = Inl x \<Longrightarrow> \<exists>y. z = Inl y \<and> f y = x"
    4.11 +lemma map_sum_InlD: "(f \<oplus> g) z = Inl x \<Longrightarrow> \<exists>y. z = Inl y \<and> f y = x"
    4.12  by (cases z) auto
    4.13  
    4.14 -lemma sum_map_InrD: "(f \<oplus> g) z = Inr x \<Longrightarrow> \<exists>y. z = Inr y \<and> g y = x"
    4.15 +lemma map_sum_InrD: "(f \<oplus> g) z = Inr x \<Longrightarrow> \<exists>y. z = Inr y \<and> g y = x"
    4.16  by (cases z) auto
    4.17  
    4.18  abbreviation case_sum_abbrev ("[[_,_]]" 800)
    4.19 @@ -37,7 +37,7 @@
    4.20  
    4.21  lemma Inl_oplus_iff[simp]: "Inl tr \<in> (id \<oplus> f) ` tns \<longleftrightarrow> Inl tr \<in> tns"
    4.22  using Inl_oplus_elim
    4.23 -by (metis id_def image_iff sum_map.simps(1))
    4.24 +by (metis id_def image_iff map_sum.simps(1))
    4.25  
    4.26  lemma Inl_m_oplus[simp]: "Inl -` (id \<oplus> f) ` tns = Inl -` tns"
    4.27  using Inl_oplus_iff unfolding vimage_def by auto
    4.28 @@ -51,7 +51,7 @@
    4.29  "Inr tr \<in> (id \<oplus> f) ` tns \<longleftrightarrow> (\<exists> n. Inr n \<in> tns \<and> f n = tr)"
    4.30  apply (rule iffI)
    4.31   apply (metis Inr_oplus_elim)
    4.32 -by (metis image_iff sum_map.simps(2))
    4.33 +by (metis image_iff map_sum.simps(2))
    4.34  
    4.35  lemma Inr_m_oplus[simp]: "Inr -` (id \<oplus> f) ` tns = f ` (Inr -` tns)"
    4.36  using Inr_oplus_iff unfolding vimage_def by auto
     5.1 --- a/src/HOL/BNF_FP_Base.thy	Thu Mar 06 12:17:26 2014 +0100
     5.2 +++ b/src/HOL/BNF_FP_Base.thy	Thu Mar 06 13:36:15 2014 +0100
     5.3 @@ -125,11 +125,11 @@
     5.4  lemma o_case_sum: "h o case_sum f g = case_sum (h o f) (h o g)"
     5.5    unfolding comp_def by (auto split: sum.splits)
     5.6  
     5.7 -lemma case_sum_o_sum_map: "case_sum f g o sum_map h1 h2 = case_sum (f o h1) (g o h2)"
     5.8 +lemma case_sum_o_map_sum: "case_sum f g o map_sum h1 h2 = case_sum (f o h1) (g o h2)"
     5.9    unfolding comp_def by (auto split: sum.splits)
    5.10  
    5.11 -lemma case_sum_o_sum_map_id: "(case_sum id g o sum_map f id) x = case_sum (f o id) g x"
    5.12 -  unfolding case_sum_o_sum_map id_comp comp_id ..
    5.13 +lemma case_sum_o_map_sum_id: "(case_sum id g o map_sum f id) x = case_sum (f o id) g x"
    5.14 +  unfolding case_sum_o_map_sum id_comp comp_id ..
    5.15  
    5.16  lemma fun_rel_def_butlast:
    5.17    "fun_rel R (fun_rel S T) f g = (\<forall>x y. R x y \<longrightarrow> (fun_rel S T) (f x) (g y))"
     6.1 --- a/src/HOL/Basic_BNFs.thy	Thu Mar 06 12:17:26 2014 +0100
     6.2 +++ b/src/HOL/Basic_BNFs.thy	Thu Mar 06 13:36:15 2014 +0100
     6.3 @@ -53,22 +53,22 @@
     6.4    unfolding sum_rel_def by simp_all
     6.5  
     6.6  bnf "'a + 'b"
     6.7 -  map: sum_map
     6.8 +  map: map_sum
     6.9    sets: setl setr
    6.10    bd: natLeq
    6.11    wits: Inl Inr
    6.12    rel: sum_rel
    6.13  proof -
    6.14 -  show "sum_map id id = id" by (rule sum_map.id)
    6.15 +  show "map_sum id id = id" by (rule map_sum.id)
    6.16  next
    6.17    fix f1 :: "'o \<Rightarrow> 's" and f2 :: "'p \<Rightarrow> 't" and g1 :: "'s \<Rightarrow> 'q" and g2 :: "'t \<Rightarrow> 'r"
    6.18 -  show "sum_map (g1 o f1) (g2 o f2) = sum_map g1 g2 o sum_map f1 f2"
    6.19 -    by (rule sum_map.comp[symmetric])
    6.20 +  show "map_sum (g1 o f1) (g2 o f2) = map_sum g1 g2 o map_sum f1 f2"
    6.21 +    by (rule map_sum.comp[symmetric])
    6.22  next
    6.23    fix x and f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r" and g1 g2
    6.24    assume a1: "\<And>z. z \<in> setl x \<Longrightarrow> f1 z = g1 z" and
    6.25           a2: "\<And>z. z \<in> setr x \<Longrightarrow> f2 z = g2 z"
    6.26 -  thus "sum_map f1 f2 x = sum_map g1 g2 x"
    6.27 +  thus "map_sum f1 f2 x = map_sum g1 g2 x"
    6.28    proof (cases x)
    6.29      case Inl thus ?thesis using a1 by (clarsimp simp: setl_def)
    6.30    next
    6.31 @@ -76,11 +76,11 @@
    6.32    qed
    6.33  next
    6.34    fix f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r"
    6.35 -  show "setl o sum_map f1 f2 = image f1 o setl"
    6.36 +  show "setl o map_sum f1 f2 = image f1 o setl"
    6.37      by (rule ext, unfold o_apply) (simp add: setl_def split: sum.split)
    6.38  next
    6.39    fix f1 :: "'o \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r"
    6.40 -  show "setr o sum_map f1 f2 = image f2 o setr"
    6.41 +  show "setr o map_sum f1 f2 = image f2 o setr"
    6.42      by (rule ext, unfold o_apply) (simp add: setr_def split: sum.split)
    6.43  next
    6.44    show "card_order natLeq" by (rule natLeq_card_order)
    6.45 @@ -105,8 +105,8 @@
    6.46  next
    6.47    fix R S
    6.48    show "sum_rel R S =
    6.49 -        (Grp {x. setl x \<subseteq> Collect (split R) \<and> setr x \<subseteq> Collect (split S)} (sum_map fst fst))\<inverse>\<inverse> OO
    6.50 -        Grp {x. setl x \<subseteq> Collect (split R) \<and> setr x \<subseteq> Collect (split S)} (sum_map snd snd)"
    6.51 +        (Grp {x. setl x \<subseteq> Collect (split R) \<and> setr x \<subseteq> Collect (split S)} (map_sum fst fst))\<inverse>\<inverse> OO
    6.52 +        Grp {x. setl x \<subseteq> Collect (split R) \<and> setr x \<subseteq> Collect (split S)} (map_sum snd snd)"
    6.53    unfolding setl_def setr_def sum_rel_def Grp_def relcompp.simps conversep.simps fun_eq_iff
    6.54    by (fastforce split: sum.splits)
    6.55  qed (auto simp: sum_set_defs)
     7.1 --- a/src/HOL/Cardinals/Ordinal_Arithmetic.thy	Thu Mar 06 12:17:26 2014 +0100
     7.2 +++ b/src/HOL/Cardinals/Ordinal_Arithmetic.thy	Thu Mar 06 13:36:15 2014 +0100
     7.3 @@ -953,7 +953,7 @@
     7.4  proof -
     7.5    from assms(1) obtain f where r: "Well_order r" and s: "Well_order s" and f: "iso r s f"
     7.6      unfolding ordIso_def by blast
     7.7 -  let ?f = "sum_map f id"
     7.8 +  let ?f = "map_sum f id"
     7.9    from f have "inj_on ?f (Field ?L)"
    7.10      unfolding Field_osum iso_def bij_betw_def inj_on_def by fastforce
    7.11    with f have "bij_betw ?f (Field ?L) (Field ?R)"
    7.12 @@ -971,7 +971,7 @@
    7.13  proof -
    7.14    from assms(1) obtain f where r: "Well_order r" and s: "Well_order s" and f: "iso r s f"
    7.15      unfolding ordIso_def by blast
    7.16 -  let ?f = "sum_map id f"
    7.17 +  let ?f = "map_sum id f"
    7.18    from f have "inj_on ?f (Field ?L)"
    7.19      unfolding Field_osum iso_def bij_betw_def inj_on_def by fastforce
    7.20    with f have "bij_betw ?f (Field ?L) (Field ?R)"
    7.21 @@ -1129,7 +1129,7 @@
    7.22    hence *: "inj_on f (Field s)" "compat s t f" "ofilter t (f ` Field s)" "f ` Field s \<subset> Field t"
    7.23      using embed_iff_compat_inj_on_ofilter[OF s t, of f] embedS_iff[OF s, of t f]
    7.24      unfolding embedS_def by auto
    7.25 -  let ?f = "sum_map id f"
    7.26 +  let ?f = "map_sum id f"
    7.27    from *(1) have "inj_on ?f (Field ?L)" unfolding Field_osum inj_on_def by fastforce
    7.28    moreover
    7.29    from *(2,4) have "compat ?L ?R ?f" unfolding compat_def osum_def map_pair_def by fastforce
    7.30 @@ -1153,7 +1153,7 @@
    7.31  proof -
    7.32    from assms obtain f where f: "\<forall>a\<in>Field r. f a \<in> Field s \<and> f ` underS r a \<subseteq> underS s (f a)"
    7.33      unfolding ordLeq_def2 by blast
    7.34 -  let ?f = "sum_map f id"
    7.35 +  let ?f = "map_sum f id"
    7.36    from f have "\<forall>a\<in>Field (r +o t).
    7.37       ?f a \<in> Field (s +o t) \<and> ?f ` underS (r +o t) a \<subseteq> underS (s +o t) (?f a)"
    7.38       unfolding Field_osum underS_def by (fastforce simp: osum_def)
     8.1 --- a/src/HOL/HOLCF/Library/Option_Cpo.thy	Thu Mar 06 12:17:26 2014 +0100
     8.2 +++ b/src/HOL/HOLCF/Library/Option_Cpo.thy	Thu Mar 06 13:36:15 2014 +0100
     8.3 @@ -275,7 +275,7 @@
     8.4  done
     8.5  
     8.6  lemma encode_option_option_map:
     8.7 -  "encode_option\<cdot>(map_option (\<lambda>x. f\<cdot>x) (decode_option\<cdot>x)) = sum_map' ID f\<cdot>x"
     8.8 +  "encode_option\<cdot>(map_option (\<lambda>x. f\<cdot>x) (decode_option\<cdot>x)) = map_sum' ID f\<cdot>x"
     8.9  by (induct x, simp_all add: decode_option_def encode_option_def)
    8.10  
    8.11  lemma isodefl_option [domain_isodefl]:
     9.1 --- a/src/HOL/HOLCF/Library/Sum_Cpo.thy	Thu Mar 06 12:17:26 2014 +0100
     9.2 +++ b/src/HOL/HOLCF/Library/Sum_Cpo.thy	Thu Mar 06 13:36:15 2014 +0100
     9.3 @@ -177,15 +177,15 @@
     9.4  
     9.5  text {* Continuity of map function. *}
     9.6  
     9.7 -lemma sum_map_eq: "sum_map f g = case_sum (\<lambda>a. Inl (f a)) (\<lambda>b. Inr (g b))"
     9.8 +lemma map_sum_eq: "map_sum f g = case_sum (\<lambda>a. Inl (f a)) (\<lambda>b. Inr (g b))"
     9.9  by (rule ext, case_tac x, simp_all)
    9.10  
    9.11 -lemma cont2cont_sum_map [simp, cont2cont]:
    9.12 +lemma cont2cont_map_sum [simp, cont2cont]:
    9.13    assumes f: "cont (\<lambda>(x, y). f x y)"
    9.14    assumes g: "cont (\<lambda>(x, y). g x y)"
    9.15    assumes h: "cont (\<lambda>x. h x)"
    9.16 -  shows "cont (\<lambda>x. sum_map (\<lambda>y. f x y) (\<lambda>y. g x y) (h x))"
    9.17 -using assms by (simp add: sum_map_eq prod_cont_iff)
    9.18 +  shows "cont (\<lambda>x. map_sum (\<lambda>y. f x y) (\<lambda>y. g x y) (h x))"
    9.19 +using assms by (simp add: map_sum_eq prod_cont_iff)
    9.20  
    9.21  subsection {* Compactness and chain-finiteness *}
    9.22  
    9.23 @@ -334,21 +334,21 @@
    9.24      sum_liftdefl\<cdot>LIFTDEFL('a)\<cdot>LIFTDEFL('b)"
    9.25  by (rule liftdefl_sum_def)
    9.26  
    9.27 -abbreviation sum_map'
    9.28 -  where "sum_map' f g \<equiv> Abs_cfun (sum_map (Rep_cfun f) (Rep_cfun g))"
    9.29 +abbreviation map_sum'
    9.30 +  where "map_sum' f g \<equiv> Abs_cfun (map_sum (Rep_cfun f) (Rep_cfun g))"
    9.31  
    9.32 -lemma sum_map_ID [domain_map_ID]: "sum_map' ID ID = ID"
    9.33 -by (simp add: ID_def cfun_eq_iff sum_map.identity id_def)
    9.34 +lemma map_sum_ID [domain_map_ID]: "map_sum' ID ID = ID"
    9.35 +by (simp add: ID_def cfun_eq_iff map_sum.identity id_def)
    9.36  
    9.37 -lemma deflation_sum_map [domain_deflation]:
    9.38 -  "\<lbrakk>deflation d1; deflation d2\<rbrakk> \<Longrightarrow> deflation (sum_map' d1 d2)"
    9.39 +lemma deflation_map_sum [domain_deflation]:
    9.40 +  "\<lbrakk>deflation d1; deflation d2\<rbrakk> \<Longrightarrow> deflation (map_sum' d1 d2)"
    9.41  apply default
    9.42  apply (induct_tac x, simp_all add: deflation.idem)
    9.43  apply (induct_tac x, simp_all add: deflation.below)
    9.44  done
    9.45  
    9.46 -lemma encode_sum_u_sum_map:
    9.47 -  "encode_sum_u\<cdot>(u_map\<cdot>(sum_map' f g)\<cdot>(decode_sum_u\<cdot>x))
    9.48 +lemma encode_sum_u_map_sum:
    9.49 +  "encode_sum_u\<cdot>(u_map\<cdot>(map_sum' f g)\<cdot>(decode_sum_u\<cdot>x))
    9.50      = ssum_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>g)\<cdot>x"
    9.51  apply (induct x, simp add: decode_sum_u_def encode_sum_u_def)
    9.52  apply (case_tac x, simp, simp add: decode_sum_u_def encode_sum_u_def)
    9.53 @@ -358,10 +358,10 @@
    9.54  lemma isodefl_sum [domain_isodefl]:
    9.55    fixes d :: "'a::predomain \<rightarrow> 'a"
    9.56    assumes "isodefl' d1 t1" and "isodefl' d2 t2"
    9.57 -  shows "isodefl' (sum_map' d1 d2) (sum_liftdefl\<cdot>t1\<cdot>t2)"
    9.58 +  shows "isodefl' (map_sum' d1 d2) (sum_liftdefl\<cdot>t1\<cdot>t2)"
    9.59  using assms unfolding isodefl'_def liftemb_sum_def liftprj_sum_def
    9.60  apply (simp add: sum_liftdefl_def cast_udefl cast_ssum_defl cast_u_liftdefl)
    9.61 -apply (simp add: cfcomp1 encode_sum_u_sum_map)
    9.62 +apply (simp add: cfcomp1 encode_sum_u_map_sum)
    9.63  apply (simp add: ssum_map_map u_emb_bottom)
    9.64  done
    9.65  
    10.1 --- a/src/HOL/Library/Quotient_Sum.thy	Thu Mar 06 12:17:26 2014 +0100
    10.2 +++ b/src/HOL/Library/Quotient_Sum.thy	Thu Mar 06 13:36:15 2014 +0100
    10.3 @@ -11,16 +11,16 @@
    10.4  subsection {* Rules for the Quotient package *}
    10.5  
    10.6  lemma sum_rel_map1:
    10.7 -  "sum_rel R1 R2 (sum_map f1 f2 x) y \<longleftrightarrow> sum_rel (\<lambda>x. R1 (f1 x)) (\<lambda>x. R2 (f2 x)) x y"
    10.8 +  "sum_rel R1 R2 (map_sum f1 f2 x) y \<longleftrightarrow> sum_rel (\<lambda>x. R1 (f1 x)) (\<lambda>x. R2 (f2 x)) x y"
    10.9    by (simp add: sum_rel_def split: sum.split)
   10.10  
   10.11  lemma sum_rel_map2:
   10.12 -  "sum_rel R1 R2 x (sum_map f1 f2 y) \<longleftrightarrow> sum_rel (\<lambda>x y. R1 x (f1 y)) (\<lambda>x y. R2 x (f2 y)) x y"
   10.13 +  "sum_rel R1 R2 x (map_sum f1 f2 y) \<longleftrightarrow> sum_rel (\<lambda>x y. R1 x (f1 y)) (\<lambda>x y. R2 x (f2 y)) x y"
   10.14    by (simp add: sum_rel_def split: sum.split)
   10.15  
   10.16 -lemma sum_map_id [id_simps]:
   10.17 -  "sum_map id id = id"
   10.18 -  by (simp add: id_def sum_map.identity fun_eq_iff)
   10.19 +lemma map_sum_id [id_simps]:
   10.20 +  "map_sum id id = id"
   10.21 +  by (simp add: id_def map_sum.identity fun_eq_iff)
   10.22  
   10.23  lemma sum_rel_eq [id_simps]:
   10.24    "sum_rel (op =) (op =) = (op =)"
   10.25 @@ -45,9 +45,9 @@
   10.26  lemma sum_quotient [quot_thm]:
   10.27    assumes q1: "Quotient3 R1 Abs1 Rep1"
   10.28    assumes q2: "Quotient3 R2 Abs2 Rep2"
   10.29 -  shows "Quotient3 (sum_rel R1 R2) (sum_map Abs1 Abs2) (sum_map Rep1 Rep2)"
   10.30 +  shows "Quotient3 (sum_rel R1 R2) (map_sum Abs1 Abs2) (map_sum Rep1 Rep2)"
   10.31    apply (rule Quotient3I)
   10.32 -  apply (simp_all add: sum_map.compositionality comp_def sum_map.identity sum_rel_eq sum_rel_map1 sum_rel_map2
   10.33 +  apply (simp_all add: map_sum.compositionality comp_def map_sum.identity sum_rel_eq sum_rel_map1 sum_rel_map2
   10.34      Quotient3_abs_rep [OF q1] Quotient3_rel_rep [OF q1] Quotient3_abs_rep [OF q2] Quotient3_rel_rep [OF q2])
   10.35    using Quotient3_rel [OF q1] Quotient3_rel [OF q2]
   10.36    apply (simp add: sum_rel_def comp_def split: sum.split)
   10.37 @@ -70,7 +70,7 @@
   10.38  lemma sum_Inl_prs [quot_preserve]:
   10.39    assumes q1: "Quotient3 R1 Abs1 Rep1"
   10.40    assumes q2: "Quotient3 R2 Abs2 Rep2"
   10.41 -  shows "(Rep1 ---> sum_map Abs1 Abs2) Inl = Inl"
   10.42 +  shows "(Rep1 ---> map_sum Abs1 Abs2) Inl = Inl"
   10.43    apply(simp add: fun_eq_iff)
   10.44    apply(simp add: Quotient3_abs_rep[OF q1])
   10.45    done
   10.46 @@ -78,7 +78,7 @@
   10.47  lemma sum_Inr_prs [quot_preserve]:
   10.48    assumes q1: "Quotient3 R1 Abs1 Rep1"
   10.49    assumes q2: "Quotient3 R2 Abs2 Rep2"
   10.50 -  shows "(Rep2 ---> sum_map Abs1 Abs2) Inr = Inr"
   10.51 +  shows "(Rep2 ---> map_sum Abs1 Abs2) Inr = Inr"
   10.52    apply(simp add: fun_eq_iff)
   10.53    apply(simp add: Quotient3_abs_rep[OF q2])
   10.54    done
    11.1 --- a/src/HOL/Lifting_Sum.thy	Thu Mar 06 12:17:26 2014 +0100
    11.2 +++ b/src/HOL/Lifting_Sum.thy	Thu Mar 06 13:36:15 2014 +0100
    11.3 @@ -59,8 +59,7 @@
    11.4  lemma Quotient_sum[quot_map]:
    11.5    assumes "Quotient R1 Abs1 Rep1 T1"
    11.6    assumes "Quotient R2 Abs2 Rep2 T2"
    11.7 -  shows "Quotient (sum_rel R1 R2) (sum_map Abs1 Abs2)
    11.8 -    (sum_map Rep1 Rep2) (sum_rel T1 T2)"
    11.9 +  shows "Quotient (sum_rel R1 R2) (map_sum Abs1 Abs2) (map_sum Rep1 Rep2) (sum_rel T1 T2)"
   11.10    using assms unfolding Quotient_alt_def
   11.11    by (simp add: split_sum_all)
   11.12  
    12.1 --- a/src/HOL/Sum_Type.thy	Thu Mar 06 12:17:26 2014 +0100
    12.2 +++ b/src/HOL/Sum_Type.thy	Thu Mar 06 13:36:15 2014 +0100
    12.3 @@ -119,24 +119,24 @@
    12.4  
    12.5  setup {* Sign.parent_path *}
    12.6  
    12.7 -primrec sum_map :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd" where
    12.8 -  "sum_map f1 f2 (Inl a) = Inl (f1 a)"
    12.9 -| "sum_map f1 f2 (Inr a) = Inr (f2 a)"
   12.10 +primrec map_sum :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd" where
   12.11 +  "map_sum f1 f2 (Inl a) = Inl (f1 a)"
   12.12 +| "map_sum f1 f2 (Inr a) = Inr (f2 a)"
   12.13  
   12.14 -functor sum_map: sum_map proof -
   12.15 +functor map_sum: map_sum proof -
   12.16    fix f g h i
   12.17 -  show "sum_map f g \<circ> sum_map h i = sum_map (f \<circ> h) (g \<circ> i)"
   12.18 +  show "map_sum f g \<circ> map_sum h i = map_sum (f \<circ> h) (g \<circ> i)"
   12.19    proof
   12.20      fix s
   12.21 -    show "(sum_map f g \<circ> sum_map h i) s = sum_map (f \<circ> h) (g \<circ> i) s"
   12.22 +    show "(map_sum f g \<circ> map_sum h i) s = map_sum (f \<circ> h) (g \<circ> i) s"
   12.23        by (cases s) simp_all
   12.24    qed
   12.25  next
   12.26    fix s
   12.27 -  show "sum_map id id = id"
   12.28 +  show "map_sum id id = id"
   12.29    proof
   12.30      fix s
   12.31 -    show "sum_map id id s = id s" 
   12.32 +    show "map_sum id id s = id s" 
   12.33        by (cases s) simp_all
   12.34    qed
   12.35  qed
    13.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Thu Mar 06 12:17:26 2014 +0100
    13.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Thu Mar 06 13:36:15 2014 +0100
    13.3 @@ -37,11 +37,11 @@
    13.4  val basic_simp_thms = @{thms simp_thms(7,8,12,14,22,24)};
    13.5  val more_simp_thms = basic_simp_thms @ @{thms simp_thms(11,15,16,21)};
    13.6  
    13.7 -val sum_prod_thms_map = @{thms id_apply map_pair_simp prod.case sum.case sum_map.simps};
    13.8 +val sum_prod_thms_map = @{thms id_apply map_pair_simp prod.case sum.case map_sum.simps};
    13.9  val sum_prod_thms_set =
   13.10    @{thms UN_empty UN_insert Un_empty_left Un_empty_right Un_iff UN_simps(10) UN_iff
   13.11        Union_Un_distrib image_iff o_apply map_pair_simp
   13.12 -      mem_Collect_eq prod_set_simps sum_map.simps sum_set_simps};
   13.13 +      mem_Collect_eq prod_set_simps map_sum.simps sum_set_simps};
   13.14  val sum_prod_thms_rel = @{thms prod_rel_apply sum_rel_simps id_apply};
   13.15  
   13.16  fun hhf_concl_conv cv ctxt ct =
    14.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Thu Mar 06 12:17:26 2014 +0100
    14.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Thu Mar 06 13:36:15 2014 +0100
    14.3 @@ -38,12 +38,12 @@
    14.4        fT --> gT --> HOLogic.mk_prodT (fAT, gAT) --> HOLogic.mk_prodT (fBT, gBT)) $ f $ g
    14.5    end;
    14.6  
    14.7 -fun mk_sum_map f g =
    14.8 +fun mk_map_sum f g =
    14.9    let
   14.10      val ((fAT, fBT), fT) = `dest_funT (fastype_of f);
   14.11      val ((gAT, gBT), gT) = `dest_funT (fastype_of g);
   14.12    in
   14.13 -    Const (@{const_name sum_map}, fT --> gT --> mk_sumT (fAT, gAT) --> mk_sumT (fBT, gBT)) $ f $ g
   14.14 +    Const (@{const_name map_sum}, fT --> gT --> mk_sumT (fAT, gAT) --> mk_sumT (fBT, gBT)) $ f $ g
   14.15    end;
   14.16  
   14.17  fun construct_mutualized_fp fp fpTs (fp_sugars : fp_sugar list) bs resBs (resDs, Dss) bnfs
   14.18 @@ -61,7 +61,7 @@
   14.19      val co_alg_argT = fp_case fp range_type domain_type;
   14.20      val co_alg_funT = fp_case fp domain_type range_type;
   14.21      val mk_co_product = curry (fp_case fp mk_convol mk_case_sum);
   14.22 -    val mk_map_co_product = fp_case fp mk_prod_map mk_sum_map;
   14.23 +    val mk_map_co_product = fp_case fp mk_prod_map mk_map_sum;
   14.24      val co_proj1_const = fp_case fp (fst_const o fst) (uncurry Inl_const o dest_sumT o snd);
   14.25      val mk_co_productT = curry (fp_case fp HOLogic.mk_prodT mk_sumT);
   14.26      val dest_co_productT = fp_case fp HOLogic.dest_prodT dest_sumT;
   14.27 @@ -404,11 +404,11 @@
   14.28          val fp_xtor_co_recs = map (mk_pointfree lthy) (of_fp_res #xtor_co_rec_thms);
   14.29  
   14.30          val fold_thms = fp_case fp @{thm comp_assoc} @{thm comp_assoc[symmetric]} ::
   14.31 -          map (fn thm => thm RS rewrite_comp_comp) @{thms map_pair.comp sum_map.comp} @
   14.32 -          @{thms id_apply comp_id id_comp map_pair.comp map_pair.id sum_map.comp sum_map.id};
   14.33 +          map (fn thm => thm RS rewrite_comp_comp) @{thms map_pair.comp map_sum.comp} @
   14.34 +          @{thms id_apply comp_id id_comp map_pair.comp map_pair.id map_sum.comp map_sum.id};
   14.35          val rec_thms = fold_thms @ fp_case fp
   14.36            @{thms fst_convol map_pair_o_convol convol_o}
   14.37 -          @{thms case_sum_o_inj(1) case_sum_o_sum_map o_case_sum};
   14.38 +          @{thms case_sum_o_inj(1) case_sum_o_map_sum o_case_sum};
   14.39  
   14.40          val eq_thm_prop_untyped = Term.aconv_untyped o pairself Thm.full_prop_of;
   14.41  
    15.1 --- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Thu Mar 06 12:17:26 2014 +0100
    15.2 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Thu Mar 06 13:36:15 2014 +0100
    15.3 @@ -527,7 +527,7 @@
    15.4        else refl);
    15.5      val map_cong_passive_args2 = replicate m (fp_case fp @{thm comp_id} @{thm id_comp} RS fun_cong);
    15.6      val map_cong_active_args2 = replicate n (if is_rec
    15.7 -      then fp_case fp @{thm map_pair_o_convol_id} @{thm case_sum_o_sum_map_id}
    15.8 +      then fp_case fp @{thm map_pair_o_convol_id} @{thm case_sum_o_map_sum_id}
    15.9        else fp_case fp @{thm id_comp} @{thm comp_id} RS fun_cong);
   15.10      fun mk_map_congs passive active = map (fn thm => thm OF (passive @ active) RS ext) map_cong0s;
   15.11      val map_cong1s = mk_map_congs map_cong_passive_args1 map_cong_active_args1;