theory CNode_AC

lemma set_original_set_cap_comm:
  "(do set_original slot' val; set_cap cap slot od) =
   (do set_cap cap slot; set_original slot' val od)" apply (rule ext) apply (clarsimp simp: bind_def split_def set_cap_def set_original_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_original slot' val;
set_cap cap slot
od = do set_cap cap slot;
set_original slot' val
od proof (prove)
goal (1 subgoal):
 1. \<And>x. (do set_original slot' val;
set_cap cap slot
od) x = (do set_cap cap slot;
set_original slot' val
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>is_original_cap := (is_original_cap x)(slot' := val)\<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), is_original_cap := (is_original_cap (snd xa))(slot' := val)\<rparr>)}) \<and> ((\<exists>ya\<in>fst (return () (x\<lparr>is_original_cap := (is_original_cap x)(slot' := val)\<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>is_original_cap := (is_original_cap x)(slot' := val)\<rparr>)). snd (return y (snd x))) \<or> snd (return () (x\<lparr>is_original_cap := (is_original_cap x)(slot' := val)\<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!