src/HOL/Bali/Conform.thy
author wenzelm
Fri Feb 18 16:36:42 2011 +0100 (2011-02-18)
changeset 41778 5f79a9e42507
parent 37956 ee939247b2fb
child 46212 d86ef6b96097
permissions -rw-r--r--
modernized specifications;
     1 (*  Title:      HOL/Bali/Conform.thy
     2     Author:     David von Oheimb
     3 *)
     4 
     5 header {* Conformance notions for the type soundness proof for Java *}
     6 
     7 theory Conform imports State begin
     8 
     9 text {*
    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 *}
    18 
    19 type_synonym env' = "prog \<times> (lname, ty) table" (* same as env of WellType.thy *)
    20 
    21 
    22 section "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 {* 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 *}
    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 section "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. Option.map 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 section "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 section "weak value list conformance"
   252 
   253 text {* 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 *}
   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 section "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 obj_ty_CInst1 obj_ty_Arr1
   374            split add: sum.split_asm obj_tag.split_asm)
   375 done
   376 
   377 section "state conformance"
   378 
   379 definition
   380   conforms :: "state \<Rightarrow> env' \<Rightarrow> bool"  ("_\<Colon>\<preceq>_" [71,71] 70)  where
   381    "xs\<Colon>\<preceq>E =
   382       (let (G, L) = E; s = snd xs; l = locals s in
   383         (\<forall>r. \<forall>obj\<in>globs s r:           G,s\<turnstile>obj   \<Colon>\<preceq>\<surd>r) \<and>
   384                     \<spacespace>                   G,s\<turnstile>l    [\<sim>\<Colon>\<preceq>]L\<spacespace> \<and>
   385         (\<forall>a. fst xs=Some(Xcpt (Loc a)) \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable)) \<and>
   386              (fst xs=Some(Jump Ret) \<longrightarrow> l Result \<noteq> None))"
   387 
   388 section "conforms"
   389 
   390 lemma conforms_globsD: 
   391 "\<lbrakk>(x, s)\<Colon>\<preceq>(G, L); globs s r = Some obj\<rbrakk> \<Longrightarrow> G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r"
   392 by (auto simp: conforms_def Let_def)
   393 
   394 lemma conforms_localD: "(x, s)\<Colon>\<preceq>(G, L) \<Longrightarrow> G,s\<turnstile>locals s[\<sim>\<Colon>\<preceq>]L"
   395 by (auto simp: conforms_def Let_def)
   396 
   397 lemma conforms_XcptLocD: "\<lbrakk>(x, s)\<Colon>\<preceq>(G, L); x = Some (Xcpt (Loc a))\<rbrakk> \<Longrightarrow>  
   398           G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable)"
   399 by (auto simp: conforms_def Let_def)
   400 
   401 lemma conforms_RetD: "\<lbrakk>(x, s)\<Colon>\<preceq>(G, L); x = Some (Jump Ret)\<rbrakk> \<Longrightarrow>  
   402           (locals s) Result \<noteq> None"
   403 by (auto simp: conforms_def Let_def)
   404 
   405 lemma conforms_RefTD: 
   406  "\<lbrakk>G,s\<turnstile>a'\<Colon>\<preceq>RefT t; a' \<noteq> Null; (x,s) \<Colon>\<preceq>(G, L)\<rbrakk> \<Longrightarrow>  
   407    \<exists>a obj. a' = Addr a \<and> globs s (Inl a) = Some obj \<and>  
   408    G\<turnstile>obj_ty obj\<preceq>RefT t \<and> is_type G (obj_ty obj)"
   409 apply (drule_tac conf_RefTD)
   410 apply clarsimp
   411 apply (rule conforms_globsD [THEN oconf_is_type])
   412 apply auto
   413 done
   414 
   415 lemma conforms_Jump [iff]:
   416   "j=Ret \<longrightarrow> locals s Result \<noteq> None 
   417    \<Longrightarrow> ((Some (Jump j), s)\<Colon>\<preceq>(G, L)) = (Norm s\<Colon>\<preceq>(G, L))"
   418 by (auto simp: conforms_def Let_def)
   419 
   420 lemma conforms_StdXcpt [iff]: 
   421   "((Some (Xcpt (Std xn)), s)\<Colon>\<preceq>(G, L)) = (Norm s\<Colon>\<preceq>(G, L))"
   422 by (auto simp: conforms_def)
   423 
   424 lemma conforms_Err [iff]:
   425    "((Some (Error e), s)\<Colon>\<preceq>(G, L)) = (Norm s\<Colon>\<preceq>(G, L))"
   426   by (auto simp: conforms_def)  
   427 
   428 lemma conforms_raise_if [iff]: 
   429   "((raise_if c xn x, s)\<Colon>\<preceq>(G, L)) = ((x, s)\<Colon>\<preceq>(G, L))"
   430 by (auto simp: abrupt_if_def)
   431 
   432 lemma conforms_error_if [iff]: 
   433   "((error_if c err x, s)\<Colon>\<preceq>(G, L)) = ((x, s)\<Colon>\<preceq>(G, L))"
   434 by (auto simp: abrupt_if_def split: split_if)
   435 
   436 lemma conforms_NormI: "(x, s)\<Colon>\<preceq>(G, L) \<Longrightarrow> Norm s\<Colon>\<preceq>(G, L)"
   437 by (auto simp: conforms_def Let_def)
   438 
   439 lemma conforms_absorb [rule_format]:
   440   "(a, b)\<Colon>\<preceq>(G, L) \<longrightarrow> (absorb j a, b)\<Colon>\<preceq>(G, L)"
   441 apply (rule impI)
   442 apply ( case_tac a)
   443 apply (case_tac "absorb j a")
   444 apply auto
   445 apply (case_tac "absorb j (Some a)",auto)
   446 apply (erule conforms_NormI)
   447 done
   448 
   449 lemma conformsI: "\<lbrakk>\<forall>r. \<forall>obj\<in>globs s r: G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r;  
   450      G,s\<turnstile>locals s[\<sim>\<Colon>\<preceq>]L;  
   451      \<forall>a. x = Some (Xcpt (Loc a)) \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable);
   452      x = Some (Jump Ret)\<longrightarrow> locals s Result \<noteq> None\<rbrakk> \<Longrightarrow> 
   453   (x, s)\<Colon>\<preceq>(G, L)"
   454 by (auto simp: conforms_def Let_def)
   455 
   456 lemma conforms_xconf: "\<lbrakk>(x, s)\<Colon>\<preceq>(G,L);   
   457  \<forall>a. x' = Some (Xcpt (Loc a)) \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable);
   458      x' = Some (Jump Ret) \<longrightarrow> locals s Result \<noteq> None\<rbrakk> \<Longrightarrow> 
   459  (x',s)\<Colon>\<preceq>(G,L)"
   460 by (fast intro: conformsI elim: conforms_globsD conforms_localD)
   461 
   462 lemma conforms_lupd: 
   463  "\<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)"
   464 by (force intro: conformsI wlconf_upd dest: conforms_globsD conforms_localD 
   465                                            conforms_XcptLocD conforms_RetD 
   466           simp: oconf_def)
   467 
   468 
   469 lemmas conforms_allocL_aux = conforms_localD [THEN wlconf_ext]
   470 
   471 lemma conforms_allocL: 
   472   "\<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))"
   473 by (force intro: conformsI dest: conforms_globsD conforms_RetD 
   474           elim: conforms_XcptLocD  conforms_allocL_aux 
   475           simp: oconf_def)
   476 
   477 lemmas conforms_deallocL_aux = conforms_localD [THEN wlconf_deallocL]
   478 
   479 lemma conforms_deallocL: "\<And>s.\<lbrakk>s\<Colon>\<preceq>(G, L(vn\<mapsto>T)); L vn = None\<rbrakk> \<Longrightarrow> s\<Colon>\<preceq>(G,L)"
   480 by (fast intro: conformsI dest: conforms_globsD conforms_RetD
   481          elim: conforms_XcptLocD conforms_deallocL_aux)
   482 
   483 lemma conforms_gext: "\<lbrakk>(x, s)\<Colon>\<preceq>(G,L); s\<le>|s';  
   484   \<forall>r. \<forall>obj\<in>globs s' r: G,s'\<turnstile>obj\<Colon>\<preceq>\<surd>r;  
   485    locals s'=locals s\<rbrakk> \<Longrightarrow> (x,s')\<Colon>\<preceq>(G,L)"
   486 apply (rule conformsI)
   487 apply     assumption
   488 apply    (drule conforms_localD) apply force
   489 apply   (intro strip)
   490 apply  (drule (1) conforms_XcptLocD) apply force 
   491 apply (intro strip)
   492 apply (drule (1) conforms_RetD) apply force
   493 done
   494 
   495 
   496 
   497 lemma conforms_xgext: 
   498   "\<lbrakk>(x ,s)\<Colon>\<preceq>(G,L); (x', s')\<Colon>\<preceq>(G, L); s'\<le>|s;dom (locals s') \<subseteq> dom (locals s)\<rbrakk> 
   499    \<Longrightarrow> (x',s)\<Colon>\<preceq>(G,L)"
   500 apply (erule_tac conforms_xconf)
   501 apply  (fast dest: conforms_XcptLocD)
   502 apply (intro strip)
   503 apply (drule (1) conforms_RetD) 
   504 apply (auto dest: domI)
   505 done
   506 
   507 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> 
   508 \<Longrightarrow>  (x, gupd(r\<mapsto>obj)s)\<Colon>\<preceq>(G, L)"
   509 apply (rule conforms_gext)
   510 apply    auto
   511 apply (force dest: conforms_globsD simp add: oconf_def)+
   512 done
   513 
   514 lemma conforms_upd_gobj: "\<lbrakk>(x,s)\<Colon>\<preceq>(G, L); globs s r = Some obj; 
   515   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)"
   516 apply (rule conforms_gext)
   517 apply auto
   518 apply (drule (1) conforms_globsD)
   519 apply (simp add: oconf_def)
   520 apply safe
   521 apply (rule lconf_upd)
   522 apply auto
   523 apply (simp only: obj_ty_cong) 
   524 apply (force dest: conforms_globsD intro!: lconf_upd 
   525        simp add: oconf_def cong del: sum.weak_case_cong)
   526 done
   527 
   528 lemma conforms_set_locals: 
   529   "\<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> 
   530    \<Longrightarrow> (x,set_locals l s)\<Colon>\<preceq>(G,L)"
   531 apply (rule conformsI)
   532 apply     (intro strip)
   533 apply     simp
   534 apply     (drule (2) conforms_globsD)
   535 apply    simp
   536 apply   (intro strip)
   537 apply   (drule (1) conforms_XcptLocD)
   538 apply   simp
   539 apply (intro strip)
   540 apply (drule (1) conforms_RetD)
   541 apply simp
   542 done
   543 
   544 lemma conforms_locals: 
   545   "\<lbrakk>(a,b)\<Colon>\<preceq>(G, L); L x = Some T;locals b x \<noteq>None\<rbrakk>
   546    \<Longrightarrow> G,b\<turnstile>the (locals b x)\<Colon>\<preceq>T"
   547 apply (force simp: conforms_def Let_def wlconf_def)
   548 done
   549 
   550 lemma conforms_return: 
   551 "\<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>  
   552   (x',set_locals (locals s) s')\<Colon>\<preceq>(G, L)"
   553 apply (rule conforms_xconf)
   554 prefer 2 apply (force dest: conforms_XcptLocD)
   555 apply (erule conforms_gext)
   556 apply (force dest: conforms_globsD)+
   557 done
   558 
   559 
   560 end