Theory SmallStep

(*  Title:      Jinja/J/SmallStep.thy
    ID:         $Id: SmallStep.thy,v 1.7 2007-07-19 21:23:12 makarius Exp $
    Author:     Tobias Nipkow
    Copyright   2003 Technische Universitaet Muenchen
*)

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

theory SmallStep imports Expr State begin

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')"

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"
          ("_ \<turnstile> ((1⟨_,/_⟩) ->/ (1⟨_,/_⟩))" [51,0,0,0,0] 81)
  and reds' :: "J_prog => expr list => state => expr list => state => bool"
          ("_ \<turnstile> ((1⟨_,/_⟩) [->]/ (1⟨_,/_⟩))" [51,0,0,0,0] 81)
  for P :: J_prog
where

  "P \<turnstile> ⟨e,s⟩ -> ⟨e',s'⟩ ≡ ((e,s), e',s') ∈ red P"
| "P \<turnstile> ⟨es,s⟩ [->] ⟨es',s'⟩ ≡ ((es,s), es',s') ∈ reds P"

| 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•F{D}, s⟩ -> ⟨e'•F{D}, s'⟩"

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

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

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

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

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

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

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

| CallParams:
  "P \<turnstile> ⟨es,s⟩ [->] ⟨es',s'⟩ ==>
  P \<turnstile> ⟨(Val v)•M(es),s⟩ -> ⟨(Val v)•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)•M(map Val vs), s⟩ -> ⟨blocks(this#pns, Class D#Ts, Addr a#vs, body), s⟩"

| RedCallNull:
  "P \<turnstile> ⟨null•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)•F{D}, s⟩ -> ⟨throw e, s⟩"
| FAssThrow1: "P \<turnstile> ⟨(throw e)•F{D}:=e2, s⟩ -> ⟨throw e,s⟩"
| FAssThrow2: "P \<turnstile> ⟨Val v•F{D}:=(throw e), s⟩ -> ⟨throw e, s⟩"
| CallThrowObj: "P \<turnstile> ⟨(throw e)•M(es), s⟩ -> ⟨throw e, s⟩"
| CallThrowParams: "[| es = map Val vs @ throw e # es' |] ==> P \<turnstile> ⟨(Val v)•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)]
  and red_reds_inducts = red_reds.inducts [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 *}

abbreviation
  Step :: "J_prog => expr => state => expr => state => bool"
          ("_ \<turnstile> ((1⟨_,/_⟩) ->*/ (1⟨_,/_⟩))" [51,0,0,0,0] 81)
  where "P \<turnstile> ⟨e,s⟩ ->* ⟨e',s'⟩ ≡ ((e,s), e',s') ∈ (red P)*"

abbreviation
  Steps :: "J_prog => expr list => state => expr list => state => bool"
          ("_ \<turnstile> ((1⟨_,/_⟩) [->]*/ (1⟨_,/_⟩))" [51,0,0,0,0] 81)
  where "P \<turnstile> ⟨es,s⟩ [->]* ⟨es',s'⟩ ≡ ((es,s), es',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: reds.cases)(*>*)

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

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


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_inducts)
  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_inducts)(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_inducts)
  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 e h l V v e' h' l' v' T l0)
  have IH: "!!l0. P \<turnstile> ⟨e,(h, l0 ++ l(V \<mapsto> v))⟩ -> ⟨e',(h', l0 ++ l')⟩"
    and l'V: "l' V = Some v'" by fact+
  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 e h l V e' h' l' T 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" by fact+
  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 e h l V e' h' l' v T 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" by fact+
  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