theory TcbQueue_C

lemma cnotification_relation_upd_tcb_no_queues:
  assumes cs: "mp thread = Some tcb"
  and   next_pres: "option_map tcbEPNext_C \<circ> mp = option_map tcbEPNext_C \<circ> mp'"
  and   prev_pres: "option_map tcbEPPrev_C \<circ> mp = option_map tcbEPPrev_C \<circ> mp'"
  shows "cnotification_relation mp a b = cnotification_relation mp' a b" proof - show ?thesis unfolding cnotification_relation_def apply (simp add: Let_def) apply (cases "ntfnObj a") apply (simp add: tcb_queue_relation'_def tcb_queue_relation_only_next_prev [OF next_pres prev_pres, symmetric])+ 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. 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)
goal (1 subgoal):
 1. ((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. ntfnObj a = Structures_H.ntfn.IdleNtfn \<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. ntfnObj a = Structures_H.ntfn.ActiveNtfn x2 \<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. ntfnObj a = Structures_H.ntfn.WaitingNtfn x3 \<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!