src/HOL/Bali/Evaln.thy
changeset 21765 89275a3ed7be
parent 18249 4398f0f12579
child 22218 30a8890d2967
     1.1 --- a/src/HOL/Bali/Evaln.thy	Mon Dec 11 12:28:16 2006 +0100
     1.2 +++ b/src/HOL/Bali/Evaln.thy	Mon Dec 11 16:06:14 2006 +0100
     1.3 @@ -28,68 +28,40 @@
     1.4  for welltyped, and definitely assigned terms.
     1.5  *}
     1.6  
     1.7 -consts
     1.8 -
     1.9 -  evaln	:: "prog \<Rightarrow> (state \<times> term \<times> nat \<times> vals \<times> state) set"
    1.10 -
    1.11 -syntax
    1.12 -
    1.13 -  evaln	:: "[prog, state, term,        nat, vals * state] => bool"
    1.14 -				("_|-_ -_>-_-> _"   [61,61,80,   61,61] 60)
    1.15 -  evarn	:: "[prog, state, var  , vvar        , nat, state] => bool"
    1.16 -				("_|-_ -_=>_-_-> _" [61,61,90,61,61,61] 60)
    1.17 -  eval_n:: "[prog, state, expr , val         , nat, state] => bool"
    1.18 -				("_|-_ -_->_-_-> _" [61,61,80,61,61,61] 60)
    1.19 -  evalsn:: "[prog, state, expr list, val list, nat, state] => bool"
    1.20 -				("_|-_ -_#>_-_-> _" [61,61,61,61,61,61] 60)
    1.21 -  execn	:: "[prog, state, stmt ,               nat, state] => bool"
    1.22 -				("_|-_ -_-_-> _"    [61,61,65,   61,61] 60)
    1.23 -
    1.24 -syntax (xsymbols)
    1.25 +inductive2
    1.26 +  evaln	:: "[prog, state, term, nat, vals, state] \<Rightarrow> bool"
    1.27 +    ("_\<turnstile>_ \<midarrow>_\<succ>\<midarrow>_\<rightarrow> '(_, _')" [61,61,80,61,0,0] 60)
    1.28 +  and evarn :: "[prog, state, var, vvar, nat, state] \<Rightarrow> bool"
    1.29 +    ("_\<turnstile>_ \<midarrow>_=\<succ>_\<midarrow>_\<rightarrow> _" [61,61,90,61,61,61] 60)
    1.30 +  and eval_n:: "[prog, state, expr, val, nat, state] \<Rightarrow> bool"
    1.31 +    ("_\<turnstile>_ \<midarrow>_-\<succ>_\<midarrow>_\<rightarrow> _" [61,61,80,61,61,61] 60)
    1.32 +  and evalsn :: "[prog, state, expr list, val  list, nat, state] \<Rightarrow> bool"
    1.33 +    ("_\<turnstile>_ \<midarrow>_\<doteq>\<succ>_\<midarrow>_\<rightarrow> _" [61,61,61,61,61,61] 60)
    1.34 +  and execn	:: "[prog, state, stmt, nat, state] \<Rightarrow> bool"
    1.35 +    ("_\<turnstile>_ \<midarrow>_\<midarrow>_\<rightarrow> _"     [61,61,65,   61,61] 60)
    1.36 +  for G :: prog
    1.37 +where
    1.38  
    1.39 -  evaln	:: "[prog, state, term,         nat, vals \<times> state] \<Rightarrow> bool"
    1.40 -				("_\<turnstile>_ \<midarrow>_\<succ>\<midarrow>_\<rightarrow> _"   [61,61,80,   61,61] 60)
    1.41 -  evarn	:: "[prog, state, var  , vvar         , nat, state] \<Rightarrow> bool"
    1.42 -				("_\<turnstile>_ \<midarrow>_=\<succ>_\<midarrow>_\<rightarrow> _" [61,61,90,61,61,61] 60)
    1.43 -  eval_n:: "[prog, state, expr , val ,          nat, state] \<Rightarrow> bool"
    1.44 -				("_\<turnstile>_ \<midarrow>_-\<succ>_\<midarrow>_\<rightarrow> _" [61,61,80,61,61,61] 60)
    1.45 -  evalsn:: "[prog, state, expr list, val  list, nat, state] \<Rightarrow> bool"
    1.46 -				("_\<turnstile>_ \<midarrow>_\<doteq>\<succ>_\<midarrow>_\<rightarrow> _" [61,61,61,61,61,61] 60)
    1.47 -  execn	:: "[prog, state, stmt ,                nat, state] \<Rightarrow> bool"
    1.48 -				("_\<turnstile>_ \<midarrow>_\<midarrow>_\<rightarrow> _"     [61,61,65,   61,61] 60)
    1.49 -
    1.50 -translations
    1.51 -
    1.52 -  "G\<turnstile>s \<midarrow>t    \<succ>\<midarrow>n\<rightarrow>  w___s' " == "(s,t,n,w___s') \<in> evaln G"
    1.53 -  "G\<turnstile>s \<midarrow>t    \<succ>\<midarrow>n\<rightarrow> (w,  s')" <= "(s,t,n,w,  s') \<in> evaln G"
    1.54 -  "G\<turnstile>s \<midarrow>t    \<succ>\<midarrow>n\<rightarrow> (w,x,s')" <= "(s,t,n,w,x,s') \<in> evaln G"
    1.55 -  "G\<turnstile>s \<midarrow>c     \<midarrow>n\<rightarrow> (x,s')" <= "G\<turnstile>s \<midarrow>In1r  c\<succ>\<midarrow>n\<rightarrow> (\<diamondsuit>    ,x,s')"
    1.56 -  "G\<turnstile>s \<midarrow>c     \<midarrow>n\<rightarrow>    s' " == "G\<turnstile>s \<midarrow>In1r  c\<succ>\<midarrow>n\<rightarrow> (\<diamondsuit>    ,  s')"
    1.57 -  "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')"
    1.58 -  "G\<turnstile>s \<midarrow>e-\<succ>v  \<midarrow>n\<rightarrow>    s' " == "G\<turnstile>s \<midarrow>In1l e\<succ>\<midarrow>n\<rightarrow> (In1 v ,  s')"
    1.59 -  "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')"
    1.60 -  "G\<turnstile>s \<midarrow>e=\<succ>vf \<midarrow>n\<rightarrow>    s' " == "G\<turnstile>s \<midarrow>In2  e\<succ>\<midarrow>n\<rightarrow> (In2 vf,  s')"
    1.61 -  "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')"
    1.62 -  "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')"
    1.63 -
    1.64 -
    1.65 -inductive "evaln G" intros
    1.66 +  "G\<turnstile>s \<midarrow>c     \<midarrow>n\<rightarrow>    s' \<equiv> G\<turnstile>s \<midarrow>In1r  c\<succ>\<midarrow>n\<rightarrow> (\<diamondsuit>    ,  s')"
    1.67 +| "G\<turnstile>s \<midarrow>e-\<succ>v  \<midarrow>n\<rightarrow>    s' \<equiv> G\<turnstile>s \<midarrow>In1l e\<succ>\<midarrow>n\<rightarrow> (In1 v ,  s')"
    1.68 +| "G\<turnstile>s \<midarrow>e=\<succ>vf \<midarrow>n\<rightarrow>    s' \<equiv> G\<turnstile>s \<midarrow>In2  e\<succ>\<midarrow>n\<rightarrow> (In2 vf,  s')"
    1.69 +| "G\<turnstile>s \<midarrow>e\<doteq>\<succ>v  \<midarrow>n\<rightarrow>    s' \<equiv> G\<turnstile>s \<midarrow>In3  e\<succ>\<midarrow>n\<rightarrow> (In3 v ,  s')"
    1.70  
    1.71  --{* propagation of abrupt completion *}
    1.72  
    1.73 -  Abrupt:   "G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (arbitrary3 t,(Some xc,s))"
    1.74 +| Abrupt:   "G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (arbitrary3 t,(Some xc,s))"
    1.75  
    1.76  
    1.77  --{* evaluation of variables *}
    1.78  
    1.79 -  LVar:	"G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<midarrow>n\<rightarrow> Norm s"
    1.80 +| LVar:	"G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<midarrow>n\<rightarrow> Norm s"
    1.81  
    1.82 -  FVar:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e-\<succ>a\<midarrow>n\<rightarrow> s2;
    1.83 +| FVar:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e-\<succ>a\<midarrow>n\<rightarrow> s2;
    1.84  	  (v,s2') = fvar statDeclC stat fn a s2;
    1.85            s3 = check_field_access G accC statDeclC fn stat a s2'\<rbrakk> \<Longrightarrow>
    1.86  	  G\<turnstile>Norm s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>v\<midarrow>n\<rightarrow> s3"
    1.87  
    1.88 -  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; 
    1.89 +| 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; 
    1.90  	  (v,s2') = avar G i a s2\<rbrakk> \<Longrightarrow>
    1.91  	              G\<turnstile>Norm s0 \<midarrow>e1.[e2]=\<succ>v\<midarrow>n\<rightarrow> s2'"
    1.92  
    1.93 @@ -98,46 +70,46 @@
    1.94  
    1.95  --{* evaluation of expressions *}
    1.96  
    1.97 -  NewC:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s1;
    1.98 +| NewC:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s1;
    1.99  	  G\<turnstile>     s1 \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   1.100  	                          G\<turnstile>Norm s0 \<midarrow>NewC C-\<succ>Addr a\<midarrow>n\<rightarrow> s2"
   1.101  
   1.102 -  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; 
   1.103 +| 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; 
   1.104  	  G\<turnstile>abupd (check_neg i') s2 \<midarrow>halloc (Arr T (the_Intg i'))\<succ>a\<rightarrow> s3\<rbrakk> \<Longrightarrow>
   1.105  	                        G\<turnstile>Norm s0 \<midarrow>New T[e]-\<succ>Addr a\<midarrow>n\<rightarrow> s3"
   1.106  
   1.107 -  Cast:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1;
   1.108 +| Cast:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1;
   1.109  	  s2 = abupd (raise_if (\<not>G,snd s1\<turnstile>v fits T) ClassCast) s1\<rbrakk> \<Longrightarrow>
   1.110  			        G\<turnstile>Norm s0 \<midarrow>Cast T e-\<succ>v\<midarrow>n\<rightarrow> s2"
   1.111  
   1.112 -  Inst:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1;
   1.113 +| Inst:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1;
   1.114  	  b = (v\<noteq>Null \<and> G,store s1\<turnstile>v fits RefT T)\<rbrakk> \<Longrightarrow>
   1.115  			      G\<turnstile>Norm s0 \<midarrow>e InstOf T-\<succ>Bool b\<midarrow>n\<rightarrow> s1"
   1.116  
   1.117 -  Lit:			   "G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<midarrow>n\<rightarrow> Norm s"
   1.118 +| Lit:			   "G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<midarrow>n\<rightarrow> Norm s"
   1.119  
   1.120 -  UnOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1\<rbrakk> 
   1.121 +| UnOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1\<rbrakk> 
   1.122           \<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>(eval_unop unop v)\<midarrow>n\<rightarrow> s1"
   1.123  
   1.124 -  BinOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<midarrow>n\<rightarrow> s1; 
   1.125 +| BinOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<midarrow>n\<rightarrow> s1; 
   1.126             G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then (In1l e2) else (In1r Skip))
   1.127              \<succ>\<midarrow>n\<rightarrow> (In1 v2,s2)\<rbrakk> 
   1.128           \<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<midarrow>n\<rightarrow> s2"
   1.129  
   1.130 -  Super:		   "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<midarrow>n\<rightarrow> Norm s"
   1.131 +| Super:		   "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<midarrow>n\<rightarrow> Norm s"
   1.132  
   1.133 -  Acc:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v,f)\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   1.134 +| Acc:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v,f)\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   1.135  	                          G\<turnstile>Norm s0 \<midarrow>Acc va-\<succ>v\<midarrow>n\<rightarrow> s1"
   1.136  
   1.137 -  Ass:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(w,f)\<midarrow>n\<rightarrow> s1;
   1.138 +| Ass:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(w,f)\<midarrow>n\<rightarrow> s1;
   1.139            G\<turnstile>     s1 \<midarrow>e-\<succ>v     \<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   1.140  				   G\<turnstile>Norm s0 \<midarrow>va:=e-\<succ>v\<midarrow>n\<rightarrow> assign f v s2"
   1.141  
   1.142 -  Cond:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<midarrow>n\<rightarrow> s1;
   1.143 +| Cond:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<midarrow>n\<rightarrow> s1;
   1.144            G\<turnstile>     s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   1.145  			    G\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<midarrow>n\<rightarrow> s2"
   1.146  
   1.147 -  Call:	
   1.148 +| Call:	
   1.149    "\<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;
   1.150      D = invocation_declclass G mode (store s2) a' statT \<lparr>name=mn,parTs=pTs\<rparr>; 
   1.151      s3=init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' vs s2;
   1.152 @@ -147,10 +119,10 @@
   1.153     \<Longrightarrow> 
   1.154      G\<turnstile>Norm s0 \<midarrow>{accC,statT,mode}e\<cdot>mn({pTs}args)-\<succ>v\<midarrow>n\<rightarrow> (restore_lvars s2 s4)"
   1.155  
   1.156 -  Methd:"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   1.157 +| Methd:"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   1.158  				G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<midarrow>Suc n\<rightarrow> s1"
   1.159  
   1.160 -  Body:	"\<lbrakk>G\<turnstile>Norm s0\<midarrow>Init D\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c\<midarrow>n\<rightarrow> s2;
   1.161 +| Body:	"\<lbrakk>G\<turnstile>Norm s0\<midarrow>Init D\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c\<midarrow>n\<rightarrow> s2;
   1.162            s3 = (if (\<exists> l. abrupt s2 = Some (Jump (Break l)) \<or>  
   1.163                           abrupt s2 = Some (Jump (Cont l)))
   1.164                    then abupd (\<lambda> x. Some (Error CrossMethodJump)) s2 
   1.165 @@ -160,57 +132,57 @@
   1.166  
   1.167  --{* evaluation of expression lists *}
   1.168  
   1.169 -  Nil:
   1.170 +| Nil:
   1.171  				"G\<turnstile>Norm s0 \<midarrow>[]\<doteq>\<succ>[]\<midarrow>n\<rightarrow> Norm s0"
   1.172  
   1.173 -  Cons:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e -\<succ> v \<midarrow>n\<rightarrow> s1;
   1.174 +| Cons:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e -\<succ> v \<midarrow>n\<rightarrow> s1;
   1.175            G\<turnstile>     s1 \<midarrow>es\<doteq>\<succ>vs\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   1.176  			     G\<turnstile>Norm s0 \<midarrow>e#es\<doteq>\<succ>v#vs\<midarrow>n\<rightarrow> s2"
   1.177  
   1.178  
   1.179  --{* execution of statements *}
   1.180  
   1.181 -  Skip:	 			    "G\<turnstile>Norm s \<midarrow>Skip\<midarrow>n\<rightarrow> Norm s"
   1.182 +| Skip:	 			    "G\<turnstile>Norm s \<midarrow>Skip\<midarrow>n\<rightarrow> Norm s"
   1.183  
   1.184 -  Expr:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   1.185 +| Expr:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   1.186  				  G\<turnstile>Norm s0 \<midarrow>Expr e\<midarrow>n\<rightarrow> s1"
   1.187  
   1.188 -  Lab:  "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c \<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   1.189 +| Lab:  "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c \<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   1.190                               G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<midarrow>n\<rightarrow> abupd (absorb l) s1"
   1.191  
   1.192 -  Comp:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1 \<midarrow>n\<rightarrow> s1;
   1.193 +| Comp:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1 \<midarrow>n\<rightarrow> s1;
   1.194  	  G\<turnstile>     s1 \<midarrow>c2 \<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   1.195  				 G\<turnstile>Norm s0 \<midarrow>c1;; c2\<midarrow>n\<rightarrow> s2"
   1.196  
   1.197 -  If:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n\<rightarrow> s1;
   1.198 +| If:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n\<rightarrow> s1;
   1.199  	  G\<turnstile>     s1\<midarrow>(if the_Bool b then c1 else c2)\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   1.200  		       G\<turnstile>Norm s0 \<midarrow>If(e) c1 Else c2 \<midarrow>n\<rightarrow> s2"
   1.201  
   1.202 -  Loop:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n\<rightarrow> s1;
   1.203 +| Loop:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n\<rightarrow> s1;
   1.204  	  if the_Bool b 
   1.205               then (G\<turnstile>s1 \<midarrow>c\<midarrow>n\<rightarrow> s2 \<and> 
   1.206                     G\<turnstile>(abupd (absorb (Cont l)) s2) \<midarrow>l\<bullet> While(e) c\<midarrow>n\<rightarrow> s3)
   1.207  	     else s3 = s1\<rbrakk> \<Longrightarrow>
   1.208  			      G\<turnstile>Norm s0 \<midarrow>l\<bullet> While(e) c\<midarrow>n\<rightarrow> s3"
   1.209    
   1.210 -  Jmp: "G\<turnstile>Norm s \<midarrow>Jmp j\<midarrow>n\<rightarrow> (Some (Jump j), s)"
   1.211 +| Jmp: "G\<turnstile>Norm s \<midarrow>Jmp j\<midarrow>n\<rightarrow> (Some (Jump j), s)"
   1.212    
   1.213 -  Throw:"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   1.214 +| Throw:"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   1.215  				 G\<turnstile>Norm s0 \<midarrow>Throw e\<midarrow>n\<rightarrow> abupd (throw a') s1"
   1.216  
   1.217 -  Try:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2;
   1.218 +| Try:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2;
   1.219  	  if G,s2\<turnstile>catch tn then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<midarrow>n\<rightarrow> s3 else s3 = s2\<rbrakk>
   1.220            \<Longrightarrow>
   1.221  		  G\<turnstile>Norm s0 \<midarrow>Try c1 Catch(tn vn) c2\<midarrow>n\<rightarrow> s3"
   1.222  
   1.223 -  Fin:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n\<rightarrow> (x1,s1);
   1.224 +| Fin:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n\<rightarrow> (x1,s1);
   1.225  	  G\<turnstile>Norm s1 \<midarrow>c2\<midarrow>n\<rightarrow> s2;
   1.226            s3=(if (\<exists> err. x1=Some (Error err)) 
   1.227                then (x1,s1) 
   1.228                else abupd (abrupt_if (x1\<noteq>None) x1) s2)\<rbrakk> \<Longrightarrow>
   1.229                G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<midarrow>n\<rightarrow> s3"
   1.230    
   1.231 -  Init:	"\<lbrakk>the (class G C) = c;
   1.232 +| Init:	"\<lbrakk>the (class G C) = c;
   1.233  	  if inited C (globs s0) then s3 = Norm s0
   1.234  	  else (G\<turnstile>Norm (init_class_obj G C s0)
   1.235  	          \<midarrow>(if C = Object then Skip else Init (super c))\<midarrow>n\<rightarrow> s1 \<and>
   1.236 @@ -229,41 +201,41 @@
   1.237  ML_setup {*
   1.238  change_simpset (fn ss => ss delloop "split_all_tac");
   1.239  *}
   1.240 -inductive_cases evaln_cases: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> vs'"
   1.241 +inductive_cases2 evaln_cases: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v, s')"
   1.242  
   1.243 -inductive_cases evaln_elim_cases:
   1.244 -	"G\<turnstile>(Some xc, s) \<midarrow>t                        \<succ>\<midarrow>n\<rightarrow> vs'"
   1.245 -	"G\<turnstile>Norm s \<midarrow>In1r Skip                      \<succ>\<midarrow>n\<rightarrow> xs'"
   1.246 -        "G\<turnstile>Norm s \<midarrow>In1r (Jmp j)                   \<succ>\<midarrow>n\<rightarrow> xs'"
   1.247 -        "G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> c)                    \<succ>\<midarrow>n\<rightarrow> xs'"
   1.248 -	"G\<turnstile>Norm s \<midarrow>In3  ([])                      \<succ>\<midarrow>n\<rightarrow> vs'"
   1.249 -	"G\<turnstile>Norm s \<midarrow>In3  (e#es)                    \<succ>\<midarrow>n\<rightarrow> vs'"
   1.250 -	"G\<turnstile>Norm s \<midarrow>In1l (Lit w)                   \<succ>\<midarrow>n\<rightarrow> vs'"
   1.251 -        "G\<turnstile>Norm s \<midarrow>In1l (UnOp unop e)             \<succ>\<midarrow>n\<rightarrow> vs'"
   1.252 -        "G\<turnstile>Norm s \<midarrow>In1l (BinOp binop e1 e2)       \<succ>\<midarrow>n\<rightarrow> vs'"
   1.253 -	"G\<turnstile>Norm s \<midarrow>In2  (LVar vn)                 \<succ>\<midarrow>n\<rightarrow> vs'"
   1.254 -	"G\<turnstile>Norm s \<midarrow>In1l (Cast T e)                \<succ>\<midarrow>n\<rightarrow> vs'"
   1.255 -	"G\<turnstile>Norm s \<midarrow>In1l (e InstOf T)              \<succ>\<midarrow>n\<rightarrow> vs'"
   1.256 -	"G\<turnstile>Norm s \<midarrow>In1l (Super)                   \<succ>\<midarrow>n\<rightarrow> vs'"
   1.257 -	"G\<turnstile>Norm s \<midarrow>In1l (Acc va)                  \<succ>\<midarrow>n\<rightarrow> vs'"
   1.258 -	"G\<turnstile>Norm s \<midarrow>In1r (Expr e)                  \<succ>\<midarrow>n\<rightarrow> xs'"
   1.259 -	"G\<turnstile>Norm s \<midarrow>In1r (c1;; c2)                 \<succ>\<midarrow>n\<rightarrow> xs'"
   1.260 -	"G\<turnstile>Norm s \<midarrow>In1l (Methd C sig)             \<succ>\<midarrow>n\<rightarrow> xs'"
   1.261 -	"G\<turnstile>Norm s \<midarrow>In1l (Body D c)                \<succ>\<midarrow>n\<rightarrow> xs'"
   1.262 -	"G\<turnstile>Norm s \<midarrow>In1l (e0 ? e1 : e2)            \<succ>\<midarrow>n\<rightarrow> vs'"
   1.263 -	"G\<turnstile>Norm s \<midarrow>In1r (If(e) c1 Else c2)        \<succ>\<midarrow>n\<rightarrow> xs'"
   1.264 -	"G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> While(e) c)           \<succ>\<midarrow>n\<rightarrow> xs'"
   1.265 -	"G\<turnstile>Norm s \<midarrow>In1r (c1 Finally c2)           \<succ>\<midarrow>n\<rightarrow> xs'"
   1.266 -	"G\<turnstile>Norm s \<midarrow>In1r (Throw e)                 \<succ>\<midarrow>n\<rightarrow> xs'"
   1.267 -	"G\<turnstile>Norm s \<midarrow>In1l (NewC C)                  \<succ>\<midarrow>n\<rightarrow> vs'"
   1.268 -	"G\<turnstile>Norm s \<midarrow>In1l (New T[e])                \<succ>\<midarrow>n\<rightarrow> vs'"
   1.269 -	"G\<turnstile>Norm s \<midarrow>In1l (Ass va e)                \<succ>\<midarrow>n\<rightarrow> vs'"
   1.270 -	"G\<turnstile>Norm s \<midarrow>In1r (Try c1 Catch(tn vn) c2)  \<succ>\<midarrow>n\<rightarrow> xs'"
   1.271 -	"G\<turnstile>Norm s \<midarrow>In2  ({accC,statDeclC,stat}e..fn) \<succ>\<midarrow>n\<rightarrow> vs'"
   1.272 -	"G\<turnstile>Norm s \<midarrow>In2  (e1.[e2])                 \<succ>\<midarrow>n\<rightarrow> vs'"
   1.273 -	"G\<turnstile>Norm s \<midarrow>In1l ({accC,statT,mode}e\<cdot>mn({pT}p)) \<succ>\<midarrow>n\<rightarrow> vs'"
   1.274 -	"G\<turnstile>Norm s \<midarrow>In1r (Init C)                  \<succ>\<midarrow>n\<rightarrow> xs'"
   1.275 -        "G\<turnstile>Norm s \<midarrow>In1r (Init C)                  \<succ>\<midarrow>n\<rightarrow> xs'"
   1.276 +inductive_cases2 evaln_elim_cases:
   1.277 +	"G\<turnstile>(Some xc, s) \<midarrow>t                        \<succ>\<midarrow>n\<rightarrow> (v, s')"
   1.278 +	"G\<turnstile>Norm s \<midarrow>In1r Skip                      \<succ>\<midarrow>n\<rightarrow> (x, s')"
   1.279 +        "G\<turnstile>Norm s \<midarrow>In1r (Jmp j)                   \<succ>\<midarrow>n\<rightarrow> (x, s')"
   1.280 +        "G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> c)                    \<succ>\<midarrow>n\<rightarrow> (x, s')"
   1.281 +	"G\<turnstile>Norm s \<midarrow>In3  ([])                      \<succ>\<midarrow>n\<rightarrow> (v, s')"
   1.282 +	"G\<turnstile>Norm s \<midarrow>In3  (e#es)                    \<succ>\<midarrow>n\<rightarrow> (v, s')"
   1.283 +	"G\<turnstile>Norm s \<midarrow>In1l (Lit w)                   \<succ>\<midarrow>n\<rightarrow> (v, s')"
   1.284 +        "G\<turnstile>Norm s \<midarrow>In1l (UnOp unop e)             \<succ>\<midarrow>n\<rightarrow> (v, s')"
   1.285 +        "G\<turnstile>Norm s \<midarrow>In1l (BinOp binop e1 e2)       \<succ>\<midarrow>n\<rightarrow> (v, s')"
   1.286 +	"G\<turnstile>Norm s \<midarrow>In2  (LVar vn)                 \<succ>\<midarrow>n\<rightarrow> (v, s')"
   1.287 +	"G\<turnstile>Norm s \<midarrow>In1l (Cast T e)                \<succ>\<midarrow>n\<rightarrow> (v, s')"
   1.288 +	"G\<turnstile>Norm s \<midarrow>In1l (e InstOf T)              \<succ>\<midarrow>n\<rightarrow> (v, s')"
   1.289 +	"G\<turnstile>Norm s \<midarrow>In1l (Super)                   \<succ>\<midarrow>n\<rightarrow> (v, s')"
   1.290 +	"G\<turnstile>Norm s \<midarrow>In1l (Acc va)                  \<succ>\<midarrow>n\<rightarrow> (v, s')"
   1.291 +	"G\<turnstile>Norm s \<midarrow>In1r (Expr e)                  \<succ>\<midarrow>n\<rightarrow> (x, s')"
   1.292 +	"G\<turnstile>Norm s \<midarrow>In1r (c1;; c2)                 \<succ>\<midarrow>n\<rightarrow> (x, s')"
   1.293 +	"G\<turnstile>Norm s \<midarrow>In1l (Methd C sig)             \<succ>\<midarrow>n\<rightarrow> (x, s')"
   1.294 +	"G\<turnstile>Norm s \<midarrow>In1l (Body D c)                \<succ>\<midarrow>n\<rightarrow> (x, s')"
   1.295 +	"G\<turnstile>Norm s \<midarrow>In1l (e0 ? e1 : e2)            \<succ>\<midarrow>n\<rightarrow> (v, s')"
   1.296 +	"G\<turnstile>Norm s \<midarrow>In1r (If(e) c1 Else c2)        \<succ>\<midarrow>n\<rightarrow> (x, s')"
   1.297 +	"G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> While(e) c)           \<succ>\<midarrow>n\<rightarrow> (x, s')"
   1.298 +	"G\<turnstile>Norm s \<midarrow>In1r (c1 Finally c2)           \<succ>\<midarrow>n\<rightarrow> (x, s')"
   1.299 +	"G\<turnstile>Norm s \<midarrow>In1r (Throw e)                 \<succ>\<midarrow>n\<rightarrow> (x, s')"
   1.300 +	"G\<turnstile>Norm s \<midarrow>In1l (NewC C)                  \<succ>\<midarrow>n\<rightarrow> (v, s')"
   1.301 +	"G\<turnstile>Norm s \<midarrow>In1l (New T[e])                \<succ>\<midarrow>n\<rightarrow> (v, s')"
   1.302 +	"G\<turnstile>Norm s \<midarrow>In1l (Ass va e)                \<succ>\<midarrow>n\<rightarrow> (v, s')"
   1.303 +	"G\<turnstile>Norm s \<midarrow>In1r (Try c1 Catch(tn vn) c2)  \<succ>\<midarrow>n\<rightarrow> (x, s')"
   1.304 +	"G\<turnstile>Norm s \<midarrow>In2  ({accC,statDeclC,stat}e..fn) \<succ>\<midarrow>n\<rightarrow> (v, s')"
   1.305 +	"G\<turnstile>Norm s \<midarrow>In2  (e1.[e2])                 \<succ>\<midarrow>n\<rightarrow> (v, s')"
   1.306 +	"G\<turnstile>Norm s \<midarrow>In1l ({accC,statT,mode}e\<cdot>mn({pT}p)) \<succ>\<midarrow>n\<rightarrow> (v, s')"
   1.307 +	"G\<turnstile>Norm s \<midarrow>In1r (Init C)                  \<succ>\<midarrow>n\<rightarrow> (x, s')"
   1.308 +        "G\<turnstile>Norm s \<midarrow>In1r (Init C)                  \<succ>\<midarrow>n\<rightarrow> (x, s')"
   1.309  
   1.310  declare split_if     [split] split_if_asm     [split] 
   1.311          option.split [split] option.split_asm [split]
   1.312 @@ -288,25 +260,32 @@
   1.313   (injection @{term In1} into generalised values @{term vals}). 
   1.314  *}
   1.315  
   1.316 +lemma evaln_expr_eq: "G\<turnstile>s \<midarrow>In1l t\<succ>\<midarrow>n\<rightarrow> (w, s') = (\<exists>v. w=In1 v \<and> G\<turnstile>s \<midarrow>t-\<succ>v \<midarrow>n\<rightarrow> s')"
   1.317 +  by (auto, frule evaln_Inj_elim, auto)
   1.318 +
   1.319 +lemma evaln_var_eq: "G\<turnstile>s \<midarrow>In2 t\<succ>\<midarrow>n\<rightarrow> (w, s') = (\<exists>vf. w=In2 vf \<and> G\<turnstile>s \<midarrow>t=\<succ>vf\<midarrow>n\<rightarrow> s')"
   1.320 +  by (auto, frule evaln_Inj_elim, auto)
   1.321 +
   1.322 +lemma evaln_exprs_eq: "G\<turnstile>s \<midarrow>In3 t\<succ>\<midarrow>n\<rightarrow> (w, s') = (\<exists>vs. w=In3 vs \<and> G\<turnstile>s \<midarrow>t\<doteq>\<succ>vs\<midarrow>n\<rightarrow> s')"
   1.323 +  by (auto, frule evaln_Inj_elim, auto)
   1.324 +
   1.325 +lemma evaln_stmt_eq: "G\<turnstile>s \<midarrow>In1r t\<succ>\<midarrow>n\<rightarrow> (w, s') = (w=\<diamondsuit> \<and> G\<turnstile>s \<midarrow>t \<midarrow>n\<rightarrow> s')"
   1.326 +  by (auto, frule evaln_Inj_elim, auto, frule evaln_Inj_elim, auto)
   1.327 +
   1.328  ML_setup {*
   1.329 -fun enf nam inj rhs =
   1.330 +fun enf name lhs =
   1.331  let
   1.332 -  val name = "evaln_" ^ nam ^ "_eq"
   1.333 -  val lhs = "G\<turnstile>s \<midarrow>" ^ inj ^ " t\<succ>\<midarrow>n\<rightarrow> (w, s')"
   1.334 -  val () = qed_goal name (the_context()) (lhs ^ " = (" ^ rhs ^ ")") 
   1.335 -	(K [Auto_tac, ALLGOALS (ftac (thm "evaln_Inj_elim")) THEN Auto_tac])
   1.336    fun is_Inj (Const (inj,_) $ _) = true
   1.337      | is_Inj _                   = false
   1.338 -  fun pred (_ $ (Const ("Pair",_) $ _ $ (Const ("Pair", _) $ _ $ 
   1.339 -    (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ x $ _ )))) $ _ ) = is_Inj x
   1.340 +  fun pred (_ $ _ $ _ $ _ $ _ $ x $ _) = is_Inj x
   1.341  in
   1.342    cond_simproc name lhs pred (thm name)
   1.343  end;
   1.344  
   1.345 -val evaln_expr_proc = enf "expr" "In1l" "\<exists>v.  w=In1 v  \<and> G\<turnstile>s \<midarrow>t-\<succ>v \<midarrow>n\<rightarrow> s'";
   1.346 -val evaln_var_proc  = enf "var"  "In2"  "\<exists>vf. w=In2 vf \<and> G\<turnstile>s \<midarrow>t=\<succ>vf\<midarrow>n\<rightarrow> s'";
   1.347 -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'";
   1.348 -val evaln_stmt_proc = enf "stmt" "In1r" "     w=\<diamondsuit>      \<and> G\<turnstile>s \<midarrow>t     \<midarrow>n\<rightarrow> s'";
   1.349 +val evaln_expr_proc  = enf "evaln_expr_eq"  "G\<turnstile>s \<midarrow>In1l t\<succ>\<midarrow>n\<rightarrow> (w, s')";
   1.350 +val evaln_var_proc   = enf "evaln_var_eq"   "G\<turnstile>s \<midarrow>In2 t\<succ>\<midarrow>n\<rightarrow> (w, s')";
   1.351 +val evaln_exprs_proc = enf "evaln_exprs_eq" "G\<turnstile>s \<midarrow>In3 t\<succ>\<midarrow>n\<rightarrow> (w, s')";
   1.352 +val evaln_stmt_proc  = enf "evaln_stmt_eq"  "G\<turnstile>s \<midarrow>In1r t\<succ>\<midarrow>n\<rightarrow> (w, s')";
   1.353  Addsimprocs [evaln_expr_proc,evaln_var_proc,evaln_exprs_proc,evaln_stmt_proc];
   1.354  
   1.355  bind_thms ("evaln_AbruptIs", sum3_instantiate (thm "evaln.Abrupt"))
   1.356 @@ -319,9 +298,7 @@
   1.357      assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
   1.358           normal: "normal s" and
   1.359           callee: "t=In1l (Callee l e)"
   1.360 -    then have "False"
   1.361 -    proof (induct)
   1.362 -    qed (auto)
   1.363 +    then have "False" by induct auto
   1.364    }
   1.365    then show ?thesis
   1.366      by (cases s') fastsimp 
   1.367 @@ -333,9 +310,7 @@
   1.368      assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
   1.369           normal: "normal s" and
   1.370           callee: "t=In1l (InsInitE c e)"
   1.371 -    then have "False"
   1.372 -    proof (induct)
   1.373 -    qed (auto)
   1.374 +    then have "False" by induct auto
   1.375    }
   1.376    then show ?thesis
   1.377      by (cases s') fastsimp
   1.378 @@ -347,9 +322,7 @@
   1.379      assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
   1.380           normal: "normal s" and
   1.381           callee: "t=In2 (InsInitV c w)"
   1.382 -    then have "False"
   1.383 -    proof (induct)
   1.384 -    qed (auto)
   1.385 +    then have "False" by induct auto
   1.386    }  
   1.387    then show ?thesis
   1.388      by (cases s') fastsimp
   1.389 @@ -361,9 +334,7 @@
   1.390      assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
   1.391           normal: "normal s" and
   1.392           callee: "t=In1r (FinA a c)"
   1.393 -    then have "False"
   1.394 -    proof (induct)
   1.395 -    qed (auto)
   1.396 +    then have "False" by induct auto
   1.397    } 
   1.398    then show ?thesis
   1.399      by (cases s') fastsimp
   1.400 @@ -385,9 +356,7 @@
   1.401  local
   1.402    fun is_Some (Const ("Pair",_) $ (Const ("Datatype.option.Some",_) $ _)$ _) =true
   1.403      | is_Some _ = false
   1.404 -  fun pred (_ $ (Const ("Pair",_) $
   1.405 -     _ $ (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ _ $
   1.406 -       (Const ("Pair", _) $ _ $ x)))) $ _ ) = is_Some x
   1.407 +  fun pred (_ $ _ $ _ $ _ $ _ $ _ $ x) = is_Some x
   1.408  in
   1.409    val evaln_abrupt_proc = 
   1.410   cond_simproc "evaln_abrupt" "G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (w,s')" pred (thm "evaln_abrupt")
   1.411 @@ -440,7 +409,7 @@
   1.412    shows "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"
   1.413  using evaln 
   1.414  proof (induct)
   1.415 -  case (Loop b c e l n s0 s1 s2 s3)
   1.416 +  case (Loop s0 e n b s1 c s2 l s3)
   1.417    have "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1".
   1.418    moreover
   1.419    have "if the_Bool b
   1.420 @@ -450,7 +419,7 @@
   1.421      using Loop.hyps by simp
   1.422    ultimately show ?case by (rule eval.Loop)
   1.423  next
   1.424 -  case (Try c1 c2 n s0 s1 s2 s3 C vn)
   1.425 +  case (Try s0 c1 n s1 s2 C vn c2 s3)
   1.426    have "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1".
   1.427    moreover
   1.428    have "G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2".
   1.429 @@ -459,7 +428,7 @@
   1.430      using Try.hyps by simp
   1.431    ultimately show ?case by (rule eval.Try)
   1.432  next
   1.433 -  case (Init C c n s0 s1 s2 s3)
   1.434 +  case (Init C c s0 s3 n s1 s2)
   1.435    have "the (class G C) = c".
   1.436    moreover
   1.437    have "if inited C (globs s0) 
   1.438 @@ -478,8 +447,7 @@
   1.439  done
   1.440  
   1.441  lemma evaln_nonstrict [rule_format (no_asm), elim]: 
   1.442 -  "\<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"
   1.443 -apply (simp (no_asm_simp) only: split_tupled_all)
   1.444 +  "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (w, s') \<Longrightarrow> \<forall>m. n\<le>m \<longrightarrow> G\<turnstile>s \<midarrow>t\<succ>\<midarrow>m\<rightarrow> (w, s')"
   1.445  apply (erule evaln.induct)
   1.446  apply (tactic {* ALLGOALS (EVERY'[strip_tac, TRY o etac (thm "Suc_le_D_lemma"),
   1.447    REPEAT o smp_tac 1, 
   1.448 @@ -490,30 +458,30 @@
   1.449  
   1.450  lemmas evaln_nonstrict_Suc = evaln_nonstrict [OF _ le_refl [THEN le_SucI]]
   1.451  
   1.452 -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> 
   1.453 -             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"
   1.454 +lemma evaln_max2: "\<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>n1\<rightarrow> (w1, s1'); G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>n2\<rightarrow> (w2, s2')\<rbrakk> \<Longrightarrow> 
   1.455 +             G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max n1 n2\<rightarrow> (w1, s1') \<and> G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max n1 n2\<rightarrow> (w2, s2')"
   1.456  by (fast intro: le_maxI1 le_maxI2)
   1.457  
   1.458  corollary evaln_max2E [consumes 2]:
   1.459 -  "\<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>n1\<rightarrow> ws1; G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>n2\<rightarrow> ws2; 
   1.460 -    \<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"
   1.461 +  "\<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>n1\<rightarrow> (w1, s1'); G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>n2\<rightarrow> (w2, s2'); 
   1.462 +    \<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max n1 n2\<rightarrow> (w1, s1');G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max n1 n2\<rightarrow> (w2, s2') \<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
   1.463  by (drule (1) evaln_max2) simp
   1.464  
   1.465  
   1.466  lemma evaln_max3: 
   1.467 -"\<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>
   1.468 - G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> ws1 \<and>
   1.469 - G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> ws2 \<and> 
   1.470 - G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> ws3"
   1.471 +"\<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>n1\<rightarrow> (w1, s1'); G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>n2\<rightarrow> (w2, s2'); G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>n3\<rightarrow> (w3, s3')\<rbrakk> \<Longrightarrow>
   1.472 + G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> (w1, s1') \<and>
   1.473 + G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> (w2, s2') \<and> 
   1.474 + G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> (w3, s3')"
   1.475  apply (drule (1) evaln_max2, erule thin_rl)
   1.476  apply (fast intro!: le_maxI1 le_maxI2)
   1.477  done
   1.478  
   1.479  corollary evaln_max3E: 
   1.480 -"\<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;
   1.481 -   \<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> ws1;
   1.482 -    G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> ws2; 
   1.483 -    G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> ws3
   1.484 +"\<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>n1\<rightarrow> (w1, s1'); G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>n2\<rightarrow> (w2, s2'); G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>n3\<rightarrow> (w3, s3');
   1.485 +   \<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> (w1, s1');
   1.486 +    G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> (w2, s2'); 
   1.487 +    G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> (w3, s3')
   1.488     \<rbrakk> \<Longrightarrow> P
   1.489    \<rbrakk> \<Longrightarrow> P"
   1.490  by (drule (2) evaln_max3) simp
   1.491 @@ -551,16 +519,16 @@
   1.492    shows  "\<exists>n. G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)"
   1.493  using eval 
   1.494  proof (induct)
   1.495 -  case (Abrupt s t xc)
   1.496 +  case (Abrupt xc s t)
   1.497    obtain n where
   1.498 -    "G\<turnstile>(Some xc, s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (arbitrary3 t, Some xc, s)"
   1.499 +    "G\<turnstile>(Some xc, s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (arbitrary3 t, (Some xc, s))"
   1.500      by (iprover intro: evaln.Abrupt)
   1.501    then show ?case ..
   1.502  next
   1.503    case Skip
   1.504    show ?case by (blast intro: evaln.Skip)
   1.505  next
   1.506 -  case (Expr e s0 s1 v)
   1.507 +  case (Expr s0 e v s1)
   1.508    then obtain n where
   1.509      "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
   1.510      by (iprover)
   1.511 @@ -568,7 +536,7 @@
   1.512      by (rule evaln.Expr) 
   1.513    then show ?case ..
   1.514  next
   1.515 -  case (Lab c l s0 s1)
   1.516 +  case (Lab s0 c s1 l)
   1.517    then obtain n where
   1.518      "G\<turnstile>Norm s0 \<midarrow>c\<midarrow>n\<rightarrow> s1"
   1.519      by (iprover)
   1.520 @@ -576,7 +544,7 @@
   1.521      by (rule evaln.Lab)
   1.522    then show ?case ..
   1.523  next
   1.524 -  case (Comp c1 c2 s0 s1 s2)
   1.525 +  case (Comp s0 c1 s1 c2 s2)
   1.526    then obtain n1 n2 where
   1.527      "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> s1"
   1.528      "G\<turnstile>s1 \<midarrow>c2\<midarrow>n2\<rightarrow> s2"
   1.529 @@ -585,7 +553,7 @@
   1.530      by (blast intro: evaln.Comp dest: evaln_max2 )
   1.531    then show ?case ..
   1.532  next
   1.533 -  case (If b c1 c2 e s0 s1 s2)
   1.534 +  case (If s0 e b s1 c1 c2 s2)
   1.535    then obtain n1 n2 where
   1.536      "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n1\<rightarrow> s1"
   1.537      "G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<midarrow>n2\<rightarrow> s2"
   1.538 @@ -594,7 +562,7 @@
   1.539      by (blast intro: evaln.If dest: evaln_max2)
   1.540    then show ?case ..
   1.541  next
   1.542 -  case (Loop b c e l s0 s1 s2 s3)
   1.543 +  case (Loop s0 e b s1 c s2 l s3)
   1.544    from Loop.hyps obtain n1 where
   1.545      "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n1\<rightarrow> s1"
   1.546      by (iprover)
   1.547 @@ -614,12 +582,12 @@
   1.548      done
   1.549    then show ?case ..
   1.550  next
   1.551 -  case (Jmp j s)
   1.552 +  case (Jmp s j)
   1.553    have "G\<turnstile>Norm s \<midarrow>Jmp j\<midarrow>n\<rightarrow> (Some (Jump j), s)"
   1.554      by (rule evaln.Jmp)
   1.555    then show ?case ..
   1.556  next
   1.557 -  case (Throw a e s0 s1)
   1.558 +  case (Throw s0 e a s1)
   1.559    then obtain n where
   1.560      "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<midarrow>n\<rightarrow> s1"
   1.561      by (iprover)
   1.562 @@ -627,7 +595,7 @@
   1.563      by (rule evaln.Throw)
   1.564    then show ?case ..
   1.565  next 
   1.566 -  case (Try catchC c1 c2 s0 s1 s2 s3 vn)
   1.567 +  case (Try s0 c1 s1 s2 catchC vn c2 s3)
   1.568    from Try.hyps obtain n1 where
   1.569      "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> s1"
   1.570      by (iprover)
   1.571 @@ -642,7 +610,7 @@
   1.572      by (auto intro!: evaln.Try le_maxI1 le_maxI2)
   1.573    then show ?case ..
   1.574  next
   1.575 -  case (Fin c1 c2 s0 s1 s2 s3 x1)
   1.576 +  case (Fin s0 c1 x1 s1 c2 s2 s3)
   1.577    from Fin obtain n1 n2 where 
   1.578      "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> (x1, s1)"
   1.579      "G\<turnstile>Norm s1 \<midarrow>c2\<midarrow>n2\<rightarrow> s2"
   1.580 @@ -657,7 +625,7 @@
   1.581      by (blast intro: evaln.Fin dest: evaln_max2)
   1.582    then show ?case ..
   1.583  next
   1.584 -  case (Init C c s0 s1 s2 s3)
   1.585 +  case (Init C c s0 s3 s1 s2)
   1.586    have     cls: "the (class G C) = c" .
   1.587    moreover from Init.hyps obtain n where
   1.588        "if inited C (globs s0) then s3 = Norm s0
   1.589 @@ -670,7 +638,7 @@
   1.590      by (rule evaln.Init)
   1.591    then show ?case ..
   1.592  next
   1.593 -  case (NewC C a s0 s1 s2)
   1.594 +  case (NewC s0 C s1 a s2)
   1.595    then obtain n where 
   1.596      "G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s1"
   1.597      by (iprover)
   1.598 @@ -679,7 +647,7 @@
   1.599      by (iprover intro: evaln.NewC)
   1.600    then show ?case ..
   1.601  next
   1.602 -  case (NewA T a e i s0 s1 s2 s3)
   1.603 +  case (NewA s0 T s1 e i s2 a s3)
   1.604    then obtain n1 n2 where 
   1.605      "G\<turnstile>Norm s0 \<midarrow>init_comp_ty T\<midarrow>n1\<rightarrow> s1"
   1.606      "G\<turnstile>s1 \<midarrow>e-\<succ>i\<midarrow>n2\<rightarrow> s2"      
   1.607 @@ -691,7 +659,7 @@
   1.608      by (blast intro: evaln.NewA dest: evaln_max2)
   1.609    then show ?case ..
   1.610  next
   1.611 -  case (Cast castT e s0 s1 s2 v)
   1.612 +  case (Cast s0 e v s1 s2 castT)
   1.613    then obtain n where
   1.614      "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
   1.615      by (iprover)
   1.616 @@ -702,7 +670,7 @@
   1.617      by (rule evaln.Cast)
   1.618    then show ?case ..
   1.619  next
   1.620 -  case (Inst T b e s0 s1 v)
   1.621 +  case (Inst s0 e v s1 b T)
   1.622    then obtain n where
   1.623      "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
   1.624      by (iprover)
   1.625 @@ -718,7 +686,7 @@
   1.626      by (rule evaln.Lit)
   1.627    then show ?case ..
   1.628  next
   1.629 -  case (UnOp e s0 s1 unop v )
   1.630 +  case (UnOp s0 e v s1 unop)
   1.631    then obtain n where
   1.632      "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
   1.633      by (iprover)
   1.634 @@ -726,7 +694,7 @@
   1.635      by (rule evaln.UnOp)
   1.636    then show ?case ..
   1.637  next
   1.638 -  case (BinOp binop e1 e2 s0 s1 s2 v1 v2)
   1.639 +  case (BinOp s0 e1 v1 s1 binop e2 v2 s2)
   1.640    then obtain n1 n2 where 
   1.641      "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<midarrow>n1\<rightarrow> s1"
   1.642      "G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then In1l e2
   1.643 @@ -742,7 +710,7 @@
   1.644      by (rule evaln.Super)
   1.645    then show ?case ..
   1.646  next
   1.647 -  case (Acc f s0 s1 v va)
   1.648 +  case (Acc s0 va v f s1)
   1.649    then obtain n where
   1.650      "G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v, f)\<midarrow>n\<rightarrow> s1"
   1.651      by (iprover)
   1.652 @@ -751,7 +719,7 @@
   1.653      by (rule evaln.Acc)
   1.654    then show ?case ..
   1.655  next
   1.656 -  case (Ass e f s0 s1 s2 v var w)
   1.657 +  case (Ass s0 var w f s1 e v s2)
   1.658    then obtain n1 n2 where 
   1.659      "G\<turnstile>Norm s0 \<midarrow>var=\<succ>(w, f)\<midarrow>n1\<rightarrow> s1"
   1.660      "G\<turnstile>s1 \<midarrow>e-\<succ>v\<midarrow>n2\<rightarrow> s2"      
   1.661 @@ -761,7 +729,7 @@
   1.662      by (blast intro: evaln.Ass dest: evaln_max2)
   1.663    then show ?case ..
   1.664  next
   1.665 -  case (Cond b e0 e1 e2 s0 s1 s2 v)
   1.666 +  case (Cond s0 e0 b s1 e1 e2 v s2)
   1.667    then obtain n1 n2 where 
   1.668      "G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<midarrow>n1\<rightarrow> s1"
   1.669      "G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<midarrow>n2\<rightarrow> s2"
   1.670 @@ -771,8 +739,7 @@
   1.671      by (blast intro: evaln.Cond dest: evaln_max2)
   1.672    then show ?case ..
   1.673  next
   1.674 -  case (Call invDeclC a' accC' args e mn mode pTs' s0 s1 s2 s3 s3' s4 statT 
   1.675 -        v vs)
   1.676 +  case (Call s0 e a' s1 args vs s2 invDeclC mode statT mn pTs' s3 s3' accC' v s4)
   1.677    then obtain n1 n2 where
   1.678      "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n1\<rightarrow> s1"
   1.679      "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<midarrow>n2\<rightarrow> s2"
   1.680 @@ -795,7 +762,7 @@
   1.681      by (auto intro!: evaln.Call le_maxI1 le_max3I1 le_max3I2)
   1.682    thus ?case ..
   1.683  next
   1.684 -  case (Methd D s0 s1 sig v )
   1.685 +  case (Methd s0 D sig v s1)
   1.686    then obtain n where
   1.687      "G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<midarrow>n\<rightarrow> s1"
   1.688      by iprover
   1.689 @@ -803,7 +770,7 @@
   1.690      by (rule evaln.Methd)
   1.691    then show ?case ..
   1.692  next
   1.693 -  case (Body D c s0 s1 s2 s3 )
   1.694 +  case (Body s0 D s1 c s2 s3)
   1.695    from Body.hyps obtain n1 n2 where 
   1.696      evaln_init: "G\<turnstile>Norm s0 \<midarrow>Init D\<midarrow>n1\<rightarrow> s1" and
   1.697      evaln_c: "G\<turnstile>s1 \<midarrow>c\<midarrow>n2\<rightarrow> s2"
   1.698 @@ -826,7 +793,7 @@
   1.699      by (iprover intro: evaln.LVar)
   1.700    then show ?case ..
   1.701  next
   1.702 -  case (FVar a accC e fn s0 s1 s2 s2' s3 stat statDeclC v)
   1.703 +  case (FVar s0 statDeclC s1 e a s2 v s2' stat fn s3 accC)
   1.704    then obtain n1 n2 where
   1.705      "G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<midarrow>n1\<rightarrow> s1"
   1.706      "G\<turnstile>s1 \<midarrow>e-\<succ>a\<midarrow>n2\<rightarrow> s2"
   1.707 @@ -839,7 +806,7 @@
   1.708      by (iprover intro: evaln.FVar dest: evaln_max2)
   1.709    then show ?case ..
   1.710  next
   1.711 -  case (AVar a e1 e2 i s0 s1 s2 s2' v )
   1.712 +  case (AVar s0 e1 a s1 e2 i s2 v s2')
   1.713    then obtain n1 n2 where 
   1.714      "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>a\<midarrow>n1\<rightarrow> s1"
   1.715      "G\<turnstile>s1 \<midarrow>e2-\<succ>i\<midarrow>n2\<rightarrow> s2"      
   1.716 @@ -854,7 +821,7 @@
   1.717    case (Nil s0)
   1.718    show ?case by (iprover intro: evaln.Nil)
   1.719  next
   1.720 -  case (Cons e es s0 s1 s2 v vs)
   1.721 +  case (Cons s0 e v s1 es vs s2)
   1.722    then obtain n1 n2 where 
   1.723      "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n1\<rightarrow> s1"
   1.724      "G\<turnstile>s1 \<midarrow>es\<doteq>\<succ>vs\<midarrow>n2\<rightarrow> s2"