[STATEMENT]
lemma red_external_wt_hconf_hext:
  assumes wf: "wf_prog wf_md P"
  and red: "P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>"
  and hext: "h'' \<unlhd> h"
  and wt: "P,h'' \<turnstile> a\<bullet>M(vs) : U"
  and tconf: "P,h'' \<turnstile> t \<surd>t"
  and hconf: "hconf h''"
  shows "\<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va', h'''\<rangle> \<and>
                        collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and>
                        collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and>
                        collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
[PROOF STEP]
using red wt hext
[PROOF STATE]
proof (prove)
using this:
P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
P,h'' \<turnstile> a\<bullet>M(vs) : U
h'' \<unlhd> h

goal (1 subgoal):
 1. \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (26 subgoals):
 1. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = start; vs = []; ta = \<lbrace>NewThread (addr2thread_id a) (C, run, a) h, ThreadStart (addr2thread_id a)\<rbrace>; va = RetVal Unit; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 2. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = start; vs = []; ta = \<lbrace>ThreadExists (addr2thread_id a) True\<rbrace>; va = RetEXC IllegalThreadState; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 3. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = join; vs = []; ta = \<lbrace>Join (addr2thread_id a), IsInterrupted t False, ThreadJoin (addr2thread_id a)\<rbrace>; va = RetVal Unit; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 4. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = join; vs = []; ta = \<lbrace>IsInterrupted t True, ClearInterrupt t, ObsInterrupted t\<rbrace>; va = RetEXC InterruptedException; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 5. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = interrupt; vs = []; ta = \<lbrace>ThreadExists (addr2thread_id a) True, WakeUp (addr2thread_id a), Interrupt (addr2thread_id a), ObsInterrupt (addr2thread_id a)\<rbrace>; va = RetVal Unit; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 6. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = interrupt; vs = []; ta = \<lbrace>ThreadExists (addr2thread_id a) False\<rbrace>; va = RetVal Unit; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 7. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = isInterrupted; vs = []; ta = \<lbrace>IsInterrupted (addr2thread_id a) True, ObsInterrupted (addr2thread_id a)\<rbrace>; va = RetVal (Bool True); h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 8. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = isInterrupted; vs = []; ta = \<lbrace>IsInterrupted (addr2thread_id a) False\<rbrace>; va = RetVal (Bool False); h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 9. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = wait; vs = []; ta = \<lbrace>(Unlock, a), (Lock, a), IsInterrupted t True, ClearInterrupt t, ObsInterrupted t\<rbrace>; va = RetEXC InterruptedException; h' = h\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 10. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = wait; vs = []; ta = \<lbrace>Suspend a, (Unlock, a), (Lock, a), (ReleaseAcquire, a), IsInterrupted t False, SyncUnlock a\<rbrace>; va = RetStaySame; h' = h\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
A total of 26 subgoals...
[PROOF STEP]
case (RedClone obs a')
[PROOF STATE]
proof (state)
this:
M = clone
vs = []
ta = (K$ [], [], [], [], [], obs)
va = RetVal (Addr a')
heap_clone P h a h' \<lfloor>(obs, a')\<rfloor>

goal (26 subgoals):
 1. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = start; vs = []; ta = \<lbrace>NewThread (addr2thread_id a) (C, run, a) h, ThreadStart (addr2thread_id a)\<rbrace>; va = RetVal Unit; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 2. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = start; vs = []; ta = \<lbrace>ThreadExists (addr2thread_id a) True\<rbrace>; va = RetEXC IllegalThreadState; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 3. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = join; vs = []; ta = \<lbrace>Join (addr2thread_id a), IsInterrupted t False, ThreadJoin (addr2thread_id a)\<rbrace>; va = RetVal Unit; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 4. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = join; vs = []; ta = \<lbrace>IsInterrupted t True, ClearInterrupt t, ObsInterrupted t\<rbrace>; va = RetEXC InterruptedException; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 5. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = interrupt; vs = []; ta = \<lbrace>ThreadExists (addr2thread_id a) True, WakeUp (addr2thread_id a), Interrupt (addr2thread_id a), ObsInterrupt (addr2thread_id a)\<rbrace>; va = RetVal Unit; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 6. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = interrupt; vs = []; ta = \<lbrace>ThreadExists (addr2thread_id a) False\<rbrace>; va = RetVal Unit; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 7. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = isInterrupted; vs = []; ta = \<lbrace>IsInterrupted (addr2thread_id a) True, ObsInterrupted (addr2thread_id a)\<rbrace>; va = RetVal (Bool True); h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 8. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = isInterrupted; vs = []; ta = \<lbrace>IsInterrupted (addr2thread_id a) False\<rbrace>; va = RetVal (Bool False); h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 9. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = wait; vs = []; ta = \<lbrace>(Unlock, a), (Lock, a), IsInterrupted t True, ClearInterrupt t, ObsInterrupted t\<rbrace>; va = RetEXC InterruptedException; h' = h\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 10. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = wait; vs = []; ta = \<lbrace>Suspend a, (Unlock, a), (Lock, a), (ReleaseAcquire, a), IsInterrupted t False, SyncUnlock a\<rbrace>; va = RetStaySame; h' = h\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
A total of 26 subgoals...
[PROOF STEP]
from wt
[PROOF STATE]
proof (chain)
picking this:
P,h'' \<turnstile> a\<bullet>M(vs) : U
[PROOF STEP]
obtain hT C Ts Ts' D
    where T: "typeof_addr h'' a = \<lfloor>hT\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
P,h'' \<turnstile> a\<bullet>M(vs) : U

goal (1 subgoal):
 1. (\<And>hT. typeof_addr h'' a = \<lfloor>hT\<rfloor> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding external_WT'_iff
[PROOF STATE]
proof (prove)
using this:
\<exists>hT Ts Ts' D. typeof_addr h'' a = \<lfloor>hT\<rfloor> \<and> map typeof\<^bsub>h''\<^esub> vs = map Some Ts \<and> P \<turnstile> class_type_of hT sees M: Ts'\<rightarrow>U = Native in D \<and> P \<turnstile> Ts [\<le>] Ts'

goal (1 subgoal):
 1. (\<And>hT. typeof_addr h'' a = \<lfloor>hT\<rfloor> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
typeof_addr h'' a = \<lfloor>hT\<rfloor>

goal (26 subgoals):
 1. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = start; vs = []; ta = \<lbrace>NewThread (addr2thread_id a) (C, run, a) h, ThreadStart (addr2thread_id a)\<rbrace>; va = RetVal Unit; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 2. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = start; vs = []; ta = \<lbrace>ThreadExists (addr2thread_id a) True\<rbrace>; va = RetEXC IllegalThreadState; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 3. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = join; vs = []; ta = \<lbrace>Join (addr2thread_id a), IsInterrupted t False, ThreadJoin (addr2thread_id a)\<rbrace>; va = RetVal Unit; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 4. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = join; vs = []; ta = \<lbrace>IsInterrupted t True, ClearInterrupt t, ObsInterrupted t\<rbrace>; va = RetEXC InterruptedException; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 5. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = interrupt; vs = []; ta = \<lbrace>ThreadExists (addr2thread_id a) True, WakeUp (addr2thread_id a), Interrupt (addr2thread_id a), ObsInterrupt (addr2thread_id a)\<rbrace>; va = RetVal Unit; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 6. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = interrupt; vs = []; ta = \<lbrace>ThreadExists (addr2thread_id a) False\<rbrace>; va = RetVal Unit; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 7. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = isInterrupted; vs = []; ta = \<lbrace>IsInterrupted (addr2thread_id a) True, ObsInterrupted (addr2thread_id a)\<rbrace>; va = RetVal (Bool True); h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 8. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = isInterrupted; vs = []; ta = \<lbrace>IsInterrupted (addr2thread_id a) False\<rbrace>; va = RetVal (Bool False); h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 9. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = wait; vs = []; ta = \<lbrace>(Unlock, a), (Lock, a), IsInterrupted t True, ClearInterrupt t, ObsInterrupted t\<rbrace>; va = RetEXC InterruptedException; h' = h\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 10. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = wait; vs = []; ta = \<lbrace>Suspend a, (Unlock, a), (Lock, a), (ReleaseAcquire, a), IsInterrupted t False, SyncUnlock a\<rbrace>; va = RetStaySame; h' = h\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
A total of 26 subgoals...
[PROOF STEP]
from heap_clone_progress[OF wf T hconf]
[PROOF STATE]
proof (chain)
picking this:
\<exists>h' res. heap_clone P h'' a h' res
[PROOF STEP]
obtain h''' res where "heap_clone P h'' a h''' res"
[PROOF STATE]
proof (prove)
using this:
\<exists>h' res. heap_clone P h'' a h' res

goal (1 subgoal):
 1. (\<And>h''' res. heap_clone P h'' a h''' res \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
heap_clone P h'' a h''' res

goal (26 subgoals):
 1. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = start; vs = []; ta = \<lbrace>NewThread (addr2thread_id a) (C, run, a) h, ThreadStart (addr2thread_id a)\<rbrace>; va = RetVal Unit; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 2. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = start; vs = []; ta = \<lbrace>ThreadExists (addr2thread_id a) True\<rbrace>; va = RetEXC IllegalThreadState; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 3. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = join; vs = []; ta = \<lbrace>Join (addr2thread_id a), IsInterrupted t False, ThreadJoin (addr2thread_id a)\<rbrace>; va = RetVal Unit; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 4. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = join; vs = []; ta = \<lbrace>IsInterrupted t True, ClearInterrupt t, ObsInterrupted t\<rbrace>; va = RetEXC InterruptedException; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 5. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = interrupt; vs = []; ta = \<lbrace>ThreadExists (addr2thread_id a) True, WakeUp (addr2thread_id a), Interrupt (addr2thread_id a), ObsInterrupt (addr2thread_id a)\<rbrace>; va = RetVal Unit; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 6. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = interrupt; vs = []; ta = \<lbrace>ThreadExists (addr2thread_id a) False\<rbrace>; va = RetVal Unit; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 7. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = isInterrupted; vs = []; ta = \<lbrace>IsInterrupted (addr2thread_id a) True, ObsInterrupted (addr2thread_id a)\<rbrace>; va = RetVal (Bool True); h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 8. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = isInterrupted; vs = []; ta = \<lbrace>IsInterrupted (addr2thread_id a) False\<rbrace>; va = RetVal (Bool False); h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 9. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = wait; vs = []; ta = \<lbrace>(Unlock, a), (Lock, a), IsInterrupted t True, ClearInterrupt t, ObsInterrupted t\<rbrace>; va = RetEXC InterruptedException; h' = h\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 10. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = wait; vs = []; ta = \<lbrace>Suspend a, (Unlock, a), (Lock, a), (ReleaseAcquire, a), IsInterrupted t False, SyncUnlock a\<rbrace>; va = RetStaySame; h' = h\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
A total of 26 subgoals...
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
heap_clone P h'' a h''' res

goal (1 subgoal):
 1. \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
[PROOF STEP]
using RedClone
[PROOF STATE]
proof (prove)
using this:
heap_clone P h'' a h''' res
M = clone
vs = []
ta = (K$ [], [], [], [], [], obs)
va = RetVal (Addr a')
heap_clone P h a h' \<lfloor>(obs, a')\<rfloor>

goal (1 subgoal):
 1. \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
[PROOF STEP]
by(cases res)(fastforce intro: red_external.intros)+
[PROOF STATE]
proof (state)
this:
\<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>

goal (25 subgoals):
 1. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = start; vs = []; ta = \<lbrace>NewThread (addr2thread_id a) (C, run, a) h, ThreadStart (addr2thread_id a)\<rbrace>; va = RetVal Unit; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 2. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = start; vs = []; ta = \<lbrace>ThreadExists (addr2thread_id a) True\<rbrace>; va = RetEXC IllegalThreadState; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 3. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = join; vs = []; ta = \<lbrace>Join (addr2thread_id a), IsInterrupted t False, ThreadJoin (addr2thread_id a)\<rbrace>; va = RetVal Unit; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 4. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = join; vs = []; ta = \<lbrace>IsInterrupted t True, ClearInterrupt t, ObsInterrupted t\<rbrace>; va = RetEXC InterruptedException; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 5. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = interrupt; vs = []; ta = \<lbrace>ThreadExists (addr2thread_id a) True, WakeUp (addr2thread_id a), Interrupt (addr2thread_id a), ObsInterrupt (addr2thread_id a)\<rbrace>; va = RetVal Unit; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 6. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = interrupt; vs = []; ta = \<lbrace>ThreadExists (addr2thread_id a) False\<rbrace>; va = RetVal Unit; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 7. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = isInterrupted; vs = []; ta = \<lbrace>IsInterrupted (addr2thread_id a) True, ObsInterrupted (addr2thread_id a)\<rbrace>; va = RetVal (Bool True); h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 8. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = isInterrupted; vs = []; ta = \<lbrace>IsInterrupted (addr2thread_id a) False\<rbrace>; va = RetVal (Bool False); h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 9. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = wait; vs = []; ta = \<lbrace>(Unlock, a), (Lock, a), IsInterrupted t True, ClearInterrupt t, ObsInterrupted t\<rbrace>; va = RetEXC InterruptedException; h' = h\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 10. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = wait; vs = []; ta = \<lbrace>Suspend a, (Unlock, a), (Lock, a), (ReleaseAcquire, a), IsInterrupted t False, SyncUnlock a\<rbrace>; va = RetStaySame; h' = h\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
A total of 25 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (25 subgoals):
 1. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = start; vs = []; ta = \<lbrace>NewThread (addr2thread_id a) (C, run, a) h, ThreadStart (addr2thread_id a)\<rbrace>; va = RetVal Unit; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 2. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = start; vs = []; ta = \<lbrace>ThreadExists (addr2thread_id a) True\<rbrace>; va = RetEXC IllegalThreadState; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 3. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = join; vs = []; ta = \<lbrace>Join (addr2thread_id a), IsInterrupted t False, ThreadJoin (addr2thread_id a)\<rbrace>; va = RetVal Unit; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 4. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = join; vs = []; ta = \<lbrace>IsInterrupted t True, ClearInterrupt t, ObsInterrupted t\<rbrace>; va = RetEXC InterruptedException; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 5. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = interrupt; vs = []; ta = \<lbrace>ThreadExists (addr2thread_id a) True, WakeUp (addr2thread_id a), Interrupt (addr2thread_id a), ObsInterrupt (addr2thread_id a)\<rbrace>; va = RetVal Unit; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 6. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = interrupt; vs = []; ta = \<lbrace>ThreadExists (addr2thread_id a) False\<rbrace>; va = RetVal Unit; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 7. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = isInterrupted; vs = []; ta = \<lbrace>IsInterrupted (addr2thread_id a) True, ObsInterrupted (addr2thread_id a)\<rbrace>; va = RetVal (Bool True); h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 8. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = isInterrupted; vs = []; ta = \<lbrace>IsInterrupted (addr2thread_id a) False\<rbrace>; va = RetVal (Bool False); h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 9. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = wait; vs = []; ta = \<lbrace>(Unlock, a), (Lock, a), IsInterrupted t True, ClearInterrupt t, ObsInterrupted t\<rbrace>; va = RetEXC InterruptedException; h' = h\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 10. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = wait; vs = []; ta = \<lbrace>Suspend a, (Unlock, a), (Lock, a), (ReleaseAcquire, a), IsInterrupted t False, SyncUnlock a\<rbrace>; va = RetStaySame; h' = h\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
A total of 25 subgoals...
[PROOF STEP]
case RedCloneFail
[PROOF STATE]
proof (state)
this:
M = clone
vs = []
ta = \<lbrace>\<rbrace>
va = RetEXC OutOfMemory
heap_clone P h a h' None

goal (25 subgoals):
 1. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = start; vs = []; ta = \<lbrace>NewThread (addr2thread_id a) (C, run, a) h, ThreadStart (addr2thread_id a)\<rbrace>; va = RetVal Unit; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 2. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = start; vs = []; ta = \<lbrace>ThreadExists (addr2thread_id a) True\<rbrace>; va = RetEXC IllegalThreadState; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 3. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = join; vs = []; ta = \<lbrace>Join (addr2thread_id a), IsInterrupted t False, ThreadJoin (addr2thread_id a)\<rbrace>; va = RetVal Unit; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 4. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = join; vs = []; ta = \<lbrace>IsInterrupted t True, ClearInterrupt t, ObsInterrupted t\<rbrace>; va = RetEXC InterruptedException; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 5. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = interrupt; vs = []; ta = \<lbrace>ThreadExists (addr2thread_id a) True, WakeUp (addr2thread_id a), Interrupt (addr2thread_id a), ObsInterrupt (addr2thread_id a)\<rbrace>; va = RetVal Unit; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 6. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = interrupt; vs = []; ta = \<lbrace>ThreadExists (addr2thread_id a) False\<rbrace>; va = RetVal Unit; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 7. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = isInterrupted; vs = []; ta = \<lbrace>IsInterrupted (addr2thread_id a) True, ObsInterrupted (addr2thread_id a)\<rbrace>; va = RetVal (Bool True); h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 8. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = isInterrupted; vs = []; ta = \<lbrace>IsInterrupted (addr2thread_id a) False\<rbrace>; va = RetVal (Bool False); h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 9. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = wait; vs = []; ta = \<lbrace>(Unlock, a), (Lock, a), IsInterrupted t True, ClearInterrupt t, ObsInterrupted t\<rbrace>; va = RetEXC InterruptedException; h' = h\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 10. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = wait; vs = []; ta = \<lbrace>Suspend a, (Unlock, a), (Lock, a), (ReleaseAcquire, a), IsInterrupted t False, SyncUnlock a\<rbrace>; va = RetStaySame; h' = h\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
A total of 25 subgoals...
[PROOF STEP]
from wt
[PROOF STATE]
proof (chain)
picking this:
P,h'' \<turnstile> a\<bullet>M(vs) : U
[PROOF STEP]
obtain hT Ts Ts'
    where T: "typeof_addr h'' a = \<lfloor>hT\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
P,h'' \<turnstile> a\<bullet>M(vs) : U

goal (1 subgoal):
 1. (\<And>hT. typeof_addr h'' a = \<lfloor>hT\<rfloor> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding external_WT'_iff
[PROOF STATE]
proof (prove)
using this:
\<exists>hT Ts Ts' D. typeof_addr h'' a = \<lfloor>hT\<rfloor> \<and> map typeof\<^bsub>h''\<^esub> vs = map Some Ts \<and> P \<turnstile> class_type_of hT sees M: Ts'\<rightarrow>U = Native in D \<and> P \<turnstile> Ts [\<le>] Ts'

goal (1 subgoal):
 1. (\<And>hT. typeof_addr h'' a = \<lfloor>hT\<rfloor> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
typeof_addr h'' a = \<lfloor>hT\<rfloor>

goal (25 subgoals):
 1. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = start; vs = []; ta = \<lbrace>NewThread (addr2thread_id a) (C, run, a) h, ThreadStart (addr2thread_id a)\<rbrace>; va = RetVal Unit; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 2. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = start; vs = []; ta = \<lbrace>ThreadExists (addr2thread_id a) True\<rbrace>; va = RetEXC IllegalThreadState; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 3. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = join; vs = []; ta = \<lbrace>Join (addr2thread_id a), IsInterrupted t False, ThreadJoin (addr2thread_id a)\<rbrace>; va = RetVal Unit; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 4. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = join; vs = []; ta = \<lbrace>IsInterrupted t True, ClearInterrupt t, ObsInterrupted t\<rbrace>; va = RetEXC InterruptedException; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 5. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = interrupt; vs = []; ta = \<lbrace>ThreadExists (addr2thread_id a) True, WakeUp (addr2thread_id a), Interrupt (addr2thread_id a), ObsInterrupt (addr2thread_id a)\<rbrace>; va = RetVal Unit; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 6. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = interrupt; vs = []; ta = \<lbrace>ThreadExists (addr2thread_id a) False\<rbrace>; va = RetVal Unit; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 7. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = isInterrupted; vs = []; ta = \<lbrace>IsInterrupted (addr2thread_id a) True, ObsInterrupted (addr2thread_id a)\<rbrace>; va = RetVal (Bool True); h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 8. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = isInterrupted; vs = []; ta = \<lbrace>IsInterrupted (addr2thread_id a) False\<rbrace>; va = RetVal (Bool False); h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 9. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = wait; vs = []; ta = \<lbrace>(Unlock, a), (Lock, a), IsInterrupted t True, ClearInterrupt t, ObsInterrupted t\<rbrace>; va = RetEXC InterruptedException; h' = h\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 10. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = wait; vs = []; ta = \<lbrace>Suspend a, (Unlock, a), (Lock, a), (ReleaseAcquire, a), IsInterrupted t False, SyncUnlock a\<rbrace>; va = RetStaySame; h' = h\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
A total of 25 subgoals...
[PROOF STEP]
from heap_clone_progress[OF wf T hconf]
[PROOF STATE]
proof (chain)
picking this:
\<exists>h' res. heap_clone P h'' a h' res
[PROOF STEP]
obtain h''' res where "heap_clone P h'' a h''' res"
[PROOF STATE]
proof (prove)
using this:
\<exists>h' res. heap_clone P h'' a h' res

goal (1 subgoal):
 1. (\<And>h''' res. heap_clone P h'' a h''' res \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
heap_clone P h'' a h''' res

goal (25 subgoals):
 1. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = start; vs = []; ta = \<lbrace>NewThread (addr2thread_id a) (C, run, a) h, ThreadStart (addr2thread_id a)\<rbrace>; va = RetVal Unit; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 2. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = start; vs = []; ta = \<lbrace>ThreadExists (addr2thread_id a) True\<rbrace>; va = RetEXC IllegalThreadState; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 3. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = join; vs = []; ta = \<lbrace>Join (addr2thread_id a), IsInterrupted t False, ThreadJoin (addr2thread_id a)\<rbrace>; va = RetVal Unit; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 4. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = join; vs = []; ta = \<lbrace>IsInterrupted t True, ClearInterrupt t, ObsInterrupted t\<rbrace>; va = RetEXC InterruptedException; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 5. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = interrupt; vs = []; ta = \<lbrace>ThreadExists (addr2thread_id a) True, WakeUp (addr2thread_id a), Interrupt (addr2thread_id a), ObsInterrupt (addr2thread_id a)\<rbrace>; va = RetVal Unit; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 6. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = interrupt; vs = []; ta = \<lbrace>ThreadExists (addr2thread_id a) False\<rbrace>; va = RetVal Unit; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 7. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = isInterrupted; vs = []; ta = \<lbrace>IsInterrupted (addr2thread_id a) True, ObsInterrupted (addr2thread_id a)\<rbrace>; va = RetVal (Bool True); h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 8. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = isInterrupted; vs = []; ta = \<lbrace>IsInterrupted (addr2thread_id a) False\<rbrace>; va = RetVal (Bool False); h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 9. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = wait; vs = []; ta = \<lbrace>(Unlock, a), (Lock, a), IsInterrupted t True, ClearInterrupt t, ObsInterrupted t\<rbrace>; va = RetEXC InterruptedException; h' = h\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 10. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = wait; vs = []; ta = \<lbrace>Suspend a, (Unlock, a), (Lock, a), (ReleaseAcquire, a), IsInterrupted t False, SyncUnlock a\<rbrace>; va = RetStaySame; h' = h\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
A total of 25 subgoals...
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
heap_clone P h'' a h''' res

goal (1 subgoal):
 1. \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
[PROOF STEP]
using RedCloneFail
[PROOF STATE]
proof (prove)
using this:
heap_clone P h'' a h''' res
M = clone
vs = []
ta = \<lbrace>\<rbrace>
va = RetEXC OutOfMemory
heap_clone P h a h' None

goal (1 subgoal):
 1. \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
[PROOF STEP]
by(cases res)(fastforce intro: red_external.intros)+
[PROOF STATE]
proof (state)
this:
\<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>

goal (24 subgoals):
 1. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = start; vs = []; ta = \<lbrace>NewThread (addr2thread_id a) (C, run, a) h, ThreadStart (addr2thread_id a)\<rbrace>; va = RetVal Unit; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 2. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = start; vs = []; ta = \<lbrace>ThreadExists (addr2thread_id a) True\<rbrace>; va = RetEXC IllegalThreadState; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 3. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = join; vs = []; ta = \<lbrace>Join (addr2thread_id a), IsInterrupted t False, ThreadJoin (addr2thread_id a)\<rbrace>; va = RetVal Unit; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 4. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = join; vs = []; ta = \<lbrace>IsInterrupted t True, ClearInterrupt t, ObsInterrupted t\<rbrace>; va = RetEXC InterruptedException; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 5. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = interrupt; vs = []; ta = \<lbrace>ThreadExists (addr2thread_id a) True, WakeUp (addr2thread_id a), Interrupt (addr2thread_id a), ObsInterrupt (addr2thread_id a)\<rbrace>; va = RetVal Unit; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 6. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = interrupt; vs = []; ta = \<lbrace>ThreadExists (addr2thread_id a) False\<rbrace>; va = RetVal Unit; h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 7. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = isInterrupted; vs = []; ta = \<lbrace>IsInterrupted (addr2thread_id a) True, ObsInterrupted (addr2thread_id a)\<rbrace>; va = RetVal (Bool True); h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 8. \<And>C. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = isInterrupted; vs = []; ta = \<lbrace>IsInterrupted (addr2thread_id a) False\<rbrace>; va = RetVal (Bool False); h' = h; typeof_addr h a = \<lfloor>Class_type C\<rfloor>; P \<turnstile> C \<preceq>\<^sup>* Thread\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 9. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = wait; vs = []; ta = \<lbrace>(Unlock, a), (Lock, a), IsInterrupted t True, ClearInterrupt t, ObsInterrupted t\<rbrace>; va = RetEXC InterruptedException; h' = h\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
 10. \<lbrakk>P,h'' \<turnstile> a\<bullet>M(vs) : U; h'' \<unlhd> h; M = wait; vs = []; ta = \<lbrace>Suspend a, (Unlock, a), (Lock, a), (ReleaseAcquire, a), IsInterrupted t False, SyncUnlock a\<rbrace>; va = RetStaySame; h' = h\<rbrakk> \<Longrightarrow> \<exists>ta' va' h'''. P,t \<turnstile> \<langle>a\<bullet>M(vs),h''\<rangle> -ta'\<rightarrow>ext \<langle>va',h'''\<rangle> \<and> collect_locks \<lbrace>ta\<rbrace>\<^bsub>l\<^esub> = collect_locks \<lbrace>ta'\<rbrace>\<^bsub>l\<^esub> \<and> collect_cond_actions \<lbrace>ta\<rbrace>\<^bsub>c\<^esub> = collect_cond_actions \<lbrace>ta'\<rbrace>\<^bsub>c\<^esub> \<and> collect_interrupts \<lbrace>ta\<rbrace>\<^bsub>i\<^esub> = collect_interrupts \<lbrace>ta'\<rbrace>\<^bsub>i\<^esub>
A total of 24 subgoals...
[PROOF STEP]
qed(fastforce simp add: ta_upd_simps elim!: external_WT'.cases intro: red_external.intros[simplified] dest: typeof_addr_hext_mono)+