theory CNode_AC

lemma set_cap_empty_slot_ext_comm:
  "(do set_cap cap slot; empty_slot_ext slot' slot_p od) =
   (do empty_slot_ext slot' slot_p; set_cap cap slot od)" apply (rule ext) apply (clarsimp simp: bind_def split_def set_cap_def empty_slot_ext_def
                        update_cdt_list_def set_cdt_list_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 split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do set_cap cap slot;
empty_slot_ext slot' slot_p
od = do empty_slot_ext slot' slot_p;
set_cap cap slot
od proof (prove)
goal (1 subgoal):
 1. \<And>x. (do set_cap cap slot;
empty_slot_ext slot' slot_p
od) x = (do empty_slot_ext slot' slot_p;
set_cap cap slot
od) x proof (prove)
goal (1 subgoal):
 1. \<And>x y. kheap x (fst slot) = Some y \<Longrightarrow> (\<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>cdt_list := case slot_p of None \<Rightarrow> (cdt_list (snd xa))(slot' := []) | Some p \<Rightarrow> if p = slot' then (cdt_list (snd xa))(slot' := list_remove (cdt_list (snd xa) slot') slot') else (cdt_list (snd xa))(p := list_replace_list (cdt_list (snd xa) p) slot' (cdt_list (snd xa) slot'), slot' := []), kheap := (kheap (snd xa))(fst slot \<mapsto> fst x)\<rparr>)}) = (\<Union>x\<in>fst (return () (cdt_list_update (\<lambda>_. case slot_p of None \<Rightarrow> (cdt_list x)(slot' := []) | Some p \<Rightarrow> if p = slot' then (cdt_list x)(slot' := list_remove (cdt_list x slot') slot') else (cdt_list x)(p := list_replace_list (cdt_list x p) slot' (cdt_list x slot'), slot' := [])) 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)\<rparr>)}) \<and> ((\<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)) = ((\<exists>ya\<in>fst (return () (cdt_list_update (\<lambda>_. case slot_p of None \<Rightarrow> (cdt_list x)(slot' := []) | Some p \<Rightarrow> if p = slot' then (cdt_list x)(slot' := list_remove (cdt_list x slot') slot') else (cdt_list x)(p := list_replace_list (cdt_list x p) slot' (cdt_list x slot'), slot' := [])) 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 () (cdt_list_update (\<lambda>_. case slot_p of None \<Rightarrow> (cdt_list x)(slot' := []) | Some p \<Rightarrow> if p = slot' then (cdt_list x)(slot' := list_remove (cdt_list x slot') slot') else (cdt_list x)(p := list_replace_list (cdt_list x p) slot' (cdt_list x slot'), slot' := [])) x)). snd (return y (snd x))) \<or> snd (return () (cdt_list_update (\<lambda>_. case slot_p of None \<Rightarrow> (cdt_list x)(slot' := []) | Some p \<Rightarrow> if p = slot' then (cdt_list x)(slot' := list_remove (cdt_list x slot') slot') else (cdt_list x)(p := list_replace_list (cdt_list x p) slot' (cdt_list x slot'), slot' := [])) x))) proof (prove)
goal:
No subgoals!