theory IpcCancel_R

lemma cancelSignal_queues[wp]:
  "\<lbrace>Invariants_H.valid_queues and st_tcb_at' (Not \<circ> runnable') t\<rbrace>
   cancelSignal t ae \<lbrace>\<lambda>_. Invariants_H.valid_queues \<rbrace>" apply (simp add: cancelSignal_def) apply (wp sts_valid_queues) apply (rule_tac Q="\<lambda>_ s. \<forall>p. t \<notin> set (ksReadyQueues s p)" in hoare_post_imp, simp) apply (wp hoare_vcg_all_lift) apply (wpc) apply (wp)+ apply (rule_tac Q="\<lambda>_ s. Invariants_H.valid_queues s \<and> (\<forall>p. t \<notin> set (ksReadyQueues s p))" in hoare_post_imp) apply (clarsimp) apply (wp) apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Invariants_H.valid_queues and st_tcb_at' (Not \<circ> runnable') t\<rbrace> cancelSignal t ae \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>Invariants_H.valid_queues and st_tcb_at' (Not \<circ> runnable') t\<rbrace> do ntfn <- getNotification ae;
y <- assert (case ntfnObj ntfn of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False);
ntfn' <- case remove1 t (ntfnQueue (ntfnObj ntfn)) of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. remove1 t (ntfnQueue (ntfnObj ntfn))) (ntfnObj ntfn);
y <- setNotification ae (ntfnObj_update (\<lambda>_. ntfn') ntfn);
setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>ntfn y ntfn'. \<lbrace>?P'6 ntfn y ntfn'\<rbrace> setNotification ae (ntfnObj_update (\<lambda>_. ntfn') ntfn) \<lbrace>\<lambda>rv s. (\<exists>p. t \<in> set (ksReadyQueues s p)) \<longrightarrow> runnable' Structures_H.thread_state.Inactive\<rbrace>
 2. \<And>ntfn y. \<lbrace>?B2 ntfn y\<rbrace> case remove1 t (ntfnQueue (ntfnObj ntfn)) of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. remove1 t (ntfnQueue (ntfnObj ntfn))) (ntfnObj ntfn) \<lbrace>\<lambda>ntfn' s. Invariants_H.valid_queues s \<and> ?P'6 ntfn y ntfn' s\<rbrace>
 3. \<And>ntfn. \<lbrace>?B1 ntfn\<rbrace> assert (case ntfnObj ntfn of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False) \<lbrace>?B2 ntfn\<rbrace>
 4. \<lbrace>?Q\<rbrace> getNotification ae \<lbrace>?B1\<rbrace>
 5. \<And>s. (Invariants_H.valid_queues and st_tcb_at' (Not \<circ> runnable') t) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>ntfn y ntfn'. \<lbrace>?P'6 ntfn y ntfn'\<rbrace> setNotification ae (ntfnObj_update (\<lambda>_. ntfn') ntfn) \<lbrace>\<lambda>_ s. \<forall>p. t \<notin> set (ksReadyQueues s p)\<rbrace>
 2. \<And>ntfn y. \<lbrace>?B2 ntfn y\<rbrace> case remove1 t (ntfnQueue (ntfnObj ntfn)) of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. remove1 t (ntfnQueue (ntfnObj ntfn))) (ntfnObj ntfn) \<lbrace>\<lambda>ntfn' s. Invariants_H.valid_queues s \<and> ?P'6 ntfn y ntfn' s\<rbrace>
 3. \<And>ntfn. \<lbrace>?B1 ntfn\<rbrace> assert (case ntfnObj ntfn of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False) \<lbrace>?B2 ntfn\<rbrace>
 4. \<lbrace>?Q\<rbrace> getNotification ae \<lbrace>?B1\<rbrace>
 5. \<And>s. (Invariants_H.valid_queues and st_tcb_at' (Not \<circ> runnable') t) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>ntfn y. \<lbrace>?B2 ntfn y\<rbrace> case remove1 t (ntfnQueue (ntfnObj ntfn)) of [] \<Rightarrow> return $ Structures_H.ntfn.IdleNtfn | a # list \<Rightarrow> return $ ntfnQueue_update (\<lambda>_. remove1 t (ntfnQueue (ntfnObj ntfn))) (ntfnObj ntfn) \<lbrace>\<lambda>ntfn' s. Invariants_H.valid_queues s \<and> (\<forall>x. t \<notin> set (ksReadyQueues s x))\<rbrace>
 2. \<And>ntfn. \<lbrace>?B1 ntfn\<rbrace> assert (case ntfnObj ntfn of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False) \<lbrace>?B2 ntfn\<rbrace>
 3. \<lbrace>?Q\<rbrace> getNotification ae \<lbrace>?B1\<rbrace>
 4. \<And>s. (Invariants_H.valid_queues and st_tcb_at' (Not \<circ> runnable') t) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>ntfn y. remove1 t (ntfnQueue (ntfnObj ntfn)) = [] \<Longrightarrow> \<lbrace>?R23 ntfn y\<rbrace> return $ Structures_H.ntfn.IdleNtfn \<lbrace>\<lambda>ntfn' s. Invariants_H.valid_queues s \<and> (\<forall>x. t \<notin> set (ksReadyQueues s x))\<rbrace>
 2. \<And>ntfn y x21 x22. remove1 t (ntfnQueue (ntfnObj ntfn)) = x21 # x22 \<Longrightarrow> \<lbrace>?R24 ntfn y x21 x22\<rbrace> return $ ntfnQueue_update (\<lambda>_. remove1 t (ntfnQueue (ntfnObj ntfn))) (ntfnObj ntfn) \<lbrace>\<lambda>ntfn' s. Invariants_H.valid_queues s \<and> (\<forall>x. t \<notin> set (ksReadyQueues s x))\<rbrace>
 3. \<And>ntfn. \<lbrace>?B1 ntfn\<rbrace> assert (case ntfnObj ntfn of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False) \<lbrace>\<lambda>y s. (remove1 t (ntfnQueue (ntfnObj ntfn)) = [] \<longrightarrow> ?R23 ntfn y s) \<and> (\<forall>x xa. remove1 t (ntfnQueue (ntfnObj ntfn)) = x # xa \<longrightarrow> ?R24 ntfn y x xa s)\<rbrace>
 4. \<lbrace>?Q\<rbrace> getNotification ae \<lbrace>?B1\<rbrace>
 5. \<And>s. (Invariants_H.valid_queues and st_tcb_at' (Not \<circ> runnable') t) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> getNotification ae \<lbrace>\<lambda>ntfn s. (case ntfnObj ntfn of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False) \<longrightarrow> (remove1 t (ntfnQueue (ntfnObj ntfn)) = [] \<longrightarrow> Invariants_H.valid_queues s \<and> (\<forall>x. t \<notin> set (ksReadyQueues s x))) \<and> (\<forall>x xa. remove1 t (ntfnQueue (ntfnObj ntfn)) = x # xa \<longrightarrow> Invariants_H.valid_queues s \<and> (\<forall>x. t \<notin> set (ksReadyQueues s x)))\<rbrace>
 2. \<And>s. (Invariants_H.valid_queues and st_tcb_at' (Not \<circ> runnable') t) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>rv s. Invariants_H.valid_queues s \<and> (\<forall>p. t \<notin> set (ksReadyQueues s p)) \<Longrightarrow> (case ntfnObj rv of Structures_H.ntfn.WaitingNtfn x \<Rightarrow> True | _ \<Rightarrow> False) \<longrightarrow> (remove1 t (ntfnQueue (ntfnObj rv)) = [] \<longrightarrow> Invariants_H.valid_queues s \<and> (\<forall>x. t \<notin> set (ksReadyQueues s x))) \<and> (\<forall>x xa. remove1 t (ntfnQueue (ntfnObj rv)) = x # xa \<longrightarrow> Invariants_H.valid_queues s \<and> (\<forall>x. t \<notin> set (ksReadyQueues s x)))
 2. \<lbrace>?Q\<rbrace> getNotification ae \<lbrace>\<lambda>_ s. Invariants_H.valid_queues s \<and> (\<forall>p. t \<notin> set (ksReadyQueues s p))\<rbrace>
 3. \<And>s. (Invariants_H.valid_queues and st_tcb_at' (Not \<circ> runnable') t) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> getNotification ae \<lbrace>\<lambda>_ s. Invariants_H.valid_queues s \<and> (\<forall>p. t \<notin> set (ksReadyQueues s p))\<rbrace>
 2. \<And>s. (Invariants_H.valid_queues and st_tcb_at' (Not \<circ> runnable') t) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (Invariants_H.valid_queues and st_tcb_at' (Not \<circ> runnable') t) s \<Longrightarrow> Invariants_H.valid_queues s \<and> (\<forall>p. t \<notin> set (ksReadyQueues s p)) proof (prove)
goal:
No subgoals!