Theory Equivalence

(*  Title:       CoreC++

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

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

section ‹Equivalence of Big Step and Small Step Semantics›

theory Equivalence imports BigStep SmallStep WWellForm begin


subsection‹Some casts-lemmas›

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

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



lemma casts_casts_eq:
"⟦ P ⊢ T casts v to v; P ⊢ T casts v to v'; wf_prog wf_md P ⟧ ⟹ v = v'"

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



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

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



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

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

  


subsection‹Small steps simulate big step›

subsection ‹Cast›

lemma StaticCastReds:
  "P,E ⊢ ⟨e,s⟩ →* ⟨e',s'⟩ ⟹ P,E ⊢ ⟨⦇C⦈e,s⟩ →* ⟨⦇C⦈e',s'⟩"

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


lemma StaticCastRedsNull:
  "P,E ⊢ ⟨e,s⟩ →* ⟨null,s'⟩ ⟹ P,E ⊢ ⟨⦇C⦈e,s⟩ →* ⟨null,s'⟩"

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


lemma StaticUpCastReds:
  "⟦ P,E ⊢ ⟨e,s⟩ →* ⟨ref(a,Cs),s'⟩; P ⊢ Path last Cs to C via Cs'; Ds = Cs@⇩pCs' ⟧ 
  ⟹ P,E ⊢ ⟨⦇C⦈e,s⟩ →* ⟨ref(a,Ds),s'⟩"

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


lemma StaticDownCastReds:
  "P,E ⊢ ⟨e,s⟩ →* ⟨ref(a,Cs@[C]@Cs'),s'⟩
  ⟹  P,E ⊢ ⟨⦇C⦈e,s⟩ →* ⟨ref(a,Cs@[C]),s'⟩"

apply(rule rtrancl_into_rtrancl)
 apply(erule StaticCastReds)
apply simp
apply(subgoal_tac "P,E ⊢ ⟨⦇C⦈ref(a,Cs@[C]@Cs'),s'⟩ → ⟨ref(a,Cs@[C]),s'⟩")
 apply simp
apply(rule RedStaticDownCast)
done


lemma StaticCastRedsFail:
  "⟦ P,E ⊢ ⟨e,s⟩ →* ⟨ref(a,Cs),s'⟩; C ∉ set Cs; ¬ P ⊢ (last Cs) ≼⇧* C ⟧
  ⟹ P,E ⊢ ⟨⦇C⦈e,s⟩ →* ⟨THROW ClassCast,s'⟩"

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


lemma StaticCastRedsThrow:
  "⟦ P,E ⊢ ⟨e,s⟩ →* ⟨Throw r,s'⟩ ⟧ ⟹ P,E ⊢ ⟨⦇C⦈e,s⟩ →* ⟨Throw r,s'⟩"

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


lemma DynCastReds:
  "P,E ⊢ ⟨e,s⟩ →* ⟨e',s'⟩ ⟹ P,E ⊢ ⟨Cast C e,s⟩ →* ⟨Cast C e',s'⟩"

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


lemma DynCastRedsNull:
  "P,E ⊢ ⟨e,s⟩ →* ⟨null,s'⟩ ⟹ P,E ⊢ ⟨Cast C e,s⟩ →* ⟨null,s'⟩"

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


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

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


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

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


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

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


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

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


lemma DynCastRedsThrow:
  "⟦ P,E ⊢ ⟨e,s⟩ →* ⟨Throw r,s'⟩ ⟧ ⟹ P,E ⊢ ⟨Cast C e,s⟩ →* ⟨Throw r,s'⟩"

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


subsection ‹LAss›

lemma LAssReds:
  "P,E ⊢ ⟨e,s⟩ →* ⟨e',s'⟩ ⟹ P,E ⊢ ⟨V:=e,s⟩ →* ⟨V:=e',s'⟩"

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


lemma LAssRedsVal:
  "⟦ P,E ⊢ ⟨e,s⟩ →* ⟨Val v,(h',l')⟩; E V = Some T; P ⊢ T casts v to v'⟧ 
  ⟹ P,E ⊢ ⟨ V:=e,s⟩ →* ⟨Val v',(h',l'(V↦v'))⟩"

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


lemma LAssRedsThrow:
  "⟦ P,E ⊢ ⟨e,s⟩ →* ⟨Throw r,s'⟩ ⟧ ⟹ P,E ⊢ ⟨ V:=e,s⟩ →* ⟨Throw r,s'⟩"

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


subsection ‹BinOp›

lemma BinOp1Reds:
  "P,E ⊢ ⟨e,s⟩ →* ⟨e',s'⟩ ⟹ P,E ⊢ ⟨ e «bop» e⇩2, s⟩ →* ⟨e' «bop» e⇩2, s'⟩"

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


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

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


lemma BinOpRedsVal:
  "⟦ P,E ⊢ ⟨e⇩1,s⇩0⟩ →* ⟨Val v⇩1,s⇩1⟩; P,E ⊢ ⟨e⇩2,s⇩1⟩ →* ⟨Val v⇩2,s⇩2⟩; 
     binop(bop,v⇩1,v⇩2) = Some v ⟧
  ⟹ P,E ⊢ ⟨e⇩1 «bop» e⇩2, s⇩0⟩ →* ⟨Val v,s⇩2⟩"

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


lemma BinOpRedsThrow1:
  "P,E ⊢ ⟨e,s⟩ →* ⟨Throw r,s'⟩ ⟹ P,E ⊢ ⟨e «bop» e⇩2, s⟩ →* ⟨Throw r, s'⟩"

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


lemma BinOpRedsThrow2:
  "⟦ P,E ⊢ ⟨e⇩1,s⇩0⟩ →* ⟨Val v⇩1,s⇩1⟩; P,E ⊢ ⟨e⇩2,s⇩1⟩ →* ⟨Throw r,s⇩2⟩⟧
  ⟹ P,E ⊢ ⟨e⇩1 «bop» e⇩2, s⇩0⟩ →* ⟨Throw r,s⇩2⟩"

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


subsection ‹FAcc›

lemma FAccReds:
  "P,E ⊢ ⟨e,s⟩ →* ⟨e',s'⟩ ⟹ P,E ⊢ ⟨e∙F{Cs}, s⟩ →* ⟨e'∙F{Cs}, s'⟩"

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


lemma FAccRedsVal:
  "⟦P,E ⊢ ⟨e,s⟩ →* ⟨ref(a,Cs'),s'⟩; hp s' a = Some(D,S); 
    Ds = Cs'@⇩pCs; (Ds,fs) ∈ S; fs F = Some v ⟧
  ⟹ P,E ⊢ ⟨e∙F{Cs},s⟩ →* ⟨Val v,s'⟩"

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


lemma FAccRedsNull:
  "P,E ⊢ ⟨e,s⟩ →* ⟨null,s'⟩ ⟹ P,E ⊢ ⟨e∙F{Cs},s⟩ →* ⟨THROW NullPointer,s'⟩"

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


lemma FAccRedsThrow:
  "P,E ⊢ ⟨e,s⟩ →* ⟨Throw r,s'⟩ ⟹ P,E ⊢ ⟨e∙F{Cs},s⟩ →* ⟨Throw r,s'⟩"

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


subsection ‹FAss›

lemma FAssReds1:
  "P,E ⊢ ⟨e,s⟩ →* ⟨e',s'⟩ ⟹ P,E ⊢ ⟨e∙F{Cs}:=e⇩2, s⟩ →* ⟨e'∙F{Cs}:=e⇩2, s'⟩"

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


lemma FAssReds2:
  "P,E ⊢ ⟨e,s⟩ →* ⟨e',s'⟩ ⟹ P,E ⊢ ⟨Val v∙F{Cs}:=e, s⟩ →* ⟨Val v∙F{Cs}:=e', s'⟩"

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


lemma FAssRedsVal:
  "⟦ P,E ⊢ ⟨e⇩1,s⇩0⟩ →* ⟨ref(a,Cs'),s⇩1⟩; P,E ⊢ ⟨e⇩2,s⇩1⟩ →* ⟨Val v,(h⇩2,l⇩2)⟩; 
    h⇩2 a = Some(D,S); P ⊢ (last Cs') has least F:T via Cs; P ⊢ T casts v to v';
    Ds = Cs'@⇩pCs; (Ds,fs) ∈ S ⟧ ⟹
  P,E ⊢ ⟨e⇩1∙F{Cs}:=e⇩2, s⇩0⟩ →* 
        ⟨Val v',(h⇩2(a↦(D,insert (Ds,fs(F↦v')) (S - {(Ds,fs)}))),l⇩2)⟩"

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


lemma FAssRedsNull:
  "⟦ P,E ⊢ ⟨e⇩1,s⇩0⟩ →* ⟨null,s⇩1⟩; P,E ⊢ ⟨e⇩2,s⇩1⟩ →* ⟨Val v,s⇩2⟩ ⟧ ⟹
  P,E ⊢ ⟨e⇩1∙F{Cs}:=e⇩2, s⇩0⟩ →* ⟨THROW NullPointer, s⇩2⟩"

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


lemma FAssRedsThrow1:
  "P,E ⊢ ⟨e,s⟩ →* ⟨Throw r,s'⟩ ⟹ P,E ⊢ ⟨e∙F{Cs}:=e⇩2, s⟩ →* ⟨Throw r, s'⟩"

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


lemma FAssRedsThrow2:
  "⟦ P,E ⊢ ⟨e⇩1,s⇩0⟩ →* ⟨Val v,s⇩1⟩; P,E ⊢ ⟨e⇩2,s⇩1⟩ →* ⟨Throw r,s⇩2⟩ ⟧
  ⟹ P,E ⊢ ⟨e⇩1∙F{Cs}:=e⇩2,s⇩0⟩ →* ⟨Throw r,s⇩2⟩"

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


subsection ‹;;›

lemma  SeqReds:
  "P,E ⊢ ⟨e,s⟩ →* ⟨e',s'⟩ ⟹ P,E ⊢ ⟨e;;e⇩2, s⟩ →* ⟨e';;e⇩2, s'⟩"

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


lemma SeqRedsThrow:
  "P,E ⊢ ⟨e,s⟩ →* ⟨Throw r,s'⟩ ⟹ P,E ⊢ ⟨e;;e⇩2, s⟩ →* ⟨Throw r, s'⟩"

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


lemma SeqReds2:
  "⟦ P,E ⊢ ⟨e⇩1,s⇩0⟩ →* ⟨Val v⇩1,s⇩1⟩; P,E ⊢ ⟨e⇩2,s⇩1⟩ →* ⟨e⇩2',s⇩2⟩ ⟧ ⟹ P,E ⊢ ⟨e⇩1;;e⇩2, s⇩0⟩ →* ⟨e⇩2',s⇩2⟩"

apply(rule rtrancl_trans)
 apply(erule SeqReds)
apply(rule_tac b="(e⇩2,s⇩1)" in converse_rtrancl_into_rtrancl)
 apply(simp add:RedSeq)
apply assumption
done



subsection ‹If›

lemma CondReds:
  "P,E ⊢ ⟨e,s⟩ →* ⟨e',s'⟩ ⟹ P,E ⊢ ⟨if (e) e⇩1 else e⇩2,s⟩ →* ⟨if (e') e⇩1 else e⇩2,s'⟩"

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


lemma CondRedsThrow:
  "P,E ⊢ ⟨e,s⟩ →* ⟨Throw r,s'⟩ ⟹ P,E ⊢ ⟨if (e) e⇩1 else e⇩2, s⟩ →* ⟨Throw r,s'⟩"

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


lemma CondReds2T:
  "⟦P,E ⊢ ⟨e,s⇩0⟩ →* ⟨true,s⇩1⟩; P,E ⊢ ⟨e⇩1, s⇩1⟩ →* ⟨e',s⇩2⟩ ⟧ ⟹ P,E ⊢ ⟨if (e) e⇩1 else e⇩2, s⇩0⟩ →* ⟨e',s⇩2⟩"

apply(rule rtrancl_trans)
 apply(erule CondReds)
apply(rule_tac b="(e⇩1, s⇩1)" in converse_rtrancl_into_rtrancl)
 apply(simp add:RedCondT)
apply assumption
done


lemma CondReds2F:
  "⟦P,E ⊢ ⟨e,s⇩0⟩ →* ⟨false,s⇩1⟩; P,E ⊢ ⟨e⇩2, s⇩1⟩ →* ⟨e',s⇩2⟩ ⟧ ⟹ P,E ⊢ ⟨if (e) e⇩1 else e⇩2, s⇩0⟩ →* ⟨e',s⇩2⟩"

apply(rule rtrancl_trans)
 apply(erule CondReds)
apply(rule_tac b="(e⇩2, s⇩1)" in  converse_rtrancl_into_rtrancl)
 apply(simp add:RedCondF)
apply assumption
done



subsection ‹While›

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

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


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

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


lemma WhileTReds:
  "⟦ P,E ⊢ ⟨b,s⇩0⟩ →* ⟨true,s⇩1⟩; P,E ⊢ ⟨c,s⇩1⟩ →* ⟨Val v⇩1,s⇩2⟩; P,E ⊢ ⟨while (b) c,s⇩2⟩ →* ⟨e,s⇩3⟩ ⟧
  ⟹ P,E ⊢ ⟨while (b) c,s⇩0⟩ →* ⟨e,s⇩3⟩"

apply(rule_tac b="(if(b) (c;;while(b) c) else unit, s⇩0)" in converse_rtrancl_into_rtrancl)
 apply(simp add:RedWhile)
apply(rule rtrancl_trans)
 apply(erule CondReds)
apply(rule_tac b="(c;;while(b) c,s⇩1)" in converse_rtrancl_into_rtrancl)
 apply(simp add:RedCondT)
apply(rule rtrancl_trans)
 apply(erule SeqReds)
apply(rule_tac b="(while(b) c,s⇩2)" in converse_rtrancl_into_rtrancl)
 apply(simp add:RedSeq)
apply assumption
done


lemma WhileTRedsThrow:
  "⟦ P,E ⊢ ⟨b,s⇩0⟩ →* ⟨true,s⇩1⟩; P,E ⊢ ⟨c,s⇩1⟩ →* ⟨Throw r,s⇩2⟩ ⟧
  ⟹ P,E ⊢ ⟨while (b) c,s⇩0⟩ →* ⟨Throw r,s⇩2⟩"

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


subsection ‹Throw›

lemma ThrowReds:
  "P,E ⊢ ⟨e,s⟩ →* ⟨e',s'⟩ ⟹ P,E ⊢ ⟨throw e,s⟩ →* ⟨throw e',s'⟩"

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


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

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


lemma ThrowRedsThrow:
  "P,E ⊢ ⟨e,s⟩ →* ⟨Throw r,s'⟩ ⟹ P,E ⊢ ⟨throw e,s⟩ →* ⟨Throw r,s'⟩"

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


subsection ‹InitBlock›

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



lemma InitBlockReds:
 "⟦P,E(V ↦ T) ⊢ ⟨e, (h,l(V↦v'))⟩ →* ⟨e', (h',l')⟩; 
   P ⊢ T casts v to v'; wf_prog wf_md P ⟧ ⟹
  ∃v'' w. P,E ⊢ ⟨{V:T := Val v; e}, (h,l)⟩ →* 
              ⟨{V:T := Val v''; e'}, (h',l'(V:=(l V)))⟩ ∧
          P ⊢ T casts v'' to w"
by(blast dest:InitBlockReds_aux)

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



subsection ‹Block›

lemma BlockRedsFinal:
assumes reds: "P,E(V ↦ T) ⊢ ⟨e⇩0,s⇩0⟩ →* ⟨e⇩2,(h⇩2,l⇩2)⟩" and fin: "final e⇩2"
  and wf:"wf_prog wf_md P"
shows "⋀h⇩0 l⇩0. s⇩0 = (h⇩0,l⇩0(V:=None)) ⟹ P,E ⊢ ⟨{V:T; e⇩0},(h⇩0,l⇩0)⟩ →* ⟨e⇩2,(h⇩2,l⇩2(V:=l⇩0 V))⟩"

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




subsection ‹List›

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

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


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

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


lemma ListRedsVal:
  "⟦ P,E ⊢ ⟨e,s⇩0⟩ →* ⟨Val v,s⇩1⟩; P,E ⊢ ⟨es,s⇩1⟩ [→]* ⟨es',s⇩2⟩ ⟧
  ⟹ P,E ⊢ ⟨e#es,s⇩0⟩ [→]* ⟨Val v # es',s⇩2⟩"

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


subsection ‹Call›

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


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



lemma Red_dom_lcl:
  "P,E ⊢ ⟨e,(h,l)⟩ → ⟨e',(h',l')⟩ ⟹ dom l' ⊆ dom l ∪ fv e" and
  "P,E ⊢ ⟨es,(h,l)⟩ [→] ⟨es',(h',l')⟩ ⟹ dom l' ⊆ dom l ∪ fvs es"

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



lemma Reds_dom_lcl:
  "⟦ wwf_prog P; P,E ⊢ ⟨e,(h,l)⟩ →* ⟨e',(h',l')⟩ ⟧ ⟹ dom l' ⊆ dom l ∪ fv e"

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


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


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

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

declare fun_upd_apply[simp del] map_upds_twist[simp del]




lemma assumes wf:"wf_prog wf_md P"
  shows blocksReds:
  "⋀l⇩0 E vs'. ⟦ length Vs = length Ts; length vs = length Ts; 
        distinct Vs; ⌦‹∀T∈set Ts. is_type P T;› P ⊢ Ts Casts vs to vs';
        P,E(Vs [↦] Ts) ⊢ ⟨e, (h⇩0,l⇩0(Vs [↦] vs'))⟩ →* ⟨e', (h⇩1,l⇩1)⟩ ⟧
  ⟹ ∃vs''. P,E ⊢ ⟨blocks(Vs,Ts,vs,e), (h⇩0,l⇩0)⟩ →* 
                   ⟨blocks(Vs,Ts,vs'',e'), (h⇩1,override_on l⇩1 l⇩0 (set Vs))⟩ ∧ 
             (∃ws. P ⊢ Ts Casts vs'' to ws) ∧ length vs = length vs''"

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



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

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



lemma assumes wfmd:"wf_prog wf_md P"
  and wf: "length Vs = length Ts" "length vs = length Ts" "distinct Vs" 
  and casts:"P ⊢ Ts Casts vs to vs'"
  and reds: "P,E(Vs [↦] Ts) ⊢ ⟨e, (h⇩0, l⇩0(Vs [↦] vs'))⟩ →* ⟨e', (h⇩1, l⇩1)⟩"
  and fin: "final e'" and l2: "l⇩2 = override_on l⇩1 l⇩0 (set Vs)"
shows blocksRedsFinal: "P,E ⊢ ⟨blocks(Vs,Ts,vs,e), (h⇩0, l⇩0)⟩ →* ⟨e', (h⇩1,l⇩2)⟩"

proof -
  obtain vs'' ws where blocks:"P,E ⊢ ⟨blocks(Vs,Ts,vs,e), (h⇩0, l⇩0)⟩ →* 
                                  ⟨blocks(Vs,Ts,vs'',e'), (h⇩1,l⇩2)⟩"
    and length:"length vs = length vs''"
    and casts':"P ⊢ Ts Casts vs'' to ws"
    using l2 blocksReds[OF wfmd wf casts reds]
     by auto
   have "P,E ⊢ ⟨blocks(Vs,Ts,vs'',e'), (h⇩1,l⇩2)⟩ →* ⟨e', (h⇩1,l⇩2)⟩"
     using blocksFinal[OF wfmd _ _ fin casts'] wf length by simp
   with blocks show ?thesis by simp
qed




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

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

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


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

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




lemma cast_lcl:
  "P,E ⊢ ⟨⦇C⦈(Val v),(h,l)⟩ → ⟨Val v',(h,l)⟩ ⟹
   P,E ⊢ ⟨⦇C⦈(Val v),(h,l')⟩ → ⟨Val v',(h,l')⟩"

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


lemma cast_env:
  "P,E ⊢ ⟨⦇C⦈(Val v),(h,l)⟩ → ⟨Val v',(h,l)⟩ ⟹ 
   P,E' ⊢ ⟨⦇C⦈(Val v),(h,l)⟩ → ⟨Val v',(h,l)⟩"

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


lemma Cast_step_Cast_or_fin:
"P,E ⊢ ⟨⦇C⦈e,s⟩ →* ⟨e',s'⟩ ⟹ final e' ∨ (∃e''. e' = ⦇C⦈e'')"
by(induct rule:rtrancl_induct2,auto elim:red.cases simp:final_def)

lemma Cast_red:"P,E ⊢ ⟨e,s⟩ →* ⟨e',s'⟩ ⟹ 
  (⋀e⇩1. ⟦e = ⦇C⦈e⇩0; e' = ⦇C⦈e⇩1⟧ ⟹ P,E ⊢ ⟨e⇩0,s⟩ →* ⟨e⇩1,s'⟩)"

proof(induct rule:rtrancl_induct2)
  case refl thus ?case by simp
next
  case (step e'' s'' e' s')
  have step:"P,E ⊢ ⟨e,s⟩ →* ⟨e'',s''⟩"
    and Red:"((e'', s''), e', s') ∈ Red P E"
    and cast:"e = ⦇C⦈e⇩0" and cast':"e' = ⦇C⦈e⇩1"
    and IH:"⋀e⇩1. ⟦e = ⦇C⦈e⇩0; e'' = ⦇C⦈e⇩1⟧ ⟹ P,E ⊢ ⟨e⇩0,s⟩ →* ⟨e⇩1,s''⟩" by fact+
  from Red have red:"P,E ⊢ ⟨e'',s''⟩ → ⟨e',s'⟩" by simp
  from step cast have "final e'' ∨ (∃ex. e'' = ⦇C⦈ex)"
    by simp(rule Cast_step_Cast_or_fin)
  thus ?case
  proof(rule disjE)
    assume "final e''"
    with red show ?thesis by(auto simp:final_def)
  next
    assume "∃ex. e'' = ⦇C⦈ex"
    then obtain ex where e'':"e'' = ⦇C⦈ex" by blast
    with cast' red have "P,E ⊢ ⟨ex,s''⟩ → ⟨e⇩1,s'⟩"
      by(auto elim:red.cases)
    with  IH[OF cast e''] show ?thesis
      by(rule_tac b="(ex,s'')" in rtrancl_into_rtrancl,simp_all)
  qed
qed


lemma Cast_final:"⟦P,E ⊢ ⟨⦇C⦈e,s⟩ →* ⟨e',s'⟩; final e'⟧ ⟹
∃e'' s''. P,E ⊢ ⟨e,s⟩ →* ⟨e'',s''⟩ ∧ P,E ⊢ ⟨⦇C⦈e'',s''⟩ → ⟨e',s'⟩ ∧ final e''"

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


lemma Cast_final_eq:
  assumes red:"P,E ⊢ ⟨⦇C⦈e,(h,l)⟩ → ⟨e',(h,l)⟩"
  and final:"final e" and final':"final e'"
  shows "P,E' ⊢ ⟨⦇C⦈e,(h,l')⟩ → ⟨e',(h,l')⟩"

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



lemma CallRedsFinal:
assumes wwf: "wwf_prog P"
and "P,E ⊢ ⟨e,s⇩0⟩ →* ⟨ref(a,Cs),s⇩1⟩"
      "P,E ⊢ ⟨es,s⇩1⟩ [→]* ⟨map Val vs,(h⇩2,l⇩2)⟩"
and hp: "h⇩2 a = Some(C,S)"
and "method": "P ⊢ last Cs has least M = (Ts',T',pns',body') via Ds"
and select: "P ⊢ (C,Cs@⇩pDs) selects M = (Ts,T,pns,body) via Cs'"
and size: "size vs = size pns"
and casts: "P ⊢ Ts Casts vs to vs'"
and l⇩2': "l⇩2' = [this ↦ Ref(a,Cs'), pns[↦]vs']"
and body_case:"new_body = (case T' of Class D ⇒ ⦇D⦈body  | _ ⇒ body)"
and body: "P,E(this ↦ Class (last Cs'), pns [↦] Ts) ⊢ ⟨new_body,(h⇩2,l⇩2')⟩ →* ⟨ef,(h⇩3,l⇩3)⟩"
and final:"final ef"
shows "P,E ⊢ ⟨e∙M(es), s⇩0⟩ →* ⟨ef,(h⇩3,l⇩2)⟩"
proof -
  have wf: "size Ts = size pns ∧ distinct pns ∧ this ∉ set pns"
    and wt: "fv body ⊆ {this} ∪ set pns"
    using assms by(fastforce dest!:select_method_wf_mdecl simp:wf_mdecl_def)+
  have "dom l⇩3 ⊆ {this} ∪ set pns"
    using Reds_dom_lcl[OF wwf body] wt l⇩2' set_take_subset body_case
    by (cases T') force+
  hence eql⇩2: "override_on (l⇩2++l⇩3) l⇩2 ({this} ∪ set pns) = l⇩2"
    by(fastforce simp add:map_add_def override_on_def fun_eq_iff)
  from wwf select have "is_class P (last Cs')"
    by (auto elim!:SelectMethodDef.cases intro:Subobj_last_isClass 
             simp:LeastMethodDef_def FinalOverriderMethodDef_def 
                  OverriderMethodDefs_def MinimalMethodDefs_def MethodDefs_def)
  hence "P ⊢ Class (last Cs') casts Ref(a,Cs') to Ref(a,Cs')"
    by(auto intro!:casts_ref Subobjs_Base simp:path_via_def appendPath_def)
  with casts
  have casts':"P ⊢ Class (last Cs')#Ts Casts Ref(a,Cs')#vs to  Ref(a,Cs')#vs'"
    by -(rule Casts_Cons)
  have 1:"P,E ⊢ ⟨e∙M(es),s⇩0⟩ →* ⟨(ref(a,Cs))∙M(es),s⇩1⟩" by(rule CallRedsObj)(rule assms(2))
  have 2:"P,E ⊢ ⟨(ref(a,Cs))∙M(es),s⇩1⟩ →*
                 ⟨(ref(a,Cs))∙M(map Val vs),(h⇩2,l⇩2)⟩"
    by(rule CallRedsParams)(rule assms(3))
  from body[THEN Red_lcl_add, of l⇩2]
  have body': "P,E(this ↦ Class (last Cs'), pns [↦] Ts) ⊢ 
             ⟨new_body,(h⇩2,l⇩2(this↦ Ref(a,Cs'), pns[↦]vs'))⟩ →* ⟨ef,(h⇩3,l⇩2++l⇩3)⟩"
    by (simp add:l⇩2')
  show ?thesis
  proof(cases "∀C. T'≠ Class C")
    case True
    hence "P,E ⊢ ⟨(ref(a,Cs))∙M(map Val vs), (h⇩2,l⇩2)⟩ → 
                 ⟨blocks(this#pns,Class(last Cs')#Ts,Ref(a,Cs')#vs,body), (h⇩2,l⇩2)⟩"
      <