src/HOL/Bali/Evaln.thy
changeset 13688 a0b16d42d489
parent 13601 fd3e3d6b37b2
child 13690 ac335b2f4a39
     1.1 --- a/src/HOL/Bali/Evaln.thy	Wed Oct 30 12:44:18 2002 +0100
     1.2 +++ b/src/HOL/Bali/Evaln.thy	Thu Oct 31 18:27:10 2002 +0100
     1.3 @@ -7,13 +7,26 @@
     1.4            statements
     1.5  *}
     1.6  
     1.7 -theory Evaln = Eval + TypeSafe:
     1.8 +theory Evaln = TypeSafe:
     1.9 +
    1.10  
    1.11  text {*
    1.12 -Variant of eval relation with counter for bounded recursive depth.
    1.13 -Evaln omits the technical accessibility tests @{term check_field_access}
    1.14 -and @{term check_method_access}, since we proved the absence of errors for
    1.15 -wellformed programs.
    1.16 +Variant of @{term eval} relation with counter for bounded recursive depth. 
    1.17 +In principal @{term evaln} could replace @{term eval}.
    1.18 +
    1.19 +Validity of the axiomatic semantics builds on @{term evaln}. 
    1.20 +For recursive method calls the axiomatic semantics rule assumes the method ok 
    1.21 +to derive a proof for the body. To prove the method rule sound we need to 
    1.22 +perform induction on the recursion depth. 
    1.23 +For the completeness proof of the axiomatic semantics the notion of the most
    1.24 +general formula is used. The most general formula right now builds on the 
    1.25 +ordinary evaluation relation @{term eval}. 
    1.26 +So sometimes we have to switch between @{term evaln} and @{term eval} and vice 
    1.27 +versa. To make
    1.28 +this switch easy @{term evaln} also does all the technical accessibility tests 
    1.29 +@{term check_field_access} and @{term check_method_access} like @{term eval}. 
    1.30 +If it would omit them @{term evaln} and @{term eval} would only be equivalent 
    1.31 +for welltyped, and definitely assigned terms.
    1.32  *}
    1.33  
    1.34  consts
    1.35 @@ -63,18 +76,19 @@
    1.36  
    1.37  inductive "evaln G" intros
    1.38  
    1.39 -(* propagation of abrupt completion *)
    1.40 +--{* propagation of abrupt completion *}
    1.41  
    1.42    Abrupt:   "G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (arbitrary3 t,(Some xc,s))"
    1.43  
    1.44  
    1.45 -(* evaluation of variables *)
    1.46 +--{* evaluation of variables *}
    1.47  
    1.48    LVar:	"G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<midarrow>n\<rightarrow> Norm s"
    1.49  
    1.50 -  FVar:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e-\<succ>a'\<midarrow>n\<rightarrow> s2;
    1.51 -	  (v,s2') = fvar statDeclC stat fn a' s2\<rbrakk> \<Longrightarrow>
    1.52 -	  G\<turnstile>Norm s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>v\<midarrow>n\<rightarrow> s2'"
    1.53 +  FVar:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e-\<succ>a\<midarrow>n\<rightarrow> s2;
    1.54 +	  (v,s2') = fvar statDeclC stat fn a s2;
    1.55 +          s3 = check_field_access G accC statDeclC fn stat a s2'\<rbrakk> \<Longrightarrow>
    1.56 +	  G\<turnstile>Norm s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>v\<midarrow>n\<rightarrow> s3"
    1.57  
    1.58    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; 
    1.59  	  (v,s2') = avar G i a s2\<rbrakk> \<Longrightarrow>
    1.60 @@ -83,7 +97,7 @@
    1.61  
    1.62  
    1.63  
    1.64 -(* evaluation of expressions *)
    1.65 +--{* evaluation of expressions *}
    1.66  
    1.67    NewC:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s1;
    1.68  	  G\<turnstile>     s1 \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s2\<rbrakk> \<Longrightarrow>
    1.69 @@ -127,19 +141,25 @@
    1.70    Call:	
    1.71    "\<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;
    1.72      D = invocation_declclass G mode (store s2) a' statT \<lparr>name=mn,parTs=pTs\<rparr>; 
    1.73 -    G\<turnstile>init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' vs s2
    1.74 -            \<midarrow>Methd D \<lparr>name=mn,parTs=pTs\<rparr>-\<succ>v\<midarrow>n\<rightarrow> s3\<rbrakk>
    1.75 +    s3=init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' vs s2;
    1.76 +    s3' = check_method_access G accC statT mode \<lparr>name=mn,parTs=pTs\<rparr> a' s3;
    1.77 +    G\<turnstile>s3'\<midarrow>Methd D \<lparr>name=mn,parTs=pTs\<rparr>-\<succ>v\<midarrow>n\<rightarrow> s4
    1.78 +   \<rbrakk>
    1.79     \<Longrightarrow> 
    1.80 -    G\<turnstile>Norm s0 \<midarrow>{accC,statT,mode}e\<cdot>mn({pTs}args)-\<succ>v\<midarrow>n\<rightarrow> (restore_lvars s2 s3)"
    1.81 +    G\<turnstile>Norm s0 \<midarrow>{accC,statT,mode}e\<cdot>mn({pTs}args)-\<succ>v\<midarrow>n\<rightarrow> (restore_lvars s2 s4)"
    1.82  
    1.83    Methd:"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
    1.84  				G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<midarrow>Suc n\<rightarrow> s1"
    1.85  
    1.86 -  Body:	"\<lbrakk>G\<turnstile>Norm s0\<midarrow>Init D\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c\<midarrow>n\<rightarrow> s2\<rbrakk>\<Longrightarrow>
    1.87 +  Body:	"\<lbrakk>G\<turnstile>Norm s0\<midarrow>Init D\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c\<midarrow>n\<rightarrow> s2;
    1.88 +          s3 = (if (\<exists> l. abrupt s2 = Some (Jump (Break l)) \<or>  
    1.89 +                         abrupt s2 = Some (Jump (Cont l)))
    1.90 +                  then abupd (\<lambda> x. Some (Error CrossMethodJump)) s2 
    1.91 +                  else s2)\<rbrakk>\<Longrightarrow>
    1.92           G\<turnstile>Norm s0 \<midarrow>Body D c
    1.93 -          -\<succ>the (locals (store s2) Result)\<midarrow>n\<rightarrow>abupd (absorb Ret) s2"
    1.94 +          -\<succ>the (locals (store s2) Result)\<midarrow>n\<rightarrow>abupd (absorb Ret) s3"
    1.95  
    1.96 -(* evaluation of expression lists *)
    1.97 +--{* evaluation of expression lists *}
    1.98  
    1.99    Nil:
   1.100  				"G\<turnstile>Norm s0 \<midarrow>[]\<doteq>\<succ>[]\<midarrow>n\<rightarrow> Norm s0"
   1.101 @@ -149,7 +169,7 @@
   1.102  			     G\<turnstile>Norm s0 \<midarrow>e#es\<doteq>\<succ>v#vs\<midarrow>n\<rightarrow> s2"
   1.103  
   1.104  
   1.105 -(* execution of statements *)
   1.106 +--{* execution of statements *}
   1.107  
   1.108    Skip:	 			    "G\<turnstile>Norm s \<midarrow>Skip\<midarrow>n\<rightarrow> Norm s"
   1.109  
   1.110 @@ -168,13 +188,13 @@
   1.111  		       G\<turnstile>Norm s0 \<midarrow>If(e) c1 Else c2 \<midarrow>n\<rightarrow> s2"
   1.112  
   1.113    Loop:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n\<rightarrow> s1;
   1.114 -	  if normal s1 \<and> the_Bool b 
   1.115 +	  if the_Bool b 
   1.116               then (G\<turnstile>s1 \<midarrow>c\<midarrow>n\<rightarrow> s2 \<and> 
   1.117                     G\<turnstile>(abupd (absorb (Cont l)) s2) \<midarrow>l\<bullet> While(e) c\<midarrow>n\<rightarrow> s3)
   1.118  	     else s3 = s1\<rbrakk> \<Longrightarrow>
   1.119  			      G\<turnstile>Norm s0 \<midarrow>l\<bullet> While(e) c\<midarrow>n\<rightarrow> s3"
   1.120    
   1.121 -  Do: "G\<turnstile>Norm s \<midarrow>Do j\<midarrow>n\<rightarrow> (Some (Jump j), s)"
   1.122 +  Jmp: "G\<turnstile>Norm s \<midarrow>Jmp j\<midarrow>n\<rightarrow> (Some (Jump j), s)"
   1.123    
   1.124    Throw:"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
   1.125  				 G\<turnstile>Norm s0 \<midarrow>Throw e\<midarrow>n\<rightarrow> abupd (throw a') s1"
   1.126 @@ -185,8 +205,11 @@
   1.127  		  G\<turnstile>Norm s0 \<midarrow>Try c1 Catch(tn vn) c2\<midarrow>n\<rightarrow> s3"
   1.128  
   1.129    Fin:	"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n\<rightarrow> (x1,s1);
   1.130 -	  G\<turnstile>Norm s1 \<midarrow>c2\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
   1.131 -              G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<midarrow>n\<rightarrow> abupd (abrupt_if (x1\<noteq>None) x1) s2"
   1.132 +	  G\<turnstile>Norm s1 \<midarrow>c2\<midarrow>n\<rightarrow> s2;
   1.133 +          s3=(if (\<exists> err. x1=Some (Error err)) 
   1.134 +              then (x1,s1) 
   1.135 +              else abupd (abrupt_if (x1\<noteq>None) x1) s2)\<rbrakk> \<Longrightarrow>
   1.136 +              G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<midarrow>n\<rightarrow> s3"
   1.137    
   1.138    Init:	"\<lbrakk>the (class G C) = c;
   1.139  	  if inited C (globs s0) then s3 = Norm s0
   1.140 @@ -202,12 +225,17 @@
   1.141  
   1.142  declare split_if     [split del] split_if_asm     [split del]
   1.143          option.split [split del] option.split_asm [split del]
   1.144 +        not_None_eq [simp del] 
   1.145 +        split_paired_All [simp del] split_paired_Ex [simp del]
   1.146 +ML_setup {*
   1.147 +simpset_ref() := simpset() delloop "split_all_tac"
   1.148 +*}
   1.149  inductive_cases evaln_cases: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> vs'"
   1.150  
   1.151  inductive_cases evaln_elim_cases:
   1.152  	"G\<turnstile>(Some xc, s) \<midarrow>t                        \<succ>\<midarrow>n\<rightarrow> vs'"
   1.153  	"G\<turnstile>Norm s \<midarrow>In1r Skip                      \<succ>\<midarrow>n\<rightarrow> xs'"
   1.154 -        "G\<turnstile>Norm s \<midarrow>In1r (Do j)                    \<succ>\<midarrow>n\<rightarrow> xs'"
   1.155 +        "G\<turnstile>Norm s \<midarrow>In1r (Jmp j)                   \<succ>\<midarrow>n\<rightarrow> xs'"
   1.156          "G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> c)                    \<succ>\<midarrow>n\<rightarrow> xs'"
   1.157  	"G\<turnstile>Norm s \<midarrow>In3  ([])                      \<succ>\<midarrow>n\<rightarrow> vs'"
   1.158  	"G\<turnstile>Norm s \<midarrow>In3  (e#es)                    \<succ>\<midarrow>n\<rightarrow> vs'"
   1.159 @@ -236,9 +264,15 @@
   1.160  	"G\<turnstile>Norm s \<midarrow>In2  (e1.[e2])                 \<succ>\<midarrow>n\<rightarrow> vs'"
   1.161  	"G\<turnstile>Norm s \<midarrow>In1l ({accC,statT,mode}e\<cdot>mn({pT}p)) \<succ>\<midarrow>n\<rightarrow> vs'"
   1.162  	"G\<turnstile>Norm s \<midarrow>In1r (Init C)                  \<succ>\<midarrow>n\<rightarrow> xs'"
   1.163 +        "G\<turnstile>Norm s \<midarrow>In1r (Init C)                  \<succ>\<midarrow>n\<rightarrow> xs'"
   1.164 +
   1.165  declare split_if     [split] split_if_asm     [split] 
   1.166          option.split [split] option.split_asm [split]
   1.167 -
   1.168 +        not_None_eq [simp] 
   1.169 +        split_paired_All [simp] split_paired_Ex [simp]
   1.170 +ML_setup {*
   1.171 +simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
   1.172 +*}
   1.173  lemma evaln_Inj_elim: "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (w,s') \<Longrightarrow> case t of In1 ec \<Rightarrow>  
   1.174    (case ec of Inl e \<Rightarrow> (\<exists>v. w = In1 v) | Inr c \<Rightarrow> w = \<diamondsuit>)  
   1.175    | In2 e \<Rightarrow> (\<exists>v. w = In2 v) | In3 e \<Rightarrow> (\<exists>v. w = In3 v)"
   1.176 @@ -248,6 +282,13 @@
   1.177  apply auto
   1.178  done
   1.179  
   1.180 +text {* The following simplification procedures set up the proper injections of
   1.181 + terms and their corresponding values in the evaluation relation:
   1.182 + E.g. an expression 
   1.183 + (injection @{term In1l} into terms) always evaluates to ordinary values 
   1.184 + (injection @{term In1} into generalised values @{term vals}). 
   1.185 +*}
   1.186 +
   1.187  ML_setup {*
   1.188  fun enf nam inj rhs =
   1.189  let
   1.190 @@ -390,663 +431,47 @@
   1.191  apply auto
   1.192  done
   1.193  
   1.194 -(* ##### FIXME: To WellType *)
   1.195 -lemma wt_elim_BinOp:
   1.196 -  "\<lbrakk>E,dt\<Turnstile>In1l (BinOp binop e1 e2)\<Colon>T;
   1.197 -    \<And>T1 T2 T3.
   1.198 -       \<lbrakk>E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2; wt_binop (prg E) binop T1 T2;
   1.199 -          E,dt\<Turnstile>(if b then In1l e2 else In1r Skip)\<Colon>T3;
   1.200 -          T = Inl (PrimT (binop_type binop))\<rbrakk>
   1.201 -       \<Longrightarrow> P\<rbrakk>
   1.202 -\<Longrightarrow> P"
   1.203 -apply (erule wt_elim_cases)
   1.204 -apply (cases b)
   1.205 -apply auto
   1.206 -done
   1.207 +
   1.208 +
   1.209  
   1.210  section {* evaln implies eval *}
   1.211 +
   1.212  lemma evaln_eval:  
   1.213 -  assumes evaln: "G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)" and
   1.214 -             wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T" and  
   1.215 -        conf_s0: "s0\<Colon>\<preceq>(G, L)" and
   1.216 -             wf: "wf_prog G" 
   1.217 -       
   1.218 +  assumes evaln: "G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)" 
   1.219    shows "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"
   1.220 -proof -
   1.221 -  from evaln 
   1.222 -  show "\<And> L accC T. \<lbrakk>s0\<Colon>\<preceq>(G, L);\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T\<rbrakk>
   1.223 -                    \<Longrightarrow> G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"
   1.224 -       (is "PROP ?EqEval s0 s1 t v")
   1.225 -  proof (induct)
   1.226 -    case Abrupt
   1.227 -    show ?case by (rule eval.Abrupt)
   1.228 -  next
   1.229 -    case LVar
   1.230 -    show ?case by (rule eval.LVar)
   1.231 -  next
   1.232 -    case (FVar a accC' e fn n s0 s1 s2 s2' stat statDeclC v L accC T)
   1.233 -    have eval_initn: "G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<midarrow>n\<rightarrow> s1" .
   1.234 -    have eval_en: "G\<turnstile>s1 \<midarrow>e-\<succ>a\<midarrow>n\<rightarrow> s2" .
   1.235 -    have hyp_init: "PROP ?EqEval (Norm s0) s1 (In1r (Init statDeclC)) \<diamondsuit>" .
   1.236 -    have hyp_e: "PROP ?EqEval s1 s2 (In1l e) (In1 a)" .
   1.237 -    have fvar: "(v, s2') = fvar statDeclC stat fn a s2" .
   1.238 -    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
   1.239 -    have wt: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>In2 ({accC',statDeclC,stat}e..fn)\<Colon>T" .
   1.240 -    then obtain statC f where
   1.241 -                wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-Class statC" and
   1.242 -            accfield: "accfield G accC statC fn = Some (statDeclC,f)" and
   1.243 -                stat: "stat=is_static f" and
   1.244 -               accC': "accC'=accC" and
   1.245 -	           T: "T=(Inl (type f))"
   1.246 -       by (rule wt_elim_cases) (auto simp add: member_is_static_simp)
   1.247 -    from wf wt_e 
   1.248 -    have iscls_statC: "is_class G statC"
   1.249 -      by (auto dest: ty_expr_is_type type_is_class)
   1.250 -    with wf accfield 
   1.251 -    have iscls_statDeclC: "is_class G statDeclC"
   1.252 -      by (auto dest!: accfield_fields dest: fields_declC)
   1.253 -    then 
   1.254 -    have wt_init: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>(Init statDeclC)\<Colon>\<surd>"
   1.255 -      by simp
   1.256 -    from conf_s0 wt_init
   1.257 -    have eval_init: "G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<rightarrow> s1"
   1.258 -      by (rule hyp_init)
   1.259 -    with wt_init conf_s0 wf 
   1.260 -    have conf_s1: "s1\<Colon>\<preceq>(G, L)"
   1.261 -      by (blast dest: exec_ts)
   1.262 -    with hyp_e wt_e
   1.263 -    have eval_e: "G\<turnstile>s1 \<midarrow>e-\<succ>a\<rightarrow> s2"
   1.264 -      by blast
   1.265 -    with wf conf_s1 wt_e
   1.266 -    obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and
   1.267 -            conf_a: "normal s2 \<longrightarrow> G,store s2\<turnstile>a\<Colon>\<preceq>Class statC"
   1.268 -      by (auto dest!: eval_type_sound)
   1.269 -    obtain s3 where
   1.270 -      check: "s3 = check_field_access G accC statDeclC fn stat a s2'"
   1.271 -      by simp
   1.272 -    from accfield wt_e eval_init eval_e conf_s2 conf_a fvar stat check  wf
   1.273 -    have eq_s3_s2': "s3=s2'"  
   1.274 -      by (auto dest!: error_free_field_access)
   1.275 -    with eval_init eval_e fvar check accC'
   1.276 -    show "G\<turnstile>Norm s0 \<midarrow>{accC',statDeclC,stat}e..fn=\<succ>v\<rightarrow> s2'"
   1.277 -      by (auto intro: eval.FVar)
   1.278 -  next
   1.279 -    case AVar
   1.280 -    with wf show ?case
   1.281 -      apply -
   1.282 -      apply (erule wt_elim_cases)
   1.283 -      apply (blast intro!: eval.AVar dest: eval_type_sound)
   1.284 -      done
   1.285 -  next
   1.286 -    case NewC
   1.287 -    with wf show ?case
   1.288 -      apply - 
   1.289 -      apply (erule wt_elim_cases)
   1.290 -      apply (blast intro!: eval.NewC dest: eval_type_sound is_acc_classD)
   1.291 -      done
   1.292 -  next
   1.293 -    case (NewA T a e i n s0 s1 s2 s3 L accC Ta) 
   1.294 -    have hyp_init: "PROP ?EqEval (Norm s0) s1 (In1r (init_comp_ty T)) \<diamondsuit>" .
   1.295 -    have hyp_size: "PROP ?EqEval s1 s2 (In1l e) (In1 i)" .
   1.296 -    have "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (New T[e])\<Colon>Ta" .
   1.297 -    then obtain
   1.298 -       wt_init: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>init_comp_ty T\<Colon>\<surd>" and
   1.299 -       wt_size: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-PrimT Integer"
   1.300 -      by (rule wt_elim_cases) (auto intro: wt_init_comp_ty dest: is_acc_typeD)
   1.301 -    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
   1.302 -    from this wt_init 
   1.303 -    have eval_init: "G\<turnstile>Norm s0 \<midarrow>init_comp_ty T\<rightarrow> s1"
   1.304 -      by (rule hyp_init)
   1.305 -    moreover
   1.306 -    from eval_init wt_init wf conf_s0
   1.307 -    have "s1\<Colon>\<preceq>(G, L)"
   1.308 -      by (auto dest: eval_type_sound)
   1.309 -    from this wt_size 
   1.310 -    have "G\<turnstile>s1 \<midarrow>e-\<succ>i\<rightarrow> s2"
   1.311 -      by (rule hyp_size)
   1.312 -    moreover note NewA
   1.313 -    ultimately show ?case
   1.314 -      by (blast intro!: eval.NewA)
   1.315 -  next
   1.316 -    case Cast
   1.317 -    with wf show ?case
   1.318 -      by - (erule wt_elim_cases, rule eval.Cast,auto dest: eval_type_sound)
   1.319 -  next
   1.320 -    case Inst
   1.321 -    with wf show ?case
   1.322 -      by - (erule wt_elim_cases, rule eval.Inst,auto dest: eval_type_sound)
   1.323 -  next
   1.324 -    case Lit
   1.325 -    show ?case by (rule eval.Lit)
   1.326 -  next
   1.327 -    case UnOp
   1.328 -    with wf show ?case
   1.329 -      by - (erule wt_elim_cases, rule eval.UnOp,auto dest: eval_type_sound)
   1.330 -  next
   1.331 -    case BinOp
   1.332 -    with wf show ?case 
   1.333 -      by - (erule wt_elim_BinOp, blast intro!: eval.BinOp dest: eval_type_sound)
   1.334 -  next
   1.335 -    case Super
   1.336 -    show ?case by (rule eval.Super)
   1.337 -  next
   1.338 -    case Acc
   1.339 -    then show ?case
   1.340 -      by - (erule wt_elim_cases, rule eval.Acc,auto dest: eval_type_sound)
   1.341 -  next
   1.342 -    case Ass
   1.343 -    with wf show ?case
   1.344 -      by - (erule wt_elim_cases, blast intro!: eval.Ass dest: eval_type_sound) 
   1.345 -  next
   1.346 -    case (Cond b e0 e1 e2 n s0 s1 s2 v L accC T)
   1.347 -    have hyp_e0: "PROP ?EqEval (Norm s0) s1 (In1l e0) (In1 b)" .
   1.348 -    have hyp_if: "PROP ?EqEval s1 s2 
   1.349 -                              (In1l (if the_Bool b then e1 else e2)) (In1 v)" .
   1.350 -    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
   1.351 -    have wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (e0 ? e1 : e2)\<Colon>T" .
   1.352 -    then obtain T1 T2 statT where
   1.353 -       wt_e0: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e0\<Colon>-PrimT Boolean" and
   1.354 -       wt_e1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e1\<Colon>-T1" and
   1.355 -       wt_e2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e2\<Colon>-T2" and 
   1.356 -       statT: "G\<turnstile>T1\<preceq>T2 \<and> statT = T2  \<or>  G\<turnstile>T2\<preceq>T1 \<and> statT =  T1" and
   1.357 -       T    : "T=Inl statT"
   1.358 -      by (rule wt_elim_cases) auto
   1.359 -    from conf_s0 wt_e0
   1.360 -    have eval_e0: "G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1"
   1.361 -      by (rule hyp_e0)
   1.362 -    moreover
   1.363 -    from eval_e0 conf_s0 wf wt_e0
   1.364 -    have "s1\<Colon>\<preceq>(G, L)"
   1.365 -      by (blast dest: eval_type_sound)
   1.366 -    with wt_e1 wt_e2 statT hyp_if
   1.367 -    have "G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<rightarrow> s2"
   1.368 -      by (cases "the_Bool b") auto
   1.369 -    ultimately
   1.370 -    show ?case
   1.371 -      by (rule eval.Cond)
   1.372 -  next
   1.373 -    case (Call invDeclC a' accC' args e mn mode n pTs' s0 s1 s2 s4 statT 
   1.374 -           v vs L accC T)
   1.375 -    txt {* Repeats large parts of the type soundness proof. One should factor
   1.376 -      out some lemmata about the relations and conformance of @{text
   1.377 -      s2}, @{text s3} and @{text s3'} *}
   1.378 -    have evaln_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n\<rightarrow> s1" .
   1.379 -    have evaln_args: "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<midarrow>n\<rightarrow> s2" .
   1.380 -    have invDeclC: "invDeclC 
   1.381 -                      = invocation_declclass G mode (store s2) a' statT 
   1.382 -                           \<lparr>name = mn, parTs = pTs'\<rparr>" .
   1.383 -    let ?InitLvars 
   1.384 -         = "init_lvars G invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> mode a' vs s2"
   1.385 -    obtain s3 s3' where 
   1.386 -      init_lvars: "s3 = 
   1.387 -             init_lvars G invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> mode a' vs s2" and
   1.388 -      check: "s3' =
   1.389 -         check_method_access G accC' statT mode \<lparr>name = mn, parTs = pTs'\<rparr> a' s3"
   1.390 -      by simp
   1.391 -    have evaln_methd: 
   1.392 -     "G\<turnstile>?InitLvars \<midarrow>Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>-\<succ>v\<midarrow>n\<rightarrow> s4" .
   1.393 -    have     hyp_e: "PROP ?EqEval (Norm s0) s1 (In1l e) (In1 a')" .
   1.394 -    have  hyp_args: "PROP ?EqEval s1 s2 (In3 args) (In3 vs)" .
   1.395 -    have hyp_methd: "PROP ?EqEval ?InitLvars s4 
   1.396 -              (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)) (In1 v)".
   1.397 -    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
   1.398 -    have      wt: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>
   1.399 -                    \<turnstile>In1l ({accC',statT,mode}e\<cdot>mn( {pTs'}args))\<Colon>T" .
   1.400 -    from wt obtain pTs statDeclT statM where
   1.401 -                 wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT" and
   1.402 -              wt_args: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>args\<Colon>\<doteq>pTs" and
   1.403 -                statM: "max_spec G accC statT \<lparr>name=mn,parTs=pTs\<rparr> 
   1.404 -                         = {((statDeclT,statM),pTs')}" and
   1.405 -                 mode: "mode = invmode statM e" and
   1.406 -                    T: "T =Inl (resTy statM)" and
   1.407 -        eq_accC_accC': "accC=accC'"
   1.408 -      by (rule wt_elim_cases) fastsimp+
   1.409 -    from conf_s0 wt_e hyp_e
   1.410 -    have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1"
   1.411 -      by blast
   1.412 -    with wf conf_s0 wt_e
   1.413 -    obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and
   1.414 -           conf_a': "normal s1 \<Longrightarrow> G, store s1\<turnstile>a'\<Colon>\<preceq>RefT statT" 
   1.415 -      by (auto dest!: eval_type_sound)
   1.416 -    from conf_s1 wt_args hyp_args
   1.417 -    have eval_args: "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<rightarrow> s2"
   1.418 -      by blast
   1.419 -    with wt_args conf_s1 wf 
   1.420 -    obtain    conf_s2: "s2\<Colon>\<preceq>(G, L)" and
   1.421 -            conf_args: "normal s2 
   1.422 -                         \<Longrightarrow>  list_all2 (conf G (store s2)) vs pTs" 
   1.423 -      by (auto dest!: eval_type_sound)
   1.424 -    from statM 
   1.425 -    obtain
   1.426 -       statM': "(statDeclT,statM)\<in>mheads G accC statT \<lparr>name=mn,parTs=pTs'\<rparr>" and
   1.427 -       pTs_widen: "G\<turnstile>pTs[\<preceq>]pTs'"
   1.428 -      by (blast dest: max_spec2mheads)
   1.429 -    from check
   1.430 -    have eq_store_s3'_s3: "store s3'=store s3"
   1.431 -      by (cases s3) (simp add: check_method_access_def Let_def)
   1.432 -    obtain invC
   1.433 -      where invC: "invC = invocation_class mode (store s2) a' statT"
   1.434 -      by simp
   1.435 -    with init_lvars
   1.436 -    have invC': "invC = (invocation_class mode (store s3) a' statT)"
   1.437 -      by (cases s2,cases mode) (auto simp add: init_lvars_def2 )
   1.438 -    show "G\<turnstile>Norm s0 \<midarrow>{accC',statT,mode}e\<cdot>mn( {pTs'}args)
   1.439 -             -\<succ>v\<rightarrow> (set_lvars (locals (store s2))) s4"
   1.440 -    proof (cases "normal s2")
   1.441 -      case False
   1.442 -      with init_lvars 
   1.443 -      obtain keep_abrupt: "abrupt s3 = abrupt s2" and
   1.444 -             "store s3 = store (init_lvars G invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> 
   1.445 -                                            mode a' vs s2)" 
   1.446 -	by (auto simp add: init_lvars_def2)
   1.447 -      moreover
   1.448 -      from keep_abrupt False check
   1.449 -      have eq_s3'_s3: "s3'=s3" 
   1.450 -	by (auto simp add: check_method_access_def Let_def)
   1.451 -      moreover
   1.452 -      from eq_s3'_s3 False keep_abrupt evaln_methd init_lvars
   1.453 -      obtain "s4=s3'"
   1.454 -      "In1 v=arbitrary3 (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>))"
   1.455 -	by auto
   1.456 -      moreover note False
   1.457 -      ultimately have
   1.458 -	"G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>-\<succ>v\<rightarrow> s4"
   1.459 -	by (auto)
   1.460 -      from eval_e eval_args invDeclC init_lvars check this
   1.461 -      show ?thesis
   1.462 -	by (rule eval.Call)
   1.463 -    next
   1.464 -      case True
   1.465 -      note normal_s2 = True
   1.466 -      with eval_args
   1.467 -      have normal_s1: "normal s1"
   1.468 -	by (cases "normal s1") auto
   1.469 -      with conf_a' eval_args 
   1.470 -      have conf_a'_s2: "G, store s2\<turnstile>a'\<Colon>\<preceq>RefT statT"
   1.471 -	by (auto dest: eval_gext intro: conf_gext)
   1.472 -      show ?thesis
   1.473 -      proof (cases "a'=Null \<longrightarrow> is_static statM")
   1.474 -	case False
   1.475 -	then obtain not_static: "\<not> is_static statM" and Null: "a'=Null" 
   1.476 -	  by blast
   1.477 -	with normal_s2 init_lvars mode
   1.478 -	obtain np: "abrupt s3 = Some (Xcpt (Std NullPointer))" and
   1.479 -                   "store s3 = store (init_lvars G invDeclC 
   1.480 -                                       \<lparr>name = mn, parTs = pTs'\<rparr> mode a' vs s2)"
   1.481 -	  by (auto simp add: init_lvars_def2)
   1.482 -	moreover
   1.483 -	from np check
   1.484 -	have eq_s3'_s3: "s3'=s3" 
   1.485 -	  by (auto simp add: check_method_access_def Let_def)
   1.486 -	moreover
   1.487 -	from eq_s3'_s3 np evaln_methd init_lvars
   1.488 -	obtain "s4=s3'"
   1.489 -      "In1 v=arbitrary3 (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>))"
   1.490 -	  by auto
   1.491 -	moreover note np 
   1.492 -	ultimately have
   1.493 -	  "G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>-\<succ>v\<rightarrow> s4"
   1.494 -	  by (auto)
   1.495 -	from eval_e eval_args invDeclC init_lvars check this
   1.496 -	show ?thesis
   1.497 -	  by (rule eval.Call)
   1.498 -      next
   1.499 -	case True
   1.500 -	with mode have notNull: "mode = IntVir \<longrightarrow> a' \<noteq> Null"
   1.501 -	  by (auto dest!: Null_staticD)
   1.502 -	with conf_s2 conf_a'_s2 wf invC 
   1.503 -	have dynT_prop: "G\<turnstile>mode\<rightarrow>invC\<preceq>statT"
   1.504 -	  by (cases s2) (auto intro: DynT_propI)
   1.505 -	with wt_e statM' invC mode wf 
   1.506 -	obtain dynM where 
   1.507 -           dynM: "dynlookup G statT invC  \<lparr>name=mn,parTs=pTs'\<rparr> = Some dynM" and
   1.508 -           acc_dynM: "G \<turnstile>Methd  \<lparr>name=mn,parTs=pTs'\<rparr> dynM 
   1.509 -                          in invC dyn_accessible_from accC"
   1.510 -	  by (force dest!: call_access_ok)
   1.511 -	with invC' check eq_accC_accC'
   1.512 -	have eq_s3'_s3: "s3'=s3"
   1.513 -	  by (auto simp add: check_method_access_def Let_def)
   1.514 -	from dynT_prop wf wt_e statM' mode invC invDeclC dynM 
   1.515 -	obtain 
   1.516 -	   wf_dynM: "wf_mdecl G invDeclC (\<lparr>name=mn,parTs=pTs'\<rparr>,mthd dynM)" and
   1.517 -	     dynM': "methd G invDeclC \<lparr>name=mn,parTs=pTs'\<rparr> = Some dynM" and
   1.518 -           iscls_invDeclC: "is_class G invDeclC" and
   1.519 -	        invDeclC': "invDeclC = declclass dynM" and
   1.520 -	     invC_widen: "G\<turnstile>invC\<preceq>\<^sub>C invDeclC" and
   1.521 -	   is_static_eq: "is_static dynM = is_static statM" and
   1.522 -	   involved_classes_prop:
   1.523 -             "(if invmode statM e = IntVir
   1.524 -               then \<forall>statC. statT = ClassT statC \<longrightarrow> G\<turnstile>invC\<preceq>\<^sub>C statC
   1.525 -               else ((\<exists>statC. statT = ClassT statC \<and> G\<turnstile>statC\<preceq>\<^sub>C invDeclC) \<or>
   1.526 -                     (\<forall>statC. statT \<noteq> ClassT statC \<and> invDeclC = Object)) \<and>
   1.527 -                      statDeclT = ClassT invDeclC)"
   1.528 -	  by (auto dest: DynT_mheadsD)
   1.529 -	obtain L' where 
   1.530 -	   L':"L'=(\<lambda> k. 
   1.531 -                 (case k of
   1.532 -                    EName e
   1.533 -                    \<Rightarrow> (case e of 
   1.534 -                          VNam v 
   1.535 -                          \<Rightarrow>(table_of (lcls (mbody (mthd dynM)))
   1.536 -                             (pars (mthd dynM)[\<mapsto>]pTs')) v
   1.537 -                        | Res \<Rightarrow> Some (resTy dynM))
   1.538 -                  | This \<Rightarrow> if is_static statM 
   1.539 -                            then None else Some (Class invDeclC)))"
   1.540 -	  by simp
   1.541 -	from wf_dynM [THEN wf_mdeclD1, THEN conjunct1] normal_s2 conf_s2 wt_e
   1.542 -              wf eval_args conf_a' mode notNull wf_dynM involved_classes_prop
   1.543 -	have conf_s3: "s3\<Colon>\<preceq>(G,L')"
   1.544 -	   apply - 
   1.545 -          (*FIXME confomrs_init_lvars should be 
   1.546 -                adjusted to be more directy applicable *)
   1.547 -	   apply (drule conforms_init_lvars [of G invDeclC 
   1.548 -                  "\<lparr>name=mn,parTs=pTs'\<rparr>" dynM "store s2" vs pTs "abrupt s2" 
   1.549 -                  L statT invC a' "(statDeclT,statM)" e])
   1.550 -	     apply (rule wf)
   1.551 -	     apply (rule conf_args,assumption)
   1.552 -	     apply (simp add: pTs_widen)
   1.553 -	     apply (cases s2,simp)
   1.554 -	     apply (rule dynM')
   1.555 -	     apply (force dest: ty_expr_is_type)
   1.556 -	     apply (rule invC_widen)
   1.557 -	     apply (force intro: conf_gext dest: eval_gext)
   1.558 -	     apply simp
   1.559 -	     apply simp
   1.560 -	     apply (simp add: invC)
   1.561 -	     apply (simp add: invDeclC)
   1.562 -	     apply (force dest: wf_mdeclD1 is_acc_typeD)
   1.563 -	     apply (cases s2, simp add: L' init_lvars
   1.564 -	                      cong add: lname.case_cong ename.case_cong)
   1.565 -	   done
   1.566 -	from is_static_eq wf_dynM L'
   1.567 -	obtain mthdT where
   1.568 -	   "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>
   1.569 -            \<turnstile>Body invDeclC (stmt (mbody (mthd dynM)))\<Colon>-mthdT" and
   1.570 -	   mthdT_widen: "G\<turnstile>mthdT\<preceq>resTy dynM"
   1.571 -	  by - (drule wf_mdecl_bodyD,
   1.572 -                auto simp: cong add: lname.case_cong ename.case_cong)
   1.573 -	with dynM' iscls_invDeclC invDeclC'
   1.574 -	have
   1.575 -	   "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>
   1.576 -            \<turnstile>(Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)\<Colon>-mthdT"
   1.577 -	  by (auto intro: wt.Methd)
   1.578 -	with conf_s3 hyp_methd init_lvars eq_s3'_s3
   1.579 -	have "G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>-\<succ>v\<rightarrow> s4"
   1.580 -	  by auto
   1.581 -	from eval_e eval_args invDeclC init_lvars check this
   1.582 -	show ?thesis
   1.583 -	  by (rule eval.Call)
   1.584 -      qed
   1.585 -    qed
   1.586 -  next
   1.587 -    case Methd
   1.588 -    with wf show ?case
   1.589 -      by - (erule wt_elim_cases, rule eval.Methd, 
   1.590 -            auto dest: eval_type_sound simp add: body_def2)
   1.591 -  next
   1.592 -    case Body
   1.593 -    with wf show ?case
   1.594 -       by - (erule wt_elim_cases, blast intro!: eval.Body dest: eval_type_sound)
   1.595 -  next
   1.596 -    case Nil
   1.597 -    show ?case by (rule eval.Nil)
   1.598 -  next
   1.599 -    case Cons
   1.600 -    with wf show ?case
   1.601 -      by - (erule wt_elim_cases, blast intro!: eval.Cons dest: eval_type_sound)
   1.602 -  next
   1.603 -    case Skip
   1.604 -    show ?case by (rule eval.Skip)
   1.605 -  next
   1.606 -    case Expr
   1.607 -    with wf show ?case
   1.608 -      by - (erule wt_elim_cases, rule eval.Expr,auto dest: eval_type_sound)
   1.609 -  next
   1.610 -    case Lab
   1.611 -    with wf show ?case
   1.612 -      by - (erule wt_elim_cases, rule eval.Lab,auto dest: eval_type_sound)
   1.613 -  next
   1.614 -    case Comp
   1.615 -    with wf show ?case
   1.616 -      by - (erule wt_elim_cases, blast intro!: eval.Comp dest: eval_type_sound)
   1.617 -  next
   1.618 -    case (If b c1 c2 e n s0 s1 s2 L accC T)
   1.619 -    have hyp_e: "PROP ?EqEval (Norm s0) s1 (In1l e) (In1 b)" .
   1.620 -    have hyp_then_else: 
   1.621 -      "PROP ?EqEval s1 s2 (In1r (if the_Bool b then c1 else c2)) \<diamondsuit>" .
   1.622 -    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
   1.623 -    have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (If(e) c1 Else c2)\<Colon>T" .
   1.624 -    then obtain 
   1.625 -              wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean" and
   1.626 -      wt_then_else: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>(if the_Bool b then c1 else c2)\<Colon>\<surd>"
   1.627 -      by (rule wt_elim_cases) (auto split add: split_if)
   1.628 -    from conf_s0 wt_e
   1.629 -    have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1"
   1.630 -      by (rule hyp_e)
   1.631 -    moreover
   1.632 -    from eval_e wt_e conf_s0 wf
   1.633 -    have "s1\<Colon>\<preceq>(G, L)"
   1.634 -      by (blast dest: eval_type_sound)
   1.635 -    from this wt_then_else
   1.636 -    have "G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2"
   1.637 -      by (rule hyp_then_else)
   1.638 -    ultimately
   1.639 -    show ?case
   1.640 -      by (rule eval.If)
   1.641 -  next
   1.642 -    case (Loop b c e l n s0 s1 s2 s3 L accC T)
   1.643 -    have hyp_e: "PROP ?EqEval (Norm s0) s1 (In1l e) (In1 b)" .
   1.644 -    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
   1.645 -    have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (l\<bullet> While(e) c)\<Colon>T" .
   1.646 -    then obtain wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean" and
   1.647 -                wt_c: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c\<Colon>\<surd>"
   1.648 -      by (rule wt_elim_cases) (blast)
   1.649 -    from conf_s0 wt_e 
   1.650 -    have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1"
   1.651 -      by (rule hyp_e)
   1.652 -    moreover
   1.653 -    from eval_e wt_e conf_s0 wf
   1.654 -    have conf_s1: "s1\<Colon>\<preceq>(G, L)"
   1.655 -      by (blast dest: eval_type_sound)
   1.656 -    have "if normal s1 \<and> the_Bool b 
   1.657 -             then (G\<turnstile>s1 \<midarrow>c\<rightarrow> s2 \<and> 
   1.658 -                   G\<turnstile>(abupd (absorb (Cont l)) s2) \<midarrow>l\<bullet> While(e) c\<rightarrow> s3)
   1.659 -	     else s3 = s1"
   1.660 -    proof (cases "normal s1 \<and> the_Bool b")
   1.661 -      case True 
   1.662 -      from Loop True have hyp_c: "PROP ?EqEval s1 s2 (In1r c) \<diamondsuit>"
   1.663 -	by (auto)
   1.664 -      from Loop True have hyp_w: "PROP ?EqEval (abupd (absorb (Cont l)) s2)
   1.665 -                                        s3 (In1r (l\<bullet> While(e) c)) \<diamondsuit>"
   1.666 -	by (auto)
   1.667 -      from conf_s1 wt_c
   1.668 -      have eval_c: "G\<turnstile>s1 \<midarrow>c\<rightarrow> s2"
   1.669 -	by (rule hyp_c)
   1.670 -      moreover
   1.671 -      from eval_c conf_s1 wt_c wf
   1.672 -      have "s2\<Colon>\<preceq>(G, L)"
   1.673 -	by (blast dest: eval_type_sound)
   1.674 -      then
   1.675 -      have "abupd (absorb (Cont l)) s2 \<Colon>\<preceq>(G, L)"
   1.676 -	by (cases s2) (auto intro: conforms_absorb)
   1.677 -      from this and wt
   1.678 -      have "G\<turnstile>abupd (absorb (Cont l)) s2 \<midarrow>l\<bullet> While(e) c\<rightarrow> s3"
   1.679 -	by (rule hyp_w)
   1.680 -      moreover note True
   1.681 -      ultimately
   1.682 -      show ?thesis
   1.683 -	by simp
   1.684 -    next
   1.685 -      case False
   1.686 -      with Loop have "s3 = s1" by simp
   1.687 -      with False
   1.688 -      show ?thesis 
   1.689 -	by auto
   1.690 -    qed
   1.691 -    ultimately
   1.692 -    show ?case
   1.693 -      by (rule eval.Loop)
   1.694 -  next
   1.695 -    case Do
   1.696 -    show ?case by (rule eval.Do)
   1.697 -  next
   1.698 -    case Throw
   1.699 -    with wf show ?case
   1.700 -      by - (erule wt_elim_cases, rule eval.Throw,auto dest: eval_type_sound)
   1.701 -  next
   1.702 -    case (Try c1 c2 n s0 s1 s2 s3 catchC vn L accC T)
   1.703 -    have  hyp_c1: "PROP ?EqEval (Norm s0) s1 (In1r c1) \<diamondsuit>" .
   1.704 -    have conf_s0:"Norm s0\<Colon>\<preceq>(G, L)" .
   1.705 -    have      wt:"\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>In1r (Try c1 Catch(catchC vn) c2)\<Colon>T" .
   1.706 -    then obtain 
   1.707 -      wt_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
   1.708 -      wt_c2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<lparr>lcl := L(VName vn\<mapsto>Class catchC)\<rparr>\<turnstile>c2\<Colon>\<surd>"
   1.709 -      by (rule wt_elim_cases) (auto)
   1.710 -    from conf_s0 wt_c1
   1.711 -    have eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1"
   1.712 -      by (rule hyp_c1)
   1.713 -    moreover
   1.714 -    have sxalloc: "G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2" .
   1.715 -    moreover
   1.716 -    from eval_c1 wt_c1 conf_s0 wf
   1.717 -    have "s1\<Colon>\<preceq>(G, L)"
   1.718 -      by (blast dest: eval_type_sound)
   1.719 -    with sxalloc wf
   1.720 -    have conf_s2: "s2\<Colon>\<preceq>(G, L)" 
   1.721 -      by (auto dest: sxalloc_type_sound split: option.splits)
   1.722 -    have "if G,s2\<turnstile>catch catchC then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<rightarrow> s3 else s3 = s2"
   1.723 -    proof (cases "G,s2\<turnstile>catch catchC")
   1.724 -      case True
   1.725 -      note Catch = this
   1.726 -      with Try have hyp_c2: "PROP ?EqEval (new_xcpt_var vn s2) s3 (In1r c2) \<diamondsuit>"
   1.727 -	by auto
   1.728 -      show ?thesis
   1.729 -      proof (cases "normal s1")
   1.730 -	case True
   1.731 -	with sxalloc wf 
   1.732 -	have eq_s2_s1: "s2=s1"
   1.733 -	  by (auto dest: sxalloc_type_sound split: option.splits)
   1.734 -	with True 
   1.735 -	have "\<not>  G,s2\<turnstile>catch catchC"
   1.736 -	  by (simp add: catch_def)
   1.737 -	with Catch show ?thesis 
   1.738 -	  by (contradiction)
   1.739 -      next 
   1.740 -	case False
   1.741 -	with sxalloc wf
   1.742 -	obtain a 
   1.743 -	  where xcpt_s2: "abrupt s2 = Some (Xcpt (Loc a))"
   1.744 -	  by (auto dest!: sxalloc_type_sound split: option.splits)
   1.745 -	with Catch
   1.746 -	have "G\<turnstile>obj_ty (the (globs (store s2) (Heap a)))\<preceq>Class catchC"
   1.747 -	  by (cases s2) simp
   1.748 -	with xcpt_s2 conf_s2 wf 
   1.749 -	have "new_xcpt_var vn s2\<Colon>\<preceq>(G, L(VName vn\<mapsto>Class catchC))"
   1.750 -	  by (auto dest: Try_lemma)
   1.751 -	from this wt_c2
   1.752 -	have "G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<rightarrow> s3"
   1.753 -	  by (auto intro: hyp_c2)
   1.754 -	with Catch 
   1.755 -	show ?thesis
   1.756 -	  by simp
   1.757 -      qed
   1.758 -    next
   1.759 -      case False
   1.760 -      with Try
   1.761 -      have "s3=s2"
   1.762 -	by simp
   1.763 -      with False
   1.764 -      show ?thesis
   1.765 -	by simp
   1.766 -    qed
   1.767 -    ultimately
   1.768 -    show ?case
   1.769 -      by (rule eval.Try)
   1.770 -  next
   1.771 -    case (Fin c1 c2 n s0 s1 s2 x1 L accC T)
   1.772 -    have hyp_c1: "PROP ?EqEval (Norm s0) (x1,s1) (In1r c1) \<diamondsuit>" .
   1.773 -    have hyp_c2: "PROP ?EqEval (Norm s1) (s2) (In1r c2) \<diamondsuit>" .
   1.774 -    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
   1.775 -    have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (c1 Finally c2)\<Colon>T" .
   1.776 -    then obtain
   1.777 -      wt_c1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
   1.778 -      wt_c2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c2\<Colon>\<surd>" 
   1.779 -      by (rule wt_elim_cases) blast
   1.780 -    from conf_s0 wt_c1
   1.781 -    have eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1, s1)"
   1.782 -      by (rule hyp_c1)
   1.783 -    with wf wt_c1 conf_s0
   1.784 -    obtain       conf_s1: "Norm s1\<Colon>\<preceq>(G, L)" and 
   1.785 -           error_free_s1: "error_free (x1,s1)"
   1.786 -      by (auto dest!: eval_type_sound intro: conforms_NormI)
   1.787 -    from conf_s1 wt_c2
   1.788 -    have eval_c2: "G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2"
   1.789 -      by (rule hyp_c2)
   1.790 -    with eval_c1 error_free_s1
   1.791 -    show "G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<rightarrow> abupd (abrupt_if (x1 \<noteq> None) x1) s2"
   1.792 -      by (auto intro: eval.Fin simp add: error_free_def)
   1.793 -  next
   1.794 -    case (Init C c n s0 s1 s2 s3 L accC T)
   1.795 -    have     cls: "the (class G C) = c" .
   1.796 -    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
   1.797 -    have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (Init C)\<Colon>T" .
   1.798 -    with cls
   1.799 -    have cls_C: "class G C = Some c"
   1.800 -      by - (erule wt_elim_cases,auto)
   1.801 -    have "if inited C (globs s0) then s3 = Norm s0
   1.802 -	  else (G\<turnstile>Norm (init_class_obj G C s0) 
   1.803 -		  \<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1 \<and>
   1.804 -	       G\<turnstile>set_lvars empty s1 \<midarrow>init c\<rightarrow> s2 \<and> s3 = restore_lvars s1 s2)"
   1.805 -    proof (cases "inited C (globs s0)")
   1.806 -      case True
   1.807 -      with Init have "s3 = Norm s0"
   1.808 -	by simp
   1.809 -      with True show ?thesis 
   1.810 -	by simp
   1.811 -    next
   1.812 -      case False
   1.813 -      with Init
   1.814 -      obtain 
   1.815 -	hyp_init_super: 
   1.816 -        "PROP ?EqEval (Norm ((init_class_obj G C) s0)) s1
   1.817 -	               (In1r (if C = Object then Skip else Init (super c))) \<diamondsuit>"
   1.818 -	and 
   1.819 -        hyp_init_c:
   1.820 -	   "PROP ?EqEval ((set_lvars empty) s1) s2 (In1r (init c)) \<diamondsuit>" and
   1.821 -	s3: "s3 = (set_lvars (locals (store s1))) s2"
   1.822 -	by (simp only: if_False)
   1.823 -      from conf_s0 wf cls_C False
   1.824 -      have conf_s0': "(Norm ((init_class_obj G C) s0))\<Colon>\<preceq>(G, L)"
   1.825 -	by (auto dest: conforms_init_class_obj)
   1.826 -      moreover
   1.827 -      from wf cls_C 
   1.828 -      have wt_init_super:
   1.829 -           "\<lparr>prg = G, cls = accC, lcl = L\<rparr>
   1.830 -                  \<turnstile>(if C = Object then Skip else Init (super c))\<Colon>\<surd>"
   1.831 -	by (cases "C=Object")
   1.832 -           (auto dest: wf_prog_cdecl wf_cdecl_supD is_acc_classD)
   1.833 -      ultimately
   1.834 -      have eval_init_super: 
   1.835 -	   "G\<turnstile>Norm ((init_class_obj G C) s0) 
   1.836 -            \<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1"
   1.837 -	by (rule hyp_init_super)
   1.838 -      with conf_s0' wt_init_super wf
   1.839 -      have "s1\<Colon>\<preceq>(G, L)"
   1.840 -	by (blast dest: eval_type_sound)
   1.841 -      then
   1.842 -      have "(set_lvars empty) s1\<Colon>\<preceq>(G, empty)"
   1.843 -	by (cases s1) (auto dest: conforms_set_locals )
   1.844 -      with wf cls_C 
   1.845 -      have eval_init_c: "G\<turnstile>(set_lvars empty) s1 \<midarrow>init c\<rightarrow> s2"
   1.846 -	by (auto intro!: hyp_init_c dest: wf_prog_cdecl wf_cdecl_wt_init)
   1.847 -      from False eval_init_super eval_init_c s3
   1.848 -      show ?thesis
   1.849 -	by simp
   1.850 -    qed
   1.851 -    with cls show ?case
   1.852 -      by (rule eval.Init)
   1.853 -  qed 
   1.854 -qed
   1.855 +using evaln 
   1.856 +proof (induct)
   1.857 +  case (Loop b c e l n s0 s1 s2 s3)
   1.858 +  have "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1".
   1.859 +  moreover
   1.860 +  have "if the_Bool b
   1.861 +        then (G\<turnstile>s1 \<midarrow>c\<rightarrow> s2) \<and> 
   1.862 +             G\<turnstile>abupd (absorb (Cont l)) s2 \<midarrow>l\<bullet> While(e) c\<rightarrow> s3
   1.863 +        else s3 = s1"
   1.864 +    using Loop.hyps by simp
   1.865 +  ultimately show ?case by (rule eval.Loop)
   1.866 +next
   1.867 +  case (Try c1 c2 n s0 s1 s2 s3 C vn)
   1.868 +  have "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1".
   1.869 +  moreover
   1.870 +  have "G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2".
   1.871 +  moreover
   1.872 +  have "if G,s2\<turnstile>catch C then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<rightarrow> s3 else s3 = s2"
   1.873 +    using Try.hyps by simp
   1.874 +  ultimately show ?case by (rule eval.Try)
   1.875 +next
   1.876 +  case (Init C c n s0 s1 s2 s3)
   1.877 +  have "the (class G C) = c".
   1.878 +  moreover
   1.879 +  have "if inited C (globs s0) 
   1.880 +           then s3 = Norm s0
   1.881 +           else G\<turnstile>Norm ((init_class_obj G C) s0) 
   1.882 +                  \<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1 \<and>
   1.883 +                G\<turnstile>(set_lvars empty) s1 \<midarrow>init c\<rightarrow> s2 \<and>
   1.884 +                s3 = (set_lvars (locals (store s1))) s2"
   1.885 +    using Init.hyps by simp
   1.886 +  ultimately show ?case by (rule eval.Init)
   1.887 +qed (rule eval.intros,(assumption+ | assumption?))+
   1.888  
   1.889  lemma Suc_le_D_lemma: "\<lbrakk>Suc n <= m'; (\<And>m. n <= m \<Longrightarrow> P (Suc m)) \<rbrakk> \<Longrightarrow> P m'"
   1.890  apply (frule Suc_le_D)
   1.891 @@ -1068,8 +493,13 @@
   1.892  
   1.893  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> 
   1.894               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"
   1.895 -apply (fast intro: le_maxI1 le_maxI2)
   1.896 -done
   1.897 +by (fast intro: le_maxI1 le_maxI2)
   1.898 +
   1.899 +corollary evaln_max2E [consumes 2]:
   1.900 +  "\<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>n1\<rightarrow> ws1; G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>n2\<rightarrow> ws2; 
   1.901 +    \<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max n1 n2\<rightarrow> ws1;G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max n1 n2\<rightarrow> ws2 \<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
   1.902 +by (drule (1) evaln_max2) simp
   1.903 +
   1.904  
   1.905  lemma evaln_max3: 
   1.906  "\<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>
   1.907 @@ -1080,6 +510,16 @@
   1.908  apply (fast intro!: le_maxI1 le_maxI2)
   1.909  done
   1.910  
   1.911 +corollary evaln_max3E: 
   1.912 +"\<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;
   1.913 +   \<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> ws1;
   1.914 +    G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> ws2; 
   1.915 +    G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> ws3
   1.916 +   \<rbrakk> \<Longrightarrow> P
   1.917 +  \<rbrakk> \<Longrightarrow> P"
   1.918 +by (drule (2) evaln_max3) simp
   1.919 +
   1.920 +
   1.921  lemma le_max3I1: "(n2::nat) \<le> max n1 (max n2 n3)"
   1.922  proof -
   1.923    have "n2 \<le> max n2 n3"
   1.924 @@ -1102,755 +542,328 @@
   1.925    show ?thesis .
   1.926  qed
   1.927  
   1.928 +ML {*
   1.929 +Delsimprocs [wt_expr_proc,wt_var_proc,wt_exprs_proc,wt_stmt_proc]
   1.930 +*}
   1.931 +
   1.932  section {* eval implies evaln *}
   1.933  lemma eval_evaln: 
   1.934 -  assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" and
   1.935 -            wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T" and  
   1.936 -       conf_s0: "s0\<Colon>\<preceq>(G, L)" and
   1.937 -            wf: "wf_prog G"  
   1.938 +  assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"
   1.939    shows  "\<exists>n. G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)"
   1.940 -proof -
   1.941 -  from eval 
   1.942 -  show "\<And> L accC T. \<lbrakk>s0\<Colon>\<preceq>(G, L);\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>t\<Colon>T\<rbrakk>
   1.943 -                     \<Longrightarrow> \<exists> n. G\<turnstile>s0 \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (v,s1)"
   1.944 -       (is "PROP ?EqEval s0 s1 t v")
   1.945 -  proof (induct)
   1.946 -    case (Abrupt s t xc L accC T)
   1.947 -    obtain n where
   1.948 -      "G\<turnstile>(Some xc, s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (arbitrary3 t, Some xc, s)"
   1.949 -      by (rules intro: evaln.Abrupt)
   1.950 -    then show ?case ..
   1.951 -  next
   1.952 -    case Skip
   1.953 -    show ?case by (blast intro: evaln.Skip)
   1.954 -  next
   1.955 -    case (Expr e s0 s1 v L accC T)
   1.956 -    then obtain n where
   1.957 -      "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
   1.958 -      by (rules elim!: wt_elim_cases)
   1.959 -    then have "G\<turnstile>Norm s0 \<midarrow>Expr e\<midarrow>n\<rightarrow> s1"
   1.960 -      by (rule evaln.Expr) 
   1.961 -    then show ?case ..
   1.962 -  next
   1.963 -    case (Lab c l s0 s1 L accC T)
   1.964 -    then obtain n where
   1.965 -      "G\<turnstile>Norm s0 \<midarrow>c\<midarrow>n\<rightarrow> s1"
   1.966 -      by (rules elim!: wt_elim_cases)
   1.967 -    then have "G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<midarrow>n\<rightarrow> abupd (absorb l) s1"
   1.968 -      by (rule evaln.Lab)
   1.969 -    then show ?case ..
   1.970 -  next
   1.971 -    case (Comp c1 c2 s0 s1 s2 L accC T)
   1.972 -    with wf obtain n1 n2 where
   1.973 -      "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> s1"
   1.974 -      "G\<turnstile>s1 \<midarrow>c2\<midarrow>n2\<rightarrow> s2"
   1.975 -      by (blast elim!: wt_elim_cases dest: eval_type_sound)
   1.976 -    then have "G\<turnstile>Norm s0 \<midarrow>c1;; c2\<midarrow>max n1 n2\<rightarrow> s2"
   1.977 -      by (blast intro: evaln.Comp dest: evaln_max2 )
   1.978 -    then show ?case ..
   1.979 -  next
   1.980 -    case (If b c1 c2 e s0 s1 s2 L accC T)
   1.981 -    with wf obtain
   1.982 -      "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean"
   1.983 -      "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>(if the_Bool b then c1 else c2)\<Colon>\<surd>"
   1.984 -      by (cases "the_Bool b") (auto elim!: wt_elim_cases)
   1.985 -    with If wf obtain n1 n2 where
   1.986 -      "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n1\<rightarrow> s1"
   1.987 -      "G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<midarrow>n2\<rightarrow> s2"
   1.988 -      by (blast dest: eval_type_sound)
   1.989 -    then have "G\<turnstile>Norm s0 \<midarrow>If(e) c1 Else c2\<midarrow>max n1 n2\<rightarrow> s2"
   1.990 -      by (blast intro: evaln.If dest: evaln_max2)
   1.991 -    then show ?case ..
   1.992 -  next
   1.993 -    case (Loop b c e l s0 s1 s2 s3 L accC T)
   1.994 -    have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1" .
   1.995 -    have hyp_e: "PROP ?EqEval (Norm s0) s1 (In1l e) (In1 b)" .
   1.996 -    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
   1.997 -    have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (l\<bullet> While(e) c)\<Colon>T" .
   1.998 -    then obtain wt_e: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e\<Colon>-PrimT Boolean" and
   1.999 -                wt_c: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>c\<Colon>\<surd>"
  1.1000 -      by (rule wt_elim_cases) (blast)
  1.1001 -    from conf_s0 wt_e 
  1.1002 -    obtain n1 where
  1.1003 -      "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n1\<rightarrow> s1"
  1.1004 -      by (rules dest: hyp_e)
  1.1005 -    moreover
  1.1006 -    from eval_e wt_e conf_s0 wf
  1.1007 -    have conf_s1: "s1\<Colon>\<preceq>(G, L)"
  1.1008 -      by (rules dest: eval_type_sound)
  1.1009 -    obtain n2 where
  1.1010 -      "if normal s1 \<and> the_Bool b 
  1.1011 -             then (G\<turnstile>s1 \<midarrow>c\<midarrow>n2\<rightarrow> s2 \<and> 
  1.1012 -                   G\<turnstile>(abupd (absorb (Cont l)) s2)\<midarrow>l\<bullet> While(e) c\<midarrow>n2\<rightarrow> s3)
  1.1013 -	     else s3 = s1"
  1.1014 -    proof (cases "normal s1 \<and> the_Bool b")
  1.1015 -      case True
  1.1016 -      from Loop True have hyp_c: "PROP ?EqEval s1 s2 (In1r c) \<diamondsuit>"
  1.1017 -	by (auto)
  1.1018 -      from Loop True have hyp_w: "PROP ?EqEval (abupd (absorb (Cont l)) s2)
  1.1019 -                                        s3 (In1r (l\<bullet> While(e) c)) \<diamondsuit>"
  1.1020 -	by (auto)
  1.1021 -      from Loop True have eval_c: "G\<turnstile>s1 \<midarrow>c\<rightarrow> s2"
  1.1022 -	by simp
  1.1023 -      from conf_s1 wt_c
  1.1024 -      obtain m1 where 
  1.1025 -	evaln_c: "G\<turnstile>s1 \<midarrow>c\<midarrow>m1\<rightarrow> s2"
  1.1026 -	by (rules dest: hyp_c)
  1.1027 -      moreover
  1.1028 -      from eval_c conf_s1 wt_c wf
  1.1029 -      have "s2\<Colon>\<preceq>(G, L)"
  1.1030 -	by (rules dest: eval_type_sound)
  1.1031 -      then
  1.1032 -      have "abupd (absorb (Cont l)) s2 \<Colon>\<preceq>(G, L)"
  1.1033 -	by (cases s2) (auto intro: conforms_absorb)
  1.1034 -      from this and wt
  1.1035 -      obtain m2 where 
  1.1036 -	"G\<turnstile>abupd (absorb (Cont l)) s2 \<midarrow>l\<bullet> While(e) c\<midarrow>m2\<rightarrow> s3"
  1.1037 -	by (blast dest: hyp_w)
  1.1038 -      moreover note True and that
  1.1039 -      ultimately show ?thesis
  1.1040 -	by simp (rules intro: evaln_nonstrict le_maxI1 le_maxI2)
  1.1041 -    next
  1.1042 -      case False
  1.1043 -      with Loop have "s3 = s1"
  1.1044 -	by simp
  1.1045 -      with False that
  1.1046 -      show ?thesis
  1.1047 -	by auto 
  1.1048 -    qed
  1.1049 -    ultimately
  1.1050 -    have "G\<turnstile>Norm s0 \<midarrow>l\<bullet> While(e) c\<midarrow>max n1 n2\<rightarrow> s3"
  1.1051 -      apply -
  1.1052 -      apply (rule evaln.Loop)
  1.1053 -      apply   (rules intro: evaln_nonstrict intro: le_maxI1)
  1.1054 +using eval 
  1.1055 +proof (induct)
  1.1056 +  case (Abrupt s t xc)
  1.1057 +  obtain n where
  1.1058 +    "G\<turnstile>(Some xc, s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (arbitrary3 t, Some xc, s)"
  1.1059 +    by (rules intro: evaln.Abrupt)
  1.1060 +  then show ?case ..
  1.1061 +next
  1.1062 +  case Skip
  1.1063 +  show ?case by (blast intro: evaln.Skip)
  1.1064 +next
  1.1065 +  case (Expr e s0 s1 v)
  1.1066 +  then obtain n where
  1.1067 +    "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
  1.1068 +    by (rules)
  1.1069 +  then have "G\<turnstile>Norm s0 \<midarrow>Expr e\<midarrow>n\<rightarrow> s1"
  1.1070 +    by (rule evaln.Expr) 
  1.1071 +  then show ?case ..
  1.1072 +next
  1.1073 +  case (Lab c l s0 s1)
  1.1074 +  then obtain n where
  1.1075 +    "G\<turnstile>Norm s0 \<midarrow>c\<midarrow>n\<rightarrow> s1"
  1.1076 +    by (rules)
  1.1077 +  then have "G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<midarrow>n\<rightarrow> abupd (absorb l) s1"
  1.1078 +    by (rule evaln.Lab)
  1.1079 +  then show ?case ..
  1.1080 +next
  1.1081 +  case (Comp c1 c2 s0 s1 s2)
  1.1082 +  then obtain n1 n2 where
  1.1083 +    "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> s1"
  1.1084 +    "G\<turnstile>s1 \<midarrow>c2\<midarrow>n2\<rightarrow> s2"
  1.1085 +    by (rules)
  1.1086 +  then have "G\<turnstile>Norm s0 \<midarrow>c1;; c2\<midarrow>max n1 n2\<rightarrow> s2"
  1.1087 +    by (blast intro: evaln.Comp dest: evaln_max2 )
  1.1088 +  then show ?case ..
  1.1089 +next
  1.1090 +  case (If b c1 c2 e s0 s1 s2)
  1.1091 +  then obtain n1 n2 where
  1.1092 +    "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n1\<rightarrow> s1"
  1.1093 +    "G\<turnstile>s1 \<midarrow>(if the_Bool b then c1 else c2)\<midarrow>n2\<rightarrow> s2"
  1.1094 +    by (rules)
  1.1095 +  then have "G\<turnstile>Norm s0 \<midarrow>If(e) c1 Else c2\<midarrow>max n1 n2\<rightarrow> s2"
  1.1096 +    by (blast intro: evaln.If dest: evaln_max2)
  1.1097 +  then show ?case ..
  1.1098 +next
  1.1099 +  case (Loop b c e l s0 s1 s2 s3)
  1.1100 +  from Loop.hyps obtain n1 where
  1.1101 +    "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n1\<rightarrow> s1"
  1.1102 +    by (rules)
  1.1103 +  moreover from Loop.hyps obtain n2 where
  1.1104 +    "if the_Bool b 
  1.1105 +        then (G\<turnstile>s1 \<midarrow>c\<midarrow>n2\<rightarrow> s2 \<and> 
  1.1106 +              G\<turnstile>(abupd (absorb (Cont l)) s2)\<midarrow>l\<bullet> While(e) c\<midarrow>n2\<rightarrow> s3)
  1.1107 +	else s3 = s1"
  1.1108 +    by simp (rules intro: evaln_nonstrict le_maxI1 le_maxI2)
  1.1109 +  ultimately
  1.1110 +  have "G\<turnstile>Norm s0 \<midarrow>l\<bullet> While(e) c\<midarrow>max n1 n2\<rightarrow> s3"
  1.1111 +    apply -
  1.1112 +    apply (rule evaln.Loop)
  1.1113 +    apply   (rules intro: evaln_nonstrict intro: le_maxI1)
  1.1114  
  1.1115 -      apply   (auto intro: evaln_nonstrict intro: le_maxI2)
  1.1116 -      done
  1.1117 -    then show ?case ..
  1.1118 -  next
  1.1119 -    case (Do j s L accC T)
  1.1120 -    have "G\<turnstile>Norm s \<midarrow>Do j\<midarrow>n\<rightarrow> (Some (Jump j), s)"
  1.1121 -      by (rule evaln.Do)
  1.1122 -    then show ?case ..
  1.1123 -  next
  1.1124 -    case (Throw a e s0 s1 L accC T)
  1.1125 -    then obtain n where
  1.1126 -      "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<midarrow>n\<rightarrow> s1"
  1.1127 -      by (rules elim!: wt_elim_cases)
  1.1128 -    then have "G\<turnstile>Norm s0 \<midarrow>Throw e\<midarrow>n\<rightarrow> abupd (throw a) s1"
  1.1129 -      by (rule evaln.Throw)
  1.1130 -    then show ?case ..
  1.1131 -  next 
  1.1132 -    case (Try catchC c1 c2 s0 s1 s2 s3 vn L accC T)
  1.1133 -    have  hyp_c1: "PROP ?EqEval (Norm s0) s1 (In1r c1) \<diamondsuit>" .
  1.1134 -    have eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1" .
  1.1135 -    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1.1136 -    have      wt: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>In1r (Try c1 Catch(catchC vn) c2)\<Colon>T" .
  1.1137 -    then obtain 
  1.1138 -      wt_c1: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<turnstile>c1\<Colon>\<surd>" and
  1.1139 -      wt_c2: "\<lparr>prg=G,cls=accC,lcl=L\<rparr>\<lparr>lcl := L(VName vn\<mapsto>Class catchC)\<rparr>\<turnstile>c2\<Colon>\<surd>"
  1.1140 -      by (rule wt_elim_cases) (auto)
  1.1141 -    from conf_s0 wt_c1
  1.1142 -    obtain n1 where
  1.1143 -      "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> s1"
  1.1144 -      by (blast dest: hyp_c1)
  1.1145 -    moreover 
  1.1146 -    have sxalloc: "G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2" .
  1.1147 -    moreover
  1.1148 -    from eval_c1 wt_c1 conf_s0 wf
  1.1149 -    have "s1\<Colon>\<preceq>(G, L)"
  1.1150 -      by (blast dest: eval_type_sound)
  1.1151 -    with sxalloc wf
  1.1152 -    have conf_s2: "s2\<Colon>\<preceq>(G, L)" 
  1.1153 -      by (auto dest: sxalloc_type_sound split: option.splits)
  1.1154 -    obtain n2 where
  1.1155 -      "if G,s2\<turnstile>catch catchC then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<midarrow>n2\<rightarrow> s3 else s3 = s2"
  1.1156 -    proof (cases "G,s2\<turnstile>catch catchC")
  1.1157 -      case True
  1.1158 -      note Catch = this
  1.1159 -      with Try have hyp_c2: "PROP ?EqEval (new_xcpt_var vn s2) s3 (In1r c2) \<diamondsuit>"
  1.1160 -	by auto
  1.1161 -      show ?thesis
  1.1162 -      proof (cases "normal s1")
  1.1163 -	case True
  1.1164 -	with sxalloc wf 
  1.1165 -	have eq_s2_s1: "s2=s1"
  1.1166 -	  by (auto dest: sxalloc_type_sound split: option.splits)
  1.1167 -	with True 
  1.1168 -	have "\<not>  G,s2\<turnstile>catch catchC"
  1.1169 -	  by (simp add: catch_def)
  1.1170 -	with Catch show ?thesis 
  1.1171 -	  by (contradiction)
  1.1172 -      next 
  1.1173 -	case False
  1.1174 -	with sxalloc wf
  1.1175 -	obtain a 
  1.1176 -	  where xcpt_s2: "abrupt s2 = Some (Xcpt (Loc a))"
  1.1177 -	  by (auto dest!: sxalloc_type_sound split: option.splits)
  1.1178 -	with Catch
  1.1179 -	have "G\<turnstile>obj_ty (the (globs (store s2) (Heap a)))\<preceq>Class catchC"
  1.1180 -	  by (cases s2) simp
  1.1181 -	with xcpt_s2 conf_s2 wf 
  1.1182 -	have "new_xcpt_var vn s2\<Colon>\<preceq>(G, L(VName vn\<mapsto>Class catchC))"
  1.1183 -	  by (auto dest: Try_lemma)
  1.1184 -	(* FIXME extract lemma for this conformance, also useful for
  1.1185 -               eval_type_sound and evaln_eval *)
  1.1186 -	from this wt_c2
  1.1187 -	obtain m where "G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<midarrow>m\<rightarrow> s3"
  1.1188 -	  by (auto dest: hyp_c2)
  1.1189 -	with True that
  1.1190 -	show ?thesis
  1.1191 -	  by simp
  1.1192 -      qed
  1.1193 -    next
  1.1194 -      case False
  1.1195 -      with Try
  1.1196 -      have "s3=s2"
  1.1197 -	by simp
  1.1198 -      with False and that
  1.1199 -      show ?thesis
  1.1200 -	by simp
  1.1201 -    qed
  1.1202 -    ultimately
  1.1203 -    have "G\<turnstile>Norm s0 \<midarrow>Try c1 Catch(catchC vn) c2\<midarrow>max n1 n2\<rightarrow> s3"
  1.1204 -      by (auto intro!: evaln.Try le_maxI1 le_maxI2)
  1.1205 -    then show ?case ..
  1.1206 -  next
  1.1207 -    case (Fin c1 c2 s0 s1 s2 s3 x1 L accC T)
  1.1208 -    have s3: "s3 = (if \<exists>err. x1 = Some (Error err) 
  1.1209 -                       then (x1, s1)
  1.1210 -                       else abupd (abrupt_if (x1 \<noteq> None) x1) s2)" .
  1.1211 -    from Fin wf obtain n1 n2 where 
  1.1212 -      "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> (x1, s1)"
  1.1213 -      "G\<turnstile>Norm s1 \<midarrow>c2\<midarrow>n2\<rightarrow> s2" and
  1.1214 -      error_free_s1: "error_free (x1,s1)"
  1.1215 -      by (blast elim!: wt_elim_cases 
  1.1216 -	         dest: eval_type_sound intro: conforms_NormI)
  1.1217 -    then have 
  1.1218 -     "G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<midarrow>max n1 n2\<rightarrow> abupd (abrupt_if (x1 \<noteq> None) x1) s2"
  1.1219 -      by (blast intro: evaln.Fin dest: evaln_max2)
  1.1220 -    with error_free_s1 s3
  1.1221 -    show "\<exists>n. G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<midarrow>n\<rightarrow> s3"
  1.1222 -      by (auto simp add: error_free_def)
  1.1223 -  next
  1.1224 -    case (Init C c s0 s1 s2 s3 L accC T)
  1.1225 -    have     cls: "the (class G C) = c" .
  1.1226 -    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1.1227 -    have      wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1r (Init C)\<Colon>T" .
  1.1228 -    with cls
  1.1229 -    have cls_C: "class G C = Some c"
  1.1230 -      by - (erule wt_elim_cases,auto)
  1.1231 -    obtain n where
  1.1232 +    apply   (auto intro: evaln_nonstrict intro: le_maxI2)
  1.1233 +    done
  1.1234 +  then show ?case ..
  1.1235 +next
  1.1236 +  case (Jmp j s)
  1.1237 +  have "G\<turnstile>Norm s \<midarrow>Jmp j\<midarrow>n\<rightarrow> (Some (Jump j), s)"
  1.1238 +    by (rule evaln.Jmp)
  1.1239 +  then show ?case ..
  1.1240 +next
  1.1241 +  case (Throw a e s0 s1)
  1.1242 +  then obtain n where
  1.1243 +    "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a\<midarrow>n\<rightarrow> s1"
  1.1244 +    by (rules)
  1.1245 +  then have "G\<turnstile>Norm s0 \<midarrow>Throw e\<midarrow>n\<rightarrow> abupd (throw a) s1"
  1.1246 +    by (rule evaln.Throw)
  1.1247 +  then show ?case ..
  1.1248 +next 
  1.1249 +  case (Try catchC c1 c2 s0 s1 s2 s3 vn)
  1.1250 +  from Try.hyps obtain n1 where
  1.1251 +    "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> s1"
  1.1252 +    by (rules)
  1.1253 +  moreover 
  1.1254 +  have sxalloc: "G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2" .
  1.1255 +  moreover
  1.1256 +  from Try.hyps obtain n2 where
  1.1257 +    "if G,s2\<turnstile>catch catchC then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<midarrow>n2\<rightarrow> s3 else s3 = s2"
  1.1258 +    by fastsimp 
  1.1259 +  ultimately
  1.1260 +  have "G\<turnstile>Norm s0 \<midarrow>Try c1 Catch(catchC vn) c2\<midarrow>max n1 n2\<rightarrow> s3"
  1.1261 +    by (auto intro!: evaln.Try le_maxI1 le_maxI2)
  1.1262 +  then show ?case ..
  1.1263 +next
  1.1264 +  case (Fin c1 c2 s0 s1 s2 s3 x1)
  1.1265 +  from Fin obtain n1 n2 where 
  1.1266 +    "G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n1\<rightarrow> (x1, s1)"
  1.1267 +    "G\<turnstile>Norm s1 \<midarrow>c2\<midarrow>n2\<rightarrow> s2"
  1.1268 +    by rules
  1.1269 +  moreover
  1.1270 +  have s3: "s3 = (if \<exists>err. x1 = Some (Error err) 
  1.1271 +                     then (x1, s1)
  1.1272 +                     else abupd (abrupt_if (x1 \<noteq> None) x1) s2)" .
  1.1273 +  ultimately 
  1.1274 +  have 
  1.1275 +    "G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<midarrow>max n1 n2\<rightarrow> s3"
  1.1276 +    by (blast intro: evaln.Fin dest: evaln_max2)
  1.1277 +  then show ?case ..
  1.1278 +next
  1.1279 +  case (Init C c s0 s1 s2 s3)
  1.1280 +  have     cls: "the (class G C) = c" .
  1.1281 +  moreover from Init.hyps obtain n where
  1.1282        "if inited C (globs s0) then s3 = Norm s0
  1.1283         else (G\<turnstile>Norm (init_class_obj G C s0)
  1.1284  	      \<midarrow>(if C = Object then Skip else Init (super c))\<midarrow>n\<rightarrow> s1 \<and>
  1.1285  	           G\<turnstile>set_lvars empty s1 \<midarrow>init c\<midarrow>n\<rightarrow> s2 \<and> 
  1.1286                     s3 = restore_lvars s1 s2)"
  1.1287 -    proof (cases "inited C (globs s0)")
  1.1288 -      case True
  1.1289 -      with Init have "s3 = Norm s0"
  1.1290 -	by simp
  1.1291 -      with True that show ?thesis 
  1.1292 -	by simp
  1.1293 -    next
  1.1294 -      case False
  1.1295 -      with Init
  1.1296 -      obtain 
  1.1297 -	hyp_init_super: 
  1.1298 -        "PROP ?EqEval (Norm ((init_class_obj G C) s0)) s1
  1.1299 -	               (In1r (if C = Object then Skip else Init (super c))) \<diamondsuit>"
  1.1300 -	and 
  1.1301 -        hyp_init_c:
  1.1302 -	   "PROP ?EqEval ((set_lvars empty) s1) s2 (In1r (init c)) \<diamondsuit>" and
  1.1303 -	s3: "s3 = (set_lvars (locals (store s1))) s2" and
  1.1304 -	eval_init_super: 
  1.1305 -	"G\<turnstile>Norm ((init_class_obj G C) s0) 
  1.1306 -           \<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1"
  1.1307 -	by (simp only: if_False)
  1.1308 -      from conf_s0 wf cls_C False
  1.1309 -      have conf_s0': "(Norm ((init_class_obj G C) s0))\<Colon>\<preceq>(G, L)"
  1.1310 -	by (auto dest: conforms_init_class_obj)
  1.1311 -      moreover
  1.1312 -      from wf cls_C 
  1.1313 -      have wt_init_super:
  1.1314 -           "\<lparr>prg = G, cls = accC, lcl = L\<rparr>
  1.1315 -                  \<turnstile>(if C = Object then Skip else Init (super c))\<Colon>\<surd>"
  1.1316 -	by (cases "C=Object")
  1.1317 -           (auto dest: wf_prog_cdecl wf_cdecl_supD is_acc_classD)
  1.1318 -      ultimately
  1.1319 -      obtain m1 where  
  1.1320 -	   "G\<turnstile>Norm ((init_class_obj G C) s0) 
  1.1321 -            \<midarrow>(if C = Object then Skip else Init (super c))\<midarrow>m1\<rightarrow> s1"
  1.1322 -	by (rules dest: hyp_init_super)
  1.1323 -      moreover
  1.1324 -      from eval_init_super conf_s0' wt_init_super wf
  1.1325 -      have "s1\<Colon>\<preceq>(G, L)"
  1.1326 -	by (rules dest: eval_type_sound)
  1.1327 -      then
  1.1328 -      have "(set_lvars empty) s1\<Colon>\<preceq>(G, empty)"
  1.1329 -	by (cases s1) (auto dest: conforms_set_locals )
  1.1330 -      with wf cls_C 
  1.1331 -      obtain m2 where
  1.1332 -	"G\<turnstile>(set_lvars empty) s1 \<midarrow>init c\<midarrow>m2\<rightarrow> s2"
  1.1333 -	by (blast dest!: hyp_init_c 
  1.1334 -                   dest: wf_prog_cdecl intro!: wf_cdecl_wt_init)
  1.1335 -      moreover note s3 and False and that
  1.1336 -      ultimately show ?thesis
  1.1337 -	by simp (rules intro: evaln_nonstrict le_maxI1 le_maxI2)
  1.1338 -    qed
  1.1339 -    from cls this have "G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s3"
  1.1340 -      by (rule evaln.Init)
  1.1341 -    then show ?case ..
  1.1342 -  next
  1.1343 -    case (NewC C a s0 s1 s2 L accC T)
  1.1344 -    with wf obtain n where 
  1.1345 -     "G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s1"
  1.1346 -      by (blast elim!: wt_elim_cases dest: is_acc_classD)
  1.1347 -    with NewC 
  1.1348 -    have "G\<turnstile>Norm s0 \<midarrow>NewC C-\<succ>Addr a\<midarrow>n\<rightarrow> s2"
  1.1349 -      by (rules intro: evaln.NewC)
  1.1350 -    then show ?case ..
  1.1351 -  next
  1.1352 -    case (NewA T a e i s0 s1 s2 s3 L accC Ta)
  1.1353 -    hence "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>init_comp_ty T\<Colon>\<surd>" 
  1.1354 -      by (auto elim!: wt_elim_cases 
  1.1355 -              intro!: wt_init_comp_ty dest: is_acc_typeD)
  1.1356 -    with NewA wf obtain n1 n2 where 
  1.1357 -      "G\<turnstile>Norm s0 \<midarrow>init_comp_ty T\<midarrow>n1\<rightarrow> s1"
  1.1358 -      "G\<turnstile>s1 \<midarrow>e-\<succ>i\<midarrow>n2\<rightarrow> s2"      
  1.1359 -      by (blast elim!: wt_elim_cases dest: eval_type_sound)
  1.1360 -    moreover
  1.1361 -    have "G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3" .
  1.1362 -    ultimately
  1.1363 -    have "G\<turnstile>Norm s0 \<midarrow>New T[e]-\<succ>Addr a\<midarrow>max n1 n2\<rightarrow> s3"
  1.1364 -      by (blast intro: evaln.NewA dest: evaln_max2)
  1.1365 -    then show ?case ..
  1.1366 -  next
  1.1367 -    case (Cast castT e s0 s1 s2 v L accC T)
  1.1368 -    with wf obtain n where
  1.1369 -      "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
  1.1370 -      by (rules elim!: wt_elim_cases)
  1.1371 -    moreover 
  1.1372 -    have "s2 = abupd (raise_if (\<not> G,snd s1\<turnstile>v fits castT) ClassCast) s1" .
  1.1373 -    ultimately
  1.1374 -    have "G\<turnstile>Norm s0 \<midarrow>Cast castT e-\<succ>v\<midarrow>n\<rightarrow> s2"
  1.1375 -      by (rule evaln.Cast)
  1.1376 -    then show ?case ..
  1.1377 -  next
  1.1378 -    case (Inst T b e s0 s1 v L accC T')
  1.1379 -    with wf obtain n where
  1.1380 -      "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
  1.1381 -      by (rules elim!: wt_elim_cases)
  1.1382 -    moreover 
  1.1383 -    have "b = (v \<noteq> Null \<and> G,snd s1\<turnstile>v fits RefT T)" .
  1.1384 -    ultimately
  1.1385 -    have "G\<turnstile>Norm s0 \<midarrow>e InstOf T-\<succ>Bool b\<midarrow>n\<rightarrow> s1"
  1.1386 -      by (rule evaln.Inst)
  1.1387 -    then show ?case ..
  1.1388 -  next
  1.1389 -    case (Lit s v L accC T)
  1.1390 -    have "G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<midarrow>n\<rightarrow> Norm s"
  1.1391 -      by (rule evaln.Lit)
  1.1392 -    then show ?case ..
  1.1393 -  next
  1.1394 -    case (UnOp e s0 s1 unop v L accC T)
  1.1395 -    with wf obtain n where
  1.1396 -      "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
  1.1397 -      by (rules elim!: wt_elim_cases)
  1.1398 -    hence "G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>eval_unop unop v\<midarrow>n\<rightarrow> s1"
  1.1399 -      by (rule evaln.UnOp)
  1.1400 -    then show ?case ..
  1.1401 -  next
  1.1402 -    case (BinOp binop e1 e2 s0 s1 s2 v1 v2 L accC T)
  1.1403 -    with wf obtain n1 n2 where 
  1.1404 -      "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<midarrow>n1\<rightarrow> s1"
  1.1405 -      "G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then In1l e2
  1.1406 +    by (auto intro: evaln_nonstrict le_maxI1 le_maxI2)
  1.1407 +  ultimately have "G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s3"
  1.1408 +    by (rule evaln.Init)
  1.1409 +  then show ?case ..
  1.1410 +next
  1.1411 +  case (NewC C a s0 s1 s2)
  1.1412 +  then obtain n where 
  1.1413 +    "G\<turnstile>Norm s0 \<midarrow>Init C\<midarrow>n\<rightarrow> s1"
  1.1414 +    by (rules)
  1.1415 +  with NewC 
  1.1416 +  have "G\<turnstile>Norm s0 \<midarrow>NewC C-\<succ>Addr a\<midarrow>n\<rightarrow> s2"
  1.1417 +    by (rules intro: evaln.NewC)
  1.1418 +  then show ?case ..
  1.1419 +next
  1.1420 +  case (NewA T a e i s0 s1 s2 s3)
  1.1421 +  then obtain n1 n2 where 
  1.1422 +    "G\<turnstile>Norm s0 \<midarrow>init_comp_ty T\<midarrow>n1\<rightarrow> s1"
  1.1423 +    "G\<turnstile>s1 \<midarrow>e-\<succ>i\<midarrow>n2\<rightarrow> s2"      
  1.1424 +    by (rules)
  1.1425 +  moreover
  1.1426 +  have "G\<turnstile>abupd (check_neg i) s2 \<midarrow>halloc Arr T (the_Intg i)\<succ>a\<rightarrow> s3" .
  1.1427 +  ultimately
  1.1428 +  have "G\<turnstile>Norm s0 \<midarrow>New T[e]-\<succ>Addr a\<midarrow>max n1 n2\<rightarrow> s3"
  1.1429 +    by (blast intro: evaln.NewA dest: evaln_max2)
  1.1430 +  then show ?case ..
  1.1431 +next
  1.1432 +  case (Cast castT e s0 s1 s2 v)
  1.1433 +  then obtain n where
  1.1434 +    "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
  1.1435 +    by (rules)
  1.1436 +  moreover 
  1.1437 +  have "s2 = abupd (raise_if (\<not> G,snd s1\<turnstile>v fits castT) ClassCast) s1" .
  1.1438 +  ultimately
  1.1439 +  have "G\<turnstile>Norm s0 \<midarrow>Cast castT e-\<succ>v\<midarrow>n\<rightarrow> s2"
  1.1440 +    by (rule evaln.Cast)
  1.1441 +  then show ?case ..
  1.1442 +next
  1.1443 +  case (Inst T b e s0 s1 v)
  1.1444 +  then obtain n where
  1.1445 +    "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
  1.1446 +    by (rules)
  1.1447 +  moreover 
  1.1448 +  have "b = (v \<noteq> Null \<and> G,snd s1\<turnstile>v fits RefT T)" .
  1.1449 +  ultimately
  1.1450 +  have "G\<turnstile>Norm s0 \<midarrow>e InstOf T-\<succ>Bool b\<midarrow>n\<rightarrow> s1"
  1.1451 +    by (rule evaln.Inst)
  1.1452 +  then show ?case ..
  1.1453 +next
  1.1454 +  case (Lit s v)
  1.1455 +  have "G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<midarrow>n\<rightarrow> Norm s"
  1.1456 +    by (rule evaln.Lit)
  1.1457 +  then show ?case ..
  1.1458 +next
  1.1459 +  case (UnOp e s0 s1 unop v )
  1.1460 +  then obtain n where
  1.1461 +    "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1"
  1.1462 +    by (rules)
  1.1463 +  hence "G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>eval_unop unop v\<midarrow>n\<rightarrow> s1"
  1.1464 +    by (rule evaln.UnOp)
  1.1465 +  then show ?case ..
  1.1466 +next
  1.1467 +  case (BinOp binop e1 e2 s0 s1 s2 v1 v2)
  1.1468 +  then obtain n1 n2 where 
  1.1469 +    "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<midarrow>n1\<rightarrow> s1"
  1.1470 +    "G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then In1l e2
  1.1471                 else In1r Skip)\<succ>\<midarrow>n2\<rightarrow> (In1 v2, s2)"    
  1.1472 -      by (blast elim!: wt_elim_BinOp dest: eval_type_sound)
  1.1473 -    hence "G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<midarrow>max n1 n2
  1.1474 -           \<rightarrow> s2"
  1.1475 -      by (blast intro!: evaln.BinOp dest: evaln_max2)
  1.1476 -    then show ?case ..
  1.1477 -  next
  1.1478 -    case (Super s L accC T)
  1.1479 -    have "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<midarrow>n\<rightarrow> Norm s"
  1.1480 -      by (rule evaln.Super)
  1.1481 -    then show ?case ..
  1.1482 -  next
  1.1483 -    case (Acc f s0 s1 v va L accC T)
  1.1484 -    with wf obtain n where
  1.1485 -      "G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v, f)\<midarrow>n\<rightarrow> s1"
  1.1486 -      by (rules elim!: wt_elim_cases)
  1.1487 -    then
  1.1488 -    have "G\<turnstile>Norm s0 \<midarrow>Acc va-\<succ>v\<midarrow>n\<rightarrow> s1"
  1.1489 -      by (rule evaln.Acc)
  1.1490 -    then show ?case ..
  1.1491 -  next
  1.1492 -    case (Ass e f s0 s1 s2 v var w L accC T)
  1.1493 -    with wf obtain n1 n2 where 
  1.1494 -      "G\<turnstile>Norm s0 \<midarrow>var=\<succ>(w, f)\<midarrow>n1\<rightarrow> s1"
  1.1495 -      "G\<turnstile>s1 \<midarrow>e-\<succ>v\<midarrow>n2\<rightarrow> s2"      
  1.1496 -      by (blast elim!: wt_elim_cases dest: eval_type_sound)
  1.1497 -    then
  1.1498 -    have "G\<turnstile>Norm s0 \<midarrow>var:=e-\<succ>v\<midarrow>max n1 n2\<rightarrow> assign f v s2"
  1.1499 -      by (blast intro: evaln.Ass dest: evaln_max2)
  1.1500 -    then show ?case ..
  1.1501 -  next
  1.1502 -    case (Cond b e0 e1 e2 s0 s1 s2 v L accC T)
  1.1503 -    have hyp_e0: "PROP ?EqEval (Norm s0) s1 (In1l e0) (In1 b)" .
  1.1504 -    have hyp_if: "PROP ?EqEval s1 s2 
  1.1505 -                              (In1l (if the_Bool b then e1 else e2)) (In1 v)" .
  1.1506 -    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1.1507 -    have wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l (e0 ? e1 : e2)\<Colon>T" .
  1.1508 -    then obtain T1 T2 statT where
  1.1509 -       wt_e0: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e0\<Colon>-PrimT Boolean" and
  1.1510 -       wt_e1: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e1\<Colon>-T1" and
  1.1511 -       wt_e2: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>e2\<Colon>-T2" and 
  1.1512 -       statT: "G\<turnstile>T1\<preceq>T2 \<and> statT = T2  \<or>  G\<turnstile>T2\<preceq>T1 \<and> statT =  T1" and
  1.1513 -       T    : "T=Inl statT"
  1.1514 -      by (rule wt_elim_cases) auto
  1.1515 -    have eval_e0: "G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1" .
  1.1516 -    from conf_s0 wt_e0
  1.1517 -    obtain n1 where 
  1.1518 -      "G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<midarrow>n1\<rightarrow> s1"
  1.1519 -      by (rules dest: hyp_e0)
  1.1520 -    moreover
  1.1521 -    from eval_e0 conf_s0 wf wt_e0
  1.1522 -    have "s1\<Colon>\<preceq>(G, L)"
  1.1523 -      by (blast dest: eval_type_sound)
  1.1524 -    with wt_e1 wt_e2 statT hyp_if obtain n2 where
  1.1525 -      "G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<midarrow>n2\<rightarrow> s2"
  1.1526 -      by  (cases "the_Bool b") force+
  1.1527 -    ultimately
  1.1528 -    have "G\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<midarrow>max n1 n2\<rightarrow> s2"
  1.1529 -      by (blast intro: evaln.Cond dest: evaln_max2)
  1.1530 -    then show ?case ..
  1.1531 -  next
  1.1532 -    case (Call invDeclC a' accC' args e mn mode pTs' s0 s1 s2 s3 s3' s4 statT 
  1.1533 -      v vs L accC T)
  1.1534 -    (* Repeats large parts of the type soundness proof. One should factor
  1.1535 -       out some lemmata about the relations and conformance of s2, s3 and s3'*)
  1.1536 -    have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1" .
  1.1537 -    have eval_args: "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<rightarrow> s2" .
  1.1538 -    have invDeclC: "invDeclC 
  1.1539 -                      = invocation_declclass G mode (store s2) a' statT 
  1.1540 -                           \<lparr>name = mn, parTs = pTs'\<rparr>" .
  1.1541 -    have
  1.1542 -      init_lvars: "s3 = 
  1.1543 -             init_lvars G invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> mode a' vs s2" .
  1.1544 -    have
  1.1545 -      check: "s3' =
  1.1546 -       check_method_access G accC' statT mode \<lparr>name = mn, parTs = pTs'\<rparr> a' s3" .
  1.1547 -    have eval_methd: 
  1.1548 -           "G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>-\<succ>v\<rightarrow> s4" .
  1.1549 -    have     hyp_e: "PROP ?EqEval (Norm s0) s1 (In1l e) (In1 a')" .
  1.1550 -    have  hyp_args: "PROP ?EqEval s1 s2 (In3 args) (In3 vs)" .
  1.1551 -    have hyp_methd: "PROP ?EqEval s3' s4 
  1.1552 -             (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)) (In1 v)".
  1.1553 -    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1.1554 -    have      wt: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>
  1.1555 -                    \<turnstile>In1l ({accC',statT,mode}e\<cdot>mn( {pTs'}args))\<Colon>T" .
  1.1556 -    from wt obtain pTs statDeclT statM where
  1.1557 -                 wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-RefT statT" and
  1.1558 -              wt_args: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>args\<Colon>\<doteq>pTs" and
  1.1559 -                statM: "max_spec G accC statT \<lparr>name=mn,parTs=pTs\<rparr> 
  1.1560 -                         = {((statDeclT,statM),pTs')}" and
  1.1561 -                 mode: "mode = invmode statM e" and
  1.1562 -                    T: "T =Inl (resTy statM)" and
  1.1563 -        eq_accC_accC': "accC=accC'"
  1.1564 -      by (rule wt_elim_cases) fastsimp+
  1.1565 -    from conf_s0 wt_e
  1.1566 -    obtain n1 where
  1.1567 -      evaln_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n1\<rightarrow> s1"
  1.1568 -      by (rules dest: hyp_e)
  1.1569 -    from wf eval_e conf_s0 wt_e
  1.1570 -    obtain conf_s1: "s1\<Colon>\<preceq>(G, L)" and
  1.1571 -           conf_a': "normal s1 \<Longrightarrow> G, store s1\<turnstile>a'\<Colon>\<preceq>RefT statT"  
  1.1572 -      by (auto dest!: eval_type_sound)
  1.1573 -    from conf_s1 wt_args
  1.1574 -    obtain n2 where
  1.1575 -      evaln_args: "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<midarrow>n2\<rightarrow> s2"
  1.1576 -      by (blast dest: hyp_args)
  1.1577 -    from wt_args conf_s1 eval_args wf 
  1.1578 -    obtain    conf_s2: "s2\<Colon>\<preceq>(G, L)" and
  1.1579 -            conf_args: "normal s2 
  1.1580 -                         \<Longrightarrow>  list_all2 (conf G (store s2)) vs pTs"  
  1.1581 -      by (auto dest!: eval_type_sound)
  1.1582 -    from statM 
  1.1583 -    obtain
  1.1584 -       statM': "(statDeclT,statM)\<in>mheads G accC statT \<lparr>name=mn,parTs=pTs'\<rparr>" and
  1.1585 -       pTs_widen: "G\<turnstile>pTs[\<preceq>]pTs'"
  1.1586 -      by (blast dest: max_spec2mheads)
  1.1587 -    from check
  1.1588 -    have eq_store_s3'_s3: "store s3'=store s3"
  1.1589 -      by (cases s3) (simp add: check_method_access_def Let_def)
  1.1590 -    obtain invC
  1.1591 -      where invC: "invC = invocation_class mode (store s2) a' statT"
  1.1592 -      by simp
  1.1593 -    with init_lvars
  1.1594 -    have invC': "invC = (invocation_class mode (store s3) a' statT)"
  1.1595 -      by (cases s2,cases mode) (auto simp add: init_lvars_def2 )
  1.1596 -    obtain n3 where
  1.1597 -     "G\<turnstile>Norm s0 \<midarrow>{accC',statT,mode}e\<cdot>mn( {pTs'}args)-\<succ>v\<midarrow>n3\<rightarrow> 
  1.1598 -          (set_lvars (locals (store s2))) s4"
  1.1599 -    proof (cases "normal s2")
  1.1600 -      case False
  1.1601 -      with init_lvars 
  1.1602 -      obtain keep_abrupt: "abrupt s3 = abrupt s2" and
  1.1603 -             "store s3 = store (init_lvars G invDeclC \<lparr>name = mn, parTs = pTs'\<rparr> 
  1.1604 -                                            mode a' vs s2)" 
  1.1605 -	by (auto simp add: init_lvars_def2)
  1.1606 -      moreover
  1.1607 -      from keep_abrupt False check
  1.1608 -      have eq_s3'_s3: "s3'=s3" 
  1.1609 -	by (auto simp add: check_method_access_def Let_def)
  1.1610 -      moreover
  1.1611 -      from eq_s3'_s3 False keep_abrupt eval_methd init_lvars
  1.1612 -      obtain "s4=s3'"
  1.1613 -      "In1 v=arbitrary3 (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>))"
  1.1614 -	by auto
  1.1615 -      moreover note False evaln.Abrupt
  1.1616 -      ultimately obtain m where 
  1.1617 -	"G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>-\<succ>v\<midarrow>m\<rightarrow> s4"
  1.1618 -	by force
  1.1619 -      from evaln_e evaln_args invDeclC init_lvars eq_s3'_s3 this
  1.1620 -      have 
  1.1621 -       "G\<turnstile>Norm s0 \<midarrow>{accC',statT,mode}e\<cdot>mn( {pTs'}args)-\<succ>v\<midarrow>max n1 (max n2 m)\<rightarrow> 
  1.1622 -            (set_lvars (locals (store s2))) s4"
  1.1623 -	by (auto intro!: evaln.Call le_maxI1 le_max3I1 le_max3I2)
  1.1624 -      with that show ?thesis 
  1.1625 -	by rules
  1.1626 -    next
  1.1627 -      case True
  1.1628 -      note normal_s2 = True
  1.1629 -      with eval_args
  1.1630 -      have normal_s1: "normal s1"
  1.1631 -	by (cases "normal s1") auto
  1.1632 -      with conf_a' eval_args 
  1.1633 -      have conf_a'_s2: "G, store s2\<turnstile>a'\<Colon>\<preceq>RefT statT"
  1.1634 -	by (auto dest: eval_gext intro: conf_gext)
  1.1635 -      show ?thesis
  1.1636 -      proof (cases "a'=Null \<longrightarrow> is_static statM")
  1.1637 -	case False
  1.1638 -	then obtain not_static: "\<not> is_static statM" and Null: "a'=Null" 
  1.1639 -	  by blast
  1.1640 -	with normal_s2 init_lvars mode
  1.1641 -	obtain np: "abrupt s3 = Some (Xcpt (Std NullPointer))" and
  1.1642 -                   "store s3 = store (init_lvars G invDeclC 
  1.1643 -                                       \<lparr>name = mn, parTs = pTs'\<rparr> mode a' vs s2)"
  1.1644 -	  by (auto simp add: init_lvars_def2)
  1.1645 -	moreover
  1.1646 -	from np check
  1.1647 -	have eq_s3'_s3: "s3'=s3" 
  1.1648 -	  by (auto simp add: check_method_access_def Let_def)
  1.1649 -	moreover
  1.1650 -	from eq_s3'_s3 np eval_methd init_lvars
  1.1651 -	obtain "s4=s3'"
  1.1652 -      "In1 v=arbitrary3 (In1l (Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>))"
  1.1653 -	  by auto
  1.1654 -	moreover note np
  1.1655 -	ultimately obtain m where 
  1.1656 -	  "G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>-\<succ>v\<midarrow>m\<rightarrow> s4"
  1.1657 -	  by force
  1.1658 -	from evaln_e evaln_args invDeclC init_lvars eq_s3'_s3 this
  1.1659 -	have 
  1.1660 -        "G\<turnstile>Norm s0 \<midarrow>{accC',statT,mode}e\<cdot>mn( {pTs'}args)-\<succ>v\<midarrow>max n1 (max n2 m)\<rightarrow> 
  1.1661 +    by (rules)
  1.1662 +  hence "G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<midarrow>max n1 n2
  1.1663 +          \<rightarrow> s2"
  1.1664 +    by (blast intro!: evaln.BinOp dest: evaln_max2)
  1.1665 +  then show ?case ..
  1.1666 +next
  1.1667 +  case (Super s )
  1.1668 +  have "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<midarrow>n\<rightarrow> Norm s"
  1.1669 +    by (rule evaln.Super)
  1.1670 +  then show ?case ..
  1.1671 +next
  1.1672 +  case (Acc f s0 s1 v va)
  1.1673 +  then obtain n where
  1.1674 +    "G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v, f)\<midarrow>n\<rightarrow> s1"
  1.1675 +    by (rules)
  1.1676 +  then
  1.1677 +  have "G\<turnstile>Norm s0 \<midarrow>Acc va-\<succ>v\<midarrow>n\<rightarrow> s1"
  1.1678 +    by (rule evaln.Acc)
  1.1679 +  then show ?case ..
  1.1680 +next
  1.1681 +  case (Ass e f s0 s1 s2 v var w)
  1.1682 +  then obtain n1 n2 where 
  1.1683 +    "G\<turnstile>Norm s0 \<midarrow>var=\<succ>(w, f)\<midarrow>n1\<rightarrow> s1"
  1.1684 +    "G\<turnstile>s1 \<midarrow>e-\<succ>v\<midarrow>n2\<rightarrow> s2"      
  1.1685 +    by (rules)
  1.1686 +  then
  1.1687 +  have "G\<turnstile>Norm s0 \<midarrow>var:=e-\<succ>v\<midarrow>max n1 n2\<rightarrow> assign f v s2"
  1.1688 +    by (blast intro: evaln.Ass dest: evaln_max2)
  1.1689 +  then show ?case ..
  1.1690 +next
  1.1691 +  case (Cond b e0 e1 e2 s0 s1 s2 v)
  1.1692 +  then obtain n1 n2 where 
  1.1693 +    "G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<midarrow>n1\<rightarrow> s1"
  1.1694 +    "G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<midarrow>n2\<rightarrow> s2"
  1.1695 +    by (rules)
  1.1696 +  then
  1.1697 +  have "G\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<midarrow>max n1 n2\<rightarrow> s2"
  1.1698 +    by (blast intro: evaln.Cond dest: evaln_max2)
  1.1699 +  then show ?case ..
  1.1700 +next
  1.1701 +  case (Call invDeclC a' accC' args e mn mode pTs' s0 s1 s2 s3 s3' s4 statT 
  1.1702 +        v vs)
  1.1703 +  then obtain n1 n2 where
  1.1704 +    "G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n1\<rightarrow> s1"
  1.1705 +    "G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<midarrow>n2\<rightarrow> s2"
  1.1706 +    by rules
  1.1707 +  moreover
  1.1708 +  have "invDeclC = invocation_declclass G mode (store s2) a' statT 
  1.1709 +                       \<lparr>name=mn,parTs=pTs'\<rparr>" .
  1.1710 +  moreover
  1.1711 +  have "s3 = init_lvars G invDeclC \<lparr>name=mn,parTs=pTs'\<rparr> mode a' vs s2" .
  1.1712 +  moreover
  1.1713 +  have "s3'=check_method_access G accC' statT mode \<lparr>name=mn,parTs=pTs'\<rparr> a' s3".
  1.1714 +  moreover 
  1.1715 +  from Call.hyps
  1.1716 +  obtain m where 
  1.1717 +    "G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name=mn, parTs=pTs'\<rparr>-\<succ>v\<midarrow>m\<rightarrow> s4"
  1.1718 +    by rules
  1.1719 +  ultimately
  1.1720 +  have "G\<turnstile>Norm s0 \<midarrow>{accC',statT,mode}e\<cdot>mn( {pTs'}args)-\<succ>v\<midarrow>max n1 (max n2 m)\<rightarrow> 
  1.1721              (set_lvars (locals (store s2))) s4"
  1.1722 -	  by (auto intro!: evaln.Call le_maxI1 le_max3I1 le_max3I2)
  1.1723 -	with that show ?thesis 
  1.1724 -	  by rules
  1.1725 -      next
  1.1726 -	case True
  1.1727 -	with mode have notNull: "mode = IntVir \<longrightarrow> a' \<noteq> Null"
  1.1728 -	  by (auto dest!: Null_staticD)
  1.1729 -	with conf_s2 conf_a'_s2 wf invC 
  1.1730 -	have dynT_prop: "G\<turnstile>mode\<rightarrow>invC\<preceq>statT"
  1.1731 -	  by (cases s2) (auto intro: DynT_propI)
  1.1732 -	with wt_e statM' invC mode wf 
  1.1733 -	obtain dynM where 
  1.1734 -           dynM: "dynlookup G statT invC  \<lparr>name=mn,parTs=pTs'\<rparr> = Some dynM" and
  1.1735 -           acc_dynM: "G \<turnstile>Methd  \<lparr>name=mn,parTs=pTs'\<rparr> dynM 
  1.1736 -                          in invC dyn_accessible_from accC"
  1.1737 -	  by (force dest!: call_access_ok)
  1.1738 -	with invC' check eq_accC_accC'
  1.1739 -	have eq_s3'_s3: "s3'=s3"
  1.1740 -	  by (auto simp add: check_method_access_def Let_def)
  1.1741 -	from dynT_prop wf wt_e statM' mode invC invDeclC dynM 
  1.1742 -	obtain 
  1.1743 -	   wf_dynM: "wf_mdecl G invDeclC (\<lparr>name=mn,parTs=pTs'\<rparr>,mthd dynM)" and
  1.1744 -	     dynM': "methd G invDeclC \<lparr>name=mn,parTs=pTs'\<rparr> = Some dynM" and
  1.1745 -           iscls_invDeclC: "is_class G invDeclC" and
  1.1746 -	        invDeclC': "invDeclC = declclass dynM" and
  1.1747 -	     invC_widen: "G\<turnstile>invC\<preceq>\<^sub>C invDeclC" and
  1.1748 -	   is_static_eq: "is_static dynM = is_static statM" and
  1.1749 -	   involved_classes_prop:
  1.1750 -             "(if invmode statM e = IntVir
  1.1751 -               then \<forall>statC. statT = ClassT statC \<longrightarrow> G\<turnstile>invC\<preceq>\<^sub>C statC
  1.1752 -               else ((\<exists>statC. statT = ClassT statC \<and> G\<turnstile>statC\<preceq>\<^sub>C invDeclC) \<or>
  1.1753 -                     (\<forall>statC. statT \<noteq> ClassT statC \<and> invDeclC = Object)) \<and>
  1.1754 -                      statDeclT = ClassT invDeclC)"
  1.1755 -	  by (auto dest: DynT_mheadsD)
  1.1756 -	obtain L' where 
  1.1757 -	   L':"L'=(\<lambda> k. 
  1.1758 -                 (case k of
  1.1759 -                    EName e
  1.1760 -                    \<Rightarrow> (case e of 
  1.1761 -                          VNam v 
  1.1762 -                          \<Rightarrow>(table_of (lcls (mbody (mthd dynM)))
  1.1763 -                             (pars (mthd dynM)[\<mapsto>]pTs')) v
  1.1764 -                        | Res \<Rightarrow> Some (resTy dynM))
  1.1765 -                  | This \<Rightarrow> if is_static statM 
  1.1766 -                            then None else Some (Class invDeclC)))"
  1.1767 -	  by simp
  1.1768 -	from wf_dynM [THEN wf_mdeclD1, THEN conjunct1] normal_s2 conf_s2 wt_e
  1.1769 -              wf eval_args conf_a' mode notNull wf_dynM involved_classes_prop
  1.1770 -	have conf_s3: "s3\<Colon>\<preceq>(G,L')"
  1.1771 -	   apply - 
  1.1772 -          (*FIXME confomrs_init_lvars should be 
  1.1773 -                adjusted to be more directy applicable *)
  1.1774 -	   apply (drule conforms_init_lvars [of G invDeclC 
  1.1775 -                  "\<lparr>name=mn,parTs=pTs'\<rparr>" dynM "store s2" vs pTs "abrupt s2" 
  1.1776 -                  L statT invC a' "(statDeclT,statM)" e])
  1.1777 -	     apply (rule wf)
  1.1778 -	     apply (rule conf_args,assumption)
  1.1779 -	     apply (simp add: pTs_widen)
  1.1780 -	     apply (cases s2,simp)
  1.1781 -	     apply (rule dynM')
  1.1782 -	     apply (force dest: ty_expr_is_type)
  1.1783 -	     apply (rule invC_widen)
  1.1784 -	     apply (force intro: conf_gext dest: eval_gext)
  1.1785 -	     apply simp
  1.1786 -	     apply simp
  1.1787 -	     apply (simp add: invC)
  1.1788 -	     apply (simp add: invDeclC)
  1.1789 -	     apply (force dest: wf_mdeclD1 is_acc_typeD)
  1.1790 -	     apply (cases s2, simp add: L' init_lvars
  1.1791 -	                      cong add: lname.case_cong ename.case_cong)
  1.1792 -	   done
  1.1793 -	with is_static_eq wf_dynM L'
  1.1794 -	obtain mthdT where
  1.1795 -	   "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>
  1.1796 -            \<turnstile>Body invDeclC (stmt (mbody (mthd dynM)))\<Colon>-mthdT" 
  1.1797 -	  by - (drule wf_mdecl_bodyD,
  1.1798 -                auto simp: cong add: lname.case_cong ename.case_cong)
  1.1799 -	with dynM' iscls_invDeclC invDeclC'
  1.1800 -	have
  1.1801 -	   "\<lparr>prg=G,cls=invDeclC,lcl=L'\<rparr>
  1.1802 -            \<turnstile>(Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>)\<Colon>-mthdT"
  1.1803 -	  by (auto intro: wt.Methd)
  1.1804 -	with conf_s3 eq_s3'_s3 hyp_methd
  1.1805 -	obtain m where
  1.1806 -	   "G\<turnstile>s3' \<midarrow>Methd invDeclC \<lparr>name = mn, parTs = pTs'\<rparr>-\<succ>v\<midarrow>m\<rightarrow> s4"
  1.1807 -	  by (blast)
  1.1808 -	from evaln_e evaln_args invDeclC init_lvars  eq_s3'_s3 this
  1.1809 -	have 
  1.1810 -        "G\<turnstile>Norm s0 \<midarrow>{accC',statT,mode}e\<cdot>mn( {pTs'}args)-\<succ>v\<midarrow>max n1 (max n2 m)\<rightarrow> 
  1.1811 -            (set_lvars (locals (store s2))) s4"
  1.1812 -	  by (auto intro!: evaln.Call le_maxI1 le_max3I1 le_max3I2)
  1.1813 -	with that show ?thesis 
  1.1814 -	  by rules
  1.1815 -      qed
  1.1816 -    qed
  1.1817 -    then show ?case ..
  1.1818 -  next
  1.1819 -    case (Methd D s0 s1 sig v L accC T)
  1.1820 -    then obtain n where
  1.1821 -      "G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<midarrow>n\<rightarrow> s1"
  1.1822 -      by - (erule wt_elim_cases, force simp add: body_def2)
  1.1823 -    then have "G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<midarrow>Suc n\<rightarrow> s1"
  1.1824 -      by (rule evaln.Methd)
  1.1825 -    then show ?case ..
  1.1826 -  next
  1.1827 -    case (Body D c s0 s1 s2 L accC T)
  1.1828 -    with wf obtain n1 n2 where 
  1.1829 -      "G\<turnstile>Norm s0 \<midarrow>Init D\<midarrow>n1\<rightarrow> s1"
  1.1830 -      "G\<turnstile>s1 \<midarrow>c\<midarrow>n2\<rightarrow> s2"
  1.1831 -      by (blast elim!: wt_elim_cases dest: eval_type_sound)
  1.1832 -    then have 
  1.1833 +    by (auto intro!: evaln.Call le_maxI1 le_max3I1 le_max3I2)
  1.1834 +  thus ?case ..
  1.1835 +next
  1.1836 +  case (Methd D s0 s1 sig v )
  1.1837 +  then obtain n where
  1.1838 +    "G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<midarrow>n\<rightarrow> s1"
  1.1839 +    by rules
  1.1840 +  then have "G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<midarrow>Suc n\<rightarrow> s1"
  1.1841 +    by (rule evaln.Methd)
  1.1842 +  then show ?case ..
  1.1843 +next
  1.1844 +  case (Body D c s0 s1 s2 s3 )
  1.1845 +  from Body.hyps obtain n1 n2 where 
  1.1846 +    evaln_init: "G\<turnstile>Norm s0 \<midarrow>Init D\<midarrow>n1\<rightarrow> s1" and
  1.1847 +    evaln_c: "G\<turnstile>s1 \<midarrow>c\<midarrow>n2\<rightarrow> s2"
  1.1848 +    by (rules)
  1.1849 +  moreover
  1.1850 +  have "s3 = (if \<exists>l. fst s2 = Some (Jump (Break l)) \<or> 
  1.1851 +                     fst s2 = Some (Jump (Cont l))
  1.1852 +                 then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2 
  1.1853 +                 else s2)".
  1.1854 +  ultimately
  1.1855 +  have
  1.1856       "G\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>the (locals (store s2) Result)\<midarrow>max n1 n2
  1.1857 -       \<rightarrow> abupd (absorb Ret) s2"
  1.1858 -      by (blast intro: evaln.Body dest: evaln_max2)
  1.1859 -    then show ?case ..
  1.1860 -  next
  1.1861 -    case (LVar s vn L accC T)
  1.1862 -    obtain n where
  1.1863 -      "G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<midarrow>n\<rightarrow> Norm s"
  1.1864 -      by (rules intro: evaln.LVar)
  1.1865 -    then show ?case ..
  1.1866 -  next
  1.1867 -    case (FVar a accC e fn s0 s1 s2 s2' s3 stat statDeclC v L accC' T)
  1.1868 -    have eval_init: "G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<rightarrow> s1" .
  1.1869 -    have eval_e: "G\<turnstile>s1 \<midarrow>e-\<succ>a\<rightarrow> s2" .
  1.1870 -    have check: "s3 = check_field_access G accC statDeclC fn stat a s2'" .
  1.1871 -    have hyp_init: "PROP ?EqEval (Norm s0) s1 (In1r (Init statDeclC)) \<diamondsuit>" .
  1.1872 -    have hyp_e: "PROP ?EqEval s1 s2 (In1l e) (In1 a)" .
  1.1873 -    have fvar: "(v, s2') = fvar statDeclC stat fn a s2" .
  1.1874 -    have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
  1.1875 -    have wt: "\<lparr>prg=G, cls=accC', lcl=L\<rparr>\<turnstile>In2 ({accC,statDeclC,stat}e..fn)\<Colon>T" .
  1.1876 -    then obtain statC f where
  1.1877 -                wt_e: "\<lparr>prg=G, cls=accC, lcl=L\<rparr>\<turnstile>e\<Colon>-Class statC" and
  1.1878 -            accfield: "accfield G accC statC fn = Some (statDeclC,f)" and
  1.1879 -                stat: "stat=is_static f" and
  1.1880 -               accC': "accC'=accC" and
  1.1881 -	           T: "T=(Inl (type f))"
  1.1882 -       by (rule wt_elim_cases) (fastsimp simp add: member_is_static_simp)
  1.1883 -    from wf wt_e 
  1.1884 -    have iscls_statC: "is_class G statC"
  1.1885 -      by (auto dest: ty_expr_is_type type_is_class)
  1.1886 -    with wf accfield 
  1.1887 -    have iscls_statDeclC: "is_class G statDeclC"
  1.1888 -      by (auto dest!: accfield_fields dest: fields_declC)
  1.1889 -    then 
  1.1890 -    have wt_init: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>(Init statDeclC)\<Colon>\<surd>"
  1.1891 -      by simp
  1.1892 -    from conf_s0 wt_init
  1.1893 -    obtain n1 where
  1.1894 -      evaln_init: "G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<midarrow>n1\<rightarrow> s1"
  1.1895 -      by (rules dest: hyp_init)
  1.1896 -    from eval_init wt_init conf_s0 wf 
  1.1897 -    have conf_s1: "s1\<Colon>\<preceq>(G, L)"
  1.1898 -      by (blast dest: eval_type_sound)
  1.1899 -    with wt_e
  1.1900 -    obtain n2 where
  1.1901 -      evaln_e: "G\<turnstile>s1 \<midarrow>e-\<succ>a\<midarrow>n2\<rightarrow> s2"
  1.1902 -      by (blast dest: hyp_e)
  1.1903 -    from eval_e wf conf_s1 wt_e
  1.1904 -    obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and
  1.1905 -            conf_a: "normal s2 \<longrightarrow> G,store s2\<turnstile>a\<Colon>\<preceq>Class statC"
  1.1906 -      by (auto dest!: eval_type_sound)
  1.1907 -    from accfield wt_e eval_init eval_e conf_s2 conf_a fvar stat check  wf
  1.1908 -    have eq_s3_s2': "s3=s2'"  
  1.1909 -      by (auto dest!: error_free_field_access)
  1.1910 -    with evaln_init evaln_e fvar accC'
  1.1911 -    have "G\<turnstile>Norm s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>v\<midarrow>max n1 n2\<rightarrow> s3"
  1.1912 -      by (auto intro: evaln.FVar dest: evaln_max2)
  1.1913 -    then show ?case ..
  1.1914 -  next
  1.1915 -    case (AVar a e1 e2 i s0 s1 s2 s2' v L accC T)
  1.1916 -    with wf obtain n1 n2 where 
  1.1917 -      "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>a\<midarrow>n1\<rightarrow> s1"
  1.1918 -      "G\<turnstile>s1 \<midarrow>e2-\<succ>i\<midarrow>n2\<rightarrow> s2"      
  1.1919 -      by (blast elim!: wt_elim_cases dest: eval_type_sound)
  1.1920 -    moreover 
  1.1921 -    have "(v, s2') = avar G i a s2" .
  1.1922 -    ultimately 
  1.1923 -    have "G\<turnstile>Norm s0 \<midarrow>e1.[e2]=\<succ>v\<midarrow>max n1 n2\<rightarrow> s2'"
  1.1924 -      by (blast intro!: evaln.AVar dest: evaln_max2)
  1.1925 -    then show ?case ..
  1.1926 -  next
  1.1927 -    case (Nil s0 L accC T)
  1.1928 -    show ?case by (rules intro: evaln.Nil)
  1.1929 -  next
  1.1930 -    case (Cons e es s0 s1 s2 v vs L accC T)
  1.1931 -    with wf obtain n1 n2 where 
  1.1932 -      "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n1\<rightarrow> s1"
  1.1933 -      "G\<turnstile>s1 \<midarrow>es\<doteq>\<succ>vs\<midarrow>n2\<rightarrow> s2"      
  1.1934 -      by (blast elim!: wt_elim_cases dest: eval_type_sound)
  1.1935 -    then
  1.1936 -    have "G\<turnstile>Norm s0 \<midarrow>e # es\<doteq>\<succ>v # vs\<midarrow>max n1 n2\<rightarrow> s2"
  1.1937 -      by (blast intro!: evaln.Cons dest: evaln_max2)
  1.1938 -    then show ?case ..
  1.1939 -  qed
  1.1940 +       \<rightarrow> abupd (absorb Ret) s3"
  1.1941 +    by (rules intro: evaln.Body dest: evaln_max2)
  1.1942 +  then show ?case ..
  1.1943 +next
  1.1944 +  case (LVar s vn )
  1.1945 +  obtain n where
  1.1946 +    "G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<midarrow>n\<rightarrow> Norm s"
  1.1947 +    by (rules intro: evaln.LVar)
  1.1948 +  then show ?case ..
  1.1949 +next
  1.1950 +  case (FVar a accC e fn s0 s1 s2 s2' s3 stat statDeclC v)
  1.1951 +  then obtain n1 n2 where
  1.1952 +    "G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<midarrow>n1\<rightarrow> s1"
  1.1953 +    "G\<turnstile>s1 \<midarrow>e-\<succ>a\<midarrow>n2\<rightarrow> s2"
  1.1954 +    by rules
  1.1955 +  moreover
  1.1956 +  have "s3 = check_field_access G accC statDeclC fn stat a s2'" 
  1.1957 +       "(v, s2') = fvar statDeclC stat fn a s2" .
  1.1958 +  ultimately
  1.1959 +  have "G\<turnstile>Norm s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>v\<midarrow>max n1 n2\<rightarrow> s3"
  1.1960 +    by (rules intro: evaln.FVar dest: evaln_max2)
  1.1961 +  then show ?case ..
  1.1962 +next
  1.1963 +  case (AVar a e1 e2 i s0 s1 s2 s2' v )
  1.1964 +  then obtain n1 n2 where 
  1.1965 +    "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>a\<midarrow>n1\<rightarrow> s1"
  1.1966 +    "G\<turnstile>s1 \<midarrow>e2-\<succ>i\<midarrow>n2\<rightarrow> s2"      
  1.1967 +    by rules
  1.1968 +  moreover 
  1.1969 +  have "(v, s2') = avar G i a s2" .
  1.1970 +  ultimately 
  1.1971 +  have "G\<turnstile>Norm s0 \<midarrow>e1.[e2]=\<succ>v\<midarrow>max n1 n2\<rightarrow> s2'"
  1.1972 +    by (blast intro!: evaln.AVar dest: evaln_max2)
  1.1973 +  then show ?case ..
  1.1974 +next
  1.1975 +  case (Nil s0)
  1.1976 +  show ?case by (rules intro: evaln.Nil)
  1.1977 +next
  1.1978 +  case (Cons e es s0 s1 s2 v vs)
  1.1979 +  then obtain n1 n2 where 
  1.1980 +    "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n1\<rightarrow> s1"
  1.1981 +    "G\<turnstile>s1 \<midarrow>es\<doteq>\<succ>vs\<midarrow>n2\<rightarrow> s2"      
  1.1982 +    by rules
  1.1983 +  then
  1.1984 +  have "G\<turnstile>Norm s0 \<midarrow>e # es\<doteq>\<succ>v # vs\<midarrow>max n1 n2\<rightarrow> s2"
  1.1985 +    by (blast intro!: evaln.Cons dest: evaln_max2)
  1.1986 +  then show ?case ..
  1.1987  qed
  1.1988 -
  1.1989 +       
  1.1990  end