theory IpcCancel_AI

lemma cancel_signal_valid_objs[wp]:
  "\<lbrace>valid_objs\<rbrace> cancel_signal t ntfnptr \<lbrace>\<lambda>_. valid_objs\<rbrace>" apply (simp add: cancel_signal_def) apply (rule hoare_seq_ext [OF _ get_simple_ko_sp]) apply (rule hoare_pre) apply (wp set_simple_ko_valid_objs
       | simp only: valid_inactive
       | simp
       | wpc)+ apply (clarsimp simp: ep_redux_simps cong: list.case_cong) apply (erule(1) obj_at_valid_objsE) apply (clarsimp simp: valid_obj_def valid_ntfn_def) apply (auto split: option.splits list.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> cancel_signal t ntfnptr \<lbrace>\<lambda>_. valid_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> do ntfn <- get_notification ntfnptr;
queue <- case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> return queue | _ \<Rightarrow> fail;
y <- set_notification ntfnptr (ntfn_set_obj ntfn (case remove1 t queue of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (remove1 t queue)));
set_thread_state t Inactive
od \<lbrace>\<lambda>_. valid_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfn. \<lbrace>ko_at (Notification ntfn) ntfnptr and valid_objs\<rbrace> do queue <- case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> return queue | _ \<Rightarrow> fail;
y <- set_notification ntfnptr (ntfn_set_obj ntfn (case remove1 t queue of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (remove1 t queue)));
set_thread_state t Inactive
od \<lbrace>\<lambda>_. valid_objs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ntfn. \<lbrace>?Q4 ntfn\<rbrace> do queue <- case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> return queue | _ \<Rightarrow> fail;
y <- set_notification ntfnptr (ntfn_set_obj ntfn (case remove1 t queue of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (remove1 t queue)));
set_thread_state t Inactive
od \<lbrace>\<lambda>_. valid_objs\<rbrace>
 2. \<And>ntfn s. (ko_at (Notification ntfn) ntfnptr and valid_objs) s \<Longrightarrow> ?Q4 ntfn s proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s. ko_at (Notification ntfn) ntfnptr s \<and> valid_objs s \<Longrightarrow> \<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> valid_ntfn (ntfn_set_obj ntfn (case remove1 t x of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (remove1 t x))) s proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s x. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; valid_objs s; ntfn_obj ntfn = WaitingNtfn x\<rbrakk> \<Longrightarrow> distinct (remove1 t x) \<and> (\<forall>t\<in>set (remove1 t x). tcb_at t s) \<and> (case ntfn_bound_tcb ntfn of None \<Rightarrow> True | Some ta \<Rightarrow> tcb_at ta s \<and> (case remove1 t x of [] \<Rightarrow> True | a # list \<Rightarrow> remove1 t x = [ta])) proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s x ko. \<lbrakk>valid_objs s; ntfn_obj ntfn = WaitingNtfn x; kheap s ntfnptr = Some ko; Notification ntfn = ko; valid_obj ntfnptr ko s\<rbrakk> \<Longrightarrow> distinct (remove1 t x) \<and> (\<forall>t\<in>set (remove1 t x). tcb_at t s) \<and> (case ntfn_bound_tcb ntfn of None \<Rightarrow> True | Some ta \<Rightarrow> tcb_at ta s \<and> (case remove1 t x of [] \<Rightarrow> True | a # list \<Rightarrow> remove1 t x = [ta])) proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s x. \<lbrakk>valid_objs s; ntfn_obj ntfn = WaitingNtfn x; kheap s ntfnptr = Some (Notification ntfn); x \<noteq> []; \<forall>t\<in>set x. tcb_at t s; distinct x; case ntfn_bound_tcb ntfn of None \<Rightarrow> True | Some tcb \<Rightarrow> x = [tcb]; valid_bound_tcb (ntfn_bound_tcb ntfn) s\<rbrakk> \<Longrightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> True | Some ta \<Rightarrow> tcb_at ta s \<and> (case remove1 t x of [] \<Rightarrow> True | a # list \<Rightarrow> remove1 t x = [ta]) proof (prove)
goal:
No subgoals!