Theory Determinism

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

section ‹Determinism Proof›

theory Determinism
imports TypeSafe
begin

subsection‹Some lemmas›

lemma maps_nth:
  "⟦(E(xs [↦] ys)) x = Some y; length xs = length ys; distinct xs⟧ 
  ⟹ ∀i. x = xs!i ∧ i < length xs ⟶ y = ys!i"
proof (induct xs arbitrary: ys E)
  case Nil thus ?case by simp
next
  case (Cons x' xs')
  have map:"(E(x' # xs' [↦] ys)) x = Some y"
    and length:"length (x'#xs') = length ys"
    and dist:"distinct (x'#xs')"
    and IH:"⋀ys E. ⟦(E(xs' [↦] ys)) x = Some y; length xs' = length ys; 
                     distinct xs'⟧ 
         ⟹ ∀i. x = xs'!i ∧ i < length xs' ⟶ y = ys!i" by fact+
  from length obtain y' ys' where ys:"ys = y'#ys'" by(cases ys) auto
  { fix i assume x:"x = (x'#xs')!i" and i:"i < length(x'#xs')"
    have "y = ys!i"
    proof(cases i)
      case 0 with x map ys dist show ?thesis by simp
    next
      case (Suc n)
      with x i have x':"x = xs'!n" and n:"n < length xs'" by simp_all
      from map ys have map':"(E(x' ↦ y', xs' [↦] ys')) x = Some y" by simp
      from length ys have length':"length xs' = length ys'" by simp
      from dist have dist':"distinct xs'" by simp
      from IH[OF map' length' dist'] 
      have "∀i. x = xs'!i ∧ i < length xs' ⟶ y = ys'!i" .
      with x' n have "y = ys'!n" by simp
      with ys n Suc show ?thesis by simp
    qed }
  thus ?case by simp
qed


lemma nth_maps:"⟦length pns = length Ts; distinct pns; i < length Ts⟧ 
  ⟹ (E(pns [↦] Ts)) (pns!i) = Some (Ts!i)"
proof (induct i arbitrary: E pns Ts)
  case 0
  have dist:"distinct pns" and length:"length pns = length Ts"
    and i_length:"0 < length Ts" by fact+
  from i_length obtain T' Ts' where Ts:"Ts = T'#Ts'" by(cases Ts) auto
  with length obtain p' pns' where "pns = p'#pns'" by(cases pns) auto
  with Ts dist show ?case by simp
next
  case (Suc n)
  have i_length:"Suc n < length Ts" and dist:"distinct pns"
    and length:"length pns = length Ts" by fact+
  from Suc obtain T' Ts' where Ts:"Ts = T'#Ts'" by(cases Ts) auto
  with length obtain p' pns' where pns:"pns = p'#pns'" by(cases pns) auto
  with Ts length dist have length':"length pns' = length Ts'" 
    and dist':"distinct pns'" and notin:"p' ∉ set pns'" by simp_all
  from i_length Ts have n_length:"n < length Ts'" by simp
  with length' dist' have map:"(E(p' ↦ T', pns' [↦] Ts')) (pns'!n) = Some(Ts'!n)" by fact
  with notin have "(E(p' ↦ T', pns' [↦] Ts')) p' = Some T'" by simp
  with pns Ts map show ?case by simp
qed

lemma casts_casts_eq_result:
  fixes s :: state
  assumes casts:"P ⊢ T casts v to v'" and casts':"P ⊢ T casts v to w'" 
  and type:"is_type P T" and wte:"P,E ⊢ e :: T'" and leq:"P ⊢ T' ≤ T"
  and eval:"P,E ⊢ ⟨e,s⟩ ⇒ ⟨Val v,(h,l)⟩" and sconf:"P,E ⊢ s √"
  and wf:"wf_C_prog P"
  shows "v' = w'"
proof(cases "∀C. T ≠ Class C")
  case True
  with casts casts' show ?thesis
    by(auto elim:casts_to.cases)
next
  case False
  then obtain C where T:"T = Class C" by auto
  with type have "is_class P C" by simp
  with wf T leq have "T' = NT ∨ (∃D. T' = Class D ∧ P ⊢ Path D to C unique)"
    by(simp add:widen_Class)
  thus ?thesis
  proof(rule disjE)
    assume "T' = NT"
    with wf eval sconf wte have "v = Null"
      by(fastforce dest:eval_preserves_type)
    with casts casts' show ?thesis by(fastforce elim:casts_to.cases)
  next
    assume "∃D. T' = Class D ∧ P ⊢ Path D to C unique"
    then obtain D where T':"T' = Class D" 
      and path_unique:"P ⊢ Path D to C unique" by auto
    with wf eval sconf wte
    have "P,E,h ⊢ Val v : T' ∨ P,E,h ⊢ Val v : NT"
      by(fastforce dest:eval_preserves_type)
    thus ?thesis
    proof(rule disjE)
      assume "P,E,h ⊢ Val v : T'"
      with T' obtain a Cs C' S where h:"h a = Some(C',S)" and v:"v = Ref(a,Cs)"
        and last:"last Cs = D"
        by(fastforce dest:typeof_Class_Subo)
      from casts' v last T obtain Cs' Ds where "P ⊢ Path D to C via Cs'"
        and "Ds = Cs@⇩pCs'" and "w' = Ref(a,Ds)"
        by(auto elim:casts_to.cases)
      with casts T v last path_unique show ?thesis
        by auto(erule casts_to.cases,auto simp:path_via_def path_unique_def)
    next
      assume "P,E,h ⊢ Val v : NT"
      with wf eval sconf wte have "v = Null"
        by(fastforce dest:eval_preserves_type)
      with casts casts' show ?thesis by(fastforce elim:casts_to.cases)
    qed
  qed
qed

lemma Casts_Casts_eq_result:
  assumes wf:"wf_C_prog P"
  shows "⟦P ⊢ Ts Casts vs to vs'; P ⊢ Ts Casts vs to ws'; ∀T ∈ set Ts. is_type P T;
          P,E ⊢ es [::] Ts'; P ⊢ Ts' [≤] Ts; P,E ⊢ ⟨es,s⟩ [⇒] ⟨map Val vs,(h,l)⟩;
          P,E ⊢ s √⟧
      ⟹ vs' = ws'"
proof (induct vs arbitrary: vs' ws' Ts Ts' es s)
  case Nil thus ?case by (auto elim!:Casts_to.cases)
next
  case (Cons x xs)
  have CastsCons:"P ⊢ Ts Casts x # xs to vs'" 
    and CastsCons':"P ⊢ Ts Casts x # xs to ws'"
    and type:"∀T ∈ set Ts. is_type P T" 
    and wtes:"P,E ⊢ es [::] Ts'" and subs:"P ⊢ Ts' [≤] Ts"
    and evals:"P,E ⊢ ⟨es,s⟩ [⇒] ⟨map Val (x#xs),(h,l)⟩"
    and sconf:"P,E ⊢ s √"
    and IH:"⋀vs' ws' Ts Ts' es s. 
    ⟦P ⊢ Ts Casts xs to vs'; P ⊢ Ts Casts xs to ws'; ∀T ∈ set Ts. is_type P T; 
     P,E ⊢ es [::] Ts'; P ⊢ Ts' [≤] Ts; P,E ⊢ ⟨es,s⟩ [⇒] ⟨map Val xs,(h,l)⟩;
     P,E ⊢ s √⟧ 
     ⟹ vs' = ws'" by fact+
  from CastsCons obtain y ys S Ss where vs':"vs' = y#ys" and Ts:"Ts = S#Ss"
    apply -
    apply(frule length_Casts_vs,cases Ts,auto)
    apply(frule length_Casts_vs',cases vs',auto)
    done
  with CastsCons have casts:"P ⊢ S casts x to y" and Casts:"P ⊢ Ss Casts xs to ys"
    by(auto elim:Casts_to.cases)
  from Ts type have type':"is_type P S" and types':"∀T ∈ set Ss. is_type P T"
    by auto
  from Ts CastsCons' obtain z zs where ws':"ws' = z#zs"
    by simp(frule length_Casts_vs',cases ws',auto)
  with Ts CastsCons' have casts':"P ⊢ S casts x to z" 
    and Casts':"P ⊢ Ss Casts xs to zs"
    by(auto elim:Casts_to.cases)
  from Ts subs obtain U Us where Ts':"Ts' = U#Us" and subs':"P ⊢ Us [≤] Ss"
    and sub:"P ⊢ U ≤ S" by(cases Ts',auto simp:fun_of_def)
  from wtes Ts' obtain e' es' where es:"es = e'#es'" and wte':"P,E ⊢ e' :: U"
    and wtes':"P,E ⊢ es' [::] Us" by(cases es) auto
  with evals obtain h' l' where eval:"P,E ⊢ ⟨e',s⟩ ⇒ ⟨Val x,(h',l')⟩"
    and evals':"P,E ⊢ ⟨es',(h',l')⟩ [⇒] ⟨map Val xs,(h,l)⟩"
    by (auto elim:evals.cases)
  from wf eval wte' sconf have "P,E ⊢ (h',l') √" by(rule eval_preserves_sconf)
  from IH[OF Casts Casts' types' wtes' subs' evals' this] have eq:"ys = zs" .
  from casts casts' type' wte' sub eval sconf wf have "y = z"
    by(rule casts_casts_eq_result)
  with eq vs' ws' show ?case by simp
qed



lemma Casts_conf: assumes wf: "wf_C_prog P"
  shows "P ⊢ Ts Casts vs to vs' ⟹ 
  (⋀es s Ts'. ⟦ P,E ⊢ es [::] Ts'; P,E ⊢ ⟨es,s⟩ [⇒] ⟨map Val vs,(h,l)⟩; P,E ⊢ s √;
             P ⊢ Ts' [≤] Ts⟧ ⟹ 
     ∀i < length Ts. P,h ⊢ vs'!i :≤ Ts!i)"
proof(induct rule:Casts_to.induct)
  case Casts_Nil thus ?case by simp
next
  case (Casts_Cons T v v' Ts vs vs')
  have casts:"P ⊢ T casts v to v'" and wtes:"P,E ⊢ es [::] Ts'" 
    and evals:"P,E ⊢ ⟨es,s⟩ [⇒] ⟨map Val (v#vs),(h,l)⟩"
    and subs:"P ⊢ Ts' [≤] (T#Ts)" and sconf:"P,E ⊢ s √"
    and IH:"⋀es s Ts'.⟦P,E ⊢ es [::] Ts'; P,E ⊢ ⟨es,s⟩ [⇒] ⟨map Val vs,(h,l)⟩; 
                   P,E ⊢ s √; P ⊢ Ts' [≤] Ts⟧
               ⟹ ∀i<length Ts. P,h ⊢ vs' ! i :≤ Ts ! i" by fact+
  from subs obtain U Us where Ts':"Ts' = U#Us" by(cases Ts') auto
  with subs have sub':"P ⊢ U ≤ T" and subs':"P ⊢ Us [≤] Ts" 
    by (simp_all add:fun_of_def)
  from wtes Ts' obtain e' es' where es:"es = e'#es'" by(cases es) auto
  with Ts' wtes have wte':"P,E ⊢ e' :: U" and wtes':"P,E ⊢ es' [::] Us" by auto
  from es evals obtain s' where eval':"P,E ⊢ ⟨e',s⟩ ⇒ ⟨Val v,s'⟩"
    and evals':"P,E ⊢ ⟨es',s'⟩ [⇒] ⟨map Val vs,(h,l)⟩" 
    by(auto elim:evals.cases)
  from wf eval' wte' sconf have sconf':"P,E ⊢ s' √" by(rule eval_preserves_sconf)
  from evals' have hext:"hp s' ⊴ h" by(cases s',auto intro:evals_hext)
  from wf eval' sconf wte' have "P,E,(hp s') ⊢ Val v :⇘NT⇙ U"
    by(rule eval_preserves_type)
  with hext have wtrt:"P,E,h ⊢ Val v :⇘NT⇙ U"
    by(cases U,auto intro:hext_typeof_mono)
  from casts wtrt sub' have "P,h ⊢ v' :≤ T"
  proof(induct rule:casts_to.induct)
    case (casts_prim T'' v'')
    have "∀C. T'' ≠ Class C" and "P,E,h ⊢ Val v'' :⇘NT⇙ U" and "P ⊢ U ≤ T''" by fact+
    thus ?case by(cases T'') auto
  next
    case (casts_null C) thus ?case by simp
  next
    case (casts_ref Cs C Cs' Ds a)
    have path:"P ⊢ Path last Cs to C via Cs'"
      and Ds:"Ds = Cs @⇩p Cs'"
      and wtref:"P,E,h ⊢ ref (a, Cs) :⇘NT⇙ U" by fact+
    from wtref obtain D S where subo:"Subobjs P D Cs" and h:"h a = Some(D,S)"
      by(cases U,auto split:if_split_asm)
    from path Ds have last:"C = last Ds"  
      by(fastforce intro!:appendPath_last Subobjs_nonempty simp:path_via_def)
    from subo path Ds wf have "Subobjs P D Ds"
      by(fastforce intro:Subobjs_appendPath simp:path_via_def)
    with last h show ?case by simp
  qed
  with IH[OF wtes' evals' sconf' subs'] show ?case
    by(auto simp:nth_Cons,case_tac i,auto)
qed


lemma map_Val_throw_False:"map Val vs = map Val ws @ throw ex # es ⟹ False"
proof (induct vs arbitrary: ws)
  case Nil thus ?case by simp
next
  case (Cons v' vs')
  have eq:"map Val (v'#vs') = map Val ws @ throw ex # es"
    and IH:"⋀ws'. map Val vs' = map Val ws' @ throw ex # es ⟹ False" by fact+
  from eq obtain w' ws' where ws:"ws = w'#ws'" by(cases ws) auto
  from eq have "tl(map Val (v'#vs')) = tl(map Val ws @ throw ex # es)" by simp
  hence "map Val vs' = tl(map Val ws @ throw ex # es)" by simp
  with ws have "map Val vs' = map Val ws' @ throw ex # es" by simp
  from IH[OF this] show ?case .
qed

lemma map_Val_throw_eq:"map Val vs @ throw ex # es = map Val ws @ throw ex' # es' 
  ⟹ vs = ws ∧ ex = ex' ∧ es = es'"
  apply(clarsimp simp:append_eq_append_conv2)
  apply(erule disjE)
   apply(case_tac us)
    apply(fastforce elim:map_injective simp:inj_on_def)
   apply(fastforce dest:map_Val_throw_False)
  apply(case_tac us)
   apply(fastforce elim:map_injective simp:inj_on_def)
  apply(fastforce dest:sym[THEN map_Val_throw_False])
  done


subsection ‹The proof›

lemma deterministic_big_step:
assumes wf:"wf_C_prog P"
shows "P,E ⊢ ⟨e,s⟩ ⇒ ⟨e⇩1,s⇩1⟩ ⟹ 
       (⋀e⇩2 s⇩2 T. ⟦P,E ⊢ ⟨e,s⟩ ⇒ ⟨e⇩2,s⇩2⟩; P,E ⊢ e :: T; P,E ⊢ s √⟧ 
       ⟹ e⇩1 = e⇩2 ∧ s⇩1 = s⇩2)"
  and "P,E ⊢ ⟨es,s⟩ [⇒] ⟨es⇩1,s⇩1⟩ ⟹ 
       (⋀es⇩2 s⇩2 Ts. ⟦P,E ⊢ ⟨es,s⟩ [⇒] ⟨es⇩2,s⇩2⟩; P,E ⊢ es [::] Ts; P,E ⊢ s √⟧ 
        ⟹ es⇩1 = es⇩2 ∧ s⇩1 = s⇩2)"
proof (induct rule:eval_evals.inducts)
  case New thus ?case by(auto elim: eval_cases)
next
  case NewFail thus ?case by(auto elim: eval_cases)
next
  case (StaticUpCast E e s⇩0 a Cs s⇩1 C Cs' Ds e⇩2 s⇩2)
  have eval:"P,E ⊢ ⟨⦇C⦈e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩"
    and path_via:"P ⊢ Path last Cs to C via Cs'" and Ds:"Ds = Cs @⇩p Cs'" 
    and wt:"P,E ⊢ ⦇C⦈e :: T" and sconf:"P,E ⊢ s⇩0 √"
    and IH:"⋀e⇩2 s⇩2 T. ⟦P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩; P,E ⊢ e :: T; P,E ⊢ s⇩0 √⟧ 
            ⟹ ref (a,Cs) = e⇩2 ∧ s⇩1 = s⇩2" by fact+
  from wt obtain D where "class":"is_class P C" and wte:"P,E ⊢ e :: Class D"
    and disj:"P ⊢ Path D to C unique ∨ 
              (P ⊢ C ≼⇧* D ∧ (∀Cs. P ⊢ Path C to D via Cs ⟶ Subobjs⇩R P C Cs))"
    by auto
  from eval show ?case
  proof(rule eval_cases)
    fix Xs Xs' a'
    assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref (a',Xs),s⇩2⟩" 
      and path_via':"P ⊢ Path last Xs to C via Xs'"
      and ref:"e⇩2 = ref (a',Xs@⇩pXs')"
    from IH[OF eval_ref wte sconf] have eq:"a = a' ∧ Cs = Xs ∧ s⇩1 = s⇩2" by simp
    with wf eval_ref sconf wte have last:"last Cs = D"
      by(auto dest:eval_preserves_type split:if_split_asm)
    from disj show "ref (a,Ds) = e⇩2 ∧ s⇩1 = s⇩2"
    proof (rule disjE)
      assume "P ⊢ Path D to C unique"
      with path_via path_via' eq last have "Cs' = Xs'"
        by(fastforce simp add:path_via_def path_unique_def)
      with eq ref Ds show ?thesis by simp
    next
      assume "P ⊢ C ≼⇧* D ∧ (∀Cs. P ⊢ Path C to D via Cs  ⟶ Subobjs⇩R P C Cs)"
      with "class" wf obtain Cs'' where "P ⊢ Path C to D via Cs''"
        by(auto dest:leq_implies_path)
      with path_via path_via' wf eq last have "Cs' = Xs'"
        by(auto dest:path_via_reverse)
      with eq ref Ds show ?thesis by simp
    qed
  next
    fix Xs Xs' a'
    assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs@C#Xs'),s⇩2⟩"
      and ref:"e⇩2 = ref (a',Xs@[C])"
    from IH[OF eval_ref wte sconf] have eq:"a = a' ∧ Cs = Xs@C#Xs' ∧ s⇩1 = s⇩2" by simp
    with wf eval_ref sconf wte obtain C' where 
      last:"last Cs = D" and "Subobjs P C' (Xs@C#Xs')"
      by(auto dest:eval_preserves_type split:if_split_asm)
    hence subo:"Subobjs P C (C#Xs')" by(fastforce intro:Subobjs_Subobjs)
    with eq last have leq:"P ⊢ C ≼⇧* D" by(fastforce dest:Subobjs_subclass)
    from path_via last have "P ⊢ D ≼⇧* C"
      by(auto dest:Subobjs_subclass simp:path_via_def)
    with leq wf have CeqD:"C = D" by(rule subcls_asym2)
    with last path_via wf have "Cs' = [D]" by(fastforce intro:path_via_C)
    with Ds last have Ds':"Ds = Cs" by(simp add:appendPath_def)
    from subo CeqD last eq wf have "Xs' = []" by(auto dest:mdc_eq_last)
    with eq Ds' ref show "ref (a,Ds) = e⇩2 ∧ s⇩1 = s⇩2" by simp
  next
    assume eval_null:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨null,s⇩2⟩"
    from IH[OF eval_null wte sconf] show "ref (a,Ds) = e⇩2 ∧ s⇩1 = s⇩2" by simp
  next
    fix Xs a'
    assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs),s⇩2⟩" and notin:"C ∉ set Xs"
      and notleq:"¬ P ⊢ last Xs ≼⇧* C" and throw:"e⇩2 = THROW ClassCast"
    from IH[OF eval_ref wte sconf] have eq:"a = a' ∧ Cs = Xs ∧ s⇩1 = s⇩2" by simp
    with wf eval_ref sconf wte have last:"last Cs = D" and notempty:"Cs ≠ []"
      by(auto dest!:eval_preserves_type Subobjs_nonempty split:if_split_asm)
    from disj have "C = D"
    proof(rule disjE)
      assume path_unique:"P ⊢ Path D to C unique"
      with last have "P ⊢ D ≼⇧* C" 
        by(fastforce dest:Subobjs_subclass simp:path_unique_def)
      with notleq last eq show ?thesis by simp
    next
      assume ass:"P ⊢ C ≼⇧* D ∧ 
                  (∀Cs. P ⊢ Path C to D via Cs  ⟶ Subobjs⇩R P C Cs)"
      with "class" wf obtain Cs'' where path_via':"P ⊢ Path C to D via Cs''"
        by(auto dest:leq_implies_path)
      with path_via wf eq last have "Cs'' = [D]"
        by(fastforce dest:path_via_reverse)
      with ass path_via' have "Subobjs⇩R P C [D]" by simp
      thus ?thesis by(fastforce dest:hd_SubobjsR)
    qed
    with last notin eq notempty show "ref (a,Ds) = e⇩2 ∧ s⇩1 = s⇩2"
      by(fastforce intro:last_in_set)
  next
    fix e' assume eval_throw:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw e',s⇩2⟩"
    from IH[OF eval_throw wte sconf] show "ref (a,Ds) = e⇩2 ∧ s⇩1 = s⇩2" by simp
  qed
next
  case (StaticDownCast E e s⇩0 a Cs C Cs' s⇩1 e⇩2 s⇩2 T)
  have eval:"P,E ⊢ ⟨⦇C⦈e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩" 
    and eval':"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a,Cs@[C]@Cs'),s⇩1⟩"
    and wt:"P,E ⊢ ⦇C⦈e :: T" and sconf:"P,E ⊢ s⇩0 √"
    and IH:"⋀e⇩2 s⇩2 T. ⟦P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩; P,E ⊢ e :: T; P,E ⊢ s⇩0 √⟧
                      ⟹ ref(a,Cs@[C]@Cs') = e⇩2 ∧ s⇩1 = s⇩2" by fact+
  from wt obtain D where wte:"P,E ⊢ e :: Class D"
    and disj:"P ⊢ Path D to C unique ∨ 
              (P ⊢ C ≼⇧* D ∧ (∀Cs. P ⊢ Path C to D via Cs ⟶ Subobjs⇩R P C Cs))"
    by auto
  from eval show ?case
  proof(rule eval_cases)
    fix Xs Xs' a'
    assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs),s⇩2⟩" 
      and path_via:"P ⊢ Path last Xs to C via Xs'"
      and ref:"e⇩2 = ref (a',Xs@⇩pXs')"
    from IH[OF eval_ref wte sconf] have eq:"a = a' ∧ Cs@[C]@Cs' = Xs ∧ s⇩1 = s⇩2"
      by simp
    with wf eval_ref sconf wte obtain C' where 
      last:"last(C#Cs') = D" and "Subobjs P C' (Cs@[C]@Cs')"
      by(auto dest:eval_preserves_type split:if_split_asm)
    hence "P ⊢ Path C to D via C#Cs'" 
      by(fastforce intro:Subobjs_Subobjs simp:path_via_def)
    with eq last path_via wf have "Xs' = [C] ∧ Cs' = [] ∧ C = D"
      apply clarsimp
      apply(split if_split_asm)
      by(simp,drule path_via_reverse,simp,simp)+
    with ref eq show "ref(a,Cs@[C]) = e⇩2 ∧ s⇩1 = s⇩2" by(fastforce simp:appendPath_def)
  next
    fix Xs Xs' a'
    assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs@C#Xs'),s⇩2⟩"
      and ref:"e⇩2 = ref (a',Xs@[C])"
    from IH[OF eval_ref wte sconf] have eq:"a = a' ∧ Cs@[C]@Cs' = Xs@C#Xs' ∧ s⇩1 = s⇩2"
      by simp
    with wf eval_ref sconf wte obtain C' where 
      last:"last(C#Xs') = D" and subo:"Subobjs P C' (Cs@[C]@Cs')"
      by(auto dest:eval_preserves_type split:if_split_asm)
    from subo wf have notin:"C ∉ set Cs" by -(rule unique2,simp)
    from subo wf have "C ∉ set Cs'"  by -(rule unique1,simp,simp)
    with notin eq have "Cs = Xs ∧ Cs' = Xs'"
      by -(rule only_one_append,simp+)
    with eq ref show "ref(a,Cs@[C]) = e⇩2 ∧ s⇩1 = s⇩2" by simp
  next
    assume eval_null:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨null,s⇩2⟩"
    from IH[OF eval_null wte sconf] show "ref (a,Cs@[C]) = e⇩2 ∧ s⇩1 = s⇩2" by simp
  next
    fix Xs a' 
    assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs),s⇩2⟩" and notin:"C ∉ set Xs"
    from IH[OF eval_ref wte sconf] have "a = a' ∧ Cs@[C]@Cs' = Xs ∧ s⇩1 = s⇩2" 
      by simp
    with notin show "ref(a,Cs@[C]) = e⇩2 ∧ s⇩1 = s⇩2" by fastforce
  next
    fix e' assume eval_throw:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw e',s⇩2⟩"
    from IH[OF eval_throw wte sconf] show "ref (a,Cs@[C]) = e⇩2 ∧ s⇩1 = s⇩2" by simp
  qed
next
  case (StaticCastNull E e s⇩0 s⇩1 C e⇩2 s⇩2 T)
  have eval:"P,E ⊢ ⟨⦇C⦈e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩"
    and wt:"P,E ⊢ ⦇C⦈e :: T" and sconf:"P,E ⊢ s⇩0 √"
    and IH:"⋀e⇩2 s⇩2 T. ⟦P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩; P,E ⊢ e :: T; P,E ⊢ s⇩0 √⟧ 
                    ⟹ null = e⇩2 ∧ s⇩1 = s⇩2" by fact+
  from wt obtain D where wte:"P,E ⊢ e :: Class D" by auto
  from eval show ?case
  proof(rule eval_cases)
    fix Xs Xs' a'
    assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref (a',Xs),s⇩2⟩" 
    from IH[OF eval_ref wte sconf] show "null = e⇩2 ∧ s⇩1 = s⇩2" by simp
  next
    fix Xs Xs' a'
    assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs@C#Xs'),s⇩2⟩"
    from IH[OF eval_ref wte sconf] show "null = e⇩2 ∧ s⇩1 = s⇩2" by simp
  next
    assume eval_null:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨null,s⇩2⟩" and "e⇩2 = null"
    with IH[OF eval_null wte sconf] show "null = e⇩2 ∧ s⇩1 = s⇩2" by simp
  next
    fix Xs a' 
    assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs),s⇩2⟩"
    from IH[OF eval_ref wte sconf] show "null = e⇩2 ∧ s⇩1 = s⇩2" by simp
  next
    fix e' assume eval_throw:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw e',s⇩2⟩"
    from IH[OF eval_throw wte sconf] show "null = e⇩2 ∧ s⇩1 = s⇩2" by simp
  qed
next
  case (StaticCastFail E e s⇩0 a Cs s⇩1 C e⇩2 s⇩2 T)
  have eval:"P,E ⊢ ⟨⦇C⦈e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩"
    and notleq:"¬ P ⊢ last Cs ≼⇧* C" and notin:"C ∉ set Cs"
    and wt:"P,E ⊢ ⦇C⦈e :: T" and sconf:"P,E ⊢ s⇩0 √"
    and IH:"⋀e⇩2 s⇩2 T. ⟦P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩; P,E ⊢ e :: T; P,E ⊢ s⇩0 √⟧ 
                    ⟹ref (a, Cs) = e⇩2 ∧ s⇩1 = s⇩2" by fact+
  from wt obtain D where wte:"P,E ⊢ e :: Class D" by auto
  from eval show ?case
  proof(rule eval_cases)
    fix Xs Xs' a'
    assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref (a',Xs),s⇩2⟩" 
      and path_via:"P ⊢ Path last Xs to C via Xs'"
    from IH[OF eval_ref wte sconf] have eq:"a = a' ∧ Cs = Xs ∧ s⇩1 = s⇩2" by simp
    with path_via wf have "P ⊢ last Cs ≼⇧* C" 
      by(auto dest:Subobjs_subclass simp:path_via_def)
    with notleq show "THROW ClassCast = e⇩2 ∧ s⇩1 = s⇩2" by simp
  next
    fix Xs Xs' a'
    assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs@C#Xs'),s⇩2⟩"
    from IH[OF eval_ref wte sconf] have "a = a' ∧ Cs = Xs@C#Xs' ∧ s⇩1 = s⇩2" by simp
    with notin show "THROW ClassCast = e⇩2 ∧ s⇩1 = s⇩2" by simp
  next
    assume eval_null:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨null,s⇩2⟩"
    from IH[OF eval_null wte sconf] show "THROW ClassCast = e⇩2 ∧ s⇩1 = s⇩2" by simp
  next
    fix Xs a' 
    assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs),s⇩2⟩"
      and throw:"e⇩2 = THROW ClassCast"
    from IH[OF eval_ref wte sconf] have "a = a' ∧ Cs = Xs ∧ s⇩1 = s⇩2"
      by simp
    with throw show "THROW ClassCast = e⇩2 ∧ s⇩1 = s⇩2" by simp
  next
    fix e' assume eval_throw:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw e',s⇩2⟩"
    from IH[OF eval_throw wte sconf] show "THROW ClassCast = e⇩2 ∧ s⇩1 = s⇩2" by simp
  qed 
next
  case (StaticCastThrow E e s⇩0 e' s⇩1 C e⇩2 s⇩2 T)
  have eval:"P,E ⊢ ⟨⦇C⦈e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩"
    and wt:"P,E ⊢ ⦇C⦈e :: T" and sconf:"P,E ⊢ s⇩0 √"
    and IH:"⋀e⇩2 s⇩2 T. ⟦P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩; P,E ⊢ e :: T; P,E ⊢ s⇩0 √⟧
                   ⟹ throw e' = e⇩2 ∧ s⇩1 = s⇩2" by fact+
  from wt obtain D where wte:"P,E ⊢ e :: Class D" by auto
  from eval show ?case
  proof(rule eval_cases)
    fix Xs Xs' a'
    assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref (a',Xs),s⇩2⟩" 
    from IH[OF eval_ref wte sconf] show " throw e' = e⇩2 ∧ s⇩1 = s⇩2" by simp
  next
    fix Xs Xs' a'
    assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs@C#Xs'),s⇩2⟩"
    from IH[OF eval_ref wte sconf] show "throw e' = e⇩2 ∧ s⇩1 = s⇩2" by simp
  next
    assume eval_null:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨null,s⇩2⟩"
    from IH[OF eval_null wte sconf] show "throw e' = e⇩2 ∧ s⇩1 = s⇩2" by simp
  next
    fix Xs a'
    assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs),s⇩2⟩"
    from IH[OF eval_ref wte sconf] show "throw e' = e⇩2 ∧ s⇩1 = s⇩2" by simp
  next
    fix e'' assume eval_throw:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw e'',s⇩2⟩"
      and throw:"e⇩2 = throw e''"
    from IH[OF eval_throw wte sconf] throw show "throw e' = e⇩2 ∧ s⇩1 = s⇩2" by simp
  qed
next
  case (StaticUpDynCast E e s⇩0 a Cs s⇩1 C Cs' Ds e⇩2 s⇩2 T)
  have eval:"P,E ⊢ ⟨Cast C e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩"
    and path_via:"P ⊢ Path last Cs to C via Cs'" 
    and path_unique:"P ⊢ Path last Cs to C unique"
    and Ds:"Ds = Cs@⇩pCs'" and wt:"P,E ⊢ Cast C e :: T" and sconf:"P,E ⊢ s⇩0 √"
    and IH:"⋀e⇩2 s⇩2 T. ⟦P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩; P,E ⊢ e :: T; P,E ⊢ s⇩0 √⟧
                    ⟹ ref(a,Cs) = e⇩2 ∧ s⇩1 = s⇩2" by fact+
  from wt obtain D where wte:"P,E ⊢ e :: Class D" by auto
  from eval show ?case
  proof(rule eval_cases)
    fix Xs Xs' a'
    assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref (a',Xs),s⇩2⟩" 
      and path_via':"P ⊢ Path last Xs to C via Xs'"
      and ref:"e⇩2 = ref (a',Xs@⇩pXs')"
    from IH[OF eval_ref wte sconf] have eq:"a = a' ∧ Cs = Xs ∧ s⇩1 = s⇩2" by simp
    with wf eval_ref sconf wte have last:"last Cs = D"
      by(auto dest:eval_preserves_type split:if_split_asm)
    with path_unique path_via path_via' eq have "Xs' = Cs'"
      by(fastforce simp:path_via_def path_unique_def)
    with eq Ds ref show "ref (a, Ds) = e⇩2 ∧ s⇩1 = s⇩2" by simp
  next
    fix Xs Xs' a'
    assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs@C#Xs'),s⇩2⟩"
      and ref:"e⇩2 = ref (a',Xs@[C])"
    from IH[OF eval_ref wte sconf] have eq:"a = a' ∧ Cs = Xs@C#Xs' ∧ s⇩1 = s⇩2" by simp
    with wf eval_ref sconf wte obtain C' where 
      last:"last Cs = D" and "Subobjs P C' (Xs@C#Xs')"
      by(auto dest:eval_preserves_type split:if_split_asm)
    hence "Subobjs P C (C#Xs')" by(fastforce intro:Subobjs_Subobjs)
    with last eq have "P ⊢ Path C to D via C#Xs'" 
      by(simp add:path_via_def)
    with path_via wf last have "Xs' = [] ∧ Cs' = [C] ∧ C = D" 
      by(fastforce dest:path_via_reverse)
    with eq Ds ref show "ref (a, Ds) = e⇩2 ∧ s⇩1 = s⇩2" by (simp add:appendPath_def)
  next
    fix Xs Xs' D' S a' h l
    assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs),(h,l)⟩"
      and h:"h a' = Some(D',S)" and path_via':"P ⊢ Path D' to C via Xs'"
      and path_unique':"P ⊢ Path D' to C unique" and s2:"s⇩2 = (h,l)"
      and ref:"e⇩2 = ref(a',Xs')"
    from IH[OF eval_ref wte sconf] s2 have eq:"a = a' ∧ Cs = Xs ∧ s⇩1 = s⇩2" by simp
    with wf eval_ref sconf wte h have "last Cs = D"
      and "Subobjs P D' Cs"
      by(auto dest:eval_preserves_type split:if_split_asm)
    with path_via wf have "P ⊢ Path D' to C via Cs@⇩pCs'"
      by(fastforce intro:Subobjs_appendPath appendPath_last[THEN sym] 
                   dest:Subobjs_nonempty simp:path_via_def)
    with path_via' path_unique' Ds have "Xs' = Ds"
      by(fastforce simp:path_via_def path_unique_def)
    with eq ref show "ref (a, Ds) = e⇩2 ∧ s⇩1 = s⇩2" by simp
  next
    assume eval_null:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨null,s⇩2⟩"
    from IH[OF eval_null wte sconf] show "ref (a, Ds) = e⇩2 ∧ s⇩1 = s⇩2" by simp
  next
    fix Xs D' S a' h l
    assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs),(h,l)⟩"
      and not_unique:"¬ P ⊢ Path last Xs to C unique" and s2:"s⇩2 = (h,l)"
    from IH[OF eval_ref wte sconf] s2 have eq:"a = a' ∧ Cs = Xs ∧ s⇩1 = s⇩2" by simp
    with path_unique not_unique show "ref (a, Ds) = e⇩2 ∧ s⇩1 = s⇩2" by simp
  next
    fix e' assume eval_throw:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw e',s⇩2⟩"
    from IH[OF eval_throw wte sconf] show "ref (a, Ds) = e⇩2 ∧ s⇩1 = s⇩2" by simp
  qed
next
  case (StaticDownDynCast E e s⇩0 a Cs C Cs' s⇩1 e⇩2 s⇩2 T)
  have eval:"P,E ⊢ ⟨Cast C e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩"
    and wt:"P,E ⊢ Cast C e :: T" and sconf:"P,E ⊢ s⇩0 √"
    and IH:"⋀e⇩2 s⇩2 T. ⟦P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩; P,E ⊢ e :: T; P,E ⊢ s⇩0 √⟧
                    ⟹ ref(a,Cs@[C]@Cs') = e⇩2 ∧ s⇩1 = s⇩2" by fact+
  from wt obtain D where wte:"P,E ⊢ e :: Class D" by auto
  from eval show ?case
  proof(rule eval_cases)
    fix Xs Xs' a'
    assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs),s⇩2⟩" 
      and path_via:"P ⊢ Path last Xs to C via Xs'"
      and ref:"e⇩2 = ref (a',Xs@⇩pXs')"
    from IH[OF eval_ref wte sconf] have eq:"a = a' ∧ Cs@[C]@Cs' = Xs ∧ s⇩1 = s⇩2"
      by simp
    with wf eval_ref sconf wte obtain C' where 
      last:"last(C#Cs') = D" and "Subobjs P C' (Cs@[C]@Cs')"
      by(auto dest:eval_preserves_type split:if_split_asm)
    hence "P ⊢ Path C to D via C#Cs'" 
      by(fastforce intro:Subobjs_Subobjs simp:path_via_def)
    with eq last path_via wf have "Xs' = [C] ∧ Cs' = [] ∧ C = D"
      apply clarsimp
      apply(split if_split_asm)
      by(simp,drule path_via_reverse,simp,simp)+
    with ref eq show "ref(a,Cs@[C]) = e⇩2 ∧ s⇩1 = s⇩2" by(fastforce simp:appendPath_def)
  next
    fix Xs Xs' a'
    assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs@C#Xs'),s⇩2⟩"
      and ref:"e⇩2 = ref (a',Xs@[C])"
    from IH[OF eval_ref wte sconf] have eq:"a = a' ∧ Cs@[C]@Cs' = Xs@C#Xs' ∧ s⇩1 = s⇩2"
      by simp
    with wf eval_ref sconf wte obtain C' where 
      last:"last(C#Xs') = D" and subo:"Subobjs P C' (Cs@[C]@Cs')"
      by(auto dest:eval_preserves_type split:if_split_asm)
    from subo wf have notin:"C ∉ set Cs" by -(rule unique2,simp)
    from subo wf have "C ∉ set Cs'"  by -(rule unique1,simp,simp)
    with notin eq have "Cs = Xs ∧ Cs' = Xs'"
      by -(rule only_one_append,simp+)
    with eq ref show "ref(a,Cs@[C]) = e⇩2 ∧ s⇩1 = s⇩2" by simp
  next
    fix Xs Xs' D' S a' h l
    assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs),(h,l)⟩"
      and h:"h a' = Some(D',S)" and path_via:"P ⊢ Path D' to C via Xs'"
      and path_unique:"P ⊢ Path D' to C unique" and s2:"s⇩2 = (h,l)"
      and ref:"e⇩2 = ref(a',Xs')"
    from IH[OF eval_ref wte sconf] s2 have eq:"a = a' ∧ Cs@[C]@Cs' = Xs ∧ s⇩1 = s⇩2"
      by simp
    with wf eval_ref sconf wte h have "Subobjs P D' (Cs@[C]@Cs')"
      by(auto dest:eval_preserves_type split:if_split_asm)
    hence "Subobjs P D' (Cs@[C])" by(fastforce intro:appendSubobj)
    with path_via path_unique have "Xs' = Cs@[C]" 
      by(fastforce simp:path_via_def path_unique_def)
    with eq ref show "ref(a,Cs@[C]) = e⇩2 ∧ s⇩1 = s⇩2" by simp
  next
    assume eval_null:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨null,s⇩2⟩"
    from IH[OF eval_null wte sconf] show "ref (a,Cs@[C]) = e⇩2 ∧ s⇩1 = s⇩2" by simp
  next
    fix Xs D' S a' h l
    assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs),(h,l)⟩"
      and notin:"C ∉ set Xs" and s2:"s⇩2 = (h,l)"
    from IH[OF eval_ref wte sconf] s2 have "a = a' ∧ Cs@[C]@Cs' = Xs ∧ s⇩1 = s⇩2"
      by simp
    with notin show "ref (a,Cs@[C]) = e⇩2 ∧ s⇩1 = s⇩2" by fastforce
  next
    fix e' assume eval_throw:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw e',s⇩2⟩"
    from IH[OF eval_throw wte sconf] show "ref (a,Cs@[C]) = e⇩2 ∧ s⇩1 = s⇩2" by simp
  qed
next
  case (DynCast E e s⇩0 a Cs h l D S C Cs' e⇩2 s⇩2 T)
  have eval:"P,E ⊢ ⟨Cast C e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩"
    and path_via:"P ⊢ Path D to C via Cs'" and path_unique:"P ⊢ Path D to C unique"
    and h:"h a = Some(D,S)" and wt:"P,E ⊢ Cast C e :: T" and sconf:"P,E ⊢ s⇩0 √"
    and IH:"⋀e⇩2 s⇩2 T. ⟦P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩; P,E ⊢ e :: T; P,E ⊢ s⇩0 √⟧
                    ⟹ ref(a,Cs) = e⇩2 ∧ (h,l) = s⇩2" by fact+
  from wt obtain D' where wte:"P,E ⊢ e :: Class D'" by auto
  from eval show ?case
  proof(rule eval_cases)
    fix Xs Xs' a'
    assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs),s⇩2⟩"
      and path_via':"P ⊢ Path last Xs to C via Xs'"
      and ref:"e⇩2 = ref (a',Xs@⇩pXs')"
    from IH[OF eval_ref wte sconf] have eq:"a = a' ∧ Cs = Xs ∧ (h,l) = s⇩2" by simp
    with wf eval_ref sconf wte h have "last Cs = D'"
      and "Subobjs P D Cs"
      by(auto dest:eval_preserves_type split:if_split_asm)
    with path_via' wf eq have "P ⊢ Path D to C via Xs@⇩pXs'"
      by(fastforce intro:Subobjs_appendPath appendPath_last[THEN sym] 
                   dest:Subobjs_nonempty simp:path_via_def)
    with path_via path_unique have "Cs' = Xs@⇩pXs'"
      by(fastforce simp:path_via_def path_unique_def)
    with ref eq show "ref(a,Cs') = e⇩2 ∧ (h, l) = s⇩2" by simp
  next
    fix Xs Xs' a'
    assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs@C#Xs'),s⇩2⟩"
      and ref:"e⇩2 = ref (a',Xs@[C])"
    from IH[OF eval_ref wte sconf] have eq:"a = a' ∧ Cs = Xs@C#Xs' ∧ (h,l) = s⇩2"
      by simp
    with wf eval_ref sconf wte h have "Subobjs P D (Xs@[C]@Xs')"
      by(auto dest:eval_preserves_type split:if_split_asm)
    hence "Subobjs P D (Xs@[C])" by(fastforce intro:appendSubobj)
    with path_via path_unique have "Cs' = Xs@[C]" 
      by(fastforce simp:path_via_def path_unique_def)
    with eq ref show "ref(a,Cs') = e⇩2 ∧ (h, l) = s⇩2" by simp
  next
    fix Xs Xs' D'' S' a' h' l'
    assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs),(h',l')⟩"
      and h':"h' a' = Some(D'',S')" and path_via':"P ⊢ Path D'' to C via Xs'"
      and s2:"s⇩2 = (h',l')" and ref:"e⇩2 = ref(a',Xs')"
    from IH[OF eval_ref wte sconf] have eq:"a = a' ∧ Cs = Xs ∧ h = h' ∧ l = l'"
      by simp
    with h h' path_via path_via' path_unique s2 ref
    show "ref(a,Cs') = e⇩2 ∧ (h,l) = s⇩2"
      by(fastforce simp:path_via_def path_unique_def)
  next
    assume eval_null:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨null,s⇩2⟩"
    from IH[OF eval_null wte sconf] show "ref(a,Cs') = e⇩2 ∧ (h,l) = s⇩2" by simp
  next
    fix Xs D'' S' a' h' l'
    assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs),(h',l')⟩"
      and h':"h' a' = Some(D'',S')" and not_unique:"¬ P ⊢ Path D'' to C unique"
    from IH[OF eval_ref wte sconf] have eq:"a = a' ∧ Cs = Xs ∧ h = h' ∧ l = l'"
      by simp
    with h h' path_unique not_unique show "ref(a,Cs') = e⇩2 ∧ (h,l) = s⇩2" by simp
  next
    fix e' assume eval_throw:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw e',s⇩2⟩"
    from IH[OF eval_throw wte sconf] show "ref (a,Cs') = e⇩2 ∧ (h,l) = s⇩2" by simp
  qed
next
  case (DynCastNull E e s⇩0 s⇩1 C e⇩2 s⇩2 T)
  have eval:"P,E ⊢ ⟨Cast C e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩"
    and wt:"P,E ⊢ Cast C e :: T" and sconf:"P,E ⊢ s⇩0 √"
    and IH:"⋀e⇩2 s⇩2 T. ⟦P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩; P,E ⊢ e :: T; P,E ⊢ s⇩0 √⟧ 
                    ⟹ null = e⇩2 ∧ s⇩1 = s⇩2" by fact+
  from wt obtain D where wte:"P,E ⊢ e :: Class D" by auto
  from eval show ?case
  proof(rule eval_cases)
    fix Xs Xs' a'
    assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref (a',Xs),s⇩2⟩" 
    from IH[OF eval_ref wte sconf] show "null = e⇩2 ∧ s⇩1 = s⇩2" by simp
  next
    fix Xs Xs' a'
    assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs@C#Xs'),s⇩2⟩"
    from IH[OF eval_ref wte sconf] show "null = e⇩2 ∧ s⇩1 = s⇩2" by simp
  next
    fix Xs Xs' D' S a' h l
    assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs),(h,l)⟩"
    from IH[OF eval_ref wte sconf] show "null = e⇩2 ∧ s⇩1 = s⇩2" by simp
  next
    assume eval_null:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨null,s⇩2⟩" and "e⇩2 = null"
    with IH[OF eval_null wte sconf] show "null = e⇩2 ∧ s⇩1 = s⇩2" by simp
  next
    fix Xs D' S a' h l
    assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs),(h,l)⟩" and s2:"s⇩2 = (h,l)"
    from IH[OF eval_ref wte sconf] s2 show "null = e⇩2 ∧ s⇩1 = s⇩2" by simp
  next
    fix e' assume eval_throw:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw e',s⇩2⟩"
    from IH[OF eval_throw wte sconf] show "null = e⇩2 ∧ s⇩1 = s⇩2" by simp
  qed
next
  case (DynCastFail E e s⇩0 a Cs h l D S C e⇩2 s⇩2 T)
  have eval:"P,E ⊢ ⟨Cast C e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩"
    and h:"h a = Some(D,S)" and not_unique1:"¬ P ⊢ Path D to C unique"
    and not_unique2:"¬ P ⊢ Path last Cs to C unique" and notin:"C ∉ set Cs"
    and wt:"P,E ⊢ Cast C e :: T" and sconf:"P,E ⊢ s⇩0 √"
    and IH:"⋀e⇩2 s⇩2 T. ⟦P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩; P,E ⊢ e :: T; P,E ⊢ s⇩0 √⟧
                   ⟹ ref (a, Cs) = e⇩2 ∧ (h,l) = s⇩2" by fact+
  from wt obtain D' where wte:"P,E ⊢ e :: Class D'" by auto
  from eval show ?case
  proof(rule eval_cases)
    fix Xs Xs' a'
    assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs),s⇩2⟩"
      and path_unique:"P ⊢ Path last Xs to C unique"
    from IH[OF eval_ref wte sconf] have eq:"a = a' ∧ Cs = Xs ∧ (h,l) = s⇩2" by simp
    with path_unique not_unique2 show "null = e⇩2 ∧ (h,l) = s⇩2" by simp
  next
    fix Xs Xs' a'
    assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs@C#Xs'),s⇩2⟩"
    from IH[OF eval_ref wte sconf] have eq:"a = a' ∧ Cs = Xs@C#Xs' ∧ (h,l) = s⇩2"
      by simp
    with notin show "null = e⇩2 ∧ (h,l) = s⇩2" by fastforce
  next
    fix Xs Xs' D'' S' a' h' l'
    assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs),(h',l')⟩"
      and h':"h' a' = Some(D'',S')" and path_unique:"P ⊢ Path D'' to C unique"
    from IH[OF eval_ref wte sconf] have "a = a' ∧ Cs = Xs ∧ h = h' ∧ l = l'"
      by simp
    with h h' not_unique1 path_unique show "null = e⇩2 ∧ (h,l) = s⇩2" by simp
  next
    assume eval_null:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨null,s⇩2⟩"
    from IH[OF eval_null wte sconf] show "null = e⇩2 ∧ (h,l) = s⇩2" by simp
  next
    fix Xs D'' S' a' h' l'
    assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs),(h',l')⟩"
      and null:"e⇩2 = null" and s2:"s⇩2 = (h',l')"
    from IH[OF eval_ref wte sconf] null s2 show "null = e⇩2 ∧ (h,l) = s⇩2" by simp
  next
    fix e' assume eval_throw:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw e',s⇩2⟩"
    from IH[OF eval_throw wte sconf] show "null = e⇩2 ∧ (h,l) = s⇩2" by simp
  qed
next
  case (DynCastThrow E e s⇩0 e' s⇩1 C e⇩2 s⇩2 T)
  have eval:"P,E ⊢ ⟨Cast C e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩"
    and wt:"P,E ⊢ Cast C e :: T" and sconf:"P,E ⊢ s⇩0 √"
    and IH:"⋀e⇩2 s⇩2 T. ⟦P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩; P,E ⊢ e :: T; P,E ⊢ s⇩0 √⟧
                   ⟹ throw e' = e⇩2 ∧ s⇩1 = s⇩2" by fact+
  from wt obtain D where wte:"P,E ⊢ e :: Class D" by auto
  from eval show ?case
  proof(rule eval_cases)
    fix Xs Xs' a'
    assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref (a',Xs),s⇩2⟩" 
    from IH[OF eval_ref wte sconf] show " throw e' = e⇩2 ∧ s⇩1 = s⇩2" by simp
  next
    fix Xs Xs' a'
    assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs@C#Xs'),s⇩2⟩"
    from IH[OF eval_ref wte sconf] show "throw e' = e⇩2 ∧ s⇩1 = s⇩2" by simp
  next
    fix Xs Xs' D'' S' a' h' l'
    assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs),(h',l')⟩"
    from IH[OF eval_ref wte sconf] show "throw e' = e⇩2 ∧ s⇩1 = s⇩2" by simp
  next
    assume eval_null:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨null,s⇩2⟩"
    from IH[OF eval_null wte sconf] show "throw e' = e⇩2 ∧ s⇩1 = s⇩2" by simp
  next
    fix Xs D'' S' a' h' l'
    assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs),(h',l')⟩"
    from IH[OF eval_ref wte sconf] show "throw e' = e⇩2 ∧ s⇩1 = s⇩2" by simp
  next
    fix e'' assume eval_throw:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw e'',s⇩2⟩"
      and throw:"e⇩2 = throw e''"
    from IH[OF eval_throw wte sconf] throw show "throw e' = e⇩2 ∧ s⇩1 = s⇩2" by simp
  qed
next
  case Val thus ?case by(auto elim: eval_cases)
next
  case (BinOp E e⇩1 s⇩0 v⇩1 s⇩1 e⇩2 v⇩2 s⇩2 bop v e⇩2' s⇩2' T)
  have eval:"P,E ⊢ ⟨e⇩1 «bop» e⇩2,s⇩0⟩ ⇒ ⟨e⇩2',s⇩2'⟩"
    and binop:"binop (bop, v⇩1, v⇩2) = Some v"
    and wt:"P,E ⊢ e⇩1 «bop» e⇩2 :: T" and sconf:"P,E ⊢ s⇩0 √"
    and IH1:"⋀ei si T. ⟦P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨ei,si⟩; P,E ⊢ e⇩1 :: T; P,E ⊢ s⇩0 √⟧
                     ⟹ Val v⇩1 = ei ∧ s⇩1 = si"
    and IH2:"⋀ei si T. ⟦P,E ⊢ ⟨e⇩2,s⇩1⟩ ⇒ ⟨ei,si⟩; P,E ⊢ e⇩2 :: T; P,E ⊢ s⇩1 √⟧
                     ⟹ Val v⇩2 = ei ∧ s⇩2 = si" by fact+
  from wt obtain T⇩1 T⇩2 where wte1:"P,E ⊢ e⇩1 :: T⇩1" and wte2:"P,E ⊢ e⇩2 :: T⇩2"
    by auto
  from eval show ?case
  proof(rule eval_cases)
    fix s w w⇩1 w⇩2
    assume eval_val1:"P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨Val w⇩1,s⟩"
      and eval_val2:"P,E ⊢ ⟨e⇩2,s⟩ ⇒ ⟨Val w⇩2,s⇩2'⟩"
      and binop':"binop(bop,w⇩1,w⇩2) = Some w" and e2':"e⇩2' = Val w"
    from IH1[OF eval_val1 wte1 sconf] have w1:"v⇩1 = w⇩1" and s:"s = s⇩1" by simp_all
    with wf eval_val1 wte1 sconf have "P,E ⊢ s⇩1 √"
      by(fastforce intro:eval_preserves_sconf)
    from IH2[OF eval_val2[simplified s] wte2 this] have "v⇩2 = w⇩2" and s2:"s⇩2 = s⇩2'"
      by simp_all
    with w1 binop binop' have "w = v" by simp
    with e2' s2 show "Val v = e⇩2' ∧ s⇩2 = s⇩2'" by simp
  next
    fix e assume eval_throw:"P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨throw e,s⇩2'⟩"
    from IH1[OF eval_throw wte1 sconf] show "Val v = e⇩2' ∧ s⇩2 = s⇩2'" by simp
  next
    fix e s w 
    assume eval_val:"P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨Val w,s⟩"
      and eval_throw:"P,E ⊢ ⟨e⇩2,s⟩ ⇒ ⟨throw e,s⇩2'⟩"
    from IH1[OF eval_val wte1 sconf] have s:"s = s⇩1" by simp_all
    with wf eval_val wte1 sconf have "P,E ⊢ s⇩1 √"
      by(fastforce intro:eval_preserves_sconf)
    from IH2[OF eval_throw[simplified s] wte2 this] show "Val v = e⇩2' ∧ s⇩2 = s⇩2'"
      by simp
  qed
next
  case (BinOpThrow1 E e⇩1 s⇩0 e s⇩1 bop e⇩2 e⇩2' s⇩2 T)
   have eval:"P,E ⊢ ⟨e⇩1 «bop» e⇩2,s⇩0⟩ ⇒ ⟨e⇩2',s⇩2⟩"
     and wt:"P,E ⊢ e⇩1 «bop» e⇩2 :: T" and sconf:"P,E ⊢ s⇩0 √"
     and IH:"⋀ei si T. ⟦P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨ei,si⟩; P,E ⊢ e⇩1 :: T; P,E ⊢ s⇩0 √⟧
                     ⟹ throw e = ei ∧ s⇩1 = si" by fact+
   from wt obtain T⇩1 T⇩2 where wte1:"P,E ⊢ e⇩1 :: T⇩1" by auto
  from eval show ?case
  proof(rule eval_cases)
    fix s w w⇩1 w⇩2
    assume eval_val:"P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨Val w⇩1,s⟩"
    from IH[OF eval_val wte1 sconf] show "throw e = e⇩2' ∧ s⇩1 = s⇩2" by simp
  next
    fix e' 
    assume eval_throw:"P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨throw e',s⇩2⟩" and throw:"e⇩2' = throw e'"
    from IH[OF eval_throw wte1 sconf] throw show "throw e = e⇩2' ∧ s⇩1 = s⇩2" by simp
  next
    fix e s w 
    assume eval_val:"P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨Val w,s⟩"
    from IH[OF eval_val wte1 sconf] show "throw e = e⇩2' ∧ s⇩1 = s⇩2" by simp
  qed
next
  case (BinOpThrow2 E e⇩1 s⇩0 v⇩1 s⇩1 e⇩2 e s⇩2 bop e⇩2' s⇩2' T)
  have eval:"P,E ⊢ ⟨e⇩1 «bop» e⇩2,s⇩0⟩ ⇒ ⟨e⇩2',s⇩2'⟩"
    and wt:"P,E ⊢ e⇩1 «bop» e⇩2 :: T" and sconf:"P,E ⊢ s⇩0 √"
    and IH1:"⋀ei si T. ⟦P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨ei,si⟩; P,E ⊢ e⇩1 :: T; P,E ⊢ s⇩0 √⟧
                    ⟹ Val v⇩1 = ei ∧ s⇩1 = si"
    and IH2:"⋀ei si T. ⟦P,E ⊢ ⟨e⇩2,s⇩1⟩ ⇒ ⟨ei,si⟩; P,E ⊢ e⇩2 :: T; P,E ⊢ s⇩1 √⟧
                    ⟹ throw e = ei ∧ s⇩2 = si" by fact+
  from wt obtain T⇩1 T⇩2 where wte1:"P,E ⊢ e⇩1 :: T⇩1" and wte2:"P,E ⊢ e⇩2 :: T⇩2"
    by auto
  from eval show ?case
  proof(rule eval_cases)
    fix s w w⇩1 w⇩2
    assume eval_val1:"P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨Val w⇩1,s⟩"
      and eval_val2:"P,E ⊢ ⟨e⇩2,s⟩ ⇒ ⟨Val w⇩2,s⇩2'⟩"
    from IH1[OF eval_val1 wte1 sconf] have s:"s = s⇩1" by simp_all
    with wf eval_val1 wte1 sconf have "P,E ⊢ s⇩1 √"
      by(fastforce intro:eval_preserves_sconf)
    from IH2[OF eval_val2[simplified s] wte2 this] show "throw e = e⇩2' ∧ s⇩2 = s⇩2'"
      by simp
  next
    fix e' 
    assume eval_throw:"P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨throw e',s⇩2'⟩"
    from IH1[OF eval_throw wte1 sconf] show "throw e = e⇩2' ∧ s⇩2 = s⇩2'" by simp
  next
    fix e' s w 
    assume eval_val:"P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨Val w,s⟩"
      and eval_throw:"P,E ⊢ ⟨e⇩2,s⟩ ⇒ ⟨throw e',s⇩2'⟩"
      and throw:"e⇩2' = throw e'"
    from IH1[OF eval_val wte1 sconf] have s:"s = s⇩1" by simp_all
    with wf eval_val wte1 sconf have "P,E ⊢ s⇩1 √"
      by(fastforce intro:eval_preserves_sconf)
    from IH2[OF eval_throw[simplified s] wte2 this] throw
    show "throw e = e⇩2' ∧ s⇩2 = s⇩2'"
      by simp
  qed
next
  case Var thus ?case by(auto elim: eval_cases)    
next
  case (LAss E e s⇩0 v h l V T v' l' e⇩2 s⇩2 T')
  have eval:"P,E ⊢ ⟨V:=e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩"
    and env:"E V = Some T" and casts:"P ⊢ T casts v to v'" and l':"l' = l(V ↦ v')"
    and wt:"P,E ⊢ V:=e :: T'" and sconf:"P,E ⊢ s⇩0 √"
    and IH:"⋀e⇩2 s⇩2 T. ⟦P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩; P,E ⊢ e :: T; P,E ⊢ s⇩0 √⟧
                    ⟹ Val v = e⇩2 ∧ (h,l) = s⇩2" by fact+
  from wt env obtain T'' where wte:"P,E ⊢ e :: T''" and leq:"P ⊢ T'' ≤ T" by auto
  from eval show ?case
  proof(rule eval_cases)
    fix U h' l'' w w'
    assume eval_val:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨Val w,(h',l'')⟩" and env':"E V = Some U"
      and casts':"P ⊢ U casts w to w'" and e2:"e⇩2 = Val w'" 
      and s2:"s⇩2 = (h',l''(V ↦ w'))"
    from env env' have UeqT:"U = T" by simp
    from IH[OF eval_val wte sconf] have eq:"v = w ∧ h = h' ∧ l = l''" by simp
    from sconf env have "is_type P T"
      by(clarsimp simp:sconf_def envconf_def)
    with casts casts' eq UeqT wte leq eval_val sconf wf have "v' = w'"
      by(auto intro:casts_casts_eq_result)
    with e2 s2 l' eq show "Val v' = e⇩2 ∧ (h, l') = s⇩2" by simp
  next
    fix e' assume eval_throw:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw e',s⇩2⟩"
    from IH[OF eval_throw wte sconf] show "Val v' = e⇩2 ∧ (h, l') = s⇩2" by simp
  qed
next
  case (LAssThrow E e s⇩0 e' s⇩1 V e⇩2 s⇩2 T)
  have eval:"P,E ⊢ ⟨V:=e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩"
    and wt:"P,E ⊢ V:=e :: T" and sconf:"P,E ⊢ s⇩0 √"
    and IH:"⋀e⇩2 s⇩2 T. ⟦P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩; P,E ⊢ e :: T; P,E ⊢ s⇩0 √⟧
                    ⟹ throw e' = e⇩2 ∧ s⇩1 = s⇩2" by fact+
  from wt obtain T'' where wte:"P,E ⊢ e :: T''" by auto
  from eval show ?case
  proof(rule eval_cases)
    fix U h' l'' w w'
    assume eval_val:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨Val w,(h',l'')⟩"
    from IH[OF eval_val wte sconf] show "throw e' = e⇩2 ∧ s⇩1 = s⇩2" by simp
  next
    fix ex 
    assume eval_throw:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw ex,s⇩2⟩" and e2:"e⇩2 = throw ex"
    from IH[OF eval_throw wte sconf] e2 show "throw e' = e⇩2 ∧ s⇩1 = s⇩2" by simp
  qed
next
  case (FAcc E e s⇩0 a Cs' h l D S Ds Cs fs F v e⇩2 s⇩2 T)
  have eval:"P,E ⊢ ⟨e∙F{Cs},s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩"
    and eval':"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref (a, Cs'),(h,l)⟩"
    and h:"h a = Some(D,S)" and Ds:"Ds = Cs'@⇩pCs"
    and S:"(Ds,fs) ∈ S" and fs:"fs F = Some v"
    and wt:"P,E ⊢ e∙F{Cs} :: T" and sconf:"P,E ⊢ s⇩0 √"
    and IH:"⋀e⇩2 s⇩2 T. ⟦P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩; P,E ⊢ e :: T; P,E ⊢ s⇩0 √⟧
                    ⟹ ref (a, Cs') = e⇩2 ∧ (h,l) = s⇩2" by fact+
  from wt obtain C where wte:"P,E ⊢ e :: Class C" by auto
  from eval_preserves_sconf[OF wf eval' wte sconf] h have oconf:"P,h ⊢ (D,S) √"
    by(simp add:sconf_def hconf_def)
  from eval show ?case
  proof(rule eval_cases)
    fix Xs' D' S' a' fs' h' l' v'
    assume eval_ref:"P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref(a',Xs'),(h',l')⟩"
    and h':"h' a' = Some(D',S')" and S':"(Xs'@⇩pCs,fs') ∈ S'"
    and fs':"fs' F = Some v'" and e2:"e⇩2 = Val v'" and s2:"s⇩2 = (h',l')"
    from IH[OF eval_ref wte sconf] h h'
    have eq:"a = a' ∧ Cs' = Xs' ∧ h = h' ∧ l = l' ∧ D = D' ∧ S = S'" by simp
    with oconf S S'