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