kings-crown/FVELER_Isabelle huggingface dataset:
theory Detype_C

lemma ko_at_is_aligned' [intro?]:
  "ko_at' ko p s \<Longrightarrow> is_aligned p (objBits ko)" apply (erule obj_atE') apply (simp add: objBits_def projectKOs project_inject) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ko_at' ko p s \<Longrightarrow> is_aligned p (objBits ko) proof (prove)
goal (1 subgoal):
 1. \<And>koa obj. \<lbrakk>ksPSpace s p = Some koa; is_aligned p (objBitsKO koa); fst (projectKO koa s) = {(obj, s)}; obj = ko; ps_clear p (objBitsKO koa) s\<rbrakk> \<Longrightarrow> is_aligned p (objBits ko) proof (prove)
goal:
No subgoals!
theory Detype_C

lemma tcb_cte_in_range:
  "\<lbrakk> ksPSpace s p = Some (KOTCB tcb); is_aligned p tcbBlockSizeBits;
  tcb_cte_cases n = Some (getF, setF) \<rbrakk>
  \<Longrightarrow> {p + n.. (p + n) + 2 ^ objBits (cte :: cte) - 1} \<subseteq> {p .. p + 2 ^ objBits tcb - 1}" apply (rule range_subsetI) apply (erule (1) tcb_cte_cases_in_range1 [where y = "p + n" and x = p, simplified]) apply (frule (1) tcb_cte_cases_in_range3 [where y = "p + n" and x = p, simplified]) apply (simp add: objBits_simps') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s p = Some (KOTCB tcb); is_aligned p tcbBlockSizeBits; tcb_cte_cases n = Some (getF, setF)\<rbrakk> \<Longrightarrow> {p + n..p + n + 2 ^ objBits cte - 1} \<subseteq> {p..p + 2 ^ objBits tcb - 1} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ksPSpace s p = Some (KOTCB tcb); is_aligned p tcbBlockSizeBits; tcb_cte_cases n = Some (getF, setF)\<rbrakk> \<Longrightarrow> p \<le> p + n
 2. \<lbrakk>ksPSpace s p = Some (KOTCB tcb); is_aligned p tcbBlockSizeBits; tcb_cte_cases n = Some (getF, setF)\<rbrakk> \<Longrightarrow> p + n + 2 ^ objBits cte - 1 \<le> p + 2 ^ objBits tcb - 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s p = Some (KOTCB tcb); is_aligned p tcbBlockSizeBits; tcb_cte_cases n = Some (getF, setF)\<rbrakk> \<Longrightarrow> p + n + 2 ^ objBits cte - 1 \<le> p + 2 ^ objBits tcb - 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s p = Some (KOTCB tcb); is_aligned p tcbBlockSizeBits; tcb_cte_cases n = Some (getF, setF); p + n + 2 ^ cteSizeBits - 1 \<le> p + 2 ^ tcbBlockSizeBits - 1\<rbrakk> \<Longrightarrow> p + n + 2 ^ objBits cte - 1 \<le> p + 2 ^ objBits tcb - 1 proof (prove)
goal:
No subgoals!
theory Detype_C

lemma tcb_cte_cases_aligned:
  "\<lbrakk>is_aligned p tcbBlockSizeBits; tcb_cte_cases n = Some (getF, setF)\<rbrakk>
  \<Longrightarrow> is_aligned (p + n) (objBits (cte :: cte))" apply (erule aligned_add_aligned) apply (simp add: tcb_cte_cases_def is_aligned_def objBits_simps' split: if_split_asm) apply (simp add: objBits_simps') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p tcbBlockSizeBits; tcb_cte_cases n = Some (getF, setF)\<rbrakk> \<Longrightarrow> is_aligned (p + n) (objBits cte) proof (prove)
goal (2 subgoals):
 1. tcb_cte_cases n = Some (getF, setF) \<Longrightarrow> is_aligned n (objBits cte)
 2. tcb_cte_cases n = Some (getF, setF) \<Longrightarrow> objBits cte \<le> tcbBlockSizeBits proof (prove)
goal (1 subgoal):
 1. tcb_cte_cases n = Some (getF, setF) \<Longrightarrow> objBits cte \<le> tcbBlockSizeBits proof (prove)
goal:
No subgoals!
theory Detype_C

lemma ep_queue_live:
  assumes invs: "invs' s"
  and     koat: "ko_at' ep p s"
  shows   "\<forall>t \<in> set (epQ ep). ko_wp_at' live' t s" proof fix t assume tin: "t \<in> set (epQ ep)" from invs koat tin show "ko_wp_at' live' t s" apply - apply (drule sym_refs_ko_atD') apply clarsimp apply (cases ep) by (auto elim!: ko_wp_at'_weakenE [OF _ refs_of_live']) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>t\<in>set (epQ ep). ko_wp_at' live' t s proof (state)
goal (1 subgoal):
 1. \<And>t. t \<in> set (epQ ep) \<Longrightarrow> ko_wp_at' live' t s proof (state)
goal (1 subgoal):
 1. \<And>t. t \<in> set (epQ ep) \<Longrightarrow> ko_wp_at' live' t s proof (state)
this:
t \<in> set (epQ ep)

goal (1 subgoal):
 1. \<And>t. t \<in> set (epQ ep) \<Longrightarrow> ko_wp_at' live' t s proof (chain)
picking this:
invs' s
ko_at' ep p s
t \<in> set (epQ ep) proof (prove)
using this:
invs' s
ko_at' ep p s
t \<in> set (epQ ep)

goal (1 subgoal):
 1. ko_wp_at' live' t s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs' s; ko_at' ep p s; t \<in> set (epQ ep)\<rbrakk> \<Longrightarrow> ko_wp_at' live' t s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invs' s; t \<in> set (epQ ep)\<rbrakk> \<Longrightarrow> sym_refs (state_refs_of' s)
 2. \<lbrakk>invs' s; t \<in> set (epQ ep); state_refs_of' s p = refs_of' (injectKOS ep) \<and> (\<forall>(x, tp)\<in>refs_of' (injectKOS ep). ko_wp_at' (\<lambda>ko. (p, symreftype tp) \<in> refs_of' ko) x s)\<rbrakk> \<Longrightarrow> ko_wp_at' live' t s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs' s; t \<in> set (epQ ep); state_refs_of' s p = refs_of' (injectKOS ep) \<and> (\<forall>(x, tp)\<in>refs_of' (injectKOS ep). ko_wp_at' (\<lambda>ko. (p, symreftype tp) \<in> refs_of' ko) x s)\<rbrakk> \<Longrightarrow> ko_wp_at' live' t s proof (prove)
goal (3 subgoals):
 1. \<And>x1. \<lbrakk>invs' s; t \<in> set (epQ ep); state_refs_of' s p = refs_of' (injectKOS ep) \<and> (\<forall>(x, tp)\<in>refs_of' (injectKOS ep). ko_wp_at' (\<lambda>ko. (p, symreftype tp) \<in> refs_of' ko) x s); ep = Structures_H.endpoint.RecvEP x1\<rbrakk> \<Longrightarrow> ko_wp_at' live' t s
 2. \<lbrakk>invs' s; t \<in> set (epQ ep); state_refs_of' s p = refs_of' (injectKOS ep) \<and> (\<forall>(x, tp)\<in>refs_of' (injectKOS ep). ko_wp_at' (\<lambda>ko. (p, symreftype tp) \<in> refs_of' ko) x s); ep = Structures_H.endpoint.IdleEP\<rbrakk> \<Longrightarrow> ko_wp_at' live' t s
 3. \<And>x3. \<lbrakk>invs' s; t \<in> set (epQ ep); state_refs_of' s p = refs_of' (injectKOS ep) \<and> (\<forall>(x, tp)\<in>refs_of' (injectKOS ep). ko_wp_at' (\<lambda>ko. (p, symreftype tp) \<in> refs_of' ko) x s); ep = Structures_H.endpoint.SendEP x3\<rbrakk> \<Longrightarrow> ko_wp_at' live' t s proof (state)
this:
ko_wp_at' live' t s

goal:
No subgoals!
theory Detype_C

lemma ntfn_queue_live:
  assumes invs: "invs' s"
  and     koat: "ko_at' ntfn p s"
  shows   "\<forall>t \<in> set (ntfnQ (ntfnObj ntfn)). ko_wp_at' live' t s" proof fix t assume tin: "t \<in> set (ntfnQ (ntfnObj ntfn))" from invs koat tin show "ko_wp_at' live' t s" apply - apply (drule sym_refs_ko_atD') apply clarsimp apply (cases "ntfnObj ntfn") apply (auto elim!: ko_wp_at'_weakenE [OF _ refs_of_live']
                  dest!: bspec) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>t\<in>set (ntfnQ (ntfnObj ntfn)). ko_wp_at' live' t s proof (state)
goal (1 subgoal):
 1. \<And>t. t \<in> set (ntfnQ (ntfnObj ntfn)) \<Longrightarrow> ko_wp_at' live' t s proof (state)
goal (1 subgoal):
 1. \<And>t. t \<in> set (ntfnQ (ntfnObj ntfn)) \<Longrightarrow> ko_wp_at' live' t s proof (state)
this:
t \<in> set (ntfnQ (ntfnObj ntfn))

goal (1 subgoal):
 1. \<And>t. t \<in> set (ntfnQ (ntfnObj ntfn)) \<Longrightarrow> ko_wp_at' live' t s proof (chain)
picking this:
invs' s
ko_at' ntfn p s
t \<in> set (ntfnQ (ntfnObj ntfn)) proof (prove)
using this:
invs' s
ko_at' ntfn p s
t \<in> set (ntfnQ (ntfnObj ntfn))

goal (1 subgoal):
 1. ko_wp_at' live' t s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs' s; ko_at' ntfn p s; t \<in> set (ntfnQ (ntfnObj ntfn))\<rbrakk> \<Longrightarrow> ko_wp_at' live' t s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invs' s; t \<in> set (ntfnQ (ntfnObj ntfn))\<rbrakk> \<Longrightarrow> sym_refs (state_refs_of' s)
 2. \<lbrakk>invs' s; t \<in> set (ntfnQ (ntfnObj ntfn)); state_refs_of' s p = refs_of' (injectKOS ntfn) \<and> (\<forall>(x, tp)\<in>refs_of' (injectKOS ntfn). ko_wp_at' (\<lambda>ko. (p, symreftype tp) \<in> refs_of' ko) x s)\<rbrakk> \<Longrightarrow> ko_wp_at' live' t s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs' s; t \<in> set (ntfnQ (ntfnObj ntfn)); state_refs_of' s p = refs_of' (injectKOS ntfn) \<and> (\<forall>(x, tp)\<in>refs_of' (injectKOS ntfn). ko_wp_at' (\<lambda>ko. (p, symreftype tp) \<in> refs_of' ko) x s)\<rbrakk> \<Longrightarrow> ko_wp_at' live' t s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>invs' s; t \<in> set (ntfnQ (ntfnObj ntfn)); state_refs_of' s p = refs_of' (injectKOS ntfn) \<and> (\<forall>(x, tp)\<in>refs_of' (injectKOS ntfn). ko_wp_at' (\<lambda>ko. (p, symreftype tp) \<in> refs_of' ko) x s); ntfnObj ntfn = Structures_H.ntfn.IdleNtfn\<rbrakk> \<Longrightarrow> ko_wp_at' live' t s
 2. \<And>x2. \<lbrakk>invs' s; t \<in> set (ntfnQ (ntfnObj ntfn)); state_refs_of' s p = refs_of' (injectKOS ntfn) \<and> (\<forall>(x, tp)\<in>refs_of' (injectKOS ntfn). ko_wp_at' (\<lambda>ko. (p, symreftype tp) \<in> refs_of' ko) x s); ntfnObj ntfn = Structures_H.ntfn.ActiveNtfn x2\<rbrakk> \<Longrightarrow> ko_wp_at' live' t s
 3. \<And>x3. \<lbrakk>invs' s; t \<in> set (ntfnQ (ntfnObj ntfn)); state_refs_of' s p = refs_of' (injectKOS ntfn) \<and> (\<forall>(x, tp)\<in>refs_of' (injectKOS ntfn). ko_wp_at' (\<lambda>ko. (p, symreftype tp) \<in> refs_of' ko) x s); ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3\<rbrakk> \<Longrightarrow> ko_wp_at' live' t s proof (prove)
goal:
No subgoals! proof (state)
this:
ko_wp_at' live' t s

goal:
No subgoals!
theory Detype_C

lemma surj_tcb_ptr_to_ctcb_ptr [simp]:
  "surj tcb_ptr_to_ctcb_ptr" by (rule surjI [where f = "ctcb_ptr_to_tcb_ptr"], simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. surj tcb_ptr_to_ctcb_ptr
theory Detype_C

lemma bij_tcb_ptr_to_ctcb_ptr [simp]:
  "bij tcb_ptr_to_ctcb_ptr" by (simp add: bijI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bij tcb_ptr_to_ctcb_ptr
theory Detype_C

lemma inj_ctcb_ptr_to_tcb_ptr [simp]:
  "inj ctcb_ptr_to_tcb_ptr" apply (rule injI) apply (simp add: ctcb_ptr_to_tcb_ptr_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. inj ctcb_ptr_to_tcb_ptr proof (prove)
goal (1 subgoal):
 1. \<And>x y. ctcb_ptr_to_tcb_ptr x = ctcb_ptr_to_tcb_ptr y \<Longrightarrow> x = y proof (prove)
goal:
No subgoals!
theory Detype_C

lemma surj_ctcb_ptr_to_tcb_ptr [simp]:
  "surj ctcb_ptr_to_tcb_ptr" by (rule surjI [where f = "tcb_ptr_to_ctcb_ptr"], simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. surj ctcb_ptr_to_tcb_ptr
theory Detype_C

lemma cmap_relation_restrict_both:
  "\<lbrakk> cmap_relation am cm f rel; bij f\<rbrakk> \<Longrightarrow> cmap_relation (am |` (- S)) (cm |` (- f ` S)) f rel" unfolding cmap_relation_def apply (rule conjI) apply (clarsimp simp: image_Int bij_image_Compl_eq bij_def) apply (rule ballI) apply (clarsimp simp: image_iff2 bij_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cmap_relation am cm f rel; bij f\<rbrakk> \<Longrightarrow> cmap_relation (am|\<^bsub>(- S)\<^esub>) (cm|\<^bsub>(- f ` S)\<^esub>) f rel proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f ` dom am = dom cm \<and> (\<forall>x\<in>dom am. rel (the (am x)) (the (cm (f x)))); bij f\<rbrakk> \<Longrightarrow> f ` dom (am|\<^bsub>(- S)\<^esub>) = dom (cm|\<^bsub>(- f ` S)\<^esub>) \<and> (\<forall>x\<in>dom (am|\<^bsub>(- S)\<^esub>). rel (the ((am|\<^bsub>(- S)\<^esub>) x)) (the ((cm|\<^bsub>(- f ` S)\<^esub>) (f x)))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>f ` dom am = dom cm \<and> (\<forall>x\<in>dom am. rel (the (am x)) (the (cm (f x)))); bij f\<rbrakk> \<Longrightarrow> f ` dom (am|\<^bsub>(- S)\<^esub>) = dom (cm|\<^bsub>(- f ` S)\<^esub>)
 2. \<lbrakk>f ` dom am = dom cm \<and> (\<forall>x\<in>dom am. rel (the (am x)) (the (cm (f x)))); bij f\<rbrakk> \<Longrightarrow> \<forall>x\<in>dom (am|\<^bsub>(- S)\<^esub>). rel (the ((am|\<^bsub>(- S)\<^esub>) x)) (the ((cm|\<^bsub>(- f ` S)\<^esub>) (f x))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f ` dom am = dom cm \<and> (\<forall>x\<in>dom am. rel (the (am x)) (the (cm (f x)))); bij f\<rbrakk> \<Longrightarrow> \<forall>x\<in>dom (am|\<^bsub>(- S)\<^esub>). rel (the ((am|\<^bsub>(- S)\<^esub>) x)) (the ((cm|\<^bsub>(- f ` S)\<^esub>) (f x))) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>f ` dom am = dom cm \<and> (\<forall>x\<in>dom am. rel (the (am x)) (the (cm (f x)))); bij f; x \<in> dom (am|\<^bsub>(- S)\<^esub>)\<rbrakk> \<Longrightarrow> rel (the ((am|\<^bsub>(- S)\<^esub>) x)) (the ((cm|\<^bsub>(- f ` S)\<^esub>) (f x))) proof (prove)
goal:
No subgoals!
theory Detype_C

lemma tcb_ptr_to_ctcb_ptr_comp:
  "tcb_ptr_to_ctcb_ptr = Ptr o (\<lambda>p. p + ctcb_offset)" apply (rule ext) apply (simp add: tcb_ptr_to_ctcb_ptr_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_ptr_to_ctcb_ptr = tcb_Ptr \<circ> (\<lambda>p. p + ctcb_offset) proof (prove)
goal (1 subgoal):
 1. \<And>x. tcb_ptr_to_ctcb_ptr x = (tcb_Ptr \<circ> (\<lambda>p. p + ctcb_offset)) x proof (prove)
goal:
No subgoals!
theory Detype_C

lemma valid_untyped_cap_ctcb_member':
  fixes tcb :: tcb
  shows "\<lbrakk>s \<turnstile>' capability.UntypedCap d ptr bits idx; ko_at' tcb x s;
  ptr_val (tcb_ptr_to_ctcb_ptr x) \<in> {ptr..+2 ^ bits}\<rbrakk>
  \<Longrightarrow> x \<in> {ptr..+ 2 ^ bits}" apply (rule valid_untyped_capE, assumption) apply (simp only: upto_intvl_eq) apply (erule (2) valid_untyped_cap_ctcb_member) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_cap' (capability.UntypedCap d ptr bits idx) s; ko_at' tcb x s; ptr_val (tcb_ptr_to_ctcb_ptr x) \<in> {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> x \<in> {ptr..+2 ^ bits} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_cap' (capability.UntypedCap d ptr bits idx) s; ko_at' tcb x s; ptr_val (tcb_ptr_to_ctcb_ptr x) \<in> {ptr..+2 ^ bits}; is_aligned ptr bits; valid_untyped' d ptr bits idx s; ptr \<noteq> 0; bits < word_bits\<rbrakk> \<Longrightarrow> x \<in> {ptr..+2 ^ bits} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_cap' (capability.UntypedCap d ptr bits idx) s; ko_at' tcb x s; ptr_val (tcb_ptr_to_ctcb_ptr x) \<in> {ptr..ptr + 2 ^ bits - 1}; is_aligned ptr bits; valid_untyped' d ptr bits idx s; ptr \<noteq> 0; bits < word_bits\<rbrakk> \<Longrightarrow> x \<in> {ptr..ptr + 2 ^ bits - 1} proof (prove)
goal:
No subgoals!
theory Detype_C

lemma heap_to_user_data_restrict:
  "heap_to_user_data (mp |` S) bhp = (heap_to_user_data mp bhp |` S)" unfolding heap_to_user_data_def apply (rule ext) apply (case_tac "p \<in> S") apply (simp_all add: Let_def map_comp_def split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. heap_to_user_data (mp|\<^bsub>S\<^esub>) bhp = heap_to_user_data mp bhp|\<^bsub>S\<^esub> proof (prove)
goal (1 subgoal):
 1. (\<lambda>p. let uhp = map_to_user_data (mp|\<^bsub>S\<^esub>) in map_option (\<lambda>_. byte_to_word_heap bhp p) (uhp p)) = (\<lambda>p. let uhp = map_to_user_data mp in map_option (\<lambda>_. byte_to_word_heap bhp p) (uhp p))|\<^bsub>S\<^esub> proof (prove)
goal (1 subgoal):
 1. \<And>p. (let uhp = map_to_user_data (mp|\<^bsub>S\<^esub>) in map_option (\<lambda>_. byte_to_word_heap bhp p) (uhp p)) = ((\<lambda>p. let uhp = map_to_user_data mp in map_option (\<lambda>_. byte_to_word_heap bhp p) (uhp p))|\<^bsub>S\<^esub>) p proof (prove)
goal (2 subgoals):
 1. \<And>p. p \<in> S \<Longrightarrow> (let uhp = map_to_user_data (mp|\<^bsub>S\<^esub>) in map_option (\<lambda>_. byte_to_word_heap bhp p) (uhp p)) = ((\<lambda>p. let uhp = map_to_user_data mp in map_option (\<lambda>_. byte_to_word_heap bhp p) (uhp p))|\<^bsub>S\<^esub>) p
 2. \<And>p. p \<notin> S \<Longrightarrow> (let uhp = map_to_user_data (mp|\<^bsub>S\<^esub>) in map_option (\<lambda>_. byte_to_word_heap bhp p) (uhp p)) = ((\<lambda>p. let uhp = map_to_user_data mp in map_option (\<lambda>_. byte_to_word_heap bhp p) (uhp p))|\<^bsub>S\<^esub>) p proof (prove)
goal:
No subgoals!
theory Detype_C

lemma heap_to_device_data_restrict:
  "heap_to_device_data (mp |` S) bhp = (heap_to_device_data mp bhp |` S)" unfolding heap_to_device_data_def apply (rule ext) apply (case_tac "p \<in> S") apply (simp_all add: Let_def map_comp_def split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. heap_to_device_data (mp|\<^bsub>S\<^esub>) bhp = heap_to_device_data mp bhp|\<^bsub>S\<^esub> proof (prove)
goal (1 subgoal):
 1. (\<lambda>p. let uhp = map_to_user_data_device (mp|\<^bsub>S\<^esub>) in map_option (\<lambda>_. byte_to_word_heap bhp p) (uhp p)) = (\<lambda>p. let uhp = map_to_user_data_device mp in map_option (\<lambda>_. byte_to_word_heap bhp p) (uhp p))|\<^bsub>S\<^esub> proof (prove)
goal (1 subgoal):
 1. \<And>p. (let uhp = map_to_user_data_device (mp|\<^bsub>S\<^esub>) in map_option (\<lambda>_. byte_to_word_heap bhp p) (uhp p)) = ((\<lambda>p. let uhp = map_to_user_data_device mp in map_option (\<lambda>_. byte_to_word_heap bhp p) (uhp p))|\<^bsub>S\<^esub>) p proof (prove)
goal (2 subgoals):
 1. \<And>p. p \<in> S \<Longrightarrow> (let uhp = map_to_user_data_device (mp|\<^bsub>S\<^esub>) in map_option (\<lambda>_. byte_to_word_heap bhp p) (uhp p)) = ((\<lambda>p. let uhp = map_to_user_data_device mp in map_option (\<lambda>_. byte_to_word_heap bhp p) (uhp p))|\<^bsub>S\<^esub>) p
 2. \<And>p. p \<notin> S \<Longrightarrow> (let uhp = map_to_user_data_device (mp|\<^bsub>S\<^esub>) in map_option (\<lambda>_. byte_to_word_heap bhp p) (uhp p)) = ((\<lambda>p. let uhp = map_to_user_data_device mp in map_option (\<lambda>_. byte_to_word_heap bhp p) (uhp p))|\<^bsub>S\<^esub>) p proof (prove)
goal:
No subgoals!
theory Detype_C

lemma ccorres_grab_asm:
  "(Q \<Longrightarrow> ccorres_underlying sr G rr xf ar ax P P' hs f g) \<Longrightarrow>
   ccorres_underlying sr G rr xf ar ax (P and K Q) P' hs f g" by (fastforce simp: ccorres_underlying_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (Q \<Longrightarrow> ccorres_underlying sr G rr xf ar ax P P' hs f g) \<Longrightarrow> ccorres_underlying sr G rr xf ar ax (P and K Q) P' hs f g
theory Detype_C

lemma ksPSpace_ksMSu_comm:
  "ksPSpace_update f (ksMachineState_update g s) =
   ksMachineState_update g (ksPSpace_update f s)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ksPSpace_update f (ksMachineState_update g s) = ksMachineState_update g (ksPSpace_update f s)
theory Detype_C

lemma ksPSpace_update_ext:
  "(\<lambda>s. s\<lparr>ksPSpace := f (ksPSpace s)\<rparr>) = (ksPSpace_update f)" by (rule ext) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. s\<lparr>ksPSpace := f (ksPSpace s)\<rparr>) = ksPSpace_update f
theory Detype_C

lemma hrs_ghost_update_comm:
  "(t_hrs_'_update f \<circ> ghost'state_'_update g) =
   (ghost'state_'_update g \<circ> t_hrs_'_update f)" by (rule ext) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. t_hrs_'_update f \<circ> ghost'state_'_update g = ghost'state_'_update g \<circ> t_hrs_'_update f
theory Detype_C

lemma htd_safe_typ_region_bytes:
  "htd_safe S htd \<Longrightarrow> {ptr ..+ 2 ^ bits} \<subseteq> S \<Longrightarrow> htd_safe S (typ_region_bytes ptr bits htd)" apply (clarsimp simp: htd_safe_def dom_s_def typ_region_bytes_def) apply (simp add: subset_iff) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>htd_safe S htd; {ptr..+2 ^ bits} \<subseteq> S\<rbrakk> \<Longrightarrow> htd_safe S (typ_region_bytes ptr bits htd) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>{ptr..+2 ^ bits} \<subseteq> S; {(x, SIndexVal) |x. fst (htd x)} \<subseteq> S \<times> UNIV; {(x, SIndexTyp n) |x n. \<exists>a b. snd (htd x) n = Some (a, b)} \<subseteq> S \<times> UNIV\<rbrakk> \<Longrightarrow> {uu_. \<exists>x. (x \<in> {ptr..+2 ^ bits} \<longrightarrow> uu_ = (x, SIndexVal)) \<and> (x \<notin> {ptr..+2 ^ bits} \<longrightarrow> uu_ = (x, SIndexVal) \<and> fst (htd x))} \<subseteq> S \<times> UNIV \<and> {uu_. \<exists>x. (x \<in> {ptr..+2 ^ bits} \<longrightarrow> uu_ = (x, SIndexTyp 0)) \<and> (x \<notin> {ptr..+2 ^ bits} \<longrightarrow> (\<exists>n. uu_ = (x, SIndexTyp n) \<and> (\<exists>a b. snd (htd x) n = Some (a, b))))} \<subseteq> S \<times> UNIV proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>t. t \<in> {ptr..+2 ^ bits} \<longrightarrow> t \<in> S; \<forall>a. fst (htd a) \<longrightarrow> a \<in> S; \<forall>a. (\<exists>n aa b. snd (htd a) n = Some (aa, b)) \<longrightarrow> a \<in> S\<rbrakk> \<Longrightarrow> (\<forall>a. (\<exists>b x. (x \<in> {ptr..+2 ^ bits} \<longrightarrow> a = x \<and> b = SIndexVal) \<and> (x \<notin> {ptr..+2 ^ bits} \<longrightarrow> a = x \<and> b = SIndexVal \<and> fst (htd x))) \<longrightarrow> a \<in> S) \<and> (\<forall>a. (\<exists>b x. (x \<in> {ptr..+2 ^ bits} \<longrightarrow> a = x \<and> b = SIndexTyp 0) \<and> (x \<notin> {ptr..+2 ^ bits} \<longrightarrow> a = x \<and> (\<exists>n. b = SIndexTyp n \<and> (\<exists>a b. snd (htd x) n = Some (a, b))))) \<longrightarrow> a \<in> S) proof (prove)
goal:
No subgoals!
theory Detype_C

lemma offs_in_intvl_iff:
  "(p + x \<in> {p ..+ n}) = (unat x < n)" apply (simp add: intvl_def, safe) apply (erule order_le_less_trans[rotated], simp add: unat_of_nat) apply (rule exI, erule conjI[rotated]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (p + x \<in> {p..+n}) = (unat x < n) proof (prove)
goal (2 subgoals):
 1. \<And>k. \<lbrakk>k < n; x = word_of_nat k\<rbrakk> \<Longrightarrow> unat (word_of_nat k) < n
 2. unat x < n \<Longrightarrow> \<exists>k. x = word_of_nat k \<and> k < n proof (prove)
goal (1 subgoal):
 1. unat x < n \<Longrightarrow> \<exists>k. x = word_of_nat k \<and> k < n proof (prove)
goal (1 subgoal):
 1. x = word_of_nat (unat x) proof (prove)
goal:
No subgoals!
theory Detype_C

lemma objBits_koTypeOf:
  fixes v :: "'a :: pspace_storable" shows
  "objBits v = objBitsT (koType TYPE('a))" using project_inject[where v=v, THEN iffD2, OF refl]
      project_koType[THEN iffD1, OF exI[where x=v]] by (simp add: objBits_def objBitsT_koTypeOf[symmetric])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. objBits v = objBitsT (koType TYPE('a)) proof (prove)
using this:
projectKO_opt (injectKOS v) = Some v
projectKO_opt ?ko1 = Some v \<Longrightarrow> koTypeOf ?ko1 = koType TYPE('a)

goal (1 subgoal):
 1. objBits v = objBitsT (koType TYPE('a))
theory Detype_C

lemma map_comp_restrict_map:
  "(f \<circ>\<^sub>m (restrict_map m S)) = (restrict_map (f \<circ>\<^sub>m m) S)" by (rule ext, simp add: restrict_map_def map_comp_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f \<circ>\<^sub>m m|\<^bsub>S\<^esub> = (f \<circ>\<^sub>m m)|\<^bsub>S\<^esub>
theory Detype_C

lemma modify_machinestate_assert_cnodes_swap:
  "do x \<leftarrow> modify (ksMachineState_update f);
    y \<leftarrow> stateAssert (\<lambda>s. \<not> cNodePartialOverlap (gsCNodes s) S) []; g od
    = do y \<leftarrow> stateAssert (\<lambda>s. \<not> cNodePartialOverlap (gsCNodes s) S) [];
        x \<leftarrow> modify (ksMachineState_update f); g od" by (simp add: fun_eq_iff exec_modify stateAssert_def
                bind_assoc exec_get assert_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do x <- modify (ksMachineState_update f);
y <- stateAssert (\<lambda>s. \<not> cNodePartialOverlap (gsCNodes s) S) [];
g
od = do y <- stateAssert (\<lambda>s. \<not> cNodePartialOverlap (gsCNodes s) S) [];
x <- modify (ksMachineState_update f);
g
od