theory CNodeInv_R

lemma n_prevD:
  notes if_cong [cong] option.case_cong [cong]
  shows "n \<turnstile> p \<leftarrow> p' \<Longrightarrow> m \<turnstile> s_d_swp p \<leftarrow> s_d_swp p'" apply (cases "p'=0") apply (simp add: mdb_prev_def) apply (cases "p=0") apply (clarsimp simp: mdb_prev_def s_d_swap_def) apply (rule conjI) apply clarsimp apply (simp add: n_dest) apply (case_tac z) apply (clarsimp simp: src split: if_split_asm) apply clarsimp apply (rule conjI) apply (clarsimp simp: dest) apply (simp add: dest2_node_def split: if_split_asm) apply clarsimp apply (case_tac z) apply clarsimp apply (simp add: n_def n'_def modify_map_if dest2_node_def) apply (insert src dest)[1] apply (clarsimp split: if_split_asm) apply (simp add: Invariants_H.valid_dlist_prevD [OF cteSwap_dlist_helper, symmetric]) apply (simp add: Invariants_H.valid_dlist_prevD [OF dlist, symmetric] next_m_n2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<turnstile> p \<leftarrow> p' \<Longrightarrow> m \<turnstile> s_d_swp p \<leftarrow> s_d_swp p' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<turnstile> p \<leftarrow> p'; p' = 0\<rbrakk> \<Longrightarrow> m \<turnstile> s_d_swp p \<leftarrow> s_d_swp p'
 2. \<lbrakk>n \<turnstile> p \<leftarrow> p'; p' \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> s_d_swp p \<leftarrow> s_d_swp p' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<turnstile> p \<leftarrow> p'; p' \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> s_d_swp p \<leftarrow> s_d_swp p' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<turnstile> p \<leftarrow> p'; p' \<noteq> 0; p = 0\<rbrakk> \<Longrightarrow> m \<turnstile> s_d_swp p \<leftarrow> s_d_swp p'
 2. \<lbrakk>n \<turnstile> p \<leftarrow> p'; p' \<noteq> 0; p \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> s_d_swp p \<leftarrow> s_d_swp p' proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>p' \<noteq> 0; p = 0; n p' = Some z; mdbPrev (cteMDBNode z) = 0\<rbrakk> \<Longrightarrow> (p' = dest \<longrightarrow> (\<exists>z. m src = Some z \<and> mdbPrev (cteMDBNode z) = 0)) \<and> (p' \<noteq> dest \<longrightarrow> (p' = src \<longrightarrow> (\<exists>z. m dest = Some z \<and> mdbPrev (cteMDBNode z) = 0)) \<and> (p' \<noteq> src \<longrightarrow> (\<exists>z. m p' = Some z \<and> mdbPrev (cteMDBNode z) = 0)))
 2. \<lbrakk>n \<turnstile> p \<leftarrow> p'; p' \<noteq> 0; p \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> s_d_swp p \<leftarrow> s_d_swp p' proof (prove)
goal (3 subgoals):
 1. \<And>z. \<lbrakk>p' \<noteq> 0; p = 0; n p' = Some z; mdbPrev (cteMDBNode z) = 0\<rbrakk> \<Longrightarrow> p' = dest \<longrightarrow> (\<exists>z. m src = Some z \<and> mdbPrev (cteMDBNode z) = 0)
 2. \<And>z. \<lbrakk>p' \<noteq> 0; p = 0; n p' = Some z; mdbPrev (cteMDBNode z) = 0\<rbrakk> \<Longrightarrow> p' \<noteq> dest \<longrightarrow> (p' = src \<longrightarrow> (\<exists>z. m dest = Some z \<and> mdbPrev (cteMDBNode z) = 0)) \<and> (p' \<noteq> src \<longrightarrow> (\<exists>z. m p' = Some z \<and> mdbPrev (cteMDBNode z) = 0))
 3. \<lbrakk>n \<turnstile> p \<leftarrow> p'; p' \<noteq> 0; p \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> s_d_swp p \<leftarrow> s_d_swp p' proof (prove)
goal (3 subgoals):
 1. \<And>z. \<lbrakk>p = 0; n dest = Some z; mdbPrev (cteMDBNode z) = 0; p' = dest\<rbrakk> \<Longrightarrow> \<exists>z. m src = Some z \<and> mdbPrev (cteMDBNode z) = 0
 2. \<And>z. \<lbrakk>p' \<noteq> 0; p = 0; n p' = Some z; mdbPrev (cteMDBNode z) = 0\<rbrakk> \<Longrightarrow> p' \<noteq> dest \<longrightarrow> (p' = src \<longrightarrow> (\<exists>z. m dest = Some z \<and> mdbPrev (cteMDBNode z) = 0)) \<and> (p' \<noteq> src \<longrightarrow> (\<exists>z. m p' = Some z \<and> mdbPrev (cteMDBNode z) = 0))
 3. \<lbrakk>n \<turnstile> p \<leftarrow> p'; p' \<noteq> 0; p \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> s_d_swp p \<leftarrow> s_d_swp p' proof (prove)
goal (3 subgoals):
 1. \<And>z. \<lbrakk>p = 0; CTE scap (MDB (if mdbNext src_node = dest then src else mdbNext src_node) (if mdbPrev src_node = dest then src else mdbPrev src_node) (mdbRevocable src_node) (mdbFirstBadged src_node)) = z; mdbPrev (cteMDBNode z) = 0; p' = dest\<rbrakk> \<Longrightarrow> \<exists>z. m src = Some z \<and> mdbPrev (cteMDBNode z) = 0
 2. \<And>z. \<lbrakk>p' \<noteq> 0; p = 0; n p' = Some z; mdbPrev (cteMDBNode z) = 0\<rbrakk> \<Longrightarrow> p' \<noteq> dest \<longrightarrow> (p' = src \<longrightarrow> (\<exists>z. m dest = Some z \<and> mdbPrev (cteMDBNode z) = 0)) \<and> (p' \<noteq> src \<longrightarrow> (\<exists>z. m p' = Some z \<and> mdbPrev (cteMDBNode z) = 0))
 3. \<lbrakk>n \<turnstile> p \<leftarrow> p'; p' \<noteq> 0; p \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> s_d_swp p \<leftarrow> s_d_swp p' proof (prove)
goal (3 subgoals):
 1. \<And>z x1 x2. \<lbrakk>p = 0; CTE scap (MDB (if mdbNext src_node = dest then src else mdbNext src_node) (if mdbPrev src_node = dest then src else mdbPrev src_node) (mdbRevocable src_node) (mdbFirstBadged src_node)) = z; mdbPrev (cteMDBNode z) = 0; p' = dest; z = CTE x1 x2\<rbrakk> \<Longrightarrow> \<exists>z. m src = Some z \<and> mdbPrev (cteMDBNode z) = 0
 2. \<And>z. \<lbrakk>p' \<noteq> 0; p = 0; n p' = Some z; mdbPrev (cteMDBNode z) = 0\<rbrakk> \<Longrightarrow> p' \<noteq> dest \<longrightarrow> (p' = src \<longrightarrow> (\<exists>z. m dest = Some z \<and> mdbPrev (cteMDBNode z) = 0)) \<and> (p' \<noteq> src \<longrightarrow> (\<exists>z. m p' = Some z \<and> mdbPrev (cteMDBNode z) = 0))
 3. \<lbrakk>n \<turnstile> p \<leftarrow> p'; p' \<noteq> 0; p \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> s_d_swp p \<leftarrow> s_d_swp p' proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>p' \<noteq> 0; p = 0; n p' = Some z; mdbPrev (cteMDBNode z) = 0\<rbrakk> \<Longrightarrow> p' \<noteq> dest \<longrightarrow> (p' = src \<longrightarrow> (\<exists>z. m dest = Some z \<and> mdbPrev (cteMDBNode z) = 0)) \<and> (p' \<noteq> src \<longrightarrow> (\<exists>z. m p' = Some z \<and> mdbPrev (cteMDBNode z) = 0))
 2. \<lbrakk>n \<turnstile> p \<leftarrow> p'; p' \<noteq> 0; p \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> s_d_swp p \<leftarrow> s_d_swp p' proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>p' \<noteq> 0; p = 0; n p' = Some z; mdbPrev (cteMDBNode z) = 0; p' \<noteq> dest\<rbrakk> \<Longrightarrow> (p' = src \<longrightarrow> (\<exists>z. m dest = Some z \<and> mdbPrev (cteMDBNode z) = 0)) \<and> (p' \<noteq> src \<longrightarrow> (\<exists>z. m p' = Some z \<and> mdbPrev (cteMDBNode z) = 0))
 2. \<lbrakk>n \<turnstile> p \<leftarrow> p'; p' \<noteq> 0; p \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> s_d_swp p \<leftarrow> s_d_swp p' proof (prove)
goal (3 subgoals):
 1. \<And>z. \<lbrakk>p' \<noteq> 0; p = 0; n p' = Some z; mdbPrev (cteMDBNode z) = 0; p' \<noteq> dest\<rbrakk> \<Longrightarrow> p' = src \<longrightarrow> (\<exists>z. m dest = Some z \<and> mdbPrev (cteMDBNode z) = 0)
 2. \<And>z. \<lbrakk>p' \<noteq> 0; p = 0; n p' = Some z; mdbPrev (cteMDBNode z) = 0; p' \<noteq> dest\<rbrakk> \<Longrightarrow> p' \<noteq> src \<longrightarrow> (\<exists>z. m p' = Some z \<and> mdbPrev (cteMDBNode z) = 0)
 3. \<lbrakk>n \<turnstile> p \<leftarrow> p'; p' \<noteq> 0; p \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> s_d_swp p \<leftarrow> s_d_swp p' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>p = 0; mdbPrev dest2_node = 0; p' = src\<rbrakk> \<Longrightarrow> mdbPrev dest_node = 0
 2. \<And>z. \<lbrakk>p' \<noteq> 0; p = 0; n p' = Some z; mdbPrev (cteMDBNode z) = 0; p' \<noteq> dest\<rbrakk> \<Longrightarrow> p' \<noteq> src \<longrightarrow> (\<exists>z. m p' = Some z \<and> mdbPrev (cteMDBNode z) = 0)
 3. \<lbrakk>n \<turnstile> p \<leftarrow> p'; p' \<noteq> 0; p \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> s_d_swp p \<leftarrow> s_d_swp p' proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>p' \<noteq> 0; p = 0; n p' = Some z; mdbPrev (cteMDBNode z) = 0; p' \<noteq> dest\<rbrakk> \<Longrightarrow> p' \<noteq> src \<longrightarrow> (\<exists>z. m p' = Some z \<and> mdbPrev (cteMDBNode z) = 0)
 2. \<lbrakk>n \<turnstile> p \<leftarrow> p'; p' \<noteq> 0; p \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> s_d_swp p \<leftarrow> s_d_swp p' proof (prove)
goal (2 subgoals):
 1. \<And>z. \<lbrakk>p' \<noteq> 0; p = 0; n p' = Some z; mdbPrev (cteMDBNode z) = 0; p' \<noteq> dest; p' \<noteq> src\<rbrakk> \<Longrightarrow> \<exists>z. m p' = Some z \<and> mdbPrev (cteMDBNode z) = 0
 2. \<lbrakk>n \<turnstile> p \<leftarrow> p'; p' \<noteq> 0; p \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> s_d_swp p \<leftarrow> s_d_swp p' proof (prove)
goal (2 subgoals):
 1. \<And>z x1 x2. \<lbrakk>p' \<noteq> 0; p = 0; n p' = Some z; mdbPrev (cteMDBNode z) = 0; p' \<noteq> dest; p' \<noteq> src; z = CTE x1 x2\<rbrakk> \<Longrightarrow> \<exists>z. m p' = Some z \<and> mdbPrev (cteMDBNode z) = 0
 2. \<lbrakk>n \<turnstile> p \<leftarrow> p'; p' \<noteq> 0; p \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> s_d_swp p \<leftarrow> s_d_swp p' proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2. \<lbrakk>p' \<noteq> 0; p = 0; n p' = Some (CTE x1 x2); mdbPrev x2 = 0; p' \<noteq> dest; p' \<noteq> src\<rbrakk> \<Longrightarrow> \<exists>z. m p' = Some z \<and> mdbPrev (cteMDBNode z) = 0
 2. \<lbrakk>n \<turnstile> p \<leftarrow> p'; p' \<noteq> 0; p \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> s_d_swp p \<leftarrow> s_d_swp p' proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2. \<lbrakk>p' \<noteq> 0; p = 0; if (if dest = mdbPrev src_node then mdbPrev src_node else mdbNext dest_node) = p' then \<exists>node. (if (if dest = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) = p' then \<exists>nodea. (if mdbNext src_node = p' then \<exists>node. (if mdbPrev src_node = p' then \<exists>nodea. m p' = Some (CTE x1 nodea) \<and> mdbNext_update (\<lambda>_. dest) nodea = node else m p' = Some (CTE x1 node)) \<and> mdbPrev_update (\<lambda>_. dest) node = nodea else if mdbPrev src_node = p' then \<exists>node. m p' = Some (CTE x1 node) \<and> mdbNext_update (\<lambda>_. dest) node = nodea else m p' = Some (CTE x1 nodea)) \<and> mdbNext_update (\<lambda>_. src) nodea = node else if mdbNext src_node = p' then \<exists>nodea. (if mdbPrev src_node = p' then \<exists>node. m p' = Some (CTE x1 node) \<and> mdbNext_update (\<lambda>_. dest) node = nodea else m p' = Some (CTE x1 nodea)) \<and> mdbPrev_update (\<lambda>_. dest) nodea = node else if mdbPrev src_node = p' then \<exists>nodea. m p' = Some (CTE x1 nodea) \<and> mdbNext_update (\<lambda>_. dest) nodea = node else m p' = Some (CTE x1 node)) \<and> mdbPrev_update (\<lambda>_. src) node = x2 else if (if dest = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) = p' then \<exists>node. (if mdbNext src_node = p' then \<exists>nodea. (if mdbPrev src_node = p' then \<exists>node. m p' = Some (CTE x1 node) \<and> mdbNext_update (\<lambda>_. dest) node = nodea else m p' = Some (CTE x1 nodea)) \<and> mdbPrev_update (\<lambda>_. dest) nodea = node else if mdbPrev src_node = p' then \<exists>nodea. m p' = Some (CTE x1 nodea) \<and> mdbNext_update (\<lambda>_. dest) nodea = node else m p' = Some (CTE x1 node)) \<and> mdbNext_update (\<lambda>_. src) node = x2 else if mdbNext src_node = p' then \<exists>node. (if mdbPrev src_node = p' then \<exists>nodea. m p' = Some (CTE x1 nodea) \<and> mdbNext_update (\<lambda>_. dest) nodea = node else m p' = Some (CTE x1 node)) \<and> mdbPrev_update (\<lambda>_. dest) node = x2 else if mdbPrev src_node = p' then \<exists>node. m p' = Some (CTE x1 node) \<and> mdbNext_update (\<lambda>_. dest) node = x2 else m p' = Some (CTE x1 x2); mdbPrev x2 = 0; p' \<noteq> dest; p' \<noteq> src\<rbrakk> \<Longrightarrow> \<exists>z. m p' = Some z \<and> mdbPrev (cteMDBNode z) = 0
 2. \<lbrakk>n \<turnstile> p \<leftarrow> p'; p' \<noteq> 0; p \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> s_d_swp p \<leftarrow> s_d_swp p' proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2. \<lbrakk>p' \<noteq> 0; p = 0; if (if dest = mdbPrev src_node then mdbPrev src_node else mdbNext dest_node) = p' then \<exists>node. (if (if dest = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) = p' then \<exists>nodea. (if mdbNext src_node = p' then \<exists>node. (if mdbPrev src_node = p' then \<exists>nodea. m p' = Some (CTE x1 nodea) \<and> mdbNext_update (\<lambda>_. dest) nodea = node else m p' = Some (CTE x1 node)) \<and> mdbPrev_update (\<lambda>_. dest) node = nodea else if mdbPrev src_node = p' then \<exists>node. m p' = Some (CTE x1 node) \<and> mdbNext_update (\<lambda>_. dest) node = nodea else m p' = Some (CTE x1 nodea)) \<and> mdbNext_update (\<lambda>_. src) nodea = node else if mdbNext src_node = p' then \<exists>nodea. (if mdbPrev src_node = p' then \<exists>node. m p' = Some (CTE x1 node) \<and> mdbNext_update (\<lambda>_. dest) node = nodea else m p' = Some (CTE x1 nodea)) \<and> mdbPrev_update (\<lambda>_. dest) nodea = node else if mdbPrev src_node = p' then \<exists>nodea. m p' = Some (CTE x1 nodea) \<and> mdbNext_update (\<lambda>_. dest) nodea = node else m p' = Some (CTE x1 node)) \<and> mdbPrev_update (\<lambda>_. src) node = x2 else if (if dest = mdbNext src_node then mdbNext src_node else mdbPrev dest_node) = p' then \<exists>node. (if mdbNext src_node = p' then \<exists>nodea. (if mdbPrev src_node = p' then \<exists>node. m p' = Some (CTE x1 node) \<and> mdbNext_update (\<lambda>_. dest) node = nodea else m p' = Some (CTE x1 nodea)) \<and> mdbPrev_update (\<lambda>_. dest) nodea = node else if mdbPrev src_node = p' then \<exists>nodea. m p' = Some (CTE x1 nodea) \<and> mdbNext_update (\<lambda>_. dest) nodea = node else m p' = Some (CTE x1 node)) \<and> mdbNext_update (\<lambda>_. src) node = x2 else if mdbNext src_node = p' then \<exists>node. (if mdbPrev src_node = p' then \<exists>nodea. m p' = Some (CTE x1 nodea) \<and> mdbNext_update (\<lambda>_. dest) nodea = node else m p' = Some (CTE x1 node)) \<and> mdbPrev_update (\<lambda>_. dest) node = x2 else if mdbPrev src_node = p' then \<exists>node. m p' = Some (CTE x1 node) \<and> mdbNext_update (\<lambda>_. dest) node = x2 else m p' = Some (CTE x1 x2); mdbPrev x2 = 0; p' \<noteq> dest; p' \<noteq> src; m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node)\<rbrakk> \<Longrightarrow> \<exists>z. m p' = Some z \<and> mdbPrev (cteMDBNode z) = 0
 2. \<lbrakk>n \<turnstile> p \<leftarrow> p'; p' \<noteq> 0; p \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> s_d_swp p \<leftarrow> s_d_swp p' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<turnstile> p \<leftarrow> p'; p' \<noteq> 0; p \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> s_d_swp p \<leftarrow> s_d_swp p' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<turnstile> p \<leadsto> p'; p' \<noteq> 0; p \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> s_d_swap p src dest \<leftarrow> s_d_swap p' src dest proof (prove)
goal:
No subgoals!