kings-crown/FVELER_Isabelle huggingface dataset:
theory Helpers_SD

lemma is_pd_default_cap[simp]:
  "is_pd obj \<Longrightarrow>
   cdl_objects spec ptr = Some obj \<Longrightarrow>
   default_cap (object_type obj) {ptr'} n b = PageDirectoryCap ptr' Real None" by (clarsimp simp: object_type_is_object default_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_pd obj; cdl_objects spec ptr = Some obj\<rbrakk> \<Longrightarrow> default_cap (object_type obj) {ptr'} n b = PageDirectoryCap ptr' Real None
theory Helpers_SD

lemma pd_at_default_cap[simp]:
  "pd_at ptr spec \<Longrightarrow>
   cdl_objects spec ptr = Some obj \<Longrightarrow>
   default_cap (object_type obj) {ptr'} n b = PageDirectoryCap ptr' Real None" by (fastforce simp: object_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pd_at ptr spec; cdl_objects spec ptr = Some obj\<rbrakk> \<Longrightarrow> default_cap (object_type obj) {ptr'} n b = PageDirectoryCap ptr' Real None
theory Helpers_SD

lemma pt_at_default_cap[simp]:
  "pt_at ptr spec \<Longrightarrow>
   cdl_objects spec ptr = Some obj \<Longrightarrow>
   default_cap (object_type obj) {ptr'} n b = PageTableCap ptr' Real None" by (clarsimp simp: object_type_is_object default_cap_def object_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pt_at ptr spec; cdl_objects spec ptr = Some obj\<rbrakk> \<Longrightarrow> default_cap (object_type obj) {ptr'} n b = PageTableCap ptr' Real None
theory Helpers_SD

lemma default_cap_not_null [elim!]:
  "default_cap type obj_ids sz dev = NullCap \<Longrightarrow> False"
  "NullCap = default_cap type obj_ids sz dev\<Longrightarrow> False" by (simp add: default_cap_def split: cdl_object_type.splits)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (default_cap type obj_ids sz dev = NullCap \<Longrightarrow> False) &&& (NullCap = default_cap type obj_ids sz dev \<Longrightarrow> False)
theory Helpers_SD

lemma cap_objects_update_cap_object [simp]:
  "\<lbrakk>cap_has_object cap; \<not>is_untyped_cap cap\<rbrakk>
  \<Longrightarrow> cap_objects (update_cap_object obj_id cap) = {obj_id}" by (clarsimp simp: cap_has_object_def update_cap_object_def
              split: cdl_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_has_object cap; cap_type cap \<noteq> Some UntypedType\<rbrakk> \<Longrightarrow> cap_objects (update_cap_object obj_id cap) = {obj_id}
theory Helpers_SD

lemma cap_has_object_default_cap [simp]:
  "type \<noteq> IRQNodeType \<Longrightarrow> cap_has_object (default_cap type ids sz dev)" by (clarsimp simp: default_cap_def cap_has_object_def split: cdl_object_type.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. type \<noteq> IRQNodeType \<Longrightarrow> cap_has_object (default_cap type ids sz dev)
theory Helpers_SD

lemma all_cdl_rights_UNIV [simp]:
  "all_cdl_rights = UNIV" by (fastforce intro: rights.exhaust simp: all_cdl_rights_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. all_cdl_rights = UNIV
theory Helpers_SD

lemma cap_rights_default_cap_cnode [simp]:
  "cap_rights (default_cap CNodeType ids sz dev) = UNIV" by (clarsimp simp: cap_rights_def default_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_rights (default_cap CNodeType ids sz dev) = UNIV
theory Helpers_SD

lemma cap_rights_cnode_cap [simp]:
  "is_cnode_cap cap \<Longrightarrow> cap_rights cap = UNIV" by (clarsimp simp: cap_type_def cap_rights_def
              split: cdl_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_cnode_cap cap \<Longrightarrow> cap_rights cap = UNIV
theory Helpers_SD

lemma cap_has_object_simps [simp]:
  "cap_has_object (IOPageTableCap x)"
  "cap_has_object (IOSpaceCap x)"
  "cap_has_object (IOPortsCap x a)"
  "cap_has_object (AsidPoolCap x b)"
  "cap_has_object (PageDirectoryCap x c d)"
  "cap_has_object (PageTableCap x e f)"
  "cap_has_object (FrameCap dev x g h i j)"
  "cap_has_object (TcbCap x)"
  "cap_has_object (CNodeCap x k l sz)"
  "cap_has_object (MasterReplyCap x)"
  "cap_has_object (ReplyCap x q)"
  "cap_has_object (NotificationCap x m n)"
  "cap_has_object (EndpointCap x p q)"
  "cap_has_object (ZombieCap x)"
  "cap_has_object (PendingSyncSendCap x s t u v w)"
  "cap_has_object (PendingSyncRecvCap x t w)"
  "cap_has_object (PendingNtfnRecvCap x)"
  "cap_has_object (UntypedCap dev ids ids') = True" by (simp_all add:cap_has_object_def)

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

lemma is_cap_NullCap [simp]:
  "\<not> is_untyped_cap NullCap"
  "\<not> is_ep_cap NullCap"
  "\<not> is_ntfn_cap NullCap"
  "\<not> is_cnode_cap NullCap"
  "\<not> is_tcb_cap NullCap"
  "\<not> is_asidpool_cap NullCap"
  "\<not> is_pt_cap NullCap"
  "\<not> is_pd_cap NullCap"
  "\<not> is_frame_cap NullCap"
  "\<not> is_fake_pt_cap NullCap"
  "\<not> is_irqhandler_cap NullCap" by (clarsimp simp: cap_type_def is_fake_pt_cap_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((cap_type NullCap \<noteq> Some UntypedType &&& cap_type NullCap \<noteq> Some EndpointType) &&& cap_type NullCap \<noteq> Some NotificationType &&& cap_type NullCap \<noteq> Some CNodeType &&& cap_type NullCap \<noteq> Some TcbType) &&& (cap_type NullCap \<noteq> Some AsidPoolType &&& cap_type NullCap \<noteq> Some PageTableType &&& cap_type NullCap \<noteq> Some PageDirectoryType) &&& \<not> is_frame_cap NullCap &&& \<not> is_fake_pt_cap NullCap &&& cap_type NullCap \<noteq> Some IRQNodeType
theory Helpers_SD

lemma is_exclusive_cap_update_cap_rights [simp]:
  "safe_for_derive (update_cap_rights rights cap) = safe_for_derive cap" by (clarsimp simp: update_cap_rights_def safe_for_derive_def
              split: cdl_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. safe_for_derive (update_cap_rights rights cap) = safe_for_derive cap
theory Helpers_SD

lemma derived_cap_safe_for_derive[simp]:
  "safe_for_derive (derived_cap cap) = safe_for_derive cap" apply (case_tac cap) apply (simp_all add:derived_cap_def safe_for_derive_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. safe_for_derive (derived_cap cap) = safe_for_derive cap proof (prove)
goal (27 subgoals):
 1. cap = NullCap \<Longrightarrow> safe_for_derive (derived_cap cap) = safe_for_derive cap
 2. \<And>x21 x22 x23. cap = UntypedCap x21 x22 x23 \<Longrightarrow> safe_for_derive (derived_cap cap) = safe_for_derive cap
 3. \<And>x31 x32 x33. cap = EndpointCap x31 x32 x33 \<Longrightarrow> safe_for_derive (derived_cap cap) = safe_for_derive cap
 4. \<And>x41 x42 x43. cap = NotificationCap x41 x42 x43 \<Longrightarrow> safe_for_derive (derived_cap cap) = safe_for_derive cap
 5. \<And>x51 x52. cap = ReplyCap x51 x52 \<Longrightarrow> safe_for_derive (derived_cap cap) = safe_for_derive cap
 6. \<And>x6. cap = MasterReplyCap x6 \<Longrightarrow> safe_for_derive (derived_cap cap) = safe_for_derive cap
 7. \<And>x71 x72 x73 x74. cap = CNodeCap x71 x72 x73 x74 \<Longrightarrow> safe_for_derive (derived_cap cap) = safe_for_derive cap
 8. \<And>x8. cap = TcbCap x8 \<Longrightarrow> safe_for_derive (derived_cap cap) = safe_for_derive cap
 9. cap = DomainCap \<Longrightarrow> safe_for_derive (derived_cap cap) = safe_for_derive cap
 10. \<And>x101 x102 x103 x104 x105 x106. cap = PendingSyncSendCap x101 x102 x103 x104 x105 x106 \<Longrightarrow> safe_for_derive (derived_cap cap) = safe_for_derive cap
A total of 27 subgoals... proof (prove)
goal:
No subgoals!
theory Helpers_SD

lemma safe_for_derive_not_non:
  "safe_for_derive cap \<Longrightarrow> cap \<noteq> NullCap" by (simp add:safe_for_derive_def split:cdl_cap.splits)

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

lemma object_default_state_def2:
  "object_default_state obj = (
    case obj of
        Untyped \<Rightarrow> Untyped
      | Endpoint \<Rightarrow> Endpoint
      | Notification \<Rightarrow> Notification
      | Tcb tcb \<Rightarrow> Tcb (default_tcb (cdl_tcb_domain tcb))
      | CNode cnode \<Rightarrow> CNode (empty_cnode (cdl_cnode_size_bits cnode))
      | IRQNode cnode \<Rightarrow> IRQNode empty_irq_node
      | AsidPool ap \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = empty_cap_map asid_low_bits\<rparr>
      | PageTable pt \<Rightarrow> PageTable \<lparr> cdl_page_table_caps = empty_cap_map 8 \<rparr>
      | PageDirectory pd \<Rightarrow> PageDirectory \<lparr> cdl_page_directory_caps = empty_cap_map 12 \<rparr>
      | Frame frame \<Rightarrow> Frame \<lparr> cdl_frame_size_bits = (cdl_frame_size_bits frame) \<rparr>)" by (clarsimp simp: object_default_state_def object_type_def default_object_def
                     object_size_bits_def object_domain_def
              split: cdl_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. object_default_state obj = (case obj of Endpoint \<Rightarrow> Endpoint | Notification \<Rightarrow> Notification | Tcb tcb \<Rightarrow> Tcb (default_tcb (cdl_tcb_domain tcb)) | CNode cnode \<Rightarrow> CNode (empty_cnode (cdl_cnode_size_bits cnode)) | AsidPool ap \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = empty_cap_map asid_low_bits\<rparr> | PageTable pt \<Rightarrow> PageTable \<lparr>cdl_page_table_caps = empty_cap_map 8\<rparr> | PageDirectory pd \<Rightarrow> PageDirectory \<lparr>cdl_page_directory_caps = empty_cap_map 12\<rparr> | Frame frame \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = cdl_frame_size_bits frame\<rparr> | Untyped \<Rightarrow> Untyped | IRQNode cnode \<Rightarrow> IRQNode empty_irq_node)
theory Helpers_SD

lemma object_type_update_slots [simp]:
  "object_type (update_slots slots x) = object_type x" by (clarsimp simp: object_type_def update_slots_def split: cdl_object.splits)

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

lemma object_slots_empty [simp]:
  "\<not> has_slots obj \<Longrightarrow> object_slots obj = Map.empty" by (clarsimp simp: object_slots_def has_slots_def split: cdl_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> has_slots obj \<Longrightarrow> object_slots obj = (\<lambda>x. None)
theory Helpers_SD

lemma object_slots_update_slots_empty [simp]:
  "\<not>has_slots obj \<Longrightarrow> object_slots (update_slots slots obj) = Map.empty" by (clarsimp simp: object_slots_def update_slots_def has_slots_def
                 split: cdl_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> has_slots obj \<Longrightarrow> object_slots (update_slots slots obj) = (\<lambda>x. None)
theory Helpers_SD

lemma update_slots_no_slots [simp]:
  "\<not>has_slots obj \<Longrightarrow> update_slots slots obj = obj" by (clarsimp simp: update_slots_def has_slots_def split: cdl_object.splits)

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

lemma update_slots_update_slots [simp]:
  "update_slots slots (update_slots slots' obj) = update_slots slots obj" by (clarsimp simp: update_slots_def split: cdl_object.splits)

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

lemma update_slots_same_object:
  "a = b \<Longrightarrow> update_slots a obj = update_slots b obj" by (erule arg_cong)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a = b \<Longrightarrow> update_slots a obj = update_slots b obj
theory Helpers_SD

lemma update_slots_eq_slots:
  "\<lbrakk>has_slots obj; update_slots slots obj = update_slots slots' obj'\<rbrakk> \<Longrightarrow> slots = slots'" by (clarsimp simp: update_slots_def has_slots_def cdl_tcb.splits cdl_cnode.splits
                     cdl_asid_pool.splits cdl_irq_node.splits
                     cdl_page_table.splits cdl_page_directory.splits
              split: cdl_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>has_slots obj; update_slots slots obj = update_slots slots' obj'\<rbrakk> \<Longrightarrow> slots = slots'
theory Helpers_SD

lemma has_slots_object_type_has_slots:
  "\<lbrakk>has_slots x; object_type x = object_type y\<rbrakk> \<Longrightarrow> has_slots y" by (clarsimp simp: object_type_def has_slots_def split: cdl_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>has_slots x; object_type x = object_type y\<rbrakk> \<Longrightarrow> has_slots y
theory Helpers_SD

lemma object_type_has_slots_eq:
  "object_type y = object_type x \<Longrightarrow> has_slots x = has_slots y" by (clarsimp simp: object_type_def has_slots_def split: cdl_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. object_type y = object_type x \<Longrightarrow> has_slots x = has_slots y
theory Helpers_SD

lemma update_slots_same [simp]:
  "object_slots obj = cap_map \<Longrightarrow> update_slots cap_map obj = obj" by (clarsimp simp: update_slots_def object_slots_def split: cdl_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. object_slots obj = cap_map \<Longrightarrow> update_slots cap_map obj = obj
theory Helpers_SD

lemma dom_sub_restrict [simp]:
  "dom (m `- A) = dom m \<inter> -A" by (auto simp: sub_restrict_map_def dom_def split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dom (m `- A) = dom m \<inter> - A
theory Helpers_SD

lemma inter_empty_not_both:
"\<lbrakk>x \<in> A; A \<inter> B = {}\<rbrakk> \<Longrightarrow> x \<notin> B" by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> A; A \<inter> B = {}\<rbrakk> \<Longrightarrow> x \<notin> B
theory Helpers_SD

lemma object_at_predicate_lift:
  "object_at P obj_id spec \<Longrightarrow> P (the (cdl_objects spec obj_id))" by (fastforce simp: object_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. object_at P obj_id spec \<Longrightarrow> P (the (cdl_objects spec obj_id))
theory Helpers_SD

lemma opt_cap_object_slot:
  "cdl_objects spec obj_id = Some obj \<Longrightarrow>
   P (object_slots obj slot) \<Longrightarrow>
   P (opt_cap (obj_id, slot) spec)" by (fastforce simp: object_at_def opt_cap_def slots_of_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cdl_objects spec obj_id = Some obj; P (object_slots obj slot)\<rbrakk> \<Longrightarrow> P (opt_cap (obj_id, slot) spec)
theory Helpers_SD

lemma opt_cap_object_slotE:
  "cdl_objects spec obj_id = Some obj \<Longrightarrow>
   object_slots obj slot = Some cap \<Longrightarrow>
   opt_cap (obj_id, slot) spec = Some cap" by (rule opt_cap_object_slot)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cdl_objects spec obj_id = Some obj; object_slots obj slot = Some cap\<rbrakk> \<Longrightarrow> opt_cap (obj_id, slot) spec = Some cap
theory Helpers_SD

lemma slots_of_object_slot:
  "cdl_objects spec obj_id = Some obj \<Longrightarrow>
   P (object_slots obj slot) \<Longrightarrow>
   P (slots_of obj_id spec slot)" by (fastforce simp: object_at_def opt_cap_def slots_of_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cdl_objects spec obj_id = Some obj; P (object_slots obj slot)\<rbrakk> \<Longrightarrow> P (slots_of obj_id spec slot)
theory Helpers_SD

lemma slots_of_object_slotE:
  "cdl_objects spec obj_id = Some obj \<Longrightarrow>
   object_slots obj slot = Some cap \<Longrightarrow>
   slots_of obj_id spec slot = Some cap" by (fastforce simp: object_at_def opt_cap_def slots_of_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cdl_objects spec obj_id = Some obj; object_slots obj slot = Some cap\<rbrakk> \<Longrightarrow> slots_of obj_id spec slot = Some cap
theory Helpers_SD

lemma object_at_cdl_objects:
  "cdl_objects spec obj_id = Some obj \<Longrightarrow>
   P obj \<Longrightarrow>
   object_at P obj_id spec" by (fastforce simp: object_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cdl_objects spec obj_id = Some obj; P obj\<rbrakk> \<Longrightarrow> object_at P obj_id spec
theory Helpers_SD

lemma opt_cap_object_slot_simp:
  "cdl_objects spec obj_id = Some obj \<Longrightarrow>
   opt_cap (obj_id, slot) spec = object_slots obj slot" by (fastforce simp: object_at_def opt_cap_def slots_of_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cdl_objects spec obj_id = Some obj \<Longrightarrow> opt_cap (obj_id, slot) spec = object_slots obj slot
theory Helpers_SD

lemma slots_of_object_slot_simp:
  "cdl_objects spec obj_id = Some obj \<Longrightarrow>
   slots_of obj_id spec slot = object_slots obj slot" by (fastforce simp: object_at_def opt_cap_def slots_of_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cdl_objects spec obj_id = Some obj \<Longrightarrow> slots_of obj_id spec slot = object_slots obj slot
theory Helpers_SD

lemma is_fake_pt_cap_cap_has_object:
  "is_fake_pt_cap cap \<Longrightarrow> cap_has_object cap" by (clarsimp simp: cap_has_object_def is_fake_pt_cap_def split: cdl_cap.splits)

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

lemma is_fake_pt_cap_pt_cap:
  "is_fake_pt_cap (PageTableCap x R z) \<longleftrightarrow> R = Fake" by (clarsimp simp: is_fake_pt_cap_def split: cdl_frame_cap_type.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_fake_pt_cap (PageTableCap x R z) = (R = Fake)
theory Helpers_SD

lemma fake_vm_cap_simp:
  "is_fake_vm_cap (FrameCap x y z a R b) \<longleftrightarrow> R = Fake" by (clarsimp simp: is_fake_vm_cap_def split: cdl_frame_cap_type.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_fake_vm_cap (FrameCap x y z a R b) = (R = Fake)
theory Helpers_SD

lemma frame_not_pt[intro!]: "\<not> (is_frame x \<and> is_pt x)" by (cases x; clarsimp simp: is_frame_def is_pt_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> (is_frame x \<and> is_pt x)
theory Helpers_SD

lemma not_frame_and_pt: "is_frame x \<Longrightarrow> is_pt x \<Longrightarrow> False" by (fastforce simp: frame_not_pt[simplified])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_frame x; is_pt x\<rbrakk> \<Longrightarrow> False
theory Helpers_SD

lemma not_cap_at_cap_not_at:
  "(slot \<in> dom (slots_of obj_id spec) \<and> \<not> cap_at P (obj_id, slot) spec) \<longleftrightarrow>
   (slot \<in> dom (slots_of obj_id spec) \<and> cap_at (\<lambda>x. \<not> P x) (obj_id, slot) spec)" by (intro iffI; clarsimp simp: cap_at_def opt_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (slot \<in> dom (slots_of obj_id spec) \<and> \<not> cap_at P (obj_id, slot) spec) = (slot \<in> dom (slots_of obj_id spec) \<and> cap_at (\<lambda>x. \<not> P x) (obj_id, slot) spec)
theory Separation_SD

lemma object_clean_def2:
  "object_clean = asid_reset \<circ> intent_reset" apply (rule ext) apply (clarsimp simp: object_clean_def intent_reset_def asid_reset_def
                        map_comp'_def object_slots_def update_slots_def
                 split:  cdl_object.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. object_clean = asid_reset \<circ> intent_reset proof (prove)
goal (1 subgoal):
 1. \<And>x. object_clean x = (asid_reset \<circ> intent_reset) x proof (prove)
goal:
No subgoals!
theory Separation_SD

lemma sep_map_general_def2:
  "sep_map_general obj_id object comp_id = (\<lambda>s.
    s = SepState (object_to_sep_state obj_id object comp_id) Map.empty)" apply (clarsimp simp: sep_map_general_def, rule ext) apply (case_tac s, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sep_map_general obj_id object comp_id = (\<lambda>s. s = SepState (object_to_sep_state obj_id object comp_id) (\<lambda>x. None)) proof (prove)
goal (1 subgoal):
 1. \<And>s. (sep_heap s = object_to_sep_state obj_id object comp_id \<and> sep_irq_node s = (\<lambda>x. None)) = (s = SepState (object_to_sep_state obj_id object comp_id) (\<lambda>x. None)) proof (prove)
goal:
No subgoals!
theory Separation_SD

lemma sep_map_S'_def2:
  "(obj_id, slots) \<mapsto>S' object \<equiv> sep_map_general obj_id object (Slot ` slots)" by (simp add: sep_map_S'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (obj_id, slots) \<mapsto>S' object \<equiv> sep_map_general obj_id object (Slot ` slots)
theory Separation_SD

lemma sep_map_s_def2:
  "(obj_id, slot) \<mapsto>s object \<equiv> sep_map_general obj_id object {Slot slot}" by (simp add: sep_map_s_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (obj_id, slot) \<mapsto>s object \<equiv> sep_map_general obj_id object {Slot slot}
theory Separation_SD

lemma offset_0 [simp]:
  "offset 0 root_cnode_size = 0" by (clarsimp simp: offset_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. offset 0 root_cnode_size = 0
theory Separation_SD

lemma offset_slot:
  "\<lbrakk>slot < 2^radix; radix < word_bits\<rbrakk> \<Longrightarrow> offset (of_nat slot) radix = slot" apply (clarsimp simp: offset_def) apply (subst Word.less_mask_eq) apply (erule (1) of_nat_less_pow_32) apply (subst unat_of_nat_eq) apply (drule_tac a="2::nat" and n=radix and N = word_bits in power_strict_increasing) apply simp apply (simp add: word_bits_def) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>slot < 2 ^ radix; radix < word_bits\<rbrakk> \<Longrightarrow> offset (word_of_nat slot) radix = slot proof (prove)
goal (1 subgoal):
 1. \<lbrakk>slot < 2 ^ radix; radix < word_bits\<rbrakk> \<Longrightarrow> unat (word_of_nat slot && mask radix) = slot proof (prove)
goal (2 subgoals):
 1. \<lbrakk>slot < 2 ^ radix; radix < word_bits\<rbrakk> \<Longrightarrow> word_of_nat slot < 2 ^ radix
 2. \<lbrakk>slot < 2 ^ radix; radix < word_bits\<rbrakk> \<Longrightarrow> unat (word_of_nat slot) = slot proof (prove)
goal (1 subgoal):
 1. \<lbrakk>slot < 2 ^ radix; radix < word_bits\<rbrakk> \<Longrightarrow> unat (word_of_nat slot) = slot proof (prove)
goal (2 subgoals):
 1. \<lbrakk>slot < 2 ^ radix; radix < word_bits\<rbrakk> \<Longrightarrow> slot < 2 ^ LENGTH(32)
 2. \<lbrakk>slot < 2 ^ radix; radix < word_bits\<rbrakk> \<Longrightarrow> slot = slot proof (prove)
goal (3 subgoals):
 1. slot < 2 ^ radix \<Longrightarrow> 1 < 2
 2. \<lbrakk>slot < 2 ^ radix; 2 ^ radix < 2 ^ word_bits\<rbrakk> \<Longrightarrow> slot < 2 ^ LENGTH(32)
 3. \<lbrakk>slot < 2 ^ radix; radix < word_bits\<rbrakk> \<Longrightarrow> slot = slot proof (prove)
goal (2 subgoals):
 1. \<lbrakk>slot < 2 ^ radix; 2 ^ radix < 2 ^ word_bits\<rbrakk> \<Longrightarrow> slot < 2 ^ LENGTH(32)
 2. \<lbrakk>slot < 2 ^ radix; radix < word_bits\<rbrakk> \<Longrightarrow> slot = slot proof (prove)
goal (1 subgoal):
 1. \<lbrakk>slot < 2 ^ radix; radix < word_bits\<rbrakk> \<Longrightarrow> slot = slot proof (prove)
goal:
No subgoals!