9 theory JTypeSafe = Eval + Conform: |
9 theory JTypeSafe = Eval + Conform: |
10 |
10 |
11 declare split_beta [simp] |
11 declare split_beta [simp] |
12 |
12 |
13 lemma NewC_conforms: |
13 lemma NewC_conforms: |
14 "[|h a = None; (h, l)::\<preceq>(G, lT); wf_prog wf_mb G; is_class G C|] ==> |
14 "[|h a = None; (x,(h, l))::\<preceq>(G, lT); wf_prog wf_mb G; is_class G C|] ==> |
15 (h(a\<mapsto>(C,(init_vars (fields (G,C))))), l)::\<preceq>(G, lT)" |
15 (x,(h(a\<mapsto>(C,(init_vars (fields (G,C))))), l))::\<preceq>(G, lT)" |
16 apply( erule conforms_upd_obj) |
16 apply( erule conforms_upd_obj) |
17 apply( unfold oconf_def) |
17 apply( unfold oconf_def) |
18 apply( auto dest!: fields_is_type) |
18 apply( auto dest!: fields_is_type) |
19 done |
19 done |
20 |
20 |
28 apply( clarify) |
28 apply( clarify) |
29 apply( drule (1) non_npD) |
29 apply( drule (1) non_npD) |
30 apply( auto intro!: conf_AddrI simp add: obj_ty_def) |
30 apply( auto intro!: conf_AddrI simp add: obj_ty_def) |
31 done |
31 done |
32 |
32 |
|
33 |
|
34 |
33 lemma FAcc_type_sound: |
35 lemma FAcc_type_sound: |
34 "[| wf_prog wf_mb G; field (G,C) fn = Some (fd, ft); (h,l)::\<preceq>(G,lT); |
36 "[| wf_prog wf_mb G; field (G,C) fn = Some (fd, ft); (x,(h,l))::\<preceq>(G,lT); |
35 x' = None --> G,h\<turnstile>a'::\<preceq> Class C; np a' x' = None |] ==> |
37 x' = None --> G,h\<turnstile>a'::\<preceq> Class C; np a' x' = None |] ==> |
36 G,h\<turnstile>the (snd (the (h (the_Addr a'))) (fn, fd))::\<preceq>ft" |
38 G,h\<turnstile>the (snd (the (h (the_Addr a'))) (fn, fd))::\<preceq>ft" |
37 apply( drule np_NoneD) |
39 apply( drule np_NoneD) |
38 apply( erule conjE) |
40 apply( erule conjE) |
39 apply( erule (1) notE impE) |
41 apply( erule (1) notE impE) |
50 "[| wf_prog wf_mb G; a = the_Addr a'; (c, fs) = the (h a); |
52 "[| wf_prog wf_mb G; a = the_Addr a'; (c, fs) = the (h a); |
51 (G, lT)\<turnstile>v::T'; G\<turnstile>T'\<preceq>ft; |
53 (G, lT)\<turnstile>v::T'; G\<turnstile>T'\<preceq>ft; |
52 (G, lT)\<turnstile>aa::Class C; |
54 (G, lT)\<turnstile>aa::Class C; |
53 field (G,C) fn = Some (fd, ft); h''\<le>|h'; |
55 field (G,C) fn = Some (fd, ft); h''\<le>|h'; |
54 x' = None --> G,h'\<turnstile>a'::\<preceq> Class C; h'\<le>|h; |
56 x' = None --> G,h'\<turnstile>a'::\<preceq> Class C; h'\<le>|h; |
55 (h, l)::\<preceq>(G, lT); G,h\<turnstile>x::\<preceq>T'; np a' x' = None|] ==> |
57 Norm (h, l)::\<preceq>(G, lT); G,h\<turnstile>x::\<preceq>T'; np a' x' = None|] ==> |
56 h''\<le>|h(a\<mapsto>(c,(fs((fn,fd)\<mapsto>x)))) \<and> |
58 h''\<le>|h(a\<mapsto>(c,(fs((fn,fd)\<mapsto>x)))) \<and> |
57 (h(a\<mapsto>(c,(fs((fn,fd)\<mapsto>x)))), l)::\<preceq>(G, lT) \<and> |
59 Norm(h(a\<mapsto>(c,(fs((fn,fd)\<mapsto>x)))), l)::\<preceq>(G, lT) \<and> |
58 G,h(a\<mapsto>(c,(fs((fn,fd)\<mapsto>x))))\<turnstile>x::\<preceq>T'" |
60 G,h(a\<mapsto>(c,(fs((fn,fd)\<mapsto>x))))\<turnstile>x::\<preceq>T'" |
59 apply( drule np_NoneD) |
61 apply( drule np_NoneD) |
60 apply( erule conjE) |
62 apply( erule conjE) |
61 apply( simp) |
63 apply( simp) |
62 apply( drule non_np_objD) |
64 apply( drule non_np_objD) |
104 apply( assumption) |
108 apply( assumption) |
105 apply( erule (2) conf_list_gext_widen) |
109 apply( erule (2) conf_list_gext_widen) |
106 done |
110 done |
107 |
111 |
108 lemma Call_type_sound: |
112 lemma Call_type_sound: |
109 "[| wf_java_prog G; a' \<noteq> Null; (h, l)::\<preceq>(G, lT); class G C = Some y; |
113 "[| wf_java_prog G; a' \<noteq> Null; Norm (h, l)::\<preceq>(G, lT); class G C = Some y; |
110 max_spec G C (mn,pTsa) = {((mda,rTa),pTs')}; xc\<le>|xh; xh\<le>|h; |
114 max_spec G C (mn,pTsa) = {((mda,rTa),pTs')}; xc\<le>|xh; xh\<le>|h; |
111 list_all2 (conf G h) pvs pTsa; |
115 list_all2 (conf G h) pvs pTsa; |
112 (md, rT, pns, lvars, blk, res) = |
116 (md, rT, pns, lvars, blk, res) = |
113 the (method (G,fst (the (h (the_Addr a')))) (mn, pTs')); |
117 the (method (G,fst (the (h (the_Addr a')))) (mn, pTs')); |
114 \<forall>lT. (h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a'))::\<preceq>(G, lT) --> |
118 \<forall>lT. (np a' None, h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a'))::\<preceq>(G, lT) --> |
115 (G, lT)\<turnstile>blk\<surd> --> h\<le>|xi \<and> (xi, xl)::\<preceq>(G, lT); |
119 (G, lT)\<turnstile>blk\<surd> --> h\<le>|xi \<and> (xcptb, xi, xl)::\<preceq>(G, lT); |
116 \<forall>lT. (xi, xl)::\<preceq>(G, lT) --> (\<forall>T. (G, lT)\<turnstile>res::T --> |
120 \<forall>lT. (xcptb,xi, xl)::\<preceq>(G, lT) --> (\<forall>T. (G, lT)\<turnstile>res::T --> |
117 xi\<le>|h' \<and> (h', xj)::\<preceq>(G, lT) \<and> (x' = None --> G,h'\<turnstile>v::\<preceq>T)); |
121 xi\<le>|h' \<and> (x',h', xj)::\<preceq>(G, lT) \<and> (x' = None --> G,h'\<turnstile>v::\<preceq>T)); |
118 G,xh\<turnstile>a'::\<preceq> Class C |] ==> |
122 G,xh\<turnstile>a'::\<preceq> Class C |
119 xc\<le>|h' \<and> (h', l)::\<preceq>(G, lT) \<and> (x' = None --> G,h'\<turnstile>v::\<preceq>rTa)" |
123 |] ==> |
|
124 xc\<le>|h' \<and> (x',(h', l))::\<preceq>(G, lT) \<and> (x' = None --> G,h'\<turnstile>v::\<preceq>rTa)" |
120 apply( drule max_spec2mheads) |
125 apply( drule max_spec2mheads) |
121 apply( clarify) |
126 apply( clarify) |
122 apply( drule (2) non_np_objD') |
127 apply( drule (2) non_np_objD') |
123 apply( clarsimp) |
128 apply( clarsimp) |
124 apply( frule (1) hext_objD) |
129 apply( frule (1) hext_objD) |
125 apply( clarsimp) |
130 apply( clarsimp) |
126 apply( drule (3) Call_lemma) |
131 apply( drule (3) Call_lemma) |
127 apply( clarsimp simp add: wf_java_mdecl_def) |
132 apply( clarsimp simp add: wf_java_mdecl_def) |
128 apply( erule_tac V = "method ?sig ?x = ?y" in thin_rl) |
133 apply( erule_tac V = "method ?sig ?x = ?y" in thin_rl) |
129 apply( drule spec, erule impE) |
134 apply( drule spec, erule impE, erule_tac [2] notE impE, tactic "assume_tac 2") |
130 apply( erule_tac [2] notE impE, tactic "assume_tac 2") |
|
131 apply( rule conformsI) |
135 apply( rule conformsI) |
132 apply( erule conforms_heapD) |
136 apply( erule conforms_heapD) |
133 apply( rule lconf_ext) |
137 apply( rule lconf_ext) |
134 apply( force elim!: Call_lemma2) |
138 apply( force elim!: Call_lemma2) |
135 apply( erule conf_hext, erule (1) conf_obj_AddrI) |
139 apply( erule conf_hext, erule (1) conf_obj_AddrI) |
136 apply( erule_tac V = "?E\<turnstile>?blk\<surd>" in thin_rl) |
140 apply( erule_tac V = "?E\<turnstile>?blk\<surd>" in thin_rl) |
|
141 apply (simp add: conforms_def) |
|
142 |
137 apply( erule conjE) |
143 apply( erule conjE) |
138 apply( drule spec, erule (1) impE) |
144 apply( drule spec, erule (1) impE) |
139 apply( drule spec, erule (1) impE) |
145 apply( drule spec, erule (1) impE) |
140 apply( erule_tac V = "?E\<turnstile>res::?rT" in thin_rl) |
146 apply( erule_tac V = "?E\<turnstile>res::?rT" in thin_rl) |
141 apply( clarify) |
147 apply( clarify) |
147 apply( frule_tac [2] conf_widen) |
153 apply( frule_tac [2] conf_widen) |
148 apply( tactic "assume_tac 4") |
154 apply( tactic "assume_tac 4") |
149 apply( tactic "assume_tac 2") |
155 apply( tactic "assume_tac 2") |
150 prefer 2 |
156 prefer 2 |
151 apply( fast elim!: widen_trans) |
157 apply( fast elim!: widen_trans) |
152 apply( erule conforms_hext) |
158 apply (rule conforms_xcpt_change) |
|
159 apply( rule conforms_hext) apply assumption |
|
160 (* apply( erule conforms_hext)*) |
153 apply( erule (1) hext_trans) |
161 apply( erule (1) hext_trans) |
154 apply( erule conforms_heapD) |
162 apply( erule conforms_heapD) |
155 done |
163 apply (simp add: conforms_def) |
|
164 done |
|
165 |
|
166 |
156 |
167 |
157 declare split_if [split del] |
168 declare split_if [split del] |
158 declare fun_upd_apply [simp del] |
169 declare fun_upd_apply [simp del] |
159 declare fun_upd_same [simp] |
170 declare fun_upd_same [simp] |
160 ML{* |
171 ML{* |
163 *} |
174 *} |
164 ML{* |
175 ML{* |
165 Unify.search_bound := 40; |
176 Unify.search_bound := 40; |
166 Unify.trace_bound := 40 |
177 Unify.trace_bound := 40 |
167 *} |
178 *} |
|
179 |
|
180 |
168 theorem eval_evals_exec_type_sound: |
181 theorem eval_evals_exec_type_sound: |
169 "wf_java_prog G ==> |
182 "wf_java_prog G ==> |
170 (G\<turnstile>(x,(h,l)) -e \<succ>v -> (x', (h',l')) --> |
183 (G\<turnstile>(x,(h,l)) -e \<succ>v -> (x', (h',l')) --> |
171 (\<forall>lT. (h ,l )::\<preceq>(G,lT) --> (\<forall>T . (G,lT)\<turnstile>e :: T --> |
184 (\<forall>lT. (x,(h ,l ))::\<preceq>(G,lT) --> (\<forall>T . (G,lT)\<turnstile>e :: T --> |
172 h\<le>|h' \<and> (h',l')::\<preceq>(G,lT) \<and> (x'=None --> G,h'\<turnstile>v ::\<preceq> T )))) \<and> |
185 h\<le>|h' \<and> (x',(h',l'))::\<preceq>(G,lT) \<and> (x'=None --> G,h'\<turnstile>v ::\<preceq> T )))) \<and> |
173 (G\<turnstile>(x,(h,l)) -es[\<succ>]vs-> (x', (h',l')) --> |
186 (G\<turnstile>(x,(h,l)) -es[\<succ>]vs-> (x', (h',l')) --> |
174 (\<forall>lT. (h ,l )::\<preceq>(G,lT) --> (\<forall>Ts. (G,lT)\<turnstile>es[::]Ts --> |
187 (\<forall>lT. (x,(h ,l ))::\<preceq>(G,lT) --> (\<forall>Ts. (G,lT)\<turnstile>es[::]Ts --> |
175 h\<le>|h' \<and> (h',l')::\<preceq>(G,lT) \<and> (x'=None --> list_all2 (\<lambda>v T. G,h'\<turnstile>v::\<preceq>T) vs Ts)))) \<and> |
188 h\<le>|h' \<and> (x',(h',l'))::\<preceq>(G,lT) \<and> (x'=None --> list_all2 (\<lambda>v T. G,h'\<turnstile>v::\<preceq>T) vs Ts)))) \<and> |
176 (G\<turnstile>(x,(h,l)) -c -> (x', (h',l')) --> |
189 (G\<turnstile>(x,(h,l)) -c -> (x', (h',l')) --> |
177 (\<forall>lT. (h ,l )::\<preceq>(G,lT) --> (G,lT)\<turnstile>c \<surd> --> |
190 (\<forall>lT. (x,(h ,l ))::\<preceq>(G,lT) --> (G,lT)\<turnstile>c \<surd> --> |
178 h\<le>|h' \<and> (h',l')::\<preceq>(G,lT)))" |
191 h\<le>|h' \<and> (x',(h',l'))::\<preceq>(G,lT)))" |
179 apply( rule eval_evals_exec_induct) |
192 apply( rule eval_evals_exec_induct) |
180 apply( unfold c_hupd_def) |
193 apply( unfold c_hupd_def) |
181 |
194 |
182 -- "several simplifications, XcptE, XcptEs, XcptS, Skip, Nil??" |
195 -- "several simplifications, XcptE, XcptEs, XcptS, Skip, Nil??" |
183 apply( simp_all) |
196 apply( simp_all) |
185 apply( tactic {* ALLGOALS (eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims") |
198 apply( tactic {* ALLGOALS (eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims") |
186 THEN_ALL_NEW Full_simp_tac) *}) |
199 THEN_ALL_NEW Full_simp_tac) *}) |
187 apply(tactic "ALLGOALS (EVERY' [REPEAT o (etac conjE), REPEAT o hyp_subst_tac])") |
200 apply(tactic "ALLGOALS (EVERY' [REPEAT o (etac conjE), REPEAT o hyp_subst_tac])") |
188 |
201 |
189 -- "Level 7" |
202 -- "Level 7" |
190 |
|
191 -- "15 NewC" |
203 -- "15 NewC" |
|
204 apply (drule sym) |
192 apply( drule new_AddrD) |
205 apply( drule new_AddrD) |
193 apply( erule disjE) |
206 apply( erule disjE) |
194 prefer 2 |
207 prefer 2 |
195 apply( simp (no_asm_simp)) |
208 apply( simp (no_asm_simp)) |
|
209 apply (rule conforms_xcpt_change, assumption) |
|
210 apply (simp (no_asm_simp) add: xconf_def) |
196 apply( clarsimp) |
211 apply( clarsimp) |
197 apply( rule conjI) |
212 apply( rule conjI) |
198 apply( force elim!: NewC_conforms) |
213 apply( force elim!: NewC_conforms) |
199 apply( rule conf_obj_AddrI) |
214 apply( rule conf_obj_AddrI) |
200 apply( rule_tac [2] rtrancl_refl) |
215 apply( rule_tac [2] rtrancl_refl) |
232 apply( fast intro: hext_trans) |
248 apply( fast intro: hext_trans) |
233 prefer 8 |
249 prefer 8 |
234 apply( fast intro: hext_trans) |
250 apply( fast intro: hext_trans) |
235 |
251 |
236 -- "10 Expr" |
252 -- "10 Expr" |
237 prefer 6 |
253 prefer 7 |
238 apply( fast) |
254 apply( fast) |
239 |
255 |
240 -- "9 ???" |
256 -- "9 ???" |
241 apply( simp_all) |
257 apply( simp_all) |
242 |
258 |
243 -- "8 Cast" |
259 -- "8 Cast" |
244 prefer 8 |
260 prefer 8 |
245 apply (rule impI) |
261 apply (rule conjI) |
246 apply (drule raise_if_NoneD) |
262 apply (fast intro: conforms_xcpt_change xconf_raise_if) |
247 apply (clarsimp) |
263 |
248 apply (fast elim: Cast_conf) |
264 apply clarify |
|
265 apply (drule raise_if_NoneD) |
|
266 apply (clarsimp) |
|
267 apply (rule Cast_conf) |
|
268 apply assumption+ |
249 |
269 |
250 -- "7 LAss" |
270 -- "7 LAss" |
251 apply (fold fun_upd_def) |
271 apply (fold fun_upd_def) |
252 apply( tactic {* (eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims") |
272 apply( tactic {* (eresolve_tac (thms "ty_expr_ty_exprs_wt_stmt.elims") |
253 THEN_ALL_NEW Full_simp_tac) 1 *}) |
273 THEN_ALL_NEW Full_simp_tac) 1 *}) |
|
274 apply (intro strip) |
|
275 apply (case_tac E) |
|
276 apply (simp) |
254 apply( blast intro: conforms_upd_local conf_widen) |
277 apply( blast intro: conforms_upd_local conf_widen) |
255 |
278 |
256 -- "6 FAcc" |
279 -- "6 FAcc" |
|
280 apply (rule conjI) |
|
281 apply (simp add: np_def) |
|
282 apply (fast intro: conforms_xcpt_change xconf_raise_if) |
257 apply( fast elim!: FAcc_type_sound) |
283 apply( fast elim!: FAcc_type_sound) |
258 |
284 |
259 -- "5 While" |
285 -- "5 While" |
260 prefer 5 |
286 prefer 5 |
261 apply(erule_tac V = "?a \<longrightarrow> ?b" in thin_rl) |
287 apply(erule_tac V = "?a \<longrightarrow> ?b" in thin_rl) |
262 apply(drule (1) ty_expr_ty_exprs_wt_stmt.Loop) |
288 apply(drule (1) ty_expr_ty_exprs_wt_stmt.Loop) |
263 apply(force elim: hext_trans) |
289 apply(force elim: hext_trans) |
264 |
290 |
265 apply (tactic "forward_hyp_tac") |
291 apply (tactic "forward_hyp_tac") |
266 |
292 |
267 -- "4 Cons" |
293 -- "4 Cond" |
|
294 prefer 4 |
|
295 apply (case_tac "the_Bool v") |
|
296 apply simp |
|
297 apply( fast dest: evals_no_xcpt intro: conf_hext hext_trans) |
|
298 apply simp |
|
299 apply( fast dest: evals_no_xcpt intro: conf_hext hext_trans) |
|
300 |
|
301 -- "3 ;;" |
268 prefer 3 |
302 prefer 3 |
269 apply( fast dest: evals_no_xcpt intro: conf_hext hext_trans) |
303 apply( fast dest: evals_no_xcpt intro: conf_hext hext_trans) |
270 |
304 |
271 -- "3 ;;" |
|
272 prefer 3 |
|
273 apply( fast intro: hext_trans) |
|
274 |
305 |
275 -- "2 FAss" |
306 -- "2 FAss" |
276 apply( case_tac "x2 = None") |
307 apply (subgoal_tac "(np a' x1, ab, ba) ::\<preceq> (G, lT)") |
277 prefer 2 |
308 prefer 2 |
278 apply( simp (no_asm_simp)) |
309 apply (simp add: np_def) |
279 apply( fast intro: hext_trans) |
310 apply (fast intro: conforms_xcpt_change xconf_raise_if) |
280 apply( simp) |
311 apply( case_tac "x2") |
281 apply( drule eval_no_xcpt) |
312 -- "x2 = None" |
282 apply( erule FAss_type_sound, rule HOL.refl, assumption+) |
313 apply (simp) |
|
314 apply (tactic forward_hyp_tac, clarify) |
|
315 apply( drule eval_no_xcpt) |
|
316 apply( erule FAss_type_sound, rule HOL.refl, assumption+) |
|
317 -- "x2 = Some a" |
|
318 apply ( simp (no_asm_simp)) |
|
319 apply( fast intro: hext_trans) |
|
320 |
283 |
321 |
284 apply( tactic prune_params_tac) |
322 apply( tactic prune_params_tac) |
285 -- "Level 52" |
323 -- "Level 52" |
286 |
324 |
287 -- "1 Call" |
325 -- "1 Call" |
300 apply( simp) |
338 apply( simp) |
301 apply( drule exec_xcpt) |
339 apply( drule exec_xcpt) |
302 apply( simp) |
340 apply( simp) |
303 apply( drule eval_xcpt) |
341 apply( drule eval_xcpt) |
304 apply( simp) |
342 apply( simp) |
305 apply( fast elim: hext_trans) |
343 apply (rule conjI) |
306 apply( drule (1) ty_expr_is_type) |
344 apply( fast elim: hext_trans) |
|
345 apply (rule conforms_xcpt_change, assumption) apply (simp (no_asm_simp) add: xconf_def) |
|
346 apply(clarsimp) |
|
347 |
|
348 apply( drule ty_expr_is_type, simp) |
307 apply(clarsimp) |
349 apply(clarsimp) |
308 apply(unfold is_class_def) |
350 apply(unfold is_class_def) |
309 apply(clarsimp) |
351 apply(clarsimp) |
|
352 |
310 apply(rule Call_type_sound); |
353 apply(rule Call_type_sound); |
311 prefer 11 |
354 prefer 11 |
312 apply blast |
355 apply blast |
313 apply (simp (no_asm_simp))+ |
356 apply (simp (no_asm_simp))+ |
|
357 |
314 done |
358 done |
315 ML{* |
359 ML{* |
316 Unify.search_bound := 20; |
360 Unify.search_bound := 20; |
317 Unify.trace_bound := 20 |
361 Unify.trace_bound := 20 |
318 *} |
362 *} |
319 |
363 |
320 lemma eval_type_sound: "!!E s s'. |
364 lemma eval_type_sound: "!!E s s'. |
321 [| G=prg E; wf_java_prog G; G\<turnstile>(x,s) -e\<succ>v -> (x',s'); s::\<preceq>E; E\<turnstile>e::T |] |
365 [| G=prg E; wf_java_prog G; G\<turnstile>(x,s) -e\<succ>v -> (x',s'); (x,s)::\<preceq>E; E\<turnstile>e::T |] |
322 ==> s'::\<preceq>E \<and> (x'=None --> G,heap s'\<turnstile>v::\<preceq>T)" |
366 ==> (x',s')::\<preceq>E \<and> (x'=None --> G,heap s'\<turnstile>v::\<preceq>T)" |
323 apply( simp (no_asm_simp) only: split_tupled_all) |
367 apply( simp (no_asm_simp) only: split_tupled_all) |
324 apply (drule eval_evals_exec_type_sound |
368 apply (drule eval_evals_exec_type_sound |
325 [THEN conjunct1, THEN mp, THEN spec, THEN mp]) |
369 [THEN conjunct1, THEN mp, THEN spec, THEN mp]) |
326 apply auto |
370 apply auto |
327 done |
371 done |
328 |
372 |
329 lemma exec_type_sound: "!!E s s'. |
373 lemma exec_type_sound: "!!E s s'. |
330 [| G=prg E; wf_java_prog G; G\<turnstile>(x,s) -s0-> (x',s'); s::\<preceq>E; E\<turnstile>s0\<surd> |] |
374 [| G=prg E; wf_java_prog G; G\<turnstile>(x,s) -s0-> (x',s'); (x,s)::\<preceq>E; E\<turnstile>s0\<surd> |] |
331 ==> s'::\<preceq>E" |
375 ==> (x',s')::\<preceq>E" |
332 apply( simp (no_asm_simp) only: split_tupled_all) |
376 apply( simp (no_asm_simp) only: split_tupled_all) |
333 apply (drule eval_evals_exec_type_sound |
377 apply (drule eval_evals_exec_type_sound |
334 [THEN conjunct2, THEN conjunct2, THEN mp, THEN spec, THEN mp]) |
378 [THEN conjunct2, THEN conjunct2, THEN mp, THEN spec, THEN mp]) |
335 apply auto |
379 apply auto |
336 done |
380 done |
337 |
381 |
338 theorem all_methods_understood: |
382 theorem all_methods_understood: |
339 "[|G=prg E; wf_java_prog G; G\<turnstile>(x,s) -e\<succ>a'-> Norm s'; a' \<noteq> Null; |
383 "[|G=prg E; wf_java_prog G; G\<turnstile>(x,s) -e\<succ>a'-> Norm s'; a' \<noteq> Null; |
340 s::\<preceq>E; E\<turnstile>e::Class C; method (G,C) sig \<noteq> None|] ==> |
384 (x,s)::\<preceq>E; E\<turnstile>e::Class C; method (G,C) sig \<noteq> None|] ==> |
341 method (G,fst (the (heap s' (the_Addr a')))) sig \<noteq> None" |
385 method (G,fst (the (heap s' (the_Addr a')))) sig \<noteq> None" |
342 apply( drule (4) eval_type_sound) |
386 apply( drule (4) eval_type_sound) |
343 apply(clarsimp) |
387 apply(clarsimp) |
344 apply( frule widen_methd) |
388 apply( frule widen_methd) |
345 apply( assumption) |
389 apply( assumption) |