|
1 (* Title: HOL/BCV/JVM.thy |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow |
|
4 Copyright 2000 TUM |
|
5 *) |
|
6 |
|
7 Addsimps [Let_def]; |
|
8 |
|
9 Addsimps [is_type_def]; |
|
10 |
|
11 Goalw [states_def,JVM.sl_def,Opt.sl_def,Err.sl_def, |
|
12 stk_esl_def,reg_sl_def,Product.esl_def, |
|
13 Listn.sl_def,upto_esl_def,JType.esl_def,Err.esl_def] |
|
14 "states S maxs maxr == opt(err((Union {list n (types S) |n. n <= maxs}) <*>\ |
|
15 \ list maxr (err(types S))))"; |
|
16 by(Simp_tac 1); |
|
17 qed "JVM_states_unfold"; |
|
18 |
|
19 Goalw [JVM.le_def,JVM.sl_def,Opt.sl_def,Err.sl_def, |
|
20 stk_esl_def,reg_sl_def,Product.esl_def, |
|
21 Listn.sl_def,upto_esl_def,JType.esl_def,Err.esl_def] |
|
22 "JVM.le S m n == \ |
|
23 \ Opt.le(Err.le(Product.le(Listn.le(subtype S))(Listn.le(Err.le(subtype S)))))"; |
|
24 by(Simp_tac 1); |
|
25 qed "JVM_le_unfold"; |
|
26 |
|
27 Goalw [wfis_def,wfi_def] |
|
28 "[| wfis S md maxr bs; bs!p = Load n; p < size bs |] ==> n < maxr"; |
|
29 by(auto_tac (claset(),simpset()addsimps [all_set_conv_all_nth])); |
|
30 qed "wf_LoadD"; |
|
31 |
|
32 Goalw [wfis_def,wfi_def] |
|
33 "[| wfis S md maxr bs; bs!p = Store n; p < size bs |] ==> n < maxr"; |
|
34 by(auto_tac (claset(),simpset()addsimps [all_set_conv_all_nth])); |
|
35 qed "wf_StoreD"; |
|
36 |
|
37 Goalw [wfis_def,wfi_def] |
|
38 "[| wfis S md m bs; bs!p = New C; p < size bs |] ==> (C,Object):S^*"; |
|
39 by(auto_tac (claset(),simpset()addsimps [all_set_conv_all_nth])); |
|
40 qed "wf_NewD"; |
|
41 |
|
42 Goalw [wfis_def,wfi_def,wf_mdict_def] |
|
43 "[| wfis S md maxr bs; wf_mdict S md; bs!p = Invoke C m pT (Class R); \ |
|
44 \ p < size bs |] ==> (R,Object):S^*"; |
|
45 by(force_tac (claset(),simpset()addsimps [all_set_conv_all_nth]) 1); |
|
46 qed "wf_InvokeD"; |
|
47 |
|
48 Goalw [wfis_def,wfi_def] |
|
49 "[|wfis S md m bs; bs!p = Getfield (Class C) D; p < size bs|] ==> \ |
|
50 \ (C,Object):S^*"; |
|
51 by(auto_tac (claset(),simpset()addsimps [all_set_conv_all_nth])); |
|
52 qed "wf_GetfieldD"; |
|
53 |
|
54 Goal "(? X. (? n. X = A n & P n) & Q X) = (? n. Q(A n) & P n)"; |
|
55 by(Blast_tac 1); |
|
56 qed "special_ex_swap_lemma"; |
|
57 AddIffs [special_ex_swap_lemma]; |
|
58 |
|
59 Goalw [pres_type_def,list_def,step_def,JVM_states_unfold] |
|
60 "[| wfis S md maxr bs; wf_mdict S md |] ==> \ |
|
61 \ pres_type (step S maxs rT bs) (size bs) (states S maxs maxr)"; |
|
62 by(clarify_tac (claset() addSEs [option_map_in_optionI,lift_in_errI]) 1); |
|
63 by(asm_simp_tac (simpset()addsimps [exec_def] addsplits [instr.split]) 1); |
|
64 |
|
65 br conjI 1; |
|
66 by(fast_tac (claset() addDs [refl RS nth_in] addSEs [wf_LoadD] addss |
|
67 (simpset() delsimps [is_type_def]addsplits [err.split])) 1); |
|
68 |
|
69 br conjI 1; |
|
70 by (fast_tac (claset() addDs [set_update_subset_insert RS subsetD] |
|
71 addSEs [wf_StoreD] addss (simpset() addsplits [list.split])) 1); |
|
72 |
|
73 br conjI 1; |
|
74 by (fast_tac (claset() addss (simpset() addsplits [list.split])) 1); |
|
75 |
|
76 br conjI 1; |
|
77 by (fast_tac (claset() addIs [wf_GetfieldD] |
|
78 addss (simpset() addsplits [list.split,ty.split])) 1); |
|
79 |
|
80 br conjI 1; |
|
81 by (fast_tac (claset() addss (simpset() addsplits [list.split])) 1); |
|
82 |
|
83 br conjI 1; |
|
84 by (fast_tac (claset() addIs [wf_NewD] addss simpset()) 1); |
|
85 |
|
86 br conjI 1; |
|
87 by(DEPTH_SOLVE_1(rtac conjI 1 ORELSE |
|
88 Clarify_tac 1 THEN asm_full_simp_tac (simpset() addsimps [wf_InvokeD] |
|
89 addsplits [list.split,ty.split,option.split]) 1)); |
|
90 |
|
91 by (fast_tac (claset() addss (simpset() addsplits [list.split])) 1); |
|
92 |
|
93 qed "exec_pres_type"; |
|
94 |
|
95 Goalw [wti_is_stable_topless_def,wti_def,stable_def,step_def, |
|
96 option_map_def,lift_def,bounded_def,JVM_le_unfold] |
|
97 "[| bounded (succs bs) (size bs) |] ==> \ |
|
98 \ wti_is_stable_topless (JVM.le S maxs maxr) \ |
|
99 \ (Some Err) \ |
|
100 \ (step S maxs rT bs) \ |
|
101 \ (wti S maxs rT bs) \ |
|
102 \ (succs bs) (size bs) (states S maxs maxr)"; |
|
103 by(simp_tac (simpset() addsplits [option.split]) 1); |
|
104 by(simp_tac (simpset() addsplits [err.split]) 1); |
|
105 by(Clarify_tac 1); |
|
106 br conjI 1; |
|
107 by(Blast_tac 1); |
|
108 by(Clarify_tac 1); |
|
109 by(EVERY1[etac allE, mp_tac]); |
|
110 by(rewrite_goals_tac [exec_def,succs_def]); |
|
111 by(split_tac [instr.split] 1); |
|
112 |
|
113 br conjI 1; |
|
114 by(Clarify_tac 1); |
|
115 by(asm_full_simp_tac (simpset() addsplits [option.split,list.split,err.split]) 1); |
|
116 |
|
117 br conjI 1; |
|
118 by(Clarify_tac 1); |
|
119 by(asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1); |
|
120 |
|
121 br conjI 1; |
|
122 by(Clarify_tac 1); |
|
123 by(asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1); |
|
124 |
|
125 br conjI 1; |
|
126 by(Clarify_tac 1); |
|
127 by(asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1); |
|
128 |
|
129 br conjI 1; |
|
130 by(Clarify_tac 1); |
|
131 by(asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1); |
|
132 by(Blast_tac 1); |
|
133 |
|
134 br conjI 1; |
|
135 by(Clarify_tac 1); |
|
136 by(asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1); |
|
137 |
|
138 br conjI 1; |
|
139 by(Clarify_tac 1); |
|
140 by(asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1); |
|
141 |
|
142 br conjI 1; |
|
143 by(Clarify_tac 1); |
|
144 by(asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1); |
|
145 |
|
146 br conjI 1; |
|
147 by(Clarify_tac 1); |
|
148 by(asm_full_simp_tac (simpset() addsplits [option.split,list.split,ty.split]) 1); |
|
149 |
|
150 br conjI 1; |
|
151 by(Clarify_tac 1); |
|
152 by(asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1); |
|
153 by(Blast_tac 1); |
|
154 |
|
155 by(Clarify_tac 1); |
|
156 by(asm_full_simp_tac (simpset() addsplits [option.split,list.split] |
|
157 addsimps [le_list_refl,le_err_refl] ) 1); |
|
158 qed "wti_is_stable_topless"; |
|
159 |
|
160 Goalw [mono_def,step_def,option_map_def,lift_def, |
|
161 JVM_states_unfold,JVM_le_unfold] |
|
162 "[| wfis S md maxr bs; wf_mdict S md |] ==> \ |
|
163 \ mono (JVM.le S maxs maxr) (step S maxs rT bs) (size bs) (states S maxs maxr)"; |
|
164 by (Clarify_tac 1); |
|
165 by(simp_tac (simpset() addsplits [option.split]) 1); |
|
166 by (Clarify_tac 1); |
|
167 by(Asm_simp_tac 1); |
|
168 by(split_tac [err.split] 1); |
|
169 br conjI 1; |
|
170 by (Clarify_tac 1); |
|
171 by (Clarify_tac 1); |
|
172 by(simp_tac (simpset() addsimps [exec_def] delsplits [split_if]) 1); |
|
173 by(split_tac [instr.split] 1); |
|
174 |
|
175 br conjI 1; |
|
176 by (fast_tac (claset() addDs [le_listD] addSEs [wf_LoadD] |
|
177 addss (simpset() addsplits [err.split])) 1); |
|
178 |
|
179 br conjI 1; |
|
180 by (fast_tac (claset() addIs [list_update_le_cong,le_listD] addSEs [wf_StoreD] |
|
181 addss (simpset() addsplits [list.split])) 1); |
|
182 |
|
183 br conjI 1; |
|
184 by(Asm_simp_tac 1); |
|
185 |
|
186 br conjI 1; |
|
187 by(Asm_simp_tac 1); |
|
188 |
|
189 br conjI 1; |
|
190 by(fast_tac (claset() addss (simpset() addsplits [list.split])) 1); |
|
191 |
|
192 br conjI 1; |
|
193 by (fast_tac (claset() addDs [rtrancl_trans] |
|
194 addss (simpset() addsplits [list.split])) 1); |
|
195 |
|
196 br conjI 1; |
|
197 by (Clarify_tac 1); |
|
198 by(asm_full_simp_tac (simpset() addsplits [list.split]) 1); |
|
199 br conjI 1; |
|
200 by (Clarify_tac 1); |
|
201 by (Clarify_tac 1); |
|
202 br conjI 1; |
|
203 by (Clarify_tac 1); |
|
204 by (Clarify_tac 1); |
|
205 br conjI 1; |
|
206 by (Clarify_tac 1); |
|
207 by (Clarify_tac 1); |
|
208 by(Asm_full_simp_tac 1); |
|
209 by (blast_tac (claset() addIs [rtrancl_trans,subtype_transD]) 1); |
|
210 |
|
211 br conjI 1; |
|
212 by(asm_full_simp_tac (simpset() addsimps [reflD] addsplits [list.split]) 1); |
|
213 |
|
214 br conjI 1; |
|
215 (* 39 *) |
|
216 by (Clarify_tac 1); |
|
217 by(asm_full_simp_tac (simpset() addsplits [list.split]) 1); |
|
218 by (blast_tac (claset() addIs [rtrancl_trans,subtype_transD]) 1); |
|
219 |
|
220 br conjI 1; |
|
221 by(fast_tac (claset() addss (simpset() addsplits [list.split,ty.split_asm] |
|
222 addsimps [is_Class_def,is_ref_def])) 1); |
|
223 |
|
224 by(asm_simp_tac (simpset() addsplits [list.split]) 1); |
|
225 by(blast_tac (claset() addIs [subtype_transD]) 1); |
|
226 |
|
227 qed "exec_mono"; |
|
228 |
|
229 |
|
230 Goalw [JVM.sl_def,stk_esl_def,reg_sl_def] |
|
231 "[| univalent S; acyclic S |] ==> semilat(JVM.sl S maxs maxr)"; |
|
232 by(REPEAT(ares_tac [semilat_opt,err_semilat_Product_esl,err_semilat_upto_esl, |
|
233 err_semilat_eslI,semilat_Listn_sl,err_semilat_JType_esl] 1)); |
|
234 qed "semilat_JVM_slI"; |
|
235 |
|
236 Goal "JVM.sl S maxs maxr == \ |
|
237 \ (states S maxs maxr, JVM.le S maxs maxr, JVM.sup S maxs maxr)"; |
|
238 by(simp_tac (simpset() addsimps [states_def,JVM.le_def,JVM.sup_def, |
|
239 surjective_pairing RS sym]) 1); |
|
240 qed "sl_triple_conv"; |
|
241 |
|
242 Goalw [kiljvm_def,sl_triple_conv] |
|
243 "[| univalent S; wf(S^-1); wfis S md maxr bs; wf_mdict S md; \ |
|
244 \ bounded (succs bs) (size bs) |] ==> \ |
|
245 \ is_bcv (JVM.le S maxs maxr) (Some Err) (wti S maxs rT bs) \ |
|
246 \ (size bs) (states S maxs maxr) (kiljvm S maxs maxr rT bs)"; |
|
247 br is_bcv_kildall 1; |
|
248 by(simp_tac (simpset() addsimps [symmetric sl_triple_conv]) 1); |
|
249 by(blast_tac (claset() addSIs [semilat_JVM_slI] addDs [wf_acyclic]) 1); |
|
250 by(simp_tac (simpset() addsimps [JVM_le_unfold]) 1); |
|
251 by(blast_tac (claset() |
|
252 addSIs [acyclic_impl_order_subtype,wf_converse_subcls1_impl_acc_subtype] |
|
253 addDs [wf_acyclic]) 1); |
|
254 by(simp_tac (simpset() addsimps [JVM_le_unfold]) 1); |
|
255 be exec_pres_type 1; |
|
256 ba 1; |
|
257 ba 1; |
|
258 be exec_mono 1; |
|
259 ba 1; |
|
260 be wti_is_stable_topless 1; |
|
261 qed "is_bcv_kiljvm"; |