theory KHeap_DR

lemma transform_cnode_contents_upd:
  "\<lbrakk>well_formed_cnode_n sz cn; cn sl' = Some ocap'\<rbrakk> \<Longrightarrow>
    (transform_cnode_contents sz cn)(nat (bl_to_bin sl') \<mapsto> transform_cap cap') =
    transform_cnode_contents sz (cn(sl' \<mapsto> cap'))" apply (rule ext) apply clarsimp apply (rule conjI) prefer 2 apply (clarsimp simp: transform_cnode_contents_def option_map_def
                         option_map_join_def nat_to_bl_to_bin
                   split: option.splits) apply (clarsimp simp: transform_cnode_contents_def option_map_def
                         option_map_join_def
                   split: option.splits) apply (frule (1) wf_cs_nD [symmetric]) apply (simp add: nat_to_bl_id2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>well_formed_cnode_n sz cn; cn sl' = Some ocap'\<rbrakk> \<Longrightarrow> (transform_cnode_contents sz cn)(nat (bl_to_bin sl') \<mapsto> transform_cap cap') = transform_cnode_contents sz (cn(sl' \<mapsto> cap')) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>well_formed_cnode_n sz cn; cn sl' = Some ocap'\<rbrakk> \<Longrightarrow> ((transform_cnode_contents sz cn)(nat (bl_to_bin sl') \<mapsto> transform_cap cap')) x = transform_cnode_contents sz (cn(sl' \<mapsto> cap')) x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>well_formed_cnode_n sz cn; cn sl' = Some ocap'\<rbrakk> \<Longrightarrow> (x = nat (bl_to_bin sl') \<longrightarrow> Some (transform_cap cap') = transform_cnode_contents sz (cn(sl' \<mapsto> cap')) (nat (bl_to_bin sl'))) \<and> (x \<noteq> nat (bl_to_bin sl') \<longrightarrow> transform_cnode_contents sz cn x = transform_cnode_contents sz (cn(sl' \<mapsto> cap')) x) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>well_formed_cnode_n sz cn; cn sl' = Some ocap'\<rbrakk> \<Longrightarrow> x = nat (bl_to_bin sl') \<longrightarrow> Some (transform_cap cap') = transform_cnode_contents sz (cn(sl' \<mapsto> cap')) (nat (bl_to_bin sl'))
 2. \<And>x. \<lbrakk>well_formed_cnode_n sz cn; cn sl' = Some ocap'\<rbrakk> \<Longrightarrow> x \<noteq> nat (bl_to_bin sl') \<longrightarrow> transform_cnode_contents sz cn x = transform_cnode_contents sz (cn(sl' \<mapsto> cap')) x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>well_formed_cnode_n sz cn; cn sl' = Some ocap'\<rbrakk> \<Longrightarrow> x \<noteq> nat (bl_to_bin sl') \<longrightarrow> transform_cnode_contents sz cn x = transform_cnode_contents sz (cn(sl' \<mapsto> cap')) x
 2. \<And>x. \<lbrakk>well_formed_cnode_n sz cn; cn sl' = Some ocap'\<rbrakk> \<Longrightarrow> x = nat (bl_to_bin sl') \<longrightarrow> Some (transform_cap cap') = transform_cnode_contents sz (cn(sl' \<mapsto> cap')) (nat (bl_to_bin sl')) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>well_formed_cnode_n sz cn; cn sl' = Some ocap'\<rbrakk> \<Longrightarrow> x = nat (bl_to_bin sl') \<longrightarrow> Some (transform_cap cap') = transform_cnode_contents sz (cn(sl' \<mapsto> cap')) (nat (bl_to_bin sl')) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>well_formed_cnode_n sz cn; cn sl' = Some ocap'\<rbrakk> \<Longrightarrow> (nat_to_bl sz (nat (bl_to_bin sl')) = None \<longrightarrow> x \<noteq> nat (bl_to_bin sl')) \<and> (\<forall>x2. x2 \<noteq> sl' \<longrightarrow> nat_to_bl sz (nat (bl_to_bin sl')) = Some x2 \<longrightarrow> (cn x2 = None \<longrightarrow> x \<noteq> nat (bl_to_bin sl')) \<and> (\<forall>x2a. cn x2 = Some x2a \<longrightarrow> x = nat (bl_to_bin sl') \<longrightarrow> transform_cap cap' = transform_cap x2a)) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>well_formed_cnode_n sz cn; cn sl' = Some ocap'; sz = length sl'\<rbrakk> \<Longrightarrow> (nat_to_bl sz (nat (bl_to_bin sl')) = None \<longrightarrow> x \<noteq> nat (bl_to_bin sl')) \<and> (\<forall>x2. x2 \<noteq> sl' \<longrightarrow> nat_to_bl sz (nat (bl_to_bin sl')) = Some x2 \<longrightarrow> (cn x2 = None \<longrightarrow> x \<noteq> nat (bl_to_bin sl')) \<and> (\<forall>x2a. cn x2 = Some x2a \<longrightarrow> x = nat (bl_to_bin sl') \<longrightarrow> transform_cap cap' = transform_cap x2a)) proof (prove)
goal:
No subgoals!