17 "Pair_Rep a b = Pair_Rep a' b' ==> a=a' & b=b'"; |
17 "Pair_Rep a b = Pair_Rep a' b' ==> a=a' & b=b'"; |
18 by (EVERY1 [rtac (major RS fun_cong RS fun_cong RS subst), |
18 by (EVERY1 [rtac (major RS fun_cong RS fun_cong RS subst), |
19 rtac conjI, rtac refl, rtac refl]); |
19 rtac conjI, rtac refl, rtac refl]); |
20 qed "Pair_Rep_inject"; |
20 qed "Pair_Rep_inject"; |
21 |
21 |
22 goal Prod.thy "inj_onto Abs_Prod Prod"; |
22 goal Prod.thy "inj_on Abs_Prod Prod"; |
23 by (rtac inj_onto_inverseI 1); |
23 by (rtac inj_on_inverseI 1); |
24 by (etac Abs_Prod_inverse 1); |
24 by (etac Abs_Prod_inverse 1); |
25 qed "inj_onto_Abs_Prod"; |
25 qed "inj_on_Abs_Prod"; |
26 |
26 |
27 val prems = goalw Prod.thy [Pair_def] |
27 val prems = goalw Prod.thy [Pair_def] |
28 "[| (a, b) = (a',b'); [| a=a'; b=b' |] ==> R |] ==> R"; |
28 "[| (a, b) = (a',b'); [| a=a'; b=b' |] ==> R |] ==> R"; |
29 by (rtac (inj_onto_Abs_Prod RS inj_ontoD RS Pair_Rep_inject RS conjE) 1); |
29 by (rtac (inj_on_Abs_Prod RS inj_onD RS Pair_Rep_inject RS conjE) 1); |
30 by (REPEAT (ares_tac (prems@[ProdI]) 1)); |
30 by (REPEAT (ares_tac (prems@[ProdI]) 1)); |
31 qed "Pair_inject"; |
31 qed "Pair_inject"; |
32 |
32 |
33 goal Prod.thy "((a,b) = (a',b')) = (a=a' & b=b')"; |
33 goal Prod.thy "((a,b) = (a',b')) = (a=a' & b=b')"; |
34 by (blast_tac (claset() addSEs [Pair_inject]) 1); |
34 by (blast_tac (claset() addSEs [Pair_inject]) 1); |
148 (*For use with split_tac and the simplifier*) |
148 (*For use with split_tac and the simplifier*) |
149 goal Prod.thy "R (split c p) = (! x y. p = (x,y) --> R (c x y))"; |
149 goal Prod.thy "R (split c p) = (! x y. p = (x,y) --> R (c x y))"; |
150 by (stac surjective_pairing 1); |
150 by (stac surjective_pairing 1); |
151 by (stac split 1); |
151 by (stac split 1); |
152 by (Blast_tac 1); |
152 by (Blast_tac 1); |
153 qed "expand_split"; |
153 qed "split_split"; |
154 |
154 |
155 (* could be done after split_tac has been speeded up significantly: |
155 (* could be done after split_tac has been speeded up significantly: |
156 simpset_ref() := simpset() addsplits [expand_split]; |
156 simpset_ref() := simpset() addsplits [split_split]; |
157 precompute the constants involved and don't do anything unless |
157 precompute the constants involved and don't do anything unless |
158 the current goal contains one of those constants |
158 the current goal contains one of those constants |
159 *) |
159 *) |
160 |
160 |
161 goal Prod.thy "R (split c p) = (~(? x y. p = (x,y) & (~R (c x y))))"; |
161 goal Prod.thy "R (split c p) = (~(? x y. p = (x,y) & (~R (c x y))))"; |
162 by (stac expand_split 1); |
162 by (stac split_split 1); |
163 by (Simp_tac 1); |
163 by (Simp_tac 1); |
164 qed "expand_split_asm"; |
164 qed "expand_split_asm"; |
165 |
165 |
166 (** split used as a logical connective or set former **) |
166 (** split used as a logical connective or set former **) |
167 |
167 |