theory KHeap_DR

lemma dcorres_do_unbind_notification:
  "dcorres dc \<top> (valid_etcbs and valid_state and not_idle_thread t) (PageTableUnmap_D.do_unbind_notification t) (IpcCancel_A.do_unbind_notification ntfnptr ntfn t)" apply (clarsimp) apply (rule corres_guard_imp) apply (rule corres_dummy_return_pl[where b="()"]) apply (rule corres_split[OF corres_dummy_set_notification]) apply (clarsimp simp: tcb_slots) apply (rule set_bound_notification_corres[where ntfn_opt=None, unfolded infer_tcb_bound_notification_def
                                       not_idle_thread_def tcb_slots, simplified]) apply wp+ apply simp apply (clarsimp simp: not_idle_thread_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (valid_etcbs and valid_state and not_idle_thread t) (PageTableUnmap_D.do_unbind_notification t) (IpcCancel_A.do_unbind_notification ntfnptr ntfn t) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (valid_etcbs and valid_state and not_idle_thread t) (PageTableUnmap_D.do_unbind_notification t) (do y <- set_notification ntfnptr (ntfn_set_bound_tcb ntfn None);
set_bound_notification t None
od) proof (prove)
goal (3 subgoals):
 1. dcorres dc ?Q ?Q' (PageTableUnmap_D.do_unbind_notification t) (do y <- set_notification ntfnptr (ntfn_set_bound_tcb ntfn None);
set_bound_notification t None
od)
 2. \<And>s. True \<Longrightarrow> ?Q s
 3. \<And>s. (valid_etcbs and valid_state and not_idle_thread t) s \<Longrightarrow> ?Q' s proof (prove)
goal (3 subgoals):
 1. dcorres dc ?Q ?Q' (do return ();
PageTableUnmap_D.do_unbind_notification t
od) (do y <- set_notification ntfnptr (ntfn_set_bound_tcb ntfn None);
set_bound_notification t None
od)
 2. \<And>s. True \<Longrightarrow> ?Q s
 3. \<And>s. (valid_etcbs and valid_state and not_idle_thread t) s \<Longrightarrow> ?Q' s proof (prove)
goal (5 subgoals):
 1. \<And>rv rv'. dc rv rv' \<Longrightarrow> dcorres dc (?R6 rv) (?R'6 rv') (K_bind (PageTableUnmap_D.do_unbind_notification t) rv) (set_bound_notification t None)
 2. \<lbrace>?Q6\<rbrace> return () \<lbrace>?R6\<rbrace>
 3. \<lbrace>?Q'6\<rbrace> set_notification ntfnptr (ntfn_set_bound_tcb ntfn None) \<lbrace>?R'6\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 5. \<And>s. (valid_etcbs and valid_state and not_idle_thread t) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s proof (prove)
goal (5 subgoals):
 1. dcorres dc (?R6 ()) (?R'6 ()) (KHeap_D.set_cap (t, 6) cdl_cap.NullCap) (set_bound_notification t None)
 2. \<lbrace>?Q6\<rbrace> return () \<lbrace>?R6\<rbrace>
 3. \<lbrace>?Q'6\<rbrace> set_notification ntfnptr (ntfn_set_bound_tcb ntfn None) \<lbrace>?R'6\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 5. \<And>s. (valid_etcbs and valid_state and not_idle_thread t) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q6\<rbrace> return () \<lbrace>\<lambda>a b. True\<rbrace>
 2. \<lbrace>?Q'6\<rbrace> set_notification ntfnptr (ntfn_set_bound_tcb ntfn None) \<lbrace>\<lambda>a. (\<lambda>s. t \<noteq> idle_thread s) and valid_etcbs and (\<lambda>y. cdl_cap.NullCap = cdl_cap.NullCap)\<rbrace>
 3. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 4. \<And>s. (valid_etcbs and valid_state and not_idle_thread t) s \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s proof (prove)
goal (2 subgoals):
 1. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True)) s
 2. \<And>s. (valid_etcbs and valid_state and not_idle_thread t) s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. t \<noteq> idle_thread s \<and> valid_etcbs s \<and> cdl_cap.NullCap = cdl_cap.NullCap)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_etcbs and valid_state and not_idle_thread t) s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. t \<noteq> idle_thread s \<and> valid_etcbs s \<and> cdl_cap.NullCap = cdl_cap.NullCap)) s proof (prove)
goal:
No subgoals!