theory StateTranslationProofs_DR

lemma caps_of_state_def2:
  "caps_of_state s = (\<lambda>ptr. case (option_map caps_of_object (kheap s (fst ptr))) of
                                None \<Rightarrow> None
                              | Some f \<Rightarrow> f (snd ptr))" unfolding caps_of_state_def get_cap_def tcb_cnode_map_def apply (rule ext) apply (clarsimp simp add: split_def get_object_def bind_def gets_def get_def return_def assert_def fail_def) apply (case_tac y, simp_all add: bind_def assert_def return_def assert_opt_def fail_def tcb_cap_cases_def
                              split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. caps_of_state s = (\<lambda>ptr. case map_option caps_of_object (kheap s (fst ptr)) of None \<Rightarrow> None | Some f \<Rightarrow> f (snd ptr)) proof (prove)
goal (1 subgoal):
 1. (\<lambda>p. if \<exists>cap. fst ((case p of (oref, cref) \<Rightarrow> do obj <- KHeap_A.get_object oref;
caps <- case obj of kernel_object.CNode sz cnode \<Rightarrow> do assert (well_formed_cnode_n sz cnode);
return cnode
od | TCB tcb \<Rightarrow> return [tcb_cnode_index 0 \<mapsto> tcb_ctable tcb, tcb_cnode_index 1 \<mapsto> tcb_vtable tcb, tcb_cnode_index 2 \<mapsto> tcb_reply tcb, tcb_cnode_index 3 \<mapsto> tcb_caller tcb, tcb_cnode_index 4 \<mapsto> tcb_ipcframe tcb] | _ \<Rightarrow> fail;
assert_opt (caps cref)
od) s) = {(cap, s)} then Some (THE cap. fst ((case p of (oref, cref) \<Rightarrow> do obj <- KHeap_A.get_object oref;
caps <- case obj of kernel_object.CNode sz cnode \<Rightarrow> do assert (well_formed_cnode_n sz cnode);
return cnode
od | TCB tcb \<Rightarrow> return [tcb_cnode_index 0 \<mapsto> tcb_ctable tcb, tcb_cnode_index 1 \<mapsto> tcb_vtable tcb, tcb_cnode_index 2 \<mapsto> tcb_reply tcb, tcb_cnode_index 3 \<mapsto> tcb_caller tcb, tcb_cnode_index 4 \<mapsto> tcb_ipcframe tcb] | _ \<Rightarrow> fail;
assert_opt (caps cref)
od) s) = {(cap, s)}) else None) = (\<lambda>ptr. case map_option caps_of_object (kheap s (fst ptr)) of None \<Rightarrow> None | Some f \<Rightarrow> f (snd ptr)) proof (prove)
goal (1 subgoal):
 1. \<And>p. (if \<exists>cap. fst ((case p of (oref, cref) \<Rightarrow> do obj <- KHeap_A.get_object oref;
caps <- case obj of kernel_object.CNode sz cnode \<Rightarrow> do assert (well_formed_cnode_n sz cnode);
return cnode
od | TCB tcb \<Rightarrow> return [tcb_cnode_index 0 \<mapsto> tcb_ctable tcb, tcb_cnode_index 1 \<mapsto> tcb_vtable tcb, tcb_cnode_index 2 \<mapsto> tcb_reply tcb, tcb_cnode_index 3 \<mapsto> tcb_caller tcb, tcb_cnode_index 4 \<mapsto> tcb_ipcframe tcb] | _ \<Rightarrow> fail;
assert_opt (caps cref)
od) s) = {(cap, s)} then Some (THE cap. fst ((case p of (oref, cref) \<Rightarrow> do obj <- KHeap_A.get_object oref;
caps <- case obj of kernel_object.CNode sz cnode \<Rightarrow> do assert (well_formed_cnode_n sz cnode);
return cnode
od | TCB tcb \<Rightarrow> return [tcb_cnode_index 0 \<mapsto> tcb_ctable tcb, tcb_cnode_index 1 \<mapsto> tcb_vtable tcb, tcb_cnode_index 2 \<mapsto> tcb_reply tcb, tcb_cnode_index 3 \<mapsto> tcb_caller tcb, tcb_cnode_index 4 \<mapsto> tcb_ipcframe tcb] | _ \<Rightarrow> fail;
assert_opt (caps cref)
od) s) = {(cap, s)}) else None) = (case map_option caps_of_object (kheap s (fst p)) of None \<Rightarrow> None | Some f \<Rightarrow> f (snd p)) proof (prove)
goal (1 subgoal):
 1. \<And>a b y. kheap s a = Some y \<Longrightarrow> ((\<exists>cap. (\<Union>x\<in>fst ((case y of kernel_object.CNode sz cnode \<Rightarrow> do assert (well_formed_cnode_n sz cnode);
return cnode
od | TCB tcb \<Rightarrow> return [tcb_cnode_index 0 \<mapsto> tcb_ctable tcb, tcb_cnode_index 1 \<mapsto> tcb_vtable tcb, tcb_cnode_index 2 \<mapsto> tcb_reply tcb, tcb_cnode_index 3 \<mapsto> tcb_caller tcb, tcb_cnode_index 4 \<mapsto> tcb_ipcframe tcb] | _ \<Rightarrow> fail) s). fst (assert_opt (fst x b) (snd x))) = {(cap, s)}) \<longrightarrow> Some (THE cap. (\<Union>x\<in>fst ((case y of kernel_object.CNode sz cnode \<Rightarrow> do assert (well_formed_cnode_n sz cnode);
return cnode
od | TCB tcb \<Rightarrow> return [tcb_cnode_index 0 \<mapsto> tcb_ctable tcb, tcb_cnode_index 1 \<mapsto> tcb_vtable tcb, tcb_cnode_index 2 \<mapsto> tcb_reply tcb, tcb_cnode_index 3 \<mapsto> tcb_caller tcb, tcb_cnode_index 4 \<mapsto> tcb_ipcframe tcb] | _ \<Rightarrow> fail) s). fst (assert_opt (fst x b) (snd x))) = {(cap, s)}) = caps_of_object y b) \<and> ((\<forall>cap. (\<Union>x\<in>fst ((case y of kernel_object.CNode sz cnode \<Rightarrow> do assert (well_formed_cnode_n sz cnode);
return cnode
od | TCB tcb \<Rightarrow> return [tcb_cnode_index 0 \<mapsto> tcb_ctable tcb, tcb_cnode_index 1 \<mapsto> tcb_vtable tcb, tcb_cnode_index 2 \<mapsto> tcb_reply tcb, tcb_cnode_index 3 \<mapsto> tcb_caller tcb, tcb_cnode_index 4 \<mapsto> tcb_ipcframe tcb] | _ \<Rightarrow> fail) s). fst (assert_opt (fst x b) (snd x))) \<noteq> {(cap, s)}) \<longrightarrow> None = caps_of_object y b) proof (prove)
goal:
No subgoals!