src/HOL/Bali/Conform.thy
author haftmann
Wed Jun 30 16:46:44 2010 +0200 (2010-06-30)
changeset 37659 14cabf5fa710
parent 35416 d8d7d1b785af
child 37956 ee939247b2fb
permissions -rw-r--r--
more speaking names
     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 types 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) where
   100            "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"
   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 lconf :: "prog \<Rightarrow> st \<Rightarrow> ('a, val) table \<Rightarrow> ('a, ty) table \<Rightarrow> bool" ("_,_\<turnstile>_[\<Colon>\<preceq>]_" [71,71,71,71] 70) where
   181            "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"
   182 
   183 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"
   184 by (force simp: lconf_def)
   185 
   186 
   187 lemma lconf_cong [simp]: "\<And>s. G,set_locals x s\<turnstile>l[\<Colon>\<preceq>]L = G,s\<turnstile>l[\<Colon>\<preceq>]L"
   188 by (auto simp: lconf_def)
   189 
   190 lemma lconf_lupd [simp]: "G,lupd(vn\<mapsto>v)s\<turnstile>l[\<Colon>\<preceq>]L = G,s\<turnstile>l[\<Colon>\<preceq>]L"
   191 by (auto simp: lconf_def)
   192 
   193 (* unused *)
   194 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"
   195 by (auto simp: lconf_def)
   196 
   197 lemma lconf_upd: "\<lbrakk>G,s\<turnstile>l[\<Colon>\<preceq>]L; G,s\<turnstile>v\<Colon>\<preceq>T; L vn = Some T\<rbrakk> \<Longrightarrow>  
   198   G,s\<turnstile>l(vn\<mapsto>v)[\<Colon>\<preceq>]L"
   199 by (auto simp: lconf_def)
   200 
   201 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)"
   202 by (auto simp: lconf_def)
   203 
   204 lemma lconf_map_sum [simp]: 
   205  "G,s\<turnstile>l1 (+) l2[\<Colon>\<preceq>]L1 (+) L2 = (G,s\<turnstile>l1[\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>l2[\<Colon>\<preceq>]L2)"
   206 apply (unfold lconf_def)
   207 apply safe
   208 apply (case_tac [3] "n")
   209 apply (force split add: sum.split)+
   210 done
   211 
   212 lemma lconf_ext_list [rule_format (no_asm)]: "
   213  \<And>X. \<lbrakk>G,s\<turnstile>l[\<Colon>\<preceq>]L\<rbrakk> \<Longrightarrow> 
   214       \<forall>vs Ts. distinct vns \<longrightarrow> length Ts = length vns 
   215       \<longrightarrow> list_all2 (conf G s) vs Ts \<longrightarrow> G,s\<turnstile>l(vns[\<mapsto>]vs)[\<Colon>\<preceq>]L(vns[\<mapsto>]Ts)"
   216 apply (unfold lconf_def)
   217 apply (induct_tac "vns")
   218 apply  clarsimp
   219 apply clarify
   220 apply (frule list_all2_lengthD)
   221 apply (clarsimp)
   222 done
   223 
   224 
   225 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"
   226 apply (simp only: lconf_def)
   227 apply safe
   228 apply (drule spec)
   229 apply (drule ospec)
   230 apply auto
   231 done 
   232 
   233 
   234 lemma lconf_gext [elim]: "\<lbrakk>G,s\<turnstile>l[\<Colon>\<preceq>]L; s\<le>|s'\<rbrakk> \<Longrightarrow> G,s'\<turnstile>l[\<Colon>\<preceq>]L"
   235 apply (simp only: lconf_def)
   236 apply fast
   237 done
   238 
   239 lemma lconf_empty [simp, intro!]: "G,s\<turnstile>vs[\<Colon>\<preceq>]empty"
   240 apply (unfold lconf_def)
   241 apply force
   242 done
   243 
   244 lemma lconf_init_vals [intro!]: 
   245         " \<forall>n. \<forall>T\<in>fs n:is_type G T \<Longrightarrow> G,s\<turnstile>init_vals fs[\<Colon>\<preceq>]fs"
   246 apply (unfold lconf_def)
   247 apply force
   248 done
   249 
   250 section "weak value list conformance"
   251 
   252 text {* Only if the value is defined it has to conform to its type. 
   253         This is the contribution of the definite assignment analysis to 
   254         the notion of conformance. The definite assignment analysis ensures
   255         that the program only attempts to access local variables that 
   256         actually have a defined value in the state. 
   257         So conformance must only ensure that the
   258         defined values are of the right type, and not also that the value
   259         is defined. 
   260 *}
   261 
   262   
   263 definition wlconf :: "prog \<Rightarrow> st \<Rightarrow> ('a, val) table \<Rightarrow> ('a, ty) table \<Rightarrow> bool" ("_,_\<turnstile>_[\<sim>\<Colon>\<preceq>]_" [71,71,71,71] 70) where
   264            "G,s\<turnstile>vs[\<sim>\<Colon>\<preceq>]Ts \<equiv> \<forall>n. \<forall>T\<in>Ts n: \<forall> v\<in>vs n: G,s\<turnstile>v\<Colon>\<preceq>T"
   265 
   266 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"
   267 by (auto simp: wlconf_def)
   268 
   269 
   270 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"
   271 by (auto simp: wlconf_def)
   272 
   273 lemma wlconf_lupd [simp]: "G,lupd(vn\<mapsto>v)s\<turnstile>l[\<sim>\<Colon>\<preceq>]L = G,s\<turnstile>l[\<sim>\<Colon>\<preceq>]L"
   274 by (auto simp: wlconf_def)
   275 
   276 
   277 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>  
   278   G,s\<turnstile>l(vn\<mapsto>v)[\<sim>\<Colon>\<preceq>]L"
   279 by (auto simp: wlconf_def)
   280 
   281 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)"
   282 by (auto simp: wlconf_def)
   283 
   284 lemma wlconf_map_sum [simp]: 
   285  "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)"
   286 apply (unfold wlconf_def)
   287 apply safe
   288 apply (case_tac [3] "n")
   289 apply (force split add: sum.split)+
   290 done
   291 
   292 lemma wlconf_ext_list [rule_format (no_asm)]: "
   293  \<And>X. \<lbrakk>G,s\<turnstile>l[\<sim>\<Colon>\<preceq>]L\<rbrakk> \<Longrightarrow> 
   294       \<forall>vs Ts. distinct vns \<longrightarrow> length Ts = length vns 
   295       \<longrightarrow> list_all2 (conf G s) vs Ts \<longrightarrow> G,s\<turnstile>l(vns[\<mapsto>]vs)[\<sim>\<Colon>\<preceq>]L(vns[\<mapsto>]Ts)"
   296 apply (unfold wlconf_def)
   297 apply (induct_tac "vns")
   298 apply  clarsimp
   299 apply clarify
   300 apply (frule list_all2_lengthD)
   301 apply clarsimp
   302 done
   303 
   304 
   305 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"
   306 apply (simp only: wlconf_def)
   307 apply safe
   308 apply (drule spec)
   309 apply (drule ospec)
   310 defer
   311 apply (drule ospec )
   312 apply auto
   313 done 
   314 
   315 
   316 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"
   317 apply (simp only: wlconf_def)
   318 apply fast
   319 done
   320 
   321 lemma wlconf_empty [simp, intro!]: "G,s\<turnstile>vs[\<sim>\<Colon>\<preceq>]empty"
   322 apply (unfold wlconf_def)
   323 apply force
   324 done
   325 
   326 lemma wlconf_empty_vals: "G,s\<turnstile>empty[\<sim>\<Colon>\<preceq>]ts"
   327   by (simp add: wlconf_def)
   328 
   329 lemma wlconf_init_vals [intro!]: 
   330         " \<forall>n. \<forall>T\<in>fs n:is_type G T \<Longrightarrow> G,s\<turnstile>init_vals fs[\<sim>\<Colon>\<preceq>]fs"
   331 apply (unfold wlconf_def)
   332 apply force
   333 done
   334 
   335 lemma lconf_wlconf:
   336  "G,s\<turnstile>l[\<Colon>\<preceq>]L \<Longrightarrow> G,s\<turnstile>l[\<sim>\<Colon>\<preceq>]L"
   337 by (force simp add: lconf_def wlconf_def)
   338 
   339 section "object conformance"
   340 
   341 definition oconf :: "prog \<Rightarrow> st \<Rightarrow> obj \<Rightarrow> oref \<Rightarrow> bool" ("_,_\<turnstile>_\<Colon>\<preceq>\<surd>_"  [71,71,71,71] 70) where
   342            "G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r \<equiv> G,s\<turnstile>values obj[\<Colon>\<preceq>]var_tys G (tag obj) r \<and> 
   343                            (case r of 
   344                               Heap a \<Rightarrow> is_type G (obj_ty obj) 
   345                             | Stat C \<Rightarrow> True)"
   346 
   347 
   348 lemma oconf_is_type: "G,s\<turnstile>obj\<Colon>\<preceq>\<surd>Heap a \<Longrightarrow> is_type G (obj_ty obj)"
   349 by (auto simp: oconf_def Let_def)
   350 
   351 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"
   352 by (simp add: oconf_def) 
   353 
   354 lemma oconf_cong [simp]: "G,set_locals l s\<turnstile>obj\<Colon>\<preceq>\<surd>r = G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r"
   355 by (auto simp: oconf_def Let_def)
   356 
   357 lemma oconf_init_obj_lemma: 
   358 "\<lbrakk>\<And>C c. class G C = Some c \<Longrightarrow> unique (DeclConcepts.fields G C);  
   359   \<And>C c f fld. \<lbrakk>class G C = Some c; 
   360                 table_of (DeclConcepts.fields G C) f = Some fld \<rbrakk> 
   361             \<Longrightarrow> is_type G (type fld);  
   362   (case r of 
   363      Heap a \<Rightarrow> is_type G (obj_ty obj) 
   364   | Stat C \<Rightarrow> is_class G C)
   365 \<rbrakk> \<Longrightarrow>  G,s\<turnstile>obj \<lparr>values:=init_vals (var_tys G (tag obj) r)\<rparr>\<Colon>\<preceq>\<surd>r"
   366 apply (auto simp add: oconf_def)
   367 apply (drule_tac var_tys_Some_eq [THEN iffD1]) 
   368 defer
   369 apply (subst obj_ty_cong)
   370 apply(auto dest!: fields_table_SomeD obj_ty_CInst1 obj_ty_Arr1
   371            split add: sum.split_asm obj_tag.split_asm)
   372 done
   373 
   374 section "state conformance"
   375 
   376 definition conforms :: "state \<Rightarrow> env' \<Rightarrow> bool"   ("_\<Colon>\<preceq>_"   [71,71]      70)  where
   377    "xs\<Colon>\<preceq>E \<equiv> let (G, L) = E; s = snd xs; l = locals s in
   378     (\<forall>r. \<forall>obj\<in>globs s r:           G,s\<turnstile>obj   \<Colon>\<preceq>\<surd>r) \<and>
   379                 \<spacespace>                   G,s\<turnstile>l    [\<sim>\<Colon>\<preceq>]L\<spacespace> \<and>
   380     (\<forall>a. fst xs=Some(Xcpt (Loc a)) \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable)) \<and>
   381          (fst xs=Some(Jump Ret) \<longrightarrow> l Result \<noteq> None)"
   382 
   383 section "conforms"
   384 
   385 lemma conforms_globsD: 
   386 "\<lbrakk>(x, s)\<Colon>\<preceq>(G, L); globs s r = Some obj\<rbrakk> \<Longrightarrow> G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r"
   387 by (auto simp: conforms_def Let_def)
   388 
   389 lemma conforms_localD: "(x, s)\<Colon>\<preceq>(G, L) \<Longrightarrow> G,s\<turnstile>locals s[\<sim>\<Colon>\<preceq>]L"
   390 by (auto simp: conforms_def Let_def)
   391 
   392 lemma conforms_XcptLocD: "\<lbrakk>(x, s)\<Colon>\<preceq>(G, L); x = Some (Xcpt (Loc a))\<rbrakk> \<Longrightarrow>  
   393           G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable)"
   394 by (auto simp: conforms_def Let_def)
   395 
   396 lemma conforms_RetD: "\<lbrakk>(x, s)\<Colon>\<preceq>(G, L); x = Some (Jump Ret)\<rbrakk> \<Longrightarrow>  
   397           (locals s) Result \<noteq> None"
   398 by (auto simp: conforms_def Let_def)
   399 
   400 lemma conforms_RefTD: 
   401  "\<lbrakk>G,s\<turnstile>a'\<Colon>\<preceq>RefT t; a' \<noteq> Null; (x,s) \<Colon>\<preceq>(G, L)\<rbrakk> \<Longrightarrow>  
   402    \<exists>a obj. a' = Addr a \<and> globs s (Inl a) = Some obj \<and>  
   403    G\<turnstile>obj_ty obj\<preceq>RefT t \<and> is_type G (obj_ty obj)"
   404 apply (drule_tac conf_RefTD)
   405 apply clarsimp
   406 apply (rule conforms_globsD [THEN oconf_is_type])
   407 apply auto
   408 done
   409 
   410 lemma conforms_Jump [iff]:
   411   "j=Ret \<longrightarrow> locals s Result \<noteq> None 
   412    \<Longrightarrow> ((Some (Jump j), s)\<Colon>\<preceq>(G, L)) = (Norm s\<Colon>\<preceq>(G, L))"
   413 by (auto simp: conforms_def Let_def)
   414 
   415 lemma conforms_StdXcpt [iff]: 
   416   "((Some (Xcpt (Std xn)), s)\<Colon>\<preceq>(G, L)) = (Norm s\<Colon>\<preceq>(G, L))"
   417 by (auto simp: conforms_def)
   418 
   419 lemma conforms_Err [iff]:
   420    "((Some (Error e), s)\<Colon>\<preceq>(G, L)) = (Norm s\<Colon>\<preceq>(G, L))"
   421   by (auto simp: conforms_def)  
   422 
   423 lemma conforms_raise_if [iff]: 
   424   "((raise_if c xn x, s)\<Colon>\<preceq>(G, L)) = ((x, s)\<Colon>\<preceq>(G, L))"
   425 by (auto simp: abrupt_if_def)
   426 
   427 lemma conforms_error_if [iff]: 
   428   "((error_if c err x, s)\<Colon>\<preceq>(G, L)) = ((x, s)\<Colon>\<preceq>(G, L))"
   429 by (auto simp: abrupt_if_def split: split_if)
   430 
   431 lemma conforms_NormI: "(x, s)\<Colon>\<preceq>(G, L) \<Longrightarrow> Norm s\<Colon>\<preceq>(G, L)"
   432 by (auto simp: conforms_def Let_def)
   433 
   434 lemma conforms_absorb [rule_format]:
   435   "(a, b)\<Colon>\<preceq>(G, L) \<longrightarrow> (absorb j a, b)\<Colon>\<preceq>(G, L)"
   436 apply (rule impI)
   437 apply ( case_tac a)
   438 apply (case_tac "absorb j a")
   439 apply auto
   440 apply (case_tac "absorb j (Some a)",auto)
   441 apply (erule conforms_NormI)
   442 done
   443 
   444 lemma conformsI: "\<lbrakk>\<forall>r. \<forall>obj\<in>globs s r: G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r;  
   445      G,s\<turnstile>locals s[\<sim>\<Colon>\<preceq>]L;  
   446      \<forall>a. x = Some (Xcpt (Loc a)) \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable);
   447      x = Some (Jump Ret)\<longrightarrow> locals s Result \<noteq> None\<rbrakk> \<Longrightarrow> 
   448   (x, s)\<Colon>\<preceq>(G, L)"
   449 by (auto simp: conforms_def Let_def)
   450 
   451 lemma conforms_xconf: "\<lbrakk>(x, s)\<Colon>\<preceq>(G,L);   
   452  \<forall>a. x' = Some (Xcpt (Loc a)) \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable);
   453      x' = Some (Jump Ret) \<longrightarrow> locals s Result \<noteq> None\<rbrakk> \<Longrightarrow> 
   454  (x',s)\<Colon>\<preceq>(G,L)"
   455 by (fast intro: conformsI elim: conforms_globsD conforms_localD)
   456 
   457 lemma conforms_lupd: 
   458  "\<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)"
   459 by (force intro: conformsI wlconf_upd dest: conforms_globsD conforms_localD 
   460                                            conforms_XcptLocD conforms_RetD 
   461           simp: oconf_def)
   462 
   463 
   464 lemmas conforms_allocL_aux = conforms_localD [THEN wlconf_ext]
   465 
   466 lemma conforms_allocL: 
   467   "\<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))"
   468 by (force intro: conformsI dest: conforms_globsD conforms_RetD 
   469           elim: conforms_XcptLocD  conforms_allocL_aux 
   470           simp: oconf_def)
   471 
   472 lemmas conforms_deallocL_aux = conforms_localD [THEN wlconf_deallocL]
   473 
   474 lemma conforms_deallocL: "\<And>s.\<lbrakk>s\<Colon>\<preceq>(G, L(vn\<mapsto>T)); L vn = None\<rbrakk> \<Longrightarrow> s\<Colon>\<preceq>(G,L)"
   475 by (fast intro: conformsI dest: conforms_globsD conforms_RetD
   476          elim: conforms_XcptLocD conforms_deallocL_aux)
   477 
   478 lemma conforms_gext: "\<lbrakk>(x, s)\<Colon>\<preceq>(G,L); s\<le>|s';  
   479   \<forall>r. \<forall>obj\<in>globs s' r: G,s'\<turnstile>obj\<Colon>\<preceq>\<surd>r;  
   480    locals s'=locals s\<rbrakk> \<Longrightarrow> (x,s')\<Colon>\<preceq>(G,L)"
   481 apply (rule conformsI)
   482 apply     assumption
   483 apply    (drule conforms_localD) apply force
   484 apply   (intro strip)
   485 apply  (drule (1) conforms_XcptLocD) apply force 
   486 apply (intro strip)
   487 apply (drule (1) conforms_RetD) apply force
   488 done
   489 
   490 
   491 
   492 lemma conforms_xgext: 
   493   "\<lbrakk>(x ,s)\<Colon>\<preceq>(G,L); (x', s')\<Colon>\<preceq>(G, L); s'\<le>|s;dom (locals s') \<subseteq> dom (locals s)\<rbrakk> 
   494    \<Longrightarrow> (x',s)\<Colon>\<preceq>(G,L)"
   495 apply (erule_tac conforms_xconf)
   496 apply  (fast dest: conforms_XcptLocD)
   497 apply (intro strip)
   498 apply (drule (1) conforms_RetD) 
   499 apply (auto dest: domI)
   500 done
   501 
   502 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> 
   503 \<Longrightarrow>  (x, gupd(r\<mapsto>obj)s)\<Colon>\<preceq>(G, L)"
   504 apply (rule conforms_gext)
   505 apply    auto
   506 apply (force dest: conforms_globsD simp add: oconf_def)+
   507 done
   508 
   509 lemma conforms_upd_gobj: "\<lbrakk>(x,s)\<Colon>\<preceq>(G, L); globs s r = Some obj; 
   510   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)"
   511 apply (rule conforms_gext)
   512 apply auto
   513 apply (drule (1) conforms_globsD)
   514 apply (simp add: oconf_def)
   515 apply safe
   516 apply (rule lconf_upd)
   517 apply auto
   518 apply (simp only: obj_ty_cong) 
   519 apply (force dest: conforms_globsD intro!: lconf_upd 
   520        simp add: oconf_def cong del: sum.weak_case_cong)
   521 done
   522 
   523 lemma conforms_set_locals: 
   524   "\<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> 
   525    \<Longrightarrow> (x,set_locals l s)\<Colon>\<preceq>(G,L)"
   526 apply (rule conformsI)
   527 apply     (intro strip)
   528 apply     simp
   529 apply     (drule (2) conforms_globsD)
   530 apply    simp
   531 apply   (intro strip)
   532 apply   (drule (1) conforms_XcptLocD)
   533 apply   simp
   534 apply (intro strip)
   535 apply (drule (1) conforms_RetD)
   536 apply simp
   537 done
   538 
   539 lemma conforms_locals: 
   540   "\<lbrakk>(a,b)\<Colon>\<preceq>(G, L); L x = Some T;locals b x \<noteq>None\<rbrakk>
   541    \<Longrightarrow> G,b\<turnstile>the (locals b x)\<Colon>\<preceq>T"
   542 apply (force simp: conforms_def Let_def wlconf_def)
   543 done
   544 
   545 lemma conforms_return: 
   546 "\<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>  
   547   (x',set_locals (locals s) s')\<Colon>\<preceq>(G, L)"
   548 apply (rule conforms_xconf)
   549 prefer 2 apply (force dest: conforms_XcptLocD)
   550 apply (erule conforms_gext)
   551 apply (force dest: conforms_globsD)+
   552 done
   553 
   554 
   555 end