theory IpcCancel_C

lemma tcb_queue_relation_update_head:
  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 NULL qhead"
  and     qh': "qhead' \<notin> tcb_ptr_to_ctcb_ptr ` set queue"
  and  cs_tcb: "mp qhead' = Some tcb"
  and valid_ep: "\<forall>t\<in>set queue. tcb_at' t s" "distinct queue"
  and     qhN: "qhead' \<noteq> 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 qhead (getPrev_update (\<lambda>_. qhead') (the (mp qhead)))
                       (mp(qhead' := Some (getPrev_update (\<lambda>_. NULL) (getNext_update (\<lambda>_. qhead)  tcb)))))
                 (ctcb_ptr_to_tcb_ptr qhead' # queue) NULL qhead'" using qr qh' cs_tcb valid_ep qhN apply (subgoal_tac "qhead \<noteq> qhead'") apply (clarsimp simp: pnu upd_unless_null_def fg_consD1 [OF fgN] fg_consD1 [OF fgP] pnu npu) apply (cases queue) apply simp apply (frule (2) tcb_queue_relation_next_not_NULL) apply simp apply (clarsimp simp: fg_consD1 [OF fgN] fg_consD1 [OF fgP] pnu npu) apply (subst tcb_queue_relation_cong [OF refl refl refl, where mp' = mp]) apply (clarsimp simp: inj_eq) apply (intro impI conjI) apply (frule_tac x = x in imageI [where f = tcb_ptr_to_ctcb_ptr]) apply simp apply simp apply simp apply clarsimp apply (cases queue) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_queue_relation getNext getPrev (upd_unless_null qhead (getPrev_update (\<lambda>_. qhead') (the (mp qhead))) (mp(qhead' \<mapsto> getPrev_update (\<lambda>_. NULL) (getNext_update (\<lambda>_. qhead) tcb)))) (ctcb_ptr_to_tcb_ptr qhead' # queue) NULL qhead' proof (prove)
using this:
tcb_queue_relation getNext getPrev mp queue NULL qhead
qhead' \<notin> tcb_ptr_to_ctcb_ptr ` set queue
mp qhead' = Some tcb
\<forall>t\<in>set queue. tcb_at' t s
distinct queue
qhead' \<noteq> NULL

goal (1 subgoal):
 1. tcb_queue_relation getNext getPrev (upd_unless_null qhead (getPrev_update (\<lambda>_. qhead') (the (mp qhead))) (mp(qhead' \<mapsto> getPrev_update (\<lambda>_. NULL) (getNext_update (\<lambda>_. qhead) tcb)))) (ctcb_ptr_to_tcb_ptr qhead' # queue) NULL qhead' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>tcb_queue_relation getNext getPrev mp queue NULL qhead; qhead' \<notin> tcb_ptr_to_ctcb_ptr ` set queue; mp qhead' = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; qhead' \<noteq> NULL; qhead \<noteq> qhead'\<rbrakk> \<Longrightarrow> tcb_queue_relation getNext getPrev (upd_unless_null qhead (getPrev_update (\<lambda>_. qhead') (the (mp qhead))) (mp(qhead' \<mapsto> getPrev_update (\<lambda>_. NULL) (getNext_update (\<lambda>_. qhead) tcb)))) (ctcb_ptr_to_tcb_ptr qhead' # queue) NULL qhead'
 2. \<lbrakk>tcb_queue_relation getNext getPrev mp queue NULL qhead; qhead' \<notin> tcb_ptr_to_ctcb_ptr ` set queue; mp qhead' = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; qhead' \<noteq> NULL\<rbrakk> \<Longrightarrow> qhead \<noteq> qhead' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>tcb_queue_relation getNext getPrev mp queue NULL qhead; qhead' \<notin> tcb_ptr_to_ctcb_ptr ` set queue; mp qhead' = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; qhead' \<noteq> NULL; qhead \<noteq> qhead'\<rbrakk> \<Longrightarrow> (qhead = NULL \<longrightarrow> tcb_queue_relation getNext getPrev (mp(qhead' \<mapsto> getPrev_update (\<lambda>_. NULL) (getNext_update (\<lambda>_. NULL) tcb))) queue qhead' NULL) \<and> (qhead \<noteq> NULL \<longrightarrow> tcb_queue_relation getNext getPrev (mp(qhead' \<mapsto> getPrev_update (\<lambda>_. NULL) (getNext_update (\<lambda>_. qhead) tcb), qhead \<mapsto> getPrev_update (\<lambda>_. qhead') (the (mp qhead)))) queue qhead' qhead)
 2. \<lbrakk>tcb_queue_relation getNext getPrev mp queue NULL qhead; qhead' \<notin> tcb_ptr_to_ctcb_ptr ` set queue; mp qhead' = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; qhead' \<noteq> NULL\<rbrakk> \<Longrightarrow> qhead \<noteq> qhead' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>tcb_queue_relation getNext getPrev mp queue NULL qhead; qhead' \<notin> tcb_ptr_to_ctcb_ptr ` set queue; mp qhead' = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; qhead' \<noteq> NULL; qhead \<noteq> qhead'; queue = []\<rbrakk> \<Longrightarrow> (qhead = NULL \<longrightarrow> tcb_queue_relation getNext getPrev (mp(qhead' \<mapsto> getPrev_update (\<lambda>_. NULL) (getNext_update (\<lambda>_. NULL) tcb))) queue qhead' NULL) \<and> (qhead \<noteq> NULL \<longrightarrow> tcb_queue_relation getNext getPrev (mp(qhead' \<mapsto> getPrev_update (\<lambda>_. NULL) (getNext_update (\<lambda>_. qhead) tcb), qhead \<mapsto> getPrev_update (\<lambda>_. qhead') (the (mp qhead)))) queue qhead' qhead)
 2. \<And>a list. \<lbrakk>tcb_queue_relation getNext getPrev mp queue NULL qhead; qhead' \<notin> tcb_ptr_to_ctcb_ptr ` set queue; mp qhead' = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; qhead' \<noteq> NULL; qhead \<noteq> qhead'; queue = a # list\<rbrakk> \<Longrightarrow> (qhead = NULL \<longrightarrow> tcb_queue_relation getNext getPrev (mp(qhead' \<mapsto> getPrev_update (\<lambda>_. NULL) (getNext_update (\<lambda>_. NULL) tcb))) queue qhead' NULL) \<and> (qhead \<noteq> NULL \<longrightarrow> tcb_queue_relation getNext getPrev (mp(qhead' \<mapsto> getPrev_update (\<lambda>_. NULL) (getNext_update (\<lambda>_. qhead) tcb), qhead \<mapsto> getPrev_update (\<lambda>_. qhead') (the (mp qhead)))) queue qhead' qhead)
 3. \<lbrakk>tcb_queue_relation getNext getPrev mp queue NULL qhead; qhead' \<notin> tcb_ptr_to_ctcb_ptr ` set queue; mp qhead' = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; qhead' \<noteq> NULL\<rbrakk> \<Longrightarrow> qhead \<noteq> qhead' proof (prove)
goal (2 subgoals):
 1. \<And>a list. \<lbrakk>tcb_queue_relation getNext getPrev mp queue NULL qhead; qhead' \<notin> tcb_ptr_to_ctcb_ptr ` set queue; mp qhead' = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; qhead' \<noteq> NULL; qhead \<noteq> qhead'; queue = a # list\<rbrakk> \<Longrightarrow> (qhead = NULL \<longrightarrow> tcb_queue_relation getNext getPrev (mp(qhead' \<mapsto> getPrev_update (\<lambda>_. NULL) (getNext_update (\<lambda>_. NULL) tcb))) queue qhead' NULL) \<and> (qhead \<noteq> NULL \<longrightarrow> tcb_queue_relation getNext getPrev (mp(qhead' \<mapsto> getPrev_update (\<lambda>_. NULL) (getNext_update (\<lambda>_. qhead) tcb), qhead \<mapsto> getPrev_update (\<lambda>_. qhead') (the (mp qhead)))) queue qhead' qhead)
 2. \<lbrakk>tcb_queue_relation getNext getPrev mp queue NULL qhead; qhead' \<notin> tcb_ptr_to_ctcb_ptr ` set queue; mp qhead' = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; qhead' \<noteq> NULL\<rbrakk> \<Longrightarrow> qhead \<noteq> qhead' proof (prove)
goal (3 subgoals):
 1. \<And>a list. \<lbrakk>tcb_queue_relation getNext getPrev mp queue NULL qhead; qhead' \<notin> tcb_ptr_to_ctcb_ptr ` set queue; mp qhead' = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; qhead' \<noteq> NULL; qhead \<noteq> qhead'; queue = a # list\<rbrakk> \<Longrightarrow> queue \<noteq> []
 2. \<And>a list. \<lbrakk>tcb_queue_relation getNext getPrev mp queue NULL qhead; qhead' \<notin> tcb_ptr_to_ctcb_ptr ` set queue; mp qhead' = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; qhead' \<noteq> NULL; qhead \<noteq> qhead'; queue = a # list; qhead \<noteq> NULL\<rbrakk> \<Longrightarrow> (qhead = NULL \<longrightarrow> tcb_queue_relation getNext getPrev (mp(qhead' \<mapsto> getPrev_update (\<lambda>_. NULL) (getNext_update (\<lambda>_. NULL) tcb))) queue qhead' NULL) \<and> (qhead \<noteq> NULL \<longrightarrow> tcb_queue_relation getNext getPrev (mp(qhead' \<mapsto> getPrev_update (\<lambda>_. NULL) (getNext_update (\<lambda>_. qhead) tcb), qhead \<mapsto> getPrev_update (\<lambda>_. qhead') (the (mp qhead)))) queue qhead' qhead)
 3. \<lbrakk>tcb_queue_relation getNext getPrev mp queue NULL qhead; qhead' \<notin> tcb_ptr_to_ctcb_ptr ` set queue; mp qhead' = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; qhead' \<noteq> NULL\<rbrakk> \<Longrightarrow> qhead \<noteq> qhead' proof (prove)
goal (2 subgoals):
 1. \<And>a list. \<lbrakk>tcb_queue_relation getNext getPrev mp queue NULL qhead; qhead' \<notin> tcb_ptr_to_ctcb_ptr ` set queue; mp qhead' = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; qhead' \<noteq> NULL; qhead \<noteq> qhead'; queue = a # list; qhead \<noteq> NULL\<rbrakk> \<Longrightarrow> (qhead = NULL \<longrightarrow> tcb_queue_relation getNext getPrev (mp(qhead' \<mapsto> getPrev_update (\<lambda>_. NULL) (getNext_update (\<lambda>_. NULL) tcb))) queue qhead' NULL) \<and> (qhead \<noteq> NULL \<longrightarrow> tcb_queue_relation getNext getPrev (mp(qhead' \<mapsto> getPrev_update (\<lambda>_. NULL) (getNext_update (\<lambda>_. qhead) tcb), qhead \<mapsto> getPrev_update (\<lambda>_. qhead') (the (mp qhead)))) queue qhead' qhead)
 2. \<lbrakk>tcb_queue_relation getNext getPrev mp queue NULL qhead; qhead' \<notin> tcb_ptr_to_ctcb_ptr ` set queue; mp qhead' = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; qhead' \<noteq> NULL\<rbrakk> \<Longrightarrow> qhead \<noteq> qhead' proof (prove)
goal (2 subgoals):
 1. \<And>a list tcba. \<lbrakk>qhead' \<notin> tcb_ptr_to_ctcb_ptr ` set list; mp qhead' = Some tcb; qhead' \<noteq> NULL; tcb_ptr_to_ctcb_ptr a \<noteq> qhead'; queue = a # list; tcb_ptr_to_ctcb_ptr a \<noteq> NULL; qhead = tcb_ptr_to_ctcb_ptr a; tcb_at' a s; \<forall>t\<in>set list. tcb_at' t s; a \<notin> set list; distinct list; mp (tcb_ptr_to_ctcb_ptr a) = Some tcba; getPrev tcba = NULL; tcb_queue_relation getNext getPrev mp list (tcb_ptr_to_ctcb_ptr a) (getNext tcba)\<rbrakk> \<Longrightarrow> tcb_queue_relation getNext getPrev (mp(qhead' \<mapsto> getPrev_update (\<lambda>_. NULL) (getNext_update (\<lambda>_. tcb_ptr_to_ctcb_ptr a) tcb), tcb_ptr_to_ctcb_ptr a \<mapsto> getPrev_update (\<lambda>_. qhead') tcba)) list (tcb_ptr_to_ctcb_ptr a) (getNext tcba)
 2. \<lbrakk>tcb_queue_relation getNext getPrev mp queue NULL qhead; qhead' \<notin> tcb_ptr_to_ctcb_ptr ` set queue; mp qhead' = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; qhead' \<noteq> NULL\<rbrakk> \<Longrightarrow> qhead \<noteq> qhead' proof (prove)
goal (3 subgoals):
 1. \<And>a list tcba p. \<lbrakk>qhead' \<notin> tcb_ptr_to_ctcb_ptr ` set list; mp qhead' = Some tcb; qhead' \<noteq> NULL; tcb_ptr_to_ctcb_ptr a \<noteq> qhead'; queue = a # list; tcb_ptr_to_ctcb_ptr a \<noteq> NULL; qhead = tcb_ptr_to_ctcb_ptr a; tcb_at' a s; \<forall>t\<in>set list. tcb_at' t s; a \<notin> set list; distinct list; mp (tcb_ptr_to_ctcb_ptr a) = Some tcba; getPrev tcba = NULL; tcb_queue_relation getNext getPrev mp list (tcb_ptr_to_ctcb_ptr a) (getNext tcba); p \<in> tcb_ptr_to_ctcb_ptr ` set list\<rbrakk> \<Longrightarrow> (mp(qhead' \<mapsto> getPrev_update (\<lambda>_. NULL) (getNext_update (\<lambda>_. tcb_ptr_to_ctcb_ptr a) tcb), tcb_ptr_to_ctcb_ptr a \<mapsto> getPrev_update (\<lambda>_. qhead') tcba)) p = mp p
 2. \<And>a list tcba. \<lbrakk>qhead' \<notin> tcb_ptr_to_ctcb_ptr ` set list; mp qhead' = Some tcb; qhead' \<noteq> NULL; tcb_ptr_to_ctcb_ptr a \<noteq> qhead'; queue = a # list; tcb_ptr_to_ctcb_ptr a \<noteq> NULL; qhead = tcb_ptr_to_ctcb_ptr a; tcb_at' a s; \<forall>t\<in>set list. tcb_at' t s; a \<notin> set list; distinct list; mp (tcb_ptr_to_ctcb_ptr a) = Some tcba; getPrev tcba = NULL; tcb_queue_relation getNext getPrev mp list (tcb_ptr_to_ctcb_ptr a) (getNext tcba)\<rbrakk> \<Longrightarrow> tcb_queue_relation getNext getPrev mp list (tcb_ptr_to_ctcb_ptr a) (getNext tcba)
 3. \<lbrakk>tcb_queue_relation getNext getPrev mp queue NULL qhead; qhead' \<notin> tcb_ptr_to_ctcb_ptr ` set queue; mp qhead' = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; qhead' \<noteq> NULL\<rbrakk> \<Longrightarrow> qhead \<noteq> qhead' proof (prove)
goal (3 subgoals):
 1. \<And>a list tcba x. \<lbrakk>qhead' \<notin> tcb_ptr_to_ctcb_ptr ` set list; mp qhead' = Some tcb; qhead' \<noteq> NULL; tcb_ptr_to_ctcb_ptr a \<noteq> qhead'; queue = a # list; tcb_ptr_to_ctcb_ptr a \<noteq> NULL; qhead = tcb_ptr_to_ctcb_ptr a; tcb_at' a s; \<forall>t\<in>set list. tcb_at' t s; a \<notin> set list; distinct list; mp (tcb_ptr_to_ctcb_ptr a) = Some tcba; getPrev tcba = NULL; tcb_queue_relation getNext getPrev mp list (tcb_ptr_to_ctcb_ptr a) (getNext tcba); x \<in> set list\<rbrakk> \<Longrightarrow> (tcb_ptr_to_ctcb_ptr x = qhead' \<longrightarrow> getPrev_update (\<lambda>_. NULL) (getNext_update (\<lambda>_. tcb_ptr_to_ctcb_ptr a) tcb) = tcb) \<and> (tcb_ptr_to_ctcb_ptr x \<noteq> qhead' \<longrightarrow> x = a \<longrightarrow> getPrev_update (\<lambda>_. qhead') tcba = tcba)
 2. \<And>a list tcba. \<lbrakk>qhead' \<notin> tcb_ptr_to_ctcb_ptr ` set list; mp qhead' = Some tcb; qhead' \<noteq> NULL; tcb_ptr_to_ctcb_ptr a \<noteq> qhead'; queue = a # list; tcb_ptr_to_ctcb_ptr a \<noteq> NULL; qhead = tcb_ptr_to_ctcb_ptr a; tcb_at' a s; \<forall>t\<in>set list. tcb_at' t s; a \<notin> set list; distinct list; mp (tcb_ptr_to_ctcb_ptr a) = Some tcba; getPrev tcba = NULL; tcb_queue_relation getNext getPrev mp list (tcb_ptr_to_ctcb_ptr a) (getNext tcba)\<rbrakk> \<Longrightarrow> tcb_queue_relation getNext getPrev mp list (tcb_ptr_to_ctcb_ptr a) (getNext tcba)
 3. \<lbrakk>tcb_queue_relation getNext getPrev mp queue NULL qhead; qhead' \<notin> tcb_ptr_to_ctcb_ptr ` set queue; mp qhead' = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; qhead' \<noteq> NULL\<rbrakk> \<Longrightarrow> qhead \<noteq> qhead' proof (prove)
goal (4 subgoals):
 1. \<And>a list tcba x. \<lbrakk>qhead' \<notin> tcb_ptr_to_ctcb_ptr ` set list; mp qhead' = Some tcb; qhead' \<noteq> NULL; tcb_ptr_to_ctcb_ptr a \<noteq> qhead'; queue = a # list; tcb_ptr_to_ctcb_ptr a \<noteq> NULL; qhead = tcb_ptr_to_ctcb_ptr a; tcb_at' a s; \<forall>t\<in>set list. tcb_at' t s; a \<notin> set list; distinct list; mp (tcb_ptr_to_ctcb_ptr a) = Some tcba; getPrev tcba = NULL; tcb_queue_relation getNext getPrev mp list (tcb_ptr_to_ctcb_ptr a) (getNext tcba); x \<in> set list; tcb_ptr_to_ctcb_ptr x = qhead'\<rbrakk> \<Longrightarrow> getPrev_update (\<lambda>_. NULL) (getNext_update (\<lambda>_. tcb_ptr_to_ctcb_ptr a) tcb) = tcb
 2. \<And>a list tcba x. \<lbrakk>qhead' \<notin> tcb_ptr_to_ctcb_ptr ` set list; mp qhead' = Some tcb; qhead' \<noteq> NULL; tcb_ptr_to_ctcb_ptr a \<noteq> qhead'; queue = a # list; tcb_ptr_to_ctcb_ptr a \<noteq> NULL; qhead = tcb_ptr_to_ctcb_ptr a; tcb_at' a s; \<forall>t\<in>set list. tcb_at' t s; a \<notin> set list; distinct list; mp (tcb_ptr_to_ctcb_ptr a) = Some tcba; getPrev tcba = NULL; tcb_queue_relation getNext getPrev mp list (tcb_ptr_to_ctcb_ptr a) (getNext tcba); x \<in> set list; tcb_ptr_to_ctcb_ptr x \<noteq> qhead'; x = a\<rbrakk> \<Longrightarrow> getPrev_update (\<lambda>_. qhead') tcba = tcba
 3. \<And>a list tcba. \<lbrakk>qhead' \<notin> tcb_ptr_to_ctcb_ptr ` set list; mp qhead' = Some tcb; qhead' \<noteq> NULL; tcb_ptr_to_ctcb_ptr a \<noteq> qhead'; queue = a # list; tcb_ptr_to_ctcb_ptr a \<noteq> NULL; qhead = tcb_ptr_to_ctcb_ptr a; tcb_at' a s; \<forall>t\<in>set list. tcb_at' t s; a \<notin> set list; distinct list; mp (tcb_ptr_to_ctcb_ptr a) = Some tcba; getPrev tcba = NULL; tcb_queue_relation getNext getPrev mp list (tcb_ptr_to_ctcb_ptr a) (getNext tcba)\<rbrakk> \<Longrightarrow> tcb_queue_relation getNext getPrev mp list (tcb_ptr_to_ctcb_ptr a) (getNext tcba)
 4. \<lbrakk>tcb_queue_relation getNext getPrev mp queue NULL qhead; qhead' \<notin> tcb_ptr_to_ctcb_ptr ` set queue; mp qhead' = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; qhead' \<noteq> NULL\<rbrakk> \<Longrightarrow> qhead \<noteq> qhead' proof (prove)
goal (4 subgoals):
 1. \<And>a list tcba x. \<lbrakk>qhead' \<notin> tcb_ptr_to_ctcb_ptr ` set list; mp qhead' = Some tcb; qhead' \<noteq> NULL; tcb_ptr_to_ctcb_ptr a \<noteq> qhead'; queue = a # list; tcb_ptr_to_ctcb_ptr a \<noteq> NULL; qhead = tcb_ptr_to_ctcb_ptr a; tcb_at' a s; \<forall>t\<in>set list. tcb_at' t s; a \<notin> set list; distinct list; mp (tcb_ptr_to_ctcb_ptr a) = Some tcba; getPrev tcba = NULL; tcb_queue_relation getNext getPrev mp list (tcb_ptr_to_ctcb_ptr a) (getNext tcba); x \<in> set list; tcb_ptr_to_ctcb_ptr x = qhead'; tcb_ptr_to_ctcb_ptr x \<in> tcb_ptr_to_ctcb_ptr ` set list\<rbrakk> \<Longrightarrow> getPrev_update (\<lambda>_. NULL) (getNext_update (\<lambda>_. tcb_ptr_to_ctcb_ptr a) tcb) = tcb
 2. \<And>a list tcba x. \<lbrakk>qhead' \<notin> tcb_ptr_to_ctcb_ptr ` set list; mp qhead' = Some tcb; qhead' \<noteq> NULL; tcb_ptr_to_ctcb_ptr a \<noteq> qhead'; queue = a # list; tcb_ptr_to_ctcb_ptr a \<noteq> NULL; qhead = tcb_ptr_to_ctcb_ptr a; tcb_at' a s; \<forall>t\<in>set list. tcb_at' t s; a \<notin> set list; distinct list; mp (tcb_ptr_to_ctcb_ptr a) = Some tcba; getPrev tcba = NULL; tcb_queue_relation getNext getPrev mp list (tcb_ptr_to_ctcb_ptr a) (getNext tcba); x \<in> set list; tcb_ptr_to_ctcb_ptr x \<noteq> qhead'; x = a\<rbrakk> \<Longrightarrow> getPrev_update (\<lambda>_. qhead') tcba = tcba
 3. \<And>a list tcba. \<lbrakk>qhead' \<notin> tcb_ptr_to_ctcb_ptr ` set list; mp qhead' = Some tcb; qhead' \<noteq> NULL; tcb_ptr_to_ctcb_ptr a \<noteq> qhead'; queue = a # list; tcb_ptr_to_ctcb_ptr a \<noteq> NULL; qhead = tcb_ptr_to_ctcb_ptr a; tcb_at' a s; \<forall>t\<in>set list. tcb_at' t s; a \<notin> set list; distinct list; mp (tcb_ptr_to_ctcb_ptr a) = Some tcba; getPrev tcba = NULL; tcb_queue_relation getNext getPrev mp list (tcb_ptr_to_ctcb_ptr a) (getNext tcba)\<rbrakk> \<Longrightarrow> tcb_queue_relation getNext getPrev mp list (tcb_ptr_to_ctcb_ptr a) (getNext tcba)
 4. \<lbrakk>tcb_queue_relation getNext getPrev mp queue NULL qhead; qhead' \<notin> tcb_ptr_to_ctcb_ptr ` set queue; mp qhead' = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; qhead' \<noteq> NULL\<rbrakk> \<Longrightarrow> qhead \<noteq> qhead' proof (prove)
goal (3 subgoals):
 1. \<And>a list tcba x. \<lbrakk>qhead' \<notin> tcb_ptr_to_ctcb_ptr ` set list; mp qhead' = Some tcb; qhead' \<noteq> NULL; tcb_ptr_to_ctcb_ptr a \<noteq> qhead'; queue = a # list; tcb_ptr_to_ctcb_ptr a \<noteq> NULL; qhead = tcb_ptr_to_ctcb_ptr a; tcb_at' a s; \<forall>t\<in>set list. tcb_at' t s; a \<notin> set list; distinct list; mp (tcb_ptr_to_ctcb_ptr a) = Some tcba; getPrev tcba = NULL; tcb_queue_relation getNext getPrev mp list (tcb_ptr_to_ctcb_ptr a) (getNext tcba); x \<in> set list; tcb_ptr_to_ctcb_ptr x \<noteq> qhead'; x = a\<rbrakk> \<Longrightarrow> getPrev_update (\<lambda>_. qhead') tcba = tcba
 2. \<And>a list tcba. \<lbrakk>qhead' \<notin> tcb_ptr_to_ctcb_ptr ` set list; mp qhead' = Some tcb; qhead' \<noteq> NULL; tcb_ptr_to_ctcb_ptr a \<noteq> qhead'; queue = a # list; tcb_ptr_to_ctcb_ptr a \<noteq> NULL; qhead = tcb_ptr_to_ctcb_ptr a; tcb_at' a s; \<forall>t\<in>set list. tcb_at' t s; a \<notin> set list; distinct list; mp (tcb_ptr_to_ctcb_ptr a) = Some tcba; getPrev tcba = NULL; tcb_queue_relation getNext getPrev mp list (tcb_ptr_to_ctcb_ptr a) (getNext tcba)\<rbrakk> \<Longrightarrow> tcb_queue_relation getNext getPrev mp list (tcb_ptr_to_ctcb_ptr a) (getNext tcba)
 3. \<lbrakk>tcb_queue_relation getNext getPrev mp queue NULL qhead; qhead' \<notin> tcb_ptr_to_ctcb_ptr ` set queue; mp qhead' = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; qhead' \<noteq> NULL\<rbrakk> \<Longrightarrow> qhead \<noteq> qhead' proof (prove)
goal (2 subgoals):
 1. \<And>a list tcba. \<lbrakk>qhead' \<notin> tcb_ptr_to_ctcb_ptr ` set list; mp qhead' = Some tcb; qhead' \<noteq> NULL; tcb_ptr_to_ctcb_ptr a \<noteq> qhead'; queue = a # list; tcb_ptr_to_ctcb_ptr a \<noteq> NULL; qhead = tcb_ptr_to_ctcb_ptr a; tcb_at' a s; \<forall>t\<in>set list. tcb_at' t s; a \<notin> set list; distinct list; mp (tcb_ptr_to_ctcb_ptr a) = Some tcba; getPrev tcba = NULL; tcb_queue_relation getNext getPrev mp list (tcb_ptr_to_ctcb_ptr a) (getNext tcba)\<rbrakk> \<Longrightarrow> tcb_queue_relation getNext getPrev mp list (tcb_ptr_to_ctcb_ptr a) (getNext tcba)
 2. \<lbrakk>tcb_queue_relation getNext getPrev mp queue NULL qhead; qhead' \<notin> tcb_ptr_to_ctcb_ptr ` set queue; mp qhead' = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; qhead' \<noteq> NULL\<rbrakk> \<Longrightarrow> qhead \<noteq> qhead' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_queue_relation getNext getPrev mp queue NULL qhead; qhead' \<notin> tcb_ptr_to_ctcb_ptr ` set queue; mp qhead' = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; qhead' \<noteq> NULL\<rbrakk> \<Longrightarrow> qhead \<noteq> qhead' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_queue_relation getNext getPrev mp queue NULL qhead'; qhead' \<notin> tcb_ptr_to_ctcb_ptr ` set queue; mp qhead' = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; qhead' \<noteq> NULL; qhead = qhead'\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>tcb_queue_relation getNext getPrev mp queue NULL qhead'; qhead' \<notin> tcb_ptr_to_ctcb_ptr ` set queue; mp qhead' = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; qhead' \<noteq> NULL; qhead = qhead'; queue = []\<rbrakk> \<Longrightarrow> False
 2. \<And>a list. \<lbrakk>tcb_queue_relation getNext getPrev mp queue NULL qhead'; qhead' \<notin> tcb_ptr_to_ctcb_ptr ` set queue; mp qhead' = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; qhead' \<noteq> NULL; qhead = qhead'; queue = a # list\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>tcb_queue_relation getNext getPrev mp queue NULL qhead'; qhead' \<notin> tcb_ptr_to_ctcb_ptr ` set queue; mp qhead' = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; qhead' \<noteq> NULL; qhead = qhead'; queue = a # list\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!