src/HOL/Bali/Evaln.thy
author haftmann
Tue Oct 07 16:07:50 2008 +0200 (2008-10-07)
changeset 28524 644b62cf678f
parent 27226 5a3e5e46d977
child 32960 69916a850301
permissions -rw-r--r--
arbitrary is undefined
     1 (*  Title:      HOL/Bali/Evaln.thy
     2     ID:         $Id$
     3     Author:     David von Oheimb and Norbert Schirmer
     4 *)
     5 header {* Operational evaluation (big-step) semantics of Java expressions and 
     6           statements
     7 *}
     8 
     9 theory Evaln imports TypeSafe begin
    10 
    11 
    12 text {*
    13 Variant of @{term eval} relation with counter for bounded recursive depth. 
    14 In principal @{term evaln} could replace @{term eval}.
    15 
    16 Validity of the axiomatic semantics builds on @{term evaln}. 
    17 For recursive method calls the axiomatic semantics rule assumes the method ok 
    18 to derive a proof for the body. To prove the method rule sound we need to 
    19 perform induction on the recursion depth. 
    20 For the completeness proof of the axiomatic semantics the notion of the most
    21 general formula is used. The most general formula right now builds on the 
    22 ordinary evaluation relation @{term eval}. 
    23 So sometimes we have to switch between @{term evaln} and @{term eval} and vice 
    24 versa. To make
    25 this switch easy @{term evaln} also does all the technical accessibility tests 
    26 @{term check_field_access} and @{term check_method_access} like @{term eval}. 
    27 If it would omit them @{term evaln} and @{term eval} would only be equivalent 
    28 for welltyped, and definitely assigned terms.
    29 *}
    30 
    31 inductive
    32   evaln	:: "[prog, state, term, nat, vals, state] \<Rightarrow> bool"
    33     ("_\<turnstile>_ \<midarrow>_\<succ>\<midarrow>_\<rightarrow> '(_, _')" [61,61,80,61,0,0] 60)
    34   and evarn :: "[prog, state, var, vvar, nat, state] \<Rightarrow> bool"
    35     ("_\<turnstile>_ \<midarrow>_=\<succ>_\<midarrow>_\<rightarrow> _" [61,61,90,61,61,61] 60)
    36   and eval_n:: "[prog, state, expr, val, nat, state] \<Rightarrow> bool"
    37     ("_\<turnstile>_ \<midarrow>_-\<succ>_\<midarrow>_\<rightarrow> _" [61,61,80,61,61,61] 60)
    38   and evalsn :: "[prog, state, expr list, val  list, nat, state] \<Rightarrow> bool"
    39     ("_\<turnstile>_ \<midarrow>_\<doteq>\<succ>_\<midarrow>_\<rightarrow> _" [61,61,61,61,61,61] 60)
    40   and execn	:: "[prog, state, stmt, nat, state] \<Rightarrow> bool"
    41     ("_\<turnstile>_ \<midarrow>_\<midarrow>_\<rightarrow> _"     [61,61,65,   61,61] 60)
    42   for G :: prog
    43 where
    44 
    45   "G\<turnstile>s \<midarrow>c     \<midarrow>n\<rightarrow>    s' \<equiv> G\<turnstile>s \<midarrow>In1r  c\<succ>\<midarrow>n\<rightarrow> (\<diamondsuit>    ,  s')"
    46 | "G\<turnstile>s \<midarrow>e-\<succ>v  \<midarrow>n\<rightarrow>    s' \<equiv> G\<turnstile>s \<midarrow>In1l e\<succ>\<midarrow>n\<rightarrow> (In1 v ,  s')"
    47 | "G\<turnstile>s \<midarrow>e=\<succ>vf \<midarrow>n\<rightarrow>    s' \<equiv> G\<turnstile>s \<midarrow>In2  e\<succ>\<midarrow>n\<rightarrow> (In2 vf,  s')"
    48 | "G\<turnstile>s \<midarrow>e\<doteq>\<succ>v  \<midarrow>n\<rightarrow>    s' \<equiv> G\<turnstile>s \<midarrow>In3  e\<succ>\<midarrow>n\<rightarrow> (In3 v ,  s')"
    49 
    50 --{* propagation of abrupt completion *}
    51 
    52 | Abrupt:   "G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (undefined3 t,(Some xc,s))"
    53 
    54 
    55 --{* evaluation of variables *}
    56 
    57 | LVar:	"G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<midarrow>n\<rightarrow> Norm s"
    58 
    59 | FVar:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e-\<succ>a\<midarrow>n\<rightarrow> s2;
    60 	  (v,s2') = fvar statDeclC stat fn a s2;
    61           s3 = check_field_access G accC statDeclC fn stat a s2'\<rbrakk> \<Longrightarrow>
    62 	  G\<turnstile>Norm s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>v\<midarrow>n\<rightarrow> s3"
    63 
    64 | 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; 
    65 	  (v,s2') = avar G i a s2\<rbrakk> \<Longrightarrow>
    66 	              G\<turnstile>Norm s0 \<midarrow>e1.[e2]=\<succ>v\<midarrow>n\<rightarrow> s2'"
    67 
    68 
    69 
    70 
    71 --{* evaluation of expressions *}
    72 
    73 | NewC:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s1;
    74 	  G\<turnstile>     s1 \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s2\<rbrakk> \<Longrightarrow>
    75 	                          G\<turnstile>Norm s0 \<midarrow>NewC C-\<succ>Addr a\<midarrow>n\<rightarrow> s2"
    76 
    77 | 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; 
    78 	  G\<turnstile>abupd (check_neg i') s2 \<midarrow>halloc (Arr T (the_Intg i'))\<succ>a\<rightarrow> s3\<rbrakk> \<Longrightarrow>
    79 	                        G\<turnstile>Norm s0 \<midarrow>New T[e]-\<succ>Addr a\<midarrow>n\<rightarrow> s3"
    80 
    81 | Cast:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1;
    82 	  s2 = abupd (raise_if (\<not>G,snd s1\<turnstile>v fits T) ClassCast) s1\<rbrakk> \<Longrightarrow>
    83 			        G\<turnstile>Norm s0 \<midarrow>Cast T e-\<succ>v\<midarrow>n\<rightarrow> s2"
    84 
    85 | Inst:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1;
    86 	  b = (v\<noteq>Null \<and> G,store s1\<turnstile>v fits RefT T)\<rbrakk> \<Longrightarrow>
    87 			      G\<turnstile>Norm s0 \<midarrow>e InstOf T-\<succ>Bool b\<midarrow>n\<rightarrow> s1"
    88 
    89 | Lit:			   "G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<midarrow>n\<rightarrow> Norm s"
    90 
    91 | UnOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1\<rbrakk> 
    92          \<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>(eval_unop unop v)\<midarrow>n\<rightarrow> s1"
    93 
    94 | BinOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<midarrow>n\<rightarrow> s1; 
    95            G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then (In1l e2) else (In1r Skip))
    96             \<succ>\<midarrow>n\<rightarrow> (In1 v2,s2)\<rbrakk> 
    97          \<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<midarrow>n\<rightarrow> s2"
    98 
    99 | Super:		   "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<midarrow>n\<rightarrow> Norm s"
   100 
   101 | Acc:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v,f)\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   102 	                          G\<turnstile>Norm s0 \<midarrow>Acc va-\<succ>v\<midarrow>n\<rightarrow> s1"
   103 
   104 | Ass:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(w,f)\<midarrow>n\<rightarrow> s1;
   105           G\<turnstile>     s1 \<midarrow>e-\<succ>v     \<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   106 				   G\<turnstile>Norm s0 \<midarrow>va:=e-\<succ>v\<midarrow>n\<rightarrow> assign f v s2"
   107 
   108 | Cond:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<midarrow>n\<rightarrow> s1;
   109           G\<turnstile>     s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   110 			    G\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<midarrow>n\<rightarrow> s2"
   111 
   112 | Call:	
   113   "\<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;
   114     D = invocation_declclass G mode (store s2) a' statT \<lparr>name=mn,parTs=pTs\<rparr>; 
   115     s3=init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' vs s2;
   116     s3' = check_method_access G accC statT mode \<lparr>name=mn,parTs=pTs\<rparr> a' s3;
   117     G\<turnstile>s3'\<midarrow>Methd D \<lparr>name=mn,parTs=pTs\<rparr>-\<succ>v\<midarrow>n\<rightarrow> s4
   118    \<rbrakk>
   119    \<Longrightarrow> 
   120     G\<turnstile>Norm s0 \<midarrow>{accC,statT,mode}e\<cdot>mn({pTs}args)-\<succ>v\<midarrow>n\<rightarrow> (restore_lvars s2 s4)"
   121 
   122 | Methd:"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   123 				G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<midarrow>Suc n\<rightarrow> s1"
   124 
   125 | Body:	"\<lbrakk>G\<turnstile>Norm s0\<midarrow>Init D\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c\<midarrow>n\<rightarrow> s2;
   126           s3 = (if (\<exists> l. abrupt s2 = Some (Jump (Break l)) \<or>  
   127                          abrupt s2 = Some (Jump (Cont l)))
   128                   then abupd (\<lambda> x. Some (Error CrossMethodJump)) s2 
   129                   else s2)\<rbrakk>\<Longrightarrow>
   130          G\<turnstile>Norm s0 \<midarrow>Body D c
   131           -\<succ>the (locals (store s2) Result)\<midarrow>n\<rightarrow>abupd (absorb Ret) s3"
   132 
   133 --{* evaluation of expression lists *}
   134 
   135 | Nil:
   136 				"G\<turnstile>Norm s0 \<midarrow>[]\<doteq>\<succ>[]\<midarrow>n\<rightarrow> Norm s0"
   137 
   138 | Cons:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e -\<succ> v \<midarrow>n\<rightarrow> s1;
   139           G\<turnstile>     s1 \<midarrow>es\<doteq>\<succ>vs\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   140 			     G\<turnstile>Norm s0 \<midarrow>e#es\<doteq>\<succ>v#vs\<midarrow>n\<rightarrow> s2"
   141 
   142 
   143 --{* execution of statements *}
   144 
   145 | Skip:	 			    "G\<turnstile>Norm s \<midarrow>Skip\<midarrow>n\<rightarrow> Norm s"
   146 
   147 | Expr:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   148 				  G\<turnstile>Norm s0 \<midarrow>Expr e\<midarrow>n\<rightarrow> s1"
   149 
   150 | Lab:  "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c \<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   151                              G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<midarrow>n\<rightarrow> abupd (absorb l) s1"
   152 
   153 | Comp:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1 \<midarrow>n\<rightarrow> s1;
   154 	  G\<turnstile>     s1 \<midarrow>c2 \<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   155 				 G\<turnstile>Norm s0 \<midarrow>c1;; c2\<midarrow>n\<rightarrow> s2"
   156 
   157 | If:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n\<rightarrow> s1;
   158 	  G\<turnstile>     s1\<midarrow>(if the_Bool b then c1 else c2)\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   159 		       G\<turnstile>Norm s0 \<midarrow>If(e) c1 Else c2 \<midarrow>n\<rightarrow> s2"
   160 
   161 | Loop:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n\<rightarrow> s1;
   162 	  if the_Bool b 
   163              then (G\<turnstile>s1 \<midarrow>c\<midarrow>n\<rightarrow> s2 \<and> 
   164                    G\<turnstile>(abupd (absorb (Cont l)) s2) \<midarrow>l\<bullet> While(e) c\<midarrow>n\<rightarrow> s3)
   165 	     else s3 = s1\<rbrakk> \<Longrightarrow>
   166 			      G\<turnstile>Norm s0 \<midarrow>l\<bullet> While(e) c\<midarrow>n\<rightarrow> s3"
   167   
   168 | Jmp: "G\<turnstile>Norm s \<midarrow>Jmp j\<midarrow>n\<rightarrow> (Some (Jump j), s)"
   169   
   170 | Throw:"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   171 				 G\<turnstile>Norm s0 \<midarrow>Throw e\<midarrow>n\<rightarrow> abupd (throw a') s1"
   172 
   173 | Try:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2;
   174 	  if G,s2\<turnstile>catch tn then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<midarrow>n\<rightarrow> s3 else s3 = s2\<rbrakk>
   175           \<Longrightarrow>
   176 		  G\<turnstile>Norm s0 \<midarrow>Try c1 Catch(tn vn) c2\<midarrow>n\<rightarrow> s3"
   177 
   178 | Fin:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n\<rightarrow> (x1,s1);
   179 	  G\<turnstile>Norm s1 \<midarrow>c2\<midarrow>n\<rightarrow> s2;
   180           s3=(if (\<exists> err. x1=Some (Error err)) 
   181               then (x1,s1) 
   182               else abupd (abrupt_if (x1\<noteq>None) x1) s2)\<rbrakk> \<Longrightarrow>
   183               G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<midarrow>n\<rightarrow> s3"
   184   
   185 | Init:	"\<lbrakk>the (class G C) = c;
   186 	  if inited C (globs s0) then s3 = Norm s0
   187 	  else (G\<turnstile>Norm (init_class_obj G C s0)
   188 	          \<midarrow>(if C = Object then Skip else Init (super c))\<midarrow>n\<rightarrow> s1 \<and>
   189 	        G\<turnstile>set_lvars empty s1 \<midarrow>init c\<midarrow>n\<rightarrow> s2 \<and> 
   190                 s3 = restore_lvars s1 s2)\<rbrakk>
   191           \<Longrightarrow>
   192 		 G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s3"
   193 monos
   194   if_bool_eq_conj
   195 
   196 
   197 declare split_if     [split del] split_if_asm     [split del]
   198         option.split [split del] option.split_asm [split del]
   199         not_None_eq [simp del] 
   200         split_paired_All [simp del] split_paired_Ex [simp del]
   201 declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
   202 
   203 inductive_cases evaln_cases: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v, s')"
   204 
   205 inductive_cases evaln_elim_cases:
   206 	"G\<turnstile>(Some xc, s) \<midarrow>t                        \<succ>\<midarrow>n\<rightarrow> (v, s')"
   207 	"G\<turnstile>Norm s \<midarrow>In1r Skip                      \<succ>\<midarrow>n\<rightarrow> (x, s')"
   208         "G\<turnstile>Norm s \<midarrow>In1r (Jmp j)                   \<succ>\<midarrow>n\<rightarrow> (x, s')"
   209         "G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> c)                    \<succ>\<midarrow>n\<rightarrow> (x, s')"
   210 	"G\<turnstile>Norm s \<midarrow>In3  ([])                      \<succ>\<midarrow>n\<rightarrow> (v, s')"
   211 	"G\<turnstile>Norm s \<midarrow>In3  (e#es)                    \<succ>\<midarrow>n\<rightarrow> (v, s')"
   212 	"G\<turnstile>Norm s \<midarrow>In1l (Lit w)                   \<succ>\<midarrow>n\<rightarrow> (v, s')"
   213         "G\<turnstile>Norm s \<midarrow>In1l (UnOp unop e)             \<succ>\<midarrow>n\<rightarrow> (v, s')"
   214         "G\<turnstile>Norm s \<midarrow>In1l (BinOp binop e1 e2)       \<succ>\<midarrow>n\<rightarrow> (v, s')"
   215 	"G\<turnstile>Norm s \<midarrow>In2  (LVar vn)                 \<succ>\<midarrow>n\<rightarrow> (v, s')"
   216 	"G\<turnstile>Norm s \<midarrow>In1l (Cast T e)                \<succ>\<midarrow>n\<rightarrow> (v, s')"
   217 	"G\<turnstile>Norm s \<midarrow>In1l (e InstOf T)              \<succ>\<midarrow>n\<rightarrow> (v, s')"
   218 	"G\<turnstile>Norm s \<midarrow>In1l (Super)                   \<succ>\<midarrow>n\<rightarrow> (v, s')"
   219 	"G\<turnstile>Norm s \<midarrow>In1l (Acc va)                  \<succ>\<midarrow>n\<rightarrow> (v, s')"
   220 	"G\<turnstile>Norm s \<midarrow>In1r (Expr e)                  \<succ>\<midarrow>n\<rightarrow> (x, s')"
   221 	"G\<turnstile>Norm s \<midarrow>In1r (c1;; c2)                 \<succ>\<midarrow>n\<rightarrow> (x, s')"
   222 	"G\<turnstile>Norm s \<midarrow>In1l (Methd C sig)             \<succ>\<midarrow>n\<rightarrow> (x, s')"
   223 	"G\<turnstile>Norm s \<midarrow>In1l (Body D c)                \<succ>\<midarrow>n\<rightarrow> (x, s')"
   224 	"G\<turnstile>Norm s \<midarrow>In1l (e0 ? e1 : e2)            \<succ>\<midarrow>n\<rightarrow> (v, s')"
   225 	"G\<turnstile>Norm s \<midarrow>In1r (If(e) c1 Else c2)        \<succ>\<midarrow>n\<rightarrow> (x, s')"
   226 	"G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> While(e) c)           \<succ>\<midarrow>n\<rightarrow> (x, s')"
   227 	"G\<turnstile>Norm s \<midarrow>In1r (c1 Finally c2)           \<succ>\<midarrow>n\<rightarrow> (x, s')"
   228 	"G\<turnstile>Norm s \<midarrow>In1r (Throw e)                 \<succ>\<midarrow>n\<rightarrow> (x, s')"
   229 	"G\<turnstile>Norm s \<midarrow>In1l (NewC C)                  \<succ>\<midarrow>n\<rightarrow> (v, s')"
   230 	"G\<turnstile>Norm s \<midarrow>In1l (New T[e])                \<succ>\<midarrow>n\<rightarrow> (v, s')"
   231 	"G\<turnstile>Norm s \<midarrow>In1l (Ass va e)                \<succ>\<midarrow>n\<rightarrow> (v, s')"
   232 	"G\<turnstile>Norm s \<midarrow>In1r (Try c1 Catch(tn vn) c2)  \<succ>\<midarrow>n\<rightarrow> (x, s')"
   233 	"G\<turnstile>Norm s \<midarrow>In2  ({accC,statDeclC,stat}e..fn) \<succ>\<midarrow>n\<rightarrow> (v, s')"
   234 	"G\<turnstile>Norm s \<midarrow>In2  (e1.[e2])                 \<succ>\<midarrow>n\<rightarrow> (v, s')"
   235 	"G\<turnstile>Norm s \<midarrow>In1l ({accC,statT,mode}e\<cdot>mn({pT}p)) \<succ>\<midarrow>n\<rightarrow> (v, s')"
   236 	"G\<turnstile>Norm s \<midarrow>In1r (Init C)                  \<succ>\<midarrow>n\<rightarrow> (x, s')"
   237         "G\<turnstile>Norm s \<midarrow>In1r (Init C)                  \<succ>\<midarrow>n\<rightarrow> (x, s')"
   238 
   239 declare split_if     [split] split_if_asm     [split] 
   240         option.split [split] option.split_asm [split]
   241         not_None_eq [simp] 
   242         split_paired_All [simp] split_paired_Ex [simp]
   243 declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
   244 
   245 lemma evaln_Inj_elim: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (w,s') \<Longrightarrow> case t of In1 ec \<Rightarrow>  
   246   (case ec of Inl e \<Rightarrow> (\<exists>v. w = In1 v) | Inr c \<Rightarrow> w = \<diamondsuit>)  
   247   | In2 e \<Rightarrow> (\<exists>v. w = In2 v) | In3 e \<Rightarrow> (\<exists>v. w = In3 v)"
   248 apply (erule evaln_cases , auto)
   249 apply (induct_tac "t")
   250 apply   (induct_tac "a")
   251 apply auto
   252 done
   253 
   254 text {* The following simplification procedures set up the proper injections of
   255  terms and their corresponding values in the evaluation relation:
   256  E.g. an expression 
   257  (injection @{term In1l} into terms) always evaluates to ordinary values 
   258  (injection @{term In1} into generalised values @{term vals}). 
   259 *}
   260 
   261 lemma evaln_expr_eq: "G\<turnstile>s \<midarrow>In1l t\<succ>\<midarrow>n\<rightarrow> (w, s') = (\<exists>v. w=In1 v \<and> G\<turnstile>s \<midarrow>t-\<succ>v \<midarrow>n\<rightarrow> s')"
   262   by (auto, frule evaln_Inj_elim, auto)
   263 
   264 lemma evaln_var_eq: "G\<turnstile>s \<midarrow>In2 t\<succ>\<midarrow>n\<rightarrow> (w, s') = (\<exists>vf. w=In2 vf \<and> G\<turnstile>s \<midarrow>t=\<succ>vf\<midarrow>n\<rightarrow> s')"
   265   by (auto, frule evaln_Inj_elim, auto)
   266 
   267 lemma evaln_exprs_eq: "G\<turnstile>s \<midarrow>In3 t\<succ>\<midarrow>n\<rightarrow> (w, s') = (\<exists>vs. w=In3 vs \<and> G\<turnstile>s \<midarrow>t\<doteq>\<succ>vs\<midarrow>n\<rightarrow> s')"
   268   by (auto, frule evaln_Inj_elim, auto)
   269 
   270 lemma evaln_stmt_eq: "G\<turnstile>s \<midarrow>In1r t\<succ>\<midarrow>n\<rightarrow> (w, s') = (w=\<diamondsuit> \<and> G\<turnstile>s \<midarrow>t \<midarrow>n\<rightarrow> s')"
   271   by (auto, frule evaln_Inj_elim, auto, frule evaln_Inj_elim, auto)
   272 
   273 simproc_setup evaln_expr ("G\<turnstile>s \<midarrow>In1l t\<succ>\<midarrow>n\<rightarrow> (w, s')") = {*
   274   fn _ => fn _ => fn ct =>
   275     (case Thm.term_of ct of
   276       (_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
   277     | _ => SOME (mk_meta_eq @{thm evaln_expr_eq})) *}
   278 
   279 simproc_setup evaln_var ("G\<turnstile>s \<midarrow>In2 t\<succ>\<midarrow>n\<rightarrow> (w, s')") = {*
   280   fn _ => fn _ => fn ct =>
   281     (case Thm.term_of ct of
   282       (_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
   283     | _ => SOME (mk_meta_eq @{thm evaln_var_eq})) *}
   284 
   285 simproc_setup evaln_exprs ("G\<turnstile>s \<midarrow>In3 t\<succ>\<midarrow>n\<rightarrow> (w, s')") = {*
   286   fn _ => fn _ => fn ct =>
   287     (case Thm.term_of ct of
   288       (_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
   289     | _ => SOME (mk_meta_eq @{thm evaln_exprs_eq})) *}
   290 
   291 simproc_setup evaln_stmt ("G\<turnstile>s \<midarrow>In1r t\<succ>\<midarrow>n\<rightarrow> (w, s')") = {*
   292   fn _ => fn _ => fn ct =>
   293     (case Thm.term_of ct of
   294       (_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
   295     | _ => SOME (mk_meta_eq @{thm evaln_stmt_eq})) *}
   296 
   297 ML {* bind_thms ("evaln_AbruptIs", sum3_instantiate @{context} @{thm evaln.Abrupt}) *}
   298 declare evaln_AbruptIs [intro!]
   299 
   300 lemma evaln_Callee: "G\<turnstile>Norm s\<midarrow>In1l (Callee l e)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
   301 proof -
   302   { fix s t v s'
   303     assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
   304          normal: "normal s" and
   305          callee: "t=In1l (Callee l e)"
   306     then have "False" by induct auto
   307   }
   308   then show ?thesis
   309     by (cases s') fastsimp 
   310 qed
   311 
   312 lemma evaln_InsInitE: "G\<turnstile>Norm s\<midarrow>In1l (InsInitE c e)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
   313 proof -
   314   { fix s t v s'
   315     assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
   316          normal: "normal s" and
   317          callee: "t=In1l (InsInitE c e)"
   318     then have "False" by induct auto
   319   }
   320   then show ?thesis
   321     by (cases s') fastsimp
   322 qed
   323 
   324 lemma evaln_InsInitV: "G\<turnstile>Norm s\<midarrow>In2 (InsInitV c w)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
   325 proof -
   326   { fix s t v s'
   327     assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
   328          normal: "normal s" and
   329          callee: "t=In2 (InsInitV c w)"
   330     then have "False" by induct auto
   331   }  
   332   then show ?thesis
   333     by (cases s') fastsimp
   334 qed
   335 
   336 lemma evaln_FinA: "G\<turnstile>Norm s\<midarrow>In1r (FinA a c)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
   337 proof -
   338   { fix s t v s'
   339     assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
   340          normal: "normal s" and
   341          callee: "t=In1r (FinA a c)"
   342     then have "False" by induct auto
   343   } 
   344   then show ?thesis
   345     by (cases s') fastsimp
   346 qed
   347 
   348 lemma evaln_abrupt_lemma: "G\<turnstile>s \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (v,s') \<Longrightarrow> 
   349  fst s = Some xc \<longrightarrow> s' = s \<and> v = undefined3 e"
   350 apply (erule evaln_cases , auto)
   351 done
   352 
   353 lemma evaln_abrupt: 
   354  "\<And>s'. G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (w,s') = (s' = (Some xc,s) \<and>  
   355   w=undefined3 e \<and> G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (undefined3 e,(Some xc,s)))"
   356 apply auto
   357 apply (frule evaln_abrupt_lemma, auto)+
   358 done
   359 
   360 simproc_setup evaln_abrupt ("G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (w,s')") = {*
   361   fn _ => fn _ => fn ct =>
   362     (case Thm.term_of ct of
   363       (_ $ _ $ _ $ _ $ _ $ _ $ (Const (@{const_name Pair}, _) $ (Const (@{const_name Some},_) $ _)$ _))
   364         => NONE
   365     | _ => SOME (mk_meta_eq @{thm evaln_abrupt}))
   366 *}
   367 
   368 lemma evaln_LitI: "G\<turnstile>s \<midarrow>Lit v-\<succ>(if normal s then v else undefined)\<midarrow>n\<rightarrow> s"
   369 apply (case_tac "s", case_tac "a = None")
   370 by (auto intro!: evaln.Lit)
   371 
   372 lemma CondI: 
   373  "\<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> 
   374   G\<turnstile>s \<midarrow>e ? e1 : e2-\<succ>(if normal s1 then v else undefined)\<midarrow>n\<rightarrow> s2"
   375 apply (case_tac "s", case_tac "a = None")
   376 by (auto intro!: evaln.Cond)
   377 
   378 lemma evaln_SkipI [intro!]: "G\<turnstile>s \<midarrow>Skip\<midarrow>n\<rightarrow> s"
   379 apply (case_tac "s", case_tac "a = None")
   380 by (auto intro!: evaln.Skip)
   381 
   382 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'"
   383 apply (case_tac "s", case_tac "a = None")
   384 by (auto intro!: evaln.Expr)
   385 
   386 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"
   387 apply (case_tac "s", case_tac "a = None")
   388 by (auto intro!: evaln.Comp)
   389 
   390 lemma evaln_IfI: 
   391  "\<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> 
   392   G\<turnstile>s \<midarrow>If(e) c1 Else c2\<midarrow>n\<rightarrow> s2"
   393 apply (case_tac "s", case_tac "a = None")
   394 by (auto intro!: evaln.If)
   395 
   396 lemma evaln_SkipD [dest!]: "G\<turnstile>s \<midarrow>Skip\<midarrow>n\<rightarrow> s' \<Longrightarrow> s' = s" 
   397 by (erule evaln_cases, auto)
   398 
   399 lemma evaln_Skip_eq [simp]: "G\<turnstile>s \<midarrow>Skip\<midarrow>n\<rightarrow> s' = (s = s')"
   400 apply auto
   401 done
   402 
   403 
   404 
   405 
   406 section {* evaln implies eval *}
   407 
   408 lemma evaln_eval:  
   409   assumes evaln: "G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)" 
   410   shows "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"
   411 using evaln 
   412 proof (induct)
   413   case (Loop s0 e b n s1 c s2 l s3)
   414   note `G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1`
   415   moreover
   416   have "if the_Bool b
   417         then (G\<turnstile>s1 \<midarrow>c\<rightarrow> s2) \<and> 
   418              G\<turnstile>abupd (absorb (Cont l)) s2 \<midarrow>l\<bullet> While(e) c\<rightarrow> s3
   419         else s3 = s1"
   420     using Loop.hyps by simp
   421   ultimately show ?case by (rule eval.Loop)
   422 next
   423   case (Try s0 c1 n s1 s2 C vn c2 s3)
   424   note `G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1`
   425   moreover
   426   note `G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2`
   427   moreover
   428   have "if G,s2\<turnstile>catch C then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<rightarrow> s3 else s3 = s2"
   429     using Try.hyps by simp
   430   ultimately show ?case by (rule eval.Try)
   431 next
   432   case (Init C c s0 s3 n s1 s2)
   433   note `the (class G C) = c`
   434   moreover
   435   have "if inited C (globs s0) 
   436            then s3 = Norm s0
   437            else G\<turnstile>Norm ((init_class_obj G C) s0) 
   438                   \<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1 \<and>
   439                 G\<turnstile>(set_lvars empty) s1 \<midarrow>init c\<rightarrow> s2 \<and>
   440                 s3 = (set_lvars (locals (store s1))) s2"
   441     using Init.hyps by simp
   442   ultimately show ?case by (rule eval.Init)
   443 qed (rule eval.intros,(assumption+ | assumption?))+
   444 
   445 lemma Suc_le_D_lemma: "\<lbrakk>Suc n <= m'; (\<And>m. n <= m \<Longrightarrow> P (Suc m)) \<rbrakk> \<Longrightarrow> P m'"
   446 apply (frule Suc_le_D)
   447 apply fast
   448 done
   449 
   450 lemma evaln_nonstrict [rule_format (no_asm), elim]: 
   451   "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (w, s') \<Longrightarrow> \<forall>m. n\<le>m \<longrightarrow> G\<turnstile>s \<midarrow>t\<succ>\<midarrow>m\<rightarrow> (w, s')"
   452 apply (erule evaln.induct)
   453 apply (tactic {* ALLGOALS (EVERY'[strip_tac, TRY o etac (thm "Suc_le_D_lemma"),
   454   REPEAT o smp_tac 1, 
   455   resolve_tac (thms "evaln.intros") THEN_ALL_NEW TRY o atac]) *})
   456 (* 3 subgoals *)
   457 apply (auto split del: split_if)
   458 done
   459 
   460 lemmas evaln_nonstrict_Suc = evaln_nonstrict [OF _ le_refl [THEN le_SucI]]
   461 
   462 lemma evaln_max2: "\<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>n1\<rightarrow> (w1, s1'); G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>n2\<rightarrow> (w2, s2')\<rbrakk> \<Longrightarrow> 
   463              G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max n1 n2\<rightarrow> (w1, s1') \<and> G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max n1 n2\<rightarrow> (w2, s2')"
   464 by (fast intro: le_maxI1 le_maxI2)
   465 
   466 corollary evaln_max2E [consumes 2]:
   467   "\<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>n1\<rightarrow> (w1, s1'); G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>n2\<rightarrow> (w2, s2'); 
   468     \<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max n1 n2\<rightarrow> (w1, s1');G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max n1 n2\<rightarrow> (w2, s2') \<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
   469 by (drule (1) evaln_max2) simp
   470 
   471 
   472 lemma evaln_max3: 
   473 "\<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>n1\<rightarrow> (w1, s1'); G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>n2\<rightarrow> (w2, s2'); G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>n3\<rightarrow> (w3, s3')\<rbrakk> \<Longrightarrow>
   474  G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> (w1, s1') \<and>
   475  G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> (w2, s2') \<and> 
   476  G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> (w3, s3')"
   477 apply (drule (1) evaln_max2, erule thin_rl)
   478 apply (fast intro!: le_maxI1 le_maxI2)
   479 done
   480 
   481 corollary evaln_max3E: 
   482 "\<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>n1\<rightarrow> (w1, s1'); G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>n2\<rightarrow> (w2, s2'); G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>n3\<rightarrow> (w3, s3');
   483    \<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> (w1, s1');
   484     G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> (w2, s2'); 
   485     G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> (w3, s3')
   486    \<rbrakk> \<Longrightarrow> P
   487   \<rbrakk> \<Longrightarrow> P"
   488 by (drule (2) evaln_max3) simp
   489 
   490 
   491 lemma le_max3I1: "(n2::nat) \<le> max n1 (max n2 n3)"
   492 proof -
   493   have "n2 \<le> max n2 n3"
   494     by (rule le_maxI1)
   495   also
   496   have "max n2 n3 \<le> max n1 (max n2 n3)"
   497     by (rule le_maxI2)
   498   finally
   499   show ?thesis .
   500 qed
   501 
   502 lemma le_max3I2: "(n3::nat) \<le> max n1 (max n2 n3)"
   503 proof -
   504   have "n3 \<le> max n2 n3"
   505     by (rule le_maxI2)
   506   also
   507   have "max n2 n3 \<le> max n1 (max n2 n3)"
   508     by (rule le_maxI2)
   509   finally
   510   show ?thesis .
   511 qed
   512 
   513 declare [[simproc del: wt_expr wt_var wt_exprs wt_stmt]]
   514 
   515 section {* eval implies evaln *}
   516 lemma eval_evaln: 
   517   assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"
   518   shows  "\<exists>n. G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)"
   519 using eval 
   520 proof (induct)
   521   case (Abrupt xc s t)
   522   obtain n where
   523     "G\<turnstile>(Some xc, s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (undefined3 t, (Some xc, s))"
   524     by (iprover intro: evaln.Abrupt)
   525   then show ?case ..
   526 next
   527   case Skip
   528   show ?case by (blast intro: evaln.Skip)
   529 next
   530   case (Expr s0 e v s1)
   531   then obtain n where
   532     "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
   533     by (iprover)
   534   then have "G\<turnstile>Norm s0 \<midarrow>Expr e\<midarrow>n\<rightarrow> s1"
   535     by (rule evaln.Expr) 
   536   then show ?case ..
   537 next
   538   case (Lab s0 c s1 l)
   539   then obtain n where
   540     "G\<turnstile>Norm s0 \<midarrow>c\<midarrow>n\<rightarrow> s1"
   541     by (iprover)
   542   then have "G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<midarrow>n\<rightarrow> abupd (absorb l) s1"
   543     by (rule evaln.Lab)
   544   then show ?case ..
   545 next
   546   case (Comp s0 c1 s1 c2 s2)
   547   then obtain n1 n2 where
   548     "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> s1"
   549     "G\<turnstile>s1 \<midarrow>c2\<midarrow>n2\<rightarrow> s2"
   550     by (iprover)
   551   then have "G\<turnstile>Norm s0 \<midarrow>c1;; c2\<midarrow>max n1 n2\<rightarrow> s2"
   552     by (blast intro: evaln.Comp dest: evaln_max2 )
   553   then show ?case ..
   554 next
   555   case (If s0 e b s1 c1 c2 s2)
   556   then obtain n1 n2 where
   557     "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n1\<rightarrow> s1"
   558     "G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<midarrow>n2\<rightarrow> s2"
   559     by (iprover)
   560   then have "G\<turnstile>Norm s0 \<midarrow>If(e) c1 Else c2\<midarrow>max n1 n2\<rightarrow> s2"
   561     by (blast intro: evaln.If dest: evaln_max2)
   562   then show ?case ..
   563 next
   564   case (Loop s0 e b s1 c s2 l s3)
   565   from Loop.hyps obtain n1 where
   566     "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n1\<rightarrow> s1"
   567     by (iprover)
   568   moreover from Loop.hyps obtain n2 where
   569     "if the_Bool b 
   570         then (G\<turnstile>s1 \<midarrow>c\<midarrow>n2\<rightarrow> s2 \<and> 
   571               G\<turnstile>(abupd (absorb (Cont l)) s2)\<midarrow>l\<bullet> While(e) c\<midarrow>n2\<rightarrow> s3)
   572 	else s3 = s1"
   573     by simp (iprover intro: evaln_nonstrict le_maxI1 le_maxI2)
   574   ultimately
   575   have "G\<turnstile>Norm s0 \<midarrow>l\<bullet> While(e) c\<midarrow>max n1 n2\<rightarrow> s3"
   576     apply -
   577     apply (rule evaln.Loop)
   578     apply   (iprover intro: evaln_nonstrict intro: le_maxI1)
   579 
   580     apply   (auto intro: evaln_nonstrict intro: le_maxI2)
   581     done
   582   then show ?case ..
   583 next
   584   case (Jmp s j)
   585   fix n have "G\<turnstile>Norm s \<midarrow>Jmp j\<midarrow>n\<rightarrow> (Some (Jump j), s)"
   586     by (rule evaln.Jmp)
   587   then show ?case ..
   588 next
   589   case (Throw s0 e a s1)
   590   then obtain n where
   591     "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<midarrow>n\<rightarrow> s1"
   592     by (iprover)
   593   then have "G\<turnstile>Norm s0 \<midarrow>Throw e\<midarrow>n\<rightarrow> abupd (throw a) s1"
   594     by (rule evaln.Throw)
   595   then show ?case ..
   596 next 
   597   case (Try s0 c1 s1 s2 catchC vn c2 s3)
   598   from Try.hyps obtain n1 where
   599     "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> s1"
   600     by (iprover)
   601   moreover 
   602   note sxalloc = `G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2`
   603   moreover
   604   from Try.hyps obtain n2 where
   605     "if G,s2\<turnstile>catch catchC then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<midarrow>n2\<rightarrow> s3 else s3 = s2"
   606     by fastsimp 
   607   ultimately
   608   have "G\<turnstile>Norm s0 \<midarrow>Try c1 Catch(catchC vn) c2\<midarrow>max n1 n2\<rightarrow> s3"
   609     by (auto intro!: evaln.Try le_maxI1 le_maxI2)
   610   then show ?case ..
   611 next
   612   case (Fin s0 c1 x1 s1 c2 s2 s3)
   613   from Fin obtain n1 n2 where 
   614     "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> (x1, s1)"
   615     "G\<turnstile>Norm s1 \<midarrow>c2\<midarrow>n2\<rightarrow> s2"
   616     by iprover
   617   moreover
   618   note s3 = `s3 = (if \<exists>err. x1 = Some (Error err) 
   619                    then (x1, s1)
   620                    else abupd (abrupt_if (x1 \<noteq> None) x1) s2)`
   621   ultimately 
   622   have 
   623     "G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<midarrow>max n1 n2\<rightarrow> s3"
   624     by (blast intro: evaln.Fin dest: evaln_max2)
   625   then show ?case ..
   626 next
   627   case (Init C c s0 s3 s1 s2)
   628   note cls = `the (class G C) = c`
   629   moreover from Init.hyps obtain n where
   630       "if inited C (globs s0) then s3 = Norm s0
   631        else (G\<turnstile>Norm (init_class_obj G C s0)
   632 	      \<midarrow>(if C = Object then Skip else Init (super c))\<midarrow>n\<rightarrow> s1 \<and>
   633 	           G\<turnstile>set_lvars empty s1 \<midarrow>init c\<midarrow>n\<rightarrow> s2 \<and> 
   634                    s3 = restore_lvars s1 s2)"
   635     by (auto intro: evaln_nonstrict le_maxI1 le_maxI2)
   636   ultimately have "G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s3"
   637     by (rule evaln.Init)
   638   then show ?case ..
   639 next
   640   case (NewC s0 C s1 a s2)
   641   then obtain n where 
   642     "G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s1"
   643     by (iprover)
   644   with NewC 
   645   have "G\<turnstile>Norm s0 \<midarrow>NewC C-\<succ>Addr a\<midarrow>n\<rightarrow> s2"
   646     by (iprover intro: evaln.NewC)
   647   then show ?case ..
   648 next
   649   case (NewA s0 T s1 e i s2 a s3)
   650   then obtain n1 n2 where 
   651     "G\<turnstile>Norm s0 \<midarrow>init_comp_ty T\<midarrow>n1\<rightarrow> s1"
   652     "G\<turnstile>s1 \<midarrow>e-\<succ>i\<midarrow>n2\<rightarrow> s2"      
   653     by (iprover)
   654   moreover
   655   note `G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3`
   656   ultimately
   657   have "G\<turnstile>Norm s0 \<midarrow>New T[e]-\<succ>Addr a\<midarrow>max n1 n2\<rightarrow> s3"
   658     by (blast intro: evaln.NewA dest: evaln_max2)
   659   then show ?case ..
   660 next
   661   case (Cast s0 e v s1 s2 castT)
   662   then obtain n where
   663     "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
   664     by (iprover)
   665   moreover 
   666   note `s2 = abupd (raise_if (\<not> G,snd s1\<turnstile>v fits castT) ClassCast) s1`
   667   ultimately
   668   have "G\<turnstile>Norm s0 \<midarrow>Cast castT e-\<succ>v\<midarrow>n\<rightarrow> s2"
   669     by (rule evaln.Cast)
   670   then show ?case ..
   671 next
   672   case (Inst s0 e v s1 b T)
   673   then obtain n where
   674     "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
   675     by (iprover)
   676   moreover 
   677   note `b = (v \<noteq> Null \<and> G,snd s1\<turnstile>v fits RefT T)`
   678   ultimately
   679   have "G\<turnstile>Norm s0 \<midarrow>e InstOf T-\<succ>Bool b\<midarrow>n\<rightarrow> s1"
   680     by (rule evaln.Inst)
   681   then show ?case ..
   682 next
   683   case (Lit s v)
   684   fix n have "G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<midarrow>n\<rightarrow> Norm s"
   685     by (rule evaln.Lit)
   686   then show ?case ..
   687 next
   688   case (UnOp s0 e v s1 unop)
   689   then obtain n where
   690     "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
   691     by (iprover)
   692   hence "G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>eval_unop unop v\<midarrow>n\<rightarrow> s1"
   693     by (rule evaln.UnOp)
   694   then show ?case ..
   695 next
   696   case (BinOp s0 e1 v1 s1 binop e2 v2 s2)
   697   then obtain n1 n2 where 
   698     "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<midarrow>n1\<rightarrow> s1"
   699     "G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then In1l e2
   700                else In1r Skip)\<succ>\<midarrow>n2\<rightarrow> (In1 v2, s2)"    
   701     by (iprover)
   702   hence "G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<midarrow>max n1 n2
   703           \<rightarrow> s2"
   704     by (blast intro!: evaln.BinOp dest: evaln_max2)
   705   then show ?case ..
   706 next
   707   case (Super s )
   708   fix n have "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<midarrow>n\<rightarrow> Norm s"
   709     by (rule evaln.Super)
   710   then show ?case ..
   711 next
   712   case (Acc s0 va v f s1)
   713   then obtain n where
   714     "G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v, f)\<midarrow>n\<rightarrow> s1"
   715     by (iprover)
   716   then
   717   have "G\<turnstile>Norm s0 \<midarrow>Acc va-\<succ>v\<midarrow>n\<rightarrow> s1"
   718     by (rule evaln.Acc)
   719   then show ?case ..
   720 next
   721   case (Ass s0 var w f s1 e v s2)
   722   then obtain n1 n2 where 
   723     "G\<turnstile>Norm s0 \<midarrow>var=\<succ>(w, f)\<midarrow>n1\<rightarrow> s1"
   724     "G\<turnstile>s1 \<midarrow>e-\<succ>v\<midarrow>n2\<rightarrow> s2"      
   725     by (iprover)
   726   then
   727   have "G\<turnstile>Norm s0 \<midarrow>var:=e-\<succ>v\<midarrow>max n1 n2\<rightarrow> assign f v s2"
   728     by (blast intro: evaln.Ass dest: evaln_max2)
   729   then show ?case ..
   730 next
   731   case (Cond s0 e0 b s1 e1 e2 v s2)
   732   then obtain n1 n2 where 
   733     "G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<midarrow>n1\<rightarrow> s1"
   734     "G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<midarrow>n2\<rightarrow> s2"
   735     by (iprover)
   736   then
   737   have "G\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<midarrow>max n1 n2\<rightarrow> s2"
   738     by (blast intro: evaln.Cond dest: evaln_max2)
   739   then show ?case ..
   740 next
   741   case (Call s0 e a' s1 args vs s2 invDeclC mode statT mn pTs' s3 s3' accC' v s4)
   742   then obtain n1 n2 where
   743     "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n1\<rightarrow> s1"
   744     "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<midarrow>n2\<rightarrow> s2"
   745     by iprover
   746   moreover
   747   note `invDeclC = invocation_declclass G mode (store s2) a' statT 
   748                        \<lparr>name=mn,parTs=pTs'\<rparr>`
   749   moreover
   750   note `s3 = init_lvars G invDeclC \<lparr>name=mn,parTs=pTs'\<rparr> mode a' vs s2`
   751   moreover
   752   note `s3'=check_method_access G accC' statT mode \<lparr>name=mn,parTs=pTs'\<rparr> a' s3`
   753   moreover 
   754   from Call.hyps
   755   obtain m where 
   756     "G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name=mn, parTs=pTs'\<rparr>-\<succ>v\<midarrow>m\<rightarrow> s4"
   757     by iprover
   758   ultimately
   759   have "G\<turnstile>Norm s0 \<midarrow>{accC',statT,mode}e\<cdot>mn( {pTs'}args)-\<succ>v\<midarrow>max n1 (max n2 m)\<rightarrow> 
   760             (set_lvars (locals (store s2))) s4"
   761     by (auto intro!: evaln.Call le_maxI1 le_max3I1 le_max3I2)
   762   thus ?case ..
   763 next
   764   case (Methd s0 D sig v s1)
   765   then obtain n where
   766     "G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<midarrow>n\<rightarrow> s1"
   767     by iprover
   768   then have "G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<midarrow>Suc n\<rightarrow> s1"
   769     by (rule evaln.Methd)
   770   then show ?case ..
   771 next
   772   case (Body s0 D s1 c s2 s3)
   773   from Body.hyps obtain n1 n2 where 
   774     evaln_init: "G\<turnstile>Norm s0 \<midarrow>Init D\<midarrow>n1\<rightarrow> s1" and
   775     evaln_c: "G\<turnstile>s1 \<midarrow>c\<midarrow>n2\<rightarrow> s2"
   776     by (iprover)
   777   moreover
   778   note `s3 = (if \<exists>l. fst s2 = Some (Jump (Break l)) \<or> 
   779                      fst s2 = Some (Jump (Cont l))
   780               then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2 
   781               else s2)`
   782   ultimately
   783   have
   784      "G\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>the (locals (store s2) Result)\<midarrow>max n1 n2
   785        \<rightarrow> abupd (absorb Ret) s3"
   786     by (iprover intro: evaln.Body dest: evaln_max2)
   787   then show ?case ..
   788 next
   789   case (LVar s vn )
   790   obtain n where
   791     "G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<midarrow>n\<rightarrow> Norm s"
   792     by (iprover intro: evaln.LVar)
   793   then show ?case ..
   794 next
   795   case (FVar s0 statDeclC s1 e a s2 v s2' stat fn s3 accC)
   796   then obtain n1 n2 where
   797     "G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<midarrow>n1\<rightarrow> s1"
   798     "G\<turnstile>s1 \<midarrow>e-\<succ>a\<midarrow>n2\<rightarrow> s2"
   799     by iprover
   800   moreover
   801   note `s3 = check_field_access G accC statDeclC fn stat a s2'`
   802     and `(v, s2') = fvar statDeclC stat fn a s2`
   803   ultimately
   804   have "G\<turnstile>Norm s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>v\<midarrow>max n1 n2\<rightarrow> s3"
   805     by (iprover intro: evaln.FVar dest: evaln_max2)
   806   then show ?case ..
   807 next
   808   case (AVar s0 e1 a s1 e2 i s2 v s2')
   809   then obtain n1 n2 where 
   810     "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>a\<midarrow>n1\<rightarrow> s1"
   811     "G\<turnstile>s1 \<midarrow>e2-\<succ>i\<midarrow>n2\<rightarrow> s2"      
   812     by iprover
   813   moreover 
   814   note `(v, s2') = avar G i a s2`
   815   ultimately 
   816   have "G\<turnstile>Norm s0 \<midarrow>e1.[e2]=\<succ>v\<midarrow>max n1 n2\<rightarrow> s2'"
   817     by (blast intro!: evaln.AVar dest: evaln_max2)
   818   then show ?case ..
   819 next
   820   case (Nil s0)
   821   show ?case by (iprover intro: evaln.Nil)
   822 next
   823   case (Cons s0 e v s1 es vs s2)
   824   then obtain n1 n2 where 
   825     "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n1\<rightarrow> s1"
   826     "G\<turnstile>s1 \<midarrow>es\<doteq>\<succ>vs\<midarrow>n2\<rightarrow> s2"      
   827     by iprover
   828   then
   829   have "G\<turnstile>Norm s0 \<midarrow>e # es\<doteq>\<succ>v # vs\<midarrow>max n1 n2\<rightarrow> s2"
   830     by (blast intro!: evaln.Cons dest: evaln_max2)
   831   then show ?case ..
   832 qed
   833 
   834 end