kings-crown/FVELER_Isabelle huggingface dataset:
theory CSpace_R

lemma src_node_revokable [simp]:
  "mdbRevocable src_node" using safe_parent ut_rev src apply (clarsimp simp add: safe_parent_for'_def) apply (erule disjE) apply clarsimp apply (erule irq_revocable, rule irq_control) apply (clarsimp simp: ut_revocable'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdbRevocable src_node proof (prove)
using this:
safe_parent_for' m src c'
ut_revocable' m
m src = Some (CTE src_cap src_node)

goal (1 subgoal):
 1. mdbRevocable src_node proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ut_revocable' m; m src = Some (CTE src_cap src_node); global.sameRegionAs src_cap c'; (\<exists>irq. c' = capability.IRQHandlerCap irq) \<and> src_cap = capability.IRQControlCap \<and> (\<forall>p n'. m p \<noteq> Some (CTE c' n')) \<or> isUntypedCap src_cap \<and> descendants_of' src m = {} \<and> capRange c' \<noteq> {} \<and> capBits c' \<le> capBits src_cap\<rbrakk> \<Longrightarrow> mdbRevocable src_node proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ut_revocable' m; m src = Some (CTE src_cap src_node); global.sameRegionAs src_cap c'; (\<exists>irq. c' = capability.IRQHandlerCap irq) \<and> src_cap = capability.IRQControlCap \<and> (\<forall>p n'. m p \<noteq> Some (CTE c' n'))\<rbrakk> \<Longrightarrow> mdbRevocable src_node
 2. \<lbrakk>ut_revocable' m; m src = Some (CTE src_cap src_node); global.sameRegionAs src_cap c'; isUntypedCap src_cap \<and> descendants_of' src m = {} \<and> capRange c' \<noteq> {} \<and> capBits c' \<le> capBits src_cap\<rbrakk> \<Longrightarrow> mdbRevocable src_node proof (prove)
goal (2 subgoals):
 1. \<And>irq. \<lbrakk>ut_revocable' m; m src = Some (CTE capability.IRQControlCap src_node); global.sameRegionAs capability.IRQControlCap (capability.IRQHandlerCap irq); c' = capability.IRQHandlerCap irq; src_cap = capability.IRQControlCap; \<forall>p n'. m p \<noteq> Some (CTE (capability.IRQHandlerCap irq) n')\<rbrakk> \<Longrightarrow> mdbRevocable src_node
 2. \<lbrakk>ut_revocable' m; m src = Some (CTE src_cap src_node); global.sameRegionAs src_cap c'; isUntypedCap src_cap \<and> descendants_of' src m = {} \<and> capRange c' \<noteq> {} \<and> capBits c' \<le> capBits src_cap\<rbrakk> \<Longrightarrow> mdbRevocable src_node proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ut_revocable' m; m src = Some (CTE src_cap src_node); global.sameRegionAs src_cap c'; isUntypedCap src_cap \<and> descendants_of' src m = {} \<and> capRange c' \<noteq> {} \<and> capBits c' \<le> capBits src_cap\<rbrakk> \<Longrightarrow> mdbRevocable src_node proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma new_child [simp]:
  "isMDBParentOf new_src new_dest" using safe_parent ut_rev src apply (simp add: new_src_def new_dest_def isMDBParentOf_def) apply (clarsimp simp: safe_parent_for'_def) apply (auto simp: isCap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isMDBParentOf new_src new_dest proof (prove)
using this:
safe_parent_for' m src c'
ut_revocable' m
m src = Some (CTE src_cap src_node)

goal (1 subgoal):
 1. isMDBParentOf new_src new_dest proof (prove)
goal (1 subgoal):
 1. \<lbrakk>safe_parent_for' m src c'; ut_revocable' m; m src = Some (CTE src_cap src_node)\<rbrakk> \<Longrightarrow> (isNotificationCap src_cap \<and> capNtfnBadge src_cap \<noteq> 0 \<longrightarrow> (isEndpointCap src_cap \<and> capEPBadge src_cap \<noteq> 0 \<longrightarrow> global.sameRegionAs src_cap c' \<and> (global.sameRegionAs src_cap c' \<longrightarrow> capEPBadge src_cap = capEPBadge c' \<and> \<not> revokable' src_cap c')) \<and> ((isEndpointCap src_cap \<longrightarrow> capEPBadge src_cap = 0) \<longrightarrow> global.sameRegionAs src_cap c' \<and> (global.sameRegionAs src_cap c' \<longrightarrow> capNtfnBadge src_cap = capNtfnBadge c' \<and> \<not> revokable' src_cap c'))) \<and> ((isNotificationCap src_cap \<longrightarrow> capNtfnBadge src_cap = 0) \<longrightarrow> (isEndpointCap src_cap \<and> capEPBadge src_cap \<noteq> 0 \<longrightarrow> global.sameRegionAs src_cap c' \<and> (global.sameRegionAs src_cap c' \<longrightarrow> capEPBadge src_cap = capEPBadge c' \<and> \<not> revokable' src_cap c')) \<and> ((isEndpointCap src_cap \<longrightarrow> capEPBadge src_cap = 0) \<longrightarrow> global.sameRegionAs src_cap c')) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ut_revocable' m; m src = Some (CTE src_cap src_node); global.sameRegionAs src_cap c'; (\<exists>irq. c' = capability.IRQHandlerCap irq) \<and> src_cap = capability.IRQControlCap \<and> (\<forall>p n'. m p \<noteq> Some (CTE c' n')) \<or> isUntypedCap src_cap \<and> descendants_of' src m = {} \<and> capRange c' \<noteq> {} \<and> capBits c' \<le> capBits src_cap\<rbrakk> \<Longrightarrow> (isNotificationCap src_cap \<and> capNtfnBadge src_cap \<noteq> 0 \<longrightarrow> (isEndpointCap src_cap \<and> capEPBadge src_cap \<noteq> 0 \<longrightarrow> capEPBadge src_cap = capEPBadge c' \<and> \<not> revokable' src_cap c') \<and> ((isEndpointCap src_cap \<longrightarrow> capEPBadge src_cap = 0) \<longrightarrow> capNtfnBadge src_cap = capNtfnBadge c' \<and> \<not> revokable' src_cap c')) \<and> ((isNotificationCap src_cap \<longrightarrow> capNtfnBadge src_cap = 0) \<longrightarrow> isEndpointCap src_cap \<and> capEPBadge src_cap \<noteq> 0 \<longrightarrow> capEPBadge src_cap = capEPBadge c' \<and> \<not> revokable' src_cap c') proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma n_dest_child:
  "n \<turnstile> src \<rightarrow> dest" apply (rule subtree.direct_parent) apply (simp add: n_direct_eq) apply simp apply (clarsimp simp: parentOf_def src dest n) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<turnstile> src \<rightarrow> dest proof (prove)
goal (3 subgoals):
 1. n \<turnstile> src \<leadsto> dest
 2. dest \<noteq> 0
 3. n \<turnstile> src parentOf dest proof (prove)
goal (2 subgoals):
 1. dest \<noteq> 0
 2. n \<turnstile> src parentOf dest proof (prove)
goal (1 subgoal):
 1. n \<turnstile> src parentOf dest proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma n_to_dest [simp]:
  "n \<turnstile> p \<leadsto> dest = (p = src)" by (simp add: n_direct_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<turnstile> p \<leadsto> dest = (p = src)
theory CSpace_R

lemma descendants:
  "descendants_of' p n =
   (if src \<in> descendants_of' p m \<or> p = src
   then descendants_of' p m \<union> {dest} else descendants_of' p m)" apply (rule set_eqI) apply (simp add: descendants_of'_def) apply (fastforce dest!: parent_n_m dest: parent_m_n simp: n_dest_child split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. descendants_of' p n = (if src \<in> descendants_of' p m \<or> p = src then descendants_of' p m \<union> {dest} else descendants_of' p m) proof (prove)
goal (1 subgoal):
 1. \<And>x. (x \<in> descendants_of' p n) = (x \<in> (if src \<in> descendants_of' p m \<or> p = src then descendants_of' p m \<union> {dest} else descendants_of' p m)) proof (prove)
goal (1 subgoal):
 1. \<And>x. (m \<turnstile> p \<rightarrow> src \<longrightarrow> n \<turnstile> p \<rightarrow> x = (x = dest \<or> m \<turnstile> p \<rightarrow> x)) \<and> (p = src \<longrightarrow> n \<turnstile> src \<rightarrow> x = (x = dest \<or> m \<turnstile> src \<rightarrow> x)) \<and> (\<not> m \<turnstile> p \<rightarrow> src \<and> p \<noteq> src \<longrightarrow> n \<turnstile> p \<rightarrow> x = m \<turnstile> p \<rightarrow> x) proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma sameRegion_capRange_sub:
  "sameRegionAs cap cap' \<Longrightarrow> capRange cap' \<subseteq> capRange cap" apply (clarsimp simp: sameRegionAs_def2 isCap_Master capRange_Master) apply (erule disjE) apply (clarsimp dest!: capMaster_capRange) apply (erule disjE) apply fastforce apply (clarsimp simp: isCap_simps capRange_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. global.sameRegionAs cap cap' \<Longrightarrow> capRange cap' \<subseteq> capRange cap proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>capMasterCap cap = capMasterCap cap' \<and> capMasterCap cap \<noteq> capability.NullCap \<and> \<not> isZombie cap \<and> \<not> isUntypedCap cap \<and> \<not> isArchPageCap cap \<and> capMasterCap cap' \<noteq> capability.NullCap \<and> \<not> isZombie cap' \<and> \<not> isUntypedCap cap' \<and> \<not> isArchPageCap cap' \<or> capRange cap' \<noteq> {} \<and> capRange cap' \<subseteq> capRange cap \<and> (isUntypedCap cap \<or> isArchPageCap cap \<and> isArchPageCap cap') \<or> isIRQControlCap cap \<and> isIRQHandlerCap cap'; x \<in> capRange cap'\<rbrakk> \<Longrightarrow> x \<in> capRange cap proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x \<in> capRange cap'; capMasterCap cap = capMasterCap cap' \<and> capMasterCap cap \<noteq> capability.NullCap \<and> \<not> isZombie cap \<and> \<not> isUntypedCap cap \<and> \<not> isArchPageCap cap \<and> capMasterCap cap' \<noteq> capability.NullCap \<and> \<not> isZombie cap' \<and> \<not> isUntypedCap cap' \<and> \<not> isArchPageCap cap'\<rbrakk> \<Longrightarrow> x \<in> capRange cap
 2. \<And>x. \<lbrakk>x \<in> capRange cap'; capRange cap' \<noteq> {} \<and> capRange cap' \<subseteq> capRange cap \<and> (isUntypedCap cap \<or> isArchPageCap cap \<and> isArchPageCap cap') \<or> isIRQControlCap cap \<and> isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> x \<in> capRange cap proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> capRange cap'; capRange cap' \<noteq> {} \<and> capRange cap' \<subseteq> capRange cap \<and> (isUntypedCap cap \<or> isArchPageCap cap \<and> isArchPageCap cap') \<or> isIRQControlCap cap \<and> isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> x \<in> capRange cap proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x \<in> capRange cap'; capRange cap' \<noteq> {} \<and> capRange cap' \<subseteq> capRange cap \<and> (isUntypedCap cap \<or> isArchPageCap cap \<and> isArchPageCap cap')\<rbrakk> \<Longrightarrow> x \<in> capRange cap
 2. \<And>x. \<lbrakk>x \<in> capRange cap'; isIRQControlCap cap \<and> isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> x \<in> capRange cap proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> capRange cap'; isIRQControlCap cap \<and> isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> x \<in> capRange cap proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma safe_parent_for_capRange_capBits:
  "\<lbrakk> safe_parent_for' m p cap; m p = Some cte \<rbrakk> \<Longrightarrow> capRange cap \<subseteq> capRange (cteCap cte)
    \<and> capBits cap \<le> capBits (cteCap cte)" apply (clarsimp simp: safe_parent_for'_def) apply (erule disjE) apply (clarsimp simp: capRange_def) by (auto simp: sameRegionAs_def2 isCap_simps capRange_def
                    capMasterCap_def capRange_Master objBits_simps
         split:capability.splits arch_capability.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>safe_parent_for' m p cap; m p = Some cte\<rbrakk> \<Longrightarrow> capRange cap \<subseteq> capRange (cteCap cte) \<and> capBits cap \<le> capBits (cteCap cte) proof (prove)
goal (1 subgoal):
 1. \<And>parent node. \<lbrakk>m p = Some (CTE parent node); cte = CTE parent node; global.sameRegionAs parent cap; (\<exists>irq. cap = capability.IRQHandlerCap irq) \<and> parent = capability.IRQControlCap \<and> (\<forall>p n'. m p \<noteq> Some (CTE cap n')) \<or> isUntypedCap parent \<and> descendants_of' p m = {} \<and> capRange cap \<noteq> {} \<and> capBits cap \<le> capBits parent\<rbrakk> \<Longrightarrow> capRange cap \<subseteq> capRange parent \<and> capBits cap \<le> capBits parent proof (prove)
goal (2 subgoals):
 1. \<And>parent node. \<lbrakk>m p = Some (CTE parent node); cte = CTE parent node; global.sameRegionAs parent cap; (\<exists>irq. cap = capability.IRQHandlerCap irq) \<and> parent = capability.IRQControlCap \<and> (\<forall>p n'. m p \<noteq> Some (CTE cap n'))\<rbrakk> \<Longrightarrow> capRange cap \<subseteq> capRange parent \<and> capBits cap \<le> capBits parent
 2. \<And>parent node. \<lbrakk>m p = Some (CTE parent node); cte = CTE parent node; global.sameRegionAs parent cap; isUntypedCap parent \<and> descendants_of' p m = {} \<and> capRange cap \<noteq> {} \<and> capBits cap \<le> capBits parent\<rbrakk> \<Longrightarrow> capRange cap \<subseteq> capRange parent \<and> capBits cap \<le> capBits parent proof (prove)
goal (1 subgoal):
 1. \<And>parent node. \<lbrakk>m p = Some (CTE parent node); cte = CTE parent node; global.sameRegionAs parent cap; isUntypedCap parent \<and> descendants_of' p m = {} \<and> capRange cap \<noteq> {} \<and> capBits cap \<le> capBits parent\<rbrakk> \<Longrightarrow> capRange cap \<subseteq> capRange parent \<and> capBits cap \<le> capBits parent
theory CSpace_R

lemma safe_parent_Null:
  "\<lbrakk> m src = Some (CTE NullCap n); safe_parent_for' m src c' \<rbrakk> \<Longrightarrow> False" by (simp add: safe_parent_for'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some (CTE capability.NullCap n); safe_parent_for' m src c'\<rbrakk> \<Longrightarrow> False
theory CSpace_R

lemma notUntypedRange:
  "\<not>isUntypedCap cap \<Longrightarrow> untypedRange cap = {}" by (cases cap) (auto simp: isCap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> isUntypedCap cap \<Longrightarrow> untypedRange cap = {}
theory CSpace_R

lemma safe_parent_for_descendants':
  "\<lbrakk> safe_parent_for' m p cap; m p = Some (CTE pcap n); isUntypedCap pcap \<rbrakk> \<Longrightarrow> descendants_of' p m = {}" by (auto simp: safe_parent_for'_def isCap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>safe_parent_for' m p cap; m p = Some (CTE pcap n); isUntypedCap pcap\<rbrakk> \<Longrightarrow> descendants_of' p m = {}
theory CSpace_R

lemma safe_parent_not_ep':
  "\<lbrakk> safe_parent_for' m p cap; m p = Some (CTE src_cap n) \<rbrakk> \<Longrightarrow> \<not>isEndpointCap src_cap" by (auto simp: safe_parent_for'_def isCap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>safe_parent_for' m p cap; m p = Some (CTE src_cap n)\<rbrakk> \<Longrightarrow> \<not> isEndpointCap src_cap
theory CSpace_R

lemma safe_parent_not_ntfn':
  "\<lbrakk> safe_parent_for' m p cap; m p = Some (CTE src_cap n) \<rbrakk> \<Longrightarrow> \<not>isNotificationCap src_cap" by (auto simp: safe_parent_for'_def isCap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>safe_parent_for' m p cap; m p = Some (CTE src_cap n)\<rbrakk> \<Longrightarrow> \<not> isNotificationCap src_cap
theory CSpace_R

lemma safe_parent_capClass:
  "\<lbrakk> safe_parent_for' m p cap; m p = Some (CTE src_cap n) \<rbrakk> \<Longrightarrow> capClass cap = capClass src_cap" by (auto simp: safe_parent_for'_def isCap_simps sameRegionAs_def2 capRange_Master capRange_def
           capMasterCap_def
           split: capability.splits arch_capability.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>safe_parent_for' m p cap; m p = Some (CTE src_cap n)\<rbrakk> \<Longrightarrow> capClass cap = capClass src_cap
theory CSpace_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 CSpace_R

lemma chain_n': "mdb_chain_0 n'" unfolding n'_def by (rule mdb_chain_0_modify_map_prev) (rule chain_n)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdb_chain_0 n' proof (prove)
goal (1 subgoal):
 1. mdb_chain_0 (modify_map n (mdbNext src_node) (cteMDBNode_update (mdbPrev_update (\<lambda>_. dest))))
theory CSpace_R

lemma n_direct_eq':
  "n' \<turnstile> p \<leadsto> p' = (if p = src then p' = dest else
                 if p = dest then m \<turnstile> src \<leadsto> p'
                 else m \<turnstile> p \<leadsto> p')" by (simp add: n'_def mdb_next_modify n_direct_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n' \<turnstile> p \<leadsto> p' = (if p = src then p' = dest else if p = dest then m \<turnstile> src \<leadsto> p' else m \<turnstile> p \<leadsto> p')
theory CSpace_R

lemma dest_no_next_p:
  "m p = Some cte \<Longrightarrow> mdbNext (cteMDBNode cte) \<noteq> dest" using dest dest_prev apply (cases cte) apply (rule notI) apply (rule dlistEn, assumption) apply clarsimp apply clarsimp done

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

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

lemma dest_no_src_next [iff]:
  "mdbNext src_node \<noteq> dest" using src by (clarsimp dest!: dest_no_next_p)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdbNext src_node \<noteq> dest proof (prove)
using this:
m src = Some (CTE src_cap src_node)

goal (1 subgoal):
 1. mdbNext src_node \<noteq> dest
theory CSpace_R

lemma n_dest':
  "n' dest = Some new_dest" by (simp add: n'_def n modify_map_if new_dest_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n' dest = Some new_dest
theory CSpace_R

lemma n'_trancl_eq:
  "n' \<turnstile> p \<leadsto>\<^sup>+ p' =
  (if p' = dest then p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src
   else if p = dest then m \<turnstile> src \<leadsto>\<^sup>+ p'
   else m \<turnstile> p \<leadsto>\<^sup>+ p')" unfolding n'_def trancl_prev_update by (simp add: n_trancl_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n' \<turnstile> p \<leadsto>\<^sup>+ p' = (if p' = dest then p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src else if p = dest then m \<turnstile> src \<leadsto>\<^sup>+ p' else m \<turnstile> p \<leadsto>\<^sup>+ p') proof (prove)
goal (1 subgoal):
 1. n \<turnstile> p \<leadsto>\<^sup>+ p' = (if p' = dest then p = src \<or> m \<turnstile> p \<leadsto>\<^sup>+ src else if p = dest then m \<turnstile> src \<leadsto>\<^sup>+ p' else m \<turnstile> p \<leadsto>\<^sup>+ p')
theory CSpace_R

lemma n_rtrancl_eq':
  "n' \<turnstile> p \<leadsto>\<^sup>* p' =
  (if p' = dest then p = dest \<or> p \<noteq> dest \<and> m \<turnstile> p \<leadsto>\<^sup>* src
   else if p = dest then p' \<noteq> src \<and> m \<turnstile> src \<leadsto>\<^sup>* p'
   else m \<turnstile> p \<leadsto>\<^sup>* p')" unfolding n'_def rtrancl_prev_update by (simp add: n_rtrancl_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n' \<turnstile> p \<leadsto>\<^sup>* p' = (if p' = dest then p = dest \<or> p \<noteq> dest \<and> m \<turnstile> p \<leadsto>\<^sup>* src else if p = dest then p' \<noteq> src \<and> m \<turnstile> src \<leadsto>\<^sup>* p' else m \<turnstile> p \<leadsto>\<^sup>* p') proof (prove)
goal (1 subgoal):
 1. n \<turnstile> p \<leadsto>\<^sup>* p' = (if p' = dest then p = dest \<or> p \<noteq> dest \<and> m \<turnstile> p \<leadsto>\<^sup>* src else if p = dest then p' \<noteq> src \<and> m \<turnstile> src \<leadsto>\<^sup>* p' else m \<turnstile> p \<leadsto>\<^sup>* p')
theory CSpace_R

lemma n'_cap:
  "n' p = Some (CTE cap node) \<Longrightarrow>
  \<exists>node'. if p = dest then cap = c' \<and> m p = Some (CTE dest_cap node')
          else m p = Some (CTE cap node')" by (auto simp add: n'_def n src dest new_src_def new_dest_def modify_map_if split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n' p = Some (CTE cap node) \<Longrightarrow> \<exists>node'. if p = dest then cap = c' \<and> m p = Some (CTE dest_cap node') else m p = Some (CTE cap node')
theory CSpace_R

lemma n'_rev:
  "n' p = Some (CTE cap node) \<Longrightarrow>
  \<exists>node'. if p = dest then mdbRevocable node = revokable' src_cap c' \<and> m p = Some (CTE dest_cap node')
          else m p = Some (CTE cap node') \<and> mdbRevocable node = mdbRevocable node'" by (auto simp add: n'_def n src dest new_src_def new_dest_def modify_map_if split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n' p = Some (CTE cap node) \<Longrightarrow> \<exists>node'. if p = dest then mdbRevocable node = revokable' src_cap c' \<and> m p = Some (CTE dest_cap node') else m p = Some (CTE cap node') \<and> mdbRevocable node = mdbRevocable node'