kings-crown/FVELER_Isabelle huggingface dataset:
theory Invariants_H

lemma ntfn_q_refs_of'_simps[simp]:
 "ntfn_q_refs_of'  IdleNtfn         = {}"
 "ntfn_q_refs_of' (WaitingNtfn q)      = set q \<times> {NTFNSignal}"
 "ntfn_q_refs_of' (ActiveNtfn b)  = {}" by (auto simp: ntfn_q_refs_of'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ntfn_q_refs_of' Structures_H.ntfn.IdleNtfn = {} &&& ntfn_q_refs_of' (Structures_H.ntfn.WaitingNtfn q) = set q \<times> {NTFNSignal} &&& ntfn_q_refs_of' (Structures_H.ntfn.ActiveNtfn b) = {}
theory Invariants_H

lemma ntfn_bound_refs'_simps[simp]:
  "ntfn_bound_refs' (Some t) = {(t, NTFNBound)}"
  "ntfn_bound_refs' None = {}" by (auto simp: ntfn_bound_refs'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ntfn_bound_refs' (Some t) = {(t, NTFNBound)} &&& ntfn_bound_refs' None = {}
theory Invariants_H

lemma tcb_bound_refs'_simps[simp]:
  "tcb_bound_refs' (Some a) = {(a, TCBBound)}"
  "tcb_bound_refs' None = {}" by (auto simp: tcb_bound_refs'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_bound_refs' (Some a) = {(a, TCBBound)} &&& tcb_bound_refs' None = {}
theory Invariants_H

lemma refs_of_rev':
 "(x, TCBBlockedRecv) \<in> refs_of' ko =
    (\<exists>tcb. ko = KOTCB tcb \<and> (\<exists>a. tcbState tcb = BlockedOnReceive x a))"
 "(x, TCBBlockedSend) \<in> refs_of' ko =
    (\<exists>tcb. ko = KOTCB tcb \<and> (\<exists>a b c d. tcbState tcb = BlockedOnSend x a b c d))"
 "(x, TCBSignal) \<in> refs_of' ko =
    (\<exists>tcb. ko = KOTCB tcb \<and> tcbState tcb = BlockedOnNotification x)"
 "(x, EPRecv) \<in> refs_of' ko =
    (\<exists>ep. ko = KOEndpoint ep \<and> (\<exists>q. ep = RecvEP q \<and> x \<in> set q))"
 "(x, EPSend) \<in> refs_of' ko =
    (\<exists>ep. ko = KOEndpoint ep \<and> (\<exists>q. ep = SendEP q \<and> x \<in> set q))"
 "(x, NTFNSignal) \<in> refs_of' ko =
    (\<exists>ntfn. ko = KONotification ntfn \<and> (\<exists>q. ntfnObj ntfn = WaitingNtfn q \<and> x \<in> set q))"
 "(x, TCBBound) \<in>  refs_of' ko =
    (\<exists>tcb. ko = KOTCB tcb \<and> (tcbBoundNotification tcb = Some x))"
 "(x, NTFNBound) \<in> refs_of' ko =
    (\<exists>ntfn. ko = KONotification ntfn \<and> (ntfnBoundTCB ntfn = Some x))" by (auto simp: refs_of'_def
                 tcb_st_refs_of'_def
                 ep_q_refs_of'_def
                 ntfn_q_refs_of'_def
                 ntfn_bound_refs'_def
                 tcb_bound_refs'_def
          split: Structures_H.kernel_object.splits
                 Structures_H.thread_state.splits
                 Structures_H.endpoint.splits
                 Structures_H.notification.splits
                 Structures_H.ntfn.splits)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((((x, TCBBlockedRecv) \<in> refs_of' ko) = (\<exists>tcb. ko = KOTCB tcb \<and> (\<exists>a. tcbState tcb = Structures_H.thread_state.BlockedOnReceive x a)) &&& ((x, TCBBlockedSend) \<in> refs_of' ko) = (\<exists>tcb. ko = KOTCB tcb \<and> (\<exists>a b c d. tcbState tcb = Structures_H.thread_state.BlockedOnSend x a b c d))) &&& ((x, TCBSignal) \<in> refs_of' ko) = (\<exists>tcb. ko = KOTCB tcb \<and> tcbState tcb = Structures_H.thread_state.BlockedOnNotification x) &&& ((x, EPRecv) \<in> refs_of' ko) = (\<exists>ep. ko = KOEndpoint ep \<and> (\<exists>q. ep = Structures_H.endpoint.RecvEP q \<and> x \<in> set q))) &&& (((x, EPSend) \<in> refs_of' ko) = (\<exists>ep. ko = KOEndpoint ep \<and> (\<exists>q. ep = Structures_H.endpoint.SendEP q \<and> x \<in> set q)) &&& ((x, NTFNSignal) \<in> refs_of' ko) = (\<exists>ntfn. ko = KONotification ntfn \<and> (\<exists>q. ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn q \<and> x \<in> set q))) &&& ((x, TCBBound) \<in> refs_of' ko) = (\<exists>tcb. ko = KOTCB tcb \<and> tcbBoundNotification tcb = Some x) &&& ((x, NTFNBound) \<in> refs_of' ko) = (\<exists>ntfn. ko = KONotification ntfn \<and> ntfnBoundTCB ntfn = Some x)
theory Invariants_H

lemma ko_wp_at'_weakenE:
  "\<lbrakk> ko_wp_at' P p s; \<And>ko. P ko \<Longrightarrow> Q ko \<rbrakk> \<Longrightarrow> ko_wp_at' Q p s" by (clarsimp simp: ko_wp_at'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_wp_at' P p s; \<And>ko. P ko \<Longrightarrow> Q ko\<rbrakk> \<Longrightarrow> ko_wp_at' Q p s
theory Invariants_H

lemma projectKO_opt_tcbD:
  "projectKO_opt ko = Some (tcb :: tcb) \<Longrightarrow> ko = KOTCB tcb" by (cases ko, simp_all add: projectKO_opt_tcb)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. projectKO_opt ko = Some tcb \<Longrightarrow> ko = KOTCB tcb
theory Invariants_H

lemma st_tcb_at_refs_of_rev':
  "ko_wp_at' (\<lambda>ko. (x, TCBBlockedRecv) \<in> refs_of' ko) t s
     = st_tcb_at' (\<lambda>ts. \<exists>a. ts = BlockedOnReceive x a) t s"
  "ko_wp_at' (\<lambda>ko. (x, TCBBlockedSend) \<in> refs_of' ko) t s
     = st_tcb_at' (\<lambda>ts. \<exists>a b c d. ts = BlockedOnSend x a b c d) t s"
  "ko_wp_at' (\<lambda>ko. (x, TCBSignal) \<in> refs_of' ko) t s
     = st_tcb_at' (\<lambda>ts. ts = BlockedOnNotification x) t s" by (fastforce simp: refs_of_rev' pred_tcb_at'_def obj_at'_real_def
                     projectKO_opt_tcb[where e="KOTCB y" for y]
              elim!: ko_wp_at'_weakenE
              dest!: projectKO_opt_tcbD)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ko_wp_at' (\<lambda>ko. (x, TCBBlockedRecv) \<in> refs_of' ko) t s = st_tcb_at' (\<lambda>ts. \<exists>a. ts = Structures_H.thread_state.BlockedOnReceive x a) t s &&& ko_wp_at' (\<lambda>ko. (x, TCBBlockedSend) \<in> refs_of' ko) t s = st_tcb_at' (\<lambda>ts. \<exists>a b c d. ts = Structures_H.thread_state.BlockedOnSend x a b c d) t s &&& ko_wp_at' (\<lambda>ko. (x, TCBSignal) \<in> refs_of' ko) t s = st_tcb_at' (\<lambda>ts. ts = Structures_H.thread_state.BlockedOnNotification x) t s
theory Invariants_H

lemma state_refs_of'_elemD:
  "\<lbrakk> ref \<in> state_refs_of' s x \<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>obj. ref \<in> refs_of' obj) x s" by (clarsimp simp add: state_refs_of'_def ko_wp_at'_def
                  split: option.splits if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ref \<in> state_refs_of' s x \<Longrightarrow> ko_wp_at' (\<lambda>obj. ref \<in> refs_of' obj) x s
theory Invariants_H

lemma obj_at_state_refs_ofD':
  "obj_at' P p s \<Longrightarrow> \<exists>obj. P obj \<and> state_refs_of' s p = refs_of' (injectKO obj)" apply (clarsimp simp: obj_at'_real_def project_inject ko_wp_at'_def conj_commute) apply (rule exI, erule conjI) apply (clarsimp simp: state_refs_of'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_at' P p s \<Longrightarrow> \<exists>obj. P obj \<and> state_refs_of' s p = refs_of' (injectKO obj) proof (prove)
goal (1 subgoal):
 1. \<And>obj. \<lbrakk>ksPSpace s p = Some (injectKO obj); is_aligned p (objBitsKO (injectKO obj)); ps_clear p (objBitsKO (injectKO obj)) s; P obj\<rbrakk> \<Longrightarrow> \<exists>obj. P obj \<and> state_refs_of' s p = refs_of' (injectKO obj) proof (prove)
goal (1 subgoal):
 1. \<And>obj. \<lbrakk>ksPSpace s p = Some (injectKO obj); is_aligned p (objBitsKO (injectKO obj)); ps_clear p (objBitsKO (injectKO obj)) s\<rbrakk> \<Longrightarrow> state_refs_of' s p = refs_of' (injectKO obj) proof (prove)
goal:
No subgoals!
theory Invariants_H

lemma ko_at_state_refs_ofD':
  "ko_at' ko p s \<Longrightarrow> state_refs_of' s p = refs_of' (injectKO ko)" by (clarsimp dest!: obj_at_state_refs_ofD')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ko_at' ko p s \<Longrightarrow> state_refs_of' s p = refs_of' (injectKO ko)
theory Invariants_H

lemma bound_tcb_at_state_refs_ofD':
  "bound_tcb_at' P t s \<Longrightarrow> \<exists>ts ntfnptr. P ntfnptr \<and> obj_at' (tcb_ntfn_is_bound' ntfnptr) t s
          \<and> state_refs_of' s t = (tcb_st_refs_of' ts \<union> tcb_bound_refs' ntfnptr)" by (auto simp: pred_tcb_at'_def obj_at'_def tcb_ntfn_is_bound'_def projectKO_eq
                 project_inject state_refs_of'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bound_tcb_at' P t s \<Longrightarrow> \<exists>ts ntfnptr. P ntfnptr \<and> obj_at' (tcb_ntfn_is_bound' ntfnptr) t s \<and> state_refs_of' s t = tcb_st_refs_of' ts \<union> tcb_bound_refs' ntfnptr
theory Invariants_H

lemma sym_refs_obj_atD':
  "\<lbrakk> obj_at' P p s; sym_refs (state_refs_of' s) \<rbrakk> \<Longrightarrow>
     \<exists>obj. P obj \<and> state_refs_of' s p = refs_of' (injectKO obj)
        \<and> (\<forall>(x, tp)\<in>refs_of' (injectKO obj). ko_wp_at' (\<lambda>ko. (p, symreftype tp) \<in> refs_of' ko) x s)" apply (drule obj_at_state_refs_ofD') apply (erule exEI, clarsimp) apply (drule sym, simp) apply (drule(1) sym_refsD) apply (erule state_refs_of'_elemD) done

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

lemma sym_refs_ko_atD':
  "\<lbrakk> ko_at' ko p s; sym_refs (state_refs_of' s) \<rbrakk> \<Longrightarrow>
     state_refs_of' s p = refs_of' (injectKO ko) \<and>
     (\<forall>(x, tp)\<in>refs_of' (injectKO ko). ko_wp_at' (\<lambda>ko. (p, symreftype tp) \<in> refs_of' ko) x s)" by (drule(1) sym_refs_obj_atD', simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at' ko p s; sym_refs (state_refs_of' s)\<rbrakk> \<Longrightarrow> state_refs_of' s p = refs_of' (injectKO ko) \<and> (\<forall>(x, tp)\<in>refs_of' (injectKO ko). ko_wp_at' (\<lambda>ko. (p, symreftype tp) \<in> refs_of' ko) x s)
theory Invariants_H

lemma if_live_then_nonz_capE':
  "\<lbrakk> if_live_then_nonz_cap' s; ko_wp_at' live' p s \<rbrakk>
     \<Longrightarrow> ex_nonz_cap_to' p s" by (fastforce simp: if_live_then_nonz_cap'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>if_live_then_nonz_cap' s; ko_wp_at' live' p s\<rbrakk> \<Longrightarrow> ex_nonz_cap_to' p s
theory Invariants_H

lemma if_live_then_nonz_capD':
  assumes x: "if_live_then_nonz_cap' s" "ko_wp_at' P p s"
  assumes y: "\<And>obj. \<lbrakk> P obj; ksPSpace s p = Some obj; is_aligned p (objBitsKO obj) \<rbrakk> \<Longrightarrow> live' obj"
  shows "ex_nonz_cap_to' p s" using x by (clarsimp elim!: if_live_then_nonz_capE' y
                simp: ko_wp_at'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ex_nonz_cap_to' p s proof (prove)
using this:
if_live_then_nonz_cap' s
ko_wp_at' P p s

goal (1 subgoal):
 1. ex_nonz_cap_to' p s
theory Invariants_H

lemma if_live_state_refsE:
  "\<lbrakk> if_live_then_nonz_cap' s;
     state_refs_of' s p \<noteq> {} \<rbrakk> \<Longrightarrow> ex_nonz_cap_to' p s" by (clarsimp simp: state_refs_of'_def ko_wp_at'_def
              split: option.splits if_split_asm
              elim!: refs_of_live' if_live_then_nonz_capE')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>if_live_then_nonz_cap' s; state_refs_of' s p \<noteq> {}\<rbrakk> \<Longrightarrow> ex_nonz_cap_to' p s
theory Invariants_H

lemma if_unsafe_then_capD':
  "\<lbrakk> cte_wp_at' P p s; if_unsafe_then_cap' s; \<And>cte. P cte \<Longrightarrow> cteCap cte \<noteq> NullCap \<rbrakk>
     \<Longrightarrow> ex_cte_cap_to' p s" unfolding if_unsafe_then_cap'_def apply (erule allE, erule mp) apply (clarsimp simp: cte_wp_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at' P p s; if_unsafe_then_cap' s; \<And>cte. P cte \<Longrightarrow> cteCap cte \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) p s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at' P p s; \<forall>cref. cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) cref s \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) cref s; \<And>cte. P cte \<Longrightarrow> cteCap cte \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) p s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at' P p s; \<And>cte. P cte \<Longrightarrow> cteCap cte \<noteq> capability.NullCap\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) p s proof (prove)
goal:
No subgoals!
theory Invariants_H

lemma max_ipc_words:
  "max_ipc_words = 0x80" unfolding max_ipc_words_def by (simp add: msgMaxLength_def msgLengthBits_def msgMaxExtraCaps_def msgExtraCapBits_def capTransferDataSize_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. max_ipc_words = 0x80 proof (prove)
goal (1 subgoal):
 1. capTransferDataSize + msgMaxLength + msgMaxExtraCaps + 2 = 0x80
theory Invariants_H

lemma valid_objsE' [elim]:
  "\<lbrakk> valid_objs' s; ksPSpace s x = Some obj; valid_obj' obj s \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R" unfolding valid_objs'_def by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs' s; ksPSpace s x = Some obj; valid_obj' obj s \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>obj\<in>ran (ksPSpace s). valid_obj' obj s; ksPSpace s x = Some obj; valid_obj' obj s \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R
theory Invariants_H

lemma pspace_distinctD':
  "\<lbrakk> ksPSpace s x = Some v; pspace_distinct' s \<rbrakk> \<Longrightarrow> ps_clear x (objBitsKO v) s" apply (simp add: pspace_distinct'_def) apply (drule bspec, erule domI) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s x = Some v; pspace_distinct' s\<rbrakk> \<Longrightarrow> ps_clear x (objBitsKO v) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s x = Some v; \<forall>x\<in>dom (ksPSpace s). ps_clear x (objBitsKO (the (ksPSpace s x))) s\<rbrakk> \<Longrightarrow> ps_clear x (objBitsKO v) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s x = Some v; ps_clear x (objBitsKO (the (ksPSpace s x))) s\<rbrakk> \<Longrightarrow> ps_clear x (objBitsKO v) s proof (prove)
goal:
No subgoals!
theory Invariants_H

lemma pspace_alignedD':
  "\<lbrakk> ksPSpace s x = Some v; pspace_aligned' s \<rbrakk> \<Longrightarrow> is_aligned x (objBitsKO v)" apply (simp add: pspace_aligned'_def) apply (drule bspec, erule domI) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s x = Some v; pspace_aligned' s\<rbrakk> \<Longrightarrow> is_aligned x (objBitsKO v) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s x = Some v; \<forall>x\<in>dom (ksPSpace s). is_aligned x (objBitsKO (the (ksPSpace s x)))\<rbrakk> \<Longrightarrow> is_aligned x (objBitsKO v) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s x = Some v; is_aligned x (objBitsKO (the (ksPSpace s x)))\<rbrakk> \<Longrightarrow> is_aligned x (objBitsKO v) proof (prove)
goal:
No subgoals!
theory Invariants_H

lemma next_unfold:
  "mdb_next s c =
   (case s c of Some cte \<Rightarrow> Some (mdbNext (cteMDBNode cte)) | None \<Rightarrow> None)" by (simp add: mdb_next_def split: option.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdb_next s c = (case s c of None \<Rightarrow> None | Some cte \<Rightarrow> Some (mdbNext (cteMDBNode cte)))
theory Invariants_H

lemma sch_act_sane_not:
  "sch_act_sane s = sch_act_not (ksCurThread s) s" by (auto simp: sch_act_sane_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sch_act_sane s = sch_act_not (ksCurThread s) s
theory Invariants_H

lemma objBits_cte_conv:
  "objBits (cte :: cte) = cteSizeBits" by (simp add: objBits_def objBitsKO_def wordSizeCase_def word_size)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. objBits cte = cteSizeBits
theory Invariants_H

lemma valid_pde_mapping'_simps[simp]:
 "valid_pde_mapping' offset (InvalidPDE) = True"
 "valid_pde_mapping' offset (SectionPDE ptr a b c d e w)
     = valid_pde_mapping_offset' offset"
 "valid_pde_mapping' offset (SuperSectionPDE ptr a' b' c' d' w)
     = valid_pde_mapping_offset' offset"
 "valid_pde_mapping' offset (PageTablePDE ptr x z'')
     = valid_pde_mapping_offset' offset" by (clarsimp simp: valid_pde_mapping'_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (valid_pde_mapping' offset ARM_H.InvalidPDE = True &&& valid_pde_mapping' offset (ARM_H.SectionPDE ptr a b c d e w) = valid_pde_mapping_offset' offset) &&& valid_pde_mapping' offset (ARM_H.SuperSectionPDE ptr a' b' c' d' w) = valid_pde_mapping_offset' offset &&& valid_pde_mapping' offset (ARM_H.PageTablePDE ptr x z'') = valid_pde_mapping_offset' offset
theory Invariants_H

lemma valid_pspaceI' [intro]:
  "\<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; valid_mdb' s; no_0_obj' s\<rbrakk>
  \<Longrightarrow> valid_pspace' s" unfolding valid_pspace'_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; valid_mdb' s; no_0_obj' s\<rbrakk> \<Longrightarrow> valid_pspace' s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; valid_mdb' s; no_0_obj' s\<rbrakk> \<Longrightarrow> (valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb') s
theory Invariants_H

lemma valid_pspaceE' [elim]:
  "\<lbrakk>valid_pspace' s;
    \<lbrakk> valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s;
      valid_mdb' s\<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R" unfolding valid_pspace'_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_pspace' s; \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb') s; \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R
theory Invariants_H

lemma idle'_no_refs:
  "valid_idle' s \<Longrightarrow> state_refs_of' s (ksIdleThread s) = {}" by (clarsimp simp: valid_idle'_def pred_tcb_at'_def obj_at'_def tcb_ntfn_is_bound'_def
                     projectKO_eq project_inject state_refs_of'_def idle_tcb'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_idle' s \<Longrightarrow> state_refs_of' s (ksIdleThread s) = {}
theory Invariants_H

lemma idle'_not_queued':
  "\<lbrakk>valid_idle' s; sym_refs (state_refs_of' s);
    state_refs_of' s ptr = insert t queue \<times> {rt}\<rbrakk>\<Longrightarrow>
   ksIdleThread s \<notin> queue" by (frule idle'_no_refs, fastforce simp: valid_idle'_def sym_refs_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle' s; sym_refs (state_refs_of' s); state_refs_of' s ptr = insert t queue \<times> {rt}\<rbrakk> \<Longrightarrow> ksIdleThread s \<notin> queue
theory Invariants_H

lemma idle'_not_queued:
  "\<lbrakk>valid_idle' s; sym_refs (state_refs_of' s);
    state_refs_of' s ptr = queue \<times> {rt}\<rbrakk> \<Longrightarrow>
   ksIdleThread s \<notin> queue" by (frule idle'_no_refs, fastforce simp: valid_idle'_def sym_refs_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle' s; sym_refs (state_refs_of' s); state_refs_of' s ptr = queue \<times> {rt}\<rbrakk> \<Longrightarrow> ksIdleThread s \<notin> queue
theory Invariants_H

lemma obj_at_conj':
  "\<lbrakk> obj_at' P p s; obj_at' Q p s \<rbrakk> \<Longrightarrow> obj_at' (\<lambda>k. P k \<and> Q k) p s" by (auto simp: obj_at'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>obj_at' P p s; obj_at' Q p s\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>k. P k \<and> Q k) p s
theory Invariants_H

lemma pred_tcb_at_conj':
  "\<lbrakk> pred_tcb_at' proj P t s; pred_tcb_at' proj Q t s \<rbrakk> \<Longrightarrow> pred_tcb_at' proj (\<lambda>a. P a \<and> Q a) t s" apply (simp add: pred_tcb_at'_def) apply (erule (1) obj_at_conj') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pred_tcb_at' proj P t s; pred_tcb_at' proj Q t s\<rbrakk> \<Longrightarrow> pred_tcb_at' proj (\<lambda>a. P a \<and> Q a) t s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>obj_at' (\<lambda>ko. P (proj (tcb_to_itcb' ko))) t s; obj_at' (\<lambda>ko. Q (proj (tcb_to_itcb' ko))) t s\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>ko. P (proj (tcb_to_itcb' ko)) \<and> Q (proj (tcb_to_itcb' ko))) t s proof (prove)
goal:
No subgoals!
theory Invariants_H

lemma obj_at_False' [simp]:
  "obj_at' (\<lambda>k. False) t s = False" by (simp add: obj_at'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_at' (\<lambda>k. False) t s = False
theory Invariants_H

lemma pred_tcb_at_False' [simp]:
  "pred_tcb_at' proj (\<lambda>st. False) t s = False" by (simp add: pred_tcb_at'_def obj_at'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pred_tcb_at' proj (\<lambda>st. False) t s = False
theory Invariants_H

lemma obj_at'_pspaceI:
  "obj_at' t ref s \<Longrightarrow> ksPSpace s = ksPSpace s' \<Longrightarrow>  obj_at' t ref s'" by (auto intro!: projectKO_stateI simp: obj_at'_def ps_clear_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>obj_at' t ref s; ksPSpace s = ksPSpace s'\<rbrakk> \<Longrightarrow> obj_at' t ref s'
theory Invariants_H

lemma valid_untyped'_pspaceI:
  "\<lbrakk>ksPSpace s = ksPSpace s'; valid_untyped' d p n idx s\<rbrakk>
  \<Longrightarrow> valid_untyped' d p n idx s'" by (simp add: valid_untyped'_def ko_wp_at'_def ps_clear_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ksPSpace s = ksPSpace s'; valid_untyped' d p n idx s\<rbrakk> \<Longrightarrow> valid_untyped' d p n idx s'
theory Invariants_H

lemma typ_at'_pspaceI:
  "typ_at' T p s \<Longrightarrow> ksPSpace s = ksPSpace s' \<Longrightarrow> typ_at' T p s'" by (simp add: typ_at'_def ko_wp_at'_def ps_clear_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>typ_at' T p s; ksPSpace s = ksPSpace s'\<rbrakk> \<Longrightarrow> typ_at' T p s'