# HG changeset patch # User blanchet # Date 1394109375 -3600 # Node ID 62156e694f3d27775968357a564057b6f136386f # Parent 25a90cebbbe5a2df88b82872d571971dadd1f8db renamed 'map_sum' to 'sum_map' diff -r 25a90cebbbe5 -r 62156e694f3d NEWS --- a/NEWS Thu Mar 06 12:17:26 2014 +0100 +++ b/NEWS Thu Mar 06 13:36:15 2014 +0100 @@ -190,6 +190,9 @@ the.simps ~> option.sel INCOMPATIBILITY. +* The following map function has been renamed: + map_sum ~> sum_map + * New theory: Cardinals/Ordinal_Arithmetic.thy diff -r 25a90cebbbe5 -r 62156e694f3d src/HOL/BNF_Examples/Derivation_Trees/DTree.thy --- a/src/HOL/BNF_Examples/Derivation_Trees/DTree.thy Thu Mar 06 12:17:26 2014 +0100 +++ b/src/HOL/BNF_Examples/Derivation_Trees/DTree.thy Thu Mar 06 13:36:15 2014 +0100 @@ -20,7 +20,7 @@ definition "Node n as \ NNode n (the_inv fset as)" definition "cont \ fset o ccont" -definition "unfold rt ct \ corec_dtree rt (the_inv fset o image (sum_map id Inr) o ct)" +definition "unfold rt ct \ corec_dtree rt (the_inv fset o image (map_sum id Inr) o ct)" definition "corec rt ct \ corec_dtree rt (the_inv fset o ct)" lemma finite_cont[simp]: "finite (cont tr)" @@ -75,10 +75,10 @@ lemma unfold: "root (unfold rt ct b) = rt b" "finite (ct b) \ cont (unfold rt ct b) = image (id \ unfold rt ct) (ct b)" -using dtree.sel_corec[of rt "the_inv fset o image (sum_map id Inr) o ct" b] unfolding unfold_def +using dtree.sel_corec[of rt "the_inv fset o image (map_sum id Inr) o ct" b] unfolding unfold_def apply blast unfolding cont_def comp_def -by (simp add: case_sum_o_inj sum_map.compositionality image_image) +by (simp add: case_sum_o_inj map_sum.compositionality image_image) lemma corec: "root (corec rt ct b) = rt b" diff -r 25a90cebbbe5 -r 62156e694f3d src/HOL/BNF_Examples/Derivation_Trees/Gram_Lang.thy --- a/src/HOL/BNF_Examples/Derivation_Trees/Gram_Lang.thy Thu Mar 06 12:17:26 2014 +0100 +++ b/src/HOL/BNF_Examples/Derivation_Trees/Gram_Lang.thy Thu Mar 06 13:36:15 2014 +0100 @@ -334,13 +334,13 @@ thus "t \ Inl -` cont tr" by(cases ttr, auto) next fix t assume "Inl t \ cont tr" thus "t \ Inl -` prodOf tr" - by (metis (lifting) id_def image_iff sum_map.simps(1) vimageI2) + by (metis (lifting) id_def image_iff map_sum.simps(1) vimageI2) qed lemma root_prodOf: assumes "Inr tr' \ cont tr" shows "Inr (root tr') \ prodOf tr" -by (metis (lifting) assms image_iff sum_map.simps(2)) +by (metis (lifting) assms image_iff map_sum.simps(2)) subsection{* Well-Formed Derivation Trees *} @@ -480,8 +480,8 @@ proof- {fix tr assume "\ n. tr = deftr n" hence "wf tr" apply(induct rule: wf_raw_coind) apply safe - unfolding deftr_simps image_compose[symmetric] sum_map.comp id_comp - root_o_deftr sum_map.id image_id id_apply apply(rule S_P) + unfolding deftr_simps image_compose[symmetric] map_sum.comp id_comp + root_o_deftr map_sum.id image_id id_apply apply(rule S_P) unfolding inj_on_def by auto } thus ?thesis by auto @@ -565,7 +565,7 @@ show "(root (hsubst tr), prodOf (hsubst tr)) \ P" unfolding tr1 apply(cases "root tr = root tr0") using wf_P[OF dtr] wf_P[OF tr0] - by (auto simp add: image_compose[symmetric] sum_map.comp) + by (auto simp add: image_compose[symmetric] map_sum.comp) show "inj_on root (Inr -` cont (hsubst tr))" apply(cases "root tr = root tr0") using wf_inj_on[OF dtr] wf_inj_on[OF tr0] unfolding inj_on_def by (auto, blast) @@ -958,7 +958,7 @@ lemma cont_H[simp]: "cont (H n) = (id \ (H o root)) ` cont (pick n)" -apply(subst id_comp[symmetric, of id]) unfolding sum_map.comp[symmetric] +apply(subst id_comp[symmetric, of id]) unfolding map_sum.comp[symmetric] unfolding image_compose unfolding H_c_def[symmetric] using unfold(2)[of H_c n H_r, OF finite_H_c] unfolding H_def .. @@ -1001,9 +1001,9 @@ assumes n: "inItr UNIV tr0 n" and t_tr: "t_tr \ cont (pick n)" shows "(id \ (root \ H \ root)) t_tr = (id \ root) t_tr" using assms apply(cases t_tr) - apply (metis (lifting) sum_map.simps(1)) + apply (metis (lifting) map_sum.simps(1)) using pick H_def H_r_def unfold(1) - inItr.Base comp_apply subtr_StepL subtr_inItr sum_map.simps(2) + inItr.Base comp_apply subtr_StepL subtr_inItr map_sum.simps(2) by (metis UNIV_I) lemma H_P: @@ -1011,7 +1011,7 @@ shows "(n, (id \ root) ` cont (H n)) \ P" (is "?L \ P") proof- have "?L = (n, (id \ root) ` cont (pick n))" - unfolding cont_H image_compose[symmetric] sum_map.comp id_comp comp_assoc[symmetric] + unfolding cont_H image_compose[symmetric] map_sum.comp id_comp comp_assoc[symmetric] unfolding Pair_eq apply(rule conjI[OF refl]) apply(rule image_cong[OF refl]) by (rule root_H_root[OF n]) moreover have "... \ P" by (metis (lifting) wf_pick root_pick wf_P n tr0) diff -r 25a90cebbbe5 -r 62156e694f3d src/HOL/BNF_Examples/Derivation_Trees/Prelim.thy --- a/src/HOL/BNF_Examples/Derivation_Trees/Prelim.thy Thu Mar 06 12:17:26 2014 +0100 +++ b/src/HOL/BNF_Examples/Derivation_Trees/Prelim.thy Thu Mar 06 13:36:15 2014 +0100 @@ -19,12 +19,12 @@ apply(rule ext) by (simp add: convol_def) abbreviation sm_abbrev (infix "\" 60) -where "f \ g \ Sum_Type.sum_map f g" +where "f \ g \ Sum_Type.map_sum f g" -lemma sum_map_InlD: "(f \ g) z = Inl x \ \y. z = Inl y \ f y = x" +lemma map_sum_InlD: "(f \ g) z = Inl x \ \y. z = Inl y \ f y = x" by (cases z) auto -lemma sum_map_InrD: "(f \ g) z = Inr x \ \y. z = Inr y \ g y = x" +lemma map_sum_InrD: "(f \ g) z = Inr x \ \y. z = Inr y \ g y = x" by (cases z) auto abbreviation case_sum_abbrev ("[[_,_]]" 800) @@ -37,7 +37,7 @@ lemma Inl_oplus_iff[simp]: "Inl tr \ (id \ f) ` tns \ Inl tr \ 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 \ f) ` tns = Inl -` tns" using Inl_oplus_iff unfolding vimage_def by auto @@ -51,7 +51,7 @@ "Inr tr \ (id \ f) ` tns \ (\ n. Inr n \ tns \ 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 \ f) ` tns = f ` (Inr -` tns)" using Inr_oplus_iff unfolding vimage_def by auto diff -r 25a90cebbbe5 -r 62156e694f3d src/HOL/BNF_FP_Base.thy --- a/src/HOL/BNF_FP_Base.thy Thu Mar 06 12:17:26 2014 +0100 +++ b/src/HOL/BNF_FP_Base.thy Thu Mar 06 13:36:15 2014 +0100 @@ -125,11 +125,11 @@ lemma o_case_sum: "h o case_sum f g = case_sum (h o f) (h o g)" unfolding comp_def by (auto split: sum.splits) -lemma case_sum_o_sum_map: "case_sum f g o sum_map h1 h2 = case_sum (f o h1) (g o h2)" +lemma case_sum_o_map_sum: "case_sum f g o map_sum h1 h2 = case_sum (f o h1) (g o h2)" unfolding comp_def by (auto split: sum.splits) -lemma case_sum_o_sum_map_id: "(case_sum id g o sum_map f id) x = case_sum (f o id) g x" - unfolding case_sum_o_sum_map id_comp comp_id .. +lemma case_sum_o_map_sum_id: "(case_sum id g o map_sum f id) x = case_sum (f o id) g x" + unfolding case_sum_o_map_sum id_comp comp_id .. lemma fun_rel_def_butlast: "fun_rel R (fun_rel S T) f g = (\x y. R x y \ (fun_rel S T) (f x) (g y))" diff -r 25a90cebbbe5 -r 62156e694f3d src/HOL/Basic_BNFs.thy --- a/src/HOL/Basic_BNFs.thy Thu Mar 06 12:17:26 2014 +0100 +++ b/src/HOL/Basic_BNFs.thy Thu Mar 06 13:36:15 2014 +0100 @@ -53,22 +53,22 @@ unfolding sum_rel_def by simp_all bnf "'a + 'b" - map: sum_map + map: map_sum sets: setl setr bd: natLeq wits: Inl Inr rel: sum_rel proof - - show "sum_map id id = id" by (rule sum_map.id) + show "map_sum id id = id" by (rule map_sum.id) next fix f1 :: "'o \ 's" and f2 :: "'p \ 't" and g1 :: "'s \ 'q" and g2 :: "'t \ 'r" - show "sum_map (g1 o f1) (g2 o f2) = sum_map g1 g2 o sum_map f1 f2" - by (rule sum_map.comp[symmetric]) + show "map_sum (g1 o f1) (g2 o f2) = map_sum g1 g2 o map_sum f1 f2" + by (rule map_sum.comp[symmetric]) next fix x and f1 :: "'o \ 'q" and f2 :: "'p \ 'r" and g1 g2 assume a1: "\z. z \ setl x \ f1 z = g1 z" and a2: "\z. z \ setr x \ f2 z = g2 z" - thus "sum_map f1 f2 x = sum_map g1 g2 x" + thus "map_sum f1 f2 x = map_sum g1 g2 x" proof (cases x) case Inl thus ?thesis using a1 by (clarsimp simp: setl_def) next @@ -76,11 +76,11 @@ qed next fix f1 :: "'o \ 'q" and f2 :: "'p \ 'r" - show "setl o sum_map f1 f2 = image f1 o setl" + show "setl o map_sum f1 f2 = image f1 o setl" by (rule ext, unfold o_apply) (simp add: setl_def split: sum.split) next fix f1 :: "'o \ 'q" and f2 :: "'p \ 'r" - show "setr o sum_map f1 f2 = image f2 o setr" + show "setr o map_sum f1 f2 = image f2 o setr" by (rule ext, unfold o_apply) (simp add: setr_def split: sum.split) next show "card_order natLeq" by (rule natLeq_card_order) @@ -105,8 +105,8 @@ next fix R S show "sum_rel R S = - (Grp {x. setl x \ Collect (split R) \ setr x \ Collect (split S)} (sum_map fst fst))\\ OO - Grp {x. setl x \ Collect (split R) \ setr x \ Collect (split S)} (sum_map snd snd)" + (Grp {x. setl x \ Collect (split R) \ setr x \ Collect (split S)} (map_sum fst fst))\\ OO + Grp {x. setl x \ Collect (split R) \ setr x \ Collect (split S)} (map_sum snd snd)" unfolding setl_def setr_def sum_rel_def Grp_def relcompp.simps conversep.simps fun_eq_iff by (fastforce split: sum.splits) qed (auto simp: sum_set_defs) diff -r 25a90cebbbe5 -r 62156e694f3d src/HOL/Cardinals/Ordinal_Arithmetic.thy --- a/src/HOL/Cardinals/Ordinal_Arithmetic.thy Thu Mar 06 12:17:26 2014 +0100 +++ b/src/HOL/Cardinals/Ordinal_Arithmetic.thy Thu Mar 06 13:36:15 2014 +0100 @@ -953,7 +953,7 @@ proof - from assms(1) obtain f where r: "Well_order r" and s: "Well_order s" and f: "iso r s f" unfolding ordIso_def by blast - let ?f = "sum_map f id" + let ?f = "map_sum f id" from f have "inj_on ?f (Field ?L)" unfolding Field_osum iso_def bij_betw_def inj_on_def by fastforce with f have "bij_betw ?f (Field ?L) (Field ?R)" @@ -971,7 +971,7 @@ proof - from assms(1) obtain f where r: "Well_order r" and s: "Well_order s" and f: "iso r s f" unfolding ordIso_def by blast - let ?f = "sum_map id f" + let ?f = "map_sum id f" from f have "inj_on ?f (Field ?L)" unfolding Field_osum iso_def bij_betw_def inj_on_def by fastforce with f have "bij_betw ?f (Field ?L) (Field ?R)" @@ -1129,7 +1129,7 @@ hence *: "inj_on f (Field s)" "compat s t f" "ofilter t (f ` Field s)" "f ` Field s \ Field t" using embed_iff_compat_inj_on_ofilter[OF s t, of f] embedS_iff[OF s, of t f] unfolding embedS_def by auto - let ?f = "sum_map id f" + let ?f = "map_sum id f" from *(1) have "inj_on ?f (Field ?L)" unfolding Field_osum inj_on_def by fastforce moreover from *(2,4) have "compat ?L ?R ?f" unfolding compat_def osum_def map_pair_def by fastforce @@ -1153,7 +1153,7 @@ proof - from assms obtain f where f: "\a\Field r. f a \ Field s \ f ` underS r a \ underS s (f a)" unfolding ordLeq_def2 by blast - let ?f = "sum_map f id" + let ?f = "map_sum f id" from f have "\a\Field (r +o t). ?f a \ Field (s +o t) \ ?f ` underS (r +o t) a \ underS (s +o t) (?f a)" unfolding Field_osum underS_def by (fastforce simp: osum_def) diff -r 25a90cebbbe5 -r 62156e694f3d src/HOL/HOLCF/Library/Option_Cpo.thy --- a/src/HOL/HOLCF/Library/Option_Cpo.thy Thu Mar 06 12:17:26 2014 +0100 +++ b/src/HOL/HOLCF/Library/Option_Cpo.thy Thu Mar 06 13:36:15 2014 +0100 @@ -275,7 +275,7 @@ done lemma encode_option_option_map: - "encode_option\(map_option (\x. f\x) (decode_option\x)) = sum_map' ID f\x" + "encode_option\(map_option (\x. f\x) (decode_option\x)) = map_sum' ID f\x" by (induct x, simp_all add: decode_option_def encode_option_def) lemma isodefl_option [domain_isodefl]: diff -r 25a90cebbbe5 -r 62156e694f3d src/HOL/HOLCF/Library/Sum_Cpo.thy --- a/src/HOL/HOLCF/Library/Sum_Cpo.thy Thu Mar 06 12:17:26 2014 +0100 +++ b/src/HOL/HOLCF/Library/Sum_Cpo.thy Thu Mar 06 13:36:15 2014 +0100 @@ -177,15 +177,15 @@ text {* Continuity of map function. *} -lemma sum_map_eq: "sum_map f g = case_sum (\a. Inl (f a)) (\b. Inr (g b))" +lemma map_sum_eq: "map_sum f g = case_sum (\a. Inl (f a)) (\b. Inr (g b))" by (rule ext, case_tac x, simp_all) -lemma cont2cont_sum_map [simp, cont2cont]: +lemma cont2cont_map_sum [simp, cont2cont]: assumes f: "cont (\(x, y). f x y)" assumes g: "cont (\(x, y). g x y)" assumes h: "cont (\x. h x)" - shows "cont (\x. sum_map (\y. f x y) (\y. g x y) (h x))" -using assms by (simp add: sum_map_eq prod_cont_iff) + shows "cont (\x. map_sum (\y. f x y) (\y. g x y) (h x))" +using assms by (simp add: map_sum_eq prod_cont_iff) subsection {* Compactness and chain-finiteness *} @@ -334,21 +334,21 @@ sum_liftdefl\LIFTDEFL('a)\LIFTDEFL('b)" by (rule liftdefl_sum_def) -abbreviation sum_map' - where "sum_map' f g \ Abs_cfun (sum_map (Rep_cfun f) (Rep_cfun g))" +abbreviation map_sum' + where "map_sum' f g \ Abs_cfun (map_sum (Rep_cfun f) (Rep_cfun g))" -lemma sum_map_ID [domain_map_ID]: "sum_map' ID ID = ID" -by (simp add: ID_def cfun_eq_iff sum_map.identity id_def) +lemma map_sum_ID [domain_map_ID]: "map_sum' ID ID = ID" +by (simp add: ID_def cfun_eq_iff map_sum.identity id_def) -lemma deflation_sum_map [domain_deflation]: - "\deflation d1; deflation d2\ \ deflation (sum_map' d1 d2)" +lemma deflation_map_sum [domain_deflation]: + "\deflation d1; deflation d2\ \ deflation (map_sum' d1 d2)" apply default apply (induct_tac x, simp_all add: deflation.idem) apply (induct_tac x, simp_all add: deflation.below) done -lemma encode_sum_u_sum_map: - "encode_sum_u\(u_map\(sum_map' f g)\(decode_sum_u\x)) +lemma encode_sum_u_map_sum: + "encode_sum_u\(u_map\(map_sum' f g)\(decode_sum_u\x)) = ssum_map\(u_map\f)\(u_map\g)\x" apply (induct x, simp add: decode_sum_u_def encode_sum_u_def) apply (case_tac x, simp, simp add: decode_sum_u_def encode_sum_u_def) @@ -358,10 +358,10 @@ lemma isodefl_sum [domain_isodefl]: fixes d :: "'a::predomain \ 'a" assumes "isodefl' d1 t1" and "isodefl' d2 t2" - shows "isodefl' (sum_map' d1 d2) (sum_liftdefl\t1\t2)" + shows "isodefl' (map_sum' d1 d2) (sum_liftdefl\t1\t2)" using assms unfolding isodefl'_def liftemb_sum_def liftprj_sum_def apply (simp add: sum_liftdefl_def cast_udefl cast_ssum_defl cast_u_liftdefl) -apply (simp add: cfcomp1 encode_sum_u_sum_map) +apply (simp add: cfcomp1 encode_sum_u_map_sum) apply (simp add: ssum_map_map u_emb_bottom) done diff -r 25a90cebbbe5 -r 62156e694f3d src/HOL/Library/Quotient_Sum.thy --- a/src/HOL/Library/Quotient_Sum.thy Thu Mar 06 12:17:26 2014 +0100 +++ b/src/HOL/Library/Quotient_Sum.thy Thu Mar 06 13:36:15 2014 +0100 @@ -11,16 +11,16 @@ subsection {* Rules for the Quotient package *} lemma sum_rel_map1: - "sum_rel R1 R2 (sum_map f1 f2 x) y \ sum_rel (\x. R1 (f1 x)) (\x. R2 (f2 x)) x y" + "sum_rel R1 R2 (map_sum f1 f2 x) y \ sum_rel (\x. R1 (f1 x)) (\x. R2 (f2 x)) x y" by (simp add: sum_rel_def split: sum.split) lemma sum_rel_map2: - "sum_rel R1 R2 x (sum_map f1 f2 y) \ sum_rel (\x y. R1 x (f1 y)) (\x y. R2 x (f2 y)) x y" + "sum_rel R1 R2 x (map_sum f1 f2 y) \ sum_rel (\x y. R1 x (f1 y)) (\x y. R2 x (f2 y)) x y" by (simp add: sum_rel_def split: sum.split) -lemma sum_map_id [id_simps]: - "sum_map id id = id" - by (simp add: id_def sum_map.identity fun_eq_iff) +lemma map_sum_id [id_simps]: + "map_sum id id = id" + by (simp add: id_def map_sum.identity fun_eq_iff) lemma sum_rel_eq [id_simps]: "sum_rel (op =) (op =) = (op =)" @@ -45,9 +45,9 @@ lemma sum_quotient [quot_thm]: assumes q1: "Quotient3 R1 Abs1 Rep1" assumes q2: "Quotient3 R2 Abs2 Rep2" - shows "Quotient3 (sum_rel R1 R2) (sum_map Abs1 Abs2) (sum_map Rep1 Rep2)" + shows "Quotient3 (sum_rel R1 R2) (map_sum Abs1 Abs2) (map_sum Rep1 Rep2)" apply (rule Quotient3I) - apply (simp_all add: sum_map.compositionality comp_def sum_map.identity sum_rel_eq sum_rel_map1 sum_rel_map2 + apply (simp_all add: map_sum.compositionality comp_def map_sum.identity sum_rel_eq sum_rel_map1 sum_rel_map2 Quotient3_abs_rep [OF q1] Quotient3_rel_rep [OF q1] Quotient3_abs_rep [OF q2] Quotient3_rel_rep [OF q2]) using Quotient3_rel [OF q1] Quotient3_rel [OF q2] apply (simp add: sum_rel_def comp_def split: sum.split) @@ -70,7 +70,7 @@ lemma sum_Inl_prs [quot_preserve]: assumes q1: "Quotient3 R1 Abs1 Rep1" assumes q2: "Quotient3 R2 Abs2 Rep2" - shows "(Rep1 ---> sum_map Abs1 Abs2) Inl = Inl" + shows "(Rep1 ---> map_sum Abs1 Abs2) Inl = Inl" apply(simp add: fun_eq_iff) apply(simp add: Quotient3_abs_rep[OF q1]) done @@ -78,7 +78,7 @@ lemma sum_Inr_prs [quot_preserve]: assumes q1: "Quotient3 R1 Abs1 Rep1" assumes q2: "Quotient3 R2 Abs2 Rep2" - shows "(Rep2 ---> sum_map Abs1 Abs2) Inr = Inr" + shows "(Rep2 ---> map_sum Abs1 Abs2) Inr = Inr" apply(simp add: fun_eq_iff) apply(simp add: Quotient3_abs_rep[OF q2]) done diff -r 25a90cebbbe5 -r 62156e694f3d src/HOL/Lifting_Sum.thy --- a/src/HOL/Lifting_Sum.thy Thu Mar 06 12:17:26 2014 +0100 +++ b/src/HOL/Lifting_Sum.thy Thu Mar 06 13:36:15 2014 +0100 @@ -59,8 +59,7 @@ lemma Quotient_sum[quot_map]: assumes "Quotient R1 Abs1 Rep1 T1" assumes "Quotient R2 Abs2 Rep2 T2" - shows "Quotient (sum_rel R1 R2) (sum_map Abs1 Abs2) - (sum_map Rep1 Rep2) (sum_rel T1 T2)" + shows "Quotient (sum_rel R1 R2) (map_sum Abs1 Abs2) (map_sum Rep1 Rep2) (sum_rel T1 T2)" using assms unfolding Quotient_alt_def by (simp add: split_sum_all) diff -r 25a90cebbbe5 -r 62156e694f3d src/HOL/Sum_Type.thy --- a/src/HOL/Sum_Type.thy Thu Mar 06 12:17:26 2014 +0100 +++ b/src/HOL/Sum_Type.thy Thu Mar 06 13:36:15 2014 +0100 @@ -119,24 +119,24 @@ setup {* Sign.parent_path *} -primrec sum_map :: "('a \ 'c) \ ('b \ 'd) \ 'a + 'b \ 'c + 'd" where - "sum_map f1 f2 (Inl a) = Inl (f1 a)" -| "sum_map f1 f2 (Inr a) = Inr (f2 a)" +primrec map_sum :: "('a \ 'c) \ ('b \ 'd) \ 'a + 'b \ 'c + 'd" where + "map_sum f1 f2 (Inl a) = Inl (f1 a)" +| "map_sum f1 f2 (Inr a) = Inr (f2 a)" -functor sum_map: sum_map proof - +functor map_sum: map_sum proof - fix f g h i - show "sum_map f g \ sum_map h i = sum_map (f \ h) (g \ i)" + show "map_sum f g \ map_sum h i = map_sum (f \ h) (g \ i)" proof fix s - show "(sum_map f g \ sum_map h i) s = sum_map (f \ h) (g \ i) s" + show "(map_sum f g \ map_sum h i) s = map_sum (f \ h) (g \ i) s" by (cases s) simp_all qed next fix s - show "sum_map id id = id" + show "map_sum id id = id" proof fix s - show "sum_map id id s = id s" + show "map_sum id id s = id s" by (cases s) simp_all qed qed diff -r 25a90cebbbe5 -r 62156e694f3d src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Thu Mar 06 12:17:26 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Thu Mar 06 13:36:15 2014 +0100 @@ -37,11 +37,11 @@ val basic_simp_thms = @{thms simp_thms(7,8,12,14,22,24)}; val more_simp_thms = basic_simp_thms @ @{thms simp_thms(11,15,16,21)}; -val sum_prod_thms_map = @{thms id_apply map_pair_simp prod.case sum.case sum_map.simps}; +val sum_prod_thms_map = @{thms id_apply map_pair_simp prod.case sum.case map_sum.simps}; val sum_prod_thms_set = @{thms UN_empty UN_insert Un_empty_left Un_empty_right Un_iff UN_simps(10) UN_iff Union_Un_distrib image_iff o_apply map_pair_simp - mem_Collect_eq prod_set_simps sum_map.simps sum_set_simps}; + mem_Collect_eq prod_set_simps map_sum.simps sum_set_simps}; val sum_prod_thms_rel = @{thms prod_rel_apply sum_rel_simps id_apply}; fun hhf_concl_conv cv ctxt ct = diff -r 25a90cebbbe5 -r 62156e694f3d src/HOL/Tools/BNF/bnf_fp_n2m.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Thu Mar 06 12:17:26 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Thu Mar 06 13:36:15 2014 +0100 @@ -38,12 +38,12 @@ fT --> gT --> HOLogic.mk_prodT (fAT, gAT) --> HOLogic.mk_prodT (fBT, gBT)) $ f $ g end; -fun mk_sum_map f g = +fun mk_map_sum f g = let val ((fAT, fBT), fT) = `dest_funT (fastype_of f); val ((gAT, gBT), gT) = `dest_funT (fastype_of g); in - Const (@{const_name sum_map}, fT --> gT --> mk_sumT (fAT, gAT) --> mk_sumT (fBT, gBT)) $ f $ g + Const (@{const_name map_sum}, fT --> gT --> mk_sumT (fAT, gAT) --> mk_sumT (fBT, gBT)) $ f $ g end; fun construct_mutualized_fp fp fpTs (fp_sugars : fp_sugar list) bs resBs (resDs, Dss) bnfs @@ -61,7 +61,7 @@ val co_alg_argT = fp_case fp range_type domain_type; val co_alg_funT = fp_case fp domain_type range_type; val mk_co_product = curry (fp_case fp mk_convol mk_case_sum); - val mk_map_co_product = fp_case fp mk_prod_map mk_sum_map; + val mk_map_co_product = fp_case fp mk_prod_map mk_map_sum; val co_proj1_const = fp_case fp (fst_const o fst) (uncurry Inl_const o dest_sumT o snd); val mk_co_productT = curry (fp_case fp HOLogic.mk_prodT mk_sumT); val dest_co_productT = fp_case fp HOLogic.dest_prodT dest_sumT; @@ -404,11 +404,11 @@ val fp_xtor_co_recs = map (mk_pointfree lthy) (of_fp_res #xtor_co_rec_thms); val fold_thms = fp_case fp @{thm comp_assoc} @{thm comp_assoc[symmetric]} :: - map (fn thm => thm RS rewrite_comp_comp) @{thms map_pair.comp sum_map.comp} @ - @{thms id_apply comp_id id_comp map_pair.comp map_pair.id sum_map.comp sum_map.id}; + map (fn thm => thm RS rewrite_comp_comp) @{thms map_pair.comp map_sum.comp} @ + @{thms id_apply comp_id id_comp map_pair.comp map_pair.id map_sum.comp map_sum.id}; val rec_thms = fold_thms @ fp_case fp @{thms fst_convol map_pair_o_convol convol_o} - @{thms case_sum_o_inj(1) case_sum_o_sum_map o_case_sum}; + @{thms case_sum_o_inj(1) case_sum_o_map_sum o_case_sum}; val eq_thm_prop_untyped = Term.aconv_untyped o pairself Thm.full_prop_of; diff -r 25a90cebbbe5 -r 62156e694f3d src/HOL/Tools/BNF/bnf_fp_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_util.ML Thu Mar 06 12:17:26 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Thu Mar 06 13:36:15 2014 +0100 @@ -527,7 +527,7 @@ else refl); val map_cong_passive_args2 = replicate m (fp_case fp @{thm comp_id} @{thm id_comp} RS fun_cong); val map_cong_active_args2 = replicate n (if is_rec - then fp_case fp @{thm map_pair_o_convol_id} @{thm case_sum_o_sum_map_id} + then fp_case fp @{thm map_pair_o_convol_id} @{thm case_sum_o_map_sum_id} else fp_case fp @{thm id_comp} @{thm comp_id} RS fun_cong); fun mk_map_congs passive active = map (fn thm => thm OF (passive @ active) RS ext) map_cong0s; val map_cong1s = mk_map_congs map_cong_passive_args1 map_cong_active_args1;