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