theory DetSchedSchedule_AI

lemma set_bound_notification_valid_blocked[wp]:
  "\<lbrace>valid_blocked\<rbrace> set_bound_notification t ntfn \<lbrace>\<lambda>_. valid_blocked\<rbrace>" apply (simp add: set_bound_notification_def) apply (simp add: set_object_def get_object_def | wp)+ apply (clarsimp simp: valid_blocked_def) apply (drule_tac x=ta in spec, clarsimp) apply (drule_tac x=st in spec) apply (simp only: st_tcb_at_kh_if_split) apply (simp add: st_tcb_def2 split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_blocked\<rbrace> set_bound_notification t ntfn \<lbrace>\<lambda>_. valid_blocked\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_blocked\<rbrace> do tcb <- gets_the (get_tcb t);
set_object t (TCB (tcb\<lparr>tcb_bound_notification := ntfn\<rparr>))
od \<lbrace>\<lambda>_. valid_blocked\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_blocked s \<Longrightarrow> (\<exists>y. get_tcb t s = Some y) \<longrightarrow> (\<exists>y. kheap s t = Some y) \<longrightarrow> a_type (the (kheap s t)) = ATCB \<longrightarrow> valid_blocked_2 (ready_queues s) (\<lambda>a. if a = t then Some (TCB (the (get_tcb t s)\<lparr>tcb_bound_notification := ntfn\<rparr>)) else kheap s a) (scheduler_action s) (cur_thread s) proof (prove)
goal (1 subgoal):
 1. \<And>s y tcb ta st. \<lbrakk>\<forall>t. not_queued t s \<longrightarrow> (\<forall>st. st_tcb_at ((=) st) t s \<longrightarrow> t \<noteq> cur_thread s \<longrightarrow> scheduler_action s \<noteq> switch_thread t \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart); get_tcb t s = Some y; kheap s t = Some (TCB tcb); not_queued ta s; st_tcb_at_kh ((=) st) ta (\<lambda>a. if a = t then Some (TCB (y\<lparr>tcb_bound_notification := ntfn\<rparr>)) else kheap s a); ta \<noteq> cur_thread s; scheduler_action s \<noteq> switch_thread ta\<rbrakk> \<Longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart proof (prove)
goal (1 subgoal):
 1. \<And>s y tcb ta st. \<lbrakk>get_tcb t s = Some y; kheap s t = Some (TCB tcb); not_queued ta s; st_tcb_at_kh ((=) st) ta (\<lambda>a. if a = t then Some (TCB (y\<lparr>tcb_bound_notification := ntfn\<rparr>)) else kheap s a); ta \<noteq> cur_thread s; scheduler_action s \<noteq> switch_thread ta; \<forall>st. st_tcb_at ((=) st) ta s \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart\<rbrakk> \<Longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart proof (prove)
goal (1 subgoal):
 1. \<And>s y tcb ta st. \<lbrakk>get_tcb t s = Some y; kheap s t = Some (TCB tcb); not_queued ta s; st_tcb_at_kh ((=) st) ta (\<lambda>a. if a = t then Some (TCB (y\<lparr>tcb_bound_notification := ntfn\<rparr>)) else kheap s a); ta \<noteq> cur_thread s; scheduler_action s \<noteq> switch_thread ta; st_tcb_at ((=) st) ta s \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart\<rbrakk> \<Longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart proof (prove)
goal (1 subgoal):
 1. \<And>s y tcb ta st. \<lbrakk>get_tcb t s = Some y; kheap s t = Some (TCB tcb); not_queued ta s; if ta = t then \<exists>tcb. Some (TCB (y\<lparr>tcb_bound_notification := ntfn\<rparr>)) = Some (TCB tcb) \<and> st = tcb_state tcb else st_tcb_at_kh ((=) st) ta (kheap s); ta \<noteq> cur_thread s; scheduler_action s \<noteq> switch_thread ta; st_tcb_at ((=) st) ta s \<longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart\<rbrakk> \<Longrightarrow> st \<noteq> Running \<and> st \<noteq> Restart proof (prove)
goal:
No subgoals!