theory Frame_SD

lemma create_one_wp:
  "\<lbrace><obj_id \<mapsto>o - \<and>* R>\<rbrace>
    Untyped_D.create_objects [{obj_id}] (Some obj)
   \<lbrace>\<lambda>_. <obj_id \<mapsto>o obj \<and>* R>\<rbrace>" apply (clarsimp simp: modify_def sep_any_exist create_objects_def) apply wp apply (clarsimp simp: sep_state_projection_def sep_map_o_conj) apply (intro conjI ext) apply (drule_tac x = xa in fun_cong) apply (clarsimp simp: object_to_sep_state_def) apply (erule arg_cong[where f = R,THEN iffD1,rotated]) apply clarsimp apply (rule ext) apply (clarsimp simp:restrict_map_def split:if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift (obj_id \<mapsto>o - \<and>* R)\<rbrace> create_objects [{obj_id}] (Some obj) \<lbrace>\<lambda>_. cdl.lift (obj_id \<mapsto>o obj \<and>* R)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<exists>x. cdl.lift (obj_id \<mapsto>o x \<and>* R) s\<rbrace> do s <- get;
put (s\<lparr>cdl_objects := \<lambda>x. if x = obj_id then Some obj else cdl_objects s x\<rparr>)
od \<lbrace>\<lambda>_. cdl.lift (obj_id \<mapsto>o obj \<and>* R)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<exists>x. cdl.lift (obj_id \<mapsto>o x \<and>* R) s \<Longrightarrow> cdl.lift (obj_id \<mapsto>o obj \<and>* R) (s\<lparr>cdl_objects := \<lambda>x. if x = obj_id then Some obj else cdl_objects s x\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>R (SepState ((\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id)) |` (UNIV - {obj_id} \<times> UNIV)) (\<lambda>irq. Some (cdl_irq_node s irq))); (\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id)) |` ({obj_id} \<times> UNIV) = object_to_sep_state obj_id x UNIV\<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)) |` ({obj_id} \<times> UNIV) = object_to_sep_state obj_id obj UNIV \<and> R (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)) |` (UNIV - {obj_id} \<times> UNIV)) (\<lambda>irq. Some (cdl_irq_node s irq))) proof (prove)
goal (2 subgoals):
 1. \<And>s x xa. \<lbrakk>R (SepState ((\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id)) |` (UNIV - {obj_id} \<times> UNIV)) (\<lambda>irq. Some (cdl_irq_node s irq))); (\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id)) |` ({obj_id} \<times> UNIV) = object_to_sep_state obj_id x UNIV\<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)) |` ({obj_id} \<times> UNIV)) xa = object_to_sep_state obj_id obj UNIV xa
 2. \<And>s x. \<lbrakk>R (SepState ((\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id)) |` (UNIV - {obj_id} \<times> UNIV)) (\<lambda>irq. Some (cdl_irq_node s irq))); (\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id)) |` ({obj_id} \<times> UNIV) = object_to_sep_state obj_id x UNIV\<rbrakk> \<Longrightarrow> R (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)) |` (UNIV - {obj_id} \<times> UNIV)) (\<lambda>irq. Some (cdl_irq_node s irq))) proof (prove)
goal (2 subgoals):
 1. \<And>s x xa. \<lbrakk>R (SepState ((\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id)) |` (UNIV - {obj_id} \<times> UNIV)) (\<lambda>irq. Some (cdl_irq_node s irq))); ((\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id)) |` ({obj_id} \<times> UNIV)) xa = object_to_sep_state obj_id x UNIV xa\<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)) |` ({obj_id} \<times> UNIV)) xa = object_to_sep_state obj_id obj UNIV xa
 2. \<And>s x. \<lbrakk>R (SepState ((\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id)) |` (UNIV - {obj_id} \<times> UNIV)) (\<lambda>irq. Some (cdl_irq_node s irq))); (\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id)) |` ({obj_id} \<times> UNIV) = object_to_sep_state obj_id x UNIV\<rbrakk> \<Longrightarrow> R (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)) |` (UNIV - {obj_id} \<times> UNIV)) (\<lambda>irq. Some (cdl_irq_node s irq))) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>R (SepState ((\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id)) |` (UNIV - {obj_id} \<times> UNIV)) (\<lambda>irq. Some (cdl_irq_node s irq))); (\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id)) |` ({obj_id} \<times> UNIV) = object_to_sep_state obj_id x UNIV\<rbrakk> \<Longrightarrow> R (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)) |` (UNIV - {obj_id} \<times> UNIV)) (\<lambda>irq. Some (cdl_irq_node s irq))) proof (prove)
goal (1 subgoal):
 1. \<And>s x. (\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id)) |` ({obj_id} \<times> UNIV) = object_to_sep_state obj_id x UNIV \<Longrightarrow> SepState ((\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id)) |` (UNIV - {obj_id} \<times> UNIV)) (\<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 else cdl_objects s obj_ida)) |` (UNIV - {obj_id} \<times> UNIV)) (\<lambda>irq. Some (cdl_irq_node s irq)) proof (prove)
goal (1 subgoal):
 1. \<And>s x. (\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id)) |` ({obj_id} \<times> UNIV) = object_to_sep_state obj_id x UNIV \<Longrightarrow> (\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id)) |` (UNIV - {obj_id} \<times> UNIV) = (\<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)) |` (UNIV - {obj_id} \<times> UNIV) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa. (\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id)) |` ({obj_id} \<times> UNIV) = object_to_sep_state obj_id x UNIV \<Longrightarrow> ((\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id)) |` (UNIV - {obj_id} \<times> UNIV)) xa = ((\<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)) |` (UNIV - {obj_id} \<times> UNIV)) xa proof (prove)
goal:
No subgoals!