theory SR_lemmas_C

lemma ntfn_blocked_in_queueD:
  "\<lbrakk> st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) thread \<sigma>; ko_at' ntfn' ntfn \<sigma>; invs' \<sigma> \<rbrakk>
   \<Longrightarrow> thread \<in> set (ntfnQueue (ntfnObj ntfn')) \<and> isWaitingNtfn (ntfnObj ntfn')" apply (drule sym_refs_st_tcb_atD') apply clarsimp apply (clarsimp simp: obj_at'_def ko_wp_at'_def projectKOs
                        refs_of_rev'[where ko = "KONotification ntfn'", simplified]) apply (cases "ntfnObj ntfn'") apply (simp_all add: isWaitingNtfn_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) thread \<sigma>; ko_at' ntfn' ntfn \<sigma>; invs' \<sigma>\<rbrakk> \<Longrightarrow> thread \<in> set (ntfnQueue (ntfnObj ntfn')) \<and> isWaitingNtfn (ntfnObj ntfn') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ko_at' ntfn' ntfn \<sigma>; invs' \<sigma>\<rbrakk> \<Longrightarrow> sym_refs (state_refs_of' \<sigma>)
 2. \<lbrakk>ko_at' ntfn' ntfn \<sigma>; invs' \<sigma>; \<exists>ts ntfnptr. Structures_H.thread_state.BlockedOnNotification ntfn = ts \<and> obj_at' (tcb_ntfn_is_bound' ntfnptr) thread \<sigma> \<and> state_refs_of' \<sigma> thread = tcb_st_refs_of' ts \<union> tcb_bound_refs' ntfnptr \<and> (\<forall>(x, tp)\<in>tcb_st_refs_of' ts \<union> tcb_bound_refs' ntfnptr. ko_wp_at' (\<lambda>ko. (thread, symreftype tp) \<in> refs_of' ko) x \<sigma>)\<rbrakk> \<Longrightarrow> thread \<in> set (ntfnQueue (ntfnObj ntfn')) \<and> isWaitingNtfn (ntfnObj ntfn') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at' ntfn' ntfn \<sigma>; invs' \<sigma>; \<exists>ts ntfnptr. Structures_H.thread_state.BlockedOnNotification ntfn = ts \<and> obj_at' (tcb_ntfn_is_bound' ntfnptr) thread \<sigma> \<and> state_refs_of' \<sigma> thread = tcb_st_refs_of' ts \<union> tcb_bound_refs' ntfnptr \<and> (\<forall>(x, tp)\<in>tcb_st_refs_of' ts \<union> tcb_bound_refs' ntfnptr. ko_wp_at' (\<lambda>ko. (thread, symreftype tp) \<in> refs_of' ko) x \<sigma>)\<rbrakk> \<Longrightarrow> thread \<in> set (ntfnQueue (ntfnObj ntfn')) \<and> isWaitingNtfn (ntfnObj ntfn') proof (prove)
goal (1 subgoal):
 1. \<And>ntfnptr q obj. \<lbrakk>invs' \<sigma>; ksPSpace \<sigma> ntfn = Some (KONotification ntfn'); is_aligned ntfn (objBitsKO (KONotification ntfn')); ps_clear ntfn (objBitsKO (KONotification ntfn')) \<sigma>; state_refs_of' \<sigma> thread = insert (ntfn, TCBSignal) (tcb_bound_refs' ntfnptr); ksPSpace \<sigma> thread = Some (KOTCB obj); \<forall>x\<in>tcb_bound_refs' ntfnptr. case x of (x, tp) \<Rightarrow> \<exists>ko. ksPSpace \<sigma> x = Some ko \<and> is_aligned x (objBitsKO ko) \<and> (thread, symreftype tp) \<in> refs_of' ko \<and> ps_clear x (objBitsKO ko) \<sigma>; is_aligned thread (objBitsKO (KOTCB obj)); ntfnObj ntfn' = Structures_H.ntfn.WaitingNtfn q; thread \<in> set q; tcb_ntfn_is_bound' ntfnptr obj; ps_clear thread (objBitsKO (KOTCB obj)) \<sigma>\<rbrakk> \<Longrightarrow> isWaitingNtfn (Structures_H.ntfn.WaitingNtfn q) proof (prove)
goal (3 subgoals):
 1. \<And>ntfnptr q obj. \<lbrakk>invs' \<sigma>; ksPSpace \<sigma> ntfn = Some (KONotification ntfn'); is_aligned ntfn (objBitsKO (KONotification ntfn')); ps_clear ntfn (objBitsKO (KONotification ntfn')) \<sigma>; state_refs_of' \<sigma> thread = insert (ntfn, TCBSignal) (tcb_bound_refs' ntfnptr); ksPSpace \<sigma> thread = Some (KOTCB obj); \<forall>x\<in>tcb_bound_refs' ntfnptr. case x of (x, tp) \<Rightarrow> \<exists>ko. ksPSpace \<sigma> x = Some ko \<and> is_aligned x (objBitsKO ko) \<and> (thread, symreftype tp) \<in> refs_of' ko \<and> ps_clear x (objBitsKO ko) \<sigma>; is_aligned thread (objBitsKO (KOTCB obj)); ntfnObj ntfn' = Structures_H.ntfn.WaitingNtfn q; thread \<in> set q; tcb_ntfn_is_bound' ntfnptr obj; ps_clear thread (objBitsKO (KOTCB obj)) \<sigma>; ntfnObj ntfn' = Structures_H.ntfn.IdleNtfn\<rbrakk> \<Longrightarrow> isWaitingNtfn (Structures_H.ntfn.WaitingNtfn q)
 2. \<And>ntfnptr q obj x2. \<lbrakk>invs' \<sigma>; ksPSpace \<sigma> ntfn = Some (KONotification ntfn'); is_aligned ntfn (objBitsKO (KONotification ntfn')); ps_clear ntfn (objBitsKO (KONotification ntfn')) \<sigma>; state_refs_of' \<sigma> thread = insert (ntfn, TCBSignal) (tcb_bound_refs' ntfnptr); ksPSpace \<sigma> thread = Some (KOTCB obj); \<forall>x\<in>tcb_bound_refs' ntfnptr. case x of (x, tp) \<Rightarrow> \<exists>ko. ksPSpace \<sigma> x = Some ko \<and> is_aligned x (objBitsKO ko) \<and> (thread, symreftype tp) \<in> refs_of' ko \<and> ps_clear x (objBitsKO ko) \<sigma>; is_aligned thread (objBitsKO (KOTCB obj)); ntfnObj ntfn' = Structures_H.ntfn.WaitingNtfn q; thread \<in> set q; tcb_ntfn_is_bound' ntfnptr obj; ps_clear thread (objBitsKO (KOTCB obj)) \<sigma>; ntfnObj ntfn' = Structures_H.ntfn.ActiveNtfn x2\<rbrakk> \<Longrightarrow> isWaitingNtfn (Structures_H.ntfn.WaitingNtfn q)
 3. \<And>ntfnptr q obj x3. \<lbrakk>invs' \<sigma>; ksPSpace \<sigma> ntfn = Some (KONotification ntfn'); is_aligned ntfn (objBitsKO (KONotification ntfn')); ps_clear ntfn (objBitsKO (KONotification ntfn')) \<sigma>; state_refs_of' \<sigma> thread = insert (ntfn, TCBSignal) (tcb_bound_refs' ntfnptr); ksPSpace \<sigma> thread = Some (KOTCB obj); \<forall>x\<in>tcb_bound_refs' ntfnptr. case x of (x, tp) \<Rightarrow> \<exists>ko. ksPSpace \<sigma> x = Some ko \<and> is_aligned x (objBitsKO ko) \<and> (thread, symreftype tp) \<in> refs_of' ko \<and> ps_clear x (objBitsKO ko) \<sigma>; is_aligned thread (objBitsKO (KOTCB obj)); ntfnObj ntfn' = Structures_H.ntfn.WaitingNtfn q; thread \<in> set q; tcb_ntfn_is_bound' ntfnptr obj; ps_clear thread (objBitsKO (KOTCB obj)) \<sigma>; ntfnObj ntfn' = Structures_H.ntfn.WaitingNtfn x3\<rbrakk> \<Longrightarrow> isWaitingNtfn (Structures_H.ntfn.WaitingNtfn q) proof (prove)
goal:
No subgoals!