src/HOL/Bali/Conform.thy
author hoelzl
Fri Feb 19 13:40:50 2016 +0100 (2016-02-19)
changeset 62378 85ed00c1fe7c
parent 62042 6c6ccf573479
child 63566 e5abbdee461a
permissions -rw-r--r--
generalize more theorems to support enat and ennreal
     1 (*  Title:      HOL/Bali/Conform.thy
     2     Author:     David von Oheimb
     3 *)
     4 
     5 subsection \<open>Conformance notions for the type soundness proof for Java\<close>
     6 
     7 theory Conform imports State begin
     8 
     9 text \<open>
    10 design issues:
    11 \begin{itemize}
    12 \item lconf allows for (arbitrary) inaccessible values
    13 \item ''conforms'' does not directly imply that the dynamic types of all 
    14       objects on the heap are indeed existing classes. Yet this can be 
    15       inferred for all referenced objs.
    16 \end{itemize}
    17 \<close>
    18 
    19 type_synonym env' = "prog \<times> (lname, ty) table" (* same as env of WellType.thy *)
    20 
    21 
    22 subsubsection "extension of global store"
    23 
    24 
    25 definition gext :: "st \<Rightarrow> st \<Rightarrow> bool" ("_\<le>|_"       [71,71]   70) where
    26    "s\<le>|s' \<equiv> \<forall>r. \<forall>obj\<in>globs s r: \<exists>obj'\<in>globs s' r: tag obj'= tag obj"
    27 
    28 text \<open>For the the proof of type soundness we will need the 
    29 property that during execution, objects are not lost and moreover retain the 
    30 values of their tags. So the object store grows conservatively. Note that if 
    31 we considered garbage collection, we would have to restrict this property to 
    32 accessible objects.
    33 \<close>
    34 
    35 lemma gext_objD: 
    36 "\<lbrakk>s\<le>|s'; globs s r = Some obj\<rbrakk> 
    37 \<Longrightarrow> \<exists>obj'. globs s' r = Some obj' \<and> tag obj' = tag obj"
    38 apply (simp only: gext_def)
    39 by force
    40 
    41 lemma rev_gext_objD: 
    42 "\<lbrakk>globs s r = Some obj; s\<le>|s'\<rbrakk> 
    43  \<Longrightarrow> \<exists>obj'. globs s' r = Some obj' \<and> tag obj' = tag obj"
    44 by (auto elim: gext_objD)
    45 
    46 lemma init_class_obj_inited: 
    47    "init_class_obj G C s1\<le>|s2 \<Longrightarrow> inited C (globs s2)"
    48 apply (unfold inited_def init_obj_def)
    49 apply (auto dest!: gext_objD)
    50 done
    51 
    52 lemma gext_refl [intro!, simp]: "s\<le>|s"
    53 apply (unfold gext_def)
    54 apply (fast del: fst_splitE)
    55 done
    56 
    57 lemma gext_gupd [simp, elim!]: "\<And>s. globs s r = None \<Longrightarrow> s\<le>|gupd(r\<mapsto>x)s"
    58 by (auto simp: gext_def)
    59 
    60 lemma gext_new [simp, elim!]: "\<And>s. globs s r = None \<Longrightarrow> s\<le>|init_obj G oi r s"
    61 apply (simp only: init_obj_def)
    62 apply (erule_tac gext_gupd)
    63 done
    64 
    65 lemma gext_trans [elim]: "\<And>X. \<lbrakk>s\<le>|s'; s'\<le>|s''\<rbrakk> \<Longrightarrow> s\<le>|s''" 
    66 by (force simp: gext_def)
    67 
    68 lemma gext_upd_gobj [intro!]: "s\<le>|upd_gobj r n v s"
    69 apply (simp only: gext_def)
    70 apply auto
    71 apply (case_tac "ra = r")
    72 apply auto
    73 apply (case_tac "globs s r = None")
    74 apply auto
    75 done
    76 
    77 lemma gext_cong1 [simp]: "set_locals l s1\<le>|s2 = s1\<le>|s2"
    78 by (auto simp: gext_def)
    79 
    80 lemma gext_cong2 [simp]: "s1\<le>|set_locals l s2 = s1\<le>|s2"
    81 by (auto simp: gext_def)
    82 
    83 
    84 lemma gext_lupd1 [simp]: "lupd(vn\<mapsto>v)s1\<le>|s2 = s1\<le>|s2"
    85 by (auto simp: gext_def)
    86 
    87 lemma gext_lupd2 [simp]: "s1\<le>|lupd(vn\<mapsto>v)s2 = s1\<le>|s2"
    88 by (auto simp: gext_def)
    89 
    90 
    91 lemma inited_gext: "\<lbrakk>inited C (globs s); s\<le>|s'\<rbrakk> \<Longrightarrow> inited C (globs s')"
    92 apply (unfold inited_def)
    93 apply (auto dest: gext_objD)
    94 done
    95 
    96 
    97 subsubsection "value conformance"
    98 
    99 definition conf :: "prog \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ty \<Rightarrow> bool" ("_,_\<turnstile>_\<Colon>\<preceq>_"   [71,71,71,71] 70)
   100   where "G,s\<turnstile>v\<Colon>\<preceq>T = (\<exists>T'\<in>typeof (\<lambda>a. map_option obj_ty (heap s a)) v:G\<turnstile>T'\<preceq>T)"
   101 
   102 lemma conf_cong [simp]: "G,set_locals l s\<turnstile>v\<Colon>\<preceq>T = G,s\<turnstile>v\<Colon>\<preceq>T"
   103 by (auto simp: conf_def)
   104 
   105 lemma conf_lupd [simp]: "G,lupd(vn\<mapsto>va)s\<turnstile>v\<Colon>\<preceq>T = G,s\<turnstile>v\<Colon>\<preceq>T"
   106 by (auto simp: conf_def)
   107 
   108 lemma conf_PrimT [simp]: "\<forall>dt. typeof dt v = Some (PrimT t) \<Longrightarrow> G,s\<turnstile>v\<Colon>\<preceq>PrimT t"
   109 apply (simp add: conf_def)
   110 done
   111 
   112 lemma conf_Boolean: "G,s\<turnstile>v\<Colon>\<preceq>PrimT Boolean \<Longrightarrow> \<exists> b. v=Bool b"
   113 by (cases v)
   114    (auto simp: conf_def obj_ty_def 
   115          dest: widen_Boolean2 
   116         split: obj_tag.splits)
   117 
   118 
   119 lemma conf_litval [rule_format (no_asm)]: 
   120   "typeof (\<lambda>a. None) v = Some T \<longrightarrow> G,s\<turnstile>v\<Colon>\<preceq>T"
   121 apply (unfold conf_def)
   122 apply (rule val.induct)
   123 apply auto
   124 done
   125 
   126 lemma conf_Null [simp]: "G,s\<turnstile>Null\<Colon>\<preceq>T = G\<turnstile>NT\<preceq>T"
   127 by (simp add: conf_def)
   128 
   129 lemma conf_Addr: 
   130   "G,s\<turnstile>Addr a\<Colon>\<preceq>T = (\<exists>obj. heap s a = Some obj \<and> G\<turnstile>obj_ty obj\<preceq>T)"
   131 by (auto simp: conf_def)
   132 
   133 lemma conf_AddrI:"\<lbrakk>heap s a = Some obj; G\<turnstile>obj_ty obj\<preceq>T\<rbrakk> \<Longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq>T"
   134 apply (rule conf_Addr [THEN iffD2])
   135 by fast
   136 
   137 lemma defval_conf [rule_format (no_asm), elim]: 
   138   "is_type G T \<longrightarrow> G,s\<turnstile>default_val T\<Colon>\<preceq>T"
   139 apply (unfold conf_def)
   140 apply (induct "T")
   141 apply (auto intro: prim_ty.induct)
   142 done
   143 
   144 lemma conf_widen [rule_format (no_asm), elim]: 
   145   "G\<turnstile>T\<preceq>T' \<Longrightarrow> G,s\<turnstile>x\<Colon>\<preceq>T \<longrightarrow> ws_prog G \<longrightarrow> G,s\<turnstile>x\<Colon>\<preceq>T'"
   146 apply (unfold conf_def)
   147 apply (rule val.induct)
   148 apply (auto elim: ws_widen_trans)
   149 done
   150 
   151 lemma conf_gext [rule_format (no_asm), elim]: 
   152   "G,s\<turnstile>v\<Colon>\<preceq>T \<longrightarrow> s\<le>|s' \<longrightarrow> G,s'\<turnstile>v\<Colon>\<preceq>T"
   153 apply (unfold gext_def conf_def)
   154 apply (rule val.induct)
   155 apply force+
   156 done
   157 
   158 
   159 lemma conf_list_widen [rule_format (no_asm)]: 
   160 "ws_prog G \<Longrightarrow>  
   161   \<forall>Ts Ts'. list_all2 (conf G s) vs Ts 
   162            \<longrightarrow>   G\<turnstile>Ts[\<preceq>] Ts' \<longrightarrow> list_all2 (conf G s) vs Ts'"
   163 apply (unfold widens_def)
   164 apply (rule list_all2_trans)
   165 apply auto
   166 done
   167 
   168 lemma conf_RefTD [rule_format (no_asm)]: 
   169  "G,s\<turnstile>a'\<Colon>\<preceq>RefT T 
   170   \<longrightarrow> a' = Null \<or> (\<exists>a obj T'. a' = Addr a \<and> heap s a = Some obj \<and>  
   171                     obj_ty obj = T' \<and> G\<turnstile>T'\<preceq>RefT T)"
   172 apply (unfold conf_def)
   173 apply (induct_tac "a'")
   174 apply (auto dest: widen_PrimT)
   175 done
   176 
   177 
   178 subsubsection "value list conformance"
   179 
   180 definition
   181   lconf :: "prog \<Rightarrow> st \<Rightarrow> ('a, val) table \<Rightarrow> ('a, ty) table \<Rightarrow> bool" ("_,_\<turnstile>_[\<Colon>\<preceq>]_" [71,71,71,71] 70)
   182   where "G,s\<turnstile>vs[\<Colon>\<preceq>]Ts = (\<forall>n. \<forall>T\<in>Ts n: \<exists>v\<in>vs n: G,s\<turnstile>v\<Colon>\<preceq>T)"
   183 
   184 lemma lconfD: "\<lbrakk>G,s\<turnstile>vs[\<Colon>\<preceq>]Ts; Ts n = Some T\<rbrakk> \<Longrightarrow> G,s\<turnstile>(the (vs n))\<Colon>\<preceq>T"
   185 by (force simp: lconf_def)
   186 
   187 
   188 lemma lconf_cong [simp]: "\<And>s. G,set_locals x s\<turnstile>l[\<Colon>\<preceq>]L = G,s\<turnstile>l[\<Colon>\<preceq>]L"
   189 by (auto simp: lconf_def)
   190 
   191 lemma lconf_lupd [simp]: "G,lupd(vn\<mapsto>v)s\<turnstile>l[\<Colon>\<preceq>]L = G,s\<turnstile>l[\<Colon>\<preceq>]L"
   192 by (auto simp: lconf_def)
   193 
   194 (* unused *)
   195 lemma lconf_new: "\<lbrakk>L vn = None; G,s\<turnstile>l[\<Colon>\<preceq>]L\<rbrakk> \<Longrightarrow> G,s\<turnstile>l(vn\<mapsto>v)[\<Colon>\<preceq>]L"
   196 by (auto simp: lconf_def)
   197 
   198 lemma lconf_upd: "\<lbrakk>G,s\<turnstile>l[\<Colon>\<preceq>]L; G,s\<turnstile>v\<Colon>\<preceq>T; L vn = Some T\<rbrakk> \<Longrightarrow>  
   199   G,s\<turnstile>l(vn\<mapsto>v)[\<Colon>\<preceq>]L"
   200 by (auto simp: lconf_def)
   201 
   202 lemma lconf_ext: "\<lbrakk>G,s\<turnstile>l[\<Colon>\<preceq>]L; G,s\<turnstile>v\<Colon>\<preceq>T\<rbrakk> \<Longrightarrow> G,s\<turnstile>l(vn\<mapsto>v)[\<Colon>\<preceq>]L(vn\<mapsto>T)"
   203 by (auto simp: lconf_def)
   204 
   205 lemma lconf_map_sum [simp]: 
   206  "G,s\<turnstile>l1 (+) l2[\<Colon>\<preceq>]L1 (+) L2 = (G,s\<turnstile>l1[\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>l2[\<Colon>\<preceq>]L2)"
   207 apply (unfold lconf_def)
   208 apply safe
   209 apply (case_tac [3] "n")
   210 apply (force split add: sum.split)+
   211 done
   212 
   213 lemma lconf_ext_list [rule_format (no_asm)]: "
   214  \<And>X. \<lbrakk>G,s\<turnstile>l[\<Colon>\<preceq>]L\<rbrakk> \<Longrightarrow> 
   215       \<forall>vs Ts. distinct vns \<longrightarrow> length Ts = length vns 
   216       \<longrightarrow> list_all2 (conf G s) vs Ts \<longrightarrow> G,s\<turnstile>l(vns[\<mapsto>]vs)[\<Colon>\<preceq>]L(vns[\<mapsto>]Ts)"
   217 apply (unfold lconf_def)
   218 apply (induct_tac "vns")
   219 apply  clarsimp
   220 apply clarify
   221 apply (frule list_all2_lengthD)
   222 apply (clarsimp)
   223 done
   224 
   225 
   226 lemma lconf_deallocL: "\<lbrakk>G,s\<turnstile>l[\<Colon>\<preceq>]L(vn\<mapsto>T); L vn = None\<rbrakk> \<Longrightarrow> G,s\<turnstile>l[\<Colon>\<preceq>]L"
   227 apply (simp only: lconf_def)
   228 apply safe
   229 apply (drule spec)
   230 apply (drule ospec)
   231 apply auto
   232 done 
   233 
   234 
   235 lemma lconf_gext [elim]: "\<lbrakk>G,s\<turnstile>l[\<Colon>\<preceq>]L; s\<le>|s'\<rbrakk> \<Longrightarrow> G,s'\<turnstile>l[\<Colon>\<preceq>]L"
   236 apply (simp only: lconf_def)
   237 apply fast
   238 done
   239 
   240 lemma lconf_empty [simp, intro!]: "G,s\<turnstile>vs[\<Colon>\<preceq>]empty"
   241 apply (unfold lconf_def)
   242 apply force
   243 done
   244 
   245 lemma lconf_init_vals [intro!]: 
   246         " \<forall>n. \<forall>T\<in>fs n:is_type G T \<Longrightarrow> G,s\<turnstile>init_vals fs[\<Colon>\<preceq>]fs"
   247 apply (unfold lconf_def)
   248 apply force
   249 done
   250 
   251 subsubsection "weak value list conformance"
   252 
   253 text \<open>Only if the value is defined it has to conform to its type. 
   254         This is the contribution of the definite assignment analysis to 
   255         the notion of conformance. The definite assignment analysis ensures
   256         that the program only attempts to access local variables that 
   257         actually have a defined value in the state. 
   258         So conformance must only ensure that the
   259         defined values are of the right type, and not also that the value
   260         is defined. 
   261 \<close>
   262 
   263   
   264 definition
   265   wlconf :: "prog \<Rightarrow> st \<Rightarrow> ('a, val) table \<Rightarrow> ('a, ty) table \<Rightarrow> bool" ("_,_\<turnstile>_[\<sim>\<Colon>\<preceq>]_" [71,71,71,71] 70)
   266   where "G,s\<turnstile>vs[\<sim>\<Colon>\<preceq>]Ts = (\<forall>n. \<forall>T\<in>Ts n: \<forall> v\<in>vs n: G,s\<turnstile>v\<Colon>\<preceq>T)"
   267 
   268 lemma wlconfD: "\<lbrakk>G,s\<turnstile>vs[\<sim>\<Colon>\<preceq>]Ts; Ts n = Some T; vs n = Some v\<rbrakk> \<Longrightarrow> G,s\<turnstile>v\<Colon>\<preceq>T"
   269 by (auto simp: wlconf_def)
   270 
   271 
   272 lemma wlconf_cong [simp]: "\<And>s. G,set_locals x s\<turnstile>l[\<sim>\<Colon>\<preceq>]L = G,s\<turnstile>l[\<sim>\<Colon>\<preceq>]L"
   273 by (auto simp: wlconf_def)
   274 
   275 lemma wlconf_lupd [simp]: "G,lupd(vn\<mapsto>v)s\<turnstile>l[\<sim>\<Colon>\<preceq>]L = G,s\<turnstile>l[\<sim>\<Colon>\<preceq>]L"
   276 by (auto simp: wlconf_def)
   277 
   278 
   279 lemma wlconf_upd: "\<lbrakk>G,s\<turnstile>l[\<sim>\<Colon>\<preceq>]L; G,s\<turnstile>v\<Colon>\<preceq>T; L vn = Some T\<rbrakk> \<Longrightarrow>  
   280   G,s\<turnstile>l(vn\<mapsto>v)[\<sim>\<Colon>\<preceq>]L"
   281 by (auto simp: wlconf_def)
   282 
   283 lemma wlconf_ext: "\<lbrakk>G,s\<turnstile>l[\<sim>\<Colon>\<preceq>]L; G,s\<turnstile>v\<Colon>\<preceq>T\<rbrakk> \<Longrightarrow> G,s\<turnstile>l(vn\<mapsto>v)[\<sim>\<Colon>\<preceq>]L(vn\<mapsto>T)"
   284 by (auto simp: wlconf_def)
   285 
   286 lemma wlconf_map_sum [simp]: 
   287  "G,s\<turnstile>l1 (+) l2[\<sim>\<Colon>\<preceq>]L1 (+) L2 = (G,s\<turnstile>l1[\<sim>\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>l2[\<sim>\<Colon>\<preceq>]L2)"
   288 apply (unfold wlconf_def)
   289 apply safe
   290 apply (case_tac [3] "n")
   291 apply (force split add: sum.split)+
   292 done
   293 
   294 lemma wlconf_ext_list [rule_format (no_asm)]: "
   295  \<And>X. \<lbrakk>G,s\<turnstile>l[\<sim>\<Colon>\<preceq>]L\<rbrakk> \<Longrightarrow> 
   296       \<forall>vs Ts. distinct vns \<longrightarrow> length Ts = length vns 
   297       \<longrightarrow> list_all2 (conf G s) vs Ts \<longrightarrow> G,s\<turnstile>l(vns[\<mapsto>]vs)[\<sim>\<Colon>\<preceq>]L(vns[\<mapsto>]Ts)"
   298 apply (unfold wlconf_def)
   299 apply (induct_tac "vns")
   300 apply  clarsimp
   301 apply clarify
   302 apply (frule list_all2_lengthD)
   303 apply clarsimp
   304 done
   305 
   306 
   307 lemma wlconf_deallocL: "\<lbrakk>G,s\<turnstile>l[\<sim>\<Colon>\<preceq>]L(vn\<mapsto>T); L vn = None\<rbrakk> \<Longrightarrow> G,s\<turnstile>l[\<sim>\<Colon>\<preceq>]L"
   308 apply (simp only: wlconf_def)
   309 apply safe
   310 apply (drule spec)
   311 apply (drule ospec)
   312 defer
   313 apply (drule ospec )
   314 apply auto
   315 done 
   316 
   317 
   318 lemma wlconf_gext [elim]: "\<lbrakk>G,s\<turnstile>l[\<sim>\<Colon>\<preceq>]L; s\<le>|s'\<rbrakk> \<Longrightarrow> G,s'\<turnstile>l[\<sim>\<Colon>\<preceq>]L"
   319 apply (simp only: wlconf_def)
   320 apply fast
   321 done
   322 
   323 lemma wlconf_empty [simp, intro!]: "G,s\<turnstile>vs[\<sim>\<Colon>\<preceq>]empty"
   324 apply (unfold wlconf_def)
   325 apply force
   326 done
   327 
   328 lemma wlconf_empty_vals: "G,s\<turnstile>empty[\<sim>\<Colon>\<preceq>]ts"
   329   by (simp add: wlconf_def)
   330 
   331 lemma wlconf_init_vals [intro!]: 
   332         " \<forall>n. \<forall>T\<in>fs n:is_type G T \<Longrightarrow> G,s\<turnstile>init_vals fs[\<sim>\<Colon>\<preceq>]fs"
   333 apply (unfold wlconf_def)
   334 apply force
   335 done
   336 
   337 lemma lconf_wlconf:
   338  "G,s\<turnstile>l[\<Colon>\<preceq>]L \<Longrightarrow> G,s\<turnstile>l[\<sim>\<Colon>\<preceq>]L"
   339 by (force simp add: lconf_def wlconf_def)
   340 
   341 subsubsection "object conformance"
   342 
   343 definition
   344   oconf :: "prog \<Rightarrow> st \<Rightarrow> obj \<Rightarrow> oref \<Rightarrow> bool" ("_,_\<turnstile>_\<Colon>\<preceq>\<surd>_"  [71,71,71,71] 70) where
   345   "(G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r) = (G,s\<turnstile>values obj[\<Colon>\<preceq>]var_tys G (tag obj) r \<and> 
   346                            (case r of 
   347                               Heap a \<Rightarrow> is_type G (obj_ty obj) 
   348                             | Stat C \<Rightarrow> True))"
   349 
   350 
   351 lemma oconf_is_type: "G,s\<turnstile>obj\<Colon>\<preceq>\<surd>Heap a \<Longrightarrow> is_type G (obj_ty obj)"
   352 by (auto simp: oconf_def Let_def)
   353 
   354 lemma oconf_lconf: "G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r \<Longrightarrow> G,s\<turnstile>values obj[\<Colon>\<preceq>]var_tys G (tag obj) r"
   355 by (simp add: oconf_def) 
   356 
   357 lemma oconf_cong [simp]: "G,set_locals l s\<turnstile>obj\<Colon>\<preceq>\<surd>r = G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r"
   358 by (auto simp: oconf_def Let_def)
   359 
   360 lemma oconf_init_obj_lemma: 
   361 "\<lbrakk>\<And>C c. class G C = Some c \<Longrightarrow> unique (DeclConcepts.fields G C);  
   362   \<And>C c f fld. \<lbrakk>class G C = Some c; 
   363                 table_of (DeclConcepts.fields G C) f = Some fld \<rbrakk> 
   364             \<Longrightarrow> is_type G (type fld);  
   365   (case r of 
   366      Heap a \<Rightarrow> is_type G (obj_ty obj) 
   367   | Stat C \<Rightarrow> is_class G C)
   368 \<rbrakk> \<Longrightarrow>  G,s\<turnstile>obj \<lparr>values:=init_vals (var_tys G (tag obj) r)\<rparr>\<Colon>\<preceq>\<surd>r"
   369 apply (auto simp add: oconf_def)
   370 apply (drule_tac var_tys_Some_eq [THEN iffD1]) 
   371 defer
   372 apply (subst obj_ty_cong)
   373 apply (auto dest!: fields_table_SomeD split add: sum.split_asm obj_tag.split_asm)
   374 done
   375 
   376 subsubsection "state conformance"
   377 
   378 definition
   379   conforms :: "state \<Rightarrow> env' \<Rightarrow> bool"  ("_\<Colon>\<preceq>_" [71,71] 70)  where
   380    "xs\<Colon>\<preceq>E =
   381       (let (G, L) = E; s = snd xs; l = locals s in
   382         (\<forall>r. \<forall>obj\<in>globs s r: G,s\<turnstile>obj \<Colon>\<preceq>\<surd>r) \<and> G,s\<turnstile>l [\<sim>\<Colon>\<preceq>]L \<and>
   383         (\<forall>a. fst xs=Some(Xcpt (Loc a)) \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable)) \<and>
   384              (fst xs=Some(Jump Ret) \<longrightarrow> l Result \<noteq> None))"
   385 
   386 subsubsection "conforms"
   387 
   388 lemma conforms_globsD: 
   389 "\<lbrakk>(x, s)\<Colon>\<preceq>(G, L); globs s r = Some obj\<rbrakk> \<Longrightarrow> G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r"
   390 by (auto simp: conforms_def Let_def)
   391 
   392 lemma conforms_localD: "(x, s)\<Colon>\<preceq>(G, L) \<Longrightarrow> G,s\<turnstile>locals s[\<sim>\<Colon>\<preceq>]L"
   393 by (auto simp: conforms_def Let_def)
   394 
   395 lemma conforms_XcptLocD: "\<lbrakk>(x, s)\<Colon>\<preceq>(G, L); x = Some (Xcpt (Loc a))\<rbrakk> \<Longrightarrow>  
   396           G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable)"
   397 by (auto simp: conforms_def Let_def)
   398 
   399 lemma conforms_RetD: "\<lbrakk>(x, s)\<Colon>\<preceq>(G, L); x = Some (Jump Ret)\<rbrakk> \<Longrightarrow>  
   400           (locals s) Result \<noteq> None"
   401 by (auto simp: conforms_def Let_def)
   402 
   403 lemma conforms_RefTD: 
   404  "\<lbrakk>G,s\<turnstile>a'\<Colon>\<preceq>RefT t; a' \<noteq> Null; (x,s) \<Colon>\<preceq>(G, L)\<rbrakk> \<Longrightarrow>  
   405    \<exists>a obj. a' = Addr a \<and> globs s (Inl a) = Some obj \<and>  
   406    G\<turnstile>obj_ty obj\<preceq>RefT t \<and> is_type G (obj_ty obj)"
   407 apply (drule_tac conf_RefTD)
   408 apply clarsimp
   409 apply (rule conforms_globsD [THEN oconf_is_type])
   410 apply auto
   411 done
   412 
   413 lemma conforms_Jump [iff]:
   414   "j=Ret \<longrightarrow> locals s Result \<noteq> None 
   415    \<Longrightarrow> ((Some (Jump j), s)\<Colon>\<preceq>(G, L)) = (Norm s\<Colon>\<preceq>(G, L))"
   416 by (auto simp: conforms_def Let_def)
   417 
   418 lemma conforms_StdXcpt [iff]: 
   419   "((Some (Xcpt (Std xn)), s)\<Colon>\<preceq>(G, L)) = (Norm s\<Colon>\<preceq>(G, L))"
   420 by (auto simp: conforms_def)
   421 
   422 lemma conforms_Err [iff]:
   423    "((Some (Error e), s)\<Colon>\<preceq>(G, L)) = (Norm s\<Colon>\<preceq>(G, L))"
   424   by (auto simp: conforms_def)  
   425 
   426 lemma conforms_raise_if [iff]: 
   427   "((raise_if c xn x, s)\<Colon>\<preceq>(G, L)) = ((x, s)\<Colon>\<preceq>(G, L))"
   428 by (auto simp: abrupt_if_def)
   429 
   430 lemma conforms_error_if [iff]: 
   431   "((error_if c err x, s)\<Colon>\<preceq>(G, L)) = ((x, s)\<Colon>\<preceq>(G, L))"
   432 by (auto simp: abrupt_if_def)
   433 
   434 lemma conforms_NormI: "(x, s)\<Colon>\<preceq>(G, L) \<Longrightarrow> Norm s\<Colon>\<preceq>(G, L)"
   435 by (auto simp: conforms_def Let_def)
   436 
   437 lemma conforms_absorb [rule_format]:
   438   "(a, b)\<Colon>\<preceq>(G, L) \<longrightarrow> (absorb j a, b)\<Colon>\<preceq>(G, L)"
   439 apply (rule impI)
   440 apply (case_tac a)
   441 apply (case_tac "absorb j a")
   442 apply auto
   443 apply (rename_tac a')
   444 apply (case_tac "absorb j (Some a')",auto)
   445 apply (erule conforms_NormI)
   446 done
   447 
   448 lemma conformsI: "\<lbrakk>\<forall>r. \<forall>obj\<in>globs s r: G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r;  
   449      G,s\<turnstile>locals s[\<sim>\<Colon>\<preceq>]L;  
   450      \<forall>a. x = Some (Xcpt (Loc a)) \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable);
   451      x = Some (Jump Ret)\<longrightarrow> locals s Result \<noteq> None\<rbrakk> \<Longrightarrow> 
   452   (x, s)\<Colon>\<preceq>(G, L)"
   453 by (auto simp: conforms_def Let_def)
   454 
   455 lemma conforms_xconf: "\<lbrakk>(x, s)\<Colon>\<preceq>(G,L);   
   456  \<forall>a. x' = Some (Xcpt (Loc a)) \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable);
   457      x' = Some (Jump Ret) \<longrightarrow> locals s Result \<noteq> None\<rbrakk> \<Longrightarrow> 
   458  (x',s)\<Colon>\<preceq>(G,L)"
   459 by (fast intro: conformsI elim: conforms_globsD conforms_localD)
   460 
   461 lemma conforms_lupd: 
   462  "\<lbrakk>(x, s)\<Colon>\<preceq>(G, L); L vn = Some T; G,s\<turnstile>v\<Colon>\<preceq>T\<rbrakk> \<Longrightarrow> (x, lupd(vn\<mapsto>v)s)\<Colon>\<preceq>(G, L)"
   463 by (force intro: conformsI wlconf_upd dest: conforms_globsD conforms_localD 
   464                                            conforms_XcptLocD conforms_RetD 
   465           simp: oconf_def)
   466 
   467 
   468 lemmas conforms_allocL_aux = conforms_localD [THEN wlconf_ext]
   469 
   470 lemma conforms_allocL: 
   471   "\<lbrakk>(x, s)\<Colon>\<preceq>(G, L); G,s\<turnstile>v\<Colon>\<preceq>T\<rbrakk> \<Longrightarrow> (x, lupd(vn\<mapsto>v)s)\<Colon>\<preceq>(G, L(vn\<mapsto>T))"
   472 by (force intro: conformsI dest: conforms_globsD conforms_RetD 
   473           elim: conforms_XcptLocD  conforms_allocL_aux 
   474           simp: oconf_def)
   475 
   476 lemmas conforms_deallocL_aux = conforms_localD [THEN wlconf_deallocL]
   477 
   478 lemma conforms_deallocL: "\<And>s.\<lbrakk>s\<Colon>\<preceq>(G, L(vn\<mapsto>T)); L vn = None\<rbrakk> \<Longrightarrow> s\<Colon>\<preceq>(G,L)"
   479 by (fast intro: conformsI dest: conforms_globsD conforms_RetD
   480          elim: conforms_XcptLocD conforms_deallocL_aux)
   481 
   482 lemma conforms_gext: "\<lbrakk>(x, s)\<Colon>\<preceq>(G,L); s\<le>|s';  
   483   \<forall>r. \<forall>obj\<in>globs s' r: G,s'\<turnstile>obj\<Colon>\<preceq>\<surd>r;  
   484    locals s'=locals s\<rbrakk> \<Longrightarrow> (x,s')\<Colon>\<preceq>(G,L)"
   485 apply (rule conformsI)
   486 apply     assumption
   487 apply    (drule conforms_localD) apply force
   488 apply   (intro strip)
   489 apply  (drule (1) conforms_XcptLocD) apply force 
   490 apply (intro strip)
   491 apply (drule (1) conforms_RetD) apply force
   492 done
   493 
   494 
   495 
   496 lemma conforms_xgext: 
   497   "\<lbrakk>(x ,s)\<Colon>\<preceq>(G,L); (x', s')\<Colon>\<preceq>(G, L); s'\<le>|s;dom (locals s') \<subseteq> dom (locals s)\<rbrakk> 
   498    \<Longrightarrow> (x',s)\<Colon>\<preceq>(G,L)"
   499 apply (erule_tac conforms_xconf)
   500 apply  (fast dest: conforms_XcptLocD)
   501 apply (intro strip)
   502 apply (drule (1) conforms_RetD) 
   503 apply (auto dest: domI)
   504 done
   505 
   506 lemma conforms_gupd: "\<And>obj. \<lbrakk>(x, s)\<Colon>\<preceq>(G, L); G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r; s\<le>|gupd(r\<mapsto>obj)s\<rbrakk> 
   507 \<Longrightarrow>  (x, gupd(r\<mapsto>obj)s)\<Colon>\<preceq>(G, L)"
   508 apply (rule conforms_gext)
   509 apply    auto
   510 apply (force dest: conforms_globsD simp add: oconf_def)+
   511 done
   512 
   513 lemma conforms_upd_gobj: "\<lbrakk>(x,s)\<Colon>\<preceq>(G, L); globs s r = Some obj; 
   514   var_tys G (tag obj) r n = Some T; G,s\<turnstile>v\<Colon>\<preceq>T\<rbrakk> \<Longrightarrow> (x,upd_gobj r n v s)\<Colon>\<preceq>(G,L)"
   515 apply (rule conforms_gext)
   516 apply auto
   517 apply (drule (1) conforms_globsD)
   518 apply (simp add: oconf_def)
   519 apply safe
   520 apply (rule lconf_upd)
   521 apply auto
   522 apply (simp only: obj_ty_cong) 
   523 apply (force dest: conforms_globsD intro!: lconf_upd 
   524        simp add: oconf_def cong del: sum.case_cong_weak)
   525 done
   526 
   527 lemma conforms_set_locals: 
   528   "\<lbrakk>(x,s)\<Colon>\<preceq>(G, L'); G,s\<turnstile>l[\<sim>\<Colon>\<preceq>]L; x=Some (Jump Ret) \<longrightarrow> l Result \<noteq> None\<rbrakk> 
   529    \<Longrightarrow> (x,set_locals l s)\<Colon>\<preceq>(G,L)"
   530 apply (rule conformsI)
   531 apply     (intro strip)
   532 apply     simp
   533 apply     (drule (2) conforms_globsD)
   534 apply    simp
   535 apply   (intro strip)
   536 apply   (drule (1) conforms_XcptLocD)
   537 apply   simp
   538 apply (intro strip)
   539 apply (drule (1) conforms_RetD)
   540 apply simp
   541 done
   542 
   543 lemma conforms_locals: 
   544   "\<lbrakk>(a,b)\<Colon>\<preceq>(G, L); L x = Some T;locals b x \<noteq>None\<rbrakk>
   545    \<Longrightarrow> G,b\<turnstile>the (locals b x)\<Colon>\<preceq>T"
   546 apply (force simp: conforms_def Let_def wlconf_def)
   547 done
   548 
   549 lemma conforms_return: 
   550 "\<And>s'. \<lbrakk>(x,s)\<Colon>\<preceq>(G, L); (x',s')\<Colon>\<preceq>(G, L'); s\<le>|s';x'\<noteq>Some (Jump Ret)\<rbrakk> \<Longrightarrow>  
   551   (x',set_locals (locals s) s')\<Colon>\<preceq>(G, L)"
   552 apply (rule conforms_xconf)
   553 prefer 2 apply (force dest: conforms_XcptLocD)
   554 apply (erule conforms_gext)
   555 apply (force dest: conforms_globsD)+
   556 done
   557 
   558 end