author | kleing |
Thu, 21 Sep 2000 10:42:49 +0200 | |
changeset 10042 | 7164dc0d24d8 |
parent 9969 | 4753185f1dd2 |
child 10138 | 412a3ced6efd |
permissions | -rw-r--r-- |
8011 | 1 |
(* Title: HOL/MicroJava/J/JBasis.ML |
2 |
ID: $Id$ |
|
3 |
Author: David von Oheimb |
|
4 |
Copyright 1999 TU Muenchen |
|
5 |
*) |
|
6 |
||
7 |
val strip_tac1 = SELECT_GOAL (safe_tac (HOL_cs delrules [conjI, disjE, impCE])); |
|
8 |
||
9 |
Goalw [image_def] |
|
10042 | 10 |
"x \\<in> f``A ==> \\<exists>y. y \\<in> A \\<and> x = f y"; |
8011 | 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 Prod.thy [split_def] |
|
10042 | 17 |
"(SOME (x,y). P x y) = (SOME xy. P (fst xy) (snd xy))" (K [rtac refl 1]); |
8011 | 18 |
|
19 |
||
20 |
val split_beta = prove_goal Prod.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 Prod.thy "(\\<lambda>(x,y). P x y) (w,z) = P w z" |
|
23 |
(fn _ => [Auto_tac]); |
|
10042 | 24 |
val splitE2 = prove_goal Prod.thy "[|Q (split P z); !!x y. [|z = (x, y); Q (P x y)|] ==> R|] ==> R" (fn prems => [ |
8011 | 25 |
REPEAT (resolve_tac (prems@[surjective_pairing]) 1), |
26 |
rtac (split_beta RS subst) 1, |
|
27 |
rtac (hd prems) 1]); |
|
10042 | 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 => [ |
8011 | 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 |
||
10042 | 36 |
val BallE = prove_goal thy "[|Ball A P; x \\<notin> A ==> Q; P x ==> Q |] ==> Q" |
8011 | 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 |
||
42 |
Addsimps [Let_def]; |
|
43 |
||
44 |
(* To HOL.ML *) |
|
45 |
||
10042 | 46 |
val ex1_some_eq_trivial = prove_goal HOL.thy "[| \\<exists>!x. P x; P y |] ==> Eps P = y" |
8011 | 47 |
(fn prems => [ |
48 |
cut_facts_tac prems 1, |
|
9969 | 49 |
rtac some_equality 1, |
8011 | 50 |
atac 1, |
51 |
etac ex1E 1, |
|
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 |
||
8116 | 69 |
Goal "{y. x = Some y} \\<subseteq> {the x}"; |
70 |
by Auto_tac; |
|
71 |
qed "some_subset_the"; |
|
72 |
||
8011 | 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 |
|
10042 | 77 |
"[| opt = None ==> P; !!x. opt = Some x ==> P |] ==> P" |
8011 | 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 [ |
|
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset
|
85 |
case_tac s i, |
8011 | 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] |
|
10042 | 90 |
"!!x. option_map f x = Some y ==> \\<exists>z. x = Some z \\<and> f z = y" (K [ |
8011 | 91 |
option_case_tac2 "x" 1, |
92 |
Auto_tac]); |
|
93 |
||
94 |
||
95 |
section "unique"; |
|
96 |
||
97 |
Goal "(x, y) : set l --> x : fst `` set l"; |
|
98 |
by (induct_tac "l" 1); |
|
99 |
by Auto_tac; |
|
100 |
qed_spec_mp "fst_in_set_lemma"; |
|
101 |
||
102 |
Goalw [unique_def] "unique []"; |
|
103 |
by (Simp_tac 1); |
|
104 |
qed "unique_Nil"; |
|
105 |
||
106 |
Goalw [unique_def] "unique ((x,y)#l) = (unique l \\<and> (!y. (x,y) ~: set l))"; |
|
107 |
by (auto_tac (claset() addDs [fst_in_set_lemma],simpset())); |
|
108 |
qed "unique_Cons"; |
|
109 |
||
110 |
Addsimps [unique_Nil,unique_Cons]; |
|
111 |
||
112 |
Goal "unique l' ==> unique l --> \ |
|
113 |
\ (!(x,y):set l. !(x',y'):set l'. x' ~= x) --> unique (l @ l')"; |
|
114 |
by (induct_tac "l" 1); |
|
115 |
by (auto_tac (claset() addDs [fst_in_set_lemma],simpset())); |
|
116 |
qed_spec_mp "unique_append"; |
|
117 |
||
118 |
Goal "unique l --> inj f --> unique (map (%(k,x). (f k, g k x)) l)"; |
|
119 |
by (induct_tac "l" 1); |
|
8082 | 120 |
by (auto_tac (claset() addDs [fst_in_set_lemma],simpset()addsimps[inj_eq])); |
8011 | 121 |
qed_spec_mp "unique_map_inj"; |
122 |
||
10042 | 123 |
Goal "!!l. unique l ==> unique (map (split (\\<lambda>k. Pair (k, C))) l)"; |
8011 | 124 |
by(etac unique_map_inj 1); |
125 |
by(rtac injI 1); |
|
126 |
by Auto_tac; |
|
127 |
qed "unique_map_Pair"; |
|
128 |
||
10042 | 129 |
Goal "[|M = N; !!x. x\\<in>N ==> f x = g x|] ==> f``M = g``N"; |
8011 | 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 Prod.thy |
|
10042 | 135 |
"!!X. ((x, y), z) \\<in> split (\\<lambda>x. Pair (x, Y)) `` A ==> y = Y" (K [ |
8011 | 136 |
etac imageE 1, |
137 |
split_all_tac 1, |
|
138 |
auto_tac(claset_of Prod.thy,simpset_of Prod.thy)]); |
|
139 |
||
140 |
||
141 |
(* More about Maps *) |
|
142 |
||
10042 | 143 |
val override_SomeD = prove_goalw thy [override_def] "(s \\<oplus> t) k = Some x ==> \ |
8011 | 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 |
||
154 |
Addsimps [fun_upd_same, fun_upd_other]; |
|
155 |
||
10042 | 156 |
Goal "unique xys --> (map_of xys x = Some y) = ((x,y) \\<in> set xys)"; |
8011 | 157 |
by(induct_tac "xys" 1); |
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 |
||
10042 | 165 |
Goal "(\\<forall>(x,y)\\<in>set l. P x y) --> (\\<forall>x. \\<forall>y. map_of l x = Some y --> P x y)"; |
8011 | 166 |
by(induct_tac "l" 1); |
167 |
by(ALLGOALS Simp_tac); |
|
168 |
by Safe_tac; |
|
169 |
by Auto_tac; |
|
170 |
bind_thm("Ball_set_table",result() RS mp); |
|
171 |
||
172 |
val table_mono = prove_goal thy |
|
10042 | 173 |
"unique l' --> (\\<forall>xy. (xy)\\<in>set l --> (xy)\\<in>set l') -->\ |
174 |
\ (\\<forall>k y. map_of l k = Some y --> map_of l' k = Some y)" (fn _ => [ |
|
8011 | 175 |
induct_tac "l" 1, |
176 |
Auto_tac, |
|
177 |
fast_tac (HOL_cs addSIs [in_set_get]) 1]) |
|
178 |
RS mp RS mp RS spec RS spec RS mp; |
|
179 |
||
10042 | 180 |
val table_map_Some' = prove_goal thy "map_of t k = Some (k', x) --> \ |
8011 | 181 |
\ map_of (map (\\<lambda>u. ((fst u, fst (snd u)), snd (snd u))) t) (k, k') = Some x" (K [ |
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 |
|
10042 | 187 |
"map_of (map (\\<lambda>((k,k'),x). (k,(k',x))) t) k = Some (k',x) --> \ |
8011 | 188 |
\map_of t (k, k') = Some x" (K [ |
189 |
induct_tac "t" 1, |
|
190 |
Auto_tac]) RS mp; |
|
191 |
||
192 |
||
10042 | 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 [ |
|
8011 | 195 |
induct_tac "t" 1, |
196 |
Auto_tac]) RS mp; |
|
197 |
val table_mapf_SomeD = prove_goal thy |
|
10042 | 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 [ |
8011 | 199 |
induct_tac "t" 1, |
200 |
Auto_tac]) RS mp; |
|
201 |
||
202 |
val table_mapf_Some2 = prove_goal thy |
|
10042 | 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 [ |
8011 | 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); |
|
215 |
auto(); |
|
216 |
qed "map_of_map"; |
|
217 |
||
218 |