Theory J0J1Bisim

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

    Reminiscent of the Jinja theory Compiler/Correctness1
*)

section ‹The bisimulation relation betwenn source and intermediate language›

theory J0J1Bisim imports
  J1
  J1WellForm
  Compiler1
  "../J/JWellForm"
  J0
begin

subsection‹Correctness of program compilation›

primrec unmod :: "'addr expr1 ⇒ nat ⇒ bool"
  and unmods :: "'addr expr1 list ⇒ nat ⇒ bool"
where
  "unmod (new C) i = True"
| "unmod (newA T⌊e⌉) i = unmod e i"
| "unmod (Cast C e) i = unmod e i"
| "unmod (e instanceof T) i = unmod e i"
| "unmod (Val v) i = True"
| "unmod (e1 «bop» e2) i = (unmod e1 i ∧ unmod e2 i)"
| "unmod (Var i) j = True"
| "unmod (i:=e) j = (i ≠ j ∧ unmod e j)"
| "unmod (a⌊i⌉) j = (unmod a j ∧ unmod i j)"
| "unmod (a⌊i⌉:=e) j = (unmod a j ∧ unmod i j ∧ unmod e j)"
| "unmod (a∙length) j = unmod a j"
| "unmod (e∙F{D}) i = unmod e i"
| "unmod (e1∙F{D}:=e2) i = (unmod e1 i ∧ unmod e2 i)"
| "unmod (e1∙compareAndSwap(D∙F, e2, e3)) i = (unmod e1 i ∧ unmod e2 i ∧ unmod e3 i)"
| "unmod (e∙M(es)) i = (unmod e i ∧ unmods es i)"
| "unmod {j:T=vo; e} i = ((i = j ⟶ vo = None) ∧ unmod e i)"
| "unmod (sync⇘V⇙ (o') e) i = (unmod o' i ∧ unmod e i ∧ i ≠ V)"
| "unmod (insync⇘V⇙ (a) e) i = unmod e i"
| "unmod (e1;;e2) i = (unmod e1 i ∧ unmod e2 i)"
| "unmod (if (e) e⇩1 else e⇩2) i = (unmod e i ∧ unmod e⇩1 i ∧ unmod e⇩2 i)"
| "unmod (while (e) c) i = (unmod e i ∧ unmod c i)"
| "unmod (throw e) i = unmod e i"
| "unmod (try e⇩1 catch(C i) e⇩2) j = (unmod e⇩1 j ∧ (if i=j then False else unmod e⇩2 j))"

| "unmods ([]) i = True"
| "unmods (e#es) i = (unmod e i ∧ unmods es i)"

lemma unmods_map_Val [simp]: "unmods (map Val vs) V"
by(induct vs) simp_all

lemma fixes e :: "'addr expr" and es :: "'addr expr list"
  shows hidden_unmod: "hidden Vs i ⟹ unmod (compE1 Vs e) i"
  and hidden_unmods: "hidden Vs i ⟹ unmods (compEs1 Vs es) i"
apply(induct Vs e and Vs es rule: compE1_compEs1_induct)
apply (simp_all add:hidden_inacc)
apply(auto simp add:hidden_def)
done

lemma unmod_extRet2J [simp]: "unmod e i ⟹ unmod (extRet2J e va) i"
by(cases va) simp_all

lemma max_dest: "(n :: nat) + max a b ≤ c ⟹ n + a ≤ c ∧ n + b ≤ c"
apply(auto simp add: max_def split: if_split_asm) 
done

declare max_dest [dest!]

lemma fixes e :: "'addr expr" and es :: "'addr expr list"
  shows fv_unmod_compE1: "⟦ i < length Vs; Vs ! i ∉ fv e ⟧ ⟹ unmod (compE1 Vs e) i"
  and fvs_unmods_compEs1: "⟦ i < length Vs; Vs ! i ∉ fvs es ⟧ ⟹ unmods (compEs1 Vs es) i"
proof(induct Vs e and Vs es rule: compE1_compEs1_induct)
  case (Block Vs V ty vo exp)
  note IH = ‹⟦i < length (Vs @ [V]); (Vs @ [V]) ! i ∉ fv exp ⟧ ⟹ unmod (compE1 (Vs @ [V]) exp) i›
  note len = ‹i < length Vs›
  hence i: "i < length (Vs @ [V])" by simp
  show ?case
  proof(cases "Vs ! i = V")
    case True
    from len have "hidden (Vs @ [Vs ! i]) i" by(rule hidden_snoc_nth)
    with len True show ?thesis by(auto intro: hidden_unmod)
  next
    case False
    with ‹Vs ! i ∉ fv {V:ty=vo; exp}› len have "(Vs @ [V]) ! i ∉ fv exp"
      by(auto simp add: nth_append)
    from IH[OF i this] len show ?thesis by(auto)
  qed
next
  case (TryCatch Vs e1 C V e2)
  note IH1 = ‹⟦i < length Vs; Vs ! i ∉ fv e1 ⟧ ⟹ unmod (compE1 Vs e1) i›
  note IH2 = ‹⟦i < length (Vs @ [V]); (Vs @ [V]) ! i ∉ fv e2 ⟧ ⟹ unmod (compE1 (Vs @ [V]) e2) i›
  note len = ‹i < length Vs›
  hence i: "i < length (Vs @ [V])" by simp
  have "unmod (compE1 (Vs @ [V]) e2) i"
  proof(cases "Vs ! i = V")
    case True
    from len have "hidden (Vs @ [Vs ! i]) i" by(rule hidden_snoc_nth)
    with len True show ?thesis by(auto intro: hidden_unmod)
  next
    case False
    with ‹Vs ! i ∉ fv (try e1 catch(C V) e2)› len have "(Vs @ [V]) ! i ∉ fv e2"
      by(auto simp add: nth_append)
    from IH2[OF i this] len show ?thesis by(auto)
  qed
  with IH1[OF len] ‹Vs ! i ∉ fv (try e1 catch(C V) e2)› len show ?case by(auto)
qed(auto dest: index_le_lengthD simp add: nth_append)

lemma hidden_lengthD: "hidden Vs i ⟹ i < length Vs"
by(simp add: hidden_def)

lemma fixes e :: "'addr expr1" and es :: "'addr expr1 list"
  shows fv_B_unmod: "⟦ V ∉ fv e; ℬ e n; V < n ⟧ ⟹ unmod e V"
  and fvs_Bs_unmods: "⟦ V ∉ fvs es; ℬs es n; V < n ⟧ ⟹ unmods es V"
by(induct e and es arbitrary: n and n rule: unmod.induct unmods.induct) auto

lemma assumes fin: "final e'"
  shows unmod_inline_call: "unmod (inline_call e' e) V ⟷ unmod e V"
  and unmods_inline_calls: "unmods (inline_calls e' es) V ⟷ unmods es V"
apply(induct e and es rule: unmod.induct unmods.induct)
apply(insert fin)
apply(auto simp add: is_vals_conv)
done

subsection ‹The delay bisimulation relation›

text ‹Delay bisimulation for expressions›

inductive bisim :: "vname list ⇒ 'addr expr ⇒ 'addr expr1 ⇒ 'addr val list ⇒ bool"
  and bisims :: "vname list ⇒ 'addr expr list ⇒ 'addr expr1 list ⇒ 'addr val list ⇒ bool"
where
  bisimNew: "bisim Vs (new C) (new C) xs"
| bisimNewArray: "bisim Vs e e' xs ⟹ bisim Vs (newA T⌊e⌉) (newA T⌊e'⌉) xs"
| bisimCast: "bisim Vs e e' xs ⟹ bisim Vs (Cast T e) (Cast T e') xs"
| bisimInstanceOf: "bisim Vs e e' xs ⟹ bisim Vs (e instanceof T) (e' instanceof T) xs"
| bisimVal: "bisim Vs (Val v) (Val v) xs"
| bisimBinOp1:
  "⟦ bisim Vs e e' xs; ¬ is_val e; ¬ contains_insync e'' ⟧ ⟹ bisim Vs (e «bop» e'') (e' «bop» compE1 Vs e'') xs"
| bisimBinOp2: "bisim Vs e e' xs ⟹ bisim Vs (Val v «bop» e) (Val v «bop» e') xs"
| bisimVar: "bisim Vs (Var V) (Var (index Vs V)) xs"
| bisimLAss: "bisim Vs e e' xs ⟹ bisim Vs (V:=e) (index Vs V:=e') xs"
| bisimAAcc1: "⟦ bisim Vs a a' xs; ¬ is_val a; ¬ contains_insync i ⟧ ⟹ bisim Vs (a⌊i⌉) (a'⌊compE1 Vs i⌉) xs"
| bisimAAcc2: "bisim Vs i i' xs ⟹ bisim Vs (Val v⌊i⌉) (Val v⌊i'⌉) xs"
| bisimAAss1:
  "⟦ bisim Vs a a' xs; ¬ is_val a; ¬ contains_insync i; ¬ contains_insync e ⟧
  ⟹ bisim Vs (a⌊i⌉:=e) (a'⌊compE1 Vs i⌉:=compE1 Vs e) xs"
| bisimAAss2: "⟦ bisim Vs i i' xs; ¬ is_val i; ¬ contains_insync e ⟧ ⟹ bisim Vs (Val v⌊i⌉:=e) (Val v⌊i'⌉:=compE1 Vs e) xs"
| bisimAAss3: "bisim Vs e e' xs ⟹ bisim Vs (Val v⌊Val i⌉ := e) (Val v⌊Val i⌉ := e') xs"
| bisimALength: "bisim Vs a a' xs ⟹ bisim Vs (a∙length) (a'∙length) xs"
| bisimFAcc: "bisim Vs e e' xs ⟹ bisim Vs (e∙F{D}) (e'∙F{D}) xs"
| bisimFAss1: "⟦ bisim Vs e e' xs; ¬ is_val e; ¬ contains_insync e'' ⟧ ⟹ bisim Vs (e∙F{D}:=e'') (e'∙F{D}:=compE1 Vs e'') xs"
| bisimFAss2: "bisim Vs e e' xs ⟹ bisim Vs (Val v∙F{D} := e) (Val v∙F{D} := e') xs"
| bisimCAS1: "⟦ bisim Vs e e' xs; ¬ is_val e; ¬ contains_insync e2; ¬ contains_insync e3 ⟧ 
  ⟹ bisim Vs (e∙compareAndSwap(D∙F, e2, e3)) (e'∙compareAndSwap(D∙F, compE1 Vs e2, compE1 Vs e3)) xs"
| bisimCAS2: "⟦ bisim Vs e e' xs; ¬ is_val e; ¬ contains_insync e3 ⟧ 
  ⟹ bisim Vs (Val v∙compareAndSwap(D∙F, e, e3)) (Val v∙compareAndSwap(D∙F, e', compE1 Vs e3)) xs"
| bisimCAS3: "bisim Vs e e' xs ⟹ bisim Vs (Val v∙compareAndSwap(D∙F, Val v', e)) (Val v∙compareAndSwap(D∙F, Val v', e')) xs"
| bisimCallObj: "⟦ bisim Vs e e' xs; ¬ is_val e; ¬ contains_insyncs es ⟧ ⟹ bisim Vs (e∙M(es)) (e'∙M(compEs1 Vs es)) xs"
| bisimCallParams: "bisims Vs es es' xs ⟹ bisim Vs (Val v∙M(es)) (Val v∙M(es')) xs"
| bisimBlockNone: "bisim (Vs@[V]) e e' xs ⟹ bisim Vs {V:T=None; e} {(length Vs):T=None; e'} xs"
| bisimBlockSome: "⟦ bisim (Vs@[V]) e e' (xs[length Vs := v]) ⟧ ⟹ bisim Vs {V:T=⌊v⌋; e} {(length Vs):T=⌊v⌋; e'} xs"
| bisimBlockSomeNone: "⟦ bisim (Vs@[V]) e e' xs; xs ! (length Vs) = v ⟧ ⟹ bisim Vs {V:T=⌊v⌋; e} {(length Vs):T=None; e'} xs"
| bisimSynchronized:
  "⟦ bisim Vs o' o'' xs; ¬ contains_insync e ⟧
  ⟹ bisim Vs (sync(o') e) (sync⇘length Vs⇙(o'') (compE1 (Vs@[fresh_var Vs]) e)) xs"
| bisimInSynchronized:
  "⟦ bisim (Vs@[fresh_var Vs]) e e' xs; xs ! length Vs = Addr a ⟧ ⟹ bisim Vs (insync(a) e) (insync⇘length Vs⇙(a) e') xs"
| bisimSeq: "⟦ bisim Vs e e' xs; ¬ contains_insync e'' ⟧ ⟹ bisim Vs (e;;e'') (e';;compE1 Vs e'') xs"
| bisimCond:
  "⟦ bisim Vs e e' xs; ¬ contains_insync e1; ¬ contains_insync e2 ⟧
  ⟹ bisim Vs (if (e) e1 else e2) (if (e') (compE1 Vs e1) else (compE1 Vs e2)) xs"
| bisimWhile:
  "⟦ ¬ contains_insync b; ¬ contains_insync e ⟧ ⟹ bisim Vs (while (b) e) (while (compE1 Vs b) (compE1 Vs e)) xs"
| bisimThrow: "bisim Vs e e' xs ⟹ bisim Vs (throw e) (throw e') xs"
| bisimTryCatch:
  "⟦ bisim Vs e e' xs; ¬ contains_insync e'' ⟧
  ⟹ bisim Vs (try e catch(C V) e'') (try e' catch(C (length Vs)) compE1 (Vs@[V]) e'') xs"

| bisimsNil: "bisims Vs [] [] xs"
| bisimsCons1: "⟦ bisim Vs e e' xs; ¬ is_val e; ¬ contains_insyncs es ⟧ ⟹ bisims Vs (e # es) (e' # compEs1 Vs es) xs"
| bisimsCons2: "bisims Vs es es' xs ⟹ bisims Vs (Val v # es) (Val v # es') xs"

declare bisimNew [iff]
declare bisimVal [iff]
declare bisimVar [iff]
declare bisimWhile [iff]
declare bisimsNil [iff]

declare bisim_bisims.intros [intro!]
declare bisimsCons1 [rule del, intro] bisimsCons2 [rule del, intro]
  bisimBinOp1 [rule del, intro] bisimAAcc1 [rule del, intro]
  bisimAAss1 [rule del, intro] bisimAAss2 [rule del, intro]
  bisimFAss1 [rule del, intro]
  bisimCAS1 [rule del, intro] bisimCAS2 [rule del, intro]
  bisimCallObj [rule del, intro] 

inductive_cases bisim_safe_cases [elim!]:
  "bisim Vs (new C) e' xs"
  "bisim Vs (newA T⌊e⌉) e' xs"
  "bisim Vs (Cast T e) e' xs"
  "bisim Vs (e instanceof T) e' xs"
  "bisim Vs (Val v) e' xs"
  "bisim Vs (Var V) e' xs"
  "bisim Vs (V:=e) e' xs"
  "bisim Vs (Val v⌊i⌉) e' xs"
  "bisim Vs (Val v⌊Val v'⌉ := e) e' xs"
  "bisim Vs (Val v∙compareAndSwap(D∙F, Val v', e)) e' xs"
  "bisim Vs (a∙length) e' xs"
  "bisim Vs (e∙F{D}) e' xs"
  "bisim Vs (sync(o') e) e' xs"
  "bisim Vs (insync(a) e) e' xs"
  "bisim Vs (e;;e') e'' xs"
  "bisim Vs (if (b) e1 else e2) e' xs"
  "bisim Vs (while (b) e) e' xs"
  "bisim Vs (throw e) e' xs"
  "bisim Vs (try e catch(C V) e') e'' xs"
  "bisim Vs e' (new C) xs"
  "bisim Vs e' (newA T⌊e⌉) xs"
  "bisim Vs e' (Cast T e) xs"
  "bisim Vs e' (e instanceof T) xs"
  "bisim Vs e' (Val v) xs"
  "bisim Vs e' (Var V) xs"
  "bisim Vs e' (V:=e) xs"
  "bisim Vs e' (Val v⌊i⌉) xs"
  "bisim Vs e' (Val v⌊Val v'⌉ := e) xs"
  "bisim Vs e' (Val v∙compareAndSwap(D∙F, Val v', e)) xs"
  "bisim Vs e' (a∙length) xs"
  "bisim Vs e' (e∙F{D}) xs"
  "bisim Vs e' (sync⇘V⇙ (o') e) xs"
  "bisim Vs e' (insync⇘V⇙ (a) e) xs"
  "bisim Vs e'' (e;;e') xs"
  "bisim Vs e' (if (b) e1 else e2) xs"
  "bisim Vs e' (while (b) e) xs"
  "bisim Vs e' (throw e) xs"
  "bisim Vs e'' (try e catch(C V) e') xs"

inductive_cases bisim_cases [elim]:
  "bisim Vs (e1 «bop» e2) e' xs"
  "bisim Vs (a⌊i⌉) e' xs"
  "bisim Vs (a⌊i⌉:=e) e' xs"
  "bisim Vs (e∙F{D}:=e') e'' xs"
  "bisim Vs (e∙compareAndSwap(D∙F, e', e'')) e''' xs"
  "bisim Vs (e∙M(es)) e' xs"
  "bisim Vs {V:T=vo; e} e' xs"
  "bisim Vs e' (e1 «bop» e2) xs"
  "bisim Vs e' (a⌊i⌉) xs"
  "bisim Vs e' (a⌊i⌉:=e) xs"
  "bisim Vs e'' (e∙F{D}:=e') xs"
  "bisim Vs e''' (e∙compareAndSwap(D∙F, e', e'')) xs"
  "bisim Vs e' (e∙M(es)) xs"
  "bisim Vs e' {V:T=vo; e} xs"

inductive_cases bisims_safe_cases [elim!]:
  "bisims Vs [] es xs"
  "bisims Vs es [] xs"

inductive_cases bisims_cases [elim]:
  "bisims Vs (e # es) es' xs"
  "bisims Vs es' (e # es) xs"

text ‹Delay bisimulation for call stacks›

inductive bisim01 :: "'addr expr ⇒ 'addr expr1 × 'addr locals1 ⇒ bool"
where
  "⟦ bisim [] e e' xs; fv e = {}; 𝒟 e ⌊{}⌋; max_vars e' ≤ length xs; call e = ⌊aMvs⌋; call1 e' = ⌊aMvs⌋ ⟧
  ⟹ bisim01 e (e', xs)"

inductive bisim_list :: "'addr expr list ⇒ ('addr expr1 × 'addr locals1) list ⇒ bool"
where
  bisim_listNil: "bisim_list [] []"
| bisim_listCons: 
  "⟦ bisim_list es exs'; bisim [] e e' xs; 
     fv e = {}; 𝒟 e ⌊{}⌋;
     max_vars e' ≤ length xs;
     call e = ⌊aMvs⌋; call1 e' = ⌊aMvs⌋ ⟧
  ⟹ bisim_list (e # es) ((e', xs) # exs')"

inductive_cases bisim_list_cases [elim!]:
 "bisim_list [] exs'"
 "bisim_list (ex # exs) exs'"
 "bisim_list exs (ex' # exs')"

fun bisim_list1 :: 
  "'addr expr × 'addr expr list ⇒ ('addr expr1 × 'addr locals1) × ('addr expr1 × 'addr locals1) list ⇒ bool"
where
  "bisim_list1 (e, es) ((e1, xs1), exs1) ⟷ 
   bisim_list es exs1 ∧ bisim [] e e1 xs1 ∧ fv e = {} ∧ 𝒟 e ⌊{}⌋ ∧ max_vars e1 ≤ length xs1"

definition bisim_red0_Red1 :: 
  "(('addr expr × 'addr expr list) × 'heap)
  ⇒ ((('addr expr1 × 'addr locals1) × ('addr expr1 × 'addr locals1) list) × 'heap) ⇒ bool"
where "bisim_red0_Red1 ≡ (λ(es, h) (exs, h'). bisim_list1 es exs ∧ h = h')"

abbreviation ta_bisim01 ::
  "('addr, 'thread_id, 'heap) J0_thread_action ⇒ ('addr, 'thread_id, 'heap) J1_thread_action ⇒ bool" 
where
  "ta_bisim01 ≡ ta_bisim (λt. bisim_red0_Red1)"

definition bisim_wait01 ::
  "('addr expr × 'addr expr list) ⇒ ('addr expr1 × 'addr locals1) × ('addr expr1 × 'addr locals1) list ⇒ bool"
where "bisim_wait01 ≡ λ(e0, es0) ((e1, xs1), exs1). call e0 ≠ None ∧ call1 e1 ≠ None"

lemma bisim_list1I[intro?]:
  "⟦ bisim_list es exs1; bisim [] e e1 xs1; fv e = {};
     𝒟 e ⌊{}⌋; max_vars e1 ≤ length xs1 ⟧
  ⟹ bisim_list1 (e, es) ((e1, xs1), exs1)"
by simp

lemma bisim_list1E[elim?]:
  assumes "bisim_list1 (e, es) ((e1, xs1), exs1)"
  obtains "bisim_list es exs1" "bisim [] e e1 xs1" "fv e = {}" "𝒟 e ⌊{}⌋" "max_vars e1 ≤ length xs1"
using assms by auto

lemma bisim_list1_elim:
  assumes "bisim_list1 es' exs"
  obtains e es e1 xs1 exs1
  where "es' = (e, es)" "exs = ((e1, xs1), exs1)"
  and "bisim_list es exs1" "bisim [] e e1 xs1" "fv e = {}" "𝒟 e ⌊{}⌋" "max_vars e1 ≤ length xs1"
using assms by(cases es')(cases exs, fastforce)

declare bisim_list1.simps [simp del]


lemma bisims_map_Val_conv [simp]: "bisims Vs (map Val vs) es xs = (es = map Val vs)"
apply(induct vs arbitrary: es)
 apply(fastforce)
apply(simp)
apply(rule iffI)
apply(erule bisims_cases, auto)
done

declare compEs1_conv_map [simp del]

lemma bisim_contains_insync: "bisim Vs e e' xs ⟹ contains_insync e = contains_insync e'"
  and bisims_contains_insyncs: "bisims Vs es es' xs ⟹ contains_insyncs es = contains_insyncs es'"
by(induct rule: bisim_bisims.inducts)(auto)

lemma bisims_map_Val_Throw: 
  "bisims Vs (map Val vs @ Throw a # es) es' xs ⟷ es' = map Val vs @ Throw a # compEs1 Vs es ∧ ¬ contains_insyncs es"
apply(induct vs arbitrary: es')
 apply(simp)
 apply(fastforce simp add: compEs1_conv_map)
apply(fastforce elim!: bisims_cases intro: bisimsCons2)
done

lemma compE1_bisim [intro]: "⟦ fv e ⊆ set Vs; ¬ contains_insync e ⟧ ⟹ bisim Vs e (compE1 Vs e) xs"
  and compEs1_bisims [intro]: "⟦ fvs es ⊆ set Vs; ¬ contains_insyncs es ⟧ ⟹ bisims Vs es (compEs1 Vs es) xs"
proof(induct Vs e and Vs es arbitrary: xs and xs rule: compE1_compEs1_induct)
  case (BinOp Vs exp1 bop exp2 x)
  thus ?case by(cases "is_val exp1")(auto)
next
  case (AAcc Vs exp1 exp2 x)
  thus ?case by(cases "is_val exp1")(auto)
next
  case (AAss Vs exp1 exp2 exp3 x)
  thus ?case by(cases "is_val exp1", cases "is_val exp2", fastforce+)
next
  case (FAss Vs exp1 F D exp2 x)
  thus ?case by(cases "is_val exp1", auto)
next
  case (CAS Vs e1 D F e2 e3 x)
  thus ?case by(cases "is_val e1", cases "is_val e2", fastforce+)
next
  case (Call Vs obj M params x)
  thus ?case by(cases "is_val obj")(auto)
next
  case (Block Vs V T vo exp xs)
  from ‹fv {V:T=vo; exp} ⊆ set Vs› have "fv exp ⊆ set (Vs@[V])" by(auto)
  with Block show ?case by(cases vo)(auto)
next
  case (Cons Vs exp list x)
  thus ?case by(cases "is_val exp")(auto intro!: bisimsCons2)
qed(auto)

lemma bisim_hidden_unmod: "⟦ bisim Vs e e' xs; hidden Vs i ⟧ ⟹ unmod e' i"
  and bisims_hidden_unmods: "⟦ bisims Vs es es' xs; hidden Vs i ⟧ ⟹ unmods es' i"
by(induct rule: bisim_bisims.inducts)(auto intro: hidden_unmod hidden_unmods dest: hidden_inacc hidden_lengthD)

lemma bisim_fv_unmod: "⟦ bisim Vs e e' xs; i < length Vs; Vs ! i ∉ fv e ⟧ ⟹ unmod e' i"
  and bisims_fvs_unmods: "⟦ bisims Vs es es' xs; i < length Vs; Vs ! i ∉ fvs es ⟧ ⟹ unmods es' i"
proof(induct rule: bisim_bisims.inducts)
  case (bisimBlockNone Vs V e e' xs T)
  note len = ‹i < length Vs›
  have "unmod e' i"
  proof(cases "Vs ! i = V")
    case True
    from len have "hidden (Vs @ [Vs ! i]) i" by(rule hidden_snoc_nth)
    with len True ‹bisim (Vs @ [V]) e e' xs› show ?thesis by(auto intro: bisim_hidden_unmod)
  next
    case False
    with bisimBlockNone show ?thesis by(auto simp add: nth_append)
  qed
  thus ?case by simp
next
  case (bisimBlockSome Vs V e e' xs v T)
  note len = ‹i < length Vs›
  show ?case
  proof(cases "Vs ! i = V")
    case True
    from len have "hidden (Vs @ [Vs ! i]) i" by(rule hidden_snoc_nth)
    with len True ‹bisim (Vs @ [V]) e e' (xs[length Vs := v])›
    show ?thesis by(auto intro: bisim_hidden_unmod)
  next
    case False
    with bisimBlockSome show ?thesis by(auto simp add: nth_append)
  qed
next
  case (bisimBlockSomeNone Vs V e e' xs v T)
  note len = ‹i < length Vs›
  show ?case
  proof(cases "Vs ! i = V")
    case True
    from len have "hidden (Vs @ [Vs ! i]) i" by(rule hidden_snoc_nth)
    with len True ‹bisim (Vs @ [V]) e e' xs›
    show ?thesis by(auto intro: bisim_hidden_unmod)
  next
    case False
    with bisimBlockSomeNone show ?thesis by(auto simp add: nth_append)
  qed
qed(fastforce dest: fv_unmod_compE1 fvs_unmods_compEs1 index_le_lengthD simp add: nth_append)+

lemma bisim_extRet2J [intro!]: "bisim Vs e e' xs ⟹ bisim Vs (extRet2J e va) (extRet2J1 e' va) xs"
by(cases va) auto

lemma bisims_map_Val_conv2 [simp]: "bisims Vs es (map Val vs) xs = (es = map Val vs)"
apply(induct vs arbitrary: es)
apply(fastforce elim!: bisims_cases)+
done

lemma bisims_map_Val_Throw2: 
  "bisims Vs es' (map Val vs @ Throw a # es) xs ⟷
   (∃es''. es' = map Val vs @ Throw a # es'' ∧ es = compEs1 Vs es'' ∧ ¬ contains_insyncs es'')"
apply(induct vs arbitrary: es')
 apply(simp)
 apply(fastforce simp add: compEs1_conv_map)
apply(fastforce elim!: bisims_cases)
done

lemma hidden_bisim_unmod: "⟦ bisim Vs e e' xs; hidden Vs i ⟧ ⟹ unmod e' i"
  and hidden_bisims_unmods: "⟦ bisims Vs es es' xs; hidden Vs i ⟧ ⟹ unmods es' i"
apply(induct rule: bisim_bisims.inducts)
apply(auto simp add:hidden_inacc intro: hidden_unmod hidden_unmods)
apply(auto simp add: hidden_def)
done

lemma bisim_list_list_all2_conv:
  "bisim_list es exs' ⟷ list_all2 bisim01 es exs'"
proof
  assume "bisim_list es exs'"
  thus "list_all2 bisim01 es exs'"
    by induct(auto intro!: bisim01.intros)
next
  assume "list_all2 bisim01 es exs'"
  thus "bisim_list es exs'"
    by(induct es arbitrary: exs')(auto intro!: bisim_listCons bisim_listNil elim!: bisim01.cases simp add: list_all2_Cons1)
qed

lemma bisim_list_extTA2J0_extTA2J1:
  assumes wf: "wf_J_prog P"
  and sees: "P ⊢ C sees M:[]→T = ⌊meth⌋ in D"
  shows "bisim_list1 (extNTA2J0 P (C, M, a)) (extNTA2J1 (compP1 P) (C, M, a))"
proof -
  obtain pns body where "meth = (pns, body)" by(cases meth)
  with sees have sees: "P ⊢ C sees M:[]→T = ⌊(pns, body)⌋ in D" by simp
  moreover let ?xs = "Addr a # replicate (max_vars body) undefined_value"
  let ?e' = "{0:Class D=None; compE1 (this # pns) body}"
  have "bisim_list1 ({this:Class D=⌊Addr a⌋; body}, []) ((?e', ?xs), [])"
  proof
    show "bisim_list [] []" ..
    from sees_wf_mdecl[OF wf_prog_wwf_prog[OF wf] sees] have "fv body ⊆ set [this]" "pns = []"
      by(auto simp add: wf_mdecl_def)
    thus "fv ({this:Class D=⌊Addr a⌋; body}) = {}" by simp
    from sees_wf_mdecl[OF wf sees] obtain T' where "P,[this ↦ Class D] ⊢ body :: T'" "this ∉ set pns"
      and "𝒟 body ⌊dom [this ↦ Addr a]⌋" by(auto simp add: wf_mdecl_def)
    hence "¬ contains_insync body" by(auto simp add: contains_insync_conv dest: WT_expr_locks)
    with ‹fv body ⊆ set [this]›
    have "bisim ([] @ [this]) body (compE1 (this # pns) body) ?xs"
      unfolding append.simps ‹pns = []› by(rule compE1_bisim)
    hence "bisim [] {this:Class D=⌊Addr a⌋; body} {length ([] :: String.literal list):Class D=None; compE1 (this # pns) body} ?xs"
      by(rule bisimBlockSomeNone)(simp)
    thus "bisim [] ({this:Class D=⌊Addr a⌋; body}) ?e' ?xs" by simp
    from ‹𝒟 body ⌊dom [this ↦ Addr a]⌋› show "𝒟 ({this:Class D=⌊Addr a⌋; body}) ⌊{}⌋" by simp
    show "max_vars ?e' ≤ length ?xs" by simp
  qed
  ultimately show ?thesis by(simp)
qed


lemma bisim_max_vars: "bisim Vs e e' xs ⟹ max_vars e = max_vars e'"
  and bisims_max_varss: "bisims Vs es es' xs ⟹ max_varss es = max_varss es'"
apply(induct rule: bisim_bisims.inducts)
apply(auto simp add: max_vars_compE1 max_varss_compEs1)
done

lemma bisim_call: "bisim Vs e e' xs ⟹ call e = call e'"
  and bisims_calls: "bisims Vs es es' xs ⟹ calls es = calls es'"
apply(induct rule: bisim_bisims.inducts)
apply(auto simp add: is_vals_conv)
done

lemma bisim_call_None_call1: "⟦ bisim Vs e e' xs; call e = None ⟧ ⟹ call1 e' = None"
  and bisims_calls_None_calls1: "⟦ bisims Vs es es' xs; calls es = None ⟧ ⟹ calls1 es' = None"
by(induct rule: bisim_bisims.inducts)(auto simp add: is_vals_conv split: if_split_asm)

lemma bisim_call1_Some_call:
  "⟦ bisim Vs e e' xs; call1 e' = ⌊aMvs⌋ ⟧ ⟹ call e = ⌊aMvs⌋"

  and bisims_calls1_Some_calls:
  "⟦ bisims Vs es es' xs; calls1 es' = ⌊aMvs⌋ ⟧ ⟹ calls es = ⌊aMvs⌋"
by(induct rule: bisim_bisims.inducts)(auto simp add: is_vals_conv split: if_split_asm)

lemma blocks_bisim: 
  assumes bisim: "bisim (Vs @ pns) e e' xs"
  and length: "length vs = length pns" "length Ts = length pns"
  and xs: "∀i. i < length vs ⟶ xs ! (i + length Vs) = vs ! i"
  shows "bisim Vs (blocks pns Ts vs e) (blocks1 (length Vs) Ts e') xs"
using bisim length xs
proof(induct pns Ts vs e arbitrary: e' Vs rule: blocks.induct)
  case (1 V Vs T Ts v vs e e' VS)
  note IH = ‹⋀e' Vsa. ⟦bisim (Vsa @ Vs) e e' xs;
                       length vs = length Vs; length Ts = length Vs; ∀i<length vs. xs ! (i + length Vsa) = vs ! i⟧
           ⟹ bisim Vsa (blocks Vs Ts vs e) (blocks1 (length Vsa) Ts e') xs›
  note xs = ‹∀i<length (v # vs). xs ! (i + length VS) = (v # vs) ! i›
  hence xs': "∀i<length vs. xs ! (i + length (VS @ [V])) = vs ! i" and v: "xs ! length VS = v" by(auto)
  from ‹bisim (VS @ V # Vs) e e' xs› have "bisim ((VS @ [V]) @ Vs) e e' xs" by simp
  from IH[OF this _ _ xs'] ‹length (v # vs) = length (V # Vs)› ‹length (T # Ts) = length (V # Vs)›
  have "bisim (VS @ [V]) (blocks Vs Ts vs e) (blocks1 (length (VS @ [V])) Ts e') xs"
    by auto
  hence "bisim VS ({V:T=⌊v⌋; blocks Vs Ts vs e}) {length VS:T=None; blocks1 (length (VS @ [V])) Ts e'} xs"
    using v by(rule bisimBlockSomeNone)
  thus ?case by simp
qed(auto)

lemma fixes e :: "('a,'b,'addr) exp" and es :: "('a,'b,'addr) exp list"
  shows inline_call_max_vars: "call e = ⌊aMvs⌋ ⟹ max_vars (inline_call e' e) ≤ max_vars e + max_vars e'"
  and inline_calls_max_varss: "calls es = ⌊aMvs⌋ ⟹ max_varss (inline_calls e' es) ≤ max_varss es + max_vars e'"
by(induct e and es rule: call.induct calls.induct)(auto)

lemma assumes "final E" "bisim VS E E' xs"
  shows inline_call_compE1: "call e = ⌊aMvs⌋ ⟹ inline_call E' (compE1 Vs e) = compE1 Vs (inline_call E e)"
  and inline_calls_compEs1: "calls es = ⌊aMvs⌋ ⟹ inline_calls E' (compEs1 Vs es) = compEs1 Vs (inline_calls E es)"
proof(induct Vs e and Vs es rule: compE1_compEs1_induct)
  case (Call Vs obj M params)
  note IHobj = ‹call obj = ⌊aMvs⌋ ⟹ inline_call E' (compE1 Vs obj) = compE1 Vs (inline_call E obj)›
  note IHparams = ‹calls params = ⌊aMvs⌋ ⟹ inline_calls E' (compEs1 Vs params) = compEs1 Vs (inline_calls E params)›
  obtain a M' vs where [simp]: "aMvs = (a, M', vs)" by (cases aMvs, auto)
  with ‹call (obj∙M(params)) = ⌊aMvs⌋› have "call (obj∙M(params)) = ⌊(a, M', vs)⌋" by simp
  thus ?case
  proof(induct rule: call_callE)
    case CallObj
    with IHobj have "inline_call E' (compE1 Vs obj) = compE1 Vs (inline_call E obj)" by auto
    with CallObj show ?case by auto
  next
    case (CallParams v)
    with IHparams have "inline_calls E' (compEs1 Vs params) = compEs1 Vs (inline_calls E params)" by auto
    with CallParams show ?case by(auto simp add: is_vals_conv)
  next
    case Call
    with ‹final E› ‹bisim VS E E' xs› show ?case by(auto simp add: is_vals_conv)
  qed
qed(auto split: if_split_asm)

lemma assumes bisim: "bisim VS E E' XS"
  and final: "final E"
  shows bisim_inline_call:
  "⟦ bisim Vs e e' xs; call e = ⌊aMvs⌋; fv e ⊆ set Vs ⟧
  ⟹ bisim Vs (inline_call E e) (inline_call E' e') xs"
  
  and bisims_inline_calls: 
  "⟦ bisims Vs es es' xs; calls es = ⌊aMvs⌋; fvs es ⊆ set Vs ⟧
  ⟹ bisims Vs (inline_calls E es) (inline_calls E' es') xs"
proof(induct rule: bisim_bisims.inducts)
  case (bisimBinOp1 Vs e e' xs bop e'')
  thus ?case by(cases "is_val (inline_call E e)")(fastforce)+
next
  case (bisimAAcc1 Vs a a' xs i)
  thus ?case by(cases "is_val (inline_call E a)")(fastforce)+
next
  case (bisimAAss1 Vs a a' xs i e)
  thus ?case by(cases "is_val (inline_call E a)", cases "is_val i")(fastforce)+
next
  case (bisimAAss2 Vs i i' xs a e)
  thus ?case by(cases "is_val (inline_call E i)")(fastforce)+
next
  case (bisimFAss1 Vs e e' xs F D e'')
  thus ?case by(cases "is_val (inline_call E e)")(fastforce)+
next
  case (bisimCAS1 Vs e e' xs e2 e3 D F)
  thus ?case 
    apply(cases "is_val (inline_call E e)")
     apply(cases "is_val e2")
      apply(fastforce)
     apply clarsimp
     apply(safe; clarsimp?)
     apply auto
    done
next
  case (bisimCAS2 Vs e e' xs e3 v D F)
  thus ?case by(cases "is_val (inline_call E e)"; safe?; clarsimp; fastforce)
next
  case (bisimCallObj Vs e e' xs es M)
  obtain a M' vs where "aMvs = (a, M', vs)" by(cases aMvs, auto)
  with ‹call (e∙M(es)) = ⌊aMvs⌋› have "call (e∙M(es)) = ⌊(a, M', vs)⌋"  by simp
  thus ?case
  proof(induct rule: call_callE)
    case CallObj
    with ‹fv (e∙M(es)) ⊆ set Vs› ‹aMvs = (a, M', vs)›
      ‹⟦call e = ⌊aMvs⌋; fv e ⊆ set Vs⟧ ⟹ bisim Vs (inline_call E e) (inline_call E' e') xs›
    have IH': "bisim Vs (inline_call E e) (inline_call E' e') xs" by(auto)
    with ‹bisim Vs e e' xs› ‹fv (e∙M(es)) ⊆ set Vs› CallObj ‹¬ contains_insyncs es› show ?thesis
      by(cases "is_val (inline_call E e)")(fastforce)+
  next
    case (CallParams v)
    hence "inline_calls E' (compEs1 Vs es) = compEs1 Vs (inline_calls E es)"
      by -(rule inline_calls_compEs1[OF final bisim])
    moreover from ‹fv (e∙M(es)) ⊆ set Vs› final fvs_inline_calls[of E es]
    have "fvs (inline_calls E es) ⊆ set Vs" by(auto elim!: final.cases)
    moreover note CallParams ‹bisim Vs e e' xs› ‹fv (e∙M(es)) ⊆ set Vs› ‹¬ contains_insyncs es› final
    ultimately show ?case by(auto simp add: is_vals_conv final_iff)
  next
    case Call
    with final bisim ‹bisim Vs e e' xs› show ?case by(auto simp add: is_vals_conv)
  qed
next
  case (bisimCallParams Vs es es' xs v M)
  obtain a M' vs where [simp]: "aMvs = (a, M', vs)" by(cases aMvs, auto)
  with ‹call (Val v∙M(es)) = ⌊aMvs⌋› have "call (Val v∙M(es)) = ⌊(a, M', vs)⌋"  by simp
  thus ?case
  proof(induct rule: call_callE)
    case CallObj thus ?case by simp
  next
    case (CallParams v')
    with ‹ ⟦calls es = ⌊aMvs⌋; fvs es ⊆ set Vs⟧ ⟹ bisims Vs (inline_calls E es) (inline_calls E' es') xs› ‹fv (Val v∙M(es)) ⊆ set Vs›
    have "bisims Vs (inline_calls E es) (inline_calls E' es') xs" by(auto)
    with final bisim ‹bisims Vs es es' xs› show ?case by(auto simp add: is_vals_conv)
  next
    case Call
    with final bisim ‹bisims Vs es es' xs› show ?case by(auto)
  qed
next
  case (bisimsCons1 Vs e e' xs es)
  thus ?case by(cases "is_val (inline_call E e)")(fastforce)+
qed(fastforce)+

declare hyperUn_ac [simp del]

lemma sqInt_lem3: "⟦ A ⊑ A'; B ⊑ B' ⟧ ⟹ A ⊓ B ⊑ A' ⊓ B'"
by(auto simp add: hyperset_defs)

lemma sqUn_lem3: "⟦ A ⊑ A'; B ⊑ B' ⟧ ⟹ A ⊔ B ⊑ A' ⊔ B'"
by(auto simp add: hyperset_defs)

lemma A_inline_call: "call e = ⌊aMvs⌋ ⟹ 𝒜 e ⊑ 𝒜 (inline_call e' e)"
  and As_inline_calls: "calls es = ⌊aMvs⌋ ⟹  𝒜s es ⊑ 𝒜s (inline_calls e' es)"
proof(induct e and es rule: call.induct calls.induct)
  case (Call obj M params)
  obtain a M' vs where [simp]: "aMvs = (a, M', vs)" by(cases aMvs, auto)
  with ‹call (obj∙M(params)) = ⌊aMvs⌋› have "call (obj∙M(params)) = ⌊(a, M', vs)⌋"  by simp
  thus ?case
  proof(induct rule: call_callE)
    case CallObj
    with ‹call obj = ⌊aMvs⌋ ⟹ 𝒜 obj ⊑ 𝒜 (inline_call e' obj)›
    show ?case by(auto intro: sqUn_lem)
  next
    case CallParams
    with ‹calls params = ⌊aMvs⌋ ⟹ 𝒜s params ⊑ 𝒜s (inline_calls e' params)›
    show ?case by(auto intro: sqUn_lem)
  next
    case Call
    thus ?case by(auto simp add: hyperset_defs)
  qed
next
  case Block thus ?case by(fastforce intro: diff_lem)
next
  case throw thus ?case by(simp add: hyperset_defs)
next
  case TryCatch thus ?case by(auto intro: sqInt_lem)
qed(fastforce intro: sqUn_lem sqUn_lem2)+

lemma assumes "final e'"
  shows defass_inline_call: "⟦ call e = ⌊aMvs⌋; 𝒟 e A ⟧ ⟹ 𝒟 (inline_call e' e) A"
  and defasss_inline_calls: "⟦ calls es = ⌊aMvs⌋; 𝒟s es A ⟧ ⟹ 𝒟s (inline_calls e' es) A"
proof(induct e and es arbitrary: A and A rule: call.induct calls.induct)
  case (Call obj M params A)
  obtain a M' vs where [simp]: "aMvs = (a, M', vs)" by(cases aMvs, auto)
  with ‹call (obj∙M(params)) = ⌊aMvs⌋› have "call (obj∙M(params)) = ⌊(a, M', vs)⌋"  by simp
  thus ?case
  proof(cases rule: call_callE)
    case CallObj
    with ‹𝒟 (obj∙M(params)) A› ‹⟦call obj = ⌊aMvs⌋; 𝒟 obj A⟧ ⟹ 𝒟 (inline_call e' obj) A›
    have "𝒟 (inline_call e' obj) A" by simp
    moreover from A_inline_call[OF CallObj, of e']
    have "A ⊔ (𝒜 obj) ⊑ A ⊔ (𝒜 (inline_call e' obj))" by(rule sqUn_lem2)
    with ‹𝒟 (obj∙M(params)) A› have "𝒟s params (A ⊔ 𝒜 (inline_call e' obj))" by(auto elim: Ds_mono')
    ultimately show ?thesis using CallObj by auto
  next
    case (CallParams v)
    with ‹𝒟 (obj∙M(params)) A› ‹⟦calls params = ⌊aMvs⌋; 𝒟s params A⟧ ⟹ 𝒟s (inline_calls e' params) A›
    have "𝒟s (inline_calls e' params) A" by(simp)
    with CallParams show ?thesis by(auto)
  next
    case Call
    with ‹final e'› show ?thesis by(auto elim!: D_mono' simp add: hyperset_defs)
  qed
next
  case (Cons_exp exp exps A)
  show ?case
  proof(cases "is_val exp")
    case True
    with ‹𝒟s (exp # exps) A› ‹⟦calls exps = ⌊aMvs⌋; 𝒟s exps A⟧ ⟹ 𝒟s (inline_calls e' exps) A› 
      ‹calls (exp # exps) = ⌊aMvs⌋›
    have "𝒟s (inline_calls e' exps) A" by(auto)
    with True show ?thesis by(auto)
  next
    case False
    with ‹⟦call exp = ⌊aMvs⌋; 𝒟 exp A⟧ ⟹ 𝒟 (inline_call e' exp) A› ‹calls (exp # exps) = ⌊aMvs⌋› ‹𝒟s (exp # exps) A›
    have "𝒟 (inline_call e' exp) A" by auto
    moreover from False ‹calls (exp # exps) = ⌊aMvs⌋› have "𝒜 exp ⊑ 𝒜 (inline_call e' exp)"
      by(auto intro: A_inline_call)
    hence "A ⊔ 𝒜 exp ⊑ A ⊔ 𝒜 (inline_call e' exp)" by(rule sqUn_lem2)
    with ‹𝒟s (exp # exps) A› have "𝒟s exps (A ⊔ 𝒜 (inline_call e' exp))"
      by(auto intro: Ds_mono')
    ultimately show ?thesis using False by(auto)
  qed
qed(fastforce split: if_split_asm elim: D_mono' intro: sqUn_lem2 sqUn_lem A_inline_call)+

lemma bisim_B: "bisim Vs e E xs ⟹ ℬ E (length Vs)"
  and bisims_Bs: "bisims Vs es Es xs ⟹ ℬs Es (length Vs)"
apply(induct rule: bisim_bisims.inducts)
apply(auto intro: ℬ ℬs)
done

lemma bisim_expr_locks_eq: "bisim Vs e e' xs ⟹ expr_locks e = expr_locks e'"
  and bisims_expr_lockss_eq: "bisims Vs es es' xs ⟹ expr_lockss es = expr_lockss es'"
by(induct rule: bisim_bisims.inducts)(auto intro!: ext)

lemma bisim_list_expr_lockss_eq: "bisim_list es exs' ⟹ expr_lockss es = expr_lockss (map fst exs')"
apply(induct rule: bisim_list.induct)
apply(auto dest: bisim_expr_locks_eq)
done

context J1_heap_base begin

lemma [simp]:
  fixes e :: "('a, 'b, 'addr) exp" and es :: "('a, 'b, 'addr) exp list"
  shows τmove1_compP: "τmove1 (compP f P) h e = τmove1 P h e"
  and τmoves1_compP: "τmoves1 (compP f P) h es = τmoves1 P h es"
by(induct e and es rule: τmove1.induct τmoves1.induct) auto

lemma τMove1_compP [simp]: "τMove1 (compP f P) = τMove1 P"
by(intro ext) auto

lemma red1_preserves_unmod:
  "⟦ uf,P,t ⊢1 ⟨e, s⟩ -ta→ ⟨e', s'⟩; unmod e i ⟧ ⟹ (lcl s') ! i = (lcl s) ! i"
  
  and reds1_preserves_unmod:
  "⟦ uf,P,t ⊢1 ⟨es, s⟩ [-ta→] ⟨es', s'⟩; unmods es i ⟧ ⟹ (lcl s') ! i = (lcl s) ! i"
apply(induct rule: red1_reds1.inducts)
apply(auto split: if_split_asm)
done

lemma red1_unmod_preserved:
  "⟦ uf,P,t ⊢1 ⟨e, s⟩ -ta→ ⟨e', s'⟩; unmod e i ⟧ ⟹ unmod e' i"
  and reds1_unmods_preserved:
  "⟦ uf,P,t ⊢1 ⟨es, s⟩ [-ta→] ⟨es', s'⟩; unmods es i ⟧ ⟹ unmods es' i"
by(induct rule: red1_reds1.inducts)(auto split: if_split_asm)

lemma τred1t_unmod_preserved:
  "⟦ τred1gt uf P t h (e, xs) (e', xs'); unmod e i ⟧ ⟹ unmod e' i"
by(induct rule: tranclp_induct2)(auto intro: red1_unmod_preserved)

lemma τred1r_unmod_preserved:
  "⟦ τred1gr uf P t h (e, xs) (e', xs'); unmod e i ⟧ ⟹ unmod e' i"
by(induct rule: rtranclp_induct2)(auto intro: red1_unmod_preserved)

lemma τred1t_preserves_unmod: 
  "⟦τred1gt uf P t h (e, xs) (e', xs'); unmod e i; i < length xs ⟧
  ⟹ xs' ! i = xs ! i"
apply(induct rule: tranclp_induct2)
 apply(auto dest: red1_preserves_unmod)
apply(drule red1_preserves_unmod)
apply(erule (1) τred1t_unmod_preserved)
apply(drule τred1t_preserves_len)
apply auto
done

lemma τred1'r_preserves_unmod: 
  "⟦τred1gr uf P t h (e, xs) (e', xs'); unmod e i; i < length xs ⟧
  ⟹ xs' ! i = xs ! i"
apply(induct rule: converse_rtranclp_induct2)
 apply(auto dest: red1_preserves_unmod red1_unmod_preserved red1_preserves_len)
apply(frule (1) red1_unmod_preserved)
apply(frule red1_preserves_len)
apply(frule (1) red1_preserves_unmod)
apply auto
done

end

context J_heap_base begin

lemma [simp]:
  fixes e :: "('a, 'b, 'addr) exp" and es :: "('a, 'b, 'addr) exp list"
  shows τmove0_compP: "τmove0 (compP f P) h e = τmove0 P h e"
  and τmoves0_compP: "τmoves0 (compP f P) h es = τmoves0 P h es"
by(induct e and es rule: τmove0.induct τmoves0.induct) auto

lemma τMove0_compP [simp]: "τMove0 (compP f P) = τMove0 P"
by(intro ext) auto

end

end