src/HOL/Bali/Evaln.thy
 author kuncar Fri Dec 09 18:07:04 2011 +0100 (2011-12-09) changeset 45802 b16f976db515 parent 44890 22f665a2e91c child 46714 a7ca72710dfe permissions -rw-r--r--
Quotient_Info stores only relation maps
```     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 *}
```
```     7
```
```     8 theory Evaln imports TypeSafe begin
```
```     9
```
```    10
```
```    11 text {*
```
```    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 *}
```
```    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 --{* propagation of abrupt completion *}
```
```    50
```
```    51 | Abrupt:   "G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (undefined3 t,(Some xc,s))"
```
```    52
```
```    53
```
```    54 --{* evaluation of variables *}
```
```    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 --{* evaluation of expressions *}
```
```    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 --{* evaluation of expression lists *}
```
```   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 --{* execution of statements *}
```
```   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 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 declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
```
```   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         "G\<turnstile>Norm s \<midarrow>In1r (Init C)                  \<succ>\<midarrow>n\<rightarrow> (x, s')"
```
```   237
```
```   238 declare split_if     [split] split_if_asm     [split]
```
```   239         option.split [split] option.split_asm [split]
```
```   240         not_None_eq [simp]
```
```   241         split_paired_All [simp] split_paired_Ex [simp]
```
```   242 declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
```
```   243
```
```   244 lemma evaln_Inj_elim: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (w,s') \<Longrightarrow> case t of In1 ec \<Rightarrow>
```
```   245   (case ec of Inl e \<Rightarrow> (\<exists>v. w = In1 v) | Inr c \<Rightarrow> w = \<diamondsuit>)
```
```   246   | In2 e \<Rightarrow> (\<exists>v. w = In2 v) | In3 e \<Rightarrow> (\<exists>v. w = In3 v)"
```
```   247 apply (erule evaln_cases , auto)
```
```   248 apply (induct_tac "t")
```
```   249 apply   (induct_tac "a")
```
```   250 apply auto
```
```   251 done
```
```   252
```
```   253 text {* The following simplification procedures set up the proper injections of
```
```   254  terms and their corresponding values in the evaluation relation:
```
```   255  E.g. an expression
```
```   256  (injection @{term In1l} into terms) always evaluates to ordinary values
```
```   257  (injection @{term In1} into generalised values @{term vals}).
```
```   258 *}
```
```   259
```
```   260 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')"
```
```   261   by (auto, frule evaln_Inj_elim, auto)
```
```   262
```
```   263 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')"
```
```   264   by (auto, frule evaln_Inj_elim, auto)
```
```   265
```
```   266 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')"
```
```   267   by (auto, frule evaln_Inj_elim, auto)
```
```   268
```
```   269 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')"
```
```   270   by (auto, frule evaln_Inj_elim, auto, frule evaln_Inj_elim, auto)
```
```   271
```
```   272 simproc_setup evaln_expr ("G\<turnstile>s \<midarrow>In1l t\<succ>\<midarrow>n\<rightarrow> (w, s')") = {*
```
```   273   fn _ => fn _ => fn ct =>
```
```   274     (case Thm.term_of ct of
```
```   275       (_ \$ _ \$ _ \$ _ \$ _ \$ (Const _ \$ _) \$ _) => NONE
```
```   276     | _ => SOME (mk_meta_eq @{thm evaln_expr_eq})) *}
```
```   277
```
```   278 simproc_setup evaln_var ("G\<turnstile>s \<midarrow>In2 t\<succ>\<midarrow>n\<rightarrow> (w, s')") = {*
```
```   279   fn _ => fn _ => fn ct =>
```
```   280     (case Thm.term_of ct of
```
```   281       (_ \$ _ \$ _ \$ _ \$ _ \$ (Const _ \$ _) \$ _) => NONE
```
```   282     | _ => SOME (mk_meta_eq @{thm evaln_var_eq})) *}
```
```   283
```
```   284 simproc_setup evaln_exprs ("G\<turnstile>s \<midarrow>In3 t\<succ>\<midarrow>n\<rightarrow> (w, s')") = {*
```
```   285   fn _ => fn _ => fn ct =>
```
```   286     (case Thm.term_of ct of
```
```   287       (_ \$ _ \$ _ \$ _ \$ _ \$ (Const _ \$ _) \$ _) => NONE
```
```   288     | _ => SOME (mk_meta_eq @{thm evaln_exprs_eq})) *}
```
```   289
```
```   290 simproc_setup evaln_stmt ("G\<turnstile>s \<midarrow>In1r t\<succ>\<midarrow>n\<rightarrow> (w, s')") = {*
```
```   291   fn _ => fn _ => fn ct =>
```
```   292     (case Thm.term_of ct of
```
```   293       (_ \$ _ \$ _ \$ _ \$ _ \$ (Const _ \$ _) \$ _) => NONE
```
```   294     | _ => SOME (mk_meta_eq @{thm evaln_stmt_eq})) *}
```
```   295
```
```   296 ML {* bind_thms ("evaln_AbruptIs", sum3_instantiate @{context} @{thm evaln.Abrupt}) *}
```
```   297 declare evaln_AbruptIs [intro!]
```
```   298
```
```   299 lemma evaln_Callee: "G\<turnstile>Norm s\<midarrow>In1l (Callee l e)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
```
```   300 proof -
```
```   301   { fix s t v s'
```
```   302     assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
```
```   303          normal: "normal s" and
```
```   304          callee: "t=In1l (Callee l e)"
```
```   305     then have "False" by induct auto
```
```   306   }
```
```   307   then show ?thesis
```
```   308     by (cases s') fastforce
```
```   309 qed
```
```   310
```
```   311 lemma evaln_InsInitE: "G\<turnstile>Norm s\<midarrow>In1l (InsInitE c e)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
```
```   312 proof -
```
```   313   { fix s t v s'
```
```   314     assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
```
```   315          normal: "normal s" and
```
```   316          callee: "t=In1l (InsInitE c e)"
```
```   317     then have "False" by induct auto
```
```   318   }
```
```   319   then show ?thesis
```
```   320     by (cases s') fastforce
```
```   321 qed
```
```   322
```
```   323 lemma evaln_InsInitV: "G\<turnstile>Norm s\<midarrow>In2 (InsInitV c w)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
```
```   324 proof -
```
```   325   { fix s t v s'
```
```   326     assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
```
```   327          normal: "normal s" and
```
```   328          callee: "t=In2 (InsInitV c w)"
```
```   329     then have "False" by induct auto
```
```   330   }
```
```   331   then show ?thesis
```
```   332     by (cases s') fastforce
```
```   333 qed
```
```   334
```
```   335 lemma evaln_FinA: "G\<turnstile>Norm s\<midarrow>In1r (FinA a c)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
```
```   336 proof -
```
```   337   { fix s t v s'
```
```   338     assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
```
```   339          normal: "normal s" and
```
```   340          callee: "t=In1r (FinA a c)"
```
```   341     then have "False" by induct auto
```
```   342   }
```
```   343   then show ?thesis
```
```   344     by (cases s') fastforce
```
```   345 qed
```
```   346
```
```   347 lemma evaln_abrupt_lemma: "G\<turnstile>s \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (v,s') \<Longrightarrow>
```
```   348  fst s = Some xc \<longrightarrow> s' = s \<and> v = undefined3 e"
```
```   349 apply (erule evaln_cases , auto)
```
```   350 done
```
```   351
```
```   352 lemma evaln_abrupt:
```
```   353  "\<And>s'. G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (w,s') = (s' = (Some xc,s) \<and>
```
```   354   w=undefined3 e \<and> G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (undefined3 e,(Some xc,s)))"
```
```   355 apply auto
```
```   356 apply (frule evaln_abrupt_lemma, auto)+
```
```   357 done
```
```   358
```
```   359 simproc_setup evaln_abrupt ("G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (w,s')") = {*
```
```   360   fn _ => fn _ => fn ct =>
```
```   361     (case Thm.term_of ct of
```
```   362       (_ \$ _ \$ _ \$ _ \$ _ \$ _ \$ (Const (@{const_name Pair}, _) \$ (Const (@{const_name Some},_) \$ _)\$ _))
```
```   363         => NONE
```
```   364     | _ => SOME (mk_meta_eq @{thm evaln_abrupt}))
```
```   365 *}
```
```   366
```
```   367 lemma evaln_LitI: "G\<turnstile>s \<midarrow>Lit v-\<succ>(if normal s then v else undefined)\<midarrow>n\<rightarrow> s"
```
```   368 apply (case_tac "s", case_tac "a = None")
```
```   369 by (auto intro!: evaln.Lit)
```
```   370
```
```   371 lemma CondI:
```
```   372  "\<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>
```
```   373   G\<turnstile>s \<midarrow>e ? e1 : e2-\<succ>(if normal s1 then v else undefined)\<midarrow>n\<rightarrow> s2"
```
```   374 apply (case_tac "s", case_tac "a = None")
```
```   375 by (auto intro!: evaln.Cond)
```
```   376
```
```   377 lemma evaln_SkipI [intro!]: "G\<turnstile>s \<midarrow>Skip\<midarrow>n\<rightarrow> s"
```
```   378 apply (case_tac "s", case_tac "a = None")
```
```   379 by (auto intro!: evaln.Skip)
```
```   380
```
```   381 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'"
```
```   382 apply (case_tac "s", case_tac "a = None")
```
```   383 by (auto intro!: evaln.Expr)
```
```   384
```
```   385 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"
```
```   386 apply (case_tac "s", case_tac "a = None")
```
```   387 by (auto intro!: evaln.Comp)
```
```   388
```
```   389 lemma evaln_IfI:
```
```   390  "\<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>
```
```   391   G\<turnstile>s \<midarrow>If(e) c1 Else c2\<midarrow>n\<rightarrow> s2"
```
```   392 apply (case_tac "s", case_tac "a = None")
```
```   393 by (auto intro!: evaln.If)
```
```   394
```
```   395 lemma evaln_SkipD [dest!]: "G\<turnstile>s \<midarrow>Skip\<midarrow>n\<rightarrow> s' \<Longrightarrow> s' = s"
```
```   396 by (erule evaln_cases, auto)
```
```   397
```
```   398 lemma evaln_Skip_eq [simp]: "G\<turnstile>s \<midarrow>Skip\<midarrow>n\<rightarrow> s' = (s = s')"
```
```   399 apply auto
```
```   400 done
```
```   401
```
```   402
```
```   403
```
```   404
```
```   405 section {* evaln implies eval *}
```
```   406
```
```   407 lemma evaln_eval:
```
```   408   assumes evaln: "G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)"
```
```   409   shows "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"
```
```   410 using evaln
```
```   411 proof (induct)
```
```   412   case (Loop s0 e b n s1 c s2 l s3)
```
```   413   note `G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1`
```
```   414   moreover
```
```   415   have "if the_Bool b
```
```   416         then (G\<turnstile>s1 \<midarrow>c\<rightarrow> s2) \<and>
```
```   417              G\<turnstile>abupd (absorb (Cont l)) s2 \<midarrow>l\<bullet> While(e) c\<rightarrow> s3
```
```   418         else s3 = s1"
```
```   419     using Loop.hyps by simp
```
```   420   ultimately show ?case by (rule eval.Loop)
```
```   421 next
```
```   422   case (Try s0 c1 n s1 s2 C vn c2 s3)
```
```   423   note `G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1`
```
```   424   moreover
```
```   425   note `G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2`
```
```   426   moreover
```
```   427   have "if G,s2\<turnstile>catch C then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<rightarrow> s3 else s3 = s2"
```
```   428     using Try.hyps by simp
```
```   429   ultimately show ?case by (rule eval.Try)
```
```   430 next
```
```   431   case (Init C c s0 s3 n s1 s2)
```
```   432   note `the (class G C) = c`
```
```   433   moreover
```
```   434   have "if inited C (globs s0)
```
```   435            then s3 = Norm s0
```
```   436            else G\<turnstile>Norm ((init_class_obj G C) s0)
```
```   437                   \<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1 \<and>
```
```   438                 G\<turnstile>(set_lvars empty) s1 \<midarrow>init c\<rightarrow> s2 \<and>
```
```   439                 s3 = (set_lvars (locals (store s1))) s2"
```
```   440     using Init.hyps by simp
```
```   441   ultimately show ?case by (rule eval.Init)
```
```   442 qed (rule eval.intros,(assumption+ | assumption?))+
```
```   443
```
```   444 lemma Suc_le_D_lemma: "\<lbrakk>Suc n <= m'; (\<And>m. n <= m \<Longrightarrow> P (Suc m)) \<rbrakk> \<Longrightarrow> P m'"
```
```   445 apply (frule Suc_le_D)
```
```   446 apply fast
```
```   447 done
```
```   448
```
```   449 lemma evaln_nonstrict [rule_format (no_asm), elim]:
```
```   450   "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')"
```
```   451 apply (erule evaln.induct)
```
```   452 apply (tactic {* ALLGOALS (EVERY'[strip_tac, TRY o etac @{thm Suc_le_D_lemma},
```
```   453   REPEAT o smp_tac 1,
```
```   454   resolve_tac @{thms evaln.intros} THEN_ALL_NEW TRY o atac]) *})
```
```   455 (* 3 subgoals *)
```
```   456 apply (auto split del: split_if)
```
```   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: le_maxI1 le_maxI2)
```
```   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!: le_maxI1 le_maxI2)
```
```   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 le_maxI1)
```
```   494   also
```
```   495   have "max n2 n3 \<le> max n1 (max n2 n3)"
```
```   496     by (rule le_maxI2)
```
```   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 le_maxI2)
```
```   505   also
```
```   506   have "max n2 n3 \<le> max n1 (max n2 n3)"
```
```   507     by (rule le_maxI2)
```
```   508   finally
```
```   509   show ?thesis .
```
```   510 qed
```
```   511
```
```   512 declare [[simproc del: wt_expr wt_var wt_exprs wt_stmt]]
```
```   513
```
```   514 section {* eval implies evaln *}
```
```   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 le_maxI1 le_maxI2)
```
```   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: le_maxI1)
```
```   578
```
```   579     apply   (auto intro: evaln_nonstrict intro: le_maxI2)
```
```   580     done
```
```   581   then show ?case ..
```
```   582 next
```
```   583   case (Jmp s j)
```
```   584   fix n have "G\<turnstile>Norm s \<midarrow>Jmp j\<midarrow>n\<rightarrow> (Some (Jump j), s)"
```
```   585     by (rule evaln.Jmp)
```
```   586   then show ?case ..
```
```   587 next
```
```   588   case (Throw s0 e a s1)
```
```   589   then obtain n where
```
```   590     "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<midarrow>n\<rightarrow> s1"
```
```   591     by (iprover)
```
```   592   then have "G\<turnstile>Norm s0 \<midarrow>Throw e\<midarrow>n\<rightarrow> abupd (throw a) s1"
```
```   593     by (rule evaln.Throw)
```
```   594   then show ?case ..
```
```   595 next
```
```   596   case (Try s0 c1 s1 s2 catchC vn c2 s3)
```
```   597   from Try.hyps obtain n1 where
```
```   598     "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> s1"
```
```   599     by (iprover)
```
```   600   moreover
```
```   601   note sxalloc = `G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2`
```
```   602   moreover
```
```   603   from Try.hyps obtain n2 where
```
```   604     "if G,s2\<turnstile>catch catchC then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<midarrow>n2\<rightarrow> s3 else s3 = s2"
```
```   605     by fastforce
```
```   606   ultimately
```
```   607   have "G\<turnstile>Norm s0 \<midarrow>Try c1 Catch(catchC vn) c2\<midarrow>max n1 n2\<rightarrow> s3"
```
```   608     by (auto intro!: evaln.Try le_maxI1 le_maxI2)
```
```   609   then show ?case ..
```
```   610 next
```
```   611   case (Fin s0 c1 x1 s1 c2 s2 s3)
```
```   612   from Fin obtain n1 n2 where
```
```   613     "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> (x1, s1)"
```
```   614     "G\<turnstile>Norm s1 \<midarrow>c2\<midarrow>n2\<rightarrow> s2"
```
```   615     by iprover
```
```   616   moreover
```
```   617   note s3 = `s3 = (if \<exists>err. x1 = Some (Error err)
```
```   618                    then (x1, s1)
```
```   619                    else abupd (abrupt_if (x1 \<noteq> None) x1) s2)`
```
```   620   ultimately
```
```   621   have
```
```   622     "G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<midarrow>max n1 n2\<rightarrow> s3"
```
```   623     by (blast intro: evaln.Fin dest: evaln_max2)
```
```   624   then show ?case ..
```
```   625 next
```
```   626   case (Init C c s0 s3 s1 s2)
```
```   627   note cls = `the (class G C) = c`
```
```   628   moreover from Init.hyps obtain n where
```
```   629       "if inited C (globs s0) then s3 = Norm s0
```
```   630        else (G\<turnstile>Norm (init_class_obj G C s0)
```
```   631               \<midarrow>(if C = Object then Skip else Init (super c))\<midarrow>n\<rightarrow> s1 \<and>
```
```   632                    G\<turnstile>set_lvars empty s1 \<midarrow>init c\<midarrow>n\<rightarrow> s2 \<and>
```
```   633                    s3 = restore_lvars s1 s2)"
```
```   634     by (auto intro: evaln_nonstrict le_maxI1 le_maxI2)
```
```   635   ultimately have "G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s3"
```
```   636     by (rule evaln.Init)
```
```   637   then show ?case ..
```
```   638 next
```
```   639   case (NewC s0 C s1 a s2)
```
```   640   then obtain n where
```
```   641     "G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s1"
```
```   642     by (iprover)
```
```   643   with NewC
```
```   644   have "G\<turnstile>Norm s0 \<midarrow>NewC C-\<succ>Addr a\<midarrow>n\<rightarrow> s2"
```
```   645     by (iprover intro: evaln.NewC)
```
```   646   then show ?case ..
```
```   647 next
```
```   648   case (NewA s0 T s1 e i s2 a s3)
```
```   649   then obtain n1 n2 where
```
```   650     "G\<turnstile>Norm s0 \<midarrow>init_comp_ty T\<midarrow>n1\<rightarrow> s1"
```
```   651     "G\<turnstile>s1 \<midarrow>e-\<succ>i\<midarrow>n2\<rightarrow> s2"
```
```   652     by (iprover)
```
```   653   moreover
```
```   654   note `G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3`
```
```   655   ultimately
```
```   656   have "G\<turnstile>Norm s0 \<midarrow>New T[e]-\<succ>Addr a\<midarrow>max n1 n2\<rightarrow> s3"
```
```   657     by (blast intro: evaln.NewA dest: evaln_max2)
```
```   658   then show ?case ..
```
```   659 next
```
```   660   case (Cast s0 e v s1 s2 castT)
```
```   661   then obtain n where
```
```   662     "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
```
```   663     by (iprover)
```
```   664   moreover
```
```   665   note `s2 = abupd (raise_if (\<not> G,snd s1\<turnstile>v fits castT) ClassCast) s1`
```
```   666   ultimately
```
```   667   have "G\<turnstile>Norm s0 \<midarrow>Cast castT e-\<succ>v\<midarrow>n\<rightarrow> s2"
```
```   668     by (rule evaln.Cast)
```
```   669   then show ?case ..
```
```   670 next
```
```   671   case (Inst s0 e v s1 b T)
```
```   672   then obtain n where
```
```   673     "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
```
```   674     by (iprover)
```
```   675   moreover
```
```   676   note `b = (v \<noteq> Null \<and> G,snd s1\<turnstile>v fits RefT T)`
```
```   677   ultimately
```
```   678   have "G\<turnstile>Norm s0 \<midarrow>e InstOf T-\<succ>Bool b\<midarrow>n\<rightarrow> s1"
```
```   679     by (rule evaln.Inst)
```
```   680   then show ?case ..
```
```   681 next
```
```   682   case (Lit s v)
```
```   683   fix n have "G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<midarrow>n\<rightarrow> Norm s"
```
```   684     by (rule evaln.Lit)
```
```   685   then show ?case ..
```
```   686 next
```
```   687   case (UnOp s0 e v s1 unop)
```
```   688   then obtain n where
```
```   689     "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
```
```   690     by (iprover)
```
```   691   hence "G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>eval_unop unop v\<midarrow>n\<rightarrow> s1"
```
```   692     by (rule evaln.UnOp)
```
```   693   then show ?case ..
```
```   694 next
```
```   695   case (BinOp s0 e1 v1 s1 binop e2 v2 s2)
```
```   696   then obtain n1 n2 where
```
```   697     "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<midarrow>n1\<rightarrow> s1"
```
```   698     "G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then In1l e2
```
```   699                else In1r Skip)\<succ>\<midarrow>n2\<rightarrow> (In1 v2, s2)"
```
```   700     by (iprover)
```
```   701   hence "G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<midarrow>max n1 n2
```
```   702           \<rightarrow> s2"
```
```   703     by (blast intro!: evaln.BinOp dest: evaln_max2)
```
```   704   then show ?case ..
```
```   705 next
```
```   706   case (Super s )
```
```   707   fix n have "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<midarrow>n\<rightarrow> Norm s"
```
```   708     by (rule evaln.Super)
```
```   709   then show ?case ..
```
```   710 next
```
```   711   case (Acc s0 va v f s1)
```
```   712   then obtain n where
```
```   713     "G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v, f)\<midarrow>n\<rightarrow> s1"
```
```   714     by (iprover)
```
```   715   then
```
```   716   have "G\<turnstile>Norm s0 \<midarrow>Acc va-\<succ>v\<midarrow>n\<rightarrow> s1"
```
```   717     by (rule evaln.Acc)
```
```   718   then show ?case ..
```
```   719 next
```
```   720   case (Ass s0 var w f s1 e v s2)
```
```   721   then obtain n1 n2 where
```
```   722     "G\<turnstile>Norm s0 \<midarrow>var=\<succ>(w, f)\<midarrow>n1\<rightarrow> s1"
```
```   723     "G\<turnstile>s1 \<midarrow>e-\<succ>v\<midarrow>n2\<rightarrow> s2"
```
```   724     by (iprover)
```
```   725   then
```
```   726   have "G\<turnstile>Norm s0 \<midarrow>var:=e-\<succ>v\<midarrow>max n1 n2\<rightarrow> assign f v s2"
```
```   727     by (blast intro: evaln.Ass dest: evaln_max2)
```
```   728   then show ?case ..
```
```   729 next
```
```   730   case (Cond s0 e0 b s1 e1 e2 v s2)
```
```   731   then obtain n1 n2 where
```
```   732     "G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<midarrow>n1\<rightarrow> s1"
```
```   733     "G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<midarrow>n2\<rightarrow> s2"
```
```   734     by (iprover)
```
```   735   then
```
```   736   have "G\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<midarrow>max n1 n2\<rightarrow> s2"
```
```   737     by (blast intro: evaln.Cond dest: evaln_max2)
```
```   738   then show ?case ..
```
```   739 next
```
```   740   case (Call s0 e a' s1 args vs s2 invDeclC mode statT mn pTs' s3 s3' accC' v s4)
```
```   741   then obtain n1 n2 where
```
```   742     "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n1\<rightarrow> s1"
```
```   743     "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<midarrow>n2\<rightarrow> s2"
```
```   744     by iprover
```
```   745   moreover
```
```   746   note `invDeclC = invocation_declclass G mode (store s2) a' statT
```
```   747                        \<lparr>name=mn,parTs=pTs'\<rparr>`
```
```   748   moreover
```
```   749   note `s3 = init_lvars G invDeclC \<lparr>name=mn,parTs=pTs'\<rparr> mode a' vs s2`
```
```   750   moreover
```
```   751   note `s3'=check_method_access G accC' statT mode \<lparr>name=mn,parTs=pTs'\<rparr> a' s3`
```
```   752   moreover
```
```   753   from Call.hyps
```
```   754   obtain m where
```
```   755     "G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name=mn, parTs=pTs'\<rparr>-\<succ>v\<midarrow>m\<rightarrow> s4"
```
```   756     by iprover
```
```   757   ultimately
```
```   758   have "G\<turnstile>Norm s0 \<midarrow>{accC',statT,mode}e\<cdot>mn( {pTs'}args)-\<succ>v\<midarrow>max n1 (max n2 m)\<rightarrow>
```
```   759             (set_lvars (locals (store s2))) s4"
```
```   760     by (auto intro!: evaln.Call le_maxI1 le_max3I1 le_max3I2)
```
```   761   thus ?case ..
```
```   762 next
```
```   763   case (Methd s0 D sig v s1)
```
```   764   then obtain n where
```
```   765     "G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<midarrow>n\<rightarrow> s1"
```
```   766     by iprover
```
```   767   then have "G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<midarrow>Suc n\<rightarrow> s1"
```
```   768     by (rule evaln.Methd)
```
```   769   then show ?case ..
```
```   770 next
```
```   771   case (Body s0 D s1 c s2 s3)
```
```   772   from Body.hyps obtain n1 n2 where
```
```   773     evaln_init: "G\<turnstile>Norm s0 \<midarrow>Init D\<midarrow>n1\<rightarrow> s1" and
```
```   774     evaln_c: "G\<turnstile>s1 \<midarrow>c\<midarrow>n2\<rightarrow> s2"
```
```   775     by (iprover)
```
```   776   moreover
```
```   777   note `s3 = (if \<exists>l. fst s2 = Some (Jump (Break l)) \<or>
```
```   778                      fst s2 = Some (Jump (Cont l))
```
```   779               then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2
```
```   780               else s2)`
```
```   781   ultimately
```
```   782   have
```
```   783      "G\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>the (locals (store s2) Result)\<midarrow>max n1 n2
```
```   784        \<rightarrow> abupd (absorb Ret) s3"
```
```   785     by (iprover intro: evaln.Body dest: evaln_max2)
```
```   786   then show ?case ..
```
```   787 next
```
```   788   case (LVar s vn )
```
```   789   obtain n where
```
```   790     "G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<midarrow>n\<rightarrow> Norm s"
```
```   791     by (iprover intro: evaln.LVar)
```
```   792   then show ?case ..
```
```   793 next
```
```   794   case (FVar s0 statDeclC s1 e a s2 v s2' stat fn s3 accC)
```
```   795   then obtain n1 n2 where
```
```   796     "G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<midarrow>n1\<rightarrow> s1"
```
```   797     "G\<turnstile>s1 \<midarrow>e-\<succ>a\<midarrow>n2\<rightarrow> s2"
```
```   798     by iprover
```
```   799   moreover
```
```   800   note `s3 = check_field_access G accC statDeclC fn stat a s2'`
```
```   801     and `(v, s2') = fvar statDeclC stat fn a s2`
```
```   802   ultimately
```
```   803   have "G\<turnstile>Norm s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>v\<midarrow>max n1 n2\<rightarrow> s3"
```
```   804     by (iprover intro: evaln.FVar dest: evaln_max2)
```
```   805   then show ?case ..
```
```   806 next
```
```   807   case (AVar s0 e1 a s1 e2 i s2 v s2')
```
```   808   then obtain n1 n2 where
```
```   809     "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>a\<midarrow>n1\<rightarrow> s1"
```
```   810     "G\<turnstile>s1 \<midarrow>e2-\<succ>i\<midarrow>n2\<rightarrow> s2"
```
```   811     by iprover
```
```   812   moreover
```
```   813   note `(v, s2') = avar G i a s2`
```
```   814   ultimately
```
```   815   have "G\<turnstile>Norm s0 \<midarrow>e1.[e2]=\<succ>v\<midarrow>max n1 n2\<rightarrow> s2'"
```
```   816     by (blast intro!: evaln.AVar dest: evaln_max2)
```
```   817   then show ?case ..
```
```   818 next
```
```   819   case (Nil s0)
```
```   820   show ?case by (iprover intro: evaln.Nil)
```
```   821 next
```
```   822   case (Cons s0 e v s1 es vs s2)
```
```   823   then obtain n1 n2 where
```
```   824     "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n1\<rightarrow> s1"
```
```   825     "G\<turnstile>s1 \<midarrow>es\<doteq>\<succ>vs\<midarrow>n2\<rightarrow> s2"
```
```   826     by iprover
```
```   827   then
```
```   828   have "G\<turnstile>Norm s0 \<midarrow>e # es\<doteq>\<succ>v # vs\<midarrow>max n1 n2\<rightarrow> s2"
```
```   829     by (blast intro!: evaln.Cons dest: evaln_max2)
```
```   830   then show ?case ..
```
```   831 qed
```
```   832
```
```   833 end
```