[STATEMENT]
lemma jmm_start_heap_ok: "jmm.start_heap_ok"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. jmm'.start_heap_ok
[PROOF STEP]
apply(simp add: jmm.start_heap_ok_def jmm.start_heap_data_def initialization_list_def sys_xcpts_list_def jmm.create_initial_object_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. jmm_allocate jmm_empty (Class_type Thread) \<noteq> {} \<and> (jmm_allocate jmm_empty (Class_type Thread) \<noteq> {} \<longrightarrow> snd (snd (jmm'.create_initial_object (jmm'.create_initial_object (jmm'.create_initial_object (jmm'.create_initial_object (jmm'.create_initial_object (jmm'.create_initial_object (jmm'.create_initial_object (jmm'.create_initial_object (jmm'.create_initial_object (jmm'.create_initial_object (case SOME ha. ha \<in> jmm_allocate jmm_empty (Class_type Thread) of (h', a'') \<Rightarrow> (h', [a''], True)) NullPointer) ClassCast) OutOfMemory) ArrayIndexOutOfBounds) ArrayStore) NegativeArraySize) ArithmeticException) IllegalMonitorState) IllegalThreadState) InterruptedException)))
[PROOF STEP]
apply(split prod.split, clarify, clarsimp simp add: jmm.create_initial_object_simps jmm_allocate_eq_empty Thread_neq_sys_xcpts sys_xcpts_neqs dest!: jmm_allocate_Eps jmm_allocate_otherD)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done