theory TcbQueue_C

lemma tcb_queue_valid_ptrsD:
  assumes in_queue: "tcbp \<in> set queue"
  and        rf_sr: "(s, s') \<in> rf_sr"
  and    valid_ntfn: "\<forall>t\<in>set queue. tcb_at' t s" "distinct queue"
  and    queue_rel: "tcb_queue_relation getNext getPrev (cslift s') queue NULL qhead"
  shows "\<exists>tcb. cslift s' (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb
               \<and> (getPrev tcb \<noteq> NULL \<longrightarrow> s' \<Turnstile>\<^sub>c (getPrev tcb)
                                           \<and> getPrev tcb \<in> tcb_ptr_to_ctcb_ptr ` set queue)
               \<and> (getNext tcb \<noteq> NULL \<longrightarrow> s' \<Turnstile>\<^sub>c (getNext tcb)
                                          \<and>  getNext tcb \<in> tcb_ptr_to_ctcb_ptr ` set queue)" using assms apply - apply (frule (3) tcb_queue_memberD) apply (elim exE) apply (frule (3) tcb_queueD) apply (auto intro!: tcb_at_h_t_valid elim!: bspec split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>tcb. cslift s' (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb \<and> (getPrev tcb \<noteq> NULL \<longrightarrow> s' \<Turnstile>\<^sub>c getPrev tcb \<and> getPrev tcb \<in> tcb_ptr_to_ctcb_ptr ` set queue) \<and> (getNext tcb \<noteq> NULL \<longrightarrow> s' \<Turnstile>\<^sub>c getNext tcb \<and> getNext tcb \<in> tcb_ptr_to_ctcb_ptr ` set queue) proof (prove)
using this:
tcbp \<in> set queue
(s, s') \<in> rf_sr
\<forall>t\<in>set queue. tcb_at' t s
distinct queue
tcb_queue_relation getNext getPrev (cslift s') queue NULL qhead

goal (1 subgoal):
 1. \<exists>tcb. cslift s' (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb \<and> (getPrev tcb \<noteq> NULL \<longrightarrow> s' \<Turnstile>\<^sub>c getPrev tcb \<and> getPrev tcb \<in> tcb_ptr_to_ctcb_ptr ` set queue) \<and> (getNext tcb \<noteq> NULL \<longrightarrow> s' \<Turnstile>\<^sub>c getNext tcb \<and> getNext tcb \<in> tcb_ptr_to_ctcb_ptr ` set queue) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcbp \<in> set queue; (s, s') \<in> rf_sr; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; tcb_queue_relation getNext getPrev (cslift s') queue NULL qhead\<rbrakk> \<Longrightarrow> \<exists>tcb. cslift s' (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb \<and> (getPrev tcb \<noteq> NULL \<longrightarrow> s' \<Turnstile>\<^sub>c getPrev tcb \<and> getPrev tcb \<in> tcb_ptr_to_ctcb_ptr ` set queue) \<and> (getNext tcb \<noteq> NULL \<longrightarrow> s' \<Turnstile>\<^sub>c getNext tcb \<and> getNext tcb \<in> tcb_ptr_to_ctcb_ptr ` set queue) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcbp \<in> set queue; (s, s') \<in> rf_sr; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; tcb_queue_relation getNext getPrev (cslift s') queue NULL qhead; \<exists>tcb. cslift s' (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb\<rbrakk> \<Longrightarrow> \<exists>tcb. cslift s' (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb \<and> (getPrev tcb \<noteq> NULL \<longrightarrow> s' \<Turnstile>\<^sub>c getPrev tcb \<and> getPrev tcb \<in> tcb_ptr_to_ctcb_ptr ` set queue) \<and> (getNext tcb \<noteq> NULL \<longrightarrow> s' \<Turnstile>\<^sub>c getNext tcb \<and> getNext tcb \<in> tcb_ptr_to_ctcb_ptr ` set queue) proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>tcbp \<in> set queue; (s, s') \<in> rf_sr; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; tcb_queue_relation getNext getPrev (cslift s') queue NULL qhead; cslift s' (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb\<rbrakk> \<Longrightarrow> \<exists>tcb. cslift s' (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb \<and> (getPrev tcb \<noteq> NULL \<longrightarrow> s' \<Turnstile>\<^sub>c getPrev tcb \<and> getPrev tcb \<in> tcb_ptr_to_ctcb_ptr ` set queue) \<and> (getNext tcb \<noteq> NULL \<longrightarrow> s' \<Turnstile>\<^sub>c getNext tcb \<and> getNext tcb \<in> tcb_ptr_to_ctcb_ptr ` set queue) proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>tcbp \<in> set queue; (s, s') \<in> rf_sr; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; tcb_queue_relation getNext getPrev (cslift s') queue NULL qhead; cslift s' (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> \<exists>tcb. cslift s' (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb \<and> (getPrev tcb \<noteq> NULL \<longrightarrow> s' \<Turnstile>\<^sub>c getPrev tcb \<and> getPrev tcb \<in> tcb_ptr_to_ctcb_ptr ` set queue) \<and> (getNext tcb \<noteq> NULL \<longrightarrow> s' \<Turnstile>\<^sub>c getNext tcb \<and> getNext tcb \<in> tcb_ptr_to_ctcb_ptr ` set queue) proof (prove)
goal:
No subgoals!