author | bulwahn |

Wed Oct 17 14:13:57 2012 +0200 (2012-10-17) | |

changeset 49897 | cc69be3c8f87 |

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)

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 *}