src/HOL/Bali/Evaln.thy
author haftmann
Wed Jan 31 16:05:10 2007 +0100 (2007-01-31)
changeset 22218 30a8890d2967
parent 21765 89275a3ed7be
child 23350 50c5b0912a0c
permissions -rw-r--r--
dropped lemma duplicates in HOL.thy
     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 inductive2
    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> (arbitrary3 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 ML_setup {*
   202 change_simpset (fn ss => ss delloop "split_all_tac");
   203 *}
   204 inductive_cases2 evaln_cases: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v, s')"
   205 
   206 inductive_cases2 evaln_elim_cases:
   207 	"G\<turnstile>(Some xc, s) \<midarrow>t                        \<succ>\<midarrow>n\<rightarrow> (v, s')"
   208 	"G\<turnstile>Norm s \<midarrow>In1r Skip                      \<succ>\<midarrow>n\<rightarrow> (x, s')"
   209         "G\<turnstile>Norm s \<midarrow>In1r (Jmp j)                   \<succ>\<midarrow>n\<rightarrow> (x, s')"
   210         "G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> c)                    \<succ>\<midarrow>n\<rightarrow> (x, s')"
   211 	"G\<turnstile>Norm s \<midarrow>In3  ([])                      \<succ>\<midarrow>n\<rightarrow> (v, s')"
   212 	"G\<turnstile>Norm s \<midarrow>In3  (e#es)                    \<succ>\<midarrow>n\<rightarrow> (v, s')"
   213 	"G\<turnstile>Norm s \<midarrow>In1l (Lit w)                   \<succ>\<midarrow>n\<rightarrow> (v, s')"
   214         "G\<turnstile>Norm s \<midarrow>In1l (UnOp unop e)             \<succ>\<midarrow>n\<rightarrow> (v, s')"
   215         "G\<turnstile>Norm s \<midarrow>In1l (BinOp binop e1 e2)       \<succ>\<midarrow>n\<rightarrow> (v, s')"
   216 	"G\<turnstile>Norm s \<midarrow>In2  (LVar vn)                 \<succ>\<midarrow>n\<rightarrow> (v, s')"
   217 	"G\<turnstile>Norm s \<midarrow>In1l (Cast T e)                \<succ>\<midarrow>n\<rightarrow> (v, s')"
   218 	"G\<turnstile>Norm s \<midarrow>In1l (e InstOf T)              \<succ>\<midarrow>n\<rightarrow> (v, s')"
   219 	"G\<turnstile>Norm s \<midarrow>In1l (Super)                   \<succ>\<midarrow>n\<rightarrow> (v, s')"
   220 	"G\<turnstile>Norm s \<midarrow>In1l (Acc va)                  \<succ>\<midarrow>n\<rightarrow> (v, s')"
   221 	"G\<turnstile>Norm s \<midarrow>In1r (Expr e)                  \<succ>\<midarrow>n\<rightarrow> (x, s')"
   222 	"G\<turnstile>Norm s \<midarrow>In1r (c1;; c2)                 \<succ>\<midarrow>n\<rightarrow> (x, s')"
   223 	"G\<turnstile>Norm s \<midarrow>In1l (Methd C sig)             \<succ>\<midarrow>n\<rightarrow> (x, s')"
   224 	"G\<turnstile>Norm s \<midarrow>In1l (Body D c)                \<succ>\<midarrow>n\<rightarrow> (x, s')"
   225 	"G\<turnstile>Norm s \<midarrow>In1l (e0 ? e1 : e2)            \<succ>\<midarrow>n\<rightarrow> (v, s')"
   226 	"G\<turnstile>Norm s \<midarrow>In1r (If(e) c1 Else c2)        \<succ>\<midarrow>n\<rightarrow> (x, s')"
   227 	"G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> While(e) c)           \<succ>\<midarrow>n\<rightarrow> (x, s')"
   228 	"G\<turnstile>Norm s \<midarrow>In1r (c1 Finally c2)           \<succ>\<midarrow>n\<rightarrow> (x, s')"
   229 	"G\<turnstile>Norm s \<midarrow>In1r (Throw e)                 \<succ>\<midarrow>n\<rightarrow> (x, s')"
   230 	"G\<turnstile>Norm s \<midarrow>In1l (NewC C)                  \<succ>\<midarrow>n\<rightarrow> (v, s')"
   231 	"G\<turnstile>Norm s \<midarrow>In1l (New T[e])                \<succ>\<midarrow>n\<rightarrow> (v, s')"
   232 	"G\<turnstile>Norm s \<midarrow>In1l (Ass va e)                \<succ>\<midarrow>n\<rightarrow> (v, s')"
   233 	"G\<turnstile>Norm s \<midarrow>In1r (Try c1 Catch(tn vn) c2)  \<succ>\<midarrow>n\<rightarrow> (x, s')"
   234 	"G\<turnstile>Norm s \<midarrow>In2  ({accC,statDeclC,stat}e..fn) \<succ>\<midarrow>n\<rightarrow> (v, s')"
   235 	"G\<turnstile>Norm s \<midarrow>In2  (e1.[e2])                 \<succ>\<midarrow>n\<rightarrow> (v, s')"
   236 	"G\<turnstile>Norm s \<midarrow>In1l ({accC,statT,mode}e\<cdot>mn({pT}p)) \<succ>\<midarrow>n\<rightarrow> (v, s')"
   237 	"G\<turnstile>Norm s \<midarrow>In1r (Init C)                  \<succ>\<midarrow>n\<rightarrow> (x, s')"
   238         "G\<turnstile>Norm s \<midarrow>In1r (Init C)                  \<succ>\<midarrow>n\<rightarrow> (x, s')"
   239 
   240 declare split_if     [split] split_if_asm     [split] 
   241         option.split [split] option.split_asm [split]
   242         not_None_eq [simp] 
   243         split_paired_All [simp] split_paired_Ex [simp]
   244 ML_setup {*
   245 change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
   246 *}
   247 lemma evaln_Inj_elim: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (w,s') \<Longrightarrow> case t of In1 ec \<Rightarrow>  
   248   (case ec of Inl e \<Rightarrow> (\<exists>v. w = In1 v) | Inr c \<Rightarrow> w = \<diamondsuit>)  
   249   | In2 e \<Rightarrow> (\<exists>v. w = In2 v) | In3 e \<Rightarrow> (\<exists>v. w = In3 v)"
   250 apply (erule evaln_cases , auto)
   251 apply (induct_tac "t")
   252 apply   (induct_tac "a")
   253 apply auto
   254 done
   255 
   256 text {* The following simplification procedures set up the proper injections of
   257  terms and their corresponding values in the evaluation relation:
   258  E.g. an expression 
   259  (injection @{term In1l} into terms) always evaluates to ordinary values 
   260  (injection @{term In1} into generalised values @{term vals}). 
   261 *}
   262 
   263 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')"
   264   by (auto, frule evaln_Inj_elim, auto)
   265 
   266 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')"
   267   by (auto, frule evaln_Inj_elim, auto)
   268 
   269 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')"
   270   by (auto, frule evaln_Inj_elim, auto)
   271 
   272 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')"
   273   by (auto, frule evaln_Inj_elim, auto, frule evaln_Inj_elim, auto)
   274 
   275 ML_setup {*
   276 fun enf name lhs =
   277 let
   278   fun is_Inj (Const (inj,_) $ _) = true
   279     | is_Inj _                   = false
   280   fun pred (_ $ _ $ _ $ _ $ _ $ x $ _) = is_Inj x
   281 in
   282   cond_simproc name lhs pred (thm name)
   283 end;
   284 
   285 val evaln_expr_proc  = enf "evaln_expr_eq"  "G\<turnstile>s \<midarrow>In1l t\<succ>\<midarrow>n\<rightarrow> (w, s')";
   286 val evaln_var_proc   = enf "evaln_var_eq"   "G\<turnstile>s \<midarrow>In2 t\<succ>\<midarrow>n\<rightarrow> (w, s')";
   287 val evaln_exprs_proc = enf "evaln_exprs_eq" "G\<turnstile>s \<midarrow>In3 t\<succ>\<midarrow>n\<rightarrow> (w, s')";
   288 val evaln_stmt_proc  = enf "evaln_stmt_eq"  "G\<turnstile>s \<midarrow>In1r t\<succ>\<midarrow>n\<rightarrow> (w, s')";
   289 Addsimprocs [evaln_expr_proc,evaln_var_proc,evaln_exprs_proc,evaln_stmt_proc];
   290 
   291 bind_thms ("evaln_AbruptIs", sum3_instantiate (thm "evaln.Abrupt"))
   292 *}
   293 declare evaln_AbruptIs [intro!]
   294 
   295 lemma evaln_Callee: "G\<turnstile>Norm s\<midarrow>In1l (Callee l e)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
   296 proof -
   297   { fix s t v s'
   298     assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
   299          normal: "normal s" and
   300          callee: "t=In1l (Callee l e)"
   301     then have "False" by induct auto
   302   }
   303   then show ?thesis
   304     by (cases s') fastsimp 
   305 qed
   306 
   307 lemma evaln_InsInitE: "G\<turnstile>Norm s\<midarrow>In1l (InsInitE c e)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
   308 proof -
   309   { fix s t v s'
   310     assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
   311          normal: "normal s" and
   312          callee: "t=In1l (InsInitE c e)"
   313     then have "False" by induct auto
   314   }
   315   then show ?thesis
   316     by (cases s') fastsimp
   317 qed
   318 
   319 lemma evaln_InsInitV: "G\<turnstile>Norm s\<midarrow>In2 (InsInitV c w)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
   320 proof -
   321   { fix s t v s'
   322     assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
   323          normal: "normal s" and
   324          callee: "t=In2 (InsInitV c w)"
   325     then have "False" by induct auto
   326   }  
   327   then show ?thesis
   328     by (cases s') fastsimp
   329 qed
   330 
   331 lemma evaln_FinA: "G\<turnstile>Norm s\<midarrow>In1r (FinA a c)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
   332 proof -
   333   { fix s t v s'
   334     assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
   335          normal: "normal s" and
   336          callee: "t=In1r (FinA a c)"
   337     then have "False" by induct auto
   338   } 
   339   then show ?thesis
   340     by (cases s') fastsimp
   341 qed
   342 
   343 lemma evaln_abrupt_lemma: "G\<turnstile>s \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (v,s') \<Longrightarrow> 
   344  fst s = Some xc \<longrightarrow> s' = s \<and> v = arbitrary3 e"
   345 apply (erule evaln_cases , auto)
   346 done
   347 
   348 lemma evaln_abrupt: 
   349  "\<And>s'. G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (w,s') = (s' = (Some xc,s) \<and>  
   350   w=arbitrary3 e \<and> G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (arbitrary3 e,(Some xc,s)))"
   351 apply auto
   352 apply (frule evaln_abrupt_lemma, auto)+
   353 done
   354 
   355 ML {*
   356 local
   357   fun is_Some (Const ("Pair",_) $ (Const ("Datatype.option.Some",_) $ _)$ _) =true
   358     | is_Some _ = false
   359   fun pred (_ $ _ $ _ $ _ $ _ $ _ $ x) = is_Some x
   360 in
   361   val evaln_abrupt_proc = 
   362  cond_simproc "evaln_abrupt" "G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (w,s')" pred (thm "evaln_abrupt")
   363 end;
   364 Addsimprocs [evaln_abrupt_proc]
   365 *}
   366 
   367 lemma evaln_LitI: "G\<turnstile>s \<midarrow>Lit v-\<succ>(if normal s then v else arbitrary)\<midarrow>n\<rightarrow> s"
   368 apply (case_tac "s", case_tac "a = None")
   369 by (auto intro!: evaln.Lit)
   370 
   371 lemma CondI: 
   372  "\<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> 
   373   G\<turnstile>s \<midarrow>e ? e1 : e2-\<succ>(if normal s1 then v else arbitrary)\<midarrow>n\<rightarrow> s2"
   374 apply (case_tac "s", case_tac "a = None")
   375 by (auto intro!: evaln.Cond)
   376 
   377 lemma evaln_SkipI [intro!]: "G\<turnstile>s \<midarrow>Skip\<midarrow>n\<rightarrow> s"
   378 apply (case_tac "s", case_tac "a = None")
   379 by (auto intro!: evaln.Skip)
   380 
   381 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'"
   382 apply (case_tac "s", case_tac "a = None")
   383 by (auto intro!: evaln.Expr)
   384 
   385 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"
   386 apply (case_tac "s", case_tac "a = None")
   387 by (auto intro!: evaln.Comp)
   388 
   389 lemma evaln_IfI: 
   390  "\<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> 
   391   G\<turnstile>s \<midarrow>If(e) c1 Else c2\<midarrow>n\<rightarrow> s2"
   392 apply (case_tac "s", case_tac "a = None")
   393 by (auto intro!: evaln.If)
   394 
   395 lemma evaln_SkipD [dest!]: "G\<turnstile>s \<midarrow>Skip\<midarrow>n\<rightarrow> s' \<Longrightarrow> s' = s" 
   396 by (erule evaln_cases, auto)
   397 
   398 lemma evaln_Skip_eq [simp]: "G\<turnstile>s \<midarrow>Skip\<midarrow>n\<rightarrow> s' = (s = s')"
   399 apply auto
   400 done
   401 
   402 
   403 
   404 
   405 section {* evaln implies eval *}
   406 
   407 lemma evaln_eval:  
   408   assumes evaln: "G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)" 
   409   shows "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"
   410 using evaln 
   411 proof (induct)
   412   case (Loop s0 e n b s1 c s2 l s3)
   413   have "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1".
   414   moreover
   415   have "if the_Bool b
   416         then (G\<turnstile>s1 \<midarrow>c\<rightarrow> s2) \<and> 
   417              G\<turnstile>abupd (absorb (Cont l)) s2 \<midarrow>l\<bullet> While(e) c\<rightarrow> s3
   418         else s3 = s1"
   419     using Loop.hyps by simp
   420   ultimately show ?case by (rule eval.Loop)
   421 next
   422   case (Try s0 c1 n s1 s2 C vn c2 s3)
   423   have "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1".
   424   moreover
   425   have "G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2".
   426   moreover
   427   have "if G,s2\<turnstile>catch C then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<rightarrow> s3 else s3 = s2"
   428     using Try.hyps by simp
   429   ultimately show ?case by (rule eval.Try)
   430 next
   431   case (Init C c s0 s3 n s1 s2)
   432   have "the (class G C) = c".
   433   moreover
   434   have "if inited C (globs s0) 
   435            then s3 = Norm s0
   436            else G\<turnstile>Norm ((init_class_obj G C) s0) 
   437                   \<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1 \<and>
   438                 G\<turnstile>(set_lvars empty) s1 \<midarrow>init c\<rightarrow> s2 \<and>
   439                 s3 = (set_lvars (locals (store s1))) s2"
   440     using Init.hyps by simp
   441   ultimately show ?case by (rule eval.Init)
   442 qed (rule eval.intros,(assumption+ | assumption?))+
   443 
   444 lemma Suc_le_D_lemma: "\<lbrakk>Suc n <= m'; (\<And>m. n <= m \<Longrightarrow> P (Suc m)) \<rbrakk> \<Longrightarrow> P m'"
   445 apply (frule Suc_le_D)
   446 apply fast
   447 done
   448 
   449 lemma evaln_nonstrict [rule_format (no_asm), elim]: 
   450   "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')"
   451 apply (erule evaln.induct)
   452 apply (tactic {* ALLGOALS (EVERY'[strip_tac, TRY o etac (thm "Suc_le_D_lemma"),
   453   REPEAT o smp_tac 1, 
   454   resolve_tac (thms "evaln.intros") THEN_ALL_NEW TRY o atac]) *})
   455 (* 3 subgoals *)
   456 apply (auto split del: split_if)
   457 done
   458 
   459 lemmas evaln_nonstrict_Suc = evaln_nonstrict [OF _ le_refl [THEN le_SucI]]
   460 
   461 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> 
   462              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')"
   463 by (fast intro: le_maxI1 le_maxI2)
   464 
   465 corollary evaln_max2E [consumes 2]:
   466   "\<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>n1\<rightarrow> (w1, s1'); G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>n2\<rightarrow> (w2, s2'); 
   467     \<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"
   468 by (drule (1) evaln_max2) simp
   469 
   470 
   471 lemma evaln_max3: 
   472 "\<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>
   473  G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> (w1, s1') \<and>
   474  G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> (w2, s2') \<and> 
   475  G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> (w3, s3')"
   476 apply (drule (1) evaln_max2, erule thin_rl)
   477 apply (fast intro!: le_maxI1 le_maxI2)
   478 done
   479 
   480 corollary evaln_max3E: 
   481 "\<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');
   482    \<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> (w1, s1');
   483     G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> (w2, s2'); 
   484     G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> (w3, s3')
   485    \<rbrakk> \<Longrightarrow> P
   486   \<rbrakk> \<Longrightarrow> P"
   487 by (drule (2) evaln_max3) simp
   488 
   489 
   490 lemma le_max3I1: "(n2::nat) \<le> max n1 (max n2 n3)"
   491 proof -
   492   have "n2 \<le> max n2 n3"
   493     by (rule le_maxI1)
   494   also
   495   have "max n2 n3 \<le> max n1 (max n2 n3)"
   496     by (rule le_maxI2)
   497   finally
   498   show ?thesis .
   499 qed
   500 
   501 lemma le_max3I2: "(n3::nat) \<le> max n1 (max n2 n3)"
   502 proof -
   503   have "n3 \<le> max n2 n3"
   504     by (rule le_maxI2)
   505   also
   506   have "max n2 n3 \<le> max n1 (max n2 n3)"
   507     by (rule le_maxI2)
   508   finally
   509   show ?thesis .
   510 qed
   511 
   512 ML {*
   513 Delsimprocs [wt_expr_proc,wt_var_proc,wt_exprs_proc,wt_stmt_proc]
   514 *}
   515 
   516 section {* eval implies evaln *}
   517 lemma eval_evaln: 
   518   assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"
   519   shows  "\<exists>n. G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)"
   520 using eval 
   521 proof (induct)
   522   case (Abrupt xc s t)
   523   obtain n where
   524     "G\<turnstile>(Some xc, s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (arbitrary3 t, (Some xc, s))"
   525     by (iprover intro: evaln.Abrupt)
   526   then show ?case ..
   527 next
   528   case Skip
   529   show ?case by (blast intro: evaln.Skip)
   530 next
   531   case (Expr s0 e v s1)
   532   then obtain n where
   533     "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
   534     by (iprover)
   535   then have "G\<turnstile>Norm s0 \<midarrow>Expr e\<midarrow>n\<rightarrow> s1"
   536     by (rule evaln.Expr) 
   537   then show ?case ..
   538 next
   539   case (Lab s0 c s1 l)
   540   then obtain n where
   541     "G\<turnstile>Norm s0 \<midarrow>c\<midarrow>n\<rightarrow> s1"
   542     by (iprover)
   543   then have "G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<midarrow>n\<rightarrow> abupd (absorb l) s1"
   544     by (rule evaln.Lab)
   545   then show ?case ..
   546 next
   547   case (Comp s0 c1 s1 c2 s2)
   548   then obtain n1 n2 where
   549     "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> s1"
   550     "G\<turnstile>s1 \<midarrow>c2\<midarrow>n2\<rightarrow> s2"
   551     by (iprover)
   552   then have "G\<turnstile>Norm s0 \<midarrow>c1;; c2\<midarrow>max n1 n2\<rightarrow> s2"
   553     by (blast intro: evaln.Comp dest: evaln_max2 )
   554   then show ?case ..
   555 next
   556   case (If s0 e b s1 c1 c2 s2)
   557   then obtain n1 n2 where
   558     "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n1\<rightarrow> s1"
   559     "G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<midarrow>n2\<rightarrow> s2"
   560     by (iprover)
   561   then have "G\<turnstile>Norm s0 \<midarrow>If(e) c1 Else c2\<midarrow>max n1 n2\<rightarrow> s2"
   562     by (blast intro: evaln.If dest: evaln_max2)
   563   then show ?case ..
   564 next
   565   case (Loop s0 e b s1 c s2 l s3)
   566   from Loop.hyps obtain n1 where
   567     "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n1\<rightarrow> s1"
   568     by (iprover)
   569   moreover from Loop.hyps obtain n2 where
   570     "if the_Bool b 
   571         then (G\<turnstile>s1 \<midarrow>c\<midarrow>n2\<rightarrow> s2 \<and> 
   572               G\<turnstile>(abupd (absorb (Cont l)) s2)\<midarrow>l\<bullet> While(e) c\<midarrow>n2\<rightarrow> s3)
   573 	else s3 = s1"
   574     by simp (iprover intro: evaln_nonstrict le_maxI1 le_maxI2)
   575   ultimately
   576   have "G\<turnstile>Norm s0 \<midarrow>l\<bullet> While(e) c\<midarrow>max n1 n2\<rightarrow> s3"
   577     apply -
   578     apply (rule evaln.Loop)
   579     apply   (iprover intro: evaln_nonstrict intro: le_maxI1)
   580 
   581     apply   (auto intro: evaln_nonstrict intro: le_maxI2)
   582     done
   583   then show ?case ..
   584 next
   585   case (Jmp s j)
   586   have "G\<turnstile>Norm s \<midarrow>Jmp j\<midarrow>n\<rightarrow> (Some (Jump j), s)"
   587     by (rule evaln.Jmp)
   588   then show ?case ..
   589 next
   590   case (Throw s0 e a s1)
   591   then obtain n where
   592     "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<midarrow>n\<rightarrow> s1"
   593     by (iprover)
   594   then have "G\<turnstile>Norm s0 \<midarrow>Throw e\<midarrow>n\<rightarrow> abupd (throw a) s1"
   595     by (rule evaln.Throw)
   596   then show ?case ..
   597 next 
   598   case (Try s0 c1 s1 s2 catchC vn c2 s3)
   599   from Try.hyps obtain n1 where
   600     "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> s1"
   601     by (iprover)
   602   moreover 
   603   have sxalloc: "G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2" .
   604   moreover
   605   from Try.hyps obtain n2 where
   606     "if G,s2\<turnstile>catch catchC then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<midarrow>n2\<rightarrow> s3 else s3 = s2"
   607     by fastsimp 
   608   ultimately
   609   have "G\<turnstile>Norm s0 \<midarrow>Try c1 Catch(catchC vn) c2\<midarrow>max n1 n2\<rightarrow> s3"
   610     by (auto intro!: evaln.Try le_maxI1 le_maxI2)
   611   then show ?case ..
   612 next
   613   case (Fin s0 c1 x1 s1 c2 s2 s3)
   614   from Fin obtain n1 n2 where 
   615     "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> (x1, s1)"
   616     "G\<turnstile>Norm s1 \<midarrow>c2\<midarrow>n2\<rightarrow> s2"
   617     by iprover
   618   moreover
   619   have s3: "s3 = (if \<exists>err. x1 = Some (Error err) 
   620                      then (x1, s1)
   621                      else abupd (abrupt_if (x1 \<noteq> None) x1) s2)" .
   622   ultimately 
   623   have 
   624     "G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<midarrow>max n1 n2\<rightarrow> s3"
   625     by (blast intro: evaln.Fin dest: evaln_max2)
   626   then show ?case ..
   627 next
   628   case (Init C c s0 s3 s1 s2)
   629   have     cls: "the (class G C) = c" .
   630   moreover from Init.hyps obtain n where
   631       "if inited C (globs s0) then s3 = Norm s0
   632        else (G\<turnstile>Norm (init_class_obj G C s0)
   633 	      \<midarrow>(if C = Object then Skip else Init (super c))\<midarrow>n\<rightarrow> s1 \<and>
   634 	           G\<turnstile>set_lvars empty s1 \<midarrow>init c\<midarrow>n\<rightarrow> s2 \<and> 
   635                    s3 = restore_lvars s1 s2)"
   636     by (auto intro: evaln_nonstrict le_maxI1 le_maxI2)
   637   ultimately have "G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s3"
   638     by (rule evaln.Init)
   639   then show ?case ..
   640 next
   641   case (NewC s0 C s1 a s2)
   642   then obtain n where 
   643     "G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s1"
   644     by (iprover)
   645   with NewC 
   646   have "G\<turnstile>Norm s0 \<midarrow>NewC C-\<succ>Addr a\<midarrow>n\<rightarrow> s2"
   647     by (iprover intro: evaln.NewC)
   648   then show ?case ..
   649 next
   650   case (NewA s0 T s1 e i s2 a s3)
   651   then obtain n1 n2 where 
   652     "G\<turnstile>Norm s0 \<midarrow>init_comp_ty T\<midarrow>n1\<rightarrow> s1"
   653     "G\<turnstile>s1 \<midarrow>e-\<succ>i\<midarrow>n2\<rightarrow> s2"      
   654     by (iprover)
   655   moreover
   656   have "G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3" .
   657   ultimately
   658   have "G\<turnstile>Norm s0 \<midarrow>New T[e]-\<succ>Addr a\<midarrow>max n1 n2\<rightarrow> s3"
   659     by (blast intro: evaln.NewA dest: evaln_max2)
   660   then show ?case ..
   661 next
   662   case (Cast s0 e v s1 s2 castT)
   663   then obtain n where
   664     "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
   665     by (iprover)
   666   moreover 
   667   have "s2 = abupd (raise_if (\<not> G,snd s1\<turnstile>v fits castT) ClassCast) s1" .
   668   ultimately
   669   have "G\<turnstile>Norm s0 \<midarrow>Cast castT e-\<succ>v\<midarrow>n\<rightarrow> s2"
   670     by (rule evaln.Cast)
   671   then show ?case ..
   672 next
   673   case (Inst s0 e v s1 b T)
   674   then obtain n where
   675     "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
   676     by (iprover)
   677   moreover 
   678   have "b = (v \<noteq> Null \<and> G,snd s1\<turnstile>v fits RefT T)" .
   679   ultimately
   680   have "G\<turnstile>Norm s0 \<midarrow>e InstOf T-\<succ>Bool b\<midarrow>n\<rightarrow> s1"
   681     by (rule evaln.Inst)
   682   then show ?case ..
   683 next
   684   case (Lit s v)
   685   have "G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<midarrow>n\<rightarrow> Norm s"
   686     by (rule evaln.Lit)
   687   then show ?case ..
   688 next
   689   case (UnOp s0 e v s1 unop)
   690   then obtain n where
   691     "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
   692     by (iprover)
   693   hence "G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>eval_unop unop v\<midarrow>n\<rightarrow> s1"
   694     by (rule evaln.UnOp)
   695   then show ?case ..
   696 next
   697   case (BinOp s0 e1 v1 s1 binop e2 v2 s2)
   698   then obtain n1 n2 where 
   699     "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<midarrow>n1\<rightarrow> s1"
   700     "G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then In1l e2
   701                else In1r Skip)\<succ>\<midarrow>n2\<rightarrow> (In1 v2, s2)"    
   702     by (iprover)
   703   hence "G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<midarrow>max n1 n2
   704           \<rightarrow> s2"
   705     by (blast intro!: evaln.BinOp dest: evaln_max2)
   706   then show ?case ..
   707 next
   708   case (Super s )
   709   have "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<midarrow>n\<rightarrow> Norm s"
   710     by (rule evaln.Super)
   711   then show ?case ..
   712 next
   713   case (Acc s0 va v f s1)
   714   then obtain n where
   715     "G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v, f)\<midarrow>n\<rightarrow> s1"
   716     by (iprover)
   717   then
   718   have "G\<turnstile>Norm s0 \<midarrow>Acc va-\<succ>v\<midarrow>n\<rightarrow> s1"
   719     by (rule evaln.Acc)
   720   then show ?case ..
   721 next
   722   case (Ass s0 var w f s1 e v s2)
   723   then obtain n1 n2 where 
   724     "G\<turnstile>Norm s0 \<midarrow>var=\<succ>(w, f)\<midarrow>n1\<rightarrow> s1"
   725     "G\<turnstile>s1 \<midarrow>e-\<succ>v\<midarrow>n2\<rightarrow> s2"      
   726     by (iprover)
   727   then
   728   have "G\<turnstile>Norm s0 \<midarrow>var:=e-\<succ>v\<midarrow>max n1 n2\<rightarrow> assign f v s2"
   729     by (blast intro: evaln.Ass dest: evaln_max2)
   730   then show ?case ..
   731 next
   732   case (Cond s0 e0 b s1 e1 e2 v s2)
   733   then obtain n1 n2 where 
   734     "G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<midarrow>n1\<rightarrow> s1"
   735     "G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<midarrow>n2\<rightarrow> s2"
   736     by (iprover)
   737   then
   738   have "G\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<midarrow>max n1 n2\<rightarrow> s2"
   739     by (blast intro: evaln.Cond dest: evaln_max2)
   740   then show ?case ..
   741 next
   742   case (Call s0 e a' s1 args vs s2 invDeclC mode statT mn pTs' s3 s3' accC' v s4)
   743   then obtain n1 n2 where
   744     "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n1\<rightarrow> s1"
   745     "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<midarrow>n2\<rightarrow> s2"
   746     by iprover
   747   moreover
   748   have "invDeclC = invocation_declclass G mode (store s2) a' statT 
   749                        \<lparr>name=mn,parTs=pTs'\<rparr>" .
   750   moreover
   751   have "s3 = init_lvars G invDeclC \<lparr>name=mn,parTs=pTs'\<rparr> mode a' vs s2" .
   752   moreover
   753   have "s3'=check_method_access G accC' statT mode \<lparr>name=mn,parTs=pTs'\<rparr> a' s3".
   754   moreover 
   755   from Call.hyps
   756   obtain m where 
   757     "G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name=mn, parTs=pTs'\<rparr>-\<succ>v\<midarrow>m\<rightarrow> s4"
   758     by iprover
   759   ultimately
   760   have "G\<turnstile>Norm s0 \<midarrow>{accC',statT,mode}e\<cdot>mn( {pTs'}args)-\<succ>v\<midarrow>max n1 (max n2 m)\<rightarrow> 
   761             (set_lvars (locals (store s2))) s4"
   762     by (auto intro!: evaln.Call le_maxI1 le_max3I1 le_max3I2)
   763   thus ?case ..
   764 next
   765   case (Methd s0 D sig v s1)
   766   then obtain n where
   767     "G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<midarrow>n\<rightarrow> s1"
   768     by iprover
   769   then have "G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<midarrow>Suc n\<rightarrow> s1"
   770     by (rule evaln.Methd)
   771   then show ?case ..
   772 next
   773   case (Body s0 D s1 c s2 s3)
   774   from Body.hyps obtain n1 n2 where 
   775     evaln_init: "G\<turnstile>Norm s0 \<midarrow>Init D\<midarrow>n1\<rightarrow> s1" and
   776     evaln_c: "G\<turnstile>s1 \<midarrow>c\<midarrow>n2\<rightarrow> s2"
   777     by (iprover)
   778   moreover
   779   have "s3 = (if \<exists>l. fst s2 = Some (Jump (Break l)) \<or> 
   780                      fst s2 = Some (Jump (Cont l))
   781                  then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2 
   782                  else s2)".
   783   ultimately
   784   have
   785      "G\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>the (locals (store s2) Result)\<midarrow>max n1 n2
   786        \<rightarrow> abupd (absorb Ret) s3"
   787     by (iprover intro: evaln.Body dest: evaln_max2)
   788   then show ?case ..
   789 next
   790   case (LVar s vn )
   791   obtain n where
   792     "G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<midarrow>n\<rightarrow> Norm s"
   793     by (iprover intro: evaln.LVar)
   794   then show ?case ..
   795 next
   796   case (FVar s0 statDeclC s1 e a s2 v s2' stat fn s3 accC)
   797   then obtain n1 n2 where
   798     "G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<midarrow>n1\<rightarrow> s1"
   799     "G\<turnstile>s1 \<midarrow>e-\<succ>a\<midarrow>n2\<rightarrow> s2"
   800     by iprover
   801   moreover
   802   have "s3 = check_field_access G accC statDeclC fn stat a s2'" 
   803        "(v, s2') = fvar statDeclC stat fn a s2" .
   804   ultimately
   805   have "G\<turnstile>Norm s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>v\<midarrow>max n1 n2\<rightarrow> s3"
   806     by (iprover intro: evaln.FVar dest: evaln_max2)
   807   then show ?case ..
   808 next
   809   case (AVar s0 e1 a s1 e2 i s2 v s2')
   810   then obtain n1 n2 where 
   811     "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>a\<midarrow>n1\<rightarrow> s1"
   812     "G\<turnstile>s1 \<midarrow>e2-\<succ>i\<midarrow>n2\<rightarrow> s2"      
   813     by iprover
   814   moreover 
   815   have "(v, s2') = avar G i a s2" .
   816   ultimately 
   817   have "G\<turnstile>Norm s0 \<midarrow>e1.[e2]=\<succ>v\<midarrow>max n1 n2\<rightarrow> s2'"
   818     by (blast intro!: evaln.AVar dest: evaln_max2)
   819   then show ?case ..
   820 next
   821   case (Nil s0)
   822   show ?case by (iprover intro: evaln.Nil)
   823 next
   824   case (Cons s0 e v s1 es vs s2)
   825   then obtain n1 n2 where 
   826     "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n1\<rightarrow> s1"
   827     "G\<turnstile>s1 \<midarrow>es\<doteq>\<succ>vs\<midarrow>n2\<rightarrow> s2"      
   828     by iprover
   829   then
   830   have "G\<turnstile>Norm s0 \<midarrow>e # es\<doteq>\<succ>v # vs\<midarrow>max n1 n2\<rightarrow> s2"
   831     by (blast intro!: evaln.Cons dest: evaln_max2)
   832   then show ?case ..
   833 qed
   834        
   835 end