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 tao = extTA2J0 P tao"
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:TsT = (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: TsT = (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: UsU = (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: UsU = (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 Te)  τ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 (ai)  τ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 (eF{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(DF, 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 (eM(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⇘hv = T  class_type_of' T = C  P  C sees M:TsTr = 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 Te)"
  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 (ee')"
  and τmove0AAcc2: "τmove0 P h e  τmove0 P h (Val ve)"
  and τmove0AAss1: "τmove0 P h e  τmove0 P h (ee1 := e2)"
  and τmove0AAss2: "τmove0 P h e  τmove0 P h (Val ve := e')"
  and τmove0AAss3: "τmove0 P h e  τmove0 P h (Val vVal v' := e)"
  and τmove0ALength: "τmove0 P h e  τmove0 P h (e∙length)"
  and τmove0FAcc: "τmove0 P h e  τmove0 P h (eF{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 vF{D} := e)"
  and τmove0CAS1: "τmove0 P h e  τmove0 P h (e∙compareAndSwap(DF, e', e''))"
  and τmove0CAS2: "τmove0 P h e'  τmove0 P h (Val v∙compareAndSwap(DF, e', e''))"
  and τmove0CAS3: "τmove0 P h e''  τmove0 P h (Val v∙compareAndSwap(DF, Val v', e''))"
  and τmove0CallObj: "τmove0 P h e  τmove0 P h (eM(es))"
  and τmove0CallParams: "τmoves0 P h es  τmove0 P h (Val vM(es))"
  and τmove0Call: "(T C Ts Tr D.  typeof⇘hv = T; class_type_of' T = C; P  C sees M:TsTr = Native in D   τexternal_defs D M)  τmove0 P h (Val vM(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 TThrow 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 ae)"
  and τmove0AAccThrow2: "τmove0 P h (Val vThrow 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 aF{D})"
  and τmove0FAssThrow1: "τmove0 P h (Throw aF{D} := e)"
  and τmove0FAssThrow2: "τmove0 P h (FAss (Val v) F D (Throw a))"
  and τmove0CallThrowObj: "τmove0 P h (Throw aM(es))"
  and τmove0CallThrowParams: "τmove0 P h (Val vM(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 Te) = 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 (ai) = (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 (eF{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(DF, 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 (eM(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 Te, xs) (newA Te', 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 (ai, 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 ai, xs) (Val ai', 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 (ai := 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 ai := e, xs) (Val ai' := 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 aVal i := e, xs) (Val aVal 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 (eF{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 (eF{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 vF{D} := e, xs) (Val vF{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(DF, e2, e3), xs) (e'∙compareAndSwap(DF, 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(DF, e, e3), xs) (Val v∙compareAndSwap(DF, 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(DF, Val v', e), xs) (Val v∙compareAndSwap(DF, 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 (eM(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 vM(es), xs) (Val vM(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 Te, xs) (newA Te', 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 (ai, 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 ai, xs) (Val ai', 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 (ai := 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 ai := e, xs) (Val ai' := 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 aVal i := e, xs) (Val aVal 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 (eF{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 (eF{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 vF{D} := e, xs) (Val vF{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(DF, e2, e3), xs) (e'∙compareAndSwap(DF, 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(DF, e, e3), xs) (Val v∙compareAndSwap(DF, 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(DF, Val v', e), xs) (Val v∙compareAndSwap(DF, 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 (eM(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 vM(es), xs) (Val vM(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 taw   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