src/HOL/Product_Type.thy
changeset 49897 cc69be3c8f87
parent 49834 b27bbb021df1
child 50104 de19856feb54
     1.1 --- a/src/HOL/Product_Type.thy	Wed Oct 17 14:13:57 2012 +0200
     1.2 +++ b/src/HOL/Product_Type.thy	Wed Oct 17 14:13:57 2012 +0200
     1.3 @@ -306,6 +306,12 @@
     1.4  
     1.5  subsubsection {* Fundamental operations and properties *}
     1.6  
     1.7 +lemma Pair_inject:
     1.8 +  assumes "(a, b) = (a', b')"
     1.9 +    and "a = a' ==> b = b' ==> R"
    1.10 +  shows R
    1.11 +  using assms by simp
    1.12 +
    1.13  lemma surj_pair [simp]: "EX x y. p = (x, y)"
    1.14    by (cases p) simp
    1.15  
    1.16 @@ -1140,12 +1146,6 @@
    1.17    obtains x y where "p = (x, y)"
    1.18    by (fact prod.exhaust)
    1.19  
    1.20 -lemma Pair_inject:
    1.21 -  assumes "(a, b) = (a', b')"
    1.22 -    and "a = a' ==> b = b' ==> R"
    1.23 -  shows R
    1.24 -  using assms by simp
    1.25 -
    1.26  lemmas Pair_eq = prod.inject
    1.27  
    1.28  lemmas split = split_conv  -- {* for backwards compatibility *}