theory TcbQueue_C

lemma tcb_queue_relation_prev_mask:
  assumes   tq: "tcb_queue_relation getNext getPrev mp queue NULL qhead"
  and valid_ep: "\<forall>t\<in>set queue. tcb_at' t s" "distinct queue"
  and   cs_tcb: "mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb"
  and in_queue: "tcbp \<in> set queue"
  and     bits: "bits \<le> ctcb_size_bits"
  shows "ptr_val (getPrev tcb) && ~~ mask bits = ptr_val (getPrev tcb)" proof (cases "(getPrev tcb) = NULL") case True thus ?thesis by simp next case False hence "ctcb_ptr_to_tcb_ptr (getPrev tcb) \<in> set queue" using assms apply - apply (drule (3) tcb_queueD) apply (clarsimp split: if_split_asm) done with valid_ep(1) have "tcb_at' (ctcb_ptr_to_tcb_ptr (getPrev tcb)) s" .. hence "is_aligned (ctcb_ptr_to_tcb_ptr (getPrev tcb)) tcbBlockSizeBits" by (rule tcb_aligned') hence "is_aligned (ptr_val (getPrev tcb)) ctcb_size_bits" by (rule ctcb_ptr_to_tcb_ptr_aligned) thus ?thesis using bits by (simp add: is_aligned_neg_mask) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ptr_val (getPrev tcb) && ~~ mask bits = ptr_val (getPrev tcb) proof (state)
goal (2 subgoals):
 1. getPrev tcb = NULL \<Longrightarrow> ptr_val (getPrev tcb) && ~~ mask bits = ptr_val (getPrev tcb)
 2. getPrev tcb \<noteq> NULL \<Longrightarrow> ptr_val (getPrev tcb) && ~~ mask bits = ptr_val (getPrev tcb) proof (state)
this:
getPrev tcb = NULL

goal (2 subgoals):
 1. getPrev tcb = NULL \<Longrightarrow> ptr_val (getPrev tcb) && ~~ mask bits = ptr_val (getPrev tcb)
 2. getPrev tcb \<noteq> NULL \<Longrightarrow> ptr_val (getPrev tcb) && ~~ mask bits = ptr_val (getPrev tcb) proof (prove)
using this:
getPrev tcb = NULL

goal (1 subgoal):
 1. ptr_val (getPrev tcb) && ~~ mask bits = ptr_val (getPrev tcb) proof (state)
this:
ptr_val (getPrev tcb) && ~~ mask bits = ptr_val (getPrev tcb)

goal (1 subgoal):
 1. getPrev tcb \<noteq> NULL \<Longrightarrow> ptr_val (getPrev tcb) && ~~ mask bits = ptr_val (getPrev tcb) proof (state)
goal (1 subgoal):
 1. getPrev tcb \<noteq> NULL \<Longrightarrow> ptr_val (getPrev tcb) && ~~ mask bits = ptr_val (getPrev tcb) proof (state)
this:
getPrev tcb \<noteq> NULL

goal (1 subgoal):
 1. getPrev tcb \<noteq> NULL \<Longrightarrow> ptr_val (getPrev tcb) && ~~ mask bits = ptr_val (getPrev tcb) proof (prove)
using this:
getPrev tcb \<noteq> NULL

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

goal (1 subgoal):
 1. ctcb_ptr_to_tcb_ptr (getPrev tcb) \<in> set queue proof (prove)
goal (1 subgoal):
 1. \<lbrakk>getPrev tcb \<noteq> NULL; tcb_queue_relation getNext getPrev mp queue NULL qhead; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcbp \<in> set queue; bits \<le> ctcb_size_bits\<rbrakk> \<Longrightarrow> ctcb_ptr_to_tcb_ptr (getPrev tcb) \<in> set queue proof (prove)
goal (1 subgoal):
 1. \<lbrakk>getPrev tcb \<noteq> NULL; \<forall>t\<in>set queue. tcb_at' t s; distinct queue; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; tcbp \<in> set queue; bits \<le> ctcb_size_bits; (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> ctcb_ptr_to_tcb_ptr (getPrev tcb) \<in> set queue proof (prove)
goal:
No subgoals! proof (state)
this:
ctcb_ptr_to_tcb_ptr (getPrev tcb) \<in> set queue

goal (1 subgoal):
 1. getPrev tcb \<noteq> NULL \<Longrightarrow> ptr_val (getPrev tcb) && ~~ mask bits = ptr_val (getPrev tcb) proof (chain)
picking this:
\<forall>t\<in>set queue. tcb_at' t s
ctcb_ptr_to_tcb_ptr (getPrev tcb) \<in> set queue proof (prove)
using this:
\<forall>t\<in>set queue. tcb_at' t s
ctcb_ptr_to_tcb_ptr (getPrev tcb) \<in> set queue

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

goal (1 subgoal):
 1. getPrev tcb \<noteq> NULL \<Longrightarrow> ptr_val (getPrev tcb) && ~~ mask bits = ptr_val (getPrev tcb) proof (prove)
using this:
tcb_at' (ctcb_ptr_to_tcb_ptr (getPrev tcb)) s

goal (1 subgoal):
 1. is_aligned (ctcb_ptr_to_tcb_ptr (getPrev tcb)) tcbBlockSizeBits proof (state)
this:
is_aligned (ctcb_ptr_to_tcb_ptr (getPrev tcb)) tcbBlockSizeBits

goal (1 subgoal):
 1. getPrev tcb \<noteq> NULL \<Longrightarrow> ptr_val (getPrev tcb) && ~~ mask bits = ptr_val (getPrev tcb) proof (prove)
using this:
is_aligned (ctcb_ptr_to_tcb_ptr (getPrev tcb)) tcbBlockSizeBits

goal (1 subgoal):
 1. is_aligned (ptr_val (getPrev tcb)) ctcb_size_bits proof (state)
this:
is_aligned (ptr_val (getPrev tcb)) ctcb_size_bits

goal (1 subgoal):
 1. getPrev tcb \<noteq> NULL \<Longrightarrow> ptr_val (getPrev tcb) && ~~ mask bits = ptr_val (getPrev tcb) proof (prove)
using this:
is_aligned (ptr_val (getPrev tcb)) ctcb_size_bits

goal (1 subgoal):
 1. ptr_val (getPrev tcb) && ~~ mask bits = ptr_val (getPrev tcb) proof (prove)
using this:
is_aligned (ptr_val (getPrev tcb)) ctcb_size_bits
bits \<le> ctcb_size_bits

goal (1 subgoal):
 1. ptr_val (getPrev tcb) && ~~ mask bits = ptr_val (getPrev tcb) proof (state)
this:
ptr_val (getPrev tcb) && ~~ mask bits = ptr_val (getPrev tcb)

goal:
No subgoals!