kings-crown/FVELER_Isabelle huggingface dataset:
theory Untyped_R

lemma n'_direct_eq:
  "n' \<turnstile> p \<leadsto> p' = (if p = parent then p' = site else
                  if p = site then m \<turnstile> parent \<leadsto> p'
                  else m \<turnstile> p \<leadsto> p')" by (simp add: n'_def n_direct_eq)

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

lemma n'_tranclD:
  "n' \<turnstile> p \<leadsto>\<^sup>+ p' \<Longrightarrow>
  (if p = site then m \<turnstile> parent \<leadsto>\<^sup>+ p'
   else if m \<turnstile> p \<leadsto>\<^sup>+ parent \<or> p = parent  then m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> p' = site
   else m \<turnstile> p \<leadsto>\<^sup>+ p')" apply (erule trancl_induct) apply (fastforce simp: n'_direct_eq split: if_split_asm) apply (fastforce simp: n'_direct_eq split: if_split_asm elim: trancl_trans) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n' \<turnstile> p \<leadsto>\<^sup>+ p' \<Longrightarrow> if p = site then m \<turnstile> parent \<leadsto>\<^sup>+ p' else if m \<turnstile> p \<leadsto>\<^sup>+ parent \<or> p = parent then m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> p' = site else m \<turnstile> p \<leadsto>\<^sup>+ p' proof (prove)
goal (2 subgoals):
 1. \<And>y. n' \<turnstile> p \<leadsto> y \<Longrightarrow> if p = site then m \<turnstile> parent \<leadsto>\<^sup>+ y else if m \<turnstile> p \<leadsto>\<^sup>+ parent \<or> p = parent then m \<turnstile> p \<leadsto>\<^sup>+ y \<or> y = site else m \<turnstile> p \<leadsto>\<^sup>+ y
 2. \<And>y z. \<lbrakk>n' \<turnstile> p \<leadsto>\<^sup>+ y; n' \<turnstile> y \<leadsto> z; if p = site then m \<turnstile> parent \<leadsto>\<^sup>+ y else if m \<turnstile> p \<leadsto>\<^sup>+ parent \<or> p = parent then m \<turnstile> p \<leadsto>\<^sup>+ y \<or> y = site else m \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> if p = site then m \<turnstile> parent \<leadsto>\<^sup>+ z else if m \<turnstile> p \<leadsto>\<^sup>+ parent \<or> p = parent then m \<turnstile> p \<leadsto>\<^sup>+ z \<or> z = site else m \<turnstile> p \<leadsto>\<^sup>+ z proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>n' \<turnstile> p \<leadsto>\<^sup>+ y; n' \<turnstile> y \<leadsto> z; if p = site then m \<turnstile> parent \<leadsto>\<^sup>+ y else if m \<turnstile> p \<leadsto>\<^sup>+ parent \<or> p = parent then m \<turnstile> p \<leadsto>\<^sup>+ y \<or> y = site else m \<turnstile> p \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> if p = site then m \<turnstile> parent \<leadsto>\<^sup>+ z else if m \<turnstile> p \<leadsto>\<^sup>+ parent \<or> p = parent then m \<turnstile> p \<leadsto>\<^sup>+ z \<or> z = site else m \<turnstile> p \<leadsto>\<^sup>+ z proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma site_in_dom: "site \<in> dom n" by (simp add: n)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. site \<in> dom n
theory Untyped_R

lemma n'_rtrancl_eq:
  "n' \<turnstile> p \<leadsto>\<^sup>* p' =
   (if p = site then p' \<noteq> site \<and> m \<turnstile> parent \<leadsto>\<^sup>+ p' \<or> p' = site
    else if m \<turnstile> p \<leadsto>\<^sup>* parent then m \<turnstile> p \<leadsto>\<^sup>* p' \<or> p' = site
    else m \<turnstile> p \<leadsto>\<^sup>* p')" by (auto simp: rtrancl_eq_or_trancl n'_trancl_eq)

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

lemma mdbNext_parent_site [simp]:
  "mdbNext parent_node \<noteq> site" proof assume "mdbNext parent_node = site" hence "m \<turnstile> parent \<leadsto> site" using parent by (unfold mdb_next_unfold) simp thus False by simp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdbNext parent_node \<noteq> site proof (state)
goal (1 subgoal):
 1. mdbNext parent_node = site \<Longrightarrow> False proof (state)
this:
mdbNext parent_node = site

goal (1 subgoal):
 1. mdbNext parent_node = site \<Longrightarrow> False proof (prove)
using this:
mdbNext parent_node = site

goal (1 subgoal):
 1. m \<turnstile> parent \<leadsto> site proof (prove)
using this:
mdbNext parent_node = site
m parent = Some (CTE parent_cap parent_node)

goal (1 subgoal):
 1. m \<turnstile> parent \<leadsto> site proof (state)
this:
m \<turnstile> parent \<leadsto> site

goal (1 subgoal):
 1. mdbNext parent_node = site \<Longrightarrow> False proof (prove)
using this:
m \<turnstile> parent \<leadsto> site

goal (1 subgoal):
 1. False proof (state)
this:
False

goal:
No subgoals!
theory Untyped_R

lemma mdbPrev_parent_site [simp]:
  "site \<noteq> mdbPrev parent_node" proof assume "site = mdbPrev parent_node" with parent site have "m \<turnstile> site \<leadsto> parent" apply (unfold mdb_next_unfold) apply simp apply (erule dlistEp) apply clarsimp apply clarsimp done with p_0 show False by simp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. site \<noteq> mdbPrev parent_node proof (state)
goal (1 subgoal):
 1. site = mdbPrev parent_node \<Longrightarrow> False proof (state)
this:
site = mdbPrev parent_node

goal (1 subgoal):
 1. site = mdbPrev parent_node \<Longrightarrow> False proof (chain)
picking this:
m parent = Some (CTE parent_cap parent_node)
m site = Some (CTE site_cap site_node)
site = mdbPrev parent_node proof (prove)
using this:
m parent = Some (CTE parent_cap parent_node)
m site = Some (CTE site_cap site_node)
site = mdbPrev parent_node

goal (1 subgoal):
 1. m \<turnstile> site \<leadsto> parent proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m site = Some (CTE site_cap site_node); site = mdbPrev parent_node\<rbrakk> \<Longrightarrow> \<exists>z. m site = Some z \<and> parent = mdbNext (cteMDBNode z) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m parent = Some (CTE parent_cap parent_node); m (mdbPrev parent_node) = Some (CTE site_cap site_node); site = mdbPrev parent_node\<rbrakk> \<Longrightarrow> parent = mdbNext site_node proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m (mdbPrev parent_node) = Some (CTE site_cap site_node); site = mdbPrev parent_node\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode (CTE parent_cap parent_node)) \<noteq> 0
 2. \<And>cte'. \<lbrakk>m (mdbPrev parent_node) = Some (CTE site_cap site_node); site = mdbPrev parent_node; m (mdbPrev (cteMDBNode (CTE parent_cap parent_node))) = Some cte'; mdbNext (cteMDBNode cte') = parent\<rbrakk> \<Longrightarrow> parent = mdbNext site_node proof (prove)
goal (1 subgoal):
 1. \<And>cte'. \<lbrakk>m (mdbPrev parent_node) = Some (CTE site_cap site_node); site = mdbPrev parent_node; m (mdbPrev (cteMDBNode (CTE parent_cap parent_node))) = Some cte'; mdbNext (cteMDBNode cte') = parent\<rbrakk> \<Longrightarrow> parent = mdbNext site_node proof (prove)
goal:
No subgoals! proof (state)
this:
m \<turnstile> site \<leadsto> parent

goal (1 subgoal):
 1. site = mdbPrev parent_node \<Longrightarrow> False proof (chain)
picking this:
site \<noteq> 0
m \<turnstile> site \<leadsto> parent proof (prove)
using this:
site \<noteq> 0
m \<turnstile> site \<leadsto> parent

goal (1 subgoal):
 1. False proof (state)
this:
False

goal:
No subgoals!
theory Untyped_R

lemma parent_prev:
  "(m \<turnstile> parent \<leftarrow> p) = (p = mdbNext parent_node \<and> p \<noteq> 0)" apply (rule iffI) apply (frule dlist_prevD, rule parent) apply (simp add: mdb_next_unfold parent) apply (clarsimp simp: mdb_prev_def) apply clarsimp apply (rule dlist_nextD0) apply (rule parent_next) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> parent \<leftarrow> p = (p = mdbNext parent_node \<and> p \<noteq> 0) proof (prove)
goal (2 subgoals):
 1. m \<turnstile> parent \<leftarrow> p \<Longrightarrow> p = mdbNext parent_node \<and> p \<noteq> 0
 2. p = mdbNext parent_node \<and> p \<noteq> 0 \<Longrightarrow> m \<turnstile> parent \<leftarrow> p proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> parent \<leftarrow> p; m \<turnstile> parent \<leadsto> p\<rbrakk> \<Longrightarrow> p = mdbNext parent_node \<and> p \<noteq> 0
 2. p = mdbNext parent_node \<and> p \<noteq> 0 \<Longrightarrow> m \<turnstile> parent \<leftarrow> p proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<turnstile> parent \<leftarrow> mdbNext parent_node; p = mdbNext parent_node\<rbrakk> \<Longrightarrow> mdbNext parent_node \<noteq> 0
 2. p = mdbNext parent_node \<and> p \<noteq> 0 \<Longrightarrow> m \<turnstile> parent \<leftarrow> p proof (prove)
goal (1 subgoal):
 1. p = mdbNext parent_node \<and> p \<noteq> 0 \<Longrightarrow> m \<turnstile> parent \<leftarrow> p proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdbNext parent_node \<noteq> 0; p = mdbNext parent_node\<rbrakk> \<Longrightarrow> m \<turnstile> parent \<leftarrow> mdbNext parent_node proof (prove)
goal (2 subgoals):
 1. \<lbrakk>mdbNext parent_node \<noteq> 0; p = mdbNext parent_node\<rbrakk> \<Longrightarrow> m \<turnstile> parent \<leadsto> mdbNext parent_node
 2. \<lbrakk>mdbNext parent_node \<noteq> 0; p = mdbNext parent_node\<rbrakk> \<Longrightarrow> mdbNext parent_node \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdbNext parent_node \<noteq> 0; p = mdbNext parent_node\<rbrakk> \<Longrightarrow> mdbNext parent_node \<noteq> 0 proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma m_cap:
  "m p = Some (CTE c node) \<Longrightarrow>
  if p = site
  then \<exists>node'. n' site = Some (CTE c' node')
  else \<exists>node'. n' p = Some (CTE c node')" by (clarsimp simp: n n'_def new_parent_def new_site_def parent)

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

lemma no_next_region:
  "\<lbrakk> m \<turnstile> parent \<leadsto> p'; m p' = Some (CTE cap' node) \<rbrakk> \<Longrightarrow> \<not>sameRegionAs c' cap'" apply (clarsimp simp: mdb_next_unfold parent) apply (frule next_wont_bite [rotated], clarsimp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> parent \<leadsto> p'; m p' = Some (CTE cap' node)\<rbrakk> \<Longrightarrow> \<not> global.sameRegionAs c' cap' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p' = mdbNext parent_node; m (mdbNext parent_node) = Some (CTE cap' node); global.sameRegionAs c' cap'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p' = mdbNext parent_node; m (mdbNext parent_node) = Some (CTE cap' node); global.sameRegionAs c' cap'; \<not> global.sameRegionAs c' (cteCap (CTE cap' node))\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma c'_not_Null: "c' \<noteq> NullCap" using same_region by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. c' \<noteq> capability.NullCap proof (prove)
using this:
global.sameRegionAs parent_cap c'

goal (1 subgoal):
 1. c' \<noteq> capability.NullCap
theory Untyped_R

lemma phys': "capClass parent_cap = PhysicalClass" using sameRegionAs_classes [OF same_region] phys by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. capClass parent_cap = PhysicalClass proof (prove)
using this:
capClass parent_cap = capClass c'
capClass c' = PhysicalClass

goal (1 subgoal):
 1. capClass parent_cap = PhysicalClass
theory Untyped_R

lemma capRange_c': "capRange c' \<subseteq> capRange parent_cap" apply (rule sameRegionAs_capRange_subset) apply (rule same_region) apply (rule phys') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. capRange c' \<subseteq> capRange parent_cap proof (prove)
goal (2 subgoals):
 1. global.sameRegionAs parent_cap c'
 2. capClass parent_cap = PhysicalClass proof (prove)
goal (1 subgoal):
 1. capClass parent_cap = PhysicalClass proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma untypedRange_c':
  assumes ut: "isUntypedCap c'"
  shows "untypedRange c' \<subseteq> untypedRange parent_cap" using ut is_untyped capRange_c' by (auto simp: isCap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. untypedRange c' \<subseteq> untypedRange parent_cap proof (prove)
using this:
isUntypedCap c'
isUntypedCap parent_cap
capRange c' \<subseteq> capRange parent_cap

goal (1 subgoal):
 1. untypedRange c' \<subseteq> untypedRange parent_cap
theory Untyped_R

lemma sameRegion_parentI:
  "sameRegionAs c' cap \<Longrightarrow> sameRegionAs parent_cap cap" using same_region apply - apply (erule (1) sameRegionAs_trans) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. global.sameRegionAs c' cap \<Longrightarrow> global.sameRegionAs parent_cap cap proof (prove)
using this:
global.sameRegionAs parent_cap c'

goal (1 subgoal):
 1. global.sameRegionAs c' cap \<Longrightarrow> global.sameRegionAs parent_cap cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>global.sameRegionAs c' cap; global.sameRegionAs parent_cap c'\<rbrakk> \<Longrightarrow> global.sameRegionAs parent_cap cap proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma rangeD:
  "\<lbrakk> m \<turnstile> parent \<rightarrow> p; m p = Some (CTE cap node) \<rbrakk> \<Longrightarrow>
  capRange cap \<inter> capRange c' = {}" using range by (rule descendants_rangeD')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> parent \<rightarrow> p; m p = Some (CTE cap node)\<rbrakk> \<Longrightarrow> capRange cap \<inter> capRange c' = {} proof (prove)
using this:
descendants_range' c' parent m

goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> parent \<rightarrow> p; m p = Some (CTE cap node)\<rbrakk> \<Longrightarrow> capRange cap \<inter> capRange c' = {}
theory Untyped_R

lemma capAligned_c': "capAligned c'" using valid_c' by (rule valid_capAligned)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. capAligned c' proof (prove)
using this:
valid_cap' c' s

goal (1 subgoal):
 1. capAligned c'
theory Untyped_R

lemma capRange_ut:
  "capRange c' \<subseteq> untypedRange parent_cap" using capRange_c' is_untyped by (clarsimp simp: isCap_simps del: subsetI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. capRange c' \<subseteq> untypedRange parent_cap proof (prove)
using this:
capRange c' \<subseteq> capRange parent_cap
isUntypedCap parent_cap

goal (1 subgoal):
 1. capRange c' \<subseteq> untypedRange parent_cap
theory Untyped_R

lemma site':
  "n' site = Some new_site" by (simp add: n n'_def modify_map_if new_site_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n' site = Some new_site
theory Untyped_R

lemma loopE: "m \<turnstile> x \<leadsto>\<^sup>+ x \<Longrightarrow> P" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> x \<leadsto>\<^sup>+ x \<Longrightarrow> P
theory Untyped_R

lemma m_loop_trancl_rtrancl:
  "m \<turnstile> y \<leadsto>\<^sup>* x \<Longrightarrow> \<not> m \<turnstile> x \<leadsto>\<^sup>+ y" apply clarsimp apply (drule(1) transitive_closure_trans) apply (erule loopE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> y \<leadsto>\<^sup>* x \<Longrightarrow> (x, y) \<notin> (mdb_next_rel m)\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> y \<leadsto>\<^sup>* x; m \<turnstile> x \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<turnstile> x \<leadsto>\<^sup>+ y; m \<turnstile> y \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma m_rtrancl_to_site:
  "m \<turnstile> p \<leadsto>\<^sup>* site = (p = site)" apply (rule iffI) apply (erule rtranclE) apply assumption apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> p \<leadsto>\<^sup>* site = (p = site) proof (prove)
goal (2 subgoals):
 1. m \<turnstile> p \<leadsto>\<^sup>* site \<Longrightarrow> p = site
 2. p = site \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>* site proof (prove)
goal (3 subgoals):
 1. p = site \<Longrightarrow> p = site
 2. \<And>y. \<lbrakk>m \<turnstile> p \<leadsto>\<^sup>* y; m \<turnstile> y \<leadsto> site\<rbrakk> \<Longrightarrow> p = site
 3. p = site \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>* site proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>m \<turnstile> p \<leadsto>\<^sup>* y; m \<turnstile> y \<leadsto> site\<rbrakk> \<Longrightarrow> p = site
 2. p = site \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>* site proof (prove)
goal (1 subgoal):
 1. p = site \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>* site proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma descendants_of'_D: "p' \<in> descendants_of' p ctes \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p' " by (clarsimp simp:descendants_of'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. p' \<in> descendants_of' p ctes \<Longrightarrow> ctes \<turnstile> p \<rightarrow> p'
theory Untyped_R

lemma parent_chunk:
  "is_chunk n' parent_cap parent site" by (clarsimp simp: is_chunk_def
                     n'_trancl_eq n'_rtrancl_eq site' new_site_def same_region
                     m_loop_trancl_rtrancl m_rtrancl_to_site)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_chunk n' parent_cap parent site
theory Untyped_R

lemma ut_rev_n' [simp]: "ut_revocable' n'" using ut_rev apply (clarsimp simp: ut_revocable'_def n'_def n_def) apply (clarsimp simp: modify_map_if split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ut_revocable' n' proof (prove)
using this:
ut_revocable' m

goal (1 subgoal):
 1. ut_revocable' n' proof (prove)
goal (1 subgoal):
 1. \<And>p cap n. \<lbrakk>\<forall>p cap n. m p = Some (CTE cap n) \<longrightarrow> isUntypedCap cap \<longrightarrow> mdbRevocable n; modify_map (modify_map (\<lambda>x. if x = site then Some (CTE c' (MDB (mdbNext parent_node) parent True True)) else m x) parent (cteMDBNode_update (mdbNext_update (\<lambda>x. site)))) (mdbNext parent_node) (cteMDBNode_update (mdbPrev_update (\<lambda>a. site))) p = Some (CTE cap n); isUntypedCap cap\<rbrakk> \<Longrightarrow> mdbRevocable n proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma class_links_m: "class_links m" using valid by (simp add: valid_mdb_ctes_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. class_links m proof (prove)
using this:
valid_mdb_ctes m

goal (1 subgoal):
 1. class_links m
theory Untyped_R

lemma parent_phys: "capClass parent_cap = PhysicalClass" using is_untyped by (clarsimp simp: isCap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. capClass parent_cap = PhysicalClass proof (prove)
using this:
isUntypedCap parent_cap

goal (1 subgoal):
 1. capClass parent_cap = PhysicalClass
theory Untyped_R

lemma irq_control_n' [simp]:
  "irq_control n'" using irq_control phys apply (clarsimp simp: irq_control_def) apply (clarsimp simp: n'_def n_def) apply (clarsimp simp: modify_map_if split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. irq_control n' proof (prove)
using this:
irq_control m
capClass c' = PhysicalClass

goal (1 subgoal):
 1. irq_control n' proof (prove)
goal (1 subgoal):
 1. \<And>p n. \<lbrakk>\<forall>p n. m p = Some (CTE capability.IRQControlCap n) \<longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p); capClass c' = PhysicalClass; n' p = Some (CTE capability.IRQControlCap n)\<rbrakk> \<Longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'a. n' p' = Some (CTE capability.IRQControlCap n'a)) \<longrightarrow> p' = p) proof (prove)
goal (1 subgoal):
 1. \<And>p n. \<lbrakk>\<forall>p n. m p = Some (CTE capability.IRQControlCap n) \<longrightarrow> mdbRevocable n \<and> (\<forall>p'. (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p); capClass c' = PhysicalClass; modify_map (modify_map (\<lambda>x. if x = site then Some (CTE c' (MDB (mdbNext parent_node) parent True True)) else m x) parent (cteMDBNode_update (mdbNext_update (\<lambda>x. site)))) (mdbNext parent_node) (cteMDBNode_update (mdbPrev_update (\<lambda>a. site))) p = Some (CTE capability.IRQControlCap n)\<rbrakk> \<Longrightarrow> mdbRevocable n \<and> (\<forall>p'. (p' = site \<longrightarrow> c' = capability.IRQControlCap \<longrightarrow> site = p) \<and> (p' \<noteq> site \<longrightarrow> (\<exists>n'. m p' = Some (CTE capability.IRQControlCap n')) \<longrightarrow> p' = p)) proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma dist_z_m:
  "distinct_zombies m" using valid by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. distinct_zombies m proof (prove)
using this:
valid_mdb_ctes m

goal (1 subgoal):
 1. distinct_zombies m
theory Untyped_R

lemma reply_masters_rvk_fb_m:
  "reply_masters_rvk_fb m" using valid by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reply_masters_rvk_fb m proof (prove)
using this:
valid_mdb_ctes m

goal (1 subgoal):
 1. reply_masters_rvk_fb m
theory Untyped_R

lemma reply_masters_rvk_fb_n[simp]:
  "reply_masters_rvk_fb n'" using reply_masters_rvk_fb_m apply (simp add: reply_masters_rvk_fb_def n'_def ball_ran_modify_map_eq
                   n_def fun_upd_def[symmetric]) apply (rule ball_ran_fun_updI, assumption) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reply_masters_rvk_fb n' proof (prove)
using this:
reply_masters_rvk_fb m

goal (1 subgoal):
 1. reply_masters_rvk_fb n' proof (prove)
goal (1 subgoal):
 1. \<forall>cte\<in>ran m. isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte) \<longrightarrow> mdbRevocable (cteMDBNode cte) \<and> mdbFirstBadged (cteMDBNode cte) \<Longrightarrow> \<forall>cte\<in>ran (m(site \<mapsto> CTE c' (MDB (mdbNext parent_node) parent True True))). isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte) \<longrightarrow> mdbRevocable (cteMDBNode cte) \<and> mdbFirstBadged (cteMDBNode cte) proof (prove)
goal (1 subgoal):
 1. \<forall>cte\<in>ran m. isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte) \<longrightarrow> mdbRevocable (cteMDBNode cte) \<and> mdbFirstBadged (cteMDBNode cte) \<Longrightarrow> \<forall>cte. Some (CTE c' (MDB (mdbNext parent_node) parent True True)) = Some cte \<longrightarrow> isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte) \<longrightarrow> mdbRevocable (cteMDBNode cte) \<and> mdbFirstBadged (cteMDBNode cte) proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma valid_n':
  "untypedRange c' \<inter> usableUntypedRange parent_cap = {} \<Longrightarrow> valid_mdb_ctes n'" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. untypedRange c' \<inter> usableUntypedRange parent_cap = {} \<Longrightarrow> valid_mdb_ctes n'