theory TcbQueue_C

lemma cready_queues_relation_not_queue_ptrs:
  assumes rel: "cready_queues_relation mp cq aq"
  and same: "option_map tcbSchedNext_C \<circ> mp' = option_map tcbSchedNext_C \<circ> mp"
  "option_map tcbSchedPrev_C \<circ> mp' = option_map tcbSchedPrev_C \<circ> mp"
  shows "cready_queues_relation mp' cq aq" using rel apply (clarsimp simp: cready_queues_relation_def tcb_queue_relation'_def Let_def all_conj_distrib) apply (drule spec, drule spec, drule mp, (erule conjI)+, assumption) apply clarsimp apply (erule iffD2 [OF tcb_queue_relation_only_next_prev, rotated -1]) apply (rule same) apply (rule same) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cready_queues_relation mp' cq aq proof (prove)
using this:
cready_queues_relation mp cq aq

goal (1 subgoal):
 1. cready_queues_relation mp' cq aq proof (prove)
goal (1 subgoal):
 1. \<And>qdom prio. \<lbrakk>\<forall>qdom prio. UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom \<and> qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom \<and> UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio \<and> prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio \<longrightarrow> StateRelation_C.end_C (cq.[cready_queues_index_to_C qdom prio]) = (if aq (qdom, prio) = [] then NULL else tcb_ptr_to_ctcb_ptr (last (aq (qdom, prio)))) \<and> sched_queue_relation mp (aq (qdom, prio)) NULL (head_C (cq.[cready_queues_index_to_C qdom prio])); \<forall>qdom prio. (UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio \<longrightarrow> qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom \<longrightarrow> UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom \<longrightarrow> \<not> prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio) \<longrightarrow> aq (qdom, prio) = []; UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom; qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom; UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio; prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio\<rbrakk> \<Longrightarrow> sched_queue_relation mp' (aq (qdom, prio)) NULL (head_C (cq.[cready_queues_index_to_C qdom prio])) proof (prove)
goal (1 subgoal):
 1. \<And>qdom prio. \<lbrakk>\<forall>qdom prio. (UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio \<longrightarrow> qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom \<longrightarrow> UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom \<longrightarrow> \<not> prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio) \<longrightarrow> aq (qdom, prio) = []; UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom; qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom; UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio; prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio; StateRelation_C.end_C (cq.[cready_queues_index_to_C qdom prio]) = (if aq (qdom, prio) = [] then NULL else tcb_ptr_to_ctcb_ptr (last (aq (qdom, prio)))) \<and> sched_queue_relation mp (aq (qdom, prio)) NULL (head_C (cq.[cready_queues_index_to_C qdom prio]))\<rbrakk> \<Longrightarrow> sched_queue_relation mp' (aq (qdom, prio)) NULL (head_C (cq.[cready_queues_index_to_C qdom prio])) proof (prove)
goal (1 subgoal):
 1. \<And>qdom prio. \<lbrakk>\<forall>qdom prio. (UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio \<longrightarrow> qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom \<longrightarrow> UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom \<longrightarrow> \<not> prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio) \<longrightarrow> aq (qdom, prio) = []; UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom; qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom; UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio; prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio; StateRelation_C.end_C (cq.[cready_queues_index_to_C qdom prio]) = (if aq (qdom, prio) = [] then NULL else tcb_ptr_to_ctcb_ptr (last (aq (qdom, prio)))); sched_queue_relation mp (aq (qdom, prio)) NULL (head_C (cq.[cready_queues_index_to_C qdom prio]))\<rbrakk> \<Longrightarrow> sched_queue_relation mp' (aq (qdom, prio)) NULL (head_C (cq.[cready_queues_index_to_C qdom prio])) proof (prove)
goal (2 subgoals):
 1. \<And>qdom prio. \<lbrakk>\<forall>qdom prio. (UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio \<longrightarrow> qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom \<longrightarrow> UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom \<longrightarrow> \<not> prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio) \<longrightarrow> aq (qdom, prio) = []; UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom; qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom; UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio; prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio; StateRelation_C.end_C (cq.[cready_queues_index_to_C qdom prio]) = (if aq (qdom, prio) = [] then NULL else tcb_ptr_to_ctcb_ptr (last (aq (qdom, prio))))\<rbrakk> \<Longrightarrow> map_option tcbSchedNext_C \<circ> mp' = map_option tcbSchedNext_C \<circ> mp
 2. \<And>qdom prio. \<lbrakk>\<forall>qdom prio. (UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio \<longrightarrow> qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom \<longrightarrow> UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom \<longrightarrow> \<not> prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio) \<longrightarrow> aq (qdom, prio) = []; UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom; qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom; UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio; prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio; StateRelation_C.end_C (cq.[cready_queues_index_to_C qdom prio]) = (if aq (qdom, prio) = [] then NULL else tcb_ptr_to_ctcb_ptr (last (aq (qdom, prio))))\<rbrakk> \<Longrightarrow> map_option tcbSchedPrev_C \<circ> mp' = map_option tcbSchedPrev_C \<circ> mp proof (prove)
goal (1 subgoal):
 1. \<And>qdom prio. \<lbrakk>\<forall>qdom prio. (UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio \<longrightarrow> qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom \<longrightarrow> UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom \<longrightarrow> \<not> prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio) \<longrightarrow> aq (qdom, prio) = []; UCAST(32 signed \<rightarrow> 8) minDom \<le> qdom; qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom; UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> prio; prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio; StateRelation_C.end_C (cq.[cready_queues_index_to_C qdom prio]) = (if aq (qdom, prio) = [] then NULL else tcb_ptr_to_ctcb_ptr (last (aq (qdom, prio))))\<rbrakk> \<Longrightarrow> map_option tcbSchedPrev_C \<circ> mp' = map_option tcbSchedPrev_C \<circ> mp proof (prove)
goal:
No subgoals!