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, clarsimp) apply (drule sym) apply (insert src dest dest2 [symmetric])[1] apply (simp add: n_def n'_def modify_map_apply) apply (simp add: modify_map_def split: if_split_asm) apply clarsimp apply (rule conjI, clarsimp) apply (drule sym) apply (insert src dest dest2 [symmetric])[1] apply (simp add: n_def n'_def modify_map_apply) apply (simp add: modify_map_def split: if_split_asm) apply clarsimp apply (insert src dest dest2) apply (clarsimp simp: n_def modify_map_cases) apply (auto dest: n'_cap) 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. \<lbrakk>n dest = Some (CTE cap node); p = dest\<rbrakk> \<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 (2 subgoals):
 1. \<lbrakk>p = dest; Some (CTE cap node) = n dest\<rbrakk> \<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 (2 subgoals):
 1. \<lbrakk>p = dest; Some (CTE cap node) = n dest; m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); Some dest2 = n' dest\<rbrakk> \<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 (2 subgoals):
 1. \<lbrakk>p = dest; Some (CTE cap node) = modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (m(src \<mapsto> CTE dcap src_node, dest \<mapsto> CTE scap dest_node)) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) src (cteMDBNode_update (const (cteMDBNode dest2)))) dest (cteMDBNode_update (const src_node))) (mdbPrev (cteMDBNode dest2)) (cteMDBNode_update (mdbNext_update (\<lambda>_. src)))) (mdbNext (cteMDBNode dest2)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. src))) dest; m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); Some dest2 = modify_map (modify_map (m(src \<mapsto> CTE dcap src_node, dest \<mapsto> CTE scap dest_node)) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) dest\<rbrakk> \<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 src = Some (CTE cap node); p = src\<rbrakk> \<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 (2 subgoals):
 1. \<lbrakk>p = src; Some (CTE cap node) = n src\<rbrakk> \<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 (2 subgoals):
 1. \<lbrakk>p = src; Some (CTE cap node) = n src; m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); Some dest2 = n' dest\<rbrakk> \<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 (2 subgoals):
 1. \<lbrakk>p = src; Some (CTE cap node) = modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (m(src \<mapsto> CTE dcap src_node, dest \<mapsto> CTE scap dest_node)) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest)))) src (cteMDBNode_update (const (cteMDBNode dest2)))) dest (cteMDBNode_update (const src_node))) (mdbPrev (cteMDBNode dest2)) (cteMDBNode_update (mdbNext_update (\<lambda>_. src)))) (mdbNext (cteMDBNode dest2)) (cteMDBNode_update (mdbPrev_update (\<lambda>_. src))) src; m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); Some dest2 = modify_map (modify_map (m(src \<mapsto> CTE dcap src_node, dest \<mapsto> CTE scap dest_node)) (mdbPrev src_node) (cteMDBNode_update (mdbNext_update (\<lambda>_. dest)))) (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))) dest\<rbrakk> \<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>n p = Some (CTE cap node); p \<noteq> dest; p \<noteq> src; m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); n' dest = Some dest2\<rbrakk> \<Longrightarrow> \<exists>node'. m p = Some (CTE cap node') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<noteq> dest; p \<noteq> src; m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); n' dest = Some dest2; mdbNext (cteMDBNode dest2) \<noteq> p \<longrightarrow> (mdbPrev (cteMDBNode dest2) \<noteq> p \<longrightarrow> n' p = Some (CTE cap node)) \<and> (mdbPrev (cteMDBNode dest2) = p \<longrightarrow> (\<exists>nodea. n' p = Some (CTE cap nodea) \<and> mdbNext_update (\<lambda>_. src) nodea = node)); mdbNext (cteMDBNode dest2) = p \<longrightarrow> (\<exists>nodea. (mdbPrev (cteMDBNode dest2) \<noteq> p \<longrightarrow> n' p = Some (CTE cap nodea)) \<and> (mdbPrev (cteMDBNode dest2) = p \<longrightarrow> (\<exists>node. n' p = Some (CTE cap node) \<and> mdbNext_update (\<lambda>_. src) node = nodea)) \<and> mdbPrev_update (\<lambda>_. src) nodea = node)\<rbrakk> \<Longrightarrow> \<exists>node'. m p = Some (CTE cap node') proof (prove)
goal:
No subgoals!