--- a/src/HOL/Bali/State.thy Thu Nov 18 17:01:16 2010 +0100
+++ b/src/HOL/Bali/State.thy Thu Nov 18 17:01:16 2010 +0100
@@ -631,11 +631,11 @@
definition
abupd :: "(abopt \<Rightarrow> abopt) \<Rightarrow> state \<Rightarrow> state"
- where "abupd f = prod_fun f id"
+ where "abupd f = map_pair f id"
definition
supd :: "(st \<Rightarrow> st) \<Rightarrow> state \<Rightarrow> state"
- where "supd = prod_fun id"
+ where "supd = map_pair id"
lemma abupd_def2 [simp]: "abupd f (x,s) = (f x,s)"
by (simp add: abupd_def)
--- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Thu Nov 18 17:01:16 2010 +0100
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Thu Nov 18 17:01:16 2010 +0100
@@ -131,7 +131,7 @@
SND > snd
CURRY > curry
UNCURRY > split
- "##" > prod_fun
+ "##" > map_pair
pair_case > split;
ignore_thms
--- a/src/HOL/Import/HOL/pair.imp Thu Nov 18 17:01:16 2010 +0100
+++ b/src/HOL/Import/HOL/pair.imp Thu Nov 18 17:01:16 2010 +0100
@@ -18,7 +18,7 @@
"LEX" > "HOL4Base.pair.LEX"
"CURRY" > "Product_Type.curry"
"," > "Product_Type.Pair"
- "##" > "prod_fun"
+ "##" > "map_pair"
thm_maps
"pair_induction" > "Datatype.prod.induct_correctness"
@@ -39,7 +39,7 @@
"RPROD_DEF" > "HOL4Base.pair.RPROD_DEF"
"PFORALL_THM" > "HOL4Base.pair.PFORALL_THM"
"PEXISTS_THM" > "HOL4Base.pair.PEXISTS_THM"
- "PAIR_MAP_THM" > "Product_Type.prod_fun"
+ "PAIR_MAP_THM" > "Product_Type.map_pair"
"PAIR_MAP" > "HOL4Compat.PAIR_MAP"
"PAIR_EQ" > "Datatype.prod.simps_1"
"PAIR" > "HOL4Compat.PAIR"
--- a/src/HOL/Import/HOL4Compat.thy Thu Nov 18 17:01:16 2010 +0100
+++ b/src/HOL/Import/HOL4Compat.thy Thu Nov 18 17:01:16 2010 +0100
@@ -95,8 +95,8 @@
lemma PAIR: "(fst x,snd x) = x"
by simp
-lemma PAIR_MAP: "prod_fun f g p = (f (fst p),g (snd p))"
- by (simp add: prod_fun_def split_def)
+lemma PAIR_MAP: "map_pair f g p = (f (fst p),g (snd p))"
+ by (simp add: map_pair_def split_def)
lemma pair_case_def: "split = split"
..;
--- a/src/HOL/Library/Efficient_Nat.thy Thu Nov 18 17:01:16 2010 +0100
+++ b/src/HOL/Library/Efficient_Nat.thy Thu Nov 18 17:01:16 2010 +0100
@@ -51,8 +51,8 @@
unfolding of_nat_mult [symmetric] by simp
lemma divmod_nat_code [code]:
- "divmod_nat n m = prod_fun nat nat (pdivmod (of_nat n) (of_nat m))"
- by (simp add: prod_fun_def split_def pdivmod_def nat_div_distrib nat_mod_distrib divmod_nat_div_mod)
+ "divmod_nat n m = map_pair nat nat (pdivmod (of_nat n) (of_nat m))"
+ by (simp add: map_pair_def split_def pdivmod_def nat_div_distrib nat_mod_distrib divmod_nat_div_mod)
lemma eq_nat_code [code]:
"HOL.equal n m \<longleftrightarrow> HOL.equal (of_nat n \<Colon> int) (of_nat m)"
--- a/src/HOL/Library/Quotient_Product.thy Thu Nov 18 17:01:16 2010 +0100
+++ b/src/HOL/Library/Quotient_Product.thy Thu Nov 18 17:01:16 2010 +0100
@@ -13,7 +13,7 @@
where
"prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
-declare [[map prod = (prod_fun, prod_rel)]]
+declare [[map prod = (map_pair, prod_rel)]]
lemma prod_rel_apply [simp]:
"prod_rel R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
@@ -34,7 +34,7 @@
lemma prod_quotient[quot_thm]:
assumes q1: "Quotient R1 Abs1 Rep1"
assumes q2: "Quotient R2 Abs2 Rep2"
- shows "Quotient (prod_rel R1 R2) (prod_fun Abs1 Abs2) (prod_fun Rep1 Rep2)"
+ shows "Quotient (prod_rel R1 R2) (map_pair Abs1 Abs2) (map_pair Rep1 Rep2)"
unfolding Quotient_def
apply(simp add: split_paired_all)
apply(simp add: Quotient_abs_rep[OF q1] Quotient_rel_rep[OF q1])
@@ -53,7 +53,7 @@
lemma Pair_prs[quot_preserve]:
assumes q1: "Quotient R1 Abs1 Rep1"
assumes q2: "Quotient R2 Abs2 Rep2"
- shows "(Rep1 ---> Rep2 ---> (prod_fun Abs1 Abs2)) Pair = Pair"
+ shows "(Rep1 ---> Rep2 ---> (map_pair Abs1 Abs2)) Pair = Pair"
apply(simp add: fun_eq_iff)
apply(simp add: Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
done
@@ -67,7 +67,7 @@
lemma fst_prs[quot_preserve]:
assumes q1: "Quotient R1 Abs1 Rep1"
assumes q2: "Quotient R2 Abs2 Rep2"
- shows "(prod_fun Rep1 Rep2 ---> Abs1) fst = fst"
+ shows "(map_pair Rep1 Rep2 ---> Abs1) fst = fst"
by (simp add: fun_eq_iff Quotient_abs_rep[OF q1])
lemma snd_rsp[quot_respect]:
@@ -79,7 +79,7 @@
lemma snd_prs[quot_preserve]:
assumes q1: "Quotient R1 Abs1 Rep1"
assumes q2: "Quotient R2 Abs2 Rep2"
- shows "(prod_fun Rep1 Rep2 ---> Abs2) snd = snd"
+ shows "(map_pair Rep1 Rep2 ---> Abs2) snd = snd"
by (simp add: fun_eq_iff Quotient_abs_rep[OF q2])
lemma split_rsp[quot_respect]:
@@ -89,7 +89,7 @@
lemma split_prs[quot_preserve]:
assumes q1: "Quotient R1 Abs1 Rep1"
and q2: "Quotient R2 Abs2 Rep2"
- shows "(((Abs1 ---> Abs2 ---> id) ---> prod_fun Rep1 Rep2 ---> id) split) = split"
+ shows "(((Abs1 ---> Abs2 ---> id) ---> map_pair Rep1 Rep2 ---> id) split) = split"
by (simp add: fun_eq_iff Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
lemma [quot_respect]:
@@ -101,7 +101,7 @@
assumes q1: "Quotient R1 abs1 rep1"
and q2: "Quotient R2 abs2 rep2"
shows "((abs1 ---> abs1 ---> id) ---> (abs2 ---> abs2 ---> id) --->
- prod_fun rep1 rep2 ---> prod_fun rep1 rep2 ---> id) prod_rel = prod_rel"
+ map_pair rep1 rep2 ---> map_pair rep1 rep2 ---> id) prod_rel = prod_rel"
by (simp add: fun_eq_iff Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
lemma [quot_preserve]:
@@ -111,8 +111,8 @@
declare Pair_eq[quot_preserve]
-lemma prod_fun_id[id_simps]:
- shows "prod_fun id id = id"
+lemma map_pair_id[id_simps]:
+ shows "map_pair id id = id"
by (simp add: fun_eq_iff)
lemma prod_rel_eq[id_simps]:
--- a/src/HOL/Product_Type.thy Thu Nov 18 17:01:16 2010 +0100
+++ b/src/HOL/Product_Type.thy Thu Nov 18 17:01:16 2010 +0100
@@ -824,58 +824,63 @@
no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
text {*
- @{term prod_fun} --- action of the product functor upon
+ @{term map_pair} --- action of the product functor upon
functions.
*}
-definition prod_fun :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'd" where
- "prod_fun f g = (\<lambda>(x, y). (f x, g y))"
+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))"
-lemma prod_fun [simp, code]: "prod_fun f g (a, b) = (f a, g b)"
- by (simp add: prod_fun_def)
+lemma map_pair_simp [simp, code]:
+ "map_pair f g (a, b) = (f a, g b)"
+ by (simp add: map_pair_def)
-lemma fst_prod_fun[simp]: "fst (prod_fun f g x) = f (fst x)"
-by (cases x, auto)
+type_mapper map_pair
+ by (simp_all add: split_paired_all)
-lemma snd_prod_fun[simp]: "snd (prod_fun f g x) = g (snd x)"
-by (cases x, auto)
+lemma fst_map_pair [simp]:
+ "fst (map_pair f g x) = f (fst x)"
+ by (cases x) simp_all
-lemma fst_comp_prod_fun[simp]: "fst \<circ> prod_fun f g = f \<circ> fst"
-by (rule ext) auto
+lemma snd_prod_fun [simp]:
+ "snd (map_pair f g x) = g (snd x)"
+ by (cases x) simp_all
-lemma snd_comp_prod_fun[simp]: "snd \<circ> prod_fun f g = g \<circ> snd"
-by (rule ext) auto
-
+lemma fst_comp_map_pair [simp]:
+ "fst \<circ> map_pair f g = f \<circ> fst"
+ by (rule ext) simp_all
-lemma prod_fun_compose:
- "prod_fun (f1 o f2) (g1 o g2) = (prod_fun f1 g1 o prod_fun f2 g2)"
-by (rule ext) auto
+lemma snd_comp_map_pair [simp]:
+ "snd \<circ> map_pair f g = g \<circ> snd"
+ by (rule ext) simp_all
-lemma prod_fun_ident [simp]: "prod_fun (%x. x) (%y. y) = (%z. z)"
- by (rule ext) auto
+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 prod_fun_imageI [intro]: "(a, b) : r ==> (f a, g b) : prod_fun f g ` r"
- apply (rule image_eqI)
- apply (rule prod_fun [symmetric], assumption)
- done
+lemma map_pair_ident [simp]:
+ "map_pair (%x. x) (%y. y) = (%z. z)"
+ by (rule ext) (simp add: map_pair.identity)
+
+lemma map_pair_imageI [intro]:
+ "(a, b) \<in> R \<Longrightarrow> (f a, g b) \<in> map_pair f g ` R"
+ by (rule image_eqI) simp_all
lemma prod_fun_imageE [elim!]:
- assumes major: "c: (prod_fun f g)`r"
- and cases: "!!x y. [| c=(f(x),g(y)); (x,y):r |] ==> P"
+ assumes major: "c \<in> map_pair 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])
apply (case_tac x)
apply (rule cases)
- apply (blast intro: prod_fun)
- apply blast
+ apply simp_all
done
-
definition apfst :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'b" where
- "apfst f = prod_fun f id"
+ "apfst f = map_pair f id"
definition apsnd :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'c" where
- "apsnd f = prod_fun id f"
+ "apsnd f = map_pair id f"
lemma apfst_conv [simp, code]:
"apfst f (x, y) = (f x, y)"
@@ -941,7 +946,7 @@
Disjoint union of a family of sets -- Sigma.
*}
-definition Sigma :: "['a set, 'a => 'b set] => ('a \<times> 'b) set" where
+definition Sigma :: "['a set, 'a => 'b set] => ('a \<times> 'b) set" where
Sigma_def: "Sigma A B == UN x:A. UN y:B x. {Pair x y}"
abbreviation
@@ -1091,66 +1096,6 @@
lemma vimage_Times: "f -` (A \<times> B) = ((fst \<circ> f) -` A) \<inter> ((snd \<circ> f) -` B)"
by (auto, case_tac "f x", auto)
-text{* The following @{const prod_fun} lemmas are due to Joachim Breitner: *}
-
-lemma prod_fun_inj_on:
- assumes "inj_on f A" and "inj_on g B"
- shows "inj_on (prod_fun 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 "prod_fun f g x = prod_fun f g y"
- hence "fst (prod_fun f g x) = fst (prod_fun 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 `prod_fun f g x = prod_fun f g y`
- have "snd (prod_fun f g x) = snd (prod_fun 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 prod_fun_surj:
- assumes "surj f" and "surj g"
- shows "surj (prod_fun 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) = prod_fun f g (a,b)" by auto
- thus "\<exists>x. y = prod_fun f g x" by auto
-qed
-
-lemma prod_fun_surj_on:
- assumes "f ` A = A'" and "g ` B = B'"
- shows "prod_fun 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 = prod_fun f g x}"
- then obtain y where "y \<in> A \<times> B" and "x = prod_fun 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 = prod_fun 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
- from `image f A = A'` and `fst x \<in> A'` have "fst x \<in> image f A" by auto
- 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) = prod_fun 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 = prod_fun f g y" by auto
- thus "x \<in> {x. \<exists>y \<in> A \<times> B. x = prod_fun f g y}" by auto
-qed
-
lemma swap_inj_on:
"inj_on (\<lambda>(i, j). (j, i)) A"
by (auto intro!: inj_onI)
@@ -1167,6 +1112,66 @@
using * eq[symmetric] by auto
qed simp_all
+text {* The following @{const map_pair} lemmas are due to Joachim Breitner: *}
+
+lemma map_pair_inj_on:
+ assumes "inj_on f A" and "inj_on g B"
+ shows "inj_on (map_pair 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)
+ 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)
+ 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:
+ assumes "surj f" and "surj g"
+ shows "surj (map_pair 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
+qed
+
+lemma map_pair_surj_on:
+ assumes "f ` A = A'" and "g ` B = B'"
+ shows "map_pair 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
+ 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)
+next
+ fix x :: "'a \<times> 'c"
+ assume "x \<in> A' \<times> B'" hence "fst x \<in> A'" and "snd x \<in> B'" by auto
+ from `image f A = A'` and `fst x \<in> A'` have "fst x \<in> image f A" by auto
+ 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
+ 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
+qed
+
subsection {* Inductively defined sets *}
--- a/src/HOL/Wellfounded.thy Thu Nov 18 17:01:16 2010 +0100
+++ b/src/HOL/Wellfounded.thy Thu Nov 18 17:01:16 2010 +0100
@@ -240,7 +240,7 @@
text{*Well-foundedness of image*}
-lemma wf_prod_fun_image: "[| wf r; inj f |] ==> wf(prod_fun f f ` r)"
+lemma wf_map_pair_image: "[| wf r; inj f |] ==> wf(map_pair 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)