theory Frame_SD

lemma detype_one_wp:
  "\<lbrace><obj_id \<mapsto>o obj \<and>* R>\<rbrace>
    modify (detype {obj_id})
   \<lbrace>\<lambda>_. <obj_id \<mapsto>o Untyped \<and>* R>\<rbrace>" apply (clarsimp simp: modify_def detype_def) apply wp apply (clarsimp simp: sep_state_projection_def sep_map_o_conj) apply (rule conjI) apply (rule ext) apply (clarsimp simp:object_project_def
      restrict_map_def 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 obj \<and>* R)\<rbrace> modify (detype {obj_id}) \<lbrace>\<lambda>_. cdl.lift (obj_id \<mapsto>o Untyped \<and>* R)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cdl.lift (obj_id \<mapsto>o obj \<and>* R)\<rbrace> do s <- get;
put (s\<lparr>cdl_objects := \<lambda>x. if x = obj_id then Some Untyped else cdl_objects s x\<rparr>)
od \<lbrace>\<lambda>_. cdl.lift (obj_id \<mapsto>o Untyped \<and>* R)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cdl.lift (obj_id \<mapsto>o obj \<and>* R) s \<Longrightarrow> cdl.lift (obj_id \<mapsto>o Untyped \<and>* R) (s\<lparr>cdl_objects := \<lambda>x. if x = obj_id then Some Untyped else cdl_objects s x\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>(\<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 obj UNIV; 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)))\<rbrakk> \<Longrightarrow> (\<lambda>(obj_ida, comp_id). map_option (object_project comp_id) (if obj_ida = obj_id then Some Untyped else cdl_objects s obj_ida)) |` ({obj_id} \<times> UNIV) = object_to_sep_state obj_id Untyped UNIV \<and> R (SepState ((\<lambda>(obj_ida, comp_id). map_option (object_project comp_id) (if obj_ida = obj_id then Some Untyped 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. \<lbrakk>(\<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 obj UNIV; 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)))\<rbrakk> \<Longrightarrow> (\<lambda>(obj_ida, comp_id). map_option (object_project comp_id) (if obj_ida = obj_id then Some Untyped else cdl_objects s obj_ida)) |` ({obj_id} \<times> UNIV) = object_to_sep_state obj_id Untyped UNIV
 2. \<And>s. \<lbrakk>(\<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 obj UNIV; 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)))\<rbrakk> \<Longrightarrow> R (SepState ((\<lambda>(obj_ida, comp_id). map_option (object_project comp_id) (if obj_ida = obj_id then Some Untyped 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. \<lbrakk>(\<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 obj UNIV; 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)))\<rbrakk> \<Longrightarrow> ((\<lambda>(obj_ida, comp_id). map_option (object_project comp_id) (if obj_ida = obj_id then Some Untyped else cdl_objects s obj_ida)) |` ({obj_id} \<times> UNIV)) x = object_to_sep_state obj_id Untyped UNIV x
 2. \<And>s. \<lbrakk>(\<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 obj UNIV; 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)))\<rbrakk> \<Longrightarrow> R (SepState ((\<lambda>(obj_ida, comp_id). map_option (object_project comp_id) (if obj_ida = obj_id then Some Untyped 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. \<lbrakk>(\<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 obj UNIV; 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)))\<rbrakk> \<Longrightarrow> R (SepState ((\<lambda>(obj_ida, comp_id). map_option (object_project comp_id) (if obj_ida = obj_id then Some Untyped 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. (\<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 obj 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 Untyped 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. (\<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 obj 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 Untyped else cdl_objects s obj_ida)) |` (UNIV - {obj_id} \<times> UNIV) 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 obj UNIV \<Longrightarrow> ((\<lambda>(obj_id, comp_id). map_option (object_project comp_id) (cdl_objects s obj_id)) |` (UNIV - {obj_id} \<times> UNIV)) x = ((\<lambda>(obj_ida, comp_id). map_option (object_project comp_id) (if obj_ida = obj_id then Some Untyped else cdl_objects s obj_ida)) |` (UNIV - {obj_id} \<times> UNIV)) x proof (prove)
goal:
No subgoals!