src/HOL/Product_Type.thy
changeset 62139 519362f817c7
parent 62101 26c0a70f78a3
child 62379 340738057c8c
     1.1 --- a/src/HOL/Product_Type.thy	Tue Jan 12 09:28:08 2016 +0100
     1.2 +++ b/src/HOL/Product_Type.thy	Tue Jan 12 14:14:28 2016 +0100
     1.3 @@ -997,6 +997,12 @@
     1.4    "(case prod.swap p of (y, x) \<Rightarrow> f x y) = (case p of (x, y) \<Rightarrow> f x y)"
     1.5    by (cases p) simp
     1.6  
     1.7 +lemma fst_swap [simp]: "fst (prod.swap x) = snd x"
     1.8 +by(cases x) simp
     1.9 +
    1.10 +lemma snd_swap [simp]: "snd (prod.swap x) = fst x"
    1.11 +by(cases x) simp
    1.12 +
    1.13  text \<open>
    1.14    Disjoint union of a family of sets -- Sigma.
    1.15  \<close>