src/HOL/Product_Type.thy
changeset 33638 548a34929e98
parent 33594 357f74e0090c
child 33959 2afc55e8ed27
equal deleted inserted replaced
33637:19a4fe8ecf24 33638:548a34929e98
   775 
   775 
   776 lemma apfst_conv [simp, code]:
   776 lemma apfst_conv [simp, code]:
   777   "apfst f (x, y) = (f x, y)" 
   777   "apfst f (x, y) = (f x, y)" 
   778   by (simp add: apfst_def)
   778   by (simp add: apfst_def)
   779 
   779 
   780 lemma upd_snd_conv [simp, code]:
   780 lemma apsnd_conv [simp, code]:
   781   "apsnd f (x, y) = (x, f y)" 
   781   "apsnd f (x, y) = (x, f y)" 
   782   by (simp add: apsnd_def)
   782   by (simp add: apsnd_def)
   783 
   783 
   784 lemma fst_apfst [simp]:
   784 lemma fst_apfst [simp]:
   785   "fst (apfst f x) = f (fst x)"
   785   "fst (apfst f x) = f (fst x)"
   827 
   827 
   828 lemma apsnd_eq_conv [simp]:
   828 lemma apsnd_eq_conv [simp]:
   829   "apsnd f x = apsnd g x \<longleftrightarrow> f (snd x) = g (snd x)"
   829   "apsnd f x = apsnd g x \<longleftrightarrow> f (snd x) = g (snd x)"
   830   by (cases x) simp
   830   by (cases x) simp
   831 
   831 
       
   832 lemma apsnd_apfst_commute:
       
   833   "apsnd f (apfst g p) = apfst g (apsnd f p)"
       
   834   by simp
   832 
   835 
   833 text {*
   836 text {*
   834   Disjoint union of a family of sets -- Sigma.
   837   Disjoint union of a family of sets -- Sigma.
   835 *}
   838 *}
   836 
   839