1.1 --- a/src/HOL/Bali/State.thy	Thu Nov 18 17:01:16 2010 +0100
     1.2 +++ b/src/HOL/Bali/State.thy	Thu Nov 18 17:01:16 2010 +0100
     1.3 @@ -631,11 +631,11 @@
     1.4  
     1.5  definition
     1.6    abupd :: "(abopt \<Rightarrow> abopt) \<Rightarrow> state \<Rightarrow> state"
     1.7 -  where "abupd f = prod_fun f id"
     1.8 +  where "abupd f = map_pair f id"
     1.9  
    1.10  definition
    1.11    supd :: "(st \<Rightarrow> st) \<Rightarrow> state \<Rightarrow> state"
    1.12 -  where "supd = prod_fun id"
    1.13 +  where "supd = map_pair id"
    1.14    
    1.15  lemma abupd_def2 [simp]: "abupd f (x,s) = (f x,s)"
    1.16  by (simp add: abupd_def)

     2.1 --- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Thu Nov 18 17:01:16 2010 +0100
     2.2 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Thu Nov 18 17:01:16 2010 +0100
     2.3 @@ -131,7 +131,7 @@
     2.4      SND       > snd
     2.5      CURRY     > curry
     2.6      UNCURRY   > split
     2.7 -    "##"      > prod_fun
     2.8 +    "##"      > map_pair
     2.9      pair_case > split;
    2.10  
    2.11  ignore_thms

     3.1 --- a/src/HOL/Import/HOL/pair.imp	Thu Nov 18 17:01:16 2010 +0100
     3.2 +++ b/src/HOL/Import/HOL/pair.imp	Thu Nov 18 17:01:16 2010 +0100
     3.3 @@ -18,7 +18,7 @@
     3.4    "LEX" > "HOL4Base.pair.LEX"
     3.5    "CURRY" > "Product_Type.curry"
     3.6    "," > "Product_Type.Pair"
     3.7 -  "##" > "prod_fun"
     3.8 +  "##" > "map_pair"
     3.9  
    3.10  thm_maps
    3.11    "pair_induction" > "Datatype.prod.induct_correctness"
    3.12 @@ -39,7 +39,7 @@
    3.13    "RPROD_DEF" > "HOL4Base.pair.RPROD_DEF"
    3.14    "PFORALL_THM" > "HOL4Base.pair.PFORALL_THM"
    3.15    "PEXISTS_THM" > "HOL4Base.pair.PEXISTS_THM"
    3.16 -  "PAIR_MAP_THM" > "Product_Type.prod_fun"
    3.17 +  "PAIR_MAP_THM" > "Product_Type.map_pair"
    3.18    "PAIR_MAP" > "HOL4Compat.PAIR_MAP"
    3.19    "PAIR_EQ" > "Datatype.prod.simps_1"
    3.20    "PAIR" > "HOL4Compat.PAIR"

     4.1 --- a/src/HOL/Import/HOL4Compat.thy	Thu Nov 18 17:01:16 2010 +0100
     4.2 +++ b/src/HOL/Import/HOL4Compat.thy	Thu Nov 18 17:01:16 2010 +0100
     4.3 @@ -95,8 +95,8 @@
     4.4  lemma PAIR: "(fst x,snd x) = x"
     4.5    by simp
     4.6  
     4.7 -lemma PAIR_MAP: "prod_fun f g p = (f (fst p),g (snd p))"
     4.8 -  by (simp add: prod_fun_def split_def)
     4.9 +lemma PAIR_MAP: "map_pair f g p = (f (fst p),g (snd p))"
    4.10 +  by (simp add: map_pair_def split_def)
    4.11  
    4.12  lemma pair_case_def: "split = split"
    4.13    ..;

     5.1 --- a/src/HOL/Library/Efficient_Nat.thy	Thu Nov 18 17:01:16 2010 +0100
     5.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Thu Nov 18 17:01:16 2010 +0100
     5.3 @@ -51,8 +51,8 @@
     5.4    unfolding of_nat_mult [symmetric] by simp
     5.5  
     5.6  lemma divmod_nat_code [code]:
     5.7 -  "divmod_nat n m = prod_fun nat nat (pdivmod (of_nat n) (of_nat m))"
     5.8 -  by (simp add: prod_fun_def split_def pdivmod_def nat_div_distrib nat_mod_distrib divmod_nat_div_mod)
     5.9 +  "divmod_nat n m = map_pair nat nat (pdivmod (of_nat n) (of_nat m))"
    5.10 +  by (simp add: map_pair_def split_def pdivmod_def nat_div_distrib nat_mod_distrib divmod_nat_div_mod)
    5.11  
    5.12  lemma eq_nat_code [code]:
    5.13    "HOL.equal n m \<longleftrightarrow> HOL.equal (of_nat n \<Colon> int) (of_nat m)"

     6.1 --- a/src/HOL/Library/Quotient_Product.thy	Thu Nov 18 17:01:16 2010 +0100
     6.2 +++ b/src/HOL/Library/Quotient_Product.thy	Thu Nov 18 17:01:16 2010 +0100
     6.3 @@ -13,7 +13,7 @@
     6.4  where
     6.5    "prod_rel R1 R2 = (\<lambda>(a, b) (c, d). R1 a c \<and> R2 b d)"
     6.6  
     6.7 -declare [[map prod = (prod_fun, prod_rel)]]
     6.8 +declare [[map prod = (map_pair, prod_rel)]]
     6.9  
    6.10  lemma prod_rel_apply [simp]:
    6.11    "prod_rel R1 R2 (a, b) (c, d) \<longleftrightarrow> R1 a c \<and> R2 b d"
    6.12 @@ -34,7 +34,7 @@
    6.13  lemma prod_quotient[quot_thm]:
    6.14    assumes q1: "Quotient R1 Abs1 Rep1"
    6.15    assumes q2: "Quotient R2 Abs2 Rep2"
    6.16 -  shows "Quotient (prod_rel R1 R2) (prod_fun Abs1 Abs2) (prod_fun Rep1 Rep2)"
    6.17 +  shows "Quotient (prod_rel R1 R2) (map_pair Abs1 Abs2) (map_pair Rep1 Rep2)"
    6.18    unfolding Quotient_def
    6.19    apply(simp add: split_paired_all)
    6.20    apply(simp add: Quotient_abs_rep[OF q1] Quotient_rel_rep[OF q1])
    6.21 @@ -53,7 +53,7 @@
    6.22  lemma Pair_prs[quot_preserve]:
    6.23    assumes q1: "Quotient R1 Abs1 Rep1"
    6.24    assumes q2: "Quotient R2 Abs2 Rep2"
    6.25 -  shows "(Rep1 ---> Rep2 ---> (prod_fun Abs1 Abs2)) Pair = Pair"
    6.26 +  shows "(Rep1 ---> Rep2 ---> (map_pair Abs1 Abs2)) Pair = Pair"
    6.27    apply(simp add: fun_eq_iff)
    6.28    apply(simp add: Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
    6.29    done
    6.30 @@ -67,7 +67,7 @@
    6.31  lemma fst_prs[quot_preserve]:
    6.32    assumes q1: "Quotient R1 Abs1 Rep1"
    6.33    assumes q2: "Quotient R2 Abs2 Rep2"
    6.34 -  shows "(prod_fun Rep1 Rep2 ---> Abs1) fst = fst"
    6.35 +  shows "(map_pair Rep1 Rep2 ---> Abs1) fst = fst"
    6.36    by (simp add: fun_eq_iff Quotient_abs_rep[OF q1])
    6.37  
    6.38  lemma snd_rsp[quot_respect]:
    6.39 @@ -79,7 +79,7 @@
    6.40  lemma snd_prs[quot_preserve]:
    6.41    assumes q1: "Quotient R1 Abs1 Rep1"
    6.42    assumes q2: "Quotient R2 Abs2 Rep2"
    6.43 -  shows "(prod_fun Rep1 Rep2 ---> Abs2) snd = snd"
    6.44 +  shows "(map_pair Rep1 Rep2 ---> Abs2) snd = snd"
    6.45    by (simp add: fun_eq_iff Quotient_abs_rep[OF q2])
    6.46  
    6.47  lemma split_rsp[quot_respect]:
    6.48 @@ -89,7 +89,7 @@
    6.49  lemma split_prs[quot_preserve]:
    6.50    assumes q1: "Quotient R1 Abs1 Rep1"
    6.51    and     q2: "Quotient R2 Abs2 Rep2"
    6.52 -  shows "(((Abs1 ---> Abs2 ---> id) ---> prod_fun Rep1 Rep2 ---> id) split) = split"
    6.53 +  shows "(((Abs1 ---> Abs2 ---> id) ---> map_pair Rep1 Rep2 ---> id) split) = split"
    6.54    by (simp add: fun_eq_iff Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
    6.55  
    6.56  lemma [quot_respect]:
    6.57 @@ -101,7 +101,7 @@
    6.58    assumes q1: "Quotient R1 abs1 rep1"
    6.59    and     q2: "Quotient R2 abs2 rep2"
    6.60    shows "((abs1 ---> abs1 ---> id) ---> (abs2 ---> abs2 ---> id) --->
    6.61 -  prod_fun rep1 rep2 ---> prod_fun rep1 rep2 ---> id) prod_rel = prod_rel"
    6.62 +  map_pair rep1 rep2 ---> map_pair rep1 rep2 ---> id) prod_rel = prod_rel"
    6.63    by (simp add: fun_eq_iff Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
    6.64  
    6.65  lemma [quot_preserve]:
    6.66 @@ -111,8 +111,8 @@
    6.67  
    6.68  declare Pair_eq[quot_preserve]
    6.69  
    6.70 -lemma prod_fun_id[id_simps]:
    6.71 -  shows "prod_fun id id = id"
    6.72 +lemma map_pair_id[id_simps]:
    6.73 +  shows "map_pair id id = id"
    6.74    by (simp add: fun_eq_iff)
    6.75  
    6.76  lemma prod_rel_eq[id_simps]:

     7.1 --- a/src/HOL/Product_Type.thy	Thu Nov 18 17:01:16 2010 +0100
     7.2 +++ b/src/HOL/Product_Type.thy	Thu Nov 18 17:01:16 2010 +0100
     7.3 @@ -824,58 +824,63 @@
     7.4  no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
     7.5  
     7.6  text {*
     7.7 -  @{term prod_fun} --- action of the product functor upon
     7.8 +  @{term map_pair} --- action of the product functor upon
     7.9    functions.
    7.10  *}
    7.11  
    7.12 -definition prod_fun :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'd" where
    7.13 -  "prod_fun f g = (\<lambda>(x, y). (f x, g y))"
    7.14 +definition map_pair :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'd" where
    7.15 +  "map_pair f g = (\<lambda>(x, y). (f x, g y))"
    7.16  
    7.17 -lemma prod_fun [simp, code]: "prod_fun f g (a, b) = (f a, g b)"
    7.18 -  by (simp add: prod_fun_def)
    7.19 +lemma map_pair_simp [simp, code]:
    7.20 +  "map_pair f g (a, b) = (f a, g b)"
    7.21 +  by (simp add: map_pair_def)
    7.22  
    7.23 -lemma fst_prod_fun[simp]: "fst (prod_fun f g x) = f (fst x)"
    7.24 -by (cases x, auto)
    7.25 +type_mapper map_pair
    7.26 +  by (simp_all add: split_paired_all)
    7.27  
    7.28 -lemma snd_prod_fun[simp]: "snd (prod_fun f g x) = g (snd x)"
    7.29 -by (cases x, auto)
    7.30 +lemma fst_map_pair [simp]:
    7.31 +  "fst (map_pair f g x) = f (fst x)"
    7.32 +  by (cases x) simp_all
    7.33  
    7.34 -lemma fst_comp_prod_fun[simp]: "fst \<circ> prod_fun f g = f \<circ> fst"
    7.35 -by (rule ext) auto
    7.36 +lemma snd_prod_fun [simp]:
    7.37 +  "snd (map_pair f g x) = g (snd x)"
    7.38 +  by (cases x) simp_all
    7.39  
    7.40 -lemma snd_comp_prod_fun[simp]: "snd \<circ> prod_fun f g = g \<circ> snd"
    7.41 -by (rule ext) auto
    7.42 +lemma fst_comp_map_pair [simp]:
    7.43 +  "fst \<circ> map_pair f g = f \<circ> fst"
    7.44 +  by (rule ext) simp_all
    7.45  
    7.46 +lemma snd_comp_map_pair [simp]:
    7.47 +  "snd \<circ> map_pair f g = g \<circ> snd"
    7.48 +  by (rule ext) simp_all
    7.49  
    7.50 -lemma prod_fun_compose:
    7.51 -  "prod_fun (f1 o f2) (g1 o g2) = (prod_fun f1 g1 o prod_fun f2 g2)"
    7.52 -by (rule ext) auto
    7.53 +lemma map_pair_compose:
    7.54 +  "map_pair (f1 o f2) (g1 o g2) = (map_pair f1 g1 o map_pair f2 g2)"
    7.55 +  by (rule ext) (simp add: map_pair.compositionality comp_def)
    7.56  
    7.57 -lemma prod_fun_ident [simp]: "prod_fun (%x. x) (%y. y) = (%z. z)"
    7.58 -  by (rule ext) auto
    7.59 +lemma map_pair_ident [simp]:
    7.60 +  "map_pair (%x. x) (%y. y) = (%z. z)"
    7.61 +  by (rule ext) (simp add: map_pair.identity)
    7.62  
    7.63 -lemma prod_fun_imageI [intro]: "(a, b) : r ==> (f a, g b) : prod_fun f g ` r"
    7.64 -  apply (rule image_eqI)
    7.65 -  apply (rule prod_fun [symmetric], assumption)
    7.66 -  done
    7.67 +lemma map_pair_imageI [intro]:
    7.68 +  "(a, b) \<in> R \<Longrightarrow> (f a, g b) \<in> map_pair f g ` R"
    7.69 +  by (rule image_eqI) simp_all
    7.70  
    7.71  lemma prod_fun_imageE [elim!]:
    7.72 -  assumes major: "c: (prod_fun f g)`r"
    7.73 -    and cases: "!!x y. [| c=(f(x),g(y));  (x,y):r |] ==> P"
    7.74 +  assumes major: "c \<in> map_pair f g ` R"
    7.75 +    and cases: "\<And>x y. c = (f x, g y) \<Longrightarrow> (x, y) \<in> R \<Longrightarrow> P"
    7.76    shows P
    7.77    apply (rule major [THEN imageE])
    7.78    apply (case_tac x)
    7.79    apply (rule cases)
    7.80 -   apply (blast intro: prod_fun)
    7.81 -  apply blast
    7.82 +  apply simp_all
    7.83    done
    7.84  
    7.85 -
    7.86  definition apfst :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'b" where
    7.87 -  "apfst f = prod_fun f id"
    7.88 +  "apfst f = map_pair f id"
    7.89  
    7.90  definition apsnd :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'c" where
    7.91 -  "apsnd f = prod_fun id f"
    7.92 +  "apsnd f = map_pair id f"
    7.93  
    7.94  lemma apfst_conv [simp, code]:
    7.95    "apfst f (x, y) = (f x, y)" 
    7.96 @@ -941,7 +946,7 @@
    7.97    Disjoint union of a family of sets -- Sigma.
    7.98  *}
    7.99  
   7.100 -definition  Sigma :: "['a set, 'a => 'b set] => ('a \<times> 'b) set" where
   7.101 +definition Sigma :: "['a set, 'a => 'b set] => ('a \<times> 'b) set" where
   7.102    Sigma_def: "Sigma A B == UN x:A. UN y:B x. {Pair x y}"
   7.103  
   7.104  abbreviation
   7.105 @@ -1091,66 +1096,6 @@
   7.106  lemma vimage_Times: "f -` (A \<times> B) = ((fst \<circ> f) -` A) \<inter> ((snd \<circ> f) -` B)"
   7.107    by (auto, case_tac "f x", auto)
   7.108  
   7.109 -text{* The following @{const prod_fun} lemmas are due to Joachim Breitner: *}
   7.110 -
   7.111 -lemma prod_fun_inj_on:
   7.112 -  assumes "inj_on f A" and "inj_on g B"
   7.113 -  shows "inj_on (prod_fun f g) (A \<times> B)"
   7.114 -proof (rule inj_onI)
   7.115 -  fix x :: "'a \<times> 'c" and y :: "'a \<times> 'c"
   7.116 -  assume "x \<in> A \<times> B" hence "fst x \<in> A" and "snd x \<in> B" by auto
   7.117 -  assume "y \<in> A \<times> B" hence "fst y \<in> A" and "snd y \<in> B" by auto
   7.118 -  assume "prod_fun f g x = prod_fun f g y"
   7.119 -  hence "fst (prod_fun f g x) = fst (prod_fun f g y)" by (auto)
   7.120 -  hence "f (fst x) = f (fst y)" by (cases x,cases y,auto)
   7.121 -  with `inj_on f A` and `fst x \<in> A` and `fst y \<in> A`
   7.122 -  have "fst x = fst y" by (auto dest:dest:inj_onD)
   7.123 -  moreover from `prod_fun f g x = prod_fun f g y`
   7.124 -  have "snd (prod_fun f g x) = snd (prod_fun f g y)" by (auto)
   7.125 -  hence "g (snd x) = g (snd y)" by (cases x,cases y,auto)
   7.126 -  with `inj_on g B` and `snd x \<in> B` and `snd y \<in> B`
   7.127 -  have "snd x = snd y" by (auto dest:dest:inj_onD)
   7.128 -  ultimately show "x = y" by(rule prod_eqI)
   7.129 -qed
   7.130 -
   7.131 -lemma prod_fun_surj:
   7.132 -  assumes "surj f" and "surj g"
   7.133 -  shows "surj (prod_fun f g)"
   7.134 -unfolding surj_def
   7.135 -proof
   7.136 -  fix y :: "'b \<times> 'd"
   7.137 -  from `surj f` obtain a where "fst y = f a" by (auto elim:surjE)
   7.138 -  moreover
   7.139 -  from `surj g` obtain b where "snd y = g b" by (auto elim:surjE)
   7.140 -  ultimately have "(fst y, snd y) = prod_fun f g (a,b)" by auto
   7.141 -  thus "\<exists>x. y = prod_fun f g x" by auto
   7.142 -qed
   7.143 -
   7.144 -lemma prod_fun_surj_on:
   7.145 -  assumes "f ` A = A'" and "g ` B = B'"
   7.146 -  shows "prod_fun f g ` (A \<times> B) = A' \<times> B'"
   7.147 -unfolding image_def
   7.148 -proof(rule set_eqI,rule iffI)
   7.149 -  fix x :: "'a \<times> 'c"
   7.150 -  assume "x \<in> {y\<Colon>'a \<times> 'c. \<exists>x\<Colon>'b \<times> 'd\<in>A \<times> B. y = prod_fun f g x}"
   7.151 -  then obtain y where "y \<in> A \<times> B" and "x = prod_fun f g y" by blast
   7.152 -  from `image f A = A'` and `y \<in> A \<times> B` have "f (fst y) \<in> A'" by auto
   7.153 -  moreover from `image g B = B'` and `y \<in> A \<times> B` have "g (snd y) \<in> B'" by auto
   7.154 -  ultimately have "(f (fst y), g (snd y)) \<in> (A' \<times> B')" by auto
   7.155 -  with `x = prod_fun f g y` show "x \<in> A' \<times> B'" by (cases y, auto)
   7.156 -next
   7.157 -  fix x :: "'a \<times> 'c"
   7.158 -  assume "x \<in> A' \<times> B'" hence "fst x \<in> A'" and "snd x \<in> B'" by auto
   7.159 -  from `image f A = A'` and `fst x \<in> A'` have "fst x \<in> image f A" by auto
   7.160 -  then obtain a where "a \<in> A" and "fst x = f a" by (rule imageE)
   7.161 -  moreover from `image g B = B'` and `snd x \<in> B'`
   7.162 -  obtain b where "b \<in> B" and "snd x = g b" by auto
   7.163 -  ultimately have "(fst x, snd x) = prod_fun f g (a,b)" by auto
   7.164 -  moreover from `a \<in> A` and  `b \<in> B` have "(a , b) \<in> A \<times> B" by auto
   7.165 -  ultimately have "\<exists>y \<in> A \<times> B. x = prod_fun f g y" by auto
   7.166 -  thus "x \<in> {x. \<exists>y \<in> A \<times> B. x = prod_fun f g y}" by auto
   7.167 -qed
   7.168 -
   7.169  lemma swap_inj_on:
   7.170    "inj_on (\<lambda>(i, j). (j, i)) A"
   7.171    by (auto intro!: inj_onI)
   7.172 @@ -1167,6 +1112,66 @@
   7.173      using * eq[symmetric] by auto
   7.174  qed simp_all
   7.175  
   7.176 +text {* The following @{const map_pair} lemmas are due to Joachim Breitner: *}
   7.177 +
   7.178 +lemma map_pair_inj_on:
   7.179 +  assumes "inj_on f A" and "inj_on g B"
   7.180 +  shows "inj_on (map_pair f g) (A \<times> B)"
   7.181 +proof (rule inj_onI)
   7.182 +  fix x :: "'a \<times> 'c" and y :: "'a \<times> 'c"
   7.183 +  assume "x \<in> A \<times> B" hence "fst x \<in> A" and "snd x \<in> B" by auto
   7.184 +  assume "y \<in> A \<times> B" hence "fst y \<in> A" and "snd y \<in> B" by auto
   7.185 +  assume "map_pair f g x = map_pair f g y"
   7.186 +  hence "fst (map_pair f g x) = fst (map_pair f g y)" by (auto)
   7.187 +  hence "f (fst x) = f (fst y)" by (cases x,cases y,auto)
   7.188 +  with `inj_on f A` and `fst x \<in> A` and `fst y \<in> A`
   7.189 +  have "fst x = fst y" by (auto dest:dest:inj_onD)
   7.190 +  moreover from `map_pair f g x = map_pair f g y`
   7.191 +  have "snd (map_pair f g x) = snd (map_pair f g y)" by (auto)
   7.192 +  hence "g (snd x) = g (snd y)" by (cases x,cases y,auto)
   7.193 +  with `inj_on g B` and `snd x \<in> B` and `snd y \<in> B`
   7.194 +  have "snd x = snd y" by (auto dest:dest:inj_onD)
   7.195 +  ultimately show "x = y" by(rule prod_eqI)
   7.196 +qed
   7.197 +
   7.198 +lemma map_pair_surj:
   7.199 +  assumes "surj f" and "surj g"
   7.200 +  shows "surj (map_pair f g)"
   7.201 +unfolding surj_def
   7.202 +proof
   7.203 +  fix y :: "'b \<times> 'd"
   7.204 +  from `surj f` obtain a where "fst y = f a" by (auto elim:surjE)
   7.205 +  moreover
   7.206 +  from `surj g` obtain b where "snd y = g b" by (auto elim:surjE)
   7.207 +  ultimately have "(fst y, snd y) = map_pair f g (a,b)" by auto
   7.208 +  thus "\<exists>x. y = map_pair f g x" by auto
   7.209 +qed
   7.210 +
   7.211 +lemma map_pair_surj_on:
   7.212 +  assumes "f ` A = A'" and "g ` B = B'"
   7.213 +  shows "map_pair f g ` (A \<times> B) = A' \<times> B'"
   7.214 +unfolding image_def
   7.215 +proof(rule set_eqI,rule iffI)
   7.216 +  fix x :: "'a \<times> 'c"
   7.217 +  assume "x \<in> {y\<Colon>'a \<times> 'c. \<exists>x\<Colon>'b \<times> 'd\<in>A \<times> B. y = map_pair f g x}"
   7.218 +  then obtain y where "y \<in> A \<times> B" and "x = map_pair f g y" by blast
   7.219 +  from `image f A = A'` and `y \<in> A \<times> B` have "f (fst y) \<in> A'" by auto
   7.220 +  moreover from `image g B = B'` and `y \<in> A \<times> B` have "g (snd y) \<in> B'" by auto
   7.221 +  ultimately have "(f (fst y), g (snd y)) \<in> (A' \<times> B')" by auto
   7.222 +  with `x = map_pair f g y` show "x \<in> A' \<times> B'" by (cases y, auto)
   7.223 +next
   7.224 +  fix x :: "'a \<times> 'c"
   7.225 +  assume "x \<in> A' \<times> B'" hence "fst x \<in> A'" and "snd x \<in> B'" by auto
   7.226 +  from `image f A = A'` and `fst x \<in> A'` have "fst x \<in> image f A" by auto
   7.227 +  then obtain a where "a \<in> A" and "fst x = f a" by (rule imageE)
   7.228 +  moreover from `image g B = B'` and `snd x \<in> B'`
   7.229 +  obtain b where "b \<in> B" and "snd x = g b" by auto
   7.230 +  ultimately have "(fst x, snd x) = map_pair f g (a,b)" by auto
   7.231 +  moreover from `a \<in> A` and  `b \<in> B` have "(a , b) \<in> A \<times> B" by auto
   7.232 +  ultimately have "\<exists>y \<in> A \<times> B. x = map_pair f g y" by auto
   7.233 +  thus "x \<in> {x. \<exists>y \<in> A \<times> B. x = map_pair f g y}" by auto
   7.234 +qed
   7.235 +
   7.236  
   7.237  subsection {* Inductively defined sets *}
   7.238  

     8.1 --- a/src/HOL/Wellfounded.thy	Thu Nov 18 17:01:16 2010 +0100
     8.2 +++ b/src/HOL/Wellfounded.thy	Thu Nov 18 17:01:16 2010 +0100
     8.3 @@ -240,7 +240,7 @@
     8.4  
     8.5  text{*Well-foundedness of image*}
     8.6  
     8.7 -lemma wf_prod_fun_image: "[| wf r; inj f |] ==> wf(prod_fun f f ` r)"
     8.8 +lemma wf_map_pair_image: "[| wf r; inj f |] ==> wf(map_pair f f ` r)"
     8.9  apply (simp only: wf_eq_minimal, clarify)
    8.10  apply (case_tac "EX p. f p : Q")
    8.11  apply (erule_tac x = "{p. f p : Q}" in allE)