theory TcbQueue_C

lemma tcb_queue_relation_not_NULL:
  assumes   tq: "tcb_queue_relation getNext getPrev mp queue qprev qhead"
  and valid_ep: "\<forall>t\<in>set queue. tcb_at' t s"
  shows   "\<forall>t \<in> set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL" proof (cases "queue = []") case True thus ?thesis by simp next case False show ?thesis proof (rule ballI, rule notI) fix t assume tq: "t \<in> set queue" and "tcb_ptr_to_ctcb_ptr t = NULL" hence "ctcb_ptr_to_tcb_ptr NULL \<in> set queue" apply - apply (erule subst) apply simp done with valid_ep(1) have "tcb_at' (ctcb_ptr_to_tcb_ptr NULL) s" .. thus False apply - apply (drule tcb_at_not_NULL) apply simp done qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL proof (state)
goal (2 subgoals):
 1. queue = [] \<Longrightarrow> \<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL
 2. queue \<noteq> [] \<Longrightarrow> \<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL proof (state)
this:
queue = []

goal (2 subgoals):
 1. queue = [] \<Longrightarrow> \<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL
 2. queue \<noteq> [] \<Longrightarrow> \<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL proof (prove)
using this:
queue = []

goal (1 subgoal):
 1. \<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL proof (state)
this:
\<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL

goal (1 subgoal):
 1. queue \<noteq> [] \<Longrightarrow> \<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL proof (state)
goal (1 subgoal):
 1. queue \<noteq> [] \<Longrightarrow> \<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL proof (state)
this:
queue \<noteq> []

goal (1 subgoal):
 1. queue \<noteq> [] \<Longrightarrow> \<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL proof (prove)
goal (1 subgoal):
 1. \<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL proof (state)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>t \<in> set queue; tcb_ptr_to_ctcb_ptr t = NULL\<rbrakk> \<Longrightarrow> False proof (state)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>t \<in> set queue; tcb_ptr_to_ctcb_ptr t = NULL\<rbrakk> \<Longrightarrow> False proof (state)
this:
t \<in> set queue
tcb_ptr_to_ctcb_ptr t = NULL

goal (1 subgoal):
 1. \<And>t. \<lbrakk>t \<in> set queue; tcb_ptr_to_ctcb_ptr t = NULL\<rbrakk> \<Longrightarrow> False proof (prove)
using this:
t \<in> set queue
tcb_ptr_to_ctcb_ptr t = NULL

goal (1 subgoal):
 1. ctcb_ptr_to_tcb_ptr NULL \<in> set queue proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t \<in> set queue; tcb_ptr_to_ctcb_ptr t = NULL\<rbrakk> \<Longrightarrow> ctcb_ptr_to_tcb_ptr NULL \<in> set queue proof (prove)
goal (1 subgoal):
 1. t \<in> set queue \<Longrightarrow> ctcb_ptr_to_tcb_ptr (tcb_ptr_to_ctcb_ptr t) \<in> set queue proof (prove)
goal:
No subgoals! proof (state)
this:
ctcb_ptr_to_tcb_ptr NULL \<in> set queue

goal (1 subgoal):
 1. \<And>t. \<lbrakk>t \<in> set queue; tcb_ptr_to_ctcb_ptr t = NULL\<rbrakk> \<Longrightarrow> False proof (chain)
picking this:
\<forall>t\<in>set queue. tcb_at' t s
ctcb_ptr_to_tcb_ptr NULL \<in> set queue proof (prove)
using this:
\<forall>t\<in>set queue. tcb_at' t s
ctcb_ptr_to_tcb_ptr NULL \<in> set queue

goal (1 subgoal):
 1. tcb_at' (ctcb_ptr_to_tcb_ptr NULL) s proof (state)
this:
tcb_at' (ctcb_ptr_to_tcb_ptr NULL) s

goal (1 subgoal):
 1. \<And>t. \<lbrakk>t \<in> set queue; tcb_ptr_to_ctcb_ptr t = NULL\<rbrakk> \<Longrightarrow> False proof (prove)
using this:
tcb_at' (ctcb_ptr_to_tcb_ptr NULL) s

goal (1 subgoal):
 1. False proof (prove)
goal (1 subgoal):
 1. tcb_at' (ctcb_ptr_to_tcb_ptr NULL) s \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. tcb_ptr_to_ctcb_ptr (ctcb_ptr_to_tcb_ptr NULL) \<noteq> NULL \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
False

goal:
No subgoals! proof (state)
this:
\<forall>t\<in>set queue. tcb_ptr_to_ctcb_ptr t \<noteq> NULL

goal:
No subgoals!