theory Retype_DP

lemma detype_one_wp:
  "<obj_id \<mapsto>o - \<and>* R> s
   \<Longrightarrow> <obj_id \<mapsto>o Untyped \<and>* R> (detype {obj_id} s)" apply (clarsimp simp: detype_def sep_any_exist) apply (clarsimp simp: sep_state_projection_def sep_map_o_conj sep_any_def) 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. cdl.lift (obj_id \<mapsto>o - \<and>* R) s \<Longrightarrow> cdl.lift (obj_id \<mapsto>o Untyped \<and>* R) (detype {obj_id} s) proof (prove)
goal (1 subgoal):
 1. \<And>x. cdl.lift (obj_id \<mapsto>o x \<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>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 x 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>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 x 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>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 x 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>x xa. \<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 x 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)) xa = object_to_sep_state obj_id Untyped UNIV xa
 2. \<And>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 x 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>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 x 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>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 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>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 Untyped else cdl_objects s obj_ida)) |` (UNIV - {obj_id} \<times> UNIV) proof (prove)
goal (1 subgoal):
 1. \<And>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 Untyped else cdl_objects s obj_ida)) |` (UNIV - {obj_id} \<times> UNIV)) xa proof (prove)
goal:
No subgoals!