theory Frame_SD

lemma set_object_cdl_field_wp:
  assumes slot: "object_slots obj_n = object_slots obj"
  and type: "object_type obj_n = object_type obj"
            "object_type obj_np = object_type obj"
            "object_type obj_p = object_type obj"
  and fields: "object_wipe_slots (object_clean obj_np) = object_wipe_slots (object_clean obj_n)"
  shows
  "\<lbrace>\<lambda>s. <obj_id \<mapsto>f obj_p \<and>* R> s \<and> object_at ((=) obj) obj_id s\<rbrace>
  set_object obj_id obj_n
  \<lbrace>\<lambda>rv. <obj_id \<mapsto>f obj_np \<and>* R>\<rbrace>" apply (clarsimp simp: set_object_def) apply wp apply (clarsimp simp: sep_state_projection_def sep_map_f_conj) apply (rule conjI) apply (simp add:object_project_def) apply (rule object_eqI) apply (cut_tac fields) apply (simp add:object_wipe_slots_object_clean) apply (rule ext) apply (simp add:object_wipe_slots_def type) apply (erule arg_cong[where f = R, THEN iffD1,rotated]) apply (clarsimp simp: object_at_def) apply (rule ext) apply (clarsimp split:if_splits option.splits) apply (cut_tac slot) apply (rule ccontr) apply (clarsimp simp: object_project_def object_slots_object_clean
                 split: cdl_component_id.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cdl.lift (obj_id \<mapsto>f obj_p \<and>* R) s \<and> ko_at obj obj_id s\<rbrace> set_object obj_id obj_n \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f obj_np \<and>* R)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cdl.lift (obj_id \<mapsto>f obj_p \<and>* R) s \<and> ko_at obj obj_id s\<rbrace> modify (\<lambda>s. s\<lparr>cdl_objects := (cdl_objects s)(obj_id \<mapsto> obj_n)\<rparr>) \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>f obj_np \<and>* R)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cdl.lift (obj_id \<mapsto>f obj_p \<and>* R) s \<and> ko_at obj obj_id s \<Longrightarrow> cdl.lift (obj_id \<mapsto>f obj_np \<and>* R) (s\<lparr>cdl_objects := (cdl_objects s)(obj_id \<mapsto> obj_n)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s z. \<lbrakk>R (SepState ((\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id))((obj_id, Fields) := None)) (\<lambda>irq. Some (cdl_irq_node s irq))); ko_at obj obj_id s; cdl_objects s obj_id = Some z; object_project Fields z = CDL_Object (object_wipe_slots (object_clean obj_p))\<rbrakk> \<Longrightarrow> object_project Fields obj_n = CDL_Object (object_wipe_slots (object_clean obj_np)) \<and> R (SepState ((\<lambda>(obj_ida, comp_id). map_option (object_project comp_id) (if obj_ida = obj_id then Some obj_n else cdl_objects s obj_ida))((obj_id, Fields) := None)) (\<lambda>irq. Some (cdl_irq_node s irq))) proof (prove)
goal (2 subgoals):
 1. \<And>s z. \<lbrakk>R (SepState ((\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id))((obj_id, Fields) := None)) (\<lambda>irq. Some (cdl_irq_node s irq))); ko_at obj obj_id s; cdl_objects s obj_id = Some z; object_project Fields z = CDL_Object (object_wipe_slots (object_clean obj_p))\<rbrakk> \<Longrightarrow> object_project Fields obj_n = CDL_Object (object_wipe_slots (object_clean obj_np))
 2. \<And>s z. \<lbrakk>R (SepState ((\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id))((obj_id, Fields) := None)) (\<lambda>irq. Some (cdl_irq_node s irq))); ko_at obj obj_id s; cdl_objects s obj_id = Some z; object_project Fields z = CDL_Object (object_wipe_slots (object_clean obj_p))\<rbrakk> \<Longrightarrow> R (SepState ((\<lambda>(obj_ida, comp_id). map_option (object_project comp_id) (if obj_ida = obj_id then Some obj_n else cdl_objects s obj_ida))((obj_id, Fields) := None)) (\<lambda>irq. Some (cdl_irq_node s irq))) proof (prove)
goal (2 subgoals):
 1. \<And>s z. \<lbrakk>R (SepState ((\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id))((obj_id, Fields) := None)) (\<lambda>irq. Some (cdl_irq_node s irq))); ko_at obj obj_id s; cdl_objects s obj_id = Some z; object_wipe_slots (object_clean z) = object_wipe_slots (object_clean obj_p)\<rbrakk> \<Longrightarrow> object_wipe_slots (object_clean obj_n) = object_wipe_slots (object_clean obj_np)
 2. \<And>s z. \<lbrakk>R (SepState ((\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id))((obj_id, Fields) := None)) (\<lambda>irq. Some (cdl_irq_node s irq))); ko_at obj obj_id s; cdl_objects s obj_id = Some z; object_project Fields z = CDL_Object (object_wipe_slots (object_clean obj_p))\<rbrakk> \<Longrightarrow> R (SepState ((\<lambda>(obj_ida, comp_id). map_option (object_project comp_id) (if obj_ida = obj_id then Some obj_n else cdl_objects s obj_ida))((obj_id, Fields) := None)) (\<lambda>irq. Some (cdl_irq_node s irq))) proof (prove)
goal (3 subgoals):
 1. \<And>s z. \<lbrakk>R (SepState ((\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id))((obj_id, Fields) := None)) (\<lambda>irq. Some (cdl_irq_node s irq))); ko_at obj obj_id s; cdl_objects s obj_id = Some z; object_wipe_slots (object_clean z) = object_wipe_slots (object_clean obj_p)\<rbrakk> \<Longrightarrow> object_wipe_slots (object_wipe_slots (object_clean obj_n)) = object_wipe_slots (object_wipe_slots (object_clean obj_np))
 2. \<And>s z. \<lbrakk>R (SepState ((\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id))((obj_id, Fields) := None)) (\<lambda>irq. Some (cdl_irq_node s irq))); ko_at obj obj_id s; cdl_objects s obj_id = Some z; object_wipe_slots (object_clean z) = object_wipe_slots (object_clean obj_p)\<rbrakk> \<Longrightarrow> object_slots (object_wipe_slots (object_clean obj_n)) = object_slots (object_wipe_slots (object_clean obj_np))
 3. \<And>s z. \<lbrakk>R (SepState ((\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id))((obj_id, Fields) := None)) (\<lambda>irq. Some (cdl_irq_node s irq))); ko_at obj obj_id s; cdl_objects s obj_id = Some z; object_project Fields z = CDL_Object (object_wipe_slots (object_clean obj_p))\<rbrakk> \<Longrightarrow> R (SepState ((\<lambda>(obj_ida, comp_id). map_option (object_project comp_id) (if obj_ida = obj_id then Some obj_n else cdl_objects s obj_ida))((obj_id, Fields) := None)) (\<lambda>irq. Some (cdl_irq_node s irq))) proof (prove)
goal (3 subgoals):
 1. \<And>s z. \<lbrakk>R (SepState ((\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id))((obj_id, Fields) := None)) (\<lambda>irq. Some (cdl_irq_node s irq))); ko_at obj obj_id s; cdl_objects s obj_id = Some z; object_wipe_slots (object_clean z) = object_wipe_slots (object_clean obj_p); object_wipe_slots (object_clean obj_np) = object_wipe_slots (object_clean obj_n)\<rbrakk> \<Longrightarrow> object_wipe_slots (object_wipe_slots (object_clean obj_n)) = object_wipe_slots (object_wipe_slots (object_clean obj_np))
 2. \<And>s z. \<lbrakk>R (SepState ((\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id))((obj_id, Fields) := None)) (\<lambda>irq. Some (cdl_irq_node s irq))); ko_at obj obj_id s; cdl_objects s obj_id = Some z; object_wipe_slots (object_clean z) = object_wipe_slots (object_clean obj_p)\<rbrakk> \<Longrightarrow> object_slots (object_wipe_slots (object_clean obj_n)) = object_slots (object_wipe_slots (object_clean obj_np))
 3. \<And>s z. \<lbrakk>R (SepState ((\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id))((obj_id, Fields) := None)) (\<lambda>irq. Some (cdl_irq_node s irq))); ko_at obj obj_id s; cdl_objects s obj_id = Some z; object_project Fields z = CDL_Object (object_wipe_slots (object_clean obj_p))\<rbrakk> \<Longrightarrow> R (SepState ((\<lambda>(obj_ida, comp_id). map_option (object_project comp_id) (if obj_ida = obj_id then Some obj_n else cdl_objects s obj_ida))((obj_id, Fields) := None)) (\<lambda>irq. Some (cdl_irq_node s irq))) proof (prove)
goal (2 subgoals):
 1. \<And>s z. \<lbrakk>R (SepState ((\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id))((obj_id, Fields) := None)) (\<lambda>irq. Some (cdl_irq_node s irq))); ko_at obj obj_id s; cdl_objects s obj_id = Some z; object_wipe_slots (object_clean z) = object_wipe_slots (object_clean obj_p)\<rbrakk> \<Longrightarrow> object_slots (object_wipe_slots (object_clean obj_n)) = object_slots (object_wipe_slots (object_clean obj_np))
 2. \<And>s z. \<lbrakk>R (SepState ((\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id))((obj_id, Fields) := None)) (\<lambda>irq. Some (cdl_irq_node s irq))); ko_at obj obj_id s; cdl_objects s obj_id = Some z; object_project Fields z = CDL_Object (object_wipe_slots (object_clean obj_p))\<rbrakk> \<Longrightarrow> R (SepState ((\<lambda>(obj_ida, comp_id). map_option (object_project comp_id) (if obj_ida = obj_id then Some obj_n else cdl_objects s obj_ida))((obj_id, Fields) := None)) (\<lambda>irq. Some (cdl_irq_node s irq))) proof (prove)
goal (2 subgoals):
 1. \<And>s z x. \<lbrakk>R (SepState ((\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id))((obj_id, Fields) := None)) (\<lambda>irq. Some (cdl_irq_node s irq))); ko_at obj obj_id s; cdl_objects s obj_id = Some z; object_wipe_slots (object_clean z) = object_wipe_slots (object_clean obj_p)\<rbrakk> \<Longrightarrow> object_slots (object_wipe_slots (object_clean obj_n)) x = object_slots (object_wipe_slots (object_clean obj_np)) x
 2. \<And>s z. \<lbrakk>R (SepState ((\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id))((obj_id, Fields) := None)) (\<lambda>irq. Some (cdl_irq_node s irq))); ko_at obj obj_id s; cdl_objects s obj_id = Some z; object_project Fields z = CDL_Object (object_wipe_slots (object_clean obj_p))\<rbrakk> \<Longrightarrow> R (SepState ((\<lambda>(obj_ida, comp_id). map_option (object_project comp_id) (if obj_ida = obj_id then Some obj_n else cdl_objects s obj_ida))((obj_id, Fields) := None)) (\<lambda>irq. Some (cdl_irq_node s irq))) proof (prove)
goal (1 subgoal):
 1. \<And>s z. \<lbrakk>R (SepState ((\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id))((obj_id, Fields) := None)) (\<lambda>irq. Some (cdl_irq_node s irq))); ko_at obj obj_id s; cdl_objects s obj_id = Some z; object_project Fields z = CDL_Object (object_wipe_slots (object_clean obj_p))\<rbrakk> \<Longrightarrow> R (SepState ((\<lambda>(obj_ida, comp_id). map_option (object_project comp_id) (if obj_ida = obj_id then Some obj_n else cdl_objects s obj_ida))((obj_id, Fields) := None)) (\<lambda>irq. Some (cdl_irq_node s irq))) proof (prove)
goal (1 subgoal):
 1. \<And>s z. \<lbrakk>ko_at obj obj_id s; cdl_objects s obj_id = Some z; object_project Fields z = CDL_Object (object_wipe_slots (object_clean obj_p))\<rbrakk> \<Longrightarrow> SepState ((\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id))((obj_id, Fields) := None)) (\<lambda>irq. Some (cdl_irq_node s irq)) = SepState ((\<lambda>(obj_ida, comp_id). map_option (object_project comp_id) (if obj_ida = obj_id then Some obj_n else cdl_objects s obj_ida))((obj_id, Fields) := None)) (\<lambda>irq. Some (cdl_irq_node s irq)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cdl_objects s obj_id = Some obj; object_project Fields obj = CDL_Object (object_wipe_slots (object_clean obj_p))\<rbrakk> \<Longrightarrow> (\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id))((obj_id, Fields) := None) = (\<lambda>(obj_ida, comp_id). map_option (object_project comp_id) (if obj_ida = obj_id then Some obj_n else cdl_objects s obj_ida))((obj_id, Fields) := None) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>cdl_objects s obj_id = Some obj; object_project Fields obj = CDL_Object (object_wipe_slots (object_clean obj_p))\<rbrakk> \<Longrightarrow> ((\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id))((obj_id, Fields) := None)) x = ((\<lambda>(obj_ida, comp_id). map_option (object_project comp_id) (if obj_ida = obj_id then Some obj_n else cdl_objects s obj_ida))((obj_id, Fields) := None)) x proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>cdl_objects s obj_id = Some obj; object_project Fields obj = CDL_Object (object_wipe_slots (object_clean obj_p)); object_project b obj \<noteq> object_project b obj_n\<rbrakk> \<Longrightarrow> b = Fields proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>cdl_objects s obj_id = Some obj; object_project Fields obj = CDL_Object (object_wipe_slots (object_clean obj_p)); object_project b obj \<noteq> object_project b obj_n; object_slots obj_n = object_slots obj\<rbrakk> \<Longrightarrow> b = Fields proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>cdl_objects s obj_id = Some obj; object_project Fields obj = CDL_Object (object_wipe_slots (object_clean obj_p)); object_project b obj \<noteq> object_project b obj_n; object_slots obj_n = object_slots obj; b \<noteq> Fields\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!