Theory SmallStep

Up to index of Isabelle/HOL/Jinja

theory SmallStep = Expr + State: 
(*  Title:      Jinja/J/SmallStep.thy
    ID:         $Id: SmallStep.html 1910 2004-05-19 04:46:04Z kleing $
    Author:     Tobias Nipkow
    Copyright   2003 Technische Universitaet Muenchen
*)

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

theory SmallStep = Expr + State:

consts blocks :: "vname list * ty list * val list * expr => expr"
recdef blocks "measure(λ(Vs,Ts,vs,e). size Vs)"
 "blocks(V#Vs, T#Ts, v#vs, e) = {V:T := Val v; blocks(Vs,Ts,vs,e)}"
 "blocks([],[],[],e) = e"


lemma [simp]:
  "[| size vs = size Vs; size Ts = size Vs |] ==> fv(blocks(Vs,Ts,vs,e)) = fv e - set Vs"
(*<*)
apply(induct rule:blocks.induct)
apply simp_all
apply blast
done
(*>*)


constdefs
  assigned :: "vname => expr => bool"
  "assigned V e  ≡  ∃v e'. e = (V := Val v;; e')"

consts
  red  :: "J_prog => ((expr × state) × (expr × state)) set"
  reds  :: "J_prog => ((expr list × state) × (expr list × state)) set"

(*<*)
syntax (xsymbols)
  red :: "J_prog => expr => state => expr => state => bool"
          ("_ \<turnstile> ((1⟨_,/_⟩) ->/ (1⟨_,/_⟩))" [51,0,0,0,0] 81)
  reds :: "J_prog => expr list => state => expr list => state => bool"
          ("_ \<turnstile> ((1⟨_,/_⟩) [->]/ (1⟨_,/_⟩))" [51,0,0,0,0] 81)
(*>*)

translations
  "P \<turnstile> ⟨e,s⟩ -> ⟨e',s'⟩"  ==  "((e,s), e',s') ∈ red P"
  "P \<turnstile> ⟨es,s⟩ [->] ⟨es',s'⟩" == "((es,s), es',s') ∈ reds P"
(*<*)
  "P \<turnstile> ⟨e,(h,l)⟩ -> ⟨e',(h',l')⟩" <= "((e,h,l), e',h',l') ∈ red P"
  "P \<turnstile> ⟨e,s⟩ -> ⟨e',(h',l')⟩" <= "((e,s), e',h',l') ∈ red P"
  "P \<turnstile> ⟨e,(h,l)⟩ -> ⟨e',s'⟩" <= "((e,h,l), e',s') ∈ red P"
  "P \<turnstile> ⟨es,(h,l)⟩ [->] ⟨es',(h',l')⟩" <= "((es,h,l), es',h',l') ∈ reds P"
  "P \<turnstile> ⟨es,s⟩ [->] ⟨es',(h',l')⟩" <= "((es,s), es',h',l') ∈ reds P"
  "P \<turnstile> ⟨es,(h,l)⟩ [->] ⟨es',s'⟩" <= "((es,h,l), es',s') ∈ reds P"
(*>*)


inductive "red P" "reds P"
intros

RedNew:
  "[| new_Addr h = Some a; P \<turnstile> C has_fields FDTs; h' = h(a\<mapsto>(C,init_fields FDTs)) |]
  ==> P \<turnstile> ⟨new C, (h,l)⟩ -> ⟨addr a, (h',l)⟩"

RedNewFail:
  "new_Addr h = None ==>
  P \<turnstile> ⟨new C, (h,l)⟩ -> ⟨THROW OutOfMemory, (h,l)⟩"

CastRed:
  "P \<turnstile> ⟨e,s⟩ -> ⟨e',s'⟩ ==>
  P \<turnstile> ⟨Cast C e, s⟩ -> ⟨Cast C e', s'⟩"

RedCastNull:
  "P \<turnstile> ⟨Cast C null, s⟩ -> ⟨null,s⟩"

RedCast:
 "[| hp s a = Some(D,fs); P \<turnstile> D \<preceq>* C |]
  ==> P \<turnstile> ⟨Cast C (addr a), s⟩ -> ⟨addr a, s⟩"

RedCastFail:
  "[| hp s a = Some(D,fs); ¬ P \<turnstile> D \<preceq>* C |]
  ==> P \<turnstile> ⟨Cast C (addr a), s⟩ -> ⟨THROW ClassCast, s⟩"

BinOpRed1:
  "P \<turnstile> ⟨e,s⟩ -> ⟨e',s'⟩ ==>
  P \<turnstile> ⟨e «bop» e2, s⟩ -> ⟨e' «bop» e2, s'⟩"

BinOpRed2:
  "P \<turnstile> ⟨e,s⟩ -> ⟨e',s'⟩ ==>
  P \<turnstile> ⟨(Val v1) «bop» e, s⟩ -> ⟨(Val v1) «bop» e', s'⟩"

RedBinOp:
  "binop(bop,v1,v2) = Some v ==>
  P \<turnstile> ⟨(Val v1) «bop» (Val v2), s⟩ -> ⟨Val v,s⟩"

RedVar:
  "lcl s V = Some v ==>
  P \<turnstile> ⟨Var V,s⟩ -> ⟨Val v,s⟩"

LAssRed:
  "P \<turnstile> ⟨e,s⟩ -> ⟨e',s'⟩ ==>
  P \<turnstile> ⟨V:=e,s⟩ -> ⟨V:=e',s'⟩"

RedLAss:
  "P \<turnstile> ⟨V:=(Val v), (h,l)⟩ -> ⟨unit, (h,l(V\<mapsto>v))⟩"

FAccRed:
  "P \<turnstile> ⟨e,s⟩ -> ⟨e',s'⟩ ==>
  P \<turnstile> ⟨e\<bullet>F{D}, s⟩ -> ⟨e'\<bullet>F{D}, s'⟩"

RedFAcc:
  "[| hp s a = Some(C,fs); fs(F,D) = Some v |]
  ==> P \<turnstile> ⟨(addr a)\<bullet>F{D}, s⟩ -> ⟨Val v,s⟩"

RedFAccNull:
  "P \<turnstile> ⟨null\<bullet>F{D}, s⟩ -> ⟨THROW NullPointer, s⟩"

FAssRed1:
  "P \<turnstile> ⟨e,s⟩ -> ⟨e',s'⟩ ==>
  P \<turnstile> ⟨e\<bullet>F{D}:=e2, s⟩ -> ⟨e'\<bullet>F{D}:=e2, s'⟩"

FAssRed2:
  "P \<turnstile> ⟨e,s⟩ -> ⟨e',s'⟩ ==>
  P \<turnstile> ⟨Val v\<bullet>F{D}:=e, s⟩ -> ⟨Val v\<bullet>F{D}:=e', s'⟩"

RedFAss:
  "h a = Some(C,fs) ==>
  P \<turnstile> ⟨(addr a)\<bullet>F{D}:=(Val v), (h,l)⟩ -> ⟨unit, (h(a \<mapsto> (C,fs((F,D) \<mapsto> v))),l)⟩"

RedFAssNull:
  "P \<turnstile> ⟨null\<bullet>F{D}:=Val v, s⟩ -> ⟨THROW NullPointer, s⟩"

CallObj:
  "P \<turnstile> ⟨e,s⟩ -> ⟨e',s'⟩ ==>
  P \<turnstile> ⟨e\<bullet>M(es),s⟩ -> ⟨e'\<bullet>M(es),s'⟩"

CallParams:
  "P \<turnstile> ⟨es,s⟩ [->] ⟨es',s'⟩ ==>
  P \<turnstile> ⟨(Val v)\<bullet>M(es),s⟩ -> ⟨(Val v)\<bullet>M(es'),s'⟩"

RedCall:
  "[| hp s a = Some(C,fs); P \<turnstile> C sees M:Ts->T = (pns,body) in D; size vs = size pns; size Ts = size pns |]
  ==> P \<turnstile> ⟨(addr a)\<bullet>M(map Val vs), s⟩ -> ⟨blocks(this#pns, Class D#Ts, Addr a#vs, body), s⟩"

RedCallNull:
  "P \<turnstile> ⟨null\<bullet>M(map Val vs),s⟩ -> ⟨THROW NullPointer,s⟩"

BlockRedNone:
  "[| P \<turnstile> ⟨e, (h,l(V:=None))⟩ -> ⟨e', (h',l')⟩; l' V = None; ¬ assigned V e |]
  ==> P \<turnstile> ⟨{V:T; e}, (h,l)⟩ -> ⟨{V:T; e'}, (h',l'(V := l V))⟩"

BlockRedSome:
  "[| P \<turnstile> ⟨e, (h,l(V:=None))⟩ -> ⟨e', (h',l')⟩; l' V = Some v;¬ assigned V e |]
  ==> P \<turnstile> ⟨{V:T; e}, (h,l)⟩ -> ⟨{V:T := Val v; e'}, (h',l'(V := l V))⟩"

InitBlockRed:
  "[| P \<turnstile> ⟨e, (h,l(V\<mapsto>v))⟩ -> ⟨e', (h',l')⟩; l' V = Some v' |]
  ==> P \<turnstile> ⟨{V:T := Val v; e}, (h,l)⟩ -> ⟨{V:T := Val v'; e'}, (h',l'(V := l V))⟩"

RedBlock:
  "P \<turnstile> ⟨{V:T; Val u}, s⟩ -> ⟨Val u, s⟩"

RedInitBlock:
  "P \<turnstile> ⟨{V:T := Val v; Val u}, s⟩ -> ⟨Val u, s⟩"

SeqRed:
  "P \<turnstile> ⟨e,s⟩ -> ⟨e',s'⟩ ==>
  P \<turnstile> ⟨e;;e2, s⟩ -> ⟨e';;e2, s'⟩"

RedSeq:
  "P \<turnstile> ⟨(Val v);;e2, s⟩ -> ⟨e2, s⟩"

CondRed:
  "P \<turnstile> ⟨e,s⟩ -> ⟨e',s'⟩ ==>
  P \<turnstile> ⟨if (e) e1 else e2, s⟩ -> ⟨if (e') e1 else e2, s'⟩"

RedCondT:
  "P \<turnstile> ⟨if (true) e1 else e2, s⟩ -> ⟨e1, s⟩"

RedCondF:
  "P \<turnstile> ⟨if (false) e1 else e2, s⟩ -> ⟨e2, s⟩"

RedWhile:
  "P \<turnstile> ⟨while(b) c, s⟩ -> ⟨if(b) (c;;while(b) c) else unit, s⟩"

ThrowRed:
  "P \<turnstile> ⟨e,s⟩ -> ⟨e',s'⟩ ==>
  P \<turnstile> ⟨throw e, s⟩ -> ⟨throw e', s'⟩"

RedThrowNull:
  "P \<turnstile> ⟨throw null, s⟩ -> ⟨THROW NullPointer, s⟩"

TryRed:
  "P \<turnstile> ⟨e,s⟩ -> ⟨e',s'⟩ ==>
  P \<turnstile> ⟨try e catch(C V) e2, s⟩ -> ⟨try e' catch(C V) e2, s'⟩"

RedTry:
  "P \<turnstile> ⟨try (Val v) catch(C V) e2, s⟩ -> ⟨Val v, s⟩"

RedTryCatch:
  "[| hp s a = Some(D,fs); P \<turnstile> D \<preceq>* C |]
  ==> P \<turnstile> ⟨try (Throw a) catch(C V) e2, s⟩ -> ⟨{V:Class C := addr a; e2}, s⟩"

RedTryFail:
  "[| hp s a = Some(D,fs); ¬ P \<turnstile> D \<preceq>* C |]
  ==> P \<turnstile> ⟨try (Throw a) catch(C V) e2, s⟩ -> ⟨Throw a, s⟩"

ListRed1:
  "P \<turnstile> ⟨e,s⟩ -> ⟨e',s'⟩ ==>
  P \<turnstile> ⟨e#es,s⟩ [->] ⟨e'#es,s'⟩"

ListRed2:
  "P \<turnstile> ⟨es,s⟩ [->] ⟨es',s'⟩ ==>
  P \<turnstile> ⟨Val v # es,s⟩ [->] ⟨Val v # es',s'⟩"

-- "Exception propagation"

CastThrow: "P \<turnstile> ⟨Cast C (throw e), s⟩ -> ⟨throw e, s⟩"
BinOpThrow1: "P \<turnstile> ⟨(throw e) «bop» e2, s⟩ -> ⟨throw e, s⟩"
BinOpThrow2: "P \<turnstile> ⟨(Val v1) «bop» (throw e), s⟩ -> ⟨throw e, s⟩"
LAssThrow: "P \<turnstile> ⟨V:=(throw e), s⟩ -> ⟨throw e, s⟩"
FAccThrow: "P \<turnstile> ⟨(throw e)\<bullet>F{D}, s⟩ -> ⟨throw e, s⟩"
FAssThrow1: "P \<turnstile> ⟨(throw e)\<bullet>F{D}:=e2, s⟩ -> ⟨throw e,s⟩"
FAssThrow2: "P \<turnstile> ⟨Val v\<bullet>F{D}:=(throw e), s⟩ -> ⟨throw e, s⟩"
CallThrowObj: "P \<turnstile> ⟨(throw e)\<bullet>M(es), s⟩ -> ⟨throw e, s⟩"
CallThrowParams: "[| es = map Val vs @ throw e # es' |] ==> P \<turnstile> ⟨(Val v)\<bullet>M(es), s⟩ -> ⟨throw e, s⟩"
BlockThrow: "P \<turnstile> ⟨{V:T; Throw a}, s⟩ -> ⟨Throw a, s⟩"
InitBlockThrow: "P \<turnstile> ⟨{V:T := Val v; Throw a}, s⟩ -> ⟨Throw a, s⟩"
SeqThrow: "P \<turnstile> ⟨(throw e);;e2, s⟩ -> ⟨throw e, s⟩"
CondThrow: "P \<turnstile> ⟨if (throw e) e1 else e2, s⟩ -> ⟨throw e, s⟩"
ThrowThrow: "P \<turnstile> ⟨throw(throw e), s⟩ -> ⟨throw e, s⟩"
(*<*)
lemmas red_reds_induct = red_reds.induct [split_format (complete)]

inductive_cases [elim!]:
 "P \<turnstile> ⟨V:=e,s⟩ -> ⟨e',s'⟩"
 "P \<turnstile> ⟨e1;;e2,s⟩ -> ⟨e',s'⟩"
(*>*)

subsection{* The reflexive transitive closure *}
(*<*)
syntax (xsymbols)
  Step :: "J_prog => expr => state => expr => state => bool"
          ("_ \<turnstile> ((1⟨_,/_⟩) ->*/ (1⟨_,/_⟩))" [51,0,0,0,0] 81)
  Steps :: "J_prog => expr list => state => expr list => state => bool"
          ("_ \<turnstile> ((1⟨_,/_⟩) [->]*/ (1⟨_,/_⟩))" [51,0,0,0,0] 81)
(*>*)
translations
  "P \<turnstile> ⟨e,s⟩ ->* ⟨e',s'⟩"  ==  "((e,s), e',s') ∈ (red P)*"
  "P \<turnstile> ⟨es,s⟩ [->]* ⟨es',s'⟩"  ==  "((es,s), es',s') ∈ (reds P)*"
(*<*)
  "P \<turnstile> ⟨e,(h,l)⟩ ->* ⟨e',(h',l')⟩" <= "((e,h,l), e',h',l') ∈ ((red P)^*)"
  "P \<turnstile> ⟨e,s⟩ ->* ⟨e',(h',l')⟩" <= "((e,s), e',h',l') ∈ ((red P)^*)"
  "P \<turnstile> ⟨e,(h,l)⟩ ->* ⟨e',s'⟩" <= "((e,h,l), e',s') ∈ ((red P)^*)"
  "P \<turnstile> ⟨e,(h,l)⟩ [->]* ⟨e',(h',l')⟩" <= "((e,h,l), e',h',l') ∈ ((reds P)^*)"
  "P \<turnstile> ⟨e,s⟩ [->]* ⟨e',(h',l')⟩" <= "((e,s), e',h',l') ∈ ((reds P)^*)"
  "P \<turnstile> ⟨e,(h,l)⟩ [->]* ⟨e',s'⟩" <= "((e,h,l), e',s') ∈ ((reds P)^*)"

lemma converse_rtrancl_induct_red[consumes 1]:
assumes "P \<turnstile> ⟨e,(h,l)⟩ ->* ⟨e',(h',l')⟩"
and "!!e h l. R e h l e h l"
and "!!e0 h0 l0 e1 h1 l1 e' h' l'.
       [| P \<turnstile> ⟨e0,(h0,l0)⟩ -> ⟨e1,(h1,l1)⟩; R e1 h1 l1 e' h' l' |] ==> R e0 h0 l0 e' h' l'"
shows "R e h l e' h' l'"
(*<*)
proof -
  { fix s s'
    assume reds: "P \<turnstile> ⟨e,s⟩ ->* ⟨e',s'⟩"
       and base: "!!e s. R e (hp s) (lcl s) e (hp s) (lcl s)"
       and red1: "!!e0 s0 e1 s1 e' s'.
           [| P \<turnstile> ⟨e0,s0⟩ -> ⟨e1,s1⟩; R e1 (hp s1) (lcl s1) e' (hp s') (lcl s') |]
           ==> R e0 (hp s0) (lcl s0) e' (hp s') (lcl s')"
    from reds have "R e (hp s) (lcl s) e' (hp s') (lcl s')"
    proof (induct rule:converse_rtrancl_induct2)
      case refl show ?case by(rule base)
    next
      case (step e0 s0 e s)
      thus ?case by(blast intro:red1)
    qed
    }
  with prems show ?thesis by fastsimp
qed
(*>*)


subsection{*Some easy lemmas*}

lemma [iff]: "¬ P \<turnstile> ⟨[],s⟩ [->] ⟨es',s'⟩"
(*<*)by(blast elim: red_reds.elims)(*>*)

lemma [iff]: "¬ P \<turnstile> ⟨Val v,s⟩ -> ⟨e',s'⟩"
(*<*)by(fastsimp elim: red_reds.elims)(*>*)

lemma [iff]: "¬ P \<turnstile> ⟨Throw a,s⟩ -> ⟨e',s'⟩"
(*<*)by(fastsimp elim: red_reds.elims)(*>*)


lemma red_hext_incr: "P \<turnstile> ⟨e,(h,l)⟩ -> ⟨e',(h',l')⟩  ==> h \<unlhd> h'"
  and reds_hext_incr: "P \<turnstile> ⟨es,(h,l)⟩ [->] ⟨es',(h',l')⟩  ==> h \<unlhd> h'"
(*<*)
proof(induct rule:red_reds_induct)
  case RedNew thus ?case
    by(fastsimp 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 \<turnstile> ⟨e,(h0,l0)⟩ -> ⟨e',(h1,l1)⟩ ==> dom l0 ⊆ dom l1"
and "P \<turnstile> ⟨es,(h0,l0)⟩ [->] ⟨es',(h1,l1)⟩ ==> dom l0 ⊆ dom l1"
(*<*)by(induct rule: red_reds_induct)(auto simp del:fun_upd_apply)(*>*)


lemma red_lcl_add: "P \<turnstile> ⟨e,(h,l)⟩ -> ⟨e',(h',l')⟩ ==> (!!l0. P \<turnstile> ⟨e,(h,l0++l)⟩ -> ⟨e',(h',l0++l')⟩)"
and "P \<turnstile> ⟨es,(h,l)⟩ [->] ⟨es',(h',l')⟩ ==> (!!l0. P \<turnstile> ⟨es,(h,l0++l)⟩ [->] ⟨es',(h',l0++l')⟩)"
(*<*)
proof (induct rule:red_reds_induct)
  case RedCast thus ?case by(fastsimp intro:red_reds.intros)
next
  case RedCastFail thus ?case by(force intro:red_reds.intros)
next
  case RedFAcc thus ?case by(fastsimp intro:red_reds.intros)
next
  case RedCall thus ?case by(fastsimp intro:red_reds.intros)
next
  case (InitBlockRed T V e e' h h' l l' v v' l0)
  have IH: "!!l0. P \<turnstile> ⟨e,(h, l0 ++ l(V \<mapsto> v))⟩ -> ⟨e',(h', l0 ++ l')⟩"
    and l'V: "l' V = Some v'" .
  from IH have IH': "P \<turnstile> ⟨e,(h, (l0 ++ l)(V \<mapsto> v))⟩ -> ⟨e',(h', l0 ++ l')⟩"
    by simp
  have "(l0 ++ l')(V := (l0 ++ l) V) = l0 ++ 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 T V e e' h h' l l' l0)
  have IH: "!!l0. P \<turnstile> ⟨e,(h, l0 ++ l(V := None))⟩ -> ⟨e',(h', l0 ++ l')⟩"
    and l'V: "l' V = None" and unass: "¬ assigned V e" .
  have "l0(V := None) ++ l(V := None) = (l0 ++ l)(V := None)"
    by(simp add:expand_fun_eq map_add_def)
  hence IH': "P \<turnstile> ⟨e,(h, (l0++l)(V := None))⟩ -> ⟨e',(h', l0(V := None) ++ l')⟩"
    using IH[of "l0(V := None)"] by simp
  have "(l0(V := None) ++ l')(V := (l0 ++ l) V) = l0 ++ l'(V := l V)"
    by(simp add:expand_fun_eq map_add_def)
  with red_reds.BlockRedNone[OF IH' _ unass] l'V show ?case
    by(simp add: map_add_def)
next
  case (BlockRedSome T V e e' h h' l l' v l0)
  have IH: "!!l0. P \<turnstile> ⟨e,(h, l0 ++ l(V := None))⟩ -> ⟨e',(h', l0 ++ l')⟩"
    and l'V: "l' V = Some v" and unass: "¬ assigned V e" .
  have "l0(V := None) ++ l(V := None) = (l0 ++ l)(V := None)"
    by(simp add:expand_fun_eq map_add_def)
  hence IH': "P \<turnstile> ⟨e,(h, (l0++l)(V := None))⟩ -> ⟨e',(h', l0(V := None) ++ l')⟩"
    using IH[of "l0(V := None)"] by simp
  have "(l0(V := None) ++ l')(V := (l0 ++ l) V) = l0 ++ l'(V := l V)"
    by(simp add:expand_fun_eq 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(fastsimp 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 \<turnstile> ⟨e,(h,l)⟩ ->* ⟨e',(h',l')⟩" shows "P \<turnstile> ⟨e,(h,l0++l)⟩ ->* ⟨e',(h',l0++l')⟩"
(*<*)
using prems
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
(*>*)


end

lemma 

  [| length vs = length Vs; length Ts = length Vs |]
  ==> fv (blocks (Vs, Ts, vs, e)) = fv e - set Vs

lemmas red_reds_induct: 

  [| !!C FDTs a h h' l.
        [| new_Addr h = ⌊a⌋; P \<turnstile> C has_fields FDTs;
           h' = h(a |-> (C, init_fields FDTs)) |]
        ==> P1 (new C) h l (addr a) h' l;
     !!C h l. new_Addr h = None ==> P1 (new C) h l (THROW OutOfMemory) h l;
     !!C e e' a b aa ba.
        [| red P e (a, b) e' (aa, ba); P1 e a b e' aa ba |]
        ==> P1 (Cast C e) a b (Cast C e') aa ba;
     !!C a b. P1 (Cast C null) a b null a b;
     !!C D a fs aa b.
        [| hp (aa, b) a = ⌊(D, fs)⌋; subcls P D C |]
        ==> P1 (Cast C (addr a)) aa b (addr a) aa b;
     !!C D a fs aa b.
        [| hp (aa, b) a = ⌊(D, fs)⌋; ¬ subcls P D C |]
        ==> P1 (Cast C (addr a)) aa b (THROW ClassCast) aa b;
     !!bop e e' e2 a b aa ba.
        [| red P e (a, b) e' (aa, ba); P1 e a b e' aa ba |]
        ==> P1 (e «bop» e2) a b (e' «bop» e2) aa ba;
     !!bop e e' a b aa ba v1.
        [| red P e (a, b) e' (aa, ba); P1 e a b e' aa ba |]
        ==> P1 (Val v1 «bop» e) a b (Val v1 «bop» e') aa ba;
     !!bop a b v v1 v2.
        binop (bop, v1, v2) = ⌊v⌋ ==> P1 (Val v1 «bop» Val v2) a b (Val v) a b;
     !!V a b v. lcl (a, b) V = ⌊v⌋ ==> P1 (Var V) a b (Val v) a b;
     !!V e e' a b aa ba.
        [| red P e (a, b) e' (aa, ba); P1 e a b e' aa ba |]
        ==> P1 (V:=e) a b (V:=e') aa ba;
     !!V h l v. P1 (V:=Val v) h l unit h (l(V |-> v));
     !!D F e e' a b aa ba.
        [| red P e (a, b) e' (aa, ba); P1 e a b e' aa ba |]
        ==> P1 (e\<bullet>F{D}) a b (e'\<bullet>F{D}) aa ba;
     !!C D F a fs aa b v.
        [| hp (aa, b) a = ⌊(C, fs)⌋; fs (F, D) = ⌊v⌋ |]
        ==> P1 (addr a\<bullet>F{D}) aa b (Val v) aa b;
     !!D F a b. P1 (null\<bullet>F{D}) a b (THROW NullPointer) a b;
     !!D F e e' e2 a b aa ba.
        [| red P e (a, b) e' (aa, ba); P1 e a b e' aa ba |]
        ==> P1 (e\<bullet>F{D} := e2) a b (e'\<bullet>F{D} := e2) aa ba;
     !!D F e e' a b aa ba v.
        [| red P e (a, b) e' (aa, ba); P1 e a b e' aa ba |]
        ==> P1 (Val v\<bullet>F{D} := e) a b (Val v\<bullet>F{D} := e') aa ba;
     !!C D F a fs h l v.
        h a = ⌊(C, fs)⌋
        ==> P1 (addr a\<bullet>F{D} := Val v) h l unit
             (h(a |-> (C, fs((F, D) |-> v)))) l;
     !!D F a b v. P1 (null\<bullet>F{D} := Val v) a b (THROW NullPointer) a b;
     !!M e e' es a b aa ba.
        [| red P e (a, b) e' (aa, ba); P1 e a b e' aa ba |]
        ==> P1 (e\<bullet>M(es)) a b (e'\<bullet>M(es)) aa ba;
     !!M es es' a b aa ba v.
        [| reds P es (a, b) es' (aa, ba); P2 es a b es' aa ba |]
        ==> P1 (Val v\<bullet>M(es)) a b (Val v\<bullet>M(es')) aa ba;
     !!C D M T Ts a body fs pns aa b vs.
        [| hp (aa, b) a = ⌊(C, fs)⌋;
           P \<turnstile> C sees M: Ts->T = (pns, body) in D;
           length vs = length pns; length Ts = length pns |]
        ==> P1 (addr a\<bullet>M(map Val vs)) aa b
             (blocks (this # pns, Class D # Ts, Addr a # vs, body)) aa b;
     !!M a b vs. P1 (null\<bullet>M(map Val vs)) a b (THROW NullPointer) a b;
     !!T V e e' h h' l l'.
        [| red P e (h, l(V := None)) e' (h', l'); P1 e h (l(V := None)) e' h' l';
           l' V = None; ¬ assigned V e |]
        ==> P1 {V:T; e} h l {V:T; e'} h' (l'(V := l V));
     !!T V e e' h h' l l' v.
        [| red P e (h, l(V := None)) e' (h', l'); P1 e h (l(V := None)) e' h' l';
           l' V = ⌊v⌋; ¬ assigned V e |]
        ==> P1 {V:T; e} h l {V:T; V:=Val v;; e'} h' (l'(V := l V));
     !!T V e e' h h' l l' v v'.
        [| red P e (h, l(V |-> v)) e' (h', l'); P1 e h (l(V |-> v)) e' h' l';
           l' V = ⌊v'⌋ |]
        ==> P1 {V:T; V:=Val v;; e} h l {V:T; V:=Val v';; e'} h' (l'(V := l V));
     !!T V a b u. P1 {V:T; Val u} a b (Val u) a b;
     !!T V a b u v. P1 {V:T; V:=Val v;; Val u} a b (Val u) a b;
     !!e e' e2 a b aa ba.
        [| red P e (a, b) e' (aa, ba); P1 e a b e' aa ba |]
        ==> P1 (e;; e2) a b (e';; e2) aa ba;
     !!e2 a b v. P1 (Val v;; e2) a b e2 a b;
     !!e e' e1 e2 a b aa ba.
        [| red P e (a, b) e' (aa, ba); P1 e a b e' aa ba |]
        ==> P1 (if (e) e1 else e2) a b (if (e') e1 else e2) aa ba;
     !!e1 e2 a b. P1 (if (true) e1 else e2) a b e1 a b;
     !!e1 e2 a b. P1 (if (false) e1 else e2) a b e2 a b;
     !!b c a ba. P1 (while (b) c) a ba (if (b) (c;; while (b) c) else unit) a ba;
     !!e e' a b aa ba.
        [| red P e (a, b) e' (aa, ba); P1 e a b e' aa ba |]
        ==> P1 (throw e) a b (throw e') aa ba;
     !!a b. P1 (throw null) a b (THROW NullPointer) a b;
     !!C V e e' e2 a b aa ba.
        [| red P e (a, b) e' (aa, ba); P1 e a b e' aa ba |]
        ==> P1 (try e catch(C V) e2) a b (try e' catch(C V) e2) aa ba;
     !!C V e2 a b v. P1 (try Val v catch(C V) e2) a b (Val v) a b;
     !!C D V a e2 fs aa b.
        [| hp (aa, b) a = ⌊(D, fs)⌋; subcls P D C |]
        ==> P1 (try Throw a catch(C V) e2) aa b {V:Class C; V:=addr a;; e2} aa b;
     !!C D V a e2 fs aa b.
        [| hp (aa, b) a = ⌊(D, fs)⌋; ¬ subcls P D C |]
        ==> P1 (try Throw a catch(C V) e2) aa b (Throw a) aa b;
     !!e e' es a b aa ba.
        [| red P e (a, b) e' (aa, ba); P1 e a b e' aa ba |]
        ==> P2 (e # es) a b (e' # es) aa ba;
     !!es es' a b aa ba v.
        [| reds P es (a, b) es' (aa, ba); P2 es a b es' aa ba |]
        ==> P2 (Val v # es) a b (Val v # es') aa ba;
     !!C e a b. P1 (Cast C (throw e)) a b (throw e) a b;
     !!bop e e2 a b. P1 (throw e «bop» e2) a b (throw e) a b;
     !!bop e a b v1. P1 (Val v1 «bop» throw e) a b (throw e) a b;
     !!V e a b. P1 (V:=throw e) a b (throw e) a b;
     !!D F e a b. P1 (throw e\<bullet>F{D}) a b (throw e) a b;
     !!D F e e2 a b. P1 (throw e\<bullet>F{D} := e2) a b (throw e) a b;
     !!D F e a b v. P1 (Val v\<bullet>F{D} := throw e) a b (throw e) a b;
     !!M e es a b. P1 (throw e\<bullet>M(es)) a b (throw e) a b;
     !!M e es es' a b v vs.
        es = map Val vs @ throw e # es'
        ==> P1 (Val v\<bullet>M(es)) a b (throw e) a b;
     !!T V a aa b. P1 {V:T; Throw a} aa b (Throw a) aa b;
     !!T V a aa b v. P1 {V:T; V:=Val v;; Throw a} aa b (Throw a) aa b;
     !!e e2 a b. P1 (throw e;; e2) a b (throw e) a b;
     !!e e1 e2 a b. P1 (if (throw e) e1 else e2) a b (throw e) a b;
     !!e a b. P1 (throw (throw e)) a b (throw e) a b |]
  ==> (red P xha (xga, xgb) xfa (xea, xeb) --> P1 xha xga xgb xfa xea xeb) &
      (reds P xda (xca, xcb) xba (xaa, xab) --> P2 xda xca xcb xba xaa xab)

lemmas 

  [| red P (V:=e) s e' s'; !!e'a. [| red P e s e'a s'; e' = V:=e'a |] ==> Pa;
     !!h l v. [| s = (h, l); e' = unit; s' = (h, l(V |-> v)); e = Val v |] ==> Pa;
     !!ea. [| e' = throw ea; s' = s; e = throw ea |] ==> Pa |]
  ==> Pa
  [| red P (e1;; e2) s e' s';
     !!e'a. [| red P e1 s e'a s'; e' = e'a;; e2 |] ==> Pa;
     !!v. [| s' = s; e1 = Val v; e2 = e' |] ==> Pa;
     !!e. [| e' = throw e; s' = s; e1 = throw e |] ==> Pa |]
  ==> Pa

The reflexive transitive closure

lemma 

  [| Step P e (h, l) e' (h', l'); !!e h l. R e h l e h l;
     !!e0 h0 l0 e1 h1 l1 e' h' l'.
        [| red P e0 (h0, l0) e1 (h1, l1); R e1 h1 l1 e' h' l' |]
        ==> R e0 h0 l0 e' h' l' |]
  ==> R e h l e' h' l'

Some easy lemmas

lemma 

  (([], s), es', s') ~: reds P

lemma 

  ((Val v, s), e', s') ~: red P

lemma 

  ((Throw a, s), e', s') ~: red P

lemma red_hext_incr: 

  red P e (h, l) e' (h', l') ==> h \<unlhd> h'

and reds_hext_incr: 

  reds P es (h, l) es' (h', l') ==> h \<unlhd> h'

lemma red_lcl_incr: 

  red P e (h0, l0) e' (h1, l1) ==> dom l0 <= dom l1

and 

  reds P es (h0, l0) es' (h1, l1) ==> dom l0 <= dom l1

lemma red_lcl_add: 

  red P e (h, l) e' (h', l') ==> red P e (h, l0 ++ l) e' (h', l0 ++ l')

and 

  reds P es (h, l) es' (h', l') ==> reds P es (h, l0 ++ l) es' (h', l0 ++ l')

lemma 

  Step P e (h, l) e' (h', l') ==> Step P e (h, l0 ++ l) e' (h', l0 ++ l')