(* Title: Jinja/J/SmallProgress.thy Author: Tobias Nipkow Copyright 2003 Technische Universitaet Muenchen *) section ‹Progress of Small Step Semantics› theory Progress imports Equivalence WellTypeRT DefAss "../Common/Conform" begin lemma final_addrE: "⟦ 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) by(clarsimp simp add:fun_upd_same assigned_def WTrt'_WTrts'.intros simp del:fun_upd_apply) next case False then show ?thesis by (simp add: WTrtBlock.hyps(2) WTrt'_WTrts'.intros) 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 by (fastforce del:exE intro!:RedNew simp add:new_Addr_def elim!:wf_Fields_Ex[THEN exE]) next assume "¬(∃a. h a = None)" with assms WTrtNew show ?thesis by(fastforce intro:RedNewFail simp add:new_Addr_def) 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 case (WTrtBinOpAdd E e1 e2) 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 proof (rule final_addrE) 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 proof (rule final_addrE) 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 proof (rule final_addrE) fix a assume e_addr: "e = addr a" 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)" by(simp add:ex_map_conv) 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) (simp add:dropWhile_eq_Cons_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