Theory J1

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

section ‹Semantics of the intermediate language›

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

abbreviation final_expr1 :: "('addr expr1 × 'addr locals1) × ('addr expr1 × 'addr locals1) list ⇒ bool" where
  "final_expr1 ≡ λ(ex, exs). final (fst ex) ∧ exs = []"

definition extNTA2J1 :: 
  "'addr J1_prog ⇒ (cname × mname × 'addr) ⇒ (('addr expr1 × 'addr locals1) × ('addr expr1 × 'addr locals1) list)"
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), [])"
by(simp add: extNTA2J1_def split_beta)

abbreviation extTA2J1 :: 
  "'addr J1_prog ⇒ ('addr, 'thread_id, 'heap) external_thread_action ⇒ ('addr, 'thread_id, 'heap) J1_thread_action"
where "extTA2J1 P ≡ convert_extTA (extNTA2J1 P)"

abbreviation (input) extRet2J1 :: "'addr expr1 ⇒ 'addr extCallRet ⇒ 'addr expr1"
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

abbreviation J1_start_state :: "'addr J1_prog ⇒ cname ⇒ mname ⇒ 'addr val list ⇒ ('addr, 'thread_id, 'heap) J1_state"
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 :: 
  "bool ⇒ 'addr J1_prog ⇒ 'thread_id ⇒ 'addr expr1 ⇒ 'heap × 'addr locals1 
  ⇒ ('addr, 'thread_id, 'heap) external_thread_action ⇒ 'addr expr1 ⇒ 'heap × 'addr locals1 ⇒ bool"
  (‹_,_,_ ⊢1 ((1⟨_,/_⟩) -_→/ (1⟨_,/_⟩))› [51,51,0,0,0,0,0,0] 81)
  and reds1 ::
  "bool ⇒ 'addr J1_prog ⇒ 'thread_id ⇒ 'addr expr1 list ⇒ 'heap × 'addr locals1
  ⇒ ('addr, 'thread_id, 'heap) external_thread_action ⇒ 'addr expr1 list ⇒ 'heap × 'addr locals1 ⇒ bool"
  (‹_,_,_ ⊢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 ::
  "bool ⇒ 'addr J1_prog ⇒ 'thread_id ⇒ ('addr expr1 × 'addr locals1) ⇒ ('addr expr1 × 'addr locals1) list ⇒ 'heap
  ⇒ ('addr, 'thread_id, 'heap) J1_thread_action
  ⇒ ('addr expr1 × 'addr locals1) ⇒ ('addr expr1 × 'addr locals1) list ⇒ 'heap ⇒ bool"
  (‹_,_,_ ⊢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⟩"

abbreviation mred1g :: "bool ⇒ 'addr J1_prog ⇒ ('addr,'thread_id,('addr expr1 × 'addr locals1) × ('addr expr1 × 'addr locals1) list,'heap,'addr,('addr, 'thread_id) obs_event) semantics"
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' :: 
  "'addr J1_prog ⇒ ('addr,'thread_id,('addr expr1 × 'addr locals1) × ('addr expr1 × 'addr locals1) list,'heap,'addr,('addr, 'thread_id) obs_event) semantics"
where "mred1' ≡ mred1g False"

abbreviation mred1 :: 
  "'addr J1_prog ⇒ ('addr,'thread_id,('addr expr1 × 'addr locals1) × ('addr expr1 × 'addr locals1) list,'heap,'addr,('addr, 'thread_id) obs_event) semantics"
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" 
  and reds1_max_varss_decr: "uf,P,t ⊢1 ⟨es, s⟩ [-ta→] ⟨es', s'⟩ ⟹ max_varss es' ≤ max_varss es"
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)
apply(fastforce dest: red_ext_new_thread_heap simp add: ta_upd_simps)+
done

lemma red1_new_threadD:
  "⟦ 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"
  and reds1_new_threadD:
  "⟦ 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)"

definition τred1g :: "bool ⇒ 'addr J1_prog ⇒ 'thread_id ⇒ 'heap ⇒ ('addr expr1 × 'addr locals1) ⇒ ('addr expr1 × 'addr locals1) ⇒ bool"
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 :: 
  "bool ⇒ 'addr J1_prog ⇒ 'thread_id ⇒ 'heap ⇒ ('addr expr1 list × 'addr locals1) ⇒ ('addr expr1 list × 'addr locals1) ⇒ bool"
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 :: 
  "bool ⇒ 'addr J1_prog ⇒ 'thread_id ⇒ 'heap ⇒ ('addr expr1 × 'addr locals1) ⇒ ('addr expr1 × 'addr locals1) ⇒ bool"
where "τred1gt uf P t h ≡ (τred1g uf P t h)^++"

abbreviation τreds1gt ::
  "bool ⇒ 'addr J1_prog ⇒ 'thread_id ⇒ 'heap ⇒ ('addr expr1 list × 'addr locals1) ⇒ ('addr expr1 list × 'addr locals1) ⇒ bool"
where "τreds1gt uf P t h ≡ (τreds1g uf P t h)^++"

abbreviation τred1gr ::
  "bool ⇒ 'addr J1_prog ⇒ 'thread_id ⇒ 'heap ⇒ ('addr expr1 × 'addr locals1) ⇒ ('addr expr1 × 'addr locals1) ⇒ bool"
where "τred1gr uf P t h ≡ (τred1g uf P t h)^**"

abbreviation τreds1gr ::
  "bool ⇒ 'addr J1_prog ⇒ 'thread_id ⇒ 'heap ⇒ ('addr expr1 list × 'addr locals1) ⇒ ('addr expr1 list × 'addr locals1) ⇒ bool"
where "τreds1gr uf P t h ≡ (τreds1g uf P t h)^**"

definition τRed1g ::
  "bool ⇒ 'addr J1_prog ⇒ 'thread_id ⇒ 'heap ⇒ ('addr expr1 × 'addr locals1) × (('addr expr1 × 'addr locals1) list)
  ⇒ ('addr expr1 × 'addr locals1) × (('addr expr1 × 'addr locals1) list) ⇒ bool"
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 ::
  "bool ⇒ 'addr J1_prog ⇒ 'thread_id ⇒ 'heap ⇒ ('addr expr1 × 'addr locals1) × (('addr expr1 × 'addr locals1) list) 
  ⇒ ('addr expr1 × 'addr locals1) × (('addr expr1 × 'addr locals1) list) ⇒ bool"
where "τRed1gt uf P t h ≡ (τRed1g uf P t h)^++"

abbreviation τRed1gr :: 
  "bool ⇒ 'addr J1_prog ⇒ 'thread_id ⇒ 'heap ⇒ ('addr expr1 × 'addr locals1) × (('addr expr1 × 'addr locals1) list) 
  ⇒ ('addr expr1 × 'addr locals1) × (('addr expr1 × 'addr locals1) list) ⇒ bool"
where "τRed1gr uf P t h ≡ (τRed1g uf P t h)^**"

abbreviation τred1 :: 
  "'addr J1_prog ⇒ 'thread_id ⇒ 'heap ⇒ ('addr expr1 × 'addr locals1) ⇒ ('addr expr1 × 'addr locals1) ⇒ bool"
where "τred1 ≡ τred1g True"

abbreviation τreds1 :: 
  "'addr J1_prog ⇒ 'thread_id ⇒ 'heap ⇒ ('addr expr1 list × 'addr locals1) ⇒ ('addr expr1 list × 'addr locals1) ⇒ bool"
where "τreds1 ≡ τreds1g True"

abbreviation τred1t :: 
  "'addr J1_prog ⇒ 'thread_id ⇒ 'heap ⇒ ('addr expr1 × 'addr locals1) ⇒ ('addr expr1 × 'addr locals1) ⇒ bool"
where "τred1t ≡ τred1gt True"

abbreviation τreds1t ::
  "'addr J1_prog ⇒ 'thread_id ⇒ 'heap ⇒ ('addr expr1 list × 'addr locals1) ⇒ ('addr expr1 list × 'addr locals1) ⇒ bool"
where "τreds1t ≡ τreds1gt True"

abbreviation τred1r ::
  "'addr J1_prog ⇒ 'thread_id ⇒ 'heap ⇒ ('addr expr1 × 'addr locals1) ⇒ ('addr expr1 × 'addr locals1) ⇒ bool"
where "τred1r ≡ τred1gr True"

abbreviation τreds1r ::
  "'addr J1_prog ⇒ 'thread_id ⇒ 'heap ⇒ ('addr expr1 list × 'addr locals1) ⇒ ('addr expr1 list × 'addr locals1) ⇒ bool"
where "τreds1r ≡ τreds1gr True"

abbreviation τRed1 ::
  "'addr J1_prog ⇒ 'thread_id ⇒ 'heap ⇒ ('addr expr1 × 'addr locals1) × (('addr expr1 × 'addr locals1) list)
  ⇒ ('addr expr1 × 'addr locals1) × (('addr expr1 × 'addr locals1) list) ⇒ bool"
where "τRed1 ≡ τRed1g True"

abbreviation τRed1t ::
  "'addr J1_prog ⇒ 'thread_id ⇒ 'heap ⇒ ('addr expr1 × 'addr locals1) × (('addr expr1 × 'addr locals1) list) 
  ⇒ ('addr expr1 × 'addr locals1) × (('addr expr1 × 'addr locals1) list) ⇒ bool"
where "τRed1t ≡ τRed1gt True"

abbreviation τRed1r :: 
  "'addr J1_prog ⇒ 'thread_id ⇒ 'heap ⇒ ('addr expr1 × 'addr locals1) × (('addr expr1 × 'addr locals1) list) 
  ⇒ ('addr expr1 × 'addr locals1) × (('addr expr1 × 'addr locals1) list) ⇒ bool"
where "τRed1r ≡ τRed1gr True"

abbreviation τred1' :: 
  "'addr J1_prog ⇒ 'thread_id ⇒ 'heap ⇒ ('addr expr1 × 'addr locals1) ⇒ ('addr expr1 × 'addr locals1) ⇒ bool"
where "τred1' ≡ τred1g False"

abbreviation τreds1' :: 
  "'addr J1_prog ⇒ 'thread_id ⇒ 'heap ⇒ ('addr expr1 list × 'addr locals1) ⇒ ('addr expr1 list × 'addr locals1) ⇒ bool"
where "τreds1' ≡ τreds1g False"

abbreviation τred1't ::
  "'addr J1_prog ⇒ 'thread_id ⇒ 'heap ⇒ ('addr expr1 × 'addr locals1) ⇒ ('addr expr1 × 'addr locals1) ⇒ bool"
where "τred1't ≡ τred1gt False"

abbreviation τreds1't :: 
  "'addr J1_prog ⇒ 'thread_id ⇒ 'heap ⇒ ('addr expr1 list × 'addr locals1) ⇒ ('addr expr1 list × 'addr locals1) ⇒ bool"
where "τreds1't ≡ τreds1gt False"

abbreviation τred1'r ::
  "'addr J1_prog ⇒ 'thread_id ⇒ 'heap ⇒ ('addr expr1 × 'addr locals1) ⇒ ('addr expr1 × 'addr locals1) ⇒ bool"
where "τred1'r ≡ τred1gr False"

abbreviation τreds1'r :: 
  "'addr J1_prog ⇒ 'thread_id ⇒ 'heap ⇒ ('addr expr1 list × 'addr locals1) ⇒ ('addr expr1 list × 'addr locals1) ⇒ bool"
where "τreds1'r ≡ τreds1gr False"

abbreviation τRed1' ::
  "'addr J1_prog ⇒ 'thread_id ⇒ 'heap ⇒ ('addr expr1 × 'addr locals1) × (('addr expr1 × 'addr locals1) list) 
  ⇒ ('addr expr1 × 'addr locals1) × (('addr expr1 × 'addr locals1) list) ⇒ bool"
where "τRed1' ≡ τRed1g False"

abbreviation τRed1't ::
  "'addr J1_prog ⇒ 'thread_id ⇒ 'heap ⇒ ('addr expr1 × 'addr locals1) × (('addr expr1 × 'addr locals1) list) 
  ⇒ ('addr expr1 × 'addr locals1) × (('addr expr1 × 'addr locals1) list) ⇒ bool"
where "τRed1't ≡ τRed1gt False"

abbreviation τRed1'r :: 
  "'addr J1_prog ⇒ 'thread_id ⇒ 'heap ⇒ ('addr expr1 × 'addr locals1) × (('addr expr1 × 'addr locals1) list) 
  ⇒ ('addr expr1 × 'addr locals1) × (('addr expr1 × 'addr locals1) list) ⇒ bool"
where "τRed1'r ≡ τRed1gr False"

abbreviation τMOVE1 :: 
  "'m prog ⇒ ((('addr expr1 × 'addr locals1) × ('addr expr1 × 'addr locals1) list) × 'heap, ('addr, 'thread_id, 'heap) J1_thread_action) trsys"
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)"
by(simp add: τred1g_def)

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)"
by(simp add: τreds1g_def)

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 τreds1t_cons_τreds1t: "τreds1gt uf P t h (es, xs) (es', xs') ⟹ τreds1gt uf P t h (Val v # es, xs) (Val v # es', xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl List1Red2 τmoves1Tl)

lemma τred1r_inj_τreds1r: "τred1gr uf P t h (e, xs) (e', xs') ⟹ τreds1gr uf P t h (e # es, xs) (e' # es, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl List1Red1 τmoves1Hd)

lemma τreds1r_cons_τreds1r: "τreds1gr uf P t h (es, xs) (es', xs') ⟹ τreds1gr uf P t h (Val v # es, xs) (Val v # es', xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl List1Red2 τmoves1Tl)

lemma NewArray_τred1t_xt:
  "τred1gt uf P t h (e, xs) (e', xs') ⟹ τred1gt uf P t h (newA T⌊e⌉, xs) (newA T⌊e'⌉, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl New1ArrayRed τmove1NewArray)

lemma Cast_τred1t_xt:
  "τred1gt uf P t h (e, xs) (e', xs') ⟹ τred1gt uf P t h (Cast T e, xs) (Cast T e', xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl Cast1Red τmove1Cast)

lemma InstanceOf_τred1t_xt:
  "τred1gt uf P t h (e, xs) (e', xs') ⟹ τred1gt uf P t h (e instanceof T, xs) (e' instanceof T, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl InstanceOf1Red τmove1InstanceOf)

lemma BinOp_τred1t_xt1:
  "τred1gt uf P t h (e1, xs) (e1', xs') ⟹ τred1gt uf P t h (e1 «bop» e2, xs) (e1' «bop» e2, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl Bin1OpRed1 τmove1BinOp1)

lemma BinOp_τred1t_xt2:
  "τred1gt uf P t h (e2, xs) (e2', xs') ⟹ τred1gt uf P t h (Val v «bop» e2, xs) (Val v «bop» e2', xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl Bin1OpRed2 τmove1BinOp2)

lemma LAss_τred1t:
  "τred1gt uf P t h (e, xs) (e', xs') ⟹ τred1gt uf P t h (V := e, xs) (V := e', xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl LAss1Red τmove1LAss)

lemma AAcc_τred1t_xt1:
  "τred1gt uf P t h (a, xs) (a', xs') ⟹ τred1gt uf P t h (a⌊i⌉, xs) (a'⌊i⌉, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl AAcc1Red1 τmove1AAcc1)

lemma AAcc_τred1t_xt2:
  "τred1gt uf P t h (i, xs) (i', xs') ⟹ τred1gt uf P t h (Val a⌊i⌉, xs) (Val a⌊i'⌉, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl AAcc1Red2 τmove1AAcc2)

lemma AAss_τred1t_xt1:
  "τred1gt uf P t h (a, xs) (a', xs') ⟹ τred1gt uf P t h (a⌊i⌉ := e, xs) (a'⌊i⌉ := e, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl AAss1Red1 τmove1AAss1)

lemma AAss_τred1t_xt2:
  "τred1gt uf P t h (i, xs) (i', xs') ⟹ τred1gt uf P t h (Val a⌊i⌉ := e, xs) (Val a⌊i'⌉ := e, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl AAss1Red2 τmove1AAss2)

lemma AAss_τred1t_xt3:
  "τred1gt uf P t h (e, xs) (e', xs') ⟹ τred1gt uf P t h (Val a⌊Val i⌉ := e, xs) (Val a⌊Val i⌉ := e', xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl AAss1Red3 τmove1AAss3)

lemma ALength_τred1t_xt:
  "τred1gt uf P t h (a, xs) (a', xs') ⟹ τred1gt uf P t h (a∙length, xs) (a'∙length, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl ALength1Red τmove1ALength)

lemma FAcc_τred1t_xt:
  "τred1gt uf P t h (e, xs) (e', xs') ⟹ τred1gt uf P t h (e∙F{D}, xs) (e'∙F{D}, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl FAcc1Red τmove1FAcc)

lemma FAss_τred1t_xt1:
  "τred1gt uf P t h (e, xs) (e', xs') ⟹ τred1gt uf P t h (e∙F{D} := e2, xs) (e'∙F{D} := e2, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl FAss1Red1 τmove1FAss1)

lemma FAss_τred1t_xt2:
  "τred1gt uf P t h (e, xs) (e', xs') ⟹ τred1gt uf P t h (Val v∙F{D} := e, xs) (Val v∙F{D} := e', xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl FAss1Red2 τmove1FAss2)

lemma CAS_τred1t_xt1:
  "τred1gt uf P t h (e, xs) (e', xs') ⟹ τred1gt uf P t h (e∙compareAndSwap(D∙F, e2, e3), xs) (e'∙compareAndSwap(D∙F, e2, e3), xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl CAS1Red1)

lemma CAS_τred1t_xt2:
  "τred1gt uf P t h (e, xs) (e', xs') ⟹ τred1gt uf P t h (Val v∙compareAndSwap(D∙F, e, e3), xs) (Val v∙compareAndSwap(D∙F, e', e3), xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl CAS1Red2)

lemma CAS_τred1t_xt3:
  "τred1gt uf P t h (e, xs) (e', xs') ⟹ τred1gt uf P t h (Val v∙compareAndSwap(D∙F, Val v', e), xs) (Val v∙compareAndSwap(D∙F, Val v', e'), xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl CAS1Red3)

lemma Call_τred1t_obj:
  "τred1gt uf P t h (e, xs) (e', xs') ⟹ τred1gt uf P t h (e∙M(ps), xs) (e'∙M(ps), xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl Call1Obj τmove1CallObj)

lemma Call_τred1t_param:
  "τreds1gt uf P t h (es, xs) (es', xs') ⟹ τred1gt uf P t h (Val v∙M(es), xs) (Val v∙M(es'), xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl Call1Params τmove1CallParams)

lemma Block_None_τred1t_xt:
  "τred1gt uf P t h (e, xs) (e', xs') ⟹ τred1gt uf P t h ({V:T=None; e}, xs) ({V:T=None; e'}, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl τmove1Block elim!: Block1Red)

lemma Block_τred1t_Some:
  "⟦ τred1gt uf P t h (e, xs[V := v]) (e', xs'); V < length xs ⟧ 
  ⟹ τred1gt uf P t h ({V:Ty=⌊v⌋; e}, xs) ({V:Ty=None; e'}, xs')"
by(blast intro: tranclp_into_tranclp2 Block1Some τmove1BlockSome Block_None_τred1t_xt)

lemma Sync_τred1t_xt:
  "τred1gt uf P t h (e, xs) (e', xs') ⟹ τred1gt uf P t h (sync⇘V⇙ (e) e2, xs) (sync⇘V⇙ (e') e2, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl Synchronized1Red1 τmove1Sync)

lemma InSync_τred1t_xt:
  "τred1gt uf P t h (e, xs) (e', xs') ⟹ τred1gt uf P t h (insync⇘V⇙ (a) e, xs) (insync⇘V⇙ (a) e', xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl Synchronized1Red2 τmove1InSync)

lemma Seq_τred1t_xt:
  "τred1gt uf P t h (e, xs) (e', xs') ⟹ τred1gt uf P t h (e;;e2, xs) (e';;e2, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl Seq1Red τmove1Seq)

lemma Cond_τred1t_xt:
  "τred1gt uf P t h (e, xs) (e', xs') ⟹ τred1gt uf P t h (if (e) e1 else e2, xs) (if (e') e1 else e2, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl Cond1Red τmove1Cond)

lemma Throw_τred1t_xt:
  "τred1gt uf P t h (e, xs) (e', xs') ⟹ τred1gt uf P t h (throw e, xs) (throw e', xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl Throw1Red τmove1Throw)

lemma Try_τred1t_xt:
  "τred1gt uf P t h (e, xs) (e', xs') ⟹ τred1gt uf P t h (try e catch(C V) e2, xs) (try e' catch(C V) e2, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl Try1Red τmove1Try)


lemma NewArray_τred1r_xt:
  "τred1gr uf P t h (e, xs) (e', xs') ⟹ τred1gr uf P t h (newA T⌊e⌉, xs) (newA T⌊e'⌉, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl New1ArrayRed τmove1NewArray)

lemma Cast_τred1r_xt:
  "τred1gr uf P t h (e, xs) (e', xs') ⟹ τred1gr uf P t h (Cast T e, xs) (Cast T e', xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl Cast1Red τmove1Cast)

lemma InstanceOf_τred1r_xt:
  "τred1gr uf P t h (e, xs) (e', xs') ⟹ τred1gr uf P t h (e instanceof T, xs) (e' instanceof T, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl InstanceOf1Red τmove1InstanceOf)

lemma BinOp_τred1r_xt1:
  "τred1gr uf P t h (e1, xs) (e1', xs') ⟹ τred1gr uf P t h (e1 «bop» e2, xs) (e1' «bop» e2, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl Bin1OpRed1 τmove1BinOp1)

lemma BinOp_τred1r_xt2:
  "τred1gr uf P t h (e2, xs) (e2', xs') ⟹ τred1gr uf P t h (Val v «bop» e2, xs) (Val v «bop» e2', xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl Bin1OpRed2 τmove1BinOp2)

lemma LAss_τred1r:
  "τred1gr uf P t h (e, xs) (e', xs') ⟹ τred1gr uf P t h (V := e, xs) (V := e', xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl LAss1Red τmove1LAss)

lemma AAcc_τred1r_xt1:
  "τred1gr uf P t h (a, xs) (a', xs') ⟹ τred1gr uf P t h (a⌊i⌉, xs) (a'⌊i⌉, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl AAcc1Red1 τmove1AAcc1)

lemma AAcc_τred1r_xt2:
  "τred1gr uf P t h (i, xs) (i', xs') ⟹ τred1gr uf P t h (Val a⌊i⌉, xs) (Val a⌊i'⌉, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl AAcc1Red2 τmove1AAcc2)

lemma AAss_τred1r_xt1:
  "τred1gr uf P t h (a, xs) (a', xs') ⟹ τred1gr uf P t h (a⌊i⌉ := e, xs) (a'⌊i⌉ := e, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl AAss1Red1 τmove1AAss1)

lemma AAss_τred1r_xt2:
  "τred1gr uf P t h (i, xs) (i', xs') ⟹ τred1gr uf P t h (Val a⌊i⌉ := e, xs) (Val a⌊i'⌉ := e, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl AAss1Red2 τmove1AAss2)

lemma AAss_τred1r_xt3:
  "τred1gr uf P t h (e, xs) (e', xs') ⟹ τred1gr uf P t h (Val a⌊Val i⌉ := e, xs) (Val a⌊Val i⌉ := e', xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl AAss1Red3 τmove1AAss3)

lemma ALength_τred1r_xt:
  "τred1gr uf P t h (a, xs) (a', xs') ⟹ τred1gr uf P t h (a∙length, xs) (a'∙length, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl ALength1Red τmove1ALength)

lemma FAcc_τred1r_xt:
  "τred1gr uf P t h (e, xs) (e', xs') ⟹ τred1gr uf P t h (e∙F{D}, xs) (e'∙F{D}, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl FAcc1Red τmove1FAcc)

lemma FAss_τred1r_xt1:
  "τred1gr uf P t h (e, xs) (e', xs') ⟹ τred1gr uf P t h (e∙F{D} := e2, xs) (e'∙F{D} := e2, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl FAss1Red1 τmove1FAss1)

lemma FAss_τred1r_xt2:
  "τred1gr uf P t h (e, xs) (e', xs') ⟹ τred1gr uf P t h (Val v∙F{D} := e, xs) (Val v∙F{D} := e', xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl FAss1Red2 τmove1FAss2)

lemma CAS_τred1r_xt1:
  "τred1gr uf P t h (e, xs) (e', xs') ⟹ τred1gr uf P t h (e∙compareAndSwap(D∙F, e2, e3), xs) (e'∙compareAndSwap(D∙F, e2, e3), xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl CAS1Red1)

lemma CAS_τred1r_xt2:
  "τred1gr uf P t h (e, xs) (e', xs') ⟹ τred1gr uf P t h (Val v∙compareAndSwap(D∙F, e, e3), xs) (Val v∙compareAndSwap(D∙F, e', e3), xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl CAS1Red2)

lemma CAS_τred1r_xt3:
  "τred1gr uf P t h (e, xs) (e', xs') ⟹ τred1gr uf P t h (Val v∙compareAndSwap(D∙F, Val v', e), xs) (Val v∙compareAndSwap(D∙F, Val v', e'), xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl CAS1Red3)

lemma Call_τred1r_obj:
  "τred1gr uf P t h (e, xs) (e', xs') ⟹ τred1gr uf P t h (e∙M(ps), xs) (e'∙M(ps), xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl Call1Obj τmove1CallObj)

lemma Call_τred1r_param:
  "τreds1gr uf P t h (es, xs) (es', xs') ⟹ τred1gr uf P t h (Val v∙M(es), xs) (Val v∙M(es'), xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl Call1Params τmove1CallParams)

lemma Block_None_τred1r_xt:
  "τred1gr uf P t h (e, xs) (e', xs') ⟹ τred1gr uf P t h ({V:T=None; e}, xs) ({V:T=None; e'}, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl τmove1Block elim!: Block1Red)

lemma Block_τred1r_Some:
  "⟦ τred1gr uf P t h (e, xs[V := v]) (e', xs'); V < length xs ⟧ 
  ⟹ τred1gr uf P t h ({V:Ty=⌊v⌋; e}, xs) ({V:Ty=None; e'}, xs')"
by(blast intro: converse_rtranclp_into_rtranclp Block1Some τmove1BlockSome Block_None_τred1r_xt)

lemma Sync_τred1r_xt:
  "τred1gr uf P t h (e, xs) (e', xs') ⟹ τred1gr uf P t h (sync⇘V⇙ (e) e2, xs) (sync⇘V⇙ (e') e2, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl Synchronized1Red1 τmove1Sync)

lemma InSync_τred1r_xt:
  "τred1gr uf P t h (e, xs) (e', xs') ⟹ τred1gr uf P t h (insync⇘V⇙ (a) e, xs) (insync⇘V⇙ (a) e', xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl Synchronized1Red2 τmove1InSync)

lemma Seq_τred1r_xt:
  "τred1gr uf P t h (e, xs) (e', xs') ⟹ τred1gr uf P t h (e;;e2, xs) (e';;e2, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl Seq1Red τmove1Seq)

lemma Cond_τred1r_xt:
  "τred1gr uf P t h (e, xs) (e', xs') ⟹ τred1gr uf P t h (if (e) e1 else e2, xs) (if (e') e1 else e2, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl Cond1Red τmove1Cond)

lemma Throw_τred1r_xt:
  "τred1gr uf P t h (e, xs) (e', xs') ⟹ τred1gr uf P t h (throw e, xs) (throw e', xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl Throw1Red τmove1Throw)

lemma Try_τred1r_xt:
  "τred1gr uf P t h (e, xs) (e', xs') ⟹ τred1gr uf P t h (try e catch(C V) e2, xs) (try e' catch(C V) e2, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl Try1Red τmove1Try)

lemma τred1t_ThrowD [dest]: "τred1gt uf P t h (Throw a, xs) (e'', xs'') ⟹ e'' = Throw a ∧ xs'' = xs"
by(induct rule: tranclp_induct2)(auto)

lemma τred1r_ThrowD [dest]: "τred1gr uf P t h (Throw a, xs) (e'', xs'') ⟹ e'' = Throw a ∧ xs'' = xs"
by(induct rule: rtranclp_induct2)(auto)

lemma τRed1_conv [iff]:
  "τRed1g uf P t h (ex, exs) (ex', exs') = (uf,P,t ⊢1 ⟨ex/exs, h⟩ -ε→ ⟨ex'/exs', h⟩ ∧ τMove1 P h (ex, exs))"
by(simp add: τRed1g_def)


lemma τred1t_into_τRed1t:
  "τred1gt uf P t h (e, xs) (e'', xs'') ⟹ τRed1gt uf P t h ((e, xs), exs) ((e'', xs''), exs)"
by(induct rule: tranclp_induct2)(fastforce dest: red1Red intro: τmove1Block tranclp.intros)+

lemma τred1r_into_τRed1r:
  "τred1gr uf P t h (e, xs) (e'', xs'') ⟹ τRed1gr uf P t h ((e, xs), exs) ((e'', xs''), exs)"
by(induct rule: rtranclp_induct2)(fastforce dest: red1Red intro: τmove1Block rtranclp.intros)+

lemma red1_max_vars: "uf,P,t ⊢1 ⟨e, s⟩ -ta→ ⟨e', s'⟩ ⟹ max_vars e' ≤ max_vars e"
  and reds1_max_varss: "uf,P,t ⊢1 ⟨es, s⟩ [-ta→] ⟨es', s'⟩ ⟹ max_varss es' ≤ max_varss es"
by(induct rule: red1_reds1.inducts) auto

lemma τred1t_max_vars: "τred1gt uf P t h (e, xs) (e', xs') ⟹ max_vars e' ≤ max_vars e"
by(induct rule: tranclp_induct2)(auto dest: red1_max_vars)

lemma τred1r_max_vars: "τred1gr uf P t h (e, xs) (e', xs') ⟹ max_vars e' ≤ max_vars e"
by(induct rule: rtranclp_induct2)(auto dest: red1_max_vars)

lemma τred1r_Val:
  "τred1gr uf P t h (Val v, xs) s' ⟷ s' = (Val v, xs)"
proof
  assume "τred1gr uf P t h (Val v, xs) s'"
  thus "s' = (Val v, xs)" by induct(auto)
qed auto

lemma τred1t_Val:
  "τred1gt uf P t h (Val v, xs) s' ⟷ False"
proof
  assume "τred1gt uf P t h (Val v, xs) s'"
  thus False by induct auto
qed auto

lemma τreds1r_map_Val:
  "τreds1gr uf P t h (map Val vs, xs) s' ⟷ s' = (map Val vs, xs)"
proof
  assume "τreds1gr uf P t h (map Val vs, xs) s'"
  thus "s' = (map Val vs, xs)" by induct auto
qed auto

lemma τreds1t_map_Val:
  "τreds1gt uf P t h (map Val vs, xs) s' ⟷ False"
proof
  assume "τreds1gt uf P t h (map Val vs, xs) s'"
  thus "False" by induct auto
qed auto

lemma τreds1r_map_Val_Throw:
  "τreds1gr uf P t h (map Val vs @ Throw a # es, xs) s' ⟷ s' = (map Val vs @ Throw a # es, xs)"
  (is "?lhs ⟷ ?rhs")
proof
  assume ?lhs thus ?rhs by induct auto
qed auto

lemma τreds1t_map_Val_Throw:
  "τreds1gt uf P t h (map Val vs @ Throw a # es, xs) s' ⟷ False"
  (is "?lhs ⟷ ?rhs")
proof
  assume ?lhs thus ?rhs by induct auto
qed auto

lemma τred1r_Throw:
  "τred1gr uf P t h (Throw a, xs) s' ⟷ s' = (Throw a, xs)" (is "?lhs ⟷ ?rhs")
proof
  assume ?lhs thus ?rhs by induct auto
qed simp

lemma τred1t_Throw:
  "τred1gt uf P t h (Throw a, xs) s' ⟷ False" (is "?lhs ⟷ ?rhs")
proof
  assume ?lhs thus ?rhs by induct auto
qed simp

lemma red1_False_into_red1_True:
  "False,P,t ⊢1 ⟨e, s⟩ -ta→ ⟨e', s'⟩ ⟹ True,P,t ⊢1 ⟨e, s⟩ -ta→ ⟨e', s'⟩"
  and reds1_False_into_reds1_True:
  "False,P,t ⊢1 ⟨es, s⟩ [-ta→] ⟨es', s'⟩ ⟹ True,P,t ⊢1 ⟨es, s⟩ [-ta→] ⟨es', s'⟩"
  by (induct rule: red1_reds1.inducts) (auto intro: red1_reds1.intros)

lemma Red1_False_into_Red1_True:
  assumes "False,P,t ⊢1 ⟨ex/exs,shr s⟩ -ta→ ⟨ex'/exs',m'⟩"
  shows "True,P,t ⊢1 ⟨ex/exs,shr s⟩ -ta→ ⟨ex'/exs',m'⟩"
using assms
by(cases)(auto dest: Red1.intros red1_False_into_red1_True)

lemma red1_Suspend_is_call:
  "⟦ uf,P,t ⊢1 ⟨e, s⟩ -ta→ ⟨e', s'⟩; Suspend w ∈ set ⦃ta⦄⇘w⇙ ⟧ ⟹ call1 e' ≠ None"
  and reds_Suspend_is_calls:
  "⟦ uf,P,t ⊢1 ⟨es, s⟩ [-ta→] ⟨es', s'⟩; Suspend w ∈ set ⦃ta⦄⇘w⇙ ⟧ ⟹ calls1 es' ≠ None"
by(induct rule: red1_reds1.inducts)(auto dest: red_external_Suspend_StaySame)

lemma Red1_Suspend_is_call:
  "⟦ uf,P,t ⊢1 ⟨(e, xs)/exs, h⟩ -ta→ ⟨(e', xs')/exs', h'⟩; Suspend w ∈ set ⦃ta⦄⇘w⇙ ⟧ ⟹ call1 e' ≠ None"
by(auto elim!: Red1.cases dest: red1_Suspend_is_call)

lemma Red1_mthr: "multithreaded final_expr1 (mred1g uf P)"
by(unfold_locales)(fastforce elim!: Red1.cases dest: red1_new_thread_heap)+

lemma red1_τmove1_heap_unchanged: "⟦ uf,P,t ⊢1 ⟨e, s⟩ -ta→ ⟨e', s'⟩; τmove1 P (hp s) e ⟧ ⟹ hp s' = hp s"
  and red1_τ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(fastforce simp add: map_eq_append_conv τexternal'_def τexternal_def dest: τexternal'_red_external_heap_unchanged)+
done

lemma Red1_τmthr_wf: "τmultithreaded_wf final_expr1 (mred1g uf P) (τMOVE1 P)"
proof -
  interpret multithreaded final_expr1 "mred1g uf P" convert_RA
    by(rule Red1_mthr)
  show ?thesis
  proof
    fix x1 m1 t ta1 x1' m1'
    assume "mred1g uf P t (x1, m1) ta1 (x1', m1')" "τMOVE1 P (x1, m1) ta1 (x1', m1')"
    thus "m1 = m1'" by(cases x1)(fastforce elim!: Red1.cases dest: red1_τmove1_heap_unchanged)
  next
    fix s ta s'
    assume "τMOVE1 P s ta s'"
    thus "ta = ε" by(simp add: split_beta)
  qed
qed

end

sublocale J1_heap_base < Red1_mthr: 
  τmultithreaded_wf 
    final_expr1
    "mred1g uf P"
    convert_RA
    "τMOVE1 P"
  for uf P
by(rule Red1_τmthr_wf)

context J1_heap_base begin

lemma τRed1't_into_Red1'_τmthr_silent_movet:
  "τRed1gt uf P t h (ex2, exs2) (ex2'', exs2'')
  ⟹ Red1_mthr.silent_movet uf P t ((ex2, exs2), h) ((ex2'', exs2''), h)"
apply(induct rule: tranclp_induct2)
 apply clarsimp
 apply(rule tranclp.r_into_trancl)
 apply(simp add: Red1_mthr.silent_move_iff)
apply(erule tranclp.trancl_into_trancl)
apply(simp add: Red1_mthr.silent_move_iff)
done

lemma τRed1t_into_Red1'_τmthr_silent_moves:
  "τRed1gt uf P t h (ex2, exs2) (ex2'', exs2'')
  ⟹ Red1_mthr.silent_moves uf P t ((ex2, exs2), h) ((ex2'', exs2''), h)"
by(rule tranclp_into_rtranclp)(rule τRed1't_into_Red1'_τmthr_silent_movet)

lemma τRed1'r_into_Red1'_τmthr_silent_moves:
  "τRed1gr uf P t h (ex, exs) (ex', exs') ⟹ Red1_mthr.silent_moves uf P t ((ex, exs), h) ((ex', exs'), h)"
apply(induct rule: rtranclp_induct2)
 apply blast
apply(erule rtranclp.rtrancl_into_rtrancl)
apply(simp add: Red1_mthr.silent_move_iff)
done

lemma τRed1r_rtranclpD:
  "τRed1gr uf P t h s s' ⟹ τtrsys.silent_moves (mred1g uf P t) (τMOVE1 P) (s, h) (s', h)"
apply(induct rule: rtranclp_induct)
apply(auto elim!: rtranclp.rtrancl_into_rtrancl intro: τtrsys.silent_move.intros)
done

lemma τRed1t_tranclpD:
  "τRed1gt uf P t h s s' ⟹ τtrsys.silent_movet (mred1g uf P t) (τMOVE1 P) (s, h) (s', h)"
apply(induct rule: tranclp_induct)
apply(rule tranclp.r_into_trancl)
apply(auto elim!: tranclp.trancl_into_trancl intro!: τtrsys.silent_move.intros simp: τRed1g_def split_def)
done

lemma τmreds1_Val_Nil: "τtrsys.silent_moves (mred1g uf P t) (τMOVE1 P) (((Val v, xs), []), h) s ⟷ s = (((Val v, xs), []), h)"
proof
  assume "τtrsys.silent_moves (mred1g uf P t) (τMOVE1 P) (((Val v, xs), []), h) s"
  thus "s = (((Val v, xs), []), h)"
    by induct(auto elim!: Red1_mthr.silent_move.cases Red1.cases)
qed auto

lemma τmreds1_Throw_Nil:
  "τtrsys.silent_moves (mred1g uf P t) (τMOVE1 P) (((Throw a, xs), []), h) s ⟷ s = (((Throw a, xs), []), h)"
proof
  assume "τtrsys.silent_moves (mred1g uf P t) (τMOVE1 P) (((Throw a, xs), []), h) s"
  thus "s = (((Throw a, xs), []), h)"
    by induct(auto elim!: Red1_mthr.silent_move.cases Red1.cases)
qed auto

end

end