Theory SmallStep

(*  Title:      JinjaDCI/J/SmallStep.thy
    Author:     Tobias Nipkow, Susannah Mansky
    Copyright   2003 Technische Universitaet Muenchen, 2019-20 UIUC

    Based on the Jinja theory J/SmallStep.thy by Tobias Nipkow
*)

section ‹ Small Step Semantics ›

theory SmallStep
imports Expr State WWellForm
begin

fun blocks :: "vname list * ty list * val list * expr ⇒ expr"
where
 "blocks(V#Vs, T#Ts, v#vs, e) = {V:T := Val v; blocks(Vs,Ts,vs,e)}"
|"blocks([],[],[],e) = e"

lemmas blocks_induct = blocks.induct[split_format (complete)]

lemma [simp]:
  "⟦ size vs = size Vs; size Ts = size Vs ⟧ ⟹ fv(blocks(Vs,Ts,vs,e)) = fv e - set Vs"
(*<*)
by (induct rule:blocks_induct) auto
(*>*)


lemma sub_RI_blocks_body[iff]: "length vs = length pns ⟹ length Ts = length pns
 ⟹ sub_RI (blocks (pns, Ts, vs, body)) ⟷ sub_RI body"
proof(induct pns arbitrary: Ts vs)
  case Nil then show ?case by simp
next
  case Cons then show ?case by(cases vs; cases Ts) auto
qed


definition assigned :: "'a ⇒ 'a exp ⇒ bool"
where
  "assigned V e  ≡  ∃v e'. e = (V := Val v;; e')"

― ‹ expression is okay to go the right side of @{text INIT} or @{text "RI ←"}
 or to have indicator Boolean be True (in latter case, given that class is
 also verified initialized) ›
fun icheck :: "'m prog ⇒ cname ⇒ 'a exp ⇒ bool" where
"icheck P C' (new C) = (C' = C)" |
"icheck P D' (C∙⇩sF{D}) = ((D' = D) ∧ (∃T. P ⊢ C has F,Static:T in D))" |
"icheck P D' (C∙⇩sF{D}:=(Val v)) = ((D' = D) ∧ (∃T. P ⊢ C has F,Static:T in D))" |
"icheck P D (C∙⇩sM(es)) = ((∃vs. es = map Val vs) ∧ (∃Ts T m. P ⊢ C sees M,Static:Ts→T = m in D))" |
"icheck P _ _ = False"

lemma nicheck_SFAss_nonVal: "val_of e⇩2 = None ⟹ ¬icheck P C' (C∙⇩sF{D} := (e⇩2::'a exp))"
 by(rule notI, cases e⇩2, auto)

inductive_set
  red  :: "J_prog ⇒ ((expr × state × bool) × (expr × state × bool)) set"
  and reds  :: "J_prog ⇒ ((expr list × state × bool) × (expr list × state × bool)) set"
  and red' :: "J_prog ⇒ expr ⇒ state ⇒ bool ⇒ expr ⇒ state ⇒ bool ⇒ bool"
          (‹_ ⊢ ((1⟨_,/_,/_⟩) →/ (1⟨_,/_,/_⟩))› [51,0,0,0,0,0,0] 81)
  and reds' :: "J_prog ⇒ expr list ⇒ state ⇒ bool ⇒ expr list ⇒ state ⇒ bool ⇒ bool"
          (‹_ ⊢ ((1⟨_,/_,/_⟩) [→]/ (1⟨_,/_,/_⟩))› [51,0,0,0,0,0,0] 81)
  for P :: J_prog
where

  "P ⊢ ⟨e,s,b⟩ → ⟨e',s',b'⟩ ≡ ((e,s,b), e',s',b') ∈ red P"
| "P ⊢ ⟨es,s,b⟩ [→] ⟨es',s',b'⟩ ≡ ((es,s,b), es',s',b') ∈ reds P"

| RedNew:
  "⟦ new_Addr h = Some a; P ⊢ C has_fields FDTs; h' = h(a↦blank P C) ⟧
  ⟹ P ⊢ ⟨new C, (h,l,sh), True⟩ → ⟨addr a, (h',l,sh), False⟩"

| RedNewFail:
  "⟦ new_Addr h = None; is_class P C ⟧ ⟹
  P ⊢ ⟨new C, (h,l,sh), True⟩ → ⟨THROW OutOfMemory, (h,l,sh), False⟩"

| NewInitDoneRed:
  "sh C = Some (sfs, Done) ⟹
  P ⊢ ⟨new C, (h,l,sh), False⟩ → ⟨new C, (h,l,sh), True⟩"

| NewInitRed:
  "⟦ ∄sfs. sh C = Some (sfs, Done); is_class P C ⟧
  ⟹ P ⊢ ⟨new C,(h,l,sh),False⟩ → ⟨INIT C ([C],False) ← new C,(h,l,sh),False⟩"

| CastRed:
  "P ⊢ ⟨e,s,b⟩ → ⟨e',s',b'⟩ ⟹
  P ⊢ ⟨Cast C e, s, b⟩ → ⟨Cast C e', s', b'⟩"

| RedCastNull:
  "P ⊢ ⟨Cast C null, s, b⟩ → ⟨null,s,b⟩"

| RedCast:
 "⟦ h a = Some(D,fs); P ⊢ D ≼⇧* C ⟧
  ⟹ P ⊢ ⟨Cast C (addr a), (h,l,sh), b⟩ → ⟨addr a, (h,l,sh), b⟩"

| RedCastFail:
  "⟦ h a = Some(D,fs); ¬ P ⊢ D ≼⇧* C ⟧
  ⟹ P ⊢ ⟨Cast C (addr a), (h,l,sh), b⟩ → ⟨THROW ClassCast, (h,l,sh), b⟩"

| BinOpRed1:
  "P ⊢ ⟨e,s,b⟩ → ⟨e',s',b'⟩ ⟹
  P ⊢ ⟨e «bop» e⇩2, s, b⟩ → ⟨e' «bop» e⇩2, s', b'⟩"

| BinOpRed2:
  "P ⊢ ⟨e,s,b⟩ → ⟨e',s',b'⟩ ⟹
  P ⊢ ⟨(Val v⇩1) «bop» e, s, b⟩ → ⟨(Val v⇩1) «bop» e', s', b'⟩"

| RedBinOp:
  "binop(bop,v⇩1,v⇩2) = Some v ⟹
  P ⊢ ⟨(Val v⇩1) «bop» (Val v⇩2), s, b⟩ → ⟨Val v,s,b⟩"

| RedVar:
  "l V = Some v ⟹
  P ⊢ ⟨Var V,(h,l,sh),b⟩ → ⟨Val v,(h,l,sh),b⟩"

| LAssRed:
  "P ⊢ ⟨e,s,b⟩ → ⟨e',s',b'⟩ ⟹
  P ⊢ ⟨V:=e,s,b⟩ → ⟨V:=e',s',b'⟩"

| RedLAss:
  "P ⊢ ⟨V:=(Val v), (h,l,sh), b⟩ → ⟨unit, (h,l(V↦v),sh), b⟩"

| FAccRed:
  "P ⊢ ⟨e,s,b⟩ → ⟨e',s',b'⟩ ⟹
  P ⊢ ⟨e∙F{D}, s, b⟩ → ⟨e'∙F{D}, s', b'⟩"

| RedFAcc:
  "⟦ h a = Some(C,fs); fs(F,D) = Some v;
     P ⊢ C has F,NonStatic:t in D ⟧
  ⟹ P ⊢ ⟨(addr a)∙F{D}, (h,l,sh), b⟩ → ⟨Val v,(h,l,sh),b⟩"

| RedFAccNull:
  "P ⊢ ⟨null∙F{D}, s, b⟩ → ⟨THROW NullPointer, s, b⟩"

| RedFAccNone:
  "⟦ h a = Some(C,fs); ¬(∃b t. P ⊢ C has F,b:t in D) ⟧
  ⟹ P ⊢ ⟨(addr a)∙F{D},(h,l,sh),b⟩ → ⟨THROW NoSuchFieldError,(h,l,sh),b⟩"

| RedFAccStatic:
  "⟦ h a = Some(C,fs); P ⊢ C has F,Static:t in D ⟧
  ⟹ P ⊢ ⟨(addr a)∙F{D},(h,l,sh),b⟩ → ⟨THROW IncompatibleClassChangeError,(h,l,sh),b⟩"

| RedSFAcc:
  "⟦ P ⊢ C has F,Static:t in D;
     sh D = Some (sfs,i);
     sfs F = Some v ⟧
  ⟹ P ⊢ ⟨C∙⇩sF{D},(h,l,sh),True⟩ → ⟨Val v,(h,l,sh),False⟩"

| SFAccInitDoneRed:
  "⟦ P ⊢ C has F,Static:t in D;
     sh D = Some (sfs,Done) ⟧
  ⟹ P ⊢ ⟨C∙⇩sF{D},(h,l,sh),False⟩ → ⟨C∙⇩sF{D},(h,l,sh),True⟩"

| SFAccInitRed:
  "⟦ P ⊢ C has F,Static:t in D;
     ∄sfs. sh D = Some (sfs,Done) ⟧
  ⟹ P ⊢ ⟨C∙⇩sF{D},(h,l,sh),False⟩ → ⟨INIT D ([D],False) ← C∙⇩sF{D},(h,l,sh),False⟩"

| RedSFAccNone:
  "¬(∃b t. P ⊢ C has F,b:t in D)
  ⟹ P ⊢ ⟨C∙⇩sF{D},(h,l,sh),b⟩ → ⟨THROW NoSuchFieldError,(h,l,sh),False⟩"

| RedSFAccNonStatic:
  "P ⊢ C has F,NonStatic:t in D
  ⟹ P ⊢ ⟨C∙⇩sF{D},(h,l,sh),b⟩ → ⟨THROW IncompatibleClassChangeError,(h,l,sh),False⟩"

| FAssRed1:
  "P ⊢ ⟨e,s,b⟩ → ⟨e',s',b'⟩ ⟹
  P ⊢ ⟨e∙F{D}:=e⇩2, s, b⟩ → ⟨e'∙F{D}:=e⇩2, s', b'⟩"

| FAssRed2:
  "P ⊢ ⟨e,s,b⟩ → ⟨e',s',b'⟩ ⟹
  P ⊢ ⟨Val v∙F{D}:=e, s, b⟩ → ⟨Val v∙F{D}:=e', s', b'⟩"

| RedFAss:
  "⟦ P ⊢ C has F,NonStatic:t in D; h a = Some(C,fs) ⟧ ⟹
  P ⊢ ⟨(addr a)∙F{D}:=(Val v), (h,l,sh), b⟩ → ⟨unit, (h(a ↦ (C,fs((F,D) ↦ v))),l,sh), b⟩"

| RedFAssNull:
  "P ⊢ ⟨null∙F{D}:=Val v, s, b⟩ → ⟨THROW NullPointer, s, b⟩"

| RedFAssNone:
  "⟦ h a = Some(C,fs); ¬(∃b t. P ⊢ C has F,b:t in D) ⟧
  ⟹ P ⊢ ⟨(addr a)∙F{D}:=(Val v),(h,l,sh),b⟩ → ⟨THROW NoSuchFieldError,(h,l,sh),b⟩"

| RedFAssStatic:
  "⟦ h a = Some(C,fs); P ⊢ C has F,Static:t in D ⟧
  ⟹ P ⊢ ⟨(addr a)∙F{D}:=(Val v),(h,l,sh),b⟩ → ⟨THROW IncompatibleClassChangeError,(h,l,sh),b⟩"

| SFAssRed:
  "P ⊢ ⟨e,s,b⟩ → ⟨e',s',b'⟩ ⟹
  P ⊢ ⟨C∙⇩sF{D}:=e, s, b⟩ → ⟨C∙⇩sF{D}:=e', s', b'⟩"

| RedSFAss:
  "⟦ P ⊢ C has F,Static:t in D;
     sh D = Some(sfs,i);
     sfs' = sfs(F↦v); sh' = sh(D↦(sfs',i)) ⟧
  ⟹ P ⊢ ⟨C∙⇩sF{D}:=(Val v),(h,l,sh),True⟩ → ⟨unit,(h,l,sh'),False⟩"

| SFAssInitDoneRed:
  "⟦ P ⊢ C has F,Static:t in D;
     sh D = Some(sfs,Done) ⟧
  ⟹ P ⊢ ⟨C∙⇩sF{D}:=(Val v),(h,l,sh),False⟩ → ⟨C∙⇩sF{D}:=(Val v),(h,l,sh),True⟩"

| SFAssInitRed:
  "⟦ P ⊢ C has F,Static:t in D;
     ∄sfs. sh D = Some(sfs,Done) ⟧
  ⟹ P ⊢ ⟨C∙⇩sF{D}:=(Val v),(h,l,sh),False⟩ → ⟨INIT D ([D],False)← C∙⇩sF{D}:=(Val v),(h,l,sh),False⟩"

| RedSFAssNone:
  "¬(∃b t. P ⊢ C has F,b:t in D)
  ⟹ P ⊢ ⟨C∙⇩sF{D}:=(Val v),s,b⟩ → ⟨THROW NoSuchFieldError,s,False⟩"

| RedSFAssNonStatic:
  "P ⊢ C has F,NonStatic:t in D
  ⟹ P ⊢ ⟨C∙⇩sF{D}:=(Val v),s,b⟩ → ⟨THROW IncompatibleClassChangeError,s,False⟩"

| CallObj:
  "P ⊢ ⟨e,s,b⟩ → ⟨e',s',b'⟩ ⟹
  P ⊢ ⟨e∙M(es),s,b⟩ → ⟨e'∙M(es),s',b'⟩"

| CallParams:
  "P ⊢ ⟨es,s,b⟩ [→] ⟨es',s',b'⟩ ⟹
  P ⊢ ⟨(Val v)∙M(es),s,b⟩ → ⟨(Val v)∙M(es'),s',b'⟩"

| RedCall:
  "⟦ h a = Some(C,fs); P ⊢ C sees M,NonStatic:Ts→T = (pns,body) in D; size vs = size pns; size Ts = size pns ⟧
  ⟹ P ⊢ ⟨(addr a)∙M(map Val vs), (h,l,sh), b⟩ → ⟨blocks(this#pns, Class D#Ts, Addr a#vs, body), (h,l,sh), b⟩"

| RedCallNull:
  "P ⊢ ⟨null∙M(map Val vs),s,b⟩ → ⟨THROW NullPointer,s,b⟩"

| RedCallNone:
  "⟦ h a = Some(C,fs); ¬(∃b Ts T m D. P ⊢ C sees M,b:Ts→T = m in D) ⟧
  ⟹ P ⊢ ⟨(addr a)∙M(map Val vs),(h,l,sh),b⟩ → ⟨THROW NoSuchMethodError,(h,l,sh),b⟩"

| RedCallStatic:
  "⟦ h a = Some(C,fs); P ⊢ C sees M,Static:Ts→T = m in D ⟧
  ⟹ P ⊢ ⟨(addr a)∙M(map Val vs),(h,l,sh),b⟩ → ⟨THROW IncompatibleClassChangeError,(h,l,sh),b⟩"

| SCallParams:
  "P ⊢ ⟨es,s,b⟩ [→] ⟨es',s',b'⟩ ⟹
  P ⊢ ⟨C∙⇩sM(es),s,b⟩ → ⟨C∙⇩sM(es'),s',b'⟩"

| RedSCall:
  "⟦ P ⊢ C sees M,Static:Ts→T = (pns,body) in D;
     length vs = length pns; size Ts = size pns ⟧
  ⟹ P ⊢ ⟨C∙⇩sM(map Val vs),s,True⟩ → ⟨blocks(pns, Ts, vs, body), s, False⟩"

| SCallInitDoneRed:
  "⟦ P ⊢ C sees M,Static:Ts→T = (pns,body) in D;
     sh D = Some(sfs,Done) ∨ (M = clinit ∧ sh D = Some(sfs,Processing)) ⟧
  ⟹ P ⊢ ⟨C∙⇩sM(map Val vs),(h,l,sh), False⟩ → ⟨C∙⇩sM(map Val vs),(h,l,sh), True⟩"

| SCallInitRed:
  "⟦ P ⊢ C sees M,Static:Ts→T = (pns,body) in D;
     ∄sfs. sh D = Some(sfs,Done); M ≠ clinit ⟧
  ⟹ P ⊢ ⟨C∙⇩sM(map Val vs),(h,l,sh), False⟩ → ⟨INIT D ([D],False) ← C∙⇩sM(map Val vs),(h,l,sh),False⟩"

| RedSCallNone:
  "⟦ ¬(∃b Ts T m D. P ⊢ C sees M,b:Ts→T = m in D) ⟧
  ⟹ P ⊢ ⟨C∙⇩sM(map Val vs),s,b⟩ → ⟨THROW NoSuchMethodError,s,False⟩"

| RedSCallNonStatic:
  "⟦ P ⊢ C sees M,NonStatic:Ts→T = m in D ⟧
  ⟹ P ⊢ ⟨C∙⇩sM(map Val vs),s,b⟩ → ⟨THROW IncompatibleClassChangeError,s,False⟩"

| BlockRedNone:
  "⟦ P ⊢ ⟨e, (h,l(V:=None),sh), b⟩ → ⟨e', (h',l',sh'), b'⟩; l' V = None; ¬ assigned V e ⟧
  ⟹ P ⊢ ⟨{V:T; e}, (h,l,sh), b⟩ → ⟨{V:T; e'}, (h',l'(V := l V),sh'), b'⟩"

| BlockRedSome:
  "⟦ P ⊢ ⟨e, (h,l(V:=None),sh), b⟩ → ⟨e', (h',l',sh'), b'⟩; l' V = Some v;¬ assigned V e ⟧
  ⟹ P ⊢ ⟨{V:T; e}, (h,l,sh), b⟩ → ⟨{V:T := Val v; e'}, (h',l'(V := l V),sh'), b'⟩"

| InitBlockRed:
  "⟦ P ⊢ ⟨e, (h,l(V↦v),sh), b⟩ → ⟨e', (h',l',sh'), b'⟩; l' V = Some v' ⟧
  ⟹ P ⊢ ⟨{V:T := Val v; e}, (h,l,sh), b⟩ → ⟨{V:T := Val v'; e'}, (h',l'(V := l V),sh'), b'⟩"

| RedBlock:
  "P ⊢ ⟨{V:T; Val u}, s, b⟩ → ⟨Val u, s, b⟩"

| RedInitBlock:
  "P ⊢ ⟨{V:T := Val v; Val u}, s, b⟩ → ⟨Val u, s, b⟩"

| SeqRed:
  "P ⊢ ⟨e,s,b⟩ → ⟨e',s',b'⟩ ⟹
  P ⊢ ⟨e;;e⇩2, s, b⟩ → ⟨e';;e⇩2, s', b'⟩"

| RedSeq:
  "P ⊢ ⟨(Val v);;e⇩2, s, b⟩ → ⟨e⇩2, s, b⟩"

| CondRed:
  "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'⟩"

| RedCondT:
  "P ⊢ ⟨if (true) e⇩1 else e⇩2, s, b⟩ → ⟨e⇩1, s, b⟩"

| RedCondF:
  "P ⊢ ⟨if (false) e⇩1 else e⇩2, s, b⟩ → ⟨e⇩2, s, b⟩"

| RedWhile:
  "P ⊢ ⟨while(b) c, s, b'⟩ → ⟨if(b) (c;;while(b) c) else unit, s, b'⟩"

| ThrowRed:
  "P ⊢ ⟨e,s,b⟩ → ⟨e',s',b'⟩ ⟹
  P ⊢ ⟨throw e, s, b⟩ → ⟨throw e', s', b'⟩"

| RedThrowNull:
  "P ⊢ ⟨throw null, s, b⟩ → ⟨THROW NullPointer, s, b⟩"

| TryRed:
  "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'⟩"

| RedTry:
  "P ⊢ ⟨try (Val v) catch(C V) e⇩2, s, b⟩ → ⟨Val v, s, b⟩"

| RedTryCatch:
  "⟦ hp s a = Some(D,fs); P ⊢ D ≼⇧* C ⟧
  ⟹ P ⊢ ⟨try (Throw a) catch(C V) e⇩2, s, b⟩ → ⟨{V:Class C := addr a; e⇩2}, s, b⟩"

| RedTryFail:
  "⟦ hp s a = Some(D,fs); ¬ P ⊢ D ≼⇧* C ⟧
  ⟹ P ⊢ ⟨try (Throw a) catch(C V) e⇩2, s, b⟩ → ⟨Throw a, s, b⟩"

| ListRed1:
  "P ⊢ ⟨e,s,b⟩ → ⟨e',s',b'⟩ ⟹
  P ⊢ ⟨e#es,s,b⟩ [→] ⟨e'#es,s',b'⟩"

| ListRed2:
  "P ⊢ ⟨es,s,b⟩ [→] ⟨es',s',b'⟩ ⟹
  P ⊢ ⟨Val v # es,s,b⟩ [→] ⟨Val v # es',s',b'⟩"

― ‹Initialization procedure›

| RedInit:
  "¬sub_RI e ⟹ P ⊢ ⟨INIT C (Nil,b) ← e,s,b'⟩ → ⟨e,s,icheck P C e⟩"

| InitNoneRed:
  "sh C = None
  ⟹ P ⊢ ⟨INIT C' (C#Cs,False) ← e,(h,l,sh),b⟩ → ⟨INIT C' (C#Cs,False) ← e,(h,l,sh(C ↦ (sblank P C, Prepared))),b⟩"

| RedInitDone:
  "sh C = Some(sfs,Done)
  ⟹ P ⊢ ⟨INIT C' (C#Cs,False) ← e,(h,l,sh),b⟩ → ⟨INIT C' (Cs,True) ← e,(h,l,sh),b⟩"

| RedInitProcessing:
  "sh C = Some(sfs,Processing)
  ⟹ P ⊢ ⟨INIT C' (C#Cs,False) ← e,(h,l,sh),b⟩ → ⟨INIT C' (Cs,True) ← e,(h,l,sh),b⟩"

| RedInitError:
  "sh C = Some(sfs,Error)
  ⟹ P ⊢ ⟨INIT C' (C#Cs,False) ← e,(h,l,sh),b⟩ → ⟨RI (C,THROW NoClassDefFoundError);Cs ← e,(h,l,sh),b⟩"

| InitObjectRed:
  "⟦ sh C = Some(sfs,Prepared);
     C = Object;
     sh' = sh(C ↦ (sfs,Processing)) ⟧
  ⟹ P ⊢ ⟨INIT C' (C#Cs,False) ← e,(h,l,sh),b⟩ → ⟨INIT C' (C#Cs,True) ← e,(h,l,sh'),b⟩"

| InitNonObjectSuperRed:
  "⟦ sh C = Some(sfs,Prepared);
     C ≠ Object;
     class P C = Some (D,r);
     sh' = sh(C ↦ (sfs,Processing)) ⟧
  ⟹ P ⊢ ⟨INIT C' (C#Cs,False) ← e,(h,l,sh),b⟩ → ⟨INIT C' (D#C#Cs,False) ← e,(h,l,sh'),b⟩"

| RedInitRInit:
  "P ⊢ ⟨INIT C' (C#Cs,True) ← e,(h,l,sh),b⟩ → ⟨RI (C,C∙⇩sclinit([]));Cs ← e,(h,l,sh),b⟩"

| RInitRed:
  "P ⊢ ⟨e,s,b⟩ → ⟨e',s',b'⟩ ⟹
  P ⊢ ⟨RI (C,e);Cs ← e⇩0, s, b⟩ → ⟨RI (C,e');Cs ← e⇩0, s', b'⟩"

| RedRInit:
  "⟦ sh C = Some (sfs, i);
     sh' = sh(C ↦ (sfs,Done));
     C' = last(C#Cs) ⟧ ⟹
  P ⊢ ⟨RI (C, Val v);Cs ← e, (h,l,sh), b⟩ → ⟨INIT C' (Cs,True) ← e, (h,l,sh'), b⟩"

― ‹Exception propagation›

| CastThrow: "P ⊢ ⟨Cast C (throw e), s, b⟩ → ⟨throw e, s, b⟩"
| BinOpThrow1: "P ⊢ ⟨(throw e) «bop» e⇩2, s, b⟩ → ⟨throw e, s, b⟩"
| BinOpThrow2: "P ⊢ ⟨(Val v⇩1) «bop» (throw e), s, b⟩ → ⟨throw e, s, b⟩"
| LAssThrow: "P ⊢ ⟨V:=(throw e), s, b⟩ → ⟨throw e, s, b⟩"
| FAccThrow: "P ⊢ ⟨(throw e)∙F{D}, s, b⟩ → ⟨throw e, s, b⟩"
| FAssThrow1: "P ⊢ ⟨(throw e)∙F{D}:=e⇩2, s, b⟩ → ⟨throw e, s, b⟩"
| FAssThrow2: "P ⊢ ⟨Val v∙F{D}:=(throw e), s, b⟩ → ⟨throw e, s, b⟩"
| SFAssThrow: "P ⊢ ⟨C∙⇩sF{D}:=(throw e), s, b⟩ → ⟨throw e, s, b⟩"
| CallThrowObj: "P ⊢ ⟨(throw e)∙M(es), s, b⟩ → ⟨throw e, s, b⟩"
| CallThrowParams: "⟦ es = map Val vs @ throw e # es' ⟧ ⟹ P ⊢ ⟨(Val v)∙M(es), s, b⟩ → ⟨throw e, s, b⟩"
| SCallThrowParams: "⟦ es = map Val vs @ throw e # es' ⟧ ⟹ P ⊢ ⟨C∙⇩sM(es), s, b⟩ → ⟨throw e, s, b⟩"
| BlockThrow: "P ⊢ ⟨{V:T; Throw a}, s, b⟩ → ⟨Throw a, s, b⟩"
| InitBlockThrow: "P ⊢ ⟨{V:T := Val v; Throw a}, s, b⟩ → ⟨Throw a, s, b⟩"
| SeqThrow: "P ⊢ ⟨(throw e);;e⇩2, s, b⟩ → ⟨throw e, s, b⟩"
| CondThrow: "P ⊢ ⟨if (throw e) e⇩1 else e⇩2, s, b⟩ → ⟨throw e, s, b⟩"
| ThrowThrow: "P ⊢ ⟨throw(throw e), s, b⟩ → ⟨throw e, s, b⟩"
| RInitInitThrow: "⟦ sh C = Some(sfs,i); sh' = sh(C ↦ (sfs,Error)) ⟧ ⟹
  P ⊢ ⟨RI (C,Throw a);D#Cs ← e,(h,l,sh),b⟩ → ⟨RI (D,Throw a);Cs ← e,(h,l,sh'),b⟩"
| RInitThrow: "⟦ sh C = Some(sfs, i); sh' = sh(C ↦ (sfs,Error)) ⟧ ⟹
  P ⊢ ⟨RI (C,Throw a);Nil ← e,(h,l,sh),b⟩ → ⟨Throw a,(h,l,sh'),b⟩"
(*<*)
lemmas red_reds_induct = red_reds.induct [split_format (complete)]
  and red_reds_inducts = red_reds.inducts [split_format (complete)]

inductive_cases [elim!]:
 "P ⊢ ⟨V:=e,s,b⟩ → ⟨e',s',b'⟩"
 "P ⊢ ⟨e1;;e2,s,b⟩ → ⟨e',s',b'⟩"
(*>*)

subsection‹ The reflexive transitive closure ›

abbreviation
  Step :: "J_prog ⇒ expr ⇒ state ⇒ bool ⇒ expr ⇒ state ⇒ bool ⇒ bool"
          (‹_ ⊢ ((1⟨_,/_,/_⟩) →*/ (1⟨_,/_,/_⟩))› [51,0,0,0,0,0,0] 81)
  where "P ⊢ ⟨e,s,b⟩ →* ⟨e',s',b'⟩ ≡ ((e,s,b), e',s',b') ∈ (red P)⇧*"

abbreviation
  Steps :: "J_prog ⇒ expr list ⇒ state ⇒ bool ⇒ expr list ⇒ state ⇒ bool ⇒ bool"
          (‹_ ⊢ ((1⟨_,/_,/_⟩) [→]*/ (1⟨_,/_,/_⟩))› [51,0,0,0,0,0,0] 81)
  where "P ⊢ ⟨es,s,b⟩ [→]* ⟨es',s',b'⟩ ≡ ((es,s,b), es',s',b') ∈ (reds P)⇧*"


lemmas converse_rtrancl_induct3 =
  converse_rtrancl_induct [of "(ax, ay, az)" "(bx, by, bz)", split_format (complete),
    consumes 1, case_names refl step]

lemma converse_rtrancl_induct_red[consumes 1]:
assumes "P ⊢ ⟨e,(h,l,sh),b⟩ →* ⟨e',(h',l',sh'),b'⟩"
and "⋀e h l sh b. R e h l sh b e h l sh b"
and "⋀e⇩0 h⇩0 l⇩0 sh⇩0 b⇩0 e⇩1 h⇩1 l⇩1 sh⇩1 b⇩1 e' h' l' sh' b'.
       ⟦ P ⊢ ⟨e⇩0,(h⇩0,l⇩0,sh⇩0),b⇩0⟩ → ⟨e⇩1,(h⇩1,l⇩1,sh⇩1),b⇩1⟩; R e⇩1 h⇩1 l⇩1 sh⇩1 b⇩1 e' h' l' sh' b' ⟧
   ⟹ R e⇩0 h⇩0 l⇩0 sh⇩0 b⇩0 e' h' l' sh' b'"
shows "R e h l sh b e' h' l' sh' b'"
(*<*)
proof -
  { fix s s'
    assume reds: "P ⊢ ⟨e,s,b⟩ →* ⟨e',s',b'⟩"
       and base: "⋀e s b. R e (hp s) (lcl s) (shp s) b e (hp s) (lcl s) (shp s) b"
       and red⇩1: "⋀e⇩0 s⇩0 b⇩0 e⇩1 s⇩1 b⇩1 e' s' b'.
           ⟦ P ⊢ ⟨e⇩0,s⇩0,b⇩0⟩ → ⟨e⇩1,s⇩1,b⇩1⟩; R e⇩1 (hp s⇩1) (lcl s⇩1) (shp s⇩1) b⇩1 e' (hp s') (lcl s') (shp s') b' ⟧
           ⟹ R e⇩0 (hp s⇩0) (lcl s⇩0) (shp s⇩0) b⇩0 e' (hp s') (lcl s') (shp s') b'"
    from reds have "R e (hp s) (lcl s) (shp s) b e' (hp s') (lcl s') (shp s') b'"
    proof (induct rule:converse_rtrancl_induct3)
      case refl show ?case by(rule base)
    next
      case step
      thus ?case by(blast intro:red⇩1)
    qed
    }
  with assms show ?thesis by fastforce
qed
(*>*)


subsection‹Some easy lemmas›

lemma [iff]: "¬ P ⊢ ⟨[],s,b⟩ [→] ⟨es',s',b'⟩"
(*<*)by(blast elim: reds.cases)(*>*)

lemma [iff]: "¬ P ⊢ ⟨Val v,s,b⟩ → ⟨e',s',b'⟩"
(*<*)by(fastforce elim: red.cases)(*>*)

lemma val_no_step: "val_of e = ⌊v⌋ ⟹ ¬ P ⊢ ⟨e,s,b⟩ → ⟨e',s',b'⟩"
(*<*)by(drule val_of_spec, simp)(*>*)

lemma [iff]: "¬ P ⊢ ⟨Throw a,s,b⟩ → ⟨e',s',b'⟩"
(*<*)by(fastforce elim: red.cases)(*>*)


lemma map_Vals_no_step [iff]: "¬ P ⊢ ⟨map Val vs,s,b⟩ [→] ⟨es',s',b'⟩"
(*<*)
proof(induct vs arbitrary: es')
  case (Cons a vs)
  { assume "P ⊢ ⟨map Val (a # vs),s,b⟩ [→] ⟨es',s',b'⟩"
    then have False by(rule reds.cases) (insert Cons, auto)
  }
  then show ?case by clarsimp
qed simp
(*>*)

lemma vals_no_step: "map_vals_of es = ⌊vs⌋ ⟹ ¬ P ⊢ ⟨es,s,b⟩ [→] ⟨es',s',b'⟩"
(*<*)by(drule map_vals_of_spec, simp)(*>*)

lemma vals_throw_no_step [iff]: "¬ P ⊢ ⟨map Val vs @ Throw a # es,s,b⟩ [→] ⟨es',s',b'⟩"
(*<*)
proof(induct vs arbitrary: es')
  case Nil
  { assume "P ⊢ ⟨Throw a # es,s,b⟩ [→] ⟨es',s',b'⟩"
    then have False by(rule reds.cases) (insert Cons, auto)
  }
  then show ?case by clarsimp
next
  case (Cons a' vs')
  { assume "P ⊢ ⟨map Val (a'#vs') @ Throw a # es,s,b⟩ [→] ⟨es',s',b'⟩"
    then have False by(rule reds.cases) (insert Cons, auto)
  }
  then show ?case by clarsimp
qed
(*>*)

lemma lass_val_of_red:
 "⟦ lass_val_of e = ⌊a⌋; P ⊢ ⟨e,(h, l, sh),b⟩ → ⟨e',(h', l', sh'),b'⟩ ⟧
  ⟹ e' = unit ∧ h' = h ∧ l' = l(fst a↦snd a) ∧ sh' = sh ∧ b = b'"
(*<*)by(drule lass_val_of_spec, auto)(*>*)


lemma final_no_step [iff]: "final e ⟹ ¬ P ⊢ ⟨e,s,b⟩ → ⟨e',s',b'⟩"
(*<*)by(erule finalE, simp+)(*>*)

lemma finals_no_step [iff]: "finals es ⟹ ¬ P ⊢ ⟨es,s,b⟩ [→] ⟨es',s',b'⟩"
(*<*)by(erule finalsE, simp+)(*>*)

lemma reds_final_same:
"P ⊢ ⟨e,s,b⟩ →* ⟨e',s',b'⟩ ⟹ final e ⟹ e = e' ∧ s = s' ∧ b = b'"
proof(induct rule:converse_rtrancl_induct3)
  case refl show ?case by simp
next
  case (step e0 s0 b0 e1 s1 b1) show ?case
  proof(rule finalE[OF step.prems(1)])
    fix v assume "e0 = Val v" then show ?thesis using step by simp
  next
    fix a assume "e0 = Throw a" then show ?thesis using step by simp
  qed
qed

lemma reds_throw:
"P ⊢ ⟨e,s,b⟩ →* ⟨e',s',b'⟩ ⟹ (⋀e⇩t. throw_of e = ⌊e⇩t⌋ ⟹ ∃e⇩t'. throw_of e' = ⌊e⇩t'⌋)"
proof(induct rule:converse_rtrancl_induct3)
  case refl then show ?case by simp
next
  case (step e0 s0 b0 e1 s1 b1)
  then show ?case by(auto elim: red.cases)
qed

lemma red_hext_incr: "P ⊢ ⟨e,(h,l,sh),b⟩ → ⟨e',(h',l',sh'),b'⟩  ⟹ h ⊴ h'"
  and reds_hext_incr: "P ⊢ ⟨es,(h,l,sh),b⟩ [→] ⟨es',(h',l',sh'),b'⟩  ⟹ h ⊴ h'"
(*<*)
proof(induct rule:red_reds_inducts)
  case RedNew thus ?case
    by(fastforce dest:new_Addr_SomeD simp:hext_def split:if_splits)
next
  case RedFAss thus ?case by(simp add:hext_def split:if_splits)
qed simp_all
(*>*)


lemma red_lcl_incr: "P ⊢ ⟨e,(h⇩0,l⇩0,sh⇩0),b⟩ → ⟨e',(h⇩1,l⇩1,sh⇩1),b'⟩ ⟹ dom l⇩0 ⊆ dom l⇩1"
and reds_lcl_incr: "P ⊢ ⟨es,(h⇩0,l⇩0,sh⇩0),b⟩ [→] ⟨es',(h⇩1,l⇩1,sh⇩1),b'⟩ ⟹ dom l⇩0 ⊆ dom l⇩1"
(*<*)by(induct rule: red_reds_inducts)(auto simp del:fun_upd_apply)(*>*)

lemma red_lcl_add: "P ⊢ ⟨e,(h,l,sh),b⟩ → ⟨e',(h',l',sh'),b'⟩ ⟹ (⋀l⇩0. P ⊢ ⟨e,(h,l⇩0++l,sh),b⟩ → ⟨e',(h',l⇩0++l',sh'),b'⟩)"
and reds_lcl_add: "P ⊢ ⟨es,(h,l,sh),b⟩ [→] ⟨es',(h',l',sh'),b'⟩ ⟹ (⋀l⇩0. P ⊢ ⟨es,(h,l⇩0++l,sh),b⟩ [→] ⟨es',(h',l⇩0++l',sh'),b'⟩)"
(*<*)
proof (induct rule:red_reds_inducts)
  case RedCast thus ?case by(fastforce intro:red_reds.intros)
next
  case RedCastFail thus ?case by(force intro:red_reds.intros)
next
  case RedFAcc thus ?case by(fastforce intro:red_reds.intros)
next
  case RedCall thus ?case by(fastforce intro:red_reds.intros)
next
  case (InitBlockRed e h l V v sh b e' h' l' sh' b' v' T l⇩0)
  have IH: "⋀l⇩0. P ⊢ ⟨e,(h, l⇩0 ++ l(V ↦ v), sh),b⟩ → ⟨e',(h', l⇩0 ++ l', sh'),b'⟩"
    and l'V: "l' V = Some v'" by fact+
  from IH have IH': "P ⊢ ⟨e,(h, (l⇩0 ++ l)(V ↦ v), sh),b⟩ → ⟨e',(h', l⇩0 ++ l', sh'),b'⟩"
    by simp
  have "(l⇩0 ++ l')(V := (l⇩0 ++ l) V) = l⇩0 ++ l'(V := l V)"
    by(rule ext)(simp add:map_add_def)
  with red_reds.InitBlockRed[OF IH'] l'V show ?case by(simp del:fun_upd_apply)
next
  case (BlockRedNone e h l V sh b e' h' l' sh' b' T l⇩0)
  have IH: "⋀l⇩0. P ⊢ ⟨e,(h, l⇩0 ++ l(V := None), sh),b⟩ → ⟨e',(h', l⇩0 ++ l', sh'),b'⟩"
    and l'V: "l' V = None" and unass: "¬ assigned V e" by fact+
  have "l⇩0(V := None) ++ l(V := None) = (l⇩0 ++ l)(V := None)"
    by(simp add:fun_eq_iff map_add_def)
  hence IH': "P ⊢ ⟨e,(h, (l⇩0++l)(V := None), sh),b⟩ → ⟨e',(h', l⇩0(V := None) ++ l', sh'),b'⟩"
    using IH[of "l⇩0(V := None)"] by simp
  have "(l⇩0(V := None) ++ l')(V := (l⇩0 ++ l) V) = l⇩0 ++ l'(V := l V)"
    by(simp add:fun_eq_iff map_add_def)
  with red_reds.BlockRedNone[OF IH' _ unass] l'V show ?case
    by(simp add: map_add_def)
next
  case (BlockRedSome e h l V sh b e' h' l' sh' b' v T l⇩0)
  have IH: "⋀l⇩0. P ⊢ ⟨e,(h, l⇩0 ++ l(V := None), sh),b⟩ → ⟨e',(h', l⇩0 ++ l', sh'),b'⟩"
    and l'V: "l' V = Some v" and unass: "¬ assigned V e" by fact+
  have "l⇩0(V := None) ++ l(V := None) = (l⇩0 ++ l)(V := None)"
    by(simp add:fun_eq_iff map_add_def)
  hence IH': "P ⊢ ⟨e,(h, (l⇩0++l)(V := None), sh),b⟩ → ⟨e',(h', l⇩0(V := None) ++ l', sh'),b'⟩"
    using IH[of "l⇩0(V := None)"] by simp
  have "(l⇩0(V := None) ++ l')(V := (l⇩0 ++ l) V) = l⇩0 ++ l'(V := l V)"
    by(simp add:fun_eq_iff map_add_def)
  with red_reds.BlockRedSome[OF IH' _ unass] l'V show ?case
    by(simp add:map_add_def)
next
  case RedTryCatch thus ?case by(fastforce intro:red_reds.intros)
next
  case RedTryFail thus ?case by(force intro!:red_reds.intros)
qed (simp_all add:red_reds.intros)
(*>*)


lemma Red_lcl_add:
assumes "P ⊢ ⟨e,(h,l,sh), b⟩ →* ⟨e',(h',l',sh'), b'⟩" shows "P ⊢ ⟨e,(h,l⇩0++l,sh),b⟩ →* ⟨e',(h',l⇩0++l',sh'),b'⟩"
(*<*)
using assms
proof(induct rule:converse_rtrancl_induct_red)
  case 1 thus ?case by simp
next
  case 2 thus ?case
    by (blast dest: red_lcl_add intro: converse_rtrancl_into_rtrancl)
qed
(*>*)

lemma assumes wf: "wwf_J_prog P"
shows red_proc_pres: "P ⊢ ⟨e,(h,l,sh),b⟩ → ⟨e',(h',l',sh'),b'⟩
  ⟹ not_init C e ⟹ sh C = ⌊(sfs, Processing)⌋ ⟹ not_init C e' ∧ (∃sfs'. sh' C = ⌊(sfs', Processing)⌋)"
  and reds_proc_pres: "P ⊢ ⟨es,(h,l,sh),b⟩ [→] ⟨es',(h',l',sh'),b'⟩
  ⟹ not_inits C es ⟹ sh C = ⌊(sfs, Processing)⌋ ⟹ not_inits C es' ∧ (∃sfs'. sh' C = ⌊(sfs', Processing)⌋)"
(*<*)
proof(induct rule:red_reds_inducts)
  case RedCall then show ?case
  using sees_wwf_nsub_RI[OF wf RedCall.hyps(2)] sub_RI_blocks_body nsub_RI_not_init by auto
next
  case RedSCall then show ?case
  using sees_wwf_nsub_RI[OF wf RedSCall.hyps(1)] sub_RI_blocks_body nsub_RI_not_init by auto
next
  case (RedInitDone sh C sfs C' Cs e h l b)
  then show ?case by(cases Cs, auto)
next
  case (RedInitProcessing sh C sfs C' Cs e h l b)
  then show ?case by(cases Cs, auto)
next
  case (RedRInit sh C sfs i sh' C' Cs v e h l b)
  then show ?case by(cases Cs, auto)
next
  case (CallThrowParams es vs e es' v M h l sh b)
  then show ?case by(auto dest: not_inits_def')
next
  case (SCallThrowParams es vs e es' C M h l sh b)
  then show ?case by(auto dest: not_inits_def')
qed(auto)

end