src/HOL/Bali/Conform.thy
author schirmer
Mon Jan 28 17:00:19 2002 +0100 (2002-01-28)
changeset 12854 00d4a435777f
child 12857 a4386cc9b1c3
permissions -rw-r--r--
Isabelle/Bali sources;
     1 (*  Title:      isabelle/Bali/Conform.thy
     2     ID:         $Id$
     3     Author:     David von Oheimb
     4     Copyright   1997 Technische Universitaet Muenchen
     5 *)
     6 
     7 header {* Conformance notions for the type soundness proof for Java *}
     8 
     9 theory Conform = State:
    10 
    11 text {*
    12 design issues:
    13 \begin{itemize}
    14 \item lconf allows for (arbitrary) inaccessible values
    15 \item ''conforms'' does not directly imply that the dynamic types of all 
    16       objects on the heap are indeed existing classes. Yet this can be 
    17       inferred for all referenced objs.
    18 \end{itemize}
    19 *}
    20 
    21 types	env_ = "prog \<times> (lname, ty) table" (* same as env of WellType.thy *)
    22 
    23 
    24 section "extension of global store"
    25 
    26 constdefs
    27 
    28   gext    :: "st \<Rightarrow> st \<Rightarrow> bool"                ("_\<le>|_"       [71,71]   70)
    29    "s\<le>|s' \<equiv> \<forall>r. \<forall>obj\<in>globs s r: \<exists>obj'\<in>globs s' r: tag obj'= tag obj"
    30 
    31 lemma gext_objD: 
    32 "\<lbrakk>s\<le>|s'; globs s r = Some obj\<rbrakk> 
    33 \<Longrightarrow> \<exists>obj'. globs s' r = Some obj' \<and> tag obj' = tag obj"
    34 apply (simp only: gext_def)
    35 by force
    36 
    37 lemma rev_gext_objD: 
    38 "\<lbrakk>globs s r = Some obj; s\<le>|s'\<rbrakk> 
    39  \<Longrightarrow> \<exists>obj'. globs s' r = Some obj' \<and> tag obj' = tag obj"
    40 by (auto elim: gext_objD)
    41 
    42 lemma init_class_obj_inited: 
    43    "init_class_obj G C s1\<le>|s2 \<Longrightarrow> inited C (globs s2)"
    44 apply (unfold inited_def init_obj_def)
    45 apply (auto dest!: gext_objD)
    46 done
    47 
    48 lemma gext_refl [intro!, simp]: "s\<le>|s"
    49 apply (unfold gext_def)
    50 apply (fast del: fst_splitE)
    51 done
    52 
    53 lemma gext_gupd [simp, elim!]: "\<And>s. globs s r = None \<Longrightarrow> s\<le>|gupd(r\<mapsto>x)s"
    54 by (auto simp: gext_def)
    55 
    56 lemma gext_new [simp, elim!]: "\<And>s. globs s r = None \<Longrightarrow> s\<le>|init_obj G oi r s"
    57 apply (simp only: init_obj_def)
    58 apply (erule_tac gext_gupd)
    59 done
    60 
    61 lemma gext_trans [elim]: "\<And>X. \<lbrakk>s\<le>|s'; s'\<le>|s''\<rbrakk> \<Longrightarrow> s\<le>|s''" 
    62 by (force simp: gext_def)
    63 
    64 lemma gext_upd_gobj [intro!]: "s\<le>|upd_gobj r n v s"
    65 apply (simp only: gext_def)
    66 apply auto
    67 apply (case_tac "ra = r")
    68 apply auto
    69 apply (case_tac "globs s r = None")
    70 apply auto
    71 done
    72 
    73 lemma gext_cong1 [simp]: "set_locals l s1\<le>|s2 = s1\<le>|s2"
    74 by (auto simp: gext_def)
    75 
    76 lemma gext_cong2 [simp]: "s1\<le>|set_locals l s2 = s1\<le>|s2"
    77 by (auto simp: gext_def)
    78 
    79 
    80 lemma gext_lupd1 [simp]: "lupd(vn\<mapsto>v)s1\<le>|s2 = s1\<le>|s2"
    81 by (auto simp: gext_def)
    82 
    83 lemma gext_lupd2 [simp]: "s1\<le>|lupd(vn\<mapsto>v)s2 = s1\<le>|s2"
    84 by (auto simp: gext_def)
    85 
    86 
    87 lemma inited_gext: "\<lbrakk>inited C (globs s); s\<le>|s'\<rbrakk> \<Longrightarrow> inited C (globs s')"
    88 apply (unfold inited_def)
    89 apply (auto dest: gext_objD)
    90 done
    91 
    92 
    93 section "value conformance"
    94 
    95 constdefs
    96 
    97   conf  :: "prog \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ty \<Rightarrow> bool"    ("_,_\<turnstile>_\<Colon>\<preceq>_"   [71,71,71,71] 70)
    98 	   "G,s\<turnstile>v\<Colon>\<preceq>T \<equiv> \<exists>T'\<in>typeof (\<lambda>a. option_map obj_ty (heap s a)) v:G\<turnstile>T'\<preceq>T"
    99 
   100 lemma conf_cong [simp]: "G,set_locals l s\<turnstile>v\<Colon>\<preceq>T = G,s\<turnstile>v\<Colon>\<preceq>T"
   101 by (auto simp: conf_def)
   102 
   103 lemma conf_lupd [simp]: "G,lupd(vn\<mapsto>va)s\<turnstile>v\<Colon>\<preceq>T = G,s\<turnstile>v\<Colon>\<preceq>T"
   104 by (auto simp: conf_def)
   105 
   106 lemma conf_PrimT [simp]: "\<forall>dt. typeof dt v = Some (PrimT t) \<Longrightarrow> G,s\<turnstile>v\<Colon>\<preceq>PrimT t"
   107 apply (simp add: conf_def)
   108 done
   109 
   110 lemma conf_litval [rule_format (no_asm)]: 
   111   "typeof (\<lambda>a. None) v = Some T \<longrightarrow> G,s\<turnstile>v\<Colon>\<preceq>T"
   112 apply (unfold conf_def)
   113 apply (rule val.induct)
   114 apply auto
   115 done
   116 
   117 lemma conf_Null [simp]: "G,s\<turnstile>Null\<Colon>\<preceq>T = G\<turnstile>NT\<preceq>T"
   118 by (simp add: conf_def)
   119 
   120 lemma conf_Addr: 
   121   "G,s\<turnstile>Addr a\<Colon>\<preceq>T = (\<exists>obj. heap s a = Some obj \<and> G\<turnstile>obj_ty obj\<preceq>T)"
   122 by (auto simp: conf_def)
   123 
   124 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"
   125 apply (rule conf_Addr [THEN iffD2])
   126 by fast
   127 
   128 lemma defval_conf [rule_format (no_asm), elim]: 
   129   "is_type G T \<longrightarrow> G,s\<turnstile>default_val T\<Colon>\<preceq>T"
   130 apply (unfold conf_def)
   131 apply (induct "T")
   132 apply (auto intro: prim_ty.induct)
   133 done
   134 
   135 lemma conf_widen [rule_format (no_asm), elim]: 
   136   "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'"
   137 apply (unfold conf_def)
   138 apply (rule val.induct)
   139 apply (auto elim: ws_widen_trans)
   140 done
   141 
   142 lemma conf_gext [rule_format (no_asm), elim]: 
   143   "G,s\<turnstile>v\<Colon>\<preceq>T \<longrightarrow> s\<le>|s' \<longrightarrow> G,s'\<turnstile>v\<Colon>\<preceq>T"
   144 apply (unfold gext_def conf_def)
   145 apply (rule val.induct)
   146 apply force+
   147 done
   148 
   149 
   150 lemma conf_list_widen [rule_format (no_asm)]: 
   151 "ws_prog G \<Longrightarrow>  
   152   \<forall>Ts Ts'. list_all2 (conf G s) vs Ts 
   153            \<longrightarrow>   G\<turnstile>Ts[\<preceq>] Ts' \<longrightarrow> list_all2 (conf G s) vs Ts'"
   154 apply (unfold widens_def)
   155 apply (rule list_all2_trans)
   156 apply auto
   157 done
   158 
   159 lemma conf_RefTD [rule_format (no_asm)]: 
   160  "G,s\<turnstile>a'\<Colon>\<preceq>RefT T 
   161   \<longrightarrow> a' = Null \<or> (\<exists>a obj T'. a' = Addr a \<and> heap s a = Some obj \<and>  
   162                     obj_ty obj = T' \<and> G\<turnstile>T'\<preceq>RefT T)"
   163 apply (unfold conf_def)
   164 apply (induct_tac "a'")
   165 apply (auto dest: widen_PrimT)
   166 done
   167 
   168 
   169 section "value list conformance"
   170 
   171 constdefs
   172 
   173   lconf :: "prog \<Rightarrow> st \<Rightarrow> ('a, val) table \<Rightarrow> ('a, ty) table \<Rightarrow> bool"
   174                                                 ("_,_\<turnstile>_[\<Colon>\<preceq>]_" [71,71,71,71] 70)
   175            "G,s\<turnstile>vs[\<Colon>\<preceq>]Ts \<equiv> \<forall>n. \<forall>T\<in>Ts n: \<exists>v\<in>vs n: G,s\<turnstile>v\<Colon>\<preceq>T"
   176 
   177 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"
   178 by (force simp: lconf_def)
   179 
   180 
   181 lemma lconf_cong [simp]: "\<And>s. G,set_locals x s\<turnstile>l[\<Colon>\<preceq>]L = G,s\<turnstile>l[\<Colon>\<preceq>]L"
   182 by (auto simp: lconf_def)
   183 
   184 lemma lconf_lupd [simp]: "G,lupd(vn\<mapsto>v)s\<turnstile>l[\<Colon>\<preceq>]L = G,s\<turnstile>l[\<Colon>\<preceq>]L"
   185 by (auto simp: lconf_def)
   186 
   187 (* unused *)
   188 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"
   189 by (auto simp: lconf_def)
   190 
   191 lemma lconf_upd: "\<lbrakk>G,s\<turnstile>l[\<Colon>\<preceq>]L; G,s\<turnstile>v\<Colon>\<preceq>T; L vn = Some T\<rbrakk> \<Longrightarrow>  
   192   G,s\<turnstile>l(vn\<mapsto>v)[\<Colon>\<preceq>]L"
   193 by (auto simp: lconf_def)
   194 
   195 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)"
   196 by (auto simp: lconf_def)
   197 
   198 lemma lconf_map_sum [simp]: 
   199  "G,s\<turnstile>l1 (+) l2[\<Colon>\<preceq>]L1 (+) L2 = (G,s\<turnstile>l1[\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>l2[\<Colon>\<preceq>]L2)"
   200 apply (unfold lconf_def)
   201 apply safe
   202 apply (case_tac [3] "n")
   203 apply (force split add: sum.split)+
   204 done
   205 
   206 lemma lconf_ext_list [rule_format (no_asm)]: "
   207  \<And>X. \<lbrakk>G,s\<turnstile>l[\<Colon>\<preceq>]L\<rbrakk> \<Longrightarrow> 
   208       \<forall>vs Ts. nodups vns \<longrightarrow> length Ts = length vns 
   209       \<longrightarrow> list_all2 (conf G s) vs Ts \<longrightarrow> G,s\<turnstile>l(vns[\<mapsto>]vs)[\<Colon>\<preceq>]L(vns[\<mapsto>]Ts)"
   210 apply (unfold lconf_def)
   211 apply (induct_tac "vns")
   212 apply  clarsimp
   213 apply clarsimp
   214 apply (frule list_all2_lengthD)
   215 apply clarsimp
   216 done
   217 
   218 
   219 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"
   220 apply (simp only: lconf_def)
   221 apply safe
   222 apply (drule spec)
   223 apply (drule ospec)
   224 apply auto
   225 done 
   226 
   227 
   228 lemma lconf_gext [elim]: "\<lbrakk>G,s\<turnstile>l[\<Colon>\<preceq>]L; s\<le>|s'\<rbrakk> \<Longrightarrow> G,s'\<turnstile>l[\<Colon>\<preceq>]L"
   229 apply (simp only: lconf_def)
   230 apply fast
   231 done
   232 
   233 lemma lconf_empty [simp, intro!]: "G,s\<turnstile>vs[\<Colon>\<preceq>]empty"
   234 apply (unfold lconf_def)
   235 apply force
   236 done
   237 
   238 lemma lconf_init_vals [intro!]: 
   239 	" \<forall>n. \<forall>T\<in>fs n:is_type G T \<Longrightarrow> G,s\<turnstile>init_vals fs[\<Colon>\<preceq>]fs"
   240 apply (unfold lconf_def)
   241 apply force
   242 done
   243 
   244 
   245 section "object conformance"
   246 
   247 constdefs
   248 
   249   oconf :: "prog \<Rightarrow> st \<Rightarrow> obj \<Rightarrow> oref \<Rightarrow> bool"  ("_,_\<turnstile>_\<Colon>\<preceq>\<surd>_"  [71,71,71,71] 70)
   250 	   "G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r \<equiv> G,s\<turnstile>values obj[\<Colon>\<preceq>]var_tys G (tag obj) r \<and> 
   251                            (case r of 
   252 		              Heap a \<Rightarrow> is_type G (obj_ty obj) 
   253                             | Stat C \<Rightarrow> True)"
   254 (*
   255 lemma oconf_def2:  "G,s\<turnstile>\<lparr>tag=oi,values=fs\<rparr>\<Colon>\<preceq>\<surd>r =  
   256   (G,s\<turnstile>fs[\<Colon>\<preceq>]var_tys G oi r \<and> 
   257   (case r of Heap a \<Rightarrow> is_type G (obj_ty \<lparr>tag=oi,values=fs\<rparr>) | Stat C \<Rightarrow> True))"
   258 by (simp add: oconf_def Let_def)
   259 *)
   260 (*
   261 lemma oconf_def2:  "G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r =  
   262   (G,s\<turnstile>values obj[\<Colon>\<preceq>]var_tys G (tag obj) r \<and> 
   263   (case r of Heap a \<Rightarrow> is_type G (obj_ty obj) | Stat C \<Rightarrow> True))"
   264 by (simp add: oconf_def Let_def)
   265 *)
   266 lemma oconf_is_type: "G,s\<turnstile>obj\<Colon>\<preceq>\<surd>Heap a \<Longrightarrow> is_type G (obj_ty obj)"
   267 by (auto simp: oconf_def Let_def)
   268 
   269 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"
   270 by (simp add: oconf_def) 
   271 
   272 lemma oconf_cong [simp]: "G,set_locals l s\<turnstile>obj\<Colon>\<preceq>\<surd>r = G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r"
   273 by (auto simp: oconf_def Let_def)
   274 
   275 lemma oconf_init_obj_lemma: 
   276 "\<lbrakk>\<And>C c. class G C = Some c \<Longrightarrow> unique (DeclConcepts.fields G C);  
   277   \<And>C c f fld. \<lbrakk>class G C = Some c; 
   278                 table_of (DeclConcepts.fields G C) f = Some fld \<rbrakk> 
   279             \<Longrightarrow> is_type G (type fld);  
   280   (case r of 
   281      Heap a \<Rightarrow> is_type G (obj_ty obj) 
   282   | Stat C \<Rightarrow> is_class G C)
   283 \<rbrakk> \<Longrightarrow>  G,s\<turnstile>obj \<lparr>values:=init_vals (var_tys G (tag obj) r)\<rparr>\<Colon>\<preceq>\<surd>r"
   284 apply (auto simp add: oconf_def)
   285 apply (drule_tac var_tys_Some_eq [THEN iffD1]) 
   286 defer
   287 apply (subst obj_ty_cong)
   288 apply(auto dest!: fields_table_SomeD obj_ty_CInst1 obj_ty_Arr1
   289            split add: sum.split_asm obj_tag.split_asm)
   290 done
   291 
   292 (*
   293 lemma oconf_init_obj_lemma: 
   294 "\<lbrakk>\<And>C c. class G C = Some c \<Longrightarrow> unique (fields G C);  
   295   \<And>C c f fld. \<lbrakk>class G C = Some c; table_of (fields G C) f = Some fld \<rbrakk> 
   296             \<Longrightarrow> is_type G (type fld);  
   297   (case r of 
   298      Heap a \<Rightarrow> is_type G (obj_ty \<lparr>tag=oi,values=fs\<rparr>) 
   299   | Stat C \<Rightarrow> is_class G C)
   300 \<rbrakk> \<Longrightarrow>  G,s\<turnstile>\<lparr>tag=oi, values=init_vals (var_tys G oi r)\<rparr>\<Colon>\<preceq>\<surd>r"
   301 apply (auto simp add: oconf_def)
   302 apply (drule_tac var_tys_Some_eq [THEN iffD1]) 
   303 defer
   304 apply (subst obj_ty_eq)
   305 apply(auto dest!: fields_table_SomeD split add: sum.split_asm obj_tag.split_asm)
   306 done
   307 *)
   308 
   309 
   310 section "state conformance"
   311 
   312 constdefs
   313 
   314   conforms :: "state \<Rightarrow> env_ \<Rightarrow> bool"          (     "_\<Colon>\<preceq>_"   [71,71]      70)
   315    "xs\<Colon>\<preceq>E \<equiv> let (G, L) = E; s = snd xs; l = locals s in
   316       (\<forall>r. \<forall>obj\<in>globs s r:           G,s\<turnstile>obj   \<Colon>\<preceq>\<surd>r) \<and>
   317                   \<spacespace>                   G,s\<turnstile>l    [\<Colon>\<preceq>]L\<spacespace> \<and>
   318       (\<forall>a. fst xs=Some(Xcpt (Loc a)) \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable))"
   319 
   320 section "conforms"
   321 
   322 lemma conforms_globsD: 
   323 "\<lbrakk>(x, s)\<Colon>\<preceq>(G, L); globs s r = Some obj\<rbrakk> \<Longrightarrow> G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r"
   324 by (auto simp: conforms_def Let_def)
   325 
   326 lemma conforms_localD: "(x, s)\<Colon>\<preceq>(G, L) \<Longrightarrow> G,s\<turnstile>locals s[\<Colon>\<preceq>]L"
   327 by (auto simp: conforms_def Let_def)
   328 
   329 lemma conforms_XcptLocD: "\<lbrakk>(x, s)\<Colon>\<preceq>(G, L); x = Some (Xcpt (Loc a))\<rbrakk> \<Longrightarrow>  
   330 	  G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable)"
   331 by (auto simp: conforms_def Let_def)
   332 
   333 lemma conforms_RefTD: 
   334  "\<lbrakk>G,s\<turnstile>a'\<Colon>\<preceq>RefT t; a' \<noteq> Null; (x,s) \<Colon>\<preceq>(G, L)\<rbrakk> \<Longrightarrow>  
   335    \<exists>a obj. a' = Addr a \<and> globs s (Inl a) = Some obj \<and>  
   336    G\<turnstile>obj_ty obj\<preceq>RefT t \<and> is_type G (obj_ty obj)"
   337 apply (drule_tac conf_RefTD)
   338 apply clarsimp
   339 apply (rule conforms_globsD [THEN oconf_is_type])
   340 apply auto
   341 done
   342 
   343 lemma conforms_Jump [iff]:
   344   "((Some (Jump j), s)\<Colon>\<preceq>(G, L)) = (Norm s\<Colon>\<preceq>(G, L))"
   345 by (auto simp: conforms_def)
   346 
   347 lemma conforms_StdXcpt [iff]: 
   348   "((Some (Xcpt (Std xn)), s)\<Colon>\<preceq>(G, L)) = (Norm s\<Colon>\<preceq>(G, L))"
   349 by (auto simp: conforms_def)
   350 
   351 lemma conforms_raise_if [iff]: 
   352   "((raise_if c xn x, s)\<Colon>\<preceq>(G, L)) = ((x, s)\<Colon>\<preceq>(G, L))"
   353 by (auto simp: abrupt_if_def)
   354 
   355 
   356 lemma conforms_NormI: "(x, s)\<Colon>\<preceq>(G, L) \<Longrightarrow> Norm s\<Colon>\<preceq>(G, L)"
   357 by (auto simp: conforms_def Let_def)
   358 
   359 
   360 lemma conforms_absorb [rule_format]:
   361   "(a, b)\<Colon>\<preceq>(G, L) \<longrightarrow> (absorb j a, b)\<Colon>\<preceq>(G, L)"
   362 apply (rule impI)
   363 apply ( case_tac a)
   364 apply (case_tac "absorb j a")
   365 apply auto
   366 apply (case_tac "absorb j (Some a)",auto)
   367 apply (erule conforms_NormI)
   368 done
   369 
   370 lemma conformsI: "\<lbrakk>\<forall>r. \<forall>obj\<in>globs s r: G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r;  
   371      G,s\<turnstile>locals s[\<Colon>\<preceq>]L;  
   372      \<forall>a. x = Some (Xcpt (Loc a)) \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable)\<rbrakk> \<Longrightarrow> 
   373   (x, s)\<Colon>\<preceq>(G, L)"
   374 by (auto simp: conforms_def Let_def)
   375 
   376 lemma conforms_xconf: "\<lbrakk>(x, s)\<Colon>\<preceq>(G,L);   
   377  \<forall>a. x' = Some (Xcpt (Loc a)) \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable)\<rbrakk> \<Longrightarrow> 
   378  (x',s)\<Colon>\<preceq>(G,L)"
   379 by (fast intro: conformsI elim: conforms_globsD conforms_localD)
   380 
   381 lemma conforms_lupd: 
   382  "\<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)"
   383 by (force intro: conformsI lconf_upd dest: conforms_globsD conforms_localD 
   384                                            conforms_XcptLocD simp: oconf_def)
   385 
   386 
   387 lemmas conforms_allocL_aux = conforms_localD [THEN lconf_ext]
   388 
   389 lemma conforms_allocL: 
   390   "\<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))"
   391 by (force intro: conformsI dest: conforms_globsD 
   392           elim: conforms_XcptLocD conforms_allocL_aux simp: oconf_def)
   393 
   394 lemmas conforms_deallocL_aux = conforms_localD [THEN lconf_deallocL]
   395 
   396 lemma conforms_deallocL: "\<And>s.\<lbrakk>s\<Colon>\<preceq>(G, L(vn\<mapsto>T)); L vn = None\<rbrakk> \<Longrightarrow> s\<Colon>\<preceq>(G,L)"
   397 by (fast intro: conformsI dest: conforms_globsD 
   398          elim: conforms_XcptLocD conforms_deallocL_aux)
   399 
   400 lemma conforms_gext: "\<lbrakk>(x, s)\<Colon>\<preceq>(G,L); s\<le>|s';  
   401   \<forall>r. \<forall>obj\<in>globs s' r: G,s'\<turnstile>obj\<Colon>\<preceq>\<surd>r;  
   402    locals s'=locals s\<rbrakk> \<Longrightarrow> (x,s')\<Colon>\<preceq>(G,L)"
   403 by (force intro!: conformsI dest: conforms_localD conforms_XcptLocD)
   404 
   405 
   406 lemma conforms_xgext: 
   407   "\<lbrakk>(x ,s)\<Colon>\<preceq>(G,L); (x', s')\<Colon>\<preceq>(G, L); s'\<le>|s\<rbrakk> \<Longrightarrow> (x',s)\<Colon>\<preceq>(G,L)"
   408 apply (erule_tac conforms_xconf)
   409 apply (fast dest: conforms_XcptLocD)
   410 done
   411 
   412 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> 
   413 \<Longrightarrow>  (x, gupd(r\<mapsto>obj)s)\<Colon>\<preceq>(G, L)"
   414 apply (rule conforms_gext)
   415 apply    auto
   416 apply (force dest: conforms_globsD simp add: oconf_def)+
   417 done
   418 
   419 lemma conforms_upd_gobj: "\<lbrakk>(x,s)\<Colon>\<preceq>(G, L); globs s r = Some obj; 
   420   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)"
   421 apply (rule conforms_gext)
   422 apply auto
   423 apply (drule (1) conforms_globsD)
   424 apply (simp add: oconf_def)
   425 apply safe
   426 apply (rule lconf_upd)
   427 apply auto
   428 apply (simp only: obj_ty_cong) 
   429 apply (force dest: conforms_globsD intro!: lconf_upd 
   430        simp add: oconf_def cong del: sum.weak_case_cong)
   431 done
   432 
   433 lemma conforms_set_locals: 
   434   "\<lbrakk>(x,s)\<Colon>\<preceq>(G, L'); G,s\<turnstile>l[\<Colon>\<preceq>]L\<rbrakk> \<Longrightarrow> (x,set_locals l s)\<Colon>\<preceq>(G,L)"
   435 apply (auto intro!: conformsI dest: conforms_globsD 
   436             elim!: conforms_XcptLocD simp add: oconf_def)
   437 done
   438 
   439 lemma conforms_return: "\<And>s'. \<lbrakk>(x,s)\<Colon>\<preceq>(G, L); (x',s')\<Colon>\<preceq>(G, L'); s\<le>|s'\<rbrakk> \<Longrightarrow>  
   440   (x',set_locals (locals s) s')\<Colon>\<preceq>(G, L)"
   441 apply (rule conforms_xconf)
   442 prefer 2 apply (force dest: conforms_XcptLocD)
   443 apply (erule conforms_gext)
   444 apply (force dest: conforms_globsD)+
   445 done
   446 
   447 end