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