src/HOL/Bali/Evaln.thy
 author wenzelm Tue Mar 18 11:07:47 2014 +0100 (2014-03-18) changeset 56199 8e8d28ed7529 parent 54863 82acc20ded73 child 58251 b13e5c3497f5 permissions -rw-r--r--
tuned signature -- rearranged modules;
1 (*  Title:      HOL/Bali/Evaln.thy
2     Author:     David von Oheimb and Norbert Schirmer
3 *)
4 header {* Operational evaluation (big-step) semantics of Java expressions and
5           statements
6 *}
8 theory Evaln imports TypeSafe begin
11 text {*
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 *}
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 --{* propagation of abrupt completion *}
51 | Abrupt:   "G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (undefined3 t,(Some xc,s))"
54 --{* evaluation of variables *}
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 --{* evaluation of expressions *}
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 --{* evaluation of expression lists *}
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 --{* execution of statements *}
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 {* map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac") *}
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 {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
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   (induct_tac "a")
249 apply auto
250 done
252 text {* 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 *}
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')") = {*
272   fn _ => fn _ => fn ct =>
273     (case Thm.term_of ct of
274       (_ \$ _ \$ _ \$ _ \$ _ \$ (Const _ \$ _) \$ _) => NONE
275     | _ => SOME (mk_meta_eq @{thm evaln_expr_eq})) *}
277 simproc_setup evaln_var ("G\<turnstile>s \<midarrow>In2 t\<succ>\<midarrow>n\<rightarrow> (w, s')") = {*
278   fn _ => fn _ => fn ct =>
279     (case Thm.term_of ct of
280       (_ \$ _ \$ _ \$ _ \$ _ \$ (Const _ \$ _) \$ _) => NONE
281     | _ => SOME (mk_meta_eq @{thm evaln_var_eq})) *}
283 simproc_setup evaln_exprs ("G\<turnstile>s \<midarrow>In3 t\<succ>\<midarrow>n\<rightarrow> (w, s')") = {*
284   fn _ => fn _ => fn ct =>
285     (case Thm.term_of ct of
286       (_ \$ _ \$ _ \$ _ \$ _ \$ (Const _ \$ _) \$ _) => NONE
287     | _ => SOME (mk_meta_eq @{thm evaln_exprs_eq})) *}
289 simproc_setup evaln_stmt ("G\<turnstile>s \<midarrow>In1r t\<succ>\<midarrow>n\<rightarrow> (w, s')") = {*
290   fn _ => fn _ => fn ct =>
291     (case Thm.term_of ct of
292       (_ \$ _ \$ _ \$ _ \$ _ \$ (Const _ \$ _) \$ _) => NONE
293     | _ => SOME (mk_meta_eq @{thm evaln_stmt_eq})) *}
295 ML {* ML_Thms.bind_thms ("evaln_AbruptIs", sum3_instantiate @{context} @{thm evaln.Abrupt}) *}
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')") = {*
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 *}
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 section {* evaln implies eval *}
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 `G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1`
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 `G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1`
423   moreover
424   note `G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2`
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 `the (class G C) = c`
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 {* ALLGOALS (EVERY'[strip_tac, TRY o etac @{thm Suc_le_D_lemma},
452   REPEAT o smp_tac 1,
453   resolve_tac @{thms evaln.intros} THEN_ALL_NEW TRY o atac]) *})
454 (* 3 subgoals *)
455 apply (auto split del: split_if)
456 done
458 lemmas evaln_nonstrict_Suc = evaln_nonstrict [OF _ le_refl [THEN le_SucI]]
460 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>
461              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')"
462 by (fast intro: max.cobounded1 max.cobounded2)
464 corollary evaln_max2E [consumes 2]:
465   "\<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>n1\<rightarrow> (w1, s1'); G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>n2\<rightarrow> (w2, s2');
466     \<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"
467 by (drule (1) evaln_max2) simp
470 lemma evaln_max3:
471 "\<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>n1\<rightarrow> (w1, s1'); G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>n2\<rightarrow> (w2, s2'); G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>n3\<rightarrow> (w3, s3')\<rbrakk> \<Longrightarrow>
472  G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> (w1, s1') \<and>
473  G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> (w2, s2') \<and>
474  G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> (w3, s3')"
475 apply (drule (1) evaln_max2, erule thin_rl)
476 apply (fast intro!: max.cobounded1 max.cobounded2)
477 done
479 corollary evaln_max3E:
480 "\<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');
481    \<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> (w1, s1');
482     G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> (w2, s2');
483     G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> (w3, s3')
484    \<rbrakk> \<Longrightarrow> P
485   \<rbrakk> \<Longrightarrow> P"
486 by (drule (2) evaln_max3) simp
489 lemma le_max3I1: "(n2::nat) \<le> max n1 (max n2 n3)"
490 proof -
491   have "n2 \<le> max n2 n3"
492     by (rule max.cobounded1)
493   also
494   have "max n2 n3 \<le> max n1 (max n2 n3)"
495     by (rule max.cobounded2)
496   finally
497   show ?thesis .
498 qed
500 lemma le_max3I2: "(n3::nat) \<le> max n1 (max n2 n3)"
501 proof -
502   have "n3 \<le> max n2 n3"
503     by (rule max.cobounded2)
504   also
505   have "max n2 n3 \<le> max n1 (max n2 n3)"
506     by (rule max.cobounded2)
507   finally
508   show ?thesis .
509 qed
511 declare [[simproc del: wt_expr wt_var wt_exprs wt_stmt]]
513 section {* eval implies evaln *}
514 lemma eval_evaln:
515   assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"
516   shows  "\<exists>n. G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)"
517 using eval
518 proof (induct)
519   case (Abrupt xc s t)
520   obtain n where
521     "G\<turnstile>(Some xc, s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (undefined3 t, (Some xc, s))"
522     by (iprover intro: evaln.Abrupt)
523   then show ?case ..
524 next
525   case Skip
526   show ?case by (blast intro: evaln.Skip)
527 next
528   case (Expr s0 e v s1)
529   then obtain n where
530     "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
531     by (iprover)
532   then have "G\<turnstile>Norm s0 \<midarrow>Expr e\<midarrow>n\<rightarrow> s1"
533     by (rule evaln.Expr)
534   then show ?case ..
535 next
536   case (Lab s0 c s1 l)
537   then obtain n where
538     "G\<turnstile>Norm s0 \<midarrow>c\<midarrow>n\<rightarrow> s1"
539     by (iprover)
540   then have "G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<midarrow>n\<rightarrow> abupd (absorb l) s1"
541     by (rule evaln.Lab)
542   then show ?case ..
543 next
544   case (Comp s0 c1 s1 c2 s2)
545   then obtain n1 n2 where
546     "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> s1"
547     "G\<turnstile>s1 \<midarrow>c2\<midarrow>n2\<rightarrow> s2"
548     by (iprover)
549   then have "G\<turnstile>Norm s0 \<midarrow>c1;; c2\<midarrow>max n1 n2\<rightarrow> s2"
550     by (blast intro: evaln.Comp dest: evaln_max2 )
551   then show ?case ..
552 next
553   case (If s0 e b s1 c1 c2 s2)
554   then obtain n1 n2 where
555     "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n1\<rightarrow> s1"
556     "G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<midarrow>n2\<rightarrow> s2"
557     by (iprover)
558   then have "G\<turnstile>Norm s0 \<midarrow>If(e) c1 Else c2\<midarrow>max n1 n2\<rightarrow> s2"
559     by (blast intro: evaln.If dest: evaln_max2)
560   then show ?case ..
561 next
562   case (Loop s0 e b s1 c s2 l s3)
563   from Loop.hyps obtain n1 where
564     "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n1\<rightarrow> s1"
565     by (iprover)
566   moreover from Loop.hyps obtain n2 where
567     "if the_Bool b
568         then (G\<turnstile>s1 \<midarrow>c\<midarrow>n2\<rightarrow> s2 \<and>
569               G\<turnstile>(abupd (absorb (Cont l)) s2)\<midarrow>l\<bullet> While(e) c\<midarrow>n2\<rightarrow> s3)
570         else s3 = s1"
571     by simp (iprover intro: evaln_nonstrict max.cobounded1 max.cobounded2)
572   ultimately
573   have "G\<turnstile>Norm s0 \<midarrow>l\<bullet> While(e) c\<midarrow>max n1 n2\<rightarrow> s3"
574     apply -
575     apply (rule evaln.Loop)
576     apply   (iprover intro: evaln_nonstrict intro: max.cobounded1)
577     apply   (auto intro: evaln_nonstrict intro: max.cobounded2)
578     done
579   then show ?case ..
580 next
581   case (Jmp s j)
582   fix n have "G\<turnstile>Norm s \<midarrow>Jmp j\<midarrow>n\<rightarrow> (Some (Jump j), s)"
583     by (rule evaln.Jmp)
584   then show ?case ..
585 next
586   case (Throw s0 e a s1)
587   then obtain n where
588     "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<midarrow>n\<rightarrow> s1"
589     by (iprover)
590   then have "G\<turnstile>Norm s0 \<midarrow>Throw e\<midarrow>n\<rightarrow> abupd (throw a) s1"
591     by (rule evaln.Throw)
592   then show ?case ..
593 next
594   case (Try s0 c1 s1 s2 catchC vn c2 s3)
595   from Try.hyps obtain n1 where
596     "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> s1"
597     by (iprover)
598   moreover
599   note sxalloc = `G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2`
600   moreover
601   from Try.hyps obtain n2 where
602     "if G,s2\<turnstile>catch catchC then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<midarrow>n2\<rightarrow> s3 else s3 = s2"
603     by fastforce
604   ultimately
605   have "G\<turnstile>Norm s0 \<midarrow>Try c1 Catch(catchC vn) c2\<midarrow>max n1 n2\<rightarrow> s3"
606     by (auto intro!: evaln.Try max.cobounded1 max.cobounded2)
607   then show ?case ..
608 next
609   case (Fin s0 c1 x1 s1 c2 s2 s3)
610   from Fin obtain n1 n2 where
611     "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> (x1, s1)"
612     "G\<turnstile>Norm s1 \<midarrow>c2\<midarrow>n2\<rightarrow> s2"
613     by iprover
614   moreover
615   note s3 = `s3 = (if \<exists>err. x1 = Some (Error err)
616                    then (x1, s1)
617                    else abupd (abrupt_if (x1 \<noteq> None) x1) s2)`
618   ultimately
619   have
620     "G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<midarrow>max n1 n2\<rightarrow> s3"
621     by (blast intro: evaln.Fin dest: evaln_max2)
622   then show ?case ..
623 next
624   case (Init C c s0 s3 s1 s2)
625   note cls = `the (class G C) = c`
626   moreover from Init.hyps obtain n where
627       "if inited C (globs s0) then s3 = Norm s0
628        else (G\<turnstile>Norm (init_class_obj G C s0)
629               \<midarrow>(if C = Object then Skip else Init (super c))\<midarrow>n\<rightarrow> s1 \<and>
630                    G\<turnstile>set_lvars empty s1 \<midarrow>init c\<midarrow>n\<rightarrow> s2 \<and>
631                    s3 = restore_lvars s1 s2)"
632     by (auto intro: evaln_nonstrict max.cobounded1 max.cobounded2)
633   ultimately have "G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s3"
634     by (rule evaln.Init)
635   then show ?case ..
636 next
637   case (NewC s0 C s1 a s2)
638   then obtain n where
639     "G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s1"
640     by (iprover)
641   with NewC
642   have "G\<turnstile>Norm s0 \<midarrow>NewC C-\<succ>Addr a\<midarrow>n\<rightarrow> s2"
643     by (iprover intro: evaln.NewC)
644   then show ?case ..
645 next
646   case (NewA s0 T s1 e i s2 a s3)
647   then obtain n1 n2 where
648     "G\<turnstile>Norm s0 \<midarrow>init_comp_ty T\<midarrow>n1\<rightarrow> s1"
649     "G\<turnstile>s1 \<midarrow>e-\<succ>i\<midarrow>n2\<rightarrow> s2"
650     by (iprover)
651   moreover
652   note `G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3`
653   ultimately
654   have "G\<turnstile>Norm s0 \<midarrow>New T[e]-\<succ>Addr a\<midarrow>max n1 n2\<rightarrow> s3"
655     by (blast intro: evaln.NewA dest: evaln_max2)
656   then show ?case ..
657 next
658   case (Cast s0 e v s1 s2 castT)
659   then obtain n where
660     "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
661     by (iprover)
662   moreover
663   note `s2 = abupd (raise_if (\<not> G,snd s1\<turnstile>v fits castT) ClassCast) s1`
664   ultimately
665   have "G\<turnstile>Norm s0 \<midarrow>Cast castT e-\<succ>v\<midarrow>n\<rightarrow> s2"
666     by (rule evaln.Cast)
667   then show ?case ..
668 next
669   case (Inst s0 e v s1 b T)
670   then obtain n where
671     "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
672     by (iprover)
673   moreover
674   note `b = (v \<noteq> Null \<and> G,snd s1\<turnstile>v fits RefT T)`
675   ultimately
676   have "G\<turnstile>Norm s0 \<midarrow>e InstOf T-\<succ>Bool b\<midarrow>n\<rightarrow> s1"
677     by (rule evaln.Inst)
678   then show ?case ..
679 next
680   case (Lit s v)
681   fix n have "G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<midarrow>n\<rightarrow> Norm s"
682     by (rule evaln.Lit)
683   then show ?case ..
684 next
685   case (UnOp s0 e v s1 unop)
686   then obtain n where
687     "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
688     by (iprover)
689   hence "G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>eval_unop unop v\<midarrow>n\<rightarrow> s1"
690     by (rule evaln.UnOp)
691   then show ?case ..
692 next
693   case (BinOp s0 e1 v1 s1 binop e2 v2 s2)
694   then obtain n1 n2 where
695     "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<midarrow>n1\<rightarrow> s1"
696     "G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then In1l e2
697                else In1r Skip)\<succ>\<midarrow>n2\<rightarrow> (In1 v2, s2)"
698     by (iprover)
699   hence "G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<midarrow>max n1 n2
700           \<rightarrow> s2"
701     by (blast intro!: evaln.BinOp dest: evaln_max2)
702   then show ?case ..
703 next
704   case (Super s )
705   fix n have "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<midarrow>n\<rightarrow> Norm s"
706     by (rule evaln.Super)
707   then show ?case ..
708 next
709   case (Acc s0 va v f s1)
710   then obtain n where
711     "G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v, f)\<midarrow>n\<rightarrow> s1"
712     by (iprover)
713   then
714   have "G\<turnstile>Norm s0 \<midarrow>Acc va-\<succ>v\<midarrow>n\<rightarrow> s1"
715     by (rule evaln.Acc)
716   then show ?case ..
717 next
718   case (Ass s0 var w f s1 e v s2)
719   then obtain n1 n2 where
720     "G\<turnstile>Norm s0 \<midarrow>var=\<succ>(w, f)\<midarrow>n1\<rightarrow> s1"
721     "G\<turnstile>s1 \<midarrow>e-\<succ>v\<midarrow>n2\<rightarrow> s2"
722     by (iprover)
723   then
724   have "G\<turnstile>Norm s0 \<midarrow>var:=e-\<succ>v\<midarrow>max n1 n2\<rightarrow> assign f v s2"
725     by (blast intro: evaln.Ass dest: evaln_max2)
726   then show ?case ..
727 next
728   case (Cond s0 e0 b s1 e1 e2 v s2)
729   then obtain n1 n2 where
730     "G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<midarrow>n1\<rightarrow> s1"
731     "G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<midarrow>n2\<rightarrow> s2"
732     by (iprover)
733   then
734   have "G\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<midarrow>max n1 n2\<rightarrow> s2"
735     by (blast intro: evaln.Cond dest: evaln_max2)
736   then show ?case ..
737 next
738   case (Call s0 e a' s1 args vs s2 invDeclC mode statT mn pTs' s3 s3' accC' v s4)
739   then obtain n1 n2 where
740     "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n1\<rightarrow> s1"
741     "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<midarrow>n2\<rightarrow> s2"
742     by iprover
743   moreover
744   note `invDeclC = invocation_declclass G mode (store s2) a' statT
745                        \<lparr>name=mn,parTs=pTs'\<rparr>`
746   moreover
747   note `s3 = init_lvars G invDeclC \<lparr>name=mn,parTs=pTs'\<rparr> mode a' vs s2`
748   moreover
749   note `s3'=check_method_access G accC' statT mode \<lparr>name=mn,parTs=pTs'\<rparr> a' s3`
750   moreover
751   from Call.hyps
752   obtain m where
753     "G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name=mn, parTs=pTs'\<rparr>-\<succ>v\<midarrow>m\<rightarrow> s4"
754     by iprover
755   ultimately
756   have "G\<turnstile>Norm s0 \<midarrow>{accC',statT,mode}e\<cdot>mn( {pTs'}args)-\<succ>v\<midarrow>max n1 (max n2 m)\<rightarrow>
757             (set_lvars (locals (store s2))) s4"
758     by (auto intro!: evaln.Call max.cobounded1 le_max3I1 le_max3I2)
759   thus ?case ..
760 next
761   case (Methd s0 D sig v s1)
762   then obtain n where
763     "G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<midarrow>n\<rightarrow> s1"
764     by iprover
765   then have "G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<midarrow>Suc n\<rightarrow> s1"
766     by (rule evaln.Methd)
767   then show ?case ..
768 next
769   case (Body s0 D s1 c s2 s3)
770   from Body.hyps obtain n1 n2 where
771     evaln_init: "G\<turnstile>Norm s0 \<midarrow>Init D\<midarrow>n1\<rightarrow> s1" and
772     evaln_c: "G\<turnstile>s1 \<midarrow>c\<midarrow>n2\<rightarrow> s2"
773     by (iprover)
774   moreover
775   note `s3 = (if \<exists>l. fst s2 = Some (Jump (Break l)) \<or>
776                      fst s2 = Some (Jump (Cont l))
777               then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2
778               else s2)`
779   ultimately
780   have
781      "G\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>the (locals (store s2) Result)\<midarrow>max n1 n2
782        \<rightarrow> abupd (absorb Ret) s3"
783     by (iprover intro: evaln.Body dest: evaln_max2)
784   then show ?case ..
785 next
786   case (LVar s vn )
787   obtain n where
788     "G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<midarrow>n\<rightarrow> Norm s"
789     by (iprover intro: evaln.LVar)
790   then show ?case ..
791 next
792   case (FVar s0 statDeclC s1 e a s2 v s2' stat fn s3 accC)
793   then obtain n1 n2 where
794     "G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<midarrow>n1\<rightarrow> s1"
795     "G\<turnstile>s1 \<midarrow>e-\<succ>a\<midarrow>n2\<rightarrow> s2"
796     by iprover
797   moreover
798   note `s3 = check_field_access G accC statDeclC fn stat a s2'`
799     and `(v, s2') = fvar statDeclC stat fn a s2`
800   ultimately
801   have "G\<turnstile>Norm s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>v\<midarrow>max n1 n2\<rightarrow> s3"
802     by (iprover intro: evaln.FVar dest: evaln_max2)
803   then show ?case ..
804 next
805   case (AVar s0 e1 a s1 e2 i s2 v s2')
806   then obtain n1 n2 where
807     "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>a\<midarrow>n1\<rightarrow> s1"
808     "G\<turnstile>s1 \<midarrow>e2-\<succ>i\<midarrow>n2\<rightarrow> s2"
809     by iprover
810   moreover
811   note `(v, s2') = avar G i a s2`
812   ultimately
813   have "G\<turnstile>Norm s0 \<midarrow>e1.[e2]=\<succ>v\<midarrow>max n1 n2\<rightarrow> s2'"
814     by (blast intro!: evaln.AVar dest: evaln_max2)
815   then show ?case ..
816 next
817   case (Nil s0)
818   show ?case by (iprover intro: evaln.Nil)
819 next
820   case (Cons s0 e v s1 es vs s2)
821   then obtain n1 n2 where
822     "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n1\<rightarrow> s1"
823     "G\<turnstile>s1 \<midarrow>es\<doteq>\<succ>vs\<midarrow>n2\<rightarrow> s2"
824     by iprover
825   then
826   have "G\<turnstile>Norm s0 \<midarrow>e # es\<doteq>\<succ>v # vs\<midarrow>max n1 n2\<rightarrow> s2"
827     by (blast intro!: evaln.Cons dest: evaln_max2)
828   then show ?case ..
829 qed
831 end