kings-crown/FVELER_Isabelle huggingface dataset:
theory CSpace1_R

lemma updateMDB_the_lot':
  assumes "(x, s'') \<in> fst (updateMDB p f s')"
  assumes "pspace_relations (ekheap sa) (kheap s) (ksPSpace s')"
  assumes "pspace_aligned' s'" "pspace_distinct' s'" "no_0 (ctes_of s')" "ekheap s = ekheap sa"
  shows "ctes_of s'' = modify_map (ctes_of s') p (cteMDBNode_update f) \<and>
         ksMachineState s'' = ksMachineState s' \<and>
         ksWorkUnitsCompleted s'' = ksWorkUnitsCompleted s' \<and>
         ksCurThread s'' = ksCurThread s' \<and>
         ksIdleThread s'' = ksIdleThread s' \<and>
         ksReadyQueues s'' = ksReadyQueues s' \<and>
         ksSchedulerAction s'' = ksSchedulerAction s' \<and>
         ksInterruptState s'' = ksInterruptState s' \<and>
         ksArchState s'' = ksArchState s' \<and>
         gsUserPages s'' = gsUserPages s' \<and>
         gsCNodes s'' = gsCNodes s' \<and>
         pspace_relations (ekheap s) (kheap s) (ksPSpace s'') \<and>
         pspace_aligned' s'' \<and> pspace_distinct' s'' \<and>
         no_0 (ctes_of s'') \<and>
         ksDomScheduleIdx s'' = ksDomScheduleIdx s' \<and>
         ksDomSchedule s''    = ksDomSchedule s' \<and>
         ksCurDomain s''      = ksCurDomain s' \<and>
         ksDomainTime s''     = ksDomainTime s'" apply (rule updateMDB_the_lot) using assms apply (fastforce simp: pspace_relations_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ctes_of s'' = modify_map (ctes_of s') p (cteMDBNode_update f) \<and> ksMachineState s'' = ksMachineState s' \<and> ksWorkUnitsCompleted s'' = ksWorkUnitsCompleted s' \<and> ksCurThread s'' = ksCurThread s' \<and> ksIdleThread s'' = ksIdleThread s' \<and> ksReadyQueues s'' = ksReadyQueues s' \<and> ksSchedulerAction s'' = ksSchedulerAction s' \<and> ksInterruptState s'' = ksInterruptState s' \<and> ksArchState s'' = ksArchState s' \<and> gsUserPages s'' = gsUserPages s' \<and> gsCNodes s'' = gsCNodes s' \<and> pspace_relations (ekheap s) (kheap s) (ksPSpace s'') \<and> pspace_aligned' s'' \<and> pspace_distinct' s'' \<and> no_0 (ctes_of s'') \<and> ksDomScheduleIdx s'' = ksDomScheduleIdx s' \<and> ksDomSchedule s'' = ksDomSchedule s' \<and> ksCurDomain s'' = ksCurDomain s' \<and> ksDomainTime s'' = ksDomainTime s' proof (prove)
goal (5 subgoals):
 1. (?x, s'') \<in> fst (updateMDB p f s')
 2. pspace_relations (ekheap s) (kheap s) (ksPSpace s')
 3. pspace_aligned' s'
 4. pspace_distinct' s'
 5. no_0 (ctes_of s') proof (prove)
using this:
(x, s'') \<in> fst (updateMDB p f s')
pspace_relations (ekheap sa) (kheap s) (ksPSpace s')
pspace_aligned' s'
pspace_distinct' s'
no_0 (ctes_of s')
ekheap s = ekheap sa

goal (5 subgoals):
 1. (?x, s'') \<in> fst (updateMDB p f s')
 2. pspace_relations (ekheap s) (kheap s) (ksPSpace s')
 3. pspace_aligned' s'
 4. pspace_distinct' s'
 5. no_0 (ctes_of s') proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma cte_map_inj_eq':
  "\<lbrakk>(cte_map p = cte_map p');
   cte_at p s \<and> cte_at p' s \<and>
   valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s\<rbrakk>
  \<Longrightarrow> p = p'" apply (rule cte_map_inj_eq; fastforce) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_map p = cte_map p'; cte_wp_at (\<lambda>_. True) p s \<and> cte_wp_at (\<lambda>_. True) p' s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s\<rbrakk> \<Longrightarrow> p = p' proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma revokable_relation_cap [simp]:
  "revokable_relation revo cs (modify_map m p (cteCap_update f)) =
  revokable_relation revo cs m" apply (rule iffI) apply (clarsimp simp add: revokable_relation_def) apply (erule allE, erule allE, erule impE, erule exI) apply (clarsimp simp: modify_map_def split: if_split_asm) apply (clarsimp simp add: revokable_relation_def modify_map_def) apply (erule allE, erule allE, erule impE, erule exI) apply (case_tac z) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. revokable_relation revo cs (modify_map m p (cteCap_update f)) = revokable_relation revo cs m proof (prove)
goal (2 subgoals):
 1. revokable_relation revo cs (modify_map m p (cteCap_update f)) \<Longrightarrow> revokable_relation revo cs m
 2. revokable_relation revo cs m \<Longrightarrow> revokable_relation revo cs (modify_map m p (cteCap_update f)) proof (prove)
goal (2 subgoals):
 1. \<And>a b y cap node. \<lbrakk>\<forall>a b. (\<exists>y. cs (a, b) = Some y) \<longrightarrow> (\<forall>cap node. modify_map m p (cteCap_update f) (cte_map (a, b)) = Some (CTE cap node) \<longrightarrow> revo (a, b) = mdbRevocable node); cs (a, b) = Some y; m (cte_map (a, b)) = Some (CTE cap node)\<rbrakk> \<Longrightarrow> revo (a, b) = mdbRevocable node
 2. revokable_relation revo cs m \<Longrightarrow> revokable_relation revo cs (modify_map m p (cteCap_update f)) proof (prove)
goal (2 subgoals):
 1. \<And>a b y cap node. \<lbrakk>cs (a, b) = Some y; m (cte_map (a, b)) = Some (CTE cap node); \<forall>cap node. modify_map m p (cteCap_update f) (cte_map (a, b)) = Some (CTE cap node) \<longrightarrow> revo (a, b) = mdbRevocable node\<rbrakk> \<Longrightarrow> revo (a, b) = mdbRevocable node
 2. revokable_relation revo cs m \<Longrightarrow> revokable_relation revo cs (modify_map m p (cteCap_update f)) proof (prove)
goal (1 subgoal):
 1. revokable_relation revo cs m \<Longrightarrow> revokable_relation revo cs (modify_map m p (cteCap_update f)) proof (prove)
goal (1 subgoal):
 1. \<And>a b y cap node z. \<lbrakk>\<forall>a b. (\<exists>y. cs (a, b) = Some y) \<longrightarrow> (\<forall>cap node. m (cte_map (a, b)) = Some (CTE cap node) \<longrightarrow> revo (a, b) = mdbRevocable node); p = cte_map (a, b); cs (a, b) = Some y; m (cte_map (a, b)) = Some z; cteCap_update f z = CTE cap node\<rbrakk> \<Longrightarrow> revo (a, b) = mdbRevocable node proof (prove)
goal (1 subgoal):
 1. \<And>a b y cap node z. \<lbrakk>p = cte_map (a, b); cs (a, b) = Some y; m (cte_map (a, b)) = Some z; cteCap_update f z = CTE cap node; \<forall>cap node. m (cte_map (a, b)) = Some (CTE cap node) \<longrightarrow> revo (a, b) = mdbRevocable node\<rbrakk> \<Longrightarrow> revo (a, b) = mdbRevocable node proof (prove)
goal (1 subgoal):
 1. \<And>a b y cap node z x1 x2. \<lbrakk>p = cte_map (a, b); cs (a, b) = Some y; m (cte_map (a, b)) = Some z; cteCap_update f z = CTE cap node; \<forall>cap node. m (cte_map (a, b)) = Some (CTE cap node) \<longrightarrow> revo (a, b) = mdbRevocable node; z = CTE x1 x2\<rbrakk> \<Longrightarrow> revo (a, b) = mdbRevocable node proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma mdb_cap_update:
  "cteMDBNode_update f (cteCap_update f' x) =
   cteCap_update f' (cteMDBNode_update f x)" by (cases x) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cteMDBNode_update f (cteCap_update f' x) = cteCap_update f' (cteMDBNode_update f x)
theory CSpace1_R

lemma prev_leadstoI:
  "\<lbrakk> m p = Some (CTE cap node); mdbPrev node \<noteq> 0; valid_dlist m\<rbrakk>
  \<Longrightarrow> m \<turnstile> mdbPrev node \<leadsto> p" by (fastforce simp add: valid_dlist_def Let_def next_unfold')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some (CTE cap node); mdbPrev node \<noteq> 0; valid_dlist m\<rbrakk> \<Longrightarrow> m \<turnstile> mdbPrev node \<leadsto> p
theory CSpace1_R

lemma mdb_next_modify_prev:
  "modify_map m x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<leadsto> b = m \<turnstile> a \<leadsto> b" by (auto simp add: next_unfold' modify_map_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. modify_map m x (cteMDBNode_update (mdbPrev_update f)) \<turnstile> a \<leadsto> b = m \<turnstile> a \<leadsto> b
theory CSpace1_R

lemma mdb_next_modify_revocable:
  "modify_map m x (cteMDBNode_update (mdbRevocable_update f)) \<turnstile> a \<leadsto> b = m \<turnstile> a \<leadsto> b" by (auto simp add: next_unfold' modify_map_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. modify_map m x (cteMDBNode_update (mdbRevocable_update f)) \<turnstile> a \<leadsto> b = m \<turnstile> a \<leadsto> b
theory CSpace1_R

lemma mdb_next_modify_cap:
  "modify_map m x (cteCap_update f) \<turnstile> a \<leadsto> b = m \<turnstile> a \<leadsto> b" by (auto simp add: next_unfold' modify_map_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. modify_map m x (cteCap_update f) \<turnstile> a \<leadsto> b = m \<turnstile> a \<leadsto> b
theory CSpace1_R

lemma in_getCTE:
  "(cte, s') \<in> fst (getCTE p s) \<Longrightarrow> s' = s \<and> cte_wp_at' ((=) cte) p s" apply (frule in_inv_by_hoareD [OF getCTE_inv]) apply (drule use_valid [OF _ getCTE_cte_wp_at], rule TrueI) apply (simp add: cte_wp_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (cte, s') \<in> fst (getCTE p s) \<Longrightarrow> s' = s \<and> cte_wp_at' ((=) cte) p s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(cte, s') \<in> fst (getCTE p s); s' = s\<rbrakk> \<Longrightarrow> s' = s \<and> cte_wp_at' ((=) cte) p s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' = s; cte_wp_at' (\<lambda>c. c = cte) p s'\<rbrakk> \<Longrightarrow> s' = s \<and> cte_wp_at' ((=) cte) p s proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma isMDBParentOf_eq_parent:
  "\<lbrakk> isMDBParentOf c cte;
     weak_derived' (cteCap c) (cteCap c');
     mdbRevocable (cteMDBNode c') = mdbRevocable (cteMDBNode c) \<rbrakk>
  \<Longrightarrow> isMDBParentOf c' cte" apply (cases c) apply (cases c') apply (cases cte) apply clarsimp apply (clarsimp simp: weak_derived'_def isMDBParentOf_CTE) apply (clarsimp simp: sameRegionAs_def2 isCap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isMDBParentOf c cte; weak_derived' (cteCap c) (cteCap c'); mdbRevocable (cteMDBNode c') = mdbRevocable (cteMDBNode c)\<rbrakk> \<Longrightarrow> isMDBParentOf c' cte proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>isMDBParentOf c cte; weak_derived' (cteCap c) (cteCap c'); mdbRevocable (cteMDBNode c') = mdbRevocable (cteMDBNode c); c = CTE x1 x2\<rbrakk> \<Longrightarrow> isMDBParentOf c' cte proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a. \<lbrakk>isMDBParentOf c cte; weak_derived' (cteCap c) (cteCap c'); mdbRevocable (cteMDBNode c') = mdbRevocable (cteMDBNode c); c = CTE x1 x2; c' = CTE x1a x2a\<rbrakk> \<Longrightarrow> isMDBParentOf c' cte proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a x1b x2b. \<lbrakk>isMDBParentOf c cte; weak_derived' (cteCap c) (cteCap c'); mdbRevocable (cteMDBNode c') = mdbRevocable (cteMDBNode c); c = CTE x1 x2; c' = CTE x1a x2a; cte = CTE x1b x2b\<rbrakk> \<Longrightarrow> isMDBParentOf c' cte proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a x1b x2b. \<lbrakk>isMDBParentOf (CTE x1 x2) (CTE x1b x2b); weak_derived' x1 x1a; mdbRevocable x2a = mdbRevocable x2; c = CTE x1 x2; c' = CTE x1a x2a; cte = CTE x1b x2b\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE x1a x2a) (CTE x1b x2b) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a x1b x2b. \<lbrakk>mdbRevocable x2a; c = CTE x1 x2; c' = CTE x1a x2a; cte = CTE x1b x2b; global.sameRegionAs x1 x1b; capMasterCap x1 = capMasterCap x1a; mdbRevocable x2; (capBadge x1a, capBadge x1b) \<in> capBadge_ordering (mdbFirstBadged x2b); capBadge x1 = capBadge x1a; capASID x1 = capASID x1a; cap_asid_base' x1 = cap_asid_base' x1a; cap_vptr' x1 = cap_vptr' x1a; isReplyCap x1 \<longrightarrow> capTCBPtr x1 = capTCBPtr x1a \<and> capReplyMaster x1 = capReplyMaster x1a\<rbrakk> \<Longrightarrow> global.sameRegionAs x1a x1b proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma isMDBParentOf_eq_child:
  "\<lbrakk> isMDBParentOf cte c;
     weak_derived' (cteCap c) (cteCap c');
     mdbFirstBadged (cteMDBNode c') = mdbFirstBadged (cteMDBNode c) \<rbrakk>
  \<Longrightarrow> isMDBParentOf cte c'" apply (cases c) apply (cases c') apply (cases cte) apply clarsimp apply (clarsimp simp: weak_derived'_def isMDBParentOf_CTE) apply (clarsimp simp: sameRegionAs_def2 isCap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isMDBParentOf cte c; weak_derived' (cteCap c) (cteCap c'); mdbFirstBadged (cteMDBNode c') = mdbFirstBadged (cteMDBNode c)\<rbrakk> \<Longrightarrow> isMDBParentOf cte c' proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>isMDBParentOf cte c; weak_derived' (cteCap c) (cteCap c'); mdbFirstBadged (cteMDBNode c') = mdbFirstBadged (cteMDBNode c); c = CTE x1 x2\<rbrakk> \<Longrightarrow> isMDBParentOf cte c' proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a. \<lbrakk>isMDBParentOf cte c; weak_derived' (cteCap c) (cteCap c'); mdbFirstBadged (cteMDBNode c') = mdbFirstBadged (cteMDBNode c); c = CTE x1 x2; c' = CTE x1a x2a\<rbrakk> \<Longrightarrow> isMDBParentOf cte c' proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a x1b x2b. \<lbrakk>isMDBParentOf cte c; weak_derived' (cteCap c) (cteCap c'); mdbFirstBadged (cteMDBNode c') = mdbFirstBadged (cteMDBNode c); c = CTE x1 x2; c' = CTE x1a x2a; cte = CTE x1b x2b\<rbrakk> \<Longrightarrow> isMDBParentOf cte c' proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a x1b x2b. \<lbrakk>isMDBParentOf (CTE x1b x2b) (CTE x1 x2); weak_derived' x1 x1a; mdbFirstBadged x2a = mdbFirstBadged x2; c = CTE x1 x2; c' = CTE x1a x2a; cte = CTE x1b x2b\<rbrakk> \<Longrightarrow> isMDBParentOf (CTE x1b x2b) (CTE x1a x2a) proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a x1b x2b. \<lbrakk>mdbFirstBadged x2a = mdbFirstBadged x2; c = CTE x1 x2; c' = CTE x1a x2a; cte = CTE x1b x2b; global.sameRegionAs x1b x1; capMasterCap x1 = capMasterCap x1a; mdbRevocable x2b; (capBadge x1b, capBadge x1a) \<in> capBadge_ordering (mdbFirstBadged x2); capBadge x1 = capBadge x1a; capASID x1 = capASID x1a; cap_asid_base' x1 = cap_asid_base' x1a; cap_vptr' x1 = cap_vptr' x1a; isReplyCap x1 \<longrightarrow> capTCBPtr x1 = capTCBPtr x1a \<and> capReplyMaster x1 = capReplyMaster x1a\<rbrakk> \<Longrightarrow> global.sameRegionAs x1b x1a proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma isMDBParentOf_eq:
  "\<lbrakk> isMDBParentOf c d;
     weak_derived' (cteCap c) (cteCap c');
     mdbRevocable (cteMDBNode c') = mdbRevocable (cteMDBNode c);
     weak_derived' (cteCap d) (cteCap d');
     mdbFirstBadged (cteMDBNode d') = mdbFirstBadged (cteMDBNode d) \<rbrakk>
  \<Longrightarrow> isMDBParentOf c' d'" apply (drule (2) isMDBParentOf_eq_parent) apply (erule (2) isMDBParentOf_eq_child) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isMDBParentOf c d; weak_derived' (cteCap c) (cteCap c'); mdbRevocable (cteMDBNode c') = mdbRevocable (cteMDBNode c); weak_derived' (cteCap d) (cteCap d'); mdbFirstBadged (cteMDBNode d') = mdbFirstBadged (cteMDBNode d)\<rbrakk> \<Longrightarrow> isMDBParentOf c' d' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>weak_derived' (cteCap c) (cteCap c'); mdbRevocable (cteMDBNode c') = mdbRevocable (cteMDBNode c); weak_derived' (cteCap d) (cteCap d'); mdbFirstBadged (cteMDBNode d') = mdbFirstBadged (cteMDBNode d); isMDBParentOf c' d\<rbrakk> \<Longrightarrow> isMDBParentOf c' d' proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma weak_derived_refl' [intro!, simp]:
  "weak_derived' c c" by (simp add: weak_derived'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. weak_derived' c c
theory CSpace1_R

lemma weak_derived_sym':
  "weak_derived' c d \<Longrightarrow> weak_derived' d c" by (clarsimp simp: weak_derived'_def isCap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. weak_derived' c d \<Longrightarrow> weak_derived' d c
theory CSpace1_R

lemma no_0_n' [intro!]: "no_0 n'" by (auto simp: n'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_0 n'
theory CSpace1_R

lemma src: "m src = Some (CTE src_cap src_node)" ..

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m src = Some (CTE src_cap src_node)
theory CSpace1_R

lemma dest: "m dest = Some (CTE dest_cap dest_node)" ..

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m dest = Some (CTE dest_cap dest_node)
theory CSpace1_R

lemma src_prev:
  "\<lbrakk> mdbPrev src_node = p; p \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cap node. m p = Some (CTE cap node) \<and> mdbNext node = src" using src apply - apply (erule dlistEp, simp) apply (case_tac cte') apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdbPrev src_node = p; p \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cap node. m p = Some (CTE cap node) \<and> mdbNext node = src proof (prove)
using this:
m src = Some (CTE src_cap src_node)

goal (1 subgoal):
 1. \<lbrakk>mdbPrev src_node = p; p \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cap node. m p = Some (CTE cap node) \<and> mdbNext node = src proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdbPrev src_node = p; p \<noteq> 0; m src = Some (CTE src_cap src_node)\<rbrakk> \<Longrightarrow> \<exists>cap node. m p = Some (CTE cap node) \<and> mdbNext node = src proof (prove)
goal (1 subgoal):
 1. \<And>cte'. \<lbrakk>mdbPrev src_node = p; p \<noteq> 0; m (mdbPrev (cteMDBNode (CTE src_cap src_node))) = Some cte'; mdbNext (cteMDBNode cte') = src\<rbrakk> \<Longrightarrow> \<exists>cap node. m p = Some (CTE cap node) \<and> mdbNext node = src proof (prove)
goal (1 subgoal):
 1. \<And>cte' x1 x2. \<lbrakk>mdbPrev src_node = p; p \<noteq> 0; m (mdbPrev (cteMDBNode (CTE src_cap src_node))) = Some cte'; mdbNext (cteMDBNode cte') = src; cte' = CTE x1 x2\<rbrakk> \<Longrightarrow> \<exists>cap node. m p = Some (CTE cap node) \<and> mdbNext node = src proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma src_next:
  "\<lbrakk> mdbNext src_node = p; p \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cap node. m p = Some (CTE cap node) \<and> mdbPrev node = src" using src apply - apply (erule dlistEn, simp) apply (case_tac cte') apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdbNext src_node = p; p \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cap node. m p = Some (CTE cap node) \<and> mdbPrev node = src proof (prove)
using this:
m src = Some (CTE src_cap src_node)

goal (1 subgoal):
 1. \<lbrakk>mdbNext src_node = p; p \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cap node. m p = Some (CTE cap node) \<and> mdbPrev node = src proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdbNext src_node = p; p \<noteq> 0; m src = Some (CTE src_cap src_node)\<rbrakk> \<Longrightarrow> \<exists>cap node. m p = Some (CTE cap node) \<and> mdbPrev node = src proof (prove)
goal (1 subgoal):
 1. \<And>cte'. \<lbrakk>mdbNext src_node = p; p \<noteq> 0; m (mdbNext (cteMDBNode (CTE src_cap src_node))) = Some cte'; mdbPrev (cteMDBNode cte') = src\<rbrakk> \<Longrightarrow> \<exists>cap node. m p = Some (CTE cap node) \<and> mdbPrev node = src proof (prove)
goal (1 subgoal):
 1. \<And>cte' x1 x2. \<lbrakk>mdbNext src_node = p; p \<noteq> 0; m (mdbNext (cteMDBNode (CTE src_cap src_node))) = Some cte'; mdbPrev (cteMDBNode cte') = src; cte' = CTE x1 x2\<rbrakk> \<Longrightarrow> \<exists>cap node. m p = Some (CTE cap node) \<and> mdbPrev node = src proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma dest_prev:
  "\<lbrakk> mdbPrev dest_node = p; p \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cap node. m p = Some (CTE cap node) \<and> mdbNext node = dest" using dest apply - apply (erule dlistEp, simp) apply (case_tac cte') apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdbPrev dest_node = p; p \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cap node. m p = Some (CTE cap node) \<and> mdbNext node = dest proof (prove)
using this:
m dest = Some (CTE dest_cap dest_node)

goal (1 subgoal):
 1. \<lbrakk>mdbPrev dest_node = p; p \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cap node. m p = Some (CTE cap node) \<and> mdbNext node = dest proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdbPrev dest_node = p; p \<noteq> 0; m dest = Some (CTE dest_cap dest_node)\<rbrakk> \<Longrightarrow> \<exists>cap node. m p = Some (CTE cap node) \<and> mdbNext node = dest proof (prove)
goal (1 subgoal):
 1. \<And>cte'. \<lbrakk>mdbPrev dest_node = p; p \<noteq> 0; m (mdbPrev (cteMDBNode (CTE dest_cap dest_node))) = Some cte'; mdbNext (cteMDBNode cte') = dest\<rbrakk> \<Longrightarrow> \<exists>cap node. m p = Some (CTE cap node) \<and> mdbNext node = dest proof (prove)
goal (1 subgoal):
 1. \<And>cte' x1 x2. \<lbrakk>mdbPrev dest_node = p; p \<noteq> 0; m (mdbPrev (cteMDBNode (CTE dest_cap dest_node))) = Some cte'; mdbNext (cteMDBNode cte') = dest; cte' = CTE x1 x2\<rbrakk> \<Longrightarrow> \<exists>cap node. m p = Some (CTE cap node) \<and> mdbNext node = dest proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma dest_next:
  "\<lbrakk> mdbNext dest_node = p; p \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cap node. m p = Some (CTE cap node) \<and> mdbPrev node = dest" using dest apply - apply (erule dlistEn, simp) apply (case_tac cte') apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdbNext dest_node = p; p \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cap node. m p = Some (CTE cap node) \<and> mdbPrev node = dest proof (prove)
using this:
m dest = Some (CTE dest_cap dest_node)

goal (1 subgoal):
 1. \<lbrakk>mdbNext dest_node = p; p \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cap node. m p = Some (CTE cap node) \<and> mdbPrev node = dest proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdbNext dest_node = p; p \<noteq> 0; m dest = Some (CTE dest_cap dest_node)\<rbrakk> \<Longrightarrow> \<exists>cap node. m p = Some (CTE cap node) \<and> mdbPrev node = dest proof (prove)
goal (1 subgoal):
 1. \<And>cte'. \<lbrakk>mdbNext dest_node = p; p \<noteq> 0; m (mdbNext (cteMDBNode (CTE dest_cap dest_node))) = Some cte'; mdbPrev (cteMDBNode cte') = dest\<rbrakk> \<Longrightarrow> \<exists>cap node. m p = Some (CTE cap node) \<and> mdbPrev node = dest proof (prove)
goal (1 subgoal):
 1. \<And>cte' x1 x2. \<lbrakk>mdbNext dest_node = p; p \<noteq> 0; m (mdbNext (cteMDBNode (CTE dest_cap dest_node))) = Some cte'; mdbPrev (cteMDBNode cte') = dest; cte' = CTE x1 x2\<rbrakk> \<Longrightarrow> \<exists>cap node. m p = Some (CTE cap node) \<and> mdbPrev node = dest proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma next_dest_prev_src [simp]:
  "(mdbNext dest_node = src) = (mdbPrev src_node = dest)" apply (rule iffI) apply (drule dest_next, simp) apply (clarsimp simp: src) apply (drule src_prev, simp) apply (clarsimp simp: dest) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (mdbNext dest_node = src) = (mdbPrev src_node = dest) proof (prove)
goal (2 subgoals):
 1. mdbNext dest_node = src \<Longrightarrow> mdbPrev src_node = dest
 2. mdbPrev src_node = dest \<Longrightarrow> mdbNext dest_node = src proof (prove)
goal (2 subgoals):
 1. \<exists>cap node. m src = Some (CTE cap node) \<and> mdbPrev node = dest \<Longrightarrow> mdbPrev src_node = dest
 2. mdbPrev src_node = dest \<Longrightarrow> mdbNext dest_node = src proof (prove)
goal (1 subgoal):
 1. mdbPrev src_node = dest \<Longrightarrow> mdbNext dest_node = src proof (prove)
goal (1 subgoal):
 1. \<exists>cap node. m dest = Some (CTE cap node) \<and> mdbNext node = src \<Longrightarrow> mdbNext dest_node = src proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma prev_dest_next_src [simp]:
  "(mdbPrev dest_node = src) = (mdbNext src_node = dest)" apply (rule iffI) apply (drule dest_prev, simp) apply (clarsimp simp: src) apply (drule src_next, simp) apply (clarsimp simp: dest) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (mdbPrev dest_node = src) = (mdbNext src_node = dest) proof (prove)
goal (2 subgoals):
 1. mdbPrev dest_node = src \<Longrightarrow> mdbNext src_node = dest
 2. mdbNext src_node = dest \<Longrightarrow> mdbPrev dest_node = src proof (prove)
goal (2 subgoals):
 1. \<exists>cap node. m src = Some (CTE cap node) \<and> mdbNext node = dest \<Longrightarrow> mdbNext src_node = dest
 2. mdbNext src_node = dest \<Longrightarrow> mdbPrev dest_node = src proof (prove)
goal (1 subgoal):
 1. mdbNext src_node = dest \<Longrightarrow> mdbPrev dest_node = src proof (prove)
goal (1 subgoal):
 1. \<exists>cap node. m dest = Some (CTE cap node) \<and> mdbPrev node = src \<Longrightarrow> mdbPrev dest_node = src proof (prove)
goal:
No subgoals!