src/HOL/Bali/Evaln.thy
author schirmer
Wed Jul 10 15:07:02 2002 +0200 (2002-07-10)
changeset 13337 f75dfc606ac7
parent 12937 0c4fd7529467
child 13384 a34e38154413
permissions -rw-r--r--
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
wenzelm@12857
     1
(*  Title:      HOL/Bali/Evaln.thy
schirmer@12854
     2
    ID:         $Id$
schirmer@12925
     3
    Author:     David von Oheimb and Norbert Schirmer
wenzelm@12859
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
schirmer@12854
     5
*)
schirmer@12854
     6
header {* Operational evaluation (big-step) semantics of Java expressions and 
schirmer@12854
     7
          statements
schirmer@12854
     8
*}
schirmer@12854
     9
schirmer@12925
    10
theory Evaln = Eval + TypeSafe:
schirmer@12854
    11
schirmer@12854
    12
text {*
schirmer@12925
    13
Variant of eval relation with counter for bounded recursive depth.
schirmer@12925
    14
Evaln omits the technical accessibility tests @{term check_field_access}
schirmer@12925
    15
and @{term check_method_access}, since we proved the absence of errors for
schirmer@12925
    16
wellformed programs.
schirmer@12854
    17
*}
schirmer@12854
    18
schirmer@12854
    19
consts
schirmer@12854
    20
schirmer@12854
    21
  evaln	:: "prog \<Rightarrow> (state \<times> term \<times> nat \<times> vals \<times> state) set"
schirmer@12854
    22
schirmer@12854
    23
syntax
schirmer@12854
    24
schirmer@12854
    25
  evaln	:: "[prog, state, term,        nat, vals * state] => bool"
schirmer@12854
    26
				("_|-_ -_>-_-> _"   [61,61,80,   61,61] 60)
schirmer@12854
    27
  evarn	:: "[prog, state, var  , vvar        , nat, state] => bool"
schirmer@12854
    28
				("_|-_ -_=>_-_-> _" [61,61,90,61,61,61] 60)
schirmer@12854
    29
  eval_n:: "[prog, state, expr , val         , nat, state] => bool"
schirmer@12854
    30
				("_|-_ -_->_-_-> _" [61,61,80,61,61,61] 60)
schirmer@12854
    31
  evalsn:: "[prog, state, expr list, val list, nat, state] => bool"
schirmer@12854
    32
				("_|-_ -_#>_-_-> _" [61,61,61,61,61,61] 60)
schirmer@12854
    33
  execn	:: "[prog, state, stmt ,               nat, state] => bool"
schirmer@12854
    34
				("_|-_ -_-_-> _"    [61,61,65,   61,61] 60)
schirmer@12854
    35
schirmer@12854
    36
syntax (xsymbols)
schirmer@12854
    37
schirmer@12854
    38
  evaln	:: "[prog, state, term,         nat, vals \<times> state] \<Rightarrow> bool"
schirmer@12854
    39
				("_\<turnstile>_ \<midarrow>_\<succ>\<midarrow>_\<rightarrow> _"   [61,61,80,   61,61] 60)
schirmer@12854
    40
  evarn	:: "[prog, state, var  , vvar         , nat, state] \<Rightarrow> bool"
schirmer@12854
    41
				("_\<turnstile>_ \<midarrow>_=\<succ>_\<midarrow>_\<rightarrow> _" [61,61,90,61,61,61] 60)
schirmer@12854
    42
  eval_n:: "[prog, state, expr , val ,          nat, state] \<Rightarrow> bool"
schirmer@12854
    43
				("_\<turnstile>_ \<midarrow>_-\<succ>_\<midarrow>_\<rightarrow> _" [61,61,80,61,61,61] 60)
schirmer@12854
    44
  evalsn:: "[prog, state, expr list, val  list, nat, state] \<Rightarrow> bool"
schirmer@12854
    45
				("_\<turnstile>_ \<midarrow>_\<doteq>\<succ>_\<midarrow>_\<rightarrow> _" [61,61,61,61,61,61] 60)
schirmer@12854
    46
  execn	:: "[prog, state, stmt ,                nat, state] \<Rightarrow> bool"
schirmer@12854
    47
				("_\<turnstile>_ \<midarrow>_\<midarrow>_\<rightarrow> _"     [61,61,65,   61,61] 60)
schirmer@12854
    48
schirmer@12854
    49
translations
schirmer@12854
    50
schirmer@12854
    51
  "G\<turnstile>s \<midarrow>t    \<succ>\<midarrow>n\<rightarrow>  w___s' " == "(s,t,n,w___s') \<in> evaln G"
schirmer@12854
    52
  "G\<turnstile>s \<midarrow>t    \<succ>\<midarrow>n\<rightarrow> (w,  s')" <= "(s,t,n,w,  s') \<in> evaln G"
schirmer@12854
    53
  "G\<turnstile>s \<midarrow>t    \<succ>\<midarrow>n\<rightarrow> (w,x,s')" <= "(s,t,n,w,x,s') \<in> evaln G"
schirmer@12854
    54
  "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
    55
  "G\<turnstile>s \<midarrow>c     \<midarrow>n\<rightarrow>    s' " == "G\<turnstile>s \<midarrow>In1r  c\<succ>\<midarrow>n\<rightarrow> (\<diamondsuit>    ,  s')"
schirmer@12854
    56
  "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
    57
  "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
    58
  "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
    59
  "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
    60
  "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
    61
  "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
    62
schirmer@12854
    63
schirmer@12854
    64
inductive "evaln G" intros
schirmer@12854
    65
schirmer@12854
    66
(* propagation of abrupt completion *)
schirmer@12854
    67
schirmer@12854
    68
  Abrupt:   "G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (arbitrary3 t,(Some xc,s))"
schirmer@12854
    69
schirmer@12854
    70
schirmer@12854
    71
(* evaluation of variables *)
schirmer@12854
    72
schirmer@12854
    73
  LVar:	"G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<midarrow>n\<rightarrow> Norm s"
schirmer@12854
    74
schirmer@12925
    75
  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@12925
    76
	  (v,s2') = fvar statDeclC stat fn a' s2\<rbrakk> \<Longrightarrow>
schirmer@12925
    77
	  G\<turnstile>Norm s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>v\<midarrow>n\<rightarrow> s2'"
schirmer@12854
    78
schirmer@12854
    79
  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
    80
	  (v,s2') = avar G i a s2\<rbrakk> \<Longrightarrow>
schirmer@12854
    81
	              G\<turnstile>Norm s0 \<midarrow>e1.[e2]=\<succ>v\<midarrow>n\<rightarrow> s2'"
schirmer@12854
    82
schirmer@12854
    83
schirmer@12854
    84
schirmer@12854
    85
schirmer@12854
    86
(* evaluation of expressions *)
schirmer@12854
    87
schirmer@12854
    88
  NewC:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s1;
schirmer@12854
    89
	  G\<turnstile>     s1 \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s2\<rbrakk> \<Longrightarrow>
schirmer@12854
    90
	                          G\<turnstile>Norm s0 \<midarrow>NewC C-\<succ>Addr a\<midarrow>n\<rightarrow> s2"
schirmer@12854
    91
schirmer@12854
    92
  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
    93
	  G\<turnstile>abupd (check_neg i') s2 \<midarrow>halloc (Arr T (the_Intg i'))\<succ>a\<rightarrow> s3\<rbrakk> \<Longrightarrow>
schirmer@12854
    94
	                        G\<turnstile>Norm s0 \<midarrow>New T[e]-\<succ>Addr a\<midarrow>n\<rightarrow> s3"
schirmer@12854
    95
schirmer@12854
    96
  Cast:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1;
schirmer@12854
    97
	  s2 = abupd (raise_if (\<not>G,snd s1\<turnstile>v fits T) ClassCast) s1\<rbrakk> \<Longrightarrow>
schirmer@12854
    98
			        G\<turnstile>Norm s0 \<midarrow>Cast T e-\<succ>v\<midarrow>n\<rightarrow> s2"
schirmer@12854
    99
schirmer@12854
   100
  Inst:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1;
schirmer@12854
   101
	  b = (v\<noteq>Null \<and> G,store s1\<turnstile>v fits RefT T)\<rbrakk> \<Longrightarrow>
schirmer@12854
   102
			      G\<turnstile>Norm s0 \<midarrow>e InstOf T-\<succ>Bool b\<midarrow>n\<rightarrow> s1"
schirmer@12854
   103
schirmer@12854
   104
  Lit:			   "G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<midarrow>n\<rightarrow> Norm s"
schirmer@12854
   105
schirmer@13337
   106
  UnOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1\<rbrakk> 
schirmer@13337
   107
         \<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>(eval_unop unop v)\<midarrow>n\<rightarrow> s1"
schirmer@13337
   108
schirmer@13337
   109
  BinOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e2-\<succ>v2\<midarrow>n\<rightarrow> s2\<rbrakk> 
schirmer@13337
   110
         \<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<midarrow>n\<rightarrow> s2"
schirmer@13337
   111
schirmer@12854
   112
  Super:		   "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<midarrow>n\<rightarrow> Norm s"
schirmer@12854
   113
schirmer@12854
   114
  Acc:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v,f)\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
schirmer@12854
   115
	                          G\<turnstile>Norm s0 \<midarrow>Acc va-\<succ>v\<midarrow>n\<rightarrow> s1"
schirmer@12854
   116
schirmer@12854
   117
  Ass:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(w,f)\<midarrow>n\<rightarrow> s1;
schirmer@12854
   118
          G\<turnstile>     s1 \<midarrow>e-\<succ>v     \<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
schirmer@12854
   119
				   G\<turnstile>Norm s0 \<midarrow>va:=e-\<succ>v\<midarrow>n\<rightarrow> assign f v s2"
schirmer@12854
   120
schirmer@12854
   121
  Cond:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<midarrow>n\<rightarrow> s1;
schirmer@12854
   122
          G\<turnstile>     s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
schirmer@12854
   123
			    G\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<midarrow>n\<rightarrow> s2"
schirmer@12854
   124
schirmer@12854
   125
  Call:	
schirmer@12854
   126
  "\<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
   127
    D = invocation_declclass G mode (store s2) a' statT \<lparr>name=mn,parTs=pTs\<rparr>; 
schirmer@12854
   128
    G\<turnstile>init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' vs s2
schirmer@12854
   129
            \<midarrow>Methd D \<lparr>name=mn,parTs=pTs\<rparr>-\<succ>v\<midarrow>n\<rightarrow> s3\<rbrakk>
schirmer@12925
   130
   \<Longrightarrow> 
schirmer@12925
   131
    G\<turnstile>Norm s0 \<midarrow>{accC,statT,mode}e\<cdot>mn({pTs}args)-\<succ>v\<midarrow>n\<rightarrow> (restore_lvars s2 s3)"
schirmer@12854
   132
schirmer@12854
   133
  Methd:"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
schirmer@12854
   134
				G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<midarrow>Suc n\<rightarrow> s1"
schirmer@12854
   135
schirmer@12854
   136
  Body:	"\<lbrakk>G\<turnstile>Norm s0\<midarrow>Init D\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c\<midarrow>n\<rightarrow> s2\<rbrakk>\<Longrightarrow>
schirmer@13337
   137
         G\<turnstile>Norm s0 \<midarrow>Body D c
schirmer@13337
   138
          -\<succ>the (locals (store s2) Result)\<midarrow>n\<rightarrow>abupd (absorb Ret) s2"
schirmer@12854
   139
schirmer@12854
   140
(* evaluation of expression lists *)
schirmer@12854
   141
schirmer@12854
   142
  Nil:
schirmer@12854
   143
				"G\<turnstile>Norm s0 \<midarrow>[]\<doteq>\<succ>[]\<midarrow>n\<rightarrow> Norm s0"
schirmer@12854
   144
schirmer@12854
   145
  Cons:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e -\<succ> v \<midarrow>n\<rightarrow> s1;
schirmer@12854
   146
          G\<turnstile>     s1 \<midarrow>es\<doteq>\<succ>vs\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
schirmer@12854
   147
			     G\<turnstile>Norm s0 \<midarrow>e#es\<doteq>\<succ>v#vs\<midarrow>n\<rightarrow> s2"
schirmer@12854
   148
schirmer@12854
   149
schirmer@12854
   150
(* execution of statements *)
schirmer@12854
   151
schirmer@12854
   152
  Skip:	 			    "G\<turnstile>Norm s \<midarrow>Skip\<midarrow>n\<rightarrow> Norm s"
schirmer@12854
   153
schirmer@12854
   154
  Expr:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
schirmer@12854
   155
				  G\<turnstile>Norm s0 \<midarrow>Expr e\<midarrow>n\<rightarrow> s1"
schirmer@12854
   156
schirmer@12854
   157
  Lab:  "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c \<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
schirmer@13337
   158
                             G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<midarrow>n\<rightarrow> abupd (absorb l) s1"
schirmer@12854
   159
schirmer@12854
   160
  Comp:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1 \<midarrow>n\<rightarrow> s1;
schirmer@12854
   161
	  G\<turnstile>     s1 \<midarrow>c2 \<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
schirmer@12854
   162
				 G\<turnstile>Norm s0 \<midarrow>c1;; c2\<midarrow>n\<rightarrow> s2"
schirmer@12854
   163
schirmer@12854
   164
  If:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n\<rightarrow> s1;
schirmer@12854
   165
	  G\<turnstile>     s1\<midarrow>(if the_Bool b then c1 else c2)\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
schirmer@12854
   166
		       G\<turnstile>Norm s0 \<midarrow>If(e) c1 Else c2 \<midarrow>n\<rightarrow> s2"
schirmer@12854
   167
schirmer@12854
   168
  Loop:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n\<rightarrow> s1;
schirmer@12854
   169
	  if normal s1 \<and> the_Bool b 
schirmer@12854
   170
             then (G\<turnstile>s1 \<midarrow>c\<midarrow>n\<rightarrow> s2 \<and> 
schirmer@12854
   171
                   G\<turnstile>(abupd (absorb (Cont l)) s2) \<midarrow>l\<bullet> While(e) c\<midarrow>n\<rightarrow> s3)
schirmer@12854
   172
	     else s3 = s1\<rbrakk> \<Longrightarrow>
schirmer@12854
   173
			      G\<turnstile>Norm s0 \<midarrow>l\<bullet> While(e) c\<midarrow>n\<rightarrow> s3"
schirmer@12854
   174
  
schirmer@12854
   175
  Do: "G\<turnstile>Norm s \<midarrow>Do j\<midarrow>n\<rightarrow> (Some (Jump j), s)"
schirmer@12854
   176
  
schirmer@12854
   177
  Throw:"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
schirmer@12854
   178
				 G\<turnstile>Norm s0 \<midarrow>Throw e\<midarrow>n\<rightarrow> abupd (throw a') s1"
schirmer@12854
   179
schirmer@12854
   180
  Try:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2;
schirmer@12854
   181
	  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
   182
          \<Longrightarrow>
schirmer@12854
   183
		  G\<turnstile>Norm s0 \<midarrow>Try c1 Catch(tn vn) c2\<midarrow>n\<rightarrow> s3"
schirmer@12854
   184
schirmer@12854
   185
  Fin:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n\<rightarrow> (x1,s1);
schirmer@12854
   186
	  G\<turnstile>Norm s1 \<midarrow>c2\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
schirmer@12854
   187
              G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<midarrow>n\<rightarrow> abupd (abrupt_if (x1\<noteq>None) x1) s2"
schirmer@12854
   188
  
schirmer@12854
   189
  Init:	"\<lbrakk>the (class G C) = c;
schirmer@12854
   190
	  if inited C (globs s0) then s3 = Norm s0
schirmer@12854
   191
	  else (G\<turnstile>Norm (init_class_obj G C s0)
schirmer@12854
   192
	          \<midarrow>(if C = Object then Skip else Init (super c))\<midarrow>n\<rightarrow> s1 \<and>
schirmer@12854
   193
	        G\<turnstile>set_lvars empty s1 \<midarrow>init c\<midarrow>n\<rightarrow> s2 \<and> 
schirmer@12854
   194
                s3 = restore_lvars s1 s2)\<rbrakk>
schirmer@12854
   195
          \<Longrightarrow>
schirmer@12854
   196
		 G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s3"
schirmer@12854
   197
monos
schirmer@12854
   198
  if_def2
schirmer@12854
   199
schirmer@12854
   200
schirmer@12854
   201
declare split_if     [split del] split_if_asm     [split del]
schirmer@12854
   202
        option.split [split del] option.split_asm [split del]
schirmer@12854
   203
inductive_cases evaln_cases: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> vs'"
schirmer@12854
   204
schirmer@12854
   205
inductive_cases evaln_elim_cases:
schirmer@12854
   206
	"G\<turnstile>(Some xc, s) \<midarrow>t                        \<succ>\<midarrow>n\<rightarrow> vs'"
schirmer@12854
   207
	"G\<turnstile>Norm s \<midarrow>In1r Skip                      \<succ>\<midarrow>n\<rightarrow> xs'"
schirmer@12854
   208
        "G\<turnstile>Norm s \<midarrow>In1r (Do j)                    \<succ>\<midarrow>n\<rightarrow> xs'"
schirmer@12854
   209
        "G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> c)                    \<succ>\<midarrow>n\<rightarrow> xs'"
schirmer@12854
   210
	"G\<turnstile>Norm s \<midarrow>In3  ([])                      \<succ>\<midarrow>n\<rightarrow> vs'"
schirmer@12854
   211
	"G\<turnstile>Norm s \<midarrow>In3  (e#es)                    \<succ>\<midarrow>n\<rightarrow> vs'"
schirmer@12854
   212
	"G\<turnstile>Norm s \<midarrow>In1l (Lit w)                   \<succ>\<midarrow>n\<rightarrow> vs'"
schirmer@13337
   213
        "G\<turnstile>Norm s \<midarrow>In1l (UnOp unop e)             \<succ>\<midarrow>n\<rightarrow> vs'"
schirmer@13337
   214
        "G\<turnstile>Norm s \<midarrow>In1l (BinOp binop e1 e2)       \<succ>\<midarrow>n\<rightarrow> vs'"
schirmer@12854
   215
	"G\<turnstile>Norm s \<midarrow>In2  (LVar vn)                 \<succ>\<midarrow>n\<rightarrow> vs'"
schirmer@12854
   216
	"G\<turnstile>Norm s \<midarrow>In1l (Cast T e)                \<succ>\<midarrow>n\<rightarrow> vs'"
schirmer@12854
   217
	"G\<turnstile>Norm s \<midarrow>In1l (e InstOf T)              \<succ>\<midarrow>n\<rightarrow> vs'"
schirmer@12854
   218
	"G\<turnstile>Norm s \<midarrow>In1l (Super)                   \<succ>\<midarrow>n\<rightarrow> vs'"
schirmer@12854
   219
	"G\<turnstile>Norm s \<midarrow>In1l (Acc va)                  \<succ>\<midarrow>n\<rightarrow> vs'"
schirmer@12854
   220
	"G\<turnstile>Norm s \<midarrow>In1r (Expr e)                  \<succ>\<midarrow>n\<rightarrow> xs'"
schirmer@12854
   221
	"G\<turnstile>Norm s \<midarrow>In1r (c1;; c2)                 \<succ>\<midarrow>n\<rightarrow> xs'"
schirmer@12854
   222
	"G\<turnstile>Norm s \<midarrow>In1l (Methd C sig)             \<succ>\<midarrow>n\<rightarrow> xs'"
schirmer@12854
   223
	"G\<turnstile>Norm s \<midarrow>In1l (Body D c)                \<succ>\<midarrow>n\<rightarrow> xs'"
schirmer@12854
   224
	"G\<turnstile>Norm s \<midarrow>In1l (e0 ? e1 : e2)            \<succ>\<midarrow>n\<rightarrow> vs'"
schirmer@12854
   225
	"G\<turnstile>Norm s \<midarrow>In1r (If(e) c1 Else c2)        \<succ>\<midarrow>n\<rightarrow> xs'"
schirmer@12854
   226
	"G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> While(e) c)           \<succ>\<midarrow>n\<rightarrow> xs'"
schirmer@12854
   227
	"G\<turnstile>Norm s \<midarrow>In1r (c1 Finally c2)           \<succ>\<midarrow>n\<rightarrow> xs'"
schirmer@12854
   228
	"G\<turnstile>Norm s \<midarrow>In1r (Throw e)                 \<succ>\<midarrow>n\<rightarrow> xs'"
schirmer@12854
   229
	"G\<turnstile>Norm s \<midarrow>In1l (NewC C)                  \<succ>\<midarrow>n\<rightarrow> vs'"
schirmer@12854
   230
	"G\<turnstile>Norm s \<midarrow>In1l (New T[e])                \<succ>\<midarrow>n\<rightarrow> vs'"
schirmer@12854
   231
	"G\<turnstile>Norm s \<midarrow>In1l (Ass va e)                \<succ>\<midarrow>n\<rightarrow> vs'"
schirmer@12854
   232
	"G\<turnstile>Norm s \<midarrow>In1r (Try c1 Catch(tn vn) c2)  \<succ>\<midarrow>n\<rightarrow> xs'"
schirmer@12925
   233
	"G\<turnstile>Norm s \<midarrow>In2  ({accC,statDeclC,stat}e..fn) \<succ>\<midarrow>n\<rightarrow> vs'"
schirmer@12854
   234
	"G\<turnstile>Norm s \<midarrow>In2  (e1.[e2])                 \<succ>\<midarrow>n\<rightarrow> vs'"
schirmer@12925
   235
	"G\<turnstile>Norm s \<midarrow>In1l ({accC,statT,mode}e\<cdot>mn({pT}p)) \<succ>\<midarrow>n\<rightarrow> vs'"
schirmer@12854
   236
	"G\<turnstile>Norm s \<midarrow>In1r (Init C)                  \<succ>\<midarrow>n\<rightarrow> xs'"
schirmer@12854
   237
declare split_if     [split] split_if_asm     [split] 
schirmer@12854
   238
        option.split [split] option.split_asm [split]
schirmer@12854
   239
schirmer@12854
   240
lemma evaln_Inj_elim: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (w,s') \<Longrightarrow> case t of In1 ec \<Rightarrow>  
schirmer@12854
   241
  (case ec of Inl e \<Rightarrow> (\<exists>v. w = In1 v) | Inr c \<Rightarrow> w = \<diamondsuit>)  
schirmer@12854
   242
  | In2 e \<Rightarrow> (\<exists>v. w = In2 v) | In3 e \<Rightarrow> (\<exists>v. w = In3 v)"
schirmer@12854
   243
apply (erule evaln_cases , auto)
schirmer@12854
   244
apply (induct_tac "t")
schirmer@12854
   245
apply   (induct_tac "a")
schirmer@12854
   246
apply auto
schirmer@12854
   247
done
schirmer@12854
   248
schirmer@12854
   249
ML_setup {*
schirmer@12854
   250
fun enf nam inj rhs =
schirmer@12854
   251
let
schirmer@12854
   252
  val name = "evaln_" ^ nam ^ "_eq"
schirmer@12854
   253
  val lhs = "G\<turnstile>s \<midarrow>" ^ inj ^ " t\<succ>\<midarrow>n\<rightarrow> (w, s')"
schirmer@12854
   254
  val () = qed_goal name (the_context()) (lhs ^ " = (" ^ rhs ^ ")") 
schirmer@12854
   255
	(K [Auto_tac, ALLGOALS (ftac (thm "evaln_Inj_elim")) THEN Auto_tac])
schirmer@12854
   256
  fun is_Inj (Const (inj,_) $ _) = true
schirmer@12854
   257
    | is_Inj _                   = false
schirmer@12854
   258
  fun pred (_ $ (Const ("Pair",_) $ _ $ (Const ("Pair", _) $ _ $ 
schirmer@12854
   259
    (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ x $ _ )))) $ _ ) = is_Inj x
schirmer@12854
   260
in
schirmer@12854
   261
  make_simproc name lhs pred (thm name)
schirmer@12854
   262
end;
schirmer@12854
   263
schirmer@12854
   264
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
   265
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
   266
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
   267
val evaln_stmt_proc = enf "stmt" "In1r" "     w=\<diamondsuit>      \<and> G\<turnstile>s \<midarrow>t     \<midarrow>n\<rightarrow> s'";
schirmer@12854
   268
Addsimprocs [evaln_expr_proc,evaln_var_proc,evaln_exprs_proc,evaln_stmt_proc];
schirmer@12854
   269
schirmer@12854
   270
bind_thms ("evaln_AbruptIs", sum3_instantiate (thm "evaln.Abrupt"))
schirmer@12854
   271
*}
schirmer@12854
   272
declare evaln_AbruptIs [intro!]
schirmer@12854
   273
schirmer@13337
   274
lemma evaln_Callee: "G\<turnstile>Norm s\<midarrow>In1l (Callee l e)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
schirmer@13337
   275
proof -
schirmer@13337
   276
  { fix s t v s'
schirmer@13337
   277
    assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
schirmer@13337
   278
         normal: "normal s" and
schirmer@13337
   279
         callee: "t=In1l (Callee l e)"
schirmer@13337
   280
    then have "False"
schirmer@13337
   281
    proof (induct)
schirmer@13337
   282
    qed (auto)
schirmer@13337
   283
  }
schirmer@13337
   284
  then show ?thesis
schirmer@13337
   285
    by (cases s') fastsimp 
schirmer@13337
   286
qed
schirmer@13337
   287
schirmer@13337
   288
lemma evaln_InsInitE: "G\<turnstile>Norm s\<midarrow>In1l (InsInitE c e)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
schirmer@13337
   289
proof -
schirmer@13337
   290
  { fix s t v s'
schirmer@13337
   291
    assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
schirmer@13337
   292
         normal: "normal s" and
schirmer@13337
   293
         callee: "t=In1l (InsInitE c e)"
schirmer@13337
   294
    then have "False"
schirmer@13337
   295
    proof (induct)
schirmer@13337
   296
    qed (auto)
schirmer@13337
   297
  }
schirmer@13337
   298
  then show ?thesis
schirmer@13337
   299
    by (cases s') fastsimp
schirmer@13337
   300
qed
schirmer@13337
   301
schirmer@13337
   302
lemma evaln_InsInitV: "G\<turnstile>Norm s\<midarrow>In2 (InsInitV c w)\<succ>\<midarrow>n\<rightarrow> (v,s') = False"
schirmer@13337
   303
proof -
schirmer@13337
   304
  { fix s t v s'
schirmer@13337
   305
    assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s')" and
schirmer@13337
   306
         normal: "normal s" and
schirmer@13337
   307
         callee: "t=In2 (InsInitV c w)"
schirmer@13337
   308
    then have "False"
schirmer@13337
   309
    proof (induct)
schirmer@13337
   310
    qed (auto)
schirmer@13337
   311
  }  
schirmer@13337
   312
  then show ?thesis
schirmer@13337
   313
    by (cases s') fastsimp
schirmer@13337
   314
qed
schirmer@13337
   315
schirmer@13337
   316
lemma evaln_FinA: "G\<turnstile>Norm s\<midarrow>In1r (FinA a c)\<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=In1r (FinA a c)"
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@12854
   330
lemma evaln_abrupt_lemma: "G\<turnstile>s \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (v,s') \<Longrightarrow> 
schirmer@12854
   331
 fst s = Some xc \<longrightarrow> s' = s \<and> v = arbitrary3 e"
schirmer@12854
   332
apply (erule evaln_cases , auto)
schirmer@12854
   333
done
schirmer@12854
   334
schirmer@12854
   335
lemma evaln_abrupt: 
schirmer@12854
   336
 "\<And>s'. G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (w,s') = (s' = (Some xc,s) \<and>  
schirmer@12854
   337
  w=arbitrary3 e \<and> G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (arbitrary3 e,(Some xc,s)))"
schirmer@12854
   338
apply auto
schirmer@12854
   339
apply (frule evaln_abrupt_lemma, auto)+
schirmer@12854
   340
done
schirmer@12854
   341
schirmer@12854
   342
ML {*
schirmer@12854
   343
local
wenzelm@12919
   344
  fun is_Some (Const ("Pair",_) $ (Const ("Datatype.option.Some",_) $ _)$ _) =true
schirmer@12854
   345
    | is_Some _ = false
schirmer@12854
   346
  fun pred (_ $ (Const ("Pair",_) $
schirmer@12854
   347
     _ $ (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ _ $
schirmer@12854
   348
       (Const ("Pair", _) $ _ $ x)))) $ _ ) = is_Some x
schirmer@12854
   349
in
schirmer@12854
   350
  val evaln_abrupt_proc = 
schirmer@12854
   351
 make_simproc "evaln_abrupt" "G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (w,s')" pred (thm "evaln_abrupt")
schirmer@12854
   352
end;
schirmer@12854
   353
Addsimprocs [evaln_abrupt_proc]
schirmer@12854
   354
*}
schirmer@12854
   355
schirmer@12854
   356
lemma evaln_LitI: "G\<turnstile>s \<midarrow>Lit v-\<succ>(if normal s then v else arbitrary)\<midarrow>n\<rightarrow> s"
schirmer@12854
   357
apply (case_tac "s", case_tac "a = None")
schirmer@12854
   358
by (auto intro!: evaln.Lit)
schirmer@12854
   359
schirmer@12854
   360
lemma CondI: 
schirmer@12854
   361
 "\<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
   362
  G\<turnstile>s \<midarrow>e ? e1 : e2-\<succ>(if normal s1 then v else arbitrary)\<midarrow>n\<rightarrow> s2"
schirmer@12854
   363
apply (case_tac "s", case_tac "a = None")
schirmer@12854
   364
by (auto intro!: evaln.Cond)
schirmer@12854
   365
schirmer@12854
   366
lemma evaln_SkipI [intro!]: "G\<turnstile>s \<midarrow>Skip\<midarrow>n\<rightarrow> s"
schirmer@12854
   367
apply (case_tac "s", case_tac "a = None")
schirmer@12854
   368
by (auto intro!: evaln.Skip)
schirmer@12854
   369
schirmer@12854
   370
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
   371
apply (case_tac "s", case_tac "a = None")
schirmer@12854
   372
by (auto intro!: evaln.Expr)
schirmer@12854
   373
schirmer@12854
   374
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
   375
apply (case_tac "s", case_tac "a = None")
schirmer@12854
   376
by (auto intro!: evaln.Comp)
schirmer@12854
   377
schirmer@12854
   378
lemma evaln_IfI: 
schirmer@12854
   379
 "\<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
   380
  G\<turnstile>s \<midarrow>If(e) c1 Else c2\<midarrow>n\<rightarrow> s2"
schirmer@12854
   381
apply (case_tac "s", case_tac "a = None")
schirmer@12854
   382
by (auto intro!: evaln.If)
schirmer@12854
   383
schirmer@12854
   384
lemma evaln_SkipD [dest!]: "G\<turnstile>s \<midarrow>Skip\<midarrow>n\<rightarrow> s' \<Longrightarrow> s' = s" 
schirmer@12854
   385
by (erule evaln_cases, auto)
schirmer@12854
   386
schirmer@12854
   387
lemma evaln_Skip_eq [simp]: "G\<turnstile>s \<midarrow>Skip\<midarrow>n\<rightarrow> s' = (s = s')"
schirmer@12854
   388
apply auto
schirmer@12854
   389
done
schirmer@12854
   390
schirmer@12925
   391
lemma evaln_eval:  
wenzelm@12937
   392
  assumes evaln: "G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)" and
schirmer@12925
   393
             wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T" and  
schirmer@12925
   394
        conf_s0: "s0\<Colon>\<preceq>(G, L)" and
schirmer@12925
   395
             wf: "wf_prog G" 
schirmer@12925
   396
       
wenzelm@12937
   397
  shows "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"
schirmer@12925
   398
proof -
schirmer@12925
   399
  from evaln 
schirmer@12925
   400
  show "\<And> L accC T. \<lbrakk>s0\<Colon>\<preceq>(G, L);\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T\<rbrakk>
schirmer@12925
   401
                    \<Longrightarrow> G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"
schirmer@12925
   402
       (is "PROP ?EqEval s0 s1 t v")
schirmer@12925
   403
  proof (induct)
schirmer@12925
   404
    case Abrupt
schirmer@12925
   405
    show ?case by (rule eval.Abrupt)
schirmer@12925
   406
  next
schirmer@12925
   407
    case LVar
schirmer@12925
   408
    show ?case by (rule eval.LVar)
schirmer@12925
   409
  next
schirmer@12925
   410
    case (FVar a accC' e fn n s0 s1 s2 s2' stat statDeclC v L accC T)
schirmer@12925
   411
    have eval_initn: "G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<midarrow>n\<rightarrow> s1" .
schirmer@12925
   412
    have eval_en: "G\<turnstile>s1 \<midarrow>e-\<succ>a\<midarrow>n\<rightarrow> s2" .
schirmer@12925
   413
    have hyp_init: "PROP ?EqEval (Norm s0) s1 (In1r (Init statDeclC)) \<diamondsuit>" .
schirmer@12925
   414
    have hyp_e: "PROP ?EqEval s1 s2 (In1l e) (In1 a)" .
schirmer@12925
   415
    have fvar: "(v, s2') = fvar statDeclC stat fn a s2" .
schirmer@12925
   416
    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
schirmer@12925
   417
    have wt: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>In2 ({accC',statDeclC,stat}e..fn)\<Colon>T" .
schirmer@12925
   418
    then obtain statC f where
schirmer@12925
   419
                wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-Class statC" and
schirmer@12925
   420
            accfield: "accfield G accC statC fn = Some (statDeclC,f)" and
schirmer@12925
   421
                stat: "stat=is_static f" and
schirmer@12925
   422
               accC': "accC'=accC" and
schirmer@12925
   423
	           T: "T=(Inl (type f))"
schirmer@12925
   424
       by (rule wt_elim_cases) (auto simp add: member_is_static_simp)
schirmer@12925
   425
    from wf wt_e 
schirmer@12925
   426
    have iscls_statC: "is_class G statC"
schirmer@12925
   427
      by (auto dest: ty_expr_is_type type_is_class)
schirmer@12925
   428
    with wf accfield 
schirmer@12925
   429
    have iscls_statDeclC: "is_class G statDeclC"
schirmer@12925
   430
      by (auto dest!: accfield_fields dest: fields_declC)
schirmer@12925
   431
    then 
schirmer@12925
   432
    have wt_init: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>(Init statDeclC)\<Colon>\<surd>"
schirmer@12925
   433
      by simp
schirmer@12925
   434
    from conf_s0 wt_init
schirmer@12925
   435
    have eval_init: "G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<rightarrow> s1"
schirmer@12925
   436
      by (rule hyp_init)
schirmer@12925
   437
    with wt_init conf_s0 wf 
schirmer@12925
   438
    have conf_s1: "s1\<Colon>\<preceq>(G, L)"
schirmer@12925
   439
      by (blast dest: exec_ts)
schirmer@12925
   440
    with hyp_e wt_e
schirmer@12925
   441
    have eval_e: "G\<turnstile>s1 \<midarrow>e-\<succ>a\<rightarrow> s2"
schirmer@12925
   442
      by blast
schirmer@12925
   443
    with wf conf_s1 wt_e
schirmer@12925
   444
    obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and
schirmer@12925
   445
            conf_a: "normal s2 \<longrightarrow> G,store s2\<turnstile>a\<Colon>\<preceq>Class statC"
schirmer@12925
   446
      by (auto dest!: eval_type_sound)
schirmer@12925
   447
    obtain s3 where
schirmer@12925
   448
      check: "s3 = check_field_access G accC statDeclC fn stat a s2'"
schirmer@12925
   449
      by simp
schirmer@12925
   450
    from accfield wt_e eval_init eval_e conf_s2 conf_a fvar stat check  wf
schirmer@12925
   451
    have eq_s3_s2': "s3=s2'"  
schirmer@12925
   452
      by (auto dest!: error_free_field_access)
schirmer@12925
   453
    with eval_init eval_e fvar check accC'
schirmer@12925
   454
    show "G\<turnstile>Norm s0 \<midarrow>{accC',statDeclC,stat}e..fn=\<succ>v\<rightarrow> s2'"
schirmer@12925
   455
      by (auto intro: eval.FVar)
schirmer@12925
   456
  next
schirmer@12925
   457
    case AVar
schirmer@12925
   458
    with wf show ?case
schirmer@12925
   459
      apply -
schirmer@12925
   460
      apply (erule wt_elim_cases)
schirmer@12925
   461
      apply (blast intro!: eval.AVar dest: eval_type_sound)
schirmer@12925
   462
      done
schirmer@12925
   463
  next
schirmer@12925
   464
    case NewC
schirmer@12925
   465
    with wf show ?case
schirmer@12925
   466
      apply - 
schirmer@12925
   467
      apply (erule wt_elim_cases)
schirmer@12925
   468
      apply (blast intro!: eval.NewC dest: eval_type_sound is_acc_classD)
schirmer@12925
   469
      done
schirmer@12925
   470
  next
schirmer@12925
   471
    case (NewA T a e i n s0 s1 s2 s3 L accC Ta) 
schirmer@12925
   472
    have hyp_init: "PROP ?EqEval (Norm s0) s1 (In1r (init_comp_ty T)) \<diamondsuit>" .
schirmer@12925
   473
    have hyp_size: "PROP ?EqEval s1 s2 (In1l e) (In1 i)" .
schirmer@12925
   474
    have "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (New T[e])\<Colon>Ta" .
schirmer@12925
   475
    then obtain
schirmer@12925
   476
       wt_init: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>init_comp_ty T\<Colon>\<surd>" and
schirmer@12925
   477
       wt_size: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-PrimT Integer"
schirmer@12925
   478
      by (rule wt_elim_cases) (auto intro: wt_init_comp_ty dest: is_acc_typeD)
schirmer@12925
   479
    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
schirmer@12925
   480
    from this wt_init 
schirmer@12925
   481
    have eval_init: "G\<turnstile>Norm s0 \<midarrow>init_comp_ty T\<rightarrow> s1"
schirmer@12925
   482
      by (rule hyp_init)
schirmer@12925
   483
    moreover
schirmer@12925
   484
    from eval_init wt_init wf conf_s0
schirmer@12925
   485
    have "s1\<Colon>\<preceq>(G, L)"
schirmer@12925
   486
      by (auto dest: eval_type_sound)
schirmer@12925
   487
    from this wt_size 
schirmer@12925
   488
    have "G\<turnstile>s1 \<midarrow>e-\<succ>i\<rightarrow> s2"
schirmer@12925
   489
      by (rule hyp_size)
schirmer@12925
   490
    moreover note NewA
schirmer@12925
   491
    ultimately show ?case
schirmer@12925
   492
      by (blast intro!: eval.NewA)
schirmer@12925
   493
  next
schirmer@12925
   494
    case Cast
schirmer@12925
   495
    with wf show ?case
schirmer@12925
   496
      by - (erule wt_elim_cases, rule eval.Cast,auto dest: eval_type_sound)
schirmer@12925
   497
  next
schirmer@12925
   498
    case Inst
schirmer@12925
   499
    with wf show ?case
schirmer@12925
   500
      by - (erule wt_elim_cases, rule eval.Inst,auto dest: eval_type_sound)
schirmer@12925
   501
  next
schirmer@12925
   502
    case Lit
schirmer@12925
   503
    show ?case by (rule eval.Lit)
schirmer@12925
   504
  next
schirmer@13337
   505
    case UnOp
schirmer@13337
   506
    with wf show ?case
schirmer@13337
   507
      by - (erule wt_elim_cases, rule eval.UnOp,auto dest: eval_type_sound)
schirmer@13337
   508
  next
schirmer@13337
   509
    case BinOp
schirmer@13337
   510
    with wf show ?case
schirmer@13337
   511
      by - (erule wt_elim_cases, blast intro!: eval.BinOp dest: eval_type_sound)
schirmer@13337
   512
  next
schirmer@12925
   513
    case Super
schirmer@12925
   514
    show ?case by (rule eval.Super)
schirmer@12925
   515
  next
schirmer@12925
   516
    case Acc
schirmer@12925
   517
    then show ?case
schirmer@12925
   518
      by - (erule wt_elim_cases, rule eval.Acc,auto dest: eval_type_sound)
schirmer@12925
   519
  next
schirmer@12925
   520
    case Ass
schirmer@12925
   521
    with wf show ?case
schirmer@12925
   522
      by - (erule wt_elim_cases, blast intro!: eval.Ass dest: eval_type_sound) 
schirmer@12925
   523
  next
schirmer@12925
   524
    case (Cond b e0 e1 e2 n s0 s1 s2 v L accC T)
schirmer@12925
   525
    have hyp_e0: "PROP ?EqEval (Norm s0) s1 (In1l e0) (In1 b)" .
schirmer@12925
   526
    have hyp_if: "PROP ?EqEval s1 s2 
schirmer@12925
   527
                              (In1l (if the_Bool b then e1 else e2)) (In1 v)" .
schirmer@12925
   528
    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
schirmer@12925
   529
    have wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (e0 ? e1 : e2)\<Colon>T" .
schirmer@12925
   530
    then obtain T1 T2 statT where
schirmer@12925
   531
       wt_e0: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e0\<Colon>-PrimT Boolean" and
schirmer@12925
   532
       wt_e1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e1\<Colon>-T1" and
schirmer@12925
   533
       wt_e2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e2\<Colon>-T2" and 
schirmer@12925
   534
       statT: "G\<turnstile>T1\<preceq>T2 \<and> statT = T2  \<or>  G\<turnstile>T2\<preceq>T1 \<and> statT =  T1" and
schirmer@12925
   535
       T    : "T=Inl statT"
schirmer@12925
   536
      by (rule wt_elim_cases) auto
schirmer@12925
   537
    from conf_s0 wt_e0
schirmer@12925
   538
    have eval_e0: "G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1"
schirmer@12925
   539
      by (rule hyp_e0)
schirmer@12925
   540
    moreover
schirmer@12925
   541
    from eval_e0 conf_s0 wf wt_e0
schirmer@12925
   542
    have "s1\<Colon>\<preceq>(G, L)"
schirmer@12925
   543
      by (blast dest: eval_type_sound)
schirmer@12925
   544
    with wt_e1 wt_e2 statT hyp_if
schirmer@12925
   545
    have "G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<rightarrow> s2"
schirmer@12925
   546
      by (cases "the_Bool b") auto
schirmer@12925
   547
    ultimately
schirmer@12925
   548
    show ?case
schirmer@12925
   549
      by (rule eval.Cond)
schirmer@12925
   550
  next
schirmer@12925
   551
    case (Call invDeclC a' accC' args e mn mode n pTs' s0 s1 s2 s4 statT 
schirmer@12925
   552
           v vs L accC T)
wenzelm@12937
   553
    txt {* Repeats large parts of the type soundness proof. One should factor
wenzelm@12937
   554
      out some lemmata about the relations and conformance of @{text
wenzelm@12937
   555
      s2}, @{text s3} and @{text s3'} *}
schirmer@12925
   556
    have evaln_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n\<rightarrow> s1" .
schirmer@12925
   557
    have evaln_args: "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<midarrow>n\<rightarrow> s2" .
schirmer@12925
   558
    have invDeclC: "invDeclC 
schirmer@12925
   559
                      = invocation_declclass G mode (store s2) a' statT 
schirmer@12925
   560
                           \<lparr>name = mn, parTs = pTs'\<rparr>" .
schirmer@12925
   561
    let ?InitLvars 
schirmer@12925
   562
         = "init_lvars G invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> mode a' vs s2"
schirmer@12925
   563
    obtain s3 s3' where 
schirmer@12925
   564
      init_lvars: "s3 = 
schirmer@12925
   565
             init_lvars G invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> mode a' vs s2" and
schirmer@12925
   566
      check: "s3' =
schirmer@12925
   567
         check_method_access G accC' statT mode \<lparr>name = mn, parTs = pTs'\<rparr> a' s3"
schirmer@12925
   568
      by simp
schirmer@12925
   569
    have evaln_methd: 
schirmer@13337
   570
     "G\<turnstile>?InitLvars \<midarrow>Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>-\<succ>v\<midarrow>n\<rightarrow> s4" .
schirmer@12925
   571
    have     hyp_e: "PROP ?EqEval (Norm s0) s1 (In1l e) (In1 a')" .
schirmer@12925
   572
    have  hyp_args: "PROP ?EqEval s1 s2 (In3 args) (In3 vs)" .
schirmer@12925
   573
    have hyp_methd: "PROP ?EqEval ?InitLvars s4 
schirmer@13337
   574
              (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)) (In1 v)".
schirmer@12925
   575
    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
schirmer@12925
   576
    have      wt: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>
schirmer@12925
   577
                    \<turnstile>In1l ({accC',statT,mode}e\<cdot>mn( {pTs'}args))\<Colon>T" .
schirmer@12925
   578
    from wt obtain pTs statDeclT statM where
schirmer@12925
   579
                 wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT" and
schirmer@12925
   580
              wt_args: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>args\<Colon>\<doteq>pTs" and
schirmer@12925
   581
                statM: "max_spec G accC statT \<lparr>name=mn,parTs=pTs\<rparr> 
schirmer@12925
   582
                         = {((statDeclT,statM),pTs')}" and
schirmer@12925
   583
                 mode: "mode = invmode statM e" and
schirmer@12925
   584
                    T: "T =Inl (resTy statM)" and
schirmer@12925
   585
        eq_accC_accC': "accC=accC'"
schirmer@12925
   586
      by (rule wt_elim_cases) auto
schirmer@12925
   587
    from conf_s0 wt_e hyp_e
schirmer@12925
   588
    have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1"
schirmer@12925
   589
      by blast
schirmer@12925
   590
    with wf conf_s0 wt_e
schirmer@12925
   591
    obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and
schirmer@12925
   592
           conf_a': "normal s1 \<Longrightarrow> G, store s1\<turnstile>a'\<Colon>\<preceq>RefT statT" 
schirmer@12925
   593
      by (auto dest!: eval_type_sound)
schirmer@12925
   594
    from conf_s1 wt_args hyp_args
schirmer@12925
   595
    have eval_args: "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<rightarrow> s2"
schirmer@12925
   596
      by blast
schirmer@12925
   597
    with wt_args conf_s1 wf 
schirmer@12925
   598
    obtain    conf_s2: "s2\<Colon>\<preceq>(G, L)" and
schirmer@12925
   599
            conf_args: "normal s2 
schirmer@12925
   600
                         \<Longrightarrow>  list_all2 (conf G (store s2)) vs pTs" 
schirmer@12925
   601
      by (auto dest!: eval_type_sound)
schirmer@12925
   602
    from statM 
schirmer@12925
   603
    obtain
schirmer@12925
   604
       statM': "(statDeclT,statM)\<in>mheads G accC statT \<lparr>name=mn,parTs=pTs'\<rparr>" and
schirmer@12925
   605
       pTs_widen: "G\<turnstile>pTs[\<preceq>]pTs'"
schirmer@12925
   606
      by (blast dest: max_spec2mheads)
schirmer@12925
   607
    from check
schirmer@12925
   608
    have eq_store_s3'_s3: "store s3'=store s3"
schirmer@12925
   609
      by (cases s3) (simp add: check_method_access_def Let_def)
schirmer@12925
   610
    obtain invC
schirmer@12925
   611
      where invC: "invC = invocation_class mode (store s2) a' statT"
schirmer@12925
   612
      by simp
schirmer@12925
   613
    with init_lvars
schirmer@12925
   614
    have invC': "invC = (invocation_class mode (store s3) a' statT)"
schirmer@12925
   615
      by (cases s2,cases mode) (auto simp add: init_lvars_def2 )
schirmer@12925
   616
    show "G\<turnstile>Norm s0 \<midarrow>{accC',statT,mode}e\<cdot>mn( {pTs'}args)
schirmer@12925
   617
             -\<succ>v\<rightarrow> (set_lvars (locals (store s2))) s4"
schirmer@12925
   618
    proof (cases "normal s2")
schirmer@12925
   619
      case False
schirmer@12925
   620
      with init_lvars 
schirmer@12925
   621
      obtain keep_abrupt: "abrupt s3 = abrupt s2" and
schirmer@12925
   622
             "store s3 = store (init_lvars G invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> 
schirmer@12925
   623
                                            mode a' vs s2)" 
schirmer@12925
   624
	by (auto simp add: init_lvars_def2)
schirmer@12925
   625
      moreover
schirmer@12925
   626
      from keep_abrupt False check
schirmer@12925
   627
      have eq_s3'_s3: "s3'=s3" 
schirmer@12925
   628
	by (auto simp add: check_method_access_def Let_def)
schirmer@12925
   629
      moreover
schirmer@12925
   630
      from eq_s3'_s3 False keep_abrupt evaln_methd init_lvars
schirmer@12925
   631
      obtain "s4=s3'"
schirmer@13337
   632
      "In1 v=arbitrary3 (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>))"
schirmer@12925
   633
	by auto
schirmer@12925
   634
      moreover note False
schirmer@12925
   635
      ultimately have
schirmer@12925
   636
	"G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>-\<succ>v\<rightarrow> s4"
schirmer@12925
   637
	by (auto)
schirmer@12925
   638
      from eval_e eval_args invDeclC init_lvars check this
schirmer@12925
   639
      show ?thesis
schirmer@12925
   640
	by (rule eval.Call)
schirmer@12925
   641
    next
schirmer@12925
   642
      case True
schirmer@12925
   643
      note normal_s2 = True
schirmer@12925
   644
      with eval_args
schirmer@12925
   645
      have normal_s1: "normal s1"
schirmer@12925
   646
	by (cases "normal s1") auto
schirmer@12925
   647
      with conf_a' eval_args 
schirmer@12925
   648
      have conf_a'_s2: "G, store s2\<turnstile>a'\<Colon>\<preceq>RefT statT"
schirmer@12925
   649
	by (auto dest: eval_gext intro: conf_gext)
schirmer@12925
   650
      show ?thesis
schirmer@12925
   651
      proof (cases "a'=Null \<longrightarrow> is_static statM")
schirmer@12925
   652
	case False
schirmer@12925
   653
	then obtain not_static: "\<not> is_static statM" and Null: "a'=Null" 
schirmer@12925
   654
	  by blast
schirmer@12925
   655
	with normal_s2 init_lvars mode
schirmer@12925
   656
	obtain np: "abrupt s3 = Some (Xcpt (Std NullPointer))" and
schirmer@12925
   657
                   "store s3 = store (init_lvars G invDeclC 
schirmer@12925
   658
                                       \<lparr>name = mn, parTs = pTs'\<rparr> mode a' vs s2)"
schirmer@12925
   659
	  by (auto simp add: init_lvars_def2)
schirmer@12925
   660
	moreover
schirmer@12925
   661
	from np check
schirmer@12925
   662
	have eq_s3'_s3: "s3'=s3" 
schirmer@12925
   663
	  by (auto simp add: check_method_access_def Let_def)
schirmer@12925
   664
	moreover
schirmer@12925
   665
	from eq_s3'_s3 np evaln_methd init_lvars
schirmer@12925
   666
	obtain "s4=s3'"
schirmer@13337
   667
      "In1 v=arbitrary3 (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>))"
schirmer@12925
   668
	  by auto
schirmer@12925
   669
	moreover note np 
schirmer@12925
   670
	ultimately have
schirmer@12925
   671
	  "G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>-\<succ>v\<rightarrow> s4"
schirmer@12925
   672
	  by (auto)
schirmer@12925
   673
	from eval_e eval_args invDeclC init_lvars check this
schirmer@12925
   674
	show ?thesis
schirmer@12925
   675
	  by (rule eval.Call)
schirmer@12925
   676
      next
schirmer@12925
   677
	case True
schirmer@12925
   678
	with mode have notNull: "mode = IntVir \<longrightarrow> a' \<noteq> Null"
schirmer@12925
   679
	  by (auto dest!: Null_staticD)
schirmer@12925
   680
	with conf_s2 conf_a'_s2 wf invC 
schirmer@12925
   681
	have dynT_prop: "G\<turnstile>mode\<rightarrow>invC\<preceq>statT"
schirmer@12925
   682
	  by (cases s2) (auto intro: DynT_propI)
schirmer@12925
   683
	with wt_e statM' invC mode wf 
schirmer@12925
   684
	obtain dynM where 
schirmer@12925
   685
           dynM: "dynlookup G statT invC  \<lparr>name=mn,parTs=pTs'\<rparr> = Some dynM" and
schirmer@12925
   686
           acc_dynM: "G \<turnstile>Methd  \<lparr>name=mn,parTs=pTs'\<rparr> dynM 
schirmer@12925
   687
                          in invC dyn_accessible_from accC"
schirmer@12925
   688
	  by (force dest!: call_access_ok)
schirmer@12925
   689
	with invC' check eq_accC_accC'
schirmer@12925
   690
	have eq_s3'_s3: "s3'=s3"
schirmer@12925
   691
	  by (auto simp add: check_method_access_def Let_def)
schirmer@12925
   692
	from dynT_prop wf wt_e statM' mode invC invDeclC dynM 
schirmer@12925
   693
	obtain 
schirmer@12925
   694
	   wf_dynM: "wf_mdecl G invDeclC (\<lparr>name=mn,parTs=pTs'\<rparr>,mthd dynM)" and
schirmer@12925
   695
	     dynM': "methd G invDeclC \<lparr>name=mn,parTs=pTs'\<rparr> = Some dynM" and
schirmer@12925
   696
           iscls_invDeclC: "is_class G invDeclC" and
schirmer@12925
   697
	        invDeclC': "invDeclC = declclass dynM" and
schirmer@12925
   698
	     invC_widen: "G\<turnstile>invC\<preceq>\<^sub>C invDeclC" and
schirmer@12925
   699
	   is_static_eq: "is_static dynM = is_static statM" and
schirmer@12925
   700
	   involved_classes_prop:
schirmer@12925
   701
             "(if invmode statM e = IntVir
schirmer@12925
   702
               then \<forall>statC. statT = ClassT statC \<longrightarrow> G\<turnstile>invC\<preceq>\<^sub>C statC
schirmer@12925
   703
               else ((\<exists>statC. statT = ClassT statC \<and> G\<turnstile>statC\<preceq>\<^sub>C invDeclC) \<or>
schirmer@12925
   704
                     (\<forall>statC. statT \<noteq> ClassT statC \<and> invDeclC = Object)) \<and>
schirmer@12925
   705
                      statDeclT = ClassT invDeclC)"
schirmer@12925
   706
	  by (auto dest: DynT_mheadsD)
schirmer@12925
   707
	obtain L' where 
schirmer@12925
   708
	   L':"L'=(\<lambda> k. 
schirmer@12925
   709
                 (case k of
schirmer@12925
   710
                    EName e
schirmer@12925
   711
                    \<Rightarrow> (case e of 
schirmer@12925
   712
                          VNam v 
schirmer@12925
   713
                          \<Rightarrow>(table_of (lcls (mbody (mthd dynM)))
schirmer@12925
   714
                             (pars (mthd dynM)[\<mapsto>]pTs')) v
schirmer@12925
   715
                        | Res \<Rightarrow> Some (resTy dynM))
schirmer@12925
   716
                  | This \<Rightarrow> if is_static statM 
schirmer@12925
   717
                            then None else Some (Class invDeclC)))"
schirmer@12925
   718
	  by simp
schirmer@12925
   719
	from wf_dynM [THEN wf_mdeclD1, THEN conjunct1] normal_s2 conf_s2 wt_e
schirmer@12925
   720
              wf eval_args conf_a' mode notNull wf_dynM involved_classes_prop
schirmer@12925
   721
	have conf_s3: "s3\<Colon>\<preceq>(G,L')"
schirmer@12925
   722
	   apply - 
schirmer@12925
   723
          (*FIXME confomrs_init_lvars should be 
schirmer@12925
   724
                adjusted to be more directy applicable *)
schirmer@12925
   725
	   apply (drule conforms_init_lvars [of G invDeclC 
schirmer@12925
   726
                  "\<lparr>name=mn,parTs=pTs'\<rparr>" dynM "store s2" vs pTs "abrupt s2" 
schirmer@12925
   727
                  L statT invC a' "(statDeclT,statM)" e])
schirmer@12925
   728
	     apply (rule wf)
schirmer@12925
   729
	     apply (rule conf_args,assumption)
schirmer@12925
   730
	     apply (simp add: pTs_widen)
schirmer@12925
   731
	     apply (cases s2,simp)
schirmer@12925
   732
	     apply (rule dynM')
schirmer@12925
   733
	     apply (force dest: ty_expr_is_type)
schirmer@12925
   734
	     apply (rule invC_widen)
schirmer@12925
   735
	     apply (force intro: conf_gext dest: eval_gext)
schirmer@12925
   736
	     apply simp
schirmer@12925
   737
	     apply simp
schirmer@12925
   738
	     apply (simp add: invC)
schirmer@12925
   739
	     apply (simp add: invDeclC)
schirmer@12925
   740
	     apply (force dest: wf_mdeclD1 is_acc_typeD)
schirmer@12925
   741
	     apply (cases s2, simp add: L' init_lvars
schirmer@12925
   742
	                      cong add: lname.case_cong ename.case_cong)
schirmer@12925
   743
	   done
schirmer@12925
   744
	from is_static_eq wf_dynM L'
schirmer@12925
   745
	obtain mthdT where
schirmer@12925
   746
	   "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>
schirmer@12925
   747
            \<turnstile>Body invDeclC (stmt (mbody (mthd dynM)))\<Colon>-mthdT" and
schirmer@12925
   748
	   mthdT_widen: "G\<turnstile>mthdT\<preceq>resTy dynM"
schirmer@12925
   749
	  by - (drule wf_mdecl_bodyD,
schirmer@13337
   750
                auto simp: cong add: lname.case_cong ename.case_cong)
schirmer@12925
   751
	with dynM' iscls_invDeclC invDeclC'
schirmer@12925
   752
	have
schirmer@12925
   753
	   "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>
schirmer@12925
   754
            \<turnstile>(Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)\<Colon>-mthdT"
schirmer@12925
   755
	  by (auto intro: wt.Methd)
schirmer@12925
   756
	with conf_s3 hyp_methd init_lvars eq_s3'_s3
schirmer@12925
   757
	have "G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>-\<succ>v\<rightarrow> s4"
schirmer@12925
   758
	  by auto
schirmer@12925
   759
	from eval_e eval_args invDeclC init_lvars check this
schirmer@12925
   760
	show ?thesis
schirmer@12925
   761
	  by (rule eval.Call)
schirmer@12925
   762
      qed
schirmer@12925
   763
    qed
schirmer@12925
   764
  next
schirmer@12925
   765
    case Methd
schirmer@12925
   766
    with wf show ?case
schirmer@12925
   767
      by - (erule wt_elim_cases, rule eval.Methd, 
schirmer@12925
   768
            auto dest: eval_type_sound simp add: body_def2)
schirmer@12925
   769
  next
schirmer@12925
   770
    case Body
schirmer@12925
   771
    with wf show ?case
schirmer@12925
   772
       by - (erule wt_elim_cases, blast intro!: eval.Body dest: eval_type_sound)
schirmer@12925
   773
  next
schirmer@12925
   774
    case Nil
schirmer@12925
   775
    show ?case by (rule eval.Nil)
schirmer@12925
   776
  next
schirmer@12925
   777
    case Cons
schirmer@12925
   778
    with wf show ?case
schirmer@12925
   779
      by - (erule wt_elim_cases, blast intro!: eval.Cons dest: eval_type_sound)
schirmer@12925
   780
  next
schirmer@12925
   781
    case Skip
schirmer@12925
   782
    show ?case by (rule eval.Skip)
schirmer@12925
   783
  next
schirmer@12925
   784
    case Expr
schirmer@12925
   785
    with wf show ?case
schirmer@12925
   786
      by - (erule wt_elim_cases, rule eval.Expr,auto dest: eval_type_sound)
schirmer@12925
   787
  next
schirmer@12925
   788
    case Lab
schirmer@12925
   789
    with wf show ?case
schirmer@12925
   790
      by - (erule wt_elim_cases, rule eval.Lab,auto dest: eval_type_sound)
schirmer@12925
   791
  next
schirmer@12925
   792
    case Comp
schirmer@12925
   793
    with wf show ?case
schirmer@12925
   794
      by - (erule wt_elim_cases, blast intro!: eval.Comp dest: eval_type_sound)
schirmer@12925
   795
  next
schirmer@12925
   796
    case (If b c1 c2 e n s0 s1 s2 L accC T)
schirmer@12925
   797
    have hyp_e: "PROP ?EqEval (Norm s0) s1 (In1l e) (In1 b)" .
schirmer@12925
   798
    have hyp_then_else: 
schirmer@12925
   799
      "PROP ?EqEval s1 s2 (In1r (if the_Bool b then c1 else c2)) \<diamondsuit>" .
schirmer@12925
   800
    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
schirmer@12925
   801
    have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (If(e) c1 Else c2)\<Colon>T" .
schirmer@12925
   802
    then obtain 
schirmer@12925
   803
              wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean" and
schirmer@12925
   804
      wt_then_else: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(if the_Bool b then c1 else c2)\<Colon>\<surd>"
schirmer@12925
   805
      by (rule wt_elim_cases) (auto split add: split_if)
schirmer@12925
   806
    from conf_s0 wt_e
schirmer@12925
   807
    have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1"
schirmer@12925
   808
      by (rule hyp_e)
schirmer@12925
   809
    moreover
schirmer@12925
   810
    from eval_e wt_e conf_s0 wf
schirmer@12925
   811
    have "s1\<Colon>\<preceq>(G, L)"
schirmer@12925
   812
      by (blast dest: eval_type_sound)
schirmer@12925
   813
    from this wt_then_else
schirmer@12925
   814
    have "G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2"
schirmer@12925
   815
      by (rule hyp_then_else)
schirmer@12925
   816
    ultimately
schirmer@12925
   817
    show ?case
schirmer@12925
   818
      by (rule eval.If)
schirmer@12925
   819
  next
schirmer@12925
   820
    case (Loop b c e l n s0 s1 s2 s3 L accC T)
schirmer@12925
   821
    have hyp_e: "PROP ?EqEval (Norm s0) s1 (In1l e) (In1 b)" .
schirmer@12925
   822
    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
schirmer@12925
   823
    have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (l\<bullet> While(e) c)\<Colon>T" .
schirmer@12925
   824
    then obtain wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean" and
schirmer@12925
   825
                wt_c: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c\<Colon>\<surd>"
schirmer@12925
   826
      by (rule wt_elim_cases) (blast)
schirmer@12925
   827
    from conf_s0 wt_e 
schirmer@12925
   828
    have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1"
schirmer@12925
   829
      by (rule hyp_e)
schirmer@12925
   830
    moreover
schirmer@12925
   831
    from eval_e wt_e conf_s0 wf
schirmer@12925
   832
    have conf_s1: "s1\<Colon>\<preceq>(G, L)"
schirmer@12925
   833
      by (blast dest: eval_type_sound)
schirmer@12925
   834
    have "if normal s1 \<and> the_Bool b 
schirmer@12925
   835
             then (G\<turnstile>s1 \<midarrow>c\<rightarrow> s2 \<and> 
schirmer@12925
   836
                   G\<turnstile>(abupd (absorb (Cont l)) s2) \<midarrow>l\<bullet> While(e) c\<rightarrow> s3)
schirmer@12925
   837
	     else s3 = s1"
schirmer@12925
   838
    proof (cases "normal s1 \<and> the_Bool b")
schirmer@12925
   839
      case True 
schirmer@12925
   840
      from Loop True have hyp_c: "PROP ?EqEval s1 s2 (In1r c) \<diamondsuit>"
schirmer@12925
   841
	by (auto)
schirmer@12925
   842
      from Loop True have hyp_w: "PROP ?EqEval (abupd (absorb (Cont l)) s2)
schirmer@12925
   843
                                        s3 (In1r (l\<bullet> While(e) c)) \<diamondsuit>"
schirmer@12925
   844
	by (auto)
schirmer@12925
   845
      from conf_s1 wt_c
schirmer@12925
   846
      have eval_c: "G\<turnstile>s1 \<midarrow>c\<rightarrow> s2"
schirmer@12925
   847
	by (rule hyp_c)
schirmer@12925
   848
      moreover
schirmer@12925
   849
      from eval_c conf_s1 wt_c wf
schirmer@12925
   850
      have "s2\<Colon>\<preceq>(G, L)"
schirmer@12925
   851
	by (blast dest: eval_type_sound)
schirmer@12925
   852
      then
schirmer@12925
   853
      have "abupd (absorb (Cont l)) s2 \<Colon>\<preceq>(G, L)"
schirmer@12925
   854
	by (cases s2) (auto intro: conforms_absorb)
schirmer@12925
   855
      from this and wt
schirmer@12925
   856
      have "G\<turnstile>abupd (absorb (Cont l)) s2 \<midarrow>l\<bullet> While(e) c\<rightarrow> s3"
schirmer@12925
   857
	by (rule hyp_w)
schirmer@12925
   858
      moreover note True
schirmer@12925
   859
      ultimately
schirmer@12925
   860
      show ?thesis
schirmer@12925
   861
	by simp
schirmer@12925
   862
    next
schirmer@12925
   863
      case False
schirmer@12925
   864
      with Loop have "s3 = s1" by simp
schirmer@12925
   865
      with False
schirmer@12925
   866
      show ?thesis 
schirmer@12925
   867
	by auto
schirmer@12925
   868
    qed
schirmer@12925
   869
    ultimately
schirmer@12925
   870
    show ?case
schirmer@12925
   871
      by (rule eval.Loop)
schirmer@12925
   872
  next
schirmer@12925
   873
    case Do
schirmer@12925
   874
    show ?case by (rule eval.Do)
schirmer@12925
   875
  next
schirmer@12925
   876
    case Throw
schirmer@12925
   877
    with wf show ?case
schirmer@12925
   878
      by - (erule wt_elim_cases, rule eval.Throw,auto dest: eval_type_sound)
schirmer@12925
   879
  next
schirmer@12925
   880
    case (Try c1 c2 n s0 s1 s2 s3 catchC vn L accC T)
schirmer@12925
   881
    have  hyp_c1: "PROP ?EqEval (Norm s0) s1 (In1r c1) \<diamondsuit>" .
schirmer@12925
   882
    have conf_s0:"Norm s0\<Colon>\<preceq>(G, L)" .
schirmer@12925
   883
    have      wt:"\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>In1r (Try c1 Catch(catchC vn) c2)\<Colon>T" .
schirmer@12925
   884
    then obtain 
schirmer@12925
   885
      wt_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
schirmer@12925
   886
      wt_c2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<lparr>lcl := L(VName vn\<mapsto>Class catchC)\<rparr>\<turnstile>c2\<Colon>\<surd>"
schirmer@12925
   887
      by (rule wt_elim_cases) (auto)
schirmer@12925
   888
    from conf_s0 wt_c1
schirmer@12925
   889
    have eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1"
schirmer@12925
   890
      by (rule hyp_c1)
schirmer@12925
   891
    moreover
schirmer@12925
   892
    have sxalloc: "G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2" .
schirmer@12925
   893
    moreover
schirmer@12925
   894
    from eval_c1 wt_c1 conf_s0 wf
schirmer@12925
   895
    have "s1\<Colon>\<preceq>(G, L)"
schirmer@12925
   896
      by (blast dest: eval_type_sound)
schirmer@12925
   897
    with sxalloc wf
schirmer@12925
   898
    have conf_s2: "s2\<Colon>\<preceq>(G, L)" 
schirmer@12925
   899
      by (auto dest: sxalloc_type_sound split: option.splits)
schirmer@12925
   900
    have "if G,s2\<turnstile>catch catchC then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<rightarrow> s3 else s3 = s2"
schirmer@12925
   901
    proof (cases "G,s2\<turnstile>catch catchC")
schirmer@12925
   902
      case True
schirmer@12925
   903
      note Catch = this
schirmer@12925
   904
      with Try have hyp_c2: "PROP ?EqEval (new_xcpt_var vn s2) s3 (In1r c2) \<diamondsuit>"
schirmer@12925
   905
	by auto
schirmer@12925
   906
      show ?thesis
schirmer@12925
   907
      proof (cases "normal s1")
schirmer@12925
   908
	case True
schirmer@12925
   909
	with sxalloc wf 
schirmer@12925
   910
	have eq_s2_s1: "s2=s1"
schirmer@12925
   911
	  by (auto dest: sxalloc_type_sound split: option.splits)
schirmer@12925
   912
	with True 
schirmer@12925
   913
	have "\<not>  G,s2\<turnstile>catch catchC"
schirmer@12925
   914
	  by (simp add: catch_def)
schirmer@12925
   915
	with Catch show ?thesis 
schirmer@12925
   916
	  by (contradiction)
schirmer@12925
   917
      next 
schirmer@12925
   918
	case False
schirmer@12925
   919
	with sxalloc wf
schirmer@12925
   920
	obtain a 
schirmer@12925
   921
	  where xcpt_s2: "abrupt s2 = Some (Xcpt (Loc a))"
schirmer@12925
   922
	  by (auto dest!: sxalloc_type_sound split: option.splits)
schirmer@12925
   923
	with Catch
schirmer@12925
   924
	have "G\<turnstile>obj_ty (the (globs (store s2) (Heap a)))\<preceq>Class catchC"
schirmer@12925
   925
	  by (cases s2) simp
schirmer@12925
   926
	with xcpt_s2 conf_s2 wf 
schirmer@12925
   927
	have "new_xcpt_var vn s2\<Colon>\<preceq>(G, L(VName vn\<mapsto>Class catchC))"
schirmer@12925
   928
	  by (auto dest: Try_lemma)
schirmer@12925
   929
	from this wt_c2
schirmer@12925
   930
	have "G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<rightarrow> s3"
schirmer@12925
   931
	  by (auto intro: hyp_c2)
schirmer@12925
   932
	with Catch 
schirmer@12925
   933
	show ?thesis
schirmer@12925
   934
	  by simp
schirmer@12925
   935
      qed
schirmer@12925
   936
    next
schirmer@12925
   937
      case False
schirmer@12925
   938
      with Try
schirmer@12925
   939
      have "s3=s2"
schirmer@12925
   940
	by simp
schirmer@12925
   941
      with False
schirmer@12925
   942
      show ?thesis
schirmer@12925
   943
	by simp
schirmer@12925
   944
    qed
schirmer@12925
   945
    ultimately
schirmer@12925
   946
    show ?case
schirmer@12925
   947
      by (rule eval.Try)
schirmer@12925
   948
  next
schirmer@13337
   949
    case (Fin c1 c2 n s0 s1 s2 x1 L accC T)
schirmer@13337
   950
    have hyp_c1: "PROP ?EqEval (Norm s0) (x1,s1) (In1r c1) \<diamondsuit>" .
schirmer@13337
   951
    have hyp_c2: "PROP ?EqEval (Norm s1) (s2) (In1r c2) \<diamondsuit>" .
schirmer@13337
   952
    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
schirmer@13337
   953
    have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (c1 Finally c2)\<Colon>T" .
schirmer@13337
   954
    then obtain
schirmer@13337
   955
      wt_c1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
schirmer@13337
   956
      wt_c2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c2\<Colon>\<surd>" 
schirmer@13337
   957
      by (rule wt_elim_cases) blast
schirmer@13337
   958
    from conf_s0 wt_c1
schirmer@13337
   959
    have eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1, s1)"
schirmer@13337
   960
      by (rule hyp_c1)
schirmer@13337
   961
    with wf wt_c1 conf_s0
schirmer@13337
   962
    obtain       conf_s1: "Norm s1\<Colon>\<preceq>(G, L)" and 
schirmer@13337
   963
           error_free_s1: "error_free (x1,s1)"
schirmer@13337
   964
      by (auto dest!: eval_type_sound intro: conforms_NormI)
schirmer@13337
   965
    from conf_s1 wt_c2
schirmer@13337
   966
    have eval_c2: "G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2"
schirmer@13337
   967
      by (rule hyp_c2)
schirmer@13337
   968
    with eval_c1 error_free_s1
schirmer@13337
   969
    show "G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<rightarrow> abupd (abrupt_if (x1 \<noteq> None) x1) s2"
schirmer@13337
   970
      by (auto intro: eval.Fin simp add: error_free_def)
schirmer@12925
   971
  next
schirmer@12925
   972
    case (Init C c n s0 s1 s2 s3 L accC T)
schirmer@12925
   973
    have     cls: "the (class G C) = c" .
schirmer@12925
   974
    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
schirmer@12925
   975
    have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (Init C)\<Colon>T" .
schirmer@12925
   976
    with cls
schirmer@12925
   977
    have cls_C: "class G C = Some c"
schirmer@12925
   978
      by - (erule wt_elim_cases,auto)
schirmer@12925
   979
    have "if inited C (globs s0) then s3 = Norm s0
schirmer@12925
   980
	  else (G\<turnstile>Norm (init_class_obj G C s0) 
schirmer@12925
   981
		  \<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1 \<and>
schirmer@12925
   982
	       G\<turnstile>set_lvars empty s1 \<midarrow>init c\<rightarrow> s2 \<and> s3 = restore_lvars s1 s2)"
schirmer@12925
   983
    proof (cases "inited C (globs s0)")
schirmer@12925
   984
      case True
schirmer@12925
   985
      with Init have "s3 = Norm s0"
schirmer@12925
   986
	by simp
schirmer@12925
   987
      with True show ?thesis 
schirmer@12925
   988
	by simp
schirmer@12925
   989
    next
schirmer@12925
   990
      case False
schirmer@12925
   991
      with Init
schirmer@12925
   992
      obtain 
schirmer@12925
   993
	hyp_init_super: 
schirmer@12925
   994
        "PROP ?EqEval (Norm ((init_class_obj G C) s0)) s1
schirmer@12925
   995
	               (In1r (if C = Object then Skip else Init (super c))) \<diamondsuit>"
schirmer@12925
   996
	and 
schirmer@12925
   997
        hyp_init_c:
schirmer@12925
   998
	   "PROP ?EqEval ((set_lvars empty) s1) s2 (In1r (init c)) \<diamondsuit>" and
schirmer@12925
   999
	s3: "s3 = (set_lvars (locals (store s1))) s2"
schirmer@12925
  1000
	by (simp only: if_False)
schirmer@12925
  1001
      from conf_s0 wf cls_C False
schirmer@12925
  1002
      have conf_s0': "(Norm ((init_class_obj G C) s0))\<Colon>\<preceq>(G, L)"
schirmer@12925
  1003
	by (auto dest: conforms_init_class_obj)
schirmer@12925
  1004
      moreover
schirmer@12925
  1005
      from wf cls_C 
schirmer@12925
  1006
      have wt_init_super:
schirmer@12925
  1007
           "\<lparr>prg = G, cls = accC, lcl = L\<rparr>
schirmer@12925
  1008
                  \<turnstile>(if C = Object then Skip else Init (super c))\<Colon>\<surd>"
schirmer@12925
  1009
	by (cases "C=Object")
schirmer@12925
  1010
           (auto dest: wf_prog_cdecl wf_cdecl_supD is_acc_classD)
schirmer@12925
  1011
      ultimately
schirmer@12925
  1012
      have eval_init_super: 
schirmer@12925
  1013
	   "G\<turnstile>Norm ((init_class_obj G C) s0) 
schirmer@12925
  1014
            \<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1"
schirmer@12925
  1015
	by (rule hyp_init_super)
schirmer@12925
  1016
      with conf_s0' wt_init_super wf
schirmer@12925
  1017
      have "s1\<Colon>\<preceq>(G, L)"
schirmer@12925
  1018
	by (blast dest: eval_type_sound)
schirmer@12925
  1019
      then
schirmer@12925
  1020
      have "(set_lvars empty) s1\<Colon>\<preceq>(G, empty)"
schirmer@12925
  1021
	by (cases s1) (auto dest: conforms_set_locals )
schirmer@12925
  1022
      with wf cls_C 
schirmer@12925
  1023
      have eval_init_c: "G\<turnstile>(set_lvars empty) s1 \<midarrow>init c\<rightarrow> s2"
schirmer@12925
  1024
	by (auto intro!: hyp_init_c dest: wf_prog_cdecl wf_cdecl_wt_init)
schirmer@12925
  1025
      from False eval_init_super eval_init_c s3
schirmer@12925
  1026
      show ?thesis
schirmer@12925
  1027
	by simp
schirmer@12925
  1028
    qed
wenzelm@12937
  1029
    with cls show ?case
schirmer@12925
  1030
      by (rule eval.Init)
schirmer@12925
  1031
  qed 
schirmer@12925
  1032
qed
schirmer@12925
  1033
schirmer@12925
  1034
lemma Suc_le_D_lemma: "\<lbrakk>Suc n <= m'; (\<And>m. n <= m \<Longrightarrow> P (Suc m)) \<rbrakk> \<Longrightarrow> P m'"
schirmer@12925
  1035
apply (frule Suc_le_D)
schirmer@12925
  1036
apply fast
schirmer@12925
  1037
done
schirmer@12925
  1038
schirmer@12925
  1039
lemma evaln_nonstrict [rule_format (no_asm), elim]: 
schirmer@12925
  1040
  "\<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
  1041
apply (simp (no_asm_simp) only: split_tupled_all)
schirmer@12925
  1042
apply (erule evaln.induct)
schirmer@12925
  1043
apply (tactic {* ALLGOALS (EVERY'[strip_tac, TRY o etac (thm "Suc_le_D_lemma"),
schirmer@12925
  1044
  REPEAT o smp_tac 1, 
schirmer@12925
  1045
  resolve_tac (thms "evaln.intros") THEN_ALL_NEW TRY o atac]) *})
schirmer@12925
  1046
(* 3 subgoals *)
schirmer@12925
  1047
apply (auto split del: split_if)
schirmer@12925
  1048
done
schirmer@12925
  1049
schirmer@12925
  1050
lemmas evaln_nonstrict_Suc = evaln_nonstrict [OF _ le_refl [THEN le_SucI]]
schirmer@12925
  1051
schirmer@12925
  1052
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
  1053
             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@12925
  1054
apply (fast intro: le_maxI1 le_maxI2)
schirmer@12925
  1055
done
schirmer@12925
  1056
schirmer@12925
  1057
lemma evaln_max3: 
schirmer@12925
  1058
"\<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
  1059
 G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> ws1 \<and>
schirmer@12925
  1060
 G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> ws2 \<and> 
schirmer@12925
  1061
 G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> ws3"
schirmer@12925
  1062
apply (drule (1) evaln_max2, erule thin_rl)
schirmer@12925
  1063
apply (fast intro!: le_maxI1 le_maxI2)
schirmer@12925
  1064
done
schirmer@12925
  1065
schirmer@12925
  1066
lemma le_max3I1: "(n2::nat) \<le> max n1 (max n2 n3)"
schirmer@12925
  1067
proof -
schirmer@12925
  1068
  have "n2 \<le> max n2 n3"
schirmer@12925
  1069
    by (rule le_maxI1)
schirmer@12925
  1070
  also
schirmer@12925
  1071
  have "max n2 n3 \<le> max n1 (max n2 n3)"
schirmer@12925
  1072
    by (rule le_maxI2)
schirmer@12925
  1073
  finally
schirmer@12925
  1074
  show ?thesis .
schirmer@12925
  1075
qed
schirmer@12925
  1076
schirmer@12925
  1077
lemma le_max3I2: "(n3::nat) \<le> max n1 (max n2 n3)"
schirmer@12925
  1078
proof -
schirmer@12925
  1079
  have "n3 \<le> max n2 n3"
schirmer@12925
  1080
    by (rule le_maxI2)
schirmer@12925
  1081
  also
schirmer@12925
  1082
  have "max n2 n3 \<le> max n1 (max n2 n3)"
schirmer@12925
  1083
    by (rule le_maxI2)
schirmer@12925
  1084
  finally
schirmer@12925
  1085
  show ?thesis .
schirmer@12925
  1086
qed
schirmer@12925
  1087
schirmer@12925
  1088
lemma eval_evaln: 
wenzelm@12937
  1089
  assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" and
wenzelm@12937
  1090
            wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T" and  
wenzelm@12937
  1091
       conf_s0: "s0\<Colon>\<preceq>(G, L)" and
wenzelm@12937
  1092
            wf: "wf_prog G"  
wenzelm@12937
  1093
  shows  "\<exists>n. G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)"
schirmer@12925
  1094
proof -
schirmer@12925
  1095
  from eval 
schirmer@12925
  1096
  show "\<And> L accC T. \<lbrakk>s0\<Colon>\<preceq>(G, L);\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T\<rbrakk>
schirmer@12925
  1097
                     \<Longrightarrow> \<exists> n. G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)"
schirmer@12925
  1098
       (is "PROP ?EqEval s0 s1 t v")
schirmer@12925
  1099
  proof (induct)
schirmer@12925
  1100
    case (Abrupt s t xc L accC T)
schirmer@12925
  1101
    obtain n where
schirmer@12925
  1102
      "G\<turnstile>(Some xc, s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (arbitrary3 t, Some xc, s)"
schirmer@12925
  1103
      by (rules intro: evaln.Abrupt)
schirmer@12925
  1104
    then show ?case ..
schirmer@12925
  1105
  next
schirmer@12925
  1106
    case Skip
schirmer@12925
  1107
    show ?case by (blast intro: evaln.Skip)
schirmer@12925
  1108
  next
schirmer@12925
  1109
    case (Expr e s0 s1 v L accC T)
schirmer@12925
  1110
    then obtain n where
schirmer@12925
  1111
      "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
schirmer@12925
  1112
      by (rules elim!: wt_elim_cases)
schirmer@12925
  1113
    then have "G\<turnstile>Norm s0 \<midarrow>Expr e\<midarrow>n\<rightarrow> s1"
schirmer@12925
  1114
      by (rule evaln.Expr) 
schirmer@12925
  1115
    then show ?case ..
schirmer@12925
  1116
  next
schirmer@12925
  1117
    case (Lab c l s0 s1 L accC T)
schirmer@12925
  1118
    then obtain n where
schirmer@12925
  1119
      "G\<turnstile>Norm s0 \<midarrow>c\<midarrow>n\<rightarrow> s1"
schirmer@12925
  1120
      by (rules elim!: wt_elim_cases)
schirmer@13337
  1121
    then have "G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<midarrow>n\<rightarrow> abupd (absorb l) s1"
schirmer@12925
  1122
      by (rule evaln.Lab)
schirmer@12925
  1123
    then show ?case ..
schirmer@12925
  1124
  next
schirmer@12925
  1125
    case (Comp c1 c2 s0 s1 s2 L accC T)
schirmer@12925
  1126
    with wf obtain n1 n2 where
schirmer@12925
  1127
      "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> s1"
schirmer@12925
  1128
      "G\<turnstile>s1 \<midarrow>c2\<midarrow>n2\<rightarrow> s2"
schirmer@12925
  1129
      by (blast elim!: wt_elim_cases dest: eval_type_sound)
schirmer@12925
  1130
    then have "G\<turnstile>Norm s0 \<midarrow>c1;; c2\<midarrow>max n1 n2\<rightarrow> s2"
schirmer@12925
  1131
      by (blast intro: evaln.Comp dest: evaln_max2 )
schirmer@12925
  1132
    then show ?case ..
schirmer@12925
  1133
  next
schirmer@12925
  1134
    case (If b c1 c2 e s0 s1 s2 L accC T)
schirmer@12925
  1135
    with wf obtain
schirmer@12925
  1136
      "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean"
schirmer@12925
  1137
      "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>(if the_Bool b then c1 else c2)\<Colon>\<surd>"
schirmer@12925
  1138
      by (cases "the_Bool b") (auto elim!: wt_elim_cases)
schirmer@12925
  1139
    with If wf obtain n1 n2 where
schirmer@12925
  1140
      "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n1\<rightarrow> s1"
schirmer@12925
  1141
      "G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<midarrow>n2\<rightarrow> s2"
schirmer@12925
  1142
      by (blast dest: eval_type_sound)
schirmer@12925
  1143
    then have "G\<turnstile>Norm s0 \<midarrow>If(e) c1 Else c2\<midarrow>max n1 n2\<rightarrow> s2"
schirmer@12925
  1144
      by (blast intro: evaln.If dest: evaln_max2)
schirmer@12925
  1145
    then show ?case ..
schirmer@12925
  1146
  next
schirmer@12925
  1147
    case (Loop b c e l s0 s1 s2 s3 L accC T)
schirmer@12925
  1148
    have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1" .
schirmer@12925
  1149
    have hyp_e: "PROP ?EqEval (Norm s0) s1 (In1l e) (In1 b)" .
schirmer@12925
  1150
    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
schirmer@12925
  1151
    have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (l\<bullet> While(e) c)\<Colon>T" .
schirmer@12925
  1152
    then obtain wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean" and
schirmer@12925
  1153
                wt_c: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c\<Colon>\<surd>"
schirmer@12925
  1154
      by (rule wt_elim_cases) (blast)
schirmer@12925
  1155
    from conf_s0 wt_e 
schirmer@12925
  1156
    obtain n1 where
schirmer@12925
  1157
      "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n1\<rightarrow> s1"
schirmer@12925
  1158
      by (rules dest: hyp_e)
schirmer@12925
  1159
    moreover
schirmer@12925
  1160
    from eval_e wt_e conf_s0 wf
schirmer@12925
  1161
    have conf_s1: "s1\<Colon>\<preceq>(G, L)"
schirmer@12925
  1162
      by (rules dest: eval_type_sound)
schirmer@12925
  1163
    obtain n2 where
schirmer@12925
  1164
      "if normal s1 \<and> the_Bool b 
schirmer@12925
  1165
             then (G\<turnstile>s1 \<midarrow>c\<midarrow>n2\<rightarrow> s2 \<and> 
schirmer@12925
  1166
                   G\<turnstile>(abupd (absorb (Cont l)) s2)\<midarrow>l\<bullet> While(e) c\<midarrow>n2\<rightarrow> s3)
schirmer@12925
  1167
	     else s3 = s1"
schirmer@12925
  1168
    proof (cases "normal s1 \<and> the_Bool b")
schirmer@12925
  1169
      case True
schirmer@12925
  1170
      from Loop True have hyp_c: "PROP ?EqEval s1 s2 (In1r c) \<diamondsuit>"
schirmer@12925
  1171
	by (auto)
schirmer@12925
  1172
      from Loop True have hyp_w: "PROP ?EqEval (abupd (absorb (Cont l)) s2)
schirmer@12925
  1173
                                        s3 (In1r (l\<bullet> While(e) c)) \<diamondsuit>"
schirmer@12925
  1174
	by (auto)
schirmer@12925
  1175
      from Loop True have eval_c: "G\<turnstile>s1 \<midarrow>c\<rightarrow> s2"
schirmer@12925
  1176
	by simp
schirmer@12925
  1177
      from conf_s1 wt_c
schirmer@12925
  1178
      obtain m1 where 
schirmer@12925
  1179
	evaln_c: "G\<turnstile>s1 \<midarrow>c\<midarrow>m1\<rightarrow> s2"
schirmer@12925
  1180
	by (rules dest: hyp_c)
schirmer@12925
  1181
      moreover
schirmer@12925
  1182
      from eval_c conf_s1 wt_c wf
schirmer@12925
  1183
      have "s2\<Colon>\<preceq>(G, L)"
schirmer@12925
  1184
	by (rules dest: eval_type_sound)
schirmer@12925
  1185
      then
schirmer@12925
  1186
      have "abupd (absorb (Cont l)) s2 \<Colon>\<preceq>(G, L)"
schirmer@12925
  1187
	by (cases s2) (auto intro: conforms_absorb)
schirmer@12925
  1188
      from this and wt
schirmer@12925
  1189
      obtain m2 where 
schirmer@12925
  1190
	"G\<turnstile>abupd (absorb (Cont l)) s2 \<midarrow>l\<bullet> While(e) c\<midarrow>m2\<rightarrow> s3"
schirmer@12925
  1191
	by (blast dest: hyp_w)
schirmer@12925
  1192
      moreover note True and that
schirmer@12925
  1193
      ultimately show ?thesis
schirmer@12925
  1194
	by simp (rules intro: evaln_nonstrict le_maxI1 le_maxI2)
schirmer@12925
  1195
    next
schirmer@12925
  1196
      case False
schirmer@12925
  1197
      with Loop have "s3 = s1"
schirmer@12925
  1198
	by simp
schirmer@12925
  1199
      with False that
schirmer@12925
  1200
      show ?thesis
schirmer@12925
  1201
	by auto 
schirmer@12925
  1202
    qed
schirmer@12925
  1203
    ultimately
schirmer@12925
  1204
    have "G\<turnstile>Norm s0 \<midarrow>l\<bullet> While(e) c\<midarrow>max n1 n2\<rightarrow> s3"
schirmer@12925
  1205
      apply -
schirmer@12925
  1206
      apply (rule evaln.Loop)
schirmer@12925
  1207
      apply   (rules intro: evaln_nonstrict intro: le_maxI1)
schirmer@12925
  1208
schirmer@12925
  1209
      apply   (auto intro: evaln_nonstrict intro: le_maxI2)
schirmer@12925
  1210
      done
schirmer@12925
  1211
    then show ?case ..
schirmer@12925
  1212
  next
schirmer@12925
  1213
    case (Do j s L accC T)
schirmer@12925
  1214
    have "G\<turnstile>Norm s \<midarrow>Do j\<midarrow>n\<rightarrow> (Some (Jump j), s)"
schirmer@12925
  1215
      by (rule evaln.Do)
schirmer@12925
  1216
    then show ?case ..
schirmer@12925
  1217
  next
schirmer@12925
  1218
    case (Throw a e s0 s1 L accC T)
schirmer@12925
  1219
    then obtain n where
schirmer@12925
  1220
      "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<midarrow>n\<rightarrow> s1"
schirmer@12925
  1221
      by (rules elim!: wt_elim_cases)
schirmer@12925
  1222
    then have "G\<turnstile>Norm s0 \<midarrow>Throw e\<midarrow>n\<rightarrow> abupd (throw a) s1"
schirmer@12925
  1223
      by (rule evaln.Throw)
schirmer@12925
  1224
    then show ?case ..
schirmer@12925
  1225
  next 
schirmer@12925
  1226
    case (Try catchC c1 c2 s0 s1 s2 s3 vn L accC T)
schirmer@12925
  1227
    have  hyp_c1: "PROP ?EqEval (Norm s0) s1 (In1r c1) \<diamondsuit>" .
schirmer@12925
  1228
    have eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1" .
schirmer@12925
  1229
    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
schirmer@12925
  1230
    have      wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>In1r (Try c1 Catch(catchC vn) c2)\<Colon>T" .
schirmer@12925
  1231
    then obtain 
schirmer@12925
  1232
      wt_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
schirmer@12925
  1233
      wt_c2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<lparr>lcl := L(VName vn\<mapsto>Class catchC)\<rparr>\<turnstile>c2\<Colon>\<surd>"
schirmer@12925
  1234
      by (rule wt_elim_cases) (auto)
schirmer@12925
  1235
    from conf_s0 wt_c1
schirmer@12925
  1236
    obtain n1 where
schirmer@12925
  1237
      "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> s1"
schirmer@12925
  1238
      by (blast dest: hyp_c1)
schirmer@12925
  1239
    moreover 
schirmer@12925
  1240
    have sxalloc: "G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2" .
schirmer@12925
  1241
    moreover
schirmer@12925
  1242
    from eval_c1 wt_c1 conf_s0 wf
schirmer@12925
  1243
    have "s1\<Colon>\<preceq>(G, L)"
schirmer@12925
  1244
      by (blast dest: eval_type_sound)
schirmer@12925
  1245
    with sxalloc wf
schirmer@12925
  1246
    have conf_s2: "s2\<Colon>\<preceq>(G, L)" 
schirmer@12925
  1247
      by (auto dest: sxalloc_type_sound split: option.splits)
schirmer@12925
  1248
    obtain n2 where
schirmer@12925
  1249
      "if G,s2\<turnstile>catch catchC then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<midarrow>n2\<rightarrow> s3 else s3 = s2"
schirmer@12925
  1250
    proof (cases "G,s2\<turnstile>catch catchC")
schirmer@12925
  1251
      case True
schirmer@12925
  1252
      note Catch = this
schirmer@12925
  1253
      with Try have hyp_c2: "PROP ?EqEval (new_xcpt_var vn s2) s3 (In1r c2) \<diamondsuit>"
schirmer@12925
  1254
	by auto
schirmer@12925
  1255
      show ?thesis
schirmer@12925
  1256
      proof (cases "normal s1")
schirmer@12925
  1257
	case True
schirmer@12925
  1258
	with sxalloc wf 
schirmer@12925
  1259
	have eq_s2_s1: "s2=s1"
schirmer@12925
  1260
	  by (auto dest: sxalloc_type_sound split: option.splits)
schirmer@12925
  1261
	with True 
schirmer@12925
  1262
	have "\<not>  G,s2\<turnstile>catch catchC"
schirmer@12925
  1263
	  by (simp add: catch_def)
schirmer@12925
  1264
	with Catch show ?thesis 
schirmer@12925
  1265
	  by (contradiction)
schirmer@12925
  1266
      next 
schirmer@12925
  1267
	case False
schirmer@12925
  1268
	with sxalloc wf
schirmer@12925
  1269
	obtain a 
schirmer@12925
  1270
	  where xcpt_s2: "abrupt s2 = Some (Xcpt (Loc a))"
schirmer@12925
  1271
	  by (auto dest!: sxalloc_type_sound split: option.splits)
schirmer@12925
  1272
	with Catch
schirmer@12925
  1273
	have "G\<turnstile>obj_ty (the (globs (store s2) (Heap a)))\<preceq>Class catchC"
schirmer@12925
  1274
	  by (cases s2) simp
schirmer@12925
  1275
	with xcpt_s2 conf_s2 wf 
schirmer@12925
  1276
	have "new_xcpt_var vn s2\<Colon>\<preceq>(G, L(VName vn\<mapsto>Class catchC))"
schirmer@12925
  1277
	  by (auto dest: Try_lemma)
wenzelm@12937
  1278
	(* FIXME extract lemma for this conformance, also useful for
schirmer@12925
  1279
               eval_type_sound and evaln_eval *)
schirmer@12925
  1280
	from this wt_c2
schirmer@12925
  1281
	obtain m where "G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<midarrow>m\<rightarrow> s3"
schirmer@12925
  1282
	  by (auto dest: hyp_c2)
schirmer@12925
  1283
	with True that
schirmer@12925
  1284
	show ?thesis
schirmer@12925
  1285
	  by simp
schirmer@12925
  1286
      qed
schirmer@12925
  1287
    next
schirmer@12925
  1288
      case False
schirmer@12925
  1289
      with Try
schirmer@12925
  1290
      have "s3=s2"
schirmer@12925
  1291
	by simp
schirmer@12925
  1292
      with False and that
schirmer@12925
  1293
      show ?thesis
schirmer@12925
  1294
	by simp
schirmer@12925
  1295
    qed
schirmer@12925
  1296
    ultimately
schirmer@12925
  1297
    have "G\<turnstile>Norm s0 \<midarrow>Try c1 Catch(catchC vn) c2\<midarrow>max n1 n2\<rightarrow> s3"
schirmer@12925
  1298
      by (auto intro!: evaln.Try le_maxI1 le_maxI2)
schirmer@12925
  1299
    then show ?case ..
schirmer@12925
  1300
  next
schirmer@13337
  1301
    case (Fin c1 c2 s0 s1 s2 s3 x1 L accC T)
schirmer@13337
  1302
    have s3: "s3 = (if \<exists>err. x1 = Some (Error err) 
schirmer@13337
  1303
                       then (x1, s1)
schirmer@13337
  1304
                       else abupd (abrupt_if (x1 \<noteq> None) x1) s2)" .
schirmer@13337
  1305
    from Fin wf obtain n1 n2 where 
schirmer@12925
  1306
      "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> (x1, s1)"
schirmer@13337
  1307
      "G\<turnstile>Norm s1 \<midarrow>c2\<midarrow>n2\<rightarrow> s2" and
schirmer@13337
  1308
      error_free_s1: "error_free (x1,s1)"
schirmer@12925
  1309
      by (blast elim!: wt_elim_cases 
schirmer@12925
  1310
	         dest: eval_type_sound intro: conforms_NormI)
schirmer@12925
  1311
    then have 
schirmer@12925
  1312
     "G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<midarrow>max n1 n2\<rightarrow> abupd (abrupt_if (x1 \<noteq> None) x1) s2"
schirmer@12925
  1313
      by (blast intro: evaln.Fin dest: evaln_max2)
schirmer@13337
  1314
    with error_free_s1 s3
schirmer@13337
  1315
    show "\<exists>n. G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<midarrow>n\<rightarrow> s3"
schirmer@13337
  1316
      by (auto simp add: error_free_def)
schirmer@12925
  1317
  next
schirmer@12925
  1318
    case (Init C c s0 s1 s2 s3 L accC T)
schirmer@12925
  1319
    have     cls: "the (class G C) = c" .
schirmer@12925
  1320
    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
schirmer@12925
  1321
    have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (Init C)\<Colon>T" .
schirmer@12925
  1322
    with cls
schirmer@12925
  1323
    have cls_C: "class G C = Some c"
schirmer@12925
  1324
      by - (erule wt_elim_cases,auto)
schirmer@12925
  1325
    obtain n where
schirmer@12925
  1326
      "if inited C (globs s0) then s3 = Norm s0
schirmer@12925
  1327
       else (G\<turnstile>Norm (init_class_obj G C s0)
schirmer@12925
  1328
	      \<midarrow>(if C = Object then Skip else Init (super c))\<midarrow>n\<rightarrow> s1 \<and>
schirmer@12925
  1329
	           G\<turnstile>set_lvars empty s1 \<midarrow>init c\<midarrow>n\<rightarrow> s2 \<and> 
schirmer@12925
  1330
                   s3 = restore_lvars s1 s2)"
schirmer@12925
  1331
    proof (cases "inited C (globs s0)")
schirmer@12925
  1332
      case True
schirmer@12925
  1333
      with Init have "s3 = Norm s0"
schirmer@12925
  1334
	by simp
schirmer@12925
  1335
      with True that show ?thesis 
schirmer@12925
  1336
	by simp
schirmer@12925
  1337
    next
schirmer@12925
  1338
      case False
schirmer@12925
  1339
      with Init
schirmer@12925
  1340
      obtain 
schirmer@12925
  1341
	hyp_init_super: 
schirmer@12925
  1342
        "PROP ?EqEval (Norm ((init_class_obj G C) s0)) s1
schirmer@12925
  1343
	               (In1r (if C = Object then Skip else Init (super c))) \<diamondsuit>"
schirmer@12925
  1344
	and 
schirmer@12925
  1345
        hyp_init_c:
schirmer@12925
  1346
	   "PROP ?EqEval ((set_lvars empty) s1) s2 (In1r (init c)) \<diamondsuit>" and
schirmer@12925
  1347
	s3: "s3 = (set_lvars (locals (store s1))) s2" and
schirmer@12925
  1348
	eval_init_super: 
schirmer@12925
  1349
	"G\<turnstile>Norm ((init_class_obj G C) s0) 
schirmer@12925
  1350
           \<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1"
schirmer@12925
  1351
	by (simp only: if_False)
schirmer@12925
  1352
      from conf_s0 wf cls_C False
schirmer@12925
  1353
      have conf_s0': "(Norm ((init_class_obj G C) s0))\<Colon>\<preceq>(G, L)"
schirmer@12925
  1354
	by (auto dest: conforms_init_class_obj)
schirmer@12925
  1355
      moreover
schirmer@12925
  1356
      from wf cls_C 
schirmer@12925
  1357
      have wt_init_super:
schirmer@12925
  1358
           "\<lparr>prg = G, cls = accC, lcl = L\<rparr>
schirmer@12925
  1359
                  \<turnstile>(if C = Object then Skip else Init (super c))\<Colon>\<surd>"
schirmer@12925
  1360
	by (cases "C=Object")
schirmer@12925
  1361
           (auto dest: wf_prog_cdecl wf_cdecl_supD is_acc_classD)
schirmer@12925
  1362
      ultimately
schirmer@12925
  1363
      obtain m1 where  
schirmer@12925
  1364
	   "G\<turnstile>Norm ((init_class_obj G C) s0) 
schirmer@12925
  1365
            \<midarrow>(if C = Object then Skip else Init (super c))\<midarrow>m1\<rightarrow> s1"
schirmer@12925
  1366
	by (rules dest: hyp_init_super)
schirmer@12925
  1367
      moreover
schirmer@12925
  1368
      from eval_init_super conf_s0' wt_init_super wf
schirmer@12925
  1369
      have "s1\<Colon>\<preceq>(G, L)"
schirmer@12925
  1370
	by (rules dest: eval_type_sound)
schirmer@12925
  1371
      then
schirmer@12925
  1372
      have "(set_lvars empty) s1\<Colon>\<preceq>(G, empty)"
schirmer@12925
  1373
	by (cases s1) (auto dest: conforms_set_locals )
schirmer@12925
  1374
      with wf cls_C 
schirmer@12925
  1375
      obtain m2 where
schirmer@12925
  1376
	"G\<turnstile>(set_lvars empty) s1 \<midarrow>init c\<midarrow>m2\<rightarrow> s2"
schirmer@12925
  1377
	by (blast dest!: hyp_init_c 
schirmer@12925
  1378
                   dest: wf_prog_cdecl intro!: wf_cdecl_wt_init)
schirmer@12925
  1379
      moreover note s3 and False and that
schirmer@12925
  1380
      ultimately show ?thesis
schirmer@12925
  1381
	by simp (rules intro: evaln_nonstrict le_maxI1 le_maxI2)
schirmer@12925
  1382
    qed
schirmer@12925
  1383
    from cls this have "G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s3"
schirmer@12925
  1384
      by (rule evaln.Init)
schirmer@12925
  1385
    then show ?case ..
schirmer@12925
  1386
  next
schirmer@12925
  1387
    case (NewC C a s0 s1 s2 L accC T)
schirmer@12925
  1388
    with wf obtain n where 
schirmer@12925
  1389
     "G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s1"
schirmer@12925
  1390
      by (blast elim!: wt_elim_cases dest: is_acc_classD)
schirmer@12925
  1391
    with NewC 
schirmer@12925
  1392
    have "G\<turnstile>Norm s0 \<midarrow>NewC C-\<succ>Addr a\<midarrow>n\<rightarrow> s2"
schirmer@12925
  1393
      by (rules intro: evaln.NewC)
schirmer@12925
  1394
    then show ?case ..
schirmer@12925
  1395
  next
schirmer@12925
  1396
    case (NewA T a e i s0 s1 s2 s3 L accC Ta)
schirmer@12925
  1397
    hence "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>init_comp_ty T\<Colon>\<surd>" 
schirmer@12925
  1398
      by (auto elim!: wt_elim_cases 
schirmer@12925
  1399
              intro!: wt_init_comp_ty dest: is_acc_typeD)
schirmer@12925
  1400
    with NewA wf obtain n1 n2 where 
schirmer@12925
  1401
      "G\<turnstile>Norm s0 \<midarrow>init_comp_ty T\<midarrow>n1\<rightarrow> s1"
schirmer@12925
  1402
      "G\<turnstile>s1 \<midarrow>e-\<succ>i\<midarrow>n2\<rightarrow> s2"      
schirmer@12925
  1403
      by (blast elim!: wt_elim_cases dest: eval_type_sound)
schirmer@12925
  1404
    moreover
schirmer@12925
  1405
    have "G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3" .
schirmer@12925
  1406
    ultimately
schirmer@12925
  1407
    have "G\<turnstile>Norm s0 \<midarrow>New T[e]-\<succ>Addr a\<midarrow>max n1 n2\<rightarrow> s3"
schirmer@12925
  1408
      by (blast intro: evaln.NewA dest: evaln_max2)
schirmer@12925
  1409
    then show ?case ..
schirmer@12925
  1410
  next
schirmer@12925
  1411
    case (Cast castT e s0 s1 s2 v L accC T)
schirmer@12925
  1412
    with wf obtain n where
schirmer@12925
  1413
      "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
schirmer@12925
  1414
      by (rules elim!: wt_elim_cases)
schirmer@12925
  1415
    moreover 
schirmer@12925
  1416
    have "s2 = abupd (raise_if (\<not> G,snd s1\<turnstile>v fits castT) ClassCast) s1" .
schirmer@12925
  1417
    ultimately
schirmer@12925
  1418
    have "G\<turnstile>Norm s0 \<midarrow>Cast castT e-\<succ>v\<midarrow>n\<rightarrow> s2"
schirmer@12925
  1419
      by (rule evaln.Cast)
schirmer@12925
  1420
    then show ?case ..
schirmer@12925
  1421
  next
schirmer@12925
  1422
    case (Inst T b e s0 s1 v L accC T')
schirmer@12925
  1423
    with wf obtain n where
schirmer@12925
  1424
      "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
schirmer@12925
  1425
      by (rules elim!: wt_elim_cases)
schirmer@12925
  1426
    moreover 
schirmer@12925
  1427
    have "b = (v \<noteq> Null \<and> G,snd s1\<turnstile>v fits RefT T)" .
schirmer@12925
  1428
    ultimately
schirmer@12925
  1429
    have "G\<turnstile>Norm s0 \<midarrow>e InstOf T-\<succ>Bool b\<midarrow>n\<rightarrow> s1"
schirmer@12925
  1430
      by (rule evaln.Inst)
schirmer@12925
  1431
    then show ?case ..
schirmer@12925
  1432
  next
schirmer@12925
  1433
    case (Lit s v L accC T)
schirmer@12925
  1434
    have "G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<midarrow>n\<rightarrow> Norm s"
schirmer@12925
  1435
      by (rule evaln.Lit)
schirmer@12925
  1436
    then show ?case ..
schirmer@12925
  1437
  next
schirmer@13337
  1438
    case (UnOp e s0 s1 unop v L accC T)
schirmer@13337
  1439
    with wf obtain n where
schirmer@13337
  1440
      "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
schirmer@13337
  1441
      by (rules elim!: wt_elim_cases)
schirmer@13337
  1442
    hence "G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>eval_unop unop v\<midarrow>n\<rightarrow> s1"
schirmer@13337
  1443
      by (rule evaln.UnOp)
schirmer@13337
  1444
    then show ?case ..
schirmer@13337
  1445
  next
schirmer@13337
  1446
    case (BinOp binop e1 e2 s0 s1 s2 v1 v2 L accC T)
schirmer@13337
  1447
    with wf obtain n1 n2 where 
schirmer@13337
  1448
      "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<midarrow>n1\<rightarrow> s1"
schirmer@13337
  1449
      "G\<turnstile>s1 \<midarrow>e2-\<succ>v2\<midarrow>n2\<rightarrow> s2"    
schirmer@13337
  1450
      by (blast elim!: wt_elim_cases dest: eval_type_sound)
schirmer@13337
  1451
    hence "G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<midarrow>max n1 n2
schirmer@13337
  1452
           \<rightarrow> s2"
schirmer@13337
  1453
      by (blast intro!: evaln.BinOp dest: evaln_max2)
schirmer@13337
  1454
    then show ?case ..
schirmer@13337
  1455
  next
schirmer@12925
  1456
    case (Super s L accC T)
schirmer@12925
  1457
    have "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<midarrow>n\<rightarrow> Norm s"
schirmer@12925
  1458
      by (rule evaln.Super)
schirmer@12925
  1459
    then show ?case ..
schirmer@12925
  1460
  next
schirmer@12925
  1461
    case (Acc f s0 s1 v va L accC T)
schirmer@12925
  1462
    with wf obtain n where
schirmer@12925
  1463
      "G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v, f)\<midarrow>n\<rightarrow> s1"
schirmer@12925
  1464
      by (rules elim!: wt_elim_cases)
schirmer@12925
  1465
    then
schirmer@12925
  1466
    have "G\<turnstile>Norm s0 \<midarrow>Acc va-\<succ>v\<midarrow>n\<rightarrow> s1"
schirmer@12925
  1467
      by (rule evaln.Acc)
schirmer@12925
  1468
    then show ?case ..
schirmer@12925
  1469
  next
schirmer@12925
  1470
    case (Ass e f s0 s1 s2 v var w L accC T)
schirmer@12925
  1471
    with wf obtain n1 n2 where 
schirmer@12925
  1472
      "G\<turnstile>Norm s0 \<midarrow>var=\<succ>(w, f)\<midarrow>n1\<rightarrow> s1"
schirmer@12925
  1473
      "G\<turnstile>s1 \<midarrow>e-\<succ>v\<midarrow>n2\<rightarrow> s2"      
schirmer@12925
  1474
      by (blast elim!: wt_elim_cases dest: eval_type_sound)
schirmer@12925
  1475
    then
schirmer@12925
  1476
    have "G\<turnstile>Norm s0 \<midarrow>var:=e-\<succ>v\<midarrow>max n1 n2\<rightarrow> assign f v s2"
schirmer@12925
  1477
      by (blast intro: evaln.Ass dest: evaln_max2)
schirmer@12925
  1478
    then show ?case ..
schirmer@12925
  1479
  next
schirmer@12925
  1480
    case (Cond b e0 e1 e2 s0 s1 s2 v L accC T)
schirmer@12925
  1481
    have hyp_e0: "PROP ?EqEval (Norm s0) s1 (In1l e0) (In1 b)" .
schirmer@12925
  1482
    have hyp_if: "PROP ?EqEval s1 s2 
schirmer@12925
  1483
                              (In1l (if the_Bool b then e1 else e2)) (In1 v)" .
schirmer@12925
  1484
    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
schirmer@12925
  1485
    have wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (e0 ? e1 : e2)\<Colon>T" .
schirmer@12925
  1486
    then obtain T1 T2 statT where
schirmer@12925
  1487
       wt_e0: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e0\<Colon>-PrimT Boolean" and
schirmer@12925
  1488
       wt_e1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e1\<Colon>-T1" and
schirmer@12925
  1489
       wt_e2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e2\<Colon>-T2" and 
schirmer@12925
  1490
       statT: "G\<turnstile>T1\<preceq>T2 \<and> statT = T2  \<or>  G\<turnstile>T2\<preceq>T1 \<and> statT =  T1" and
schirmer@12925
  1491
       T    : "T=Inl statT"
schirmer@12925
  1492
      by (rule wt_elim_cases) auto
schirmer@12925
  1493
    have eval_e0: "G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1" .
schirmer@12925
  1494
    from conf_s0 wt_e0
schirmer@12925
  1495
    obtain n1 where 
schirmer@12925
  1496
      "G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<midarrow>n1\<rightarrow> s1"
schirmer@12925
  1497
      by (rules dest: hyp_e0)
schirmer@12925
  1498
    moreover
schirmer@12925
  1499
    from eval_e0 conf_s0 wf wt_e0
schirmer@12925
  1500
    have "s1\<Colon>\<preceq>(G, L)"
schirmer@12925
  1501
      by (blast dest: eval_type_sound)
schirmer@12925
  1502
    with wt_e1 wt_e2 statT hyp_if obtain n2 where
schirmer@12925
  1503
      "G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<midarrow>n2\<rightarrow> s2"
schirmer@12925
  1504
      by  (cases "the_Bool b") force+
schirmer@12925
  1505
    ultimately
schirmer@12925
  1506
    have "G\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<midarrow>max n1 n2\<rightarrow> s2"
schirmer@12925
  1507
      by (blast intro: evaln.Cond dest: evaln_max2)
schirmer@12925
  1508
    then show ?case ..
schirmer@12925
  1509
  next
schirmer@12925
  1510
    case (Call invDeclC a' accC' args e mn mode pTs' s0 s1 s2 s3 s3' s4 statT 
schirmer@12925
  1511
      v vs L accC T)
schirmer@12925
  1512
    (* Repeats large parts of the type soundness proof. One should factor
schirmer@12925
  1513
       out some lemmata about the relations and conformance of s2, s3 and s3'*)
schirmer@12925
  1514
    have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1" .
schirmer@12925
  1515
    have eval_args: "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<rightarrow> s2" .
schirmer@12925
  1516
    have invDeclC: "invDeclC 
schirmer@12925
  1517
                      = invocation_declclass G mode (store s2) a' statT 
schirmer@12925
  1518
                           \<lparr>name = mn, parTs = pTs'\<rparr>" .
schirmer@12925
  1519
    have
schirmer@12925
  1520
      init_lvars: "s3 = 
schirmer@12925
  1521
             init_lvars G invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> mode a' vs s2" .
schirmer@12925
  1522
    have
schirmer@12925
  1523
      check: "s3' =
schirmer@12925
  1524
       check_method_access G accC' statT mode \<lparr>name = mn, parTs = pTs'\<rparr> a' s3" .
schirmer@12925
  1525
    have eval_methd: 
schirmer@12925
  1526
           "G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>-\<succ>v\<rightarrow> s4" .
schirmer@12925
  1527
    have     hyp_e: "PROP ?EqEval (Norm s0) s1 (In1l e) (In1 a')" .
schirmer@12925
  1528
    have  hyp_args: "PROP ?EqEval s1 s2 (In3 args) (In3 vs)" .
schirmer@12925
  1529
    have hyp_methd: "PROP ?EqEval s3' s4 
schirmer@13337
  1530
             (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)) (In1 v)".
schirmer@12925
  1531
    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
schirmer@12925
  1532
    have      wt: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>
schirmer@12925
  1533
                    \<turnstile>In1l ({accC',statT,mode}e\<cdot>mn( {pTs'}args))\<Colon>T" .
schirmer@12925
  1534
    from wt obtain pTs statDeclT statM where
schirmer@12925
  1535
                 wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT" and
schirmer@12925
  1536
              wt_args: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>args\<Colon>\<doteq>pTs" and
schirmer@12925
  1537
                statM: "max_spec G accC statT \<lparr>name=mn,parTs=pTs\<rparr> 
schirmer@12925
  1538
                         = {((statDeclT,statM),pTs')}" and
schirmer@12925
  1539
                 mode: "mode = invmode statM e" and
schirmer@12925
  1540
                    T: "T =Inl (resTy statM)" and
schirmer@12925
  1541
        eq_accC_accC': "accC=accC'"
schirmer@12925
  1542
      by (rule wt_elim_cases) auto
schirmer@12925
  1543
    from conf_s0 wt_e
schirmer@12925
  1544
    obtain n1 where
schirmer@12925
  1545
      evaln_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n1\<rightarrow> s1"
schirmer@12925
  1546
      by (rules dest: hyp_e)
schirmer@12925
  1547
    from wf eval_e conf_s0 wt_e
schirmer@12925
  1548
    obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and
schirmer@12925
  1549
           conf_a': "normal s1 \<Longrightarrow> G, store s1\<turnstile>a'\<Colon>\<preceq>RefT statT"  
schirmer@12925
  1550
      by (auto dest!: eval_type_sound)
schirmer@12925
  1551
    from conf_s1 wt_args
schirmer@12925
  1552
    obtain n2 where
schirmer@12925
  1553
      evaln_args: "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<midarrow>n2\<rightarrow> s2"
schirmer@12925
  1554
      by (blast dest: hyp_args)
schirmer@12925
  1555
    from wt_args conf_s1 eval_args wf 
schirmer@12925
  1556
    obtain    conf_s2: "s2\<Colon>\<preceq>(G, L)" and
schirmer@12925
  1557
            conf_args: "normal s2 
schirmer@12925
  1558
                         \<Longrightarrow>  list_all2 (conf G (store s2)) vs pTs"  
schirmer@12925
  1559
      by (auto dest!: eval_type_sound)
schirmer@12925
  1560
    from statM 
schirmer@12925
  1561
    obtain
schirmer@12925
  1562
       statM': "(statDeclT,statM)\<in>mheads G accC statT \<lparr>name=mn,parTs=pTs'\<rparr>" and
schirmer@12925
  1563
       pTs_widen: "G\<turnstile>pTs[\<preceq>]pTs'"
schirmer@12925
  1564
      by (blast dest: max_spec2mheads)
schirmer@12925
  1565
    from check
schirmer@12925
  1566
    have eq_store_s3'_s3: "store s3'=store s3"
schirmer@12925
  1567
      by (cases s3) (simp add: check_method_access_def Let_def)
schirmer@12925
  1568
    obtain invC
schirmer@12925
  1569
      where invC: "invC = invocation_class mode (store s2) a' statT"
schirmer@12925
  1570
      by simp
schirmer@12925
  1571
    with init_lvars
schirmer@12925
  1572
    have invC': "invC = (invocation_class mode (store s3) a' statT)"
schirmer@12925
  1573
      by (cases s2,cases mode) (auto simp add: init_lvars_def2 )
schirmer@12925
  1574
    obtain n3 where
schirmer@12925
  1575
     "G\<turnstile>Norm s0 \<midarrow>{accC',statT,mode}e\<cdot>mn( {pTs'}args)-\<succ>v\<midarrow>n3\<rightarrow> 
schirmer@12925
  1576
          (set_lvars (locals (store s2))) s4"
schirmer@12925
  1577
    proof (cases "normal s2")
schirmer@12925
  1578
      case False
schirmer@12925
  1579
      with init_lvars 
schirmer@12925
  1580
      obtain keep_abrupt: "abrupt s3 = abrupt s2" and
schirmer@12925
  1581
             "store s3 = store (init_lvars G invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> 
schirmer@12925
  1582
                                            mode a' vs s2)" 
schirmer@12925
  1583
	by (auto simp add: init_lvars_def2)
schirmer@12925
  1584
      moreover
schirmer@12925
  1585
      from keep_abrupt False check
schirmer@12925
  1586
      have eq_s3'_s3: "s3'=s3" 
schirmer@12925
  1587
	by (auto simp add: check_method_access_def Let_def)
schirmer@12925
  1588
      moreover
schirmer@12925
  1589
      from eq_s3'_s3 False keep_abrupt eval_methd init_lvars
schirmer@12925
  1590
      obtain "s4=s3'"
schirmer@13337
  1591
      "In1 v=arbitrary3 (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>))"
schirmer@12925
  1592
	by auto
schirmer@12925
  1593
      moreover note False evaln.Abrupt
schirmer@12925
  1594
      ultimately obtain m where 
schirmer@12925
  1595
	"G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>-\<succ>v\<midarrow>m\<rightarrow> s4"
schirmer@12925
  1596
	by force
schirmer@12925
  1597
      from evaln_e evaln_args invDeclC init_lvars eq_s3'_s3 this
schirmer@12925
  1598
      have 
schirmer@12925
  1599
       "G\<turnstile>Norm s0 \<midarrow>{accC',statT,mode}e\<cdot>mn( {pTs'}args)-\<succ>v\<midarrow>max n1 (max n2 m)\<rightarrow> 
schirmer@12925
  1600
            (set_lvars (locals (store s2))) s4"
schirmer@12925
  1601
	by (auto intro!: evaln.Call le_maxI1 le_max3I1 le_max3I2)
schirmer@12925
  1602
      with that show ?thesis 
schirmer@12925
  1603
	by rules
schirmer@12925
  1604
    next
schirmer@12925
  1605
      case True
schirmer@12925
  1606
      note normal_s2 = True
schirmer@12925
  1607
      with eval_args
schirmer@12925
  1608
      have normal_s1: "normal s1"
schirmer@12925
  1609
	by (cases "normal s1") auto
schirmer@12925
  1610
      with conf_a' eval_args 
schirmer@12925
  1611
      have conf_a'_s2: "G, store s2\<turnstile>a'\<Colon>\<preceq>RefT statT"
schirmer@12925
  1612
	by (auto dest: eval_gext intro: conf_gext)
schirmer@12925
  1613
      show ?thesis
schirmer@12925
  1614
      proof (cases "a'=Null \<longrightarrow> is_static statM")
schirmer@12925
  1615
	case False
schirmer@12925
  1616
	then obtain not_static: "\<not> is_static statM" and Null: "a'=Null" 
schirmer@12925
  1617
	  by blast
schirmer@12925
  1618
	with normal_s2 init_lvars mode
schirmer@12925
  1619
	obtain np: "abrupt s3 = Some (Xcpt (Std NullPointer))" and
schirmer@12925
  1620
                   "store s3 = store (init_lvars G invDeclC 
schirmer@12925
  1621
                                       \<lparr>name = mn, parTs = pTs'\<rparr> mode a' vs s2)"
schirmer@12925
  1622
	  by (auto simp add: init_lvars_def2)
schirmer@12925
  1623
	moreover
schirmer@12925
  1624
	from np check
schirmer@12925
  1625
	have eq_s3'_s3: "s3'=s3" 
schirmer@12925
  1626
	  by (auto simp add: check_method_access_def Let_def)
schirmer@12925
  1627
	moreover
schirmer@12925
  1628
	from eq_s3'_s3 np eval_methd init_lvars
schirmer@12925
  1629
	obtain "s4=s3'"
schirmer@13337
  1630
      "In1 v=arbitrary3 (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>))"
schirmer@12925
  1631
	  by auto
schirmer@12925
  1632
	moreover note np
schirmer@12925
  1633
	ultimately obtain m where 
schirmer@12925
  1634
	  "G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>-\<succ>v\<midarrow>m\<rightarrow> s4"
schirmer@12925
  1635
	  by force
schirmer@12925
  1636
	from evaln_e evaln_args invDeclC init_lvars eq_s3'_s3 this
schirmer@12925
  1637
	have 
schirmer@12925
  1638
        "G\<turnstile>Norm s0 \<midarrow>{accC',statT,mode}e\<cdot>mn( {pTs'}args)-\<succ>v\<midarrow>max n1 (max n2 m)\<rightarrow> 
schirmer@12925
  1639
            (set_lvars (locals (store s2))) s4"
schirmer@12925
  1640
	  by (auto intro!: evaln.Call le_maxI1 le_max3I1 le_max3I2)
schirmer@12925
  1641
	with that show ?thesis 
schirmer@12925
  1642
	  by rules
schirmer@12925
  1643
      next
schirmer@12925
  1644
	case True
schirmer@12925
  1645
	with mode have notNull: "mode = IntVir \<longrightarrow> a' \<noteq> Null"
schirmer@12925
  1646
	  by (auto dest!: Null_staticD)
schirmer@12925
  1647
	with conf_s2 conf_a'_s2 wf invC 
schirmer@12925
  1648
	have dynT_prop: "G\<turnstile>mode\<rightarrow>invC\<preceq>statT"
schirmer@12925
  1649
	  by (cases s2) (auto intro: DynT_propI)
schirmer@12925
  1650
	with wt_e statM' invC mode wf 
schirmer@12925
  1651
	obtain dynM where 
schirmer@12925
  1652
           dynM: "dynlookup G statT invC  \<lparr>name=mn,parTs=pTs'\<rparr> = Some dynM" and
schirmer@12925
  1653
           acc_dynM: "G \<turnstile>Methd  \<lparr>name=mn,parTs=pTs'\<rparr> dynM 
schirmer@12925
  1654
                          in invC dyn_accessible_from accC"
schirmer@12925
  1655
	  by (force dest!: call_access_ok)
schirmer@12925
  1656
	with invC' check eq_accC_accC'
schirmer@12925
  1657
	have eq_s3'_s3: "s3'=s3"
schirmer@12925
  1658
	  by (auto simp add: check_method_access_def Let_def)
schirmer@12925
  1659
	from dynT_prop wf wt_e statM' mode invC invDeclC dynM 
schirmer@12925
  1660
	obtain 
schirmer@12925
  1661
	   wf_dynM: "wf_mdecl G invDeclC (\<lparr>name=mn,parTs=pTs'\<rparr>,mthd dynM)" and
schirmer@12925
  1662
	     dynM': "methd G invDeclC \<lparr>name=mn,parTs=pTs'\<rparr> = Some dynM" and
schirmer@12925
  1663
           iscls_invDeclC: "is_class G invDeclC" and
schirmer@12925
  1664
	        invDeclC': "invDeclC = declclass dynM" and
schirmer@12925
  1665
	     invC_widen: "G\<turnstile>invC\<preceq>\<^sub>C invDeclC" and
schirmer@12925
  1666
	   is_static_eq: "is_static dynM = is_static statM" and
schirmer@12925
  1667
	   involved_classes_prop:
schirmer@12925
  1668
             "(if invmode statM e = IntVir
schirmer@12925
  1669
               then \<forall>statC. statT = ClassT statC \<longrightarrow> G\<turnstile>invC\<preceq>\<^sub>C statC
schirmer@12925
  1670
               else ((\<exists>statC. statT = ClassT statC \<and> G\<turnstile>statC\<preceq>\<^sub>C invDeclC) \<or>
schirmer@12925
  1671
                     (\<forall>statC. statT \<noteq> ClassT statC \<and> invDeclC = Object)) \<and>
schirmer@12925
  1672
                      statDeclT = ClassT invDeclC)"
schirmer@12925
  1673
	  by (auto dest: DynT_mheadsD)
schirmer@12925
  1674
	obtain L' where 
schirmer@12925
  1675
	   L':"L'=(\<lambda> k. 
schirmer@12925
  1676
                 (case k of
schirmer@12925
  1677
                    EName e
schirmer@12925
  1678
                    \<Rightarrow> (case e of 
schirmer@12925
  1679
                          VNam v 
schirmer@12925
  1680
                          \<Rightarrow>(table_of (lcls (mbody (mthd dynM)))
schirmer@12925
  1681
                             (pars (mthd dynM)[\<mapsto>]pTs')) v
schirmer@12925
  1682
                        | Res \<Rightarrow> Some (resTy dynM))
schirmer@12925
  1683
                  | This \<Rightarrow> if is_static statM 
schirmer@12925
  1684
                            then None else Some (Class invDeclC)))"
schirmer@12925
  1685
	  by simp
schirmer@12925
  1686
	from wf_dynM [THEN wf_mdeclD1, THEN conjunct1] normal_s2 conf_s2 wt_e
schirmer@12925
  1687
              wf eval_args conf_a' mode notNull wf_dynM involved_classes_prop
schirmer@12925
  1688
	have conf_s3: "s3\<Colon>\<preceq>(G,L')"
schirmer@12925
  1689
	   apply - 
schirmer@12925
  1690
          (*FIXME confomrs_init_lvars should be 
schirmer@12925
  1691
                adjusted to be more directy applicable *)
schirmer@12925
  1692
	   apply (drule conforms_init_lvars [of G invDeclC 
schirmer@12925
  1693
                  "\<lparr>name=mn,parTs=pTs'\<rparr>" dynM "store s2" vs pTs "abrupt s2" 
schirmer@12925
  1694
                  L statT invC a' "(statDeclT,statM)" e])
schirmer@12925
  1695
	     apply (rule wf)
schirmer@12925
  1696
	     apply (rule conf_args,assumption)
schirmer@12925
  1697
	     apply (simp add: pTs_widen)
schirmer@12925
  1698
	     apply (cases s2,simp)
schirmer@12925
  1699
	     apply (rule dynM')
schirmer@12925
  1700
	     apply (force dest: ty_expr_is_type)
schirmer@12925
  1701
	     apply (rule invC_widen)
schirmer@12925
  1702
	     apply (force intro: conf_gext dest: eval_gext)
schirmer@12925
  1703
	     apply simp
schirmer@12925
  1704
	     apply simp
schirmer@12925
  1705
	     apply (simp add: invC)
schirmer@12925
  1706
	     apply (simp add: invDeclC)
schirmer@12925
  1707
	     apply (force dest: wf_mdeclD1 is_acc_typeD)
schirmer@12925
  1708
	     apply (cases s2, simp add: L' init_lvars
schirmer@12925
  1709
	                      cong add: lname.case_cong ename.case_cong)
schirmer@12925
  1710
	   done
schirmer@12925
  1711
	with is_static_eq wf_dynM L'
schirmer@12925
  1712
	obtain mthdT where
schirmer@12925
  1713
	   "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>
schirmer@12925
  1714
            \<turnstile>Body invDeclC (stmt (mbody (mthd dynM)))\<Colon>-mthdT" 
schirmer@12925
  1715
	  by - (drule wf_mdecl_bodyD,
schirmer@13337
  1716
                auto simp: cong add: lname.case_cong ename.case_cong)
schirmer@12925
  1717
	with dynM' iscls_invDeclC invDeclC'
schirmer@12925
  1718
	have
schirmer@12925
  1719
	   "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>
schirmer@12925
  1720
            \<turnstile>(Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)\<Colon>-mthdT"
schirmer@12925
  1721
	  by (auto intro: wt.Methd)
schirmer@12925
  1722
	with conf_s3 eq_s3'_s3 hyp_methd
schirmer@12925
  1723
	obtain m where
schirmer@12925
  1724
	   "G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>-\<succ>v\<midarrow>m\<rightarrow> s4"
schirmer@12925
  1725
	  by (blast)
schirmer@12925
  1726
	from evaln_e evaln_args invDeclC init_lvars  eq_s3'_s3 this
schirmer@12925
  1727
	have 
schirmer@12925
  1728
        "G\<turnstile>Norm s0 \<midarrow>{accC',statT,mode}e\<cdot>mn( {pTs'}args)-\<succ>v\<midarrow>max n1 (max n2 m)\<rightarrow> 
schirmer@12925
  1729
            (set_lvars (locals (store s2))) s4"
schirmer@12925
  1730
	  by (auto intro!: evaln.Call le_maxI1 le_max3I1 le_max3I2)
schirmer@12925
  1731
	with that show ?thesis 
schirmer@12925
  1732
	  by rules
schirmer@12925
  1733
      qed
schirmer@12925
  1734
    qed
schirmer@12925
  1735
    then show ?case ..
schirmer@12925
  1736
  next
schirmer@12925
  1737
    case (Methd D s0 s1 sig v L accC T)
schirmer@12925
  1738
    then obtain n where
schirmer@12925
  1739
      "G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<midarrow>n\<rightarrow> s1"
schirmer@12925
  1740
      by - (erule wt_elim_cases, force simp add: body_def2)
schirmer@12925
  1741
    then have "G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<midarrow>Suc n\<rightarrow> s1"
schirmer@12925
  1742
      by (rule evaln.Methd)
schirmer@12925
  1743
    then show ?case ..
schirmer@12925
  1744
  next
schirmer@12925
  1745
    case (Body D c s0 s1 s2 L accC T)
schirmer@12925
  1746
    with wf obtain n1 n2 where 
schirmer@12925
  1747
      "G\<turnstile>Norm s0 \<midarrow>Init D\<midarrow>n1\<rightarrow> s1"
schirmer@12925
  1748
      "G\<turnstile>s1 \<midarrow>c\<midarrow>n2\<rightarrow> s2"
schirmer@12925
  1749
      by (blast elim!: wt_elim_cases dest: eval_type_sound)
schirmer@12925
  1750
    then have 
schirmer@12925
  1751
     "G\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>the (locals (store s2) Result)\<midarrow>max n1 n2
schirmer@12925
  1752
       \<rightarrow> abupd (absorb Ret) s2"
schirmer@12925
  1753
      by (blast intro: evaln.Body dest: evaln_max2)
schirmer@12925
  1754
    then show ?case ..
schirmer@12925
  1755
  next
schirmer@12925
  1756
    case (LVar s vn L accC T)
schirmer@12925
  1757
    obtain n where
schirmer@12925
  1758
      "G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<midarrow>n\<rightarrow> Norm s"
schirmer@12925
  1759
      by (rules intro: evaln.LVar)
schirmer@12925
  1760
    then show ?case ..
schirmer@12925
  1761
  next
schirmer@12925
  1762
    case (FVar a accC e fn s0 s1 s2 s2' s3 stat statDeclC v L accC' T)
schirmer@12925
  1763
    have eval_init: "G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<rightarrow> s1" .
schirmer@12925
  1764
    have eval_e: "G\<turnstile>s1 \<midarrow>e-\<succ>a\<rightarrow> s2" .
schirmer@12925
  1765
    have check: "s3 = check_field_access G accC statDeclC fn stat a s2'" .
schirmer@12925
  1766
    have hyp_init: "PROP ?EqEval (Norm s0) s1 (In1r (Init statDeclC)) \<diamondsuit>" .
schirmer@12925
  1767
    have hyp_e: "PROP ?EqEval s1 s2 (In1l e) (In1 a)" .
schirmer@12925
  1768
    have fvar: "(v, s2') = fvar statDeclC stat fn a s2" .
schirmer@12925
  1769
    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
schirmer@12925
  1770
    have wt: "\<lparr>prg=G, cls=accC', lcl=L\<rparr>\<turnstile>In2 ({accC,statDeclC,stat}e..fn)\<Colon>T" .
schirmer@12925
  1771
    then obtain statC f where
schirmer@12925
  1772
                wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-Class statC" and
schirmer@12925
  1773
            accfield: "accfield G accC statC fn = Some (statDeclC,f)" and
schirmer@12925
  1774
                stat: "stat=is_static f" and
schirmer@12925
  1775
               accC': "accC'=accC" and
schirmer@12925
  1776
	           T: "T=(Inl (type f))"
schirmer@12925
  1777
       by (rule wt_elim_cases) (auto simp add: member_is_static_simp)
schirmer@12925
  1778
    from wf wt_e 
schirmer@12925
  1779
    have iscls_statC: "is_class G statC"
schirmer@12925
  1780
      by (auto dest: ty_expr_is_type type_is_class)
schirmer@12925
  1781
    with wf accfield 
schirmer@12925
  1782
    have iscls_statDeclC: "is_class G statDeclC"
schirmer@12925
  1783
      by (auto dest!: accfield_fields dest: fields_declC)
schirmer@12925
  1784
    then 
schirmer@12925
  1785
    have wt_init: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>(Init statDeclC)\<Colon>\<surd>"
schirmer@12925
  1786
      by simp
schirmer@12925
  1787
    from conf_s0 wt_init
schirmer@12925
  1788
    obtain n1 where
schirmer@12925
  1789
      evaln_init: "G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<midarrow>n1\<rightarrow> s1"
schirmer@12925
  1790
      by (rules dest: hyp_init)
schirmer@12925
  1791
    from eval_init wt_init conf_s0 wf 
schirmer@12925
  1792
    have conf_s1: "s1\<Colon>\<preceq>(G, L)"
schirmer@12925
  1793
      by (blast dest: eval_type_sound)
schirmer@12925
  1794
    with wt_e
schirmer@12925
  1795
    obtain n2 where
schirmer@12925
  1796
      evaln_e: "G\<turnstile>s1 \<midarrow>e-\<succ>a\<midarrow>n2\<rightarrow> s2"
schirmer@12925
  1797
      by (blast dest: hyp_e)
schirmer@12925
  1798
    from eval_e wf conf_s1 wt_e
schirmer@12925
  1799
    obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and
schirmer@12925
  1800
            conf_a: "normal s2 \<longrightarrow> G,store s2\<turnstile>a\<Colon>\<preceq>Class statC"
schirmer@12925
  1801
      by (auto dest!: eval_type_sound)
schirmer@12925
  1802
    from accfield wt_e eval_init eval_e conf_s2 conf_a fvar stat check  wf
schirmer@12925
  1803
    have eq_s3_s2': "s3=s2'"  
schirmer@12925
  1804
      by (auto dest!: error_free_field_access)
schirmer@12925
  1805
    with evaln_init evaln_e fvar accC'
schirmer@12925
  1806
    have "G\<turnstile>Norm s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>v\<midarrow>max n1 n2\<rightarrow> s3"
schirmer@12925
  1807
      by (auto intro: evaln.FVar dest: evaln_max2)
schirmer@12925
  1808
    then show ?case ..
schirmer@12925
  1809
  next
schirmer@12925
  1810
    case (AVar a e1 e2 i s0 s1 s2 s2' v L accC T)
schirmer@12925
  1811
    with wf obtain n1 n2 where 
schirmer@12925
  1812
      "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>a\<midarrow>n1\<rightarrow> s1"
schirmer@12925
  1813
      "G\<turnstile>s1 \<midarrow>e2-\<succ>i\<midarrow>n2\<rightarrow> s2"      
schirmer@12925
  1814
      by (blast elim!: wt_elim_cases dest: eval_type_sound)
schirmer@12925
  1815
    moreover 
schirmer@12925
  1816
    have "(v, s2') = avar G i a s2" .
schirmer@12925
  1817
    ultimately 
schirmer@12925
  1818
    have "G\<turnstile>Norm s0 \<midarrow>e1.[e2]=\<succ>v\<midarrow>max n1 n2\<rightarrow> s2'"
schirmer@12925
  1819
      by (blast intro!: evaln.AVar dest: evaln_max2)
schirmer@12925
  1820
    then show ?case ..
schirmer@12925
  1821
  next
schirmer@12925
  1822
    case (Nil s0 L accC T)
schirmer@12925
  1823
    show ?case by (rules intro: evaln.Nil)
schirmer@12925
  1824
  next
schirmer@12925
  1825
    case (Cons e es s0 s1 s2 v vs L accC T)
schirmer@12925
  1826
    with wf obtain n1 n2 where 
schirmer@12925
  1827
      "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n1\<rightarrow> s1"
schirmer@12925
  1828
      "G\<turnstile>s1 \<midarrow>es\<doteq>\<succ>vs\<midarrow>n2\<rightarrow> s2"      
schirmer@12925
  1829
      by (blast elim!: wt_elim_cases dest: eval_type_sound)
schirmer@12925
  1830
    then
schirmer@12925
  1831
    have "G\<turnstile>Norm s0 \<midarrow>e # es\<doteq>\<succ>v # vs\<midarrow>max n1 n2\<rightarrow> s2"
schirmer@12925
  1832
      by (blast intro!: evaln.Cons dest: evaln_max2)
schirmer@12925
  1833
    then show ?case ..
schirmer@12925
  1834
  qed
schirmer@12925
  1835
qed
schirmer@12925
  1836
schirmer@12854
  1837
end