Theory Progress

(*  Title:       CoreC++

    Author:      Daniel Wasserrab
    Maintainer:  Daniel Wasserrab <wasserra at fmi.uni-passau.de>

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

section ‹Progress of Small Step Semantics›

theory Progress imports Equivalence DefAss Conform begin


subsection ‹Some pre-definitions›

lemma final_refE:
  " P,E,h  e : Class C; final e;
    r. e = ref r  Q;
    r. e = Throw r  Q   Q"
by (simp add:final_def,auto,case_tac v,auto)


lemma finalRefE:
  " P,E,h  e : T; is_refT T; final e;
  e = null  Q;
  r. e = ref r  Q;
  r. e = Throw r  Q  Q"

apply (cases T)
apply (simp add:is_refT_def)+
 apply (simp add:final_def)
 apply (erule disjE)
  apply clarsimp
 apply (erule exE)+
apply fastforce
apply (auto simp:final_def is_refT_def)
apply (case_tac v)
apply auto
done


lemma subE:
  " P  T  T'; is_type P T'; wf_prog wf_md P;
      T = T'; C. T  Class C   Q;
     C D.  T = Class C; T' = Class D; P  Path C to D unique   Q;
     C.  T = NT; T' = Class C   Q   Q"

apply(cases T')
apply auto
apply(drule_tac T = "T" in widen_Class)
apply auto
done


lemma assumes wf:"wf_prog wf_md P"
  and typeof:" P  typeofh v = Some T'"
  and type:"is_type P T"
shows sub_casts:"P  T'  T  v'. P  T casts v to v'"

proof(erule subE)
  from type show "is_type P T" .
next
  from wf show "wf_prog wf_md P" .
next
  assume "T' = T" and "C. T'  Class C"
  thus "v'. P  T casts v to v'" by(fastforce intro:casts_prim)
next
  fix C D
  assume T':"T' = Class C" and T:"T = Class D"
    and path_unique:"P  Path C to D unique"
  from T' typeof obtain a Cs where v:"v = Ref(a,Cs)" and last:"last Cs = C"
    by(auto dest!:typeof_Class_Subo)
  from last path_unique obtain Cs' where "P  Path last Cs to D via Cs'"
    by(auto simp:path_unique_def path_via_def)
  hence "P  Class D casts Ref(a,Cs) to Ref(a,Cs@pCs')"
    by -(rule casts_ref,simp_all)
  with T v show "v'. P  T casts v to v'" by auto
next
  fix C
  assume "T' = NT" and T:"T = Class C"
  with typeof have "v = Null" by simp
  with T show "v'. P  T casts v to v'" by(fastforce intro:casts_null)
qed



text‹Derivation of new induction scheme for well typing:›

inductive
  WTrt' :: "[prog,env,heap,expr,     ty     ]  bool"
        ("_,_,_  _ :'' _"   [51,51,51]50)
  and WTrts':: "[prog,env,heap,expr list,ty list]  bool"
        ("_,_,_  _ [:''] _" [51,51,51]50)
  for P :: prog
where
  "is_class P C   P,E,h  new C :' Class C"
| "is_class P C; P,E,h  e :' T; is_refT T 
    P,E,h  Cast C e :' Class C"
| "is_class P C; P,E,h  e :' T; is_refT T 
    P,E,h  Ce :' Class C"
| "P  typeofh v = Some T  P,E,h  Val v :' T"
| "E V = Some T    P,E,h  Var V :' T"
| " P,E,h  e1 :' T1;  P,E,h  e2 :' T2;
    case bop of Eq  T = Boolean
    | Add  T1 = Integer  T2 = Integer  T = Integer 
    P,E,h  e1 «bop» e2 :' T"
| " P,E,h  Var V :' T; P,E,h  e :' T' ⌦‹V ≠ This›; P  T'  T 
    P,E,h  V:=e :' T"
| "P,E,h  e :' Class C; Cs  []; P  C has least F:T via Cs 
   P,E,h  eF{Cs} :' T"
| "P,E,h  e :' NT  P,E,h  eF{Cs} :' T"
| "P,E,h  e1 :' Class C; Cs  []; P  C has least F:T via Cs;
    P,E,h  e2 :' T'; P  T'  T  
   P,E,h  e1F{Cs}:=e2 :' T"
| " P,E,h  e1:'NT; P,E,h  e2 :' T'; P  T'  T  
    P,E,h  e1F{Cs}:=e2 :' T"
| " P,E,h  e :' Class C;  P  C has least M = (Ts,T,m) via Cs;
    P,E,h  es [:'] Ts'; P  Ts' [≤] Ts 
     P,E,h  eM(es) :' T" 
| " P,E,h  e :' Class C'; P  Path C' to C unique;
    P  C has least M = (Ts,T,m) via Cs; 
    P,E,h  es [:'] Ts'; P  Ts' [≤] Ts 
     P,E,h  e∙(C::)M(es) :' T"
| "P,E,h  e :' NT; P,E,h  es [:'] Ts  P,E,h  Call e Copt M es :' T"
| " P  typeofh v = Some T'; P,E(VT),h  e2 :' T2; P  T'  T; is_type P T 
     P,E,h  {V:T := Val v; e2} :' T2"
| " P,E(VT),h  e :' T'; ¬ assigned V e; is_type P T 
     P,E,h  {V:T; e} :' T'"
| " P,E,h  e1 :' T1; P,E,h  e2 :' T2     P,E,h  e1;;e2 :' T2"
| " P,E,h  e :' Boolean;  P,E,h  e1:' T;  P,E,h  e2:' T 
    P,E,h  if (e) e1 else e2 :' T"
| " P,E,h  e :' Boolean;  P,E,h  c:' T 
     P,E,h  while(e) c :' Void"
| " P,E,h  e :' T'; is_refT T'    P,E,h  throw e :' T"

| "P,E,h  [] [:'] []"
| " P,E,h  e :' T;  P,E,h  es [:'] Ts    P,E,h  e#es [:'] T#Ts"



lemmas WTrt'_induct = WTrt'_WTrts'.induct [split_format (complete)]
  and WTrt'_inducts = WTrt'_WTrts'.inducts [split_format (complete)]

inductive_cases WTrt'_elim_cases[elim!]:
  "P,E,h  V :=e :' T"


text‹... and some easy consequences:›

lemma [iff]: "P,E,h  e1;;e2 :' T2 = (T1. P,E,h  e1:' T1  P,E,h  e2:' T2)"

apply(rule iffI)
apply (auto elim: WTrt'.cases intro!:WTrt'_WTrts'.intros)
done


lemma [iff]: "P,E,h  Val v :' T = (P  typeofh v = Some T)"

apply(rule iffI)
apply (auto elim: WTrt'.cases intro!:WTrt'_WTrts'.intros)
done


lemma [iff]: "P,E,h  Var V :' T = (E V = Some T)"

apply(rule iffI)
apply (auto elim: WTrt'.cases intro!:WTrt'_WTrts'.intros)
done



lemma wt_wt': "P,E,h  e : T  P,E,h  e :' T"
and wts_wts': "P,E,h  es [:] Ts  P,E,h  es [:'] Ts"

proof (induct rule:WTrt_inducts)
  case (WTrtBlock E V T h e T')
  thus ?case
    apply(case_tac "assigned V e")
    apply(auto intro:WTrt'_WTrts'.intros 
          simp add:fun_upd_same assigned_def simp del:fun_upd_apply)
    done
qed(auto intro:WTrt'_WTrts'.intros simp del:fun_upd_apply)


lemma wt'_wt: "P,E,h  e :' T  P,E,h  e : T"
and wts'_wts: "P,E,h  es [:'] Ts  P,E,h  es [:] Ts"

apply (induct rule:WTrt'_inducts)
apply (fastforce intro: WTrt_WTrts.intros)+
done



corollary wt'_iff_wt: "(P,E,h  e :' T) = (P,E,h  e : T)"
by(blast intro:wt_wt' wt'_wt)


corollary wts'_iff_wts: "(P,E,h  es [:'] Ts) = (P,E,h  es [:] Ts)"
by(blast intro:wts_wts' wts'_wts)

lemmas WTrt_inducts2 = WTrt'_inducts [unfolded wt'_iff_wt wts'_iff_wts,
  case_names WTrtNew WTrtDynCast WTrtStaticCast WTrtVal WTrtVar WTrtBinOp 
  WTrtLAss WTrtFAcc WTrtFAccNT WTrtFAss WTrtFAssNT WTrtCall WTrtStaticCall WTrtCallNT 
  WTrtInitBlock WTrtBlock WTrtSeq WTrtCond WTrtWhile WTrtThrow 
  WTrtNil WTrtCons, consumes 1]


subsection‹The theorem progress›


lemma mdc_leq_dyn_type:
"P,E,h  e : T  
  C a Cs D S. T = Class C  e = ref(a,Cs)  h a = Some(D,S)  P  D * C"
and "P,E,h  es [:] Ts 
  T Ts' e es' C a Cs D S. Ts = T#Ts'  es = e#es'  
                           T = Class C  e = ref(a,Cs)  h a = Some(D,S)
       P  D * C"

proof (induct rule:WTrt_inducts2)
  case (WTrtVal h v T E)
  have type:"P  typeofh v = Some T" by fact
  { fix C a Cs D S
    assume "T = Class C" and "Val v = ref(a,Cs)" and "h a = Some(D,S)"
    with type have "Subobjs P D Cs" and "C = last Cs" by (auto split:if_split_asm)
    hence "P  D * C" by simp (rule Subobjs_subclass) }
  thus ?case by blast
qed auto



lemma appendPath_append_last:
  assumes notempty:"Ds  []" 
  shows"(Cs @p Ds) @p [last Ds] = (Cs @p Ds)"

proof -
  have "last Cs = hd Ds  last (Cs @ tl Ds) = last Ds"
  proof(cases "tl Ds = []")
    case True
    assume last:"last Cs = hd Ds"
    with True notempty have "Ds = [last Cs]" by (fastforce dest:hd_Cons_tl)
    hence "last Ds = last Cs" by simp
    with True show ?thesis by simp
  next
    case False
    assume last:"last Cs = hd Ds"
    from notempty False have "last (tl Ds) = last Ds"
      by -(drule hd_Cons_tl,drule_tac x="hd Ds" in last_ConsR,simp)
    with False show ?thesis by simp
  qed
  thus ?thesis by(simp add:appendPath_def)
qed




theorem assumes wf: "wwf_prog P"
shows progress: "P,E,h  e : T 
 (l.  P  h ; P  E ; 𝒟 e dom l; ¬ final e   e' s'. P,E  e,(h,l)  e',s')"
and "P,E,h  es [:] Ts 
 (l.  P  h ; P  E ; 𝒟s es dom l; ¬ finals es   es' s'. P,E  es,(h,l) [→] es',s')"
proof (induct rule:WTrt_inducts2)
  case (WTrtNew C E h)
  show ?case
  proof cases
    assume "a. h a = None"
    with WTrtNew show ?thesis
      by (fastforce del:exE intro!:RedNew simp:new_Addr_def)
  next
    assume "¬(a. h a = None)"
    with WTrtNew show ?thesis
      by(fastforce intro:RedNewFail simp add:new_Addr_def)
  qed
next
  case (WTrtDynCast C E h e T)
  have wte: "P,E,h  e : T" and refT: "is_refT T" and "class": "is_class P C"
    and IH: "l. P  h ; P  E ; 𝒟 e dom l; ¬ final e
                 e' s'. P,E  e,(h,l)  e',s'"
    and D: "𝒟 (Cast C e) dom l" 
    and hconf: "P  h " and envconf:"P  E " by fact+
  from D have De: "𝒟 e dom l" by auto
  show ?case
  proof cases
    assume "final e"
    with wte refT show ?thesis
    proof (rule finalRefE)
      assume "e = null" thus ?case by(fastforce intro:RedDynCastNull)
    next
      fix r assume "e = ref r"
      then obtain a Cs where ref:"e = ref(a,Cs)" by (cases r) auto
      with wte obtain D S where h:"h a = Some(D,S)" by auto
      show ?thesis
      proof (cases "P  Path D to C unique")
        case True
        then obtain Cs' where path:"P  Path D to C via Cs'"
          by (fastforce simp:path_via_def path_unique_def)
        then obtain Ds where "Ds = appendPath Cs Cs'" by simp
        with h path True ref show ?thesis by (fastforce intro:RedDynCast)
      next
        case False
        hence path_not_unique:"¬ P  Path D to C unique" .
        show ?thesis
        proof(cases "P  Path last Cs to C unique")
          case True
          then obtain Cs' where "P  Path last Cs to C via Cs'"
            by(auto simp:path_via_def path_unique_def)
          with True ref show ?thesis by(fastforce intro:RedStaticUpDynCast)
        next
          case False
          hence path_not_unique':"¬ P  Path last Cs to C unique" .
          thus ?thesis
          proof(cases "C  set Cs")
            case False
            then obtain Ds Ds' where "Cs = Ds@[C]@Ds'"
              by (auto simp:in_set_conv_decomp)
            with ref show ?thesis by(fastforce intro:RedStaticDownDynCast)
          next
            case True
            with path_not_unique path_not_unique' h ref 
            show ?thesis by (fastforce intro:RedDynCastFail)
          qed
        qed
      qed
    next
      fix r assume "e = Throw r"
      thus ?thesis by(blast intro!:red_reds.DynCastThrow)
    qed
  next
    assume nf: "¬ final e"
    from IH[OF hconf envconf De nf] show ?thesis by (blast intro:DynCastRed)
  qed
next
  case (WTrtStaticCast C E h e T)
  have wte: "P,E,h  e : T" and refT: "is_refT T" and "class": "is_class P C"
   and IH: "l. P  h ; P  E ; 𝒟 e dom l; ¬ final e
                 e' s'. P,E  e,(h,l)  e',s'"
   and D: "𝒟 (Ce) dom l" 
    and hconf: "P  h " and envconf:"P  E " by fact+
  from D have De: "𝒟 e dom l" by auto
  show ?case
  proof cases
    assume "final e"
    with wte refT show ?thesis
    proof (rule finalRefE)
      assume "e = null" with "class" show ?case by(fastforce intro:RedStaticCastNull)
    next
      fix r assume "e = ref r"
      then obtain a Cs where ref:"e = ref(a,Cs)" by (cases r) auto
      with wte wf have "class":"is_class P (last Cs)" 
        by (auto intro:Subobj_last_isClass split:if_split_asm)
      show ?thesis
      proof(cases "P  (last Cs) * C")
        case True
        with "class" wf obtain Cs'  where "P  Path last Cs to C via Cs'"
          by(fastforce dest:leq_implies_path)
        with True ref show ?thesis by(fastforce intro:RedStaticUpCast)
      next
        case False
        have notleq:"¬ P  last Cs * C" by fact
        thus ?thesis
        proof(cases "C  set Cs")
          case False
          then obtain Ds Ds' where "Cs = Ds@[C]@Ds'"
            by (auto simp:in_set_conv_decomp)
          with ref show ?thesis
            by(fastforce intro:RedStaticDownCast)
        next
          case True
          with ref notleq show ?thesis by (fastforce intro:RedStaticCastFail)
        qed
      qed
    next
      fix r assume "e = Throw r"
      thus ?thesis by(blast intro!:red_reds.StaticCastThrow)
    qed
  next
    assume nf: "¬ final e"
    from IH[OF hconf envconf De nf] show ?thesis by (blast intro:StaticCastRed)
  qed
next
  case WTrtVal thus ?case by(simp add:final_def)
next
  case WTrtVar thus ?case by(fastforce intro:RedVar simp:hyper_isin_def)
next
  case (WTrtBinOp E h e1 T1 e2 T2 bop T')
  have bop:"case bop of Eq  T' = Boolean
                      | Add  T1 = Integer  T2 = Integer  T' = Integer"
    and wte1:"P,E,h  e1 : T1" and wte2:"P,E,h  e2 : T2" by fact+
  show ?case
  proof cases
    assume "final e1"
    thus ?thesis
    proof (rule finalE)
      fix v1 assume e1 [simp]:"e1 = Val v1"
      show ?thesis
      proof cases
        assume "final e2"
        thus ?thesis
        proof (rule finalE)
          fix v2 assume e2 [simp]:"e2 = Val v2"
          show ?thesis
          proof (cases bop)
            assume "bop = Eq"
            thus ?thesis using WTrtBinOp by(fastforce intro:RedBinOp)
          next
            assume Add:"bop = Add"
            with e1 e2 wte1 wte2 bop obtain i1 i2 
              where "v1 = Intg i1" and "v2 = Intg i2"
              by (auto dest!:typeof_Integer)
            with Add obtain v where "binop(bop,v1,v2) = Some v" by simp
            with e1 e2 show ?thesis by (fastforce intro:RedBinOp)
          qed
        next
          fix a assume "e2 = Throw a"
          thus ?thesis by(auto intro:red_reds.BinOpThrow2)
        qed
      next
        assume "¬ final e2" with WTrtBinOp show ?thesis
          by simp (fast intro!:BinOpRed2)
      qed
    next
      fix r assume "e1 = Throw r"
      thus ?thesis by simp (fast intro:red_reds.BinOpThrow1)
    qed
  next
    assume "¬ final e1" with WTrtBinOp show ?thesis
      by simp (fast intro:BinOpRed1)
  qed
next
  case (WTrtLAss E h V T e T')
  have wte:"P,E,h  e : T'"
    and wtvar:"P,E,h  Var V : T"
    and sub:"P  T'  T"
    and envconf:"P  E " by fact+
  from envconf wtvar have type:"is_type P T" by(auto simp:envconf_def)
  show ?case
  proof cases
    assume fin:"final e"
    from fin show ?case
    proof (rule finalE)
      fix v assume e:"e = Val v"
      from sub type wf show ?case
      proof(rule subE)
        assume eq:"T' = T" and "C. T'  Class C"
        hence "P  T casts v to v"
          by simp(rule casts_prim)
        with wte wtvar eq e show ?thesis
          by(auto intro!:RedLAss)
      next
        fix C D
        assume T':"T' = Class C" and T:"T = Class D"
          and path_unique:"P  Path C to D unique"
        from wte e T' obtain a Cs where ref:"e = ref(a,Cs)"
          and last:"last Cs = C" 
          by (auto dest!:typeof_Class_Subo)
        from path_unique obtain Cs' where path_via:"P  Path C to D via Cs'"
          by(auto simp:path_unique_def path_via_def)
        with last have "P  Class D casts Ref(a,Cs) to Ref(a,Cs@pCs')"
          by (fastforce intro:casts_ref simp:path_via_def)
        with wte wtvar T ref show ?thesis
          by(auto intro!:RedLAss)
      next
        fix C
        assume T':"T' = NT" and T:"T = Class C"
        with wte e have null:"e = null" by auto
        have "P  Class C casts Null to Null"
          by -(rule casts_null)
        with wte wtvar T null show ?thesis
          by(auto intro!:RedLAss)
      qed
    next
      fix r assume "e = Throw r"
      thus ?thesis by(fastforce intro:red_reds.LAssThrow)
    qed
  next
    assume "¬ final e" with WTrtLAss show ?thesis
      by simp (fast intro:LAssRed)
  qed
next
  case (WTrtFAcc E h e C Cs F T)
  have wte: "P,E,h  e : Class C" 
    and field: "P  C has least F:T via Cs"
    and notemptyCs:"Cs  []"
    and hconf: "P  h " by fact+
  show ?case
  proof cases
    assume "final e"
    with wte show ?thesis
    proof (rule final_refE)
      fix r assume e: "e = ref r"
      then obtain a Cs' where ref:"e = ref(a,Cs')" by (cases r) auto
      with wte obtain D S where h:"h a = Some(D,S)" and suboD:"Subobjs P D Cs'"
        and last:"last Cs' = C"
        by (fastforce split:if_split_asm)
      from field obtain Bs fs ms
        where "class": "class P (last Cs) = Some(Bs,fs,ms)"
        and fs:"map_of fs F = Some T"
        by (fastforce simp:LeastFieldDecl_def FieldDecls_def)
      obtain Ds where Ds:"Ds = Cs'@pCs" by simp
      with notemptyCs "class" have class':"class P (last Ds) = Some(Bs,fs,ms)"
        by (drule_tac Cs'="Cs'" in appendPath_last) simp
      from field suboD last Ds wf have subo:"Subobjs P D Ds"
        by(fastforce intro:Subobjs_appendPath simp:LeastFieldDecl_def FieldDecls_def)
      with hconf h have "P,h  (D,S) " by (auto simp:hconf_def)
      with class' subo obtain fs' where S:"(Ds,fs')  S"
        and "P,h  fs' (:≤) map_of fs"
        apply (auto simp:oconf_def)
        apply (erule_tac x="Ds" in allE)
        apply auto
        apply (erule_tac x="Ds" in allE)
        apply (erule_tac x="fs'" in allE)
        apply auto
        done
      with fs obtain v where "fs' F = Some v"
        by (fastforce simp:fconf_def)
      with h last Ds S
      have "P,E  (ref (a,Cs'))F{Cs}, (h,l)  Val v,(h,l)"
        by (fastforce intro:RedFAcc)
      with ref show ?thesis by blast
    next
      fix r assume "e = Throw r"
      thus ?thesis by(fastforce intro:red_reds.FAccThrow)
    qed
  next
    assume "¬ final e" with WTrtFAcc show ?thesis
      by(fastforce intro!:FAccRed)
  qed
next
  case (WTrtFAccNT E h e F Cs T)
  show ?case
  proof cases
    assume "final e"  ― ‹@{term e} is @{term null} or @{term throw}
    with WTrtFAccNT show ?thesis
      by(fastforce simp:final_def intro: RedFAccNull red_reds.FAccThrow 
                  dest!:typeof_NT)
  next
    assume "¬ final e" ― ‹@{term e} reduces by IH›
    with WTrtFAccNT show ?thesis by simp (fast intro:FAccRed)
  qed
next
  case (WTrtFAss E h e1 C Cs F T e2 T')
  have wte1:"P,E,h  e1 : Class C"
    and wte2:"P,E,h  e2 : T'"
    and field:"P  C has least F:T via Cs" 
    and notemptyCs:"Cs  []"
    and sub:"P  T'  T"
    and hconf:"P  h " by fact+
  from field wf have type:"is_type P T" by(rule least_field_is_type)
  show ?case
  proof cases
    assume "final e1"
    with wte1 show ?thesis
    proof (rule final_refE)
      fix r assume e1: "e1 = ref r"
      show ?thesis
      proof cases
        assume "final e2"
        thus ?thesis
        proof (rule finalE)
          fix v assume e2:"e2 = Val v"
          from e1 obtain a Cs' where ref:"e1 = ref(a,Cs')" by (cases r) auto
          with wte1 obtain D S where h:"h a = Some(D,S)" 
            and suboD:"Subobjs P D Cs'" and last:"last Cs' = C"
            by (fastforce split:if_split_asm)
          from field obtain Bs fs ms
            where "class": "class P (last Cs) = Some(Bs,fs,ms)"
            and fs:"map_of fs F = Some T"
            by (fastforce simp:LeastFieldDecl_def FieldDecls_def)
          obtain Ds where Ds:"Ds = Cs'@pCs" by simp
          with notemptyCs "class" have class':"class P (last Ds) = Some(Bs,fs,ms)"
            by (drule_tac Cs'="Cs'" in appendPath_last) simp
          from field suboD last Ds wf have subo:"Subobjs P D Ds"
            by(fastforce intro:Subobjs_appendPath 
              simp:LeastFieldDecl_def FieldDecls_def)
          with hconf h have "P,h  (D,S) " by (auto simp:hconf_def)
          with class' subo obtain fs' where S:"(Ds,fs')  S"
            by (auto simp:oconf_def)
          from sub type wf show ?thesis
          proof(rule subE)
            assume eq:"T' = T" and "C. T'  Class C"
            hence "P  T casts v to v"
              by simp(rule casts_prim)
            with h last field Ds notemptyCs S eq
            have "P,E  (ref (a,Cs'))F{Cs}:=(Val v), (h,l)  
              Val v, (h(a  (D,insert (Ds,fs'(Fv)) (S -  {(Ds,fs')}))),l)"
              by (fastforce intro:RedFAss)
            with ref e2 show ?thesis by blast
          next
            fix C' D'
            assume T':"T' = Class C'" and T:"T = Class D'"
            and path_unique:"P  Path C' to D' unique"
            from wte2 e2 T' obtain a' Cs'' where ref2:"e2 = ref(a',Cs'')"
              and last':"last Cs'' = C'"
              by (auto dest!:typeof_Class_Subo)
            from path_unique obtain Ds' where "P  Path C' to D' via Ds'"
              by(auto simp:path_via_def path_unique_def)
            with last' 
            have casts:"P  Class D' casts Ref(a',Cs'') to Ref(a',Cs''@pDs')"
              by (fastforce intro:casts_ref simp:path_via_def)
            obtain v' where "v' = Ref(a',Cs''@pDs')" by simp
            with h last field Ds notemptyCs S ref e2 ref2 T casts
            have "P,E  (ref (a,Cs'))F{Cs}:=(Val v), (h,l)  
                        Val v',(h(a  (D,insert (Ds,fs'(Fv'))(S-{(Ds,fs')}))),l)"
              by (fastforce intro:RedFAss)
            with ref e2 show ?thesis by blast
          next
            fix C'
            assume T':"T' = NT" and T:"T = Class C'"
            from e2 wte2 T' have null:"e2 = null" by auto
            have casts:"P  Class C' casts Null to Null"
              by -(rule casts_null)
            obtain v' where "v' = Null" by simp
            with h last field Ds notemptyCs S ref e2 null T casts
            have "P,E  (ref (a,Cs'))F{Cs}:=(Val v), (h,l)  
                  Val v', (h(a  (D,insert (Ds,fs'(Fv')) (S -  {(Ds,fs')}))),l)"
              by (fastforce intro:RedFAss)
            with ref e2 show ?thesis by blast
          qed
        next
          fix r assume "e2 = Throw r"
          thus ?thesis using e1 by(fastforce intro:red_reds.FAssThrow2)
        qed
      next
        assume "¬ final e2" with WTrtFAss e1 show ?thesis
          by simp (fast intro!:FAssRed2)
      qed
    next
      fix r assume "e1 = Throw r"
      thus ?thesis by(fastforce intro:red_reds.FAssThrow1)
    qed
  next
    assume "¬ final e1" with WTrtFAss show ?thesis
      by simp (blast intro!:FAssRed1)
  qed
next
  case (WTrtFAssNT E h e1 e2 T' T F Cs)
  show ?case
  proof cases
    assume e1: "final e1"  ― ‹@{term e1} is @{term null} or @{term throw}
    show ?thesis
    proof cases
      assume "final e2"  ― ‹@{term e2} is @{term Val} or @{term throw}
      with WTrtFAssNT e1 show ?thesis
        by(fastforce simp:final_def intro:RedFAssNull red_reds.FAssThrow1 
                                         red_reds.FAssThrow2 dest!:typeof_NT)
    next
      assume  "¬ final e2" ― ‹@{term e2} reduces by IH›
      with WTrtFAssNT e1 show ?thesis
        by (fastforce simp:final_def intro!:red_reds.FAssRed2 red_reds.FAssThrow1)
    qed
  next
    assume "¬ final e1" ― ‹@{term e1} reduces by IH›
    with WTrtFAssNT show ?thesis by (fastforce intro:FAssRed1)
  qed
next
  case (WTrtCall E h e C M Ts T pns body Cs es Ts')
  have wte: "P,E,h  e : Class C"
    and "method":"P  C has least M = (Ts, T, pns, body) via Cs"
    and wtes: "P,E,h  es [:] Ts'"and sub: "P  Ts' [≤] Ts"
    and IHes: "l. P  h ; P  E ; 𝒟s es dom l; ¬ finals es
              es' s'. P,E  es,(h,l) [→] es',s'"
    and hconf: "P  h " and envconf:"P  E " 
    and D: "𝒟 (eM(es)) dom l" by fact+
  show ?case
  proof cases
    assume final:"final e"
    with wte show ?thesis
    proof (rule final_refE)
      fix r assume ref: "e = ref r"
      show ?thesis
      proof cases
        assume es: "vs. es = map Val vs"
        from ref obtain a Cs' where ref:"e = ref(a,Cs')" by (cases r) auto
        with wte obtain D S where h:"h a = Some(D,S)" and suboD:"Subobjs P D Cs'"
          and last:"last Cs' = C"
          by (fastforce split:if_split_asm)
        from wte ref h have subcls:"P  D * C" by -(drule mdc_leq_dyn_type,auto)
        from "method" have has:"P  C has M = (Ts,T,pns,body) via Cs"
            by(rule has_least_method_has_method)
        from es obtain vs where vs:"es = map Val vs" by auto
        obtain Cs'' Ts'' T' pns' body' where 
          ass:"P  (D,Cs'@pCs) selects M = (Ts'',T',pns',body') via Cs'' 
           length Ts'' = length pns'  length vs = length pns'  P  T'  T"
        proof (cases "Ts'' T' pns' body' Ds. P  D has least M = (Ts'',T',pns',body') via Ds")
          case True
          then obtain Ts'' T' pns' body' Cs'' 
            where least:"P  D has least M = (Ts'',T',pns',body') via Cs''"
            by auto
          hence select:"P  (D,Cs'@pCs) selects M = (Ts'',T',pns',body') via Cs''"
            by(rule dyn_unique)
          from subcls least wf has have "Ts = Ts''" and leq:"P  T'  T"
            by -(drule leq_method_subtypes,simp_all,blast)+
          hence "length Ts = length Ts''" by (simp add:list_all2_iff)
          with sub have "length Ts' = length Ts''" by (simp add:list_all2_iff)
          with WTrts_same_length[OF wtes] vs have length:"length vs = length Ts''"
            by simp
          from has_least_wf_mdecl[OF wf least] 
          have lengthParams:"length Ts'' = length pns'" by (simp add:wf_mdecl_def)
          with length have "length vs = length pns'" by simp
          with select lengthParams leq show ?thesis using that by blast
        next
          case False
          hence non_dyn:"Ts'' T' pns' body' Ds. 
              ¬ P  D has least M = (Ts'',T',pns',body') via Ds" by auto
          from suboD last have path:"P  Path D to C via Cs'" 
            by(simp add:path_via_def)
          from "method" have notempty:"Cs  []" 
            by(fastforce intro!:Subobjs_nonempty 
                        simp:LeastMethodDef_def MethodDefs_def)
          from suboD have "class": "is_class P D" by(rule Subobjs_isClass)
          from suboD last have path:"P  Path D to C via Cs'"
            by(simp add:path_via_def)
          with "method" wf have "P  D has M = (Ts,T,pns,body) via Cs'@pCs"
            by(auto intro:has_path_has has_least_method_has_method)
          with "class" wf obtain Cs'' Ts'' T' pns' body' where overrider:
            "P  (D,Cs'@pCs) has overrider M = (Ts'',T',pns',body') via Cs''"
            by(auto dest!:class_wf simp:is_class_def wf_cdecl_def,blast)
          with non_dyn
          have select:"P  (D,Cs'@pCs) selects M = (Ts'',T',pns',body') via Cs''"
            by-(rule dyn_ambiguous,simp_all)
          from notempty have eq:"(Cs' @p Cs) @p [last Cs] = (Cs' @p Cs)"
            by(rule appendPath_append_last)
          from "method" wf
          have "P  last Cs has least M = (Ts,T,pns,body) via [last Cs]"
            by(auto dest:Subobj_last_isClass intro:Subobjs_Base subobjs_rel
                    simp:LeastMethodDef_def MethodDefs_def)
          with notempty
          have "P  last(Cs'@pCs) has least M = (Ts,T,pns,body) via [last Cs]"
            by -(drule_tac Cs'="Cs'" in appendPath_last,simp)
          with overrider wf eq
          have "(Cs'',(Ts'',T',pns',body'))  MinimalMethodDefs P D M"
            and "P,D  Cs''  Cs'@pCs"
            by(auto simp:FinalOverriderMethodDef_def OverriderMethodDefs_def)
              (drule wf_sees_method_fun,auto)
          with subcls wf notempty has path have "Ts = Ts''" and leq:"P  T'  T"
            by -(drule leq_methods_subtypes,simp_all,blast)+
          hence "length Ts = length Ts''" by (simp add:list_all2_iff)
          with sub have "length Ts' = length Ts''" by (simp add:list_all2_iff)
          with WTrts_same_length[OF wtes] vs have length:"length vs = length Ts''"
            by simp
          from select_method_wf_mdecl[OF wf select]
          have lengthParams:"length Ts'' = length pns'" by (simp add:wf_mdecl_def)
          with length have "length vs = length pns'" by simp
          with select lengthParams leq show ?thesis using that by blast
        qed
        obtain new_body where "case T of Class D  
           new_body = Dblocks(this#pns',Class(last Cs'')#Ts'',Ref(a,Cs'')#vs,body')
    | _  new_body = blocks(this#pns',Class(last Cs'')#Ts'',Ref(a,Cs'')#vs,body')"
          by(cases T) auto
        with h "method" last ass ref vs
          show ?thesis by (auto intro!:exI RedCall)
      next
        assume "¬(vs. es = map Val vs)"
        hence not_all_Val: "¬(e  set es. v. e = Val v)"
          by(simp add:ex_map_conv)
        let ?ves = "takeWhile (λe. v. e = Val v) es"
        let ?rest = "dropWhile (λe. v. e = Val v) es"
        let ?ex = "hd ?rest" let ?rst = "tl ?rest"
        from not_all_Val have nonempty: "?rest  []" by auto
        hence es: "es = ?ves @ ?ex # ?rst" by simp
        have "e  set ?ves. v. e = Val v" by(fastforce dest:set_takeWhileD)
        then obtain vs where ves: "?ves = map Val vs"
          using ex_map_conv by blast
        show ?thesis
        proof cases
          assume "final ?ex"
          moreover from nonempty have "¬(v. ?ex = Val v)"
            by(auto simp:neq_Nil_conv simp del:dropWhile_eq_Nil_conv)
              (simp add:dropWhile_eq_Cons_conv)
          ultimately obtain r' where ex_Throw: "?ex = Throw r'"
            by(fast elim!:finalE)
          show ?thesis using ref es ex_Throw ves
            by(fastforce intro:red_reds.CallThrowParams)
        next
          assume not_fin: "¬ final ?ex"
          have "finals es = finals(?ves @ ?ex # ?rst)" using es
            by(rule arg_cong)
          also have " = finals(?ex # ?rst)" using ves by simp
          finally have "finals es = finals(?ex # ?rst)" .
          hence "¬ finals es" using not_finals_ConsI[OF not_fin] by blast
          thus ?thesis using ref D IHes[OF hconf envconf]
            by(fastforce intro!:CallParams)
        qed
      qed
    next
      fix r assume "e = Throw r"
      with WTrtCall.prems show ?thesis by(fast intro!:red_reds.CallThrowObj)
    qed
  next
    assume "¬ final e"
    with WTrtCall show ?thesis by simp (blast intro!:CallObj)
  qed
next
  case (WTrtStaticCall E h e C' C M Ts T pns body Cs es Ts')
  have 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, pns, body) via Cs"
    and wtes: "P,E,h  es [:] Ts'"and sub: "P  Ts' [≤] Ts"
    and IHes: "l.
              P  h ; envconf P E; 𝒟s es dom l; ¬ finals es
               es' s'. P,E  es,(h,l) [→] es',s'"
    and hconf: "P  h " and envconf:"envconf P E"
    and D: "𝒟 (e∙(C::)M(es)) dom l" by fact+
  show ?case
  proof cases
    assume final:"final e"
    with wte show ?thesis
    proof (rule final_refE)
      fix r assume ref: "e = ref r"
      show ?thesis
      proof cases
        assume es: "vs. es = map Val vs"
        from ref obtain a Cs' where ref:"e = ref(a,Cs')" by (cases r) auto
        with wte have last:"last Cs' = C'"
          by (fastforce split:if_split_asm)
        with path_unique obtain Cs''
          where path_via:"P  Path (last Cs') to C via Cs''"
          by (auto simp add:path_via_def path_unique_def)
        obtain Ds where Ds:"Ds = (Cs'@pCs'')@pCs" by simp
        from es obtain vs where vs:"es = map Val vs" by auto
        from sub have "length Ts' = length Ts" by (simp add:list_all2_iff)
        with WTrts_same_length[OF wtes] vs have length:"length vs = length Ts"
          by simp
        from has_least_wf_mdecl[OF wf "method"]
        have lengthParams:"length Ts = length pns" by (simp add:wf_mdecl_def)
        with "method" last path_unique path_via Ds length ref vs show ?thesis
          by (auto intro!:exI RedStaticCall)
      next
        assume "¬(vs. es = map Val vs)"
        hence not_all_Val: "¬(e  set es. v. e = Val v)"
          by(simp add:ex_map_conv)
        let ?ves = "takeWhile (λe. v. e = Val v) es"
        let ?rest = "dropWhile (λe. v. e = Val v) es"
        let ?ex = "hd ?rest" let ?rst = "tl ?rest"
        from not_all_Val have nonempty: "?rest  []" by auto
        hence es: "es = ?ves @ ?ex # ?rst" by simp
        have "e  set ?ves. v. e = Val v" by(fastforce dest:set_takeWhileD)
        then obtain vs where ves: "?ves = map Val vs"
          using ex_map_conv by blast
        show ?thesis
        proof cases
          assume "final ?ex"
          moreover from nonempty have "¬(v. ?ex = Val v)"
            by(auto simp:neq_Nil_conv simp del:dropWhile_eq_Nil_conv)
              (simp add:dropWhile_eq_Cons_conv)
          ultimately obtain r' where ex_Throw: "?ex = Throw r'"
            by(fast elim!:finalE)
          show ?thesis using ref es ex_Throw ves
            by(fastforce intro:red_reds.CallThrowParams)
        next
          assume not_fin: "¬ final ?ex"
          have "finals es = finals(?ves @ ?ex # ?rst)" using es
            by(rule arg_cong)
          also have " = finals(?ex # ?rst)" using ves by simp
          finally have "finals es = finals(?ex # ?rst)" .
          hence "¬ finals es" using not_finals_ConsI[OF not_fin] by blast
          thus ?thesis using ref D IHes[OF hconf envconf]
            by(fastforce intro!:CallParams)
        qed
      qed
    next
      fix r assume "e = Throw r"
      with WTrtStaticCall.prems show ?thesis by(fast intro!:red_reds.CallThrowObj)
    qed
  next
    assume "¬ final e"
    with WTrtStaticCall show ?thesis by simp (blast intro!:CallObj)
  qed
next
  case (WTrtCallNT E h e es Ts Copt M T)
  show ?case
  proof cases
    assume "final e"
    moreover
    { fix v assume e: "e = Val v"
      hence "e = null" using WTrtCallNT by simp
      have ?case
      proof cases
        assume "finals es"
        moreover
        { fix vs assume "es = map Val vs"
          with WTrtCallNT e have ?thesis by(fastforce intro: RedCallNull dest!:typeof_NT) }
        moreover
        { fix vs a es' assume "es = map Val vs @ Throw a # es'"
          with WTrtCallNT e have ?thesis by(fastforce intro: CallThrowParams) }
        ultimately show ?thesis by(fastforce simp:finals_def)
      next
        assume "¬ finals es" ― ‹@{term es} reduces by IH›
        with WTrtCallNT e show ?thesis by(fastforce intro: CallParams)
      qed
    }
    moreover
    { fix r assume "e = Throw r"
      with WTrtCallNT have ?case by(fastforce intro: CallThrowObj) }
    ultimately show ?thesis by(fastforce simp:final_def)
  next
    assume "¬ final e" ― ‹@{term e} reduces by IH›
    with WTrtCallNT show ?thesis by (fastforce intro:CallObj)
  qed
next
  case (WTrtInitBlock h v T' E V T e2 T2)
  have IH2: "l. P  h ; P  E(V  T) ; 𝒟 e2 dom l; ¬ final e2
                   e' s'. P,E(V  T)  e2,(h,l)  e',s'"
    and typeof:"P  typeofh v = Some T'"
    and type:"is_type P T" and sub:"P  T'  T"
    and hconf: "P  h " and envconf:"P  E "
    and D: "𝒟 {V:T := Val v; e2} dom l" by fact+
  from wf typeof type sub obtain v' where casts:"P  T casts v to v'"
    by(auto dest:sub_casts)
  show ?case
  proof cases
    assume fin:"final e2"
    with casts show ?thesis
      by(fastforce elim:finalE intro:RedInitBlock red_reds.InitBlockThrow)
  next
    assume not_fin2: "¬ final e2"
    from D have D2: "𝒟 e2 dom(l(Vv'))" by (auto simp:hyperset_defs)
    from envconf type have "P  E(V  T) " by(auto simp:envconf_def)
    from IH2[OF hconf this D2 not_fin2]
    obtain h' l' e' where red2: "P,E(V  T)  e2,(h, l(Vv'))  e',(h', l')"
      by auto
    from red_lcl_incr[OF red2] have "V  dom l'" by auto
    with red2 casts show ?thesis by(fastforce intro:InitBlockRed)
  qed
next
  case (WTrtBlock E V T h e T')
  have IH: "l. P  h ; P  E(V  T) ; 𝒟 e dom l; ¬ final e
                  e' s'. P,E(V  T)  e,(h,l)  e',s'"
   and unass: "¬ assigned V e" and type:"is_type P T"
   and hconf: "P  h " and envconf:"P  E " 
    and D: "𝒟 {V:T; e} dom l" by fact+
  show ?case
  proof cases
    assume "final e"
    thus ?thesis
    proof (rule finalE)
      fix v assume "e = Val v" with type show ?thesis by(fast intro:RedBlock)
    next
      fix r assume "e = Throw r"
      with type show ?thesis by(fast intro:red_reds.BlockThrow)
    qed
  next
    assume not_fin: "¬ final e"
    from D have De: "𝒟 e dom(l(V:=None))" by(simp add:hyperset_defs)
    from envconf type have "P  E(V  T) " by(auto simp:envconf_def)
    from IH[OF hconf this De not_fin]
    obtain h' l' e' where red: "P,E(V  T)  e,(h,l(V:=None))  e',(h',l')"
      by auto
    show ?thesis
    proof (cases "l' V")
      assume "l' V = None"
      with red unass show ?thesis by(blast intro: BlockRedNone)
    next
      fix v assume "l' V = Some v"
      with red unass type show ?thesis by(blast intro: BlockRedSome)
    qed
  qed
next
  case (WTrtSeq E h e1 T1 e2 T2)
  show ?case
  proof cases
    assume "final e1"
    thus ?thesis
      by(fast elim:finalE intro:intro:RedSeq red_reds.SeqThrow)
  next
    assume "¬ final e1" with WTrtSeq show ?thesis
      by simp (blast intro:SeqRed)
  qed
next
  case (WTrtCond E h e e1 T e2)
  have wt: "P,E,h  e : Boolean" by fact
  show ?case
  proof cases
    assume "final e"
    thus ?thesis
    proof (rule finalE)
      fix v assume val: "e = Val v"
      then obtain b where v: "v = Bool b" using wt by (fastforce dest:typeof_Boolean)
      show ?thesis
      proof (cases b)
        case True with val v show ?thesis by(auto intro:RedCondT)
      next
        case False with val v show ?thesis by(auto intro:RedCondF)
      qed
    next
      fix r assume "e = Throw r"
      thus ?thesis by(fast intro:red_reds.CondThrow)
    qed
  next
    assume "¬ final e" with WTrtCond show ?thesis
      by simp (fast intro:CondRed)
  qed
next
  case WTrtWhile show ?case by(fast intro:RedWhile)
next
  case (WTrtThrow E h e T' T)
  show ?case
  proof cases
    assume "final e" ― ‹Then @{term e} must be @{term throw} or @{term null}
    with WTrtThrow show ?thesis
      by(fastforce simp:final_def is_refT_def
                  intro:red_reds.ThrowThrow red_reds.RedThrowNull
                  dest!:typeof_NT typeof_Class_Subo)
  next
    assume "¬ final e" ― ‹Then @{term e} must reduce›
    with WTrtThrow show ?thesis by simp (blast intro:ThrowRed)
  qed
next
  case WTrtNil thus ?case by simp
next
  case (WTrtCons E h e T es Ts)
  have IHe: "l. P  h ; P  E ; 𝒟 e dom l; ¬ final e
                 e' s'. P,E  e,(h,l)  e',s'"
   and IHes: "l. P  h ; P  E ; 𝒟s es dom l; ¬ finals es
              es' s'. P,E  es,(h,l) [→] es',s'"
   and hconf: "P  h " and envconf:"P  E "
    and D: "𝒟s (e#es) dom l"
   and not_fins: "¬ finals(e # es)" by fact+
  have De: "𝒟 e dom l" and Des: "𝒟s es (dom l  𝒜 e)"
    using D by auto
  show ?case
  proof cases
    assume "final e"
    thus ?thesis
    proof (rule finalE)
      fix v assume e: "e = Val v"
      hence Des': "𝒟s es dom l" using De Des by auto
      have not_fins_tl: "¬ finals es" using not_fins e by simp
      show ?thesis using e IHes[OF hconf envconf Des' not_fins_tl]
        by (blast intro!:ListRed2)
    next
      fix r assume "e = Throw r"
      hence False using not_fins by simp
      thus ?thesis ..
    qed
  next
    assume "¬ final e"
    from IHe[OF hconf envconf De this] show ?thesis by(fast intro!:ListRed1)
  qed
qed


end