theory KHeap_R

lemma set_ntfn_valid_queues'[wp]:
  "\<lbrace>valid_queues'\<rbrace> setNotification p ntfn \<lbrace>\<lambda>rv. valid_queues'\<rbrace>" apply (unfold setNotification_def) apply (rule setObject_ntfn_pre) apply (simp only: valid_queues'_def imp_conv_disj
                    obj_at'_real_def) apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift) apply (rule setObject_ko_wp_at) apply simp apply (simp add: objBits_simps') apply simp apply (wp updateObject_default_inv | simp)+ apply (clarsimp simp: projectKOs ko_wp_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues'\<rbrace> setNotification p ntfn \<lbrace>\<lambda>rv. valid_queues'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues'\<rbrace> setObject p ntfn \<lbrace>\<lambda>rv. valid_queues'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues' and ntfn_at' p\<rbrace> setObject p ntfn \<lbrace>\<lambda>rv. valid_queues'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<forall>d p t. \<not> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> inQ d p obj) t s \<or> t \<in> set (ksReadyQueues s (d, p))) and ntfn_at' p\<rbrace> setObject p ntfn \<lbrace>\<lambda>rv s. \<forall>d p t. \<not> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> inQ d p obj) t s \<or> t \<in> set (ksReadyQueues s (d, p))\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>d pa t. \<lbrace>?P6 d pa t\<rbrace> setObject p ntfn \<lbrace>\<lambda>rv s. \<not> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> inQ d pa obj) t s\<rbrace>
 2. \<And>d pa t. \<lbrace>?P'6 d pa t\<rbrace> setObject p ntfn \<lbrace>\<lambda>rv s. t \<in> set (ksReadyQueues s (d, pa))\<rbrace>
 3. \<And>s. ((\<lambda>s. \<forall>d p t. \<not> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> inQ d p obj) t s \<or> t \<in> set (ksReadyQueues s (d, p))) and ntfn_at' p) s \<Longrightarrow> \<forall>x xa xb. ?P6 x xa xb s \<or> ?P'6 x xa xb s proof (prove)
goal (5 subgoals):
 1. \<And>d pa t ko s x y n. updateObject ntfn ko p y n s = updateObject_default ntfn ko p y n s
 2. \<And>d p t v'. objBits v' = ?n7 d p t
 3. \<And>d p t. 1 < 2 ^ ?n7 d p t
 4. \<And>d pa t. \<lbrace>?P'6 d pa t\<rbrace> setObject p ntfn \<lbrace>\<lambda>rv s. t \<in> set (ksReadyQueues s (d, pa))\<rbrace>
 5. \<And>s. ((\<lambda>s. \<forall>d p t. \<not> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> inQ d p obj) t s \<or> t \<in> set (ksReadyQueues s (d, p))) and ntfn_at' p) s \<Longrightarrow> \<forall>x xa xb. (ntfn_at' p s \<longrightarrow> \<not> ko_wp_at' (if p = xb then K (\<exists>obj. projectKO_opt (injectKO ntfn) = Some obj \<and> inQ x xa obj) else (\<lambda>a. \<exists>obj. projectKO_opt a = Some obj \<and> inQ x xa obj)) xb s) \<or> ?P'6 x xa xb s proof (prove)
goal (4 subgoals):
 1. \<And>d p t v'. objBits v' = ?n7 d p t
 2. \<And>d p t. 1 < 2 ^ ?n7 d p t
 3. \<And>d pa t. \<lbrace>?P'6 d pa t\<rbrace> setObject p ntfn \<lbrace>\<lambda>rv s. t \<in> set (ksReadyQueues s (d, pa))\<rbrace>
 4. \<And>s. ((\<lambda>s. \<forall>d p t. \<not> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> inQ d p obj) t s \<or> t \<in> set (ksReadyQueues s (d, p))) and ntfn_at' p) s \<Longrightarrow> \<forall>x xa xb. (ntfn_at' p s \<longrightarrow> \<not> ko_wp_at' (if p = xb then K (\<exists>obj. projectKO_opt (injectKO ntfn) = Some obj \<and> inQ x xa obj) else (\<lambda>a. \<exists>obj. projectKO_opt a = Some obj \<and> inQ x xa obj)) xb s) \<or> ?P'6 x xa xb s proof (prove)
goal (3 subgoals):
 1. \<And>d p t. 1 < 2 ^ 4
 2. \<And>d pa t. \<lbrace>?P'6 d pa t\<rbrace> setObject p ntfn \<lbrace>\<lambda>rv s. t \<in> set (ksReadyQueues s (d, pa))\<rbrace>
 3. \<And>s. ((\<lambda>s. \<forall>d p t. \<not> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> inQ d p obj) t s \<or> t \<in> set (ksReadyQueues s (d, p))) and ntfn_at' p) s \<Longrightarrow> \<forall>x xa xb. (ntfn_at' p s \<longrightarrow> \<not> ko_wp_at' (if p = xb then K (\<exists>obj. projectKO_opt (injectKO ntfn) = Some obj \<and> inQ x xa obj) else (\<lambda>a. \<exists>obj. projectKO_opt a = Some obj \<and> inQ x xa obj)) xb s) \<or> ?P'6 x xa xb s proof (prove)
goal (2 subgoals):
 1. \<And>d pa t. \<lbrace>?P'6 d pa t\<rbrace> setObject p ntfn \<lbrace>\<lambda>rv s. t \<in> set (ksReadyQueues s (d, pa))\<rbrace>
 2. \<And>s. ((\<lambda>s. \<forall>d p t. \<not> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> inQ d p obj) t s \<or> t \<in> set (ksReadyQueues s (d, p))) and ntfn_at' p) s \<Longrightarrow> \<forall>x xa xb. (ntfn_at' p s \<longrightarrow> \<not> ko_wp_at' (if p = xb then K (\<exists>obj. projectKO_opt (injectKO ntfn) = Some obj \<and> inQ x xa obj) else (\<lambda>a. \<exists>obj. projectKO_opt a = Some obj \<and> inQ x xa obj)) xb s) \<or> ?P'6 x xa xb s proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>d p t. ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> inQ d p obj) t s \<longrightarrow> t \<in> set (ksReadyQueues s (d, p))) \<and> ntfn_at' p s \<Longrightarrow> \<forall>x xa. ko_wp_at' (\<lambda>y. \<exists>obj. projectKO_opt (KONotification ntfn) = Some obj \<and> inQ x xa obj) p s \<longrightarrow> p \<in> set (ksReadyQueues s (x, xa)) proof (prove)
goal:
No subgoals!