1.1 --- a/src/HOL/Product_Type.thy	Wed Jun 02 08:01:45 2010 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Wed Jun 02 12:40:12 2010 +0200
     1.3 @@ -856,8 +856,22 @@
     1.4  lemma prod_fun [simp, code]: "prod_fun f g (a, b) = (f a, g b)"
     1.5    by (simp add: prod_fun_def)
     1.6  
     1.7 -lemma prod_fun_compose: "prod_fun (f1 o f2) (g1 o g2) = (prod_fun f1 g1 o prod_fun f2 g2)"
     1.8 -  by (rule ext) auto
     1.9 +lemma fst_prod_fun[simp]: "fst (prod_fun f g x) = f (fst x)"
    1.10 +by (cases x, auto)
    1.11 +
    1.12 +lemma snd_prod_fun[simp]: "snd (prod_fun f g x) = g (snd x)"
    1.13 +by (cases x, auto)
    1.14 +
    1.15 +lemma fst_comp_prod_fun[simp]: "fst \<circ> prod_fun f g = f \<circ> fst"
    1.16 +by (rule ext) auto
    1.17 +
    1.18 +lemma snd_comp_prod_fun[simp]: "snd \<circ> prod_fun f g = g \<circ> snd"
    1.19 +by (rule ext) auto
    1.20 +
    1.21 +
    1.22 +lemma prod_fun_compose:
    1.23 +  "prod_fun (f1 o f2) (g1 o g2) = (prod_fun f1 g1 o prod_fun f2 g2)"
    1.24 +by (rule ext) auto
    1.25  
    1.26  lemma prod_fun_ident [simp]: "prod_fun (%x. x) (%y. y) = (%z. z)"
    1.27    by (rule ext) auto
    1.28 @@ -878,6 +892,7 @@
    1.29    apply blast
    1.30    done
    1.31  
    1.32 +
    1.33  definition apfst :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'b" where
    1.34    "apfst f = prod_fun f id"
    1.35  
    1.36 @@ -1098,6 +1113,66 @@
    1.37  lemma vimage_Times: "f -` (A \<times> B) = ((fst \<circ> f) -` A) \<inter> ((snd \<circ> f) -` B)"
    1.38    by (auto, case_tac "f x", auto)
    1.39  
    1.40 +text{* The following @{const prod_fun} lemmas are due to Joachim Breitner: *}
    1.41 +
    1.42 +lemma prod_fun_inj_on:
    1.43 +  assumes "inj_on f A" and "inj_on g B"
    1.44 +  shows "inj_on (prod_fun f g) (A \<times> B)"
    1.45 +proof (rule inj_onI)
    1.46 +  fix x :: "'a \<times> 'c" and y :: "'a \<times> 'c"
    1.47 +  assume "x \<in> A \<times> B" hence "fst x \<in> A" and "snd x \<in> B" by auto
    1.48 +  assume "y \<in> A \<times> B" hence "fst y \<in> A" and "snd y \<in> B" by auto
    1.49 +  assume "prod_fun f g x = prod_fun f g y"
    1.50 +  hence "fst (prod_fun f g x) = fst (prod_fun f g y)" by (auto)
    1.51 +  hence "f (fst x) = f (fst y)" by (cases x,cases y,auto)
    1.52 +  with `inj_on f A` and `fst x \<in> A` and `fst y \<in> A`
    1.53 +  have "fst x = fst y" by (auto dest:dest:inj_onD)
    1.54 +  moreover from `prod_fun f g x = prod_fun f g y`
    1.55 +  have "snd (prod_fun f g x) = snd (prod_fun f g y)" by (auto)
    1.56 +  hence "g (snd x) = g (snd y)" by (cases x,cases y,auto)
    1.57 +  with `inj_on g B` and `snd x \<in> B` and `snd y \<in> B`
    1.58 +  have "snd x = snd y" by (auto dest:dest:inj_onD)
    1.59 +  ultimately show "x = y" by(rule prod_eqI)
    1.60 +qed
    1.61 +
    1.62 +lemma prod_fun_surj:
    1.63 +  assumes "surj f" and "surj g"
    1.64 +  shows "surj (prod_fun f g)"
    1.65 +unfolding surj_def
    1.66 +proof
    1.67 +  fix y :: "'b \<times> 'd"
    1.68 +  from `surj f` obtain a where "fst y = f a" by (auto elim:surjE)
    1.69 +  moreover
    1.70 +  from `surj g` obtain b where "snd y = g b" by (auto elim:surjE)
    1.71 +  ultimately have "(fst y, snd y) = prod_fun f g (a,b)" by auto
    1.72 +  thus "\<exists>x. y = prod_fun f g x" by auto
    1.73 +qed
    1.74 +
    1.75 +lemma prod_fun_surj_on:
    1.76 +  assumes "f ` A = A'" and "g ` B = B'"
    1.77 +  shows "prod_fun f g ` (A \<times> B) = A' \<times> B'"
    1.78 +unfolding image_def
    1.79 +proof(rule set_ext,rule iffI)
    1.80 +  fix x :: "'a \<times> 'c"
    1.81 +  assume "x \<in> {y\<Colon>'a \<times> 'c. \<exists>x\<Colon>'b \<times> 'd\<in>A \<times> B. y = prod_fun f g x}"
    1.82 +  then obtain y where "y \<in> A \<times> B" and "x = prod_fun f g y" by blast
    1.83 +  from `image f A = A'` and `y \<in> A \<times> B` have "f (fst y) \<in> A'" by auto
    1.84 +  moreover from `image g B = B'` and `y \<in> A \<times> B` have "g (snd y) \<in> B'" by auto
    1.85 +  ultimately have "(f (fst y), g (snd y)) \<in> (A' \<times> B')" by auto
    1.86 +  with `x = prod_fun f g y` show "x \<in> A' \<times> B'" by (cases y, auto)
    1.87 +next
    1.88 +  fix x :: "'a \<times> 'c"
    1.89 +  assume "x \<in> A' \<times> B'" hence "fst x \<in> A'" and "snd x \<in> B'" by auto
    1.90 +  from `image f A = A'` and `fst x \<in> A'` have "fst x \<in> image f A" by auto
    1.91 +  then obtain a where "a \<in> A" and "fst x = f a" by (rule imageE)
    1.92 +  moreover from `image g B = B'` and `snd x \<in> B'`
    1.93 +  obtain b where "b \<in> B" and "snd x = g b" by auto
    1.94 +  ultimately have "(fst x, snd x) = prod_fun f g (a,b)" by auto
    1.95 +  moreover from `a \<in> A` and  `b \<in> B` have "(a , b) \<in> A \<times> B" by auto
    1.96 +  ultimately have "\<exists>y \<in> A \<times> B. x = prod_fun f g y" by auto
    1.97 +  thus "x \<in> {x. \<exists>y \<in> A \<times> B. x = prod_fun f g y}" by auto
    1.98 +qed
    1.99 +
   1.100  lemma swap_inj_on:
   1.101    "inj_on (\<lambda>(i, j). (j, i)) A"
   1.102    by (auto intro!: inj_onI)