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]
|
|
10 |
"x \\<in> f``A \\<Longrightarrow> \\<exists>y. y \\<in> A \\<and> x = f y";
|
|
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]
|
|
17 |
"(\\<epsilon>(x,y). P x y) = (\\<epsilon>xy. P (fst xy) (snd xy))" (K [rtac refl 1]);
|
|
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]);
|
|
24 |
val splitE2 = prove_goal Prod.thy "\\<lbrakk>Q (split P z); \\<And>x y. \\<lbrakk>z = (x, y); Q (P x y)\\<rbrakk> \\<Longrightarrow> R\\<rbrakk> \\<Longrightarrow> 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 Prod.thy "\\<lbrakk>((\\<lambda>(x,y). P x y) z) w; \\<And>x y. \\<lbrakk>z = (x, y); (P x y) w\\<rbrakk> \\<Longrightarrow> R\\<rbrakk> \\<Longrightarrow> 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 "\\<lbrakk>Ball A P; x \\<notin> A \\<Longrightarrow> Q; P x \\<Longrightarrow> Q \\<rbrakk> \\<Longrightarrow> 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 |
|
|
42 |
Addsimps [Let_def];
|
|
43 |
Addsimps [surjective_pairing RS sym];
|
|
44 |
|
|
45 |
(* To HOL.ML *)
|
|
46 |
|
|
47 |
val ex1_Eps_eq = prove_goal HOL.thy "\\<lbrakk> \\<exists>!x. P x; P y \\<rbrakk> \\<Longrightarrow> Eps P = y"
|
|
48 |
(fn prems => [
|
|
49 |
cut_facts_tac prems 1,
|
|
50 |
rtac select_equality 1,
|
|
51 |
atac 1,
|
|
52 |
etac ex1E 1,
|
|
53 |
etac all_dupE 1,
|
|
54 |
fast_tac HOL_cs 1]);
|
|
55 |
|
|
56 |
|
|
57 |
val ball_insert = prove_goalw equalities.thy [Ball_def]
|
|
58 |
"Ball (insert x A) P = (P x \\<and> Ball A P)" (fn _ => [
|
|
59 |
fast_tac set_cs 1]);
|
|
60 |
|
|
61 |
fun option_case_tac i = EVERY [
|
|
62 |
etac option_caseE i,
|
|
63 |
rotate_tac ~2 (i+1), asm_full_simp_tac HOL_basic_ss (i+1),
|
|
64 |
rotate_tac ~2 i , asm_full_simp_tac HOL_basic_ss i];
|
|
65 |
|
|
66 |
val not_None_tac = EVERY' [dtac (not_None_eq RS iffD1),rotate_tac ~1,etac exE,
|
|
67 |
rotate_tac ~1,asm_full_simp_tac
|
|
68 |
(simpset() delsimps [split_paired_All,split_paired_Ex])];
|
|
69 |
|
|
70 |
fun ex_ftac thm = EVERY' [forward_tac [thm], REPEAT o (etac exE), rotate_tac ~1,
|
|
71 |
asm_full_simp_tac (simpset() delsimps [split_paired_All,split_paired_Ex])];
|
|
72 |
|
|
73 |
val optionE = prove_goal thy
|
|
74 |
"\\<lbrakk> opt = None \\<Longrightarrow> P; \\<And>x. opt = Some x \\<Longrightarrow> P \\<rbrakk> \\<Longrightarrow> P"
|
|
75 |
(fn prems => [
|
|
76 |
case_tac "opt = None" 1,
|
|
77 |
eresolve_tac prems 1,
|
|
78 |
not_None_tac 1,
|
|
79 |
eresolve_tac prems 1]);
|
|
80 |
|
|
81 |
fun option_case_tac2 s i = EVERY [
|
|
82 |
exhaust_tac s i,
|
|
83 |
rotate_tac ~1 (i+1), asm_full_simp_tac HOL_basic_ss (i+1),
|
|
84 |
rotate_tac ~1 i , asm_full_simp_tac HOL_basic_ss i];
|
|
85 |
|
|
86 |
val option_map_SomeD = prove_goalw thy [option_map_def]
|
|
87 |
"\\<And>x. option_map f x = Some y \\<Longrightarrow> \\<exists>z. x = Some z \\<and> f z = y" (K [
|
|
88 |
option_case_tac2 "x" 1,
|
|
89 |
Auto_tac]);
|
|
90 |
|
|
91 |
|
|
92 |
section "unique";
|
|
93 |
|
|
94 |
Goal "(x, y) : set l --> x : fst `` set l";
|
|
95 |
by (induct_tac "l" 1);
|
|
96 |
by Auto_tac;
|
|
97 |
qed_spec_mp "fst_in_set_lemma";
|
|
98 |
|
|
99 |
Goalw [unique_def] "unique []";
|
|
100 |
by (Simp_tac 1);
|
|
101 |
qed "unique_Nil";
|
|
102 |
|
|
103 |
Goalw [unique_def] "unique ((x,y)#l) = (unique l \\<and> (!y. (x,y) ~: set l))";
|
|
104 |
by (auto_tac (claset() addDs [fst_in_set_lemma],simpset()));
|
|
105 |
qed "unique_Cons";
|
|
106 |
|
|
107 |
Addsimps [unique_Nil,unique_Cons];
|
|
108 |
|
|
109 |
Goal "unique l' ==> unique l --> \
|
|
110 |
\ (!(x,y):set l. !(x',y'):set l'. x' ~= x) --> unique (l @ l')";
|
|
111 |
by (induct_tac "l" 1);
|
|
112 |
by (auto_tac (claset() addDs [fst_in_set_lemma],simpset()));
|
|
113 |
qed_spec_mp "unique_append";
|
|
114 |
|
|
115 |
Goal "unique l --> inj f --> unique (map (%(k,x). (f k, g k x)) l)";
|
|
116 |
by (induct_tac "l" 1);
|
|
117 |
by (auto_tac (claset() addDs [fst_in_set_lemma],simpset()));
|
|
118 |
qed_spec_mp "unique_map_inj";
|
|
119 |
|
|
120 |
Goal "\\<And>l. unique l \\<Longrightarrow> unique (map (split (\\<lambda>k. Pair (k, C))) l)";
|
|
121 |
by(etac unique_map_inj 1);
|
|
122 |
by(rtac injI 1);
|
|
123 |
by Auto_tac;
|
|
124 |
qed "unique_map_Pair";
|
|
125 |
|
|
126 |
Goal "\\<lbrakk>M = N; \\<And>x. x\\<in>N \\<Longrightarrow> f x = g x\\<rbrakk> \\<Longrightarrow> f``M = g``N";
|
|
127 |
by(rtac set_ext 1);
|
|
128 |
by(simp_tac (simpset() addsimps image_def::premises()) 1);
|
|
129 |
qed "image_cong";
|
|
130 |
|
|
131 |
val split_Pair_eq = prove_goal Prod.thy
|
|
132 |
"\\<And>X. ((x, y), z) \\<in> split (\\<lambda>x. Pair (x, Y)) `` A \\<Longrightarrow> y = Y" (K [
|
|
133 |
etac imageE 1,
|
|
134 |
split_all_tac 1,
|
|
135 |
auto_tac(claset_of Prod.thy,simpset_of Prod.thy)]);
|
|
136 |
|
|
137 |
|
|
138 |
section "list_all2";
|
|
139 |
|
|
140 |
val list_all2_lengthD = prove_goalw thy [list_all2_def]
|
|
141 |
"\\<And>X. list_all2 P as bs \\<Longrightarrow> length as = length bs" (K [Auto_tac]);
|
|
142 |
|
|
143 |
val list_all2_Nil = prove_goalw thy [list_all2_def]
|
|
144 |
"list_all2 P [] []" (K [Auto_tac]);
|
|
145 |
Addsimps[list_all2_Nil];
|
|
146 |
AddSIs[list_all2_Nil];
|
|
147 |
|
|
148 |
val list_all2_Cons = prove_goalw thy [list_all2_def]
|
|
149 |
"\\<And>X. list_all2 P (a#as) (b#bs) = (P a b \\<and> list_all2 P as bs)" (K [Auto_tac]);
|
|
150 |
AddIffs[list_all2_Cons];
|
|
151 |
|
|
152 |
|
|
153 |
(* More about Maps *)
|
|
154 |
|
|
155 |
val override_SomeD = prove_goalw thy [override_def] "(s \\<oplus> t) k = Some x \\<Longrightarrow> \
|
|
156 |
\ t k = Some x | t k = None \\<and> s k = Some x" (fn prems => [
|
|
157 |
cut_facts_tac prems 1,
|
|
158 |
case_tac "\\<exists>x. t k = Some x" 1,
|
|
159 |
etac exE 1,
|
|
160 |
rotate_tac ~1 1,
|
|
161 |
Asm_full_simp_tac 1,
|
|
162 |
asm_full_simp_tac (HOL_ss addsimps [not_None_eq RS sym]) 1,
|
|
163 |
rotate_tac ~1 1,
|
|
164 |
Asm_full_simp_tac 1]);
|
|
165 |
|
|
166 |
Addsimps [fun_upd_same, fun_upd_other];
|
|
167 |
|
|
168 |
Goal "unique xys \\<longrightarrow> (map_of xys x = Some y) = ((x,y) \\<in> set xys)";
|
|
169 |
by(induct_tac "xys" 1);
|
|
170 |
by(Simp_tac 1);
|
|
171 |
by(force_tac (claset(), simpset() addsimps [unique_Cons]) 1);
|
|
172 |
qed_spec_mp "unique_map_of_Some_conv";
|
|
173 |
|
|
174 |
val in_set_get = unique_map_of_Some_conv RS iffD2;
|
|
175 |
val get_in_set = unique_map_of_Some_conv RS iffD1;
|
|
176 |
|
|
177 |
Goal "(\\<forall>(x,y)\\<in>set l. P x y) \\<longrightarrow> (\\<forall>x. \\<forall>y. map_of l x = Some y \\<longrightarrow> P x y)";
|
|
178 |
by(induct_tac "l" 1);
|
|
179 |
by(ALLGOALS Simp_tac);
|
|
180 |
by Safe_tac;
|
|
181 |
by Auto_tac;
|
|
182 |
bind_thm("Ball_set_table",result() RS mp);
|
|
183 |
|
|
184 |
val table_mono = prove_goal thy
|
|
185 |
"unique l' \\<longrightarrow> (\\<forall>xy. (xy)\\<in>set l \\<longrightarrow> (xy)\\<in>set l') \\<longrightarrow>\
|
|
186 |
\ (\\<forall>k y. map_of l k = Some y \\<longrightarrow> map_of l' k = Some y)" (fn _ => [
|
|
187 |
induct_tac "l" 1,
|
|
188 |
Auto_tac,
|
|
189 |
fast_tac (HOL_cs addSIs [in_set_get]) 1])
|
|
190 |
RS mp RS mp RS spec RS spec RS mp;
|
|
191 |
|
|
192 |
val table_map_Some' = prove_goal thy "map_of t k = Some (k', x) \\<longrightarrow> \
|
|
193 |
\ map_of (map (\\<lambda>u. ((fst u, fst (snd u)), snd (snd u))) t) (k, k') = Some x" (K [
|
|
194 |
induct_tac "t" 1,
|
|
195 |
ALLGOALS Simp_tac,
|
|
196 |
case_tac1 "k = fst a" 1,
|
|
197 |
Auto_tac]) RS mp;
|
|
198 |
val table_map_Some = prove_goal thy
|
|
199 |
"map_of (map (\\<lambda>((k,k'),x). (k,(k',x))) t) k = Some (k',x) \\<longrightarrow> \
|
|
200 |
\map_of t (k, k') = Some x" (K [
|
|
201 |
induct_tac "t" 1,
|
|
202 |
Auto_tac]) RS mp;
|
|
203 |
|
|
204 |
|
|
205 |
val table_mapf_Some = prove_goal thy "\\<And>f. \\<forall>x y. f x = f y \\<longrightarrow> x = y \\<Longrightarrow> \
|
|
206 |
\ map_of (map (\\<lambda>(k,x). (k,f x)) t) k = Some (f x) \\<longrightarrow> map_of t k = Some x" (K [
|
|
207 |
induct_tac "t" 1,
|
|
208 |
Auto_tac]) RS mp;
|
|
209 |
val table_mapf_SomeD = prove_goal thy
|
|
210 |
"map_of (map (\\<lambda>(k,x). (k, f x)) t) k = Some z \\<longrightarrow> (\\<exists>y. (k,y)\\<in>set t \\<and> z = f y)"(K [
|
|
211 |
induct_tac "t" 1,
|
|
212 |
Auto_tac]) RS mp;
|
|
213 |
|
|
214 |
val table_mapf_Some2 = prove_goal thy
|
|
215 |
"\\<And>k. map_of (map (\\<lambda>(k,x). (k,C,x)) t) k = Some (D,x) \\<Longrightarrow> C = D \\<and> map_of t k = Some x" (K [
|
|
216 |
forward_tac [table_mapf_SomeD] 1,
|
|
217 |
Auto_tac,
|
|
218 |
rtac table_mapf_Some 1,
|
|
219 |
atac 2,
|
|
220 |
Fast_tac 1]);
|
|
221 |
|
|
222 |
val finite_map_of = rewrite_rule [dom_def] finite_dom_map_of;
|
|
223 |
|
|
224 |
Goal
|
|
225 |
"map_of (map (\\<lambda>(a,b). (a,f b)) xs) x = option_map f (map_of xs x)";
|
|
226 |
by (induct_tac "xs" 1);
|
|
227 |
auto();
|
|
228 |
qed "map_of_map";
|
|
229 |
|
|
230 |
|