# Theory SmallStep

```(*  Title:      Jinja/J/SmallStep.thy
Author:     Tobias Nipkow
*)

section ‹Small Step Semantics›

theory SmallStep
imports Expr State
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
(*>*)

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

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

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

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

| RedNewFail:
P ⊢ ⟨new C, (h,l)⟩ → ⟨THROW OutOfMemory, (h,l)⟩"

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

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

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

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

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

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

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

| RedVar:
"lcl s V = Some v ⟹
P ⊢ ⟨Var V,s⟩ → ⟨Val v,s⟩"

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

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

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

| RedFAcc:
"⟦ hp s a = Some(C,fs); fs(F,D) = Some v ⟧
⟹ P ⊢ ⟨(addr a)∙F{D}, s⟩ → ⟨Val v,s⟩"

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

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

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

| RedFAss:
"h a = Some(C,fs) ⟹
P ⊢ ⟨(addr a)∙F{D}:=(Val v), (h,l)⟩ → ⟨unit, (h(a ↦ (C,fs((F,D) ↦ v))),l)⟩"

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

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

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

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

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

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

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

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

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

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

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

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

| CondRed:
"P ⊢ ⟨e,s⟩ → ⟨e',s'⟩ ⟹
P ⊢ ⟨if (e) e⇩1 else e⇩2, s⟩ → ⟨if (e') e⇩1 else e⇩2, s'⟩"

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

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

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

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

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

| TryRed:
"P ⊢ ⟨e,s⟩ → ⟨e',s'⟩ ⟹
P ⊢ ⟨try e catch(C V) e⇩2, s⟩ → ⟨try e' catch(C V) e⇩2, s'⟩"

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

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

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

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

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

― ‹Exception propagation›

| CastThrow: "P ⊢ ⟨Cast C (throw e), s⟩ → ⟨throw e, s⟩"
| BinOpThrow1: "P ⊢ ⟨(throw e) «bop» e⇩2, s⟩ → ⟨throw e, s⟩"
| BinOpThrow2: "P ⊢ ⟨(Val v⇩1) «bop» (throw e), s⟩ → ⟨throw e, s⟩"
| LAssThrow: "P ⊢ ⟨V:=(throw e), s⟩ → ⟨throw e, s⟩"
| FAccThrow: "P ⊢ ⟨(throw e)∙F{D}, s⟩ → ⟨throw e, s⟩"
| FAssThrow1: "P ⊢ ⟨(throw e)∙F{D}:=e⇩2, s⟩ → ⟨throw e,s⟩"
| FAssThrow2: "P ⊢ ⟨Val v∙F{D}:=(throw e), s⟩ → ⟨throw e, s⟩"
| CallThrowObj: "P ⊢ ⟨(throw e)∙M(es), s⟩ → ⟨throw e, s⟩"
| CallThrowParams: "⟦ es = map Val vs @ throw e # es' ⟧ ⟹ P ⊢ ⟨(Val v)∙M(es), s⟩ → ⟨throw e, s⟩"
| BlockThrow: "P ⊢ ⟨{V:T; Throw a}, s⟩ → ⟨Throw a, s⟩"
| InitBlockThrow: "P ⊢ ⟨{V:T := Val v; Throw a}, s⟩ → ⟨Throw a, s⟩"
| SeqThrow: "P ⊢ ⟨(throw e);;e⇩2, s⟩ → ⟨throw e, s⟩"
| CondThrow: "P ⊢ ⟨if (throw e) e⇩1 else e⇩2, s⟩ → ⟨throw e, s⟩"
| ThrowThrow: "P ⊢ ⟨throw(throw e), s⟩ → ⟨throw e, s⟩"
(*<*)
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⟩ → ⟨e',s'⟩"
"P ⊢ ⟨e1;;e2,s⟩ → ⟨e',s'⟩"
(*>*)

subsection‹The reflexive transitive closure›

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

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

lemma converse_rtrancl_induct_red[consumes 1]:
assumes "P ⊢ ⟨e,(h,l)⟩ →* ⟨e',(h',l')⟩"
and "⋀e h l. R e h l e h l"
and "⋀e⇩0 h⇩0 l⇩0 e⇩1 h⇩1 l⇩1 e' h' l'.
⟦ P ⊢ ⟨e⇩0,(h⇩0,l⇩0)⟩ → ⟨e⇩1,(h⇩1,l⇩1)⟩; R e⇩1 h⇩1 l⇩1 e' h' l' ⟧ ⟹ R e⇩0 h⇩0 l⇩0 e' h' l'"
shows "R e h l e' h' l'"
(*<*)
proof -
{ fix s s'
assume reds: "P ⊢ ⟨e,s⟩ →* ⟨e',s'⟩"
and base: "⋀e s. R e (hp s) (lcl s) e (hp s) (lcl s)"
and red⇩1: "⋀e⇩0 s⇩0 e⇩1 s⇩1 e' s'.
⟦ P ⊢ ⟨e⇩0,s⇩0⟩ → ⟨e⇩1,s⇩1⟩; R e⇩1 (hp s⇩1) (lcl s⇩1) e' (hp s') (lcl s') ⟧
⟹ R e⇩0 (hp s⇩0) (lcl s⇩0) 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 e⇩0 s⇩0 e s)
thus ?case by(blast intro:red⇩1)
qed
}
with assms show ?thesis by fastforce
qed
(*>*)

subsection‹Some easy lemmas›

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

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

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

lemma red_hext_incr: "P ⊢ ⟨e,(h,l)⟩ → ⟨e',(h',l')⟩  ⟹ h ⊴ h'"
and reds_hext_incr: "P ⊢ ⟨es,(h,l)⟩ [→] ⟨es',(h',l')⟩  ⟹ h ⊴ h'"
(*<*)
proof(induct rule:red_reds_inducts)
case RedNew thus ?case
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)⟩ → ⟨e',(h⇩1,l⇩1)⟩ ⟹ dom l⇩0 ⊆ dom l⇩1"
and "P ⊢ ⟨es,(h⇩0,l⇩0)⟩ [→] ⟨es',(h⇩1,l⇩1)⟩ ⟹ 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)⟩ → ⟨e',(h',l')⟩ ⟹ (⋀l⇩0. P ⊢ ⟨e,(h,l⇩0++l)⟩ → ⟨e',(h',l⇩0++l')⟩)"
and "P ⊢ ⟨es,(h,l)⟩ [→] ⟨es',(h',l')⟩ ⟹ (⋀l⇩0. P ⊢ ⟨es,(h,l⇩0++l)⟩ [→] ⟨es',(h',l⇩0++l')⟩)"
(*<*)
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 e' h' l' v' T l⇩0)
have IH: "⋀l⇩0. P ⊢ ⟨e,(h, l⇩0 ++ l(V ↦ v))⟩ → ⟨e',(h', l⇩0 ++ l')⟩"
and l'V: "l' V = Some v'" by fact+
from IH have IH': "P ⊢ ⟨e,(h, (l⇩0 ++ l)(V ↦ v))⟩ → ⟨e',(h', l⇩0 ++ l')⟩"
by simp
have "(l⇩0 ++ l')(V := (l⇩0 ++ l) V) = l⇩0 ++ l'(V := l V)"
with red_reds.InitBlockRed[OF IH'] l'V show ?case by(simp del:fun_upd_apply)
next
case (BlockRedNone e h l V e' h' l' T l⇩0)
have IH: "⋀l⇩0. P ⊢ ⟨e,(h, l⇩0 ++ l(V := None))⟩ → ⟨e',(h', l⇩0 ++ l')⟩"
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)"
hence IH': "P ⊢ ⟨e,(h, (l⇩0++l)(V := None))⟩ → ⟨e',(h', l⇩0(V := None) ++ l')⟩"
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)"
with red_reds.BlockRedNone[OF IH' _ unass] l'V show ?case
next
case (BlockRedSome e h l V e' h' l' v T l⇩0)
have IH: "⋀l⇩0. P ⊢ ⟨e,(h, l⇩0 ++ l(V := None))⟩ → ⟨e',(h', l⇩0 ++ l')⟩"
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)"
hence IH': "P ⊢ ⟨e,(h, (l⇩0++l)(V := None))⟩ → ⟨e',(h', l⇩0(V := None) ++ l')⟩"
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)"
with red_reds.BlockRedSome[OF IH' _ unass] l'V show ?case
next
case RedTryCatch thus ?case by(fastforce intro:red_reds.intros)
next
case RedTryFail thus ?case by(force intro!:red_reds.intros)
(*>*)

assumes "P ⊢ ⟨e,(h,l)⟩ →* ⟨e',(h',l')⟩" shows "P ⊢ ⟨e,(h,l⇩0++l)⟩ →* ⟨e',(h',l⇩0++l')⟩"
(*<*)
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
(*>*)

end
```