theory DetSchedSchedule_AI

lemma as_user_valid_queues[wp]: "\<lbrace>valid_queues\<rbrace> as_user ptr s \<lbrace>\<lambda>_. valid_queues\<rbrace>" apply (simp add: as_user_def set_object_def get_object_def | wpc | wp)+ apply (clarsimp simp: valid_queues_def st_tcb_at_kh_if_split st_tcb_at_def obj_at_def) apply (drule_tac x=d in spec) apply (drule_tac x=p in spec) apply clarsimp apply (drule (1) bspec, clarsimp simp: st_tcb_def2) apply (drule get_tcb_SomeD, auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues\<rbrace> as_user ptr s \<lbrace>\<lambda>_. valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sa. valid_queues 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_queues_2 (ready_queues 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)) proof (prove)
goal (1 subgoal):
 1. \<And>sa y a b tcb d p. \<lbrakk>\<forall>d p. (\<forall>t\<in>set (ready_queues sa d p). is_etcb_at t sa \<and> etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t sa \<and> (\<exists>ko. kheap sa t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> runnable (tcb_state tcb)))) \<and> distinct (ready_queues sa d p); get_tcb ptr sa = Some y; (a, b) \<in> fst (s (arch_tcb_context_get (tcb_arch y))); kheap sa ptr = Some (TCB tcb); ptr \<in> set (ready_queues sa d p)\<rbrakk> \<Longrightarrow> runnable (tcb_state y) proof (prove)
goal (1 subgoal):
 1. \<And>sa y a b tcb d p. \<lbrakk>get_tcb ptr sa = Some y; (a, b) \<in> fst (s (arch_tcb_context_get (tcb_arch y))); kheap sa ptr = Some (TCB tcb); ptr \<in> set (ready_queues sa d p); \<forall>p. (\<forall>t\<in>set (ready_queues sa d p). is_etcb_at t sa \<and> etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t sa \<and> (\<exists>ko. kheap sa t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> runnable (tcb_state tcb)))) \<and> distinct (ready_queues sa d p)\<rbrakk> \<Longrightarrow> runnable (tcb_state y) proof (prove)
goal (1 subgoal):
 1. \<And>sa y a b tcb d p. \<lbrakk>get_tcb ptr sa = Some y; (a, b) \<in> fst (s (arch_tcb_context_get (tcb_arch y))); kheap sa ptr = Some (TCB tcb); ptr \<in> set (ready_queues sa d p); (\<forall>t\<in>set (ready_queues sa d p). is_etcb_at t sa \<and> etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t sa \<and> (\<exists>ko. kheap sa t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> runnable (tcb_state tcb)))) \<and> distinct (ready_queues sa d p)\<rbrakk> \<Longrightarrow> runnable (tcb_state y) proof (prove)
goal (1 subgoal):
 1. \<And>sa y a b tcb d p. \<lbrakk>get_tcb ptr sa = Some y; (a, b) \<in> fst (s (arch_tcb_context_get (tcb_arch y))); kheap sa ptr = Some (TCB tcb); ptr \<in> set (ready_queues sa d p); \<forall>t\<in>set (ready_queues sa d p). is_etcb_at t sa \<and> etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t sa \<and> (\<exists>ko. kheap sa t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> runnable (tcb_state tcb))); distinct (ready_queues sa d p)\<rbrakk> \<Longrightarrow> runnable (tcb_state y) proof (prove)
goal (1 subgoal):
 1. \<And>sa y a b tcb d p. \<lbrakk>get_tcb ptr sa = Some y; (a, b) \<in> fst (s (arch_tcb_context_get (tcb_arch y))); kheap sa ptr = Some (TCB tcb); ptr \<in> set (ready_queues sa d p); distinct (ready_queues sa d p); is_etcb_at ptr sa; etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) ptr sa; runnable (tcb_state tcb)\<rbrakk> \<Longrightarrow> runnable (tcb_state y) proof (prove)
goal:
No subgoals!