# Theory Progress

```(*  Title:      Jinja/J/SmallProgress.thy

Author:     Tobias Nipkow
*)

section ‹Progress of Small Step Semantics›

theory Progress
imports Equivalence WellTypeRT DefAss "../Common/Conform"
begin

"⟦ P,E,h ⊢ e : Class C; final e;
⋀a. e = addr a ⟹ R;
⋀a. e = Throw a ⟹ R ⟧ ⟹ R"
(*<*)by(auto simp:final_def)(*>*)

lemma finalRefE:
"⟦ P,E,h ⊢ e : T; is_refT T; final e;
e = null ⟹ R;
⋀a C. ⟦ e = addr a; T = Class C ⟧ ⟹ R;
⋀a. e = Throw a ⟹ R ⟧ ⟹ R"
(*<*)by(auto simp:final_def is_refT_def)(*>*)

text‹Derivation of new induction scheme for well typing:›

inductive
WTrt' :: "[J_prog,heap,env,expr,ty] ⇒ bool"
and WTrts' :: "[J_prog,heap,env,expr list, ty list] ⇒ bool"
and WTrt2' :: "[J_prog,env,heap,expr,ty] ⇒ bool"
("_,_,_ ⊢ _ :'' _"   [51,51,51]50)
and WTrts2' :: "[J_prog,env,heap,expr list, ty list] ⇒ bool"
("_,_,_ ⊢ _ [:''] _" [51,51,51]50)
for P :: J_prog and h :: heap
where
"P,E,h ⊢ e :' T ≡ WTrt' P h E e T"
| "P,E,h ⊢ es [:'] Ts ≡ WTrts' P h E es Ts"

| "is_class P C  ⟹  P,E,h ⊢ new C :' Class C"
| "⟦ P,E,h ⊢ e :' T; is_refT T; is_class P C ⟧
⟹ P,E,h ⊢ Cast C e :' Class C"
| "typeof⇘h⇙ v = Some T ⟹ P,E,h ⊢ Val v :' T"
| "E v = Some T  ⟹  P,E,h ⊢ Var v :' T"
| "⟦ P,E,h ⊢ e⇩1 :' T⇩1;  P,E,h ⊢ e⇩2 :' T⇩2 ⟧
⟹ P,E,h ⊢ e⇩1 «Eq» e⇩2 :' Boolean"
| "⟦ P,E,h ⊢ e⇩1 :' Integer;  P,E,h ⊢ e⇩2 :' Integer ⟧
⟹ P,E,h ⊢ e⇩1 «Add» e⇩2 :' Integer"
| "⟦ P,E,h ⊢ Var V :' T;  P,E,h ⊢ e :' T';  P ⊢ T' ≤ T ⌦‹V ≠ This› ⟧
⟹ P,E,h ⊢ V:=e :' Void"
| "⟦ P,E,h ⊢ e :' Class C; P ⊢ C has F:T in D ⟧ ⟹ P,E,h ⊢ e∙F{D} :' T"
| "P,E,h ⊢ e :' NT ⟹ P,E,h ⊢ e∙F{D} :' T"
| "⟦ P,E,h ⊢ e⇩1 :' Class C;  P ⊢ C has F:T in D;
P,E,h ⊢ e⇩2 :' T⇩2;  P ⊢ T⇩2 ≤ T ⟧
⟹ P,E,h ⊢ e⇩1∙F{D}:=e⇩2 :' Void"
| "⟦ P,E,h ⊢ e⇩1:'NT; P,E,h ⊢ e⇩2 :' T⇩2 ⟧ ⟹ P,E,h ⊢ e⇩1∙F{D}:=e⇩2 :' Void"
| "⟦ P,E,h ⊢ e :' Class C; P ⊢ C sees M:Ts → T = (pns,body) in D;
P,E,h ⊢ es [:'] Ts'; P ⊢ Ts' [≤] Ts ⟧
⟹ P,E,h ⊢ e∙M(es) :' T"
| "⟦ P,E,h ⊢ e :' NT; P,E,h ⊢ es [:'] Ts ⟧ ⟹ P,E,h ⊢ e∙M(es) :' T"
| "P,E,h ⊢ [] [:'] []"
| "⟦ P,E,h ⊢ e :' T;  P,E,h ⊢ es [:'] Ts ⟧ ⟹  P,E,h ⊢ e#es [:'] T#Ts"
| "⟦ typeof⇘h⇙ v = Some T⇩1; P ⊢ T⇩1 ≤ T; P,E(V↦T),h ⊢ e⇩2 :' T⇩2 ⟧
⟹  P,E,h ⊢ {V:T := Val v; e⇩2} :' T⇩2"
| "⟦ P,E(V↦T),h ⊢ e :' T'; ¬ assigned V e ⟧ ⟹  P,E,h ⊢ {V:T; e} :' T'"
| "⟦ P,E,h ⊢ e⇩1:' T⇩1;  P,E,h ⊢ e⇩2:'T⇩2 ⟧  ⟹  P,E,h ⊢ e⇩1;;e⇩2 :' T⇩2"
| "⟦ P,E,h ⊢ e :' Boolean;  P,E,h ⊢ e⇩1:' T⇩1;  P,E,h ⊢ e⇩2:' T⇩2;
P ⊢ T⇩1 ≤ T⇩2 ∨ P ⊢ T⇩2 ≤ T⇩1;
P ⊢ T⇩1 ≤ T⇩2 ⟶ T = T⇩2; P ⊢ T⇩2 ≤ T⇩1 ⟶ T = T⇩1 ⟧
⟹ P,E,h ⊢ if (e) e⇩1 else e⇩2 :' T"
(*
"⟦ P,E,h ⊢ e :' Boolean;  P,E,h ⊢ e⇩1:' T⇩1;  P,E,h ⊢ e⇩2:' T⇩2; P ⊢ T⇩1 ≤ T⇩2 ⟧
⟹ P,E,h ⊢ if (e) e⇩1 else e⇩2 :' T⇩2"
"⟦ P,E,h ⊢ e :' Boolean;  P,E,h ⊢ e⇩1:' T⇩1;  P,E,h ⊢ e⇩2:' T⇩2; P ⊢ T⇩2 ≤ T⇩1 ⟧
⟹ P,E,h ⊢ if (e) e⇩1 else e⇩2 :' T⇩1"
*)
| "⟦ P,E,h ⊢ e :' Boolean;  P,E,h ⊢ c:' T ⟧
⟹  P,E,h ⊢ while(e) c :' Void"
| "⟦ P,E,h ⊢ e :' T⇩r; is_refT T⇩r ⟧  ⟹  P,E,h ⊢ throw e :' T"
| "⟦ P,E,h ⊢ e⇩1 :' T⇩1;  P,E(V ↦ Class C),h ⊢ e⇩2 :' T⇩2; P ⊢ T⇩1 ≤ T⇩2 ⟧
⟹ P,E,h ⊢ try e⇩1 catch(C V) e⇩2 :' T⇩2"

(*<*)
lemmas WTrt'_induct = WTrt'_WTrts'.induct [split_format (complete)]
and WTrt'_inducts = WTrt'_WTrts'.inducts [split_format (complete)]

inductive_cases WTrt'_elim_cases[elim!]:
"P,E,h ⊢ V :=e :' T"
(*>*)

lemma [iff]: "P,E,h ⊢ e⇩1;;e⇩2 :' T⇩2 = (∃T⇩1. P,E,h ⊢ e⇩1:' T⇩1 ∧ P,E,h ⊢ e⇩2:' T⇩2)"
(*<*)by(rule iffI) (auto elim: WTrt'.cases intro!:WTrt'_WTrts'.intros)(*>*)

lemma [iff]: "P,E,h ⊢ Val v :' T = (typeof⇘h⇙ v = Some T)"
(*<*)by(rule iffI) (auto elim: WTrt'.cases intro!:WTrt'_WTrts'.intros)(*>*)

lemma [iff]: "P,E,h ⊢ Var v :' T = (E v = Some T)"
(*<*)by(rule iffI) (auto elim: WTrt'.cases intro!:WTrt'_WTrts'.intros)(*>*)

lemma wt_wt': "P,E,h ⊢ e : T ⟹ P,E,h ⊢ e :' T"
and wts_wts': "P,E,h ⊢ es [:] Ts ⟹ P,E,h ⊢ es [:'] Ts"
(*<*)
proof(induct rule:WTrt_inducts)
case (WTrtBlock E V T e T')
then show ?case
proof(cases "assigned V e")
case True then show ?thesis using WTrtBlock.hyps(2)
simp del:fun_upd_apply)
next
case False then show ?thesis
qed
qed (blast intro:WTrt'_WTrts'.intros)+
(*>*)

lemma wt'_wt: "P,E,h ⊢ e :' T ⟹ P,E,h ⊢ e : T"
and wts'_wts: "P,E,h ⊢ es [:'] Ts ⟹ P,E,h ⊢ es [:] Ts"
(*<*)
proof(induct rule:WTrt'_inducts)
case Block: (16 v T⇩1 T E V e⇩2 T⇩2)
let ?E = "E(V ↦ T)"
have "P,?E,h ⊢ Val v : T⇩1" using Block.hyps(1) by simp
moreover have "P ⊢ T⇩1 ≤ T" by(rule Block.hyps(2))
ultimately have "P,?E,h ⊢ V:=Val v : Void" using WTrtLAss by simp
moreover have "P,?E,h ⊢ e⇩2 : T⇩2" by(rule Block.hyps(4))
ultimately have "P,?E,h ⊢ V:=Val v;; e⇩2 : T⇩2" by blast
then show ?case by simp
qed (blast intro:WTrt_WTrts.intros)+
(*>*)

corollary wt'_iff_wt: "(P,E,h ⊢ e :' T) = (P,E,h ⊢ e : T)"
(*<*)by(blast intro:wt_wt' wt'_wt)(*>*)

corollary wts'_iff_wts: "(P,E,h ⊢ es [:'] Ts) = (P,E,h ⊢ es [:] Ts)"
(*<*)by(blast intro:wts_wts' wts'_wts)(*>*)

(*<*)
lemmas WTrt_inducts2 = WTrt'_inducts [unfolded wt'_iff_wt wts'_iff_wts,
case_names WTrtNew WTrtCast WTrtVal WTrtVar WTrtBinOpEq WTrtBinOpAdd WTrtLAss WTrtFAcc WTrtFAccNT WTrtFAss
WTrtFAssNT WTrtCall WTrtCallNT WTrtNil WTrtCons WTrtInitBlock WTrtBlock WTrtSeq WTrtCond
WTrtWhile WTrtThrow WTrtTry, consumes 1]
(*>*)

theorem assumes wf: "wwf_J_prog P" and hconf: "P ⊢ h √"
shows progress: "P,E,h ⊢ e : T ⟹
(⋀l. ⟦ 𝒟 e ⌊dom l⌋; ¬ final e ⟧ ⟹ ∃e' s'. P ⊢ ⟨e,(h,l)⟩ → ⟨e',s'⟩)"
and "P,E,h ⊢ es [:] Ts ⟹
(⋀l. ⟦ 𝒟s es ⌊dom l⌋; ¬ finals es ⟧ ⟹ ∃es' s'. P ⊢ ⟨es,(h,l)⟩ [→] ⟨es',s'⟩)"
(*<*)
proof (induct rule:WTrt_inducts2)
case WTrtNew
show ?case
proof cases
assume "∃a. h a = None"
with assms WTrtNew show ?thesis
elim!:wf_Fields_Ex[THEN exE])
next
assume "¬(∃a. h a = None)"
with assms WTrtNew show ?thesis
qed
next
case (WTrtCast E e T C)
have wte: "P,E,h ⊢ e : T" and ref: "is_refT T"
and IH: "⋀l. ⟦𝒟 e ⌊dom l⌋; ¬ final e⟧
⟹ ∃e' s'. P ⊢ ⟨e,(h,l)⟩ → ⟨e',s'⟩"
and D: "𝒟 (Cast C e) ⌊dom l⌋" by fact+
from D have De: "𝒟 e ⌊dom l⌋" by auto
show ?case
proof cases
assume "final e"
with wte ref show ?thesis
proof (rule finalRefE)
assume "e = null" thus ?case by(fastforce intro:RedCastNull)
next
fix D a assume A: "T = Class D" "e = addr a"
show ?thesis
proof cases
assume "P ⊢ D ≼⇧* C"
thus ?thesis using A wte by(fastforce intro:RedCast)
next
assume "¬ P ⊢ D ≼⇧* C"
thus ?thesis using A wte by(force intro!:RedCastFail)
qed
next
fix a assume "e = Throw a"
thus ?thesis by(blast intro!:red_reds.CastThrow)
qed
next
assume nf: "¬ final e"
from IH[OF De nf] show ?thesis by (blast intro:CastRed)
qed
next
case WTrtVal thus ?case by(simp add:final_def)
next
case WTrtVar thus ?case by(fastforce intro:RedVar simp:hyper_isin_def)
next
case (WTrtBinOpEq E e1 T1 e2 T2)
show ?case
proof cases
assume "final e1"
thus ?thesis
proof (rule finalE)
fix v1 assume [simp]: "e1 = Val v1"
show ?thesis
proof cases
assume "final e2"
thus ?thesis
proof (rule finalE)
fix v2 assume "e2 = Val v2"
thus ?thesis using WTrtBinOpEq by(fastforce intro:RedBinOp)
next
fix a assume "e2 = Throw a"
thus ?thesis by(auto intro:red_reds.BinOpThrow2)
qed
next
assume "¬ final e2" with WTrtBinOpEq show ?thesis
by simp (fast intro!:BinOpRed2)
qed
next
fix a assume "e1 = Throw a"
thus ?thesis by simp (fast intro:red_reds.BinOpThrow1)
qed
next
assume "¬ final e1" with WTrtBinOpEq show ?thesis
by simp (fast intro:BinOpRed1)
qed
next
show ?case
proof cases
assume "final e1"
thus ?thesis
proof (rule finalE)
fix v1 assume [simp]: "e1 = Val v1"
show ?thesis
proof cases
assume "final e2"
thus ?thesis
proof (rule finalE)
fix v2 assume "e2 = Val v2"
thus ?thesis using WTrtBinOpAdd by(fastforce intro:RedBinOp)
next
fix a assume "e2 = Throw a"
thus ?thesis by(auto intro:red_reds.BinOpThrow2)
qed
next
assume "¬ final e2" with WTrtBinOpAdd show ?thesis
by simp (fast intro!:BinOpRed2)
qed
next
fix a assume "e1 = Throw a"
thus ?thesis by simp (fast intro:red_reds.BinOpThrow1)
qed
next
assume "¬ final e1" with WTrtBinOpAdd show ?thesis
by simp (fast intro:BinOpRed1)
qed
next
case (WTrtLAss E V T e T')
show ?case
proof cases
assume "final e" with WTrtLAss show ?thesis
by(auto simp:final_def intro!:RedLAss red_reds.LAssThrow)
next
assume "¬ final e" with WTrtLAss show ?thesis
by simp (fast intro:LAssRed)
qed
next
case (WTrtFAcc E e C F T D)
have wte: "P,E,h ⊢ e : Class C"
and field: "P ⊢ C has F:T in D" by fact+
show ?case
proof cases
assume "final e"
with wte show ?thesis
fix a assume e: "e = addr a"
with wte obtain fs where hp: "h a = Some(C,fs)" by auto
with hconf have "P,h ⊢ (C,fs) √" using hconf_def by fastforce
then obtain v where "fs(F,D) = Some v" using field
by(fastforce dest:has_fields_fun simp:oconf_def has_field_def)
with hp e show ?thesis by(fastforce intro:RedFAcc)
next
fix a assume "e = Throw a"
thus ?thesis by(fastforce intro:red_reds.FAccThrow)
qed
next
assume "¬ final e" with WTrtFAcc show ?thesis
by(fastforce intro!:FAccRed)
qed
next
case (WTrtFAccNT E e F D T)
show ?case
proof cases
assume "final e"  ― ‹@{term e} is @{term null} or @{term throw}›
with WTrtFAccNT show ?thesis
by(fastforce simp:final_def intro: RedFAccNull red_reds.FAccThrow)
next
assume "¬ final e" ― ‹@{term e} reduces by IH›
with WTrtFAccNT show ?thesis by simp (fast intro:FAccRed)
qed
next
case (WTrtFAss E e1 C F T D e2 T2)
have wte1: "P,E,h ⊢ e1 : Class C" by fact
show ?case
proof cases
assume "final e1"
with wte1 show ?thesis
fix a assume e1: "e1 = addr a"
show ?thesis
proof cases
assume "final e2"
thus ?thesis
proof (rule finalE)
fix v assume "e2 = Val v"
thus ?thesis using e1 wte1 by(fastforce intro:RedFAss)
next
fix a assume "e2 = Throw a"
thus ?thesis using e1 by(fastforce intro:red_reds.FAssThrow2)
qed
next
assume "¬ final e2" with WTrtFAss e1 show ?thesis
by simp (fast intro!:FAssRed2)
qed
next
fix a assume "e1 = Throw a"
thus ?thesis by(fastforce intro:red_reds.FAssThrow1)
qed
next
assume "¬ final e1" with WTrtFAss show ?thesis
by simp (blast intro!:FAssRed1)
qed
next
case (WTrtFAssNT E e⇩1 e⇩2 T⇩2 F D)
show ?case
proof cases
assume e1: "final e⇩1"  ― ‹@{term e⇩1} is @{term null} or @{term throw}›
show ?thesis
proof cases
assume "final e⇩2"  ― ‹@{term e⇩2} is @{term Val} or @{term throw}›
with WTrtFAssNT e1 show ?thesis
by(fastforce simp:final_def intro: RedFAssNull red_reds.FAssThrow1 red_reds.FAssThrow2)
next
assume "¬ final e⇩2" ― ‹@{term e⇩2} reduces by IH›
with WTrtFAssNT e1 show ?thesis
by (fastforce  simp:final_def intro!:red_reds.FAssRed2 red_reds.FAssThrow1)
qed
next
assume "¬ final e⇩1" ― ‹@{term e⇩1} reduces by IH›
with WTrtFAssNT show ?thesis by (fastforce intro:FAssRed1)
qed
next
case (WTrtCall E e C M Ts T pns body D es Ts')
have wte: "P,E,h ⊢ e : Class C"
and "method": "P ⊢ C sees M:Ts→T = (pns,body) in D"
and wtes: "P,E,h ⊢ es [:] Ts'"and sub: "P ⊢ Ts' [≤] Ts"
and IHes: "⋀l.
⟦𝒟s es ⌊dom l⌋; ¬ finals es⟧
⟹ ∃es' s'. P ⊢ ⟨es,(h,l)⟩ [→] ⟨es',s'⟩"
and D: "𝒟 (e∙M(es)) ⌊dom l⌋" by fact+
show ?case
proof cases
assume "final e"
with wte show ?thesis
show ?thesis
proof cases
assume es: "∃vs. es = map Val vs"
from wte e_addr obtain fs where ha: "h a = Some(C,fs)" by auto
show ?thesis
using e_addr ha "method" WTrts_same_length[OF wtes] sub es sees_wf_mdecl[OF wf "method"]
by (fastforce intro!: RedCall simp:list_all2_iff wf_mdecl_def)
next
assume "¬(∃vs. es = map Val vs)"
hence not_all_Val: "¬(∀e ∈ set es. ∃v. e = Val v)"
let ?ves = "takeWhile (λe. ∃v. e = Val v) es"
let ?rest = "dropWhile (λe. ∃v. e = Val v) es"
let ?ex = "hd ?rest" let ?rst = "tl ?rest"
from not_all_Val have nonempty: "?rest ≠ []" by auto
hence es: "es = ?ves @ ?ex # ?rst" by simp
have "∀e ∈ set ?ves. ∃v. e = Val v" by(fastforce dest:set_takeWhileD)
then obtain vs where ves: "?ves = map Val vs"
using ex_map_conv by blast
show ?thesis
proof cases
assume "final ?ex"
moreover from nonempty have "¬(∃v. ?ex = Val v)"
by(auto simp:neq_Nil_conv simp del:dropWhile_eq_Nil_conv)
ultimately obtain b where ex_Throw: "?ex = Throw b"
by(fast elim!:finalE)
show ?thesis using e_addr es ex_Throw ves
by(fastforce intro:CallThrowParams)
next
assume not_fin: "¬ final ?ex"
have "finals es = finals(?ves @ ?ex # ?rst)" using es
by(rule arg_cong)
also have "… = finals(?ex # ?rst)" using ves by simp
finally have "finals es = finals(?ex # ?rst)" .
hence "¬ finals es" using not_finals_ConsI[OF not_fin] by blast
thus ?thesis using e_addr D IHes  by(fastforce intro!:CallParams)
qed
qed
next
fix a assume "e = Throw a"
with WTrtCall.prems show ?thesis by(fast intro!:CallThrowObj)
qed
next
assume "¬ final e"
with WTrtCall show ?thesis by simp (blast intro!:CallObj)
qed
next
case (WTrtCallNT E e es Ts M T)
show ?case
proof cases
assume "final e"
moreover
{ fix v assume e: "e = Val v"
hence "e = null" using WTrtCallNT by simp
have ?case
proof cases
assume "finals es"
moreover
{ fix vs assume "es = map Val vs"
with WTrtCallNT e have ?thesis by(fastforce intro: RedCallNull) }
moreover
{ fix vs a es' assume "es = map Val vs @ Throw a # es'"
with WTrtCallNT e have ?thesis by(fastforce intro: CallThrowParams) }
ultimately show ?thesis by(fastforce simp:finals_def)
next
assume "¬ finals es" ― ‹@{term es} reduces by IH›
with WTrtCallNT e show ?thesis by(fastforce intro: CallParams)
qed
}
moreover
{ fix a assume "e = Throw a"
with WTrtCallNT have ?case by(fastforce intro: CallThrowObj) }
ultimately show ?thesis by(fastforce simp:final_def)
next
assume "¬ final e" ― ‹@{term e} reduces by IH›
with WTrtCallNT show ?thesis by (fastforce intro:CallObj)
qed
next
case WTrtNil thus ?case by simp
next
case (WTrtCons E e T es Ts)
have IHe: "⋀l. ⟦𝒟 e ⌊dom l⌋; ¬ final e⟧
⟹ ∃e' s'. P ⊢ ⟨e,(h,l)⟩ → ⟨e',s'⟩"
and IHes: "⋀l. ⟦𝒟s es ⌊dom l⌋; ¬ finals es⟧
⟹ ∃es' s'. P ⊢ ⟨es,(h,l)⟩ [→] ⟨es',s'⟩"
and D: "𝒟s (e#es) ⌊dom l⌋" and not_fins: "¬ finals(e # es)" by fact+
have De: "𝒟 e ⌊dom l⌋" and Des: "𝒟s es (⌊dom l⌋ ⊔ 𝒜 e)"
using D by auto
show ?case
proof cases
assume "final e"
thus ?thesis
proof (rule finalE)
fix v assume e: "e = Val v"
hence Des': "𝒟s es ⌊dom l⌋" using De Des by auto
have not_fins_tl: "¬ finals es" using not_fins e by simp
show ?thesis using e IHes[OF Des' not_fins_tl]
by (blast intro!:ListRed2)
next
fix a assume "e = Throw a"
hence False using not_fins by simp
thus ?thesis ..
qed
next
assume "¬ final e"
with IHe[OF De] show ?thesis by(fast intro!:ListRed1)
qed
next
case (WTrtInitBlock v T⇩1 T E V e⇩2 T⇩2)
have IH2: "⋀l. ⟦𝒟 e⇩2 ⌊dom l⌋; ¬ final e⇩2⟧
⟹ ∃e' s'. P ⊢ ⟨e⇩2,(h,l)⟩ → ⟨e',s'⟩"
and D: "𝒟 {V:T := Val v; e⇩2} ⌊dom l⌋" by fact+
show ?case
proof cases
assume "final e⇩2"
then show ?thesis
proof (rule finalE)
fix v⇩2 assume "e⇩2 = Val v⇩2"
thus ?thesis by(fast intro:RedInitBlock)
next
fix a assume "e⇩2 = Throw a"
thus ?thesis by(fast intro:red_reds.InitBlockThrow)
qed
next
assume not_fin2: "¬ final e⇩2"
from D have D2: "𝒟 e⇩2 ⌊dom(l(V↦v))⌋" by (auto simp:hyperset_defs)
from IH2[OF D2 not_fin2]
obtain h' l' e' where red2: "P ⊢ ⟨e⇩2,(h, l(V↦v))⟩ → ⟨e',(h', l')⟩"
by auto
from red_lcl_incr[OF red2] have "V ∈ dom l'" by auto
with red2 show ?thesis by(fastforce intro:InitBlockRed)
qed
next
case (WTrtBlock E V T e T')
have IH: "⋀l. ⟦𝒟 e ⌊dom l⌋; ¬ final e⟧
⟹ ∃e' s'. P ⊢ ⟨e,(h,l)⟩ → ⟨e',s'⟩"
and unass: "¬ assigned V e" and D: "𝒟 {V:T; e} ⌊dom l⌋" by fact+
show ?case
proof cases
assume "final e"
thus ?thesis
proof (rule finalE)
fix v assume "e = Val v" thus ?thesis by(fast intro:RedBlock)
next
fix a assume "e = Throw a"
thus ?thesis by(fast intro:red_reds.BlockThrow)
qed
next
assume not_fin: "¬ final e"
from D have De: "𝒟 e ⌊dom(l(V:=None))⌋" by(simp add:hyperset_defs)
from IH[OF De not_fin]
obtain h' l' e' where red: "P ⊢ ⟨e,(h,l(V:=None))⟩ → ⟨e',(h',l')⟩"
by auto
show ?thesis
proof (cases "l' V")
assume "l' V = None"
with red unass show ?thesis by(blast intro: BlockRedNone)
next
fix v assume "l' V = Some v"
with red unass show ?thesis by(blast intro: BlockRedSome)
qed
qed
next
case (WTrtSeq E e1 T1 e2 T2)
show ?case
proof cases
assume "final e1"
thus ?thesis
by(fast elim:finalE intro:RedSeq red_reds.SeqThrow)
next
assume "¬ final e1" with WTrtSeq show ?thesis
by simp (blast intro:SeqRed)
qed
next
case (WTrtCond E e e⇩1 T⇩1 e⇩2 T⇩2 T)
have wt: "P,E,h ⊢ e : Boolean" by fact
show ?case
proof cases
assume "final e"
thus ?thesis
proof (rule finalE)
fix v assume val: "e = Val v"
then obtain b where v: "v = Bool b" using wt by auto
show ?thesis
proof (cases b)
case True with val v show ?thesis by(auto intro:RedCondT)
next
case False with val v show ?thesis by(auto intro:RedCondF)
qed
next
fix a assume "e = Throw a"
thus ?thesis by(fast intro:red_reds.CondThrow)
qed
next
assume "¬ final e" with WTrtCond show ?thesis
by simp (fast intro:CondRed)
qed
next
case WTrtWhile show ?case by(fast intro:RedWhile)
next
case (WTrtThrow E e T⇩r T)
show ?case
proof cases
assume "final e" ― ‹Then @{term e} must be @{term throw} or @{term null}›
with WTrtThrow show ?thesis
by(fastforce simp:final_def is_refT_def
intro:red_reds.ThrowThrow red_reds.RedThrowNull)
next
assume "¬ final e" ― ‹Then @{term e} must reduce›
with WTrtThrow show ?thesis by simp (blast intro:ThrowRed)
qed
next
case (WTrtTry E e1 T1 V C e2 T2)
have wt1: "P,E,h ⊢ e1 : T1" by fact
show ?case
proof cases
assume "final e1"
thus ?thesis
proof (rule finalE)
fix v assume "e1 = Val v"
thus ?thesis by(fast intro:RedTry)
next
fix a assume e1_Throw: "e1 = Throw a"
with wt1 obtain D fs where ha: "h a = Some(D,fs)" by fastforce
show ?thesis
proof cases
assume "P ⊢ D ≼⇧* C"
with e1_Throw ha show ?thesis by(fastforce intro!:RedTryCatch)
next
assume "¬ P ⊢ D ≼⇧* C"
with e1_Throw ha show ?thesis by(force intro!:RedTryFail)
qed
qed
next
assume "¬ final e1"
with WTrtTry show ?thesis by simp (fast intro:TryRed)
qed
qed
(*>*)

end
```