theory Fastpath_C

lemma cnotification_relation_isActive:
  "cnotification_relation tcbs ntfn ntfn'
       \<Longrightarrow> (notification_CL.state_CL (notification_lift ntfn') = scast NtfnState_Active)
     = EndpointDecls_H.isActive ntfn" apply (clarsimp simp: cnotification_relation_def Let_def) apply (cases ntfn, simp) apply (rename_tac ntfna ooeuoue) apply (case_tac ntfna, simp_all add: notification_state_defs isActive_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cnotification_relation tcbs ntfn ntfn' \<Longrightarrow> (notification_CL.state_CL (notification_lift ntfn') = SCAST(32 signed \<rightarrow> 32) NtfnState_Active) = EndpointDecls_H.isActive ntfn proof (prove)
goal (1 subgoal):
 1. \<lbrakk>case ntfnObj ntfn of Structures_H.ntfn.IdleNtfn \<Rightarrow> notification_CL.state_CL (notification_lift ntfn') = SCAST(32 signed \<rightarrow> 32) NtfnState_Idle \<and> ep_queue_relation' tcbs [] (tcb_Ptr (ntfnQueue_head_CL (notification_lift ntfn'))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift ntfn'))) | Structures_H.ntfn.ActiveNtfn msgid \<Rightarrow> notification_CL.state_CL (notification_lift ntfn') = SCAST(32 signed \<rightarrow> 32) NtfnState_Active \<and> msgid = ntfnMsgIdentifier_CL (notification_lift ntfn') \<and> ep_queue_relation' tcbs [] (tcb_Ptr (ntfnQueue_head_CL (notification_lift ntfn'))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift ntfn'))) | Structures_H.ntfn.WaitingNtfn q \<Rightarrow> notification_CL.state_CL (notification_lift ntfn') = SCAST(32 signed \<rightarrow> 32) NtfnState_Waiting \<and> ep_queue_relation' tcbs q (tcb_Ptr (ntfnQueue_head_CL (notification_lift ntfn'))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift ntfn'))); option_to_ctcb_ptr (ntfnBoundTCB ntfn) = tcb_Ptr (ntfnBoundTCB_CL (notification_lift ntfn'))\<rbrakk> \<Longrightarrow> (notification_CL.state_CL (notification_lift ntfn') = SCAST(32 signed \<rightarrow> 32) NtfnState_Active) = EndpointDecls_H.isActive ntfn proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>case x1 of Structures_H.ntfn.IdleNtfn \<Rightarrow> notification_CL.state_CL (notification_lift ntfn') = SCAST(32 signed \<rightarrow> 32) NtfnState_Idle \<and> ep_queue_relation' tcbs [] (tcb_Ptr (ntfnQueue_head_CL (notification_lift ntfn'))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift ntfn'))) | Structures_H.ntfn.ActiveNtfn msgid \<Rightarrow> notification_CL.state_CL (notification_lift ntfn') = SCAST(32 signed \<rightarrow> 32) NtfnState_Active \<and> msgid = ntfnMsgIdentifier_CL (notification_lift ntfn') \<and> ep_queue_relation' tcbs [] (tcb_Ptr (ntfnQueue_head_CL (notification_lift ntfn'))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift ntfn'))) | Structures_H.ntfn.WaitingNtfn q \<Rightarrow> notification_CL.state_CL (notification_lift ntfn') = SCAST(32 signed \<rightarrow> 32) NtfnState_Waiting \<and> ep_queue_relation' tcbs q (tcb_Ptr (ntfnQueue_head_CL (notification_lift ntfn'))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift ntfn'))); option_to_ctcb_ptr x2 = tcb_Ptr (ntfnBoundTCB_CL (notification_lift ntfn')); ntfn = NTFN x1 x2\<rbrakk> \<Longrightarrow> (notification_CL.state_CL (notification_lift ntfn') = SCAST(32 signed \<rightarrow> 32) NtfnState_Active) = EndpointDecls_H.isActive (NTFN x1 x2) proof (prove)
goal (1 subgoal):
 1. \<And>ntfna ooeuoue. \<lbrakk>case ntfna of Structures_H.ntfn.IdleNtfn \<Rightarrow> notification_CL.state_CL (notification_lift ntfn') = SCAST(32 signed \<rightarrow> 32) NtfnState_Idle \<and> ep_queue_relation' tcbs [] (tcb_Ptr (ntfnQueue_head_CL (notification_lift ntfn'))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift ntfn'))) | Structures_H.ntfn.ActiveNtfn msgid \<Rightarrow> notification_CL.state_CL (notification_lift ntfn') = SCAST(32 signed \<rightarrow> 32) NtfnState_Active \<and> msgid = ntfnMsgIdentifier_CL (notification_lift ntfn') \<and> ep_queue_relation' tcbs [] (tcb_Ptr (ntfnQueue_head_CL (notification_lift ntfn'))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift ntfn'))) | Structures_H.ntfn.WaitingNtfn q \<Rightarrow> notification_CL.state_CL (notification_lift ntfn') = SCAST(32 signed \<rightarrow> 32) NtfnState_Waiting \<and> ep_queue_relation' tcbs q (tcb_Ptr (ntfnQueue_head_CL (notification_lift ntfn'))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift ntfn'))); option_to_ctcb_ptr ooeuoue = tcb_Ptr (ntfnBoundTCB_CL (notification_lift ntfn')); ntfn = NTFN ntfna ooeuoue\<rbrakk> \<Longrightarrow> (notification_CL.state_CL (notification_lift ntfn') = SCAST(32 signed \<rightarrow> 32) NtfnState_Active) = EndpointDecls_H.isActive (NTFN ntfna ooeuoue) proof (prove)
goal:
No subgoals!