# HG changeset patch
# User haftmann
# Date 1257865899 -3600
# Node ID 357f74e0090c1aef0c64bc12234ee69ec0a257bd
# Parent  ef54e2108b74a99047c15d2d24663ea835d51886
lemmas about apfst and apsnd

diff -r ef54e2108b74 -r 357f74e0090c src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Tue Nov 10 16:11:37 2009 +0100
+++ b/src/HOL/Product_Type.thy	Tue Nov 10 16:11:39 2009 +0100
@@ -781,6 +781,54 @@
   "apsnd f (x, y) = (x, f y)" 
   by (simp add: apsnd_def)
 
+lemma fst_apfst [simp]:
+  "fst (apfst f x) = f (fst x)"
+  by (cases x) simp
+
+lemma fst_apsnd [simp]:
+  "fst (apsnd f x) = fst x"
+  by (cases x) simp
+
+lemma snd_apfst [simp]:
+  "snd (apfst f x) = snd x"
+  by (cases x) simp
+
+lemma snd_apsnd [simp]:
+  "snd (apsnd f x) = f (snd x)"
+  by (cases x) simp
+
+lemma apfst_compose:
+  "apfst f (apfst g x) = apfst (f \<circ> g) x"
+  by (cases x) simp
+
+lemma apsnd_compose:
+  "apsnd f (apsnd g x) = apsnd (f \<circ> g) x"
+  by (cases x) simp
+
+lemma apfst_apsnd [simp]:
+  "apfst f (apsnd g x) = (f (fst x), g (snd x))"
+  by (cases x) simp
+
+lemma apsnd_apfst [simp]:
+  "apsnd f (apfst g x) = (g (fst x), f (snd x))"
+  by (cases x) simp
+
+lemma apfst_id [simp] :
+  "apfst id = id"
+  by (simp add: expand_fun_eq)
+
+lemma apsnd_id [simp] :
+  "apsnd id = id"
+  by (simp add: expand_fun_eq)
+
+lemma apfst_eq_conv [simp]:
+  "apfst f x = apfst g x \<longleftrightarrow> f (fst x) = g (fst x)"
+  by (cases x) simp
+
+lemma apsnd_eq_conv [simp]:
+  "apsnd f x = apsnd g x \<longleftrightarrow> f (snd x) = g (snd x)"
+  by (cases x) simp
+
 
 text {*
   Disjoint union of a family of sets -- Sigma.