theory Separation_SD

lemma sep_map_c_def_alt:
  "(obj_id, slot) \<mapsto>c cap \<equiv>  \<lambda>s.
    sep_heap s = cap_to_sep_state obj_id cap slot \<and>
    sep_irq_node s = Map.empty" apply (clarsimp simp: sep_map_c_def2 sep_map_s_def sep_map_general_def
                        object_to_sep_state_def cap_to_sep_state_def) apply (rule eq_reflection, rule ext, rule iffI) apply (clarsimp, rule ext, clarsimp) apply (drule object_project_cap_project [symmetric], simp) 
  (* Pick any object with the capability in the right slot. *)
   apply (rule exI [where x="update_slots [slot \<mapsto> cap] (CNode (empty_cnode 1))"]) apply (clarsimp simp: object_slots_def update_slots_def) apply (case_tac "has_slots (update_slots [slot \<mapsto> cap] (CNode (empty_cnode 1)))") apply (fastforce simp: cap_project_def object_project_def
                          object_clean_def asid_reset_def) apply (clarsimp simp: update_slots_def has_slots_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (obj_id, slot) \<mapsto>c cap \<equiv> \<lambda>s. sep_heap s = cap_to_sep_state obj_id cap slot \<and> sep_irq_node s = (\<lambda>x. None) proof (prove)
goal (1 subgoal):
 1. \<lambda>s. \<exists>obj. sep_heap s = (\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id = Slot slot then Some (object_project comp_id obj) else None) \<and> sep_irq_node s = (\<lambda>x. None) \<and> object_slots obj slot = Some cap \<equiv> \<lambda>s. sep_heap s = (\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id = Slot slot then Some (cap_project cap) else None) \<and> sep_irq_node s = (\<lambda>x. None) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<exists>obj. sep_heap s = (\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id = Slot slot then Some (object_project comp_id obj) else None) \<and> sep_irq_node s = (\<lambda>x. None) \<and> object_slots obj slot = Some cap \<Longrightarrow> sep_heap s = (\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id = Slot slot then Some (cap_project cap) else None) \<and> sep_irq_node s = (\<lambda>x. None)
 2. \<And>s. sep_heap s = (\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id = Slot slot then Some (cap_project cap) else None) \<and> sep_irq_node s = (\<lambda>x. None) \<Longrightarrow> \<exists>obj. sep_heap s = (\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id = Slot slot then Some (object_project comp_id obj) else None) \<and> sep_irq_node s = (\<lambda>x. None) \<and> object_slots obj slot = Some cap proof (prove)
goal (2 subgoals):
 1. \<And>s obj a b. \<lbrakk>sep_heap s = (\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id = Slot slot then Some (object_project comp_id obj) else None); sep_irq_node s = (\<lambda>x. None); object_slots obj slot = Some cap\<rbrakk> \<Longrightarrow> (a = obj_id \<and> b = Slot slot \<longrightarrow> object_project (Slot slot) obj = cap_project cap) \<and> ((a = obj_id \<longrightarrow> b \<noteq> Slot slot) \<longrightarrow> a = obj_id \<and> b = Slot slot \<longrightarrow> object_project (Slot slot) obj = cap_project cap)
 2. \<And>s. sep_heap s = (\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id = Slot slot then Some (cap_project cap) else None) \<and> sep_irq_node s = (\<lambda>x. None) \<Longrightarrow> \<exists>obj. sep_heap s = (\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id = Slot slot then Some (object_project comp_id obj) else None) \<and> sep_irq_node s = (\<lambda>x. None) \<and> object_slots obj slot = Some cap proof (prove)
goal (1 subgoal):
 1. \<And>s. sep_heap s = (\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id = Slot slot then Some (cap_project cap) else None) \<and> sep_irq_node s = (\<lambda>x. None) \<Longrightarrow> \<exists>obj. sep_heap s = (\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id = Slot slot then Some (object_project comp_id obj) else None) \<and> sep_irq_node s = (\<lambda>x. None) \<and> object_slots obj slot = Some cap proof (prove)
goal (1 subgoal):
 1. \<And>s. sep_heap s = (\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id = Slot slot then Some (cap_project cap) else None) \<and> sep_irq_node s = (\<lambda>x. None) \<Longrightarrow> \<exists>obj. sep_heap s = (\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id = Slot slot then Some (object_project comp_id obj) else None) \<and> sep_irq_node s = (\<lambda>x. None) \<and> object_slots obj slot = Some cap proof (prove)
goal (1 subgoal):
 1. \<And>s. sep_heap s = (\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id = Slot slot then Some (cap_project cap) else None) \<and> sep_irq_node s = (\<lambda>x. None) \<Longrightarrow> sep_heap s = (\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id = Slot slot then Some (object_project comp_id (update_slots [slot \<mapsto> cap] (CNode (empty_cnode 1)))) else None) \<and> sep_irq_node s = (\<lambda>x. None) \<and> object_slots (update_slots [slot \<mapsto> cap] (CNode (empty_cnode 1))) slot = Some cap proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>sep_heap s = (\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id = Slot slot then Some (cap_project cap) else None); sep_irq_node s = (\<lambda>x. None)\<rbrakk> \<Longrightarrow> (\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id = Slot slot then Some (cap_project cap) else None) = (\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id = Slot slot then Some (object_project comp_id (update_slots [slot \<mapsto> cap] (CNode (empty_cnode 1)))) else None) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>sep_heap s = (\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id = Slot slot then Some (cap_project cap) else None); sep_irq_node s = (\<lambda>x. None); has_slots (update_slots [slot \<mapsto> cap] (CNode (empty_cnode 1)))\<rbrakk> \<Longrightarrow> (\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id = Slot slot then Some (cap_project cap) else None) = (\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id = Slot slot then Some (object_project comp_id (update_slots [slot \<mapsto> cap] (CNode (empty_cnode 1)))) else None)
 2. \<And>s. \<lbrakk>sep_heap s = (\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id = Slot slot then Some (cap_project cap) else None); sep_irq_node s = (\<lambda>x. None); \<not> has_slots (update_slots [slot \<mapsto> cap] (CNode (empty_cnode 1)))\<rbrakk> \<Longrightarrow> (\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id = Slot slot then Some (cap_project cap) else None) = (\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id = Slot slot then Some (object_project comp_id (update_slots [slot \<mapsto> cap] (CNode (empty_cnode 1)))) else None) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>sep_heap s = (\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id = Slot slot then Some (cap_project cap) else None); sep_irq_node s = (\<lambda>x. None); \<not> has_slots (update_slots [slot \<mapsto> cap] (CNode (empty_cnode 1)))\<rbrakk> \<Longrightarrow> (\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id = Slot slot then Some (cap_project cap) else None) = (\<lambda>(obj_id', comp_id). if obj_id' = obj_id \<and> comp_id = Slot slot then Some (object_project comp_id (update_slots [slot \<mapsto> cap] (CNode (empty_cnode 1)))) else None) proof (prove)
goal:
No subgoals!