Theory J0

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

section ‹The JinjaThreads source language with explicit call stacks›

theory J0 imports
  "../J/WWellForm"
  "../J/WellType"
  "../J/Threaded" 
  "../Framework/FWBisimulation" 
  CallExpr
begin

declare widen_refT [elim]

abbreviation final_expr0 :: "'addr expr × 'addr expr list ⇒ bool" where
  "final_expr0 ≡ λ(e, es). final e ∧ es = []"

type_synonym
  ('addr, 'thread_id, 'heap) J0_thread_action = 
  "('addr, 'thread_id, 'addr expr × 'addr expr list,'heap) Jinja_thread_action"

type_synonym
  ('addr, 'thread_id, 'heap) J0_state = "('addr,'thread_id,'addr expr × 'addr expr list,'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 "list"}, _) $
              (Const (@{type_syntax "exp"}, _) $
                 Const (@{type_syntax "String.literal"}, _) $
                 Const (@{type_syntax "unit"}, _) $ a3))
       , h] =
      if a1 = a2 andalso a2 = a3 then Syntax.const @{type_syntax "J0_thread_action"} $ a1 $ t $ h
      else raise Match;
    in [(@{type_syntax "Jinja_thread_action"}, K tr')]
  end
›
typ "('addr,'thread_id,'heap) J0_thread_action"

(* pretty printing for J0_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 "list"}, _) $
              (Const (@{type_syntax "exp"}, _) $
                 Const (@{type_syntax "String.literal"}, _) $
                 Const (@{type_syntax "unit"}, _) $ a3))
       , h, a4] =
      if a1 = a2 andalso a2 = a3 then Syntax.const @{type_syntax "J0_state"} $ a1 $ t $ h
      else raise Match;
    in [(@{type_syntax "state"}, K tr')]
  end
›
typ "('addr, 'thread_id, 'heap) J0_state"

definition extNTA2J0 :: "'addr J_prog ⇒ (cname × mname × 'addr) ⇒ ('addr expr × 'addr expr list)"
where
  "extNTA2J0 P = (λ(C, M, a). let (D, _, _, meth) = method P C M; (_, body) = the meth
                               in ({this:Class D=⌊Addr a⌋; body}, []))"

lemma extNTA2J0_iff [simp]:
  "extNTA2J0 P (C, M, a) = 
   ({this:Class (fst (method P C M))=⌊Addr a⌋; snd (the (snd (snd (snd (method P C M)))))}, [])"
by(simp add: extNTA2J0_def split_def)

abbreviation extTA2J0 :: 
  "'addr J_prog ⇒ ('addr, 'thread_id, 'heap) external_thread_action ⇒ ('addr, 'thread_id, 'heap) J0_thread_action"
where "extTA2J0 P ≡ convert_extTA (extNTA2J0 P)"

lemma obs_a_extTA2J_eq_obs_a_extTA2J0 [simp]: "⦃extTA2J P ta⦄⇘o⇙ = ⦃extTA2J0 P ta⦄⇘o⇙"
by(cases ta)(simp add: ta_upd_simps)

lemma extTA2J0_ε: "extTA2J0 P ε = ε"
by(simp)

context J_heap_base begin

definition no_call :: "'m prog ⇒ 'heap ⇒ ('a, 'b, 'addr) exp ⇒ bool"
where "no_call P h e = (∀aMvs. call e = ⌊aMvs⌋ ⟶ synthesized_call P h aMvs)"

definition no_calls :: "'m prog ⇒ 'heap ⇒ ('a, 'b, 'addr) exp list ⇒ bool"
where "no_calls P h es = (∀aMvs. calls es = ⌊aMvs⌋ ⟶ synthesized_call P h aMvs)"

inductive red0 :: 
  "'addr J_prog ⇒ 'thread_id ⇒ 'addr expr ⇒ 'addr expr list ⇒ 'heap
  ⇒ ('addr, 'thread_id, 'heap) J0_thread_action ⇒ 'addr expr ⇒ 'addr expr list ⇒ 'heap ⇒ bool"
  ("_,_ ⊢0 ((1⟨_'/_,/_⟩) -_→/ (1⟨_'/_,/_⟩))" [51,0,0,0,0,0,0,0,0] 81)
for P :: "'addr J_prog" and t :: 'thread_id
where

  red0Red:
  "⟦ extTA2J0 P,P,t ⊢ ⟨e, (h, Map.empty)⟩ -ta→ ⟨e', (h', xs')⟩;
     ∀aMvs. call e = ⌊aMvs⌋ ⟶ synthesized_call P h aMvs ⟧
  ⟹ P,t ⊢0 ⟨e/es, h⟩ -ta→ ⟨e'/es, h'⟩"

| red0Call:
  "⟦ call e = ⌊(a, M, vs)⌋; typeof_addr h a = ⌊U⌋; 
     P ⊢ class_type_of U sees M:Ts→T = ⌊(pns, body)⌋ in D; 
     size vs = size pns; size Ts = size pns ⟧
  ⟹ P,t ⊢0 ⟨e/es, h⟩ -ε→ ⟨blocks (this # pns) (Class D # Ts) (Addr a # vs) body/e#es, h⟩"

| red0Return:
  "final e' ⟹ P,t ⊢0 ⟨e'/e#es, h⟩ -ε→ ⟨inline_call e' e/es, h⟩"

abbreviation J0_start_state :: "'addr J_prog ⇒ cname ⇒ mname ⇒ 'addr val list ⇒ ('addr, 'thread_id, 'heap) J0_state"
where
  "J0_start_state ≡ 
   start_state (λC M Ts T (pns, body) vs. (blocks (this # pns) (Class C # Ts) (Null # vs) body, []))"

abbreviation mred0 ::
  "'addr J_prog ⇒ ('addr,'thread_id,'addr expr × 'addr expr list,'heap,'addr,('addr, 'thread_id) obs_event) semantics"
where "mred0 P ≡ (λt ((e, es), h) ta ((e', es'), h'). red0 P t e es h ta e' es' h')"

end

declare domIff[iff, simp del]

context J_heap_base begin

lemma assumes wf: "wwf_J_prog P"
  shows red_fv_subset: "extTA,P,t ⊢ ⟨e, s⟩ -ta→ ⟨e', s'⟩ ⟹ fv e' ⊆ fv e"
  and reds_fvs_subset: "extTA,P,t ⊢ ⟨es, s⟩ [-ta→] ⟨es', s'⟩ ⟹ fvs es' ⊆ fvs es"
proof(induct rule: red_reds.inducts)
  case (RedCall s a U M Ts T pns body D vs)
  hence "fv body ⊆ {this} ∪ set pns"
    using wf by(fastforce dest!:sees_wf_mdecl simp:wf_mdecl_def)
  with RedCall show ?case by fastforce
next
  case RedCallExternal thus ?case by(auto simp add: extRet2J_def split: extCallRet.split_asm)
qed(fastforce)+

end

declare domIff[iff del]

context J_heap_base begin

lemma assumes wwf: "wwf_J_prog P"
  shows red_fv_ok: "⟦ extTA,P,t ⊢ ⟨e, s⟩ -ta→ ⟨e', s'⟩; fv e ⊆ dom (lcl s) ⟧ ⟹ fv e' ⊆ dom (lcl s')"
  and reds_fvs_ok: "⟦ extTA,P,t ⊢ ⟨es, s⟩ [-ta→] ⟨es', s'⟩; fvs es ⊆ dom (lcl s) ⟧ ⟹ fvs es' ⊆ dom (lcl s')"
proof(induct rule: red_reds.inducts)
  case (RedCall s a U M Ts T pns body D vs)
  from ‹P ⊢ class_type_of U sees M: Ts→T = ⌊(pns, body)⌋ in D› have "wwf_J_mdecl P D (M,Ts,T,pns,body)"
    by(auto dest!: sees_wf_mdecl[OF wwf] simp add: wf_mdecl_def)
  with RedCall show ?case by(auto)
next
  case RedCallExternal thus ?case by(auto simp add: extRet2J_def split: extCallRet.split_asm)
next
  case (BlockRed e h x V vo ta e' h' x' T)
  note red = ‹extTA,P,t ⊢ ⟨e,(h, x(V := vo))⟩ -ta→ ⟨e',(h', x')⟩›
  hence "fv e' ⊆ fv e" by(auto dest: red_fv_subset[OF wwf] del: subsetI)
  moreover from ‹ fv {V:T=vo; e} ⊆ dom (lcl (h, x))›
  have "fv e - {V} ⊆ dom x" by(simp)
  ultimately have "fv e' - {V} ⊆ dom x - {V}" by(auto)
  moreover from red have "dom (x(V := vo)) ⊆ dom x'"
    by(auto dest: red_lcl_incr del: subsetI)
  ultimately have "fv e' - {V} ⊆ dom x' - {V}"
    by(auto split: if_split_asm)
  thus ?case by(auto simp del: fun_upd_apply)
qed(fastforce dest: red_lcl_incr del: subsetI)+

lemma is_call_red_state_unchanged: 
  "⟦ extTA,P,t ⊢ ⟨e, s⟩ -ta→ ⟨e', s'⟩; call e = ⌊aMvs⌋; ¬ synthesized_call P (hp s) aMvs ⟧ ⟹ s' = s ∧ ta = ε"

  and is_calls_reds_state_unchanged:
  "⟦ extTA,P,t ⊢ ⟨es, s⟩ [-ta→] ⟨es', s'⟩; calls es = ⌊aMvs⌋; ¬ synthesized_call P (hp s) aMvs ⟧ ⟹ s' = s ∧ ta = ε"
apply(induct rule: red_reds.inducts)
apply(fastforce split: if_split_asm simp add: synthesized_call_def)+
done

lemma called_methodD:
  "⟦ extTA,P,t ⊢ ⟨e, s⟩ -ta→ ⟨e', s'⟩; call e = ⌊(a, M, vs)⌋; ¬ synthesized_call P (hp s) (a, M, vs) ⟧ 
  ⟹ ∃hT D Us U pns body. hp s' = hp s ∧ typeof_addr (hp s) a = ⌊hT⌋ ∧
                           P ⊢ class_type_of hT sees M: Us→U = ⌊(pns, body)⌋ in D ∧ 
                           length vs = length pns ∧ length Us = length pns"

  and called_methodsD:
  "⟦ extTA,P,t ⊢ ⟨es, s⟩ [-ta→] ⟨es', s'⟩; calls es = ⌊(a, M, vs)⌋; ¬ synthesized_call P (hp s) (a, M, vs) ⟧ 
  ⟹ ∃hT D Us U pns body. hp s' = hp s ∧ typeof_addr (hp s) a = ⌊hT⌋ ∧
                           P ⊢ class_type_of hT sees M: Us→U = ⌊(pns, body)⌋ in D ∧
                           length vs = length pns ∧ length Us = length pns"
apply(induct rule: red_reds.inducts)
apply(auto split: if_split_asm simp add: synthesized_call_def)
apply(fastforce)
done

subsection ‹Silent moves›

primrec  τmove0 :: "'m prog ⇒ 'heap ⇒ ('a, 'b, 'addr) exp ⇒ bool"
  and τmoves0 :: "'m prog ⇒ 'heap ⇒ ('a, 'b, 'addr) exp list ⇒ bool"
where
  "τmove0 P h (new C) ⟷ False"
| "τmove0 P h (newA T⌊e⌉) ⟷ τmove0 P h e ∨ (∃a. e = Throw a)"
| "τmove0 P h (Cast U e) ⟷ τmove0 P h e ∨ (∃a. e = Throw a) ∨ (∃v. e = Val v)"
| "τmove0 P h (e instanceof T) ⟷ τmove0 P h e ∨ (∃a. e = Throw a) ∨ (∃v. e = Val v)"
| "τmove0 P h (e «bop» e') ⟷ τmove0 P h e ∨ (∃a. e = Throw a) ∨ (∃v. e = Val v ∧
   (τmove0 P h e' ∨ (∃a. e' = Throw a) ∨ (∃v. e' = Val v)))"
| "τmove0 P h (Val v) ⟷ False"
| "τmove0 P h (Var V) ⟷ True"
| "τmove0 P h (V := e) ⟷ τmove0 P h e ∨ (∃a. e = Throw a) ∨ (∃v. e = Val v)"
| "τmove0 P h (a⌊i⌉) ⟷ τmove0 P h a ∨ (∃ad. a = Throw ad) ∨ (∃v. a = Val v ∧ (τmove0 P h i ∨ (∃a. i = Throw a)))"
| "τmove0 P h (AAss a i e) ⟷ τmove0 P h a ∨ (∃ad. a = Throw ad) ∨ (∃v. a = Val v ∧ 
   (τmove0 P h i ∨ (∃a. i = Throw a) ∨ (∃v. i = Val v ∧ (τmove0 P h e ∨ (∃a. e = Throw a)))))"
| "τmove0 P h (a∙length) ⟷ τmove0 P h a ∨ (∃ad. a = Throw ad)"
| "τmove0 P h (e∙F{D}) ⟷ τmove0 P h e ∨ (∃a. e = Throw a)"
| "τmove0 P h (FAss e F D e') ⟷ τmove0 P h e ∨ (∃a. e = Throw a) ∨ (∃v. e = Val v ∧ (τmove0 P h e' ∨ (∃a. e' = Throw a)))"
| "τmove0 P h (e∙compareAndSwap(D∙F, e', e'')) ⟷ τmove0 P h e ∨ (∃a. e = Throw a) ∨ (∃v. e = Val v ∧
   (τmove0 P h e' ∨ (∃a. e' = Throw a) ∨ (∃v. e' = Val v ∧ (τmove0 P h e'' ∨ (∃a. e'' = Throw a)))))"
| "τmove0 P h (e∙M(es)) ⟷ τmove0 P h e ∨ (∃a. e = Throw a) ∨ (∃v. e = Val v ∧
   ((τmoves0 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)))))"
| "τmove0 P h ({V:T=vo; e}) ⟷ τmove0 P h e ∨ ((∃a. e = Throw a) ∨ (∃v. e = Val v))"
| "τmove0 P h (sync⇘V'⇙(e) e') ⟷ τmove0 P h e ∨ (∃a. e = Throw a)"
| "τmove0 P h (insync⇘V'⇙(ad) e) ⟷ τmove0 P h e"
| "τmove0 P h (e;;e') ⟷ τmove0 P h e ∨ (∃a. e = Throw a) ∨ (∃v. e = Val v)"
| "τmove0 P h (if (e) e' else e'') ⟷ τmove0 P h e ∨ (∃a. e = Throw a) ∨ (∃v. e = Val v)"
| "τmove0 P h (while (e) e') = True"
| ― ‹@{term "Throw a"} is no @{text "τmove0"} because there is no reduction for it.
  If it were, most defining equations would be simpler. However, @{term "insync⇘V'⇙(ad) (Throw ad)"}
  must not be a @{text "τmove0"}, but would be if @{term "Throw a"} was.›
  "τmove0 P h (throw e) ⟷ τmove0 P h e ∨ (∃a. e = Throw a) ∨ e = null"
| "τmove0 P h (try e catch(C V) e') ⟷ τmove0 P h e ∨ (∃a. e = Throw a) ∨ (∃v. e = Val v)"

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

abbreviation τMOVE :: "'m prog ⇒ (('addr expr × 'addr locals) × 'heap, ('addr, 'thread_id, 'heap) J_thread_action) trsys"
where "τMOVE ≡ λP ((e, x), h) ta s'. τmove0 P h e ∧ ta = ε"

primrec τMove0 :: "'m prog ⇒ 'heap ⇒ ('addr expr × 'addr expr list) ⇒ bool"
where
  "τMove0 P h (e, exs) = (τmove0 P h e ∨ final e)"
  
abbreviation τMOVE0 :: "'m prog ⇒ (('addr expr × 'addr expr list) × 'heap, ('addr, 'thread_id, 'heap) J0_thread_action) trsys"
where "τMOVE0 ≡ λP (es, h) ta s. τMove0 P h es ∧ ta = ε"

definition τred0 ::
  "(('addr, 'thread_id, 'heap) external_thread_action ⇒ ('addr, 'thread_id, 'x,'heap) Jinja_thread_action)
  ⇒ 'addr J_prog ⇒ 'thread_id ⇒ 'heap ⇒ ('addr expr × 'addr locals) ⇒ ('addr expr × 'addr locals) ⇒ bool"
where
  "τred0 extTA P t h exs e'xs' =
   (extTA,P,t ⊢ ⟨fst exs, (h, snd exs)⟩ -ε→ ⟨fst e'xs', (h, snd e'xs')⟩ ∧ τmove0 P h (fst exs) ∧ no_call P h (fst exs))"

definition τreds0 :: 
  "(('addr, 'thread_id, 'heap) external_thread_action ⇒ ('addr, 'thread_id, 'x,'heap) Jinja_thread_action) 
  ⇒ 'addr J_prog ⇒ 'thread_id ⇒ 'heap ⇒ ('addr expr list × 'addr locals) ⇒ ('addr expr list × 'addr locals) ⇒ bool"
where 
  "τreds0 extTA P t h esxs es'xs' = 
   (extTA,P,t ⊢ ⟨fst esxs, (h, snd esxs)⟩ [-ε→] ⟨fst es'xs', (h, snd es'xs')⟩ ∧ τmoves0 P h (fst esxs) ∧
    no_calls P h (fst esxs))"

abbreviation τred0t ::
  "(('addr, 'thread_id, 'heap) external_thread_action ⇒ ('addr, 'thread_id, 'x,'heap) Jinja_thread_action) 
  ⇒ 'addr J_prog ⇒ 'thread_id ⇒ 'heap ⇒ ('addr expr × 'addr locals) ⇒ ('addr expr × 'addr locals) ⇒ bool"
where "τred0t extTA P t h ≡ (τred0 extTA P t h)^++"

abbreviation τreds0t ::
  "(('addr, 'thread_id, 'heap) external_thread_action ⇒ ('addr, 'thread_id, 'x,'heap) Jinja_thread_action) 
  ⇒ 'addr J_prog ⇒ 'thread_id ⇒ 'heap ⇒ ('addr expr list × 'addr locals) ⇒ ('addr expr list × 'addr locals) ⇒ bool"
where "τreds0t extTA P t h ≡ (τreds0 extTA P t h)^++"

abbreviation τred0r :: 
  "(('addr, 'thread_id, 'heap) external_thread_action ⇒ ('addr, 'thread_id, 'x,'heap) Jinja_thread_action) 
  ⇒ 'addr J_prog ⇒ 'thread_id ⇒ 'heap ⇒ ('addr expr × 'addr locals) ⇒ ('addr expr × 'addr locals) ⇒ bool"
where "τred0r extTA P t h ≡ (τred0 extTA P t h)^**"

abbreviation τreds0r :: 
  "(('addr, 'thread_id, 'heap) external_thread_action ⇒ ('addr, 'thread_id, 'x,'heap) Jinja_thread_action)
  ⇒ 'addr J_prog ⇒ 'thread_id ⇒ 'heap ⇒ ('addr expr list × 'addr locals) ⇒ ('addr expr list × 'addr locals) ⇒ bool"
where "τreds0r extTA P t h ≡ (τreds0 extTA P t h)^**"

definition τRed0 :: 
  "'addr J_prog ⇒ 'thread_id ⇒ 'heap ⇒ ('addr expr × 'addr expr list) ⇒ ('addr expr × 'addr expr list) ⇒ bool"
where "τRed0 P t h ees e'es' = (P,t ⊢0 ⟨fst ees/snd ees, h⟩ -ε→ ⟨fst e'es'/snd e'es', h⟩ ∧ τMove0 P h ees)"

abbreviation τRed0r ::
  "'addr J_prog ⇒ 'thread_id ⇒ 'heap ⇒ ('addr expr × 'addr expr list) ⇒ ('addr expr × 'addr expr list) ⇒ bool"
where "τRed0r P t h ≡ (τRed0 P t h)^**"

abbreviation τRed0t ::
  "'addr J_prog ⇒ 'thread_id ⇒ 'heap ⇒ ('addr expr × 'addr expr list) ⇒ ('addr expr × 'addr expr list) ⇒ bool"
where "τRed0t P t h ≡ (τRed0 P t h)^++"

lemma τmove0_τmoves0_intros:
  fixes e e1 e2 e' :: "('a, 'b, 'addr) exp" and es :: "('a, 'b, 'addr) exp list"
  shows τmove0NewArray: "τmove0 P h e ⟹ τmove0 P h (newA T⌊e⌉)"
  and τmove0Cast: "τmove0 P h e ⟹ τmove0 P h (Cast U e)"
  and τmove0CastRed: "τmove0 P h (Cast U (Val v))"
  and τmove0InstanceOf: "τmove0 P h e ⟹ τmove0 P h (e instanceof T)"
  and τmove0InstanceOfRed: "τmove0 P h ((Val v) instanceof T)"
  and τmove0BinOp1: "τmove0 P h e ⟹ τmove0 P h (e«bop»e')"
  and τmove0BinOp2: "τmove0 P h e ⟹ τmove0 P h (Val v«bop»e)"
  and τmove0BinOp: "τmove0 P h (Val v«bop»Val v')"
  and τmove0Var: "τmove0 P h (Var V)"
  and τmove0LAss: "τmove0 P h e ⟹ τmove0 P h (V := e)"
  and τmove0LAssRed: "τmove0 P h (V := Val v)"
  and τmove0AAcc1: "τmove0 P h e ⟹ τmove0 P h (e⌊e'⌉)"
  and τmove0AAcc2: "τmove0 P h e ⟹ τmove0 P h (Val v⌊e⌉)"
  and τmove0AAss1: "τmove0 P h e ⟹ τmove0 P h (e⌊e1⌉ := e2)"
  and τmove0AAss2: "τmove0 P h e ⟹ τmove0 P h (Val v⌊e⌉ := e')"
  and τmove0AAss3: "τmove0 P h e ⟹ τmove0 P h (Val v⌊Val v'⌉ := e)"
  and τmove0ALength: "τmove0 P h e ⟹ τmove0 P h (e∙length)"
  and τmove0FAcc: "τmove0 P h e ⟹ τmove0 P h (e∙F{D})"
  and τmove0FAss1: "τmove0 P h e ⟹ τmove0 P h (FAss e F D e')"
  and τmove0FAss2: "τmove0 P h e ⟹ τmove0 P h (Val v∙F{D} := e)"
  and τmove0CAS1: "τmove0 P h e ⟹ τmove0 P h (e∙compareAndSwap(D∙F, e', e''))"
  and τmove0CAS2: "τmove0 P h e' ⟹ τmove0 P h (Val v∙compareAndSwap(D∙F, e', e''))"
  and τmove0CAS3: "τmove0 P h e'' ⟹ τmove0 P h (Val v∙compareAndSwap(D∙F, Val v', e''))"
  and τmove0CallObj: "τmove0 P h e ⟹ τmove0 P h (e∙M(es))"
  and τmove0CallParams: "τmoves0 P h es ⟹ τmove0 P h (Val v∙M(es))"
  and τmove0Call: "(⋀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) ⟹ τmove0 P h (Val v∙M(map Val vs))"
  and τmove0Block: "τmove0 P h e ⟹ τmove0 P h {V:T=vo; e}"
  and τmove0BlockRed: "τmove0 P h {V:T=vo; Val v}"
  and τmove0Sync: "τmove0 P h e ⟹ τmove0 P h (sync⇘V'⇙ (e) e')"
  and τmove0InSync: "τmove0 P h e ⟹ τmove0 P h (insync⇘V'⇙ (a) e)"
  and τmove0Seq: "τmove0 P h e ⟹ τmove0 P h (e;;e')"
  and τmove0SeqRed: "τmove0 P h (Val v;; e')"
  and τmove0Cond: "τmove0 P h e ⟹ τmove0 P h (if (e) e1 else e2)"
  and τmove0CondRed: "τmove0 P h (if (Val v) e1 else e2)"
  and τmove0WhileRed: "τmove0 P h (while (e) e')"
  and τmove0Throw: "τmove0 P h e ⟹ τmove0 P h (throw e)"
  and τmove0ThrowNull: "τmove0 P h (throw null)"
  and τmove0Try: "τmove0 P h e ⟹ τmove0 P h (try e catch(C V) e')"
  and τmove0TryRed: "τmove0 P h (try Val v catch(C V) e)"
  and τmove0TryThrow: "τmove0 P h (try Throw a catch(C V) e)"
  and τmove0NewArrayThrow: "τmove0 P h (newA T⌊Throw a⌉)"
  and τmove0CastThrow: "τmove0 P h (Cast T (Throw a))"
  and τmove0CInstanceOfThrow: "τmove0 P h ((Throw a) instanceof T)"
  and τmove0BinOpThrow1: "τmove0 P h (Throw a «bop» e')"
  and τmove0BinOpThrow2: "τmove0 P h (Val v «bop» Throw a)"
  and τmove0LAssThrow: "τmove0 P h (V:=(Throw a))"
  and τmove0AAccThrow1: "τmove0 P h (Throw a⌊e⌉)"
  and τmove0AAccThrow2: "τmove0 P h (Val v⌊Throw a⌉)"
  and τmove0AAssThrow1: "τmove0 P h (AAss (Throw a) e e')"
  and τmove0AAssThrow2: "τmove0 P h (AAss (Val v) (Throw a) e')"
  and τmove0AAssThrow3: "τmove0 P h (AAss (Val v) (Val v') (Throw a))"
  and τmove0ALengthThrow: "τmove0 P h (Throw a∙length)"
  and τmove0FAccThrow: "τmove0 P h (Throw a∙F{D})"
  and τmove0FAssThrow1: "τmove0 P h (Throw a∙F{D} := e)"
  and τmove0FAssThrow2: "τmove0 P h (FAss (Val v) F D (Throw a))"
  and τmove0CallThrowObj: "τmove0 P h (Throw a∙M(es))"
  and τmove0CallThrowParams: "τmove0 P h (Val v∙M(map Val vs @ Throw a # es))"
  and τmove0BlockThrow: "τmove0 P h {V:T=vo; Throw a}"
  and τmove0SyncThrow: "τmove0 P h (sync⇘V'⇙ (Throw a) e)"
  and τmove0SeqThrow: "τmove0 P h (Throw a;;e)"
  and τmove0CondThrow: "τmove0 P h (if (Throw a) e1 else e2)"
  and τmove0ThrowThrow: "τmove0 P h (throw (Throw a))"

  and τmoves0Hd: "τmove0 P h e ⟹ τmoves0 P h (e # es)"
  and τmoves0Tl: "τmoves0 P h es ⟹ τmoves0 P h (Val v # es)"
by auto

lemma τmoves0_map_Val [iff]:
  "¬ τmoves0 P h (map Val vs)"
by(induct vs) auto

lemma τmoves0_map_Val_append [simp]:
  "τmoves0 P h (map Val vs @ es) = τmoves0 P h es"
by(induct vs)(auto)

lemma no_reds_map_Val_Throw [simp]:
  "extTA,P,t ⊢ ⟨map Val vs @ Throw a # es, s⟩ [-ta→] ⟨es', s'⟩ = False"
by(induct vs arbitrary: es')(auto elim: reds.cases)

lemma assumes [simp]: "extTA ε = ε"
  shows red_τ_taD: "⟦ extTA,P,t ⊢ ⟨e, s⟩ -ta→ ⟨e', s'⟩; τmove0 P (hp s) e ⟧ ⟹ ta = ε"
  and reds_τ_taD: "⟦ extTA,P,t ⊢ ⟨es, s⟩ [-ta→] ⟨es', s'⟩; τmoves0 P (hp s) es ⟧ ⟹ ta = ε"
apply(induct rule: red_reds.inducts)
apply(fastforce simp add: map_eq_append_conv τexternal'_def τexternal_def dest: τexternal'_red_external_TA_empty)+
done

lemma τmove0_heap_unchanged: "⟦ extTA,P,t ⊢ ⟨e, s⟩ -ta→ ⟨e', s'⟩; τmove0 P (hp s) e ⟧ ⟹ hp s' = hp s"
  and τmoves0_heap_unchanged: "⟦ extTA,P,t ⊢ ⟨es, s⟩ [-ta→] ⟨es', s'⟩; τmoves0 P (hp s) es ⟧ ⟹ hp s' = hp s"
apply(induct rule: red_reds.inducts)
apply(auto)
apply(fastforce simp add: map_eq_append_conv τexternal'_def τexternal_def dest: τexternal'_red_external_heap_unchanged)+
done

lemma τMove0_iff:
  "τMove0 P h ees ⟷ (let (e, _) = ees in τmove0 P h e ∨ final e)"
by(cases ees)(simp)

lemma no_call_simps [simp]:
  "no_call P h (new C) = True"
  "no_call P h (newA T⌊e⌉) = no_call P h e"
  "no_call P h (Cast T e) = no_call P h e"
  "no_call P h (e instanceof T) = no_call P h e"
  "no_call P h (Val v) = True"
  "no_call P h (Var V) = True"
  "no_call P h (V := e) = no_call P h e"
  "no_call P h (e «bop» e') = (if is_val e then no_call P h e' else no_call P h e)"
  "no_call P h (a⌊i⌉) = (if is_val a then no_call P h i else no_call P h a)"
  "no_call P h (AAss a i e) = (if is_val a then (if is_val i then no_call P h e else no_call P h i) else no_call P h a)"
  "no_call P h (a∙length) = no_call P h a"
  "no_call P h (e∙F{D}) = no_call P h e"
  "no_call P h (FAss e F D e') = (if is_val e then no_call P h e' else no_call P h e)"
  "no_call P h (e∙compareAndSwap(D∙F, e', e'')) = (if is_val e then (if is_val e' then no_call P h e'' else no_call P h e') else no_call P h e)"
  "no_call P h (e∙M(es)) = (if is_val e then (if is_vals es ∧ is_addr e then synthesized_call P h (THE a. e = addr a, M, THE vs. es = map Val vs) else no_calls P h es) else no_call P h e)"
  "no_call P h ({V:T=vo; e}) = no_call P h e"
  "no_call P h (sync⇘V'⇙ (e) e') = no_call P h e"
  "no_call P h (insync⇘V'⇙ (ad) e) = no_call P h e"
  "no_call P h (e;;e') = no_call P h e"
  "no_call P h (if (e) e1 else e2) = no_call P h e"
  "no_call P h (while(e) e') = True"
  "no_call P h (throw e) = no_call P h e"
  "no_call P h (try e catch(C V) e') = no_call P h e"
by(auto simp add: no_call_def no_calls_def)

lemma no_calls_simps [simp]:
  "no_calls P h [] = True"
  "no_calls P h (e # es) = (if is_val e then no_calls P h es else no_call P h e)"
by(simp_all add: no_call_def no_calls_def)

lemma no_calls_map_Val [simp]:
  "no_calls P h (map Val vs)"
by(induct vs) simp_all

lemma assumes nfin: "¬ final e'"
 shows inline_call_τmove0_inv: "call e = ⌊aMvs⌋ ⟹ τmove0 P h (inline_call e' e) = τmove0 P h e'"
  and inline_calls_τmoves0_inv: "calls es = ⌊aMvs⌋ ⟹ τmoves0 P h (inline_calls e' es) = τmove0 P h e'"
apply(induct e and es rule: τmove0.induct τmoves0.induct)
apply(insert nfin)
apply simp_all
apply auto
done

lemma τred0_iff [iff]:
  "τred0 extTA P t h (e, xs) (e', xs') = (extTA,P,t ⊢ ⟨e, (h, xs)⟩ -ε→ ⟨e', (h, xs')⟩ ∧ τmove0 P h e ∧ no_call P h e)"
by(simp add: τred0_def)

lemma τreds0_iff [iff]:
  "τreds0 extTA P t h (es, xs) (es', xs') =
  (extTA,P,t ⊢ ⟨es, (h, xs)⟩ [-ε→] ⟨es', (h, xs')⟩ ∧ τmoves0 P h es ∧ no_calls P h es)"
by(simp add: τreds0_def)

lemma τred0t_1step:
  "⟦ extTA,P,t ⊢ ⟨e, (h, xs)⟩ -ε→ ⟨e', (h, xs')⟩; τmove0 P h e; no_call P h e ⟧
  ⟹ τred0t extTA P t h (e, xs) (e', xs')"
by(blast intro: tranclp.r_into_trancl)

lemma τred0t_2step:
  "⟦ extTA,P,t ⊢ ⟨e, (h, xs)⟩ -ε→ ⟨e', (h, xs')⟩; τmove0 P h e; no_call P h e;
     extTA,P,t ⊢ ⟨e', (h, xs')⟩ -ε→ ⟨e'', (h, xs'')⟩; τmove0 P h e'; no_call P h e' ⟧
  ⟹ τred0t extTA P t h (e, xs) (e'', xs'')"
by(blast intro: tranclp.trancl_into_trancl[OF τred0t_1step])

lemma τred1t_3step:
  "⟦ extTA,P,t ⊢ ⟨e, (h, xs)⟩ -ε→ ⟨e', (h, xs')⟩; τmove0 P h e; no_call P h e; 
     extTA,P,t ⊢ ⟨e', (h, xs')⟩ -ε→ ⟨e'', (h, xs'')⟩; τmove0 P h e'; no_call P h e';
     extTA,P,t ⊢ ⟨e'', (h, xs'')⟩ -ε→ ⟨e''', (h, xs''')⟩; τmove0 P h e''; no_call P h e'' ⟧
  ⟹ τred0t extTA P t h (e, xs) (e''', xs''')"
by(blast intro: tranclp.trancl_into_trancl[OF τred0t_2step])

lemma τreds0t_1step:
  "⟦ extTA,P,t ⊢ ⟨es, (h, xs)⟩ [-ε→] ⟨es', (h, xs')⟩; τmoves0 P h es; no_calls P h es ⟧
  ⟹ τreds0t extTA P t h (es, xs) (es', xs')"
by(blast intro: tranclp.r_into_trancl)

lemma τreds0t_2step:
  "⟦ extTA,P,t ⊢ ⟨es, (h, xs)⟩ [-ε→] ⟨es', (h, xs')⟩; τmoves0 P h es; no_calls P h es; 
     extTA,P,t ⊢ ⟨es', (h, xs')⟩ [-ε→] ⟨es'', (h, xs'')⟩; τmoves0 P h es'; no_calls P h es' ⟧
  ⟹ τreds0t extTA P t h (es, xs) (es'', xs'')"
by(blast intro: tranclp.trancl_into_trancl[OF τreds0t_1step])

lemma τreds0t_3step:
  "⟦ extTA,P,t ⊢ ⟨es, (h, xs)⟩ [-ε→] ⟨es', (h, xs')⟩; τmoves0 P h es; no_calls P h es; 
     extTA,P,t ⊢ ⟨es', (h, xs')⟩ [-ε→] ⟨es'', (h, xs'')⟩; τmoves0 P h es'; no_calls P h es';
     extTA,P,t ⊢ ⟨es'', (h, xs'')⟩ [-ε→] ⟨es''', (h, xs''')⟩; τmoves0 P h es''; no_calls P h es'' ⟧
  ⟹ τreds0t extTA P t h (es, xs) (es''', xs''')"
by(blast intro: tranclp.trancl_into_trancl[OF τreds0t_2step])

lemma τred0r_1step:
  "⟦ extTA,P,t ⊢ ⟨e, (h, xs)⟩ -ε→ ⟨e', (h, xs')⟩; τmove0 P h e; no_call P h e ⟧
  ⟹ τred0r extTA P t h (e, xs) (e', xs')"
by(blast intro: r_into_rtranclp)

lemma τred0r_2step:
  "⟦ extTA,P,t ⊢ ⟨e, (h, xs)⟩ -ε→ ⟨e', (h, xs')⟩; τmove0 P h e; no_call P h e;
     extTA,P,t ⊢ ⟨e', (h, xs')⟩ -ε→ ⟨e'', (h, xs'')⟩; τmove0 P h e'; no_call P h e' ⟧
  ⟹ τred0r extTA P t h (e, xs) (e'', xs'')"
by(blast intro: rtranclp.rtrancl_into_rtrancl[OF τred0r_1step])

lemma τred0r_3step:
  "⟦ extTA,P,t ⊢ ⟨e, (h, xs)⟩ -ε→ ⟨e', (h, xs')⟩; τmove0 P h e; no_call P h e; 
     extTA,P,t ⊢ ⟨e', (h, xs')⟩ -ε→ ⟨e'', (h, xs'')⟩; τmove0 P h e'; no_call P h e';
     extTA,P,t ⊢ ⟨e'', (h, xs'')⟩ -ε→ ⟨e''', (h, xs''')⟩; τmove0 P h e''; no_call P h e'' ⟧
  ⟹ τred0r extTA P t h (e, xs) (e''', xs''')"
by(blast intro: rtranclp.rtrancl_into_rtrancl[OF τred0r_2step])

lemma τreds0r_1step:
  "⟦ extTA,P,t ⊢ ⟨es, (h, xs)⟩ [-ε→] ⟨es', (h, xs')⟩; τmoves0 P h es; no_calls P h es ⟧
  ⟹ τreds0r extTA P t h (es, xs) (es', xs')"
by(blast intro: r_into_rtranclp)

lemma τreds0r_2step:
  "⟦ extTA,P,t ⊢ ⟨es, (h, xs)⟩ [-ε→] ⟨es', (h, xs')⟩; τmoves0 P h es; no_calls P h es; 
     extTA,P,t ⊢ ⟨es', (h, xs')⟩ [-ε→] ⟨es'', (h, xs'')⟩; τmoves0 P h es'; no_calls P h es' ⟧
  ⟹ τreds0r extTA P t h (es, xs) (es'', xs'')"
by(blast intro: rtranclp.rtrancl_into_rtrancl[OF τreds0r_1step])

lemma τreds0r_3step:
  "⟦ extTA,P,t ⊢ ⟨es, (h, xs)⟩ [-ε→] ⟨es', (h, xs')⟩; τmoves0 P h es; no_calls P h es; 
     extTA,P,t ⊢ ⟨es', (h, xs')⟩ [-ε→] ⟨es'', (h, xs'')⟩; τmoves0 P h es'; no_calls P h es';
     extTA,P,t ⊢ ⟨es'', (h, xs'')⟩ [-ε→] ⟨es''', (h, xs''')⟩; τmoves0 P h es''; no_calls P h es'' ⟧
  ⟹ τreds0r extTA P t h (es, xs) (es''', xs''')"
by(blast intro: rtranclp.rtrancl_into_rtrancl[OF τreds0r_2step])

lemma τred0t_inj_τreds0t:
  "τred0t extTA P t h (e, xs) (e', xs')
  ⟹ τreds0t extTA P t h (e # es, xs) (e' # es, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl ListRed1)

lemma τreds0t_cons_τreds0t:
  "τreds0t extTA P t h (es, xs) (es', xs')
  ⟹ τreds0t extTA P t h (Val v # es, xs) (Val v # es', xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl ListRed2)

lemma τred0r_inj_τreds0r:
  "τred0r extTA P t h (e, xs) (e', xs')
  ⟹ τreds0r extTA P t h (e # es, xs) (e' # es, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl ListRed1)

lemma τreds0r_cons_τreds0r:
  "τreds0r extTA P t h (es, xs) (es', xs') 
  ⟹ τreds0r extTA P t h (Val v # es, xs) (Val v # es', xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl ListRed2)

lemma NewArray_τred0t_xt:
  "τred0t extTA P t h (e, xs) (e', xs')
  ⟹ τred0t extTA P t h (newA T⌊e⌉, xs) (newA T⌊e'⌉, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl NewArrayRed)

lemma Cast_τred0t_xt:
  "τred0t extTA P t h (e, xs) (e', xs') ⟹ τred0t extTA P t h (Cast T e, xs) (Cast T e', xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl CastRed)

lemma InstanceOf_τred0t_xt:
  "τred0t extTA P t h (e, xs) (e', xs') ⟹ τred0t extTA P t h (e instanceof T, xs) (e' instanceof T, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl InstanceOfRed)

lemma BinOp_τred0t_xt1:
  "τred0t extTA P t h (e1, xs) (e1', xs') ⟹ τred0t extTA P t h (e1 «bop» e2, xs) (e1' «bop» e2, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl BinOpRed1)

lemma BinOp_τred0t_xt2:
  "τred0t extTA P t h (e2, xs) (e2', xs') ⟹ τred0t extTA P t h (Val v «bop» e2, xs) (Val v «bop» e2', xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl BinOpRed2)

lemma LAss_τred0t:
  "τred0t extTA P t h (e, xs) (e', xs') ⟹ τred0t extTA P t h (V := e, xs) (V := e', xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl LAssRed)

lemma AAcc_τred0t_xt1:
  "τred0t extTA P t h (a, xs) (a', xs') ⟹ τred0t extTA P t h (a⌊i⌉, xs) (a'⌊i⌉, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl AAccRed1)

lemma AAcc_τred0t_xt2:
  "τred0t extTA P t h (i, xs) (i', xs') ⟹ τred0t extTA P t h (Val a⌊i⌉, xs) (Val a⌊i'⌉, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl AAccRed2)

lemma AAss_τred0t_xt1:
  "τred0t extTA P t h (a, xs) (a', xs') ⟹ τred0t extTA P t h (a⌊i⌉ := e, xs) (a'⌊i⌉ := e, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl AAssRed1)

lemma AAss_τred0t_xt2:
  "τred0t extTA P t h (i, xs) (i', xs') ⟹ τred0t extTA P t h (Val a⌊i⌉ := e, xs) (Val a⌊i'⌉ := e, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl AAssRed2)

lemma AAss_τred0t_xt3:
  "τred0t extTA P t h (e, xs) (e', xs') ⟹ τred0t extTA 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 AAssRed3)

lemma ALength_τred0t_xt:
  "τred0t extTA P t h (a, xs) (a', xs') ⟹ τred0t extTA P t h (a∙length, xs) (a'∙length, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl ALengthRed)

lemma FAcc_τred0t_xt:
  "τred0t extTA P t h (e, xs) (e', xs') ⟹ τred0t extTA P t h (e∙F{D}, xs) (e'∙F{D}, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl FAccRed)

lemma FAss_τred0t_xt1:
  "τred0t extTA P t h (e, xs) (e', xs') ⟹ τred0t extTA P t h (e∙F{D} := e2, xs) (e'∙F{D} := e2, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl FAssRed1)

lemma FAss_τred0t_xt2:
  "τred0t extTA P t h (e, xs) (e', xs') ⟹ τred0t extTA 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 FAssRed2)

lemma CAS_τred0t_xt1:
  "τred0t extTA P t h (e, xs) (e', xs') ⟹ τred0t extTA 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 CASRed1)

lemma CAS_τred0t_xt2:
  "τred0t extTA P t h (e, xs) (e', xs') ⟹ τred0t extTA 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 CASRed2)

lemma CAS_τred0t_xt3:
  "τred0t extTA P t h (e, xs) (e', xs') ⟹ τred0t extTA 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 CASRed3)

lemma Call_τred0t_obj:
  "τred0t extTA P t h (e, xs) (e', xs') ⟹ τred0t extTA P t h (e∙M(ps), xs) (e'∙M(ps), xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl CallObj)

lemma Call_τred0t_param:
  "τreds0t extTA P t h (es, xs) (es', xs') ⟹ τred0t extTA P t h (Val v∙M(es), xs) (Val v∙M(es'), xs')"
by(induct rule: tranclp_induct2)(fastforce intro: tranclp.trancl_into_trancl CallParams)+

lemma Block_τred0t_xt:
  "τred0t extTA P t h (e, xs(V := vo)) (e', xs') ⟹ τred0t extTA P t h ({V:T=vo; e}, xs) ({V:T=xs' V; e'}, xs'(V := xs V))"
proof(induct rule: tranclp_induct2)
  case base thus ?case by(auto intro: BlockRed simp del: fun_upd_apply)
next
  case (step e' xs' e'' xs'')
  from ‹τred0 extTA P t h (e', xs') (e'', xs'')› 
  have "extTA,P,t ⊢ ⟨e',(h, xs')⟩ -ε→ ⟨e'',(h, xs'')⟩" "τmove0 P h e'" "no_call P h e'" by auto
  hence "extTA,P,t ⊢ ⟨e',(h, xs'(V := xs V, V := xs' V))⟩ -ε→ ⟨e'',(h, xs'')⟩" by simp
  from BlockRed[OF this, of T] ‹τmove0 P h e'› ‹no_call P h e'›
  have "τred0 extTA P t h ({V:T=xs' V; e'}, xs'(V := xs V)) ({V:T=xs'' V; e''}, xs''(V := xs V))" by(auto)
  with ‹τred0t extTA P t h ({V:T=vo; e}, xs) ({V:T=xs' V; e'}, xs'(V := xs V))› show ?case ..
qed

lemma Sync_τred0t_xt:
  "τred0t extTA P t h (e, xs) (e', xs') ⟹ τred0t extTA P t h (sync⇘V⇙ (e) e2, xs) (sync⇘V⇙ (e') e2, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl SynchronizedRed1)

lemma InSync_τred0t_xt:
  "τred0t extTA P t h (e, xs) (e', xs') ⟹ τred0t extTA P t h (insync⇘V⇙ (a) e, xs) (insync⇘V⇙ (a) e', xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl SynchronizedRed2)

lemma Seq_τred0t_xt:
  "τred0t extTA P t h (e, xs) (e', xs') ⟹ τred0t extTA P t h (e;;e2, xs) (e';;e2, xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl SeqRed)

lemma Cond_τred0t_xt:
  "τred0t extTA P t h (e, xs) (e', xs') ⟹ τred0t extTA 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 CondRed)

lemma Throw_τred0t_xt:
  "τred0t extTA P t h (e, xs) (e', xs') ⟹ τred0t extTA P t h (throw e, xs) (throw e', xs')"
by(induct rule: tranclp_induct2)(auto intro: tranclp.trancl_into_trancl ThrowRed)

lemma Try_τred0t_xt:
  "τred0t extTA P t h (e, xs) (e', xs') ⟹ τred0t extTA 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 TryRed)

lemma NewArray_τred0r_xt:
  "τred0r extTA P t h (e, xs) (e', xs') ⟹ τred0r extTA P t h (newA T⌊e⌉, xs) (newA T⌊e'⌉, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl NewArrayRed)

lemma Cast_τred0r_xt:
  "τred0r extTA P t h (e, xs) (e', xs') ⟹ τred0r extTA P t h (Cast T e, xs) (Cast T e', xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl CastRed)

lemma InstanceOf_τred0r_xt:
  "τred0r extTA P t h (e, xs) (e', xs') ⟹ τred0r extTA P t h (e instanceof T, xs) (e' instanceof T, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl InstanceOfRed)

lemma BinOp_τred0r_xt1:
  "τred0r extTA P t h (e1, xs) (e1', xs') ⟹ τred0r extTA P t h (e1 «bop» e2, xs) (e1' «bop» e2, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl BinOpRed1)

lemma BinOp_τred0r_xt2:
  "τred0r extTA P t h (e2, xs) (e2', xs') ⟹ τred0r extTA P t h (Val v «bop» e2, xs) (Val v «bop» e2', xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl BinOpRed2)

lemma LAss_τred0r:
  "τred0r extTA P t h (e, xs) (e', xs') ⟹ τred0r extTA P t h (V := e, xs) (V := e', xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl LAssRed)

lemma AAcc_τred0r_xt1:
  "τred0r extTA P t h (a, xs) (a', xs') ⟹ τred0r extTA P t h (a⌊i⌉, xs) (a'⌊i⌉, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl AAccRed1)

lemma AAcc_τred0r_xt2:
  "τred0r extTA P t h (i, xs) (i', xs') ⟹ τred0r extTA P t h (Val a⌊i⌉, xs) (Val a⌊i'⌉, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl AAccRed2)

lemma AAss_τred0r_xt1:
  "τred0r extTA P t h (a, xs) (a', xs') ⟹ τred0r extTA P t h (a⌊i⌉ := e, xs) (a'⌊i⌉ := e, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl AAssRed1)

lemma AAss_τred0r_xt2:
  "τred0r extTA P t h (i, xs) (i', xs') ⟹ τred0r extTA P t h (Val a⌊i⌉ := e, xs) (Val a⌊i'⌉ := e, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl AAssRed2)

lemma AAss_τred0r_xt3:
  "τred0r extTA P t h (e, xs) (e', xs') ⟹ τred0r extTA 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 AAssRed3)

lemma ALength_τred0r_xt:
  "τred0r extTA P t h (a, xs) (a', xs') ⟹ τred0r extTA P t h (a∙length, xs) (a'∙length, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl ALengthRed)

lemma FAcc_τred0r_xt:
  "τred0r extTA P t h (e, xs) (e', xs') ⟹ τred0r extTA P t h (e∙F{D}, xs) (e'∙F{D}, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl FAccRed)

lemma FAss_τred0r_xt1:
  "τred0r extTA P t h (e, xs) (e', xs') ⟹ τred0r extTA P t h (e∙F{D} := e2, xs) (e'∙F{D} := e2, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl FAssRed1)

lemma FAss_τred0r_xt2:
  "τred0r extTA P t h (e, xs) (e', xs') ⟹ τred0r extTA 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 FAssRed2)

lemma CAS_τred0r_xt1:
  "τred0r extTA P t h (e, xs) (e', xs') ⟹ τred0r extTA 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 CASRed1)

lemma CAS_τred0r_xt2:
  "τred0r extTA P t h (e, xs) (e', xs') ⟹ τred0r extTA 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 CASRed2)

lemma CAS_τred0r_xt3:
  "τred0r extTA P t h (e, xs) (e', xs') ⟹ τred0r extTA 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 CASRed3)

lemma Call_τred0r_obj:
  "τred0r extTA P t h (e, xs) (e', xs') ⟹ τred0r extTA P t h (e∙M(ps), xs) (e'∙M(ps), xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl CallObj)

lemma Call_τred0r_param:
  "τreds0r extTA P t h (es, xs) (es', xs') ⟹ τred0r extTA P t h (Val v∙M(es), xs) (Val v∙M(es'), xs')"
by(induct rule: rtranclp_induct2)(fastforce intro: rtranclp.rtrancl_into_rtrancl CallParams)+

lemma Block_τred0r_xt:
  "τred0r extTA P t h (e, xs(V := vo)) (e', xs') ⟹ τred0r extTA P t h ({V:T=vo; e}, xs) ({V:T=xs' V; e'}, xs'(V := xs V))"
proof(induct rule: rtranclp_induct2)
  case refl thus ?case by(simp del: fun_upd_apply)(auto simp add: fun_upd_apply)
next
  case (step e' xs' e'' xs'')
  from ‹τred0 extTA P t h (e', xs') (e'', xs'')› 
  have "extTA,P,t ⊢ ⟨e',(h, xs')⟩ -ε→ ⟨e'',(h, xs'')⟩" "τmove0 P h e'" "no_call P h e'" by auto
  hence "extTA,P,t ⊢ ⟨e',(h, xs'(V := xs V, V := xs' V))⟩ -ε→ ⟨e'',(h, xs'')⟩" by simp
  from BlockRed[OF this, of T] ‹τmove0 P h e'› ‹no_call P h e'›
  have "τred0 extTA P t h ({V:T=xs' V; e'}, xs'(V := xs V)) ({V:T=xs'' V; e''}, xs''(V := xs V))" by auto
  with ‹τred0r extTA P t h ({V:T=vo; e}, xs) ({V:T=xs' V; e'}, xs'(V := xs V))› show ?case ..
qed

lemma Sync_τred0r_xt:
  "τred0r extTA P t h (e, xs) (e', xs') ⟹ τred0r extTA P t h (sync⇘V⇙ (e) e2, xs) (sync⇘V⇙ (e') e2, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl SynchronizedRed1)

lemma InSync_τred0r_xt:
  "τred0r extTA P t h (e, xs) (e', xs') ⟹ τred0r extTA P t h (insync⇘V⇙ (a) e, xs) (insync⇘V⇙ (a) e', xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl SynchronizedRed2)

lemma Seq_τred0r_xt:
  "τred0r extTA P t h (e, xs) (e', xs') ⟹ τred0r extTA P t h (e;;e2, xs) (e';;e2, xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl SeqRed)

lemma Cond_τred0r_xt:
  "τred0r extTA P t h (e, xs) (e', xs') ⟹ τred0r extTA 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 CondRed)

lemma Throw_τred0r_xt:
  "τred0r extTA P t h (e, xs) (e', xs') ⟹ τred0r extTA P t h (throw e, xs) (throw e', xs')"
by(induct rule: rtranclp_induct2)(auto intro: rtranclp.rtrancl_into_rtrancl ThrowRed)

lemma Try_τred0r_xt:
  "τred0r extTA P t h (e, xs) (e', xs') ⟹ τred0r extTA 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 TryRed)

lemma τRed0_conv [iff]:
  "τRed0 P t h (e, es) (e', es') = (P,t ⊢0 ⟨e/es, h⟩ -ε→ ⟨e'/es', h⟩ ∧ τMove0 P h (e, es))"
by(simp add: τRed0_def)

lemma τred0r_lcl_incr:
  "τred0r extTA P t h (e, xs) (e', xs') ⟹ dom xs ⊆ dom xs'"
by(induct rule: rtranclp_induct2)(auto dest: red_lcl_incr del: subsetI)

lemma τred0t_lcl_incr:
  "τred0t extTA P t h (e, xs) (e', xs') ⟹ dom xs ⊆ dom xs'"
by(rule τred0r_lcl_incr)(rule tranclp_into_rtranclp)

lemma τred0r_dom_lcl:
  assumes wwf: "wwf_J_prog P"
  shows "τred0r extTA P t h (e, xs) (e', xs') ⟹ dom xs' ⊆ dom xs ∪ fv e"
apply(induct rule: converse_rtranclp_induct2)
 apply blast
apply(clarsimp del: subsetI)
apply(frule red_dom_lcl)
 apply(drule red_fv_subset[OF wwf])
apply auto
done

lemma τred0t_dom_lcl:
  assumes wwf: "wwf_J_prog P"
  shows "τred0t extTA P t h (e, xs) (e', xs') ⟹ dom xs' ⊆ dom xs ∪ fv e"
by(rule τred0r_dom_lcl[OF wwf])(rule tranclp_into_rtranclp)

lemma τred0r_fv_subset:
  assumes wwf: "wwf_J_prog P"
  shows "τred0r extTA P t h (e, xs) (e', xs') ⟹ fv e' ⊆ fv e"
by(induct rule: converse_rtranclp_induct2)(auto dest: red_fv_subset[OF wwf])

lemma τred0t_fv_subset:
  assumes wwf: "wwf_J_prog P"
  shows "τred0t extTA P t h (e, xs) (e', xs') ⟹ fv e' ⊆ fv e"
by(rule τred0r_fv_subset[OF wwf])(rule tranclp_into_rtranclp)

lemma fixes e :: "('a, 'b, 'addr) exp" and es :: "('a, 'b, 'addr) exp list"
  shows τmove0_callD: "call e = ⌊(a, M, vs)⌋ ⟹ τmove0 P h e ⟷ (synthesized_call P h (a, M, vs) ⟶ τexternal' P h a M)"
  and τmoves0_callsD: "calls es = ⌊(a, M, vs)⌋ ⟹ τmoves0 P h es ⟷ (synthesized_call P h (a, M, vs) ⟶ τexternal' P h a M)"
apply(induct e and es rule: call.induct calls.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 fixes e :: "('a, 'b, 'addr) exp" and es :: "('a, 'b, 'addr) exp list"
  shows τmove0_not_call: "⟦ τmove0 P h e; call e = ⌊(a, M, vs)⌋; synthesized_call P h (a, M, vs) ⟧ ⟹ τexternal' P h a M"
  and τmoves0_not_calls: "⟦ τmoves0 P h es; calls es = ⌊(a, M, vs)⌋; synthesized_call P h (a, M, vs) ⟧ ⟹ τexternal' P h a M"
apply(drule τmove0_callD[where P=P and h=h], simp)
apply(drule τmoves0_callsD[where P=P and h=h], simp)
done

lemma τred0_into_τRed0:
  assumes red: "τred0 (extTA2J0 P) P t h (e, Map.empty) (e', xs')"
  shows "τRed0 P t h (e, es) (e', es)"
proof -
  from red have red: "extTA2J0 P,P,t ⊢ ⟨e, (h, Map.empty)⟩ -ε→ ⟨e', (h, xs')⟩"
    and "τmove0 P h e" and "no_call P h e" by auto
  hence "P,t ⊢0 ⟨e/es,h⟩ -ε→ ⟨e'/es,h⟩"
    by-(erule red0Red,auto simp add: no_call_def)
  thus ?thesis using ‹τmove0 P h e› by(auto)
qed

lemma τred0r_into_τRed0r:
  assumes wwf: "wwf_J_prog P"
  shows
  "⟦ τred0r (extTA2J0 P) P t h (e, Map.empty) (e'', Map.empty); fv e = {} ⟧
  ⟹ τRed0r P t h (e, es) (e'', es)"
proof(induct e xs≡"Map.empty :: 'addr locals" rule: converse_rtranclp_induct2)
  case refl show ?case by blast
next
  case (step e e' xs')
  from ‹τred0 (extTA2J0 P) P t h (e, Map.empty) (e', xs')›
  have red: "extTA2J0 P,P,t ⊢ ⟨e, (h, Map.empty)⟩ -ε→ ⟨e', (h, xs')⟩"
    and "τmove0 P h e"  and "no_call P h e" by auto
  from red_dom_lcl[OF red] ‹fv e = {}› 
  have "dom xs' = {}" by(auto split:if_split_asm)
  hence "xs' = Map.empty" by(auto)
  moreover
  from wwf red have "fv e' ⊆ fv e" by(rule red_fv_subset)
  with ‹fv e = {}› have "fv e' = {}" by blast
  ultimately have "τRed0r P t h (e', es) (e'', es)" by(rule step)
  moreover from red ‹τmove0 P h e› ‹xs' = Map.empty› ‹no_call P h e›
  have "τRed0 P t h (e, es) (e', es)" by(auto simp add: no_call_def intro!: red0Red)
  ultimately show ?case by(blast intro: converse_rtranclp_into_rtranclp)
qed


lemma τred0t_into_τRed0t:
  assumes wwf: "wwf_J_prog P"
  shows
  "⟦ τred0t (extTA2J0 P) P t h (e, Map.empty) (e'', Map.empty); fv e = {} ⟧
  ⟹ τRed0t P t h (e, es) (e'', es)"
proof(induct e xs≡"Map.empty :: 'addr locals" rule: converse_tranclp_induct2)
  case base thus ?case
    by(blast intro!: tranclp.r_into_trancl τred0_into_τRed0)
next
  case (step e e' xs')
  from ‹τred0 (extTA2J0 P) P t h (e, Map.empty) (e', xs')› 
  have red: "extTA2J0 P,P,t ⊢ ⟨e, (h, Map.empty)⟩ -ε→ ⟨e', (h, xs')⟩" and "τmove0 P h e" and "no_call P h e" by auto
  from red_dom_lcl[OF red] ‹fv e = {}›
  have "dom xs' = {}" by(auto split:if_split_asm)
  hence "xs' = Map.empty" by auto
  moreover from wwf red have "fv e' ⊆ fv e" by(rule red_fv_subset)
  with ‹fv e = {}› have "fv e' = {}" by blast
  ultimately have "τRed0t P t h (e', es) (e'', es)" by(rule step)
  moreover from red ‹τmove0 P h e› ‹xs' = Map.empty› ‹no_call P h e›
  have "τRed0 P t h (e, es) (e', es)" by(auto simp add: no_call_def intro!: red0Red)
  ultimately show ?case by(blast intro: tranclp_into_tranclp2)
qed

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

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

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

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

lemma Red_Suspend_is_call:
  "⟦ P,t ⊢0 ⟨e/exs, h⟩ -ta→ ⟨e'/exs', h'⟩; Suspend w ∈ set ⦃ta⦄⇘w⇙ ⟧ ⟹ is_call e'"
by(auto elim!: red0.cases dest: red_Suspend_is_call simp add: is_call_def)


lemma red0_mthr: "multithreaded final_expr0 (mred0 P)"
by(unfold_locales)(auto elim!: red0.cases dest: red_new_thread_heap)

lemma red0_τmthr_wf: "τmultithreaded_wf final_expr0 (mred0 P) (τMOVE0 P)"
proof -
  interpret multithreaded final_expr0 "mred0 P" by(rule red0_mthr)
  show ?thesis
  proof
    fix x1 m1 t ta1 x1' m1'
    assume "mred0 P t (x1, m1) ta1 (x1', m1')" "τMOVE0 P (x1, m1) ta1 (x1', m1')"
    thus "m1 = m1'" by(cases x1)(fastforce elim!: red0.cases dest: τmove0_heap_unchanged)
  qed(simp add: split_beta)
qed

lemma red_τmthr_wf: "τmultithreaded_wf final_expr (mred P) (τMOVE P)"
proof
  fix x1 m1 t ta1 x1' m1'
  assume "mred P t (x1, m1) ta1 (x1', m1')" "τMOVE P (x1, m1) ta1 (x1', m1')"
  thus "m1 = m1'" by(auto dest: τmove0_heap_unchanged simp add: split_def)
qed(simp add: split_beta)

end

sublocale J_heap_base < red_mthr: 
  τmultithreaded_wf 
    final_expr
    "mred P"
    convert_RA
    "τMOVE P"
  for P
by(rule red_τmthr_wf)

sublocale J_heap_base < red0_mthr:
  τmultithreaded_wf 
    final_expr0
    "mred0 P"
    convert_RA
    "τMOVE0 P"
  for P
by(rule red0_τmthr_wf)

context J_heap_base begin

lemma τRed0r_into_red0_τmthr_silent_moves:
  "τRed0r P t h (e, es) (e'', es'') ⟹ red0_mthr.silent_moves P t ((e, es), h) ((e'', es''), h)"
apply(induct rule: rtranclp_induct2)
 apply blast
apply(erule rtranclp.rtrancl_into_rtrancl)
apply(simp add: red0_mthr.silent_move_iff)
done

lemma τRed0t_into_red0_τmthr_silent_movet:
  "τRed0t P t h (e, es) (e'', es'') ⟹ red0_mthr.silent_movet P t ((e, es), h) ((e'', es''), h)"
apply(induct rule: tranclp_induct2)
apply(fastforce simp add: red0_mthr.silent_move_iff elim: tranclp.trancl_into_trancl)+
done

end

end