kings-crown/FVELER_Isabelle huggingface dataset:
theory CNodeInv_R

lemma (in mdb_swap) dest_prev_next [intro?]:
  "mdbPrev dest_node \<noteq> 0 \<Longrightarrow> m \<turnstile> mdbPrev dest_node \<leadsto> dest" using dest apply - apply (erule dlistEp) apply simp apply (rule next_fold) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdbPrev dest_node \<noteq> 0 \<Longrightarrow> m \<turnstile> mdbPrev dest_node \<leadsto> dest proof (prove)
using this:
m dest = Some (CTE dest_cap dest_node)

goal (1 subgoal):
 1. mdbPrev dest_node \<noteq> 0 \<Longrightarrow> m \<turnstile> mdbPrev dest_node \<leadsto> dest proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdbPrev dest_node \<noteq> 0; m dest = Some (CTE dest_cap dest_node)\<rbrakk> \<Longrightarrow> m \<turnstile> mdbPrev dest_node \<leadsto> dest proof (prove)
goal (2 subgoals):
 1. mdbPrev dest_node \<noteq> 0 \<Longrightarrow> mdbPrev (cteMDBNode (CTE dest_cap dest_node)) \<noteq> 0
 2. \<And>cte'. \<lbrakk>mdbPrev dest_node \<noteq> 0; m (mdbPrev (cteMDBNode (CTE dest_cap dest_node))) = Some cte'; mdbNext (cteMDBNode cte') = dest\<rbrakk> \<Longrightarrow> m \<turnstile> mdbPrev dest_node \<leadsto> dest proof (prove)
goal (1 subgoal):
 1. \<And>cte'. \<lbrakk>mdbPrev dest_node \<noteq> 0; m (mdbPrev (cteMDBNode (CTE dest_cap dest_node))) = Some cte'; mdbNext (cteMDBNode cte') = dest\<rbrakk> \<Longrightarrow> m \<turnstile> mdbPrev dest_node \<leadsto> dest proof (prove)
goal (2 subgoals):
 1. \<And>cte'. \<lbrakk>mdbPrev dest_node \<noteq> 0; m (mdbPrev (cteMDBNode (CTE dest_cap dest_node))) = Some cte'; mdbNext (cteMDBNode cte') = dest\<rbrakk> \<Longrightarrow> m (mdbPrev dest_node) = Some (?cte4 cte')
 2. \<And>cte'. \<lbrakk>mdbPrev dest_node \<noteq> 0; m (mdbPrev (cteMDBNode (CTE dest_cap dest_node))) = Some cte'; mdbNext (cteMDBNode cte') = dest\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode (?cte4 cte')) = dest proof (prove)
goal (1 subgoal):
 1. \<And>cte'. \<lbrakk>mdbPrev dest_node \<noteq> 0; m (mdbPrev (cteMDBNode (CTE dest_cap dest_node))) = Some cte'; mdbNext (cteMDBNode cte') = dest\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode cte') = dest proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma (in mdb_swap) dest2_node_next:
  "mdbNext dest2_node = (if dest = mdbPrev src_node then dest else mdbNext dest_node)" unfolding dest2_node_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdbNext dest2_node = (if dest = mdbPrev src_node then dest else mdbNext dest_node) proof (prove)
goal (1 subgoal):
 1. mdbNext (MDB (if dest = mdbPrev src_node then dest else mdbNext dest_node) (if dest = mdbNext src_node then dest else mdbPrev dest_node) (mdbRevocable dest_node) (mdbFirstBadged dest_node)) = (if dest = mdbPrev src_node then dest else mdbNext dest_node)
theory CNodeInv_R

lemma (in mdb_swap) dest2_node_prev:
  "mdbPrev dest2_node = (if dest = mdbNext src_node then dest else mdbPrev dest_node)" unfolding dest2_node_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdbPrev dest2_node = (if dest = mdbNext src_node then dest else mdbPrev dest_node) proof (prove)
goal (1 subgoal):
 1. mdbPrev (MDB (if dest = mdbPrev src_node then dest else mdbNext dest_node) (if dest = mdbNext src_node then dest else mdbPrev dest_node) (mdbRevocable dest_node) (mdbFirstBadged dest_node)) = (if dest = mdbNext src_node then dest else mdbPrev dest_node)
theory CNodeInv_R

lemma (in mdb_swap) n_other:
  assumes     other: "p \<noteq> mdbPrev src_node" "p \<noteq> src" "p \<noteq> mdbNext src_node"
  "p \<noteq> mdbPrev dest_node" "p \<noteq> dest" "p \<noteq> mdbNext dest_node"
  shows   "n p = m p" using other unfolding n_def n'_def by (simp add: modify_map_other dest2_node_next dest2_node_prev)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n p = m p proof (prove)
using this:
p \<noteq> mdbPrev src_node
p \<noteq> src
p \<noteq> mdbNext src_node
p \<noteq> mdbPrev dest_node
p \<noteq> dest
p \<noteq> mdbNext dest_node

goal (1 subgoal):
 1. n p = m p proof (prove)
using this:
p \<noteq> mdbPrev src_node
p \<noteq> src
p \<noteq> mdbNext src_node
p \<noteq> mdbPrev dest_node
p \<noteq> dest
p \<noteq> mdbNext dest_node

goal (1 subgoal):
 1. modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map m src (cteCap_update (\<lambda>_. dcap))) dest (cteCap_update (\<lambda>_. scap))) (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))) p = m p
theory CNodeInv_R

lemma (in mdb_swap) dom_n_m:
  "dom n = dom m" unfolding n_def n'_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dom n = dom m proof (prove)
goal (1 subgoal):
 1. dom (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map (modify_map m src (cteCap_update (\<lambda>_. dcap))) dest (cteCap_update (\<lambda>_. scap))) (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)))) = dom m
theory CNodeInv_R

lemma (in mdb_swap) swap_ptr_cases [case_names p_src_prev p_src p_src_next p_dest_prev p_dest p_dest_next p_other]:
  "\<lbrakk>p = mdbPrev src_node \<Longrightarrow> P; p = src \<Longrightarrow> P; p = mdbNext src_node \<Longrightarrow> P;
  p = mdbPrev dest_node \<Longrightarrow> P; p = dest \<Longrightarrow> P; p = mdbNext dest_node \<Longrightarrow> P;
  \<lbrakk>p \<noteq> mdbPrev src_node; p \<noteq> src; p \<noteq> mdbNext src_node;
  p \<noteq> mdbPrev dest_node; p \<noteq> dest; p \<noteq> mdbNext dest_node\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p = mdbPrev src_node \<Longrightarrow> P; p = src \<Longrightarrow> P; p = mdbNext src_node \<Longrightarrow> P; p = mdbPrev dest_node \<Longrightarrow> P; p = dest \<Longrightarrow> P; p = mdbNext dest_node \<Longrightarrow> P; \<lbrakk>p \<noteq> mdbPrev src_node; p \<noteq> src; p \<noteq> mdbNext src_node; p \<noteq> mdbPrev dest_node; p \<noteq> dest; p \<noteq> mdbNext dest_node\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
theory CNodeInv_R

lemma sameRegionAs_eq_child:
  "\<lbrakk> sameRegionAs cap c; weak_derived' c c' \<rbrakk>
  \<Longrightarrow> sameRegionAs cap c'" by (clarsimp simp: weak_derived'_def sameRegionAs_def2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>global.sameRegionAs cap c; weak_derived' c c'\<rbrakk> \<Longrightarrow> global.sameRegionAs cap c'
theory CNodeInv_R

lemma sameRegionAs_eq_parent:
  "\<lbrakk> sameRegionAs c cap; weak_derived' c c' \<rbrakk>
  \<Longrightarrow> sameRegionAs c' cap" by (clarsimp simp: weak_derived'_def sameRegionAs_def2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>global.sameRegionAs c cap; weak_derived' c c'\<rbrakk> \<Longrightarrow> global.sameRegionAs c' cap
theory CNodeInv_R

lemma sameRegionAs_dcap_parent:
  "sameRegionAs dcap cap = sameRegionAs dest_cap cap" apply (rule iffI) apply (erule sameRegionAs_eq_parent, rule weak_derived_sym', rule dest_derived) apply (erule sameRegionAs_eq_parent, rule dest_derived) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. global.sameRegionAs dcap cap = global.sameRegionAs dest_cap cap proof (prove)
goal (2 subgoals):
 1. global.sameRegionAs dcap cap \<Longrightarrow> global.sameRegionAs dest_cap cap
 2. global.sameRegionAs dest_cap cap \<Longrightarrow> global.sameRegionAs dcap cap proof (prove)
goal (1 subgoal):
 1. global.sameRegionAs dest_cap cap \<Longrightarrow> global.sameRegionAs dcap cap proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma sameRegionAs_dcap_child:
  "sameRegionAs cap dcap = sameRegionAs cap dest_cap" apply (rule iffI) apply (erule sameRegionAs_eq_child, rule weak_derived_sym', rule dest_derived) apply (erule sameRegionAs_eq_child, rule dest_derived) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. global.sameRegionAs cap dcap = global.sameRegionAs cap dest_cap proof (prove)
goal (2 subgoals):
 1. global.sameRegionAs cap dcap \<Longrightarrow> global.sameRegionAs cap dest_cap
 2. global.sameRegionAs cap dest_cap \<Longrightarrow> global.sameRegionAs cap dcap proof (prove)
goal (1 subgoal):
 1. global.sameRegionAs cap dest_cap \<Longrightarrow> global.sameRegionAs cap dcap proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma sameRegionAs_scap_parent:
  "sameRegionAs scap cap = sameRegionAs src_cap cap" apply (rule iffI) apply (erule sameRegionAs_eq_parent, rule weak_derived_sym', rule src_derived) apply (erule sameRegionAs_eq_parent, rule src_derived) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. global.sameRegionAs scap cap = global.sameRegionAs src_cap cap proof (prove)
goal (2 subgoals):
 1. global.sameRegionAs scap cap \<Longrightarrow> global.sameRegionAs src_cap cap
 2. global.sameRegionAs src_cap cap \<Longrightarrow> global.sameRegionAs scap cap proof (prove)
goal (1 subgoal):
 1. global.sameRegionAs src_cap cap \<Longrightarrow> global.sameRegionAs scap cap proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma master_srcI:
  "\<lbrakk> \<And>cap. F (capMasterCap cap) = F cap \<rbrakk>
      \<Longrightarrow> F scap = F src_cap" using src_derived by (clarsimp simp: weak_derived'_def elim!: master_eqI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>cap. F (capMasterCap cap) = F cap) \<Longrightarrow> F scap = F src_cap proof (prove)
using this:
weak_derived' src_cap scap

goal (1 subgoal):
 1. (\<And>cap. F (capMasterCap cap) = F cap) \<Longrightarrow> F scap = F src_cap
theory CNodeInv_R

lemma isEPsrc:
  "isEndpointCap scap = isEndpointCap src_cap" by (rule master_srcI, rule isCap_Master)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isEndpointCap scap = isEndpointCap src_cap
theory CNodeInv_R

lemma isEPbadge_src:
  "isEndpointCap src_cap \<Longrightarrow> capEPBadge scap = capEPBadge src_cap" using src_derived by (clarsimp simp: isCap_simps weak_derived'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isEndpointCap src_cap \<Longrightarrow> capEPBadge scap = capEPBadge src_cap proof (prove)
using this:
weak_derived' src_cap scap

goal (1 subgoal):
 1. isEndpointCap src_cap \<Longrightarrow> capEPBadge scap = capEPBadge src_cap
theory CNodeInv_R

lemma isNTFNsrc:
  "isNotificationCap scap = isNotificationCap src_cap" by (rule master_srcI, rule isCap_Master)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isNotificationCap scap = isNotificationCap src_cap
theory CNodeInv_R

lemma isNTFNbadge_src:
  "isNotificationCap src_cap \<Longrightarrow> capNtfnBadge scap = capNtfnBadge src_cap" using src_derived by (clarsimp simp: isCap_simps weak_derived'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isNotificationCap src_cap \<Longrightarrow> capNtfnBadge scap = capNtfnBadge src_cap proof (prove)
using this:
weak_derived' src_cap scap

goal (1 subgoal):
 1. isNotificationCap src_cap \<Longrightarrow> capNtfnBadge scap = capNtfnBadge src_cap
theory CNodeInv_R

lemma isEPdest:
  "isEndpointCap dcap = isEndpointCap dest_cap" using dest_derived by (fastforce simp: isCap_simps weak_derived'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isEndpointCap dcap = isEndpointCap dest_cap proof (prove)
using this:
weak_derived' dest_cap dcap

goal (1 subgoal):
 1. isEndpointCap dcap = isEndpointCap dest_cap
theory CNodeInv_R

lemma isEPbadge_dest:
  "isEndpointCap dest_cap \<Longrightarrow> capEPBadge dcap = capEPBadge dest_cap" using dest_derived by (auto simp: weak_derived'_def isCap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isEndpointCap dest_cap \<Longrightarrow> capEPBadge dcap = capEPBadge dest_cap proof (prove)
using this:
weak_derived' dest_cap dcap

goal (1 subgoal):
 1. isEndpointCap dest_cap \<Longrightarrow> capEPBadge dcap = capEPBadge dest_cap
theory CNodeInv_R

lemma isNTFNdest:
  "isNotificationCap dcap = isNotificationCap dest_cap" using dest_derived by (auto simp: weak_derived'_def isCap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isNotificationCap dcap = isNotificationCap dest_cap proof (prove)
using this:
weak_derived' dest_cap dcap

goal (1 subgoal):
 1. isNotificationCap dcap = isNotificationCap dest_cap
theory CNodeInv_R

lemma isNTFNbadge_dest:
  "isNotificationCap dest_cap \<Longrightarrow> capNtfnBadge dcap = capNtfnBadge dest_cap" using dest_derived by (auto simp: weak_derived'_def isCap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isNotificationCap dest_cap \<Longrightarrow> capNtfnBadge dcap = capNtfnBadge dest_cap proof (prove)
using this:
weak_derived' dest_cap dcap

goal (1 subgoal):
 1. isNotificationCap dest_cap \<Longrightarrow> capNtfnBadge dcap = capNtfnBadge dest_cap
theory CNodeInv_R

lemma sameRegion_ep:
  "\<lbrakk> sameRegionAs cap cap'; isEndpointCap cap \<rbrakk> \<Longrightarrow> isEndpointCap cap'" by (auto simp: isCap_simps sameRegionAs_def3)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>global.sameRegionAs cap cap'; isEndpointCap cap\<rbrakk> \<Longrightarrow> isEndpointCap cap'
theory CNodeInv_R

lemma sameRegion_ntfn:
  "\<lbrakk> sameRegionAs cap cap'; isNotificationCap cap \<rbrakk> \<Longrightarrow> isNotificationCap cap'" by (auto simp: isCap_simps sameRegionAs_def3)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>global.sameRegionAs cap cap'; isNotificationCap cap\<rbrakk> \<Longrightarrow> isNotificationCap cap'
theory CNodeInv_R

lemma (in mdb_swap) m_trancl:
  assumes "m \<turnstile> p \<leadsto>\<^sup>+ p'"
  shows "n \<turnstile> s_d_swp p \<leadsto>\<^sup>+ s_d_swp p'" using assms proof induct case (base x) thus ?case by (fastforce simp: next_m_n) next case (step x y) thus ?case by (fastforce simp: next_m_n elim: trancl_trans) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<turnstile> s_d_swp p \<leadsto>\<^sup>+ s_d_swp p' proof (prove)
using this:
m \<turnstile> p \<leadsto>\<^sup>+ p'

goal (1 subgoal):
 1. n \<turnstile> s_d_swp p \<leadsto>\<^sup>+ s_d_swp p' proof (state)
goal (2 subgoals):
 1. \<And>y. m \<turnstile> p \<leadsto> y \<Longrightarrow> n \<turnstile> s_d_swp p \<leadsto>\<^sup>+ s_d_swp y
 2. \<And>y z. \<lbrakk>m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; n \<turnstile> s_d_swp p \<leadsto>\<^sup>+ s_d_swp y\<rbrakk> \<Longrightarrow> n \<turnstile> s_d_swp p \<leadsto>\<^sup>+ s_d_swp z proof (state)
this:
m \<turnstile> p \<leadsto> x

goal (2 subgoals):
 1. \<And>y. m \<turnstile> p \<leadsto> y \<Longrightarrow> n \<turnstile> s_d_swp p \<leadsto>\<^sup>+ s_d_swp y
 2. \<And>y z. \<lbrakk>m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; n \<turnstile> s_d_swp p \<leadsto>\<^sup>+ s_d_swp y\<rbrakk> \<Longrightarrow> n \<turnstile> s_d_swp p \<leadsto>\<^sup>+ s_d_swp z proof (prove)
using this:
m \<turnstile> p \<leadsto> x

goal (1 subgoal):
 1. n \<turnstile> s_d_swp p \<leadsto>\<^sup>+ s_d_swp x proof (state)
this:
n \<turnstile> s_d_swp p \<leadsto>\<^sup>+ s_d_swp x

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; n \<turnstile> s_d_swp p \<leadsto>\<^sup>+ s_d_swp y\<rbrakk> \<Longrightarrow> n \<turnstile> s_d_swp p \<leadsto>\<^sup>+ s_d_swp z proof (state)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; n \<turnstile> s_d_swp p \<leadsto>\<^sup>+ s_d_swp y\<rbrakk> \<Longrightarrow> n \<turnstile> s_d_swp p \<leadsto>\<^sup>+ s_d_swp z proof (state)
this:
m \<turnstile> p \<leadsto>\<^sup>+ x
m \<turnstile> x \<leadsto> y
n \<turnstile> s_d_swp p \<leadsto>\<^sup>+ s_d_swp x

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>m \<turnstile> p \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto> z; n \<turnstile> s_d_swp p \<leadsto>\<^sup>+ s_d_swp y\<rbrakk> \<Longrightarrow> n \<turnstile> s_d_swp p \<leadsto>\<^sup>+ s_d_swp z proof (prove)
using this:
m \<turnstile> p \<leadsto>\<^sup>+ x
m \<turnstile> x \<leadsto> y
n \<turnstile> s_d_swp p \<leadsto>\<^sup>+ s_d_swp x

goal (1 subgoal):
 1. n \<turnstile> s_d_swp p \<leadsto>\<^sup>+ s_d_swp y proof (state)
this:
n \<turnstile> s_d_swp p \<leadsto>\<^sup>+ s_d_swp y

goal:
No subgoals!
theory CNodeInv_R

lemma (in mdb_swap) n_trancl:
  "n \<turnstile> p \<leadsto>\<^sup>+ p' = m \<turnstile> s_d_swp p \<leadsto>\<^sup>+ s_d_swp p'" proof assume "n \<turnstile> p \<leadsto>\<^sup>+ p'" thus "m \<turnstile> s_d_swp p \<leadsto>\<^sup>+ s_d_swp p'" by induct (auto simp: next_m_n2 elim!: trancl_trans) next assume "m \<turnstile> s_d_swp p \<leadsto>\<^sup>+ s_d_swp p'" thus "n \<turnstile> p \<leadsto>\<^sup>+ p'" by (fastforce dest: m_trancl) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<turnstile> p \<leadsto>\<^sup>+ p' = m \<turnstile> s_d_swp p \<leadsto>\<^sup>+ s_d_swp p' proof (state)
goal (2 subgoals):
 1. n \<turnstile> p \<leadsto>\<^sup>+ p' \<Longrightarrow> m \<turnstile> s_d_swp p \<leadsto>\<^sup>+ s_d_swp p'
 2. m \<turnstile> s_d_swp p \<leadsto>\<^sup>+ s_d_swp p' \<Longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ p' proof (state)
this:
n \<turnstile> p \<leadsto>\<^sup>+ p'

goal (2 subgoals):
 1. n \<turnstile> p \<leadsto>\<^sup>+ p' \<Longrightarrow> m \<turnstile> s_d_swp p \<leadsto>\<^sup>+ s_d_swp p'
 2. m \<turnstile> s_d_swp p \<leadsto>\<^sup>+ s_d_swp p' \<Longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
using this:
n \<turnstile> p \<leadsto>\<^sup>+ p'

goal (1 subgoal):
 1. m \<turnstile> s_d_swp p \<leadsto>\<^sup>+ s_d_swp p' proof (state)
this:
m \<turnstile> s_d_swp p \<leadsto>\<^sup>+ s_d_swp p'

goal (1 subgoal):
 1. m \<turnstile> s_d_swp p \<leadsto>\<^sup>+ s_d_swp p' \<Longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ p' proof (state)
goal (1 subgoal):
 1. m \<turnstile> s_d_swp p \<leadsto>\<^sup>+ s_d_swp p' \<Longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ p' proof (state)
this:
m \<turnstile> s_d_swp p \<leadsto>\<^sup>+ s_d_swp p'

goal (1 subgoal):
 1. m \<turnstile> s_d_swp p \<leadsto>\<^sup>+ s_d_swp p' \<Longrightarrow> n \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
using this:
m \<turnstile> s_d_swp p \<leadsto>\<^sup>+ s_d_swp p'

goal (1 subgoal):
 1. n \<turnstile> p \<leadsto>\<^sup>+ p' proof (state)
this:
n \<turnstile> p \<leadsto>\<^sup>+ p'

goal:
No subgoals!
theory CNodeInv_R

lemma (in mdb_swap) n_rtrancl:
  "n \<turnstile> p \<leadsto>\<^sup>* p' = m \<turnstile> s_d_swp p \<leadsto>\<^sup>* s_d_swp p'" by (simp add: rtrancl_eq_or_trancl n_trancl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<turnstile> p \<leadsto>\<^sup>* p' = m \<turnstile> s_d_swp p \<leadsto>\<^sup>* s_d_swp p'
theory CNodeInv_R

lemma (in mdb_swap) n_cap_eq:
  "(\<exists>n'. n p = Some (CTE cap n')) =
  (\<exists>n'. if p = src then m (s_d_swp p) = Some (CTE dest_cap n') \<and> cap = dcap
        else if p = dest then m (s_d_swp p) = Some (CTE src_cap n') \<and> cap = scap
        else m (s_d_swp p) = Some (CTE cap n'))" apply (simp add: s_d_swp_def n_cap_eq' src dest) apply (auto simp: s_d_swap_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<exists>n'. n p = Some (CTE cap n')) = (\<exists>n'. if p = src then m (s_d_swp p) = Some (CTE dest_cap n') \<and> cap = dcap else if p = dest then m (s_d_swp p) = Some (CTE src_cap n') \<and> cap = scap else m (s_d_swp p) = Some (CTE cap n')) proof (prove)
goal (1 subgoal):
 1. p \<noteq> dest \<longrightarrow> p \<noteq> src \<longrightarrow> (\<exists>n'. m p = Some (CTE cap n')) = (\<exists>n'. m (s_d_swap p src dest) = Some (CTE cap n')) proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma isUntyped_new:
  "isUntypedCap new = isUntypedCap old" using derived by (auto simp: weak_derived'_def isCap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isUntypedCap new = isUntypedCap old proof (prove)
using this:
weak_derived' new old

goal (1 subgoal):
 1. isUntypedCap new = isUntypedCap old
theory CNodeInv_R

lemma capRange_new:
  "capRange new = capRange old" using derived apply (clarsimp simp: weak_derived'_def) apply (rule master_eqI, rule capRange_Master) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. capRange new = capRange old proof (prove)
using this:
weak_derived' new old

goal (1 subgoal):
 1. capRange new = capRange old proof (prove)
goal (1 subgoal):
 1. \<lbrakk>capMasterCap new = capMasterCap old; capBadge new = capBadge old; capASID new = capASID old; cap_asid_base' new = cap_asid_base' old; cap_vptr' new = cap_vptr' old; isReplyCap new \<longrightarrow> capTCBPtr new = capTCBPtr old \<and> capReplyMaster new = capReplyMaster old\<rbrakk> \<Longrightarrow> capRange new = capRange old proof (prove)
goal (1 subgoal):
 1. \<lbrakk>capMasterCap new = capMasterCap old; capBadge new = capBadge old; capASID new = capASID old; cap_asid_base' new = cap_asid_base' old; cap_vptr' new = cap_vptr' old; isReplyCap new \<longrightarrow> capTCBPtr new = capTCBPtr old \<and> capReplyMaster new = capReplyMaster old\<rbrakk> \<Longrightarrow> capRange (capMasterCap new) = capRange (capMasterCap old) proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma isReplyMaster_eq:
  "(isReplyCap new \<and> capReplyMaster new)
      = (isReplyCap old \<and> capReplyMaster old)" using derived by (fastforce simp: weak_derived'_def isCap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (isReplyCap new \<and> capReplyMaster new) = (isReplyCap old \<and> capReplyMaster old) proof (prove)
using this:
weak_derived' new old

goal (1 subgoal):
 1. (isReplyCap new \<and> capReplyMaster new) = (isReplyCap old \<and> capReplyMaster old)
theory CNodeInv_R

lemma weak_derived_Null' [simp]:
  "weak_derived' cap NullCap = (cap = NullCap)" by (auto simp add: weak_derived'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. weak_derived' cap capability.NullCap = (cap = capability.NullCap)
theory CNodeInv_R

lemma Null_weak_derived_Null' [simp]:
  "weak_derived' NullCap cap = (cap = NullCap)" by (auto simp add: weak_derived'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. weak_derived' capability.NullCap cap = (cap = capability.NullCap)
theory CNodeInv_R

lemma weak_der_src:
  "weak_der' src_cap scap" apply unfold_locales apply (rule weak_derived_sym') apply (rule src_derived) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. weak_der' src_cap scap proof (prove)
goal (1 subgoal):
 1. weak_derived' scap src_cap proof (prove)
goal (1 subgoal):
 1. weak_derived' src_cap scap proof (prove)
goal:
No subgoals!
theory CNodeInv_R

lemma weak_der_dest:
  "weak_der' dest_cap dcap" apply unfold_locales apply (rule weak_derived_sym') apply (rule dest_derived) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. weak_der' dest_cap dcap proof (prove)
goal (1 subgoal):
 1. weak_derived' dcap dest_cap proof (prove)
goal (1 subgoal):
 1. weak_derived' dest_cap dcap proof (prove)
goal:
No subgoals!