src/HOL/Bali/Evaln.thy
 author wenzelm Sun Sep 18 20:33:48 2016 +0200 (2016-09-18) changeset 63915 bab633745c7f parent 62390 842917225d56 child 67443 3abf6a722518 permissions -rw-r--r--
tuned proofs;
```     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>
```
```     7
```
```     8 theory Evaln imports TypeSafe begin
```
```     9
```
```    10
```
```    11 text \<open>
```
```    12 Variant of @{term eval} relation with counter for bounded recursive depth.
```
```    13 In principal @{term evaln} could replace @{term eval}.
```
```    14
```
```    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>
```
```    29
```
```    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
```
```    43
```
```    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')"
```
```    48
```
```    49 \<comment>\<open>propagation of abrupt completion\<close>
```
```    50
```
```    51 | Abrupt:   "G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (undefined3 t,(Some xc,s))"
```
```    52
```
```    53
```
```    54 \<comment>\<open>evaluation of variables\<close>
```
```    55
```
```    56 | LVar: "G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<midarrow>n\<rightarrow> Norm s"
```
```    57
```
```    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"
```
```    62
```
```    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'"
```
```    66
```
```    67
```
```    68
```
```    69
```
```    70 \<comment>\<open>evaluation of expressions\<close>
```
```    71
```
```    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"
```
```    75
```
```    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"
```
```    79
```
```    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"
```
```    83
```
```    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"
```
```    87
```
```    88 | Lit:                     "G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<midarrow>n\<rightarrow> Norm s"
```
```    89
```
```    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"
```
```    92
```
```    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"
```
```    97
```
```    98 | Super:                   "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<midarrow>n\<rightarrow> Norm s"
```
```    99
```
```   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"
```
```   102
```
```   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"
```
```   106
```
```   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"
```
```   110
```
```   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)"
```
```   120
```
```   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"
```
```   123
```
```   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"
```
```   131
```
```   132 \<comment>\<open>evaluation of expression lists\<close>
```
```   133
```
```   134 | Nil:
```
```   135                                 "G\<turnstile>Norm s0 \<midarrow>[]\<doteq>\<succ>[]\<midarrow>n\<rightarrow> Norm s0"
```
```   136
```
```   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"
```
```   140
```
```   141
```
```   142 \<comment>\<open>execution of statements\<close>
```
```   143
```
```   144 | Skip:                             "G\<turnstile>Norm s \<midarrow>Skip\<midarrow>n\<rightarrow> Norm s"
```
```   145
```
```   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"
```
```   148
```
```   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"
```
```   151
```
```   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"
```
```   155
```
```   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"
```
```   159
```
```   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"
```
```   166
```
```   167 | Jmp: "G\<turnstile>Norm s \<midarrow>Jmp j\<midarrow>n\<rightarrow> (Some (Jump j), s)"
```
```   168
```
```   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"
```
```   171
```
```   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"
```
```   176
```
```   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"
```
```   183
```
```   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
```
```   194
```
```   195
```
```   196 declare if_split     [split del] if_split_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>
```
```   201
```
```   202 inductive_cases evaln_cases: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v, s')"
```
```   203
```
```   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')"
```
```   236
```
```   237 declare if_split     [split] if_split_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>
```
```   242
```
```   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
```
```   251
```
```   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>
```
```   258
```
```   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)
```
```   261
```
```   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)
```
```   264
```
```   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)
```
```   267
```
```   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)
```
```   270
```
```   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>
```
```   276
```
```   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>
```
```   282
```
```   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>
```
```   288
```
```   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>
```
```   294
```
```   295 ML \<open>ML_Thms.bind_thms ("evaln_AbruptIs", sum3_instantiate @{context} @{thm evaln.Abrupt})\<close>
```
```   296 declare evaln_AbruptIs [intro!]
```
```   297
```
```   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
```
```   309
```
```   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
```
```   321
```
```   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
```
```   333
```
```   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
```
```   345
```
```   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
```
```   350
```
```   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
```
```   357
```
```   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>
```
```   365
```
```   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)
```
```   369
```
```   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)
```
```   375
```
```   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)
```
```   379
```
```   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)
```
```   383
```
```   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)
```
```   387
```
```   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)
```
```   393
```
```   394 lemma evaln_SkipD [dest!]: "G\<turnstile>s \<midarrow>Skip\<midarrow>n\<rightarrow> s' \<Longrightarrow> s' = s"
```
```   395 by (erule evaln_cases, auto)
```
```   396
```
```   397 lemma evaln_Skip_eq [simp]: "G\<turnstile>s \<midarrow>Skip\<midarrow>n\<rightarrow> s' = (s = s')"
```
```   398 apply auto
```
```   399 done
```
```   400
```
```   401
```
```   402
```
```   403
```
```   404 subsubsection \<open>evaln implies eval\<close>
```
```   405
```
```   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?))+
```
```   442
```
```   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
```
```   447
```
```   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: if_split)
```
```   457 done
```
```   458
```
```   459 lemmas evaln_nonstrict_Suc = evaln_nonstrict [OF _ le_refl [THEN le_SucI]]
```
```   460
```
```   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)
```
```   464
```
```   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
```
```   469
```
```   470
```
```   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
```
```   479
```
```   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
```
```   488
```
```   489
```
```   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
```
```   500
```
```   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
```
```   511
```
```   512 declare [[simproc del: wt_expr wt_var wt_exprs wt_stmt]]
```
```   513
```
```   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
```
```   831
```
```   832 end
```