Theory SmallStep

(*  Title:      Jinja/J/SmallStep.thy
    Author:     Tobias Nipkow
    Copyright   2003 Technische Universitaet Muenchen
*)

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:
  "new_Addr h = None 
  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» e2, s  e' «bop» e2, s'"

| BinOpRed2:
  "P  e,s  e',s' 
  P  (Val v1) «bop» e, s  (Val v1) «bop» e', s'"

| RedBinOp:
  "binop(bop,v1,v2) = Some v 
  P  (Val v1) «bop» (Val v2), 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(Vv))"

| FAccRed:
  "P  e,s  e',s' 
  P  eF{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  nullF{D}, s  THROW NullPointer, s"

| FAssRed1:
  "P  e,s  e',s' 
  P  eF{D}:=e2, s  e'F{D}:=e2, s'"

| FAssRed2:
  "P  e,s  e',s' 
  P  Val vF{D}:=e, s  Val vF{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  nullF{D}:=Val v, s  THROW NullPointer, s"

| CallObj:
  "P  e,s  e',s' 
  P  eM(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:TsT = (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  nullM(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(Vv))  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;;e2, s  e';;e2, s'"

| RedSeq:
  "P  (Val v);;e2, s  e2, s"

| CondRed:
  "P  e,s  e',s' 
  P  if (e) e1 else e2, s  if (e') e1 else e2, s'"

| RedCondT:
  "P  if (true) e1 else e2, s  e1, s"

| RedCondF:
  "P  if (false) e1 else e2, s  e2, 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) e2, s  try e' catch(C V) e2, s'"

| RedTry:
  "P  try (Val v) catch(C V) e2, s  Val v, s"

| RedTryCatch:
  " hp s a = Some(D,fs); P  D * C 
   P  try (Throw a) catch(C V) e2, s  {V:Class C := addr a; e2}, s"

| RedTryFail:
  " hp s a = Some(D,fs); ¬ P  D * C 
   P  try (Throw a) catch(C V) e2, 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» e2, s  throw e, s"
| BinOpThrow2: "P  (Val v1) «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}:=e2, s  throw e,s"
| FAssThrow2: "P  Val vF{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);;e2, s  throw e, s"
| CondThrow: "P  if (throw e) e1 else e2, 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 "e0 h0 l0 e1 h1 l1 e' h' l'.
        P  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  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  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 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
    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,(h0,l0)  e',(h1,l1)  dom l0  dom l1"
and "P  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  e,(h,l)  e',(h',l')  (l0. P  e,(h,l0++l)  e',(h',l0++l'))"
and "P  es,(h,l) [→] es',(h',l')  (l0. P  es,(h,l0++l) [→] es',(h',l0++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 l0)
  have IH: "l0. P  e,(h, l0 ++ l(V  v))  e',(h', l0 ++ l')"
    and l'V: "l' V = Some v'" by fact+
  from IH have IH': "P  e,(h, (l0 ++ l)(V  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  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:fun_eq_iff map_add_def)
  hence IH': "P  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: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 e' h' l' v T l0)
  have IH: "l0. P  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:fun_eq_iff map_add_def)
  hence IH': "P  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: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) →* e',(h',l')" shows "P  e,(h,l0++l) →* e',(h',l0++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