theory Invocation_DP

lemma sep_map_c_asid_reset:
  "reset_cap_asid cap = reset_cap_asid cap'
  \<Longrightarrow> sep_map_c ptr cap = sep_map_c ptr cap'" apply (intro ext) apply (clarsimp simp:sep_map_c_def split_def) apply (rule iffI) apply clarsimp apply (case_tac "\<not> has_slots obj") apply simp apply (rule_tac x = "update_slots ((object_slots obj)(snd ptr \<mapsto> cap')) obj"
     in exI) apply (simp add:sep_map_general_def object_to_sep_state_slot) apply clarsimp apply (case_tac "\<not> has_slots obj") apply simp apply (rule_tac x = "update_slots ((object_slots obj)(snd ptr \<mapsto> cap)) obj"
    in exI) apply (simp add:sep_map_general_def object_to_sep_state_slot) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reset_cap_asid cap = reset_cap_asid cap' \<Longrightarrow> ptr \<mapsto>c cap = ptr \<mapsto>c cap' proof (prove)
goal (1 subgoal):
 1. \<And>x. reset_cap_asid cap = reset_cap_asid cap' \<Longrightarrow> (ptr \<mapsto>c cap) x = (ptr \<mapsto>c cap') x proof (prove)
goal (1 subgoal):
 1. \<And>x. reset_cap_asid cap = reset_cap_asid cap' \<Longrightarrow> (\<exists>obj. sep_map_general (fst ptr) obj {Slot (snd ptr)} x \<and> object_slots obj = [snd ptr \<mapsto> cap]) = (\<exists>obj. sep_map_general (fst ptr) obj {Slot (snd ptr)} x \<and> object_slots obj = [snd ptr \<mapsto> cap']) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>reset_cap_asid cap = reset_cap_asid cap'; \<exists>obj. sep_map_general (fst ptr) obj {Slot (snd ptr)} x \<and> object_slots obj = [snd ptr \<mapsto> cap]\<rbrakk> \<Longrightarrow> \<exists>obj. sep_map_general (fst ptr) obj {Slot (snd ptr)} x \<and> object_slots obj = [snd ptr \<mapsto> cap']
 2. \<And>x. \<lbrakk>reset_cap_asid cap = reset_cap_asid cap'; \<exists>obj. sep_map_general (fst ptr) obj {Slot (snd ptr)} x \<and> object_slots obj = [snd ptr \<mapsto> cap']\<rbrakk> \<Longrightarrow> \<exists>obj. sep_map_general (fst ptr) obj {Slot (snd ptr)} x \<and> object_slots obj = [snd ptr \<mapsto> cap] proof (prove)
goal (2 subgoals):
 1. \<And>x obj. \<lbrakk>reset_cap_asid cap = reset_cap_asid cap'; sep_map_general (fst ptr) obj {Slot (snd ptr)} x; object_slots obj = [snd ptr \<mapsto> cap]\<rbrakk> \<Longrightarrow> \<exists>obj. sep_map_general (fst ptr) obj {Slot (snd ptr)} x \<and> object_slots obj = [snd ptr \<mapsto> cap']
 2. \<And>x. \<lbrakk>reset_cap_asid cap = reset_cap_asid cap'; \<exists>obj. sep_map_general (fst ptr) obj {Slot (snd ptr)} x \<and> object_slots obj = [snd ptr \<mapsto> cap']\<rbrakk> \<Longrightarrow> \<exists>obj. sep_map_general (fst ptr) obj {Slot (snd ptr)} x \<and> object_slots obj = [snd ptr \<mapsto> cap] proof (prove)
goal (3 subgoals):
 1. \<And>x obj. \<lbrakk>reset_cap_asid cap = reset_cap_asid cap'; sep_map_general (fst ptr) obj {Slot (snd ptr)} x; object_slots obj = [snd ptr \<mapsto> cap]; \<not> has_slots obj\<rbrakk> \<Longrightarrow> \<exists>obj. sep_map_general (fst ptr) obj {Slot (snd ptr)} x \<and> object_slots obj = [snd ptr \<mapsto> cap']
 2. \<And>x obj. \<lbrakk>reset_cap_asid cap = reset_cap_asid cap'; sep_map_general (fst ptr) obj {Slot (snd ptr)} x; object_slots obj = [snd ptr \<mapsto> cap]; \<not> \<not> has_slots obj\<rbrakk> \<Longrightarrow> \<exists>obj. sep_map_general (fst ptr) obj {Slot (snd ptr)} x \<and> object_slots obj = [snd ptr \<mapsto> cap']
 3. \<And>x. \<lbrakk>reset_cap_asid cap = reset_cap_asid cap'; \<exists>obj. sep_map_general (fst ptr) obj {Slot (snd ptr)} x \<and> object_slots obj = [snd ptr \<mapsto> cap']\<rbrakk> \<Longrightarrow> \<exists>obj. sep_map_general (fst ptr) obj {Slot (snd ptr)} x \<and> object_slots obj = [snd ptr \<mapsto> cap] proof (prove)
goal (2 subgoals):
 1. \<And>x obj. \<lbrakk>reset_cap_asid cap = reset_cap_asid cap'; sep_map_general (fst ptr) obj {Slot (snd ptr)} x; object_slots obj = [snd ptr \<mapsto> cap]; \<not> \<not> has_slots obj\<rbrakk> \<Longrightarrow> \<exists>obj. sep_map_general (fst ptr) obj {Slot (snd ptr)} x \<and> object_slots obj = [snd ptr \<mapsto> cap']
 2. \<And>x. \<lbrakk>reset_cap_asid cap = reset_cap_asid cap'; \<exists>obj. sep_map_general (fst ptr) obj {Slot (snd ptr)} x \<and> object_slots obj = [snd ptr \<mapsto> cap']\<rbrakk> \<Longrightarrow> \<exists>obj. sep_map_general (fst ptr) obj {Slot (snd ptr)} x \<and> object_slots obj = [snd ptr \<mapsto> cap] proof (prove)
goal (2 subgoals):
 1. \<And>x obj. \<lbrakk>reset_cap_asid cap = reset_cap_asid cap'; sep_map_general (fst ptr) obj {Slot (snd ptr)} x; object_slots obj = [snd ptr \<mapsto> cap]; \<not> \<not> has_slots obj\<rbrakk> \<Longrightarrow> sep_map_general (fst ptr) (update_slots ((object_slots obj)(snd ptr \<mapsto> cap')) obj) {Slot (snd ptr)} x \<and> object_slots (update_slots ((object_slots obj)(snd ptr \<mapsto> cap')) obj) = [snd ptr \<mapsto> cap']
 2. \<And>x. \<lbrakk>reset_cap_asid cap = reset_cap_asid cap'; \<exists>obj. sep_map_general (fst ptr) obj {Slot (snd ptr)} x \<and> object_slots obj = [snd ptr \<mapsto> cap']\<rbrakk> \<Longrightarrow> \<exists>obj. sep_map_general (fst ptr) obj {Slot (snd ptr)} x \<and> object_slots obj = [snd ptr \<mapsto> cap] proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>reset_cap_asid cap = reset_cap_asid cap'; \<exists>obj. sep_map_general (fst ptr) obj {Slot (snd ptr)} x \<and> object_slots obj = [snd ptr \<mapsto> cap']\<rbrakk> \<Longrightarrow> \<exists>obj. sep_map_general (fst ptr) obj {Slot (snd ptr)} x \<and> object_slots obj = [snd ptr \<mapsto> cap] proof (prove)
goal (1 subgoal):
 1. \<And>x obj. \<lbrakk>reset_cap_asid cap = reset_cap_asid cap'; sep_map_general (fst ptr) obj {Slot (snd ptr)} x; object_slots obj = [snd ptr \<mapsto> cap']\<rbrakk> \<Longrightarrow> \<exists>obj. sep_map_general (fst ptr) obj {Slot (snd ptr)} x \<and> object_slots obj = [snd ptr \<mapsto> cap] proof (prove)
goal (2 subgoals):
 1. \<And>x obj. \<lbrakk>reset_cap_asid cap = reset_cap_asid cap'; sep_map_general (fst ptr) obj {Slot (snd ptr)} x; object_slots obj = [snd ptr \<mapsto> cap']; \<not> has_slots obj\<rbrakk> \<Longrightarrow> \<exists>obj. sep_map_general (fst ptr) obj {Slot (snd ptr)} x \<and> object_slots obj = [snd ptr \<mapsto> cap]
 2. \<And>x obj. \<lbrakk>reset_cap_asid cap = reset_cap_asid cap'; sep_map_general (fst ptr) obj {Slot (snd ptr)} x; object_slots obj = [snd ptr \<mapsto> cap']; \<not> \<not> has_slots obj\<rbrakk> \<Longrightarrow> \<exists>obj. sep_map_general (fst ptr) obj {Slot (snd ptr)} x \<and> object_slots obj = [snd ptr \<mapsto> cap] proof (prove)
goal (1 subgoal):
 1. \<And>x obj. \<lbrakk>reset_cap_asid cap = reset_cap_asid cap'; sep_map_general (fst ptr) obj {Slot (snd ptr)} x; object_slots obj = [snd ptr \<mapsto> cap']; \<not> \<not> has_slots obj\<rbrakk> \<Longrightarrow> \<exists>obj. sep_map_general (fst ptr) obj {Slot (snd ptr)} x \<and> object_slots obj = [snd ptr \<mapsto> cap] proof (prove)
goal (1 subgoal):
 1. \<And>x obj. \<lbrakk>reset_cap_asid cap = reset_cap_asid cap'; sep_map_general (fst ptr) obj {Slot (snd ptr)} x; object_slots obj = [snd ptr \<mapsto> cap']; \<not> \<not> has_slots obj\<rbrakk> \<Longrightarrow> sep_map_general (fst ptr) (update_slots ((object_slots obj)(snd ptr \<mapsto> cap)) obj) {Slot (snd ptr)} x \<and> object_slots (update_slots ((object_slots obj)(snd ptr \<mapsto> cap)) obj) = [snd ptr \<mapsto> cap] proof (prove)
goal:
No subgoals!