theory DetSchedSchedule_AI

lemma as_user_valid_blocked[wp]:
  "\<lbrace>valid_blocked and ct_in_q\<rbrace> as_user tp S \<lbrace>\<lambda>_. valid_blocked and ct_in_q\<rbrace>" apply (simp add: as_user_def set_object_def get_object_def | wpc | wp)+ apply (clarsimp simp: valid_blocked_def st_tcb_at_kh_if_split st_tcb_at_def obj_at_def) apply (drule_tac x=tp in spec) apply (drule get_tcb_SomeD, simp) apply (simp add: ct_in_q_def) apply (case_tac "tp = cur_thread s"; clarsimp simp: st_tcb_at_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_blocked and ct_in_q\<rbrace> as_user tp S \<lbrace>\<lambda>_. valid_blocked and ct_in_q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_blocked s \<and> ct_in_q s \<Longrightarrow> (\<exists>y. get_tcb tp s = Some y) \<longrightarrow> (\<forall>x\<in>fst (S (arch_tcb_context_get (tcb_arch (the (get_tcb tp s))))). \<forall>xa xb. x = (xa, xb) \<longrightarrow> (\<exists>y. kheap s tp = Some y) \<longrightarrow> a_type (the (kheap s tp)) = ATCB \<longrightarrow> valid_blocked_2 (ready_queues s) (\<lambda>a. if a = tp then Some (TCB (the (get_tcb tp s)\<lparr>tcb_arch := arch_tcb_context_set xb (tcb_arch (the (get_tcb tp s)))\<rparr>)) else kheap s a) (scheduler_action s) (cur_thread s) \<and> ct_in_q (s\<lparr>kheap := \<lambda>a. if a = tp then Some (TCB (the (get_tcb tp s)\<lparr>tcb_arch := arch_tcb_context_set xb (tcb_arch (the (get_tcb tp s)))\<rparr>)) else kheap s a\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s y x xa tcb. \<lbrakk>\<forall>t. not_queued t s \<longrightarrow> (\<forall>st. (\<exists>ko. kheap s t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> st = tcb_state tcb)) \<longrightarrow> t \<noteq> cur_thread s \<longrightarrow> scheduler_action s \<noteq> switch_thread t \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart); ct_in_q s; (x, xa) \<in> fst (S (arch_tcb_context_get (tcb_arch y))); get_tcb tp s = Some y; kheap s tp = Some (TCB tcb)\<rbrakk> \<Longrightarrow> (not_queued tp s \<longrightarrow> tp \<noteq> cur_thread s \<longrightarrow> scheduler_action s \<noteq> switch_thread tp \<longrightarrow> tcb_state y \<noteq> Running \<and> tcb_state y \<noteq> Restart) \<and> ct_in_q (s\<lparr>kheap := \<lambda>a. if a = tp then Some (TCB (y\<lparr>tcb_arch := arch_tcb_context_set xa (tcb_arch y)\<rparr>)) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s y x xa tcb. \<lbrakk>ct_in_q s; (x, xa) \<in> fst (S (arch_tcb_context_get (tcb_arch y))); get_tcb tp s = Some y; kheap s tp = Some (TCB tcb); not_queued tp s \<longrightarrow> (\<forall>st. (\<exists>ko. kheap s tp = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> st = tcb_state tcb)) \<longrightarrow> tp \<noteq> cur_thread s \<longrightarrow> scheduler_action s \<noteq> switch_thread tp \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart)\<rbrakk> \<Longrightarrow> (not_queued tp s \<longrightarrow> tp \<noteq> cur_thread s \<longrightarrow> scheduler_action s \<noteq> switch_thread tp \<longrightarrow> tcb_state y \<noteq> Running \<and> tcb_state y \<noteq> Restart) \<and> ct_in_q (s\<lparr>kheap := \<lambda>a. if a = tp then Some (TCB (y\<lparr>tcb_arch := arch_tcb_context_set xa (tcb_arch y)\<rparr>)) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s y x xa tcb. \<lbrakk>ct_in_q s; (x, xa) \<in> fst (S (arch_tcb_context_get (tcb_arch tcb))); y = tcb; not_queued tp s \<longrightarrow> tp \<noteq> cur_thread s \<longrightarrow> scheduler_action s \<noteq> switch_thread tp \<longrightarrow> tcb_state tcb \<noteq> Running \<and> tcb_state tcb \<noteq> Restart; kheap s tp = Some (TCB tcb)\<rbrakk> \<Longrightarrow> ct_in_q (s\<lparr>kheap := \<lambda>a. if a = tp then Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set xa (tcb_arch tcb)\<rparr>)) else kheap s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s y x xa tcb. \<lbrakk>st_tcb_at runnable (cur_thread s) s \<longrightarrow> (\<exists>d p. cur_thread s \<in> set (ready_queues s d p)); (x, xa) \<in> fst (S (arch_tcb_context_get (tcb_arch tcb))); y = tcb; not_queued tp s \<longrightarrow> tp \<noteq> cur_thread s \<longrightarrow> scheduler_action s \<noteq> switch_thread tp \<longrightarrow> tcb_state tcb \<noteq> Running \<and> tcb_state tcb \<noteq> Restart; kheap s tp = Some (TCB tcb)\<rbrakk> \<Longrightarrow> st_tcb_at runnable (cur_thread s) (s\<lparr>kheap := \<lambda>a. if a = tp then Some (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set xa (tcb_arch tcb)\<rparr>)) else kheap s a\<rparr>) \<longrightarrow> (\<exists>d p. cur_thread s \<in> set (ready_queues s d p)) proof (prove)
goal:
No subgoals!