theory Ipc_C

lemma tcbEPAppend_update:
  assumes sr: "ep_queue_relation' mp queue qhead qend"
  and    qe': "qend' \<notin> tcb_ptr_to_ctcb_ptr ` set queue"
  and  cs_tcb: "mp qend' = Some tcb"
  and valid_ep: "\<forall>t\<in>set queue. tcb_at' t s" "distinct queue"
  and     qeN: "qend' \<noteq> NULL"
  shows "ep_queue_relation'
                   (upd_unless_null qend (tcbEPNext_C_update (\<lambda>_. qend') (the (mp qend)))
                (mp(qend' \<mapsto> tcb\<lparr>tcbEPPrev_C := qend, tcbEPNext_C := NULL\<rparr>)))
            (queue @ [ctcb_ptr_to_tcb_ptr qend'])
            (if qhead = NULL then qend' else qhead) qend'" using sr qe' cs_tcb valid_ep qeN apply - apply (erule tcb_queue_relationE') apply (rule tcb_queue_relationI') apply (erule(6) tcb_queue_relation_update_end
             [where getNext_update = tcbEPNext_C_update
                and getPrev_update = tcbEPPrev_C_update]) apply simp_all done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ep_queue_relation' (upd_unless_null qend (tcbEPNext_C_update (\<lambda>_. qend') (the (mp qend))) (mp(qend' \<mapsto> tcbEPNext_C_update (\<lambda>_. NULL) (tcbEPPrev_C_update (\<lambda>_. qend) tcb)))) (queue @ [ctcb_ptr_to_tcb_ptr qend']) (if qhead = NULL then qend' else qhead) qend' proof (prove)
using this:
ep_queue_relation' mp queue qhead qend
qend' \<notin> tcb_ptr_to_ctcb_ptr ` set queue
mp qend' = Some tcb
\<forall>t\<in>set queue. tcb_at' t s
distinct queue
qend' \<noteq> NULL

goal (1 subgoal):
 1. ep_queue_relation' (upd_unless_null qend (tcbEPNext_C_update (\<lambda>_. qend') (the (mp qend))) (mp(qend' \<mapsto> tcbEPNext_C_update (\<lambda>_. NULL) (tcbEPPrev_C_update (\<lambda>_. qend) tcb)))) (queue @ [ctcb_ptr_to_tcb_ptr qend']) (if qhead = NULL then qend' else qhead) qend' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ep_queue_relation' mp queue qhead qend; qend' \<notin> tcb_ptr_to_ctcb_ptr ` set queue; mp qend' = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; qend' \<noteq> NULL\<rbrakk> \<Longrightarrow> ep_queue_relation' (upd_unless_null qend (tcbEPNext_C_update (\<lambda>_. qend') (the (mp qend))) (mp(qend' \<mapsto> tcbEPNext_C_update (\<lambda>_. NULL) (tcbEPPrev_C_update (\<lambda>_. qend) tcb)))) (queue @ [ctcb_ptr_to_tcb_ptr qend']) (if qhead = NULL then qend' else qhead) qend' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>qend' \<notin> tcb_ptr_to_ctcb_ptr ` set queue; mp qend' = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; qend' \<noteq> NULL; ep_queue_relation mp queue NULL qhead; qend = (if queue = [] then NULL else tcb_ptr_to_ctcb_ptr (last queue))\<rbrakk> \<Longrightarrow> ep_queue_relation' (upd_unless_null qend (tcbEPNext_C_update (\<lambda>_. qend') (the (mp qend))) (mp(qend' \<mapsto> tcbEPNext_C_update (\<lambda>_. NULL) (tcbEPPrev_C_update (\<lambda>_. qend) tcb)))) (queue @ [ctcb_ptr_to_tcb_ptr qend']) (if qhead = NULL then qend' else qhead) qend' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>qend' \<notin> tcb_ptr_to_ctcb_ptr ` set queue; mp qend' = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; qend' \<noteq> NULL; ep_queue_relation mp queue NULL qhead; qend = (if queue = [] then NULL else tcb_ptr_to_ctcb_ptr (last queue))\<rbrakk> \<Longrightarrow> ep_queue_relation (upd_unless_null qend (tcbEPNext_C_update (\<lambda>_. qend') (the (mp qend))) (mp(qend' \<mapsto> tcbEPNext_C_update (\<lambda>_. NULL) (tcbEPPrev_C_update (\<lambda>_. qend) tcb)))) (queue @ [ctcb_ptr_to_tcb_ptr qend']) NULL (if qhead = NULL then qend' else qhead)
 2. \<lbrakk>qend' \<notin> tcb_ptr_to_ctcb_ptr ` set queue; mp qend' = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; qend' \<noteq> NULL; ep_queue_relation mp queue NULL qhead; qend = (if queue = [] then NULL else tcb_ptr_to_ctcb_ptr (last queue))\<rbrakk> \<Longrightarrow> qend' = (if queue @ [ctcb_ptr_to_tcb_ptr qend'] = [] then NULL else tcb_ptr_to_ctcb_ptr (last (queue @ [ctcb_ptr_to_tcb_ptr qend']))) proof (prove)
goal (6 subgoals):
 1. \<lbrakk>qend' \<notin> tcb_ptr_to_ctcb_ptr ` set queue; mp qend' = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; qend' \<noteq> NULL; qend = (if queue = [] then NULL else tcb_ptr_to_ctcb_ptr (last queue))\<rbrakk> \<Longrightarrow> queue = [] \<longrightarrow> NULL = NULL
 2. \<lbrakk>qend' \<notin> tcb_ptr_to_ctcb_ptr ` set queue; mp qend' = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; qend' \<noteq> NULL; qend = (if queue = [] then NULL else tcb_ptr_to_ctcb_ptr (last queue))\<rbrakk> \<Longrightarrow> fg_cons tcbEPNext_C (tcbEPNext_C_update \<circ> (\<lambda>x _. x))
 3. \<lbrakk>qend' \<notin> tcb_ptr_to_ctcb_ptr ` set queue; mp qend' = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; qend' \<noteq> NULL; qend = (if queue = [] then NULL else tcb_ptr_to_ctcb_ptr (last queue))\<rbrakk> \<Longrightarrow> fg_cons tcbEPPrev_C (tcbEPPrev_C_update \<circ> (\<lambda>x _. x))
 4. \<And>f t. \<lbrakk>qend' \<notin> tcb_ptr_to_ctcb_ptr ` set queue; mp qend' = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; qend' \<noteq> NULL; qend = (if queue = [] then NULL else tcb_ptr_to_ctcb_ptr (last queue))\<rbrakk> \<Longrightarrow> tcbEPNext_C (tcbEPPrev_C_update f t) = tcbEPNext_C t
 5. \<And>f t. \<lbrakk>qend' \<notin> tcb_ptr_to_ctcb_ptr ` set queue; mp qend' = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; qend' \<noteq> NULL; qend = (if queue = [] then NULL else tcb_ptr_to_ctcb_ptr (last queue))\<rbrakk> \<Longrightarrow> tcbEPPrev_C (tcbEPNext_C_update f t) = tcbEPPrev_C t
 6. \<lbrakk>qend' \<notin> tcb_ptr_to_ctcb_ptr ` set queue; mp qend' = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; qend' \<noteq> NULL; ep_queue_relation mp queue NULL qhead; qend = (if queue = [] then NULL else tcb_ptr_to_ctcb_ptr (last queue))\<rbrakk> \<Longrightarrow> qend' = (if queue @ [ctcb_ptr_to_tcb_ptr qend'] = [] then NULL else tcb_ptr_to_ctcb_ptr (last (queue @ [ctcb_ptr_to_tcb_ptr qend']))) proof (prove)
goal:
No subgoals!