theory StateTranslation_D

lemma transform_objects_ms_underlying_mem:
  "transform_objects s =
   transform_objects (s \<lparr> machine_state :=
     undefined \<lparr> underlying_memory := underlying_memory (machine_state s) \<rparr> \<rparr>)" supply option.case_cong[cong] apply (rule ext) apply (simp add: transform_objects_def map_add_def option_map_def
            split: option.split) apply (simp add: transform_object_def transform_tcb_def
                   transform_full_intent_def Let_def
            split: Structures_A.kernel_object.split) apply (clarsimp simp: transform_intent_def cong: get_tcb_mrs_cong get_ipc_buffer_words_cong) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. transform_objects s = transform_objects (s\<lparr>machine_state := undefined\<lparr>underlying_memory := underlying_memory (machine_state s)\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. transform_objects s = transform_objects (s\<lparr>machine_state := undefined\<lparr>underlying_memory := underlying_memory (machine_state s)\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>x. transform_objects s x = transform_objects (s\<lparr>machine_state := undefined\<lparr>underlying_memory := underlying_memory (machine_state s)\<rparr>\<rparr>) x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<forall>x2. (kheap s |` (- {idle_thread s})) x = Some x2 \<longrightarrow> transform_object (machine_state s) x ((ekheap s |` (- {idle_thread s})) x) x2 = transform_object (undefined\<lparr>underlying_memory := underlying_memory (machine_state s)\<rparr>) x ((ekheap s |` (- {idle_thread s})) x) x2 proof (prove)
goal (1 subgoal):
 1. \<And>x. \<forall>x2. (kheap s |` (- {idle_thread s})) x = Some (TCB x2) \<longrightarrow> (case (ekheap s |` (- {idle_thread s})) x of Some x2a \<Rightarrow> Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable x2), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable x2), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply x2), tcb_caller_slot \<mapsto> transform_cap (tcb_caller x2), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe x2), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op x (tcb_state x2), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification x2)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler x2), cdl_tcb_intent = \<lparr>cdl_intent_op = transform_intent (invocation_type (mi_label (get_tcb_message_info x2))) (get_tcb_mrs (machine_state s) x2), cdl_intent_error = guess_error (mi_label (get_tcb_message_info x2)), cdl_intent_cap = arch_tcb_context_get (tcb_arch x2) cap_register, cdl_intent_extras = get_ipc_buffer_words (machine_state s) x2 [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (get_tcb_message_info x2))], cdl_intent_recv_slot = case get_ipc_buffer_words (machine_state s) x2 [Suc (Suc (msg_max_length + msg_max_extra_caps))..<5 + (msg_max_length + msg_max_extra_caps)] of [] \<Rightarrow> None | [croot] \<Rightarrow> None | [croot, index] \<Rightarrow> None | [croot, index, depth] \<Rightarrow> Some (croot, index, unat depth) | croot # index # depth # ac # lista \<Rightarrow> None\<rparr>, cdl_tcb_has_fault = \<exists>y. tcb_fault x2 = Some y, cdl_tcb_domain = tcb_domain x2a\<rparr>) = (case (ekheap s |` (- {idle_thread s})) x of Some etcb \<Rightarrow> Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable x2), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable x2), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply x2), tcb_caller_slot \<mapsto> transform_cap (tcb_caller x2), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe x2), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op x (tcb_state x2), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification x2)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler x2), cdl_tcb_intent = \<lparr>cdl_intent_op = transform_intent (invocation_type (mi_label (get_tcb_message_info x2))) (get_tcb_mrs (undefined\<lparr>underlying_memory := underlying_memory (machine_state s)\<rparr>) x2), cdl_intent_error = guess_error (mi_label (get_tcb_message_info x2)), cdl_intent_cap = arch_tcb_context_get (tcb_arch x2) cap_register, cdl_intent_extras = get_ipc_buffer_words (undefined\<lparr>underlying_memory := underlying_memory (machine_state s)\<rparr>) x2 [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (get_tcb_message_info x2))], cdl_intent_recv_slot = case get_ipc_buffer_words (undefined\<lparr>underlying_memory := underlying_memory (machine_state s)\<rparr>) x2 [Suc (Suc (msg_max_length + msg_max_extra_caps))..<5 + (msg_max_length + msg_max_extra_caps)] of [] \<Rightarrow> None | [croot] \<Rightarrow> None | [croot, index] \<Rightarrow> None | [croot, index, depth] \<Rightarrow> Some (croot, index, unat depth) | croot # index # depth # ac # lista \<Rightarrow> None\<rparr>, cdl_tcb_has_fault = \<exists>y. tcb_fault x2 = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) proof (prove)
goal:
No subgoals!