Renamed upd_snd_conv to apsnd_conv to be consistent with apfst_conv; Added apsnd_apfst_commute

--- a/src/HOL/Product_Type.thy	Thu Nov 12 15:50:05 2009 +0100
+++ b/src/HOL/Product_Type.thy	Thu Nov 12 17:21:43 2009 +0100
@@ -777,7 +777,7 @@
   "apfst f (x, y) = (f x, y)" 
   by (simp add: apfst_def)
 
-lemma upd_snd_conv [simp, code]:
+lemma apsnd_conv [simp, code]:
   "apsnd f (x, y) = (x, f y)" 
   by (simp add: apsnd_def)
 
@@ -829,6 +829,9 @@
   "apsnd f x = apsnd g x \<longleftrightarrow> f (snd x) = g (snd x)"
   by (cases x) simp
 
+lemma apsnd_apfst_commute:
+  "apsnd f (apfst g p) = apfst g (apsnd f p)"
+  by simp
 
 text {*
   Disjoint union of a family of sets -- Sigma.