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