src/HOL/Product_Type.thy
changeset 40607 30d512bf47a7
parent 40590 b994d855dbd2
child 40702 cf26dd7395e4
     1.1 --- a/src/HOL/Product_Type.thy	Thu Nov 18 17:01:16 2010 +0100
     1.2 +++ b/src/HOL/Product_Type.thy	Thu Nov 18 17:01:16 2010 +0100
     1.3 @@ -824,58 +824,63 @@
     1.4  no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
     1.5  
     1.6  text {*
     1.7 -  @{term prod_fun} --- action of the product functor upon
     1.8 +  @{term map_pair} --- action of the product functor upon
     1.9    functions.
    1.10  *}
    1.11  
    1.12 -definition prod_fun :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'd" where
    1.13 -  "prod_fun f g = (\<lambda>(x, y). (f x, g y))"
    1.14 +definition map_pair :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'd" where
    1.15 +  "map_pair f g = (\<lambda>(x, y). (f x, g y))"
    1.16  
    1.17 -lemma prod_fun [simp, code]: "prod_fun f g (a, b) = (f a, g b)"
    1.18 -  by (simp add: prod_fun_def)
    1.19 +lemma map_pair_simp [simp, code]:
    1.20 +  "map_pair f g (a, b) = (f a, g b)"
    1.21 +  by (simp add: map_pair_def)
    1.22  
    1.23 -lemma fst_prod_fun[simp]: "fst (prod_fun f g x) = f (fst x)"
    1.24 -by (cases x, auto)
    1.25 +type_mapper map_pair
    1.26 +  by (simp_all add: split_paired_all)
    1.27  
    1.28 -lemma snd_prod_fun[simp]: "snd (prod_fun f g x) = g (snd x)"
    1.29 -by (cases x, auto)
    1.30 +lemma fst_map_pair [simp]:
    1.31 +  "fst (map_pair f g x) = f (fst x)"
    1.32 +  by (cases x) simp_all
    1.33  
    1.34 -lemma fst_comp_prod_fun[simp]: "fst \<circ> prod_fun f g = f \<circ> fst"
    1.35 -by (rule ext) auto
    1.36 +lemma snd_prod_fun [simp]:
    1.37 +  "snd (map_pair f g x) = g (snd x)"
    1.38 +  by (cases x) simp_all
    1.39  
    1.40 -lemma snd_comp_prod_fun[simp]: "snd \<circ> prod_fun f g = g \<circ> snd"
    1.41 -by (rule ext) auto
    1.42 -
    1.43 +lemma fst_comp_map_pair [simp]:
    1.44 +  "fst \<circ> map_pair f g = f \<circ> fst"
    1.45 +  by (rule ext) simp_all
    1.46  
    1.47 -lemma prod_fun_compose:
    1.48 -  "prod_fun (f1 o f2) (g1 o g2) = (prod_fun f1 g1 o prod_fun f2 g2)"
    1.49 -by (rule ext) auto
    1.50 +lemma snd_comp_map_pair [simp]:
    1.51 +  "snd \<circ> map_pair f g = g \<circ> snd"
    1.52 +  by (rule ext) simp_all
    1.53  
    1.54 -lemma prod_fun_ident [simp]: "prod_fun (%x. x) (%y. y) = (%z. z)"
    1.55 -  by (rule ext) auto
    1.56 +lemma map_pair_compose:
    1.57 +  "map_pair (f1 o f2) (g1 o g2) = (map_pair f1 g1 o map_pair f2 g2)"
    1.58 +  by (rule ext) (simp add: map_pair.compositionality comp_def)
    1.59  
    1.60 -lemma prod_fun_imageI [intro]: "(a, b) : r ==> (f a, g b) : prod_fun f g ` r"
    1.61 -  apply (rule image_eqI)
    1.62 -  apply (rule prod_fun [symmetric], assumption)
    1.63 -  done
    1.64 +lemma map_pair_ident [simp]:
    1.65 +  "map_pair (%x. x) (%y. y) = (%z. z)"
    1.66 +  by (rule ext) (simp add: map_pair.identity)
    1.67 +
    1.68 +lemma map_pair_imageI [intro]:
    1.69 +  "(a, b) \<in> R \<Longrightarrow> (f a, g b) \<in> map_pair f g ` R"
    1.70 +  by (rule image_eqI) simp_all
    1.71  
    1.72  lemma prod_fun_imageE [elim!]:
    1.73 -  assumes major: "c: (prod_fun f g)`r"
    1.74 -    and cases: "!!x y. [| c=(f(x),g(y));  (x,y):r |] ==> P"
    1.75 +  assumes major: "c \<in> map_pair f g ` R"
    1.76 +    and cases: "\<And>x y. c = (f x, g y) \<Longrightarrow> (x, y) \<in> R \<Longrightarrow> P"
    1.77    shows P
    1.78    apply (rule major [THEN imageE])
    1.79    apply (case_tac x)
    1.80    apply (rule cases)
    1.81 -   apply (blast intro: prod_fun)
    1.82 -  apply blast
    1.83 +  apply simp_all
    1.84    done
    1.85  
    1.86 -
    1.87  definition apfst :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'b" where
    1.88 -  "apfst f = prod_fun f id"
    1.89 +  "apfst f = map_pair f id"
    1.90  
    1.91  definition apsnd :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> 'c" where
    1.92 -  "apsnd f = prod_fun id f"
    1.93 +  "apsnd f = map_pair id f"
    1.94  
    1.95  lemma apfst_conv [simp, code]:
    1.96    "apfst f (x, y) = (f x, y)" 
    1.97 @@ -941,7 +946,7 @@
    1.98    Disjoint union of a family of sets -- Sigma.
    1.99  *}
   1.100  
   1.101 -definition  Sigma :: "['a set, 'a => 'b set] => ('a \<times> 'b) set" where
   1.102 +definition Sigma :: "['a set, 'a => 'b set] => ('a \<times> 'b) set" where
   1.103    Sigma_def: "Sigma A B == UN x:A. UN y:B x. {Pair x y}"
   1.104  
   1.105  abbreviation
   1.106 @@ -1091,66 +1096,6 @@
   1.107  lemma vimage_Times: "f -` (A \<times> B) = ((fst \<circ> f) -` A) \<inter> ((snd \<circ> f) -` B)"
   1.108    by (auto, case_tac "f x", auto)
   1.109  
   1.110 -text{* The following @{const prod_fun} lemmas are due to Joachim Breitner: *}
   1.111 -
   1.112 -lemma prod_fun_inj_on:
   1.113 -  assumes "inj_on f A" and "inj_on g B"
   1.114 -  shows "inj_on (prod_fun f g) (A \<times> B)"
   1.115 -proof (rule inj_onI)
   1.116 -  fix x :: "'a \<times> 'c" and y :: "'a \<times> 'c"
   1.117 -  assume "x \<in> A \<times> B" hence "fst x \<in> A" and "snd x \<in> B" by auto
   1.118 -  assume "y \<in> A \<times> B" hence "fst y \<in> A" and "snd y \<in> B" by auto
   1.119 -  assume "prod_fun f g x = prod_fun f g y"
   1.120 -  hence "fst (prod_fun f g x) = fst (prod_fun f g y)" by (auto)
   1.121 -  hence "f (fst x) = f (fst y)" by (cases x,cases y,auto)
   1.122 -  with `inj_on f A` and `fst x \<in> A` and `fst y \<in> A`
   1.123 -  have "fst x = fst y" by (auto dest:dest:inj_onD)
   1.124 -  moreover from `prod_fun f g x = prod_fun f g y`
   1.125 -  have "snd (prod_fun f g x) = snd (prod_fun f g y)" by (auto)
   1.126 -  hence "g (snd x) = g (snd y)" by (cases x,cases y,auto)
   1.127 -  with `inj_on g B` and `snd x \<in> B` and `snd y \<in> B`
   1.128 -  have "snd x = snd y" by (auto dest:dest:inj_onD)
   1.129 -  ultimately show "x = y" by(rule prod_eqI)
   1.130 -qed
   1.131 -
   1.132 -lemma prod_fun_surj:
   1.133 -  assumes "surj f" and "surj g"
   1.134 -  shows "surj (prod_fun f g)"
   1.135 -unfolding surj_def
   1.136 -proof
   1.137 -  fix y :: "'b \<times> 'd"
   1.138 -  from `surj f` obtain a where "fst y = f a" by (auto elim:surjE)
   1.139 -  moreover
   1.140 -  from `surj g` obtain b where "snd y = g b" by (auto elim:surjE)
   1.141 -  ultimately have "(fst y, snd y) = prod_fun f g (a,b)" by auto
   1.142 -  thus "\<exists>x. y = prod_fun f g x" by auto
   1.143 -qed
   1.144 -
   1.145 -lemma prod_fun_surj_on:
   1.146 -  assumes "f ` A = A'" and "g ` B = B'"
   1.147 -  shows "prod_fun f g ` (A \<times> B) = A' \<times> B'"
   1.148 -unfolding image_def
   1.149 -proof(rule set_eqI,rule iffI)
   1.150 -  fix x :: "'a \<times> 'c"
   1.151 -  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.152 -  then obtain y where "y \<in> A \<times> B" and "x = prod_fun f g y" by blast
   1.153 -  from `image f A = A'` and `y \<in> A \<times> B` have "f (fst y) \<in> A'" by auto
   1.154 -  moreover from `image g B = B'` and `y \<in> A \<times> B` have "g (snd y) \<in> B'" by auto
   1.155 -  ultimately have "(f (fst y), g (snd y)) \<in> (A' \<times> B')" by auto
   1.156 -  with `x = prod_fun f g y` show "x \<in> A' \<times> B'" by (cases y, auto)
   1.157 -next
   1.158 -  fix x :: "'a \<times> 'c"
   1.159 -  assume "x \<in> A' \<times> B'" hence "fst x \<in> A'" and "snd x \<in> B'" by auto
   1.160 -  from `image f A = A'` and `fst x \<in> A'` have "fst x \<in> image f A" by auto
   1.161 -  then obtain a where "a \<in> A" and "fst x = f a" by (rule imageE)
   1.162 -  moreover from `image g B = B'` and `snd x \<in> B'`
   1.163 -  obtain b where "b \<in> B" and "snd x = g b" by auto
   1.164 -  ultimately have "(fst x, snd x) = prod_fun f g (a,b)" by auto
   1.165 -  moreover from `a \<in> A` and  `b \<in> B` have "(a , b) \<in> A \<times> B" by auto
   1.166 -  ultimately have "\<exists>y \<in> A \<times> B. x = prod_fun f g y" by auto
   1.167 -  thus "x \<in> {x. \<exists>y \<in> A \<times> B. x = prod_fun f g y}" by auto
   1.168 -qed
   1.169 -
   1.170  lemma swap_inj_on:
   1.171    "inj_on (\<lambda>(i, j). (j, i)) A"
   1.172    by (auto intro!: inj_onI)
   1.173 @@ -1167,6 +1112,66 @@
   1.174      using * eq[symmetric] by auto
   1.175  qed simp_all
   1.176  
   1.177 +text {* The following @{const map_pair} lemmas are due to Joachim Breitner: *}
   1.178 +
   1.179 +lemma map_pair_inj_on:
   1.180 +  assumes "inj_on f A" and "inj_on g B"
   1.181 +  shows "inj_on (map_pair f g) (A \<times> B)"
   1.182 +proof (rule inj_onI)
   1.183 +  fix x :: "'a \<times> 'c" and y :: "'a \<times> 'c"
   1.184 +  assume "x \<in> A \<times> B" hence "fst x \<in> A" and "snd x \<in> B" by auto
   1.185 +  assume "y \<in> A \<times> B" hence "fst y \<in> A" and "snd y \<in> B" by auto
   1.186 +  assume "map_pair f g x = map_pair f g y"
   1.187 +  hence "fst (map_pair f g x) = fst (map_pair f g y)" by (auto)
   1.188 +  hence "f (fst x) = f (fst y)" by (cases x,cases y,auto)
   1.189 +  with `inj_on f A` and `fst x \<in> A` and `fst y \<in> A`
   1.190 +  have "fst x = fst y" by (auto dest:dest:inj_onD)
   1.191 +  moreover from `map_pair f g x = map_pair f g y`
   1.192 +  have "snd (map_pair f g x) = snd (map_pair f g y)" by (auto)
   1.193 +  hence "g (snd x) = g (snd y)" by (cases x,cases y,auto)
   1.194 +  with `inj_on g B` and `snd x \<in> B` and `snd y \<in> B`
   1.195 +  have "snd x = snd y" by (auto dest:dest:inj_onD)
   1.196 +  ultimately show "x = y" by(rule prod_eqI)
   1.197 +qed
   1.198 +
   1.199 +lemma map_pair_surj:
   1.200 +  assumes "surj f" and "surj g"
   1.201 +  shows "surj (map_pair f g)"
   1.202 +unfolding surj_def
   1.203 +proof
   1.204 +  fix y :: "'b \<times> 'd"
   1.205 +  from `surj f` obtain a where "fst y = f a" by (auto elim:surjE)
   1.206 +  moreover
   1.207 +  from `surj g` obtain b where "snd y = g b" by (auto elim:surjE)
   1.208 +  ultimately have "(fst y, snd y) = map_pair f g (a,b)" by auto
   1.209 +  thus "\<exists>x. y = map_pair f g x" by auto
   1.210 +qed
   1.211 +
   1.212 +lemma map_pair_surj_on:
   1.213 +  assumes "f ` A = A'" and "g ` B = B'"
   1.214 +  shows "map_pair f g ` (A \<times> B) = A' \<times> B'"
   1.215 +unfolding image_def
   1.216 +proof(rule set_eqI,rule iffI)
   1.217 +  fix x :: "'a \<times> 'c"
   1.218 +  assume "x \<in> {y\<Colon>'a \<times> 'c. \<exists>x\<Colon>'b \<times> 'd\<in>A \<times> B. y = map_pair f g x}"
   1.219 +  then obtain y where "y \<in> A \<times> B" and "x = map_pair f g y" by blast
   1.220 +  from `image f A = A'` and `y \<in> A \<times> B` have "f (fst y) \<in> A'" by auto
   1.221 +  moreover from `image g B = B'` and `y \<in> A \<times> B` have "g (snd y) \<in> B'" by auto
   1.222 +  ultimately have "(f (fst y), g (snd y)) \<in> (A' \<times> B')" by auto
   1.223 +  with `x = map_pair f g y` show "x \<in> A' \<times> B'" by (cases y, auto)
   1.224 +next
   1.225 +  fix x :: "'a \<times> 'c"
   1.226 +  assume "x \<in> A' \<times> B'" hence "fst x \<in> A'" and "snd x \<in> B'" by auto
   1.227 +  from `image f A = A'` and `fst x \<in> A'` have "fst x \<in> image f A" by auto
   1.228 +  then obtain a where "a \<in> A" and "fst x = f a" by (rule imageE)
   1.229 +  moreover from `image g B = B'` and `snd x \<in> B'`
   1.230 +  obtain b where "b \<in> B" and "snd x = g b" by auto
   1.231 +  ultimately have "(fst x, snd x) = map_pair f g (a,b)" by auto
   1.232 +  moreover from `a \<in> A` and  `b \<in> B` have "(a , b) \<in> A \<times> B" by auto
   1.233 +  ultimately have "\<exists>y \<in> A \<times> B. x = map_pair f g y" by auto
   1.234 +  thus "x \<in> {x. \<exists>y \<in> A \<times> B. x = map_pair f g y}" by auto
   1.235 +qed
   1.236 +
   1.237  
   1.238  subsection {* Inductively defined sets *}
   1.239