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