# Theory ExternalCall

```(*  Title:      JinjaThreads/Common/ExternalCall.thy
Author:     Andreas Lochbihler
*)

section ‹Semantics of method calls that cannot be defined inside JinjaThreads›

theory ExternalCall
imports
"../Framework/FWSemantics"
Conform
begin

type_synonym

(* pretty printing for external_thread_action type *)
print_translation ‹
let
fun tr'
[a1, t
, Const (@{type_syntax "prod"}, _) \$ Const (@{type_syntax "String.literal"}, _) \$
(Const (@{type_syntax "prod"}, _) \$ Const (@{type_syntax "String.literal"}, _) \$ a2)
, h] =
if a1 = a2 then Syntax.const @{type_syntax "external_thread_action"} \$ a1 \$ t \$ h
else raise Match;
end
›

subsection ‹Typing of external calls›

inductive external_WT_defs :: "cname ⇒ mname ⇒ ty list ⇒ ty ⇒ bool" ("(_∙_'(_')) :: _" [50, 0, 0, 50] 60)
where
| "Object∙wait([]) :: Void"
| "Object∙notify([]) :: Void"
| "Object∙notifyAll([]) :: Void"
| "Object∙clone([]) :: Class Object"
| "Object∙hashcode([]) :: Integer"
| "Object∙print([Integer]) :: Void"
| "Object∙interrupted([]) :: Boolean"
| "Object∙yield([]) :: Void"

inductive_cases external_WT_defs_cases:
"a∙start(vs) :: T"
"a∙join(vs) :: T"
"a∙interrupt(vs) :: T"
"a∙isInterrupted(vs) :: T"
"a∙wait(vs) :: T"
"a∙notify(vs) :: T"
"a∙notifyAll(vs) :: T"
"a∙clone(vs) :: T"
"a∙hashcode(vs) :: T"
"a∙print(vs) :: T"
"a∙interrupted([]) :: T"
"a∙yield(vs) :: T"

inductive is_native :: "'m prog ⇒ htype ⇒ mname ⇒ bool"
for P :: "'m prog" and hT :: htype and M :: mname
where "⟦ P ⊢ class_type_of hT sees M:Ts→T = Native in D; D∙M(Ts) :: T ⟧ ⟹ is_native P hT M"

lemma is_nativeD: "is_native P hT M ⟹ ∃Ts T D. P ⊢ class_type_of hT sees M:Ts→T = Native in D ∧ D∙M(Ts)::T"

inductive (in heap_base) external_WT' :: "'m prog ⇒ 'heap ⇒ 'addr ⇒ mname ⇒ 'addr val list ⇒ ty ⇒ bool"
("_,_ ⊢ (_∙_'(_')) : _" [50,0,0,0,50] 60)
for P :: "'m prog" and h :: 'heap and a :: 'addr and M :: mname and vs :: "'addr val list" and U :: ty
where
"⟦ typeof_addr h a = ⌊hT⌋; map typeof⇘h⇙ vs = map Some Ts; P ⊢ class_type_of hT sees M:Ts'→U = Native in D;
P ⊢ Ts [≤] Ts' ⟧
⟹ P,h ⊢ a∙M(vs) : U"

context heap_base begin

lemma external_WT'_iff:
"P,h ⊢ a∙M(vs) : U ⟷
(∃hT Ts Ts' D. typeof_addr h a = ⌊hT⌋ ∧ map typeof⇘h⇙ vs = map Some Ts ∧ P ⊢ class_type_of hT sees M:Ts'→U=Native in D ∧ P ⊢ Ts [≤] Ts')"

end

context heap begin

lemma external_WT'_hext_mono:
"⟦ P,h ⊢ a∙M(vs) : T; h ⊴ h' ⟧ ⟹ P,h' ⊢ a∙M(vs) : T"

end

subsection ‹Semantics of external calls›

| RetStaySame

lemma rec_extCallRet [simp]: "rec_extCallRet = case_extCallRet"
by(auto simp add: fun_eq_iff split: extCallRet.split)

context heap_base begin

abbreviation RetEXC :: "cname ⇒ 'addr extCallRet"
where "RetEXC C ≡ RetExc (addr_of_sys_xcpt C)"

where
"⟦ heap_read h a al v; heap_write h a' al v h' ⟧
⟹ heap_copy_loc a a' al h ([ReadMem a al v, WriteMem a' al v]) h'"

where
Nil: "heap_copies a a' [] h [] h"
| Cons:
"⟦ heap_copy_loc a a' al h ob h'; heap_copies a a' als h' obs h'' ⟧
⟹ heap_copies a a' (al # als) h (ob @ obs) h''"

inductive_cases heap_copies_cases:
"heap_copies a a' [] h ops h'"
"heap_copies a a' (al#als) h ops h'"

text ‹
Contrary to Sun's JVM 1.6.0\_07, cloning an interrupted thread does not yield an interrupted thread,
because the interrupt flag is not stored inside the thread object.
Starting a clone of a started thread with Sun JVM 1.6.0\_07 raises an illegal thread state exception,
The thread at @{url "http://mail.openjdk.java.net/pipermail/core-libs-dev/2010-August/004715.html"} discusses
the general problem of thread cloning and argues against that.
The bug report @{url "http://bugs.sun.com/bugdatabase/view_bug.do?bug_id=6968584"}
such that \texttt{Object.clone()} can no longer be accessed for Thread and subclasses in Java 7.

Array cells are never volatile themselves.
›

for P :: "'m prog" and h :: 'heap and a :: 'addr
where
CloneFail:
"⟦ typeof_addr h a = ⌊hT⌋; allocate h hT = {} ⟧
⟹ heap_clone P h a h None"
| ObjClone:
"⟦ typeof_addr h a = ⌊Class_type C⌋; (h', a') ∈ allocate h (Class_type C);
P ⊢ C has_fields FDTs; heap_copies a a' (map (λ((F, D), Tfm). CField D F) FDTs) h' obs h'' ⟧
⟹ heap_clone P h a h'' ⌊(NewHeapElem a' (Class_type C) # obs, a')⌋"
| ArrClone:
"⟦ typeof_addr h a = ⌊Array_type T n⌋; (h', a') ∈ allocate h (Array_type T n); P ⊢ Object has_fields FDTs;
heap_copies a a' (map (λ((F, D), Tfm). CField D F) FDTs @ map ACell [0..<n]) h' obs  h'' ⟧
⟹ heap_clone P h a h'' ⌊(NewHeapElem a' (Array_type T n) # obs, a')⌋"

inductive red_external ::
and red_external_syntax ::
("_,_ ⊢ (⟨(_∙_'(_')),/_⟩) -_→ext (⟨(_),/(_)⟩)" [50, 0, 0, 0, 0, 0, 0, 0, 0] 51)
for P :: "'m prog" and t :: 'thread_id and h :: 'heap and a :: 'addr
where
"P,t ⊢ ⟨a∙M(vs), h⟩ -ta→ext ⟨va, h'⟩ ≡ red_external P t h a M vs ta va h'"

"⟦ typeof_addr h a = ⌊Class_type C⌋; P ⊢ C ≼⇧* Thread ⟧

"⟦ typeof_addr h a = ⌊Class_type C⌋; P ⊢ C ≼⇧* Thread ⟧

| RedJoin:
"⟦ typeof_addr h a = ⌊Class_type C⌋; P ⊢ C ≼⇧* Thread ⟧

| RedJoinInterrupt:
"⟦ typeof_addr h a = ⌊Class_type C⌋; P ⊢ C ≼⇧* Thread ⟧
⟹ P,t ⊢ ⟨a∙join([]), h⟩ -⦃IsInterrupted t True, ClearInterrupt t, ObsInterrupted t⦄→ext ⟨RetEXC InterruptedException, h⟩"

― ‹Interruption should produce inter-thread actions (JLS 17.4.4) for the synchronizes-with order.
They should synchronize with the inter-thread actions that determine whether a thread has been interrupted.
Hence, interruption generates an @{term "ObsInterrupt"} action.

Although @{term WakeUp} causes the interrupted thread to raise an @{term InterruptedException}
independent of the interrupt status, the interrupt flag must be set with @{term "Interrupt"}
while it competes for the monitor lock again.

Interrupting a thread which has not yet been started does not set the interrupt flag
(tested with Sun HotSpot JVM 1.6.0\_07).›

| RedInterrupt:
"⟦ typeof_addr h a = ⌊Class_type C⌋; P ⊢ C ≼⇧* Thread ⟧
⟹ P,t ⊢ ⟨a∙interrupt([]), h⟩
⟨RetVal Unit, h⟩"

| RedInterruptInexist:
"⟦ typeof_addr h a = ⌊Class_type C⌋; P ⊢ C ≼⇧* Thread ⟧
⟹ P,t ⊢ ⟨a∙interrupt([]), h⟩
⟨RetVal Unit, h⟩"

| RedIsInterruptedTrue:
"⟦ typeof_addr h a = ⌊Class_type C⌋; P ⊢ C ≼⇧* Thread ⟧
⟨RetVal (Bool True), h⟩"

| RedIsInterruptedFalse:
"⟦ typeof_addr h a = ⌊Class_type C⌋; P ⊢ C ≼⇧* Thread ⟧
⟹ P,t ⊢ ⟨a∙isInterrupted([]), h⟩ -⦃IsInterrupted (addr2thread_id a) False⦄→ext ⟨RetVal (Bool False), h⟩"

― ‹The JLS leaves unspecified whether @{term wait} first checks for the monitor state
(whether the thread holds a lock on the monitor) or for the interrupt flag of the current thread.
Sun Hotspot JVM 1.6.0\_07 seems to check for the monitor state first, so we do it here, too.›
| RedWaitInterrupt:
"P,t ⊢ ⟨a∙wait([]), h⟩ -⦃Unlock→a, Lock→a, IsInterrupted t True, ClearInterrupt t, ObsInterrupted t⦄ →ext
⟨RetEXC InterruptedException, h⟩"

| RedWait:
"P,t ⊢ ⟨a∙wait([]), h⟩ -⦃Suspend a, Unlock→a, Lock→a, ReleaseAcquire→a, IsInterrupted t False, SyncUnlock a ⦄→ext
⟨RetStaySame, h⟩"

| RedWaitFail:
"P,t ⊢ ⟨a∙wait([]), h⟩ -⦃UnlockFail→a⦄→ext ⟨RetEXC IllegalMonitorState, h⟩"

| RedWaitNotified:
"P,t ⊢ ⟨a∙wait([]), h⟩ -⦃Notified⦄→ext ⟨RetVal Unit, h⟩"

― ‹This rule does NOT check that the interrupted flag is set, but still clears it.
The semantics will be that only the executing thread clears its interrupt.›
| RedWaitInterrupted:
"P,t ⊢ ⟨a∙wait([]), h⟩ -⦃WokenUp, ClearInterrupt t, ObsInterrupted t⦄→ext ⟨RetEXC InterruptedException, h⟩"

― ‹Calls to wait may decide to immediately wake up spuriously. This is
indistinguishable from waking up spuriously any time before being
notified or interrupted. Spurious wakeups are configured by the
@{term spurious_wakeup} parameter of the @{term heap_base} locale.›
| RedWaitSpurious:
"spurious_wakeups ⟹
P,t ⊢ ⟨a∙wait([]), h⟩ -⦃Unlock→a, Lock→a, ReleaseAcquire→a, IsInterrupted t False, SyncUnlock a⦄ →ext
⟨RetVal Unit, h⟩"

― ‹@{term notify} and @{term notifyAll} do not perform synchronization inter-thread actions
because they only tests whether the thread holds a lock, but do not change the lock state.›

| RedNotify:
"P,t ⊢ ⟨a∙notify([]), h⟩ -⦃Notify a, Unlock→a, Lock→a⦄→ext ⟨RetVal Unit, h⟩"

| RedNotifyFail:
"P,t ⊢ ⟨a∙notify([]), h⟩ -⦃UnlockFail→a⦄→ext ⟨RetEXC IllegalMonitorState, h⟩"

| RedNotifyAll:
"P,t ⊢ ⟨a∙notifyAll([]), h⟩ -⦃NotifyAll a, Unlock→a, Lock→a⦄→ext ⟨RetVal Unit, h⟩"

| RedNotifyAllFail:
"P,t ⊢ ⟨a∙notifyAll([]), h⟩ -⦃UnlockFail→a⦄→ext ⟨RetEXC IllegalMonitorState, h⟩"

| RedClone:
"heap_clone P h a h' ⌊(obs, a')⌋
⟹ P,t ⊢ ⟨a∙clone([]), h⟩ -(K\$ [], [], [], [], [], obs)→ext ⟨RetVal (Addr a'), h'⟩"

| RedCloneFail:
"heap_clone P h a h' None ⟹ P,t ⊢ ⟨a∙clone([]), h⟩ -ε→ext ⟨RetEXC OutOfMemory, h'⟩"

| RedHashcode:
"P,t ⊢ ⟨a∙hashcode([]), h⟩ -⦃⦄→ext ⟨RetVal (Intg (word_of_int (hash_addr a))), h⟩"

| RedPrint:
"P,t ⊢ ⟨a∙print(vs), h⟩ -⦃ExternalCall a print vs Unit⦄→ext ⟨RetVal Unit, h⟩"

| RedInterruptedTrue:
"P,t ⊢ ⟨a∙interrupted([]), h⟩ -⦃IsInterrupted t True, ClearInterrupt t, ObsInterrupted t⦄→ext ⟨RetVal (Bool True), h⟩"

| RedInterruptedFalse:
"P,t ⊢ ⟨a∙interrupted([]), h⟩ -⦃IsInterrupted t False⦄→ext ⟨RetVal (Bool False), h⟩"

| RedYield:
"P,t ⊢ ⟨a∙yield([]), h⟩ -⦃Yield⦄→ext ⟨RetVal Unit, h⟩"

subsection ‹Aggressive formulation for external cals›

definition red_external_aggr ::
where
"red_external_aggr P t a M vs h =
(if M = wait then
in {(⦃Unlock→a, Lock→a, IsInterrupted t True, ClearInterrupt t, ObsInterrupted t⦄, RetEXC InterruptedException, h),
(⦃Suspend a, Unlock→a, Lock→a, ReleaseAcquire→a, IsInterrupted t False, SyncUnlock a⦄, RetStaySame, h),
(⦃UnlockFail→a⦄, RetEXC IllegalMonitorState, h),
(⦃Notified⦄, RetVal Unit, h),
(⦃WokenUp, ClearInterrupt t, ObsInterrupted t⦄, RetEXC InterruptedException, h)} ∪
(if spurious_wakeups then {(⦃Unlock→a, Lock→a, ReleaseAcquire→a, IsInterrupted t False, SyncUnlock a⦄, RetVal Unit, h)} else {})
else if M = notify then {(⦃Notify a, Unlock→a, Lock→a⦄, RetVal Unit, h),
(⦃UnlockFail→a⦄, RetEXC IllegalMonitorState, h)}
else if M = notifyAll then {(⦃NotifyAll a, Unlock→a, Lock→a ⦄, RetVal Unit, h),
(⦃UnlockFail→a⦄, RetEXC IllegalMonitorState, h)}
else if M = clone then
{((K\$ [], [], [], [], [], obs), RetVal (Addr a'), h')|obs a' h'. heap_clone P h a h' ⌊(obs, a')⌋}
∪ {(⦃⦄, RetEXC OutOfMemory, h')|h'. heap_clone P h a h' None}
else if M = hashcode then {(⦃⦄, RetVal (Intg (word_of_int (hash_addr a))), h)}
else if M = print then {(⦃ExternalCall a M vs Unit⦄, RetVal Unit, h)}
else if M = interrupted then {(⦃IsInterrupted t True, ClearInterrupt t, ObsInterrupted t⦄, RetVal (Bool True), h),
(⦃IsInterrupted t False⦄, RetVal (Bool False), h)}
else if M = yield then {(⦃Yield⦄, RetVal Unit, h)}
else
let hT = the (typeof_addr h a)
in if P ⊢ ty_of_htype hT ≤ Class Thread then
in if M = start then
{(⦃NewThread t_a (the_Class (ty_of_htype hT), run, a) h, ThreadStart t_a⦄, RetVal Unit, h),
else if M = join then
{(⦃Join t_a, IsInterrupted t False, ThreadJoin t_a⦄, RetVal Unit, h),
(⦃IsInterrupted t True, ClearInterrupt t, ObsInterrupted t⦄, RetEXC InterruptedException, h)}
else if M = interrupt then
{(⦃ThreadExists t_a True, WakeUp t_a, Interrupt t_a, ObsInterrupt t_a⦄, RetVal Unit, h),
(⦃ThreadExists t_a False⦄, RetVal Unit, h)}
else if M = isInterrupted then
{(⦃IsInterrupted t_a False⦄, RetVal (Bool False), h),
(⦃IsInterrupted t_a True, ObsInterrupted t_a⦄, RetVal (Bool True), h)}
else {(⦃⦄, undefined)}
else {(⦃⦄, undefined)})"

lemma red_external_imp_red_external_aggr:
"P,t ⊢ ⟨a∙M(vs), h⟩ -ta→ext ⟨va, h'⟩ ⟹ (ta, va, h') ∈ red_external_aggr P t a M vs h"
unfolding red_external_aggr_def
by(auto elim!: red_external.cases split del: if_split simp add: split_beta)

end

context heap begin

lemma hext_heap_copy_loc:
"heap_copy_loc a a' al h obs h' ⟹ h ⊴ h'"
by(blast elim: heap_copy_loc.cases dest: hext_heap_ops)

lemma hext_heap_copies:
assumes "heap_copies a a' als h obs h'"
shows "h ⊴ h'"
using assms by induct(blast intro: hext_heap_copy_loc hext_trans)+

lemma hext_heap_clone:
assumes "heap_clone P h a h' res"
shows "h ⊴ h'"
using assms by(blast elim: heap_clone.cases dest: hext_heap_ops hext_heap_copies intro: hext_trans)

theorem red_external_hext:
assumes "P,t ⊢ ⟨a∙M(vs), h⟩ -ta→ext ⟨va, h'⟩"
shows "hext h h'"
using assms
by(cases)(blast intro: hext_heap_ops hext_heap_clone)+

lemma red_external_preserves_tconf:
"⟦ P,t ⊢ ⟨a∙M(vs), h⟩ -ta→ext ⟨va, h'⟩; P,h ⊢ t' √t ⟧ ⟹ P,h' ⊢ t' √t"
by(drule red_external_hext)(rule tconf_hext_mono)

end

context heap_conf begin

assumes "heap_clone P h a h' ⌊(obs, a')⌋"
and "hconf h"
using assms

end

context heap_base begin

"⟦ P,t ⊢ ⟨a∙M(vs), h⟩ -ta→ext ⟨va, h'⟩; NewThread t' ex h'' ∈ set ⦃ta⦄⇘t⇙ ⟧ ⟹ h'' = h'"
by(auto elim: red_external.cases simp add: ta_upd_simps)

"⟦ (ta, va, h') ∈ red_external_aggr P t a M vs h; NewThread t' ex h'' ∈ set ⦃ta⦄⇘t⇙ ⟧ ⟹ h'' = h'"
by(auto simp add: red_external_aggr_def is_native.simps split_beta ta_upd_simps split: if_split_asm)

end

"⟦ P,t ⊢ ⟨a∙M(vs), h⟩ -ta→ext ⟨va, h'⟩; NewThread t' x h'' ∈ set ⦃ta⦄⇘t⇙ ⟧
by(auto elim!: red_external.cases dest!: Array_widen simp add: ta_upd_simps)

"⟦ (ta, va, h') ∈ red_external_aggr P t a M vs h; typeof_addr h a ≠ None;
NewThread t' x h'' ∈ set ⦃ta⦄⇘t⇙ ⟧
by(auto simp add: red_external_aggr_def is_native.simps split_beta ta_upd_simps widen_Class split: if_split_asm dest!: Array_widen)

end

context heap begin

lemma red_external_aggr_hext:
"⟦ (ta, va, h') ∈ red_external_aggr P t a M vs h; is_native P (the (typeof_addr h a)) M ⟧ ⟹ h ⊴ h'"
apply(auto simp add: red_external_aggr_def split_beta is_native.simps elim!: external_WT_defs_cases hext_heap_clone split: if_split_asm)
apply(auto elim!: external_WT_defs.cases dest!: sees_method_decl_above intro: widen_trans simp add: class_type_of_eq split: htype.split_asm)
done

lemma red_external_aggr_preserves_tconf:
"⟦ (ta, va, h') ∈ red_external_aggr P t a M vs h; is_native P (the (typeof_addr h a)) M; P,h ⊢ t' √t ⟧
⟹ P,h' ⊢ t' √t"
by(blast dest: red_external_aggr_hext intro: tconf_hext_mono)

end

context heap_base begin

lemma red_external_Wakeup_no_Join_no_Lock_no_Interrupt:
"⟦ P,t ⊢ ⟨a∙M(vs), h⟩ -ta→ext ⟨va, h'⟩; Notified ∈ set ⦃ta⦄⇘w⇙ ∨ WokenUp ∈ set ⦃ta⦄⇘w⇙ ⟧ ⟹
collect_locks ⦃ta⦄⇘l⇙ = {} ∧ collect_cond_actions ⦃ta⦄⇘c⇙ = {} ∧ collect_interrupts ⦃ta⦄⇘i⇙ = {}"
by(auto elim!: red_external.cases simp add: ta_upd_simps collect_locks_def collect_interrupts_def)

lemma red_external_aggr_Wakeup_no_Join:
"⟦ (ta, va, h') ∈ red_external_aggr P t a M vs h;
Notified ∈ set ⦃ta⦄⇘w⇙ ∨ WokenUp ∈ set ⦃ta⦄⇘w⇙ ⟧
⟹ collect_locks ⦃ta⦄⇘l⇙ = {} ∧ collect_cond_actions ⦃ta⦄⇘c⇙ = {} ∧ collect_interrupts ⦃ta⦄⇘i⇙ = {}"
by(auto simp add: red_external_aggr_def split_beta ta_upd_simps collect_locks_def collect_interrupts_def split: if_split_asm)

lemma red_external_Suspend_StaySame:
"⟦ P,t ⊢ ⟨a∙M(vs), h⟩ -ta→ext ⟨va, h'⟩; Suspend w ∈ set ⦃ta⦄⇘w⇙ ⟧ ⟹ va = RetStaySame"
by(auto elim!: red_external.cases simp add: ta_upd_simps)

lemma red_external_aggr_Suspend_StaySame:
"⟦ (ta, va, h') ∈ red_external_aggr P t a M vs h; Suspend w ∈ set ⦃ta⦄⇘w⇙ ⟧ ⟹ va = RetStaySame"
by(auto simp add: red_external_aggr_def split_beta ta_upd_simps split: if_split_asm)

lemma red_external_Suspend_waitD:
"⟦ P,t ⊢ ⟨a∙M(vs), h⟩ -ta→ext ⟨va, h'⟩; Suspend w ∈ set ⦃ta⦄⇘w⇙ ⟧ ⟹ M = wait"
by(auto elim!: red_external.cases simp add: ta_upd_simps)

lemma red_external_aggr_Suspend_waitD:
"⟦ (ta, va, h') ∈ red_external_aggr P t a M vs h; Suspend w ∈ set ⦃ta⦄⇘w⇙ ⟧ ⟹ M = wait"
by(auto simp add: red_external_aggr_def split_beta ta_upd_simps split: if_split_asm)

"⟦ P,t ⊢ ⟨a∙M(vs), h⟩ -ta→ext ⟨va, h'⟩; NewThread t' (C, M', a') h'' ∈ set ⦃ta⦄⇘t⇙ ⟧
⟹ typeof_addr h' a' = ⌊Class_type C⌋ ∧ P ⊢ C ≼⇧* Thread ∧ M' = run"
by(auto elim!: red_external.cases simp add: widen_Class ta_upd_simps)

"⟦ (ta, va, h') ∈ red_external_aggr P t a M vs h; typeof_addr h a ≠ None;
NewThread t' (C, M', a') h'' ∈ set ⦃ta⦄⇘t⇙ ⟧
⟹ typeof_addr h' a' = ⌊Class_type C⌋ ∧ P ⊢ C ≼⇧* Thread ∧ M' = run"
by(auto simp add: red_external_aggr_def split_beta ta_upd_simps widen_Class split: if_split_asm dest!: Array_widen)

lemma heap_copy_loc_length:
assumes "heap_copy_loc a a' al h obs h'"
shows "length obs = 2"
using assms by(cases) simp

lemma heap_copies_length:
assumes "heap_copies a a' als h obs h'"
shows "length obs = 2 * length als"
using assms by(induct)(auto dest!: heap_copy_loc_length)

end

subsection ‹‹τ›-moves›

inductive τexternal_defs :: "cname ⇒ mname ⇒ bool"
where
"τexternal_defs Object hashcode"

definition τexternal :: "'m prog ⇒ htype ⇒ mname ⇒ bool"
where "τexternal P hT M ⟷ (∃Ts Tr D. P ⊢ class_type_of hT sees M:Ts→Tr = Native in D ∧ τexternal_defs D M)"

context heap_base begin

definition τexternal' :: "'m prog ⇒ 'heap ⇒ 'addr ⇒ mname ⇒ bool"
where "τexternal' P h a M ⟷ (∃hT. typeof_addr h a = Some hT ∧ τexternal P hT M)"

lemma τexternal'_red_external_heap_unchanged:
"⟦ P,t ⊢ ⟨a∙M(vs), h⟩ -ta→ext ⟨va, h'⟩; τexternal' P h a M ⟧ ⟹ h' = h"
by(auto elim!: red_external.cases τexternal_defs.cases simp add: τexternal_def τexternal'_def)

lemma τexternal'_red_external_aggr_heap_unchanged:
"⟦ (ta, va, h') ∈ red_external_aggr P t a M vs h; τexternal' P h a M ⟧ ⟹ h' = h"
by(auto elim!: τexternal_defs.cases simp add: τexternal_def τexternal'_def red_external_aggr_def)

lemma τexternal'_red_external_TA_empty:
"⟦ P,t ⊢ ⟨a∙M(vs), h⟩ -ta→ext ⟨va, h'⟩; τexternal' P h a M ⟧ ⟹ ta = ε"
by(auto elim!: red_external.cases τexternal_defs.cases simp add: τexternal_def τexternal'_def)

lemma τexternal'_red_external_aggr_TA_empty:
"⟦ (ta, va, h') ∈ red_external_aggr P t a M vs h; τexternal' P h a M ⟧ ⟹ ta = ε"
by(auto elim!: τexternal_defs.cases simp add: τexternal_def τexternal'_def red_external_aggr_def)

"⟦ P,t ⊢ ⟨a∙M(vs),h⟩ -ta→ext ⟨va,h'⟩; NewThread t (C, M, a') h'' ∈ set ⦃ta⦄⇘t⇙ ⟧
by(auto elim!: red_external.cases simp add: conf_def ta_upd_simps)

lemma τexternal_red_external_aggr_heap_unchanged:
"⟦ (ta, va, h') ∈ red_external_aggr P t a M vs h; τexternal P (the (typeof_addr h a)) M ⟧ ⟹ h' = h"
by(auto elim!: τexternal_defs.cases simp add: τexternal_def red_external_aggr_def)

lemma τexternal_red_external_aggr_TA_empty:
"⟦ (ta, va, h') ∈ red_external_aggr P t a M vs h; τexternal P (the (typeof_addr h a)) M ⟧ ⟹ ta = ε"
by(auto elim!: τexternal_defs.cases simp add: τexternal_def red_external_aggr_def)

end

subsection ‹Code generation›

code_pred
(modes:
i ⇒ i ⇒ i ⇒ i ⇒ bool,
i ⇒ i ⇒ i ⇒ o ⇒ bool,
i ⇒ i ⇒ o ⇒ o ⇒ bool,
o ⇒ i ⇒ o ⇒ o ⇒ bool)
external_WT_defs
.

code_pred
(modes: i ⇒ i ⇒ i ⇒ bool)
[inductify, skip_proof]
is_native
.

declare heap_base.heap_copy_loc.intros[code_pred_intro]

code_pred
(modes: (i ⇒ i ⇒ i ⇒ o ⇒ bool) ⇒ (i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ bool) ⇒ i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ o ⇒ bool)
heap_base.heap_copy_loc
proof -
case heap_copy_loc
from heap_copy_loc.prems show thesis
by(rule heap_base.heap_copy_loc.cases)(rule heap_copy_loc.that[OF refl refl refl refl refl refl])
qed

declare heap_base.heap_copies.intros [code_pred_intro]

code_pred
(modes: (i ⇒ i ⇒ i ⇒ o ⇒ bool) => (i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ bool) ⇒ i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ o ⇒ bool)
heap_base.heap_copies
proof -
case heap_copies
from heap_copies.prems show thesis
by(rule heap_base.heap_copies.cases)(erule (3) heap_copies.that[OF refl refl refl refl]|assumption)+
qed

declare heap_base.heap_clone.intros [folded Predicate_Compile.contains_def, code_pred_intro]

code_pred
(modes: i ⇒ i ⇒ (i ⇒ i ⇒ i ⇒ o ⇒ bool) ⇒ (i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ bool) ⇒ i ⇒ i ⇒ i ⇒ o ⇒ o ⇒ bool)
heap_base.heap_clone
proof -
case heap_clone
from heap_clone.prems show thesis
by(rule heap_base.heap_clone.cases[folded Predicate_Compile.contains_def])(erule (3) heap_clone.that[OF refl refl refl refl refl refl refl]|assumption)+
qed

text ‹
code\_pred in Isabelle2012 cannot handle boolean parameters as premises properly,
so this replacement rule explicitly tests for @{term "True"}
›

lemma (in heap_base) RedWaitSpurious_Code:
"spurious_wakeups = True ⟹
P,t ⊢ ⟨a∙wait([]),h⟩ -⦃Unlock→a, Lock→a, ReleaseAcquire→a, IsInterrupted t False, SyncUnlock a⦄→ext ⟨RetVal Unit,h⟩"
by(rule RedWaitSpurious) simp

lemmas [code_pred_intro] =
heap_base.RedJoin heap_base.RedJoinInterrupt
heap_base.RedInterrupt heap_base.RedInterruptInexist heap_base.RedIsInterruptedTrue heap_base.RedIsInterruptedFalse
heap_base.RedWaitInterrupt heap_base.RedWait heap_base.RedWaitFail heap_base.RedWaitNotified heap_base.RedWaitInterrupted
declare heap_base.RedWaitSpurious_Code [code_pred_intro RedWaitSpurious]
lemmas [code_pred_intro] =
heap_base.RedNotify heap_base.RedNotifyFail heap_base.RedNotifyAll heap_base.RedNotifyAllFail
heap_base.RedClone heap_base.RedCloneFail
heap_base.RedInterruptedTrue heap_base.RedInterruptedFalse
heap_base.RedYield

code_pred
(modes: i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ (i ⇒ i ⇒ i ⇒ o ⇒ bool) ⇒ (i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ bool) ⇒ i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ i ⇒ o ⇒ o ⇒ o ⇒ bool)
heap_base.red_external
proof -
case red_external
from red_external.prems show ?thesis
apply(rule heap_base.red_external.cases)
apply(erule (4) red_external.that[OF refl refl refl refl refl refl refl refl refl refl refl refl]|assumption|erule eqTrueI)+
done
qed

end
```