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