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
  ('addr, 'thread_id, 'heap) J_thread_action =
  "('addr, 'thread_id, 'addr expr × 'addr locals,'heap) Jinja_thread_action"

type_synonym
  ('addr, 'thread_id, 'heap) J_state = 
  "('addr,'thread_id,'addr expr × 'addr locals,'heap,'addr) state"

(* 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;
    in [(@{type_syntax "Jinja_thread_action"}, K tr')]
  end
›
typ "('addr,'thread_id,'heap) J_thread_action"

(* 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
›
typ "('addr, 'thread_id, 'heap) J_state"

definition extNTA2J :: "'addr J_prog ⇒ (cname × mname × 'addr) ⇒ 'addr expr × 'addr locals"
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
  ⇒ 'addr expr × 'addr locals"
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) 
  J_start_state :: "'addr J_prog ⇒ cname ⇒ mname ⇒ 'addr val list ⇒ ('addr, 'thread_id, 'heap) J_state"
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)"
by(simp add: extNTA2J_def split_beta)

abbreviation extTA2J :: 
  "'addr J_prog ⇒ ('addr, 'thread_id, 'heap) external_thread_action ⇒ ('addr, 'thread_id, 'heap) J_thread_action"
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 :: 
  "(('addr, 'thread_id, 'heap) external_thread_action ⇒ ('addr, 'thread_id, 'x,'heap) Jinja_thread_action)
   ⇒ 'addr J_prog ⇒ 'thread_id
   ⇒ 'addr expr ⇒ ('addr, 'heap) Jstate
   ⇒ ('addr, 'thread_id, 'x,'heap) Jinja_thread_action
   ⇒ 'addr expr ⇒ ('addr, 'heap) Jstate ⇒ bool"
  ("_,_,_ ⊢ ((1⟨_,/_⟩) -_→/ (1⟨_,/_⟩))" [51,51,0,0,0,0,0,0] 81)
 and reds ::
  "(('addr, 'thread_id, 'heap) external_thread_action ⇒ ('addr, 'thread_id, 'x,'heap) Jinja_thread_action)
   ⇒ 'addr J_prog ⇒ 'thread_id 
   ⇒ 'addr expr list ⇒ ('addr, 'heap) Jstate 
   ⇒ ('addr, 'thread_id, 'x,'heap) Jinja_thread_action
   ⇒ 'addr expr list ⇒ ('addr, 'heap) Jstate ⇒ bool"
               ("_,_,_ ⊢ ((1⟨_,/_⟩) [-_→]/ (1⟨_,/_⟩))" [51,51,0,0,0,0,0,0] 81)
for extTA :: "('addr, 'thread_id, 'heap) external_thread_action ⇒ ('addr, 'thread_id, 'x, 'heap) Jinja_thread_action"
and P :: "'addr J_prog" and t :: 'thread_id
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' ::
  "'addr J_prog ⇒ 'thread_id ⇒ 'addr expr ⇒ ('heap × 'addr locals) 
  ⇒ ('addr, 'thread_id, 'heap) J_thread_action ⇒ 'addr expr ⇒ ('heap × 'addr locals) ⇒ bool"
  ("_,_ ⊢ ((1⟨_,/_⟩) -_→/ (1⟨_,/_⟩))" [51,0,0,0,0,0,0] 81)
where "red' P ≡ red (extTA2J P) P"

abbreviation reds' :: 
  "'addr J_prog ⇒ 'thread_id ⇒ 'addr expr list ⇒ ('heap × 'addr locals)
  ⇒ ('addr, 'thread_id, 'heap) J_thread_action ⇒ 'addr expr list ⇒ ('heap × 'addr locals) ⇒ bool"
  ("_,_ ⊢ ((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

lemma red_lcl_add_aux:
  "extTA,P,t ⊢ ⟨e, s⟩ -ta→ ⟨e', s'⟩ ⟹ extTA,P,t ⊢ ⟨e, (hp s, l0 ++ lcl s)⟩ -ta→ ⟨e', (hp s', l0 ++ lcl s')⟩"
  and reds_lcl_add_aux:
  "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)" 
    by(simp add:fun_eq_iff map_add_def)
  have lrew1: "⋀X X' X'' vo. (X(V := vo) ++ X')(V := (X ++ X'') V) = X ++ X'(V := X'' V)"
    by(simp add: fun_eq_iff map_add_def)
  have lrew2: "⋀X X'. (X(V := None) ++ X') V = X' V"
    by(simp add: map_add_def) 
  show ?case
  proof(cases vo)
    case None
    from IH[of "l0(V := vo)"]
    show ?thesis
      apply(simp del: fun_upd_apply add: lrew)
      apply(drule red_reds.BlockRed)
      by(simp only: lrew1 None lrew2)
  next
    case (Some v)
    with ‹extTA,P,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')⟩"
by(auto dest:red_lcl_add_aux reds_lcl_add_aux)

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]
    show ?thesis by(simp add: o_def)
  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]
    show ?thesis by(simp add: o_def)
  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]
    show ?thesis by(simp add: o_def)
  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(auto simp add: is_Throws_conv)
      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