Theory SmallStep

(*  Title:      JinjaThreads/J/SmallStep.thy
    Author:     Tobias Nipkow, Andreas Lochbihler
*)

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

theory SmallStep imports
  Expr
  State
  "../Common/ExternalCall"
begin

consts blocks :: "'a list * ty list * val list * ('a,'b) exp => ('a,'b) exp"
recdef blocks "measure(λ(Vs,Ts,vs,e). size Vs)"
 "blocks(V#Vs, T#Ts, v#vs, e) = {V:T=⌊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
(*>*)

lemma expr_locks_blocks:
  "[| length vs = length pns; length Ts = length pns |]
  ==> expr_locks (blocks (pns, Ts, vs, e)) = expr_locks e"
by(induct pns Ts vs e rule: blocks.induct)(auto)

types
  J_thread_action = "(addr,thread_id,expr × locals,heap,addr,obs_event option) thread_action"

translations
  "J_thread_action" <= (type) "(nat,nat,expr × (message_string \<rightharpoonup> val),heap,nat,obs_event option) thread_action"

definition extNTA2J :: "J_prog => (cname × mname × addr) => expr × locals"
where "extNTA2J P = (λ(C, M, a). let (D,Ts,T,pns,body) = method P C M
                                 in ({this:Class D=⌊Addr a⌋; body}, empty))"

lemma extNTA2J_iff [simp]:
  "extNTA2J P (C, M, a) = ({this:Class (fst (method P C M))=⌊Addr a⌋; snd (snd (snd (snd (method P C M))))}, empty)"
by(simp add: extNTA2J_def split_beta)

abbreviation extTA2J :: "J_prog => external_thread_action => J_thread_action"
where "extTA2J P ≡ convert_extTA (extNTA2J P)"

primrec extRet2J :: "val + addr => ('a, 'b) exp"
where
  "extRet2J (Inl v) = Val v"
| "extRet2J (Inr a) = Throw a"

text{* Locking mechanism:
  The expression on which the thread is synchronized is evaluated first to a value.
  If this expression evaluates to null, a null pointer expression is thrown.
  If this expression evaluates to an address, a lock must be obtained on this address, the
  sync expression is rewritten to insync.
  For insync expressions, the body expression may be evaluated.
  If the body expression is only a value or a thrown exception, the lock is released and
  the synchronized expression reduces to the body's expression. This is the normal Java semantics,
  not the one as presented in LNCS 1523, Cenciarelli/Knapp/Reus/Wirsing. There
  the expression on which the thread synchronized is evaluated except for the last step.
  If the thread can obtain the lock on the object immediately after the last evaluation step, the evaluation is
  done and the lock acquired. If the lock cannot be obtained, the evaluation step is discarded. If another thread
  changes the evaluation result of this last step, the thread then will try to synchronize on the new object. *}

inductive red :: "(external_thread_action => (addr,thread_id,'x,heap,addr,obs_event option) thread_action) => J_prog => 
                 expr => (heap × locals) => (addr,thread_id,'x,heap,addr,obs_event option) thread_action => expr => (heap × locals) => bool"
                ("_,_ \<turnstile> ((1⟨_,/_⟩) -_->/ (1⟨_,/_⟩))" [51,51,0,0,0,0,0] 81)
 and reds ::  "(external_thread_action => (addr,thread_id,'x,heap,addr,obs_event option) thread_action) => J_prog =>
                 expr list => (heap × locals) => (addr,thread_id,'x,heap,addr,obs_event option) thread_action => expr list => (heap × locals) => bool"
               ("_,_ \<turnstile> ((1⟨_,/_⟩) [-_->]/ (1⟨_,/_⟩))" [51,51,0,0,0,0,0] 81)
for extTA :: "external_thread_action => (addr,thread_id,'x,heap,addr,obs_event option) thread_action" and P :: J_prog
where
  RedNew:
  "[| new_Addr h = Some a; P \<turnstile> C has_fields FDTs; h' = h(a\<mapsto>(Obj C (init_fields FDTs))) |]
  ==> extTA,P \<turnstile> ⟨new C, (h, l)⟩ -ε-> ⟨addr a, (h', l)⟩"

| RedNewFail:
  "new_Addr (hp s) = None ==>
  extTA,P \<turnstile> ⟨new C, s⟩ -ε-> ⟨THROW OutOfMemory, s⟩"

| NewArrayRed:
  "extTA,P \<turnstile> ⟨e, s⟩ -ta-> ⟨e', s'⟩ ==> extTA,P \<turnstile> ⟨newA T⌊e⌉, s⟩ -ta-> ⟨newA T⌊e'⌉, s'⟩"

| RedNewArray:
  "[| new_Addr h = Some a; i ≥ 0; h' = h(a \<mapsto> (Arr T (replicate (nat i) (default_val T)))) |]
  ==> extTA,P \<turnstile> ⟨newA T⌊Val (Intg i)⌉, (h, l)⟩ -ε-> ⟨addr a, (h', l)⟩"

| RedNewArrayNegative:
  "i < 0 ==> extTA,P \<turnstile> ⟨newA T⌊Val (Intg i)⌉, s⟩ -ε-> ⟨THROW NegativeArraySize, s⟩"

| RedNewArrayFail:
  "[| new_Addr h = None; i ≥ 0 |]
  ==> extTA,P \<turnstile> ⟨newA T⌊Val (Intg i)⌉, (h, l)⟩ -ε-> ⟨THROW OutOfMemory, (h, l)⟩"

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

| RedCast:
 "[| typeofhp s v = ⌊U⌋; P \<turnstile> U ≤ T |]
  ==> extTA,P \<turnstile> ⟨Cast T (Val v), s⟩ -ε-> ⟨Val v, s⟩"

| RedCastFail:
  "[| typeofhp s v = ⌊U⌋; ¬ P \<turnstile> U ≤ T |]
  ==> extTA,P \<turnstile> ⟨Cast T (Val v), s⟩ -ε-> ⟨THROW ClassCast, s⟩"

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

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

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

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

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

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

| AAccRed1:
  "extTA,P \<turnstile> ⟨a, s⟩ -ta-> ⟨a', s'⟩ ==> extTA,P \<turnstile> ⟨a⌊i⌉, s⟩ -ta-> ⟨a'⌊i⌉, s'⟩"

| AAccRed2:
  "extTA,P \<turnstile> ⟨i, s⟩ -ta-> ⟨i', s'⟩ ==> extTA,P \<turnstile> ⟨(Val a)⌊i⌉, s⟩ -ta-> ⟨(Val a)⌊i'⌉, s'⟩"

| RedAAccNull:
  "extTA,P \<turnstile> ⟨null⌊Val i⌉, s⟩ -ε-> ⟨THROW NullPointer, s⟩"

| RedAAccBounds:
  "[| hp s a = Some(Arr T el); i < 0 ∨ i ≥ int (length el) |]
  ==> extTA,P \<turnstile> ⟨(addr a)⌊Val (Intg i)⌉, s⟩ -ε-> ⟨THROW ArrayIndexOutOfBounds, s⟩"

| RedAAcc:
  "[| hp s a = Some(Arr T el); i ≥ 0; i < int (length el) |]
  ==> extTA,P \<turnstile> ⟨(addr a)⌊Val (Intg i)⌉, s⟩ -ε-> ⟨Val (el ! nat i), s⟩"

| AAssRed1:
  "extTA,P \<turnstile> ⟨a, s⟩ -ta-> ⟨a', s'⟩ ==> extTA,P \<turnstile> ⟨a⌊i⌉ := e, s⟩ -ta-> ⟨a'⌊i⌉ := e, s'⟩"

| AAssRed2:
  "extTA,P \<turnstile> ⟨i, s⟩ -ta-> ⟨i', s'⟩ ==> extTA,P \<turnstile> ⟨(Val a)⌊i⌉ := e, s⟩ -ta-> ⟨(Val a)⌊i'⌉ := e, s'⟩"

| AAssRed3:
  "extTA,P \<turnstile> ⟨(e::expr), s⟩ -ta-> ⟨e', s'⟩ ==> extTA,P \<turnstile> ⟨(Val a)⌊Val i⌉ := e, s⟩ -ta-> ⟨(Val a)⌊Val i⌉ := e', s'⟩"

| RedAAssNull:
  "extTA,P \<turnstile> ⟨null⌊Val i⌉ := (Val e::expr), s⟩ -ε-> ⟨THROW NullPointer, s⟩"

| RedAAssBounds:
  "[| hp s a = Some(Arr T el); i < 0 ∨ i ≥ int (length el) |]
  ==> extTA,P \<turnstile> ⟨(addr a)⌊Val (Intg i)⌉ := (Val e::expr), s⟩ -ε-> ⟨THROW ArrayIndexOutOfBounds, s⟩"

| RedAAssStore:
  "[| hp s a = Some(Arr T el); i ≥ 0; i < int (length el); typeofhp s w = ⌊U⌋; ¬ (P \<turnstile> U ≤ T) |]
  ==> extTA,P \<turnstile> ⟨(addr a)⌊Val (Intg i)⌉ := (Val w::expr), s⟩ -ε-> ⟨THROW ArrayStore, s⟩"

| RedAAss:
  "[| h a = Some(Arr T el); i ≥ 0; i < int (length el); typeofh w = Some U; P \<turnstile> U ≤ T;
    h' = h(a \<mapsto> (Arr T (el[nat i := w]))) |]
  ==> extTA,P \<turnstile> ⟨(addr a)⌊Val (Intg i)⌉ := Val w::expr, (h, l)⟩ -ε-> ⟨unit, (h', l)⟩"

| ALengthRed:
  "extTA,P \<turnstile> ⟨a, s⟩ -ta-> ⟨a', s'⟩ ==> extTA,P \<turnstile> ⟨a•length, s⟩ -ta-> ⟨a'•length, s'⟩"

| RedALength:
  "hp s a = ⌊Arr T el⌋ ==> extTA,P \<turnstile> ⟨addr a•length, s⟩ -ε-> ⟨Val (Intg (int (length el))), s⟩"

| RedALengthNull:
  "extTA,P \<turnstile> ⟨null•length, s⟩ -ε-> ⟨THROW NullPointer, s⟩"

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

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

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

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

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

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

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

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

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

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

| RedCallExternal:
  "[| typeofhp s (Addr a) = ⌊T⌋; is_external_call P T M; P \<turnstile> ⟨a•M(vs), hp s⟩ -ta->ext ⟨va, h'⟩;
     ta' = extTA ta; e' = extRet2J va; s' = (h', lcl s) |]
  ==> extTA,P \<turnstile> ⟨(addr a)•M(map Val vs), s⟩ -ta'-> ⟨e', s'⟩"

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

| BlockRed:
  "extTA,P \<turnstile> ⟨e, (h, l(V:=vo))⟩ -ta-> ⟨e', (h', l')⟩
  ==> extTA,P \<turnstile> ⟨{V:T=vo; e}, (h, l)⟩ -ta-> ⟨{V:T=l' V; e'}, (h', l'(V := l V))⟩"

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

| SynchronizedRed1:
  "extTA,P \<turnstile> ⟨o', s⟩ -ta-> ⟨o'', s'⟩ ==> extTA,P \<turnstile> ⟨sync(o') e, s⟩ -ta-> ⟨sync(o'') e, s'⟩"

| SynchronizedNull:
  "extTA,P \<turnstile> ⟨sync(null) e, s⟩ -ε-> ⟨THROW NullPointer, s⟩"

| LockSynchronized:
  "hp s a = ⌊arrobj⌋ ==> extTA,P \<turnstile> ⟨sync(addr a) e, s⟩ -ε\<lbrace>l Lock->a \<rbrace>\<lbrace>oSynchronization a\<rbrace>-> ⟨insync(a) e, s⟩"

| SynchronizedRed2:
  "extTA,P \<turnstile> ⟨e, s⟩ -ta-> ⟨e', s'⟩ ==> extTA,P \<turnstile> ⟨insync(a) e, s⟩ -ta-> ⟨insync(a) e', s'⟩"

| UnlockSynchronized:
  "extTA,P \<turnstile> ⟨insync(a) (Val v), s⟩ -ε\<lbrace>l Unlock->a \<rbrace>\<lbrace>oSynchronization a\<rbrace>-> ⟨Val v, s⟩"

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

| RedSeq:
  "extTA,P \<turnstile> ⟨(Val v);;e, s⟩ -ε-> ⟨e, s⟩"

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

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

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

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

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

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

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

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

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

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

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

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

-- "Exception propagation"

| NewArrayThrow: "extTA,P \<turnstile> ⟨newA T⌊Throw a⌉, s⟩ -ε-> ⟨Throw a, s⟩"
| CastThrow: "extTA,P \<turnstile> ⟨Cast C (Throw a), s⟩ -ε-> ⟨Throw a, s⟩"
| BinOpThrow1: "extTA,P \<turnstile> ⟨(Throw a) «bop» e2, s⟩ -ε-> ⟨Throw a, s⟩"
| BinOpThrow2: "extTA,P \<turnstile> ⟨(Val v1) «bop» (Throw a), s⟩ -ε-> ⟨Throw a, s⟩"
| LAssThrow: "extTA,P \<turnstile> ⟨V:=(Throw a), s⟩ -ε-> ⟨Throw a, s⟩"
| AAccThrow1: "extTA,P \<turnstile> ⟨(Throw a)⌊i⌉, s⟩ -ε-> ⟨Throw a, s⟩"
| AAccThrow2: "extTA,P \<turnstile> ⟨(Val v)⌊Throw a⌉, s⟩ -ε-> ⟨Throw a, s⟩"
| AAssThrow1: "extTA,P \<turnstile> ⟨(Throw a)⌊i⌉ := e, s⟩ -ε-> ⟨Throw a, s⟩"
| AAssThrow2: "extTA,P \<turnstile> ⟨(Val v)⌊Throw a⌉ := e, s⟩ -ε-> ⟨Throw a, s⟩"
| AAssThrow3: "extTA,P \<turnstile> ⟨(Val v)⌊Val i⌉ := Throw a :: expr, s⟩ -ε-> ⟨Throw a, s⟩"
| ALengthThrow: "extTA,P \<turnstile> ⟨(Throw a)•length, s⟩ -ε-> ⟨Throw a, s⟩"
| FAccThrow: "extTA,P \<turnstile> ⟨(Throw a)•F{D}, s⟩ -ε-> ⟨Throw a, s⟩"
| FAssThrow1: "extTA,P \<turnstile> ⟨(Throw a)•F{D}:=e2, s⟩ -ε-> ⟨Throw a, s⟩"
| FAssThrow2: "extTA,P \<turnstile> ⟨Val v•F{D}:=(Throw a::expr), s⟩ -ε-> ⟨Throw a, s⟩"
| CallThrowObj: "extTA,P \<turnstile> ⟨(Throw a)•M(es), s⟩ -ε-> ⟨Throw a, s⟩"
| CallThrowParams: "[| es = map Val vs @ Throw a # es' |] ==> extTA,P \<turnstile> ⟨(Val v)•M(es), s⟩ -ε-> ⟨Throw a, s⟩"
| BlockThrow: "extTA,P \<turnstile> ⟨{V:T=vo; Throw a}, s⟩ -ε-> ⟨Throw a, s⟩"
| SynchronizedThrow1: "extTA,P \<turnstile> ⟨sync(Throw a) e, s⟩ -ε-> ⟨Throw a, s⟩"
| SynchronizedThrow2: "extTA,P \<turnstile> ⟨insync(a) Throw ad, s⟩ -ε\<lbrace>l Unlock->a \<rbrace>\<lbrace>oSynchronization a\<rbrace>-> ⟨Throw ad, s⟩"
| SeqThrow: "extTA,P \<turnstile> ⟨(Throw a);;e2, s⟩ -ε-> ⟨Throw a, s⟩"
| CondThrow: "extTA,P \<turnstile> ⟨if (Throw a) e1 else e2, s⟩ -ε-> ⟨Throw a, s⟩"
| ThrowThrow: "extTA,P \<turnstile> ⟨throw(Throw a), s⟩ -ε-> ⟨Throw a, s⟩"

inductive_cases red_cases:
  "extTA,P \<turnstile> ⟨new C, s⟩ -ta-> ⟨e', s'⟩"
  "extTA,P \<turnstile> ⟨newA T⌊e⌉, s⟩ -ta-> ⟨e', s'⟩"
  "extTA,P \<turnstile> ⟨Cast T e, s⟩ -ta-> ⟨e', s'⟩"
  "extTA,P \<turnstile> ⟨e «bop» e', s⟩ -ta-> ⟨e'', s'⟩"
  "extTA,P \<turnstile> ⟨Var V, s⟩ -ta-> ⟨e', s'⟩"
  "extTA,P \<turnstile> ⟨V:=e, s⟩ -ta-> ⟨e', s'⟩"
  "extTA,P \<turnstile> ⟨a⌊i⌉, s⟩ -ta-> ⟨e', s'⟩"
  "extTA,P \<turnstile> ⟨a⌊i⌉ := e, s⟩ -ta-> ⟨e', s'⟩"
  "extTA,P \<turnstile> ⟨a•length, s⟩ -ta-> ⟨e', s'⟩"
  "extTA,P \<turnstile> ⟨e•F{D}, s⟩ -ta-> ⟨e', s'⟩"
  "extTA,P \<turnstile> ⟨e•F{D} := e', s⟩ -ta-> ⟨e'', s'⟩"
  "extTA,P \<turnstile> ⟨e•M(es), s⟩ -ta-> ⟨e', s'⟩"
  "extTA,P \<turnstile> ⟨{V:T=vo; e}, s⟩ -ta-> ⟨e', s'⟩"
  "extTA,P \<turnstile> ⟨sync(o') e, s⟩ -ta-> ⟨e', s'⟩"
  "extTA,P \<turnstile> ⟨insync(a) e, s⟩ -ta-> ⟨e', s'⟩"
  "extTA,P \<turnstile> ⟨e;;e', s⟩ -ta-> ⟨e'', s'⟩"
  "extTA,P \<turnstile> ⟨if (b) e1 else e2, s ⟩ -ta-> ⟨e', s'⟩"
  "extTA,P \<turnstile> ⟨while (b) e, s ⟩ -ta-> ⟨e', s'⟩"
  "extTA,P \<turnstile> ⟨throw e, s ⟩ -ta-> ⟨e', s'⟩"
  "extTA,P \<turnstile> ⟨try e catch(C V) e', s⟩ -ta-> ⟨e'', s'⟩"

inductive_cases reds_cases:
  "extTA,P \<turnstile> ⟨e # es, s⟩ [-ta->] ⟨es', s'⟩"


abbreviation red' :: "J_prog => expr => (heap × locals) => J_thread_action => expr => (heap × locals) => bool"
                ("_ \<turnstile> ((1⟨_,/_⟩) -_->/ (1⟨_,/_⟩))" [51,0,0,0,0,0] 81)
where "red' P ≡ red (extTA2J P) P"

abbreviation reds' :: "J_prog => expr list => (heap × locals) => J_thread_action => expr list => (heap × locals) => bool"
               ("_ \<turnstile> ((1⟨_,/_⟩) [-_->]/ (1⟨_,/_⟩))" [51,0,0,0,0,0] 81)
where "reds' P ≡ reds (extTA2J P) P"

subsection{* The reflexive transitive closure *}

abbreviation
  Step :: "(external_thread_action => (addr,thread_id,'x,heap,addr,obs_event option) thread_action) => J_prog =>
           expr => (heap × locals) => ((addr,thread_id,'x,heap,addr,obs_event option) thread_action) list =>
           expr => (heap × locals) => bool"
          ("_,_ \<turnstile> ((1⟨_,/_⟩) -_->*/ (1⟨_,/_⟩))" [51,51,0,0,0,0,0] 81)
where
  "extTA,P \<turnstile> ⟨e, s⟩ -ta->* ⟨e', s'⟩ == rtrancl3p (λ(e, s) ta (e', s'). extTA,P \<turnstile> ⟨e, s⟩ -ta-> ⟨e', s'⟩) (e,s) ta (e',s')"

lemmas Step_induct = rtrancl3p.induct[where r = "λ(e, s) ta (e', s'). extTA,P \<turnstile> ⟨e, s⟩ -ta-> ⟨e', s'⟩", split_format (complete), simplified, consumes 1, case_names refl step]

subsection{*Some easy lemmas*}

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

lemma red_no_val [dest]:
  "[| extTA,P \<turnstile> ⟨e, s⟩ -tas-> ⟨e', s'⟩; is_val e |] ==> False"
by(auto)


lemma [iff]: "¬ extTA,P \<turnstile> ⟨Throw a, s⟩ -ta-> ⟨e', s'⟩"
by(fastsimp elim: red_cases)

lemma reds_preserves_len:
  "extTA,P \<turnstile> ⟨es, s⟩ [-ta->] ⟨es', s'⟩ ==> length es' = length es"
by(induct es arbitrary: es')(auto elim: reds.cases)

lemma red_hext_incr: "extTA,P \<turnstile> ⟨e, s⟩ -ta-> ⟨e', s'⟩ ==> hp s \<unlhd> hp s'"
  and reds_hext_incr: "extTA,P \<turnstile> ⟨es, s⟩ [-ta->] ⟨es', s'⟩ ==> hp s \<unlhd> hp s'"
proof(induct rule:red_reds.inducts)
  case (RedNew C FDTs a h h' l) thus ?case by(auto dest: new_Addr_SomeD intro: hext_new simp del: fun_upd_apply)
next
  case RedNewArray thus ?case by(auto dest: new_Addr_SomeD intro: hext_new simp del: fun_upd_apply)
next
  case RedAAss thus ?case by(fastsimp dest:new_Addr_SomeD simp:hext_def split:if_splits)
next
  case RedFAss thus ?case by(fastsimp simp add:hext_def split:if_splits)
next
  case RedCallExternal thus ?case by(auto intro: red_external_hext)
qed fastsimp+

lemma red_lcl_incr: "extTA,P \<turnstile> ⟨e, s⟩ -ta-> ⟨e', s'⟩ ==> dom (lcl s) ⊆ dom (lcl s')"
  and reds_lcl_incr: "extTA,P \<turnstile> ⟨es, s⟩ [-ta->] ⟨es', s'⟩ ==> dom (lcl s) ⊆ dom (lcl s')"
apply(induct rule:red_reds.inducts)
apply(auto simp del: fun_upd_apply split: split_if_asm)
done

lemma red_lcl_add_aux:
  "extTA,P \<turnstile> ⟨e, s⟩ -ta-> ⟨e', s'⟩ ==> extTA,P \<turnstile> ⟨e, (hp s, l0 ++ lcl s)⟩ -ta-> ⟨e', (hp s', l0 ++ lcl s')⟩"
  and reds_lcl_add_aux:
  "extTA,P \<turnstile> ⟨es, s⟩ [-ta->] ⟨es', s'⟩ ==> extTA,P \<turnstile> ⟨es, (hp s, l0 ++ lcl s)⟩ [-ta->] ⟨es', (hp s', l0 ++ lcl s')⟩"
proof (induct arbitrary: l0 and l0 rule:red_reds.inducts)
  case (BlockRed e h x V vo ta e' h' x' T)
  note IH = `!!l0. extTA,P \<turnstile> ⟨e,(hp (h, x(V := vo)), l0 ++ lcl (h, x(V := vo)))⟩ -ta-> ⟨e',(hp (h', x'), l0 ++ lcl (h', x'))⟩`[simplified]
  have lrew: "!!x x'. x(V := vo) ++ x'(V := vo) = (x ++ x')(V := vo)" 
    by(simp add:expand_fun_eq map_add_def)
  have lrew1: "!!X X' X'' vo. (X(V := vo) ++ X')(V := (X ++ X'') V) = X ++ X'(V := X'' V)"
    by(simp add: expand_fun_eq map_add_def)
  have lrew2: "!!X X'. (X(V := None) ++ X') V = X' V"
    by(simp add: map_add_def) 
  show ?case
  proof(cases vo)
    case None
    from IH[of "l0(V := vo)"]
    show ?thesis
      apply(simp del: fun_upd_apply add: lrew)
      apply(drule red_reds.BlockRed)
      by(simp only: lrew1 None lrew2)
  next
    case (Some v)
    with `extTA,P \<turnstile> ⟨e,(h, x(V := vo))⟩ -ta-> ⟨e',(h', x')⟩`
    have "x' V ≠ None"
      by -(drule red_lcl_incr, auto split: split_if_asm)
    with IH[of "l0(V := vo)"]
    show ?thesis
      apply(clarsimp simp del: fun_upd_apply simp add: lrew)
      apply(drule red_reds.BlockRed)
      by(simp add: lrew1 Some del: fun_upd_apply)
  qed
next
  case (RedTryFail s a D fs C V e2 l0) thus ?case
    by(auto intro: red_reds.RedTryFail)
qed(fastsimp intro:red_reds.intros simp del: fun_upd_apply)+

lemma red_lcl_add: "extTA,P \<turnstile> ⟨e, (h, l)⟩ -ta-> ⟨e', (h', l')⟩ ==> extTA,P \<turnstile> ⟨e, (h, l0 ++ l)⟩ -ta-> ⟨e', (h', l0 ++ l')⟩"
  and reds_lcl_add: "extTA,P \<turnstile> ⟨es, (h, l)⟩ [-ta->] ⟨es', (h', l')⟩ ==> extTA,P \<turnstile> ⟨es, (h, l0 ++ l)⟩ [-ta->] ⟨es', (h', l0 ++ l')⟩"
by(auto dest:red_lcl_add_aux reds_lcl_add_aux)

lemma Step_lcl_add:
  "extTA,P \<turnstile> ⟨e, (h, l)⟩ -ta->* ⟨e', (h', l')⟩ ==> extTA,P \<turnstile> ⟨e, (h, l0 ++ l)⟩ -ta->* ⟨e', (h', l0 ++ l')⟩"
proof(induct rule: Step_induct)
  case refl thus ?case by(auto intro: rtrancl3p.intros)
next
  case (step e h l ta e' h' l' las tas cas was obs e'' h'' l'')
  have IH: "extTA,P \<turnstile> ⟨e,(h, l0 ++ l)⟩ -ta->* ⟨e',(h', l0 ++ l')⟩"
   and red: "extTA,P \<turnstile> ⟨e',(h', l')⟩ -(las, tas, cas, was, obs)-> ⟨e'',(h'', l'')⟩" by fact+
  from red have "extTA,P \<turnstile> ⟨e',(h', l0 ++ l')⟩ -(las, tas, cas, was, obs)-> ⟨e'',(h'', l0 ++ l'')⟩" by(rule red_lcl_add)
  with IH show ?case by(auto elim: rtrancl3p_step)
qed

lemma reds_no_val [dest]:
  "[| extTA,P \<turnstile> ⟨es, s⟩ [-ta->] ⟨es', s'⟩; is_vals es |] ==> False"
apply(induct es arbitrary: s ta es' s')
 apply(blast elim: reds.cases)
apply(erule reds.cases)
apply(auto, blast)
done

lemma red_no_Throw [dest!]:
  "extTA,P \<turnstile> ⟨Throw a, s⟩ -ta-> ⟨e', s'⟩ ==> False"
by(auto elim!: red_cases)

lemma red_lcl_sub:
  "[| extTA,P \<turnstile> ⟨e, s⟩ -ta-> ⟨e', s'⟩; fv e ⊆ W |] ==> extTA,P \<turnstile> ⟨e, (hp s, (lcl s)|`W)⟩ -ta-> ⟨e', (hp s', (lcl s')|`W)⟩"

  and reds_lcl_sub:
  "[| extTA,P \<turnstile> ⟨es, s⟩ [-ta->] ⟨es', s'⟩; fvs es ⊆ W |] ==> extTA,P \<turnstile> ⟨es, (hp s, (lcl s)|`W)⟩ [-ta->] ⟨es', (hp s', (lcl s')|`W)⟩"
proof(induct arbitrary: W and W rule: red_reds.inducts)
  case (RedLAss V v h l W)
  have "extTA,P \<turnstile> ⟨V:=Val v,(h, l |` W)⟩ -ε-> ⟨unit,(h, (l |`W)(V \<mapsto> v))⟩"
    by(rule red_reds.RedLAss)
  with RedLAss show ?case by(simp del: fun_upd_apply)
next
  case (BlockRed e h x V vo ta e' h' x' T)
  have IH: "!!W. fv e ⊆ W ==> extTA,P \<turnstile> ⟨e,(hp (h, x(V := vo)), lcl (h, x(V := vo)) |` W)⟩ -ta-> ⟨e',(hp (h', x'), lcl (h', x') |` W)⟩" by fact
  from `fv {V:T=vo; e} ⊆ W` have fve: "fv e ⊆ insert V W" by auto
  show ?case
  proof(cases "V ∈ W")
    case True
    with fve have "fv e ⊆ W" by auto
    from True IH[OF this] have "extTA,P \<turnstile> ⟨e,(h, (x |` W )(V := vo))⟩ -ta-> ⟨e',(h', x' |` W)⟩" by(simp)
    with True have "extTA,P \<turnstile> ⟨{V:T=vo; e},(h, x |` W)⟩ -ta-> ⟨{V:T=x' V; e'},(h', (x' |` W)(V := x V))⟩"
      by -(drule red_reds.BlockRed[where T=T], simp)
    with True show ?thesis by(simp del: fun_upd_apply)
  next
    case False
    with IH[OF fve] have "extTA,P \<turnstile> ⟨e,(h, (x |` W)(V := vo))⟩ -ta-> ⟨e',(h', x' |` insert V W)⟩" by(simp)
    with False have "extTA,P \<turnstile> ⟨{V:T=vo; e},(h, x |` W)⟩ -ta-> ⟨{V:T=x' V; e'},(h', (x' |` W))⟩"
      by -(drule red_reds.BlockRed[where T=T],simp)
    with False show ?thesis by(simp del: fun_upd_apply)
  qed
next
  case RedTryFail thus ?case by(auto intro: red_reds.RedTryFail)
qed(fastsimp intro: red_reds.intros)+

lemma red_notfree_unchanged: "[| extTA,P \<turnstile> ⟨e, s⟩ -ta-> ⟨e', s'⟩; V ∉ fv e |] ==> lcl s' V = lcl s V"
  and reds_notfree_unchanged: "[| extTA,P \<turnstile> ⟨es, s⟩ [-ta->] ⟨es', s'⟩; V ∉ fvs es |] ==> lcl s' V = lcl s V"
apply(induct rule: red_reds.inducts)
apply(fastsimp)+
done

lemma red_dom_lcl: "extTA,P \<turnstile> ⟨e, s⟩ -ta-> ⟨e', s'⟩ ==> dom (lcl s') ⊆ dom (lcl s) ∪ fv e"
  and reds_dom_lcl: "extTA,P \<turnstile> ⟨es, s⟩ [-ta->] ⟨es', s'⟩ ==> dom (lcl s') ⊆ dom (lcl s) ∪ fvs es"
proof (induct rule:red_reds.inducts)
  case (BlockRed e h x V vo ta e' h' x' T)
  thus ?case by(clarsimp)(fastsimp split:split_if_asm)
qed auto

subsection {* Final expressions *}

inductive final :: "('a,'b) exp => bool" where
  "final (Val v)"
| "final (Throw a)"

declare final.cases [elim]
declare final.intros[simp]

lemmas finalE[consumes 1, case_names Val Throw] = final.cases

lemma final_iff: "final e <-> (∃v. e = Val v) ∨ (∃a. e = Throw a)"
by(auto)

lemma final_locks: "final e ==> expr_locks e l = 0"
by(auto elim: finalE)

constdefs
  finals:: "('a,'b) exp list => bool"
  "finals es  ≡  (∃vs. es = map Val vs) ∨ (∃vs a es'. es = map Val vs @ Throw a # es')"

lemma [iff]: "finals []"
by(simp add:finals_def)

lemma [iff]: "finals (Val v # es) = finals es"
apply(clarsimp simp add: finals_def)
apply(rule iffI)
 apply(erule disjE)
  apply fastsimp
 apply(rule disjI2)
 apply clarsimp
 apply(case_tac vs)
  apply simp
 apply fastsimp
apply(erule disjE)
 apply clarsimp
 apply(rule_tac x="v#vs" in exI)
 apply(simp)
apply(rule disjI2)
apply clarsimp
apply(rule_tac x = "v#vs" in exI)
apply simp
done

lemma finals_app_map[iff]: "finals (map Val vs @ es) = finals es"
(*<*)by(induct_tac vs, auto)(*>*)

lemma [iff]: "finals (map Val vs)"
(*<*)using finals_app_map[of vs "[]"]by(simp)(*>*)

lemma [iff]: "finals (throw e # es) = (∃a. e = addr a)"
(*<*)
apply(simp add:finals_def)
apply(rule iffI)
 apply(erule disjE)
  apply(fastsimp)
 apply clarsimp
 apply(case_tac vs)
  apply simp
 apply fastsimp
apply clarsimp
apply(rule_tac x = "[]" in exI)
apply simp
apply(erule_tac x="[]" in allE)
apply(fastsimp)
done
(*>*)

lemma not_finals_ConsI: "¬ final e ==> ¬ finals(e#es)"
 (*<*)
apply(clarsimp simp add:finals_def final_iff)
apply(rule conjI)
 apply(fastsimp)
apply(clarsimp)
apply(case_tac vs)
apply auto
done
(*>*)


end