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