theory CSpace_AI

lemma set_original_set_cap_comm:
  "(set_original slot val >>= (\<lambda>_. set_cap cap slot)) =
   (set_cap cap slot >>= (\<lambda>_. set_original slot val))" 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 return_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 ((case y 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) (x\<lparr>is_original_cap := (is_original_cap x)(slot := val)\<rparr>)). \<Union>xa\<in>fst ((if \<exists>y. kheap (snd x) (fst slot) = Some y then return () else fail) (snd x)). \<Union>xa\<in>fst ((if a_type (the (kheap (snd x) (fst slot))) = a_type (fst x) then return () else fail) (snd xa)). {((), snd xa\<lparr>kheap := (kheap (snd xa))(fst slot \<mapsto> fst x)\<rparr>)}) = (\<Union>x\<in>fst ((case y 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) x). \<Union>xa\<in>fst ((if \<exists>y. kheap (snd x) (fst slot) = Some y then return () else fail) (snd x)). \<Union>xa\<in>fst ((if a_type (the (kheap (snd x) (fst slot))) = a_type (fst x) then return () else fail) (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>x\<in>fst ((case y 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) (x\<lparr>is_original_cap := (is_original_cap x)(slot := val)\<rparr>)). a_type (the (kheap (snd x) (fst slot))) = a_type (fst x) \<longrightarrow> kheap (snd x) (fst slot) = None) \<or> snd ((case y 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) (x\<lparr>is_original_cap := (is_original_cap x)(slot := val)\<rparr>))) = ((\<exists>x\<in>fst ((case y 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) x). a_type (the (kheap (snd x) (fst slot))) = a_type (fst x) \<longrightarrow> kheap (snd x) (fst slot) = None) \<or> snd ((case y 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) x)) proof (prove)
goal:
No subgoals!