src/HOL/Bali/TypeSafe.thy
author haftmann
Tue May 04 08:55:43 2010 +0200 (2010-05-04)
changeset 36635 080b755377c0
parent 36176 3fe7e97ccca8
child 37956 ee939247b2fb
permissions -rw-r--r--
locale predicates of classes carry a mandatory "class" prefix
     1 (*  Title:      HOL/Bali/TypeSafe.thy
     2     Author:     David von Oheimb and Norbert Schirmer
     3 *)
     4 header {* The type soundness proof for Java *}
     5 
     6 theory TypeSafe
     7 imports DefiniteAssignmentCorrect Conform
     8 begin
     9 
    10 section "error free"
    11  
    12 lemma error_free_halloc:
    13   assumes halloc: "G\<turnstile>s0 \<midarrow>halloc oi\<succ>a\<rightarrow> s1" and
    14           error_free_s0: "error_free s0"
    15   shows "error_free s1"
    16 proof -
    17   from halloc error_free_s0
    18   obtain abrupt0 store0 abrupt1 store1
    19     where eqs: "s0=(abrupt0,store0)" "s1=(abrupt1,store1)" and
    20           halloc': "G\<turnstile>(abrupt0,store0) \<midarrow>halloc oi\<succ>a\<rightarrow> (abrupt1,store1)" and
    21           error_free_s0': "error_free (abrupt0,store0)"
    22     by (cases s0,cases s1) auto
    23   from halloc' error_free_s0'
    24   have "error_free (abrupt1,store1)"
    25   proof (induct)
    26     case Abrupt 
    27     then show ?case .
    28   next
    29     case New
    30     then show ?case
    31       by (auto split: split_if_asm)
    32   qed
    33   with eqs 
    34   show ?thesis
    35     by simp
    36 qed
    37 
    38 lemma error_free_sxalloc:
    39   assumes sxalloc: "G\<turnstile>s0 \<midarrow>sxalloc\<rightarrow> s1" and error_free_s0: "error_free s0"
    40   shows "error_free s1"
    41 proof -
    42   from sxalloc error_free_s0
    43   obtain abrupt0 store0 abrupt1 store1
    44     where eqs: "s0=(abrupt0,store0)" "s1=(abrupt1,store1)" and
    45           sxalloc': "G\<turnstile>(abrupt0,store0) \<midarrow>sxalloc\<rightarrow> (abrupt1,store1)" and
    46           error_free_s0': "error_free (abrupt0,store0)"
    47     by (cases s0,cases s1) auto
    48   from sxalloc' error_free_s0'
    49   have "error_free (abrupt1,store1)"
    50   proof (induct)
    51   qed (auto)
    52   with eqs 
    53   show ?thesis 
    54     by simp
    55 qed
    56 
    57 lemma error_free_check_field_access_eq:
    58  "error_free (check_field_access G accC statDeclC fn stat a s)
    59  \<Longrightarrow> (check_field_access G accC statDeclC fn stat a s) = s"
    60 apply (cases s)
    61 apply (auto simp add: check_field_access_def Let_def error_free_def 
    62                       abrupt_if_def 
    63             split: split_if_asm)
    64 done
    65 
    66 lemma error_free_check_method_access_eq:
    67 "error_free (check_method_access G accC statT mode sig a' s)
    68  \<Longrightarrow> (check_method_access G accC statT mode sig a' s) = s"
    69 apply (cases s)
    70 apply (auto simp add: check_method_access_def Let_def error_free_def 
    71                       abrupt_if_def 
    72             split: split_if_asm)
    73 done
    74 
    75 lemma error_free_FVar_lemma: 
    76      "error_free s 
    77        \<Longrightarrow> error_free (abupd (if stat then id else np a) s)"
    78   by (case_tac s) (auto split: split_if) 
    79 
    80 lemma error_free_init_lvars [simp,intro]:
    81 "error_free s \<Longrightarrow> 
    82   error_free (init_lvars G C sig mode a pvs s)"
    83 by (cases s) (auto simp add: init_lvars_def Let_def split: split_if)
    84 
    85 lemma error_free_LVar_lemma:   
    86 "error_free s \<Longrightarrow> error_free (assign (\<lambda>v. supd lupd(vn\<mapsto>v)) w s)"
    87 by (cases s) simp
    88 
    89 lemma error_free_throw [simp,intro]:
    90   "error_free s \<Longrightarrow> error_free (abupd (throw x) s)"
    91 by (cases s) (simp add: throw_def)
    92 
    93 
    94 section "result conformance"
    95 
    96 definition assign_conforms :: "st \<Rightarrow> (val \<Rightarrow> state \<Rightarrow> state) \<Rightarrow> ty \<Rightarrow> env' \<Rightarrow> bool" ("_\<le>|_\<preceq>_\<Colon>\<preceq>_" [71,71,71,71] 70) where
    97 "s\<le>|f\<preceq>T\<Colon>\<preceq>E \<equiv>
    98  (\<forall>s' w. Norm s'\<Colon>\<preceq>E \<longrightarrow> fst E,s'\<turnstile>w\<Colon>\<preceq>T \<longrightarrow> s\<le>|s' \<longrightarrow> assign f w (Norm s')\<Colon>\<preceq>E) \<and>
    99  (\<forall>s' w. error_free s' \<longrightarrow> (error_free (assign f w s')))"      
   100 
   101 
   102 definition rconf :: "prog \<Rightarrow> lenv \<Rightarrow> st \<Rightarrow> term \<Rightarrow> vals \<Rightarrow> tys \<Rightarrow> bool" ("_,_,_\<turnstile>_\<succ>_\<Colon>\<preceq>_" [71,71,71,71,71,71] 70) where
   103   "G,L,s\<turnstile>t\<succ>v\<Colon>\<preceq>T 
   104     \<equiv> case T of
   105         Inl T  \<Rightarrow> if (\<exists> var. t=In2 var)
   106                   then (\<forall> n. (the_In2 t) = LVar n 
   107                          \<longrightarrow> (fst (the_In2 v) = the (locals s n)) \<and>
   108                              (locals s n \<noteq> None \<longrightarrow> G,s\<turnstile>fst (the_In2 v)\<Colon>\<preceq>T)) \<and>
   109                       (\<not> (\<exists> n. the_In2 t=LVar n) \<longrightarrow> (G,s\<turnstile>fst (the_In2 v)\<Colon>\<preceq>T))\<and>
   110                       (s\<le>|snd (the_In2 v)\<preceq>T\<Colon>\<preceq>(G,L))
   111                   else G,s\<turnstile>the_In1 v\<Colon>\<preceq>T
   112       | Inr Ts \<Rightarrow> list_all2 (conf G s) (the_In3 v) Ts"
   113 
   114 text {*
   115  With @{term rconf} we describe the conformance of the result value of a term.
   116  This definition gets rather complicated because of the relations between the
   117  injections of the different terms, types and values. The main case distinction
   118  is between single values and value lists. In case of value lists, every 
   119  value has to conform to its type. For single values we have to do a further
   120  case distinction, between values of variables @{term "\<exists>var. t=In2 var" } and
   121  ordinary values. Values of variables are modelled as pairs consisting of the
   122  current value and an update function which will perform an assignment to the
   123  variable. This stems form the decision, that we only have one evaluation rule
   124  for each kind of variable. The decision if we read or write to the 
   125  variable is made by syntactic enclosing rules. So conformance of 
   126  variable-values must ensure that both the current value and an update will 
   127  conform to the type. With the introduction of definite assignment of local
   128  variables we have to do another case distinction. For the notion of conformance
   129  local variables are allowed to be @{term None}, since the definedness is not 
   130  ensured by conformance but by definite assignment. Field and array variables 
   131  must contain a value. 
   132 *}
   133  
   134 
   135 
   136 lemma rconf_In1 [simp]: 
   137  "G,L,s\<turnstile>In1 ec\<succ>In1 v \<Colon>\<preceq>Inl T  =  G,s\<turnstile>v\<Colon>\<preceq>T"
   138 apply (unfold rconf_def)
   139 apply (simp (no_asm))
   140 done
   141 
   142 lemma rconf_In2_no_LVar [simp]: 
   143  "\<forall> n. va\<noteq>LVar n \<Longrightarrow> 
   144    G,L,s\<turnstile>In2 va\<succ>In2 vf\<Colon>\<preceq>Inl T  = (G,s\<turnstile>fst vf\<Colon>\<preceq>T \<and> s\<le>|snd vf\<preceq>T\<Colon>\<preceq>(G,L))"
   145 apply (unfold rconf_def)
   146 apply auto
   147 done
   148 
   149 lemma rconf_In2_LVar [simp]: 
   150  "va=LVar n \<Longrightarrow> 
   151    G,L,s\<turnstile>In2 va\<succ>In2 vf\<Colon>\<preceq>Inl T  
   152     = ((fst vf = the (locals s n)) \<and>
   153        (locals s n \<noteq> None \<longrightarrow> G,s\<turnstile>fst vf\<Colon>\<preceq>T) \<and> s\<le>|snd vf\<preceq>T\<Colon>\<preceq>(G,L))"
   154 apply (unfold rconf_def)
   155 by simp
   156 
   157 lemma rconf_In3 [simp]: 
   158  "G,L,s\<turnstile>In3 es\<succ>In3 vs\<Colon>\<preceq>Inr Ts = list_all2 (\<lambda>v T. G,s\<turnstile>v\<Colon>\<preceq>T) vs Ts"
   159 apply (unfold rconf_def)
   160 apply (simp (no_asm))
   161 done
   162 
   163 section "fits and conf"
   164 
   165 (* unused *)
   166 lemma conf_fits: "G,s\<turnstile>v\<Colon>\<preceq>T \<Longrightarrow> G,s\<turnstile>v fits T"
   167 apply (unfold fits_def)
   168 apply clarify
   169 apply (erule contrapos_np, simp (no_asm_use))
   170 apply (drule conf_RefTD)
   171 apply auto
   172 done
   173 
   174 lemma fits_conf: 
   175   "\<lbrakk>G,s\<turnstile>v\<Colon>\<preceq>T; G\<turnstile>T\<preceq>? T'; G,s\<turnstile>v fits T'; ws_prog G\<rbrakk> \<Longrightarrow> G,s\<turnstile>v\<Colon>\<preceq>T'"
   176 apply (auto dest!: fitsD cast_PrimT2 cast_RefT2)
   177 apply (force dest: conf_RefTD intro: conf_AddrI)
   178 done
   179 
   180 lemma fits_Array: 
   181  "\<lbrakk>G,s\<turnstile>v\<Colon>\<preceq>T; G\<turnstile>T'.[]\<preceq>T.[]; G,s\<turnstile>v fits T'; ws_prog G\<rbrakk> \<Longrightarrow> G,s\<turnstile>v\<Colon>\<preceq>T'"
   182 apply (auto dest!: fitsD widen_ArrayPrimT widen_ArrayRefT)
   183 apply (force dest: conf_RefTD intro: conf_AddrI)
   184 done
   185 
   186 
   187 
   188 section "gext"
   189 
   190 lemma halloc_gext: "\<And>s1 s2. G\<turnstile>s1 \<midarrow>halloc oi\<succ>a\<rightarrow> s2 \<Longrightarrow> snd s1\<le>|snd s2"
   191 apply (simp (no_asm_simp) only: split_tupled_all)
   192 apply (erule halloc.induct)
   193 apply  (auto dest!: new_AddrD)
   194 done
   195 
   196 lemma sxalloc_gext: "\<And>s1 s2. G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2 \<Longrightarrow> snd s1\<le>|snd s2"
   197 apply (simp (no_asm_simp) only: split_tupled_all)
   198 apply (erule sxalloc.induct)
   199 apply   (auto dest!: halloc_gext)
   200 done
   201 
   202 lemma eval_gext_lemma [rule_format (no_asm)]: 
   203  "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') \<Longrightarrow> snd s\<le>|snd s' \<and> (case w of  
   204     In1 v \<Rightarrow> True  
   205   | In2 vf \<Rightarrow> normal s \<longrightarrow> (\<forall>v x s. s\<le>|snd (assign (snd vf) v (x,s)))  
   206   | In3 vs \<Rightarrow> True)"
   207 apply (erule eval_induct)
   208 prefer 26 
   209   apply (case_tac "inited C (globs s0)", clarsimp, erule thin_rl) (* Init *)
   210 apply (auto del: conjI  dest!: not_initedD gext_new sxalloc_gext halloc_gext
   211  simp  add: lvar_def fvar_def2 avar_def2 init_lvars_def2 
   212             check_field_access_def check_method_access_def Let_def
   213  split del: split_if_asm split add: sum3.split)
   214 (* 6 subgoals *)
   215 apply force+
   216 done
   217 
   218 lemma evar_gext_f: 
   219   "G\<turnstile>Norm s1 \<midarrow>e=\<succ>vf \<rightarrow> s2 \<Longrightarrow> s\<le>|snd (assign (snd vf) v (x,s))"
   220 apply (drule eval_gext_lemma [THEN conjunct2])
   221 apply auto
   222 done
   223 
   224 lemmas eval_gext = eval_gext_lemma [THEN conjunct1]
   225 
   226 lemma eval_gext': "G\<turnstile>(x1,s1) \<midarrow>t\<succ>\<rightarrow> (w,(x2,s2)) \<Longrightarrow> s1\<le>|s2"
   227 apply (drule eval_gext)
   228 apply auto
   229 done
   230 
   231 lemma init_yields_initd: "G\<turnstile>Norm s1 \<midarrow>Init C\<rightarrow> s2 \<Longrightarrow> initd C s2"
   232 apply (erule eval_cases , auto split del: split_if_asm)
   233 apply (case_tac "inited C (globs s1)")
   234 apply  (clarsimp split del: split_if_asm)+
   235 apply (drule eval_gext')+
   236 apply (drule init_class_obj_inited)
   237 apply (erule inited_gext)
   238 apply (simp (no_asm_use))
   239 done
   240 
   241 
   242 section "Lemmas"
   243 
   244 lemma obj_ty_obj_class1: 
   245  "\<lbrakk>wf_prog G; is_type G (obj_ty obj)\<rbrakk> \<Longrightarrow> is_class G (obj_class obj)"
   246 apply (case_tac "tag obj")
   247 apply (auto simp add: obj_ty_def obj_class_def)
   248 done
   249 
   250 lemma oconf_init_obj: 
   251  "\<lbrakk>wf_prog G;  
   252  (case r of Heap a \<Rightarrow> is_type G (obj_ty obj) | Stat C \<Rightarrow> is_class G C)
   253 \<rbrakk> \<Longrightarrow> G,s\<turnstile>obj \<lparr>values:=init_vals (var_tys G (tag obj) r)\<rparr>\<Colon>\<preceq>\<surd>r"
   254 apply (auto intro!: oconf_init_obj_lemma unique_fields)
   255 done
   256 
   257 lemma conforms_newG: "\<lbrakk>globs s oref = None; (x, s)\<Colon>\<preceq>(G,L);   
   258   wf_prog G; case oref of Heap a \<Rightarrow> is_type G (obj_ty \<lparr>tag=oi,values=vs\<rparr>)  
   259                         | Stat C \<Rightarrow> is_class G C\<rbrakk> \<Longrightarrow>  
   260   (x, init_obj G oi oref s)\<Colon>\<preceq>(G, L)"
   261 apply (unfold init_obj_def)
   262 apply (auto elim!: conforms_gupd dest!: oconf_init_obj 
   263             )
   264 done
   265 
   266 lemma conforms_init_class_obj: 
   267  "\<lbrakk>(x,s)\<Colon>\<preceq>(G, L); wf_prog G; class G C=Some y; \<not> inited C (globs s)\<rbrakk> \<Longrightarrow> 
   268   (x,init_class_obj G C s)\<Colon>\<preceq>(G, L)"
   269 apply (rule not_initedD [THEN conforms_newG])
   270 apply    (auto)
   271 done
   272 
   273 
   274 lemma fst_init_lvars[simp]: 
   275  "fst (init_lvars G C sig (invmode m e) a' pvs (x,s)) = 
   276   (if is_static m then x else (np a') x)"
   277 apply (simp (no_asm) add: init_lvars_def2)
   278 done
   279 
   280 
   281 lemma halloc_conforms: "\<And>s1. \<lbrakk>G\<turnstile>s1 \<midarrow>halloc oi\<succ>a\<rightarrow> s2; wf_prog G; s1\<Colon>\<preceq>(G, L); 
   282   is_type G (obj_ty \<lparr>tag=oi,values=fs\<rparr>)\<rbrakk> \<Longrightarrow> s2\<Colon>\<preceq>(G, L)"
   283 apply (simp (no_asm_simp) only: split_tupled_all)
   284 apply (case_tac "aa")
   285 apply  (auto elim!: halloc_elim_cases dest!: new_AddrD 
   286        intro!: conforms_newG [THEN conforms_xconf] conf_AddrI)
   287 done
   288 
   289 lemma halloc_type_sound: 
   290 "\<And>s1. \<lbrakk>G\<turnstile>s1 \<midarrow>halloc oi\<succ>a\<rightarrow> (x,s); wf_prog G; s1\<Colon>\<preceq>(G, L);
   291   T = obj_ty \<lparr>tag=oi,values=fs\<rparr>; is_type G T\<rbrakk> \<Longrightarrow>  
   292   (x,s)\<Colon>\<preceq>(G, L) \<and> (x = None \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq>T)"
   293 apply (auto elim!: halloc_conforms)
   294 apply (case_tac "aa")
   295 apply (subst obj_ty_eq)
   296 apply  (auto elim!: halloc_elim_cases dest!: new_AddrD intro!: conf_AddrI)
   297 done
   298 
   299 lemma sxalloc_type_sound: 
   300  "\<And>s1 s2. \<lbrakk>G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2; wf_prog G\<rbrakk> \<Longrightarrow> 
   301   case fst s1 of  
   302     None \<Rightarrow> s2 = s1 
   303   | Some abr \<Rightarrow> (case abr of
   304                    Xcpt x \<Rightarrow> (\<exists>a. fst s2 = Some(Xcpt (Loc a)) \<and> 
   305                                   (\<forall>L. s1\<Colon>\<preceq>(G,L) \<longrightarrow> s2\<Colon>\<preceq>(G,L)))
   306                  | Jump j \<Rightarrow> s2 = s1
   307                  | Error e \<Rightarrow> s2 = s1)"
   308 apply (simp (no_asm_simp) only: split_tupled_all)
   309 apply (erule sxalloc.induct)
   310 apply   auto
   311 apply (rule halloc_conforms [THEN conforms_xconf])
   312 apply     (auto elim!: halloc_elim_cases dest!: new_AddrD intro!: conf_AddrI)
   313 done
   314 
   315 lemma wt_init_comp_ty: 
   316 "is_acc_type G (pid C) T \<Longrightarrow> \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>init_comp_ty T\<Colon>\<surd>"
   317 apply (unfold init_comp_ty_def)
   318 apply (clarsimp simp add: accessible_in_RefT_simp 
   319                           is_acc_type_def is_acc_class_def)
   320 done
   321 
   322 
   323 declare fun_upd_same [simp]
   324 
   325 declare fun_upd_apply [simp del]
   326 
   327 definition DynT_prop :: "[prog,inv_mode,qtname,ref_ty] \<Rightarrow> bool" ("_\<turnstile>_\<rightarrow>_\<preceq>_"[71,71,71,71]70) where
   328   "G\<turnstile>mode\<rightarrow>D\<preceq>t \<equiv> mode = IntVir \<longrightarrow> is_class G D \<and> 
   329                      (if (\<exists>T. t=ArrayT T) then D=Object else G\<turnstile>Class D\<preceq>RefT t)"
   330 
   331 lemma DynT_propI: 
   332  "\<lbrakk>(x,s)\<Colon>\<preceq>(G, L); G,s\<turnstile>a'\<Colon>\<preceq>RefT statT; wf_prog G; mode = IntVir \<longrightarrow> a' \<noteq> Null\<rbrakk> 
   333   \<Longrightarrow>  G\<turnstile>mode\<rightarrow>invocation_class mode s a' statT\<preceq>statT"
   334 proof (unfold DynT_prop_def)
   335   assume state_conform: "(x,s)\<Colon>\<preceq>(G, L)"
   336      and      statT_a': "G,s\<turnstile>a'\<Colon>\<preceq>RefT statT"
   337      and            wf: "wf_prog G"
   338      and          mode: "mode = IntVir \<longrightarrow> a' \<noteq> Null"
   339   let ?invCls = "(invocation_class mode s a' statT)"
   340   let ?IntVir = "mode = IntVir"
   341   let ?Concl  = "\<lambda>invCls. is_class G invCls \<and>
   342                           (if \<exists>T. statT = ArrayT T
   343                                   then invCls = Object
   344                                   else G\<turnstile>Class invCls\<preceq>RefT statT)"
   345   show "?IntVir \<longrightarrow> ?Concl ?invCls"
   346   proof  
   347     assume modeIntVir: ?IntVir 
   348     with mode have not_Null: "a' \<noteq> Null" ..
   349     from statT_a' not_Null state_conform 
   350     obtain a obj 
   351       where obj_props:  "a' = Addr a" "globs s (Inl a) = Some obj"   
   352                         "G\<turnstile>obj_ty obj\<preceq>RefT statT" "is_type G (obj_ty obj)"
   353       by (blast dest: conforms_RefTD)
   354     show "?Concl ?invCls"
   355     proof (cases "tag obj")
   356       case CInst
   357       with modeIntVir obj_props
   358       show ?thesis 
   359         by (auto dest!: widen_Array2 split add: split_if)
   360     next
   361       case Arr
   362       from Arr obtain T where "obj_ty obj = T.[]" by (blast dest: obj_ty_Arr1)
   363       moreover from Arr have "obj_class obj = Object" 
   364         by (blast dest: obj_class_Arr1)
   365       moreover note modeIntVir obj_props wf 
   366       ultimately show ?thesis by (auto dest!: widen_Array )
   367     qed
   368   qed
   369 qed
   370 
   371 lemma invocation_methd:
   372 "\<lbrakk>wf_prog G; statT \<noteq> NullT; 
   373  (\<forall> statC. statT = ClassT statC \<longrightarrow> is_class G statC);
   374  (\<forall>     I. statT = IfaceT I \<longrightarrow> is_iface G I \<and> mode \<noteq> SuperM);
   375  (\<forall>     T. statT = ArrayT T \<longrightarrow> mode \<noteq> SuperM);
   376  G\<turnstile>mode\<rightarrow>invocation_class mode s a' statT\<preceq>statT;  
   377  dynlookup G statT (invocation_class mode s a' statT) sig = Some m \<rbrakk> 
   378 \<Longrightarrow> methd G (invocation_declclass G mode s a' statT sig) sig = Some m"
   379 proof -
   380   assume         wf: "wf_prog G"
   381      and  not_NullT: "statT \<noteq> NullT"
   382      and statC_prop: "(\<forall> statC. statT = ClassT statC \<longrightarrow> is_class G statC)"
   383      and statI_prop: "(\<forall> I. statT = IfaceT I \<longrightarrow> is_iface G I \<and> mode \<noteq> SuperM)"
   384      and statA_prop: "(\<forall>     T. statT = ArrayT T \<longrightarrow> mode \<noteq> SuperM)"
   385      and  invC_prop: "G\<turnstile>mode\<rightarrow>invocation_class mode s a' statT\<preceq>statT"
   386      and  dynlookup: "dynlookup G statT (invocation_class mode s a' statT) sig 
   387                       = Some m"
   388   show ?thesis
   389   proof (cases statT)
   390     case NullT
   391     with not_NullT show ?thesis by simp
   392   next
   393     case IfaceT
   394     with statI_prop obtain I 
   395       where    statI: "statT = IfaceT I" and 
   396             is_iface: "is_iface G I"     and
   397           not_SuperM: "mode \<noteq> SuperM" by blast            
   398     
   399     show ?thesis 
   400     proof (cases mode)
   401       case Static
   402       with wf dynlookup statI is_iface 
   403       show ?thesis
   404         by (auto simp add: invocation_declclass_def dynlookup_def 
   405                            dynimethd_def dynmethd_C_C 
   406                     intro: dynmethd_declclass
   407                     dest!: wf_imethdsD
   408                      dest: table_of_map_SomeI
   409                     split: split_if_asm)
   410     next        
   411       case SuperM
   412       with not_SuperM show ?thesis ..
   413     next
   414       case IntVir
   415       with wf dynlookup IfaceT invC_prop show ?thesis 
   416         by (auto simp add: invocation_declclass_def dynlookup_def dynimethd_def
   417                            DynT_prop_def
   418                     intro: methd_declclass dynmethd_declclass
   419                     split: split_if_asm)
   420     qed
   421   next
   422     case ClassT
   423     show ?thesis
   424     proof (cases mode)
   425       case Static
   426       with wf ClassT dynlookup statC_prop 
   427       show ?thesis by (auto simp add: invocation_declclass_def dynlookup_def
   428                                intro: dynmethd_declclass)
   429     next
   430       case SuperM
   431       with wf ClassT dynlookup statC_prop 
   432       show ?thesis by (auto simp add: invocation_declclass_def dynlookup_def
   433                                intro: dynmethd_declclass)
   434     next
   435       case IntVir
   436       with wf ClassT dynlookup statC_prop invC_prop 
   437       show ?thesis
   438         by (auto simp add: invocation_declclass_def dynlookup_def dynimethd_def
   439                            DynT_prop_def
   440                     intro: dynmethd_declclass)
   441     qed
   442   next
   443     case ArrayT
   444     show ?thesis
   445     proof (cases mode)
   446       case Static
   447       with wf ArrayT dynlookup show ?thesis
   448         by (auto simp add: invocation_declclass_def dynlookup_def 
   449                            dynimethd_def dynmethd_C_C
   450                     intro: dynmethd_declclass
   451                      dest: table_of_map_SomeI)
   452     next
   453       case SuperM
   454       with ArrayT statA_prop show ?thesis by blast
   455     next
   456       case IntVir
   457       with wf ArrayT dynlookup invC_prop show ?thesis
   458         by (auto simp add: invocation_declclass_def dynlookup_def dynimethd_def
   459                            DynT_prop_def dynmethd_C_C
   460                     intro: dynmethd_declclass
   461                      dest: table_of_map_SomeI)
   462     qed
   463   qed
   464 qed
   465 
   466 lemma DynT_mheadsD: 
   467 "\<lbrakk>G\<turnstile>invmode sm e\<rightarrow>invC\<preceq>statT; 
   468   wf_prog G; \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT; 
   469   (statDeclT,sm) \<in> mheads G C statT sig; 
   470   invC = invocation_class (invmode sm e) s a' statT;
   471   declC =invocation_declclass G (invmode sm e) s a' statT sig
   472  \<rbrakk> \<Longrightarrow> 
   473   \<exists> dm. 
   474   methd G declC sig = Some dm \<and> dynlookup G statT invC sig = Some dm  \<and> 
   475   G\<turnstile>resTy (mthd dm)\<preceq>resTy sm \<and> 
   476   wf_mdecl G declC (sig, mthd dm) \<and>
   477   declC = declclass dm \<and>
   478   is_static dm = is_static sm \<and>  
   479   is_class G invC \<and> is_class G declC  \<and> G\<turnstile>invC\<preceq>\<^sub>C declC \<and>  
   480   (if invmode sm e = IntVir
   481       then (\<forall> statC. statT=ClassT statC \<longrightarrow> G\<turnstile>invC \<preceq>\<^sub>C statC)
   482       else (  (\<exists> statC. statT=ClassT statC \<and> G\<turnstile>statC\<preceq>\<^sub>C declC)
   483             \<or> (\<forall> statC. statT\<noteq>ClassT statC \<and> declC=Object)) \<and> 
   484             statDeclT = ClassT (declclass dm))"
   485 proof -
   486   assume invC_prop: "G\<turnstile>invmode sm e\<rightarrow>invC\<preceq>statT" 
   487      and        wf: "wf_prog G" 
   488      and      wt_e: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT"
   489      and        sm: "(statDeclT,sm) \<in> mheads G C statT sig" 
   490      and      invC: "invC = invocation_class (invmode sm e) s a' statT"
   491      and     declC: "declC = 
   492                     invocation_declclass G (invmode sm e) s a' statT sig"
   493   from wt_e wf have type_statT: "is_type G (RefT statT)"
   494     by (auto dest: ty_expr_is_type)
   495   from sm have not_Null: "statT \<noteq> NullT" by auto
   496   from type_statT 
   497   have wf_C: "(\<forall> statC. statT = ClassT statC \<longrightarrow> is_class G statC)"
   498     by (auto)
   499   from type_statT wt_e 
   500   have wf_I: "(\<forall>I. statT = IfaceT I \<longrightarrow> is_iface G I \<and> 
   501                                         invmode sm e \<noteq> SuperM)"
   502     by (auto dest: invocationTypeExpr_noClassD)
   503   from wt_e
   504   have wf_A: "(\<forall>     T. statT = ArrayT T \<longrightarrow> invmode sm e \<noteq> SuperM)"
   505     by (auto dest: invocationTypeExpr_noClassD)
   506   show ?thesis
   507   proof (cases "invmode sm e = IntVir")
   508     case True
   509     with invC_prop not_Null
   510     have invC_prop': " is_class G invC \<and> 
   511                       (if (\<exists>T. statT=ArrayT T) then invC=Object 
   512                                               else G\<turnstile>Class invC\<preceq>RefT statT)"
   513       by (auto simp add: DynT_prop_def) 
   514     from True 
   515     have "\<not> is_static sm"
   516       by (simp add: invmode_IntVir_eq member_is_static_simp)
   517     with invC_prop' not_Null
   518     have "G,statT \<turnstile> invC valid_lookup_cls_for (is_static sm)"
   519       by (cases statT) auto
   520     with sm wf type_statT obtain dm where
   521            dm: "dynlookup G statT invC sig = Some dm" and
   522       resT_dm: "G\<turnstile>resTy (mthd dm)\<preceq>resTy sm"      and
   523        static: "is_static dm = is_static sm"
   524       by  - (drule dynamic_mheadsD,force+)
   525     with declC invC not_Null 
   526     have declC': "declC = (declclass dm)" 
   527       by (auto simp add: invocation_declclass_def)
   528     with wf invC declC not_Null wf_C wf_I wf_A invC_prop dm 
   529     have dm': "methd G declC sig = Some dm"
   530       by - (drule invocation_methd,auto)
   531     from wf dm invC_prop' declC' type_statT 
   532     have declC_prop: "G\<turnstile>invC \<preceq>\<^sub>C declC \<and> is_class G declC"
   533       by (auto dest: dynlookup_declC)
   534     from wf dm' declC_prop declC' 
   535     have wf_dm: "wf_mdecl G declC (sig,(mthd dm))"
   536       by (auto dest: methd_wf_mdecl)
   537     from invC_prop' 
   538     have statC_prop: "(\<forall> statC. statT=ClassT statC \<longrightarrow> G\<turnstile>invC \<preceq>\<^sub>C statC)"
   539       by auto
   540     from True dm' resT_dm wf_dm invC_prop' declC_prop statC_prop declC' static
   541          dm
   542     show ?thesis by auto
   543   next
   544     case False
   545     with type_statT wf invC not_Null wf_I wf_A
   546     have invC_prop': "is_class G invC \<and>  
   547                      ((\<exists> statC. statT=ClassT statC \<and> invC=statC) \<or>
   548                       (\<forall> statC. statT\<noteq>ClassT statC \<and> invC=Object))"
   549         by (case_tac "statT") (auto simp add: invocation_class_def 
   550                                        split: inv_mode.splits)
   551     with not_Null wf
   552     have dynlookup_static: "dynlookup G statT invC sig = methd G invC sig"
   553       by (case_tac "statT") (auto simp add: dynlookup_def dynmethd_C_C
   554                                             dynimethd_def)
   555     from sm wf wt_e not_Null False invC_prop' obtain "dm" where
   556                     dm: "methd G invC sig = Some dm"          and
   557         eq_declC_sm_dm:"statDeclT = ClassT (declclass dm)"  and
   558              eq_mheads:"sm=mhead (mthd dm) "
   559       by - (drule static_mheadsD, (force dest: accmethd_SomeD)+)
   560     then have static: "is_static dm = is_static sm" by - (auto)
   561     with declC invC dynlookup_static dm
   562     have declC': "declC = (declclass dm)"  
   563       by (auto simp add: invocation_declclass_def)
   564     from invC_prop' wf declC' dm 
   565     have dm': "methd G declC sig = Some dm"
   566       by (auto intro: methd_declclass)
   567     from dynlookup_static dm 
   568     have dm'': "dynlookup G statT invC sig = Some dm"
   569       by simp
   570     from wf dm invC_prop' declC' type_statT 
   571     have declC_prop: "G\<turnstile>invC \<preceq>\<^sub>C declC \<and> is_class G declC"
   572       by (auto dest: methd_declC )
   573     then have declC_prop1: "invC=Object \<longrightarrow> declC=Object"  by auto
   574     from wf dm' declC_prop declC' 
   575     have wf_dm: "wf_mdecl G declC (sig,(mthd dm))"
   576       by (auto dest: methd_wf_mdecl)
   577     from invC_prop' declC_prop declC_prop1
   578     have statC_prop: "(   (\<exists> statC. statT=ClassT statC \<and> G\<turnstile>statC\<preceq>\<^sub>C declC)
   579                        \<or>  (\<forall> statC. statT\<noteq>ClassT statC \<and> declC=Object))" 
   580       by auto
   581     from False dm' dm'' wf_dm invC_prop' declC_prop statC_prop declC' 
   582          eq_declC_sm_dm eq_mheads static
   583     show ?thesis by auto
   584   qed
   585 qed
   586 
   587 corollary DynT_mheadsE [consumes 7]: 
   588 --{* Same as @{text DynT_mheadsD} but better suited for application in 
   589 typesafety proof   *}
   590  assumes invC_compatible: "G\<turnstile>mode\<rightarrow>invC\<preceq>statT" 
   591      and wf: "wf_prog G" 
   592      and wt_e: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT"
   593      and mheads: "(statDeclT,sm) \<in> mheads G C statT sig"
   594      and mode: "mode=invmode sm e" 
   595      and invC: "invC = invocation_class mode s a' statT"
   596      and declC: "declC =invocation_declclass G mode s a' statT sig"
   597      and dm: "\<And> dm. \<lbrakk>methd G declC sig = Some dm; 
   598                       dynlookup G statT invC sig = Some dm; 
   599                       G\<turnstile>resTy (mthd dm)\<preceq>resTy sm; 
   600                       wf_mdecl G declC (sig, mthd dm);
   601                       declC = declclass dm;
   602                       is_static dm = is_static sm;  
   603                       is_class G invC; is_class G declC; G\<turnstile>invC\<preceq>\<^sub>C declC;  
   604                       (if invmode sm e = IntVir
   605                       then (\<forall> statC. statT=ClassT statC \<longrightarrow> G\<turnstile>invC \<preceq>\<^sub>C statC)
   606                       else (  (\<exists> statC. statT=ClassT statC \<and> G\<turnstile>statC\<preceq>\<^sub>C declC)
   607                              \<or> (\<forall> statC. statT\<noteq>ClassT statC \<and> declC=Object)) \<and>
   608                              statDeclT = ClassT (declclass dm))\<rbrakk> \<Longrightarrow> P"
   609    shows "P"
   610 proof -
   611     from invC_compatible mode have "G\<turnstile>invmode sm e\<rightarrow>invC\<preceq>statT" by simp 
   612     moreover note wf wt_e mheads
   613     moreover from invC mode 
   614     have "invC = invocation_class (invmode sm e) s a' statT" by simp
   615     moreover from declC mode 
   616     have "declC =invocation_declclass G (invmode sm e) s a' statT sig" by simp
   617     ultimately show ?thesis
   618       by (rule DynT_mheadsD [THEN exE,rule_format])
   619          (elim conjE,rule dm)
   620 qed
   621    
   622 
   623 lemma DynT_conf: "\<lbrakk>G\<turnstile>invocation_class mode s a' statT \<preceq>\<^sub>C declC; wf_prog G;
   624  isrtype G (statT);
   625  G,s\<turnstile>a'\<Colon>\<preceq>RefT statT; mode = IntVir \<longrightarrow> a' \<noteq> Null;  
   626   mode \<noteq> IntVir \<longrightarrow>    (\<exists> statC. statT=ClassT statC \<and> G\<turnstile>statC\<preceq>\<^sub>C declC)
   627                     \<or>  (\<forall> statC. statT\<noteq>ClassT statC \<and> declC=Object)\<rbrakk> 
   628  \<Longrightarrow>G,s\<turnstile>a'\<Colon>\<preceq> Class declC"
   629 apply (case_tac "mode = IntVir")
   630 apply (drule conf_RefTD)
   631 apply (force intro!: conf_AddrI 
   632             simp add: obj_class_def split add: obj_tag.split_asm)
   633 apply  clarsimp
   634 apply  safe
   635 apply    (erule (1) widen.subcls [THEN conf_widen])
   636 apply    (erule wf_ws_prog)
   637 
   638 apply    (frule widen_Object) apply (erule wf_ws_prog)
   639 apply    (erule (1) conf_widen) apply (erule wf_ws_prog)
   640 done
   641 
   642 lemma Ass_lemma:
   643 "\<lbrakk> G\<turnstile>Norm s0 \<midarrow>var=\<succ>(w, f)\<rightarrow> Norm s1; G\<turnstile>Norm s1 \<midarrow>e-\<succ>v\<rightarrow> Norm s2;
   644    G,s2\<turnstile>v\<Colon>\<preceq>eT;s1\<le>|s2 \<longrightarrow> assign f v (Norm s2)\<Colon>\<preceq>(G, L)\<rbrakk>
   645 \<Longrightarrow> assign f v (Norm s2)\<Colon>\<preceq>(G, L) \<and>
   646       (normal (assign f v (Norm s2)) \<longrightarrow> G,store (assign f v (Norm s2))\<turnstile>v\<Colon>\<preceq>eT)"
   647 apply (drule_tac x = "None" and s = "s2" and v = "v" in evar_gext_f)
   648 apply (drule eval_gext', clarsimp)
   649 apply (erule conf_gext)
   650 apply simp
   651 done
   652 
   653 lemma Throw_lemma: "\<lbrakk>G\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable; wf_prog G; (x1,s1)\<Colon>\<preceq>(G, L);  
   654     x1 = None \<longrightarrow> G,s1\<turnstile>a'\<Colon>\<preceq> Class tn\<rbrakk> \<Longrightarrow> (throw a' x1, s1)\<Colon>\<preceq>(G, L)"
   655 apply (auto split add: split_abrupt_if simp add: throw_def2)
   656 apply (erule conforms_xconf)
   657 apply (frule conf_RefTD)
   658 apply (auto elim: widen.subcls [THEN conf_widen])
   659 done
   660 
   661 lemma Try_lemma: "\<lbrakk>G\<turnstile>obj_ty (the (globs s1' (Heap a)))\<preceq> Class tn; 
   662  (Some (Xcpt (Loc a)), s1')\<Colon>\<preceq>(G, L); wf_prog G\<rbrakk> 
   663  \<Longrightarrow> Norm (lupd(vn\<mapsto>Addr a) s1')\<Colon>\<preceq>(G, L(vn\<mapsto>Class tn))"
   664 apply (rule conforms_allocL)
   665 apply  (erule conforms_NormI)
   666 apply (drule conforms_XcptLocD [THEN conf_RefTD],rule HOL.refl)
   667 apply (auto intro!: conf_AddrI)
   668 done
   669 
   670 lemma Fin_lemma: 
   671 "\<lbrakk>G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> (x2,s2); wf_prog G; (Some a, s1)\<Colon>\<preceq>(G, L); (x2,s2)\<Colon>\<preceq>(G, L);
   672   dom (locals s1) \<subseteq> dom (locals s2)\<rbrakk> 
   673 \<Longrightarrow>  (abrupt_if True (Some a) x2, s2)\<Colon>\<preceq>(G, L)"
   674 apply (auto elim: eval_gext' conforms_xgext split add: split_abrupt_if)
   675 done
   676 
   677 lemma FVar_lemma1: 
   678 "\<lbrakk>table_of (DeclConcepts.fields G statC) (fn, statDeclC) = Some f ; 
   679   x2 = None \<longrightarrow> G,s2\<turnstile>a\<Colon>\<preceq> Class statC; wf_prog G; G\<turnstile>statC\<preceq>\<^sub>C statDeclC; 
   680   statDeclC \<noteq> Object; 
   681   class G statDeclC = Some y; (x2,s2)\<Colon>\<preceq>(G, L); s1\<le>|s2; 
   682   inited statDeclC (globs s1); 
   683   (if static f then id else np a) x2 = None\<rbrakk> 
   684  \<Longrightarrow>  
   685   \<exists>obj. globs s2 (if static f then Inr statDeclC else Inl (the_Addr a)) 
   686                   = Some obj \<and> 
   687   var_tys G (tag obj)  (if static f then Inr statDeclC else Inl(the_Addr a)) 
   688           (Inl(fn,statDeclC)) = Some (type f)"
   689 apply (drule initedD)
   690 apply (frule subcls_is_class2, simp (no_asm_simp))
   691 apply (case_tac "static f")
   692 apply  clarsimp
   693 apply  (drule (1) rev_gext_objD, clarsimp)
   694 apply  (frule fields_declC, erule wf_ws_prog, simp (no_asm_simp))
   695 apply  (rule var_tys_Some_eq [THEN iffD2])
   696 apply  clarsimp
   697 apply  (erule fields_table_SomeI, simp (no_asm))
   698 apply clarsimp
   699 apply (drule conf_RefTD, clarsimp, rule var_tys_Some_eq [THEN iffD2])
   700 apply (auto dest!: widen_Array split add: obj_tag.split)
   701 apply (rule fields_table_SomeI)
   702 apply (auto elim!: fields_mono subcls_is_class2)
   703 done
   704 
   705 lemma FVar_lemma2: "error_free state
   706        \<Longrightarrow> error_free
   707            (assign
   708              (\<lambda>v. supd
   709                    (upd_gobj
   710                      (if static field then Inr statDeclC
   711                       else Inl (the_Addr a))
   712                      (Inl (fn, statDeclC)) v))
   713              w state)"
   714 proof -
   715   assume error_free: "error_free state"
   716   obtain a s where "state=(a,s)"
   717     by (cases state)
   718   with error_free
   719   show ?thesis
   720     by (cases a) auto
   721 qed
   722 
   723 declare split_paired_All [simp del] split_paired_Ex [simp del] 
   724 declare split_if     [split del] split_if_asm     [split del] 
   725         option.split [split del] option.split_asm [split del]
   726 declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
   727 declaration {* K (Classical.map_cs (fn cs => cs delSWrapper "split_all_tac")) *}
   728 
   729 lemma FVar_lemma: 
   730 "\<lbrakk>((v, f), Norm s2') = fvar statDeclC (static field) fn a (x2, s2); 
   731   G\<turnstile>statC\<preceq>\<^sub>C statDeclC;  
   732   table_of (DeclConcepts.fields G statC) (fn, statDeclC) = Some field; 
   733   wf_prog G;   
   734   x2 = None \<longrightarrow> G,s2\<turnstile>a\<Colon>\<preceq>Class statC; 
   735   statDeclC \<noteq> Object; class G statDeclC = Some y;   
   736   (x2, s2)\<Colon>\<preceq>(G, L); s1\<le>|s2; inited statDeclC (globs s1)\<rbrakk> \<Longrightarrow>  
   737   G,s2'\<turnstile>v\<Colon>\<preceq>type field \<and> s2'\<le>|f\<preceq>type field\<Colon>\<preceq>(G, L)"
   738 apply (unfold assign_conforms_def)
   739 apply (drule sym)
   740 apply (clarsimp simp add: fvar_def2)
   741 apply (drule (9) FVar_lemma1)
   742 apply (clarsimp)
   743 apply (drule (2) conforms_globsD [THEN oconf_lconf, THEN lconfD])
   744 apply clarsimp
   745 apply (rule conjI)
   746 apply   clarsimp
   747 apply   (drule (1) rev_gext_objD)
   748 apply   (force elim!: conforms_upd_gobj)
   749 
   750 apply   (blast intro: FVar_lemma2)
   751 done
   752 declare split_paired_All [simp] split_paired_Ex [simp] 
   753 declare split_if     [split] split_if_asm     [split] 
   754         option.split [split] option.split_asm [split]
   755 declaration {* K (Classical.map_cs (fn cs => cs addSbefore ("split_all_tac", split_all_tac))) *}
   756 declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
   757 
   758 
   759 lemma AVar_lemma1: "\<lbrakk>globs s (Inl a) = Some obj;tag obj=Arr ty i; 
   760  the_Intg i' in_bounds i; wf_prog G; G\<turnstile>ty.[]\<preceq>Tb.[]; Norm s\<Colon>\<preceq>(G, L)
   761 \<rbrakk> \<Longrightarrow> G,s\<turnstile>the ((values obj) (Inr (the_Intg i')))\<Colon>\<preceq>Tb"
   762 apply (erule widen_Array_Array [THEN conf_widen])
   763 apply  (erule_tac [2] wf_ws_prog)
   764 apply (drule (1) conforms_globsD [THEN oconf_lconf, THEN lconfD])
   765 defer apply assumption
   766 apply (force intro: var_tys_Some_eq [THEN iffD2])
   767 done
   768 
   769 lemma obj_split: "\<exists> t vs. obj = \<lparr>tag=t,values=vs\<rparr>"
   770   by (cases obj) auto
   771  
   772 lemma AVar_lemma2: "error_free state 
   773        \<Longrightarrow> error_free
   774            (assign
   775              (\<lambda>v (x, s').
   776                  ((raise_if (\<not> G,s'\<turnstile>v fits T) ArrStore) x,
   777                   upd_gobj (Inl a) (Inr (the_Intg i)) v s'))
   778              w state)"
   779 proof -
   780   assume error_free: "error_free state"
   781   obtain a s where "state=(a,s)"
   782     by (cases state)
   783   with error_free
   784   show ?thesis
   785     by (cases a) auto
   786 qed
   787 
   788 lemma AVar_lemma: "\<lbrakk>wf_prog G; G\<turnstile>(x1, s1) \<midarrow>e2-\<succ>i\<rightarrow> (x2, s2);  
   789   ((v,f), Norm s2') = avar G i a (x2, s2); x1 = None \<longrightarrow> G,s1\<turnstile>a\<Colon>\<preceq>Ta.[];  
   790   (x2, s2)\<Colon>\<preceq>(G, L); s1\<le>|s2\<rbrakk> \<Longrightarrow> G,s2'\<turnstile>v\<Colon>\<preceq>Ta \<and> s2'\<le>|f\<preceq>Ta\<Colon>\<preceq>(G, L)"
   791 apply (unfold assign_conforms_def)
   792 apply (drule sym)
   793 apply (clarsimp simp add: avar_def2)
   794 apply (drule (1) conf_gext)
   795 apply (drule conf_RefTD, clarsimp)
   796 apply (subgoal_tac "\<exists> t vs. obj = \<lparr>tag=t,values=vs\<rparr>")
   797 defer
   798 apply   (rule obj_split)
   799 apply clarify
   800 apply (frule obj_ty_widenD)
   801 apply (auto dest!: widen_Class)
   802 apply   (force dest: AVar_lemma1)
   803 
   804 apply   (force elim!: fits_Array dest: gext_objD 
   805          intro: var_tys_Some_eq [THEN iffD2] conforms_upd_gobj)
   806 done
   807 
   808 
   809 section "Call"
   810 
   811 lemma conforms_init_lvars_lemma: "\<lbrakk>wf_prog G;  
   812   wf_mhead G P sig mh;
   813   list_all2 (conf G s) pvs pTsa; G\<turnstile>pTsa[\<preceq>](parTs sig)\<rbrakk> \<Longrightarrow>  
   814   G,s\<turnstile>empty (pars mh[\<mapsto>]pvs)
   815       [\<sim>\<Colon>\<preceq>]table_of lvars(pars mh[\<mapsto>]parTs sig)"
   816 apply (unfold wf_mhead_def)
   817 apply clarify
   818 apply (erule (1) wlconf_empty_vals [THEN wlconf_ext_list])
   819 apply (drule wf_ws_prog)
   820 apply (erule (2) conf_list_widen)
   821 done
   822 
   823 
   824 lemma lconf_map_lname [simp]: 
   825   "G,s\<turnstile>(lname_case l1 l2)[\<Colon>\<preceq>](lname_case L1 L2)
   826    =
   827   (G,s\<turnstile>l1[\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>(\<lambda>x::unit . l2)[\<Colon>\<preceq>](\<lambda>x::unit. L2))"
   828 apply (unfold lconf_def)
   829 apply (auto split add: lname.splits)
   830 done
   831 
   832 lemma wlconf_map_lname [simp]: 
   833   "G,s\<turnstile>(lname_case l1 l2)[\<sim>\<Colon>\<preceq>](lname_case L1 L2)
   834    =
   835   (G,s\<turnstile>l1[\<sim>\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>(\<lambda>x::unit . l2)[\<sim>\<Colon>\<preceq>](\<lambda>x::unit. L2))"
   836 apply (unfold wlconf_def)
   837 apply (auto split add: lname.splits)
   838 done
   839 
   840 lemma lconf_map_ename [simp]:
   841   "G,s\<turnstile>(ename_case l1 l2)[\<Colon>\<preceq>](ename_case L1 L2)
   842    =
   843   (G,s\<turnstile>l1[\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>(\<lambda>x::unit. l2)[\<Colon>\<preceq>](\<lambda>x::unit. L2))"
   844 apply (unfold lconf_def)
   845 apply (auto split add: ename.splits)
   846 done
   847 
   848 lemma wlconf_map_ename [simp]:
   849   "G,s\<turnstile>(ename_case l1 l2)[\<sim>\<Colon>\<preceq>](ename_case L1 L2)
   850    =
   851   (G,s\<turnstile>l1[\<sim>\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>(\<lambda>x::unit. l2)[\<sim>\<Colon>\<preceq>](\<lambda>x::unit. L2))"
   852 apply (unfold wlconf_def)
   853 apply (auto split add: ename.splits)
   854 done
   855 
   856 
   857 
   858 lemma defval_conf1 [rule_format (no_asm), elim]: 
   859   "is_type G T \<longrightarrow> (\<exists>v\<in>Some (default_val T): G,s\<turnstile>v\<Colon>\<preceq>T)"
   860 apply (unfold conf_def)
   861 apply (induct "T")
   862 apply (auto intro: prim_ty.induct)
   863 done
   864 
   865 lemma np_no_jump: "x\<noteq>Some (Jump j) \<Longrightarrow> (np a') x \<noteq> Some (Jump j)"
   866 by (auto simp add: abrupt_if_def)
   867 
   868 declare split_paired_All [simp del] split_paired_Ex [simp del] 
   869 declare split_if     [split del] split_if_asm     [split del] 
   870         option.split [split del] option.split_asm [split del]
   871 declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
   872 declaration {* K (Classical.map_cs (fn cs => cs delSWrapper "split_all_tac")) *}
   873 
   874 lemma conforms_init_lvars: 
   875 "\<lbrakk>wf_mhead G (pid declC) sig (mhead (mthd dm)); wf_prog G;  
   876   list_all2 (conf G s) pvs pTsa; G\<turnstile>pTsa[\<preceq>](parTs sig);  
   877   (x, s)\<Colon>\<preceq>(G, L); 
   878   methd G declC sig = Some dm;  
   879   isrtype G statT;
   880   G\<turnstile>invC\<preceq>\<^sub>C declC; 
   881   G,s\<turnstile>a'\<Colon>\<preceq>RefT statT;  
   882   invmode (mhd sm) e = IntVir \<longrightarrow> a' \<noteq> Null; 
   883   invmode (mhd sm) e \<noteq> IntVir \<longrightarrow>  
   884        (\<exists> statC. statT=ClassT statC \<and> G\<turnstile>statC\<preceq>\<^sub>C declC)
   885     \<or>  (\<forall> statC. statT\<noteq>ClassT statC \<and> declC=Object);
   886   invC  = invocation_class (invmode (mhd sm) e) s a' statT;
   887   declC = invocation_declclass G (invmode (mhd sm) e) s a' statT sig;
   888   x\<noteq>Some (Jump Ret) 
   889  \<rbrakk> \<Longrightarrow>  
   890   init_lvars G declC sig (invmode (mhd sm) e) a'  
   891   pvs (x,s)\<Colon>\<preceq>(G,\<lambda> k. 
   892                 (case k of
   893                    EName e \<Rightarrow> (case e of 
   894                                  VNam v 
   895                                   \<Rightarrow> (table_of (lcls (mbody (mthd dm)))
   896                                         (pars (mthd dm)[\<mapsto>]parTs sig)) v
   897                                | Res \<Rightarrow> Some (resTy (mthd dm)))
   898                  | This \<Rightarrow> if (is_static (mthd sm)) 
   899                               then None else Some (Class declC)))"
   900 apply (simp add: init_lvars_def2)
   901 apply (rule conforms_set_locals)
   902 apply  (simp (no_asm_simp) split add: split_if)
   903 apply (drule  (4) DynT_conf)
   904 apply clarsimp
   905 (* apply intro *)
   906 apply (drule (3) conforms_init_lvars_lemma 
   907                  [where ?lvars="(lcls (mbody (mthd dm)))"])
   908 apply (case_tac "dm",simp)
   909 apply (rule conjI)
   910 apply (unfold wlconf_def, clarify)
   911 apply   (clarsimp simp add: wf_mhead_def is_acc_type_def)
   912 apply   (case_tac "is_static sm")
   913 apply     simp
   914 apply     simp
   915 
   916 apply   simp
   917 apply   (case_tac "is_static sm")
   918 apply     simp
   919 apply     (simp add: np_no_jump)
   920 done
   921 declare split_paired_All [simp] split_paired_Ex [simp] 
   922 declare split_if     [split] split_if_asm     [split] 
   923         option.split [split] option.split_asm [split]
   924 declaration {* K (Classical.map_cs (fn cs => cs addSbefore ("split_all_tac", split_all_tac))) *}
   925 declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
   926 
   927 
   928 subsection "accessibility"
   929 
   930 theorem dynamic_field_access_ok:
   931   assumes wf: "wf_prog G" and
   932     not_Null: "\<not> stat \<longrightarrow> a\<noteq>Null" and
   933    conform_a: "G,(store s)\<turnstile>a\<Colon>\<preceq> Class statC" and
   934    conform_s: "s\<Colon>\<preceq>(G, L)" and 
   935     normal_s: "normal s" and
   936         wt_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e\<Colon>-Class statC" and
   937            f: "accfield G accC statC fn = Some f" and
   938         dynC: "if stat then dynC=declclass f  
   939                        else dynC=obj_class (lookup_obj (store s) a)" and
   940         stat: "if stat then (is_static f) else (\<not> is_static f)"
   941   shows "table_of (DeclConcepts.fields G dynC) (fn,declclass f) = Some (fld f)\<and>
   942          G\<turnstile>Field fn f in dynC dyn_accessible_from accC"
   943 proof (cases "stat")
   944   case True
   945   with stat have static: "(is_static f)" by simp
   946   from True dynC 
   947   have dynC': "dynC=declclass f" by simp
   948   with f
   949   have "table_of (DeclConcepts.fields G statC) (fn,declclass f) = Some (fld f)"
   950     by (auto simp add: accfield_def Let_def intro!: table_of_remap_SomeD)
   951   moreover
   952   from wt_e wf have "is_class G statC"
   953     by (auto dest!: ty_expr_is_type)
   954   moreover note wf dynC'
   955   ultimately have
   956      "table_of (DeclConcepts.fields G dynC) (fn,declclass f) = Some (fld f)"
   957     by (auto dest: fields_declC)
   958   with dynC' f static wf
   959   show ?thesis
   960     by (auto dest: static_to_dynamic_accessible_from_static
   961             dest!: accfield_accessibleD )
   962 next
   963   case False
   964   with wf conform_a not_Null conform_s dynC
   965   obtain subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and
   966     "is_class G dynC"
   967     by (auto dest!: conforms_RefTD [of _ _ _ _ "(fst s)" L]
   968               dest: obj_ty_obj_class1
   969           simp add: obj_ty_obj_class )
   970   with wf f
   971   have "table_of (DeclConcepts.fields G dynC) (fn,declclass f) = Some (fld f)"
   972     by (auto simp add: accfield_def Let_def
   973                  dest: fields_mono
   974                 dest!: table_of_remap_SomeD)
   975   moreover
   976   from f subclseq
   977   have "G\<turnstile>Field fn f in dynC dyn_accessible_from accC"
   978     by (auto intro!: static_to_dynamic_accessible_from wf
   979                dest: accfield_accessibleD)
   980   ultimately show ?thesis
   981     by blast
   982 qed
   983 
   984 lemma error_free_field_access:
   985   assumes accfield: "accfield G accC statC fn = Some (statDeclC, f)" and
   986               wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-Class statC" and
   987          eval_init: "G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<rightarrow> s1" and
   988             eval_e: "G\<turnstile>s1 \<midarrow>e-\<succ>a\<rightarrow> s2" and
   989            conf_s2: "s2\<Colon>\<preceq>(G, L)" and
   990             conf_a: "normal s2 \<Longrightarrow> G, store s2\<turnstile>a\<Colon>\<preceq>Class statC" and
   991               fvar: "(v,s2')=fvar statDeclC (is_static f) fn a s2" and
   992                 wf: "wf_prog G"   
   993   shows "check_field_access G accC statDeclC fn (is_static f) a s2' = s2'"
   994 proof -
   995   from fvar
   996   have store_s2': "store s2'=store s2"
   997     by (cases s2) (simp add: fvar_def2)
   998   with fvar conf_s2 
   999   have conf_s2': "s2'\<Colon>\<preceq>(G, L)"
  1000     by (cases s2,cases "is_static f") (auto simp add: fvar_def2)
  1001   from eval_init 
  1002   have initd_statDeclC_s1: "initd statDeclC s1"
  1003     by (rule init_yields_initd)
  1004   with eval_e store_s2'
  1005   have initd_statDeclC_s2': "initd statDeclC s2'"
  1006     by (auto dest: eval_gext intro: inited_gext)
  1007   show ?thesis
  1008   proof (cases "normal s2'")
  1009     case False
  1010     then show ?thesis 
  1011       by (auto simp add: check_field_access_def Let_def)
  1012   next
  1013     case True
  1014     with fvar store_s2' 
  1015     have not_Null: "\<not> (is_static f) \<longrightarrow> a\<noteq>Null" 
  1016       by (cases s2) (auto simp add: fvar_def2)
  1017     from True fvar store_s2'
  1018     have "normal s2"
  1019       by (cases s2,cases "is_static f") (auto simp add: fvar_def2)
  1020     with conf_a store_s2'
  1021     have conf_a': "G,store s2'\<turnstile>a\<Colon>\<preceq>Class statC"
  1022       by simp
  1023     from conf_a' conf_s2' True initd_statDeclC_s2' 
  1024       dynamic_field_access_ok [OF wf not_Null conf_a' conf_s2' 
  1025                                    True wt_e accfield ] 
  1026     show ?thesis
  1027       by  (cases "is_static f")
  1028           (auto dest!: initedD
  1029            simp add: check_field_access_def Let_def)
  1030   qed
  1031 qed
  1032 
  1033 lemma call_access_ok:
  1034   assumes invC_prop: "G\<turnstile>invmode statM e\<rightarrow>invC\<preceq>statT" 
  1035       and        wf: "wf_prog G" 
  1036       and      wt_e: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT"
  1037       and     statM: "(statDeclT,statM) \<in> mheads G accC statT sig" 
  1038       and      invC: "invC = invocation_class (invmode statM e) s a statT"
  1039   shows "\<exists> dynM. dynlookup G statT invC sig = Some dynM \<and>
  1040   G\<turnstile>Methd sig dynM in invC dyn_accessible_from accC"
  1041 proof -
  1042   from wt_e wf have type_statT: "is_type G (RefT statT)"
  1043     by (auto dest: ty_expr_is_type)
  1044   from statM have not_Null: "statT \<noteq> NullT" by auto
  1045   from type_statT wt_e 
  1046   have wf_I: "(\<forall>I. statT = IfaceT I \<longrightarrow> is_iface G I \<and> 
  1047                                         invmode statM e \<noteq> SuperM)"
  1048     by (auto dest: invocationTypeExpr_noClassD)
  1049   from wt_e
  1050   have wf_A: "(\<forall>     T. statT = ArrayT T \<longrightarrow> invmode statM e \<noteq> SuperM)"
  1051     by (auto dest: invocationTypeExpr_noClassD)
  1052   show ?thesis
  1053   proof (cases "invmode statM e = IntVir")
  1054     case True
  1055     with invC_prop not_Null
  1056     have invC_prop': "is_class G invC \<and>  
  1057                       (if (\<exists>T. statT=ArrayT T) then invC=Object 
  1058                                               else G\<turnstile>Class invC\<preceq>RefT statT)"
  1059       by (auto simp add: DynT_prop_def)
  1060     with True not_Null
  1061     have "G,statT \<turnstile> invC valid_lookup_cls_for is_static statM"
  1062      by (cases statT) (auto simp add: invmode_def) 
  1063     with statM type_statT wf 
  1064     show ?thesis
  1065       by - (rule dynlookup_access,auto)
  1066   next
  1067     case False
  1068     with type_statT wf invC not_Null wf_I wf_A
  1069     have invC_prop': " is_class G invC \<and>
  1070                       ((\<exists> statC. statT=ClassT statC \<and> invC=statC) \<or>
  1071                       (\<forall> statC. statT\<noteq>ClassT statC \<and> invC=Object)) "
  1072         by (case_tac "statT") (auto simp add: invocation_class_def 
  1073                                        split: inv_mode.splits)
  1074     with not_Null wf
  1075     have dynlookup_static: "dynlookup G statT invC sig = methd G invC sig"
  1076       by (case_tac "statT") (auto simp add: dynlookup_def dynmethd_C_C
  1077                                             dynimethd_def)
  1078    from statM wf wt_e not_Null False invC_prop' obtain dynM where
  1079                 "accmethd G accC invC sig = Some dynM" 
  1080      by (auto dest!: static_mheadsD)
  1081    from invC_prop' False not_Null wf_I
  1082    have "G,statT \<turnstile> invC valid_lookup_cls_for is_static statM"
  1083      by (cases statT) (auto simp add: invmode_def) 
  1084    with statM type_statT wf 
  1085     show ?thesis
  1086       by - (rule dynlookup_access,auto)
  1087   qed
  1088 qed
  1089 
  1090 lemma error_free_call_access:
  1091   assumes
  1092    eval_args: "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<rightarrow> s2" and
  1093         wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-(RefT statT)" and  
  1094        statM: "max_spec G accC statT \<lparr>name = mn, parTs = pTs\<rparr> 
  1095                = {((statDeclT, statM), pTs')}" and
  1096      conf_s2: "s2\<Colon>\<preceq>(G, L)" and
  1097       conf_a: "normal s1 \<Longrightarrow> G, store s1\<turnstile>a\<Colon>\<preceq>RefT statT" and
  1098      invProp: "normal s3 \<Longrightarrow>
  1099                 G\<turnstile>invmode statM e\<rightarrow>invC\<preceq>statT" and
  1100           s3: "s3=init_lvars G invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> 
  1101                         (invmode statM e) a vs s2" and
  1102         invC: "invC = invocation_class (invmode statM e) (store s2) a statT"and
  1103     invDeclC: "invDeclC = invocation_declclass G (invmode statM e) (store s2) 
  1104                              a statT \<lparr>name = mn, parTs = pTs'\<rparr>" and
  1105           wf: "wf_prog G"
  1106   shows "check_method_access G accC statT (invmode statM e) \<lparr>name=mn,parTs=pTs'\<rparr> a s3
  1107    = s3"
  1108 proof (cases "normal s2")
  1109   case False
  1110   with s3 
  1111   have "abrupt s3 = abrupt s2"  
  1112     by (auto simp add: init_lvars_def2)
  1113   with False
  1114   show ?thesis
  1115     by (auto simp add: check_method_access_def Let_def)
  1116 next
  1117   case True
  1118   note normal_s2 = True
  1119   with eval_args
  1120   have normal_s1: "normal s1"
  1121     by (cases "normal s1") auto
  1122   with conf_a eval_args 
  1123   have conf_a_s2: "G, store s2\<turnstile>a\<Colon>\<preceq>RefT statT"
  1124     by (auto dest: eval_gext intro: conf_gext)
  1125   show ?thesis
  1126   proof (cases "a=Null \<longrightarrow> (is_static statM)")
  1127     case False
  1128     then obtain "\<not> is_static statM" "a=Null" 
  1129       by blast
  1130     with normal_s2 s3
  1131     have "abrupt s3 = Some (Xcpt (Std NullPointer))" 
  1132       by (auto simp add: init_lvars_def2)
  1133     then show ?thesis
  1134       by (auto simp add: check_method_access_def Let_def)
  1135   next
  1136     case True
  1137     from statM 
  1138     obtain
  1139       statM': "(statDeclT,statM)\<in>mheads G accC statT \<lparr>name=mn,parTs=pTs'\<rparr>" 
  1140       by (blast dest: max_spec2mheads)
  1141     from True normal_s2 s3
  1142     have "normal s3"
  1143       by (auto simp add: init_lvars_def2)
  1144     then have "G\<turnstile>invmode statM e\<rightarrow>invC\<preceq>statT"
  1145       by (rule invProp)
  1146     with wt_e statM' wf invC
  1147     obtain dynM where 
  1148       dynM: "dynlookup G statT invC  \<lparr>name=mn,parTs=pTs'\<rparr> = Some dynM" and
  1149       acc_dynM: "G \<turnstile>Methd  \<lparr>name=mn,parTs=pTs'\<rparr> dynM 
  1150                           in invC dyn_accessible_from accC"
  1151       by (force dest!: call_access_ok)
  1152     moreover
  1153     from s3 invC
  1154     have invC': "invC=(invocation_class (invmode statM e) (store s3) a statT)"
  1155       by (cases s2,cases "invmode statM e") 
  1156          (simp add: init_lvars_def2 del: invmode_Static_eq)+
  1157     ultimately
  1158     show ?thesis
  1159       by (auto simp add: check_method_access_def Let_def)
  1160   qed
  1161 qed
  1162 
  1163 lemma map_upds_eq_length_append_simp:
  1164   "\<And> tab qs. length ps = length qs \<Longrightarrow>  tab(ps[\<mapsto>]qs@zs) = tab(ps[\<mapsto>]qs)"
  1165 proof (induct ps) 
  1166   case Nil thus ?case by simp
  1167 next
  1168   case (Cons p ps tab qs)
  1169   from `length (p#ps) = length qs`
  1170   obtain q qs' where qs: "qs=q#qs'" and eq_length: "length ps=length qs'"
  1171     by (cases qs) auto
  1172   from eq_length have "(tab(p\<mapsto>q))(ps[\<mapsto>]qs'@zs)=(tab(p\<mapsto>q))(ps[\<mapsto>]qs')"
  1173     by (rule Cons.hyps)
  1174   with qs show ?case 
  1175     by simp
  1176 qed
  1177 
  1178 lemma map_upds_upd_eq_length_simp:
  1179   "\<And> tab qs x y. length ps = length qs 
  1180                   \<Longrightarrow> tab(ps[\<mapsto>]qs)(x\<mapsto>y) = tab(ps@[x][\<mapsto>]qs@[y])"
  1181 proof (induct "ps")
  1182   case Nil thus ?case by simp
  1183 next
  1184   case (Cons p ps tab qs x y)
  1185   from `length (p#ps) = length qs`
  1186   obtain q qs' where qs: "qs=q#qs'" and eq_length: "length ps=length qs'"
  1187     by (cases qs) auto
  1188   from eq_length 
  1189   have "(tab(p\<mapsto>q))(ps[\<mapsto>]qs')(x\<mapsto>y) = (tab(p\<mapsto>q))(ps@[x][\<mapsto>]qs'@[y])"
  1190     by (rule Cons.hyps)
  1191   with qs show ?case
  1192     by simp
  1193 qed
  1194 
  1195 
  1196 lemma map_upd_cong: "tab=tab'\<Longrightarrow> tab(x\<mapsto>y) = tab'(x\<mapsto>y)"
  1197 by simp
  1198 
  1199 lemma map_upd_cong_ext: "tab z=tab' z\<Longrightarrow> (tab(x\<mapsto>y)) z = (tab'(x\<mapsto>y)) z"
  1200 by (simp add: fun_upd_def)
  1201 
  1202 lemma map_upds_cong: "tab=tab'\<Longrightarrow> tab(xs[\<mapsto>]ys) = tab'(xs[\<mapsto>]ys)"
  1203 by (cases xs) simp+
  1204 
  1205 lemma map_upds_cong_ext: 
  1206  "\<And> tab tab' ys. tab z=tab' z \<Longrightarrow> (tab(xs[\<mapsto>]ys)) z = (tab'(xs[\<mapsto>]ys)) z"
  1207 proof (induct xs)
  1208   case Nil thus ?case by simp
  1209 next
  1210   case (Cons x xs tab tab' ys)
  1211   note Hyps = this
  1212   show ?case
  1213   proof (cases ys)
  1214     case Nil
  1215     with Hyps
  1216     show ?thesis by simp
  1217   next
  1218     case (Cons y ys')
  1219     have "(tab(x\<mapsto>y)(xs[\<mapsto>]ys')) z = (tab'(x\<mapsto>y)(xs[\<mapsto>]ys')) z"
  1220       by (iprover intro: Hyps map_upd_cong_ext)
  1221     with Cons show ?thesis
  1222       by simp
  1223   qed
  1224 qed
  1225    
  1226 lemma map_upd_override: "(tab(x\<mapsto>y)) x = (tab'(x\<mapsto>y)) x"
  1227   by simp
  1228 
  1229 lemma map_upds_eq_length_suffix: "\<And> tab qs. 
  1230         length ps = length qs \<Longrightarrow> tab(ps@xs[\<mapsto>]qs) = tab(ps[\<mapsto>]qs)(xs[\<mapsto>][])"
  1231 proof (induct ps)
  1232   case Nil thus ?case by simp
  1233 next
  1234   case (Cons p ps tab qs)
  1235   then obtain q qs' where qs: "qs=q#qs'" and eq_length: "length ps=length qs'"
  1236     by (cases qs) auto
  1237   from eq_length
  1238   have "tab(p\<mapsto>q)(ps @ xs[\<mapsto>]qs') = tab(p\<mapsto>q)(ps[\<mapsto>]qs')(xs[\<mapsto>][])"
  1239     by (rule Cons.hyps)
  1240   with qs show ?case 
  1241     by simp
  1242 qed
  1243   
  1244   
  1245 lemma map_upds_upds_eq_length_prefix_simp:
  1246   "\<And> tab qs. length ps = length qs
  1247               \<Longrightarrow> tab(ps[\<mapsto>]qs)(xs[\<mapsto>]ys) = tab(ps@xs[\<mapsto>]qs@ys)"
  1248 proof (induct ps)
  1249   case Nil thus ?case by simp
  1250 next
  1251   case (Cons p ps tab qs)
  1252   then obtain q qs' where qs: "qs=q#qs'" and eq_length: "length ps=length qs'"
  1253     by (cases qs) auto
  1254   from eq_length 
  1255   have "tab(p\<mapsto>q)(ps[\<mapsto>]qs')(xs[\<mapsto>]ys) = tab(p\<mapsto>q)(ps @ xs[\<mapsto>](qs' @ ys))"
  1256     by (rule Cons.hyps)
  1257   with qs 
  1258   show ?case by simp
  1259 qed
  1260 
  1261 lemma map_upd_cut_irrelevant:
  1262 "\<lbrakk>(tab(x\<mapsto>y)) vn = Some el; (tab'(x\<mapsto>y)) vn = None\<rbrakk>
  1263     \<Longrightarrow> tab vn = Some el"
  1264 by (cases "tab' vn = None") (simp add: fun_upd_def)+
  1265 
  1266 lemma map_upd_Some_expand:
  1267 "\<lbrakk>tab vn = Some z\<rbrakk>
  1268     \<Longrightarrow> \<exists> z. (tab(x\<mapsto>y)) vn = Some z"
  1269 by (simp add: fun_upd_def)
  1270 
  1271 lemma map_upds_Some_expand:
  1272 "\<And> tab ys z. \<lbrakk>tab vn = Some z\<rbrakk>
  1273     \<Longrightarrow> \<exists> z. (tab(xs[\<mapsto>]ys)) vn = Some z"
  1274 proof (induct xs)
  1275   case Nil thus ?case by simp
  1276 next
  1277   case (Cons x xs tab ys z)
  1278   note z = `tab vn = Some z`
  1279   show ?case
  1280   proof (cases ys)
  1281     case Nil
  1282     with z show ?thesis by simp
  1283   next
  1284     case (Cons y ys')
  1285     note ys = `ys = y#ys'`
  1286     from z obtain z' where "(tab(x\<mapsto>y)) vn = Some z'"
  1287       by (rule map_upd_Some_expand [of tab,elim_format]) blast
  1288     hence "\<exists>z. ((tab(x\<mapsto>y))(xs[\<mapsto>]ys')) vn = Some z"
  1289       by (rule Cons.hyps)
  1290     with ys show ?thesis
  1291       by simp
  1292   qed
  1293 qed
  1294 
  1295 
  1296 lemma map_upd_Some_swap:
  1297  "(tab(r\<mapsto>w)(u\<mapsto>v)) vn = Some z \<Longrightarrow> \<exists> z. (tab(u\<mapsto>v)(r\<mapsto>w)) vn = Some z"
  1298 by (simp add: fun_upd_def)
  1299 
  1300 lemma map_upd_None_swap:
  1301  "(tab(r\<mapsto>w)(u\<mapsto>v)) vn = None \<Longrightarrow> (tab(u\<mapsto>v)(r\<mapsto>w)) vn = None"
  1302 by (simp add: fun_upd_def)
  1303 
  1304 
  1305 lemma map_eq_upd_eq: "tab vn = tab' vn \<Longrightarrow> (tab(x\<mapsto>y)) vn = (tab'(x\<mapsto>y)) vn"
  1306 by (simp add: fun_upd_def)
  1307 
  1308 lemma map_upd_in_expansion_map_swap:
  1309  "\<lbrakk>(tab(x\<mapsto>y)) vn = Some z;tab vn \<noteq> Some z\<rbrakk> 
  1310                  \<Longrightarrow>  (tab'(x\<mapsto>y)) vn = Some z"
  1311 by (simp add: fun_upd_def)
  1312 
  1313 lemma map_upds_in_expansion_map_swap:
  1314  "\<And>tab tab' ys z. \<lbrakk>(tab(xs[\<mapsto>]ys)) vn = Some z;tab vn \<noteq> Some z\<rbrakk> 
  1315                  \<Longrightarrow>  (tab'(xs[\<mapsto>]ys)) vn = Some z"
  1316 proof (induct xs)
  1317   case Nil thus ?case by simp
  1318 next
  1319   case (Cons x xs tab tab' ys z)
  1320   note some = `(tab(x # xs[\<mapsto>]ys)) vn = Some z`
  1321   note tab_not_z = `tab vn \<noteq> Some z`
  1322   show ?case
  1323   proof (cases ys)
  1324     case Nil with some tab_not_z show ?thesis by simp
  1325   next
  1326     case (Cons y tl)
  1327     note ys = `ys = y#tl`
  1328     show ?thesis
  1329     proof (cases "(tab(x\<mapsto>y)) vn \<noteq> Some z")
  1330       case True
  1331       with some ys have "(tab'(x\<mapsto>y)(xs[\<mapsto>]tl)) vn = Some z"
  1332         by (fastsimp intro: Cons.hyps)
  1333       with ys show ?thesis 
  1334         by simp
  1335     next
  1336       case False
  1337       hence tabx_z: "(tab(x\<mapsto>y)) vn = Some z" by blast
  1338       moreover
  1339       from tabx_z tab_not_z
  1340       have "(tab'(x\<mapsto>y)) vn = Some z" 
  1341         by (rule map_upd_in_expansion_map_swap)
  1342       ultimately
  1343       have "(tab(x\<mapsto>y)) vn =(tab'(x\<mapsto>y)) vn"
  1344         by simp
  1345       hence "(tab(x\<mapsto>y)(xs[\<mapsto>]tl)) vn = (tab'(x\<mapsto>y)(xs[\<mapsto>]tl)) vn"
  1346         by (rule map_upds_cong_ext)
  1347       with some ys
  1348       show ?thesis 
  1349         by simp
  1350     qed
  1351   qed
  1352 qed
  1353    
  1354 lemma map_upds_Some_swap: 
  1355  assumes r_u: "(tab(r\<mapsto>w)(u\<mapsto>v)(xs[\<mapsto>]ys)) vn = Some z"
  1356     shows "\<exists> z. (tab(u\<mapsto>v)(r\<mapsto>w)(xs[\<mapsto>]ys)) vn = Some z"
  1357 proof (cases "(tab(r\<mapsto>w)(u\<mapsto>v)) vn = Some z")
  1358   case True
  1359   then obtain z' where "(tab(u\<mapsto>v)(r\<mapsto>w)) vn = Some z'"
  1360     by (rule map_upd_Some_swap [elim_format]) blast
  1361   thus "\<exists> z. (tab(u\<mapsto>v)(r\<mapsto>w)(xs[\<mapsto>]ys)) vn = Some z"
  1362     by (rule map_upds_Some_expand)
  1363 next
  1364   case False
  1365   with r_u
  1366   have "(tab(u\<mapsto>v)(r\<mapsto>w)(xs[\<mapsto>]ys)) vn = Some z"
  1367     by (rule map_upds_in_expansion_map_swap)
  1368   thus ?thesis
  1369     by simp
  1370 qed
  1371  
  1372 lemma map_upds_Some_insert:
  1373   assumes z: "(tab(xs[\<mapsto>]ys)) vn = Some z"
  1374     shows "\<exists> z. (tab(u\<mapsto>v)(xs[\<mapsto>]ys)) vn = Some z"
  1375 proof (cases "\<exists> z. tab vn = Some z")
  1376   case True
  1377   then obtain z' where "tab vn = Some z'" by blast
  1378   then obtain z'' where "(tab(u\<mapsto>v)) vn = Some z''"
  1379     by (rule map_upd_Some_expand [elim_format]) blast
  1380   thus ?thesis
  1381     by (rule map_upds_Some_expand)
  1382 next
  1383   case False
  1384   hence "tab vn \<noteq> Some z" by simp
  1385   with z
  1386   have "(tab(u\<mapsto>v)(xs[\<mapsto>]ys)) vn = Some z"
  1387     by (rule map_upds_in_expansion_map_swap)
  1388   thus ?thesis ..
  1389 qed
  1390    
  1391 lemma map_upds_None_cut:
  1392 assumes expand_None: "(tab(xs[\<mapsto>]ys)) vn = None"
  1393   shows "tab vn = None"
  1394 proof (cases "tab vn = None")
  1395   case True thus ?thesis by simp
  1396 next
  1397   case False then obtain z where "tab vn = Some z" by blast
  1398   then obtain z' where "(tab(xs[\<mapsto>]ys)) vn = Some z'"
  1399     by (rule map_upds_Some_expand [where  ?tab="tab",elim_format]) blast
  1400   with expand_None show ?thesis
  1401     by simp
  1402 qed
  1403     
  1404 
  1405 lemma map_upds_cut_irrelevant:
  1406 "\<And> tab tab' ys. \<lbrakk>(tab(xs[\<mapsto>]ys)) vn = Some el; (tab'(xs[\<mapsto>]ys)) vn = None\<rbrakk>
  1407                   \<Longrightarrow> tab vn = Some el"
  1408 proof  (induct "xs")
  1409   case Nil thus ?case by simp
  1410 next
  1411   case (Cons x xs tab tab' ys)
  1412   note tab_vn = `(tab(x # xs[\<mapsto>]ys)) vn = Some el`
  1413   note tab'_vn = `(tab'(x # xs[\<mapsto>]ys)) vn = None`
  1414   show ?case
  1415   proof (cases ys)
  1416     case Nil
  1417     with tab_vn show ?thesis by simp
  1418   next
  1419     case (Cons y tl)
  1420     note ys = `ys=y#tl`
  1421     with tab_vn tab'_vn 
  1422     have "(tab(x\<mapsto>y)) vn = Some el"
  1423       by - (rule Cons.hyps,auto)
  1424     moreover from tab'_vn ys
  1425     have "(tab'(x\<mapsto>y)(xs[\<mapsto>]tl)) vn = None" 
  1426       by simp
  1427     hence "(tab'(x\<mapsto>y)) vn = None"
  1428       by (rule map_upds_None_cut)
  1429     ultimately show "tab vn = Some el" 
  1430       by (rule map_upd_cut_irrelevant)
  1431   qed
  1432 qed
  1433 
  1434    
  1435 lemma dom_vname_split:
  1436  "dom (lname_case (ename_case (tab(x\<mapsto>y)(xs[\<mapsto>]ys)) a) b)
  1437    = dom (lname_case (ename_case (tab(x\<mapsto>y)) a) b) \<union> 
  1438      dom (lname_case (ename_case (tab(xs[\<mapsto>]ys)) a) b)"
  1439   (is "?List x xs y ys = ?Hd x y \<union> ?Tl xs ys")
  1440 proof 
  1441   show "?List x xs y ys \<subseteq> ?Hd x y \<union> ?Tl xs ys"
  1442   proof 
  1443     fix el 
  1444     assume el_in_list: "el \<in> ?List x xs y ys"
  1445     show "el \<in>  ?Hd x y \<union> ?Tl xs ys"
  1446     proof (cases el)
  1447       case This
  1448       with el_in_list show ?thesis by (simp add: dom_def)
  1449     next
  1450       case (EName en)
  1451       show ?thesis
  1452       proof (cases en)
  1453         case Res
  1454         with EName el_in_list show ?thesis by (simp add: dom_def)
  1455       next
  1456         case (VNam vn)
  1457         with EName el_in_list show ?thesis 
  1458           by (auto simp add: dom_def dest: map_upds_cut_irrelevant)
  1459       qed
  1460     qed
  1461   qed
  1462 next
  1463   show "?Hd x y \<union> ?Tl xs ys  \<subseteq> ?List x xs y ys" 
  1464   proof (rule subsetI)
  1465     fix el 
  1466     assume  el_in_hd_tl: "el \<in>  ?Hd x y \<union> ?Tl xs ys"
  1467     show "el \<in> ?List x xs y ys"
  1468     proof (cases el)
  1469       case This
  1470       with el_in_hd_tl show ?thesis by (simp add: dom_def)
  1471     next
  1472       case (EName en)
  1473       show ?thesis
  1474       proof (cases en)
  1475         case Res
  1476         with EName el_in_hd_tl show ?thesis by (simp add: dom_def)
  1477       next
  1478         case (VNam vn)
  1479         with EName el_in_hd_tl show ?thesis 
  1480           by (auto simp add: dom_def intro: map_upds_Some_expand 
  1481                                             map_upds_Some_insert)
  1482       qed
  1483     qed
  1484   qed
  1485 qed
  1486 
  1487 lemma dom_map_upd: "\<And> tab. dom (tab(x\<mapsto>y)) = dom tab \<union> {x}"
  1488 by (auto simp add: dom_def fun_upd_def)
  1489 
  1490 lemma dom_map_upds: "\<And> tab ys. length xs = length ys 
  1491   \<Longrightarrow> dom (tab(xs[\<mapsto>]ys)) = dom tab \<union> set xs"
  1492 proof (induct xs)
  1493   case Nil thus ?case by (simp add: dom_def)
  1494 next
  1495   case (Cons x xs tab ys)
  1496   note Hyp = Cons.hyps
  1497   note len = `length (x#xs)=length ys`
  1498   show ?case
  1499   proof (cases ys)
  1500     case Nil with len show ?thesis by simp
  1501   next
  1502     case (Cons y tl)
  1503     with len have "dom (tab(x\<mapsto>y)(xs[\<mapsto>]tl)) = dom (tab(x\<mapsto>y)) \<union> set xs"
  1504       by - (rule Hyp,simp)
  1505     moreover 
  1506     have "dom (tab(x\<mapsto>hd ys)) = dom tab \<union> {x}"
  1507       by (rule dom_map_upd)
  1508     ultimately
  1509     show ?thesis using Cons
  1510       by simp
  1511   qed
  1512 qed
  1513  
  1514 lemma dom_ename_case_None_simp:
  1515  "dom (ename_case vname_tab None) = VNam ` (dom vname_tab)"
  1516   apply (auto simp add: dom_def image_def )
  1517   apply (case_tac "x")
  1518   apply auto
  1519   done
  1520 
  1521 lemma dom_ename_case_Some_simp:
  1522  "dom (ename_case vname_tab (Some a)) = VNam ` (dom vname_tab) \<union> {Res}"
  1523   apply (auto simp add: dom_def image_def )
  1524   apply (case_tac "x")
  1525   apply auto
  1526   done
  1527 
  1528 lemma dom_lname_case_None_simp:
  1529   "dom (lname_case ename_tab None) = EName ` (dom ename_tab)"
  1530   apply (auto simp add: dom_def image_def )
  1531   apply (case_tac "x")
  1532   apply auto
  1533   done
  1534 
  1535 lemma dom_lname_case_Some_simp:
  1536  "dom (lname_case ename_tab (Some a)) = EName ` (dom ename_tab) \<union> {This}"
  1537   apply (auto simp add: dom_def image_def)
  1538   apply (case_tac "x")
  1539   apply auto
  1540   done
  1541 
  1542 lemmas dom_lname_ename_case_simps =  
  1543      dom_ename_case_None_simp dom_ename_case_Some_simp 
  1544      dom_lname_case_None_simp dom_lname_case_Some_simp
  1545 
  1546 lemma image_comp: 
  1547  "f ` g ` A = (f \<circ> g) ` A"
  1548 by (auto simp add: image_def)
  1549 
  1550 
  1551 lemma dom_locals_init_lvars: 
  1552   assumes m: "m=(mthd (the (methd G C sig)))"  
  1553   assumes len: "length (pars m) = length pvs"
  1554   shows "dom (locals (store (init_lvars G C sig (invmode m e) a pvs s)))  
  1555            = parameters m"
  1556 proof -
  1557   from m
  1558   have static_m': "is_static m = static m"
  1559     by simp
  1560   from len
  1561   have dom_vnames: "dom (empty(pars m[\<mapsto>]pvs))=set (pars m)"
  1562     by (simp add: dom_map_upds)
  1563   show ?thesis
  1564   proof (cases "static m")
  1565     case True
  1566     with static_m' dom_vnames m
  1567     show ?thesis
  1568       by (cases s) (simp add: init_lvars_def Let_def parameters_def
  1569                               dom_lname_ename_case_simps image_comp)
  1570   next
  1571     case False
  1572     with static_m' dom_vnames m
  1573     show ?thesis
  1574       by (cases s) (simp add: init_lvars_def Let_def parameters_def
  1575                               dom_lname_ename_case_simps image_comp)
  1576   qed
  1577 qed
  1578 
  1579 
  1580 lemma da_e2_BinOp:
  1581   assumes da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1582                   \<turnstile>dom (locals (store s0)) \<guillemotright>\<langle>BinOp binop e1 e2\<rangle>\<^sub>e\<guillemotright> A"
  1583     and wt_e1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e1\<Colon>-e1T"
  1584     and wt_e2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e2\<Colon>-e2T" 
  1585     and wt_binop: "wt_binop G binop e1T e2T" 
  1586     and conf_s0: "s0\<Colon>\<preceq>(G,L)"  
  1587     and normal_s1: "normal s1"
  1588     and eval_e1: "G\<turnstile>s0 \<midarrow>e1-\<succ>v1\<rightarrow> s1"
  1589     and conf_v1: "G,store s1\<turnstile>v1\<Colon>\<preceq>e1T"
  1590     and wf: "wf_prog G"
  1591   shows "\<exists> E2. \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) 
  1592          \<guillemotright>(if need_second_arg binop v1 then \<langle>e2\<rangle>\<^sub>e else \<langle>Skip\<rangle>\<^sub>s)\<guillemotright> E2"
  1593 proof -
  1594   note inj_term_simps [simp]
  1595   from da obtain E1 where
  1596     da_e1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr> \<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>e1\<rangle>\<^sub>e\<guillemotright> E1"
  1597     by cases simp+
  1598   obtain E2 where
  1599     "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) 
  1600       \<guillemotright>(if need_second_arg binop v1 then \<langle>e2\<rangle>\<^sub>e else \<langle>Skip\<rangle>\<^sub>s)\<guillemotright> E2"
  1601   proof (cases "need_second_arg binop v1")
  1602     case False
  1603     obtain S where
  1604       daSkip: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1605                   \<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>Skip\<rangle>\<^sub>s\<guillemotright> S"
  1606       by (auto intro: da_Skip [simplified] assigned.select_convs)
  1607     thus ?thesis
  1608       using that by (simp add: False)
  1609   next
  1610     case True
  1611     from eval_e1 have 
  1612       s0_s1:"dom (locals (store s0)) \<subseteq> dom (locals (store s1))"
  1613       by (rule dom_locals_eval_mono_elim)
  1614     {
  1615       assume condAnd: "binop=CondAnd"
  1616       have ?thesis
  1617       proof -
  1618         from da obtain E2' where
  1619           "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1620              \<turnstile> dom (locals (store s0)) \<union> assigns_if True e1 \<guillemotright>\<langle>e2\<rangle>\<^sub>e\<guillemotright> E2'"
  1621           by cases (simp add: condAnd)+
  1622         moreover
  1623         have "dom (locals (store s0)) 
  1624           \<union> assigns_if True e1 \<subseteq> dom (locals (store s1))"
  1625         proof -
  1626           from condAnd wt_binop have e1T: "e1T=PrimT Boolean"
  1627             by simp
  1628           with normal_s1 conf_v1 obtain b where "v1=Bool b"
  1629             by (auto dest: conf_Boolean)
  1630           with True condAnd
  1631           have v1: "v1=Bool True"
  1632             by simp
  1633           from eval_e1 normal_s1 
  1634           have "assigns_if True e1 \<subseteq> dom (locals (store s1))"
  1635             by (rule assigns_if_good_approx' [elim_format])
  1636                (insert wt_e1, simp_all add: e1T v1)
  1637           with s0_s1 show ?thesis by (rule Un_least)
  1638         qed
  1639         ultimately
  1640         show ?thesis
  1641           using that by (cases rule: da_weakenE) (simp add: True)
  1642       qed
  1643     }
  1644     moreover
  1645     { 
  1646       assume condOr: "binop=CondOr"
  1647       have ?thesis
  1648         (* Beweis durch Analogie/Example/Pattern?, True\<rightarrow>False; And\<rightarrow>Or *)
  1649       proof -
  1650         from da obtain E2' where
  1651           "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1652               \<turnstile> dom (locals (store s0)) \<union> assigns_if False e1 \<guillemotright>\<langle>e2\<rangle>\<^sub>e\<guillemotright> E2'"
  1653           by cases (simp add: condOr)+
  1654         moreover
  1655         have "dom (locals (store s0)) 
  1656                      \<union> assigns_if False e1 \<subseteq> dom (locals (store s1))"
  1657         proof -
  1658           from condOr wt_binop have e1T: "e1T=PrimT Boolean"
  1659             by simp
  1660           with normal_s1 conf_v1 obtain b where "v1=Bool b"
  1661             by (auto dest: conf_Boolean)
  1662           with True condOr
  1663           have v1: "v1=Bool False"
  1664             by simp
  1665           from eval_e1 normal_s1 
  1666           have "assigns_if False e1 \<subseteq> dom (locals (store s1))"
  1667             by (rule assigns_if_good_approx' [elim_format])
  1668                (insert wt_e1, simp_all add: e1T v1)
  1669           with s0_s1 show ?thesis by (rule Un_least)
  1670         qed
  1671         ultimately
  1672         show ?thesis
  1673           using that by (rule da_weakenE) (simp add: True)
  1674       qed
  1675     }
  1676     moreover
  1677     {
  1678       assume notAndOr: "binop\<noteq>CondAnd" "binop\<noteq>CondOr"
  1679       have ?thesis
  1680       proof -
  1681         from da notAndOr obtain E1' where
  1682           da_e1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  1683                   \<turnstile> dom (locals (store s0)) \<guillemotright>\<langle>e1\<rangle>\<^sub>e\<guillemotright> E1'"
  1684           and da_e2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> nrm E1' \<guillemotright>In1l e2\<guillemotright> A"
  1685           by cases simp+
  1686         from eval_e1 wt_e1 da_e1 wf normal_s1 
  1687         have "nrm E1' \<subseteq> dom (locals (store s1))"
  1688           by (cases rule: da_good_approxE') iprover
  1689         with da_e2 show ?thesis
  1690           using that by (rule da_weakenE) (simp add: True)
  1691       qed
  1692     }
  1693     ultimately show ?thesis
  1694       by (cases binop) auto
  1695   qed
  1696   thus ?thesis ..
  1697 qed
  1698 
  1699 section "main proof of type safety"
  1700     
  1701 lemma eval_type_sound:
  1702   assumes  eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" 
  1703    and      wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T" 
  1704    and      da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>t\<guillemotright>A"
  1705    and      wf: "wf_prog G" 
  1706    and conf_s0: "s0\<Colon>\<preceq>(G,L)"           
  1707   shows "s1\<Colon>\<preceq>(G,L) \<and>  (normal s1 \<longrightarrow> G,L,store s1\<turnstile>t\<succ>v\<Colon>\<preceq>T) \<and> 
  1708          (error_free s0 = error_free s1)"
  1709 proof -
  1710   note inj_term_simps [simp]
  1711   let ?TypeSafeObj = "\<lambda> s0 s1 t v. 
  1712           \<forall>  L accC T A. s0\<Colon>\<preceq>(G,L) \<longrightarrow> \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T
  1713                       \<longrightarrow> \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>t\<guillemotright>A  
  1714                       \<longrightarrow> s1\<Colon>\<preceq>(G,L) \<and> (normal s1 \<longrightarrow> G,L,store s1\<turnstile>t\<succ>v\<Colon>\<preceq>T)
  1715                           \<and> (error_free s0 = error_free s1)"
  1716   from eval 
  1717   have "\<And> L accC T A. \<lbrakk>s0\<Colon>\<preceq>(G,L);\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T;
  1718                       \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>t\<guillemotright>A\<rbrakk>  
  1719         \<Longrightarrow> s1\<Colon>\<preceq>(G,L) \<and> (normal s1 \<longrightarrow> G,L,store s1\<turnstile>t\<succ>v\<Colon>\<preceq>T)
  1720             \<and> (error_free s0 = error_free s1)"
  1721    (is "PROP ?TypeSafe s0 s1 t v"
  1722     is "\<And> L accC T A. ?Conform L s0 \<Longrightarrow> ?WellTyped L accC T t  
  1723                  \<Longrightarrow> ?DefAss L accC s0 t A 
  1724                  \<Longrightarrow> ?Conform L s1 \<and> ?ValueTyped L T s1 t v \<and>
  1725                      ?ErrorFree s0 s1")
  1726   proof (induct)
  1727     case (Abrupt xc s t L accC T A) 
  1728     from `(Some xc, s)\<Colon>\<preceq>(G,L)`
  1729     show "(Some xc, s)\<Colon>\<preceq>(G,L) \<and> 
  1730       (normal (Some xc, s) 
  1731       \<longrightarrow> G,L,store (Some xc,s)\<turnstile>t\<succ>undefined3 t\<Colon>\<preceq>T) \<and> 
  1732       (error_free (Some xc, s) = error_free (Some xc, s))"
  1733       by simp
  1734   next
  1735     case (Skip s L accC T A)
  1736     from `Norm s\<Colon>\<preceq>(G, L)` and
  1737       `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r Skip\<Colon>T`
  1738     show "Norm s\<Colon>\<preceq>(G, L) \<and>
  1739               (normal (Norm s) \<longrightarrow> G,L,store (Norm s)\<turnstile>In1r Skip\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and> 
  1740               (error_free (Norm s) = error_free (Norm s))"
  1741       by simp
  1742   next
  1743     case (Expr s0 e v s1 L accC T A)
  1744     note `G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1`
  1745     note hyp = `PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)`
  1746     note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
  1747     moreover
  1748     note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (Expr e)\<Colon>T`
  1749     then obtain eT 
  1750       where "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l e\<Colon>eT"
  1751       by (rule wt_elim_cases) blast
  1752     moreover
  1753     from Expr.prems obtain E where
  1754       "\<lparr>prg=G,cls=accC, lcl=L\<rparr>\<turnstile>dom (locals (store ((Norm s0)::state)))\<guillemotright>In1l e\<guillemotright>E"
  1755       by (elim da_elim_cases) simp
  1756     ultimately 
  1757     obtain "s1\<Colon>\<preceq>(G, L)" and "error_free s1"
  1758       by (rule hyp [elim_format]) simp
  1759     with wt
  1760     show "s1\<Colon>\<preceq>(G, L) \<and>
  1761           (normal s1 \<longrightarrow> G,L,store s1\<turnstile>In1r (Expr e)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and> 
  1762           (error_free (Norm s0) = error_free s1)"
  1763       by (simp)
  1764   next
  1765     case (Lab s0 c s1 l L accC T A)
  1766     note hyp = `PROP ?TypeSafe (Norm s0) s1 (In1r c) \<diamondsuit>`
  1767     note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
  1768     moreover
  1769     note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (l\<bullet> c)\<Colon>T`
  1770     then have "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c\<Colon>\<surd>"
  1771       by (rule wt_elim_cases) blast
  1772     moreover from Lab.prems obtain C where
  1773      "\<lparr>prg=G,cls=accC, lcl=L\<rparr>\<turnstile>dom (locals (store ((Norm s0)::state)))\<guillemotright>In1r c\<guillemotright>C"
  1774       by (elim da_elim_cases) simp
  1775     ultimately
  1776     obtain       conf_s1: "s1\<Colon>\<preceq>(G, L)" and 
  1777            error_free_s1: "error_free s1" 
  1778       by (rule hyp [elim_format]) simp
  1779     from conf_s1 have "abupd (absorb l) s1\<Colon>\<preceq>(G, L)"
  1780       by (cases s1) (auto intro: conforms_absorb)
  1781     with wt error_free_s1
  1782     show "abupd (absorb l) s1\<Colon>\<preceq>(G, L) \<and>
  1783           (normal (abupd (absorb l) s1)
  1784            \<longrightarrow> G,L,store (abupd (absorb l) s1)\<turnstile>In1r (l\<bullet> c)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
  1785           (error_free (Norm s0) = error_free (abupd (absorb l) s1))"
  1786       by (simp)
  1787   next
  1788     case (Comp s0 c1 s1 c2 s2 L accC T A)
  1789     note eval_c1 = `G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1`
  1790     note eval_c2 = `G\<turnstile>s1 \<midarrow>c2\<rightarrow> s2`
  1791     note hyp_c1 = `PROP ?TypeSafe (Norm s0) s1 (In1r c1) \<diamondsuit>`
  1792     note hyp_c2 = `PROP ?TypeSafe s1        s2 (In1r c2) \<diamondsuit>`
  1793     note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
  1794     note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (c1;; c2)\<Colon>T`
  1795     then obtain wt_c1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
  1796                 wt_c2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c2\<Colon>\<surd>"
  1797       by (rule wt_elim_cases) blast
  1798     from Comp.prems
  1799     obtain C1 C2
  1800       where da_c1: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile> 
  1801                       dom (locals (store ((Norm s0)::state))) \<guillemotright>In1r c1\<guillemotright> C1" and 
  1802             da_c2: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>  nrm C1 \<guillemotright>In1r c2\<guillemotright> C2" 
  1803       by (elim da_elim_cases) simp
  1804     from conf_s0 wt_c1 da_c1
  1805     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and 
  1806            error_free_s1: "error_free s1"
  1807       by (rule hyp_c1 [elim_format]) simp
  1808     show "s2\<Colon>\<preceq>(G, L) \<and>
  1809           (normal s2 \<longrightarrow> G,L,store s2\<turnstile>In1r (c1;; c2)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
  1810           (error_free (Norm s0) = error_free s2)"
  1811     proof (cases "normal s1")
  1812       case False
  1813       with eval_c2 have "s2=s1" by auto
  1814       with conf_s1 error_free_s1 False wt show ?thesis
  1815         by simp
  1816     next
  1817       case True
  1818       obtain C2' where 
  1819         "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>In1r c2\<guillemotright> C2'"
  1820       proof -
  1821         from eval_c1 wt_c1 da_c1 wf True
  1822         have "nrm C1 \<subseteq> dom (locals (store s1))"
  1823           by (cases rule: da_good_approxE') iprover
  1824         with da_c2 show thesis
  1825           by (rule da_weakenE) (rule that)
  1826       qed
  1827       with conf_s1 wt_c2 
  1828       obtain "s2\<Colon>\<preceq>(G, L)" and "error_free s2"
  1829         by (rule hyp_c2 [elim_format]) (simp add: error_free_s1)
  1830       thus ?thesis
  1831         using wt by simp
  1832     qed
  1833   next
  1834     case (If s0 e b s1 c1 c2 s2 L accC T A)
  1835     note eval_e = `G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1`
  1836     note eval_then_else = `G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2`
  1837     note hyp_e = `PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 b)`
  1838     note hyp_then_else =
  1839       `PROP ?TypeSafe s1 s2 (In1r (if the_Bool b then c1 else c2)) \<diamondsuit>`
  1840     note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
  1841     note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (If(e) c1 Else c2)\<Colon>T`
  1842     then obtain 
  1843               wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean" and
  1844       wt_then_else: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(if the_Bool b then c1 else c2)\<Colon>\<surd>"
  1845       (*
  1846                 wt_c1: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
  1847                 wt_c2: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>c2\<Colon>\<surd>"*)
  1848       by (rule wt_elim_cases) (auto split add: split_if)
  1849     from If.prems obtain E C where
  1850       da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store ((Norm s0)::state))) 
  1851                                        \<guillemotright>In1l e\<guillemotright> E" and
  1852       da_then_else: 
  1853       "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> 
  1854          (dom (locals (store ((Norm s0)::state))) \<union> assigns_if (the_Bool b) e)
  1855           \<guillemotright>In1r (if the_Bool b then c1 else c2)\<guillemotright> C"
  1856      (*
  1857      da_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store ((Norm s0)::state))) 
  1858                                       \<union> assigns_if True e) \<guillemotright>In1r c1\<guillemotright> C1" and
  1859      da_c2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store ((Norm s0)::state))) 
  1860                                        \<union> assigns_if False e) \<guillemotright>In1r c2\<guillemotright> C2" *)
  1861       by (elim da_elim_cases) (cases "the_Bool b",auto)
  1862     from conf_s0 wt_e da_e  
  1863     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1"
  1864       by (rule hyp_e [elim_format]) simp
  1865     show "s2\<Colon>\<preceq>(G, L) \<and>
  1866            (normal s2 \<longrightarrow> G,L,store s2\<turnstile>In1r (If(e) c1 Else c2)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
  1867            (error_free (Norm s0) = error_free s2)"
  1868     proof (cases "normal s1")
  1869       case False
  1870       with eval_then_else have "s2=s1" by auto
  1871       with conf_s1 error_free_s1 False wt show ?thesis
  1872         by simp
  1873     next
  1874       case True
  1875       obtain C' where
  1876         "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> 
  1877           (dom (locals (store s1)))\<guillemotright>In1r (if the_Bool b then c1 else c2)\<guillemotright> C'"
  1878       proof -
  1879         from eval_e have 
  1880           "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
  1881           by (rule dom_locals_eval_mono_elim)
  1882         moreover
  1883         from eval_e True wt_e 
  1884         have "assigns_if (the_Bool b) e \<subseteq> dom (locals (store s1))"
  1885           by (rule assigns_if_good_approx')
  1886         ultimately 
  1887         have "dom (locals (store ((Norm s0)::state))) 
  1888                 \<union> assigns_if (the_Bool b) e \<subseteq> dom (locals (store s1))"
  1889           by (rule Un_least)
  1890         with da_then_else show thesis
  1891           by (rule da_weakenE) (rule that)
  1892       qed
  1893       with conf_s1 wt_then_else  
  1894       obtain "s2\<Colon>\<preceq>(G, L)" and "error_free s2"
  1895         by (rule hyp_then_else [elim_format]) (simp add: error_free_s1)
  1896       with wt show ?thesis
  1897         by simp
  1898     qed
  1899     -- {* Note that we don't have to show that @{term b} really is a boolean 
  1900           value. With @{term the_Bool} we enforce to get a value of boolean 
  1901           type. So execution will be type safe, even if b would be
  1902           a string, for example. We might not expect such a behaviour to be
  1903           called type safe. To remedy the situation we would have to change
  1904           the evaulation rule, so that it only has a type safe evaluation if
  1905           we actually get a boolean value for the condition. That b is actually
  1906           a boolean value is part of @{term hyp_e}. See also Loop 
  1907        *}
  1908   next
  1909     case (Loop s0 e b s1 c s2 l s3 L accC T A)
  1910     note eval_e = `G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1`
  1911     note hyp_e = `PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 b)`
  1912     note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
  1913     note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (l\<bullet> While(e) c)\<Colon>T`
  1914     then obtain wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean" and
  1915                 wt_c: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c\<Colon>\<surd>"
  1916       by (rule wt_elim_cases) blast
  1917     note da = `\<lparr>prg=G, cls=accC, lcl=L\<rparr>
  1918             \<turnstile> dom (locals(store ((Norm s0)::state))) \<guillemotright>In1r (l\<bullet> While(e) c)\<guillemotright> A`
  1919     then
  1920     obtain E C where
  1921       da_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>
  1922               \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1l e\<guillemotright> E" and
  1923       da_c: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>
  1924               \<turnstile> (dom (locals (store ((Norm s0)::state))) 
  1925                    \<union> assigns_if True e) \<guillemotright>In1r c\<guillemotright> C" 
  1926       by (rule da_elim_cases) simp
  1927     from conf_s0 wt_e da_e
  1928     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1"
  1929       by (rule hyp_e [elim_format]) simp
  1930     show "s3\<Colon>\<preceq>(G, L) \<and>
  1931           (normal s3 \<longrightarrow> G,L,store s3\<turnstile>In1r (l\<bullet> While(e) c)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
  1932           (error_free (Norm s0) = error_free s3)"
  1933     proof (cases "normal s1")
  1934       case True
  1935       note normal_s1 = this
  1936       show ?thesis
  1937       proof (cases "the_Bool b")
  1938         case True
  1939         with Loop.hyps  obtain
  1940           eval_c: "G\<turnstile>s1 \<midarrow>c\<rightarrow> s2" and 
  1941           eval_while: "G\<turnstile>abupd (absorb (Cont l)) s2 \<midarrow>l\<bullet> While(e) c\<rightarrow> s3"
  1942           by simp 
  1943         have "?TypeSafeObj s1 s2 (In1r c) \<diamondsuit>"
  1944           using Loop.hyps True by simp
  1945         note hyp_c = this [rule_format]
  1946         have "?TypeSafeObj (abupd (absorb (Cont l)) s2)
  1947           s3 (In1r (l\<bullet> While(e) c)) \<diamondsuit>"
  1948           using Loop.hyps True by simp
  1949         note hyp_w = this [rule_format]
  1950         from eval_e have 
  1951           s0_s1: "dom (locals (store ((Norm s0)::state)))
  1952                     \<subseteq> dom (locals (store s1))"
  1953           by (rule dom_locals_eval_mono_elim)
  1954         obtain C' where
  1955           "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(dom (locals (store s1)))\<guillemotright>In1r c\<guillemotright> C'" 
  1956         proof -
  1957           note s0_s1
  1958           moreover
  1959           from eval_e normal_s1 wt_e 
  1960           have "assigns_if True e \<subseteq> dom (locals (store s1))"
  1961             by (rule assigns_if_good_approx' [elim_format]) (simp add: True)
  1962           ultimately 
  1963           have "dom (locals (store ((Norm s0)::state))) 
  1964                  \<union> assigns_if True e \<subseteq> dom (locals (store s1))"
  1965             by (rule Un_least)
  1966           with da_c show thesis
  1967             by (rule da_weakenE) (rule that)
  1968         qed
  1969         with conf_s1 wt_c  
  1970         obtain conf_s2:  "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"
  1971           by (rule hyp_c [elim_format]) (simp add: error_free_s1)
  1972         from error_free_s2 
  1973         have error_free_ab_s2: "error_free (abupd (absorb (Cont l)) s2)"
  1974           by simp
  1975         from conf_s2 have "abupd (absorb (Cont l)) s2 \<Colon>\<preceq>(G, L)"
  1976           by (cases s2) (auto intro: conforms_absorb)
  1977         moreover note wt
  1978         moreover
  1979         obtain A' where 
  1980           "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> 
  1981               dom (locals(store (abupd (absorb (Cont l)) s2)))
  1982                 \<guillemotright>In1r (l\<bullet> While(e) c)\<guillemotright> A'"
  1983         proof -
  1984           note s0_s1
  1985           also from eval_c 
  1986           have "dom (locals (store s1)) \<subseteq> dom (locals (store s2))"
  1987             by (rule dom_locals_eval_mono_elim)
  1988           also have "\<dots> \<subseteq> dom (locals (store (abupd (absorb (Cont l)) s2)))"
  1989             by simp
  1990           finally
  1991           have "dom (locals (store ((Norm s0)::state))) \<subseteq> \<dots>" .
  1992           with da show thesis
  1993             by (rule da_weakenE) (rule that)
  1994         qed
  1995         ultimately obtain "s3\<Colon>\<preceq>(G, L)" and "error_free s3"
  1996           by (rule hyp_w [elim_format]) (simp add: error_free_ab_s2)
  1997         with wt show ?thesis
  1998           by simp
  1999       next
  2000         case False
  2001         with Loop.hyps have "s3=s1" by simp
  2002         with conf_s1 error_free_s1 wt
  2003         show ?thesis
  2004           by simp
  2005       qed
  2006     next
  2007       case False
  2008       have "s3=s1"
  2009       proof -
  2010         from False obtain abr where abr: "abrupt s1 = Some abr"
  2011           by (cases s1) auto
  2012         from eval_e _ wt_e have no_jmp: "\<And> j. abrupt s1 \<noteq> Some (Jump j)"
  2013           by (rule eval_expression_no_jump 
  2014                [where ?Env="\<lparr>prg=G,cls=accC,lcl=L\<rparr>",simplified]) 
  2015              (simp_all add: wf)
  2016             
  2017         show ?thesis
  2018         proof (cases "the_Bool b")
  2019           case True  
  2020           with Loop.hyps obtain
  2021             eval_c: "G\<turnstile>s1 \<midarrow>c\<rightarrow> s2" and 
  2022             eval_while: "G\<turnstile>abupd (absorb (Cont l)) s2 \<midarrow>l\<bullet> While(e) c\<rightarrow> s3"
  2023             by simp
  2024           from eval_c abr have "s2=s1" by auto
  2025           moreover from calculation no_jmp have "abupd (absorb (Cont l)) s2=s2"
  2026             by (cases s1) (simp add: absorb_def)
  2027           ultimately show ?thesis
  2028             using eval_while abr
  2029             by auto
  2030         next
  2031           case False
  2032           with Loop.hyps show ?thesis by simp
  2033         qed
  2034       qed
  2035       with conf_s1 error_free_s1 wt
  2036       show ?thesis
  2037         by simp
  2038     qed
  2039   next
  2040     case (Jmp s j L accC T A)
  2041     note `Norm s\<Colon>\<preceq>(G, L)`
  2042     moreover
  2043     from Jmp.prems 
  2044     have "j=Ret \<longrightarrow> Result \<in> dom (locals (store ((Norm s)::state)))"
  2045       by (elim da_elim_cases)
  2046     ultimately have "(Some (Jump j), s)\<Colon>\<preceq>(G, L)" by auto
  2047     then 
  2048     show "(Some (Jump j), s)\<Colon>\<preceq>(G, L) \<and>
  2049            (normal (Some (Jump j), s) 
  2050            \<longrightarrow> G,L,store (Some (Jump j), s)\<turnstile>In1r (Jmp j)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
  2051            (error_free (Norm s) = error_free (Some (Jump j), s))"
  2052       by simp
  2053   next
  2054     case (Throw s0 e a s1 L accC T A)
  2055     note `G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<rightarrow> s1`
  2056     note hyp = `PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 a)`
  2057     note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
  2058     note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (Throw e)\<Colon>T`
  2059     then obtain tn 
  2060       where      wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-Class tn" and
  2061             throwable: "G\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable"
  2062       by (rule wt_elim_cases) (auto)
  2063     from Throw.prems obtain E where 
  2064       da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2065              \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1l e\<guillemotright> E"
  2066       by (elim da_elim_cases) simp
  2067     from conf_s0 wt_e da_e obtain
  2068       "s1\<Colon>\<preceq>(G, L)" and
  2069       "(normal s1 \<longrightarrow> G,store s1\<turnstile>a\<Colon>\<preceq>Class tn)" and
  2070       error_free_s1: "error_free s1"
  2071       by (rule hyp [elim_format]) simp
  2072     with wf throwable
  2073     have "abupd (throw a) s1\<Colon>\<preceq>(G, L)" 
  2074       by (cases s1) (auto dest: Throw_lemma)
  2075     with wt error_free_s1
  2076     show "abupd (throw a) s1\<Colon>\<preceq>(G, L) \<and>
  2077             (normal (abupd (throw a) s1) \<longrightarrow>
  2078             G,L,store (abupd (throw a) s1)\<turnstile>In1r (Throw e)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
  2079             (error_free (Norm s0) = error_free (abupd (throw a) s1))"
  2080       by simp
  2081   next
  2082     case (Try s0 c1 s1 s2 catchC vn c2 s3 L accC T A)
  2083     note eval_c1 = `G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1`
  2084     note sx_alloc = `G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2`
  2085     note hyp_c1 = `PROP ?TypeSafe (Norm s0) s1 (In1r c1) \<diamondsuit>`
  2086     note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
  2087     note wt = `\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>In1r (Try c1 Catch(catchC vn) c2)\<Colon>T`
  2088     then obtain 
  2089       wt_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
  2090       wt_c2: "\<lparr>prg=G,cls=accC,lcl=L(VName vn\<mapsto>Class catchC)\<rparr>\<turnstile>c2\<Colon>\<surd>" and
  2091       fresh_vn: "L(VName vn)=None"
  2092       by (rule wt_elim_cases) simp
  2093     from Try.prems obtain C1 C2 where
  2094       da_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2095                 \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1r c1\<guillemotright> C1"  and
  2096       da_c2:
  2097        "\<lparr>prg=G,cls=accC,lcl=L(VName vn\<mapsto>Class catchC)\<rparr>
  2098         \<turnstile> (dom (locals (store ((Norm s0)::state))) \<union> {VName vn}) \<guillemotright>In1r c2\<guillemotright> C2"
  2099       by (elim da_elim_cases) simp
  2100     from conf_s0 wt_c1 da_c1
  2101     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1"
  2102       by (rule hyp_c1 [elim_format]) simp
  2103     from conf_s1 sx_alloc wf 
  2104     have conf_s2: "s2\<Colon>\<preceq>(G, L)" 
  2105       by (auto dest: sxalloc_type_sound split: option.splits abrupt.splits)
  2106     from sx_alloc error_free_s1 
  2107     have error_free_s2: "error_free s2"
  2108       by (rule error_free_sxalloc)
  2109     show "s3\<Colon>\<preceq>(G, L) \<and>
  2110           (normal s3 \<longrightarrow> G,L,store s3\<turnstile>In1r (Try c1 Catch(catchC vn) c2)\<succ>\<diamondsuit>\<Colon>\<preceq>T)\<and>
  2111           (error_free (Norm s0) = error_free s3)"
  2112     proof (cases "\<exists> x. abrupt s1 = Some (Xcpt x)")
  2113       case False
  2114       from sx_alloc wf
  2115       have eq_s2_s1: "s2=s1"
  2116         by (rule sxalloc_type_sound [elim_format])
  2117            (insert False, auto split: option.splits abrupt.splits )
  2118       with False 
  2119       have "\<not>  G,s2\<turnstile>catch catchC"
  2120         by (simp add: catch_def)
  2121       with Try
  2122       have "s3=s2"
  2123         by simp
  2124       with wt conf_s1 error_free_s1 eq_s2_s1
  2125       show ?thesis
  2126         by simp
  2127     next
  2128       case True
  2129       note exception_s1 = this
  2130       show ?thesis
  2131       proof (cases "G,s2\<turnstile>catch catchC") 
  2132         case False
  2133         with Try
  2134         have "s3=s2"
  2135           by simp
  2136         with wt conf_s2 error_free_s2 
  2137         show ?thesis
  2138           by simp
  2139       next
  2140         case True
  2141         with Try have "G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<rightarrow> s3" by simp
  2142         from True Try.hyps
  2143         have "?TypeSafeObj (new_xcpt_var vn s2) s3 (In1r c2) \<diamondsuit>"
  2144           by simp
  2145         note hyp_c2 = this [rule_format]
  2146         from exception_s1 sx_alloc wf
  2147         obtain a 
  2148           where xcpt_s2: "abrupt s2 = Some (Xcpt (Loc a))"
  2149           by (auto dest!: sxalloc_type_sound split: option.splits abrupt.splits)
  2150         with True
  2151         have "G\<turnstile>obj_ty (the (globs (store s2) (Heap a)))\<preceq>Class catchC"
  2152           by (cases s2) simp
  2153         with xcpt_s2 conf_s2 wf
  2154         have "new_xcpt_var vn s2 \<Colon>\<preceq>(G, L(VName vn\<mapsto>Class catchC))"
  2155           by (auto dest: Try_lemma)
  2156         moreover note wt_c2
  2157         moreover
  2158         obtain C2' where
  2159           "\<lparr>prg=G,cls=accC,lcl=L(VName vn\<mapsto>Class catchC)\<rparr>
  2160           \<turnstile> (dom (locals (store (new_xcpt_var vn s2)))) \<guillemotright>In1r c2\<guillemotright> C2'"
  2161         proof -
  2162           have "(dom (locals (store ((Norm s0)::state))) \<union> {VName vn}) 
  2163                   \<subseteq> dom (locals (store (new_xcpt_var vn s2)))"
  2164           proof -
  2165             from `G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1`
  2166             have "dom (locals (store ((Norm s0)::state))) 
  2167                     \<subseteq> dom (locals (store s1))"
  2168               by (rule dom_locals_eval_mono_elim)
  2169             also
  2170             from sx_alloc
  2171             have "\<dots> \<subseteq> dom (locals (store s2))"
  2172               by (rule dom_locals_sxalloc_mono)
  2173             also 
  2174             have "\<dots> \<subseteq> dom (locals (store (new_xcpt_var vn s2)))" 
  2175               by (cases s2) (simp add: new_xcpt_var_def, blast) 
  2176             also
  2177             have "{VName vn} \<subseteq> \<dots>"
  2178               by (cases s2) simp
  2179             ultimately show ?thesis
  2180               by (rule Un_least)
  2181           qed
  2182           with da_c2 show thesis
  2183             by (rule da_weakenE) (rule that)
  2184         qed
  2185         ultimately
  2186         obtain       conf_s3: "s3\<Colon>\<preceq>(G, L(VName vn\<mapsto>Class catchC))" and
  2187                error_free_s3: "error_free s3"
  2188           by (rule hyp_c2 [elim_format])
  2189              (cases s2, simp add: xcpt_s2 error_free_s2) 
  2190         from conf_s3 fresh_vn 
  2191         have "s3\<Colon>\<preceq>(G,L)"
  2192           by (blast intro: conforms_deallocL)
  2193         with wt error_free_s3
  2194         show ?thesis
  2195           by simp
  2196       qed
  2197     qed
  2198   next
  2199     case (Fin s0 c1 x1 s1 c2 s2 s3 L accC T A)
  2200     note eval_c1 = `G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1, s1)`
  2201     note eval_c2 = `G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2`
  2202     note s3 = `s3 = (if \<exists>err. x1 = Some (Error err)
  2203                      then (x1, s1)
  2204                      else abupd (abrupt_if (x1 \<noteq> None) x1) s2)`
  2205     note hyp_c1 = `PROP ?TypeSafe (Norm s0) (x1,s1) (In1r c1) \<diamondsuit>`
  2206     note hyp_c2 = `PROP ?TypeSafe (Norm s1) s2      (In1r c2) \<diamondsuit>`
  2207     note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
  2208     note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (c1 Finally c2)\<Colon>T`
  2209     then obtain
  2210       wt_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
  2211       wt_c2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c2\<Colon>\<surd>"
  2212       by (rule wt_elim_cases) blast
  2213     from Fin.prems obtain C1 C2 where
  2214       da_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2215                \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1r c1\<guillemotright> C1" and
  2216       da_c2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2217                \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1r c2\<guillemotright> C2"
  2218       by (elim da_elim_cases) simp 
  2219     from conf_s0 wt_c1 da_c1   
  2220     obtain conf_s1: "(x1,s1)\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free (x1,s1)"
  2221       by (rule hyp_c1 [elim_format]) simp
  2222     from conf_s1 have "Norm s1\<Colon>\<preceq>(G, L)"
  2223       by (rule conforms_NormI)
  2224     moreover note wt_c2
  2225     moreover obtain C2'
  2226       where "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2227                \<turnstile> dom (locals (store ((Norm s1)::state))) \<guillemotright>In1r c2\<guillemotright> C2'"
  2228     proof -
  2229       from eval_c1
  2230       have "dom (locals (store ((Norm s0)::state))) 
  2231              \<subseteq> dom (locals (store (x1,s1)))"
  2232         by (rule dom_locals_eval_mono_elim)
  2233       hence "dom (locals (store ((Norm s0)::state))) 
  2234               \<subseteq> dom (locals (store ((Norm s1)::state)))"
  2235         by simp
  2236       with da_c2 show thesis
  2237         by (rule da_weakenE) (rule that)
  2238     qed
  2239     ultimately
  2240     obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"
  2241       by (rule hyp_c2 [elim_format]) simp
  2242     from error_free_s1 s3 
  2243     have s3': "s3=abupd (abrupt_if (x1 \<noteq> None) x1) s2"
  2244       by simp
  2245     show "s3\<Colon>\<preceq>(G, L) \<and>
  2246           (normal s3 \<longrightarrow> G,L,store s3 \<turnstile>In1r (c1 Finally c2)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and> 
  2247           (error_free (Norm s0) = error_free s3)"
  2248     proof (cases x1)
  2249       case None with conf_s2 s3' wt error_free_s2
  2250       show ?thesis by auto
  2251     next
  2252       case (Some x) 
  2253       from eval_c2 have 
  2254         "dom (locals (store ((Norm s1)::state))) \<subseteq> dom (locals (store s2))"
  2255         by (rule dom_locals_eval_mono_elim)
  2256       with Some eval_c2 wf conf_s1 conf_s2
  2257       have conf: "(abrupt_if True (Some x) (abrupt s2), store s2)\<Colon>\<preceq>(G, L)"
  2258         by (cases s2) (auto dest: Fin_lemma)
  2259       from Some error_free_s1
  2260       have "\<not> (\<exists> err. x=Error err)"
  2261         by (simp add: error_free_def)
  2262       with error_free_s2
  2263       have "error_free (abrupt_if True (Some x) (abrupt s2), store s2)"
  2264         by (cases s2) simp
  2265       with Some wt conf s3' show ?thesis
  2266         by (cases s2) auto
  2267     qed
  2268   next
  2269     case (Init C c s0 s3 s1 s2 L accC T A)
  2270     note cls = `the (class G C) = c`
  2271     note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
  2272     note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (Init C)\<Colon>T`
  2273     with cls
  2274     have cls_C: "class G C = Some c"
  2275       by - (erule wt_elim_cases, auto)
  2276     show "s3\<Colon>\<preceq>(G, L) \<and> (normal s3 \<longrightarrow> G,L,store s3\<turnstile>In1r (Init C)\<succ>\<diamondsuit>\<Colon>\<preceq>T) \<and>
  2277           (error_free (Norm s0) = error_free s3)"
  2278     proof (cases "inited C (globs s0)")
  2279       case True
  2280       with Init.hyps have "s3 = Norm s0"
  2281         by simp
  2282       with conf_s0 wt show ?thesis 
  2283         by simp
  2284     next
  2285       case False
  2286       with Init.hyps obtain 
  2287            eval_init_super: 
  2288            "G\<turnstile>Norm ((init_class_obj G C) s0) 
  2289               \<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1" and
  2290         eval_init: "G\<turnstile>(set_lvars empty) s1 \<midarrow>init c\<rightarrow> s2" and
  2291         s3: "s3 = (set_lvars (locals (store s1))) s2" 
  2292         by simp
  2293       have "?TypeSafeObj (Norm ((init_class_obj G C) s0)) s1
  2294                       (In1r (if C = Object then Skip else Init (super c))) \<diamondsuit>"
  2295         using False Init.hyps by simp
  2296       note hyp_init_super = this [rule_format] 
  2297       have "?TypeSafeObj ((set_lvars empty) s1) s2 (In1r (init c)) \<diamondsuit>"
  2298         using False Init.hyps by simp
  2299       note hyp_init_c = this [rule_format]
  2300       from conf_s0 wf cls_C False
  2301       have "(Norm ((init_class_obj G C) s0))\<Colon>\<preceq>(G, L)"
  2302         by (auto dest: conforms_init_class_obj)
  2303       moreover from wf cls_C have
  2304         wt_init_super: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>
  2305                          \<turnstile>(if C = Object then Skip else Init (super c))\<Colon>\<surd>"
  2306         by (cases "C=Object")
  2307            (auto dest: wf_prog_cdecl wf_cdecl_supD is_acc_classD)
  2308       moreover
  2309       obtain S where
  2310         da_init_super:
  2311         "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2312           \<turnstile> dom (locals (store ((Norm ((init_class_obj G C) s0))::state))) 
  2313                \<guillemotright>In1r (if C = Object then Skip else Init (super c))\<guillemotright> S"
  2314       proof (cases "C=Object")
  2315         case True 
  2316         with da_Skip show ?thesis
  2317           using that by (auto intro: assigned.select_convs)
  2318       next
  2319         case False 
  2320         with da_Init show ?thesis
  2321           by - (rule that, auto intro: assigned.select_convs)
  2322       qed
  2323       ultimately 
  2324       obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1"
  2325         by (rule hyp_init_super [elim_format]) simp
  2326       from eval_init_super wt_init_super wf
  2327       have s1_no_ret: "\<And> j. abrupt s1 \<noteq> Some (Jump j)"
  2328         by - (rule eval_statement_no_jump [where ?Env="\<lparr>prg=G,cls=accC,lcl=L\<rparr>"],
  2329               auto)
  2330       with conf_s1
  2331       have "(set_lvars empty) s1\<Colon>\<preceq>(G, empty)"
  2332         by (cases s1) (auto intro: conforms_set_locals)
  2333       moreover 
  2334       from error_free_s1
  2335       have error_free_empty: "error_free ((set_lvars empty) s1)"
  2336         by simp
  2337       from cls_C wf have wt_init_c: "\<lparr>prg=G, cls=C,lcl=empty\<rparr>\<turnstile>(init c)\<Colon>\<surd>"
  2338         by (rule wf_prog_cdecl [THEN wf_cdecl_wt_init])
  2339       moreover from cls_C wf obtain I
  2340         where "\<lparr>prg=G,cls=C,lcl=empty\<rparr>\<turnstile> {} \<guillemotright>In1r (init c)\<guillemotright> I"
  2341         by (rule wf_prog_cdecl [THEN wf_cdeclE,simplified]) blast
  2342        (*  simplified: to rewrite \<langle>init c\<rangle> to In1r (init c) *) 
  2343       then obtain I' where
  2344         "\<lparr>prg=G,cls=C,lcl=empty\<rparr>\<turnstile>dom (locals (store ((set_lvars empty) s1))) 
  2345             \<guillemotright>In1r (init c)\<guillemotright> I'"
  2346           by (rule da_weakenE) simp
  2347       ultimately
  2348       obtain conf_s2: "s2\<Colon>\<preceq>(G, empty)" and error_free_s2: "error_free s2"
  2349         by (rule hyp_init_c [elim_format]) (simp add: error_free_empty)
  2350       have "abrupt s2 \<noteq> Some (Jump Ret)"
  2351       proof -
  2352         from s1_no_ret 
  2353         have "\<And> j. abrupt ((set_lvars empty) s1) \<noteq> Some (Jump j)"
  2354           by simp
  2355         moreover
  2356         from cls_C wf have "jumpNestingOkS {} (init c)"
  2357           by (rule wf_prog_cdecl [THEN wf_cdeclE])
  2358         ultimately 
  2359         show ?thesis
  2360           using eval_init wt_init_c wf
  2361           by - (rule eval_statement_no_jump 
  2362                      [where ?Env="\<lparr>prg=G,cls=C,lcl=empty\<rparr>"],simp+)
  2363       qed
  2364       with conf_s2 s3 conf_s1 eval_init
  2365       have "s3\<Colon>\<preceq>(G, L)"
  2366         by (cases s2,cases s1) (force dest: conforms_return eval_gext')
  2367       moreover from error_free_s2 s3
  2368       have "error_free s3"
  2369         by simp
  2370       moreover note wt
  2371       ultimately show ?thesis
  2372         by simp
  2373     qed
  2374   next
  2375     case (NewC s0 C s1 a s2 L accC T A)
  2376     note `G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s1`
  2377     note halloc = `G\<turnstile>s1 \<midarrow>halloc CInst C\<succ>a\<rightarrow> s2`
  2378     note hyp = `PROP ?TypeSafe (Norm s0) s1 (In1r (Init C)) \<diamondsuit>`
  2379     note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
  2380     moreover
  2381     note wt = `\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>In1l (NewC C)\<Colon>T`
  2382     then obtain is_cls_C: "is_class G C" and
  2383                        T: "T=Inl (Class C)"
  2384       by (rule wt_elim_cases) (auto dest: is_acc_classD)
  2385     hence "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>Init C\<Colon>\<surd>" by auto
  2386     moreover obtain I where 
  2387       "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2388           \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1r (Init C)\<guillemotright> I"
  2389       by (auto intro: da_Init [simplified] assigned.select_convs)
  2390      (* simplified: to rewrite \<langle>Init C\<rangle> to In1r (Init C) *)
  2391     ultimately 
  2392     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1"
  2393       by (rule hyp [elim_format]) simp 
  2394     from conf_s1 halloc wf is_cls_C
  2395     obtain halloc_type_safe: "s2\<Colon>\<preceq>(G, L)" 
  2396                              "(normal s2 \<longrightarrow> G,store s2\<turnstile>Addr a\<Colon>\<preceq>Class C)"
  2397       by (cases s2) (auto dest!: halloc_type_sound)
  2398     from halloc error_free_s1 
  2399     have "error_free s2"
  2400       by (rule error_free_halloc)
  2401     with halloc_type_safe T
  2402     show "s2\<Colon>\<preceq>(G, L) \<and> 
  2403           (normal s2 \<longrightarrow> G,L,store s2\<turnstile>In1l (NewC C)\<succ>In1 (Addr a)\<Colon>\<preceq>T)  \<and>
  2404           (error_free (Norm s0) = error_free s2)"
  2405       by auto
  2406   next
  2407     case (NewA s0 elT s1 e i s2 a s3 L accC T A)
  2408     note eval_init = `G\<turnstile>Norm s0 \<midarrow>init_comp_ty elT\<rightarrow> s1`
  2409     note eval_e = `G\<turnstile>s1 \<midarrow>e-\<succ>i\<rightarrow> s2`
  2410     note halloc = `G\<turnstile>abupd (check_neg i) s2\<midarrow>halloc Arr elT (the_Intg i)\<succ>a\<rightarrow> s3`
  2411     note hyp_init = `PROP ?TypeSafe (Norm s0) s1 (In1r (init_comp_ty elT)) \<diamondsuit>`
  2412     note hyp_size = `PROP ?TypeSafe s1 s2 (In1l e) (In1 i)`
  2413     note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
  2414     note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (New elT[e])\<Colon>T`
  2415     then obtain
  2416       wt_init: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>init_comp_ty elT\<Colon>\<surd>" and
  2417       wt_size: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-PrimT Integer" and
  2418             elT: "is_type G elT" and
  2419            T: "T=Inl (elT.[])"
  2420       by (rule wt_elim_cases) (auto intro: wt_init_comp_ty dest: is_acc_typeD)
  2421     from NewA.prems 
  2422     have da_e:"\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2423                  \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1l e\<guillemotright> A"
  2424       by (elim da_elim_cases) simp
  2425     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1"
  2426     proof -
  2427       note conf_s0 wt_init
  2428       moreover obtain I where
  2429         "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2430          \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1r (init_comp_ty elT)\<guillemotright> I"
  2431       proof (cases "\<exists>C. elT = Class C")
  2432         case True
  2433         thus ?thesis
  2434           by - (rule that, (auto intro: da_Init [simplified] 
  2435                                         assigned.select_convs
  2436                               simp add: init_comp_ty_def))
  2437          (* simplified: to rewrite \<langle>Init C\<rangle> to In1r (Init C) *)
  2438       next
  2439         case False
  2440         thus ?thesis
  2441         by - (rule that, (auto intro: da_Skip [simplified] 
  2442                                       assigned.select_convs
  2443                            simp add: init_comp_ty_def))
  2444          (* simplified: to rewrite \<langle>Skip\<rangle> to In1r (Skip) *)
  2445       qed
  2446       ultimately show thesis
  2447         by (rule hyp_init [elim_format]) (auto intro: that)
  2448     qed 
  2449     obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"
  2450     proof -
  2451       from eval_init 
  2452       have "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
  2453         by (rule dom_locals_eval_mono_elim)
  2454       with da_e 
  2455       obtain A' where
  2456        "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2457             \<turnstile> dom (locals (store s1)) \<guillemotright>In1l e\<guillemotright> A'"
  2458         by (rule da_weakenE)
  2459       with conf_s1 wt_size
  2460       show ?thesis
  2461         by (rule hyp_size [elim_format]) (simp add: that error_free_s1) 
  2462     qed
  2463     from conf_s2 have "abupd (check_neg i) s2\<Colon>\<preceq>(G, L)"
  2464       by (cases s2) auto
  2465     with halloc wf elT 
  2466     have halloc_type_safe:
  2467           "s3\<Colon>\<preceq>(G, L) \<and> (normal s3 \<longrightarrow> G,store s3\<turnstile>Addr a\<Colon>\<preceq>elT.[])"
  2468       by (cases s3) (auto dest!: halloc_type_sound)
  2469     from halloc error_free_s2
  2470     have "error_free s3"
  2471       by (auto dest: error_free_halloc)
  2472     with halloc_type_safe T
  2473     show "s3\<Colon>\<preceq>(G, L) \<and> 
  2474           (normal s3 \<longrightarrow> G,L,store s3\<turnstile>In1l (New elT[e])\<succ>In1 (Addr a)\<Colon>\<preceq>T) \<and>
  2475           (error_free (Norm s0) = error_free s3) "
  2476       by simp
  2477   next
  2478     case (Cast s0 e v s1 s2 castT L accC T A)
  2479     note `G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1`
  2480     note s2 = `s2 = abupd (raise_if (\<not> G,store s1\<turnstile>v fits castT) ClassCast) s1`
  2481     note hyp = `PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)`
  2482     note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
  2483     note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (Cast castT e)\<Colon>T`
  2484     then obtain eT
  2485       where wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-eT" and
  2486               eT: "G\<turnstile>eT\<preceq>? castT" and 
  2487                T: "T=Inl castT"
  2488       by (rule wt_elim_cases) auto
  2489     from Cast.prems 
  2490     have "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2491                  \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1l e\<guillemotright> A"
  2492       by (elim da_elim_cases) simp
  2493     with conf_s0 wt_e
  2494     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and
  2495            v_ok: "normal s1 \<longrightarrow> G,store s1\<turnstile>v\<Colon>\<preceq>eT" and
  2496       error_free_s1: "error_free s1"
  2497       by (rule hyp [elim_format]) simp
  2498     from conf_s1 s2 
  2499     have conf_s2: "s2\<Colon>\<preceq>(G, L)"
  2500       by (cases s1) simp
  2501     from error_free_s1 s2
  2502     have error_free_s2: "error_free s2"
  2503       by simp
  2504     {
  2505       assume norm_s2: "normal s2"
  2506       have "G,L,store s2\<turnstile>In1l (Cast castT e)\<succ>In1 v\<Colon>\<preceq>T"
  2507       proof -
  2508         from s2 norm_s2 have "normal s1"
  2509           by (cases s1) simp
  2510         with v_ok 
  2511         have "G,store s1\<turnstile>v\<Colon>\<preceq>eT"
  2512           by simp
  2513         with eT wf s2 T norm_s2
  2514         show ?thesis
  2515           by (cases s1) (auto dest: fits_conf)
  2516       qed
  2517     }
  2518     with conf_s2 error_free_s2
  2519     show "s2\<Colon>\<preceq>(G, L) \<and> 
  2520            (normal s2 \<longrightarrow> G,L,store s2\<turnstile>In1l (Cast castT e)\<succ>In1 v\<Colon>\<preceq>T)  \<and>
  2521            (error_free (Norm s0) = error_free s2)"
  2522       by blast
  2523   next
  2524     case (Inst s0 e v s1 b instT L accC T A)
  2525     note hyp = `PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)`
  2526     note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
  2527     from Inst.prems obtain eT
  2528     where wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-RefT eT"  and
  2529              T: "T=Inl (PrimT Boolean)" 
  2530       by (elim wt_elim_cases) simp
  2531     from Inst.prems 
  2532     have da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2533                  \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1l e\<guillemotright> A"
  2534       by (elim da_elim_cases) simp
  2535     from conf_s0 wt_e da_e
  2536     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and
  2537               v_ok: "normal s1 \<longrightarrow> G,store s1\<turnstile>v\<Colon>\<preceq>RefT eT" and
  2538       error_free_s1: "error_free s1"
  2539       by (rule hyp [elim_format]) simp
  2540     with T show ?case
  2541       by simp
  2542   next
  2543     case (Lit s v L accC T A)
  2544     then show ?case
  2545       by (auto elim!: wt_elim_cases 
  2546                intro: conf_litval simp add: empty_dt_def)
  2547   next
  2548     case (UnOp s0 e v s1 unop L accC T A)
  2549     note hyp = `PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)`
  2550     note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
  2551     note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (UnOp unop e)\<Colon>T`
  2552     then obtain eT
  2553       where    wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-eT" and
  2554             wt_unop: "wt_unop unop eT" and
  2555                   T: "T=Inl (PrimT (unop_type unop))" 
  2556       by (auto elim!: wt_elim_cases)
  2557     from UnOp.prems obtain A where
  2558        da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2559                   \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1l e\<guillemotright> A"
  2560       by (elim da_elim_cases) simp
  2561     from conf_s0 wt_e da_e
  2562     obtain     conf_s1: "s1\<Colon>\<preceq>(G, L)"  and
  2563                   wt_v: "normal s1 \<longrightarrow> G,store s1\<turnstile>v\<Colon>\<preceq>eT" and
  2564          error_free_s1: "error_free s1"
  2565       by (rule hyp [elim_format]) simp
  2566     from wt_v T wt_unop
  2567     have "normal s1\<longrightarrow>G,L,snd s1\<turnstile>In1l (UnOp unop e)\<succ>In1 (eval_unop unop v)\<Colon>\<preceq>T"
  2568       by (cases unop) auto
  2569     with conf_s1 error_free_s1
  2570     show "s1\<Colon>\<preceq>(G, L) \<and>
  2571      (normal s1 \<longrightarrow> G,L,snd s1\<turnstile>In1l (UnOp unop e)\<succ>In1 (eval_unop unop v)\<Colon>\<preceq>T) \<and>
  2572      error_free (Norm s0) = error_free s1"
  2573       by simp
  2574   next
  2575     case (BinOp s0 e1 v1 s1 binop e2 v2 s2 L accC T A)
  2576     note eval_e1 = `G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<rightarrow> s1`
  2577     note eval_e2 = `G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then In1l e2
  2578                              else In1r Skip)\<succ>\<rightarrow> (In1 v2, s2)`
  2579     note hyp_e1 = `PROP ?TypeSafe (Norm s0) s1 (In1l e1) (In1 v1)`
  2580     note hyp_e2 = `PROP ?TypeSafe       s1  s2 
  2581                    (if need_second_arg binop v1 then In1l e2 else In1r Skip) 
  2582                    (In1 v2)`
  2583     note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
  2584     note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (BinOp binop e1 e2)\<Colon>T`
  2585     then obtain e1T e2T where
  2586          wt_e1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e1\<Colon>-e1T" and
  2587          wt_e2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e2\<Colon>-e2T" and
  2588       wt_binop: "wt_binop G binop e1T e2T" and
  2589              T: "T=Inl (PrimT (binop_type binop))"
  2590       by (elim wt_elim_cases) simp
  2591     have wt_Skip: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>Skip\<Colon>\<surd>"
  2592       by simp
  2593     obtain S where
  2594       daSkip: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2595                   \<turnstile> dom (locals (store s1)) \<guillemotright>In1r Skip\<guillemotright> S"
  2596       by (auto intro: da_Skip [simplified] assigned.select_convs)
  2597     note da = `\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store ((Norm s0::state)))) 
  2598                   \<guillemotright>\<langle>BinOp binop e1 e2\<rangle>\<^sub>e\<guillemotright> A`
  2599     then obtain E1 where
  2600       da_e1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2601                   \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1l e1\<guillemotright> E1"
  2602       by (elim da_elim_cases) simp+
  2603     from conf_s0 wt_e1 da_e1
  2604     obtain      conf_s1: "s1\<Colon>\<preceq>(G, L)"  and
  2605                   wt_v1: "normal s1 \<longrightarrow> G,store s1\<turnstile>v1\<Colon>\<preceq>e1T" and
  2606           error_free_s1: "error_free s1"
  2607       by (rule hyp_e1 [elim_format]) simp
  2608     from wt_binop T
  2609     have conf_v:
  2610       "G,L,snd s2\<turnstile>In1l (BinOp binop e1 e2)\<succ>In1 (eval_binop binop v1 v2)\<Colon>\<preceq>T"
  2611       by (cases binop) auto
  2612     -- {* Note that we don't use the information that v1 really is compatible 
  2613           with the expected type e1T and v2 is compatible with e2T, 
  2614           because @{text eval_binop} will anyway produce an output of 
  2615           the right type.
  2616           So evaluating the addition of an integer with a string is type
  2617           safe. This is a little bit annoying since we may regard such a
  2618           behaviour as not type safe.
  2619           If we want to avoid this we can redefine @{text eval_binop} so that
  2620           it only produces a output of proper type if it is assigned to 
  2621           values of the expected types, and arbitrary if the inputs have 
  2622           unexpected types. The proof can easily be adapted since we
  2623           have the hypothesis that the values have a proper type.
  2624           This also applies to unary operations.
  2625        *}
  2626     from eval_e1 have 
  2627       s0_s1:"dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
  2628       by (rule dom_locals_eval_mono_elim)
  2629     show "s2\<Colon>\<preceq>(G, L) \<and>
  2630           (normal s2 \<longrightarrow>
  2631         G,L,snd s2\<turnstile>In1l (BinOp binop e1 e2)\<succ>In1 (eval_binop binop v1 v2)\<Colon>\<preceq>T) \<and>
  2632           error_free (Norm s0) = error_free s2"
  2633     proof (cases "normal s1")
  2634       case False
  2635       with eval_e2 have "s2=s1" by auto
  2636       with conf_s1 error_free_s1 False show ?thesis
  2637         by auto
  2638     next
  2639       case True
  2640       note normal_s1 = this
  2641       show ?thesis 
  2642       proof (cases "need_second_arg binop v1")
  2643         case False
  2644         with normal_s1 eval_e2 have "s2=s1"
  2645           by (cases s1) (simp, elim eval_elim_cases,simp)
  2646         with conf_s1 conf_v error_free_s1
  2647         show ?thesis by simp
  2648       next
  2649         case True
  2650         note need_second_arg = this
  2651         with hyp_e2 
  2652         have hyp_e2': "PROP ?TypeSafe s1 s2 (In1l e2) (In1 v2)" by simp
  2653         from da wt_e1 wt_e2 wt_binop conf_s0 normal_s1 eval_e1 
  2654           wt_v1 [rule_format,OF normal_s1] wf
  2655         obtain E2 where
  2656           "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>In1l e2\<guillemotright> E2"
  2657           by (rule da_e2_BinOp [elim_format]) 
  2658              (auto simp add: need_second_arg )
  2659         with conf_s1 wt_e2 
  2660         obtain "s2\<Colon>\<preceq>(G, L)" and "error_free s2"
  2661           by (rule hyp_e2' [elim_format]) (simp add: error_free_s1)
  2662         with conf_v show ?thesis by simp
  2663       qed
  2664     qed
  2665   next
  2666     case (Super s L accC T A)
  2667     note conf_s = `Norm s\<Colon>\<preceq>(G, L)`
  2668     note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l Super\<Colon>T`
  2669     then obtain C c where
  2670              C: "L This = Some (Class C)" and
  2671        neq_Obj: "C\<noteq>Object" and
  2672          cls_C: "class G C = Some c" and
  2673              T: "T=Inl (Class (super c))"
  2674       by (rule wt_elim_cases) auto
  2675     from Super.prems
  2676     obtain "This \<in> dom (locals s)"
  2677       by (elim da_elim_cases) simp
  2678     with conf_s C  have "G,s\<turnstile>val_this s\<Colon>\<preceq>Class C"
  2679       by (auto dest: conforms_localD [THEN wlconfD])
  2680     with neq_Obj cls_C wf
  2681     have "G,s\<turnstile>val_this s\<Colon>\<preceq>Class (super c)"
  2682       by (auto intro: conf_widen
  2683                 dest: subcls_direct[THEN widen.subcls])
  2684     with T conf_s
  2685     show "Norm s\<Colon>\<preceq>(G, L) \<and>
  2686            (normal (Norm s) \<longrightarrow> 
  2687               G,L,store (Norm s)\<turnstile>In1l Super\<succ>In1 (val_this s)\<Colon>\<preceq>T) \<and>
  2688            (error_free (Norm s) = error_free (Norm s))"
  2689       by simp
  2690   next
  2691     case (Acc s0 v w upd s1 L accC T A)
  2692     note hyp = `PROP ?TypeSafe (Norm s0) s1 (In2 v) (In2 (w,upd))`
  2693     note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
  2694     from Acc.prems obtain vT where
  2695       wt_v: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>v\<Colon>=vT" and
  2696          T: "T=Inl vT"
  2697       by (elim wt_elim_cases) simp
  2698     from Acc.prems obtain V where
  2699       da_v: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2700                   \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In2 v\<guillemotright> V"
  2701       by (cases "\<exists> n. v=LVar n") (insert da.LVar, auto elim!: da_elim_cases)
  2702     {
  2703       fix n assume lvar: "v=LVar n"
  2704       have "locals (store s1) n \<noteq> None"
  2705       proof -
  2706         from Acc.prems lvar have 
  2707           "n \<in> dom (locals s0)"
  2708           by (cases "\<exists> n. v=LVar n") (auto elim!: da_elim_cases)
  2709         also
  2710         have "dom (locals s0) \<subseteq> dom (locals (store s1))"
  2711         proof -
  2712           from `G\<turnstile>Norm s0 \<midarrow>v=\<succ>(w, upd)\<rightarrow> s1`
  2713           show ?thesis
  2714             by (rule dom_locals_eval_mono_elim) simp
  2715         qed
  2716         finally show ?thesis
  2717           by blast
  2718       qed
  2719     } note lvar_in_locals = this 
  2720     from conf_s0 wt_v da_v
  2721     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)"
  2722       and  conf_var: "(normal s1 \<longrightarrow> G,L,store s1\<turnstile>In2 v\<succ>In2 (w, upd)\<Colon>\<preceq>Inl vT)"
  2723       and  error_free_s1: "error_free s1"
  2724       by (rule hyp [elim_format]) simp
  2725     from lvar_in_locals conf_var T
  2726     have "(normal s1 \<longrightarrow> G,L,store s1\<turnstile>In1l (Acc v)\<succ>In1 w\<Colon>\<preceq>T)"
  2727       by (cases "\<exists> n. v=LVar n") auto
  2728     with conf_s1 error_free_s1 show ?case
  2729       by simp
  2730   next
  2731     case (Ass s0 var w upd s1 e v s2 L accC T A)
  2732     note eval_var = `G\<turnstile>Norm s0 \<midarrow>var=\<succ>(w, upd)\<rightarrow> s1`
  2733     note eval_e = `G\<turnstile>s1 \<midarrow>e-\<succ>v\<rightarrow> s2`
  2734     note hyp_var = `PROP ?TypeSafe (Norm s0) s1 (In2 var) (In2 (w,upd))`
  2735     note hyp_e = `PROP ?TypeSafe s1 s2 (In1l e) (In1 v)`
  2736     note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
  2737     note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (var:=e)\<Colon>T`
  2738     then obtain varT eT where
  2739          wt_var: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>var\<Colon>=varT" and
  2740            wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-eT" and
  2741           widen: "G\<turnstile>eT\<preceq>varT" and
  2742               T: "T=Inl eT"
  2743       by (rule wt_elim_cases) auto
  2744     show "assign upd v s2\<Colon>\<preceq>(G, L) \<and>
  2745            (normal (assign upd v s2) \<longrightarrow>
  2746             G,L,store (assign upd v s2)\<turnstile>In1l (var:=e)\<succ>In1 v\<Colon>\<preceq>T) \<and>
  2747       (error_free (Norm s0) = error_free (assign upd v s2))"
  2748     proof (cases "\<exists> vn. var=LVar vn")
  2749       case False
  2750       with Ass.prems
  2751       obtain V E where
  2752         da_var: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2753                    \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In2 var\<guillemotright> V" and
  2754         da_e:   "\<lparr>prg=G,cls=accC,lcl=L\<rparr> \<turnstile> nrm V \<guillemotright>In1l e\<guillemotright> E"
  2755         by (elim da_elim_cases) simp+
  2756       from conf_s0 wt_var da_var 
  2757       obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" 
  2758         and  conf_var: "normal s1 
  2759                          \<longrightarrow> G,L,store s1\<turnstile>In2 var\<succ>In2 (w, upd)\<Colon>\<preceq>Inl varT"
  2760         and  error_free_s1: "error_free s1"
  2761         by (rule hyp_var [elim_format]) simp
  2762       show ?thesis
  2763       proof (cases "normal s1")
  2764         case False
  2765         with eval_e have "s2=s1" by auto
  2766         with False have "assign upd v s2=s1"
  2767           by simp
  2768         with conf_s1 error_free_s1 False show ?thesis
  2769           by auto
  2770       next
  2771         case True
  2772         note normal_s1=this
  2773         obtain A' where "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2774                          \<turnstile> dom (locals (store s1)) \<guillemotright>In1l e\<guillemotright> A'"
  2775         proof -
  2776           from eval_var wt_var da_var wf normal_s1
  2777           have "nrm V \<subseteq>  dom (locals (store s1))"
  2778             by (cases rule: da_good_approxE') iprover
  2779           with da_e show thesis
  2780             by (rule da_weakenE) (rule that)
  2781         qed
  2782         with conf_s1 wt_e 
  2783         obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and 
  2784           conf_v: "normal s2 \<longrightarrow> G,store s2\<turnstile>v\<Colon>\<preceq>eT" and
  2785           error_free_s2: "error_free s2"
  2786           by (rule hyp_e [elim_format]) (simp add: error_free_s1)
  2787         show ?thesis 
  2788         proof (cases "normal s2")
  2789           case False
  2790           with conf_s2 error_free_s2 
  2791           show ?thesis
  2792             by auto
  2793         next
  2794           case True
  2795           from True conf_v
  2796           have conf_v_eT: "G,store s2\<turnstile>v\<Colon>\<preceq>eT"
  2797             by simp
  2798           with widen wf
  2799           have conf_v_varT: "G,store s2\<turnstile>v\<Colon>\<preceq>varT"
  2800             by (auto intro: conf_widen)
  2801           from normal_s1 conf_var
  2802           have "G,L,store s1\<turnstile>In2 var\<succ>In2 (w, upd)\<Colon>\<preceq>Inl varT"
  2803             by simp
  2804           then 
  2805           have conf_assign:  "store s1\<le>|upd\<preceq>varT\<Colon>\<preceq>(G, L)" 
  2806             by (simp add: rconf_def)
  2807           from conf_v_eT conf_v_varT conf_assign normal_s1 True wf eval_var 
  2808             eval_e T conf_s2 error_free_s2
  2809           show ?thesis
  2810             by (cases s1, cases s2) 
  2811                (auto dest!: Ass_lemma simp add: assign_conforms_def)
  2812         qed
  2813       qed
  2814     next
  2815       case True
  2816       then obtain vn where vn: "var=LVar vn"
  2817         by blast
  2818       with Ass.prems
  2819       obtain E where
  2820         da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr> 
  2821                    \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1l e\<guillemotright> E"
  2822         by (elim da_elim_cases) simp+
  2823       from da.LVar vn obtain V where
  2824         da_var: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2825                    \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In2 var\<guillemotright> V"
  2826         by auto
  2827       obtain E' where
  2828         da_e': "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2829                    \<turnstile> dom (locals (store s1)) \<guillemotright>In1l e\<guillemotright> E'"
  2830       proof -
  2831         have "dom (locals (store ((Norm s0)::state))) 
  2832                 \<subseteq> dom (locals (store (s1)))"
  2833           by (rule dom_locals_eval_mono_elim) (rule Ass.hyps)
  2834         with da_e show thesis
  2835           by (rule da_weakenE) (rule that)
  2836       qed
  2837       from conf_s0 wt_var da_var 
  2838       obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" 
  2839         and  conf_var: "normal s1 
  2840                          \<longrightarrow> G,L,store s1\<turnstile>In2 var\<succ>In2 (w, upd)\<Colon>\<preceq>Inl varT"
  2841         and  error_free_s1: "error_free s1"
  2842         by (rule hyp_var [elim_format]) simp
  2843       show ?thesis
  2844       proof (cases "normal s1")
  2845         case False
  2846         with eval_e have "s2=s1" by auto
  2847         with False have "assign upd v s2=s1"
  2848           by simp
  2849         with conf_s1 error_free_s1 False show ?thesis
  2850           by auto
  2851       next
  2852         case True
  2853         note normal_s1 = this
  2854         from conf_s1 wt_e da_e'
  2855         obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and 
  2856           conf_v: "normal s2 \<longrightarrow> G,store s2\<turnstile>v\<Colon>\<preceq>eT" and
  2857           error_free_s2: "error_free s2"
  2858           by (rule hyp_e [elim_format]) (simp add: error_free_s1)
  2859         show ?thesis 
  2860         proof (cases "normal s2")
  2861           case False
  2862           with conf_s2 error_free_s2 
  2863           show ?thesis
  2864             by auto
  2865         next
  2866           case True
  2867           from True conf_v
  2868           have conf_v_eT: "G,store s2\<turnstile>v\<Colon>\<preceq>eT"
  2869             by simp
  2870           with widen wf
  2871           have conf_v_varT: "G,store s2\<turnstile>v\<Colon>\<preceq>varT"
  2872             by (auto intro: conf_widen)
  2873           from normal_s1 conf_var
  2874           have "G,L,store s1\<turnstile>In2 var\<succ>In2 (w, upd)\<Colon>\<preceq>Inl varT"
  2875             by simp
  2876           then 
  2877           have conf_assign:  "store s1\<le>|upd\<preceq>varT\<Colon>\<preceq>(G, L)" 
  2878             by (simp add: rconf_def)
  2879           from conf_v_eT conf_v_varT conf_assign normal_s1 True wf eval_var 
  2880             eval_e T conf_s2 error_free_s2
  2881           show ?thesis
  2882             by (cases s1, cases s2) 
  2883                (auto dest!: Ass_lemma simp add: assign_conforms_def)
  2884         qed
  2885       qed
  2886     qed
  2887   next
  2888     case (Cond s0 e0 b s1 e1 e2 v s2 L accC T A)
  2889     note eval_e0 = `G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1`
  2890     note eval_e1_e2 = `G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<rightarrow> s2`
  2891     note hyp_e0 = `PROP ?TypeSafe (Norm s0) s1 (In1l e0) (In1 b)`
  2892     note hyp_if = `PROP ?TypeSafe s1 s2
  2893                        (In1l (if the_Bool b then e1 else e2)) (In1 v)`
  2894     note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
  2895     note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (e0 ? e1 : e2)\<Colon>T`
  2896     then obtain T1 T2 statT where
  2897       wt_e0: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e0\<Colon>-PrimT Boolean" and
  2898       wt_e1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e1\<Colon>-T1" and
  2899       wt_e2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e2\<Colon>-T2" and 
  2900       statT: "G\<turnstile>T1\<preceq>T2 \<and> statT = T2  \<or>  G\<turnstile>T2\<preceq>T1 \<and> statT =  T1" and
  2901       T    : "T=Inl statT"
  2902       by (rule wt_elim_cases) auto
  2903     with Cond.prems obtain E0 E1 E2 where
  2904          da_e0: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2905                   \<turnstile> dom (locals (store ((Norm s0)::state))) 
  2906                       \<guillemotright>In1l e0\<guillemotright> E0" and
  2907          da_e1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2908                   \<turnstile> (dom (locals (store ((Norm s0)::state))) 
  2909                          \<union> assigns_if True e0) \<guillemotright>In1l e1\<guillemotright> E1" and
  2910          da_e2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  2911                   \<turnstile> (dom (locals (store ((Norm s0)::state))) 
  2912                         \<union> assigns_if False e0) \<guillemotright>In1l e2\<guillemotright> E2"
  2913        by (elim da_elim_cases) simp+
  2914     from conf_s0 wt_e0 da_e0  
  2915     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1" 
  2916       by (rule hyp_e0 [elim_format]) simp
  2917     show "s2\<Colon>\<preceq>(G, L) \<and>
  2918            (normal s2 \<longrightarrow> G,L,store s2\<turnstile>In1l (e0 ? e1 : e2)\<succ>In1 v\<Colon>\<preceq>T) \<and>
  2919            (error_free (Norm s0) = error_free s2)"
  2920     proof (cases "normal s1")
  2921       case False
  2922       with eval_e1_e2 have "s2=s1" by auto
  2923       with conf_s1 error_free_s1 False show ?thesis
  2924         by auto
  2925     next
  2926       case True
  2927       have s0_s1: "dom (locals (store ((Norm s0)::state))) 
  2928                     \<union> assigns_if (the_Bool b) e0 \<subseteq> dom (locals (store s1))"
  2929       proof -
  2930         from eval_e0 have 
  2931           "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
  2932           by (rule dom_locals_eval_mono_elim)
  2933         moreover
  2934         from eval_e0 True wt_e0 
  2935         have "assigns_if (the_Bool b) e0 \<subseteq> dom (locals (store s1))"
  2936           by (rule assigns_if_good_approx') 
  2937         ultimately show ?thesis by (rule Un_least)
  2938       qed 
  2939       show ?thesis
  2940       proof (cases "the_Bool b")
  2941         case True
  2942         with hyp_if have hyp_e1: "PROP ?TypeSafe s1 s2 (In1l e1) (In1 v)" 
  2943           by simp
  2944         from da_e1 s0_s1 True obtain E1' where
  2945           "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s1)))\<guillemotright>In1l e1\<guillemotright> E1'"
  2946           by - (rule da_weakenE, auto iff del: Un_subset_iff le_sup_iff)
  2947         with conf_s1 wt_e1
  2948         obtain 
  2949           "s2\<Colon>\<preceq>(G, L)"
  2950           "(normal s2 \<longrightarrow> G,L,store s2\<turnstile>In1l e1\<succ>In1 v\<Colon>\<preceq>Inl T1)"
  2951           "error_free s2"            
  2952           by (rule hyp_e1 [elim_format]) (simp add: error_free_s1)
  2953         moreover
  2954         from statT  
  2955         have "G\<turnstile>T1\<preceq>statT"
  2956           by auto
  2957         ultimately show ?thesis
  2958           using T wf by auto
  2959       next
  2960         case False
  2961         with hyp_if have hyp_e2: "PROP ?TypeSafe s1 s2 (In1l e2) (In1 v)" 
  2962           by simp
  2963         from da_e2 s0_s1 False obtain E2' where
  2964           "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s1)))\<guillemotright>In1l e2\<guillemotright> E2'"
  2965           by - (rule da_weakenE, auto iff del: Un_subset_iff le_sup_iff)
  2966         with conf_s1 wt_e2
  2967         obtain 
  2968           "s2\<Colon>\<preceq>(G, L)"
  2969           "(normal s2 \<longrightarrow> G,L,store s2\<turnstile>In1l e2\<succ>In1 v\<Colon>\<preceq>Inl T2)"
  2970           "error_free s2"            
  2971           by (rule hyp_e2 [elim_format]) (simp add: error_free_s1)
  2972         moreover
  2973         from statT  
  2974         have "G\<turnstile>T2\<preceq>statT"
  2975           by auto
  2976         ultimately show ?thesis
  2977           using T wf by auto
  2978       qed
  2979     qed
  2980   next
  2981     case (Call s0 e a s1 args vs s2 invDeclC mode statT mn pTs' s3 s3' accC'
  2982            v s4 L accC T A)
  2983     note eval_e = `G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<rightarrow> s1`
  2984     note eval_args = `G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<rightarrow> s2`
  2985     note invDeclC = `invDeclC 
  2986                       = invocation_declclass G mode (store s2) a statT 
  2987                            \<lparr>name = mn, parTs = pTs'\<rparr>`
  2988     note init_lvars =
  2989       `s3 = init_lvars G invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> mode a vs s2`
  2990     note check = `s3' =
  2991         check_method_access G accC' statT mode \<lparr>name = mn, parTs = pTs'\<rparr> a s3`
  2992     note eval_methd =
  2993       `G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>-\<succ>v\<rightarrow> s4`
  2994     note hyp_e = `PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 a)`
  2995     note hyp_args = `PROP ?TypeSafe s1 s2 (In3 args) (In3 vs)`
  2996     note hyp_methd = `PROP ?TypeSafe s3' s4 
  2997         (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)) (In1 v)`
  2998     note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
  2999     note wt = `\<lparr>prg=G, cls=accC, lcl=L\<rparr>
  3000         \<turnstile>In1l ({accC',statT,mode}e\<cdot>mn( {pTs'}args))\<Colon>T`
  3001     from wt obtain pTs statDeclT statM where
  3002                  wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT" and
  3003               wt_args: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>args\<Colon>\<doteq>pTs" and
  3004                 statM: "max_spec G accC statT \<lparr>name=mn,parTs=pTs\<rparr> 
  3005                          = {((statDeclT,statM),pTs')}" and
  3006                  mode: "mode = invmode statM e" and
  3007                     T: "T =Inl (resTy statM)" and
  3008         eq_accC_accC': "accC=accC'"
  3009       by (rule wt_elim_cases) fastsimp+
  3010     from Call.prems obtain E where
  3011       da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  3012                \<turnstile> (dom (locals (store ((Norm s0)::state))))\<guillemotright>In1l e\<guillemotright> E" and
  3013       da_args: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> nrm E \<guillemotright>In3 args\<guillemotright> A" 
  3014       by (elim da_elim_cases) simp
  3015     from conf_s0 wt_e da_e  
  3016     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and
  3017            conf_a: "normal s1 \<Longrightarrow> G, store s1\<turnstile>a\<Colon>\<preceq>RefT statT" and
  3018            error_free_s1: "error_free s1" 
  3019       by (rule hyp_e [elim_format]) simp
  3020     { 
  3021       assume abnormal_s2: "\<not> normal s2"
  3022       have "set_lvars (locals (store s2)) s4 = s2"
  3023       proof -
  3024         from abnormal_s2 init_lvars 
  3025         obtain keep_abrupt: "abrupt s3 = abrupt s2" and
  3026              "store s3 = store (init_lvars G invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> 
  3027                                             mode a vs s2)" 
  3028           by (auto simp add: init_lvars_def2)
  3029         moreover
  3030         from keep_abrupt abnormal_s2 check
  3031         have eq_s3'_s3: "s3'=s3" 
  3032           by (auto simp add: check_method_access_def Let_def)
  3033         moreover
  3034         from eq_s3'_s3 abnormal_s2 keep_abrupt eval_methd
  3035         have "s4=s3'"
  3036           by auto
  3037         ultimately show
  3038           "set_lvars (locals (store s2)) s4 = s2"
  3039           by (cases s2,cases s3) (simp add: init_lvars_def2)
  3040       qed
  3041     } note propagate_abnormal_s2 = this
  3042     show "(set_lvars (locals (store s2))) s4\<Colon>\<preceq>(G, L) \<and>
  3043            (normal ((set_lvars (locals (store s2))) s4) \<longrightarrow>
  3044              G,L,store ((set_lvars (locals (store s2))) s4)
  3045                \<turnstile>In1l ({accC',statT,mode}e\<cdot>mn( {pTs'}args))\<succ>In1 v\<Colon>\<preceq>T) \<and>
  3046            (error_free (Norm s0) =
  3047                 error_free ((set_lvars (locals (store s2))) s4))"
  3048     proof (cases "normal s1")
  3049       case False
  3050       with eval_args have "s2=s1" by auto
  3051       with False propagate_abnormal_s2 conf_s1 error_free_s1 
  3052       show ?thesis
  3053         by auto
  3054     next
  3055       case True
  3056       note normal_s1 = this
  3057       obtain A' where 
  3058         "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>In3 args\<guillemotright> A'"
  3059       proof -
  3060         from eval_e wt_e da_e wf normal_s1
  3061         have "nrm E \<subseteq>  dom (locals (store s1))"
  3062           by (cases rule: da_good_approxE') iprover
  3063         with da_args show thesis
  3064           by (rule da_weakenE) (rule that)
  3065       qed
  3066       with conf_s1 wt_args 
  3067       obtain    conf_s2: "s2\<Colon>\<preceq>(G, L)" and
  3068               conf_args: "normal s2 
  3069                          \<Longrightarrow>  list_all2 (conf G (store s2)) vs pTs" and
  3070           error_free_s2: "error_free s2" 
  3071         by (rule hyp_args [elim_format]) (simp add: error_free_s1)
  3072       from error_free_s2 init_lvars
  3073       have error_free_s3: "error_free s3"
  3074         by (auto simp add: init_lvars_def2)
  3075       from statM 
  3076       obtain
  3077         statM': "(statDeclT,statM)\<in>mheads G accC statT \<lparr>name=mn,parTs=pTs'\<rparr>" and
  3078         pTs_widen: "G\<turnstile>pTs[\<preceq>]pTs'"
  3079         by (blast dest: max_spec2mheads)
  3080       from check
  3081       have eq_store_s3'_s3: "store s3'=store s3"
  3082         by (cases s3) (simp add: check_method_access_def Let_def)
  3083       obtain invC
  3084         where invC: "invC = invocation_class mode (store s2) a statT"
  3085         by simp
  3086       with init_lvars
  3087       have invC': "invC = (invocation_class mode (store s3) a statT)"
  3088         by (cases s2,cases mode) (auto simp add: init_lvars_def2 )
  3089       show ?thesis
  3090       proof (cases "normal s2")
  3091         case False
  3092         with propagate_abnormal_s2 conf_s2 error_free_s2
  3093         show ?thesis
  3094           by auto
  3095       next
  3096         case True
  3097         note normal_s2 = True
  3098         with normal_s1 conf_a eval_args 
  3099         have conf_a_s2: "G, store s2\<turnstile>a\<Colon>\<preceq>RefT statT"
  3100           by (auto dest: eval_gext intro: conf_gext)
  3101         show ?thesis
  3102         proof (cases "a=Null \<longrightarrow> is_static statM")
  3103           case False
  3104           then obtain not_static: "\<not> is_static statM" and Null: "a=Null" 
  3105             by blast
  3106           with normal_s2 init_lvars mode
  3107           obtain np: "abrupt s3 = Some (Xcpt (Std NullPointer))" and
  3108                      "store s3 = store (init_lvars G invDeclC 
  3109                                        \<lparr>name = mn, parTs = pTs'\<rparr> mode a vs s2)"
  3110             by (auto simp add: init_lvars_def2)
  3111           moreover
  3112           from np check
  3113           have eq_s3'_s3: "s3'=s3" 
  3114             by (auto simp add: check_method_access_def Let_def)
  3115           moreover
  3116           from eq_s3'_s3 np eval_methd
  3117           have "s4=s3'"
  3118             by auto
  3119           ultimately have
  3120             "set_lvars (locals (store s2)) s4 
  3121             = (Some (Xcpt (Std NullPointer)),store s2)"
  3122             by (cases s2,cases s3) (simp add: init_lvars_def2)
  3123           with conf_s2 error_free_s2
  3124           show ?thesis
  3125             by (cases s2) (auto dest: conforms_NormI)
  3126         next
  3127           case True
  3128           with mode have notNull: "mode = IntVir \<longrightarrow> a \<noteq> Null"
  3129             by (auto dest!: Null_staticD)
  3130           with conf_s2 conf_a_s2 wf invC  
  3131           have dynT_prop: "G\<turnstile>mode\<rightarrow>invC\<preceq>statT"
  3132             by (cases s2) (auto intro: DynT_propI)
  3133           with wt_e statM' invC mode wf 
  3134           obtain dynM where 
  3135             dynM: "dynlookup G statT invC  \<lparr>name=mn,parTs=pTs'\<rparr> = Some dynM" and
  3136             acc_dynM: "G \<turnstile>Methd  \<lparr>name=mn,parTs=pTs'\<rparr> dynM 
  3137                             in invC dyn_accessible_from accC"
  3138             by (force dest!: call_access_ok)
  3139           with invC' check eq_accC_accC'
  3140           have eq_s3'_s3: "s3'=s3"
  3141             by (auto simp add: check_method_access_def Let_def)
  3142           from dynT_prop wf wt_e statM' mode invC invDeclC dynM 
  3143           obtain 
  3144             wf_dynM: "wf_mdecl G invDeclC (\<lparr>name=mn,parTs=pTs'\<rparr>,mthd dynM)" and
  3145               dynM': "methd G invDeclC \<lparr>name=mn,parTs=pTs'\<rparr> = Some dynM" and
  3146             iscls_invDeclC: "is_class G invDeclC" and
  3147                  invDeclC': "invDeclC = declclass dynM" and
  3148               invC_widen: "G\<turnstile>invC\<preceq>\<^sub>C invDeclC" and
  3149              resTy_widen: "G\<turnstile>resTy dynM\<preceq>resTy statM" and
  3150             is_static_eq: "is_static dynM = is_static statM" and
  3151             involved_classes_prop:
  3152              "(if invmode statM e = IntVir
  3153                then \<forall>statC. statT = ClassT statC \<longrightarrow> G\<turnstile>invC\<preceq>\<^sub>C statC
  3154                else ((\<exists>statC. statT = ClassT statC \<and> G\<turnstile>statC\<preceq>\<^sub>C invDeclC) \<or>
  3155                      (\<forall>statC. statT \<noteq> ClassT statC \<and> invDeclC = Object)) \<and>
  3156                       statDeclT = ClassT invDeclC)"
  3157             by (cases rule: DynT_mheadsE) simp
  3158           obtain L' where 
  3159            L':"L'=(\<lambda> k. 
  3160                  (case k of
  3161                     EName e
  3162                     \<Rightarrow> (case e of 
  3163                           VNam v 
  3164                           \<Rightarrow>(table_of (lcls (mbody (mthd dynM)))
  3165                              (pars (mthd dynM)[\<mapsto>]pTs')) v
  3166                         | Res \<Rightarrow> Some (resTy dynM))
  3167                   | This \<Rightarrow> if is_static statM 
  3168                             then None else Some (Class invDeclC)))"
  3169             by simp
  3170           from wf_dynM [THEN wf_mdeclD1, THEN conjunct1] normal_s2 conf_s2 wt_e
  3171             wf eval_args conf_a mode notNull wf_dynM involved_classes_prop
  3172           have conf_s3: "s3\<Colon>\<preceq>(G,L')"
  3173             apply - 
  3174                (* FIXME confomrs_init_lvars should be 
  3175                   adjusted to be more directy applicable *)
  3176             apply (drule conforms_init_lvars [of G invDeclC 
  3177                     "\<lparr>name=mn,parTs=pTs'\<rparr>" dynM "store s2" vs pTs "abrupt s2" 
  3178                     L statT invC a "(statDeclT,statM)" e])
  3179             apply (rule wf)
  3180             apply (rule conf_args,assumption)
  3181             apply (simp add: pTs_widen)
  3182             apply (cases s2,simp)
  3183             apply (rule dynM')
  3184             apply (force dest: ty_expr_is_type)
  3185             apply (rule invC_widen)
  3186             apply (force intro: conf_gext dest: eval_gext)
  3187             apply simp
  3188             apply simp
  3189             apply (simp add: invC)
  3190             apply (simp add: invDeclC)
  3191             apply (simp add: normal_s2)
  3192             apply (cases s2, simp add: L' init_lvars
  3193                              cong add: lname.case_cong ename.case_cong)
  3194             done
  3195           with eq_s3'_s3 
  3196           have conf_s3': "s3'\<Colon>\<preceq>(G,L')" by simp
  3197           moreover
  3198           from  is_static_eq wf_dynM L'
  3199           obtain mthdT where
  3200             "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>
  3201                \<turnstile>Body invDeclC (stmt (mbody (mthd dynM)))\<Colon>-mthdT" and
  3202             mthdT_widen: "G\<turnstile>mthdT\<preceq>resTy dynM"
  3203             by - (drule wf_mdecl_bodyD,
  3204                  auto simp add: callee_lcl_def  
  3205                       cong add: lname.case_cong ename.case_cong)
  3206           with dynM' iscls_invDeclC invDeclC'
  3207           have
  3208             "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>
  3209                \<turnstile>(Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)\<Colon>-mthdT"
  3210             by (auto intro: wt.Methd)
  3211           moreover
  3212           obtain M where 
  3213             "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr> 
  3214                \<turnstile> dom (locals (store s3')) 
  3215                   \<guillemotright>In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)\<guillemotright> M"
  3216           proof -
  3217             from wf_dynM
  3218             obtain M' where
  3219               da_body: 
  3220               "\<lparr>prg=G, cls=invDeclC
  3221                ,lcl=callee_lcl invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> (mthd dynM)
  3222                \<rparr> \<turnstile> parameters (mthd dynM) \<guillemotright>\<langle>stmt (mbody (mthd dynM))\<rangle>\<guillemotright> M'" and
  3223               res: "Result \<in> nrm M'"
  3224               by (rule wf_mdeclE) iprover
  3225             from da_body is_static_eq L' have
  3226               "\<lparr>prg=G, cls=invDeclC,lcl=L'\<rparr> 
  3227                  \<turnstile> parameters (mthd dynM) \<guillemotright>\<langle>stmt (mbody (mthd dynM))\<rangle>\<guillemotright> M'"
  3228               by (simp add: callee_lcl_def  
  3229                   cong add: lname.case_cong ename.case_cong)
  3230             moreover have "parameters (mthd dynM) \<subseteq>  dom (locals (store s3'))"
  3231             proof -
  3232               from is_static_eq 
  3233               have "(invmode (mthd dynM) e) = (invmode statM e)"
  3234                 by (simp add: invmode_def)
  3235               moreover
  3236               have "length (pars (mthd dynM)) = length vs" 
  3237               proof -
  3238                 from normal_s2 conf_args
  3239                 have "length vs = length pTs"
  3240                   by (simp add: list_all2_def)
  3241                 also from pTs_widen
  3242                 have "\<dots> = length pTs'"
  3243                   by (simp add: widens_def list_all2_def)
  3244                 also from wf_dynM
  3245                 have "\<dots> = length (pars (mthd dynM))"
  3246                   by (simp add: wf_mdecl_def wf_mhead_def)
  3247                 finally show ?thesis ..
  3248               qed
  3249               moreover note init_lvars dynM' is_static_eq normal_s2 mode 
  3250               ultimately
  3251               have "parameters (mthd dynM) = dom (locals (store s3))"
  3252                 using dom_locals_init_lvars 
  3253                   [of "mthd dynM" G invDeclC "\<lparr>name=mn,parTs=pTs'\<rparr>" vs e a s2]
  3254                 by simp
  3255               also from check
  3256               have "dom (locals (store s3)) \<subseteq>  dom (locals (store s3'))"
  3257                 by (simp add:  eq_s3'_s3)
  3258               finally show ?thesis .
  3259             qed
  3260             ultimately obtain M2 where
  3261               da:
  3262               "\<lparr>prg=G, cls=invDeclC,lcl=L'\<rparr> 
  3263                 \<turnstile> dom (locals (store s3')) \<guillemotright>\<langle>stmt (mbody (mthd dynM))\<rangle>\<guillemotright> M2" and
  3264               M2: "nrm M' \<subseteq> nrm M2"
  3265               by (rule da_weakenE)
  3266             from res M2 have "Result \<in> nrm M2"
  3267               by blast
  3268             moreover from wf_dynM
  3269             have "jumpNestingOkS {Ret} (stmt (mbody (mthd dynM)))"
  3270               by (rule wf_mdeclE)
  3271             ultimately
  3272             obtain M3 where
  3273               "\<lparr>prg=G, cls=invDeclC,lcl=L'\<rparr> \<turnstile> dom (locals (store s3')) 
  3274                      \<guillemotright>\<langle>Body (declclass dynM) (stmt (mbody (mthd dynM)))\<rangle>\<guillemotright> M3"
  3275               using da
  3276               by (iprover intro: da.Body assigned.select_convs)
  3277             from _ this [simplified]
  3278             show ?thesis
  3279               by (rule da.Methd [simplified,elim_format]) (auto intro: dynM' that)
  3280           qed
  3281           ultimately obtain  
  3282             conf_s4: "s4\<Colon>\<preceq>(G, L')" and 
  3283             conf_Res: "normal s4 \<longrightarrow> G,store s4\<turnstile>v\<Colon>\<preceq>mthdT" and
  3284             error_free_s4: "error_free s4"
  3285             by (rule hyp_methd [elim_format]) 
  3286                (simp add: error_free_s3 eq_s3'_s3)
  3287           from init_lvars eval_methd eq_s3'_s3 
  3288           have "store s2\<le>|store s4"
  3289             by (cases s2) (auto dest!: eval_gext simp add: init_lvars_def2 )
  3290           moreover
  3291           have "abrupt s4 \<noteq> Some (Jump Ret)"
  3292           proof -
  3293             from normal_s2 init_lvars
  3294             have "abrupt s3 \<noteq> Some (Jump Ret)"
  3295               by (cases s2) (simp add: init_lvars_def2 abrupt_if_def)
  3296             with check
  3297             have "abrupt s3' \<noteq> Some (Jump Ret)"
  3298               by (cases s3) (auto simp add: check_method_access_def Let_def)
  3299             with eval_methd
  3300             show ?thesis
  3301               by (rule Methd_no_jump)
  3302           qed
  3303           ultimately 
  3304           have "(set_lvars (locals (store s2))) s4\<Colon>\<preceq>(G, L)"
  3305             using conf_s2 conf_s4
  3306             by (cases s2,cases s4) (auto intro: conforms_return)
  3307           moreover 
  3308           from conf_Res mthdT_widen resTy_widen wf
  3309           have "normal s4 
  3310                   \<longrightarrow> G,store s4\<turnstile>v\<Colon>\<preceq>(resTy statM)"
  3311             by (auto dest: widen_trans)
  3312           then
  3313           have "normal ((set_lvars (locals (store s2))) s4)
  3314              \<longrightarrow> G,store((set_lvars (locals (store s2))) s4) \<turnstile>v\<Colon>\<preceq>(resTy statM)"
  3315             by (cases s4) auto
  3316           moreover note error_free_s4 T
  3317           ultimately 
  3318           show ?thesis
  3319             by simp
  3320         qed
  3321       qed
  3322     qed
  3323   next
  3324     case (Methd s0 D sig v s1 L accC T A)
  3325     note `G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<rightarrow> s1`
  3326     note hyp = `PROP ?TypeSafe (Norm s0) s1 (In1l (body G D sig)) (In1 v)`
  3327     note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
  3328     note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (Methd D sig)\<Colon>T`
  3329     then obtain m bodyT where
  3330       D: "is_class G D" and
  3331       m: "methd G D sig = Some m" and
  3332       wt_body: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>
  3333                   \<turnstile>Body (declclass m) (stmt (mbody (mthd m)))\<Colon>-bodyT" and
  3334       T: "T=Inl bodyT"
  3335       by (rule wt_elim_cases) auto
  3336     moreover
  3337     from Methd.prems m have 
  3338        da_body: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  3339                    \<turnstile> (dom (locals (store ((Norm s0)::state))))
  3340                        \<guillemotright>In1l (Body (declclass m) (stmt (mbody (mthd m))))\<guillemotright> A"
  3341       by - (erule da_elim_cases,simp)
  3342     ultimately
  3343     show "s1\<Colon>\<preceq>(G, L) \<and> 
  3344            (normal s1 \<longrightarrow> G,L,snd s1\<turnstile>In1l (Methd D sig)\<succ>In1 v\<Colon>\<preceq>T) \<and>
  3345            (error_free (Norm s0) = error_free s1)"
  3346       using hyp [of _ _ "(Inl bodyT)"] conf_s0 
  3347       by (auto simp add: Let_def body_def)
  3348   next
  3349     case (Body s0 D s1 c s2 s3 L accC T A)
  3350     note eval_init = `G\<turnstile>Norm s0 \<midarrow>Init D\<rightarrow> s1`
  3351     note eval_c = `G\<turnstile>s1 \<midarrow>c\<rightarrow> s2`
  3352     note hyp_init = `PROP ?TypeSafe (Norm s0) s1 (In1r (Init D)) \<diamondsuit>`
  3353     note hyp_c = `PROP ?TypeSafe s1 s2 (In1r c) \<diamondsuit>`
  3354     note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
  3355     note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (Body D c)\<Colon>T`
  3356     then obtain bodyT where
  3357          iscls_D: "is_class G D" and
  3358             wt_c: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c\<Colon>\<surd>" and
  3359          resultT: "L Result = Some bodyT" and
  3360       isty_bodyT: "is_type G bodyT" and (* ### not needed! remove from wt? *)
  3361                T: "T=Inl bodyT"
  3362       by (rule wt_elim_cases) auto
  3363     from Body.prems obtain C where
  3364       da_c: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  3365                    \<turnstile> (dom (locals (store ((Norm s0)::state))))\<guillemotright>In1r c\<guillemotright> C" and
  3366       jmpOk: "jumpNestingOkS {Ret} c" and
  3367       res: "Result \<in> nrm C"
  3368       by (elim da_elim_cases) simp
  3369     note conf_s0
  3370     moreover from iscls_D 
  3371     have "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>Init D\<Colon>\<surd>" by auto
  3372     moreover obtain I where 
  3373       "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  3374           \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1r (Init D)\<guillemotright> I"
  3375       by (auto intro: da_Init [simplified] assigned.select_convs)
  3376     ultimately obtain
  3377       conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1:  "error_free s1"
  3378        by (rule hyp_init [elim_format]) simp
  3379     obtain C' where da_C': "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  3380                              \<turnstile> (dom (locals (store s1)))\<guillemotright>In1r c\<guillemotright> C'"
  3381                and nrm_C': "nrm C \<subseteq> nrm C'"
  3382     proof -
  3383       from eval_init 
  3384       have "(dom (locals (store ((Norm s0)::state)))) 
  3385                      \<subseteq> (dom (locals (store s1)))"
  3386         by (rule dom_locals_eval_mono_elim)
  3387       with da_c show thesis by (rule da_weakenE) (rule that)
  3388     qed
  3389     from conf_s1 wt_c da_C' 
  3390     obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"
  3391       by (rule hyp_c [elim_format]) (simp add: error_free_s1)
  3392     from conf_s2
  3393     have "abupd (absorb Ret) s2\<Colon>\<preceq>(G, L)"
  3394       by (cases s2) (auto intro: conforms_absorb)
  3395     moreover
  3396     from error_free_s2
  3397     have "error_free (abupd (absorb Ret) s2)"
  3398       by simp
  3399     moreover have "abrupt (abupd (absorb Ret) s3) \<noteq> Some (Jump Ret)"
  3400       by (cases s3) (simp add: absorb_def)
  3401     moreover have "s3=s2"
  3402     proof -
  3403       from iscls_D
  3404       have wt_init: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(Init D)\<Colon>\<surd>"
  3405         by auto
  3406       from eval_init wf
  3407       have s1_no_jmp: "\<And> j. abrupt s1 \<noteq> Some (Jump j)"
  3408         by - (rule eval_statement_no_jump [OF _ _ _ wt_init],auto)
  3409       from eval_c _ wt_c wf
  3410       have "\<And> j. abrupt s2 = Some (Jump j) \<Longrightarrow> j=Ret"
  3411         by (rule jumpNestingOk_evalE) (auto intro: jmpOk simp add: s1_no_jmp)
  3412       moreover 
  3413       note `s3 =
  3414                 (if \<exists>l. abrupt s2 = Some (Jump (Break l)) \<or> 
  3415                         abrupt s2 = Some (Jump (Cont l))
  3416                  then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2 else s2)`
  3417       ultimately show ?thesis
  3418         by force
  3419     qed
  3420     moreover
  3421     {
  3422       assume normal_upd_s2:  "normal (abupd (absorb Ret) s2)"
  3423       have "Result \<in> dom (locals (store s2))"
  3424       proof -
  3425         from normal_upd_s2
  3426         have "normal s2 \<or> abrupt s2 = Some (Jump Ret)"
  3427           by (cases s2) (simp add: absorb_def)
  3428         thus ?thesis
  3429         proof 
  3430           assume "normal s2"
  3431           with eval_c wt_c da_C' wf res nrm_C'
  3432           show ?thesis
  3433             by (cases rule: da_good_approxE') blast
  3434         next
  3435           assume "abrupt s2 = Some (Jump Ret)"
  3436           with conf_s2 show ?thesis
  3437             by (cases s2) (auto dest: conforms_RetD simp add: dom_def)
  3438         qed 
  3439       qed
  3440     }
  3441     moreover note T resultT
  3442     ultimately
  3443     show "abupd (absorb Ret) s3\<Colon>\<preceq>(G, L) \<and>
  3444            (normal (abupd (absorb Ret) s3) \<longrightarrow>
  3445              G,L,store (abupd (absorb Ret) s3)
  3446              \<turnstile>In1l (Body D c)\<succ>In1 (the (locals (store s2) Result))\<Colon>\<preceq>T) \<and>
  3447           (error_free (Norm s0) = error_free (abupd (absorb Ret) s3)) "
  3448       by (cases s2) (auto intro: conforms_locals)
  3449   next
  3450     case (LVar s vn L accC T)
  3451     note conf_s = `Norm s\<Colon>\<preceq>(G, L)` and
  3452       wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In2 (LVar vn)\<Colon>T`
  3453     then obtain vnT where
  3454       vnT: "L vn = Some vnT" and
  3455         T: "T=Inl vnT"
  3456       by (auto elim!: wt_elim_cases)
  3457     from conf_s vnT
  3458     have conf_fst: "locals s vn \<noteq> None \<longrightarrow> G,s\<turnstile>fst (lvar vn s)\<Colon>\<preceq>vnT"  
  3459      by (auto elim: conforms_localD [THEN wlconfD]  
  3460               simp add: lvar_def) 
  3461     moreover
  3462     from conf_s conf_fst vnT 
  3463     have "s\<le>|snd (lvar vn s)\<preceq>vnT\<Colon>\<preceq>(G, L)"
  3464       by (auto elim: conforms_lupd simp add: assign_conforms_def lvar_def)
  3465     moreover note conf_s T
  3466     ultimately 
  3467     show "Norm s\<Colon>\<preceq>(G, L) \<and>
  3468                  (normal (Norm s) \<longrightarrow>
  3469                     G,L,store (Norm s)\<turnstile>In2 (LVar vn)\<succ>In2 (lvar vn s)\<Colon>\<preceq>T) \<and>
  3470                  (error_free (Norm s) = error_free (Norm s))"
  3471       by (simp add: lvar_def) 
  3472   next
  3473     case (FVar s0 statDeclC s1 e a s2 v s2' stat fn s3 accC L accC' T A)
  3474     note eval_init = `G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<rightarrow> s1`
  3475     note eval_e = `G\<turnstile>s1 \<midarrow>e-\<succ>a\<rightarrow> s2`
  3476     note fvar = `(v, s2') = fvar statDeclC stat fn a s2`
  3477     note check = `s3 = check_field_access G accC statDeclC fn stat a s2'`
  3478     note hyp_init = `PROP ?TypeSafe (Norm s0) s1 (In1r (Init statDeclC)) \<diamondsuit>`
  3479     note hyp_e = `PROP ?TypeSafe s1 s2 (In1l e) (In1 a)`
  3480     note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
  3481     note wt = `\<lparr>prg=G, cls=accC', lcl=L\<rparr>\<turnstile>In2 ({accC,statDeclC,stat}e..fn)\<Colon>T`
  3482     then obtain statC f where
  3483                 wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-Class statC" and
  3484             accfield: "accfield G accC statC fn = Some (statDeclC,f)" and
  3485        eq_accC_accC': "accC=accC'" and
  3486                 stat: "stat=is_static f" and
  3487                    T: "T=(Inl (type f))"
  3488       by (rule wt_elim_cases) (auto simp add: member_is_static_simp)
  3489     from FVar.prems eq_accC_accC'
  3490     have da_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>
  3491                  \<turnstile> (dom (locals (store ((Norm s0)::state))))\<guillemotright>In1l e\<guillemotright> A"
  3492       by (elim da_elim_cases) simp
  3493     note conf_s0
  3494     moreover
  3495     from wf wt_e 
  3496     have iscls_statC: "is_class G statC"
  3497       by (auto dest: ty_expr_is_type type_is_class)
  3498     with wf accfield 
  3499     have iscls_statDeclC: "is_class G statDeclC"
  3500       by (auto dest!: accfield_fields dest: fields_declC)
  3501     hence "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(Init statDeclC)\<Colon>\<surd>"
  3502       by simp
  3503     moreover obtain I where 
  3504       "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  3505         \<turnstile> dom (locals (store ((Norm s0)::state))) \<guillemotright>In1r (Init statDeclC)\<guillemotright> I"
  3506       by (auto intro: da_Init [simplified] assigned.select_convs)
  3507     ultimately 
  3508     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1"
  3509       by (rule hyp_init [elim_format]) simp
  3510     obtain A' where 
  3511       "\<lparr>prg=G, cls=accC, lcl=L\<rparr> \<turnstile> (dom (locals (store s1)))\<guillemotright>In1l e\<guillemotright> A'"
  3512     proof -
  3513       from eval_init
  3514       have "(dom (locals (store ((Norm s0)::state)))) 
  3515                \<subseteq> (dom (locals (store s1)))"
  3516         by (rule dom_locals_eval_mono_elim)
  3517       with da_e show thesis
  3518         by (rule da_weakenE) (rule that)
  3519     qed
  3520     with conf_s1 wt_e 
  3521     obtain       conf_s2: "s2\<Colon>\<preceq>(G, L)" and
  3522                   conf_a: "normal s2 \<longrightarrow> G,store s2\<turnstile>a\<Colon>\<preceq>Class statC" and
  3523            error_free_s2: "error_free s2"
  3524       by (rule hyp_e [elim_format]) (simp add: error_free_s1)
  3525     from fvar 
  3526     have store_s2': "store s2'=store s2"
  3527       by (cases s2) (simp add: fvar_def2)
  3528     with fvar conf_s2 
  3529     have conf_s2': "s2'\<Colon>\<preceq>(G, L)"
  3530       by (cases s2,cases stat) (auto simp add: fvar_def2)
  3531     from eval_init 
  3532     have initd_statDeclC_s1: "initd statDeclC s1"
  3533       by (rule init_yields_initd)
  3534     from accfield wt_e eval_init eval_e conf_s2 conf_a fvar stat check  wf
  3535     have eq_s3_s2': "s3=s2'"  
  3536       by (auto dest!: error_free_field_access)
  3537     have conf_v: "normal s2' \<Longrightarrow> 
  3538            G,store s2'\<turnstile>fst v\<Colon>\<preceq>type f \<and> store s2'\<le>|snd v\<preceq>type f\<Colon>\<preceq>(G, L)"
  3539     proof - (*###FVar_lemma should be adjusted to be more directy applicable *)
  3540       assume normal: "normal s2'"
  3541       obtain vv vf x2 store2 store2'
  3542         where  v: "v=(vv,vf)" and
  3543               s2: "s2=(x2,store2)" and
  3544          store2': "store s2' = store2'"
  3545         by (cases v,cases s2,cases s2') blast
  3546       from iscls_statDeclC obtain c
  3547         where c: "class G statDeclC = Some c"
  3548         by auto
  3549       have "G,store2'\<turnstile>vv\<Colon>\<preceq>type f \<and> store2'\<le>|vf\<preceq>type f\<Colon>\<preceq>(G, L)"
  3550       proof (rule FVar_lemma [of vv vf store2' statDeclC f fn a x2 store2 
  3551                                statC G c L "store s1"])
  3552         from v normal s2 fvar stat store2' 
  3553         show "((vv, vf), Norm store2') = 
  3554                fvar statDeclC (static f) fn a (x2, store2)"
  3555           by (auto simp add: member_is_static_simp)
  3556         from accfield iscls_statC wf
  3557         show "G\<turnstile>statC\<preceq>\<^sub>C statDeclC"
  3558           by (auto dest!: accfield_fields dest: fields_declC)
  3559         from accfield
  3560         show fld: "table_of (DeclConcepts.fields G statC) (fn, statDeclC) = Some f"
  3561           by (auto dest!: accfield_fields)
  3562         from wf show "wf_prog G" .
  3563         from conf_a s2 show "x2 = None \<longrightarrow> G,store2\<turnstile>a\<Colon>\<preceq>Class statC"
  3564           by auto
  3565         from fld wf iscls_statC
  3566         show "statDeclC \<noteq> Object "
  3567           by (cases "statDeclC=Object") (drule fields_declC,simp+)+
  3568         from c show "class G statDeclC = Some c" .
  3569         from conf_s2 s2 show "(x2, store2)\<Colon>\<preceq>(G, L)" by simp
  3570         from eval_e s2 show "snd s1\<le>|store2" by (auto dest: eval_gext)
  3571         from initd_statDeclC_s1 show "inited statDeclC (globs (snd s1))" 
  3572           by simp
  3573       qed
  3574       with v s2 store2'  
  3575       show ?thesis
  3576         by simp
  3577     qed
  3578     from fvar error_free_s2
  3579     have "error_free s2'"
  3580       by (cases s2)
  3581          (auto simp add: fvar_def2 intro!: error_free_FVar_lemma)
  3582     with conf_v T conf_s2' eq_s3_s2'
  3583     show "s3\<Colon>\<preceq>(G, L) \<and>
  3584           (normal s3 
  3585            \<longrightarrow> G,L,store s3\<turnstile>In2 ({accC,statDeclC,stat}e..fn)\<succ>In2 v\<Colon>\<preceq>T) \<and>
  3586           (error_free (Norm s0) = error_free s3)"
  3587       by auto
  3588   next
  3589     case (AVar s0 e1 a s1 e2 i s2 v s2' L accC T A)
  3590     note eval_e1 = `G\<turnstile>Norm s0 \<midarrow>e1-\<succ>a\<rightarrow> s1`
  3591     note eval_e2 = `G\<turnstile>s1 \<midarrow>e2-\<succ>i\<rightarrow> s2`
  3592     note hyp_e1 = `PROP ?TypeSafe (Norm s0) s1 (In1l e1) (In1 a)`
  3593     note hyp_e2 = `PROP ?TypeSafe s1 s2 (In1l e2) (In1 i)`
  3594     note avar = `(v, s2') = avar G i a s2`
  3595     note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
  3596     note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In2 (e1.[e2])\<Colon>T`
  3597     then obtain elemT
  3598        where wt_e1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e1\<Colon>-elemT.[]" and
  3599              wt_e2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e2\<Colon>-PrimT Integer" and
  3600                  T: "T= Inl elemT"
  3601       by (rule wt_elim_cases) auto
  3602     from AVar.prems obtain E1 where
  3603       da_e1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  3604                 \<turnstile> (dom (locals (store ((Norm s0)::state))))\<guillemotright>In1l e1\<guillemotright> E1" and
  3605       da_e2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> nrm E1 \<guillemotright>In1l e2\<guillemotright> A" 
  3606       by (elim da_elim_cases) simp
  3607     from conf_s0 wt_e1 da_e1  
  3608     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and
  3609             conf_a: "(normal s1 \<longrightarrow> G,store s1\<turnstile>a\<Colon>\<preceq>elemT.[])" and
  3610             error_free_s1: "error_free s1"
  3611       by (rule hyp_e1 [elim_format]) simp
  3612     show "s2'\<Colon>\<preceq>(G, L) \<and>
  3613            (normal s2' \<longrightarrow> G,L,store s2'\<turnstile>In2 (e1.[e2])\<succ>In2 v\<Colon>\<preceq>T) \<and>
  3614            (error_free (Norm s0) = error_free s2') "
  3615     proof (cases "normal s1")
  3616       case False
  3617       moreover
  3618       from False eval_e2 have eq_s2_s1: "s2=s1" by auto
  3619       moreover
  3620       from eq_s2_s1 False have  "\<not> normal s2" by simp
  3621       then have "snd (avar G i a s2) = s2"
  3622         by (cases s2) (simp add: avar_def2)
  3623       with avar have "s2'=s2"
  3624         by (cases "(avar G i a s2)") simp
  3625       ultimately show ?thesis
  3626         using conf_s1 error_free_s1
  3627         by auto
  3628     next
  3629       case True
  3630       obtain A' where 
  3631         "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>In1l e2\<guillemotright> A'"
  3632       proof -
  3633         from eval_e1 wt_e1 da_e1 wf True
  3634         have "nrm E1 \<subseteq> dom (locals (store s1))"
  3635           by (cases rule: da_good_approxE') iprover
  3636         with da_e2 show thesis
  3637           by (rule da_weakenE) (rule that)
  3638       qed
  3639       with conf_s1 wt_e2
  3640       obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"
  3641         by (rule hyp_e2 [elim_format]) (simp add: error_free_s1)
  3642       from avar 
  3643       have "store s2'=store s2"
  3644         by (cases s2) (simp add: avar_def2)
  3645       with avar conf_s2 
  3646       have conf_s2': "s2'\<Colon>\<preceq>(G, L)"
  3647         by (cases s2) (auto simp add: avar_def2)
  3648       from avar error_free_s2
  3649       have error_free_s2': "error_free s2'"
  3650         by (cases s2) (auto simp add: avar_def2 )
  3651       have "normal s2' \<Longrightarrow> 
  3652         G,store s2'\<turnstile>fst v\<Colon>\<preceq>elemT \<and> store s2'\<le>|snd v\<preceq>elemT\<Colon>\<preceq>(G, L)"
  3653       proof -(*###AVar_lemma should be adjusted to be more directy applicable *)
  3654         assume normal: "normal s2'"
  3655         show ?thesis
  3656         proof -
  3657           obtain vv vf x1 store1 x2 store2 store2'
  3658             where  v: "v=(vv,vf)" and
  3659                   s1: "s1=(x1,store1)" and
  3660                   s2: "s2=(x2,store2)" and
  3661              store2': "store2'=store s2'"
  3662             by (cases v,cases s1, cases s2, cases s2') blast 
  3663           have "G,store2'\<turnstile>vv\<Colon>\<preceq>elemT \<and> store2'\<le>|vf\<preceq>elemT\<Colon>\<preceq>(G, L)"
  3664           proof (rule AVar_lemma [of G x1 store1 e2 i x2 store2 vv vf store2' a,
  3665                                   OF wf])
  3666             from s1 s2 eval_e2 show "G\<turnstile>(x1, store1) \<midarrow>e2-\<succ>i\<rightarrow> (x2, store2)"
  3667               by simp
  3668             from v normal s2 store2' avar 
  3669             show "((vv, vf), Norm store2') = avar G i a (x2, store2)"
  3670               by auto
  3671             from s2 conf_s2 show "(x2, store2)\<Colon>\<preceq>(G, L)" by simp
  3672             from s1 conf_a show  "x1 = None \<longrightarrow> G,store1\<turnstile>a\<Colon>\<preceq>elemT.[]" by simp 
  3673             from eval_e2 s1 s2 show "store1\<le>|store2" by (auto dest: eval_gext)
  3674           qed
  3675           with v s1 s2 store2' 
  3676           show ?thesis
  3677             by simp
  3678         qed
  3679       qed
  3680       with conf_s2' error_free_s2' T 
  3681       show ?thesis 
  3682         by auto
  3683     qed
  3684   next
  3685     case (Nil s0 L accC T)
  3686     then show ?case
  3687       by (auto elim!: wt_elim_cases)
  3688   next
  3689     case (Cons s0 e v s1 es vs s2 L accC T A)
  3690     note eval_e = `G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1`
  3691     note eval_es = `G\<turnstile>s1 \<midarrow>es\<doteq>\<succ>vs\<rightarrow> s2`
  3692     note hyp_e = `PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 v)`
  3693     note hyp_es = `PROP ?TypeSafe s1 s2 (In3 es) (In3 vs)`
  3694     note conf_s0 = `Norm s0\<Colon>\<preceq>(G, L)`
  3695     note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In3 (e # es)\<Colon>T`
  3696     then obtain eT esT where
  3697        wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-eT" and
  3698        wt_es: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>es\<Colon>\<doteq>esT" and
  3699        T: "T=Inr (eT#esT)"
  3700       by (rule wt_elim_cases) blast
  3701     from Cons.prems obtain E where
  3702       da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  3703                 \<turnstile> (dom (locals (store ((Norm s0)::state))))\<guillemotright>In1l e\<guillemotright> E" and
  3704       da_es: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> nrm E \<guillemotright>In3 es\<guillemotright> A" 
  3705       by (elim da_elim_cases) simp
  3706     from conf_s0 wt_e da_e 
  3707     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and error_free_s1: "error_free s1" and 
  3708       conf_v: "normal s1 \<longrightarrow> G,store s1\<turnstile>v\<Colon>\<preceq>eT"
  3709       by (rule hyp_e [elim_format]) simp
  3710     show 
  3711       "s2\<Colon>\<preceq>(G, L) \<and> 
  3712       (normal s2 \<longrightarrow> G,L,store s2\<turnstile>In3 (e # es)\<succ>In3 (v # vs)\<Colon>\<preceq>T) \<and>
  3713       (error_free (Norm s0) = error_free s2)"
  3714     proof (cases "normal s1")
  3715       case False
  3716       with eval_es have "s2=s1" by auto
  3717       with False conf_s1 error_free_s1
  3718       show ?thesis
  3719         by auto
  3720     next
  3721       case True
  3722       obtain A' where 
  3723         "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>In3 es\<guillemotright> A'"
  3724       proof -
  3725         from eval_e wt_e da_e wf True
  3726         have "nrm E \<subseteq> dom (locals (store s1))"
  3727           by (cases rule: da_good_approxE') iprover
  3728         with da_es show thesis
  3729           by (rule da_weakenE) (rule that)
  3730       qed
  3731       with conf_s1 wt_es
  3732       obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and 
  3733            error_free_s2: "error_free s2" and
  3734            conf_vs: "normal s2 \<longrightarrow> list_all2 (conf G (store s2)) vs esT"
  3735         by (rule hyp_es [elim_format]) (simp add: error_free_s1)
  3736       moreover
  3737       from True eval_es conf_v 
  3738       have conf_v': "G,store s2\<turnstile>v\<Colon>\<preceq>eT"
  3739         apply clarify
  3740         apply (rule conf_gext)
  3741         apply (auto dest: eval_gext)
  3742         done
  3743       ultimately show ?thesis using T by simp
  3744     qed
  3745   qed
  3746   from this and conf_s0 wt da show ?thesis .
  3747 qed
  3748 
  3749 text {* 
  3750 
  3751 
  3752 *} (* dummy text command to break paragraph for latex;
  3753               large paragraphs exhaust memory of debian pdflatex *)
  3754 
  3755 corollary eval_type_soundE [consumes 5]:
  3756   assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v, s1)"
  3757   and     conf: "s0\<Colon>\<preceq>(G, L)"
  3758   and       wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>t\<Colon>T"
  3759   and       da: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile> dom (locals (snd s0)) \<guillemotright>t\<guillemotright> A"
  3760   and       wf: "wf_prog G"
  3761   and     elim: "\<lbrakk>s1\<Colon>\<preceq>(G, L); normal s1 \<Longrightarrow> G,L,snd s1\<turnstile>t\<succ>v\<Colon>\<preceq>T; 
  3762                   error_free s0 = error_free s1\<rbrakk> \<Longrightarrow> P"
  3763   shows "P"
  3764 using eval wt da wf conf
  3765 by (rule eval_type_sound [elim_format]) (iprover intro: elim) 
  3766 
  3767  
  3768 corollary eval_ts: 
  3769  "\<lbrakk>G\<turnstile>s \<midarrow>e-\<succ>v \<rightarrow> s'; wf_prog G; s\<Colon>\<preceq>(G,L); \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>e\<Colon>-T;
  3770    \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>In1l e\<guillemotright>A\<rbrakk> 
  3771 \<Longrightarrow>  s'\<Colon>\<preceq>(G,L) \<and> (normal s' \<longrightarrow> G,store s'\<turnstile>v\<Colon>\<preceq>T) \<and> 
  3772      (error_free s = error_free s')"
  3773 apply (drule (4) eval_type_sound)
  3774 apply clarsimp
  3775 done
  3776 
  3777 corollary evals_ts: 
  3778 "\<lbrakk>G\<turnstile>s \<midarrow>es\<doteq>\<succ>vs\<rightarrow> s'; wf_prog G; s\<Colon>\<preceq>(G,L); \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>es\<Colon>\<doteq>Ts;
  3779   \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>In3 es\<guillemotright>A\<rbrakk> 
  3780 \<Longrightarrow>  s'\<Colon>\<preceq>(G,L) \<and> (normal s' \<longrightarrow> list_all2 (conf G (store s')) vs Ts) \<and> 
  3781      (error_free s = error_free s')" 
  3782 apply (drule (4) eval_type_sound)
  3783 apply clarsimp
  3784 done
  3785 
  3786 corollary evar_ts: 
  3787 "\<lbrakk>G\<turnstile>s \<midarrow>v=\<succ>vf\<rightarrow> s'; wf_prog G; s\<Colon>\<preceq>(G,L); \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>v\<Colon>=T;
  3788  \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>In2 v\<guillemotright>A\<rbrakk> \<Longrightarrow>  
  3789   s'\<Colon>\<preceq>(G,L) \<and> (normal s' \<longrightarrow> G,L,(store s')\<turnstile>In2 v\<succ>In2 vf\<Colon>\<preceq>Inl T) \<and> 
  3790   (error_free s = error_free s')"
  3791 apply (drule (4) eval_type_sound)
  3792 apply clarsimp
  3793 done
  3794 
  3795 theorem exec_ts: 
  3796 "\<lbrakk>G\<turnstile>s \<midarrow>c\<rightarrow> s'; wf_prog G; s\<Colon>\<preceq>(G,L); \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>c\<Colon>\<surd>;
  3797  \<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store s))\<guillemotright>In1r c\<guillemotright>A\<rbrakk> 
  3798  \<Longrightarrow> s'\<Colon>\<preceq>(G,L) \<and> (error_free s \<longrightarrow> error_free s')"
  3799 apply (drule (4) eval_type_sound)
  3800 apply clarsimp
  3801 done
  3802 
  3803 lemma wf_eval_Fin: 
  3804   assumes wf:    "wf_prog G" 
  3805     and   wt_c1: "\<lparr>prg = G, cls = C, lcl = L\<rparr>\<turnstile>In1r c1\<Colon>Inl (PrimT Void)"
  3806     and   da_c1: "\<lparr>prg=G,cls=C,lcl=L\<rparr>\<turnstile>dom (locals (store (Norm s0)))\<guillemotright>In1r c1\<guillemotright>A"
  3807     and conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" 
  3808     and eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1,s1)" 
  3809     and eval_c2: "G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2" 
  3810     and      s3: "s3=abupd (abrupt_if (x1\<noteq>None) x1) s2"
  3811   shows "G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<rightarrow> s3"
  3812 proof -
  3813   from eval_c1 wt_c1 da_c1 wf conf_s0
  3814   have "error_free (x1,s1)"
  3815     by (auto dest: eval_type_sound)
  3816   with eval_c1 eval_c2 s3
  3817   show ?thesis
  3818     by - (rule eval.Fin, auto simp add: error_free_def)
  3819 qed
  3820 
  3821 subsection "Ideas for the future"
  3822 
  3823 text {* In the type soundness proof and the correctness proof of 
  3824 definite assignment we perform induction on the evaluation relation with the 
  3825 further preconditions that the term is welltyped and definitely assigned. During
  3826 the proofs we have to establish the welltypedness and definite assignment of 
  3827 the subterms to be able to apply the induction hypothesis. So large parts of
  3828 both proofs are the same work in propagating welltypedness and definite 
  3829 assignment. So we can derive a new induction rule for induction on the 
  3830 evaluation of a wellformed term, were these propagations is already done, once
  3831 and forever. 
  3832 Then we can do the proofs with this rule and can enjoy the time we have saved.
  3833 Here is a first and incomplete sketch of such a rule.*}
  3834 theorem wellformed_eval_induct [consumes 4, case_names Abrupt Skip Expr Lab 
  3835                                 Comp If]:
  3836   assumes  eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" 
  3837    and      wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T" 
  3838    and      da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>t\<guillemotright>A"
  3839    and      wf: "wf_prog G" 
  3840    and  abrupt: "\<And> s t abr L accC T A. 
  3841                   \<lbrakk>\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T; 
  3842                    \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store (Some abr,s)))\<guillemotright>t\<guillemotright>A
  3843                   \<rbrakk> \<Longrightarrow> P L accC (Some abr, s) t (undefined3 t) (Some abr, s)"
  3844    and    skip: "\<And> s L accC. P L accC (Norm s) \<langle>Skip\<rangle>\<^sub>s \<diamondsuit> (Norm s)"
  3845    and    expr: "\<And> e s0 s1 v L accC eT E.
  3846                  \<lbrakk>\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e\<Colon>-eT;
  3847                   \<lparr>prg=G,cls=accC,lcl=L\<rparr>
  3848                      \<turnstile>dom (locals (store ((Norm s0)::state)))\<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright>E;
  3849                   P L accC (Norm s0) \<langle>e\<rangle>\<^sub>e \<lfloor>v\<rfloor>\<^sub>e s1\<rbrakk> 
  3850                  \<Longrightarrow>  P L accC (Norm s0) \<langle>Expr e\<rangle>\<^sub>s \<diamondsuit> s1"
  3851    and     lab: "\<And> c l s0 s1 L accC C.
  3852                  \<lbrakk>\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c\<Colon>\<surd>;
  3853                   \<lparr>prg=G,cls=accC, lcl=L\<rparr>
  3854                      \<turnstile>dom (locals (store ((Norm s0)::state)))\<guillemotright>\<langle>c\<rangle>\<^sub>s\<guillemotright>C;
  3855                   P L accC (Norm s0) \<langle>c\<rangle>\<^sub>s \<diamondsuit> s1\<rbrakk>
  3856                   \<Longrightarrow> P L accC (Norm s0) \<langle>l\<bullet> c\<rangle>\<^sub>s \<diamondsuit> (abupd (absorb l) s1)"
  3857    and    comp: "\<And> c1 c2 s0 s1 s2 L accC C1.
  3858                  \<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1 \<rightarrow> s1;G\<turnstile>s1 \<midarrow>c2 \<rightarrow> s2;
  3859                   \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c1\<Colon>\<surd>;
  3860                   \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c2\<Colon>\<surd>;
  3861                   \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> 
  3862                      dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>c1\<rangle>\<^sub>s\<guillemotright> C1;
  3863                   P L accC (Norm s0) \<langle>c1\<rangle>\<^sub>s \<diamondsuit> s1;
  3864                   \<And> Q. \<lbrakk>normal s1; 
  3865                          \<And> C2.\<lbrakk>\<lparr>prg=G,cls=accC,lcl=L\<rparr>
  3866                                   \<turnstile>dom (locals (store s1)) \<guillemotright>\<langle>c2\<rangle>\<^sub>s\<guillemotright> C2;
  3867                                P L accC s1 \<langle>c2\<rangle>\<^sub>s \<diamondsuit> s2\<rbrakk> \<Longrightarrow> Q
  3868                         \<rbrakk> \<Longrightarrow> Q 
  3869                   \<rbrakk>\<Longrightarrow> P L accC (Norm s0) \<langle>c1;; c2\<rangle>\<^sub>s \<diamondsuit> s2" 
  3870     and  "if": "\<And> b c1 c2 e s0 s1 s2 L accC E.
  3871                 \<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1;
  3872                  G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2;
  3873                  \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean;
  3874                  \<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(if the_Bool b then c1 else c2)\<Colon>\<surd>;
  3875                  \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> 
  3876                      dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> E;
  3877                  P L accC (Norm s0) \<langle>e\<rangle>\<^sub>e \<lfloor>b\<rfloor>\<^sub>e s1;
  3878                  \<And> Q. \<lbrakk>normal s1;
  3879                         \<And> C. \<lbrakk>\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s1)))
  3880                                    \<guillemotright>\<langle>if the_Bool b then c1 else c2\<rangle>\<^sub>s\<guillemotright> C;
  3881                               P L accC s1 \<langle>if the_Bool b then c1 else c2\<rangle>\<^sub>s \<diamondsuit> s2
  3882                               \<rbrakk> \<Longrightarrow> Q
  3883                        \<rbrakk> \<Longrightarrow> Q
  3884                 \<rbrakk> \<Longrightarrow> P L accC (Norm s0) \<langle>If(e) c1 Else c2\<rangle>\<^sub>s \<diamondsuit> s2" 
  3885    shows "P L accC s0 t v s1"  
  3886 proof -
  3887   note inj_term_simps [simp]
  3888   from eval 
  3889   show "\<And> L accC T A. \<lbrakk>\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T;
  3890                        \<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s0))\<guillemotright>t\<guillemotright>A\<rbrakk>  
  3891         \<Longrightarrow> P L accC s0 t v s1" (is "PROP ?Hyp s0 t v s1")
  3892   proof (induct)
  3893     case Abrupt with abrupt show ?case .
  3894   next
  3895     case Skip from skip show ?case by simp
  3896   next
  3897     case (Expr s0 e v s1 L accC T A) 
  3898     from Expr.prems obtain eT where 
  3899       "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-eT"
  3900       by (elim wt_elim_cases) 
  3901     moreover
  3902     from Expr.prems obtain E where
  3903       "\<lparr>prg=G,cls=accC, lcl=L\<rparr>\<turnstile>dom (locals (store ((Norm s0)::state)))\<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright>E"
  3904       by (elim da_elim_cases) simp
  3905     moreover from calculation
  3906     have "P L accC (Norm s0) \<langle>e\<rangle>\<^sub>e \<lfloor>v\<rfloor>\<^sub>e s1"
  3907       by (rule Expr.hyps) 
  3908     ultimately show ?case
  3909       by (rule expr)
  3910   next
  3911     case (Lab s0 c s1 l L accC T A)
  3912     from Lab.prems 
  3913     have "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c\<Colon>\<surd>"
  3914       by (elim wt_elim_cases)
  3915     moreover
  3916     from Lab.prems obtain C where
  3917       "\<lparr>prg=G,cls=accC, lcl=L\<rparr>\<turnstile>dom (locals (store ((Norm s0)::state)))\<guillemotright>\<langle>c\<rangle>\<^sub>s\<guillemotright>C"
  3918       by (elim da_elim_cases) simp
  3919     moreover from calculation
  3920     have "P L accC (Norm s0) \<langle>c\<rangle>\<^sub>s \<diamondsuit> s1"
  3921       by (rule  Lab.hyps)  
  3922     ultimately show ?case
  3923       by (rule lab)
  3924   next
  3925     case (Comp s0 c1 s1 c2 s2 L accC T A) 
  3926     note eval_c1 = `G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1`
  3927     note eval_c2 = `G\<turnstile>s1 \<midarrow>c2\<rightarrow> s2`
  3928     from Comp.prems obtain 
  3929       wt_c1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
  3930       wt_c2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c2\<Colon>\<surd>"
  3931       by (elim wt_elim_cases) 
  3932     from Comp.prems
  3933     obtain C1 C2
  3934       where da_c1: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile> 
  3935                       dom (locals (store ((Norm s0)::state))) \<guillemotright>\<langle>c1\<rangle>\<^sub>s\<guillemotright> C1" and 
  3936             da_c2: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>  nrm C1 \<guillemotright>\<langle>c2\<rangle>\<^sub>s\<guillemotright> C2" 
  3937       by (elim da_elim_cases) simp
  3938     from wt_c1 da_c1
  3939     have P_c1: "P L accC (Norm s0) \<langle>c1\<rangle>\<^sub>s \<diamondsuit> s1"
  3940       by (rule Comp.hyps)
  3941     {
  3942       fix Q
  3943       assume normal_s1: "normal s1"
  3944       assume elim: "\<And> C2'. 
  3945                     \<lbrakk>\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>dom (locals (store s1))\<guillemotright>\<langle>c2\<rangle>\<^sub>s\<guillemotright>C2';
  3946                        P L accC s1 \<langle>c2\<rangle>\<^sub>s \<diamondsuit> s2\<rbrakk> \<Longrightarrow> Q"
  3947       have Q
  3948       proof -
  3949         obtain C2' where 
  3950           da: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile> dom (locals (store s1)) \<guillemotright>\<langle>c2\<rangle>\<^sub>s\<guillemotright> C2'"
  3951         proof -
  3952           from eval_c1 wt_c1 da_c1 wf normal_s1
  3953           have "nrm C1 \<subseteq> dom (locals (store s1))"
  3954             by (cases rule: da_good_approxE') iprover
  3955           with da_c2 show thesis
  3956             by (rule da_weakenE) (rule that)
  3957         qed
  3958         with wt_c2 have "P L accC s1 \<langle>c2\<rangle>\<^sub>s \<diamondsuit> s2"
  3959           by (rule Comp.hyps)
  3960         with da show ?thesis
  3961           using elim by iprover
  3962       qed
  3963     }
  3964     with eval_c1 eval_c2 wt_c1 wt_c2 da_c1 P_c1 
  3965     show ?case
  3966       by (rule comp) iprover+
  3967   next
  3968     case (If s0 e b s1 c1 c2 s2 L accC T A)
  3969     note eval_e = `G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1`
  3970     note eval_then_else = `G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2`
  3971     from If.prems
  3972     obtain 
  3973               wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean" and
  3974       wt_then_else: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(if the_Bool b then c1 else c2)\<Colon>\<surd>"
  3975       by (elim wt_elim_cases) (auto split add: split_if)
  3976     from If.prems obtain E C where
  3977       da_e: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> dom (locals (store ((Norm s0)::state))) 
  3978                                        \<guillemotright>\<langle>e\<rangle>\<^sub>e\<guillemotright> E" and
  3979       da_then_else: 
  3980       "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> 
  3981          (dom (locals (store ((Norm s0)::state))) \<union> assigns_if (the_Bool b) e)
  3982           \<guillemotright>\<langle>if the_Bool b then c1 else c2\<rangle>\<^sub>s\<guillemotright> C"
  3983       by (elim da_elim_cases) (cases "the_Bool b",auto)
  3984     from wt_e da_e
  3985     have P_e: "P L accC (Norm s0) \<langle>e\<rangle>\<^sub>e \<lfloor>b\<rfloor>\<^sub>e s1"
  3986       by (rule If.hyps)
  3987     {
  3988       fix Q
  3989       assume normal_s1: "normal s1"
  3990       assume elim: "\<And> C. \<lbrakk>\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> (dom (locals (store s1)))
  3991                                    \<guillemotright>\<langle>if the_Bool b then c1 else c2\<rangle>\<^sub>s\<guillemotright> C;
  3992                               P L accC s1 \<langle>if the_Bool b then c1 else c2\<rangle>\<^sub>s \<diamondsuit> s2
  3993                               \<rbrakk> \<Longrightarrow> Q"
  3994       have Q
  3995       proof -
  3996         obtain C' where
  3997           da: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile> 
  3998                 (dom (locals (store s1)))\<guillemotright>\<langle>if the_Bool b then c1 else c2\<rangle>\<^sub>s \<guillemotright> C'"
  3999         proof -
  4000           from eval_e have 
  4001             "dom (locals (store ((Norm s0)::state))) \<subseteq> dom (locals (store s1))"
  4002             by (rule dom_locals_eval_mono_elim)
  4003           moreover
  4004           from eval_e normal_s1 wt_e 
  4005           have "assigns_if (the_Bool b) e \<subseteq> dom (locals (store s1))"
  4006             by (rule assigns_if_good_approx')
  4007           ultimately 
  4008           have "dom (locals (store ((Norm s0)::state))) 
  4009             \<union> assigns_if (the_Bool b) e \<subseteq> dom (locals (store s1))"
  4010             by (rule Un_least)
  4011           with da_then_else show thesis
  4012             by (rule da_weakenE) (rule that)
  4013         qed
  4014         with wt_then_else
  4015         have "P L accC s1 \<langle>if the_Bool b then c1 else c2\<rangle>\<^sub>s \<diamondsuit> s2"
  4016           by (rule If.hyps)
  4017         with da show ?thesis using elim by iprover
  4018       qed
  4019     }
  4020     with eval_e eval_then_else wt_e wt_then_else da_e P_e
  4021     show ?case
  4022       by (rule "if") iprover+
  4023   next
  4024     oops
  4025 
  4026 end