# HG changeset patch # User haftmann # Date 1290096076 -3600 # Node ID 30d512bf47a7d8cbc0abf62a8baaef652520d174 # Parent af1a0b0c6202f7c1c6e77dae01be8e0967b3a2c5 map_pair replaces prod_fun diff -r af1a0b0c6202 -r 30d512bf47a7 src/HOL/Bali/State.thy --- 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 \ abopt) \ state \ state" - where "abupd f = prod_fun f id" + where "abupd f = map_pair f id" definition supd :: "(st \ st) \ state \ 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) diff -r af1a0b0c6202 -r 30d512bf47a7 src/HOL/Import/Generate-HOL/GenHOL4Base.thy --- 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 diff -r af1a0b0c6202 -r 30d512bf47a7 src/HOL/Import/HOL/pair.imp --- 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" diff -r af1a0b0c6202 -r 30d512bf47a7 src/HOL/Import/HOL4Compat.thy --- 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" ..; diff -r af1a0b0c6202 -r 30d512bf47a7 src/HOL/Library/Efficient_Nat.thy --- 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 \ HOL.equal (of_nat n \ int) (of_nat m)" diff -r af1a0b0c6202 -r 30d512bf47a7 src/HOL/Library/Quotient_Product.thy --- 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 = (\(a, b) (c, d). R1 a c \ 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) \ R1 a c \ 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]: diff -r af1a0b0c6202 -r 30d512bf47a7 src/HOL/Product_Type.thy --- 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 "\\" 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 \ 'c) \ ('b \ 'd) \ 'a \ 'b \ 'c \ 'd" where - "prod_fun f g = (\(x, y). (f x, g y))" +definition map_pair :: "('a \ 'c) \ ('b \ 'd) \ 'a \ 'b \ 'c \ 'd" where + "map_pair f g = (\(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 \ prod_fun f g = f \ 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 \ prod_fun f g = g \ snd" -by (rule ext) auto - +lemma fst_comp_map_pair [simp]: + "fst \ map_pair f g = f \ 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 \ map_pair f g = g \ 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) \ R \ (f a, g b) \ 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 \ map_pair f g ` R" + and cases: "\x y. c = (f x, g y) \ (x, y) \ R \ 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 \ 'c) \ 'a \ 'b \ 'c \ 'b" where - "apfst f = prod_fun f id" + "apfst f = map_pair f id" definition apsnd :: "('b \ 'c) \ 'a \ 'b \ 'a \ '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 \ 'b) set" where +definition Sigma :: "['a set, 'a => 'b set] => ('a \ '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 \ B) = ((fst \ f) -` A) \ ((snd \ 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 \ 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 "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 \ A` and `fst y \ 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 \ 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 prod_fun_surj: - assumes "surj f" and "surj g" - shows "surj (prod_fun 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) = prod_fun f g (a,b)" by auto - thus "\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 \ 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 = prod_fun f g x}" - then obtain y where "y \ A \ B" and "x = prod_fun 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 = prod_fun 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 - from `image f A = A'` and `fst x \ A'` have "fst x \ image f A" by auto - 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) = prod_fun 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 = prod_fun f g y" by auto - thus "x \ {x. \y \ A \ B. x = prod_fun f g y}" by auto -qed - lemma swap_inj_on: "inj_on (\(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 \ 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) + 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) + 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: + assumes "surj f" and "surj g" + shows "surj (map_pair 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 +qed + +lemma map_pair_surj_on: + assumes "f ` A = A'" and "g ` B = B'" + shows "map_pair 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 + 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) +next + fix x :: "'a \ 'c" + assume "x \ A' \ B'" hence "fst x \ A'" and "snd x \ B'" by auto + from `image f A = A'` and `fst x \ A'` have "fst x \ image f A" by auto + 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 + 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 +qed + subsection {* Inductively defined sets *} diff -r af1a0b0c6202 -r 30d512bf47a7 src/HOL/Wellfounded.thy --- 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)