1.1 --- a/src/HOL/Product_Type.thy Wed Jun 02 11:53:17 2010 +0200
1.2 +++ b/src/HOL/Product_Type.thy Wed Jun 02 12:40:25 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)