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