author | nipkow |
Tue, 09 Jan 2001 15:32:27 +0100 | |
changeset 10834 | a7897aebbffc |
parent 10812 | ead84e90bfeb |
child 10897 | 697fab84709e |
permissions | -rw-r--r-- |
10592 | 1 |
(* Title: HOL/BCV/JVM.thy |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow |
|
4 |
Copyright 2000 TUM |
|
5 |
||
6 |
*) |
|
7 |
||
10637 | 8 |
header "Kildall for the JVM" |
10592 | 9 |
|
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10657
diff
changeset
|
10 |
theory JVM = Kildall + JVMType + Opt + Product + DFA_err + StepMono + BVSpec: |
10592 | 11 |
|
12 |
constdefs |
|
13 |
exec :: "jvm_prog \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> instr list \<Rightarrow> nat \<Rightarrow> state \<Rightarrow> state" |
|
14 |
"exec G maxs rT bs == err_step (\<lambda>pc. app (bs!pc) G maxs rT) (\<lambda>pc. step (bs!pc) G)" |
|
15 |
||
16 |
kiljvm :: "jvm_prog => nat => nat => ty => instr list => state list => state list" |
|
17 |
"kiljvm G maxs maxr rT bs == |
|
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10657
diff
changeset
|
18 |
kildall (JVMType.sl G maxs maxr) (exec G maxs rT bs) (\<lambda>pc. succs (bs!pc) pc)" |
10592 | 19 |
|
10637 | 20 |
wt_kil :: "jvm_prog \<Rightarrow> cname \<Rightarrow> ty list \<Rightarrow> ty \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> instr list \<Rightarrow> bool" |
21 |
"wt_kil G C pTs rT mxs mxl ins == |
|
22 |
bounded (\<lambda>n. succs (ins!n) n) (size ins) \<and> 0 < size ins \<and> |
|
23 |
(let first = Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)); |
|
24 |
start = OK first#(replicate (size ins-1) (OK None)); |
|
25 |
result = kiljvm G mxs (1+size pTs+mxl) rT ins start |
|
26 |
in \<forall>n < size ins. result!n \<noteq> Err)" |
|
27 |
||
28 |
wt_jvm_prog_kildall :: "jvm_prog => bool" |
|
29 |
"wt_jvm_prog_kildall G == |
|
30 |
wf_prog (\<lambda>G C (sig,rT,(maxs,maxl,b)). wt_kil G C (snd sig) rT maxs maxl b) G" |
|
10592 | 31 |
|
32 |
||
33 |
lemma special_ex_swap_lemma [iff]: |
|
34 |
"(? X. (? n. X = A n & P n) & Q X) = (? n. Q(A n) & P n)" |
|
35 |
by blast |
|
36 |
||
10630 | 37 |
lemmas [iff del] = not_None_eq |
38 |
||
10592 | 39 |
theorem exec_pres_type: |
40 |
"[| wf_prog wf_mb S |] ==> |
|
41 |
pres_type (exec S maxs rT bs) (size bs) (states S maxs maxr)" |
|
42 |
apply (unfold pres_type_def list_def step_def JVM_states_unfold) |
|
43 |
apply (clarify elim!: option_map_in_optionI lift_in_errI) |
|
44 |
apply (simp add: exec_def err_step_def lift_def split: err.split) |
|
45 |
apply (simp add: step_def option_map_def split: option.splits) |
|
46 |
apply clarify |
|
47 |
apply (case_tac "bs!p") |
|
48 |
||
10637 | 49 |
apply fastsimp |
50 |
apply fastsimp |
|
51 |
apply fastsimp |
|
52 |
apply fastsimp |
|
53 |
apply fastsimp |
|
10592 | 54 |
apply clarsimp |
55 |
defer |
|
10637 | 56 |
apply fastsimp |
57 |
apply fastsimp |
|
10592 | 58 |
apply clarsimp |
59 |
defer |
|
10637 | 60 |
apply fastsimp |
61 |
apply fastsimp |
|
62 |
apply fastsimp |
|
63 |
apply fastsimp |
|
64 |
apply fastsimp |
|
65 |
apply fastsimp |
|
66 |
apply fastsimp |
|
67 |
apply fastsimp |
|
68 |
apply fastsimp |
|
10592 | 69 |
defer |
70 |
||
10637 | 71 |
(* Invoke *) |
10592 | 72 |
apply (simp add: Un_subset_iff) |
10630 | 73 |
apply (drule method_wf_mdecl, assumption+) |
10592 | 74 |
apply (simp add: wf_mdecl_def wf_mhead_def) |
75 |
||
10637 | 76 |
(* Getfield *) |
10630 | 77 |
apply (rule_tac fn = "(vname,cname)" in fields_is_type) |
78 |
defer |
|
79 |
apply assumption+ |
|
80 |
apply (simp add: field_def) |
|
81 |
apply (drule map_of_SomeD) |
|
82 |
apply (rule map_of_SomeI) |
|
83 |
apply (auto simp add: unique_fields) |
|
10592 | 84 |
done |
85 |
||
10630 | 86 |
|
87 |
lemmas [iff] = not_None_eq |
|
88 |
||
89 |
||
10592 | 90 |
theorem exec_mono: |
91 |
"wf_prog wf_mb G ==> |
|
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10657
diff
changeset
|
92 |
mono (JVMType.le G maxs maxr) (exec G maxs rT bs) (size bs) (states G maxs maxr)" |
10592 | 93 |
apply (unfold mono_def) |
94 |
apply clarify |
|
95 |
apply (unfold lesub_def) |
|
96 |
apply (case_tac t) |
|
97 |
apply (simp add: JVM_le_unfold Err.le_def exec_def err_step_def lift_def) |
|
98 |
apply (case_tac s) |
|
99 |
apply (simp add: JVM_le_unfold Err.le_def exec_def err_step_def lift_def) |
|
100 |
apply (simp add: JVM_le_convert exec_def err_step_def lift_def) |
|
101 |
apply (simp add: JVM_le_unfold Err.le_def exec_def err_step_def lift_def) |
|
102 |
apply (rule conjI) |
|
103 |
apply clarify |
|
104 |
apply (rule step_mono, assumption+) |
|
105 |
apply (rule impI) |
|
106 |
apply (erule contrapos_nn) |
|
107 |
apply (rule app_mono, assumption+) |
|
108 |
done |
|
109 |
||
110 |
theorem semilat_JVM_slI: |
|
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10657
diff
changeset
|
111 |
"[| wf_prog wf_mb G |] ==> semilat (JVMType.sl G maxs maxr)" |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10657
diff
changeset
|
112 |
apply (unfold JVMType.sl_def stk_esl_def reg_sl_def) |
10592 | 113 |
apply (rule semilat_opt) |
114 |
apply (rule err_semilat_Product_esl) |
|
115 |
apply (rule err_semilat_upto_esl) |
|
116 |
apply (rule err_semilat_JType_esl, assumption+) |
|
117 |
apply (rule err_semilat_eslI) |
|
118 |
apply (rule semilat_Listn_sl) |
|
119 |
apply (rule err_semilat_JType_esl, assumption+) |
|
120 |
done |
|
121 |
||
122 |
lemma sl_triple_conv: |
|
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10657
diff
changeset
|
123 |
"JVMType.sl G maxs maxr == |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10657
diff
changeset
|
124 |
(states G maxs maxr, JVMType.le G maxs maxr, JVMType.sup G maxs maxr)" |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10657
diff
changeset
|
125 |
by (simp (no_asm) add: states_def JVMType.le_def JVMType.sup_def) |
10592 | 126 |
|
127 |
||
128 |
theorem is_bcv_kiljvm: |
|
129 |
"[| wf_prog wf_mb G; bounded (\<lambda>pc. succs (bs!pc) pc) (size bs) |] ==> |
|
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10657
diff
changeset
|
130 |
is_bcv (JVMType.le G maxs maxr) Err (exec G maxs rT bs) (\<lambda>pc. succs (bs!pc) pc) |
10592 | 131 |
(size bs) (states G maxs maxr) (kiljvm G maxs maxr rT bs)" |
132 |
apply (unfold kiljvm_def sl_triple_conv) |
|
133 |
apply (rule is_bcv_kildall) |
|
134 |
apply (simp (no_asm) add: sl_triple_conv [symmetric]) |
|
135 |
apply (force intro!: semilat_JVM_slI dest: wf_acyclic simp add: symmetric sl_triple_conv) |
|
136 |
apply (simp (no_asm) add: JVM_le_unfold) |
|
137 |
apply (blast intro!: order_widen wf_converse_subcls1_impl_acc_subtype |
|
138 |
dest: wf_subcls1 wf_acyclic) |
|
139 |
apply (simp add: JVM_le_unfold) |
|
140 |
apply (erule exec_pres_type) |
|
141 |
apply assumption |
|
142 |
apply (erule exec_mono) |
|
143 |
done |
|
144 |
||
10637 | 145 |
|
146 |
theorem wt_kil_correct: |
|
147 |
"[| wt_kil G C pTs rT maxs mxl bs; wf_prog wf_mb G; |
|
10592 | 148 |
is_class G C; \<forall>x \<in> set pTs. is_type G x |] |
149 |
==> \<exists>phi. wt_method G C pTs rT maxs mxl bs phi" |
|
150 |
proof - |
|
151 |
let ?start = "OK (Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err))) |
|
152 |
#(replicate (size bs-1) (OK None))" |
|
153 |
||
10637 | 154 |
assume wf: "wf_prog wf_mb G" |
155 |
assume isclass: "is_class G C" |
|
156 |
assume istype: "\<forall>x \<in> set pTs. is_type G x" |
|
157 |
||
158 |
assume "wt_kil G C pTs rT maxs mxl bs" |
|
159 |
then obtain maxr r where |
|
160 |
bounded: "bounded (\<lambda>pc. succs (bs!pc) pc) (size bs)" and |
|
161 |
result: "r = kiljvm G maxs maxr rT bs ?start" and |
|
162 |
success: "\<forall>n < size bs. r!n \<noteq> Err" and |
|
163 |
instrs: "0 < size bs" and |
|
164 |
maxr: "maxr = Suc (length pTs + mxl)" |
|
165 |
by (unfold wt_kil_def) simp |
|
10592 | 166 |
|
167 |
{ fix pc |
|
168 |
have "succs (bs!pc) pc \<noteq> []" |
|
169 |
by (cases "bs!pc") auto |
|
170 |
} |
|
171 |
||
172 |
hence non_empty: "non_empty (\<lambda>pc. succs (bs!pc) pc)" |
|
173 |
by (unfold non_empty_def) blast |
|
174 |
||
175 |
from wf bounded |
|
176 |
have bcv: |
|
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10657
diff
changeset
|
177 |
"is_bcv (JVMType.le G maxs maxr) Err (exec G maxs rT bs) (\<lambda>pc. succs (bs!pc) pc) |
10592 | 178 |
(size bs) (states G maxs maxr) (kiljvm G maxs maxr rT bs)" |
179 |
by (rule is_bcv_kiljvm) |
|
180 |
||
181 |
{ fix l x |
|
182 |
have "set (replicate l x) \<subseteq> {x}" |
|
183 |
by (cases "0 < l") simp+ |
|
184 |
} note subset_replicate = this |
|
185 |
||
186 |
from istype |
|
187 |
have "set pTs \<subseteq> types G" |
|
188 |
by auto |
|
189 |
||
10834 | 190 |
hence "OK ` set pTs \<subseteq> err (types G)" |
10592 | 191 |
by auto |
192 |
||
193 |
with instrs maxr isclass |
|
194 |
have "?start \<in> list (length bs) (states G maxs maxr)" |
|
195 |
apply (unfold list_def JVM_states_unfold) |
|
196 |
apply simp |
|
197 |
apply (rule conjI) |
|
198 |
apply (simp add: Un_subset_iff) |
|
199 |
apply (rule_tac B = "{Err}" in subset_trans) |
|
200 |
apply (simp add: subset_replicate) |
|
201 |
apply simp |
|
202 |
apply (rule_tac B = "{OK None}" in subset_trans) |
|
203 |
apply (simp add: subset_replicate) |
|
204 |
apply simp |
|
205 |
done |
|
206 |
||
207 |
with bcv success result |
|
208 |
have |
|
209 |
"\<exists>ts\<in>list (length bs) (states G maxs maxr). |
|
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10657
diff
changeset
|
210 |
?start <=[JVMType.le G maxs maxr] ts \<and> |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10657
diff
changeset
|
211 |
welltyping (JVMType.le G maxs maxr) Err (exec G maxs rT bs) (\<lambda>pc. succs (bs ! pc) pc) ts" |
10592 | 212 |
by (unfold is_bcv_def) auto |
213 |
||
214 |
then obtain phi' where |
|
215 |
l: "phi' \<in> list (length bs) (states G maxs maxr)" and |
|
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10657
diff
changeset
|
216 |
s: "?start <=[JVMType.le G maxs maxr] phi'" and |
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10657
diff
changeset
|
217 |
w: "welltyping (JVMType.le G maxs maxr) Err (exec G maxs rT bs) (\<lambda>pc. succs (bs ! pc) pc) phi'" |
10592 | 218 |
by blast |
219 |
||
220 |
hence dynamic: |
|
221 |
"dynamic_wt (sup_state_opt G) (exec G maxs rT bs) (\<lambda>pc. succs (bs ! pc) pc) phi'" |
|
222 |
by (simp add: dynamic_wt_def exec_def JVM_le_Err_conv) |
|
223 |
||
224 |
from s |
|
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10657
diff
changeset
|
225 |
have le: "JVMType.le G maxs maxr (?start ! 0) (phi'!0)" |
10592 | 226 |
by (drule_tac p=0 in le_listD) (simp add: lesub_def)+ |
227 |
||
228 |
from l |
|
229 |
have l: "size phi' = size bs" |
|
230 |
by simp |
|
231 |
||
232 |
with instrs w |
|
233 |
have "phi' ! 0 \<noteq> Err" |
|
234 |
by (unfold welltyping_def) simp |
|
235 |
||
236 |
with instrs l |
|
237 |
have phi0: "OK (map ok_val phi' ! 0) = phi' ! 0" |
|
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10657
diff
changeset
|
238 |
by (clarsimp simp add: not_Err_eq) |
10592 | 239 |
|
240 |
from l bounded |
|
241 |
have "bounded (\<lambda>pc. succs (bs ! pc) pc) (length phi')" |
|
242 |
by simp |
|
243 |
||
244 |
with dynamic non_empty |
|
245 |
have "static_wt (sup_state_opt G) (\<lambda>pc. app (bs!pc) G maxs rT) (\<lambda>pc. step (bs!pc) G) |
|
246 |
(\<lambda>pc. succs (bs!pc) pc) (map ok_val phi')" |
|
247 |
by (auto intro: dynamic_imp_static simp add: exec_def) |
|
248 |
||
249 |
with instrs l le bounded |
|
250 |
have "wt_method G C pTs rT maxs mxl bs (map ok_val phi')" |
|
251 |
apply (unfold wt_method_def static_wt_def) |
|
252 |
apply simp |
|
253 |
apply (rule conjI) |
|
254 |
apply (unfold wt_start_def) |
|
255 |
apply (rule JVM_le_convert [THEN iffD1]) |
|
256 |
apply (simp (no_asm) add: phi0) |
|
257 |
apply clarify |
|
258 |
apply (erule allE, erule impE, assumption) |
|
259 |
apply (elim conjE) |
|
260 |
apply (clarsimp simp add: lesub_def wt_instr_def) |
|
261 |
apply (unfold bounded_def) |
|
262 |
apply blast |
|
263 |
done |
|
264 |
||
265 |
thus ?thesis by blast |
|
266 |
qed |
|
267 |
||
10651 | 268 |
|
10657 | 269 |
(* there's still one easy, and one nontrivial (but provable) sorry in here *) |
270 |
(* |
|
10651 | 271 |
theorem wt_kil_complete: |
272 |
"[| wt_method G C pTs rT maxs mxl bs phi; wf_prog wf_mb G; |
|
273 |
length phi = length bs; is_class G C; \<forall>x \<in> set pTs. is_type G x |] |
|
274 |
==> wt_kil G C pTs rT maxs mxl bs" |
|
275 |
proof - |
|
276 |
assume wf: "wf_prog wf_mb G" |
|
277 |
assume isclass: "is_class G C" |
|
278 |
assume istype: "\<forall>x \<in> set pTs. is_type G x" |
|
279 |
assume length: "length phi = length bs" |
|
280 |
||
281 |
assume "wt_method G C pTs rT maxs mxl bs phi" |
|
282 |
then obtain |
|
283 |
instrs: "0 < length bs" and |
|
284 |
wt_start: "wt_start G C pTs mxl phi" and |
|
285 |
wt_ins: "\<forall>pc. pc < length bs \<longrightarrow> |
|
286 |
wt_instr (bs ! pc) G rT phi maxs (length bs) pc" |
|
287 |
by (unfold wt_method_def) simp |
|
288 |
||
289 |
let ?succs = "\<lambda>pc. succs (bs!pc) pc" |
|
290 |
let ?step = "\<lambda>pc. step (bs!pc) G" |
|
291 |
let ?app = "\<lambda>pc. app (bs!pc) G maxs rT" |
|
292 |
||
293 |
from wt_ins |
|
294 |
have bounded: "bounded ?succs (size bs)" |
|
295 |
by (unfold wt_instr_def bounded_def) blast |
|
296 |
||
297 |
from wt_ins |
|
298 |
have "static_wt (sup_state_opt G) ?app ?step ?succs phi" |
|
299 |
apply (unfold static_wt_def wt_instr_def lesub_def) |
|
300 |
apply (simp (no_asm) only: length) |
|
301 |
apply blast |
|
302 |
done |
|
303 |
||
304 |
with bounded |
|
305 |
have "dynamic_wt (sup_state_opt G) (err_step ?app ?step) ?succs (map OK phi)" |
|
306 |
by - (erule static_imp_dynamic, simp add: length) |
|
307 |
||
308 |
hence dynamic: |
|
309 |
"dynamic_wt (sup_state_opt G) (exec G maxs rT bs) ?succs (map OK phi)" |
|
310 |
by (unfold exec_def) |
|
311 |
||
312 |
let ?maxr = "1+size pTs+mxl" |
|
313 |
||
314 |
from wf bounded |
|
315 |
have is_bcv: |
|
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10657
diff
changeset
|
316 |
"is_bcv (JVMType.le G maxs ?maxr) Err (exec G maxs rT bs) ?succs |
10651 | 317 |
(size bs) (states G maxs ?maxr) (kiljvm G maxs ?maxr rT bs)" |
318 |
by (rule is_bcv_kiljvm) |
|
319 |
||
320 |
let ?start = "OK (Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err))) |
|
321 |
#(replicate (size bs-1) (OK None))" |
|
322 |
||
323 |
{ fix l x |
|
324 |
have "set (replicate l x) \<subseteq> {x}" |
|
325 |
by (cases "0 < l") simp+ |
|
326 |
} note subset_replicate = this |
|
327 |
||
328 |
from istype |
|
329 |
have "set pTs \<subseteq> types G" |
|
330 |
by auto |
|
331 |
||
10834 | 332 |
hence "OK ` set pTs \<subseteq> err (types G)" |
10651 | 333 |
by auto |
334 |
||
335 |
with instrs isclass |
|
336 |
have start: |
|
337 |
"?start \<in> list (length bs) (states G maxs ?maxr)" |
|
338 |
apply (unfold list_def JVM_states_unfold) |
|
339 |
apply simp |
|
340 |
apply (rule conjI) |
|
341 |
apply (simp add: Un_subset_iff) |
|
342 |
apply (rule_tac B = "{Err}" in subset_trans) |
|
343 |
apply (simp add: subset_replicate) |
|
344 |
apply simp |
|
345 |
apply (rule_tac B = "{OK None}" in subset_trans) |
|
346 |
apply (simp add: subset_replicate) |
|
347 |
apply simp |
|
348 |
done |
|
349 |
||
350 |
let ?phi = "map OK phi" |
|
351 |
||
352 |
have 1: "?phi \<in> list (length bs) (states G maxs ?maxr)" sorry |
|
353 |
||
10657 | 354 |
have 2: "?start <=[le G maxs ?maxr] ?phi" |
355 |
proof - |
|
356 |
{ fix n |
|
357 |
from wt_start |
|
358 |
have "G \<turnstile> ok_val (?start!0) <=' phi!0" |
|
359 |
by (simp add: wt_start_def) |
|
360 |
moreover |
|
361 |
from instrs length |
|
362 |
have "0 < length phi" by simp |
|
363 |
ultimately |
|
364 |
have "le G maxs ?maxr (?start!0) (?phi!0)" |
|
365 |
by (simp add: JVM_le_Err_conv Err.le_def lesub_def) |
|
366 |
moreover |
|
367 |
{ fix n' |
|
368 |
have "le G maxs ?maxr (OK None) (?phi!n)" |
|
369 |
by (auto simp add: JVM_le_Err_conv Err.le_def lesub_def |
|
370 |
split: err.splits) |
|
371 |
hence "[| n = Suc n'; n < length ?start |] |
|
372 |
==> le G maxs ?maxr (?start!n) (?phi!n)" |
|
373 |
by simp |
|
374 |
} |
|
375 |
ultimately |
|
376 |
have "n < length ?start ==> le G maxs ?maxr (?start!n) (?phi!n)" |
|
377 |
by - (cases n, blast+) |
|
378 |
} |
|
379 |
thus ?thesis sorry |
|
380 |
qed |
|
10651 | 381 |
|
382 |
from dynamic |
|
383 |
have "welltyping (le G maxs ?maxr) Err (exec G maxs rT bs) ?succs ?phi" |
|
384 |
by (simp add: dynamic_wt_def JVM_le_Err_conv) |
|
385 |
||
386 |
with start 1 2 is_bcv |
|
387 |
have "\<forall>p. p < length bs \<longrightarrow> kiljvm G maxs ?maxr rT bs ?start ! p \<noteq> Err" |
|
388 |
by (unfold is_bcv_def) blast |
|
389 |
||
390 |
with bounded instrs |
|
391 |
show "wt_kil G C pTs rT maxs mxl bs" |
|
392 |
by (unfold wt_kil_def) simp |
|
393 |
qed |
|
10657 | 394 |
*) |
10651 | 395 |
|
10637 | 396 |
lemma is_type_pTs: |
397 |
"[| wf_prog wf_mb G; (C,S,fs,mdecls) \<in> set G; (sig,rT,code) \<in> set mdecls; |
|
398 |
t \<in> set (snd sig) |] |
|
399 |
==> is_type G t" |
|
400 |
proof - |
|
401 |
assume "wf_prog wf_mb G" |
|
402 |
"(C,S,fs,mdecls) \<in> set G" |
|
403 |
"(sig,rT,code) \<in> set mdecls" |
|
404 |
hence "wf_mdecl wf_mb G C (sig,rT,code)" |
|
405 |
by (unfold wf_prog_def wf_cdecl_def) auto |
|
406 |
hence "\<forall>t \<in> set (snd sig). is_type G t" |
|
407 |
by (unfold wf_mdecl_def wf_mhead_def) auto |
|
408 |
moreover |
|
409 |
assume "t \<in> set (snd sig)" |
|
410 |
ultimately |
|
411 |
show ?thesis by blast |
|
412 |
qed |
|
413 |
||
414 |
||
415 |
theorem jvm_kildall_correct: |
|
416 |
"wt_jvm_prog_kildall G ==> \<exists>Phi. wt_jvm_prog G Phi" |
|
417 |
proof - |
|
418 |
assume wtk: "wt_jvm_prog_kildall G" |
|
419 |
||
420 |
then obtain wf_mb where |
|
421 |
wf: "wf_prog wf_mb G" |
|
422 |
by (auto simp add: wt_jvm_prog_kildall_def) |
|
423 |
||
424 |
let ?Phi = "\<lambda>C sig. let (C,rT,(maxs,maxl,ins)) = the (method (G,C) sig) in |
|
425 |
SOME phi. wt_method G C (snd sig) rT maxs maxl ins phi" |
|
426 |
||
427 |
{ fix C S fs mdecls sig rT code |
|
428 |
assume "(C,S,fs,mdecls) \<in> set G" "(sig,rT,code) \<in> set mdecls" |
|
429 |
with wf |
|
430 |
have "method (G,C) sig = Some (C,rT,code) \<and> is_class G C \<and> (\<forall>t \<in> set (snd sig). is_type G t)" |
|
431 |
by (simp add: methd is_type_pTs) |
|
432 |
} note this [simp] |
|
433 |
||
434 |
from wtk |
|
435 |
have "wt_jvm_prog G ?Phi" |
|
436 |
apply (unfold wt_jvm_prog_def wt_jvm_prog_kildall_def wf_prog_def wf_cdecl_def) |
|
437 |
apply clarsimp |
|
438 |
apply (drule bspec, assumption) |
|
439 |
apply (unfold wf_mdecl_def) |
|
440 |
apply clarsimp |
|
441 |
apply (drule bspec, assumption) |
|
442 |
apply clarsimp |
|
443 |
apply (drule wt_kil_correct [OF _ wf]) |
|
444 |
apply (auto intro: someI) |
|
445 |
done |
|
446 |
||
447 |
thus ?thesis by blast |
|
448 |
qed |
|
449 |
||
10592 | 450 |
end |