15 by( rewtac oconf_def); |
15 by( rewtac oconf_def); |
16 by( auto_tac (claset() addSDs [is_type_fields, map_of_SomeD], simpset())); |
16 by( auto_tac (claset() addSDs [is_type_fields, map_of_SomeD], simpset())); |
17 qed "NewC_conforms"; |
17 qed "NewC_conforms"; |
18 |
18 |
19 Goalw [cast_ok_def] |
19 Goalw [cast_ok_def] |
20 "\\<lbrakk> wf_prog wf_mb G; G,h\\<turnstile>v\\<Colon>\\<preceq>Tb; G\\<turnstile>Tb\\<preceq>? RefT T'; cast_ok G T' h v\\<rbrakk> \ |
20 "\\<lbrakk> wf_prog wf_mb G; G,h\\<turnstile>v\\<Colon>\\<preceq>Class C; G\\<turnstile>C\\<preceq>? D; cast_ok G D h v\\<rbrakk> \ |
21 \ \\<Longrightarrow> G,h\\<turnstile>v\\<Colon>\\<preceq>RefT T'"; |
21 \ \\<Longrightarrow> G,h\\<turnstile>v\\<Colon>\\<preceq>Class D"; |
22 by( case_tac1 "v = Null" 1); |
22 by( case_tac1 "v = Null" 1); |
23 by( Asm_full_simp_tac 1); |
23 by( Asm_full_simp_tac 1); |
24 by( dtac widen_RefT 1); |
24 by( dtac widen_RefT 1); |
25 by( Clarify_tac 1); |
25 by( Clarify_tac 1); |
26 by( forward_tac [cast_RefT] 1); |
|
27 by( Clarify_tac 1); |
|
28 by( rtac widen.null 1); |
26 by( rtac widen.null 1); |
29 by( Asm_full_simp_tac 1); |
27 by( datac non_npD 1 1); |
30 by( forward_tac [cast_RefT2] 1); |
28 by( auto_tac (claset() addSIs [conf_AddrI], simpset() addsimps [obj_ty_def])); |
31 by( strip_tac1 1); |
|
32 by( dtac non_npD 1); |
|
33 by( atac 1); |
|
34 by( rewrite_goals_tac [obj_ty_def]); |
|
35 by Auto_tac ; |
|
36 by( ALLGOALS (rtac conf_AddrI)); |
|
37 by Auto_tac; |
|
38 qed "Cast_conf"; |
29 qed "Cast_conf"; |
39 |
30 |
40 Goal "\\<lbrakk> wf_prog wf_mb G; field (G,C) fn = Some (fd, ft); (h,l)\\<Colon>\\<preceq>(G,lT); \ |
31 Goal "\\<lbrakk> wf_prog wf_mb G; field (G,C) fn = Some (fd, ft); (h,l)\\<Colon>\\<preceq>(G,lT); \ |
41 \ x' = None \\<longrightarrow> G,h\\<turnstile>a'\\<Colon>\\<preceq> Class C; np a' x' = None \\<rbrakk> \\<Longrightarrow> \ |
32 \ x' = None \\<longrightarrow> G,h\\<turnstile>a'\\<Colon>\\<preceq> Class C; np a' x' = None \\<rbrakk> \\<Longrightarrow> \ |
42 \ G,h\\<turnstile>the (snd (the (h (the_Addr a'))) (fn, fd))\\<Colon>\\<preceq>ft"; |
33 \ G,h\\<turnstile>the (snd (the (h (the_Addr a'))) (fn, fd))\\<Colon>\\<preceq>ft"; |
301 by( dtac exec_xcpt 1); |
292 by( dtac exec_xcpt 1); |
302 by( Asm_full_simp_tac 1); |
293 by( Asm_full_simp_tac 1); |
303 by( dtac eval_xcpt 1); |
294 by( dtac eval_xcpt 1); |
304 by( Asm_full_simp_tac 1); |
295 by( Asm_full_simp_tac 1); |
305 by( fast_tac (HOL_cs addEs [hext_trans]) 1); |
296 by( fast_tac (HOL_cs addEs [hext_trans]) 1); |
306 by( (rtac (rewrite_rule[wf_java_prog_def]Call_type_sound) THEN_ALL_NEW Asm_simp_tac) 1); |
297 by( (rtac (rewrite_rule[wf_java_prog_def]Call_type_sound) |
|
298 THEN_ALL_NEW Asm_simp_tac) 1); |
307 qed "eval_evals_exec_type_sound"; |
299 qed "eval_evals_exec_type_sound"; |
308 |
300 |
309 Goal "\\<And>E s s'. \ |
301 Goal "\\<And>E s s'. \ |
310 \ \\<lbrakk> G=prg E; wf_java_prog G; G\\<turnstile>(x,s) -e\\<succ>v \\<rightarrow> (x',s'); s\\<Colon>\\<preceq>E; E\\<turnstile>e\\<Colon>T \\<rbrakk> \ |
302 \ \\<lbrakk> G=prg E; wf_java_prog G; G\\<turnstile>(x,s) -e\\<succ>v \\<rightarrow> (x',s'); s\\<Colon>\\<preceq>E; E\\<turnstile>e\\<Colon>T \\<rbrakk> \ |
311 \ \\<Longrightarrow> s'\\<Colon>\\<preceq>E \\<and> (x'=None \\<longrightarrow> G,heap s'\\<turnstile>v\\<Colon>\\<preceq>T)"; |
303 \ \\<Longrightarrow> s'\\<Colon>\\<preceq>E \\<and> (x'=None \\<longrightarrow> G,heap s'\\<turnstile>v\\<Colon>\\<preceq>T)"; |