theory SR_lemmas_C

lemma ntfn_to_ep_queue:
  assumes ko: "ko_at' ntfn' ntfn s"
  and     waiting: "isWaitingNtfn (ntfnObj ntfn')"
  and     rf: "(s, s') \<in> rf_sr"
  shows "ep_queue_relation' (cslift s') (ntfnQueue (ntfnObj ntfn'))
              (Ptr (ntfnQueue_head_CL
                     (notification_lift (the (cslift s' (Ptr ntfn))))))
              (Ptr (ntfnQueue_tail_CL
                     (notification_lift (the (cslift s' (Ptr ntfn))))))" proof - from rf have
    "cmap_relation (map_to_ntfns (ksPSpace s)) (cslift s') Ptr (cnotification_relation (cslift s'))" by (rule cmap_relation_ntfn) thus ?thesis using ko waiting apply - apply (erule (1) cmap_relation_ko_atE) apply (clarsimp simp: cnotification_relation_def Let_def isWaitingNtfn_def
                   split: Structures_H.notification.splits ntfn.splits) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ep_queue_relation' (cslift s') (ntfnQueue (ntfnObj ntfn')) (tcb_Ptr (ntfnQueue_head_CL (notification_lift (the (cslift s' (ntfn_Ptr ntfn)))))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift (the (cslift s' (ntfn_Ptr ntfn)))))) proof (state)
goal (1 subgoal):
 1. ep_queue_relation' (cslift s') (ntfnQueue (ntfnObj ntfn')) (tcb_Ptr (ntfnQueue_head_CL (notification_lift (the (cslift s' (ntfn_Ptr ntfn)))))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift (the (cslift s' (ntfn_Ptr ntfn)))))) 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_ntfns (ksPSpace s)) (cslift s') ntfn_Ptr (cnotification_relation (cslift s')) proof (state)
this:
cmap_relation (map_to_ntfns (ksPSpace s)) (cslift s') ntfn_Ptr (cnotification_relation (cslift s'))

goal (1 subgoal):
 1. ep_queue_relation' (cslift s') (ntfnQueue (ntfnObj ntfn')) (tcb_Ptr (ntfnQueue_head_CL (notification_lift (the (cslift s' (ntfn_Ptr ntfn)))))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift (the (cslift s' (ntfn_Ptr ntfn)))))) proof (prove)
using this:
cmap_relation (map_to_ntfns (ksPSpace s)) (cslift s') ntfn_Ptr (cnotification_relation (cslift s'))

goal (1 subgoal):
 1. ep_queue_relation' (cslift s') (ntfnQueue (ntfnObj ntfn')) (tcb_Ptr (ntfnQueue_head_CL (notification_lift (the (cslift s' (ntfn_Ptr ntfn)))))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift (the (cslift s' (ntfn_Ptr ntfn)))))) proof (prove)
using this:
cmap_relation (map_to_ntfns (ksPSpace s)) (cslift s') ntfn_Ptr (cnotification_relation (cslift s'))
ko_at' ntfn' ntfn s
isWaitingNtfn (ntfnObj ntfn')

goal (1 subgoal):
 1. ep_queue_relation' (cslift s') (ntfnQueue (ntfnObj ntfn')) (tcb_Ptr (ntfnQueue_head_CL (notification_lift (the (cslift s' (ntfn_Ptr ntfn)))))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift (the (cslift s' (ntfn_Ptr ntfn)))))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cmap_relation (map_to_ntfns (ksPSpace s)) (cslift s') ntfn_Ptr (cnotification_relation (cslift s')); ko_at' ntfn' ntfn s; isWaitingNtfn (ntfnObj ntfn')\<rbrakk> \<Longrightarrow> ep_queue_relation' (cslift s') (ntfnQueue (ntfnObj ntfn')) (tcb_Ptr (ntfnQueue_head_CL (notification_lift (the (cslift s' (ntfn_Ptr ntfn)))))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift (the (cslift s' (ntfn_Ptr ntfn)))))) proof (prove)
goal (1 subgoal):
 1. \<And>ko'. \<lbrakk>ko_at' ntfn' ntfn s; isWaitingNtfn (ntfnObj ntfn'); cslift s' (ntfn_Ptr ntfn) = Some ko'; cnotification_relation (cslift s') ntfn' ko'\<rbrakk> \<Longrightarrow> ep_queue_relation' (cslift s') (ntfnQueue (ntfnObj ntfn')) (tcb_Ptr (ntfnQueue_head_CL (notification_lift (the (cslift s' (ntfn_Ptr ntfn)))))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift (the (cslift s' (ntfn_Ptr ntfn)))))) proof (prove)
goal:
No subgoals! proof (state)
this:
ep_queue_relation' (cslift s') (ntfnQueue (ntfnObj ntfn')) (tcb_Ptr (ntfnQueue_head_CL (notification_lift (the (cslift s' (ntfn_Ptr ntfn)))))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift (the (cslift s' (ntfn_Ptr ntfn))))))

goal:
No subgoals!