src/HOL/Product_Type.thy
changeset 33594 357f74e0090c
parent 33275 b497b2574bf6
child 33638 548a34929e98
     1.1 --- a/src/HOL/Product_Type.thy	Tue Nov 10 16:11:37 2009 +0100
     1.2 +++ b/src/HOL/Product_Type.thy	Tue Nov 10 16:11:39 2009 +0100
     1.3 @@ -781,6 +781,54 @@
     1.4    "apsnd f (x, y) = (x, f y)" 
     1.5    by (simp add: apsnd_def)
     1.6  
     1.7 +lemma fst_apfst [simp]:
     1.8 +  "fst (apfst f x) = f (fst x)"
     1.9 +  by (cases x) simp
    1.10 +
    1.11 +lemma fst_apsnd [simp]:
    1.12 +  "fst (apsnd f x) = fst x"
    1.13 +  by (cases x) simp
    1.14 +
    1.15 +lemma snd_apfst [simp]:
    1.16 +  "snd (apfst f x) = snd x"
    1.17 +  by (cases x) simp
    1.18 +
    1.19 +lemma snd_apsnd [simp]:
    1.20 +  "snd (apsnd f x) = f (snd x)"
    1.21 +  by (cases x) simp
    1.22 +
    1.23 +lemma apfst_compose:
    1.24 +  "apfst f (apfst g x) = apfst (f \<circ> g) x"
    1.25 +  by (cases x) simp
    1.26 +
    1.27 +lemma apsnd_compose:
    1.28 +  "apsnd f (apsnd g x) = apsnd (f \<circ> g) x"
    1.29 +  by (cases x) simp
    1.30 +
    1.31 +lemma apfst_apsnd [simp]:
    1.32 +  "apfst f (apsnd g x) = (f (fst x), g (snd x))"
    1.33 +  by (cases x) simp
    1.34 +
    1.35 +lemma apsnd_apfst [simp]:
    1.36 +  "apsnd f (apfst g x) = (g (fst x), f (snd x))"
    1.37 +  by (cases x) simp
    1.38 +
    1.39 +lemma apfst_id [simp] :
    1.40 +  "apfst id = id"
    1.41 +  by (simp add: expand_fun_eq)
    1.42 +
    1.43 +lemma apsnd_id [simp] :
    1.44 +  "apsnd id = id"
    1.45 +  by (simp add: expand_fun_eq)
    1.46 +
    1.47 +lemma apfst_eq_conv [simp]:
    1.48 +  "apfst f x = apfst g x \<longleftrightarrow> f (fst x) = g (fst x)"
    1.49 +  by (cases x) simp
    1.50 +
    1.51 +lemma apsnd_eq_conv [simp]:
    1.52 +  "apsnd f x = apsnd g x \<longleftrightarrow> f (snd x) = g (snd x)"
    1.53 +  by (cases x) simp
    1.54 +
    1.55  
    1.56  text {*
    1.57    Disjoint union of a family of sets -- Sigma.