theory CSpace1_R

lemma badge_n:
  "n p = Some (CTE cap node) \<Longrightarrow>
  if p = src then mdbFirstBadged node = mdbFirstBadged dest_node
  else if p = dest then mdbFirstBadged node = mdbFirstBadged src_node
  else \<exists>cap' node'. m p = Some (CTE cap' node') \<and>
                    mdbFirstBadged node = mdbFirstBadged node'" apply (drule sym) apply (insert src dest dest2 [symmetric])[1] apply clarsimp apply (rule conjI, clarsimp) apply (simp add: n_def n'_def modify_map_apply) apply (simp add: modify_map_def const_def split: if_split_asm) apply clarsimp apply (rule conjI, clarsimp) apply (simp add: n_def n'_def modify_map_apply) apply (simp add: modify_map_def const_def split: if_split_asm) apply (clarsimp simp: n_def) apply (clarsimp simp add: modify_map_def map_option_case split: if_split_asm option.splits) apply (auto split: cteMDBNode_update_split_asm elim: badge_n' badge_n'[OF sym]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n p = Some (CTE cap node) \<Longrightarrow> if p = src then mdbFirstBadged node = mdbFirstBadged dest_node else if p = dest then mdbFirstBadged node = mdbFirstBadged src_node else \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbFirstBadged node = mdbFirstBadged node' proof (prove)
goal (1 subgoal):
 1. Some (CTE cap node) = n p \<Longrightarrow> if p = src then mdbFirstBadged node = mdbFirstBadged dest_node else if p = dest then mdbFirstBadged node = mdbFirstBadged src_node else \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbFirstBadged node = mdbFirstBadged node' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Some (CTE cap node) = n p; m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); Some dest2 = n' dest\<rbrakk> \<Longrightarrow> if p = src then mdbFirstBadged node = mdbFirstBadged dest_node else if p = dest then mdbFirstBadged node = mdbFirstBadged src_node else \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbFirstBadged node = mdbFirstBadged node' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Some (CTE cap node) = n p; m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); Some dest2 = n' dest\<rbrakk> \<Longrightarrow> (p = dest \<longrightarrow> mdbFirstBadged node = mdbFirstBadged src_node) \<and> (p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> mdbFirstBadged node = mdbFirstBadged dest_node) \<and> (p \<noteq> src \<longrightarrow> (\<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbFirstBadged node = mdbFirstBadged node'))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>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; p = dest\<rbrakk> \<Longrightarrow> mdbFirstBadged node = mdbFirstBadged src_node
 2. \<lbrakk>Some (CTE cap node) = n p; m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); Some dest2 = n' dest\<rbrakk> \<Longrightarrow> p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> mdbFirstBadged node = mdbFirstBadged dest_node) \<and> (p \<noteq> src \<longrightarrow> (\<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbFirstBadged node = mdbFirstBadged node')) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>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; p = dest\<rbrakk> \<Longrightarrow> mdbFirstBadged node = mdbFirstBadged src_node
 2. \<lbrakk>Some (CTE cap node) = n p; m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); Some dest2 = n' dest\<rbrakk> \<Longrightarrow> p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> mdbFirstBadged node = mdbFirstBadged dest_node) \<and> (p \<noteq> src \<longrightarrow> (\<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbFirstBadged node = mdbFirstBadged node')) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Some (CTE cap node) = n p; m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); Some dest2 = n' dest\<rbrakk> \<Longrightarrow> p \<noteq> dest \<longrightarrow> (p = src \<longrightarrow> mdbFirstBadged node = mdbFirstBadged dest_node) \<and> (p \<noteq> src \<longrightarrow> (\<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbFirstBadged node = mdbFirstBadged node')) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Some (CTE cap node) = n p; m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); Some dest2 = n' dest; p \<noteq> dest\<rbrakk> \<Longrightarrow> (p = src \<longrightarrow> mdbFirstBadged node = mdbFirstBadged dest_node) \<and> (p \<noteq> src \<longrightarrow> (\<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbFirstBadged node = mdbFirstBadged node')) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>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; p = src\<rbrakk> \<Longrightarrow> mdbFirstBadged node = mdbFirstBadged dest_node
 2. \<lbrakk>Some (CTE cap node) = n p; m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); Some dest2 = n' dest; p \<noteq> dest\<rbrakk> \<Longrightarrow> p \<noteq> src \<longrightarrow> (\<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbFirstBadged node = mdbFirstBadged node') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>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; p = src\<rbrakk> \<Longrightarrow> mdbFirstBadged node = mdbFirstBadged dest_node
 2. \<lbrakk>Some (CTE cap node) = n p; m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); Some dest2 = n' dest; p \<noteq> dest\<rbrakk> \<Longrightarrow> p \<noteq> src \<longrightarrow> (\<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbFirstBadged node = mdbFirstBadged node') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Some (CTE cap node) = n p; m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); Some dest2 = n' dest; p \<noteq> dest\<rbrakk> \<Longrightarrow> p \<noteq> src \<longrightarrow> (\<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbFirstBadged node = mdbFirstBadged node') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Some (CTE cap node) = modify_map (modify_map (modify_map (modify_map n' 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))) p; m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); Some dest2 = n' dest; p \<noteq> dest; p \<noteq> src\<rbrakk> \<Longrightarrow> \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbFirstBadged node = mdbFirstBadged node' proof (prove)
goal (4 subgoals):
 1. \<And>x2a. \<lbrakk>CTE cap node = cteMDBNode_update (mdbPrev_update (\<lambda>_. src)) (cteMDBNode_update (mdbNext_update (\<lambda>_. src)) x2a); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); Some dest2 = n' dest; mdbPrev (cteMDBNode dest2) \<noteq> dest; mdbPrev (cteMDBNode dest2) \<noteq> src; p = mdbPrev (cteMDBNode dest2); mdbNext (cteMDBNode dest2) = mdbPrev (cteMDBNode dest2); n' (mdbPrev (cteMDBNode dest2)) = Some x2a\<rbrakk> \<Longrightarrow> \<exists>cap' node'. m (mdbPrev (cteMDBNode dest2)) = Some (CTE cap' node') \<and> mdbFirstBadged node = mdbFirstBadged node'
 2. \<And>x2. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); Some dest2 = n' dest; mdbNext (cteMDBNode dest2) \<noteq> dest; mdbNext (cteMDBNode dest2) \<noteq> src; p = mdbNext (cteMDBNode dest2); mdbNext (cteMDBNode dest2) \<noteq> mdbPrev (cteMDBNode dest2); n' (mdbNext (cteMDBNode dest2)) = Some x2; CTE cap node = cteMDBNode_update (mdbPrev_update (\<lambda>_. src)) x2\<rbrakk> \<Longrightarrow> \<exists>cap' node'. m (mdbNext (cteMDBNode dest2)) = Some (CTE cap' node') \<and> mdbFirstBadged node = mdbFirstBadged node'
 3. \<And>x2. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); Some dest2 = n' dest; mdbPrev (cteMDBNode dest2) \<noteq> dest; mdbPrev (cteMDBNode dest2) \<noteq> src; mdbPrev (cteMDBNode dest2) \<noteq> mdbNext (cteMDBNode dest2); p = mdbPrev (cteMDBNode dest2); n' (mdbPrev (cteMDBNode dest2)) = Some x2; CTE cap node = cteMDBNode_update (mdbNext_update (\<lambda>_. src)) x2\<rbrakk> \<Longrightarrow> \<exists>cap' node'. m (mdbPrev (cteMDBNode dest2)) = Some (CTE cap' node') \<and> mdbFirstBadged node = mdbFirstBadged node'
 4. \<lbrakk>m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); Some dest2 = n' dest; p \<noteq> dest; p \<noteq> src; p \<noteq> mdbNext (cteMDBNode dest2); p \<noteq> mdbPrev (cteMDBNode dest2); Some (CTE cap node) = n' p\<rbrakk> \<Longrightarrow> \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbFirstBadged node = mdbFirstBadged node' proof (prove)
goal:
No subgoals!