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