kings-crown/FVELER_Isabelle huggingface dataset:
theory Invariants_AI

lemma ko_at_tcb_at:
  "ko_at (TCB t) p s \<Longrightarrow> tcb_at p s" by (simp add: obj_at_def is_tcb)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ko_at (TCB t) p s \<Longrightarrow> tcb_at p s
theory Invariants_AI

lemma tcb_at_def:
  "tcb_at t s = (\<exists>tcb. get_tcb t s = Some tcb)" by (simp add: obj_at_def get_tcb_def is_tcb_def
           split: option.splits kernel_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_at t s = (\<exists>tcb. get_tcb t s = Some tcb)
theory Invariants_AI

lemma pred_tcb_def2:
  "pred_tcb_at proj test addr s = (\<exists>tcb. (get_tcb addr s) = Some tcb \<and> test (proj (tcb_to_itcb tcb)))" by (simp add: obj_at_def pred_tcb_at_def get_tcb_def
            split: option.splits kernel_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pred_tcb_at proj test addr s = (\<exists>tcb. get_tcb addr s = Some tcb \<and> test (proj (tcb_to_itcb tcb)))
theory Invariants_AI

lemma ntfn_at_typ:
  "ntfn_at = typ_at ANTFN" apply (rule obj_at_eq_helper) apply (simp add: is_ntfn_def a_type_def
            split: kernel_object.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ntfn_at = typ_at ANTFN proof (prove)
goal (1 subgoal):
 1. \<And>obj. is_ntfn obj = (a_type obj = ANTFN) proof (prove)
goal:
No subgoals!
theory Invariants_AI

lemma ep_at_typ:
  "ep_at = typ_at AEndpoint" apply (rule obj_at_eq_helper) apply (simp add: is_ep_def a_type_def
            split: kernel_object.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ep_at = typ_at AEndpoint proof (prove)
goal (1 subgoal):
 1. \<And>obj. is_ep obj = (a_type obj = AEndpoint) proof (prove)
goal:
No subgoals!
theory Invariants_AI

lemma length_set_helper:
  "({x :: 'a list. length x = l} = {x. length x = l'}) = (l = l')" apply (rule iffI, simp_all) apply (cases "replicate l undefined \<in> {x :: 'a list. length x = l}") apply simp apply (subst(asm) mem_simps) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ({x. length x = l} = {x. length x = l'}) = (l = l') proof (prove)
goal (1 subgoal):
 1. {x. length x = l} = {x. length x = l'} \<Longrightarrow> l = l' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>{x. length x = l} = {x. length x = l'}; replicate l undefined \<in> {x. length x = l}\<rbrakk> \<Longrightarrow> l = l'
 2. \<lbrakk>{x. length x = l} = {x. length x = l'}; replicate l undefined \<notin> {x. length x = l}\<rbrakk> \<Longrightarrow> l = l' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>{x. length x = l} = {x. length x = l'}; replicate l undefined \<notin> {x. length x = l}\<rbrakk> \<Longrightarrow> l = l' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>{x. length x = l} = {x. length x = l'}; length (replicate l undefined) \<noteq> l\<rbrakk> \<Longrightarrow> l = l' proof (prove)
goal:
No subgoals!
theory Invariants_AI

lemma cap_table_at_typ:
  "cap_table_at n = typ_at (ACapTable n)" apply (rule obj_at_eq_helper) apply (case_tac obj, simp_all add: is_cap_table_def a_type_def
                                     well_formed_cnode_n_def) apply (auto simp: length_set_helper) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_table_at n = typ_at (ACapTable n) proof (prove)
goal (1 subgoal):
 1. \<And>obj. is_cap_table n obj = (a_type obj = ACapTable n) proof (prove)
goal (1 subgoal):
 1. \<And>obj x11 x12. obj = CNode x11 x12 \<Longrightarrow> dom x12 = {x. length x = x11} \<longrightarrow> (n = x11 \<and> {x. length x = x11} = {x. length x = n}) = (x11 = n) proof (prove)
goal:
No subgoals!
theory Invariants_AI

lemma cte_at_def:
  "cte_at p s \<equiv> \<exists>cap. fst (get_cap p s) = {(cap,s)}" by (simp add: cte_wp_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at (\<lambda>_. True) p s \<equiv> \<exists>cap. fst (get_cap p s) = {(cap, s)}
theory Invariants_AI

lemma tcb_cnode_index_distinct[simp]:
  "(tcb_cnode_index n = tcb_cnode_index m)
       = ((of_nat n :: 3 word) = (of_nat m :: 3 word))" by (simp add: tcb_cnode_index_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (tcb_cnode_index n = tcb_cnode_index m) = (word_of_nat n = word_of_nat m)
theory Invariants_AI

lemma tcb_cap_cases_simps[simp]:
  "tcb_cap_cases (tcb_cnode_index 0) =
   Some (tcb_ctable, tcb_ctable_update, (\<lambda>_ _. \<top>))"
  "tcb_cap_cases (tcb_cnode_index (Suc 0)) =
   Some (tcb_vtable, tcb_vtable_update, (\<lambda>_ _. is_valid_vtable_root or ((=) NullCap)))"
  "tcb_cap_cases (tcb_cnode_index 2) =
   Some (tcb_reply, tcb_reply_update,
         (\<lambda>t st c. (is_master_reply_cap c \<and> obj_ref_of c = t \<and> AllowGrant \<in> cap_rights c) \<or>
                   (halted st \<and> (c = NullCap))))"
  "tcb_cap_cases (tcb_cnode_index 3) =
   Some (tcb_caller, tcb_caller_update,
         (\<lambda>_ st. case st of
                   BlockedOnReceive e data \<Rightarrow> ((=) NullCap)
                 | _ \<Rightarrow> is_reply_cap or ((=) NullCap)))"
  "tcb_cap_cases (tcb_cnode_index 4) =
   Some (tcb_ipcframe, tcb_ipcframe_update,
         (\<lambda>_ _. is_nondevice_page_cap or ((=) cap.NullCap)))" by (simp add: tcb_cap_cases_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (tcb_cap_cases (tcb_cnode_index 0) = Some (tcb_ctable, tcb_ctable_update, \<lambda>_ _ _. True) &&& tcb_cap_cases (tcb_cnode_index (Suc 0)) = Some (tcb_vtable, tcb_vtable_update, \<lambda>_ _. is_valid_vtable_root or (=) NullCap)) &&& tcb_cap_cases (tcb_cnode_index 2) = Some (tcb_reply, tcb_reply_update, \<lambda>t st c. is_master_reply_cap c \<and> obj_ref_of c = t \<and> AllowGrant \<in> cap_rights c \<or> halted st \<and> c = NullCap) &&& tcb_cap_cases (tcb_cnode_index 3) = Some (tcb_caller, tcb_caller_update, \<lambda>_ st. case st of BlockedOnReceive e data \<Rightarrow> (=) NullCap | _ \<Rightarrow> is_reply_cap or (=) NullCap) &&& tcb_cap_cases (tcb_cnode_index 4) = Some (tcb_ipcframe, tcb_ipcframe_update, \<lambda>_ _. is_nondevice_page_cap or (=) NullCap)
theory Invariants_AI

lemma ran_tcb_cap_cases:
  "ran (tcb_cap_cases) =
    {(tcb_ctable, tcb_ctable_update, (\<lambda>_ _. \<top>)),
     (tcb_vtable, tcb_vtable_update, (\<lambda>_ _. is_valid_vtable_root or ((=) NullCap))),
     (tcb_reply, tcb_reply_update, (\<lambda>t st c.
                                       (is_master_reply_cap c \<and> obj_ref_of c = t
                                        \<and> AllowGrant \<in> cap_rights c)
                                     \<or> (halted st \<and> (c = NullCap)))),
     (tcb_caller, tcb_caller_update, (\<lambda>_ st. case st of
                                       Structures_A.BlockedOnReceive e data \<Rightarrow>
                                         ((=) NullCap)
                                     | _ \<Rightarrow> is_reply_cap or ((=) NullCap))),
     (tcb_ipcframe, tcb_ipcframe_update, (\<lambda>_ _. is_nondevice_page_cap or ((=) NullCap)))}" by (simp add: tcb_cap_cases_def insert_commute)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ran tcb_cap_cases = {(tcb_ctable, tcb_ctable_update, \<lambda>_ _ _. True), (tcb_vtable, tcb_vtable_update, \<lambda>_ _. is_valid_vtable_root or (=) NullCap), (tcb_reply, tcb_reply_update, \<lambda>t st c. is_master_reply_cap c \<and> obj_ref_of c = t \<and> AllowGrant \<in> cap_rights c \<or> halted st \<and> c = NullCap), (tcb_caller, tcb_caller_update, \<lambda>_ st. case st of BlockedOnReceive e data \<Rightarrow> (=) NullCap | _ \<Rightarrow> is_reply_cap or (=) NullCap), (tcb_ipcframe, tcb_ipcframe_update, \<lambda>_ _. is_nondevice_page_cap or (=) NullCap)}
theory Invariants_AI

lemma tcb_cnode_map_tcb_cap_cases:
  "tcb_cnode_map tcb = (\<lambda>bl. map_option (\<lambda>x. fst x tcb) (tcb_cap_cases bl))" by (rule ext) (simp add: tcb_cnode_map_def tcb_cap_cases_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_cnode_map tcb = (\<lambda>bl. map_option (\<lambda>x. fst x tcb) (tcb_cap_cases bl))
theory Invariants_AI

lemma ran_tcb_cnode_map:
  "ran (tcb_cnode_map t) =
   {tcb_vtable t, tcb_ctable t, tcb_caller t, tcb_reply t, tcb_ipcframe t}" by (fastforce simp: tcb_cnode_map_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ran (tcb_cnode_map t) = {tcb_vtable t, tcb_ctable t, tcb_caller t, tcb_reply t, tcb_ipcframe t}
theory Invariants_AI

lemma st_tcb_idle_cap_valid_Null [simp]:
  "st_tcb_at (idle or inactive) (fst sl) s \<longrightarrow>
   tcb_cap_valid NullCap sl s" by (fastforce simp: tcb_cap_valid_def tcb_cap_cases_def
                      pred_tcb_at_def obj_at_def
                      valid_ipc_buffer_cap_null)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. st_tcb_at (idle or inactive) (fst sl) s \<longrightarrow> tcb_cap_valid NullCap sl s
theory Invariants_AI

lemma valid_objsI [intro]:
  "(\<And>obj x. kheap s x = Some obj \<Longrightarrow> valid_obj x obj s) \<Longrightarrow> valid_objs s" unfolding valid_objs_def by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>obj x. kheap s x = Some obj \<Longrightarrow> valid_obj x obj s) \<Longrightarrow> valid_objs s proof (prove)
goal (1 subgoal):
 1. (\<And>obj x. kheap s x = Some obj \<Longrightarrow> valid_obj x obj s) \<Longrightarrow> \<forall>ptr\<in>dom $ kheap s. \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s
theory Invariants_AI

lemma valid_objsE [elim]:
  "\<lbrakk> valid_objs s; kheap s x = Some obj; valid_obj x obj s \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R" unfolding valid_objs_def by (auto simp: dom_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; kheap s x = Some obj; valid_obj x obj s \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>ptr\<in>dom $ kheap s. \<exists>obj. kheap s ptr = Some obj \<and> valid_obj ptr obj s; kheap s x = Some obj; valid_obj x obj s \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R
theory Invariants_AI

lemma valid_obj_arch_valid_obj:
  "valid_obj p (ArchObj ao) s = arch_valid_obj ao s" by (simp add: valid_obj_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_obj p (ArchObj ao) s = arch_valid_obj ao s
theory Invariants_AI

lemma obj_at_ko_at:
  "obj_at P p s \<Longrightarrow> \<exists>ko. ko_at ko p s \<and> P ko" by (auto simp add: obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_at P p s \<Longrightarrow> \<exists>ko. ko_at ko p s \<and> P ko
theory Invariants_AI

lemma tcb_st_refs_of_simps[simp]: (* ARMHYP add TCBHypRef? *)
 "tcb_st_refs_of (Running)               = {}"
 "tcb_st_refs_of (Inactive)              = {}"
 "tcb_st_refs_of (Restart)               = {}"
 "tcb_st_refs_of (BlockedOnReply)        = {}"
 "tcb_st_refs_of (IdleThreadState)       = {}"
 "\<And>x. tcb_st_refs_of (BlockedOnReceive x payl')  = {(x, TCBBlockedRecv)}"
 "\<And>x. tcb_st_refs_of (BlockedOnSend x payl)  = {(x, TCBBlockedSend)}"
 "\<And>x. tcb_st_refs_of (BlockedOnNotification x) = {(x, TCBSignal)}" by (auto simp: tcb_st_refs_of_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((tcb_st_refs_of Running = {} &&& tcb_st_refs_of Inactive = {}) &&& tcb_st_refs_of Restart = {} &&& tcb_st_refs_of BlockedOnReply = {}) &&& (tcb_st_refs_of IdleThreadState = {} &&& (\<And>x. tcb_st_refs_of (BlockedOnReceive x payl') = {(x, TCBBlockedRecv)})) &&& (\<And>x. tcb_st_refs_of (BlockedOnSend x payl) = {(x, TCBBlockedSend)}) &&& (\<And>x. tcb_st_refs_of (BlockedOnNotification x) = {(x, TCBSignal)})
theory Invariants_AI

lemma ep_q_refs_of_simps[simp]:
 "ep_q_refs_of  IdleEP    = {}"
 "\<And>q. ep_q_refs_of (RecvEP q) = set q \<times> {EPRecv}"
 "\<And>q. ep_q_refs_of (SendEP q) = set q \<times> {EPSend}" by (auto simp: ep_q_refs_of_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ep_q_refs_of IdleEP = {} &&& (\<And>q. ep_q_refs_of (RecvEP q) = set q \<times> {EPRecv}) &&& (\<And>q. ep_q_refs_of (SendEP q) = set q \<times> {EPSend})
theory Invariants_AI

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 IdleNtfn = {} &&& ntfn_q_refs_of (WaitingNtfn q) = set q \<times> {NTFNSignal} &&& ntfn_q_refs_of (ActiveNtfn b) = {}
theory Invariants_AI

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_AI

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_AI

lemma refs_of_simps[simp]:
 "refs_of (CNode sz cs)       = {}"
 "refs_of (TCB tcb)           = tcb_st_refs_of (tcb_state tcb) \<union> tcb_bound_refs (tcb_bound_notification tcb)"
 "refs_of (Endpoint ep)       = ep_q_refs_of ep"
 "refs_of (Notification ntfn) = ntfn_q_refs_of (ntfn_obj ntfn) \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn)"
 "refs_of (ArchObj ao)        = {}" by (auto simp: refs_of_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (refs_of (CNode sz cs) = {} &&& refs_of (TCB tcb) = tcb_st_refs_of (tcb_state tcb) \<union> tcb_bound_refs (tcb_bound_notification tcb)) &&& refs_of (Endpoint ep) = ep_q_refs_of ep &&& refs_of (Notification ntfn) = ntfn_q_refs_of (ntfn_obj ntfn) \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn) &&& refs_of (ArchObj ao) = {}
theory Invariants_AI

lemma refs_of_rev:
 "(x, TCBBlockedRecv) \<in> refs_of ko =
    (\<exists>tcb. ko = TCB tcb \<and> (\<exists>pl. tcb_state tcb = BlockedOnReceive x pl))"
 "(x, TCBBlockedSend) \<in> refs_of ko =
    (\<exists>tcb. ko = TCB tcb \<and> (\<exists>pl. tcb_state tcb = BlockedOnSend x pl))"
 "(x, TCBSignal) \<in> refs_of ko =
    (\<exists>tcb. ko = TCB tcb \<and> (tcb_state tcb = BlockedOnNotification x))"
 "(x, EPRecv) \<in> refs_of ko =
    (\<exists>ep. ko = Endpoint ep \<and> (\<exists>q. ep = RecvEP q \<and> x \<in> set q))"
 "(x, EPSend) \<in> refs_of ko =
    (\<exists>ep. ko = Endpoint ep \<and> (\<exists>q. ep = SendEP q \<and> x \<in> set q))"
 "(x, NTFNSignal) \<in> refs_of ko =
    (\<exists>ntfn. ko = Notification ntfn \<and> (\<exists>q. ntfn_obj ntfn = WaitingNtfn q \<and> x \<in> set q))"
 "(x, TCBBound) \<in>  refs_of ko =
    (\<exists>tcb. ko = TCB tcb \<and> (tcb_bound_notification tcb = Some x))"
 "(x, NTFNBound) \<in> refs_of ko =
    (\<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb 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: kernel_object.splits
                     thread_state.splits
                     endpoint.splits
                     ntfn.splits
                     option.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((((x, TCBBlockedRecv) \<in> refs_of ko) = (\<exists>tcb. ko = TCB tcb \<and> (\<exists>pl. tcb_state tcb = BlockedOnReceive x pl)) &&& ((x, TCBBlockedSend) \<in> refs_of ko) = (\<exists>tcb. ko = TCB tcb \<and> (\<exists>pl. tcb_state tcb = BlockedOnSend x pl))) &&& ((x, TCBSignal) \<in> refs_of ko) = (\<exists>tcb. ko = TCB tcb \<and> tcb_state tcb = BlockedOnNotification x) &&& ((x, EPRecv) \<in> refs_of ko) = (\<exists>ep. ko = Endpoint ep \<and> (\<exists>q. ep = RecvEP q \<and> x \<in> set q))) &&& (((x, EPSend) \<in> refs_of ko) = (\<exists>ep. ko = Endpoint ep \<and> (\<exists>q. ep = SendEP q \<and> x \<in> set q)) &&& ((x, NTFNSignal) \<in> refs_of ko) = (\<exists>ntfn. ko = Notification ntfn \<and> (\<exists>q. ntfn_obj ntfn = WaitingNtfn q \<and> x \<in> set q))) &&& ((x, TCBBound) \<in> refs_of ko) = (\<exists>tcb. ko = TCB tcb \<and> tcb_bound_notification tcb = Some x) &&& ((x, NTFNBound) \<in> refs_of ko) = (\<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = Some x)
theory Invariants_AI

lemma st_tcb_at_refs_of_rev:
  "obj_at (\<lambda>ko. (x, TCBBlockedRecv) \<in> refs_of ko) t s
     = st_tcb_at (\<lambda>ts. \<exists>pl. ts = BlockedOnReceive x pl) t s"
  "obj_at (\<lambda>ko. (x, TCBBlockedSend) \<in> refs_of ko) t s
     = st_tcb_at (\<lambda>ts. \<exists>pl. ts = BlockedOnSend x pl   ) t s"
  "obj_at (\<lambda>ko. (x, TCBSignal) \<in> refs_of ko) t s
     = st_tcb_at (\<lambda>ts.      ts = BlockedOnNotification x) t s" by (simp add: refs_of_rev pred_tcb_at_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_at (\<lambda>ko. (x, TCBBlockedRecv) \<in> refs_of ko) t s = st_tcb_at (\<lambda>ts. \<exists>pl. ts = BlockedOnReceive x pl) t s &&& obj_at (\<lambda>ko. (x, TCBBlockedSend) \<in> refs_of ko) t s = st_tcb_at (\<lambda>ts. \<exists>pl. ts = BlockedOnSend x pl) t s &&& obj_at (\<lambda>ko. (x, TCBSignal) \<in> refs_of ko) t s = st_tcb_at (\<lambda>ts. ts = BlockedOnNotification x) t s
theory Invariants_AI

lemma state_refs_of_elemD:
  "\<lbrakk> ref \<in> state_refs_of s x \<rbrakk> \<Longrightarrow> obj_at (\<lambda>obj. ref \<in> refs_of obj) x s" by (clarsimp simp add: state_refs_of_def obj_at_def
                  split: option.splits)

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

lemma obj_at_state_refs_ofD:
  "obj_at P p s \<Longrightarrow> \<exists>ko. P ko \<and> state_refs_of s p = refs_of ko" apply (clarsimp simp: obj_at_def state_refs_of_def) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_at P p s \<Longrightarrow> \<exists>ko. P ko \<and> state_refs_of s p = refs_of ko proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>kheap s p = Some ko; P ko\<rbrakk> \<Longrightarrow> \<exists>koa. P koa \<and> refs_of ko = refs_of koa proof (prove)
goal:
No subgoals!
theory Invariants_AI

lemma ko_at_state_refs_ofD:
  "ko_at ko p s \<Longrightarrow> state_refs_of s p = refs_of 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 ko
theory Invariants_AI

lemma st_tcb_at_state_refs_ofD:
  "st_tcb_at P t s \<Longrightarrow> \<exists>ts ntfnptr. P ts \<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
                 state_refs_of_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. st_tcb_at P t s \<Longrightarrow> \<exists>ts ntfnptr. P ts \<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_AI

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
                 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_AI

lemma sym_refs_obj_atD:
  "\<lbrakk> obj_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. obj_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>ko. P ko \<and> state_refs_of s p = refs_of ko \<and> (\<forall>(x, tp)\<in>refs_of ko. obj_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>ko. P ko \<and> state_refs_of s p = refs_of ko\<rbrakk> \<Longrightarrow> \<exists>ko. P ko \<and> state_refs_of s p = refs_of ko \<and> (\<forall>(x, tp)\<in>refs_of ko. obj_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 x; P x; state_refs_of s p = refs_of x\<rbrakk> \<Longrightarrow> obj_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 x = state_refs_of s p\<rbrakk> \<Longrightarrow> obj_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 x = state_refs_of s p; (p, symreftype b) \<in> state_refs_of s a\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. (p, symreftype b) \<in> refs_of ko) a s proof (prove)
goal:
No subgoals!
theory Invariants_AI

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 ko \<and>
     (\<forall>(x, tp)\<in>refs_of ko.  obj_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 ko \<and> (\<forall>(x, tp)\<in>refs_of ko. obj_at (\<lambda>ko. (p, symreftype tp) \<in> refs_of ko) x s)
theory Invariants_AI

lemma pspace_alignedE [elim]:
  "\<lbrakk> pspace_aligned s;
   x \<in> dom (kheap s); is_aligned x (obj_bits (the (kheap s x))) \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R" unfolding pspace_aligned_def by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_aligned s; x \<in> dom (kheap s); is_aligned x (obj_bits (the (kheap s x))) \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>dom (kheap s). is_aligned x (obj_bits (the (kheap s x))); x \<in> dom (kheap s); is_aligned x (obj_bits (the (kheap s x))) \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R
theory Invariants_AI

lemma hyp_refs_of_live:
  "hyp_refs_of ko \<noteq> {} \<Longrightarrow> live ko" by (cases ko, simp_all add: live_def hyp_refs_of_hyp_live)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. hyp_refs_of ko \<noteq> {} \<Longrightarrow> live ko
theory Invariants_AI

lemma refs_of_live_obj:
  "\<lbrakk> obj_at P p s; \<And>ko. \<lbrakk> P ko; refs_of ko = {} \<rbrakk> \<Longrightarrow> False \<rbrakk> \<Longrightarrow> obj_at live p s" by (fastforce simp: obj_at_def intro!: refs_of_live)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>obj_at P p s; \<And>ko. \<lbrakk>P ko; refs_of ko = {}\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> obj_at live p s