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⇘h⇙ v = 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(V↦T),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(V↦T)"
    by (simp add:lconf_def fun_upd_apply)
  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 (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(V↦T),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(V↦T)"
    by (simp add:lconf_def fun_upd_apply)
  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 (InitBlockRed E V T e h l v' e' h' l' v'' v T')
  have red: "P,E(V ↦ T) ⊢ ⟨e, (h, l(V↦v'))⟩ → ⟨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(V↦T),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(V↦T)"
    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⇘h⇙ vs = 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⇘h⇙ vs = 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⇘h⇙ vs = map Some Ts'" and subs:"P ⊢ Ts' [≤] Ts"
      by auto
    from wt obtain T'' where "P ⊢ typeof⇘h⇙ v = 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⇘h⇙ v = 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 ⊢ ⦇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' ⊢ ⦇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 RedStaticCastNull
  thus ?case by (auto elim:WTrt.cases)
next
  case (RedStaticUpCast Cs C Cs' Ds E a h l)
  have wt:"P,E,h ⊢ ⦇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 (RedStaticDownCast E C a Cs Cs' h l)
  have "P,E,h ⊢ ⦇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 (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 e⇩2)
  have red:"P,E ⊢ ⟨e,(h, l)⟩ → ⟨e',(h', l')⟩"
    and wt:"P,E,h ⊢ e «bop» e⇩2 : 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⇩1 T⇩2 where wte:"P,E,h ⊢ e : T⇩1" and wte2:"P,E,h ⊢ e⇩2 : T⇩2"
    and binop:"case bop of Eq ⇒ T = Boolean
                        | Add ⇒ T⇩1 = Integer ∧ T⇩2 = Integer ∧ T = Integer"
    by auto
  from WTrt_hext_mono[OF wte2 red_hext_incr[OF red]] have wte2':"P,E,h' ⊢ e⇩2 : T⇩2" .
  have "P,E,h' ⊢ e' «bop» e⇩2 : T"
  proof (cases bop)
    assume Eq:"bop = Eq"
    from IH[OF sconf wte] obtain T' where "P,E,h' ⊢ e' : T'"
      by (cases "T⇩1") auto
    with wte2' binop Eq show ?thesis by(cases bop) auto
  next
    assume Add:"bop = Add"
    with binop have Intg:"T⇩1 = 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' v⇩1 bop)
  have red:"P,E ⊢ ⟨e,(h,l)⟩ → ⟨e',(h',l')⟩"
    and wt:"P,E,h ⊢ Val v⇩1 «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 T⇩1 T⇩2 where wtval:"P,E,h ⊢ Val v⇩1 : T⇩1" and wte:"P,E,h ⊢ e : T⇩2"
    and binop:"case bop of Eq ⇒ T = Boolean
                        | Add ⇒ T⇩1 = Integer ∧ T⇩2 = Integer ∧ T = Integer"
    by auto
  from WTrt_hext_mono[OF wtval red_hext_incr[OF red]]
  have wtval':"P,E,h' ⊢ Val v⇩1 : T⇩1" .
  have "P,E,h' ⊢ Val v⇩1 «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 "T⇩2") auto
    with wtval' binop Eq show ?thesis by(cases bop) auto
  next
    assume Add:"bop = Add"
    with binop have Intg:"T⇩2 = 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 v⇩1 v⇩2 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⇘h⇙ v = 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⇘h⇙ v = Some(Class C) ∨ P ⊢ typeof⇘h⇙ v = 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 ⊢ e∙F{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 e⇩2)
  have red:"P,E ⊢ ⟨e,(h,l)⟩ → ⟨e',(h',l')⟩"
    and wt:"P,E,h ⊢ e∙F{Cs} := e⇩2 : 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} := e⇩2 : 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 ⊢ e⇩2 : T'" and sub:"P ⊢ T' ≤ T"
    have wte2': "P,E,h' ⊢ e⇩2 : 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 ⊢ e⇩2 : T'" and sub:"P ⊢ T' ≤ T"
    have wte2': "P,E,h' ⊢ e⇩2 : 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 v∙F{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 v∙F{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 T⇩0 w)
    have "T⇩0 = T'" and "∀C. T⇩0 ≠ 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 ⊢ e∙M(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 v∙M(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 ⇒ ⦇D⦈bs | _ ⇒ 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:"∀T∈set (Class(last Cs')#Ts). is_type P T"
    and wtabody:"P,[this↦Class(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(this↦Class(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:"∀T∈set (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, l) √" and wt:"P,E,h ⊢ {V:T; e} : T'" by fact+
  from wt have type:"is_type P T" and wte:"P,E(V↦T),h ⊢ e : T'" by auto
  from sconf type have "P,E(V ↦ T) ⊢ (h, l(V := None)) √"
    by (auto simp:sconf_def lconf_def envconf_def)
  from IH[OF this wte] type show ?case by (cases T') auto
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, l(V := None)) √; P,E(V ↦ T),h ⊢ e : T'⟧
                  ⟹ P,E(V ↦ T),h' ⊢ e' :⇘NT⇙ T'"
    and Some:"l' V = Some v"
    and sconf:"P,E ⊢ (h, l) √" and wt:"P,E,h ⊢ {V:T; e} : T'" by fact+
  from wt have wte:"P,E(V↦T),h ⊢ e : T'"  and type:"is_type P T" by auto
  with sconf wf red type have "P,h' ⊢ l' (:≤)⇩w E(V ↦ T)"
    by -(auto simp:sconf_def,rule red_preserves_lconf,
         auto intro:wf_prog_wwf_prog simp:envconf_def lconf_def)
  hence conf:"P,h' ⊢ v :≤ T" using Some 
    by(auto simp:lconf_def,erule_tac x="V" in allE,clarsimp)
  have wtval:"P,E(V ↦ T),h' ⊢ V:=Val v : T"
  proof(cases T)
    case Void with conf show ?thesis by auto
  next
    case Boolean with conf show ?thesis by auto
  next
    case Integer with conf show ?thesis by auto
  next
    case NT with conf show ?thesis by auto
  next
    case (Class C)
    with conf have "P,E(V ↦ T),h' ⊢ Val v : T ∨ P,E(V ↦ T),h' ⊢ Val v : NT"
      by auto
    with Class show ?thesis by auto
  qed
  from sconf type have "P,E(V ↦ T) ⊢ (h, l(V := None)) √"
    by (auto simp:sconf_def lconf_def envconf_def)
  from IH[OF this wte] wtval type show ?case by(cases T') auto
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(V ↦ v'))⟩ → ⟨e',(h', l')⟩"
    and IH:"⋀T'. ⟦P,E(V ↦ T) ⊢ (h, l(V ↦ v')) √; P,E(V ↦ T),h ⊢ e : T'⟧
              ⟹ P,E(V ↦ T),h' ⊢ e' :⇘NT⇙ T'"
    and Some:"l' V = Some v''" and casts:"P ⊢ T casts v to v'"
    and sconf:"P,E ⊢ (h, l) √" and wt:"P,E,h ⊢ {V:T := Val v; e} : T'" by fact+
  from wt have wte:"P,E(V ↦ T),h ⊢ e : T'" and wtval:"P,E(V ↦ T),h ⊢ V:=Val v : T"
    and type:"is_type P T"
    by auto
  from wf casts wtval have "P,h ⊢ v' :≤ T"
    by(fastforce intro!:casts_conf wf_prog_wwf_prog)
  with sconf have lconf:"P,h ⊢ l(V ↦ v') (:≤)⇩w E(V ↦ T)"
    by (fastforce intro!:lconf_upd2 simp:sconf_def)
  from sconf type have "envconf P (E(V ↦ T))" by(simp add:sconf_def envconf_def)
  from red_preserves_lconf[OF wf_prog_wwf_prog[OF wf] red wte lconf this]
  have "P,h' ⊢ l' (:≤)⇩w E(V ↦ T)" .
  with Some have "P,h' ⊢ v'' :≤ T"
    by(simp add:lconf_def,erule_tac x="V" in allE,auto)
  hence wtval':"P,E(V ↦ T),h' ⊢ V:=Val v'' : T"
    by(cases T) auto
  from lconf sconf type have "P,E(V ↦ T) ⊢ (h, l(V ↦ v')) √"
    by(auto simp:sconf_def envconf_def)
  from IH[OF this wte] wtval' type show ?case by(cases T') auto
next
  case RedBlock thus ?case by (fastforce intro:wt_same_type_typeconf)
next
  case RedInitBlock thus ?case by (fastforce intro:wt_same_type_typeconf)
next
  case (SeqRed E e h l e' h' l' e⇩2 T)
  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 ⊢ e;; e⇩2 : T" by fact+
  from wt obtain T' where wte:"P,E,h ⊢ e : T'" and wte2:"P,E,h ⊢ e⇩2 : T" by auto
  from WTrt_hext_mono[OF wte2 red_hext_incr[OF red]] have wte2':"P,E,h' ⊢ e⇩2 : T" .
  from IH[OF sconf wte] obtain T'' where "P,E,h' ⊢ e' : T''" by(cases T') auto
  with wte2' have "P,E,h' ⊢ e';; e⇩2 : T" by auto
  thus ?case by(rule wt_same_type_typeconf)
next
  case RedSeq thus ?case by (fastforce intro:wt_same_type_typeconf)
next
  case (CondRed E e h l e' h' l' e⇩1 e⇩2)
  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 wt:"P,E,h ⊢ if (e) e⇩1 else e⇩2 : T"
    and sconf:"P,E ⊢ (h,l) √" by fact+
  from wt have wte:"P,E,h ⊢ e : Boolean"
      and wte1:"P,E,h ⊢ e⇩1 : T" and wte2:"P,E,h ⊢ e⇩2 : T" by auto
  from IH[OF sconf wte] have wte':"P,E,h' ⊢ e' : Boolean" by auto
  from wte' WTrt_hext_mono[OF wte1 red_hext_incr[OF red]]
    WTrt_hext_mono[OF wte2 red_hext_incr[OF red]]
  have "P,E,h' ⊢ if (e') e⇩1 else e⇩2 : T"
    by (rule WTrtCond)
  thus ?case by(rule wt_same_type_typeconf)
next
  case RedCondT thus ?case by (fastforce intro: wt_same_type_typeconf)
next
  case RedCondF thus ?case by (fastforce intro: wt_same_type_typeconf)
next
  case RedWhile thus ?case by (fastforce intro: wt_same_type_typeconf)
next
  case (ThrowRed E e h l e' h' l' T)
  have 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 ⊢ throw e : T" by fact+
  from wt obtain T' where wte:"P,E,h ⊢ e : T'" and ref:"is_refT T'"
    by auto
  from ref have "P,E,h' ⊢ throw e' : T"
  proof(rule refTE)
    assume T':"T' = NT"
    with wte have "P,E,h ⊢ e : NT" by simp
    from IH[OF sconf this] ref T' show ?thesis by auto
    
  next
    fix C assume T':"T' = Class C"
    with wte have "P,E,h ⊢ e : Class C" by simp
    from IH[OF sconf this] 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"
      have "is_refT (Class C)" by simp
      with wte' show ?thesis by auto
    next
      assume wte':"P,E,h' ⊢ e' : NT"
      have "is_refT NT" by simp
      with wte' show ?thesis by auto
    qed
  qed
  thus ?case by (rule wt_same_type_typeconf)
next
  case (RedThrowNull E 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 (ListRed1 E e h l e' h' l' es Ts)
  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 ⊢ e # es [:] Ts" by fact+
  from wt obtain U Us where Ts:"Ts = U#Us" by(cases Ts) auto
  with wt have wte:"P,E,h ⊢ e : U" and wtes:"P,E,h ⊢ es [:] Us" by simp_all
  from WTrts_hext_mono[OF wtes red_hext_incr[OF red]] 
  have wtes':"P,E,h' ⊢ es [:] Us" .
  hence "length es = length Us" by (rule WTrts_same_length)
  with wtes' have "types_conf P E h' es Us"
    by (fastforce intro:wts_same_types_typesconf)
  with IH[OF sconf wte] Ts show ?case by simp
next
  case (ListRed2 E es h l es' h' l' v Ts)
  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 ⊢ Val v#es [:] Ts" by fact+
  from wt obtain U Us where Ts:"Ts = U#Us" by(cases Ts) auto
  with wt have wtval:"P,E,h ⊢ Val v : U" and wtes:"P,E,h ⊢ es [:] Us" by simp_all
  from WTrt_hext_mono[OF wtval reds_hext_incr[OF reds]]
  have "P,E,h' ⊢ Val v : U" .
  hence "P,E,h' ⊢ (Val v) :⇘NT⇙ U" by(rule wt_same_type_typeconf)
  with IH[OF sconf wtes] Ts show ?case by simp
next
  case (CallThrowObj E h l Copt M es h' l')
  thus ?case by(cases Copt)(auto intro:wt_same_type_typeconf)
next
  case (CallThrowParams es vs h l es' E v Copt M h' l')
  thus ?case by(cases Copt)(auto intro:wt_same_type_typeconf)
qed (fastforce intro:wt_same_type_typeconf)+



corollary subject_reduction:
  "⟦ wf_C_prog P; P,E ⊢ ⟨e,s⟩ → ⟨e',s'⟩; P,E ⊢ s √; P,E,hp s ⊢ e:T ⟧
  ⟹ P,E,(hp s') ⊢ e' :⇘NT⇙ T"
by(cases s, cases s', fastforce dest:subject_reduction2)

corollary subjects_reduction:
  "⟦ wf_C_prog P; P,E ⊢ ⟨es,s⟩ [→] ⟨es',s'⟩; P,E ⊢ s √; P,E,hp s ⊢ es[:]Ts ⟧
  ⟹ types_conf P E (hp s') es' Ts"
by(cases s, cases s', fastforce dest:subjects_reduction2)


subsection ‹Lifting to ‹→*››

text‹Now all these preservation lemmas are first lifted to the transitive
closure \dots›

lemma step_preserves_sconf:
assumes wf: "wf_C_prog P" and step: "P,E ⊢ ⟨e,s⟩ →* ⟨e',s'⟩"
shows "⋀T. ⟦ P,E,hp s ⊢ e : T; P,E ⊢ s √ ⟧ ⟹ P,E ⊢ s' √"

using step
proof (induct rule:converse_rtrancl_induct2)
  case refl show ?case by fact 
next
  case step
  thus ?case using wf
    apply simp
    apply (frule subject_reduction[OF wf])
      apply (rule step.prems)
      apply (rule step.prems)
      apply (cases T)
      apply (auto dest:red_preserves_sconf intro:wf_prog_wwf_prog)
      done
qed

lemma steps_preserves_sconf:
assumes wf: "wf_C_prog P" and step: "P,E ⊢ ⟨es,s⟩ [→]* ⟨es',s'⟩"
shows "⋀Ts. ⟦ P,E,hp s ⊢ es [:] Ts; P,E ⊢ s √ ⟧ ⟹ P,E ⊢ s' √"

using step
proof (induct rule:converse_rtrancl_induct2)
  case refl show ?case by fact
next
  case (step es s es'' s'' Ts)
  have Reds:"((es, s), es'', s'') ∈ Reds P E"
    and reds:"P,E ⊢ ⟨es'',s''⟩ [→]* ⟨es',s'⟩"
    and wtes:"P,E,hp s ⊢ es [:] Ts"
    and sconf:"P,E ⊢ s √"
    and IH:"⋀Ts. ⟦P,E,hp s'' ⊢ es'' [:] Ts; P,E ⊢ s'' √⟧ ⟹ P,E ⊢ s' √" by fact+
  from Reds have reds1:"P,E ⊢ ⟨es,s⟩ [→] ⟨es'',s''⟩" by simp
  from subjects_reduction[OF wf this sconf wtes] 
  have type:"types_conf P E (hp s'') es'' Ts" .
  from reds1 wtes sconf wf have sconf':"P,E ⊢ s'' √" 
    by(fastforce intro:wf_prog_wwf_prog reds_preserves_sconf)
  from type have "∃Ts'. P,E,hp s'' ⊢ es'' [:] Ts'"
  proof (induct Ts arbitrary: es'')
    fix esi
    assume "types_conf P E (hp s'') esi []"
    thus "∃Ts'. P,E,hp s'' ⊢ esi [:] Ts'"
    proof(induct esi)
      case Nil thus "∃Ts'. P,E,hp s'' ⊢ [] [:] Ts'" by simp
    next
      fix ex esx
      assume "types_conf P E (hp s'') (ex#esx) []"
      thus "∃Ts'. P,E,hp s'' ⊢ ex#esx [:] Ts'" by simp
    qed
  next
    fix T' Ts' esi
    assume type':"types_conf P E (hp s'') esi (T'#Ts')"
      and IH:"⋀es''. types_conf P E (hp s'') es'' Ts' ⟹
                      ∃Ts''. P,E,hp s'' ⊢ es'' [:] Ts''"
    from type' show "∃Ts'. P,E,hp s'' ⊢ esi [:] Ts'"
    proof(induct esi)
      case Nil thus "∃Ts'. P,E,hp s'' ⊢ [] [:] Ts'" by simp
    next
      fix ex esx
      assume "types_conf P E (hp s'') (ex#esx) (T'#Ts')"
      hence type':"P,E,hp s'' ⊢ ex :⇘NT⇙ T'" 
        and types':"types_conf P E (hp s'') esx Ts'" by simp_all
      from type' obtain Tx where type'':"P,E,hp s'' ⊢ ex : Tx"
        by(cases T') auto
      from IH[OF types'] obtain Tsx where "P,E,hp s'' ⊢ esx [:] Tsx" by auto
      with type'' show "∃Ts'. P,E,hp s'' ⊢ ex#esx [:] Ts'" by auto
    qed
  qed
  then obtain Ts' where "P,E,hp s'' ⊢ es'' [:] Ts'" by blast
  from IH[OF this sconf'] show ?case .
qed


lemma step_preserves_defass:
assumes wf: "wf_C_prog P" and step: "P,E ⊢ ⟨e,s⟩ →* ⟨e',s'⟩"
shows "𝒟 e ⌊dom(lcl s)⌋ ⟹ 𝒟 e' ⌊dom(lcl s')⌋"

using step
proof (induct rule:converse_rtrancl_induct2)
  case refl thus ?case .
next
  case (step e s e' s') thus ?case
    by(cases s,cases s')(auto dest:red_preserves_defass[OF wf])
qed



lemma step_preserves_type:
assumes wf: "wf_C_prog P" and step: "P,E ⊢ ⟨e,s⟩ →* ⟨e',s'⟩"
shows "⋀T. ⟦ P,E ⊢ s √; P,E,hp s ⊢ e:T ⟧
    ⟹ P,E,(hp s') ⊢ e' :⇘NT⇙ T"

using step
proof (induct rule:converse_rtrancl_induct2)
  case refl thus ?case by -(rule wt_same_type_typeconf)
next
  case (step e s e'' s'' T) thus ?case using wf
    apply simp
    apply (frule subject_reduction[OF wf])
    apply (auto dest!:red_preserves_sconf intro:wf_prog_wwf_prog)
    apply(cases T)
    apply fastforce+
    done
qed


text‹predicate to show the same lemma for lists›

fun
  conformable :: "ty list ⇒ ty list ⇒ bool"
where
  "conformable [] [] ⟷ True"
  | "conformable (T''#Ts'') (T'#Ts') ⟷ (T'' = T'
     ∨ (∃C. T'' = NT ∧ T' = Class C)) ∧ conformable Ts'' Ts'"
  | "conformable _ _ ⟷ False"

lemma types_conf_conf_types_conf:
  "⟦types_conf P E h es Ts; conformable Ts Ts'⟧ ⟹ types_conf P E h es Ts'"
proof (induct Ts arbitrary: Ts' es)
  case Nil thus ?case by (cases Ts') (auto split: if_split_asm)
next
  case (Cons T'' Ts'')
  have type:"types_conf P E h es (T''#Ts'')"
    and conf:"conformable (T''#Ts'') Ts'"
    and IH:"⋀Ts' es. ⟦types_conf P E h es Ts''; conformable Ts'' Ts'⟧
                   ⟹ types_conf P E h es Ts'" by fact+
  from type obtain e' es' where es:"es = e'#es'" by (cases es) auto
  with type have type':"P,E,h ⊢ e' :⇘NT⇙ T''"
    and types': "types_conf P E h es' Ts''"
    by simp_all
  from conf obtain U Us where Ts': "Ts' = U#Us" by (cases Ts') auto
  with conf have disj:"T'' = U ∨ (∃C. T'' = NT ∧ U = Class C)"
    and conf':"conformable Ts'' Us"
    by simp_all
  from type' disj have "P,E,h ⊢ e' :⇘NT⇙ U" by auto
  with IH[OF types' conf'] Ts' es show ?case by simp
qed


lemma types_conf_Wtrt_conf:
  "types_conf P E h es Ts ⟹ ∃Ts'. P,E,h ⊢ es [:] Ts' ∧ conformable Ts' Ts"
proof (induct Ts arbitrary: es)
  case Nil thus ?case by (cases es) (auto split:if_split_asm)
next
  case (Cons T'' Ts'')
  have type:"types_conf P E h es (T''#Ts'')"
    and IH:"⋀es. types_conf P E h es Ts'' ⟹
                  ∃Ts'. P,E,h ⊢ es [:] Ts' ∧ conformable Ts' Ts''" by fact+
  from type obtain e' es' where es:"es = e'#es'" by (cases es) auto
  with type have type':"P,E,h ⊢ e' :⇘NT⇙ T''"
    and types': "types_conf P E h es' Ts''"
    by simp_all
  from type' obtain T' where "P,E,h ⊢ e' : T'" and 
    "T' = T'' ∨ (∃C. T' = NT ∧ T'' = Class C)" by(cases T'') auto
  with IH[OF types'] es show ?case 
    by(auto,rule_tac x="T''#Ts'" in exI,simp,rule_tac x="NT#Ts'" in exI,simp)
qed



lemma steps_preserves_types:
assumes wf: "wf_C_prog P" and steps: "P,E ⊢ ⟨es,s⟩ [→]* ⟨es',s'⟩"
shows "⋀Ts. ⟦ P,E ⊢ s √; P,E,hp s ⊢ es [:] Ts⟧
  ⟹ types_conf P E (hp s') es' Ts"
  
using steps
proof (induct rule:converse_rtrancl_induct2)
  case refl thus ?case by -(rule wts_same_types_typesconf)
next
  case (step es s es'' s'' Ts)
  have Reds:"((es, s), es'', s'') ∈ Reds P E"
    and steps:"P,E ⊢ ⟨es'',s''⟩ [→]* ⟨es',s'⟩"
    and sconf:"P,E ⊢ s √" and wtes:"P,E,hp s ⊢ es [:] Ts"
    and IH:"⋀Ts. ⟦P,E ⊢ s'' √; P,E,hp s'' ⊢ es'' [:] Ts ⟧ 
               ⟹ types_conf P E (hp s') es' Ts" by fact+
  from Reds have step:"P,E ⊢ ⟨es,s⟩ [→] ⟨es'',s''⟩" by simp
  with wtes sconf wf have sconf':"P,E ⊢ s'' √"
    by(auto intro:reds_preserves_sconf wf_prog_wwf_prog)
  from wtes have "length es = length Ts" by(fastforce dest:WTrts_same_length)
  from step sconf wtes
  have type': "types_conf P E (hp s'') es'' Ts"
    by (rule subjects_reduction[OF wf])
  then obtain Ts' where wtes'':"P,E,hp s'' ⊢ es'' [:] Ts'" 
    and conf:"conformable Ts' Ts" by (auto dest:types_conf_Wtrt_conf)
  from IH[OF sconf' wtes''] have "types_conf P E (hp s') es' Ts'" .
  with conf show ?case by(fastforce intro:types_conf_conf_types_conf)
qed
  

subsection ‹Lifting to ‹⇒››

text‹\dots and now to the big step semantics, just for fun.›

lemma eval_preserves_sconf:
  "⟦ wf_C_prog P; P,E ⊢ ⟨e,s⟩ ⇒ ⟨e',s'⟩; P,E ⊢ e::T; P,E ⊢ s √ ⟧ ⟹ P,E ⊢ s' √"

by(blast intro:step_preserves_sconf big_by_small WT_implies_WTrt wf_prog_wwf_prog)

lemma evals_preserves_sconf:
  "⟦ wf_C_prog P; P,E ⊢ ⟨es,s⟩ [⇒] ⟨es',s'⟩; P,E ⊢ es [::] Ts; P,E ⊢ s √ ⟧ 
  ⟹ P,E ⊢ s' √"
  by(blast intro:steps_preserves_sconf bigs_by_smalls WTs_implies_WTrts 
                 wf_prog_wwf_prog)



lemma eval_preserves_type: assumes wf: "wf_C_prog P"
shows "⟦ P,E ⊢ ⟨e,s⟩ ⇒ ⟨e',s'⟩; P,E ⊢ s √; P,E ⊢ e::T ⟧
   ⟹ P,E,(hp s') ⊢ e' :⇘NT⇙ T"

  using wf
  by (auto dest!:big_by_small[OF wf_prog_wwf_prog[OF wf]] WT_implies_WTrt 
           intro:wf_prog_wwf_prog
           dest!:step_preserves_type[OF wf])


lemma evals_preserves_types: assumes wf: "wf_C_prog P"
shows "⟦ P,E ⊢ ⟨es,s⟩ [⇒] ⟨es',s'⟩; P,E ⊢ s √; P,E ⊢ es [::] Ts ⟧
  ⟹ types_conf P E (hp s') es' Ts"
using wf
  by (auto dest!:bigs_by_smalls[OF wf_prog_wwf_prog[OF wf]] WTs_implies_WTrts
           intro:wf_prog_wwf_prog
           dest!:steps_preserves_types[OF wf])


subsection ‹The final polish›

text‹The above preservation lemmas are now combined and packed nicely.›

definition wf_config :: "prog ⇒ env ⇒ state ⇒ expr ⇒ ty ⇒ bool" ("_,_,_ ⊢ _ : _ √"   [51,0,0,0,0]50) where
  "P,E,s ⊢ e:T √  ≡  P,E ⊢ s √ ∧ P,E,hp s ⊢ e : T"

theorem Subject_reduction: assumes wf: "wf_C_prog P"
shows "P,E ⊢ ⟨e,s⟩ → ⟨e',s'⟩ ⟹ P,E,s ⊢ e : T √
       ⟹ P,E,(hp s') ⊢ e' :⇘NT⇙ T"

  using wf
  by (force elim!:red_preserves_sconf intro:wf_prog_wwf_prog 
            dest:subject_reduction[OF wf] simp:wf_config_def)



theorem Subject_reductions:
assumes wf: "wf_C_prog P" and reds: "P,E ⊢ ⟨e,s⟩ →* ⟨e',s'⟩"
shows "⋀T. P,E,s ⊢ e : T √ ⟹ P,E,(hp s') ⊢ e' :⇘NT⇙ T"

using reds
proof (induct rule:converse_rtrancl_induct2)
  case refl thus ?case
    by (fastforce intro:wt_same_type_typeconf simp:wf_config_def)
next
  case (step e s e'' s'' T)
  have Red:"((e, s), e'', s'') ∈ Red P E"
    and IH:"⋀T. P,E,s'' ⊢ e'' : T √ ⟹ P,E,(hp s') ⊢ e' :⇘NT⇙ T"
    and wte:"P,E,s ⊢ e : T √" by fact+
  from Red have red:"P,E ⊢ ⟨e,s⟩ → ⟨e'',s''⟩" by simp
  from red_preserves_sconf[OF red] wte wf have sconf:"P,E ⊢ s'' √"
    by(fastforce dest:wf_prog_wwf_prog simp:wf_config_def)
  from wf red wte have type_conf:"P,E,(hp s'') ⊢ e'' :⇘NT⇙ T"
    by(rule Subject_reduction)
  show ?case
  proof(cases T)
    case Void
    with type_conf have "P,E,hp s'' ⊢ e'' : T" by simp
    with sconf have "P,E,s'' ⊢ e'' : T √" by(simp add:wf_config_def)
    from IH[OF this] show ?thesis .
  next
    case Boolean
    with type_conf have "P,E,hp s'' ⊢ e'' : T" by simp
    with sconf have "P,E,s'' ⊢ e'' : T √" by(simp add:wf_config_def)
    from IH[OF this] show ?thesis .
  next
    case Integer
    with type_conf have "P,E,hp s'' ⊢ e'' : T" by simp
    with sconf have "P,E,s'' ⊢ e'' : T √" by(simp add:wf_config_def)
    from IH[OF this] show ?thesis .
  next
    case NT
    with type_conf have "P,E,hp s'' ⊢ e'' : T" by simp
    with sconf have "P,E,s'' ⊢ e'' : T √" by(simp add:wf_config_def)
    from IH[OF this] show ?thesis .
  next
    case (Class C)
    with type_conf have "P,E,hp s'' ⊢ e'' : T ∨ P,E,hp s'' ⊢ e'' : NT" by simp
    thus ?thesis
    proof(rule disjE)
      assume "P,E,hp s'' ⊢ e'' : T"
      with sconf have "P,E,s'' ⊢ e'' : T √" by(simp add:wf_config_def)
      from IH[OF this] show ?thesis .
    next
      assume "P,E,hp s'' ⊢ e'' : NT"
      with sconf have "P,E,s'' ⊢ e'' : NT √" by(simp add:wf_config_def)
      from IH[OF this] have "P,E,hp s' ⊢ e' : NT" by simp
      with Class show ?thesis by simp
    qed
  qed
qed



corollary Progress: assumes wf: "wf_C_prog P"
shows "⟦ P,E,s  ⊢ e : T √; 𝒟 e ⌊dom(lcl s)⌋; ¬ final e ⟧ ⟹ ∃e' s'. P,E ⊢ ⟨e,s⟩ → ⟨e',s'⟩"

using progress[OF wf_prog_wwf_prog[OF wf]]
by(auto simp:wf_config_def sconf_def)


corollary TypeSafety:
fixes s s' :: state
assumes wf:"wf_C_prog P" and sconf:"P,E ⊢ s √" and wte:"P,E ⊢ e :: T"
  and D:"𝒟 e ⌊dom(lcl s)⌋" and step:"P,E ⊢ ⟨e,s⟩ →* ⟨e',s'⟩"
  and nored:"¬(∃e'' s''. P,E ⊢ ⟨e',s'⟩ → ⟨e'',s''⟩)"
shows "(∃v. e' = Val v ∧ P,hp s' ⊢ v :≤ T) ∨
      (∃r. e' = Throw r ∧ the_addr (Ref r) ∈ dom(hp s'))"
proof -
  from sconf wte wf have wf_config:"P,E,s ⊢ e : T √"
    by(fastforce intro:WT_implies_WTrt simp:wf_config_def)
  with wf step have type_conf:"P,E,(hp s') ⊢ e' :⇘NT⇙ T"
    by(rule Subject_reductions)
  from step_preserves_sconf[OF wf step wte[THEN WT_implies_WTrt] sconf] wf
  have sconf':"P,E ⊢ s' √" by simp
  from wf step D have D':"𝒟 e' ⌊dom(lcl s')⌋" by(rule step_preserves_defass)
  show ?thesis
  proof(cases T)
    case Void 
    with type_conf have wte':"P,E,hp s' ⊢ e' : T" by simp
    with sconf' have wf_config':"P,E,s' ⊢ e' : T √" by(simp add:wf_config_def)
    { assume "¬ final e'"
      from Progress[OF wf wf_config' D' this] nored have False
        by simp }
    hence "final e'" by fast
    with wte' show ?thesis by(auto simp:final_def)
  next
    case Boolean
    with type_conf have wte':"P,E,hp s' ⊢ e' : T" by simp
    with sconf' have wf_config':"P,E,s' ⊢ e' : T √" by(simp add:wf_config_def)
    { assume "¬ final e'"
      from Progress[OF wf wf_config' D' this] nored have False
        by simp }
    hence "final e'" by fast
    with wte' show ?thesis by(auto simp:final_def)
  next
    case Integer
    with type_conf have wte':"P,E,hp s' ⊢ e' : T" by simp
    with sconf' have wf_config':"P,E,s' ⊢ e' : T √" by(simp add:wf_config_def)
    { assume "¬ final e'"
      from Progress[OF wf wf_config' D' this] nored have False
        by simp }
    hence "final e'" by fast
    with wte' show ?thesis by(auto simp:final_def)
  next
    case NT
    with type_conf have wte':"P,E,hp s' ⊢ e' : T" by simp
    with sconf' have wf_config':"P,E,s' ⊢ e' : T √" by(simp add:wf_config_def)
    { assume "¬ final e'"
      from Progress[OF wf wf_config' D' this] nored have False
        by simp }
    hence "final e'" by fast
    with wte' show ?thesis by(auto simp:final_def)
  next
    case (Class C)
    with type_conf have wte':"P,E,hp s' ⊢ e' : T ∨ P,E,hp s' ⊢ e' : NT" by simp
    thus ?thesis
    proof(rule disjE)
      assume wte':"P,E,hp s' ⊢ e' : T"
      with sconf' have wf_config':"P,E,s' ⊢ e' : T √" by(simp add:wf_config_def)
      { assume "¬ final e'"
        from Progress[OF wf wf_config' D' this] nored have False
          by simp }
      hence "final e'" by fast
      with wte' show ?thesis by(auto simp:final_def)
    next
      assume wte':"P,E,hp s' ⊢ e' : NT"
      with sconf' have wf_config':"P,E,s' ⊢ e' : NT √" by(simp add:wf_config_def)
      { assume "¬ final e'"
        from Progress[OF wf wf_config' D' this] nored have False
          by simp }
      hence "final e'" by fast
      with wte' Class show ?thesis by(auto simp:final_def)
    qed
  qed
qed

end