theory IpcCancel_C

lemma tcbSchedAppend_update:
  assumes sr: "sched_queue_relation' mp queue qhead qend"
  and     qh': "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     qhN: "qend' \<noteq> NULL"
  shows
  "sched_queue_relation'
            (upd_unless_null qend (tcbSchedNext_C_update (\<lambda>_. qend') (the (mp qend)))
                (mp(qend' \<mapsto> tcb\<lparr>tcbSchedNext_C := NULL, tcbSchedPrev_C := qend\<rparr>)))
            (queue @ [ctcb_ptr_to_tcb_ptr qend']) (if queue = [] then qend' else qhead) qend'" using sr qh' valid_ep cs_tcb qhN apply - apply (rule rev_cases[where xs=queue]) apply (simp add: tcb_queue_relation'_def upd_unless_null_def) apply (clarsimp simp: tcb_queue_relation'_def upd_unless_null_def tcb_at_not_NULL) apply (drule_tac qend'=qend' and tn_update=tcbSchedNext_C_update
             and tp_update=tcbSchedPrev_C_update and qend="tcb_ptr_to_ctcb_ptr y"
             in tcb_queue_relation_append, simp_all) apply (fastforce simp add: tcb_at_not_NULL) apply (simp add: fun_upd_twist) done

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

goal (1 subgoal):
 1. sched_queue_relation' (upd_unless_null qend (tcbSchedNext_C_update (\<lambda>_. qend') (the (mp qend))) (mp(qend' \<mapsto> tcbSchedPrev_C_update (\<lambda>_. qend) (tcbSchedNext_C_update (\<lambda>_. NULL) tcb)))) (queue @ [ctcb_ptr_to_tcb_ptr qend']) (if queue = [] then qend' else qhead) qend' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sched_queue_relation' mp queue qhead qend; qend' \<notin> tcb_ptr_to_ctcb_ptr ` set queue; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; mp qend' = Some tcb; qend' \<noteq> NULL\<rbrakk> \<Longrightarrow> sched_queue_relation' (upd_unless_null qend (tcbSchedNext_C_update (\<lambda>_. qend') (the (mp qend))) (mp(qend' \<mapsto> tcbSchedPrev_C_update (\<lambda>_. qend) (tcbSchedNext_C_update (\<lambda>_. NULL) tcb)))) (queue @ [ctcb_ptr_to_tcb_ptr qend']) (if queue = [] then qend' else qhead) qend' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sched_queue_relation' mp queue qhead qend; qend' \<notin> tcb_ptr_to_ctcb_ptr ` set queue; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; mp qend' = Some tcb; qend' \<noteq> NULL; queue = []\<rbrakk> \<Longrightarrow> sched_queue_relation' (upd_unless_null qend (tcbSchedNext_C_update (\<lambda>_. qend') (the (mp qend))) (mp(qend' \<mapsto> tcbSchedPrev_C_update (\<lambda>_. qend) (tcbSchedNext_C_update (\<lambda>_. NULL) tcb)))) (queue @ [ctcb_ptr_to_tcb_ptr qend']) (if queue = [] then qend' else qhead) qend'
 2. \<And>ys y. \<lbrakk>sched_queue_relation' mp queue qhead qend; qend' \<notin> tcb_ptr_to_ctcb_ptr ` set queue; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; mp qend' = Some tcb; qend' \<noteq> NULL; queue = ys @ [y]\<rbrakk> \<Longrightarrow> sched_queue_relation' (upd_unless_null qend (tcbSchedNext_C_update (\<lambda>_. qend') (the (mp qend))) (mp(qend' \<mapsto> tcbSchedPrev_C_update (\<lambda>_. qend) (tcbSchedNext_C_update (\<lambda>_. NULL) tcb)))) (queue @ [ctcb_ptr_to_tcb_ptr qend']) (if queue = [] then qend' else qhead) qend' proof (prove)
goal (1 subgoal):
 1. \<And>ys y. \<lbrakk>sched_queue_relation' mp queue qhead qend; qend' \<notin> tcb_ptr_to_ctcb_ptr ` set queue; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; mp qend' = Some tcb; qend' \<noteq> NULL; queue = ys @ [y]\<rbrakk> \<Longrightarrow> sched_queue_relation' (upd_unless_null qend (tcbSchedNext_C_update (\<lambda>_. qend') (the (mp qend))) (mp(qend' \<mapsto> tcbSchedPrev_C_update (\<lambda>_. qend) (tcbSchedNext_C_update (\<lambda>_. NULL) tcb)))) (queue @ [ctcb_ptr_to_tcb_ptr qend']) (if queue = [] then qend' else qhead) qend' proof (prove)
goal (1 subgoal):
 1. \<And>ys y. \<lbrakk>mp qend' = Some tcb; qend' \<noteq> NULL; queue = ys @ [y]; qend = tcb_ptr_to_ctcb_ptr y; sched_queue_relation mp (ys @ [y]) NULL qhead; qend' \<noteq> tcb_ptr_to_ctcb_ptr y; qend' \<notin> tcb_ptr_to_ctcb_ptr ` set ys; tcb_at' y s; \<forall>t\<in>set ys. tcb_at' t s; distinct ys; y \<notin> set ys\<rbrakk> \<Longrightarrow> sched_queue_relation (mp(qend' \<mapsto> tcbSchedPrev_C_update (\<lambda>_. tcb_ptr_to_ctcb_ptr y) (tcbSchedNext_C_update (\<lambda>_. NULL) tcb), tcb_ptr_to_ctcb_ptr y \<mapsto> tcbSchedNext_C_update (\<lambda>_. qend') (the (mp (tcb_ptr_to_ctcb_ptr y))))) (ys @ [y, ctcb_ptr_to_tcb_ptr qend']) NULL qhead proof (prove)
goal (2 subgoals):
 1. \<And>ys y. \<lbrakk>mp qend' = Some tcb; qend' \<noteq> NULL; queue = ys @ [y]; qend = tcb_ptr_to_ctcb_ptr y; qend' \<noteq> tcb_ptr_to_ctcb_ptr y; qend' \<notin> tcb_ptr_to_ctcb_ptr ` set ys; tcb_at' y s; \<forall>t\<in>set ys. tcb_at' t s; distinct ys; y \<notin> set ys\<rbrakk> \<Longrightarrow> tcb_ptr_to_ctcb_ptr y \<noteq> NULL \<and> (\<forall>x\<in>set ys. tcb_ptr_to_ctcb_ptr x \<noteq> NULL)
 2. \<And>ys y. \<lbrakk>mp qend' = Some tcb; qend' \<noteq> NULL; queue = ys @ [y]; qend = tcb_ptr_to_ctcb_ptr y; qend' \<noteq> tcb_ptr_to_ctcb_ptr y; qend' \<notin> tcb_ptr_to_ctcb_ptr ` set ys; tcb_at' y s; \<forall>t\<in>set ys. tcb_at' t s; distinct ys; y \<notin> set ys; sched_queue_relation (mp(tcb_ptr_to_ctcb_ptr y \<mapsto> tcbSchedNext_C_update (\<lambda>_. qend') (the (mp (tcb_ptr_to_ctcb_ptr y))), qend' \<mapsto> tcbSchedPrev_C_update (\<lambda>_. tcb_ptr_to_ctcb_ptr y) (tcbSchedNext_C_update (\<lambda>_. NULL) tcb))) (ys @ [y, ctcb_ptr_to_tcb_ptr qend']) NULL qhead\<rbrakk> \<Longrightarrow> sched_queue_relation (mp(qend' \<mapsto> tcbSchedPrev_C_update (\<lambda>_. tcb_ptr_to_ctcb_ptr y) (tcbSchedNext_C_update (\<lambda>_. NULL) tcb), tcb_ptr_to_ctcb_ptr y \<mapsto> tcbSchedNext_C_update (\<lambda>_. qend') (the (mp (tcb_ptr_to_ctcb_ptr y))))) (ys @ [y, ctcb_ptr_to_tcb_ptr qend']) NULL qhead proof (prove)
goal (1 subgoal):
 1. \<And>ys y. \<lbrakk>mp qend' = Some tcb; qend' \<noteq> NULL; queue = ys @ [y]; qend = tcb_ptr_to_ctcb_ptr y; qend' \<noteq> tcb_ptr_to_ctcb_ptr y; qend' \<notin> tcb_ptr_to_ctcb_ptr ` set ys; tcb_at' y s; \<forall>t\<in>set ys. tcb_at' t s; distinct ys; y \<notin> set ys; sched_queue_relation (mp(tcb_ptr_to_ctcb_ptr y \<mapsto> tcbSchedNext_C_update (\<lambda>_. qend') (the (mp (tcb_ptr_to_ctcb_ptr y))), qend' \<mapsto> tcbSchedPrev_C_update (\<lambda>_. tcb_ptr_to_ctcb_ptr y) (tcbSchedNext_C_update (\<lambda>_. NULL) tcb))) (ys @ [y, ctcb_ptr_to_tcb_ptr qend']) NULL qhead\<rbrakk> \<Longrightarrow> sched_queue_relation (mp(qend' \<mapsto> tcbSchedPrev_C_update (\<lambda>_. tcb_ptr_to_ctcb_ptr y) (tcbSchedNext_C_update (\<lambda>_. NULL) tcb), tcb_ptr_to_ctcb_ptr y \<mapsto> tcbSchedNext_C_update (\<lambda>_. qend') (the (mp (tcb_ptr_to_ctcb_ptr y))))) (ys @ [y, ctcb_ptr_to_tcb_ptr qend']) NULL qhead proof (prove)
goal:
No subgoals!