--- 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 \<union> varsOf x"
| "varsOf (Lam x b) = {x} \<union> varsOf b"
-| "varsOf (Lt F t) = varsOf t \<union> (\<Union> { {x} \<union> X | x X. (x,X) |\<in>| fimage (map_pair id varsOf) F})"
+| "varsOf (Lt F t) = varsOf t \<union> (\<Union> { {x} \<union> X | x X. (x,X) |\<in>| fimage (map_prod id varsOf) F})"
primrec fvarsOf :: "'a trm \<Rightarrow> 'a set" where
"fvarsOf (Var x) = {x}"
| "fvarsOf (App t1 t2) = fvarsOf t1 \<union> fvarsOf t2"
| "fvarsOf (Lam x t) = fvarsOf t - {x}"
-| "fvarsOf (Lt xts t) = fvarsOf t - {x | x X. (x,X) |\<in>| fimage (map_pair id varsOf) xts} \<union>
- (\<Union> {X | x X. (x,X) |\<in>| fimage (map_pair id varsOf) xts})"
+| "fvarsOf (Lt xts t) = fvarsOf t - {x | x X. (x,X) |\<in>| fimage (map_prod id varsOf) xts} \<union>
+ (\<Union> {X | x X. (x,X) |\<in>| fimage (map_prod id varsOf) xts})"
lemma diff_Un_incl_triv: "\<lbrakk>A \<subseteq> D; C \<subseteq> E\<rbrakk> \<Longrightarrow> A - B \<union> C \<subseteq> D \<union> E" by blast
-lemma in_fimage_map_pair_fset_iff[simp]:
- "(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)"
+lemma in_fimage_map_prod_fset_iff[simp]:
+ "(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)"
by force
lemma fvarsOf_varsOf: "fvarsOf t \<subseteq> varsOf t"
--- 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 \<Rightarrow> Var (f s)
| App l l' \<Rightarrow> App (rename_lam f l) (rename_lam f l')
| Abs s l \<Rightarrow> Abs (f s) (rename_lam f l)
- | Let SL l \<Rightarrow> Let (fimage (map_pair f (rename_lam f)) SL) (rename_lam f l))"
+ | Let SL l \<Rightarrow> Let (fimage (map_prod f (rename_lam f)) SL) (rename_lam f l))"
primcorec
j1_sum :: "('a\<Colon>{zero,one,plus}) \<Rightarrow> 'a J1" and
--- 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\<Colon>{zero,plus}) I1 \<Rightarrow> 'a" and
--- 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 @@
"\<theta> xb = F id <id, \<lambda> a. (snd xb)> (fst xb)"
(* The strength laws for \<theta>: *)
-lemma \<theta>_natural: "F id (map_pair f g) o \<theta> = \<theta> o map_pair (F id f) g"
- unfolding \<theta>_def F.map_comp comp_def id_apply convol_def map_pair_def split_beta fst_conv snd_conv ..
+lemma \<theta>_natural: "F id (map_prod f g) o \<theta> = \<theta> o map_prod (F id f) g"
+ unfolding \<theta>_def F.map_comp comp_def id_apply convol_def map_prod_def split_beta fst_conv snd_conv ..
definition assl :: "'a * ('b * 'c) \<Rightarrow> ('a * 'b) * 'c" where
"assl abc = ((fst abc, fst (snd abc)), snd (snd abc))"
@@ -167,8 +167,8 @@
lemma \<theta>_rid: "F id fst o \<theta> = fst"
unfolding \<theta>_def F.map_comp F.map_id comp_def id_apply convol_def fst_conv sym[OF id_def] ..
-lemma \<theta>_assl: "F id assl o \<theta> = \<theta> o map_pair \<theta> id o assl"
- unfolding assl_def \<theta>_def F.map_comp comp_def id_apply convol_def map_pair_def split fst_conv snd_conv ..
+lemma \<theta>_assl: "F id assl o \<theta> = \<theta> o map_prod \<theta> id o assl"
+ unfolding assl_def \<theta>_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>\<mu> = GetF "'a \<Rightarrow> ('a, 'b, 'c) spF\<^sub>\<mu>" | PutF "('b,'c) F"
codatatype ('a, 'b) spF\<^sub>\<nu> = InF (outF: "('a, 'b, ('a, 'b) spF\<^sub>\<nu>) spF\<^sub>\<mu>")
--- 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: "<f, g> o h = <f o h, g o h>"
unfolding convol_def by auto
-lemma map_pair_o_convol: "map_pair h1 h2 o <f, g> = <h1 o f, h2 o g>"
+lemma map_prod_o_convol: "map_prod h1 h2 o <f, g> = <h1 o f, h2 o g>"
unfolding convol_def by auto
-lemma map_pair_o_convol_id: "(map_pair f id \<circ> <id , g>) x = <id \<circ> f , g> x"
- unfolding map_pair_o_convol id_comp comp_id ..
+lemma map_prod_o_convol_id: "(map_prod f id \<circ> <id , g>) x = <id \<circ> 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)
--- 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 \<Rightarrow> abopt) \<Rightarrow> state \<Rightarrow> state"
- where "abupd f = map_pair f id"
+ where "abupd f = map_prod f id"
definition
supd :: "(st \<Rightarrow> st) \<Rightarrow> state \<Rightarrow> 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)
--- 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 \<times> '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 "\<And>z. z \<in> {fst x} \<Longrightarrow> f1 z = g1 z" "\<And>z. z \<in> {snd x} \<Longrightarrow> 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 "(\<lambda>x. {fst x}) o map_pair f1 f2 = image f1 o (\<lambda>x. {fst x})"
+ show "(\<lambda>x. {fst x}) o map_prod f1 f2 = image f1 o (\<lambda>x. {fst x})"
by (rule ext, unfold o_apply) simp
next
fix f1 f2
- show "(\<lambda>x. {snd x}) o map_pair f1 f2 = image f2 o (\<lambda>x. {snd x})"
+ show "(\<lambda>x. {snd x}) o map_prod f1 f2 = image f2 o (\<lambda>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} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_pair fst fst))\<inverse>\<inverse> OO
- Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_pair snd snd)"
+ (Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> Collect (split S)} (map_prod fst fst))\<inverse>\<inverse> OO
+ Grp {x. {fst x} \<subseteq> Collect (split R) \<and> {snd x} \<subseteq> 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
--- 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 \<Rightarrow> 'b rel \<Rightarrow> ('a + 'b) rel" (infixr "+o" 70)
where
- "r +o r' = map_pair Inl Inl ` r \<union> map_pair Inr Inr ` r' \<union>
+ "r +o r' = map_prod Inl Inl ` r \<union> map_prod Inr Inr ` r' \<union>
{(Inl a, Inr a') | a a' . a \<in> Field r \<and> a' \<in> Field r'}"
lemma Field_osum: "Field(r +o r') = Inl ` Field r \<union> 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 \<le> Id \<Longrightarrow> (r +o r') - Id \<le> (Inl ` Field r \<times> Inr ` Field r') \<union> (map_pair Inr Inr ` (r' - Id))"
+ "r \<le> Id \<Longrightarrow> (r +o r') - Id \<le> (Inl ` Field r \<times> Inr ` Field r') \<union> (map_prod Inr Inr ` (r' - Id))"
unfolding osum_def by auto
lemma osum_minus_Id2:
- "r' \<le> Id \<Longrightarrow> (r +o r') - Id \<le> (map_pair Inl Inl ` (r - Id)) \<union> (Inl ` Field r \<times> Inr ` Field r')"
+ "r' \<le> Id \<Longrightarrow> (r +o r') - Id \<le> (map_prod Inl Inl ` (r - Id)) \<union> (Inl ` Field r \<times> Inr ` Field r')"
unfolding osum_def by auto
lemma osum_wf_Id:
@@ -122,11 +122,11 @@
proof (elim disjE)
assume "r \<subseteq> 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' \<subseteq> 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 \<le>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: "\<lbrakk>Well_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> map_pair f f ` r =o r"
+lemma map_prod_ordIso: "\<lbrakk>Well_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> map_prod f f ` r =o r"
unfolding dir_image_alt[symmetric] by (rule ordIso_symmetric[OF dir_image_ordIso])
definition oprod :: "'a rel \<Rightarrow> 'b rel \<Rightarrow> ('a \<times> '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) \<in> ?L"
thus "(?f a, ?f b) \<in> ?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 \<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 = "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 \<noteq> {}" by (metis ozero_def ozero_ordIso)
hence "Field r \<noteq> {}" unfolding Field_def by auto
with *(4) have "?f ` Field ?L \<subset> 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: "\<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 = "map_pair f id"
+ let ?f = "map_prod 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_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
--- 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)
--- 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]:
--- 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 =) ===>
--- 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 \<times> 'a) set \<Rightarrow> nat \<Rightarrow> ('a list \<times> '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 \<and> length ys = Suc n}"
definition lex :: "('a \<times> 'a) set \<Rightarrow> ('a list \<times> '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
--- 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
--- 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: "(\<lambda>(x, y). (f x, g y)) ` (A \<times> B) = (f ` A) \<times> (g ` B)"
-by (metis map_pair_def map_pair_surj_on)
+by (metis map_prod_def map_prod_surj_on)
lemma image_TimesB:
"(\<lambda>(x, y, z). (f x, g y, h z)) ` (A \<times> B \<times> C) = (f ` A) \<times> (g ` B) \<times> (h ` C)"
--- 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
--- 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 "\<circ>\<rightarrow>" 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 \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'd" where
- "map_pair f g = (\<lambda>(x, y). (f x, g y))"
+definition map_prod :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'd" where
+ "map_prod f g = (\<lambda>(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 \<circ> map_pair f g = f \<circ> fst"
+lemma fst_comp_map_prod [simp]:
+ "fst \<circ> map_prod f g = f \<circ> fst"
by (rule ext) simp_all
-lemma snd_comp_map_pair [simp]:
- "snd \<circ> map_pair f g = g \<circ> snd"
+lemma snd_comp_map_prod [simp]:
+ "snd \<circ> map_prod f g = g \<circ> 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) \<in> R \<Longrightarrow> (f a, g b) \<in> map_pair f g ` R"
+lemma map_prod_imageI [intro]:
+ "(a, b) \<in> R \<Longrightarrow> (f a, g b) \<in> map_prod f g ` R"
by (rule image_eqI) simp_all
lemma prod_fun_imageE [elim!]:
- assumes major: "c \<in> map_pair f g ` R"
+ assumes major: "c \<in> map_prod f g ` R"
and cases: "\<And>x y. c = (f x, g y) \<Longrightarrow> (x, y) \<in> R \<Longrightarrow> P"
shows P
apply (rule major [THEN imageE])
@@ -873,10 +873,10 @@
done
definition apfst :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'b" where
- "apfst f = map_pair f id"
+ "apfst f = map_prod f id"
definition apsnd :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> '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 \<in> Product_Type.product A B \<longleftrightarrow> x \<in> A \<times> 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 \<times> B)"
+ shows "inj_on (map_prod f g) (A \<times> B)"
proof (rule inj_onI)
fix x :: "'a \<times> 'c" and y :: "'a \<times> 'c"
assume "x \<in> A \<times> B" hence "fst x \<in> A" and "snd x \<in> B" by auto
assume "y \<in> A \<times> B" hence "fst y \<in> A" and "snd y \<in> 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 \<in> A` and `fst y \<in> 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 \<in> B` and `snd y \<in> 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 \<Rightarrow> 'b" and g :: "'c \<Rightarrow> '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 \<times> '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 "\<exists>x. y = map_pair f g x" by auto
+ ultimately have "(fst y, snd y) = map_prod f g (a,b)" by auto
+ thus "\<exists>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 \<times> B) = A' \<times> B'"
+ shows "map_prod f g ` (A \<times> B) = A' \<times> B'"
unfolding image_def
proof(rule set_eqI,rule iffI)
fix x :: "'a \<times> 'c"
- assume "x \<in> {y\<Colon>'a \<times> 'c. \<exists>x\<Colon>'b \<times> 'd\<in>A \<times> B. y = map_pair f g x}"
- then obtain y where "y \<in> A \<times> B" and "x = map_pair f g y" by blast
+ assume "x \<in> {y\<Colon>'a \<times> 'c. \<exists>x\<Colon>'b \<times> 'd\<in>A \<times> B. y = map_prod f g x}"
+ then obtain y where "y \<in> A \<times> B" and "x = map_prod f g y" by blast
from `image f A = A'` and `y \<in> A \<times> B` have "f (fst y) \<in> A'" by auto
moreover from `image g B = B'` and `y \<in> A \<times> B` have "g (snd y) \<in> B'" by auto
ultimately have "(f (fst y), g (snd y)) \<in> (A' \<times> B')" by auto
- with `x = map_pair f g y` show "x \<in> A' \<times> B'" by (cases y, auto)
+ with `x = map_prod f g y` show "x \<in> A' \<times> B'" by (cases y, auto)
next
fix x :: "'a \<times> 'c"
assume "x \<in> A' \<times> B'" hence "fst x \<in> A'" and "snd x \<in> B'" by auto
@@ -1199,10 +1199,10 @@
then obtain a where "a \<in> A" and "fst x = f a" by (rule imageE)
moreover from `image g B = B'` and `snd x \<in> B'`
obtain b where "b \<in> 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 \<in> A` and `b \<in> B` have "(a , b) \<in> A \<times> B" by auto
- ultimately have "\<exists>y \<in> A \<times> B. x = map_pair f g y" by auto
- thus "x \<in> {x. \<exists>y \<in> A \<times> B. x = map_pair f g y}" by auto
+ ultimately have "\<exists>y \<in> A \<times> B. x = map_prod f g y" by auto
+ thus "x \<in> {x. \<exists>y \<in> A \<times> B. x = map_prod f g y}" by auto
qed
--- 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};
--- 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;
--- 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;
--- 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')
--- 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)
--- 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 "\<lambda> f g h . g o h o f"]]
-primrec map_pair :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a * 'b) \<Rightarrow> ('c * 'd)" where
- "map_pair f g (x,y) = (f x, g y)"
+primrec map_prod :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a * 'b) \<Rightarrow> ('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 *)