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.7 -theory Evaln = Eval + TypeSafe:
1.8 +theory Evaln = TypeSafe:
1.9 +
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.34  consts
1.35 @@ -63,18 +76,19 @@
1.37  inductive "evaln G" intros
1.39 -(* propagation of abrupt completion *)
1.40 +--{* propagation of abrupt completion *}
1.42    Abrupt:   "G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (arbitrary3 t,(Some xc,s))"
1.45 -(* evaluation of variables *)
1.46 +--{* evaluation of variables *}
1.48    LVar:	"G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<midarrow>n\<rightarrow> Norm s"
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.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.64 -(* evaluation of expressions *)
1.65 +--{* evaluation of expressions *}
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.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.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.96 -(* evaluation of expression lists *)
1.97 +--{* evaluation of expression lists *}
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.105 -(* execution of statements *)
1.106 +--{* execution of statements *}
1.108    Skip:	 			    "G\<turnstile>Norm s \<midarrow>Skip\<midarrow>n\<rightarrow> Norm s"
1.110 @@ -168,13 +188,13 @@
1.111  		       G\<turnstile>Norm s0 \<midarrow>If(e) c1 Else c2 \<midarrow>n\<rightarrow> s2"
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.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.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.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.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.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.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.165  declare split_if     [split] split_if_asm     [split]
1.166          option.split [split] option.split_asm [split]
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.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.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.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.210  section {* evaln implies eval *}
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.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.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.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.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.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.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.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.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.928 +ML {*
1.929 +Delsimprocs [wt_expr_proc,wt_var_proc,wt_exprs_proc,wt_stmt_proc]
1.930 +*}
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.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.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.1990  end