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