theory Finalise_AI

lemma set_cap_revokable_update:
  "((),s') \<in> fst (set_cap c p s) \<Longrightarrow>
  ((),is_original_cap_update f s') \<in> fst (set_cap c p (is_original_cap_update f s))" apply (cases p) apply (clarsimp simp add: set_cap_def in_monad get_object_def) apply (case_tac y) apply (auto simp add: in_monad set_object_def get_object_def split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((), s') \<in> fst (set_cap c p s) \<Longrightarrow> ((), is_original_cap_update f s') \<in> fst (set_cap c p (is_original_cap_update f s)) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>((), s') \<in> fst (set_cap c p s); p = (a, b)\<rbrakk> \<Longrightarrow> ((), is_original_cap_update f s') \<in> fst (set_cap c p (is_original_cap_update f s)) proof (prove)
goal (1 subgoal):
 1. \<And>a b y s'' x. \<lbrakk>p = (a, b); kheap s a = Some y; (x, s'') \<in> fst ((case y of CNode sz cn \<Rightarrow> if b \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(b \<mapsto> c) else fail | TCB tcb \<Rightarrow> if b = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := c\<rparr> else if b = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := c\<rparr> else if b = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := c\<rparr> else if b = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := c\<rparr> else if b = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := c\<rparr> else fail | _ \<Rightarrow> fail) s); ((), s') \<in> fst (set_object a x s'')\<rbrakk> \<Longrightarrow> \<exists>s'' x. (x, s'') \<in> fst ((case y of CNode sz cn \<Rightarrow> if b \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(b \<mapsto> c) else fail | TCB tcb \<Rightarrow> if b = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := c\<rparr> else if b = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := c\<rparr> else if b = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := c\<rparr> else if b = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := c\<rparr> else if b = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := c\<rparr> else fail | _ \<Rightarrow> fail) (is_original_cap_update f s)) \<and> ((), is_original_cap_update f s') \<in> fst (set_object a x s'') proof (prove)
goal (5 subgoals):
 1. \<And>a b y s'' x x11 x12. \<lbrakk>p = (a, b); kheap s a = Some y; (x, s'') \<in> fst ((case y of CNode sz cn \<Rightarrow> if b \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(b \<mapsto> c) else fail | TCB tcb \<Rightarrow> if b = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := c\<rparr> else if b = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := c\<rparr> else if b = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := c\<rparr> else if b = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := c\<rparr> else if b = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := c\<rparr> else fail | _ \<Rightarrow> fail) s); ((), s') \<in> fst (set_object a x s''); y = CNode x11 x12\<rbrakk> \<Longrightarrow> \<exists>s'' x. (x, s'') \<in> fst ((case y of CNode sz cn \<Rightarrow> if b \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(b \<mapsto> c) else fail | TCB tcb \<Rightarrow> if b = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := c\<rparr> else if b = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := c\<rparr> else if b = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := c\<rparr> else if b = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := c\<rparr> else if b = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := c\<rparr> else fail | _ \<Rightarrow> fail) (is_original_cap_update f s)) \<and> ((), is_original_cap_update f s') \<in> fst (set_object a x s'')
 2. \<And>a b y s'' x x2. \<lbrakk>p = (a, b); kheap s a = Some y; (x, s'') \<in> fst ((case y of CNode sz cn \<Rightarrow> if b \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(b \<mapsto> c) else fail | TCB tcb \<Rightarrow> if b = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := c\<rparr> else if b = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := c\<rparr> else if b = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := c\<rparr> else if b = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := c\<rparr> else if b = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := c\<rparr> else fail | _ \<Rightarrow> fail) s); ((), s') \<in> fst (set_object a x s''); y = TCB x2\<rbrakk> \<Longrightarrow> \<exists>s'' x. (x, s'') \<in> fst ((case y of CNode sz cn \<Rightarrow> if b \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(b \<mapsto> c) else fail | TCB tcb \<Rightarrow> if b = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := c\<rparr> else if b = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := c\<rparr> else if b = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := c\<rparr> else if b = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := c\<rparr> else if b = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := c\<rparr> else fail | _ \<Rightarrow> fail) (is_original_cap_update f s)) \<and> ((), is_original_cap_update f s') \<in> fst (set_object a x s'')
 3. \<And>a b y s'' x x3. \<lbrakk>p = (a, b); kheap s a = Some y; (x, s'') \<in> fst ((case y of CNode sz cn \<Rightarrow> if b \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(b \<mapsto> c) else fail | TCB tcb \<Rightarrow> if b = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := c\<rparr> else if b = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := c\<rparr> else if b = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := c\<rparr> else if b = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := c\<rparr> else if b = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := c\<rparr> else fail | _ \<Rightarrow> fail) s); ((), s') \<in> fst (set_object a x s''); y = Endpoint x3\<rbrakk> \<Longrightarrow> \<exists>s'' x. (x, s'') \<in> fst ((case y of CNode sz cn \<Rightarrow> if b \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(b \<mapsto> c) else fail | TCB tcb \<Rightarrow> if b = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := c\<rparr> else if b = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := c\<rparr> else if b = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := c\<rparr> else if b = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := c\<rparr> else if b = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := c\<rparr> else fail | _ \<Rightarrow> fail) (is_original_cap_update f s)) \<and> ((), is_original_cap_update f s') \<in> fst (set_object a x s'')
 4. \<And>a b y s'' x x4. \<lbrakk>p = (a, b); kheap s a = Some y; (x, s'') \<in> fst ((case y of CNode sz cn \<Rightarrow> if b \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(b \<mapsto> c) else fail | TCB tcb \<Rightarrow> if b = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := c\<rparr> else if b = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := c\<rparr> else if b = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := c\<rparr> else if b = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := c\<rparr> else if b = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := c\<rparr> else fail | _ \<Rightarrow> fail) s); ((), s') \<in> fst (set_object a x s''); y = Notification x4\<rbrakk> \<Longrightarrow> \<exists>s'' x. (x, s'') \<in> fst ((case y of CNode sz cn \<Rightarrow> if b \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(b \<mapsto> c) else fail | TCB tcb \<Rightarrow> if b = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := c\<rparr> else if b = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := c\<rparr> else if b = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := c\<rparr> else if b = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := c\<rparr> else if b = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := c\<rparr> else fail | _ \<Rightarrow> fail) (is_original_cap_update f s)) \<and> ((), is_original_cap_update f s') \<in> fst (set_object a x s'')
 5. \<And>a b y s'' x x5. \<lbrakk>p = (a, b); kheap s a = Some y; (x, s'') \<in> fst ((case y of CNode sz cn \<Rightarrow> if b \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(b \<mapsto> c) else fail | TCB tcb \<Rightarrow> if b = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := c\<rparr> else if b = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := c\<rparr> else if b = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := c\<rparr> else if b = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := c\<rparr> else if b = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := c\<rparr> else fail | _ \<Rightarrow> fail) s); ((), s') \<in> fst (set_object a x s''); y = ArchObj x5\<rbrakk> \<Longrightarrow> \<exists>s'' x. (x, s'') \<in> fst ((case y of CNode sz cn \<Rightarrow> if b \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(b \<mapsto> c) else fail | TCB tcb \<Rightarrow> if b = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := c\<rparr> else if b = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := c\<rparr> else if b = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := c\<rparr> else if b = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := c\<rparr> else if b = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := c\<rparr> else fail | _ \<Rightarrow> fail) (is_original_cap_update f s)) \<and> ((), is_original_cap_update f s') \<in> fst (set_object a x s'') proof (prove)
goal:
No subgoals!