Theory Equivalence

(*  Title:       CoreC++
    ID:          $Id: Equivalence.thy,v 1.20 2009-03-20 17:56:16 makarius Exp $
    Author:      Daniel Wasserrab
    Maintainer:  Daniel Wasserrab <wasserra at fmi.uni-passau.de>

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


header {* \isaheader{Equivalence of Big Step and Small Step Semantics} *}

theory Equivalence imports BigStep SmallStep WWellForm begin


section{* Some casts-lemmas *}

lemma assumes wf:"wf_prog wf_md P"
shows casts_casts:
"P \<turnstile> T casts v to v' ==> P \<turnstile> 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 \<turnstile> 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 \<turnstile> Path last Ds to C via [C]"
    by(fastsimp intro:Subobjs_Base simp:path_via_def)
  with Ds' show ?case by(fastsimp intro:casts_to.casts_ref)
qed



lemma casts_casts_eq:
"[| P \<turnstile> T casts v to v; P \<turnstile> 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 \<turnstile> ⟨e,(h,l)⟩ -> ⟨e',(h',l')⟩ ==>
  (!!V. [|l V = None; E V = Some T; l' V = Some v'|]
  ==> P \<turnstile> T casts v' to v')"
and "P,E \<turnstile> ⟨es,(h,l)⟩ [->] ⟨es',(h',l')⟩ ==>
  (!!V. [|l V = None; E V = Some T; l' V = Some v'|]
  ==> P \<turnstile> 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 \<mapsto> w')) V' = Some v'"
    and casts:"P \<turnstile> 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(fastsimp intro:casts_casts)
  next
    case False
    with lupd have "l V' = Some v'" by(fastsimp split:split_if_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 \<mapsto> T')) V' = Some T; 
                   l' V' = Some v'|]
            ==> P \<turnstile> T casts v' to v'" by fact+
  show ?case
  proof(cases "V = V'")
    case True 
    with l'upd l show ?thesis by fastsimp
  next
    case False
    with l  l'upd have lnew:"(l(V := None)) V' = None"
      and l'new:"l' V' = Some v'" by (auto split:split_if_asm)
    from env False have env':"(E(V \<mapsto> T')) V' = Some T" by fastsimp
    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 \<mapsto> T')) V' = Some T; 
                   l' V' = Some v'|]
            ==> P \<turnstile> T casts v' to v'" by fact+
  show ?case
  proof(cases "V = V'")
    case True
    with l l'upd show ?thesis by fastsimp
  next
    case False
    with l  l'upd have lnew:"(l(V := None)) V' = None"
      and l'new:"l' V' = Some v'" by (auto split:split_if_asm)
    from env False have env':"(E(V \<mapsto> T')) V' = Some T" by fastsimp
    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 \<mapsto> w')) V' = None; (E(V \<mapsto> T')) V' = Some T; 
                   l' V' = Some v'|]
            ==> P \<turnstile> T casts v' to v'" by fact+
  show ?case
  proof(cases "V = V'")
    case True
    with l l'upd show ?thesis by fastsimp
  next
    case False
    with l  l'upd have lnew:"(l(V \<mapsto> w')) V' = None"
      and l'new:"l' V' = Some v'" by (auto split:split_if_asm)
    from env False have env':"(E(V \<mapsto> T')) V' = Some T" by fastsimp
    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 \<turnstile> ⟨e,(h,l)⟩ -> ⟨e',(h',l')⟩ ==>
  (!!V. [|l V = Some v; E V = Some T;
      P \<turnstile> T casts v'' to v; l' V = Some v'|]
  ==> P \<turnstile> T casts v' to v')"
and "P,E \<turnstile> ⟨es,(h,l)⟩ [->] ⟨es',(h',l')⟩ ==>
  (!!V. [|l V = Some v; E V = Some T;
      P \<turnstile> T casts v'' to v; l' V = Some v'|]
  ==> P \<turnstile> 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 \<turnstile> T casts v'' to v " by fact+
  from l1 l2 have eq:"v = v'" by simp
  with casts wf show ?case by(fastsimp intro:casts_casts)
next
  case (RedLAss E V T' w w' h l V')
  have l:"l V' = Some v" and lupd:"(l(V \<mapsto> w')) V' = Some v'"
    and T'casts:"P \<turnstile> T' casts w to w'"
    and env:"E V = Some T'" and env':"E V' = Some T"
    and casts:"P \<turnstile> 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(fastsimp intro:casts_casts)
  next
    case False
    with l lupd have "v = v'" by (auto split:split_if_asm)
    with casts wf show ?thesis by(fastsimp 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 \<turnstile> T' casts w to w'"
    and casts:"P \<turnstile> T casts v'' to v" by fact+
  from l1 l2 have eq:"v = v'" by simp
  with casts wf show ?case by(fastsimp 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 \<turnstile> T casts v'' to v"
    and IH:"!!V'. [|(l(V := None)) V' = Some v; (E(V \<mapsto> T')) V' = Some T; 
                  P \<turnstile> T casts v'' to v ; l' V' = Some v'|]
            ==> P \<turnstile> 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(fastsimp 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:split_if_asm)
    from env False have env':"(E(V \<mapsto> T')) V' = Some T" by fastsimp
    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 \<turnstile> T casts v'' to v"
    and IH:"!!V'. [|(l(V := None)) V' = Some v; (E(V \<mapsto> T')) V' = Some T; 
                   P \<turnstile> T casts v'' to v ; l' V' = Some v'|]
            ==> P \<turnstile> 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(fastsimp 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:split_if_asm)
    from env False have env':"(E(V \<mapsto> T')) V' = Some T" by fastsimp
    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 \<turnstile> T casts v'' to v"
    and IH:"!!V'. [|(l(V \<mapsto> w')) V' = Some v; (E(V \<mapsto> T')) V' = Some T; 
                   P \<turnstile> T casts v'' to v ; l' V' = Some v'|]
            ==> P \<turnstile> 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(fastsimp intro:casts_casts)
  next
    case False
    with l  l'upd have lnew:"(l(V \<mapsto> w')) V' = Some v"
      and l'new:"l' V' = Some v'" by (auto split:split_if_asm)
    from env False have env':"(E(V \<mapsto> T')) V' = Some T" by fastsimp
    from IH[OF lnew env' casts l'new] show ?thesis .
  qed
qed (auto intro:casts_casts wf)

  


section{*Small steps simulate big step*}

subsection {*Cast*}

lemma StaticCastReds:
  "P,E \<turnstile> ⟨e,s⟩ ->* ⟨e',s'⟩ ==> P,E \<turnstile> ⟨(|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 \<turnstile> ⟨e,s⟩ ->* ⟨null,s'⟩ ==> P,E \<turnstile> ⟨(|C|)),e,s⟩ ->* ⟨null,s'⟩"

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


lemma StaticUpCastReds:
  "[| P,E \<turnstile> ⟨e,s⟩ ->* ⟨ref(a,Cs),s'⟩; P \<turnstile> Path last Cs to C via Cs'; Ds = Cs@pCs' |] 
  ==> P,E \<turnstile> ⟨(|C|)),e,s⟩ ->* ⟨ref(a,Ds),s'⟩"

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


lemma StaticDownCastReds:
  "P,E \<turnstile> ⟨e,s⟩ ->* ⟨ref(a,Cs@[C]@Cs'),s'⟩
  ==>  P,E \<turnstile> ⟨(|C|)),e,s⟩ ->* ⟨ref(a,Cs@[C]),s'⟩"

apply(rule rtrancl_into_rtrancl)
 apply(erule StaticCastReds)
apply simp
apply(subgoal_tac "P,E \<turnstile> ⟨(|C|)),ref(a,Cs@[C]@Cs'),s'⟩ -> ⟨ref(a,Cs@[C]),s'⟩")
 apply simp
apply(rule RedStaticDownCast)
done


lemma StaticCastRedsFail:
  "[| P,E \<turnstile> ⟨e,s⟩ ->* ⟨ref(a,Cs),s'⟩; C ∉ set Cs; ¬ P \<turnstile> (last Cs) \<preceq>* C |]
  ==> P,E \<turnstile> ⟨(|C|)),e,s⟩ ->* ⟨THROW ClassCast,s'⟩"

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


lemma StaticCastRedsThrow:
  "[| P,E \<turnstile> ⟨e,s⟩ ->* ⟨Throw r,s'⟩ |] ==> P,E \<turnstile> ⟨(|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 \<turnstile> ⟨e,s⟩ ->* ⟨e',s'⟩ ==> P,E \<turnstile> ⟨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 \<turnstile> ⟨e,s⟩ ->* ⟨null,s'⟩ ==> P,E \<turnstile> ⟨Cast C e,s⟩ ->* ⟨null,s'⟩"

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


lemma DynCastRedsRef:
  "[| P,E \<turnstile> ⟨e,s⟩ ->* ⟨ref(a,Cs),s'⟩; hp s' a = Some (D,S); P \<turnstile> Path D to C via Cs';
     P \<turnstile> Path D to C unique |] 
 ==> P,E \<turnstile> ⟨Cast C e,s⟩ ->* ⟨ref(a,Cs'),s'⟩"

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


lemma StaticUpDynCastReds:
  "[| P,E \<turnstile> ⟨e,s⟩ ->* ⟨ref(a,Cs),s'⟩; P \<turnstile> Path last Cs to C unique;
  P \<turnstile> Path last Cs to C via Cs'; Ds = Cs@pCs' |] 
  ==> P,E \<turnstile> ⟨Cast C e,s⟩ ->* ⟨ref(a,Ds),s'⟩"

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


lemma StaticDownDynCastReds:
  "P,E \<turnstile> ⟨e,s⟩ ->* ⟨ref(a,Cs@[C]@Cs'),s'⟩
  ==>  P,E \<turnstile> ⟨Cast C e,s⟩ ->* ⟨ref(a,Cs@[C]),s'⟩"

apply(rule rtrancl_into_rtrancl)
 apply(erule DynCastReds)
apply simp
apply(subgoal_tac "P,E \<turnstile> ⟨Cast C (ref(a,Cs@[C]@Cs')),s'⟩ -> ⟨ref(a,Cs@[C]),s'⟩")
 apply simp
apply(rule RedStaticDownDynCast)
done


lemma DynCastRedsFail:
  "[| P,E \<turnstile> ⟨e,s⟩ ->* ⟨ref(a,Cs),s'⟩; hp s' a = Some (D,S); ¬ P \<turnstile> Path D to C unique;
    ¬ P \<turnstile> Path last Cs to C unique; C ∉ set Cs |]
  ==> P,E \<turnstile> ⟨Cast C e,s⟩ ->* ⟨null,s'⟩"

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


lemma DynCastRedsThrow:
  "[| P,E \<turnstile> ⟨e,s⟩ ->* ⟨Throw r,s'⟩ |] ==> P,E \<turnstile> ⟨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 \<turnstile> ⟨e,s⟩ ->* ⟨e',s'⟩ ==> P,E \<turnstile> ⟨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 \<turnstile> ⟨e,s⟩ ->* ⟨Val v,(h',l')⟩; E V = Some T; P \<turnstile> T casts v to v'|] 
  ==> P,E \<turnstile> ⟨ V:=e,s⟩ ->* ⟨Val v',(h',l'(V\<mapsto>v'))⟩"

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


lemma LAssRedsThrow:
  "[| P,E \<turnstile> ⟨e,s⟩ ->* ⟨Throw r,s'⟩ |] ==> P,E \<turnstile> ⟨ 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 \<turnstile> ⟨e,s⟩ ->* ⟨e',s'⟩ ==> P,E \<turnstile> ⟨ 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 \<turnstile> ⟨e,s⟩ ->* ⟨e',s'⟩ ==> P,E \<turnstile> ⟨(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 \<turnstile> ⟨e1,s0⟩ ->* ⟨Val v1,s1⟩; P,E \<turnstile> ⟨e2,s1⟩ ->* ⟨Val v2,s2⟩; 
     binop(bop,v1,v2) = Some v |]
  ==> P,E \<turnstile> ⟨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 \<turnstile> ⟨e,s⟩ ->* ⟨Throw r,s'⟩ ==> P,E \<turnstile> ⟨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 \<turnstile> ⟨e1,s0⟩ ->* ⟨Val v1,s1⟩; P,E \<turnstile> ⟨e2,s1⟩ ->* ⟨Throw r,s2⟩|]
  ==> P,E \<turnstile> ⟨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 \<turnstile> ⟨e,s⟩ ->* ⟨e',s'⟩ ==> P,E \<turnstile> ⟨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 \<turnstile> ⟨e,s⟩ ->* ⟨ref(a,Cs'),s'⟩; hp s' a = Some(D,S); 
    Ds = Cs'@pCs; (Ds,fs) ∈ S; fs F = Some v |]
  ==> P,E \<turnstile> ⟨e•F{Cs},s⟩ ->* ⟨Val v,s'⟩"

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


lemma FAccRedsNull:
  "P,E \<turnstile> ⟨e,s⟩ ->* ⟨null,s'⟩ ==> P,E \<turnstile> ⟨e•F{Cs},s⟩ ->* ⟨THROW NullPointer,s'⟩"

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


lemma FAccRedsThrow:
  "P,E \<turnstile> ⟨e,s⟩ ->* ⟨Throw r,s'⟩ ==> P,E \<turnstile> ⟨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 \<turnstile> ⟨e,s⟩ ->* ⟨e',s'⟩ ==> P,E \<turnstile> ⟨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 \<turnstile> ⟨e,s⟩ ->* ⟨e',s'⟩ ==> P,E \<turnstile> ⟨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 \<turnstile> ⟨e1,s0⟩ ->* ⟨ref(a,Cs'),s1⟩; P,E \<turnstile> ⟨e2,s1⟩ ->* ⟨Val v,(h2,l2)⟩; 
    h2 a = Some(D,S); P \<turnstile> (last Cs') has least F:T via Cs; P \<turnstile> T casts v to v';
    Ds = Cs'@pCs; (Ds,fs) ∈ S |] ==>
  P,E \<turnstile> ⟨e1•F{Cs}:=e2, s0⟩ ->* 
        ⟨Val v',(h2(a\<mapsto>(D,insert (Ds,fs(F\<mapsto>v')) (S - {(Ds,fs)}))),l2)⟩"

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


lemma FAssRedsNull:
  "[| P,E \<turnstile> ⟨e1,s0⟩ ->* ⟨null,s1⟩; P,E \<turnstile> ⟨e2,s1⟩ ->* ⟨Val v,s2⟩ |] ==>
  P,E \<turnstile> ⟨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 \<turnstile> ⟨e,s⟩ ->* ⟨Throw r,s'⟩ ==> P,E \<turnstile> ⟨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 \<turnstile> ⟨e1,s0⟩ ->* ⟨Val v,s1⟩; P,E \<turnstile> ⟨e2,s1⟩ ->* ⟨Throw r,s2⟩ |]
  ==> P,E \<turnstile> ⟨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 \<turnstile> ⟨e,s⟩ ->* ⟨e',s'⟩ ==> P,E \<turnstile> ⟨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 \<turnstile> ⟨e,s⟩ ->* ⟨Throw r,s'⟩ ==> P,E \<turnstile> ⟨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 \<turnstile> ⟨e1,s0⟩ ->* ⟨Val v1,s1⟩; P,E \<turnstile> ⟨e2,s1⟩ ->* ⟨e2',s2⟩ |] ==> P,E \<turnstile> ⟨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 \<turnstile> ⟨e,s⟩ ->* ⟨e',s'⟩ ==> P,E \<turnstile> ⟨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 \<turnstile> ⟨e,s⟩ ->* ⟨Throw r,s'⟩ ==> P,E \<turnstile> ⟨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 \<turnstile> ⟨e,s0⟩ ->* ⟨true,s1⟩; P,E \<turnstile> ⟨e1, s1⟩ ->* ⟨e',s2⟩ |] ==> P,E \<turnstile> ⟨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 \<turnstile> ⟨e,s0⟩ ->* ⟨false,s1⟩; P,E \<turnstile> ⟨e2, s1⟩ ->* ⟨e',s2⟩ |] ==> P,E \<turnstile> ⟨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 \<turnstile> ⟨b,s⟩ ->* ⟨false,s'⟩ ==> P,E \<turnstile> ⟨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 \<turnstile> ⟨b,s⟩ ->* ⟨Throw r,s'⟩ ==> P,E \<turnstile> ⟨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 \<turnstile> ⟨b,s0⟩ ->* ⟨true,s1⟩; P,E \<turnstile> ⟨c,s1⟩ ->* ⟨Val v1,s2⟩; P,E \<turnstile> ⟨while (b) c,s2⟩ ->* ⟨e,s3⟩ |]
  ==> P,E \<turnstile> ⟨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 \<turnstile> ⟨b,s0⟩ ->* ⟨true,s1⟩; P,E \<turnstile> ⟨c,s1⟩ ->* ⟨Throw r,s2⟩ |]
  ==> P,E \<turnstile> ⟨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 \<turnstile> ⟨e,s⟩ ->* ⟨e',s'⟩ ==> P,E \<turnstile> ⟨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 \<turnstile> ⟨e,s⟩ ->* ⟨null,s'⟩ ==> P,E \<turnstile> ⟨throw e,s⟩ ->* ⟨THROW NullPointer,s'⟩"

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


lemma ThrowRedsThrow:
  "P,E \<turnstile> ⟨e,s⟩ ->* ⟨Throw r,s'⟩ ==> P,E \<turnstile> ⟨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 \<mapsto> T) \<turnstile> ⟨e,s⟩ ->* ⟨e',s'⟩ ==>
  ∀h l h' l' v v'. s = (h,l(V\<mapsto>v')) --> 
                   P \<turnstile> T casts v to v' --> s' = (h',l') -->
                   (∃v'' w. P,E \<turnstile> ⟨{V:T := Val v; e},(h,l)⟩ ->* 
                                ⟨{V:T := Val v''; e'},(h',l'(V:=(l V)))⟩ ∧
                            P \<turnstile> T casts v'' to w)"
proof (erule converse_rtrancl_induct2)
  { fix h l h' l' v v'
    assume "s' = (h, l(V \<mapsto> v'))" and "s' = (h', l')"
    hence h:"h = h'" and l':"l' = l(V \<mapsto> v')" by simp_all
    hence "P,E \<turnstile> ⟨{V:T; V:=Val v;; e'},(h, l)⟩ ->*
                 ⟨{V:T; V:=Val v;; e'},(h', l'(V := l V))⟩"
      by(fastsimp simp: fun_upd_same simp del:fun_upd_apply) }
  hence "∀h l h' l' v v'.
         s' = (h, l(V \<mapsto> v')) -->
           P \<turnstile> T casts v to v'  -->
             s' = (h', l') -->
               P,E \<turnstile> ⟨{V:T; V:=Val v;; e'},(h, l)⟩ ->*
                     ⟨{V:T; V:=Val v;; e'},(h', l'(V := l V))⟩ ∧
               P \<turnstile> T casts v to v'"
    by auto
  thus "∀h l h' l' v v'.
       s' = (h, l(V \<mapsto> v')) -->
         P \<turnstile> T casts v to v'  -->
           s' = (h', l') -->
             (∃v'' w. P,E \<turnstile> ⟨{V:T; V:=Val v;; e'},(h, l)⟩ ->*
                            ⟨{V:T; V:=Val v'';; e'},(h', l'(V := l V))⟩ ∧
                      P \<turnstile> T casts v'' to w)"
    by auto
next
  fix e s e'' s''
  assume Red:"((e,s),e'',s'') ∈ Red P (E(V \<mapsto> T))"
    and reds:"P,E(V \<mapsto> T) \<turnstile> ⟨e'',s''⟩ ->* ⟨e',s'⟩"
    and IH:"∀h l h' l' v v'.
           s'' = (h, l(V \<mapsto> v')) -->
             P \<turnstile> T casts v to v'  -->
               s' = (h', l') -->
                 (∃v'' w. P,E \<turnstile> ⟨{V:T; V:=Val v;; e''},(h, l)⟩ ->*
                                ⟨{V:T; V:=Val v'';; e'},(h', l'(V := l V))⟩ ∧
                          P \<turnstile> T casts v'' to w)"
  { fix h l h' l' v v'
    assume s:"s = (h, l(V \<mapsto> v'))" and s':"s' = (h', l')"
      and casts:"P \<turnstile> 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 (fastsimp dest:red_lcl_incr)
    then obtain v'' where l'':"l'' V = Some v''" by auto
    with Red s s'' casts
    have step:"P,E \<turnstile> ⟨{V:T := Val v; e},(h, l)⟩ ->  
              ⟨{V:T := Val v''; e''}, (h'',l''(V := l V))⟩"
      by(fastsimp intro:InitBlockRed)
    from Red s s'' l'' casts wf
    have casts':"P \<turnstile> T casts v'' to v''" by(fastsimp intro:Some_lcl_casts_values)
    with IH s'' s' l'' obtain v''' w
      where "P,E \<turnstile> ⟨{V:T := Val v''; e''}, (h'',l''(V := l V))⟩ ->*
                   ⟨{V:T := Val v'''; e'},(h', l'(V := l V))⟩ ∧
             P \<turnstile> 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 \<turnstile> ⟨{V:T; V:=Val v;; e},(h, l)⟩ ->*
                                   ⟨{V:T; V:=Val v'';; e'},(h', l'(V := l V))⟩ ∧
                            P \<turnstile> 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 \<mapsto> v')) -->
             P \<turnstile> T casts v to v'  -->
             s' = (h', l') -->
             (∃v'' w. P,E \<turnstile> ⟨{V:T; V:=Val v;; e},(h, l)⟩ ->*
                            ⟨{V:T; V:=Val v'';; e'},(h', l'(V := l V))⟩ ∧
                      P \<turnstile> T casts v'' to w)"
    by auto
qed



lemma InitBlockReds:
 "[|P,E(V \<mapsto> T) \<turnstile> ⟨e, (h,l(V\<mapsto>v'))⟩ ->* ⟨e', (h',l')⟩; 
   P \<turnstile> T casts v to v'; wf_prog wf_md P |] ==>
  ∃v'' w. P,E \<turnstile> ⟨{V:T := Val v; e}, (h,l)⟩ ->* 
              ⟨{V:T := Val v''; e'}, (h',l'(V:=(l V)))⟩ ∧
          P \<turnstile> T casts v'' to w"
by(blast dest:InitBlockReds_aux)

lemma InitBlockRedsFinal:
  assumes reds:"P,E(V \<mapsto> T) \<turnstile> ⟨e,(h,l(V\<mapsto>v'))⟩ ->* ⟨e',(h',l')⟩"
  and final:"final e'" and casts:"P \<turnstile> T casts v to v'"
  and wf:"wf_prog wf_md P"
  shows "P,E \<turnstile> ⟨{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 \<turnstile> ⟨{V:T := Val v; e},(h,l)⟩ ->* 
                        ⟨{V:T := Val v''; e'}, (h',l'(V:=(l V)))⟩"
    and casts':"P \<turnstile> T casts v'' to w"
    by (auto dest:InitBlockReds)
  from final casts casts'
  have step:"P,E \<turnstile> ⟨{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(fastsimp intro:rtrancl_into_rtrancl)
qed



subsection {*Block*}

lemma BlockRedsFinal:
assumes reds: "P,E(V \<mapsto> T) \<turnstile> ⟨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 \<turnstile> ⟨{V:T; e0},(h0,l0)⟩ ->* ⟨e2,(h2,l2(V:=l0 V))⟩"

using reds
proof (induct rule:converse_rtrancl_induct2)
  case refl thus ?case
    by(fastsimp 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 \<mapsto> T))"
   and reds: "P,E(V \<mapsto> T) \<turnstile> ⟨e1,s1⟩ ->* ⟨e2,(h2,l2)⟩"
   and IH: "!!h l. s1 = (h,l(V := None))
                ==> P,E \<turnstile> ⟨{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 fastsimp
  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 \<mapsto> v'))" and casts:"P \<turnstile> 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 \<mapsto> T) \<turnstile> ⟨e1,s1⟩ -> ⟨e',s'⟩"
      and reds': "P,E(V \<mapsto> T) \<turnstile> ⟨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(fastsimp 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 \<turnstile> ⟨{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 \<turnstile> ⟨{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 \<turnstile> T casts v to v"
        by(fastsimp intro:None_lcl_casts_values)
      from Some
      have "P,E \<turnstile> ⟨{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 \<turnstile> ⟨{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 \<turnstile> ⟨e,s⟩ ->* ⟨e',s'⟩ ==> P,E \<turnstile> ⟨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 \<turnstile> ⟨es,s⟩ [->]* ⟨es',s'⟩ ==> P,E \<turnstile> ⟨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 \<turnstile> ⟨e,s0⟩ ->* ⟨Val v,s1⟩; P,E \<turnstile> ⟨es,s1⟩ [->]* ⟨es',s2⟩ |]
  ==> P,E \<turnstile> ⟨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 \<turnstile> ⟨e,(h,l)⟩ -> ⟨e',(h',l')⟩ ==> fv e' ⊆ fv e"
  and  "P,E \<turnstile> ⟨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 prems by(fastsimp dest!:select_method_wf_mdecl simp:wf_mdecl_def)
  with prems 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 prems by(fastsimp dest!:has_least_wf_mdecl simp:wf_mdecl_def)
  with prems show ?case
    by auto
qed auto



lemma Red_dom_lcl:
  "P,E \<turnstile> ⟨e,(h,l)⟩ -> ⟨e',(h',l')⟩ ==> dom l' ⊆ dom l ∪ fv e" and
  "P,E \<turnstile> ⟨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 (fastsimp split:if_splits)
next
  case BlockRedSome thus ?case by clarsimp (fastsimp split:if_splits)
next
  case InitBlockRed thus ?case by clarsimp (fastsimp split:if_splits)
qed auto



lemma Reds_dom_lcl:
  "[| wwf_prog P; P,E \<turnstile> ⟨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\<mapsto>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 \<turnstile> Ts Casts vs to vs';
        P,E(Vs [\<mapsto>] Ts) \<turnstile> ⟨e, (h0,l0(Vs [\<mapsto>] vs'))⟩ ->* ⟨e', (h1,l1)⟩ |]
  ==> ∃vs''. P,E \<turnstile> ⟨blocks(Vs,Ts,vs,e), (h0,l0)⟩ ->* 
                   ⟨blocks(Vs,Ts,vs'',e'), (h1,override_on l1 l0 (set Vs))⟩ ∧ 
             (∃ws. P \<turnstile> Ts Casts vs'' to ws) ∧ length vs = length vs''"

proof(induct Vs Ts vs e rule:blocks.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 \<turnstile> (T#Ts) Casts (v#vs) to vs'"
    and reds:"P,E(V#Vs [\<mapsto>] T#Ts) \<turnstile> ⟨e,(h0,l0(V#Vs [\<mapsto>] vs'))⟩ ->* ⟨e',(h1,l1)⟩"
    and IH:"!!l0 E vs''. [|length Vs = length Ts; length vs = length Ts; 
       distinct Vs; P \<turnstile> Ts Casts vs to vs'';
       P,E(Vs [\<mapsto>] Ts) \<turnstile> ⟨e,(h0,l0(Vs [\<mapsto>] vs''))⟩ ->* ⟨e',(h1,l1)⟩|]
        ==> ∃vs''. P,E \<turnstile> ⟨blocks (Vs,Ts,vs,e),(h0,l0)⟩ ->*
                         ⟨blocks (Vs,Ts,vs'',e'),(h1, override_on l1 l0 (set Vs))⟩ ∧
                   (∃ws. P \<turnstile> 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 \<mapsto> T)(Vs [\<mapsto>] Ts) \<turnstile> ⟨e,(h0,l0(V \<mapsto> x)(Vs [\<mapsto>] xs))⟩ 
                                    ->* ⟨e',(h1,l1)⟩"
    by simp
  from casts vs' have casts':"P \<turnstile> Ts Casts vs to xs" 
    and cast':"P \<turnstile> 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 \<mapsto> T) \<turnstile> ⟨blocks (Vs, Ts, vs, e),(h0, l0(V \<mapsto> x))⟩ ->*
             ⟨blocks (Vs, Ts, vs'', e'),(h1, override_on l1 (l0(V \<mapsto> x)) (set Vs))⟩"
    and castsws:"P \<turnstile> 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 \<turnstile> ⟨{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 \<mapsto> x)) (set Vs))(V := l0 V))⟩"
    and "P \<turnstile> T casts v'' to w" by auto
  with castsws have "P \<turnstile> 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 \<turnstile> [] Casts [] to vs'" 
    and step:"P,E([] [\<mapsto>] []) \<turnstile> ⟨e,(h0, l0([] [\<mapsto>] vs'))⟩ ->* ⟨e',(h1, l1)⟩" by fact+
  from casts have "vs' = []" by(fastsimp dest:length_Casts_vs')
  with step have "P,E \<turnstile> ⟨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 \<turnstile> Ts Casts vs to vs' |] ==>
       P,E \<turnstile> ⟨blocks(Vs,Ts,vs,e), (h,l)⟩ ->* ⟨e, (h,l)⟩"

proof(induct Vs Ts vs e rule:blocks.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 \<turnstile> T # Ts Casts v # vs to vs'"
    and IH:"!!E l vs'. [|length Vs = length Ts; length vs = length Ts; final e;
                   P \<turnstile> Ts Casts vs to vs' |]
                  ==> P,E \<turnstile> ⟨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 \<turnstile> Ts Casts vs to xs" 
    and cast':"P \<turnstile> 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 \<turnstile> ⟨{V:T; V:=Val v;; blocks (Vs, Ts, vs, e)},(h, l)⟩ ->*
                        ⟨{V:T; V:=Val v'';; e},(h,l)⟩"
    and "P \<turnstile> T casts v'' to w" by auto blast
  with final have "P,E \<turnstile> ⟨{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 \<turnstile> Ts Casts vs to vs'"
  and reds: "P,E(Vs [\<mapsto>] Ts) \<turnstile> ⟨e, (h0, l0(Vs [\<mapsto>] vs'))⟩ ->* ⟨e', (h1, l1)⟩"
  and fin: "final e'" and l2: "l2 = override_on l1 l0 (set Vs)"
shows blocksRedsFinal: "P,E \<turnstile> ⟨blocks(Vs,Ts,vs,e), (h0, l0)⟩ ->* ⟨e', (h1,l2)⟩"

proof -
  obtain vs'' ws where blocks:"P,E \<turnstile> ⟨blocks(Vs,Ts,vs,e), (h0, l0)⟩ ->* 
                                  ⟨blocks(Vs,Ts,vs'',e'), (h1,l2)⟩"
    and length:"length vs = length vs''"
    and casts':"P \<turnstile> Ts Casts vs'' to ws"
    using l2 blocksReds[OF wfmd wf casts reds]
     by auto
   have "P,E \<turnstile> ⟨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 \<turnstile> ⟨e,s⟩ ->* ⟨e',s'⟩ ==> 
  P,E \<turnstile> ⟨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 \<turnstile> ⟨es,s⟩ [->]* ⟨es',s'⟩ ==> 
  P,E \<turnstile> ⟨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 \<turnstile> ⟨(|C|)),(Val v),(h,l)⟩ -> ⟨Val v',(h,l)⟩ ==>
   P,E \<turnstile> ⟨(|C|)),(Val v),(h,l')⟩ -> ⟨Val v',(h,l')⟩"

apply(erule red.cases)
apply(auto intro:red_reds.intros)
apply(subgoal_tac "P,E \<turnstile> ⟨(|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 \<turnstile> ⟨(|C|)),(Val v),(h,l)⟩ -> ⟨Val v',(h,l)⟩ ==> 
   P,E' \<turnstile> ⟨(|C|)),(Val v),(h,l)⟩ -> ⟨Val v',(h,l)⟩"

apply(erule red.cases)
apply(auto intro:red_reds.intros)
apply(subgoal_tac "P,E' \<turnstile> ⟨(|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 \<turnstile> ⟨(|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 \<turnstile> ⟨e,s⟩ ->* ⟨e',s'⟩ ==> 
  (!!e1. [|e = (|C|)),e0; e' = (|C|)),e1|] ==> P,E \<turnstile> ⟨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 \<turnstile> ⟨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 \<turnstile> ⟨e0,s⟩ ->* ⟨e1,s''⟩" by fact+
  from Red have red:"P,E \<turnstile> ⟨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 \<turnstile> ⟨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 \<turnstile> ⟨(|C|)),e,s⟩ ->* ⟨e',s'⟩; final e'|] ==>
∃e'' s''. P,E \<turnstile> ⟨e,s⟩ ->* ⟨e'',s''⟩ ∧ P,E \<turnstile> ⟨(|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 \<turnstile> ⟨(|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 \<turnstile> ⟨e,s⟩ ->* ⟨ex,sx⟩ ∧ P,E \<turnstile> ⟨(|C|)),ex,sx⟩ -> ⟨e'',s''⟩ ∧ final ex" by fact+
  from Red have red:"P,E \<turnstile> ⟨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 \<turnstile> ⟨e,s⟩ ->* ⟨ex,s''⟩"
      by(fastsimp intro:Cast_red)
    with e'' red final' show ?thesis by blast
  qed
qed


lemma Cast_final_eq:
  assumes red:"P,E \<turnstile> ⟨(|C|)),e,(h,l)⟩ -> ⟨e',(h,l)⟩"
  and final:"final e" and final':"final e'"
  shows "P,E' \<turnstile> ⟨(|C|)),e,(h,l')⟩ -> ⟨e',(h,l')⟩"

proof -
  from red final show ?thesis
  proof(auto simp:final_def)
    fix v assume "P,E \<turnstile> ⟨(|C|)),(Val v),(h,l)⟩ -> ⟨e',(h,l)⟩"
    with final' show "P,E' \<turnstile> ⟨(|C|)),(Val v),(h,l')⟩ -> ⟨e',(h,l')⟩"
    proof(auto simp:final_def)
      fix v' assume "P,E \<turnstile> ⟨(|C|)),(Val v),(h,l)⟩ -> ⟨Val v',(h,l)⟩"
      thus "P,E' \<turnstile> ⟨(|C|)),(Val v),(h,l')⟩ -> ⟨Val v',(h,l')⟩"
        by(auto intro:cast_lcl cast_env)
    next
      fix a Cs assume "P,E \<turnstile> ⟨(|C|)),(Val v),(h,l)⟩ -> ⟨Throw (a,Cs),(h,l)⟩"
      thus "P,E' \<turnstile> ⟨(|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 \<turnstile> ⟨(|C|)),(Throw (a,Cs)),(h,l)⟩ -> ⟨e',(h,l)⟩"
    with final' show "P,E' \<turnstile> ⟨(|C|)),(Throw (a,Cs)),(h,l')⟩ -> ⟨e',(h,l')⟩"
    proof(auto simp:final_def)
      fix v assume "P,E \<turnstile> ⟨(|C|)),(Throw (a,Cs)),(h,l)⟩ -> ⟨Val v,(h,l)⟩"
      thus "P,E' \<turnstile> ⟨(|C|)),(Throw (a,Cs)),(h,l')⟩ -> ⟨Val v,(h,l')⟩"
        by(auto elim:red.cases)
    next
      fix a' Cs'
      assume "P,E \<turnstile> ⟨(|C|)),(Throw (a,Cs)),(h,l)⟩ -> ⟨Throw (a',Cs'),(h,l)⟩"
      thus "P,E' \<turnstile> ⟨(|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 \<turnstile> ⟨e,s0⟩ ->* ⟨ref(a,Cs),s1⟩"
      "P,E \<turnstile> ⟨es,s1⟩ [->]* ⟨map Val vs,(h2,l2)⟩"
and hp: "h2 a = Some(C,S)"
and method: "P \<turnstile> last Cs has least M = (Ts',T',pns',body') via Ds"
and select: "P \<turnstile> (C,Cs@pDs) selects M = (Ts,T,pns,body) via Cs'"
and size: "size vs = size pns"
and casts: "P \<turnstile> Ts Casts vs to vs'"
and l2': "l2' = [this \<mapsto> Ref(a,Cs'), pns[\<mapsto>]vs']"
and body_case:"new_body = (case T' of Class D => (|D|)),body  | _ => body)"
and body: "P,E(this \<mapsto> Class (last Cs'), pns [\<mapsto>] Ts) \<turnstile> ⟨new_body,(h2,l2')⟩ ->* ⟨ef,(h3,l3)⟩"
and final:"final ef"
shows "P,E \<turnstile> ⟨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 prems by(fastsimp 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(fastsimp simp add:map_add_def override_on_def expand_fun_eq)
  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 \<turnstile> 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 \<turnstile> Class (last Cs')#Ts Casts Ref(a,Cs')#vs to  Ref(a,Cs')#vs'"
    by -(rule Casts_Cons)
  have 1:"P,E \<turnstile> ⟨e•M(es),s0⟩ ->* ⟨(ref(a,Cs))•M(es),s1⟩" by(rule CallRedsObj)(rule assms(2))
  have 2:"P,E \<turnstile> ⟨(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 \<mapsto> Class (last Cs'), pns [\<mapsto>] Ts) \<turnstile> 
             ⟨new_body,(h2,l2(this\<mapsto> Ref(a,Cs'), pns[\<mapsto>]vs'))⟩ ->* ⟨ef,(h3,l2++l3)⟩"
    by (simp add:l2')
  show ?thesis
  proof(cases "∀C. T'≠ Class C")
    case True
    hence "P,E \<turnstile> ⟨(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 \<turnstile> ⟨(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 \<turnstile> ⟨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 \<mapsto> Class (last Cs'),pns [\<mapsto>] Ts) \<turnstile> 
                           ⟨body,(h2,l2(this\<mapsto> Ref(a,Cs'), pns[\<mapsto>]vs'))⟩ ->* ⟨e',s'⟩"
      and final':"final e'" 
      and cast:"P,E(this \<mapsto> Class (last Cs'), pns [\<mapsto>] Ts) \<turnstile> ⟨(|D|)),e',s'⟩ -> 
                                                           ⟨ef,(h3,l2++l3)⟩"
      by(cases T')(auto dest:Cast_final)
    from T' have "P,E \<turnstile> ⟨(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 \<turnstile> ⟨(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 \<turnstile> ⟨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 \<turnstile> ⟨(|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 \<turnstile> ⟨(|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(fastsimp intro:Cast_final_eq)
    ultimately
    have "P,E \<turnstile> ⟨(|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 \<turnstile> ⟨e,s0⟩ ->* ⟨ref(a,Cs),s1⟩"
      "P,E \<turnstile> ⟨es,s1⟩ [->]* ⟨map Val vs,(h2,l2)⟩"
and path_unique: "P \<turnstile> Path (last Cs) to C unique"
and path_via: "P \<turnstile> Path (last Cs) to C via Cs''" 
and Ds: "Ds = (Cs@pCs'')@pCs'"
and least: "P \<turnstile> C has least M = (Ts,T,pns,body) via Cs'"
and size: "size vs = size pns"
and casts: "P \<turnstile> Ts Casts vs to vs'"
and l2': "l2' = [this \<mapsto> Ref(a,Ds), pns[\<mapsto>]vs']"
and body: "P,E(this\<mapsto>Class(last Ds), pns[\<mapsto>]Ts) \<turnstile> ⟨body,(h2,l2')⟩ ->* ⟨ef,(h3,l3)⟩"
and final:"final ef"
shows "P,E \<turnstile> ⟨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 prems by(fastsimp 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(fastsimp simp add:map_add_def override_on_def expand_fun_eq)
  from wwf least have "Cs' ≠ []"
    by (auto elim!:Subobjs_nonempty simp:LeastMethodDef_def MethodDefs_def)
  with Ds have "last Cs' = last Ds" by(fastsimp 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 \<turnstile> 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 \<turnstile> Class (last Ds)#Ts Casts Ref(a,Ds)#vs to Ref(a,Ds)#vs'"
    by -(rule Casts_Cons)
  have 1:"P,E \<turnstile> ⟨e•(C::)M(es),s0⟩ ->* ⟨(ref(a,Cs))•(C::)M(es),s1⟩"
    by(rule CallRedsObj)(rule assms(2))
  have 2:"P,E \<turnstile> ⟨(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\<mapsto>Class(last Ds), pns[\<mapsto>]Ts) \<turnstile> 
              ⟨body,(h2,l2(this\<mapsto> Ref(a,Ds), pns[\<mapsto>]vs'))⟩ ->* ⟨ef,(h3,l2++l3)⟩"
    by (simp add:l2')
  have "P,E \<turnstile> ⟨(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 \<turnstile> ⟨(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 \<turnstile> ⟨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 \<turnstile> ⟨e,s0⟩ ->* ⟨Val v,s1⟩;  
    P,E \<turnstile> ⟨es,s1⟩ [->]* ⟨map Val vs1 @ Throw ex # es2,s2⟩ |]
  ==> P,E \<turnstile> ⟨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 \<turnstile> ⟨e,s0⟩ ->* ⟨Throw ex,s1⟩ ==> P,E \<turnstile> ⟨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 \<turnstile> ⟨e,s0⟩ ->* ⟨null,s1⟩; P,E \<turnstile> ⟨es,s1⟩ [->]* ⟨map Val vs,s2⟩ |]
  ==> P,E \<turnstile> ⟨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 \<turnstile> ⟨e,s⟩ => ⟨e',s'⟩ ==> P,E \<turnstile> ⟨e,s⟩ ->* ⟨e',s'⟩"
and bigs_by_smalls: "P,E \<turnstile> ⟨es,s⟩ [=>] ⟨es',s'⟩ ==> P,E \<turnstile> ⟨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(fastsimp intro:DynCastRedsRef)
next
  case DynCastNull thus ?case by(simp add:DynCastRedsNull)
next
  case DynCastFail thus ?case by(fastsimp 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(fastsimp simp:BinOpRedsVal)
next
  case BinOpThrow1 thus ?case by(fastsimp dest!:eval_final simp: BinOpRedsThrow1)
next
  case BinOpThrow2 thus ?case by(fastsimp dest!:eval_final simp: BinOpRedsThrow2)
next
  case Var thus ?case by (fastsimp simp:RedVar)
next
  case LAss thus ?case by(fastsimp simp: LAssRedsVal)
next
  case LAssThrow thus ?case by(fastsimp dest!:eval_final simp: LAssRedsThrow)
next
  case FAcc thus ?case by(fastsimp intro:FAccRedsVal)
next
  case FAccNull thus ?case by(simp add:FAccRedsNull)
next
  case FAccThrow thus ?case by(fastsimp dest!:eval_final simp:FAccRedsThrow)
next
  case FAss thus ?case by(fastsimp simp:FAssRedsVal)
next
  case FAssNull thus ?case by(fastsimp simp:FAssRedsNull)
next
  case FAssThrow1 thus ?case by(fastsimp dest!:eval_final simp:FAssRedsThrow1)
next
  case FAssThrow2 thus ?case by(fastsimp dest!:eval_final simp:FAssRedsThrow2)
next
  case CallObjThrow thus ?case by(fastsimp dest!:eval_final simp:CallRedsThrowObj)
next
  case CallNull thus ?case thm CallRedsNull by(simp add:CallRedsNull)
next
  case CallParamsThrow thus ?case
    by(fastsimp 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 \<turnstile> ⟨e,s0⟩ ->* ⟨ref(a,Cs),s1⟩"
    and IHes: "P,E \<turnstile> ⟨ps,s1⟩ [->]* ⟨map Val vs,(h2,l2)⟩"
    and h2a: "h2 a = Some(C,S)"
    and method: "P \<turnstile> last Cs has least M = (Ts',T',pns',body') via Ds"
    and select: "P \<turnstile> (C,Cs@pDs) selects M = (Ts,T,pns,body) via Cs'"
    and same_length: "length vs = length pns"
    and casts: "P \<turnstile> Ts Casts vs to vs'"
    and l2': "l2' = [this \<mapsto> Ref (a,Cs'), pns[\<mapsto>]vs']"
    and body_case: "new_body = (case T' of Class D => (|D|)),body | _ => body)"
    and eval_body: "P,E(this \<mapsto> Class (last Cs'), pns [\<mapsto>] Ts) \<turnstile> 
                      ⟨new_body,(h2, l2')⟩ => ⟨e',(h3, l3)⟩"
    and IHbody: "P,E(this \<mapsto> Class (last Cs'), pns [\<mapsto>] Ts) \<turnstile> 
                      ⟨new_body,(h2, l2')⟩ ->* ⟨e',(h3, l3)⟩" by fact+
  from wwf select same_length have lengthTs:"length Ts = length vs"
    by (fastsimp dest!:select_method_wf_mdecl simp:wf_mdecl_def)
  show "P,E \<turnstile> ⟨e•M(ps),s0⟩ ->* ⟨e',(h3, l2)⟩"
    using method select same_length l2' h2a casts body_case
      IHbody eval_final[OF eval_body]
    by(fastsimp 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 \<turnstile> ⟨e,s0⟩ ->* ⟨ref(a,Cs),s1⟩"
   and IHes: "P,E \<turnstile> ⟨ps,s1⟩ [->]* ⟨map Val vs,(h2,l2)⟩"
   and path_unique: "P \<turnstile> Path last Cs to C unique"
   and path_via: "P \<turnstile> Path last Cs to C via Cs''"
   and least: "P \<turnstile> 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 \<turnstile> Ts Casts vs to vs'"
   and l2': "l2' = [this \<mapsto> Ref (a,Ds), pns[\<mapsto>]vs']"
   and eval_body: "P,E(this \<mapsto> Class (last Ds), pns [\<mapsto>] Ts) \<turnstile> 
                         ⟨body,(h2, l2')⟩ => ⟨e',(h3, l3)⟩"
   and IHbody: "P,E(this \<mapsto> Class (last Ds), pns [\<mapsto>] Ts) \<turnstile> 
                      ⟨body,(h2, l2')⟩ ->* ⟨e',(h3, l3)⟩" by fact+
 from wwf least same_length have lengthTs:"length Ts = length vs"
    by (fastsimp dest!:has_least_wf_mdecl simp:wf_mdecl_def)
  show "P,E \<turnstile> ⟨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(fastsimp intro!:StaticCallRedsFinal[OF wwf IHe IHes])
next
  case Block with wwf show ?case by(fastsimp simp: BlockRedsFinal dest:eval_final)
next
  case Seq thus ?case by(fastsimp simp:SeqReds2)
next
  case SeqThrow thus ?case by(fastsimp dest!:eval_final simp: SeqRedsThrow)
next
  case CondT thus ?case by(fastsimp simp:CondReds2T)
next
  case CondF thus ?case by(fastsimp simp:CondReds2F)
next
  case CondThrow thus ?case by(fastsimp dest!:eval_final simp:CondRedsThrow)
next
  case WhileF thus ?case by(fastsimp simp:WhileFReds)
next
  case WhileT thus ?case by(fastsimp simp: WhileTReds)
next
  case WhileCondThrow thus ?case by(fastsimp dest!:eval_final simp: WhileRedsThrow)
next
  case WhileBodyThrow thus ?case by(fastsimp dest!:eval_final simp: WhileTRedsThrow)
next
  case Throw thus ?case by(fastsimp simp:ThrowReds)
next
  case ThrowNull thus ?case by(fastsimp simp:ThrowRedsNull)
next
  case ThrowThrow thus ?case by(fastsimp dest!:eval_final simp:ThrowRedsThrow)
next
  case Nil thus ?case by simp
next
  case Cons thus ?case
    by(fastsimp intro!:Cons_eq_appendI[OF refl refl] ListRedsVal)
next
  case ConsThrow thus ?case by(fastsimp elim: ListReds1)
qed



section{*Big steps simulates small step*}


text {* The big step equivalent of @{text RedWhile}: *} 

lemma unfold_while: 
  "P,E \<turnstile> ⟨while(b) c,s⟩ => ⟨e',s'⟩  =  P,E \<turnstile> ⟨if(b) (c;;while(b) c) else (unit),s⟩ => ⟨e',s'⟩"

proof
  assume "P,E \<turnstile> ⟨while (b) c,s⟩ => ⟨e',s'⟩"
  thus "P,E \<turnstile> ⟨if (b) (c;; while (b) c) else unit,s⟩ => ⟨e',s'⟩"
    by cases (fastsimp intro: eval_evals.intros)+
next
  assume "P,E \<turnstile> ⟨if (b) (c;; while (b) c) else unit,s⟩ => ⟨e',s'⟩"
  thus "P,E \<turnstile> ⟨while (b) c,s⟩ => ⟨e',s'⟩"
  proof (cases)
    fix ex
    assume e': "e' = throw ex"
    assume "P,E \<turnstile> ⟨b,s⟩ => ⟨throw ex,s'⟩"  
    hence "P,E \<turnstile> ⟨while(b) c,s⟩ => ⟨throw ex,s'⟩" by (rule WhileCondThrow)
    with e' show ?thesis by simp
  next
    fix s1
    assume eval_false: "P,E \<turnstile> ⟨b,s⟩ => ⟨false,s1⟩"
    and eval_unit: "P,E \<turnstile> ⟨unit,s1⟩ => ⟨e',s'⟩"
    with eval_unit have "s' = s1" "e' = unit" by (auto elim: eval_cases)
    moreover from eval_false have "P,E \<turnstile> ⟨while (b) c,s⟩ => ⟨unit,s1⟩"
      by - (rule WhileF, simp)
    ultimately show ?thesis by simp
  next
    fix s1
    assume eval_true: "P,E \<turnstile> ⟨b,s⟩ => ⟨true,s1⟩"
    and eval_rest: "P,E \<turnstile> ⟨c;; while (b) c,s1⟩=>⟨e',s'⟩"
    from eval_rest show ?thesis
    proof (cases)
      fix s2 v1
      assume "P,E \<turnstile> ⟨c,s1⟩ => ⟨Val v1,s2⟩" "P,E \<turnstile> ⟨while (b) c,s2⟩ => ⟨e',s'⟩"
      with eval_true show "P,E \<turnstile> ⟨while(b) c,s⟩ => ⟨e',s'⟩" by (rule WhileT)
    next
      fix ex
      assume "P,E \<turnstile> ⟨c,s1⟩ => ⟨throw ex,s'⟩" "e' = throw ex"
      with eval_true show "P,E \<turnstile> ⟨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 \<turnstile> ⟨blocks(ps,Ts,vs,e),(h,l)⟩ => ⟨e',(h',l')⟩ |]
    ==> ∃ l'' vs'. P,E(ps [\<mapsto>] Ts) \<turnstile> ⟨e,(h,l(ps[\<mapsto>]vs'))⟩ => ⟨e',(h',l'')⟩ ∧
                   P \<turnstile> Ts Casts vs to vs' ∧ length vs' = length vs"

proof (induct ps)
  case Nil then show ?case by(fastsimp 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 \<turnstile> ⟨blocks (ps',Ts,vs,e),(h,l)⟩ => ⟨e',(h',l')⟩|]
  ==> ∃l'' vs'. P,E(ps' [\<mapsto>] Ts) \<turnstile> ⟨e,(h,l(ps' [\<mapsto>] vs'))⟩ => ⟨e',(h', l'')⟩ ∧
                P \<turnstile> 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 \<turnstile> ⟨blocks (p # ps', Ts, vs, e),(h,l)⟩ => ⟨e',(h', l')⟩" by fact
  with Ts vs
  have blocks:"P,E \<turnstile> ⟨{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 \<mapsto> T) \<turnstile> ⟨blocks (ps',Ts',vs',e),(h,l(p\<mapsto>v'))⟩ => ⟨e',(h',l''')⟩"
    and l''': "l'=l'''(p:=l p)"
    and casts:"P \<turnstile> 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 \<mapsto> T)(ps' [\<mapsto>] Ts') \<turnstile> ⟨e,(h, l(p\<mapsto>v')(ps'[\<mapsto>]vs''))⟩ => 
                                       ⟨e',(h',l'')⟩"
    and "P \<turnstile> 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 \<turnstile> ⟨(|C'|)),(blocks(ps,Ts,vs,e)),(h,l)⟩ => ⟨e',(h',l')⟩ |]
    ==> ∃ l'' vs'. P,E(ps [\<mapsto>] Ts) \<turnstile> ⟨(|C'|)),e,(h,l(ps[\<mapsto>]vs'))⟩ => ⟨e',(h',l'')⟩ ∧
                   P \<turnstile> Ts Casts vs to vs' ∧ length vs' = length vs"

proof (induct ps)
  case Nil then show ?case by(fastsimp 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 \<turnstile> ⟨(|C'|)),(blocks (p # ps', Ts, vs, e)),(h,l)⟩ => ⟨e',(h', l')⟩" by fact
  moreover
  { fix a Cs Cs'
    assume blocks:"P,E \<turnstile> ⟨blocks(p#ps',Ts,vs,e),(h,l)⟩ => ⟨ref (a,Cs),(h',l')⟩"
      and path_via:"P \<turnstile> 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' [\<mapsto>] Ts) \<turnstile> ⟨e,(h,l(p#ps'[\<mapsto>]vs''))⟩ => 
                                 ⟨ref (a,Cs),(h',l'')⟩"
      and casts:"P \<turnstile> Ts Casts vs to vs''"
      and length:"length vs'' = length vs"
      by -(drule blocksEval,auto)
    from eval path_via have 
      "P,E(p#ps'[\<mapsto>]Ts) \<turnstile> ⟨(|C'|)),e,(h,l(p#ps'[\<mapsto>]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 \<turnstile> ⟨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' [\<mapsto>] Ts) \<turnstile> ⟨e,(h,l(p#ps'[\<mapsto>]vs''))⟩ => 
                                 ⟨ref (a,Cs@C'# Cs'),(h',l'')⟩"
      and casts:"P \<turnstile> Ts Casts vs to vs''"
      and length:"length vs'' = length vs"
      by -(drule blocksEval,auto)
    from eval have "P,E(p#ps'[\<mapsto>]Ts) \<turnstile> ⟨(|C'|)),e,(h,l(p#ps'[\<mapsto>]vs''))⟩ => 
                                             ⟨ref(a,Cs@[C']),(h',l'')⟩"
      by(auto intro:StaticDownCast)
    with e' casts length have ?case by simp blast }
  moreover
  { assume "P,E \<turnstile> ⟨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' [\<mapsto>] Ts) \<turnstile> ⟨e,(h,l(p#ps'[\<mapsto>]vs''))⟩ => 
                                 ⟨null,(h',l'')⟩"
      and casts:"P \<turnstile> Ts Casts vs to vs''"
      and length:"length vs'' = length vs"
      by -(drule blocksEval,auto)
    from eval have "P,E(p#ps' [\<mapsto>] Ts) \<turnstile> ⟨(|C'|)),e,(h,l(p#ps'[\<mapsto>]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 \<turnstile> ⟨blocks(p#ps',Ts,vs,e),(h,l)⟩ => ⟨ref (a,Cs),(h',l')⟩"
      and notin:"C' ∉ set Cs" and leq:"¬ P \<turnstile> (last Cs) \<preceq>* C'"
      and  e':"e' = THROW ClassCast"
    from blocks length_eqs obtain l'' vs''
      where eval:"P,E(p#ps' [\<mapsto>] Ts) \<turnstile> ⟨e,(h,l(p#ps'[\<mapsto>]vs''))⟩ => 
                                 ⟨ref (a,Cs),(h',l'')⟩"
      and casts:"P \<turnstile> Ts Casts vs to vs''"
      and length:"length vs'' = length vs"
      by -(drule blocksEval,auto)
    from eval notin leq have 
      "P,E(p#ps'[\<mapsto>]Ts) \<turnstile> ⟨(|C'|)),e,(h,l(p#ps'[\<mapsto>]vs''))⟩ => 
                          ⟨THROW ClassCast,(h',l'')⟩"
      by(auto intro:StaticCastFail)
    with e' casts length have ?case by simp blast }
  moreover
  { fix r assume "P,E \<turnstile> ⟨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' [\<mapsto>] Ts) \<turnstile> ⟨e,(h,l(p#ps'[\<mapsto>]vs''))⟩ => 
                                 ⟨throw r,(h',l'')⟩"
      and casts:"P \<turnstile> Ts Casts vs to vs''"
      and length:"length vs'' = length vs"
      by -(drule blocksEval,auto)
    from eval have 
      "P,E(p#ps'[\<mapsto>]Ts) \<turnstile> ⟨(|C'|)),e,(h,l(p#ps'[\<mapsto>]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,fastsimp+)
qed



lemma
assumes wf: "wwf_prog P"
shows eval_restrict_lcl:
  "P,E \<turnstile> ⟨e,(h,l)⟩ => ⟨e',(h',l')⟩ ==> (!!W. fv e ⊆ W ==> P,E \<turnstile> ⟨e,(h,l|`W)⟩ => ⟨e',(h',l'|`W)⟩)"
and "P,E \<turnstile> ⟨es,(h,l)⟩ [=>] ⟨es',(h',l')⟩ ==> (!!W. fvs es ⊆ W ==> P,E \<turnstile> ⟨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 \<mapsto> T) \<turnstile> ⟨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 \<mapsto> T) \<turnstile> ⟨e0,(h0, (l0|`W)(V := None))⟩ => ⟨e1,(h1, l1|`insert V W)⟩"
    by fastsimp
  from eval_evals.Block[OF this] show ?case by fastsimp
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 \<turnstile> ⟨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 \<turnstile> ⟨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 \<turnstile> ⟨e,(h0,l0|`W)⟩ => ⟨Val v,(h,l|`W)⟩"
    and env:"E V = ⌊T⌋" and casts:"P \<turnstile> T casts v to v'"
    and [simp]: "l' = l(V \<mapsto> 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 fastsimp
next
  case LAssThrow thus ?case by(fastsimp intro: eval_evals.LAssThrow)
next
  case FAcc thus ?case by simp (blast intro: eval_evals.FAcc)
next
  case FAccNull thus ?case by(fastsimp intro: eval_evals.FAccNull)
next
  case FAccThrow thus ?case by(fastsimp 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 \<turnstile> ⟨e1,(h, l|`W)⟩ => ⟨ref (a, Cs'),(h', l'|`W)⟩"
    and IH2: "!!W. fv e2 ⊆ W ==> P,E \<turnstile> ⟨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 \<mapsto> v')"
    and S':"S' = S - {(Ds, fs)} ∪ {(Ds, fs')}" 
    and h':"h2' = h2(a \<mapsto> (D, S'))" 
    and field:"P \<turnstile> last Cs' has least F:T via Cs"
    and casts:"P \<turnstile> 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 \<turnstile> ⟨e,(h0,l0|`W)⟩ => ⟨ref(a,Cs),(h1,l1|`W)⟩"
    and IHps: "!!W. fvs ps ⊆ W ==> P,E \<turnstile> ⟨ps,(h1,l1|`W)⟩ [=>] ⟨map Val vs,(h2,l2|`W)⟩"
    and IHbd: "!!W. fv new_body ⊆ W ==> P,E(this \<mapsto> Class (last Cs'), pns [\<mapsto>] Ts) \<turnstile> 
                                    ⟨new_body,(h2,l2'|`W)⟩ => ⟨e',(h3,l3|`W)⟩"
    and h2a: "h2 a = Some (C,S)"
    and method: "P \<turnstile> last Cs has least M = (Ts',T',pns',body') via Ds"
    and select:"P \<turnstile> (C,Cs@pDs) selects M = (Ts,T,pns,body) via Cs'"
    and same_len: "size vs = size pns"
    and casts:"P \<turnstile> Ts Casts vs to vs'"
    and l2': "l2' = [this \<mapsto> Ref(a,Cs'), pns [\<mapsto>] 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(fastsimp 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 \<mapsto> Ref (a, Cs'), pns [\<mapsto>] 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 \<turnstile> ⟨e,(h0,l0|`W)⟩ => ⟨ref(a,Cs),(h1,l1|`W)⟩"
    and IHps: "!!W. fvs ps ⊆ W ==> P,E \<turnstile> ⟨ps,(h1,l1|`W)⟩ [=>] ⟨map Val vs,(h2,l2|`W)⟩"
    and IHbd: "!!W. fv body ⊆ W ==> P,E(this \<mapsto> Class (last Ds), pns [\<mapsto>] Ts) \<turnstile> 
                                    ⟨body,(h2,l2'|`W)⟩ => ⟨e',(h3,l3|`W)⟩"
    and path_unique: "P \<turnstile> Path last Cs to C unique"
    and path_via: "P \<turnstile> Path last Cs to C via Cs''"
    and least: "P \<turnstile> 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 \<turnstile> Ts Casts vs to vs'"
    and l2': "l2' = [this \<mapsto> Ref(a,Ds), pns [\<mapsto>] 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(fastsimp 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 \<mapsto> Ref(a,Ds), pns [\<mapsto>] 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 \<turnstile> ⟨e,(h,l)⟩ => ⟨e',(h',l')⟩ ==> (!!V. V ∉ fv e ==> l' V = l V)"
and "P,E \<turnstile> ⟨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) fastsimp
qed simp_all



lemma eval_closed_lcl_unchanged:
  assumes wf:"wwf_prog P"
  and eval:"P,E \<turnstile> ⟨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:expand_fun_eq)
qed



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

declare split_paired_All [simp del] split_paired_Ex [simp del]

declaration {* K (Simplifier.map_ss (fn ss => ss delloop "split_all_tac")) *}
declaration {* K (Classical.map_cs (fn cs => cs delSWrapper "split_all_tac")) *}


lemma list_eval_Throw: 
assumes eval_e: "P,E \<turnstile> ⟨throw x,s⟩ => ⟨e',s'⟩"
shows "P,E \<turnstile> ⟨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 \<turnstile> ⟨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 \<turnstile> ⟨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 \<turnstile> ⟨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 \<turnstile> ⟨e,s⟩ => ⟨Val v,s⟩"
          by (iprover intro: eval_evals.Val)
        moreover from es 
        have "P,E \<turnstile> ⟨es,s⟩ [=>] ⟨map Val vs' @ e' # es',s'⟩"
          by (rule Cons.hyps)
        ultimately show 
          "P,E \<turnstile> ⟨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 \<turnstile> ⟨e,s⟩ -> ⟨e'',s''⟩ ==>  (!!s' e'. P,E \<turnstile> ⟨e'',s''⟩ => ⟨e',s'⟩ ==> P,E \<turnstile> ⟨e,s⟩ => ⟨e',s'⟩)"
and extend_1_evals:
  "P,E \<turnstile> ⟨es,t⟩ [->] ⟨es'',t''⟩ ==> (!!t' es'. P,E \<turnstile> ⟨es'',t''⟩ [=>] ⟨es',t'⟩ ==> P,E \<turnstile> ⟨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 (fastsimp 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 \<turnstile> ⟨e'',s''⟩ => ⟨ref(a,Cs@[C]@Cs'),s'⟩",
         rule_tac Cs'="Cs'" in StaticDownCast,auto)
next
  case RedStaticCastNull thus ?case
    by (fastsimp elim: eval_cases intro: eval_evals.intros)
next
  case RedStaticUpCast thus ?case
    by (fastsimp elim: eval_cases intro: eval_evals.intros)
next
  case RedStaticDownCast thus ?case
    by (fastsimp elim: eval_cases intro: eval_evals.intros)
next
  case RedStaticCastFail thus ?case
    by (fastsimp elim: eval_cases intro: eval_evals.intros)
next
  case RedStaticUpDynCast thus ?case
    by (fastsimp elim: eval_cases intro: eval_evals.intros)
next
  case RedStaticDownDynCast thus ?case
    by (fastsimp elim: eval_cases intro: eval_evals.intros)
next
  case (DynCastRed E e s e'' s'' C s' e')
  have eval:"P,E \<turnstile> ⟨Cast C e'',s''⟩ => ⟨e',s'⟩"
    and IH:"!!ex sx. P,E \<turnstile> ⟨e'',s''⟩ => ⟨ex,sx⟩ ==> P,E \<turnstile> ⟨e,s⟩ => ⟨ex,sx⟩" by fact+
  moreover 
  { fix Cs Cs' a
    assume "P,E \<turnstile> ⟨e'',s''⟩ => ⟨ref (a, Cs @ C # Cs'),s'⟩"
    from IH[OF this] have "P,E \<turnstile> ⟨e,s⟩ => ⟨ref (a, Cs@[C]@Cs'),s'⟩" by simp
    hence "P,E \<turnstile> ⟨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 (fastsimp 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)(fastsimp 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 (fastsimp 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)(fastsimp elim:eval_cases intro:eval_evals.intros)
next
  case RedFAccNull thus ?case by (fastsimp elim!:eval_cases intro:eval_evals.intros)
next
  case (FAssRed1 E e1 s e1' s'' F Cs e2 s' e')
  have eval:"P,E \<turnstile> ⟨e1'•F{Cs} := e2,s''⟩ => ⟨e',s'⟩"
    and IH:"!!ex sx. P,E \<turnstile> ⟨e1',s''⟩ => ⟨ex,sx⟩ ==> P,E \<turnstile> ⟨e1,s⟩ => ⟨ex,sx⟩" by fact+
  { fix Cs' D S T a fs h2 l2 s1 v v'
    assume ref:"P,E \<turnstile> ⟨e1',s''⟩ => ⟨ref (a, Cs'),s1⟩" 
      and rest:"P,E \<turnstile> ⟨e2,s1⟩ => ⟨Val v,(h2, l2)⟩" "h2 a = ⌊(D, S)⌋" 
      "P \<turnstile> last Cs' has least F:T via Cs" "P \<turnstile> T casts v to v'"
      "(Cs' @p Cs, fs) ∈ S"
    from IH[OF ref] have "P,E \<turnstile> ⟨e1,s⟩ => ⟨ref (a, Cs'),s1⟩" .
    with rest have "P,E \<turnstile> ⟨e1•F{Cs} := e2,s⟩ =>
          ⟨Val v',(h2(a \<mapsto> (D,insert (Cs'@pCs,fs(F \<mapsto> v'))(S - {(Cs'@pCs,fs)}))),l2)⟩"
      by-(rule FAss,simp_all) }
  moreover
  { fix s1 v 
    assume null:"P,E \<turnstile> ⟨e1',s''⟩ => ⟨null,s1⟩" 
      and rest:"P,E \<turnstile> ⟨e2,s1⟩ => ⟨Val v,s'⟩"
    from IH[OF null] have "P,E \<turnstile> ⟨e1,s⟩ => ⟨null,s1⟩" .
    with rest have "P,E \<turnstile> ⟨e1•F{Cs} := e2,s⟩ => ⟨THROW NullPointer,s'⟩"
      by-(rule FAssNull,simp_all) }
  moreover
  { fix e' assume throw:"P,E \<turnstile> ⟨e1',s''⟩ => ⟨throw e',s'⟩"
    from IH[OF throw] have "P,E \<turnstile> ⟨e1,s⟩ => ⟨throw e',s'⟩" .
    hence "P,E \<turnstile> ⟨e1•F{Cs} := e2,s⟩ => ⟨throw e',s'⟩"
      by-(rule eval_evals.FAssThrow1,simp_all) }
  moreover
  { fix e' s1 v
    assume val:"P,E \<turnstile> ⟨e1',s''⟩ => ⟨Val v,s1⟩"
      and rest:"P,E \<turnstile> ⟨e2,s1⟩ => ⟨throw e',s'⟩"
    from IH[OF val] have "P,E \<turnstile> ⟨e1,s⟩ => ⟨Val v,s1⟩" .
    with rest have "P,E \<turnstile> ⟨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 \<turnstile> ⟨Val v•F{Cs} := e2',s''⟩ => ⟨e',s'⟩"
    and IH:"!!ex sx. P,E \<turnstile> ⟨e2',s''⟩ => ⟨ex,sx⟩ ==> P,E \<turnstile> ⟨e2,s⟩ => ⟨ex,sx⟩" by fact+
  { fix Cs' D S T a fs h2 l2 s1 v' v''
    assume val1:"P,E \<turnstile> ⟨Val v,s''⟩ => ⟨ref (a,Cs'),s1⟩"
      and val2:"P,E \<turnstile> ⟨e2',s1⟩ => ⟨Val v',(h2, l2)⟩"
      and rest:"h2 a = ⌊(D, S)⌋" "P \<turnstile> last Cs' has least F:T via Cs"
               "P \<turnstile> T casts v' to v''" "(Cs'@pCs,fs) ∈ S"
    from val1 have s'':"s1 = s''" by -(erule eval_cases)
    with val1 have "P,E \<turnstile> ⟨Val v,s⟩ => ⟨ref (a,Cs'),s⟩"
      by(fastsimp elim:eval_cases intro:eval_finalId)
    also from IH[OF val2[simplified s'']] have "P,E \<turnstile> ⟨e2,s⟩ => ⟨Val v',(h2, l2)⟩" .
    ultimately have "P,E \<turnstile> ⟨Val v•F{Cs} := e2,s⟩ =>
           ⟨Val v'',(h2(a\<mapsto>(D,insert(Cs'@pCs,fs(F \<mapsto> v''))(S - {(Cs'@pCs,fs)}))),l2)⟩"
      using rest by -(rule FAss,simp_all) }
  moreover
  { fix s1 v'
    assume val1:"P,E \<turnstile> ⟨Val v,s''⟩ => ⟨null,s1⟩"
      and val2:"P,E \<turnstile> ⟨e2',s1⟩ => ⟨Val v',s'⟩"
    from val1 have s'':"s1 = s''" by -(erule eval_cases)
    with val1 have "P,E \<turnstile> ⟨Val v,s⟩ => ⟨null,s⟩"
      by(fastsimp elim:eval_cases intro:eval_finalId)
    also from IH[OF val2[simplified s'']] have "P,E \<turnstile> ⟨e2,s⟩ => ⟨Val v',s'⟩" .
    ultimately have "P,E \<turnstile> ⟨Val v•F{Cs} := e2,s⟩ => ⟨THROW NullPointer,s'⟩"
      by -(rule FAssNull,simp_all) }
  moreover
  { fix r assume val:"P,E \<turnstile> ⟨Val v,s''⟩ => ⟨throw r,s'⟩"
    hence s'':"s'' = s'" by -(erule eval_cases,simp)
    with val have "P,E \<turnstile> ⟨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 \<turnstile> ⟨Val v,s''⟩ => ⟨Val v',s1⟩"
      and val2:"P,E \<turnstile> ⟨e2',s1⟩ => ⟨throw r,s'⟩"
    from val1 have s'':"s1 = s''" by -(erule eval_cases)
    with val1 have "P,E \<turnstile> ⟨Val v,s⟩ => ⟨Val v',s⟩"
      by(fastsimp elim:eval_cases intro:eval_finalId)
    also from IH[OF val2[simplified s'']] have "P,E \<turnstile> ⟨e2,s⟩ => ⟨throw r,s'⟩" .
    ultimately have "P,E \<turnstile> ⟨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 \<turnstile> ⟨Val v',(h(a \<mapsto> (D,insert (Ds,fs(F \<mapsto> v'))(S - {(Ds,fs)}))),l)⟩ => 
                  ⟨e',s'⟩"
    and rest:"h a = ⌊(D, S)⌋" "P \<turnstile> last Cs' has least F:T via Cs"
             "P \<turnstile> T casts v to v'" "Ds = Cs' @p Cs" "(Ds, fs) ∈ S" by fact+
  from val have "s' = (h(a \<mapsto> (D,insert (Ds,fs(F \<mapsto> 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 (fastsimp 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 \<turnstile> ⟨Call (Val v) Copt M es',s''⟩ => ⟨e',s'⟩"
    and IH:"!!esx sx. P,E \<turnstile> ⟨es',s''⟩ [=>] ⟨esx,sx⟩ ==> P,E \<turnstile> ⟨es,s⟩ [=>] ⟨esx,sx⟩" by fact+
  show ?case
    proof(cases Copt)
    case None with call have eval:"P,E \<turnstile> ⟨Val v•M(es'),s''⟩ => ⟨e',s'⟩" by simp
    from eval show ?thesis
    proof(rule eval_cases)
      fix r assume "P,E \<turnstile> ⟨Val v,s''⟩ => ⟨throw r,s'⟩" "e' = throw r"
      with None show "P,E \<turnstile> ⟨Call (Val v) Copt M es,s⟩ => ⟨e',s'⟩"
        by(fastsimp elim:eval_cases)
    next
      fix es'' r sx v' vs
      assume val:"P,E \<turnstile> ⟨Val v,s''⟩ => ⟨Val v',sx⟩"
        and evals:"P,E \<turnstile> ⟨es',sx⟩ [=>] ⟨map Val vs @ throw r # es'',s'⟩"
        and e':"e' = throw r"
      have val':"P,E \<turnstile> ⟨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 \<turnstile> ⟨es,s⟩ [=>] ⟨map Val vs @ throw r # es'',s'⟩"
        by simp
      with eq CallParamsThrow[OF val'] e' None
      show "P,E \<turnstile> ⟨Call (Val v) Copt M es,s⟩ => ⟨e',s'⟩"
        by fastsimp
    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 \<turnstile> ⟨Val v,s''⟩ => ⟨ref(a,Cs),s1⟩"
        and evals:"P,E \<turnstile> ⟨es',s1⟩ [=>] ⟨map Val vs,(h2,l2)⟩"
        and hp:"h2 a = Some(C, S)"
        and method:"P \<turnstile> last Cs has least M = (Ts',T',pns',body') via Ds"
        and select:"P \<turnstile> (C,Cs@pDs) selects M = (Ts,T,pns,body) via Cs'"
        and length:"length vs = length pns"
        and casts:"P \<turnstile> Ts Casts vs to vs'"
        and body:"P,E(this \<mapsto> Class (last Cs'), pns [\<mapsto>] Ts) \<turnstile> 
    ⟨case T' of Class D => (|D|)),body | _ => body,(h2,[this \<mapsto> Ref(a,Cs'),pns [\<mapsto>] vs'])⟩
        => ⟨e',(h3, l3)⟩"
        and s':"s' = (h3, l2)"
      from val have val':"P,E \<turnstile> ⟨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 \<mapsto> Class (last Cs'), pns [\<mapsto>] Ts) \<turnstile> 
        ⟨new_body,(h2,[this \<mapsto> Ref(a,Cs'),pns [\<mapsto>] vs'])⟩ => ⟨e',(h3, l3)⟩"
        by simp
      from eq IH evals have "P,E \<turnstile> ⟨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 \<turnstile> ⟨Call (Val v) Copt M es,s⟩ => ⟨e',s'⟩" by fastsimp
    next
      fix s1 vs
      assume val:"P,E \<turnstile> ⟨Val v,s''⟩ => ⟨null,s1⟩"
        and evals:"P,E \<turnstile> ⟨es',s1⟩ [=>] ⟨map Val vs,s'⟩"
        and e':"e' = THROW NullPointer"
      from val have val':"P,E \<turnstile> ⟨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 \<turnstile> ⟨es,s⟩ [=>] ⟨map Val vs,s'⟩" by simp
      with eq CallNull[OF val'] e' None
      show "P,E \<turnstile> ⟨Call (Val v) Copt M es,s⟩ => ⟨e',s'⟩" by fastsimp
    qed
  next
    case (Some C) with call have eval:"P,E \<turnstile> ⟨Val v•(C::)M(es'),s''⟩ => ⟨e',s'⟩"
      by simp
    from eval show ?thesis
    proof(rule eval_cases)
      fix r assume "P,E \<turnstile> ⟨Val v,s''⟩ => ⟨throw r,s'⟩" "e' = throw r"
      with Some show "P,E \<turnstile> ⟨Call (Val v) Copt M es,s⟩ => ⟨e',s'⟩"
        by(fastsimp elim:eval_cases)
    next
      fix es'' r sx v' vs
      assume val:"P,E \<turnstile> ⟨Val v,s''⟩ => ⟨Val v',sx⟩"
        and evals:"P,E \<turnstile> ⟨es',sx⟩ [=>] ⟨map Val vs @ throw r # es'',s'⟩"
        and e':"e' = throw r"
      have val':"P,E \<turnstile> ⟨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 \<turnstile> ⟨es,s⟩ [=>] ⟨map Val vs @ throw r # es'',s'⟩"
        by simp
      with eq CallParamsThrow[OF val'] e' Some
      show "P,E \<turnstile> ⟨Call (Val v) Copt M es,s⟩ => ⟨e',s'⟩"
        by fastsimp
    next
      fix Cs Cs' Cs'' T Ts a body h2 h3 l2 l3 pns s1 vs vs'
      assume val:"P,E \<turnstile> ⟨Val v,s''⟩ => ⟨ref (a,Cs),s1⟩"
        and evals:"P,E \<turnstile> ⟨es',s1⟩ [=>] ⟨map Val vs,(h2,l2)⟩"
        and path_unique:"P \<turnstile> Path last Cs to C unique"
        and path_via:"P \<turnstile> Path last Cs to C via Cs''"
        and least:"P \<turnstile> C has least M = (Ts, T, pns, body) via Cs'"
        and length:"length vs = length pns"
        and casts:"P \<turnstile> Ts Casts vs to vs'"
        and body:"P,E(this \<mapsto> Class (last ((Cs @p Cs'') @p Cs')), pns [\<mapsto>] Ts) \<turnstile> 
           ⟨body,(h2,[this \<mapsto> Ref(a,(Cs@pCs'')@pCs'),pns [\<mapsto>] vs'])⟩ => ⟨e',(h3,l3)⟩"
        and s':"s' = (h3,l2)"
      from val have val':"P,E \<turnstile> ⟨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 \<turnstile> ⟨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 \<turnstile> ⟨Call (Val v) Copt M es,s⟩ => ⟨e',s'⟩" by fastsimp
    next
      fix s1 vs
      assume val:"P,E \<turnstile> ⟨Val v,s''⟩ => ⟨null,s1⟩"
        and evals:"P,E \<turnstile> ⟨es',s1⟩ [=>] ⟨map Val vs,s'⟩"
        and e':"e' = THROW NullPointer"
      from val have val':"P,E \<turnstile> ⟨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 \<turnstile> ⟨es,s⟩ [=>] ⟨map Val vs,s'⟩" by simp
      with eq CallNull[OF val'] e' Some
      show "P,E \<turnstile> ⟨Call (Val v) Copt M es,s⟩ => ⟨e',s'⟩"
        by fastsimp
    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 \<turnstile> ⟨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 \<turnstile> ⟨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 \<turnstile> last Cs has least M = (Ts',T',pns',body') via Ds" by fact
  moreover have select:"P \<turnstile> (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 (fastsimp 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 \<turnstile> ⟨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 \<turnstile> ⟨new_body,(h2,l2)⟩ => ⟨e',(h3,l3)⟩" using s s' by simp
  have casts_unique:"!!vs'. P \<turnstile> 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\<mapsto>Class(last Cs'), pns[\<mapsto>]Ts) \<turnstile> 
              ⟨new_body',(h2,l2(this # pns[\<mapsto>]Ref(a,Cs')#vs'))⟩ => ⟨e',(h3, l'')⟩ ∧ 
     P \<turnstile> 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\<mapsto>Class(last Cs'), pns[\<mapsto>]Ts) \<turnstile> 
                    ⟨body,(h2,l2(this # pns[\<mapsto>]Ref(a,Cs')#vs'))⟩ => ⟨e',(h3, l'')⟩"
      and casts:"P \<turnstile> 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\<mapsto>Class(last Cs'), pns[\<mapsto>]Ts) \<turnstile> 
                    ⟨(|D|)),body,(h2,l2(this # pns[\<mapsto>]Ref(a,Cs')#vs'))⟩ => 
                    ⟨e',(h3, l'')⟩"
      and casts:"P \<turnstile> 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\<mapsto>Class(last Cs'), pns[\<mapsto>]Ts) \<turnstile> 
               ⟨new_body',(h2,l2(this # pns[\<mapsto>]Ref(a,Cs')#vs'))⟩ => ⟨e',(h3, l'')⟩"
    and casts:"P \<turnstile> 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[\<mapsto>]Ref(a,Cs')#vs')|`(set(this#pns)) = 
          [this # pns[\<mapsto>]Ref(a,Cs')#vs']" by simp
  with eval_restrict_lcl[OF wf body fv'] this_distinct same_len1 same_len
  have "P,E(this\<mapsto>Class(last Cs'), pns[\<mapsto>]Ts) \<turnstile> 
   ⟨new_body',(h2,[this # pns[\<mapsto>]Ref(a,Cs')#vs'])⟩ => ⟨e',(h3, l''|`(set(this#pns)))⟩"
    by simp
  with casts obtain l2' l3' vs' where
        "P \<turnstile> Ts Casts vs to vs'"
    and "P,E(this\<mapsto>Class(last Cs'), pns[\<mapsto>]Ts) \<turnstile> 
                                      ⟨new_body',(h2,l2')⟩ => ⟨e',(h3,l3')⟩"
    and "l2' = [this\<mapsto>Ref(a,Cs'),pns[\<mapsto>]vs']"
    by(auto elim:Casts_to.cases)
  ultimately have "P,E \<turnstile> ⟨(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 \<turnstile> ⟨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 \<turnstile> ⟨map Val vs,s⟩ [=>] ⟨map Val vs,(h2,l2)⟩"
    by (iprover intro: eval_finalsId)
  moreover have path_unique:"P \<turnstile> Path last Cs to C unique" by fact
  moreover have path_via:"P \<turnstile> Path last Cs to C via Cs''" by fact
  moreover have least:"P \<turnstile> 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 (fastsimp 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 \<turnstile> ⟨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 \<turnstile> ⟨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 \<turnstile> 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\<mapsto>Class(last Ds), pns[\<mapsto>]Ts) \<turnstile> 
               ⟨body,(h2,l2(this # pns[\<mapsto>]Ref(a,Ds)#vs'))⟩ => ⟨e',(h3, l'')⟩"
    and casts:"P \<turnstile> 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[\<mapsto>]Ref(a,Ds)#vs')|`(set(this#pns)) = 
          [this # pns[\<mapsto>]Ref(a,Ds)#vs']" by simp
  with eval_restrict_lcl[OF wf body fv] this_distinct same_len1 same_len
  have "P,E(this\<mapsto>Class(last Ds), pns[\<mapsto>]Ts) \<turnstile> 
   ⟨body,(h2,[this#pns [\<mapsto>] Ref(a,Ds)#vs'])⟩ => ⟨e',(h3, l''|`(set(this#pns)))⟩"
    by simp
  with casts obtain l2' l3' vs' where
        "P \<turnstile> Ts Casts vs to vs'"
    and "P,E(this \<mapsto> Class(last Ds),pns [\<mapsto>] Ts) \<turnstile> ⟨body,(h2,l2')⟩ => ⟨e',(h3,l3')⟩"
    and "l2' = [this \<mapsto> Ref(a,Ds),pns [\<mapsto>] vs']"
    by(auto elim:Casts_to.cases)
  ultimately have "P,E \<turnstile> ⟨(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 (fastsimp elim: eval_cases intro: eval_evals.intros eval_finalsId)
next
  case BlockRedNone
  thus ?case
    by (fastsimp 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 \<turnstile> ⟨{V:T:=Val v; e''},(h', l'(V := l V))⟩ => ⟨e',s'⟩"
    and red:"P,E(V \<mapsto> T) \<turnstile> ⟨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 \<mapsto> T) \<turnstile> ⟨e'',(h', l')⟩ => ⟨ex,sx⟩ ==>
                     P,E(V \<mapsto> T) \<turnstile> ⟨e,(h, l(V := None))⟩ => ⟨ex,sx⟩" by fact+
  from l' have l'upd:"l'(V \<mapsto> v) = l'" by (rule map_upd_triv)
  from wf red l' have casts:"P \<turnstile> 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 \<mapsto> T) \<turnstile> ⟨V:=Val v;; e'',(h',l'(V:=None))⟩ => ⟨e',(h'',l'')⟩ ∧ 
    s' = (h'',l''(V:=l V))"
    by (fastsimp elim:eval_cases simp:fun_upd_same fun_upd_idem)
  moreover
  { fix T' h0 l0 v' v''
    assume eval':"P,E(V \<mapsto> T) \<turnstile> ⟨e'',(h0,l0(V \<mapsto> v''))⟩ => ⟨e',(h'', l'')⟩"
      and val:"P,E(V \<mapsto> T) \<turnstile> ⟨Val v,(h', l'(V := None))⟩ => ⟨Val v',(h0,l0)⟩"
      and env:"(E(V \<mapsto> T)) V = Some T'" and casts':"P \<turnstile> 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 \<mapsto> T) \<turnstile> ⟨e'',(h', l'(V \<mapsto> v))⟩ => ⟨e',(h'', l'')⟩"
      by clarsimp }
  ultimately have "P,E(V \<mapsto> T) \<turnstile> ⟨e'',(h',l'(V \<mapsto> 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 \<mapsto> T) \<turnstile> ⟨e'',(h',l')⟩ => ⟨e',(h'',l'')⟩"
    by simp
  from IH[OF eval''] have "P,E(V \<mapsto> T) \<turnstile> ⟨e,(h, l(V := None))⟩ => ⟨e',(h'', l'')⟩" .
  with s' show ?case by(fastsimp intro:Block)
next
  case (InitBlockRed E V T e h l v' e'' h' l' v'' v s' e')
  have eval:" P,E \<turnstile> ⟨{V:T:=Val v''; e''},(h', l'(V := l V))⟩ => ⟨e',s'⟩"
    and red:"P,E(V \<mapsto> T) \<turnstile> ⟨e,(h, l(V \<mapsto> v'))⟩ -> ⟨e'',(h', l')⟩"
    and casts:"P \<turnstile> T casts v to v'" and l':"l' V = Some v''"
    and IH:"!!ex sx. P,E(V \<mapsto> T) \<turnstile> ⟨e'',(h', l')⟩ => ⟨ex,sx⟩ ==>
                     P,E(V \<mapsto> T) \<turnstile> ⟨e,(h, l(V \<mapsto> v'))⟩ => ⟨ex,sx⟩" by fact+
  from l' have l'upd:"l'(V \<mapsto> v'') = l'" by (rule map_upd_triv)
  from wf casts have "P \<turnstile> T casts v' to v'" by(rule casts_casts)
  with wf red l' have casts':"P \<turnstile> 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 \<mapsto> T) \<turnstile> ⟨V:=Val v'';; e'',(h',l'(V:=None))⟩ => ⟨e',(h'',l'')⟩ ∧ 
    s' = (h'',l''(V:=l V))"
    by (fastsimp elim:eval_cases simp:fun_upd_same fun_upd_idem)
  moreover
  { fix T' v'''
    assume eval':"P,E(V \<mapsto> T) \<turnstile> ⟨e'',(h',l'(V \<mapsto> v'''))⟩ => ⟨e',(h'', l'')⟩"
      and env:"(E(V \<mapsto> T)) V = Some T'" and casts'':"P \<turnstile> 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 \<mapsto> T) \<turnstile> ⟨e'',(h', l'(V \<mapsto> v''))⟩ => ⟨e',(h'', l'')⟩" by simp }
  ultimately have "P,E(V \<mapsto> T) \<turnstile> ⟨e'',(h',l'(V \<mapsto> 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 \<mapsto> T) \<turnstile> ⟨e'',(h',l')⟩ => ⟨e',(h'',l'')⟩"
    by simp
  from IH[OF eval'']
  have evale:"P,E(V \<mapsto> T) \<turnstile> ⟨e,(h, l(V \<mapsto> v'))⟩ => ⟨e',(h'', l'')⟩" .
  from casts
  have "P,E(V \<mapsto> T) \<turnstile> ⟨V:=Val v,(h,l(V:=None))⟩ => ⟨Val v',(h,l(V \<mapsto> 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(fastsimp intro:Block Seq)
next
  case (RedBlock E V T v s s' e')
  have "P,E \<turnstile> ⟨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 \<mapsto> T) \<turnstile> ⟨Val v,(h,l(V:=None))⟩ => ⟨Val v,(h,l(V:=None))⟩" 
    by (rule eval_evals.intros)
  hence "P,E \<turnstile> ⟨{V:T;Val v},(h,l)⟩ => ⟨Val v,(h,(l(V:=None))(V:=l V))⟩"
    by (rule eval_evals.Block)
  thus "P,E \<turnstile> ⟨{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 \<turnstile> ⟨Val u,s⟩ => ⟨e',s'⟩" and casts:"P \<turnstile> 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 \<mapsto> T) \<turnstile> ⟨Val v,(h,l(V:=None))⟩ => ⟨Val v,(h,l(V:=None))⟩"
    by (rule eval_evals.intros)
  with casts
  have "P,E(V \<mapsto> T) \<turnstile> ⟨V:=Val v,(h,l(V:=None))⟩ => ⟨Val v',(h,l(V \<mapsto> v'))⟩"
    by -(rule_tac l="l(V:=None)" in LAss,auto simp:fun_upd_same)
  hence "P,E \<turnstile> ⟨{V:T :=Val v; Val u},(h,l)⟩ => ⟨Val u,(h, (l(V\<mapsto>v'))(V:=l V))⟩"
    by (fastsimp intro!: eval_evals.intros)
  thus ?case using s s' e' by simp
next
  case SeqRed thus ?case by (fastsimp elim: eval_cases intro: eval_evals.intros)
next
  case RedSeq thus ?case by (fastsimp elim: eval_cases intro: eval_evals.intros)
next
  case CondRed thus ?case by (fastsimp elim: eval_cases intro: eval_evals.intros)
next
  case RedCondT thus ?case by (fastsimp elim: eval_cases intro: eval_evals.intros)
next
  case RedCondF thus ?case by (fastsimp 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 (fastsimp 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 (fastsimp elim: evals_cases intro: eval_evals.intros)
next
  case ListRed2
  thus ?case by (fastsimp elim!: evals_cases eval_cases 
                          intro: eval_evals.intros eval_finalId)
next
  case StaticCastThrow
  thus ?case by (fastsimp elim: eval_cases intro: eval_evals.intros)
next
  case DynCastThrow
  thus ?case by (fastsimp elim: eval_cases intro: eval_evals.intros)
next
  case BinOpThrow1 thus ?case by (fastsimp elim: eval_cases intro: eval_evals.intros)
next
  case BinOpThrow2 thus ?case by (fastsimp elim: eval_cases intro: eval_evals.intros)
next
  case LAssThrow thus ?case by (fastsimp elim: eval_cases intro: eval_evals.intros)
next
  case FAccThrow thus ?case by (fastsimp elim: eval_cases intro: eval_evals.intros)
next
  case FAssThrow1 thus ?case by (fastsimp elim: eval_cases intro: eval_evals.intros)
next
  case FAssThrow2 thus ?case by (fastsimp elim: eval_cases intro: eval_evals.intros)
next
  case CallThrowObj thus ?case by (fastsimp elim: eval_cases intro: eval_evals.intros)
next
  case (CallThrowParams es vs r es' E v Copt M s s' e')
  have "P,E \<turnstile> ⟨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 \<turnstile> ⟨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 \<turnstile> ⟨es,s⟩ [=>] ⟨map Val vs @ Throw r # es',s'⟩" by simp
  ultimately have "P,E \<turnstile> ⟨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 \<turnstile> ⟨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 \<mapsto> T) \<turnstile> ⟨Throw r, (h,l(V:=None))⟩ => ⟨Throw r, (h,l(V:=None))⟩"
    by (simp add:eval_evals.intros eval_finalId)
  hence "P,E \<turnstile> ⟨{V:T;Throw r},(h,l)⟩ => ⟨Throw r, (h,(l(V:=None))(V:=l V))⟩"
    by (rule eval_evals.Block)
  thus "P,E \<turnstile> ⟨{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 \<turnstile> ⟨Throw r,s⟩ => ⟨e',s'⟩" and casts:"P \<turnstile> 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 \<mapsto> T) \<turnstile> ⟨Val v,(h,l(V:=None))⟩ => ⟨Val v,(h,l(V:=None))⟩"
    by (rule eval_evals.intros)
  with casts
  have "P,E(V \<mapsto> T) \<turnstile> ⟨V:=Val v,(h,l(V := None))⟩ => ⟨Val v',(h,l(V \<mapsto> v'))⟩"
    by -(rule_tac l="l(V:=None)" in LAss,auto simp:fun_upd_same)
  hence "P,E \<turnstile> ⟨{V:T := Val v; Throw r},(h,l)⟩ => ⟨Throw r, (h, (l(V\<mapsto>v'))(V:=l V))⟩"
    by(fastsimp intro:eval_evals.intros)
  thus "P,E \<turnstile> ⟨{V:T := Val v; Throw r},s⟩ => ⟨e',s'⟩" using s s' e' by simp
next
  case SeqThrow thus ?case by (fastsimp elim: eval_cases intro: eval_evals.intros)
next
  case CondThrow thus ?case by (fastsimp elim: eval_cases intro: eval_evals.intros)
next
  case ThrowThrow thus ?case by (fastsimp elim: eval_cases intro: eval_evals.intros)
qed


(* ... und wieder anschalten: *)
declare split_paired_All [simp] split_paired_Ex [simp]
declaration {* K (Classical.map_cs (fn cs => cs addSbefore ("split_all_tac", split_all_tac))) *}
declaration {* K (Simplifier.map_ss (fn ss => ss addloop ("split_all_tac", split_all_tac))) *}


text {* Its extension to @{text"->*"}: *} 

lemma extend_eval:
assumes wf: "wwf_prog P"
and reds: "P,E \<turnstile> ⟨e,s⟩ ->* ⟨e'',s''⟩" and eval_rest:  "P,E \<turnstile> ⟨e'',s''⟩ => ⟨e',s'⟩"
shows "P,E \<turnstile> ⟨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 \<turnstile> ⟨es,s⟩ [->]* ⟨es'',s''⟩" and eval_rest:  "P,E \<turnstile> ⟨es'',s''⟩ [=>] ⟨es',s'⟩"
shows "P,E \<turnstile> ⟨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 \<turnstile> ⟨e,s⟩ ->* ⟨e',s'⟩; final e'|] ==> P,E \<turnstile> ⟨e,s⟩ => ⟨e',s'⟩"
and "[|P,E \<turnstile> ⟨es,s⟩ [->]* ⟨es',s'⟩; finals es'|] ==> P,E \<turnstile> ⟨es,s⟩ [=>] ⟨es',s'⟩"

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


section {*Equivalence*}

text{* And now, the crowning achievement: *}

corollary big_iff_small:
  "wwf_prog P ==>
  P,E \<turnstile> ⟨e,s⟩ => ⟨e',s'⟩  =  (P,E \<turnstile> ⟨e,s⟩ ->* ⟨e',s'⟩ ∧ final e')"
by(blast dest: big_by_small eval_final small_by_big)


end