src/HOL/Bali/Evaln.thy
author nipkow
Mon Sep 12 07:55:43 2011 +0200 (2011-09-12)
changeset 44890 22f665a2e91c
parent 39159 0dec18004e75
child 46714 a7ca72710dfe
permissions -rw-r--r--
new fastforce replacing fastsimp - less confusing name
     1 (*  Title:      HOL/Bali/Evaln.thy
     2     Author:     David von Oheimb and Norbert Schirmer
     3 *)
     4 header {* Operational evaluation (big-step) semantics of Java expressions and 
     5           statements
     6 *}
     7 
     8 theory Evaln imports TypeSafe begin
     9 
    10 
    11 text {*
    12 Variant of @{term eval} relation with counter for bounded recursive depth. 
    13 In principal @{term evaln} could replace @{term eval}.
    14 
    15 Validity of the axiomatic semantics builds on @{term evaln}. 
    16 For recursive method calls the axiomatic semantics rule assumes the method ok 
    17 to derive a proof for the body. To prove the method rule sound we need to 
    18 perform induction on the recursion depth. 
    19 For the completeness proof of the axiomatic semantics the notion of the most
    20 general formula is used. The most general formula right now builds on the 
    21 ordinary evaluation relation @{term eval}. 
    22 So sometimes we have to switch between @{term evaln} and @{term eval} and vice 
    23 versa. To make
    24 this switch easy @{term evaln} also does all the technical accessibility tests 
    25 @{term check_field_access} and @{term check_method_access} like @{term eval}. 
    26 If it would omit them @{term evaln} and @{term eval} would only be equivalent 
    27 for welltyped, and definitely assigned terms.
    28 *}
    29 
    30 inductive
    31   evaln :: "[prog, state, term, nat, vals, state] \<Rightarrow> bool"
    32     ("_\<turnstile>_ \<midarrow>_\<succ>\<midarrow>_\<rightarrow> '(_, _')" [61,61,80,61,0,0] 60)
    33   and evarn :: "[prog, state, var, vvar, nat, state] \<Rightarrow> bool"
    34     ("_\<turnstile>_ \<midarrow>_=\<succ>_\<midarrow>_\<rightarrow> _" [61,61,90,61,61,61] 60)
    35   and eval_n:: "[prog, state, expr, val, nat, state] \<Rightarrow> bool"
    36     ("_\<turnstile>_ \<midarrow>_-\<succ>_\<midarrow>_\<rightarrow> _" [61,61,80,61,61,61] 60)
    37   and evalsn :: "[prog, state, expr list, val  list, nat, state] \<Rightarrow> bool"
    38     ("_\<turnstile>_ \<midarrow>_\<doteq>\<succ>_\<midarrow>_\<rightarrow> _" [61,61,61,61,61,61] 60)
    39   and execn     :: "[prog, state, stmt, nat, state] \<Rightarrow> bool"
    40     ("_\<turnstile>_ \<midarrow>_\<midarrow>_\<rightarrow> _"     [61,61,65,   61,61] 60)
    41   for G :: prog
    42 where
    43 
    44   "G\<turnstile>s \<midarrow>c     \<midarrow>n\<rightarrow>    s' \<equiv> G\<turnstile>s \<midarrow>In1r  c\<succ>\<midarrow>n\<rightarrow> (\<diamondsuit>    ,  s')"
    45 | "G\<turnstile>s \<midarrow>e-\<succ>v  \<midarrow>n\<rightarrow>    s' \<equiv> G\<turnstile>s \<midarrow>In1l e\<succ>\<midarrow>n\<rightarrow> (In1 v ,  s')"
    46 | "G\<turnstile>s \<midarrow>e=\<succ>vf \<midarrow>n\<rightarrow>    s' \<equiv> G\<turnstile>s \<midarrow>In2  e\<succ>\<midarrow>n\<rightarrow> (In2 vf,  s')"
    47 | "G\<turnstile>s \<midarrow>e\<doteq>\<succ>v  \<midarrow>n\<rightarrow>    s' \<equiv> G\<turnstile>s \<midarrow>In3  e\<succ>\<midarrow>n\<rightarrow> (In3 v ,  s')"
    48 
    49 --{* propagation of abrupt completion *}
    50 
    51 | Abrupt:   "G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (undefined3 t,(Some xc,s))"
    52 
    53 
    54 --{* evaluation of variables *}
    55 
    56 | LVar: "G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<midarrow>n\<rightarrow> Norm s"
    57 
    58 | FVar: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e-\<succ>a\<midarrow>n\<rightarrow> s2;
    59           (v,s2') = fvar statDeclC stat fn a s2;
    60           s3 = check_field_access G accC statDeclC fn stat a s2'\<rbrakk> \<Longrightarrow>
    61           G\<turnstile>Norm s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>v\<midarrow>n\<rightarrow> s3"
    62 
    63 | AVar: "\<lbrakk>G\<turnstile> Norm s0 \<midarrow>e1-\<succ>a\<midarrow>n\<rightarrow> s1 ; G\<turnstile>s1 \<midarrow>e2-\<succ>i\<midarrow>n\<rightarrow> s2; 
    64           (v,s2') = avar G i a s2\<rbrakk> \<Longrightarrow>
    65                       G\<turnstile>Norm s0 \<midarrow>e1.[e2]=\<succ>v\<midarrow>n\<rightarrow> s2'"
    66 
    67 
    68 
    69 
    70 --{* evaluation of expressions *}
    71 
    72 | NewC: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s1;
    73           G\<turnstile>     s1 \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s2\<rbrakk> \<Longrightarrow>
    74                                   G\<turnstile>Norm s0 \<midarrow>NewC C-\<succ>Addr a\<midarrow>n\<rightarrow> s2"
    75 
    76 | NewA: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>init_comp_ty T\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e-\<succ>i'\<midarrow>n\<rightarrow> s2; 
    77           G\<turnstile>abupd (check_neg i') s2 \<midarrow>halloc (Arr T (the_Intg i'))\<succ>a\<rightarrow> s3\<rbrakk> \<Longrightarrow>
    78                                 G\<turnstile>Norm s0 \<midarrow>New T[e]-\<succ>Addr a\<midarrow>n\<rightarrow> s3"
    79 
    80 | Cast: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1;
    81           s2 = abupd (raise_if (\<not>G,snd s1\<turnstile>v fits T) ClassCast) s1\<rbrakk> \<Longrightarrow>
    82                                 G\<turnstile>Norm s0 \<midarrow>Cast T e-\<succ>v\<midarrow>n\<rightarrow> s2"
    83 
    84 | Inst: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1;
    85           b = (v\<noteq>Null \<and> G,store s1\<turnstile>v fits RefT T)\<rbrakk> \<Longrightarrow>
    86                               G\<turnstile>Norm s0 \<midarrow>e InstOf T-\<succ>Bool b\<midarrow>n\<rightarrow> s1"
    87 
    88 | Lit:                     "G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<midarrow>n\<rightarrow> Norm s"
    89 
    90 | UnOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1\<rbrakk> 
    91          \<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>(eval_unop unop v)\<midarrow>n\<rightarrow> s1"
    92 
    93 | BinOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<midarrow>n\<rightarrow> s1; 
    94            G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then (In1l e2) else (In1r Skip))
    95             \<succ>\<midarrow>n\<rightarrow> (In1 v2,s2)\<rbrakk> 
    96          \<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<midarrow>n\<rightarrow> s2"
    97 
    98 | Super:                   "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<midarrow>n\<rightarrow> Norm s"
    99 
   100 | Acc:  "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v,f)\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   101                                   G\<turnstile>Norm s0 \<midarrow>Acc va-\<succ>v\<midarrow>n\<rightarrow> s1"
   102 
   103 | Ass:  "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(w,f)\<midarrow>n\<rightarrow> s1;
   104           G\<turnstile>     s1 \<midarrow>e-\<succ>v     \<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   105                                    G\<turnstile>Norm s0 \<midarrow>va:=e-\<succ>v\<midarrow>n\<rightarrow> assign f v s2"
   106 
   107 | Cond: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<midarrow>n\<rightarrow> s1;
   108           G\<turnstile>     s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   109                             G\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<midarrow>n\<rightarrow> s2"
   110 
   111 | Call: 
   112   "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<midarrow>n\<rightarrow> s2;
   113     D = invocation_declclass G mode (store s2) a' statT \<lparr>name=mn,parTs=pTs\<rparr>; 
   114     s3=init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' vs s2;
   115     s3' = check_method_access G accC statT mode \<lparr>name=mn,parTs=pTs\<rparr> a' s3;
   116     G\<turnstile>s3'\<midarrow>Methd D \<lparr>name=mn,parTs=pTs\<rparr>-\<succ>v\<midarrow>n\<rightarrow> s4
   117    \<rbrakk>
   118    \<Longrightarrow> 
   119     G\<turnstile>Norm s0 \<midarrow>{accC,statT,mode}e\<cdot>mn({pTs}args)-\<succ>v\<midarrow>n\<rightarrow> (restore_lvars s2 s4)"
   120 
   121 | Methd:"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   122                                 G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<midarrow>Suc n\<rightarrow> s1"
   123 
   124 | Body: "\<lbrakk>G\<turnstile>Norm s0\<midarrow>Init D\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c\<midarrow>n\<rightarrow> s2;
   125           s3 = (if (\<exists> l. abrupt s2 = Some (Jump (Break l)) \<or>  
   126                          abrupt s2 = Some (Jump (Cont l)))
   127                   then abupd (\<lambda> x. Some (Error CrossMethodJump)) s2 
   128                   else s2)\<rbrakk>\<Longrightarrow>
   129          G\<turnstile>Norm s0 \<midarrow>Body D c
   130           -\<succ>the (locals (store s2) Result)\<midarrow>n\<rightarrow>abupd (absorb Ret) s3"
   131 
   132 --{* evaluation of expression lists *}
   133 
   134 | Nil:
   135                                 "G\<turnstile>Norm s0 \<midarrow>[]\<doteq>\<succ>[]\<midarrow>n\<rightarrow> Norm s0"
   136 
   137 | Cons: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e -\<succ> v \<midarrow>n\<rightarrow> s1;
   138           G\<turnstile>     s1 \<midarrow>es\<doteq>\<succ>vs\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   139                              G\<turnstile>Norm s0 \<midarrow>e#es\<doteq>\<succ>v#vs\<midarrow>n\<rightarrow> s2"
   140 
   141 
   142 --{* execution of statements *}
   143 
   144 | Skip:                             "G\<turnstile>Norm s \<midarrow>Skip\<midarrow>n\<rightarrow> Norm s"
   145 
   146 | Expr: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   147                                   G\<turnstile>Norm s0 \<midarrow>Expr e\<midarrow>n\<rightarrow> s1"
   148 
   149 | Lab:  "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c \<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   150                              G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<midarrow>n\<rightarrow> abupd (absorb l) s1"
   151 
   152 | Comp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1 \<midarrow>n\<rightarrow> s1;
   153           G\<turnstile>     s1 \<midarrow>c2 \<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   154                                  G\<turnstile>Norm s0 \<midarrow>c1;; c2\<midarrow>n\<rightarrow> s2"
   155 
   156 | If:   "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n\<rightarrow> s1;
   157           G\<turnstile>     s1\<midarrow>(if the_Bool b then c1 else c2)\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   158                        G\<turnstile>Norm s0 \<midarrow>If(e) c1 Else c2 \<midarrow>n\<rightarrow> s2"
   159 
   160 | Loop: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n\<rightarrow> s1;
   161           if the_Bool b 
   162              then (G\<turnstile>s1 \<midarrow>c\<midarrow>n\<rightarrow> s2 \<and> 
   163                    G\<turnstile>(abupd (absorb (Cont l)) s2) \<midarrow>l\<bullet> While(e) c\<midarrow>n\<rightarrow> s3)
   164              else s3 = s1\<rbrakk> \<Longrightarrow>
   165                               G\<turnstile>Norm s0 \<midarrow>l\<bullet> While(e) c\<midarrow>n\<rightarrow> s3"
   166   
   167 | Jmp: "G\<turnstile>Norm s \<midarrow>Jmp j\<midarrow>n\<rightarrow> (Some (Jump j), s)"
   168   
   169 | Throw:"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   170                                  G\<turnstile>Norm s0 \<midarrow>Throw e\<midarrow>n\<rightarrow> abupd (throw a') s1"
   171 
   172 | Try:  "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2;
   173           if G,s2\<turnstile>catch tn then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<midarrow>n\<rightarrow> s3 else s3 = s2\<rbrakk>
   174           \<Longrightarrow>
   175                   G\<turnstile>Norm s0 \<midarrow>Try c1 Catch(tn vn) c2\<midarrow>n\<rightarrow> s3"
   176 
   177 | Fin:  "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n\<rightarrow> (x1,s1);
   178           G\<turnstile>Norm s1 \<midarrow>c2\<midarrow>n\<rightarrow> s2;
   179           s3=(if (\<exists> err. x1=Some (Error err)) 
   180               then (x1,s1) 
   181               else abupd (abrupt_if (x1\<noteq>None) x1) s2)\<rbrakk> \<Longrightarrow>
   182               G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<midarrow>n\<rightarrow> s3"
   183   
   184 | Init: "\<lbrakk>the (class G C) = c;
   185           if inited C (globs s0) then s3 = Norm s0
   186           else (G\<turnstile>Norm (init_class_obj G C s0)
   187                   \<midarrow>(if C = Object then Skip else Init (super c))\<midarrow>n\<rightarrow> s1 \<and>
   188                 G\<turnstile>set_lvars empty s1 \<midarrow>init c\<midarrow>n\<rightarrow> s2 \<and> 
   189                 s3 = restore_lvars s1 s2)\<rbrakk>
   190           \<Longrightarrow>
   191                  G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s3"
   192 monos
   193   if_bool_eq_conj
   194 
   195 
   196 declare split_if     [split del] split_if_asm     [split del]
   197         option.split [split del] option.split_asm [split del]
   198         not_None_eq [simp del] 
   199         split_paired_All [simp del] split_paired_Ex [simp del]
   200 declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
   201 
   202 inductive_cases evaln_cases: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v, s')"
   203 
   204 inductive_cases evaln_elim_cases:
   205         "G\<turnstile>(Some xc, s) \<midarrow>t                        \<succ>\<midarrow>n\<rightarrow> (v, s')"
   206         "G\<turnstile>Norm s \<midarrow>In1r Skip                      \<succ>\<midarrow>n\<rightarrow> (x, s')"
   207         "G\<turnstile>Norm s \<midarrow>In1r (Jmp j)                   \<succ>\<midarrow>n\<rightarrow> (x, s')"
   208         "G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> c)                    \<succ>\<midarrow>n\<rightarrow> (x, s')"
   209         "G\<turnstile>Norm s \<midarrow>In3  ([])                      \<succ>\<midarrow>n\<rightarrow> (v, s')"
   210         "G\<turnstile>Norm s \<midarrow>In3  (e#es)                    \<succ>\<midarrow>n\<rightarrow> (v, s')"
   211         "G\<turnstile>Norm s \<midarrow>In1l (Lit w)                   \<succ>\<midarrow>n\<rightarrow> (v, s')"
   212         "G\<turnstile>Norm s \<midarrow>In1l (UnOp unop e)             \<succ>\<midarrow>n\<rightarrow> (v, s')"
   213         "G\<turnstile>Norm s \<midarrow>In1l (BinOp binop e1 e2)       \<succ>\<midarrow>n\<rightarrow> (v, s')"
   214         "G\<turnstile>Norm s \<midarrow>In2  (LVar vn)                 \<succ>\<midarrow>n\<rightarrow> (v, s')"
   215         "G\<turnstile>Norm s \<midarrow>In1l (Cast T e)                \<succ>\<midarrow>n\<rightarrow> (v, s')"
   216         "G\<turnstile>Norm s \<midarrow>In1l (e InstOf T)              \<succ>\<midarrow>n\<rightarrow> (v, s')"
   217         "G\<turnstile>Norm s \<midarrow>In1l (Super)                   \<succ>\<midarrow>n\<rightarrow> (v, s')"
   218         "G\<turnstile>Norm s \<midarrow>In1l (Acc va)                  \<succ>\<midarrow>n\<rightarrow> (v, s')"
   219         "G\<turnstile>Norm s \<midarrow>In1r (Expr e)                  \<succ>\<midarrow>n\<rightarrow> (x, s')"
   220         "G\<turnstile>Norm s \<midarrow>In1r (c1;; c2)                 \<succ>\<midarrow>n\<rightarrow> (x, s')"
   221         "G\<turnstile>Norm s \<midarrow>In1l (Methd C sig)             \<succ>\<midarrow>n\<rightarrow> (x, s')"
   222         "G\<turnstile>Norm s \<midarrow>In1l (Body D c)                \<succ>\<midarrow>n\<rightarrow> (x, s')"
   223         "G\<turnstile>Norm s \<midarrow>In1l (e0 ? e1 : e2)            \<succ>\<midarrow>n\<rightarrow> (v, s')"
   224         "G\<turnstile>Norm s \<midarrow>In1r (If(e) c1 Else c2)        \<succ>\<midarrow>n\<rightarrow> (x, s')"
   225         "G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> While(e) c)           \<succ>\<midarrow>n\<rightarrow> (x, s')"
   226         "G\<turnstile>Norm s \<midarrow>In1r (c1 Finally c2)           \<succ>\<midarrow>n\<rightarrow> (x, s')"
   227         "G\<turnstile>Norm s \<midarrow>In1r (Throw e)                 \<succ>\<midarrow>n\<rightarrow> (x, s')"
   228         "G\<turnstile>Norm s \<midarrow>In1l (NewC C)                  \<succ>\<midarrow>n\<rightarrow> (v, s')"
   229         "G\<turnstile>Norm s \<midarrow>In1l (New T[e])                \<succ>\<midarrow>n\<rightarrow> (v, s')"
   230         "G\<turnstile>Norm s \<midarrow>In1l (Ass va e)                \<succ>\<midarrow>n\<rightarrow> (v, s')"
   231         "G\<turnstile>Norm s \<midarrow>In1r (Try c1 Catch(tn vn) c2)  \<succ>\<midarrow>n\<rightarrow> (x, s')"
   232         "G\<turnstile>Norm s \<midarrow>In2  ({accC,statDeclC,stat}e..fn) \<succ>\<midarrow>n\<rightarrow> (v, s')"
   233         "G\<turnstile>Norm s \<midarrow>In2  (e1.[e2])                 \<succ>\<midarrow>n\<rightarrow> (v, s')"
   234         "G\<turnstile>Norm s \<midarrow>In1l ({accC,statT,mode}e\<cdot>mn({pT}p)) \<succ>\<midarrow>n\<rightarrow> (v, s')"
   235         "G\<turnstile>Norm s \<midarrow>In1r (Init C)                  \<succ>\<midarrow>n\<rightarrow> (x, s')"
   236         "G\<turnstile>Norm s \<midarrow>In1r (Init C)                  \<succ>\<midarrow>n\<rightarrow> (x, s')"
   237 
   238 declare split_if     [split] split_if_asm     [split] 
   239         option.split [split] option.split_asm [split]
   240         not_None_eq [simp] 
   241         split_paired_All [simp] split_paired_Ex [simp]
   242 declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}
   243 
   244 lemma evaln_Inj_elim: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (w,s') \<Longrightarrow> case t of In1 ec \<Rightarrow>  
   245   (case ec of Inl e \<Rightarrow> (\<exists>v. w = In1 v) | Inr c \<Rightarrow> w = \<diamondsuit>)  
   246   | In2 e \<Rightarrow> (\<exists>v. w = In2 v) | In3 e \<Rightarrow> (\<exists>v. w = In3 v)"
   247 apply (erule evaln_cases , auto)
   248 apply (induct_tac "t")
   249 apply   (induct_tac "a")
   250 apply auto
   251 done
   252 
   253 text {* The following simplification procedures set up the proper injections of
   254  terms and their corresponding values in the evaluation relation:
   255  E.g. an expression 
   256  (injection @{term In1l} into terms) always evaluates to ordinary values 
   257  (injection @{term In1} into generalised values @{term vals}). 
   258 *}
   259 
   260 lemma evaln_expr_eq: "G\<turnstile>s \<midarrow>In1l t\<succ>\<midarrow>n\<rightarrow> (w, s') = (\<exists>v. w=In1 v \<and> G\<turnstile>s \<midarrow>t-\<succ>v \<midarrow>n\<rightarrow> s')"
   261   by (auto, frule evaln_Inj_elim, auto)
   262 
   263 lemma evaln_var_eq: "G\<turnstile>s \<midarrow>In2 t\<succ>\<midarrow>n\<rightarrow> (w, s') = (\<exists>vf. w=In2 vf \<and> G\<turnstile>s \<midarrow>t=\<succ>vf\<midarrow>n\<rightarrow> s')"
   264   by (auto, frule evaln_Inj_elim, auto)
   265 
   266 lemma evaln_exprs_eq: "G\<turnstile>s \<midarrow>In3 t\<succ>\<midarrow>n\<rightarrow> (w, s') = (\<exists>vs. w=In3 vs \<and> G\<turnstile>s \<midarrow>t\<doteq>\<succ>vs\<midarrow>n\<rightarrow> s')"
   267   by (auto, frule evaln_Inj_elim, auto)
   268 
   269 lemma evaln_stmt_eq: "G\<turnstile>s \<midarrow>In1r t\<succ>\<midarrow>n\<rightarrow> (w, s') = (w=\<diamondsuit> \<and> G\<turnstile>s \<midarrow>t \<midarrow>n\<rightarrow> s')"
   270   by (auto, frule evaln_Inj_elim, auto, frule evaln_Inj_elim, auto)
   271 
   272 simproc_setup evaln_expr ("G\<turnstile>s \<midarrow>In1l t\<succ>\<midarrow>n\<rightarrow> (w, s')") = {*
   273   fn _ => fn _ => fn ct =>
   274     (case Thm.term_of ct of
   275       (_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
   276     | _ => SOME (mk_meta_eq @{thm evaln_expr_eq})) *}
   277 
   278 simproc_setup evaln_var ("G\<turnstile>s \<midarrow>In2 t\<succ>\<midarrow>n\<rightarrow> (w, s')") = {*
   279   fn _ => fn _ => fn ct =>
   280     (case Thm.term_of ct of
   281       (_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
   282     | _ => SOME (mk_meta_eq @{thm evaln_var_eq})) *}
   283 
   284 simproc_setup evaln_exprs ("G\<turnstile>s \<midarrow>In3 t\<succ>\<midarrow>n\<rightarrow> (w, s')") = {*
   285   fn _ => fn _ => fn ct =>
   286     (case Thm.term_of ct of
   287       (_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
   288     | _ => SOME (mk_meta_eq @{thm evaln_exprs_eq})) *}
   289 
   290 simproc_setup evaln_stmt ("G\<turnstile>s \<midarrow>In1r t\<succ>\<midarrow>n\<rightarrow> (w, s')") = {*
   291   fn _ => fn _ => fn ct =>
   292     (case Thm.term_of ct of
   293       (_ $ _ $ _ $ _ $ _ $ (Const _ $ _) $ _) => NONE
   294     | _ => SOME (mk_meta_eq @{thm evaln_stmt_eq})) *}
   295 
   296 ML {* bind_thms ("evaln_AbruptIs", sum3_instantiate @{context} @{thm evaln.Abrupt}) *}
   297 declare evaln_AbruptIs [intro!]
   298 
   299 lemma evaln_Callee: "G\<turnstile>Norm s\<midarrow>In1l (Callee l e)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
   300 proof -
   301   { fix s t v s'
   302     assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
   303          normal: "normal s" and
   304          callee: "t=In1l (Callee l e)"
   305     then have "False" by induct auto
   306   }
   307   then show ?thesis
   308     by (cases s') fastforce 
   309 qed
   310 
   311 lemma evaln_InsInitE: "G\<turnstile>Norm s\<midarrow>In1l (InsInitE c e)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
   312 proof -
   313   { fix s t v s'
   314     assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
   315          normal: "normal s" and
   316          callee: "t=In1l (InsInitE c e)"
   317     then have "False" by induct auto
   318   }
   319   then show ?thesis
   320     by (cases s') fastforce
   321 qed
   322 
   323 lemma evaln_InsInitV: "G\<turnstile>Norm s\<midarrow>In2 (InsInitV c w)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
   324 proof -
   325   { fix s t v s'
   326     assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
   327          normal: "normal s" and
   328          callee: "t=In2 (InsInitV c w)"
   329     then have "False" by induct auto
   330   }  
   331   then show ?thesis
   332     by (cases s') fastforce
   333 qed
   334 
   335 lemma evaln_FinA: "G\<turnstile>Norm s\<midarrow>In1r (FinA a c)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
   336 proof -
   337   { fix s t v s'
   338     assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
   339          normal: "normal s" and
   340          callee: "t=In1r (FinA a c)"
   341     then have "False" by induct auto
   342   } 
   343   then show ?thesis
   344     by (cases s') fastforce
   345 qed
   346 
   347 lemma evaln_abrupt_lemma: "G\<turnstile>s \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (v,s') \<Longrightarrow> 
   348  fst s = Some xc \<longrightarrow> s' = s \<and> v = undefined3 e"
   349 apply (erule evaln_cases , auto)
   350 done
   351 
   352 lemma evaln_abrupt: 
   353  "\<And>s'. G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (w,s') = (s' = (Some xc,s) \<and>  
   354   w=undefined3 e \<and> G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (undefined3 e,(Some xc,s)))"
   355 apply auto
   356 apply (frule evaln_abrupt_lemma, auto)+
   357 done
   358 
   359 simproc_setup evaln_abrupt ("G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (w,s')") = {*
   360   fn _ => fn _ => fn ct =>
   361     (case Thm.term_of ct of
   362       (_ $ _ $ _ $ _ $ _ $ _ $ (Const (@{const_name Pair}, _) $ (Const (@{const_name Some},_) $ _)$ _))
   363         => NONE
   364     | _ => SOME (mk_meta_eq @{thm evaln_abrupt}))
   365 *}
   366 
   367 lemma evaln_LitI: "G\<turnstile>s \<midarrow>Lit v-\<succ>(if normal s then v else undefined)\<midarrow>n\<rightarrow> s"
   368 apply (case_tac "s", case_tac "a = None")
   369 by (auto intro!: evaln.Lit)
   370 
   371 lemma CondI: 
   372  "\<And>s1. \<lbrakk>G\<turnstile>s \<midarrow>e-\<succ>b\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow> 
   373   G\<turnstile>s \<midarrow>e ? e1 : e2-\<succ>(if normal s1 then v else undefined)\<midarrow>n\<rightarrow> s2"
   374 apply (case_tac "s", case_tac "a = None")
   375 by (auto intro!: evaln.Cond)
   376 
   377 lemma evaln_SkipI [intro!]: "G\<turnstile>s \<midarrow>Skip\<midarrow>n\<rightarrow> s"
   378 apply (case_tac "s", case_tac "a = None")
   379 by (auto intro!: evaln.Skip)
   380 
   381 lemma evaln_ExprI: "G\<turnstile>s \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s' \<Longrightarrow> G\<turnstile>s \<midarrow>Expr e\<midarrow>n\<rightarrow> s'"
   382 apply (case_tac "s", case_tac "a = None")
   383 by (auto intro!: evaln.Expr)
   384 
   385 lemma evaln_CompI: "\<lbrakk>G\<turnstile>s \<midarrow>c1\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c2\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow> G\<turnstile>s \<midarrow>c1;; c2\<midarrow>n\<rightarrow> s2"
   386 apply (case_tac "s", case_tac "a = None")
   387 by (auto intro!: evaln.Comp)
   388 
   389 lemma evaln_IfI: 
   390  "\<lbrakk>G\<turnstile>s \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>(if the_Bool v then c1 else c2)\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow> 
   391   G\<turnstile>s \<midarrow>If(e) c1 Else c2\<midarrow>n\<rightarrow> s2"
   392 apply (case_tac "s", case_tac "a = None")
   393 by (auto intro!: evaln.If)
   394 
   395 lemma evaln_SkipD [dest!]: "G\<turnstile>s \<midarrow>Skip\<midarrow>n\<rightarrow> s' \<Longrightarrow> s' = s" 
   396 by (erule evaln_cases, auto)
   397 
   398 lemma evaln_Skip_eq [simp]: "G\<turnstile>s \<midarrow>Skip\<midarrow>n\<rightarrow> s' = (s = s')"
   399 apply auto
   400 done
   401 
   402 
   403 
   404 
   405 section {* evaln implies eval *}
   406 
   407 lemma evaln_eval:  
   408   assumes evaln: "G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)" 
   409   shows "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"
   410 using evaln 
   411 proof (induct)
   412   case (Loop s0 e b n s1 c s2 l s3)
   413   note `G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1`
   414   moreover
   415   have "if the_Bool b
   416         then (G\<turnstile>s1 \<midarrow>c\<rightarrow> s2) \<and> 
   417              G\<turnstile>abupd (absorb (Cont l)) s2 \<midarrow>l\<bullet> While(e) c\<rightarrow> s3
   418         else s3 = s1"
   419     using Loop.hyps by simp
   420   ultimately show ?case by (rule eval.Loop)
   421 next
   422   case (Try s0 c1 n s1 s2 C vn c2 s3)
   423   note `G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1`
   424   moreover
   425   note `G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2`
   426   moreover
   427   have "if G,s2\<turnstile>catch C then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<rightarrow> s3 else s3 = s2"
   428     using Try.hyps by simp
   429   ultimately show ?case by (rule eval.Try)
   430 next
   431   case (Init C c s0 s3 n s1 s2)
   432   note `the (class G C) = c`
   433   moreover
   434   have "if inited C (globs s0) 
   435            then s3 = Norm s0
   436            else G\<turnstile>Norm ((init_class_obj G C) s0) 
   437                   \<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1 \<and>
   438                 G\<turnstile>(set_lvars empty) s1 \<midarrow>init c\<rightarrow> s2 \<and>
   439                 s3 = (set_lvars (locals (store s1))) s2"
   440     using Init.hyps by simp
   441   ultimately show ?case by (rule eval.Init)
   442 qed (rule eval.intros,(assumption+ | assumption?))+
   443 
   444 lemma Suc_le_D_lemma: "\<lbrakk>Suc n <= m'; (\<And>m. n <= m \<Longrightarrow> P (Suc m)) \<rbrakk> \<Longrightarrow> P m'"
   445 apply (frule Suc_le_D)
   446 apply fast
   447 done
   448 
   449 lemma evaln_nonstrict [rule_format (no_asm), elim]: 
   450   "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (w, s') \<Longrightarrow> \<forall>m. n\<le>m \<longrightarrow> G\<turnstile>s \<midarrow>t\<succ>\<midarrow>m\<rightarrow> (w, s')"
   451 apply (erule evaln.induct)
   452 apply (tactic {* ALLGOALS (EVERY'[strip_tac, TRY o etac @{thm Suc_le_D_lemma},
   453   REPEAT o smp_tac 1, 
   454   resolve_tac @{thms evaln.intros} THEN_ALL_NEW TRY o atac]) *})
   455 (* 3 subgoals *)
   456 apply (auto split del: split_if)
   457 done
   458 
   459 lemmas evaln_nonstrict_Suc = evaln_nonstrict [OF _ le_refl [THEN le_SucI]]
   460 
   461 lemma evaln_max2: "\<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>n1\<rightarrow> (w1, s1'); G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>n2\<rightarrow> (w2, s2')\<rbrakk> \<Longrightarrow> 
   462              G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max n1 n2\<rightarrow> (w1, s1') \<and> G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max n1 n2\<rightarrow> (w2, s2')"
   463 by (fast intro: le_maxI1 le_maxI2)
   464 
   465 corollary evaln_max2E [consumes 2]:
   466   "\<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>n1\<rightarrow> (w1, s1'); G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>n2\<rightarrow> (w2, s2'); 
   467     \<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max n1 n2\<rightarrow> (w1, s1');G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max n1 n2\<rightarrow> (w2, s2') \<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
   468 by (drule (1) evaln_max2) simp
   469 
   470 
   471 lemma evaln_max3: 
   472 "\<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>n1\<rightarrow> (w1, s1'); G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>n2\<rightarrow> (w2, s2'); G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>n3\<rightarrow> (w3, s3')\<rbrakk> \<Longrightarrow>
   473  G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> (w1, s1') \<and>
   474  G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> (w2, s2') \<and> 
   475  G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> (w3, s3')"
   476 apply (drule (1) evaln_max2, erule thin_rl)
   477 apply (fast intro!: le_maxI1 le_maxI2)
   478 done
   479 
   480 corollary evaln_max3E: 
   481 "\<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>n1\<rightarrow> (w1, s1'); G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>n2\<rightarrow> (w2, s2'); G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>n3\<rightarrow> (w3, s3');
   482    \<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> (w1, s1');
   483     G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> (w2, s2'); 
   484     G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> (w3, s3')
   485    \<rbrakk> \<Longrightarrow> P
   486   \<rbrakk> \<Longrightarrow> P"
   487 by (drule (2) evaln_max3) simp
   488 
   489 
   490 lemma le_max3I1: "(n2::nat) \<le> max n1 (max n2 n3)"
   491 proof -
   492   have "n2 \<le> max n2 n3"
   493     by (rule le_maxI1)
   494   also
   495   have "max n2 n3 \<le> max n1 (max n2 n3)"
   496     by (rule le_maxI2)
   497   finally
   498   show ?thesis .
   499 qed
   500 
   501 lemma le_max3I2: "(n3::nat) \<le> max n1 (max n2 n3)"
   502 proof -
   503   have "n3 \<le> max n2 n3"
   504     by (rule le_maxI2)
   505   also
   506   have "max n2 n3 \<le> max n1 (max n2 n3)"
   507     by (rule le_maxI2)
   508   finally
   509   show ?thesis .
   510 qed
   511 
   512 declare [[simproc del: wt_expr wt_var wt_exprs wt_stmt]]
   513 
   514 section {* eval implies evaln *}
   515 lemma eval_evaln: 
   516   assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"
   517   shows  "\<exists>n. G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)"
   518 using eval 
   519 proof (induct)
   520   case (Abrupt xc s t)
   521   obtain n where
   522     "G\<turnstile>(Some xc, s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (undefined3 t, (Some xc, s))"
   523     by (iprover intro: evaln.Abrupt)
   524   then show ?case ..
   525 next
   526   case Skip
   527   show ?case by (blast intro: evaln.Skip)
   528 next
   529   case (Expr s0 e v s1)
   530   then obtain n where
   531     "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
   532     by (iprover)
   533   then have "G\<turnstile>Norm s0 \<midarrow>Expr e\<midarrow>n\<rightarrow> s1"
   534     by (rule evaln.Expr) 
   535   then show ?case ..
   536 next
   537   case (Lab s0 c s1 l)
   538   then obtain n where
   539     "G\<turnstile>Norm s0 \<midarrow>c\<midarrow>n\<rightarrow> s1"
   540     by (iprover)
   541   then have "G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<midarrow>n\<rightarrow> abupd (absorb l) s1"
   542     by (rule evaln.Lab)
   543   then show ?case ..
   544 next
   545   case (Comp s0 c1 s1 c2 s2)
   546   then obtain n1 n2 where
   547     "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> s1"
   548     "G\<turnstile>s1 \<midarrow>c2\<midarrow>n2\<rightarrow> s2"
   549     by (iprover)
   550   then have "G\<turnstile>Norm s0 \<midarrow>c1;; c2\<midarrow>max n1 n2\<rightarrow> s2"
   551     by (blast intro: evaln.Comp dest: evaln_max2 )
   552   then show ?case ..
   553 next
   554   case (If s0 e b s1 c1 c2 s2)
   555   then obtain n1 n2 where
   556     "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n1\<rightarrow> s1"
   557     "G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<midarrow>n2\<rightarrow> s2"
   558     by (iprover)
   559   then have "G\<turnstile>Norm s0 \<midarrow>If(e) c1 Else c2\<midarrow>max n1 n2\<rightarrow> s2"
   560     by (blast intro: evaln.If dest: evaln_max2)
   561   then show ?case ..
   562 next
   563   case (Loop s0 e b s1 c s2 l s3)
   564   from Loop.hyps obtain n1 where
   565     "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n1\<rightarrow> s1"
   566     by (iprover)
   567   moreover from Loop.hyps obtain n2 where
   568     "if the_Bool b 
   569         then (G\<turnstile>s1 \<midarrow>c\<midarrow>n2\<rightarrow> s2 \<and> 
   570               G\<turnstile>(abupd (absorb (Cont l)) s2)\<midarrow>l\<bullet> While(e) c\<midarrow>n2\<rightarrow> s3)
   571         else s3 = s1"
   572     by simp (iprover intro: evaln_nonstrict le_maxI1 le_maxI2)
   573   ultimately
   574   have "G\<turnstile>Norm s0 \<midarrow>l\<bullet> While(e) c\<midarrow>max n1 n2\<rightarrow> s3"
   575     apply -
   576     apply (rule evaln.Loop)
   577     apply   (iprover intro: evaln_nonstrict intro: le_maxI1)
   578 
   579     apply   (auto intro: evaln_nonstrict intro: le_maxI2)
   580     done
   581   then show ?case ..
   582 next
   583   case (Jmp s j)
   584   fix n have "G\<turnstile>Norm s \<midarrow>Jmp j\<midarrow>n\<rightarrow> (Some (Jump j), s)"
   585     by (rule evaln.Jmp)
   586   then show ?case ..
   587 next
   588   case (Throw s0 e a s1)
   589   then obtain n where
   590     "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<midarrow>n\<rightarrow> s1"
   591     by (iprover)
   592   then have "G\<turnstile>Norm s0 \<midarrow>Throw e\<midarrow>n\<rightarrow> abupd (throw a) s1"
   593     by (rule evaln.Throw)
   594   then show ?case ..
   595 next 
   596   case (Try s0 c1 s1 s2 catchC vn c2 s3)
   597   from Try.hyps obtain n1 where
   598     "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> s1"
   599     by (iprover)
   600   moreover 
   601   note sxalloc = `G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2`
   602   moreover
   603   from Try.hyps obtain n2 where
   604     "if G,s2\<turnstile>catch catchC then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<midarrow>n2\<rightarrow> s3 else s3 = s2"
   605     by fastforce 
   606   ultimately
   607   have "G\<turnstile>Norm s0 \<midarrow>Try c1 Catch(catchC vn) c2\<midarrow>max n1 n2\<rightarrow> s3"
   608     by (auto intro!: evaln.Try le_maxI1 le_maxI2)
   609   then show ?case ..
   610 next
   611   case (Fin s0 c1 x1 s1 c2 s2 s3)
   612   from Fin obtain n1 n2 where 
   613     "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> (x1, s1)"
   614     "G\<turnstile>Norm s1 \<midarrow>c2\<midarrow>n2\<rightarrow> s2"
   615     by iprover
   616   moreover
   617   note s3 = `s3 = (if \<exists>err. x1 = Some (Error err) 
   618                    then (x1, s1)
   619                    else abupd (abrupt_if (x1 \<noteq> None) x1) s2)`
   620   ultimately 
   621   have 
   622     "G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<midarrow>max n1 n2\<rightarrow> s3"
   623     by (blast intro: evaln.Fin dest: evaln_max2)
   624   then show ?case ..
   625 next
   626   case (Init C c s0 s3 s1 s2)
   627   note cls = `the (class G C) = c`
   628   moreover from Init.hyps obtain n where
   629       "if inited C (globs s0) then s3 = Norm s0
   630        else (G\<turnstile>Norm (init_class_obj G C s0)
   631               \<midarrow>(if C = Object then Skip else Init (super c))\<midarrow>n\<rightarrow> s1 \<and>
   632                    G\<turnstile>set_lvars empty s1 \<midarrow>init c\<midarrow>n\<rightarrow> s2 \<and> 
   633                    s3 = restore_lvars s1 s2)"
   634     by (auto intro: evaln_nonstrict le_maxI1 le_maxI2)
   635   ultimately have "G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s3"
   636     by (rule evaln.Init)
   637   then show ?case ..
   638 next
   639   case (NewC s0 C s1 a s2)
   640   then obtain n where 
   641     "G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s1"
   642     by (iprover)
   643   with NewC 
   644   have "G\<turnstile>Norm s0 \<midarrow>NewC C-\<succ>Addr a\<midarrow>n\<rightarrow> s2"
   645     by (iprover intro: evaln.NewC)
   646   then show ?case ..
   647 next
   648   case (NewA s0 T s1 e i s2 a s3)
   649   then obtain n1 n2 where 
   650     "G\<turnstile>Norm s0 \<midarrow>init_comp_ty T\<midarrow>n1\<rightarrow> s1"
   651     "G\<turnstile>s1 \<midarrow>e-\<succ>i\<midarrow>n2\<rightarrow> s2"      
   652     by (iprover)
   653   moreover
   654   note `G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3`
   655   ultimately
   656   have "G\<turnstile>Norm s0 \<midarrow>New T[e]-\<succ>Addr a\<midarrow>max n1 n2\<rightarrow> s3"
   657     by (blast intro: evaln.NewA dest: evaln_max2)
   658   then show ?case ..
   659 next
   660   case (Cast s0 e v s1 s2 castT)
   661   then obtain n where
   662     "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
   663     by (iprover)
   664   moreover 
   665   note `s2 = abupd (raise_if (\<not> G,snd s1\<turnstile>v fits castT) ClassCast) s1`
   666   ultimately
   667   have "G\<turnstile>Norm s0 \<midarrow>Cast castT e-\<succ>v\<midarrow>n\<rightarrow> s2"
   668     by (rule evaln.Cast)
   669   then show ?case ..
   670 next
   671   case (Inst s0 e v s1 b T)
   672   then obtain n where
   673     "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
   674     by (iprover)
   675   moreover 
   676   note `b = (v \<noteq> Null \<and> G,snd s1\<turnstile>v fits RefT T)`
   677   ultimately
   678   have "G\<turnstile>Norm s0 \<midarrow>e InstOf T-\<succ>Bool b\<midarrow>n\<rightarrow> s1"
   679     by (rule evaln.Inst)
   680   then show ?case ..
   681 next
   682   case (Lit s v)
   683   fix n have "G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<midarrow>n\<rightarrow> Norm s"
   684     by (rule evaln.Lit)
   685   then show ?case ..
   686 next
   687   case (UnOp s0 e v s1 unop)
   688   then obtain n where
   689     "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
   690     by (iprover)
   691   hence "G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>eval_unop unop v\<midarrow>n\<rightarrow> s1"
   692     by (rule evaln.UnOp)
   693   then show ?case ..
   694 next
   695   case (BinOp s0 e1 v1 s1 binop e2 v2 s2)
   696   then obtain n1 n2 where 
   697     "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<midarrow>n1\<rightarrow> s1"
   698     "G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then In1l e2
   699                else In1r Skip)\<succ>\<midarrow>n2\<rightarrow> (In1 v2, s2)"    
   700     by (iprover)
   701   hence "G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<midarrow>max n1 n2
   702           \<rightarrow> s2"
   703     by (blast intro!: evaln.BinOp dest: evaln_max2)
   704   then show ?case ..
   705 next
   706   case (Super s )
   707   fix n have "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<midarrow>n\<rightarrow> Norm s"
   708     by (rule evaln.Super)
   709   then show ?case ..
   710 next
   711   case (Acc s0 va v f s1)
   712   then obtain n where
   713     "G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v, f)\<midarrow>n\<rightarrow> s1"
   714     by (iprover)
   715   then
   716   have "G\<turnstile>Norm s0 \<midarrow>Acc va-\<succ>v\<midarrow>n\<rightarrow> s1"
   717     by (rule evaln.Acc)
   718   then show ?case ..
   719 next
   720   case (Ass s0 var w f s1 e v s2)
   721   then obtain n1 n2 where 
   722     "G\<turnstile>Norm s0 \<midarrow>var=\<succ>(w, f)\<midarrow>n1\<rightarrow> s1"
   723     "G\<turnstile>s1 \<midarrow>e-\<succ>v\<midarrow>n2\<rightarrow> s2"      
   724     by (iprover)
   725   then
   726   have "G\<turnstile>Norm s0 \<midarrow>var:=e-\<succ>v\<midarrow>max n1 n2\<rightarrow> assign f v s2"
   727     by (blast intro: evaln.Ass dest: evaln_max2)
   728   then show ?case ..
   729 next
   730   case (Cond s0 e0 b s1 e1 e2 v s2)
   731   then obtain n1 n2 where 
   732     "G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<midarrow>n1\<rightarrow> s1"
   733     "G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<midarrow>n2\<rightarrow> s2"
   734     by (iprover)
   735   then
   736   have "G\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<midarrow>max n1 n2\<rightarrow> s2"
   737     by (blast intro: evaln.Cond dest: evaln_max2)
   738   then show ?case ..
   739 next
   740   case (Call s0 e a' s1 args vs s2 invDeclC mode statT mn pTs' s3 s3' accC' v s4)
   741   then obtain n1 n2 where
   742     "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n1\<rightarrow> s1"
   743     "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<midarrow>n2\<rightarrow> s2"
   744     by iprover
   745   moreover
   746   note `invDeclC = invocation_declclass G mode (store s2) a' statT 
   747                        \<lparr>name=mn,parTs=pTs'\<rparr>`
   748   moreover
   749   note `s3 = init_lvars G invDeclC \<lparr>name=mn,parTs=pTs'\<rparr> mode a' vs s2`
   750   moreover
   751   note `s3'=check_method_access G accC' statT mode \<lparr>name=mn,parTs=pTs'\<rparr> a' s3`
   752   moreover 
   753   from Call.hyps
   754   obtain m where 
   755     "G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name=mn, parTs=pTs'\<rparr>-\<succ>v\<midarrow>m\<rightarrow> s4"
   756     by iprover
   757   ultimately
   758   have "G\<turnstile>Norm s0 \<midarrow>{accC',statT,mode}e\<cdot>mn( {pTs'}args)-\<succ>v\<midarrow>max n1 (max n2 m)\<rightarrow> 
   759             (set_lvars (locals (store s2))) s4"
   760     by (auto intro!: evaln.Call le_maxI1 le_max3I1 le_max3I2)
   761   thus ?case ..
   762 next
   763   case (Methd s0 D sig v s1)
   764   then obtain n where
   765     "G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<midarrow>n\<rightarrow> s1"
   766     by iprover
   767   then have "G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<midarrow>Suc n\<rightarrow> s1"
   768     by (rule evaln.Methd)
   769   then show ?case ..
   770 next
   771   case (Body s0 D s1 c s2 s3)
   772   from Body.hyps obtain n1 n2 where 
   773     evaln_init: "G\<turnstile>Norm s0 \<midarrow>Init D\<midarrow>n1\<rightarrow> s1" and
   774     evaln_c: "G\<turnstile>s1 \<midarrow>c\<midarrow>n2\<rightarrow> s2"
   775     by (iprover)
   776   moreover
   777   note `s3 = (if \<exists>l. fst s2 = Some (Jump (Break l)) \<or> 
   778                      fst s2 = Some (Jump (Cont l))
   779               then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2 
   780               else s2)`
   781   ultimately
   782   have
   783      "G\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>the (locals (store s2) Result)\<midarrow>max n1 n2
   784        \<rightarrow> abupd (absorb Ret) s3"
   785     by (iprover intro: evaln.Body dest: evaln_max2)
   786   then show ?case ..
   787 next
   788   case (LVar s vn )
   789   obtain n where
   790     "G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<midarrow>n\<rightarrow> Norm s"
   791     by (iprover intro: evaln.LVar)
   792   then show ?case ..
   793 next
   794   case (FVar s0 statDeclC s1 e a s2 v s2' stat fn s3 accC)
   795   then obtain n1 n2 where
   796     "G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<midarrow>n1\<rightarrow> s1"
   797     "G\<turnstile>s1 \<midarrow>e-\<succ>a\<midarrow>n2\<rightarrow> s2"
   798     by iprover
   799   moreover
   800   note `s3 = check_field_access G accC statDeclC fn stat a s2'`
   801     and `(v, s2') = fvar statDeclC stat fn a s2`
   802   ultimately
   803   have "G\<turnstile>Norm s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>v\<midarrow>max n1 n2\<rightarrow> s3"
   804     by (iprover intro: evaln.FVar dest: evaln_max2)
   805   then show ?case ..
   806 next
   807   case (AVar s0 e1 a s1 e2 i s2 v s2')
   808   then obtain n1 n2 where 
   809     "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>a\<midarrow>n1\<rightarrow> s1"
   810     "G\<turnstile>s1 \<midarrow>e2-\<succ>i\<midarrow>n2\<rightarrow> s2"      
   811     by iprover
   812   moreover 
   813   note `(v, s2') = avar G i a s2`
   814   ultimately 
   815   have "G\<turnstile>Norm s0 \<midarrow>e1.[e2]=\<succ>v\<midarrow>max n1 n2\<rightarrow> s2'"
   816     by (blast intro!: evaln.AVar dest: evaln_max2)
   817   then show ?case ..
   818 next
   819   case (Nil s0)
   820   show ?case by (iprover intro: evaln.Nil)
   821 next
   822   case (Cons s0 e v s1 es vs s2)
   823   then obtain n1 n2 where 
   824     "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n1\<rightarrow> s1"
   825     "G\<turnstile>s1 \<midarrow>es\<doteq>\<succ>vs\<midarrow>n2\<rightarrow> s2"      
   826     by iprover
   827   then
   828   have "G\<turnstile>Norm s0 \<midarrow>e # es\<doteq>\<succ>v # vs\<midarrow>max n1 n2\<rightarrow> s2"
   829     by (blast intro!: evaln.Cons dest: evaln_max2)
   830   then show ?case ..
   831 qed
   832 
   833 end