# 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) ← e⇩i) e = (INIT C (Cs,b) ← e)" |
"init_switch (RI(C,e');Cs ← e⇩i) 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,e⇩0);Cs ← e) = Some (last (C#Cs))" |
"INIT_class _ = None"

lemma init_red_init:
"⟦ init_exp_of e⇩0 = ⌊e⌋; P ⊢ ⟨e⇩0,s⇩0,b⇩0⟩ → ⟨e⇩1,s⇩1,b⇩1⟩ ⟧
⟹ (init_exp_of e⇩1 = ⌊e⌋ ∧ (INIT_class e⇩0 = ⌊C⌋ ⟶ INIT_class e⇩1 = ⌊C⌋))
∨ (e⇩1 = e ∧ b⇩1 = icheck P (the(INIT_class e⇩0)) e) ∨ (∃a. e⇩1 = throw a)"
by(erule red.cases, auto)

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

lemma init_red_sync:
"⟦ P ⊢ ⟨e⇩0,s⇩0,b⇩0⟩ → ⟨e⇩1,s⇩1,b⇩1⟩; init_exp_of e⇩0 = ⌊e⌋; e⇩1 ≠ e ⟧
⟹ (⋀e'. P ⊢ ⟨init_switch e⇩0 e',s⇩0,b⇩0⟩ → ⟨init_switch e⇩1 e',s⇩1,b⇩1⟩)"
proof(induct rule: red.cases) qed(simp_all add: red_reds.intros)

lemma init_red_sync_end:
"⟦ P ⊢ ⟨e⇩0,s⇩0,b⇩0⟩ → ⟨e⇩1,s⇩1,b⇩1⟩; init_exp_of e⇩0 = ⌊e⌋; e⇩1 = e; throw_of e = None ⟧
⟹ (⋀e'. ¬sub_RI e' ⟹ P ⊢ ⟨init_switch e⇩0 e',s⇩0,b⇩0⟩ → ⟨e',s⇩1,icheck P (the(INIT_class e⇩0)) e'⟩)"
proof(induct rule: red.cases) qed(simp_all add: red_reds.intros)

lemma init_reds_sync_unit':
"⟦ P ⊢ ⟨e⇩0,s⇩0,b⇩0⟩ →* ⟨Val v',s⇩1,b⇩1⟩; init_exp_of e⇩0 = ⌊unit⌋; INIT_class e⇩0 = ⌊C⌋ ⟧
⟹ (⋀e'. ¬sub_RI e' ⟹ P ⊢ ⟨init_switch e⇩0 e',s⇩0,b⇩0⟩ →* ⟨e',s⇩1,icheck P (the(INIT_class e⇩0)) 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',s⇩1,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 = s⇩1" "b1 = b⇩1" using reds_final_same[OF step.hyps(2)] assm
then have step': "P ⊢ ⟨init_switch e0 e',s0,b0⟩ → ⟨e',s⇩1,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',s⇩1,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 ⊢ ⟨e⇩0,s⇩0,b⇩0⟩ →* ⟨throw a,s⇩1,b⇩1⟩; init_exp_of e⇩0 = ⌊unit⌋ ⟧
⟹ (⋀e'. P ⊢ ⟨init_switch e⇩0 e',s⇩0,b⇩0⟩ →* ⟨throw a,s⇩1,b⇩1⟩)"
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 ⊢ ⟨e⇩0,s⇩0,b⇩0⟩ →* ⟨Val v',s⇩1,b⇩1⟩" and "init_exp_of e⇩0 = ⌊unit⌋" and "INIT_class e⇩0 = ⌊C⌋"
and "¬sub_RI e'"
shows "P ⊢ ⟨init_switch e⇩0 e',s⇩0,b⇩0⟩ →* ⟨e',s⇩1,icheck P (the(INIT_class e⇩0)) e'⟩"
using init_reds_sync_unit'[OF assms] by clarsimp

lemma init_reds_sync_unit_throw:
assumes "P ⊢ ⟨e⇩0,s⇩0,b⇩0⟩ →* ⟨throw a,s⇩1,b⇩1⟩" and "init_exp_of e⇩0 = ⌊unit⌋"
shows "P ⊢ ⟨init_switch e⇩0 e',s⇩0,b⇩0⟩ →* ⟨throw a,s⇩1,b⇩1⟩"
using init_reds_sync_unit_throw'[OF assms] by clarsimp

― ‹ init reds lemmas ›

lemma InitSeqReds:
assumes "P ⊢ ⟨INIT C ([C],b) ← unit,s⇩0,b⇩0⟩ →* ⟨Val v',s⇩1,b⇩1⟩"
and "P ⊢ ⟨e,s⇩1,icheck P C e⟩ →* ⟨e⇩2,s⇩2,b⇩2⟩" and "¬sub_RI e"
shows "P ⊢ ⟨INIT C ([C],b) ← e,s⇩0,b⇩0⟩ →* ⟨e⇩2,s⇩2,b⇩2⟩"
using assms
proof -
have "P ⊢ ⟨init_switch (INIT C ([C],b) ← unit) e,s⇩0,b⇩0⟩ →* ⟨e,s⇩1,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,s⇩0,b⇩0⟩ →* ⟨throw a,s⇩1,b⇩1⟩"
shows "P ⊢ ⟨INIT C ([C],b) ← e,s⇩0,b⇩0⟩ →* ⟨throw a,s⇩1,b⇩1⟩"
using assms
proof -
have "P ⊢ ⟨init_switch (INIT C ([C],b) ← unit) e,s⇩0,b⇩0⟩ →* ⟨throw a,s⇩1,b⇩1⟩"
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 ← e⇩0, s, b⟩ →* ⟨RI (C,e');Cs ← e⇩0, 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 ⊢ ⟨e⇩0,s⇩0,b⇩0⟩ →* ⟨Val v,(h⇩1,l⇩1,sh⇩1),b⇩1⟩;
sh⇩1 C = Some (sfs, i); sh⇩2 = sh⇩1(C ↦ (sfs,Done)); C' = last(C#Cs);
P ⊢ ⟨INIT C' (Cs,True) ← e,(h⇩1,l⇩1,sh⇩2),b⇩1⟩ →* ⟨e',s',b'⟩ ⟧
⟹ P ⊢ ⟨RI (C, e⇩0);Cs ← e,s⇩0,b⇩0⟩ →* ⟨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 ← e⇩0, (h',l',sh''),b'⟩ →* ⟨e⇩1,s⇩1,b⇩1⟩ ⟧
⟹ P ⊢ ⟨RI (C, e);D#Cs ← e⇩0,s,b⟩ →* ⟨e⇩1,s⇩1,b⇩1⟩"
(*<*)
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 ← e⇩0,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])(*>*)

"⟦ 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» e⇩2, s,b⟩ →* ⟨e' «bop» e⇩2, 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 e⇩1_steps: "P ⊢ ⟨e⇩1,s⇩0,b⇩0⟩ →* ⟨Val v⇩1,s⇩1,b⇩1⟩"
and e⇩2_steps: "P ⊢ ⟨e⇩2,s⇩1,b⇩1⟩ →* ⟨Val v⇩2,s⇩2,b⇩2⟩"
and op: "binop(bop,v⇩1,v⇩2) = Some v"
shows "P ⊢ ⟨e⇩1 «bop» e⇩2, s⇩0,b⇩0⟩ →* ⟨Val v,s⇩2,b⇩2⟩"
(*<*)(is "(?x, ?z) ∈ (red P)⇧*")
proof -
let ?y = "(Val v⇩1 «bop» e⇩2, s⇩1,b⇩1)"
let ?y' = "(Val v⇩1 «bop» Val v⇩2, s⇩2,b⇩2)"
have "(?x, ?y) ∈ (red P)⇧*" by(rule BinOp1Reds[OF e⇩1_steps])
also have "(?y, ?y') ∈ (red P)⇧*" by(rule BinOp2Reds[OF e⇩2_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» e⇩2, s,b⟩ →* ⟨throw e', s',b'⟩"
(*<*)by(rule BinOp1Reds[THEN rtrancl_into_rtrancl, OF _ red_reds.BinOpThrow1])(*>*)

lemma BinOpRedsThrow2:
assumes e⇩1_steps: "P ⊢ ⟨e⇩1,s⇩0,b⇩0⟩ →* ⟨Val v⇩1,s⇩1,b⇩1⟩"
and e⇩2_steps: "P ⊢ ⟨e⇩2,s⇩1,b⇩1⟩ →* ⟨throw e,s⇩2,b⇩2⟩"
shows "P ⊢ ⟨e⇩1 «bop» e⇩2, s⇩0,b⇩0⟩ →* ⟨throw e,s⇩2,b⇩2⟩"
(*<*)(is "(?x, ?z) ∈ (red P)⇧*")
proof -
let ?y = "(Val v⇩1 «bop» e⇩2, s⇩1,b⇩1)"
let ?y' = "(Val v⇩1 «bop» throw e, s⇩2,b⇩2)"
have "(?x, ?y) ∈ (red P)⇧*" by(rule BinOp1Reds[OF e⇩1_steps])
also have "(?y, ?y') ∈ (red P)⇧*" by(rule BinOp2Reds[OF e⇩2_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}:=e⇩2, s,b⟩ →* ⟨e'∙F{D}:=e⇩2, 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 e⇩1_steps: "P ⊢ ⟨e⇩1,s⇩0,b⇩0⟩ →* ⟨addr a,s⇩1,b⇩1⟩"
and e⇩2_steps: "P ⊢ ⟨e⇩2,s⇩1,b⇩1⟩ →* ⟨Val v,(h⇩2,l⇩2,sh⇩2),b⇩2⟩"
and cF: "P ⊢ C has F,NonStatic:t in D" and hC: "Some(C,fs) = h⇩2 a"
shows "P ⊢ ⟨e⇩1∙F{D}:=e⇩2, s⇩0, b⇩0⟩ →* ⟨unit, (h⇩2(a↦(C,fs((F,D)↦v))),l⇩2,sh⇩2),b⇩2⟩"
(*<*)(is "(?x, ?z) ∈ (red P)⇧*")
proof -
let ?y = "(addr a∙F{D}:=e⇩2, s⇩1, b⇩1)"
let ?y' = "(addr a∙F{D}:=Val v::expr,(h⇩2,l⇩2,sh⇩2),b⇩2)"
have "(?x, ?y) ∈ (red P)⇧*" by(rule FAssReds1[OF e⇩1_steps])
also have "(?y, ?y') ∈ (red P)⇧*" by(rule FAssReds2[OF e⇩2_steps])
also have "(?y', ?z) ∈ (red P)" using RedFAss[OF cF] hC by simp
ultimately show ?thesis by simp
qed
(*>*)

lemma FAssRedsNull:
assumes e⇩1_steps: "P ⊢ ⟨e⇩1,s⇩0,b⇩0⟩ →* ⟨null,s⇩1,b⇩1⟩"
and e⇩2_steps: "P ⊢ ⟨e⇩2,s⇩1,b⇩1⟩ →* ⟨Val v,s⇩2,b⇩2⟩"
shows "P ⊢ ⟨e⇩1∙F{D}:=e⇩2, s⇩0, b⇩0⟩ →* ⟨THROW NullPointer, s⇩2, b⇩2⟩"
(*<*)(is "(?x, ?z) ∈ (red P)⇧*")
proof -
let ?y = "(null∙F{D}:=e⇩2, s⇩1, b⇩1)"
let ?y' = "(null∙F{D}:=Val v::expr,s⇩2,b⇩2)"
have "(?x, ?y) ∈ (red P)⇧*" by(rule FAssReds1[OF e⇩1_steps])
also have "(?y, ?y') ∈ (red P)⇧*" by(rule FAssReds2[OF e⇩2_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}:=e⇩2, s,b⟩ →* ⟨throw e', s',b'⟩"
(*<*)by(rule FAssReds1[THEN rtrancl_into_rtrancl, OF _ red_reds.FAssThrow1])(*>*)

lemma FAssRedsThrow2:
assumes e⇩1_steps: "P ⊢ ⟨e⇩1,s⇩0,b⇩0⟩ →* ⟨Val v,s⇩1,b⇩1⟩"
and e⇩2_steps: "P ⊢ ⟨e⇩2,s⇩1,b⇩1⟩ →* ⟨throw e,s⇩2,b⇩2⟩"
shows "P ⊢ ⟨e⇩1∙F{D}:=e⇩2,s⇩0,b⇩0⟩ →* ⟨throw e,s⇩2,b⇩2⟩"
(*<*)(is "(?x, ?z) ∈ (red P)⇧*")
proof -
let ?y = "(Val v∙F{D}:=e⇩2,s⇩1,b⇩1)"
let ?y' = "(Val v∙F{D}:=throw e,s⇩2,b⇩2)"
have "(?x, ?y) ∈ (red P)⇧*" by(rule FAssReds1[OF e⇩1_steps])
also have "(?y, ?y') ∈ (red P)⇧*" by(rule FAssReds2[OF e⇩2_steps])
also have "(?y', ?z) ∈ (red P)" by(rule red_reds.FAssThrow2)
ultimately show ?thesis by simp
qed
(*>*)

lemma FAssRedsNone:
assumes e⇩1_steps: "P ⊢ ⟨e⇩1,s⇩0,b⇩0⟩ →* ⟨addr a,s⇩1,b⇩1⟩"
and e⇩2_steps: "P ⊢ ⟨e⇩2,s⇩1,b⇩1⟩ →* ⟨Val v,(h⇩2,l⇩2,sh⇩2),b⇩2⟩"
and hC: "h⇩2 a = Some(C,fs)" and ncF: "¬(∃b t. P ⊢ C has F,b:t in D)"
shows "P ⊢ ⟨e⇩1∙F{D}:=e⇩2, s⇩0, b⇩0⟩ →* ⟨THROW NoSuchFieldError, (h⇩2,l⇩2,sh⇩2), b⇩2⟩"
(*<*)(is "(?x, ?z) ∈ (red P)⇧*")
proof -
let ?y = "(addr a∙F{D}:=e⇩2, s⇩1, b⇩1)"
let ?y' = "(addr a∙F{D}:=Val v::expr,(h⇩2,l⇩2,sh⇩2),b⇩2)"
have "(?x, ?y) ∈ (red P)⇧*" by(rule FAssReds1[OF e⇩1_steps])
also have "(?y, ?y') ∈ (red P)⇧*" by(rule FAssReds2[OF e⇩2_steps])
also have "(?y', ?z) ∈ (red P)"
using RedFAssNone[OF _ ncF] hC by simp
ultimately show ?thesis by simp
qed
(*>*)

lemma FAssRedsStatic:
assumes e⇩1_steps: "P ⊢ ⟨e⇩1,s⇩0,b⇩0⟩ →* ⟨addr a,s⇩1,b⇩1⟩"
and e⇩2_steps: "P ⊢ ⟨e⇩2,s⇩1,b⇩1⟩ →* ⟨Val v,(h⇩2,l⇩2,sh⇩2),b⇩2⟩"
and hC: "h⇩2 a = Some(C,fs)" and cF_Static: "P ⊢ C has F,Static:t in D"
shows "P ⊢ ⟨e⇩1∙F{D}:=e⇩2, s⇩0, b⇩0⟩ →* ⟨THROW IncompatibleClassChangeError, (h⇩2,l⇩2,sh⇩2), b⇩2⟩"
(*<*)(is "(?x, ?z) ∈ (red P)⇧*")
proof -
let ?y = "(addr a∙F{D}:=e⇩2, s⇩1, b⇩1)"
let ?y' = "(addr a∙F{D}:=Val v::expr,(h⇩2,l⇩2,sh⇩2),b⇩2)"
have "(?x, ?y) ∈ (red P)⇧*" by(rule FAssReds1[OF e⇩1_steps])
also have "(?y, ?y') ∈ (red P)⇧*" by(rule FAssReds2[OF e⇩2_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 e⇩2_steps: "P ⊢ ⟨e⇩2,s⇩0,b⇩0⟩ →* ⟨Val v,(h⇩2,l⇩2,sh⇩2),b⇩2⟩"
and cF: "P ⊢ C has F,Static:t in D"
and shD: "sh⇩2 D = ⌊(sfs,Done)⌋"
shows "P ⊢ ⟨C∙⇩sF{D}:=e⇩2, s⇩0, b⇩0⟩ →* ⟨unit, (h⇩2,l⇩2,sh⇩2(D↦(sfs(F↦v), Done))),False⟩"
(*<*)(is "(?a, ?c) ∈ (red P)⇧*")
proof -
let ?b = "(C∙⇩sF{D}:=Val v::expr, (h⇩2,l⇩2,sh⇩2), b⇩2)"
have "(?a, ?b) ∈ (red P)⇧*" by(rule SFAssReds[OF e⇩2_steps])
also have "(?b, ?c) ∈ (red P)⇧*" proof(cases b⇩2)
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, (h⇩2,l⇩2,sh⇩2), 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 ⊢ ⟨e⇩2,s⇩0,b⇩0⟩ →* ⟨throw e,s⇩2,b⇩2⟩ ⟧
⟹ P ⊢ ⟨C∙⇩sF{D}:=e⇩2,s⇩0,b⇩0⟩ →* ⟨throw e,s⇩2,b⇩2⟩"
(*<*)by(rule SFAssReds[THEN rtrancl_into_rtrancl, OF _ red_reds.SFAssThrow])(*>*)

lemma SFAssRedsNone:
"⟦ P ⊢ ⟨e⇩2,s⇩0,b⇩0⟩ →* ⟨Val v,(h⇩2,l⇩2,sh⇩2),b⇩2⟩;
¬(∃b t. P ⊢ C has F,b:t in D) ⟧ ⟹
P ⊢ ⟨C∙⇩sF{D}:=e⇩2,s⇩0,b⇩0⟩ →* ⟨THROW NoSuchFieldError, (h⇩2,l⇩2,sh⇩2),False⟩"
(*<*)by(rule SFAssReds[THEN rtrancl_into_rtrancl, OF _ RedSFAssNone])(*>*)

lemma SFAssRedsNonStatic:
"⟦ P ⊢ ⟨e⇩2,s⇩0,b⇩0⟩ →* ⟨Val v,(h⇩2,l⇩2,sh⇩2),b⇩2⟩;
P ⊢ C has F,NonStatic:t in D ⟧ ⟹
P ⊢ ⟨C∙⇩sF{D}:=e⇩2,s⇩0,b⇩0⟩ →* ⟨THROW IncompatibleClassChangeError,(h⇩2,l⇩2,sh⇩2),False⟩"
(*<*)by(rule SFAssReds[THEN rtrancl_into_rtrancl, OF _ RedSFAssNonStatic])(*>*)

lemma SFAssInitReds:
assumes e⇩2_steps: "P ⊢ ⟨e⇩2,s⇩0,b⇩0⟩ →* ⟨Val v,(h⇩2,l⇩2,sh⇩2),False⟩"
and cF: "P ⊢ C has F,Static:t in D"
and nDone: "∄sfs. sh⇩2 D = Some (sfs, Done)"
and INIT_steps: "P ⊢ ⟨INIT D ([D],False) ← unit,(h⇩2,l⇩2,sh⇩2),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}:=e⇩2,s⇩0,b⇩0⟩ →* ⟨unit,(h',l',sh''),False⟩"
(*<*)(is "(?x, ?z) ∈ (red P)⇧*")
proof -
let ?y = "(C∙⇩sF{D} := Val v::expr,(h⇩2, l⇩2, sh⇩2),False)"
let ?y' = "(INIT D ([D],False) ← C∙⇩sF{D} := Val v::expr,(h⇩2, l⇩2, sh⇩2),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 e⇩2_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 e⇩2_steps: "P ⊢ ⟨e⇩2,s⇩0,b⇩0⟩ →* ⟨Val v,(h⇩2,l⇩2,sh⇩2),False⟩"
and cF: "P ⊢ C has F,Static:t in D"
and nDone: "∄sfs. sh⇩2 D = Some (sfs, Done)"
and INIT_steps: "P ⊢ ⟨INIT D ([D],False) ← unit,(h⇩2,l⇩2,sh⇩2),False⟩ →* ⟨throw a,s',b'⟩"
shows "P ⊢ ⟨C∙⇩sF{D}:=e⇩2,s⇩0,b⇩0⟩ →* ⟨throw a,s',b'⟩"
(*<*)(is "(?x, ?z) ∈ (red P)⇧*")
proof -
let ?y = "(C∙⇩sF{D} := Val v::expr,(h⇩2, l⇩2, sh⇩2),False)"
let ?y' = "(INIT D ([D],False) ← C∙⇩sF{D} := Val v::expr,(h⇩2, l⇩2, sh⇩2),False)"
have "(?x, ?y) ∈ (red P)⇧*" by(rule SFAssReds[OF e⇩2_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;;e⇩2, s,b⟩ →* ⟨e';;e⇩2, 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;;e⇩2, s,b⟩ →* ⟨throw e', s',b'⟩"
(*<*)by(rule SeqReds[THEN rtrancl_into_rtrancl, OF _ red_reds.SeqThrow])(*>*)

lemma SeqReds2:
assumes e⇩1_steps: "P ⊢ ⟨e⇩1,s⇩0,b⇩0⟩ →* ⟨Val v⇩1,s⇩1,b⇩1⟩"
and   e⇩2_steps: "P ⊢ ⟨e⇩2,s⇩1,b⇩1⟩ →* ⟨e⇩2',s⇩2,b⇩2⟩"
shows "P ⊢ ⟨e⇩1;;e⇩2, s⇩0,b⇩0⟩ →* ⟨e⇩2',s⇩2,b⇩2⟩"
(*<*)(is "(?x, ?z) ∈ (red P)⇧*")
proof -
let ?y = "(Val v⇩1;; e⇩2,s⇩1,b⇩1)"
have "(?x, ?y) ∈ (red P)⇧*" by(rule SeqReds[OF e⇩1_steps])
also have "(?y, ?z) ∈ (red P)⇧*"
by(rule RedSeq[THEN converse_rtrancl_into_rtrancl, OF e⇩2_steps])
ultimately show ?thesis by simp
qed
(*>*)

subsubsection"If"

lemma CondReds:
"P ⊢ ⟨e,s,b⟩ →* ⟨e',s',b'⟩ ⟹ P ⊢ ⟨if (e) e⇩1 else e⇩2,s,b⟩ →* ⟨if (e') e⇩1 else e⇩2,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) e⇩1 else e⇩2, s,b⟩ →* ⟨throw a,s',b'⟩"
(*<*)by(rule CondReds[THEN rtrancl_into_rtrancl, OF _ red_reds.CondThrow])(*>*)

lemma CondReds2T:
assumes e_steps: "P ⊢ ⟨e,s⇩0,b⇩0⟩ →* ⟨true,s⇩1,b⇩1⟩"
and   e⇩1_steps: "P ⊢ ⟨e⇩1, s⇩1,b⇩1⟩ →* ⟨e',s⇩2,b⇩2⟩"
shows "P ⊢ ⟨if (e) e⇩1 else e⇩2, s⇩0,b⇩0⟩ →* ⟨e',s⇩2,b⇩2⟩"
(*<*)(is "(?x, ?z) ∈ (red P)⇧*")
proof -
let ?y = "(if (true) e⇩1 else e⇩2,s⇩1,b⇩1)"
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 e⇩1_steps])
ultimately show ?thesis by simp
qed
(*>*)

lemma CondReds2F:
assumes e_steps: "P ⊢ ⟨e,s⇩0,b⇩0⟩ →* ⟨false,s⇩1,b⇩1⟩"
and   e⇩2_steps: "P ⊢ ⟨e⇩2, s⇩1,b⇩1⟩ →* ⟨e',s⇩2,b⇩2⟩"
shows "P ⊢ ⟨if (e) e⇩1 else e⇩2, s⇩0,b⇩0⟩ →* ⟨e',s⇩2,b⇩2⟩"
(*<*)(is "(?x, ?z) ∈ (red P)⇧*")
proof -
let ?y = "(if (false) e⇩1 else e⇩2,s⇩1,b⇩1)"
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 e⇩2_steps])
ultimately show ?thesis by simp
qed
(*>*)

subsubsection "While"

lemma WhileFReds:
assumes b_steps: "P ⊢ ⟨b,s,b⇩0⟩ →* ⟨false,s',b'⟩"
shows "P ⊢ ⟨while (b) c,s,b⇩0⟩ →* ⟨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,b⇩0⟩ →* ⟨throw e,s',b'⟩"
shows "P ⊢ ⟨while (b) c,s,b⇩0⟩ →* ⟨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,s⇩0,b⇩0⟩ →* ⟨true,s⇩1,b⇩1⟩"
and c_steps: "P ⊢ ⟨c,s⇩1,b⇩1⟩ →* ⟨Val v⇩1,s⇩2,b⇩2⟩"
and while_steps: "P ⊢ ⟨while (b) c,s⇩2,b⇩2⟩ →* ⟨e,s⇩3,b⇩3⟩"
shows "P ⊢ ⟨while (b) c,s⇩0,b⇩0⟩ →* ⟨e,s⇩3,b⇩3⟩"
(*<*)(is "(?a, ?c) ∈ (red P)⇧*")
proof -
let ?b = "(if (b) (c;; while (b) c) else unit,s⇩0,b⇩0)"
let ?y = "(if (true) (c;; while (b) c) else unit,s⇩1,b⇩1)"
let ?b' = "(c;; while (b) c,s⇩1,b⇩1)"
let ?y' = "(Val v⇩1;; while (b) c,s⇩2,b⇩2)"
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,s⇩0,b⇩0⟩ →* ⟨true,s⇩1,b⇩1⟩"
and c_steps: "P ⊢ ⟨c,s⇩1,b⇩1⟩ →* ⟨throw e,s⇩2,b⇩2⟩"
shows "P ⊢ ⟨while (b) c,s⇩0,b⇩0⟩ →* ⟨throw e,s⇩2,b⇩2⟩"
(*<*)(is "(?a, ?c) ∈ (red P)⇧*")
proof -
let ?b = "(if (b) (c;; while (b) c) else unit,s⇩0,b⇩0)"
let ?y = "(if (true) (c;; while (b) c) else unit,s⇩1,b⇩1)"
let ?b' = "(c;; while (b) c,s⇩1,b⇩1)"
let ?y' = "(throw e;; while (b) c,s⇩2,b⇩2)"
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 ⊢ ⟨e⇩0,s⇩0,b⇩0⟩ →* ⟨e⇩2,(h⇩2,l⇩2,sh⇩2),b⇩2⟩" and fin: "final e⇩2"
shows "⋀h⇩0 l⇩0 sh⇩0. s⇩0 = (h⇩0,l⇩0(V:=None),sh⇩0) ⟹ P ⊢ ⟨{V:T; e⇩0},(h⇩0,l⇩0,sh⇩0),b⇩0⟩ →* ⟨e⇩2,(h⇩2,l⇩2(V:=l⇩0 V),sh⇩2),b⇩2⟩"
(*<*)
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 e⇩0 s⇩0 b⇩0 e⇩1 s⇩1 b⇩1)
have red: "P ⊢ ⟨e⇩0,s⇩0,b⇩0⟩ → ⟨e⇩1,s⇩1,b⇩1⟩"
and reds: "P ⊢ ⟨e⇩1,s⇩1,b⇩1⟩ →* ⟨e⇩2,(h⇩2,l⇩2,sh⇩2),b⇩2⟩"
and IH: "⋀h l sh. s⇩1 = (h,l(V := None),sh)
⟹ P ⊢ ⟨{V:T; e⇩1},(h,l,sh),b⇩1⟩ →* ⟨e⇩2,(h⇩2, l⇩2(V := l V),sh⇩2),b⇩2⟩"
and s⇩0: "s⇩0 = (h⇩0, l⇩0(V := None),sh⇩0)" by fact+
obtain h⇩1 l⇩1 sh⇩1 where s⇩1: "s⇩1 = (h⇩1,l⇩1,sh⇩1)"
using prod_cases3 by blast
show ?case
proof cases
assume "assigned V e⇩0"
then obtain v e where e⇩0: "e⇩0 = V := Val v;; e"
by (unfold assigned_def)blast
from red e⇩0 s⇩0 have e⇩1: "e⇩1 = unit;;e" and s⇩1: "s⇩1 = (h⇩0, l⇩0(V ↦ v),sh⇩0)" and b⇩1: "b⇩1 = b⇩0"
by auto
from e⇩1 fin have "e⇩1 ≠ e⇩2" by (auto simp:final_def)
then obtain e' s' b' where red1: "P ⊢ ⟨e⇩1,s⇩1,b⇩1⟩ → ⟨e',s',b'⟩"
and reds': "P ⊢ ⟨e',s',b'⟩ →* ⟨e⇩2,(h⇩2,l⇩2,sh⇩2),b⇩2⟩"
using converse_rtranclE3[OF reds] by blast
from red1 e⇩1 b⇩1 have es': "e' = e" "s' = s⇩1" "b' = b⇩0" by auto
show ?case using e⇩0 s⇩1 es' reds'
by(auto intro!: InitBlockRedsFinal[OF _ fin] simp del:fun_upd_apply)
next
assume unass: "¬ assigned V e⇩0"
show ?thesis
proof (cases "l⇩1 V")
assume None: "l⇩1 V = None"
hence "P ⊢ ⟨{V:T; e⇩0},(h⇩0,l⇩0,sh⇩0),b⇩0⟩ → ⟨{V:T; e⇩1},(h⇩1, l⇩1(V := l⇩0 V),sh⇩1),b⇩1⟩"
using s⇩0 s⇩1 red by(simp add: BlockRedNone[OF _ _ unass])
moreover
have "P ⊢ ⟨{V:T; e⇩1},(h⇩1, l⇩1(V := l⇩0 V),sh⇩1),b⇩1⟩ →* ⟨e⇩2,(h⇩2, l⇩2(V := l⇩0 V),sh⇩2),b⇩2⟩"
using IH[of _ "l⇩1(V := l⇩0 V)"] s⇩1 None by(simp add:fun_upd_idem)
ultimately show ?case by(rule converse_rtrancl_into_rtrancl)
next
fix v assume Some: "l⇩1 V = Some v"
hence "P ⊢ ⟨{V:T;e⇩0},(h⇩0,l⇩0,sh⇩0),b⇩0⟩ → ⟨{V:T := Val v; e⇩1},(h⇩1,l⇩1(V := l⇩0 V),sh⇩1),b⇩1⟩"
using s⇩0 s⇩1 red by(simp add: BlockRedSome[OF _ _ unass])
moreover
have "P ⊢ ⟨{V:T := Val v; e⇩1},(h⇩1,l⇩1(V:= l⇩0 V),sh⇩1),b⇩1⟩ →*
⟨e⇩2,(h⇩2,l⇩2(V:=l⇩0 V),sh⇩2),b⇩2⟩"
using InitBlockRedsFinal[OF _ fin,of _ _ "l⇩1(V:=l⇩0 V)" V]
Some reds s⇩1 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) e⇩2,s,b⟩ →* ⟨try e' catch(C V) e⇩2,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 ⊢ ⟨```