theory KHeap_DR

lemma transform_objects_update_kheap_simp:
  "\<lbrakk>kheap s ptr = Some ko; ekheap s ptr = opt_etcb\<rbrakk>
    \<Longrightarrow> transform_objects (update_kheap ((kheap s)(ptr \<mapsto> obj)) s) =
    (\<lambda>x. if x \<noteq> ptr then transform_objects s x else
    (if ptr = idle_thread s then None else
           Some (transform_object (machine_state s) ptr opt_etcb obj)))" apply (rule ext) apply (clarsimp split:if_splits) apply (case_tac "x = ptr") apply (clarsimp simp: map_add_def transform_objects_def) apply (simp add:restrict_map_def map_add_def transform_objects_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s ptr = Some ko; ekheap s ptr = opt_etcb\<rbrakk> \<Longrightarrow> transform_objects (update_kheap ((kheap s)(ptr \<mapsto> obj)) s) = (\<lambda>x. if x \<noteq> ptr then transform_objects s x else if ptr = idle_thread s then None else Some (transform_object (machine_state s) ptr opt_etcb obj)) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>kheap s ptr = Some ko; ekheap s ptr = opt_etcb\<rbrakk> \<Longrightarrow> transform_objects (update_kheap ((kheap s)(ptr \<mapsto> obj)) s) x = (if x \<noteq> ptr then transform_objects s x else if ptr = idle_thread s then None else Some (transform_object (machine_state s) ptr opt_etcb obj)) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>kheap s ptr = Some ko; opt_etcb = ekheap s ptr\<rbrakk> \<Longrightarrow> (ptr = idle_thread s \<longrightarrow> (x \<noteq> idle_thread s \<longrightarrow> transform_objects (update_kheap ((kheap s)(idle_thread s \<mapsto> obj)) s) x = transform_objects s x) \<and> (x = idle_thread s \<longrightarrow> transform_objects (update_kheap ((kheap s)(idle_thread s \<mapsto> obj)) s) (idle_thread s) = None)) \<and> (ptr \<noteq> idle_thread s \<longrightarrow> (x \<noteq> ptr \<longrightarrow> transform_objects (update_kheap ((kheap s)(ptr \<mapsto> obj)) s) x = transform_objects s x) \<and> (x = ptr \<longrightarrow> transform_objects (update_kheap ((kheap s)(ptr \<mapsto> obj)) s) ptr = Some (transform_object (machine_state s) ptr (ekheap s ptr) obj))) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>kheap s ptr = Some ko; opt_etcb = ekheap s ptr; x = ptr\<rbrakk> \<Longrightarrow> (ptr = idle_thread s \<longrightarrow> (x \<noteq> idle_thread s \<longrightarrow> transform_objects (update_kheap ((kheap s)(idle_thread s \<mapsto> obj)) s) x = transform_objects s x) \<and> (x = idle_thread s \<longrightarrow> transform_objects (update_kheap ((kheap s)(idle_thread s \<mapsto> obj)) s) (idle_thread s) = None)) \<and> (ptr \<noteq> idle_thread s \<longrightarrow> (x \<noteq> ptr \<longrightarrow> transform_objects (update_kheap ((kheap s)(ptr \<mapsto> obj)) s) x = transform_objects s x) \<and> (x = ptr \<longrightarrow> transform_objects (update_kheap ((kheap s)(ptr \<mapsto> obj)) s) ptr = Some (transform_object (machine_state s) ptr (ekheap s ptr) obj)))
 2. \<And>x. \<lbrakk>kheap s ptr = Some ko; opt_etcb = ekheap s ptr; x \<noteq> ptr\<rbrakk> \<Longrightarrow> (ptr = idle_thread s \<longrightarrow> (x \<noteq> idle_thread s \<longrightarrow> transform_objects (update_kheap ((kheap s)(idle_thread s \<mapsto> obj)) s) x = transform_objects s x) \<and> (x = idle_thread s \<longrightarrow> transform_objects (update_kheap ((kheap s)(idle_thread s \<mapsto> obj)) s) (idle_thread s) = None)) \<and> (ptr \<noteq> idle_thread s \<longrightarrow> (x \<noteq> ptr \<longrightarrow> transform_objects (update_kheap ((kheap s)(ptr \<mapsto> obj)) s) x = transform_objects s x) \<and> (x = ptr \<longrightarrow> transform_objects (update_kheap ((kheap s)(ptr \<mapsto> obj)) s) ptr = Some (transform_object (machine_state s) ptr (ekheap s ptr) obj))) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>kheap s ptr = Some ko; opt_etcb = ekheap s ptr; x \<noteq> ptr\<rbrakk> \<Longrightarrow> (ptr = idle_thread s \<longrightarrow> (x \<noteq> idle_thread s \<longrightarrow> transform_objects (update_kheap ((kheap s)(idle_thread s \<mapsto> obj)) s) x = transform_objects s x) \<and> (x = idle_thread s \<longrightarrow> transform_objects (update_kheap ((kheap s)(idle_thread s \<mapsto> obj)) s) (idle_thread s) = None)) \<and> (ptr \<noteq> idle_thread s \<longrightarrow> (x \<noteq> ptr \<longrightarrow> transform_objects (update_kheap ((kheap s)(ptr \<mapsto> obj)) s) x = transform_objects s x) \<and> (x = ptr \<longrightarrow> transform_objects (update_kheap ((kheap s)(ptr \<mapsto> obj)) s) ptr = Some (transform_object (machine_state s) ptr (ekheap s ptr) obj))) proof (prove)
goal:
No subgoals!