2 ID: $Id$ |
2 ID: $Id$ |
3 Author: David von Oheimb |
3 Author: David von Oheimb |
4 Copyright 1999 TU Muenchen |
4 Copyright 1999 TU Muenchen |
5 *) |
5 *) |
6 |
6 |
7 val strip_tac1 = SELECT_GOAL (safe_tac (HOL_cs delrules [conjI, disjE, impCE])); |
7 (*###TO Product_Type*) |
8 |
8 Goalw [split_def] "Eps (split P) = (SOME xy. P (fst xy) (snd xy))"; |
9 Goalw [image_def] |
9 by (rtac refl 1); |
10 "x \\<in> f``A ==> \\<exists>y. y \\<in> A \\<and> x = f y"; |
10 qed "select_split"; |
11 by(Auto_tac); |
|
12 qed "image_rev"; |
|
13 |
|
14 fun case_tac1 s i = EVERY [case_tac s i, rotate_tac ~1 i, rotate_tac ~1 (i+1)]; |
|
15 |
|
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]); |
|
18 |
|
19 |
|
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]); |
|
22 val split_beta2 = prove_goal Product_Type.thy "(\\<lambda>(x,y). P x y) (w,z) = P w z" |
|
23 (fn _ => [Auto_tac]); |
|
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), |
|
26 rtac (split_beta RS subst) 1, |
|
27 rtac (hd prems) 1]); |
|
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), |
|
30 res_inst_tac [("P1","P")] (split_beta RS subst) 1, |
|
31 rtac (hd prems) 1]); |
|
32 |
|
33 |
|
34 fun pair_tac s = res_inst_tac [("p",s)] PairE THEN' hyp_subst_tac; |
|
35 |
|
36 val BallE = prove_goal thy "[|Ball A P; x \\<notin> A ==> Q; P x ==> Q |] ==> Q" |
|
37 (fn prems => [rtac ballE 1, resolve_tac prems 1, |
|
38 eresolve_tac prems 1, eresolve_tac prems 1]); |
|
39 |
|
40 val set_cs2 = set_cs delrules [ballE] addSEs [BallE]; |
|
41 |
11 |
42 Addsimps [Let_def]; |
12 Addsimps [Let_def]; |
43 |
13 |
44 (* To HOL.ML *) |
14 (* ### To HOL.ML *) |
45 |
15 Goal "[| ?!x. P x; P y |] ==> Eps P = y"; |
46 val ex1_some_eq_trivial = prove_goal HOL.thy "[| \\<exists>!x. P x; P y |] ==> Eps P = y" |
16 by (rtac some_equality 1); |
47 (fn prems => [ |
17 by (atac 1); |
48 cut_facts_tac prems 1, |
18 by (etac ex1E 1); |
49 rtac some_equality 1, |
19 by (etac all_dupE 1); |
50 atac 1, |
20 by (fast_tac HOL_cs 1); |
51 etac ex1E 1, |
21 qed "ex1_some_eq_trivial"; |
52 etac all_dupE 1, |
|
53 fast_tac HOL_cs 1]); |
|
54 |
|
55 |
|
56 val ball_insert = prove_goalw equalities.thy [Ball_def] |
|
57 "Ball (insert x A) P = (P x \\<and> Ball A P)" (fn _ => [ |
|
58 fast_tac set_cs 1]); |
|
59 |
|
60 fun option_case_tac i = EVERY [ |
|
61 etac option_caseE i, |
|
62 rotate_tac ~2 (i+1), asm_full_simp_tac HOL_basic_ss (i+1), |
|
63 rotate_tac ~2 i , asm_full_simp_tac HOL_basic_ss i]; |
|
64 |
|
65 val not_None_tac = EVERY' [dtac (not_None_eq RS iffD1),rotate_tac ~1,etac exE, |
|
66 rotate_tac ~1,asm_full_simp_tac |
|
67 (simpset() delsimps [split_paired_All,split_paired_Ex])]; |
|
68 |
|
69 Goal "{y. x = Some y} \\<subseteq> {the x}"; |
|
70 by Auto_tac; |
|
71 qed "some_subset_the"; |
|
72 |
|
73 fun ex_ftac thm = EVERY' [forward_tac [thm], REPEAT o (etac exE), rotate_tac ~1, |
|
74 asm_full_simp_tac (simpset() delsimps [split_paired_All,split_paired_Ex])]; |
|
75 |
|
76 val optionE = prove_goal thy |
|
77 "[| opt = None ==> P; !!x. opt = Some x ==> P |] ==> P" |
|
78 (fn prems => [ |
|
79 case_tac "opt = None" 1, |
|
80 eresolve_tac prems 1, |
|
81 not_None_tac 1, |
|
82 eresolve_tac prems 1]); |
|
83 |
|
84 fun option_case_tac2 s i = EVERY [ |
|
85 case_tac s i, |
|
86 rotate_tac ~1 (i+1), asm_full_simp_tac HOL_basic_ss (i+1), |
|
87 rotate_tac ~1 i , asm_full_simp_tac HOL_basic_ss i]; |
|
88 |
|
89 val option_map_SomeD = prove_goalw thy [option_map_def] |
|
90 "!!x. option_map f x = Some y ==> \\<exists>z. x = Some z \\<and> f z = y" (K [ |
|
91 option_case_tac2 "x" 1, |
|
92 Auto_tac]); |
|
93 |
22 |
94 |
23 |
95 section "unique"; |
24 section "unique"; |
96 |
25 |
97 Goal "(x, y) : set l --> x : fst `` set l"; |
26 Goal "(x, y) : set l --> x : fst `` set l"; |
118 Goal "unique l --> inj f --> unique (map (%(k,x). (f k, g k x)) l)"; |
47 Goal "unique l --> inj f --> unique (map (%(k,x). (f k, g k x)) l)"; |
119 by (induct_tac "l" 1); |
48 by (induct_tac "l" 1); |
120 by (auto_tac (claset() addDs [fst_in_set_lemma],simpset()addsimps[inj_eq])); |
49 by (auto_tac (claset() addDs [fst_in_set_lemma],simpset()addsimps[inj_eq])); |
121 qed_spec_mp "unique_map_inj"; |
50 qed_spec_mp "unique_map_inj"; |
122 |
51 |
123 Goal "!!l. unique l ==> unique (map (split (\\<lambda>k. Pair (k, C))) l)"; |
|
124 by(etac unique_map_inj 1); |
|
125 by(rtac injI 1); |
|
126 by Auto_tac; |
|
127 qed "unique_map_Pair"; |
|
128 |
|
129 Goal "[|M = N; !!x. x\\<in>N ==> f x = g x|] ==> f``M = g``N"; |
|
130 by(rtac set_ext 1); |
|
131 by(simp_tac (simpset() addsimps image_def::premises()) 1); |
|
132 qed "image_cong"; |
|
133 |
|
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 [ |
|
136 etac imageE 1, |
|
137 split_all_tac 1, |
|
138 auto_tac(claset_of Product_Type.thy,simpset_of Product_Type.thy)]); |
|
139 |
|
140 |
|
141 (* More about Maps *) |
52 (* More about Maps *) |
142 |
53 |
143 val override_SomeD = prove_goalw thy [override_def] "(s ++ t) k = Some x ==> \ |
54 (*###Addsimps [fun_upd_same, fun_upd_other];*) |
144 \ t k = Some x | t k = None \\<and> s k = Some x" (fn prems => [ |
|
145 cut_facts_tac prems 1, |
|
146 case_tac "\\<exists>x. t k = Some x" 1, |
|
147 etac exE 1, |
|
148 rotate_tac ~1 1, |
|
149 Asm_full_simp_tac 1, |
|
150 asm_full_simp_tac (HOL_ss addsimps [not_None_eq RS sym]) 1, |
|
151 rotate_tac ~1 1, |
|
152 Asm_full_simp_tac 1]); |
|
153 |
55 |
154 Addsimps [fun_upd_same, fun_upd_other]; |
56 Goal "unique l --> (k, x) : set l --> map_of l k = Some x"; |
155 |
57 by (induct_tac "l" 1); |
156 Goal "unique xys --> (map_of xys x = Some y) = ((x,y) \\<in> set xys)"; |
58 by Auto_tac; |
157 by(induct_tac "xys" 1); |
59 qed_spec_mp "map_of_SomeI"; |
158 by(Simp_tac 1); |
|
159 by(force_tac (claset(), simpset() addsimps [unique_Cons]) 1); |
|
160 qed_spec_mp "unique_map_of_Some_conv"; |
|
161 |
|
162 val in_set_get = unique_map_of_Some_conv RS iffD2; |
|
163 val get_in_set = unique_map_of_Some_conv RS iffD1; |
|
164 |
60 |
165 Goal "(\\<forall>(x,y)\\<in>set l. P x y) --> (\\<forall>x. \\<forall>y. map_of l x = Some y --> P x y)"; |
61 Goal "(\\<forall>(x,y)\\<in>set l. P x y) --> (\\<forall>x. \\<forall>y. map_of l x = Some y --> P x y)"; |
166 by(induct_tac "l" 1); |
62 by(induct_tac "l" 1); |
167 by(ALLGOALS Simp_tac); |
63 by(ALLGOALS Simp_tac); |
168 by Safe_tac; |
64 by Safe_tac; |
169 by Auto_tac; |
65 by Auto_tac; |
170 bind_thm("Ball_set_table",result() RS mp); |
66 bind_thm("Ball_set_table",result() RS mp); |
171 |
67 |
172 val table_mono = prove_goal thy |
68 Goal "map_of (map (\\<lambda>((k,k'),x). (k,(k',x))) t) k = Some (k',x) --> \ |
173 "unique l' --> (\\<forall>xy. (xy)\\<in>set l --> (xy)\\<in>set l') -->\ |
69 \map_of t (k, k') = Some x"; |
174 \ (\\<forall>k y. map_of l k = Some y --> map_of l' k = Some y)" (fn _ => [ |
70 by (induct_tac "t" 1); |
175 induct_tac "l" 1, |
71 by Auto_tac; |
176 Auto_tac, |
72 qed_spec_mp "table_of_remap_SomeD"; |
177 fast_tac (HOL_cs addSIs [in_set_get]) 1]) |
|
178 RS mp RS mp RS spec RS spec RS mp; |
|
179 |
73 |
180 val table_map_Some' = prove_goal thy "map_of t k = Some (k', x) --> \ |
74 (* ### To Map.ML *) |
181 \ map_of (map (\\<lambda>u. ((fst u, fst (snd u)), snd (snd u))) t) (k, k') = Some x" (K [ |
75 Goal "map_of (map (\\<lambda>(a,b). (a,f b)) xs) x = option_map f (map_of xs x)"; |
182 induct_tac "t" 1, |
|
183 ALLGOALS Simp_tac, |
|
184 case_tac1 "k = fst a" 1, |
|
185 Auto_tac]) RS mp; |
|
186 val table_map_Some = prove_goal thy |
|
187 "map_of (map (\\<lambda>((k,k'),x). (k,(k',x))) t) k = Some (k',x) --> \ |
|
188 \map_of t (k, k') = Some x" (K [ |
|
189 induct_tac "t" 1, |
|
190 Auto_tac]) RS mp; |
|
191 |
|
192 |
|
193 val table_mapf_Some = prove_goal thy "!!f. \\<forall>x y. f x = f y --> x = y ==> \ |
|
194 \ map_of (map (\\<lambda>(k,x). (k,f x)) t) k = Some (f x) --> map_of t k = Some x" (K [ |
|
195 induct_tac "t" 1, |
|
196 Auto_tac]) RS mp; |
|
197 val table_mapf_SomeD = prove_goal thy |
|
198 "map_of (map (\\<lambda>(k,x). (k, f x)) t) k = Some z --> (\\<exists>y. (k,y)\\<in>set t \\<and> z = f y)"(K [ |
|
199 induct_tac "t" 1, |
|
200 Auto_tac]) RS mp; |
|
201 |
|
202 val table_mapf_Some2 = prove_goal thy |
|
203 "!!k. map_of (map (\\<lambda>(k,x). (k,C,x)) t) k = Some (D,x) ==> C = D \\<and> map_of t k = Some x" (K [ |
|
204 forward_tac [table_mapf_SomeD] 1, |
|
205 Auto_tac, |
|
206 rtac table_mapf_Some 1, |
|
207 atac 2, |
|
208 Fast_tac 1]); |
|
209 |
|
210 val finite_map_of = rewrite_rule [dom_def] finite_dom_map_of; |
|
211 |
|
212 Goal |
|
213 "map_of (map (\\<lambda>(a,b). (a,f b)) xs) x = option_map f (map_of xs x)"; |
|
214 by (induct_tac "xs" 1); |
76 by (induct_tac "xs" 1); |
215 auto(); |
77 by Auto_tac; |
216 qed "map_of_map"; |
78 qed "map_of_map"; |
217 |
|
218 |
|