theory StateTranslationProofs_DR

lemma transform_objects_update_kheap_same_caps:
  "\<lbrakk> kh ptr = Some ko; caps_of_object ko' = caps_of_object ko; a_type ko' = a_type ko\<rbrakk> \<Longrightarrow>
  transform_objects (update_kheap (kh(ptr \<mapsto> ko')) s) =
  (if ptr = idle_thread s then
         transform_objects (update_kheap kh s)
  else
         (transform_objects (update_kheap kh s))(ptr \<mapsto> transform_object (machine_state s) ptr (ekheap s ptr) ko'))" unfolding transform_objects_def apply (rule ext) apply (simp add: map_option_case restrict_map_def map_add_def ) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kh ptr = Some ko; caps_of_object ko' = caps_of_object ko; a_type ko' = a_type ko\<rbrakk> \<Longrightarrow> transform_objects (update_kheap (kh(ptr \<mapsto> ko')) s) = (if ptr = idle_thread s then transform_objects (update_kheap kh s) else (transform_objects (update_kheap kh s))(ptr \<mapsto> transform_object (machine_state s) ptr (ekheap s ptr) ko')) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kh ptr = Some ko; caps_of_object ko' = caps_of_object ko; a_type ko' = a_type ko\<rbrakk> \<Longrightarrow> (\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread (update_kheap (kh(ptr \<mapsto> ko')) s)}) ++ (\<lambda>ptra. map_option (transform_object (machine_state (update_kheap (kh(ptr \<mapsto> ko')) s)) ptra ((ekheap (update_kheap (kh(ptr \<mapsto> ko')) s) |` (- {idle_thread (update_kheap (kh(ptr \<mapsto> ko')) s)})) ptra)) ((kheap (update_kheap (kh(ptr \<mapsto> ko')) s) |` (- {idle_thread (update_kheap (kh(ptr \<mapsto> ko')) s)})) ptra)) = (if ptr = idle_thread s then (\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread (update_kheap kh s)}) ++ (\<lambda>ptr. map_option (transform_object (machine_state (update_kheap kh s)) ptr ((ekheap (update_kheap kh s) |` (- {idle_thread (update_kheap kh s)})) ptr)) ((kheap (update_kheap kh s) |` (- {idle_thread (update_kheap kh s)})) ptr)) else ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread (update_kheap kh s)}) ++ (\<lambda>ptr. map_option (transform_object (machine_state (update_kheap kh s)) ptr ((ekheap (update_kheap kh s) |` (- {idle_thread (update_kheap kh s)})) ptr)) ((kheap (update_kheap kh s) |` (- {idle_thread (update_kheap kh s)})) ptr)))(ptr \<mapsto> transform_object (machine_state s) ptr (ekheap s ptr) ko')) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>kh ptr = Some ko; caps_of_object ko' = caps_of_object ko; a_type ko' = a_type ko\<rbrakk> \<Longrightarrow> ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread (update_kheap (kh(ptr \<mapsto> ko')) s)}) ++ (\<lambda>ptra. map_option (transform_object (machine_state (update_kheap (kh(ptr \<mapsto> ko')) s)) ptra ((ekheap (update_kheap (kh(ptr \<mapsto> ko')) s) |` (- {idle_thread (update_kheap (kh(ptr \<mapsto> ko')) s)})) ptra)) ((kheap (update_kheap (kh(ptr \<mapsto> ko')) s) |` (- {idle_thread (update_kheap (kh(ptr \<mapsto> ko')) s)})) ptra))) x = (if ptr = idle_thread s then (\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread (update_kheap kh s)}) ++ (\<lambda>ptr. map_option (transform_object (machine_state (update_kheap kh s)) ptr ((ekheap (update_kheap kh s) |` (- {idle_thread (update_kheap kh s)})) ptr)) ((kheap (update_kheap kh s) |` (- {idle_thread (update_kheap kh s)})) ptr)) else ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread (update_kheap kh s)}) ++ (\<lambda>ptr. map_option (transform_object (machine_state (update_kheap kh s)) ptr ((ekheap (update_kheap kh s) |` (- {idle_thread (update_kheap kh s)})) ptr)) ((kheap (update_kheap kh s) |` (- {idle_thread (update_kheap kh s)})) ptr)))(ptr \<mapsto> transform_object (machine_state s) ptr (ekheap s ptr) ko')) x proof (prove)
goal:
No subgoals!