theory Ipc_C

lemma tcb_queue_relation_update_end:
  fixes getNext_update :: "(tcb_C ptr \<Rightarrow> tcb_C ptr) \<Rightarrow> tcb_C \<Rightarrow> tcb_C" and
  getPrev_update :: "(tcb_C ptr \<Rightarrow> tcb_C ptr) \<Rightarrow> tcb_C \<Rightarrow> tcb_C"
  assumes qr: "tcb_queue_relation getNext getPrev mp queue qprev qhead"
  and      qe: "qend = (if queue = [] then NULL
                                      else tcb_ptr_to_ctcb_ptr (last queue))"
  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"
  and     qpN: "queue = [] \<longrightarrow> qprev = NULL"
  and     fgN: "fg_cons getNext (getNext_update \<circ> (\<lambda>x _. x))"
  and     fgP: "fg_cons getPrev (getPrev_update \<circ> (\<lambda>x _. x))"
  and     npu: "\<And>f t. getNext (getPrev_update f t) = getNext t"
  and     pnu: "\<And>f t. getPrev (getNext_update f t) = getPrev t"
  shows   "tcb_queue_relation getNext getPrev
                 (upd_unless_null qend (getNext_update (\<lambda>_. qend') (the (mp qend)))
                       (mp(qend' := Some (getNext_update (\<lambda>_. NULL) (getPrev_update (\<lambda>_. qend)  tcb)))))
                 (queue @ [ctcb_ptr_to_tcb_ptr qend'])
                 qprev (if qhead = NULL then qend' else qhead)" using qr qe qe' cs_tcb valid_ep qeN qpN proof (induct queue arbitrary: qhead qprev qend) case Nil thus ?case by (clarsimp simp: upd_unless_null_def fg_consD1 [OF fgN]
                       fg_consD1 [OF fgP] pnu npu) next case (Cons tcb' tcbs) have not_NULL[simplified]: "tcb_ptr_to_ctcb_ptr (last (tcb'#tcbs)) \<noteq> NULL"
                             "qhead \<noteq> NULL" using tcb_queue_relation_next_not_NULL tcb_queue_relation_last_not_NULL
          Cons tcb_at_not_NULL by (auto split: if_split) thus ?case using Cons.prems apply (clarsimp simp: upd_unless_null_def fg_consD1 [OF fgN]
                          fg_consD1 [OF fgP] pnu npu
                   split: if_split) apply (rule conjI, clarsimp) apply (rule impI) apply (subst tcb_queue_relation_cong) prefer 5 apply (erule Cons.hyps [OF _ refl], simp_all add: upd_unless_null_def) apply (frule(3) tcb_queue_relation_next_not_NULL, simp) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_queue_relation getNext getPrev (upd_unless_null qend (getNext_update (\<lambda>_. qend') (the (mp qend))) (mp(qend' \<mapsto> getNext_update (\<lambda>_. NULL) (getPrev_update (\<lambda>_. qend) tcb)))) (queue @ [ctcb_ptr_to_tcb_ptr qend']) qprev (if qhead = NULL then qend' else qhead) proof (prove)
using this:
tcb_queue_relation getNext getPrev mp queue qprev qhead
qend = (if queue = [] then NULL else tcb_ptr_to_ctcb_ptr (last queue))
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
queue = [] \<longrightarrow> qprev = NULL

goal (1 subgoal):
 1. tcb_queue_relation getNext getPrev (upd_unless_null qend (getNext_update (\<lambda>_. qend') (the (mp qend))) (mp(qend' \<mapsto> getNext_update (\<lambda>_. NULL) (getPrev_update (\<lambda>_. qend) tcb)))) (queue @ [ctcb_ptr_to_tcb_ptr qend']) qprev (if qhead = NULL then qend' else qhead) proof (state)
goal (2 subgoals):
 1. \<And>qhead qprev qend. \<lbrakk>tcb_queue_relation getNext getPrev mp [] qprev qhead; qend = (if [] = [] then NULL else tcb_ptr_to_ctcb_ptr (last [])); qend' \<notin> tcb_ptr_to_ctcb_ptr ` set []; mp qend' = Some tcb; \<forall>t\<in>set []. tcb_at' t s; distinct []; qend' \<noteq> NULL; [] = [] \<longrightarrow> qprev = NULL\<rbrakk> \<Longrightarrow> tcb_queue_relation getNext getPrev (upd_unless_null qend (getNext_update (\<lambda>_. qend') (the (mp qend))) (mp(qend' \<mapsto> getNext_update (\<lambda>_. NULL) (getPrev_update (\<lambda>_. qend) tcb)))) ([] @ [ctcb_ptr_to_tcb_ptr qend']) qprev (if qhead = NULL then qend' else qhead)
 2. \<And>x1 queue qhead qprev qend. \<lbrakk>\<And>qhead qprev qend. \<lbrakk>tcb_queue_relation getNext getPrev mp queue qprev qhead; qend = (if queue = [] then NULL else tcb_ptr_to_ctcb_ptr (last queue)); 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; queue = [] \<longrightarrow> qprev = NULL\<rbrakk> \<Longrightarrow> tcb_queue_relation getNext getPrev (upd_unless_null qend (getNext_update (\<lambda>_. qend') (the (mp qend))) (mp(qend' \<mapsto> getNext_update (\<lambda>_. NULL) (getPrev_update (\<lambda>_. qend) tcb)))) (queue @ [ctcb_ptr_to_tcb_ptr qend']) qprev (if qhead = NULL then qend' else qhead); tcb_queue_relation getNext getPrev mp (x1 # queue) qprev qhead; qend = (if x1 # queue = [] then NULL else tcb_ptr_to_ctcb_ptr (last (x1 # queue))); qend' \<notin> tcb_ptr_to_ctcb_ptr ` set (x1 # queue); mp qend' = Some tcb; \<forall>t\<in>set (x1 # queue). tcb_at' t s; distinct (x1 # queue); qend' \<noteq> NULL; x1 # queue = [] \<longrightarrow> qprev = NULL\<rbrakk> \<Longrightarrow> tcb_queue_relation getNext getPrev (upd_unless_null qend (getNext_update (\<lambda>_. qend') (the (mp qend))) (mp(qend' \<mapsto> getNext_update (\<lambda>_. NULL) (getPrev_update (\<lambda>_. qend) tcb)))) ((x1 # queue) @ [ctcb_ptr_to_tcb_ptr qend']) qprev (if qhead = NULL then qend' else qhead) proof (state)
this:
tcb_queue_relation getNext getPrev mp [] qprev qhead
qend = (if [] = [] then NULL else tcb_ptr_to_ctcb_ptr (last []))
qend' \<notin> tcb_ptr_to_ctcb_ptr ` set []
mp qend' = Some tcb
\<forall>t\<in>set []. tcb_at' t s
distinct []
qend' \<noteq> NULL
[] = [] \<longrightarrow> qprev = NULL

goal (2 subgoals):
 1. \<And>qhead qprev qend. \<lbrakk>tcb_queue_relation getNext getPrev mp [] qprev qhead; qend = (if [] = [] then NULL else tcb_ptr_to_ctcb_ptr (last [])); qend' \<notin> tcb_ptr_to_ctcb_ptr ` set []; mp qend' = Some tcb; \<forall>t\<in>set []. tcb_at' t s; distinct []; qend' \<noteq> NULL; [] = [] \<longrightarrow> qprev = NULL\<rbrakk> \<Longrightarrow> tcb_queue_relation getNext getPrev (upd_unless_null qend (getNext_update (\<lambda>_. qend') (the (mp qend))) (mp(qend' \<mapsto> getNext_update (\<lambda>_. NULL) (getPrev_update (\<lambda>_. qend) tcb)))) ([] @ [ctcb_ptr_to_tcb_ptr qend']) qprev (if qhead = NULL then qend' else qhead)
 2. \<And>x1 queue qhead qprev qend. \<lbrakk>\<And>qhead qprev qend. \<lbrakk>tcb_queue_relation getNext getPrev mp queue qprev qhead; qend = (if queue = [] then NULL else tcb_ptr_to_ctcb_ptr (last queue)); 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; queue = [] \<longrightarrow> qprev = NULL\<rbrakk> \<Longrightarrow> tcb_queue_relation getNext getPrev (upd_unless_null qend (getNext_update (\<lambda>_. qend') (the (mp qend))) (mp(qend' \<mapsto> getNext_update (\<lambda>_. NULL) (getPrev_update (\<lambda>_. qend) tcb)))) (queue @ [ctcb_ptr_to_tcb_ptr qend']) qprev (if qhead = NULL then qend' else qhead); tcb_queue_relation getNext getPrev mp (x1 # queue) qprev qhead; qend = (if x1 # queue = [] then NULL else tcb_ptr_to_ctcb_ptr (last (x1 # queue))); qend' \<notin> tcb_ptr_to_ctcb_ptr ` set (x1 # queue); mp qend' = Some tcb; \<forall>t\<in>set (x1 # queue). tcb_at' t s; distinct (x1 # queue); qend' \<noteq> NULL; x1 # queue = [] \<longrightarrow> qprev = NULL\<rbrakk> \<Longrightarrow> tcb_queue_relation getNext getPrev (upd_unless_null qend (getNext_update (\<lambda>_. qend') (the (mp qend))) (mp(qend' \<mapsto> getNext_update (\<lambda>_. NULL) (getPrev_update (\<lambda>_. qend) tcb)))) ((x1 # queue) @ [ctcb_ptr_to_tcb_ptr qend']) qprev (if qhead = NULL then qend' else qhead) proof (prove)
using this:
tcb_queue_relation getNext getPrev mp [] qprev qhead
qend = (if [] = [] then NULL else tcb_ptr_to_ctcb_ptr (last []))
qend' \<notin> tcb_ptr_to_ctcb_ptr ` set []
mp qend' = Some tcb
\<forall>t\<in>set []. tcb_at' t s
distinct []
qend' \<noteq> NULL
[] = [] \<longrightarrow> qprev = NULL

goal (1 subgoal):
 1. tcb_queue_relation getNext getPrev (upd_unless_null qend (getNext_update (\<lambda>_. qend') (the (mp qend))) (mp(qend' \<mapsto> getNext_update (\<lambda>_. NULL) (getPrev_update (\<lambda>_. qend) tcb)))) ([] @ [ctcb_ptr_to_tcb_ptr qend']) qprev (if qhead = NULL then qend' else qhead) proof (state)
this:
tcb_queue_relation getNext getPrev (upd_unless_null qend (getNext_update (\<lambda>_. qend') (the (mp qend))) (mp(qend' \<mapsto> getNext_update (\<lambda>_. NULL) (getPrev_update (\<lambda>_. qend) tcb)))) ([] @ [ctcb_ptr_to_tcb_ptr qend']) qprev (if qhead = NULL then qend' else qhead)

goal (1 subgoal):
 1. \<And>x1 queue qhead qprev qend. \<lbrakk>\<And>qhead qprev qend. \<lbrakk>tcb_queue_relation getNext getPrev mp queue qprev qhead; qend = (if queue = [] then NULL else tcb_ptr_to_ctcb_ptr (last queue)); 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; queue = [] \<longrightarrow> qprev = NULL\<rbrakk> \<Longrightarrow> tcb_queue_relation getNext getPrev (upd_unless_null qend (getNext_update (\<lambda>_. qend') (the (mp qend))) (mp(qend' \<mapsto> getNext_update (\<lambda>_. NULL) (getPrev_update (\<lambda>_. qend) tcb)))) (queue @ [ctcb_ptr_to_tcb_ptr qend']) qprev (if qhead = NULL then qend' else qhead); tcb_queue_relation getNext getPrev mp (x1 # queue) qprev qhead; qend = (if x1 # queue = [] then NULL else tcb_ptr_to_ctcb_ptr (last (x1 # queue))); qend' \<notin> tcb_ptr_to_ctcb_ptr ` set (x1 # queue); mp qend' = Some tcb; \<forall>t\<in>set (x1 # queue). tcb_at' t s; distinct (x1 # queue); qend' \<noteq> NULL; x1 # queue = [] \<longrightarrow> qprev = NULL\<rbrakk> \<Longrightarrow> tcb_queue_relation getNext getPrev (upd_unless_null qend (getNext_update (\<lambda>_. qend') (the (mp qend))) (mp(qend' \<mapsto> getNext_update (\<lambda>_. NULL) (getPrev_update (\<lambda>_. qend) tcb)))) ((x1 # queue) @ [ctcb_ptr_to_tcb_ptr qend']) qprev (if qhead = NULL then qend' else qhead) proof (state)
goal (1 subgoal):
 1. \<And>x1 queue qhead qprev qend. \<lbrakk>\<And>qhead qprev qend. \<lbrakk>tcb_queue_relation getNext getPrev mp queue qprev qhead; qend = (if queue = [] then NULL else tcb_ptr_to_ctcb_ptr (last queue)); 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; queue = [] \<longrightarrow> qprev = NULL\<rbrakk> \<Longrightarrow> tcb_queue_relation getNext getPrev (upd_unless_null qend (getNext_update (\<lambda>_. qend') (the (mp qend))) (mp(qend' \<mapsto> getNext_update (\<lambda>_. NULL) (getPrev_update (\<lambda>_. qend) tcb)))) (queue @ [ctcb_ptr_to_tcb_ptr qend']) qprev (if qhead = NULL then qend' else qhead); tcb_queue_relation getNext getPrev mp (x1 # queue) qprev qhead; qend = (if x1 # queue = [] then NULL else tcb_ptr_to_ctcb_ptr (last (x1 # queue))); qend' \<notin> tcb_ptr_to_ctcb_ptr ` set (x1 # queue); mp qend' = Some tcb; \<forall>t\<in>set (x1 # queue). tcb_at' t s; distinct (x1 # queue); qend' \<noteq> NULL; x1 # queue = [] \<longrightarrow> qprev = NULL\<rbrakk> \<Longrightarrow> tcb_queue_relation getNext getPrev (upd_unless_null qend (getNext_update (\<lambda>_. qend') (the (mp qend))) (mp(qend' \<mapsto> getNext_update (\<lambda>_. NULL) (getPrev_update (\<lambda>_. qend) tcb)))) ((x1 # queue) @ [ctcb_ptr_to_tcb_ptr qend']) qprev (if qhead = NULL then qend' else qhead) proof (state)
this:
\<lbrakk>tcb_queue_relation getNext getPrev mp tcbs ?qprev1 ?qhead1; ?qend1 = (if tcbs = [] then NULL else tcb_ptr_to_ctcb_ptr (last tcbs)); qend' \<notin> tcb_ptr_to_ctcb_ptr ` set tcbs; mp qend' = Some tcb; \<forall>t\<in>set tcbs. tcb_at' t s; distinct tcbs; qend' \<noteq> NULL; tcbs = [] \<longrightarrow> ?qprev1 = NULL\<rbrakk> \<Longrightarrow> tcb_queue_relation getNext getPrev (upd_unless_null ?qend1 (getNext_update (\<lambda>_. qend') (the (mp ?qend1))) (mp(qend' \<mapsto> getNext_update (\<lambda>_. NULL) (getPrev_update (\<lambda>_. ?qend1) tcb)))) (tcbs @ [ctcb_ptr_to_tcb_ptr qend']) ?qprev1 (if ?qhead1 = NULL then qend' else ?qhead1)
tcb_queue_relation getNext getPrev mp (tcb' # tcbs) qprev qhead
qend = (if tcb' # tcbs = [] then NULL else tcb_ptr_to_ctcb_ptr (last (tcb' # tcbs)))
qend' \<notin> tcb_ptr_to_ctcb_ptr ` set (tcb' # tcbs)
mp qend' = Some tcb
\<forall>t\<in>set (tcb' # tcbs). tcb_at' t s
distinct (tcb' # tcbs)
qend' \<noteq> NULL
tcb' # tcbs = [] \<longrightarrow> qprev = NULL

goal (1 subgoal):
 1. \<And>x1 queue qhead qprev qend. \<lbrakk>\<And>qhead qprev qend. \<lbrakk>tcb_queue_relation getNext getPrev mp queue qprev qhead; qend = (if queue = [] then NULL else tcb_ptr_to_ctcb_ptr (last queue)); 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; queue = [] \<longrightarrow> qprev = NULL\<rbrakk> \<Longrightarrow> tcb_queue_relation getNext getPrev (upd_unless_null qend (getNext_update (\<lambda>_. qend') (the (mp qend))) (mp(qend' \<mapsto> getNext_update (\<lambda>_. NULL) (getPrev_update (\<lambda>_. qend) tcb)))) (queue @ [ctcb_ptr_to_tcb_ptr qend']) qprev (if qhead = NULL then qend' else qhead); tcb_queue_relation getNext getPrev mp (x1 # queue) qprev qhead; qend = (if x1 # queue = [] then NULL else tcb_ptr_to_ctcb_ptr (last (x1 # queue))); qend' \<notin> tcb_ptr_to_ctcb_ptr ` set (x1 # queue); mp qend' = Some tcb; \<forall>t\<in>set (x1 # queue). tcb_at' t s; distinct (x1 # queue); qend' \<noteq> NULL; x1 # queue = [] \<longrightarrow> qprev = NULL\<rbrakk> \<Longrightarrow> tcb_queue_relation getNext getPrev (upd_unless_null qend (getNext_update (\<lambda>_. qend') (the (mp qend))) (mp(qend' \<mapsto> getNext_update (\<lambda>_. NULL) (getPrev_update (\<lambda>_. qend) tcb)))) ((x1 # queue) @ [ctcb_ptr_to_tcb_ptr qend']) qprev (if qhead = NULL then qend' else qhead) proof (prove)
goal (1 subgoal):
 1. tcb_ptr_to_ctcb_ptr (last (tcb' # tcbs)) \<noteq> NULL &&& qhead \<noteq> NULL proof (prove)
using this:
\<lbrakk>tcb_queue_relation ?getNext ?getPrev ?mp ?queue ?qprev ?qhead; \<forall>t\<in>set ?queue. tcb_at' t ?s; distinct ?queue; ?queue \<noteq> []\<rbrakk> \<Longrightarrow> ?qhead \<noteq> NULL
\<lbrakk>tcb_queue_relation ?getNext ?getPrev ?mp ?queue ?qprev ?qhead; \<forall>t\<in>set ?queue. tcb_at' t ?s; distinct ?queue; ?queue \<noteq> []\<rbrakk> \<Longrightarrow> tcb_ptr_to_ctcb_ptr (last ?queue) \<noteq> NULL
\<lbrakk>tcb_queue_relation getNext getPrev mp tcbs ?qprev1 ?qhead1; ?qend1 = (if tcbs = [] then NULL else tcb_ptr_to_ctcb_ptr (last tcbs)); qend' \<notin> tcb_ptr_to_ctcb_ptr ` set tcbs; mp qend' = Some tcb; \<forall>t\<in>set tcbs. tcb_at' t s; distinct tcbs; qend' \<noteq> NULL; tcbs = [] \<longrightarrow> ?qprev1 = NULL\<rbrakk> \<Longrightarrow> tcb_queue_relation getNext getPrev (upd_unless_null ?qend1 (getNext_update (\<lambda>_. qend') (the (mp ?qend1))) (mp(qend' \<mapsto> getNext_update (\<lambda>_. NULL) (getPrev_update (\<lambda>_. ?qend1) tcb)))) (tcbs @ [ctcb_ptr_to_tcb_ptr qend']) ?qprev1 (if ?qhead1 = NULL then qend' else ?qhead1)
tcb_queue_relation getNext getPrev mp (tcb' # tcbs) qprev qhead
qend = (if tcb' # tcbs = [] then NULL else tcb_ptr_to_ctcb_ptr (last (tcb' # tcbs)))
qend' \<notin> tcb_ptr_to_ctcb_ptr ` set (tcb' # tcbs)
mp qend' = Some tcb
\<forall>t\<in>set (tcb' # tcbs). tcb_at' t s
distinct (tcb' # tcbs)
qend' \<noteq> NULL
tcb' # tcbs = [] \<longrightarrow> qprev = NULL
tcb_at' ?t ?s \<Longrightarrow> tcb_ptr_to_ctcb_ptr ?t \<noteq> NULL

goal (1 subgoal):
 1. tcb_ptr_to_ctcb_ptr (last (tcb' # tcbs)) \<noteq> NULL &&& qhead \<noteq> NULL proof (state)
this:
tcb_ptr_to_ctcb_ptr (if tcbs = [] then tcb' else last tcbs) \<noteq> NULL
qhead \<noteq> NULL

goal (1 subgoal):
 1. \<And>x1 queue qhead qprev qend. \<lbrakk>\<And>qhead qprev qend. \<lbrakk>tcb_queue_relation getNext getPrev mp queue qprev qhead; qend = (if queue = [] then NULL else tcb_ptr_to_ctcb_ptr (last queue)); 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; queue = [] \<longrightarrow> qprev = NULL\<rbrakk> \<Longrightarrow> tcb_queue_relation getNext getPrev (upd_unless_null qend (getNext_update (\<lambda>_. qend') (the (mp qend))) (mp(qend' \<mapsto> getNext_update (\<lambda>_. NULL) (getPrev_update (\<lambda>_. qend) tcb)))) (queue @ [ctcb_ptr_to_tcb_ptr qend']) qprev (if qhead = NULL then qend' else qhead); tcb_queue_relation getNext getPrev mp (x1 # queue) qprev qhead; qend = (if x1 # queue = [] then NULL else tcb_ptr_to_ctcb_ptr (last (x1 # queue))); qend' \<notin> tcb_ptr_to_ctcb_ptr ` set (x1 # queue); mp qend' = Some tcb; \<forall>t\<in>set (x1 # queue). tcb_at' t s; distinct (x1 # queue); qend' \<noteq> NULL; x1 # queue = [] \<longrightarrow> qprev = NULL\<rbrakk> \<Longrightarrow> tcb_queue_relation getNext getPrev (upd_unless_null qend (getNext_update (\<lambda>_. qend') (the (mp qend))) (mp(qend' \<mapsto> getNext_update (\<lambda>_. NULL) (getPrev_update (\<lambda>_. qend) tcb)))) ((x1 # queue) @ [ctcb_ptr_to_tcb_ptr qend']) qprev (if qhead = NULL then qend' else qhead) proof (prove)
using this:
tcb_ptr_to_ctcb_ptr (if tcbs = [] then tcb' else last tcbs) \<noteq> NULL
qhead \<noteq> NULL

goal (1 subgoal):
 1. tcb_queue_relation getNext getPrev (upd_unless_null qend (getNext_update (\<lambda>_. qend') (the (mp qend))) (mp(qend' \<mapsto> getNext_update (\<lambda>_. NULL) (getPrev_update (\<lambda>_. qend) tcb)))) ((tcb' # tcbs) @ [ctcb_ptr_to_tcb_ptr qend']) qprev (if qhead = NULL then qend' else qhead) proof (prove)
using this:
tcb_ptr_to_ctcb_ptr (if tcbs = [] then tcb' else last tcbs) \<noteq> NULL
qhead \<noteq> NULL
tcb_queue_relation getNext getPrev mp (tcb' # tcbs) qprev qhead
qend = (if tcb' # tcbs = [] then NULL else tcb_ptr_to_ctcb_ptr (last (tcb' # tcbs)))
qend' \<notin> tcb_ptr_to_ctcb_ptr ` set (tcb' # tcbs)
mp qend' = Some tcb
\<forall>t\<in>set (tcb' # tcbs). tcb_at' t s
distinct (tcb' # tcbs)
qend' \<noteq> NULL
tcb' # tcbs = [] \<longrightarrow> qprev = NULL

goal (1 subgoal):
 1. tcb_queue_relation getNext getPrev (upd_unless_null qend (getNext_update (\<lambda>_. qend') (the (mp qend))) (mp(qend' \<mapsto> getNext_update (\<lambda>_. NULL) (getPrev_update (\<lambda>_. qend) tcb)))) ((tcb' # tcbs) @ [ctcb_ptr_to_tcb_ptr qend']) qprev (if qhead = NULL then qend' else qhead) proof (prove)
goal (1 subgoal):
 1. \<And>tcba. \<lbrakk>tcb_ptr_to_ctcb_ptr (last tcbs) \<noteq> NULL; tcb_ptr_to_ctcb_ptr tcb' \<noteq> NULL; qend = tcb_ptr_to_ctcb_ptr (last tcbs); mp qend' = Some tcb; qend' \<noteq> NULL; qhead = tcb_ptr_to_ctcb_ptr tcb'; qend' \<noteq> tcb_ptr_to_ctcb_ptr tcb'; qend' \<notin> tcb_ptr_to_ctcb_ptr ` set tcbs; tcb_at' tcb' s; \<forall>t\<in>set tcbs. tcb_at' t s; tcb' \<notin> set tcbs; distinct tcbs; mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcba; tcb_queue_relation getNext getPrev mp tcbs (tcb_ptr_to_ctcb_ptr tcb') (getNext tcba); qprev = getPrev tcba; tcbs \<noteq> []\<rbrakk> \<Longrightarrow> (tcb' = last tcbs \<longrightarrow> getPrev (the (mp (tcb_ptr_to_ctcb_ptr (last tcbs)))) = getPrev tcba \<and> tcb_queue_relation getNext getPrev (\<lambda>a. if a = tcb_ptr_to_ctcb_ptr (last tcbs) then Some (getNext_update (\<lambda>_. qend') (the (mp (tcb_ptr_to_ctcb_ptr (last tcbs))))) else if a = qend' then Some (getNext_update (\<lambda>_. NULL) (getPrev_update (\<lambda>_. tcb_ptr_to_ctcb_ptr (last tcbs)) tcb)) else mp a) (tcbs @ [ctcb_ptr_to_tcb_ptr qend']) (tcb_ptr_to_ctcb_ptr (last tcbs)) qend') \<and> (tcb' \<noteq> last tcbs \<longrightarrow> tcb_queue_relation getNext getPrev (\<lambda>a. if a = tcb_ptr_to_ctcb_ptr (last tcbs) then Some (getNext_update (\<lambda>_. qend') (the (mp (tcb_ptr_to_ctcb_ptr (last tcbs))))) else if a = qend' then Some (getNext_update (\<lambda>_. NULL) (getPrev_update (\<lambda>_. tcb_ptr_to_ctcb_ptr (last tcbs)) tcb)) else mp a) (tcbs @ [ctcb_ptr_to_tcb_ptr qend']) (tcb_ptr_to_ctcb_ptr tcb') (getNext tcba)) proof (prove)
goal (1 subgoal):
 1. \<And>tcba. \<lbrakk>tcb_ptr_to_ctcb_ptr (last tcbs) \<noteq> NULL; tcb_ptr_to_ctcb_ptr tcb' \<noteq> NULL; qend = tcb_ptr_to_ctcb_ptr (last tcbs); mp qend' = Some tcb; qend' \<noteq> NULL; qhead = tcb_ptr_to_ctcb_ptr tcb'; qend' \<noteq> tcb_ptr_to_ctcb_ptr tcb'; qend' \<notin> tcb_ptr_to_ctcb_ptr ` set tcbs; tcb_at' tcb' s; \<forall>t\<in>set tcbs. tcb_at' t s; tcb' \<notin> set tcbs; distinct tcbs; mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcba; tcb_queue_relation getNext getPrev mp tcbs (tcb_ptr_to_ctcb_ptr tcb') (getNext tcba); qprev = getPrev tcba; tcbs \<noteq> []\<rbrakk> \<Longrightarrow> tcb' \<noteq> last tcbs \<longrightarrow> tcb_queue_relation getNext getPrev (\<lambda>a. if a = tcb_ptr_to_ctcb_ptr (last tcbs) then Some (getNext_update (\<lambda>_. qend') (the (mp (tcb_ptr_to_ctcb_ptr (last tcbs))))) else if a = qend' then Some (getNext_update (\<lambda>_. NULL) (getPrev_update (\<lambda>_. tcb_ptr_to_ctcb_ptr (last tcbs)) tcb)) else mp a) (tcbs @ [ctcb_ptr_to_tcb_ptr qend']) (tcb_ptr_to_ctcb_ptr tcb') (getNext tcba) proof (prove)
goal (1 subgoal):
 1. \<And>tcba. \<lbrakk>tcb_ptr_to_ctcb_ptr (last tcbs) \<noteq> NULL; tcb_ptr_to_ctcb_ptr tcb' \<noteq> NULL; qend = tcb_ptr_to_ctcb_ptr (last tcbs); mp qend' = Some tcb; qend' \<noteq> NULL; qhead = tcb_ptr_to_ctcb_ptr tcb'; qend' \<noteq> tcb_ptr_to_ctcb_ptr tcb'; qend' \<notin> tcb_ptr_to_ctcb_ptr ` set tcbs; tcb_at' tcb' s; \<forall>t\<in>set tcbs. tcb_at' t s; tcb' \<notin> set tcbs; distinct tcbs; mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcba; tcb_queue_relation getNext getPrev mp tcbs (tcb_ptr_to_ctcb_ptr tcb') (getNext tcba); qprev = getPrev tcba; tcbs \<noteq> []; tcb' \<noteq> last tcbs\<rbrakk> \<Longrightarrow> tcb_queue_relation getNext getPrev (\<lambda>a. if a = tcb_ptr_to_ctcb_ptr (last tcbs) then Some (getNext_update (\<lambda>_. qend') (the (mp (tcb_ptr_to_ctcb_ptr (last tcbs))))) else if a = qend' then Some (getNext_update (\<lambda>_. NULL) (getPrev_update (\<lambda>_. tcb_ptr_to_ctcb_ptr (last tcbs)) tcb)) else mp a) (tcbs @ [ctcb_ptr_to_tcb_ptr qend']) (tcb_ptr_to_ctcb_ptr tcb') (getNext tcba) proof (prove)
goal (5 subgoals):
 1. \<And>tcba. \<lbrakk>tcb_ptr_to_ctcb_ptr (last tcbs) \<noteq> NULL; tcb_ptr_to_ctcb_ptr tcb' \<noteq> NULL; qend = tcb_ptr_to_ctcb_ptr (last tcbs); mp qend' = Some tcb; qend' \<noteq> NULL; qhead = tcb_ptr_to_ctcb_ptr tcb'; qend' \<noteq> tcb_ptr_to_ctcb_ptr tcb'; qend' \<notin> tcb_ptr_to_ctcb_ptr ` set tcbs; tcb_at' tcb' s; \<forall>t\<in>set tcbs. tcb_at' t s; tcb' \<notin> set tcbs; distinct tcbs; mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcba; tcb_queue_relation getNext getPrev mp tcbs (tcb_ptr_to_ctcb_ptr tcb') (getNext tcba); qprev = getPrev tcba; tcbs \<noteq> []; tcb' \<noteq> last tcbs\<rbrakk> \<Longrightarrow> tcbs @ [ctcb_ptr_to_tcb_ptr qend'] = ?queue'47 tcba
 2. \<And>tcba. \<lbrakk>tcb_ptr_to_ctcb_ptr (last tcbs) \<noteq> NULL; tcb_ptr_to_ctcb_ptr tcb' \<noteq> NULL; qend = tcb_ptr_to_ctcb_ptr (last tcbs); mp qend' = Some tcb; qend' \<noteq> NULL; qhead = tcb_ptr_to_ctcb_ptr tcb'; qend' \<noteq> tcb_ptr_to_ctcb_ptr tcb'; qend' \<notin> tcb_ptr_to_ctcb_ptr ` set tcbs; tcb_at' tcb' s; \<forall>t\<in>set tcbs. tcb_at' t s; tcb' \<notin> set tcbs; distinct tcbs; mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcba; tcb_queue_relation getNext getPrev mp tcbs (tcb_ptr_to_ctcb_ptr tcb') (getNext tcba); qprev = getPrev tcba; tcbs \<noteq> []; tcb' \<noteq> last tcbs\<rbrakk> \<Longrightarrow> tcb_ptr_to_ctcb_ptr tcb' = ?qprev'47 tcba
 3. \<And>tcba. \<lbrakk>tcb_ptr_to_ctcb_ptr (last tcbs) \<noteq> NULL; tcb_ptr_to_ctcb_ptr tcb' \<noteq> NULL; qend = tcb_ptr_to_ctcb_ptr (last tcbs); mp qend' = Some tcb; qend' \<noteq> NULL; qhead = tcb_ptr_to_ctcb_ptr tcb'; qend' \<noteq> tcb_ptr_to_ctcb_ptr tcb'; qend' \<notin> tcb_ptr_to_ctcb_ptr ` set tcbs; tcb_at' tcb' s; \<forall>t\<in>set tcbs. tcb_at' t s; tcb' \<notin> set tcbs; distinct tcbs; mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcba; tcb_queue_relation getNext getPrev mp tcbs (tcb_ptr_to_ctcb_ptr tcb') (getNext tcba); qprev = getPrev tcba; tcbs \<noteq> []; tcb' \<noteq> last tcbs\<rbrakk> \<Longrightarrow> getNext tcba = ?qhead'47 tcba
 4. \<And>tcba p. \<lbrakk>tcb_ptr_to_ctcb_ptr (last tcbs) \<noteq> NULL; tcb_ptr_to_ctcb_ptr tcb' \<noteq> NULL; qend = tcb_ptr_to_ctcb_ptr (last tcbs); mp qend' = Some tcb; qend' \<noteq> NULL; qhead = tcb_ptr_to_ctcb_ptr tcb'; qend' \<noteq> tcb_ptr_to_ctcb_ptr tcb'; qend' \<notin> tcb_ptr_to_ctcb_ptr ` set tcbs; tcb_at' tcb' s; \<forall>t\<in>set tcbs. tcb_at' t s; tcb' \<notin> set tcbs; distinct tcbs; mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcba; tcb_queue_relation getNext getPrev mp tcbs (tcb_ptr_to_ctcb_ptr tcb') (getNext tcba); qprev = getPrev tcba; tcbs \<noteq> []; tcb' \<noteq> last tcbs; p \<in> tcb_ptr_to_ctcb_ptr ` set (?queue'47 tcba)\<rbrakk> \<Longrightarrow> (if p = tcb_ptr_to_ctcb_ptr (last tcbs) then Some (getNext_update (\<lambda>_. qend') (the (mp (tcb_ptr_to_ctcb_ptr (last tcbs))))) else if p = qend' then Some (getNext_update (\<lambda>_. NULL) (getPrev_update (\<lambda>_. tcb_ptr_to_ctcb_ptr (last tcbs)) tcb)) else mp p) = ?mp'47 tcba p
 5. \<And>tcba. \<lbrakk>tcb_ptr_to_ctcb_ptr (last tcbs) \<noteq> NULL; tcb_ptr_to_ctcb_ptr tcb' \<noteq> NULL; qend = tcb_ptr_to_ctcb_ptr (last tcbs); mp qend' = Some tcb; qend' \<noteq> NULL; qhead = tcb_ptr_to_ctcb_ptr tcb'; qend' \<noteq> tcb_ptr_to_ctcb_ptr tcb'; qend' \<notin> tcb_ptr_to_ctcb_ptr ` set tcbs; tcb_at' tcb' s; \<forall>t\<in>set tcbs. tcb_at' t s; tcb' \<notin> set tcbs; distinct tcbs; mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcba; tcb_queue_relation getNext getPrev mp tcbs (tcb_ptr_to_ctcb_ptr tcb') (getNext tcba); qprev = getPrev tcba; tcbs \<noteq> []; tcb' \<noteq> last tcbs\<rbrakk> \<Longrightarrow> tcb_queue_relation getNext getPrev (?mp'47 tcba) (?queue'47 tcba) (?qprev'47 tcba) (?qhead'47 tcba) proof (prove)
goal (5 subgoals):
 1. \<And>tcba. \<lbrakk>tcb_ptr_to_ctcb_ptr (last tcbs) \<noteq> NULL; tcb_ptr_to_ctcb_ptr tcb' \<noteq> NULL; qend = tcb_ptr_to_ctcb_ptr (last tcbs); mp qend' = Some tcb; qend' \<noteq> NULL; qhead = tcb_ptr_to_ctcb_ptr tcb'; qend' \<noteq> tcb_ptr_to_ctcb_ptr tcb'; qend' \<notin> tcb_ptr_to_ctcb_ptr ` set tcbs; tcb_at' tcb' s; \<forall>t\<in>set tcbs. tcb_at' t s; tcb' \<notin> set tcbs; distinct tcbs; mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcba; tcb_queue_relation getNext getPrev mp tcbs (tcb_ptr_to_ctcb_ptr tcb') (getNext tcba); qprev = getPrev tcba; tcbs \<noteq> []; tcb' \<noteq> last tcbs\<rbrakk> \<Longrightarrow> tcb_queue_relation getNext getPrev (?mp'47 tcba) (?queue'47 tcba) (?qprev'47 tcba) (?qhead'47 tcba)
 2. \<And>tcba. \<lbrakk>tcb_ptr_to_ctcb_ptr (last tcbs) \<noteq> NULL; tcb_ptr_to_ctcb_ptr tcb' \<noteq> NULL; qend = tcb_ptr_to_ctcb_ptr (last tcbs); mp qend' = Some tcb; qend' \<noteq> NULL; qhead = tcb_ptr_to_ctcb_ptr tcb'; qend' \<noteq> tcb_ptr_to_ctcb_ptr tcb'; qend' \<notin> tcb_ptr_to_ctcb_ptr ` set tcbs; tcb_at' tcb' s; \<forall>t\<in>set tcbs. tcb_at' t s; tcb' \<notin> set tcbs; distinct tcbs; mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcba; tcb_queue_relation getNext getPrev mp tcbs (tcb_ptr_to_ctcb_ptr tcb') (getNext tcba); qprev = getPrev tcba; tcbs \<noteq> []; tcb' \<noteq> last tcbs\<rbrakk> \<Longrightarrow> tcbs @ [ctcb_ptr_to_tcb_ptr qend'] = ?queue'47 tcba
 3. \<And>tcba. \<lbrakk>tcb_ptr_to_ctcb_ptr (last tcbs) \<noteq> NULL; tcb_ptr_to_ctcb_ptr tcb' \<noteq> NULL; qend = tcb_ptr_to_ctcb_ptr (last tcbs); mp qend' = Some tcb; qend' \<noteq> NULL; qhead = tcb_ptr_to_ctcb_ptr tcb'; qend' \<noteq> tcb_ptr_to_ctcb_ptr tcb'; qend' \<notin> tcb_ptr_to_ctcb_ptr ` set tcbs; tcb_at' tcb' s; \<forall>t\<in>set tcbs. tcb_at' t s; tcb' \<notin> set tcbs; distinct tcbs; mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcba; tcb_queue_relation getNext getPrev mp tcbs (tcb_ptr_to_ctcb_ptr tcb') (getNext tcba); qprev = getPrev tcba; tcbs \<noteq> []; tcb' \<noteq> last tcbs\<rbrakk> \<Longrightarrow> tcb_ptr_to_ctcb_ptr tcb' = ?qprev'47 tcba
 4. \<And>tcba. \<lbrakk>tcb_ptr_to_ctcb_ptr (last tcbs) \<noteq> NULL; tcb_ptr_to_ctcb_ptr tcb' \<noteq> NULL; qend = tcb_ptr_to_ctcb_ptr (last tcbs); mp qend' = Some tcb; qend' \<noteq> NULL; qhead = tcb_ptr_to_ctcb_ptr tcb'; qend' \<noteq> tcb_ptr_to_ctcb_ptr tcb'; qend' \<notin> tcb_ptr_to_ctcb_ptr ` set tcbs; tcb_at' tcb' s; \<forall>t\<in>set tcbs. tcb_at' t s; tcb' \<notin> set tcbs; distinct tcbs; mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcba; tcb_queue_relation getNext getPrev mp tcbs (tcb_ptr_to_ctcb_ptr tcb') (getNext tcba); qprev = getPrev tcba; tcbs \<noteq> []; tcb' \<noteq> last tcbs\<rbrakk> \<Longrightarrow> getNext tcba = ?qhead'47 tcba
 5. \<And>tcba p. \<lbrakk>tcb_ptr_to_ctcb_ptr (last tcbs) \<noteq> NULL; tcb_ptr_to_ctcb_ptr tcb' \<noteq> NULL; qend = tcb_ptr_to_ctcb_ptr (last tcbs); mp qend' = Some tcb; qend' \<noteq> NULL; qhead = tcb_ptr_to_ctcb_ptr tcb'; qend' \<noteq> tcb_ptr_to_ctcb_ptr tcb'; qend' \<notin> tcb_ptr_to_ctcb_ptr ` set tcbs; tcb_at' tcb' s; \<forall>t\<in>set tcbs. tcb_at' t s; tcb' \<notin> set tcbs; distinct tcbs; mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcba; tcb_queue_relation getNext getPrev mp tcbs (tcb_ptr_to_ctcb_ptr tcb') (getNext tcba); qprev = getPrev tcba; tcbs \<noteq> []; tcb' \<noteq> last tcbs; p \<in> tcb_ptr_to_ctcb_ptr ` set (?queue'47 tcba)\<rbrakk> \<Longrightarrow> (if p = tcb_ptr_to_ctcb_ptr (last tcbs) then Some (getNext_update (\<lambda>_. qend') (the (mp (tcb_ptr_to_ctcb_ptr (last tcbs))))) else if p = qend' then Some (getNext_update (\<lambda>_. NULL) (getPrev_update (\<lambda>_. tcb_ptr_to_ctcb_ptr (last tcbs)) tcb)) else mp p) = ?mp'47 tcba p proof (prove)
goal (1 subgoal):
 1. \<And>tcba. \<lbrakk>tcb_ptr_to_ctcb_ptr (last tcbs) \<noteq> NULL; tcb_ptr_to_ctcb_ptr tcb' \<noteq> NULL; qend = tcb_ptr_to_ctcb_ptr (last tcbs); mp qend' = Some tcb; qend' \<noteq> NULL; qhead = tcb_ptr_to_ctcb_ptr tcb'; qend' \<noteq> tcb_ptr_to_ctcb_ptr tcb'; qend' \<notin> tcb_ptr_to_ctcb_ptr ` set tcbs; tcb_at' tcb' s; \<forall>t\<in>set tcbs. tcb_at' t s; tcb' \<notin> set tcbs; distinct tcbs; mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcba; tcb_queue_relation getNext getPrev mp tcbs (tcb_ptr_to_ctcb_ptr tcb') (getNext tcba); qprev = getPrev tcba; tcbs \<noteq> []; tcb' \<noteq> last tcbs\<rbrakk> \<Longrightarrow> getNext tcba = (if getNext tcba = NULL then qend' else getNext tcba) proof (prove)
goal:
No subgoals! proof (state)
this:
tcb_queue_relation getNext getPrev (upd_unless_null qend (getNext_update (\<lambda>_. qend') (the (mp qend))) (mp(qend' \<mapsto> getNext_update (\<lambda>_. NULL) (getPrev_update (\<lambda>_. qend) tcb)))) ((tcb' # tcbs) @ [ctcb_ptr_to_tcb_ptr qend']) qprev (if qhead = NULL then qend' else qhead)

goal:
No subgoals!