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