kings-crown/FVELER_Isabelle huggingface dataset:
theory Helpers_SD

lemma capless_at_def2:
  "capless_at p s = object_at (\<lambda>obj. \<not> (has_slots obj)) p s" apply (clarsimp simp: has_slots_def object_at_def) apply (fastforce simp: is_untyped_def is_ep_def is_ntfn_def is_frame_def
                 split: cdl_object.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. capless_at p s = object_at (\<lambda>obj. \<not> has_slots obj) p s proof (prove)
goal (1 subgoal):
 1. ((\<exists>object. cdl_objects s p = Some object \<and> is_untyped object) \<or> (\<exists>object. cdl_objects s p = Some object \<and> is_ep object) \<or> (\<exists>object. cdl_objects s p = Some object \<and> is_ntfn object) \<or> (\<exists>object. cdl_objects s p = Some object \<and> is_frame object)) = (\<exists>object. cdl_objects s p = Some object \<and> \<not> (case object of Endpoint \<Rightarrow> False | Notification \<Rightarrow> False | Frame cdl_frame_ext \<Rightarrow> False | Untyped \<Rightarrow> False | _ \<Rightarrow> True)) proof (prove)
goal:
No subgoals!
theory Helpers_SD

lemma ko_at_tcb_at:
  "ko_at (Tcb t) p s \<Longrightarrow> tcb_at p s" by (simp add: object_at_def is_tcb_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ko_at (Tcb t) p s \<Longrightarrow> tcb_at p s
theory Helpers_SD

lemma length_used_irq_list [simp]:
  "length (used_irq_list spec) = card (used_irqs spec)" by (clarsimp simp: used_irq_list_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length (used_irq_list spec) = card (used_irqs spec)
theory Helpers_SD

lemma distinct_used_irq_list [simp]:
  "distinct (used_irq_list spec)" by (simp add: used_irq_list_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. distinct (used_irq_list spec)
theory Helpers_SD

lemma set_used_irq_list [simp]:
  "set (used_irq_list spec) = used_irqs spec" by (simp add: used_irq_list_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set (used_irq_list spec) = used_irqs spec
theory Helpers_SD

lemma object_type_is_object:
  "is_untyped obj  = (object_type obj = UntypedType)"
  "is_ep obj       = (object_type obj = EndpointType)"
  "is_ntfn obj      = (object_type obj = NotificationType)"
  "is_tcb obj      = (object_type obj = TcbType)"
  "is_cnode obj    = (object_type obj = CNodeType)"
  "is_irq_node obj = (object_type obj = IRQNodeType)"
  "is_asidpool obj = (object_type obj = AsidPoolType)"
  "is_pt obj       = (object_type obj = PageTableType)"
  "is_pd obj       = (object_type obj = PageDirectoryType)"
  "is_frame obj    = (\<exists>n. object_type obj = FrameType n)" by (simp_all add: object_type_def is_untyped_def is_ep_def is_ntfn_def is_tcb_def
                    is_cnode_def is_irq_node_def is_asidpool_def is_pt_def is_pd_def is_frame_def
             split: cdl_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((is_untyped obj = (object_type obj = UntypedType) &&& is_ep obj = (object_type obj = EndpointType)) &&& is_ntfn obj = (object_type obj = NotificationType) &&& is_tcb obj = (object_type obj = TcbType) &&& is_cnode obj = (object_type obj = CNodeType)) &&& (is_irq_node obj = (object_type obj = IRQNodeType) &&& is_asidpool obj = (object_type obj = AsidPoolType)) &&& is_pt obj = (object_type obj = PageTableType) &&& is_pd obj = (object_type obj = PageDirectoryType) &&& is_frame obj = (\<exists>n. object_type obj = FrameType n)
theory Helpers_SD

lemma is_ptD[dest]: "is_pt obj \<Longrightarrow> \<exists>x. obj = PageTable x" by (clarsimp simp: is_pt_def split: cdl_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_pt obj \<Longrightarrow> \<exists>x. obj = PageTable x
theory Helpers_SD

lemma object_at_object_type:
  "\<lbrakk>cdl_objects spec obj_id = Some obj; untyped_at obj_id spec\<rbrakk> \<Longrightarrow> object_type obj = UntypedType"
  "\<lbrakk>cdl_objects spec obj_id = Some obj; ep_at obj_id spec\<rbrakk> \<Longrightarrow> object_type obj = EndpointType"
  "\<lbrakk>cdl_objects spec obj_id = Some obj; ntfn_at obj_id spec\<rbrakk> \<Longrightarrow> object_type obj = NotificationType"
  "\<lbrakk>cdl_objects spec obj_id = Some obj; tcb_at obj_id spec\<rbrakk> \<Longrightarrow> object_type obj = TcbType"
  "\<lbrakk>cdl_objects spec obj_id = Some obj; cnode_at obj_id spec\<rbrakk> \<Longrightarrow> object_type obj = CNodeType"
  "\<lbrakk>cdl_objects spec obj_id = Some obj; irq_node_at obj_id spec\<rbrakk> \<Longrightarrow> object_type obj = IRQNodeType"
  "\<lbrakk>cdl_objects spec obj_id = Some obj; asidpool_at obj_id spec\<rbrakk> \<Longrightarrow> object_type obj = AsidPoolType"
  "\<lbrakk>cdl_objects spec obj_id = Some obj; pt_at obj_id spec\<rbrakk> \<Longrightarrow> object_type obj = PageTableType"
  "\<lbrakk>cdl_objects spec obj_id = Some obj; pd_at obj_id spec\<rbrakk> \<Longrightarrow> object_type obj = PageDirectoryType"
  "\<lbrakk>cdl_objects spec obj_id = Some obj; frame_at obj_id spec\<rbrakk> \<Longrightarrow> \<exists>n. object_type obj = FrameType n" by (simp_all add: object_at_def object_type_is_object)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (((\<lbrakk>cdl_objects spec obj_id = Some obj; untyped_at obj_id spec\<rbrakk> \<Longrightarrow> object_type obj = UntypedType) &&& (\<lbrakk>cdl_objects spec obj_id = Some obj; ep_at obj_id spec\<rbrakk> \<Longrightarrow> object_type obj = EndpointType)) &&& (\<lbrakk>cdl_objects spec obj_id = Some obj; ntfn_at obj_id spec\<rbrakk> \<Longrightarrow> object_type obj = NotificationType) &&& (\<lbrakk>cdl_objects spec obj_id = Some obj; tcb_at obj_id spec\<rbrakk> \<Longrightarrow> object_type obj = TcbType) &&& (\<lbrakk>cdl_objects spec obj_id = Some obj; cnode_at obj_id spec\<rbrakk> \<Longrightarrow> object_type obj = CNodeType)) &&& ((\<lbrakk>cdl_objects spec obj_id = Some obj; irq_node_at obj_id spec\<rbrakk> \<Longrightarrow> object_type obj = IRQNodeType) &&& (\<lbrakk>cdl_objects spec obj_id = Some obj; asidpool_at obj_id spec\<rbrakk> \<Longrightarrow> object_type obj = AsidPoolType)) &&& (\<lbrakk>cdl_objects spec obj_id = Some obj; pt_at obj_id spec\<rbrakk> \<Longrightarrow> object_type obj = PageTableType) &&& (\<lbrakk>cdl_objects spec obj_id = Some obj; pd_at obj_id spec\<rbrakk> \<Longrightarrow> object_type obj = PageDirectoryType) &&& (\<lbrakk>cdl_objects spec obj_id = Some obj; frame_at obj_id spec\<rbrakk> \<Longrightarrow> \<exists>n. object_type obj = FrameType n)
theory Helpers_SD

lemma object_type_object_at:
  "\<lbrakk>cdl_objects spec obj_id = Some obj; object_type obj = UntypedType\<rbrakk> \<Longrightarrow> untyped_at obj_id spec"
  "\<lbrakk>cdl_objects spec obj_id = Some obj; object_type obj = EndpointType\<rbrakk> \<Longrightarrow> ep_at obj_id spec"
  "\<lbrakk>cdl_objects spec obj_id = Some obj; object_type obj = NotificationType\<rbrakk> \<Longrightarrow> ntfn_at obj_id spec"
  "\<lbrakk>cdl_objects spec obj_id = Some obj; object_type obj = TcbType\<rbrakk> \<Longrightarrow> tcb_at obj_id spec"
  "\<lbrakk>cdl_objects spec obj_id = Some obj; object_type obj = CNodeType\<rbrakk> \<Longrightarrow> cnode_at obj_id spec"
  "\<lbrakk>cdl_objects spec obj_id = Some obj; object_type obj = IRQNodeType\<rbrakk> \<Longrightarrow> irq_node_at obj_id spec"
  "\<lbrakk>cdl_objects spec obj_id = Some obj; object_type obj = AsidPoolType\<rbrakk> \<Longrightarrow> asidpool_at obj_id spec"
  "\<lbrakk>cdl_objects spec obj_id = Some obj; object_type obj = PageTableType\<rbrakk> \<Longrightarrow> pt_at obj_id spec"
  "\<lbrakk>cdl_objects spec obj_id = Some obj; object_type obj = PageDirectoryType\<rbrakk> \<Longrightarrow> pd_at obj_id spec" by (simp_all add: object_at_def object_type_is_object)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (((\<lbrakk>cdl_objects spec obj_id = Some obj; object_type obj = UntypedType\<rbrakk> \<Longrightarrow> untyped_at obj_id spec) &&& (\<lbrakk>cdl_objects spec obj_id = Some obj; object_type obj = EndpointType\<rbrakk> \<Longrightarrow> ep_at obj_id spec)) &&& (\<lbrakk>cdl_objects spec obj_id = Some obj; object_type obj = NotificationType\<rbrakk> \<Longrightarrow> ntfn_at obj_id spec) &&& (\<lbrakk>cdl_objects spec obj_id = Some obj; object_type obj = TcbType\<rbrakk> \<Longrightarrow> tcb_at obj_id spec)) &&& ((\<lbrakk>cdl_objects spec obj_id = Some obj; object_type obj = CNodeType\<rbrakk> \<Longrightarrow> cnode_at obj_id spec) &&& (\<lbrakk>cdl_objects spec obj_id = Some obj; object_type obj = IRQNodeType\<rbrakk> \<Longrightarrow> irq_node_at obj_id spec)) &&& (\<lbrakk>cdl_objects spec obj_id = Some obj; object_type obj = AsidPoolType\<rbrakk> \<Longrightarrow> asidpool_at obj_id spec) &&& (\<lbrakk>cdl_objects spec obj_id = Some obj; object_type obj = PageTableType\<rbrakk> \<Longrightarrow> pt_at obj_id spec) &&& (\<lbrakk>cdl_objects spec obj_id = Some obj; object_type obj = PageDirectoryType\<rbrakk> \<Longrightarrow> pd_at obj_id spec)
theory Helpers_SD

lemma set_object_type [simp]:
  "{obj_id \<in> dom (cdl_objects spec). object_at P obj_id spec} = {obj_id. object_at P obj_id spec}"
  "{obj_id \<in> dom (cdl_objects spec). table_at obj_id spec} = {obj_id. table_at obj_id spec}"
  "{obj_id \<in> dom (cdl_objects spec). capless_at obj_id spec} = {obj_id. capless_at obj_id spec}"
  "{obj_id \<in> dom (cdl_objects spec). cnode_or_tcb_at obj_id spec} = {obj_id. cnode_or_tcb_at obj_id spec}"
  "{obj_id \<in> dom (cdl_objects spec). cnode_at obj_id spec} = {obj_id. cnode_at obj_id spec}"
  "{obj_id \<in> dom (cdl_objects spec). real_object_at obj_id spec} = {obj_id. real_object_at obj_id spec}" by (auto simp: object_at_def real_object_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ({obj_id \<in> dom (cdl_objects spec). object_at P obj_id spec} = {obj_id. object_at P obj_id spec} &&& {obj_id \<in> dom (cdl_objects spec). table_at obj_id spec} = {obj_id. table_at obj_id spec} &&& {obj_id \<in> dom (cdl_objects spec). capless_at obj_id spec} = {obj_id. capless_at obj_id spec}) &&& {obj_id \<in> dom (cdl_objects spec). cnode_or_tcb_at obj_id spec} = {obj_id. cnode_or_tcb_at obj_id spec} &&& {obj_id \<in> dom (cdl_objects spec). cnode_at obj_id spec} = {obj_id. cnode_at obj_id spec} &&& {obj_id \<in> dom (cdl_objects spec). real_object_at obj_id spec} = {obj_id. real_object_at obj_id spec}
theory Helpers_SD

lemma cnode_or_tcb_at_simps:
  "(cnode_or_tcb_at obj_id spec \<and> cnode_at obj_id spec) = cnode_at obj_id spec"
  "(cnode_or_tcb_at obj_id spec \<and> \<not> cnode_at obj_id spec) = tcb_at obj_id spec" by (auto simp: object_at_def object_type_is_object)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (cnode_or_tcb_at obj_id spec \<and> cnode_at obj_id spec) = cnode_at obj_id spec &&& (cnode_or_tcb_at obj_id spec \<and> \<not> cnode_at obj_id spec) = tcb_at obj_id spec
theory Helpers_SD

lemma is_fake_pt_cap_is_pt_cap [elim!]:
  "is_fake_pt_cap cap \<Longrightarrow> is_pt_cap cap" by (clarsimp simp: is_fake_pt_cap_def split: cdl_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_fake_pt_cap cap \<Longrightarrow> is_pt_cap cap
theory Helpers_SD

lemma is_cnode_cap_simps:
  "is_cnode_cap (UntypedCap dev ids ids') = False"
  "is_cnode_cap (IOPageTableCap x) = False"
  "is_cnode_cap (IOSpaceCap x) = False"
  "is_cnode_cap (IOPortsCap x a) = False"
  "is_cnode_cap (AsidPoolCap x b) = False"
  "is_cnode_cap (PageDirectoryCap x c d) = False"
  "is_cnode_cap (PageTableCap x e f) = False"
  "is_cnode_cap (FrameCap dev x g h i j) = False"
  "is_cnode_cap (TcbCap x) = False"
  "is_cnode_cap (MasterReplyCap x) = False"
  "is_cnode_cap (ReplyCap x q) = False"
  "is_cnode_cap (NotificationCap x m n) = False"
  "is_cnode_cap (EndpointCap x p q) = False"
  "is_cnode_cap (ZombieCap x) = False"
  "is_cnode_cap (PendingSyncSendCap x s t u v w) = False"
  "is_cnode_cap (PendingSyncRecvCap x t w) = False"
  "is_cnode_cap (PendingNtfnRecvCap x) = False"

  "is_cnode_cap (CNodeCap x k l sz) = True" by (unfold cap_type_def, simp_all split: cdl_object_type.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (((is_cnode_cap (UntypedCap dev ids ids') = False &&& is_cnode_cap (IOPageTableCap x) = False) &&& is_cnode_cap (IOSpaceCap x) = False &&& is_cnode_cap (IOPortsCap x a) = False) &&& (is_cnode_cap (AsidPoolCap x b) = False &&& is_cnode_cap (PageDirectoryCap x c d) = False) &&& is_cnode_cap (PageTableCap x e f) = False &&& is_cnode_cap (FrameCap dev x g h i j) = False &&& is_cnode_cap (TcbCap x) = False) &&& ((is_cnode_cap (MasterReplyCap x) = False &&& is_cnode_cap (ReplyCap x q) = False) &&& is_cnode_cap (NotificationCap x m n) = False &&& is_cnode_cap (EndpointCap x p q) = False) &&& (is_cnode_cap (ZombieCap x) = False &&& is_cnode_cap (PendingSyncSendCap x s t u v w) = False) &&& is_cnode_cap (PendingSyncRecvCap x t w) = False &&& is_cnode_cap (PendingNtfnRecvCap x) = False &&& is_cnode_cap (CNodeCap x k l sz) = True
theory Helpers_SD

lemma default_cap_eq:
  "\<lbrakk>is_default_cap cap; is_default_cap cap';
    cap_type cap = cap_type cap'; cap_objects cap = cap_objects cap';
    cnode_cap_size cap = cnode_cap_size cap';
    cap_irq cap = cap_irq cap'; is_device_cap cap = is_device_cap cap'\<rbrakk>
  \<Longrightarrow> cap = cap'" by (auto simp: is_default_cap_def cap_type_def cap_irq_def default_cap_def
          split: cdl_cap.splits )

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_default_cap cap; is_default_cap cap'; cap_type cap = cap_type cap'; cap_objects cap = cap_objects cap'; cnode_cap_size cap = cnode_cap_size cap'; cap_irq cap = cap_irq cap'; is_device_cap cap = is_device_cap cap'\<rbrakk> \<Longrightarrow> cap = cap'
theory Helpers_SD

lemma cnode_cap_size_non_cnode [simp]:
  "\<not> is_cnode_cap cap \<Longrightarrow> cnode_cap_size cap = 0" by (clarsimp simp: cap_type_def cnode_cap_size_def split: cdl_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_type cap \<noteq> Some CNodeType \<Longrightarrow> cnode_cap_size cap = 0
theory Helpers_SD

lemma irqhandler_cap_irq_non_irqhandler [simp]:
  "\<not> is_irqhandler_cap cap \<Longrightarrow> cap_irq cap = undefined" by (clarsimp simp: cap_irq_def split: cdl_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_type cap \<noteq> Some IRQNodeType \<Longrightarrow> cap_irq cap = undefined
theory Helpers_SD

lemma default_cap_eq_non_cnode:
  "\<lbrakk>is_default_cap cap; is_default_cap cap';
   \<not> is_cnode_cap cap; \<not> is_irqhandler_cap cap;
    cap_type cap = cap_type cap'; cap_objects cap = cap_objects cap';
    is_device_cap cap = is_device_cap cap'\<rbrakk>
  \<Longrightarrow> cap = cap'" apply (rule default_cap_eq) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_default_cap cap; is_default_cap cap'; cap_type cap \<noteq> Some CNodeType; cap_type cap \<noteq> Some IRQNodeType; cap_type cap = cap_type cap'; cap_objects cap = cap_objects cap'; is_device_cap cap = is_device_cap cap'\<rbrakk> \<Longrightarrow> cap = cap' proof (prove)
goal (7 subgoals):
 1. \<lbrakk>is_default_cap cap; is_default_cap cap'; cap_type cap \<noteq> Some CNodeType; cap_type cap \<noteq> Some IRQNodeType; cap_type cap = cap_type cap'; cap_objects cap = cap_objects cap'; is_device_cap cap = is_device_cap cap'\<rbrakk> \<Longrightarrow> is_default_cap cap
 2. \<lbrakk>is_default_cap cap; is_default_cap cap'; cap_type cap \<noteq> Some CNodeType; cap_type cap \<noteq> Some IRQNodeType; cap_type cap = cap_type cap'; cap_objects cap = cap_objects cap'; is_device_cap cap = is_device_cap cap'\<rbrakk> \<Longrightarrow> is_default_cap cap'
 3. \<lbrakk>is_default_cap cap; is_default_cap cap'; cap_type cap \<noteq> Some CNodeType; cap_type cap \<noteq> Some IRQNodeType; cap_type cap = cap_type cap'; cap_objects cap = cap_objects cap'; is_device_cap cap = is_device_cap cap'\<rbrakk> \<Longrightarrow> cap_type cap = cap_type cap'
 4. \<lbrakk>is_default_cap cap; is_default_cap cap'; cap_type cap \<noteq> Some CNodeType; cap_type cap \<noteq> Some IRQNodeType; cap_type cap = cap_type cap'; cap_objects cap = cap_objects cap'; is_device_cap cap = is_device_cap cap'\<rbrakk> \<Longrightarrow> cap_objects cap = cap_objects cap'
 5. \<lbrakk>is_default_cap cap; is_default_cap cap'; cap_type cap \<noteq> Some CNodeType; cap_type cap \<noteq> Some IRQNodeType; cap_type cap = cap_type cap'; cap_objects cap = cap_objects cap'; is_device_cap cap = is_device_cap cap'\<rbrakk> \<Longrightarrow> cnode_cap_size cap = cnode_cap_size cap'
 6. \<lbrakk>is_default_cap cap; is_default_cap cap'; cap_type cap \<noteq> Some CNodeType; cap_type cap \<noteq> Some IRQNodeType; cap_type cap = cap_type cap'; cap_objects cap = cap_objects cap'; is_device_cap cap = is_device_cap cap'\<rbrakk> \<Longrightarrow> cap_irq cap = cap_irq cap'
 7. \<lbrakk>is_default_cap cap; is_default_cap cap'; cap_type cap \<noteq> Some CNodeType; cap_type cap \<noteq> Some IRQNodeType; cap_type cap = cap_type cap'; cap_objects cap = cap_objects cap'; is_device_cap cap = is_device_cap cap'\<rbrakk> \<Longrightarrow> is_device_cap cap = is_device_cap cap' proof (prove)
goal:
No subgoals!
theory Helpers_SD

lemma cap_type_default_cap [simp]:
  "cap_type (default_cap type {obj_id} sz dev) = Some type" by (clarsimp simp: default_cap_def cap_type_def split: cdl_object_type.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_type (default_cap type {obj_id} sz dev) = Some type
theory Helpers_SD

lemma is_tcb_update_slots [simp]:
  "is_tcb (update_slots slots obj) = is_tcb obj" by (clarsimp simp: is_tcb_def update_slots_def split: cdl_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_tcb (update_slots slots obj) = is_tcb obj
theory Helpers_SD

lemma tcb_has_slots [elim!]:
  "is_tcb obj \<Longrightarrow> has_slots obj" by (clarsimp simp: is_tcb_def has_slots_def split: cdl_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_tcb obj \<Longrightarrow> has_slots obj
theory Helpers_SD

lemma cnode_has_slots [elim!]:
  "is_cnode obj \<Longrightarrow> has_slots obj" by (clarsimp simp: is_cnode_def has_slots_def split: cdl_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_cnode obj \<Longrightarrow> has_slots obj
theory Helpers_SD

lemma pt_has_slots [elim!]:
  "is_pt obj \<Longrightarrow> has_slots obj" by (clarsimp simp: is_pt_def has_slots_def split: cdl_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_pt obj \<Longrightarrow> has_slots obj
theory Helpers_SD

lemma pd_has_slots [elim!]:
  "is_pd obj \<Longrightarrow> has_slots obj" by (clarsimp simp: is_pd_def has_slots_def split: cdl_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_pd obj \<Longrightarrow> has_slots obj
theory Helpers_SD

lemma asidpool_has_slots [elim!]:
  "is_asidpool obj \<Longrightarrow> has_slots obj" by (clarsimp simp: is_asidpool_def has_slots_def split: cdl_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_asidpool obj \<Longrightarrow> has_slots obj
theory Helpers_SD

lemma object_type_has_slots [elim!]:
  "object_type obj = TcbType \<Longrightarrow> has_slots obj"
  "object_type obj = CNodeType \<Longrightarrow> has_slots obj"
  "object_type obj = IRQNodeType \<Longrightarrow> has_slots obj"
  "object_type obj = PageTableType \<Longrightarrow> has_slots obj"
  "object_type obj = PageDirectoryType \<Longrightarrow> has_slots obj"
  "object_type obj = AsidPoolType \<Longrightarrow> has_slots obj" by (clarsimp simp: object_type_def has_slots_def split: cdl_object.splits)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((object_type obj = TcbType \<Longrightarrow> has_slots obj) &&& (object_type obj = CNodeType \<Longrightarrow> has_slots obj) &&& (object_type obj = IRQNodeType \<Longrightarrow> has_slots obj)) &&& (object_type obj = PageTableType \<Longrightarrow> has_slots obj) &&& (object_type obj = PageDirectoryType \<Longrightarrow> has_slots obj) &&& (object_type obj = AsidPoolType \<Longrightarrow> has_slots obj)
theory Helpers_SD

lemma cap_type_update_cap_objects [simp]:
  "cap_type (update_cap_objects x cap) = cap_type cap" apply (clarsimp simp: cap_type_def update_cap_objects_def) apply (cases cap, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_type (update_cap_objects x cap) = cap_type cap proof (prove)
goal (1 subgoal):
 1. (case case cap of UntypedCap d xa xb \<Rightarrow> UntypedCap d x xb | _ \<Rightarrow> cap of UntypedCap x xa xb \<Rightarrow> Some UntypedType | EndpointCap x xa xb \<Rightarrow> Some EndpointType | NotificationCap x xa xb \<Rightarrow> Some NotificationType | CNodeCap x xa xb xc \<Rightarrow> Some CNodeType | TcbCap x \<Rightarrow> Some TcbType | IrqHandlerCap x \<Rightarrow> Some IRQNodeType | FrameCap x xa xb f xc xd \<Rightarrow> Some (FrameType f) | PageTableCap x xa xb \<Rightarrow> Some PageTableType | PageDirectoryCap x xa xb \<Rightarrow> Some PageDirectoryType | AsidPoolCap x xa \<Rightarrow> Some AsidPoolType | _ \<Rightarrow> None) = (case cap of UntypedCap x xa xb \<Rightarrow> Some UntypedType | EndpointCap x xa xb \<Rightarrow> Some EndpointType | NotificationCap x xa xb \<Rightarrow> Some NotificationType | CNodeCap x xa xb xc \<Rightarrow> Some CNodeType | TcbCap x \<Rightarrow> Some TcbType | IrqHandlerCap x \<Rightarrow> Some IRQNodeType | FrameCap x xa xb f xc xd \<Rightarrow> Some (FrameType f) | PageTableCap x xa xb \<Rightarrow> Some PageTableType | PageDirectoryCap x xa xb \<Rightarrow> Some PageDirectoryType | AsidPoolCap x xa \<Rightarrow> Some AsidPoolType | _ \<Rightarrow> None) proof (prove)
goal:
No subgoals!
theory Helpers_SD

lemma cap_has_object_update_cap_objects [simp]:
  "cap_has_object (update_cap_objects x cap) = cap_has_object cap" apply (clarsimp simp: update_cap_object_def
                        cap_has_object_def update_cap_objects_def) apply (cases cap, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_has_object (update_cap_objects x cap) = cap_has_object cap proof (prove)
goal (1 subgoal):
 1. (case case cap of UntypedCap d xa xb \<Rightarrow> UntypedCap d x xb | _ \<Rightarrow> cap of NullCap \<Rightarrow> False | DomainCap \<Rightarrow> False | RestartCap \<Rightarrow> False | RunningCap \<Rightarrow> False | IrqControlCap \<Rightarrow> False | IrqHandlerCap x \<Rightarrow> False | AsidControlCap \<Rightarrow> False | IOSpaceMasterCap \<Rightarrow> False | _ \<Rightarrow> True) = (case cap of NullCap \<Rightarrow> False | DomainCap \<Rightarrow> False | RestartCap \<Rightarrow> False | RunningCap \<Rightarrow> False | IrqControlCap \<Rightarrow> False | IrqHandlerCap x \<Rightarrow> False | AsidControlCap \<Rightarrow> False | IOSpaceMasterCap \<Rightarrow> False | _ \<Rightarrow> True) proof (prove)
goal:
No subgoals!
theory Helpers_SD

lemma cap_has_object_update_cap_object [simp]:
  "cap_has_object (update_cap_object x cap) = cap_has_object cap" by (clarsimp simp: update_cap_object_def cap_has_object_def
              split: cdl_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_has_object (update_cap_object x cap) = cap_has_object cap
theory Helpers_SD

lemma cap_object_default_cap [simp]:
  "\<lbrakk>type \<noteq> UntypedType; type \<noteq> IRQNodeType\<rbrakk>
  \<Longrightarrow> cap_object (default_cap type {obj_id} sz dev) = obj_id" by (clarsimp simp: default_cap_def  object_type_def is_untyped_def
              split: cdl_object_type.splits cdl_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>type \<noteq> UntypedType; type \<noteq> IRQNodeType\<rbrakk> \<Longrightarrow> cap_object (default_cap type {obj_id} sz dev) = obj_id
theory Helpers_SD

lemma cap_object_default_cap_frame:
  "is_frame_cap cap \<Longrightarrow> cap_object (default_cap (the (cap_type cap)) {obj_id} sz dev) = obj_id" by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_frame_cap cap \<Longrightarrow> cap_object (default_cap (the (cap_type cap)) {obj_id} sz dev) = obj_id