Theory TypeSafe

(*  Title:       CoreC++
    Author:      Daniel Wasserrab
    Maintainer:  Daniel Wasserrab <wasserra at fmi.uni-passau.de>

    Based on the Jinja theory J/TypeSafe.thy by Tobias Nipkow 
*)

section ‹Type Safety Proof›

theory TypeSafe
imports HeapExtension CWellForm
begin


subsection‹Basic preservation lemmas›

lemma assumes wf:"wwf_prog P" and casts:"P  T casts v to v'"
  and typeof:"P  typeof⇘hv = Some T'" and leq:"P  T'  T"
  shows casts_conf:"P,h  v' :≤ T"

proof -
  { fix a' C Cs S'
    assume leq:"P  Class (last Cs)  T" and subo:"Subobjs P C Cs"
      and casts':"P  T casts Ref (a',Cs) to v'" and h:"h a' = Some(C,S')"
    from subo wf have "is_class P (last Cs)" by(fastforce intro:Subobj_last_isClass)
    with leq wf obtain C' where T:"T = Class C'"
      and path_unique:"P  Path (last Cs) to C' unique"
      by(auto dest:Class_widen)
    from path_unique obtain Cs' where path_via:"P  Path (last Cs) to C' via Cs'"
      by(auto simp:path_via_def path_unique_def)
    with T path_unique casts' have v':"v' = Ref (a',Cs@pCs')"
      by -(erule casts_to.cases,auto simp:path_unique_def path_via_def)
    from subo path_via wf have "Subobjs P C (Cs@pCs')"
      and "last (Cs@pCs') = C'"
      apply(auto intro:Subobjs_appendPath simp:path_via_def)
      apply(drule_tac Cs="Cs'" in Subobjs_nonempty)
      by(rule sym[OF appendPath_last])
    with T h v' have ?thesis by auto }
  with casts typeof wf typeof leq show ?thesis
    by(cases v,auto elim:casts_to.cases split:if_split_asm)
qed



theorem assumes wf:"wwf_prog P"
shows red_preserves_hconf:
  "P,E  e,(h,l)  e',(h',l')  (T.  P,E,h  e : T; P  h    P  h' )"
and reds_preserves_hconf:
  "P,E  es,(h,l) [→] es',(h',l')  (Ts.  P,E,h  es [:] Ts; P  h    P  h' )"

proof (induct rule:red_reds_inducts)
  case (RedNew h a h' C E l)
  have new: "new_Addr h = Some a" and h':"h' = h(a  (C, Collect (init_obj P C)))"
    and hconf:"P  h " and wt_New:"P,E,h  new C : T" by fact+
  from new have None: "h a = None" by(rule new_Addr_SomeD)
  with wf have oconf:"P,h  (C, Collect (init_obj P C)) "
    apply (auto simp:oconf_def)
    apply (rule_tac x="init_class_fieldmap P (last Cs)" in exI)
    by (fastforce intro:init_obj.intros fconf_init_fields 
                 elim: init_obj.cases dest!:Subobj_last_isClass simp:is_class_def)+
  thus ?case using h' None by(fast intro: hconf_new[OF hconf])
next
  case (RedFAss h a D S Cs' F T Cs v v' Ds fs' E l T')
  let ?fs' = "fs'(F  v')"
  let ?S' = "insert (Ds, ?fs') (S - {(Ds, fs')})"
  have ha:"h a = Some(D,S)" and hconf:"P  h "
    and field:"P  last Cs' has least F:T via Cs"
    and casts:"P  T casts v to v'"
    and Ds:"Ds = Cs' @p Cs" and S:"(Ds,fs')  S"
    and wte:"P,E,h  ref(a,Cs')F{Cs} := Val v : T'" by fact+
  from wte have "P  last Cs' has least F:T' via Cs" by (auto split:if_split_asm)
  with field have eq:"T = T'" by (rule sees_field_fun)
  with casts wte wf have conf:"P,h  v' :≤ T'"
    by(auto intro:casts_conf)
  from hconf ha have oconf:"P,h  (D,S) " by (fastforce simp:hconf_def)
  with S have suboD:"Subobjs P D Ds" by (fastforce simp:oconf_def)
  from field obtain Bs fs ms
    where subo:"Subobjs P (last Cs') Cs"
    and "class": "class P (last Cs) = Some(Bs,fs,ms)"
    and map:"map_of fs F = Some T"
    by (auto simp:LeastFieldDecl_def FieldDecls_def)
  from Ds subo have last:"last Cs = last Ds"
    by(fastforce dest:Subobjs_nonempty intro:appendPath_last simp:appendPath_last)
  with "class" have classDs:"class P (last Ds) = Some(Bs,fs,ms)" by simp
  with S suboD oconf have "P,h  fs' (:≤) map_of fs"
    apply (auto simp:oconf_def)
    apply (erule allE)
    apply (erule_tac x="Ds" in allE)
    apply (erule_tac x="fs'" in allE)
    apply clarsimp
    done
  with map conf eq have fconf:"P,h  fs'(F  v') (:≤) map_of fs"
    by (simp add:fconf_def)
  from oconf have "Cs fs'. (Cs,fs')  S  Subobjs P D Cs  
                    (fs Bs ms. class P (last Cs) = Some (Bs,fs,ms)  
                                P,h  fs' (:≤) map_of fs)"
    by(simp add:oconf_def)
  with suboD classDs fconf 
  have oconf':"Cs fs'. (Cs,fs')  ?S'  Subobjs P D Cs  
                    (fs Bs ms. class P (last Cs) = Some (Bs,fs,ms)  
                                P,h  fs' (:≤) map_of fs)"
    by auto
  from oconf have all:"Cs. Subobjs P D Cs  (∃!fs'. (Cs,fs')  S)"
    by(simp add:oconf_def)
  with S have "Cs. Subobjs P D Cs  (∃!fs'. (Cs,fs')  ?S')" by blast
  with oconf' have oconf':"P,h  (D,?S') "
    by (simp add:oconf_def)
  with hconf ha show ?case by (rule hconf_upd_obj)
next
  case (CallObj E e h l e' h' l' Copt M es) thus ?case by (cases Copt) auto
next
  case (CallParams E es h l es' h' l' v Copt M) thus ?case by (cases Copt) auto
next
  case (RedCallNull E Copt M vs h l) thus ?case by (cases Copt) auto
qed auto




theorem assumes wf:"wwf_prog P"
shows red_preserves_lconf:
  "P,E  e,(h,l)  e',(h',l') 
  (T.  P,E,h  e:T; P,h  l (:≤)w E; P  E    P,h'  l' (:≤)w E)"
and reds_preserves_lconf:
  "P,E  es,(h,l) [→] es',(h',l') 
  (Ts.  P,E,h  es[:]Ts; P,h  l (:≤)w E; P  E    P,h'  l' (:≤)w E)"

proof(induct rule:red_reds_inducts)
  case RedNew thus ?case
    by(fast intro:lconf_hext red_hext_incr[OF red_reds.RedNew])
next
  case (RedLAss E V T v v' h l T')
  have casts:"P  T casts v to v'" and env:"E V = Some T"
    and wt:"P,E,h  V:=Val v : T'" and lconf:"P,h  l (:≤)w E" by fact+
  from wt env have eq:"T = T'" by auto
  with casts wt wf have conf:"P,h  v' :≤ T'"
    by(auto intro:casts_conf)
  with lconf env eq show ?case
    by (simp del:fun_upd_apply)(erule lconf_upd,simp_all)
next
  case RedFAss thus ?case
    by(auto intro:lconf_hext red_hext_incr[OF red_reds.RedFAss] 
         simp del:fun_upd_apply)
next
  case (BlockRedNone E V T e h l e' h' l' T')
  have red:"P,E(V  T)  e,(h, l(V := None))  e',(h', l')"
    and IH: "T''.  P,E(V  T),h  e : T''; P,h  l(V:=None) (:≤)w E(V  T);
                      envconf P (E(V  T)) 
                    P,h'  l' (:≤)w E(V  T)"
    and lconf: "P,h  l (:≤)w E" and wte: "P,E,h  {V:T; e} : T'"
    and envconf:"envconf P E" by fact+
  from lconf_hext[OF lconf red_hext_incr[OF red]]
  have lconf':"P,h'  l (:≤)w E" .
  from wte have wte':"P,E(VT),h  e : T'" and type:"is_type P T"
    by (auto elim:WTrt.cases)
  from envconf type have envconf':"envconf P (E(V  T))"
    by(auto simp:envconf_def)
  from lconf have "P,h  (l(V := None)) (:≤)w E(VT)"
    by (simp add:lconf_def fun_upd_apply)
  from IH[OF wte' this envconf'] have "P,h'  l' (:≤)w E(VT)" .
  with lconf' show ?case
    by (fastforce simp:lconf_def fun_upd_apply split:if_split_asm)
next
  case (BlockRedSome E V T e h l e' h' l' v T')
  have red:"P,E(V  T)  e,(h, l(V := None))  e',(h', l')"
    and IH: "T''.  P,E(V  T),h  e : T''; P,h  l(V:=None) (:≤)w E(V  T);
                      envconf P (E(V  T)) 
                    P,h'  l' (:≤)w E(V  T)"
    and lconf: "P,h  l (:≤)w E" and wte: "P,E,h  {V:T; e} : T'"
    and envconf:"envconf P E" by fact+
  from lconf_hext[OF lconf red_hext_incr[OF red]]
  have lconf':"P,h'  l (:≤)w E" .
  from wte have wte':"P,E(VT),h  e : T'" and type:"is_type P T"
    by (auto elim:WTrt.cases)
  from envconf type have envconf':"envconf P (E(V  T))"
    by(auto simp:envconf_def)
  from lconf have "P,h  (l(V := None)) (:≤)w E(VT)"
    by (simp add:lconf_def fun_upd_apply)
  from IH[OF wte' this envconf'] have "P,h'  l' (:≤)w E(VT)" .
  with lconf' show ?case
    by (fastforce simp:lconf_def fun_upd_apply split:if_split_asm)
next
  case (InitBlockRed E V T e h l v' e' h' l' v'' v T')
  have red: "P,E(V  T)  e, (h, l(Vv'))  e',(h', l')"
     and IH: "T''.  P,E(V  T),h  e : T''; P,h  l(V  v') (:≤)w E(V  T); 
                       envconf P (E(V  T)) 
                    P,h'  l' (:≤)w E(V  T)"
    and lconf:"P,h  l (:≤)w E" and l':"l' V = Some v''"
    and wte:"P,E,h  {V:T; V:=Val v;; e} : T'"
    and casts:"P  T casts v to v'" and envconf:"envconf P E" by fact+
  from lconf_hext[OF lconf red_hext_incr[OF red]]
  have lconf':"P,h'  l (:≤)w E" .
  from wte obtain T'' where wte':"P,E(VT),h  e : T'"
    and wt:"P,E(V  T),h  V:=Val v : T''"
    and type:"is_type P T"
    by (auto elim:WTrt.cases)
  from envconf type have envconf':"envconf P (E(V  T))"
    by(auto simp:envconf_def)
  from wt have "T'' = T" by auto
  with wf casts wt have "P,h  v' :≤ T"
    by(auto intro:casts_conf)
  with lconf have "P,h  l(V  v') (:≤)w E(VT)"
    by -(rule lconf_upd2)
  from IH[OF wte' this envconf'] have "P,h'  l' (:≤)w E(V  T)" .
  with lconf' show ?case
    by (fastforce simp:lconf_def fun_upd_apply split:if_split_asm)
next
  case (CallObj E e h l e' h' l' Copt M es) thus ?case by (cases Copt) auto
next
  case (CallParams E es h l es' h' l' v Copt M) thus ?case by (cases Copt) auto
next
  case (RedCallNull E Copt M vs h l) thus ?case by (cases Copt) auto
qed auto




text‹Preservation of definite assignment more complex and requires a
few lemmas first.›

lemma [iff]: "A.  length Vs = length Ts; length vs = length Ts 
 𝒟 (blocks (Vs,Ts,vs,e)) A = 𝒟 e (A  set Vs)"

apply(induct Vs Ts vs e rule:blocks_old_induct)
apply(simp_all add:hyperset_defs)
done


lemma red_lA_incr: "P,E  e,(h,l)  e',(h',l')  dom l  𝒜 e   dom l'  𝒜 e'"
  and reds_lA_incr: "P,E  es,(h,l) [→] es',(h',l')  dom l  𝒜s es   dom l'  𝒜s es'"
  apply (induct rule:red_reds_inducts)
  apply (simp_all del: fun_upd_apply add: hyperset_defs)
  apply blast
  apply blast
  apply blast
  apply blast
  apply blast
  apply blast
  apply blast
  apply auto
  done



text‹Now preservation of definite assignment.›

lemma assumes wf: "wf_C_prog P"
shows red_preserves_defass:
  "P,E  e,(h,l)  e',(h',l')  𝒟 e dom l  𝒟 e' dom l'"
and "P,E  es,(h,l) [→] es',(h',l')  𝒟s es dom l  𝒟s es' dom l'"

proof (induct rule:red_reds_inducts)
  case BinOpRed1 thus ?case by (auto elim!: D_mono[OF red_lA_incr])
next
  case FAssRed1 thus ?case by (auto elim!: D_mono[OF red_lA_incr])
next
  case CallObj thus ?case by (auto elim!: Ds_mono[OF red_lA_incr])
next
  case (RedCall h l a C S Cs M Ts' T' pns' body' Ds Ts T pns body Cs'
                vs bs new_body E)
  thus ?case
    apply (auto dest!:select_method_wf_mdecl[OF wf] simp:wf_mdecl_def elim!:D_mono')
    apply(cases T') apply auto
    by(rule_tac A="insert this (set pns)" in D_mono,clarsimp simp:hyperset_defs,
          assumption)+
next
  case RedStaticCall thus ?case
    apply (auto dest!:has_least_wf_mdecl[OF wf] simp:wf_mdecl_def elim!:D_mono')
    by(auto simp:hyperset_defs)
next
  case InitBlockRed thus ?case
    by(auto simp:hyperset_defs elim!:D_mono' simp del:fun_upd_apply)
next
  case BlockRedNone thus ?case
    by(auto simp:hyperset_defs elim!:D_mono' simp del:fun_upd_apply)
next
  case BlockRedSome thus ?case
    by(auto simp:hyperset_defs elim!:D_mono' simp del:fun_upd_apply)
next
  case SeqRed thus ?case by (auto elim!: D_mono[OF red_lA_incr])
next
  case CondRed thus ?case by (auto elim!: D_mono[OF red_lA_incr])
next
  case RedWhile thus ?case by(auto simp:hyperset_defs elim!:D_mono')
next
  case ListRed1 thus ?case by (auto elim!: Ds_mono[OF red_lA_incr])
qed (auto simp:hyperset_defs)




text‹Combining conformance of heap and local variables:›

definition sconf :: "prog  env  state  bool"  ("_,_  _ "   [51,51,51]50) where
  "P,E  s     let (h,l) = s in P  h   P,h  l (:≤)w E  P  E "

lemma red_preserves_sconf:
  " P,E  e,s  e',s'; P,E,hp s  e : T; P,E  s ; wwf_prog P 
 P,E  s' "

by(fastforce intro:red_preserves_hconf red_preserves_lconf
            simp add:sconf_def)


lemma reds_preserves_sconf:
  " P,E  es,s [→] es',s'; P,E,hp s  es [:] Ts; P,E  s ; wwf_prog P 
 P,E  s' "

by(fastforce intro:reds_preserves_hconf reds_preserves_lconf
            simp add:sconf_def)





subsection "Subject reduction"

lemma wt_blocks:
 "E.  length Vs = length Ts; length vs = length Ts;
         T'  set Ts. is_type P T' 
       (P,E,h  blocks(Vs,Ts,vs,e) : T) =
  (P,E(Vs[↦]Ts),h  e:T  
  (Ts'. map (P  typeof⇘h) vs = map Some Ts'  P  Ts' [≤] Ts))"

proof(induct Vs Ts vs e rule:blocks_old_induct)
  case (5 V Vs T' Ts v vs e)
  have length:"length (V#Vs) = length (T'#Ts)" "length (v#vs) = length (T'#Ts)"
    and type:"S  set (T'#Ts). is_type P S"
    and IH:"E. length Vs = length Ts; length vs = length Ts;
                  S  set Ts. is_type P S
      (P,E,h  blocks (Vs, Ts, vs, e) : T) =
         (P,E(Vs [↦] Ts),h  e : T 
            (Ts'. map P  typeof⇘hvs = map Some Ts'  P  Ts' [≤] Ts))" by fact+
  from type have typeT':"is_type P T'" and type':"S  set Ts. is_type P S"
    by simp_all
  from length have "length Vs = length Ts" "length vs = length Ts"
    by simp_all
  from IH[OF this type'] have eq:"(P,E(V  T'),h  blocks (Vs,Ts,vs,e) : T) =
  (P,E(V  T', Vs [↦] Ts),h  e : T 
   (Ts'. map P  typeof⇘hvs = map Some Ts'  P  Ts' [≤] Ts))" .
  show ?case
  proof(rule iffI)
    assume "P,E,h  blocks (V#Vs,T'#Ts,v#vs,e) : T"
    then have wt:"P,E(V  T'),h  V:=Val v : T'"
      and blocks:"P,E(V  T'),h  blocks (Vs,Ts,vs,e) : T" by auto
    from blocks eq obtain Ts' where wte:"P,E(V  T', Vs [↦] Ts),h  e : T"
      and typeof:"map P  typeof⇘hvs = map Some Ts'" and subs:"P  Ts' [≤] Ts"
      by auto
    from wt obtain T'' where "P  typeof⇘hv = Some T''" and "P  T''  T'"
      by auto
    with wte typeof subs
    show "P,E(V # Vs [↦] T' # Ts),h  e : T 
          (Ts'. map P  typeof⇘h(v # vs) = map Some Ts'  P  Ts' [≤] (T' # Ts))"
      by auto
  next
    assume "P,E(V # Vs [↦] T' # Ts),h  e : T 
      (Ts'. map P  typeof⇘h(v # vs) = map Some Ts'  P  Ts' [≤] (T' # Ts))"
    then obtain Ts' where wte:"P,E(V # Vs [↦] T' # Ts),h  e : T"
      and typeof:"map P  typeof⇘h(v # vs) = map Some Ts'"
      and subs:"P  Ts' [≤] (T'#Ts)" by auto
    from subs obtain U Us where Ts':"Ts' = U#Us" by(cases Ts') auto
    with wte typeof subs eq have blocks:"P,E(V  T'),h  blocks (Vs,Ts,vs,e) : T"
      by auto
    from Ts' typeof subs have "P  typeof⇘hv = Some U"
      and "P  U  T'" by (auto simp:fun_of_def)
    hence wtval:"P,E(V  T'),h  V:=Val v : T'" by auto
    with blocks typeT' show "P,E,h  blocks (V#Vs,T'#Ts,v#vs,e) : T" by auto
  qed
qed auto




theorem assumes wf: "wf_C_prog P"
shows subject_reduction2: "P,E  e,(h,l)  e',(h',l') 
  (T.  P,E  (h,l) ; P,E,h  e : T   P,E,h'  e' :NT T)"
and subjects_reduction2: "P,E  es,(h,l) [→] es',(h',l') 
  (Ts. P,E  (h,l) ; P,E,h  es [:] Ts   types_conf P E h' es' Ts)"

proof (induct rule:red_reds_inducts)
  case (RedNew h a h' C E l)
  have new:"new_Addr h = Some a" and h':"h' = h(a  (C, Collect (init_obj P C)))" 
    and wt:"P,E,h  new C : T" by fact+
  from wt have eq:"T = Class C" and "class": "is_class P C" by auto
  from "class" have subo:"Subobjs P C [C]" by(rule Subobjs_Base)
  from h' have "h' a = Some(C, Collect (init_obj P C))" by(simp add:map_upd_Some_unfold)
  with subo have "P,E,h'  ref(a,[C]) : Class C" by auto
  with eq show ?case by auto
next
  case (RedNewFail h E C l)
  have sconf:"P,E  (h, l) " by fact
  from wf have "is_class P OutOfMemory" 
    by (fastforce intro:is_class_xcpt wf_prog_wwf_prog)
  hence "preallocated h  P  typeof⇘h(Ref (addr_of_sys_xcpt OutOfMemory,[OutOfMemory])) = Some(Class OutOfMemory)"
    by (auto elim: preallocatedE dest!:preallocatedD Subobjs_Base)
  with sconf have "P,E,h  THROW OutOfMemory : T" by(auto simp:sconf_def hconf_def)
  thus ?case by (fastforce intro:wt_same_type_typeconf)
next
  case (StaticCastRed E e h l e' h' l' C)
  have wt:"P,E,h  Ce : T"
    and IH:"T'. P,E  (h,l) ; P,E,h  e : T' 
             P,E,h'  e' :NT T'"
    and sconf:"P,E  (h, l) " by fact+
  from wt obtain T' where wte:"P,E,h  e : T'" and isref:"is_refT T'" 
    and "class": "is_class P C" and T:"T = Class C"
    by auto
  from isref have "P,E,h'  Ce' : Class C"
  proof(rule refTE)
    assume "T' = NT"
    with IH[OF sconf wte] isref "class" show ?thesis by auto
  next
    fix D assume "T' = Class D"
    with IH[OF sconf wte] isref "class" show ?thesis by auto
  qed
  with T show ?case by (fastforce intro:wt_same_type_typeconf)
next
  case RedStaticCastNull
  thus ?case by (auto elim:WTrt.cases)
next
  case (RedStaticUpCast Cs C Cs' Ds E a h l)
  have wt:"P,E,h  Cref (a,Cs) : T"
    and path_via:"P  Path last Cs to C via Cs'"
    and Ds:"Ds = Cs @p Cs'" by fact+
  from wt have typeof:"P  typeof⇘h(Ref(a,Cs)) = Some(Class(last Cs))"
    and "class": "is_class P C" and T:"T = Class C"
    by auto
  from typeof obtain D S where h:"h a = Some(D,S)" and subo:"Subobjs P D Cs"
    by (auto dest:typeof_Class_Subo split:if_split_asm)
  from path_via subo wf Ds have "Subobjs P D Ds" and last:"last Ds = C"
    by(auto intro!:Subobjs_appendPath appendPath_last[THEN sym] Subobjs_nonempty
            simp:path_via_def)
  with h have "P,E,h  ref (a,Ds) : Class C" by auto
  with T show ?case by (fastforce intro:wt_same_type_typeconf)
next
  case (RedStaticDownCast E C a Cs Cs' h l)
  have "P,E,h  Cref (a,Cs@[C]@Cs') : T" by fact
  hence typeof:"P  typeof⇘h(Ref(a,Cs@[C]@Cs')) = Some(Class(last(Cs@[C]@Cs')))"
    and "class": "is_class P C" and T:"T = Class C"
    by auto
  from typeof obtain D S where h:"h a = Some(D,S)" 
    and subo:"Subobjs P D (Cs@[C]@Cs')"
    by (auto dest:typeof_Class_Subo split:if_split_asm)
  from subo have "Subobjs P D (Cs@[C])" by(fastforce intro:appendSubobj)
  with h have "P,E,h  ref (a,Cs@[C]) : Class C" by auto
  with T show ?case by (fastforce intro:wt_same_type_typeconf)
next
  case (RedStaticCastFail C Cs E a h l)
  have sconf:"P,E  (h, l) " by fact
  from wf have "is_class P ClassCast" 
    by (fastforce intro:is_class_xcpt wf_prog_wwf_prog)
  hence "preallocated h  P  typeof⇘h(Ref (addr_of_sys_xcpt ClassCast,[ClassCast])) = Some(Class ClassCast)"
    by (auto elim: preallocatedE dest!:preallocatedD Subobjs_Base)
  with sconf have "P,E,h  THROW ClassCast : T" by(auto simp:sconf_def hconf_def)
  thus ?case by (fastforce intro:wt_same_type_typeconf)
next
  case (DynCastRed E e h l e' h' l' C)
  have wt:"P,E,h  Cast C e : T"
    and IH:"T'. P,E  (h,l) ; P,E,h  e : T' 
             P,E,h'  e' :NT T'"
    and sconf:"P,E  (h,l) " by fact+
  from wt obtain T' where wte:"P,E,h  e : T'" and isref:"is_refT T'" 
    and "class": "is_class P C" and T:"T = Class C"
    by auto
  from isref have "P,E,h'  Cast C e' : Class C"
  proof(rule refTE)
    assume "T' = NT"
    with IH[OF sconf wte] isref "class" show ?thesis by auto
  next
    fix D assume "T' = Class D"
    with IH[OF sconf wte] isref "class" show ?thesis by auto
  qed
  with T show ?case by (fastforce intro:wt_same_type_typeconf)
next
  case RedDynCastNull
  thus ?case by (auto elim:WTrt.cases)
next
  case (RedDynCast h l a D S C Cs' E Cs)
  have wt:"P,E,h  Cast C (ref (a,Cs)) : T"
    and path_via:"P  Path D to C via Cs'"
    and hp:"hp (h,l) a = Some(D,S)" by fact+
  from wt have typeof:"P  typeof⇘h(Ref(a,Cs)) = Some(Class(last Cs))"
    and "class": "is_class P C" and T:"T = Class C"
    by auto
  from typeof hp have subo:"Subobjs P D Cs"
    by (auto dest:typeof_Class_Subo split:if_split_asm)
  from path_via subo have "Subobjs P D Cs'" 
    and last:"last Cs' = C" by (auto simp:path_via_def)
  with hp have "P,E,h  ref (a,Cs') : Class C" by auto
  with T show ?case by (fastforce intro:wt_same_type_typeconf)
next
  case (RedStaticUpDynCast Cs C Cs' Ds E a h l)
  have wt:"P,E,h  Cast C (ref (a,Cs)) : T"
    and path_via:"P  Path last Cs to C via Cs'"
    and Ds:"Ds = Cs @p Cs'" by fact+
  from wt have typeof:"P  typeof⇘h(Ref(a,Cs)) = Some(Class(last Cs))"
    and "class": "is_class P C" and T:"T = Class C"
    by auto
  from typeof obtain D S where h:"h a = Some(D,S)" and subo:"Subobjs P D Cs"
    by (auto dest:typeof_Class_Subo split:if_split_asm)
  from path_via subo wf Ds have "Subobjs P D Ds" and last:"last Ds = C"
    by(auto intro!:Subobjs_appendPath appendPath_last[THEN sym] Subobjs_nonempty
            simp:path_via_def)
  with h have "P,E,h  ref (a,Ds) : Class C" by auto
  with T show ?case by (fastforce intro:wt_same_type_typeconf)
next
  case (RedStaticDownDynCast E C a Cs Cs' h l)
  have "P,E,h  Cast C (ref (a,Cs@[C]@Cs')) : T" by fact
  hence typeof:"P  typeof⇘h(Ref(a,Cs@[C]@Cs')) = Some(Class(last(Cs@[C]@Cs')))"
    and "class": "is_class P C" and T:"T = Class C"
    by auto
  from typeof obtain D S where h:"h a = Some(D,S)" 
    and subo:"Subobjs P D (Cs@[C]@Cs')"
    by (auto dest:typeof_Class_Subo split:if_split_asm)
  from subo have "Subobjs P D (Cs@[C])" by(fastforce intro:appendSubobj)
  with h have "P,E,h  ref (a,Cs@[C]) : Class C" by auto
  with T show ?case by (fastforce intro:wt_same_type_typeconf)
next
  case RedDynCastFail thus ?case by fastforce
next
  case (BinOpRed1 E e h l e' h' l' bop e2)
  have red:"P,E  e,(h, l)  e',(h', l')"
    and wt:"P,E,h  e «bop» e2 : T"
    and IH:"T'. P,E  (h,l) ; P,E,h  e : T' 
             P,E,h'  e' :NT T'"
    and sconf:"P,E  (h,l) " by fact+
  from wt obtain T1 T2 where wte:"P,E,h  e : T1" and wte2:"P,E,h  e2 : T2"
    and binop:"case bop of Eq  T = Boolean
                        | Add  T1 = Integer  T2 = Integer  T = Integer"
    by auto
  from WTrt_hext_mono[OF wte2 red_hext_incr[OF red]] have wte2':"P,E,h'  e2 : T2" .
  have "P,E,h'  e' «bop» e2 : T"
  proof (cases bop)
    assume Eq:"bop = Eq"
    from IH[OF sconf wte] obtain T' where "P,E,h'  e' : T'"
      by (cases "T1") auto
    with wte2' binop Eq show ?thesis by(cases bop) auto
  next
    assume Add:"bop = Add"
    with binop have Intg:"T1 = Integer" by simp
    with IH[OF sconf wte] have "P,E,h'  e' : Integer" by simp
    with wte2' binop Add show ?thesis by(cases bop) auto
  qed
  with binop show ?case by(cases bop) simp_all
next
  case (BinOpRed2 E e h l e' h' l' v1 bop)
  have red:"P,E  e,(h,l)  e',(h',l')"
    and wt:"P,E,h  Val v1 «bop» e : T"
    and IH:"T'. P,E  (h,l) ; P,E,h  e : T' 
             P,E,h'  e' :NT T'"
    and sconf:"P,E  (h,l) " by fact+
  from wt obtain T1 T2 where wtval:"P,E,h  Val v1 : T1" and wte:"P,E,h  e : T2"
    and binop:"case bop of Eq  T = Boolean
                        | Add  T1 = Integer  T2 = Integer  T = Integer"
    by auto
  from WTrt_hext_mono[OF wtval red_hext_incr[OF red]]
  have wtval':"P,E,h'  Val v1 : T1" .
  have "P,E,h'  Val v1 «bop» e' : T"
  proof (cases bop)
    assume Eq:"bop = Eq"
    from IH[OF sconf wte] obtain T' where "P,E,h'  e' : T'"
      by (cases "T2") auto
    with wtval' binop Eq show ?thesis by(cases bop) auto
  next
    assume Add:"bop = Add"
    with binop have Intg:"T2 = Integer" by simp
    with IH[OF sconf wte] have "P,E,h'  e' : Integer" by simp
    with wtval' binop Add show ?thesis by(cases bop) auto
  qed
  with binop show ?case by(cases bop) simp_all
next
  case (RedBinOp bop v1 v2 v E a b) thus ?case
  proof (cases bop)
    case Eq thus ?thesis using RedBinOp by auto
  next
    case Add thus ?thesis using RedBinOp by auto
  qed
next
  case (RedVar h l V v E)
  have l:"lcl (h, l) V = Some v" and sconf:"P,E  (h, l) "
    and wt:"P,E,h  Var V : T" by fact+
  hence conf:"P,h  v :≤ T" by(force simp:sconf_def lconf_def)
  show ?case
  proof(cases "C. T  Class C")
    case True 
    with conf have "P  typeof⇘hv = Some T" by(cases T) auto
    hence "P,E,h  Val v : T" by auto
    thus ?thesis by(rule wt_same_type_typeconf)
  next
    case False
    then obtain C where T:"T = Class C" by auto
    with conf have "P  typeof⇘hv = Some(Class C)  P  typeof⇘hv = Some NT"
      by simp
    with T show ?thesis by simp
  qed
next
  case (LAssRed E e h l e' h' l' V)
  have wt:"P,E,h  V:=e : T" and sconf:"P,E  (h, l) "
    and IH:"T'. P,E  (h, l) ; P,E,h  e : T'  P,E,h'  e' :NT T'" by fact+
  from wt obtain T' where wte:"P,E,h  e : T'" and env:"E V = Some T" 
    and sub:"P  T'  T" by auto
  from sconf env have "is_type P T" by(auto simp:sconf_def envconf_def)
  from sub this wf show ?case
  proof(rule subE)
    assume eq:"T' = T" and notclass:"C. T'  Class C"
    with IH[OF sconf wte] have "P,E,h'  e' : T" by(cases T) auto
    with eq env have "P,E,h'  V:=e' : T" by auto
    with eq show ?thesis by(cases T) auto
  next
    fix C D
    assume T':"T' = Class C" and T:"T = Class D" 
      and path_unique:"P  Path C to D unique"
    with IH[OF sconf wte] have "P,E,h'  e' : Class C  P,E,h'  e' : NT"
      by simp
    hence "P,E,h'  V:=e' : T"
    proof(rule disjE)
      assume "P,E,h'  e' : Class C"
      with env T' sub show ?thesis by (fastforce intro:WTrtLAss)
    next
      assume "P,E,h'  e' : NT"
      with env T show ?thesis by (fastforce intro:WTrtLAss)
    qed
    with T show ?thesis by(cases T) auto
  next
    fix C
    assume T':"T' = NT" and T:"T = Class C"
    with IH[OF sconf wte] have "P,E,h'  e' : NT" by simp
    with env T show ?thesis by (fastforce intro:WTrtLAss)
  qed
next
  case (RedLAss E V T v v' h l T')
  have env:"E V = Some T" and casts:"P  T casts v to v'"
    and sconf:"P,E  (h, l) " and wt:"P,E,h  V:=Val v : T'" by fact+
  show ?case
  proof(cases "C. T  Class C")
    case True
    with casts wt env show ?thesis
      by(cases T',auto elim!:casts_to.cases)
  next
    case False
    then obtain C where "T = Class C" by auto
    with casts wt env wf show ?thesis
      by(auto elim!:casts_to.cases,
         auto intro!:sym[OF appendPath_last] Subobjs_nonempty split:if_split_asm 
              simp:path_via_def,drule_tac Cs="Cs" in Subobjs_appendPath,auto)
  qed
next
  case (FAccRed E e h l e' h' l' F Cs)
  have red:"P,E  e,(h,l)  e',(h',l')"
    and wt:"P,E,h  eF{Cs} : T"
    and IH:"T'. P,E  (h,l) ; P,E,h  e : T' 
             P,E,h'  e' :NT T'"
    and sconf:"P,E  (h,l) " by fact+
  from wt have "P,E,h'  e'F{Cs} : T"
  proof(rule WTrt_elim_cases)
    fix C assume wte: "P,E,h  e : Class C"
      and field:"P  C has least F:T via Cs"
      and notemptyCs:"Cs  []"
    from field have "class": "is_class P C"
      by (fastforce intro:Subobjs_isClass simp add:LeastFieldDecl_def FieldDecls_def)
    from IH[OF sconf wte] have "P,E,h'  e' : NT  P,E,h'  e' : Class C" by auto
    thus ?thesis
    proof(rule disjE)
      assume "P,E,h'  e' : NT"
      thus ?thesis by (fastforce intro!:WTrtFAccNT)
    next
      assume wte':"P,E,h'  e' : Class C"
      from wte' notemptyCs field show ?thesis by(rule WTrtFAcc)
    qed
  next
    assume wte: "P,E,h  e : NT"
    from IH[OF sconf wte] have "P,E,h'  e' : NT" by auto
    thus ?thesis by (rule WTrtFAccNT)
  qed
  thus ?case by(rule wt_same_type_typeconf)
next
  case (RedFAcc h l a D S Ds Cs' Cs fs' F v E)
  have h:"hp (h,l) a = Some(D,S)" 
    and Ds:"Ds = Cs'@pCs" and S:"(Ds,fs')  S"
    and fs':"fs' F = Some v" and sconf:"P,E  (h,l) "
    and wte:"P,E,h  ref (a,Cs')F{Cs} : T" by fact+
  from wte have field:"P  last Cs' has least F:T via Cs"
    and notemptyCs:"Cs  []"
    by (auto split:if_split_asm)
  from h S sconf obtain Bs fs ms where classDs:"class P (last Ds) = Some (Bs,fs,ms)"
    and fconf:"P,h  fs' (:≤) map_of fs"
    by (simp add:sconf_def hconf_def oconf_def) blast
  from field Ds have "last Cs = last Ds"
    by (fastforce intro!:appendPath_last Subobjs_nonempty 
                   simp:LeastFieldDecl_def FieldDecls_def)
  with field classDs have map:"map_of fs F =  Some T"
    by (simp add:LeastFieldDecl_def FieldDecls_def)
  with fconf fs' have conf:"P,h  v :≤ T"
    by (simp add:fconf_def,erule_tac x="F" in allE,fastforce)
  thus ?case by (cases T) auto
next
  case (RedFAccNull E F Cs h l)
  have sconf:"P,E  (h, l) " by fact
  from wf have "is_class P NullPointer" 
    by (fastforce intro:is_class_xcpt wf_prog_wwf_prog)
  hence "preallocated h  P  typeof⇘h(Ref (addr_of_sys_xcpt NullPointer,[NullPointer])) = Some(Class NullPointer)"
    by (auto elim: preallocatedE dest!:preallocatedD Subobjs_Base)
  with sconf have "P,E,h  THROW NullPointer : T" by(auto simp:sconf_def hconf_def)
  thus ?case by (fastforce intro:wt_same_type_typeconf wf_prog_wwf_prog)
next
  case (FAssRed1 E e h l e' h' l' F Cs e2)
  have red:"P,E  e,(h,l)  e',(h',l')"
    and wt:"P,E,h  eF{Cs} := e2 : T"
    and IH:"T'. P,E  (h,l) ; P,E,h  e : T' 
             P,E,h'  e' :NT T'"
    and sconf:"P,E  (h,l) " by fact+
  from wt have "P,E,h'  e'F{Cs} := e2 : T"
  proof (rule WTrt_elim_cases)
    fix C T' assume wte: "P,E,h  e : Class C"
      and field:"P  C has least F:T via Cs"
      and notemptyCs:"Cs  []"
      and wte2:"P,E,h  e2 : T'" and sub:"P  T'  T"
    have wte2': "P,E,h'  e2 : T'"
      by(rule WTrt_hext_mono[OF wte2 red_hext_incr[OF red]])
    from IH[OF sconf wte] have "P,E,h'  e' : Class C  P,E,h'  e' : NT"
      by simp
    thus ?thesis
    proof(rule disjE)
      assume wte':"P,E,h'  e' : Class C"
      from wte' notemptyCs field wte2' sub show ?thesis by (rule WTrtFAss)
    next
      assume wte':"P,E,h'  e' : NT"
      from wte' wte2' sub show ?thesis by (rule WTrtFAssNT)
    qed
  next
    fix T' assume wte:"P,E,h  e : NT"
      and wte2:"P,E,h  e2 : T'" and sub:"P  T'  T"
    have wte2': "P,E,h'  e2 : T'"
      by(rule WTrt_hext_mono[OF wte2 red_hext_incr[OF red]])
    from IH[OF sconf wte] have wte':"P,E,h'  e' : NT" by simp
    from wte' wte2' sub show ?thesis by (rule WTrtFAssNT)
  qed
  thus ?case by(rule wt_same_type_typeconf)
next
  case (FAssRed2 E e h l e' h' l' v F Cs)
  have red:"P,E  e,(h,l)  e',(h',l')"
    and wt:"P,E,h  Val vF{Cs} := e : T"
    and IH:"T'. P,E  (h,l) ; P,E,h  e : T' 
             P,E,h'  e' :NT T'"
    and sconf:"P,E  (h,l) " by fact+
  from wt have "P,E,h'  Val vF{Cs}:=e' : T"
  proof (rule WTrt_elim_cases)
    fix C T' assume wtval:"P,E,h  Val v : Class C"
      and field:"P  C has least F:T via Cs"
      and notemptyCs:"Cs  []"
      and wte:"P,E,h  e : T'"
      and sub:"P  T'  T"
    have wtval':"P,E,h'  Val v : Class C"
      by(rule WTrt_hext_mono[OF wtval red_hext_incr[OF red]])
    from field wf have type:"is_type P T" by(rule least_field_is_type)
    from sub type wf show ?thesis
    proof(rule subE)
      assume "T' = T" and notclass:"C. T'  Class C"
      from IH[OF sconf wte] notclass have wte':"P,E,h'  e' : T'" 
        by(cases T') auto
      from wtval' notemptyCs field wte' sub show ?thesis
        by(rule WTrtFAss)
    next
      fix C' D assume T':"T' = Class C'" and T:"T = Class D" 
        and path_unique:"P  Path C' to D unique"
      from IH[OF sconf wte] T' have "P,E,h'  e' : Class C'  P,E,h'  e' : NT"
        by simp
      thus ?thesis
      proof(rule disjE)
        assume wte':"P,E,h'  e' : Class C'"
        from wtval' notemptyCs field wte' sub T' show ?thesis 
          by (fastforce intro: WTrtFAss)
      next
        assume wte':"P,E,h'  e' : NT"
        from wtval' notemptyCs field wte' sub T show ?thesis
          by (fastforce intro: WTrtFAss)
      qed
    next
      fix C' assume T':"T' = NT" and T:"T = Class C'"
      from IH[OF sconf wte] T' have wte':"P,E,h'  e' : NT" by simp
      from wtval' notemptyCs field wte' sub T show ?thesis
        by (fastforce intro: WTrtFAss)
    qed
  next
    fix T' assume wtval:"P,E,h  Val v : NT"
      and wte:"P,E,h  e : T'"
      and sub:"P  T'  T"
    have wtval':"P,E,h'  Val v : NT"
      by(rule WTrt_hext_mono[OF wtval red_hext_incr[OF red]])
    from IH[OF sconf wte] sub obtain T'' where wte':"P,E,h'  e' : T''"
      and sub':"P  T''  T" by (cases T',auto,cases T,auto)
    from wtval' wte' sub' show ?thesis
      by(rule WTrtFAssNT)
  qed
  thus ?case by(rule wt_same_type_typeconf)
next
  case (RedFAss h a D S Cs' F T Cs v v' Ds fs E l T')
  let ?fs' = "fs(F  v')"
  let ?S' = "insert (Ds, ?fs') (S - {(Ds, fs)})"
  let ?h' = "h(a  (D,?S'))"
  have h:"h a = Some(D,S)" and casts:"P  T casts v to v'"
    and field:"P  last Cs' has least F:T via Cs"
    and wt:"P,E,h  ref (a,Cs')F{Cs} := Val v : T'" by fact+
  from wt wf have type:"is_type P T'" 
    by (auto dest:least_field_is_type split:if_split_asm)
  from wt field obtain T'' where wtval:"P,E,h  Val v : T''" and eq:"T = T'" 
    and leq:"P  T''  T'"
    by (auto dest:sees_field_fun split:if_split_asm)
  from casts eq wtval show ?case
  proof(induct rule:casts_to.induct)
    case (casts_prim T0 w)
    have "T0 = T'" and "C. T0  Class C" and wtval':"P,E,h  Val w : T''" by fact+
    with leq have "T' = T''" by(cases T',auto)
    with wtval' have "P,E,h  Val w : T'" by simp
    with h have "P,E,(h(a(D,insert(Ds,fs(F  w))(S-{(Ds,fs)}))))  Val w : T'"
      by(cases w,auto split:if_split_asm)
    thus "P,E,(h(a(D,insert(Ds,fs(F  w))(S-{(Ds,fs)}))))  (Val w) :NT T'"
      by(rule wt_same_type_typeconf)
  next
    case (casts_null C'')
    have T':"Class C'' = T'" by fact
    have "P,E,(h(a(D,insert(Ds,fs(F  Null))(S-{(Ds,fs)}))))  null : NT"
      by simp
    with sym[OF T']
    show "P,E,(h(a(D,insert(Ds,fs(F  Null))(S-{(Ds,fs)}))))  null :NT T'"
      by simp
  next
    case (casts_ref Xs C'' Xs' Ds'' a')
    have "Class C'' = T'" and "Ds'' = Xs @p Xs'"
      and "P  Path last Xs to C'' via Xs'"
      and "P,E,h  ref (a', Xs) : T''" by fact+
    with wf have "P,E,h  ref (a',Ds'') : T'"
      by (auto intro!:appendPath_last[THEN sym] Subobjs_nonempty
        split:if_split_asm simp:path_via_def,
        drule_tac Cs="Xs" in Subobjs_appendPath,auto)
    with h have "P,E,(h(a(D,insert(Ds,fs(F  Ref(a',Ds'')))(S-{(Ds,fs)}))))  
      ref (a',Ds'') : T'"
      by auto
    thus "P,E,(h(a(D,insert(Ds,fs(F  Ref(a',Ds'')))(S-{(Ds,fs)}))))  
      ref (a',Ds'') :NT T'"
      by(rule wt_same_type_typeconf)
  qed
next
  case (RedFAssNull E F Cs v h l)
  have sconf:"P,E  (h, l) " by fact
  from wf have "is_class P NullPointer"
    by (fastforce intro:is_class_xcpt wf_prog_wwf_prog)
  hence "preallocated h  P  typeof⇘h(Ref (addr_of_sys_xcpt NullPointer,[NullPointer])) = Some(Class NullPointer)"
    by (auto elim: preallocatedE dest!:preallocatedD Subobjs_Base)
  with sconf have "P,E,h  THROW NullPointer : T" by(auto simp:sconf_def hconf_def)
  thus ?case by (fastforce intro:wt_same_type_typeconf wf_prog_wwf_prog)
next
  case (CallObj E e h l e' h' l' Copt M es)
  have red: "P,E  e,(h,l)  e',(h',l')"
   and IH: "T'. P,E  (h,l) ; P,E,h  e : T'
                  P,E,h'  e' :NT T'"
   and sconf: "P,E  (h,l) " and wt: "P,E,h  Call e Copt M es : T" by fact+
  from wt have "P,E,h'  Call e' Copt M es : T"
  proof(cases Copt)
    case None
    with wt have "P,E,h  eM(es) : T" by simp
    hence "P,E,h'  e'M(es) : T"
    proof(rule WTrt_elim_cases)
      fix C Cs Ts Ts' m
      assume wte:"P,E,h  e : Class C"
        and "method":"P  C has least M = (Ts, T, m) via Cs"
        and wtes:"P,E,h  es [:] Ts'" and subs: "P  Ts' [≤] Ts"
      from IH[OF sconf wte] have "P,E,h'  e' : NT  P,E,h'  e' : Class C" by auto
      thus ?thesis
      proof(rule disjE)
        assume wte':"P,E,h'  e' : NT"
        have "P,E,h'  es [:] Ts'"
          by(rule WTrts_hext_mono[OF wtes red_hext_incr[OF red]])
        with wte' show ?thesis by(rule WTrtCallNT)
      next
        assume wte':"P,E,h'  e' : Class C"
        have wtes':"P,E,h'  es [:] Ts'"
          by(rule WTrts_hext_mono[OF wtes red_hext_incr[OF red]])
        from wte' "method" wtes' subs show ?thesis by(rule WTrtCall)
      qed
    next
      fix Ts 
      assume wte:"P,E,h  e : NT" and wtes:"P,E,h  es [:] Ts"
      from IH[OF sconf wte] have wte':"P,E,h'  e' : NT" by simp
      have "P,E,h'  es [:] Ts"
        by(rule WTrts_hext_mono[OF wtes red_hext_incr[OF red]])
      with wte' show ?thesis by(rule WTrtCallNT)
    qed
    with None show ?thesis by simp
  next
    case (Some C)
    with wt have "P,E,h  e∙(C::)M(es) : T" by simp
    hence "P,E,h'  e'∙(C::)M(es) : T"
    proof(rule WTrt_elim_cases)
      fix C' Cs Ts Ts' m
      assume wte:"P,E,h  e : Class C'" and path_unique:"P  Path C' to C unique"
        and "method":"P  C has least M = (Ts, T, m) via Cs"
        and wtes:"P,E,h  es [:] Ts'" and subs: "P  Ts' [≤] Ts"
      from IH[OF sconf wte] have "P,E,h'  e' : NT  P,E,h'  e' : Class C'" by auto
      thus ?thesis
      proof(rule disjE)
        assume wte':"P,E,h'  e' : NT"
        have "P,E,h'  es [:] Ts'"
          by(rule WTrts_hext_mono[OF wtes red_hext_incr[OF red]])
        with wte' show ?thesis by(rule WTrtCallNT)
      next
        assume wte':"P,E,h'  e' : Class C'"
        have wtes':"P,E,h'  es [:] Ts'"
          by(rule WTrts_hext_mono[OF wtes red_hext_incr[OF red]])
        from wte' path_unique "method" wtes' subs show ?thesis by(rule WTrtStaticCall)
      qed
    next
      fix Ts 
      assume wte:"P,E,h  e : NT" and wtes:"P,E,h  es [:] Ts"
      from IH[OF sconf wte] have wte':"P,E,h'  e' : NT" by simp
      have "P,E,h'  es [:] Ts"
        by(rule WTrts_hext_mono[OF wtes red_hext_incr[OF red]])
      with wte' show ?thesis by(rule WTrtCallNT)
    qed
    with Some show ?thesis by simp
  qed
  thus ?case by (rule wt_same_type_typeconf)
next
  case (CallParams E es h l es' h' l' v Copt M)
  have reds: "P,E  es,(h,l) [→] es',(h',l')"
   and IH: "Ts. P,E  (h,l) ; P,E,h  es [:] Ts
                  types_conf P E h' es' Ts"
   and sconf: "P,E  (h,l) " and wt: "P,E,h  Call (Val v) Copt M es : T" by fact+
  from wt have "P,E,h'  Call (Val v) Copt M es' : T"
  proof(cases Copt)
    case None
    with wt have "P,E,h  (Val v)M(es) : T" by simp
    hence "P,E,h'  Val vM(es') : T"
    proof (rule WTrt_elim_cases)
      fix C Cs Ts Ts' m
      assume wte: "P,E,h  Val v : Class C"
        and "method":"P  C has least M = (Ts,T,m) via Cs"
        and wtes: "P,E,h  es [:] Ts'" and subs:"P  Ts' [≤] Ts"
      from wtes have "length es = length Ts'" by(rule WTrts_same_length)
      with reds have "length es' = length Ts'"
        by -(drule reds_length,simp)
      with IH[OF sconf wtes] subs obtain Ts'' where wtes':"P,E,h'  es' [:] Ts''"
        and subs':"P  Ts'' [≤] Ts" by(auto dest:types_conf_smaller_types)
      have wte':"P,E,h'  Val v : Class C"
        by(rule WTrt_hext_mono[OF wte reds_hext_incr[OF reds]])
      from wte' "method" wtes' subs' show ?thesis
        by(rule WTrtCall)
    next
      fix Ts
      assume wte:"P,E,h  Val v : NT" 
        and wtes:"P,E,h  es [:] Ts"
      from wtes have "length es = length Ts" by(rule WTrts_same_length)
      with reds have "length es' = length Ts"
        by -(drule reds_length,simp)
      with IH[OF sconf wtes] obtain Ts' where wtes':"P,E,h'  es' [:] Ts'"
        and "P  Ts' [≤] Ts" by(auto dest:types_conf_smaller_types)
      have wte':"P,E,h'  Val v : NT"
        by(rule WTrt_hext_mono[OF wte reds_hext_incr[OF reds]])
      from wte' wtes' show ?thesis by(rule WTrtCallNT)
    qed
    with None show ?thesis by simp
  next
    case (Some C)
    with wt have "P,E,h  (Val v)∙(C::)M(es) : T" by simp
    hence "P,E,h'  (Val v)∙(C::)M(es') : T"
    proof(rule WTrt_elim_cases)
      fix C' Cs Ts Ts' m
      assume wte:"P,E,h  Val v : Class C'" and path_unique:"P  Path C' to C unique"
        and "method":"P  C has least M = (Ts,T,m) via Cs"
        and wtes:"P,E,h  es [:] Ts'" and subs: "P  Ts' [≤] Ts"
      from wtes have "length es = length Ts'" by(rule WTrts_same_length)
      with reds have "length es' = length Ts'"
        by -(drule reds_length,simp)
      with IH[OF sconf wtes] subs obtain Ts'' where wtes':"P,E,h'  es' [:] Ts''"
        and subs':"P  Ts'' [≤] Ts" by(auto dest:types_conf_smaller_types)
      have wte':"P,E,h'  Val v : Class C'"
        by(rule WTrt_hext_mono[OF wte reds_hext_incr[OF reds]])
      from wte' path_unique "method" wtes' subs' show ?thesis
        by(rule WTrtStaticCall)
    next
      fix Ts
      assume wte:"P,E,h  Val v : NT" 
        and wtes:"P,E,h  es [:] Ts"
      from wtes have "length es = length Ts" by(rule WTrts_same_length)
      with reds have "length es' = length Ts"
        by -(drule reds_length,simp)
      with IH[OF sconf wtes] obtain Ts' where wtes':"P,E,h'  es' [:] Ts'"
        and "P  Ts' [≤] Ts" by(auto dest:types_conf_smaller_types)
      have wte':"P,E,h'  Val v : NT"
        by(rule WTrt_hext_mono[OF wte reds_hext_incr[OF reds]])
      from wte' wtes' show ?thesis by(rule WTrtCallNT)
    qed
    with Some show ?thesis by simp
  qed
  thus ?case by (rule wt_same_type_typeconf)
next
  case (RedCall h l a C S Cs M Ts' T' pns' body' Ds Ts T pns body Cs'
                vs bs new_body E T'')
  have hp:"hp (h,l) a = Some(C,S)"
    and "method":"P  last Cs has least M = (Ts',T',pns',body') via Ds"
    and select:"P  (C,Cs@pDs) selects M = (Ts,T,pns,body) via Cs'"
    and length1:"length vs = length pns" and length2:"length Ts = length pns"
    and bs:"bs = blocks(this#pns,Class(last Cs')#Ts,Ref(a,Cs')#vs,body)"
    and body_case:"new_body = (case T' of Class D  Dbs | _  bs)"
    and wt:"P,E,h  ref (a,Cs)M(map Val vs) : T''" by fact+
  from wt hp "method" wf obtain Ts''
    where wtref:"P,E,h  ref (a,Cs) : Class (last Cs)" and eq:"T'' = T'"
    and wtes:"P,E,h  map Val vs [:] Ts''" and subs: "P  Ts'' [≤] Ts'"
    by(auto dest:wf_sees_method_fun split:if_split_asm)
  from select wf have "is_class P (last Cs')"
    by(induct rule:SelectMethodDef.induct,
       auto intro:Subobj_last_isClass simp:FinalOverriderMethodDef_def 
      OverriderMethodDefs_def MinimalMethodDefs_def LeastMethodDef_def MethodDefs_def)
  with select_method_wf_mdecl[OF wf select]
  have length_pns:"length (this#pns) = length (Class(last Cs')#Ts)" 
    and notNT:"T  NT" and type:"Tset (Class(last Cs')#Ts). is_type P T"
    and wtabody:"P,[thisClass(last Cs'),pns[↦]Ts]  body :: T"
    by(auto simp:wf_mdecl_def)
  from wtes hp select
  have map:"map (P  typeof⇘h) (Ref(a,Cs')#vs) = map Some (Class(last Cs')#Ts'')"
    by(auto elim:SelectMethodDef.cases split:if_split_asm 
            simp:FinalOverriderMethodDef_def OverriderMethodDefs_def 
                 MinimalMethodDefs_def LeastMethodDef_def MethodDefs_def)
  from wtref hp have "P  Path C to (last Cs) via Cs"
    by (auto simp:path_via_def split:if_split_asm)
  with select "method" wf have "Ts' = Ts  P  T  T'"
    by -(rule select_least_methods_subtypes,simp_all)
  hence eqs:"Ts' = Ts" and sub:"P  T  T'" by auto
  from wf wtabody have "P,Map.empty(thisClass(last Cs'),pns[↦]Ts),h  body : T"
    by -(rule WT_implies_WTrt,simp_all)
  hence wtbody:"P,E(this#pns [↦] Class (last Cs')#Ts),h  body : T"
    by(rule WTrt_env_mono) simp
  from wtes have "length vs = length Ts''"
    by (fastforce dest:WTrts_same_length)
  with eqs subs
  have length_vs:"length (Ref(a,Cs')#vs) = length (Class(last Cs')#Ts)"
    by (simp add:list_all2_iff)
  from subs eqs have "P  (Class(last Cs')#Ts'') [≤] (Class(last Cs')#Ts)"
    by (simp add:fun_of_def)
  with wt_blocks[OF length_pns length_vs type] wtbody map eq
  have blocks:"P,E,h  blocks(this#pns,Class(last Cs')#Ts,Ref(a,Cs')#vs,body) : T"
    by auto
  have "P,E,h  new_body : T'"
  proof(cases "C. T'  Class C")
    case True
    with sub notNT have "T = T'" by (cases T') auto
    with blocks True body_case bs show ?thesis by(cases T') auto
  next
    case False
    then obtain D where T':"T' = Class D" by auto
    with "method" sub wf have "class": "is_class P D"
      by (auto elim!:widen.cases dest:least_method_is_type 
               intro:Subobj_last_isClass simp:path_unique_def)
    with blocks T' body_case bs "class" sub show ?thesis
      by(cases T',auto,cases T,auto)
  qed
  with eq show ?case by(fastforce intro:wt_same_type_typeconf)
next
  case (RedStaticCall Cs C Cs'' M Ts T pns body Cs' Ds vs E a h l T')
  have "method":"P  C has least M = (Ts, T, pns, body) via Cs'"
    and length1:"length vs = length pns"
    and length2:"length Ts = length pns"
    and path_unique:"P  Path last Cs to C unique"
    and path_via:"P  Path last Cs to C via Cs''"
    and Ds:"Ds = (Cs @p Cs'') @p Cs'"
    and wt:"P,E,h  ref (a,Cs)∙(C::)M(map Val vs) : T'" by fact+
  from wt "method" wf obtain Ts'
    where wtref:"P,E,h  ref (a,Cs) : Class (last Cs)"
    and wtes:"P,E,h  map Val vs [:] Ts'" and subs:"P  Ts' [≤] Ts"
    and TeqT':"T = T'"
    by(auto dest:wf_sees_method_fun split:if_split_asm)
  from wtref obtain D S where hp:"h a = Some(D,S)" and subo:"Subobjs P D Cs"
    by (auto split:if_split_asm)
  from length1 length2
  have length_vs: "length (Ref(a,Ds)#vs) = length (Class (last Ds)#Ts)" by simp
  from length2 have length_pns:"length (this#pns) = length (Class (last Ds)#Ts)"
    by simp
  from "method" have "Cs'  []" 
    by (fastforce intro!:Subobjs_nonempty simp add:LeastMethodDef_def MethodDefs_def)
  with Ds have last:"last Cs' = last Ds"
    by (fastforce dest:appendPath_last)
  with "method" have "is_class P (last Ds)"
    by(auto simp:LeastMethodDef_def MethodDefs_def is_class_def)
  with last has_least_wf_mdecl[OF wf "method"]
  have wtabody: "P,[this#pns [↦] Class (last Ds)#Ts]  body :: T"
    and type:"Tset (Class(last Ds)#Ts). is_type P T"
    by(auto simp:wf_mdecl_def)
  from path_via have suboCs'':"Subobjs P (last Cs) Cs''" 
    and lastCs'':"last Cs'' = C" 
    by (auto simp add:path_via_def)
  with subo wf have subo':"Subobjs P D (Cs@pCs'')"
     by(fastforce intro: Subobjs_appendPath)
   from lastCs'' suboCs'' have lastC:"C = last(Cs@pCs'')"
     by (fastforce dest:Subobjs_nonempty intro:appendPath_last)
  from "method" have "Subobjs P C Cs'"
    by (auto simp:LeastMethodDef_def MethodDefs_def)
  with subo' wf lastC have "Subobjs P D ((Cs @p Cs'') @p Cs')"
    by (fastforce intro:Subobjs_appendPath)
  with Ds have suboDs:"Subobjs P D Ds" by simp
  from wtabody have "P,Map.empty(this#pns [↦] Class (last Ds)#Ts),h  body : T"
    by(rule WT_implies_WTrt)
  hence "P,E(this#pns [↦] Class (last Ds)#Ts),h  body : T"
    by(rule WTrt_env_mono) simp
  hence "P,E,h  blocks(this#pns, Class (last Ds)#Ts, Ref(a,Ds)#vs, body) : T"
    using wtes subs wt_blocks[OF length_pns length_vs type] hp suboDs
    by(auto simp add:rel_list_all2_Cons2)
  with TeqT' show ?case by(fastforce intro:wt_same_type_typeconf)
next
  case (RedCallNull E Copt M vs h l)
  have sconf:"P,E  (h, l) " by fact
  from wf have "is_class P NullPointer" 
    by (fastforce intro:is_class_xcpt wf_prog_wwf_prog)
  hence "preallocated h  P  typeof⇘h(Ref (addr_of_sys_xcpt NullPointer,[NullPointer])) = Some(Class NullPointer)"
    by (auto elim: preallocatedE dest!:preallocatedD Subobjs_Base)
  with sconf have "P,E,h  THROW NullPointer : T" by(auto simp:sconf_def hconf_def)
  thus ?case by (fastforce intro:wt_same_type_typeconf)
next
  case (BlockRedNone E V T e h l e' h' l' T')
  have IH:"T'. P,E(V  T)  (h, l(V := None)) ; P,E(V  T),h  e : T'
                  P,E(V  T),h'  e' :NT T'"
    and sconf:"P,E  (h