theory TcbQueue_C

lemma cendpoint_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 "cendpoint_relation mp a b = cendpoint_relation mp' a b" proof - show ?thesis unfolding cendpoint_relation_def apply (simp add: Let_def) apply (cases 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. cendpoint_relation mp a b = cendpoint_relation mp' a b proof (state)
goal (1 subgoal):
 1. cendpoint_relation mp a b = cendpoint_relation mp' a b proof (prove)
goal (1 subgoal):
 1. cendpoint_relation mp a b = cendpoint_relation mp' a b proof (prove)
goal (1 subgoal):
 1. (let cstate = endpoint_CL.state_CL (endpoint_lift b); chead = (tcb_Ptr \<circ> epQueue_head_CL \<circ> endpoint_lift) b; cend = (tcb_Ptr \<circ> epQueue_tail_CL \<circ> endpoint_lift) b in case a of Structures_H.endpoint.RecvEP q \<Rightarrow> cstate = SCAST(32 signed \<rightarrow> 32) EPState_Recv \<and> ep_queue_relation' mp q chead cend | Structures_H.endpoint.IdleEP \<Rightarrow> cstate = SCAST(32 signed \<rightarrow> 32) EPState_Idle \<and> ep_queue_relation' mp [] chead cend | Structures_H.endpoint.SendEP q \<Rightarrow> cstate = SCAST(32 signed \<rightarrow> 32) EPState_Send \<and> ep_queue_relation' mp q chead cend) = (let cstate = endpoint_CL.state_CL (endpoint_lift b); chead = (tcb_Ptr \<circ> epQueue_head_CL \<circ> endpoint_lift) b; cend = (tcb_Ptr \<circ> epQueue_tail_CL \<circ> endpoint_lift) b in case a of Structures_H.endpoint.RecvEP q \<Rightarrow> cstate = SCAST(32 signed \<rightarrow> 32) EPState_Recv \<and> ep_queue_relation' mp' q chead cend | Structures_H.endpoint.IdleEP \<Rightarrow> cstate = SCAST(32 signed \<rightarrow> 32) EPState_Idle \<and> ep_queue_relation' mp' [] chead cend | Structures_H.endpoint.SendEP q \<Rightarrow> cstate = SCAST(32 signed \<rightarrow> 32) EPState_Send \<and> ep_queue_relation' mp' q chead cend) proof (prove)
goal (1 subgoal):
 1. (case a of Structures_H.endpoint.RecvEP q \<Rightarrow> endpoint_CL.state_CL (endpoint_lift b) = SCAST(32 signed \<rightarrow> 32) EPState_Recv \<and> ep_queue_relation' mp q (tcb_Ptr (epQueue_head_CL (endpoint_lift b))) (tcb_Ptr (epQueue_tail_CL (endpoint_lift b))) | Structures_H.endpoint.IdleEP \<Rightarrow> endpoint_CL.state_CL (endpoint_lift b) = SCAST(32 signed \<rightarrow> 32) EPState_Idle \<and> ep_queue_relation' mp [] (tcb_Ptr (epQueue_head_CL (endpoint_lift b))) (tcb_Ptr (epQueue_tail_CL (endpoint_lift b))) | Structures_H.endpoint.SendEP q \<Rightarrow> endpoint_CL.state_CL (endpoint_lift b) = SCAST(32 signed \<rightarrow> 32) EPState_Send \<and> ep_queue_relation' mp q (tcb_Ptr (epQueue_head_CL (endpoint_lift b))) (tcb_Ptr (epQueue_tail_CL (endpoint_lift b)))) = (case a of Structures_H.endpoint.RecvEP q \<Rightarrow> endpoint_CL.state_CL (endpoint_lift b) = SCAST(32 signed \<rightarrow> 32) EPState_Recv \<and> ep_queue_relation' mp' q (tcb_Ptr (epQueue_head_CL (endpoint_lift b))) (tcb_Ptr (epQueue_tail_CL (endpoint_lift b))) | Structures_H.endpoint.IdleEP \<Rightarrow> endpoint_CL.state_CL (endpoint_lift b) = SCAST(32 signed \<rightarrow> 32) EPState_Idle \<and> ep_queue_relation' mp' [] (tcb_Ptr (epQueue_head_CL (endpoint_lift b))) (tcb_Ptr (epQueue_tail_CL (endpoint_lift b))) | Structures_H.endpoint.SendEP q \<Rightarrow> endpoint_CL.state_CL (endpoint_lift b) = SCAST(32 signed \<rightarrow> 32) EPState_Send \<and> ep_queue_relation' mp' q (tcb_Ptr (epQueue_head_CL (endpoint_lift b))) (tcb_Ptr (epQueue_tail_CL (endpoint_lift b)))) proof (prove)
goal (3 subgoals):
 1. \<And>x1. a = Structures_H.endpoint.RecvEP x1 \<Longrightarrow> (case a of Structures_H.endpoint.RecvEP q \<Rightarrow> endpoint_CL.state_CL (endpoint_lift b) = SCAST(32 signed \<rightarrow> 32) EPState_Recv \<and> ep_queue_relation' mp q (tcb_Ptr (epQueue_head_CL (endpoint_lift b))) (tcb_Ptr (epQueue_tail_CL (endpoint_lift b))) | Structures_H.endpoint.IdleEP \<Rightarrow> endpoint_CL.state_CL (endpoint_lift b) = SCAST(32 signed \<rightarrow> 32) EPState_Idle \<and> ep_queue_relation' mp [] (tcb_Ptr (epQueue_head_CL (endpoint_lift b))) (tcb_Ptr (epQueue_tail_CL (endpoint_lift b))) | Structures_H.endpoint.SendEP q \<Rightarrow> endpoint_CL.state_CL (endpoint_lift b) = SCAST(32 signed \<rightarrow> 32) EPState_Send \<and> ep_queue_relation' mp q (tcb_Ptr (epQueue_head_CL (endpoint_lift b))) (tcb_Ptr (epQueue_tail_CL (endpoint_lift b)))) = (case a of Structures_H.endpoint.RecvEP q \<Rightarrow> endpoint_CL.state_CL (endpoint_lift b) = SCAST(32 signed \<rightarrow> 32) EPState_Recv \<and> ep_queue_relation' mp' q (tcb_Ptr (epQueue_head_CL (endpoint_lift b))) (tcb_Ptr (epQueue_tail_CL (endpoint_lift b))) | Structures_H.endpoint.IdleEP \<Rightarrow> endpoint_CL.state_CL (endpoint_lift b) = SCAST(32 signed \<rightarrow> 32) EPState_Idle \<and> ep_queue_relation' mp' [] (tcb_Ptr (epQueue_head_CL (endpoint_lift b))) (tcb_Ptr (epQueue_tail_CL (endpoint_lift b))) | Structures_H.endpoint.SendEP q \<Rightarrow> endpoint_CL.state_CL (endpoint_lift b) = SCAST(32 signed \<rightarrow> 32) EPState_Send \<and> ep_queue_relation' mp' q (tcb_Ptr (epQueue_head_CL (endpoint_lift b))) (tcb_Ptr (epQueue_tail_CL (endpoint_lift b))))
 2. a = Structures_H.endpoint.IdleEP \<Longrightarrow> (case a of Structures_H.endpoint.RecvEP q \<Rightarrow> endpoint_CL.state_CL (endpoint_lift b) = SCAST(32 signed \<rightarrow> 32) EPState_Recv \<and> ep_queue_relation' mp q (tcb_Ptr (epQueue_head_CL (endpoint_lift b))) (tcb_Ptr (epQueue_tail_CL (endpoint_lift b))) | Structures_H.endpoint.IdleEP \<Rightarrow> endpoint_CL.state_CL (endpoint_lift b) = SCAST(32 signed \<rightarrow> 32) EPState_Idle \<and> ep_queue_relation' mp [] (tcb_Ptr (epQueue_head_CL (endpoint_lift b))) (tcb_Ptr (epQueue_tail_CL (endpoint_lift b))) | Structures_H.endpoint.SendEP q \<Rightarrow> endpoint_CL.state_CL (endpoint_lift b) = SCAST(32 signed \<rightarrow> 32) EPState_Send \<and> ep_queue_relation' mp q (tcb_Ptr (epQueue_head_CL (endpoint_lift b))) (tcb_Ptr (epQueue_tail_CL (endpoint_lift b)))) = (case a of Structures_H.endpoint.RecvEP q \<Rightarrow> endpoint_CL.state_CL (endpoint_lift b) = SCAST(32 signed \<rightarrow> 32) EPState_Recv \<and> ep_queue_relation' mp' q (tcb_Ptr (epQueue_head_CL (endpoint_lift b))) (tcb_Ptr (epQueue_tail_CL (endpoint_lift b))) | Structures_H.endpoint.IdleEP \<Rightarrow> endpoint_CL.state_CL (endpoint_lift b) = SCAST(32 signed \<rightarrow> 32) EPState_Idle \<and> ep_queue_relation' mp' [] (tcb_Ptr (epQueue_head_CL (endpoint_lift b))) (tcb_Ptr (epQueue_tail_CL (endpoint_lift b))) | Structures_H.endpoint.SendEP q \<Rightarrow> endpoint_CL.state_CL (endpoint_lift b) = SCAST(32 signed \<rightarrow> 32) EPState_Send \<and> ep_queue_relation' mp' q (tcb_Ptr (epQueue_head_CL (endpoint_lift b))) (tcb_Ptr (epQueue_tail_CL (endpoint_lift b))))
 3. \<And>x3. a = Structures_H.endpoint.SendEP x3 \<Longrightarrow> (case a of Structures_H.endpoint.RecvEP q \<Rightarrow> endpoint_CL.state_CL (endpoint_lift b) = SCAST(32 signed \<rightarrow> 32) EPState_Recv \<and> ep_queue_relation' mp q (tcb_Ptr (epQueue_head_CL (endpoint_lift b))) (tcb_Ptr (epQueue_tail_CL (endpoint_lift b))) | Structures_H.endpoint.IdleEP \<Rightarrow> endpoint_CL.state_CL (endpoint_lift b) = SCAST(32 signed \<rightarrow> 32) EPState_Idle \<and> ep_queue_relation' mp [] (tcb_Ptr (epQueue_head_CL (endpoint_lift b))) (tcb_Ptr (epQueue_tail_CL (endpoint_lift b))) | Structures_H.endpoint.SendEP q \<Rightarrow> endpoint_CL.state_CL (endpoint_lift b) = SCAST(32 signed \<rightarrow> 32) EPState_Send \<and> ep_queue_relation' mp q (tcb_Ptr (epQueue_head_CL (endpoint_lift b))) (tcb_Ptr (epQueue_tail_CL (endpoint_lift b)))) = (case a of Structures_H.endpoint.RecvEP q \<Rightarrow> endpoint_CL.state_CL (endpoint_lift b) = SCAST(32 signed \<rightarrow> 32) EPState_Recv \<and> ep_queue_relation' mp' q (tcb_Ptr (epQueue_head_CL (endpoint_lift b))) (tcb_Ptr (epQueue_tail_CL (endpoint_lift b))) | Structures_H.endpoint.IdleEP \<Rightarrow> endpoint_CL.state_CL (endpoint_lift b) = SCAST(32 signed \<rightarrow> 32) EPState_Idle \<and> ep_queue_relation' mp' [] (tcb_Ptr (epQueue_head_CL (endpoint_lift b))) (tcb_Ptr (epQueue_tail_CL (endpoint_lift b))) | Structures_H.endpoint.SendEP q \<Rightarrow> endpoint_CL.state_CL (endpoint_lift b) = SCAST(32 signed \<rightarrow> 32) EPState_Send \<and> ep_queue_relation' mp' q (tcb_Ptr (epQueue_head_CL (endpoint_lift b))) (tcb_Ptr (epQueue_tail_CL (endpoint_lift b)))) proof (prove)
goal:
No subgoals! proof (state)
this:
cendpoint_relation mp a b = cendpoint_relation mp' a b

goal:
No subgoals!