equal
deleted
inserted
replaced
99 |
99 |
100 val prems = goalw Prod.thy [split_def] |
100 val prems = goalw Prod.thy [split_def] |
101 "[| split(c,p); !!x y. [| p = <x,y>; c(x,y) |] ==> Q |] ==> Q"; |
101 "[| split(c,p); !!x y. [| p = <x,y>; c(x,y) |] ==> Q |] ==> Q"; |
102 by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1)); |
102 by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1)); |
103 val splitE = result(); |
103 val splitE = result(); |
|
104 |
|
105 goal Prod.thy "!!R a b. split(R,<a,b>) ==> R(a,b)"; |
|
106 by (etac (split RS iffD1) 1); |
|
107 val splitD = result(); |
104 |
108 |
105 goal Prod.thy "!!a b c. z: c(a,b) ==> z: split(c, <a,b>)"; |
109 goal Prod.thy "!!a b c. z: c(a,b) ==> z: split(c, <a,b>)"; |
106 by (asm_simp_tac pair_ss 1); |
110 by (asm_simp_tac pair_ss 1); |
107 val mem_splitI = result(); |
111 val mem_splitI = result(); |
108 |
112 |