Theory Equivalence

(*  Title:      JinjaDCI/J/Equivalence.thy
    Author:     Tobias Nipkow, Susannah Mansky
    Copyright   2003 Technische Universitaet Muenchen, 2019-20 UIUC

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

section ‹ Equivalence of Big Step and Small Step Semantics ›

theory Equivalence imports TypeSafe WWellForm begin

subsection‹Small steps simulate big step›

subsubsection "Init"

text "The reduction of initialization expressions doesn't touch or use
 their on-hold expressions (the subexpression to the right of @{text ←})
 until the initialization operation completes. This function is used to prove
 this and related properties. It is then used for general reduction of
 initialization expressions separately from their on-hold expressions by
 using the on-hold expression @{term unit}, then putting the real on-hold
 expression back in at the end."

fun init_switch :: "'a exp ⇒ 'a exp ⇒ 'a exp" where
"init_switch (INIT C (Cs,b) ← ei) e = (INIT C (Cs,b) ← e)" |
"init_switch (RI(C,e');Cs ← ei) e = (RI(C,e');Cs ← e)" |
"init_switch e' e = e'"

fun INIT_class :: "'a exp ⇒ cname option" where
"INIT_class (INIT C (Cs,b) ← e) = (if C = last (C#Cs) then Some C else None)" |
"INIT_class (RI(C,e0);Cs ← e) = Some (last (C#Cs))" |
"INIT_class _ = None"

lemma init_red_init:
"⟦ init_exp_of e0 = ⌊e⌋; P ⊢ ⟨e0,s0,b0⟩ → ⟨e1,s1,b1⟩ ⟧
  ⟹ (init_exp_of e1 = ⌊e⌋ ∧ (INIT_class e0 = ⌊C⌋ ⟶ INIT_class e1 = ⌊C⌋))
   ∨ (e1 = e ∧ b1 = icheck P (the(INIT_class e0)) e) ∨ (∃a. e1 = throw a)"
 by(erule red.cases, auto)

lemma init_exp_switch[simp]:
"init_exp_of e0 = ⌊e⌋ ⟹ init_exp_of (init_switch e0 e') = ⌊e'⌋"
 by(cases e0, simp_all)

lemma init_red_sync:
"⟦ P ⊢ ⟨e0,s0,b0⟩ → ⟨e1,s1,b1⟩; init_exp_of e0 = ⌊e⌋; e1 ≠ e ⟧
  ⟹ (⋀e'. P ⊢ ⟨init_switch e0 e',s0,b0⟩ → ⟨init_switch e1 e',s1,b1⟩)"
proof(induct rule: red.cases) qed(simp_all add: red_reds.intros)

lemma init_red_sync_end:
"⟦ P ⊢ ⟨e0,s0,b0⟩ → ⟨e1,s1,b1⟩; init_exp_of e0 = ⌊e⌋; e1 = e; throw_of e = None ⟧
  ⟹ (⋀e'. ¬sub_RI e' ⟹ P ⊢ ⟨init_switch e0 e',s0,b0⟩ → ⟨e',s1,icheck P (the(INIT_class e0)) e'⟩)"
proof(induct rule: red.cases) qed(simp_all add: red_reds.intros)

lemma init_reds_sync_unit':
 "⟦ P ⊢ ⟨e0,s0,b0⟩ →* ⟨Val v',s1,b1⟩; init_exp_of e0 = ⌊unit⌋; INIT_class e0 = ⌊C⌋ ⟧
  ⟹ (⋀e'. ¬sub_RI e' ⟹ P ⊢ ⟨init_switch e0 e',s0,b0⟩ →* ⟨e',s1,icheck P (the(INIT_class e0)) e'⟩)"
proof(induct rule:converse_rtrancl_induct3)
case refl then show ?case by simp
next
  case (step e0 s0 b0 e1 s1 b1)
  have "(init_exp_of e1 = ⌊unit⌋ ∧ (INIT_class e0 = ⌊C⌋ ⟶ INIT_class e1 = ⌊C⌋))
          ∨ (e1 = unit ∧ b1 = icheck P (the(INIT_class e0)) unit) ∨ (∃a. e1 = throw a)"
    using init_red_init[OF step.prems(1) step.hyps(1)] by simp
  then show ?case
  proof(rule disjE)
    assume assm: "init_exp_of e1 = ⌊unit⌋ ∧ (INIT_class e0 = ⌊C⌋ ⟶ INIT_class e1 = ⌊C⌋)"
    then have red: "P ⊢ ⟨init_switch e0 e',s0,b0⟩ → ⟨init_switch e1 e',s1,b1⟩"
      using init_red_sync[OF step.hyps(1) step.prems(1)] by simp
    have reds: "P ⊢ ⟨init_switch e1 e',s1,b1⟩ →* ⟨e',s1,icheck P (the (INIT_class e0)) e'⟩"
      using step.hyps(3)[OF _ _ step.prems(3)] assm step.prems(2) by simp
    show ?thesis by(rule converse_rtrancl_into_rtrancl[OF red reds])
  next
    assume "(e1 = unit ∧ b1 = icheck P (the(INIT_class e0)) unit) ∨ (∃a. e1 = throw a)"
    then show ?thesis
    proof(rule disjE)
      assume assm: "e1 = unit ∧ b1 = icheck P (the(INIT_class e0)) unit" then have e1: "e1 = unit" by simp
      have sb: "s1 = s1" "b1 = b1" using reds_final_same[OF step.hyps(2)] assm
        by(simp_all add: final_def)
      then have step': "P ⊢ ⟨init_switch e0 e',s0,b0⟩ → ⟨e',s1,icheck P (the (INIT_class e0)) e'⟩"
        using init_red_sync_end[OF step.hyps(1) step.prems(1) e1 _ step.prems(3)] by auto
      then have "P ⊢ ⟨init_switch e0 e',s0,b0⟩ →* ⟨e',s1,icheck P (the (INIT_class e0)) e'⟩"
        using r_into_rtrancl by auto
      then show ?thesis using step assm sb by simp
    next
      assume "∃a. e1 = throw a" then obtain a where "e1 = throw a" by clarsimp
      then have tof: "throw_of e1 = ⌊a⌋" by simp
      then show ?thesis using reds_throw[OF step.hyps(2) tof] by simp
    qed
  qed
qed

lemma init_reds_sync_unit_throw':
 "⟦ P ⊢ ⟨e0,s0,b0⟩ →* ⟨throw a,s1,b1⟩; init_exp_of e0 = ⌊unit⌋ ⟧
  ⟹ (⋀e'. P ⊢ ⟨init_switch e0 e',s0,b0⟩ →* ⟨throw a,s1,b1⟩)"
proof(induct rule:converse_rtrancl_induct3)
case refl then show ?case by simp
next
  case (step e0 s0 b0 e1 s1 b1)
  have "init_exp_of e1 = ⌊unit⌋ ∧ (∀C. INIT_class e0 = ⌊C⌋ ⟶ INIT_class e1 = ⌊C⌋) ∨
  e1 = unit ∧ b1 = icheck P (the (INIT_class e0)) unit ∨ (∃a. e1 = throw a)"
    using init_red_init[OF step.prems(1) step.hyps(1)] by auto
  then show ?case
  proof(rule disjE)
    assume assm: "init_exp_of e1 = ⌊unit⌋ ∧ (∀C. INIT_class e0 = ⌊C⌋ ⟶ INIT_class e1 = ⌊C⌋)"
    then have "P ⊢ ⟨init_switch e0 e',s0,b0⟩ → ⟨init_switch e1 e',s1,b1⟩"
      using step init_red_sync[OF step.hyps(1) step.prems] by simp
    then show ?thesis using step assm by (meson converse_rtrancl_into_rtrancl)
  next
    assume "e1 = unit ∧ b1 = icheck P (the (INIT_class e0)) unit ∨ (∃a. e1 = throw a)"
    then show ?thesis
    proof(rule disjE)
      assume "e1 = unit ∧ b1 = icheck P (the (INIT_class e0)) unit"
      then show ?thesis using step using final_def reds_final_same by blast
    next
      assume assm: "∃a. e1 = throw a"
      then have "P ⊢ ⟨init_switch e0 e',s0,b0⟩ → ⟨e1,s1,b1⟩"
        using init_red_sync[OF step.hyps(1) step.prems] by clarsimp
      then show ?thesis using step by simp
    qed
  qed
qed

lemma init_reds_sync_unit:
assumes "P ⊢ ⟨e0,s0,b0⟩ →* ⟨Val v',s1,b1⟩" and "init_exp_of e0 = ⌊unit⌋" and "INIT_class e0 = ⌊C⌋"
  and "¬sub_RI e'"
shows "P ⊢ ⟨init_switch e0 e',s0,b0⟩ →* ⟨e',s1,icheck P (the(INIT_class e0)) e'⟩"
using init_reds_sync_unit'[OF assms] by clarsimp

lemma init_reds_sync_unit_throw:
assumes "P ⊢ ⟨e0,s0,b0⟩ →* ⟨throw a,s1,b1⟩" and "init_exp_of e0 = ⌊unit⌋"
shows "P ⊢ ⟨init_switch e0 e',s0,b0⟩ →* ⟨throw a,s1,b1⟩"
using init_reds_sync_unit_throw'[OF assms] by clarsimp

― ‹ init reds lemmas ›

lemma InitSeqReds:
assumes "P ⊢ ⟨INIT C ([C],b) ← unit,s0,b0⟩ →* ⟨Val v',s1,b1⟩"
 and "P ⊢ ⟨e,s1,icheck P C e⟩ →* ⟨e2,s2,b2⟩" and "¬sub_RI e"
shows "P ⊢ ⟨INIT C ([C],b) ← e,s0,b0⟩ →* ⟨e2,s2,b2⟩"
using assms
proof -
  have "P ⊢ ⟨init_switch (INIT C ([C],b) ← unit) e,s0,b0⟩ →* ⟨e,s1,icheck P C e⟩"
    using init_reds_sync_unit[OF assms(1) _ _ assms(3)] by simp
  then show ?thesis using assms(2) by simp
qed

lemma InitSeqThrowReds:
assumes "P ⊢ ⟨INIT C ([C],b) ← unit,s0,b0⟩ →* ⟨throw a,s1,b1⟩"
shows "P ⊢ ⟨INIT C ([C],b) ← e,s0,b0⟩ →* ⟨throw a,s1,b1⟩"
using assms
proof -
  have "P ⊢ ⟨init_switch (INIT C ([C],b) ← unit) e,s0,b0⟩ →* ⟨throw a,s1,b1⟩"
    using init_reds_sync_unit_throw[OF assms(1)] by simp
  then show ?thesis by simp
qed

lemma InitNoneReds:
 "⟦ sh C = None;
    P ⊢ ⟨INIT C' (C # Cs,False) ← e,(h, l, sh(C ↦ (sblank P C, Prepared))),b⟩ →* ⟨e',s',b'⟩ ⟧
⟹ P ⊢ ⟨INIT C' (C#Cs,False) ← e,(h,l,sh),b⟩ →* ⟨e',s',b'⟩"
(*<*)by(rule InitNoneRed[THEN converse_rtrancl_into_rtrancl])(*>*)

lemma InitDoneReds:
 "⟦ sh C = Some(sfs,Done); P ⊢ ⟨INIT C' (Cs,True) ← e,(h,l,sh),b⟩ →* ⟨e',s',b'⟩ ⟧
⟹ P ⊢ ⟨INIT C' (C#Cs,False) ← e,(h,l,sh),b⟩ →* ⟨e',s',b'⟩"
(*<*)by(rule RedInitDone[THEN converse_rtrancl_into_rtrancl])(*>*)

lemma InitProcessingReds:
 "⟦ sh C = Some(sfs,Processing); P ⊢ ⟨INIT C' (Cs,True) ← e,(h,l,sh),b⟩ →* ⟨e',s',b'⟩ ⟧
⟹ P ⊢ ⟨INIT C' (C#Cs,False) ← e,(h,l,sh),b⟩ →* ⟨e',s',b'⟩"
(*<*)by(rule RedInitProcessing[THEN converse_rtrancl_into_rtrancl])(*>*)

lemma InitErrorReds:
 "⟦ sh C = Some(sfs,Error); P ⊢ ⟨RI (C,THROW NoClassDefFoundError);Cs ← e,(h,l,sh),b⟩ →* ⟨e',s',b'⟩ ⟧
⟹ P ⊢ ⟨INIT C' (C#Cs,False) ← e,(h,l,sh),b⟩ →* ⟨e',s',b'⟩"
(*<*)by(rule RedInitError[THEN converse_rtrancl_into_rtrancl])(*>*)

lemma InitObjectReds:
 "⟦ sh C = Some(sfs,Prepared); C = Object; sh' = sh(C ↦ (sfs,Processing));
    P ⊢ ⟨INIT C' (C#Cs,True) ← e,(h,l,sh'),b⟩ →* ⟨e',s',b'⟩ ⟧
⟹ P ⊢ ⟨INIT C' (C#Cs,False) ← e,(h,l,sh),b⟩ →* ⟨e',s',b'⟩"
(*<*)by(rule InitObjectRed[THEN converse_rtrancl_into_rtrancl])(*>*)

lemma InitNonObjectReds:
 "⟦ sh C = Some(sfs,Prepared); C ≠ Object; class P C = Some (D,r);
    sh' = sh(C ↦ (sfs,Processing));
    P ⊢ ⟨INIT C' (D#C#Cs,False) ← e,(h,l,sh'),b⟩ →* ⟨e',s',b'⟩ ⟧
⟹ P ⊢ ⟨INIT C' (C#Cs,False) ← e,(h,l,sh),b⟩ →* ⟨e',s',b'⟩"
(*<*)by(rule InitNonObjectSuperRed[THEN converse_rtrancl_into_rtrancl])(*>*)

lemma RedsInitRInit:
 "P ⊢ ⟨RI (C,C∙sclinit([]));Cs ← e,(h,l,sh),b⟩ →* ⟨e',s',b'⟩
⟹ P ⊢ ⟨INIT C' (C#Cs,True) ← e,(h,l,sh),b⟩ →* ⟨e',s',b'⟩"
(*<*)by(rule RedInitRInit[THEN converse_rtrancl_into_rtrancl])(*>*)

lemmas rtrancl_induct3 =
  rtrancl_induct[of "(ax,ay,az)" "(bx,by,bz)", split_format (complete), consumes 1, case_names refl step]

lemma RInitReds:
 "P ⊢ ⟨e,s,b⟩ →* ⟨e',s',b'⟩
⟹ P ⊢ ⟨RI (C,e);Cs ← e0, s, b⟩ →* ⟨RI (C,e');Cs ← e0, s', b'⟩"
(*<*)
proof(induct rule: rtrancl_induct3)
  case refl show ?case by blast
next
  case step show ?case
   by(rule rtrancl_into_rtrancl[OF step(3) RInitRed[OF step(2)]])
qed
(*>*)

lemma RedsRInit:
 "⟦ P ⊢ ⟨e0,s0,b0⟩ →* ⟨Val v,(h1,l1,sh1),b1⟩;
    sh1 C = Some (sfs, i); sh2 = sh1(C ↦ (sfs,Done)); C' = last(C#Cs);
    P ⊢ ⟨INIT C' (Cs,True) ← e,(h1,l1,sh2),b1⟩ →* ⟨e',s',b'⟩ ⟧
  ⟹ P ⊢ ⟨RI (C, e0);Cs ← e,s0,b0⟩ →* ⟨e',s',b'⟩"
(*<*)
by(rule rtrancl_trans[OF RInitReds
                         RedRInit[THEN converse_rtrancl_into_rtrancl]])
(*>*)


lemma RInitInitThrowReds:
 "⟦ P ⊢ ⟨e,s,b⟩ →* ⟨Throw a,(h',l',sh'),b'⟩;
    sh' C = Some (sfs, i); sh'' = sh'(C ↦ (sfs,Error));
    P ⊢ ⟨RI (D,Throw a);Cs ← e0, (h',l',sh''),b'⟩ →* ⟨e1,s1,b1⟩ ⟧
  ⟹ P ⊢ ⟨RI (C, e);D#Cs ← e0,s,b⟩ →* ⟨e1,s1,b1⟩"
(*<*)
by(rule rtrancl_trans[OF RInitReds
                         RInitInitThrow[THEN converse_rtrancl_into_rtrancl]])
(*>*)

lemma RInitThrowReds:
  "⟦ P ⊢ ⟨e,s,b⟩ →* ⟨Throw a, (h',l',sh'),b'⟩;
     sh' C = Some(sfs, i); sh'' = sh'(C ↦ (sfs, Error)) ⟧
  ⟹ P ⊢ ⟨RI (C,e);Nil ← e0,s,b⟩ →* ⟨Throw a, (h',l',sh''),b'⟩"
(*<*)by(rule RInitReds[THEN rtrancl_into_rtrancl, OF _ RInitThrow])(*>*)

subsubsection "New"

lemma NewInitDoneReds:
  "⟦ sh C = Some (sfs, Done); new_Addr h = Some a;
     P ⊢ C has_fields FDTs; h' = h(a↦blank P C) ⟧
   ⟹ P ⊢ ⟨new C,(h,l,sh),False⟩ →* ⟨addr a,(h',l,sh),False⟩"
(*<*)
by(rule NewInitDoneRed[THEN converse_rtrancl_into_rtrancl,
                       OF _ RedNew[THEN r_into_rtrancl]])
(*>*)

lemma NewInitDoneReds2:
  "⟦ sh C = Some (sfs, Done); new_Addr h = None; is_class P C ⟧
   ⟹ P ⊢ ⟨new C,(h,l,sh),False⟩ →* ⟨THROW OutOfMemory, (h,l,sh), False⟩"
(*<*)
by(rule NewInitDoneRed[THEN converse_rtrancl_into_rtrancl,
                       OF _ RedNewFail[THEN r_into_rtrancl]])
(*>*)

lemma NewInitReds:
assumes nDone: "∄sfs. shp s C = Some (sfs, Done)"
  and INIT_steps: "P ⊢ ⟨INIT C ([C],False) ← unit,s,False⟩ →* ⟨Val v',(h',l',sh'),b'⟩"
  and Addr: "new_Addr h' = Some a" and has: "P ⊢ C has_fields FDTs"
  and h'': "h'' = h'(a↦blank P C)" and cls_C: "is_class P C"
shows "P ⊢ ⟨new C,s,False⟩ →* ⟨addr a,(h'',l',sh'),False⟩"
(*<*)(is "(?a, ?c) ∈ (red P)*")
proof -
  let ?b = "(INIT C ([C],False) ← new C,s,False)"
  let ?b' = "(new C,(h', l', sh'),icheck P C (new C::expr))"
  have b'c: "(?b', ?c) ∈ (red P)*"
    using RedNew[OF Addr has h'', THEN r_into_rtrancl] by simp
  obtain h l sh where [simp]: "s = (h, l, sh)" by(cases s) simp
  have "(?a, ?b) ∈ (red P)*"
    using NewInitRed[OF _ cls_C] nDone by fastforce
  also have "(?b, ?c) ∈ (red P)*"
    by(rule InitSeqReds[OF INIT_steps b'c]) simp
  ultimately show ?thesis by simp
qed
(*>*)

lemma NewInitOOMReds:
assumes nDone: "∄sfs. shp s C = Some (sfs, Done)"
  and INIT_steps: "P ⊢ ⟨INIT C ([C],False) ← unit,s,False⟩ →* ⟨Val v',(h',l',sh'),b'⟩"
  and Addr: "new_Addr h' = None" and cls_C: "is_class P C"
shows "P ⊢ ⟨new C,s,False⟩ →* ⟨THROW OutOfMemory,(h',l',sh'),False⟩"
(*<*)(is "(?a, ?c) ∈ (red P)*")
proof -
  let ?b = "(INIT C ([C],False) ← new C,s,False)"
  let ?b' = "(new C,(h', l', sh'),icheck P C (new C::expr))"
  have b'c: "(?b', ?c) ∈ (red P)*"
    using RedNewFail[OF Addr cls_C, THEN r_into_rtrancl] by simp
  obtain h l sh where [simp]: "s = (h, l, sh)" by(cases s) simp
  have "(?a, ?b) ∈ (red P)*"
    using NewInitRed[OF _ cls_C] nDone by fastforce
  also have "(?b, ?c) ∈ (red P)*"
    by(rule InitSeqReds[OF INIT_steps b'c]) simp
  ultimately show ?thesis by simp
qed
(*>*)

lemma NewInitThrowReds:
assumes nDone: "∄sfs. shp s C = Some (sfs, Done)"
  and cls_C: "is_class P C"
  and INIT_steps: "P ⊢ ⟨INIT C ([C],False) ← unit,s,False⟩ →* ⟨throw a,s',b'⟩"
shows "P ⊢ ⟨new C,s,False⟩ →* ⟨throw a,s',b'⟩"
(*<*)(is "(?a, ?c) ∈ (red P)*")
proof -
  let ?b = "(INIT C ([C],False) ← new C,s,False)"
  obtain h l sh where [simp]: "s = (h, l, sh)" by(cases s) simp
  have "(?a, ?b) ∈ (red P)*"
    using NewInitRed[OF _ cls_C] nDone by fastforce
  also have "(?b, ?c) ∈ (red P)*"
    using InitSeqThrowReds[OF INIT_steps] by simp
  ultimately show ?thesis by simp
qed
(*>*)

subsubsection "Cast"

lemma CastReds:
  "P ⊢ ⟨e,s,b⟩ →* ⟨e',s',b'⟩ ⟹ P ⊢ ⟨Cast C e,s,b⟩ →* ⟨Cast C e',s',b'⟩"
(*<*)
proof(induct rule: rtrancl_induct3)
  case refl show ?case by blast
next
  case step show ?case
   by(rule rtrancl_into_rtrancl[OF step(3) CastRed[OF step(2)]])
qed
(*>*)

lemma CastRedsNull:
  "P ⊢ ⟨e,s,b⟩ →* ⟨null,s',b'⟩ ⟹ P ⊢ ⟨Cast C e,s,b⟩ →* ⟨null,s',b'⟩"
(*<*)by(rule CastReds[THEN rtrancl_into_rtrancl, OF _ RedCastNull])(*>*)

lemma CastRedsAddr:
  "⟦ P ⊢ ⟨e,s,b⟩ →* ⟨addr a,s',b'⟩; hp s' a = Some(D,fs); P ⊢ D ≼* C ⟧ ⟹
  P ⊢ ⟨Cast C e,s,b⟩ →* ⟨addr a,s',b'⟩"
(*<*)by(cases s', simp) (rule CastReds[THEN rtrancl_into_rtrancl, OF _ RedCast])(*>*)

lemma CastRedsFail:
  "⟦ P ⊢ ⟨e,s,b⟩ →* ⟨addr a,s',b'⟩; hp s' a = Some(D,fs); ¬ P ⊢ D ≼* C ⟧ ⟹
  P ⊢ ⟨Cast C e,s,b⟩ →* ⟨THROW ClassCast,s',b'⟩"
(*<*)by(cases s', simp) (rule CastReds[THEN rtrancl_into_rtrancl, OF _ RedCastFail])(*>*)

lemma CastRedsThrow:
  "⟦ P ⊢ ⟨e,s,b⟩ →* ⟨throw a,s',b'⟩ ⟧ ⟹ P ⊢ ⟨Cast C e,s,b⟩ →* ⟨throw a,s',b'⟩"
(*<*)by(rule CastReds[THEN rtrancl_into_rtrancl, OF _ red_reds.CastThrow])(*>*)

subsubsection "LAss"

lemma LAssReds:
  "P ⊢ ⟨e,s,b⟩ →* ⟨e',s',b'⟩ ⟹ P ⊢ ⟨ V:=e,s,b⟩ →* ⟨ V:=e',s',b'⟩"
(*<*)
proof(induct rule: rtrancl_induct3)
  case refl show ?case by blast
next
  case step show ?case
   by(rule rtrancl_into_rtrancl[OF step(3) LAssRed[OF step(2)]])
qed
(*>*)

lemma LAssRedsVal:
  "⟦ P ⊢ ⟨e,s,b⟩ →* ⟨Val v,(h',l',sh'),b'⟩ ⟧ ⟹ P ⊢ ⟨ V:=e,s,b⟩ →* ⟨unit,(h',l'(V↦v),sh'),b'⟩"
(*<*)by(rule LAssReds[THEN rtrancl_into_rtrancl, OF _ RedLAss])(*>*)

lemma LAssRedsThrow:
  "⟦ P ⊢ ⟨e,s,b⟩ →* ⟨throw a,s',b'⟩ ⟧ ⟹ P ⊢ ⟨ V:=e,s,b⟩ →* ⟨throw a,s',b'⟩"
(*<*)by(rule LAssReds[THEN rtrancl_into_rtrancl, OF _ red_reds.LAssThrow])(*>*)

subsubsection "BinOp"

lemma BinOp1Reds:
  "P ⊢ ⟨e,s,b⟩ →* ⟨e',s',b'⟩ ⟹ P ⊢ ⟨ e «bop» e2, s,b⟩ →* ⟨e' «bop» e2, s',b'⟩"
(*<*)
proof(induct rule: rtrancl_induct3)
  case refl show ?case by blast
next
  case step show ?case
   by(rule rtrancl_into_rtrancl[OF step(3) BinOpRed1[OF step(2)]])
qed
(*>*)

lemma BinOp2Reds:
  "P ⊢ ⟨e,s,b⟩ →* ⟨e',s',b'⟩ ⟹ P ⊢ ⟨(Val v) «bop» e, s,b⟩ →* ⟨(Val v) «bop» e', s',b'⟩"
(*<*)
proof(induct rule: rtrancl_induct3)
  case refl show ?case by blast
next
  case step show ?case
   by(rule rtrancl_into_rtrancl[OF step(3) BinOpRed2[OF step(2)]])
qed
(*>*)

lemma BinOpRedsVal:
assumes e1_steps: "P ⊢ ⟨e1,s0,b0⟩ →* ⟨Val v1,s1,b1⟩"
  and e2_steps: "P ⊢ ⟨e2,s1,b1⟩ →* ⟨Val v2,s2,b2⟩"
  and op: "binop(bop,v1,v2) = Some v"
shows "P ⊢ ⟨e1 «bop» e2, s0,b0⟩ →* ⟨Val v,s2,b2⟩"
(*<*)(is "(?x, ?z) ∈ (red P)*")
proof -
  let ?y = "(Val v1 «bop» e2, s1,b1)"
  let ?y' = "(Val v1 «bop» Val v2, s2,b2)"
  have "(?x, ?y) ∈ (red P)*" by(rule BinOp1Reds[OF e1_steps])
  also have "(?y, ?y') ∈ (red P)*" by(rule BinOp2Reds[OF e2_steps])
  also have "(?y', ?z) ∈ (red P)" by(rule RedBinOp[OF op])
  ultimately show ?thesis by simp
qed
(*>*)

lemma BinOpRedsThrow1:
  "P ⊢ ⟨e,s,b⟩ →* ⟨throw e',s',b'⟩ ⟹ P ⊢ ⟨e «bop» e2, s,b⟩ →* ⟨throw e', s',b'⟩"
(*<*)by(rule BinOp1Reds[THEN rtrancl_into_rtrancl, OF _ red_reds.BinOpThrow1])(*>*)

lemma BinOpRedsThrow2:
assumes e1_steps: "P ⊢ ⟨e1,s0,b0⟩ →* ⟨Val v1,s1,b1⟩"
  and e2_steps: "P ⊢ ⟨e2,s1,b1⟩ →* ⟨throw e,s2,b2⟩"
shows "P ⊢ ⟨e1 «bop» e2, s0,b0⟩ →* ⟨throw e,s2,b2⟩"
(*<*)(is "(?x, ?z) ∈ (red P)*")
proof -
  let ?y = "(Val v1 «bop» e2, s1,b1)"
  let ?y' = "(Val v1 «bop» throw e, s2,b2)"
  have "(?x, ?y) ∈ (red P)*" by(rule BinOp1Reds[OF e1_steps])
  also have "(?y, ?y') ∈ (red P)*" by(rule BinOp2Reds[OF e2_steps])
  also have "(?y', ?z) ∈ (red P)" by(rule red_reds.BinOpThrow2)
  ultimately show ?thesis by simp
qed
(*>*)

subsubsection "FAcc"

lemma FAccReds:
  "P ⊢ ⟨e,s,b⟩ →* ⟨e',s',b'⟩ ⟹ P ⊢ ⟨e∙F{D}, s,b⟩ →* ⟨e'∙F{D}, s',b'⟩"
(*<*)
proof(induct rule: rtrancl_induct3)
  case refl show ?case by blast
next
  case step show ?case
   by(rule rtrancl_into_rtrancl[OF step(3) FAccRed[OF step(2)]])
qed
(*>*)

lemma FAccRedsVal:
  "⟦ P ⊢ ⟨e,s,b⟩ →* ⟨addr a,s',b'⟩; hp s' a = Some(C,fs); fs(F,D) = Some v;
    P ⊢ C has F,NonStatic:t in D ⟧
  ⟹ P ⊢ ⟨e∙F{D},s,b⟩ →* ⟨Val v,s',b'⟩"
(*<*)by(cases s',simp) (rule FAccReds[THEN rtrancl_into_rtrancl, OF _ RedFAcc])(*>*)

lemma FAccRedsNull:
  "P ⊢ ⟨e,s,b⟩ →* ⟨null,s',b'⟩ ⟹ P ⊢ ⟨e∙F{D},s,b⟩ →* ⟨THROW NullPointer,s',b'⟩"
(*<*)by(rule FAccReds[THEN rtrancl_into_rtrancl, OF _ RedFAccNull])(*>*)

lemma FAccRedsNone:
  "⟦ P ⊢ ⟨e,s,b⟩ →* ⟨addr a,s',b'⟩;
     hp s' a = Some(C,fs);
    ¬(∃b t. P ⊢ C has F,b:t in D) ⟧
  ⟹ P ⊢ ⟨e∙F{D},s,b⟩ →* ⟨THROW NoSuchFieldError,s',b'⟩"
(*<*)by(cases s',simp) (auto intro: FAccReds[THEN rtrancl_into_rtrancl, OF _ RedFAccNone])(*>*)

lemma FAccRedsStatic:
  "⟦ P ⊢ ⟨e,s,b⟩ →* ⟨addr a,s',b'⟩;
     hp s' a = Some(C,fs);
    P ⊢ C has F,Static:t in D ⟧
  ⟹ P ⊢ ⟨e∙F{D},s,b⟩ →* ⟨THROW IncompatibleClassChangeError,s',b'⟩"
(*<*)by(cases s',simp) (rule FAccReds[THEN rtrancl_into_rtrancl, OF _ RedFAccStatic])(*>*)

lemma FAccRedsThrow:
  "P ⊢ ⟨e,s,b⟩ →* ⟨throw a,s',b'⟩ ⟹ P ⊢ ⟨e∙F{D},s,b⟩ →* ⟨throw a,s',b'⟩"
(*<*)by(rule FAccReds[THEN rtrancl_into_rtrancl, OF _ red_reds.FAccThrow])(*>*)

subsubsection "SFAcc"

lemma SFAccReds:
  "⟦ P ⊢ C has F,Static:t in D;
     shp s D = Some(sfs,Done); sfs F = Some v ⟧
  ⟹ P ⊢ ⟨C∙sF{D},s,True⟩ →* ⟨Val v,s,False⟩"
(*<*)by(cases s,simp) (rule RedSFAcc[THEN r_into_rtrancl])(*>*)

lemma SFAccRedsNone:
  "¬(∃b t. P ⊢ C has F,b:t in D)
  ⟹ P ⊢ ⟨C∙sF{D},s,b⟩ →* ⟨THROW NoSuchFieldError,s,False⟩"
(*<*)by(cases s,simp) (auto intro: RedSFAccNone[THEN r_into_rtrancl])(*>*)

lemma SFAccRedsNonStatic:
  "P ⊢ C has F,NonStatic:t in D
  ⟹ P ⊢ ⟨C∙sF{D},s,b⟩ →* ⟨THROW IncompatibleClassChangeError,s,False⟩"
(*<*)by(cases s,simp) (rule RedSFAccNonStatic[THEN r_into_rtrancl])(*>*)

lemma SFAccInitDoneReds:
assumes cF: "P ⊢ C has F,Static:t in D"
  and shp: "shp s D = Some (sfs,Done)" and sfs: "sfs F = Some v"
shows "P ⊢ ⟨C∙sF{D}, s, b⟩ →* ⟨Val v, s, False⟩"
(*<*)(is "(?a, ?c) ∈ (red P)*")
proof -
  obtain h l sh where [simp]: "s = (h, l, sh)" by(cases s) simp
  show ?thesis proof(cases b)
    case True
    then show ?thesis using assms
      by simp (rule RedSFAcc[THEN r_into_rtrancl])
  next
    case False
    let ?b = "(C∙sF{D},s,True)"
    have "(?a, ?b) ∈ (red P)*"
      using False SFAccInitDoneRed[where sh="shp s", OF cF shp] by fastforce
    also have "(?b, ?c) ∈ (red P)*" by(rule SFAccReds[OF assms])
    ultimately show ?thesis by simp
  qed
qed
(*>*)

lemma SFAccInitReds:
assumes cF: "P ⊢ C has F,Static:t in D"
  and nDone: "∄sfs. shp s D = Some (sfs,Done)"
  and INIT_steps: "P ⊢ ⟨INIT D ([D],False) ← unit,s,False⟩ →* ⟨Val v',s',b'⟩"
  and shp': "shp s' D = Some (sfs,i)" and sfs: "sfs F = Some v"
shows "P ⊢ ⟨C∙sF{D},s,False⟩ →* ⟨Val v,s',False⟩"
(*<*)(is "(?a, ?c) ∈ (red P)*")
proof -
  let ?b = "(INIT D ([D],False) ← C∙sF{D},s,False)"
  let ?b' = "(C∙sF{D},s',icheck P D (C∙sF{D}::expr))"
  obtain h l sh where [simp]: "s = (h, l, sh)" by(cases s) simp
  obtain h' l' sh' where [simp]: "s' = (h', l', sh')" by(cases s') simp
  have icheck: "icheck P D (C∙sF{D}) = True" using cF by fastforce
  then have b'c: "(?b', ?c) ∈ (red P)*"
    using RedSFAcc[THEN r_into_rtrancl, OF cF] shp' sfs by simp
  have "(?a, ?b) ∈ (red P)" using SFAccInitRed[OF cF] nDone by simp
  also have "(?b, ?c) ∈ (red P)*"
    by(rule InitSeqReds[OF INIT_steps b'c]) simp
  ultimately show ?thesis by simp
qed
(*>*)

lemma SFAccInitThrowReds:
  "⟦ P ⊢ C has F,Static:t in D;
     ∄sfs. shp s D = Some (sfs,Done);
     P ⊢ ⟨INIT D ([D],False) ← unit,s,False⟩ →* ⟨throw a,s',b'⟩ ⟧
 ⟹ P ⊢ ⟨C∙sF{D},s,False⟩ →* ⟨throw a,s',b'⟩"
(*<*)
by(cases s, simp)
  (auto elim: converse_rtrancl_into_rtrancl[OF SFAccInitRed InitSeqThrowReds])
(*>*)

subsubsection "FAss"

lemma FAssReds1:
  "P ⊢ ⟨e,s,b⟩ →* ⟨e',s',b'⟩ ⟹ P ⊢ ⟨e∙F{D}:=e2, s,b⟩ →* ⟨e'∙F{D}:=e2, s',b'⟩"
(*<*)
proof(induct rule: rtrancl_induct3)
  case refl show ?case by blast
next
  case step show ?case
   by(rule rtrancl_into_rtrancl[OF step(3) FAssRed1[OF step(2)]])
qed
(*>*)

lemma FAssReds2:
  "P ⊢ ⟨e,s,b⟩ →* ⟨e',s',b'⟩ ⟹ P ⊢ ⟨Val v∙F{D}:=e, s,b⟩ →* ⟨Val v∙F{D}:=e', s',b'⟩"
(*<*)
proof(induct rule: rtrancl_induct3)
  case refl show ?case by blast
next
  case step show ?case
   by(rule rtrancl_into_rtrancl[OF step(3) FAssRed2[OF step(2)]])
qed
(*>*)

lemma FAssRedsVal:
assumes e1_steps: "P ⊢ ⟨e1,s0,b0⟩ →* ⟨addr a,s1,b1⟩"
  and e2_steps: "P ⊢ ⟨e2,s1,b1⟩ →* ⟨Val v,(h2,l2,sh2),b2⟩"
  and cF: "P ⊢ C has F,NonStatic:t in D" and hC: "Some(C,fs) = h2 a"
shows "P ⊢ ⟨e1∙F{D}:=e2, s0, b0⟩ →* ⟨unit, (h2(a↦(C,fs((F,D)↦v))),l2,sh2),b2⟩"
(*<*)(is "(?x, ?z) ∈ (red P)*")
proof -
  let ?y = "(addr a∙F{D}:=e2, s1, b1)"
  let ?y' = "(addr a∙F{D}:=Val v::expr,(h2,l2,sh2),b2)"
  have "(?x, ?y) ∈ (red P)*" by(rule FAssReds1[OF e1_steps])
  also have "(?y, ?y') ∈ (red P)*" by(rule FAssReds2[OF e2_steps])
  also have "(?y', ?z) ∈ (red P)" using RedFAss[OF cF] hC by simp
  ultimately show ?thesis by simp
qed
(*>*)

lemma FAssRedsNull:
assumes e1_steps: "P ⊢ ⟨e1,s0,b0⟩ →* ⟨null,s1,b1⟩"
  and e2_steps: "P ⊢ ⟨e2,s1,b1⟩ →* ⟨Val v,s2,b2⟩"
shows "P ⊢ ⟨e1∙F{D}:=e2, s0, b0⟩ →* ⟨THROW NullPointer, s2, b2⟩"
(*<*)(is "(?x, ?z) ∈ (red P)*")
proof -
  let ?y = "(null∙F{D}:=e2, s1, b1)"
  let ?y' = "(null∙F{D}:=Val v::expr,s2,b2)"
  have "(?x, ?y) ∈ (red P)*" by(rule FAssReds1[OF e1_steps])
  also have "(?y, ?y') ∈ (red P)*" by(rule FAssReds2[OF e2_steps])
  also have "(?y', ?z) ∈ (red P)" by(rule RedFAssNull)
  ultimately show ?thesis by simp
qed
(*>*)

lemma FAssRedsThrow1:
  "P ⊢ ⟨e,s,b⟩ →* ⟨throw e',s',b'⟩ ⟹ P ⊢ ⟨e∙F{D}:=e2, s,b⟩ →* ⟨throw e', s',b'⟩"
(*<*)by(rule FAssReds1[THEN rtrancl_into_rtrancl, OF _ red_reds.FAssThrow1])(*>*)

lemma FAssRedsThrow2:
assumes e1_steps: "P ⊢ ⟨e1,s0,b0⟩ →* ⟨Val v,s1,b1⟩"
  and e2_steps: "P ⊢ ⟨e2,s1,b1⟩ →* ⟨throw e,s2,b2⟩"
shows "P ⊢ ⟨e1∙F{D}:=e2,s0,b0⟩ →* ⟨throw e,s2,b2⟩"
(*<*)(is "(?x, ?z) ∈ (red P)*")
proof -
  let ?y = "(Val v∙F{D}:=e2,s1,b1)"
  let ?y' = "(Val v∙F{D}:=throw e,s2,b2)"
  have "(?x, ?y) ∈ (red P)*" by(rule FAssReds1[OF e1_steps])
  also have "(?y, ?y') ∈ (red P)*" by(rule FAssReds2[OF e2_steps])
  also have "(?y', ?z) ∈ (red P)" by(rule red_reds.FAssThrow2)
  ultimately show ?thesis by simp
qed
(*>*)

lemma FAssRedsNone:
assumes e1_steps: "P ⊢ ⟨e1,s0,b0⟩ →* ⟨addr a,s1,b1⟩"
  and e2_steps: "P ⊢ ⟨e2,s1,b1⟩ →* ⟨Val v,(h2,l2,sh2),b2⟩"
  and hC: "h2 a = Some(C,fs)" and ncF: "¬(∃b t. P ⊢ C has F,b:t in D)"
shows "P ⊢ ⟨e1∙F{D}:=e2, s0, b0⟩ →* ⟨THROW NoSuchFieldError, (h2,l2,sh2), b2⟩"
(*<*)(is "(?x, ?z) ∈ (red P)*")
proof -
  let ?y = "(addr a∙F{D}:=e2, s1, b1)"
  let ?y' = "(addr a∙F{D}:=Val v::expr,(h2,l2,sh2),b2)"
  have "(?x, ?y) ∈ (red P)*" by(rule FAssReds1[OF e1_steps])
  also have "(?y, ?y') ∈ (red P)*" by(rule FAssReds2[OF e2_steps])
  also have "(?y', ?z) ∈ (red P)"
    using RedFAssNone[OF _ ncF] hC by simp
  ultimately show ?thesis by simp
qed
(*>*)

lemma FAssRedsStatic:
assumes e1_steps: "P ⊢ ⟨e1,s0,b0⟩ →* ⟨addr a,s1,b1⟩"
  and e2_steps: "P ⊢ ⟨e2,s1,b1⟩ →* ⟨Val v,(h2,l2,sh2),b2⟩"
  and hC: "h2 a = Some(C,fs)" and cF_Static: "P ⊢ C has F,Static:t in D"
shows "P ⊢ ⟨e1∙F{D}:=e2, s0, b0⟩ →* ⟨THROW IncompatibleClassChangeError, (h2,l2,sh2), b2⟩"
(*<*)(is "(?x, ?z) ∈ (red P)*")
proof -
  let ?y = "(addr a∙F{D}:=e2, s1, b1)"
  let ?y' = "(addr a∙F{D}:=Val v::expr,(h2,l2,sh2),b2)"
  have "(?x, ?y) ∈ (red P)*" by(rule FAssReds1[OF e1_steps])
  also have "(?y, ?y') ∈ (red P)*" by(rule FAssReds2[OF e2_steps])
  also have "(?y', ?z) ∈ (red P)"
    using RedFAssStatic[OF _ cF_Static] hC by simp
  ultimately show ?thesis by simp
qed
(*>*)

subsubsection "SFAss"

lemma SFAssReds:
  "P ⊢ ⟨e,s,b⟩ →* ⟨e',s',b'⟩ ⟹ P ⊢ ⟨C∙sF{D}:=e,s,b⟩ →* ⟨C∙sF{D}:=e',s',b'⟩"
(*<*)
proof(induct rule: rtrancl_induct3)
  case refl show ?case by blast
next
  case step show ?case
   by(rule rtrancl_into_rtrancl[OF step(3) SFAssRed[OF step(2)]])
qed
(*>*)

lemma SFAssRedsVal:
assumes e2_steps: "P ⊢ ⟨e2,s0,b0⟩ →* ⟨Val v,(h2,l2,sh2),b2⟩"
  and cF: "P ⊢ C has F,Static:t in D"
  and shD: "sh2 D = ⌊(sfs,Done)⌋"
shows "P ⊢ ⟨C∙sF{D}:=e2, s0, b0⟩ →* ⟨unit, (h2,l2,sh2(D↦(sfs(F↦v), Done))),False⟩"
(*<*)(is "(?a, ?c) ∈ (red P)*")
proof -
  let ?b = "(C∙sF{D}:=Val v::expr, (h2,l2,sh2), b2)"
  have "(?a, ?b) ∈ (red P)*" by(rule SFAssReds[OF e2_steps])
  also have "(?b, ?c) ∈ (red P)*" proof(cases b2)
    case True
    then show ?thesis
      using RedSFAss[THEN r_into_rtrancl, OF cF] shD by simp
  next
    case False
    let ?b' = "(C∙sF{D}:=Val v::expr, (h2,l2,sh2), True)"
    have "(?b, ?b') ∈ (red P)*"
      using False SFAssInitDoneRed[THEN converse_rtrancl_into_rtrancl, OF cF] shD
        by simp
    also have "(?b', ?c) ∈ (red P)*"
      using RedSFAss[THEN r_into_rtrancl, OF cF] shD by simp
    ultimately show ?thesis by simp
  qed
  ultimately show ?thesis by simp
qed
(*>*)

lemma SFAssRedsThrow:
  "⟦ P ⊢ ⟨e2,s0,b0⟩ →* ⟨throw e,s2,b2⟩ ⟧
  ⟹ P ⊢ ⟨C∙sF{D}:=e2,s0,b0⟩ →* ⟨throw e,s2,b2⟩"
(*<*)by(rule SFAssReds[THEN rtrancl_into_rtrancl, OF _ red_reds.SFAssThrow])(*>*)

lemma SFAssRedsNone:
  "⟦ P ⊢ ⟨e2,s0,b0⟩ →* ⟨Val v,(h2,l2,sh2),b2⟩;
     ¬(∃b t. P ⊢ C has F,b:t in D) ⟧ ⟹
  P ⊢ ⟨C∙sF{D}:=e2,s0,b0⟩ →* ⟨THROW NoSuchFieldError, (h2,l2,sh2),False⟩"
(*<*)by(rule SFAssReds[THEN rtrancl_into_rtrancl, OF _ RedSFAssNone])(*>*)

lemma SFAssRedsNonStatic:
  "⟦ P ⊢ ⟨e2,s0,b0⟩ →* ⟨Val v,(h2,l2,sh2),b2⟩;
     P ⊢ C has F,NonStatic:t in D ⟧ ⟹
  P ⊢ ⟨C∙sF{D}:=e2,s0,b0⟩ →* ⟨THROW IncompatibleClassChangeError,(h2,l2,sh2),False⟩"
(*<*)by(rule SFAssReds[THEN rtrancl_into_rtrancl, OF _ RedSFAssNonStatic])(*>*)

lemma SFAssInitReds:
assumes e2_steps: "P ⊢ ⟨e2,s0,b0⟩ →* ⟨Val v,(h2,l2,sh2),False⟩"
  and cF: "P ⊢ C has F,Static:t in D"
  and nDone: "∄sfs. sh2 D = Some (sfs, Done)"
  and INIT_steps: "P ⊢ ⟨INIT D ([D],False) ← unit,(h2,l2,sh2),False⟩ →* ⟨Val v',(h',l',sh'),b'⟩"
  and sh'D: "sh' D = Some(sfs,i)"
  and sfs': "sfs' = sfs(F↦v)" and sh'': "sh'' = sh'(D↦(sfs',i))"
shows "P ⊢ ⟨C∙sF{D}:=e2,s0,b0⟩ →* ⟨unit,(h',l',sh''),False⟩"
(*<*)(is "(?x, ?z) ∈ (red P)*")
proof -
  let ?y = "(C∙sF{D} := Val v::expr,(h2, l2, sh2),False)"
  let ?y' = "(INIT D ([D],False) ← C∙sF{D} := Val v::expr,(h2, l2, sh2),False)"
  let ?y'' = "(C∙sF{D} := Val v::expr,(h', l', sh'),icheck P D (C∙sF{D} := Val v::expr))"
  have icheck: "icheck P D (C∙sF{D} := Val v::expr)" using cF by fastforce
  then have y''z: "(?y'',?z) ∈ (red P)"
    using RedSFAss[OF cF _ sfs' sh''] sh'D by simp
  have "(?x, ?y) ∈ (red P)*" by(rule SFAssReds[OF e2_steps])
  also have "(?y, ?y') ∈ (red P)*"
    using SFAssInitRed[THEN converse_rtrancl_into_rtrancl, OF cF] nDone
      by simp
  also have "(?y', ?z) ∈ (red P)*"
    using InitSeqReds[OF INIT_steps y''z[THEN r_into_rtrancl]] by simp
  ultimately show ?thesis by simp
qed
(*>*)

lemma SFAssInitThrowReds:
assumes e2_steps: "P ⊢ ⟨e2,s0,b0⟩ →* ⟨Val v,(h2,l2,sh2),False⟩"
  and cF: "P ⊢ C has F,Static:t in D"
  and nDone: "∄sfs. sh2 D = Some (sfs, Done)"
  and INIT_steps: "P ⊢ ⟨INIT D ([D],False) ← unit,(h2,l2,sh2),False⟩ →* ⟨throw a,s',b'⟩"
shows "P ⊢ ⟨C∙sF{D}:=e2,s0,b0⟩ →* ⟨throw a,s',b'⟩"
(*<*)(is "(?x, ?z) ∈ (red P)*")
proof -
  let ?y = "(C∙sF{D} := Val v::expr,(h2, l2, sh2),False)"
  let ?y' = "(INIT D ([D],False) ← C∙sF{D} := Val v::expr,(h2, l2, sh2),False)"
  have "(?x, ?y) ∈ (red P)*" by(rule SFAssReds[OF e2_steps])
  also have "(?y, ?y') ∈ (red P)*"
    using SFAssInitRed[THEN converse_rtrancl_into_rtrancl, OF cF] nDone
      by simp
  also have "(?y', ?z) ∈ (red P)*"
    using InitSeqThrowReds[OF INIT_steps] by simp
  ultimately show ?thesis by simp
qed
(*>*)

subsubsection";;"

lemma  SeqReds:
  "P ⊢ ⟨e,s,b⟩ →* ⟨e',s',b'⟩ ⟹ P ⊢ ⟨e;;e2, s,b⟩ →* ⟨e';;e2, s',b'⟩"
(*<*)
proof(induct rule: rtrancl_induct3)
  case refl show ?case by blast
next
  case step show ?case
   by(rule rtrancl_into_rtrancl[OF step(3) SeqRed[OF step(2)]])
qed
(*>*)

lemma SeqRedsThrow:
  "P ⊢ ⟨e,s,b⟩ →* ⟨throw e',s',b'⟩ ⟹ P ⊢ ⟨e;;e2, s,b⟩ →* ⟨throw e', s',b'⟩"
(*<*)by(rule SeqReds[THEN rtrancl_into_rtrancl, OF _ red_reds.SeqThrow])(*>*)

lemma SeqReds2:
assumes e1_steps: "P ⊢ ⟨e1,s0,b0⟩ →* ⟨Val v1,s1,b1⟩"
  and   e2_steps: "P ⊢ ⟨e2,s1,b1⟩ →* ⟨e2',s2,b2⟩"
shows "P ⊢ ⟨e1;;e2, s0,b0⟩ →* ⟨e2',s2,b2⟩"
(*<*)(is "(?x, ?z) ∈ (red P)*")
proof -
  let ?y = "(Val v1;; e2,s1,b1)"
  have "(?x, ?y) ∈ (red P)*" by(rule SeqReds[OF e1_steps])
  also have "(?y, ?z) ∈ (red P)*"
    by(rule RedSeq[THEN converse_rtrancl_into_rtrancl, OF e2_steps])
  ultimately show ?thesis by simp
qed
(*>*)


subsubsection"If"

lemma CondReds:
  "P ⊢ ⟨e,s,b⟩ →* ⟨e',s',b'⟩ ⟹ P ⊢ ⟨if (e) e1 else e2,s,b⟩ →* ⟨if (e') e1 else e2,s',b'⟩"
(*<*)
proof(induct rule: rtrancl_induct3)
  case refl show ?case by blast
next
  case step show ?case
   by(rule rtrancl_into_rtrancl[OF step(3) CondRed[OF step(2)]])
qed
(*>*)

lemma CondRedsThrow:
  "P ⊢ ⟨e,s,b⟩ →* ⟨throw a,s',b'⟩ ⟹ P ⊢ ⟨if (e) e1 else e2, s,b⟩ →* ⟨throw a,s',b'⟩"
(*<*)by(rule CondReds[THEN rtrancl_into_rtrancl, OF _ red_reds.CondThrow])(*>*)

lemma CondReds2T:
assumes e_steps: "P ⊢ ⟨e,s0,b0⟩ →* ⟨true,s1,b1⟩"
  and   e1_steps: "P ⊢ ⟨e1, s1,b1⟩ →* ⟨e',s2,b2⟩"
shows "P ⊢ ⟨if (e) e1 else e2, s0,b0⟩ →* ⟨e',s2,b2⟩"
(*<*)(is "(?x, ?z) ∈ (red P)*")
proof -
  let ?y = "(if (true) e1 else e2,s1,b1)"
  have "(?x, ?y) ∈ (red P)*" by(rule CondReds[OF e_steps])
  also have "(?y, ?z) ∈ (red P)*"
    by(rule RedCondT[THEN converse_rtrancl_into_rtrancl, OF e1_steps])
  ultimately show ?thesis by simp
qed
(*>*)

lemma CondReds2F:
assumes e_steps: "P ⊢ ⟨e,s0,b0⟩ →* ⟨false,s1,b1⟩"
  and   e2_steps: "P ⊢ ⟨e2, s1,b1⟩ →* ⟨e',s2,b2⟩"
shows "P ⊢ ⟨if (e) e1 else e2, s0,b0⟩ →* ⟨e',s2,b2⟩"
(*<*)(is "(?x, ?z) ∈ (red P)*")
proof -
  let ?y = "(if (false) e1 else e2,s1,b1)"
  have "(?x, ?y) ∈ (red P)*" by(rule CondReds[OF e_steps])
  also have "(?y, ?z) ∈ (red P)*"
    by(rule RedCondF[THEN converse_rtrancl_into_rtrancl, OF e2_steps])
  ultimately show ?thesis by simp
qed
(*>*)


subsubsection "While"

lemma WhileFReds:
assumes b_steps: "P ⊢ ⟨b,s,b0⟩ →* ⟨false,s',b'⟩"
shows "P ⊢ ⟨while (b) c,s,b0⟩ →* ⟨unit,s',b'⟩"
(*<*)
by(rule RedWhile[THEN converse_rtrancl_into_rtrancl,
                 OF CondReds[THEN rtrancl_into_rtrancl,
                             OF b_steps RedCondF]])
(*>*)

lemma WhileRedsThrow:
assumes b_steps: "P ⊢ ⟨b,s,b0⟩ →* ⟨throw e,s',b'⟩"
shows "P ⊢ ⟨while (b) c,s,b0⟩ →* ⟨throw e,s',b'⟩"
(*<*)
by(rule RedWhile[THEN converse_rtrancl_into_rtrancl,
                 OF CondReds[THEN rtrancl_into_rtrancl,
                             OF b_steps red_reds.CondThrow]])
(*>*)

lemma WhileTReds:
assumes b_steps: "P ⊢ ⟨b,s0,b0⟩ →* ⟨true,s1,b1⟩"
    and c_steps: "P ⊢ ⟨c,s1,b1⟩ →* ⟨Val v1,s2,b2⟩"
    and while_steps: "P ⊢ ⟨while (b) c,s2,b2⟩ →* ⟨e,s3,b3⟩"
shows "P ⊢ ⟨while (b) c,s0,b0⟩ →* ⟨e,s3,b3⟩"
(*<*)(is "(?a, ?c) ∈ (red P)*")
proof -
  let ?b = "(if (b) (c;; while (b) c) else unit,s0,b0)"
  let ?y = "(if (true) (c;; while (b) c) else unit,s1,b1)"
  let ?b' = "(c;; while (b) c,s1,b1)"
  let ?y' = "(Val v1;; while (b) c,s2,b2)"
  have "(?a, ?b) ∈ (red P)*"
    using RedWhile[THEN converse_rtrancl_into_rtrancl] by simp
  also have "(?b, ?y) ∈ (red P)*" by(rule CondReds[OF b_steps])
  also have "(?y, ?b') ∈ (red P)*"
    using RedCondT[THEN converse_rtrancl_into_rtrancl] by simp
  also have "(?b', ?y') ∈ (red P)*" by(rule SeqReds[OF c_steps])
  also have "(?y', ?c) ∈ (red P)*"
    by(rule RedSeq[THEN converse_rtrancl_into_rtrancl, OF while_steps])
  ultimately show ?thesis by simp
qed
(*>*)

lemma WhileTRedsThrow:
assumes b_steps: "P ⊢ ⟨b,s0,b0⟩ →* ⟨true,s1,b1⟩"
    and c_steps: "P ⊢ ⟨c,s1,b1⟩ →* ⟨throw e,s2,b2⟩"
shows "P ⊢ ⟨while (b) c,s0,b0⟩ →* ⟨throw e,s2,b2⟩"
(*<*)(is "(?a, ?c) ∈ (red P)*")
proof -
  let ?b = "(if (b) (c;; while (b) c) else unit,s0,b0)"
  let ?y = "(if (true) (c;; while (b) c) else unit,s1,b1)"
  let ?b' = "(c;; while (b) c,s1,b1)"
  let ?y' = "(throw e;; while (b) c,s2,b2)"
  have "(?a, ?b) ∈ (red P)*"
    using RedWhile[THEN converse_rtrancl_into_rtrancl] by simp
  also have "(?b, ?y) ∈ (red P)*" by(rule CondReds[OF b_steps])
  also have "(?y, ?b') ∈ (red P)*"
    using RedCondT[THEN converse_rtrancl_into_rtrancl] by simp
  also have "(?b', ?y') ∈ (red P)*" by(rule SeqReds[OF c_steps])
  also have "(?y', ?c) ∈ (red P)" by(rule red_reds.SeqThrow)
  ultimately show ?thesis by simp
qed
(*>*)

subsubsection"Throw"

lemma ThrowReds:
  "P ⊢ ⟨e,s,b⟩ →* ⟨e',s',b'⟩ ⟹ P ⊢ ⟨throw e,s,b⟩ →* ⟨throw e',s',b'⟩"
(*<*)
proof(induct rule: rtrancl_induct3)
  case refl show ?case by blast
next
  case step show ?case
   by(rule rtrancl_into_rtrancl[OF step(3) ThrowRed[OF step(2)]])
qed
(*>*)

lemma ThrowRedsNull:
  "P ⊢ ⟨e,s,b⟩ →* ⟨null,s',b'⟩ ⟹ P ⊢ ⟨throw e,s,b⟩ →* ⟨THROW NullPointer,s',b'⟩"
(*<*)by(rule ThrowReds[THEN rtrancl_into_rtrancl, OF _ RedThrowNull])(*>*)

lemma ThrowRedsThrow:
  "P ⊢ ⟨e,s,b⟩ →* ⟨throw a,s',b'⟩ ⟹ P ⊢ ⟨throw e,s,b⟩ →* ⟨throw a,s',b'⟩"
(*<*)by(rule ThrowReds[THEN rtrancl_into_rtrancl, OF _ red_reds.ThrowThrow])(*>*)

subsubsection "InitBlock"

lemma InitBlockReds_aux:
  "P ⊢ ⟨e,s,b⟩ →* ⟨e',s',b'⟩ ⟹
  ∀h l sh h' l' sh' v. s = (h,l(V↦v),sh) ⟶ s' = (h',l',sh') ⟶
  P ⊢ ⟨{V:T := Val v; e},(h,l,sh),b⟩ →* ⟨{V:T := Val(the(l' V)); e'},(h',l'(V:=(l V)),sh'),b'⟩"
(*<*)
proof(induct rule: converse_rtrancl_induct3)
  case refl then show ?case
    by(fastforce simp: fun_upd_same simp del:fun_upd_apply)
next
  case (step e0 s0 b0 e1 s1 b1)
  obtain h1 l1 sh1 where s1[simp]: "s1 = (h1, l1, sh1)" by(cases s1) simp
  { fix h0 l0 sh0 h2 l2 sh2 v0
    assume [simp]: "s0 = (h0, l0(V ↦ v0), sh0)" and s'[simp]: "s' = (h2, l2, sh2)"    
    then have "V ∈ dom l1" using step(1) by(auto dest!: red_lcl_incr)
    then obtain v1 where l1V[simp]: "l1 V = ⌊v1⌋" by blast

    let ?a = "({V:T; V:=Val v0;; e0},(h0, l0, sh0),b0)"
    let ?b = "({V:T; V:=Val v1;; e1},(h1, l1(V := l0 V), sh1),b1)"
    let ?c = "({V:T; V:=Val (the (l2 V));; e'},(h2, l2(V := l0 V), sh2),b')"
    let ?l = "l1(V := l0 V)" and ?v = v1

    have e0_steps: "P ⊢ ⟨e0,(h0, l0(V ↦ v0), sh0),b0⟩ → ⟨e1,(h1, l1, sh1),b1⟩"
      using step(1) by simp

    have lv: "⋀l v. l1 = l(V ↦ v) ⟶
             P ⊢ ⟨{V:T; V:=Val v;; e1},(h1, l, sh1),b1⟩ →*
                  ⟨{V:T; V:=Val (the (l2 V));; e'},(h2, l2(V := l V), sh2),b'⟩"
      using step(3) s' s1 by blast
    moreover have "l1 = ?l(V ↦ ?v)" by(rule ext) (simp add:fun_upd_def)
    ultimately have "(?b, ?c) ∈ (red P)*" using lv[of ?l ?v] by simp
    then have "(?a, ?c) ∈ (red P)*"
      by(rule InitBlockRed[THEN converse_rtrancl_into_rtrancl, OF e0_steps l1V])
  }
  then show ?case by blast
qed
(*>*)

lemma InitBlockReds:
 "P ⊢ ⟨e, (h,l(V↦v),sh),b⟩ →* ⟨e', (h',l',sh'),b'⟩ ⟹
  P ⊢ ⟨{V:T := Val v; e}, (h,l,sh),b⟩ →* ⟨{V:T := Val(the(l' V)); e'}, (h',l'(V:=(l V)),sh'),b'⟩"
(*<*)by(blast dest:InitBlockReds_aux)(*>*)

lemma InitBlockRedsFinal:
  "⟦ P ⊢ ⟨e,(h,l(V↦v),sh),b⟩ →* ⟨e',(h',l',sh'),b'⟩; final e' ⟧ ⟹
  P ⊢ ⟨{V:T := Val v; e},(h,l,sh),b⟩ →* ⟨e',(h', l'(V := l V),sh'),b'⟩"
(*<*)
by(fast elim!:InitBlockReds[THEN rtrancl_into_rtrancl] finalE
        intro:RedInitBlock InitBlockThrow)
(*>*)


subsubsection "Block"

lemmas converse_rtranclE3 = converse_rtranclE [of "(xa,xb,xc)" "(za,zb,zc)", split_rule]

lemma BlockRedsFinal:
assumes reds: "P ⊢ ⟨e0,s0,b0⟩ →* ⟨e2,(h2,l2,sh2),b2⟩" and fin: "final e2"
shows "⋀h0 l0 sh0. s0 = (h0,l0(V:=None),sh0) ⟹ P ⊢ ⟨{V:T; e0},(h0,l0,sh0),b0⟩ →* ⟨e2,(h2,l2(V:=l0 V),sh2),b2⟩"
(*<*)
using reds
proof (induct rule:converse_rtrancl_induct3)
  case refl thus ?case
    by(fastforce intro:finalE[OF fin] RedBlock BlockThrow
                simp del:fun_upd_apply)
next
  case (step e0 s0 b0 e1 s1 b1)
  have red: "P ⊢ ⟨e0,s0,b0⟩ → ⟨e1,s1,b1⟩"
   and reds: "P ⊢ ⟨e1,s1,b1⟩ →* ⟨e2,(h2,l2,sh2),b2⟩"
   and IH: "⋀h l sh. s1 = (h,l(V := None),sh)
                ⟹ P ⊢ ⟨{V:T; e1},(h,l,sh),b1⟩ →* ⟨e2,(h2, l2(V := l V),sh2),b2⟩"
   and s0: "s0 = (h0, l0(V := None),sh0)" by fact+
  obtain h1 l1 sh1 where s1: "s1 = (h1,l1,sh1)"
    using prod_cases3 by blast
  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 have e1: "e1 = unit;;e" and s1: "s1 = (h0, l0(V ↦ v),sh0)" and b1: "b1 = b0"
      by auto
    from e1 fin have "e1 ≠ e2" by (auto simp:final_def)
    then obtain e' s' b' where red1: "P ⊢ ⟨e1,s1,b1⟩ → ⟨e',s',b'⟩"
      and reds': "P ⊢ ⟨e',s',b'⟩ →* ⟨e2,(h2,l2,sh2),b2⟩"
      using converse_rtranclE3[OF reds] by blast
    from red1 e1 b1 have es': "e' = e" "s' = s1" "b' = b0" by auto
    show ?case using e0 s1 es' reds'
      by(auto intro!: InitBlockRedsFinal[OF _ fin] simp del:fun_upd_apply)
  next
    assume unass: "¬ assigned V e0"
    show ?thesis
    proof (cases "l1 V")
      assume None: "l1 V = None"
      hence "P ⊢ ⟨{V:T; e0},(h0,l0,sh0),b0⟩ → ⟨{V:T; e1},(h1, l1(V := l0 V),sh1),b1⟩"
        using s0 s1 red by(simp add: BlockRedNone[OF _ _ unass])
      moreover
      have "P ⊢ ⟨{V:T; e1},(h1, l1(V := l0 V),sh1),b1⟩ →* ⟨e2,(h2, l2(V := l0 V),sh2),b2⟩"
        using IH[of _ "l1(V := l0 V)"] s1 None by(simp add:fun_upd_idem)
      ultimately show ?case by(rule converse_rtrancl_into_rtrancl)
    next
      fix v assume Some: "l1 V = Some v"
      hence "P ⊢ ⟨{V:T;e0},(h0,l0,sh0),b0⟩ → ⟨{V:T := Val v; e1},(h1,l1(V := l0 V),sh1),b1⟩"
        using s0 s1 red by(simp add: BlockRedSome[OF _ _ unass])
      moreover
      have "P ⊢ ⟨{V:T := Val v; e1},(h1,l1(V:= l0 V),sh1),b1⟩ →*
                ⟨e2,(h2,l2(V:=l0 V),sh2),b2⟩"
        using InitBlockRedsFinal[OF _ fin,of _ _ "l1(V:=l0 V)" V]
              Some reds s1 by(simp add:fun_upd_idem)
      ultimately show ?case by(rule converse_rtrancl_into_rtrancl)
    qed
  qed
qed
(*>*)


subsubsection "try-catch"

lemma TryReds:
  "P ⊢ ⟨e,s,b⟩ →* ⟨e',s',b'⟩ ⟹ P ⊢ ⟨try e catch(C V) e2,s,b⟩ →* ⟨try e' catch(C V) e2,s',b'⟩"
(*<*)
proof(induct rule: rtrancl_induct3)
  case refl show ?case by blast
next
  case step show ?case
   by(rule rtrancl_into_rtrancl[OF step(3) TryRed[OF step(2)]])
qed
(*>*)

lemma TryRedsVal:
  "P ⊢ ⟨e,s,b⟩ →* ⟨Val v,s',b'⟩ ⟹ P ⊢ ⟨try e catch(C V) e2,s,b⟩ →* ⟨Val v,s',b'⟩"
(*<*)by(rule TryReds[THEN rtrancl_into_rtrancl, OF _ RedTry])(*>*)

lemma TryCatchRedsFinal:
assumes e1_steps: "P ⊢ ⟨e1,s0,b0⟩ →* ⟨Throw a,(h1,l1,sh1),b1⟩"
  and h1a: "h1 a = Some(D,fs)" and sub: "P ⊢ D ≼* C"
  and e2_steps: "P ⊢ ⟨e2, (h1, l1(V ↦ Addr a),sh1),b1⟩ →* ⟨e2', (h2,l2,sh2), b2⟩"
  and final: "final e2'"
shows "P ⊢ ⟨try e1 catch(C V) e2, s0, b0⟩ →* ⟨e2', (h2, (l2::locals)(V := l1 V),sh2),b2⟩"
(*<*)(is "(?x, ?z) ∈ (red P)*")
proof -
  let ?y = "(try Throw a catch(C V) e2,(h1, l1, sh1),b1)"
  let ?b = "({V:Class C; V:=addr a;; e2},(h1, l1, sh1),b1)"
  have bz: "(?b, ?z) ∈ (red P)*"
    by(rule InitBlockRedsFinal[OF e2_steps final])
  have hp: "hp (h1, l1, sh1) a = ⌊(D, fs)⌋" using h1a by simp
  have "(?x, ?y) ∈ (red P)*" by(rule TryReds[OF e1_steps])
  also have "(?y, ?z) ∈ (red P)*"
    by(rule RedTryCatch[THEN converse_rtrancl_into_rtrancl, OF hp sub bz])
  ultimately show ?thesis by simp
qed
(*>*)

lemma TryRedsFail:
  "⟦ P ⊢ ⟨e1,s,b⟩ →* ⟨Throw a,(h,l,sh),b'⟩; h a = Some(D,fs); ¬ P ⊢ D ≼* C ⟧
  ⟹ P ⊢ ⟨try e1 catch(C V) e2,s,b⟩ →* ⟨Throw a,(h,l,sh),b'⟩"
(*<*)by(fastforce intro!: TryReds[THEN rtrancl_into_rtrancl, OF _ RedTryFail])(*>*)

subsubsection "List"

lemma ListReds1:
  "P ⊢ ⟨e,s,b⟩ →* ⟨e',s',b'⟩ ⟹ P ⊢ ⟨e#es,s,b⟩ [→]* ⟨e' # es,s',b'⟩"
(*<*)
proof(induct rule: rtrancl_induct3)
  case refl show ?case by blast
next
  case step show ?case
   by(rule rtrancl_into_rtrancl[OF step(3) ListRed1[OF step(2)]])
qed
(*>*)

lemma ListReds2:
  "P ⊢ ⟨es,s,b⟩ [→]* ⟨es',s',b'⟩ ⟹ P ⊢ ⟨Val v # es,s,b⟩ [→]* ⟨Val v # es',s',b'⟩"
(*<*)
proof(induct rule: rtrancl_induct3)
  case refl show ?case by blast
next
  case step show ?case
   by(rule rtrancl_into_rtrancl[OF step(3) ListRed2[OF step(2)]])
qed
(*>*)

lemma ListRedsVal:
  "⟦ P ⊢ ⟨e,s0,b0⟩ →* ⟨Val v,s1,b1⟩; P ⊢ ⟨es,s1,b1⟩ [→]* ⟨es',s2,b2⟩ ⟧
  ⟹ P ⊢ ⟨e#es,s0,b0⟩ [→]* ⟨Val v # es',s2,b2⟩"
(*<*)by(rule rtrancl_trans[OF ListReds1 ListReds2])(*>*)

subsubsection"Call"

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

lemma assumes wf: "wwf_J_prog P"
shows Red_fv: "P ⊢ ⟨e,(h,l,sh),b⟩ → ⟨e',(h',l',sh'),b'⟩ ⟹ fv e' ⊆ fv e"
  and  "P ⊢ ⟨es,(h,l,sh),b⟩ [→] ⟨es',(h',l',sh'),b'⟩ ⟹ fvs es' ⊆ fvs es"
(*<*)
proof (induct rule:red_reds_inducts)
  case (RedCall h a C fs M Ts T pns body D vs l sh b)
  hence "fv body ⊆ {this} ∪ set pns"
    using assms by(fastforce dest!:sees_wf_mdecl simp:wf_mdecl_def)
  with RedCall.hyps show ?case by fastforce
next
  case (RedSCall C M Ts T pns body D vs)
  hence "fv body ⊆ set pns"
    using assms by(fastforce dest!:sees_wf_mdecl simp:wf_mdecl_def)
  with RedSCall.hyps show ?case by fastforce
qed auto
(*>*)


lemma Red_dom_lcl:
  "P ⊢ ⟨e,(h,l,sh),b⟩ → ⟨e',(h',l',sh'),b'⟩ ⟹ dom l' ⊆ dom l ∪ fv e" and
  "P ⊢ ⟨es,(h,l,sh),b⟩ [→] ⟨es',(h',l',sh'),b'⟩ ⟹ 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:
assumes wf: "wwf_J_prog P"
shows "P ⊢ ⟨e,(h,l,sh),b⟩ →* ⟨e',(h',l',sh'),b'⟩ ⟹ dom l' ⊆ dom l ∪ fv e"
(*<*)
proof(induct rule: converse_rtrancl_induct_red)
  case 1 then show ?case by blast
next
  case 2 then show ?case using wf by(blast dest: Red_fv Red_dom_lcl)
qed
(*>*)

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)"
(*<*)by(rule ext) (simp add:override_on_def)

declare fun_upd_apply[simp del] map_upds_twist[simp del]
(*>*)


lemma blocksReds:
  "⋀l. ⟦ length Vs = length Ts; length vs = length Ts; distinct Vs;
         P ⊢ ⟨e, (h,l(Vs [↦] vs),sh),b⟩ →* ⟨e', (h',l',sh'),b'⟩ ⟧
        ⟹ P ⊢ ⟨blocks(Vs,Ts,vs,e), (h,l,sh),b⟩ →* ⟨blocks(Vs,Ts,map (the ∘ l') Vs,e'), (h',override_on l' l (set Vs),sh'),b'⟩"
(*<*)
proof(induct Vs Ts vs e rule:blocks_induct)
  case (1 V Vs T Ts v vs e) show ?case
    using InitBlockReds[OF "1.hyps"[of "l(V↦v)"]] "1.prems"
    by(auto simp:override_on_upd_lemma)
qed auto
(*>*)


lemma blocksFinal:
 "⋀l. ⟦ length Vs = length Ts; length vs = length Ts; final e ⟧ ⟹
       P ⊢ ⟨blocks(Vs,Ts,vs,e), (h,l,sh),b⟩ →* ⟨e, (h,l,sh),b⟩"
(*<*)
proof(induct Vs Ts vs e rule:blocks_induct)
  case 1
  show ?case using "1.prems" InitBlockReds[OF "1.hyps"]
    by(fastforce elim!:finalE elim: rtrancl_into_rtrancl[OF _ RedInitBlock]
                                   rtrancl_into_rtrancl[OF _ InitBlockThrow])
qed auto
(*>*)


lemma blocksRedsFinal:
assumes wf: "length Vs = length Ts" "length vs = length Ts" "distinct Vs"
    and reds: "P ⊢ ⟨e, (h,l(Vs [↦] vs),sh),b⟩ →* ⟨e', (h',l',sh'),b'⟩"
    and fin: "final e'" and l'': "l'' = override_on l' l (set Vs)"
shows "P ⊢ ⟨blocks(Vs,Ts,vs,e), (h,l,sh),b⟩ →* ⟨e', (h',l'',sh'),b'⟩"
(*<*)
proof -
  let ?bv = "blocks(Vs,Ts,map (the o l') Vs,e')"
  have "P ⊢ ⟨blocks(Vs,Ts,vs,e), (h,l,sh),b⟩ →* ⟨?bv, (h',l'',sh'),b'⟩"
    using l'' by simp (rule blocksReds[OF wf reds])
  also have "P ⊢ ⟨?bv, (h',l'',sh'),b'⟩ →* ⟨e', (h',l'',sh'),b'⟩"
    using wf by(fastforce intro:blocksFinal fin)
  finally show ?thesis .
qed
(*>*)

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

lemma CallRedsObj:
 "P ⊢ ⟨e,s,b⟩ →* ⟨e',s',b'⟩ ⟹ P ⊢ ⟨e∙M(es),s,b⟩ →* ⟨e'∙M(es),s',b'⟩"
(*<*)
proof(induct rule: rtrancl_induct3)
  case refl show ?case by blast
next
  case step show ?case
   by(rule rtrancl_into_rtrancl[OF step(3) CallObj[OF step(2)]])
qed
(*>*)


lemma CallRedsParams:
 "P ⊢ ⟨es,s,b⟩ [→]* ⟨es',s',b'⟩ ⟹ P ⊢ ⟨(Val v)∙M(es),s,b⟩ →* ⟨(Val v)∙M(es'),s',b'⟩"
(*<*)
proof(induct rule: rtrancl_induct3)
  case refl show ?case by blast
next
  case step show ?case
   by(rule rtrancl_into_rtrancl[OF step(3) CallParams[OF step(2)]])
qed
(*>*)


lemma CallRedsFinal:
assumes wwf: "wwf_J_prog P"
and "P ⊢ ⟨e,s0,b0⟩ →* ⟨addr a,s1,b1⟩"
      "P ⊢ ⟨es,s1,b1⟩ [→]* ⟨map Val vs,(h2,l2,sh2),b2⟩"
      "h2 a = Some(C,fs)" "P ⊢ C sees M,NonStatic:Ts→T = (pns,body) in D"
      "size vs = size pns"
and l2': "l2' = [this ↦ Addr a, pns[↦]vs]"
and body: "P ⊢ ⟨body,(h2,l2',sh2),b2⟩ →* ⟨ef,(h3,l3,sh3),b3⟩"
and "final ef"
shows "P ⊢ ⟨e∙M(es), s0,b0⟩ →* ⟨ef,(h3,l2,sh3),b3⟩"
(*<*)
proof -
  have wf: "size Ts = size pns ∧ distinct pns ∧ this ∉ set pns"
    and wt: "fv body ⊆ {this} ∪ set pns"
    using assms by(fastforce dest!:sees_wf_mdecl simp:wf_mdecl_def)+
  from body[THEN Red_lcl_add, of l2]
  have body': "P ⊢ ⟨body,(h2,l2(this↦ Addr a, pns[↦]vs),sh2),b2⟩ →* ⟨ef,(h3,l2++l3,sh3),b3⟩"
    by (simp add:l2')
  have "dom l3 ⊆ {this} ∪ set pns"
    using Reds_dom_lcl[OF wwf body] wt l2' set_take_subset by force
  hence eql2: "override_on (l2++l3) l2 ({this} ∪ set pns) = l2"
    by(fastforce simp add:map_add_def override_on_def fun_eq_iff)
  have "P ⊢ ⟨e∙M(es),s0,b0⟩ →* ⟨(addr a)∙M(es),s1,b1⟩" by(rule CallRedsObj)(rule assms(2))
  also have "P ⊢ ⟨(addr a)∙M(es),s1,b1⟩ →*
                 ⟨(addr a)∙M(map Val vs),(h2,l2,sh2),b2⟩"
    by(rule CallRedsParams)(rule assms(3))
  also have "P ⊢ ⟨(addr a)∙M(map Val vs), (h2,l2,sh2),b2⟩ →
                 ⟨blocks(this#pns, Class D#Ts, Addr a#vs, body), (h2,l2,sh2),b2⟩"
    by(rule RedCall)(auto simp: assms wf, rule assms(5))
  also (rtrancl_into_rtrancl) have "P ⊢ ⟨blocks(this#pns, Class D#Ts, Addr a#vs, body), (h2,l2,sh2),b2⟩
                 →* ⟨ef,(h3,override_on (l2++l3) l2 ({this} ∪ set pns),sh3),b3⟩"
    by(rule blocksRedsFinal, insert assms wf body', simp_all)
  finally show ?thesis using eql2 by simp
qed
(*>*)


lemma CallRedsThrowParams:
assumes e_steps: "P ⊢ ⟨e,s0,b0⟩ →* ⟨Val v,s1,b1⟩"
  and es_steps: "P ⊢ ⟨es,s1,b1⟩ [→]* ⟨map Val vs1 @ throw a # es2,s2,b2⟩"
shows "P ⊢ ⟨e∙M(es),s0,b0⟩ →* ⟨throw a,s2,b2⟩"
(*<*)(is "(?x, ?z) ∈ (red P)*")
proof -
  let ?y = "(Val v∙M(es),s1,b1)"
  let ?y' = "(Val v∙M(map Val vs1 @ throw a # es2),s2,b2)"
  have "(?x, ?y) ∈ (red P)*" by(rule CallRedsObj[OF e_steps])
  also have "(?y, ?y') ∈ (red P)*" by(rule CallRedsParams[OF es_steps])
  also have "(?y', ?z) ∈ (red P)*" using CallThrowParams by fast
  ultimately show ?thesis by simp
qed
(*>*)


lemma CallRedsThrowObj:
  "P ⊢ ⟨e,s0,b0⟩ →* ⟨throw a,s1,b1⟩ ⟹ P ⊢ ⟨e∙M(es),s0,b0⟩ →* ⟨throw a,s1,b1⟩"
(*<*)by(rule CallRedsObj[THEN rtrancl_into_rtrancl, OF _ CallThrowObj])(*>*)


lemma CallRedsNull:
assumes e_steps: "P ⊢ ⟨e,s0,b0⟩ →* ⟨null,s1,b1⟩"
  and es_steps: "P ⊢ ⟨es,s1,b1⟩ [→]* ⟨map Val vs,s2,b2⟩"
shows "P ⊢ ⟨e∙M(es),s0,b0⟩ →* ⟨THROW NullPointer,s2,b2⟩"
(*<*)(is "(?x, ?z) ∈ (red P)*")
proof -
  let ?y = "(null∙M(es),s1,b1)"
  let ?y' = "(null∙M(map Val vs),s2,b2)"
  have "(?x, ?y) ∈ (red P)*" by(rule CallRedsObj[OF e_steps])
  also have "(?y, ?y') ∈ (red P)*" by(rule CallRedsParams[OF es_steps])
  also have "(?y', ?z) ∈ (red P)" by(rule RedCallNull)
  ultimately show ?thesis by simp
qed
(*>*)

lemma CallRedsNone:
assumes e_steps: "P ⊢ ⟨e,s,b⟩ →* ⟨addr a,s1,b1⟩"
  and es_steps: "P ⊢ ⟨es,s1,b1⟩ [→]* ⟨map Val vs,s2,b2⟩"
  and hp2a: "hp s2 a = Some(C,fs)"
  and ncM: "¬(∃b Ts T m D. P ⊢ C sees M,b:Ts→T = m in D)"
shows "P ⊢ ⟨e∙M(es),s,b⟩ →* ⟨THROW NoSuchMethodError,s2,b2⟩"
(*<*)(is "(?x, ?z) ∈ (red P)*")
proof -
  let ?y = "(addr a∙M(es),s1,b1)"
  let ?y' = "(addr a∙M(map Val vs),s2,b2)"
  have "(?x, ?y) ∈ (red P)*" by(rule CallRedsObj[OF e_steps])
  also have "(?y, ?y') ∈ (red P)*" by(rule CallRedsParams[OF es_steps])
  also have "(?y', ?z) ∈ (red P)" using RedCallNone[OF _ ncM] hp2a
    by(cases s2) simp
  ultimately show ?thesis by simp
qed
(*>*)

lemma CallRedsStatic:
assumes e_steps: "P ⊢ ⟨e,s,b⟩ →* ⟨addr a,s1,b1⟩"
  and es_steps: "P ⊢ ⟨es,s1,b1⟩ [→]* ⟨map Val vs,s2,b2⟩"
  and hp2a: "hp s2 a = Some(C,fs)"
  and cM_Static: "P ⊢ C sees M,Static:Ts→T = m in D"
shows "P ⊢ ⟨e∙M(es),s,b⟩ →* ⟨THROW IncompatibleClassChangeError,s2,b2⟩"
(*<*)(is "(?x, ?z) ∈ (red P)*")
proof -
  let ?y = "(addr a∙M(es),s1,b1)"
  let ?y' = "(addr a∙M(map Val vs),s2,b2)"
  have "(?x, ?y) ∈ (red P)*" by(rule CallRedsObj[OF e_steps])
  also have "(?y, ?y') ∈ (red P)*" by(rule CallRedsParams[OF es_steps])
  also have "(?y', ?z) ∈ (red P)" using RedCallStatic[OF _ cM_Static] hp2a
    by(cases s2) simp
  ultimately show ?thesis by simp
qed
(*>*)

subsection‹SCall›

lemma SCallRedsParams:
 "P ⊢ ⟨es,s,b⟩ [→]* ⟨es',s',b'⟩ ⟹ P ⊢ ⟨C∙sM(es),s,b⟩ →* ⟨C∙sM(es'),s',b'⟩"
(*<*)
proof(induct rule: rtrancl_induct3)
  case refl show ?case by blast
next
  case step show ?case
   by(rule rtrancl_into_rtrancl[OF step(3) SCallParams[OF step(2)]])
qed
(*>*)

lemma SCallRedsFinal:
assumes wwf: "wwf_J_prog P"
and "P ⊢ ⟨es,s0,b0⟩ [→]* ⟨map Val vs,(h2,l2,sh2),b2⟩"
      "P ⊢ C sees M,Static:Ts→T = (pns,body) in D"
      "sh2 D = Some(sfs,Done) ∨ (M = clinit ∧ sh2 D = ⌊(sfs, Processing)⌋)"
      "size vs = size pns"
and l2': "l2' = [pns[↦]vs]"
and body: "P ⊢ ⟨body,(h2,l2',sh2),False⟩ →* ⟨ef,(h3,l3,sh3),b3⟩"
and "final ef"
shows "P ⊢ ⟨C∙sM(es), s0,b0⟩ →* ⟨ef,(h3,l2,sh3),b3⟩"
(*<*)
proof -
  have wf: "size Ts = size pns ∧ distinct pns"
    and wt: "fv body ⊆ set pns"
    using assms by(fastforce dest!:sees_wf_mdecl simp:wf_mdecl_def)+
  from body[THEN Red_lcl_add, of l2]
  have body': "P ⊢ ⟨body,(h2,l2(pns[↦]vs),sh2),False⟩ →* ⟨ef,(h3,l2++l3,sh3),b3⟩"
    by (simp add:l2')
  have "dom l3 ⊆ set pns"
    using Reds_dom_lcl[OF wwf body] wt l2' set_take_subset by force
  hence eql2: "override_on (l2++l3) l2 (set pns) = l2"
    by(fastforce simp add:map_add_def override_on_def fun_eq_iff)
  have b2T: "P ⊢ ⟨C∙sM(map Val vs), (h2,l2,sh2),b2⟩ →* ⟨C∙sM(map Val vs), (h2,l2,sh2),True⟩"
  proof(cases b2)
    case True then show ?thesis by simp
  next
    case False then show ?thesis using assms(3,4) by(auto elim: SCallInitDoneRed)
  qed
  have "P ⊢ ⟨C∙sM(es),s0,b0⟩ →* ⟨C∙sM(map Val vs),(h2,l2,sh2),b2⟩"
    by(rule SCallRedsParams)(rule assms(2))
  also have "P ⊢ ⟨C∙sM(map Val vs), (h2,l2,sh2),b2⟩ →* ⟨blocks(pns, Ts, vs, body), (h2,l2,sh2),False⟩"
    by(auto intro!: rtrancl_into_rtrancl[OF b2T] RedSCall assms(3) simp: assms wf)
  also (rtrancl_trans) have "P ⊢ ⟨blocks(pns, Ts, vs, body), (h2,l2,sh2),False⟩
                 →* ⟨ef,(h3,override_on (l2++l3) l2 (set pns),sh3),b3⟩"
    by(rule blocksRedsFinal, insert assms wf body', simp_all)
  finally show ?thesis using eql2 by simp
qed
(*>*)

lemma SCallRedsThrowParams:
  "⟦ P ⊢ ⟨es,s0,b0⟩ [→]* ⟨map Val vs1 @ throw a # es2,s2,b2⟩ ⟧
  ⟹ P ⊢ ⟨C∙sM(es),s0,b0⟩ →* ⟨throw a,s2,b2⟩"
(*<*)
by(erule SCallRedsParams[THEN rtrancl_into_rtrancl, OF _ SCallThrowParams])
   simp
(*>*)

lemma SCallRedsNone:
  "⟦ P ⊢ ⟨es,s,b⟩ [→]* ⟨map Val vs,s2,False⟩;
    ¬(∃b Ts T m D. P ⊢ C sees M,b:Ts→T = m in D) ⟧
  ⟹ P ⊢ ⟨C∙sM(es),s,b⟩ →* ⟨THROW NoSuchMethodError,s2,False⟩"
(*<*)
by(erule SCallRedsParams[THEN rtrancl_into_rtrancl, OF _ RedSCallNone])
   simp
(*>*)

lemma SCallRedsNonStatic:
  "⟦ P ⊢ ⟨es,s,b⟩ [→]* ⟨map Val vs,s2,False⟩;
     P ⊢ C sees M,NonStatic:Ts→T = m in D ⟧
  ⟹ P ⊢ ⟨C∙sM(es),s,b⟩ →* ⟨THROW IncompatibleClassChangeError,s2,False⟩"
(*<*)
by(erule SCallRedsParams[THEN rtrancl_into_rtrancl, OF _ RedSCallNonStatic])
   simp
(*>*)

lemma SCallInitThrowReds:
assumes wwf: "wwf_J_prog P"
and "P ⊢ ⟨es,s0,b0⟩ [→]* ⟨map Val vs,(h1,l1,sh1),False⟩"
      "P ⊢ C sees M,Static:Ts→T = (pns,body) in D"
      "∄sfs. sh1 D = Some(sfs,Done)"
      "M ≠ clinit"
and "P ⊢ ⟨INIT D ([D],False) ← unit,(h1,l1,sh1),False⟩ →* ⟨throw a,(h2,l2,sh2),b2⟩"
shows "P ⊢ ⟨C∙sM(es), s0,b0⟩ →* ⟨throw a,(h2,l2,sh2),b2⟩"
(*<*)(is "(?x, ?z) ∈ (red P)*")
proof -
  let ?y = "(C∙sM(map Val vs),(h1,l1,sh1),False)"
  let ?y' = "(INIT D ([D],False) ← C∙sM(map Val vs),(h1,l1,sh1),False)"
  have "(?x, ?y) ∈ (red P)*" by(rule SCallRedsParams[OF assms(2)])
  also have "(?y, ?y') ∈ (red P)*"
    using SCallInitRed[OF assms(3)] assms(4-5) by auto
  also have "(?y', ?z) ∈ (red P)*" by(rule InitSeqThrowReds[OF assms(6)])
  finally show ?thesis by simp
qed
(*>*)

lemma SCallInitReds:
assumes wwf: "wwf_J_prog P"
and "P ⊢ ⟨es,s0,b0⟩ [→]* ⟨map Val vs,(h1,l1,sh1),False⟩"
      "P ⊢ C sees M,Static:Ts→T = (pns,body) in D"
      "∄sfs. sh1 D = Some(sfs,Done)"
      "M ≠ clinit"
and "P ⊢ ⟨INIT D ([D],False) ← unit,(h1,l1,sh1),False⟩ →* ⟨Val v',(h2,l2,sh2),b2⟩"
and "size vs = size pns"
and l2': "l2' = [pns[↦]vs]"
and body: "P ⊢ ⟨body,(h2,l2',sh2),False⟩ →* ⟨ef,(h3,l3,sh3),b3⟩"
and "final ef"
shows "P ⊢ ⟨C∙sM(es),s0,b0⟩ →* ⟨ef,(h3,l2,sh3),b3⟩"
(*<*)
proof -
  have wf: "size Ts = size pns ∧ distinct pns"
    and wt: "fv body ⊆ set pns"
    using assms by(fastforce dest!:sees_wf_mdecl simp:wf_mdecl_def)+
  from body[THEN Red_lcl_add, of l2]
  have body': "P ⊢ ⟨body,(h2,l2(pns[↦]vs),sh2),False⟩ →* ⟨ef,(h3,l2++l3,sh3),b3⟩"
    by (simp add:l2')
  have "dom l3 ⊆ set pns"
    using Reds_dom_lcl[OF wwf body] wt l2' set_take_subset by force
  hence eql2: "override_on (l2++l3) l2 (set pns) = l2"
    by(fastforce simp add:map_add_def override_on_def fun_eq_iff)
  have "icheck P D (C∙sM(map Val vs)::'a exp)" using assms(3) by auto
  then have "P ⊢ ⟨C∙sM(map Val vs),(h2, l2, sh2),icheck P D (C∙sM(map Val vs))⟩
       → ⟨blocks(pns, Ts, vs, body), (h2, l2, sh2), False⟩"
    by (metis (full_types) assms(3) assms(7) local.wf red_reds.RedSCall)
  also have "P ⊢ ⟨blocks(pns, Ts, vs, body), (h2, l2, sh2), False⟩
         →* ⟨ef,(h3,override_on (l2++l3) l2 (set pns),sh3),b3⟩"
    by(rule blocksRedsFinal, insert assms wf body', simp_all)
  finally have trueReds: "P ⊢ ⟨C∙sM(map Val vs),(h2, l2, sh2),icheck P D (C∙sM(map Val vs))⟩
                   →* ⟨ef,(h3,override_on (l2++l3) l2 (set pns),sh3),b3⟩" by simp
  have "P ⊢ ⟨C∙sM(es),s0,b0⟩ →* ⟨C∙sM(map Val vs),(h1,l1,sh1),False⟩"
    by(rule SCallRedsParams)(rule assms(2))
  also have "P ⊢ ⟨C∙sM(map Val vs),(h1,l1,sh1),False⟩ → ⟨INIT D ([D],False) ← C∙sM(map Val vs),(h1,l1,sh1),False⟩"
    using SCallInitRed[OF assms(3)] assms(4-5) by auto
  also (rtrancl_into_rtrancl) have "P ⊢ ⟨INIT D ([D],False) ← C∙sM(map Val vs),(h1,l1,sh1),False⟩
                 →* ⟨ef,(h3,override_on (l2++l3) l2 (set pns),sh3),b3⟩"
    using InitSeqReds[OF assms(6) trueReds] assms(5) by simp
  finally show ?thesis using eql2 by simp
qed
(*>*)

lemma SCallInitProcessingReds:
assumes wwf: "wwf_J_prog P"
and "P ⊢ ⟨es,s0,b0⟩ [→]* ⟨map Val vs,(h2,l2,sh2),b2⟩"
      "P ⊢ C sees M,Static:Ts→T = (pns,body) in D"
      "sh2 D = Some(sfs,Processing)"
and "size vs = size pns"
and l2': "l2' = [pns[↦]vs]"
and body: "P ⊢ ⟨body,(h2,l2',sh2),False⟩ →* ⟨ef,(h3,l3,sh3),b3⟩"
and "final ef"
shows "P ⊢ ⟨C∙sM(es),s0,b0⟩ →* ⟨ef,(h3,l2,sh3),b3⟩"
(*<*)
proof -
  have wf: "size Ts = size pns ∧ distinct pns"
    and wt: "fv body ⊆ set pns"
    using assms by(fastforce dest!:sees_wf_mdecl simp:wf_mdecl_def)+
  from body[THEN Red_lcl_add, of l2]
  have body': "P ⊢ ⟨body,(h2,l2(pns[↦]vs),sh2),False⟩ →* ⟨ef,(h3,l2++l3,sh3),b3⟩"
    by (simp add:l2')
  have "dom l3 ⊆ set pns"
    using Reds_dom_lcl[OF wwf body] wt l2' set_take_subset by force
  hence eql2: "override_on (l2++l3) l2 (set pns) = l2"
    by(fastforce simp add:map_add_def override_on_def fun_eq_iff)
  have b2T: "P ⊢ ⟨C∙sM(map Val vs), (h2,l2,sh2),b2⟩ →* ⟨C∙sM(map Val vs), (h2,l2,sh2),True⟩"
  proof(cases b2)
    case True then show ?thesis by simp
  next
    case False
    show ?thesis
    proof(cases "M = clinit")
      case True then show ?thesis using False assms(3) red_reds.SCallInitDoneRed assms(4)
        by (simp add: r_into_rtrancl)
    next
      case nclinit: False
      have icheck: "icheck P D (C∙sM(map Val vs))" using assms(3) by auto
      have "P ⊢ ⟨C∙sM(map Val vs),(h2, l2, sh2),b2⟩
         → ⟨INIT D ([D],False) ← C∙sM(map Val vs),(h2, l2, sh2),False⟩"
        using SCallInitRed[OF assms(3)] assms(4) False nclinit by simp
      also have "P ⊢ ⟨INIT D ([D],False) ← C∙sM(map Val vs),(h2, l2, sh2),False⟩
         → ⟨INIT D (Nil,True) ← C∙sM(map Val vs),(h2, l2, sh2),False⟩"
        using RedInitProcessing assms(4) by simp
      also have "P ⊢ ⟨INIT D (Nil,True) ← C∙sM(map Val vs),(h2, l2, sh2),False⟩
         → ⟨C∙sM(map Val vs),(h2, l2, sh2),True⟩"
        using RedInit[of "C∙sM(map Val vs)" D _ _ _ P] icheck nclinit
         by (metis (full_types) nsub_RI_Vals sub_RI.simps(12))
      finally show ?thesis by simp
    qed
  qed
  have "P ⊢ ⟨C∙sM(es),s0,b0⟩ →* ⟨C∙sM(map Val vs),(h2,l2,sh2),b2⟩"
    by(rule SCallRedsParams)(rule assms(2))
  also have "P ⊢ ⟨C∙sM(map Val vs), (h2,l2,sh2),b2⟩ →* ⟨blocks(pns, Ts, vs, body), (h2,l2,sh2),False⟩"
    by(auto intro!: rtrancl_into_rtrancl[OF b2T] RedSCall assms(3) simp: assms wf)
  also (rtrancl_trans) have "P ⊢ ⟨blocks(pns, Ts, vs, body), (h2,l2,sh2),False⟩
                 →* ⟨ef,(h3,override_on (l2++l3) l2 (set pns),sh3),b3⟩"
    by(rule blocksRedsFinal, insert assms wf body', simp_all)
  finally show ?thesis using eql2 by simp
qed
(*>*)

(***********************************)

subsubsection "The main Theorem"

lemma assumes wwf: "wwf_J_prog P"
shows big_by_small: "P ⊢ ⟨e,s⟩ ⇒ ⟨e',s'⟩
   ⟹ (⋀b. iconf (shp s) e ⟹ P,shp s ⊢b (e,b) √ ⟹ P ⊢ ⟨e,s,b⟩ →* ⟨e',s',False⟩)"
and bigs_by_smalls: "P ⊢ ⟨es,s⟩ [⇒] ⟨es',s'⟩
   ⟹ (⋀b. iconfs (shp s) es ⟹ P,shp s ⊢b (es,b) √ ⟹ P ⊢ ⟨es,s,b⟩ [→]* ⟨es',s',False⟩)"
(*<*)
proof (induct rule: eval_evals.inducts)
  case New show ?case
  proof(cases b)
    case True then show ?thesis using RedNew[OF New.hyps(2-4)] by auto
  next
    case False then show ?thesis using New.hyps(1) NewInitDoneReds[OF _ New.hyps(2-4)] by auto
  qed
next
  case NewFail show ?case
  proof(cases b)
    case True then show ?thesis using RedNewFail[OF NewFail.hyps(2)] NewFail.hyps(3) by fastforce
  next
    case False
    then show ?thesis using NewInitDoneReds2[OF _ NewFail.hyps(2)] NewFail by fastforce
  qed
next
  case (NewInit sh C h l v' h' l' sh' a FDTs h'') show ?case
  proof(cases b)
    case True
    then obtain sfs where shC: "sh C = ⌊(sfs, Processing)⌋"
      using NewInit.hyps(1) NewInit.prems by(clarsimp simp: bconf_def initPD_def)
    then have s': "(h',l',sh') = (h,l,sh)" using NewInit.hyps(2) init_ProcessingE by clarsimp
    then show ?thesis using RedNew[OF NewInit.hyps(4-6)] True by auto
  next
    case False
    then have init: "P ⊢ ⟨INIT C ([C],False) ← unit,(h, l, sh),False⟩ →* ⟨Val v',(h', l', sh'),False⟩"
      using NewInit.hyps(3) by(auto simp: bconf_def)
    then show ?thesis using NewInit NewInitReds[OF _ init NewInit.hyps(4-6)] False
     has_fields_is_class[OF NewInit.hyps(5)] by auto
  qed
next
  case (NewInitOOM sh C h l v' h' l' sh') show ?case
  proof(cases b)
    case True
    then obtain sfs where shC: "sh C = ⌊(sfs, Processing)⌋"
      using NewInitOOM.hyps(1) NewInitOOM.prems by(clarsimp simp: bconf_def initPD_def)
    then have s': "(h',l',sh') = (h,l,sh)" using NewInitOOM.hyps(2) init_ProcessingE by clarsimp
    then show ?thesis using RedNewFail[OF NewInitOOM.hyps(4)] True r_into_rtrancl NewInitOOM.hyps(5)
      by auto
  next
    case False
    then have init: "P ⊢ ⟨INIT C ([C],False) ← unit,(h, l, sh),False⟩ →* ⟨Val v',(h', l', sh'),False⟩"
      using NewInitOOM.hyps(3) by(auto simp: bconf_def)
    then show ?thesis using NewInitOOM.hyps(1) NewInitOOMReds[OF _ init NewInitOOM.hyps(4)] False
      NewInitOOM.hyps(5) by auto
  qed
next
  case (NewInitThrow sh C h l a s') show ?case
  proof(cases b)
    case True
    then obtain sfs where shC: "sh C = ⌊(sfs, Processing)⌋"
      using NewInitThrow.hyps(1) NewInitThrow.prems by(clarsimp simp: bconf_def initPD_def)
    then show ?thesis using NewInitThrow.hyps(2) init_ProcessingE by blast
  next
    case False
    then have init: "P ⊢ ⟨INIT C ([C],False) ← unit,(h, l, sh),b⟩ →* ⟨throw a,s',False⟩"
      using NewInitThrow.hyps(3) by(auto simp: bconf_def)
    then show ?thesis using NewInitThrow NewInitThrowReds[of "(h,l,sh)" C P a s'] False by auto
  qed
next
  case Cast then show ?case by(fastforce intro:CastRedsAddr)
next
  case CastNull then show ?case by(fastforce intro: CastRedsNull)
next
  case CastFail thus ?case by(fastforce intro!:CastRedsFail)
next
  case CastThrow thus ?case by(fastforce dest!:eval_final intro:CastRedsThrow)
next
  case Val then show ?case using exI[of _ b] by(simp add: bconf_def)
next
  case (BinOp e1 s0 v1 s1 e2 v2 s2 bop v)
  show ?case
  proof(cases "val_of e1")
    case None
    then have iconf: "iconf (shp s0) e1" using None BinOp.prems by auto
    have bconf: "P,shp s0 ⊢b (e1,b) √" using None BinOp.prems by auto
    then have b1: "P ⊢ ⟨e1,s0,b⟩ →* ⟨Val v1,s1,False⟩" using iconf BinOp.hyps(2) by auto
    have binop: "P ⊢ ⟨e1 «bop» e2,s0,b⟩ →* ⟨Val v1 «bop» e2,s1,False⟩" by(rule BinOp1Reds[OF b1])
    then have iconf2': "iconf (shp s1) e2" using Red_preserves_iconf[OF wwf binop] None BinOp by auto
    have "P,shp s1 ⊢b (e2,False) √" by(simp add: bconf_def)
    then have b2: "P ⊢ ⟨e2,s1,False⟩ →* ⟨Val v2,s2,False⟩" using BinOp.hyps(4)[OF iconf2'] by auto
    then show ?thesis using BinOpRedsVal[OF b1 b2 BinOp.hyps(5)] by fast
  next
    case (Some a)
    then obtain b1 where b1: "P ⊢ ⟨e1,s0,b⟩ →* ⟨Val v1,s1,b1⟩"
      by (metis (no_types, lifting) BinOp.hyps(1) eval_cases(3) rtrancl.rtrancl_refl val_of_spec)
    have binop: "P ⊢ ⟨e1 «bop» e2,s0,b⟩ →* ⟨Val v1 «bop» e2,s1,b1⟩" by(rule BinOp1Reds[OF b1])
    then have iconf2': "iconf (shp s1) e2" using Red_preserves_iconf[OF wwf binop] BinOp by auto
    have bconf2: "P,shp s0 ⊢b (e2,b) √" using BinOp.prems Some by simp
    then have "P,shp s1 ⊢b (e2,b1) √" using Red_preserves_bconf[OF wwf binop BinOp.prems] by simp
    then have b2: "P ⊢ ⟨e2,s1,b1⟩ →* ⟨Val v2,s2,False⟩" using BinOp.hyps(4)[OF iconf2'] by auto
    then show ?thesis using BinOpRedsVal[OF b1 b2 BinOp.hyps(5)] by fast
  qed
next
  case (BinOpThrow1 e1 s0 e s1 bop e2) show ?case
  proof(cases "val_of e1")
    case None
    then have "iconf (shp s0) e1" and "P,shp s0 ⊢b (e1,b) √" using BinOpThrow1.prems by auto
    then have b1: "P ⊢ ⟨e1,s0,b⟩ →* ⟨throw e,s1,False⟩" using BinOpThrow1.hyps(2) by auto
    then have "P ⊢ ⟨e1 «bop» e2,s0,b⟩ →* ⟨throw e,s1,False⟩"
      using BinOpThrow1 None by(auto dest!:eval_final simp: BinOpRedsThrow1[OF b1])
    then show ?thesis by fast
  next
    case (Some a)
    then show ?thesis using eval_final_same[OF BinOpThrow1.hyps(1)] val_of_spec[OF Some] by auto
  qed
next
  case (BinOpThrow2 e1 s0 v1 s1 e2 e s2 bop)
  show ?case
  proof(cases "val_of e1")
    case None
    then have iconf: "iconf (shp s0) e1" using None BinOpThrow2.prems by auto
    have bconf: "P,shp s0 ⊢b (e1,b) √" using None BinOpThrow2.prems by auto
    then have b1: "P ⊢ ⟨e1,s0,b⟩ →* ⟨Val v1,s1,False⟩" using iconf BinOpThrow2.hyps(2) by auto
    have binop: "P ⊢ ⟨e1 «bop» e2,s0,b⟩ →* ⟨Val v1 «bop» e2,s1,False⟩" by(rule BinOp1Reds[OF b1])
    then have iconf2': "iconf (shp s1) e2" using Red_preserves_iconf[OF wwf binop] None BinOpThrow2 by auto
    have "P,shp s1 ⊢b (e2,False) √" by(simp add: bconf_def)
    then have b2: "P ⊢ ⟨e2,s1,False⟩ →* ⟨throw e,s2,False⟩" using BinOpThrow2.hyps(4)[OF iconf2'] by auto
    then show ?thesis using BinOpRedsThrow2[OF b1 b2] by fast
  next
    case (Some a)
    then obtain b1 where b1: "P ⊢ ⟨e1,s0,b⟩ →* ⟨Val v1,s1,b1⟩"
      by (metis (no_types, lifting) BinOpThrow2.hyps(1) eval_cases(3) rtrancl.rtrancl_refl val_of_spec)
    have binop: "P ⊢ ⟨e1 «bop» e2,s0,b⟩ →* ⟨Val v1 «bop» e2,s1,b1⟩" by(rule BinOp1Reds[OF b1])
    then have iconf2': "iconf (shp s1) e2" using Red_preserves_iconf[OF wwf binop] BinOpThrow2 by auto
    have bconf2: "P,shp s0 ⊢b (e2,b) √" using BinOpThrow2.prems Some by simp
    then have "P,shp s1 ⊢b (e2,b1) √" using Red_preserves_bconf[OF wwf binop BinOpThrow2.prems] by simp
    then have b2: "P ⊢ ⟨e2,s1,b1⟩ →* ⟨throw e,s2,False⟩" using BinOpThrow2.hyps(4)[OF iconf2'] by auto
    then show ?thesis using BinOpRedsThrow2[OF b1 b2] by fast
  qed
next
  case Var thus ?case by(auto dest:RedVar simp: bconf_def)
next
  case LAss thus ?case by(auto dest: LAssRedsVal)
next
  case LAssThrow thus ?case by(auto dest!:eval_final dest: LAssRedsThrow)
next
  case FAcc thus ?case by(fastforce intro:FAccRedsVal)
next
  case FAccNull thus ?case by(auto dest:FAccRedsNull)
next
  case FAccThrow thus ?case by(auto dest!:eval_final dest:FAccRedsThrow)
next
  case FAccNone then show ?case by(fastforce intro: FAccRedsNone)
next
  case FAccStatic then show ?case by(fastforce intro: FAccRedsStatic)
next
  case SFAcc show ?case
  proof(cases b)
    case True then show ?thesis using RedSFAcc SFAcc.hyps by auto
  next
    case False then show ?thesis using SFAcc.hyps SFAccInitDoneReds[OF SFAcc.hyps(1)] by auto
  qed
next
  case (SFAccInit C F t D sh h l v' h' l' sh' sfs i v) show ?case
  proof(cases b)
    case True
    then obtain sfs where shC: "sh D = ⌊(sfs, Processing)⌋"
      using SFAccInit.hyps(2) SFAccInit.prems by(clarsimp simp: bconf_def initPD_def)
    then have s': "(h',l',sh') = (h,l,sh)" using SFAccInit.hyps(3) init_ProcessingE by clarsimp
    then show ?thesis using RedSFAcc SFAccInit.hyps True by auto
  next
    case False
    then have init: "P ⊢ ⟨INIT D ([D],False) ← unit,(h, l, sh),False⟩ →* ⟨Val v',(h', l', sh'),False⟩"
      using SFAccInit.hyps(4) by(auto simp: bconf_def)
    then show ?thesis using SFAccInit SFAccInitReds[OF _ _ init] False by auto
  qed
next
  case (SFAccInitThrow C F t D sh h l a s') show ?case
  proof(cases b)
    case True
    then obtain sfs where shC: "sh D = ⌊(sfs, Processing)⌋"
      using SFAccInitThrow.hyps(2) SFAccInitThrow.prems(2) by(clarsimp simp: bconf_def initPD_def)
    then show ?thesis using SFAccInitThrow.hyps(3) init_ProcessingE by blast
  next
    case False
    then have init: "P ⊢ ⟨INIT D ([D],False) ← unit,(h, l, sh),b⟩ →* ⟨throw a,s',False⟩"
      using SFAccInitThrow.hyps(4) by(auto simp: bconf_def)
    then show ?thesis using SFAccInitThrow SFAccInitThrowReds False by auto
  qed
next
  case SFAccNone then show ?case by(fastforce intro: SFAccRedsNone)
next
  case SFAccNonStatic then show ?case by(fastforce intro: SFAccRedsNonStatic)
next
  case (FAss e1 s0 a s1 e2 v h2 l2 sh2 C fs F t D fs' h2')
  show ?case
  proof(cases "val_of e1")
    case None
    then have iconf: "iconf (shp s0) e1" using None FAss.prems by auto
    have bconf: "P,shp s0 ⊢b (e1,b) √" using None FAss.prems by auto
    then have b1: "P ⊢ ⟨e1,s0,b⟩ →* ⟨addr a,s1,False⟩" using iconf FAss.hyps(2) by auto
    have fass: "P ⊢ ⟨e1∙F{D} := e2,s0,b⟩ →* ⟨addr a∙F{D} := e2,s1,False⟩" by(rule FAssReds1[OF b1])
    then have iconf2': "iconf (shp s1) e2" using Red_preserves_iconf[OF wwf fass] None FAss by auto
    have "P,shp s1 ⊢b (e2,False) √" by(simp add: bconf_def)
    then have b2: "P ⊢ ⟨e2,s1,False⟩ →* ⟨Val v,(h2, l2, sh2),False⟩" using FAss.hyps(4)[OF iconf2'] by auto
    then show ?thesis using FAssRedsVal[OF b1 b2 FAss.hyps(6) FAss.hyps(5)[THEN sym]] FAss.hyps(7,8) by fast
  next
    case (Some a')
    then obtain b1 where b1: "P ⊢ ⟨e1,s0,b⟩ →* ⟨addr a,s1,b1⟩"
      by (metis (no_types, lifting) FAss.hyps(1) eval_cases(3) rtrancl.rtrancl_refl val_of_spec)
    have fass: "P ⊢ ⟨e1∙F{D} := e2,s0,b⟩ →* ⟨addr a∙F{D} := e2,s1,b1⟩" by(rule FAssReds1[OF b1])
    then have iconf2': "iconf (shp s1) e2" using Red_preserves_iconf[OF wwf fass] FAss by auto
    have bconf2: "P,shp s0 ⊢b (e2,b) √" using FAss.prems Some by simp
    then have "P,shp s1 ⊢b (e2,b1) √" using Red_preserves_bconf[OF wwf fass FAss.prems] by simp
    then have b2: "P ⊢ ⟨e2,s1,b1⟩ →* ⟨Val v,(h2, l2, sh2),False⟩" using FAss.hyps(4)[OF iconf2'] by auto
    then show ?thesis using FAssRedsVal[OF b1 b2] FAss.hyps(5)[THEN sym] FAss.hyps(6-8) by fast
  qed
next
  case (FAssNull e1 s0 s1 e2 v s2 F D)
  show ?case
  proof(cases "val_of e1")
    case None
    then have iconf: "iconf (shp s0) e1" using FAssNull.prems(1) by simp
    have bconf: "P,shp s0 ⊢b (e1,b) √" using FAssNull.prems(2) None by simp
    then have b1: "P ⊢ ⟨e1,s0,b⟩ →* ⟨null,s1,False⟩" using FAssNull.hyps(2)[OF iconf] by auto
    have fass: "P ⊢ ⟨e1∙F{D} := e2,s0,b⟩ →* ⟨null∙F{D} := e2,s1,False⟩" by(rule FAssReds1[OF b1])
    then have iconf2': "iconf (shp s1) e2" using Red_preserves_iconf[OF wwf fass] None FAssNull by auto
    have "P,shp s1 ⊢b (e2,False) √" by(simp add: bconf_def)
    then have b2: "P ⊢ ⟨e2,s1,False⟩ →* ⟨Val v,s2,False⟩" using FAssNull.hyps(4)[OF iconf2'] by auto
    then show ?thesis using FAssRedsNull[OF b1 b2] by fast
  next
    case (Some a')
    then obtain b1 where b1: "P ⊢ ⟨e1,s0,b⟩ →* ⟨null,s1,b1⟩"
      by (metis (no_types, lifting) FAssNull.hyps(1) eval_cases(3) rtrancl.rtrancl_refl val_of_spec)
    have fass: "P ⊢ ⟨e1∙F{D} := e2,s0,b⟩ →* ⟨null∙F{D} := e2,s1,b1⟩" by(rule FAssReds1[OF b1])
    then have iconf2': "iconf (shp s1) e2" using Red_preserves_iconf[OF wwf fass] FAssNull by auto
    have bconf2: "P,shp s0 ⊢b (e2,b) √" using FAssNull.prems Some by simp
    then have "P,shp s1 ⊢b (e2,b1) √" using Red_preserves_bconf[OF wwf fass FAssNull.prems] by simp
    then have b2: "P ⊢ ⟨e2,s1,b1⟩ →* ⟨Val v,s2,False⟩" using FAssNull.hyps(4)[OF iconf2'] by auto
    then show ?thesis using FAssRedsNull[OF b1 b2] by fast
  qed
next
  case (FAssThrow1 e1 s0 e' s1 F D e2) show ?case
  proof(cases "val_of e1")
    case None
    then have "iconf (shp s0) e1" and "P,shp s0 ⊢b (e1,b) √" using FAssThrow1.prems by auto
    then have b1: "P ⊢ ⟨e1,s0,b⟩ →* ⟨throw e',s1,False⟩" using FAssThrow1.hyps(2) by auto
    then have "P ⊢ ⟨e1∙F{D} := e2,s0,b⟩ →* ⟨throw e',s1,False⟩"
      using FAssThrow1 None by(auto dest!:eval_final simp: FAssRedsThrow1[OF b1])
    then show ?thesis by fast
  next
    case (Some a)
    then show ?thesis using eval_final_same[OF FAssThrow1.hyps(1)] val_of_spec[OF Some] by auto
  qed
next
  case (FAssThrow2 e1 s0 v s1 e2 e' s2 F D)
  show ?case
  proof(cases "val_of e1")
    case None
    then have iconf: "iconf (shp s0) e1" using None FAssThrow2.prems by auto
    have bconf: "P,shp s0 ⊢b (e1,b) √" using None FAssThrow2.prems by auto
    then have b1: "P ⊢ ⟨e1,s0,b⟩ →* ⟨Val v,s1,False⟩" using iconf FAssThrow2.hyps(2) by auto
    have fass: "P ⊢ ⟨e1∙F{D} := e2,s0,b⟩ →* ⟨Val v∙F{D} := e2,s1,False⟩" by(rule FAssReds1[OF b1])
    then have iconf2': "iconf (shp s1) e2" using Red_preserves_iconf[OF wwf fass] None FAssThrow2 by auto
    have "P,shp s1 ⊢b (e2,False) √" by(simp add: bconf_def)
    then have b2: "P ⊢ ⟨e2,s1,False⟩ →* ⟨throw e',s2,False⟩" using FAssThrow2.hyps(4)[OF iconf2'] by auto
    then show ?thesis using FAssRedsThrow2[OF b1 b2] by fast
  next
    case (Some a')
    then obtain b1 where b1: "P ⊢ ⟨e1,s0,b⟩ →* ⟨Val v,s1,b1⟩"
      by (metis (no_types, lifting) FAssThrow2.hyps(1) eval_cases(3) rtrancl.rtrancl_refl val_of_spec)
    have fass: "P ⊢ ⟨e1∙F{D} := e2,s0,b⟩ →* ⟨Val v∙F{D} := e2,s1,b1⟩" by(rule FAssReds1[OF b1])
    then have iconf2': "iconf (shp s1) e2" using Red_preserves_iconf[OF wwf fass] FAssThrow2 by auto
    have bconf2: "P,shp s0 ⊢b (e2,b) √" using FAssThrow2.prems Some by simp
    then have "P,shp s1 ⊢b (e2,b1) √" using Red_preserves_bconf[OF wwf fass FAssThrow2.prems] by simp
    then have b2: "P ⊢ ⟨e2,s1,b1⟩ →* ⟨throw e',s2,False⟩" using FAssThrow2.hyps(4)[OF iconf2'] by auto
    then show ?thesis using FAssRedsThrow2[OF b1 b2] by fast
  qed
next
  case (FAssNone e1 s0 a s1 e2 v h2 l2 sh2 C fs F D)
  show ?case
  proof(cases "val_of e1")
    case None
    then have iconf: "iconf (shp s0) e1" using None FAssNone.prems by auto
    have bconf: "P,shp s0 ⊢b (e1,b) √" using None FAssNone.prems by auto
    then have b1: "P ⊢ ⟨e1,s0,b⟩ →* ⟨addr a,s1,False⟩" using iconf FAssNone.hyps(2) by auto
    have fass: "P ⊢ ⟨e1∙F{D} := e2,s0,b⟩ →* ⟨addr a∙F{D} := e2,s1,False⟩" by(rule FAssReds1[OF b1])
    then have iconf2': "iconf (shp s1) e2" using Red_preserves_iconf[OF wwf fass] None FAssNone by auto
    have "P,shp s1 ⊢b (e2,False) √" by(simp add: bconf_def)
    then have b2: "P ⊢ ⟨e2,s1,False⟩ →* ⟨Val v,(h2, l2, sh2),False⟩" using FAssNone.hyps(4)[OF iconf2'] by auto
    then show ?thesis using FAssRedsNone[OF b1 b2 FAssNone.hyps(5,6)] by fast
  next
    case (Some a')
    then obtain b1 where b1: "P ⊢ ⟨e1,s0,b⟩ →* ⟨addr a,s1,b1⟩"
      by (metis (no_types, lifting) FAssNone.hyps(1) eval_cases(3) rtrancl.rtrancl_refl val_of_spec)
    have fass: "P ⊢ ⟨e1∙F{D} := e2,s0,b⟩ →* ⟨addr a∙F{D} := e2,s1,b1⟩" by(rule FAssReds1[OF b1])
    then have iconf2': "iconf (shp s1) e2" using Red_preserves_iconf[OF wwf fass] FAssNone by auto
    have bconf2: "P,shp s0 ⊢b (e2,b) √" using FAssNone.prems Some by simp
    then have "P,shp s1 ⊢b (e2,b1) √" using Red_preserves_bconf[OF wwf fass FAssNone.prems] by simp
    then have b2: "P ⊢ ⟨e2,s1,b1⟩ →* ⟨Val v,(h2, l2, sh2),False⟩" using FAssNone.hyps(4)[OF iconf2'] by auto
    then show ?thesis using FAssRedsNone[OF b1 b2 FAssNone.hyps(5,6)] by fast
  qed
next
  case (FAssStatic e1 s0 a s1 e2 v h2 l2 sh2 C fs F t D)
  show ?case
  proof(cases "val_of e1")
    case None
    then have iconf: "iconf (shp s0) e1" using None FAssStatic.prems by auto
    have bconf: "P,shp s0 ⊢b (e1,b) √" using None FAssStatic.prems by auto
    then have b1: "P ⊢ ⟨e1,s0,b⟩ →* ⟨addr a,s1,False⟩" using iconf FAssStatic.hyps(2) by auto
    have fass: "P ⊢ ⟨e1∙F{D} := e2,s0,b⟩ →* ⟨addr a∙F{D} := e2,s1,False⟩" by(rule FAssReds1[OF b1])
    then have iconf2': "iconf (shp s1) e2" using Red_preserves_iconf[OF wwf fass] None FAssStatic by auto
    have "P,shp s1 ⊢b (e2,False) √" by(simp add: bconf_def)
    then have b2: "P ⊢ ⟨e2,s1,False⟩ →* ⟨Val v,(h2, l2, sh2),False⟩" using FAssStatic.hyps(4)[OF iconf2'] by auto
    then show ?thesis using FAssRedsStatic[OF b1 b2 FAssStatic.hyps(5,6)] by fast
  next
    case (Some a')
    then obtain b1 where b1: "P ⊢ ⟨e1,s0,b⟩ →* ⟨addr a,s1,b1⟩"
      by (metis (no_types, lifting) FAssStatic.hyps(1) eval_cases(3) rtrancl.rtrancl_refl val_of_spec)
    have fass: "P ⊢ ⟨e1∙F{D} := e2,s0,b⟩ →* ⟨addr a∙F{D} := e2,s1,b1⟩" by(rule FAssReds1[OF b1])
    then have iconf2': "iconf (shp s1) e2" using Red_preserves_iconf[OF wwf fass] FAssStatic by auto
    have bconf2: "P,shp s0 ⊢b (e2,b) √" using FAssStatic.prems Some by simp
    then have "P,shp s1 ⊢b (e2,b1) √" using Red_preserves_bconf[OF wwf fass FAssStatic.prems] by simp
    then have b2: "P ⊢ ⟨e2,s1,b1⟩ →* ⟨Val v,(h2, l2, sh2),False⟩" using FAssStatic.hyps(4)[OF iconf2'] by auto
    then show ?thesis using FAssRedsStatic[OF b1 b2 FAssStatic.hyps(5,6)] by fast
  qed
next
  case (SFAss e2 s0 v h1 l1 sh1 C F t D sfs sfs' sh1')
  show ?case
  proof(cases "val_of e2")
    case None
    then have bconf: "P,shp s0 ⊢b (e2,b) √" using SFAss.prems(2) by simp
    then have b1: "P ⊢ ⟨e2,s0,b⟩ →* ⟨Val v,(h1, l1, sh1),False⟩" using SFAss by auto
    thus ?thesis using SFAssRedsVal[OF b1 SFAss.hyps(3,4)] SFAss.hyps(5,6) by fast
  next
    case (Some a)
    then obtain b1 where b1: "P ⊢ ⟨e2,s0,b⟩ →* ⟨Val v,(h1, l1, sh1),b1⟩"
      by (metis (no_types, lifting) SFAss.hyps(1) eval_cases(3) rtrancl.rtrancl_refl val_of_spec)
    thus ?thesis using SFAssRedsVal[OF b1 SFAss.hyps(3,4)] SFAss.hyps(5,6) by fast
  qed
next
  case (SFAssInit e2 s0 v h1 l1 sh1 C F t D v' h' l' sh' sfs i sfs' sh'')
  then have iconf: "iconf (shp s0) e2" by simp
  show ?case
  proof(cases "val_of e2")
    case None
    then have bconf: "P,shp s0 ⊢b (e2,b) √" using SFAssInit.prems(2) by simp
    then have reds: "P ⊢ ⟨e2,s0,b⟩ →* ⟨Val v,(h1, l1, sh1),False⟩"
      using SFAssInit.hyps(2)[OF iconf bconf] by auto
    then have init: "P ⊢ ⟨INIT D ([D],False) ← unit,(h1, l1, sh1),False⟩ →* ⟨Val v',(h', l', sh'),False⟩"
      using SFAssInit.hyps(6) by(auto simp: bconf_def)
    then show ?thesis using SFAssInit SFAssInitReds[OF reds SFAssInit.hyps(3) _ init] by auto
  next
    case (Some v2) show ?thesis
    proof(cases b)
      case False
      then have bconf: "P,shp s0 ⊢b (e2,b) √" by(simp add: bconf_def)
      then have reds: "P ⊢ ⟨e2,s0,b⟩ →* ⟨Val v,(h1, l1, sh1),False⟩"
        using SFAssInit.hyps(2)[OF iconf bconf] by auto
      then have init: "P ⊢ ⟨INIT D ([D],False) ← unit,(h1, l1, sh1),False⟩ →* ⟨Val v',(h', l', sh'),False⟩"
        using SFAssInit.hyps(6) by(auto simp: bconf_def)
      then show ?thesis using SFAssInit SFAssInitReds[OF reds SFAssInit.hyps(3) _ init] by auto
    next
      case True
      have e2: "e2 = Val v2" using val_of_spec[OF Some] by simp
      then have vs: "v2 = v ∧ s0 = (h1, l1, sh1)" using eval_final_same[OF SFAssInit.hyps(1)] by simp
      then obtain sfs where shC: "sh1 D = ⌊(sfs, Processing)⌋"
        using SFAssInit.hyps(3,4) SFAssInit.prems(2) Some True
          by(cases e2, auto simp: bconf_def initPD_def dest: sees_method_fun)
      then have s': "(h',l',sh') = (h1, l1, sh1)" using SFAssInit.hyps(5) init_ProcessingE by clarsimp
      then show ?thesis using SFAssInit.hyps(3,7-9) True e2 red_reds.RedSFAss vs by auto
    qed
  qed
next
  case (SFAssInitThrow e2 s0 v h1 l1 sh1 C F t D a s')
  then have iconf: "iconf (shp s0) e2" by simp
  show ?case
  proof(cases "val_of e2")
    case None
    then have bconf: "P,shp s0 ⊢b (e2,b) √" using SFAssInitThrow.prems(2) by simp
    then have reds: "P ⊢ ⟨e2,s0,b⟩ →* ⟨Val v,(h1, l1, sh1),False⟩"
      using SFAssInitThrow.hyps(2)[OF iconf bconf] by auto
    then have init: "P ⊢ ⟨INIT D ([D],False) ← unit,(h1, l1, sh1),False⟩ →* ⟨throw a,s',False⟩"
      using SFAssInitThrow.hyps(6) by(auto simp: bconf_def)
    then show ?thesis using SFAssInitThrow SFAssInitThrowReds[OF reds _ _ init] by auto
  next
    case (Some v2) show ?thesis
    proof(cases b)
      case False
      then have bconf: "P,shp s0 ⊢b (e2,b) √" by(simp add: bconf_def)
      then have reds: "P ⊢ ⟨e2,s0,b⟩ →* ⟨Val v,(h1, l1, sh1),False⟩"
        using SFAssInitThrow.hyps(2)[OF iconf bconf] by auto
      then have init: "P ⊢ ⟨INIT D ([D],False) ← unit,(h1, l1, sh1),False⟩ →* ⟨throw a,s',False⟩"
        using SFAssInitThrow.hyps(6) by(auto simp: bconf_def)
      then show ?thesis using SFAssInitThrow SFAssInitThrowReds[OF reds _ _ init] by auto
    next
      case True
      obtain v2 where e2: "e2 = Val v2" using val_of_spec[OF Some] by simp
      then have vs: "v2 = v ∧ s0 = (h1, l1, sh1)"
        using eval_final_same[OF SFAssInitThrow.hyps(1)] by simp
      then obtain sfs where shC: "sh1 D = ⌊(sfs, Processing)⌋"
       using SFAssInitThrow.hyps(4) SFAssInitThrow.prems(2) Some True
        by(cases e2, auto simp: bconf_def initPD_def dest: sees_method_fun)
      then show ?thesis using SFAssInitThrow.hyps(5) init_ProcessingE by blast
    qed
  qed
next
  case (SFAssThrow e2 s0 e' s2 C F D)
  show ?case
  proof(cases "val_of e2")
    case None
    then have bconf: "P,shp s0 ⊢b (e2,b) √" using SFAssThrow.prems(2) None by simp
    then have b1: "P ⊢ ⟨e2,s0,b⟩ →* ⟨throw e',s2,False⟩" using SFAssThrow by auto
    thus ?thesis using SFAssRedsThrow[OF b1] by fast
  next
    case (Some a)
    then show ?thesis using eval_final_same[OF SFAssThrow.hyps(1)] val_of_spec[OF Some] by auto
  qed
next
  case (SFAssNone e2 s0 v h2 l2 sh2 C F D)
  show ?case
  proof(cases "val_of e2")
    case None
    then have iconf: "iconf (shp s0) e2" using SFAssNone by simp
    then have bconf: "P,shp s0 ⊢b (e2,b) √" using SFAssNone.prems(2) None by simp
    then have b1: "P ⊢ ⟨e2,s0,b⟩ →* ⟨Val v,(h2, l2, sh2),False⟩" using SFAssNone.hyps(2) iconf by auto
    thus ?thesis using SFAssRedsNone[OF b1 SFAssNone.hyps(3)] by fast
  next
    case (Some a)
    then obtain b1 where b1: "P ⊢ ⟨e2,s0,b⟩ →* ⟨Val v,(h2, l2, sh2),b1⟩"
      by (metis (no_types, lifting) SFAssNone.hyps(1) eval_cases(3) rtrancl.rtrancl_refl val_of_spec)
    thus ?thesis using SFAssRedsNone[OF b1 SFAssNone.hyps(3)] by fast
  qed
next
  case (SFAssNonStatic e2 s0 v h2 l2 sh2 C F t D) show ?case
  proof(cases "val_of e2")
    case None
    then have iconf: "iconf (shp s0) e2" using SFAssNonStatic by simp
    then have bconf: "P,shp s0 ⊢b (e2,b) √" using SFAssNonStatic.prems(2) None by simp
    then have b1: "P ⊢ ⟨e2,s0,b⟩ →* ⟨Val v,(h2, l2, sh2),False⟩" using SFAssNonStatic.hyps(2) iconf by auto
    thus ?thesis using SFAssRedsNonStatic[OF b1 SFAssNonStatic.hyps(3)] by fast
  next
    case (Some a)
    then obtain b' where b1: "P ⊢ ⟨e2,s0,b⟩ →* ⟨Val v,(h2, l2, sh2),b'⟩"
      by (metis (no_types, lifting) SFAssNonStatic.hyps(1) eval_cases(3) rtrancl.rtrancl_refl val_of_spec)
    thus ?thesis using SFAssRedsNonStatic[OF b1 SFAssNonStatic.hyps(3)] by fast
  qed
next
  case (CallObjThrow e s0 e' s1 M ps) show ?case
  proof(cases "val_of e")
    case None
    then have "iconf (shp s0) e" and "P,shp s0 ⊢b (e,b) √" using CallObjThrow.prems by auto
    then have b1: "P ⊢ ⟨e,s0,b⟩ →* ⟨throw e',s1,False⟩" using CallObjThrow.hyps(2) by auto
    then have "P ⊢ ⟨e∙M(ps),s0,b⟩ →* ⟨throw e',s1,False⟩"
      using CallObjThrow None by(auto dest!:eval_final simp: CallRedsThrowObj[OF b1])
    then show ?thesis by fast
  next
    case (Some a)
    then show ?thesis using eval_final_same[OF CallObjThrow.hyps(1)] val_of_spec[OF Some] by auto
  qed
next
  case (CallNull e s0 s1 ps vs s2 M) show ?case
  proof(cases "val_of e")
    case None
    then have iconf: "iconf (shp s0) e" using CallNull.prems(1) by simp
    have bconf: "P,shp s0 ⊢b (e,b) √" using CallNull.prems(2) None by simp
    then have b1: "P ⊢ ⟨e,s0,b⟩ →* ⟨null,s1,False⟩" using CallNull.hyps(2)[OF iconf] by auto
    have call: "P ⊢ ⟨e∙M(ps),s0,b⟩ →* ⟨null∙M(ps),s1,False⟩" by(rule CallRedsObj[OF b1])
    then have iconf2': "iconfs (shp s1) ps" using Red_preserves_iconf[OF wwf call] None CallNull by auto
    have "P,shp s1 ⊢b (ps,False) √" by(simp add: bconfs_def)
    then have b2: "P ⊢ ⟨ps,s1,False⟩ [→]* ⟨map Val vs,s2,False⟩" using CallNull.hyps(4)[OF iconf2'] by auto
    then show ?thesis using CallRedsNull[OF b1 b2] by fast
  next
    case (Some a')
    then obtain b1 where b1: "P ⊢ ⟨e,s0,b⟩ →* ⟨null,s1,b1⟩"
      by (metis (no_types, lifting) CallNull.hyps(1) eval_cases(3) rtrancl.rtrancl_refl val_of_spec)
    have fass: "P ⊢ ⟨e∙M(ps),s0,b⟩ →* ⟨null∙M(ps),s1,b1⟩" by(rule CallRedsObj[OF b1])
    then have iconf2': "iconfs (shp s1) ps" using Red_preserves_iconf[OF wwf fass] CallNull by auto
    have bconf2: "P,shp s0 ⊢b (ps,b) √" using CallNull.prems Some by simp
    then have "P,shp s1 ⊢b (ps,b1) √" using Red_preserves_bconf[OF wwf fass CallNull.prems] by simp
    then have b2: "P ⊢ ⟨ps,s1,b1⟩ [→]* ⟨map Val vs,s2,False⟩" using CallNull.hyps(4)[OF iconf2'] by auto
    then show ?thesis using CallRedsNull[OF b1 b2] by fast
  qed
next
  case (CallParamsThrow e s0 v s1 es vs ex es' s2 M) show ?case
  proof(cases "val_of e")
    case None
    then have iconf: "iconf (shp s0) e" using CallParamsThrow.prems(1) by simp
    have bconf: "P,shp s0 ⊢b (e,b) √" using CallParamsThrow.prems(2) None by simp
    then have b1: "P ⊢ ⟨e,s0,b⟩ →* ⟨Val v,s1,False⟩" using CallParamsThrow.hyps(2)[OF iconf] by auto
    have call: "P ⊢ ⟨e∙M(es),s0,b⟩ →* ⟨Val v∙M(es),s1,False⟩" by(rule CallRedsObj[OF b1])
    then have iconf2': "iconfs (shp s1) es" using Red_preserves_iconf[OF wwf call] None CallParamsThrow by auto
    have "P,shp s1 ⊢b (es,False) √" by(simp add: bconfs_def)
    then have b2: "P ⊢ ⟨es,s1,False⟩ [→]* ⟨map Val vs @ throw ex # es',s2,False⟩"
      using CallParamsThrow.hyps(4)[OF iconf2'] by auto
    then show ?thesis using CallRedsThrowParams[OF b1 b2] by fast
  next
    case (Some a')
    then obtain b1 where b1: "P ⊢ ⟨e,s0,b⟩ →* ⟨Val v,s1,b1⟩"
      by (metis (no_types, lifting) CallParamsThrow.hyps(1) eval_cases(3) rtrancl.rtrancl_refl val_of_spec)
    have fass: "P ⊢ ⟨e∙M(es),s0,b⟩ →* ⟨Val v∙M(es),s1,b1⟩" by(rule CallRedsObj[OF b1])
    then have iconf2': "iconfs (shp s1) es" using Red_preserves_iconf[OF wwf fass] CallParamsThrow by auto
    have bconf2: "P,shp s0 ⊢b (es,b) √" using CallParamsThrow.prems Some by simp
    then have "P,shp s1 ⊢b (es,b1) √" using Red_preserves_bconf[OF wwf fass CallParamsThrow.prems] by simp
    then have b2: "P ⊢ ⟨es,s1,b1⟩ [→]* ⟨map Val vs @ throw ex # es',s2,False⟩"
      using CallParamsThrow.hyps(4)[OF iconf2'] by auto
    then show ?thesis using CallRedsThrowParams[OF b1 b2] by fast
  qed
next
  case (CallNone e s0 a s1 ps vs h2 l2 sh2 C fs M) show ?case
  proof(cases "val_of e")
    case None
    then have iconf: "iconf (shp s0) e" using CallNone.prems(1) by simp
    have bconf: "P,shp s0 ⊢b (e,b) √" using CallNone.prems(2) None by simp
    then have b1: "P ⊢ ⟨e,s0,b⟩ →* ⟨addr a,s1,False⟩" using CallNone.hyps(2)[OF iconf] by auto
    have call: "P ⊢ ⟨e∙M(ps),s0,b⟩ →* ⟨addr a∙M(ps),s1,False⟩" by(rule CallRedsObj[OF b1])
    then have iconf2': "iconfs (shp s1) ps" using Red_preserves_iconf[OF wwf call] None CallNone by auto
    have "P,shp s1 ⊢b (ps,False) √" by(simp add: bconfs_def)
    then have b2: "P ⊢ ⟨ps,s1,False⟩ [→]* ⟨map Val vs,(h2, l2, sh2),False⟩"
      using CallNone.hyps(4)[OF iconf2'] by auto
    then show ?thesis using CallRedsNone[OF b1 b2 _ CallNone.hyps(6)] CallNone.hyps(5) by fastforce
  next
    case (Some a')
    then obtain b1 where b1: "P ⊢ ⟨e,s0,b⟩ →* ⟨addr a,s1,b1⟩"
      by (metis (no_types, lifting) CallNone.hyps(1) eval_cases(3) rtrancl.rtrancl_refl val_of_spec)
    have fass: "P ⊢ ⟨e∙M(ps),s0,b⟩ →* ⟨addr a∙M(ps),s1,b1⟩" by(rule CallRedsObj[OF b1])
    then have iconf2': "iconfs (shp s1) ps" using Red_preserves_iconf[OF wwf fass] CallNone by auto
    have bconf2: "P,shp s0 ⊢b (ps,b) √" using CallNone.prems Some by simp
    then have "P,shp s1 ⊢b (ps,b1) √" using Red_preserves_bconf[OF wwf fass CallNone.prems] by simp
    then have b2: "P ⊢ ⟨ps,s1,b1⟩ [→]* ⟨map Val vs,(h2, l2, sh2),False⟩"
      using CallNone.hyps(4)[OF iconf2'] by auto
    then show ?thesis using CallRedsNone[OF b1 b2 _ CallNone.hyps(6)] CallNone.hyps(5) by fastforce
  qed
next
  case (CallStatic e s0 a s1 ps vs h2 l2 sh2 C fs M Ts T m D) show ?case
  proof(cases "val_of e")
    case None
    then have iconf: "iconf (shp s0) e" using CallStatic.prems(1) by simp
    have bconf: "P,shp s0 ⊢b (e,b) √" using CallStatic.prems(2) None by simp
    then have b1: "P ⊢ ⟨e,s0,b⟩ →* ⟨addr a,s1,False⟩" using CallStatic.hyps(2)[OF iconf] by auto
    have call: "P ⊢ ⟨e∙M(ps),s0,b⟩ →* ⟨addr a∙M(ps),s1,False⟩" by(rule CallRedsObj[OF b1])
    then have iconf2': "iconfs (shp s1) ps" using Red_preserves_iconf[OF wwf call] None CallStatic by auto
    have "P,shp s1 ⊢b (ps,False) √" by(simp add: bconfs_def)
    then have b2: "P ⊢ ⟨ps,s1,False⟩ [→]* ⟨map Val vs,(h2, l2, sh2),False⟩"
      using CallStatic.hyps(4)[OF iconf2'] by auto
    then show ?thesis using CallRedsStatic[OF b1 b2 _ CallStatic.hyps(6)] CallStatic.hyps(5) by fastforce
  next
    case (Some a')
    then obtain b1 where b1: "P ⊢ ⟨e,s0,b⟩ →* ⟨addr a,s1,b1⟩"
      by (metis (no_types, lifting) CallStatic.hyps(1) eval_cases(3) rtrancl.rtrancl_refl val_of_spec)
    have call: "P ⊢ ⟨e∙M(ps),s0,b⟩ →* ⟨addr a∙M(ps),s1,b1⟩" by(rule CallRedsObj[OF b1])
    then have iconf2': "iconfs (shp s1) ps" using Red_preserves_iconf[OF wwf call] CallStatic by auto
    have bconf2: "P,shp s0 ⊢b (ps,b) √" using CallStatic.prems Some by simp
    then have "P,shp s1 ⊢b (ps,b1) √" using Red_preserves_bconf[OF wwf call CallStatic.prems] by simp
    then have b2: "P ⊢ ⟨ps,s1,b1⟩ [→]* ⟨map Val vs,(h2, l2, sh2),False⟩"
      using CallStatic.hyps(4)[OF iconf2'] by auto
    then show ?thesis using CallRedsStatic[OF b1 b2 _ CallStatic.hyps(6)] CallStatic.hyps(5) by fastforce
  qed
next
  case (Call e s0 a s1 ps vs h2 l2 sh2 C fs M Ts T pns body D l2' e' h3 l3 sh3) show ?case
  proof(cases "val_of e")
    case None
    then have iconf: "iconf (shp s0) e" using Call.prems(1) by simp
    have bconf: "P,shp s0 ⊢b (e,b) √" using Call.prems(2) None by simp
    then have b1: "P ⊢ ⟨e,s0,b⟩ →* ⟨addr a,s1,False⟩" using Call.hyps(2)[OF iconf] by auto
    have call: "P ⊢ ⟨e∙M(ps),s0,b⟩ →* ⟨addr a∙M(ps),s1,False⟩" by(rule CallRedsObj[OF b1])
    then have iconf2: "iconfs (shp s1) ps" using Red_preserves_iconf[OF wwf call] None Call by auto
    have "P,shp s1 ⊢b (ps,False) √" by(simp add: bconfs_def)
    then have b2: "P ⊢ ⟨ps,s1,False⟩ [→]* ⟨map Val vs,(h2, l2, sh2),False⟩"
      using Call.hyps(4)[OF iconf2] by simp
    have iconf3: "iconf (shp (h2, l2', sh2)) body"
      by(rule nsub_RI_iconf[OF sees_wwf_nsub_RI[OF wwf Call.hyps(6)]])
    have "P,shp (h2, l2', sh2) ⊢b (body,False) √" by(simp add: bconf_def)
    then have b3: "P ⊢ ⟨body,(h2, l2', sh2),False⟩ →* ⟨e',(h3, l3, sh3),False⟩"
      using Call.hyps(10)[OF iconf3] by simp
    show ?thesis by(rule CallRedsFinal[OF wwf b1 b2 Call.hyps(5-8) b3 eval_final[OF Call.hyps(9)]])
  next
    case (Some a')
    then obtain b1 where b1: "P ⊢ ⟨e,s0,b⟩ →* ⟨addr a,s1,b1⟩"
      by (metis (no_types, lifting) Call.hyps(1) eval_cases(3) rtrancl.rtrancl_refl val_of_spec)
    have call: "P ⊢ ⟨e∙M(ps),s0,b⟩ →* ⟨addr a∙M(ps),s1,b1⟩" by(rule CallRedsObj[OF b1])
    then have iconf2': "iconfs (shp s1) ps" using Red_preserves_iconf[OF wwf call] Call by auto
    have bconf2: "P,shp s0 ⊢b (ps,b) √" using Call.prems Some by simp
    then have "P,shp s1 ⊢b (ps,b1) √" using Red_preserves_bconf[OF wwf call Call.prems] by simp
    then have b2: "P ⊢ ⟨ps,s1,b1⟩ [→]* ⟨map Val vs,(h2, l2, sh2),False⟩"
      using Call.hyps(4)[OF iconf2'] by auto
    have iconf3: "iconf (shp (h2, l2', sh2)) body"
      by(rule nsub_RI_iconf[OF sees_wwf_nsub_RI[OF wwf Call.hyps(6)]])
    have "P,shp (h2, l2', sh2) ⊢b (body,False) √" by(simp add: bconf_def)
    then have b3: "P ⊢ ⟨body,(h2, l2', sh2),False⟩ →* ⟨e',(h3, l3, sh3),False⟩"
      using Call.hyps(10)[OF iconf3] by simp
    show ?thesis by(rule CallRedsFinal[OF wwf b1 b2 Call.hyps(5-8) b3 eval_final[OF Call.hyps(9)]])
  qed
next
  case (SCallParamsThrow es s0 vs ex es' s2 C M) show ?case
  proof(cases "map_vals_of es")
    case None
    then have iconf: "iconfs (shp s0) es" using SCallParamsThrow.prems(1) by simp
    have bconf: "P,shp s0 ⊢b (es,b) √" using SCallParamsThrow.prems(2) None by simp
    then have b1: "P ⊢ ⟨es,s0,b⟩ [→]* ⟨map Val vs @ throw ex # es',s2,False⟩"
      using SCallParamsThrow.hyps(2)[OF iconf] by simp
    show ?thesis using SCallRedsThrowParams[OF b1] by simp
  next
    case (Some vs')
    then have "es = map Val vs'" by(rule map_vals_of_spec)
    then show ?thesis using evals_finals_same[OF _ SCallParamsThrow.hyps(1)] map_Val_nthrow_neq
      by auto
  qed
next
  case (SCallNone ps s0 vs s2 C M) show ?case
  proof(cases "map_vals_of ps")
    case None
    then have iconf: "iconfs (shp s0) ps" using SCallNone.prems(1) by simp
    have bconf: "P,shp s0 ⊢b (ps,b) √" using SCallNone.prems(2) None by simp
    then have b1: "P ⊢ ⟨ps,s0,b⟩ [→]* ⟨map Val vs,s2,False⟩" using SCallNone.hyps(2)[OF iconf] by auto
    then show ?thesis using SCallRedsNone[OF b1 SCallNone.hyps(3)] SCallNone.hyps(1) by simp
  next
    case (Some vs')
    then have ps: "ps = map Val vs'" by(rule map_vals_of_spec)
    then have s0: "s0 = s2" using SCallNone.hyps(1) evals_finals_same by blast
    then show ?thesis using RedSCallNone[OF SCallNone.hyps(3)] ps by(cases s2, auto)
  qed
next
  case (SCallNonStatic ps s0 vs s2 C M Ts T m D) show ?case
  proof(cases "map_vals_of ps")
    case None
    then have iconf: "iconfs (shp s0) ps" using SCallNonStatic.prems(1) by simp
    have bconf: "P,shp s0 ⊢b (ps,b) √" using SCallNonStatic.prems(2) None by simp
    then have b1: "P ⊢ ⟨ps,s0,b⟩ [→]* ⟨map Val vs,s2,False⟩" using SCallNonStatic.hyps(2)[OF iconf] by auto
    then show ?thesis using SCallRedsNonStatic[OF b1 SCallNonStatic.hyps(3)] SCallNonStatic.hyps(1) by simp
  next
    case (Some vs')
    then have ps: "ps = map Val vs'" by(rule map_vals_of_spec)
    then have s0: "s0 = s2" using SCallNonStatic.hyps(1) evals_finals_same by blast
    then show ?thesis using RedSCallNonStatic[OF SCallNonStatic.hyps(3)] ps by(cases s2, auto)
  qed
next
  case (SCallInitThrow ps s0 vs h1 l1 sh1 C M Ts T pns body D a s') show ?case
  proof(cases "map_vals_of ps")
    case None
    then have iconf: "iconfs (shp s0) ps" using SCallInitThrow.prems(1) by simp
    have bconf: "P,shp s0 ⊢b (ps,b) √" using SCallInitThrow.prems(2) None by simp
    then have b1: "P ⊢ ⟨ps,s0,b⟩ [→]* ⟨map Val vs,(h1, l1, sh1),False⟩"
      using SCallInitThrow.hyps(2)[OF iconf] by auto
    have bconf2: "P,shp (h1, l1, sh1) ⊢b (INIT D ([D],False) ← unit,False) √" by(simp add: bconf_def)
    then have b2: "P ⊢ ⟨INIT D ([D],False) ← unit,(h1, l1, sh1),False⟩ →* ⟨throw a,s',False⟩"
      using SCallInitThrow.hyps(7) by auto
    then show ?thesis using SCallInitThrowReds[OF wwf b1 SCallInitThrow.hyps(3-5)]
      by(cases s', auto)
  next
    case (Some vs')
    have ps: "ps = map Val vs'" by(rule map_vals_of_spec[OF Some])
    then have vs: "vs = vs' ∧ s0 = (h1, l1, sh1)"
      using evals_finals_same[OF _ SCallInitThrow.hyps(1)] map_Val_eq by auto
    show ?thesis
    proof(cases b)
      case True
      obtain sfs where shC: "sh1 D = ⌊(sfs, Processing)⌋"
        using SCallInitThrow.hyps(3,4) SCallInitThrow.prems(2) True Some vs
          by(auto simp: bconf_def initPD_def dest: sees_method_fun)
      then show ?thesis using init_ProcessingE[OF _ SCallInitThrow.hyps(6)] by blast
    next
      case False
      then have b1: "P ⊢ ⟨ps,s0,b⟩ [→]* ⟨map Val vs,(h1, l1, sh1),False⟩" using ps vs by simp
      have bconf2: "P,shp (h1, l1, sh1) ⊢b (INIT D ([D],False) ← unit,False) √" by(simp add: bconf_def)
      then have b2: "P ⊢ ⟨INIT D ([D],False) ← unit,(h1, l1, sh1),False⟩ →* ⟨throw a,s',False⟩"
        using SCallInitThrow.hyps(7) by auto
      then show ?thesis using SCallInitThrowReds[OF wwf b1 SCallInitThrow.hyps(3-5)] by(cases s', auto)
    qed
  qed
next
  case (SCallInit ps s0 vs h1 l1 sh1 C M Ts T pns body D v' h2 l2 sh2 l2' e' h3 l3 sh3) show ?case
  proof(cases "map_vals_of ps")
    case None
    then have iconf: "iconfs (shp s0) ps" using SCallInit.prems(1) by simp
    have bconf: "P,shp s0 ⊢b (ps,b) √" using SCallInit.prems(2) None by simp
    then have b1: "P ⊢ ⟨ps,s0,b⟩ [→]* ⟨map Val vs,(h1, l1, sh1),False⟩"
      using SCallInit.hyps(2)[OF iconf] by auto
    have bconf2: "P,shp (h1, l1, sh1) ⊢b (INIT D ([D],False) ← unit,False) √" by(simp add: bconf_def)
    then have b2: "P ⊢ ⟨INIT D ([D],False) ← unit,(h1, l1, sh1),False⟩ →* ⟨Val v',(h2, l2, sh2),False⟩"
      using SCallInit.hyps(7) by auto
    have iconf3: "iconf (shp (h2, l2', sh2)) body"
      by(rule nsub_RI_iconf[OF sees_wwf_nsub_RI[OF wwf SCallInit.hyps(3)]])
    have "P,shp (h2, l2', sh2) ⊢b (body,False) √" by(simp add: bconf_def)
    then have b3: "P ⊢ ⟨body,(h2, l2', sh2),False⟩ →* ⟨e',(h3, l3, sh3),False⟩"
      using SCallInit.hyps(11)[OF iconf3] by simp
    show ?thesis by(rule SCallInitReds[OF wwf b1 SCallInit.hyps(3-5) b2 SCallInit.hyps(8-9)
                           b3 eval_final[OF SCallInit.hyps(10)]])
  next
    case (Some vs')
    then have ps: "ps = map Val vs'" by(rule map_vals_of_spec)
    then have vs: "vs = vs' ∧ s0 = (h1, l1, sh1)"
      using evals_finals_same[OF _ SCallInit.hyps(1)] map_Val_eq by auto
    show ?thesis
    proof(cases b)
      case True
      then have b1: "P ⊢ ⟨ps,s0,b⟩ [→]* ⟨map Val vs,(h1, l1, sh1),b⟩" using ps vs by simp
      obtain sfs where shC: "sh1 D = ⌊(sfs, Processing)⌋"
        using SCallInit.hyps(3,4) SCallInit.prems(2) True Some vs
          by(auto simp: bconf_def initPD_def dest: sees_method_fun)
      then have s': "(h1, l1, sh1) = (h2, l2, sh2)" using init_ProcessingE[OF _ SCallInit.hyps(6)] by simp
      have iconf3: "iconf (shp (h2, l2', sh2)) body"
        by(rule nsub_RI_iconf[OF sees_wwf_nsub_RI[OF wwf SCallInit.hyps(3)]])
      have "P,shp (h2, l2', sh2) ⊢b (body,False) √" by(simp add: bconf_def)
      then have b3: "P ⊢ ⟨body,(h2, l2', sh2),False⟩ →* ⟨e',(h3, l3, sh3),False⟩"
        using SCallInit.hyps(11)[OF iconf3] by simp
      then have b3': "P ⊢ ⟨body,(h1, l2', sh1),False⟩ →* ⟨e',(h3, l3, sh3),False⟩"
        using s' by simp
      then show ?thesis using SCallInitProcessingReds[OF wwf b1 SCallInit.hyps(3) shC
                           SCallInit.hyps(8-9) b3' eval_final[OF SCallInit.hyps(10)]] s' by simp
    next
      case False
      then have b1: "P ⊢ ⟨ps,s0,b⟩ [→]* ⟨map Val vs,(h1, l1, sh1),False⟩" using ps vs by simp
      have bconf2: "P,shp (h1, l1, sh1) ⊢b (INIT D ([D],False) ← unit,False) √" by(simp add: bconf_def)
      then have b2: "P ⊢ ⟨INIT D ([D],False) ← unit,(h1, l1, sh1),False⟩ →* ⟨Val v',(h2, l2, sh2),False⟩"
        using SCallInit.hyps(7) by auto
      have iconf3: "iconf (shp (h2, l2', sh2)) body"
        by(rule nsub_RI_iconf[OF sees_wwf_nsub_RI[OF wwf SCallInit.hyps(3)]])
      have "P,shp (h2, l2', sh2) ⊢b (body,False) √" by(simp add: bconf_def)
      then have b3: "P ⊢ ⟨body,(h2, l2', sh2),False⟩ →* ⟨e',(h3, l3, sh3),False⟩"
        using SCallInit.hyps(11)[OF iconf3] by simp
      show ?thesis by(rule SCallInitReds[OF wwf b1 SCallInit.hyps(3-5) b2 SCallInit.hyps(8-9)
                             b3 eval_final[OF SCallInit.hyps(10)]])
    qed
  qed
next
  case (SCall ps s0 vs h2 l2 sh2 C M Ts T pns body D sfs l2' e' h3 l3 sh3) show ?case
  proof(cases "map_vals_of ps")
    case None
    then have iconf: "iconfs (shp s0) ps" using SCall.prems(1) by simp
    have bconf: "P,shp s0 ⊢b (ps,b) √" using SCall.prems(2) None by simp
    then have b1: "P ⊢ ⟨ps,s0,b⟩ [→]* ⟨map Val vs,(h2, l2, sh2),False⟩"
      using SCall.hyps(2)[OF iconf] by auto
    have iconf3: "iconf (shp (h2, l2', sh2)) body"
      by(rule nsub_RI_iconf[OF sees_wwf_nsub_RI[OF wwf SCall.hyps(3)]])
    have "P,shp (h2, l2', sh2) ⊢b (body,False) √" by(simp add: bconf_def)
    then have b2: "P ⊢ ⟨body,(h2, l2', sh2),False⟩ →* ⟨e',(h3, l3, sh3),False⟩"
      using SCall.hyps(8)[OF iconf3] by simp
    show ?thesis by(rule SCallRedsFinal[OF wwf b1 SCall.hyps(3-6) b2 eval_final[OF SCall.hyps(7)]])
  next
    case (Some vs')
    then have ps: "ps = map Val vs'" by(rule map_vals_of_spec)
    then have vs: "vs = vs' ∧ s0 = (h2, l2, sh2)"
      using evals_finals_same[OF _ SCall.hyps(1)] map_Val_eq by auto
    then have b1: "P ⊢ ⟨ps,s0,b⟩ [→]* ⟨map Val vs,(h2, l2, sh2),b⟩" using ps by simp
    have iconf3: "iconf (shp (h2, l2', sh2)) body"
      by(rule nsub_RI_iconf[OF sees_wwf_nsub_RI[OF wwf SCall.hyps(3)]])
    have "P,shp (h2, l2', sh2) ⊢b (body,False) √" by(simp add: bconf_def)
    then have b2: "P ⊢ ⟨body,(h2, l2', sh2),False⟩ →* ⟨e',(h3, l3, sh3),False⟩"
      using SCall.hyps(8)[OF iconf3] by simp
    show ?thesis by(rule SCallRedsFinal[OF wwf b1 SCall.hyps(3-6) b2 eval_final[OF SCall.hyps(7)]])
  qed
next
  case (Block e0 h0 l0 V sh0 e1 h1 l1 sh1 T)
  have iconf: "iconf (shp (h0, l0(V := None), sh0)) e0"
    using Block.prems(1) by (auto simp: assigned_def)
  have bconf: "P,shp (h0, l0(V := None), sh0) ⊢b (e0,b) √" using Block.prems(2)
    by(auto simp: bconf_def)
  then have b': "P ⊢ ⟨e0,(h0, l0(V := None), sh0),b⟩ →* ⟨e1,(h1, l1, sh1),False⟩"
    using Block.hyps(2)[OF iconf] by auto
  have fin: "final e1" using Block by(auto dest: eval_final)
  thus ?case using BlockRedsFinal[OF b' fin] by simp
next
  case (Seq e0 s0 v s1 e1 e2 s2)
  then have iconf: "iconf (shp s0) e0" using Seq.prems(1)
    by(auto dest: val_of_spec lass_val_of_spec)
  have b1: "∃b1. P ⊢ ⟨e0,s0,b⟩ →* ⟨Val v,s1,b1⟩"
  proof(cases "val_of e0")
    case None show ?thesis
    proof(cases "lass_val_of e0")
      case lNone:None
      then have bconf: "P,shp s0 ⊢b (e0,b) √" using Seq.prems(2) None by simp
      then have "P ⊢ ⟨e0,s0,b⟩ →* ⟨Val v,s1,False⟩" using iconf Seq.hyps(2) by auto
      then show ?thesis by fast
    next
      case (Some p)
      obtain V' v' where p: "p = (V',v')" and e0: "e0 = V':=Val v'"
        using lass_val_of_spec[OF Some] by(cases p, auto)
      obtain h l sh h' l' sh' where s0: "s0 = (h,l,sh)" and s1: "s1 = (h',l',sh')" by(cases s0, cases s1)
      then have eval: "P ⊢ ⟨e0,(h,l,sh)⟩ ⇒ ⟨Val v,(h',l',sh')⟩" using Seq.hyps(1) by simp
      then have s1': "Val v = unit ∧ h' = h ∧ l' = l(V' ↦ v') ∧ sh' = sh"
        using lass_val_of_eval[OF Some eval] p e0 by simp
      then have "P ⊢ ⟨e0,s0,b⟩ → ⟨Val v,s1,b⟩" using e0 s0 s1 by(auto intro: RedLAss)
      then show ?thesis by auto
    qed
  next
    case (Some a)
    then have "e0 = Val v" and "s0 = s1" using Seq.hyps(1) eval_cases(3) val_of_spec by blast+
    then show ?thesis using Seq by auto
  qed
  then obtain b1 where b1': "P ⊢ ⟨e0,s0,b⟩ →* ⟨Val v,s1,b1⟩" by clarsimp
  have seq: "P ⊢ ⟨e0;;e1,s0,b⟩ →* ⟨Val v;;e1,s1,b1⟩" by(rule SeqReds[OF b1'])
  then have iconf2: "iconf (shp s1) e1" using Red_preserves_iconf[OF wwf seq] Seq nsub_RI_iconf
    by auto
  have "P,shp s1 ⊢b (Val v;; e1,b1) √" by(rule Red_preserves_bconf[OF wwf seq Seq.prems])
  then have bconf2: "P,shp s1 ⊢b (e1,b1) √" by simp
  have b2: "P ⊢ ⟨e1,s1,b1⟩ →* ⟨e2,s2,False⟩" by(rule Seq.hyps(4)[OF iconf2 bconf2])
  then show ?case using SeqReds2[OF b1' b2] by fast
next
  case (SeqThrow e0 s0 a s1 e1 b)
  have notVal: "val_of e0 = None" "lass_val_of e0 = None"
    using SeqThrow.hyps(1) eval_throw_nonVal eval_throw_nonLAss by auto
  thus ?case using SeqThrow notVal by(auto dest!:eval_final dest: SeqRedsThrow)
next
  case (CondT e s0 s1 e1 e' s2 e2)
  then have iconf: "iconf (shp s0) e" using CondT.prems(1) by auto
  have bconf: "P,shp s0 ⊢b (e,b) √" using CondT.prems(2) by auto
  then have b1: "P ⊢ ⟨e,s0,b⟩ →* ⟨true,s1,False⟩" using iconf CondT.hyps(2) by auto
  have cond: "P ⊢ ⟨if (e) e1 else e2,s0,b⟩ →* ⟨if (true) e1 else e2,s1,False⟩" by(rule CondReds[OF b1])
  then have iconf2': "iconf (shp s1) e1" using Red_preserves_iconf[OF wwf cond] CondT nsub_RI_iconf
    by auto
  have "P,shp s1 ⊢b (e1,False) √" by(simp add: bconf_def)
  then have b2: "P ⊢ ⟨e1,s1,False⟩ →* ⟨e',s2,False⟩" using CondT.hyps(4)[OF iconf2'] by auto
  then show ?case using CondReds2T[OF b1 b2] by fast
next
  case (CondF e s0 s1 e2 e' s2 e1)
  then have iconf: "iconf (shp s0) e" using CondF.prems(1) by auto
  have bconf: "P,shp s0 ⊢b (e,b) √" using CondF.prems(2) by auto
  then have b1: "P ⊢ ⟨e,s0,b⟩ →* ⟨false,s1,False⟩" using iconf CondF.hyps(2) by auto
  have cond: "P ⊢ ⟨if (e) e1 else e2,s0,b⟩ →* ⟨if (false) e1 else e2,s1,False⟩" by(rule CondReds[OF b1])
  then have iconf2': "iconf (shp s1) e2" using Red_preserves_iconf[OF wwf cond] CondF nsub_RI_iconf
    by auto
  have "P,shp s1 ⊢b (e2,False) √" by(simp add: bconf_def)
  then have b2: "P ⊢ ⟨e2,s1,False⟩ →* ⟨e',s2,False⟩" using CondF.hyps(4)[OF iconf2'] by auto
  then show ?case using CondReds2F[OF b1 b2] by fast
next
  case CondThrow thus ?case by(auto dest!:eval_final dest:CondRedsThrow)
next
  case (WhileF e s0 s1 c)
  then have iconf: "iconf (shp s0) e" using nsub_RI_iconf by auto
  then have bconf: "P,shp s0 ⊢b (e,b) √" using WhileF.prems(2) by(simp add: bconf_def)
  then have b': "P ⊢ ⟨e,s0,b⟩ →* ⟨false,s1,False⟩" using WhileF.hyps(2) iconf by auto
  thus ?case using WhileFReds[OF b'] by fast
next
  case (WhileT e s0 s1 c v1 s2 e3 s3)
  then have iconf: "iconf (shp s0) e" using nsub_RI_iconf by auto
  then have bconf: "P,shp s0 ⊢b (e,b) √" using WhileT.prems(2) by(simp add: bconf_def)
  then have b1: "P ⊢ ⟨e,s0,b⟩ →* ⟨true,s1,False⟩" using WhileT.hyps(2) iconf by auto
  have iconf2: "iconf (shp s1) c" using WhileT.prems(1) nsub_RI_iconf by auto
  have bconf2: "P,shp s1 ⊢b (c,False) √" by(simp add: bconf_def)
  then have b2: "P ⊢ ⟨c,s1,False⟩ →* ⟨Val v1,s2,False⟩" using WhileT.hyps(4) iconf2 by auto
  have iconf3: "iconf (shp s2) (while (e) c)" using WhileT.prems(1) by auto
  have "P,shp s2 ⊢b (while (e) c,False) √" by(simp add: bconf_def)
  then have b3: "P ⊢ ⟨while (e) c,s2,False⟩ →* ⟨e3,s3,False⟩" using WhileT.hyps(6) iconf3 by auto
  show ?case using WhileTReds[OF b1 b2 b3] by fast
next
  case WhileCondThrow thus ?case
    by (metis (no_types, lifting) WhileRedsThrow iconf.simps(16) bconf_While bconf_def nsub_RI_iconf)
next
  case (WhileBodyThrow e s0 s1 c e' s2)
  then have iconf: "iconf (shp s0) e" using nsub_RI_iconf by auto
  then have bconf: "P,shp s0 ⊢b (e,b) √" using WhileBodyThrow.prems(2) by(simp add: bconf_def)
  then have b1: "P ⊢ ⟨e,s0,b⟩ →* ⟨true,s1,False⟩" using WhileBodyThrow.hyps(2) iconf by auto
  have iconf2: "iconf (shp s1) c" using WhileBodyThrow.prems(1) nsub_RI_iconf by auto
  have bconf2: "P,shp s1 ⊢b (c,False) √" by(simp add: bconf_def)
  then have b2: "P ⊢ ⟨c,s1,False⟩ →* ⟨throw e',s2,False⟩" using WhileBodyThrow.hyps(4) iconf2 by auto
  show ?case using WhileTRedsThrow[OF b1 b2] by fast
next
  case Throw thus ?case by (meson ThrowReds iconf.simps(17) bconf_Throw)
next
  case ThrowNull thus ?case by (meson ThrowRedsNull iconf.simps(17) bconf_Throw)
next
  case ThrowThrow thus ?case by (meson ThrowRedsThrow iconf.simps(17) bconf_Throw)
next
  case Try thus ?case by (meson TryRedsVal iconf.simps(18) bconf_Try)
next
  case (TryCatch e1 s0 a h1 l1 sh1 D fs C e2 V e2' h2 l2 sh2)
  then have b1: "P ⊢ ⟨e1,s0,b⟩ →* ⟨Throw a,(h1, l1, sh1),False⟩" by auto
  have Try: "P ⊢ ⟨try e1 catch(C V) e2,s0,b⟩ →* ⟨try (Throw a) catch(C V) e2,(h1, l1, sh1),False⟩"
    by(rule TryReds[OF b1])
  have iconf: "iconf sh1 e2" using Red_preserves_iconf[OF wwf Try] TryCatch nsub_RI_iconf
    by auto
  have bconf: "P,shp (h1, l1(V ↦ Addr a), sh1) ⊢b (e2,False) √" by(simp add: bconf_def)
  then have b2: "P ⊢ ⟨e2,(h1, l1(V ↦ Addr a), sh1),False⟩ →* ⟨e2',(h2, l2, sh2),False⟩"
    using TryCatch.hyps(6) iconf by auto
  thus ?case using TryCatchRedsFinal[OF b1] TryCatch.hyps(3-5) by (meson eval_final)
next
  case TryThrow thus ?case by (meson TryRedsFail iconf.simps(18) bconf_Try)
next
  case Nil thus ?case by(auto simp: bconfs_def)
next
  case (Cons e s0 v s1 es es' s2) show ?case
  proof(cases "val_of e")
    case None
    then have iconf: "iconf (shp s0) e" using Cons.prems(1) by simp
    have bconf: "P,shp s0 ⊢b (e,b) √" using Cons.prems(2) None by simp
    then have b1: "P ⊢ ⟨e,s0,b⟩ →* ⟨Val v,s1,False⟩" using Cons.hyps(2) iconf by auto
    have cons: "P ⊢ ⟨e # es,s0,b⟩ [→]* ⟨Val v # es,s1,False⟩" by(rule ListReds1[OF b1])
    then have iconf2': "iconfs (shp s1) es" using Reds_preserves_iconf[OF wwf cons] None Cons by auto
    have "P,shp s1 ⊢b (es,False) √" by(simp add: bconfs_def)
    then have b2: "P ⊢ ⟨es,s1,False⟩ [→]* ⟨es',s2,False⟩" using Cons.hyps(4)[OF iconf2'] by auto
    show ?thesis using ListRedsVal[OF b1 b2] by auto
  next
    case (Some a)
    then obtain b1 where b1: "P ⊢ ⟨e,s0,b⟩ →* ⟨Val v,s1,b1⟩"
      by (metis (no_types, lifting) Cons.hyps(1) eval_cases(3) rtrancl.rtrancl_refl val_of_spec)
    have cons: "P ⊢ ⟨e # es,s0,b⟩ [→]* ⟨Val v # es,s1,b1⟩" by(rule ListReds1[OF b1])
    then have iconf2': "iconfs (shp s1) es" using Reds_preserves_iconf[OF wwf cons] Cons by auto
    have bconf2: "P,shp s0 ⊢b (es,b) √" using Cons.prems Some by simp
    then have "P,shp s1 ⊢b (es,b1) √" using Reds_preserves_bconf[OF wwf cons Cons.prems] by simp
    then have b2: "P ⊢ ⟨es,s1,b1⟩ [→]* ⟨es',s2,False⟩" using Cons.hyps(4)[OF iconf2'] by auto
    show ?thesis using ListRedsVal[OF b1 b2] by auto
  qed
next
  case (ConsThrow e s0 e' s1 es) show ?case
  proof(cases "val_of e")
    case None
    then have iconf: "iconf (shp s0) e" using ConsThrow.prems(1) by simp
    have bconf: "P,shp s0 ⊢b (e,b) √" using ConsThrow.prems(2) None by simp
    then have b1: "P ⊢ ⟨e,s0,b⟩ →* ⟨throw e',s1,False⟩" using ConsThrow.hyps(2) iconf by auto
    have cons: "P ⊢ ⟨e # es,s0,b⟩ [→]* ⟨throw e' # es,s1,False⟩" by(rule ListReds1[OF b1])
    then show ?thesis by fast
  next
    case (Some a)
    then show ?thesis using eval_final_same[OF ConsThrow.hyps(1)] val_of_spec[OF Some] by auto
  qed
next
  case (InitFinal e s e' s' C b')
  then have "¬sub_RI e" by simp
  then show ?case using InitFinal RedInit[of e C b' s b P]
    by (meson converse_rtrancl_into_rtrancl nsub_RI_iconf red_preserves_bconf RedInit)
next
  case (InitNone sh C C' Cs e h l e' s')
  then have init: "P ⊢ ⟨INIT C' (C # Cs,False) ← e,(h, l, sh(C ↦ (sblank P C, Prepared))),b⟩ →* ⟨e',s',False⟩"
    by(simp add: bconf_def)
  show ?case by(rule InitNoneReds[OF InitNone.hyps(1) init])
next
  case (InitDone sh C sfs C' Cs e h l e' s')
  then have "iconf (shp (h, l, sh)) (INIT C' (Cs,True) ← e)" using InitDone.hyps(1)
  proof(cases Cs)
    case Nil
    then have "C = C'" "¬sub_RI e" using InitDone.prems(1) by simp+
    then show ?thesis using Nil InitDone.hyps(1) by(simp add: initPD_def)
  qed(auto)
  then have init: "P ⊢ ⟨INIT C' (Cs,True) ← e,(h, l, sh),b⟩ →* ⟨e',s',False⟩"
    using InitDone by(simp add: bconf_def)
  show ?case by(rule InitDoneReds[OF InitDone.hyps(1) init])
next
  case (InitProcessing sh C sfs C' Cs e h l e' s')
  then have "iconf (shp (h, l, sh)) (INIT C' (Cs,True) ← e)" using InitProcessing.hyps(1)
  proof(cases Cs)
    case Nil
    then have "C = C'" "¬sub_RI e" using InitProcessing.prems(1) by simp+
    then show ?thesis using Nil InitProcessing.hyps(1) by(simp add: initPD_def)
  qed(auto)
  then have init: "P ⊢ ⟨INIT C' (Cs,True) ← e,(h, l, sh),b⟩ →* ⟨e',s',False⟩"
    using InitProcessing by(simp add: bconf_def)
  show ?case by(rule InitProcessingReds[OF InitProcessing.hyps(1) init])
next
  case InitError thus ?case by(fastforce intro: InitErrorReds simp: bconf_def)
next
  case InitObject thus ?case by(fastforce intro: InitObjectReds simp: bconf_def)
next
  case InitNonObject thus ?case by(fastforce intro: InitNonObjectReds simp: bconf_def)
next
  case InitRInit thus ?case by(fastforce intro: RedsInitRInit simp: bconf_def)
next
  case (RInit e s v h' l' sh' C sfs i sh'' C' Cs e' e1 s1)
  then have iconf2: "iconf (shp (h', l', sh'')) (INIT C' (Cs,True) ← e')"
    by(auto simp: initPD_def fun_upd_same list_nonempty_induct)
  show ?case
  proof(cases "val_of e")
    case None
    then have iconf: "iconf (shp s) e" using RInit.prems(1) by simp
    have bconf: "P,shp s ⊢b (e,b) √" using RInit.prems(2) None by simp
    then have b1: "P ⊢ ⟨e,s,b⟩ →* ⟨Val v,(h',l',sh'),False⟩" using RInit.hyps(2)[OF iconf] by auto
    have "P,shp (h', l', sh'') ⊢b (INIT C' (Cs,True) ← e',False) √" by(simp add: bconf_def)
    then have b2: "P ⊢ ⟨INIT C' (Cs,True) ← e',(h',l',sh''),False⟩ →* ⟨e1,s1,False⟩"
      using RInit.hyps(7)[OF iconf2] by auto
    then show ?thesis using RedsRInit[OF b1 RInit.hyps(3-5) b2] by fast
  next
    case (Some a')
    then obtain b1 where b1: "P ⊢ ⟨e,s,b⟩ →* ⟨Val v,(h',l',sh'),b1⟩"
      by (metis (no_types, lifting) RInit.hyps(1) eval_cases(3) rtrancl.rtrancl_refl val_of_spec)
    have fin: "final e" by(simp add: val_of_spec[OF Some])
    have "¬b" using RInit.prems(2) Some by(simp add: bconf_def)
    then have nb1: "¬b1" using reds_final_same[OF b1 fin] by simp
    have "P,shp (h', l', sh'') ⊢b (INIT C' (Cs,True) ← e',b1) √" using nb1
      by(simp add: bconf_def)
    then have b2: "P ⊢ ⟨INIT C' (Cs,True) ← e',(h', l', sh''),b1⟩ →* ⟨e1,s1,False⟩"
      using RInit.hyps(7)[OF iconf2] by auto
    then show ?thesis using RedsRInit[OF b1 RInit.hyps(3-5) b2] by fast
  qed
next
  case (RInitInitFail e s a h' l' sh' C sfs i sh'' D Cs e' e1 s1)
  have fin: "final (throw a)" using eval_final[OF RInitInitFail.hyps(1)] by simp
  then obtain a' where a': "throw a = Throw a'" by auto
  have iconf2: "iconf (shp (h', l', sh'')) (RI (D,Throw a') ; Cs ← e')"
    using RInitInitFail.prems(1) by auto
  show ?case
  proof(cases "val_of e")
    case None
    then have iconf: "iconf (shp s) e" using RInitInitFail.prems(1) by simp
    have bconf: "P,shp s ⊢b (e,b) √" using RInitInitFail.prems(2) None by simp
    then have b1: "P ⊢ ⟨e,s,b⟩ →* ⟨Throw a',(h',l',sh'),False⟩"
      using RInitInitFail.hyps(2)[OF iconf] a' by auto
    have "P,shp (h', l', sh'') ⊢b (RI (D,Throw a') ; Cs ← e',False) √" by(simp add: bconf_def)
    then have b2: "P ⊢ ⟨RI (D,Throw a') ; Cs ← e',(h',l',sh''),False⟩ →* ⟨e1,s1,False⟩"
      using RInitInitFail.hyps(6) iconf2 a' by auto
    show ?thesis using RInitInitThrowReds[OF b1 RInitInitFail.hyps(3-4) b2] by fast
  next
    case (Some a1)
    then obtain b1 where b1: "P ⊢ ⟨e,s,b⟩ →* ⟨Throw a',(h',l',sh'),b1⟩" using a'
      by (metis (no_types, lifting) RInitInitFail.hyps(1) eval_cases(3) rtrancl.rtrancl_refl val_of_spec)
    have fin: "final e" by(simp add: val_of_spec[OF Some])
    have "¬b" using RInitInitFail.prems(2) Some by(simp add: bconf_def)
    then have nb1: "¬b1" using reds_final_same[OF b1 fin] by simp
    have "P,shp (h', l', sh'') ⊢b (RI (D,Throw a') ; Cs ← e',b1) √" using nb1
      by(simp add: bconf_def)
    then have b2: "P ⊢ ⟨RI (D,Throw a') ; Cs ← e',(h', l', sh''),b1⟩ →* ⟨e1,s1,False⟩"
      using RInitInitFail.hyps(6) iconf2 a' by auto
    show ?thesis using RInitInitThrowReds[OF b1 RInitInitFail.hyps(3-4) b2] by fast
  qed
next
  case (RInitFailFinal e s a h' l' sh' C sfs i sh'' e')
  have fin: "final (throw a)" using eval_final[OF RInitFailFinal.hyps(1)] by simp
  then obtain a' where a': "throw a = Throw a'" by auto
  show ?case
  proof(cases "val_of e")
    case None
    then have iconf: "iconf (shp s) e" using RInitFailFinal.prems(1) by simp
    have bconf: "P,shp s ⊢b (e,b) √" using RInitFailFinal.prems(2) None by simp
    then have b1: "P ⊢ ⟨e,s,b⟩ →* ⟨Throw a',(h',l',sh'),False⟩"
      using RInitFailFinal.hyps(2)[OF iconf] a' by auto
    show ?thesis using RInitThrowReds[OF b1 RInitFailFinal.hyps(3-4)] a' by fast
  next
    case (Some a1)
    then show ?thesis using eval_final_same[OF RInitFailFinal.hyps(1)] val_of_spec[OF Some] by auto
  qed
qed
(*>*)


subsection‹Big steps simulates small step›

text‹ This direction was carried out by Norbert Schirmer and Daniel
Wasserrab (and modified to include statics and DCI by Susannah Mansky). ›

text ‹ The big step equivalent of @{text RedWhile}: › 

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


lemma blocksEval:
  "⋀Ts vs l l'. ⟦size ps = size Ts; size ps = size vs; P ⊢ ⟨blocks(ps,Ts,vs,e),(h,l,sh)⟩ ⇒ ⟨e',(h',l',sh')⟩ ⟧
    ⟹ ∃ l''. P ⊢ ⟨e,(h,l(ps[↦]vs),sh)⟩ ⇒ ⟨e',(h',l'',sh')⟩"
(*<*)
proof (induct ps)
  case Nil then show ?case by fastforce
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
  have "P ⊢ ⟨blocks (p # ps', Ts, vs, e),(h,l,sh)⟩ ⇒ ⟨e',(h', l',sh')⟩" by fact
  with Ts vs 
  have "P ⊢ ⟨{p:T := Val v; blocks (ps', Ts', vs', e)},(h,l,sh)⟩ ⇒ ⟨e',(h', l',sh')⟩"
    by simp
  then obtain l''' where
    eval_ps': "P ⊢ ⟨blocks (ps', Ts', vs', e),(h, l(p↦v), sh)⟩ ⇒ ⟨e',(h', l''', sh')⟩"
    and l''': "l'=l'''(p:=l p)"
    by (auto elim!: eval_cases)
  then obtain l'' where 
    hyp: "P ⊢ ⟨e,(h, l(p↦v, ps'[↦]vs'), sh)⟩ ⇒ ⟨e',(h', l'', sh')⟩"
    using length_eqs Ts vs Cons.hyps [OF _ _ eval_ps'] by auto
  from hyp
  show "∃l''. P ⊢ ⟨e,(h, l(p # ps'[↦]vs), sh)⟩ ⇒ ⟨e',(h', l'', sh')⟩"
    using Ts vs by auto
qed
(*>*)

lemma
assumes wf: "wwf_J_prog P"
shows eval_restrict_lcl:
  "P ⊢ ⟨e,(h,l,sh)⟩ ⇒ ⟨e',(h',l',sh')⟩ ⟹ (⋀W. fv e ⊆ W ⟹ P ⊢ ⟨e,(h,l|`W,sh)⟩ ⇒ ⟨e',(h',l'|`W,sh')⟩)"
and "P ⊢ ⟨es,(h,l,sh)⟩ [⇒] ⟨es',(h',l',sh')⟩ ⟹ (⋀W. fvs es ⊆ W ⟹ P ⊢ ⟨es,(h,l|`W,sh)⟩ [⇒] ⟨es',(h',l'|`W,sh')⟩)"
(*<*)
proof(induct rule:eval_evals_inducts)
  case (Block e0 h0 l0 V sh0 e1 h1 l1 sh1 T)
  have IH: "⋀W. fv e0 ⊆ W ⟹ P ⊢ ⟨e0,(h0,l0(V:=None)|`W,sh0)⟩ ⇒ ⟨e1,(h1,l1|`W,sh1)⟩" by fact
  have "fv({V:T; e0}) ⊆ W" by fact+
  hence "fv e0 - {V} ⊆ W" by simp_all
  hence "fv e0 ⊆ insert V W" by fast
  from IH[OF this]
  have "P ⊢ ⟨e0,(h0, (l0|`W)(V := None), sh0)⟩ ⇒ ⟨e1,(h1, l1|`insert V W, sh1)⟩"
    by fastforce
  from eval_evals.Block[OF this] show ?case by fastforce
next
  case Seq thus ?case by simp (blast intro:eval_evals.Seq)
next
  case New thus ?case by(simp add:eval_evals.intros)
next
  case NewFail thus ?case by(simp add:eval_evals.intros)
next
  case (NewInit sh C h l v' h' l' sh' a h'')
  have "fv(INIT C ([C],False) ← unit) ⊆ W" by simp
  then have "P ⊢ ⟨INIT C ([C],False) ← unit,(h, l |` W, sh)⟩ ⇒ ⟨Val v',(h', l' |` W, sh')⟩"
    by (simp add: NewInit.hyps(3))
  thus ?case using NewInit.hyps(1,4-6) eval_evals.NewInit by blast
next
  case (NewInitOOM sh C h l v' h' l' sh')
  have "fv(INIT C ([C],False) ← unit) ⊆ W" by simp
  then have "P ⊢ ⟨INIT C ([C],False) ← unit,(h, l |` W, sh)⟩ ⇒ ⟨Val v',(h', l' |` W, sh')⟩"
    by (simp add: NewInitOOM.hyps(3))
  thus ?case
    using NewInitOOM.hyps(1,4,5) eval_evals.NewInitOOM by auto
next
  case NewInitThrow thus ?case by(simp add:eval_evals.intros)
next
  case Cast thus ?case by simp (blast intro:eval_evals.Cast)
next
  case CastNull thus ?case by simp (blast intro:eval_evals.CastNull)
next
  case CastFail thus ?case by simp (blast intro:eval_evals.CastFail)
next
  case CastThrow 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 h0 l0 sh0 v h l sh l' V)
  have IH: "⋀W. fv e ⊆ W ⟹ P ⊢ ⟨e,(h0,l0|`W,sh0)⟩ ⇒ ⟨Val v,(h,l|`W,sh)⟩"
   and [simp]: "l' = l(V ↦ v)" by fact+
  have "fv (V:=e) ⊆ W" by fact
  hence fv: "fv e ⊆ W" and VinW: "V ∈ W" by auto
  from eval_evals.LAss[OF IH[OF fv] refl, of V] VinW
  show ?case by simp
next
  case LAssThrow thus ?case by(fastforce intro: eval_evals.LAssThrow)
next
  case FAcc thus ?case by simp (blast intro: eval_evals.FAcc)
next
  case FAccNull thus ?case by(fastforce intro: eval_evals.FAccNull)
next
  case FAccThrow thus ?case by(fastforce intro: eval_evals.FAccThrow)
next
  case FAccNone thus ?case by(metis eval_evals.FAccNone fv.simps(7))
next
  case FAccStatic thus ?case by(metis eval_evals.FAccStatic fv.simps(7))
next
  case SFAcc thus ?case by simp (blast intro: eval_evals.SFAcc)
next
  case SFAccInit thus ?case by simp (blast intro: eval_evals.SFAccInit)
next
  case SFAccInitThrow thus ?case by simp (blast intro: eval_evals.SFAccInitThrow)
next
  case SFAccNone thus ?case by simp (blast intro: eval_evals.SFAccNone)
next
  case SFAccNonStatic thus ?case by simp (blast intro: eval_evals.SFAccNonStatic)
next
  case FAss thus ?case by simp (blast intro: eval_evals.FAss)
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 FAssNone thus ?case by simp (blast intro: eval_evals.FAssNone)
next
  case FAssStatic thus ?case by simp (blast intro: eval_evals.FAssStatic)
next
  case SFAss thus ?case by simp (blast intro: eval_evals.SFAss)
next
  case SFAssInit thus ?case by simp (blast intro: eval_evals.SFAssInit)
next
  case SFAssInitThrow thus ?case by simp (blast intro: eval_evals.SFAssInitThrow)
next
  case SFAssThrow thus ?case by simp (blast intro: eval_evals.SFAssThrow)
next
  case SFAssNone thus ?case by simp (blast intro: eval_evals.SFAssNone)
next
  case SFAssNonStatic thus ?case by simp (blast intro: eval_evals.SFAssNonStatic)
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 (CallNone e h l sh a h' l' sh' ps vs h2 l2 sh2 C fs M)
  have f1: "P ⊢ ⟨e,(h, l |` W, sh)⟩ ⇒ ⟨addr a,(h', l' |` W, sh')⟩"
    by (metis (no_types) fv.simps(11) le_sup_iff local.CallNone(2) local.CallNone(7))
  have "P ⊢ ⟨ps,(h', l' |` W, sh')⟩ [⇒] ⟨map Val vs, (h2, l2 |` W, sh2)⟩"
    using local.CallNone(4) local.CallNone(7) by auto
  then show ?case
    using f1 eval_evals.CallNone local.CallNone(5) local.CallNone(6) by auto
next
  case CallStatic thus ?case
    by (metis (no_types, lifting) eval_evals.CallStatic fv.simps(11) le_sup_iff)
next
  case CallParamsThrow thus ?case
    by simp (blast intro: eval_evals.CallParamsThrow)
next
  case (Call e h0 l0 sh0 a h1 l1 sh1 ps vs h2 l2 sh2 C fs M Ts T pns body
      D l2' e' h3 l3 sh3)
  have IHe: "⋀W. fv e ⊆ W ⟹ P ⊢ ⟨e,(h0,l0|`W,sh0)⟩ ⇒ ⟨addr a,(h1,l1|`W,sh1)⟩"
   and IHps: "⋀W. fvs ps ⊆ W ⟹ P ⊢ ⟨ps,(h1,l1|`W,sh1)⟩ [⇒] ⟨map Val vs,(h2,l2|`W,sh2)⟩"
   and IHbd: "⋀W. fv body ⊆ W ⟹ P ⊢ ⟨body,(h2,l2'|`W,sh2)⟩ ⇒ ⟨e',(h3,l3|`W,sh3)⟩"
   and h2a: "h2 a = Some (C, fs)"
   and "method": "P ⊢ C sees M,NonStatic: Ts→T = (pns, body) in D"
   and same_len: "size vs = size pns"
   and l2': "l2' = [this ↦ Addr a, pns [↦] vs]" 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 "method" wf by(fastforce dest!:sees_wf_mdecl simp:wf_mdecl_def)+
  show ?case
    using IHbd[OF fvbd] l2' same_len wfmethod h2a
      eval_evals.Call[OF IHe[OF fve] IHps[OF fvps] _ "method" same_len l2']
    by (simp add:subset_insertI)
next
  case (SCallNone ps h l sh vs h' l' sh' C M)
  have "P ⊢ ⟨ps,(h, l |` W, sh)⟩ [⇒] ⟨map Val vs,(h', l' |` W, sh')⟩"
    using SCallNone.hyps(2) SCallNone.prems by auto
  then show ?case using SCallNone.hyps(3) eval_evals.SCallNone by auto
next
  case SCallNonStatic thus ?case by (metis eval_evals.SCallNonStatic fv.simps(12))
next
  case SCallParamsThrow thus ?case
    by simp (blast intro: eval_evals.SCallParamsThrow)
next
  case SCallInitThrow thus ?case by simp (blast intro: eval_evals.SCallInitThrow)
next
  case SCallInit thus ?case by simp (blast intro: eval_evals.SCallInit)
next
  case (SCall ps h0 l0 sh0 vs h2 l2 sh2 C M Ts T pns body D sfs l2' e' h3 l3 sh3)
  have IHps: "⋀W. fvs ps ⊆ W ⟹ P ⊢ ⟨ps,(h0,l0|`W,sh0)⟩ [⇒] ⟨map Val vs,(h2,l2|`W,sh2)⟩"
   and IHbd: "⋀W. fv body ⊆ W ⟹ P ⊢ ⟨body,(h2,l2'|`W,sh2)⟩ ⇒ ⟨e',(h3,l3|`W,sh3)⟩"
   and sh2D: "sh2 D = Some (sfs, Done) ∨ M = clinit ∧ sh2 D = ⌊(sfs, Processing)⌋"
   and "method": "P ⊢ C sees M,Static: Ts→T = (pns, body) in D"
   and same_len: "size vs = size pns"
   and l2': "l2' = [pns [↦] vs]" by fact+
  have "fv (C∙sM(ps)) ⊆ W" by fact
  hence fvps: "fvs(ps) ⊆ W" by auto
  have wfmethod: "size Ts = size pns" and fvbd: "fv body ⊆ set pns"
    using "method" wf by(fastforce dest!:sees_wf_mdecl simp:wf_mdecl_def)+
  show ?case
    using IHbd[OF fvbd] l2' same_len wfmethod sh2D
      eval_evals.SCall[OF IHps[OF fvps] "method" _ same_len l2']
    by (simp add:subset_insertI)
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 Try thus ?case by simp (blast intro: eval_evals.Try)
next
  case (TryCatch e1 h0 l0 sh0 a h1 l1 sh1 D fs C e2 V e2' h2 l2 sh2)
  have IH1: "⋀W. fv e1 ⊆ W ⟹ P ⊢ ⟨e1,(h0,l0|`W,sh0)⟩ ⇒ ⟨Throw a,(h1,l1|`W,sh1)⟩"
   and IH2: "⋀W. fv e2 ⊆ W ⟹ P ⊢ ⟨e2,(h1,l1(V↦Addr a)|`W,sh1)⟩ ⇒ ⟨e2',(h2,l2|`W,sh2)⟩"
   and lookup: "h1 a = Some(D, fs)" and subtype: "P ⊢ D ≼* C" by fact+
  have "fv (try e1 catch(C V) e2) ⊆ W" by fact
  hence fv1: "fv e1 ⊆ W" and fv2: "fv e2 ⊆ insert V W" by auto
  have IH2': "P ⊢ ⟨e2,(h1,(l1|`W)(V ↦ Addr a),sh1)⟩ ⇒ ⟨e2',(h2,l2|`insert V W,sh2)⟩"
    using IH2[OF fv2] fun_upd_restrict[of l1 W] (*FIXME just l|W instead of l|(W-V) in simp rule??*) by simp
  with eval_evals.TryCatch[OF IH1[OF fv1] _ subtype IH2'] lookup
  show ?case by fastforce
next
  case TryThrow thus ?case by simp (blast intro: eval_evals.TryThrow)
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)
next
  case InitFinal thus ?case by (simp add: eval_evals.InitFinal)
next
  case InitNone thus ?case by(blast intro: eval_evals.InitNone)
next
  case InitDone thus ?case
    by (simp add: InitDone.hyps(2) InitDone.prems eval_evals.InitDone)
next
  case InitProcessing thus ?case by (simp add: eval_evals.InitProcessing)
next
  case InitError thus ?case using eval_evals.InitError by auto
next
  case InitObject thus ?case by(simp add: eval_evals.InitObject)
next
  case InitNonObject thus ?case by(simp add: eval_evals.InitNonObject)
next
  case InitRInit thus ?case by(simp add: eval_evals.InitRInit)
next
  case (RInit e h l sh v h' l' sh' C sfs i sh'' C' Cs e' e1 h1 l1 sh1)
  have f1: "fv e ⊆ W ∧ fv (INIT C' (Cs,True) ← e') ⊆ W"
    using RInit.prems by auto
  then have f2: "P ⊢ ⟨e,(h, l |` W, sh)⟩ ⇒ ⟨Val v,(h', l' |` W, sh')⟩"
    using RInit.hyps(2) by blast
  have "P ⊢ ⟨INIT C' (Cs,True) ← e', (h', l' |` W, sh'')⟩ ⇒ ⟨e1,(h1, l1 |` W, sh1)⟩"
    using f1 by (meson RInit.hyps(7))
  then show ?case
    using f2 RInit.hyps(3) RInit.hyps(4) RInit.hyps(5) eval_evals.RInit by blast
next
  case (RInitInitFail e h l sh a h' l' sh' C sfs i sh'' D Cs e' e1 h1 l1 sh1)
  have f1: "fv e ⊆ W" "fv e' ⊆ W"
    using RInitInitFail.prems by auto
  then have f2: "P ⊢ ⟨e,(h, l |` W, sh)⟩ ⇒ ⟨throw a,(h', l' |` W, sh')⟩"
    using RInitInitFail.hyps(2) by blast
  then have f2': "fv (throw a) ⊆ W"
    using eval_final[OF f2] by auto
  then have f1': "fv (RI (D,throw a);Cs ← e') ⊆ W"
    using f1 by auto
  have "P ⊢ ⟨RI (D,throw a);Cs ← e', (h', l' |` W, sh'')⟩ ⇒ ⟨e1,(h1, l1 |` W, sh1)⟩"
    using f1' by (meson RInitInitFail.hyps(6))
  then show ?case
    using f2 by (simp add: RInitInitFail.hyps(3,4) eval_evals.RInitInitFail)
next
  case (RInitFailFinal e h l sh a h' l' sh' sh'' C)
  have f1: "fv e ⊆ W"
    using RInitFailFinal.prems by auto
  then have f2: "P ⊢ ⟨e,(h, l |` W, sh)⟩ ⇒ ⟨throw a,(h', l' |` W, sh')⟩"
    using RInitFailFinal.hyps(2) by blast
  then have f2': "fv (throw a) ⊆ W"
    using eval_final[OF f2] by auto
  then show ?case using f2 RInitFailFinal.hyps(3,4) eval_evals.RInitFailFinal by blast
qed
(*>*)


lemma eval_notfree_unchanged:
  "P ⊢ ⟨e,(h,l,sh)⟩ ⇒ ⟨e',(h',l',sh')⟩ ⟹ (⋀V. V ∉ fv e ⟹ l' V = l V)"
and "P ⊢ ⟨es,(h,l,sh)⟩ [⇒] ⟨es',(h',l',sh')⟩ ⟹ (⋀V. V ∉ fvs es ⟹ l' V = l V)"
(*<*)
proof(induct rule:eval_evals_inducts)
  case LAss thus ?case by(simp add:fun_upd_apply)
next
  case Block thus ?case
    by (simp only:fun_upd_apply split:if_splits) fastforce
next
  case TryCatch thus ?case
    by (simp only:fun_upd_apply split:if_splits) fastforce
next
  case (RInitInitFail e h l sh a h' l' sh' C sfs i sh'' D Cs e1 h1 l1 sh1)
  have "fv (throw a) = {}"
    using RInitInitFail.hyps(1) eval_final final_fv by blast 
  then have "fv e ∪ fv (RI (D,throw a) ; Cs ← unit) ⊆ fv (RI (C,e) ; D#Cs ← unit)" 
    by auto
  then show ?case using RInitInitFail.hyps(2,6) RInitInitFail.prems by fastforce
qed simp_all
(*>*)


lemma eval_closed_lcl_unchanged:
  "⟦ P ⊢ ⟨e,(h,l,sh)⟩ ⇒ ⟨e',(h',l',sh')⟩; fv e = {} ⟧ ⟹ l' = l"
(*<*)by(fastforce dest:eval_notfree_unchanged simp add:fun_eq_iff [where 'b="val option"])(*>*)


lemma list_eval_Throw: 
assumes eval_e: "P ⊢ ⟨throw x,s⟩ ⇒ ⟨e',s'⟩"
shows "P ⊢ ⟨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 ⊢ ⟨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 # 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 ⊢ ⟨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,s⟩ ⇒ ⟨Val v,s⟩"
          by (iprover intro: eval_evals.Val)
        moreover from es 
        have "P ⊢ ⟨es,s⟩ [⇒] ⟨map Val vs' @ e' # es',s'⟩"
          by (rule Cons.hyps)
        ultimately show 
          "P ⊢ ⟨e#es,s⟩ [⇒] ⟨map Val vs @ e' # es',s'⟩"
          using vs by (auto intro: eval_evals.Cons)
      qed
    qed
  }
  thus ?thesis
    by simp
qed
(*>*)

― ‹ separate evaluation of first subexp of a sequence ›
lemma seq_ext:
assumes IH: "⋀e' s'. P ⊢ ⟨e'',s''⟩ ⇒ ⟨e',s'⟩ ⟹ P ⊢ ⟨e,s⟩ ⇒ ⟨e',s'⟩"
 and seq: "P ⊢ ⟨e'' ;; e0,s''⟩ ⇒ ⟨e',s'⟩"
shows "P ⊢ ⟨e ;; e0,s⟩ ⇒ ⟨e',s'⟩"
proof(rule eval_cases(14)[OF seq]) ― ‹ Seq ›
  fix v' s1 assume e'': "P ⊢ ⟨e'',s''⟩ ⇒ ⟨Val v',s1⟩" and estep: "P ⊢ ⟨e0,s1⟩ ⇒ ⟨e',s'⟩"
  have "P ⊢ ⟨e,s⟩ ⇒ ⟨Val v',s1⟩" using e'' IH by simp
  then show ?thesis using estep Seq by simp
next
  fix et assume e'': "P ⊢ ⟨e'',s''⟩ ⇒ ⟨throw et,s'⟩" and e': "e' = throw et"
  have "P ⊢ ⟨e,s⟩ ⇒ ⟨throw et,s'⟩" using e'' IH by simp
  then show ?thesis using eval_evals.SeqThrow e' by simp
qed

― ‹ separate evaluation of @{text RI} subexp, val case ›
lemma rinit_Val_ext:
assumes ri: "P ⊢ ⟨RI (C,e'') ; Cs ← e0,s''⟩ ⇒ ⟨Val v',s1⟩"
 and IH: "⋀e' s'. P ⊢ ⟨e'',s''⟩ ⇒ ⟨e',s'⟩ ⟹ P ⊢ ⟨e,s⟩ ⇒ ⟨e',s'⟩"
shows "P ⊢ ⟨RI (C,e) ; Cs ← e0,s⟩ ⇒ ⟨Val v',s1⟩"
proof(rule eval_cases(20)[OF ri]) ― ‹ RI ›
  fix v'' h' l' sh' sfs i
  assume e''step: "P ⊢ ⟨e'',s''⟩ ⇒ ⟨Val v'',(h', l', sh')⟩"
     and shC: "sh' C = ⌊(sfs, i)⌋"
     and init: "P ⊢ ⟨INIT (if Cs = [] then C else last Cs) (Cs,True) ← e0,(h', l', sh'(C ↦ (sfs, Done)))⟩ ⇒
        ⟨Val v',s1⟩"
  have "P ⊢ ⟨e,s⟩ ⇒ ⟨Val v'',(h', l', sh')⟩" using IH[OF e''step] by simp
  then show ?thesis using RInit init shC by auto
next
  fix a h' l' sh' sfs i D Cs'
  assume e''step: "P ⊢ ⟨e'',s''⟩ ⇒ ⟨throw a,(h', l', sh')⟩"
     and riD: "P ⊢ ⟨RI (D,throw a) ; Cs' ← e0,(h', l', sh'(C ↦ (sfs, Error)))⟩ ⇒ ⟨Val v',s1⟩"
  have "P ⊢ ⟨e,s⟩ ⇒ ⟨throw a,(h', l', sh')⟩" using IH[OF e''step] by simp
  then show ?thesis using riD rinit_throwE by blast
qed(simp)

― ‹ separate evaluation of @{text RI} subexp, throw case ›
lemma rinit_throw_ext:
assumes ri: "P ⊢ ⟨RI (C,e'') ; Cs ← e0,s''⟩ ⇒ ⟨throw et,s'⟩"
 and IH: "⋀e' s'. P ⊢ ⟨e'',s''⟩ ⇒ ⟨e',s'⟩ ⟹ P ⊢ ⟨e,s⟩ ⇒ ⟨e',s'⟩"
shows "P ⊢ ⟨RI (C,e) ; Cs ← e0,s⟩ ⇒ ⟨throw et,s'⟩"
proof(rule eval_cases(20)[OF ri]) ― ‹ RI ›
  fix v h' l' sh' sfs i
  assume e''step: "P ⊢ ⟨e'',s''⟩ ⇒ ⟨Val v,(h', l', sh')⟩"
     and shC: "sh' C = ⌊(sfs, i)⌋"
     and init: "P ⊢ ⟨INIT (if Cs = [] then C else last Cs) (Cs,True) ← e0,(h', l', sh'(C ↦ (sfs, Done)))⟩ ⇒
        ⟨throw et,s'⟩"
  have "P ⊢ ⟨e,s⟩ ⇒ ⟨Val v,(h', l', sh')⟩" using IH[OF e''step] by simp
  then show ?thesis using RInit init shC by auto
next
  fix a h' l' sh' sfs i D Cs'
  assume e''step: "P ⊢ ⟨e'',s''⟩ ⇒ ⟨throw a,(h', l', sh')⟩"
     and shC: "sh' C = ⌊(sfs, i)⌋"
     and riD: "P ⊢ ⟨RI (D,throw a) ; Cs' ← e0,(h', l', sh'(C ↦ (sfs, Error)))⟩ ⇒ ⟨throw et,s'⟩"
     and cons: "Cs = D # Cs'"
  have estep': "P ⊢ ⟨e,s⟩ ⇒ ⟨throw a,(h', l', sh')⟩" using IH[OF e''step] by simp
  then show ?thesis using RInitInitFail cons riD shC by simp
next
  fix a h' l' sh' sfs i
  assume "throw et = throw a"
     and "s' = (h', l', sh'(C ↦ (sfs, Error)))"
     and "P ⊢ ⟨e'',s''⟩ ⇒ ⟨throw a,(h', l', sh')⟩"
     and "sh' C = ⌊(sfs, i)⌋"
     and "Cs = []"
  then show ?thesis using RInitFailFinal IH by auto
qed

― ‹ separate evaluation of @{text RI} subexp ›
lemma rinit_ext:
assumes IH: "⋀e' s'. P ⊢ ⟨e'',s''⟩ ⇒ ⟨e',s'⟩ ⟹ P ⊢ ⟨e,s⟩ ⇒ ⟨e',s'⟩"
shows "⋀e' s'. P ⊢ ⟨RI (C,e'') ; Cs ← e0,s''⟩ ⇒ ⟨e',s'⟩
 ⟹ P ⊢ ⟨RI (C,e) ; Cs ← e0,s⟩ ⇒ ⟨e',s'⟩"
proof -
  fix e' s' assume ri'': "P ⊢ ⟨RI (C,e'') ; Cs ← e0,s''⟩ ⇒ ⟨e',s'⟩"
  then have "final e'" using eval_final by simp
  then show "P ⊢ ⟨RI (C,e) ; Cs ← e0,s⟩ ⇒ ⟨e',s'⟩"
  proof(rule finalE)
    fix v assume "e' = Val v" then show ?thesis using rinit_Val_ext[OF _ IH] ri'' by simp
  next
    fix a assume "e' = throw a" then show ?thesis using rinit_throw_ext[OF _ IH] ri'' by simp
  qed
qed

― ‹ @{text INIT} and @{text RI} return either @{text Val} with @{text Done} or
 @{text Processing} flag or @{text Throw} with @{text Error} flag ›
lemma
shows eval_init_return: "P ⊢ ⟨e,s⟩ ⇒ ⟨e',s'⟩
  ⟹ iconf (shp s) e
  ⟹ (∃Cs b. e = INIT C' (Cs,b) ← unit) ∨ (∃C e0 Cs ei. e = RI(C,e0);Cs@[C'] ← unit)
     ∨ (∃e0. e = RI(C',e0);Nil ← unit)
  ⟹ (val_of e' = Some v ⟶ (∃sfs i. shp s' C' = ⌊(sfs,i)⌋ ∧ (i = Done ∨ i = Processing)))
   ∧ (throw_of e' = Some a ⟶ (∃sfs i. shp s' C' = ⌊(sfs,Error)⌋))"
and "P ⊢ ⟨es,s⟩ [⇒] ⟨es',s'⟩ ⟹ True"
proof(induct rule: eval_evals.inducts)
  case (InitFinal e s e' s' C b) then show ?case
    by(fastforce simp: initPD_def dest: eval_final_same)
next
  case (InitDone sh C sfs C' Cs e h l e' s')
  then have "final e'" using eval_final by simp
  then show ?case
  proof(rule finalE)
    fix v assume e': "e' = Val v" then show ?thesis using InitDone initPD_def
    proof(cases Cs) qed(auto)
  next
    fix a assume e': "e' = throw a" then show ?thesis using InitDone initPD_def
    proof(cases Cs) qed(auto)
  qed
next
  case (InitProcessing sh C sfs C' Cs e h l e' s')
  then have "final e'" using eval_final by simp
  then show ?case
  proof(rule finalE)
    fix v assume e': "e' = Val v" then show ?thesis using InitProcessing initPD_def
    proof(cases Cs) qed(auto)
  next
    fix a assume e': "e' = throw a" then show ?thesis using InitProcessing initPD_def
    proof(cases Cs) qed(auto)
  qed
next
  case (InitError sh C sfs Cs e h l e' s' C') show ?case
  proof(cases Cs)
    case Nil then show ?thesis using InitError by simp
  next
    case (Cons C2 list)
    then have "final e'" using InitError eval_final by simp
    then show ?thesis
    proof(rule finalE)
      fix v assume e': "e' = Val v" then show ?thesis
      using InitError
      proof -
        obtain ccss :: "char list list" and bb :: bool where
          "INIT C' (C # Cs,False) ← e = INIT C' (ccss,bb) ← unit"
          using InitError.prems(2) by blast
        then show ?thesis using InitError.hyps(2) e' by(auto dest!: rinit_throwE)
      qed
    next
      fix a assume e': "e' = throw a"
      then show ?thesis using Cons InitError cons_to_append[of list] by clarsimp
    qed
  qed
next
  case (InitRInit C Cs h l sh e' s' C') show ?case
  proof(cases Cs)
    case Nil then show ?thesis using InitRInit by simp
  next
    case (Cons C' list) then show ?thesis
      using InitRInit Cons cons_to_append[of list] by clarsimp
  qed
next
  case (RInit e s v h' l' sh' C sfs i sh'' C' Cs e' e1 s1)
  then have final: "final e1" using eval_final by simp
  then show ?case
  proof(cases Cs)
    case Nil show ?thesis using final
    proof(rule finalE)
      fix v assume e': "e1 = Val v" show ?thesis
      using RInit Nil by(auto simp: fun_upd_same initPD_def)
    next
      fix a assume e': "e1 = throw a" show ?thesis
      using RInit Nil by(auto simp: fun_upd_same initPD_def)
    qed
  next
    case (Cons a list) show ?thesis
    proof(rule finalE[OF final])
      fix v assume e': "e1 = Val v" then show ?thesis
      using RInit Cons by clarsimp (metis last.simps last_appendR list.distinct(1))
    next
      fix a assume e': "e1 = throw a" then show ?thesis
      using RInit Cons by clarsimp (metis last.simps last_appendR list.distinct(1))
    qed
  qed
next
  case (RInitInitFail e s a h' l' sh' C sfs i sh'' D Cs e' e1 s1)
  then have final: "final e1" using eval_final by simp
  then show ?case
  proof(rule finalE)
    fix v assume e': "e1 = Val v" then show ?thesis
    using RInitInitFail by clarsimp (meson exp.distinct(101) rinit_throwE)
  next
    fix a' assume e': "e1 = Throw a'"
    then have "iconf (sh'(C ↦ (sfs, Error))) a"
      using RInitInitFail.hyps(1) eval_final by fastforce
    then show ?thesis using RInitInitFail e'
      by clarsimp (meson Cons_eq_append_conv list.inject)
  qed
qed(auto simp: fun_upd_same)

lemma init_Val_PD: "P ⊢ ⟨INIT C' (Cs,b) ← unit,s⟩ ⇒ ⟨Val v,s'⟩
  ⟹ iconf (shp s) (INIT C' (Cs,b) ← unit)
  ⟹ ∃sfs i. shp s' C' = ⌊(sfs,i)⌋ ∧ (i = Done ∨ i = Processing)"
 by(drule_tac v = v in eval_init_return, simp+)

lemma init_throw_PD: "P ⊢ ⟨INIT C' (Cs,b) ← unit,s⟩ ⇒ ⟨throw a,s'⟩
  ⟹ iconf (shp s) (INIT C' (Cs,b) ← unit)
  ⟹ ∃sfs i. shp s' C' = ⌊(sfs,Error)⌋"
 by(drule_tac a = a in eval_init_return, simp+)

lemma rinit_Val_PD: "P ⊢ ⟨RI(C,e0);Cs ← unit,s⟩ ⇒ ⟨Val v,s'⟩
  ⟹ iconf (shp s) (RI(C,e0);Cs ← unit) ⟹ last(C#Cs) = C'
  ⟹ ∃sfs i. shp s' C' = ⌊(sfs,i)⌋ ∧ (i = Done ∨ i = Processing)"
by(auto dest!: eval_init_return [where C'=C']
               append_butlast_last_id[THEN sym])

lemma rinit_throw_PD: "P ⊢ ⟨RI(C,e0);Cs ← unit,s⟩ ⇒ ⟨throw a,s'⟩
  ⟹ iconf (shp s) (RI(C,e0);Cs ← unit) ⟹ last(C#Cs) = C'
  ⟹ ∃sfs i. shp s' C' = ⌊(sfs,Error)⌋"
by(auto dest!: eval_init_return [where C'=C']
               append_butlast_last_id[THEN sym])

― ‹ combining the above to get evaluation of @{text INIT} in a sequence ›

(* 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]
(*>*)

lemma eval_init_seq': "P ⊢ ⟨e,s⟩ ⇒ ⟨e',s'⟩
  ⟹ (∃C Cs b ei. e = INIT C (Cs,b) ← ei) ∨ (∃C e0 Cs ei. e = RI(C,e0);Cs ← ei)
  ⟹ (∃C Cs b ei. e = INIT C (Cs,b) ← ei ∧ P ⊢ ⟨(INIT C (Cs,b) ← unit);; ei,s⟩ ⇒ ⟨e',s'⟩)
     ∨ (∃C e0 Cs ei. e = RI(C,e0);Cs ← ei ∧ P ⊢ ⟨(RI(C,e0);Cs ← unit);; ei,s⟩ ⇒ ⟨e',s'⟩)"
and "P ⊢ ⟨es,s⟩ [⇒] ⟨es',s'⟩ ⟹ True"
proof(induct rule: eval_evals.inducts)
  case InitFinal then show ?case by(auto simp: Seq[OF eval_evals.InitFinal[OF Val[where v=Unit]]])
next
  case (InitNone sh) then show ?case
   using seq_ext[OF eval_evals.InitNone[where sh=sh and e=unit, OF InitNone.hyps(1)]] by fastforce
next
  case (InitDone sh) then show ?case
   using seq_ext[OF eval_evals.InitDone[where sh=sh and e=unit, OF InitDone.hyps(1)]] by fastforce
next
  case (InitProcessing sh) then show ?case
   using seq_ext[OF eval_evals.InitProcessing[where sh=sh and e=unit, OF InitProcessing.hyps(1)]]
     by fastforce
next
  case (InitError sh) then show ?case
   using seq_ext[OF eval_evals.InitError[where sh=sh and e=unit, OF InitError.hyps(1)]] by fastforce
next
  case (InitObject sh) then show ?case
   using seq_ext[OF eval_evals.InitObject[where sh=sh and e=unit, OF InitObject.hyps(1)]]
     by fastforce
next
  case (InitNonObject sh) then show ?case
   using seq_ext[OF eval_evals.InitNonObject[where sh=sh and e=unit, OF InitNonObject.hyps(1)]]
     by fastforce
next
  case (InitRInit C Cs e h l sh e' s' C') then show ?case
   using seq_ext[OF eval_evals.InitRInit[where e=unit]] by fastforce
next
  case RInit then show ?case
   using seq_ext[OF eval_evals.RInit[where e=unit, OF RInit.hyps(1)]] by fastforce
next
  case RInitInitFail then show ?case
   using seq_ext[OF eval_evals.RInitInitFail[where e=unit, OF RInitInitFail.hyps(1)]] by fastforce
next
  case RInitFailFinal
  then show ?case using eval_evals.RInitFailFinal eval_evals.SeqThrow by auto
qed(auto)

lemma eval_init_seq: "P ⊢ ⟨INIT C (Cs,b) ← e,(h, l, sh)⟩ ⇒ ⟨e',s'⟩
 ⟹ P ⊢ ⟨(INIT C (Cs,b) ← unit);; e,(h, l, sh)⟩ ⇒ ⟨e',s'⟩"
 by(auto dest: eval_init_seq')


text ‹ The key lemma: ›
lemma
assumes wf: "wwf_J_prog P"
shows extend_1_eval: "P ⊢ ⟨e,s,b⟩ → ⟨e'',s'',b''⟩ ⟹ P,shp s ⊢b (e,b) √
   ⟹ (⋀s' e'.  P ⊢ ⟨e'',s''⟩ ⇒ ⟨e',s'⟩ ⟹ P ⊢ ⟨e,s⟩ ⇒ ⟨e',s'⟩)"
and extend_1_evals: "P ⊢ ⟨es,s,b⟩ [→] ⟨es'',s'',b''⟩ ⟹ P,shp s ⊢b (es,b) √
   ⟹ (⋀s' es'. P ⊢ ⟨es'',s''⟩ [⇒] ⟨es',s'⟩ ⟹ P ⊢ ⟨es,s⟩ [⇒] ⟨es',s'⟩)"
proof (induct rule: red_reds.inducts)
  case (RedNew h a C FDTs h' l sh)
  then have e':"e' = addr a" and s':"s' = (h(a ↦ blank P C), l, sh)"
    using eval_cases(3) by fastforce+
  obtain sfs i where shC: "sh C = ⌊(sfs, i)⌋" and "i = Done ∨ i = Processing"
   using RedNew by (clarsimp simp: bconf_def initPD_def)
  then show ?case
  proof(cases i)
    case Done then show ?thesis using RedNew shC e' s' New by simp
  next
    case Processing
    then have shC': "∄sfs. sh C = Some(sfs,Done)" and shP: "sh C = Some(sfs,Processing)"
      using shC by simp+
    then have init: "P ⊢ ⟨INIT C ([C],False) ← unit,(h,l,sh)⟩ ⇒ ⟨unit,(h,l,sh)⟩"
      by(simp add: InitFinal InitProcessing Val)
    have "P ⊢ ⟨new C,(h, l, sh)⟩ ⇒ ⟨addr a,(h(a ↦ blank P C),l,sh)⟩"
      using RedNew shC' by(auto intro: NewInit[OF _ init])
    then show ?thesis using e' s' by simp
  qed(auto)
next
  case (RedNewFail h C l sh)
  then have e':"e' = THROW OutOfMemory" and s':"s' = (h, l, sh)"
    using eval_final_same final_def by fastforce+
  obtain sfs i where shC: "sh C = ⌊(sfs, i)⌋" and "i = Done ∨ i = Processing"
   using RedNewFail by (clarsimp simp: bconf_def initPD_def)
  then show ?case
  proof(cases i)
    case Done then show ?thesis using RedNewFail shC e' s' NewFail by simp
  next
    case Processing
    then have shC': "∄sfs. sh C = Some(sfs,Done)" and shP: "sh C = Some(sfs,Processing)"
      using shC by simp+
    then have init: "P ⊢ ⟨INIT C ([C],False) ← unit,(h,l,sh)⟩ ⇒ ⟨unit,(h,l,sh)⟩"
      by(simp add: InitFinal InitProcessing Val)
    have "P ⊢ ⟨new C,(h, l, sh)⟩ ⇒ ⟨THROW OutOfMemory,(h,l,sh)⟩"
      using RedNewFail shC' by(auto intro: NewInitOOM[OF _ init])
    then show ?thesis using e' s' by simp
  qed(auto)
next
  case (NewInitRed sh C h l)
  then have seq: "P ⊢ ⟨(INIT C ([C],False) ← unit);; new C,(h, l, sh)⟩ ⇒ ⟨e',s'⟩"
    using eval_init_seq by simp
  then show ?case
  proof(rule eval_cases(14)) ― ‹ Seq ›
    fix v s1 assume init: "P ⊢ ⟨INIT C ([C],False) ← unit,(h, l, sh)⟩ ⇒ ⟨Val v,s1⟩"
      and new: "P ⊢ ⟨new C,s1⟩ ⇒ ⟨e',s'⟩"
    obtain h1 l1 sh1 where s1: "s1 = (h1,l1,sh1)" by(cases s1)
    then obtain sfs i where shC: "sh1 C = ⌊(sfs, i)⌋" and iDP: "i = Done ∨ i = Processing"
      using init_Val_PD[OF init] by auto
    show ?thesis
    proof(rule eval_cases(1)[OF new]) ― ‹ New ›
      fix sha ha a FDTs la
      assume s1a: "s1 = (ha, la, sha)" and e': "e' = addr a"
         and s': "s' = (ha(a ↦ blank P C), la, sha)"
         and addr: "new_Addr ha = ⌊a⌋" and fields: "P ⊢ C has_fields FDTs"
      then show ?thesis using NewInit[OF _ _ addr fields] NewInitRed.hyps init by simp
    next
      fix sha ha la
      assume "s1 = (ha, la, sha)" and "e' = THROW OutOfMemory"
         and "s' = (ha, la, sha)" and "new_Addr ha = None"
      then show ?thesis using NewInitOOM NewInitRed.hyps init by simp
    next
      fix sha ha la v' h' l' sh' a FDTs
      assume s1a: "s1 = (ha, la, sha)" and e': "e' = addr a"
         and s': "s' = (h'(a ↦ blank P C), l', sh')"
         and shaC: "∀sfs. sha C ≠ ⌊(sfs, Done)⌋"
         and init': "P ⊢ ⟨INIT C ([C],False) ← unit,(ha, la, sha)⟩ ⇒ ⟨Val v',(h', l', sh')⟩"
         and addr: "new_Addr h' = ⌊a⌋" and fields: "P ⊢ C has_fields FDTs"
      then have i: "i = Processing" using iDP shC s1 by simp
      then have "(h', l', sh') = (ha, la, sha)" using init' init_ProcessingE s1 s1a shC by blast
      then show ?thesis using NewInit NewInitRed.hyps s1a addr fields init shaC e' s' by auto
    next
      fix sha ha la v' h' l' sh'
      assume s1a: "s1 = (ha, la, sha)" and e': "e' = THROW OutOfMemory"
         and s': "s' = (h', l', sh')" and "∀sfs. sha C ≠ ⌊(sfs, Done)⌋"
         and init': "P ⊢ ⟨INIT C ([C],False) ← unit,(ha, la, sha)⟩ ⇒ ⟨Val v',(h', l', sh')⟩"
         and addr: "new_Addr h' = None"
      then have i: "i = Processing" using iDP shC s1 by simp
      then have "(h', l', sh') = (ha, la, sha)" using init' init_ProcessingE s1 s1a shC by blast
      then show ?thesis
        using NewInitOOM NewInitRed.hyps e' addr s' s1a init by auto
    next
      fix sha ha la a
      assume s1a: "s1 = (ha, la, sha)"
         and "∀sfs. sha C ≠ ⌊(sfs, Done)⌋"
         and init': "P ⊢ ⟨INIT C ([C],False) ← unit,(ha, la, sha)⟩ ⇒ ⟨throw a,s'⟩"
      then have i: "i = Processing" using iDP shC s1 by simp
      then show ?thesis using init' init_ProcessingE s1 s1a shC by blast
    qed
  next
    fix e assume e': "e' = throw e"
      and init: "P ⊢ ⟨INIT C ([C],False) ← unit,(h, l, sh)⟩ ⇒ ⟨throw e,s'⟩"
    obtain h' l' sh' where s': "s' = (h',l',sh')" by(cases s')
    then obtain sfs i where shC: "sh' C = ⌊(sfs, i)⌋" and iDP: "i = Error"
      using init_throw_PD[OF init] by auto
    then show ?thesis by (simp add: NewInitRed.hyps NewInitThrow e' init)
  qed
next
  case CastRed then show ?case
    by(fastforce elim!: eval_cases intro: eval_evals.intros intro!: CastFail)
next
  case RedCastNull
  then show ?case
    by simp (iprover elim: eval_cases intro: eval_evals.intros)
next
  case RedCast
  then show ?case
    by (auto elim: eval_cases intro: eval_evals.intros)
next
  case RedCastFail
  then show ?case
    by (auto elim!: eval_cases intro: eval_evals.intros)
next
  case BinOpRed1 then show ?case
    by(fastforce elim!: eval_cases intro: eval_evals.intros simp: val_no_step)
next
  case BinOpRed2
  thus ?case
    by (fastforce elim!: eval_cases intro: eval_evals.intros eval_finalId)
next
  case RedBinOp
  thus ?case
    by simp (iprover elim: eval_cases intro: eval_evals.intros)
next
  case RedVar
  thus ?case
    by (fastforce elim: eval_cases intro: eval_evals.intros)
next
  case LAssRed thus ?case
    by(fastforce elim: eval_cases intro: eval_evals.intros)
next
  case RedLAss
  thus ?case
    by (fastforce elim: eval_cases intro: eval_evals.intros)
next
  case FAccRed thus ?case
    by(fastforce elim: eval_cases intro: eval_evals.intros)
next
  case RedFAcc then show ?case
    by (fastforce elim: eval_cases intro: eval_evals.intros)
next
  case RedFAccNull then show ?case
    by (fastforce elim!: eval_cases intro: eval_evals.intros)
next
  case RedFAccNone thus ?case
    by(fastforce elim: eval_cases intro: eval_evals.intros)
next
  case RedFAccStatic thus ?case
    by(fastforce elim: eval_cases intro: eval_evals.intros)
next
  case (RedSFAcc C F t D sh sfs i v h l)
  then have e':"e' = Val v" and s':"s' = (h, l, sh)"
    using eval_cases(3) by fastforce+
  have "i = Done ∨ i = Processing" using RedSFAcc by (clarsimp simp: bconf_def initPD_def)
  then show ?case
  proof(cases i)
    case Done then show ?thesis using RedSFAcc e' s' SFAcc by simp
  next
    case Processing
    then have shC': "∄sfs. sh D = Some(sfs,Done)" and shP: "sh D = Some(sfs,Processing)"
      using RedSFAcc by simp+
    then have init: "P ⊢ ⟨INIT D ([D],False) ← unit,(h,l,sh)⟩ ⇒ ⟨unit,(h,l,sh)⟩"
      by(simp add: InitFinal InitProcessing Val)
    have "P ⊢ ⟨C∙sF{D},(h, l, sh)⟩ ⇒ ⟨Val v,(h,l,sh)⟩"
      by(rule SFAccInit[OF RedSFAcc.hyps(1) shC' init shP RedSFAcc.hyps(3)])
    then show ?thesis using e' s' by simp
  qed(auto)
next
  case (SFAccInitRed C F t D sh h l)
  then have seq: "P ⊢ ⟨(INIT D ([D],False) ← unit);; C∙sF{D},(h, l, sh)⟩ ⇒ ⟨e',s'⟩"
    using eval_init_seq by simp
  then show ?case
  proof(rule eval_cases(14)) ― ‹ Seq ›
    fix v s1 assume init: "P ⊢ ⟨INIT D ([D],False) ← unit,(h, l, sh)⟩ ⇒ ⟨Val v,s1⟩"
      and acc: "P ⊢ ⟨C∙sF{D},s1⟩ ⇒ ⟨e',s'⟩"
    obtain h1 l1 sh1 where s1: "s1 = (h1,l1,sh1)" by(cases s1)
    then obtain sfs i where shD: "sh1 D = ⌊(sfs, i)⌋" and iDP: "i = Done ∨ i = Processing"
      using init_Val_PD[OF init] by auto
    show ?thesis
    proof(rule eval_cases(8)[OF acc]) ― ‹ SFAcc ›
      fix t sha sfs v ha la
      assume "s1 = (ha, la, sha)" and "e' = Val v"
         and "s' = (ha, la, sha)" and "P ⊢ C has F,Static:t in D"
         and "sha D = ⌊(sfs, Done)⌋" and "sfs F = ⌊v⌋"
      then show ?thesis using SFAccInit SFAccInitRed.hyps(2) init by auto
    next
      fix t sha ha la v' h' l' sh' sfs i' v
      assume s1a: "s1 = (ha, la, sha)" and e': "e' = Val v"
         and s': "s' = (h', l', sh')" and field: "P ⊢ C has F,Static:t in D"
         and "∀sfs. sha D ≠ ⌊(sfs, Done)⌋"
         and init': "P ⊢ ⟨INIT D ([D],False) ← unit,(ha, la, sha)⟩ ⇒ ⟨Val v',(h', l', sh')⟩"
         and shD': "sh' D = ⌊(sfs, i')⌋" and sfsF: "sfs F = ⌊v⌋"
      then have i: "i = Processing" using iDP shD s1 by simp
      then have "(h', l', sh') = (ha, la, sha)" using init' init_ProcessingE s1 s1a shD by blast
      then show ?thesis using SFAccInit SFAccInitRed.hyps(2) e' s' field init s1a sfsF shD' by auto
    next
      fix t sha ha la a
      assume s1a: "s1 = (ha, la, sha)" and "e' = throw a"
         and "P ⊢ C has F,Static:t in D" and "∀sfs. sha D ≠ ⌊(sfs, Done)⌋"
         and init': "P ⊢ ⟨INIT D ([D],False) ← unit,(ha, la, sha)⟩ ⇒ ⟨throw a,s'⟩"
      then have i: "i = Processing" using iDP shD s1 by simp
      then show ?thesis using init' init_ProcessingE s1 s1a shD by blast
    next
      assume "∀b t. ¬ P ⊢ C has F,b:t in D"
      then show ?thesis using SFAccInitRed.hyps(1) by blast
    next
      fix t assume field: "P ⊢ C has F,NonStatic:t in D"
      then show ?thesis using has_field_fun[OF SFAccInitRed.hyps(1) field] by simp
    qed
  next
    fix e assume e': "e' = throw e"
     and init: "P ⊢ ⟨INIT D ([D],False) ← unit,(h, l, sh)⟩ ⇒ ⟨throw e,s'⟩"
    obtain h' l' sh' where s': "s' = (h',l',sh')" by(cases s')
    then obtain sfs i where shC: "sh' D = ⌊(sfs, i)⌋" and iDP: "i = Error"
      using init_throw_PD[OF init] by auto
    then show ?thesis
      using SFAccInitRed.hyps(1) SFAccInitRed.hyps(2) SFAccInitThrow e' init by auto
  qed
next
  case RedSFAccNone thus ?case
    by(fastforce elim: eval_cases intro: eval_evals.intros)
next
  case RedSFAccNonStatic thus ?case
    by(fastforce elim: eval_cases intro: eval_evals.intros)
next
  case (FAssRed1 e s b e1 s1 b1 F D e2)
  obtain h' l' sh' where "s'=(h',l',sh')" by(cases s')
  with FAssRed1 show ?case
    by(fastforce elim!: eval_cases(9)[where e1=e1] intro: eval_evals.intros simp: val_no_step
                 intro!: FAss FAssNull FAssNone FAssStatic FAssThrow2)
next
  case FAssRed2
  obtain h' l' sh' where "s'=(h',l',sh')" by(cases s')
  with FAssRed2 show ?case
    by(auto elim!: eval_cases intro: eval_evals.intros
            intro!: FAss FAssNull FAssNone FAssStatic FAssThrow2 Val)
next
  case RedFAss
  thus ?case
    by (fastforce elim!: eval_cases intro: eval_evals.intros)
next
  case RedFAssNull
  thus ?case
    by (fastforce elim!: eval_cases intro: eval_evals.intros)
next
  case RedFAssNone
  then show ?case
    by(auto elim!: eval_cases intro: eval_evals.intros eval_finalId)
next
  case RedFAssStatic
  then show ?case
    by(auto elim!: eval_cases intro: eval_evals.intros eval_finalId)
next
  case (SFAssRed e s b e'' s'' b'' C F D)
  obtain h l sh where [simp]: "s = (h,l,sh)" by(cases s)
  obtain h' l' sh' where [simp]: "s'=(h',l',sh')" by(cases s')
  have "val_of e = None" using val_no_step SFAssRed.hyps(1) by(meson option.exhaust)
  then have bconf: "P,sh ⊢b (e,b) √" using SFAssRed by simp
  show ?case using SFAssRed.prems(2) SFAssRed bconf
  proof cases
    case 2 with SFAssRed bconf show ?thesis by(auto intro!: SFAssInit)
  next
    case 3 with SFAssRed bconf show ?thesis by(auto intro!: SFAssInitThrow)
  qed(auto intro: eval_evals.intros intro!: SFAss SFAssInit SFAssNone SFAssNonStatic)
next
  case (RedSFAss C F t D sh sfs i sfs' v sh' h l)
  let ?sfs' = "sfs(F ↦ v)"
  have e':"e' = unit" and s':"s' = (h, l, sh(D ↦ (?sfs', i)))"
    using RedSFAss eval_cases(3) by fastforce+
  have "i = Done ∨ i = Processing" using RedSFAss by(clarsimp simp: bconf_def initPD_def)
  then show ?case
  proof(cases i)
    case Done then show ?thesis using RedSFAss e' s' SFAss Val by auto
  next
    case Processing
    then have shC': "∄sfs. sh D = Some(sfs,Done)" and shP: "sh D = Some(sfs,Processing)"
      using RedSFAss by simp+
    then have init: "P ⊢ ⟨INIT D ([D],False) ← unit,(h,l,sh)⟩ ⇒ ⟨unit,(h,l,sh)⟩"
      by(simp add: InitFinal InitProcessing Val)
    have "P ⊢ ⟨C∙sF{D} := Val v,(h, l, sh)⟩ ⇒ ⟨unit,(h,l,sh(D ↦ (?sfs', i)))⟩"
      using Processing by(auto intro: SFAssInit[OF Val RedSFAss.hyps(1) shC' init shP])
    then show ?thesis using e' s' by simp
  qed(auto)
next
  case (SFAssInitRed C F t D sh v h l)
  then have seq: "P ⊢ ⟨(INIT D ([D],False) ← unit);; C∙sF{D} := Val v,(h, l, sh)⟩ ⇒ ⟨e',s'⟩"
    using eval_init_seq by simp
  then show ?case
  proof(rule eval_cases(14)) ― ‹ Seq ›
    fix v' s1 assume init: "P ⊢ ⟨INIT D ([D],False) ← unit,(h, l, sh)⟩ ⇒ ⟨Val v',s1⟩"
      and acc: "P ⊢ ⟨C∙sF{D} := Val v,s1⟩ ⇒ ⟨e',s'⟩"
    obtain h1 l1 sh1 where s1: "s1 = (h1,l1,sh1)" by(cases s1)
    then obtain sfs i where shD: "sh1 D = ⌊(sfs, i)⌋" and iDP: "i = Done ∨ i = Processing"
      using init_Val_PD[OF init] by auto
    show ?thesis
    proof(rule eval_cases(10)[OF acc]) ― ‹ SFAss ›
      fix va h1 l1 sh1 t sfs
      assume e': "e' = unit" and s': "s' = (h1, l1, sh1(D ↦ (sfs(F ↦ va), Done)))"
         and val: "P ⊢ ⟨Val v,s1⟩ ⇒ ⟨Val va,(h1, l1, sh1)⟩"
         and field: "P ⊢ C has F,Static:t in D" and shD': "sh1 D = ⌊(sfs, Done)⌋"
      have "v = va" and "s1 = (h1, l1, sh1)" using eval_final_same[OF val] by auto
      then show ?thesis using SFAssInit field SFAssInitRed.hyps(2) shD' e' s' init val
        by (metis eval_final eval_finalId)
    next
      fix va h1 l1 sh1 t v' h' l' sh' sfs i'
      assume e': "e' = unit" and s': "s' = (h', l', sh'(D ↦ (sfs(F ↦ va), i')))"
         and val: "P ⊢ ⟨Val v,s1⟩ ⇒ ⟨Val va,(h1, l1, sh1)⟩"
         and field: "P ⊢ C has F,Static:t in D" and nDone: "∀sfs. sh1 D ≠ ⌊(sfs, Done)⌋"
         and init': "P ⊢ ⟨INIT D ([D],False) ← unit,(h1, l1, sh1)⟩ ⇒ ⟨Val v',(h', l', sh')⟩"
         and shD': "sh' D = ⌊(sfs, i')⌋"
      have v: "v = va" and s1a: "s1 = (h1, l1, sh1)" using eval_final_same[OF val] by auto
      then have i: "i = Processing" using iDP shD s1 nDone by simp
      then have "(h1, l1, sh1) = (h', l', sh')" using init' init_ProcessingE s1 s1a shD by blast
      then show ?thesis using SFAssInit SFAssInitRed.hyps(2) e' s' field init v s1a shD' val
        by (metis eval_final eval_finalId)
    next
      fix va h1 l1 sh1 t a
      assume "e' = throw a" and val: "P ⊢ ⟨Val v,s1⟩ ⇒ ⟨Val va,(h1, l1, sh1)⟩"
         and "P ⊢ C has F,Static:t in D" and nDone: "∀sfs. sh1 D ≠ ⌊(sfs, Done)⌋"
         and init': "P ⊢ ⟨INIT D ([D],False) ← unit,(h1, l1, sh1)⟩ ⇒ ⟨throw a,s'⟩"
      have v: "v = va" and s1a: "s1 = (h1, l1, sh1)" using eval_final_same[OF val] by auto
      then have i: "i = Processing" using iDP shD s1 nDone by simp
      then have "(h1, l1, sh1) = s'" using init' init_ProcessingE s1 s1a shD by blast
      then show ?thesis using init' init_ProcessingE s1 s1a shD i by blast
    next
      fix e'' assume val:"P ⊢ ⟨Val v,s1⟩ ⇒ ⟨throw e'',s'⟩"
      then show ?thesis using eval_final_same[OF val] by simp
    next
      assume "∀b t. ¬ P ⊢ C has F,b:t in D"
      then show ?thesis using SFAssInitRed.hyps(1) by blast
    next
      fix t assume field: "P ⊢ C has F,NonStatic:t in D"
      then show ?thesis using has_field_fun[OF SFAssInitRed.hyps(1) field] by simp
    qed
  next
    fix e assume e': "e' = throw e"
     and init: "P ⊢ ⟨INIT D ([D],False) ← unit,(h, l, sh)⟩ ⇒ ⟨throw e,s'⟩"
    obtain h' l' sh' where s': "s' = (h',l',sh')" by(cases s')
    then obtain sfs i where shC: "sh' D = ⌊(sfs, i)⌋" and iDP: "i = Error"
      using init_throw_PD[OF init] by auto
    then show ?thesis using SFAssInitRed.hyps(1) SFAssInitRed.hyps(2) SFAssInitThrow Val
      by (metis e' init)
  qed
next
  case (RedSFAssNone C F D v s b) then show ?case
    by(cases s) (auto elim!: eval_cases intro: eval_evals.intros eval_finalId)
next
  case (RedSFAssNonStatic C F t D v s b) then show ?case
    by(cases s) (auto elim!: eval_cases intro: eval_evals.intros eval_finalId)
next
  case CallObj
  note val_no_step[simp]
  from CallObj.prems(2) CallObj show ?case
  proof cases
    case 2 with CallObj show ?thesis by(fastforce intro!: CallParamsThrow)
  next
    case 3 with CallObj show ?thesis by(fastforce intro!: CallNull)
  next
    case 4 with CallObj show ?thesis by(fastforce intro!: CallNone)
  next
    case 5 with CallObj show ?thesis by(fastforce intro!: CallStatic)
  qed(fastforce intro!: CallObjThrow Call)+
next
  case (CallParams es s b es'' s'' b'' v M s')
  then obtain h' l' sh' where "s' = (h',l',sh')" by(cases s')
  with CallParams show ?case
   by(auto elim!: eval_cases intro!: CallNone eval_finalId CallStatic Val)
     (auto intro!: CallParamsThrow CallNull Call Val)
next
  case (RedCall h a C fs M Ts T pns body D vs l sh b)
  have "P ⊢ ⟨addr a,(h,l,sh)⟩ ⇒ ⟨addr a,(h,l,sh)⟩" by (rule eval_evals.intros)
  moreover
  have finals: "finals(map Val vs)" by simp
  with finals have "P ⊢ ⟨map Val vs,(h,l,sh)⟩ [⇒] ⟨map Val vs,(h,l,sh)⟩"
    by (iprover intro: eval_finalsId)
  moreover have "h a = Some (C, fs)" using RedCall by simp
  moreover have "method": "P ⊢ C sees M,NonStatic: Ts→T = (pns, body) in D" by fact
  moreover have same_len1: "length Ts = length pns"
   and this_distinct: "this ∉ set pns" and fv: "fv (body) ⊆ {this} ∪ set pns"
    using "method" wf by (fastforce dest!:sees_wf_mdecl simp:wf_mdecl_def)+
  have same_len: "length vs = length pns" by fact
  moreover
  obtain l2' where l2': "l2' = [this↦Addr a,pns[↦]vs]" by simp
  moreover
  obtain h3 l3 sh3 where s': "s' = (h3,l3,sh3)" by (cases s')
  have eval_blocks:
    "P ⊢ ⟨(blocks (this # pns, Class D # Ts, Addr a # vs, body)),(h,l,sh)⟩ ⇒ ⟨e',s'⟩" by fact
  hence id: "l3 = l" using fv s' same_len1 same_len
    by(fastforce elim: eval_closed_lcl_unchanged)
  from eval_blocks obtain l3' where "P ⊢ ⟨body,(h,l2',sh)⟩ ⇒ ⟨e',(h3,l3',sh3)⟩"
  proof -
    from same_len1 have "length(this#pns) = length(Class D#Ts)" by simp
    moreover from same_len1 same_len
    have same_len2: "length (this#pns) = length (Addr a#vs)" by simp
    moreover from eval_blocks
    have "P ⊢ ⟨blocks (this#pns,Class D#Ts,Addr a#vs,body),(h,l,sh)⟩
              ⇒⟨e',(h3,l3,sh3)⟩" using s' same_len1 same_len2 by simp
    ultimately obtain l''
      where "P ⊢ ⟨body,(h,l(this # pns[↦]Addr a # vs),sh)⟩⇒⟨e',(h3, l'',sh3)⟩"
      by (blast dest:blocksEval)
    from eval_restrict_lcl[OF wf this fv] this_distinct same_len1 same_len
    have "P ⊢ ⟨body,(h,[this # pns[↦]Addr a # vs],sh)⟩ ⇒
               ⟨e',(h3, l''|`(set(this#pns)),sh3)⟩" using wf method
      by(simp add:subset_insert_iff insert_Diff_if)
    thus ?thesis by(fastforce intro!:that simp add: l2')
  qed
  ultimately
  have "P ⊢ ⟨(addr a)∙M(map Val vs),(h,l,sh)⟩ ⇒ ⟨e',(h3,l,sh3)⟩" by (rule Call)
  with s' id show ?case by simp
next
  case RedCallNull
  thus ?case
    by (fastforce elim: eval_cases intro: eval_evals.intros eval_finalsId)
next
  case (RedCallNone h a C fs M vs l sh b)
  then have tes: "THROW NoSuchMethodError = e' ∧ (h,l,sh) = s'"
    using eval_final_same by simp
  have "P ⊢ ⟨addr a,(h,l,sh)⟩ ⇒ ⟨addr a,(h,l,sh)⟩" and "P ⊢ ⟨map Val vs,(h,l,sh)⟩ [⇒] ⟨map Val vs,(h,l,sh)⟩"
    using eval_finalId eval_finalsId by auto
  then show ?case using RedCallNone CallNone tes by auto
next
  case (RedCallStatic h a C fs M Ts T m D vs l sh b)
  then have tes: "THROW IncompatibleClassChangeError = e' ∧ (h,l,sh) = s'"
    using eval_final_same by simp
  have "P ⊢ ⟨addr a,(h,l,sh)⟩ ⇒ ⟨addr a,(h,l,sh)⟩" and "P ⊢ ⟨map Val vs,(h,l,sh)⟩ [⇒] ⟨map Val vs,(h,l,sh)⟩"
    using eval_finalId eval_finalsId by auto
  then show ?case using RedCallStatic CallStatic tes by fastforce
next
  case (SCallParams es s b es'' s'' b' C M s')
  obtain h' l' sh' where s'[simp]: "s' = (h',l',sh')" by(cases s')
  obtain h l sh where s[simp]: "s = (h,l,sh)" by(cases s)
  have es: "map_vals_of es = None" using vals_no_step SCallParams.hyps(1) by (meson not_Some_eq)
  have bconf: "P,sh ⊢b (es,b) √" using s SCallParams.prems(1) by (simp add: bconf_SCall[OF es])
  from SCallParams.prems(2) SCallParams bconf show ?case
  proof cases
    case 2 with SCallParams bconf show ?thesis by(auto intro!: SCallNone)
  next
    case 3 with SCallParams bconf show ?thesis by(auto intro!: SCallNonStatic)
  next
    case 4 with SCallParams bconf show ?thesis by(auto intro!: SCallInitThrow)
  next
    case 5 with SCallParams bconf show ?thesis by(auto intro!: SCallInit)
  qed(auto intro!: SCallParamsThrow SCall)
next
  case (RedSCall C M Ts T pns body D vs s)
  then obtain h l sh where s:"s = (h,l,sh)" by(cases s)
  then obtain sfs i where shC: "sh D = ⌊(sfs, i)⌋" and "i = Done ∨ i = Processing"
   using RedSCall by(auto simp: bconf_def initPD_def dest: sees_method_fun)
  have finals: "finals(map Val vs)" by simp
  with finals have mVs: "P ⊢ ⟨map Val vs,(h,l,sh)⟩ [⇒] ⟨map Val vs,(h,l,sh)⟩"
    by (iprover intro: eval_finalsId)
  obtain sfs i where shC: "sh D = ⌊(sfs, i)⌋"
   using RedSCall s by(auto simp: bconf_def initPD_def dest: sees_method_fun)
  then have iDP: "i = Done ∨ i = Processing" using RedSCall s
    by (auto simp: bconf_def initPD_def dest: sees_method_fun[OF RedSCall.hyps(1)])
  have "method": "P ⊢ C sees M,Static: Ts→T = (pns, body) in D" by fact
  have same_len1: "length Ts = length pns" and fv: "fv (body) ⊆ set pns"
    using "method" wf by (fastforce dest!:sees_wf_mdecl simp:wf_mdecl_def)+
  have same_len: "length vs = length pns" by fact
  obtain l2' where l2': "l2' = [pns[↦]vs]" by simp
  obtain h3 l3 sh3 where s': "s' = (h3,l3,sh3)" by (cases s')
  have eval_blocks:
    "P ⊢ ⟨(blocks (pns, Ts, vs, body)),(h,l,sh)⟩ ⇒ ⟨e',s'⟩" using RedSCall.prems(2) s by simp
  hence id: "l3 = l" using fv s' same_len1 same_len
    by(fastforce elim: eval_closed_lcl_unchanged)
  from eval_blocks obtain l3' where body: "P ⊢ ⟨body,(h,l2',sh)⟩ ⇒ ⟨e',(h3,l3',sh3)⟩"
  proof -
    from eval_blocks
    have "P ⊢ ⟨blocks (pns,Ts,vs,body),(h,l,sh)⟩
              ⇒⟨e',(h3,l3,sh3)⟩" using s' same_len same_len1 by simp
    then obtain l''
      where "P ⊢ ⟨body,(h,l(pns[↦]vs),sh)⟩ ⇒ ⟨e',(h3, l'',sh3)⟩"
      by (blast dest:blocksEval[OF same_len1[THEN sym] same_len[THEN sym]])
    from eval_restrict_lcl[OF wf this fv] same_len1 same_len
    have "P ⊢ ⟨body,(h,[pns[↦]vs],sh)⟩ ⇒ ⟨e',(h3, l''|`(set(pns)),sh3)⟩" using wf method
      by(simp add:subset_insert_iff insert_Diff_if)
    thus ?thesis by(fastforce intro!:that simp add: l2')
  qed
  show ?case using iDP
  proof(cases i)
    case Done
    then have shC': "sh D = ⌊(sfs, Done)⌋ ∨ M = clinit ∧ sh D = ⌊(sfs, Processing)⌋"
      using shC by simp
    have "P ⊢ ⟨C∙sM(map Val vs),(h,l,sh)⟩ ⇒ ⟨e',(h3,l,sh3)⟩"
     by (rule SCall[OF mVs method shC' same_len l2' body])
    with s s' id show ?thesis by simp
  next
    case Processing
    then have shC': "∄sfs. sh D = Some(sfs,Done)" and shP: "sh D = Some(sfs,Processing)"
      using shC by simp+
    then have init: "P ⊢ ⟨INIT D ([D],False) ← unit,(h,l,sh)⟩ ⇒ ⟨unit,(h,l,sh)⟩"
      by(simp add: InitFinal InitProcessing Val)
    have "P ⊢ ⟨C∙sM(map Val vs),(h,l,sh)⟩ ⇒ ⟨e',(h3,l,sh3)⟩"
    proof(cases "M = clinit")
      case False show ?thesis by(rule SCallInit[OF mVs method shC' False init same_len l2' body])
    next
      case True
      then have shC': "sh D = ⌊(sfs, Done)⌋ ∨ M = clinit ∧ sh D = ⌊(sfs, Processing)⌋"
        using shC Processing by simp
      have "P ⊢ ⟨C∙sM(map Val vs),(h,l,sh)⟩ ⇒ ⟨e',(h3,l,sh3)⟩"
       by (rule SCall[OF mVs method shC' same_len l2' body])
      with s s' id show ?thesis by simp
    qed
    with s s' id show ?thesis by simp
  qed(auto)
next
  case (SCallInitRed C M Ts T pns body D sh vs h l)
  then have seq: "P ⊢ ⟨(INIT D ([D],False) ← unit);; C∙sM(map Val vs),(h, l, sh)⟩ ⇒ ⟨e',s'⟩"
    using eval_init_seq by simp
  then show ?case
  proof(rule eval_cases(14)) ― ‹ Seq ›
    fix v' s1 assume init: "P ⊢ ⟨INIT D ([D],False) ← unit,(h, l, sh)⟩ ⇒ ⟨Val v',s1⟩"
      and call: "P ⊢ ⟨C∙sM(map Val vs),s1⟩ ⇒ ⟨e',s'⟩"
    obtain h1 l1 sh1 where s1: "s1 = (h1,l1,sh1)" by(cases s1)
    then obtain sfs i where shD: "sh1 D = ⌊(sfs, i)⌋" and iDP: "i = Done ∨ i = Processing"
      using init_Val_PD[OF init] by auto
    show ?thesis
    proof(rule eval_cases(12)[OF call]) ― ‹ SCall ›
      fix vsa ex es' assume "P ⊢ ⟨map Val vs,s1⟩ [⇒] ⟨map Val vsa @ throw ex # es',s'⟩"
      then show ?thesis using evals_finals_same by (meson finals_def map_Val_nthrow_neq)
    next
      assume "∀b Ts T a ba x. ¬ P ⊢ C sees M, b :  Ts→T = (a, ba) in x"
      then show ?thesis using SCallInitRed.hyps(1) by auto
    next
      fix Ts T m D assume "P ⊢ C sees M, NonStatic :  Ts→T = m in D"
      then show ?thesis using sees_method_fun[OF SCallInitRed.hyps(1)] by blast
    next
      fix vsa h1 l1 sh1 Ts T pns body D' a
      assume "e' = throw a" and vals: "P ⊢ ⟨map Val vs,s1⟩ [⇒] ⟨map Val vsa,(h1, l1, sh1)⟩"
         and method: "P ⊢ C sees M, Static :  Ts→T = (pns, body) in D'"
         and nDone: "∀sfs. sh1 D' ≠ ⌊(sfs, Done)⌋"
         and init': "P ⊢ ⟨INIT D' ([D'],False) ← unit,(h1, l1, sh1)⟩ ⇒ ⟨throw a,s'⟩"
      have vs: "vs = vsa" and s1a: "s1 = (h1, l1, sh1)"
        using evals_finals_same[OF _ vals] map_Val_eq by auto
      have D: "D = D'" using sees_method_fun[OF SCallInitRed.hyps(1) method] by simp
      then have i: "i = Processing" using iDP shD s1 s1a nDone by simp
      then show ?thesis using D init' init_ProcessingE s1 s1a shD by blast
    next
      fix vsa h1 l1 sh1 Ts T pns' body' D' v' h2 l2 sh2 h3 l3 sh3
      assume s': "s' = (h3, l2, sh3)"
         and vals: "P ⊢ ⟨map Val vs,s1⟩ [⇒] ⟨map Val vsa,(h1, l1, sh1)⟩"
         and method: "P ⊢ C sees M, Static :  Ts→T = (pns', body') in D'"
         and nDone: "∀sfs. sh1 D' ≠ ⌊(sfs, Done)⌋"
         and init': "P ⊢ ⟨INIT D' ([D'],False) ← unit,(h1, l1, sh1)⟩ ⇒ ⟨Val v',(h2, l2, sh2)⟩"
         and len: "length vsa = length pns'"
         and bstep: "P ⊢ ⟨body',(h2, [pns' [↦] vsa], sh2)⟩ ⇒ ⟨e',(h3, l3, sh3)⟩"
      have vs: "vs = vsa" and s1a: "s1 = (h1, l1, sh1)"
        using evals_finals_same[OF _ vals] map_Val_eq by auto
      have D: "D = D'" and pns: "pns = pns'" and body: "body = body'"
        using sees_method_fun[OF SCallInitRed.hyps(1) method] by auto
      then have i: "i = Processing" using iDP shD s1 s1a nDone by simp
      then have s2: "(h2, l2, sh2) = s1" using D init' init_ProcessingE s1 s1a shD by blast
      then show ?thesis
        using eval_finalId SCallInit[OF eval_finalsId[of "map Val vs" P "(h,l,sh)"]
          SCallInitRed.hyps(1)] init init' len bstep nDone D pns body s' s1 s1a shD vals vs
          SCallInitRed.hyps(2-3) s2 by auto
    next
      fix vsa h2 l2 sh2 Ts T pns' body' D' sfs h3 l3 sh3
      assume s': "s' = (h3, l2, sh3)" and vals: "P ⊢ ⟨map Val vs,s1⟩ [⇒] ⟨map Val vsa,(h2, l2, sh2)⟩"
         and method: "P ⊢ C sees M, Static :  Ts→T = (pns', body') in D'"
         and "sh2 D' = ⌊(sfs, Done)⌋ ∨ M = clinit ∧ sh2 D' = ⌊(sfs, Processing)⌋"
         and len: "length vsa = length pns'"
         and bstep: "P ⊢ ⟨body',(h2, [pns' [↦] vsa], sh2)⟩ ⇒ ⟨e',(h3, l3, sh3)⟩"
      have vs: "vs = vsa" and s1a: "s1 = (h2, l2, sh2)"
        using evals_finals_same[OF _ vals] map_Val_eq by auto
      have D: "D = D'" and pns: "pns = pns'" and body: "body = body'"
        using sees_method_fun[OF SCallInitRed.hyps(1) method] by auto
      then show ?thesis using SCallInit[OF eval_finalsId[of "map Val vs" P "(h,l,sh)"]
        SCallInitRed.hyps(1)] bstep SCallInitRed.hyps(2-3) len s' s1a vals vs init by auto
    qed
  next
    fix e assume e': "e' = throw e"
     and init: "P ⊢ ⟨INIT D ([D],False) ← unit,(h, l, sh)⟩ ⇒ ⟨throw e,s'⟩"
    obtain h' l' sh' where s': "s' = (h',l',sh')" by(cases s')
    then obtain sfs i where shC: "sh' D = ⌊(sfs, i)⌋" and iDP: "i = Error"
      using init_throw_PD[OF init] by auto
    then show ?thesis using SCallInitRed.hyps(2-3) init e'
      SCallInitThrow[OF eval_finalsId[of "map Val vs" _] SCallInitRed.hyps(1)]
     by auto
  qed
next
  case (RedSCallNone C M vs s b)
  then have tes: "THROW NoSuchMethodError = e' ∧ s = s'"
    using eval_final_same by simp
  have "P ⊢ ⟨map Val vs,s⟩ [⇒] ⟨map Val vs,s⟩" using eval_finalsId by simp
  then show ?case using RedSCallNone eval_evals.SCallNone tes by auto
next
  case (RedSCallNonStatic C M Ts T m D vs s b)
  then have tes: "THROW IncompatibleClassChangeError = e' ∧ s = s'"
    using eval_final_same by simp
  have "P ⊢ ⟨map Val vs,s⟩ [⇒] ⟨map Val vs,s⟩" using eval_finalsId by simp
  then show ?case using RedSCallNonStatic eval_evals.SCallNonStatic tes by auto
next
  case InitBlockRed
  thus ?case
    by (fastforce elim!: eval_cases intro: eval_evals.intros eval_finalId
                  simp: assigned_def map_upd_triv fun_upd_same)
next
  case (RedInitBlock V T v u s b)
  then have "P ⊢ ⟨Val u,s⟩ ⇒ ⟨e',s'⟩" by simp
  then obtain s': "s'=s" and e': "e'=Val u" by cases simp
  obtain h l sh where s: "s=(h,l,sh)" by (cases s)
  have "P ⊢ ⟨{V:T :=Val v; Val u},(h,l,sh)⟩ ⇒ ⟨Val u,(h, (l(V↦v))(V:=l V), sh)⟩"
    by (fastforce intro!: eval_evals.intros)
  then have "P ⊢ ⟨{V:T := Val v; Val u},s⟩ ⇒ ⟨e',s'⟩" using s s' e' by simp
  then show ?case by simp
next
  case BlockRedNone
  thus ?case
    by (fastforce elim!: eval_cases intro: eval_evals.intros 
                 simp add: fun_upd_same fun_upd_idem)
next
  case BlockRedSome
  thus ?case
    by (fastforce elim!: eval_cases intro: eval_evals.intros 
                 simp add:  fun_upd_same fun_upd_idem)
next
 case (RedBlock V T v s b) 
 then have "P ⊢ ⟨Val v,s⟩ ⇒ ⟨e',s'⟩" by simp
 then obtain s': "s'=s" and e': "e'=Val v" 
    by cases simp
  obtain h l sh where s: "s=(h,l,sh)" by (cases s)
 have "P ⊢ ⟨Val v,(h,l(V:=None),sh)⟩ ⇒ ⟨Val v,(h,l(V:=None),sh)⟩" 
   by (rule eval_evals.intros)
 hence "P ⊢ ⟨{V:T;Val v},(h,l,sh)⟩ ⇒ ⟨Val v,(h,(l(V:=None))(V:=l V),sh)⟩"
   by (rule eval_evals.Block)
 then have "P ⊢ ⟨{V:T; Val v},s⟩ ⇒ ⟨e',s'⟩" using s s' e' by simp
 then show ?case by simp
next
  case (SeqRed e s b e1 s1 b1 e2) show ?case
  proof(cases "val_of e")
    case None show ?thesis
    proof(cases "lass_val_of e")
      case lNone:None
      then have bconf: "P,shp s ⊢b (e,b) √" using SeqRed.prems(1) None by simp
      then show ?thesis using SeqRed using seq_ext by fastforce
    next
      case (Some p)
      obtain V' v' where p: "p = (V',v')" and e: "e = V':=Val v'"
        using lass_val_of_spec[OF Some] by(cases p, auto)
      obtain h l sh h' l' sh' where s: "s = (h,l,sh)" and s1: "s1 = (h',l',sh')" by(cases s, cases s1)
      then have red: "P ⊢ ⟨e,(h,l,sh),b⟩ → ⟨e1,(h',l',sh'),b1⟩" using SeqRed.hyps(1) by simp
      then have s1': "e1 = unit ∧ h' = h ∧ l' = l(V' ↦ v') ∧ sh' = sh"
        using lass_val_of_red[OF Some red] p e by simp
      then have eval: "P ⊢ ⟨e,s⟩ ⇒ ⟨e1,s1⟩" using e s s1 LAss Val by auto
      then show ?thesis
        by (metis SeqRed.prems(2) eval_final eval_final_same seq_ext)
    qed
  next
    case (Some a) then show ?thesis using SeqRed.hyps(1) val_no_step by blast
  qed
next
  case RedSeq
  thus ?case
    by (fastforce elim: eval_cases intro: eval_evals.intros)
next
  case CondRed
  thus ?case
    by (fastforce elim: eval_cases intro: eval_evals.intros simp: val_no_step) 
next
  case RedCondT
  thus ?case
    by (fastforce elim: eval_cases intro: eval_evals.intros)
next
  case RedCondF
  thus ?case
    by (fastforce elim: eval_cases intro: eval_evals.intros)
next
  case RedWhile
  thus ?case
    by (auto simp add: unfold_while intro:eval_evals.intros elim:eval_cases)
next
  case ThrowRed then show ?case by(fastforce elim: eval_cases simp: eval_evals.intros)
next
  case RedThrowNull
  thus ?case
    by (fastforce elim: eval_cases intro: eval_evals.intros)
next
  case TryRed thus ?case
    by(fastforce elim: eval_cases intro: eval_evals.intros)
next
  case RedTryCatch
  thus ?case
    by (fastforce elim: eval_cases intro: eval_evals.intros)
next
  case (RedTryFail s a D fs C V e2 b)
  thus ?case
    by (cases s)(auto elim!: eval_cases intro: eval_evals.intros)
next
  case ListRed1
  thus ?case
    by (fastforce elim: evals_cases intro: eval_evals.intros simp: val_no_step)
next
  case ListRed2
  thus ?case
    by (fastforce elim!: evals_cases eval_cases 
                 intro: eval_evals.intros eval_finalId)
next
  case (RedInit e1 C b s1 b') then show ?case using InitFinal by simp
next
  case (InitNoneRed sh C C' Cs e h l b)
  show ?case using InitNone InitNoneRed.hyps InitNoneRed.prems(2) by auto
next
  case (RedInitDone sh C sfs C' Cs e h l b)
  show ?case using InitDone RedInitDone.hyps RedInitDone.prems(2) by auto
next
  case (RedInitProcessing sh C sfs C' Cs e h l b)
  show ?case using InitProcessing RedInitProcessing.hyps RedInitProcessing.prems(2) by auto
next
  case (RedInitError sh C sfs C' Cs e h l b)
  show ?case using InitError RedInitError.hyps RedInitError.prems(2) by auto
next
  case (InitObjectRed sh C sfs sh' C' Cs e h l b) show ?case using InitObject InitObjectRed by auto
next
  case (InitNonObjectSuperRed sh C sfs D r sh' C' Cs e h l b)
  show ?case using InitNonObject InitNonObjectSuperRed by auto
next
  case (RedInitRInit C' C Cs e h l sh b)
  show ?case using InitRInit RedInitRInit by auto
next
  case (RInitRed e s b e'' s'' b'' C Cs e0)
  then have IH: "⋀e' s'. P ⊢ ⟨e'',s''⟩ ⇒ ⟨e',s'⟩ ⟹ P ⊢ ⟨e,s⟩ ⇒ ⟨e',s'⟩" by simp
  show ?case using RInitRed rinit_ext[OF IH] by simp
next
  case (RedRInit sh C sfs i sh' C' Cs v e h l b s' e')
  then have init: "P ⊢ ⟨(INIT C' (Cs,True) ← e), (h, l, sh(C ↦ (sfs, Done)))⟩ ⇒ ⟨e',s'⟩"
    using RedRInit by simp
  then show ?case using RInit RedRInit.hyps(1) RedRInit.hyps(3) Val by fastforce
next
  case BinOpThrow2
  thus ?case
    by (fastforce elim: eval_cases intro: eval_evals.intros)
next
  case FAssThrow2
  thus ?case
    by (fastforce elim: eval_cases intro: eval_evals.intros)
next
  case SFAssThrow
  then show ?case
    by (fastforce elim: eval_cases intro: eval_evals.intros)
next
  case (CallThrowParams es vs e es' v M s b)
  have val: "P ⊢ ⟨Val v,s⟩ ⇒ ⟨Val v,s⟩" by (rule eval_evals.intros)
  have eval_e: "P ⊢ ⟨throw (e),s⟩ ⇒ ⟨e',s'⟩" using CallThrowParams by simp
  then obtain xa where e': "e' = Throw xa" by (cases) (auto dest!: eval_final)
  with list_eval_Throw [OF eval_e]
  have vals: "P ⊢ ⟨es,s⟩ [⇒] ⟨map Val vs @ Throw xa # es',s'⟩"
    using CallThrowParams.hyps(1) eval_e list_eval_Throw by blast
  then have "P ⊢ ⟨Val v∙M(es),s⟩ ⇒ ⟨Throw xa,s'⟩"
   using eval_evals.CallParamsThrow[OF val vals] by simp
  thus ?case using e' by simp
next
  case (SCallThrowParams es vs e es' C M s b)
  have eval_e: "P ⊢ ⟨throw (e),s⟩ ⇒ ⟨e',s'⟩" using SCallThrowParams by simp
  then obtain xa where e': "e' = Throw xa" by (cases) (auto dest!: eval_final)
  then have "P ⊢ ⟨es,s⟩ [⇒] ⟨map Val vs @ Throw xa # es',s'⟩"
    using SCallThrowParams.hyps(1) eval_e list_eval_Throw by blast
  then have "P ⊢ ⟨C∙sM(es),s⟩ ⇒ ⟨Throw xa,s'⟩"
    by (rule eval_evals.SCallParamsThrow)
  thus ?case using e' by simp
next
  case (BlockThrow V T a s b)
  then have "P ⊢ ⟨Throw a, s⟩ ⇒ ⟨e',s'⟩" by simp
  then obtain s': "s' = s" and e': "e' = Throw a"
    by cases (auto elim!:eval_cases)
  obtain h l sh where s: "s=(h,l,sh)" by (cases s)
  have "P ⊢ ⟨Throw a, (h,l(V:=None),sh)⟩ ⇒ ⟨Throw a, (h,l(V:=None),sh)⟩"
    by (simp add:eval_evals.intros eval_finalId)
  hence "P⊢⟨{V:T;Throw a},(h,l,sh)⟩ ⇒ ⟨Throw a, (h,(l(V:=None))(V:=l V),sh)⟩"
    by (rule eval_evals.Block)
  then have "P ⊢ ⟨{V:T; Throw a},s⟩ ⇒ ⟨e',s'⟩" using s s' e' by simp
  then show ?case by simp
next
  case (InitBlockThrow V T v a s b)
  then have "P ⊢ ⟨Throw a,s⟩ ⇒ ⟨e',s'⟩" by simp
  then obtain s': "s' = s" and e': "e' = Throw a"
    by cases (auto elim!:eval_cases)
  obtain h l sh where s: "s = (h,l,sh)" by (cases s)
  have "P ⊢ ⟨{V:T :=Val v; Throw a},(h,l,sh)⟩ ⇒ ⟨Throw a, (h, (l(V↦v))(V:=l V),sh)⟩"
    by(fastforce intro:eval_evals.intros)
  then have "P ⊢ ⟨{V:T := Val v; Throw a},s⟩ ⇒ ⟨e',s'⟩" using s s' e' by simp
  then show ?case by simp
next
  case (RInitInitThrow sh C sfs i sh' a D Cs e h l b)
  have IH: "⋀e' s'. P ⊢ ⟨RI (D,Throw a) ; Cs ← e,(h, l, sh(C ↦ (sfs, Error)))⟩ ⇒ ⟨e',s'⟩ ⟹
    P ⊢ ⟨RI (C,Throw a) ; D # Cs ← e,(h, l, sh)⟩ ⇒ ⟨e',s'⟩"
    using RInitInitFail[OF eval_finalId] RInitInitThrow by simp
  then show ?case using RInitInitThrow.hyps(2) RInitInitThrow.prems(2) by auto
next
  case (RInitThrow sh C sfs i sh' a e h l b)
  then have e': "e' = Throw a" and s': "s' = (h,l,sh')"
    using eval_final_same final_def by fastforce+
  show ?case using RInitFailFinal RInitThrow.hyps(1) RInitThrow.hyps(2) e' eval_finalId s' by auto
qed(auto elim: eval_cases simp: eval_evals.intros)
(*>*)

(*<*)
(* ... und wieder anschalten: *)
declare split_paired_All [simp] split_paired_Ex [simp]
(*>*)

text ‹ Its extension to @{text"→*"}: › 

lemma extend_eval:
assumes wf: "wwf_J_prog P"
shows "⟦ P ⊢ ⟨e,s,b⟩ →* ⟨e'',s'',b''⟩; P ⊢ ⟨e'',s''⟩ ⇒ ⟨e',s'⟩;
         iconf (shp s) e; P,shp s ⊢b (e::expr,b) √ ⟧
  ⟹ P ⊢ ⟨e,s⟩ ⇒ ⟨e',s'⟩"
(*<*)
proof (induct rule: converse_rtrancl_induct3)
  case refl then show ?case by simp
next
  case (step e1 s1 b1 e2 s2 b2)
  then have ic: "iconf (shp s2) e2" using Red_preserves_iconf local.wf by blast
  then have ec: "P,shp s2 ⊢b (e2,b2) √"
    using Red_preserves_bconf local.wf step.hyps(1) step.prems(2) step.prems(3) by blast
  show ?case using step ic ec extend_1_eval[OF wf step.hyps(1)] by simp
qed
(*>*)


lemma extend_evals:
assumes wf: "wwf_J_prog P"
shows "⟦ P ⊢ ⟨es,s,b⟩ [→]* ⟨es'',s'',b''⟩; P ⊢ ⟨es'',s''⟩ [⇒] ⟨es',s'⟩;
         iconfs (shp s) es; P,shp s ⊢b (es::expr list,b) √ ⟧
  ⟹ P ⊢ ⟨es,s⟩ [⇒] ⟨es',s'⟩"
(*<*)
proof (induct rule: converse_rtrancl_induct3)
  case refl then show ?case by simp
next
  case (step es1 s1 b1 es2 s2 b2)
  then have ic: "iconfs (shp s2) es2" using Reds_preserves_iconf local.wf by blast
  then have ec: "P,shp s2 ⊢b (es2,b2) √"
    using Reds_preserves_bconf local.wf step.hyps(1) step.prems(2) step.prems(3) by blast
  show ?case using step ic ec extend_1_evals[OF wf step.hyps(1)] by simp
qed
(*>*)

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

theorem
assumes wf: "wwf_J_prog P"
shows small_by_big:
 "⟦P ⊢ ⟨e,s,b⟩ →* ⟨e',s',b'⟩; iconf (shp s) e; P,shp s ⊢b (e,b) √; final e'⟧
   ⟹ P ⊢ ⟨e,s⟩ ⇒ ⟨e',s'⟩"
and "⟦P ⊢ ⟨es,s,b⟩ [→]* ⟨es',s',b'⟩; iconfs (shp s) es; P,shp s ⊢b (es,b) √; finals es'⟧
   ⟹ P ⊢ ⟨es,s⟩ [⇒] ⟨es',s'⟩"
(*<*)
proof -
  note wf 
  moreover assume "P ⊢ ⟨e,s,b⟩ →* ⟨e',s',b'⟩"
  moreover assume "final e'"
  then have "P ⊢ ⟨e',s'⟩ ⇒ ⟨e',s'⟩"
    by (simp add: eval_finalId)
  moreover assume "iconf (shp s) e"
  moreover assume "P,shp s ⊢b (e,b) √"
  ultimately show "P ⊢ ⟨e,s⟩ ⇒ ⟨e',s'⟩"
    by (rule extend_eval)
next
  assume fins: "finals es'"
  note wf 
  moreover assume "P ⊢ ⟨es,s,b⟩ [→]* ⟨es',s',b'⟩"
  moreover have "P ⊢ ⟨es',s'⟩ [⇒] ⟨es',s'⟩" using fins
    by (rule eval_finalsId)
  moreover assume "iconfs (shp s) es"
  moreover assume "P,shp s ⊢b (es,b) √"
  ultimately show "P ⊢ ⟨es,s⟩ [⇒] ⟨es',s'⟩"
    by (rule extend_evals)
qed
(*>*)

subsection "Equivalence"

text‹ And now, the crowning achievement: ›

corollary big_iff_small:
"⟦ wwf_J_prog P; iconf (shp s) e; P,shp s ⊢b (e::expr,b) √ ⟧
  ⟹ P ⊢ ⟨e,s⟩ ⇒ ⟨e',s'⟩  =  (P ⊢ ⟨e,s,b⟩ →* ⟨e',s',False⟩ ∧ final e')"
(*<*)by(blast dest: big_by_small eval_final small_by_big)(*>*)

corollary big_iff_small_WT:
  "wwf_J_prog P ⟹ P,E ⊢ e::T ⟹ P,shp s ⊢b (e,b) √ ⟹
  P ⊢ ⟨e,s⟩ ⇒ ⟨e',s'⟩  =  (P ⊢ ⟨e,s,b⟩ →* ⟨e',s',False⟩ ∧ final e')"
(*<*)by(blast dest: big_iff_small WT_nsub_RI nsub_RI_iconf)(*>*)


subsection ‹ Lifting type safety to @{text"⇒"} ›

text‹ \dots and now to the big step semantics, just for fun. ›

lemma eval_preserves_sconf:
fixes s::state and s'::state
assumes  "wf_J_prog P" and "P ⊢ ⟨e,s⟩ ⇒ ⟨e',s'⟩" and "iconf (shp s) e"
 and "P,E ⊢ e::T" and "P,E ⊢ s√"
shows "P,E ⊢ s'√"
(*<*)
proof -
  have "P,shp s ⊢b (e,False) √" by(simp add: bconf_def)
  with assms show ?thesis
    by(blast intro:Red_preserves_sconf Red_preserves_iconf Red_preserves_bconf big_by_small
                   WT_implies_WTrt wf_prog_wwf_prog)
qed
(*>*)


lemma eval_preserves_type:
fixes s::state
assumes wf: "wf_J_prog P"
 and "P ⊢ ⟨e,s⟩ ⇒ ⟨e',s'⟩" and "P,E ⊢ s√" and "iconf (shp s) e" and "P,E ⊢ e::T"
shows "∃T'. P ⊢ T' ≤ T ∧ P,E,hp s',shp s' ⊢ e':T'"
(*<*)
proof -
  have "P,shp s ⊢b (e,False) √" by(simp add: bconf_def)
  with assms show ?thesis by(blast dest:big_by_small[OF wf_prog_wwf_prog[OF wf]]
                                        WT_implies_WTrt Red_preserves_type[OF wf])
qed
(*>*)


end