# Theory SmallStep

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

section ‹Small Step Semantics›

theory SmallStep
imports
Expr
State
JHeap
begin

type_synonym

type_synonym

(* pretty printing for J_thread_action type *)
print_translation ‹
let
fun tr'
[a1, t
, Const (@{type_syntax "prod"}, _) \$
(Const (@{type_syntax "exp"}, _) \$
Const (@{type_syntax "String.literal"}, _) \$ Const (@{type_syntax "unit"}, _) \$ a2) \$
(Const (@{type_syntax "fun"}, _) \$
Const (@{type_syntax "String.literal"}, _) \$
(Const (@{type_syntax "option"}, _) \$
(Const (@{type_syntax "val"}, _) \$ a3)))
, h] =
if a1 = a2 andalso a2 = a3 then Syntax.const @{type_syntax "J_thread_action"} \$ a1 \$ t \$ h
else raise Match;
end
›

(* pretty printing for J_state type *)
print_translation ‹
let
fun tr'
[a1, t
, Const (@{type_syntax "prod"}, _) \$
(Const (@{type_syntax "exp"}, _) \$
Const (@{type_syntax "String.literal"}, _) \$ Const (@{type_syntax "unit"}, _) \$ a2) \$
(Const (@{type_syntax "fun"}, _) \$
Const (@{type_syntax "String.literal"}, _) \$
(Const (@{type_syntax "option"}, _) \$
(Const (@{type_syntax "val"}, _) \$ a3)))
, h, a4] =
if a1 = a2 andalso a2 = a3 andalso a3 = a4 then Syntax.const @{type_syntax "J_state"} \$ a1 \$ t \$ h
else raise Match;
in [(@{type_syntax "state"}, K tr')]
end
›

where "extNTA2J P = (λ(C, M, a). let (D,Ts,T,meth) = method P C M; (pns,body) = the meth
in ({this:Class D=⌊Addr a⌋; body}, Map.empty))"

abbreviation J_local_start ::
"cname ⇒ mname ⇒ ty list ⇒ ty ⇒ 'addr J_mb ⇒ 'addr val list
where
"J_local_start ≡
λC M Ts T (pns, body) vs.
(blocks (this # pns) (Class C # Ts) (Null # vs) body, Map.empty)"

abbreviation (in J_heap_base)
where
"J_start_state ≡ start_state J_local_start"

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

abbreviation extTA2J ::
where "extTA2J P ≡ convert_extTA (extNTA2J P)"

lemma extTA2J_ε: "extTA2J P ε = ε"
by(simp)

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.›

context J_heap_base begin

inductive red ::
("_,_,_ ⊢ ((1⟨_,/_⟩) -_→/ (1⟨_,/_⟩))" [51,51,0,0,0,0,0,0] 81)
and reds ::
("_,_,_ ⊢ ((1⟨_,/_⟩) [-_→]/ (1⟨_,/_⟩))" [51,51,0,0,0,0,0,0] 81)
where
RedNew:
"(h', a) ∈ allocate h (Class_type C)
⟹ extTA,P,t ⊢ ⟨new C, (h, l)⟩ -⦃NewHeapElem a (Class_type C)⦄→ ⟨addr a, (h', l)⟩"

| RedNewFail:
"allocate h (Class_type C) = {}
⟹ extTA,P,t ⊢ ⟨new C, (h, l)⟩ -ε→ ⟨THROW OutOfMemory, (h, l)⟩"

| NewArrayRed:
"extTA,P,t ⊢ ⟨e, s⟩ -ta→ ⟨e', s'⟩ ⟹ extTA,P,t ⊢ ⟨newA T⌊e⌉, s⟩ -ta→ ⟨newA T⌊e'⌉, s'⟩"

| RedNewArray:
"⟦ 0 <=s i; (h', a) ∈ allocate h (Array_type T (nat (sint i))) ⟧
⟹ extTA,P,t ⊢ ⟨newA T⌊Val (Intg i)⌉, (h, l)⟩ -⦃NewHeapElem a (Array_type T (nat (sint i)))⦄→ ⟨addr a, (h', l)⟩"

| RedNewArrayNegative:
"i <s 0 ⟹ extTA,P,t ⊢ ⟨newA T⌊Val (Intg i)⌉, s⟩ -ε→ ⟨THROW NegativeArraySize, s⟩"

| RedNewArrayFail:
"⟦ 0 <=s i; allocate h (Array_type T (nat (sint i))) = {} ⟧
⟹ extTA,P,t ⊢ ⟨newA T⌊Val (Intg i)⌉, (h, l)⟩ -ε→ ⟨THROW OutOfMemory, (h, l)⟩"

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

| RedCast:
"⟦ typeof⇘hp s⇙ v = ⌊U⌋; P ⊢ U ≤ T ⟧
⟹ extTA,P,t ⊢ ⟨Cast T (Val v), s⟩ -ε→ ⟨Val v, s⟩"

| RedCastFail:
"⟦ typeof⇘hp s⇙ v = ⌊U⌋; ¬ P ⊢ U ≤ T ⟧
⟹ extTA,P,t ⊢ ⟨Cast T (Val v), s⟩ -ε→ ⟨THROW ClassCast, s⟩"

| InstanceOfRed:
"extTA,P,t ⊢ ⟨e, s⟩ -ta→ ⟨e', s'⟩ ⟹ extTA,P,t ⊢ ⟨e instanceof T, s⟩ -ta→ ⟨e' instanceof T, s'⟩"

| RedInstanceOf:
"⟦ typeof⇘hp s⇙ v = ⌊U⌋; b ⟷ v ≠ Null ∧ P ⊢ U ≤ T ⟧
⟹ extTA,P,t ⊢ ⟨(Val v) instanceof T, s⟩ -ε→ ⟨Val (Bool b), s⟩"

| BinOpRed1:
"extTA,P,t ⊢ ⟨e, s⟩ -ta→ ⟨e', s'⟩ ⟹ extTA,P,t ⊢ ⟨e «bop» e2, s⟩ -ta→ ⟨e' «bop» e2, s'⟩"

| BinOpRed2:
"extTA,P,t ⊢ ⟨e, s⟩ -ta→ ⟨e', s'⟩ ⟹ extTA,P,t ⊢ ⟨(Val v) «bop» e, s⟩ -ta→ ⟨(Val v) «bop» e', s'⟩"

| RedBinOp:
"binop bop v1 v2 = Some (Inl v) ⟹
extTA,P,t ⊢ ⟨(Val v1) «bop» (Val v2), s⟩ -ε→ ⟨Val v, s⟩"

| RedBinOpFail:
"binop bop v1 v2 = Some (Inr a) ⟹
extTA,P,t ⊢ ⟨(Val v1) «bop» (Val v2), s⟩ -ε→ ⟨Throw a, s⟩"

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

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

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

| AAccRed1:
"extTA,P,t ⊢ ⟨a, s⟩ -ta→ ⟨a', s'⟩ ⟹ extTA,P,t ⊢ ⟨a⌊i⌉, s⟩ -ta→ ⟨a'⌊i⌉, s'⟩"

| AAccRed2:
"extTA,P,t ⊢ ⟨i, s⟩ -ta→ ⟨i', s'⟩ ⟹ extTA,P,t ⊢ ⟨(Val a)⌊i⌉, s⟩ -ta→ ⟨(Val a)⌊i'⌉, s'⟩"

| RedAAccNull:
"extTA,P,t ⊢ ⟨null⌊Val i⌉, s⟩ -ε→ ⟨THROW NullPointer, s⟩"

| RedAAccBounds:
"⟦ typeof_addr (hp s) a = ⌊Array_type T n⌋; i <s 0 ∨ sint i ≥ int n ⟧
⟹ extTA,P,t ⊢ ⟨(addr a)⌊Val (Intg i)⌉, s⟩ -ε→ ⟨THROW ArrayIndexOutOfBounds, s⟩"

| RedAAcc:
"⟦ typeof_addr h a = ⌊Array_type T n⌋; 0 <=s i; sint i < int n;
heap_read h a (ACell (nat (sint i))) v ⟧
⟹ extTA,P,t ⊢ ⟨(addr a)⌊Val (Intg i)⌉, (h, l)⟩ -⦃ReadMem a (ACell (nat (sint i))) v⦄→ ⟨Val v, (h, l)⟩"

| AAssRed1:
"extTA,P,t ⊢ ⟨a, s⟩ -ta→ ⟨a', s'⟩ ⟹ extTA,P,t ⊢ ⟨a⌊i⌉ := e, s⟩ -ta→ ⟨a'⌊i⌉ := e, s'⟩"

| AAssRed2:
"extTA,P,t ⊢ ⟨i, s⟩ -ta→ ⟨i', s'⟩ ⟹ extTA,P,t ⊢ ⟨(Val a)⌊i⌉ := e, s⟩ -ta→ ⟨(Val a)⌊i'⌉ := e, s'⟩"

| AAssRed3:
"extTA,P,t ⊢ ⟨(e::'addr expr), s⟩ -ta→ ⟨e', s'⟩ ⟹ extTA,P,t ⊢ ⟨(Val a)⌊Val i⌉ := e, s⟩ -ta→ ⟨(Val a)⌊Val i⌉ := e', s'⟩"

| RedAAssNull:
"extTA,P,t ⊢ ⟨null⌊Val i⌉ := (Val e::'addr expr), s⟩ -ε→ ⟨THROW NullPointer, s⟩"

| RedAAssBounds:
"⟦ typeof_addr (hp s) a = ⌊Array_type T n⌋; i <s 0 ∨ sint i ≥ int n ⟧
⟹ extTA,P,t ⊢ ⟨(addr a)⌊Val (Intg i)⌉ := (Val e::'addr expr), s⟩ -ε→ ⟨THROW ArrayIndexOutOfBounds, s⟩"

| RedAAssStore:
"⟦ typeof_addr (hp s) a = ⌊Array_type T n⌋; 0 <=s i; sint i < int n;
typeof⇘hp s⇙ w = ⌊U⌋; ¬ (P ⊢ U ≤ T) ⟧
⟹ extTA,P,t ⊢ ⟨(addr a)⌊Val (Intg i)⌉ := (Val w::'addr expr), s⟩ -ε→ ⟨THROW ArrayStore, s⟩"

| RedAAss:
"⟦ typeof_addr h a = ⌊Array_type T n⌋; 0 <=s i; sint i < int n; typeof⇘h⇙ w = Some U; P ⊢ U ≤ T;
heap_write h a (ACell (nat (sint i))) w h' ⟧
⟹ extTA,P,t ⊢ ⟨(addr a)⌊Val (Intg i)⌉ := Val w::'addr expr, (h, l)⟩ -⦃WriteMem a (ACell (nat (sint i))) w⦄→ ⟨unit, (h', l)⟩"

| ALengthRed:
"extTA,P,t ⊢ ⟨a, s⟩ -ta→ ⟨a', s'⟩ ⟹ extTA,P,t ⊢ ⟨a∙length, s⟩ -ta→ ⟨a'∙length, s'⟩"

| RedALength:
"typeof_addr h a = ⌊Array_type T n⌋
⟹ extTA,P,t ⊢ ⟨addr a∙length, (h, l)⟩ -ε→ ⟨Val (Intg (word_of_nat n)), (h, l)⟩"

| RedALengthNull:
"extTA,P,t ⊢ ⟨null∙length, s⟩ -ε→ ⟨THROW NullPointer, s⟩"

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

| RedFAcc:
"heap_read h a (CField D F) v
⟹ extTA,P,t ⊢ ⟨(addr a)∙F{D}, (h, l)⟩ -⦃ReadMem a (CField D F) v⦄→ ⟨Val v, (h, l)⟩"

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

| FAssRed1:
"extTA,P,t ⊢ ⟨e, s⟩ -ta→ ⟨e', s'⟩ ⟹ extTA,P,t ⊢ ⟨e∙F{D}:=e2, s⟩ -ta→ ⟨e'∙F{D}:=e2, s'⟩"

| FAssRed2:
"extTA,P,t ⊢ ⟨(e::'addr expr), s⟩ -ta→ ⟨e', s'⟩ ⟹ extTA,P,t ⊢ ⟨Val v∙F{D}:=e, s⟩ -ta→ ⟨Val v∙F{D}:=e', s'⟩"

| RedFAss:
"heap_write h a (CField D F) v h' ⟹
extTA,P,t ⊢ ⟨(addr a)∙F{D}:= Val v, (h, l)⟩ -⦃WriteMem a (CField D F) v⦄→ ⟨unit, (h', l)⟩"

| RedFAssNull:
"extTA,P,t ⊢ ⟨null∙F{D}:=Val v::'addr expr, s⟩ -ε→ ⟨THROW NullPointer, s⟩"

| CASRed1:
"extTA,P,t ⊢ ⟨e, s⟩ -ta→ ⟨e', s'⟩ ⟹
extTA,P,t ⊢ ⟨e∙compareAndSwap(D∙F, e2, e3), s⟩ -ta→ ⟨e'∙compareAndSwap(D∙F, e2, e3), s'⟩"

| CASRed2:
"extTA,P,t ⊢ ⟨e, s⟩ -ta→ ⟨e', s'⟩ ⟹
extTA,P,t ⊢ ⟨Val v∙compareAndSwap(D∙F, e, e3), s⟩ -ta→ ⟨Val v∙compareAndSwap(D∙F, e', e3), s'⟩"

| CASRed3:
"extTA,P,t ⊢ ⟨e, s⟩ -ta→ ⟨e', s'⟩ ⟹
extTA,P,t ⊢ ⟨Val v∙compareAndSwap(D∙F, Val v', e), s⟩ -ta→ ⟨Val v∙compareAndSwap(D∙F, Val v', e'), s'⟩"

| CASNull:
"extTA,P,t ⊢ ⟨null∙compareAndSwap(D∙F, Val v, Val v'), s⟩ -ε→ ⟨THROW NullPointer, s⟩"

| RedCASSucceed:
"⟦ heap_read h a (CField D F) v; heap_write h a (CField D F) v' h' ⟧ ⟹
extTA,P,t ⊢ ⟨addr a∙compareAndSwap(D∙F, Val v, Val v'), (h, l)⟩
-⦃ReadMem a (CField D F) v, WriteMem a (CField D F) v'⦄→
⟨true, (h', l)⟩"

| RedCASFail:
"⟦ heap_read h a (CField D F) v''; v ≠ v'' ⟧ ⟹
extTA,P,t ⊢ ⟨addr a∙compareAndSwap(D∙F, Val v, Val v'), (h, l)⟩
-⦃ReadMem a (CField D F) v''⦄→
⟨false, (h, l)⟩"

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

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

| RedCall:
"⟦ typeof_addr (hp s) a = ⌊hU⌋; P ⊢ class_type_of hU sees M:Ts→T = ⌊(pns,body)⌋ in D;
size vs = size pns; size Ts = size pns ⟧
⟹ extTA,P,t ⊢ ⟨(addr a)∙M(map Val vs), s⟩ -ε→ ⟨blocks (this # pns) (Class D # Ts) (Addr a # vs) body, s⟩"

| RedCallExternal:
"⟦ typeof_addr (hp s) a = ⌊hU⌋; P ⊢ class_type_of hU sees M:Ts→T = Native in D;
P,t ⊢ ⟨a∙M(vs), hp s⟩ -ta→ext ⟨va, h'⟩;
ta' = extTA ta; e' = extRet2J ((addr a)∙M(map Val vs)) va; s' = (h', lcl s) ⟧
⟹ extTA,P,t ⊢ ⟨(addr a)∙M(map Val vs), s⟩ -ta'→ ⟨e', s'⟩"

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

| BlockRed:
"extTA,P,t ⊢ ⟨e, (h, l(V:=vo))⟩ -ta→ ⟨e', (h', l')⟩
⟹ extTA,P,t ⊢ ⟨{V:T=vo; e}, (h, l)⟩ -ta→ ⟨{V:T=l' V; e'}, (h', l'(V := l V))⟩"

| RedBlock:
"extTA,P,t ⊢ ⟨{V:T=vo; Val u}, s⟩ -ε→ ⟨Val u, s⟩"

| SynchronizedRed1:
"extTA,P,t ⊢ ⟨o', s⟩ -ta→ ⟨o'', s'⟩ ⟹ extTA,P,t ⊢ ⟨sync(o') e, s⟩ -ta→ ⟨sync(o'') e, s'⟩"

| SynchronizedNull:
"extTA,P,t ⊢ ⟨sync(null) e, s⟩ -ε→ ⟨THROW NullPointer, s⟩"

| LockSynchronized:
"extTA,P,t ⊢ ⟨sync(addr a) e, s⟩ -⦃Lock→a, SyncLock a⦄→ ⟨insync(a) e, s⟩"

| SynchronizedRed2:
"extTA,P,t ⊢ ⟨e, s⟩ -ta→ ⟨e', s'⟩ ⟹ extTA,P,t ⊢ ⟨insync(a) e, s⟩ -ta→ ⟨insync(a) e', s'⟩"

| UnlockSynchronized:
"extTA,P,t ⊢ ⟨insync(a) (Val v), s⟩ -⦃Unlock→a, SyncUnlock a⦄→ ⟨Val v, s⟩"

| SeqRed:
"extTA,P,t ⊢ ⟨e, s⟩ -ta→ ⟨e', s'⟩ ⟹ extTA,P,t ⊢ ⟨e;;e2, s⟩ -ta→ ⟨e';;e2, s'⟩"

| RedSeq:
"extTA,P,t ⊢ ⟨(Val v);;e, s⟩ -ε→ ⟨e, s⟩"

| CondRed:
"extTA,P,t ⊢ ⟨b, s⟩ -ta→ ⟨b', s'⟩ ⟹ extTA,P,t ⊢ ⟨if (b) e1 else e2, s⟩ -ta→ ⟨if (b') e1 else e2, s'⟩"

| RedCondT:
"extTA,P,t ⊢ ⟨if (true) e1 else e2, s⟩ -ε→ ⟨e1, s⟩"

| RedCondF:
"extTA,P,t ⊢ ⟨if (false) e1 else e2, s⟩ -ε→ ⟨e2, s⟩"

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

| ThrowRed:
"extTA,P,t ⊢ ⟨e, s⟩ -ta→ ⟨e', s'⟩ ⟹ extTA,P,t ⊢ ⟨throw e, s⟩ -ta→ ⟨throw e', s'⟩"

| RedThrowNull:
"extTA,P,t ⊢ ⟨throw null, s⟩ -ε→ ⟨THROW NullPointer, s⟩"

| TryRed:
"extTA,P,t ⊢ ⟨e, s⟩ -ta→ ⟨e', s'⟩ ⟹ extTA,P,t ⊢ ⟨try e catch(C V) e2, s⟩ -ta→ ⟨try e' catch(C V) e2, s'⟩"

| RedTry:
"extTA,P,t ⊢ ⟨try (Val v) catch(C V) e2, s⟩ -ε→ ⟨Val v, s⟩"

| RedTryCatch:
"⟦ typeof_addr (hp s) a = ⌊Class_type D⌋; P ⊢ D ≼⇧* C ⟧
⟹ extTA,P,t ⊢ ⟨try (Throw a) catch(C V) e2, s⟩ -ε→ ⟨{V:Class C=⌊Addr a⌋; e2}, s⟩"

| RedTryFail:
"⟦ typeof_addr (hp s) a = ⌊Class_type D⌋; ¬ P ⊢ D ≼⇧* C ⟧
⟹ extTA,P,t ⊢ ⟨try (Throw a) catch(C V) e2, s⟩ -ε→ ⟨Throw a, s⟩"

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

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

― ‹Exception propagation›

| NewArrayThrow: "extTA,P,t ⊢ ⟨newA T⌊Throw a⌉, s⟩ -ε→ ⟨Throw a, s⟩"
| CastThrow: "extTA,P,t ⊢ ⟨Cast C (Throw a), s⟩ -ε→ ⟨Throw a, s⟩"
| InstanceOfThrow: "extTA,P,t ⊢ ⟨(Throw a) instanceof T, s⟩ -ε→ ⟨Throw a, s⟩"
| BinOpThrow1: "extTA,P,t ⊢ ⟨(Throw a) «bop» e⇩2, s⟩ -ε→ ⟨Throw a, s⟩"
| BinOpThrow2: "extTA,P,t ⊢ ⟨(Val v⇩1) «bop» (Throw a), s⟩ -ε→ ⟨Throw a, s⟩"
| LAssThrow: "extTA,P,t ⊢ ⟨V:=(Throw a), s⟩ -ε→ ⟨Throw a, s⟩"
| AAccThrow1: "extTA,P,t ⊢ ⟨(Throw a)⌊i⌉, s⟩ -ε→ ⟨Throw a, s⟩"
| AAccThrow2: "extTA,P,t ⊢ ⟨(Val v)⌊Throw a⌉, s⟩ -ε→ ⟨Throw a, s⟩"
| AAssThrow1: "extTA,P,t ⊢ ⟨(Throw a)⌊i⌉ := e, s⟩ -ε→ ⟨Throw a, s⟩"
| AAssThrow2: "extTA,P,t ⊢ ⟨(Val v)⌊Throw a⌉ := e, s⟩ -ε→ ⟨Throw a, s⟩"
| AAssThrow3: "extTA,P,t ⊢ ⟨(Val v)⌊Val i⌉ := Throw a :: 'addr expr, s⟩ -ε→ ⟨Throw a, s⟩"
| ALengthThrow: "extTA,P,t ⊢ ⟨(Throw a)∙length, s⟩ -ε→ ⟨Throw a, s⟩"
| FAccThrow: "extTA,P,t ⊢ ⟨(Throw a)∙F{D}, s⟩ -ε→ ⟨Throw a, s⟩"
| FAssThrow1: "extTA,P,t ⊢ ⟨(Throw a)∙F{D}:=e⇩2, s⟩ -ε→ ⟨Throw a, s⟩"
| FAssThrow2: "extTA,P,t ⊢ ⟨Val v∙F{D}:=(Throw a::'addr expr), s⟩ -ε→ ⟨Throw a, s⟩"
| CASThrow: "extTA,P,t ⊢ ⟨Throw a∙compareAndSwap(D∙F, e2, e3), s⟩ -ε→ ⟨Throw a, s⟩"
| CASThrow2: "extTA,P,t ⊢ ⟨Val v∙compareAndSwap(D∙F, Throw a, e3), s⟩ -ε→ ⟨Throw a, s⟩"
| CASThrow3: "extTA,P,t ⊢ ⟨Val v∙compareAndSwap(D∙F, Val v', Throw a), s⟩ -ε→ ⟨Throw a, s⟩"
| CallThrowObj: "extTA,P,t ⊢ ⟨(Throw a)∙M(es), s⟩ -ε→ ⟨Throw a, s⟩"
| CallThrowParams: "⟦ es = map Val vs @ Throw a # es' ⟧ ⟹ extTA,P,t ⊢ ⟨(Val v)∙M(es), s⟩ -ε→ ⟨Throw a, s⟩"
| BlockThrow: "extTA,P,t ⊢ ⟨{V:T=vo; Throw a}, s⟩ -ε→ ⟨Throw a, s⟩"
| SynchronizedThrow1: "extTA,P,t ⊢ ⟨sync(Throw a) e, s⟩ -ε→ ⟨Throw a, s⟩"
| SynchronizedThrow2: "extTA,P,t ⊢ ⟨insync(a) Throw ad, s⟩ -⦃Unlock→a, SyncUnlock a⦄→ ⟨Throw ad, s⟩"
| SeqThrow: "extTA,P,t ⊢ ⟨(Throw a);;e⇩2, s⟩ -ε→ ⟨Throw a, s⟩"
| CondThrow: "extTA,P,t ⊢ ⟨if (Throw a) e⇩1 else e⇩2, s⟩ -ε→ ⟨Throw a, s⟩"
| ThrowThrow: "extTA,P,t ⊢ ⟨throw(Throw a), s⟩ -ε→ ⟨Throw a, s⟩"

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

inductive_cases reds_cases:
"extTA,P,t ⊢ ⟨e # es, s⟩ [-ta→] ⟨es', s'⟩"

abbreviation red' ::
("_,_ ⊢ ((1⟨_,/_⟩) -_→/ (1⟨_,/_⟩))" [51,0,0,0,0,0,0] 81)
where "red' P ≡ red (extTA2J P) P"

abbreviation reds' ::
("_,_ ⊢ ((1⟨_,/_⟩) [-_→]/ (1⟨_,/_⟩))" [51,0,0,0,0,0,0] 81)
where "reds' P ≡ reds (extTA2J P) P"

subsection‹Some easy lemmas›

lemma [iff]:
"¬ extTA,P,t ⊢ ⟨Val v, s⟩ -ta→ ⟨e', s'⟩"
by(fastforce elim:red.cases)

lemma red_no_val [dest]:
"⟦ extTA,P,t ⊢ ⟨e, s⟩ -tas→ ⟨e', s'⟩; is_val e ⟧ ⟹ False"
by(auto)

lemma [iff]: "¬ extTA,P,t ⊢ ⟨Throw a, s⟩ -ta→ ⟨e', s'⟩"
by(fastforce elim: red_cases)

lemma reds_map_Val_Throw:
"extTA,P,t ⊢ ⟨map Val vs @ Throw a # es, s⟩ [-ta→] ⟨es', s'⟩ ⟷ False"
by(induct vs arbitrary: es')(auto elim!: reds_cases)

lemma reds_preserves_len:
"extTA,P,t ⊢ ⟨es, s⟩ [-ta→] ⟨es', s'⟩ ⟹ length es' = length es"
by(induct es arbitrary: es')(auto elim: reds.cases)

lemma red_lcl_incr: "extTA,P,t ⊢ ⟨e, s⟩ -ta→ ⟨e', s'⟩ ⟹ dom (lcl s) ⊆ dom (lcl s')"
and reds_lcl_incr: "extTA,P,t ⊢ ⟨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: if_split_asm)
done

"extTA,P,t ⊢ ⟨e, s⟩ -ta→ ⟨e', s'⟩ ⟹ extTA,P,t ⊢ ⟨e, (hp s, l0 ++ lcl s)⟩ -ta→ ⟨e', (hp s', l0 ++ lcl s')⟩"
"extTA,P,t ⊢ ⟨es, s⟩ [-ta→] ⟨es', s'⟩ ⟹ extTA,P,t ⊢ ⟨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,t ⊢ ⟨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)"
have lrew1: "⋀X X' X'' vo. (X(V := vo) ++ X')(V := (X ++ X'') V) = X ++ X'(V := X'' V)"
have lrew2: "⋀X X'. (X(V := None) ++ X') V = X' V"
show ?case
proof(cases vo)
case None
from IH[of "l0(V := vo)"]
show ?thesis
apply(drule red_reds.BlockRed)
by(simp only: lrew1 None lrew2)
next
case (Some v)
with ‹extTA,P,t ⊢ ⟨e,(h, x(V := vo))⟩ -ta→ ⟨e',(h', x')⟩›
have "x' V ≠ None"
by -(drule red_lcl_incr, auto split: if_split_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 thus ?case
by(auto intro: red_reds.RedTryFail)
qed(fastforce intro:red_reds.intros simp del: fun_upd_apply)+

lemma red_lcl_add: "extTA,P,t ⊢ ⟨e, (h, l)⟩ -ta→ ⟨e', (h', l')⟩ ⟹ extTA,P,t ⊢ ⟨e, (h, l0 ++ l)⟩ -ta→ ⟨e', (h', l0 ++ l')⟩"
and reds_lcl_add: "extTA,P,t ⊢ ⟨es, (h, l)⟩ [-ta→] ⟨es', (h', l')⟩ ⟹ extTA,P,t ⊢ ⟨es, (h, l0 ++ l)⟩ [-ta→] ⟨es', (h', l0 ++ l')⟩"

lemma reds_no_val [dest]:
"⟦ extTA,P,t ⊢ ⟨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,t ⊢ ⟨Throw a, s⟩ -ta→ ⟨e', s'⟩ ⟹ False"
by(auto elim!: red_cases)

lemma red_lcl_sub:
"⟦ extTA,P,t ⊢ ⟨e, s⟩ -ta→ ⟨e', s'⟩; fv e ⊆ W ⟧
⟹ extTA,P,t ⊢ ⟨e, (hp s, (lcl s)|`W)⟩ -ta→ ⟨e', (hp s', (lcl s')|`W)⟩"

and reds_lcl_sub:
"⟦ extTA,P,t ⊢ ⟨es, s⟩ [-ta→] ⟨es', s'⟩; fvs es ⊆ W ⟧
⟹ extTA,P,t ⊢ ⟨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,t ⊢ ⟨V:=Val v,(h, l |` W)⟩ -ε→ ⟨unit,(h, (l |`W)(V ↦ 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,t ⊢ ⟨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,t ⊢ ⟨e,(h, (x |` W )(V := vo))⟩ -ta→ ⟨e',(h', x' |` W)⟩" by(simp)
with True have "extTA,P,t ⊢ ⟨{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,t ⊢ ⟨e,(h, (x |` W)(V := vo))⟩ -ta→ ⟨e',(h', x' |` insert V W)⟩" by(simp)
with False have "extTA,P,t ⊢ ⟨{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(fastforce intro: red_reds.intros)+

lemma red_notfree_unchanged: "⟦ extTA,P,t ⊢ ⟨e, s⟩ -ta→ ⟨e', s'⟩; V ∉ fv e ⟧ ⟹ lcl s' V = lcl s V"
and reds_notfree_unchanged: "⟦ extTA,P,t ⊢ ⟨es, s⟩ [-ta→] ⟨es', s'⟩; V ∉ fvs es ⟧ ⟹ lcl s' V = lcl s V"
apply(induct rule: red_reds.inducts)
apply(fastforce)+
done

lemma red_dom_lcl: "extTA,P,t ⊢ ⟨e, s⟩ -ta→ ⟨e', s'⟩ ⟹ dom (lcl s') ⊆ dom (lcl s) ∪ fv e"
and reds_dom_lcl: "extTA,P,t ⊢ ⟨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)(fastforce split:if_split_asm)
qed auto

lemma red_Suspend_is_call:
"⟦ convert_extTA extNTA,P,t ⊢ ⟨e, s⟩ -ta→ ⟨e', s'⟩; Suspend w ∈ set ⦃ta⦄⇘w⇙ ⟧
⟹ ∃a vs hT Ts Tr D. call e' = ⌊(a, wait, vs)⌋ ∧ typeof_addr (hp s) a = ⌊hT⌋ ∧ P ⊢ class_type_of hT sees wait:Ts→Tr = Native in D"
and reds_Suspend_is_calls:
"⟦ convert_extTA extNTA,P,t ⊢ ⟨es, s⟩ [-ta→] ⟨es', s'⟩; Suspend w ∈ set ⦃ta⦄⇘w⇙ ⟧
⟹ ∃a vs hT Ts Tr D. calls es' = ⌊(a, wait, vs)⌋ ∧ typeof_addr (hp s) a = ⌊hT⌋ ∧ P ⊢ class_type_of hT sees wait:Ts→Tr = Native in D"
proof(induct rule: red_reds.inducts)
case RedCallExternal
thus ?case
apply clarsimp
apply(frule red_external_Suspend_StaySame, simp)
apply(drule red_external_Suspend_waitD, fastforce+)
done
qed auto

end

context J_heap begin

lemma red_hext_incr: "extTA,P,t ⊢ ⟨e, s⟩ -ta→ ⟨e', s'⟩ ⟹ hp s ⊴ hp s'"
and reds_hext_incr: "extTA,P,t ⊢ ⟨es, s⟩ [-ta→] ⟨es', s'⟩ ⟹ hp s ⊴ hp s'"
by(induct rule:red_reds.inducts)(auto intro: hext_heap_ops red_external_hext)

lemma red_preserves_tconf: "⟦ extTA,P,t ⊢ ⟨e, s⟩ -ta→ ⟨e', s'⟩; P,hp s ⊢ t √t ⟧ ⟹ P,hp s' ⊢ t √t"
by(drule red_hext_incr)(rule tconf_hext_mono)

lemma reds_preserves_tconf: "⟦ extTA,P,t ⊢ ⟨es, s⟩ [-ta→] ⟨es', s'⟩; P,hp s ⊢ t √t ⟧ ⟹ P,hp s' ⊢ t √t"
by(drule reds_hext_incr)(rule tconf_hext_mono)

end

subsection ‹Code generation›

context J_heap_base begin

lemma RedCall_code:
"⟦ is_vals es; typeof_addr (hp s) a = ⌊hU⌋; P ⊢ class_type_of hU sees M:Ts→T = ⌊(pns,body)⌋ in D;
size es = size pns; size Ts = size pns ⟧
⟹ extTA,P,t ⊢ ⟨(addr a)∙M(es), s⟩ -ε→ ⟨blocks (this # pns) (Class D # Ts) (Addr a # map the_Val es) body, s⟩"

and RedCallExternal_code:
"⟦ is_vals es; typeof_addr (hp s) a = ⌊hU⌋; P ⊢ class_type_of hU sees M:Ts→T = Native in D;
P,t ⊢ ⟨a∙M(map the_Val es), hp s⟩ -ta→ext ⟨va, h'⟩ ⟧
⟹ extTA,P,t ⊢ ⟨(addr a)∙M(es), s⟩ -extTA ta→ ⟨extRet2J ((addr a)∙M(es)) va, (h', lcl s)⟩"

and RedCallNull_code:
"is_vals es ⟹ extTA,P,t ⊢ ⟨null∙M(es), s⟩ -ε→ ⟨THROW NullPointer, s⟩"

and CallThrowParams_code:
"is_Throws es ⟹ extTA,P,t ⊢ ⟨(Val v)∙M(es), s⟩ -ε→ ⟨hd (dropWhile is_val es), s⟩"

apply(auto simp add: is_vals_conv is_Throws_conv o_def intro: RedCall RedCallExternal RedCallNull simp del: blocks.simps)
apply(subst dropWhile_append2)
apply(auto intro: CallThrowParams)
done

end

lemmas [code_pred_intro] =
J_heap_base.RedNew[folded Predicate_Compile.contains_def] J_heap_base.RedNewFail J_heap_base.NewArrayRed
J_heap_base.RedNewArray[folded Predicate_Compile.contains_def]
J_heap_base.RedNewArrayNegative J_heap_base.RedNewArrayFail
J_heap_base.CastRed J_heap_base.RedCast J_heap_base.RedCastFail J_heap_base.InstanceOfRed
J_heap_base.RedInstanceOf J_heap_base.BinOpRed1 J_heap_base.BinOpRed2 J_heap_base.RedBinOp J_heap_base.RedBinOpFail
J_heap_base.RedVar J_heap_base.LAssRed J_heap_base.RedLAss
J_heap_base.AAccRed1 J_heap_base.AAccRed2 J_heap_base.RedAAccNull
J_heap_base.RedAAccBounds J_heap_base.RedAAcc J_heap_base.AAssRed1 J_heap_base.AAssRed2 J_heap_base.AAssRed3
J_heap_base.RedAAssNull J_heap_base.RedAAssBounds J_heap_base.RedAAssStore J_heap_base.RedAAss J_heap_base.ALengthRed
J_heap_base.RedALength J_heap_base.RedALengthNull J_heap_base.FAccRed J_heap_base.RedFAcc J_heap_base.RedFAccNull
J_heap_base.FAssRed1 J_heap_base.FAssRed2 J_heap_base.RedFAss J_heap_base.RedFAssNull
J_heap_base.CASRed1 J_heap_base.CASRed2 J_heap_base.CASRed3 J_heap_base.CASNull J_heap_base.RedCASSucceed J_heap_base.RedCASFail
J_heap_base.CallObj J_heap_base.CallParams

declare
J_heap_base.RedCall_code[code_pred_intro RedCall_code]
J_heap_base.RedCallExternal_code[code_pred_intro RedCallExternal_code]
J_heap_base.RedCallNull_code[code_pred_intro RedCallNull_code]

lemmas [code_pred_intro] =
J_heap_base.BlockRed J_heap_base.RedBlock J_heap_base.SynchronizedRed1 J_heap_base.SynchronizedNull
J_heap_base.LockSynchronized J_heap_base.SynchronizedRed2 J_heap_base.UnlockSynchronized
J_heap_base.SeqRed J_heap_base.RedSeq J_heap_base.CondRed J_heap_base.RedCondT J_heap_base.RedCondF J_heap_base.RedWhile
J_heap_base.ThrowRed

declare
J_heap_base.RedThrowNull[code_pred_intro RedThrowNull']

lemmas [code_pred_intro] =
J_heap_base.TryRed J_heap_base.RedTry J_heap_base.RedTryCatch
J_heap_base.RedTryFail J_heap_base.ListRed1 J_heap_base.ListRed2
J_heap_base.NewArrayThrow J_heap_base.CastThrow J_heap_base.InstanceOfThrow J_heap_base.BinOpThrow1 J_heap_base.BinOpThrow2
J_heap_base.LAssThrow J_heap_base.AAccThrow1 J_heap_base.AAccThrow2 J_heap_base.AAssThrow1 J_heap_base.AAssThrow2
J_heap_base.AAssThrow3 J_heap_base.ALengthThrow J_heap_base.FAccThrow J_heap_base.FAssThrow1 J_heap_base.FAssThrow2
J_heap_base.CASThrow J_heap_base.CASThrow2 J_heap_base.CASThrow3
J_heap_base.CallThrowObj

declare
J_heap_base.CallThrowParams_code[code_pred_intro CallThrowParams_code]

lemmas [code_pred_intro] =
J_heap_base.BlockThrow J_heap_base.SynchronizedThrow1 J_heap_base.SynchronizedThrow2 J_heap_base.SeqThrow
J_heap_base.CondThrow

declare
J_heap_base.ThrowThrow[code_pred_intro ThrowThrow']

code_pred
(modes:
J_heap_base.red: i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ (i ⇒ i ⇒ i ⇒ o ⇒ bool) ⇒ (i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ bool) ⇒ i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ o ⇒ o ⇒ bool
and
J_heap_base.reds: i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ (i ⇒ i ⇒ i ⇒ o ⇒ bool) ⇒ (i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ bool) ⇒ i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ o ⇒ o ⇒ bool)
[detect_switches, skip_proof] ― ‹proofs are possible, but take veeerry long›
J_heap_base.red
proof -
case red
from red.prems show thesis
proof(cases rule: J_heap_base.red.cases[consumes 1, case_names
RedNew RedNewFail NewArrayRed RedNewArray RedNewArrayNegative RedNewArrayFail CastRed RedCast RedCastFail InstanceOfRed
RedInstanceOf BinOpRed1 BinOpRed2 RedBinOp RedBinOpFail RedVar LAssRed RedLAss
AAccRed1 AAccRed2 RedAAccNull RedAAccBounds RedAAcc
AAssRed1 AAssRed2 AAssRed3 RedAAssNull RedAAssBounds RedAAssStore RedAAss ALengthRed RedALength RedALengthNull FAccRed
RedFAcc RedFAccNull FAssRed1 FAssRed2 RedFAss RedFAssNull CASRed1 CASRed2 CASRed3 RedCASNull RedCASSucceed RedCASFail
CallObj CallParams RedCall RedCallExternal RedCallNull
BlockRed RedBlock SynchronizedRed1 SynchronizedNull LockSynchronized SynchronizedRed2 UnlockSynchronized SeqRed
RedSeq CondRed RedCondT RedCondF RedWhile ThrowRed RedThrowNull TryRed RedTry RedTryCatch RedTryFail
NewArrayThrow CastThrow InstanceOfThrow BinOpThrow1 BinOpThrow2 LAssThrow AAccThrow1 AAccThrow2 AAssThrow1 AAssThrow2
AAssThrow3 ALengthThrow FAccThrow FAssThrow1 FAssThrow2 CASThrow CASThrow2 CASThrow3
CallThrowObj CallThrowParams BlockThrow SynchronizedThrow1
SynchronizedThrow2 SeqThrow CondThrow ThrowThrow])

case (RedCall s a U M Ts T pns body D vs)
with red.RedCall_code[OF refl refl refl refl refl refl refl refl refl refl refl, of a M "map Val vs" s pns D Ts body U T]
next
case (RedCallExternal s a U M Ts T D vs ta va h' ta' e' s')
with red.RedCallExternal_code[OF refl refl refl refl refl refl refl refl refl refl refl, of a M "map Val vs" s ta va h' U Ts T D]
next
case (RedCallNull M vs s)
with red.RedCallNull_code[OF refl refl refl refl refl refl refl refl refl refl refl, of M "map Val vs" s]
next
case (CallThrowParams es vs a es' v M s)
with red.CallThrowParams_code[OF refl refl refl refl refl refl refl refl refl refl refl, of v M "map Val vs @ Throw a # es'" s]
show ?thesis
apply(erule meta_impE)
apply(subst dropWhile_append2)
apply auto
done
next
case RedThrowNull thus ?thesis
by-(erule (4) red.RedThrowNull'[OF refl refl refl refl refl refl refl refl refl refl refl])
next
case ThrowThrow thus ?thesis
by-(erule (4) red.ThrowThrow'[OF refl refl refl refl refl refl refl refl refl refl refl])
qed(assumption|erule (4) red.that[unfolded Predicate_Compile.contains_def, OF refl refl refl refl refl refl refl refl refl refl refl])+
next
case reds
from reds.prems show thesis
by(rule J_heap_base.reds.cases)(assumption|erule (4) reds.that[OF refl refl refl refl refl refl refl refl refl refl refl])+
qed

end
```