theory TcbQueue_C

lemma tcbDequeue_update:
  assumes queue_rel: "tcb_queue_relation' tn tp mp queue qhead qend"
  and      in_queue: "tcbp \<in> set queue"
  and    valid_ntfn: "\<forall>t\<in>set queue. tcb_at' t s" "distinct queue"
  and       cs_tcb: "mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb"
  and            f: "\<And>v f g. tn (tn_update f v) = f (tn v) \<and> tp (tp_update g v) = g (tp v)
                           \<and> tn (tp_update f v) = tn v \<and> tp (tn_update g v) = tp v"
  shows "tcb_queue_relation' tn tp
          (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb))))
            (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp))
            (remove1 tcbp queue)
            (if tp tcb = NULL then tn tcb else qhead)
            (if tn tcb = NULL then tp tcb else qend)" proof - have ne: "NULL = (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tp tcb else NULL)" using queue_rel in_queue cs_tcb apply - apply (drule tcb_queue_relation'_queue_rel) apply (clarsimp split: if_split) apply (cases queue) apply simp apply clarsimp done have if2: "(if tp tcb = NULL then tn tcb else qhead) =
             (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tn tcb else qhead)" using tcb_queue_relation'_queue_rel [OF queue_rel] in_queue cs_tcb valid_ntfn apply - apply (cases queue) apply simp apply (frule (3) tcb_queueD) apply (simp add: inj_eq) apply (intro impI) apply simp apply (elim conjE exE) apply (cut_tac x = "queue ! n"
      in bspec [OF tcb_queue_relation_not_NULL [OF  tcb_queue_relation'_queue_rel [OF queue_rel] valid_ntfn(1)]]) apply (rule nth_mem) apply clarsimp apply clarsimp done note null_not_in' = null_not_in [OF tcb_queue_relation'_queue_rel [OF queue_rel] valid_ntfn(1) valid_ntfn(2)] show ?thesis proof (rule tcb_queue_relationI') show "tcb_queue_relation tn tp
     (upd_unless_null (tn tcb)
       (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb))))
       (upd_unless_null (tp tcb)
         (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp))
     (remove1 tcbp queue) NULL
     (if tp tcb = NULL then tn tcb else qhead)" using in_queue valid_ntfn tcb_queue_relation'_queue_rel [OF queue_rel] null_not_in' cs_tcb by (subst ne, subst if2, rule tcbDequeue_update0[rotated -1, OF f]) next have r1: "(remove1 tcbp queue = []) = (tn tcb = NULL \<and> tp tcb = NULL)" using in_queue tcb_queue_relation'_queue_rel [OF queue_rel] cs_tcb valid_ntfn null_not_in' apply - apply (subst tcb_queue_singleton_iff [symmetric], assumption+) apply (fastforce simp: remove1_empty) done have "queue \<noteq> []" using in_queue by clarsimp thus "(if tn tcb = NULL then tp tcb else qend) =
          (if remove1 tcbp queue = [] then NULL else tcb_ptr_to_ctcb_ptr (last (remove1 tcbp queue)))" using queue_rel in_queue cs_tcb valid_ntfn
        tcb_queue_relation_not_NULL [OF tcb_queue_relation'_queue_rel [OF queue_rel] valid_ntfn(1)] apply - apply (erule tcb_queue_relationE') apply (frule (3) tcb_queueD) apply (subst r1) apply simp apply (intro impI conjI) apply (subgoal_tac "tcbp = last queue") apply simp apply (subgoal_tac "(remove1 (last queue) queue) \<noteq> []") apply (clarsimp simp: inj_eq last_conv_nth nth_eq_iff_index_eq length_remove1
           distinct_remove1_take_drop split: if_split_asm) apply arith apply (clarsimp simp: remove1_empty last_conv_nth hd_conv_nth nth_eq_iff_index_eq not_le split: if_split_asm) apply (cases queue) apply simp apply simp apply (fastforce simp: inj_eq split: if_split_asm) apply (clarsimp simp: last_conv_nth distinct_remove1_take_drop nth_eq_iff_index_eq inj_eq split: if_split_asm) apply arith apply (simp add: nth_append min_def nth_eq_iff_index_eq) apply clarsimp apply arith done qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_queue_relation' tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp queue) (if tp tcb = NULL then tn tcb else qhead) (if tn tcb = NULL then tp tcb else qend) proof (state)
goal (1 subgoal):
 1. tcb_queue_relation' tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp queue) (if tp tcb = NULL then tn tcb else qhead) (if tn tcb = NULL then tp tcb else qend) proof (prove)
goal (1 subgoal):
 1. NULL = (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tp tcb else NULL) proof (prove)
using this:
tcb_queue_relation' tn tp mp queue qhead qend
tcbp \<in> set queue
mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb

goal (1 subgoal):
 1. NULL = (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tp tcb else NULL) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_queue_relation' tn tp mp queue qhead qend; tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb\<rbrakk> \<Longrightarrow> NULL = (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tp tcb else NULL) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcb_queue_relation tn tp mp queue NULL qhead\<rbrakk> \<Longrightarrow> NULL = (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tp tcb else NULL) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcb_queue_relation tn tp mp queue NULL (tcb_ptr_to_ctcb_ptr tcbp); qhead = tcb_ptr_to_ctcb_ptr tcbp\<rbrakk> \<Longrightarrow> NULL = tp tcb proof (prove)
goal (2 subgoals):
 1. \<lbrakk>tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcb_queue_relation tn tp mp queue NULL (tcb_ptr_to_ctcb_ptr tcbp); qhead = tcb_ptr_to_ctcb_ptr tcbp; queue = []\<rbrakk> \<Longrightarrow> NULL = tp tcb
 2. \<And>a list. \<lbrakk>tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcb_queue_relation tn tp mp queue NULL (tcb_ptr_to_ctcb_ptr tcbp); qhead = tcb_ptr_to_ctcb_ptr tcbp; queue = a # list\<rbrakk> \<Longrightarrow> NULL = tp tcb proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcb_queue_relation tn tp mp queue NULL (tcb_ptr_to_ctcb_ptr tcbp); qhead = tcb_ptr_to_ctcb_ptr tcbp; queue = a # list\<rbrakk> \<Longrightarrow> NULL = tp tcb proof (prove)
goal:
No subgoals! proof (state)
this:
NULL = (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tp tcb else NULL)

goal (1 subgoal):
 1. tcb_queue_relation' tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp queue) (if tp tcb = NULL then tn tcb else qhead) (if tn tcb = NULL then tp tcb else qend) proof (prove)
goal (1 subgoal):
 1. (if tp tcb = NULL then tn tcb else qhead) = (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tn tcb else qhead) proof (prove)
using this:
tcb_queue_relation tn tp mp queue NULL qhead
tcbp \<in> set queue
mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb
\<forall>t\<in>set queue. tcb_at' t s
distinct queue

goal (1 subgoal):
 1. (if tp tcb = NULL then tn tcb else qhead) = (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tn tcb else qhead) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_queue_relation tn tp mp queue NULL qhead; tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue\<rbrakk> \<Longrightarrow> (if tp tcb = NULL then tn tcb else qhead) = (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tn tcb else qhead) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>tcb_queue_relation tn tp mp queue NULL qhead; tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; queue = []\<rbrakk> \<Longrightarrow> (if tp tcb = NULL then tn tcb else qhead) = (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tn tcb else qhead)
 2. \<And>a list. \<lbrakk>tcb_queue_relation tn tp mp queue NULL qhead; tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; queue = a # list\<rbrakk> \<Longrightarrow> (if tp tcb = NULL then tn tcb else qhead) = (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tn tcb else qhead) proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>tcb_queue_relation tn tp mp queue NULL qhead; tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; queue = a # list\<rbrakk> \<Longrightarrow> (if tp tcb = NULL then tn tcb else qhead) = (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tn tcb else qhead) proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>tcb_queue_relation tn tp mp queue NULL qhead; tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; queue = a # list; (if tcbp = hd queue then tp tcb = NULL else \<exists>n<length queue - 1. tp tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> tcbp = queue ! Suc n) \<and> (if tcbp = last queue then tn tcb = NULL else \<exists>n<length queue - 1. tcbp = queue ! n \<and> tn tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n))\<rbrakk> \<Longrightarrow> (if tp tcb = NULL then tn tcb else qhead) = (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tn tcb else qhead) proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>qhead = tcb_ptr_to_ctcb_ptr a \<and> (\<exists>tcb. mp qhead = Some tcb \<and> tp tcb = NULL \<and> tcb_queue_relation tn tp mp list qhead (tn tcb)); tcbp = a \<or> tcbp \<in> set list; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcb_at' a s \<and> (\<forall>t\<in>set list. tcb_at' t s); a \<notin> set list \<and> distinct list; queue = a # list; (if tcbp = a then tp tcb = NULL else \<exists>n<length queue - 1. tp tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> tcbp = queue ! Suc n) \<and> (if tcbp = (if list = [] then a else last list) then tn tcb = NULL else \<exists>n<length queue - 1. tcbp = queue ! n \<and> tn tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n))\<rbrakk> \<Longrightarrow> tp tcb = NULL \<longrightarrow> tcbp \<noteq> a \<longrightarrow> tn tcb = tcb_ptr_to_ctcb_ptr a proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>qhead = tcb_ptr_to_ctcb_ptr a \<and> (\<exists>tcb. mp qhead = Some tcb \<and> tp tcb = NULL \<and> tcb_queue_relation tn tp mp list qhead (tn tcb)); tcbp = a \<or> tcbp \<in> set list; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcb_at' a s \<and> (\<forall>t\<in>set list. tcb_at' t s); a \<notin> set list \<and> distinct list; queue = a # list; (if tcbp = a then tp tcb = NULL else \<exists>n<length queue - 1. tp tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> tcbp = queue ! Suc n) \<and> (if tcbp = (if list = [] then a else last list) then tn tcb = NULL else \<exists>n<length queue - 1. tcbp = queue ! n \<and> tn tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n)); tp tcb = NULL; tcbp \<noteq> a\<rbrakk> \<Longrightarrow> tn tcb = tcb_ptr_to_ctcb_ptr a proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>qhead = tcb_ptr_to_ctcb_ptr a \<and> (\<exists>tcb. mp qhead = Some tcb \<and> tp tcb = NULL \<and> tcb_queue_relation tn tp mp list qhead (tn tcb)); tcbp \<in> set list; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcb_at' a s \<and> (\<forall>t\<in>set list. tcb_at' t s); a \<notin> set list \<and> distinct list; queue = a # list; (\<exists>n<length list. NULL = tcb_ptr_to_ctcb_ptr ((a # list) ! n) \<and> tcbp = list ! n) \<and> (if tcbp = (if list = [] then a else last list) then tn tcb = NULL else \<exists>n<length queue - 1. tcbp = queue ! n \<and> tn tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n)); tp tcb = NULL; tcbp \<noteq> a\<rbrakk> \<Longrightarrow> tn tcb = tcb_ptr_to_ctcb_ptr a proof (prove)
goal (1 subgoal):
 1. \<And>a list tcba n. \<lbrakk>tcbp \<in> set list; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; queue = a # list; tp tcb = NULL; tcbp \<noteq> a; 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; if tcbp = (if list = [] then a else last list) then tn tcb = NULL else \<exists>n<length queue - 1. tcbp = queue ! n \<and> tn tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n); mp qhead = Some tcba; tp tcba = NULL; tcb_queue_relation tn tp mp list qhead (tn tcba); n < length list; NULL = tcb_ptr_to_ctcb_ptr ((a # list) ! n); tcbp = list ! n\<rbrakk> \<Longrightarrow> tn tcb = tcb_ptr_to_ctcb_ptr a proof (prove)
goal (2 subgoals):
 1. \<And>a list tcba n. \<lbrakk>tcbp \<in> set list; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; queue = a # list; tp tcb = NULL; tcbp \<noteq> a; 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; if tcbp = (if list = [] then a else last list) then tn tcb = NULL else \<exists>n<length queue - 1. tcbp = queue ! n \<and> tn tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n); mp qhead = Some tcba; tp tcba = NULL; tcb_queue_relation tn tp mp list qhead (tn tcba); n < length list; NULL = tcb_ptr_to_ctcb_ptr ((a # list) ! n); tcbp = list ! n\<rbrakk> \<Longrightarrow> queue ! n \<in> set queue
 2. \<And>a list tcba n. \<lbrakk>tcbp \<in> set list; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; queue = a # list; tp tcb = NULL; tcbp \<noteq> a; 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; if tcbp = (if list = [] then a else last list) then tn tcb = NULL else \<exists>n<length queue - 1. tcbp = queue ! n \<and> tn tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n); mp qhead = Some tcba; tp tcba = NULL; tcb_queue_relation tn tp mp list qhead (tn tcba); n < length list; NULL = tcb_ptr_to_ctcb_ptr ((a # list) ! n); tcbp = list ! n; tcb_ptr_to_ctcb_ptr (queue ! n) \<noteq> NULL\<rbrakk> \<Longrightarrow> tn tcb = tcb_ptr_to_ctcb_ptr a proof (prove)
goal (2 subgoals):
 1. \<And>a list tcba n. \<lbrakk>tcbp \<in> set list; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; queue = a # list; tp tcb = NULL; tcbp \<noteq> a; 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; if tcbp = (if list = [] then a else last list) then tn tcb = NULL else \<exists>n<length queue - 1. tcbp = queue ! n \<and> tn tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n); mp qhead = Some tcba; tp tcba = NULL; tcb_queue_relation tn tp mp list qhead (tn tcba); n < length list; NULL = tcb_ptr_to_ctcb_ptr ((a # list) ! n); tcbp = list ! n\<rbrakk> \<Longrightarrow> n < length queue
 2. \<And>a list tcba n. \<lbrakk>tcbp \<in> set list; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; queue = a # list; tp tcb = NULL; tcbp \<noteq> a; 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; if tcbp = (if list = [] then a else last list) then tn tcb = NULL else \<exists>n<length queue - 1. tcbp = queue ! n \<and> tn tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n); mp qhead = Some tcba; tp tcba = NULL; tcb_queue_relation tn tp mp list qhead (tn tcba); n < length list; NULL = tcb_ptr_to_ctcb_ptr ((a # list) ! n); tcbp = list ! n; tcb_ptr_to_ctcb_ptr (queue ! n) \<noteq> NULL\<rbrakk> \<Longrightarrow> tn tcb = tcb_ptr_to_ctcb_ptr a proof (prove)
goal (1 subgoal):
 1. \<And>a list tcba n. \<lbrakk>tcbp \<in> set list; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; queue = a # list; tp tcb = NULL; tcbp \<noteq> a; 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; if tcbp = (if list = [] then a else last list) then tn tcb = NULL else \<exists>n<length queue - 1. tcbp = queue ! n \<and> tn tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n); mp qhead = Some tcba; tp tcba = NULL; tcb_queue_relation tn tp mp list qhead (tn tcba); n < length list; NULL = tcb_ptr_to_ctcb_ptr ((a # list) ! n); tcbp = list ! n; tcb_ptr_to_ctcb_ptr (queue ! n) \<noteq> NULL\<rbrakk> \<Longrightarrow> tn tcb = tcb_ptr_to_ctcb_ptr a proof (prove)
goal:
No subgoals! proof (state)
this:
(if tp tcb = NULL then tn tcb else qhead) = (if tcb_ptr_to_ctcb_ptr tcbp = qhead then tn tcb else qhead)

goal (1 subgoal):
 1. tcb_queue_relation' tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp queue) (if tp tcb = NULL then tn tcb else qhead) (if tn tcb = NULL then tp tcb else qend) proof (state)
this:
ctcb_ptr_to_tcb_ptr NULL \<notin> set queue

goal (1 subgoal):
 1. tcb_queue_relation' tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp queue) (if tp tcb = NULL then tn tcb else qhead) (if tn tcb = NULL then tp tcb else qend) proof (prove)
goal (1 subgoal):
 1. tcb_queue_relation' tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp queue) (if tp tcb = NULL then tn tcb else qhead) (if tn tcb = NULL then tp tcb else qend) proof (state)
goal (2 subgoals):
 1. tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp queue) NULL (if tp tcb = NULL then tn tcb else qhead)
 2. (if tn tcb = NULL then tp tcb else qend) = (if remove1 tcbp queue = [] then NULL else tcb_ptr_to_ctcb_ptr (last (remove1 tcbp queue))) proof (prove)
goal (1 subgoal):
 1. tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp queue) NULL (if tp tcb = NULL then tn tcb else qhead) proof (prove)
using this:
tcbp \<in> set queue
\<forall>t\<in>set queue. tcb_at' t s
distinct queue
tcb_queue_relation tn tp mp queue NULL qhead
ctcb_ptr_to_tcb_ptr NULL \<notin> set queue
mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb

goal (1 subgoal):
 1. tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp queue) NULL (if tp tcb = NULL then tn tcb else qhead) proof (state)
this:
tcb_queue_relation tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp queue) NULL (if tp tcb = NULL then tn tcb else qhead)

goal (1 subgoal):
 1. (if tn tcb = NULL then tp tcb else qend) = (if remove1 tcbp queue = [] then NULL else tcb_ptr_to_ctcb_ptr (last (remove1 tcbp queue))) proof (state)
goal (1 subgoal):
 1. (if tn tcb = NULL then tp tcb else qend) = (if remove1 tcbp queue = [] then NULL else tcb_ptr_to_ctcb_ptr (last (remove1 tcbp queue))) proof (prove)
goal (1 subgoal):
 1. (remove1 tcbp queue = []) = (tn tcb = NULL \<and> tp tcb = NULL) proof (prove)
using this:
tcbp \<in> set queue
tcb_queue_relation tn tp mp queue NULL qhead
mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb
\<forall>t\<in>set queue. tcb_at' t s
distinct queue
ctcb_ptr_to_tcb_ptr NULL \<notin> set queue

goal (1 subgoal):
 1. (remove1 tcbp queue = []) = (tn tcb = NULL \<and> tp tcb = NULL) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcbp \<in> set queue; tcb_queue_relation tn tp mp queue NULL qhead; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; ctcb_ptr_to_tcb_ptr NULL \<notin> set queue\<rbrakk> \<Longrightarrow> (remove1 tcbp queue = []) = (tn tcb = NULL \<and> tp tcb = NULL) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcbp \<in> set queue; tcb_queue_relation tn tp mp queue NULL qhead; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; ctcb_ptr_to_tcb_ptr NULL \<notin> set queue\<rbrakk> \<Longrightarrow> (remove1 tcbp queue = []) = (queue = [tcbp]) proof (prove)
goal:
No subgoals! proof (state)
this:
(remove1 tcbp queue = []) = (tn tcb = NULL \<and> tp tcb = NULL)

goal (1 subgoal):
 1. (if tn tcb = NULL then tp tcb else qend) = (if remove1 tcbp queue = [] then NULL else tcb_ptr_to_ctcb_ptr (last (remove1 tcbp queue))) proof (prove)
goal (1 subgoal):
 1. queue \<noteq> [] proof (prove)
using this:
tcbp \<in> set queue

goal (1 subgoal):
 1. queue \<noteq> [] proof (state)
this:
queue \<noteq> []

goal (1 subgoal):
 1. (if tn tcb = NULL then tp tcb else qend) = (if remove1 tcbp queue = [] then NULL else tcb_ptr_to_ctcb_ptr (last (remove1 tcbp queue))) proof (prove)
using this:
queue \<noteq> []

goal (1 subgoal):
 1. (if tn tcb = NULL then tp tcb else qend) = (if remove1 tcbp queue = [] then NULL else tcb_ptr_to_ctcb_ptr (last (remove1 tcbp queue))) proof (prove)
using this:
queue \<noteq> []
tcb_queue_relation' tn tp mp queue qhead qend
tcbp \<in> set queue
mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb
\<forall>t\<in>set queue. tcb_at' t s
distinct queue
\<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL

goal (1 subgoal):
 1. (if tn tcb = NULL then tp tcb else qend) = (if remove1 tcbp queue = [] then NULL else tcb_ptr_to_ctcb_ptr (last (remove1 tcbp queue))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>queue \<noteq> []; tcb_queue_relation' tn tp mp queue qhead qend; tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; \<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL\<rbrakk> \<Longrightarrow> (if tn tcb = NULL then tp tcb else qend) = (if remove1 tcbp queue = [] then NULL else tcb_ptr_to_ctcb_ptr (last (remove1 tcbp queue))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>queue \<noteq> []; tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; \<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL; tcb_queue_relation tn tp mp queue NULL qhead; qend = (if queue = [] then NULL else tcb_ptr_to_ctcb_ptr (last queue))\<rbrakk> \<Longrightarrow> (if tn tcb = NULL then tp tcb else qend) = (if remove1 tcbp queue = [] then NULL else tcb_ptr_to_ctcb_ptr (last (remove1 tcbp queue))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>queue \<noteq> []; tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; \<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL; tcb_queue_relation tn tp mp queue NULL qhead; qend = (if queue = [] then NULL else tcb_ptr_to_ctcb_ptr (last queue)); (if tcbp = hd queue then tp tcb = NULL else \<exists>n<length queue - 1. tp tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> tcbp = queue ! Suc n) \<and> (if tcbp = last queue then tn tcb = NULL else \<exists>n<length queue - 1. tcbp = queue ! n \<and> tn tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n))\<rbrakk> \<Longrightarrow> (if tn tcb = NULL then tp tcb else qend) = (if remove1 tcbp queue = [] then NULL else tcb_ptr_to_ctcb_ptr (last (remove1 tcbp queue))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>queue \<noteq> []; tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; \<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL; tcb_queue_relation tn tp mp queue NULL qhead; qend = (if queue = [] then NULL else tcb_ptr_to_ctcb_ptr (last queue)); (if tcbp = hd queue then tp tcb = NULL else \<exists>n<length queue - 1. tp tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> tcbp = queue ! Suc n) \<and> (if tcbp = last queue then tn tcb = NULL else \<exists>n<length queue - 1. tcbp = queue ! n \<and> tn tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n))\<rbrakk> \<Longrightarrow> (if tn tcb = NULL then tp tcb else qend) = (if tn tcb = NULL \<and> tp tcb = NULL then NULL else tcb_ptr_to_ctcb_ptr (last (remove1 tcbp queue))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>queue \<noteq> []; tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; \<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL; tcb_queue_relation tn tp mp queue NULL qhead; qend = tcb_ptr_to_ctcb_ptr (last queue); (if tcbp = hd queue then tp tcb = NULL else \<exists>n<length queue - 1. tp tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> tcbp = queue ! Suc n) \<and> (if tcbp = last queue then tn tcb = NULL else \<exists>n<length queue - 1. tcbp = queue ! n \<and> tn tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n))\<rbrakk> \<Longrightarrow> (tn tcb = NULL \<longrightarrow> tp tcb \<noteq> NULL \<longrightarrow> tp tcb = tcb_ptr_to_ctcb_ptr (last (remove1 tcbp queue))) \<and> (tn tcb \<noteq> NULL \<longrightarrow> last queue = last (remove1 tcbp queue)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>queue \<noteq> []; tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; \<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL; tcb_queue_relation tn tp mp queue NULL qhead; qend = tcb_ptr_to_ctcb_ptr (last queue); (if tcbp = hd queue then tp tcb = NULL else \<exists>n<length queue - 1. tp tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> tcbp = queue ! Suc n) \<and> (if tcbp = last queue then tn tcb = NULL else \<exists>n<length queue - 1. tcbp = queue ! n \<and> tn tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n)); tn tcb = NULL; tp tcb \<noteq> NULL\<rbrakk> \<Longrightarrow> tp tcb = tcb_ptr_to_ctcb_ptr (last (remove1 tcbp queue))
 2. \<lbrakk>queue \<noteq> []; tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; \<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL; tcb_queue_relation tn tp mp queue NULL qhead; qend = tcb_ptr_to_ctcb_ptr (last queue); (if tcbp = hd queue then tp tcb = NULL else \<exists>n<length queue - 1. tp tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> tcbp = queue ! Suc n) \<and> (if tcbp = last queue then tn tcb = NULL else \<exists>n<length queue - 1. tcbp = queue ! n \<and> tn tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n)); tn tcb \<noteq> NULL\<rbrakk> \<Longrightarrow> last queue = last (remove1 tcbp queue) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>queue \<noteq> []; tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; \<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL; tcb_queue_relation tn tp mp queue NULL qhead; qend = tcb_ptr_to_ctcb_ptr (last queue); (if tcbp = hd queue then tp tcb = NULL else \<exists>n<length queue - 1. tp tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> tcbp = queue ! Suc n) \<and> (if tcbp = last queue then tn tcb = NULL else \<exists>n<length queue - 1. tcbp = queue ! n \<and> tn tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n)); tn tcb = NULL; tp tcb \<noteq> NULL; tcbp = last queue\<rbrakk> \<Longrightarrow> tp tcb = tcb_ptr_to_ctcb_ptr (last (remove1 tcbp queue))
 2. \<lbrakk>queue \<noteq> []; tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; \<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL; tcb_queue_relation tn tp mp queue NULL qhead; qend = tcb_ptr_to_ctcb_ptr (last queue); (if tcbp = hd queue then tp tcb = NULL else \<exists>n<length queue - 1. tp tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> tcbp = queue ! Suc n) \<and> (if tcbp = last queue then tn tcb = NULL else \<exists>n<length queue - 1. tcbp = queue ! n \<and> tn tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n)); tn tcb = NULL; tp tcb \<noteq> NULL\<rbrakk> \<Longrightarrow> tcbp = last queue
 3. \<lbrakk>queue \<noteq> []; tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; \<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL; tcb_queue_relation tn tp mp queue NULL qhead; qend = tcb_ptr_to_ctcb_ptr (last queue); (if tcbp = hd queue then tp tcb = NULL else \<exists>n<length queue - 1. tp tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> tcbp = queue ! Suc n) \<and> (if tcbp = last queue then tn tcb = NULL else \<exists>n<length queue - 1. tcbp = queue ! n \<and> tn tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n)); tn tcb \<noteq> NULL\<rbrakk> \<Longrightarrow> last queue = last (remove1 tcbp queue) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>queue \<noteq> []; mp (tcb_ptr_to_ctcb_ptr (last queue)) = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; \<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL; tcb_queue_relation tn tp mp queue NULL qhead; qend = tcb_ptr_to_ctcb_ptr (last queue); if last queue = hd queue then tp tcb = NULL else \<exists>n<length queue - 1. tp tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> tcbp = queue ! Suc n; tn tcb = NULL; tp tcb \<noteq> NULL; tcbp = last queue\<rbrakk> \<Longrightarrow> tp tcb = tcb_ptr_to_ctcb_ptr (last (remove1 (last queue) queue))
 2. \<lbrakk>queue \<noteq> []; tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; \<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL; tcb_queue_relation tn tp mp queue NULL qhead; qend = tcb_ptr_to_ctcb_ptr (last queue); (if tcbp = hd queue then tp tcb = NULL else \<exists>n<length queue - 1. tp tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> tcbp = queue ! Suc n) \<and> (if tcbp = last queue then tn tcb = NULL else \<exists>n<length queue - 1. tcbp = queue ! n \<and> tn tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n)); tn tcb = NULL; tp tcb \<noteq> NULL\<rbrakk> \<Longrightarrow> tcbp = last queue
 3. \<lbrakk>queue \<noteq> []; tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; \<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL; tcb_queue_relation tn tp mp queue NULL qhead; qend = tcb_ptr_to_ctcb_ptr (last queue); (if tcbp = hd queue then tp tcb = NULL else \<exists>n<length queue - 1. tp tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> tcbp = queue ! Suc n) \<and> (if tcbp = last queue then tn tcb = NULL else \<exists>n<length queue - 1. tcbp = queue ! n \<and> tn tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n)); tn tcb \<noteq> NULL\<rbrakk> \<Longrightarrow> last queue = last (remove1 tcbp queue) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>queue \<noteq> []; mp (tcb_ptr_to_ctcb_ptr (last queue)) = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; \<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL; tcb_queue_relation tn tp mp queue NULL qhead; qend = tcb_ptr_to_ctcb_ptr (last queue); if last queue = hd queue then tp tcb = NULL else \<exists>n<length queue - 1. tp tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> tcbp = queue ! Suc n; tn tcb = NULL; tp tcb \<noteq> NULL; tcbp = last queue; remove1 (last queue) queue \<noteq> []\<rbrakk> \<Longrightarrow> tp tcb = tcb_ptr_to_ctcb_ptr (last (remove1 (last queue) queue))
 2. \<lbrakk>queue \<noteq> []; mp (tcb_ptr_to_ctcb_ptr (last queue)) = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; \<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL; tcb_queue_relation tn tp mp queue NULL qhead; qend = tcb_ptr_to_ctcb_ptr (last queue); if last queue = hd queue then tp tcb = NULL else \<exists>n<length queue - 1. tp tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> tcbp = queue ! Suc n; tn tcb = NULL; tp tcb \<noteq> NULL; tcbp = last queue\<rbrakk> \<Longrightarrow> remove1 (last queue) queue \<noteq> []
 3. \<lbrakk>queue \<noteq> []; tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; \<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL; tcb_queue_relation tn tp mp queue NULL qhead; qend = tcb_ptr_to_ctcb_ptr (last queue); (if tcbp = hd queue then tp tcb = NULL else \<exists>n<length queue - 1. tp tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> tcbp = queue ! Suc n) \<and> (if tcbp = last queue then tn tcb = NULL else \<exists>n<length queue - 1. tcbp = queue ! n \<and> tn tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n)); tn tcb = NULL; tp tcb \<noteq> NULL\<rbrakk> \<Longrightarrow> tcbp = last queue
 4. \<lbrakk>queue \<noteq> []; tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; \<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL; tcb_queue_relation tn tp mp queue NULL qhead; qend = tcb_ptr_to_ctcb_ptr (last queue); (if tcbp = hd queue then tp tcb = NULL else \<exists>n<length queue - 1. tp tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> tcbp = queue ! Suc n) \<and> (if tcbp = last queue then tn tcb = NULL else \<exists>n<length queue - 1. tcbp = queue ! n \<and> tn tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n)); tn tcb \<noteq> NULL\<rbrakk> \<Longrightarrow> last queue = last (remove1 tcbp queue) proof (prove)
goal (4 subgoals):
 1. \<And>n. \<lbrakk>tn tcb = NULL; tcbp = queue ! Suc n; \<not> length queue \<le> Suc 0; queue \<noteq> []; mp (tcb_ptr_to_ctcb_ptr (queue ! Suc n)) = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; \<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL; tcb_queue_relation tn tp mp queue NULL qhead; qend = tcb_ptr_to_ctcb_ptr (queue ! Suc n); queue ! Suc n \<noteq> hd queue; tp tcb = tcb_ptr_to_ctcb_ptr (queue ! n); length queue - Suc 0 = Suc n\<rbrakk> \<Longrightarrow> n = length queue - Suc (Suc 0)
 2. \<lbrakk>queue \<noteq> []; mp (tcb_ptr_to_ctcb_ptr (last queue)) = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; \<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL; tcb_queue_relation tn tp mp queue NULL qhead; qend = tcb_ptr_to_ctcb_ptr (last queue); if last queue = hd queue then tp tcb = NULL else \<exists>n<length queue - 1. tp tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> tcbp = queue ! Suc n; tn tcb = NULL; tp tcb \<noteq> NULL; tcbp = last queue\<rbrakk> \<Longrightarrow> remove1 (last queue) queue \<noteq> []
 3. \<lbrakk>queue \<noteq> []; tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; \<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL; tcb_queue_relation tn tp mp queue NULL qhead; qend = tcb_ptr_to_ctcb_ptr (last queue); (if tcbp = hd queue then tp tcb = NULL else \<exists>n<length queue - 1. tp tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> tcbp = queue ! Suc n) \<and> (if tcbp = last queue then tn tcb = NULL else \<exists>n<length queue - 1. tcbp = queue ! n \<and> tn tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n)); tn tcb = NULL; tp tcb \<noteq> NULL\<rbrakk> \<Longrightarrow> tcbp = last queue
 4. \<lbrakk>queue \<noteq> []; tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; \<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL; tcb_queue_relation tn tp mp queue NULL qhead; qend = tcb_ptr_to_ctcb_ptr (last queue); (if tcbp = hd queue then tp tcb = NULL else \<exists>n<length queue - 1. tp tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> tcbp = queue ! Suc n) \<and> (if tcbp = last queue then tn tcb = NULL else \<exists>n<length queue - 1. tcbp = queue ! n \<and> tn tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n)); tn tcb \<noteq> NULL\<rbrakk> \<Longrightarrow> last queue = last (remove1 tcbp queue) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>queue \<noteq> []; mp (tcb_ptr_to_ctcb_ptr (last queue)) = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; \<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL; tcb_queue_relation tn tp mp queue NULL qhead; qend = tcb_ptr_to_ctcb_ptr (last queue); if last queue = hd queue then tp tcb = NULL else \<exists>n<length queue - 1. tp tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> tcbp = queue ! Suc n; tn tcb = NULL; tp tcb \<noteq> NULL; tcbp = last queue\<rbrakk> \<Longrightarrow> remove1 (last queue) queue \<noteq> []
 2. \<lbrakk>queue \<noteq> []; tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; \<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL; tcb_queue_relation tn tp mp queue NULL qhead; qend = tcb_ptr_to_ctcb_ptr (last queue); (if tcbp = hd queue then tp tcb = NULL else \<exists>n<length queue - 1. tp tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> tcbp = queue ! Suc n) \<and> (if tcbp = last queue then tn tcb = NULL else \<exists>n<length queue - 1. tcbp = queue ! n \<and> tn tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n)); tn tcb = NULL; tp tcb \<noteq> NULL\<rbrakk> \<Longrightarrow> tcbp = last queue
 3. \<lbrakk>queue \<noteq> []; tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; \<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL; tcb_queue_relation tn tp mp queue NULL qhead; qend = tcb_ptr_to_ctcb_ptr (last queue); (if tcbp = hd queue then tp tcb = NULL else \<exists>n<length queue - 1. tp tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> tcbp = queue ! Suc n) \<and> (if tcbp = last queue then tn tcb = NULL else \<exists>n<length queue - 1. tcbp = queue ! n \<and> tn tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n)); tn tcb \<noteq> NULL\<rbrakk> \<Longrightarrow> last queue = last (remove1 tcbp queue) proof (prove)
goal (3 subgoals):
 1. \<And>n. \<lbrakk>tn tcb = NULL; tcbp = queue ! Suc n; queue \<noteq> []; mp (tcb_ptr_to_ctcb_ptr (queue ! Suc n)) = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; \<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL; tcb_queue_relation tn tp mp queue NULL qhead; qend = tcb_ptr_to_ctcb_ptr (queue ! Suc n); Suc 0 < length queue; tp tcb = tcb_ptr_to_ctcb_ptr (queue ! n); length queue - Suc 0 = Suc n; queue = [queue ! Suc n]\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>queue \<noteq> []; tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; \<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL; tcb_queue_relation tn tp mp queue NULL qhead; qend = tcb_ptr_to_ctcb_ptr (last queue); (if tcbp = hd queue then tp tcb = NULL else \<exists>n<length queue - 1. tp tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> tcbp = queue ! Suc n) \<and> (if tcbp = last queue then tn tcb = NULL else \<exists>n<length queue - 1. tcbp = queue ! n \<and> tn tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n)); tn tcb = NULL; tp tcb \<noteq> NULL\<rbrakk> \<Longrightarrow> tcbp = last queue
 3. \<lbrakk>queue \<noteq> []; tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; \<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL; tcb_queue_relation tn tp mp queue NULL qhead; qend = tcb_ptr_to_ctcb_ptr (last queue); (if tcbp = hd queue then tp tcb = NULL else \<exists>n<length queue - 1. tp tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> tcbp = queue ! Suc n) \<and> (if tcbp = last queue then tn tcb = NULL else \<exists>n<length queue - 1. tcbp = queue ! n \<and> tn tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n)); tn tcb \<noteq> NULL\<rbrakk> \<Longrightarrow> last queue = last (remove1 tcbp queue) proof (prove)
goal (4 subgoals):
 1. \<And>n. \<lbrakk>tn tcb = NULL; tcbp = queue ! Suc n; queue \<noteq> []; mp (tcb_ptr_to_ctcb_ptr (queue ! Suc n)) = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; \<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL; tcb_queue_relation tn tp mp queue NULL qhead; qend = tcb_ptr_to_ctcb_ptr (queue ! Suc n); Suc 0 < length queue; tp tcb = tcb_ptr_to_ctcb_ptr (queue ! n); length queue - Suc 0 = Suc n; queue = [queue ! Suc n]; queue = []\<rbrakk> \<Longrightarrow> False
 2. \<And>n a list. \<lbrakk>tn tcb = NULL; tcbp = queue ! Suc n; queue \<noteq> []; mp (tcb_ptr_to_ctcb_ptr (queue ! Suc n)) = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; \<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL; tcb_queue_relation tn tp mp queue NULL qhead; qend = tcb_ptr_to_ctcb_ptr (queue ! Suc n); Suc 0 < length queue; tp tcb = tcb_ptr_to_ctcb_ptr (queue ! n); length queue - Suc 0 = Suc n; queue = [queue ! Suc n]; queue = a # list\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>queue \<noteq> []; tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; \<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL; tcb_queue_relation tn tp mp queue NULL qhead; qend = tcb_ptr_to_ctcb_ptr (last queue); (if tcbp = hd queue then tp tcb = NULL else \<exists>n<length queue - 1. tp tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> tcbp = queue ! Suc n) \<and> (if tcbp = last queue then tn tcb = NULL else \<exists>n<length queue - 1. tcbp = queue ! n \<and> tn tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n)); tn tcb = NULL; tp tcb \<noteq> NULL\<rbrakk> \<Longrightarrow> tcbp = last queue
 4. \<lbrakk>queue \<noteq> []; tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; \<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL; tcb_queue_relation tn tp mp queue NULL qhead; qend = tcb_ptr_to_ctcb_ptr (last queue); (if tcbp = hd queue then tp tcb = NULL else \<exists>n<length queue - 1. tp tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> tcbp = queue ! Suc n) \<and> (if tcbp = last queue then tn tcb = NULL else \<exists>n<length queue - 1. tcbp = queue ! n \<and> tn tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n)); tn tcb \<noteq> NULL\<rbrakk> \<Longrightarrow> last queue = last (remove1 tcbp queue) proof (prove)
goal (3 subgoals):
 1. \<And>n a list. \<lbrakk>tn tcb = NULL; tcbp = queue ! Suc n; queue \<noteq> []; mp (tcb_ptr_to_ctcb_ptr (queue ! Suc n)) = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; \<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL; tcb_queue_relation tn tp mp queue NULL qhead; qend = tcb_ptr_to_ctcb_ptr (queue ! Suc n); Suc 0 < length queue; tp tcb = tcb_ptr_to_ctcb_ptr (queue ! n); length queue - Suc 0 = Suc n; queue = [queue ! Suc n]; queue = a # list\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>queue \<noteq> []; tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; \<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL; tcb_queue_relation tn tp mp queue NULL qhead; qend = tcb_ptr_to_ctcb_ptr (last queue); (if tcbp = hd queue then tp tcb = NULL else \<exists>n<length queue - 1. tp tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> tcbp = queue ! Suc n) \<and> (if tcbp = last queue then tn tcb = NULL else \<exists>n<length queue - 1. tcbp = queue ! n \<and> tn tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n)); tn tcb = NULL; tp tcb \<noteq> NULL\<rbrakk> \<Longrightarrow> tcbp = last queue
 3. \<lbrakk>queue \<noteq> []; tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; \<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL; tcb_queue_relation tn tp mp queue NULL qhead; qend = tcb_ptr_to_ctcb_ptr (last queue); (if tcbp = hd queue then tp tcb = NULL else \<exists>n<length queue - 1. tp tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> tcbp = queue ! Suc n) \<and> (if tcbp = last queue then tn tcb = NULL else \<exists>n<length queue - 1. tcbp = queue ! n \<and> tn tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n)); tn tcb \<noteq> NULL\<rbrakk> \<Longrightarrow> last queue = last (remove1 tcbp queue) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>queue \<noteq> []; tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; \<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL; tcb_queue_relation tn tp mp queue NULL qhead; qend = tcb_ptr_to_ctcb_ptr (last queue); (if tcbp = hd queue then tp tcb = NULL else \<exists>n<length queue - 1. tp tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> tcbp = queue ! Suc n) \<and> (if tcbp = last queue then tn tcb = NULL else \<exists>n<length queue - 1. tcbp = queue ! n \<and> tn tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n)); tn tcb = NULL; tp tcb \<noteq> NULL\<rbrakk> \<Longrightarrow> tcbp = last queue
 2. \<lbrakk>queue \<noteq> []; tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; \<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL; tcb_queue_relation tn tp mp queue NULL qhead; qend = tcb_ptr_to_ctcb_ptr (last queue); (if tcbp = hd queue then tp tcb = NULL else \<exists>n<length queue - 1. tp tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> tcbp = queue ! Suc n) \<and> (if tcbp = last queue then tn tcb = NULL else \<exists>n<length queue - 1. tcbp = queue ! n \<and> tn tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n)); tn tcb \<noteq> NULL\<rbrakk> \<Longrightarrow> last queue = last (remove1 tcbp queue) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>queue \<noteq> []; tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; \<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL; tcb_queue_relation tn tp mp queue NULL qhead; qend = tcb_ptr_to_ctcb_ptr (last queue); (if tcbp = hd queue then tp tcb = NULL else \<exists>n<length queue - 1. tp tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> tcbp = queue ! Suc n) \<and> (if tcbp = last queue then tn tcb = NULL else \<exists>n<length queue - 1. tcbp = queue ! n \<and> tn tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n)); tn tcb \<noteq> NULL\<rbrakk> \<Longrightarrow> last queue = last (remove1 tcbp queue) proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>queue \<noteq> []; mp (tcb_ptr_to_ctcb_ptr (queue ! n)) = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; \<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL; tcb_queue_relation tn tp mp queue NULL qhead; qend = tcb_ptr_to_ctcb_ptr (queue ! (length queue - Suc 0)); tcbp = queue ! n; tp tcb = NULL; n < length queue - Suc 0; hd queue = queue ! n; tn tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n)\<rbrakk> \<Longrightarrow> length queue - Suc 0 = Suc (length queue - 2)
 2. \<And>n. \<lbrakk>queue \<noteq> []; mp (tcb_ptr_to_ctcb_ptr (queue ! Suc n)) = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; \<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL; tcb_queue_relation tn tp mp queue NULL qhead; qend = tcb_ptr_to_ctcb_ptr (queue ! (length queue - Suc 0)); queue ! Suc n \<noteq> hd queue; Suc n < length queue - Suc 0; tp tcb = tcb_ptr_to_ctcb_ptr (queue ! n); tcbp = queue ! Suc n; tn tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc (Suc n))\<rbrakk> \<Longrightarrow> queue ! (length queue - Suc 0) = (take (Suc n) queue @ drop (Suc (Suc n)) queue) ! (length queue - Suc (Suc 0)) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>queue \<noteq> []; mp (tcb_ptr_to_ctcb_ptr (queue ! Suc n)) = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; \<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL; tcb_queue_relation tn tp mp queue NULL qhead; qend = tcb_ptr_to_ctcb_ptr (queue ! (length queue - Suc 0)); queue ! Suc n \<noteq> hd queue; Suc n < length queue - Suc 0; tp tcb = tcb_ptr_to_ctcb_ptr (queue ! n); tcbp = queue ! Suc n; tn tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc (Suc n))\<rbrakk> \<Longrightarrow> queue ! (length queue - Suc 0) = (take (Suc n) queue @ drop (Suc (Suc n)) queue) ! (length queue - Suc (Suc 0)) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>queue \<noteq> []; mp (tcb_ptr_to_ctcb_ptr (queue ! Suc n)) = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; \<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL; tcb_queue_relation tn tp mp queue NULL qhead; qend = tcb_ptr_to_ctcb_ptr (queue ! (length queue - Suc 0)); queue ! Suc n \<noteq> hd queue; Suc n < length queue - Suc 0; tp tcb = tcb_ptr_to_ctcb_ptr (queue ! n); tcbp = queue ! Suc n; tn tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc (Suc n))\<rbrakk> \<Longrightarrow> \<not> length queue \<le> Suc n \<longrightarrow> \<not> length queue - Suc (Suc 0) < Suc n \<longrightarrow> length queue - Suc 0 = Suc (Suc (length queue - 3)) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>queue \<noteq> []; mp (tcb_ptr_to_ctcb_ptr (queue ! Suc n)) = Some tcb; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; \<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL; tcb_queue_relation tn tp mp queue NULL qhead; qend = tcb_ptr_to_ctcb_ptr (queue ! (length queue - Suc 0)); queue ! Suc n \<noteq> hd queue; Suc n < length queue - Suc 0; tp tcb = tcb_ptr_to_ctcb_ptr (queue ! n); tcbp = queue ! Suc n; tn tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc (Suc n)); \<not> length queue \<le> Suc n; \<not> length queue - Suc (Suc 0) < Suc n\<rbrakk> \<Longrightarrow> length queue - Suc 0 = Suc (Suc (length queue - 3)) proof (prove)
goal:
No subgoals! proof (state)
this:
(if tn tcb = NULL then tp tcb else qend) = (if remove1 tcbp queue = [] then NULL else tcb_ptr_to_ctcb_ptr (last (remove1 tcbp queue)))

goal:
No subgoals! proof (state)
this:
tcb_queue_relation' tn tp (upd_unless_null (tn tcb) (tp_update (\<lambda>_. tp tcb) (the (mp (tn tcb)))) (upd_unless_null (tp tcb) (tn_update (\<lambda>_. tn tcb) (the (mp (tp tcb)))) mp)) (remove1 tcbp queue) (if tp tcb = NULL then tn tcb else qhead) (if tn tcb = NULL then tp tcb else qend)

goal:
No subgoals!