theory TcbQueue_C

lemma tcb_queueD:
  assumes queue_rel: "tcb_queue_relation getNext getPrev mp queue qprev qhead"
  and     valid_ntfn: "distinct queue"
  and      in_queue: "tcbp \<in> set queue"
  and        cs_tcb: "mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb"
  shows "(if tcbp = hd queue then getPrev tcb = qprev
                  else (\<exists>n < (length queue) - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr (queue ! n)
                                                                    \<and> tcbp = queue ! Suc n))
         \<and> (if tcbp = last queue then getNext tcb = NULL
                  else (\<exists>n < (length queue) - 1. tcbp = queue ! n
                        \<and> getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n)))"
  (is "?prev tcb queue qprev \<and> ?next tcb queue") using queue_rel in_queue valid_ntfn proof (induct queue arbitrary: qprev qhead) case Nil thus ?case by simp next case (Cons tcb' tcbs qprev' qhead') have "tcbp = tcb' \<or> tcbp \<in> set tcbs" using Cons.prems by simp thus ?case proof assume tcbp: "tcbp = tcb'" hence "?prev tcb (tcb' # tcbs) qprev'" using Cons.prems cs_tcb by clarsimp moreover have "?next tcb (tcb' # tcbs)" proof (cases "tcbs = []") case True thus ?thesis using tcbp Cons.prems cs_tcb by clarsimp next case False hence "tcbp \<noteq> last tcbs" using tcbp Cons.prems by clarsimp thus ?thesis using False tcbp Cons.prems cs_tcb apply clarsimp apply (rule exI [where x = 0]) apply simp apply (cases tcbs) apply simp_all done qed ultimately show ?thesis .. next assume tcbp: "tcbp \<in> set tcbs" obtain tcb2 where cs_tcb2: "mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2"
      and rel2: "tcb_queue_relation getNext getPrev mp tcbs (tcb_ptr_to_ctcb_ptr tcb') (getNext tcb2)" using Cons.prems by clarsimp have ih: "?prev tcb tcbs (tcb_ptr_to_ctcb_ptr tcb') \<and> ?next tcb tcbs" proof (rule Cons.hyps) from Cons.prems show (* "\<forall>t\<in>set tcbs. tcb_at' t s"
        and *) "distinct tcbs" by simp_all qed fact+ from tcbp Cons.prems have tcbp_not_tcb': "tcbp \<noteq> tcb'" by clarsimp from tcbp have tcbsnz: "tcbs \<noteq> []" by clarsimp hence hd_tcbs: "hd tcbs = tcbs ! 0" by (simp add: hd_conv_nth) show ?case proof (rule conjI) show "?prev tcb (tcb' # tcbs) qprev'" using ih [THEN conjunct1] tcbp_not_tcb' hd_tcbs tcbsnz apply (clarsimp split: if_split_asm) apply fastforce apply (rule_tac x = "Suc n" in exI) apply simp done next show "?next tcb (tcb' # tcbs)" using ih [THEN conjunct2] tcbp_not_tcb' hd_tcbs tcbsnz apply (clarsimp split: if_split_asm) apply (rule_tac x = "Suc n" in exI) apply simp done qed qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (if tcbp = hd queue then getPrev tcb = qprev else \<exists>n<length queue - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> tcbp = queue ! Suc n) \<and> (if tcbp = last queue then getNext tcb = NULL else \<exists>n<length queue - 1. tcbp = queue ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n)) proof (prove)
using this:
tcb_queue_relation getNext getPrev mp queue qprev qhead
tcbp \<in> set queue
distinct queue

goal (1 subgoal):
 1. (if tcbp = hd queue then getPrev tcb = qprev else \<exists>n<length queue - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> tcbp = queue ! Suc n) \<and> (if tcbp = last queue then getNext tcb = NULL else \<exists>n<length queue - 1. tcbp = queue ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n)) proof (state)
goal (2 subgoals):
 1. \<And>qprev qhead. \<lbrakk>tcb_queue_relation getNext getPrev mp [] qprev qhead; tcbp \<in> set []; distinct []\<rbrakk> \<Longrightarrow> (if tcbp = hd [] then getPrev tcb = qprev else \<exists>n<length [] - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr ([] ! n) \<and> tcbp = [] ! Suc n) \<and> (if tcbp = last [] then getNext tcb = NULL else \<exists>n<length [] - 1. tcbp = [] ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ([] ! Suc n))
 2. \<And>x1 queue qprev qhead. \<lbrakk>\<And>qprev qhead. \<lbrakk>tcb_queue_relation getNext getPrev mp queue qprev qhead; tcbp \<in> set queue; distinct queue\<rbrakk> \<Longrightarrow> (if tcbp = hd queue then getPrev tcb = qprev else \<exists>n<length queue - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> tcbp = queue ! Suc n) \<and> (if tcbp = last queue then getNext tcb = NULL else \<exists>n<length queue - 1. tcbp = queue ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n)); tcb_queue_relation getNext getPrev mp (x1 # queue) qprev qhead; tcbp \<in> set (x1 # queue); distinct (x1 # queue)\<rbrakk> \<Longrightarrow> (if tcbp = hd (x1 # queue) then getPrev tcb = qprev else \<exists>n<length (x1 # queue) - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr ((x1 # queue) ! n) \<and> tcbp = (x1 # queue) ! Suc n) \<and> (if tcbp = last (x1 # queue) then getNext tcb = NULL else \<exists>n<length (x1 # queue) - 1. tcbp = (x1 # queue) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ((x1 # queue) ! Suc n)) proof (state)
this:
tcb_queue_relation getNext getPrev mp [] qprev qhead
tcbp \<in> set []
distinct []

goal (2 subgoals):
 1. \<And>qprev qhead. \<lbrakk>tcb_queue_relation getNext getPrev mp [] qprev qhead; tcbp \<in> set []; distinct []\<rbrakk> \<Longrightarrow> (if tcbp = hd [] then getPrev tcb = qprev else \<exists>n<length [] - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr ([] ! n) \<and> tcbp = [] ! Suc n) \<and> (if tcbp = last [] then getNext tcb = NULL else \<exists>n<length [] - 1. tcbp = [] ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ([] ! Suc n))
 2. \<And>x1 queue qprev qhead. \<lbrakk>\<And>qprev qhead. \<lbrakk>tcb_queue_relation getNext getPrev mp queue qprev qhead; tcbp \<in> set queue; distinct queue\<rbrakk> \<Longrightarrow> (if tcbp = hd queue then getPrev tcb = qprev else \<exists>n<length queue - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> tcbp = queue ! Suc n) \<and> (if tcbp = last queue then getNext tcb = NULL else \<exists>n<length queue - 1. tcbp = queue ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n)); tcb_queue_relation getNext getPrev mp (x1 # queue) qprev qhead; tcbp \<in> set (x1 # queue); distinct (x1 # queue)\<rbrakk> \<Longrightarrow> (if tcbp = hd (x1 # queue) then getPrev tcb = qprev else \<exists>n<length (x1 # queue) - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr ((x1 # queue) ! n) \<and> tcbp = (x1 # queue) ! Suc n) \<and> (if tcbp = last (x1 # queue) then getNext tcb = NULL else \<exists>n<length (x1 # queue) - 1. tcbp = (x1 # queue) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ((x1 # queue) ! Suc n)) proof (prove)
using this:
tcb_queue_relation getNext getPrev mp [] qprev qhead
tcbp \<in> set []
distinct []

goal (1 subgoal):
 1. (if tcbp = hd [] then getPrev tcb = qprev else \<exists>n<length [] - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr ([] ! n) \<and> tcbp = [] ! Suc n) \<and> (if tcbp = last [] then getNext tcb = NULL else \<exists>n<length [] - 1. tcbp = [] ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ([] ! Suc n)) proof (state)
this:
(if tcbp = hd [] then getPrev tcb = qprev else \<exists>n<length [] - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr ([] ! n) \<and> tcbp = [] ! Suc n) \<and> (if tcbp = last [] then getNext tcb = NULL else \<exists>n<length [] - 1. tcbp = [] ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ([] ! Suc n))

goal (1 subgoal):
 1. \<And>x1 queue qprev qhead. \<lbrakk>\<And>qprev qhead. \<lbrakk>tcb_queue_relation getNext getPrev mp queue qprev qhead; tcbp \<in> set queue; distinct queue\<rbrakk> \<Longrightarrow> (if tcbp = hd queue then getPrev tcb = qprev else \<exists>n<length queue - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> tcbp = queue ! Suc n) \<and> (if tcbp = last queue then getNext tcb = NULL else \<exists>n<length queue - 1. tcbp = queue ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n)); tcb_queue_relation getNext getPrev mp (x1 # queue) qprev qhead; tcbp \<in> set (x1 # queue); distinct (x1 # queue)\<rbrakk> \<Longrightarrow> (if tcbp = hd (x1 # queue) then getPrev tcb = qprev else \<exists>n<length (x1 # queue) - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr ((x1 # queue) ! n) \<and> tcbp = (x1 # queue) ! Suc n) \<and> (if tcbp = last (x1 # queue) then getNext tcb = NULL else \<exists>n<length (x1 # queue) - 1. tcbp = (x1 # queue) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ((x1 # queue) ! Suc n)) proof (state)
goal (1 subgoal):
 1. \<And>x1 queue qprev qhead. \<lbrakk>\<And>qprev qhead. \<lbrakk>tcb_queue_relation getNext getPrev mp queue qprev qhead; tcbp \<in> set queue; distinct queue\<rbrakk> \<Longrightarrow> (if tcbp = hd queue then getPrev tcb = qprev else \<exists>n<length queue - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> tcbp = queue ! Suc n) \<and> (if tcbp = last queue then getNext tcb = NULL else \<exists>n<length queue - 1. tcbp = queue ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n)); tcb_queue_relation getNext getPrev mp (x1 # queue) qprev qhead; tcbp \<in> set (x1 # queue); distinct (x1 # queue)\<rbrakk> \<Longrightarrow> (if tcbp = hd (x1 # queue) then getPrev tcb = qprev else \<exists>n<length (x1 # queue) - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr ((x1 # queue) ! n) \<and> tcbp = (x1 # queue) ! Suc n) \<and> (if tcbp = last (x1 # queue) then getNext tcb = NULL else \<exists>n<length (x1 # queue) - 1. tcbp = (x1 # queue) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ((x1 # queue) ! Suc n)) proof (state)
this:
\<lbrakk>tcb_queue_relation getNext getPrev mp tcbs ?qprev ?qhead; tcbp \<in> set tcbs; distinct tcbs\<rbrakk> \<Longrightarrow> (if tcbp = hd tcbs then getPrev tcb = ?qprev else \<exists>n<length tcbs - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr (tcbs ! n) \<and> tcbp = tcbs ! Suc n) \<and> (if tcbp = last tcbs then getNext tcb = NULL else \<exists>n<length tcbs - 1. tcbp = tcbs ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr (tcbs ! Suc n))
tcb_queue_relation getNext getPrev mp (tcb' # tcbs) qprev' qhead'
tcbp \<in> set (tcb' # tcbs)
distinct (tcb' # tcbs)

goal (1 subgoal):
 1. \<And>x1 queue qprev qhead. \<lbrakk>\<And>qprev qhead. \<lbrakk>tcb_queue_relation getNext getPrev mp queue qprev qhead; tcbp \<in> set queue; distinct queue\<rbrakk> \<Longrightarrow> (if tcbp = hd queue then getPrev tcb = qprev else \<exists>n<length queue - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> tcbp = queue ! Suc n) \<and> (if tcbp = last queue then getNext tcb = NULL else \<exists>n<length queue - 1. tcbp = queue ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n)); tcb_queue_relation getNext getPrev mp (x1 # queue) qprev qhead; tcbp \<in> set (x1 # queue); distinct (x1 # queue)\<rbrakk> \<Longrightarrow> (if tcbp = hd (x1 # queue) then getPrev tcb = qprev else \<exists>n<length (x1 # queue) - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr ((x1 # queue) ! n) \<and> tcbp = (x1 # queue) ! Suc n) \<and> (if tcbp = last (x1 # queue) then getNext tcb = NULL else \<exists>n<length (x1 # queue) - 1. tcbp = (x1 # queue) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ((x1 # queue) ! Suc n)) proof (prove)
goal (1 subgoal):
 1. tcbp = tcb' \<or> tcbp \<in> set tcbs proof (prove)
using this:
tcb_queue_relation getNext getPrev mp (tcb' # tcbs) qprev' qhead'
tcbp \<in> set (tcb' # tcbs)
distinct (tcb' # tcbs)

goal (1 subgoal):
 1. tcbp = tcb' \<or> tcbp \<in> set tcbs proof (state)
this:
tcbp = tcb' \<or> tcbp \<in> set tcbs

goal (1 subgoal):
 1. \<And>x1 queue qprev qhead. \<lbrakk>\<And>qprev qhead. \<lbrakk>tcb_queue_relation getNext getPrev mp queue qprev qhead; tcbp \<in> set queue; distinct queue\<rbrakk> \<Longrightarrow> (if tcbp = hd queue then getPrev tcb = qprev else \<exists>n<length queue - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr (queue ! n) \<and> tcbp = queue ! Suc n) \<and> (if tcbp = last queue then getNext tcb = NULL else \<exists>n<length queue - 1. tcbp = queue ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n)); tcb_queue_relation getNext getPrev mp (x1 # queue) qprev qhead; tcbp \<in> set (x1 # queue); distinct (x1 # queue)\<rbrakk> \<Longrightarrow> (if tcbp = hd (x1 # queue) then getPrev tcb = qprev else \<exists>n<length (x1 # queue) - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr ((x1 # queue) ! n) \<and> tcbp = (x1 # queue) ! Suc n) \<and> (if tcbp = last (x1 # queue) then getNext tcb = NULL else \<exists>n<length (x1 # queue) - 1. tcbp = (x1 # queue) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ((x1 # queue) ! Suc n)) proof (prove)
using this:
tcbp = tcb' \<or> tcbp \<in> set tcbs

goal (1 subgoal):
 1. (if tcbp = hd (tcb' # tcbs) then getPrev tcb = qprev' else \<exists>n<length (tcb' # tcbs) - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! n) \<and> tcbp = (tcb' # tcbs) ! Suc n) \<and> (if tcbp = last (tcb' # tcbs) then getNext tcb = NULL else \<exists>n<length (tcb' # tcbs) - 1. tcbp = (tcb' # tcbs) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! Suc n)) proof (state)
goal (2 subgoals):
 1. tcbp = tcb' \<Longrightarrow> (if tcbp = hd (tcb' # tcbs) then getPrev tcb = qprev' else \<exists>n<length (tcb' # tcbs) - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! n) \<and> tcbp = (tcb' # tcbs) ! Suc n) \<and> (if tcbp = last (tcb' # tcbs) then getNext tcb = NULL else \<exists>n<length (tcb' # tcbs) - 1. tcbp = (tcb' # tcbs) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! Suc n))
 2. tcbp \<in> set tcbs \<Longrightarrow> (if tcbp = hd (tcb' # tcbs) then getPrev tcb = qprev' else \<exists>n<length (tcb' # tcbs) - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! n) \<and> tcbp = (tcb' # tcbs) ! Suc n) \<and> (if tcbp = last (tcb' # tcbs) then getNext tcb = NULL else \<exists>n<length (tcb' # tcbs) - 1. tcbp = (tcb' # tcbs) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! Suc n)) proof (state)
this:
tcbp = tcb'

goal (2 subgoals):
 1. tcbp = tcb' \<Longrightarrow> (if tcbp = hd (tcb' # tcbs) then getPrev tcb = qprev' else \<exists>n<length (tcb' # tcbs) - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! n) \<and> tcbp = (tcb' # tcbs) ! Suc n) \<and> (if tcbp = last (tcb' # tcbs) then getNext tcb = NULL else \<exists>n<length (tcb' # tcbs) - 1. tcbp = (tcb' # tcbs) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! Suc n))
 2. tcbp \<in> set tcbs \<Longrightarrow> (if tcbp = hd (tcb' # tcbs) then getPrev tcb = qprev' else \<exists>n<length (tcb' # tcbs) - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! n) \<and> tcbp = (tcb' # tcbs) ! Suc n) \<and> (if tcbp = last (tcb' # tcbs) then getNext tcb = NULL else \<exists>n<length (tcb' # tcbs) - 1. tcbp = (tcb' # tcbs) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! Suc n)) proof (prove)
using this:
tcbp = tcb'

goal (1 subgoal):
 1. if tcbp = hd (tcb' # tcbs) then getPrev tcb = qprev' else \<exists>n<length (tcb' # tcbs) - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! n) \<and> tcbp = (tcb' # tcbs) ! Suc n proof (prove)
using this:
tcbp = tcb'
tcb_queue_relation getNext getPrev mp (tcb' # tcbs) qprev' qhead'
tcbp \<in> set (tcb' # tcbs)
distinct (tcb' # tcbs)
mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb

goal (1 subgoal):
 1. if tcbp = hd (tcb' # tcbs) then getPrev tcb = qprev' else \<exists>n<length (tcb' # tcbs) - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! n) \<and> tcbp = (tcb' # tcbs) ! Suc n proof (state)
this:
if tcbp = hd (tcb' # tcbs) then getPrev tcb = qprev' else \<exists>n<length (tcb' # tcbs) - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! n) \<and> tcbp = (tcb' # tcbs) ! Suc n

goal (2 subgoals):
 1. tcbp = tcb' \<Longrightarrow> (if tcbp = hd (tcb' # tcbs) then getPrev tcb = qprev' else \<exists>n<length (tcb' # tcbs) - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! n) \<and> tcbp = (tcb' # tcbs) ! Suc n) \<and> (if tcbp = last (tcb' # tcbs) then getNext tcb = NULL else \<exists>n<length (tcb' # tcbs) - 1. tcbp = (tcb' # tcbs) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! Suc n))
 2. tcbp \<in> set tcbs \<Longrightarrow> (if tcbp = hd (tcb' # tcbs) then getPrev tcb = qprev' else \<exists>n<length (tcb' # tcbs) - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! n) \<and> tcbp = (tcb' # tcbs) ! Suc n) \<and> (if tcbp = last (tcb' # tcbs) then getNext tcb = NULL else \<exists>n<length (tcb' # tcbs) - 1. tcbp = (tcb' # tcbs) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! Suc n)) proof (state)
this:
if tcbp = hd (tcb' # tcbs) then getPrev tcb = qprev' else \<exists>n<length (tcb' # tcbs) - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! n) \<and> tcbp = (tcb' # tcbs) ! Suc n

goal (2 subgoals):
 1. tcbp = tcb' \<Longrightarrow> (if tcbp = hd (tcb' # tcbs) then getPrev tcb = qprev' else \<exists>n<length (tcb' # tcbs) - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! n) \<and> tcbp = (tcb' # tcbs) ! Suc n) \<and> (if tcbp = last (tcb' # tcbs) then getNext tcb = NULL else \<exists>n<length (tcb' # tcbs) - 1. tcbp = (tcb' # tcbs) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! Suc n))
 2. tcbp \<in> set tcbs \<Longrightarrow> (if tcbp = hd (tcb' # tcbs) then getPrev tcb = qprev' else \<exists>n<length (tcb' # tcbs) - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! n) \<and> tcbp = (tcb' # tcbs) ! Suc n) \<and> (if tcbp = last (tcb' # tcbs) then getNext tcb = NULL else \<exists>n<length (tcb' # tcbs) - 1. tcbp = (tcb' # tcbs) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! Suc n)) proof (prove)
goal (1 subgoal):
 1. if tcbp = last (tcb' # tcbs) then getNext tcb = NULL else \<exists>n<length (tcb' # tcbs) - 1. tcbp = (tcb' # tcbs) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! Suc n) proof (state)
goal (2 subgoals):
 1. tcbs = [] \<Longrightarrow> if tcbp = last (tcb' # tcbs) then getNext tcb = NULL else \<exists>n<length (tcb' # tcbs) - 1. tcbp = (tcb' # tcbs) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! Suc n)
 2. tcbs \<noteq> [] \<Longrightarrow> if tcbp = last (tcb' # tcbs) then getNext tcb = NULL else \<exists>n<length (tcb' # tcbs) - 1. tcbp = (tcb' # tcbs) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! Suc n) proof (state)
this:
tcbs = []

goal (2 subgoals):
 1. tcbs = [] \<Longrightarrow> if tcbp = last (tcb' # tcbs) then getNext tcb = NULL else \<exists>n<length (tcb' # tcbs) - 1. tcbp = (tcb' # tcbs) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! Suc n)
 2. tcbs \<noteq> [] \<Longrightarrow> if tcbp = last (tcb' # tcbs) then getNext tcb = NULL else \<exists>n<length (tcb' # tcbs) - 1. tcbp = (tcb' # tcbs) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! Suc n) proof (prove)
using this:
tcbs = []

goal (1 subgoal):
 1. if tcbp = last (tcb' # tcbs) then getNext tcb = NULL else \<exists>n<length (tcb' # tcbs) - 1. tcbp = (tcb' # tcbs) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! Suc n) proof (prove)
using this:
tcbs = []
tcbp = tcb'
tcb_queue_relation getNext getPrev mp (tcb' # tcbs) qprev' qhead'
tcbp \<in> set (tcb' # tcbs)
distinct (tcb' # tcbs)
mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb

goal (1 subgoal):
 1. if tcbp = last (tcb' # tcbs) then getNext tcb = NULL else \<exists>n<length (tcb' # tcbs) - 1. tcbp = (tcb' # tcbs) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! Suc n) proof (state)
this:
if tcbp = last (tcb' # tcbs) then getNext tcb = NULL else \<exists>n<length (tcb' # tcbs) - 1. tcbp = (tcb' # tcbs) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! Suc n)

goal (1 subgoal):
 1. tcbs \<noteq> [] \<Longrightarrow> if tcbp = last (tcb' # tcbs) then getNext tcb = NULL else \<exists>n<length (tcb' # tcbs) - 1. tcbp = (tcb' # tcbs) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! Suc n) proof (state)
goal (1 subgoal):
 1. tcbs \<noteq> [] \<Longrightarrow> if tcbp = last (tcb' # tcbs) then getNext tcb = NULL else \<exists>n<length (tcb' # tcbs) - 1. tcbp = (tcb' # tcbs) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! Suc n) proof (state)
this:
tcbs \<noteq> []

goal (1 subgoal):
 1. tcbs \<noteq> [] \<Longrightarrow> if tcbp = last (tcb' # tcbs) then getNext tcb = NULL else \<exists>n<length (tcb' # tcbs) - 1. tcbp = (tcb' # tcbs) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! Suc n) proof (prove)
using this:
tcbs \<noteq> []

goal (1 subgoal):
 1. tcbp \<noteq> last tcbs proof (prove)
using this:
tcbs \<noteq> []
tcbp = tcb'
tcb_queue_relation getNext getPrev mp (tcb' # tcbs) qprev' qhead'
tcbp \<in> set (tcb' # tcbs)
distinct (tcb' # tcbs)

goal (1 subgoal):
 1. tcbp \<noteq> last tcbs proof (state)
this:
tcbp \<noteq> last tcbs

goal (1 subgoal):
 1. tcbs \<noteq> [] \<Longrightarrow> if tcbp = last (tcb' # tcbs) then getNext tcb = NULL else \<exists>n<length (tcb' # tcbs) - 1. tcbp = (tcb' # tcbs) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! Suc n) proof (prove)
using this:
tcbp \<noteq> last tcbs

goal (1 subgoal):
 1. if tcbp = last (tcb' # tcbs) then getNext tcb = NULL else \<exists>n<length (tcb' # tcbs) - 1. tcbp = (tcb' # tcbs) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! Suc n) proof (prove)
using this:
tcbp \<noteq> last tcbs
tcbs \<noteq> []
tcbp = tcb'
tcb_queue_relation getNext getPrev mp (tcb' # tcbs) qprev' qhead'
tcbp \<in> set (tcb' # tcbs)
distinct (tcb' # tcbs)
mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb

goal (1 subgoal):
 1. if tcbp = last (tcb' # tcbs) then getNext tcb = NULL else \<exists>n<length (tcb' # tcbs) - 1. tcbp = (tcb' # tcbs) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! Suc n) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb' \<noteq> last tcbs; tcbs \<noteq> []; tcbp = tcb'; qhead' = tcb_ptr_to_ctcb_ptr tcb'; tcb' \<notin> set tcbs; distinct tcbs; mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb; tcb_queue_relation getNext getPrev mp tcbs (tcb_ptr_to_ctcb_ptr tcb') (getNext tcb); qprev' = getPrev tcb\<rbrakk> \<Longrightarrow> \<exists>n<length tcbs. tcb' = (tcb' # tcbs) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr (tcbs ! n) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb' \<noteq> last tcbs; tcbs \<noteq> []; tcbp = tcb'; qhead' = tcb_ptr_to_ctcb_ptr tcb'; tcb' \<notin> set tcbs; distinct tcbs; mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb; tcb_queue_relation getNext getPrev mp tcbs (tcb_ptr_to_ctcb_ptr tcb') (getNext tcb); qprev' = getPrev tcb\<rbrakk> \<Longrightarrow> 0 < length tcbs \<and> tcb' = (tcb' # tcbs) ! 0 \<and> getNext tcb = tcb_ptr_to_ctcb_ptr (tcbs ! 0) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb' \<noteq> last tcbs; tcbs \<noteq> []; tcbp = tcb'; qhead' = tcb_ptr_to_ctcb_ptr tcb'; tcb' \<notin> set tcbs; distinct tcbs; mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb; tcb_queue_relation getNext getPrev mp tcbs (tcb_ptr_to_ctcb_ptr tcb') (getNext tcb); qprev' = getPrev tcb\<rbrakk> \<Longrightarrow> getNext tcb = tcb_ptr_to_ctcb_ptr (tcbs ! 0) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>tcb' \<noteq> last tcbs; tcbs \<noteq> []; tcbp = tcb'; qhead' = tcb_ptr_to_ctcb_ptr tcb'; tcb' \<notin> set tcbs; distinct tcbs; mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb; tcb_queue_relation getNext getPrev mp tcbs (tcb_ptr_to_ctcb_ptr tcb') (getNext tcb); qprev' = getPrev tcb; tcbs = []\<rbrakk> \<Longrightarrow> getNext tcb = tcb_ptr_to_ctcb_ptr (tcbs ! 0)
 2. \<And>a list. \<lbrakk>tcb' \<noteq> last tcbs; tcbs \<noteq> []; tcbp = tcb'; qhead' = tcb_ptr_to_ctcb_ptr tcb'; tcb' \<notin> set tcbs; distinct tcbs; mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb; tcb_queue_relation getNext getPrev mp tcbs (tcb_ptr_to_ctcb_ptr tcb') (getNext tcb); qprev' = getPrev tcb; tcbs = a # list\<rbrakk> \<Longrightarrow> getNext tcb = tcb_ptr_to_ctcb_ptr (tcbs ! 0) proof (prove)
goal:
No subgoals! proof (state)
this:
if tcbp = last (tcb' # tcbs) then getNext tcb = NULL else \<exists>n<length (tcb' # tcbs) - 1. tcbp = (tcb' # tcbs) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! Suc n)

goal:
No subgoals! proof (state)
this:
if tcbp = last (tcb' # tcbs) then getNext tcb = NULL else \<exists>n<length (tcb' # tcbs) - 1. tcbp = (tcb' # tcbs) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! Suc n)

goal (2 subgoals):
 1. tcbp = tcb' \<Longrightarrow> (if tcbp = hd (tcb' # tcbs) then getPrev tcb = qprev' else \<exists>n<length (tcb' # tcbs) - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! n) \<and> tcbp = (tcb' # tcbs) ! Suc n) \<and> (if tcbp = last (tcb' # tcbs) then getNext tcb = NULL else \<exists>n<length (tcb' # tcbs) - 1. tcbp = (tcb' # tcbs) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! Suc n))
 2. tcbp \<in> set tcbs \<Longrightarrow> (if tcbp = hd (tcb' # tcbs) then getPrev tcb = qprev' else \<exists>n<length (tcb' # tcbs) - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! n) \<and> tcbp = (tcb' # tcbs) ! Suc n) \<and> (if tcbp = last (tcb' # tcbs) then getNext tcb = NULL else \<exists>n<length (tcb' # tcbs) - 1. tcbp = (tcb' # tcbs) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! Suc n)) proof (chain)
picking this:
if tcbp = hd (tcb' # tcbs) then getPrev tcb = qprev' else \<exists>n<length (tcb' # tcbs) - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! n) \<and> tcbp = (tcb' # tcbs) ! Suc n
if tcbp = last (tcb' # tcbs) then getNext tcb = NULL else \<exists>n<length (tcb' # tcbs) - 1. tcbp = (tcb' # tcbs) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! Suc n) proof (prove)
using this:
if tcbp = hd (tcb' # tcbs) then getPrev tcb = qprev' else \<exists>n<length (tcb' # tcbs) - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! n) \<and> tcbp = (tcb' # tcbs) ! Suc n
if tcbp = last (tcb' # tcbs) then getNext tcb = NULL else \<exists>n<length (tcb' # tcbs) - 1. tcbp = (tcb' # tcbs) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! Suc n)

goal (1 subgoal):
 1. (if tcbp = hd (tcb' # tcbs) then getPrev tcb = qprev' else \<exists>n<length (tcb' # tcbs) - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! n) \<and> tcbp = (tcb' # tcbs) ! Suc n) \<and> (if tcbp = last (tcb' # tcbs) then getNext tcb = NULL else \<exists>n<length (tcb' # tcbs) - 1. tcbp = (tcb' # tcbs) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! Suc n)) proof (state)
this:
(if tcbp = hd (tcb' # tcbs) then getPrev tcb = qprev' else \<exists>n<length (tcb' # tcbs) - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! n) \<and> tcbp = (tcb' # tcbs) ! Suc n) \<and> (if tcbp = last (tcb' # tcbs) then getNext tcb = NULL else \<exists>n<length (tcb' # tcbs) - 1. tcbp = (tcb' # tcbs) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! Suc n))

goal (1 subgoal):
 1. tcbp \<in> set tcbs \<Longrightarrow> (if tcbp = hd (tcb' # tcbs) then getPrev tcb = qprev' else \<exists>n<length (tcb' # tcbs) - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! n) \<and> tcbp = (tcb' # tcbs) ! Suc n) \<and> (if tcbp = last (tcb' # tcbs) then getNext tcb = NULL else \<exists>n<length (tcb' # tcbs) - 1. tcbp = (tcb' # tcbs) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! Suc n)) proof (state)
goal (1 subgoal):
 1. tcbp \<in> set tcbs \<Longrightarrow> (if tcbp = hd (tcb' # tcbs) then getPrev tcb = qprev' else \<exists>n<length (tcb' # tcbs) - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! n) \<and> tcbp = (tcb' # tcbs) ! Suc n) \<and> (if tcbp = last (tcb' # tcbs) then getNext tcb = NULL else \<exists>n<length (tcb' # tcbs) - 1. tcbp = (tcb' # tcbs) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! Suc n)) proof (state)
this:
tcbp \<in> set tcbs

goal (1 subgoal):
 1. tcbp \<in> set tcbs \<Longrightarrow> (if tcbp = hd (tcb' # tcbs) then getPrev tcb = qprev' else \<exists>n<length (tcb' # tcbs) - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! n) \<and> tcbp = (tcb' # tcbs) ! Suc n) \<and> (if tcbp = last (tcb' # tcbs) then getNext tcb = NULL else \<exists>n<length (tcb' # tcbs) - 1. tcbp = (tcb' # tcbs) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! Suc n)) proof (prove)
goal (1 subgoal):
 1. (\<And>tcb2. \<lbrakk>mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2; tcb_queue_relation getNext getPrev mp tcbs (tcb_ptr_to_ctcb_ptr tcb') (getNext tcb2)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
using this:
tcb_queue_relation getNext getPrev mp (tcb' # tcbs) qprev' qhead'
tcbp \<in> set (tcb' # tcbs)
distinct (tcb' # tcbs)

goal (1 subgoal):
 1. (\<And>tcb2. \<lbrakk>mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2; tcb_queue_relation getNext getPrev mp tcbs (tcb_ptr_to_ctcb_ptr tcb') (getNext tcb2)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
mp (tcb_ptr_to_ctcb_ptr tcb') = Some tcb2
tcb_queue_relation getNext getPrev mp tcbs (tcb_ptr_to_ctcb_ptr tcb') (getNext tcb2)

goal (1 subgoal):
 1. tcbp \<in> set tcbs \<Longrightarrow> (if tcbp = hd (tcb' # tcbs) then getPrev tcb = qprev' else \<exists>n<length (tcb' # tcbs) - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! n) \<and> tcbp = (tcb' # tcbs) ! Suc n) \<and> (if tcbp = last (tcb' # tcbs) then getNext tcb = NULL else \<exists>n<length (tcb' # tcbs) - 1. tcbp = (tcb' # tcbs) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! Suc n)) proof (prove)
goal (1 subgoal):
 1. (if tcbp = hd tcbs then getPrev tcb = tcb_ptr_to_ctcb_ptr tcb' else \<exists>n<length tcbs - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr (tcbs ! n) \<and> tcbp = tcbs ! Suc n) \<and> (if tcbp = last tcbs then getNext tcb = NULL else \<exists>n<length tcbs - 1. tcbp = tcbs ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr (tcbs ! Suc n)) proof (state)
goal (3 subgoals):
 1. tcb_queue_relation getNext getPrev mp tcbs (tcb_ptr_to_ctcb_ptr tcb') ?qhead
 2. tcbp \<in> set tcbs
 3. distinct tcbs proof (chain)
picking this:
tcb_queue_relation getNext getPrev mp (tcb' # tcbs) qprev' qhead'
tcbp \<in> set (tcb' # tcbs)
distinct (tcb' # tcbs) proof (prove)
using this:
tcb_queue_relation getNext getPrev mp (tcb' # tcbs) qprev' qhead'
tcbp \<in> set (tcb' # tcbs)
distinct (tcb' # tcbs)

goal (1 subgoal):
 1. distinct tcbs proof (state)
this:
distinct tcbs

goal (2 subgoals):
 1. tcb_queue_relation getNext getPrev mp tcbs (tcb_ptr_to_ctcb_ptr tcb') ?qhead
 2. tcbp \<in> set tcbs proof (state)
this:
(if tcbp = hd tcbs then getPrev tcb = tcb_ptr_to_ctcb_ptr tcb' else \<exists>n<length tcbs - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr (tcbs ! n) \<and> tcbp = tcbs ! Suc n) \<and> (if tcbp = last tcbs then getNext tcb = NULL else \<exists>n<length tcbs - 1. tcbp = tcbs ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr (tcbs ! Suc n))

goal (1 subgoal):
 1. tcbp \<in> set tcbs \<Longrightarrow> (if tcbp = hd (tcb' # tcbs) then getPrev tcb = qprev' else \<exists>n<length (tcb' # tcbs) - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! n) \<and> tcbp = (tcb' # tcbs) ! Suc n) \<and> (if tcbp = last (tcb' # tcbs) then getNext tcb = NULL else \<exists>n<length (tcb' # tcbs) - 1. tcbp = (tcb' # tcbs) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! Suc n)) proof (chain)
picking this:
tcbp \<in> set tcbs
tcb_queue_relation getNext getPrev mp (tcb' # tcbs) qprev' qhead'
tcbp \<in> set (tcb' # tcbs)
distinct (tcb' # tcbs) proof (prove)
using this:
tcbp \<in> set tcbs
tcb_queue_relation getNext getPrev mp (tcb' # tcbs) qprev' qhead'
tcbp \<in> set (tcb' # tcbs)
distinct (tcb' # tcbs)

goal (1 subgoal):
 1. tcbp \<noteq> tcb' proof (state)
this:
tcbp \<noteq> tcb'

goal (1 subgoal):
 1. tcbp \<in> set tcbs \<Longrightarrow> (if tcbp = hd (tcb' # tcbs) then getPrev tcb = qprev' else \<exists>n<length (tcb' # tcbs) - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! n) \<and> tcbp = (tcb' # tcbs) ! Suc n) \<and> (if tcbp = last (tcb' # tcbs) then getNext tcb = NULL else \<exists>n<length (tcb' # tcbs) - 1. tcbp = (tcb' # tcbs) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! Suc n)) proof (chain)
picking this:
tcbp \<in> set tcbs proof (prove)
using this:
tcbp \<in> set tcbs

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

goal (1 subgoal):
 1. tcbp \<in> set tcbs \<Longrightarrow> (if tcbp = hd (tcb' # tcbs) then getPrev tcb = qprev' else \<exists>n<length (tcb' # tcbs) - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! n) \<and> tcbp = (tcb' # tcbs) ! Suc n) \<and> (if tcbp = last (tcb' # tcbs) then getNext tcb = NULL else \<exists>n<length (tcb' # tcbs) - 1. tcbp = (tcb' # tcbs) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! Suc n)) proof (prove)
using this:
tcbs \<noteq> []

goal (1 subgoal):
 1. hd tcbs = tcbs ! 0 proof (state)
this:
hd tcbs = tcbs ! 0

goal (1 subgoal):
 1. tcbp \<in> set tcbs \<Longrightarrow> (if tcbp = hd (tcb' # tcbs) then getPrev tcb = qprev' else \<exists>n<length (tcb' # tcbs) - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! n) \<and> tcbp = (tcb' # tcbs) ! Suc n) \<and> (if tcbp = last (tcb' # tcbs) then getNext tcb = NULL else \<exists>n<length (tcb' # tcbs) - 1. tcbp = (tcb' # tcbs) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! Suc n)) proof (prove)
goal (1 subgoal):
 1. (if tcbp = hd (tcb' # tcbs) then getPrev tcb = qprev' else \<exists>n<length (tcb' # tcbs) - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! n) \<and> tcbp = (tcb' # tcbs) ! Suc n) \<and> (if tcbp = last (tcb' # tcbs) then getNext tcb = NULL else \<exists>n<length (tcb' # tcbs) - 1. tcbp = (tcb' # tcbs) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! Suc n)) proof (state)
goal (2 subgoals):
 1. if tcbp = hd (tcb' # tcbs) then getPrev tcb = qprev' else \<exists>n<length (tcb' # tcbs) - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! n) \<and> tcbp = (tcb' # tcbs) ! Suc n
 2. if tcbp = last (tcb' # tcbs) then getNext tcb = NULL else \<exists>n<length (tcb' # tcbs) - 1. tcbp = (tcb' # tcbs) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! Suc n) proof (prove)
goal (1 subgoal):
 1. if tcbp = hd (tcb' # tcbs) then getPrev tcb = qprev' else \<exists>n<length (tcb' # tcbs) - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! n) \<and> tcbp = (tcb' # tcbs) ! Suc n proof (prove)
using this:
if tcbp = hd tcbs then getPrev tcb = tcb_ptr_to_ctcb_ptr tcb' else \<exists>n<length tcbs - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr (tcbs ! n) \<and> tcbp = tcbs ! Suc n
tcbp \<noteq> tcb'
hd tcbs = tcbs ! 0
tcbs \<noteq> []

goal (1 subgoal):
 1. if tcbp = hd (tcb' # tcbs) then getPrev tcb = qprev' else \<exists>n<length (tcb' # tcbs) - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! n) \<and> tcbp = (tcb' # tcbs) ! Suc n proof (prove)
goal (2 subgoals):
 1. \<lbrakk>tcbs ! 0 \<noteq> tcb'; hd tcbs = tcbs ! 0; tcbs \<noteq> []; tcbp = tcbs ! 0; getPrev tcb = tcb_ptr_to_ctcb_ptr tcb'\<rbrakk> \<Longrightarrow> \<exists>n<length tcbs. tcb' = (tcb' # tcbs) ! n \<and> tcbs ! 0 = tcbs ! n
 2. \<And>n. \<lbrakk>tcbs ! Suc n \<noteq> tcb'; hd tcbs = tcbs ! 0; tcbs \<noteq> []; tcbs ! Suc n \<noteq> tcbs ! 0; n < length tcbs - Suc 0; getPrev tcb = tcb_ptr_to_ctcb_ptr (tcbs ! n); tcbp = tcbs ! Suc n\<rbrakk> \<Longrightarrow> \<exists>na<length tcbs. tcbs ! n = (tcb' # tcbs) ! na \<and> tcbs ! Suc n = tcbs ! na proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>tcbs ! Suc n \<noteq> tcb'; hd tcbs = tcbs ! 0; tcbs \<noteq> []; tcbs ! Suc n \<noteq> tcbs ! 0; n < length tcbs - Suc 0; getPrev tcb = tcb_ptr_to_ctcb_ptr (tcbs ! n); tcbp = tcbs ! Suc n\<rbrakk> \<Longrightarrow> \<exists>na<length tcbs. tcbs ! n = (tcb' # tcbs) ! na \<and> tcbs ! Suc n = tcbs ! na proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>tcbs ! Suc n \<noteq> tcb'; hd tcbs = tcbs ! 0; tcbs \<noteq> []; tcbs ! Suc n \<noteq> tcbs ! 0; n < length tcbs - Suc 0; getPrev tcb = tcb_ptr_to_ctcb_ptr (tcbs ! n); tcbp = tcbs ! Suc n\<rbrakk> \<Longrightarrow> Suc n < length tcbs \<and> tcbs ! n = (tcb' # tcbs) ! Suc n \<and> tcbs ! Suc n = tcbs ! Suc n proof (prove)
goal:
No subgoals! proof (state)
this:
if tcbp = hd (tcb' # tcbs) then getPrev tcb = qprev' else \<exists>n<length (tcb' # tcbs) - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! n) \<and> tcbp = (tcb' # tcbs) ! Suc n

goal (1 subgoal):
 1. if tcbp = last (tcb' # tcbs) then getNext tcb = NULL else \<exists>n<length (tcb' # tcbs) - 1. tcbp = (tcb' # tcbs) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! Suc n) proof (state)
goal (1 subgoal):
 1. if tcbp = last (tcb' # tcbs) then getNext tcb = NULL else \<exists>n<length (tcb' # tcbs) - 1. tcbp = (tcb' # tcbs) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! Suc n) proof (prove)
goal (1 subgoal):
 1. if tcbp = last (tcb' # tcbs) then getNext tcb = NULL else \<exists>n<length (tcb' # tcbs) - 1. tcbp = (tcb' # tcbs) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! Suc n) proof (prove)
using this:
if tcbp = last tcbs then getNext tcb = NULL else \<exists>n<length tcbs - 1. tcbp = tcbs ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr (tcbs ! Suc n)
tcbp \<noteq> tcb'
hd tcbs = tcbs ! 0
tcbs \<noteq> []

goal (1 subgoal):
 1. if tcbp = last (tcb' # tcbs) then getNext tcb = NULL else \<exists>n<length (tcb' # tcbs) - 1. tcbp = (tcb' # tcbs) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! Suc n) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>tcbs ! n \<noteq> tcb'; hd tcbs = tcbs ! 0; tcbs \<noteq> []; tcbs ! n \<noteq> last tcbs; n < length tcbs - Suc 0; getNext tcb = tcb_ptr_to_ctcb_ptr (tcbs ! Suc n); tcbp = tcbs ! n\<rbrakk> \<Longrightarrow> \<exists>na<length tcbs. tcbs ! n = (tcb' # tcbs) ! na \<and> tcbs ! Suc n = tcbs ! na proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>tcbs ! n \<noteq> tcb'; hd tcbs = tcbs ! 0; tcbs \<noteq> []; tcbs ! n \<noteq> last tcbs; n < length tcbs - Suc 0; getNext tcb = tcb_ptr_to_ctcb_ptr (tcbs ! Suc n); tcbp = tcbs ! n\<rbrakk> \<Longrightarrow> Suc n < length tcbs \<and> tcbs ! n = (tcb' # tcbs) ! Suc n \<and> tcbs ! Suc n = tcbs ! Suc n proof (prove)
goal:
No subgoals! proof (state)
this:
if tcbp = last (tcb' # tcbs) then getNext tcb = NULL else \<exists>n<length (tcb' # tcbs) - 1. tcbp = (tcb' # tcbs) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! Suc n)

goal:
No subgoals! proof (state)
this:
(if tcbp = hd (tcb' # tcbs) then getPrev tcb = qprev' else \<exists>n<length (tcb' # tcbs) - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! n) \<and> tcbp = (tcb' # tcbs) ! Suc n) \<and> (if tcbp = last (tcb' # tcbs) then getNext tcb = NULL else \<exists>n<length (tcb' # tcbs) - 1. tcbp = (tcb' # tcbs) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! Suc n))

goal:
No subgoals! proof (state)
this:
(if tcbp = hd (tcb' # tcbs) then getPrev tcb = qprev' else \<exists>n<length (tcb' # tcbs) - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! n) \<and> tcbp = (tcb' # tcbs) ! Suc n) \<and> (if tcbp = last (tcb' # tcbs) then getNext tcb = NULL else \<exists>n<length (tcb' # tcbs) - 1. tcbp = (tcb' # tcbs) ! n \<and> getNext tcb = tcb_ptr_to_ctcb_ptr ((tcb' # tcbs) ! Suc n))

goal:
No subgoals!