Theory J0Bisim
section ‹Bisimulation proof for between source code small step semantics
with and without callstacks for single threads›
theory J0Bisim imports
J0
"../J/JWellForm"
"../Common/ExternalCallWF"
begin
inductive wf_state :: "'addr expr × 'addr expr list ⇒ bool"
where
"⟦ fvs (e # es) = {}; ∀e ∈ set es. is_call e ⟧
⟹ wf_state (e, es)"
inductive bisim_red_red0 :: "('addr expr × 'addr locals) × 'heap ⇒ ('addr expr × 'addr expr list) × 'heap ⇒ bool"
where
"wf_state ees ⟹ bisim_red_red0 ((collapse ees, Map.empty), h) (ees, h)"
abbreviation ta_bisim0 :: "('addr, 'thread_id, 'heap) J_thread_action ⇒ ('addr, 'thread_id, 'heap) J0_thread_action ⇒ bool"
where "ta_bisim0 ≡ ta_bisim (λt. bisim_red_red0)"
lemma wf_state_iff [simp, code]:
"wf_state (e, es) ⟷ fvs (e # es) = {} ∧ (∀e ∈ set es. is_call e)"
by(simp add: wf_state.simps)
lemma bisim_red_red0I [intro]:
"⟦ e' = collapse ees; xs = Map.empty; h' = h; wf_state ees ⟧ ⟹ bisim_red_red0 ((e', xs), h') (ees, h)"
by(simp add: bisim_red_red0.simps del: split_paired_Ex)
lemma bisim_red_red0_final0D:
"⟦ bisim_red_red0 (x1, m1) (x2, m2); final_expr0 x2 ⟧ ⟹ final_expr x1"
by(erule bisim_red_red0.cases) auto
context J_heap_base begin
lemma red0_preserves_wf_state:
assumes wf: "wwf_J_prog P"
and red: "P,t ⊢0 ⟨e / es, h⟩ -ta→ ⟨e' / es', h'⟩"
and wf_state: "wf_state (e, es)"
shows "wf_state (e', es')"
using wf_state
proof(cases)
assume "fvs (e # es) = {}" and icl: "∀e ∈ set es. is_call e"
hence fv: "fv e = {}" "fvs es = {}" by auto
show ?thesis
proof
from red show "fvs (e' # es') = {}"
proof cases
case (red0Red xs')
hence [simp]: "es' = es"
and red: "extTA2J0 P,P,t ⊢ ⟨e,(h, Map.empty)⟩ -ta→ ⟨e',(h', xs')⟩" by auto
from red_fv_subset[OF wf red] fv have "fv e' = {}" by auto
with fv show ?thesis by simp
next
case (red0Call a M vs U Ts T pns body D)
hence [simp]: "ta = ε"
"e' = blocks (this # pns) (Class D # Ts) (Addr a # vs) body"
"es' = e # es" "h' = h"
and sees: "P ⊢ class_type_of U sees M: Ts→T = ⌊(pns, body)⌋ in D" by auto
from sees_wf_mdecl[OF wf sees]
have "fv body ⊆ insert this (set pns)" "length Ts = length pns" by(simp_all add: wf_mdecl_def)
thus ?thesis using fv ‹length vs = length pns› by auto
next
case (red0Return E)
with fv_inline_call[of e E] show ?thesis using fv by auto
qed
next
from red icl show "∀e∈set es'. is_call e"
by cases(simp_all add: is_call_def)
qed
qed
lemma new_thread_bisim0_extNTA2J_extNTA2J0:
assumes wf: "wwf_J_prog P"
and red: "P,t ⊢ ⟨a'∙M'(vs), h⟩ -ta→ext ⟨va, h'⟩"
and nt: "NewThread t' CMa m ∈ set ⦃ta⦄⇘t⇙"
shows "bisim_red_red0 (extNTA2J P CMa, m) (extNTA2J0 P CMa, m)"
proof -
obtain C M a where CMa [simp]: "CMa = (C, M, a)" by(cases CMa)
from red nt have [simp]: "m = h'" by(rule red_ext_new_thread_heap)
from red_external_new_thread_sees[OF wf red nt[unfolded CMa]]
obtain T pns body D where h'a: "typeof_addr h' a = ⌊Class_type C⌋"
and sees: "P ⊢ C sees M: []→T = ⌊(pns, body)⌋ in D" by auto
from sees_wf_mdecl[OF wf sees] have "fv body ⊆ {this}" by(auto simp add: wf_mdecl_def)
with red nt h'a sees show ?thesis by(fastforce simp add: is_call_def intro: bisim_red_red0.intros)
qed
lemma ta_bisim0_extNTA2J_extNTA2J0:
"⟦ wwf_J_prog P; P,t ⊢ ⟨a'∙M'(vs), h⟩ -ta→ext ⟨va, h'⟩ ⟧
⟹ ta_bisim0 (extTA2J P ta) (extTA2J0 P ta)"
apply(auto simp add: ta_bisim_def intro!: list_all2_all_nthI)
apply(case_tac "⦃ta⦄⇘t⇙ ! n")
apply(simp_all)
apply(erule (1) new_thread_bisim0_extNTA2J_extNTA2J0)
apply(auto simp add: in_set_conv_nth)
done
lemma assumes wf: "wwf_J_prog P"
shows red_red0_tabisim0:
"P,t ⊢ ⟨e, s⟩ -ta→ ⟨e', s'⟩ ⟹ ∃ta'. extTA2J0 P,P,t ⊢ ⟨e, s⟩ -ta'→ ⟨e', s'⟩ ∧ ta_bisim0 ta ta'"
and reds_reds0_tabisim0:
"P,t ⊢ ⟨es, s⟩ [-ta→] ⟨es', s'⟩ ⟹ ∃ta'. extTA2J0 P,P,t ⊢ ⟨es, s⟩ [-ta'→] ⟨es', s'⟩ ∧ ta_bisim0 ta ta'"
proof(induct rule: red_reds.inducts)
case (RedCallExternal s a T M Ts Tr D vs ta va h' ta' e' s')
note red = ‹P,t ⊢ ⟨a∙M(vs),hp s⟩ -ta→ext ⟨va,h'⟩›
note T = ‹typeof_addr (hp s) a = ⌊T⌋›
from T ‹P ⊢ class_type_of T sees M: Ts→Tr = Native in D› red
have "extTA2J0 P,P,t ⊢ ⟨addr a∙M(map Val vs),s⟩ -extTA2J0 P ta→ ⟨e',(h', lcl s)⟩"
by(rule red_reds.RedCallExternal)(simp_all add: ‹e' = extRet2J (addr a∙M(map Val vs)) va›)
moreover from ‹ta' = extTA2J P ta› T red wf
have "ta_bisim0 ta' (extTA2J0 P ta)" by(auto intro: ta_bisim0_extNTA2J_extNTA2J0)
ultimately show ?case unfolding ‹s' = (h', lcl s)› by blast
next
case RedTryFail thus ?case by(force intro: red_reds.RedTryFail)
qed(fastforce intro: red_reds.intros simp add: ta_bisim_def ta_upd_simps)+
lemma assumes wf: "wwf_J_prog P"
shows red0_red_tabisim0:
"extTA2J0 P,P,t ⊢ ⟨e, s⟩ -ta→ ⟨e', s'⟩ ⟹ ∃ta'. P,t ⊢ ⟨e, s⟩ -ta'→ ⟨e', s'⟩ ∧ ta_bisim0 ta' ta"
and reds0_reds_tabisim0:
"extTA2J0 P,P,t ⊢ ⟨es, s⟩ [-ta→] ⟨es', s'⟩ ⟹ ∃ta'. P,t ⊢ ⟨es, s⟩ [-ta'→] ⟨es', s'⟩ ∧ ta_bisim0 ta' ta"
proof(induct rule: red_reds.inducts)
case (RedCallExternal s a T M Ts Tr D vs ta va h' ta' e' s')
note red = ‹P,t ⊢ ⟨a∙M(vs),hp s⟩ -ta→ext ⟨va,h'⟩›
note T = ‹typeof_addr (hp s) a = ⌊T⌋›
from T ‹P ⊢ class_type_of T sees M: Ts→Tr = Native in D› red
have "P,t ⊢ ⟨addr a∙M(map Val vs),s⟩ -extTA2J P ta→ ⟨e',(h', lcl s)⟩"
by(rule red_reds.RedCallExternal)(simp_all add: ‹e' = extRet2J (addr a∙M(map Val vs)) va›)
moreover from ‹ta' = extTA2J0 P ta› T red wf
have "ta_bisim0 (extTA2J P ta) ta'" by(auto intro: ta_bisim0_extNTA2J_extNTA2J0)
ultimately show ?case unfolding ‹s' = (h', lcl s)› by blast
next
case RedTryFail thus ?case by(force intro: red_reds.RedTryFail)
qed(fastforce intro: red_reds.intros simp add: ta_bisim_def ta_upd_simps)+
lemma red_inline_call_red:
assumes red: "P,t ⊢ ⟨e, (h, Map.empty)⟩ -ta→ ⟨e', (h', Map.empty)⟩"
shows "call E = ⌊aMvs⌋ ⟹ P,t ⊢ ⟨inline_call e E, (h, x)⟩ -ta→ ⟨inline_call e' E, (h', x)⟩"
(is "_ ⟹ ?concl E x")
and
"calls Es = ⌊aMvs⌋ ⟹ P,t ⊢ ⟨inline_calls e Es, (h, x)⟩ [-ta→] ⟨inline_calls e' Es, (h', x)⟩"
(is "_ ⟹ ?concls Es x")
proof(induct E and Es arbitrary: x and x rule: call.induct calls.induct)
case (Call obj M pns x)
note IHobj = ‹⋀x. call obj = ⌊aMvs⌋ ⟹ ?concl obj x›
note IHpns = ‹⋀x. calls pns = ⌊aMvs⌋ ⟹ ?concls pns x›
obtain a M' vs where [simp]: "aMvs = (a, M', vs)" by(cases aMvs, auto)
from ‹call (obj∙M(pns)) = ⌊aMvs⌋› have "call (obj∙M(pns)) = ⌊(a, M', vs)⌋" by simp
thus ?case
proof(induct rule: call_callE)
case CallObj
with IHobj[of x] show ?case by(fastforce intro: red_reds.CallObj)
next
case (CallParams v'')
with IHpns[of x] show ?case by(fastforce intro: red_reds.CallParams)
next
case Call
from red_lcl_add[OF red, where ?l0.0=x]
have "P,t ⊢ ⟨e,(h, x)⟩ -ta→ ⟨e', (h', x)⟩" by simp
with Call show ?case by(fastforce dest: BlockRed)
qed
next
case (Block V T' vo exp x)
note IH = ‹⋀x. call exp = ⌊aMvs⌋ ⟹ ?concl exp x›
from IH[of "x(V := vo)"] ‹call {V:T'=vo; exp} = ⌊aMvs⌋›
show ?case by(clarsimp simp del: fun_upd_apply)(drule BlockRed, auto)
next
case (Cons_exp exp exps x)
show ?case
proof(cases "is_val exp")
case True
with ‹calls (exp # exps) = ⌊aMvs⌋› have "calls exps = ⌊aMvs⌋" by auto
with ‹calls exps = ⌊aMvs⌋ ⟹ ?concls exps x› True
show ?thesis by(fastforce intro: ListRed2)
next
case False
with ‹calls (exp # exps) = ⌊aMvs⌋› have "call exp = ⌊aMvs⌋" by auto
with ‹call exp = ⌊aMvs⌋ ⟹ ?concl exp x›
show ?thesis by(fastforce intro: ListRed1)
qed
qed(fastforce intro: red_reds.intros)+
lemma
assumes "P ⊢ class_type_of T sees M:Us→U = ⌊(pns, body)⌋ in D" "length vs = length pns" "length Us = length pns"
shows is_call_red_inline_call:
"⟦ call e = ⌊(a, M, vs)⌋; typeof_addr (hp s) a = ⌊T⌋ ⟧
⟹ P,t ⊢ ⟨e, s⟩ -ε→ ⟨inline_call (blocks (this # pns) (Class D # Us) (Addr a # vs) body) e, s⟩"
(is "_ ⟹ _ ⟹ ?red e s")
and is_calls_reds_inline_calls:
"⟦ calls es = ⌊(a, M, vs)⌋; typeof_addr (hp s) a = ⌊T⌋ ⟧
⟹ P,t ⊢ ⟨es, s⟩ [-ε→] ⟨inline_calls (blocks (this # pns) (Class D # Us) (Addr a # vs) body) es, s⟩"
(is "_ ⟹ _ ⟹ ?reds es s")
proof(induct e and es arbitrary: s and s rule: call.induct calls.induct)
case (Call obj M' params s)
note IHObj = ‹⋀s. ⟦call obj = ⌊(a, M, vs)⌋; typeof_addr (hp s) a = ⌊T⌋ ⟧ ⟹ ?red obj s›
note IHParams = ‹⋀s. ⟦ calls params = ⌊(a, M, vs)⌋; typeof_addr (hp s) a = ⌊T⌋ ⟧ ⟹ ?reds params s›
from ‹call (obj∙M'(params)) = ⌊(a, M, vs)⌋›
show ?case
proof(induct rule: call_callE)
case CallObj
from IHObj[OF CallObj] ‹typeof_addr (hp s) a = ⌊T⌋› have "?red obj s" by blast
moreover from CallObj have "¬ is_val obj" by auto
ultimately show ?case by(auto intro: red_reds.CallObj)
next
case (CallParams v)
from IHParams[OF ‹calls params = ⌊(a, M, vs)⌋›] ‹typeof_addr (hp s) a = ⌊T⌋›
have "?reds params s" by blast
moreover from CallParams have "¬ is_vals params" by auto
ultimately show ?case using ‹obj = Val v› by(auto intro: red_reds.CallParams)
next
case Call
with RedCall[where s=s, simplified, OF ‹typeof_addr (hp s) a = ⌊T⌋› ‹P ⊢ class_type_of T sees M:Us→U = ⌊(pns, body)⌋ in D› ‹length vs = length pns› ‹length Us = length pns›]
show ?thesis by(simp)
qed
next
case (Block V ty vo exp s)
note IH = ‹⋀s. ⟦call exp = ⌊(a, M, vs)⌋; typeof_addr (hp s) a = ⌊T⌋ ⟧ ⟹ ?red exp s›
from ‹call {V:ty=vo; exp} = ⌊(a, M, vs)⌋› IH[of "(hp s, (lcl s)(V := vo))"] ‹typeof_addr (hp s) a = ⌊T⌋›
show ?case by(cases s, simp del: fun_upd_apply)(drule red_reds.BlockRed, simp)
qed(fastforce intro: red_reds.intros)+
lemma red_inline_call_red':
assumes fv: "fv ee = {}"
and eefin: "¬ final ee"
shows "⟦ call E = ⌊aMvs⌋; P,t ⊢ ⟨inline_call ee E, (h, x)⟩ -ta→ ⟨E', (h', x')⟩ ⟧
⟹ ∃ee'. E' = inline_call ee' E ∧ P,t ⊢ ⟨ee, (h, Map.empty)⟩ -ta→ ⟨ee', (h', Map.empty)⟩ ∧ x = x'"
(is "⟦ _; _ ⟧ ⟹ ?concl E E' x x'")
and "⟦ calls Es = ⌊aMvs⌋; P,t ⊢ ⟨inline_calls ee Es, (h, x)⟩ [-ta→] ⟨Es', (h', x')⟩ ⟧
⟹ ∃ee'. Es' = inline_calls ee' Es ∧ P,t ⊢ ⟨ee, (h, Map.empty)⟩ -ta→ ⟨ee', (h', Map.empty)⟩ ∧ x = x'"
(is "⟦ _; _ ⟧ ⟹ ?concls Es Es' x x'")
proof(induct E and Es arbitrary: E' x x' and Es' x x' rule: call.induct calls.induct)
case new thus ?case by simp
next
case (newArray T exp E' x x')
thus ?case using eefin by(auto elim!: red_cases)
next
case Cast thus ?case using eefin by(auto elim!:red_cases)
next
case InstanceOf thus ?case using eefin by(auto elim!:red_cases)
next
case Val thus ?case by simp
next
case Var thus ?case by simp
next
case LAss
thus ?case using eefin by(auto elim!: red_cases)
next
case BinOp
thus ?case using eefin by(auto elim!: red_cases split: if_split_asm)
next
case AAcc
thus ?case using eefin by(auto elim!: red_cases split: if_split_asm)
next
case AAss thus ?case using eefin by(auto elim!: red_cases split: if_split_asm)
next
case ALen thus ?case using eefin by(auto elim!: red_cases split: if_split_asm)
next
case FAcc thus ?case using eefin by(auto elim!: red_cases)
next
case FAss thus ?case using eefin by(auto elim!: red_cases split: if_split_asm)
next
case CompareAndSwap thus ?case using eefin by(auto elim!: red_cases split: if_split_asm)
next
case (Call obj M pns E' x x')
note IHobj = ‹⋀x E' x'. ⟦call obj = ⌊aMvs⌋; P,t ⊢ ⟨inline_call ee obj,(h, x)⟩ -ta→ ⟨E',(h', x')⟩⟧
⟹ ?concl obj E' x x'›
note IHpns = ‹⋀Es' x x'. ⟦calls pns = ⌊aMvs⌋; P,t ⊢ ⟨inline_calls ee pns,(h, x)⟩ [-ta→] ⟨Es',(h', x')⟩⟧
⟹ ?concls pns Es' x x'›
note red = ‹P,t ⊢ ⟨inline_call ee (obj∙M(pns)),(h, x)⟩ -ta→ ⟨E',(h', x')⟩›
obtain a M' vs where [simp]: "aMvs = (a, M', vs)" by(cases aMvs, auto)
from ‹call (obj∙M(pns)) = ⌊aMvs⌋› have "call (obj∙M(pns)) = ⌊(a,M',vs)⌋" by simp
thus ?case
proof(cases rule: call_callE)
case CallObj
hence "¬ is_val obj" by auto
with red CallObj eefin obtain obj' where "E' = obj'∙M(pns)"
and red': "P,t ⊢ ⟨inline_call ee obj,(h, x)⟩ -ta→ ⟨obj',(h', x')⟩"
by(auto elim!: red_cases)
from IHobj[OF _ red'] CallObj obtain ee'
where "inline_call ee' obj = obj'" "x = x'"
and "P,t ⊢ ⟨ee,(h, Map.empty)⟩ -ta→ ⟨ee',(h', Map.empty)⟩" by(auto simp del: fun_upd_apply)
with ‹E' = obj'∙M(pns)› CallObj red' show ?thesis by(fastforce simp del: fun_upd_apply)
next
case (CallParams v'')
hence "¬ is_vals pns" by auto
with red CallParams eefin obtain pns' where "E' = obj∙M(pns')"
and red': "P,t ⊢ ⟨inline_calls ee pns,(h, x)⟩ [-ta→] ⟨pns',(h', x')⟩"
by(auto elim!: red_cases)
from IHpns[OF _ red'] CallParams obtain ee'
where "inline_calls ee' pns = pns'" "x = x'"
and "P,t ⊢ ⟨ee,(h, Map.empty)⟩ -ta→ ⟨ee',(h', Map.empty)⟩"
by(auto simp del: fun_upd_apply)
with ‹E' = obj∙M(pns')› CallParams red' ‹¬ is_vals pns›
show ?thesis by(auto simp del: fun_upd_apply)
next
case Call
with red have red': "P,t ⊢ ⟨ee,(h, x)⟩ -ta→ ⟨E',(h', x')⟩" by(auto)
from red_lcl_sub[OF red', of "{}"] fv
have "P,t ⊢ ⟨ee,(h, Map.empty)⟩ -ta→ ⟨E',(h', Map.empty)⟩" by simp
moreover have "x' = x"
proof(rule ext)
fix V
from red_notfree_unchanged[OF red', of V] fv
show "x' V = x V" by simp
qed
ultimately show ?thesis using Call by simp
qed
next
case (Block V ty voo exp E' x x')
note IH = ‹⋀x E' x'. ⟦call exp = ⌊aMvs⌋; P,t ⊢ ⟨inline_call ee exp,(h, x)⟩ -ta→ ⟨E',(h', x')⟩⟧
⟹ ?concl exp E' x x'›
from ‹call {V:ty=voo; exp} = ⌊aMvs⌋› have ic: "call exp = ⌊aMvs⌋" by simp
note red = ‹P,t ⊢ ⟨inline_call ee {V:ty=voo; exp},(h, x)⟩ -ta→ ⟨E',(h', x')⟩›
hence "P,t ⊢ ⟨{V:ty=voo; inline_call ee exp},(h, x)⟩ -ta→ ⟨E',(h', x')⟩" by simp
with ic eefin obtain exp' x'' where "E' = {V:ty=x'' V; exp'}"
and red': "P,t ⊢ ⟨inline_call ee exp,(h, fun_upd x V voo)⟩ -ta→ ⟨exp',(h', x'')⟩"
and "x' = fun_upd x'' V (x V)"
by -(erule red.cases,auto dest: inline_call_eq_Val)
from IH[OF ic red'] obtain ee' vo'
where icl: "inline_call ee' exp = exp'" "x'' = fun_upd x V voo"
and red'': "P,t ⊢ ⟨ee,(h, Map.empty)⟩ -ta→ ⟨ee',(h', Map.empty)⟩" by blast
from ‹x'' = fun_upd x V voo› have "x'' V = voo" by(simp add: fun_eq_iff)
with icl red'' ‹E' = {V:ty=x'' V; exp'}› ‹x' = fun_upd x'' V (x V)› red'
show ?case by(auto simp del: fun_upd_apply)
next
case Synchronized thus ?case using eefin by(auto elim!: red_cases)
next
case InSynchronized thus ?case using eefin by(auto elim!: red_cases)
next
case Seq
thus ?case using eefin by(auto elim!: red_cases)
next
case Cond thus ?case using eefin by(auto elim!: red_cases)
next
case While thus ?case by simp
next
case throw
thus ?case using eefin by(auto elim!: red_cases)
next
case TryCatch
thus ?case using eefin by(auto elim!: red_cases)
next
case Nil_exp thus ?case by simp
next
case Cons_exp
thus ?case using eefin by(auto elim!: reds_cases split: if_split_asm)
qed
lemma assumes sees: "P ⊢ class_type_of T sees M:Us→U = ⌊(pns, body)⌋ in D"
shows is_call_red_inline_callD:
"⟦ P,t ⊢ ⟨e, s⟩ -ta→ ⟨e', s'⟩; call e = ⌊(a, M, vs)⌋; typeof_addr (hp s) a = ⌊T⌋ ⟧
⟹ e' = inline_call (blocks (this # pns) (Class D # Us) (Addr a # vs) body) e"
and is_calls_reds_inline_callsD:
"⟦ P,t ⊢ ⟨es, s⟩ [-ta→] ⟨es', s'⟩; calls es = ⌊(a, M, vs)⌋; typeof_addr (hp s) a = ⌊T⌋ ⟧
⟹ es' = inline_calls (blocks (this # pns) (Class D # Us) (Addr a # vs) body) es"
proof(induct rule: red_reds.inducts)
case RedCall with sees show ?case by(auto dest: sees_method_fun)
next
case RedCallExternal
with sees show ?case by(auto dest: sees_method_fun)
next
case (BlockRed e h x V vo ta e' h' x' T')
from ‹call {V:T'=vo; e} = ⌊(a, M, vs)⌋› ‹typeof_addr (hp (h, x)) a = ⌊T⌋› sees
have "call e = ⌊(a, M, vs)⌋" and "¬ synthesized_call P h (a, M, vs)"
by(auto simp add: synthesized_call_conv dest: sees_method_fun)
with ‹P,t ⊢ ⟨e,(h, x(V := vo))⟩ -ta→ ⟨e',(h', x')⟩›
have "x(V := vo) = x'" by(auto dest: is_call_red_state_unchanged)
hence "x' V = vo" by auto
with BlockRed show ?case by(simp)
qed(fastforce split: if_split_asm)+
lemma (in -) wf_state_ConsD: "wf_state (e, e' # es) ⟹ wf_state (e', es)"
by(simp)
lemma red_fold_exs:
"⟦ P,t ⊢ ⟨e,(h, Map.empty)⟩ -ta→ ⟨e',(h', Map.empty)⟩; wf_state (e, es) ⟧
⟹ P,t ⊢ ⟨collapse (e, es), (h, Map.empty)⟩ -ta→ ⟨collapse (e', es), (h', Map.empty)⟩"
(is "⟦ _; _ ⟧ ⟹ ?concl e e' es")
proof(induction es arbitrary: e e')
case Nil thus ?case by simp
next
case (Cons E es)
note wf = ‹wf_state (e, E # es)›
note red = ‹P,t ⊢ ⟨e,(h, Map.empty)⟩ -ta→ ⟨e',(h', Map.empty)⟩›
from wf obtain a M vs arrobj where call: "call E = ⌊(a, M, vs)⌋"
by(auto simp add: is_call_def)
from red call have "P,t ⊢ ⟨inline_call e E,(h, Map.empty)⟩ -ta→ ⟨inline_call e' E,(h', Map.empty)⟩"
by(rule red_inline_call_red)
hence "P,t ⊢ ⟨collapse (inline_call e E, es),(h, Map.empty)⟩ -ta→ ⟨collapse (inline_call e' E, es),(h', Map.empty)⟩"
proof(rule Cons.IH)
from wf have "fv E = {}" "fv e = {}" by auto
with fv_inline_call[of e E] have "fv (inline_call e E) = {}" by auto
thus "wf_state (inline_call e E, es)" using wf by auto
qed
thus ?case by simp
qed
lemma red_fold_exs':
"⟦ P,t ⊢ ⟨collapse (e, es), (h, Map.empty)⟩ -ta→ ⟨e', (h', x')⟩; wf_state (e, es); ¬ final e ⟧
⟹ ∃E'. e' = collapse (E', es) ∧ P,t ⊢ ⟨e, (h, Map.empty)⟩ -ta→ ⟨E', (h', Map.empty)⟩"
(is "⟦ _; _; _ ⟧ ⟹ ?concl e es")
proof(induction es arbitrary: e)
case Nil
hence red': "P,t ⊢ ⟨e,(h, Map.empty)⟩ -ta→ ⟨e',(h', x')⟩" by simp
with red_dom_lcl[OF this] ‹wf_state (e, [])› show ?case by auto
next
case (Cons E es)
note wf = ‹wf_state (e, E # es)›
note nfin = ‹¬ final e›
from wf have "fv e = {}" by simp
from wf obtain a M vs where call: "call E = ⌊(a, M, vs)⌋" by(auto simp add: is_call_def)
from ‹P,t ⊢ ⟨collapse (e, E # es),(h, Map.empty)⟩ -ta→ ⟨e',(h', x')⟩›
have "P,t ⊢ ⟨collapse (inline_call e E, es),(h, Map.empty)⟩ -ta→ ⟨e',(h', x')⟩" by simp
moreover from wf fv_inline_call[of e E] have "wf_state (inline_call e E, es)" by auto
moreover from nfin call have "¬ final (inline_call e E)" by(auto elim!: final.cases)
ultimately have "?concl (inline_call e E) es" by(rule Cons.IH)
then obtain E' where e': "e' = collapse (E', es)"
and red': "P,t ⊢ ⟨inline_call e E,(h, Map.empty)⟩ -ta→ ⟨E',(h', Map.empty)⟩" by blast
from red_inline_call_red'(1)[OF ‹fv e = {}› nfin ‹call E = ⌊(a, M, vs)⌋› red']
obtain e' where "E' = inline_call e' E" "P,t ⊢ ⟨e,(h, Map.empty)⟩ -ta→ ⟨e',(h', Map.empty)⟩" by auto
thus ?case using e' by auto
qed
lemma τRed0r_inline_call_not_final:
"∃e' es'. τRed0r P t h (e, es) (e', es') ∧ (final e' ⟶ es' = []) ∧ collapse (e, es) = collapse (e', es')"
proof(induct es arbitrary: e)
case Nil thus ?case by blast
next
case (Cons e es E) show ?case
proof(cases "final E")
case True
hence "τRed0 P t h (E, e # es) (inline_call E e, es)" by(auto intro: red0Return)
moreover from Cons[of "inline_call E e"] obtain e' es'
where "τRed0r P t h (inline_call E e, es) (e', es')" "final e' ⟶ es' = []"
"collapse (inline_call E e, es) = collapse (e', es')" by blast
ultimately show ?thesis unfolding collapse.simps by(blast intro: converse_rtranclp_into_rtranclp)
qed blast
qed
lemma τRed0_preserves_wf_state:
"⟦ wwf_J_prog P; τRed0 P t h (e, es) (e', es'); wf_state (e, es) ⟧ ⟹ wf_state (e', es')"
by(auto simp del: wf_state_iff intro: red0_preserves_wf_state)
lemma τRed0r_preserves_wf_state:
assumes wf: "wwf_J_prog P"
shows "⟦ τRed0r P t h (e, es) (e', es'); wf_state (e, es) ⟧ ⟹ wf_state (e', es')"
by(induct rule: rtranclp_induct2)(blast intro: τRed0_preserves_wf_state[OF wf])+
lemma τRed0t_preserves_wf_state:
assumes wf: "wwf_J_prog P"
shows "⟦ τRed0t P t h (e, es) (e', es'); wf_state (e, es) ⟧ ⟹ wf_state (e', es')"
by(induct rule: tranclp_induct2)(blast intro: τRed0_preserves_wf_state[OF wf])+
lemma collapse_τmove0_inv:
"⟦ ∀e∈set es. is_call e; ¬ final e ⟧ ⟹ τmove0 P h (collapse (e, es)) = τmove0 P h e"
proof(induction es arbitrary: e)
case Nil thus ?case by clarsimp
next
case (Cons e es e'')
from ‹∀a∈set (e # es). is_call a› obtain aMvs where calls: "∀e∈set es. is_call e"
and call: "call e = ⌊aMvs⌋" by(auto simp add: is_call_def)
note calls moreover
from ‹¬ final e''› call have "¬ final (inline_call e'' e)" by(auto simp add: final_iff)
ultimately have "τmove0 P h (collapse (inline_call e'' e, es)) = τmove0 P h (inline_call e'' e)"
by(rule Cons.IH)
also from call ‹¬ final e''› have "… = τmove0 P h e''" by(auto simp add: inline_call_τmove0_inv)
finally show ?case by simp
qed
lemma τRed0r_into_silent_moves:
"τRed0r P t h (e, es) (e', es') ⟹ red0_mthr.silent_moves P t ((e, es), h) ((e', es'), h)"
by(induct rule: rtranclp_induct2)(fastforce intro: τtrsys.silent_move.intros elim!: rtranclp.rtrancl_into_rtrancl)+
lemma τRed0t_into_silent_movet:
"τRed0t P t h (e, es) (e', es') ⟹ red0_mthr.silent_movet P t ((e, es), h) ((e', es'), h)"
by(induct rule: tranclp_induct2)(fastforce intro: τtrsys.silent_move.intros elim!: tranclp.trancl_into_trancl)+
lemma red_simulates_red0:
assumes wwf: "wwf_J_prog P"
and sim: "bisim_red_red0 s1 s2" "mred0 P t s2 ta2 s2'" "¬ τMOVE0 P s2 ta2 s2'"
shows "∃s1' ta1. mred P t s1 ta1 s1' ∧ ¬ τMOVE P s1 ta1 s1' ∧ bisim_red_red0 s1' s2' ∧ ta_bisim0 ta1 ta2"
proof -
note sim
moreover obtain e1 h1 x1 where s1: "s1 = ((e1, x1), h1)" by(cases s1, auto)
moreover obtain e' es' h2' where s2': "s2' = ((e', es'), h2')" by(cases s2', auto)
moreover obtain e es h2 where s2: "s2 = ((e, es), h2)" by(cases s2, auto)
ultimately have bisim: "bisim_red_red0 ((e1, x1), h1) ((e, es), h2)"
and red: "P,t ⊢0 ⟨e/es, h2⟩ -ta2→ ⟨e'/es', h2'⟩"
and τ: "¬ τmove0 P h2 e ∧ ¬ final e ∨ ta2 ≠ ε" by auto
from red τ have τ: "¬ τmove0 P h2 e" and nfin: "¬ final e"
by(cases, auto dest: red_τ_taD[where extTA="extTA2J0 P", OF extTA2J0_ε])+
from bisim have heap: "h1 = h2" and fold: "e1 = collapse (e, es)"
and x1: "x1 = Map.empty" and wf_state: "wf_state (e, es)"
by(auto elim!: bisim_red_red0.cases)
from red wf_state have wf_state': "wf_state (e', es')" by(rule red0_preserves_wf_state[OF wwf])
from red show ?thesis
proof(cases)
case (red0Red xs')
hence [simp]: "es' = es"
and "extTA2J0 P,P,t ⊢ ⟨e, (h2, Map.empty)⟩ -ta2→ ⟨e', (h2', xs')⟩" by auto
from red0_red_tabisim0[OF wwf this(2)] obtain ta1
where red': "P,t ⊢ ⟨e,(h2, Map.empty)⟩ -ta1→ ⟨e',(h2', xs')⟩"
and tasim: "ta_bisim0 ta1 ta2" by auto
moreover from wf_state have "fv e = {}" by auto
with red_dom_lcl[OF red'] red_fv_subset[OF wwf red'] have "xs' = Map.empty" by auto
ultimately have "P,t ⊢ ⟨e,(h2, Map.empty)⟩ -ta1→ ⟨e',(h2', Map.empty)⟩" by simp
with wf_state have "P,t ⊢ ⟨collapse (e, es),(h2, Map.empty)⟩ -ta1→ ⟨collapse (e', es),(h2', Map.empty)⟩"
by -(erule red_fold_exs, auto)
moreover from τ wf_state fold nfin have "¬ τmove0 P h2 e1" by(auto simp add: collapse_τmove0_inv)
hence "¬ τMOVE P ((collapse (e, es), Map.empty), h2) ta1 ((collapse (e', es), Map.empty), h2')"
unfolding fold by auto
moreover from wf_state' have "bisim_red_red0 ((collapse (e', es), Map.empty), h2') s2'"
unfolding s2' by(auto)
ultimately show ?thesis unfolding heap s1 s2 s2' fold x1
using tasim by(fastforce intro!: exI rtranclp.rtrancl_refl)
next
case red0Call
with τ have False
by(auto simp add: synthesized_call_def τexternal'_def dest!: τmove0_callD[where P=P and h=h2] dest: sees_method_fun)
thus ?thesis ..
next
case red0Return with nfin show ?thesis by simp
qed
qed
lemma delay_bisimulation_measure_red_red0:
assumes wf: "wwf_J_prog P"
shows "delay_bisimulation_measure (mred P t) (mred0 P t) bisim_red_red0 ta_bisim0 (τMOVE P) (τMOVE0 P) (λe e'. False) (λ((e, es), h) ((e, es'), h). length es < length es')"
proof
show "wfP (λe e'. False)" by auto
next
have "wf {(x :: nat, y). x < y}" by(rule wf_less)
hence "wf (inv_image {(x :: nat, y). x < y} (length o snd o fst))" by(rule wf_inv_image)
also have "inv_image {(x :: nat, y). x < y} (length o snd o fst) = {(x, y). (λ((e, es), h) ((e, es'), h). length es < length es') x y}" by auto
finally show "wfP (λ((e, es), h) ((e, es'), h). length es < length es')"
unfolding wfp_def .
next
fix s1 s2 s1'
assume "bisim_red_red0 s1 s2" and "red_mthr.silent_move P t s1 s1'"
moreover obtain e1 h1 x1 where s1: "s1 = ((e1, x1), h1)" by(cases s1, auto)
moreover obtain e1' h1' x1' where s1': "s1' = ((e1', x1'), h1')" by(cases s1', auto)
moreover obtain e es h2 where s2: "s2 = ((e, es), h2)" by(cases s2, auto)
ultimately have bisim: "bisim_red_red0 ((e1, x1), h1) ((e, es), h2)"
and red: "P,t ⊢ ⟨e1, (h1, x1)⟩ -ε→ ⟨e1', (h1', x1')⟩"
and τ: "τmove0 P h1 e1" by(auto elim: τtrsys.silent_move.cases)
from bisim have heap: "h1 = h2"
and fold: "e1 = collapse (e, es)"
and x1: "x1 = Map.empty"
and wf_state: "wf_state (e, es)"
by(auto elim!: bisim_red_red0.cases)
from τRed0r_inline_call_not_final[of P t h1 e es]
obtain e' es' where red1: "τRed0r P t h1 (e, es) (e', es')"
and "final e' ⟹ es' = []"
and feq: "collapse (e, es) = collapse (e', es')" by blast
have nfin: "¬ final e'"
proof
assume fin: "final e'"
hence "es' = []" by(rule ‹final e' ⟹ es' = []›)
with fold fin feq have "final e1" by simp
with red show False by auto
qed
from red1 wf_state have wf_state': "wf_state (e', es')" by(rule τRed0r_preserves_wf_state[OF wf])
hence fv: "fvs (e' # es') = {}" and icl: "∀e∈set es'. is_call e" by auto
from red_fold_exs'[OF red[unfolded fold x1 feq] wf_state' nfin]
obtain E' where e1': "e1' = collapse (E', es')"
and red': "P,t ⊢ ⟨e',(h1, Map.empty)⟩ -ε→ ⟨E',(h1', Map.empty)⟩" by auto
from fv fv_collapse[of es e] wf_state fold feq have "fv e1 = {}" by(auto)
with red_dom_lcl[OF red] x1 have x1': "x1' = Map.empty" by simp
from red_red0_tabisim0[OF wf red']
have red'': "extTA2J0 P,P,t ⊢ ⟨e',(h1, Map.empty)⟩ -ε→ ⟨E',(h1', Map.empty)⟩" by simp
show "bisim_red_red0 s1' s2 ∧ (λe e'. False)^++ s1' s1 ∨
(∃s2'. red0_mthr.silent_movet P t s2 s2' ∧ bisim_red_red0 s1' s2')"
proof(cases "no_call P h1 e'")
case True
with red'' have "P,t ⊢0 ⟨e'/es', h1⟩ -ε→ ⟨E'/es', h1'⟩" unfolding no_call_def by(rule red0Red)
moreover from red τ have [simp]: "h1' = h1" by(auto dest: τmove0_heap_unchanged)
moreover from τ fold feq icl nfin have "τmove0 P h1 e'" by(simp add: collapse_τmove0_inv)
ultimately have "τRed0 P t h1 (e', es') (E', es')" using ‹τmove0 P h1 e'› by auto
with red1 have "τRed0t P t h1 (e, es) (E', es')" by(rule rtranclp_into_tranclp1)
moreover hence "wf_state (E', es')" using wf_state by(rule τRed0t_preserves_wf_state[OF wf])
hence "bisim_red_red0 ((e1', x1'), h1) ((E', es'), h1)" unfolding x1' e1' by(auto)
ultimately show ?thesis using s1 s1' s2 heap by simp(blast intro: τRed0t_into_silent_movet)
next
case False
then obtain a M vs where call: "call e' = ⌊(a, M, vs)⌋"
and notsynth: "¬ synthesized_call P h1 (a, M, vs)" by(auto simp add: no_call_def)
from notsynth called_methodD[OF red'' call] obtain T D Us U pns body
where "h1' = h1"
and ha: "typeof_addr h1 a = ⌊T⌋"
and sees: "P ⊢ class_type_of T sees M: Us→U = ⌊(pns, body)⌋ in D"
and length: "length vs = length pns" "length Us = length pns"
by(auto)
let ?e = "blocks (this # pns) (Class D # Us) (Addr a # vs) body"
from call ha have "P,t ⊢0 ⟨e'/es',h1⟩ -ε→ ⟨?e/e' # es',h1⟩"
using sees length by(rule red0Call)
moreover from τ fold feq icl nfin False have "τmove0 P h1 e'" by(simp add: collapse_τmove0_inv)
ultimately have "τRed0 P t h1 (e', es') (?e, e' # es')" by auto
with red1 have "τRed0t P t h1 (e, es) (?e, e' # es')" by(rule rtranclp_into_tranclp1)
moreover {
from ‹P,t ⊢0 ⟨e'/es',h1⟩ -ε→ ⟨?e/e' # es',h1⟩› have "wf_state (?e, e' # es')"
using wf_state' by(rule red0_preserves_wf_state[OF wf])
moreover from is_call_red_inline_callD[OF sees red' call] ha
have "E' = inline_call ?e e'" by auto
ultimately have "bisim_red_red0 s1' ((?e, e' # es'), h1')" unfolding s1' e1' x1'
by(auto del: wf_state.cases wf_state.intros) }
moreover from red' call notsynth have "h1 = h1'"
by(auto dest: is_call_red_state_unchanged)
ultimately show ?thesis unfolding heap x1' x1 s2 s1' ‹h1' = h1›
by(blast intro: τRed0t_into_silent_movet)
qed
next
fix s1 s2 s2'
assume "bisim_red_red0 s1 s2" and "red0_mthr.silent_move P t s2 s2'"
moreover obtain e1 h1 x1 where s1: "s1 = ((e1, x1), h1)" by(cases s1, auto)
moreover obtain e' es' h2' where s2': "s2' = ((e', es'), h2')" by(cases s2', auto)
moreover obtain e es h2 where s2: "s2 = ((e, es), h2)" by(cases s2, auto)
ultimately have bisim: "bisim_red_red0 ((e1, x1), h1) ((e, es), h2)"
and red: "P,t ⊢0 ⟨e/es, h2⟩ -ε→ ⟨e'/es', h2'⟩"
and τ: "τmove0 P h2 e ∨ final e" by(auto elim: τtrsys.silent_move.cases)
from bisim have heap: "h1 = h2"
and fold: "e1 = collapse (e, es)"
and x1: "x1 = Map.empty" and wf_state: "wf_state (e, es)"
by(auto elim!: bisim_red_red0.cases)
from red wf_state have wf_state': "wf_state (e', es')" by(rule red0_preserves_wf_state[OF wf])
from red show "bisim_red_red0 s1 s2' ∧ (λ((e, es), h) ((e, es'), h). length es < length es')⇧+⇧+ s2' s2 ∨
(∃s1'. red_mthr.silent_movet P t s1 s1' ∧ bisim_red_red0 s1' s2')"
proof cases
case (red0Red xs')
hence [simp]: "es' = es"
and "extTA2J0 P,P,t ⊢ ⟨e, (h2, Map.empty)⟩ -ε→ ⟨e', (h2', xs')⟩" by auto
from red0_red_tabisim0[OF wf this(2)] have red': "P,t ⊢ ⟨e,(h2, Map.empty)⟩ -ε→ ⟨e',(h2', xs')⟩" by auto
moreover from wf_state have "fv e = {}" by auto
with red_dom_lcl[OF red'] red_fv_subset[OF wf red'] have "xs' = Map.empty" by auto
ultimately have "P,t ⊢ ⟨e,(h2, Map.empty)⟩ -ε→ ⟨e',(h2', Map.empty)⟩" by simp
hence "P,t ⊢ ⟨collapse (e, es),(h2, Map.empty)⟩ -ε→ ⟨collapse (e', es),(h2', Map.empty)⟩"
using wf_state by(rule red_fold_exs)
moreover from red' have "¬ final e" by auto
with τ wf_state fold have "τmove0 P h2 e1" by(auto simp add: collapse_τmove0_inv)
ultimately have "red_mthr.silent_movet P t s1 ((collapse (e', es), Map.empty), h2')"
using s1 fold τ x1 heap by(auto intro: τtrsys.silent_move.intros)
moreover from wf_state' have "bisim_red_red0 ((collapse (e', es), Map.empty), h2') s2'"
unfolding s2' by(auto)
ultimately show ?thesis by blast
next
case (red0Call a M vs U Ts T pns body D)
hence [simp]: "es' = e # es" "h2' = h2" "e' = blocks (this # pns) (Class D # Ts) (Addr a # vs) body"
and call: "call e = ⌊(a, M, vs)⌋"
and ha: "typeof_addr h2 a = ⌊U⌋"
and sees: "P ⊢ class_type_of U sees M: Ts→T = ⌊(pns, body)⌋ in D"
and len: "length vs = length pns" "length Ts = length pns" by auto
from is_call_red_inline_call(1)[OF sees len call, of "(h2, Map.empty)"] ha
have "P,t ⊢ ⟨e,(h2, Map.empty)⟩ -ε→ ⟨inline_call e' e, (h2, Map.empty)⟩" by simp
hence "P,t ⊢ ⟨collapse (e, es), (h2, Map.empty)⟩ -ε→ ⟨collapse (inline_call e' e, es), (h2, Map.empty)⟩"
using wf_state by(rule red_fold_exs)
moreover from call ha wf_state τ have "τmove0 P h2 (collapse (e, es))"
by(subst collapse_τmove0_inv) auto
hence "τMOVE P ((collapse (e, es), Map.empty), h2) ε ((collapse (inline_call e' e, es), Map.empty), h2)" by auto
moreover from wf_state'
have "bisim_red_red0 ((collapse (inline_call e' e, es), Map.empty), h2) ((e', es'), h2')"
by(auto)
ultimately show ?thesis unfolding s1 s2 s2' fold heap x1 by(fastforce)
next
case (red0Return E)
hence [simp]: "es = E # es'" "e' = inline_call e E" "h2' = h2" by auto
from fold wf_state'
have "bisim_red_red0 ((e1, Map.empty), h1) ((inline_call e E, es'), h2)"
unfolding heap by(auto)
thus ?thesis using s1 s2' s2 x1 by auto
qed
next
fix s1 s2 ta1 s1'
assume "bisim_red_red0 s1 s2" and "mred P t s1 ta1 s1'" and "¬ τMOVE P s1 ta1 s1'"
moreover obtain e1 h1 x1 where s1: "s1 = ((e1, x1), h1)" by(cases s1, auto)
moreover obtain e1' h1' x1' where s1': "s1' = ((e1', x1'), h1')" by(cases s1', auto)
moreover obtain e es h2 where s2: "s2 = ((e, es), h2)" by(cases s2, auto)
ultimately have bisim: "bisim_red_red0 ((e1, x1), h1) ((e, es), h2)"
and red: "P,t ⊢ ⟨e1, (h1, x1)⟩ -ta1→ ⟨e1', (h1', x1')⟩"
and τ: "¬ τmove0 P h1 e1" by(auto dest: red_τ_taD[where extTA="extTA2J P", OF extTA2J_ε])
from bisim have heap: "h1 = h2"
and fold: "e1 = collapse (e, es)"
and x1: "x1 = Map.empty"
and wf_state: "wf_state (e, es)"
by(auto elim!: bisim_red_red0.cases)
from τRed0r_inline_call_not_final[of P t h1 e es]
obtain e' es' where red1: "τRed0r P t h1 (e, es) (e', es')"
and "final e' ⟹ es' = []" and feq: "collapse (e, es) = collapse (e', es')" by blast
hence red1': "red0_mthr.silent_moves P t ((e, es), h2) ((e', es'), h2)"
unfolding heap by -(rule τRed0r_into_silent_moves)
have nfin: "¬ final e'"
proof
assume fin: "final e'"
hence "es' = []" by(rule ‹final e' ⟹ es' = []›)
with fold fin feq have "final e1" by simp
with red show False by auto
qed
from red1 wf_state have wf_state': "wf_state (e', es')" by(rule τRed0r_preserves_wf_state[OF wf])
hence fv: "fvs (e' # es') = {}" and icl: "∀e ∈ set es'. is_call e" by auto
from red_fold_exs'[OF red[unfolded fold x1 feq] wf_state' nfin]
obtain E' where e1': "e1' = collapse (E', es')"
and red': "P,t ⊢ ⟨e',(h1, Map.empty)⟩ -ta1→ ⟨E',(h1', Map.empty)⟩" by auto
from fv fv_collapse[OF icl, of e'] fold feq have "fv e1 = {}" by(auto)
with red_dom_lcl[OF red] x1 have x1': "x1' = Map.empty" by simp
from red_red0_tabisim0[OF wf red'] obtain ta2
where red'': "extTA2J0 P,P,t ⊢ ⟨e',(h1, Map.empty)⟩ -ta2→ ⟨E',(h1', Map.empty)⟩"
and tasim: "ta_bisim0 ta1 ta2" by auto
from τ fold feq icl nfin have "¬ τmove0 P h1 e'" by(simp add: collapse_τmove0_inv)
hence "∀aMvs. call e' = ⌊aMvs⌋ ⟶ synthesized_call P h1 aMvs"
by(auto dest: τmove0_callD)
with red'' have red''': "P,t ⊢0 ⟨e'/es', h1⟩ -ta2→ ⟨E'/es', h1'⟩" by(rule red0Red)
moreover from τ fold feq icl nfin have "¬ τmove0 P h1 e'" by(simp add: collapse_τmove0_inv)
hence "¬ τMOVE0 P ((e', es'), h1) ta2 ((E', es'), h1')" using nfin by auto
moreover from red''' wf_state' have "wf_state (E', es')" by(rule red0_preserves_wf_state[OF wf])
hence "bisim_red_red0 s1' ((E', es'), h1')" unfolding s1' e1' x1' by(auto)
ultimately show "∃s2' s2'' ta2. red0_mthr.silent_moves P t s2 s2' ∧ mred0 P t s2' ta2 s2'' ∧
¬ τMOVE0 P s2' ta2 s2'' ∧ bisim_red_red0 s1' s2'' ∧ ta_bisim0 ta1 ta2"
using tasim red1' heap unfolding s1' s2 by -(rule exI conjI|assumption|auto)+
next
fix s1 s2 ta2 s2'
assume "bisim_red_red0 s1 s2" and "mred0 P t s2 ta2 s2'" "¬ τMOVE0 P s2 ta2 s2'"
from red_simulates_red0[OF wf this]
show "∃s1' s1'' ta1. red_mthr.silent_moves P t s1 s1' ∧ mred P t s1' ta1 s1'' ∧
¬ τMOVE P s1' ta1 s1'' ∧ bisim_red_red0 s1'' s2' ∧ ta_bisim0 ta1 ta2"
by(blast intro: rtranclp.rtrancl_refl)
qed
lemma delay_bisimulation_diverge_red_red0:
assumes "wwf_J_prog P"
shows "delay_bisimulation_diverge (mred P t) (mred0 P t) bisim_red_red0 ta_bisim0 (τMOVE P) (τMOVE0 P)"
proof -
interpret delay_bisimulation_measure
"mred P t" "mred0 P t" "bisim_red_red0" "ta_bisim0" "τMOVE P" "τMOVE0 P"
"λe e'. False" "λ((e, es), h) ((e, es'), h). length es < length es'"
using assms by(rule delay_bisimulation_measure_red_red0)
show ?thesis by unfold_locales
qed
lemma bisim_red_red0_finalD:
assumes bisim: "bisim_red_red0 (x1, m1) (x2, m2)"
and "final_expr x1"
shows "∃x2'. red0_mthr.silent_moves P t (x2, m2) (x2', m2) ∧ bisim_red_red0 (x1, m1) (x2', m2) ∧ final_expr0 x2'"
proof -
from bisim
obtain e' e es where wf_state: "wf_state (e, es)"
and [simp]: "x1 = (e', Map.empty)" "x2 = (e, es)" "e' = collapse (e, es)" "m2 = m1"
by cases(cases x2, auto)
from ‹final_expr x1› have "final (collapse (e, es))" by simp
moreover from wf_state have "∀e∈set es. is_call e" by auto
ultimately have "red0_mthr.silent_moves P t ((e, es), m1) ((collapse (e, es), []), m1)"
proof(induction es arbitrary: e)
case Nil thus ?case by simp
next
case (Cons e' es)
from ‹final (collapse (e, e' # es))› have "final (collapse (inline_call e e', es))" by simp
moreover from ‹∀e∈set (e' # es). is_call e› have "∀e∈set es. is_call e" by simp
ultimately have "red0_mthr.silent_moves P t ((inline_call e e', es), m1) ((collapse (inline_call e e', es), []), m1)"
by(rule Cons.IH)
moreover from ‹final (collapse (e, e' # es))› ‹∀e∈set (e' # es). is_call e›
have "final e" by(rule collapse_finalD)
hence "P,t ⊢0 ⟨e/e'#es, m1⟩ -ε→ ⟨inline_call e e'/es, m1⟩" by(rule red0Return)
with ‹final e› have "red0_mthr.silent_move P t ((e, e'#es), m1) ((inline_call e e', es), m1)" by auto
ultimately show ?case by -(erule converse_rtranclp_into_rtranclp, simp)
qed
moreover have "bisim_red_red0 ((collapse (e, es), Map.empty), m1) ((collapse (e, es), []), m1)"
using ‹final (collapse (e, es))› by(auto intro!: bisim_red_red0I)
ultimately show ?thesis using ‹final (collapse (e, es))› by auto
qed
lemma red0_simulates_red_not_final:
assumes wwf: "wwf_J_prog P"
assumes bisim: "bisim_red_red0 ((e, xs), h) ((e0, es0), h0)"
and red: "P,t ⊢ ⟨e, (h, xs)⟩ -ta→ ⟨e', (h', xs')⟩"
and fin: "¬ final e0"
and nτ: "¬ τmove0 P h e"
shows "∃e0' ta0. P,t ⊢0 ⟨e0/es0, h⟩ -ta0→ ⟨e0'/es0, h'⟩ ∧ bisim_red_red0 ((e', xs'), h') ((e0', es0), h') ∧ ta_bisim0 ta ta0"
proof -
from bisim have [simp]: "xs = Map.empty" "h0 = h" and e: "e = collapse (e0, es0)"
and wfs: "wf_state (e0, es0)" by(auto elim!: bisim_red_red0.cases)
with red have "P,t ⊢ ⟨collapse (e0, es0), (h, Map.empty)⟩ -ta→ ⟨e', (h', xs')⟩" by simp
from wfs red_fold_exs'[OF this] fin obtain e0' where e': "e' = collapse (e0', es0)"
and red': "P,t ⊢ ⟨e0,(h, Map.empty)⟩ -ta→ ⟨e0',(h', Map.empty)⟩" by(auto)
from wfs fv_collapse[of es0, of e0] e have "fv e = {}" by(auto)
with red_dom_lcl[OF red] have [simp]: "xs' = Map.empty" by simp
from red_red0_tabisim0[OF wwf red'] obtain ta0
where red'': "extTA2J0 P,P,t ⊢ ⟨e0,(h, Map.empty)⟩ -ta0→ ⟨e0',(h', Map.empty)⟩"
and tasim: "ta_bisim0 ta ta0" by auto
from nτ e wfs fin have "¬ τmove0 P h e0" by(auto simp add: collapse_τmove0_inv)
hence "∀aMvs. call e0 = ⌊aMvs⌋ ⟶ synthesized_call P h aMvs"
by(auto dest: τmove0_callD)
with red'' have red''': "P,t ⊢0 ⟨e0/es0, h⟩ -ta0→ ⟨e0'/es0, h'⟩" by(rule red0Red)
moreover from red''' wfs have "wf_state (e0', es0)" by(rule red0_preserves_wf_state[OF wwf])
hence "bisim_red_red0 ((e', xs'), h') ((e0', es0), h')" unfolding e' by(auto)
ultimately show ?thesis using tasim by(auto simp del: split_paired_Ex)
qed
lemma red_red0_FWbisim:
assumes wf: "wwf_J_prog P"
shows "FWdelay_bisimulation_diverge final_expr (mred P) final_expr0 (mred0 P)
(λt. bisim_red_red0) (λexs (e0, es0). ¬ final e0) (τMOVE P) (τMOVE0 P)"
proof -
interpret delay_bisimulation_diverge "mred P t" "mred0 P t" "bisim_red_red0" "ta_bisim0" "τMOVE P" "τMOVE0 P"
for t by(rule delay_bisimulation_diverge_red_red0[OF wf])
show ?thesis
proof
fix t and s1 :: "(('addr expr × 'addr locals) × 'heap)" and s2 :: "(('addr expr × 'addr expr list) × 'heap)"
assume "bisim_red_red0 s1 s2" "(λ(x1, m). final_expr x1) s1"
moreover obtain x1 m1 where [simp]: "s1 = (x1, m1)" by(cases s1)
moreover obtain x2 m2 where [simp]: "s2 = (x2, m2)" by(cases s2)
ultimately have "bisim_red_red0 (x1, m1) (x2, m2)" "final_expr x1" by simp_all
from bisim_red_red0_finalD[OF this, of P t]
show "∃s2'. red0_mthr.silent_moves P t s2 s2' ∧ bisim_red_red0 s1 s2' ∧ (λ(x2, m). final_expr0 x2) s2'" by auto
next
fix t and s1 :: "(('addr expr × 'addr locals) × 'heap)" and s2 :: "(('addr expr × 'addr expr list) × 'heap)"
assume "bisim_red_red0 s1 s2" "(λ(x2, m). final_expr0 x2) s2"
moreover obtain x1 m1 where [simp]: "s1 = (x1, m1)" by(cases s1)
moreover obtain x2 m2 where [simp]: "s2 = (x2, m2)" by(cases s2)
ultimately have "bisim_red_red0 (x1, m1) (x2, m2)" "final_expr0 x2" by simp_all
moreover hence "final_expr x1" by(rule bisim_red_red0_final0D)
ultimately show "∃s1'. red_mthr.silent_moves P t s1 s1' ∧ bisim_red_red0 s1' s2 ∧ (λ(x1, m). final_expr x1) s1'" by auto
next
fix t' x m1 xx m2 t x1 x2 x1' ta1 x1'' m1' x2' ta2 x2'' m2'
assume b: "bisim_red_red0 (x, m1) (xx, m2)" and bo: "bisim_red_red0 (x1, m1) (x2, m2)"
and "red_mthr.silent_moves P t (x1, m1) (x1', m1)"
and red1: "mred P t (x1', m1) ta1 (x1'', m1')" and "¬ τMOVE P (x1', m1) ta1 (x1'', m1')"
and "red0_mthr.silent_moves P t (x2, m2) (x2', m2)"
and red2: "mred0 P t (x2', m2) ta2 (x2'', m2')" and "¬ τMOVE0 P (x2', m2) ta2 (x2'', m2')"
and bo': "bisim_red_red0 (x1'', m1') (x2'', m2')"
and tb: "ta_bisim0 ta1 ta2"
from b have "m1 = m2" by(auto elim: bisim_red_red0.cases)
moreover from bo' have "m1' = m2'" by(auto elim: bisim_red_red0.cases)
ultimately show "bisim_red_red0 (x, m1') (xx, m2')" using b
by(auto elim: bisim_red_red0.cases)
next
fix t x1 m1 x2 m2 x1' ta1 x1'' m1' x2' ta2 x2'' m2' w
assume b: "bisim_red_red0 (x1, m1) (x2, m2)"
and "red_mthr.silent_moves P t (x1, m1) (x1', m1)"
and red1: "mred P t (x1', m1) ta1 (x1'', m1')" and "¬ τMOVE P (x1', m1) ta1 (x1'', m1')"
and "red0_mthr.silent_moves P t (x2, m2) (x2', m2)"
and red2: "mred0 P t (x2', m2) ta2 (x2'', m2')" and "¬ τMOVE0 P (x2', m2) ta2 (x2'', m2')"
and b': "bisim_red_red0 (x1'', m1') (x2'', m2')" and "ta_bisim0 ta1 ta2"
and Suspend: "Suspend w ∈ set ⦃ta1⦄⇘w⇙" "Suspend w ∈ set ⦃ta2⦄⇘w⇙"
hence "(λexs (e0, es0). is_call e0) x1'' x2''"
by(cases x1')(cases x2', auto dest: Red_Suspend_is_call simp add: final_iff)
thus "(λexs (e0, es0). ¬ final e0) x1'' x2''" by(auto simp add: final_iff is_call_def)
next
fix t x1 m1 x2 m2 ta1 x1' m1'
assume b: "bisim_red_red0 (x1, m1) (x2, m2)"
and c: "(λ(e0, es0). ¬ final e0) x2"
and red1: "mred P t (x1, m1) ta1 (x1', m1')"
and wakeup: "Notified ∈ set ⦃ta1⦄⇘w⇙ ∨ WokenUp ∈ set ⦃ta1⦄⇘w⇙"
from c have "¬ final (fst x2)" by(auto simp add: is_call_def)
moreover from red1 wakeup have "¬ τmove0 P m1 (fst x1)"
by(cases x1)(auto dest: red_τ_taD[where extTA="extTA2J P", simplified] simp add: ta_upd_simps)
moreover from b have "m2 = m1" by(cases) auto
ultimately obtain e0' ta0 where "P,t ⊢0 ⟨fst x2/snd x2,m2⟩ -ta0→ ⟨e0'/snd x2,m1'⟩"
"bisim_red_red0 ((fst x1', snd x1'), m1') ((e0', snd x2), m1')" "ta_bisim0 ta1 ta0"
using red0_simulates_red_not_final[OF wf, of "fst x1" "snd x1" m1 "fst x2" "snd x2" m2 t ta1 "fst x1'" m1' "snd x1'"]
using b red1 by(auto simp add: split_beta)
thus "∃ta2 x2' m2'. mred0 P t (x2, m2) ta2 (x2', m2') ∧ bisim_red_red0 (x1', m1') (x2', m2') ∧ ta_bisim0 ta1 ta2"
by(cases ta0)(fastforce simp add: split_beta)
next
fix t x1 m1 x2 m2 ta2 x2' m2'
assume b: "bisim_red_red0 (x1, m1) (x2, m2)"
and c: "(λ(e0, es0). ¬ final e0) x2"
and red2: "mred0 P t (x2, m2) ta2 (x2', m2')"
and wakeup: "Notified ∈ set ⦃ta2⦄⇘w⇙ ∨ WokenUp ∈ set ⦃ta2⦄⇘w⇙"
from b have [simp]: "m1 = m2" by cases auto
with red_simulates_red0[OF wf b red2] wakeup obtain s1' ta1
where "mred P t (x1, m1) ta1 s1'" "bisim_red_red0 s1' (x2', m2')" "ta_bisim0 ta1 ta2"
by(fastforce simp add: split_paired_Ex)
moreover from ‹bisim_red_red0 s1' (x2', m2')› have "m2' = snd s1'" by cases auto
ultimately
show "∃ta1 x1' m1'. mred P t (x1, m1) ta1 (x1', m1') ∧ bisim_red_red0 (x1', m1') (x2', m2') ∧ ta_bisim0 ta1 ta2"
by(cases ta1)(fastforce simp add: split_beta)
next
show "(∃x. final_expr x) ⟷ (∃x. final_expr0 x)"
by(auto simp add: final_iff)
qed
qed
end
sublocale J_heap_base < red_red0:
FWdelay_bisimulation_base
final_expr
"mred P"
final_expr0
"mred0 P"
convert_RA
"λt. bisim_red_red0"
"λexs (e0, es0). ¬ final e0"
"τMOVE P" "τMOVE0 P"
for P
by(unfold_locales)
context J_heap_base begin
lemma bisim_J_J0_start:
assumes wf: "wwf_J_prog P"
and wf_start: "wf_start_state P C M vs"
shows "red_red0.mbisim (J_start_state P C M vs) (J0_start_state P C M vs)"
proof -
from wf_start obtain Ts T pns body D
where sees: "P ⊢ C sees M:Ts→T=⌊(pns,body)⌋ in D"
and conf: "P,start_heap ⊢ vs [:≤] Ts"
by cases auto
from conf have vs: "length vs = length Ts" by(rule list_all2_lengthD)
from sees_wf_mdecl[OF wf sees]
have wwfCM: "wwf_J_mdecl P D (M, Ts, T, pns, body)"
and len: "length pns = length Ts" by(auto simp add: wf_mdecl_def)
from wwfCM have fvbody: "fv body ⊆ {this} ∪ set pns"
and pns: "length pns = length Ts" by simp_all
with vs len have fv: "fv (blocks pns Ts vs body) ⊆ {this}" by auto
with len vs sees show ?thesis unfolding start_state_def
by(auto intro!: red_red0.mbisimI)(auto intro!: bisim_red_red0.intros wset_thread_okI simp add: is_call_def split: if_split_asm)
qed
end
end