# Theory J1

```(*  Title:      JinjaThreads/Compiler/J1.thy
Author:     Andreas Lochbihler
*)

section ‹Semantics of the intermediate language›

theory J1 imports
J1State
J1Heap
"../Framework/FWBisimulation"
begin

"final_expr1 ≡ λ(ex, exs). final (fst ex) ∧ exs = []"

definition extNTA2J1 ::
where
"extNTA2J1 P = (λ(C, M, a). let (D, _, _, meth) = method P C M; body = the meth
in (({0:Class D=None; body}, Addr a # replicate (max_vars body) undefined_value), []))"

lemma extNTA2J1_iff [simp]:
"extNTA2J1 P (C, M, a) = (({0:Class (fst (method P C M))=None; the (snd (snd (snd (method P C M))))}, Addr a # replicate (max_vars (the (snd (snd (snd (method P C M)))))) undefined_value), [])"

abbreviation extTA2J1 ::
where "extTA2J1 P ≡ convert_extTA (extNTA2J1 P)"

where "extRet2J1 ≡ extRet2J"

lemma max_vars_extRet2J1 [simp]:
"max_vars e = 0 ⟹ max_vars (extRet2J1 e va) = 0"
by(cases va) simp_all

context J1_heap_base begin

where
"J1_start_state ≡
start_state (λC M Ts T body vs. ((blocks1 0 (Class C # Ts) body, Null # vs @ replicate (max_vars body) undefined_value), []))"

inductive red1 ::
("_,_,_ ⊢1 ((1⟨_,/_⟩) -_→/ (1⟨_,/_⟩))" [51,51,0,0,0,0,0,0] 81)
and reds1 ::
("_,_,_ ⊢1 ((1⟨_,/_⟩) [-_→]/ (1⟨_,/_⟩))" [51,51,0,0,0,0,0,0] 81)
for uf :: bool and P :: "'addr J1_prog" and t :: 'thread_id
where
Red1New:
"(h', a) ∈ allocate h (Class_type C)
⟹ uf,P,t ⊢1 ⟨new C, (h, l)⟩ -⦃NewHeapElem a (Class_type C)⦄→ ⟨addr a, (h', l)⟩"

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

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

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

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

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

| Cast1Red:
"uf,P,t ⊢1 ⟨e, s⟩ -ta→ ⟨e', s'⟩
⟹ uf,P,t ⊢1 ⟨Cast C e, s⟩ -ta→ ⟨Cast C e', s'⟩"

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

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

| InstanceOf1Red:
"uf,P,t ⊢1 ⟨e, s⟩ -ta→ ⟨e', s'⟩ ⟹ uf,P,t ⊢1 ⟨e instanceof T, s⟩ -ta→ ⟨e' instanceof T, s'⟩"

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

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

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

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

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

| Red1Var:
"⟦ (lcl s)!V = v; V < size (lcl s) ⟧
⟹ uf,P,t ⊢1 ⟨Var V, s⟩ -ε→ ⟨Val v, s⟩"

| LAss1Red:
"uf,P,t ⊢1 ⟨e, s⟩ -ta→ ⟨e', s'⟩
⟹ uf,P,t ⊢1 ⟨V:=e, s⟩ -ta→ ⟨V:=e', s'⟩"

| Red1LAss:
"V < size l
⟹ uf,P,t ⊢1 ⟨V:=(Val v), (h, l)⟩ -ε→ ⟨unit, (h, l[V := v])⟩"

| AAcc1Red1:
"uf,P,t ⊢1 ⟨a, s⟩ -ta→ ⟨a', s'⟩ ⟹ uf,P,t ⊢1 ⟨a⌊i⌉, s⟩ -ta→ ⟨a'⌊i⌉, s'⟩"

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

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

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

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

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

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

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

| Red1AAssNull:
"uf,P,t ⊢1 ⟨AAss null (Val i) (Val e), s⟩ -ε→ ⟨THROW NullPointer, s⟩"

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

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

| Red1AAss:
"⟦ 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' ⟧
⟹ uf,P,t ⊢1 ⟨AAss (addr a) (Val (Intg i)) (Val w), (h, l)⟩ -⦃WriteMem a (ACell (nat (sint i))) w⦄→ ⟨unit, (h', l)⟩"

| ALength1Red:
"uf,P,t ⊢1 ⟨a, s⟩ -ta→ ⟨a', s'⟩ ⟹ uf,P,t ⊢1 ⟨a∙length, s⟩ -ta→ ⟨a'∙length, s'⟩"

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

| Red1ALengthNull:
"uf,P,t ⊢1 ⟨null∙length, s⟩ -ε→ ⟨THROW NullPointer, s⟩"

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

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

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

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

| FAss1Red2:
"uf,P,t ⊢1 ⟨e, s⟩ -ta→ ⟨e', s'⟩ ⟹ uf,P,t ⊢1 ⟨FAss (Val v) F D e, s⟩ -ta→ ⟨Val v∙F{D}:=e', s'⟩"

| Red1FAss:
"heap_write h a (CField D F) v h' ⟹
uf,P,t ⊢1 ⟨FAss (addr a) F D (Val v), (h, l)⟩ -⦃WriteMem a (CField D F) v⦄→ ⟨unit, (h', l)⟩"

| Red1FAssNull:
"uf,P,t ⊢1 ⟨FAss null F D (Val v), s⟩ -ε→ ⟨THROW NullPointer, s⟩"

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

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

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

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

| Red1CASSucceed:
"⟦ heap_read h a (CField D F) v; heap_write h a (CField D F) v' h' ⟧ ⟹
uf,P,t ⊢1 ⟨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)⟩"

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

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

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

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

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

| Block1Some:
"V < length x ⟹ uf,P,t ⊢1 ⟨{V:T=⌊v⌋; e}, (h, x)⟩ -ε→ ⟨{V:T=None; e}, (h, x[V := v])⟩"

| Block1Red:
"uf,P,t ⊢1 ⟨e, (h, x)⟩ -ta→ ⟨e', (h', x')⟩
⟹ uf,P,t ⊢1 ⟨{V:T=None; e}, (h, x)⟩ -ta→ ⟨{V:T=None; e'}, (h', x')⟩"

| Red1Block:
"uf,P,t ⊢1 ⟨{V:T=None; Val u}, s⟩ -ε→ ⟨Val u, s⟩"

| Synchronized1Red1:
"uf,P,t ⊢1 ⟨o', s⟩ -ta→ ⟨o'', s'⟩ ⟹ uf,P,t ⊢1 ⟨sync⇘V⇙ (o') e, s⟩ -ta→ ⟨sync⇘V⇙ (o'') e, s'⟩"

| Synchronized1Null:
"V < length xs ⟹ uf,P,t ⊢1 ⟨sync⇘V⇙ (null) e, (h, xs)⟩ -ε→ ⟨THROW NullPointer, (h, xs[V := Null])⟩"

| Lock1Synchronized:
"V < length xs ⟹ uf,P,t ⊢1 ⟨sync⇘V⇙ (addr a) e, (h, xs)⟩ -⦃Lock→a, SyncLock a⦄→ ⟨insync⇘V⇙ (a) e, (h, xs[V := Addr a])⟩"

| Synchronized1Red2:
"uf,P,t ⊢1 ⟨e, s⟩ -ta→ ⟨e', s'⟩ ⟹ uf,P,t ⊢1 ⟨insync⇘V⇙ (a) e, s⟩ -ta→ ⟨insync⇘V⇙ (a) e', s'⟩"

| Unlock1Synchronized:
"⟦ xs ! V = Addr a'; V < length xs ⟧ ⟹ uf,P,t ⊢1 ⟨insync⇘V⇙ (a) (Val v), (h, xs)⟩ -⦃Unlock→a', SyncUnlock a'⦄→ ⟨Val v, (h, xs)⟩"

| Unlock1SynchronizedNull:
"⟦ xs ! V = Null; V < length xs ⟧ ⟹ uf,P,t ⊢1 ⟨insync⇘V⇙ (a) (Val v), (h, xs)⟩ -ε→ ⟨THROW NullPointer, (h, xs)⟩"

| Unlock1SynchronizedFail:
"⟦ uf; xs ! V = Addr a'; V < length xs ⟧
⟹ uf,P,t ⊢1 ⟨insync⇘V⇙ (a) (Val v), (h, xs)⟩ -⦃UnlockFail→a'⦄→ ⟨THROW IllegalMonitorState, (h, xs)⟩"

| Seq1Red:
"uf,P,t ⊢1 ⟨e, s⟩ -ta→ ⟨e', s'⟩ ⟹ uf,P,t ⊢1 ⟨e;;e2, s⟩ -ta→ ⟨e';;e2, s'⟩"

| Red1Seq:
"uf,P,t ⊢1 ⟨Seq (Val v) e, s⟩ -ε→ ⟨e, s⟩"

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

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

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

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

| Throw1Red:
"uf,P,t ⊢1 ⟨e, s⟩ -ta→ ⟨e', s'⟩ ⟹ uf,P,t ⊢1 ⟨throw e, s⟩ -ta→ ⟨throw e', s'⟩"

| Red1ThrowNull:
"uf,P,t ⊢1 ⟨throw null, s⟩ -ε→ ⟨THROW NullPointer, s⟩"

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

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

| Red1TryCatch:
"⟦ typeof_addr h a = ⌊Class_type D⌋; P ⊢ D ≼⇧* C; V < length x ⟧
⟹ uf,P,t ⊢1 ⟨try (Throw a) catch(C V) e2, (h, x)⟩ -ε→ ⟨{V:Class C=None; e2}, (h, x[V := Addr a])⟩"

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

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

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

| New1ArrayThrow: "uf,P,t ⊢1 ⟨newA T⌊Throw a⌉, s⟩ -ε→ ⟨Throw a, s⟩"
| Cast1Throw: "uf,P,t ⊢1 ⟨Cast C (Throw a), s⟩ -ε→ ⟨Throw a, s⟩"
| InstanceOf1Throw: "uf,P,t ⊢1 ⟨(Throw a) instanceof T, s⟩ -ε→ ⟨Throw a, s⟩"
| Bin1OpThrow1: "uf,P,t ⊢1 ⟨(Throw a) «bop» e⇩2, s⟩ -ε→ ⟨Throw a, s⟩"
| Bin1OpThrow2: "uf,P,t ⊢1 ⟨(Val v⇩1) «bop» (Throw a), s⟩ -ε→ ⟨Throw a, s⟩"
| LAss1Throw: "uf,P,t ⊢1 ⟨V:=(Throw a), s⟩ -ε→ ⟨Throw a, s⟩"
| AAcc1Throw1: "uf,P,t ⊢1 ⟨(Throw a)⌊i⌉, s⟩ -ε→ ⟨Throw a, s⟩"
| AAcc1Throw2: "uf,P,t ⊢1 ⟨(Val v)⌊Throw a⌉, s⟩ -ε→ ⟨Throw a, s⟩"
| AAss1Throw1: "uf,P,t ⊢1 ⟨(Throw a)⌊i⌉ := e, s⟩ -ε→ ⟨Throw a, s⟩"
| AAss1Throw2: "uf,P,t ⊢1 ⟨(Val v)⌊Throw a⌉ := e, s⟩ -ε→ ⟨Throw a, s⟩"
| AAss1Throw3: "uf,P,t ⊢1 ⟨AAss (Val v) (Val i) (Throw a), s⟩ -ε→ ⟨Throw a, s⟩"
| ALength1Throw: "uf,P,t ⊢1 ⟨(Throw a)∙length, s⟩ -ε→ ⟨Throw a, s⟩"
| FAcc1Throw: "uf,P,t ⊢1 ⟨(Throw a)∙F{D}, s⟩ -ε→ ⟨Throw a, s⟩"
| FAss1Throw1: "uf,P,t ⊢1 ⟨(Throw a)∙F{D}:=e⇩2, s⟩ -ε→ ⟨Throw a, s⟩"
| FAss1Throw2: "uf,P,t ⊢1 ⟨FAss (Val v) F D (Throw a), s⟩ -ε→ ⟨Throw a, s⟩"
| CAS1Throw: "uf,P,t ⊢1 ⟨Throw a∙compareAndSwap(D∙F, e2, e3), s⟩ -ε→ ⟨Throw a, s⟩"
| CAS1Throw2: "uf,P,t ⊢1 ⟨Val v∙compareAndSwap(D∙F, Throw a, e3), s⟩ -ε→ ⟨Throw a, s⟩"
| CAS1Throw3: "uf,P,t ⊢1 ⟨Val v∙compareAndSwap(D∙F, Val v', Throw a), s⟩ -ε→ ⟨Throw a, s⟩"
| Call1ThrowObj: "uf,P,t ⊢1 ⟨(Throw a)∙M(es), s⟩ -ε→ ⟨Throw a, s⟩"
| Call1ThrowParams: "⟦ es = map Val vs @ Throw a # es' ⟧ ⟹ uf,P,t ⊢1 ⟨(Val v)∙M(es), s⟩ -ε→ ⟨Throw a, s⟩"
| Block1Throw: "uf,P,t ⊢1 ⟨{V:T=None; Throw a}, s⟩ -ε→ ⟨Throw a, s⟩"
| Synchronized1Throw1: "uf,P,t ⊢1 ⟨sync⇘V⇙ (Throw a) e, s⟩ -ε→ ⟨Throw a, s⟩"
| Synchronized1Throw2:
"⟦ xs ! V = Addr a'; V < length xs ⟧
⟹ uf,P,t ⊢1 ⟨insync⇘V⇙ (a) Throw ad, (h, xs)⟩ -⦃Unlock→a', SyncUnlock a'⦄→ ⟨Throw ad, (h, xs)⟩"
| Synchronized1Throw2Fail:
"⟦ uf; xs ! V = Addr a'; V < length xs ⟧
⟹ uf,P,t ⊢1 ⟨insync⇘V⇙ (a) Throw ad, (h, xs)⟩ -⦃UnlockFail→a'⦄→ ⟨THROW IllegalMonitorState, (h, xs)⟩"
| Synchronized1Throw2Null:
"⟦ xs ! V = Null; V < length xs ⟧
⟹ uf,P,t ⊢1 ⟨insync⇘V⇙ (a) Throw ad, (h, xs)⟩ -ε→ ⟨THROW NullPointer, (h, xs)⟩"
| Seq1Throw: "uf,P,t ⊢1 ⟨(Throw a);;e⇩2, s⟩ -ε→ ⟨Throw a, s⟩"
| Cond1Throw: "uf,P,t ⊢1 ⟨if (Throw a) e⇩1 else e⇩2, s⟩ -ε→ ⟨Throw a, s⟩"
| Throw1Throw: "uf,P,t ⊢1 ⟨throw(Throw a), s⟩ -ε→ ⟨Throw a, s⟩"

inductive_cases red1_cases:
"uf,P,t ⊢1 ⟨new C, s⟩ -ta→ ⟨e', s'⟩"
"uf,P,t ⊢1 ⟨new T⌊e⌉, s⟩ -ta→ ⟨e', s'⟩"
"uf,P,t ⊢1 ⟨e «bop» e', s⟩ -ta→ ⟨e'', s'⟩"
"uf,P,t ⊢1 ⟨Var V, s⟩ -ta→ ⟨e', s'⟩"
"uf,P,t ⊢1 ⟨V:=e, s⟩ -ta→ ⟨e', s'⟩"
"uf,P,t ⊢1 ⟨a⌊i⌉, s⟩ -ta→ ⟨e', s'⟩"
"uf,P,t ⊢1 ⟨a⌊i⌉ := e, s⟩ -ta→ ⟨e', s'⟩"
"uf,P,t ⊢1 ⟨a∙length, s⟩ -ta→ ⟨e', s'⟩"
"uf,P,t ⊢1 ⟨e∙F{D}, s⟩ -ta→ ⟨e', s'⟩"
"uf,P,t ⊢1 ⟨e∙F{D} := e2, s⟩ -ta→ ⟨e', s'⟩"
"uf,P,t ⊢1 ⟨e∙compareAndSwap(D∙F, e', e''), s⟩ -ta→ ⟨e''', s'⟩"
"uf,P,t ⊢1 ⟨e∙M(es), s⟩ -ta→ ⟨e', s'⟩"
"uf,P,t ⊢1 ⟨{V:T=vo; e}, s⟩ -ta→ ⟨e', s'⟩"
"uf,P,t ⊢1 ⟨sync⇘V⇙ (o') e, s⟩ -ta→ ⟨e', s'⟩"
"uf,P,t ⊢1 ⟨insync⇘V⇙ (a) e, s⟩ -ta→ ⟨e', s'⟩"
"uf,P,t ⊢1 ⟨e;;e', s⟩ -ta→ ⟨e'', s'⟩"
"uf,P,t ⊢1 ⟨throw e, s ⟩ -ta→ ⟨e', s'⟩"
"uf,P,t ⊢1 ⟨try e catch(C V) e'', s ⟩ -ta→ ⟨e', s'⟩"

inductive Red1 ::
("_,_,_ ⊢1 ((1⟨_'/_,/_⟩) -_→/ (1⟨_'/_,/_⟩))" [51,51,0,0,0,0,0,0,0,0] 81)
for uf :: bool and P :: "'addr J1_prog" and t :: 'thread_id
where

red1Red:
"uf,P,t ⊢1 ⟨e, (h, x)⟩ -ta→ ⟨e', (h', x')⟩
⟹ uf,P,t ⊢1 ⟨(e, x)/exs, h⟩ -extTA2J1 P ta→ ⟨(e', x')/exs, h'⟩"

| red1Call:
"⟦ call1 e = ⌊(a, M, vs)⌋; typeof_addr h a = ⌊U⌋;
P ⊢ class_type_of U sees M:Ts→T = ⌊body⌋ in D;
size vs = size Ts ⟧
⟹ uf,P,t ⊢1 ⟨(e, x)/exs, h⟩ -ε→ ⟨(blocks1 0 (Class D#Ts) body, Addr a # vs @ replicate (max_vars body) undefined_value)/(e, x)#exs, h⟩"

| red1Return:
"final e' ⟹ uf,P,t ⊢1 ⟨(e', x')/(e, x)#exs, h⟩ -ε→ ⟨(inline_call e' e, x)/exs, h⟩"

where "mred1g uf P ≡ λt ((ex, exs), h) ta ((ex', exs'), h'). uf,P,t ⊢1 ⟨ex/exs, h⟩ -ta→ ⟨ex'/exs', h'⟩"

abbreviation mred1' ::
where "mred1' ≡ mred1g False"

abbreviation mred1 ::
where "mred1 ≡ mred1g True"

lemma red1_preserves_len: "uf,P,t ⊢1 ⟨e, s⟩ -ta→ ⟨e', s'⟩ ⟹ length (lcl s') = length (lcl s)"
and reds1_preserves_len: "uf,P,t ⊢1 ⟨es, s⟩ [-ta→] ⟨es', s'⟩ ⟹ length (lcl s') = length (lcl s)"
by(induct rule: red1_reds1.inducts)(auto)

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

lemma red1_Val_iff [iff]:
"¬ uf,P,t ⊢1 ⟨Val v, s⟩ -ta→ ⟨e', s'⟩"
by(auto elim: red1.cases)

lemma red1_Throw_iff [iff]:
"¬ uf,P,t ⊢1 ⟨Throw a, xs⟩ -ta→ ⟨e', s'⟩"
by(auto elim: red1.cases)

lemma reds1_Nil_iff [iff]:
"¬ uf,P,t ⊢1 ⟨[], s⟩ [-ta→] ⟨es', s'⟩"
by(auto elim: reds1.cases)

lemma reds1_Val_iff [iff]:
"¬ uf,P,t ⊢1 ⟨map Val vs, s⟩ [-ta→] ⟨es', s'⟩"
by(induct vs arbitrary: es')(auto elim: reds1.cases)

lemma reds1_map_Val_Throw_iff [iff]:
"¬ uf,P,t ⊢1 ⟨map Val vs @ Throw a # es, s⟩ [-ta→] ⟨es', s'⟩"
by(induct vs arbitrary: es')(auto elim: reds1.cases elim!: red1_cases)

lemma red1_max_vars_decr: "uf,P,t ⊢1 ⟨e, s⟩ -ta→ ⟨e', s'⟩ ⟹ max_vars e' ≤ max_vars e"
by(induct rule: red1_reds1.inducts)(auto)

lemma red1_new_thread_heap: "⟦uf,P,t ⊢1 ⟨e, s⟩ -ta→ ⟨e', s'⟩; NewThread t' ex h ∈ set ⦃ta⦄⇘t⇙ ⟧ ⟹ h = hp s'"
and reds1_new_thread_heap: "⟦uf,P,t ⊢1 ⟨es, s⟩ [-ta→] ⟨es', s'⟩; NewThread t' ex h ∈ set ⦃ta⦄⇘t⇙ ⟧ ⟹ h = hp s'"
apply(induct rule: red1_reds1.inducts)
done

"⟦ uf,P,t ⊢1 ⟨e, s⟩ -ta→ ⟨e', s'⟩; NewThread t' x H ∈ set ⦃ta⦄⇘t⇙ ⟧
⟹ ∃a M vs va T Ts Tr D. P,t ⊢ ⟨a∙M(vs), hp s⟩ -ta→ext ⟨va, hp s'⟩ ∧ typeof_addr (hp s) a = ⌊T⌋ ∧ P ⊢ class_type_of T sees M:Ts→Tr = Native in D"
"⟦ uf,P,t ⊢1 ⟨es, s⟩ [-ta→] ⟨es', s'⟩; NewThread t' x H ∈ set ⦃ta⦄⇘t⇙ ⟧
⟹ ∃a M vs va T Ts Tr D. P,t ⊢ ⟨a∙M(vs), hp s⟩ -ta→ext ⟨va, hp s'⟩ ∧ typeof_addr (hp s) a = ⌊T⌋ ∧ P ⊢ class_type_of T sees M:Ts→Tr = Native in D"
by(induct rule: red1_reds1.inducts)(fastforce simp add: ta_upd_simps)+

lemma red1_call_synthesized: "⟦ uf,P,t ⊢1 ⟨e, s⟩ -ta→ ⟨e', s'⟩; call1 e = ⌊aMvs⌋ ⟧ ⟹ synthesized_call P (hp s) aMvs"
and reds1_calls_synthesized: "⟦ uf,P,t ⊢1 ⟨es, s⟩ [-ta→] ⟨es', s'⟩; calls1 es = ⌊aMvs⌋ ⟧ ⟹ synthesized_call P (hp s) aMvs"
apply(induct rule: red1_reds1.inducts)
apply(auto split: if_split_asm simp add: is_vals_conv append_eq_map_conv synthesized_call_conv)
apply blast
done

lemma red1_preserves_B: "⟦ uf,P,t ⊢1 ⟨e, s⟩ -ta→ ⟨e', s'⟩; ℬ e n⟧ ⟹ ℬ e' n"
and reds1_preserves_Bs: "⟦ uf,P,t ⊢1 ⟨es, s⟩ [-ta→] ⟨es', s'⟩; ℬs es n⟧ ⟹ ℬs es' n"
by(induct arbitrary: n and n rule: red1_reds1.inducts)(auto)

end

context J1_heap begin

lemma red1_hext_incr: "uf,P,t ⊢1 ⟨e, s⟩ -ta→ ⟨e', s'⟩ ⟹ hext (hp s) (hp s')"
and reds1_hext_incr: "uf,P,t ⊢1 ⟨es, s⟩ [-ta→] ⟨es', s'⟩ ⟹ hext (hp s) (hp s')"
by(induct rule: red1_reds1.inducts)(auto intro: hext_heap_ops red_external_hext)

lemma Red1_hext_incr: "uf,P,t ⊢1 ⟨ex/exs,h⟩ -ta→ ⟨ex'/exs',h'⟩ ⟹ h ⊴ h'"
by(auto elim!: Red1.cases dest: red1_hext_incr)

end

subsection ‹Silent moves›

context J1_heap_base begin

primrec τmove1 :: "'m prog ⇒ 'heap ⇒ ('a, 'b, 'addr) exp ⇒ bool"
and τmoves1 :: "'m prog ⇒ 'heap ⇒ ('a, 'b, 'addr) exp list ⇒ bool"
where
"τmove1 P h (new C) ⟷ False"
| "τmove1 P h (newA T⌊e⌉) ⟷ τmove1 P h e ∨ (∃a. e = Throw a)"
| "τmove1 P h (Cast U e) ⟷ τmove1 P h e ∨ final e"
| "τmove1 P h (e instanceof T) ⟷ τmove1 P h e ∨ final e"
| "τmove1 P h (e «bop» e') ⟷ τmove1 P h e ∨ (∃a. e = Throw a) ∨ (∃v. e = Val v ∧ (τmove1 P h e' ∨ final e'))"
| "τmove1 P h (Val v) ⟷ False"
| "τmove1 P h (Var V) ⟷ True"
| "τmove1 P h (V := e) ⟷ τmove1 P h e ∨ final e"
| "τmove1 P h (a⌊i⌉) ⟷ τmove1 P h a ∨ (∃ad. a = Throw ad) ∨ (∃v. a = Val v ∧ (τmove1 P h i ∨ (∃a. i = Throw a)))"
| "τmove1 P h (AAss a i e) ⟷ τmove1 P h a ∨ (∃ad. a = Throw ad) ∨ (∃v. a = Val v ∧ (τmove1 P h i ∨ (∃a. i = Throw a) ∨ (∃v. i = Val v ∧ (τmove1 P h e ∨ (∃a. e = Throw a)))))"
| "τmove1 P h (a∙length) ⟷ τmove1 P h a ∨ (∃ad. a = Throw ad)"
| "τmove1 P h (e∙F{D}) ⟷ τmove1 P h e ∨ (∃a. e = Throw a)"
| "τmove1 P h (FAss e F D e') ⟷ τmove1 P h e ∨ (∃a. e = Throw a) ∨ (∃v. e = Val v ∧ (τmove1 P h e' ∨ (∃a. e' = Throw a)))"
| "τmove1 P h (e∙compareAndSwap(D∙F, e', e'')) ⟷ τmove1 P h e ∨ (∃a. e = Throw a) ∨ (∃v. e = Val v ∧
(τmove1 P h e' ∨ (∃a. e' = Throw a) ∨ (∃v. e' = Val v ∧ (τmove1 P h e'' ∨ (∃a. e'' = Throw a)))))"
| "τmove1 P h (e∙M(es)) ⟷ τmove1 P h e ∨ (∃a. e = Throw a) ∨ (∃v. e = Val v ∧
(τmoves1 P h es ∨ (∃vs a es'. es = map Val vs @ Throw a # es') ∨
(∃vs. es = map Val vs ∧ (v = Null ∨ (∀T C Ts Tr D. typeof⇘h⇙ v = ⌊T⌋ ⟶ class_type_of' T = ⌊C⌋ ⟶ P ⊢ C sees M:Ts→Tr = Native in D ⟶ τexternal_defs D M)))))"
| "τmove1 P h ({V:T=vo; e}) ⟷ vo ≠ None ∨ τmove1 P h e ∨ final e"
| "τmove1 P h (sync⇘V'⇙(e) e') ⟷ τmove1 P h e ∨ (∃a. e = Throw a)"
| "τmove1 P h (insync⇘V'⇙(ad) e) ⟷ τmove1 P h e"
| "τmove1 P h (e;;e') ⟷ τmove1 P h e ∨ final e"
| "τmove1 P h (if (e) e' else e'') ⟷ τmove1 P h e ∨ final e"
| "τmove1 P h (while (e) e') = True"
| "τmove1 P h (throw e) ⟷ τmove1 P h e ∨ (∃a. e = Throw a) ∨ e = null"
| "τmove1 P h (try e catch(C V) e') ⟷ τmove1 P h e ∨ final e"

| "τmoves1 P h [] ⟷ False"
| "τmoves1 P h (e # es) ⟷ τmove1 P h e ∨ (∃v. e = Val v ∧ τmoves1 P h es)"

fun τMove1 :: "'m prog ⇒ 'heap ⇒ (('a, 'b, 'addr) exp × 'c) × (('a, 'b, 'addr) exp × 'd) list ⇒ bool"
where
"τMove1 P h ((e, x), exs) = (τmove1 P h e ∨ final e)"

where "τred1g uf P t h exs e'xs' = (uf,P,t ⊢1 ⟨fst exs, (h, snd exs)⟩ -ε→ ⟨fst e'xs', (h, snd e'xs')⟩ ∧ τmove1 P h (fst exs))"

definition τreds1g ::
where
"τreds1g uf P t h esxs es'xs' =
(uf,P,t ⊢1 ⟨fst esxs, (h, snd esxs)⟩ [-ε→] ⟨fst es'xs', (h, snd es'xs')⟩ ∧ τmoves1 P h (fst esxs))"

abbreviation τred1gt ::
where "τred1gt uf P t h ≡ (τred1g uf P t h)^++"

abbreviation τreds1gt ::
where "τreds1gt uf P t h ≡ (τreds1g uf P t h)^++"

abbreviation τred1gr ::
where "τred1gr uf P t h ≡ (τred1g uf P t h)^**"

abbreviation τreds1gr ::
where "τreds1gr uf P t h ≡ (τreds1g uf P t h)^**"

definition τRed1g ::
where "τRed1g uf P t h exexs ex'exs' = (uf,P,t ⊢1 ⟨fst exexs/snd exexs, h⟩ -ε→ ⟨fst ex'exs'/snd ex'exs', h⟩ ∧ τMove1 P h exexs)"

abbreviation τRed1gt ::
where "τRed1gt uf P t h ≡ (τRed1g uf P t h)^++"

abbreviation τRed1gr ::
where "τRed1gr uf P t h ≡ (τRed1g uf P t h)^**"

abbreviation τred1 ::
where "τred1 ≡ τred1g True"

abbreviation τreds1 ::
where "τreds1 ≡ τreds1g True"

abbreviation τred1t ::
where "τred1t ≡ τred1gt True"

abbreviation τreds1t ::
where "τreds1t ≡ τreds1gt True"

abbreviation τred1r ::
where "τred1r ≡ τred1gr True"

abbreviation τreds1r ::
where "τreds1r ≡ τreds1gr True"

abbreviation τRed1 ::
where "τRed1 ≡ τRed1g True"

abbreviation τRed1t ::
where "τRed1t ≡ τRed1gt True"

abbreviation τRed1r ::
where "τRed1r ≡ τRed1gr True"

abbreviation τred1' ::
where "τred1' ≡ τred1g False"

abbreviation τreds1' ::
where "τreds1' ≡ τreds1g False"

abbreviation τred1't ::
where "τred1't ≡ τred1gt False"

abbreviation τreds1't ::
where "τreds1't ≡ τreds1gt False"

abbreviation τred1'r ::
where "τred1'r ≡ τred1gr False"

abbreviation τreds1'r ::
where "τreds1'r ≡ τreds1gr False"

abbreviation τRed1' ::
where "τRed1' ≡ τRed1g False"

abbreviation τRed1't ::
where "τRed1't ≡ τRed1gt False"

abbreviation τRed1'r ::
where "τRed1'r ≡ τRed1gr False"

abbreviation τMOVE1 ::
where "τMOVE1 P ≡ λ(exexs, h) ta s. τMove1 P h exexs ∧ ta = ε"

lemma τmove1_τmoves1_intros:
fixes e :: "('a, 'b, 'addr) exp" and es :: "('a, 'b, 'addr) exp list"
shows τmove1NewArray: "τmove1 P h e ⟹ τmove1 P h (newA T⌊e⌉)"
and τmove1Cast: "τmove1 P h e ⟹ τmove1 P h (Cast U e)"
and τmove1CastRed: "τmove1 P h (Cast U (Val v))"
and τmove1InstanceOf: "τmove1 P h e ⟹ τmove1 P h (e instanceof U)"
and τmove1InstanceOfRed: "τmove1 P h ((Val v) instanceof U)"
and τmove1BinOp1: "τmove1 P h e ⟹ τmove1 P h (e«bop»e')"
and τmove1BinOp2: "τmove1 P h e ⟹ τmove1 P h (Val v«bop»e)"
and τmove1BinOp: "τmove1 P h (Val v«bop»Val v')"
and τmove1Var: "τmove1 P h (Var V)"
and τmove1LAss: "τmove1 P h e ⟹ τmove1 P h (V := e)"
and τmove1LAssRed: "τmove1 P h (V := Val v)"
and τmove1AAcc1: "τmove1 P h e ⟹ τmove1 P h (e⌊e'⌉)"
and τmove1AAcc2: "τmove1 P h e ⟹ τmove1 P h (Val v⌊e⌉)"
and τmove1AAss1: "τmove1 P h e ⟹ τmove1 P h (AAss e e' e'')"
and τmove1AAss2: "τmove1 P h e ⟹ τmove1 P h (AAss (Val v) e e')"
and τmove1AAss3: "τmove1 P h e ⟹ τmove1 P h (AAss (Val v) (Val v') e)"
and τmove1ALength: "τmove1 P h e ⟹ τmove1 P h (e∙length)"
and τmove1FAcc: "τmove1 P h e ⟹ τmove1 P h (e∙F{D})"
and τmove1FAss1: "τmove1 P h e ⟹ τmove1 P h (FAss e F D e')"
and τmove1FAss2: "τmove1 P h e ⟹ τmove1 P h (FAss (Val v) F D e)"
and τmove1CAS1: "τmove1 P h e ⟹ τmove1 P h (e∙compareAndSwap(D∙F, e', e''))"
and τmove1CAS2: "τmove1 P h e ⟹ τmove1 P h (Val v∙compareAndSwap(D∙F, e, e''))"
and τmove1CAS3: "τmove1 P h e ⟹ τmove1 P h (Val v∙compareAndSwap(D∙F, Val v', e))"
and τmove1CallObj: "τmove1 P h obj ⟹ τmove1 P h (obj∙M(ps))"
and τmove1CallParams: "τmoves1 P h ps ⟹ τmove1 P h (Val v∙M(ps))"
and τmove1Call: "(⋀T C Ts Tr D. ⟦ typeof⇘h⇙ v = ⌊T⌋; class_type_of' T = ⌊C⌋; P ⊢ C sees M:Ts→Tr = Native in D ⟧ ⟹ τexternal_defs D M) ⟹ τmove1 P h (Val v∙M(map Val vs))"
and τmove1BlockSome: "τmove1 P h {V:T=⌊v⌋; e}"
and τmove1Block: "τmove1 P h e ⟹ τmove1 P h {V:T=None; e}"
and τmove1BlockRed: "τmove1 P h {V:T=None; Val v}"
and τmove1Sync: "τmove1 P h e ⟹ τmove1 P h (sync⇘V'⇙ (e) e')"
and τmove1InSync: "τmove1 P h e ⟹ τmove1 P h (insync⇘V'⇙ (a) e)"
and τmove1Seq: "τmove1 P h e ⟹ τmove1 P h (e;;e')"
and τmove1SeqRed: "τmove1 P h (Val v;; e)"
and τmove1Cond: "τmove1 P h e ⟹ τmove1 P h (if (e) e1 else e2)"
and τmove1CondRed: "τmove1 P h (if (Val v) e1 else e2)"
and τmove1WhileRed: "τmove1 P h (while (c) e)"
and τmove1Throw: "τmove1 P h e ⟹ τmove1 P h (throw e)"
and τmove1ThrowNull: "τmove1 P h (throw null)"
and τmove1Try: "τmove1 P h e ⟹ τmove1 P h (try e catch(C V) e'')"
and τmove1TryRed: "τmove1 P h (try Val v catch(C V) e)"
and τmove1TryThrow: "τmove1 P h (try Throw a catch(C V) e)"
and τmove1NewArrayThrow: "τmove1 P h (newA T⌊Throw a⌉)"
and τmove1CastThrow: "τmove1 P h (Cast T (Throw a))"
and τmove1InstanceOfThrow: "τmove1 P h ((Throw a) instanceof T)"
and τmove1BinOpThrow1: "τmove1 P h (Throw a «bop» e2)"
and τmove1BinOpThrow2: "τmove1 P h (Val v «bop» Throw a)"
and τmove1LAssThrow: "τmove1 P h (V:=(Throw a))"
and τmove1AAccThrow1: "τmove1 P h (Throw a⌊e⌉)"
and τmove1AAccThrow2: "τmove1 P h (Val v⌊Throw a⌉)"
and τmove1AAssThrow1: "τmove1 P h (AAss (Throw a) e e')"
and τmove1AAssThrow2: "τmove1 P h (AAss (Val v) (Throw a) e')"
and τmove1AAssThrow3: "τmove1 P h (AAss (Val v) (Val v') (Throw a))"
and τmove1ALengthThrow: "τmove1 P h (Throw a∙length)"
and τmove1FAccThrow: "τmove1 P h (Throw a∙F{D})"
and τmove1FAssThrow1: "τmove1 P h (Throw a∙F{D} := e)"
and τmove1FAssThrow2: "τmove1 P h (FAss (Val v) F D (Throw a))"
and τmove1CASThrow1: "τmove1 P h (CompareAndSwap (Throw a) D F e e')"
and τmove1CASThrow2: "τmove1 P h (CompareAndSwap (Val v) D F (Throw a) e')"
and τmove1CASThrow3: "τmove1 P h (CompareAndSwap (Val v) D F (Val v') (Throw a))"
and τmove1CallThrowObj: "τmove1 P h (Throw a∙M(es))"
and τmove1CallThrowParams: "τmove1 P h (Val v∙M(map Val vs @ Throw a # es))"
and τmove1BlockThrow: "τmove1 P h {V:T=None; Throw a}"
and τmove1SyncThrow: "τmove1 P h (sync⇘V'⇙ (Throw a) e)"
and τmove1SeqThrow: "τmove1 P h (Throw a;;e)"
and τmove1CondThrow: "τmove1 P h (if (Throw a) e1 else e2)"
and τmove1ThrowThrow: "τmove1 P h (throw (Throw a))"

and τmoves1Hd: "τmove1 P h e ⟹ τmoves1 P h (e # es)"
and τmoves1Tl: "τmoves1 P h es ⟹ τmoves1 P h (Val v # es)"
by fastforce+

lemma τmoves1_map_Val [dest!]:
"τmoves1 P h (map Val es) ⟹ False"
by(induct es)(auto)

lemma τmoves1_map_Val_ThrowD [simp]: "τmoves1 P h (map Val vs @ Throw a # es) = False"
by(induct vs)(fastforce)+

lemma fixes e :: "('a, 'b, 'addr) exp" and es :: "('a, 'b, 'addr) exp list"
shows τmove1_not_call1:
"call1 e = ⌊(a, M, vs)⌋ ⟹ τmove1 P h e ⟷ (synthesized_call P h (a, M, vs) ⟶ τexternal' P h a M)"
and τmoves1_not_calls1:
"calls1 es = ⌊(a, M, vs)⌋ ⟹ τmoves1 P h es ⟷ (synthesized_call P h (a, M, vs) ⟶ τexternal' P h a M)"
apply(induct e and es rule: call1.induct calls1.induct)
apply(auto split: if_split_asm simp add: is_vals_conv)
apply(fastforce simp add: synthesized_call_def map_eq_append_conv τexternal'_def τexternal_def dest: sees_method_fun)+
done

lemma red1_τ_taD: "⟦ uf,P,t ⊢1 ⟨e, s⟩ -ta→ ⟨e', s'⟩; τmove1 P (hp s) e ⟧ ⟹ ta = ε"
and reds1_τ_taD: "⟦ uf,P,t ⊢1 ⟨es, s⟩ [-ta→] ⟨es', s'⟩; τmoves1 P (hp s) es ⟧ ⟹ ta = ε"
apply(induct rule: red1_reds1.inducts)
apply(fastforce simp add: map_eq_append_conv τexternal'_def τexternal_def dest: τexternal'_red_external_TA_empty)+
done

lemma τmove1_heap_unchanged: "⟦ uf,P,t ⊢1 ⟨e, s⟩ -ta→ ⟨e', s'⟩; τmove1 P (hp s) e ⟧ ⟹ hp s' = hp s"
and τmoves1_heap_unchanged: "⟦ uf,P,t ⊢1 ⟨es, s⟩ [-ta→] ⟨es', s'⟩; τmoves1 P (hp s) es ⟧ ⟹ hp s' = hp s"
apply(induct rule: red1_reds1.inducts)
apply(auto)
apply(fastforce simp add: map_eq_append_conv τexternal'_def τexternal_def dest: τexternal'_red_external_heap_unchanged)+
done

lemma τMove1_iff:
"τMove1 P h exexs ⟷ (let ((e, _), _) = exexs in τmove1 P h e ∨ final e)"
by(cases exexs)(auto)

lemma τred1_iff [iff]:
"τred1g uf P t h (e, xs) (e', xs') = (uf,P,t ⊢1 ⟨e, (h, xs)⟩ -ε→ ⟨e', (h, xs')⟩ ∧ τmove1 P h e)"

lemma τreds1_iff [iff]:
"τreds1g uf P t h (es, xs) (es', xs') = (uf,P,t ⊢1 ⟨es, (h, xs)⟩ [-ε→] ⟨es', (h, xs')⟩ ∧ τmoves1 P h es)"

lemma τred1t_1step:
"⟦ uf,P,t ⊢1 ⟨e, (h, xs)⟩ -ε→ ⟨e', (h, xs')⟩; τmove1 P h e ⟧
⟹ τred1gt uf P t h (e, xs) (e', xs')"
by(blast intro: tranclp.r_into_trancl)

lemma τred1t_2step:
"⟦ uf,P,t ⊢1 ⟨e, (h, xs)⟩ -ε→ ⟨e', (h, xs')⟩; τmove1 P h e;
uf,P,t ⊢1 ⟨e', (h, xs')⟩ -ε→ ⟨e'', (h, xs'')⟩; τmove1 P h e' ⟧
⟹ τred1gt uf P t h (e, xs) (e'', xs'')"
by(blast intro: tranclp.trancl_into_trancl[OF τred1t_1step])

lemma τred1t_3step:
"⟦ uf,P,t ⊢1 ⟨e, (h, xs)⟩ -ε→ ⟨e', (h, xs')⟩; τmove1 P h e;
uf,P,t ⊢1 ⟨e', (h, xs')⟩ -ε→ ⟨e'', (h, xs'')⟩; τmove1 P h e';
uf,P,t ⊢1 ⟨e'', (h, xs'')⟩ -ε→ ⟨e''', (h, xs''')⟩; τmove1 P h e'' ⟧
⟹ τred1gt uf P t h (e, xs) (e''', xs''')"
by(blast intro: tranclp.trancl_into_trancl[OF τred1t_2step])

lemma τreds1t_1step:
"⟦ uf,P,t ⊢1 ⟨es, (h, xs)⟩ [-ε→] ⟨es', (h, xs')⟩; τmoves1 P h es ⟧
⟹ τreds1gt uf P t h (es, xs) (es', xs')"
by(blast intro: tranclp.r_into_trancl)

lemma τreds1t_2step:
"⟦ uf,P,t ⊢1 ⟨es, (h, xs)⟩ [-ε→] ⟨es', (h, xs')⟩; τmoves1 P h es;
uf,P,t ⊢1 ⟨es', (h, xs')⟩ [-ε→] ⟨es'', (h, xs'')⟩; τmoves1 P h es' ⟧
⟹ τreds1gt uf P t h (es, xs) (es'', xs'')"
by(blast intro: tranclp.trancl_into_trancl[OF τreds1t_1step])

lemma τreds1t_3step:
"⟦ uf,P,t ⊢1 ⟨es, (h, xs)⟩ [-ε→] ⟨es', (h, xs')⟩; τmoves1 P h es;
uf,P,t ⊢1 ⟨es', (h, xs')⟩ [-ε→] ⟨es'', (h, xs'')⟩; τmoves1 P h es';
uf,P,t ⊢1 ⟨es'', (h, xs'')⟩ [-ε→] ⟨es''', (h, xs''')⟩; τmoves1 P h es'' ⟧
⟹ τreds1gt uf P t h (es, xs) (es''', xs''')"
by(blast intro: tranclp.trancl_into_trancl[OF τreds1t_2step])

lemma τred1r_1step:
"⟦ uf,P,t ⊢1 ⟨e, (h, xs)⟩ -ε→ ⟨e', (h, xs')⟩; τmove1 P h e ⟧
⟹ τred1gr uf P t h (e, xs) (e', xs')"
by(blast intro: r_into_rtranclp)

lemma τred1r_2step:
"⟦ uf,P,t ⊢1 ⟨e, (h, xs)⟩ -ε→ ⟨e', (h, xs')⟩; τmove1 P h e;
uf,P,t ⊢1 ⟨e', (h, xs')⟩ -ε→ ⟨e'', (h, xs'')⟩; τmove1 P h e' ⟧
⟹ τred1gr uf P t h (e, xs) (e'', xs'')"
by(blast intro: rtranclp.rtrancl_into_rtrancl[OF τred1r_1step])

lemma τred1r_3step:
"⟦ uf,P,t ⊢1 ⟨e, (h, xs)⟩ -ε→ ⟨e', (h, xs')⟩; τmove1 P h e;
uf,P,t ⊢1 ⟨e', (h, xs')⟩ -ε→ ⟨e'', (h, xs'')⟩; τmove1 P h e';
uf,P,t ⊢1 ⟨e'', (h, xs'')⟩ -ε→ ⟨e''', (h, xs''')⟩; τmove1 P h e'' ⟧
⟹ τred1gr uf P t h (e, xs) (e''', xs''')"
by(blast intro: rtranclp.rtrancl_into_rtrancl[OF τred1r_2step])

lemma τreds1r_1step:
"⟦ uf,P,t ⊢1 ⟨es, (h, xs)⟩ [-ε→] ⟨es', (h, xs')⟩; τmoves1 P h es ⟧
⟹ τreds1gr uf P t h (es, xs) (es', xs')"
by(blast intro: r_into_rtranclp)

lemma τreds1r_2step:
"⟦ uf,P,t ⊢1 ⟨es, (h, xs)⟩ [-ε→] ⟨es', (h, xs')⟩; τmoves1 P h es;
uf,P,t ⊢1 ⟨es', (h, xs')⟩ [-ε→] ⟨es'', (h, xs'')⟩; τmoves1 P h es' ⟧
⟹ τreds1gr uf P t h (es, xs) (es'', xs'')"
by(blast intro: rtranclp.rtrancl_into_rtrancl[OF τreds1r_1step])

lemma τreds1r_3step:
"⟦ uf,P,t ⊢1 ⟨es, (h, xs)⟩ [-ε→] ⟨es', (h, xs')⟩; τmoves1 P h es;
uf,P,t ⊢1 ⟨es', (h, xs')⟩ [-ε→] ⟨es'', (h, xs'')⟩; τmoves1 P h es';
uf,P,t ⊢1 ⟨es'', (h, xs'')⟩ [-ε→] ⟨es''', (h, xs''')⟩; τmoves1 P h es'' ⟧
⟹ τreds1gr uf P t h (es, xs) (es''', xs''')"
by(blast intro: rtranclp.rtrancl_into_rtrancl[OF τreds1r_2step])

lemma τred1t_preserves_len: "τred1gt uf P t h (e, xs) (e', xs') ⟹ length xs' = length xs"
by(induct rule: tranclp_induct2)(auto dest: red1_preserves_len)

lemma τred1r_preserves_len: "τred1gr uf P t h (e, xs) (e', xs') ⟹ length xs' = length xs"
by(induct rule: rtranclp_induct2)(auto dest: red1_preserves_len)

lemma τred1t_inj_τreds1t: "τred1gt uf P t h (e, xs) (e', xs') ⟹ τreds1gt uf P t h (e # es, xs) (e' # es, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl List1Red1 τmoves1Hd)

lemma ```