theory Finalise_R

lemma unbindMaybeNotification_ct_not_ksQ:
 "\<lbrace>invs' and ct_in_state' simple' and sch_act_sane
          and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace>
   unbindMaybeNotification t
   \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>" apply (simp add: unbindMaybeNotification_def) apply (rule hoare_seq_ext[OF _ get_ntfn_sp']) apply (case_tac "ntfnBoundTCB ntfn", simp, wp, simp+) apply (rule hoare_pre) apply wp apply (wps setBoundNotification_ct') apply (wp sbn_ksQ) apply (wps setNotification_ksCurThread, wp) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> unbindMaybeNotification t \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> do ntfn <- getNotification t;
case ntfnBoundTCB ntfn of None \<Rightarrow> return () | Some ta \<Rightarrow> do y <- setNotification t (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None ta
od
od \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfn. \<lbrace>invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p)) and ko_at' ntfn t\<rbrace> case ntfnBoundTCB ntfn of None \<Rightarrow> return () | Some ta \<Rightarrow> do y <- setNotification t (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None ta
od \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfn a. ntfnBoundTCB ntfn = Some a \<Longrightarrow> \<lbrace>invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p)) and ko_at' ntfn t\<rbrace> do y <- setNotification t (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None a
od \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ntfn a. ntfnBoundTCB ntfn = Some a \<Longrightarrow> \<lbrace>?Q13 ntfn a\<rbrace> do y <- setNotification t (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None a
od \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>
 2. \<And>ntfn a s. \<lbrakk>ntfnBoundTCB ntfn = Some a; (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p)) and ko_at' ntfn t) s\<rbrakk> \<Longrightarrow> ?Q13 ntfn a s proof (prove)
goal (3 subgoals):
 1. \<And>ntfn a y. ntfnBoundTCB ntfn = Some a \<Longrightarrow> \<lbrace>?B17 ntfn a y\<rbrace> setBoundNotification None a \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>
 2. \<And>ntfn a. ntfnBoundTCB ntfn = Some a \<Longrightarrow> \<lbrace>?Q13 ntfn a\<rbrace> setNotification t (ntfnBoundTCB_update (\<lambda>_. None) ntfn) \<lbrace>?B17 ntfn a\<rbrace>
 3. \<And>ntfn a s. \<lbrakk>ntfnBoundTCB ntfn = Some a; (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p)) and ko_at' ntfn t) s\<rbrakk> \<Longrightarrow> ?Q13 ntfn a s proof (prove)
goal (3 subgoals):
 1. \<And>ntfn a y prev_s. ntfnBoundTCB ntfn = Some a \<Longrightarrow> \<lbrace>?P19 ntfn a y prev_s\<rbrace> setBoundNotification None a \<lbrace>\<lambda>rv s'. ksCurThread prev_s \<notin> set (ksReadyQueues s' p)\<rbrace>
 2. \<And>ntfn a. ntfnBoundTCB ntfn = Some a \<Longrightarrow> \<lbrace>?Q13 ntfn a\<rbrace> setNotification t (ntfnBoundTCB_update (\<lambda>_. None) ntfn) \<lbrace>\<lambda>y s. ?P19 ntfn a y s s\<rbrace>
 3. \<And>ntfn a s. \<lbrakk>ntfnBoundTCB ntfn = Some a; (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p)) and ko_at' ntfn t) s\<rbrakk> \<Longrightarrow> ?Q13 ntfn a s proof (prove)
goal (2 subgoals):
 1. \<And>ntfn a. ntfnBoundTCB ntfn = Some a \<Longrightarrow> \<lbrace>?Q13 ntfn a\<rbrace> setNotification t (ntfnBoundTCB_update (\<lambda>_. None) ntfn) \<lbrace>\<lambda>y s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>
 2. \<And>ntfn a s. \<lbrakk>ntfnBoundTCB ntfn = Some a; (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p)) and ko_at' ntfn t) s\<rbrakk> \<Longrightarrow> ?Q13 ntfn a s proof (prove)
goal (1 subgoal):
 1. \<And>ntfn a s. \<lbrakk>ntfnBoundTCB ntfn = Some a; (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p)) and ko_at' ntfn t) s\<rbrakk> \<Longrightarrow> ksCurThread s \<notin> set (ksReadyQueues s p) proof (prove)
goal:
No subgoals!