Theory Progress (Isabelle repository snapshot 408271602165 12-Mar-2013)

(*  Title:      Jinja/J/SmallProgress.thy

    Author:     Tobias Nipkow
    Copyright   2003 Technische Universitaet Muenchen
*)

header {* \isaheader{Progress of Small Step Semantics} *}

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

lemma final_addrE:
  "[| P,E,h \<turnstile> 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 \<turnstile> 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"
        ("_,_,_ \<turnstile> _ :' _"   [51,51,51]50)
  and WTrts2' :: "[J_prog,env,heap,expr list, ty list] => bool"
        ("_,_,_ \<turnstile> _ [:''] _" [51,51,51]50)
  for P :: J_prog and h :: heap
where
  "P,E,h \<turnstile> e :' T ≡ WTrt' P h E e T"
| "P,E,h \<turnstile> es [:'] Ts ≡ WTrts' P h E es Ts"

| "is_class P C  ==>  P,E,h \<turnstile> new C :' Class C"
| "[| P,E,h \<turnstile> e :' T; is_refT T; is_class P C |]
  ==> P,E,h \<turnstile> Cast C e :' Class C"
| "typeof⇘_h⇙ v = Some T ==> P,E,h \<turnstile> Val v :' T"
| "E v = Some T  ==>  P,E,h \<turnstile> Var v :' T"
| "[| P,E,h \<turnstile> e⇣₁ :' T⇣₁;  P,E,h \<turnstile> e⇣₂ :' T⇣₂ |]
  ==> P,E,h \<turnstile> e⇣₁ «Eq» e⇣₂ :' Boolean"
| "[| P,E,h \<turnstile> e⇣₁ :' Integer;  P,E,h \<turnstile> e⇣₂ :' Integer |]
  ==> P,E,h \<turnstile> e⇣₁ «Add» e⇣₂ :' Integer"
| "[| P,E,h \<turnstile> Var V :' T;  P,E,h \<turnstile> e :' T';  P \<turnstile> T' ≤ T (* V ≠ This*) |]
  ==> P,E,h \<turnstile> V:=e :' Void"
| "[| P,E,h \<turnstile> e :' Class C; P \<turnstile> C has F:T in D |] ==> P,E,h \<turnstile> e•F{D} :' T"
| "P,E,h \<turnstile> e :' NT ==> P,E,h \<turnstile> e•F{D} :' T"
| "[| P,E,h \<turnstile> e⇣₁ :' Class C;  P \<turnstile> C has F:T in D;
    P,E,h \<turnstile> e⇣₂ :' T⇣₂;  P \<turnstile> T⇣₂ ≤ T |]
  ==> P,E,h \<turnstile> e⇣₁•F{D}:=e⇣₂ :' Void"
| "[| P,E,h \<turnstile> e⇣₁:'NT; P,E,h \<turnstile> e⇣₂ :' T⇣₂ |] ==> P,E,h \<turnstile> e⇣₁•F{D}:=e⇣₂ :' Void"
| "[| P,E,h \<turnstile> e :' Class C; P \<turnstile> C sees M:Ts -> T = (pns,body) in D;
    P,E,h \<turnstile> es [:'] Ts'; P \<turnstile> Ts' [≤] Ts |]
  ==> P,E,h \<turnstile> e•M(es) :' T"
| "[| P,E,h \<turnstile> e :' NT; P,E,h \<turnstile> es [:'] Ts |] ==> P,E,h \<turnstile> e•M(es) :' T"
| "P,E,h \<turnstile> [] [:'] []"
| "[| P,E,h \<turnstile> e :' T;  P,E,h \<turnstile> es [:'] Ts |] ==>  P,E,h \<turnstile> e#es [:'] T#Ts"
| "[| typeof⇘_h⇙ v = Some T⇣₁; P \<turnstile> T⇣₁ ≤ T; P,E(V\<mapsto>T),h \<turnstile> e⇣₂ :' T⇣₂ |]
  ==>  P,E,h \<turnstile> {V:T := Val v; e⇣₂} :' T⇣₂"
| "[| P,E(V\<mapsto>T),h \<turnstile> e :' T'; ¬ assigned V e |] ==>  P,E,h \<turnstile> {V:T; e} :' T'"
| "[| P,E,h \<turnstile> e⇣₁:' T⇣₁;  P,E,h \<turnstile> e⇣₂:'T⇣₂ |]  ==>  P,E,h \<turnstile> e⇣₁;;e⇣₂ :' T⇣₂"
| "[| P,E,h \<turnstile> e :' Boolean;  P,E,h \<turnstile> e⇣₁:' T⇣₁;  P,E,h \<turnstile> e⇣₂:' T⇣₂;
    P \<turnstile> T⇣₁ ≤ T⇣₂ ∨ P \<turnstile> T⇣₂ ≤ T⇣₁;
    P \<turnstile> T⇣₁ ≤ T⇣₂ --> T = T⇣₂; P \<turnstile> T⇣₂ ≤ T⇣₁ --> T = T⇣₁ |]
  ==> P,E,h \<turnstile> if (e) e⇣₁ else e⇣₂ :' T"
(*
 "[| P,E,h \<turnstile> e :' Boolean;  P,E,h \<turnstile> e⇣₁:' T⇣₁;  P,E,h \<turnstile> e⇣₂:' T⇣₂; P \<turnstile> T⇣₁ ≤ T⇣₂ |]
  ==> P,E,h \<turnstile> if (e) e⇣₁ else e⇣₂ :' T⇣₂"
 "[| P,E,h \<turnstile> e :' Boolean;  P,E,h \<turnstile> e⇣₁:' T⇣₁;  P,E,h \<turnstile> e⇣₂:' T⇣₂; P \<turnstile> T⇣₂ ≤ T⇣₁ |]
  ==> P,E,h \<turnstile> if (e) e⇣₁ else e⇣₂ :' T⇣₁"
*)
| "[| P,E,h \<turnstile> e :' Boolean;  P,E,h \<turnstile> c:' T |]
  ==>  P,E,h \<turnstile> while(e) c :' Void"
| "[| P,E,h \<turnstile> e :' T⇣_r; is_refT T⇣_r |]  ==>  P,E,h \<turnstile> throw e :' T"
| "[| P,E,h \<turnstile> e⇣₁ :' T⇣₁;  P,E(V \<mapsto> Class C),h \<turnstile> e⇣₂ :' T⇣₂; P \<turnstile> T⇣₁ ≤ T⇣₂ |]
  ==> P,E,h \<turnstile> try e⇣₁ catch(C V) e⇣₂ :' T⇣₂"

(*<*)
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 \<turnstile> V :=e :' T"
(*>*)

lemma [iff]: "P,E,h \<turnstile> e⇣₁;;e⇣₂ :' T⇣₂ = (∃T⇣₁. P,E,h \<turnstile> e⇣₁:' T⇣₁ ∧ P,E,h \<turnstile> e⇣₂:' T⇣₂)"
(*<*)
apply(rule iffI)
apply (auto elim: WTrt'.cases intro!:WTrt'_WTrts'.intros)
done
(*>*)

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

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


lemma wt_wt': "P,E,h \<turnstile> e : T ==> P,E,h \<turnstile> e :' T"
and wts_wts': "P,E,h \<turnstile> es [:] Ts ==> P,E,h \<turnstile> es [:'] Ts"
(*<*)
apply (induct rule:WTrt_inducts)
prefer 14
apply(case_tac "assigned V e")
apply(clarsimp simp add:fun_upd_same assigned_def simp del:fun_upd_apply)
apply(erule (2) WTrt'_WTrts'.intros)
apply(erule (1) WTrt'_WTrts'.intros)
apply(blast intro:WTrt'_WTrts'.intros)+
done
(*>*)


lemma wt'_wt: "P,E,h \<turnstile> e :' T ==> P,E,h \<turnstile> e : T"
and wts'_wts: "P,E,h \<turnstile> es [:'] Ts ==> P,E,h \<turnstile> es [:] Ts"
(*<*)
apply (induct rule:WTrt'_inducts)
prefer 16
apply(rule WTrt_WTrts.intros)
apply(rule WTrt_WTrts.intros)
apply(rule WTrt_WTrts.intros)
apply simp
apply(erule (2) WTrt_WTrts.intros)
apply(blast intro:WTrt_WTrts.intros)+
done
(*>*)


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


corollary wts'_iff_wts: "(P,E,h \<turnstile> es [:'] Ts) = (P,E,h \<turnstile> 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 \<turnstile> h \<surd>"
shows progress: "P,E,h \<turnstile> e : T ==>
 (!!l. [| \<D> e ⌊dom l⌋; ¬ final e |] ==> ∃e' s'. P \<turnstile> ⟨e,(h,l)⟩ -> ⟨e',s'⟩)"
and "P,E,h \<turnstile> es [:] Ts ==>
 (!!l. [| \<D>s es ⌊dom l⌋; ¬ finals es |] ==> ∃es' s'. P \<turnstile> ⟨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 \<turnstile> e : T" and ref: "is_refT T"
   and IH: "!!l. [|\<D> e ⌊dom l⌋; ¬ final e|]
                ==> ∃e' s'. P \<turnstile> ⟨e,(h,l)⟩ -> ⟨e',s'⟩"
   and D: "\<D> (Cast C e) ⌊dom l⌋" by fact+
  from D have De: "\<D> 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 \<turnstile> D \<preceq>⇧^* C"
        thus ?thesis using A wte by(fastforce intro:RedCast)
      next
        assume "¬ P \<turnstile> D \<preceq>⇧^* 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 \<turnstile> e : Class C"
   and field: "P \<turnstile> 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 \<turnstile> (C,fs) \<surd>" 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 \<turnstile> 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⇣₁ e⇣₂ T⇣₂ F D)
  show ?case
  proof cases
    assume e1: "final e⇣₁"  --"@{term e⇣₁} is @{term null} or @{term throw}"
    show ?thesis
    proof cases
      assume "final e⇣₂"  --"@{term e⇣₂} 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⇣₂" --"@{term e⇣₂} 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⇣₁" --"@{term e⇣₁} 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 \<turnstile> e : Class C"
   and method: "P \<turnstile> C sees M:Ts->T = (pns,body) in D"
   and wtes: "P,E,h \<turnstile> es [:] Ts'"and sub: "P \<turnstile> Ts' [≤] Ts"
   and IHes: "!!l.
             [|\<D>s es ⌊dom l⌋; ¬ finals es|]
             ==> ∃es' s'. P \<turnstile> ⟨es,(h,l)⟩ [->] ⟨es',s'⟩"
   and D: "\<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_def 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. [|\<D> e ⌊dom l⌋; ¬ final e|]
                ==> ∃e' s'. P \<turnstile> ⟨e,(h,l)⟩ -> ⟨e',s'⟩"
   and IHes: "!!l. [|\<D>s es ⌊dom l⌋; ¬ finals es|]
             ==> ∃es' s'. P \<turnstile> ⟨es,(h,l)⟩ [->] ⟨es',s'⟩"
   and D: "\<D>s (e#es) ⌊dom l⌋" and not_fins: "¬ finals(e # es)" by fact+
  have De: "\<D> e ⌊dom l⌋" and Des: "\<D>s es (⌊dom l⌋ \<squnion> \<A> 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': "\<D>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⇣₁ T E V e⇣₂ T⇣₂)
  have IH2: "!!l. [|\<D> e⇣₂ ⌊dom l⌋; ¬ final e⇣₂|]
                  ==> ∃e' s'. P \<turnstile> ⟨e⇣₂,(h,l)⟩ -> ⟨e',s'⟩"
   and D: "\<D> {V:T := Val v; e⇣₂} ⌊dom l⌋" by fact+
  show ?case
  proof cases
    assume "final e⇣₂"
    then show ?thesis
    proof (rule finalE)
      fix v⇣₂ assume "e⇣₂ = Val v⇣₂"
      thus ?thesis by(fast intro:RedInitBlock)
    next
      fix a assume "e⇣₂ = Throw a"
      thus ?thesis by(fast intro:red_reds.InitBlockThrow)
    qed
  next
    assume not_fin2: "¬ final e⇣₂"
    from D have D2: "\<D> e⇣₂ ⌊dom(l(V\<mapsto>v))⌋" by (auto simp:hyperset_defs)
    from IH2[OF D2 not_fin2]
    obtain h' l' e' where red2: "P \<turnstile> ⟨e⇣₂,(h, l(V\<mapsto>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. [|\<D> e ⌊dom l⌋; ¬ final e|]
                 ==> ∃e' s'. P \<turnstile> ⟨e,(h,l)⟩ -> ⟨e',s'⟩"
   and unass: "¬ assigned V e" and D: "\<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: "\<D> e ⌊dom(l(V:=None))⌋" by(simp add:hyperset_defs)
    from IH[OF De not_fin]
    obtain h' l' e' where red: "P \<turnstile> ⟨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⇣₁ T⇣₁ e⇣₂ T⇣₂ T)
  have wt: "P,E,h \<turnstile> 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 \<turnstile> 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 \<turnstile> D \<preceq>⇧^* C"
        with e1_Throw ha show ?thesis by(fastforce intro!:RedTryCatch)
      next
        assume "¬ P \<turnstile> D \<preceq>⇧^* 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