theory Frame_SD

lemma set_object_wp:
  "\<lbrace>< (obj_id \<mapsto>o -) \<and>* R>\<rbrace>
   set_object obj_id obj
   \<lbrace>\<lambda>rv. <obj_id \<mapsto>o obj \<and>* R>\<rbrace>" apply (clarsimp simp: set_object_def sep_state_projection_def) apply wp apply (clarsimp simp: sep_conj_def) apply (simp add:sep_map_o_def sep_map_general_def) apply (rule_tac x = "SepState (object_to_sep_state obj_id obj UNIV) Map.empty" in exI) apply (rule_tac x=y in exI) apply (clarsimp simp: plus_sep_state_def sep_disj_sep_state_def
    sep_state_disj_def sep_any_def map_disj_def
    sep_map_o_def sep_map_general_def) apply (frule disjoint_subset[OF
    dom_map_restrict,rotated,where a1 = "{obj_id} \<times> UNIV"]) apply (clarsimp simp:dom_object_to_sep_state object_to_sep_state_restrict) apply (clarsimp simp:sep_state_add_def) apply (rule ext, rename_tac sep_id) apply (case_tac sep_id, rename_tac ptr component, clarsimp) apply (clarsimp simp:object_to_sep_state_add) apply (clarsimp simp:object_to_sep_state_def) apply (drule_tac x = "(ptr,component)" in fun_cong)+ apply (simp add:map_add_def) apply (clarsimp split:option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift (obj_id \<mapsto>o - \<and>* R)\<rbrace> set_object obj_id obj \<lbrace>\<lambda>rv. cdl.lift (obj_id \<mapsto>o obj \<and>* R)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (obj_id \<mapsto>o - \<and>* R) (SepState (\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id)) (\<lambda>irq. Some (cdl_irq_node s irq)))\<rbrace> modify (\<lambda>s. s\<lparr>cdl_objects := (cdl_objects s)(obj_id \<mapsto> obj)\<rparr>) \<lbrace>\<lambda>rv s. (obj_id \<mapsto>o obj \<and>* R) (SepState (\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id)) (\<lambda>irq. Some (cdl_irq_node s irq)))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (obj_id \<mapsto>o - \<and>* R) (SepState (\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id)) (\<lambda>irq. Some (cdl_irq_node s irq))) \<Longrightarrow> (obj_id \<mapsto>o obj \<and>* R) (SepState (\<lambda>(obj_ida, comp_id). map_option (object_project comp_id) (cdl_objects (s\<lparr>cdl_objects := (cdl_objects s)(obj_id \<mapsto> obj)\<rparr>) obj_ida)) (\<lambda>irq. Some (cdl_irq_node (s\<lparr>cdl_objects := (cdl_objects s)(obj_id \<mapsto> obj)\<rparr>) irq))) proof (prove)
goal (1 subgoal):
 1. \<And>s x y. \<lbrakk>x ## y; SepState (\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id)) (\<lambda>irq. Some (cdl_irq_node s irq)) = x + y; (obj_id \<mapsto>o -) x; R y\<rbrakk> \<Longrightarrow> \<exists>x y. x ## y \<and> SepState (\<lambda>(obj_ida, comp_id). map_option (object_project comp_id) (if obj_ida = obj_id then Some obj else cdl_objects s obj_ida)) (\<lambda>irq. Some (cdl_irq_node s irq)) = x + y \<and> (obj_id \<mapsto>o obj) x \<and> R y proof (prove)
goal (1 subgoal):
 1. \<And>s x y. \<lbrakk>x ## y; SepState (\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id)) (\<lambda>irq. Some (cdl_irq_node s irq)) = x + y; (obj_id \<mapsto>o -) x; R y\<rbrakk> \<Longrightarrow> \<exists>x y. x ## y \<and> SepState (\<lambda>(obj_ida, comp_id). map_option (object_project comp_id) (if obj_ida = obj_id then Some obj else cdl_objects s obj_ida)) (\<lambda>irq. Some (cdl_irq_node s irq)) = x + y \<and> sep_heap x = object_to_sep_state obj_id obj UNIV \<and> sep_irq_node x = (\<lambda>x. None) \<and> R y proof (prove)
goal (1 subgoal):
 1. \<And>s x y. \<lbrakk>x ## y; SepState (\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id)) (\<lambda>irq. Some (cdl_irq_node s irq)) = x + y; (obj_id \<mapsto>o -) x; R y\<rbrakk> \<Longrightarrow> \<exists>y. SepState (object_to_sep_state obj_id obj UNIV) (\<lambda>x. None) ## y \<and> SepState (\<lambda>(obj_ida, comp_id). map_option (object_project comp_id) (if obj_ida = obj_id then Some obj else cdl_objects s obj_ida)) (\<lambda>irq. Some (cdl_irq_node s irq)) = SepState (object_to_sep_state obj_id obj UNIV) (\<lambda>x. None) + y \<and> sep_heap (SepState (object_to_sep_state obj_id obj UNIV) (\<lambda>x. None)) = object_to_sep_state obj_id obj UNIV \<and> sep_irq_node (SepState (object_to_sep_state obj_id obj UNIV) (\<lambda>x. None)) = (\<lambda>x. None) \<and> R y proof (prove)
goal (1 subgoal):
 1. \<And>s x y. \<lbrakk>x ## y; SepState (\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id)) (\<lambda>irq. Some (cdl_irq_node s irq)) = x + y; (obj_id \<mapsto>o -) x; R y\<rbrakk> \<Longrightarrow> SepState (object_to_sep_state obj_id obj UNIV) (\<lambda>x. None) ## y \<and> SepState (\<lambda>(obj_ida, comp_id). map_option (object_project comp_id) (if obj_ida = obj_id then Some obj else cdl_objects s obj_ida)) (\<lambda>irq. Some (cdl_irq_node s irq)) = SepState (object_to_sep_state obj_id obj UNIV) (\<lambda>x. None) + y \<and> sep_heap (SepState (object_to_sep_state obj_id obj UNIV) (\<lambda>x. None)) = object_to_sep_state obj_id obj UNIV \<and> sep_irq_node (SepState (object_to_sep_state obj_id obj UNIV) (\<lambda>x. None)) = (\<lambda>x. None) \<and> R y proof (prove)
goal (1 subgoal):
 1. \<And>s x y v. \<lbrakk>dom (object_to_sep_state obj_id v UNIV) \<inter> dom (sep_heap y) = {}; SepState (\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id)) (\<lambda>irq. Some (cdl_irq_node s irq)) = sep_state_add x y; R y; sep_irq_node x = (\<lambda>x. None); sep_heap x = object_to_sep_state obj_id v UNIV\<rbrakk> \<Longrightarrow> dom (object_to_sep_state obj_id obj UNIV) \<inter> dom (sep_heap y) = {} \<and> SepState (\<lambda>(obj_ida, comp_id). map_option (object_project comp_id) (if obj_ida = obj_id then Some obj else cdl_objects s obj_ida)) (\<lambda>irq. Some (cdl_irq_node s irq)) = sep_state_add (SepState (object_to_sep_state obj_id obj UNIV) (\<lambda>x. None)) y proof (prove)
goal (1 subgoal):
 1. \<And>s x y v. \<lbrakk>dom (object_to_sep_state obj_id v UNIV) \<inter> dom (sep_heap y) = {}; SepState (\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id)) (\<lambda>irq. Some (cdl_irq_node s irq)) = sep_state_add x y; R y; sep_irq_node x = (\<lambda>x. None); sep_heap x = object_to_sep_state obj_id v UNIV; dom (object_to_sep_state obj_id v UNIV |` ({obj_id} \<times> UNIV)) \<inter> dom (sep_heap y) = {}\<rbrakk> \<Longrightarrow> dom (object_to_sep_state obj_id obj UNIV) \<inter> dom (sep_heap y) = {} \<and> SepState (\<lambda>(obj_ida, comp_id). map_option (object_project comp_id) (if obj_ida = obj_id then Some obj else cdl_objects s obj_ida)) (\<lambda>irq. Some (cdl_irq_node s irq)) = sep_state_add (SepState (object_to_sep_state obj_id obj UNIV) (\<lambda>x. None)) y proof (prove)
goal (1 subgoal):
 1. \<And>s x y v. \<lbrakk>{obj_id} \<times> UNIV \<inter> dom (sep_heap y) = {}; SepState (\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id)) (\<lambda>irq. Some (cdl_irq_node s irq)) = sep_state_add x y; R y; sep_irq_node x = (\<lambda>x. None); sep_heap x = object_to_sep_state obj_id v UNIV\<rbrakk> \<Longrightarrow> SepState (\<lambda>(obj_ida, comp_id). map_option (object_project comp_id) (if obj_ida = obj_id then Some obj else cdl_objects s obj_ida)) (\<lambda>irq. Some (cdl_irq_node s irq)) = sep_state_add (SepState (object_to_sep_state obj_id obj UNIV) (\<lambda>x. None)) y proof (prove)
goal (1 subgoal):
 1. \<And>s x y v. \<lbrakk>{obj_id} \<times> UNIV \<inter> dom (sep_heap y) = {}; R y; sep_irq_node x = (\<lambda>x. None); sep_heap x = object_to_sep_state obj_id v UNIV; (\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id)) = object_to_sep_state obj_id v UNIV ++ sep_heap y; (\<lambda>irq. Some (cdl_irq_node s irq)) = sep_irq_node y\<rbrakk> \<Longrightarrow> (\<lambda>(obj_ida, comp_id). map_option (object_project comp_id) (if obj_ida = obj_id then Some obj else cdl_objects s obj_ida)) = object_to_sep_state obj_id obj UNIV ++ sep_heap y proof (prove)
goal (1 subgoal):
 1. \<And>s x y v sep_id. \<lbrakk>{obj_id} \<times> UNIV \<inter> dom (sep_heap y) = {}; R y; sep_irq_node x = (\<lambda>x. None); sep_heap x = object_to_sep_state obj_id v UNIV; (\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id)) = object_to_sep_state obj_id v UNIV ++ sep_heap y; (\<lambda>irq. Some (cdl_irq_node s irq)) = sep_irq_node y\<rbrakk> \<Longrightarrow> (case sep_id of (obj_ida, comp_id) \<Rightarrow> map_option (object_project comp_id) (if obj_ida = obj_id then Some obj else cdl_objects s obj_ida)) = (object_to_sep_state obj_id obj UNIV ++ sep_heap y) sep_id proof (prove)
goal (1 subgoal):
 1. \<And>s x y v ptr component. \<lbrakk>{obj_id} \<times> UNIV \<inter> dom (sep_heap y) = {}; R y; sep_irq_node x = (\<lambda>x. None); sep_heap x = object_to_sep_state obj_id v UNIV; (\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id)) = object_to_sep_state obj_id v UNIV ++ sep_heap y; (\<lambda>irq. Some (cdl_irq_node s irq)) = sep_irq_node y\<rbrakk> \<Longrightarrow> (ptr = obj_id \<longrightarrow> Some (object_project component obj) = (object_to_sep_state obj_id obj UNIV ++ sep_heap y) (obj_id, component)) \<and> (ptr \<noteq> obj_id \<longrightarrow> map_option (object_project component) (cdl_objects s ptr) = (object_to_sep_state obj_id obj UNIV ++ sep_heap y) (ptr, component)) proof (prove)
goal (1 subgoal):
 1. \<And>s x y v ptr component. \<lbrakk>{obj_id} \<times> UNIV \<inter> dom (sep_heap y) = {}; R y; sep_irq_node x = (\<lambda>x. None); sep_heap x = object_to_sep_state obj_id v UNIV; (\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id)) = object_to_sep_state obj_id v UNIV ++ sep_heap y; (\<lambda>irq. Some (cdl_irq_node s irq)) = sep_irq_node y; ptr \<noteq> obj_id\<rbrakk> \<Longrightarrow> map_option (object_project component) (cdl_objects s ptr) = (object_to_sep_state obj_id obj UNIV ++ sep_heap y) (ptr, component) proof (prove)
goal (1 subgoal):
 1. \<And>s x y v ptr component. \<lbrakk>{obj_id} \<times> UNIV \<inter> dom (sep_heap y) = {}; R y; sep_irq_node x = (\<lambda>x. None); sep_heap x = (\<lambda>(obj_id', comp_id). if obj_id' = obj_id then Some (object_project comp_id v) else None); (\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id)) = (\<lambda>(obj_id', comp_id). if obj_id' = obj_id then Some (object_project comp_id v) else None) ++ sep_heap y; (\<lambda>irq. Some (cdl_irq_node s irq)) = sep_irq_node y; ptr \<noteq> obj_id\<rbrakk> \<Longrightarrow> map_option (object_project component) (cdl_objects s ptr) = ((\<lambda>(obj_id', comp_id). if obj_id' = obj_id then Some (object_project comp_id obj) else None) ++ sep_heap y) (ptr, component) proof (prove)
goal (1 subgoal):
 1. \<And>s x y v ptr component. \<lbrakk>{obj_id} \<times> UNIV \<inter> dom (sep_heap y) = {}; R y; sep_irq_node x = (\<lambda>x. None); (\<lambda>irq. Some (cdl_irq_node s irq)) = sep_irq_node y; ptr \<noteq> obj_id; sep_heap x (ptr, component) = (case (ptr, component) of (obj_id', comp_id) \<Rightarrow> if obj_id' = obj_id then Some (object_project comp_id v) else None); (case (ptr, component) of (obj_id, comp_id) \<Rightarrow> map_option (object_project comp_id) (cdl_objects s obj_id)) = ((\<lambda>(obj_id', comp_id). if obj_id' = obj_id then Some (object_project comp_id v) else None) ++ sep_heap y) (ptr, component)\<rbrakk> \<Longrightarrow> map_option (object_project component) (cdl_objects s ptr) = ((\<lambda>(obj_id', comp_id). if obj_id' = obj_id then Some (object_project comp_id obj) else None) ++ sep_heap y) (ptr, component) proof (prove)
goal (1 subgoal):
 1. \<And>s x y v ptr component. \<lbrakk>{obj_id} \<times> UNIV \<inter> dom (sep_heap y) = {}; R y; sep_irq_node x = (\<lambda>x. None); (\<lambda>irq. Some (cdl_irq_node s irq)) = sep_irq_node y; ptr \<noteq> obj_id; sep_heap x (ptr, component) = None; map_option (object_project component) (cdl_objects s ptr) = (case sep_heap y (ptr, component) of None \<Rightarrow> case (ptr, component) of (obj_id', comp_id) \<Rightarrow> if obj_id' = obj_id then Some (object_project comp_id v) else None | Some x \<Rightarrow> Some x)\<rbrakk> \<Longrightarrow> (case sep_heap y (ptr, component) of None \<Rightarrow> case (ptr, component) of (obj_id', comp_id) \<Rightarrow> if obj_id' = obj_id then Some (object_project comp_id v) else None | Some x \<Rightarrow> Some x) = (case sep_heap y (ptr, component) of None \<Rightarrow> case (ptr, component) of (obj_id', comp_id) \<Rightarrow> if obj_id' = obj_id then Some (object_project comp_id obj) else None | Some x \<Rightarrow> Some x) proof (prove)
goal:
No subgoals!