theory IpcCancel_C

lemma ep_to_ep_queue:
  assumes ko: "ko_at' ep' ep s"
  and     waiting: "(isSendEP ep' \<or> isRecvEP ep')"
  and     rf: "(s, s') \<in> rf_sr"
  shows "ep_queue_relation' (cslift s') (epQueue ep')
              (Ptr (epQueue_head_CL
                     (endpoint_lift (the (cslift s' (Ptr ep))))))
              (Ptr (epQueue_tail_CL
                     (endpoint_lift (the (cslift s' (Ptr ep))))))" proof - from rf have
    "cmap_relation (map_to_eps (ksPSpace s)) (cslift s') Ptr (cendpoint_relation (cslift s'))" by (rule cmap_relation_ep) thus ?thesis using ko waiting apply - apply (erule (1) cmap_relation_ko_atE) apply (clarsimp simp: cendpoint_relation_def Let_def isSendEP_def isRecvEP_def split: endpoint.splits) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ep_queue_relation' (cslift s') (epQueue ep') (tcb_Ptr (epQueue_head_CL (endpoint_lift (the (cslift s' (ep_Ptr ep)))))) (tcb_Ptr (epQueue_tail_CL (endpoint_lift (the (cslift s' (ep_Ptr ep)))))) proof (state)
goal (1 subgoal):
 1. ep_queue_relation' (cslift s') (epQueue ep') (tcb_Ptr (epQueue_head_CL (endpoint_lift (the (cslift s' (ep_Ptr ep)))))) (tcb_Ptr (epQueue_tail_CL (endpoint_lift (the (cslift s' (ep_Ptr ep)))))) proof (chain)
picking this:
(s, s') \<in> rf_sr proof (prove)
using this:
(s, s') \<in> rf_sr

goal (1 subgoal):
 1. cmap_relation (map_to_eps (ksPSpace s)) (cslift s') ep_Ptr (cendpoint_relation (cslift s')) proof (state)
this:
cmap_relation (map_to_eps (ksPSpace s)) (cslift s') ep_Ptr (cendpoint_relation (cslift s'))

goal (1 subgoal):
 1. ep_queue_relation' (cslift s') (epQueue ep') (tcb_Ptr (epQueue_head_CL (endpoint_lift (the (cslift s' (ep_Ptr ep)))))) (tcb_Ptr (epQueue_tail_CL (endpoint_lift (the (cslift s' (ep_Ptr ep)))))) proof (prove)
using this:
cmap_relation (map_to_eps (ksPSpace s)) (cslift s') ep_Ptr (cendpoint_relation (cslift s'))

goal (1 subgoal):
 1. ep_queue_relation' (cslift s') (epQueue ep') (tcb_Ptr (epQueue_head_CL (endpoint_lift (the (cslift s' (ep_Ptr ep)))))) (tcb_Ptr (epQueue_tail_CL (endpoint_lift (the (cslift s' (ep_Ptr ep)))))) proof (prove)
using this:
cmap_relation (map_to_eps (ksPSpace s)) (cslift s') ep_Ptr (cendpoint_relation (cslift s'))
ko_at' ep' ep s
isSendEP ep' \<or> isRecvEP ep'

goal (1 subgoal):
 1. ep_queue_relation' (cslift s') (epQueue ep') (tcb_Ptr (epQueue_head_CL (endpoint_lift (the (cslift s' (ep_Ptr ep)))))) (tcb_Ptr (epQueue_tail_CL (endpoint_lift (the (cslift s' (ep_Ptr ep)))))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cmap_relation (map_to_eps (ksPSpace s)) (cslift s') ep_Ptr (cendpoint_relation (cslift s')); ko_at' ep' ep s; isSendEP ep' \<or> isRecvEP ep'\<rbrakk> \<Longrightarrow> ep_queue_relation' (cslift s') (epQueue ep') (tcb_Ptr (epQueue_head_CL (endpoint_lift (the (cslift s' (ep_Ptr ep)))))) (tcb_Ptr (epQueue_tail_CL (endpoint_lift (the (cslift s' (ep_Ptr ep)))))) proof (prove)
goal (1 subgoal):
 1. \<And>ko'. \<lbrakk>ko_at' ep' ep s; isSendEP ep' \<or> isRecvEP ep'; cslift s' (ep_Ptr ep) = Some ko'; cendpoint_relation (cslift s') ep' ko'\<rbrakk> \<Longrightarrow> ep_queue_relation' (cslift s') (epQueue ep') (tcb_Ptr (epQueue_head_CL (endpoint_lift (the (cslift s' (ep_Ptr ep)))))) (tcb_Ptr (epQueue_tail_CL (endpoint_lift (the (cslift s' (ep_Ptr ep)))))) proof (prove)
goal:
No subgoals! proof (state)
this:
ep_queue_relation' (cslift s') (epQueue ep') (tcb_Ptr (epQueue_head_CL (endpoint_lift (the (cslift s' (ep_Ptr ep)))))) (tcb_Ptr (epQueue_tail_CL (endpoint_lift (the (cslift s' (ep_Ptr ep))))))

goal:
No subgoals!