[STATEMENT]
theorem external_call_progress:
  assumes wf: "wf_prog wf_md P"
  and wt: "P,h \<turnstile> a\<bullet>M(vs) : U"
  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>"
[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>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
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>
[PROOF STEP]
note [simp del] = split_paired_Ex
[PROOF STATE]
proof (state)
this:
(\<exists>x. ?P x) = (\<exists>a b. ?P (a, b))

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>
[PROOF STEP]
from wt
[PROOF STATE]
proof (chain)
picking this:
P,h \<turnstile> a\<bullet>M(vs) : U
[PROOF STEP]
obtain hT Ts Ts' D
    where T: "typeof_addr h a = \<lfloor>hT\<rfloor>" and Ts: "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 subTs: "P \<turnstile> Ts [\<le>] Ts'"
[PROOF STATE]
proof (prove)
using this:
P,h \<turnstile> a\<bullet>M(vs) : U

goal (1 subgoal):
 1. (\<And>hT Ts Ts' D. \<lbrakk>typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> class_type_of hT sees M: Ts'\<rightarrow>U = Native in D; P \<turnstile> Ts [\<le>] Ts'\<rbrakk> \<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 Ts Ts' D. \<lbrakk>typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> class_type_of hT sees M: Ts'\<rightarrow>U = Native in D; P \<turnstile> Ts [\<le>] Ts'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
typeof_addr h a = \<lfloor>hT\<rfloor>
map typeof\<^bsub>h\<^esub> vs = map Some Ts
P \<turnstile> class_type_of hT sees M: Ts'\<rightarrow>U = Native in D
P \<turnstile> Ts [\<le>] Ts'

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>
[PROOF STEP]
from wf \<open>P \<turnstile> class_type_of hT sees M:Ts'\<rightarrow>U = Native in D\<close>
[PROOF STATE]
proof (chain)
picking this:
wf_prog wf_md P
P \<turnstile> class_type_of hT sees M: Ts'\<rightarrow>U = Native in D
[PROOF STEP]
have "D\<bullet>M(Ts') :: U"
[PROOF STATE]
proof (prove)
using this:
wf_prog wf_md P
P \<turnstile> class_type_of hT sees M: Ts'\<rightarrow>U = Native in D

goal (1 subgoal):
 1. D\<bullet>M(Ts') :: U
[PROOF STEP]
by(rule sees_wf_native)
[PROOF STATE]
proof (state)
this:
D\<bullet>M(Ts') :: U

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>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
D\<bullet>M(Ts') :: U

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>
[PROOF STEP]
from \<open>P \<turnstile> class_type_of hT sees M:Ts'\<rightarrow>U = Native in D\<close>
[PROOF STATE]
proof (chain)
picking this:
P \<turnstile> class_type_of hT sees M: Ts'\<rightarrow>U = Native in D
[PROOF STEP]
have "P \<turnstile> ty_of_htype hT \<le> Class D"
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> class_type_of hT sees M: Ts'\<rightarrow>U = Native in D

goal (1 subgoal):
 1. P \<turnstile> ty_of_htype hT \<le> Class D
[PROOF STEP]
by(cases hT)(auto dest: sees_method_decl_above intro: widen_trans widen_array_object)
[PROOF STATE]
proof (state)
this:
P \<turnstile> ty_of_htype hT \<le> Class D

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>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
D\<bullet>M(Ts') :: U
P \<turnstile> ty_of_htype hT \<le> Class D
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
D\<bullet>M(Ts') :: U
P \<turnstile> ty_of_htype hT \<le> Class D

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>
[PROOF STEP]
using T Ts subTs
[PROOF STATE]
proof (prove)
using this:
D\<bullet>M(Ts') :: U
P \<turnstile> ty_of_htype hT \<le> Class D
typeof_addr h a = \<lfloor>hT\<rfloor>
map typeof\<^bsub>h\<^esub> vs = map Some Ts
P \<turnstile> Ts [\<le>] Ts'

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>
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (13 subgoals):
 1. \<lbrakk>P \<turnstile> ty_of_htype hT \<le> Class D; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> Ts [\<le>] Ts'; D = Thread; M = start; Ts' = []; U = Void\<rbrakk> \<Longrightarrow> \<exists>ta va h'. P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
 2. \<lbrakk>P \<turnstile> ty_of_htype hT \<le> Class D; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> Ts [\<le>] Ts'; D = Thread; M = join; Ts' = []; U = Void\<rbrakk> \<Longrightarrow> \<exists>ta va h'. P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
 3. \<lbrakk>P \<turnstile> ty_of_htype hT \<le> Class D; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> Ts [\<le>] Ts'; D = Thread; M = interrupt; Ts' = []; U = Void\<rbrakk> \<Longrightarrow> \<exists>ta va h'. P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
 4. \<lbrakk>P \<turnstile> ty_of_htype hT \<le> Class D; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> Ts [\<le>] Ts'; D = Thread; M = isInterrupted; Ts' = []; U = Boolean\<rbrakk> \<Longrightarrow> \<exists>ta va h'. P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
 5. \<lbrakk>P \<turnstile> ty_of_htype hT \<le> Class D; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> Ts [\<le>] Ts'; D = Object; M = wait; Ts' = []; U = Void\<rbrakk> \<Longrightarrow> \<exists>ta va h'. P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
 6. \<lbrakk>P \<turnstile> ty_of_htype hT \<le> Class D; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> Ts [\<le>] Ts'; D = Object; M = notify; Ts' = []; U = Void\<rbrakk> \<Longrightarrow> \<exists>ta va h'. P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
 7. \<lbrakk>P \<turnstile> ty_of_htype hT \<le> Class D; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> Ts [\<le>] Ts'; D = Object; M = notifyAll; Ts' = []; U = Void\<rbrakk> \<Longrightarrow> \<exists>ta va h'. P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
 8. \<lbrakk>P \<turnstile> ty_of_htype hT \<le> Class D; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> Ts [\<le>] Ts'; D = Object; M = clone; Ts' = []; U = Class Object\<rbrakk> \<Longrightarrow> \<exists>ta va h'. P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
 9. \<lbrakk>P \<turnstile> ty_of_htype hT \<le> Class D; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> Ts [\<le>] Ts'; D = Object; M = hashcode; Ts' = []; U = Integer\<rbrakk> \<Longrightarrow> \<exists>ta va h'. P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
 10. \<lbrakk>P \<turnstile> ty_of_htype hT \<le> Class D; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> Ts [\<le>] Ts'; D = Object; M = print; Ts' = [Integer]; U = Void\<rbrakk> \<Longrightarrow> \<exists>ta va h'. P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
A total of 13 subgoals...
[PROOF STEP]
assume [simp]: "D = Object" "M = clone" "Ts' = []" "U = Class Object"
[PROOF STATE]
proof (state)
this:
D = Object
M = clone
Ts' = []
U = Class Object

goal (13 subgoals):
 1. \<lbrakk>P \<turnstile> ty_of_htype hT \<le> Class D; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> Ts [\<le>] Ts'; D = Thread; M = start; Ts' = []; U = Void\<rbrakk> \<Longrightarrow> \<exists>ta va h'. P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
 2. \<lbrakk>P \<turnstile> ty_of_htype hT \<le> Class D; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> Ts [\<le>] Ts'; D = Thread; M = join; Ts' = []; U = Void\<rbrakk> \<Longrightarrow> \<exists>ta va h'. P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
 3. \<lbrakk>P \<turnstile> ty_of_htype hT \<le> Class D; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> Ts [\<le>] Ts'; D = Thread; M = interrupt; Ts' = []; U = Void\<rbrakk> \<Longrightarrow> \<exists>ta va h'. P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
 4. \<lbrakk>P \<turnstile> ty_of_htype hT \<le> Class D; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> Ts [\<le>] Ts'; D = Thread; M = isInterrupted; Ts' = []; U = Boolean\<rbrakk> \<Longrightarrow> \<exists>ta va h'. P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
 5. \<lbrakk>P \<turnstile> ty_of_htype hT \<le> Class D; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> Ts [\<le>] Ts'; D = Object; M = wait; Ts' = []; U = Void\<rbrakk> \<Longrightarrow> \<exists>ta va h'. P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
 6. \<lbrakk>P \<turnstile> ty_of_htype hT \<le> Class D; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> Ts [\<le>] Ts'; D = Object; M = notify; Ts' = []; U = Void\<rbrakk> \<Longrightarrow> \<exists>ta va h'. P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
 7. \<lbrakk>P \<turnstile> ty_of_htype hT \<le> Class D; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> Ts [\<le>] Ts'; D = Object; M = notifyAll; Ts' = []; U = Void\<rbrakk> \<Longrightarrow> \<exists>ta va h'. P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
 8. \<lbrakk>P \<turnstile> ty_of_htype hT \<le> Class D; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> Ts [\<le>] Ts'; D = Object; M = clone; Ts' = []; U = Class Object\<rbrakk> \<Longrightarrow> \<exists>ta va h'. P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
 9. \<lbrakk>P \<turnstile> ty_of_htype hT \<le> Class D; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> Ts [\<le>] Ts'; D = Object; M = hashcode; Ts' = []; U = Integer\<rbrakk> \<Longrightarrow> \<exists>ta va h'. P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
 10. \<lbrakk>P \<turnstile> ty_of_htype hT \<le> Class D; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> Ts [\<le>] Ts'; D = Object; M = print; Ts' = [Integer]; U = Void\<rbrakk> \<Longrightarrow> \<exists>ta va h'. P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
A total of 13 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 (13 subgoals):
 1. \<lbrakk>P \<turnstile> ty_of_htype hT \<le> Class D; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> Ts [\<le>] Ts'; D = Thread; M = start; Ts' = []; U = Void\<rbrakk> \<Longrightarrow> \<exists>ta va h'. P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
 2. \<lbrakk>P \<turnstile> ty_of_htype hT \<le> Class D; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> Ts [\<le>] Ts'; D = Thread; M = join; Ts' = []; U = Void\<rbrakk> \<Longrightarrow> \<exists>ta va h'. P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
 3. \<lbrakk>P \<turnstile> ty_of_htype hT \<le> Class D; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> Ts [\<le>] Ts'; D = Thread; M = interrupt; Ts' = []; U = Void\<rbrakk> \<Longrightarrow> \<exists>ta va h'. P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
 4. \<lbrakk>P \<turnstile> ty_of_htype hT \<le> Class D; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> Ts [\<le>] Ts'; D = Thread; M = isInterrupted; Ts' = []; U = Boolean\<rbrakk> \<Longrightarrow> \<exists>ta va h'. P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
 5. \<lbrakk>P \<turnstile> ty_of_htype hT \<le> Class D; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> Ts [\<le>] Ts'; D = Object; M = wait; Ts' = []; U = Void\<rbrakk> \<Longrightarrow> \<exists>ta va h'. P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
 6. \<lbrakk>P \<turnstile> ty_of_htype hT \<le> Class D; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> Ts [\<le>] Ts'; D = Object; M = notify; Ts' = []; U = Void\<rbrakk> \<Longrightarrow> \<exists>ta va h'. P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
 7. \<lbrakk>P \<turnstile> ty_of_htype hT \<le> Class D; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> Ts [\<le>] Ts'; D = Object; M = notifyAll; Ts' = []; U = Void\<rbrakk> \<Longrightarrow> \<exists>ta va h'. P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
 8. \<lbrakk>P \<turnstile> ty_of_htype hT \<le> Class D; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> Ts [\<le>] Ts'; D = Object; M = clone; Ts' = []; U = Class Object\<rbrakk> \<Longrightarrow> \<exists>ta va h'. P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
 9. \<lbrakk>P \<turnstile> ty_of_htype hT \<le> Class D; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> Ts [\<le>] Ts'; D = Object; M = hashcode; Ts' = []; U = Integer\<rbrakk> \<Longrightarrow> \<exists>ta va h'. P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
 10. \<lbrakk>P \<turnstile> ty_of_htype hT \<le> Class D; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> Ts [\<le>] Ts'; D = Object; M = print; Ts' = [Integer]; U = Void\<rbrakk> \<Longrightarrow> \<exists>ta va h'. P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
A total of 13 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>
[PROOF STEP]
using subTs Ts
[PROOF STATE]
proof (prove)
using this:
heap_clone P h a h' res
P \<turnstile> Ts [\<le>] Ts'
map typeof\<^bsub>h\<^esub> vs = map Some Ts

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>
[PROOF STEP]
by(cases res)(auto 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>

goal (12 subgoals):
 1. \<lbrakk>P \<turnstile> ty_of_htype hT \<le> Class D; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> Ts [\<le>] Ts'; D = Thread; M = start; Ts' = []; U = Void\<rbrakk> \<Longrightarrow> \<exists>ta va h'. P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
 2. \<lbrakk>P \<turnstile> ty_of_htype hT \<le> Class D; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> Ts [\<le>] Ts'; D = Thread; M = join; Ts' = []; U = Void\<rbrakk> \<Longrightarrow> \<exists>ta va h'. P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
 3. \<lbrakk>P \<turnstile> ty_of_htype hT \<le> Class D; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> Ts [\<le>] Ts'; D = Thread; M = interrupt; Ts' = []; U = Void\<rbrakk> \<Longrightarrow> \<exists>ta va h'. P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
 4. \<lbrakk>P \<turnstile> ty_of_htype hT \<le> Class D; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> Ts [\<le>] Ts'; D = Thread; M = isInterrupted; Ts' = []; U = Boolean\<rbrakk> \<Longrightarrow> \<exists>ta va h'. P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
 5. \<lbrakk>P \<turnstile> ty_of_htype hT \<le> Class D; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> Ts [\<le>] Ts'; D = Object; M = wait; Ts' = []; U = Void\<rbrakk> \<Longrightarrow> \<exists>ta va h'. P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
 6. \<lbrakk>P \<turnstile> ty_of_htype hT \<le> Class D; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> Ts [\<le>] Ts'; D = Object; M = notify; Ts' = []; U = Void\<rbrakk> \<Longrightarrow> \<exists>ta va h'. P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
 7. \<lbrakk>P \<turnstile> ty_of_htype hT \<le> Class D; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> Ts [\<le>] Ts'; D = Object; M = notifyAll; Ts' = []; U = Void\<rbrakk> \<Longrightarrow> \<exists>ta va h'. P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
 8. \<lbrakk>P \<turnstile> ty_of_htype hT \<le> Class D; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> Ts [\<le>] Ts'; D = Object; M = hashcode; Ts' = []; U = Integer\<rbrakk> \<Longrightarrow> \<exists>ta va h'. P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
 9. \<lbrakk>P \<turnstile> ty_of_htype hT \<le> Class D; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> Ts [\<le>] Ts'; D = Object; M = print; Ts' = [Integer]; U = Void\<rbrakk> \<Longrightarrow> \<exists>ta va h'. P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
 10. \<lbrakk>P \<turnstile> ty_of_htype hT \<le> Class D; typeof_addr h a = \<lfloor>hT\<rfloor>; map typeof\<^bsub>h\<^esub> vs = map Some Ts; P \<turnstile> Ts [\<le>] Ts'; D = Object; M = currentThread; Ts' = []; U = Class Thread\<rbrakk> \<Longrightarrow> \<exists>ta va h'. P,t \<turnstile> \<langle>a\<bullet>M(vs),h\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>
A total of 12 subgoals...
[PROOF STEP]
qed(auto simp add: widen_Class 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>

goal:
No subgoals!
[PROOF STEP]
qed