kings-crown/FVELER_Isabelle huggingface dataset:
theory CSpace_I

lemma mdb_next_update_other:
  "\<lbrakk> m (x \<mapsto> y) \<turnstile> a \<leadsto> b; x \<noteq> a \<rbrakk> \<Longrightarrow> m \<turnstile> a \<leadsto> b" by (simp add: mdb_next_rel_def mdb_next_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m(x \<mapsto> y) \<turnstile> a \<leadsto> b; x \<noteq> a\<rbrakk> \<Longrightarrow> m \<turnstile> a \<leadsto> b
theory CSpace_I

lemma no_self_loop_next_noloop:
  assumes no_loop: "no_loops m"
  and     lup: "m ptr = Some cte"
  shows   "mdbNext (cteMDBNode cte) \<noteq> ptr" proof - from no_loop have "\<not> m \<turnstile> ptr \<leadsto> ptr" unfolding no_loops_def by - (drule spec, erule contrapos_nn, erule r_into_trancl) thus ?thesis using lup by (simp add: next_unfold') qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdbNext (cteMDBNode cte) \<noteq> ptr proof (state)
goal (1 subgoal):
 1. mdbNext (cteMDBNode cte) \<noteq> ptr proof (chain)
picking this:
no_loops m proof (prove)
using this:
no_loops m

goal (1 subgoal):
 1. (ptr, ptr) \<notin> mdb_next_rel m proof (prove)
using this:
\<forall>c. (c, c) \<notin> (mdb_next_rel m)\<^sup>+

goal (1 subgoal):
 1. (ptr, ptr) \<notin> mdb_next_rel m proof (state)
this:
(ptr, ptr) \<notin> mdb_next_rel m

goal (1 subgoal):
 1. mdbNext (cteMDBNode cte) \<noteq> ptr proof (prove)
using this:
(ptr, ptr) \<notin> mdb_next_rel m

goal (1 subgoal):
 1. mdbNext (cteMDBNode cte) \<noteq> ptr proof (prove)
using this:
(ptr, ptr) \<notin> mdb_next_rel m
m ptr = Some cte

goal (1 subgoal):
 1. mdbNext (cteMDBNode cte) \<noteq> ptr proof (state)
this:
mdbNext (cteMDBNode cte) \<noteq> ptr

goal:
No subgoals!
theory CSpace_I

lemma valid_dlistI [intro?]:
  defines "nxt \<equiv> \<lambda>cte. mdbNext (cteMDBNode cte)"
  and     "prv \<equiv> \<lambda>cte. mdbPrev (cteMDBNode cte)"
  assumes r1: "\<And>p cte. \<lbrakk> m p = Some cte; prv cte \<noteq> 0 \<rbrakk> \<Longrightarrow> \<exists>cte'. m (prv cte) = Some cte' \<and> nxt cte' = p"
  and     r2: "\<And>p cte. \<lbrakk> m p = Some cte; nxt cte \<noteq> 0 \<rbrakk> \<Longrightarrow> \<exists>cte'. m (nxt cte) = Some cte' \<and> prv cte' = p"
  shows   "valid_dlist m" unfolding valid_dlist_def by (auto dest: r1 r2 simp: Let_def prv_def nxt_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_dlist m proof (prove)
goal (1 subgoal):
 1. \<forall>p cte. m p = Some cte \<longrightarrow> (let prev = mdbPrev (cteMDBNode cte); next = mdbNext (cteMDBNode cte) in (prev \<noteq> 0 \<longrightarrow> (\<exists>cte'. m prev = Some cte' \<and> mdbNext (cteMDBNode cte') = p)) \<and> (next \<noteq> 0 \<longrightarrow> (\<exists>cte'. m next = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)))
theory CSpace_I

lemma no_loops_tranclE:
  assumes nl: "no_loops m"
  and    nxt: "m \<turnstile> x \<leadsto>\<^sup>+ y"
  shows   "\<not> m \<turnstile> y \<leadsto>\<^sup>* x" proof assume "m \<turnstile> y \<leadsto>\<^sup>* x" hence "m \<turnstile> x \<leadsto>\<^sup>+ x" using nxt by simp thus False using nl unfolding no_loops_def by auto qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (y, x) \<notin> (mdb_next_rel m)\<^sup>* proof (state)
goal (1 subgoal):
 1. m \<turnstile> y \<leadsto>\<^sup>* x \<Longrightarrow> False proof (state)
this:
m \<turnstile> y \<leadsto>\<^sup>* x

goal (1 subgoal):
 1. m \<turnstile> y \<leadsto>\<^sup>* x \<Longrightarrow> False proof (prove)
using this:
m \<turnstile> y \<leadsto>\<^sup>* x

goal (1 subgoal):
 1. m \<turnstile> x \<leadsto>\<^sup>+ x proof (prove)
using this:
m \<turnstile> y \<leadsto>\<^sup>* x
m \<turnstile> x \<leadsto>\<^sup>+ y

goal (1 subgoal):
 1. m \<turnstile> x \<leadsto>\<^sup>+ x proof (state)
this:
m \<turnstile> x \<leadsto>\<^sup>+ x

goal (1 subgoal):
 1. m \<turnstile> y \<leadsto>\<^sup>* x \<Longrightarrow> False proof (prove)
using this:
m \<turnstile> x \<leadsto>\<^sup>+ x

goal (1 subgoal):
 1. False proof (prove)
using this:
m \<turnstile> x \<leadsto>\<^sup>+ x
no_loops m

goal (1 subgoal):
 1. False proof (prove)
using this:
m \<turnstile> x \<leadsto>\<^sup>+ x
\<forall>c. (c, c) \<notin> (mdb_next_rel m)\<^sup>+

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

goal:
No subgoals!
theory CSpace_I

lemma neg_next_rtrancl_trancl:
  "\<lbrakk> \<not> m \<turnstile> y \<leadsto>\<^sup>* r; m \<turnstile> x \<leadsto> y \<rbrakk> \<Longrightarrow> \<not> m \<turnstile> x \<leadsto>\<^sup>+ r" apply (erule contrapos_nn) apply (drule tranclD) apply (clarsimp simp: next_unfold') done

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

lemma no_0_neq [intro?]:
  "\<lbrakk>m c = Some cte; no_0 m\<rbrakk> \<Longrightarrow> c \<noteq> 0" by (auto simp add: no_0_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m c = Some cte; no_0 m\<rbrakk> \<Longrightarrow> c \<noteq> (0::'b)
theory CSpace_I

lemma no_0_update:
  assumes no0: "no_0 m"
  and     pnz: "p \<noteq> 0"
  shows "no_0 (m(p \<mapsto> cte))" using no0 pnz unfolding no_0_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_0 (m(p \<mapsto> cte)) proof (prove)
using this:
no_0 m
p \<noteq> (0::'a)

goal (1 subgoal):
 1. no_0 (m(p \<mapsto> cte)) proof (prove)
using this:
m (0::'a) = None
p \<noteq> (0::'a)

goal (1 subgoal):
 1. (m(p \<mapsto> cte)) (0::'a) = None
theory CSpace_I

lemma mdb_rtrancl_update_other:
  assumes  upd: "m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>* y"
  and   nopath: "\<not> m \<turnstile> x \<leadsto>\<^sup>* p"
  shows "m \<turnstile> x \<leadsto>\<^sup>* y" using upd proof (cases rule: next_rtrancl_tranclE) case eq thus ?thesis by simp next case trancl thus ?thesis by (auto intro: trancl_into_rtrancl elim: mdb_trancl_update_other [OF _ nopath]) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<turnstile> x \<leadsto>\<^sup>* y proof (prove)
using this:
m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>* y

goal (1 subgoal):
 1. m \<turnstile> x \<leadsto>\<^sup>* y proof (state)
goal (2 subgoals):
 1. x = y \<Longrightarrow> m \<turnstile> x \<leadsto>\<^sup>* y
 2. \<lbrakk>x \<noteq> y; m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> m \<turnstile> x \<leadsto>\<^sup>* y proof (state)
this:
x = y

goal (2 subgoals):
 1. x = y \<Longrightarrow> m \<turnstile> x \<leadsto>\<^sup>* y
 2. \<lbrakk>x \<noteq> y; m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> m \<turnstile> x \<leadsto>\<^sup>* y proof (prove)
using this:
x = y

goal (1 subgoal):
 1. m \<turnstile> x \<leadsto>\<^sup>* y proof (state)
this:
m \<turnstile> x \<leadsto>\<^sup>* y

goal (1 subgoal):
 1. \<lbrakk>x \<noteq> y; m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> m \<turnstile> x \<leadsto>\<^sup>* y proof (state)
goal (1 subgoal):
 1. \<lbrakk>x \<noteq> y; m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> m \<turnstile> x \<leadsto>\<^sup>* y proof (state)
this:
x \<noteq> y
m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>+ y

goal (1 subgoal):
 1. \<lbrakk>x \<noteq> y; m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> m \<turnstile> x \<leadsto>\<^sup>* y proof (prove)
using this:
x \<noteq> y
m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>+ y

goal (1 subgoal):
 1. m \<turnstile> x \<leadsto>\<^sup>* y proof (state)
this:
m \<turnstile> x \<leadsto>\<^sup>* y

goal:
No subgoals!
theory CSpace_I

lemma mdb_rtrancl_other_update:
  assumes upd: "m \<turnstile> x \<leadsto>\<^sup>* y"
  and  nopath: "\<not> m \<turnstile> x \<leadsto>\<^sup>* p"
  shows   "m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>* y" using upd proof (cases rule: next_rtrancl_tranclE) case eq thus ?thesis by simp next case trancl thus ?thesis by (auto intro: trancl_into_rtrancl elim: mdb_trancl_other_update [OF _ nopath]) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>* y proof (prove)
using this:
m \<turnstile> x \<leadsto>\<^sup>* y

goal (1 subgoal):
 1. m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>* y proof (state)
goal (2 subgoals):
 1. x = y \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>* y
 2. \<lbrakk>x \<noteq> y; m \<turnstile> x \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>* y proof (state)
this:
x = y

goal (2 subgoals):
 1. x = y \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>* y
 2. \<lbrakk>x \<noteq> y; m \<turnstile> x \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>* y proof (prove)
using this:
x = y

goal (1 subgoal):
 1. m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>* y proof (state)
this:
m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>* y

goal (1 subgoal):
 1. \<lbrakk>x \<noteq> y; m \<turnstile> x \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>* y proof (state)
goal (1 subgoal):
 1. \<lbrakk>x \<noteq> y; m \<turnstile> x \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>* y proof (state)
this:
x \<noteq> y
m \<turnstile> x \<leadsto>\<^sup>+ y

goal (1 subgoal):
 1. \<lbrakk>x \<noteq> y; m \<turnstile> x \<leadsto>\<^sup>+ y\<rbrakk> \<Longrightarrow> m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>* y proof (prove)
using this:
x \<noteq> y
m \<turnstile> x \<leadsto>\<^sup>+ y

goal (1 subgoal):
 1. m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>* y proof (state)
this:
m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>* y

goal:
No subgoals!
theory CSpace_I

lemma mdb_chain_0_update_0:
  assumes x: "mdbNext (cteMDBNode cte) = 0"
  assumes p: "p \<noteq> 0"
  assumes 0: "no_0 m"
  assumes n: "mdb_chain_0 m"
  shows "mdb_chain_0 (m(p \<mapsto> cte))" using x 0 p apply - apply (rule mdb_chain_0_update [OF _ _ p 0 n]) apply (auto elim: next_rtrancl_tranclE dest: no_0_lhs_trancl) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdb_chain_0 (m(p \<mapsto> cte)) proof (prove)
using this:
mdbNext (cteMDBNode cte) = 0
no_0 m
p \<noteq> 0

goal (1 subgoal):
 1. mdb_chain_0 (m(p \<mapsto> cte)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdbNext (cteMDBNode cte) = 0; no_0 m; p \<noteq> 0\<rbrakk> \<Longrightarrow> mdb_chain_0 (m(p \<mapsto> cte)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>mdbNext (cteMDBNode cte) = 0; no_0 m; p \<noteq> 0\<rbrakk> \<Longrightarrow> m \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* 0
 2. \<lbrakk>mdbNext (cteMDBNode cte) = 0; no_0 m; p \<noteq> 0\<rbrakk> \<Longrightarrow> (mdbNext (cteMDBNode cte), p) \<notin> (mdb_next_rel m)\<^sup>* proof (prove)
goal:
No subgoals!
theory CSpace_I

lemma fresh_virt_cap_class_Physical[simp]:
  "fresh_virt_cap_class PhysicalClass = \<top>" by (rule ext, simp add: fresh_virt_cap_class_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fresh_virt_cap_class PhysicalClass = (\<lambda>_. True)
theory CSpace_I

lemma fresh_virt_cap_classD:
  "\<lbrakk> m x = Some cte; fresh_virt_cap_class C m \<rbrakk>
     \<Longrightarrow> C \<noteq> PhysicalClass \<longrightarrow> capClass (cteCap cte) \<noteq> C" by (auto simp: fresh_virt_cap_class_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m x = Some cte; fresh_virt_cap_class C m\<rbrakk> \<Longrightarrow> C \<noteq> PhysicalClass \<longrightarrow> capClass (cteCap cte) \<noteq> C
theory CSpace_I

lemma capRange_untyped:
  "capRange cap' \<inter> untypedRange cap \<noteq> {} \<Longrightarrow> isUntypedCap cap" by (cases cap, auto simp: isCap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. capRange cap' \<inter> untypedRange cap \<noteq> {} \<Longrightarrow> isUntypedCap cap
theory CSpace_I

lemma capRange_of_untyped [simp]:
  "capRange (UntypedCap d r n f) = untypedRange (UntypedCap d r n f)" by (simp add: capRange_def isCap_simps capUntypedSize_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. capRange (capability.UntypedCap d r n f) = untypedRange (capability.UntypedCap d r n f)
theory CSpace_I

lemma no_mdb_next:
  "\<lbrakk> m p = Some cte; no_mdb cte; valid_dlist m; no_0 m \<rbrakk> \<Longrightarrow> \<not> m \<turnstile> x \<leadsto> p" apply clarsimp apply (frule vdlist_nextD0) apply clarsimp apply assumption apply (clarsimp simp: mdb_prev_def no_mdb_def mdb_next_unfold) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some cte; no_mdb cte; valid_dlist m; no_0 m\<rbrakk> \<Longrightarrow> (x, p) \<notin> mdb_next_rel m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some cte; no_mdb cte; valid_dlist m; no_0 m; m \<turnstile> x \<leadsto> p\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m p = Some cte; no_mdb cte; valid_dlist m; no_0 m; m \<turnstile> x \<leadsto> p\<rbrakk> \<Longrightarrow> p \<noteq> 0
 2. \<lbrakk>m p = Some cte; no_mdb cte; valid_dlist m; no_0 m; m \<turnstile> x \<leadsto> p\<rbrakk> \<Longrightarrow> valid_dlist m
 3. \<lbrakk>m p = Some cte; no_mdb cte; valid_dlist m; no_0 m; m \<turnstile> x \<leadsto> p; m \<turnstile> x \<leftarrow> p\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m p = Some cte; no_mdb cte; valid_dlist m; no_0 m; m \<turnstile> x \<leadsto> p\<rbrakk> \<Longrightarrow> valid_dlist m
 2. \<lbrakk>m p = Some cte; no_mdb cte; valid_dlist m; no_0 m; m \<turnstile> x \<leadsto> p; m \<turnstile> x \<leftarrow> p\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some cte; no_mdb cte; valid_dlist m; no_0 m; m \<turnstile> x \<leadsto> p; m \<turnstile> x \<leftarrow> p\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory CSpace_I

lemma no_mdb_rtrancl:
  "\<lbrakk> m p = Some cte; no_mdb cte; p \<noteq> x; valid_dlist m; no_0 m \<rbrakk> \<Longrightarrow> \<not> m \<turnstile> x \<leadsto>\<^sup>* p" apply (clarsimp dest!: rtranclD) apply (drule tranclD2) apply clarsimp apply (drule (3) no_mdb_next) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some cte; no_mdb cte; p \<noteq> x; valid_dlist m; no_0 m\<rbrakk> \<Longrightarrow> (x, p) \<notin> (mdb_next_rel m)\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some cte; no_mdb cte; p \<noteq> x; valid_dlist m; no_0 m; m \<turnstile> x \<leadsto>\<^sup>+ p\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some cte; no_mdb cte; p \<noteq> x; valid_dlist m; no_0 m; \<exists>z. m \<turnstile> x \<leadsto>\<^sup>* z \<and> m \<turnstile> z \<leadsto> p\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>m p = Some cte; no_mdb cte; p \<noteq> x; valid_dlist m; no_0 m; m \<turnstile> x \<leadsto>\<^sup>* z; m \<turnstile> z \<leadsto> p\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>no_mdb cte; p \<noteq> x; valid_dlist m; no_0 m; m \<turnstile> x \<leadsto>\<^sup>* z; m \<turnstile> z \<leadsto> p; (?x6 z, p) \<notin> mdb_next_rel m\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory CSpace_I

lemma isNullCap [simp]:
  "isNullCap cap = (cap = NullCap)" by (simp add: isCap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isNullCap cap = (cap = capability.NullCap)
theory CSpace_I

lemma isDomainCap [simp]:
  "isDomainCap cap = (cap = DomainCap)" by (simp add: isCap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isDomainCap cap = (cap = capability.DomainCap)
theory CSpace_I

lemma capBadge_simps[simp]:
 "capBadge (UntypedCap d p n f)               = None"
 "capBadge (NullCap)                          = None"
 "capBadge (DomainCap)                        = None"
 "capBadge (EndpointCap ref badge s r g gr)   = Some badge"
 "capBadge (NotificationCap ref badge s r)    = Some badge"
 "capBadge (CNodeCap ref bits gd gs)          = None"
 "capBadge (ThreadCap ref)                    = None"
 "capBadge (Zombie ref b n)                   = None"
 "capBadge (ArchObjectCap cap)                = None"
 "capBadge (IRQControlCap)                    = None"
 "capBadge (IRQHandlerCap irq)                = None"
 "capBadge (ReplyCap tcb master g)            = None" by (simp add: capBadge_def isCap_defs)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((capBadge (capability.UntypedCap d p n f) = None &&& capBadge capability.NullCap = None &&& capBadge capability.DomainCap = None) &&& capBadge (capability.EndpointCap ref badge s r g gr) = Some badge &&& capBadge (capability.NotificationCap ref badge s r) = Some badge &&& capBadge (capability.CNodeCap ref bits gd gs) = None) &&& (capBadge (capability.ThreadCap ref) = None &&& capBadge (capability.Zombie ref b n) = None &&& capBadge (capability.ArchObjectCap cap) = None) &&& capBadge capability.IRQControlCap = None &&& capBadge (capability.IRQHandlerCap irq) = None &&& capBadge (capability.ReplyCap tcb master g) = None
theory CSpace_I

lemma capClass_Master:
  "capClass (capMasterCap cap) = capClass cap" by (simp add: capMasterCap_def split: capability.split arch_capability.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. capClass (capMasterCap cap) = capClass cap
theory CSpace_I

lemma capRange_Master:
  "capRange (capMasterCap cap) = capRange cap" by (simp add: capMasterCap_def split: capability.split arch_capability.split,
      simp add: capRange_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. capRange (capMasterCap cap) = capRange cap
theory CSpace_I

lemma master_eqI:
  "\<lbrakk> \<And>cap. F (capMasterCap cap) = F cap; F (capMasterCap cap) = F (capMasterCap cap') \<rbrakk>
     \<Longrightarrow> F cap = F cap'" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>cap. F (capMasterCap cap) = F cap; F (capMasterCap cap) = F (capMasterCap cap')\<rbrakk> \<Longrightarrow> F cap = F cap'
theory CSpace_I

lemma isCap_Master:
  "isZombie (capMasterCap cap) = isZombie cap"
  "isArchObjectCap (capMasterCap cap) = isArchObjectCap cap"
  "isThreadCap (capMasterCap cap) = isThreadCap cap"
  "isCNodeCap (capMasterCap cap) = isCNodeCap cap"
  "isNotificationCap (capMasterCap cap) = isNotificationCap cap"
  "isEndpointCap (capMasterCap cap) = isEndpointCap cap"
  "isUntypedCap (capMasterCap cap) = isUntypedCap cap"
  "isReplyCap (capMasterCap cap) = isReplyCap cap"
  "isIRQControlCap (capMasterCap cap) = isIRQControlCap cap"
  "isIRQHandlerCap (capMasterCap cap) = isIRQHandlerCap cap"
  "isNullCap (capMasterCap cap) = isNullCap cap"
  "isDomainCap (capMasterCap cap) = isDomainCap cap"
  "isArchPageCap (capMasterCap cap) = isArchPageCap cap" by (simp add: isCap_simps capMasterCap_def
         split: capability.split arch_capability.split)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((isZombie (capMasterCap cap) = isZombie cap &&& isArchObjectCap (capMasterCap cap) = isArchObjectCap cap &&& isThreadCap (capMasterCap cap) = isThreadCap cap) &&& isCNodeCap (capMasterCap cap) = isCNodeCap cap &&& isNotificationCap (capMasterCap cap) = isNotificationCap cap &&& isEndpointCap (capMasterCap cap) = isEndpointCap cap) &&& (isUntypedCap (capMasterCap cap) = isUntypedCap cap &&& isReplyCap (capMasterCap cap) = isReplyCap cap &&& isIRQControlCap (capMasterCap cap) = isIRQControlCap cap) &&& (isIRQHandlerCap (capMasterCap cap) = isIRQHandlerCap cap &&& isNullCap (capMasterCap cap) = isNullCap cap) &&& isDomainCap (capMasterCap cap) = isDomainCap cap &&& isArchPageCap (capMasterCap cap) = isArchPageCap cap
theory CSpace_I

lemma capUntypedSize_capBits:
  "capClass cap = PhysicalClass \<Longrightarrow> capUntypedSize cap = 2 ^ (capBits cap)" apply (simp add: capUntypedSize_def objBits_simps
                   ARM_H.capUntypedSize_def
                   pteBits_def pdeBits_def
                   ptBits_def pdBits_def
                   shiftl_eq_mult
            split: capability.splits arch_capability.splits
                   zombie_type.splits) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. capClass cap = PhysicalClass \<Longrightarrow> global.capUntypedSize cap = 2 ^ capBits cap proof (prove)
goal (1 subgoal):
 1. capClass cap = PhysicalClass \<Longrightarrow> cap \<noteq> capability.NullCap proof (prove)
goal:
No subgoals!
theory CSpace_I

lemma sameRegionAsE:
  "\<lbrakk> sameRegionAs cap cap';
     \<lbrakk> capMasterCap cap = capMasterCap cap'; \<not> isNullCap cap; \<not> isZombie cap;
         \<not> isUntypedCap cap; \<not> isArchPageCap cap \<rbrakk> \<Longrightarrow> R;
     \<lbrakk> capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isUntypedCap cap \<rbrakk> \<Longrightarrow> R;
     \<lbrakk> capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isArchPageCap cap;
          isArchPageCap cap' \<rbrakk> \<Longrightarrow> R;
     \<lbrakk> isIRQControlCap cap; isIRQHandlerCap cap' \<rbrakk> \<Longrightarrow> R
      \<rbrakk> \<Longrightarrow> R" by (simp add: sameRegionAs_def3, fastforce)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>global.sameRegionAs cap cap'; \<lbrakk>capMasterCap cap = capMasterCap cap'; \<not> isNullCap cap; \<not> isZombie cap; \<not> isUntypedCap cap; \<not> isArchPageCap cap\<rbrakk> \<Longrightarrow> R; \<lbrakk>capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isUntypedCap cap\<rbrakk> \<Longrightarrow> R; \<lbrakk>capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isArchPageCap cap; isArchPageCap cap'\<rbrakk> \<Longrightarrow> R; \<lbrakk>isIRQControlCap cap; isIRQHandlerCap cap'\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R
theory CSpace_I

lemma sameObjectAsE:
  "\<lbrakk> sameObjectAs cap cap';
     \<lbrakk> capMasterCap cap = capMasterCap cap'; \<not> isNullCap cap; \<not> isZombie cap;
         \<not> isUntypedCap cap;
         isArchPageCap cap \<Longrightarrow> capRange cap \<noteq> {} \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R" by (clarsimp simp add: sameObjectAs_def3)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>global.sameObjectAs cap cap'; \<lbrakk>capMasterCap cap = capMasterCap cap'; \<not> isNullCap cap; \<not> isZombie cap; \<not> isUntypedCap cap; isArchPageCap cap \<Longrightarrow> capRange cap \<noteq> {}\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R
theory CSpace_I

lemma sameObjectAs_sameRegionAs:
  "sameObjectAs cap cap' \<Longrightarrow> sameRegionAs cap cap'" by (clarsimp simp add: sameObjectAs_def2 sameRegionAs_def2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. global.sameObjectAs cap cap' \<Longrightarrow> global.sameRegionAs cap cap'
theory CSpace_I

lemma sameObjectAs_sym:
  "sameObjectAs c d = sameObjectAs d c" by (simp add: sameObjectAs_def2 eq_commute conj_comms)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. global.sameObjectAs c d = global.sameObjectAs d c
theory CSpace_I

lemma untypedRange_Master:
  "untypedRange (capMasterCap cap) = untypedRange cap" by (simp add: capMasterCap_def split: capability.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. untypedRange (capMasterCap cap) = untypedRange cap
theory CSpace_I

lemma sameRegionAs_Null [simp]:
  "sameRegionAs c NullCap = False"
  "sameRegionAs NullCap c = False" by (simp add: sameRegionAs_def3 capRange_def isCap_simps)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. global.sameRegionAs c capability.NullCap = False &&& global.sameRegionAs capability.NullCap c = False