kings-crown/FVELER_Isabelle huggingface dataset:
theory MonadSep

lemma sep_set_conj_subset_wp':
  "\<lbrakk>xs \<subseteq> ys; finite xs; finite ys;
   \<And>R. \<lbrace><P \<and>* (\<And>* x \<in> xs. I x) \<and>* S \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* (\<And>* x \<in> xs. I x) \<and>* S \<and>* R>\<rbrace>\<rbrakk>
  \<Longrightarrow> \<lbrace><P \<and>* (\<And>* x \<in> ys. I x) \<and>* S \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* (\<And>* x \<in> ys. I x) \<and>* S \<and>* R>\<rbrace>" apply (cut_tac sep_set_conj_subset_wp [where P="P \<and>* S" and Q="Q \<and>* S" and
       I=I and R=R and ys=ys and xs=xs and f=f]) apply (fastforce simp: sep_conj_ac)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xs \<subseteq> ys; finite xs; finite ys; \<And>R. \<lbrace><P \<and>* sep_map_set_conj I xs \<and>* S \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* sep_map_set_conj I xs \<and>* S \<and>* R>\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace><P \<and>* sep_map_set_conj I ys \<and>* S \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* sep_map_set_conj I ys \<and>* S \<and>* R>\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<lbrakk>xs \<subseteq> ys; finite xs; finite ys; \<And>R. \<lbrace><P \<and>* sep_map_set_conj I xs \<and>* S \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* sep_map_set_conj I xs \<and>* S \<and>* R>\<rbrace>; \<lbrace><(P \<and>* S) \<and>* sep_map_set_conj I ys \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <(Q \<and>* S) \<and>* sep_map_set_conj I ys \<and>* R>\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace><P \<and>* sep_map_set_conj I ys \<and>* S \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* sep_map_set_conj I ys \<and>* S \<and>* R>\<rbrace>
 2. \<lbrakk>xs \<subseteq> ys; finite xs; finite ys; \<And>R. \<lbrace><P \<and>* sep_map_set_conj I xs \<and>* S \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* sep_map_set_conj I xs \<and>* S \<and>* R>\<rbrace>\<rbrakk> \<Longrightarrow> xs \<subseteq> ys
 3. \<lbrakk>xs \<subseteq> ys; finite xs; finite ys; \<And>R. \<lbrace><P \<and>* sep_map_set_conj I xs \<and>* S \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* sep_map_set_conj I xs \<and>* S \<and>* R>\<rbrace>\<rbrakk> \<Longrightarrow> finite xs
 4. \<lbrakk>xs \<subseteq> ys; finite xs; finite ys; \<And>R. \<lbrace><P \<and>* sep_map_set_conj I xs \<and>* S \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* sep_map_set_conj I xs \<and>* S \<and>* R>\<rbrace>\<rbrakk> \<Longrightarrow> finite ys
 5. \<And>R. \<lbrakk>xs \<subseteq> ys; finite xs; finite ys; \<And>R. \<lbrace><P \<and>* sep_map_set_conj I xs \<and>* S \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <Q \<and>* sep_map_set_conj I xs \<and>* S \<and>* R>\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace><(P \<and>* S) \<and>* sep_map_set_conj I xs \<and>* R>\<rbrace> f \<lbrace>\<lambda>_. <(Q \<and>* S) \<and>* sep_map_set_conj I xs \<and>* R>\<rbrace> proof (prove)
goal:
No subgoals!
theory Sep_Tactic_Helper

lemma no_exception_conjE:
  "\<lbrakk>\<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>, -; \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P and P'\<rbrace> f \<lbrace>\<lambda>r s. Q r s \<and> Q' r s\<rbrace>, \<lbrace>E\<rbrace>" by (fastforce simp: validE_def validE_R_def valid_def split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>, -; \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P and P'\<rbrace> f \<lbrace>\<lambda>r s. Q r s \<and> Q' r s\<rbrace>, \<lbrace>E\<rbrace>
theory Sep_Tactic_Helper

lemma sep_any_imp[sep_cancel]: "(m p e) s \<Longrightarrow> sep_any m p s" by (fastforce simp: sep_any_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m p e s \<Longrightarrow> sep_any m p s
theory Lookups_D

lemma throwError_FaultError [simp]:
  "throwError FaultError = throw" apply (cases "undefined::cdl_fault_error") apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. throwError FaultError = throw proof (prove)
goal (1 subgoal):
 1. undefined = FaultError \<Longrightarrow> throwError FaultError = throw proof (prove)
goal:
No subgoals!
theory Helpers_SD

lemma tcb_ipc_buffer_address_non_zero:
  "tcb_ipc_buffer_address tcb \<noteq> 0" by (clarsimp simp: tcb_ipc_buffer_address_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_ipc_buffer_address tcb \<noteq> 0
theory Helpers_SD

lemma map_upd_nonempty' [simp]: "Map.empty \<noteq> t(k\<mapsto>x)" by (rule not_sym, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. None) \<noteq> t(k \<mapsto> x)
theory Helpers_SD

lemma insert_unit_set [simp]:
  "insert () A = UNIV" by auto

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

lemma restrict_map_not_empty [simp]:
  "f p = Some v \<Longrightarrow> f |` {p} \<noteq> Map.empty"
  "f p = Some v \<Longrightarrow> Map.empty \<noteq> f |` {p}" by (clarsimp simp: restrict_map_def fun_eq_iff split: if_split_asm)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (f p = Some v \<Longrightarrow> f |` {p} \<noteq> (\<lambda>x. None)) &&& (f p = Some v \<Longrightarrow> (\<lambda>x. None) \<noteq> f |` {p})
theory Helpers_SD

lemma map_comp'_apply [simp]: "(f \<circ>\<^sub>M g) x = case_option None (\<lambda>x. Some (f x)) (g x)" by (clarsimp simp: map_comp'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (f o_M g) x = (case g x of None \<Rightarrow> None | Some x \<Rightarrow> Some (f x))
theory Helpers_SD

lemma map_comp'_empty [simp]:
  "m \<circ>\<^sub>M Map.empty = Map.empty" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m o_M (\<lambda>x. None) = (\<lambda>x. None)
theory Helpers_SD

lemma dom_map_comp' [simp]:
  "dom (f \<circ>\<^sub>M m) = dom m" by (clarsimp simp: dom_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dom (f o_M m) = dom m
theory Helpers_SD

lemma restrict_map_comp' [simp]:
  "f \<circ>\<^sub>M g |` S = (f \<circ>\<^sub>M g) |` S" by (rule ext, clarsimp simp: map_comp'_def restrict_map_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f o_M g |` S = (f o_M g) |` S
theory Helpers_SD

lemma nat_list_not_UNIV [simp]:
  "set (xs::nat list) \<noteq> UNIV" by (metis UNIV_I gt_ex leD maximum_ge)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set xs \<noteq> UNIV
theory Helpers_SD

lemma map_add_self:
  "m ++ m = m" by (auto simp add:map_add_def split:option.splits)

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

lemma restrict_map_disj':
  "S \<inter> T = {} \<Longrightarrow> h |` S \<bottom> h' |` T" by (auto simp: map_disj_def restrict_map_def dom_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. S \<inter> T = {} \<Longrightarrow> h |` S \<bottom> h' |` T
theory Helpers_SD

lemma map_add_restrict_comm:
  "S \<inter> T = {} \<Longrightarrow> h |` S ++ h' |` T = h' |` T ++ h |` S" apply (drule restrict_map_disj') apply (erule map_add_com) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. S \<inter> T = {} \<Longrightarrow> h |` S ++ h' |` T = h' |` T ++ h |` S proof (prove)
goal (1 subgoal):
 1. ?h |` S \<bottom> ?h' |` T \<Longrightarrow> h |` S ++ h' |` T = h' |` T ++ h |` S proof (prove)
goal:
No subgoals!
theory Helpers_SD

lemma restrict_map_not_self_UNIV [simp]:
  "h |` (UNIV - dom h) = Map.empty" by (rule ext, clarsimp simp: restrict_map_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. h |` (UNIV - dom h) = (\<lambda>x. None)
theory Helpers_SD

lemma map_add_emptyE [elim!]:
  "\<lbrakk>a ++ b = Map.empty; \<lbrakk>a = Map.empty; b = Map.empty\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" by (metis map_add_None)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a ++ b = (\<lambda>x. None); \<lbrakk>a = (\<lambda>x. None); b = (\<lambda>x. None)\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R
theory Helpers_SD

lemma restrict_map_sub_singleton [simp]:
  "s \<noteq> t \<Longrightarrow> h `- {t} |` {s} = h |` {s}" by (rule ext)(clarsimp simp: restrict_map_def sub_restrict_map_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<noteq> t \<Longrightarrow> h `- {t} |` {s} = h |` {s}
theory Helpers_SD

lemma restrict_map_sub_add': "h `- S ++ h |` S = h" by (fastforce simp: sub_restrict_map_def map_add_def
               split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. h `- S ++ h |` S = h
theory Helpers_SD

lemma map_add_restrict_singleton:
  "s \<noteq> t \<Longrightarrow> (m |` {s} ++ m' |` {t}) |` {s} = m |` {s}" apply (rule ext) apply (clarsimp simp: map_add_def restrict_map_def split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<noteq> t \<Longrightarrow> (m |` {s} ++ m' |` {t}) |` {s} = m |` {s} proof (prove)
goal (1 subgoal):
 1. \<And>x. s \<noteq> t \<Longrightarrow> ((m |` {s} ++ m' |` {t}) |` {s}) x = (m |` {s}) x proof (prove)
goal:
No subgoals!
theory Helpers_SD

lemma map_add_restrict_singleton':
  "s \<noteq> t \<Longrightarrow> (m |` {s} ++ m' |` {t}) |` {t} = m' |` {t}" apply (rule ext) apply (clarsimp simp: map_add_def restrict_map_def split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<noteq> t \<Longrightarrow> (m |` {s} ++ m' |` {t}) |` {t} = m' |` {t} proof (prove)
goal (1 subgoal):
 1. \<And>x. s \<noteq> t \<Longrightarrow> ((m |` {s} ++ m' |` {t}) |` {t}) x = (m' |` {t}) x proof (prove)
goal:
No subgoals!
theory Helpers_SD

lemma all_capsE [elim!]:
  "\<lbrakk>opt_cap (obj_id, slot) spec = Some cap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> cap \<in> all_caps spec"
  "\<lbrakk>opt_cap cap_ref spec = Some cap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> cap \<in> all_caps spec" apply (clarsimp simp: all_caps_def|fast)+ by (metis surj_pair)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>opt_cap (obj_id, slot) spec = Some cap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> cap \<in> all_caps spec) &&& (\<lbrakk>opt_cap cap_ref spec = Some cap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> cap \<in> all_caps spec) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>opt_cap cap_ref spec = Some cap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<exists>obj_id slot. opt_cap (obj_id, slot) spec = Some cap
theory Helpers_SD

lemma default_tcb_slots:
 "[0 ..< tcb_pending_op_slot] = [0,1,2,3,4]"
 "[0 ..< 5] = [0,1,2,3,4]"
 "[0 .e. tcb_pending_op_slot] = [0,1,2,3,4,5]"
 "[0 .e. (5::nat)] = [0,1,2,3,4,5]"
 "[0..< 6] = [0,1,2,3,4,5]"
 "[0..< 7] = [0,1,2,3,4,5,6]" by (clarsimp simp: tcb_pending_op_slot_def upt_rec)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ([0..<tcb_pending_op_slot] = [0, 1, 2, 3, 4] &&& [0..<5] = [0, 1, 2, 3, 4] &&& [0 .e. tcb_pending_op_slot] = [0, 1, 2, 3, 4, 5]) &&& [0 .e. 5] = [0, 1, 2, 3, 4, 5] &&& [0..<6] = [0, 1, 2, 3, 4, 5] &&& [0..<7] = [0, 1, 2, 3, 4, 5, 6]
theory Helpers_SD

lemma update_tcb_fault_endpoint_id [simp]:
  "cdl_tcb_fault_endpoint tcb = fault_ep
  \<Longrightarrow> update_tcb_fault_endpoint fault_ep tcb = tcb" by (clarsimp simp: update_tcb_fault_endpoint_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cdl_tcb_fault_endpoint tcb = fault_ep \<Longrightarrow> update_tcb_fault_endpoint fault_ep tcb = tcb
theory Helpers_SD

lemma slots_of_cdl_objects:
  "slots_of obj_id s slot = Some cap \<Longrightarrow> \<exists>obj. cdl_objects s obj_id = Some obj" by (clarsimp simp: slots_of_def split: option.splits)

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

lemma opt_cap_cdl_objects:
  "opt_cap (obj_id, slot) s = Some cap \<Longrightarrow> \<exists>obj. cdl_objects s obj_id = Some obj" by (clarsimp simp: opt_cap_def slots_of_cdl_objects)

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

lemma object_slots_slots_of:
  "\<lbrakk>slots_of obj_id spec slot = Some cap; cdl_objects spec obj_id = Some obj\<rbrakk>
  \<Longrightarrow> object_slots obj slot = Some cap" by (clarsimp simp: slots_of_def)

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

lemma object_slots_opt_cap:
  "\<lbrakk>opt_cap cap_ref spec = Some cap; cdl_objects spec obj_id = Some obj; cap_ref = (obj_id, slot)\<rbrakk>
  \<Longrightarrow> object_slots obj slot = Some cap" by (clarsimp simp: opt_cap_def object_slots_slots_of split: prod.split_asm)+

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

lemma object_slots_opt_capI:
  "\<lbrakk>opt_cap (obj_id, slot) spec = Some cap; cdl_objects spec obj_id = Some obj\<rbrakk>
  \<Longrightarrow> object_slots obj slot = Some cap" by (clarsimp simp: opt_cap_def object_slots_slots_of split: prod.split_asm)

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

lemma object_slots_has_slots:
  "object_slots obj \<noteq> Map.empty \<Longrightarrow> has_slots obj" by (clarsimp simp: has_slots_def object_slots_def split: cdl_object.splits)

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

lemma slots_of_dom_cdl_objects [elim!]:
  "slots_of obj_id spec slot = Some cap \<Longrightarrow> obj_id \<in> dom (cdl_objects spec)"
  "slots_of obj_id spec slot = Some cap \<Longrightarrow> \<exists>slot. cdl_objects spec obj_id = Some slot" by (clarsimp simp: slots_of_def split:option.splits)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (slots_of obj_id spec slot = Some cap \<Longrightarrow> obj_id \<in> dom (cdl_objects spec)) &&& (slots_of obj_id spec slot = Some cap \<Longrightarrow> \<exists>slot. cdl_objects spec obj_id = Some slot)
theory Helpers_SD

lemma opt_cap_dom_cdl_objects [elim]:
  "opt_cap (obj_id, slot) spec = Some cap \<Longrightarrow> obj_id \<in> dom (cdl_objects spec)"
  "opt_cap cap_ref spec = Some cap \<Longrightarrow> fst cap_ref \<in> dom (cdl_objects spec)" by (clarsimp simp: opt_cap_def split: prod.split_asm)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (opt_cap (obj_id, slot) spec = Some cap \<Longrightarrow> obj_id \<in> dom (cdl_objects spec)) &&& (opt_cap cap_ref spec = Some cap \<Longrightarrow> fst cap_ref \<in> dom (cdl_objects spec))
theory Helpers_SD

lemma opt_cap_dom_slots_of [elim]:
  "opt_cap (obj_id, slot) spec = Some cap \<Longrightarrow> slot \<in> dom (slots_of obj_id spec)"
  "opt_cap cap_ref spec = Some cap \<Longrightarrow> snd cap_ref \<in> dom (slots_of (fst cap_ref) spec)" by (clarsimp simp: opt_cap_def split: prod.split_asm)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (opt_cap (obj_id, slot) spec = Some cap \<Longrightarrow> slot \<in> dom (slots_of obj_id spec)) &&& (opt_cap cap_ref spec = Some cap \<Longrightarrow> snd cap_ref \<in> dom (slots_of (fst cap_ref) spec))
theory Helpers_SD

lemma cap_free_ids_simps:
  "cap_free_ids (UntypedCap d cover_ids available_ids) = available_ids" by (clarsimp simp: cap_free_ids_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_free_ids (UntypedCap d cover_ids available_ids) = available_ids
theory Helpers_SD

lemma cap_objects_remove_free_ids [simp]:
  "cap_objects (remove_free_ids cap obj_ids) = cap_objects cap" by (clarsimp simp: cap_objects_def remove_free_ids_def
              split: cdl_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_objects (remove_free_ids cap obj_ids) = cap_objects cap
theory Helpers_SD

lemma cap_free_ids_remove_free_ids:
  "cap_free_ids (remove_free_ids cap obj_ids) = cap_free_ids cap - obj_ids" by (clarsimp simp: remove_free_ids_def cap_free_ids_def
              split: cdl_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_free_ids (remove_free_ids cap obj_ids) = cap_free_ids cap - obj_ids
theory Helpers_SD

lemma cap_type_remove_free_ids [simp]:
  "cap_type (remove_free_ids cap obj_ids) = cap_type cap" by (clarsimp simp: cap_type_def remove_free_ids_def
              split: cdl_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_type (remove_free_ids cap obj_ids) = cap_type cap
theory Helpers_SD

lemma remove_free_ids_simps:
  "\<lbrakk>is_untyped_cap cap; available_ids \<subseteq> cap_free_ids cap\<rbrakk>
  \<Longrightarrow> remove_free_ids cap (cap_free_ids cap - available_ids)
    = UntypedCap (is_device_cap cap) (cap_objects cap) available_ids" by (auto simp: remove_free_ids_def cap_free_ids_def cap_type_def
          split: cdl_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_untyped_cap cap; available_ids \<subseteq> cap_free_ids cap\<rbrakk> \<Longrightarrow> remove_free_ids cap (cap_free_ids cap - available_ids) = UntypedCap (is_device_cap cap) (cap_objects cap) available_ids
theory Helpers_SD

lemma is_full_untyped_cap_is_untyped_cap:
  "is_full_untyped_cap cap \<Longrightarrow> is_untyped_cap cap" by (clarsimp simp: is_full_untyped_cap_def split: cdl_cap.splits)

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

lemma is_full_untyped_cap_simps:
  "is_full_untyped_cap cap \<Longrightarrow> cap_objects cap = cap_free_ids cap" by (auto simp: is_full_untyped_cap_def cap_free_ids_def
          split: cdl_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_full_untyped_cap cap \<Longrightarrow> cap_objects cap = cap_free_ids cap
theory Helpers_SD

lemma is_full_untyped_cap_eq:
  "is_untyped_cap cap
  \<Longrightarrow> is_full_untyped_cap cap = (cap_objects cap = cap_free_ids cap)" by (auto simp: is_full_untyped_cap_def cap_free_ids_def
                 cap_objects_def cap_type_def
          split: cdl_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_untyped_cap cap \<Longrightarrow> is_full_untyped_cap cap = (cap_objects cap = cap_free_ids cap)
theory Helpers_SD

lemma well_formed_untyped_cap_remove_free_ids:
  "well_formed_untyped_cap cap
  \<Longrightarrow> well_formed_untyped_cap (remove_free_ids cap obj_ids)" by (auto simp: well_formed_untyped_cap_def remove_free_ids_def
          split: cdl_cap.splits)

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

lemma well_formed_untyped_cap_simps:
  "is_untyped_cap cap
  \<Longrightarrow> well_formed_untyped_cap cap = (cap_free_ids cap \<subseteq> cap_objects cap)" by (clarsimp simp: well_formed_untyped_cap_def cap_free_ids_def
                     cap_objects_def cap_type_def
              split: cdl_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_untyped_cap cap \<Longrightarrow> well_formed_untyped_cap cap = (cap_free_ids cap \<subseteq> cap_objects cap)
theory Helpers_SD

lemma some_nat_Some [simp]:
  "some_nat (Some n) = n" by (simp add: some_nat_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. some_nat (Some n) = n
theory Helpers_SD

lemma some_nat_None [simp]:
  "some_nat None = 0" by (simp add: some_nat_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. some_nat None = 0
theory Helpers_SD

lemma is_object_simps [simp]:
  "is_untyped Untyped"
  "is_ep Endpoint"
  "is_ntfn Notification"
  "is_tcb (Tcb tcb)"
  "is_cnode (CNode c)"
  "is_asidpool (AsidPool a)"
  "is_pd (PageDirectory pd)"
  "is_pt (PageTable pt)"
  "is_frame (Frame f)" by (clarsimp simp: is_untyped_def is_ep_def is_ntfn_def is_tcb_def is_cnode_def
                     is_asidpool_def is_pt_def is_pd_def is_frame_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((is_untyped Untyped &&& is_ep Endpoint) &&& is_ntfn Notification &&& is_tcb (Tcb tcb)) &&& (is_cnode (CNode c) &&& is_asidpool (AsidPool a)) &&& is_pd (PageDirectory pd) &&& is_pt (PageTable pt) &&& is_frame (Frame f)
theory Helpers_SD

lemma object_size_bits_default_tcb [simp]:
  "object_size_bits (Tcb (default_tcb domain)) = 0" by (clarsimp simp: object_size_bits_def default_tcb_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. object_size_bits (Tcb (default_tcb domain)) = 0
theory Helpers_SD

lemma object_size_bits_empty_cnode [simp]:
  "object_size_bits (CNode (empty_cnode sz)) = sz" by (clarsimp simp: object_size_bits_def empty_cnode_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. object_size_bits (CNode (empty_cnode sz)) = sz
theory Helpers_SD

lemma is_pt_pt_size[simp]: "is_pt obj \<Longrightarrow> object_size_bits obj = pt_size" by (clarsimp simp: object_size_bits_def pt_size_def is_pt_def split: cdl_object.splits)

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

lemma is_pd_pd_size[simp]: "is_pd obj \<Longrightarrow> object_size_bits obj = pd_size" by (clarsimp simp: object_size_bits_def pt_size_def is_pd_def split: cdl_object.splits)

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

lemma object_at_pointer_size_bits_simp [simp]:
  "cdl_objects spec obj_id = Some object
  \<Longrightarrow> object_at_pointer_size_bits spec obj_id = object_size_bits object" by (simp add: object_at_pointer_size_bits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cdl_objects spec obj_id = Some object \<Longrightarrow> object_at_pointer_size_bits spec obj_id = object_size_bits object
theory Helpers_SD

lemma bound_irq_list_set[simp]: "set (bound_irq_list s) = bound_irqs s" apply (clarsimp simp: bound_irqs_def bound_irq_list_def image_def) apply (intro set_eqI iffI) apply (fastforce split: option.splits) apply (unat_arith, clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set (bound_irq_list s) = bound_irqs s proof (prove)
goal (1 subgoal):
 1. {x. case slots_of (cdl_irq_node s x) s 0 of None \<Rightarrow> False | Some cap \<Rightarrow> cap \<noteq> NullCap} = {irq. \<exists>cap. slots_of (cdl_irq_node s irq) s 0 = Some cap \<and> cap \<noteq> NullCap} proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> {x. case slots_of (cdl_irq_node s x) s 0 of None \<Rightarrow> False | Some cap \<Rightarrow> cap \<noteq> NullCap} \<Longrightarrow> x \<in> {irq. \<exists>cap. slots_of (cdl_irq_node s irq) s 0 = Some cap \<and> cap \<noteq> NullCap}
 2. \<And>x. x \<in> {irq. \<exists>cap. slots_of (cdl_irq_node s irq) s 0 = Some cap \<and> cap \<noteq> NullCap} \<Longrightarrow> x \<in> {x. case slots_of (cdl_irq_node s x) s 0 of None \<Rightarrow> False | Some cap \<Rightarrow> cap \<noteq> NullCap} proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> {irq. \<exists>cap. slots_of (cdl_irq_node s irq) s 0 = Some cap \<and> cap \<noteq> NullCap} \<Longrightarrow> x \<in> {x. case slots_of (cdl_irq_node s x) s 0 of None \<Rightarrow> False | Some cap \<Rightarrow> cap \<noteq> NullCap} proof (prove)
goal:
No subgoals!
theory Helpers_SD

lemma bound_irq_list_distinct[intro]: "distinct (bound_irq_list s)" by (clarsimp simp: bound_irq_list_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. distinct (bound_irq_list s)