kings-crown/FVELER_Isabelle huggingface dataset:
theory Tcb_R

lemma slot_long_running_inv'[wp]:
  "\<lbrace>P\<rbrace> slotCapLongRunningDelete ptr \<lbrace>\<lambda>rv. P\<rbrace>" apply (simp add: slotCapLongRunningDelete_def) apply (rule hoare_seq_ext [OF _ getCTE_inv]) apply (rule hoare_pre, wpcw, (wp isFinalCapability_inv)+) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> slotCapLongRunningDelete ptr \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> do cte <- getCTE ptr;
case cteCap cte of capability.NullCap \<Rightarrow> return False | _ \<Rightarrow> do final <- isFinalCapability cte;
return $ final \<and> longRunningDelete (cteCap cte)
od
od \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrace>P\<rbrace> case cteCap cte of capability.NullCap \<Rightarrow> return False | _ \<Rightarrow> do final <- isFinalCapability cte;
return $ final \<and> longRunningDelete (cteCap cte)
od \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cte s. P s \<Longrightarrow> (\<forall>x. P s) \<and> P s \<and> (\<forall>x xa xb xc. P s) \<and> (\<forall>x. P s) \<and> (\<forall>x xa xb xc xd xe. P s) \<and> P s \<and> (\<forall>x xa xb. P s) \<and> (\<forall>x. P s) \<and> (\<forall>x xa xb. P s) \<and> (\<forall>x xa xb xc. P s) \<and> (\<forall>x xa xb xc. P s) \<and> P s proof (prove)
goal:
No subgoals!
theory Tcb_R

lemma cap_CNode_case_throw:
  "(case cap of CNodeCap a b c d \<Rightarrow> m | _ \<Rightarrow> throw x)
     = (doE unlessE (isCNodeCap cap) (throw x); m odE)" by (cases cap, simp_all add: isCap_simps unlessE_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (case cap of capability.CNodeCap a b c d \<Rightarrow> m | _ \<Rightarrow> throw x) = doE unlessE (isCNodeCap cap) (throw x);
m
odE
theory Tcb_R

lemma isThreadControl_def2:
  "isThreadControl tinv = (\<exists>a b c d e f g h. tinv = ThreadControl a b c d e f g h)" by (cases tinv, simp_all add: isThreadControl_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isThreadControl tinv = (\<exists>a b c d e f g h. tinv = tcbinvocation.ThreadControl a b c d e f g h)
theory Tcb_R

lemma lsft_real_cte:
  "\<lbrace>valid_objs'\<rbrace> lookupSlotForThread t x \<lbrace>\<lambda>rv. real_cte_at' rv\<rbrace>, -" apply (simp add: lookupSlotForThread_def) apply (wp resolveAddressBits_real_cte_at'|simp add: split_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs'\<rbrace> lookupSlotForThread t x \<lbrace>real_cte_at'\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs'\<rbrace> doE threadRootSlot <- liftE (getThreadCSpaceRoot t);
threadRoot <- liftE (getSlotCap threadRootSlot);
(s, uu_) <- CSpace_H.resolveAddressBits threadRoot x (size x);
returnOk s
odE \<lbrace>real_cte_at'\<rbrace>, - proof (prove)
goal:
No subgoals!
theory Tcb_R

lemma tcb_real_cte_16:
  "\<lbrakk> real_cte_at' (t+2^cteSizeBits) s; tcb_at' t s \<rbrakk> \<Longrightarrow> False" by (clarsimp simp: obj_at'_def projectKOs objBitsKO_def ps_clear_16)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>real_cte_at' (t + 2 ^ cteSizeBits) s; tcb_at' t s\<rbrakk> \<Longrightarrow> False
theory Tcb_R

lemma decodeSetTLSBase_corres:
  "corres (ser \<oplus> tcbinv_relation) (tcb_at t) (tcb_at' t)
          (decode_set_tls_base w (cap.ThreadCap t))
          (decodeSetTLSBase w (capability.ThreadCap t))" by (clarsimp simp: decode_set_tls_base_def decodeSetTLSBase_def returnOk_def
               split: list.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (ser \<oplus> tcbinv_relation) (tcb_at t) (tcb_at' t) (decode_set_tls_base w (cap.ThreadCap t)) (decodeSetTLSBase w (capability.ThreadCap t))
theory Tcb_R

lemma real_cte_at_not_tcb_at':
  "real_cte_at' x s \<Longrightarrow> \<not> tcb_at' x s"
  "real_cte_at' (x + 2^cteSizeBits) s \<Longrightarrow> \<not> tcb_at' x s" apply (clarsimp simp: obj_at'_def projectKOs) apply (clarsimp elim!: tcb_real_cte_16) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (real_cte_at' x s \<Longrightarrow> \<not> tcb_at' x s) &&& (real_cte_at' (x + 2 ^ cteSizeBits) s \<Longrightarrow> \<not> tcb_at' x s) proof (prove)
goal (1 subgoal):
 1. real_cte_at' (x + 2 ^ cteSizeBits) s \<Longrightarrow> \<not> tcb_at' x s proof (prove)
goal:
No subgoals!
theory Tcb_R

lemma decodeUnbindNotification_wf:
  "\<lbrace>invs' and tcb_at' t and ex_nonz_cap_to' t\<rbrace>
     decodeUnbindNotification (capability.ThreadCap t)
   \<lbrace>tcb_inv_wf'\<rbrace>,-" apply (simp add: decodeUnbindNotification_def) apply (wp getObject_tcb_wp | wpc | simp add: threadGet_def getBoundNotification_def)+ apply (auto simp: obj_at'_def pred_tcb_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and tcb_at' t and ex_nonz_cap_to' t\<rbrace> decodeUnbindNotification (capability.ThreadCap t) \<lbrace>tcb_inv_wf'\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and tcb_at' t and ex_nonz_cap_to' t\<rbrace> doE ntfn <- liftE (getBoundNotification t);
y <- case ntfn of None \<Rightarrow> throwError Fault_H.syscall_error.IllegalOperation | Some v15 \<Rightarrow> returnOk ();
returnOk (tcbinvocation.NotificationControl t None)
odE \<lbrace>tcb_inv_wf'\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s. invs' s \<and> tcb_at' t s \<and> ex_nonz_cap_to' t s \<Longrightarrow> bound_tcb_at' (\<lambda>rv. True) t s \<and> (\<exists>ta. ko_at' ta t s) proof (prove)
goal:
No subgoals!
theory Tcb_R

lemma decodeSetTLSBase_wf:
  "\<lbrace>invs' and tcb_at' t and ex_nonz_cap_to' t\<rbrace>
     decodeSetTLSBase w (capability.ThreadCap t)
   \<lbrace>tcb_inv_wf'\<rbrace>,-" apply (simp add: decodeSetTLSBase_def
             cong: list.case_cong) by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and tcb_at' t and ex_nonz_cap_to' t\<rbrace> decodeSetTLSBase w (capability.ThreadCap t) \<lbrace>tcb_inv_wf'\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and tcb_at' t and ex_nonz_cap_to' t\<rbrace> case w of [] \<Rightarrow> throwError Fault_H.syscall_error.TruncatedMessage | tls_base # x \<Rightarrow> returnOk (tcbinvocation.SetTLSBase t tls_base) \<lbrace>tcb_inv_wf'\<rbrace>, -
theory Detype_R

lemma null_filter_simp'[simp]:
  "null_filter' (null_filter' x) = null_filter' x" apply (rule ext) apply (auto simp:null_filter'_def split:if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. null_filter' (null_filter' x) = null_filter' x proof (prove)
goal (1 subgoal):
 1. \<And>xa. null_filter' (null_filter' x) xa = null_filter' x xa proof (prove)
goal:
No subgoals!
theory Detype_R

lemma descendants_rangeD':
  "\<lbrakk> descendants_range' cap p m; m \<turnstile> p \<rightarrow> p'; m p' = Some (CTE c n) \<rbrakk>
  \<Longrightarrow> capRange c \<inter> capRange cap = {}" by (simp add: descendants_range'_def descendants_of'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>descendants_range' cap p m; m \<turnstile> p \<rightarrow> p'; m p' = Some (CTE c n)\<rbrakk> \<Longrightarrow> capRange c \<inter> capRange cap = {}
theory Detype_R

lemma descendants_range_inD':
  "\<lbrakk>descendants_range_in' S p ms; p'\<in>descendants_of' p ms; ms p' = Some cte\<rbrakk>
   \<Longrightarrow> capRange (cteCap cte) \<inter> S = {}" apply (case_tac cte) apply (auto simp:descendants_range_in'_def cte_wp_at_ctes_of dest!:bspec) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>descendants_range_in' S p ms; p' \<in> descendants_of' p ms; ms p' = Some cte\<rbrakk> \<Longrightarrow> capRange (cteCap cte) \<inter> S = {} proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>descendants_range_in' S p ms; p' \<in> descendants_of' p ms; ms p' = Some cte; cte = CTE x1 x2\<rbrakk> \<Longrightarrow> capRange (cteCap cte) \<inter> S = {} proof (prove)
goal:
No subgoals!
theory Detype_R

lemma descendants_range'_def2:
  "descendants_range' cap p = descendants_range_in' (capRange cap) p" by (simp add: descendants_range_in'_def descendants_range'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. descendants_range' cap p = descendants_range_in' (capRange cap) p
theory Detype_R

lemma cte_map_obj_range_helper:
  "\<lbrakk> cte_at cref s; pspace_aligned s; valid_objs s \<rbrakk>
    \<Longrightarrow> \<exists>ko. kheap s (fst cref) = Some ko \<and> cte_map cref \<in> obj_range (fst cref) ko" apply (drule(2) cte_at_cte_map_in_obj_bits) apply (clarsimp simp: obj_range_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at (\<lambda>_. True) cref s; pspace_aligned s; valid_objs s\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s (fst cref) = Some ko \<and> cte_map cref \<in> obj_range (fst cref) ko proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_aligned s; valid_objs s; cte_map cref \<in> {fst cref..fst cref + 2 ^ obj_bits (the (kheap s (fst cref))) - 1} \<and> kheap s (fst cref) \<noteq> None\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s (fst cref) = Some ko \<and> cte_map cref \<in> obj_range (fst cref) ko proof (prove)
goal:
No subgoals!
theory Detype_R

lemma pspace_aligned'_cut:
  "pspace_aligned' s \<Longrightarrow>
   pspace_aligned' (s \<lparr> ksPSpace := \<lambda>x. if P x then None else ksPSpace s x\<rparr>)" by (simp add: pspace_aligned'_def dom_if_None)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pspace_aligned' s \<Longrightarrow> pspace_aligned' (s\<lparr>ksPSpace := \<lambda>x. if P x then None else ksPSpace s x\<rparr>)
theory Detype_R

lemma pspace_distinct'_cut:
  "pspace_distinct' s \<Longrightarrow>
   pspace_distinct' (s \<lparr> ksPSpace := \<lambda>x. if P x then None else ksPSpace s x\<rparr>)" by (simp add: pspace_distinct'_def dom_if_None ps_clear_def
                Diff_Int_distrib)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pspace_distinct' s \<Longrightarrow> pspace_distinct' (s\<lparr>ksPSpace := \<lambda>x. if P x then None else ksPSpace s x\<rparr>)
theory Detype_R

lemma obj_at_delete':
  "pspace_distinct' s \<Longrightarrow>
   obj_at' P p (s \<lparr> ksPSpace := \<lambda>x. if base \<le> x \<and> x \<le> base + (2 ^ magnitude - 1) then None else ksPSpace s x \<rparr>)
    = (\<not> (base \<le> p \<and> p \<le> base + (2 ^ magnitude - 1)) \<and> obj_at' P p s)" unfolding obj_at'_real_def by (rule ko_wp_at_delete')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pspace_distinct' s \<Longrightarrow> obj_at' P p (s\<lparr>ksPSpace := \<lambda>x. if base \<le> x \<and> x \<le> base + (2 ^ magnitude - 1) then None else ksPSpace s x\<rparr>) = (\<not> (base \<le> p \<and> p \<le> base + (2 ^ magnitude - 1)) \<and> obj_at' P p s) proof (prove)
goal (1 subgoal):
 1. pspace_distinct' s \<Longrightarrow> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> P obj) p (s\<lparr>ksPSpace := \<lambda>x. if base \<le> x \<and> x \<le> base + (2 ^ magnitude - 1) then None else ksPSpace s x\<rparr>) = (\<not> (base \<le> p \<and> p \<le> base + (2 ^ magnitude - 1)) \<and> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> P obj) p s)
theory Detype_R

lemma corres_machine_op:
  assumes P: "corres_underlying Id False True r P Q x x'"
  shows      "corres r (P \<circ> machine_state) (Q \<circ> ksMachineState)
                       (do_machine_op x) (doMachineOp x')" apply (rule corres_submonad3
              [OF submonad_do_machine_op submonad_doMachineOp _ _ _ _ P]) apply (simp_all add: state_relation_def swp_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres r (P \<circ> machine_state) (Q \<circ> ksMachineState) (do_machine_op x) (doMachineOp x') proof (prove)
goal (4 subgoals):
 1. \<forall>s s'. (s, s') \<in> state_relation \<and> True \<and> True \<longrightarrow> (machine_state s, ksMachineState s') \<in> Id
 2. \<forall>s s' ss ss'. (s, s') \<in> state_relation \<and> (ss, ss') \<in> Id \<longrightarrow> ((machine_state_update \<circ> K) ss s, (ksMachineState_update \<circ> K) ss' s') \<in> state_relation
 3. \<forall>s. (P \<circ> machine_state) s \<longrightarrow> True \<and> P (machine_state s)
 4. \<forall>s'. (Q \<circ> ksMachineState) s' \<longrightarrow> True \<and> Q (ksMachineState s') proof (prove)
goal:
No subgoals!
theory Detype_R

lemma ekheap_relation_detype:
  "ekheap_relation ekh kh \<Longrightarrow>
   ekheap_relation (\<lambda>x. if P x then None else (ekh x)) (\<lambda>x. if P x then None else (kh x))" by (fastforce simp add: ekheap_relation_def split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ekheap_relation ekh kh \<Longrightarrow> ekheap_relation (\<lambda>x. if P x then None else ekh x) (\<lambda>x. if P x then None else kh x)
theory Detype_R

lemma sym_refs_hyp_refs_triv[simp]: "sym_refs (state_hyp_refs_of s)" apply (auto simp: state_hyp_refs_of_def sym_refs_def) apply (case_tac "kheap s x"; simp add: hyp_refs_of_def) apply (rename_tac ko) apply (case_tac ko; clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sym_refs (state_hyp_refs_of s) proof (prove)
goal (1 subgoal):
 1. \<And>x a b. (a, b) \<in> (case kheap s x of None \<Rightarrow> {} | Some x2 \<Rightarrow> hyp_refs_of x2) \<Longrightarrow> (x, symreftype b) \<in> (case kheap s a of None \<Rightarrow> {} | Some x2 \<Rightarrow> hyp_refs_of x2) proof (prove)
goal (1 subgoal):
 1. \<And>x a b aa. \<lbrakk>(a, b) \<in> (case aa of TCB tcb \<Rightarrow> tcb_hyp_refs (tcb_arch tcb) | ArchObj x \<Rightarrow> refs_of_a x | _ \<Rightarrow> {}); kheap s x = Some aa\<rbrakk> \<Longrightarrow> (x, symreftype b) \<in> (case kheap s a of None \<Rightarrow> {} | Some (TCB tcb) \<Rightarrow> tcb_hyp_refs (tcb_arch tcb) | Some (ArchObj ao) \<Rightarrow> refs_of_a ao | Some _ \<Rightarrow> {}) proof (prove)
goal (1 subgoal):
 1. \<And>x a b ko. \<lbrakk>(a, b) \<in> (case ko of TCB tcb \<Rightarrow> tcb_hyp_refs (tcb_arch tcb) | ArchObj x \<Rightarrow> refs_of_a x | _ \<Rightarrow> {}); kheap s x = Some ko\<rbrakk> \<Longrightarrow> (x, symreftype b) \<in> (case kheap s a of None \<Rightarrow> {} | Some (TCB tcb) \<Rightarrow> tcb_hyp_refs (tcb_arch tcb) | Some (ArchObj ao) \<Rightarrow> refs_of_a ao | Some _ \<Rightarrow> {}) proof (prove)
goal:
No subgoals!
theory Detype_R

lemma caps_containedD':
  "\<lbrakk> ctes_of s p = Some cte; ctes_of s p' = Some cte';
     \<not> isUntypedCap (cteCap cte); capRange (cteCap cte) \<inter> untypedRange (cteCap cte') \<noteq> {};
     caps_contained' (ctes_of s) \<rbrakk> \<Longrightarrow>
     capRange (cteCap cte) \<subseteq> untypedRange (cteCap cte')" apply (cases cte, cases cte') apply (simp add: caps_contained'_def) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s p = Some cte; ctes_of s p' = Some cte'; \<not> isUntypedCap (cteCap cte); capRange (cteCap cte) \<inter> untypedRange (cteCap cte') \<noteq> {}; caps_contained' (ctes_of s)\<rbrakk> \<Longrightarrow> capRange (cteCap cte) \<subseteq> untypedRange (cteCap cte') proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a. \<lbrakk>ctes_of s p = Some cte; ctes_of s p' = Some cte'; \<not> isUntypedCap (cteCap cte); capRange (cteCap cte) \<inter> untypedRange (cteCap cte') \<noteq> {}; caps_contained' (ctes_of s); cte = CTE x1 x2; cte' = CTE x1a x2a\<rbrakk> \<Longrightarrow> capRange (cteCap cte) \<subseteq> untypedRange (cteCap cte') proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x1a x2a. \<lbrakk>ctes_of s p = Some (CTE x1 x2); ctes_of s p' = Some (CTE x1a x2a); \<not> isUntypedCap x1; capRange x1 \<inter> untypedRange x1a \<noteq> {}; \<forall>p p' c. (\<exists>n. ctes_of s p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. ctes_of s p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); cte = CTE x1 x2; cte' = CTE x1a x2a\<rbrakk> \<Longrightarrow> capRange x1 \<subseteq> untypedRange x1a proof (prove)
goal:
No subgoals!
theory Detype_R

lemma untyped_mdbD':
  "\<lbrakk> ctes p = Some cte; ctes p' = Some cte';
     isUntypedCap (cteCap cte); capRange (cteCap cte') \<inter> untypedRange (cteCap cte) \<noteq> {};
     \<not> isUntypedCap (cteCap cte');
     untyped_mdb' ctes \<rbrakk> \<Longrightarrow> p' \<in> descendants_of' p ctes" by (cases cte, cases cte', simp add: untyped_mdb'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes p = Some cte; ctes p' = Some cte'; isUntypedCap (cteCap cte); capRange (cteCap cte') \<inter> untypedRange (cteCap cte) \<noteq> {}; \<not> isUntypedCap (cteCap cte'); untyped_mdb' ctes\<rbrakk> \<Longrightarrow> p' \<in> descendants_of' p ctes
theory Detype_R

lemma ko_wp_at_state_refs_ofD:
  "\<lbrakk> ko_wp_at' P p s \<rbrakk> \<Longrightarrow> (\<exists>ko. P ko \<and> state_refs_of' s p = refs_of' ko)" by (fastforce simp: ko_wp_at'_def state_refs_of'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ko_wp_at' P p s \<Longrightarrow> \<exists>ko. P ko \<and> state_refs_of' s p = refs_of' ko
theory Detype_R

lemma sym_refs_ko_wp_atD:
  "\<lbrakk> ko_wp_at' P p s; sym_refs (state_refs_of' s) \<rbrakk>
      \<Longrightarrow> (\<exists>ko. P ko \<and> state_refs_of' s p = refs_of' ko
                    \<and> (\<forall>(x, tp) \<in> refs_of' ko. (p, symreftype tp) \<in> state_refs_of' s x))" apply (clarsimp dest!: ko_wp_at_state_refs_ofD) apply (rule exI, erule conjI) apply (drule sym) apply clarsimp apply (erule(1) sym_refsD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_wp_at' P p s; sym_refs (state_refs_of' s)\<rbrakk> \<Longrightarrow> \<exists>ko. P ko \<and> state_refs_of' s p = refs_of' ko \<and> (\<forall>(x, tp)\<in>refs_of' ko. (p, symreftype tp) \<in> state_refs_of' s x) proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>sym_refs (state_refs_of' s); P ko; state_refs_of' s p = refs_of' ko\<rbrakk> \<Longrightarrow> \<exists>koa. P koa \<and> refs_of' ko = refs_of' koa \<and> (\<forall>x\<in>refs_of' koa. case x of (x, tp) \<Rightarrow> (p, symreftype tp) \<in> state_refs_of' s x) proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>sym_refs (state_refs_of' s); state_refs_of' s p = refs_of' ko\<rbrakk> \<Longrightarrow> refs_of' ko = refs_of' ko \<and> (\<forall>x\<in>refs_of' ko. case x of (x, tp) \<Rightarrow> (p, symreftype tp) \<in> state_refs_of' s x) proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>sym_refs (state_refs_of' s); refs_of' ko = state_refs_of' s p\<rbrakk> \<Longrightarrow> refs_of' ko = refs_of' ko \<and> (\<forall>x\<in>refs_of' ko. case x of (x, tp) \<Rightarrow> (p, symreftype tp) \<in> state_refs_of' s x) proof (prove)
goal (1 subgoal):
 1. \<And>ko a b. \<lbrakk>sym_refs (state_refs_of' s); refs_of' ko = state_refs_of' s p; (a, b) \<in> state_refs_of' s p\<rbrakk> \<Longrightarrow> (p, symreftype b) \<in> state_refs_of' s a proof (prove)
goal:
No subgoals!
theory Detype_R

lemma zobj_refs_capRange:
  "capAligned c \<Longrightarrow> zobj_refs' c \<subseteq> capRange c" by (cases c, simp_all add: capRange_def capAligned_def is_aligned_no_overflow)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. capAligned c \<Longrightarrow> zobj_refs' c \<subseteq> capRange c
theory Detype_R

lemma ko_wp_at'[simp]:
  "\<And>P p. (ko_wp_at' P p state') = (ko_wp_at' P p s \<and> p \<notin> base_bits)" by (fastforce simp add: ko_wp_at_delete'[OF pd])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>P p. ko_wp_at' P p state' = (ko_wp_at' P p s \<and> p \<notin> base_bits)
theory Detype_R

lemma obj_at'[simp]:
  "\<And>P p. (obj_at' P p state') = (obj_at' P p s \<and> p \<notin> base_bits)" by (fastforce simp add: obj_at'_real_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>P p. obj_at' P p state' = (obj_at' P p s \<and> p \<notin> base_bits)
theory Detype_R

lemma typ_at'[simp]:
  "\<And>T p. (typ_at' P p state') = (typ_at' P p s \<and> p \<notin> base_bits)" by (simp add: typ_at'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>T p. typ_at' P p state' = (typ_at' P p s \<and> p \<notin> base_bits)
theory Detype_R

lemma valid_untyped[simp]:
  "s \<turnstile>' UntypedCap d base bits idx" using cte_wp_at_valid_objs_valid_cap' [OF cap valid_objs] by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_cap' (capability.UntypedCap d base bits idx) s proof (prove)
using this:
\<exists>cte. cteCap cte = capability.UntypedCap d base bits idx \<and> valid_cap' (cteCap cte) s

goal (1 subgoal):
 1. valid_cap' (capability.UntypedCap d base bits idx) s
theory Detype_R

lemma cte_wp_at'[simp]:
  "\<And>P p. (cte_wp_at' P p state') = (cte_wp_at' P p s \<and> p \<notin> base_bits)" by (fastforce simp:cte_wp_at_delete'[where idx = idx,OF valid_untyped pd ])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>P p. cte_wp_at' P p state' = (cte_wp_at' P p s \<and> p \<notin> base_bits)
theory Detype_R

lemma ctes_of_valid [elim!]:
  "ctes_of s p = Some cte \<Longrightarrow> s \<turnstile>' cteCap cte" by (case_tac cte, simp add: ctes_of_valid_cap' [OF _ valid_objs])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ctes_of s p = Some cte \<Longrightarrow> valid_cap' (cteCap cte) s
theory Detype_R

lemma valid_cap2:
  "\<lbrakk> cte_wp_at' (\<lambda>cte. cteCap cte = c) p s \<rbrakk> \<Longrightarrow> state' \<turnstile>' c" apply (case_tac "isUntypedCap c") apply (drule cte_wp_at_valid_objs_valid_cap' [OF _ valid_objs]) apply (clarsimp simp: valid_cap'_def isCap_simps valid_untyped'_def) apply (rule valid_cap'[rotated], assumption) apply (clarsimp simp: cte_wp_at_ctes_of dest!: objRefs_notrange) apply (clarsimp simp: cte_wp_at_ctes_of) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at' (\<lambda>cte. cteCap cte = c) p s \<Longrightarrow> valid_cap' c state' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; isUntypedCap c\<rbrakk> \<Longrightarrow> valid_cap' c state'
 2. \<lbrakk>cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; \<not> isUntypedCap c\<rbrakk> \<Longrightarrow> valid_cap' c state' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>isUntypedCap c; \<exists>cte. cteCap cte = c \<and> valid_cap' (cteCap cte) s\<rbrakk> \<Longrightarrow> valid_cap' c state'
 2. \<lbrakk>cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; \<not> isUntypedCap c\<rbrakk> \<Longrightarrow> valid_cap' c state' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; \<not> isUntypedCap c\<rbrakk> \<Longrightarrow> valid_cap' c state' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; \<not> isUntypedCap c\<rbrakk> \<Longrightarrow> capRange c \<inter> base_bits = {}
 2. \<lbrakk>cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; \<not> isUntypedCap c\<rbrakk> \<Longrightarrow> valid_cap' c s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; \<not> isUntypedCap c\<rbrakk> \<Longrightarrow> valid_cap' c s proof (prove)
goal:
No subgoals!