theory KHeap_DR

lemma cdt_single_update_eq:
assumes mdb:"mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)"
shows
"\<lbrakk>cte_at p s; cte_at c s\<rbrakk> \<Longrightarrow> cdl_cdt (cdl_cdt_single_update (transform s) (transform_cslot_ptr c) (transform_cslot_ptr p)) = transform_cdt (abs_cdt_single_update s c p)" apply (simp add: transform_cdt_def abs_cdt_single_update_def) apply (subst map_lift_over_upd[unfolded fun_upd_def]) defer apply (rule ext) apply (clarsimp simp:cdl_cdt_single_update_def transform_def transform_cdt_def) apply (rule transform_cdt_slot_inj_on_cte_at[where P=\<top>]) apply (auto simp: cte_wp_at_caps_of_state ran_def dest!: mdb_cte_atD [OF _ mdb]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_wp_at (\<lambda>_. True) c s\<rbrakk> \<Longrightarrow> cdl_cdt (cdl_cdt_single_update (transform s) (transform_cslot_ptr c) (transform_cslot_ptr p)) = transform_cdt (abs_cdt_single_update s c p) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_wp_at (\<lambda>_. True) c s\<rbrakk> \<Longrightarrow> cdl_cdt (cdl_cdt_single_update (transform s) (transform_cslot_ptr c) (transform_cslot_ptr p)) = map_lift_over transform_cslot_ptr (\<lambda>x. if x = c then Some p else cdt s x) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_wp_at (\<lambda>_. True) c s\<rbrakk> \<Longrightarrow> inj_on transform_cslot_ptr ({c} \<union> set_option (Some p) \<union> dom (cdt s) \<union> ran (cdt s))
 2. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_wp_at (\<lambda>_. True) c s\<rbrakk> \<Longrightarrow> cdl_cdt (cdl_cdt_single_update (transform s) (transform_cslot_ptr c) (transform_cslot_ptr p)) = (\<lambda>x. if x = transform_cslot_ptr c then map_option transform_cslot_ptr (Some p) else map_lift_over transform_cslot_ptr (cdt s) x) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_wp_at (\<lambda>_. True) c s\<rbrakk> \<Longrightarrow> cdl_cdt (cdl_cdt_single_update (transform s) (transform_cslot_ptr c) (transform_cslot_ptr p)) = (\<lambda>x. if x = transform_cslot_ptr c then map_option transform_cslot_ptr (Some p) else map_lift_over transform_cslot_ptr (cdt s) x)
 2. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_wp_at (\<lambda>_. True) c s\<rbrakk> \<Longrightarrow> inj_on transform_cslot_ptr ({c} \<union> set_option (Some p) \<union> dom (cdt s) \<union> ran (cdt s)) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_wp_at (\<lambda>_. True) c s\<rbrakk> \<Longrightarrow> cdl_cdt (cdl_cdt_single_update (transform s) (transform_cslot_ptr c) (transform_cslot_ptr p)) x = (if x = transform_cslot_ptr c then map_option transform_cslot_ptr (Some p) else map_lift_over transform_cslot_ptr (cdt s) x)
 2. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_wp_at (\<lambda>_. True) c s\<rbrakk> \<Longrightarrow> inj_on transform_cslot_ptr ({c} \<union> set_option (Some p) \<union> dom (cdt s) \<union> ran (cdt s)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_wp_at (\<lambda>_. True) c s\<rbrakk> \<Longrightarrow> inj_on transform_cslot_ptr ({c} \<union> set_option (Some p) \<union> dom (cdt s) \<union> ran (cdt s)) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_wp_at (\<lambda>_. True) c s; x \<in> {c} \<union> set_option (Some p) \<union> dom (cdt s) \<union> ran (cdt s)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) x ?s6 proof (prove)
goal:
No subgoals!