moving Pair_inject from legacy and duplicate section to general section, as Pair_inject was considered a duplicate in e8400e31528a by mistake (cf. communication on dev mailing list)
authorbulwahn
Wed Oct 17 14:13:57 2012 +0200 (2012-10-17)
changeset 49897cc69be3c8f87
parent 49896 a39deedd5c3f
child 49898 dd2ae15ac74f
moving Pair_inject from legacy and duplicate section to general section, as Pair_inject was considered a duplicate in e8400e31528a by mistake (cf. communication on dev mailing list)
src/HOL/Product_Type.thy
     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 *}