63 correct_state ("_,_ \<turnstile>JVM _ \<surd>" [51,51] 50) |
63 correct_state ("_,_ \<turnstile>JVM _ \<surd>" [51,51] 50) |
64 |
64 |
65 |
65 |
66 lemma sup_ty_opt_OK: |
66 lemma sup_ty_opt_OK: |
67 "(G \<turnstile> X <=o (OK T')) = (\<exists>T. X = OK T \<and> G \<turnstile> T \<preceq> T')" |
67 "(G \<turnstile> X <=o (OK T')) = (\<exists>T. X = OK T \<and> G \<turnstile> T \<preceq> T')" |
68 apply (cases X) |
68 by (cases X) auto |
69 apply auto |
|
70 done |
|
71 |
69 |
72 |
70 |
73 section {* approx-val *} |
71 section {* approx-val *} |
74 |
72 |
75 lemma approx_val_Err [simp,intro!]: |
73 lemma approx_val_Err [simp,intro!]: |
89 by (cases T) (blast intro: conf_hext)+ |
87 by (cases T) (blast intro: conf_hext)+ |
90 |
88 |
91 lemma approx_val_heap_update: |
89 lemma approx_val_heap_update: |
92 "\<lbrakk> hp a = Some obj'; G,hp\<turnstile> v::\<preceq>T; obj_ty obj = obj_ty obj'\<rbrakk> |
90 "\<lbrakk> hp a = Some obj'; G,hp\<turnstile> v::\<preceq>T; obj_ty obj = obj_ty obj'\<rbrakk> |
93 \<Longrightarrow> G,hp(a\<mapsto>obj)\<turnstile> v::\<preceq>T" |
91 \<Longrightarrow> G,hp(a\<mapsto>obj)\<turnstile> v::\<preceq>T" |
94 by (cases v, auto simp add: obj_ty_def conf_def) |
92 by (cases v) (auto simp add: obj_ty_def conf_def) |
95 |
93 |
96 lemma approx_val_widen: |
94 lemma approx_val_widen: |
97 "\<lbrakk> approx_val G hp v T; G \<turnstile> T <=o T'; wf_prog wt G \<rbrakk> |
95 "\<lbrakk> approx_val G hp v T; G \<turnstile> T <=o T'; wf_prog wt G \<rbrakk> |
98 \<Longrightarrow> approx_val G hp v T'" |
96 \<Longrightarrow> approx_val G hp v T'" |
99 by (cases T', auto simp add: sup_ty_opt_OK intro: conf_widen) |
97 by (cases T') (auto simp add: sup_ty_opt_OK intro: conf_widen) |
100 |
98 |
101 section {* approx-loc *} |
99 section {* approx-loc *} |
102 |
100 |
103 lemma approx_loc_Nil [simp,intro!]: |
101 lemma approx_loc_Nil [simp,intro!]: |
104 "approx_loc G hp [] []" |
102 "approx_loc G hp [] []" |