# HG changeset patch # User blanchet # Date 1394109408 -3600 # Node ID 68c5104d2204c1ab99f3a9373c1a89c4e25eb65f # Parent 62156e694f3d27775968357a564057b6f136386f renamed 'map_pair' to 'map_prod' diff -r 62156e694f3d -r 68c5104d2204 src/HOL/BNF_Examples/Lambda_Term.thy --- a/src/HOL/BNF_Examples/Lambda_Term.thy Thu Mar 06 13:36:15 2014 +0100 +++ b/src/HOL/BNF_Examples/Lambda_Term.thy Thu Mar 06 13:36:48 2014 +0100 @@ -27,19 +27,19 @@ "varsOf (Var a) = {a}" | "varsOf (App f x) = varsOf f \ varsOf x" | "varsOf (Lam x b) = {x} \ varsOf b" -| "varsOf (Lt F t) = varsOf t \ (\ { {x} \ X | x X. (x,X) |\| fimage (map_pair id varsOf) F})" +| "varsOf (Lt F t) = varsOf t \ (\ { {x} \ X | x X. (x,X) |\| fimage (map_prod id varsOf) F})" primrec fvarsOf :: "'a trm \ 'a set" where "fvarsOf (Var x) = {x}" | "fvarsOf (App t1 t2) = fvarsOf t1 \ fvarsOf t2" | "fvarsOf (Lam x t) = fvarsOf t - {x}" -| "fvarsOf (Lt xts t) = fvarsOf t - {x | x X. (x,X) |\| fimage (map_pair id varsOf) xts} \ - (\ {X | x X. (x,X) |\| fimage (map_pair id varsOf) xts})" +| "fvarsOf (Lt xts t) = fvarsOf t - {x | x X. (x,X) |\| fimage (map_prod id varsOf) xts} \ + (\ {X | x X. (x,X) |\| fimage (map_prod id varsOf) xts})" lemma diff_Un_incl_triv: "\A \ D; C \ E\ \ A - B \ C \ D \ E" by blast -lemma in_fimage_map_pair_fset_iff[simp]: - "(x, y) |\| fimage (map_pair f g) xts \ (\ t1 t2. (t1, t2) |\| xts \ x = f t1 \ y = g t2)" +lemma in_fimage_map_prod_fset_iff[simp]: + "(x, y) |\| fimage (map_prod f g) xts \ (\ t1 t2. (t1, t2) |\| xts \ x = f t1 \ y = g t2)" by force lemma fvarsOf_varsOf: "fvarsOf t \ varsOf t" diff -r 62156e694f3d -r 68c5104d2204 src/HOL/BNF_Examples/Misc_Primcorec.thy --- a/src/HOL/BNF_Examples/Misc_Primcorec.thy Thu Mar 06 13:36:15 2014 +0100 +++ b/src/HOL/BNF_Examples/Misc_Primcorec.thy Thu Mar 06 13:36:48 2014 +0100 @@ -45,7 +45,7 @@ Var s \ Var (f s) | App l l' \ App (rename_lam f l) (rename_lam f l') | Abs s l \ Abs (f s) (rename_lam f l) - | Let SL l \ Let (fimage (map_pair f (rename_lam f)) SL) (rename_lam f l))" + | Let SL l \ Let (fimage (map_prod f (rename_lam f)) SL) (rename_lam f l))" primcorec j1_sum :: "('a\{zero,one,plus}) \ 'a J1" and diff -r 62156e694f3d -r 68c5104d2204 src/HOL/BNF_Examples/Misc_Primrec.thy --- a/src/HOL/BNF_Examples/Misc_Primrec.thy Thu Mar 06 13:36:15 2014 +0100 +++ b/src/HOL/BNF_Examples/Misc_Primrec.thy Thu Mar 06 13:36:48 2014 +0100 @@ -51,7 +51,7 @@ "rename_lam f (Var s) = Var (f s)" | "rename_lam f (App l l') = App (rename_lam f l) (rename_lam f l')" | "rename_lam f (Abs s l) = Abs (f s) (rename_lam f l)" | - "rename_lam f (Let SL l) = Let (fimage (map_pair f (rename_lam f)) SL) (rename_lam f l)" + "rename_lam f (Let SL l) = Let (fimage (map_prod f (rename_lam f)) SL) (rename_lam f l)" primrec sum_i1 :: "('a\{zero,plus}) I1 \ 'a" and diff -r 62156e694f3d -r 68c5104d2204 src/HOL/BNF_Examples/Stream_Processor.thy --- a/src/HOL/BNF_Examples/Stream_Processor.thy Thu Mar 06 13:36:15 2014 +0100 +++ b/src/HOL/BNF_Examples/Stream_Processor.thy Thu Mar 06 13:36:48 2014 +0100 @@ -158,8 +158,8 @@ "\ xb = F id a. (snd xb)> (fst xb)" (* The strength laws for \: *) -lemma \_natural: "F id (map_pair f g) o \ = \ o map_pair (F id f) g" - unfolding \_def F.map_comp comp_def id_apply convol_def map_pair_def split_beta fst_conv snd_conv .. +lemma \_natural: "F id (map_prod f g) o \ = \ o map_prod (F id f) g" + unfolding \_def F.map_comp comp_def id_apply convol_def map_prod_def split_beta fst_conv snd_conv .. definition assl :: "'a * ('b * 'c) \ ('a * 'b) * 'c" where "assl abc = ((fst abc, fst (snd abc)), snd (snd abc))" @@ -167,8 +167,8 @@ lemma \_rid: "F id fst o \ = fst" unfolding \_def F.map_comp F.map_id comp_def id_apply convol_def fst_conv sym[OF id_def] .. -lemma \_assl: "F id assl o \ = \ o map_pair \ id o assl" - unfolding assl_def \_def F.map_comp comp_def id_apply convol_def map_pair_def split fst_conv snd_conv .. +lemma \_assl: "F id assl o \ = \ o map_prod \ id o assl" + unfolding assl_def \_def F.map_comp comp_def id_apply convol_def map_prod_def split fst_conv snd_conv .. datatype_new ('a, 'b, 'c) spF\<^sub>\ = GetF "'a \ ('a, 'b, 'c) spF\<^sub>\" | PutF "('b,'c) F" codatatype ('a, 'b) spF\<^sub>\ = InF (outF: "('a, 'b, ('a, 'b) spF\<^sub>\) spF\<^sub>\") diff -r 62156e694f3d -r 68c5104d2204 src/HOL/BNF_FP_Base.thy --- a/src/HOL/BNF_FP_Base.thy Thu Mar 06 13:36:15 2014 +0100 +++ b/src/HOL/BNF_FP_Base.thy Thu Mar 06 13:36:48 2014 +0100 @@ -116,11 +116,11 @@ lemma convol_o: " o h = " unfolding convol_def by auto -lemma map_pair_o_convol: "map_pair h1 h2 o =

" +lemma map_prod_o_convol: "map_prod h1 h2 o =

" unfolding convol_def by auto -lemma map_pair_o_convol_id: "(map_pair f id \ ) x = f , g> x" - unfolding map_pair_o_convol id_comp comp_id .. +lemma map_prod_o_convol_id: "(map_prod f id \ ) x = f , g> x" + unfolding map_prod_o_convol id_comp comp_id .. 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) diff -r 62156e694f3d -r 68c5104d2204 src/HOL/Bali/State.thy --- a/src/HOL/Bali/State.thy Thu Mar 06 13:36:15 2014 +0100 +++ b/src/HOL/Bali/State.thy Thu Mar 06 13:36:48 2014 +0100 @@ -631,11 +631,11 @@ definition abupd :: "(abopt \ abopt) \ state \ state" - where "abupd f = map_pair f id" + where "abupd f = map_prod f id" definition supd :: "(st \ st) \ state \ state" - where "supd = map_pair id" + where "supd = map_prod id" lemma abupd_def2 [simp]: "abupd f (x,s) = (f x,s)" by (simp add: abupd_def) diff -r 62156e694f3d -r 68c5104d2204 src/HOL/Basic_BNFs.thy --- a/src/HOL/Basic_BNFs.thy Thu Mar 06 13:36:15 2014 +0100 +++ b/src/HOL/Basic_BNFs.thy Thu Mar 06 13:36:48 2014 +0100 @@ -129,27 +129,27 @@ by (simp add: prod_rel_def) bnf "'a \ 'b" - map: map_pair + map: map_prod sets: fsts snds bd: natLeq rel: prod_rel proof (unfold prod_set_defs) - show "map_pair id id = id" by (rule map_pair.id) + show "map_prod id id = id" by (rule map_prod.id) next fix f1 f2 g1 g2 - show "map_pair (g1 o f1) (g2 o f2) = map_pair g1 g2 o map_pair f1 f2" - by (rule map_pair.comp[symmetric]) + show "map_prod (g1 o f1) (g2 o f2) = map_prod g1 g2 o map_prod f1 f2" + by (rule map_prod.comp[symmetric]) next fix x f1 f2 g1 g2 assume "\z. z \ {fst x} \ f1 z = g1 z" "\z. z \ {snd x} \ f2 z = g2 z" - thus "map_pair f1 f2 x = map_pair g1 g2 x" by (cases x) simp + thus "map_prod f1 f2 x = map_prod g1 g2 x" by (cases x) simp next fix f1 f2 - show "(\x. {fst x}) o map_pair f1 f2 = image f1 o (\x. {fst x})" + show "(\x. {fst x}) o map_prod f1 f2 = image f1 o (\x. {fst x})" by (rule ext, unfold o_apply) simp next fix f1 f2 - show "(\x. {snd x}) o map_pair f1 f2 = image f2 o (\x. {snd x})" + show "(\x. {snd x}) o map_prod f1 f2 = image f2 o (\x. {snd x})" by (rule ext, unfold o_apply) simp next show "card_order natLeq" by (rule natLeq_card_order) @@ -169,8 +169,8 @@ next fix R S show "prod_rel R S = - (Grp {x. {fst x} \ Collect (split R) \ {snd x} \ Collect (split S)} (map_pair fst fst))\\ OO - Grp {x. {fst x} \ Collect (split R) \ {snd x} \ Collect (split S)} (map_pair snd snd)" + (Grp {x. {fst x} \ Collect (split R) \ {snd x} \ Collect (split S)} (map_prod fst fst))\\ OO + Grp {x. {fst x} \ Collect (split R) \ {snd x} \ Collect (split S)} (map_prod snd snd)" unfolding prod_set_defs prod_rel_def Grp_def relcompp.simps conversep.simps fun_eq_iff by auto qed diff -r 62156e694f3d -r 68c5104d2204 src/HOL/Cardinals/Ordinal_Arithmetic.thy --- a/src/HOL/Cardinals/Ordinal_Arithmetic.thy Thu Mar 06 13:36:15 2014 +0100 +++ b/src/HOL/Cardinals/Ordinal_Arithmetic.thy Thu Mar 06 13:36:48 2014 +0100 @@ -13,7 +13,7 @@ definition osum :: "'a rel \ 'b rel \ ('a + 'b) rel" (infixr "+o" 70) where - "r +o r' = map_pair Inl Inl ` r \ map_pair Inr Inr ` r' \ + "r +o r' = map_prod Inl Inl ` r \ map_prod Inr Inr ` r' \ {(Inl a, Inr a') | a a' . a \ Field r \ a' \ Field r'}" lemma Field_osum: "Field(r +o r') = Inl ` Field r \ Inr ` Field r'" @@ -100,11 +100,11 @@ unfolding osum_def Total_Id_Field[OF r] Total_Id_Field[OF r'] by auto lemma osum_minus_Id1: - "r \ Id \ (r +o r') - Id \ (Inl ` Field r \ Inr ` Field r') \ (map_pair Inr Inr ` (r' - Id))" + "r \ Id \ (r +o r') - Id \ (Inl ` Field r \ Inr ` Field r') \ (map_prod Inr Inr ` (r' - Id))" unfolding osum_def by auto lemma osum_minus_Id2: - "r' \ Id \ (r +o r') - Id \ (map_pair Inl Inl ` (r - Id)) \ (Inl ` Field r \ Inr ` Field r')" + "r' \ Id \ (r +o r') - Id \ (map_prod Inl Inl ` (r - Id)) \ (Inl ` Field r \ Inr ` Field r')" unfolding osum_def by auto lemma osum_wf_Id: @@ -122,11 +122,11 @@ proof (elim disjE) assume "r \ Id" thus "wf ((r +o r') - Id)" - by (rule wf_subset[rotated, OF osum_minus_Id1 wf_Un[OF 1 wf_map_pair_image[OF WF']]]) auto + by (rule wf_subset[rotated, OF osum_minus_Id1 wf_Un[OF 1 wf_map_prod_image[OF WF']]]) auto next assume "r' \ Id" thus "wf ((r +o r') - Id)" - by (rule wf_subset[rotated, OF osum_minus_Id2 wf_Un[OF wf_map_pair_image[OF WF] 1]]) auto + by (rule wf_subset[rotated, OF osum_minus_Id2 wf_Un[OF wf_map_prod_image[OF WF] 1]]) auto qed qed @@ -158,10 +158,10 @@ shows "r \o r +o r'" using assms osum_embedL osum_Well_order unfolding ordLeq_def by blast -lemma dir_image_alt: "dir_image r f = map_pair f f ` r" - unfolding dir_image_def map_pair_def by auto +lemma dir_image_alt: "dir_image r f = map_prod f f ` r" + unfolding dir_image_def map_prod_def by auto -lemma map_pair_ordIso: "\Well_order r; inj_on f (Field r)\ \ map_pair f f ` r =o r" +lemma map_prod_ordIso: "\Well_order r; inj_on f (Field r)\ \ map_prod f f ` r =o r" unfolding dir_image_alt[symmetric] by (rule ordIso_symmetric[OF dir_image_ordIso]) definition oprod :: "'a rel \ 'b rel \ ('a \ 'b) rel" (infixr "*o" 80) @@ -960,7 +960,7 @@ unfolding Field_osum iso_def bij_betw_def image_image image_Un by auto moreover from f have "compat ?L ?R ?f" unfolding osum_def iso_iff3[OF r s] compat_def bij_betw_def - by (auto simp: map_pair_imageI) + by (auto simp: map_prod_imageI) ultimately have "iso ?L ?R ?f" by (subst iso_iff3) (auto intro: osum_Well_order r s t) thus ?thesis unfolding ordIso_def by (auto intro: osum_Well_order r s t) qed @@ -978,7 +978,7 @@ unfolding Field_osum iso_def bij_betw_def image_image image_Un by auto moreover from f have "compat ?L ?R ?f" unfolding osum_def iso_iff3[OF r s] compat_def bij_betw_def - by (auto simp: map_pair_imageI) + by (auto simp: map_prod_imageI) ultimately have "iso ?L ?R ?f" by (subst iso_iff3) (auto intro: osum_Well_order r s t) thus ?thesis unfolding ordIso_def by (auto intro: osum_Well_order r s t) qed @@ -1019,14 +1019,14 @@ 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 = "map_pair f id" + let ?f = "map_prod f id" from f have "inj_on ?f (Field ?L)" unfolding Field_oprod iso_def bij_betw_def inj_on_def by fastforce with f have "bij_betw ?f (Field ?L) (Field ?R)" - unfolding Field_oprod iso_def bij_betw_def by (auto intro!: map_pair_surj_on) + unfolding Field_oprod iso_def bij_betw_def by (auto intro!: map_prod_surj_on) moreover from f have "compat ?L ?R ?f" unfolding iso_iff3[OF r s] compat_def oprod_def bij_betw_def - by (auto simp: map_pair_imageI) + by (auto simp: map_prod_imageI) ultimately have "iso ?L ?R ?f" by (subst iso_iff3) (auto intro: oprod_Well_order r s t) thus ?thesis unfolding ordIso_def by (auto intro: oprod_Well_order r s t) qed @@ -1037,14 +1037,14 @@ 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 = "map_pair id f" + let ?f = "map_prod id f" from f have "inj_on ?f (Field ?L)" unfolding Field_oprod iso_def bij_betw_def inj_on_def by fastforce with f have "bij_betw ?f (Field ?L) (Field ?R)" - unfolding Field_oprod iso_def bij_betw_def by (auto intro!: map_pair_surj_on) + unfolding Field_oprod iso_def bij_betw_def by (auto intro!: map_prod_surj_on) moreover from f well_order_on_domain[OF r] have "compat ?L ?R ?f" unfolding iso_iff3[OF r s] compat_def oprod_def bij_betw_def - by (auto simp: map_pair_imageI dest: inj_onD) + by (auto simp: map_prod_imageI dest: inj_onD) ultimately have "iso ?L ?R ?f" by (subst iso_iff3) (auto intro: oprod_Well_order r s t) thus ?thesis unfolding ordIso_def by (auto intro: oprod_Well_order r s t) qed @@ -1095,10 +1095,10 @@ begin lemma osum_ozeroL: "ozero +o r =o r" - using r unfolding osum_def ozero_def by (auto intro: map_pair_ordIso) + using r unfolding osum_def ozero_def by (auto intro: map_prod_ordIso) lemma osum_ozeroR: "r +o ozero =o r" - using r unfolding osum_def ozero_def by (auto intro: map_pair_ordIso) + using r unfolding osum_def ozero_def by (auto intro: map_prod_ordIso) lemma osum_assoc: "(r +o s) +o t =o r +o s +o t" (is "?L =o ?R") proof - @@ -1113,7 +1113,7 @@ assume "(a, b) \ ?L" thus "(?f a, ?f b) \ ?R" unfolding osum_def[of "r +o s" t] osum_def[of r "s +o t"] Field_osum - unfolding osum_def Field_osum image_iff image_Un map_pair_def + unfolding osum_def Field_osum image_iff image_Un map_prod_def by fastforce qed ultimately have "iso ?L ?R ?f" using r s t by (subst iso_iff3) (auto intro: osum_Well_order) @@ -1132,7 +1132,7 @@ 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 + from *(2,4) have "compat ?L ?R ?f" unfolding compat_def osum_def map_prod_def by fastforce moreover interpret t!: wo_rel t by unfold_locales (rule t) interpret rt!: wo_rel ?R by unfold_locales (rule osum_Well_order[OF r t]) @@ -1194,7 +1194,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 = "map_pair id f" + let ?f = "map_prod id f" from *(1) have "inj_on ?f (Field ?L)" unfolding Field_oprod inj_on_def by fastforce moreover from *(2,4) the_inv_into_f_f[OF *(1)] have "compat ?L ?R ?f" unfolding compat_def oprod_def @@ -1211,7 +1211,7 @@ from not_ordLess_ordIso[OF assms(1)] have "r \ {}" by (metis ozero_def ozero_ordIso) hence "Field r \ {}" unfolding Field_def by auto with *(4) have "?f ` Field ?L \ Field ?R" unfolding Field_oprod - by auto (metis SigmaD2 SigmaI map_pair_surj_on) + by auto (metis SigmaD2 SigmaI map_prod_surj_on) ultimately have "embedS ?L ?R ?f" using embedS_iff[OF oprod_Well_order[OF r s], of ?R ?f] by auto thus ?thesis unfolding ordLess_def by (auto intro: oprod_Well_order r s t) qed @@ -1222,10 +1222,10 @@ 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 = "map_pair f id" + let ?f = "map_prod 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_oprod underS_def unfolding map_pair_def oprod_def by auto + unfolding Field_oprod underS_def unfolding map_prod_def oprod_def by auto thus ?thesis unfolding ordLeq_def2 by (auto intro: oprod_Well_order r s t) qed diff -r 62156e694f3d -r 68c5104d2204 src/HOL/Library/Code_Target_Int.thy --- a/src/HOL/Library/Code_Target_Int.thy Thu Mar 06 13:36:15 2014 +0100 +++ b/src/HOL/Library/Code_Target_Int.thy Thu Mar 06 13:36:48 2014 +0100 @@ -67,7 +67,7 @@ by simp lemma [code]: - "Divides.divmod_abs k l = map_pair int_of_integer int_of_integer + "Divides.divmod_abs k l = map_prod int_of_integer int_of_integer (Code_Numeral.divmod_abs (of_int k) (of_int l))" by (simp add: prod_eq_iff) diff -r 62156e694f3d -r 68c5104d2204 src/HOL/Library/Quotient_Product.thy --- a/src/HOL/Library/Quotient_Product.thy Thu Mar 06 13:36:15 2014 +0100 +++ b/src/HOL/Library/Quotient_Product.thy Thu Mar 06 13:36:48 2014 +0100 @@ -10,8 +10,8 @@ subsection {* Rules for the Quotient package *} -lemma map_pair_id [id_simps]: - shows "map_pair id id = id" +lemma map_prod_id [id_simps]: + shows "map_prod id id = id" by (simp add: fun_eq_iff) lemma prod_rel_eq [id_simps]: @@ -27,9 +27,9 @@ lemma prod_quotient [quot_thm]: assumes "Quotient3 R1 Abs1 Rep1" assumes "Quotient3 R2 Abs2 Rep2" - shows "Quotient3 (prod_rel R1 R2) (map_pair Abs1 Abs2) (map_pair Rep1 Rep2)" + shows "Quotient3 (prod_rel R1 R2) (map_prod Abs1 Abs2) (map_prod Rep1 Rep2)" apply (rule Quotient3I) - apply (simp add: map_pair.compositionality comp_def map_pair.identity + apply (simp add: map_prod.compositionality comp_def map_prod.identity Quotient3_abs_rep [OF assms(1)] Quotient3_abs_rep [OF assms(2)]) apply (simp add: split_paired_all Quotient3_rel_rep [OF assms(1)] Quotient3_rel_rep [OF assms(2)]) using Quotient3_rel [OF assms(1)] Quotient3_rel [OF assms(2)] @@ -47,7 +47,7 @@ lemma Pair_prs [quot_preserve]: assumes q1: "Quotient3 R1 Abs1 Rep1" assumes q2: "Quotient3 R2 Abs2 Rep2" - shows "(Rep1 ---> Rep2 ---> (map_pair Abs1 Abs2)) Pair = Pair" + shows "(Rep1 ---> Rep2 ---> (map_prod Abs1 Abs2)) Pair = Pair" apply(simp add: fun_eq_iff) apply(simp add: Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2]) done @@ -61,7 +61,7 @@ lemma fst_prs [quot_preserve]: assumes q1: "Quotient3 R1 Abs1 Rep1" assumes q2: "Quotient3 R2 Abs2 Rep2" - shows "(map_pair Rep1 Rep2 ---> Abs1) fst = fst" + shows "(map_prod Rep1 Rep2 ---> Abs1) fst = fst" by (simp add: fun_eq_iff Quotient3_abs_rep[OF q1]) lemma snd_rsp [quot_respect]: @@ -73,7 +73,7 @@ lemma snd_prs [quot_preserve]: assumes q1: "Quotient3 R1 Abs1 Rep1" assumes q2: "Quotient3 R2 Abs2 Rep2" - shows "(map_pair Rep1 Rep2 ---> Abs2) snd = snd" + shows "(map_prod Rep1 Rep2 ---> Abs2) snd = snd" by (simp add: fun_eq_iff Quotient3_abs_rep[OF q2]) lemma split_rsp [quot_respect]: @@ -83,7 +83,7 @@ lemma split_prs [quot_preserve]: assumes q1: "Quotient3 R1 Abs1 Rep1" and q2: "Quotient3 R2 Abs2 Rep2" - shows "(((Abs1 ---> Abs2 ---> id) ---> map_pair Rep1 Rep2 ---> id) split) = split" + shows "(((Abs1 ---> Abs2 ---> id) ---> map_prod Rep1 Rep2 ---> id) split) = split" by (simp add: fun_eq_iff Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2]) lemma [quot_respect]: @@ -95,7 +95,7 @@ assumes q1: "Quotient3 R1 abs1 rep1" and q2: "Quotient3 R2 abs2 rep2" shows "((abs1 ---> abs1 ---> id) ---> (abs2 ---> abs2 ---> id) ---> - map_pair rep1 rep2 ---> map_pair rep1 rep2 ---> id) prod_rel = prod_rel" + map_prod rep1 rep2 ---> map_prod rep1 rep2 ---> id) prod_rel = prod_rel" by (simp add: fun_eq_iff Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2]) lemma [quot_preserve]: diff -r 62156e694f3d -r 68c5104d2204 src/HOL/Lifting_Product.thy --- a/src/HOL/Lifting_Product.thy Thu Mar 06 13:36:15 2014 +0100 +++ b/src/HOL/Lifting_Product.thy Thu Mar 06 13:36:48 2014 +0100 @@ -70,8 +70,7 @@ lemma Quotient_prod[quot_map]: assumes "Quotient R1 Abs1 Rep1 T1" assumes "Quotient R2 Abs2 Rep2 T2" - shows "Quotient (prod_rel R1 R2) (map_pair Abs1 Abs2) - (map_pair Rep1 Rep2) (prod_rel T1 T2)" + shows "Quotient (prod_rel R1 R2) (map_prod Abs1 Abs2) (map_prod Rep1 Rep2) (prod_rel T1 T2)" using assms unfolding Quotient_alt_def by auto subsection {* Transfer rules for the Transfer package *} @@ -97,10 +96,10 @@ "((prod_rel A B ===> C) ===> A ===> B ===> C) curry curry" unfolding curry_def by transfer_prover -lemma map_pair_transfer [transfer_rule]: +lemma map_prod_transfer [transfer_rule]: "((A ===> C) ===> (B ===> D) ===> prod_rel A B ===> prod_rel C D) - map_pair map_pair" - unfolding map_pair_def [abs_def] by transfer_prover + map_prod map_prod" + unfolding map_prod_def [abs_def] by transfer_prover lemma prod_rel_transfer [transfer_rule]: "((A ===> B ===> op =) ===> (C ===> D ===> op =) ===> diff -r 62156e694f3d -r 68c5104d2204 src/HOL/List.thy --- a/src/HOL/List.thy Thu Mar 06 13:36:15 2014 +0100 +++ b/src/HOL/List.thy Thu Mar 06 13:36:48 2014 +0100 @@ -5251,7 +5251,7 @@ lexn :: "('a \ 'a) set \ nat \ ('a list \ 'a list) set" where "lexn r 0 = {}" | "lexn r (Suc n) = - (map_pair (%(x, xs). x#xs) (%(x, xs). x#xs) ` (r <*lex*> lexn r n)) Int + (map_prod (%(x, xs). x#xs) (%(x, xs). x#xs) ` (r <*lex*> lexn r n)) Int {(xs, ys). length xs = Suc n \ length ys = Suc n}" definition lex :: "('a \ 'a) set \ ('a list \ 'a list) set" where @@ -5265,7 +5265,7 @@ apply (induct n, simp, simp) apply(rule wf_subset) prefer 2 apply (rule Int_lower1) -apply(rule wf_map_pair_image) +apply(rule wf_map_prod_image) prefer 2 apply (rule inj_onI, auto) done diff -r 62156e694f3d -r 68c5104d2204 src/HOL/Matrix_LP/ComputeNumeral.thy --- a/src/HOL/Matrix_LP/ComputeNumeral.thy Thu Mar 06 13:36:15 2014 +0100 +++ b/src/HOL/Matrix_LP/ComputeNumeral.thy Thu Mar 06 13:36:48 2014 +0100 @@ -58,7 +58,7 @@ else apsnd uminus (posDivAlg (-a) (-b)))" by (auto simp only: divmod_int_def) -lemmas compute_div_mod = div_int_def mod_int_def divmod adjust apsnd_def map_pair_def posDivAlg.simps negDivAlg.simps +lemmas compute_div_mod = div_int_def mod_int_def divmod adjust apsnd_def map_prod_def posDivAlg.simps negDivAlg.simps diff -r 62156e694f3d -r 68c5104d2204 src/HOL/Metis_Examples/Abstraction.thy --- a/src/HOL/Metis_Examples/Abstraction.thy Thu Mar 06 13:36:15 2014 +0100 +++ b/src/HOL/Metis_Examples/Abstraction.thy Thu Mar 06 13:36:48 2014 +0100 @@ -160,7 +160,7 @@ by (metis (lifting) imageE) lemma image_TimesA: "(\(x, y). (f x, g y)) ` (A \ B) = (f ` A) \ (g ` B)" -by (metis map_pair_def map_pair_surj_on) +by (metis map_prod_def map_prod_surj_on) lemma image_TimesB: "(\(x, y, z). (f x, g y, h z)) ` (A \ B \ C) = (f ` A) \ (g ` B) \ (h ` C)" diff -r 62156e694f3d -r 68c5104d2204 src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Thu Mar 06 13:36:15 2014 +0100 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Thu Mar 06 13:36:48 2014 +0100 @@ -1564,8 +1564,8 @@ text {* Case expressions *} definition - "map_pairs xs ys = (map (%((a, b), c). (a, b, c)) xs = ys)" + "map_prods xs ys = (map (%((a, b), c). (a, b, c)) xs = ys)" -code_pred [inductify] map_pairs . +code_pred [inductify] map_prods . end diff -r 62156e694f3d -r 68c5104d2204 src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Thu Mar 06 13:36:15 2014 +0100 +++ b/src/HOL/Product_Type.thy Thu Mar 06 13:36:48 2014 +0100 @@ -820,50 +820,50 @@ no_notation scomp (infixl "\\" 60) text {* - @{term map_pair} --- action of the product functor upon + @{term map_prod} --- action of the product functor upon functions. *} -definition map_pair :: "('a \ 'c) \ ('b \ 'd) \ 'a \ 'b \ 'c \ 'd" where - "map_pair f g = (\(x, y). (f x, g y))" +definition map_prod :: "('a \ 'c) \ ('b \ 'd) \ 'a \ 'b \ 'c \ 'd" where + "map_prod f g = (\(x, y). (f x, g y))" -lemma map_pair_simp [simp, code]: - "map_pair f g (a, b) = (f a, g b)" - by (simp add: map_pair_def) +lemma map_prod_simp [simp, code]: + "map_prod f g (a, b) = (f a, g b)" + by (simp add: map_prod_def) -functor map_pair: map_pair +functor map_prod: map_prod by (auto simp add: split_paired_all) -lemma fst_map_pair [simp]: - "fst (map_pair f g x) = f (fst x)" +lemma fst_map_prod [simp]: + "fst (map_prod f g x) = f (fst x)" by (cases x) simp_all lemma snd_prod_fun [simp]: - "snd (map_pair f g x) = g (snd x)" + "snd (map_prod f g x) = g (snd x)" by (cases x) simp_all -lemma fst_comp_map_pair [simp]: - "fst \ map_pair f g = f \ fst" +lemma fst_comp_map_prod [simp]: + "fst \ map_prod f g = f \ fst" by (rule ext) simp_all -lemma snd_comp_map_pair [simp]: - "snd \ map_pair f g = g \ snd" +lemma snd_comp_map_prod [simp]: + "snd \ map_prod f g = g \ snd" by (rule ext) simp_all -lemma map_pair_compose: - "map_pair (f1 o f2) (g1 o g2) = (map_pair f1 g1 o map_pair f2 g2)" - by (rule ext) (simp add: map_pair.compositionality comp_def) +lemma map_prod_compose: + "map_prod (f1 o f2) (g1 o g2) = (map_prod f1 g1 o map_prod f2 g2)" + by (rule ext) (simp add: map_prod.compositionality comp_def) -lemma map_pair_ident [simp]: - "map_pair (%x. x) (%y. y) = (%z. z)" - by (rule ext) (simp add: map_pair.identity) +lemma map_prod_ident [simp]: + "map_prod (%x. x) (%y. y) = (%z. z)" + by (rule ext) (simp add: map_prod.identity) -lemma map_pair_imageI [intro]: - "(a, b) \ R \ (f a, g b) \ map_pair f g ` R" +lemma map_prod_imageI [intro]: + "(a, b) \ R \ (f a, g b) \ map_prod f g ` R" by (rule image_eqI) simp_all lemma prod_fun_imageE [elim!]: - assumes major: "c \ map_pair f g ` R" + assumes major: "c \ map_prod f g ` R" and cases: "\x y. c = (f x, g y) \ (x, y) \ R \ P" shows P apply (rule major [THEN imageE]) @@ -873,10 +873,10 @@ done definition apfst :: "('a \ 'c) \ 'a \ 'b \ 'c \ 'b" where - "apfst f = map_pair f id" + "apfst f = map_prod f id" definition apsnd :: "('b \ 'c) \ 'a \ 'b \ 'a \ 'c" where - "apsnd f = map_pair id f" + "apsnd f = map_prod id f" lemma apfst_conv [simp, code]: "apfst f (x, y) = (f x, y)" @@ -1144,54 +1144,54 @@ "x \ Product_Type.product A B \ x \ A \ B" by (simp add: product_def) -text {* The following @{const map_pair} lemmas are due to Joachim Breitner: *} +text {* The following @{const map_prod} lemmas are due to Joachim Breitner: *} -lemma map_pair_inj_on: +lemma map_prod_inj_on: assumes "inj_on f A" and "inj_on g B" - shows "inj_on (map_pair f g) (A \ B)" + shows "inj_on (map_prod f g) (A \ B)" proof (rule inj_onI) fix x :: "'a \ 'c" and y :: "'a \ 'c" assume "x \ A \ B" hence "fst x \ A" and "snd x \ B" by auto assume "y \ A \ B" hence "fst y \ A" and "snd y \ B" by auto - assume "map_pair f g x = map_pair f g y" - hence "fst (map_pair f g x) = fst (map_pair f g y)" by (auto) + assume "map_prod f g x = map_prod f g y" + hence "fst (map_prod f g x) = fst (map_prod f g y)" by (auto) hence "f (fst x) = f (fst y)" by (cases x,cases y,auto) with `inj_on f A` and `fst x \ A` and `fst y \ A` have "fst x = fst y" by (auto dest:dest:inj_onD) - moreover from `map_pair f g x = map_pair f g y` - have "snd (map_pair f g x) = snd (map_pair f g y)" by (auto) + moreover from `map_prod f g x = map_prod f g y` + have "snd (map_prod f g x) = snd (map_prod f g y)" by (auto) hence "g (snd x) = g (snd y)" by (cases x,cases y,auto) with `inj_on g B` and `snd x \ B` and `snd y \ B` have "snd x = snd y" by (auto dest:dest:inj_onD) ultimately show "x = y" by(rule prod_eqI) qed -lemma map_pair_surj: +lemma map_prod_surj: fixes f :: "'a \ 'b" and g :: "'c \ 'd" assumes "surj f" and "surj g" - shows "surj (map_pair f g)" + shows "surj (map_prod f g)" unfolding surj_def proof fix y :: "'b \ 'd" from `surj f` obtain a where "fst y = f a" by (auto elim:surjE) moreover from `surj g` obtain b where "snd y = g b" by (auto elim:surjE) - ultimately have "(fst y, snd y) = map_pair f g (a,b)" by auto - thus "\x. y = map_pair f g x" by auto + ultimately have "(fst y, snd y) = map_prod f g (a,b)" by auto + thus "\x. y = map_prod f g x" by auto qed -lemma map_pair_surj_on: +lemma map_prod_surj_on: assumes "f ` A = A'" and "g ` B = B'" - shows "map_pair f g ` (A \ B) = A' \ B'" + shows "map_prod f g ` (A \ B) = A' \ B'" unfolding image_def proof(rule set_eqI,rule iffI) fix x :: "'a \ 'c" - assume "x \ {y\'a \ 'c. \x\'b \ 'd\A \ B. y = map_pair f g x}" - then obtain y where "y \ A \ B" and "x = map_pair f g y" by blast + assume "x \ {y\'a \ 'c. \x\'b \ 'd\A \ B. y = map_prod f g x}" + then obtain y where "y \ A \ B" and "x = map_prod f g y" by blast from `image f A = A'` and `y \ A \ B` have "f (fst y) \ A'" by auto moreover from `image g B = B'` and `y \ A \ B` have "g (snd y) \ B'" by auto ultimately have "(f (fst y), g (snd y)) \ (A' \ B')" by auto - with `x = map_pair f g y` show "x \ A' \ B'" by (cases y, auto) + with `x = map_prod f g y` show "x \ A' \ B'" by (cases y, auto) next fix x :: "'a \ 'c" assume "x \ A' \ B'" hence "fst x \ A'" and "snd x \ B'" by auto @@ -1199,10 +1199,10 @@ then obtain a where "a \ A" and "fst x = f a" by (rule imageE) moreover from `image g B = B'` and `snd x \ B'` obtain b where "b \ B" and "snd x = g b" by auto - ultimately have "(fst x, snd x) = map_pair f g (a,b)" by auto + ultimately have "(fst x, snd x) = map_prod f g (a,b)" by auto moreover from `a \ A` and `b \ B` have "(a , b) \ A \ B" by auto - ultimately have "\y \ A \ B. x = map_pair f g y" by auto - thus "x \ {x. \y \ A \ B. x = map_pair f g y}" by auto + ultimately have "\y \ A \ B. x = map_prod f g y" by auto + thus "x \ {x. \y \ A \ B. x = map_prod f g y}" by auto qed diff -r 62156e694f3d -r 68c5104d2204 src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Thu Mar 06 13:36:15 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Thu Mar 06 13:36:48 2014 +0100 @@ -37,10 +37,10 @@ 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 map_sum.simps}; +val sum_prod_thms_map = @{thms id_apply map_prod_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 + Union_Un_distrib image_iff o_apply map_prod_simp 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}; diff -r 62156e694f3d -r 68c5104d2204 src/HOL/Tools/BNF/bnf_fp_n2m.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Thu Mar 06 13:36:15 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Thu Mar 06 13:36:48 2014 +0100 @@ -34,7 +34,7 @@ val ((fAT, fBT), fT) = `dest_funT (fastype_of f); val ((gAT, gBT), gT) = `dest_funT (fastype_of g); in - Const (@{const_name map_pair}, + Const (@{const_name map_prod}, fT --> gT --> HOLogic.mk_prodT (fAT, gAT) --> HOLogic.mk_prodT (fBT, gBT)) $ f $ g end; @@ -404,10 +404,10 @@ 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 map_sum.comp} @ - @{thms id_apply comp_id id_comp map_pair.comp map_pair.id map_sum.comp map_sum.id}; + map (fn thm => thm RS rewrite_comp_comp) @{thms map_prod.comp map_sum.comp} @ + @{thms id_apply comp_id id_comp map_prod.comp map_prod.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 fst_convol map_prod_o_convol convol_o} @{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 62156e694f3d -r 68c5104d2204 src/HOL/Tools/BNF/bnf_fp_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_util.ML Thu Mar 06 13:36:15 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Thu Mar 06 13:36:48 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_map_sum_id} + then fp_case fp @{thm map_prod_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; diff -r 62156e694f3d -r 68c5104d2204 src/HOL/Tools/Quickcheck/narrowing_generators.ML --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Thu Mar 06 13:36:15 2014 +0100 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Thu Mar 06 13:36:48 2014 +0100 @@ -366,7 +366,7 @@ val (ft', fT') = eval_function fT val (st', sT') = eval_function sT val T' = Type (@{type_name prod}, [fT', sT']) - val map_const = Const (@{const_name map_pair}, (fT' --> fT) --> (sT' --> sT) --> T' --> T) + val map_const = Const (@{const_name map_prod}, (fT' --> fT) --> (sT' --> sT) --> T' --> T) fun apply_dummy T t = absdummy T (t (Bound 0)) in (fn t => list_comb (map_const, [apply_dummy fT' ft', apply_dummy sT' st', t]), T') diff -r 62156e694f3d -r 68c5104d2204 src/HOL/Wellfounded.thy --- a/src/HOL/Wellfounded.thy Thu Mar 06 13:36:15 2014 +0100 +++ b/src/HOL/Wellfounded.thy Thu Mar 06 13:36:48 2014 +0100 @@ -240,7 +240,7 @@ text{*Well-foundedness of image*} -lemma wf_map_pair_image: "[| wf r; inj f |] ==> wf(map_pair f f ` r)" +lemma wf_map_prod_image: "[| wf r; inj f |] ==> wf (map_prod f f ` r)" apply (simp only: wf_eq_minimal, clarify) apply (case_tac "EX p. f p : Q") apply (erule_tac x = "{p. f p : Q}" in allE) diff -r 62156e694f3d -r 68c5104d2204 src/HOL/ex/Coercion_Examples.thy --- a/src/HOL/ex/Coercion_Examples.thy Thu Mar 06 13:36:15 2014 +0100 +++ b/src/HOL/ex/Coercion_Examples.thy Thu Mar 06 13:36:48 2014 +0100 @@ -52,10 +52,10 @@ declare [[coercion_map "\ f g h . g o h o f"]] -primrec map_pair :: "('a \ 'c) \ ('b \ 'd) \ ('a * 'b) \ ('c * 'd)" where - "map_pair f g (x,y) = (f x, g y)" +primrec map_prod :: "('a \ 'c) \ ('b \ 'd) \ ('a * 'b) \ ('c * 'd)" where + "map_prod f g (x,y) = (f x, g y)" -declare [[coercion_map map_pair]] +declare [[coercion_map map_prod]] (* Examples taken from the haskell draft implementation *)