src/HOL/Bali/Evaln.thy
author schirmer
Wed Jul 10 15:07:02 2002 +0200 (2002-07-10 ago)
changeset 13337 f75dfc606ac7
parent 12937 0c4fd7529467
child 13384 a34e38154413
permissions -rw-r--r--
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
     1 (*  Title:      HOL/Bali/Evaln.thy
     2     ID:         $Id$
     3     Author:     David von Oheimb and Norbert Schirmer
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 *)
     6 header {* Operational evaluation (big-step) semantics of Java expressions and 
     7           statements
     8 *}
     9 
    10 theory Evaln = Eval + TypeSafe:
    11 
    12 text {*
    13 Variant of eval relation with counter for bounded recursive depth.
    14 Evaln omits the technical accessibility tests @{term check_field_access}
    15 and @{term check_method_access}, since we proved the absence of errors for
    16 wellformed programs.
    17 *}
    18 
    19 consts
    20 
    21   evaln	:: "prog \<Rightarrow> (state \<times> term \<times> nat \<times> vals \<times> state) set"
    22 
    23 syntax
    24 
    25   evaln	:: "[prog, state, term,        nat, vals * state] => bool"
    26 				("_|-_ -_>-_-> _"   [61,61,80,   61,61] 60)
    27   evarn	:: "[prog, state, var  , vvar        , nat, state] => bool"
    28 				("_|-_ -_=>_-_-> _" [61,61,90,61,61,61] 60)
    29   eval_n:: "[prog, state, expr , val         , nat, state] => bool"
    30 				("_|-_ -_->_-_-> _" [61,61,80,61,61,61] 60)
    31   evalsn:: "[prog, state, expr list, val list, nat, state] => bool"
    32 				("_|-_ -_#>_-_-> _" [61,61,61,61,61,61] 60)
    33   execn	:: "[prog, state, stmt ,               nat, state] => bool"
    34 				("_|-_ -_-_-> _"    [61,61,65,   61,61] 60)
    35 
    36 syntax (xsymbols)
    37 
    38   evaln	:: "[prog, state, term,         nat, vals \<times> state] \<Rightarrow> bool"
    39 				("_\<turnstile>_ \<midarrow>_\<succ>\<midarrow>_\<rightarrow> _"   [61,61,80,   61,61] 60)
    40   evarn	:: "[prog, state, var  , vvar         , nat, state] \<Rightarrow> bool"
    41 				("_\<turnstile>_ \<midarrow>_=\<succ>_\<midarrow>_\<rightarrow> _" [61,61,90,61,61,61] 60)
    42   eval_n:: "[prog, state, expr , val ,          nat, state] \<Rightarrow> bool"
    43 				("_\<turnstile>_ \<midarrow>_-\<succ>_\<midarrow>_\<rightarrow> _" [61,61,80,61,61,61] 60)
    44   evalsn:: "[prog, state, expr list, val  list, nat, state] \<Rightarrow> bool"
    45 				("_\<turnstile>_ \<midarrow>_\<doteq>\<succ>_\<midarrow>_\<rightarrow> _" [61,61,61,61,61,61] 60)
    46   execn	:: "[prog, state, stmt ,                nat, state] \<Rightarrow> bool"
    47 				("_\<turnstile>_ \<midarrow>_\<midarrow>_\<rightarrow> _"     [61,61,65,   61,61] 60)
    48 
    49 translations
    50 
    51   "G\<turnstile>s \<midarrow>t    \<succ>\<midarrow>n\<rightarrow>  w___s' " == "(s,t,n,w___s') \<in> evaln G"
    52   "G\<turnstile>s \<midarrow>t    \<succ>\<midarrow>n\<rightarrow> (w,  s')" <= "(s,t,n,w,  s') \<in> evaln G"
    53   "G\<turnstile>s \<midarrow>t    \<succ>\<midarrow>n\<rightarrow> (w,x,s')" <= "(s,t,n,w,x,s') \<in> evaln G"
    54   "G\<turnstile>s \<midarrow>c     \<midarrow>n\<rightarrow> (x,s')" <= "G\<turnstile>s \<midarrow>In1r  c\<succ>\<midarrow>n\<rightarrow> (\<diamondsuit>    ,x,s')"
    55   "G\<turnstile>s \<midarrow>c     \<midarrow>n\<rightarrow>    s' " == "G\<turnstile>s \<midarrow>In1r  c\<succ>\<midarrow>n\<rightarrow> (\<diamondsuit>    ,  s')"
    56   "G\<turnstile>s \<midarrow>e-\<succ>v  \<midarrow>n\<rightarrow> (x,s')" <= "G\<turnstile>s \<midarrow>In1l e\<succ>\<midarrow>n\<rightarrow> (In1 v ,x,s')"
    57   "G\<turnstile>s \<midarrow>e-\<succ>v  \<midarrow>n\<rightarrow>    s' " == "G\<turnstile>s \<midarrow>In1l e\<succ>\<midarrow>n\<rightarrow> (In1 v ,  s')"
    58   "G\<turnstile>s \<midarrow>e=\<succ>vf \<midarrow>n\<rightarrow> (x,s')" <= "G\<turnstile>s \<midarrow>In2  e\<succ>\<midarrow>n\<rightarrow> (In2 vf,x,s')"
    59   "G\<turnstile>s \<midarrow>e=\<succ>vf \<midarrow>n\<rightarrow>    s' " == "G\<turnstile>s \<midarrow>In2  e\<succ>\<midarrow>n\<rightarrow> (In2 vf,  s')"
    60   "G\<turnstile>s \<midarrow>e\<doteq>\<succ>v  \<midarrow>n\<rightarrow> (x,s')" <= "G\<turnstile>s \<midarrow>In3  e\<succ>\<midarrow>n\<rightarrow> (In3 v ,x,s')"
    61   "G\<turnstile>s \<midarrow>e\<doteq>\<succ>v  \<midarrow>n\<rightarrow>    s' " == "G\<turnstile>s \<midarrow>In3  e\<succ>\<midarrow>n\<rightarrow> (In3 v ,  s')"
    62 
    63 
    64 inductive "evaln G" intros
    65 
    66 (* propagation of abrupt completion *)
    67 
    68   Abrupt:   "G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (arbitrary3 t,(Some xc,s))"
    69 
    70 
    71 (* evaluation of variables *)
    72 
    73   LVar:	"G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<midarrow>n\<rightarrow> Norm s"
    74 
    75   FVar:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e-\<succ>a'\<midarrow>n\<rightarrow> s2;
    76 	  (v,s2') = fvar statDeclC stat fn a' s2\<rbrakk> \<Longrightarrow>
    77 	  G\<turnstile>Norm s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>v\<midarrow>n\<rightarrow> s2'"
    78 
    79   AVar:	"\<lbrakk>G\<turnstile> Norm s0 \<midarrow>e1-\<succ>a\<midarrow>n\<rightarrow> s1 ; G\<turnstile>s1 \<midarrow>e2-\<succ>i\<midarrow>n\<rightarrow> s2; 
    80 	  (v,s2') = avar G i a s2\<rbrakk> \<Longrightarrow>
    81 	              G\<turnstile>Norm s0 \<midarrow>e1.[e2]=\<succ>v\<midarrow>n\<rightarrow> s2'"
    82 
    83 
    84 
    85 
    86 (* evaluation of expressions *)
    87 
    88   NewC:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s1;
    89 	  G\<turnstile>     s1 \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s2\<rbrakk> \<Longrightarrow>
    90 	                          G\<turnstile>Norm s0 \<midarrow>NewC C-\<succ>Addr a\<midarrow>n\<rightarrow> s2"
    91 
    92   NewA:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>init_comp_ty T\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e-\<succ>i'\<midarrow>n\<rightarrow> s2; 
    93 	  G\<turnstile>abupd (check_neg i') s2 \<midarrow>halloc (Arr T (the_Intg i'))\<succ>a\<rightarrow> s3\<rbrakk> \<Longrightarrow>
    94 	                        G\<turnstile>Norm s0 \<midarrow>New T[e]-\<succ>Addr a\<midarrow>n\<rightarrow> s3"
    95 
    96   Cast:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1;
    97 	  s2 = abupd (raise_if (\<not>G,snd s1\<turnstile>v fits T) ClassCast) s1\<rbrakk> \<Longrightarrow>
    98 			        G\<turnstile>Norm s0 \<midarrow>Cast T e-\<succ>v\<midarrow>n\<rightarrow> s2"
    99 
   100   Inst:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1;
   101 	  b = (v\<noteq>Null \<and> G,store s1\<turnstile>v fits RefT T)\<rbrakk> \<Longrightarrow>
   102 			      G\<turnstile>Norm s0 \<midarrow>e InstOf T-\<succ>Bool b\<midarrow>n\<rightarrow> s1"
   103 
   104   Lit:			   "G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<midarrow>n\<rightarrow> Norm s"
   105 
   106   UnOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1\<rbrakk> 
   107          \<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>(eval_unop unop v)\<midarrow>n\<rightarrow> s1"
   108 
   109   BinOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e2-\<succ>v2\<midarrow>n\<rightarrow> s2\<rbrakk> 
   110          \<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<midarrow>n\<rightarrow> s2"
   111 
   112   Super:		   "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<midarrow>n\<rightarrow> Norm s"
   113 
   114   Acc:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v,f)\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   115 	                          G\<turnstile>Norm s0 \<midarrow>Acc va-\<succ>v\<midarrow>n\<rightarrow> s1"
   116 
   117   Ass:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(w,f)\<midarrow>n\<rightarrow> s1;
   118           G\<turnstile>     s1 \<midarrow>e-\<succ>v     \<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   119 				   G\<turnstile>Norm s0 \<midarrow>va:=e-\<succ>v\<midarrow>n\<rightarrow> assign f v s2"
   120 
   121   Cond:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<midarrow>n\<rightarrow> s1;
   122           G\<turnstile>     s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   123 			    G\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<midarrow>n\<rightarrow> s2"
   124 
   125   Call:	
   126   "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<midarrow>n\<rightarrow> s2;
   127     D = invocation_declclass G mode (store s2) a' statT \<lparr>name=mn,parTs=pTs\<rparr>; 
   128     G\<turnstile>init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' vs s2
   129             \<midarrow>Methd D \<lparr>name=mn,parTs=pTs\<rparr>-\<succ>v\<midarrow>n\<rightarrow> s3\<rbrakk>
   130    \<Longrightarrow> 
   131     G\<turnstile>Norm s0 \<midarrow>{accC,statT,mode}e\<cdot>mn({pTs}args)-\<succ>v\<midarrow>n\<rightarrow> (restore_lvars s2 s3)"
   132 
   133   Methd:"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   134 				G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<midarrow>Suc n\<rightarrow> s1"
   135 
   136   Body:	"\<lbrakk>G\<turnstile>Norm s0\<midarrow>Init D\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c\<midarrow>n\<rightarrow> s2\<rbrakk>\<Longrightarrow>
   137          G\<turnstile>Norm s0 \<midarrow>Body D c
   138           -\<succ>the (locals (store s2) Result)\<midarrow>n\<rightarrow>abupd (absorb Ret) s2"
   139 
   140 (* evaluation of expression lists *)
   141 
   142   Nil:
   143 				"G\<turnstile>Norm s0 \<midarrow>[]\<doteq>\<succ>[]\<midarrow>n\<rightarrow> Norm s0"
   144 
   145   Cons:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e -\<succ> v \<midarrow>n\<rightarrow> s1;
   146           G\<turnstile>     s1 \<midarrow>es\<doteq>\<succ>vs\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   147 			     G\<turnstile>Norm s0 \<midarrow>e#es\<doteq>\<succ>v#vs\<midarrow>n\<rightarrow> s2"
   148 
   149 
   150 (* execution of statements *)
   151 
   152   Skip:	 			    "G\<turnstile>Norm s \<midarrow>Skip\<midarrow>n\<rightarrow> Norm s"
   153 
   154   Expr:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   155 				  G\<turnstile>Norm s0 \<midarrow>Expr e\<midarrow>n\<rightarrow> s1"
   156 
   157   Lab:  "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c \<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   158                              G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<midarrow>n\<rightarrow> abupd (absorb l) s1"
   159 
   160   Comp:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1 \<midarrow>n\<rightarrow> s1;
   161 	  G\<turnstile>     s1 \<midarrow>c2 \<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   162 				 G\<turnstile>Norm s0 \<midarrow>c1;; c2\<midarrow>n\<rightarrow> s2"
   163 
   164   If:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n\<rightarrow> s1;
   165 	  G\<turnstile>     s1\<midarrow>(if the_Bool b then c1 else c2)\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   166 		       G\<turnstile>Norm s0 \<midarrow>If(e) c1 Else c2 \<midarrow>n\<rightarrow> s2"
   167 
   168   Loop:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n\<rightarrow> s1;
   169 	  if normal s1 \<and> the_Bool b 
   170              then (G\<turnstile>s1 \<midarrow>c\<midarrow>n\<rightarrow> s2 \<and> 
   171                    G\<turnstile>(abupd (absorb (Cont l)) s2) \<midarrow>l\<bullet> While(e) c\<midarrow>n\<rightarrow> s3)
   172 	     else s3 = s1\<rbrakk> \<Longrightarrow>
   173 			      G\<turnstile>Norm s0 \<midarrow>l\<bullet> While(e) c\<midarrow>n\<rightarrow> s3"
   174   
   175   Do: "G\<turnstile>Norm s \<midarrow>Do j\<midarrow>n\<rightarrow> (Some (Jump j), s)"
   176   
   177   Throw:"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   178 				 G\<turnstile>Norm s0 \<midarrow>Throw e\<midarrow>n\<rightarrow> abupd (throw a') s1"
   179 
   180   Try:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2;
   181 	  if G,s2\<turnstile>catch tn then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<midarrow>n\<rightarrow> s3 else s3 = s2\<rbrakk>
   182           \<Longrightarrow>
   183 		  G\<turnstile>Norm s0 \<midarrow>Try c1 Catch(tn vn) c2\<midarrow>n\<rightarrow> s3"
   184 
   185   Fin:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n\<rightarrow> (x1,s1);
   186 	  G\<turnstile>Norm s1 \<midarrow>c2\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   187               G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<midarrow>n\<rightarrow> abupd (abrupt_if (x1\<noteq>None) x1) s2"
   188   
   189   Init:	"\<lbrakk>the (class G C) = c;
   190 	  if inited C (globs s0) then s3 = Norm s0
   191 	  else (G\<turnstile>Norm (init_class_obj G C s0)
   192 	          \<midarrow>(if C = Object then Skip else Init (super c))\<midarrow>n\<rightarrow> s1 \<and>
   193 	        G\<turnstile>set_lvars empty s1 \<midarrow>init c\<midarrow>n\<rightarrow> s2 \<and> 
   194                 s3 = restore_lvars s1 s2)\<rbrakk>
   195           \<Longrightarrow>
   196 		 G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s3"
   197 monos
   198   if_def2
   199 
   200 
   201 declare split_if     [split del] split_if_asm     [split del]
   202         option.split [split del] option.split_asm [split del]
   203 inductive_cases evaln_cases: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> vs'"
   204 
   205 inductive_cases evaln_elim_cases:
   206 	"G\<turnstile>(Some xc, s) \<midarrow>t                        \<succ>\<midarrow>n\<rightarrow> vs'"
   207 	"G\<turnstile>Norm s \<midarrow>In1r Skip                      \<succ>\<midarrow>n\<rightarrow> xs'"
   208         "G\<turnstile>Norm s \<midarrow>In1r (Do j)                    \<succ>\<midarrow>n\<rightarrow> xs'"
   209         "G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> c)                    \<succ>\<midarrow>n\<rightarrow> xs'"
   210 	"G\<turnstile>Norm s \<midarrow>In3  ([])                      \<succ>\<midarrow>n\<rightarrow> vs'"
   211 	"G\<turnstile>Norm s \<midarrow>In3  (e#es)                    \<succ>\<midarrow>n\<rightarrow> vs'"
   212 	"G\<turnstile>Norm s \<midarrow>In1l (Lit w)                   \<succ>\<midarrow>n\<rightarrow> vs'"
   213         "G\<turnstile>Norm s \<midarrow>In1l (UnOp unop e)             \<succ>\<midarrow>n\<rightarrow> vs'"
   214         "G\<turnstile>Norm s \<midarrow>In1l (BinOp binop e1 e2)       \<succ>\<midarrow>n\<rightarrow> vs'"
   215 	"G\<turnstile>Norm s \<midarrow>In2  (LVar vn)                 \<succ>\<midarrow>n\<rightarrow> vs'"
   216 	"G\<turnstile>Norm s \<midarrow>In1l (Cast T e)                \<succ>\<midarrow>n\<rightarrow> vs'"
   217 	"G\<turnstile>Norm s \<midarrow>In1l (e InstOf T)              \<succ>\<midarrow>n\<rightarrow> vs'"
   218 	"G\<turnstile>Norm s \<midarrow>In1l (Super)                   \<succ>\<midarrow>n\<rightarrow> vs'"
   219 	"G\<turnstile>Norm s \<midarrow>In1l (Acc va)                  \<succ>\<midarrow>n\<rightarrow> vs'"
   220 	"G\<turnstile>Norm s \<midarrow>In1r (Expr e)                  \<succ>\<midarrow>n\<rightarrow> xs'"
   221 	"G\<turnstile>Norm s \<midarrow>In1r (c1;; c2)                 \<succ>\<midarrow>n\<rightarrow> xs'"
   222 	"G\<turnstile>Norm s \<midarrow>In1l (Methd C sig)             \<succ>\<midarrow>n\<rightarrow> xs'"
   223 	"G\<turnstile>Norm s \<midarrow>In1l (Body D c)                \<succ>\<midarrow>n\<rightarrow> xs'"
   224 	"G\<turnstile>Norm s \<midarrow>In1l (e0 ? e1 : e2)            \<succ>\<midarrow>n\<rightarrow> vs'"
   225 	"G\<turnstile>Norm s \<midarrow>In1r (If(e) c1 Else c2)        \<succ>\<midarrow>n\<rightarrow> xs'"
   226 	"G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> While(e) c)           \<succ>\<midarrow>n\<rightarrow> xs'"
   227 	"G\<turnstile>Norm s \<midarrow>In1r (c1 Finally c2)           \<succ>\<midarrow>n\<rightarrow> xs'"
   228 	"G\<turnstile>Norm s \<midarrow>In1r (Throw e)                 \<succ>\<midarrow>n\<rightarrow> xs'"
   229 	"G\<turnstile>Norm s \<midarrow>In1l (NewC C)                  \<succ>\<midarrow>n\<rightarrow> vs'"
   230 	"G\<turnstile>Norm s \<midarrow>In1l (New T[e])                \<succ>\<midarrow>n\<rightarrow> vs'"
   231 	"G\<turnstile>Norm s \<midarrow>In1l (Ass va e)                \<succ>\<midarrow>n\<rightarrow> vs'"
   232 	"G\<turnstile>Norm s \<midarrow>In1r (Try c1 Catch(tn vn) c2)  \<succ>\<midarrow>n\<rightarrow> xs'"
   233 	"G\<turnstile>Norm s \<midarrow>In2  ({accC,statDeclC,stat}e..fn) \<succ>\<midarrow>n\<rightarrow> vs'"
   234 	"G\<turnstile>Norm s \<midarrow>In2  (e1.[e2])                 \<succ>\<midarrow>n\<rightarrow> vs'"
   235 	"G\<turnstile>Norm s \<midarrow>In1l ({accC,statT,mode}e\<cdot>mn({pT}p)) \<succ>\<midarrow>n\<rightarrow> vs'"
   236 	"G\<turnstile>Norm s \<midarrow>In1r (Init C)                  \<succ>\<midarrow>n\<rightarrow> xs'"
   237 declare split_if     [split] split_if_asm     [split] 
   238         option.split [split] option.split_asm [split]
   239 
   240 lemma evaln_Inj_elim: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (w,s') \<Longrightarrow> case t of In1 ec \<Rightarrow>  
   241   (case ec of Inl e \<Rightarrow> (\<exists>v. w = In1 v) | Inr c \<Rightarrow> w = \<diamondsuit>)  
   242   | In2 e \<Rightarrow> (\<exists>v. w = In2 v) | In3 e \<Rightarrow> (\<exists>v. w = In3 v)"
   243 apply (erule evaln_cases , auto)
   244 apply (induct_tac "t")
   245 apply   (induct_tac "a")
   246 apply auto
   247 done
   248 
   249 ML_setup {*
   250 fun enf nam inj rhs =
   251 let
   252   val name = "evaln_" ^ nam ^ "_eq"
   253   val lhs = "G\<turnstile>s \<midarrow>" ^ inj ^ " t\<succ>\<midarrow>n\<rightarrow> (w, s')"
   254   val () = qed_goal name (the_context()) (lhs ^ " = (" ^ rhs ^ ")") 
   255 	(K [Auto_tac, ALLGOALS (ftac (thm "evaln_Inj_elim")) THEN Auto_tac])
   256   fun is_Inj (Const (inj,_) $ _) = true
   257     | is_Inj _                   = false
   258   fun pred (_ $ (Const ("Pair",_) $ _ $ (Const ("Pair", _) $ _ $ 
   259     (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ x $ _ )))) $ _ ) = is_Inj x
   260 in
   261   make_simproc name lhs pred (thm name)
   262 end;
   263 
   264 val evaln_expr_proc = enf "expr" "In1l" "\<exists>v.  w=In1 v  \<and> G\<turnstile>s \<midarrow>t-\<succ>v \<midarrow>n\<rightarrow> s'";
   265 val evaln_var_proc  = enf "var"  "In2"  "\<exists>vf. w=In2 vf \<and> G\<turnstile>s \<midarrow>t=\<succ>vf\<midarrow>n\<rightarrow> s'";
   266 val evaln_exprs_proc= enf "exprs""In3"  "\<exists>vs. w=In3 vs \<and> G\<turnstile>s \<midarrow>t\<doteq>\<succ>vs\<midarrow>n\<rightarrow> s'";
   267 val evaln_stmt_proc = enf "stmt" "In1r" "     w=\<diamondsuit>      \<and> G\<turnstile>s \<midarrow>t     \<midarrow>n\<rightarrow> s'";
   268 Addsimprocs [evaln_expr_proc,evaln_var_proc,evaln_exprs_proc,evaln_stmt_proc];
   269 
   270 bind_thms ("evaln_AbruptIs", sum3_instantiate (thm "evaln.Abrupt"))
   271 *}
   272 declare evaln_AbruptIs [intro!]
   273 
   274 lemma evaln_Callee: "G\<turnstile>Norm s\<midarrow>In1l (Callee l e)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
   275 proof -
   276   { fix s t v s'
   277     assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
   278          normal: "normal s" and
   279          callee: "t=In1l (Callee l e)"
   280     then have "False"
   281     proof (induct)
   282     qed (auto)
   283   }
   284   then show ?thesis
   285     by (cases s') fastsimp 
   286 qed
   287 
   288 lemma evaln_InsInitE: "G\<turnstile>Norm s\<midarrow>In1l (InsInitE c e)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
   289 proof -
   290   { fix s t v s'
   291     assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
   292          normal: "normal s" and
   293          callee: "t=In1l (InsInitE c e)"
   294     then have "False"
   295     proof (induct)
   296     qed (auto)
   297   }
   298   then show ?thesis
   299     by (cases s') fastsimp
   300 qed
   301 
   302 lemma evaln_InsInitV: "G\<turnstile>Norm s\<midarrow>In2 (InsInitV c w)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
   303 proof -
   304   { fix s t v s'
   305     assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
   306          normal: "normal s" and
   307          callee: "t=In2 (InsInitV c w)"
   308     then have "False"
   309     proof (induct)
   310     qed (auto)
   311   }  
   312   then show ?thesis
   313     by (cases s') fastsimp
   314 qed
   315 
   316 lemma evaln_FinA: "G\<turnstile>Norm s\<midarrow>In1r (FinA a c)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
   317 proof -
   318   { fix s t v s'
   319     assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
   320          normal: "normal s" and
   321          callee: "t=In1r (FinA a c)"
   322     then have "False"
   323     proof (induct)
   324     qed (auto)
   325   } 
   326   then show ?thesis
   327     by (cases s') fastsimp
   328 qed
   329 
   330 lemma evaln_abrupt_lemma: "G\<turnstile>s \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (v,s') \<Longrightarrow> 
   331  fst s = Some xc \<longrightarrow> s' = s \<and> v = arbitrary3 e"
   332 apply (erule evaln_cases , auto)
   333 done
   334 
   335 lemma evaln_abrupt: 
   336  "\<And>s'. G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (w,s') = (s' = (Some xc,s) \<and>  
   337   w=arbitrary3 e \<and> G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (arbitrary3 e,(Some xc,s)))"
   338 apply auto
   339 apply (frule evaln_abrupt_lemma, auto)+
   340 done
   341 
   342 ML {*
   343 local
   344   fun is_Some (Const ("Pair",_) $ (Const ("Datatype.option.Some",_) $ _)$ _) =true
   345     | is_Some _ = false
   346   fun pred (_ $ (Const ("Pair",_) $
   347      _ $ (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ _ $
   348        (Const ("Pair", _) $ _ $ x)))) $ _ ) = is_Some x
   349 in
   350   val evaln_abrupt_proc = 
   351  make_simproc "evaln_abrupt" "G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (w,s')" pred (thm "evaln_abrupt")
   352 end;
   353 Addsimprocs [evaln_abrupt_proc]
   354 *}
   355 
   356 lemma evaln_LitI: "G\<turnstile>s \<midarrow>Lit v-\<succ>(if normal s then v else arbitrary)\<midarrow>n\<rightarrow> s"
   357 apply (case_tac "s", case_tac "a = None")
   358 by (auto intro!: evaln.Lit)
   359 
   360 lemma CondI: 
   361  "\<And>s1. \<lbrakk>G\<turnstile>s \<midarrow>e-\<succ>b\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow> 
   362   G\<turnstile>s \<midarrow>e ? e1 : e2-\<succ>(if normal s1 then v else arbitrary)\<midarrow>n\<rightarrow> s2"
   363 apply (case_tac "s", case_tac "a = None")
   364 by (auto intro!: evaln.Cond)
   365 
   366 lemma evaln_SkipI [intro!]: "G\<turnstile>s \<midarrow>Skip\<midarrow>n\<rightarrow> s"
   367 apply (case_tac "s", case_tac "a = None")
   368 by (auto intro!: evaln.Skip)
   369 
   370 lemma evaln_ExprI: "G\<turnstile>s \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s' \<Longrightarrow> G\<turnstile>s \<midarrow>Expr e\<midarrow>n\<rightarrow> s'"
   371 apply (case_tac "s", case_tac "a = None")
   372 by (auto intro!: evaln.Expr)
   373 
   374 lemma evaln_CompI: "\<lbrakk>G\<turnstile>s \<midarrow>c1\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c2\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow> G\<turnstile>s \<midarrow>c1;; c2\<midarrow>n\<rightarrow> s2"
   375 apply (case_tac "s", case_tac "a = None")
   376 by (auto intro!: evaln.Comp)
   377 
   378 lemma evaln_IfI: 
   379  "\<lbrakk>G\<turnstile>s \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>(if the_Bool v then c1 else c2)\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow> 
   380   G\<turnstile>s \<midarrow>If(e) c1 Else c2\<midarrow>n\<rightarrow> s2"
   381 apply (case_tac "s", case_tac "a = None")
   382 by (auto intro!: evaln.If)
   383 
   384 lemma evaln_SkipD [dest!]: "G\<turnstile>s \<midarrow>Skip\<midarrow>n\<rightarrow> s' \<Longrightarrow> s' = s" 
   385 by (erule evaln_cases, auto)
   386 
   387 lemma evaln_Skip_eq [simp]: "G\<turnstile>s \<midarrow>Skip\<midarrow>n\<rightarrow> s' = (s = s')"
   388 apply auto
   389 done
   390 
   391 lemma evaln_eval:  
   392   assumes evaln: "G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)" and
   393              wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T" and  
   394         conf_s0: "s0\<Colon>\<preceq>(G, L)" and
   395              wf: "wf_prog G" 
   396        
   397   shows "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"
   398 proof -
   399   from evaln 
   400   show "\<And> L accC T. \<lbrakk>s0\<Colon>\<preceq>(G, L);\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T\<rbrakk>
   401                     \<Longrightarrow> G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"
   402        (is "PROP ?EqEval s0 s1 t v")
   403   proof (induct)
   404     case Abrupt
   405     show ?case by (rule eval.Abrupt)
   406   next
   407     case LVar
   408     show ?case by (rule eval.LVar)
   409   next
   410     case (FVar a accC' e fn n s0 s1 s2 s2' stat statDeclC v L accC T)
   411     have eval_initn: "G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<midarrow>n\<rightarrow> s1" .
   412     have eval_en: "G\<turnstile>s1 \<midarrow>e-\<succ>a\<midarrow>n\<rightarrow> s2" .
   413     have hyp_init: "PROP ?EqEval (Norm s0) s1 (In1r (Init statDeclC)) \<diamondsuit>" .
   414     have hyp_e: "PROP ?EqEval s1 s2 (In1l e) (In1 a)" .
   415     have fvar: "(v, s2') = fvar statDeclC stat fn a s2" .
   416     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
   417     have wt: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>In2 ({accC',statDeclC,stat}e..fn)\<Colon>T" .
   418     then obtain statC f where
   419                 wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-Class statC" and
   420             accfield: "accfield G accC statC fn = Some (statDeclC,f)" and
   421                 stat: "stat=is_static f" and
   422                accC': "accC'=accC" and
   423 	           T: "T=(Inl (type f))"
   424        by (rule wt_elim_cases) (auto simp add: member_is_static_simp)
   425     from wf wt_e 
   426     have iscls_statC: "is_class G statC"
   427       by (auto dest: ty_expr_is_type type_is_class)
   428     with wf accfield 
   429     have iscls_statDeclC: "is_class G statDeclC"
   430       by (auto dest!: accfield_fields dest: fields_declC)
   431     then 
   432     have wt_init: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>(Init statDeclC)\<Colon>\<surd>"
   433       by simp
   434     from conf_s0 wt_init
   435     have eval_init: "G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<rightarrow> s1"
   436       by (rule hyp_init)
   437     with wt_init conf_s0 wf 
   438     have conf_s1: "s1\<Colon>\<preceq>(G, L)"
   439       by (blast dest: exec_ts)
   440     with hyp_e wt_e
   441     have eval_e: "G\<turnstile>s1 \<midarrow>e-\<succ>a\<rightarrow> s2"
   442       by blast
   443     with wf conf_s1 wt_e
   444     obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and
   445             conf_a: "normal s2 \<longrightarrow> G,store s2\<turnstile>a\<Colon>\<preceq>Class statC"
   446       by (auto dest!: eval_type_sound)
   447     obtain s3 where
   448       check: "s3 = check_field_access G accC statDeclC fn stat a s2'"
   449       by simp
   450     from accfield wt_e eval_init eval_e conf_s2 conf_a fvar stat check  wf
   451     have eq_s3_s2': "s3=s2'"  
   452       by (auto dest!: error_free_field_access)
   453     with eval_init eval_e fvar check accC'
   454     show "G\<turnstile>Norm s0 \<midarrow>{accC',statDeclC,stat}e..fn=\<succ>v\<rightarrow> s2'"
   455       by (auto intro: eval.FVar)
   456   next
   457     case AVar
   458     with wf show ?case
   459       apply -
   460       apply (erule wt_elim_cases)
   461       apply (blast intro!: eval.AVar dest: eval_type_sound)
   462       done
   463   next
   464     case NewC
   465     with wf show ?case
   466       apply - 
   467       apply (erule wt_elim_cases)
   468       apply (blast intro!: eval.NewC dest: eval_type_sound is_acc_classD)
   469       done
   470   next
   471     case (NewA T a e i n s0 s1 s2 s3 L accC Ta) 
   472     have hyp_init: "PROP ?EqEval (Norm s0) s1 (In1r (init_comp_ty T)) \<diamondsuit>" .
   473     have hyp_size: "PROP ?EqEval s1 s2 (In1l e) (In1 i)" .
   474     have "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (New T[e])\<Colon>Ta" .
   475     then obtain
   476        wt_init: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>init_comp_ty T\<Colon>\<surd>" and
   477        wt_size: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-PrimT Integer"
   478       by (rule wt_elim_cases) (auto intro: wt_init_comp_ty dest: is_acc_typeD)
   479     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
   480     from this wt_init 
   481     have eval_init: "G\<turnstile>Norm s0 \<midarrow>init_comp_ty T\<rightarrow> s1"
   482       by (rule hyp_init)
   483     moreover
   484     from eval_init wt_init wf conf_s0
   485     have "s1\<Colon>\<preceq>(G, L)"
   486       by (auto dest: eval_type_sound)
   487     from this wt_size 
   488     have "G\<turnstile>s1 \<midarrow>e-\<succ>i\<rightarrow> s2"
   489       by (rule hyp_size)
   490     moreover note NewA
   491     ultimately show ?case
   492       by (blast intro!: eval.NewA)
   493   next
   494     case Cast
   495     with wf show ?case
   496       by - (erule wt_elim_cases, rule eval.Cast,auto dest: eval_type_sound)
   497   next
   498     case Inst
   499     with wf show ?case
   500       by - (erule wt_elim_cases, rule eval.Inst,auto dest: eval_type_sound)
   501   next
   502     case Lit
   503     show ?case by (rule eval.Lit)
   504   next
   505     case UnOp
   506     with wf show ?case
   507       by - (erule wt_elim_cases, rule eval.UnOp,auto dest: eval_type_sound)
   508   next
   509     case BinOp
   510     with wf show ?case
   511       by - (erule wt_elim_cases, blast intro!: eval.BinOp dest: eval_type_sound)
   512   next
   513     case Super
   514     show ?case by (rule eval.Super)
   515   next
   516     case Acc
   517     then show ?case
   518       by - (erule wt_elim_cases, rule eval.Acc,auto dest: eval_type_sound)
   519   next
   520     case Ass
   521     with wf show ?case
   522       by - (erule wt_elim_cases, blast intro!: eval.Ass dest: eval_type_sound) 
   523   next
   524     case (Cond b e0 e1 e2 n s0 s1 s2 v L accC T)
   525     have hyp_e0: "PROP ?EqEval (Norm s0) s1 (In1l e0) (In1 b)" .
   526     have hyp_if: "PROP ?EqEval s1 s2 
   527                               (In1l (if the_Bool b then e1 else e2)) (In1 v)" .
   528     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
   529     have wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (e0 ? e1 : e2)\<Colon>T" .
   530     then obtain T1 T2 statT where
   531        wt_e0: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e0\<Colon>-PrimT Boolean" and
   532        wt_e1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e1\<Colon>-T1" and
   533        wt_e2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e2\<Colon>-T2" and 
   534        statT: "G\<turnstile>T1\<preceq>T2 \<and> statT = T2  \<or>  G\<turnstile>T2\<preceq>T1 \<and> statT =  T1" and
   535        T    : "T=Inl statT"
   536       by (rule wt_elim_cases) auto
   537     from conf_s0 wt_e0
   538     have eval_e0: "G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1"
   539       by (rule hyp_e0)
   540     moreover
   541     from eval_e0 conf_s0 wf wt_e0
   542     have "s1\<Colon>\<preceq>(G, L)"
   543       by (blast dest: eval_type_sound)
   544     with wt_e1 wt_e2 statT hyp_if
   545     have "G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<rightarrow> s2"
   546       by (cases "the_Bool b") auto
   547     ultimately
   548     show ?case
   549       by (rule eval.Cond)
   550   next
   551     case (Call invDeclC a' accC' args e mn mode n pTs' s0 s1 s2 s4 statT 
   552            v vs L accC T)
   553     txt {* Repeats large parts of the type soundness proof. One should factor
   554       out some lemmata about the relations and conformance of @{text
   555       s2}, @{text s3} and @{text s3'} *}
   556     have evaln_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n\<rightarrow> s1" .
   557     have evaln_args: "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<midarrow>n\<rightarrow> s2" .
   558     have invDeclC: "invDeclC 
   559                       = invocation_declclass G mode (store s2) a' statT 
   560                            \<lparr>name = mn, parTs = pTs'\<rparr>" .
   561     let ?InitLvars 
   562          = "init_lvars G invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> mode a' vs s2"
   563     obtain s3 s3' where 
   564       init_lvars: "s3 = 
   565              init_lvars G invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> mode a' vs s2" and
   566       check: "s3' =
   567          check_method_access G accC' statT mode \<lparr>name = mn, parTs = pTs'\<rparr> a' s3"
   568       by simp
   569     have evaln_methd: 
   570      "G\<turnstile>?InitLvars \<midarrow>Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>-\<succ>v\<midarrow>n\<rightarrow> s4" .
   571     have     hyp_e: "PROP ?EqEval (Norm s0) s1 (In1l e) (In1 a')" .
   572     have  hyp_args: "PROP ?EqEval s1 s2 (In3 args) (In3 vs)" .
   573     have hyp_methd: "PROP ?EqEval ?InitLvars s4 
   574               (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)) (In1 v)".
   575     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
   576     have      wt: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>
   577                     \<turnstile>In1l ({accC',statT,mode}e\<cdot>mn( {pTs'}args))\<Colon>T" .
   578     from wt obtain pTs statDeclT statM where
   579                  wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT" and
   580               wt_args: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>args\<Colon>\<doteq>pTs" and
   581                 statM: "max_spec G accC statT \<lparr>name=mn,parTs=pTs\<rparr> 
   582                          = {((statDeclT,statM),pTs')}" and
   583                  mode: "mode = invmode statM e" and
   584                     T: "T =Inl (resTy statM)" and
   585         eq_accC_accC': "accC=accC'"
   586       by (rule wt_elim_cases) auto
   587     from conf_s0 wt_e hyp_e
   588     have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1"
   589       by blast
   590     with wf conf_s0 wt_e
   591     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and
   592            conf_a': "normal s1 \<Longrightarrow> G, store s1\<turnstile>a'\<Colon>\<preceq>RefT statT" 
   593       by (auto dest!: eval_type_sound)
   594     from conf_s1 wt_args hyp_args
   595     have eval_args: "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<rightarrow> s2"
   596       by blast
   597     with wt_args conf_s1 wf 
   598     obtain    conf_s2: "s2\<Colon>\<preceq>(G, L)" and
   599             conf_args: "normal s2 
   600                          \<Longrightarrow>  list_all2 (conf G (store s2)) vs pTs" 
   601       by (auto dest!: eval_type_sound)
   602     from statM 
   603     obtain
   604        statM': "(statDeclT,statM)\<in>mheads G accC statT \<lparr>name=mn,parTs=pTs'\<rparr>" and
   605        pTs_widen: "G\<turnstile>pTs[\<preceq>]pTs'"
   606       by (blast dest: max_spec2mheads)
   607     from check
   608     have eq_store_s3'_s3: "store s3'=store s3"
   609       by (cases s3) (simp add: check_method_access_def Let_def)
   610     obtain invC
   611       where invC: "invC = invocation_class mode (store s2) a' statT"
   612       by simp
   613     with init_lvars
   614     have invC': "invC = (invocation_class mode (store s3) a' statT)"
   615       by (cases s2,cases mode) (auto simp add: init_lvars_def2 )
   616     show "G\<turnstile>Norm s0 \<midarrow>{accC',statT,mode}e\<cdot>mn( {pTs'}args)
   617              -\<succ>v\<rightarrow> (set_lvars (locals (store s2))) s4"
   618     proof (cases "normal s2")
   619       case False
   620       with init_lvars 
   621       obtain keep_abrupt: "abrupt s3 = abrupt s2" and
   622              "store s3 = store (init_lvars G invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> 
   623                                             mode a' vs s2)" 
   624 	by (auto simp add: init_lvars_def2)
   625       moreover
   626       from keep_abrupt False check
   627       have eq_s3'_s3: "s3'=s3" 
   628 	by (auto simp add: check_method_access_def Let_def)
   629       moreover
   630       from eq_s3'_s3 False keep_abrupt evaln_methd init_lvars
   631       obtain "s4=s3'"
   632       "In1 v=arbitrary3 (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>))"
   633 	by auto
   634       moreover note False
   635       ultimately have
   636 	"G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>-\<succ>v\<rightarrow> s4"
   637 	by (auto)
   638       from eval_e eval_args invDeclC init_lvars check this
   639       show ?thesis
   640 	by (rule eval.Call)
   641     next
   642       case True
   643       note normal_s2 = True
   644       with eval_args
   645       have normal_s1: "normal s1"
   646 	by (cases "normal s1") auto
   647       with conf_a' eval_args 
   648       have conf_a'_s2: "G, store s2\<turnstile>a'\<Colon>\<preceq>RefT statT"
   649 	by (auto dest: eval_gext intro: conf_gext)
   650       show ?thesis
   651       proof (cases "a'=Null \<longrightarrow> is_static statM")
   652 	case False
   653 	then obtain not_static: "\<not> is_static statM" and Null: "a'=Null" 
   654 	  by blast
   655 	with normal_s2 init_lvars mode
   656 	obtain np: "abrupt s3 = Some (Xcpt (Std NullPointer))" and
   657                    "store s3 = store (init_lvars G invDeclC 
   658                                        \<lparr>name = mn, parTs = pTs'\<rparr> mode a' vs s2)"
   659 	  by (auto simp add: init_lvars_def2)
   660 	moreover
   661 	from np check
   662 	have eq_s3'_s3: "s3'=s3" 
   663 	  by (auto simp add: check_method_access_def Let_def)
   664 	moreover
   665 	from eq_s3'_s3 np evaln_methd init_lvars
   666 	obtain "s4=s3'"
   667       "In1 v=arbitrary3 (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>))"
   668 	  by auto
   669 	moreover note np 
   670 	ultimately have
   671 	  "G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>-\<succ>v\<rightarrow> s4"
   672 	  by (auto)
   673 	from eval_e eval_args invDeclC init_lvars check this
   674 	show ?thesis
   675 	  by (rule eval.Call)
   676       next
   677 	case True
   678 	with mode have notNull: "mode = IntVir \<longrightarrow> a' \<noteq> Null"
   679 	  by (auto dest!: Null_staticD)
   680 	with conf_s2 conf_a'_s2 wf invC 
   681 	have dynT_prop: "G\<turnstile>mode\<rightarrow>invC\<preceq>statT"
   682 	  by (cases s2) (auto intro: DynT_propI)
   683 	with wt_e statM' invC mode wf 
   684 	obtain dynM where 
   685            dynM: "dynlookup G statT invC  \<lparr>name=mn,parTs=pTs'\<rparr> = Some dynM" and
   686            acc_dynM: "G \<turnstile>Methd  \<lparr>name=mn,parTs=pTs'\<rparr> dynM 
   687                           in invC dyn_accessible_from accC"
   688 	  by (force dest!: call_access_ok)
   689 	with invC' check eq_accC_accC'
   690 	have eq_s3'_s3: "s3'=s3"
   691 	  by (auto simp add: check_method_access_def Let_def)
   692 	from dynT_prop wf wt_e statM' mode invC invDeclC dynM 
   693 	obtain 
   694 	   wf_dynM: "wf_mdecl G invDeclC (\<lparr>name=mn,parTs=pTs'\<rparr>,mthd dynM)" and
   695 	     dynM': "methd G invDeclC \<lparr>name=mn,parTs=pTs'\<rparr> = Some dynM" and
   696            iscls_invDeclC: "is_class G invDeclC" and
   697 	        invDeclC': "invDeclC = declclass dynM" and
   698 	     invC_widen: "G\<turnstile>invC\<preceq>\<^sub>C invDeclC" and
   699 	   is_static_eq: "is_static dynM = is_static statM" and
   700 	   involved_classes_prop:
   701              "(if invmode statM e = IntVir
   702                then \<forall>statC. statT = ClassT statC \<longrightarrow> G\<turnstile>invC\<preceq>\<^sub>C statC
   703                else ((\<exists>statC. statT = ClassT statC \<and> G\<turnstile>statC\<preceq>\<^sub>C invDeclC) \<or>
   704                      (\<forall>statC. statT \<noteq> ClassT statC \<and> invDeclC = Object)) \<and>
   705                       statDeclT = ClassT invDeclC)"
   706 	  by (auto dest: DynT_mheadsD)
   707 	obtain L' where 
   708 	   L':"L'=(\<lambda> k. 
   709                  (case k of
   710                     EName e
   711                     \<Rightarrow> (case e of 
   712                           VNam v 
   713                           \<Rightarrow>(table_of (lcls (mbody (mthd dynM)))
   714                              (pars (mthd dynM)[\<mapsto>]pTs')) v
   715                         | Res \<Rightarrow> Some (resTy dynM))
   716                   | This \<Rightarrow> if is_static statM 
   717                             then None else Some (Class invDeclC)))"
   718 	  by simp
   719 	from wf_dynM [THEN wf_mdeclD1, THEN conjunct1] normal_s2 conf_s2 wt_e
   720               wf eval_args conf_a' mode notNull wf_dynM involved_classes_prop
   721 	have conf_s3: "s3\<Colon>\<preceq>(G,L')"
   722 	   apply - 
   723           (*FIXME confomrs_init_lvars should be 
   724                 adjusted to be more directy applicable *)
   725 	   apply (drule conforms_init_lvars [of G invDeclC 
   726                   "\<lparr>name=mn,parTs=pTs'\<rparr>" dynM "store s2" vs pTs "abrupt s2" 
   727                   L statT invC a' "(statDeclT,statM)" e])
   728 	     apply (rule wf)
   729 	     apply (rule conf_args,assumption)
   730 	     apply (simp add: pTs_widen)
   731 	     apply (cases s2,simp)
   732 	     apply (rule dynM')
   733 	     apply (force dest: ty_expr_is_type)
   734 	     apply (rule invC_widen)
   735 	     apply (force intro: conf_gext dest: eval_gext)
   736 	     apply simp
   737 	     apply simp
   738 	     apply (simp add: invC)
   739 	     apply (simp add: invDeclC)
   740 	     apply (force dest: wf_mdeclD1 is_acc_typeD)
   741 	     apply (cases s2, simp add: L' init_lvars
   742 	                      cong add: lname.case_cong ename.case_cong)
   743 	   done
   744 	from is_static_eq wf_dynM L'
   745 	obtain mthdT where
   746 	   "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>
   747             \<turnstile>Body invDeclC (stmt (mbody (mthd dynM)))\<Colon>-mthdT" and
   748 	   mthdT_widen: "G\<turnstile>mthdT\<preceq>resTy dynM"
   749 	  by - (drule wf_mdecl_bodyD,
   750                 auto simp: cong add: lname.case_cong ename.case_cong)
   751 	with dynM' iscls_invDeclC invDeclC'
   752 	have
   753 	   "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>
   754             \<turnstile>(Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)\<Colon>-mthdT"
   755 	  by (auto intro: wt.Methd)
   756 	with conf_s3 hyp_methd init_lvars eq_s3'_s3
   757 	have "G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>-\<succ>v\<rightarrow> s4"
   758 	  by auto
   759 	from eval_e eval_args invDeclC init_lvars check this
   760 	show ?thesis
   761 	  by (rule eval.Call)
   762       qed
   763     qed
   764   next
   765     case Methd
   766     with wf show ?case
   767       by - (erule wt_elim_cases, rule eval.Methd, 
   768             auto dest: eval_type_sound simp add: body_def2)
   769   next
   770     case Body
   771     with wf show ?case
   772        by - (erule wt_elim_cases, blast intro!: eval.Body dest: eval_type_sound)
   773   next
   774     case Nil
   775     show ?case by (rule eval.Nil)
   776   next
   777     case Cons
   778     with wf show ?case
   779       by - (erule wt_elim_cases, blast intro!: eval.Cons dest: eval_type_sound)
   780   next
   781     case Skip
   782     show ?case by (rule eval.Skip)
   783   next
   784     case Expr
   785     with wf show ?case
   786       by - (erule wt_elim_cases, rule eval.Expr,auto dest: eval_type_sound)
   787   next
   788     case Lab
   789     with wf show ?case
   790       by - (erule wt_elim_cases, rule eval.Lab,auto dest: eval_type_sound)
   791   next
   792     case Comp
   793     with wf show ?case
   794       by - (erule wt_elim_cases, blast intro!: eval.Comp dest: eval_type_sound)
   795   next
   796     case (If b c1 c2 e n s0 s1 s2 L accC T)
   797     have hyp_e: "PROP ?EqEval (Norm s0) s1 (In1l e) (In1 b)" .
   798     have hyp_then_else: 
   799       "PROP ?EqEval s1 s2 (In1r (if the_Bool b then c1 else c2)) \<diamondsuit>" .
   800     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
   801     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (If(e) c1 Else c2)\<Colon>T" .
   802     then obtain 
   803               wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean" and
   804       wt_then_else: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(if the_Bool b then c1 else c2)\<Colon>\<surd>"
   805       by (rule wt_elim_cases) (auto split add: split_if)
   806     from conf_s0 wt_e
   807     have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1"
   808       by (rule hyp_e)
   809     moreover
   810     from eval_e wt_e conf_s0 wf
   811     have "s1\<Colon>\<preceq>(G, L)"
   812       by (blast dest: eval_type_sound)
   813     from this wt_then_else
   814     have "G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2"
   815       by (rule hyp_then_else)
   816     ultimately
   817     show ?case
   818       by (rule eval.If)
   819   next
   820     case (Loop b c e l n s0 s1 s2 s3 L accC T)
   821     have hyp_e: "PROP ?EqEval (Norm s0) s1 (In1l e) (In1 b)" .
   822     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
   823     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (l\<bullet> While(e) c)\<Colon>T" .
   824     then obtain wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean" and
   825                 wt_c: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c\<Colon>\<surd>"
   826       by (rule wt_elim_cases) (blast)
   827     from conf_s0 wt_e 
   828     have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1"
   829       by (rule hyp_e)
   830     moreover
   831     from eval_e wt_e conf_s0 wf
   832     have conf_s1: "s1\<Colon>\<preceq>(G, L)"
   833       by (blast dest: eval_type_sound)
   834     have "if normal s1 \<and> the_Bool b 
   835              then (G\<turnstile>s1 \<midarrow>c\<rightarrow> s2 \<and> 
   836                    G\<turnstile>(abupd (absorb (Cont l)) s2) \<midarrow>l\<bullet> While(e) c\<rightarrow> s3)
   837 	     else s3 = s1"
   838     proof (cases "normal s1 \<and> the_Bool b")
   839       case True 
   840       from Loop True have hyp_c: "PROP ?EqEval s1 s2 (In1r c) \<diamondsuit>"
   841 	by (auto)
   842       from Loop True have hyp_w: "PROP ?EqEval (abupd (absorb (Cont l)) s2)
   843                                         s3 (In1r (l\<bullet> While(e) c)) \<diamondsuit>"
   844 	by (auto)
   845       from conf_s1 wt_c
   846       have eval_c: "G\<turnstile>s1 \<midarrow>c\<rightarrow> s2"
   847 	by (rule hyp_c)
   848       moreover
   849       from eval_c conf_s1 wt_c wf
   850       have "s2\<Colon>\<preceq>(G, L)"
   851 	by (blast dest: eval_type_sound)
   852       then
   853       have "abupd (absorb (Cont l)) s2 \<Colon>\<preceq>(G, L)"
   854 	by (cases s2) (auto intro: conforms_absorb)
   855       from this and wt
   856       have "G\<turnstile>abupd (absorb (Cont l)) s2 \<midarrow>l\<bullet> While(e) c\<rightarrow> s3"
   857 	by (rule hyp_w)
   858       moreover note True
   859       ultimately
   860       show ?thesis
   861 	by simp
   862     next
   863       case False
   864       with Loop have "s3 = s1" by simp
   865       with False
   866       show ?thesis 
   867 	by auto
   868     qed
   869     ultimately
   870     show ?case
   871       by (rule eval.Loop)
   872   next
   873     case Do
   874     show ?case by (rule eval.Do)
   875   next
   876     case Throw
   877     with wf show ?case
   878       by - (erule wt_elim_cases, rule eval.Throw,auto dest: eval_type_sound)
   879   next
   880     case (Try c1 c2 n s0 s1 s2 s3 catchC vn L accC T)
   881     have  hyp_c1: "PROP ?EqEval (Norm s0) s1 (In1r c1) \<diamondsuit>" .
   882     have conf_s0:"Norm s0\<Colon>\<preceq>(G, L)" .
   883     have      wt:"\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>In1r (Try c1 Catch(catchC vn) c2)\<Colon>T" .
   884     then obtain 
   885       wt_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
   886       wt_c2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<lparr>lcl := L(VName vn\<mapsto>Class catchC)\<rparr>\<turnstile>c2\<Colon>\<surd>"
   887       by (rule wt_elim_cases) (auto)
   888     from conf_s0 wt_c1
   889     have eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1"
   890       by (rule hyp_c1)
   891     moreover
   892     have sxalloc: "G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2" .
   893     moreover
   894     from eval_c1 wt_c1 conf_s0 wf
   895     have "s1\<Colon>\<preceq>(G, L)"
   896       by (blast dest: eval_type_sound)
   897     with sxalloc wf
   898     have conf_s2: "s2\<Colon>\<preceq>(G, L)" 
   899       by (auto dest: sxalloc_type_sound split: option.splits)
   900     have "if G,s2\<turnstile>catch catchC then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<rightarrow> s3 else s3 = s2"
   901     proof (cases "G,s2\<turnstile>catch catchC")
   902       case True
   903       note Catch = this
   904       with Try have hyp_c2: "PROP ?EqEval (new_xcpt_var vn s2) s3 (In1r c2) \<diamondsuit>"
   905 	by auto
   906       show ?thesis
   907       proof (cases "normal s1")
   908 	case True
   909 	with sxalloc wf 
   910 	have eq_s2_s1: "s2=s1"
   911 	  by (auto dest: sxalloc_type_sound split: option.splits)
   912 	with True 
   913 	have "\<not>  G,s2\<turnstile>catch catchC"
   914 	  by (simp add: catch_def)
   915 	with Catch show ?thesis 
   916 	  by (contradiction)
   917       next 
   918 	case False
   919 	with sxalloc wf
   920 	obtain a 
   921 	  where xcpt_s2: "abrupt s2 = Some (Xcpt (Loc a))"
   922 	  by (auto dest!: sxalloc_type_sound split: option.splits)
   923 	with Catch
   924 	have "G\<turnstile>obj_ty (the (globs (store s2) (Heap a)))\<preceq>Class catchC"
   925 	  by (cases s2) simp
   926 	with xcpt_s2 conf_s2 wf 
   927 	have "new_xcpt_var vn s2\<Colon>\<preceq>(G, L(VName vn\<mapsto>Class catchC))"
   928 	  by (auto dest: Try_lemma)
   929 	from this wt_c2
   930 	have "G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<rightarrow> s3"
   931 	  by (auto intro: hyp_c2)
   932 	with Catch 
   933 	show ?thesis
   934 	  by simp
   935       qed
   936     next
   937       case False
   938       with Try
   939       have "s3=s2"
   940 	by simp
   941       with False
   942       show ?thesis
   943 	by simp
   944     qed
   945     ultimately
   946     show ?case
   947       by (rule eval.Try)
   948   next
   949     case (Fin c1 c2 n s0 s1 s2 x1 L accC T)
   950     have hyp_c1: "PROP ?EqEval (Norm s0) (x1,s1) (In1r c1) \<diamondsuit>" .
   951     have hyp_c2: "PROP ?EqEval (Norm s1) (s2) (In1r c2) \<diamondsuit>" .
   952     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
   953     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (c1 Finally c2)\<Colon>T" .
   954     then obtain
   955       wt_c1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
   956       wt_c2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c2\<Colon>\<surd>" 
   957       by (rule wt_elim_cases) blast
   958     from conf_s0 wt_c1
   959     have eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1, s1)"
   960       by (rule hyp_c1)
   961     with wf wt_c1 conf_s0
   962     obtain       conf_s1: "Norm s1\<Colon>\<preceq>(G, L)" and 
   963            error_free_s1: "error_free (x1,s1)"
   964       by (auto dest!: eval_type_sound intro: conforms_NormI)
   965     from conf_s1 wt_c2
   966     have eval_c2: "G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2"
   967       by (rule hyp_c2)
   968     with eval_c1 error_free_s1
   969     show "G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<rightarrow> abupd (abrupt_if (x1 \<noteq> None) x1) s2"
   970       by (auto intro: eval.Fin simp add: error_free_def)
   971   next
   972     case (Init C c n s0 s1 s2 s3 L accC T)
   973     have     cls: "the (class G C) = c" .
   974     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
   975     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (Init C)\<Colon>T" .
   976     with cls
   977     have cls_C: "class G C = Some c"
   978       by - (erule wt_elim_cases,auto)
   979     have "if inited C (globs s0) then s3 = Norm s0
   980 	  else (G\<turnstile>Norm (init_class_obj G C s0) 
   981 		  \<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1 \<and>
   982 	       G\<turnstile>set_lvars empty s1 \<midarrow>init c\<rightarrow> s2 \<and> s3 = restore_lvars s1 s2)"
   983     proof (cases "inited C (globs s0)")
   984       case True
   985       with Init have "s3 = Norm s0"
   986 	by simp
   987       with True show ?thesis 
   988 	by simp
   989     next
   990       case False
   991       with Init
   992       obtain 
   993 	hyp_init_super: 
   994         "PROP ?EqEval (Norm ((init_class_obj G C) s0)) s1
   995 	               (In1r (if C = Object then Skip else Init (super c))) \<diamondsuit>"
   996 	and 
   997         hyp_init_c:
   998 	   "PROP ?EqEval ((set_lvars empty) s1) s2 (In1r (init c)) \<diamondsuit>" and
   999 	s3: "s3 = (set_lvars (locals (store s1))) s2"
  1000 	by (simp only: if_False)
  1001       from conf_s0 wf cls_C False
  1002       have conf_s0': "(Norm ((init_class_obj G C) s0))\<Colon>\<preceq>(G, L)"
  1003 	by (auto dest: conforms_init_class_obj)
  1004       moreover
  1005       from wf cls_C 
  1006       have wt_init_super:
  1007            "\<lparr>prg = G, cls = accC, lcl = L\<rparr>
  1008                   \<turnstile>(if C = Object then Skip else Init (super c))\<Colon>\<surd>"
  1009 	by (cases "C=Object")
  1010            (auto dest: wf_prog_cdecl wf_cdecl_supD is_acc_classD)
  1011       ultimately
  1012       have eval_init_super: 
  1013 	   "G\<turnstile>Norm ((init_class_obj G C) s0) 
  1014             \<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1"
  1015 	by (rule hyp_init_super)
  1016       with conf_s0' wt_init_super wf
  1017       have "s1\<Colon>\<preceq>(G, L)"
  1018 	by (blast dest: eval_type_sound)
  1019       then
  1020       have "(set_lvars empty) s1\<Colon>\<preceq>(G, empty)"
  1021 	by (cases s1) (auto dest: conforms_set_locals )
  1022       with wf cls_C 
  1023       have eval_init_c: "G\<turnstile>(set_lvars empty) s1 \<midarrow>init c\<rightarrow> s2"
  1024 	by (auto intro!: hyp_init_c dest: wf_prog_cdecl wf_cdecl_wt_init)
  1025       from False eval_init_super eval_init_c s3
  1026       show ?thesis
  1027 	by simp
  1028     qed
  1029     with cls show ?case
  1030       by (rule eval.Init)
  1031   qed 
  1032 qed
  1033 
  1034 lemma Suc_le_D_lemma: "\<lbrakk>Suc n <= m'; (\<And>m. n <= m \<Longrightarrow> P (Suc m)) \<rbrakk> \<Longrightarrow> P m'"
  1035 apply (frule Suc_le_D)
  1036 apply fast
  1037 done
  1038 
  1039 lemma evaln_nonstrict [rule_format (no_asm), elim]: 
  1040   "\<And>ws. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> ws \<Longrightarrow> \<forall>m. n\<le>m \<longrightarrow> G\<turnstile>s \<midarrow>t\<succ>\<midarrow>m\<rightarrow> ws"
  1041 apply (simp (no_asm_simp) only: split_tupled_all)
  1042 apply (erule evaln.induct)
  1043 apply (tactic {* ALLGOALS (EVERY'[strip_tac, TRY o etac (thm "Suc_le_D_lemma"),
  1044   REPEAT o smp_tac 1, 
  1045   resolve_tac (thms "evaln.intros") THEN_ALL_NEW TRY o atac]) *})
  1046 (* 3 subgoals *)
  1047 apply (auto split del: split_if)
  1048 done
  1049 
  1050 lemmas evaln_nonstrict_Suc = evaln_nonstrict [OF _ le_refl [THEN le_SucI]]
  1051 
  1052 lemma evaln_max2: "\<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>n1\<rightarrow> ws1; G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>n2\<rightarrow> ws2\<rbrakk> \<Longrightarrow> 
  1053              G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max n1 n2\<rightarrow> ws1 \<and> G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max n1 n2\<rightarrow> ws2"
  1054 apply (fast intro: le_maxI1 le_maxI2)
  1055 done
  1056 
  1057 lemma evaln_max3: 
  1058 "\<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>n1\<rightarrow> ws1; G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>n2\<rightarrow> ws2; G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>n3\<rightarrow> ws3\<rbrakk> \<Longrightarrow>
  1059  G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> ws1 \<and>
  1060  G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> ws2 \<and> 
  1061  G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> ws3"
  1062 apply (drule (1) evaln_max2, erule thin_rl)
  1063 apply (fast intro!: le_maxI1 le_maxI2)
  1064 done
  1065 
  1066 lemma le_max3I1: "(n2::nat) \<le> max n1 (max n2 n3)"
  1067 proof -
  1068   have "n2 \<le> max n2 n3"
  1069     by (rule le_maxI1)
  1070   also
  1071   have "max n2 n3 \<le> max n1 (max n2 n3)"
  1072     by (rule le_maxI2)
  1073   finally
  1074   show ?thesis .
  1075 qed
  1076 
  1077 lemma le_max3I2: "(n3::nat) \<le> max n1 (max n2 n3)"
  1078 proof -
  1079   have "n3 \<le> max n2 n3"
  1080     by (rule le_maxI2)
  1081   also
  1082   have "max n2 n3 \<le> max n1 (max n2 n3)"
  1083     by (rule le_maxI2)
  1084   finally
  1085   show ?thesis .
  1086 qed
  1087 
  1088 lemma eval_evaln: 
  1089   assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" and
  1090             wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T" and  
  1091        conf_s0: "s0\<Colon>\<preceq>(G, L)" and
  1092             wf: "wf_prog G"  
  1093   shows  "\<exists>n. G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)"
  1094 proof -
  1095   from eval 
  1096   show "\<And> L accC T. \<lbrakk>s0\<Colon>\<preceq>(G, L);\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T\<rbrakk>
  1097                      \<Longrightarrow> \<exists> n. G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)"
  1098        (is "PROP ?EqEval s0 s1 t v")
  1099   proof (induct)
  1100     case (Abrupt s t xc L accC T)
  1101     obtain n where
  1102       "G\<turnstile>(Some xc, s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (arbitrary3 t, Some xc, s)"
  1103       by (rules intro: evaln.Abrupt)
  1104     then show ?case ..
  1105   next
  1106     case Skip
  1107     show ?case by (blast intro: evaln.Skip)
  1108   next
  1109     case (Expr e s0 s1 v L accC T)
  1110     then obtain n where
  1111       "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
  1112       by (rules elim!: wt_elim_cases)
  1113     then have "G\<turnstile>Norm s0 \<midarrow>Expr e\<midarrow>n\<rightarrow> s1"
  1114       by (rule evaln.Expr) 
  1115     then show ?case ..
  1116   next
  1117     case (Lab c l s0 s1 L accC T)
  1118     then obtain n where
  1119       "G\<turnstile>Norm s0 \<midarrow>c\<midarrow>n\<rightarrow> s1"
  1120       by (rules elim!: wt_elim_cases)
  1121     then have "G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<midarrow>n\<rightarrow> abupd (absorb l) s1"
  1122       by (rule evaln.Lab)
  1123     then show ?case ..
  1124   next
  1125     case (Comp c1 c2 s0 s1 s2 L accC T)
  1126     with wf obtain n1 n2 where
  1127       "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> s1"
  1128       "G\<turnstile>s1 \<midarrow>c2\<midarrow>n2\<rightarrow> s2"
  1129       by (blast elim!: wt_elim_cases dest: eval_type_sound)
  1130     then have "G\<turnstile>Norm s0 \<midarrow>c1;; c2\<midarrow>max n1 n2\<rightarrow> s2"
  1131       by (blast intro: evaln.Comp dest: evaln_max2 )
  1132     then show ?case ..
  1133   next
  1134     case (If b c1 c2 e s0 s1 s2 L accC T)
  1135     with wf obtain
  1136       "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean"
  1137       "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>(if the_Bool b then c1 else c2)\<Colon>\<surd>"
  1138       by (cases "the_Bool b") (auto elim!: wt_elim_cases)
  1139     with If wf obtain n1 n2 where
  1140       "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n1\<rightarrow> s1"
  1141       "G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<midarrow>n2\<rightarrow> s2"
  1142       by (blast dest: eval_type_sound)
  1143     then have "G\<turnstile>Norm s0 \<midarrow>If(e) c1 Else c2\<midarrow>max n1 n2\<rightarrow> s2"
  1144       by (blast intro: evaln.If dest: evaln_max2)
  1145     then show ?case ..
  1146   next
  1147     case (Loop b c e l s0 s1 s2 s3 L accC T)
  1148     have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1" .
  1149     have hyp_e: "PROP ?EqEval (Norm s0) s1 (In1l e) (In1 b)" .
  1150     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1151     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (l\<bullet> While(e) c)\<Colon>T" .
  1152     then obtain wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean" and
  1153                 wt_c: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c\<Colon>\<surd>"
  1154       by (rule wt_elim_cases) (blast)
  1155     from conf_s0 wt_e 
  1156     obtain n1 where
  1157       "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n1\<rightarrow> s1"
  1158       by (rules dest: hyp_e)
  1159     moreover
  1160     from eval_e wt_e conf_s0 wf
  1161     have conf_s1: "s1\<Colon>\<preceq>(G, L)"
  1162       by (rules dest: eval_type_sound)
  1163     obtain n2 where
  1164       "if normal s1 \<and> the_Bool b 
  1165              then (G\<turnstile>s1 \<midarrow>c\<midarrow>n2\<rightarrow> s2 \<and> 
  1166                    G\<turnstile>(abupd (absorb (Cont l)) s2)\<midarrow>l\<bullet> While(e) c\<midarrow>n2\<rightarrow> s3)
  1167 	     else s3 = s1"
  1168     proof (cases "normal s1 \<and> the_Bool b")
  1169       case True
  1170       from Loop True have hyp_c: "PROP ?EqEval s1 s2 (In1r c) \<diamondsuit>"
  1171 	by (auto)
  1172       from Loop True have hyp_w: "PROP ?EqEval (abupd (absorb (Cont l)) s2)
  1173                                         s3 (In1r (l\<bullet> While(e) c)) \<diamondsuit>"
  1174 	by (auto)
  1175       from Loop True have eval_c: "G\<turnstile>s1 \<midarrow>c\<rightarrow> s2"
  1176 	by simp
  1177       from conf_s1 wt_c
  1178       obtain m1 where 
  1179 	evaln_c: "G\<turnstile>s1 \<midarrow>c\<midarrow>m1\<rightarrow> s2"
  1180 	by (rules dest: hyp_c)
  1181       moreover
  1182       from eval_c conf_s1 wt_c wf
  1183       have "s2\<Colon>\<preceq>(G, L)"
  1184 	by (rules dest: eval_type_sound)
  1185       then
  1186       have "abupd (absorb (Cont l)) s2 \<Colon>\<preceq>(G, L)"
  1187 	by (cases s2) (auto intro: conforms_absorb)
  1188       from this and wt
  1189       obtain m2 where 
  1190 	"G\<turnstile>abupd (absorb (Cont l)) s2 \<midarrow>l\<bullet> While(e) c\<midarrow>m2\<rightarrow> s3"
  1191 	by (blast dest: hyp_w)
  1192       moreover note True and that
  1193       ultimately show ?thesis
  1194 	by simp (rules intro: evaln_nonstrict le_maxI1 le_maxI2)
  1195     next
  1196       case False
  1197       with Loop have "s3 = s1"
  1198 	by simp
  1199       with False that
  1200       show ?thesis
  1201 	by auto 
  1202     qed
  1203     ultimately
  1204     have "G\<turnstile>Norm s0 \<midarrow>l\<bullet> While(e) c\<midarrow>max n1 n2\<rightarrow> s3"
  1205       apply -
  1206       apply (rule evaln.Loop)
  1207       apply   (rules intro: evaln_nonstrict intro: le_maxI1)
  1208 
  1209       apply   (auto intro: evaln_nonstrict intro: le_maxI2)
  1210       done
  1211     then show ?case ..
  1212   next
  1213     case (Do j s L accC T)
  1214     have "G\<turnstile>Norm s \<midarrow>Do j\<midarrow>n\<rightarrow> (Some (Jump j), s)"
  1215       by (rule evaln.Do)
  1216     then show ?case ..
  1217   next
  1218     case (Throw a e s0 s1 L accC T)
  1219     then obtain n where
  1220       "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<midarrow>n\<rightarrow> s1"
  1221       by (rules elim!: wt_elim_cases)
  1222     then have "G\<turnstile>Norm s0 \<midarrow>Throw e\<midarrow>n\<rightarrow> abupd (throw a) s1"
  1223       by (rule evaln.Throw)
  1224     then show ?case ..
  1225   next 
  1226     case (Try catchC c1 c2 s0 s1 s2 s3 vn L accC T)
  1227     have  hyp_c1: "PROP ?EqEval (Norm s0) s1 (In1r c1) \<diamondsuit>" .
  1228     have eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1" .
  1229     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1230     have      wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>In1r (Try c1 Catch(catchC vn) c2)\<Colon>T" .
  1231     then obtain 
  1232       wt_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
  1233       wt_c2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<lparr>lcl := L(VName vn\<mapsto>Class catchC)\<rparr>\<turnstile>c2\<Colon>\<surd>"
  1234       by (rule wt_elim_cases) (auto)
  1235     from conf_s0 wt_c1
  1236     obtain n1 where
  1237       "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> s1"
  1238       by (blast dest: hyp_c1)
  1239     moreover 
  1240     have sxalloc: "G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2" .
  1241     moreover
  1242     from eval_c1 wt_c1 conf_s0 wf
  1243     have "s1\<Colon>\<preceq>(G, L)"
  1244       by (blast dest: eval_type_sound)
  1245     with sxalloc wf
  1246     have conf_s2: "s2\<Colon>\<preceq>(G, L)" 
  1247       by (auto dest: sxalloc_type_sound split: option.splits)
  1248     obtain n2 where
  1249       "if G,s2\<turnstile>catch catchC then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<midarrow>n2\<rightarrow> s3 else s3 = s2"
  1250     proof (cases "G,s2\<turnstile>catch catchC")
  1251       case True
  1252       note Catch = this
  1253       with Try have hyp_c2: "PROP ?EqEval (new_xcpt_var vn s2) s3 (In1r c2) \<diamondsuit>"
  1254 	by auto
  1255       show ?thesis
  1256       proof (cases "normal s1")
  1257 	case True
  1258 	with sxalloc wf 
  1259 	have eq_s2_s1: "s2=s1"
  1260 	  by (auto dest: sxalloc_type_sound split: option.splits)
  1261 	with True 
  1262 	have "\<not>  G,s2\<turnstile>catch catchC"
  1263 	  by (simp add: catch_def)
  1264 	with Catch show ?thesis 
  1265 	  by (contradiction)
  1266       next 
  1267 	case False
  1268 	with sxalloc wf
  1269 	obtain a 
  1270 	  where xcpt_s2: "abrupt s2 = Some (Xcpt (Loc a))"
  1271 	  by (auto dest!: sxalloc_type_sound split: option.splits)
  1272 	with Catch
  1273 	have "G\<turnstile>obj_ty (the (globs (store s2) (Heap a)))\<preceq>Class catchC"
  1274 	  by (cases s2) simp
  1275 	with xcpt_s2 conf_s2 wf 
  1276 	have "new_xcpt_var vn s2\<Colon>\<preceq>(G, L(VName vn\<mapsto>Class catchC))"
  1277 	  by (auto dest: Try_lemma)
  1278 	(* FIXME extract lemma for this conformance, also useful for
  1279                eval_type_sound and evaln_eval *)
  1280 	from this wt_c2
  1281 	obtain m where "G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<midarrow>m\<rightarrow> s3"
  1282 	  by (auto dest: hyp_c2)
  1283 	with True that
  1284 	show ?thesis
  1285 	  by simp
  1286       qed
  1287     next
  1288       case False
  1289       with Try
  1290       have "s3=s2"
  1291 	by simp
  1292       with False and that
  1293       show ?thesis
  1294 	by simp
  1295     qed
  1296     ultimately
  1297     have "G\<turnstile>Norm s0 \<midarrow>Try c1 Catch(catchC vn) c2\<midarrow>max n1 n2\<rightarrow> s3"
  1298       by (auto intro!: evaln.Try le_maxI1 le_maxI2)
  1299     then show ?case ..
  1300   next
  1301     case (Fin c1 c2 s0 s1 s2 s3 x1 L accC T)
  1302     have s3: "s3 = (if \<exists>err. x1 = Some (Error err) 
  1303                        then (x1, s1)
  1304                        else abupd (abrupt_if (x1 \<noteq> None) x1) s2)" .
  1305     from Fin wf obtain n1 n2 where 
  1306       "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> (x1, s1)"
  1307       "G\<turnstile>Norm s1 \<midarrow>c2\<midarrow>n2\<rightarrow> s2" and
  1308       error_free_s1: "error_free (x1,s1)"
  1309       by (blast elim!: wt_elim_cases 
  1310 	         dest: eval_type_sound intro: conforms_NormI)
  1311     then have 
  1312      "G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<midarrow>max n1 n2\<rightarrow> abupd (abrupt_if (x1 \<noteq> None) x1) s2"
  1313       by (blast intro: evaln.Fin dest: evaln_max2)
  1314     with error_free_s1 s3
  1315     show "\<exists>n. G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<midarrow>n\<rightarrow> s3"
  1316       by (auto simp add: error_free_def)
  1317   next
  1318     case (Init C c s0 s1 s2 s3 L accC T)
  1319     have     cls: "the (class G C) = c" .
  1320     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1321     have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (Init C)\<Colon>T" .
  1322     with cls
  1323     have cls_C: "class G C = Some c"
  1324       by - (erule wt_elim_cases,auto)
  1325     obtain n where
  1326       "if inited C (globs s0) then s3 = Norm s0
  1327        else (G\<turnstile>Norm (init_class_obj G C s0)
  1328 	      \<midarrow>(if C = Object then Skip else Init (super c))\<midarrow>n\<rightarrow> s1 \<and>
  1329 	           G\<turnstile>set_lvars empty s1 \<midarrow>init c\<midarrow>n\<rightarrow> s2 \<and> 
  1330                    s3 = restore_lvars s1 s2)"
  1331     proof (cases "inited C (globs s0)")
  1332       case True
  1333       with Init have "s3 = Norm s0"
  1334 	by simp
  1335       with True that show ?thesis 
  1336 	by simp
  1337     next
  1338       case False
  1339       with Init
  1340       obtain 
  1341 	hyp_init_super: 
  1342         "PROP ?EqEval (Norm ((init_class_obj G C) s0)) s1
  1343 	               (In1r (if C = Object then Skip else Init (super c))) \<diamondsuit>"
  1344 	and 
  1345         hyp_init_c:
  1346 	   "PROP ?EqEval ((set_lvars empty) s1) s2 (In1r (init c)) \<diamondsuit>" and
  1347 	s3: "s3 = (set_lvars (locals (store s1))) s2" and
  1348 	eval_init_super: 
  1349 	"G\<turnstile>Norm ((init_class_obj G C) s0) 
  1350            \<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1"
  1351 	by (simp only: if_False)
  1352       from conf_s0 wf cls_C False
  1353       have conf_s0': "(Norm ((init_class_obj G C) s0))\<Colon>\<preceq>(G, L)"
  1354 	by (auto dest: conforms_init_class_obj)
  1355       moreover
  1356       from wf cls_C 
  1357       have wt_init_super:
  1358            "\<lparr>prg = G, cls = accC, lcl = L\<rparr>
  1359                   \<turnstile>(if C = Object then Skip else Init (super c))\<Colon>\<surd>"
  1360 	by (cases "C=Object")
  1361            (auto dest: wf_prog_cdecl wf_cdecl_supD is_acc_classD)
  1362       ultimately
  1363       obtain m1 where  
  1364 	   "G\<turnstile>Norm ((init_class_obj G C) s0) 
  1365             \<midarrow>(if C = Object then Skip else Init (super c))\<midarrow>m1\<rightarrow> s1"
  1366 	by (rules dest: hyp_init_super)
  1367       moreover
  1368       from eval_init_super conf_s0' wt_init_super wf
  1369       have "s1\<Colon>\<preceq>(G, L)"
  1370 	by (rules dest: eval_type_sound)
  1371       then
  1372       have "(set_lvars empty) s1\<Colon>\<preceq>(G, empty)"
  1373 	by (cases s1) (auto dest: conforms_set_locals )
  1374       with wf cls_C 
  1375       obtain m2 where
  1376 	"G\<turnstile>(set_lvars empty) s1 \<midarrow>init c\<midarrow>m2\<rightarrow> s2"
  1377 	by (blast dest!: hyp_init_c 
  1378                    dest: wf_prog_cdecl intro!: wf_cdecl_wt_init)
  1379       moreover note s3 and False and that
  1380       ultimately show ?thesis
  1381 	by simp (rules intro: evaln_nonstrict le_maxI1 le_maxI2)
  1382     qed
  1383     from cls this have "G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s3"
  1384       by (rule evaln.Init)
  1385     then show ?case ..
  1386   next
  1387     case (NewC C a s0 s1 s2 L accC T)
  1388     with wf obtain n where 
  1389      "G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s1"
  1390       by (blast elim!: wt_elim_cases dest: is_acc_classD)
  1391     with NewC 
  1392     have "G\<turnstile>Norm s0 \<midarrow>NewC C-\<succ>Addr a\<midarrow>n\<rightarrow> s2"
  1393       by (rules intro: evaln.NewC)
  1394     then show ?case ..
  1395   next
  1396     case (NewA T a e i s0 s1 s2 s3 L accC Ta)
  1397     hence "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>init_comp_ty T\<Colon>\<surd>" 
  1398       by (auto elim!: wt_elim_cases 
  1399               intro!: wt_init_comp_ty dest: is_acc_typeD)
  1400     with NewA wf obtain n1 n2 where 
  1401       "G\<turnstile>Norm s0 \<midarrow>init_comp_ty T\<midarrow>n1\<rightarrow> s1"
  1402       "G\<turnstile>s1 \<midarrow>e-\<succ>i\<midarrow>n2\<rightarrow> s2"      
  1403       by (blast elim!: wt_elim_cases dest: eval_type_sound)
  1404     moreover
  1405     have "G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3" .
  1406     ultimately
  1407     have "G\<turnstile>Norm s0 \<midarrow>New T[e]-\<succ>Addr a\<midarrow>max n1 n2\<rightarrow> s3"
  1408       by (blast intro: evaln.NewA dest: evaln_max2)
  1409     then show ?case ..
  1410   next
  1411     case (Cast castT e s0 s1 s2 v L accC T)
  1412     with wf obtain n where
  1413       "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
  1414       by (rules elim!: wt_elim_cases)
  1415     moreover 
  1416     have "s2 = abupd (raise_if (\<not> G,snd s1\<turnstile>v fits castT) ClassCast) s1" .
  1417     ultimately
  1418     have "G\<turnstile>Norm s0 \<midarrow>Cast castT e-\<succ>v\<midarrow>n\<rightarrow> s2"
  1419       by (rule evaln.Cast)
  1420     then show ?case ..
  1421   next
  1422     case (Inst T b e s0 s1 v L accC T')
  1423     with wf obtain n where
  1424       "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
  1425       by (rules elim!: wt_elim_cases)
  1426     moreover 
  1427     have "b = (v \<noteq> Null \<and> G,snd s1\<turnstile>v fits RefT T)" .
  1428     ultimately
  1429     have "G\<turnstile>Norm s0 \<midarrow>e InstOf T-\<succ>Bool b\<midarrow>n\<rightarrow> s1"
  1430       by (rule evaln.Inst)
  1431     then show ?case ..
  1432   next
  1433     case (Lit s v L accC T)
  1434     have "G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<midarrow>n\<rightarrow> Norm s"
  1435       by (rule evaln.Lit)
  1436     then show ?case ..
  1437   next
  1438     case (UnOp e s0 s1 unop v L accC T)
  1439     with wf obtain n where
  1440       "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
  1441       by (rules elim!: wt_elim_cases)
  1442     hence "G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>eval_unop unop v\<midarrow>n\<rightarrow> s1"
  1443       by (rule evaln.UnOp)
  1444     then show ?case ..
  1445   next
  1446     case (BinOp binop e1 e2 s0 s1 s2 v1 v2 L accC T)
  1447     with wf obtain n1 n2 where 
  1448       "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<midarrow>n1\<rightarrow> s1"
  1449       "G\<turnstile>s1 \<midarrow>e2-\<succ>v2\<midarrow>n2\<rightarrow> s2"    
  1450       by (blast elim!: wt_elim_cases dest: eval_type_sound)
  1451     hence "G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<midarrow>max n1 n2
  1452            \<rightarrow> s2"
  1453       by (blast intro!: evaln.BinOp dest: evaln_max2)
  1454     then show ?case ..
  1455   next
  1456     case (Super s L accC T)
  1457     have "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<midarrow>n\<rightarrow> Norm s"
  1458       by (rule evaln.Super)
  1459     then show ?case ..
  1460   next
  1461     case (Acc f s0 s1 v va L accC T)
  1462     with wf obtain n where
  1463       "G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v, f)\<midarrow>n\<rightarrow> s1"
  1464       by (rules elim!: wt_elim_cases)
  1465     then
  1466     have "G\<turnstile>Norm s0 \<midarrow>Acc va-\<succ>v\<midarrow>n\<rightarrow> s1"
  1467       by (rule evaln.Acc)
  1468     then show ?case ..
  1469   next
  1470     case (Ass e f s0 s1 s2 v var w L accC T)
  1471     with wf obtain n1 n2 where 
  1472       "G\<turnstile>Norm s0 \<midarrow>var=\<succ>(w, f)\<midarrow>n1\<rightarrow> s1"
  1473       "G\<turnstile>s1 \<midarrow>e-\<succ>v\<midarrow>n2\<rightarrow> s2"      
  1474       by (blast elim!: wt_elim_cases dest: eval_type_sound)
  1475     then
  1476     have "G\<turnstile>Norm s0 \<midarrow>var:=e-\<succ>v\<midarrow>max n1 n2\<rightarrow> assign f v s2"
  1477       by (blast intro: evaln.Ass dest: evaln_max2)
  1478     then show ?case ..
  1479   next
  1480     case (Cond b e0 e1 e2 s0 s1 s2 v L accC T)
  1481     have hyp_e0: "PROP ?EqEval (Norm s0) s1 (In1l e0) (In1 b)" .
  1482     have hyp_if: "PROP ?EqEval s1 s2 
  1483                               (In1l (if the_Bool b then e1 else e2)) (In1 v)" .
  1484     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1485     have wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (e0 ? e1 : e2)\<Colon>T" .
  1486     then obtain T1 T2 statT where
  1487        wt_e0: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e0\<Colon>-PrimT Boolean" and
  1488        wt_e1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e1\<Colon>-T1" and
  1489        wt_e2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e2\<Colon>-T2" and 
  1490        statT: "G\<turnstile>T1\<preceq>T2 \<and> statT = T2  \<or>  G\<turnstile>T2\<preceq>T1 \<and> statT =  T1" and
  1491        T    : "T=Inl statT"
  1492       by (rule wt_elim_cases) auto
  1493     have eval_e0: "G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1" .
  1494     from conf_s0 wt_e0
  1495     obtain n1 where 
  1496       "G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<midarrow>n1\<rightarrow> s1"
  1497       by (rules dest: hyp_e0)
  1498     moreover
  1499     from eval_e0 conf_s0 wf wt_e0
  1500     have "s1\<Colon>\<preceq>(G, L)"
  1501       by (blast dest: eval_type_sound)
  1502     with wt_e1 wt_e2 statT hyp_if obtain n2 where
  1503       "G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<midarrow>n2\<rightarrow> s2"
  1504       by  (cases "the_Bool b") force+
  1505     ultimately
  1506     have "G\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<midarrow>max n1 n2\<rightarrow> s2"
  1507       by (blast intro: evaln.Cond dest: evaln_max2)
  1508     then show ?case ..
  1509   next
  1510     case (Call invDeclC a' accC' args e mn mode pTs' s0 s1 s2 s3 s3' s4 statT 
  1511       v vs L accC T)
  1512     (* Repeats large parts of the type soundness proof. One should factor
  1513        out some lemmata about the relations and conformance of s2, s3 and s3'*)
  1514     have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1" .
  1515     have eval_args: "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<rightarrow> s2" .
  1516     have invDeclC: "invDeclC 
  1517                       = invocation_declclass G mode (store s2) a' statT 
  1518                            \<lparr>name = mn, parTs = pTs'\<rparr>" .
  1519     have
  1520       init_lvars: "s3 = 
  1521              init_lvars G invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> mode a' vs s2" .
  1522     have
  1523       check: "s3' =
  1524        check_method_access G accC' statT mode \<lparr>name = mn, parTs = pTs'\<rparr> a' s3" .
  1525     have eval_methd: 
  1526            "G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>-\<succ>v\<rightarrow> s4" .
  1527     have     hyp_e: "PROP ?EqEval (Norm s0) s1 (In1l e) (In1 a')" .
  1528     have  hyp_args: "PROP ?EqEval s1 s2 (In3 args) (In3 vs)" .
  1529     have hyp_methd: "PROP ?EqEval s3' s4 
  1530              (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)) (In1 v)".
  1531     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1532     have      wt: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>
  1533                     \<turnstile>In1l ({accC',statT,mode}e\<cdot>mn( {pTs'}args))\<Colon>T" .
  1534     from wt obtain pTs statDeclT statM where
  1535                  wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT" and
  1536               wt_args: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>args\<Colon>\<doteq>pTs" and
  1537                 statM: "max_spec G accC statT \<lparr>name=mn,parTs=pTs\<rparr> 
  1538                          = {((statDeclT,statM),pTs')}" and
  1539                  mode: "mode = invmode statM e" and
  1540                     T: "T =Inl (resTy statM)" and
  1541         eq_accC_accC': "accC=accC'"
  1542       by (rule wt_elim_cases) auto
  1543     from conf_s0 wt_e
  1544     obtain n1 where
  1545       evaln_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n1\<rightarrow> s1"
  1546       by (rules dest: hyp_e)
  1547     from wf eval_e conf_s0 wt_e
  1548     obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and
  1549            conf_a': "normal s1 \<Longrightarrow> G, store s1\<turnstile>a'\<Colon>\<preceq>RefT statT"  
  1550       by (auto dest!: eval_type_sound)
  1551     from conf_s1 wt_args
  1552     obtain n2 where
  1553       evaln_args: "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<midarrow>n2\<rightarrow> s2"
  1554       by (blast dest: hyp_args)
  1555     from wt_args conf_s1 eval_args wf 
  1556     obtain    conf_s2: "s2\<Colon>\<preceq>(G, L)" and
  1557             conf_args: "normal s2 
  1558                          \<Longrightarrow>  list_all2 (conf G (store s2)) vs pTs"  
  1559       by (auto dest!: eval_type_sound)
  1560     from statM 
  1561     obtain
  1562        statM': "(statDeclT,statM)\<in>mheads G accC statT \<lparr>name=mn,parTs=pTs'\<rparr>" and
  1563        pTs_widen: "G\<turnstile>pTs[\<preceq>]pTs'"
  1564       by (blast dest: max_spec2mheads)
  1565     from check
  1566     have eq_store_s3'_s3: "store s3'=store s3"
  1567       by (cases s3) (simp add: check_method_access_def Let_def)
  1568     obtain invC
  1569       where invC: "invC = invocation_class mode (store s2) a' statT"
  1570       by simp
  1571     with init_lvars
  1572     have invC': "invC = (invocation_class mode (store s3) a' statT)"
  1573       by (cases s2,cases mode) (auto simp add: init_lvars_def2 )
  1574     obtain n3 where
  1575      "G\<turnstile>Norm s0 \<midarrow>{accC',statT,mode}e\<cdot>mn( {pTs'}args)-\<succ>v\<midarrow>n3\<rightarrow> 
  1576           (set_lvars (locals (store s2))) s4"
  1577     proof (cases "normal s2")
  1578       case False
  1579       with init_lvars 
  1580       obtain keep_abrupt: "abrupt s3 = abrupt s2" and
  1581              "store s3 = store (init_lvars G invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> 
  1582                                             mode a' vs s2)" 
  1583 	by (auto simp add: init_lvars_def2)
  1584       moreover
  1585       from keep_abrupt False check
  1586       have eq_s3'_s3: "s3'=s3" 
  1587 	by (auto simp add: check_method_access_def Let_def)
  1588       moreover
  1589       from eq_s3'_s3 False keep_abrupt eval_methd init_lvars
  1590       obtain "s4=s3'"
  1591       "In1 v=arbitrary3 (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>))"
  1592 	by auto
  1593       moreover note False evaln.Abrupt
  1594       ultimately obtain m where 
  1595 	"G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>-\<succ>v\<midarrow>m\<rightarrow> s4"
  1596 	by force
  1597       from evaln_e evaln_args invDeclC init_lvars eq_s3'_s3 this
  1598       have 
  1599        "G\<turnstile>Norm s0 \<midarrow>{accC',statT,mode}e\<cdot>mn( {pTs'}args)-\<succ>v\<midarrow>max n1 (max n2 m)\<rightarrow> 
  1600             (set_lvars (locals (store s2))) s4"
  1601 	by (auto intro!: evaln.Call le_maxI1 le_max3I1 le_max3I2)
  1602       with that show ?thesis 
  1603 	by rules
  1604     next
  1605       case True
  1606       note normal_s2 = True
  1607       with eval_args
  1608       have normal_s1: "normal s1"
  1609 	by (cases "normal s1") auto
  1610       with conf_a' eval_args 
  1611       have conf_a'_s2: "G, store s2\<turnstile>a'\<Colon>\<preceq>RefT statT"
  1612 	by (auto dest: eval_gext intro: conf_gext)
  1613       show ?thesis
  1614       proof (cases "a'=Null \<longrightarrow> is_static statM")
  1615 	case False
  1616 	then obtain not_static: "\<not> is_static statM" and Null: "a'=Null" 
  1617 	  by blast
  1618 	with normal_s2 init_lvars mode
  1619 	obtain np: "abrupt s3 = Some (Xcpt (Std NullPointer))" and
  1620                    "store s3 = store (init_lvars G invDeclC 
  1621                                        \<lparr>name = mn, parTs = pTs'\<rparr> mode a' vs s2)"
  1622 	  by (auto simp add: init_lvars_def2)
  1623 	moreover
  1624 	from np check
  1625 	have eq_s3'_s3: "s3'=s3" 
  1626 	  by (auto simp add: check_method_access_def Let_def)
  1627 	moreover
  1628 	from eq_s3'_s3 np eval_methd init_lvars
  1629 	obtain "s4=s3'"
  1630       "In1 v=arbitrary3 (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>))"
  1631 	  by auto
  1632 	moreover note np
  1633 	ultimately obtain m where 
  1634 	  "G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>-\<succ>v\<midarrow>m\<rightarrow> s4"
  1635 	  by force
  1636 	from evaln_e evaln_args invDeclC init_lvars eq_s3'_s3 this
  1637 	have 
  1638         "G\<turnstile>Norm s0 \<midarrow>{accC',statT,mode}e\<cdot>mn( {pTs'}args)-\<succ>v\<midarrow>max n1 (max n2 m)\<rightarrow> 
  1639             (set_lvars (locals (store s2))) s4"
  1640 	  by (auto intro!: evaln.Call le_maxI1 le_max3I1 le_max3I2)
  1641 	with that show ?thesis 
  1642 	  by rules
  1643       next
  1644 	case True
  1645 	with mode have notNull: "mode = IntVir \<longrightarrow> a' \<noteq> Null"
  1646 	  by (auto dest!: Null_staticD)
  1647 	with conf_s2 conf_a'_s2 wf invC 
  1648 	have dynT_prop: "G\<turnstile>mode\<rightarrow>invC\<preceq>statT"
  1649 	  by (cases s2) (auto intro: DynT_propI)
  1650 	with wt_e statM' invC mode wf 
  1651 	obtain dynM where 
  1652            dynM: "dynlookup G statT invC  \<lparr>name=mn,parTs=pTs'\<rparr> = Some dynM" and
  1653            acc_dynM: "G \<turnstile>Methd  \<lparr>name=mn,parTs=pTs'\<rparr> dynM 
  1654                           in invC dyn_accessible_from accC"
  1655 	  by (force dest!: call_access_ok)
  1656 	with invC' check eq_accC_accC'
  1657 	have eq_s3'_s3: "s3'=s3"
  1658 	  by (auto simp add: check_method_access_def Let_def)
  1659 	from dynT_prop wf wt_e statM' mode invC invDeclC dynM 
  1660 	obtain 
  1661 	   wf_dynM: "wf_mdecl G invDeclC (\<lparr>name=mn,parTs=pTs'\<rparr>,mthd dynM)" and
  1662 	     dynM': "methd G invDeclC \<lparr>name=mn,parTs=pTs'\<rparr> = Some dynM" and
  1663            iscls_invDeclC: "is_class G invDeclC" and
  1664 	        invDeclC': "invDeclC = declclass dynM" and
  1665 	     invC_widen: "G\<turnstile>invC\<preceq>\<^sub>C invDeclC" and
  1666 	   is_static_eq: "is_static dynM = is_static statM" and
  1667 	   involved_classes_prop:
  1668              "(if invmode statM e = IntVir
  1669                then \<forall>statC. statT = ClassT statC \<longrightarrow> G\<turnstile>invC\<preceq>\<^sub>C statC
  1670                else ((\<exists>statC. statT = ClassT statC \<and> G\<turnstile>statC\<preceq>\<^sub>C invDeclC) \<or>
  1671                      (\<forall>statC. statT \<noteq> ClassT statC \<and> invDeclC = Object)) \<and>
  1672                       statDeclT = ClassT invDeclC)"
  1673 	  by (auto dest: DynT_mheadsD)
  1674 	obtain L' where 
  1675 	   L':"L'=(\<lambda> k. 
  1676                  (case k of
  1677                     EName e
  1678                     \<Rightarrow> (case e of 
  1679                           VNam v 
  1680                           \<Rightarrow>(table_of (lcls (mbody (mthd dynM)))
  1681                              (pars (mthd dynM)[\<mapsto>]pTs')) v
  1682                         | Res \<Rightarrow> Some (resTy dynM))
  1683                   | This \<Rightarrow> if is_static statM 
  1684                             then None else Some (Class invDeclC)))"
  1685 	  by simp
  1686 	from wf_dynM [THEN wf_mdeclD1, THEN conjunct1] normal_s2 conf_s2 wt_e
  1687               wf eval_args conf_a' mode notNull wf_dynM involved_classes_prop
  1688 	have conf_s3: "s3\<Colon>\<preceq>(G,L')"
  1689 	   apply - 
  1690           (*FIXME confomrs_init_lvars should be 
  1691                 adjusted to be more directy applicable *)
  1692 	   apply (drule conforms_init_lvars [of G invDeclC 
  1693                   "\<lparr>name=mn,parTs=pTs'\<rparr>" dynM "store s2" vs pTs "abrupt s2" 
  1694                   L statT invC a' "(statDeclT,statM)" e])
  1695 	     apply (rule wf)
  1696 	     apply (rule conf_args,assumption)
  1697 	     apply (simp add: pTs_widen)
  1698 	     apply (cases s2,simp)
  1699 	     apply (rule dynM')
  1700 	     apply (force dest: ty_expr_is_type)
  1701 	     apply (rule invC_widen)
  1702 	     apply (force intro: conf_gext dest: eval_gext)
  1703 	     apply simp
  1704 	     apply simp
  1705 	     apply (simp add: invC)
  1706 	     apply (simp add: invDeclC)
  1707 	     apply (force dest: wf_mdeclD1 is_acc_typeD)
  1708 	     apply (cases s2, simp add: L' init_lvars
  1709 	                      cong add: lname.case_cong ename.case_cong)
  1710 	   done
  1711 	with is_static_eq wf_dynM L'
  1712 	obtain mthdT where
  1713 	   "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>
  1714             \<turnstile>Body invDeclC (stmt (mbody (mthd dynM)))\<Colon>-mthdT" 
  1715 	  by - (drule wf_mdecl_bodyD,
  1716                 auto simp: cong add: lname.case_cong ename.case_cong)
  1717 	with dynM' iscls_invDeclC invDeclC'
  1718 	have
  1719 	   "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>
  1720             \<turnstile>(Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)\<Colon>-mthdT"
  1721 	  by (auto intro: wt.Methd)
  1722 	with conf_s3 eq_s3'_s3 hyp_methd
  1723 	obtain m where
  1724 	   "G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>-\<succ>v\<midarrow>m\<rightarrow> s4"
  1725 	  by (blast)
  1726 	from evaln_e evaln_args invDeclC init_lvars  eq_s3'_s3 this
  1727 	have 
  1728         "G\<turnstile>Norm s0 \<midarrow>{accC',statT,mode}e\<cdot>mn( {pTs'}args)-\<succ>v\<midarrow>max n1 (max n2 m)\<rightarrow> 
  1729             (set_lvars (locals (store s2))) s4"
  1730 	  by (auto intro!: evaln.Call le_maxI1 le_max3I1 le_max3I2)
  1731 	with that show ?thesis 
  1732 	  by rules
  1733       qed
  1734     qed
  1735     then show ?case ..
  1736   next
  1737     case (Methd D s0 s1 sig v L accC T)
  1738     then obtain n where
  1739       "G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<midarrow>n\<rightarrow> s1"
  1740       by - (erule wt_elim_cases, force simp add: body_def2)
  1741     then have "G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<midarrow>Suc n\<rightarrow> s1"
  1742       by (rule evaln.Methd)
  1743     then show ?case ..
  1744   next
  1745     case (Body D c s0 s1 s2 L accC T)
  1746     with wf obtain n1 n2 where 
  1747       "G\<turnstile>Norm s0 \<midarrow>Init D\<midarrow>n1\<rightarrow> s1"
  1748       "G\<turnstile>s1 \<midarrow>c\<midarrow>n2\<rightarrow> s2"
  1749       by (blast elim!: wt_elim_cases dest: eval_type_sound)
  1750     then have 
  1751      "G\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>the (locals (store s2) Result)\<midarrow>max n1 n2
  1752        \<rightarrow> abupd (absorb Ret) s2"
  1753       by (blast intro: evaln.Body dest: evaln_max2)
  1754     then show ?case ..
  1755   next
  1756     case (LVar s vn L accC T)
  1757     obtain n where
  1758       "G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<midarrow>n\<rightarrow> Norm s"
  1759       by (rules intro: evaln.LVar)
  1760     then show ?case ..
  1761   next
  1762     case (FVar a accC e fn s0 s1 s2 s2' s3 stat statDeclC v L accC' T)
  1763     have eval_init: "G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<rightarrow> s1" .
  1764     have eval_e: "G\<turnstile>s1 \<midarrow>e-\<succ>a\<rightarrow> s2" .
  1765     have check: "s3 = check_field_access G accC statDeclC fn stat a s2'" .
  1766     have hyp_init: "PROP ?EqEval (Norm s0) s1 (In1r (Init statDeclC)) \<diamondsuit>" .
  1767     have hyp_e: "PROP ?EqEval s1 s2 (In1l e) (In1 a)" .
  1768     have fvar: "(v, s2') = fvar statDeclC stat fn a s2" .
  1769     have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1770     have wt: "\<lparr>prg=G, cls=accC', lcl=L\<rparr>\<turnstile>In2 ({accC,statDeclC,stat}e..fn)\<Colon>T" .
  1771     then obtain statC f where
  1772                 wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-Class statC" and
  1773             accfield: "accfield G accC statC fn = Some (statDeclC,f)" and
  1774                 stat: "stat=is_static f" and
  1775                accC': "accC'=accC" and
  1776 	           T: "T=(Inl (type f))"
  1777        by (rule wt_elim_cases) (auto simp add: member_is_static_simp)
  1778     from wf wt_e 
  1779     have iscls_statC: "is_class G statC"
  1780       by (auto dest: ty_expr_is_type type_is_class)
  1781     with wf accfield 
  1782     have iscls_statDeclC: "is_class G statDeclC"
  1783       by (auto dest!: accfield_fields dest: fields_declC)
  1784     then 
  1785     have wt_init: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>(Init statDeclC)\<Colon>\<surd>"
  1786       by simp
  1787     from conf_s0 wt_init
  1788     obtain n1 where
  1789       evaln_init: "G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<midarrow>n1\<rightarrow> s1"
  1790       by (rules dest: hyp_init)
  1791     from eval_init wt_init conf_s0 wf 
  1792     have conf_s1: "s1\<Colon>\<preceq>(G, L)"
  1793       by (blast dest: eval_type_sound)
  1794     with wt_e
  1795     obtain n2 where
  1796       evaln_e: "G\<turnstile>s1 \<midarrow>e-\<succ>a\<midarrow>n2\<rightarrow> s2"
  1797       by (blast dest: hyp_e)
  1798     from eval_e wf conf_s1 wt_e
  1799     obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and
  1800             conf_a: "normal s2 \<longrightarrow> G,store s2\<turnstile>a\<Colon>\<preceq>Class statC"
  1801       by (auto dest!: eval_type_sound)
  1802     from accfield wt_e eval_init eval_e conf_s2 conf_a fvar stat check  wf
  1803     have eq_s3_s2': "s3=s2'"  
  1804       by (auto dest!: error_free_field_access)
  1805     with evaln_init evaln_e fvar accC'
  1806     have "G\<turnstile>Norm s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>v\<midarrow>max n1 n2\<rightarrow> s3"
  1807       by (auto intro: evaln.FVar dest: evaln_max2)
  1808     then show ?case ..
  1809   next
  1810     case (AVar a e1 e2 i s0 s1 s2 s2' v L accC T)
  1811     with wf obtain n1 n2 where 
  1812       "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>a\<midarrow>n1\<rightarrow> s1"
  1813       "G\<turnstile>s1 \<midarrow>e2-\<succ>i\<midarrow>n2\<rightarrow> s2"      
  1814       by (blast elim!: wt_elim_cases dest: eval_type_sound)
  1815     moreover 
  1816     have "(v, s2') = avar G i a s2" .
  1817     ultimately 
  1818     have "G\<turnstile>Norm s0 \<midarrow>e1.[e2]=\<succ>v\<midarrow>max n1 n2\<rightarrow> s2'"
  1819       by (blast intro!: evaln.AVar dest: evaln_max2)
  1820     then show ?case ..
  1821   next
  1822     case (Nil s0 L accC T)
  1823     show ?case by (rules intro: evaln.Nil)
  1824   next
  1825     case (Cons e es s0 s1 s2 v vs L accC T)
  1826     with wf obtain n1 n2 where 
  1827       "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n1\<rightarrow> s1"
  1828       "G\<turnstile>s1 \<midarrow>es\<doteq>\<succ>vs\<midarrow>n2\<rightarrow> s2"      
  1829       by (blast elim!: wt_elim_cases dest: eval_type_sound)
  1830     then
  1831     have "G\<turnstile>Norm s0 \<midarrow>e # es\<doteq>\<succ>v # vs\<midarrow>max n1 n2\<rightarrow> s2"
  1832       by (blast intro!: evaln.Cons dest: evaln_max2)
  1833     then show ?case ..
  1834   qed
  1835 qed
  1836 
  1837 end