theory Example_Valid_State

lemma valid_sched_s0[simp]:
  "valid_sched s0_internal" apply (simp add: valid_sched_def s0_internal_def exst0_def) apply (intro conjI) apply (clarsimp simp: valid_etcbs_def s0_ptr_defs kh0_def kh0_obj_def is_etcb_at'_def
                              st_tcb_at_kh_def obj_at_kh_def obj_at_def) apply (clarsimp simp: const_def) apply (clarsimp simp: const_def) apply (clarsimp simp: valid_sched_action_def is_activatable_def st_tcb_at_kh_def
                           obj_at_kh_def obj_at_def kh0_def kh0_obj_def s0_ptr_defs) apply (clarsimp simp: ct_in_cur_domain_def in_cur_domain_def etcb_at'_def ekh0_obj_def
                          s0_ptr_defs) apply (clarsimp simp: const_def valid_blocked_def st_tcb_at_kh_def obj_at_kh_def obj_at_def
                         kh0_def kh0_obj_def split: if_split_asm) apply (clarsimp simp: valid_idle_etcb_def etcb_at'_def ekh0_obj_def s0_ptr_defs idle_thread_ptr_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_sched s0_internal proof (prove)
goal (1 subgoal):
 1. valid_etcbs_2 [Low_tcb_ptr \<mapsto> Low_etcb, High_tcb_ptr \<mapsto> High_etcb, idle_tcb_ptr \<mapsto> default_etcb] kh0 \<and> valid_queues_2 (const (const [])) [Low_tcb_ptr \<mapsto> Low_etcb, High_tcb_ptr \<mapsto> High_etcb, idle_tcb_ptr \<mapsto> default_etcb] kh0 \<and> ct_not_in_q_2 (const (const [])) resume_cur_thread Low_tcb_ptr \<and> valid_sched_action_2 resume_cur_thread [Low_tcb_ptr \<mapsto> Low_etcb, High_tcb_ptr \<mapsto> High_etcb, idle_tcb_ptr \<mapsto> default_etcb] kh0 Low_tcb_ptr 0 \<and> ct_in_cur_domain_2 Low_tcb_ptr idle_tcb_ptr resume_cur_thread 0 [Low_tcb_ptr \<mapsto> Low_etcb, High_tcb_ptr \<mapsto> High_etcb, idle_tcb_ptr \<mapsto> default_etcb] \<and> valid_blocked_2 (const (const [])) kh0 resume_cur_thread Low_tcb_ptr \<and> valid_idle_etcb_2 [Low_tcb_ptr \<mapsto> Low_etcb, High_tcb_ptr \<mapsto> High_etcb, idle_tcb_ptr \<mapsto> default_etcb] proof (prove)
goal (7 subgoals):
 1. valid_etcbs_2 [Low_tcb_ptr \<mapsto> Low_etcb, High_tcb_ptr \<mapsto> High_etcb, idle_tcb_ptr \<mapsto> default_etcb] kh0
 2. valid_queues_2 (const (const [])) [Low_tcb_ptr \<mapsto> Low_etcb, High_tcb_ptr \<mapsto> High_etcb, idle_tcb_ptr \<mapsto> default_etcb] kh0
 3. ct_not_in_q_2 (const (const [])) resume_cur_thread Low_tcb_ptr
 4. valid_sched_action_2 resume_cur_thread [Low_tcb_ptr \<mapsto> Low_etcb, High_tcb_ptr \<mapsto> High_etcb, idle_tcb_ptr \<mapsto> default_etcb] kh0 Low_tcb_ptr 0
 5. ct_in_cur_domain_2 Low_tcb_ptr idle_tcb_ptr resume_cur_thread 0 [Low_tcb_ptr \<mapsto> Low_etcb, High_tcb_ptr \<mapsto> High_etcb, idle_tcb_ptr \<mapsto> default_etcb]
 6. valid_blocked_2 (const (const [])) kh0 resume_cur_thread Low_tcb_ptr
 7. valid_idle_etcb_2 [Low_tcb_ptr \<mapsto> Low_etcb, High_tcb_ptr \<mapsto> High_etcb, idle_tcb_ptr \<mapsto> default_etcb] proof (prove)
goal (6 subgoals):
 1. valid_queues_2 (const (const [])) [Low_tcb_ptr \<mapsto> Low_etcb, High_tcb_ptr \<mapsto> High_etcb, idle_tcb_ptr \<mapsto> default_etcb] kh0
 2. ct_not_in_q_2 (const (const [])) resume_cur_thread Low_tcb_ptr
 3. valid_sched_action_2 resume_cur_thread [Low_tcb_ptr \<mapsto> Low_etcb, High_tcb_ptr \<mapsto> High_etcb, idle_tcb_ptr \<mapsto> default_etcb] kh0 Low_tcb_ptr 0
 4. ct_in_cur_domain_2 Low_tcb_ptr idle_tcb_ptr resume_cur_thread 0 [Low_tcb_ptr \<mapsto> Low_etcb, High_tcb_ptr \<mapsto> High_etcb, idle_tcb_ptr \<mapsto> default_etcb]
 5. valid_blocked_2 (const (const [])) kh0 resume_cur_thread Low_tcb_ptr
 6. valid_idle_etcb_2 [Low_tcb_ptr \<mapsto> Low_etcb, High_tcb_ptr \<mapsto> High_etcb, idle_tcb_ptr \<mapsto> default_etcb] proof (prove)
goal (5 subgoals):
 1. ct_not_in_q_2 (const (const [])) resume_cur_thread Low_tcb_ptr
 2. valid_sched_action_2 resume_cur_thread [Low_tcb_ptr \<mapsto> Low_etcb, High_tcb_ptr \<mapsto> High_etcb, idle_tcb_ptr \<mapsto> default_etcb] kh0 Low_tcb_ptr 0
 3. ct_in_cur_domain_2 Low_tcb_ptr idle_tcb_ptr resume_cur_thread 0 [Low_tcb_ptr \<mapsto> Low_etcb, High_tcb_ptr \<mapsto> High_etcb, idle_tcb_ptr \<mapsto> default_etcb]
 4. valid_blocked_2 (const (const [])) kh0 resume_cur_thread Low_tcb_ptr
 5. valid_idle_etcb_2 [Low_tcb_ptr \<mapsto> Low_etcb, High_tcb_ptr \<mapsto> High_etcb, idle_tcb_ptr \<mapsto> default_etcb] proof (prove)
goal (4 subgoals):
 1. valid_sched_action_2 resume_cur_thread [Low_tcb_ptr \<mapsto> Low_etcb, High_tcb_ptr \<mapsto> High_etcb, idle_tcb_ptr \<mapsto> default_etcb] kh0 Low_tcb_ptr 0
 2. ct_in_cur_domain_2 Low_tcb_ptr idle_tcb_ptr resume_cur_thread 0 [Low_tcb_ptr \<mapsto> Low_etcb, High_tcb_ptr \<mapsto> High_etcb, idle_tcb_ptr \<mapsto> default_etcb]
 3. valid_blocked_2 (const (const [])) kh0 resume_cur_thread Low_tcb_ptr
 4. valid_idle_etcb_2 [Low_tcb_ptr \<mapsto> Low_etcb, High_tcb_ptr \<mapsto> High_etcb, idle_tcb_ptr \<mapsto> default_etcb] proof (prove)
goal (3 subgoals):
 1. ct_in_cur_domain_2 Low_tcb_ptr idle_tcb_ptr resume_cur_thread 0 [Low_tcb_ptr \<mapsto> Low_etcb, High_tcb_ptr \<mapsto> High_etcb, idle_tcb_ptr \<mapsto> default_etcb]
 2. valid_blocked_2 (const (const [])) kh0 resume_cur_thread Low_tcb_ptr
 3. valid_idle_etcb_2 [Low_tcb_ptr \<mapsto> Low_etcb, High_tcb_ptr \<mapsto> High_etcb, idle_tcb_ptr \<mapsto> default_etcb] proof (prove)
goal (2 subgoals):
 1. valid_blocked_2 (const (const [])) kh0 resume_cur_thread Low_tcb_ptr
 2. valid_idle_etcb_2 [Low_tcb_ptr \<mapsto> Low_etcb, High_tcb_ptr \<mapsto> High_etcb, idle_tcb_ptr \<mapsto> default_etcb] proof (prove)
goal (1 subgoal):
 1. valid_idle_etcb_2 [Low_tcb_ptr \<mapsto> Low_etcb, High_tcb_ptr \<mapsto> High_etcb, idle_tcb_ptr \<mapsto> default_etcb] proof (prove)
goal:
No subgoals!