theory CSpaceInv_AI

lemma set_cap_obj_at_other:
  "\<lbrace>\<lambda>s. P (obj_at P' p s) \<and> p \<noteq> fst p'\<rbrace> set_cap cap p' \<lbrace>\<lambda>rv s. P (obj_at P' p s)\<rbrace>" apply (simp add: set_cap_def split_def) apply (rule hoare_seq_ext [OF _ get_object_inv]) apply (case_tac obj, simp_all split del: if_split) apply (wpsimp wp: set_object_wp simp: obj_at_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (obj_at P' p s) \<and> p \<noteq> fst p'\<rbrace> set_cap cap p' \<lbrace>\<lambda>rv s. P (obj_at P' p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (obj_at P' p s) \<and> p \<noteq> fst p'\<rbrace> do obj <- get_object (fst p');
(case obj of CNode sz cn \<Rightarrow> if snd p' \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(snd p' \<mapsto> cap) else fail | TCB tcb \<Rightarrow> if snd p' = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := cap\<rparr> else if snd p' = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := cap\<rparr> else if snd p' = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := cap\<rparr> else if snd p' = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := cap\<rparr> else if snd p' = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := cap\<rparr> else fail | _ \<Rightarrow> fail) >>= set_object (fst p')
od \<lbrace>\<lambda>rv s. P (obj_at P' p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>obj. \<lbrace>\<lambda>s. P (obj_at P' p s) \<and> p \<noteq> fst p'\<rbrace> (case obj of CNode sz cn \<Rightarrow> if snd p' \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(snd p' \<mapsto> cap) else fail | TCB tcb \<Rightarrow> if snd p' = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := cap\<rparr> else if snd p' = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := cap\<rparr> else if snd p' = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := cap\<rparr> else if snd p' = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := cap\<rparr> else if snd p' = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := cap\<rparr> else fail | _ \<Rightarrow> fail) >>= set_object (fst p') \<lbrace>\<lambda>rv s. P (obj_at P' p s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>obj x11 x12. obj = CNode x11 x12 \<Longrightarrow> \<lbrace>\<lambda>s. P (obj_at P' p s) \<and> p \<noteq> fst p'\<rbrace> (if snd p' \<in> dom x12 \<and> well_formed_cnode_n x11 x12 then return $ CNode x11 $ x12(snd p' \<mapsto> cap) else fail) >>= set_object (fst p') \<lbrace>\<lambda>rv s. P (obj_at P' p s)\<rbrace>
 2. \<And>obj x2. obj = TCB x2 \<Longrightarrow> \<lbrace>\<lambda>s. P (obj_at P' p s) \<and> p \<noteq> fst p'\<rbrace> (if snd p' = tcb_cnode_index 0 then return $ TCB $ x2\<lparr>tcb_ctable := cap\<rparr> else if snd p' = tcb_cnode_index 1 then return $ TCB $ x2\<lparr>tcb_vtable := cap\<rparr> else if snd p' = tcb_cnode_index 2 then return $ TCB $ x2\<lparr>tcb_reply := cap\<rparr> else if snd p' = tcb_cnode_index 3 then return $ TCB $ x2\<lparr>tcb_caller := cap\<rparr> else if snd p' = tcb_cnode_index 4 then return $ TCB $ x2\<lparr>tcb_ipcframe := cap\<rparr> else fail) >>= set_object (fst p') \<lbrace>\<lambda>rv s. P (obj_at P' p s)\<rbrace> proof (prove)
goal:
No subgoals!