# 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)
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"
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"
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"

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)
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›

where
"⟦ bisim [] e e' xs; fv e = {}; 𝒟 e ⌊{}⌋; max_vars e' ≤ length xs; call e = ⌊aMvs⌋; call1 e' = ⌊aMvs⌋ ⟧
⟹ bisim01 e (e', xs)"

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 ::
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 ::
where "bisim_red0_Red1 ≡ (λ(es, h) (exs, h'). bisim_list1 es exs ∧ h = h')"

abbreviation ta_bisim01 ::
where
"ta_bisim01 ≡ ta_bisim (λt. bisim_red0_Red1)"

definition bisim_wait01 ::
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 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 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)
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 = []"
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'"
apply(induct rule: bisim_bisims.inducts)
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)
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'"

lemma sqUn_lem3: "⟦ A ⊑ A'; B ⊑ B' ⟧ ⟹ A ⊔ B ⊑ A' ⊔ B'"

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
```