theory DetSchedSchedule_AI

lemma as_user_valid_sched_action[wp]: "\<lbrace>valid_sched_action\<rbrace> as_user ptr s \<lbrace>\<lambda>_. valid_sched_action\<rbrace>" apply (simp add: as_user_def set_object_def get_object_def | wpc | wp)+ apply (clarsimp simp: valid_sched_action_def st_tcb_at_def obj_at_def) apply (rule conjI) apply (clarsimp simp: is_activatable_def st_tcb_at_def obj_at_def st_tcb_at_kh_if_split) apply (drule get_tcb_SomeD, clarsimp) apply (clarsimp simp: weak_valid_sched_action_def st_tcb_at_def obj_at_def st_tcb_at_kh_if_split) apply (drule get_tcb_SomeD, clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched_action\<rbrace> as_user ptr s \<lbrace>\<lambda>_. valid_sched_action\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sa. valid_sched_action sa \<Longrightarrow> (\<exists>y. get_tcb ptr sa = Some y) \<longrightarrow> (\<forall>x\<in>fst (s (arch_tcb_context_get (tcb_arch (the (get_tcb ptr sa))))). \<forall>xa xb. x = (xa, xb) \<longrightarrow> (\<exists>y. kheap sa ptr = Some y) \<longrightarrow> a_type (the (kheap sa ptr)) = ATCB \<longrightarrow> valid_sched_action_2 (scheduler_action sa) (ekheap sa) (\<lambda>a. if a = ptr then Some (TCB (the (get_tcb ptr sa)\<lparr>tcb_arch := arch_tcb_context_set xb (tcb_arch (the (get_tcb ptr sa)))\<rparr>)) else kheap sa a) (cur_thread sa) (cur_domain sa)) proof (prove)
goal (1 subgoal):
 1. \<And>sa y x xa tcb. \<lbrakk>is_activatable (cur_thread sa) sa; weak_valid_sched_action sa; switch_in_cur_domain sa; (x, xa) \<in> fst (s (arch_tcb_context_get (tcb_arch y))); get_tcb ptr sa = Some y; kheap sa ptr = Some (TCB tcb)\<rbrakk> \<Longrightarrow> is_activatable_2 (cur_thread sa) (scheduler_action sa) (\<lambda>a. if a = ptr then Some (TCB (y\<lparr>tcb_arch := arch_tcb_context_set xa (tcb_arch y)\<rparr>)) else kheap sa a) \<and> weak_valid_sched_action_2 (scheduler_action sa) (ekheap sa) (\<lambda>a. if a = ptr then Some (TCB (y\<lparr>tcb_arch := arch_tcb_context_set xa (tcb_arch y)\<rparr>)) else kheap sa a) proof (prove)
goal (2 subgoals):
 1. \<And>sa y x xa tcb. \<lbrakk>is_activatable (cur_thread sa) sa; weak_valid_sched_action sa; switch_in_cur_domain sa; (x, xa) \<in> fst (s (arch_tcb_context_get (tcb_arch y))); get_tcb ptr sa = Some y; kheap sa ptr = Some (TCB tcb)\<rbrakk> \<Longrightarrow> is_activatable_2 (cur_thread sa) (scheduler_action sa) (\<lambda>a. if a = ptr then Some (TCB (y\<lparr>tcb_arch := arch_tcb_context_set xa (tcb_arch y)\<rparr>)) else kheap sa a)
 2. \<And>sa y x xa tcb. \<lbrakk>is_activatable (cur_thread sa) sa; weak_valid_sched_action sa; switch_in_cur_domain sa; (x, xa) \<in> fst (s (arch_tcb_context_get (tcb_arch y))); get_tcb ptr sa = Some y; kheap sa ptr = Some (TCB tcb)\<rbrakk> \<Longrightarrow> weak_valid_sched_action_2 (scheduler_action sa) (ekheap sa) (\<lambda>a. if a = ptr then Some (TCB (y\<lparr>tcb_arch := arch_tcb_context_set xa (tcb_arch y)\<rparr>)) else kheap sa a) proof (prove)
goal (2 subgoals):
 1. \<And>sa y x xa tcb. \<lbrakk>(x, xa) \<in> fst (s (arch_tcb_context_get (tcb_arch y))); get_tcb (cur_thread sa) sa = Some y; ptr = cur_thread sa; scheduler_action sa = resume_cur_thread; tcb_state y \<noteq> IdleThreadState; kheap sa (cur_thread sa) = Some (TCB tcb); activatable (tcb_state tcb)\<rbrakk> \<Longrightarrow> runnable (tcb_state y)
 2. \<And>sa y x xa tcb. \<lbrakk>is_activatable (cur_thread sa) sa; weak_valid_sched_action sa; switch_in_cur_domain sa; (x, xa) \<in> fst (s (arch_tcb_context_get (tcb_arch y))); get_tcb ptr sa = Some y; kheap sa ptr = Some (TCB tcb)\<rbrakk> \<Longrightarrow> weak_valid_sched_action_2 (scheduler_action sa) (ekheap sa) (\<lambda>a. if a = ptr then Some (TCB (y\<lparr>tcb_arch := arch_tcb_context_set xa (tcb_arch y)\<rparr>)) else kheap sa a) proof (prove)
goal (1 subgoal):
 1. \<And>sa y x xa tcb. \<lbrakk>is_activatable (cur_thread sa) sa; weak_valid_sched_action sa; switch_in_cur_domain sa; (x, xa) \<in> fst (s (arch_tcb_context_get (tcb_arch y))); get_tcb ptr sa = Some y; kheap sa ptr = Some (TCB tcb)\<rbrakk> \<Longrightarrow> weak_valid_sched_action_2 (scheduler_action sa) (ekheap sa) (\<lambda>a. if a = ptr then Some (TCB (y\<lparr>tcb_arch := arch_tcb_context_set xa (tcb_arch y)\<rparr>)) else kheap sa a) proof (prove)
goal (1 subgoal):
 1. \<And>sa y x xa tcb. \<lbrakk>runnable (tcb_state tcb); switch_in_cur_domain_2 (switch_thread ptr) (ekheap sa) (cur_domain sa); (x, xa) \<in> fst (s (arch_tcb_context_get (tcb_arch y))); get_tcb ptr sa = Some y; kheap sa ptr = Some (TCB tcb); scheduler_action sa = switch_thread ptr\<rbrakk> \<Longrightarrow> runnable (tcb_state y) proof (prove)
goal:
No subgoals!