Theory Equivalence

(*  Title:       CoreC++

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

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

section ‹Equivalence of Big Step and Small Step Semantics›

theory Equivalence imports BigStep SmallStep WWellForm begin


subsection‹Some casts-lemmas›

lemma assumes wf:"wf_prog wf_md P"
shows casts_casts:
"P  T casts v to v'  P  T casts v' to v'"

proof(induct rule:casts_to.induct)
  case casts_prim thus ?case by(rule casts_to.casts_prim)
next
  case (casts_null C) thus ?case by(rule casts_to.casts_null)
next
  case (casts_ref Cs C Cs' Ds a)
  have path_via:"P  Path last Cs to C via Cs'" and Ds:"Ds = Cs @p Cs'" by fact+
  with wf have "last Cs' = C" and "Cs'  []" and "class": "is_class P C"
    by(auto intro!:Subobjs_nonempty Subobj_last_isClass simp:path_via_def)
  with Ds have last:"last Ds = C"
    by -(drule_tac Cs' = "Cs" in appendPath_last,simp)
  hence Ds':"Ds = Ds @p [C]" by(simp add:appendPath_def)
  from last "class" have "P  Path last Ds to C via [C]"
    by(fastforce intro:Subobjs_Base simp:path_via_def)
  with Ds' show ?case by(fastforce intro:casts_to.casts_ref)
qed



lemma casts_casts_eq:
" P  T casts v to v; P  T casts v to v'; wf_prog wf_md P   v = v'"

  apply -
  apply(erule casts_to.cases)
    apply clarsimp
    apply(erule casts_to.cases)
      apply simp
     apply simp
    apply (simp (asm_lr))
   apply(erule casts_to.cases)
     apply simp
    apply simp
   apply simp
  apply simp
  apply(erule casts_to.cases)
    apply simp
   apply simp
  apply clarsimp
  apply(erule appendPath_path_via)
  by auto



lemma assumes wf:"wf_prog wf_md P"
shows None_lcl_casts_values:
"P,E  e,(h,l)  e',(h',l') 
  (V. l V = None; E V = Some T; l' V = Some v'
   P  T casts v' to v')"
and "P,E  es,(h,l) [→] es',(h',l') 
  (V. l V = None; E V = Some T; l' V = Some v'
   P  T casts v' to v')"

proof(induct rule:red_reds_inducts)
  case (RedLAss E V T' w w' h l V')
  have env:"E V = Some T'" and env':"E V' = Some T"
    and l:"l V' = None" and lupd:"(l(V  w')) V' = Some v'"
    and casts:"P  T' casts w to w'" by fact+
  show ?case
  proof(cases "V = V'")
    case True
    with lupd have v':"v' = w'" by simp
    from True env env' have "T = T'" by simp
    with v' casts wf show ?thesis by(fastforce intro:casts_casts)
  next
    case False
    with lupd have "l V' = Some v'" by(fastforce split:if_split_asm)
    with l show ?thesis by simp
  qed
next
  case (BlockRedNone E V T' e h l e' h' l' V')
  have l:"l V' = None"
    and l'upd:"(l'(V := l V)) V' = Some v'" and env:"E V' = Some T"
    and IH:"V'. (l(V := None)) V' = None; (E(V  T')) V' = Some T; 
                   l' V' = Some v'
             P  T casts v' to v'" by fact+
  show ?case
  proof(cases "V = V'")
    case True 
    with l'upd l show ?thesis by fastforce
  next
    case False
    with l  l'upd have lnew:"(l(V := None)) V' = None"
      and l'new:"l' V' = Some v'" by (auto split:if_split_asm)
    from env False have env':"(E(V  T')) V' = Some T" by fastforce
    from IH[OF lnew env' l'new] show ?thesis .
  qed
next
  case (BlockRedSome E V T' e h l e' h' l' v V')
  have l:"l V' = None"
    and l'upd:"(l'(V := l V)) V' = Some v'" and env:"E V' = Some T"
    and IH:"V'. (l(V := None)) V' = None; (E(V  T')) V' = Some T; 
                   l' V' = Some v'
             P  T casts v' to v'" by fact+
  show ?case
  proof(cases "V = V'")
    case True
    with l l'upd show ?thesis by fastforce
  next
    case False
    with l  l'upd have lnew:"(l(V := None)) V' = None"
      and l'new:"l' V' = Some v'" by (auto split:if_split_asm)
    from env False have env':"(E(V  T')) V' = Some T" by fastforce
    from IH[OF lnew env' l'new] show ?thesis .
  qed
next
  case (InitBlockRed E V T' e h l w' e' h' l' w'' w V')
  have l:"l V' = None"
    and l'upd:"(l'(V := l V)) V' = Some v'" and env:"E V' = Some T"
    and IH:"V'. (l(V  w')) V' = None; (E(V  T')) V' = Some T; 
                   l' V' = Some v'
             P  T casts v' to v'" by fact+
  show ?case
  proof(cases "V = V'")
    case True
    with l l'upd show ?thesis by fastforce
  next
    case False
    with l  l'upd have lnew:"(l(V  w')) V' = None"
      and l'new:"l' V' = Some v'" by (auto split:if_split_asm)
    from env False have env':"(E(V  T')) V' = Some T" by fastforce
    from IH[OF lnew env' l'new] show ?thesis .
  qed
qed (auto intro:casts_casts wf)



lemma assumes wf:"wf_prog wf_md P"
shows Some_lcl_casts_values:
"P,E  e,(h,l)  e',(h',l') 
  (V. l V = Some v; E V = Some T;
      P  T casts v'' to v; l' V = Some v'
   P  T casts v' to v')"
and "P,E  es,(h,l) [→] es',(h',l') 
  (V. l V = Some v; E V = Some T;
      P  T casts v'' to v; l' V = Some v'
   P  T casts v' to v')"

proof(induct rule:red_reds_inducts)
  case (RedNew h a h' C' E l V)
  have l1:"l V = Some v" and l2:"l V = Some v'"
    and casts:"P  T casts v'' to v " by fact+
  from l1 l2 have eq:"v = v'" by simp
  with casts wf show ?case by(fastforce intro:casts_casts)
next
  case (RedLAss E V T' w w' h l V')
  have l:"l V' = Some v" and lupd:"(l(V  w')) V' = Some v'"
    and T'casts:"P  T' casts w to w'"
    and env:"E V = Some T'" and env':"E V' = Some T"
    and casts:"P  T casts v'' to v" by fact+
  show ?case
  proof (cases "V = V'")
    case True
    with lupd have v':"v' = w'" by simp
    from True env env' have "T = T'" by simp
    with T'casts v' wf show ?thesis by(fastforce intro:casts_casts)
  next
    case False
    with l lupd have "v = v'" by (auto split:if_split_asm)
    with casts wf show ?thesis by(fastforce intro:casts_casts)
  qed
next
  case (RedFAss h a D S Cs' F T' Cs w w' Ds fs E l V)
  have l1:"l V = Some v" and l2:"l V = Some v'"
    and hp:"h a = Some(D, S)"
    and T'casts:"P  T' casts w to w'"
    and casts:"P  T casts v'' to v" by fact+
  from l1 l2 have eq:"v = v'" by simp
  with casts wf show ?case by(fastforce intro:casts_casts)
next
  case (BlockRedNone E V T' e h l e' h' l' V')
  have l':"l' V = None" and l:"l V' = Some v"
    and l'upd:"(l'(V := l V)) V' = Some v'" and env:"E V' = Some T"
    and casts:"P  T casts v'' to v"
    and IH:"V'. (l(V := None)) V' = Some v; (E(V  T')) V' = Some T; 
                  P  T casts v'' to v ; l' V' = Some v'
             P  T casts v' to v'" by fact+
  show ?case
  proof(cases "V = V'")
    case True
    with l' l'upd have "l V = Some v'" by auto
    with True l have eq:"v = v'" by simp
    with casts wf show ?thesis by(fastforce intro:casts_casts)
  next
    case False
    with l  l'upd have lnew:"(l(V := None)) V' = Some v"
      and l'new:"l' V' = Some v'" by (auto split:if_split_asm)
    from env False have env':"(E(V  T')) V' = Some T" by fastforce
    from IH[OF lnew env' casts l'new] show ?thesis .
  qed
next
  case (BlockRedSome E V T' e h l e' h' l' w V')
  have l':"l' V = Some w" and l:"l V' = Some v"
    and l'upd:"(l'(V := l V)) V' = Some v'" and env:"E V' = Some T"
    and casts:"P  T casts v'' to v"
    and IH:"V'. (l(V := None)) V' = Some v; (E(V  T')) V' = Some T; 
                   P  T casts v'' to v ; l' V' = Some v'
             P  T casts v' to v'" by fact+
  show ?case
  proof(cases "V = V'")
    case True
    with l' l'upd have "l V = Some v'" by auto
    with True l have eq:"v = v'" by simp
    with casts wf show ?thesis by(fastforce intro:casts_casts)
  next
    case False
    with l  l'upd have lnew:"(l(V := None)) V' = Some v"
      and l'new:"l' V' = Some v'" by (auto split:if_split_asm)
    from env False have env':"(E(V  T')) V' = Some T" by fastforce
    from IH[OF lnew env' casts l'new] show ?thesis .
  qed
next
  case (InitBlockRed E V T' e h l w' e' h' l' w'' w V')
  have l:"l V' = Some v" and l':"l' V = Some w''"
    and l'upd:"(l'(V := l V)) V' = Some v'" and env:"E V' = Some T"
    and casts:"P  T casts v'' to v"
    and IH:"V'. (l(V  w')) V' = Some v; (E(V  T')) V' = Some T; 
                   P  T casts v'' to v ; l' V' = Some v'
             P  T casts v' to v'" by fact+
  show ?case
  proof(cases "V = V'")
    case True
    with l' l'upd have "l V = Some v'" by auto
    with True l have eq:"v = v'" by simp
    with casts wf show ?thesis by(fastforce intro:casts_casts)
  next
    case False
    with l  l'upd have lnew:"(l(V  w')) V' = Some v"
      and l'new:"l' V' = Some v'" by (auto split:if_split_asm)
    from env False have env':"(E(V  T')) V' = Some T" by fastforce
    from IH[OF lnew env' casts l'new] show ?thesis .
  qed
qed (auto intro:casts_casts wf)

  


subsection‹Small steps simulate big step›

subsection ‹Cast›

lemma StaticCastReds:
  "P,E  e,s →* e',s'  P,E  Ce,s →* Ce',s'"

apply(erule rtrancl_induct2)
 apply blast
apply(erule rtrancl_into_rtrancl)
apply (simp add:StaticCastRed)
done


lemma StaticCastRedsNull:
  "P,E  e,s →* null,s'  P,E  Ce,s →* null,s'"

apply(rule rtrancl_into_rtrancl)
 apply(erule StaticCastReds)
apply(simp add:RedStaticCastNull)
done


lemma StaticUpCastReds:
  " P,E  e,s →* ref(a,Cs),s'; P  Path last Cs to C via Cs'; Ds = Cs@pCs'  
   P,E  Ce,s →* ref(a,Ds),s'"

apply(rule rtrancl_into_rtrancl)
 apply(erule StaticCastReds)
apply(fastforce intro:RedStaticUpCast)
done


lemma StaticDownCastReds:
  "P,E  e,s →* ref(a,Cs@[C]@Cs'),s'
    P,E  Ce,s →* ref(a,Cs@[C]),s'"

apply(rule rtrancl_into_rtrancl)
 apply(erule StaticCastReds)
apply simp
apply(subgoal_tac "P,E  Cref(a,Cs@[C]@Cs'),s'  ref(a,Cs@[C]),s'")
 apply simp
apply(rule RedStaticDownCast)
done


lemma StaticCastRedsFail:
  " P,E  e,s →* ref(a,Cs),s'; C  set Cs; ¬ P  (last Cs) * C 
   P,E  Ce,s →* THROW ClassCast,s'"

apply(rule rtrancl_into_rtrancl)
 apply(erule StaticCastReds)
apply(fastforce intro:RedStaticCastFail)
done


lemma StaticCastRedsThrow:
  " P,E  e,s →* Throw r,s'   P,E  Ce,s →* Throw r,s'"

apply(rule rtrancl_into_rtrancl)
 apply(erule StaticCastReds)
apply(simp add:red_reds.StaticCastThrow)
done


lemma DynCastReds:
  "P,E  e,s →* e',s'  P,E  Cast C e,s →* Cast C e',s'"

apply(erule rtrancl_induct2)
 apply blast
apply(erule rtrancl_into_rtrancl)
apply (simp add:DynCastRed)
done


lemma DynCastRedsNull:
  "P,E  e,s →* null,s'  P,E  Cast C e,s →* null,s'"

apply(rule rtrancl_into_rtrancl)
 apply(erule DynCastReds)
apply(simp add:RedDynCastNull)
done


lemma DynCastRedsRef:
  " P,E  e,s →* ref(a,Cs),s'; hp s' a = Some (D,S); P  Path D to C via Cs';
     P  Path D to C unique  
  P,E  Cast C e,s →* ref(a,Cs'),s'"

apply(rule rtrancl_into_rtrancl)
 apply(erule DynCastReds)
apply(fastforce intro:RedDynCast)
done


lemma StaticUpDynCastReds:
  " P,E  e,s →* ref(a,Cs),s'; P  Path last Cs to C unique;
  P  Path last Cs to C via Cs'; Ds = Cs@pCs'  
   P,E  Cast C e,s →* ref(a,Ds),s'"

apply(rule rtrancl_into_rtrancl)
 apply(erule DynCastReds)
apply(fastforce intro:RedStaticUpDynCast)
done


lemma StaticDownDynCastReds:
  "P,E  e,s →* ref(a,Cs@[C]@Cs'),s'
    P,E  Cast C e,s →* ref(a,Cs@[C]),s'"

apply(rule rtrancl_into_rtrancl)
 apply(erule DynCastReds)
apply simp
apply(subgoal_tac "P,E  Cast C (ref(a,Cs@[C]@Cs')),s'  ref(a,Cs@[C]),s'")
 apply simp
apply(rule RedStaticDownDynCast)
done


lemma DynCastRedsFail:
  " P,E  e,s →* ref(a,Cs),s'; hp s' a = Some (D,S); ¬ P  Path D to C unique;
    ¬ P  Path last Cs to C unique; C  set Cs 
   P,E  Cast C e,s →* null,s'"

apply(rule rtrancl_into_rtrancl)
 apply(erule DynCastReds)
apply(fastforce intro:RedDynCastFail)
done


lemma DynCastRedsThrow:
  " P,E  e,s →* Throw r,s'   P,E  Cast C e,s →* Throw r,s'"

apply(rule rtrancl_into_rtrancl)
 apply(erule DynCastReds)
apply(simp add:red_reds.DynCastThrow)
done


subsection ‹LAss›

lemma LAssReds:
  "P,E  e,s →* e',s'  P,E  V:=e,s →* V:=e',s'"

apply(erule rtrancl_induct2)
 apply blast
apply(erule rtrancl_into_rtrancl)
apply(simp add:LAssRed)
done


lemma LAssRedsVal:
  " P,E  e,s →* Val v,(h',l'); E V = Some T; P  T casts v to v' 
   P,E   V:=e,s →* Val v',(h',l'(Vv'))"

apply(rule rtrancl_into_rtrancl)
 apply(erule LAssReds)
apply(simp add:RedLAss)
done


lemma LAssRedsThrow:
  " P,E  e,s →* Throw r,s'   P,E   V:=e,s →* Throw r,s'"

apply(rule rtrancl_into_rtrancl)
 apply(erule LAssReds)
apply(simp add:red_reds.LAssThrow)
done


subsection ‹BinOp›

lemma BinOp1Reds:
  "P,E  e,s →* e',s'  P,E   e «bop» e2, s →* e' «bop» e2, s'"

apply(erule rtrancl_induct2)
 apply blast
apply(erule rtrancl_into_rtrancl)
apply(simp add:BinOpRed1)
done


lemma BinOp2Reds:
  "P,E  e,s →* e',s'  P,E  (Val v) «bop» e, s →* (Val v) «bop» e', s'"

apply(erule rtrancl_induct2)
 apply blast
apply(erule rtrancl_into_rtrancl)
apply(simp add:BinOpRed2)
done


lemma BinOpRedsVal:
  " P,E  e1,s0 →* Val v1,s1; P,E  e2,s1 →* Val v2,s2; 
     binop(bop,v1,v2) = Some v 
   P,E  e1 «bop» e2, s0 →* Val v,s2"

apply(rule rtrancl_trans)
 apply(erule BinOp1Reds)
apply(rule rtrancl_into_rtrancl)
 apply(erule BinOp2Reds)
apply(simp add:RedBinOp)
done


lemma BinOpRedsThrow1:
  "P,E  e,s →* Throw r,s'  P,E  e «bop» e2, s →* Throw r, s'"

apply(rule rtrancl_into_rtrancl)
 apply(erule BinOp1Reds)
apply(simp add:red_reds.BinOpThrow1)
done


lemma BinOpRedsThrow2:
  " P,E  e1,s0 →* Val v1,s1; P,E  e2,s1 →* Throw r,s2
   P,E  e1 «bop» e2, s0 →* Throw r,s2"

apply(rule rtrancl_trans)
 apply(erule BinOp1Reds)
apply(rule rtrancl_into_rtrancl)
 apply(erule BinOp2Reds)
apply(simp add:red_reds.BinOpThrow2)
done


subsection ‹FAcc›

lemma FAccReds:
  "P,E  e,s →* e',s'  P,E  eF{Cs}, s →* e'F{Cs}, s'"

apply(erule rtrancl_induct2)
 apply blast
apply(erule rtrancl_into_rtrancl)
apply(simp add:FAccRed)
done


lemma FAccRedsVal:
  "P,E  e,s →* ref(a,Cs'),s'; hp s' a = Some(D,S); 
    Ds = Cs'@pCs; (Ds,fs)  S; fs F = Some v 
   P,E  eF{Cs},s →* Val v,s'"

apply(rule rtrancl_into_rtrancl)
 apply(erule FAccReds)
apply (fastforce intro:RedFAcc)
done


lemma FAccRedsNull:
  "P,E  e,s →* null,s'  P,E  eF{Cs},s →* THROW NullPointer,s'"

apply(rule rtrancl_into_rtrancl)
 apply(erule FAccReds)
apply(simp add:RedFAccNull)
done


lemma FAccRedsThrow:
  "P,E  e,s →* Throw r,s'  P,E  eF{Cs},s →* Throw r,s'"

apply(rule rtrancl_into_rtrancl)
 apply(erule FAccReds)
apply(simp add:red_reds.FAccThrow)
done


subsection ‹FAss›

lemma FAssReds1:
  "P,E  e,s →* e',s'  P,E  eF{Cs}:=e2, s →* e'F{Cs}:=e2, s'"

apply(erule rtrancl_induct2)
 apply blast
apply(erule rtrancl_into_rtrancl)
apply(simp add:FAssRed1)
done


lemma FAssReds2:
  "P,E  e,s →* e',s'  P,E  Val vF{Cs}:=e, s →* Val vF{Cs}:=e', s'"

apply(erule rtrancl_induct2)
 apply blast
apply(erule rtrancl_into_rtrancl)
apply(simp add:FAssRed2)
done


lemma FAssRedsVal:
  " P,E  e1,s0 →* ref(a,Cs'),s1; P,E  e2,s1 →* Val v,(h2,l2); 
    h2 a = Some(D,S); P  (last Cs') has least F:T via Cs; P  T casts v to v';
    Ds = Cs'@pCs; (Ds,fs)  S  
  P,E  e1F{Cs}:=e2, s0 →* 
        Val v',(h2(a(D,insert (Ds,fs(Fv')) (S - {(Ds,fs)}))),l2)"

apply(rule rtrancl_trans)
 apply(erule FAssReds1)
apply(rule rtrancl_into_rtrancl)
 apply(erule FAssReds2)
apply(fastforce intro:RedFAss)
done


lemma FAssRedsNull:
  " P,E  e1,s0 →* null,s1; P,E  e2,s1 →* Val v,s2  
  P,E  e1F{Cs}:=e2, s0 →* THROW NullPointer, s2"

apply(rule rtrancl_trans)
 apply(erule FAssReds1)
apply(rule rtrancl_into_rtrancl)
 apply(erule FAssReds2)
apply(simp add:RedFAssNull)
done


lemma FAssRedsThrow1:
  "P,E  e,s →* Throw r,s'  P,E  eF{Cs}:=e2, s →* Throw r, s'"

apply(rule rtrancl_into_rtrancl)
 apply(erule FAssReds1)
apply(simp add:red_reds.FAssThrow1)
done


lemma FAssRedsThrow2:
  " P,E  e1,s0 →* Val v,s1; P,E  e2,s1 →* Throw r,s2 
   P,E  e1F{Cs}:=e2,s0 →* Throw r,s2"

apply(rule rtrancl_trans)
 apply(erule FAssReds1)
apply(rule rtrancl_into_rtrancl)
 apply(erule FAssReds2)
apply(simp add:red_reds.FAssThrow2)
done


subsection ‹;;›

lemma  SeqReds:
  "P,E  e,s →* e',s'  P,E  e;;e2, s →* e';;e2, s'"

apply(erule rtrancl_induct2)
 apply blast
apply(erule rtrancl_into_rtrancl)
apply(simp add:SeqRed)
done


lemma SeqRedsThrow:
  "P,E  e,s →* Throw r,s'  P,E  e;;e2, s →* Throw r, s'"

apply(rule rtrancl_into_rtrancl)
 apply(erule SeqReds)
apply(simp add:red_reds.SeqThrow)
done


lemma SeqReds2:
  " P,E  e1,s0 →* Val v1,s1; P,E  e2,s1 →* e2',s2   P,E  e1;;e2, s0 →* e2',s2"

apply(rule rtrancl_trans)
 apply(erule SeqReds)
apply(rule_tac b="(e2,s1)" in converse_rtrancl_into_rtrancl)
 apply(simp add:RedSeq)
apply assumption
done



subsection ‹If›

lemma CondReds:
  "P,E  e,s →* e',s'  P,E  if (e) e1 else e2,s →* if (e') e1 else e2,s'"

apply(erule rtrancl_induct2)
 apply blast
apply(erule rtrancl_into_rtrancl)
apply(simp add:CondRed)
done


lemma CondRedsThrow:
  "P,E  e,s →* Throw r,s'  P,E  if (e) e1 else e2, s →* Throw r,s'"

apply(rule rtrancl_into_rtrancl)
 apply(erule CondReds)
apply(simp add:red_reds.CondThrow)
done


lemma CondReds2T:
  "P,E  e,s0 →* true,s1; P,E  e1, s1 →* e',s2   P,E  if (e) e1 else e2, s0 →* e',s2"

apply(rule rtrancl_trans)
 apply(erule CondReds)
apply(rule_tac b="(e1, s1)" in converse_rtrancl_into_rtrancl)
 apply(simp add:RedCondT)
apply assumption
done


lemma CondReds2F:
  "P,E  e,s0 →* false,s1; P,E  e2, s1 →* e',s2   P,E  if (e) e1 else e2, s0 →* e',s2"

apply(rule rtrancl_trans)
 apply(erule CondReds)
apply(rule_tac b="(e2, s1)" in  converse_rtrancl_into_rtrancl)
 apply(simp add:RedCondF)
apply assumption
done



subsection ‹While›

lemma WhileFReds:
  "P,E  b,s →* false,s'  P,E  while (b) c,s →* unit,s'"

apply(rule_tac b="(if(b) (c;;while(b) c) else unit, s)" in converse_rtrancl_into_rtrancl)
 apply(simp add:RedWhile)
apply(rule rtrancl_into_rtrancl)
 apply(erule CondReds)
apply(simp add:RedCondF)
done


lemma WhileRedsThrow:
  "P,E  b,s →* Throw r,s'  P,E  while (b) c,s →* Throw r,s'"

apply(rule_tac b="(if(b) (c;;while(b) c) else unit, s)" in converse_rtrancl_into_rtrancl)
 apply(simp add:RedWhile)
apply(rule rtrancl_into_rtrancl)
 apply(erule CondReds)
apply(simp add:red_reds.CondThrow)
done


lemma WhileTReds:
  " P,E  b,s0 →* true,s1; P,E  c,s1 →* Val v1,s2; P,E  while (b) c,s2 →* e,s3 
   P,E  while (b) c,s0 →* e,s3"

apply(rule_tac b="(if(b) (c;;while(b) c) else unit, s0)" in converse_rtrancl_into_rtrancl)
 apply(simp add:RedWhile)
apply(rule rtrancl_trans)
 apply(erule CondReds)
apply(rule_tac b="(c;;while(b) c,s1)" in converse_rtrancl_into_rtrancl)
 apply(simp add:RedCondT)
apply(rule rtrancl_trans)
 apply(erule SeqReds)
apply(rule_tac b="(while(b) c,s2)" in converse_rtrancl_into_rtrancl)
 apply(simp add:RedSeq)
apply assumption
done


lemma WhileTRedsThrow:
  " P,E  b,s0 →* true,s1; P,E  c,s1 →* Throw r,s2 
   P,E  while (b) c,s0 →* Throw r,s2"

apply(rule_tac b="(if(b) (c;;while(b) c) else unit, s0)" in converse_rtrancl_into_rtrancl)
 apply(simp add:RedWhile)
apply(rule rtrancl_trans)
 apply(erule CondReds)
apply(rule_tac b="(c;;while(b) c,s1)" in converse_rtrancl_into_rtrancl)
 apply(simp add:RedCondT)
apply(rule rtrancl_trans)
 apply(erule SeqReds)
apply(rule_tac b="(Throw r,s2)" in converse_rtrancl_into_rtrancl)
 apply(simp add:red_reds.SeqThrow)
apply simp
done


subsection ‹Throw›

lemma ThrowReds:
  "P,E  e,s →* e',s'  P,E  throw e,s →* throw e',s'"

apply(erule rtrancl_induct2)
 apply blast
apply(erule rtrancl_into_rtrancl)
apply(simp add:ThrowRed)
done


lemma ThrowRedsNull:
  "P,E  e,s →* null,s'  P,E  throw e,s →* THROW NullPointer,s'"

apply(rule rtrancl_into_rtrancl)
 apply(erule ThrowReds)
apply(simp add:RedThrowNull)
done


lemma ThrowRedsThrow:
  "P,E  e,s →* Throw r,s'  P,E  throw e,s →* Throw r,s'"

apply(rule rtrancl_into_rtrancl)
 apply(erule ThrowReds)
apply(simp add:red_reds.ThrowThrow)
done


subsection ‹InitBlock›

lemma assumes wf:"wf_prog wf_md P"
shows InitBlockReds_aux:
"P,E(V  T)  e,s →* e',s' 
  h l h' l' v v'. s = (h,l(Vv'))  
                   P  T casts v to v'  s' = (h',l') 
                   (v'' w. P,E  {V:T := Val v; e},(h,l) →* 
                                {V:T := Val v''; e'},(h',l'(V:=(l V))) 
                            P  T casts v'' to w)"
proof (erule converse_rtrancl_induct2)
  { fix h l h' l' v v'
    assume "s' = (h, l(V  v'))" and "s' = (h', l')"
    hence h:"h = h'" and l':"l' = l(V  v')" by simp_all
    hence "P,E  {V:T; V:=Val v;; e'},(h, l) →*
                 {V:T; V:=Val v;; e'},(h', l'(V := l V))"
      by(fastforce simp: fun_upd_same simp del:fun_upd_apply) }
  hence "h l h' l' v v'.
         s' = (h, l(V  v')) 
           P  T casts v to v'  
             s' = (h', l') 
               P,E  {V:T; V:=Val v;; e'},(h, l) →*
                     {V:T; V:=Val v;; e'},(h', l'(V := l V)) 
               P  T casts v to v'"
    by auto
  thus "h l h' l' v v'.
       s' = (h, l(V  v')) 
         P  T casts v to v'  
           s' = (h', l') 
             (v'' w. P,E  {V:T; V:=Val v;; e'},(h, l) →*
                            {V:T; V:=Val v'';; e'},(h', l'(V := l V)) 
                      P  T casts v'' to w)"
    by auto
next
  fix e s e'' s''
  assume Red:"((e,s),e'',s'')  Red P (E(V  T))"
    and reds:"P,E(V  T)  e'',s'' →* e',s'"
    and IH:"h l h' l' v v'.
           s'' = (h, l(V  v')) 
             P  T casts v to v'  
               s' = (h', l') 
                 (v'' w. P,E  {V:T; V:=Val v;; e''},(h, l) →*
                                {V:T; V:=Val v'';; e'},(h', l'(V := l V)) 
                          P  T casts v'' to w)"
  { fix h l h' l' v v'
    assume s:"s = (h, l(V  v'))" and s':"s' = (h', l')"
      and casts:"P  T casts v to v'"
    obtain h'' l'' where s'':"s'' = (h'',l'')" by (cases s'') auto
    with Red s have "V  dom l''" by (fastforce dest:red_lcl_incr)
    then obtain v'' where l'':"l'' V = Some v''" by auto
    with Red s s'' casts
    have step:"P,E  {V:T := Val v; e},(h, l)   
              {V:T := Val v''; e''}, (h'',l''(V := l V))"
      by(fastforce intro:InitBlockRed)
    from Red s s'' l'' casts wf
    have casts':"P  T casts v'' to v''" by(fastforce intro:Some_lcl_casts_values)
    with IH s'' s' l'' obtain v''' w
      where "P,E  {V:T := Val v''; e''}, (h'',l''(V := l V)) →*
                   {V:T := Val v'''; e'},(h', l'(V := l V)) 
             P  T casts v''' to w"
      apply simp
      apply (erule_tac x = "l''(V := l V)" in allE)
      apply (erule_tac x = "v''" in allE)
      apply (erule_tac x = "v''" in allE)
      by(auto intro:ext)
    with step have "v'' w. P,E  {V:T; V:=Val v;; e},(h, l) →*
                                   {V:T; V:=Val v'';; e'},(h', l'(V := l V)) 
                            P  T casts v'' to w"
      apply(rule_tac x="v'''" in exI)
      apply auto
       apply (rule converse_rtrancl_into_rtrancl)
      by simp_all }
  thus "h l h' l' v v'.
             s = (h, l(V  v')) 
             P  T casts v to v'  
             s' = (h', l') 
             (v'' w. P,E  {V:T; V:=Val v;; e},(h, l) →*
                            {V:T; V:=Val v'';; e'},(h', l'(V := l V)) 
                      P  T casts v'' to w)"
    by auto
qed



lemma InitBlockReds:
 "P,E(V  T)  e, (h,l(Vv')) →* e', (h',l'); 
   P  T casts v to v'; wf_prog wf_md P  
  v'' w. P,E  {V:T := Val v; e}, (h,l) →* 
              {V:T := Val v''; e'}, (h',l'(V:=(l V))) 
          P  T casts v'' to w"
by(blast dest:InitBlockReds_aux)

lemma InitBlockRedsFinal:
  assumes reds:"P,E(V  T)  e,(h,l(Vv')) →* e',(h',l')"
  and final:"final e'" and casts:"P  T casts v to v'"
  and wf:"wf_prog wf_md P"
  shows "P,E  {V:T := Val v; e},(h,l) →* e',(h', l'(V := l V))"
proof -
  from reds casts wf obtain v'' and w
    where steps:"P,E  {V:T := Val v; e},(h,l) →* 
                        {V:T := Val v''; e'}, (h',l'(V:=(l V)))"
    and casts':"P  T casts v'' to w"
    by (auto dest:InitBlockReds)
  from final casts casts'
  have step:"P,E  {V:T := Val v''; e'}, (h',l'(V:=(l V))) 
                    e',(h',l'(V := l V))"
    by(auto elim!:finalE intro:RedInitBlock InitBlockThrow)
  from step steps show ?thesis
    by(fastforce intro:rtrancl_into_rtrancl)
qed



subsection ‹Block›

lemma BlockRedsFinal:
assumes reds: "P,E(V  T)  e0,s0 →* e2,(h2,l2)" and fin: "final e2"
  and wf:"wf_prog wf_md P"
shows "h0 l0. s0 = (h0,l0(V:=None))  P,E  {V:T; e0},(h0,l0) →* e2,(h2,l2(V:=l0 V))"

using reds
proof (induct rule:converse_rtrancl_induct2)
  case refl thus ?case
    by(fastforce intro:finalE[OF fin] RedBlock BlockThrow
                simp del:fun_upd_apply)
next
  case (step e0 s0 e1 s1)
  have Red: "((e0,s0),e1,s1)  Red P (E(V  T))"
   and reds: "P,E(V  T)  e1,s1 →* e2,(h2,l2)"
   and IH: "h l. s1 = (h,l(V := None))
                 P,E  {V:T; e1},(h,l) →* e2,(h2, l2(V := l V))"
   and s0: "s0 = (h0, l0(V := None))" by fact+
  obtain h1 l1 where s1: "s1 = (h1,l1)" by fastforce
  show ?case
  proof cases
    assume "assigned V e0"
    then obtain v e where e0: "e0 = V:= Val v;; e"
      by (unfold assigned_def)blast
    from Red e0 s0 obtain v' where e1: "e1 = Val v';;e" 
      and s1: "s1 = (h0, l0(V  v'))" and casts:"P  T casts v to v'"
      by auto
    from e1 fin have "e1  e2" by (auto simp:final_def)
    then obtain e' s' where red1: "P,E(V  T)  e1,s1  e',s'"
      and reds': "P,E(V  T)  e',s' →* e2,(h2,l2)"
      using converse_rtranclE2[OF reds] by simp blast
    from red1 e1 have es': "e' = e" "s' = s1" by auto
    show ?thesis using e0 s1 es' reds'
        by(fastforce intro!: InitBlockRedsFinal[OF _ fin casts wf] 
                    simp del:fun_upd_apply)
  next
    assume unass: "¬ assigned V e0"
    show ?thesis
    proof (cases "l1 V")
      assume None: "l1 V = None"
      hence "P,E  {V:T; e0},(h0,l0)  {V:T; e1},(h1, l1(V := l0 V))"
        using s0 s1 Red by(simp add: BlockRedNone[OF _ _ unass])
      moreover
      have "P,E  {V:T; e1},(h1, l1(V := l0 V)) →* e2,(h2, l2(V := l0 V))"
        using IH[of _ "l1(V := l0 V)"] s1 None by(simp add:fun_upd_idem)
      ultimately show ?case
        by(rule_tac b="({V:T; e1},(h1, l1(V := l0 V)))" in converse_rtrancl_into_rtrancl,simp)
    next
      fix v assume Some: "l1 V = Some v"
      with Red Some s0 s1 wf
      have casts:"P  T casts v to v"
        by(fastforce intro:None_lcl_casts_values)
      from Some
      have "P,E  {V:T;e0},(h0,l0)  {V:T := Val v; e1},(h1,l1(V := l0 V))"
        using s0 s1 Red by(simp add: BlockRedSome[OF _ _ unass])
      moreover
      have "P,E  {V:T := Val v; e1},(h1,l1(V:= l0 V)) →*
                e2,(h2,l2(V:=l0 V))"
        using InitBlockRedsFinal[OF _ fin casts wf,of _ _ "l1(V:=l0 V)" V] 
          Some reds s1
        by (simp add:fun_upd_idem)
      ultimately show ?case 
        by(rule_tac b="({V:T; V:=Val v;; e1},(h1, l1(V := l0 V)))" in converse_rtrancl_into_rtrancl,simp)
    qed
  qed
qed




subsection ‹List›

lemma ListReds1:
  "P,E  e,s →* e',s'  P,E  e#es,s [→]* e' # es,s'"

apply(erule rtrancl_induct2)
 apply blast
apply(erule rtrancl_into_rtrancl)
apply(simp add:ListRed1)
done


lemma ListReds2:
  "P,E  es,s [→]* es',s'  P,E  Val v # es,s [→]* Val v # es',s'"

apply(erule rtrancl_induct2)
 apply blast
apply(erule rtrancl_into_rtrancl)
apply(simp add:ListRed2)
done


lemma ListRedsVal:
  " P,E  e,s0 →* Val v,s1; P,E  es,s1 [→]* es',s2 
   P,E  e#es,s0 [→]* Val v # es',s2"

apply(rule rtrancl_trans)
 apply(erule ListReds1)
apply(erule ListReds2)
done


subsection ‹Call›

text‹First a few lemmas on what happens to free variables during redction.›


lemma assumes wf: "wwf_prog P"
shows Red_fv: "P,E  e,(h,l)  e',(h',l')  fv e'  fv e"
  and  "P,E  es,(h,l) [→] es',(h',l')  fvs es'  fvs es"
proof (induct rule:red_reds_inducts)
  case (RedCall h l a C S Cs M Ts' T' pns' body' Ds Ts T pns body Cs' vs bs new_body E)
  hence "fv body  {this}  set pns"
    using assms by(fastforce dest!:select_method_wf_mdecl simp:wf_mdecl_def)
  with RedCall.hyps show ?case
    by(cases T') auto
next
  case (RedStaticCall Cs C Cs'' M Ts T pns body Cs' Ds vs E a a' b)
  hence "fv body  {this}  set pns"
    using assms by(fastforce dest!:has_least_wf_mdecl simp:wf_mdecl_def)
  with RedStaticCall.hyps show ?case
    by auto
qed auto



lemma Red_dom_lcl:
  "P,E  e,(h,l)  e',(h',l')  dom l'  dom l  fv e" and
  "P,E  es,(h,l) [→] es',(h',l')  dom l'  dom l  fvs es"

proof (induct rule:red_reds_inducts)
  case RedLAss thus ?case by(force split:if_splits)
next
  case CallParams thus ?case by(force split:if_splits)
next
  case BlockRedNone thus ?case by clarsimp (fastforce split:if_splits)
next
  case BlockRedSome thus ?case by clarsimp (fastforce split:if_splits)
next
  case InitBlockRed thus ?case by clarsimp (fastforce split:if_splits)
qed auto



lemma Reds_dom_lcl:
  " wwf_prog P; P,E  e,(h,l) →* e',(h',l')   dom l'  dom l  fv e"

apply(erule converse_rtrancl_induct_red)
 apply blast
apply(blast dest: Red_fv Red_dom_lcl)
done


text‹Now a few lemmas on the behaviour of blocks during reduction.›


lemma override_on_upd_lemma:
  "(override_on f (g(ab)) A)(a := g a) = override_on f g (insert a A)"

apply(rule ext)
apply(simp add:override_on_def)
done

declare fun_upd_apply[simp del] map_upds_twist[simp del]




lemma assumes wf:"wf_prog wf_md P"
  shows blocksReds:
  "l0 E vs'.  length Vs = length Ts; length vs = length Ts; 
        distinct Vs; ⌦‹∀T∈set Ts. is_type P T;› P  Ts Casts vs to vs';
        P,E(Vs [↦] Ts)  e, (h0,l0(Vs [↦] vs')) →* e', (h1,l1) 
   vs''. P,E  blocks(Vs,Ts,vs,e), (h0,l0) →* 
                   blocks(Vs,Ts,vs'',e'), (h1,override_on l1 l0 (set Vs))  
             (ws. P  Ts Casts vs'' to ws)  length vs = length vs''"

proof(induct Vs Ts vs e rule:blocks_old_induct)
  case (5 V Vs T Ts v vs e)
  have length1:"length (V#Vs) = length (T#Ts)"
    and length2:"length (v#vs) = length (T#Ts)"
    and dist:"distinct (V#Vs)"
    and casts:"P  (T#Ts) Casts (v#vs) to vs'"
    and reds:"P,E(V#Vs [↦] T#Ts)  e,(h0,l0(V#Vs [↦] vs')) →* e',(h1,l1)"
    and IH:"l0 E vs''. length Vs = length Ts; length vs = length Ts; 
       distinct Vs; P  Ts Casts vs to vs'';
       P,E(Vs [↦] Ts)  e,(h0,l0(Vs [↦] vs'')) →* e',(h1,l1)
         vs''. P,E  blocks (Vs,Ts,vs,e),(h0,l0) →*
                         blocks (Vs,Ts,vs'',e'),(h1, override_on l1 l0 (set Vs)) 
                   (ws. P  Ts Casts vs'' to ws)  length vs = length vs''" by fact+
  from length1 have length1':"length Vs = length Ts" by simp
  from length2 have length2':"length vs = length Ts" by simp
  from dist have dist':"distinct Vs" by simp
  from casts obtain x xs where vs':"vs' = x#xs"
    by(cases vs',auto dest:length_Casts_vs')
  with reds
  have reds':"P,E(V  T)(Vs [↦] Ts)  e,(h0,l0(V  x)(Vs [↦] xs)) 
                                    →* e',(h1,l1)"
    by simp
  from casts vs' have casts':"P  Ts Casts vs to xs" 
    and cast':"P  T casts v to x"
    by(auto elim:Casts_to.cases)
  from IH[OF length1' length2' dist' casts' reds']
  obtain vs'' ws
    where blocks:"P,E(V  T)  blocks (Vs, Ts, vs, e),(h0, l0(V  x)) →*
             blocks (Vs, Ts, vs'', e'),(h1, override_on l1 (l0(V  x)) (set Vs))"
    and castsws:"P  Ts Casts vs'' to ws"
    and lengthvs'':"length vs = length vs''" by auto
  from InitBlockReds[OF blocks cast' wf] obtain v'' w where
    blocks':"P,E  {V:T; V:=Val v;; blocks (Vs, Ts, vs, e)},(h0, l0) →*
                   {V:T; V:=Val v'';; blocks (Vs, Ts, vs'', e')},
                    (h1, (override_on l1 (l0(V  x)) (set Vs))(V := l0 V))"
    and "P  T casts v'' to w" by auto
  with castsws have "P  T#Ts Casts v''#vs'' to w#ws"
    by -(rule Casts_Cons)
  with blocks' lengthvs'' show ?case
    by(rule_tac x="v''#vs''" in exI,auto simp:override_on_upd_lemma)
next
  case (6 e)
  have casts:"P  [] Casts [] to vs'" 
    and step:"P,E([] [↦] [])  e,(h0, l0([] [↦] vs')) →* e',(h1, l1)" by fact+
  from casts have "vs' = []" by(fastforce dest:length_Casts_vs')
  with step have "P,E  e,(h0, l0) →* e',(h1, l1)" by simp
  with casts show ?case by auto
qed simp_all



lemma assumes wf:"wf_prog wf_md P"
  shows blocksFinal:
 "E l vs'.  length Vs = length Ts; length vs = length Ts;
           ⌦‹∀T∈set Ts. is_type P T;› final e; P  Ts Casts vs to vs'  
       P,E  blocks(Vs,Ts,vs,e), (h,l) →* e, (h,l)"

proof(induct Vs Ts vs e rule:blocks_old_induct)
  case (5 V Vs T Ts v vs e)
  have length1:"length (V # Vs) = length (T # Ts)"
    and length2:"length (v # vs) = length (T # Ts)"
    and final:"final e" and casts:"P  T # Ts Casts v # vs to vs'"
    and IH:"E l vs'. length Vs = length Ts; length vs = length Ts; final e;
                   P  Ts Casts vs to vs' 
                   P,E  blocks (Vs, Ts, vs, e),(h, l) →* e,(h, l)" by fact+
  from length1 length2
  have length1':"length Vs = length Ts" and length2':"length vs = length Ts"
    by simp_all
  from casts obtain x xs where vs':"vs' = x#xs"
    by(cases vs',auto dest:length_Casts_vs')
  with casts have casts':"P  Ts Casts vs to xs" 
    and cast':"P  T casts v to x"
    by(auto elim:Casts_to.cases)
  from InitBlockReds[OF IH[OF length1' length2' final casts'] cast' wf, of V l]
  obtain v'' w
    where blocks:"P,E  {V:T; V:=Val v;; blocks (Vs, Ts, vs, e)},(h, l) →*
                        {V:T; V:=Val v'';; e},(h,l)"
    and "P  T casts v'' to w" by auto blast
  with final have "P,E  {V:T; V:=Val v'';; e},(h,l)  e,(h,l)"
    by(auto elim!:finalE intro:RedInitBlock InitBlockThrow)
  with blocks show ?case
    by -(rule_tac b="({V:T; V:=Val v'';; e},(h, l))" in rtrancl_into_rtrancl,simp_all)
qed auto



lemma assumes wfmd:"wf_prog wf_md P"
  and wf: "length Vs = length Ts" "length vs = length Ts" "distinct Vs" 
  and casts:"P  Ts Casts vs to vs'"
  and reds: "P,E(Vs [↦] Ts)  e, (h0, l0(Vs [↦] vs')) →* e', (h1, l1)"
  and fin: "final e'" and l2: "l2 = override_on l1 l0 (set Vs)"
shows blocksRedsFinal: "P,E  blocks(Vs,Ts,vs,e), (h0, l0) →* e', (h1,l2)"

proof -
  obtain vs'' ws where blocks:"P,E  blocks(Vs,Ts,vs,e), (h0, l0) →* 
                                  blocks(Vs,Ts,vs'',e'), (h1,l2)"
    and length:"length vs = length vs''"
    and casts':"P  Ts Casts vs'' to ws"
    using l2 blocksReds[OF wfmd wf casts reds]
     by auto
   have "P,E  blocks(Vs,Ts,vs'',e'), (h1,l2) →* e', (h1,l2)"
     using blocksFinal[OF wfmd _ _ fin casts'] wf length by simp
   with blocks show ?thesis by simp
qed




text‹An now the actual method call reduction lemmas.›

lemma CallRedsObj:
 "P,E  e,s →* e',s'  
  P,E  Call e Copt M es,s →* Call e' Copt M es,s'"

apply(erule rtrancl_induct2)
 apply blast
apply(erule rtrancl_into_rtrancl)
apply(simp add:CallObj)
done


lemma CallRedsParams:
 "P,E  es,s [→]* es',s'  
  P,E  Call (Val v) Copt M es,s →* Call (Val v) Copt M es',s'"

apply(erule rtrancl_induct2)
 apply blast
apply(erule rtrancl_into_rtrancl)
apply(simp add:CallParams)
done




lemma cast_lcl:
  "P,E  C(Val v),(h,l)  Val v',(h,l) 
   P,E  C(Val v),(h,l')  Val v',(h,l')"

apply(erule red.cases)
apply(auto intro:red_reds.intros)
apply(subgoal_tac "P,E  Cref (a,Cs@[C]@Cs'),(h,l')  ref (a,Cs@[C]),(h,l')")
 apply simp
apply(rule RedStaticDownCast)
done


lemma cast_env:
  "P,E  C(Val v),(h,l)  Val v',(h,l)  
   P,E'  C(Val v),(h,l)  Val v',(h,l)"

apply(erule red.cases)
apply(auto intro:red_reds.intros)
apply(subgoal_tac "P,E'  Cref (a,Cs@[C]@Cs'),(h,l)  ref (a,Cs@[C]),(h,l)")
 apply simp
apply(rule RedStaticDownCast)
done


lemma Cast_step_Cast_or_fin:
"P,E  Ce,s →* e',s'  final e'  (e''. e' = Ce'')"
by(induct rule:rtrancl_induct2,auto elim:red.cases simp:final_def)

lemma Cast_red:"P,E  e,s →* e',s'  
  (e1. e = Ce0; e' = Ce1  P,E  e0,s →* e1,s')"

proof(induct rule:rtrancl_induct2)
  case refl thus ?case by simp
next
  case (step e'' s'' e' s')
  have step:"P,E  e,s →* e'',s''"
    and Red:"((e'', s''), e', s')  Red P E"
    and cast:"e = Ce0" and cast':"e' = Ce1"
    and IH:"e1. e = Ce0; e'' = Ce1  P,E  e0,s →* e1,s''" by fact+
  from Red have red:"P,E  e'',s''  e',s'" by simp
  from step cast have "final e''  (ex. e'' = Cex)"
    by simp(rule Cast_step_Cast_or_fin)
  thus ?case
  proof(rule disjE)
    assume "final e''"
    with red show ?thesis by(auto simp:final_def)
  next
    assume "ex. e'' = Cex"
    then obtain ex where e'':"e'' = Cex" by blast
    with cast' red have "P,E  ex,s''  e1,s'"
      by(auto elim:red.cases)
    with  IH[OF cast e''] show ?thesis
      by(rule_tac b="(ex,s'')" in rtrancl_into_rtrancl,simp_all)
  qed
qed


lemma Cast_final:"P,E  Ce,s →* e',s'; final e' 
e'' s''. P,E  e,s →* e'',s''  P,E  Ce'',s''  e',s'  final e''"

proof(induct rule:rtrancl_induct2)
  case refl thus ?case by (simp add:final_def)
next
  case (step e'' s'' e' s')
  have step:"P,E  Ce,s →* e'',s''"
    and Red:"((e'', s''), e', s')  Red P E"
    and final:"final e'"
    and IH:"final e''  
   ex sx. P,E  e,s →* ex,sx  P,E  Cex,sx  e'',s''  final ex" by fact+
  from Red have red:"P,E  e'',s''  e',s'" by simp
  from step have "final e''  (ex. e'' = Cex)" by(rule Cast_step_Cast_or_fin)
  thus ?case
  proof(rule disjE)
    assume "final e''"
    with red show ?thesis by(auto simp:final_def)
  next
    assume "ex. e'' = Cex"
    then obtain ex where e'':"e'' = Cex" by blast
    with red final have final':"final ex"
      by(auto elim:red.cases simp:final_def)
    from step e'' have "P,E  e,s →* ex,s''"
      by(fastforce intro:Cast_red)
    with e'' red final' show ?thesis by blast
  qed
qed


lemma Cast_final_eq:
  assumes red:"P,E  Ce,(h,l)  e',(h,l)"
  and final:"final e" and final':"final e'"
  shows "P,E'  Ce,(h,l')  e',(h,l')"

proof -
  from red final show ?thesis
  proof(auto simp:final_def)
    fix v assume "P,E  C(Val v),(h,l)  e',(h,l)"
    with final' show "P,E'  C(Val v),(h,l')  e',(h,l')"
    proof(auto simp:final_def)
      fix v' assume "P,E  C(Val v),(h,l)  Val v',(h,l)"
      thus "P,E'  C(Val v),(h,l')  Val v',(h,l')"
        by(auto intro:cast_lcl cast_env)
    next
      fix a Cs assume "P,E  C(Val v),(h,l)  Throw (a,Cs),(h,l)"
      thus "P,E'  C(Val v),(h,l')  Throw (a,Cs),(h,l')"
        by(auto elim:red.cases intro!:RedStaticCastFail)
    qed
  next
    fix a Cs assume "P,E  C(Throw (a,Cs)),(h,l)  e',(h,l)"
    with final' show "P,E'  C(Throw (a,Cs)),(h,l')  e',(h,l')"
    proof(auto simp:final_def)
      fix v assume "P,E  C(Throw (a,Cs)),(h,l)  Val v,(h,l)"
      thus "P,E'  C(Throw (a,Cs)),(h,l')  Val v,(h,l')"
        by(auto elim:red.cases)
    next
      fix a' Cs'
      assume "P,E  C(Throw (a,Cs)),(h,l)  Throw (a',Cs'),(h,l)"
      thus "P,E'  C(Throw (a,Cs)),(h,l')  Throw (a',Cs'),(h,l')"
        by(auto elim:red.cases intro:red_reds.StaticCastThrow)
    qed
  qed
qed



lemma CallRedsFinal:
assumes wwf: "wwf_prog P"
and "P,E  e,s0 →* ref(a,Cs),s1"
      "P,E  es,s1 [→]* map Val vs,(h2,l2)"
and hp: "h2 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 size: "size vs = size pns"
and casts: "P  Ts Casts vs to vs'"
and l2': "l2' = [this  Ref(a,Cs'), pns[↦]vs']"
and body_case:"new_body = (case T' of Class D  Dbody  | _  body)"
and body: "P,E(this  Class (last Cs'), pns [↦] Ts)  new_body,(h2,l2') →* ef,(h3,l3)"
and final:"final ef"
shows "P,E  eM(es), s0 →* ef,(h3,l2)"
proof -
  have wf: "size Ts = size pns  distinct pns  this  set pns"
    and wt: "fv body  {this}  set pns"
    using assms by(fastforce dest!:select_method_wf_mdecl simp:wf_mdecl_def)+
  have "dom l3  {this}  set pns"
    using Reds_dom_lcl[OF wwf body] wt l2' set_take_subset body_case
    by (cases T') force+
  hence eql2: "override_on (l2++l3) l2 ({this}  set pns) = l2"
    by(fastforce simp add:map_add_def override_on_def fun_eq_iff)
  from wwf select have "is_class P (last Cs')"
    by (auto elim!:SelectMethodDef.cases intro:Subobj_last_isClass 
             simp:LeastMethodDef_def FinalOverriderMethodDef_def 
                  OverriderMethodDefs_def MinimalMethodDefs_def MethodDefs_def)
  hence "P  Class (last Cs') casts Ref(a,Cs') to Ref(a,Cs')"
    by(auto intro!:casts_ref Subobjs_Base simp:path_via_def appendPath_def)
  with casts
  have casts':"P  Class (last Cs')#Ts Casts Ref(a,Cs')#vs to  Ref(a,Cs')#vs'"
    by -(rule Casts_Cons)
  have 1:"P,E  eM(es),s0 →* (ref(a,Cs))M(es),s1" by(rule CallRedsObj)(rule assms(2))
  have 2:"P,E  (ref(a,Cs))M(es),s1 →*
                 (ref(a,Cs))M(map Val vs),(h2,l2)"
    by(rule CallRedsParams)(rule assms(3))
  from body[THEN Red_lcl_add, of l2]
  have body': "P,E(this  Class (last Cs'), pns [↦] Ts)  
             new_body,(h2,l2(this Ref(a,Cs'), pns[↦]vs')) →* ef,(h3,l2++l3)"
    by (simp add:l2')
  show ?thesis
  proof(cases "C. T' Class C")
    case True
    hence "P,E  (ref(a,Cs))M(map Val vs), (h2,l2)  
                 blocks(this#pns,Class(last Cs')#Ts,Ref(a,Cs')#vs,body), (h2,l2)"
      using hp "method" select size wf
      by -(rule RedCall,auto,cases T',auto)
    hence 3:"P,E  (ref(a,Cs))M(map Val vs), (h2,l2) →* 
                   blocks(this#pns,Class(last Cs')#Ts,Ref(a,Cs')#vs,body), (h2,l2)"
      by(simp add:r_into_rtrancl)
    have "P,E  blocks(this#pns,Class(last Cs')#Ts,Ref(a,Cs')#vs,body),(h2,l2) →* 
                ef,(h3,override_on (l2++l3) l2 ({this}  set pns))"
      using True wf body' wwf size final casts' body_case
      by -(rule_tac vs'="Ref(a,Cs')#vs'" in blocksRedsFinal,simp_all,cases T',auto)
    with 1 2 3 show ?thesis using eql2
      by simp
  next
    case False
    then obtain D where T':"T' = Class D" by auto
    with final body' body_case obtain s' e' where 
      body'':"P,E(this  Class (last Cs'),pns [↦] Ts)  
                           body,(h2,l2(this Ref(a,Cs'), pns[↦]vs')) →* e',s'"
      and final':"final e'" 
      and cast:"P,E(this  Class (last Cs'), pns [↦] Ts)  De',s'  
                                                           ef,(h3,l2++l3)"
      by(cases T')(auto dest:Cast_final)
    from T' have "P,E  (ref(a,Cs))M(map Val vs), (h2,l2)  
                 Dblocks(this#pns,Class(last Cs')#Ts,Ref(a,Cs')#vs,body), (h2,l2)"
      using hp "method" select size wf
      by -(rule RedCall,auto)
    hence 3:"P,E  (ref(a,Cs))M(map Val vs), (h2,l2) →* 
                  Dblocks(this#pns,Class(last Cs')#Ts,Ref(a,Cs')#vs,body),(h2,l2)"
      by(simp add:r_into_rtrancl)
    from cast final have eq:"s' = (h3,l2++l3)"
      by(auto elim:red.cases simp:final_def)
    hence "P,E  blocks(this#pns, Class (last Cs')#Ts, Ref(a,Cs')#vs,body), (h2,l2)
                 →* e',(h3,override_on (l2++l3) l2 ({this}  set pns))"
      using wf body'' wwf size final' casts'
      by -(rule_tac vs'="Ref(a,Cs')#vs'" in blocksRedsFinal,simp_all)
    hence "P,E  D(blocks(this#pns,Class(last Cs')#Ts,Ref(a,Cs')#vs,body)),(h2,l2)
             →* De',(h3,override_on (l2++l3) l2 ({this}  set pns))"
      by(rule StaticCastReds)
    moreover
    have "P,E  De',(h3,override_on (l2++l3) l2 ({this}  set pns))  
                ef,(h3,override_on (l2++l3) l2 ({this}  set pns))"
      using eq cast final final'
      by(fastforce intro:Cast_final_eq)
    ultimately
    have "P,E  D(blocks(this#pns, Class (last Cs')#Ts, Ref(a,Cs')#vs,body)), 
                  (h2,l2) →* ef,(h3,override_on (l2++l3) l2 ({this}  set pns))"
      by(rule_tac b="(De',(h3,override_on (l2++l3) l2 ({this}  set pns)))"
        in rtrancl_into_rtrancl,simp_all)
    with 1 2 3 show ?thesis using eql2
      by simp
  qed
qed


lemma StaticCallRedsFinal:
assumes wwf: "wwf_prog P"
and "P,E  e,s0 →* ref(a,Cs),s1"
      "P,E  es,s1 [→]* map Val vs,(h2,l2)"
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@pCs'')@pCs'"
and least: "P  C has least M = (Ts,T,pns,body) via Cs'"
and size: "size vs = size pns"
and casts: "P  Ts Casts vs to vs'"
and l2': "l2' = [this  Ref(a,Ds), pns[↦]vs']"
and body: "P,E(thisClass(last Ds), pns[↦]Ts)  body,(h2,l2') →* ef,(h3,l3)"
and final:"final ef"
shows "P,E  e∙(C::)M(es), s0 →* ef,(h3,l2)"
proof -
  have wf: "size Ts = size pns  distinct pns  this  set pns  
            (Tset Ts. is_type P T)"
    and wt: "fv body  {this}  set pns"
    using assms by(fastforce dest!:has_least_wf_mdecl simp:wf_mdecl_def)+
  have "dom l3  {this}  set pns"
    using Reds_dom_lcl[OF wwf body] wt l2' set_take_subset
    by force
  hence eql2: "override_on (l2++l3) l2 ({this}  set pns) = l2"
    by(fastforce simp add:map_add_def override_on_def fun_eq_iff)
  from wwf least have "Cs'  []"
    by (auto elim!:Subobjs_nonempty simp:LeastMethodDef_def MethodDefs_def)
  with Ds have "last Cs' = last Ds" by(fastforce intro:appendPath_last)
  with wwf least have "is_class P (last Ds)"
    by(auto dest:Subobj_last_isClass simp:LeastMethodDef_def MethodDefs_def)
  hence "P  Class (last Ds) casts Ref(a,Ds) to Ref(a,Ds)"
    by(auto intro!:casts_ref Subobjs_Base simp:path_via_def appendPath_def)
  with casts
  have casts':"P  Class (last Ds)#Ts Casts Ref(a,Ds)#vs to Ref(a,Ds)#vs'"
    by -(rule Casts_Cons)
  have 1:"P,E  e∙(C::)M(es),s0 →* (ref(a,Cs))∙(C::)M(es),s1"
    by(rule CallRedsObj)(rule assms(2))
  have 2:"P,E  (ref(a,Cs))∙(C::)M(es),s1 →*
                 (ref(a,Cs))∙(C::)M(map Val vs),(h2,l2)"
    by(rule CallRedsParams)(rule assms(3))
  from body[THEN Red_lcl_add, of l2]
  have body': "P,E(thisClass(last Ds), pns[↦]Ts)  
              body,(h2,l2(this Ref(a,Ds), pns[↦]vs')) →* ef,(h3,l2++l3)"
    by (simp add:l2')
  have "P,E  (ref(a,Cs))∙(C::)M(map Val vs), (h2,l2) 
              blocks(this#pns, Class (last Ds)#Ts, Ref(a,Ds)#vs, body), (h2,l2)"
    using path_unique path_via least size wf Ds
    by -(rule RedStaticCall,auto)
  hence 3:"P,E  (ref(a,Cs))∙(C::)M(map Val vs), (h2,l2) →* 
                   blocks(this#pns,Class(last Ds)#Ts,Ref(a,Ds)#vs,body), (h2,l2)"
    by(simp add:r_into_rtrancl)
  have "P,E  blocks(this#pns,Class(last Ds)#Ts,Ref(a,Ds)#vs,body),(h2,l2) →* 
                ef,(h3,override_on (l2++l3) l2 ({this}  set pns))"
    using wf body' wwf size final casts'
    by -(rule_tac vs'="Ref(a,Ds)#vs'" in blocksRedsFinal,simp_all)
  with 1 2 3 show ?thesis using eql2
    by simp
qed



lemma CallRedsThrowParams:
  " P,E  e,s0 →* Val v,s1;  
    P,E  es,s1 [→]* map Val vs1 @ Throw ex # es2,s2 
   P,E  Call e Copt M es,s0 →* Throw ex,s2"

apply(rule rtrancl_trans)
 apply(erule CallRedsObj)
apply(rule rtrancl_into_rtrancl)
 apply(erule CallRedsParams)
apply(simp add:CallThrowParams)
done



lemma CallRedsThrowObj:
  "P,E  e,s0 →* Throw ex,s1  P,E  Call e Copt M es,s0 →* Throw ex,s1"

apply(rule rtrancl_into_rtrancl)
 apply(erule CallRedsObj)
apply(simp add:CallThrowObj)
done



lemma CallRedsNull:
  " P,E  e,s0 →* null,s1; P,E  es,s1 [→]* map Val vs,s2 
   P,E  Call e Copt M es,s0 →* THROW NullPointer,s2"

apply(rule rtrancl_trans)
 apply(erule CallRedsObj)
apply(rule rtrancl_into_rtrancl)
 apply(erule CallRedsParams)
apply(simp add:RedCallNull)
done



subsection ‹The main Theorem›

lemma assumes wwf: "wwf_prog P"
shows big_by_small: "P,E  e,s  e',s'  P,E  e,s →* e',s'"
and bigs_by_smalls: "P,E  es,s [⇒] es',s'  P,E  es,s [→]* es',s'"

proof (induct rule: eval_evals.inducts)
  case New thus ?case by (auto simp:RedNew)
next
  case NewFail thus ?case by (auto simp:RedNewFail)
next
  case StaticUpCast thus ?case by(simp add:StaticUpCastReds)
next
  case StaticDownCast thus ?case by(simp add:StaticDownCastReds)
next
  case StaticCastNull thus ?case by(simp add:StaticCastRedsNull)
next
  case StaticCastFail thus ?case by(simp add:StaticCastRedsFail)
next
  case StaticCastThrow thus ?case by(auto dest!:eval_final simp:StaticCastRedsThrow)
next
  case StaticUpDynCast thus ?case by(simp add:StaticUpDynCastReds)
next
  case StaticDownDynCast thus ?case by(simp add:StaticDownDynCastReds)
next
  case DynCast thus ?case by(fastforce intro:DynCastRedsRef)
next
  case DynCastNull thus ?case by(simp add:DynCastRedsNull)
next
  case DynCastFail thus ?case by(fastforce intro!:DynCastRedsFail)
next
  case DynCastThrow thus ?case by(auto dest!:eval_final simp:DynCastRedsThrow)
next
  case Val thus ?case by simp
next
  case BinOp thus ?case by(fastforce simp:BinOpRedsVal)
next
  case BinOpThrow1 thus ?case by(fastforce dest!:eval_final simp: BinOpRedsThrow1)
next
  case BinOpThrow2 thus ?case by(fastforce dest!:eval_final simp: BinOpRedsThrow2)
next
  case Var thus ?case by (fastforce simp:RedVar)
next
  case LAss thus ?case by(fastforce simp: LAssRedsVal)
next
  case LAssThrow thus ?case by(fastforce dest!:eval_final simp: LAssRedsThrow)
next
  case FAcc thus ?case by(fastforce intro:FAccRedsVal)
next
  case FAccNull thus ?case by(simp add:FAccRedsNull)
next
  case FAccThrow thus ?case by(fastforce dest!:eval_final simp:FAccRedsThrow)
next
  case FAss thus ?case by(fastforce simp:FAssRedsVal)
next
  case FAssNull thus ?case by(fastforce simp:FAssRedsNull)
next
  case FAssThrow1 thus ?case by(fastforce dest!:eval_final simp:FAssRedsThrow1)
next
  case FAssThrow2 thus ?case by(fastforce dest!:eval_final simp:FAssRedsThrow2)
next
  case CallObjThrow thus ?case by(fastforce dest!:eval_final simp:CallRedsThrowObj)
next
  case CallNull thus ?case thm CallRedsNull by(simp add:CallRedsNull)
next
  case CallParamsThrow thus ?case
    by(fastforce dest!:evals_final simp:CallRedsThrowParams)
next
  case (Call E e s0 a Cs s1 ps vs h2 l2 C S M Ts' T' pns' body' Ds Ts T pns
             body Cs' vs' l2' new_body e' h3 l3)
  have IHe: "P,E  e,s0 →* ref(a,Cs),s1"
    and IHes: "P,E  ps,s1 [→]* map Val vs,(h2,l2)"
    and h2a: "h2 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 same_length: "length vs = length pns"
    and casts: "P  Ts Casts vs to vs'"
    and l2': "l2' = [this  Ref (a,Cs'), pns[↦]vs']"
    and body_case: "new_body = (case T' of Class D  Dbody | _  body)"
    and eval_body: "P,E(this  Class (last Cs'), pns [↦] Ts)  
                      new_body,(h2, l2')  e',(h3, l3)"
    and IHbody: "P,E(this  Class (last Cs'), pns [↦] Ts)  
                      new_body,(h2, l2') →* e',(h3, l3)" by fact+
  from wwf select same_length have lengthTs:"length Ts = length vs"
    by (fastforce dest!:select_method_wf_mdecl simp:wf_mdecl_def)
  show "P,E  eM(ps),s0 →* e',(h3, l2)"
    using "method" select same_length l2' h2a casts body_case
      IHbody eval_final[OF eval_body]
    by(fastforce intro!:CallRedsFinal[OF wwf IHe IHes])
next
  case (StaticCall E e s0 a Cs s1 ps vs h2 l2 C Cs'' M Ts T pns body Cs'
                   Ds vs' l2' e' h3 l3)
 have IHe: "P,E  e,s0 →* ref(a,Cs),s1"
   and IHes: "P,E  ps,s1 [→]* map Val vs,(h2,l2)"
   and path_unique: "P  Path last Cs to C unique"
   and path_via: "P  Path last Cs to C via Cs''"
   and least: "P  C has least M = (Ts, T, pns, body) via Cs'"
   and Ds: "Ds = (Cs @p Cs'') @p Cs'"
   and same_length: "length vs = length pns"
   and casts: "P  Ts Casts vs to vs'"
   and l2': "l2' = [this  Ref (a,Ds), pns[↦]vs']"
   and eval_body: "P,E(this  Class (last Ds), pns [↦] Ts)  
                         body,(h2, l2')  e',(h3, l3)"
   and IHbody: "P,E(this  Class (last Ds), pns [↦] Ts)  
                      body,(h2, l2') →* e',(h3, l3)" by fact+
 from wwf least same_length have lengthTs:"length Ts = length vs"
    by (fastforce dest!:has_least_wf_mdecl simp:wf_mdecl_def)
  show "P,E  e∙(C::)M(ps),s0 →* e',(h3, l2)"
    using path_unique path_via least Ds same_length l2' casts
      IHbody eval_final[OF eval_body]
    by(fastforce intro!:StaticCallRedsFinal[OF wwf IHe IHes])
next
  case Block with wwf show ?case by(fastforce simp: BlockRedsFinal dest:eval_final)
next
  case Seq thus ?case by(fastforce simp:SeqReds2)
next
  case SeqThrow thus ?case by(fastforce dest!:eval_final simp: SeqRedsThrow)
next
  case CondT thus ?case by(fastforce simp:CondReds2T)
next
  case CondF thus ?case by(fastforce simp:CondReds2F)
next
  case CondThrow thus ?case by(fastforce dest!:eval_final simp:CondRedsThrow)
next
  case WhileF thus ?case by(fastforce simp:WhileFReds)
next
  case WhileT thus ?case by(fastforce simp: WhileTReds)
next
  case WhileCondThrow thus ?case by(fastforce dest!:eval_final simp: WhileRedsThrow)
next
  case WhileBodyThrow thus ?case by(fastforce dest!:eval_final simp: WhileTRedsThrow)
next
  case Throw thus ?case by(fastforce simp:ThrowReds)
next
  case ThrowNull thus ?case by(fastforce simp:ThrowRedsNull)
next
  case ThrowThrow thus ?case by(fastforce dest!:eval_final simp:ThrowRedsThrow)
next
  case Nil thus ?case by simp
next
  case Cons thus ?case
    by(fastforce intro!:Cons_eq_appendI[OF refl refl] ListRedsVal)
next
  case ConsThrow thus ?case by(fastforce elim: ListReds1)
qed



subsection‹Big steps simulates small step›


text ‹The big step equivalent of RedWhile›:› 

lemma unfold_while: 
  "P,E  while(b) c,s  e',s'  =  P,E  if(b) (c;;while(b) c) else (unit),s  e',s'"

proof
  assume "P,E  while (b) c,s  e',s'"
  thus "P,E  if (b) (c;; while (b) c) else unit,s  e',s'"
    by cases (fastforce intro: eval_evals.intros)+
next
  assume "P,E  if (b) (c;; while (b) c) else unit,s  e',s'"
  thus "P,E  while (b) c,s  e',s'"
  proof (cases)
    fix ex
    assume e': "e' = throw ex"
    assume "P,E  b,s  throw ex,s'"  
    hence "P,E  while(b) c,s  throw ex,s'" by (rule WhileCondThrow)
    with e' show ?thesis by simp
  next
    fix s1
    assume eval_false: "P,E  b,s  false,s1"
    and eval_unit: "P,E  unit,s1  e',s'"
    with eval_unit have "s' = s1" "e' = unit" by (auto elim: eval_cases)
    moreover from eval_false have "P,E  while (b) c,s  unit,s1"
      by - (rule WhileF, simp)
    ultimately show ?thesis by simp
  next
    fix s1
    assume eval_true: "P,E  b,s  true,s1"
    and eval_rest: "P,E  c;; while (b) c,s1e',s'"
    from eval_rest show ?thesis
    proof (cases)
      fix s2 v1
      assume "P,E  c,s1  Val v1,s2" "P,E  while (b) c,s2  e',s'"
      with eval_true show "P,E  while(b) c,s  e',s'" by (rule WhileT)
    next
      fix ex
      assume "P,E  c,s1  throw ex,s'" "e' = throw ex"
      with eval_true show "P,E  while(b) c,s  e',s'"
        by (iprover intro: WhileBodyThrow)
    qed
  qed
qed



lemma blocksEval:
  "Ts vs l l' E. size ps = size Ts; size ps = size vs; 
                    P,E  blocks(ps,Ts,vs,e),(h,l)  e',(h',l') 
      l'' vs'. P,E(ps [↦] Ts)  e,(h,l(ps[↦]vs'))  e',(h',l'') 
                   P  Ts Casts vs to vs'  length vs' = length vs"

proof (induct ps)
  case Nil then show ?case by(fastforce intro:Casts_Nil)
next
  case (Cons p ps')
  have length_eqs: "length (p # ps') = length Ts" 
                   "length (p # ps') = length vs"
    and IH:"Ts vs l l' E. length ps' = length Ts; length ps' = length vs;
                             P,E  blocks (ps',Ts,vs,e),(h,l)  e',(h',l')
   l'' vs'. P,E(ps' [↦] Ts)  e,(h,l(ps' [↦] vs'))  e',(h', l'') 
                P  Ts Casts vs to vs'  length vs' = length vs" by fact+
  then obtain T Ts' where Ts: "Ts = T#Ts'" by (cases "Ts") simp
  obtain v vs' where vs: "vs = v#vs'" using length_eqs by (cases "vs") simp
  with length_eqs Ts have length1:"length ps' = length Ts'" 
    and length2:"length ps' = length vs'" by simp_all
  have "P,E  blocks (p # ps', Ts, vs, e),(h,l)  e',(h', l')" by fact
  with Ts vs
  have blocks:"P,E  {p:T := Val v; blocks (ps',Ts',vs',e)},(h,l)  e',(h',l')"
    by simp
  then obtain l''' v' where
    eval_ps': "P,E(p  T)  blocks (ps',Ts',vs',e),(h,l(pv'))  e',(h',l''')"
    and l''': "l'=l'''(p:=l p)"
    and casts:"P  T casts v to v'"
    by(auto elim!: eval_cases simp:fun_upd_same)
  from IH[OF length1 length2 eval_ps'] obtain l'' vs'' where
    "P,E(p  T)(ps' [↦] Ts')  e,(h, l(pv')(ps'[↦]vs''))  
                                       e',(h',l'')"
    and "P  Ts' Casts vs' to vs''"
    and "length vs'' = length vs'" by auto
  with Ts vs casts show ?case
    by -(rule_tac x="l''" in exI,rule_tac x="v'#vs''" in exI,simp,
         rule Casts_Cons)
qed



lemma CastblocksEval:
  "Ts vs l l' E. size ps = size Ts; size ps = size vs; 
                   P,E  C'(blocks(ps,Ts,vs,e)),(h,l)  e',(h',l') 
      l'' vs'. P,E(ps [↦] Ts)  C'e,(h,l(ps[↦]vs'))  e',(h',l'') 
                   P  Ts Casts vs to vs'  length vs' = length vs"

proof (induct ps)
  case Nil then show ?case by(fastforce intro:Casts_Nil)
next
  case (Cons p ps')
  have length_eqs: "length (p # ps') = length Ts" 
                   "length (p # ps') = length vs" by fact+
  then obtain T Ts' where Ts: "Ts = T#Ts'" by (cases "Ts") simp
  obtain v vs' where vs: "vs = v#vs'" using length_eqs by (cases "vs") simp
  with length_eqs Ts have length1:"length ps' = length Ts'" 
    and length2:"length ps' = length vs'" by simp_all
  have "P,E  C'(blocks (p # ps', Ts, vs, e)),(h,l)  e',(h', l')" by fact
  moreover
  { fix a Cs Cs'
    assume blocks:"P,E  blocks(p#ps',Ts,vs,e),(h,l)  ref (a,Cs),(h',l')"
      and path_via:"P  Path last Cs to C' via Cs'"
      and e':"e' = ref(a,Cs@pCs')"
    from blocks length_eqs obtain l'' vs''
      where eval:"P,E(p#ps' [↦] Ts)  e,(h,l(p#ps'[↦]vs''))  
                                 ref (a,Cs),(h',l'')"
      and casts:"P  Ts Casts vs to vs''"
      and length:"length vs'' = length vs"
      by -(drule blocksEval,auto)
    from eval path_via have 
      "P,E(p#ps'[↦]Ts)  C'e,(h,l(p#ps'[↦]vs''))  ref(a,Cs@pCs'),(h',l'')"
      by(auto intro:StaticUpCast)
    with e' casts length have ?case by simp blast }
  moreover
  { fix a Cs Cs'
    assume blocks:"P,E  blocks(p#ps',Ts,vs,e),(h,l)  
                         ref (a,Cs@C'# Cs'),(h',l')"
      and e':"e' = ref (a,Cs@[C'])"
    from blocks length_eqs obtain l'' vs''
      where eval:"P,E(p#ps' [↦] Ts)  e,(h,l(p#ps'[↦]vs''))  
                                 ref (a,Cs@C'# Cs'),(h',l'')"
      and casts:"P  Ts Casts vs to vs''"
      and length:"length vs'' = length vs"
      by -(drule blocksEval,auto)
    from eval have "P,E(p#ps'[↦]Ts)  C'e,(h,l(p#ps'[↦]vs''))  
                                             ref(a,Cs@[C']),(h',l'')"
      by(auto intro:StaticDownCast)
    with e' casts length have ?case by simp blast }
  moreover
  { assume "P,E  blocks(p#ps',Ts,vs,e),(h,l)  null,(h',l')"
    and e':"e' = null"
    with length_eqs obtain l'' vs''
      where eval:"P,E(p#ps' [↦] Ts)  e,(h,l(p#ps'[↦]vs''))  
                                 null,(h',l'')"
      and casts:"P  Ts Casts vs to vs''"
      and length:"length vs'' = length vs"
      by -(drule blocksEval,auto)
    from eval have "P,E(p#ps' [↦] Ts)  C'e,(h,l(p#ps'[↦]vs''))  
                                               null,(h',l'')"
      by(auto intro:StaticCastNull)
    with e' casts length have ?case by simp blast }
  moreover
  { fix a Cs
    assume blocks:"P,E  blocks(p#ps',Ts,vs,e),(h,l)  ref (a,Cs),(h',l')"
      and notin:"C'  set Cs" and leq:"¬ P  (last Cs) * C'"
      and  e':"e' = THROW ClassCast"
    from blocks length_eqs obtain l'' vs''
      where eval:"P,E(p#ps' [↦] Ts)  e,(h,l(p#ps'[↦]vs''))  
                                 ref (a,Cs),(h',l'')"
      and casts:"P  Ts Casts vs to vs''"
      and length:"length vs'' = length vs"
      by -(drule blocksEval,auto)
    from eval notin leq have 
      "P,E(p#ps'[↦]Ts)  C'e,(h,l(p#ps'[↦]vs''))  
                          THROW ClassCast,(h',l'')"
      by(auto intro:StaticCastFail)
    with e' casts length have ?case by simp blast }
  moreover
  { fix r assume "P,E  blocks(p#ps',Ts,vs,e),(h,l)  throw r,(h',l')"
    and e':"e' = throw r"
     with length_eqs obtain l'' vs''
      where eval:"P,E(p#ps' [↦] Ts)  e,(h,l(p#ps'[↦]vs''))  
                                 throw r,(h',l'')"
      and casts:"P  Ts Casts vs to vs''"
      and length:"length vs'' = length vs"
      by -(drule blocksEval,auto)
    from eval have 
      "P,E(p#ps'[↦]Ts)  C'e,(h,l(p#ps'[↦]vs''))  
                          throw r,(h',l'')"
      by(auto intro:eval_evals.StaticCastThrow)
    with e' casts length have ?case by simp blast }
  ultimately show ?case
    by -(erule eval_cases,fastforce+)
qed



lemma
assumes wf: "wwf_prog P"
shows eval_restrict_lcl:
  "P,E  e,(h,l)  e',(h',l')  (W. fv e  W  P,E  e,(h,l|`W)  e',(h',l'|`W))"
and "P,E  es,(h,l) [⇒] es',(h',l')  (W. fvs es  W  P,E  es,(h,l|`W) [⇒] es',(h',l'|`W))"

proof(induct rule:eval_evals_inducts)
  case (Block E V T e0 h0 l0 e1 h1 l1)
  have IH: "W. fv e0  W  
                 P,E(V  T)  e0,(h0,l0(V:=None)|`W)  e1,(h1,l1|`W)" by fact
  (*have type:"is_type P T" .*)
  have "fv({V:T; e0})  W" by fact
  hence "fv e0 - {V}  W" by simp_all
  hence "fv e0  insert V W" by fast
  with IH[OF this]
  have "P,E(V  T)  e0,(h0, (l0|`W)(V := None))  e1,(h1, l1|`insert V W)"
    by fastforce
  from eval_evals.Block[OF this] show ?case by fastforce
next
  case Seq thus ?case by simp (blast intro:eval_evals.Seq)
next
  case New thus ?case by(simp add:eval_evals.intros)
next
  case NewFail thus ?case by(simp add:eval_evals.intros)
next
  case StaticUpCast thus ?case by simp (blast intro:eval_evals.StaticUpCast)
next
  case (StaticDownCast E e h l a Cs C Cs' h' l')
  have IH:"W. fv e  W  
                P,E  e,(h,l |` W)  ref(a,Cs@[C]@Cs'),(h',l' |` W)" by fact
  have "fv (Ce)  W" by fact
  hence "fv e  W" by simp
  from IH[OF this] show ?case by(rule eval_evals.StaticDownCast)
next
  case StaticCastNull thus ?case by simp (blast intro:eval_evals.StaticCastNull)
next
  case StaticCastFail thus ?case by simp (blast intro:eval_evals.StaticCastFail)
next
  case StaticCastThrow thus ?case by(simp add:eval_evals.intros)
next
  case DynCast thus ?case by simp (blast intro:eval_evals.DynCast)
next
  case StaticUpDynCast thus ?case by simp (blast intro:eval_evals.StaticUpDynCast)
next
  case (StaticDownDynCast E e h l a Cs C Cs' h' l')
  have IH:"W. fv e  W  
                P,E  e,(h,l |` W)  ref(a,Cs@[C]@Cs'),(h',l' |` W)" by fact
  have "fv (Cast C e)  W" by fact
  hence "fv e  W" by simp
  from IH[OF this] show ?case by(rule eval_evals.StaticDownDynCast)
next
  case DynCastNull thus ?case by simp (blast intro:eval_evals.DynCastNull)
next
  case DynCastFail thus ?case by simp (blast intro:eval_evals.DynCastFail)
next
  case DynCastThrow thus ?case by(simp add:eval_evals.intros)
next
  case Val thus ?case by(simp add:eval_evals.intros)
next
  case BinOp thus ?case by simp (blast intro:eval_evals.BinOp)
next
  case BinOpThrow1 thus ?case by simp (blast intro:eval_evals.BinOpThrow1)
next
  case BinOpThrow2 thus ?case by simp (blast intro:eval_evals.BinOpThrow2)
next
  case Var thus ?case by(simp add:eval_evals.intros)
next
  case (LAss E e h0 l0 v h l V T v' l')
  have IH: "W. fv e  W  P,E  e,(h0,l0|`W)  Val v,(h,l|`W)"
    and env:"E V = T" and casts:"P  T casts v to v'"
    and [simp]: "l' = l(V  v')" by fact+
  have "fv (V:=e)  W" by fact
  hence fv: "fv e  W" and VinW: "V  W" by auto
  from eval_evals.LAss[OF IH[OF fv] _ casts] env VinW
  show ?case by fastforce
next
  case LAssThrow thus ?case by(fastforce intro: eval_evals.LAssThrow)
next
  case FAcc thus ?case by simp (blast intro: eval_evals.FAcc)
next
  case FAccNull thus ?case by(fastforce intro: eval_evals.FAccNull)
next
  case FAccThrow thus ?case by(fastforce intro: eval_evals.FAccThrow)
next
  case (FAss E e1 h l a Cs' h' l' e2 v h2 l2 D S F T Cs v' Ds fs fs' S' h2' W)
  have IH1: "W. fv e1  W  P,E  e1,(h, l|`W)  ref (a, Cs'),(h', l'|`W)"
    and IH2: "W. fv e2  W  P,E  e2,(h', l'|`W)  Val v,(h2, l2|`W)"
    and fv:"fv (e1F{Cs} := e2)  W"
    and h:"h2 a = Some(D,S)" and Ds:"Ds = Cs' @p Cs"
    and S:"(Ds,fs)  S" and fs':"fs' = fs(F  v')"
    and S':"S' = S - {(Ds, fs)}  {(Ds, fs')}" 
    and h':"h2' = h2(a  (D, S'))" 
    and field:"P  last Cs' has least F:T via Cs"
    and casts:"P  T casts v to v'" by fact+
  from fv have fv1:"fv e1  W" and fv2:"fv e2  W" by auto
  from eval_evals.FAss[OF IH1[OF fv1] IH2[OF fv2] _ field casts] h Ds S fs' S' h'
  show ?case by simp
next
  case FAssNull thus ?case by simp (blast intro: eval_evals.FAssNull)
next
  case FAssThrow1 thus ?case by simp (blast intro: eval_evals.FAssThrow1)
next
  case FAssThrow2 thus ?case by simp (blast intro: eval_evals.FAssThrow2)
next
  case CallObjThrow thus ?case by simp (blast intro: eval_evals.intros)
next
  case CallNull thus ?case by simp (blast intro: eval_evals.CallNull)
next
  case CallParamsThrow thus ?case
    by simp (blast intro: eval_evals.CallParamsThrow)
next
  case (Call E e h0 l0 a Cs h1 l1 ps vs h2 l2 C S M Ts' T' pns'
             body' Ds Ts T pns body Cs' vs' l2' new_body e' h3 l3 W)
  have IHe: "W. fv e  W  P,E  e,(h0,l0|`W)  ref(a,Cs),(h1,l1|`W)"
    and IHps: "W. fvs ps  W  P,E  ps,(h1,l1|`W) [⇒] map Val vs,(h2,l2|`W)"
    and IHbd: "W. fv new_body  W  P,E(this  Class (last Cs'), pns [↦] Ts)  
                                    new_body,(h2,l2'|`W)  e',(h3,l3|`W)"
    and h2a: "h2 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 same_len: "size vs = size pns"
    and casts:"P  Ts Casts vs to vs'"
    and l2': "l2' = [this  Ref(a,Cs'), pns [↦] vs']"
    and body_case: "new_body = (case T' of Class D  Dbody | _  body)" by fact+
  have "fv (eM(ps))  W" by fact
  hence fve: "fv e  W" and fvps: "fvs(ps)  W" by auto
  have wfmethod: "size Ts = size pns  this  set pns" and
       fvbd: "fv body  {this}  set pns"
    using select wf by(fastforce dest!:select_method_wf_mdecl simp:wf_mdecl_def)+
  from fvbd body_case have fvbd':"fv new_body  {this}  set pns"
    by(cases T') auto
  from l2' have "l2' |` ({this}  set pns) = [this  Ref (a, Cs'), pns [↦] vs']"
    by (auto intro!:ext simp:restrict_map_def fun_upd_def)
  with eval_evals.Call[OF IHe[OF fve] IHps[OF fvps] _ "method" select same_len
                          casts _ body_case IHbd[OF fvbd']] h2a
  show ?case by simp
next
  case (StaticCall E e h0 l0 a Cs h1 l1 ps vs h2 l2 C Cs'' M Ts T pns body
                   Cs' Ds vs' l2' e' h3 l3 W)
  have IHe: "W. fv e  W  P,E  e,(h0,l0|`W)  ref(a,Cs),(h1,l1|`W)"
    and IHps: "W. fvs ps  W  P,E  ps,(h1,l1|`W) [⇒] map Val vs,(h2,l2|`W)"
    and IHbd: "W. fv body  W  P,E(this  Class (last Ds), pns [↦] Ts)  
                                    body,(h2,l2'|`W)  e',(h3,l3|`W)"
    and path_unique: "P  Path last Cs to C unique"
    and path_via: "P  Path last Cs to C via Cs''"
    and least: "P  C has least M = (Ts, T, pns, body) via Cs'"
    and Ds: "Ds = (Cs @p Cs'') @p Cs'"
    and same_len: "size vs = size pns"
    and casts:"P  Ts Casts vs to vs'"
    and l2': "l2' = [this  Ref(a,Ds), pns [↦] vs']" by fact+
  have "fv (e∙(C::)M(ps))  W" by fact
  hence fve: "fv e  W" and fvps: "fvs(ps)  W" by auto
  have wfmethod: "size Ts = size pns  this  set pns" and
       fvbd: "fv body  {this}  set pns"
    using least wf by(fastforce dest!:has_least_wf_mdecl simp:wf_mdecl_def)+
  from fvbd have fvbd':"fv body  {this}  set pns"
    by auto
  from l2' have "l2' |` ({this}  set pns) = [this  Ref(a,Ds), pns [↦] vs']"
    by (auto intro!:ext simp:restrict_map_def fun_upd_def)
  with eval_evals.StaticCall[OF IHe[OF fve] IHps[OF fvps] path_unique path_via
                                least Ds same_len casts _ IHbd[OF fvbd']]
  show ?case by simp
next
  case SeqThrow thus ?case by simp (blast intro: eval_evals.SeqThrow)
next
  case CondT thus ?case by simp (blast intro: eval_evals.CondT)
next
  case CondF thus ?case by simp (blast intro: eval_evals.CondF)
next
  case CondThrow thus ?case by simp (blast intro: eval_evals.CondThrow)
next
  case WhileF thus ?case by simp (blast intro: eval_evals.WhileF)
next
  case WhileT thus ?case by simp (blast intro: eval_evals.WhileT)
next
  case WhileCondThrow thus ?case by simp (blast intro: eval_evals.WhileCondThrow)
next
  case WhileBodyThrow thus ?case by simp (blast intro: eval_evals.WhileBodyThrow)
next
  case Throw thus ?case by simp (blast intro: eval_evals.Throw)
next
  case ThrowNull thus ?case by simp (blast intro: eval_evals.ThrowNull)
next
  case ThrowThrow thus ?case by simp (blast intro: eval_evals.ThrowThrow)
next
  case Nil thus ?case by (simp add: eval_evals.Nil)
next
  case Cons thus ?case by simp (blast intro: eval_evals.Cons)
next
  case ConsThrow thus ?case by simp (blast intro: eval_evals.ConsThrow)
qed



lemma eval_notfree_unchanged:
assumes wf:"wwf_prog P"
shows "P,E  e,(h,l)  e',(h',l')  (V. V  fv e  l' V = l V)"
and "P,E  es,(h,l) [⇒] es',(h',l')  (V. V  fvs es  l' V = l V)"

proof(induct rule:eval_evals_inducts)
  case LAss thus ?case by(simp add:fun_upd_apply)
next
  case Block thus ?case
    by (simp only:fun_upd_apply split:if_splits) fastforce
qed simp_all



lemma eval_closed_lcl_unchanged:
  assumes wf:"wwf_prog P"
  and eval:"P,E  e,(h,l)  e',(h',l')"
  and fv:"fv e = {}"
  shows "l' = l"

proof -
  from wf eval have "V. V  fv e  l' V = l V" by (rule eval_notfree_unchanged)
  with fv have "V. l' V = l V" by simp
  thus ?thesis by(simp add:fun_eq_iff)
qed



(* Hiermit kann man die ganze pair-Splitterei in den automatischen Taktiken
abschalten. Wieder anschalten siehe nach dem Beweis. *)

declare split_paired_All [simp del] split_paired_Ex [simp del]

declaration ‹K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac"))
setup map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac")


lemma list_eval_Throw: 
assumes eval_e: "P,E  throw x,s  e',s'"
shows "P,E  map Val vs @ throw x # es',s [⇒] map Val vs @ e' # es',s'"

proof -
  from eval_e 
  obtain a where e': "e' = Throw a"
    by (cases) (auto dest!: eval_final)
  {
    fix es
    have "vs. es = map Val vs @ throw x # es' 
            P,E  es,s[⇒]map Val vs @ e' # es',s'"
    proof (induct es type: list)
      case Nil thus ?case by simp
    next
      case (Cons e es vs)
      have e_es: "e # es = map Val vs @ throw x # es'" by fact
      show "P,E  e # es,s [⇒] map Val vs @ e' # es',s'"
      proof (cases vs)
        case Nil
        with e_es obtain "e=throw x" "es=es'" by simp
        moreover from eval_e e'
        have "P,E  throw x # es,s [⇒] Throw a # es,s'"
          by (iprover intro: ConsThrow)
        ultimately show ?thesis using Nil e' by simp
      next
        case (Cons v vs')
        have vs: "vs = v # vs'" by fact
        with e_es obtain 
          e: "e=Val v" and es:"es= map Val vs' @ throw x # es'"
          by simp
        from e 
        have "P,E  e,s  Val v,s"
          by (iprover intro: eval_evals.Val)
        moreover from es 
        have "P,E  es,s [⇒] map Val vs' @ e' # es',s'"
          by (rule Cons.hyps)
        ultimately show 
          "P,E  e#es,s [⇒] map Val vs @ e' # es',s'"
          using vs by (auto intro: eval_evals.Cons)
      qed
    qed
  }
  thus ?thesis
    by simp
qed




text ‹The key lemma:›

lemma
assumes wf: "wwf_prog P"
shows extend_1_eval:
  "P,E  e,s  e'',s''   (s' e'. P,E  e'',s''  e',s'  P,E  e,s  e',s')"
and extend_1_evals:
  "P,E  es,t [→] es'',t''  (t' es'. P,E  es'',t'' [⇒] es',t'  P,E  es,t [⇒] es',t')"

proof (induct rule: red_reds.inducts)
 case RedNew thus ?case by (iprover elim: eval_cases intro: eval_evals.intros)
next
  case RedNewFail thus ?case by (fastforce elim: eval_cases intro: eval_evals.intros)
next
  case (StaticCastRed E e s e'' s'' C s' e') thus ?case
    by -(erule eval_cases,auto intro:eval_evals.intros,
         subgoal_tac "P,E  e'',s''  ref(a,Cs@[C]@Cs'),s'",
         rule_tac Cs'="Cs'" in StaticDownCast,auto)
next
  case RedStaticCastNull thus ?case
    by (fastforce elim: eval_cases intro: eval_evals.intros)
next
  case RedStaticUpCast thus ?case
    by (fastforce elim: eval_cases intro: eval_evals.intros)
next
  case RedStaticDownCast thus ?case
    by (fastforce elim: eval_cases intro: eval_evals.intros)
next
  case RedStaticCastFail thus ?case
    by (fastforce elim: eval_cases intro: eval_evals.intros)
next
  case RedStaticUpDynCast thus ?case
    by (fastforce elim: eval_cases intro: eval_evals.intros)
next
  case RedStaticDownDynCast thus ?case
    by (fastforce elim: eval_cases intro: eval_evals.intros)
next
  case (DynCastRed E e s e'' s'' C s' e')
  have eval:"P,E  Cast C e'',s''  e',s'"
    and IH:"ex sx. P,E  e'',s''  ex,sx  P,E  e,s  ex,sx" by fact+
  moreover 
  { fix Cs Cs' a
    assume "P,E  e'',s''  ref (a, Cs @ C # Cs'),s'"
    from IH[OF this] have "P,E  e,s  ref (a, Cs@[C]@Cs'),s'" by simp
    hence "P,E  Cast C e,s  ref (a, Cs@[C]),s'" by(rule StaticDownDynCast) }
  ultimately show ?case by -(erule eval_cases,auto intro: eval_evals.intros)
next
  case RedDynCastNull thus ?case by (iprover elim:eval_cases intro:eval_evals.intros)
next
  case (RedDynCast s a D S C Cs' E Cs s' e')
  thus ?case by (cases s)(auto elim!:eval_cases intro:eval_evals.intros)
next
  case (RedDynCastFail s a D S C Cs E s'' e'')
  thus ?case by (cases s)(auto elim!: eval_cases intro: eval_evals.intros)
next
  case BinOpRed1 thus ?case by -(erule eval_cases,auto intro: eval_evals.intros)
next
  case BinOpRed2 
  thus ?case by (fastforce elim!:eval_cases intro:eval_evals.intros eval_finalId)
next
  case RedBinOp thus ?case by (iprover elim:eval_cases intro:eval_evals.intros)
next
  case (RedVar s V v E s' e')
  thus ?case by (cases s)(fastforce elim:eval_cases intro:eval_evals.intros)
next
  case LAssRed thus ?case by -(erule eval_cases,auto intro:eval_evals.intros)
next
  case RedLAss
  thus ?case by (fastforce elim:eval_cases intro:eval_evals.intros)
next
  case FAccRed thus ?case by -(erule eval_cases,auto intro:eval_evals.intros)
next
  case (RedFAcc s a D S Ds Cs' Cs fs F v E s' e')
  thus ?case by (cases s)(fastforce elim:eval_cases intro:eval_evals.intros)
next
  case RedFAccNull thus ?case by (fastforce elim!:eval_cases intro:eval_evals.intros)
next
  case (FAssRed1 E e1 s e1' s'' F Cs e2 s' e')
  have eval:"P,E  e1'F{Cs} := e2,s''  e',s'"
    and IH:"ex sx. P,E  e1',s''  ex,sx  P,E  e1,s  ex,sx" by fact+
  { fix Cs' D S T a fs h2 l2 s1 v v'
    assume ref:"P,E  e1',s''  ref (a, Cs'),s1" 
      and rest:"P,E  e2,s1  Val v,(h2, l2)" "h2 a = (D, S)" 
      "P  last Cs' has least F:T via Cs" "P  T casts v to v'"
      "(Cs' @p Cs, fs)  S"
    from IH[OF ref] have "P,E  e1,s  ref (a, Cs'),s1" .
    with rest have "P,E  e1F{Cs} := e2,s 
          Val v',(h2(a  (D,insert (Cs'@pCs,fs(F  v'))(S - {(Cs'@pCs,fs)}))),l2)"
      by-(rule FAss,simp_all) }
  moreover
  { fix s1 v 
    assume null:"P,E  e1',s''  null,s1" 
      and rest:"P,E  e2,s1  Val v,s'"
    from IH[OF null] have "P,E  e1,s  null,s1" .
    with rest have "P,E  e1F{Cs} := e2,s  THROW NullPointer,s'"
      by-(rule FAssNull,simp_all) }
  moreover
  { fix e' assume throw:"P,E  e1',s''  throw e',s'"
    from IH[OF throw] have "P,E  e1,s  throw e',s'" .
    hence "P,E  e1F{Cs} := e2,s  throw e',s'"
      by-(rule eval_evals.FAssThrow1,simp_all) }
  moreover
  { fix e' s1 v
    assume val:"P,E  e1',s''  Val v,s1"
      and rest:"P,E  e2,s1  throw e',s'"
    from IH[OF val] have "P,E  e1,s  Val v,s1" .
    with rest have "P,E  e1F{Cs} := e2,s  throw e',s'"
      by-(rule eval_evals.FAssThrow2,simp_all) }
  ultimately show ?case using eval
    by -(erule eval_cases,auto)
next
  case (FAssRed2 E e2 s e2' s'' v F Cs s' e')
  have eval:"P,E  Val vF{Cs} := e2',s''  e',s'"
    and IH:"ex sx. P,E  e2',s''  ex,sx  P,E  e2,s  ex,sx" by fact+
  { fix Cs' D S T a fs h2 l2 s1 v' v''
    assume val1:"P,E  Val v,s''  ref (a,Cs'),s1"
      and val2:"P,E  e2',s1  Val v',(h2, l2)"
      and rest:"h2 a = (D, S)" "P  last Cs' has least F:T via Cs"
               "P  T casts v' to v''" "(Cs'@pCs,fs)  S"
    from val1 have s'':"s1 = s''" by -(erule eval_cases)
    with val1 have "P,E  Val v,s  ref (a,Cs'),s"
      by(fastforce elim:eval_cases intro:eval_finalId)
    also from IH[OF val2[simplified s'']] have "P,E  e2,s  Val v',(h2, l2)" .
    ultimately have "P,E  Val vF{Cs} := e2,s 
           Val v'',(h2(a(D,insert(Cs'@pCs,fs(F  v''))(S - {(Cs'@pCs,fs)}))),l2)"
      using rest by -(rule FAss,simp_all) }
  moreover
  { fix s1 v'
    assume val1:"P,E  Val v,s''  null,s1"
      and val2:"P,E  e2',s1  Val v',s'"
    from val1 have s'':"s1 = s''" by -(erule eval_cases)
    with val1 have "P,E  Val v,s  null,s"
      by(fastforce elim:eval_cases intro:eval_finalId)
    also from IH[OF val2[simplified s'']] have "P,E  e2,s  Val v',s'" .
    ultimately have "P,E  Val vF{Cs} := e2,s  THROW NullPointer,s'"
      by -(rule FAssNull,simp_all) }
  moreover
  { fix r assume val:"P,E  Val v,s''  throw r,s'"
    hence s'':"s'' = s'" by -(erule eval_cases,simp)
    with val have "P,E  Val vF{Cs} := e2,s  throw r,s'" 
      by -(rule eval_evals.FAssThrow1,erule eval_cases,simp) }
  moreover
  { fix r s1 v'
    assume val1:"P,E  Val v,s''  Val v',s1"
      and val2:"P,E  e2',s1  throw r,s'"
    from val1 have s'':"s1 = s''" by -(erule eval_cases)
    with val1 have "P,E  Val v,s  Val v',s"
      by(fastforce elim:eval_cases intro:eval_finalId)
    also from IH[OF val2[simplified s'']] have "P,E  e2,s  throw r,s'" .
    ultimately have "P,E  Val vF{Cs} := e2,s  throw r,s'" 
      by -(rule eval_evals.FAssThrow2,simp_all) }
  ultimately show ?case using eval
    by -(erule eval_cases,auto)
next
  case (RedFAss h a D S Cs' F T Cs v v' Ds fs E l s' e')
  have val:"P,E  Val v',(h(a  (D,insert (Ds,fs(F  v'))(S - {(Ds,fs)}))),l)  
                  e',s'"
    and rest:"h a = (D, S)" "P  last Cs' has least F:T via Cs"
             "P  T casts v to v'" "Ds = Cs' @p Cs" "(Ds, fs)  S" by fact+
  from val have "s' = (h(a  (D,insert (Ds,fs(F  v')) (S - {(Ds,fs)}))),l)"
    and "e' = Val v'" by -(erule eval_cases,simp_all)+
  with rest show ?case apply simp
    by(rule FAss,simp_all)(rule eval_finalId,simp)+
next
  case RedFAssNull
  thus ?case by (fastforce elim!: eval_cases intro: eval_evals.intros)
next
  case (CallObj E e s e' s' Copt M es s'' e'')
  thus ?case
    apply -
    apply(cases Copt,simp)
    by(erule eval_cases,auto intro:eval_evals.intros)+
next
  case (CallParams E es s es' s'' v Copt M s' e')
  have call:"P,E  Call (Val v) Copt M es',s''  e',s'"
    and IH:"esx sx. P,E  es',s'' [⇒] esx,sx  P,E  es,s [⇒] esx,sx" by fact+
  show ?case
    proof(cases Copt)
    case None with call have eval:"P,E  Val vM(es'),s''  e',s'" by simp
    from eval show ?thesis
    proof(rule eval_cases)
      fix r assume "P,E  Val v,s''  throw r,s'" "e' = throw r"
      with None show "P,E  Call (Val v) Copt M es,s  e',s'"
        by(fastforce elim:eval_cases)
    next
      fix es'' r sx v' vs
      assume val:"P,E  Val v,s''  Val v',sx"
        and evals:"P,E  es',sx [⇒] map Val vs @ throw r # es'',s'"
        and e':"e' = throw r"
      have val':"P,E  Val v,s  Val v,s" by(rule Val)
      from val have eq:"v' = v  s'' = sx" by -(erule eval_cases,simp)
      with IH evals have "P,E  es,s [⇒] map Val vs @ throw r # es'',s'"
        by simp
      with eq CallParamsThrow[OF val'] e' None
      show "P,E  Call (Val v) Copt M es,s  e',s'"
        by fastforce
    next
      fix C Cs Cs' Ds S T T' Ts Ts' a body body' h2 h3 l2 l3 pns pns' s1 vs vs'
      assume val:"P,E  Val v,s''  ref(a,Cs),s1"
        and evals:"P,E  es',s1 [⇒] map Val vs,(h2,l2)"
        and hp:"h2 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 length:"length vs = length pns"
        and casts:"P  Ts Casts vs to vs'"
        and body:"P,E(this  Class (last Cs'), pns [↦] Ts)  
    case T' of Class D  Dbody | _  body,(h2,[this  Ref(a,Cs'),pns [↦] vs'])
         e',(h3, l3)"
        and s':"s' = (h3, l2)"
      from val have val':"P,E  Val v,s  ref(a,Cs),s"
        and eq:"s'' = s1  v = Ref(a,Cs)"
        by(auto elim:eval_cases intro:Val)
      from body obtain new_body 
        where body_case:"new_body = (case T' of Class D  Dbody | _  body)"
        and body':"P,E(this  Class (last Cs'), pns [↦] Ts)  
        new_body,(h2,[this  Ref(a,Cs'),pns [↦] vs'])  e',(h3, l3)"
        by simp
      from eq IH evals have "P,E  es,s [⇒] map Val vs,(h2,l2)" by simp
      with eq Call[OF val' _ _ "method" select length casts _ body_case] 
           hp body' s' None
      show "P,E  Call (Val v) Copt M es,s  e',s'" by fastforce
    next
      fix s1 vs
      assume val:"P,E  Val v,s''  null,s1"
        and evals:"P,E  es',s1 [⇒] map Val vs,s'"
        and e':"e' = THROW NullPointer"
      from val have val':"P,E  Val v,s  null,s"
        and eq:"s'' = s1  v = Null"
        by(auto elim:eval_cases intro:Val)
      from eq IH evals have "P,E  es,s [⇒] map Val vs,s'" by simp
      with eq CallNull[OF val'] e' None
      show "P,E  Call (Val v) Copt M es,s  e',s'" by fastforce
    qed
  next
    case (Some C) with call have eval:"P,E  Val v∙(C::)M(es'),s''  e',s'"
      by simp
    from eval show ?thesis
    proof(rule eval_cases)
      fix r assume "P,E  Val v,s''  throw r,s'" "e' = throw r"
      with Some show "P,E  Call (Val v) Copt M es,s  e',s'"
        by(fastforce elim:eval_cases)
    next
      fix es'' r sx v' vs
      assume val:"P,E  Val v,s''  Val v',sx"
        and evals:"P,E  es',sx [⇒] map Val vs @ throw r # es'',s'"
        and e':"e' = throw r"
      have val':"P,E  Val v,s  Val v,s" by(rule Val)
      from val have eq:"v' = v  s'' = sx" by -(erule eval_cases,simp)
      with IH evals have "P,E  es,s [⇒] map Val vs @ throw r # es'',s'"
        by simp
      with eq CallParamsThrow[OF val'] e' Some
      show "P,E  Call (Val v) Copt M es,s  e',s'"
        by fastforce
    next
      fix Cs Cs' Cs'' T Ts a body h2 h3 l2 l3 pns s1 vs vs'
      assume val:"P,E  Val v,s''  ref (a,Cs),s1"
        and evals:"P,E  es',s1 [⇒] map Val vs,(h2,l2)"
        and path_unique:"P  Path last Cs to C unique"
        and path_via:"P  Path last Cs to C via Cs''"
        and least:"P  C has least M = (Ts, T, pns, body) via Cs'"
        and length:"length vs = length pns"
        and casts:"P  Ts Casts vs to vs'"
        and body:"P,E(this  Class (last ((Cs @p Cs'') @p Cs')), pns [↦] Ts)  
           body,(h2,[this  Ref(a,(Cs@pCs'')@pCs'),pns [↦] vs'])  e',(h3,l3)"
        and s':"s' = (h3,l2)"
      from val have val':"P,E  Val v,s  ref(a,Cs),s"
        and eq:"s'' = s1  v = Ref(a,Cs)"
        by(auto elim:eval_cases intro:Val)
      from eq IH evals have "P,E  es,s [⇒] map Val vs,(h2,l2)" by simp
      with eq StaticCall[OF val' _ path_unique path_via least _ _ casts _ body] 
           length s' Some
      show "P,E  Call (Val v) Copt M es,s  e',s'" by fastforce
    next
      fix s1 vs
      assume val:"P,E  Val v,s''  null,s1"
        and evals:"P,E  es',s1 [⇒] map Val vs,s'"
        and e':"e' = THROW NullPointer"
      from val have val':"P,E  Val v,s  null,s"
        and eq:"s'' = s1  v = Null"
        by(auto elim:eval_cases intro:Val)
      from eq IH evals have "P,E  es,s [⇒] map Val vs,s'" by simp
      with eq CallNull[OF val'] e' Some
      show "P,E  Call (Val v) Copt M es,s  e',s'"
        by fastforce
    qed
  qed
next
  case (RedCall s a C S Cs M Ts' T' pns' body' Ds Ts T pns body Cs' vs
                bs new_body E s' e')
  obtain h l where "s' = (h,l)" by(cases s') auto
  have "P,E  ref(a,Cs),s  ref(a,Cs),s" by (rule eval_evals.intros)
  moreover
  have finals: "finals(map Val vs)" by simp
  obtain h2 l2 where s: "s = (h2,l2)" by (cases s)
  with finals have "P,E  map Val vs,s [⇒] map Val vs,(h2,l2)"
    by (iprover intro: eval_finalsId)
  moreover from s have h2a:"h2 a = Some (C,S)" using RedCall by simp
  moreover have "method": "P  last Cs has least M = (Ts',T',pns',body') via Ds" by fact
  moreover have select:"P  (C,Cs@pDs) selects M = (Ts,T,pns,body) via Cs'" by fact
  moreover have blocks:"bs = blocks(this#pns,Class(last Cs')#Ts,Ref(a,Cs')#vs,body)" by fact
  moreover have body_case:"new_body = (case T' of Class D  Dbs | _  bs)" by fact
  moreover have same_len1: "length Ts = length pns"
   and this_distinct: "this  set pns" and fv: "fv body  {this}  set pns"
    using select wf by (fastforce dest!:select_method_wf_mdecl simp:wf_mdecl_def)+
  have same_len: "length vs = length pns" by fact
  moreover
  obtain h3 l3 where s': "s' = (h3,l3)" by (cases s')
  have eval_blocks:"P,E  new_body,s  e',s'" by fact
  hence id: "l3 = l2" using fv s s' same_len1 same_len wf blocks body_case
    by(cases T')(auto elim!: eval_closed_lcl_unchanged)
  from same_len1 have same_len':"length(this#pns) = length(Class (last Cs')#Ts)" 
    by simp
  from same_len1 same_len
  have same_len2:"length(this#pns) = length(Ref(a,Cs')#vs)" by simp
  from eval_blocks
  have eval_blocks':"P,E  new_body,(h2,l2)  e',(h3,l3)" using s s' by simp
  have casts_unique:"vs'. P  Class (last Cs')#Ts Casts Ref(a,Cs')#vs to vs'
                             vs' = Ref(a,Cs')#tl vs'"
    using wf
    by -(erule Casts_to.cases,auto elim!:casts_to.cases dest!:mdc_eq_last
                                      simp:path_via_def appendPath_def)
  have "l'' vs' new_body'. P,E(thisClass(last Cs'), pns[↦]Ts)  
              new_body',(h2,l2(this # pns[↦]Ref(a,Cs')#vs'))  e',(h3, l'')  
     P  Class(last Cs')#Ts Casts Ref(a,Cs')#vs to Ref(a,Cs')#vs' 
     length vs' = length vs  fv new_body'  {this}  set pns 
     new_body' = (case T' of Class D  Dbody  | _   body)"
  proof(cases "C. T'  Class C")
    case True
    with same_len' same_len2 eval_blocks' casts_unique body_case blocks
    obtain l'' vs'
      where body:"P,E(thisClass(last Cs'), pns[↦]Ts)  
                    body,(h2,l2(this # pns[↦]Ref(a,Cs')#vs'))  e',(h3, l'')"
      and casts:"P  Class(last Cs')#Ts Casts Ref(a,Cs')#vs to Ref(a,Cs')#vs'"
      and lengthvs':"length vs' = length vs"
      by -(drule_tac vs="Ref(a,Cs')#vs" in blocksEval,assumption,cases T',
           auto simp:length_Suc_conv,blast)
    with fv True show ?thesis by(cases T') auto
  next
    case False
    then obtain D where T':"T' = Class D" by auto
    with same_len' same_len2 eval_blocks' casts_unique body_case blocks
    obtain l'' vs'
      where body:"P,E(thisClass(last Cs'), pns[↦]Ts)  
                    Dbody,(h2,l2(this # pns[↦]Ref(a,Cs')#vs'))  
                    e',(h3, l'')"
      and casts:"P  Class(last Cs')#Ts Casts Ref(a,Cs')#vs to Ref(a,Cs')#vs'"
      and lengthvs':"length vs' = length vs"
      by - (drule_tac vs="Ref(a,Cs')#vs" in CastblocksEval,
            assumption,simp,clarsimp simp:length_Suc_conv,auto)
    from fv have "fv (Dbody)  {this}  set pns"
      by simp
    with body casts lengthvs' T' show ?thesis by auto
  qed
  then obtain l'' vs' new_body'
    where body:"P,E(thisClass(last Cs'), pns[↦]Ts)  
               new_body',(h2,l2(this # pns[↦]Ref(a,Cs')#vs'))  e',(h3, l'')"
    and casts:"P  Class(last Cs')#Ts Casts Ref(a,Cs')#vs to Ref(a,Cs')#vs'"
    and lengthvs':"length vs' = length vs"
    and body_case':"new_body' = (case T' of Class D  Dbody  | _  body)"
    and fv':"fv new_body'  {this}  set pns"
    by auto
  from same_len2 lengthvs'
  have same_len3:"length (this # pns) = length (Ref (a, Cs') # vs')" by simp
  from restrict_map_upds[OF same_len3,of "set(this#pns)" "l2"]
  have "l2(this # pns[↦]Ref(a,Cs')#vs')|`(set(this#pns)) = 
          [this # pns[↦]Ref(a,Cs')#vs']" by simp
  with eval_restrict_lcl[OF wf body fv'] this_distinct same_len1 same_len
  have "P,E(thisClass(last Cs'), pns[↦]Ts)  
   new_body',(h2,[this # pns[↦]Ref(a,Cs')#vs'])  e',(h3, l''|`(set(this#pns)))"
    by simp
  with casts obtain l2' l3' vs' where
        "P  Ts Casts vs to vs'"
    and "P,E(thisClass(last Cs'), pns[↦]Ts)  
                                      new_body',(h2,l2')  e',(h3,l3')"
    and "l2' = [thisRef(a,Cs'),pns[↦]vs']"
    by(auto elim:Casts_to.cases)
  ultimately have "P,E  (ref(a,Cs))M(map Val vs),s  e',(h3,l2)"
    using body_case'
    by -(rule Call,simp_all)
  with s' id show ?case by simp
next
  case (RedStaticCall Cs C Cs'' M Ts T pns body Cs' Ds vs E a s s' e')
  have "P,E  ref(a,Cs),s  ref(a,Cs),s" by (rule eval_evals.intros)
  moreover
  have finals: "finals(map Val vs)" by simp
  obtain h2 l2 where s: "s = (h2,l2)" by (cases s)
  with finals have "P,E  map Val vs,s [⇒] map Val vs,(h2,l2)"
    by (iprover intro: eval_finalsId)
  moreover have path_unique:"P  Path last Cs to C unique" by fact
  moreover have path_via:"P  Path last Cs to C via Cs''" by fact
  moreover have least:"P  C has least M = (Ts, T, pns, body) via Cs'" by fact
  moreover have same_len1: "length Ts = length pns"
   and this_distinct: "this  set pns" and fv: "fv body  {this}  set pns"
    using least wf by (fastforce dest!:has_least_wf_mdecl simp:wf_mdecl_def)+
  moreover have same_len:"length vs = length pns" by fact
  moreover have Ds:"Ds = (Cs @p Cs'') @p Cs'" by fact
  moreover
  obtain h3 l3 where s': "s' = (h3,l3)" by (cases s')
  have eval_blocks:"P,E  blocks(this#pns,Class(last Ds)#Ts,Ref(a,Ds)#vs,body),s
                        e',s'" by fact
  hence id: "l3 = l2" using fv s s' same_len1 same_len wf
    by(auto elim!: eval_closed_lcl_unchanged)
  from same_len1 have same_len':"length(this#pns) = length(Class (last Ds)#Ts)"
    by simp
  from same_len1 same_len
  have same_len2:"length(this#pns) = length(Ref(a,Ds)#vs)" by simp
  from eval_blocks
  have eval_blocks':"P,E  blocks(this#pns,Class(last Ds)#Ts,Ref(a,Ds)#vs,body),
                               (h2,l2)  e',(h3,l3)" using s s' by simp
  have casts_unique:"vs'. P  Class (last Ds)#Ts Casts Ref(a,Ds)#vs to vs'
                             vs' = Ref(a,Ds)#tl vs'"
    using wf
    by -(erule Casts_to.cases,auto elim!:casts_to.cases dest!:mdc_eq_last
                                      simp:path_via_def appendPath_def)
  from same_len' same_len2 eval_blocks' casts_unique
  obtain l'' vs' where body:"P,E(thisClass(last Ds), pns[↦]Ts)  
               body,(h2,l2(this # pns[↦]Ref(a,Ds)#vs'))  e',(h3, l'')"
    and casts:"P  Class(last Ds)#Ts Casts Ref(a,Ds)#vs to Ref(a,Ds)#vs'"
    and lengthvs':"length vs' = length vs"
    by -(drule_tac vs="Ref(a,Ds)#vs" in blocksEval,auto simp:length_Suc_conv,blast)
  from same_len2 lengthvs'
  have same_len3:"length (this # pns) = length (Ref(a,Ds) # vs')" by simp
  from restrict_map_upds[OF same_len3,of "set(this#pns)" "l2"]
  have "l2(this # pns[↦]Ref(a,Ds)#vs')|`(set(this#pns)) = 
          [this # pns[↦]Ref(a,Ds)#vs']" by simp
  with eval_restrict_lcl[OF wf body fv] this_distinct same_len1 same_len
  have "P,E(thisClass(last Ds), pns[↦]Ts)  
   body,(h2,[this#pns [↦] Ref(a,Ds)#vs'])  e',(h3, l''|`(set(this#pns)))"
    by simp
  with casts obtain l2' l3' vs' where
        "P  Ts Casts vs to vs'"
    and "P,E(this  Class(last Ds),pns [↦] Ts)  body,(h2,l2')  e',(h3,l3')"
    and "l2' = [this  Ref(a,Ds),pns [↦] vs']"
    by(auto elim:Casts_to.cases)
  ultimately have "P,E  (ref(a,Cs))∙(C::)M(map Val vs),s  e',(h3,l2)"
    by -(rule StaticCall,simp_all)
  with s' id show ?case by simp
next
  case RedCallNull
  thus ?case
    by (fastforce elim: eval_cases intro: eval_evals.intros eval_finalsId)
next
  case BlockRedNone
  thus ?case
    by (fastforce elim!: eval_cases intro: eval_evals.intros 
                 simp add: fun_upd_same fun_upd_idem)
next
  case (BlockRedSome E V T e h l e'' h' l' v s' e')
  have eval:"P,E  {V:T:=Val v; e''},(h', l'(V := l V))  e',s'"
    and red:"P,E(V  T)  e,(h, l(V := None))  e'',(h', l')"
    and notassigned:"¬ assigned V e" and l':"l' V = Some v"
    and IH:"ex sx. P,E(V  T)  e'',(h', l')  ex,sx 
                     P,E(V  T)  e,(h, l(V := None))  ex,sx" by fact+
  from l' have l'upd:"l'(V  v) = l'" by (rule map_upd_triv)
  from wf red l' have casts:"P  T casts v to v"
    apply -
    apply(erule_tac V="V" in None_lcl_casts_values)
    by(simp add:fun_upd_same)+
  from eval obtain h'' l''
  where "P,E(V  T)  V:=Val v;; e'',(h',l'(V:=None))  e',(h'',l'')  
    s' = (h'',l''(V:=l V))"
    by (fastforce elim:eval_cases simp:fun_upd_same fun_upd_idem)
  moreover
  { fix T' h0 l0 v' v''
    assume eval':"P,E(V  T)  e'',(h0,l0(V  v''))  e',(h'', l'')"
      and val:"P,E(V  T)  Val v,(h', l'(V := None))  Val v',(h0,l0)"
      and env:"(E(V  T)) V = Some T'" and casts':"P  T' casts v' to v''"
    from env have TeqT':"T = T'" by (simp add:fun_upd_same)
    from val have eq:"v = v'  h' = h0  l'(V := None) = l0"
      by -(erule eval_cases,simp)
    with casts casts' wf TeqT' have "v = v''"
      by clarsimp(rule casts_casts_eq)
    with eq eval'
    have "P,E(V  T)  e'',(h', l'(V  v))  e',(h'', l'')"
      by clarsimp }
  ultimately have "P,E(V  T)  e'',(h',l'(V  v))  e',(h'',l'')" 
    and s':"s' = (h'',l''(V:=l V))"
    apply auto
    apply(erule eval_cases)
     apply(erule eval_cases) apply auto
    apply(erule eval_cases) apply auto
    apply(erule eval_cases) apply auto
    done
  with l'upd have eval'':"P,E(V  T)  e'',(h',l')  e',(h'',l'')"
    by simp
  from IH[OF eval''] have "P,E(V  T)  e,(h, l(V := None))  e',(h'', l'')" .
  with s' show ?case by(fastforce intro:Block)
next
  case (InitBlockRed E V T e h l v' e'' h' l' v'' v s' e')
  have eval:" P,E  {V:T:=Val v''; e''},(h', l'(V := l V))  e',s'"
    and red:"P,E(V  T)  e,(h, l(V  v'))  e'',(h', l')"
    and casts:"P  T casts v to v'" and l':"l' V = Some v''"
    and IH:"ex sx. P,E(V  T)  e'',(h', l')  ex,sx 
                     P,E(V  T)  e,(h, l(V  v'))  ex,sx" by fact+
  from l' have l'upd:"l'(V  v'') = l'" by (rule map_upd_triv)
  from wf casts have "P  T casts v' to v'" by(rule casts_casts)
  with wf red l' have casts':"P  T casts v'' to v''"
    apply -
    apply(erule_tac V="V" in Some_lcl_casts_values)
    by(simp add:fun_upd_same)+
  from eval obtain h'' l''
  where "P,E(V  T)  V:=Val v'';; e'',(h',l'(V:=None))  e',(h'',l'')  
    s' = (h'',l''(V:=l V))"
    by (fastforce elim:eval_cases simp:fun_upd_same fun_upd_idem)
  moreover
  { fix T' v'''
    assume eval':"P,E(V  T)  e'',(h',l'(V  v'''))  e',(h'', l'')"
      and env:"(E(V  T)) V = Some T'" and casts'':"P  T' casts v'' to v'''"
    from env have "T = T'" by (simp add:fun_upd_same)
    with casts' casts'' wf have "v'' = v'''" by simp(rule casts_casts_eq)
    with eval' have "P,E(V  T)  e'',(h', l'(V  v''))  e',(h'', l'')" by simp }
  ultimately have "P,E(V  T)  e'',(h',l'(V  v''))  e',(h'',l'')"
    and s':"s' = (h'',l''(V:=l V))"
    by(auto elim!:eval_cases)
 with l'upd have eval'':"P,E(V  T)  e'',(h',l')  e',(h'',l'')"
    by simp
  from IH[OF eval'']
  have evale:"P,E(V  T)  e,(h, l(V  v'))  e',(h'', l'')" .
  from casts
  have "P,E(V  T)  V:=Val v,(h,l(V:=None))  Val v',(h,l(V  v'))"
    by -(rule_tac l="l(V:=None)" in LAss,
         auto intro:eval_evals.intros simp:fun_upd_same)
  with evale s' show ?case by(fastforce intro:Block Seq)
next
  case (RedBlock E V T v s s' e')
  have "P,E  Val v,s  e',s'" by fact
  then obtain s': "s'=s" and e': "e'=Val v"
    by cases simp
  obtain h l where s: "s=(h,l)" by (cases s)
  have "P,E(V  T)  Val v,(h,l(V:=None))  Val v,(h,l(V:=None))" 
    by (rule eval_evals.intros)
  hence "P,E  {V:T;Val v},(h,l)  Val v,(h,(l(V:=None))(V:=l V))"
    by (rule eval_evals.Block)
  thus "P,E  {V:T; Val v},s  e',s'"
    using s s' e'
    by simp
next
  case (RedInitBlock T v v' E V u s s' e')
  have "P,E  Val u,s  e',s'" and casts:"P  T casts v to v'" by fact+
  then obtain s': "s' = s" and e': "e'=Val u" by cases simp
  obtain h l where s: "s=(h,l)" by (cases s)
  have val:"P,E(V  T)  Val v,(h,l(V:=None))  Val v,(h,l(V:=None))"
    by (rule eval_evals.intros)
  with casts
  have "P,E(V  T)  V:=Val v,(h,l(V:=None))  Val v',(h,l(V  v'))"
    by -(rule_tac l="l(V:=None)" in LAss,auto simp:fun_upd_same)
  hence "P,E  {V:T :=Val v; Val u},(h,l)  Val u,(h, (l(Vv'))(V:=l V))"
    by (fastforce intro!: eval_evals.intros)
  thus ?case using s s' e' by simp
next
  case SeqRed thus ?case by (fastforce elim: eval_cases intro: eval_evals.intros)
next
  case RedSeq thus ?case by (fastforce elim: eval_cases intro: eval_evals.intros)
next
  case CondRed thus ?case by (fastforce elim: eval_cases intro: eval_evals.intros)
next
  case RedCondT thus ?case by (fastforce elim: eval_cases intro: eval_evals.intros)
next
  case RedCondF thus ?case by (fastforce elim: eval_cases intro: eval_evals.intros)
next
  case RedWhile
  thus ?case by (auto simp add: unfold_while intro:eval_evals.intros elim:eval_cases)
next
  case ThrowRed thus ?case by (fastforce elim: eval_cases intro: eval_evals.intros)
next
  case RedThrowNull
  thus ?case by -(auto elim!:eval_cases intro!:eval_evals.ThrowNull eval_finalId)
next
  case ListRed1 thus ?case by (fastforce elim: evals_cases intro: eval_evals.intros)
next
  case ListRed2
  thus ?case by (fastforce elim!: evals_cases eval_cases 
                          intro: eval_evals.intros eval_finalId)
next
  case StaticCastThrow
  thus