kings-crown/FVELER_Isabelle huggingface dataset:
theory CSpace_AI

lemma parent_m:
  "m \<Turnstile> p \<rightarrow> p' \<Longrightarrow> n \<Turnstile> p \<rightarrow> p'" apply (erule trancl_induct) apply (rule r_into_trancl) apply (simp add: n_def cdt_parent_defs) apply (rule impI) apply simp apply (erule trancl_into_trancl) apply (simp add: n_def cdt_parent_defs) apply (rule impI) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<Turnstile> p \<rightarrow> p' \<Longrightarrow> n \<Turnstile> p \<rightarrow> p' proof (prove)
goal (2 subgoals):
 1. \<And>y. m \<Turnstile> p \<leadsto> y \<Longrightarrow> n \<Turnstile> p \<rightarrow> y
 2. \<And>y z. \<lbrakk>m \<Turnstile> p \<rightarrow> y; m \<Turnstile> y \<leadsto> z; n \<Turnstile> p \<rightarrow> y\<rbrakk> \<Longrightarrow> n \<Turnstile> p \<rightarrow> z proof (prove)
goal (2 subgoals):
 1. \<And>y. m \<Turnstile> p \<leadsto> y \<Longrightarrow> n \<Turnstile> p \<leadsto> y
 2. \<And>y z. \<lbrakk>m \<Turnstile> p \<rightarrow> y; m \<Turnstile> y \<leadsto> z; n \<Turnstile> p \<rightarrow> y\<rbrakk> \<Longrightarrow> n \<Turnstile> p \<rightarrow> z proof (prove)
goal (2 subgoals):
 1. \<And>y. m y = Some p \<Longrightarrow> y = dest \<longrightarrow> m src = Some p
 2. \<And>y z. \<lbrakk>m \<Turnstile> p \<rightarrow> y; m \<Turnstile> y \<leadsto> z; n \<Turnstile> p \<rightarrow> y\<rbrakk> \<Longrightarrow> n \<Turnstile> p \<rightarrow> z proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>m y = Some p; y = dest\<rbrakk> \<Longrightarrow> m src = Some p
 2. \<And>y z. \<lbrakk>m \<Turnstile> p \<rightarrow> y; m \<Turnstile> y \<leadsto> z; n \<Turnstile> p \<rightarrow> y\<rbrakk> \<Longrightarrow> n \<Turnstile> p \<rightarrow> z proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>m \<Turnstile> p \<rightarrow> y; m \<Turnstile> y \<leadsto> z; n \<Turnstile> p \<rightarrow> y\<rbrakk> \<Longrightarrow> n \<Turnstile> p \<rightarrow> z proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>m \<Turnstile> p \<rightarrow> y; m \<Turnstile> y \<leadsto> z\<rbrakk> \<Longrightarrow> n \<Turnstile> y \<leadsto> z proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(p, y) \<in> {(p, c). m c = Some p}\<^sup>+; m z = Some y\<rbrakk> \<Longrightarrow> z = dest \<longrightarrow> m src = Some y proof (prove)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(p, y) \<in> {(p, c). m c = Some p}\<^sup>+; m z = Some y; z = dest\<rbrakk> \<Longrightarrow> m src = Some y proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma parent_n_eq:
  "n \<Turnstile> p \<rightarrow> p' = (if p' = dest then m \<Turnstile> p \<rightarrow> src else m \<Turnstile> p \<rightarrow> p')" apply (rule iffI) apply (erule parent_n) apply (simp split: if_split_asm) apply (erule parent_m_dest) apply (erule parent_m) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<Turnstile> p \<rightarrow> p' = (if p' = dest then m \<Turnstile> p \<rightarrow> src else m \<Turnstile> p \<rightarrow> p') proof (prove)
goal (2 subgoals):
 1. n \<Turnstile> p \<rightarrow> p' \<Longrightarrow> if p' = dest then m \<Turnstile> p \<rightarrow> src else m \<Turnstile> p \<rightarrow> p'
 2. if p' = dest then m \<Turnstile> p \<rightarrow> src else m \<Turnstile> p \<rightarrow> p' \<Longrightarrow> n \<Turnstile> p \<rightarrow> p' proof (prove)
goal (1 subgoal):
 1. if p' = dest then m \<Turnstile> p \<rightarrow> src else m \<Turnstile> p \<rightarrow> p' \<Longrightarrow> n \<Turnstile> p \<rightarrow> p' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p' = dest; m \<Turnstile> p \<rightarrow> src\<rbrakk> \<Longrightarrow> n \<Turnstile> p \<rightarrow> dest
 2. \<lbrakk>p' \<noteq> dest; m \<Turnstile> p \<rightarrow> p'\<rbrakk> \<Longrightarrow> n \<Turnstile> p \<rightarrow> p' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p' \<noteq> dest; m \<Turnstile> p \<rightarrow> p'\<rbrakk> \<Longrightarrow> n \<Turnstile> p \<rightarrow> p' proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma descendants:
  "descendants_of p n =
   descendants_of p m \<union> (if src \<in> descendants_of p m then {dest} else {})" by (rule set_eqI) (simp add: descendants_of_def parent_n_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. descendants_of p n = descendants_of p m \<union> (if src \<in> descendants_of p m then {dest} else {})
theory CSpace_AI

lemma master_cap_class:
  "cap_master_cap a = cap_master_cap b
  \<Longrightarrow> cap_class a = cap_class b" apply (case_tac a) apply (clarsimp simp: cap_master_cap_simps dest!:cap_master_cap_eqDs master_arch_cap_cap_class)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_master_cap a = cap_master_cap b \<Longrightarrow> cap_class a = cap_class b proof (prove)
goal (12 subgoals):
 1. \<lbrakk>cap_master_cap a = cap_master_cap b; a = NullCap\<rbrakk> \<Longrightarrow> cap_class a = cap_class b
 2. \<And>x21 x22 x23 x24. \<lbrakk>cap_master_cap a = cap_master_cap b; a = UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> cap_class a = cap_class b
 3. \<And>x31 x32 x33. \<lbrakk>cap_master_cap a = cap_master_cap b; a = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> cap_class a = cap_class b
 4. \<And>x41 x42 x43. \<lbrakk>cap_master_cap a = cap_master_cap b; a = NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> cap_class a = cap_class b
 5. \<And>x51 x52 x53. \<lbrakk>cap_master_cap a = cap_master_cap b; a = ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> cap_class a = cap_class b
 6. \<And>x61 x62 x63. \<lbrakk>cap_master_cap a = cap_master_cap b; a = CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> cap_class a = cap_class b
 7. \<And>x7. \<lbrakk>cap_master_cap a = cap_master_cap b; a = ThreadCap x7\<rbrakk> \<Longrightarrow> cap_class a = cap_class b
 8. \<lbrakk>cap_master_cap a = cap_master_cap b; a = DomainCap\<rbrakk> \<Longrightarrow> cap_class a = cap_class b
 9. \<lbrakk>cap_master_cap a = cap_master_cap b; a = IRQControlCap\<rbrakk> \<Longrightarrow> cap_class a = cap_class b
 10. \<And>x10. \<lbrakk>cap_master_cap a = cap_master_cap b; a = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> cap_class a = cap_class b
A total of 12 subgoals... proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma mdb_cte_at_Null_None:
  "\<lbrakk> cs p = Some cap.NullCap;
     mdb_cte_at (\<lambda>p. \<exists>c. cs p = Some c \<and> cap.NullCap \<noteq> c) m \<rbrakk>
  \<Longrightarrow> m p = None" apply (simp add: mdb_cte_at_def) apply (rule classical) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cs p = Some NullCap; mdb_cte_at (\<lambda>p. \<exists>c. cs p = Some c \<and> NullCap \<noteq> c) m\<rbrakk> \<Longrightarrow> m p = None proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cs p = Some NullCap; \<forall>p c. m c = Some p \<longrightarrow> (\<exists>c. cs p = Some c \<and> NullCap \<noteq> c) \<and> (\<exists>ca. cs c = Some ca \<and> NullCap \<noteq> ca)\<rbrakk> \<Longrightarrow> m p = None proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cs p = Some NullCap; \<forall>p c. m c = Some p \<longrightarrow> (\<exists>c. cs p = Some c \<and> NullCap \<noteq> c) \<and> (\<exists>ca. cs c = Some ca \<and> NullCap \<noteq> ca); m p \<noteq> None\<rbrakk> \<Longrightarrow> m p = None proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma mdb_cte_at_Null_descendants:
  "\<lbrakk> cs p = Some cap.NullCap;
     mdb_cte_at (\<lambda>p. \<exists>c. cs p = Some c \<and> cap.NullCap \<noteq> c) m \<rbrakk>
  \<Longrightarrow> descendants_of p m = {}" apply (simp add: mdb_cte_at_def descendants_of_def) apply clarsimp apply (drule tranclD) apply (clarsimp simp: cdt_parent_of_def) apply (cases p) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cs p = Some NullCap; mdb_cte_at (\<lambda>p. \<exists>c. cs p = Some c \<and> NullCap \<noteq> c) m\<rbrakk> \<Longrightarrow> descendants_of p m = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cs p = Some NullCap; \<forall>a b aa ba. m (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>c. cs (a, b) = Some c \<and> NullCap \<noteq> c) \<and> (\<exists>c. cs (aa, ba) = Some c \<and> NullCap \<noteq> c)\<rbrakk> \<Longrightarrow> \<forall>a b. (p, a, b) \<notin> (cdt_parent_rel m)\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>cs p = Some NullCap; \<forall>a b aa ba. m (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>c. cs (a, b) = Some c \<and> NullCap \<noteq> c) \<and> (\<exists>c. cs (aa, ba) = Some c \<and> NullCap \<noteq> c); m \<Turnstile> p \<rightarrow> (a, b)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>cs p = Some NullCap; \<forall>a b aa ba. m (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>c. cs (a, b) = Some c \<and> NullCap \<noteq> c) \<and> (\<exists>c. cs (aa, ba) = Some c \<and> NullCap \<noteq> c); \<exists>z. m \<Turnstile> p \<leadsto> z \<and> m \<Turnstile> z \<rightarrow>* (a, b)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>cs p = Some NullCap; \<forall>a b aa ba. m (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>c. cs (a, b) = Some c \<and> NullCap \<noteq> c) \<and> (\<exists>c. cs (aa, ba) = Some c \<and> NullCap \<noteq> c); m (aa, ba) = Some p; m \<Turnstile> (aa, ba) \<rightarrow>* (a, b)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba ab bb. \<lbrakk>cs p = Some NullCap; \<forall>a b aa ba. m (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>c. cs (a, b) = Some c \<and> NullCap \<noteq> c) \<and> (\<exists>c. cs (aa, ba) = Some c \<and> NullCap \<noteq> c); m (aa, ba) = Some p; m \<Turnstile> (aa, ba) \<rightarrow>* (a, b); p = (ab, bb)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma (in mdb_insert_abs) parency:
  "(m (dest \<mapsto> src) \<Turnstile> p \<rightarrow> p') =
  (if m \<Turnstile> p \<rightarrow> src \<or> p = src then p' = dest \<or> m \<Turnstile> p \<rightarrow> p' else m \<Turnstile> p \<rightarrow> p')" using descendants_child [where x=p] unfolding descendants_of_def by simp fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m(dest \<mapsto> src) \<Turnstile> p \<rightarrow> p' = (if m \<Turnstile> p \<rightarrow> src \<or> p = src then p' = dest \<or> m \<Turnstile> p \<rightarrow> p' else m \<Turnstile> p \<rightarrow> p') proof (prove)
using this:
descendants_of p (m(dest \<mapsto> src)) = (if src \<in> descendants_of p m \<or> p = src then descendants_of p m \<union> {dest} else descendants_of p m)

goal (1 subgoal):
 1. m(dest \<mapsto> src) \<Turnstile> p \<rightarrow> p' = (if m \<Turnstile> p \<rightarrow> src \<or> p = src then p' = dest \<or> m \<Turnstile> p \<rightarrow> p' else m \<Turnstile> p \<rightarrow> p') proof (prove)
using this:
{q. m(dest \<mapsto> src) \<Turnstile> p \<rightarrow> q} = (if src \<in> {q. m \<Turnstile> p \<rightarrow> q} \<or> p = src then {q. m \<Turnstile> p \<rightarrow> q} \<union> {dest} else {q. m \<Turnstile> p \<rightarrow> q})

goal (1 subgoal):
 1. m(dest \<mapsto> src) \<Turnstile> p \<rightarrow> p' = (if m \<Turnstile> p \<rightarrow> src \<or> p = src then p' = dest \<or> m \<Turnstile> p \<rightarrow> p' else m \<Turnstile> p \<rightarrow> p')
theory CSpace_AI

lemma (in mdb_insert_abs) reply_caps_mdb:
  assumes r: "reply_caps_mdb m cs"
  assumes src: "cs src = Some c"
  assumes d: "is_derived m src cap c"
  shows "reply_caps_mdb (m(dest \<mapsto> src)) (cs(dest \<mapsto> cap))" unfolding reply_caps_mdb_def using r d apply (intro allI impI) apply (simp add: desc neq split: if_split_asm del: split_paired_Ex) apply (fastforce simp: src is_derived_def is_cap_simps cap_master_cap_def) apply (erule(1) reply_caps_mdbE) apply (fastforce dest:m_Some_not_dest) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reply_caps_mdb (m(dest \<mapsto> src)) (cs(dest \<mapsto> cap)) proof (prove)
goal (1 subgoal):
 1. \<forall>ptr t rights. (cs(dest \<mapsto> cap)) ptr = Some (ReplyCap t False rights) \<longrightarrow> (\<exists>ptr' rights'. (m(dest \<mapsto> src)) ptr = Some ptr' \<and> (cs(dest \<mapsto> cap)) ptr' = Some (ReplyCap t True rights')) proof (prove)
using this:
reply_caps_mdb m cs
is_derived m src cap c

goal (1 subgoal):
 1. \<forall>ptr t rights. (cs(dest \<mapsto> cap)) ptr = Some (ReplyCap t False rights) \<longrightarrow> (\<exists>ptr' rights'. (m(dest \<mapsto> src)) ptr = Some ptr' \<and> (cs(dest \<mapsto> cap)) ptr' = Some (ReplyCap t True rights')) proof (prove)
goal (1 subgoal):
 1. \<And>ptr t rights. \<lbrakk>reply_caps_mdb m cs; is_derived m src cap c; (cs(dest \<mapsto> cap)) ptr = Some (ReplyCap t False rights)\<rbrakk> \<Longrightarrow> \<exists>ptr' rights'. (m(dest \<mapsto> src)) ptr = Some ptr' \<and> (cs(dest \<mapsto> cap)) ptr' = Some (ReplyCap t True rights') proof (prove)
goal (2 subgoals):
 1. \<And>ptr t rights. \<lbrakk>reply_caps_mdb m cs; is_derived m src (ReplyCap t False rights) c; ptr = dest; cap = ReplyCap t False rights\<rbrakk> \<Longrightarrow> \<exists>rights'. cs src = Some (ReplyCap t True rights')
 2. \<And>ptr t rights. \<lbrakk>reply_caps_mdb m cs; is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t False rights)\<rbrakk> \<Longrightarrow> \<exists>ptr'. ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> m ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))) proof (prove)
goal (1 subgoal):
 1. \<And>ptr t rights. \<lbrakk>reply_caps_mdb m cs; is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t False rights)\<rbrakk> \<Longrightarrow> \<exists>ptr'. ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> m ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))) proof (prove)
goal (1 subgoal):
 1. \<And>ptr t rights ptra R'. \<lbrakk>is_derived m src cap c; ptr \<noteq> dest; cs ptr = Some (ReplyCap t False rights); m ptr = Some ptra; cs ptra = Some (ReplyCap t True R')\<rbrakk> \<Longrightarrow> \<exists>ptr'. ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> m ptr = Some ptr' \<and> (\<exists>rights'. cs ptr' = Some (ReplyCap t True rights'))) proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma (in mdb_insert_abs) reply_mdb:
  assumes r: "reply_mdb m cs"
  assumes src: "cs src = Some c"
  assumes dst: "cs dest = Some cap.NullCap"
  assumes d: "is_derived m src cap c"
  shows "reply_mdb (m(dest \<mapsto> src)) (cs(dest \<mapsto> cap))" using r unfolding reply_mdb_def by (simp add: reply_caps_mdb reply_masters_mdb src dst d)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reply_mdb (m(dest \<mapsto> src)) (cs(dest \<mapsto> cap)) proof (prove)
using this:
reply_mdb m cs

goal (1 subgoal):
 1. reply_mdb (m(dest \<mapsto> src)) (cs(dest \<mapsto> cap)) proof (prove)
using this:
reply_caps_mdb m cs \<and> reply_masters_mdb m cs

goal (1 subgoal):
 1. reply_caps_mdb (m(dest \<mapsto> src)) (cs(dest \<mapsto> cap)) \<and> reply_masters_mdb (m(dest \<mapsto> src)) (cs(dest \<mapsto> cap))
theory CSpace_AI

lemma (in mdb_insert_abs_sib) reply_mdb_sib:
  assumes r: "reply_mdb m cs"
  assumes src: "cs src = Some c"
  assumes dst: "cs dest = Some cap.NullCap"
  assumes d: "is_derived m src cap c"
  assumes p: "\<not>should_be_parent_of c r cap f"
  assumes rev: "is_master_reply_cap c \<longrightarrow> r"
  shows "reply_mdb n (cs(dest \<mapsto> cap))" using r src dst d p rev unfolding reply_mdb_def by (simp add: reply_caps_mdb_sib reply_masters_mdb_sib)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reply_mdb n (cs(dest \<mapsto> cap)) proof (prove)
using this:
reply_mdb m cs
cs src = Some c
cs dest = Some NullCap
is_derived m src cap c
\<not> should_be_parent_of c r cap f
is_master_reply_cap c \<longrightarrow> r

goal (1 subgoal):
 1. reply_mdb n (cs(dest \<mapsto> cap)) proof (prove)
using this:
reply_caps_mdb m cs \<and> reply_masters_mdb m cs
cs src = Some c
cs dest = Some NullCap
is_derived m src cap c
\<not> should_be_parent_of c r cap f
is_master_reply_cap c \<longrightarrow> r

goal (1 subgoal):
 1. reply_caps_mdb n (cs(dest \<mapsto> cap)) \<and> reply_masters_mdb n (cs(dest \<mapsto> cap))
theory CSpace_AI

lemma not_parent_not_untyped:
  assumes p: "\<not>should_be_parent_of c r c' f" "is_derived m p c' c" "cap_aligned c'"
  assumes r: "is_untyped_cap c \<longrightarrow> r"
  shows "\<not>is_untyped_cap c" using p r apply (clarsimp simp: cap_master_cap_def should_be_parent_of_def is_cap_simps is_derived_def
    split: if_split_asm cap.splits) apply (simp add: cap_aligned_def is_physical_def) apply (elim conjE) apply (drule is_aligned_no_overflow, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> is_untyped_cap c proof (prove)
using this:
\<not> should_be_parent_of c r c' f
is_derived m p c' c
cap_aligned c'
is_untyped_cap c \<longrightarrow> r

goal (1 subgoal):
 1. \<not> is_untyped_cap c proof (prove)
goal (1 subgoal):
 1. \<And>dev ra bits f x24 deva. \<lbrakk>cap_aligned (UntypedCap dev ra bits x24); r; ra \<le> ra + 2 ^ bits - 1 \<longrightarrow> \<not> is_physical (UntypedCap dev ra bits x24); c = UntypedCap dev ra bits f; c' = UntypedCap dev ra bits x24; descendants_of p m = {}; is_derived_arch (UntypedCap dev ra bits x24) (UntypedCap dev ra bits f)\<rbrakk> \<Longrightarrow> dev = (\<not> deva) proof (prove)
goal (1 subgoal):
 1. \<And>dev ra bits f x24 deva. \<lbrakk>is_aligned ra bits \<and> bits < word_bits; r; \<not> ra \<le> ra + 2 ^ bits - 1; c = UntypedCap dev ra bits f; c' = UntypedCap dev ra bits x24; descendants_of p m = {}; is_derived_arch (UntypedCap dev ra bits x24) (UntypedCap dev ra bits f)\<rbrakk> \<Longrightarrow> dev = (\<not> deva) proof (prove)
goal (1 subgoal):
 1. \<And>dev ra bits f x24 deva. \<lbrakk>r; \<not> ra \<le> ra + 2 ^ bits - 1; c = UntypedCap dev ra bits f; c' = UntypedCap dev ra bits x24; descendants_of p m = {}; is_derived_arch (UntypedCap dev ra bits x24) (UntypedCap dev ra bits f); is_aligned ra bits; bits < word_bits\<rbrakk> \<Longrightarrow> dev = (\<not> deva) proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma IRQ_not_derived [simp]:
  "\<not>is_derived m src cap.IRQControlCap cap" by (simp add: is_derived_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> is_derived m src IRQControlCap cap
theory CSpace_AI

lemma update_original_mdb_cte_at:
  "mdb_cte_at (swp (cte_wp_at P) (s\<lparr>is_original_cap := x\<rparr>))
              (cdt (s\<lparr>is_original_cap := x\<rparr>)) =
   mdb_cte_at (swp (cte_wp_at P) s) (cdt s)" by (clarsimp simp:mdb_cte_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdb_cte_at (swp (cte_wp_at P) (s\<lparr>is_original_cap := x\<rparr>)) (cdt (s\<lparr>is_original_cap := x\<rparr>)) = mdb_cte_at (swp (cte_wp_at P) s) (cdt s)
theory CSpace_AI

lemma update_cdt_mdb_cte_at:
  "\<lbrace>\<lambda>s. mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<and>
        (case (f (cdt s)) of Some p \<Rightarrow> cte_wp_at P p s \<and> cte_wp_at P c s
                           | None \<Rightarrow> True)\<rbrace>
   update_cdt (\<lambda>cdt. cdt(c := (f cdt)))
   \<lbrace>\<lambda>xc s. mdb_cte_at (swp (cte_wp_at P) s) (cdt s)\<rbrace>" apply (clarsimp simp: update_cdt_def gets_def get_def set_cdt_def
                        put_def bind_def return_def valid_def) apply (clarsimp simp: mdb_cte_at_def split:option.splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<and> (case f (cdt s) of None \<Rightarrow> True | Some p \<Rightarrow> cte_wp_at P p s \<and> cte_wp_at P c s)\<rbrace> update_cdt (\<lambda>cdt. cdt(c := f cdt)) \<lbrace>\<lambda>xc s. mdb_cte_at (swp (cte_wp_at P) s) (cdt s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at P) s) (cdt s); case f (cdt s) of None \<Rightarrow> True | Some p \<Rightarrow> cte_wp_at P p s \<and> cte_wp_at P c s\<rbrakk> \<Longrightarrow> mdb_cte_at (swp (cte_wp_at P) (s\<lparr>cdt := (cdt s)(c := f (cdt s))\<rparr>)) ((cdt s)(c := f (cdt s))) proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma mdb_cte_at_cte_wp_at:
  "\<lbrakk>mdb_cte_at (swp (cte_wp_at P) s) (cdt s);
    src \<in> dom (cdt s) \<or> src \<in> ran (cdt s)\<rbrakk>
   \<Longrightarrow> cte_wp_at P src s" apply (case_tac src) apply (auto simp:mdb_cte_at_def ran_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdb_cte_at (swp (cte_wp_at P) s) (cdt s); src \<in> dom (cdt s) \<or> src \<in> ran (cdt s)\<rbrakk> \<Longrightarrow> cte_wp_at P src s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>mdb_cte_at (swp (cte_wp_at P) s) (cdt s); src \<in> dom (cdt s) \<or> src \<in> ran (cdt s); src = (a, b)\<rbrakk> \<Longrightarrow> cte_wp_at P src s proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma no_mloop_weaken:
  "\<lbrakk>no_mloop m\<rbrakk> \<Longrightarrow> m a \<noteq> Some a" apply (clarsimp simp:no_mloop_def cdt_parent_rel_def) apply (subgoal_tac "(a,a)\<in> {(x, y). is_cdt_parent m x y}") apply (drule r_into_trancl') apply (drule_tac x = "fst a" in spec) apply (drule_tac x = "snd a" in spec) apply clarsimp apply(simp add:is_cdt_parent_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_mloop m \<Longrightarrow> m a \<noteq> Some a proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>a b. ((a, b), a, b) \<notin> {(x, y). is_cdt_parent m x y}\<^sup>+; m a = Some a\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>a b. ((a, b), a, b) \<notin> {(x, y). is_cdt_parent m x y}\<^sup>+; m a = Some a; (a, a) \<in> {(x, y). is_cdt_parent m x y}\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>\<forall>a b. ((a, b), a, b) \<notin> {(x, y). is_cdt_parent m x y}\<^sup>+; m a = Some a\<rbrakk> \<Longrightarrow> (a, a) \<in> {(x, y). is_cdt_parent m x y} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>a b. ((a, b), a, b) \<notin> {(x, y). is_cdt_parent m x y}\<^sup>+; m a = Some a; (a, a) \<in> {(x, y). is_cdt_parent m x y}\<^sup>+\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>\<forall>a b. ((a, b), a, b) \<notin> {(x, y). is_cdt_parent m x y}\<^sup>+; m a = Some a\<rbrakk> \<Longrightarrow> (a, a) \<in> {(x, y). is_cdt_parent m x y} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m a = Some a; (a, a) \<in> {(x, y). is_cdt_parent m x y}\<^sup>+; \<forall>b. ((fst a, b), fst a, b) \<notin> {(x, y). is_cdt_parent m x y}\<^sup>+\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>\<forall>a b. ((a, b), a, b) \<notin> {(x, y). is_cdt_parent m x y}\<^sup>+; m a = Some a\<rbrakk> \<Longrightarrow> (a, a) \<in> {(x, y). is_cdt_parent m x y} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m a = Some a; (a, a) \<in> {(x, y). is_cdt_parent m x y}\<^sup>+; ((fst a, snd a), fst a, snd a) \<notin> {(x, y). is_cdt_parent m x y}\<^sup>+\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>\<forall>a b. ((a, b), a, b) \<notin> {(x, y). is_cdt_parent m x y}\<^sup>+; m a = Some a\<rbrakk> \<Longrightarrow> (a, a) \<in> {(x, y). is_cdt_parent m x y} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>a b. ((a, b), a, b) \<notin> {(x, y). is_cdt_parent m x y}\<^sup>+; m a = Some a\<rbrakk> \<Longrightarrow> (a, a) \<in> {(x, y). is_cdt_parent m x y} proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma no_mloop_neq:
  "\<lbrakk>no_mloop m;m a = Some b\<rbrakk> \<Longrightarrow> a\<noteq> b" apply (rule ccontr) apply (auto simp:no_mloop_weaken) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_mloop m; m a = Some b\<rbrakk> \<Longrightarrow> a \<noteq> b proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_mloop m; m a = Some b; \<not> a \<noteq> b\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma is_derived_not_Null:
  "is_derived (cdt s) src cap capa \<Longrightarrow> cap \<noteq> cap.NullCap" by (simp add:is_derived_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_derived (cdt s) src cap capa \<Longrightarrow> cap \<noteq> NullCap