11 by(Auto_tac); |
11 by(Auto_tac); |
12 qed "image_rev"; |
12 qed "image_rev"; |
13 |
13 |
14 fun case_tac1 s i = EVERY [case_tac s i, rotate_tac ~1 i, rotate_tac ~1 (i+1)]; |
14 fun case_tac1 s i = EVERY [case_tac s i, rotate_tac ~1 i, rotate_tac ~1 (i+1)]; |
15 |
15 |
16 val select_split = prove_goalw Prod.thy [split_def] |
16 val select_split = prove_goalw Product_Type.thy [split_def] |
17 "(SOME (x,y). P x y) = (SOME xy. P (fst xy) (snd xy))" (K [rtac refl 1]); |
17 "(SOME (x,y). P x y) = (SOME xy. P (fst xy) (snd xy))" (K [rtac refl 1]); |
18 |
18 |
19 |
19 |
20 val split_beta = prove_goal Prod.thy "(\\<lambda>(x,y). P x y) z = P (fst z) (snd z)" |
20 val split_beta = prove_goal Product_Type.thy "(\\<lambda>(x,y). P x y) z = P (fst z) (snd z)" |
21 (fn _ => [stac surjective_pairing 1, stac split 1, rtac refl 1]); |
21 (fn _ => [stac surjective_pairing 1, stac split 1, rtac refl 1]); |
22 val split_beta2 = prove_goal Prod.thy "(\\<lambda>(x,y). P x y) (w,z) = P w z" |
22 val split_beta2 = prove_goal Product_Type.thy "(\\<lambda>(x,y). P x y) (w,z) = P w z" |
23 (fn _ => [Auto_tac]); |
23 (fn _ => [Auto_tac]); |
24 val splitE2 = prove_goal Prod.thy "[|Q (split P z); !!x y. [|z = (x, y); Q (P x y)|] ==> R|] ==> R" (fn prems => [ |
24 val splitE2 = prove_goal Product_Type.thy "[|Q (split P z); !!x y. [|z = (x, y); Q (P x y)|] ==> R|] ==> R" (fn prems => [ |
25 REPEAT (resolve_tac (prems@[surjective_pairing]) 1), |
25 REPEAT (resolve_tac (prems@[surjective_pairing]) 1), |
26 rtac (split_beta RS subst) 1, |
26 rtac (split_beta RS subst) 1, |
27 rtac (hd prems) 1]); |
27 rtac (hd prems) 1]); |
28 val splitE2' = prove_goal Prod.thy "[|((\\<lambda>(x,y). P x y) z) w; !!x y. [|z = (x, y); (P x y) w|] ==> R|] ==> R" (fn prems => [ |
28 val splitE2' = prove_goal Product_Type.thy "[|((\\<lambda>(x,y). P x y) z) w; !!x y. [|z = (x, y); (P x y) w|] ==> R|] ==> R" (fn prems => [ |
29 REPEAT (resolve_tac (prems@[surjective_pairing]) 1), |
29 REPEAT (resolve_tac (prems@[surjective_pairing]) 1), |
30 res_inst_tac [("P1","P")] (split_beta RS subst) 1, |
30 res_inst_tac [("P1","P")] (split_beta RS subst) 1, |
31 rtac (hd prems) 1]); |
31 rtac (hd prems) 1]); |
32 |
32 |
33 |
33 |
129 Goal "[|M = N; !!x. x\\<in>N ==> f x = g x|] ==> f``M = g``N"; |
129 Goal "[|M = N; !!x. x\\<in>N ==> f x = g x|] ==> f``M = g``N"; |
130 by(rtac set_ext 1); |
130 by(rtac set_ext 1); |
131 by(simp_tac (simpset() addsimps image_def::premises()) 1); |
131 by(simp_tac (simpset() addsimps image_def::premises()) 1); |
132 qed "image_cong"; |
132 qed "image_cong"; |
133 |
133 |
134 val split_Pair_eq = prove_goal Prod.thy |
134 val split_Pair_eq = prove_goal Product_Type.thy |
135 "!!X. ((x, y), z) \\<in> split (\\<lambda>x. Pair (x, Y)) `` A ==> y = Y" (K [ |
135 "!!X. ((x, y), z) \\<in> split (\\<lambda>x. Pair (x, Y)) `` A ==> y = Y" (K [ |
136 etac imageE 1, |
136 etac imageE 1, |
137 split_all_tac 1, |
137 split_all_tac 1, |
138 auto_tac(claset_of Prod.thy,simpset_of Prod.thy)]); |
138 auto_tac(claset_of Product_Type.thy,simpset_of Product_Type.thy)]); |
139 |
139 |
140 |
140 |
141 (* More about Maps *) |
141 (* More about Maps *) |
142 |
142 |
143 val override_SomeD = prove_goalw thy [override_def] "(s ++ t) k = Some x ==> \ |
143 val override_SomeD = prove_goalw thy [override_def] "(s ++ t) k = Some x ==> \ |