theory DomainSepInv

lemma set_bound_notification_neg_cte_wp_at[wp]:
  "set_bound_notification a b \<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace>" apply (simp add: set_bound_notification_def) apply (wp set_object_wp get_object_wp dxo_wp_weak| simp)+ apply (case_tac "a = fst slot") apply (clarsimp split: kernel_object.splits) apply (erule notE) apply (erule cte_wp_atE) apply (fastforce simp: obj_at_def) apply (drule get_tcb_SomeD) apply (rule cte_wp_at_tcbI) apply simp apply assumption apply (fastforce simp: tcb_cap_cases_def split: if_splits) apply (fastforce elim: cte_wp_atE intro: cte_wp_at_cteI cte_wp_at_tcbI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace> set_bound_notification a b \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace> do tcb <- gets_the (get_tcb a);
set_object a (TCB (tcb\<lparr>tcb_bound_notification := b\<rparr>))
od \<lbrace>\<lambda>_ s. \<not> cte_wp_at P slot s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<not> cte_wp_at P slot s \<Longrightarrow> (\<exists>y. get_tcb a s = Some y) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (the (get_tcb a s)\<lparr>tcb_bound_notification := b\<rparr>))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<not> cte_wp_at P slot s; a = fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb a s = Some y) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (the (get_tcb a s)\<lparr>tcb_bound_notification := b\<rparr>))\<rparr>)
 2. \<And>s. \<lbrakk>\<not> cte_wp_at P slot s; a \<noteq> fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb a s = Some y) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (the (get_tcb a s)\<lparr>tcb_bound_notification := b\<rparr>))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s y. \<lbrakk>\<not> cte_wp_at P slot s; a = fst slot; get_tcb (fst slot) s = Some y; cte_wp_at P slot (s\<lparr>kheap := (kheap s)(fst slot \<mapsto> TCB (y\<lparr>tcb_bound_notification := b\<rparr>))\<rparr>)\<rbrakk> \<Longrightarrow> False
 2. \<And>s. \<lbrakk>\<not> cte_wp_at P slot s; a \<noteq> fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb a s = Some y) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (the (get_tcb a s)\<lparr>tcb_bound_notification := b\<rparr>))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s y. \<lbrakk>a = fst slot; get_tcb (fst slot) s = Some y; cte_wp_at P slot (s\<lparr>kheap := (kheap s)(fst slot \<mapsto> TCB (y\<lparr>tcb_bound_notification := b\<rparr>))\<rparr>)\<rbrakk> \<Longrightarrow> cte_wp_at P slot s
 2. \<And>s. \<lbrakk>\<not> cte_wp_at P slot s; a \<noteq> fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb a s = Some y) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (the (get_tcb a s)\<lparr>tcb_bound_notification := b\<rparr>))\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>s y sz fun cte. \<lbrakk>a = fst slot; get_tcb (fst slot) s = Some y; kheap (s\<lparr>kheap := (kheap s)(fst slot \<mapsto> TCB (y\<lparr>tcb_bound_notification := b\<rparr>))\<rparr>) (fst slot) = Some (CNode sz fun); well_formed_cnode_n sz fun; fun (snd slot) = Some cte; P cte\<rbrakk> \<Longrightarrow> cte_wp_at P slot s
 2. \<And>s y tcb getF setF restr. \<lbrakk>a = fst slot; get_tcb (fst slot) s = Some y; kheap (s\<lparr>kheap := (kheap s)(fst slot \<mapsto> TCB (y\<lparr>tcb_bound_notification := b\<rparr>))\<rparr>) (fst slot) = Some (TCB tcb); tcb_cap_cases (snd slot) = Some (getF, setF, restr); P (getF tcb)\<rbrakk> \<Longrightarrow> cte_wp_at P slot s
 3. \<And>s. \<lbrakk>\<not> cte_wp_at P slot s; a \<noteq> fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb a s = Some y) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (the (get_tcb a s)\<lparr>tcb_bound_notification := b\<rparr>))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s y tcb getF setF restr. \<lbrakk>a = fst slot; get_tcb (fst slot) s = Some y; kheap (s\<lparr>kheap := (kheap s)(fst slot \<mapsto> TCB (y\<lparr>tcb_bound_notification := b\<rparr>))\<rparr>) (fst slot) = Some (TCB tcb); tcb_cap_cases (snd slot) = Some (getF, setF, restr); P (getF tcb)\<rbrakk> \<Longrightarrow> cte_wp_at P slot s
 2. \<And>s. \<lbrakk>\<not> cte_wp_at P slot s; a \<noteq> fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb a s = Some y) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (the (get_tcb a s)\<lparr>tcb_bound_notification := b\<rparr>))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s y tcb getF setF restr. \<lbrakk>a = fst slot; kheap (s\<lparr>kheap := (kheap s)(fst slot \<mapsto> TCB (y\<lparr>tcb_bound_notification := b\<rparr>))\<rparr>) (fst slot) = Some (TCB tcb); tcb_cap_cases (snd slot) = Some (getF, setF, restr); P (getF tcb); kheap s (fst slot) = Some (TCB y)\<rbrakk> \<Longrightarrow> cte_wp_at P slot s
 2. \<And>s. \<lbrakk>\<not> cte_wp_at P slot s; a \<noteq> fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb a s = Some y) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (the (get_tcb a s)\<lparr>tcb_bound_notification := b\<rparr>))\<rparr>) proof (prove)
goal (4 subgoals):
 1. \<And>s y tcb getF setF restr. \<lbrakk>a = fst slot; kheap (s\<lparr>kheap := (kheap s)(fst slot \<mapsto> TCB (y\<lparr>tcb_bound_notification := b\<rparr>))\<rparr>) (fst slot) = Some (TCB tcb); tcb_cap_cases (snd slot) = Some (getF, setF, restr); P (getF tcb); kheap s (fst slot) = Some (TCB y)\<rbrakk> \<Longrightarrow> kheap s (fst slot) = Some (TCB (?tcb19 s y tcb getF setF restr))
 2. \<And>s y tcb getF setF restr. \<lbrakk>a = fst slot; kheap (s\<lparr>kheap := (kheap s)(fst slot \<mapsto> TCB (y\<lparr>tcb_bound_notification := b\<rparr>))\<rparr>) (fst slot) = Some (TCB tcb); tcb_cap_cases (snd slot) = Some (getF, setF, restr); P (getF tcb); kheap s (fst slot) = Some (TCB y)\<rbrakk> \<Longrightarrow> tcb_cap_cases (snd slot) = Some (?getF19 s y tcb getF setF restr, ?setF19 s y tcb getF setF restr)
 3. \<And>s y tcb getF setF restr. \<lbrakk>a = fst slot; kheap (s\<lparr>kheap := (kheap s)(fst slot \<mapsto> TCB (y\<lparr>tcb_bound_notification := b\<rparr>))\<rparr>) (fst slot) = Some (TCB tcb); tcb_cap_cases (snd slot) = Some (getF, setF, restr); P (getF tcb); kheap s (fst slot) = Some (TCB y)\<rbrakk> \<Longrightarrow> P (?getF19 s y tcb getF setF restr (?tcb19 s y tcb getF setF restr))
 4. \<And>s. \<lbrakk>\<not> cte_wp_at P slot s; a \<noteq> fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb a s = Some y) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (the (get_tcb a s)\<lparr>tcb_bound_notification := b\<rparr>))\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>s y tcb getF setF restr. \<lbrakk>a = fst slot; kheap (s\<lparr>kheap := (kheap s)(fst slot \<mapsto> TCB (y\<lparr>tcb_bound_notification := b\<rparr>))\<rparr>) (fst slot) = Some (TCB tcb); tcb_cap_cases (snd slot) = Some (getF, setF, restr); P (getF tcb); kheap s (fst slot) = Some (TCB y)\<rbrakk> \<Longrightarrow> tcb_cap_cases (snd slot) = Some (?getF19 s y tcb getF setF restr, ?setF19 s y tcb getF setF restr)
 2. \<And>s y tcb getF setF restr. \<lbrakk>a = fst slot; kheap (s\<lparr>kheap := (kheap s)(fst slot \<mapsto> TCB (y\<lparr>tcb_bound_notification := b\<rparr>))\<rparr>) (fst slot) = Some (TCB tcb); tcb_cap_cases (snd slot) = Some (getF, setF, restr); P (getF tcb); kheap s (fst slot) = Some (TCB y)\<rbrakk> \<Longrightarrow> P (?getF19 s y tcb getF setF restr y)
 3. \<And>s. \<lbrakk>\<not> cte_wp_at P slot s; a \<noteq> fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb a s = Some y) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (the (get_tcb a s)\<lparr>tcb_bound_notification := b\<rparr>))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s y tcb getF setF restr. \<lbrakk>a = fst slot; kheap (s\<lparr>kheap := (kheap s)(fst slot \<mapsto> TCB (y\<lparr>tcb_bound_notification := b\<rparr>))\<rparr>) (fst slot) = Some (TCB tcb); tcb_cap_cases (snd slot) = Some (getF, setF, restr); P (getF tcb); kheap s (fst slot) = Some (TCB y)\<rbrakk> \<Longrightarrow> P (getF y)
 2. \<And>s. \<lbrakk>\<not> cte_wp_at P slot s; a \<noteq> fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb a s = Some y) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (the (get_tcb a s)\<lparr>tcb_bound_notification := b\<rparr>))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<not> cte_wp_at P slot s; a \<noteq> fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb a s = Some y) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (the (get_tcb a s)\<lparr>tcb_bound_notification := b\<rparr>))\<rparr>) proof (prove)
goal:
No subgoals!