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 ⊢ ⟨