theory DomainSepInv

lemma thread_set_tcb_ipc_buffer_update_neg_cte_wp_at[wp]:
  "thread_set (tcb_ipc_buffer_update f) t \<lbrace>\<lambda>s. \<not> cte_wp_at P slot s\<rbrace>" unfolding thread_set_def apply (wp set_object_wp | simp)+ apply (case_tac "t = 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> thread_set (tcb_ipc_buffer_update f) t \<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 t;
set_object t $ TCB $ tcb_ipc_buffer_update f tcb
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 t s = Some y) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (tcb_ipc_buffer_update f (the (get_tcb t s))))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<not> cte_wp_at P slot s; t = fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb t s = Some y) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (tcb_ipc_buffer_update f (the (get_tcb t s))))\<rparr>)
 2. \<And>s. \<lbrakk>\<not> cte_wp_at P slot s; t \<noteq> fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb t s = Some y) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (tcb_ipc_buffer_update f (the (get_tcb t s))))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s y. \<lbrakk>\<not> cte_wp_at P slot s; t = fst slot; get_tcb (fst slot) s = Some y; cte_wp_at P slot (s\<lparr>kheap := (kheap s)(fst slot \<mapsto> TCB (tcb_ipc_buffer_update f y))\<rparr>)\<rbrakk> \<Longrightarrow> False
 2. \<And>s. \<lbrakk>\<not> cte_wp_at P slot s; t \<noteq> fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb t s = Some y) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (tcb_ipc_buffer_update f (the (get_tcb t s))))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s y. \<lbrakk>t = fst slot; get_tcb (fst slot) s = Some y; cte_wp_at P slot (s\<lparr>kheap := (kheap s)(fst slot \<mapsto> TCB (tcb_ipc_buffer_update f y))\<rparr>)\<rbrakk> \<Longrightarrow> cte_wp_at P slot s
 2. \<And>s. \<lbrakk>\<not> cte_wp_at P slot s; t \<noteq> fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb t s = Some y) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (tcb_ipc_buffer_update f (the (get_tcb t s))))\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>s y sz fun cte. \<lbrakk>t = fst slot; get_tcb (fst slot) s = Some y; kheap (s\<lparr>kheap := (kheap s)(fst slot \<mapsto> TCB (tcb_ipc_buffer_update f y))\<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>t = fst slot; get_tcb (fst slot) s = Some y; kheap (s\<lparr>kheap := (kheap s)(fst slot \<mapsto> TCB (tcb_ipc_buffer_update f y))\<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; t \<noteq> fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb t s = Some y) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (tcb_ipc_buffer_update f (the (get_tcb t s))))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s y tcb getF setF restr. \<lbrakk>t = fst slot; get_tcb (fst slot) s = Some y; kheap (s\<lparr>kheap := (kheap s)(fst slot \<mapsto> TCB (tcb_ipc_buffer_update f y))\<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; t \<noteq> fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb t s = Some y) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (tcb_ipc_buffer_update f (the (get_tcb t s))))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s y tcb getF setF restr. \<lbrakk>t = fst slot; kheap (s\<lparr>kheap := (kheap s)(fst slot \<mapsto> TCB (tcb_ipc_buffer_update f y))\<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; t \<noteq> fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb t s = Some y) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (tcb_ipc_buffer_update f (the (get_tcb t s))))\<rparr>) proof (prove)
goal (4 subgoals):
 1. \<And>s y tcb getF setF restr. \<lbrakk>t = fst slot; kheap (s\<lparr>kheap := (kheap s)(fst slot \<mapsto> TCB (tcb_ipc_buffer_update f y))\<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 (?tcb21 s y tcb getF setF restr))
 2. \<And>s y tcb getF setF restr. \<lbrakk>t = fst slot; kheap (s\<lparr>kheap := (kheap s)(fst slot \<mapsto> TCB (tcb_ipc_buffer_update f y))\<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 (?getF21 s y tcb getF setF restr, ?setF21 s y tcb getF setF restr)
 3. \<And>s y tcb getF setF restr. \<lbrakk>t = fst slot; kheap (s\<lparr>kheap := (kheap s)(fst slot \<mapsto> TCB (tcb_ipc_buffer_update f y))\<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 (?getF21 s y tcb getF setF restr (?tcb21 s y tcb getF setF restr))
 4. \<And>s. \<lbrakk>\<not> cte_wp_at P slot s; t \<noteq> fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb t s = Some y) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (tcb_ipc_buffer_update f (the (get_tcb t s))))\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>s y tcb getF setF restr. \<lbrakk>t = fst slot; kheap (s\<lparr>kheap := (kheap s)(fst slot \<mapsto> TCB (tcb_ipc_buffer_update f y))\<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 (?getF21 s y tcb getF setF restr, ?setF21 s y tcb getF setF restr)
 2. \<And>s y tcb getF setF restr. \<lbrakk>t = fst slot; kheap (s\<lparr>kheap := (kheap s)(fst slot \<mapsto> TCB (tcb_ipc_buffer_update f y))\<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 (?getF21 s y tcb getF setF restr y)
 3. \<And>s. \<lbrakk>\<not> cte_wp_at P slot s; t \<noteq> fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb t s = Some y) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (tcb_ipc_buffer_update f (the (get_tcb t s))))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s y tcb getF setF restr. \<lbrakk>t = fst slot; kheap (s\<lparr>kheap := (kheap s)(fst slot \<mapsto> TCB (tcb_ipc_buffer_update f y))\<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; t \<noteq> fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb t s = Some y) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (tcb_ipc_buffer_update f (the (get_tcb t s))))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<not> cte_wp_at P slot s; t \<noteq> fst slot\<rbrakk> \<Longrightarrow> (\<exists>y. get_tcb t s = Some y) \<longrightarrow> \<not> cte_wp_at P slot (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (tcb_ipc_buffer_update f (the (get_tcb t s))))\<rparr>) proof (prove)
goal:
No subgoals!