kings-crown/FVELER_Isabelle huggingface dataset:
theory CSpace1_R

lemma cte_map_inj_ps:
  assumes "p \<noteq> p'"
  assumes "cte_at p s"
  assumes "cte_at p' s"
  assumes "valid_pspace s"
  shows "cte_map p \<noteq> cte_map p'" using assms apply - apply (rule cte_map_inj) apply (auto simp: valid_pspace_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_map p \<noteq> cte_map p' proof (prove)
using this:
p \<noteq> p'
cte_wp_at (\<lambda>_. True) p s
cte_wp_at (\<lambda>_. True) p' s
valid_pspace s

goal (1 subgoal):
 1. cte_map p \<noteq> cte_map p' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<noteq> p'; cte_wp_at (\<lambda>_. True) p s; cte_wp_at (\<lambda>_. True) p' s; valid_pspace s\<rbrakk> \<Longrightarrow> cte_map p \<noteq> cte_map p' proof (prove)
goal (6 subgoals):
 1. \<lbrakk>p \<noteq> p'; cte_wp_at (\<lambda>_. True) p s; cte_wp_at (\<lambda>_. True) p' s; valid_pspace s\<rbrakk> \<Longrightarrow> p \<noteq> p'
 2. \<lbrakk>p \<noteq> p'; cte_wp_at (\<lambda>_. True) p s; cte_wp_at (\<lambda>_. True) p' s; valid_pspace s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p ?s4
 3. \<lbrakk>p \<noteq> p'; cte_wp_at (\<lambda>_. True) p s; cte_wp_at (\<lambda>_. True) p' s; valid_pspace s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) p' ?s4
 4. \<lbrakk>p \<noteq> p'; cte_wp_at (\<lambda>_. True) p s; cte_wp_at (\<lambda>_. True) p' s; valid_pspace s\<rbrakk> \<Longrightarrow> valid_objs ?s4
 5. \<lbrakk>p \<noteq> p'; cte_wp_at (\<lambda>_. True) p s; cte_wp_at (\<lambda>_. True) p' s; valid_pspace s\<rbrakk> \<Longrightarrow> pspace_aligned ?s4
 6. \<lbrakk>p \<noteq> p'; cte_wp_at (\<lambda>_. True) p s; cte_wp_at (\<lambda>_. True) p' s; valid_pspace s\<rbrakk> \<Longrightarrow> pspace_distinct ?s4 proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma cte_map_inj_eq:
  "\<lbrakk>cte_map p = cte_map p';
   cte_at p s; cte_at p' s;
   valid_objs s; pspace_aligned s; pspace_distinct s\<rbrakk>
  \<Longrightarrow> p = p'" apply (rule classical) apply (drule (5) cte_map_inj) apply simp done

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

lemma tcb_cases_related2:
  "tcb_cte_cases (v - x) = Some (getF, setF) \<Longrightarrow>
   \<exists>getF' setF' restr. tcb_cap_cases (tcb_cnode_index (unat ((v - x) >> cte_level_bits))) = Some (getF', setF', restr)
          \<and> cte_map (x, tcb_cnode_index (unat ((v - x) >> cte_level_bits))) = v
          \<and> (\<forall>tcb tcb'. tcb_relation tcb tcb' \<longrightarrow> cap_relation (getF' tcb) (cteCap (getF tcb')))
          \<and> (\<forall>tcb tcb' cap cte. tcb_relation tcb tcb' \<longrightarrow> cap_relation cap (cteCap cte)
                        \<longrightarrow> tcb_relation (setF' (\<lambda>x. cap) tcb) (setF (\<lambda>x. cte) tcb'))" apply (clarsimp simp: tcb_cte_cases_def tcb_relation_def cte_level_bits_def
                        tcb_cap_cases_simps[simplified]
                 split: if_split_asm) apply (simp_all add: tcb_cnode_index_def cte_level_bits_def cte_map_def field_simps to_bl_1) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_cte_cases (v - x) = Some (getF, setF) \<Longrightarrow> \<exists>getF' setF' restr. tcb_cap_cases (tcb_cnode_index (unat (v - x >> cte_level_bits))) = Some (getF', setF', restr) \<and> cte_map (x, tcb_cnode_index (unat (v - x >> cte_level_bits))) = v \<and> (\<forall>tcb tcb'. tcb_relation tcb tcb' \<longrightarrow> cap_relation (getF' tcb) (cteCap (getF tcb'))) \<and> (\<forall>tcb tcb' cap cte. tcb_relation tcb tcb' \<longrightarrow> cap_relation cap (cteCap cte) \<longrightarrow> tcb_relation (setF' (\<lambda>x. cap) tcb) (setF (\<lambda>x. cte) tcb')) proof (prove)
goal (5 subgoals):
 1. \<lbrakk>v - x = 0x40; getF = tcbIPCBufferFrame; setF = tcbIPCBufferFrame_update\<rbrakk> \<Longrightarrow> cte_map (x, tcb_cnode_index 4) = v
 2. \<lbrakk>v - x = 0x30; getF = tcbCaller; setF = tcbCaller_update\<rbrakk> \<Longrightarrow> cte_map (x, tcb_cnode_index 3) = v
 3. \<lbrakk>v - x = 0x20; getF = tcbReply; setF = tcbReply_update\<rbrakk> \<Longrightarrow> cte_map (x, tcb_cnode_index 2) = v
 4. \<lbrakk>v - x = 0x10; getF = tcbVTable; setF = tcbVTable_update\<rbrakk> \<Longrightarrow> cte_map (x, tcb_cnode_index (Suc 0)) = v
 5. \<lbrakk>v = x; getF = tcbCTable; setF = tcbCTable_update\<rbrakk> \<Longrightarrow> cte_map (x, tcb_cnode_index 0) = x proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma other_obj_relation_KOCTE[simp]:
  "\<not> other_obj_relation ko (KOCTE cte)" by (simp add: other_obj_relation_def
         split: Structures_A.kernel_object.splits
                ARM_A.arch_kernel_obj.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> other_obj_relation ko (KOCTE cte)
theory CSpace1_R

lemma setCTE_pspace_only:
  "(rv, s') \<in> fst (setCTE p v s) \<Longrightarrow> \<exists>ps'. s' = ksPSpace_update (\<lambda>s. ps') s" apply (clarsimp simp: setCTE_def setObject_def in_monad split_def
                 dest!: in_inv_by_hoareD [OF updateObject_cte_inv]) apply (rule exI, rule refl) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (rv, s') \<in> fst (setCTE p v s) \<Longrightarrow> \<exists>ps'. s' = s\<lparr>ksPSpace := ps'\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>a b obj'. \<lbrakk>fst (lookupAround2 p (ksPSpace s)) = Some (a, b); s' = s\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr>\<rbrakk> \<Longrightarrow> \<exists>ps'. s\<lparr>ksPSpace := (ksPSpace s)(a \<mapsto> obj')\<rparr> = s\<lparr>ksPSpace := ps'\<rparr> proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma pspace_relation_cte_wp_atI:
  "\<lbrakk> pspace_relation (kheap s) (ksPSpace s');
     ctes_of (s' :: kernel_state) x = Some cte; valid_objs s \<rbrakk>
  \<Longrightarrow> \<exists>c slot. cte_wp_at ((=) c) slot s \<and> cap_relation c (cteCap cte) \<and> x = cte_map slot" apply (erule pspace_relation_cte_wp_atI'[where x=x]) apply (simp add: cte_wp_at_ctes_of) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); ctes_of s' x = Some cte; valid_objs s\<rbrakk> \<Longrightarrow> \<exists>c slot. cte_wp_at ((=) c) slot s \<and> cap_relation c (cteCap cte) \<and> x = cte_map slot proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ctes_of s' x = Some cte; valid_objs s\<rbrakk> \<Longrightarrow> cte_wp_at' ((=) cte) x s'
 2. \<lbrakk>ctes_of s' x = Some cte; valid_objs s\<rbrakk> \<Longrightarrow> valid_objs s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s' x = Some cte; valid_objs s\<rbrakk> \<Longrightarrow> valid_objs s proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma sameRegion_corres:
  "\<lbrakk> sameRegionAs c' d'; cap_relation c c'; cap_relation d d' \<rbrakk>
  \<Longrightarrow> same_region_as c d" by (simp add: same_region_as_relation)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>global.sameRegionAs c' d'; cap_relation c c'; cap_relation d d'\<rbrakk> \<Longrightarrow> same_region_as c d
theory CSpace1_R

lemma obj_refs_relation_Master:
  "cap_relation cap cap' \<Longrightarrow>
   obj_refs cap = (if isUntypedCap (capMasterCap cap') then {}
                    else if capClass (capMasterCap cap') = PhysicalClass
                    then {capUntypedPtr (capMasterCap cap')}
                    else {})" by (simp add: isCap_simps
         split: cap_relation_split_asm arch_cap.split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_relation cap cap' \<Longrightarrow> obj_refs cap = (if isUntypedCap (capMasterCap cap') then {} else if capClass (capMasterCap cap') = PhysicalClass then {global.capUntypedPtr (capMasterCap cap')} else {})
theory CSpace1_R

lemma cap_irqs_relation_Master:
  "cap_relation cap cap' \<Longrightarrow>
   cap_irqs cap = (case capMasterCap cap' of IRQHandlerCap irq \<Rightarrow> {irq} | _ \<Rightarrow> {})" by (simp split: cap_relation_split_asm arch_cap.split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_relation cap cap' \<Longrightarrow> cap_irqs cap = (case capMasterCap cap' of capability.IRQHandlerCap irq \<Rightarrow> {irq} | _ \<Rightarrow> {})
theory CSpace1_R

lemma arch_gen_refs_relation_Master:
  "cap_relation cap cap' \<Longrightarrow>
   arch_gen_refs cap = {}" by (simp split: cap_relation_split_asm arch_cap.split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_relation cap cap' \<Longrightarrow> arch_gen_refs cap = {}
theory CSpace1_R

lemma isMDBParent_sameRegion:
  "isMDBParentOf cte cte' \<Longrightarrow> sameRegionAs (cteCap cte) (cteCap cte')" by (simp add: isMDBParentOf_def split: cte.split_asm if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isMDBParentOf cte cte' \<Longrightarrow> global.sameRegionAs (cteCap cte) (cteCap cte')
theory CSpace1_R

lemma no_loops_no_subtree:
  "no_loops m \<Longrightarrow> m \<turnstile> x \<rightarrow> x = False" apply clarsimp apply (drule subtree_mdb_next) apply (simp add: no_loops_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_loops m \<Longrightarrow> m \<turnstile> x \<rightarrow> x = False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_loops m; m \<turnstile> x \<rightarrow> x\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_loops m; m \<turnstile> x \<leadsto>\<^sup>+ x\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma use_update_ztc_one:
  "((c \<noteq> slot \<or> True) \<longrightarrow> descendants_of' c m \<subseteq> descendants_of' c m')
           \<and> (True \<longrightarrow> descendants_of' c m' \<subseteq> descendants_of' c m)
      \<Longrightarrow> descendants_of' c m = descendants_of' c m'" by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (c \<noteq> slot \<or> True \<longrightarrow> descendants_of' c m \<subseteq> descendants_of' c m') \<and> (True \<longrightarrow> descendants_of' c m' \<subseteq> descendants_of' c m) \<Longrightarrow> descendants_of' c m = descendants_of' c m'
theory CSpace1_R

lemma use_update_ztc_two:
  "((c \<noteq> slot \<or> False) \<longrightarrow> descendants_of' c m \<subseteq> descendants_of' c m')
           \<and> (False \<longrightarrow> descendants_of' c m' \<subseteq> descendants_of' c m)
       \<Longrightarrow> descendants_of' slot m = {}
       \<Longrightarrow> descendants_of' c m \<subseteq> descendants_of' c m'" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(c \<noteq> slot \<or> False \<longrightarrow> descendants_of' c m \<subseteq> descendants_of' c m') \<and> (False \<longrightarrow> descendants_of' c m' \<subseteq> descendants_of' c m); descendants_of' slot m = {}\<rbrakk> \<Longrightarrow> descendants_of' c m \<subseteq> descendants_of' c m'
theory CSpace1_R

lemma cte_at'_obj_at':
  "cte_at' addr s = (obj_at' (\<lambda>_ :: cte. True) addr s
                      \<or> (\<exists>n \<in> dom tcb_cte_cases. tcb_at' (addr - n) s))" by (simp add: cte_wp_at'_obj_at')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at' (\<lambda>_. True) addr s = (real_cte_at' addr s \<or> (\<exists>n\<in>dom tcb_cte_cases. tcb_at' (addr - n) s))
theory CSpace1_R

lemma no_fail_updateCap [wp]:
  "no_fail (cte_at' p) (updateCap p cap')" apply (simp add: updateCap_def) apply (rule no_fail_pre, wp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (cte_wp_at' (\<lambda>_. True) p) (updateCap p cap') proof (prove)
goal (1 subgoal):
 1. no_fail (cte_wp_at' (\<lambda>_. True) p) (do cte <- getCTE p;
setCTE p (cteCap_update (\<lambda>_. cap') cte)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s. cte_wp_at' (\<lambda>_. True) p s \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) p and cte_wp_at' (\<lambda>_. True) p) s proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma capRange_cap_relation:
  "\<lbrakk> cap_relation cap cap'; cap_relation cap cap' \<Longrightarrow> capClass cap' = PhysicalClass \<rbrakk>
    \<Longrightarrow> capRange cap' = {obj_ref_of cap .. obj_ref_of cap + obj_size cap - 1}" by (simp add: capRange_def objBits_simps' cte_level_bits_def
                asid_low_bits_def pageBits_def zbits_map_def
         split: cap_relation_split_asm arch_cap.split_asm
                option.split sum.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation cap cap'; cap_relation cap cap' \<Longrightarrow> capClass cap' = PhysicalClass\<rbrakk> \<Longrightarrow> capRange cap' = {obj_ref_of cap..obj_ref_of cap + obj_size cap - 1}
theory CSpace1_R

lemma cap_relation_untyped_ptr_obj_refs:
  "cap_relation cap cap' \<Longrightarrow> capClass cap' = PhysicalClass \<Longrightarrow> \<not> isUntypedCap cap'
        \<Longrightarrow> capUntypedPtr cap' \<in> obj_refs cap" by (clarsimp simp add: isCap_simps
               simp del: not_ex
                  split: cap_relation_split_asm arch_cap.split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation cap cap'; capClass cap' = PhysicalClass; \<not> isUntypedCap cap'\<rbrakk> \<Longrightarrow> global.capUntypedPtr cap' \<in> obj_refs cap
theory CSpace1_R

lemma obj_refs_cap_relation_untyped_ptr:
  "\<lbrakk> cap_relation cap cap'; obj_refs cap \<noteq> {} \<rbrakk> \<Longrightarrow> capUntypedPtr cap' \<in> obj_refs cap" by (clarsimp split: cap_relation_split_asm arch_cap.split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation cap cap'; obj_refs cap \<noteq> {}\<rbrakk> \<Longrightarrow> global.capUntypedPtr cap' \<in> obj_refs cap
theory CSpace1_R

lemma capClass_ztc_relation:
  "\<lbrakk> is_zombie c \<or> is_cnode_cap c \<or> is_thread_cap c;
       cap_relation c c' \<rbrakk> \<Longrightarrow> capClass c' = PhysicalClass" by (auto simp: is_cap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_zombie c \<or> is_cnode_cap c \<or> is_thread_cap c; cap_relation c c'\<rbrakk> \<Longrightarrow> capClass c' = PhysicalClass
theory CSpace1_R

lemma exst_set_cap:
  "(x,s') \<in> fst (set_cap p c s) \<Longrightarrow> exst s' = exst s" by (clarsimp simp: set_cap_def in_monad split_def get_object_def set_object_def
               split: if_split_asm Structures_A.kernel_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x, s') \<in> fst (set_cap p c s) \<Longrightarrow> exst s' = exst s
theory CSpace1_R

lemma updateMDB_pspace_relations:
  assumes "(x, s'') \<in> fst (updateMDB p f s')"
  assumes "pspace_relations (ekheap s) (kheap s) (ksPSpace s')"
  assumes "pspace_aligned' s'" "pspace_distinct' s'"
  shows "pspace_relations (ekheap s) (kheap s) (ksPSpace s'')" using assms by (simp add: pspace_relations_def updateMDB_pspace_relation updateMDB_ekheap_relation)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pspace_relations (ekheap s) (kheap s) (ksPSpace s'') proof (prove)
using this:
(x, s'') \<in> fst (updateMDB p f s')
pspace_relations (ekheap s) (kheap s) (ksPSpace s')
pspace_aligned' s'
pspace_distinct' s'

goal (1 subgoal):
 1. pspace_relations (ekheap s) (kheap s) (ksPSpace s'')
theory CSpace1_R

lemma updateMDB_ctes_of:
  assumes "(x, s') \<in> fst (updateMDB p f s)"
  assumes "no_0 (ctes_of s)"
  shows "ctes_of s' = modify_map (ctes_of s) p (cteMDBNode_update f)" using assms apply (clarsimp simp: valid_def) apply (drule use_valid) apply (rule updateMDB_ctes_of_no_0) prefer 2 apply assumption apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ctes_of s' = modify_map (ctes_of s) p (cteMDBNode_update f) proof (prove)
using this:
(x, s') \<in> fst (updateMDB p f s)
no_0 (ctes_of s)

goal (1 subgoal):
 1. ctes_of s' = modify_map (ctes_of s) p (cteMDBNode_update f) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((), s') \<in> fst (updateMDB p f s); no_0 (ctes_of s)\<rbrakk> \<Longrightarrow> ctes_of s' = modify_map (ctes_of s) p (cteMDBNode_update f) proof (prove)
goal (3 subgoals):
 1. no_0 (ctes_of s) \<Longrightarrow> \<lbrace>?P2\<rbrace> updateMDB p f \<lbrace>?Q2\<rbrace>
 2. no_0 (ctes_of s) \<Longrightarrow> ?P2 s
 3. \<lbrakk>no_0 (ctes_of s); ?Q2 () s'\<rbrakk> \<Longrightarrow> ctes_of s' = modify_map (ctes_of s) p (cteMDBNode_update f) proof (prove)
goal (2 subgoals):
 1. no_0 (ctes_of s) \<Longrightarrow> no_0 (ctes_of s) \<and> ?P6 (modify_map (ctes_of s) p (cteMDBNode_update f))
 2. \<lbrakk>no_0 (ctes_of s); ?P6 (ctes_of s')\<rbrakk> \<Longrightarrow> ctes_of s' = modify_map (ctes_of s) p (cteMDBNode_update f) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>no_0 (ctes_of s); ?P6 (ctes_of s')\<rbrakk> \<Longrightarrow> ctes_of s' = modify_map (ctes_of s) p (cteMDBNode_update f)
 2. no_0 (ctes_of s) \<Longrightarrow> no_0 (ctes_of s) \<and> ?P6 (modify_map (ctes_of s) p (cteMDBNode_update f)) proof (prove)
goal (1 subgoal):
 1. no_0 (ctes_of s) \<Longrightarrow> no_0 (ctes_of s) \<and> modify_map (ctes_of s) p (cteMDBNode_update f) = modify_map (ctes_of s) p (cteMDBNode_update f) proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma revokable_eq:
  "\<lbrakk> cap_relation c c'; cap_relation src_cap src_cap'; sameRegionAs src_cap' c';
     is_untyped_cap src_cap \<longrightarrow> \<not> is_ep_cap c \<and> \<not> is_ntfn_cap c\<rbrakk>
  \<Longrightarrow> revokable src_cap c = revokable' src_cap' c'" apply (clarsimp simp: isCap_simps objBits_simps pageBits_def
                        bits_of_def revokable_def revokable'_def
                        sameRegionAs_def3
                 split: cap_relation_split_asm arch_cap.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation c c'; cap_relation src_cap src_cap'; global.sameRegionAs src_cap' c'; is_untyped_cap src_cap \<longrightarrow> \<not> is_ep_cap c \<and> \<not> is_ntfn_cap c\<rbrakk> \<Longrightarrow> revokable src_cap c = revokable' src_cap' c' proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma isMDBParentOf_prev_update [simp]:
  "isMDBParentOf (cteMDBNode_update (mdbPrev_update f) cte) cte' =
   isMDBParentOf cte cte'"
  "isMDBParentOf cte (cteMDBNode_update (mdbPrev_update f) cte') =
   isMDBParentOf cte cte'" apply (cases cte) apply (cases cte') apply (simp add: isMDBParentOf_def) apply (cases cte) apply (cases cte') apply (clarsimp simp: isMDBParentOf_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isMDBParentOf (cteMDBNode_update (mdbPrev_update f) cte) cte' = isMDBParentOf cte cte' &&& isMDBParentOf cte (cteMDBNode_update (mdbPrev_update f) cte') = isMDBParentOf cte cte' proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2. cte = CTE x1 x2 \<Longrightarrow> isMDBParentOf (cteMDBNode_update (mdbPrev_update f) cte) cte' = isMDBParentOf cte cte'
 2. isMDBParentOf cte (cteMDBNode_update (mdbPrev_update f) cte') = isMDBParentOf cte cte' proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x1a x2a. \<lbrakk>cte = CTE x1 x2; cte' = CTE x1a x2a\<rbrakk> \<Longrightarrow> isMDBParentOf (cteMDBNode_update (mdbPrev_update f) cte) cte' = isMDBParentOf cte cte'
 2. isMDBParentOf cte (cteMDBNode_update (mdbPrev_update f) cte') = isMDBParentOf cte cte' proof (prove)
goal (1 subgoal):
 1. isMDBParentOf cte (cteMDBNode_update (mdbPrev_update f) cte') = isMDBParentOf cte cte' proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. cte = CTE x1 x2 \<Longrightarrow> isMDBParentOf cte (cteMDBNode_update (mdbPrev_update f) cte') = isMDBParentOf cte cte' proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a. \<lbrakk>cte = CTE x1 x2; cte' = CTE x1a x2a\<rbrakk> \<Longrightarrow> isMDBParentOf cte (cteMDBNode_update (mdbPrev_update f) cte') = isMDBParentOf cte cte' proof (prove)
goal:
No subgoals!
theory CSpace1_R

lemma prev_update_modify_mdb_relation:
  "cdt_relation c m (modify_map m' x (cteMDBNode_update (mdbPrev_update f)))
  = cdt_relation c m m'" by (fastforce simp: cdt_relation_def descendants_of'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cdt_relation c m (modify_map m' x (cteMDBNode_update (mdbPrev_update f))) = cdt_relation c m m'
theory CSpace1_R

lemma isArchCap_simps[simp]:
  "isArchCap P (capability.ThreadCap xc) = False"
  "isArchCap P capability.NullCap = False"
  "isArchCap P capability.DomainCap = False"
  "isArchCap P (capability.NotificationCap xca xba xaa xd) = False"
  "isArchCap P (capability.EndpointCap xda xcb xbb xab xe xi) = False"
  "isArchCap P (capability.IRQHandlerCap xf) = False"
  "isArchCap P (capability.Zombie xbc xac xg) = False"
  "isArchCap P (capability.ArchObjectCap xh) = P xh"
  "isArchCap P (capability.ReplyCap xad xi xia) = False"
  "isArchCap P (capability.UntypedCap d xae xj f) = False"
  "isArchCap P (capability.CNodeCap xfa xea xdb xcc) = False"
  "isArchCap P capability.IRQControlCap = False" by (simp add: isArchCap_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((isArchCap P (capability.ThreadCap xc) = False &&& isArchCap P capability.NullCap = False &&& isArchCap P capability.DomainCap = False) &&& isArchCap P (capability.NotificationCap xca xba xaa xd) = False &&& isArchCap P (capability.EndpointCap xda xcb xbb xab xe xi) = False &&& isArchCap P (capability.IRQHandlerCap xf) = False) &&& (isArchCap P (capability.Zombie xbc xac xg) = False &&& isArchCap P (capability.ArchObjectCap xh) = P xh &&& isArchCap P (capability.ReplyCap xad xi xia) = False) &&& isArchCap P (capability.UntypedCap d xae xj f) = False &&& isArchCap P (capability.CNodeCap xfa xea xdb xcc) = False &&& isArchCap P capability.IRQControlCap = False
theory CSpace1_R

lemma zbits_map_eq[simp]:
  "(zbits_map zbits = zbits_map zbits')
      = (zbits = zbits')" by (simp add: zbits_map_def split: option.split sum.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (zbits_map zbits = zbits_map zbits') = (zbits = zbits')
theory CSpace1_R

lemma master_cap_relation:
  "\<lbrakk> cap_relation c c'; cap_relation d d' \<rbrakk> \<Longrightarrow>
  (capMasterCap c' = capMasterCap d') =
  (cap_master_cap c = cap_master_cap d)" by (auto simp add: cap_master_cap_def capMasterCap_def split: cap.splits arch_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation c c'; cap_relation d d'\<rbrakk> \<Longrightarrow> (capMasterCap c' = capMasterCap d') = (cap_master_cap c = cap_master_cap d)
theory CSpace1_R

lemma cap_badge_relation:
  "\<lbrakk> cap_relation c c'; cap_relation d d' \<rbrakk> \<Longrightarrow>
  (capBadge c' = capBadge d') =
  (cap_badge c = cap_badge d)" by (auto simp add: cap_badge_def split: cap.splits arch_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation c c'; cap_relation d d'\<rbrakk> \<Longrightarrow> (capBadge c' = capBadge d') = (cap_badge c = cap_badge d)