theory CSpace1_R

lemma n'_cap:
  "n' p = Some (CTE cap node) \<Longrightarrow>
  if p = src then cap = dcap
  else if p = dest then cap = scap
  else \<exists>node'. m p = Some (CTE cap node')" apply clarsimp apply (rule conjI) apply (fastforce simp add: n'_def modify_map_cases) apply clarsimp apply (rule conjI) apply (fastforce simp add: n'_def modify_map_cases) apply clarsimp apply (simp add: n'_def modify_map_cases) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n' p = Some (CTE cap node) \<Longrightarrow> if p = src then cap = dcap else if p = dest then cap = scap else \<exists>node'. m p = Some (CTE cap node') proof (prove)
goal (1 subgoal):
 1. n' p = Some (CTE cap node) \<Longrightarrow> (p = dest \<longrightarrow> cap = scap) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> cap = dcap) \<and> (p \<noteq> src \<longrightarrow> (\<exists>node'. m p = Some (CTE cap node')))) proof (prove)
goal (2 subgoals):
 1. n' p = Some (CTE cap node) \<Longrightarrow> p = dest \<longrightarrow> cap = scap
 2. n' p = Some (CTE cap node) \<Longrightarrow> p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> cap = dcap) \<and> (p \<noteq> src \<longrightarrow> (\<exists>node'. m p = Some (CTE cap node'))) proof (prove)
goal (1 subgoal):
 1. n' p = Some (CTE cap node) \<Longrightarrow> p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> cap = dcap) \<and> (p \<noteq> src \<longrightarrow> (\<exists>node'. m p = Some (CTE cap node'))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n' p = Some (CTE cap node); p \<noteq> dest\<rbrakk> \<Longrightarrow> (p = src \<longrightarrow> cap = dcap) \<and> (p \<noteq> src \<longrightarrow> (\<exists>node'. m p = Some (CTE cap node'))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n' p = Some (CTE cap node); p \<noteq> dest\<rbrakk> \<Longrightarrow> p = src \<longrightarrow> cap = dcap
 2. \<lbrakk>n' p = Some (CTE cap node); p \<noteq> dest\<rbrakk> \<Longrightarrow> p \<noteq> src \<longrightarrow> (\<exists>node'. m p = Some (CTE cap node')) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n' p = Some (CTE cap node); p \<noteq> dest\<rbrakk> \<Longrightarrow> p \<noteq> src \<longrightarrow> (\<exists>node'. m p = Some (CTE cap node')) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n' p = Some (CTE cap node); p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> \<exists>node'. m p = Some (CTE cap node') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(mdbNext src_node \<noteq> p \<longrightarrow> (mdbPrev src_node \<noteq> p \<longrightarrow> m p = Some (CTE cap node)) \<and> (mdbPrev src_node = p \<longrightarrow> (\<exists>nodea. m p = Some (CTE cap nodea) \<and> mdbNext_update (\<lambda>_. dest) nodea = node))) \<and> (mdbNext src_node = p \<longrightarrow> (\<exists>nodea. (mdbPrev src_node \<noteq> p \<longrightarrow> m p = Some (CTE cap nodea)) \<and> (mdbPrev src_node = p \<longrightarrow> (\<exists>node. m p = Some (CTE cap node) \<and> mdbNext_update (\<lambda>_. dest) node = nodea)) \<and> mdbPrev_update (\<lambda>_. dest) nodea = node)); p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> \<exists>node'. m p = Some (CTE cap node') proof (prove)
goal:
No subgoals!