theory IpcCancel_C

lemma cnotification_relation_ep_queue:
  assumes   srs: "sym_refs (state_refs_of' s)"
  and      koat: "ko_at' ep epptr s"
  and iswaiting: "(isSendEP ep \<or> isRecvEP ep)"
  and      mpeq: "(mp' |` (- (tcb_ptr_to_ctcb_ptr ` set (epQueue ep))))
  = (mp |` (- (tcb_ptr_to_ctcb_ptr ` set (epQueue ep))))"
  and      koat': "ko_at' a ntfnPtr s"
  shows "cnotification_relation mp a b = cnotification_relation mp' a b" proof - have rl: "\<And>p. \<lbrakk> p \<in> tcb_ptr_to_ctcb_ptr ` set (ntfnQueue (ntfnObj a));
                  isWaitingNtfn (ntfnObj a) \<rbrakk>
    \<Longrightarrow> mp p = mp' p" using srs koat' koat iswaiting mpeq apply - apply (drule (4) ntfn_ep_disjoint) apply (erule restrict_map_eqI [symmetric]) apply (erule imageE) apply (fastforce simp: disjoint_iff_not_equal inj_eq) done show ?thesis unfolding cnotification_relation_def using rl apply (simp add: Let_def) apply (cases "ntfnObj a") apply (simp add: isWaitingNtfn_def cong: tcb_queue_relation'_cong)+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cnotification_relation mp a b = cnotification_relation mp' a b proof (state)
goal (1 subgoal):
 1. cnotification_relation mp a b = cnotification_relation mp' a b proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>p \<in> tcb_ptr_to_ctcb_ptr ` set (ntfnQueue (ntfnObj a)); isWaitingNtfn (ntfnObj a)\<rbrakk> \<Longrightarrow> mp p = mp' p proof (prove)
using this:
sym_refs (state_refs_of' s)
ko_at' a ntfnPtr s
ko_at' ep epptr s
isSendEP ep \<or> isRecvEP ep
mp'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` set (epQueue ep))\<^esub> = mp|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` set (epQueue ep))\<^esub>

goal (1 subgoal):
 1. \<And>p. \<lbrakk>p \<in> tcb_ptr_to_ctcb_ptr ` set (ntfnQueue (ntfnObj a)); isWaitingNtfn (ntfnObj a)\<rbrakk> \<Longrightarrow> mp p = mp' p proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>p \<in> tcb_ptr_to_ctcb_ptr ` set (ntfnQueue (ntfnObj a)); isWaitingNtfn (ntfnObj a); sym_refs (state_refs_of' s); ko_at' a ntfnPtr s; ko_at' ep epptr s; isSendEP ep \<or> isRecvEP ep; mp'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` set (epQueue ep))\<^esub> = mp|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` set (epQueue ep))\<^esub>\<rbrakk> \<Longrightarrow> mp p = mp' p proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>p \<in> tcb_ptr_to_ctcb_ptr ` set (ntfnQueue (ntfnObj a)); isWaitingNtfn (ntfnObj a); ko_at' a ntfnPtr s; ko_at' ep epptr s; isSendEP ep \<or> isRecvEP ep; mp'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` set (epQueue ep))\<^esub> = mp|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` set (epQueue ep))\<^esub>; set (epQueue ep) \<inter> set (ntfnQueue (ntfnObj a)) = {}\<rbrakk> \<Longrightarrow> mp p = mp' p proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>p \<in> tcb_ptr_to_ctcb_ptr ` set (ntfnQueue (ntfnObj a)); isWaitingNtfn (ntfnObj a); ko_at' a ntfnPtr s; ko_at' ep epptr s; isSendEP ep \<or> isRecvEP ep; set (epQueue ep) \<inter> set (ntfnQueue (ntfnObj a)) = {}\<rbrakk> \<Longrightarrow> p \<in> - tcb_ptr_to_ctcb_ptr ` set (epQueue ep) proof (prove)
goal (1 subgoal):
 1. \<And>p x. \<lbrakk>isWaitingNtfn (ntfnObj a); ko_at' a ntfnPtr s; ko_at' ep epptr s; isSendEP ep \<or> isRecvEP ep; set (epQueue ep) \<inter> set (ntfnQueue (ntfnObj a)) = {}; p = tcb_ptr_to_ctcb_ptr x; x \<in> set (ntfnQueue (ntfnObj a))\<rbrakk> \<Longrightarrow> p \<in> - tcb_ptr_to_ctcb_ptr ` set (epQueue ep) proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>?p1 \<in> tcb_ptr_to_ctcb_ptr ` set (ntfnQueue (ntfnObj a)); isWaitingNtfn (ntfnObj a)\<rbrakk> \<Longrightarrow> mp ?p1 = mp' ?p1

goal (1 subgoal):
 1. cnotification_relation mp a b = cnotification_relation mp' a b proof (prove)
goal (1 subgoal):
 1. cnotification_relation mp a b = cnotification_relation mp' a b proof (prove)
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 a of Structures_H.ntfn.IdleNtfn \<Rightarrow> cstate = SCAST(32 signed \<rightarrow> 32) NtfnState_Idle \<and> ep_queue_relation' mp [] 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' mp [] chead cend | Structures_H.ntfn.WaitingNtfn q \<Rightarrow> cstate = SCAST(32 signed \<rightarrow> 32) NtfnState_Waiting \<and> ep_queue_relation' mp q chead cend) \<and> option_to_ctcb_ptr (ntfnBoundTCB a) = cbound) = (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 a of Structures_H.ntfn.IdleNtfn \<Rightarrow> cstate = SCAST(32 signed \<rightarrow> 32) NtfnState_Idle \<and> ep_queue_relation' mp' [] 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' mp' [] chead cend | Structures_H.ntfn.WaitingNtfn q \<Rightarrow> cstate = SCAST(32 signed \<rightarrow> 32) NtfnState_Waiting \<and> ep_queue_relation' mp' q chead cend) \<and> option_to_ctcb_ptr (ntfnBoundTCB a) = cbound) proof (prove)
using this:
\<lbrakk>?p1 \<in> tcb_ptr_to_ctcb_ptr ` set (ntfnQueue (ntfnObj a)); isWaitingNtfn (ntfnObj a)\<rbrakk> \<Longrightarrow> mp ?p1 = mp' ?p1

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 a of Structures_H.ntfn.IdleNtfn \<Rightarrow> cstate = SCAST(32 signed \<rightarrow> 32) NtfnState_Idle \<and> ep_queue_relation' mp [] 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' mp [] chead cend | Structures_H.ntfn.WaitingNtfn q \<Rightarrow> cstate = SCAST(32 signed \<rightarrow> 32) NtfnState_Waiting \<and> ep_queue_relation' mp q chead cend) \<and> option_to_ctcb_ptr (ntfnBoundTCB a) = cbound) = (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 a of Structures_H.ntfn.IdleNtfn \<Rightarrow> cstate = SCAST(32 signed \<rightarrow> 32) NtfnState_Idle \<and> ep_queue_relation' mp' [] 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' mp' [] chead cend | Structures_H.ntfn.WaitingNtfn q \<Rightarrow> cstate = SCAST(32 signed \<rightarrow> 32) NtfnState_Waiting \<and> ep_queue_relation' mp' q chead cend) \<and> option_to_ctcb_ptr (ntfnBoundTCB a) = cbound) proof (prove)
goal (1 subgoal):
 1. (\<And>p. \<lbrakk>p \<in> tcb_ptr_to_ctcb_ptr ` set (ntfnQueue (ntfnObj a)); isWaitingNtfn (ntfnObj a)\<rbrakk> \<Longrightarrow> mp p = mp' p) \<Longrightarrow> ((case ntfnObj a of Structures_H.ntfn.IdleNtfn \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Idle \<and> ep_queue_relation' mp [] (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' mp [] (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' mp q (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b)))) \<and> option_to_ctcb_ptr (ntfnBoundTCB a) = tcb_Ptr (ntfnBoundTCB_CL (notification_lift b))) = ((case ntfnObj a of Structures_H.ntfn.IdleNtfn \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Idle \<and> ep_queue_relation' mp' [] (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' mp' [] (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' mp' q (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b)))) \<and> option_to_ctcb_ptr (ntfnBoundTCB a) = tcb_Ptr (ntfnBoundTCB_CL (notification_lift b))) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<And>p. \<lbrakk>p \<in> tcb_ptr_to_ctcb_ptr ` set (ntfnQueue (ntfnObj a)); isWaitingNtfn (ntfnObj a)\<rbrakk> \<Longrightarrow> mp p = mp' p; ntfnObj a = Structures_H.ntfn.IdleNtfn\<rbrakk> \<Longrightarrow> ((case ntfnObj a of Structures_H.ntfn.IdleNtfn \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Idle \<and> ep_queue_relation' mp [] (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' mp [] (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' mp q (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b)))) \<and> option_to_ctcb_ptr (ntfnBoundTCB a) = tcb_Ptr (ntfnBoundTCB_CL (notification_lift b))) = ((case ntfnObj a of Structures_H.ntfn.IdleNtfn \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Idle \<and> ep_queue_relation' mp' [] (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' mp' [] (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' mp' q (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b)))) \<and> option_to_ctcb_ptr (ntfnBoundTCB a) = tcb_Ptr (ntfnBoundTCB_CL (notification_lift b)))
 2. \<And>x2. \<lbrakk>\<And>p. \<lbrakk>p \<in> tcb_ptr_to_ctcb_ptr ` set (ntfnQueue (ntfnObj a)); isWaitingNtfn (ntfnObj a)\<rbrakk> \<Longrightarrow> mp p = mp' p; ntfnObj a = Structures_H.ntfn.ActiveNtfn x2\<rbrakk> \<Longrightarrow> ((case ntfnObj a of Structures_H.ntfn.IdleNtfn \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Idle \<and> ep_queue_relation' mp [] (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' mp [] (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' mp q (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b)))) \<and> option_to_ctcb_ptr (ntfnBoundTCB a) = tcb_Ptr (ntfnBoundTCB_CL (notification_lift b))) = ((case ntfnObj a of Structures_H.ntfn.IdleNtfn \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Idle \<and> ep_queue_relation' mp' [] (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' mp' [] (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' mp' q (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b)))) \<and> option_to_ctcb_ptr (ntfnBoundTCB a) = tcb_Ptr (ntfnBoundTCB_CL (notification_lift b)))
 3. \<And>x3. \<lbrakk>\<And>p. \<lbrakk>p \<in> tcb_ptr_to_ctcb_ptr ` set (ntfnQueue (ntfnObj a)); isWaitingNtfn (ntfnObj a)\<rbrakk> \<Longrightarrow> mp p = mp' p; ntfnObj a = Structures_H.ntfn.WaitingNtfn x3\<rbrakk> \<Longrightarrow> ((case ntfnObj a of Structures_H.ntfn.IdleNtfn \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Idle \<and> ep_queue_relation' mp [] (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' mp [] (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' mp q (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b)))) \<and> option_to_ctcb_ptr (ntfnBoundTCB a) = tcb_Ptr (ntfnBoundTCB_CL (notification_lift b))) = ((case ntfnObj a of Structures_H.ntfn.IdleNtfn \<Rightarrow> notification_CL.state_CL (notification_lift b) = SCAST(32 signed \<rightarrow> 32) NtfnState_Idle \<and> ep_queue_relation' mp' [] (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' mp' [] (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' mp' q (tcb_Ptr (ntfnQueue_head_CL (notification_lift b))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift b)))) \<and> option_to_ctcb_ptr (ntfnBoundTCB a) = tcb_Ptr (ntfnBoundTCB_CL (notification_lift b))) proof (prove)
goal:
No subgoals! proof (state)
this:
cnotification_relation mp a b = cnotification_relation mp' a b

goal:
No subgoals!