equal
deleted
inserted
replaced
267 |
267 |
268 lemma surjective_pairing: "p = (fst p, snd p)" |
268 lemma surjective_pairing: "p = (fst p, snd p)" |
269 -- {* Do not add as rewrite rule: invalidates some proofs in IMP *} |
269 -- {* Do not add as rewrite rule: invalidates some proofs in IMP *} |
270 by (cases p) simp |
270 by (cases p) simp |
271 |
271 |
272 declare surjective_pairing [symmetric, simp] |
272 lemmas pair_collapse = surjective_pairing [symmetric] |
|
273 declare pair_collapse [simp] |
273 |
274 |
274 lemma surj_pair [simp]: "EX x y. z = (x, y)" |
275 lemma surj_pair [simp]: "EX x y. z = (x, y)" |
275 apply (rule exI) |
276 apply (rule exI) |
276 apply (rule exI) |
277 apply (rule exI) |
277 apply (rule surjective_pairing) |
278 apply (rule surjective_pairing) |