src/HOL/Bali/Evaln.thy
author wenzelm
Sat Jan 02 18:48:45 2016 +0100 (2016-01-02)
changeset 62042 6c6ccf573479
parent 60754 02924903a6fd
child 62390 842917225d56
permissions -rw-r--r--
isabelle update_cartouches -c -t;
     1 (*  Title:      HOL/Bali/Evaln.thy
     2     Author:     David von Oheimb and Norbert Schirmer
     3 *)
     4 subsection \<open>Operational evaluation (big-step) semantics of Java expressions and 
     5           statements
     6 \<close>
     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 split_if     [split del] split_if_asm     [split del]
   197         option.split [split del] option.split_asm [split del]
   198         not_None_eq [simp del] 
   199         split_paired_All [simp del] split_paired_Ex [simp del]
   200 setup \<open>map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")\<close>
   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 split_if     [split] split_if_asm     [split] 
   238         option.split [split] option.split_asm [split]
   239         not_None_eq [simp] 
   240         split_paired_All [simp] split_paired_Ex [simp]
   241 declaration \<open>K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac)))\<close>
   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: 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: 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