--- 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
--- 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 \<equiv> NNode n (the_inv fset as)"
definition "cont \<equiv> fset o ccont"
-definition "unfold rt ct \<equiv> corec_dtree rt (the_inv fset o image (sum_map id Inr) o ct)"
+definition "unfold rt ct \<equiv> corec_dtree rt (the_inv fset o image (map_sum id Inr) o ct)"
definition "corec rt ct \<equiv> 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) \<Longrightarrow> cont (unfold rt ct b) = image (id \<oplus> 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"
--- 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 \<in> Inl -` cont tr" by(cases ttr, auto)
next
fix t assume "Inl t \<in> cont tr" thus "t \<in> 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' \<in> cont tr"
shows "Inr (root tr') \<in> 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 "\<exists> 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)) \<in> 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 \<oplus> (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 \<in> cont (pick n)"
shows "(id \<oplus> (root \<circ> H \<circ> root)) t_tr = (id \<oplus> 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 \<oplus> root) ` cont (H n)) \<in> P" (is "?L \<in> P")
proof-
have "?L = (n, (id \<oplus> 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 "... \<in> P" by (metis (lifting) wf_pick root_pick wf_P n tr0)
--- 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 "\<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)
@@ -37,7 +37,7 @@
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
@@ -51,7 +51,7 @@
"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
--- 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 = (\<forall>x y. R x y \<longrightarrow> (fun_rel S T) (f x) (g y))"
--- 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 \<Rightarrow> 's" and f2 :: "'p \<Rightarrow> 't" and g1 :: "'s \<Rightarrow> 'q" and g2 :: "'t \<Rightarrow> '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 \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> 'r" and g1 g2
assume a1: "\<And>z. z \<in> setl x \<Longrightarrow> f1 z = g1 z" and
a2: "\<And>z. z \<in> setr x \<Longrightarrow> 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 \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> '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 \<Rightarrow> 'q" and f2 :: "'p \<Rightarrow> '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 \<subseteq> Collect (split R) \<and> setr x \<subseteq> Collect (split S)} (sum_map fst fst))\<inverse>\<inverse> OO
- Grp {x. setl x \<subseteq> Collect (split R) \<and> setr x \<subseteq> Collect (split S)} (sum_map snd snd)"
+ (Grp {x. setl x \<subseteq> Collect (split R) \<and> setr x \<subseteq> Collect (split S)} (map_sum fst fst))\<inverse>\<inverse> OO
+ Grp {x. setl x \<subseteq> Collect (split R) \<and> setr x \<subseteq> 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)
--- 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 \<subset> 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: "\<forall>a\<in>Field r. f a \<in> Field s \<and> f ` underS r a \<subseteq> underS s (f a)"
unfolding ordLeq_def2 by blast
- let ?f = "sum_map f id"
+ let ?f = "map_sum f id"
from f have "\<forall>a\<in>Field (r +o t).
?f a \<in> Field (s +o t) \<and> ?f ` underS (r +o t) a \<subseteq> underS (s +o t) (?f a)"
unfolding Field_osum underS_def by (fastforce simp: osum_def)
--- 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\<cdot>(map_option (\<lambda>x. f\<cdot>x) (decode_option\<cdot>x)) = sum_map' ID f\<cdot>x"
+ "encode_option\<cdot>(map_option (\<lambda>x. f\<cdot>x) (decode_option\<cdot>x)) = map_sum' ID f\<cdot>x"
by (induct x, simp_all add: decode_option_def encode_option_def)
lemma isodefl_option [domain_isodefl]:
--- 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 (\<lambda>a. Inl (f a)) (\<lambda>b. Inr (g b))"
+lemma map_sum_eq: "map_sum f g = case_sum (\<lambda>a. Inl (f a)) (\<lambda>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 (\<lambda>(x, y). f x y)"
assumes g: "cont (\<lambda>(x, y). g x y)"
assumes h: "cont (\<lambda>x. h x)"
- shows "cont (\<lambda>x. sum_map (\<lambda>y. f x y) (\<lambda>y. g x y) (h x))"
-using assms by (simp add: sum_map_eq prod_cont_iff)
+ shows "cont (\<lambda>x. map_sum (\<lambda>y. f x y) (\<lambda>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\<cdot>LIFTDEFL('a)\<cdot>LIFTDEFL('b)"
by (rule liftdefl_sum_def)
-abbreviation sum_map'
- where "sum_map' f g \<equiv> Abs_cfun (sum_map (Rep_cfun f) (Rep_cfun g))"
+abbreviation map_sum'
+ where "map_sum' f g \<equiv> 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]:
- "\<lbrakk>deflation d1; deflation d2\<rbrakk> \<Longrightarrow> deflation (sum_map' d1 d2)"
+lemma deflation_map_sum [domain_deflation]:
+ "\<lbrakk>deflation d1; deflation d2\<rbrakk> \<Longrightarrow> 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\<cdot>(u_map\<cdot>(sum_map' f g)\<cdot>(decode_sum_u\<cdot>x))
+lemma encode_sum_u_map_sum:
+ "encode_sum_u\<cdot>(u_map\<cdot>(map_sum' f g)\<cdot>(decode_sum_u\<cdot>x))
= ssum_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>g)\<cdot>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 \<rightarrow> 'a"
assumes "isodefl' d1 t1" and "isodefl' d2 t2"
- shows "isodefl' (sum_map' d1 d2) (sum_liftdefl\<cdot>t1\<cdot>t2)"
+ shows "isodefl' (map_sum' d1 d2) (sum_liftdefl\<cdot>t1\<cdot>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
--- 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 \<longleftrightarrow> sum_rel (\<lambda>x. R1 (f1 x)) (\<lambda>x. R2 (f2 x)) x y"
+ "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"
by (simp add: sum_rel_def split: sum.split)
lemma sum_rel_map2:
- "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"
+ "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"
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
--- 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)
--- 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 \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a + 'b \<Rightarrow> '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 \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a + 'b \<Rightarrow> '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 \<circ> sum_map h i = sum_map (f \<circ> h) (g \<circ> i)"
+ show "map_sum f g \<circ> map_sum h i = map_sum (f \<circ> h) (g \<circ> i)"
proof
fix s
- show "(sum_map f g \<circ> sum_map h i) s = sum_map (f \<circ> h) (g \<circ> i) s"
+ show "(map_sum f g \<circ> map_sum h i) s = map_sum (f \<circ> h) (g \<circ> 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
--- 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 =
--- 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;
--- 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;