theory TcbQueue_C

lemma cnotification_relation_ntfn_queue:
  fixes ntfn :: "Structures_H.notification"
  defines "qs \<equiv> if isWaitingNtfn (ntfnObj ntfn) then set (ntfnQueue (ntfnObj ntfn)) else {}"
  assumes  ntfn: "cnotification_relation (cslift t) ntfn' b"
  and      srs: "sym_refs (state_refs_of' s)"
  and     koat: "ko_at' ntfn ntfnptr s"
  and    koat': "ko_at' ntfn' ntfnptr' s"
  and     mpeq: "(cslift t' |` (- (tcb_ptr_to_ctcb_ptr ` qs))) = (cslift t |` (- (tcb_ptr_to_ctcb_ptr ` qs)))"
  and      neq: "ntfnptr' \<noteq> ntfnptr"
  shows  "cnotification_relation (cslift t') ntfn' b" proof - have rl: "\<And>p. \<lbrakk> p \<in> tcb_ptr_to_ctcb_ptr ` set (ntfnQueue (ntfnObj ntfn'));
                    isWaitingNtfn (ntfnObj ntfn); isWaitingNtfn (ntfnObj ntfn')\<rbrakk>
    \<Longrightarrow> cslift t p = cslift t' p" using srs koat' koat mpeq neq apply - apply (drule (3) ntfn_ntfn_disjoint [OF _ koat koat']) apply (erule restrict_map_eqI [symmetric]) apply (erule imageE) apply (fastforce simp: disjoint_iff_not_equal inj_eq qs_def) done show ?thesis using ntfn rl mpeq unfolding cnotification_relation_def apply (simp add: Let_def) apply (cases "ntfnObj ntfn'") apply simp apply simp apply (cases "isWaitingNtfn (ntfnObj ntfn)") apply (simp add: isWaitingNtfn_def cong: tcb_queue_relation'_cong) apply (simp add: qs_def) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cnotification_relation (cslift t') ntfn' b proof (state)
goal (1 subgoal):
 1. cnotification_relation (cslift t') ntfn' b proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>p \<in> tcb_ptr_to_ctcb_ptr ` set (ntfnQueue (ntfnObj ntfn')); isWaitingNtfn (ntfnObj ntfn); isWaitingNtfn (ntfnObj ntfn')\<rbrakk> \<Longrightarrow> cslift t p = cslift t' p proof (prove)
using this:
sym_refs (state_refs_of' s)
ko_at' ntfn' ntfnptr' s
ko_at' ntfn ntfnptr s
cslift t'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub> = cslift t|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub>
ntfnptr' \<noteq> ntfnptr

goal (1 subgoal):
 1. \<And>p. \<lbrakk>p \<in> tcb_ptr_to_ctcb_ptr ` set (ntfnQueue (ntfnObj ntfn')); isWaitingNtfn (ntfnObj ntfn); isWaitingNtfn (ntfnObj ntfn')\<rbrakk> \<Longrightarrow> cslift t p = cslift t' p proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>p \<in> tcb_ptr_to_ctcb_ptr ` set (ntfnQueue (ntfnObj ntfn')); isWaitingNtfn (ntfnObj ntfn); isWaitingNtfn (ntfnObj ntfn'); sym_refs (state_refs_of' s); ko_at' ntfn' ntfnptr' s; ko_at' ntfn ntfnptr s; cslift t'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub> = cslift t|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub>; ntfnptr' \<noteq> ntfnptr\<rbrakk> \<Longrightarrow> cslift t p = cslift t' p proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>p \<in> tcb_ptr_to_ctcb_ptr ` set (ntfnQueue (ntfnObj ntfn')); isWaitingNtfn (ntfnObj ntfn); isWaitingNtfn (ntfnObj ntfn'); ko_at' ntfn' ntfnptr' s; ko_at' ntfn ntfnptr s; cslift t'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub> = cslift t|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub>; ntfnptr' \<noteq> ntfnptr; set (ntfnQueue (ntfnObj ntfn)) \<inter> set (ntfnQueue (ntfnObj ntfn')) = {}\<rbrakk> \<Longrightarrow> cslift t p = cslift t' p proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>p \<in> tcb_ptr_to_ctcb_ptr ` set (ntfnQueue (ntfnObj ntfn')); isWaitingNtfn (ntfnObj ntfn); isWaitingNtfn (ntfnObj ntfn'); ko_at' ntfn' ntfnptr' s; ko_at' ntfn ntfnptr s; ntfnptr' \<noteq> ntfnptr; set (ntfnQueue (ntfnObj ntfn)) \<inter> set (ntfnQueue (ntfnObj ntfn')) = {}\<rbrakk> \<Longrightarrow> p \<in> - tcb_ptr_to_ctcb_ptr ` qs proof (prove)
goal (1 subgoal):
 1. \<And>p x. \<lbrakk>isWaitingNtfn (ntfnObj ntfn); isWaitingNtfn (ntfnObj ntfn'); ko_at' ntfn' ntfnptr' s; ko_at' ntfn ntfnptr s; ntfnptr' \<noteq> ntfnptr; set (ntfnQueue (ntfnObj ntfn)) \<inter> set (ntfnQueue (ntfnObj ntfn')) = {}; p = tcb_ptr_to_ctcb_ptr x; x \<in> set (ntfnQueue (ntfnObj ntfn'))\<rbrakk> \<Longrightarrow> p \<in> - tcb_ptr_to_ctcb_ptr ` qs proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>?p \<in> tcb_ptr_to_ctcb_ptr ` set (ntfnQueue (ntfnObj ntfn')); isWaitingNtfn (ntfnObj ntfn); isWaitingNtfn (ntfnObj ntfn')\<rbrakk> \<Longrightarrow> cslift t ?p = cslift t' ?p

goal (1 subgoal):
 1. cnotification_relation (cslift t') ntfn' b proof (prove)
goal (1 subgoal):
 1. cnotification_relation (cslift t') ntfn' b proof (prove)
using this:
cnotification_relation (cslift t) ntfn' b
\<lbrakk>?p \<in> tcb_ptr_to_ctcb_ptr ` set (ntfnQueue (ntfnObj ntfn')); isWaitingNtfn (ntfnObj ntfn); isWaitingNtfn (ntfnObj ntfn')\<rbrakk> \<Longrightarrow> cslift t ?p = cslift t' ?p
cslift t'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub> = cslift t|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub>

goal (1 subgoal):
 1. cnotification_relation (cslift t') ntfn' b proof (prove)
using this:
let cntfn' = notification_lift b; cstate = notification_CL.state_CL cntfn'; chead = (tcb_Ptr \<circ> ntfnQueue_head_CL) cntfn'; cend = (tcb_Ptr \<circ> ntfnQueue_tail_CL) cntfn'; cbound = (tcb_Ptr \<circ> ntfnBoundTCB_CL) cntfn' in (case ntfnObj ntfn' of Structures_H.ntfn.IdleNtfn \<Rightarrow> cstate = SCAST(32 signed \<rightarrow> 32) NtfnState_Idle \<and> ep_queue_relation' (cslift t) [] chead cend | Structures_H.ntfn.ActiveNtfn msgid \<Rightarrow> cstate = SCAST(32 signed \<rightarrow> 32) NtfnState_Active \<and> msgid = ntfnMsgIdentifier_CL cntfn' \<and> ep_queue_relation' (cslift t) [] chead cend | Structures_H.ntfn.WaitingNtfn q \<Rightarrow> cstate = SCAST(32 signed \<rightarrow> 32) NtfnState_Waiting \<and> ep_queue_relation' (cslift t) q chead cend) \<and> option_to_ctcb_ptr (ntfnBoundTCB ntfn') = cbound
\<lbrakk>?p \<in> tcb_ptr_to_ctcb_ptr ` set (ntfnQueue (ntfnObj ntfn')); isWaitingNtfn (ntfnObj ntfn); isWaitingNtfn (ntfnObj ntfn')\<rbrakk> \<Longrightarrow> cslift t ?p = cslift t' ?p
cslift t'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub> = cslift t|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub>

goal (1 subgoal):
 1. let cntfn' = notification_lift b; cstate = notification_CL.state_CL cntfn'; chead = (tcb_Ptr \<circ> ntfnQueue_head_CL) cntfn'; cend = (tcb_Ptr \<circ> ntfnQueue_tail_CL) cntfn'; cbound = (tcb_Ptr \<circ> ntfnBoundTCB_CL) cntfn' in (case ntfnObj ntfn' of Structures_H.ntfn.IdleNtfn \<Rightarrow> cstate = SCAST(32 signed \<rightarrow> 32) NtfnState_Idle \<and> ep_queue_relation' (cslift t') [] chead cend | Structures_H.ntfn.ActiveNtfn msgid \<Rightarrow> cstate = SCAST(32 signed \<rightarrow> 32) NtfnState_Active \<and> msgid = ntfnMsgIdentifier_CL cntfn' \<and> ep_queue_relation' (cslift t') [] chead cend | Structures_H.ntfn.WaitingNtfn q \<Rightarrow> cstate = SCAST(32 signed \<rightarrow> 32) NtfnState_Waiting \<and> ep_queue_relation' (cslift t') q chead cend) \<and> option_to_ctcb_ptr (ntfnBoundTCB ntfn') = cbound proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(case ntfnObj ntfn' of Structures_H.ntfn.IdleNtfn \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Idle \<and> ep_queue_relation' (cslift t) [] (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b))) | Structures_H.ntfn.ActiveNtfn msgid \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Active \<and> msgid = ntfnMsgIdentifier_CL (notification_lift b) \<and> ep_queue_relation' (cslift t) [] (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b))) | Structures_H.ntfn.WaitingNtfn q \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Waiting \<and> ep_queue_relation' (cslift t) q (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b)))) \<and> option_to_ctcb_ptr (ntfnBoundTCB ntfn') = tcb_Ptr (ntfnBoundTCB_CL (notification_lift b)); \<And>p. \<lbrakk>p \<in> tcb_ptr_to_ctcb_ptr ` set (ntfnQueue (ntfnObj ntfn')); isWaitingNtfn (ntfnObj ntfn); isWaitingNtfn (ntfnObj ntfn')\<rbrakk> \<Longrightarrow> cslift t p = cslift t' p; cslift t'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub> = cslift t|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub>\<rbrakk> \<Longrightarrow> case ntfnObj ntfn' of Structures_H.ntfn.IdleNtfn \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Idle \<and> ep_queue_relation' (cslift t') [] (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b))) | Structures_H.ntfn.ActiveNtfn msgid \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Active \<and> msgid = ntfnMsgIdentifier_CL (notification_lift b) \<and> ep_queue_relation' (cslift t') [] (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b))) | Structures_H.ntfn.WaitingNtfn q \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Waiting \<and> ep_queue_relation' (cslift t') q (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b))) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>(case ntfnObj ntfn' of Structures_H.ntfn.IdleNtfn \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Idle \<and> ep_queue_relation' (cslift t) [] (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b))) | Structures_H.ntfn.ActiveNtfn msgid \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Active \<and> msgid = ntfnMsgIdentifier_CL (notification_lift b) \<and> ep_queue_relation' (cslift t) [] (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b))) | Structures_H.ntfn.WaitingNtfn q \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Waiting \<and> ep_queue_relation' (cslift t) q (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b)))) \<and> option_to_ctcb_ptr (ntfnBoundTCB ntfn') = tcb_Ptr (ntfnBoundTCB_CL (notification_lift b)); \<And>p. \<lbrakk>p \<in> tcb_ptr_to_ctcb_ptr ` set (ntfnQueue (ntfnObj ntfn')); isWaitingNtfn (ntfnObj ntfn); isWaitingNtfn (ntfnObj ntfn')\<rbrakk> \<Longrightarrow> cslift t p = cslift t' p; cslift t'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub> = cslift t|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub>; ntfnObj ntfn' = Structures_H.ntfn.IdleNtfn\<rbrakk> \<Longrightarrow> case ntfnObj ntfn' of Structures_H.ntfn.IdleNtfn \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Idle \<and> ep_queue_relation' (cslift t') [] (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b))) | Structures_H.ntfn.ActiveNtfn msgid \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Active \<and> msgid = ntfnMsgIdentifier_CL (notification_lift b) \<and> ep_queue_relation' (cslift t') [] (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b))) | Structures_H.ntfn.WaitingNtfn q \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Waiting \<and> ep_queue_relation' (cslift t') q (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b)))
 2. \<And>x2. \<lbrakk>(case ntfnObj ntfn' of Structures_H.ntfn.IdleNtfn \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Idle \<and> ep_queue_relation' (cslift t) [] (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b))) | Structures_H.ntfn.ActiveNtfn msgid \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Active \<and> msgid = ntfnMsgIdentifier_CL (notification_lift b) \<and> ep_queue_relation' (cslift t) [] (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b))) | Structures_H.ntfn.WaitingNtfn q \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Waiting \<and> ep_queue_relation' (cslift t) q (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b)))) \<and> option_to_ctcb_ptr (ntfnBoundTCB ntfn') = tcb_Ptr (ntfnBoundTCB_CL (notification_lift b)); \<And>p. \<lbrakk>p \<in> tcb_ptr_to_ctcb_ptr ` set (ntfnQueue (ntfnObj ntfn')); isWaitingNtfn (ntfnObj ntfn); isWaitingNtfn (ntfnObj ntfn')\<rbrakk> \<Longrightarrow> cslift t p = cslift t' p; cslift t'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub> = cslift t|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub>; ntfnObj ntfn' = Structures_H.ntfn.ActiveNtfn x2\<rbrakk> \<Longrightarrow> case ntfnObj ntfn' of Structures_H.ntfn.IdleNtfn \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Idle \<and> ep_queue_relation' (cslift t') [] (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b))) | Structures_H.ntfn.ActiveNtfn msgid \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Active \<and> msgid = ntfnMsgIdentifier_CL (notification_lift b) \<and> ep_queue_relation' (cslift t') [] (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b))) | Structures_H.ntfn.WaitingNtfn q \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Waiting \<and> ep_queue_relation' (cslift t') q (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b)))
 3. \<And>x3. \<lbrakk>(case ntfnObj ntfn' of Structures_H.ntfn.IdleNtfn \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Idle \<and> ep_queue_relation' (cslift t) [] (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b))) | Structures_H.ntfn.ActiveNtfn msgid \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Active \<and> msgid = ntfnMsgIdentifier_CL (notification_lift b) \<and> ep_queue_relation' (cslift t) [] (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b))) | Structures_H.ntfn.WaitingNtfn q \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Waiting \<and> ep_queue_relation' (cslift t) q (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b)))) \<and> option_to_ctcb_ptr (ntfnBoundTCB ntfn') = tcb_Ptr (ntfnBoundTCB_CL (notification_lift b)); \<And>p. \<lbrakk>p \<in> tcb_ptr_to_ctcb_ptr ` set (ntfnQueue (ntfnObj ntfn')); isWaitingNtfn (ntfnObj ntfn); isWaitingNtfn (ntfnObj ntfn')\<rbrakk> \<Longrightarrow> cslift t p = cslift t' p; cslift t'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub> = cslift t|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub>; ntfnObj ntfn' = Structures_H.ntfn.WaitingNtfn x3\<rbrakk> \<Longrightarrow> case ntfnObj ntfn' of Structures_H.ntfn.IdleNtfn \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Idle \<and> ep_queue_relation' (cslift t') [] (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b))) | Structures_H.ntfn.ActiveNtfn msgid \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Active \<and> msgid = ntfnMsgIdentifier_CL (notification_lift b) \<and> ep_queue_relation' (cslift t') [] (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b))) | Structures_H.ntfn.WaitingNtfn q \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Waiting \<and> ep_queue_relation' (cslift t') q (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b))) proof (prove)
goal (2 subgoals):
 1. \<And>x2. \<lbrakk>(case ntfnObj ntfn' of Structures_H.ntfn.IdleNtfn \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Idle \<and> ep_queue_relation' (cslift t) [] (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b))) | Structures_H.ntfn.ActiveNtfn msgid \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Active \<and> msgid = ntfnMsgIdentifier_CL (notification_lift b) \<and> ep_queue_relation' (cslift t) [] (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b))) | Structures_H.ntfn.WaitingNtfn q \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Waiting \<and> ep_queue_relation' (cslift t) q (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b)))) \<and> option_to_ctcb_ptr (ntfnBoundTCB ntfn') = tcb_Ptr (ntfnBoundTCB_CL (notification_lift b)); \<And>p. \<lbrakk>p \<in> tcb_ptr_to_ctcb_ptr ` set (ntfnQueue (ntfnObj ntfn')); isWaitingNtfn (ntfnObj ntfn); isWaitingNtfn (ntfnObj ntfn')\<rbrakk> \<Longrightarrow> cslift t p = cslift t' p; cslift t'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub> = cslift t|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub>; ntfnObj ntfn' = Structures_H.ntfn.ActiveNtfn x2\<rbrakk> \<Longrightarrow> case ntfnObj ntfn' of Structures_H.ntfn.IdleNtfn \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Idle \<and> ep_queue_relation' (cslift t') [] (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b))) | Structures_H.ntfn.ActiveNtfn msgid \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Active \<and> msgid = ntfnMsgIdentifier_CL (notification_lift b) \<and> ep_queue_relation' (cslift t') [] (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b))) | Structures_H.ntfn.WaitingNtfn q \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Waiting \<and> ep_queue_relation' (cslift t') q (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b)))
 2. \<And>x3. \<lbrakk>(case ntfnObj ntfn' of Structures_H.ntfn.IdleNtfn \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Idle \<and> ep_queue_relation' (cslift t) [] (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b))) | Structures_H.ntfn.ActiveNtfn msgid \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Active \<and> msgid = ntfnMsgIdentifier_CL (notification_lift b) \<and> ep_queue_relation' (cslift t) [] (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b))) | Structures_H.ntfn.WaitingNtfn q \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Waiting \<and> ep_queue_relation' (cslift t) q (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b)))) \<and> option_to_ctcb_ptr (ntfnBoundTCB ntfn') = tcb_Ptr (ntfnBoundTCB_CL (notification_lift b)); \<And>p. \<lbrakk>p \<in> tcb_ptr_to_ctcb_ptr ` set (ntfnQueue (ntfnObj ntfn')); isWaitingNtfn (ntfnObj ntfn); isWaitingNtfn (ntfnObj ntfn')\<rbrakk> \<Longrightarrow> cslift t p = cslift t' p; cslift t'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub> = cslift t|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub>; ntfnObj ntfn' = Structures_H.ntfn.WaitingNtfn x3\<rbrakk> \<Longrightarrow> case ntfnObj ntfn' of Structures_H.ntfn.IdleNtfn \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Idle \<and> ep_queue_relation' (cslift t') [] (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b))) | Structures_H.ntfn.ActiveNtfn msgid \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Active \<and> msgid = ntfnMsgIdentifier_CL (notification_lift b) \<and> ep_queue_relation' (cslift t') [] (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b))) | Structures_H.ntfn.WaitingNtfn q \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Waiting \<and> ep_queue_relation' (cslift t') q (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b))) proof (prove)
goal (1 subgoal):
 1. \<And>x3. \<lbrakk>(case ntfnObj ntfn' of Structures_H.ntfn.IdleNtfn \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Idle \<and> ep_queue_relation' (cslift t) [] (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b))) | Structures_H.ntfn.ActiveNtfn msgid \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Active \<and> msgid = ntfnMsgIdentifier_CL (notification_lift b) \<and> ep_queue_relation' (cslift t) [] (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b))) | Structures_H.ntfn.WaitingNtfn q \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Waiting \<and> ep_queue_relation' (cslift t) q (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b)))) \<and> option_to_ctcb_ptr (ntfnBoundTCB ntfn') = tcb_Ptr (ntfnBoundTCB_CL (notification_lift b)); \<And>p. \<lbrakk>p \<in> tcb_ptr_to_ctcb_ptr ` set (ntfnQueue (ntfnObj ntfn')); isWaitingNtfn (ntfnObj ntfn); isWaitingNtfn (ntfnObj ntfn')\<rbrakk> \<Longrightarrow> cslift t p = cslift t' p; cslift t'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub> = cslift t|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub>; ntfnObj ntfn' = Structures_H.ntfn.WaitingNtfn x3\<rbrakk> \<Longrightarrow> case ntfnObj ntfn' of Structures_H.ntfn.IdleNtfn \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Idle \<and> ep_queue_relation' (cslift t') [] (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b))) | Structures_H.ntfn.ActiveNtfn msgid \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Active \<and> msgid = ntfnMsgIdentifier_CL (notification_lift b) \<and> ep_queue_relation' (cslift t') [] (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b))) | Structures_H.ntfn.WaitingNtfn q \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Waiting \<and> ep_queue_relation' (cslift t') q (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b))) proof (prove)
goal (2 subgoals):
 1. \<And>x3. \<lbrakk>(case ntfnObj ntfn' of Structures_H.ntfn.IdleNtfn \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Idle \<and> ep_queue_relation' (cslift t) [] (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b))) | Structures_H.ntfn.ActiveNtfn msgid \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Active \<and> msgid = ntfnMsgIdentifier_CL (notification_lift b) \<and> ep_queue_relation' (cslift t) [] (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b))) | Structures_H.ntfn.WaitingNtfn q \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Waiting \<and> ep_queue_relation' (cslift t) q (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b)))) \<and> option_to_ctcb_ptr (ntfnBoundTCB ntfn') = tcb_Ptr (ntfnBoundTCB_CL (notification_lift b)); \<And>p. \<lbrakk>p \<in> tcb_ptr_to_ctcb_ptr ` set (ntfnQueue (ntfnObj ntfn')); isWaitingNtfn (ntfnObj ntfn); isWaitingNtfn (ntfnObj ntfn')\<rbrakk> \<Longrightarrow> cslift t p = cslift t' p; cslift t'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub> = cslift t|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub>; ntfnObj ntfn' = Structures_H.ntfn.WaitingNtfn x3; isWaitingNtfn (ntfnObj ntfn)\<rbrakk> \<Longrightarrow> case ntfnObj ntfn' of Structures_H.ntfn.IdleNtfn \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Idle \<and> ep_queue_relation' (cslift t') [] (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b))) | Structures_H.ntfn.ActiveNtfn msgid \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Active \<and> msgid = ntfnMsgIdentifier_CL (notification_lift b) \<and> ep_queue_relation' (cslift t') [] (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b))) | Structures_H.ntfn.WaitingNtfn q \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Waiting \<and> ep_queue_relation' (cslift t') q (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b)))
 2. \<And>x3. \<lbrakk>(case ntfnObj ntfn' of Structures_H.ntfn.IdleNtfn \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Idle \<and> ep_queue_relation' (cslift t) [] (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b))) | Structures_H.ntfn.ActiveNtfn msgid \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Active \<and> msgid = ntfnMsgIdentifier_CL (notification_lift b) \<and> ep_queue_relation' (cslift t) [] (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b))) | Structures_H.ntfn.WaitingNtfn q \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Waiting \<and> ep_queue_relation' (cslift t) q (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b)))) \<and> option_to_ctcb_ptr (ntfnBoundTCB ntfn') = tcb_Ptr (ntfnBoundTCB_CL (notification_lift b)); \<And>p. \<lbrakk>p \<in> tcb_ptr_to_ctcb_ptr ` set (ntfnQueue (ntfnObj ntfn')); isWaitingNtfn (ntfnObj ntfn); isWaitingNtfn (ntfnObj ntfn')\<rbrakk> \<Longrightarrow> cslift t p = cslift t' p; cslift t'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub> = cslift t|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub>; ntfnObj ntfn' = Structures_H.ntfn.WaitingNtfn x3; \<not> isWaitingNtfn (ntfnObj ntfn)\<rbrakk> \<Longrightarrow> case ntfnObj ntfn' of Structures_H.ntfn.IdleNtfn \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Idle \<and> ep_queue_relation' (cslift t') [] (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b))) | Structures_H.ntfn.ActiveNtfn msgid \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Active \<and> msgid = ntfnMsgIdentifier_CL (notification_lift b) \<and> ep_queue_relation' (cslift t') [] (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b))) | Structures_H.ntfn.WaitingNtfn q \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Waiting \<and> ep_queue_relation' (cslift t') q (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b))) proof (prove)
goal (1 subgoal):
 1. \<And>x3. \<lbrakk>(case ntfnObj ntfn' of Structures_H.ntfn.IdleNtfn \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Idle \<and> ep_queue_relation' (cslift t) [] (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b))) | Structures_H.ntfn.ActiveNtfn msgid \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Active \<and> msgid = ntfnMsgIdentifier_CL (notification_lift b) \<and> ep_queue_relation' (cslift t) [] (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b))) | Structures_H.ntfn.WaitingNtfn q \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Waiting \<and> ep_queue_relation' (cslift t) q (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b)))) \<and> option_to_ctcb_ptr (ntfnBoundTCB ntfn') = tcb_Ptr (ntfnBoundTCB_CL (notification_lift b)); \<And>p. \<lbrakk>p \<in> tcb_ptr_to_ctcb_ptr ` set (ntfnQueue (ntfnObj ntfn')); isWaitingNtfn (ntfnObj ntfn); isWaitingNtfn (ntfnObj ntfn')\<rbrakk> \<Longrightarrow> cslift t p = cslift t' p; cslift t'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub> = cslift t|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` qs)\<^esub>; ntfnObj ntfn' = Structures_H.ntfn.WaitingNtfn x3; \<not> isWaitingNtfn (ntfnObj ntfn)\<rbrakk> \<Longrightarrow> case ntfnObj ntfn' of Structures_H.ntfn.IdleNtfn \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Idle \<and> ep_queue_relation' (cslift t') [] (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b))) | Structures_H.ntfn.ActiveNtfn msgid \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Active \<and> msgid = ntfnMsgIdentifier_CL (notification_lift b) \<and> ep_queue_relation' (cslift t') [] (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b))) | Structures_H.ntfn.WaitingNtfn q \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Waiting \<and> ep_queue_relation' (cslift t') q (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b))) proof (prove)
goal:
No subgoals! proof (state)
this:
cnotification_relation (cslift t') ntfn' b

goal:
No subgoals!