renamed 'map_pair' to 'map_prod'
authorblanchet
Thu Mar 06 13:36:48 2014 +0100 (2014-03-06)
changeset 5593268c5104d2204
parent 55931 62156e694f3d
child 55933 12ee2c407dad
renamed 'map_pair' to 'map_prod'
src/HOL/BNF_Examples/Lambda_Term.thy
src/HOL/BNF_Examples/Misc_Primcorec.thy
src/HOL/BNF_Examples/Misc_Primrec.thy
src/HOL/BNF_Examples/Stream_Processor.thy
src/HOL/BNF_FP_Base.thy
src/HOL/Bali/State.thy
src/HOL/Basic_BNFs.thy
src/HOL/Cardinals/Ordinal_Arithmetic.thy
src/HOL/Library/Code_Target_Int.thy
src/HOL/Library/Quotient_Product.thy
src/HOL/Lifting_Product.thy
src/HOL/List.thy
src/HOL/Matrix_LP/ComputeNumeral.thy
src/HOL/Metis_Examples/Abstraction.thy
src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
src/HOL/Product_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
src/HOL/Tools/Quickcheck/narrowing_generators.ML
src/HOL/Wellfounded.thy
src/HOL/ex/Coercion_Examples.thy
     1.1 --- a/src/HOL/BNF_Examples/Lambda_Term.thy	Thu Mar 06 13:36:15 2014 +0100
     1.2 +++ b/src/HOL/BNF_Examples/Lambda_Term.thy	Thu Mar 06 13:36:48 2014 +0100
     1.3 @@ -27,19 +27,19 @@
     1.4    "varsOf (Var a) = {a}"
     1.5  | "varsOf (App f x) = varsOf f \<union> varsOf x"
     1.6  | "varsOf (Lam x b) = {x} \<union> varsOf b"
     1.7 -| "varsOf (Lt F t) = varsOf t \<union> (\<Union> { {x} \<union> X | x X. (x,X) |\<in>| fimage (map_pair id varsOf) F})"
     1.8 +| "varsOf (Lt F t) = varsOf t \<union> (\<Union> { {x} \<union> X | x X. (x,X) |\<in>| fimage (map_prod id varsOf) F})"
     1.9  
    1.10  primrec fvarsOf :: "'a trm \<Rightarrow> 'a set" where
    1.11    "fvarsOf (Var x) = {x}"
    1.12  | "fvarsOf (App t1 t2) = fvarsOf t1 \<union> fvarsOf t2"
    1.13  | "fvarsOf (Lam x t) = fvarsOf t - {x}"
    1.14 -| "fvarsOf (Lt xts t) = fvarsOf t - {x | x X. (x,X) |\<in>| fimage (map_pair id varsOf) xts} \<union>
    1.15 -    (\<Union> {X | x X. (x,X) |\<in>| fimage (map_pair id varsOf) xts})"
    1.16 +| "fvarsOf (Lt xts t) = fvarsOf t - {x | x X. (x,X) |\<in>| fimage (map_prod id varsOf) xts} \<union>
    1.17 +    (\<Union> {X | x X. (x,X) |\<in>| fimage (map_prod id varsOf) xts})"
    1.18  
    1.19  lemma diff_Un_incl_triv: "\<lbrakk>A \<subseteq> D; C \<subseteq> E\<rbrakk> \<Longrightarrow> A - B \<union> C \<subseteq> D \<union> E" by blast
    1.20  
    1.21 -lemma in_fimage_map_pair_fset_iff[simp]:
    1.22 -  "(x, y) |\<in>| fimage (map_pair f g) xts \<longleftrightarrow> (\<exists> t1 t2. (t1, t2) |\<in>| xts \<and> x = f t1 \<and> y = g t2)"
    1.23 +lemma in_fimage_map_prod_fset_iff[simp]:
    1.24 +  "(x, y) |\<in>| fimage (map_prod f g) xts \<longleftrightarrow> (\<exists> t1 t2. (t1, t2) |\<in>| xts \<and> x = f t1 \<and> y = g t2)"
    1.25    by force
    1.26  
    1.27  lemma fvarsOf_varsOf: "fvarsOf t \<subseteq> varsOf t"
     2.1 --- a/src/HOL/BNF_Examples/Misc_Primcorec.thy	Thu Mar 06 13:36:15 2014 +0100
     2.2 +++ b/src/HOL/BNF_Examples/Misc_Primcorec.thy	Thu Mar 06 13:36:48 2014 +0100
     2.3 @@ -45,7 +45,7 @@
     2.4         Var s \<Rightarrow> Var (f s)
     2.5       | App l l' \<Rightarrow> App (rename_lam f l) (rename_lam f l')
     2.6       | Abs s l \<Rightarrow> Abs (f s) (rename_lam f l)
     2.7 -     | Let SL l \<Rightarrow> Let (fimage (map_pair f (rename_lam f)) SL) (rename_lam f l))"
     2.8 +     | Let SL l \<Rightarrow> Let (fimage (map_prod f (rename_lam f)) SL) (rename_lam f l))"
     2.9  
    2.10  primcorec
    2.11    j1_sum :: "('a\<Colon>{zero,one,plus}) \<Rightarrow> 'a J1" and
     3.1 --- a/src/HOL/BNF_Examples/Misc_Primrec.thy	Thu Mar 06 13:36:15 2014 +0100
     3.2 +++ b/src/HOL/BNF_Examples/Misc_Primrec.thy	Thu Mar 06 13:36:48 2014 +0100
     3.3 @@ -51,7 +51,7 @@
     3.4    "rename_lam f (Var s) = Var (f s)" |
     3.5    "rename_lam f (App l l') = App (rename_lam f l) (rename_lam f l')" |
     3.6    "rename_lam f (Abs s l) = Abs (f s) (rename_lam f l)" |
     3.7 -  "rename_lam f (Let SL l) = Let (fimage (map_pair f (rename_lam f)) SL) (rename_lam f l)"
     3.8 +  "rename_lam f (Let SL l) = Let (fimage (map_prod f (rename_lam f)) SL) (rename_lam f l)"
     3.9  
    3.10  primrec
    3.11    sum_i1 :: "('a\<Colon>{zero,plus}) I1 \<Rightarrow> 'a" and
     4.1 --- a/src/HOL/BNF_Examples/Stream_Processor.thy	Thu Mar 06 13:36:15 2014 +0100
     4.2 +++ b/src/HOL/BNF_Examples/Stream_Processor.thy	Thu Mar 06 13:36:48 2014 +0100
     4.3 @@ -158,8 +158,8 @@
     4.4    "\<theta> xb = F id <id, \<lambda> a. (snd xb)> (fst xb)"
     4.5  
     4.6  (* The strength laws for \<theta>: *)
     4.7 -lemma \<theta>_natural: "F id (map_pair f g) o \<theta> = \<theta> o map_pair (F id f) g"
     4.8 -  unfolding \<theta>_def F.map_comp comp_def id_apply convol_def map_pair_def split_beta fst_conv snd_conv ..
     4.9 +lemma \<theta>_natural: "F id (map_prod f g) o \<theta> = \<theta> o map_prod (F id f) g"
    4.10 +  unfolding \<theta>_def F.map_comp comp_def id_apply convol_def map_prod_def split_beta fst_conv snd_conv ..
    4.11  
    4.12  definition assl :: "'a * ('b * 'c) \<Rightarrow> ('a * 'b) * 'c" where
    4.13    "assl abc = ((fst abc, fst (snd abc)), snd (snd abc))"
    4.14 @@ -167,8 +167,8 @@
    4.15  lemma \<theta>_rid: "F id fst o \<theta> = fst"
    4.16    unfolding \<theta>_def F.map_comp F.map_id comp_def id_apply convol_def fst_conv sym[OF id_def] ..
    4.17  
    4.18 -lemma \<theta>_assl: "F id assl o \<theta> = \<theta> o map_pair \<theta> id o assl"
    4.19 -  unfolding assl_def \<theta>_def F.map_comp comp_def id_apply convol_def map_pair_def split fst_conv snd_conv ..
    4.20 +lemma \<theta>_assl: "F id assl o \<theta> = \<theta> o map_prod \<theta> id o assl"
    4.21 +  unfolding assl_def \<theta>_def F.map_comp comp_def id_apply convol_def map_prod_def split fst_conv snd_conv ..
    4.22  
    4.23  datatype_new ('a, 'b, 'c) spF\<^sub>\<mu> = GetF "'a \<Rightarrow> ('a, 'b, 'c) spF\<^sub>\<mu>" | PutF "('b,'c) F"
    4.24  codatatype ('a, 'b) spF\<^sub>\<nu> = InF (outF: "('a, 'b, ('a, 'b) spF\<^sub>\<nu>) spF\<^sub>\<mu>")
     5.1 --- a/src/HOL/BNF_FP_Base.thy	Thu Mar 06 13:36:15 2014 +0100
     5.2 +++ b/src/HOL/BNF_FP_Base.thy	Thu Mar 06 13:36:48 2014 +0100
     5.3 @@ -116,11 +116,11 @@
     5.4  lemma convol_o: "<f, g> o h = <f o h, g o h>"
     5.5    unfolding convol_def by auto
     5.6  
     5.7 -lemma map_pair_o_convol: "map_pair h1 h2 o <f, g> = <h1 o f, h2 o g>"
     5.8 +lemma map_prod_o_convol: "map_prod h1 h2 o <f, g> = <h1 o f, h2 o g>"
     5.9    unfolding convol_def by auto
    5.10  
    5.11 -lemma map_pair_o_convol_id: "(map_pair f id \<circ> <id , g>) x = <id \<circ> f , g> x"
    5.12 -  unfolding map_pair_o_convol id_comp comp_id ..
    5.13 +lemma map_prod_o_convol_id: "(map_prod f id \<circ> <id , g>) x = <id \<circ> f , g> x"
    5.14 +  unfolding map_prod_o_convol id_comp comp_id ..
    5.15  
    5.16  lemma o_case_sum: "h o case_sum f g = case_sum (h o f) (h o g)"
    5.17    unfolding comp_def by (auto split: sum.splits)
     6.1 --- a/src/HOL/Bali/State.thy	Thu Mar 06 13:36:15 2014 +0100
     6.2 +++ b/src/HOL/Bali/State.thy	Thu Mar 06 13:36:48 2014 +0100
     6.3 @@ -631,11 +631,11 @@
     6.4  
     6.5  definition
     6.6    abupd :: "(abopt \<Rightarrow> abopt) \<Rightarrow> state \<Rightarrow> state"
     6.7 -  where "abupd f = map_pair f id"
     6.8 +  where "abupd f = map_prod f id"
     6.9  
    6.10  definition
    6.11    supd :: "(st \<Rightarrow> st) \<Rightarrow> state \<Rightarrow> state"
    6.12 -  where "supd = map_pair id"
    6.13 +  where "supd = map_prod id"
    6.14    
    6.15  lemma abupd_def2 [simp]: "abupd f (x,s) = (f x,s)"
    6.16  by (simp add: abupd_def)
     7.1 --- a/src/HOL/Basic_BNFs.thy	Thu Mar 06 13:36:15 2014 +0100
     7.2 +++ b/src/HOL/Basic_BNFs.thy	Thu Mar 06 13:36:48 2014 +0100
     7.3 @@ -129,27 +129,27 @@
     7.4    by (simp add: prod_rel_def)
     7.5  
     7.6  bnf "'a \<times> 'b"
     7.7 -  map: map_pair
     7.8 +  map: map_prod
     7.9    sets: fsts snds
    7.10    bd: natLeq
    7.11    rel: prod_rel
    7.12  proof (unfold prod_set_defs)
    7.13 -  show "map_pair id id = id" by (rule map_pair.id)
    7.14 +  show "map_prod id id = id" by (rule map_prod.id)
    7.15  next
    7.16    fix f1 f2 g1 g2
    7.17 -  show "map_pair (g1 o f1) (g2 o f2) = map_pair g1 g2 o map_pair f1 f2"
    7.18 -    by (rule map_pair.comp[symmetric])
    7.19 +  show "map_prod (g1 o f1) (g2 o f2) = map_prod g1 g2 o map_prod f1 f2"
    7.20 +    by (rule map_prod.comp[symmetric])
    7.21  next
    7.22    fix x f1 f2 g1 g2
    7.23    assume "\<And>z. z \<in> {fst x} \<Longrightarrow> f1 z = g1 z" "\<And>z. z \<in> {snd x} \<Longrightarrow> f2 z = g2 z"
    7.24 -  thus "map_pair f1 f2 x = map_pair g1 g2 x" by (cases x) simp
    7.25 +  thus "map_prod f1 f2 x = map_prod g1 g2 x" by (cases x) simp
    7.26  next
    7.27    fix f1 f2
    7.28 -  show "(\<lambda>x. {fst x}) o map_pair f1 f2 = image f1 o (\<lambda>x. {fst x})"
    7.29 +  show "(\<lambda>x. {fst x}) o map_prod f1 f2 = image f1 o (\<lambda>x. {fst x})"
    7.30      by (rule ext, unfold o_apply) simp
    7.31  next
    7.32    fix f1 f2
    7.33 -  show "(\<lambda>x. {snd x}) o map_pair f1 f2 = image f2 o (\<lambda>x. {snd x})"
    7.34 +  show "(\<lambda>x. {snd x}) o map_prod f1 f2 = image f2 o (\<lambda>x. {snd x})"
    7.35      by (rule ext, unfold o_apply) simp
    7.36  next
    7.37    show "card_order natLeq" by (rule natLeq_card_order)
    7.38 @@ -169,8 +169,8 @@
    7.39  next
    7.40    fix R S
    7.41    show "prod_rel R S =
    7.42 -        (Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_pair fst fst))\<inverse>\<inverse> OO
    7.43 -        Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_pair snd snd)"
    7.44 +        (Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_prod fst fst))\<inverse>\<inverse> OO
    7.45 +        Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_prod snd snd)"
    7.46    unfolding prod_set_defs prod_rel_def Grp_def relcompp.simps conversep.simps fun_eq_iff
    7.47    by auto
    7.48  qed
     8.1 --- a/src/HOL/Cardinals/Ordinal_Arithmetic.thy	Thu Mar 06 13:36:15 2014 +0100
     8.2 +++ b/src/HOL/Cardinals/Ordinal_Arithmetic.thy	Thu Mar 06 13:36:48 2014 +0100
     8.3 @@ -13,7 +13,7 @@
     8.4  
     8.5  definition osum :: "'a rel \<Rightarrow> 'b rel \<Rightarrow> ('a + 'b) rel"  (infixr "+o" 70)
     8.6  where
     8.7 -  "r +o r' = map_pair Inl Inl ` r \<union> map_pair Inr Inr ` r' \<union> 
     8.8 +  "r +o r' = map_prod Inl Inl ` r \<union> map_prod Inr Inr ` r' \<union> 
     8.9       {(Inl a, Inr a') | a a' . a \<in> Field r \<and> a' \<in> Field r'}"
    8.10  
    8.11  lemma Field_osum: "Field(r +o r') = Inl ` Field r \<union> Inr ` Field r'"
    8.12 @@ -100,11 +100,11 @@
    8.13    unfolding osum_def Total_Id_Field[OF r] Total_Id_Field[OF r'] by auto
    8.14  
    8.15  lemma osum_minus_Id1:
    8.16 -  "r \<le> Id \<Longrightarrow> (r +o r') - Id \<le> (Inl ` Field r \<times> Inr ` Field r') \<union> (map_pair Inr Inr ` (r' - Id))"
    8.17 +  "r \<le> Id \<Longrightarrow> (r +o r') - Id \<le> (Inl ` Field r \<times> Inr ` Field r') \<union> (map_prod Inr Inr ` (r' - Id))"
    8.18    unfolding osum_def by auto
    8.19  
    8.20  lemma osum_minus_Id2:
    8.21 -  "r' \<le> Id \<Longrightarrow> (r +o r') - Id \<le> (map_pair Inl Inl ` (r - Id)) \<union> (Inl ` Field r \<times> Inr ` Field r')"
    8.22 +  "r' \<le> Id \<Longrightarrow> (r +o r') - Id \<le> (map_prod Inl Inl ` (r - Id)) \<union> (Inl ` Field r \<times> Inr ` Field r')"
    8.23    unfolding osum_def by auto
    8.24  
    8.25  lemma osum_wf_Id:
    8.26 @@ -122,11 +122,11 @@
    8.27    proof (elim disjE)
    8.28      assume "r \<subseteq> Id"
    8.29      thus "wf ((r +o r') - Id)"
    8.30 -      by (rule wf_subset[rotated, OF osum_minus_Id1 wf_Un[OF 1 wf_map_pair_image[OF WF']]]) auto
    8.31 +      by (rule wf_subset[rotated, OF osum_minus_Id1 wf_Un[OF 1 wf_map_prod_image[OF WF']]]) auto
    8.32    next
    8.33      assume "r' \<subseteq> Id"
    8.34      thus "wf ((r +o r') - Id)"
    8.35 -      by (rule wf_subset[rotated, OF osum_minus_Id2 wf_Un[OF wf_map_pair_image[OF WF] 1]]) auto
    8.36 +      by (rule wf_subset[rotated, OF osum_minus_Id2 wf_Un[OF wf_map_prod_image[OF WF] 1]]) auto
    8.37    qed
    8.38  qed
    8.39  
    8.40 @@ -158,10 +158,10 @@
    8.41    shows "r \<le>o r +o r'"
    8.42    using assms osum_embedL osum_Well_order unfolding ordLeq_def by blast
    8.43  
    8.44 -lemma dir_image_alt: "dir_image r f = map_pair f f ` r"
    8.45 -  unfolding dir_image_def map_pair_def by auto
    8.46 +lemma dir_image_alt: "dir_image r f = map_prod f f ` r"
    8.47 +  unfolding dir_image_def map_prod_def by auto
    8.48  
    8.49 -lemma map_pair_ordIso: "\<lbrakk>Well_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> map_pair f f ` r =o r"
    8.50 +lemma map_prod_ordIso: "\<lbrakk>Well_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> map_prod f f ` r =o r"
    8.51    unfolding dir_image_alt[symmetric] by (rule ordIso_symmetric[OF dir_image_ordIso])
    8.52  
    8.53  definition oprod :: "'a rel \<Rightarrow> 'b rel \<Rightarrow> ('a \<times> 'b) rel"  (infixr "*o" 80)
    8.54 @@ -960,7 +960,7 @@
    8.55      unfolding Field_osum iso_def bij_betw_def image_image image_Un by auto
    8.56    moreover from f have "compat ?L ?R ?f"
    8.57      unfolding osum_def iso_iff3[OF r s] compat_def bij_betw_def 
    8.58 -    by (auto simp: map_pair_imageI)
    8.59 +    by (auto simp: map_prod_imageI)
    8.60    ultimately have "iso ?L ?R ?f" by (subst iso_iff3) (auto intro: osum_Well_order r s t)
    8.61    thus ?thesis unfolding ordIso_def by (auto intro: osum_Well_order r s t)
    8.62  qed
    8.63 @@ -978,7 +978,7 @@
    8.64      unfolding Field_osum iso_def bij_betw_def image_image image_Un by auto
    8.65    moreover from f have "compat ?L ?R ?f"
    8.66      unfolding osum_def iso_iff3[OF r s] compat_def bij_betw_def 
    8.67 -    by (auto simp: map_pair_imageI)
    8.68 +    by (auto simp: map_prod_imageI)
    8.69    ultimately have "iso ?L ?R ?f" by (subst iso_iff3) (auto intro: osum_Well_order r s t)
    8.70    thus ?thesis unfolding ordIso_def by (auto intro: osum_Well_order r s t)
    8.71  qed
    8.72 @@ -1019,14 +1019,14 @@
    8.73  proof -
    8.74    from assms(1) obtain f where r: "Well_order r" and s: "Well_order s" and f: "iso r s f"
    8.75      unfolding ordIso_def by blast
    8.76 -  let ?f = "map_pair f id"
    8.77 +  let ?f = "map_prod f id"
    8.78    from f have "inj_on ?f (Field ?L)"
    8.79      unfolding Field_oprod iso_def bij_betw_def inj_on_def by fastforce
    8.80    with f have "bij_betw ?f (Field ?L) (Field ?R)"
    8.81 -    unfolding Field_oprod iso_def bij_betw_def by (auto intro!: map_pair_surj_on)
    8.82 +    unfolding Field_oprod iso_def bij_betw_def by (auto intro!: map_prod_surj_on)
    8.83    moreover from f have "compat ?L ?R ?f"
    8.84      unfolding iso_iff3[OF r s] compat_def oprod_def bij_betw_def
    8.85 -    by (auto simp: map_pair_imageI)
    8.86 +    by (auto simp: map_prod_imageI)
    8.87    ultimately have "iso ?L ?R ?f" by (subst iso_iff3) (auto intro: oprod_Well_order r s t)
    8.88    thus ?thesis unfolding ordIso_def by (auto intro: oprod_Well_order r s t)
    8.89  qed
    8.90 @@ -1037,14 +1037,14 @@
    8.91  proof -
    8.92    from assms(1) obtain f where r: "Well_order r" and s: "Well_order s" and f: "iso r s f"
    8.93      unfolding ordIso_def by blast
    8.94 -  let ?f = "map_pair id f"
    8.95 +  let ?f = "map_prod id f"
    8.96    from f have "inj_on ?f (Field ?L)"
    8.97      unfolding Field_oprod iso_def bij_betw_def inj_on_def by fastforce
    8.98    with f have "bij_betw ?f (Field ?L) (Field ?R)"
    8.99 -    unfolding Field_oprod iso_def bij_betw_def by (auto intro!: map_pair_surj_on)
   8.100 +    unfolding Field_oprod iso_def bij_betw_def by (auto intro!: map_prod_surj_on)
   8.101    moreover from f well_order_on_domain[OF r] have "compat ?L ?R ?f"
   8.102      unfolding iso_iff3[OF r s] compat_def oprod_def bij_betw_def
   8.103 -    by (auto simp: map_pair_imageI dest: inj_onD)
   8.104 +    by (auto simp: map_prod_imageI dest: inj_onD)
   8.105    ultimately have "iso ?L ?R ?f" by (subst iso_iff3) (auto intro: oprod_Well_order r s t)
   8.106    thus ?thesis unfolding ordIso_def by (auto intro: oprod_Well_order r s t)
   8.107  qed
   8.108 @@ -1095,10 +1095,10 @@
   8.109  begin
   8.110  
   8.111  lemma osum_ozeroL: "ozero +o r =o r"
   8.112 -  using r unfolding osum_def ozero_def by (auto intro: map_pair_ordIso)
   8.113 +  using r unfolding osum_def ozero_def by (auto intro: map_prod_ordIso)
   8.114  
   8.115  lemma osum_ozeroR: "r +o ozero =o r"
   8.116 -  using r unfolding osum_def ozero_def by (auto intro: map_pair_ordIso)
   8.117 +  using r unfolding osum_def ozero_def by (auto intro: map_prod_ordIso)
   8.118  
   8.119  lemma osum_assoc: "(r +o s) +o t =o r +o s +o t" (is "?L =o ?R")
   8.120  proof -
   8.121 @@ -1113,7 +1113,7 @@
   8.122      assume "(a, b) \<in> ?L"
   8.123      thus "(?f a, ?f b) \<in> ?R"
   8.124        unfolding osum_def[of "r +o s" t] osum_def[of r "s +o t"] Field_osum
   8.125 -      unfolding osum_def Field_osum image_iff image_Un map_pair_def
   8.126 +      unfolding osum_def Field_osum image_iff image_Un map_prod_def
   8.127        by fastforce
   8.128    qed
   8.129    ultimately have "iso ?L ?R ?f" using r s t by (subst iso_iff3) (auto intro: osum_Well_order)
   8.130 @@ -1132,7 +1132,7 @@
   8.131    let ?f = "map_sum id f"
   8.132    from *(1) have "inj_on ?f (Field ?L)" unfolding Field_osum inj_on_def by fastforce
   8.133    moreover
   8.134 -  from *(2,4) have "compat ?L ?R ?f" unfolding compat_def osum_def map_pair_def by fastforce
   8.135 +  from *(2,4) have "compat ?L ?R ?f" unfolding compat_def osum_def map_prod_def by fastforce
   8.136    moreover
   8.137    interpret t!: wo_rel t by unfold_locales (rule t)
   8.138    interpret rt!: wo_rel ?R by unfold_locales (rule osum_Well_order[OF r t])
   8.139 @@ -1194,7 +1194,7 @@
   8.140    hence *: "inj_on f (Field s)" "compat s t f" "ofilter t (f ` Field s)" "f ` Field s \<subset> Field t"
   8.141      using embed_iff_compat_inj_on_ofilter[OF s t, of f] embedS_iff[OF s, of t f]
   8.142      unfolding embedS_def by auto
   8.143 -  let ?f = "map_pair id f"
   8.144 +  let ?f = "map_prod id f"
   8.145    from *(1) have "inj_on ?f (Field ?L)" unfolding Field_oprod inj_on_def by fastforce
   8.146    moreover
   8.147    from *(2,4) the_inv_into_f_f[OF *(1)] have "compat ?L ?R ?f" unfolding compat_def oprod_def
   8.148 @@ -1211,7 +1211,7 @@
   8.149    from not_ordLess_ordIso[OF assms(1)] have "r \<noteq> {}" by (metis ozero_def ozero_ordIso)
   8.150    hence "Field r \<noteq> {}" unfolding Field_def by auto
   8.151    with *(4) have "?f ` Field ?L \<subset> Field ?R" unfolding Field_oprod
   8.152 -    by auto (metis SigmaD2 SigmaI map_pair_surj_on)
   8.153 +    by auto (metis SigmaD2 SigmaI map_prod_surj_on)
   8.154    ultimately have "embedS ?L ?R ?f" using embedS_iff[OF oprod_Well_order[OF r s], of ?R ?f] by auto
   8.155    thus ?thesis unfolding ordLess_def by (auto intro: oprod_Well_order r s t)
   8.156  qed
   8.157 @@ -1222,10 +1222,10 @@
   8.158  proof -
   8.159    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)"
   8.160      unfolding ordLeq_def2 by blast
   8.161 -  let ?f = "map_pair f id"
   8.162 +  let ?f = "map_prod f id"
   8.163    from f have "\<forall>a\<in>Field (r *o t).
   8.164       ?f a \<in> Field (s *o t) \<and> ?f ` underS (r *o t) a \<subseteq> underS (s *o t) (?f a)"
   8.165 -     unfolding Field_oprod underS_def unfolding map_pair_def oprod_def by auto
   8.166 +     unfolding Field_oprod underS_def unfolding map_prod_def oprod_def by auto
   8.167    thus ?thesis unfolding ordLeq_def2 by (auto intro: oprod_Well_order r s t)
   8.168  qed
   8.169  
     9.1 --- a/src/HOL/Library/Code_Target_Int.thy	Thu Mar 06 13:36:15 2014 +0100
     9.2 +++ b/src/HOL/Library/Code_Target_Int.thy	Thu Mar 06 13:36:48 2014 +0100
     9.3 @@ -67,7 +67,7 @@
     9.4    by simp
     9.5  
     9.6  lemma [code]:
     9.7 -  "Divides.divmod_abs k l = map_pair int_of_integer int_of_integer
     9.8 +  "Divides.divmod_abs k l = map_prod int_of_integer int_of_integer
     9.9      (Code_Numeral.divmod_abs (of_int k) (of_int l))"
    9.10    by (simp add: prod_eq_iff)
    9.11  
    10.1 --- a/src/HOL/Library/Quotient_Product.thy	Thu Mar 06 13:36:15 2014 +0100
    10.2 +++ b/src/HOL/Library/Quotient_Product.thy	Thu Mar 06 13:36:48 2014 +0100
    10.3 @@ -10,8 +10,8 @@
    10.4  
    10.5  subsection {* Rules for the Quotient package *}
    10.6  
    10.7 -lemma map_pair_id [id_simps]:
    10.8 -  shows "map_pair id id = id"
    10.9 +lemma map_prod_id [id_simps]:
   10.10 +  shows "map_prod id id = id"
   10.11    by (simp add: fun_eq_iff)
   10.12  
   10.13  lemma prod_rel_eq [id_simps]:
   10.14 @@ -27,9 +27,9 @@
   10.15  lemma prod_quotient [quot_thm]:
   10.16    assumes "Quotient3 R1 Abs1 Rep1"
   10.17    assumes "Quotient3 R2 Abs2 Rep2"
   10.18 -  shows "Quotient3 (prod_rel R1 R2) (map_pair Abs1 Abs2) (map_pair Rep1 Rep2)"
   10.19 +  shows "Quotient3 (prod_rel R1 R2) (map_prod Abs1 Abs2) (map_prod Rep1 Rep2)"
   10.20    apply (rule Quotient3I)
   10.21 -  apply (simp add: map_pair.compositionality comp_def map_pair.identity
   10.22 +  apply (simp add: map_prod.compositionality comp_def map_prod.identity
   10.23       Quotient3_abs_rep [OF assms(1)] Quotient3_abs_rep [OF assms(2)])
   10.24    apply (simp add: split_paired_all Quotient3_rel_rep [OF assms(1)] Quotient3_rel_rep [OF assms(2)])
   10.25    using Quotient3_rel [OF assms(1)] Quotient3_rel [OF assms(2)]
   10.26 @@ -47,7 +47,7 @@
   10.27  lemma Pair_prs [quot_preserve]:
   10.28    assumes q1: "Quotient3 R1 Abs1 Rep1"
   10.29    assumes q2: "Quotient3 R2 Abs2 Rep2"
   10.30 -  shows "(Rep1 ---> Rep2 ---> (map_pair Abs1 Abs2)) Pair = Pair"
   10.31 +  shows "(Rep1 ---> Rep2 ---> (map_prod Abs1 Abs2)) Pair = Pair"
   10.32    apply(simp add: fun_eq_iff)
   10.33    apply(simp add: Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2])
   10.34    done
   10.35 @@ -61,7 +61,7 @@
   10.36  lemma fst_prs [quot_preserve]:
   10.37    assumes q1: "Quotient3 R1 Abs1 Rep1"
   10.38    assumes q2: "Quotient3 R2 Abs2 Rep2"
   10.39 -  shows "(map_pair Rep1 Rep2 ---> Abs1) fst = fst"
   10.40 +  shows "(map_prod Rep1 Rep2 ---> Abs1) fst = fst"
   10.41    by (simp add: fun_eq_iff Quotient3_abs_rep[OF q1])
   10.42  
   10.43  lemma snd_rsp [quot_respect]:
   10.44 @@ -73,7 +73,7 @@
   10.45  lemma snd_prs [quot_preserve]:
   10.46    assumes q1: "Quotient3 R1 Abs1 Rep1"
   10.47    assumes q2: "Quotient3 R2 Abs2 Rep2"
   10.48 -  shows "(map_pair Rep1 Rep2 ---> Abs2) snd = snd"
   10.49 +  shows "(map_prod Rep1 Rep2 ---> Abs2) snd = snd"
   10.50    by (simp add: fun_eq_iff Quotient3_abs_rep[OF q2])
   10.51  
   10.52  lemma split_rsp [quot_respect]:
   10.53 @@ -83,7 +83,7 @@
   10.54  lemma split_prs [quot_preserve]:
   10.55    assumes q1: "Quotient3 R1 Abs1 Rep1"
   10.56    and     q2: "Quotient3 R2 Abs2 Rep2"
   10.57 -  shows "(((Abs1 ---> Abs2 ---> id) ---> map_pair Rep1 Rep2 ---> id) split) = split"
   10.58 +  shows "(((Abs1 ---> Abs2 ---> id) ---> map_prod Rep1 Rep2 ---> id) split) = split"
   10.59    by (simp add: fun_eq_iff Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2])
   10.60  
   10.61  lemma [quot_respect]:
   10.62 @@ -95,7 +95,7 @@
   10.63    assumes q1: "Quotient3 R1 abs1 rep1"
   10.64    and     q2: "Quotient3 R2 abs2 rep2"
   10.65    shows "((abs1 ---> abs1 ---> id) ---> (abs2 ---> abs2 ---> id) --->
   10.66 -  map_pair rep1 rep2 ---> map_pair rep1 rep2 ---> id) prod_rel = prod_rel"
   10.67 +  map_prod rep1 rep2 ---> map_prod rep1 rep2 ---> id) prod_rel = prod_rel"
   10.68    by (simp add: fun_eq_iff Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2])
   10.69  
   10.70  lemma [quot_preserve]:
    11.1 --- a/src/HOL/Lifting_Product.thy	Thu Mar 06 13:36:15 2014 +0100
    11.2 +++ b/src/HOL/Lifting_Product.thy	Thu Mar 06 13:36:48 2014 +0100
    11.3 @@ -70,8 +70,7 @@
    11.4  lemma Quotient_prod[quot_map]:
    11.5    assumes "Quotient R1 Abs1 Rep1 T1"
    11.6    assumes "Quotient R2 Abs2 Rep2 T2"
    11.7 -  shows "Quotient (prod_rel R1 R2) (map_pair Abs1 Abs2)
    11.8 -    (map_pair Rep1 Rep2) (prod_rel T1 T2)"
    11.9 +  shows "Quotient (prod_rel R1 R2) (map_prod Abs1 Abs2) (map_prod Rep1 Rep2) (prod_rel T1 T2)"
   11.10    using assms unfolding Quotient_alt_def by auto
   11.11  
   11.12  subsection {* Transfer rules for the Transfer package *}
   11.13 @@ -97,10 +96,10 @@
   11.14    "((prod_rel A B ===> C) ===> A ===> B ===> C) curry curry"
   11.15    unfolding curry_def by transfer_prover
   11.16  
   11.17 -lemma map_pair_transfer [transfer_rule]:
   11.18 +lemma map_prod_transfer [transfer_rule]:
   11.19    "((A ===> C) ===> (B ===> D) ===> prod_rel A B ===> prod_rel C D)
   11.20 -    map_pair map_pair"
   11.21 -  unfolding map_pair_def [abs_def] by transfer_prover
   11.22 +    map_prod map_prod"
   11.23 +  unfolding map_prod_def [abs_def] by transfer_prover
   11.24  
   11.25  lemma prod_rel_transfer [transfer_rule]:
   11.26    "((A ===> B ===> op =) ===> (C ===> D ===> op =) ===>
    12.1 --- a/src/HOL/List.thy	Thu Mar 06 13:36:15 2014 +0100
    12.2 +++ b/src/HOL/List.thy	Thu Mar 06 13:36:48 2014 +0100
    12.3 @@ -5251,7 +5251,7 @@
    12.4    lexn :: "('a \<times> 'a) set \<Rightarrow> nat \<Rightarrow> ('a list \<times> 'a list) set" where
    12.5  "lexn r 0 = {}" |
    12.6  "lexn r (Suc n) =
    12.7 -  (map_pair (%(x, xs). x#xs) (%(x, xs). x#xs) ` (r <*lex*> lexn r n)) Int
    12.8 +  (map_prod (%(x, xs). x#xs) (%(x, xs). x#xs) ` (r <*lex*> lexn r n)) Int
    12.9    {(xs, ys). length xs = Suc n \<and> length ys = Suc n}"
   12.10  
   12.11  definition lex :: "('a \<times> 'a) set \<Rightarrow> ('a list \<times> 'a list) set" where
   12.12 @@ -5265,7 +5265,7 @@
   12.13  apply (induct n, simp, simp)
   12.14  apply(rule wf_subset)
   12.15   prefer 2 apply (rule Int_lower1)
   12.16 -apply(rule wf_map_pair_image)
   12.17 +apply(rule wf_map_prod_image)
   12.18   prefer 2 apply (rule inj_onI, auto)
   12.19  done
   12.20  
    13.1 --- a/src/HOL/Matrix_LP/ComputeNumeral.thy	Thu Mar 06 13:36:15 2014 +0100
    13.2 +++ b/src/HOL/Matrix_LP/ComputeNumeral.thy	Thu Mar 06 13:36:48 2014 +0100
    13.3 @@ -58,7 +58,7 @@
    13.4                    else apsnd uminus (posDivAlg (-a) (-b)))"
    13.5    by (auto simp only: divmod_int_def)
    13.6  
    13.7 -lemmas compute_div_mod = div_int_def mod_int_def divmod adjust apsnd_def map_pair_def posDivAlg.simps negDivAlg.simps
    13.8 +lemmas compute_div_mod = div_int_def mod_int_def divmod adjust apsnd_def map_prod_def posDivAlg.simps negDivAlg.simps
    13.9  
   13.10  
   13.11  
    14.1 --- a/src/HOL/Metis_Examples/Abstraction.thy	Thu Mar 06 13:36:15 2014 +0100
    14.2 +++ b/src/HOL/Metis_Examples/Abstraction.thy	Thu Mar 06 13:36:48 2014 +0100
    14.3 @@ -160,7 +160,7 @@
    14.4  by (metis (lifting) imageE)
    14.5  
    14.6  lemma image_TimesA: "(\<lambda>(x, y). (f x, g y)) ` (A \<times> B) = (f ` A) \<times> (g ` B)"
    14.7 -by (metis map_pair_def map_pair_surj_on)
    14.8 +by (metis map_prod_def map_prod_surj_on)
    14.9  
   14.10  lemma image_TimesB:
   14.11      "(\<lambda>(x, y, z). (f x, g y, h z)) ` (A \<times> B \<times> C) = (f ` A) \<times> (g ` B) \<times> (h ` C)"
    15.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Thu Mar 06 13:36:15 2014 +0100
    15.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Thu Mar 06 13:36:48 2014 +0100
    15.3 @@ -1564,8 +1564,8 @@
    15.4  text {* Case expressions *}
    15.5  
    15.6  definition
    15.7 -  "map_pairs xs ys = (map (%((a, b), c). (a, b, c)) xs = ys)"
    15.8 +  "map_prods xs ys = (map (%((a, b), c). (a, b, c)) xs = ys)"
    15.9  
   15.10 -code_pred [inductify] map_pairs .
   15.11 +code_pred [inductify] map_prods .
   15.12  
   15.13  end
    16.1 --- a/src/HOL/Product_Type.thy	Thu Mar 06 13:36:15 2014 +0100
    16.2 +++ b/src/HOL/Product_Type.thy	Thu Mar 06 13:36:48 2014 +0100
    16.3 @@ -820,50 +820,50 @@
    16.4  no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
    16.5  
    16.6  text {*
    16.7 -  @{term map_pair} --- action of the product functor upon
    16.8 +  @{term map_prod} --- action of the product functor upon
    16.9    functions.
   16.10  *}
   16.11  
   16.12 -definition map_pair :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'd" where
   16.13 -  "map_pair f g = (\<lambda>(x, y). (f x, g y))"
   16.14 +definition map_prod :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'd" where
   16.15 +  "map_prod f g = (\<lambda>(x, y). (f x, g y))"
   16.16  
   16.17 -lemma map_pair_simp [simp, code]:
   16.18 -  "map_pair f g (a, b) = (f a, g b)"
   16.19 -  by (simp add: map_pair_def)
   16.20 +lemma map_prod_simp [simp, code]:
   16.21 +  "map_prod f g (a, b) = (f a, g b)"
   16.22 +  by (simp add: map_prod_def)
   16.23  
   16.24 -functor map_pair: map_pair
   16.25 +functor map_prod: map_prod
   16.26    by (auto simp add: split_paired_all)
   16.27  
   16.28 -lemma fst_map_pair [simp]:
   16.29 -  "fst (map_pair f g x) = f (fst x)"
   16.30 +lemma fst_map_prod [simp]:
   16.31 +  "fst (map_prod f g x) = f (fst x)"
   16.32    by (cases x) simp_all
   16.33  
   16.34  lemma snd_prod_fun [simp]:
   16.35 -  "snd (map_pair f g x) = g (snd x)"
   16.36 +  "snd (map_prod f g x) = g (snd x)"
   16.37    by (cases x) simp_all
   16.38  
   16.39 -lemma fst_comp_map_pair [simp]:
   16.40 -  "fst \<circ> map_pair f g = f \<circ> fst"
   16.41 +lemma fst_comp_map_prod [simp]:
   16.42 +  "fst \<circ> map_prod f g = f \<circ> fst"
   16.43    by (rule ext) simp_all
   16.44  
   16.45 -lemma snd_comp_map_pair [simp]:
   16.46 -  "snd \<circ> map_pair f g = g \<circ> snd"
   16.47 +lemma snd_comp_map_prod [simp]:
   16.48 +  "snd \<circ> map_prod f g = g \<circ> snd"
   16.49    by (rule ext) simp_all
   16.50  
   16.51 -lemma map_pair_compose:
   16.52 -  "map_pair (f1 o f2) (g1 o g2) = (map_pair f1 g1 o map_pair f2 g2)"
   16.53 -  by (rule ext) (simp add: map_pair.compositionality comp_def)
   16.54 +lemma map_prod_compose:
   16.55 +  "map_prod (f1 o f2) (g1 o g2) = (map_prod f1 g1 o map_prod f2 g2)"
   16.56 +  by (rule ext) (simp add: map_prod.compositionality comp_def)
   16.57  
   16.58 -lemma map_pair_ident [simp]:
   16.59 -  "map_pair (%x. x) (%y. y) = (%z. z)"
   16.60 -  by (rule ext) (simp add: map_pair.identity)
   16.61 +lemma map_prod_ident [simp]:
   16.62 +  "map_prod (%x. x) (%y. y) = (%z. z)"
   16.63 +  by (rule ext) (simp add: map_prod.identity)
   16.64  
   16.65 -lemma map_pair_imageI [intro]:
   16.66 -  "(a, b) \<in> R \<Longrightarrow> (f a, g b) \<in> map_pair f g ` R"
   16.67 +lemma map_prod_imageI [intro]:
   16.68 +  "(a, b) \<in> R \<Longrightarrow> (f a, g b) \<in> map_prod f g ` R"
   16.69    by (rule image_eqI) simp_all
   16.70  
   16.71  lemma prod_fun_imageE [elim!]:
   16.72 -  assumes major: "c \<in> map_pair f g ` R"
   16.73 +  assumes major: "c \<in> map_prod f g ` R"
   16.74      and cases: "\<And>x y. c = (f x, g y) \<Longrightarrow> (x, y) \<in> R \<Longrightarrow> P"
   16.75    shows P
   16.76    apply (rule major [THEN imageE])
   16.77 @@ -873,10 +873,10 @@
   16.78    done
   16.79  
   16.80  definition apfst :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'b" where
   16.81 -  "apfst f = map_pair f id"
   16.82 +  "apfst f = map_prod f id"
   16.83  
   16.84  definition apsnd :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'c" where
   16.85 -  "apsnd f = map_pair id f"
   16.86 +  "apsnd f = map_prod id f"
   16.87  
   16.88  lemma apfst_conv [simp, code]:
   16.89    "apfst f (x, y) = (f x, y)" 
   16.90 @@ -1144,54 +1144,54 @@
   16.91    "x \<in> Product_Type.product A B \<longleftrightarrow> x \<in> A \<times> B"
   16.92    by (simp add: product_def)
   16.93  
   16.94 -text {* The following @{const map_pair} lemmas are due to Joachim Breitner: *}
   16.95 +text {* The following @{const map_prod} lemmas are due to Joachim Breitner: *}
   16.96  
   16.97 -lemma map_pair_inj_on:
   16.98 +lemma map_prod_inj_on:
   16.99    assumes "inj_on f A" and "inj_on g B"
  16.100 -  shows "inj_on (map_pair f g) (A \<times> B)"
  16.101 +  shows "inj_on (map_prod f g) (A \<times> B)"
  16.102  proof (rule inj_onI)
  16.103    fix x :: "'a \<times> 'c" and y :: "'a \<times> 'c"
  16.104    assume "x \<in> A \<times> B" hence "fst x \<in> A" and "snd x \<in> B" by auto
  16.105    assume "y \<in> A \<times> B" hence "fst y \<in> A" and "snd y \<in> B" by auto
  16.106 -  assume "map_pair f g x = map_pair f g y"
  16.107 -  hence "fst (map_pair f g x) = fst (map_pair f g y)" by (auto)
  16.108 +  assume "map_prod f g x = map_prod f g y"
  16.109 +  hence "fst (map_prod f g x) = fst (map_prod f g y)" by (auto)
  16.110    hence "f (fst x) = f (fst y)" by (cases x,cases y,auto)
  16.111    with `inj_on f A` and `fst x \<in> A` and `fst y \<in> A`
  16.112    have "fst x = fst y" by (auto dest:dest:inj_onD)
  16.113 -  moreover from `map_pair f g x = map_pair f g y`
  16.114 -  have "snd (map_pair f g x) = snd (map_pair f g y)" by (auto)
  16.115 +  moreover from `map_prod f g x = map_prod f g y`
  16.116 +  have "snd (map_prod f g x) = snd (map_prod f g y)" by (auto)
  16.117    hence "g (snd x) = g (snd y)" by (cases x,cases y,auto)
  16.118    with `inj_on g B` and `snd x \<in> B` and `snd y \<in> B`
  16.119    have "snd x = snd y" by (auto dest:dest:inj_onD)
  16.120    ultimately show "x = y" by(rule prod_eqI)
  16.121  qed
  16.122  
  16.123 -lemma map_pair_surj:
  16.124 +lemma map_prod_surj:
  16.125    fixes f :: "'a \<Rightarrow> 'b" and g :: "'c \<Rightarrow> 'd"
  16.126    assumes "surj f" and "surj g"
  16.127 -  shows "surj (map_pair f g)"
  16.128 +  shows "surj (map_prod f g)"
  16.129  unfolding surj_def
  16.130  proof
  16.131    fix y :: "'b \<times> 'd"
  16.132    from `surj f` obtain a where "fst y = f a" by (auto elim:surjE)
  16.133    moreover
  16.134    from `surj g` obtain b where "snd y = g b" by (auto elim:surjE)
  16.135 -  ultimately have "(fst y, snd y) = map_pair f g (a,b)" by auto
  16.136 -  thus "\<exists>x. y = map_pair f g x" by auto
  16.137 +  ultimately have "(fst y, snd y) = map_prod f g (a,b)" by auto
  16.138 +  thus "\<exists>x. y = map_prod f g x" by auto
  16.139  qed
  16.140  
  16.141 -lemma map_pair_surj_on:
  16.142 +lemma map_prod_surj_on:
  16.143    assumes "f ` A = A'" and "g ` B = B'"
  16.144 -  shows "map_pair f g ` (A \<times> B) = A' \<times> B'"
  16.145 +  shows "map_prod f g ` (A \<times> B) = A' \<times> B'"
  16.146  unfolding image_def
  16.147  proof(rule set_eqI,rule iffI)
  16.148    fix x :: "'a \<times> 'c"
  16.149 -  assume "x \<in> {y\<Colon>'a \<times> 'c. \<exists>x\<Colon>'b \<times> 'd\<in>A \<times> B. y = map_pair f g x}"
  16.150 -  then obtain y where "y \<in> A \<times> B" and "x = map_pair f g y" by blast
  16.151 +  assume "x \<in> {y\<Colon>'a \<times> 'c. \<exists>x\<Colon>'b \<times> 'd\<in>A \<times> B. y = map_prod f g x}"
  16.152 +  then obtain y where "y \<in> A \<times> B" and "x = map_prod f g y" by blast
  16.153    from `image f A = A'` and `y \<in> A \<times> B` have "f (fst y) \<in> A'" by auto
  16.154    moreover from `image g B = B'` and `y \<in> A \<times> B` have "g (snd y) \<in> B'" by auto
  16.155    ultimately have "(f (fst y), g (snd y)) \<in> (A' \<times> B')" by auto
  16.156 -  with `x = map_pair f g y` show "x \<in> A' \<times> B'" by (cases y, auto)
  16.157 +  with `x = map_prod f g y` show "x \<in> A' \<times> B'" by (cases y, auto)
  16.158  next
  16.159    fix x :: "'a \<times> 'c"
  16.160    assume "x \<in> A' \<times> B'" hence "fst x \<in> A'" and "snd x \<in> B'" by auto
  16.161 @@ -1199,10 +1199,10 @@
  16.162    then obtain a where "a \<in> A" and "fst x = f a" by (rule imageE)
  16.163    moreover from `image g B = B'` and `snd x \<in> B'`
  16.164    obtain b where "b \<in> B" and "snd x = g b" by auto
  16.165 -  ultimately have "(fst x, snd x) = map_pair f g (a,b)" by auto
  16.166 +  ultimately have "(fst x, snd x) = map_prod f g (a,b)" by auto
  16.167    moreover from `a \<in> A` and  `b \<in> B` have "(a , b) \<in> A \<times> B" by auto
  16.168 -  ultimately have "\<exists>y \<in> A \<times> B. x = map_pair f g y" by auto
  16.169 -  thus "x \<in> {x. \<exists>y \<in> A \<times> B. x = map_pair f g y}" by auto
  16.170 +  ultimately have "\<exists>y \<in> A \<times> B. x = map_prod f g y" by auto
  16.171 +  thus "x \<in> {x. \<exists>y \<in> A \<times> B. x = map_prod f g y}" by auto
  16.172  qed
  16.173  
  16.174  
    17.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Thu Mar 06 13:36:15 2014 +0100
    17.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Thu Mar 06 13:36:48 2014 +0100
    17.3 @@ -37,10 +37,10 @@
    17.4  val basic_simp_thms = @{thms simp_thms(7,8,12,14,22,24)};
    17.5  val more_simp_thms = basic_simp_thms @ @{thms simp_thms(11,15,16,21)};
    17.6  
    17.7 -val sum_prod_thms_map = @{thms id_apply map_pair_simp prod.case sum.case map_sum.simps};
    17.8 +val sum_prod_thms_map = @{thms id_apply map_prod_simp prod.case sum.case map_sum.simps};
    17.9  val sum_prod_thms_set =
   17.10    @{thms UN_empty UN_insert Un_empty_left Un_empty_right Un_iff UN_simps(10) UN_iff
   17.11 -      Union_Un_distrib image_iff o_apply map_pair_simp
   17.12 +      Union_Un_distrib image_iff o_apply map_prod_simp
   17.13        mem_Collect_eq prod_set_simps map_sum.simps sum_set_simps};
   17.14  val sum_prod_thms_rel = @{thms prod_rel_apply sum_rel_simps id_apply};
   17.15  
    18.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Thu Mar 06 13:36:15 2014 +0100
    18.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Thu Mar 06 13:36:48 2014 +0100
    18.3 @@ -34,7 +34,7 @@
    18.4      val ((fAT, fBT), fT) = `dest_funT (fastype_of f);
    18.5      val ((gAT, gBT), gT) = `dest_funT (fastype_of g);
    18.6    in
    18.7 -    Const (@{const_name map_pair},
    18.8 +    Const (@{const_name map_prod},
    18.9        fT --> gT --> HOLogic.mk_prodT (fAT, gAT) --> HOLogic.mk_prodT (fBT, gBT)) $ f $ g
   18.10    end;
   18.11  
   18.12 @@ -404,10 +404,10 @@
   18.13          val fp_xtor_co_recs = map (mk_pointfree lthy) (of_fp_res #xtor_co_rec_thms);
   18.14  
   18.15          val fold_thms = fp_case fp @{thm comp_assoc} @{thm comp_assoc[symmetric]} ::
   18.16 -          map (fn thm => thm RS rewrite_comp_comp) @{thms map_pair.comp map_sum.comp} @
   18.17 -          @{thms id_apply comp_id id_comp map_pair.comp map_pair.id map_sum.comp map_sum.id};
   18.18 +          map (fn thm => thm RS rewrite_comp_comp) @{thms map_prod.comp map_sum.comp} @
   18.19 +          @{thms id_apply comp_id id_comp map_prod.comp map_prod.id map_sum.comp map_sum.id};
   18.20          val rec_thms = fold_thms @ fp_case fp
   18.21 -          @{thms fst_convol map_pair_o_convol convol_o}
   18.22 +          @{thms fst_convol map_prod_o_convol convol_o}
   18.23            @{thms case_sum_o_inj(1) case_sum_o_map_sum o_case_sum};
   18.24  
   18.25          val eq_thm_prop_untyped = Term.aconv_untyped o pairself Thm.full_prop_of;
    19.1 --- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Thu Mar 06 13:36:15 2014 +0100
    19.2 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Thu Mar 06 13:36:48 2014 +0100
    19.3 @@ -527,7 +527,7 @@
    19.4        else refl);
    19.5      val map_cong_passive_args2 = replicate m (fp_case fp @{thm comp_id} @{thm id_comp} RS fun_cong);
    19.6      val map_cong_active_args2 = replicate n (if is_rec
    19.7 -      then fp_case fp @{thm map_pair_o_convol_id} @{thm case_sum_o_map_sum_id}
    19.8 +      then fp_case fp @{thm map_prod_o_convol_id} @{thm case_sum_o_map_sum_id}
    19.9        else fp_case fp @{thm id_comp} @{thm comp_id} RS fun_cong);
   19.10      fun mk_map_congs passive active = map (fn thm => thm OF (passive @ active) RS ext) map_cong0s;
   19.11      val map_cong1s = mk_map_congs map_cong_passive_args1 map_cong_active_args1;
    20.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Mar 06 13:36:15 2014 +0100
    20.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Mar 06 13:36:48 2014 +0100
    20.3 @@ -366,7 +366,7 @@
    20.4            val (ft', fT') = eval_function fT
    20.5            val (st', sT') = eval_function sT
    20.6            val T' = Type (@{type_name prod}, [fT', sT'])
    20.7 -          val map_const = Const (@{const_name map_pair}, (fT' --> fT) --> (sT' --> sT) --> T' --> T)
    20.8 +          val map_const = Const (@{const_name map_prod}, (fT' --> fT) --> (sT' --> sT) --> T' --> T)
    20.9            fun apply_dummy T t = absdummy T (t (Bound 0))
   20.10          in
   20.11            (fn t => list_comb (map_const, [apply_dummy fT' ft', apply_dummy sT' st', t]), T')
    21.1 --- a/src/HOL/Wellfounded.thy	Thu Mar 06 13:36:15 2014 +0100
    21.2 +++ b/src/HOL/Wellfounded.thy	Thu Mar 06 13:36:48 2014 +0100
    21.3 @@ -240,7 +240,7 @@
    21.4  
    21.5  text{*Well-foundedness of image*}
    21.6  
    21.7 -lemma wf_map_pair_image: "[| wf r; inj f |] ==> wf(map_pair f f ` r)"
    21.8 +lemma wf_map_prod_image: "[| wf r; inj f |] ==> wf (map_prod f f ` r)"
    21.9  apply (simp only: wf_eq_minimal, clarify)
   21.10  apply (case_tac "EX p. f p : Q")
   21.11  apply (erule_tac x = "{p. f p : Q}" in allE)
    22.1 --- a/src/HOL/ex/Coercion_Examples.thy	Thu Mar 06 13:36:15 2014 +0100
    22.2 +++ b/src/HOL/ex/Coercion_Examples.thy	Thu Mar 06 13:36:48 2014 +0100
    22.3 @@ -52,10 +52,10 @@
    22.4  
    22.5  declare [[coercion_map "\<lambda> f g h . g o h o f"]]
    22.6  
    22.7 -primrec map_pair :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a * 'b) \<Rightarrow> ('c * 'd)" where
    22.8 - "map_pair f g (x,y) = (f x, g y)"
    22.9 +primrec map_prod :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a * 'b) \<Rightarrow> ('c * 'd)" where
   22.10 + "map_prod f g (x,y) = (f x, g y)"
   22.11  
   22.12 -declare [[coercion_map map_pair]]
   22.13 +declare [[coercion_map map_prod]]
   22.14  
   22.15  (* Examples taken from the haskell draft implementation *)
   22.16