theory TcbQueue_C

lemma tcb_queue_singleton_iff:
  assumes queue_rel: "tcb_queue_relation getNext getPrev mp queue NULL qhead"
  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"
  shows    "(queue = [tcbp]) = (getNext tcb = NULL \<and> getPrev tcb = NULL)" proof (rule iffI) assume "queue = [tcbp]" thus "(getNext tcb = NULL \<and> getPrev tcb = NULL)" using queue_rel cs_tcb by clarsimp next assume asms: "getNext tcb = NULL \<and> getPrev tcb = NULL" hence "hd queue = tcbp" using queue_rel valid_ntfn in_queue cs_tcb apply - apply (drule (3) tcb_queueD) apply (rule classical) apply clarsimp apply (cut_tac x = "queue ! n" in bspec [OF tcb_queue_relation_not_NULL [OF  queue_rel valid_ntfn(1)]]) apply clarsimp apply simp done moreover have "last queue = tcbp" using queue_rel valid_ntfn in_queue cs_tcb asms apply - apply (drule (3) tcb_queueD) apply (rule classical) apply clarsimp apply (cut_tac x = "queue ! Suc n" in bspec [OF tcb_queue_relation_not_NULL [OF  queue_rel valid_ntfn(1)]]) apply clarsimp apply simp done moreover have "queue \<noteq> []" using in_queue by clarsimp ultimately show "queue = [tcbp]" using valid_ntfn in_queue apply clarsimp apply (simp add: hd_conv_nth last_conv_nth nth_eq_iff_index_eq) apply (cases queue) apply simp apply simp done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (queue = [tcbp]) = (getNext tcb = NULL \<and> getPrev tcb = NULL) proof (state)
goal (2 subgoals):
 1. queue = [tcbp] \<Longrightarrow> getNext tcb = NULL \<and> getPrev tcb = NULL
 2. getNext tcb = NULL \<and> getPrev tcb = NULL \<Longrightarrow> queue = [tcbp] proof (state)
this:
queue = [tcbp]

goal (2 subgoals):
 1. queue = [tcbp] \<Longrightarrow> getNext tcb = NULL \<and> getPrev tcb = NULL
 2. getNext tcb = NULL \<and> getPrev tcb = NULL \<Longrightarrow> queue = [tcbp] proof (prove)
using this:
queue = [tcbp]

goal (1 subgoal):
 1. getNext tcb = NULL \<and> getPrev tcb = NULL proof (prove)
using this:
queue = [tcbp]
tcb_queue_relation getNext getPrev mp queue NULL qhead
mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb

goal (1 subgoal):
 1. getNext tcb = NULL \<and> getPrev tcb = NULL proof (state)
this:
getNext tcb = NULL \<and> getPrev tcb = NULL

goal (1 subgoal):
 1. getNext tcb = NULL \<and> getPrev tcb = NULL \<Longrightarrow> queue = [tcbp] proof (state)
goal (1 subgoal):
 1. getNext tcb = NULL \<and> getPrev tcb = NULL \<Longrightarrow> queue = [tcbp] proof (state)
this:
getNext tcb = NULL \<and> getPrev tcb = NULL

goal (1 subgoal):
 1. getNext tcb = NULL \<and> getPrev tcb = NULL \<Longrightarrow> queue = [tcbp] proof (prove)
using this:
getNext tcb = NULL \<and> getPrev tcb = NULL

goal (1 subgoal):
 1. hd queue = tcbp proof (prove)
using this:
getNext tcb = NULL \<and> getPrev tcb = NULL
tcb_queue_relation getNext getPrev mp queue NULL qhead
\<forall>t\<in>set queue. tcb_at' t s
distinct queue
tcbp \<in> set queue
mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb

goal (1 subgoal):
 1. hd queue = tcbp proof (prove)
goal (1 subgoal):
 1. \<lbrakk>getNext tcb = NULL \<and> getPrev tcb = NULL; tcb_queue_relation getNext getPrev mp queue NULL qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb\<rbrakk> \<Longrightarrow> hd queue = tcbp proof (prove)
goal (1 subgoal):
 1. \<lbrakk>getNext tcb = NULL \<and> getPrev tcb = NULL; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; (if tcbp = hd queue then getPrev tcb = NULL 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))\<rbrakk> \<Longrightarrow> hd queue = tcbp proof (prove)
goal (1 subgoal):
 1. \<lbrakk>getNext tcb = NULL \<and> getPrev tcb = NULL; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; (if tcbp = hd queue then getPrev tcb = NULL 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)); hd queue \<noteq> tcbp\<rbrakk> \<Longrightarrow> hd queue = tcbp proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>t\<in>set queue. tcb_at' t s; distinct queue; mp (tcb_ptr_to_ctcb_ptr (queue ! Suc n)) = Some tcb; hd queue \<noteq> queue ! Suc n; getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! n); getPrev tcb = tcb_ptr_to_ctcb_ptr (queue ! n); if queue ! Suc n = last queue then getNext tcb = NULL else \<exists>na<length queue - 1. queue ! Suc n = queue ! na \<and> getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc na); n < length queue - Suc 0; NULL = tcb_ptr_to_ctcb_ptr (queue ! n); tcbp = queue ! Suc n\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>\<forall>t\<in>set queue. tcb_at' t s; distinct queue; mp (tcb_ptr_to_ctcb_ptr (queue ! Suc n)) = Some tcb; hd queue \<noteq> queue ! Suc n; getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! n); getPrev tcb = tcb_ptr_to_ctcb_ptr (queue ! n); if queue ! Suc n = last queue then getNext tcb = NULL else \<exists>na<length queue - 1. queue ! Suc n = queue ! na \<and> getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc na); n < length queue - Suc 0; NULL = tcb_ptr_to_ctcb_ptr (queue ! n); tcbp = queue ! Suc n\<rbrakk> \<Longrightarrow> queue ! n \<in> set queue
 2. \<And>n. \<lbrakk>\<forall>t\<in>set queue. tcb_at' t s; distinct queue; mp (tcb_ptr_to_ctcb_ptr (queue ! Suc n)) = Some tcb; hd queue \<noteq> queue ! Suc n; getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! n); getPrev tcb = tcb_ptr_to_ctcb_ptr (queue ! n); if queue ! Suc n = last queue then getNext tcb = NULL else \<exists>na<length queue - 1. queue ! Suc n = queue ! na \<and> getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc na); n < length queue - Suc 0; NULL = tcb_ptr_to_ctcb_ptr (queue ! n); tcbp = queue ! Suc n; tcb_ptr_to_ctcb_ptr (queue ! n) \<noteq> NULL\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>t\<in>set queue. tcb_at' t s; distinct queue; mp (tcb_ptr_to_ctcb_ptr (queue ! Suc n)) = Some tcb; hd queue \<noteq> queue ! Suc n; getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! n); getPrev tcb = tcb_ptr_to_ctcb_ptr (queue ! n); if queue ! Suc n = last queue then getNext tcb = NULL else \<exists>na<length queue - 1. queue ! Suc n = queue ! na \<and> getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc na); n < length queue - Suc 0; NULL = tcb_ptr_to_ctcb_ptr (queue ! n); tcbp = queue ! Suc n; tcb_ptr_to_ctcb_ptr (queue ! n) \<noteq> NULL\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
hd queue = tcbp

goal (1 subgoal):
 1. getNext tcb = NULL \<and> getPrev tcb = NULL \<Longrightarrow> queue = [tcbp] proof (state)
this:
hd queue = tcbp

goal (1 subgoal):
 1. getNext tcb = NULL \<and> getPrev tcb = NULL \<Longrightarrow> queue = [tcbp] proof (prove)
goal (1 subgoal):
 1. last queue = tcbp proof (prove)
using this:
tcb_queue_relation getNext getPrev mp queue NULL qhead
\<forall>t\<in>set queue. tcb_at' t s
distinct queue
tcbp \<in> set queue
mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb
getNext tcb = NULL \<and> getPrev tcb = NULL

goal (1 subgoal):
 1. last queue = tcbp proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_queue_relation getNext getPrev mp queue NULL qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; getNext tcb = NULL \<and> getPrev tcb = NULL\<rbrakk> \<Longrightarrow> last queue = tcbp proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>t\<in>set queue. tcb_at' t s; distinct queue; tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; getNext tcb = NULL \<and> getPrev tcb = NULL; (if tcbp = hd queue then getPrev tcb = NULL 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))\<rbrakk> \<Longrightarrow> last queue = tcbp proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>t\<in>set queue. tcb_at' t s; distinct queue; tcbp \<in> set queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; getNext tcb = NULL \<and> getPrev tcb = NULL; (if tcbp = hd queue then getPrev tcb = NULL 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)); last queue \<noteq> tcbp\<rbrakk> \<Longrightarrow> last queue = tcbp proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>t\<in>set queue. tcb_at' t s; distinct queue; mp (tcb_ptr_to_ctcb_ptr (queue ! n)) = Some tcb; last queue \<noteq> queue ! n; getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n); getPrev tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n); if queue ! n = hd queue then getPrev tcb = NULL else \<exists>na<length queue - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr (queue ! na) \<and> queue ! n = queue ! Suc na; n < length queue - Suc 0; NULL = tcb_ptr_to_ctcb_ptr (queue ! Suc n); tcbp = queue ! n\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>\<forall>t\<in>set queue. tcb_at' t s; distinct queue; mp (tcb_ptr_to_ctcb_ptr (queue ! n)) = Some tcb; last queue \<noteq> queue ! n; getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n); getPrev tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n); if queue ! n = hd queue then getPrev tcb = NULL else \<exists>na<length queue - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr (queue ! na) \<and> queue ! n = queue ! Suc na; n < length queue - Suc 0; NULL = tcb_ptr_to_ctcb_ptr (queue ! Suc n); tcbp = queue ! n\<rbrakk> \<Longrightarrow> queue ! Suc n \<in> set queue
 2. \<And>n. \<lbrakk>\<forall>t\<in>set queue. tcb_at' t s; distinct queue; mp (tcb_ptr_to_ctcb_ptr (queue ! n)) = Some tcb; last queue \<noteq> queue ! n; getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n); getPrev tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n); if queue ! n = hd queue then getPrev tcb = NULL else \<exists>na<length queue - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr (queue ! na) \<and> queue ! n = queue ! Suc na; n < length queue - Suc 0; NULL = tcb_ptr_to_ctcb_ptr (queue ! Suc n); tcbp = queue ! n; tcb_ptr_to_ctcb_ptr (queue ! Suc n) \<noteq> NULL\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>t\<in>set queue. tcb_at' t s; distinct queue; mp (tcb_ptr_to_ctcb_ptr (queue ! n)) = Some tcb; last queue \<noteq> queue ! n; getNext tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n); getPrev tcb = tcb_ptr_to_ctcb_ptr (queue ! Suc n); if queue ! n = hd queue then getPrev tcb = NULL else \<exists>na<length queue - 1. getPrev tcb = tcb_ptr_to_ctcb_ptr (queue ! na) \<and> queue ! n = queue ! Suc na; n < length queue - Suc 0; NULL = tcb_ptr_to_ctcb_ptr (queue ! Suc n); tcbp = queue ! n; tcb_ptr_to_ctcb_ptr (queue ! Suc n) \<noteq> NULL\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
last queue = tcbp

goal (1 subgoal):
 1. getNext tcb = NULL \<and> getPrev tcb = NULL \<Longrightarrow> queue = [tcbp] proof (state)
this:
last queue = tcbp

goal (1 subgoal):
 1. getNext tcb = NULL \<and> getPrev tcb = NULL \<Longrightarrow> queue = [tcbp] 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. getNext tcb = NULL \<and> getPrev tcb = NULL \<Longrightarrow> queue = [tcbp] proof (chain)
picking this:
hd queue = tcbp
last queue = tcbp
queue \<noteq> [] proof (prove)
using this:
hd queue = tcbp
last queue = tcbp
queue \<noteq> []

goal (1 subgoal):
 1. queue = [tcbp] proof (prove)
using this:
hd queue = tcbp
last queue = tcbp
queue \<noteq> []
\<forall>t\<in>set queue. tcb_at' t s
distinct queue
tcbp \<in> set queue

goal (1 subgoal):
 1. queue = [tcbp] proof (prove)
goal (1 subgoal):
 1. \<lbrakk>last queue = hd queue; queue \<noteq> []; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; tcbp = hd queue\<rbrakk> \<Longrightarrow> queue = [hd queue] proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length queue \<le> Suc 0; queue \<noteq> []; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; tcbp = queue ! 0\<rbrakk> \<Longrightarrow> queue = [queue ! 0] proof (prove)
goal (2 subgoals):
 1. \<lbrakk>length queue \<le> Suc 0; queue \<noteq> []; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; tcbp = queue ! 0; queue = []\<rbrakk> \<Longrightarrow> queue = [queue ! 0]
 2. \<And>a list. \<lbrakk>length queue \<le> Suc 0; queue \<noteq> []; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; tcbp = queue ! 0; queue = a # list\<rbrakk> \<Longrightarrow> queue = [queue ! 0] proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>length queue \<le> Suc 0; queue \<noteq> []; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; tcbp = queue ! 0; queue = a # list\<rbrakk> \<Longrightarrow> queue = [queue ! 0] proof (prove)
goal:
No subgoals! proof (state)
this:
queue = [tcbp]

goal:
No subgoals!