Renamed upd_snd_conv to apsnd_conv to be consistent with apfst_conv; Added apsnd_apfst_commute
authorhoelzl
Thu Nov 12 17:21:43 2009 +0100 (2009-11-12)
changeset 33638548a34929e98
parent 33637 19a4fe8ecf24
child 33639 603320b93668
Renamed upd_snd_conv to apsnd_conv to be consistent with apfst_conv; Added apsnd_apfst_commute
src/HOL/Product_Type.thy
     1.1 --- a/src/HOL/Product_Type.thy	Thu Nov 12 15:50:05 2009 +0100
     1.2 +++ b/src/HOL/Product_Type.thy	Thu Nov 12 17:21:43 2009 +0100
     1.3 @@ -777,7 +777,7 @@
     1.4    "apfst f (x, y) = (f x, y)" 
     1.5    by (simp add: apfst_def)
     1.6  
     1.7 -lemma upd_snd_conv [simp, code]:
     1.8 +lemma apsnd_conv [simp, code]:
     1.9    "apsnd f (x, y) = (x, f y)" 
    1.10    by (simp add: apsnd_def)
    1.11  
    1.12 @@ -829,6 +829,9 @@
    1.13    "apsnd f x = apsnd g x \<longleftrightarrow> f (snd x) = g (snd x)"
    1.14    by (cases x) simp
    1.15  
    1.16 +lemma apsnd_apfst_commute:
    1.17 +  "apsnd f (apfst g p) = apfst g (apsnd f p)"
    1.18 +  by simp
    1.19  
    1.20  text {*
    1.21    Disjoint union of a family of sets -- Sigma.