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 ⊢ ⟨⦇C⦈e,s⟩ →* ⟨⦇C⦈e',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 ⊢ ⟨⦇C⦈e,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 ⊢ ⟨⦇C⦈e,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 ⊢ ⟨⦇C⦈e,s⟩ →* ⟨ref(a,Cs@[C]),s'⟩"

apply(rule rtrancl_into_rtrancl)
 apply(erule StaticCastReds)
apply simp
apply(subgoal_tac "P,E ⊢ ⟨⦇C⦈ref(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 ⊢ ⟨⦇C⦈e,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 ⊢ ⟨⦇C⦈e,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'(V↦v'))⟩"

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 ⊢ ⟨e∙F{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 ⊢ ⟨e∙F{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 ⊢ ⟨e∙F{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 ⊢ ⟨e∙F{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 ⊢ ⟨e∙F{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 v∙F{Cs}:=e, s⟩ →* ⟨Val v∙F{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 ⊢ ⟨e1∙F{Cs}:=e2, s0⟩ →* 
        ⟨Val v',(h2(a↦(D,insert (Ds,fs(F↦v')) (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 ⊢ ⟨e1∙F{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 ⊢ ⟨e∙F{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 ⊢ ⟨e1∙F{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(V↦v')) ⟶ 
                   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(V↦v'))⟩ →* ⟨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(V↦v'))⟩ →* ⟨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(a↦b)) 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 ⊢ ⟨⦇C⦈ref (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' ⊢ ⟨⦇C⦈ref (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 ⊢ ⟨⦇C⦈e,s⟩ →* ⟨e',s'⟩ ⟹ final e' ∨ (∃e''. e' = ⦇C⦈e'')"
by(induct rule:rtrancl_induct2,auto elim:red.cases simp:final_def)

lemma Cast_red:"P,E ⊢ ⟨e,s⟩ →* ⟨e',s'⟩ ⟹ 
  (⋀e1. ⟦e = ⦇C⦈e0; e' = ⦇C⦈e1⟧ ⟹ 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 = ⦇C⦈e0" and cast':"e' = ⦇C⦈e1"
    and IH:"⋀e1. ⟦e = ⦇C⦈e0; e'' = ⦇C⦈e1⟧ ⟹ 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'' = ⦇C⦈ex)"
    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'' = ⦇C⦈ex"
    then obtain ex where e'':"e'' = ⦇C⦈ex" 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 ⊢ ⟨⦇C⦈e,s⟩ →* ⟨e',s'⟩; final e'⟧ ⟹
∃e'' s''. P,E ⊢ ⟨e,s⟩ →* ⟨e'',s''⟩ ∧ P,E ⊢ ⟨⦇C⦈e'',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 ⊢ ⟨⦇C⦈e,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 ⊢ ⟨⦇C⦈ex,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'' = ⦇C⦈ex)" 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'' = ⦇C⦈ex"
    then obtain ex where e'':"e'' = ⦇C⦈ex" 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 ⊢ ⟨⦇C⦈e,(h,l)⟩ → ⟨e',(h,l)⟩"
  and final:"final e" and final':"final e'"
  shows "P,E' ⊢ ⟨⦇C⦈e,(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 ⇒ ⦇D⦈body  | _ ⇒ 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 ⊢ ⟨e∙M(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 ⊢ ⟨e∙M(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) ⊢ ⟨⦇D⦈e',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)⟩ → 
                 ⟨⦇D⦈blocks(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)⟩ →* 
                  ⟨⦇D⦈blocks(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)⟩
             →* ⟨⦇D⦈e',(h3,override_on (l2++l3) l2 ({this} ∪ set pns))⟩"
      by(rule StaticCastReds)
    moreover
    have "P,E ⊢ ⟨⦇D⦈e',(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="(⦇D⦈e',(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(this↦Class(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 ∧ 
            (∀T∈set 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(this↦Class(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 ⇒ ⦇D⦈body | _ ⇒ 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 ⊢ ⟨e∙M(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,s1⟩⇒⟨e',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(p↦v'))⟩ ⇒ ⟨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(p↦v', 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 (⦇C⦈e) ⊆ 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 (e1∙F{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 ⇒ ⦇D⦈body | _ ⇒ body)" by fact+
  have "fv (e∙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 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 |> Simplifier.del_loop "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 ⊢ ⟨e1∙F{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 ⊢ ⟨e1∙F{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 ⊢ ⟨e1∙F{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 ⊢ ⟨e1∙F{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 v∙F{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 v∙F{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 v∙F{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 v∙F{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 v∙F{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 v∙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 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 ⇒ ⦇D⦈body | _ ⇒ 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 ⇒ ⦇D⦈body | _ ⇒ 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 ⇒ ⦇D⦈bs | _ ⇒ 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(this↦Class(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 ⇒ ⦇D⦈body  | _  ⇒ 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(this↦Class(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(this↦Class(last Cs'), pns[↦]Ts) ⊢ 
                    ⟨⦇D⦈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 CastblocksEval,
            assumption,simp,clarsimp simp:length_Suc_conv,auto)
    from fv have "fv (⦇D⦈body) ⊆ {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(this↦Class(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 ⇒ ⦇D⦈body  | _ ⇒ 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(this↦Class(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(this↦Class(last Cs'), pns[↦]Ts) ⊢ 
                                      ⟨new_body',(h2,l2')⟩ ⇒ ⟨e',(h3,l3')⟩"
    and "l2' = [this↦Ref(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(this↦Class(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(this↦Class(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(V↦v'))(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 ?case by (fastforce elim: eval_cases intro: eval_evals.intros)
next
  case DynCastThrow
  thus ?case by (fastforce elim: eval_cases intro: eval_evals.intros)
next
  case BinOpThrow1 thus ?case by (fastforce elim: eval_cases intro: eval_evals.intros)
next
  case BinOpThrow2 thus ?case by (fastforce elim: eval_cases intro: eval_evals.intros)
next
  case LAssThrow thus ?case by (fastforce elim: eval_cases intro: eval_evals.intros)
next
  case FAccThrow thus ?case by (fastforce elim: eval_cases intro: eval_evals.intros)
next
  case FAssThrow1 thus ?case by (fastforce elim: eval_cases intro: eval_evals.intros)
next
  case FAssThrow2 thus ?case by (fastforce elim: eval_cases intro: eval_evals.intros)
next
  case CallThrowObj thus ?case by (fastforce elim: eval_cases intro: eval_evals.intros)
next
  case (CallThrowParams es vs r es' E v Copt M s s' e')
  have "P,E ⊢ ⟨Val v,s⟩ ⇒ ⟨Val v,s⟩" by (rule eval_evals.intros)
  moreover
  have es: "es = map Val vs @ Throw r # es'" by fact
  have eval_e: "P,E ⊢ ⟨Throw r,s⟩ ⇒ ⟨e',s'⟩" by fact
  then obtain s': "s' = s" and e': "e' = Throw r"
    by cases (auto elim!:eval_cases)
  with list_eval_Throw [OF eval_e] es
  have "P,E ⊢ ⟨es,s⟩ [⇒] ⟨map Val vs @ Throw r # es',s'⟩" by simp
  ultimately have "P,E ⊢ ⟨Call (Val v) Copt M es,s⟩ ⇒ ⟨Throw r,s'⟩"
    by (rule eval_evals.CallParamsThrow)
  thus ?case using e' by simp
next
  case (BlockThrow E V T r s s' e')
  have "P,E ⊢ ⟨Throw r, s⟩ ⇒ ⟨e',s'⟩" by fact
  then obtain s': "s' = s" and e': "e' = Throw r"
    by cases (auto elim!:eval_cases)
  obtain h l where s: "s=(h,l)" by (cases s)
  have "P,E(V ↦ T) ⊢ ⟨Throw r, (h,l(V:=None))⟩ ⇒ ⟨Throw r, (h,l(V:=None))⟩"
    by (simp add:eval_evals.intros eval_finalId)
  hence "P,E ⊢ ⟨{V:T;Throw r},(h,l)⟩ ⇒ ⟨Throw r, (h,(l(V:=None))(V:=l V))⟩"
    by (rule eval_evals.Block)
  thus "P,E ⊢ ⟨{V:T; Throw r},s⟩ ⇒ ⟨e',s'⟩" using s s' e' by simp
next
  case (InitBlockThrow T v v' E V r s s' e')
  have "P,E ⊢ ⟨Throw r,s⟩ ⇒ ⟨e',s'⟩" and casts:"P ⊢ T casts v to v'" by fact+
  then obtain s': "s' = s" and e': "e' = Throw r"
    by cases (auto elim!:eval_cases)
  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)
  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; Throw r},(h,l)⟩ ⇒ ⟨Throw r, (h, (l(V↦v'))(V:=l V))⟩"
    by(fastforce intro:eval_evals.intros)
  thus "P,E ⊢ ⟨{V:T := Val v; Throw r},s⟩ ⇒ ⟨e',s'⟩" using s s' e' by simp
next
  case SeqThrow thus ?case by (fastforce elim: eval_cases intro: eval_evals.intros)
next
  case CondThrow thus ?case by (fastforce elim: eval_cases intro: eval_evals.intros)
next
  case ThrowThrow thus ?case by (fastforce elim: eval_cases intro: eval_evals.intros)
qed


(* ... und wieder anschalten: *)
declare split_paired_All [simp] split_paired_Ex [simp]
setup ‹map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac))›
setup ‹map_theory_simpset (fn ctxt => ctxt |> Simplifier.add_loop ("split_all_tac", split_all_tac))›


text ‹Its extension to ‹→*›:› 

lemma extend_eval:
assumes wf: "wwf_prog P"
and reds: "P,E ⊢ ⟨e,s⟩ →* ⟨e'',s''⟩" and eval_rest:  "P,E ⊢ ⟨e'',s''⟩ ⇒ ⟨e',s'⟩"
shows "P,E ⊢ ⟨e,s⟩ ⇒ ⟨e',s'⟩"

using reds eval_rest 
apply (induct rule: converse_rtrancl_induct2)
apply simp
apply simp
apply (rule extend_1_eval)
apply (rule wf)
apply assumption+
done



lemma extend_evals:
assumes wf: "wwf_prog P"
and reds: "P,E ⊢ ⟨es,s⟩ [→]* ⟨es'',s''⟩" and eval_rest:  "P,E ⊢ ⟨es'',s''⟩ [⇒] ⟨es',s'⟩"
shows "P,E ⊢ ⟨es,s⟩ [⇒] ⟨es',s'⟩"

using reds eval_rest 
apply (induct rule: converse_rtrancl_induct2)
apply simp
apply simp
apply (rule extend_1_evals)
apply (rule wf)
apply assumption+
done


text ‹Finally, small step semantics can be simulated by big step semantics:
›

theorem
assumes wf: "wwf_prog P"
shows small_by_big: "⟦P,E ⊢ ⟨e,s⟩ →* ⟨e',s'⟩; final e'⟧ ⟹ P,E ⊢ ⟨e,s⟩ ⇒ ⟨e',s'⟩"
and "⟦P,E ⊢ ⟨es,s⟩ [→]* ⟨es',s'⟩; finals es'⟧ ⟹ P,E ⊢ ⟨es,s⟩ [⇒] ⟨es',s'⟩"

proof -
  note wf 
  moreover assume "P,E ⊢ ⟨e,s⟩ →* ⟨e',s'⟩"
  moreover assume "final e'"
  then have "P,E ⊢ ⟨e',s'⟩ ⇒ ⟨e',s'⟩"
    by (rule eval_finalId)
  ultimately show "P,E ⊢ ⟨e,s⟩⇒⟨e',s'⟩"
    by (rule extend_eval)
next
  note wf 
  moreover assume "P,E ⊢ ⟨es,s⟩ [→]* ⟨es',s'⟩"
  moreover assume "finals es'"
  then have "P,E ⊢ ⟨es',s'⟩ [⇒] ⟨es',s'⟩"
    by (rule eval_finalsId)
  ultimately show "P,E ⊢ ⟨es,s⟩ [⇒] ⟨es',s'⟩"
    by (rule extend_evals)
qed


subsection ‹Equivalence›

text‹And now, the crowning achievement:›

corollary big_iff_small:
  "wwf_prog P ⟹
  P,E ⊢ ⟨e,s⟩ ⇒ ⟨e',s'⟩  =  (P,E ⊢ ⟨e,s⟩ →* ⟨e',s'⟩ ∧ final e')"
by(blast dest: big_by_small eval_final small_by_big)


end