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