theory CNode_AC

lemma set_cdt_set_cap_comm:
  "(do set_cdt c; set_cap cap slot od) =
   (do set_cap cap slot; set_cdt c od)" apply (rule ext) apply (clarsimp simp: bind_def split_def set_cap_def set_cdt_def
                        get_object_def set_object_def get_def put_def
                        simpler_gets_def simpler_modify_def
                        assert_def fail_def) apply (case_tac y; simp add: return_def fail_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do set_cdt c;
set_cap cap slot
od = do set_cap cap slot;
set_cdt c
od proof (prove)
goal (1 subgoal):
 1. \<And>x. (do set_cdt c;
set_cap cap slot
od) x = (do set_cap cap slot;
set_cdt c
od) x proof (prove)
goal (1 subgoal):
 1. \<And>x y. kheap x (fst slot) = Some y \<Longrightarrow> (\<Union>x\<in>fst (return () (x\<lparr>cdt := c\<rparr>)). \<Union>x\<in>fst (return y (snd x)). \<Union>x\<in>fst ((case fst x of CNode sz cn \<Rightarrow> if snd slot \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(snd slot \<mapsto> cap) else fail | TCB tcb \<Rightarrow> if snd slot = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := cap\<rparr> else if snd slot = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := cap\<rparr> else if snd slot = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := cap\<rparr> else if snd slot = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := cap\<rparr> else if snd slot = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := cap\<rparr> else fail | _ \<Rightarrow> fail) (snd x)). \<Union>xa\<in>fst ((if \<exists>y. kheap (snd x) (fst slot) = Some y then return () else (\<lambda>s. ({}, True))) (snd x)). \<Union>xa\<in>fst (return (the (kheap (snd x) (fst slot))) (snd xa)). \<Union>xa\<in>fst ((if a_type (fst xa) = a_type (fst x) then return () else (\<lambda>s. ({}, True))) (snd xa)). {((), snd xa\<lparr>kheap := (kheap (snd xa))(fst slot \<mapsto> fst x)\<rparr>)}) = (\<Union>x\<in>fst (return () x). \<Union>x\<in>fst (return y (snd x)). \<Union>x\<in>fst ((case fst x of CNode sz cn \<Rightarrow> if snd slot \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(snd slot \<mapsto> cap) else fail | TCB tcb \<Rightarrow> if snd slot = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := cap\<rparr> else if snd slot = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := cap\<rparr> else if snd slot = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := cap\<rparr> else if snd slot = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := cap\<rparr> else if snd slot = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := cap\<rparr> else fail | _ \<Rightarrow> fail) (snd x)). \<Union>xa\<in>fst ((if \<exists>y. kheap (snd x) (fst slot) = Some y then return () else (\<lambda>s. ({}, True))) (snd x)). \<Union>xa\<in>fst (return (the (kheap (snd x) (fst slot))) (snd xa)). \<Union>xa\<in>fst ((if a_type (fst xa) = a_type (fst x) then return () else (\<lambda>s. ({}, True))) (snd xa)). {((), snd xa\<lparr>kheap := (kheap (snd xa))(fst slot \<mapsto> fst x), cdt := c\<rparr>)}) \<and> ((\<exists>ya\<in>fst (return () (x\<lparr>cdt := c\<rparr>)). \<exists>x\<in>fst (return y (snd ya)). (\<exists>x\<in>fst ((case fst x of CNode sz cn \<Rightarrow> if snd slot \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(snd slot \<mapsto> cap) else fail | TCB tcb \<Rightarrow> if snd slot = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := cap\<rparr> else if snd slot = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := cap\<rparr> else if snd slot = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := cap\<rparr> else if snd slot = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := cap\<rparr> else if snd slot = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := cap\<rparr> else fail | _ \<Rightarrow> fail) (snd x)). (\<exists>y. kheap (snd x) (fst slot) = Some y) \<longrightarrow> (\<exists>y\<in>fst (return () (snd x)). \<exists>xa\<in>fst (return (the (kheap (snd x) (fst slot))) (snd y)). a_type (fst xa) = a_type (fst x) \<longrightarrow> snd (return () (snd xa))) \<or> (\<exists>xa\<in>fst (return () (snd x)). snd (return (the (kheap (snd x) (fst slot))) (snd xa))) \<or> snd (return () (snd x))) \<or> snd ((case fst x of CNode sz cn \<Rightarrow> if snd slot \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(snd slot \<mapsto> cap) else fail | TCB tcb \<Rightarrow> if snd slot = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := cap\<rparr> else if snd slot = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := cap\<rparr> else if snd slot = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := cap\<rparr> else if snd slot = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := cap\<rparr> else if snd slot = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := cap\<rparr> else fail | _ \<Rightarrow> fail) (snd x))) \<or> (\<exists>x\<in>fst (return () (x\<lparr>cdt := c\<rparr>)). snd (return y (snd x))) \<or> snd (return () (x\<lparr>cdt := c\<rparr>))) = ((\<exists>ya\<in>fst (return () x). \<exists>x\<in>fst (return y (snd ya)). (\<exists>x\<in>fst ((case fst x of CNode sz cn \<Rightarrow> if snd slot \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(snd slot \<mapsto> cap) else fail | TCB tcb \<Rightarrow> if snd slot = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := cap\<rparr> else if snd slot = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := cap\<rparr> else if snd slot = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := cap\<rparr> else if snd slot = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := cap\<rparr> else if snd slot = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := cap\<rparr> else fail | _ \<Rightarrow> fail) (snd x)). (\<exists>y. kheap (snd x) (fst slot) = Some y) \<longrightarrow> (\<exists>y\<in>fst (return () (snd x)). \<exists>xa\<in>fst (return (the (kheap (snd x) (fst slot))) (snd y)). a_type (fst xa) = a_type (fst x) \<longrightarrow> snd (return () (snd xa))) \<or> (\<exists>xa\<in>fst (return () (snd x)). snd (return (the (kheap (snd x) (fst slot))) (snd xa))) \<or> snd (return () (snd x))) \<or> snd ((case fst x of CNode sz cn \<Rightarrow> if snd slot \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(snd slot \<mapsto> cap) else fail | TCB tcb \<Rightarrow> if snd slot = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := cap\<rparr> else if snd slot = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := cap\<rparr> else if snd slot = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := cap\<rparr> else if snd slot = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := cap\<rparr> else if snd slot = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := cap\<rparr> else fail | _ \<Rightarrow> fail) (snd x))) \<or> (\<exists>x\<in>fst (return () x). snd (return y (snd x))) \<or> snd (return () x)) proof (prove)
goal:
No subgoals!