theory ADT_C

lemma cready_queues_to_H_correct:
  "cready_queues_relation (clift s) cs as \<Longrightarrow>
   cready_queues_to_H (clift s) cs = as" apply (clarsimp simp: cready_queues_to_H_def cready_queues_relation_def
                   fun_eq_iff) apply (rule the_equality) apply simp apply (clarsimp simp: Let_def) apply (rule_tac hp="clift s" in tcb_queue_rel'_unique, simp_all add: lift_t_NULL) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cready_queues_relation (clift s) cs as \<Longrightarrow> cready_queues_to_H (clift s) cs = as proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<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> (let cqueue = cs.[cready_queues_index_to_C qdom prio] in sched_queue_relation' (clift s) (as (qdom, prio)) (head_C cqueue) (StateRelation_C.end_C cqueue))) \<and> ((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> as (qdom, prio) = []); UCAST(32 signed \<rightarrow> 8) minDom \<le> a; a \<le> UCAST(32 signed \<rightarrow> 8) maxDom; UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> b; b \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio\<rbrakk> \<Longrightarrow> (THE aq. let cqueue = cs.[cready_queues_index_to_C a b] in sched_queue_relation' (clift s) aq (head_C cqueue) (StateRelation_C.end_C cqueue)) = as (a, b) proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<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> (let cqueue = cs.[cready_queues_index_to_C qdom prio] in sched_queue_relation' (clift s) (as (qdom, prio)) (head_C cqueue) (StateRelation_C.end_C cqueue))) \<and> ((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> as (qdom, prio) = []); UCAST(32 signed \<rightarrow> 8) minDom \<le> a; a \<le> UCAST(32 signed \<rightarrow> 8) maxDom; UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> b; b \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio\<rbrakk> \<Longrightarrow> let cqueue = cs.[cready_queues_index_to_C a b] in sched_queue_relation' (clift s) (as (a, b)) (head_C cqueue) (StateRelation_C.end_C cqueue)
 2. \<And>a b aq. \<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> (let cqueue = cs.[cready_queues_index_to_C qdom prio] in sched_queue_relation' (clift s) (as (qdom, prio)) (head_C cqueue) (StateRelation_C.end_C cqueue))) \<and> ((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> as (qdom, prio) = []); UCAST(32 signed \<rightarrow> 8) minDom \<le> a; a \<le> UCAST(32 signed \<rightarrow> 8) maxDom; UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> b; b \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio; let cqueue = cs.[cready_queues_index_to_C a b] in sched_queue_relation' (clift s) aq (head_C cqueue) (StateRelation_C.end_C cqueue)\<rbrakk> \<Longrightarrow> aq = as (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>a b aq. \<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> (let cqueue = cs.[cready_queues_index_to_C qdom prio] in sched_queue_relation' (clift s) (as (qdom, prio)) (head_C cqueue) (StateRelation_C.end_C cqueue))) \<and> ((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> as (qdom, prio) = []); UCAST(32 signed \<rightarrow> 8) minDom \<le> a; a \<le> UCAST(32 signed \<rightarrow> 8) maxDom; UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> b; b \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio; let cqueue = cs.[cready_queues_index_to_C a b] in sched_queue_relation' (clift s) aq (head_C cqueue) (StateRelation_C.end_C cqueue)\<rbrakk> \<Longrightarrow> aq = as (a, b) proof (prove)
goal (1 subgoal):
 1. \<And>a b aq. \<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> sched_queue_relation' (clift s) (as (qdom, prio)) (head_C (cs.[cready_queues_index_to_C qdom prio])) (StateRelation_C.end_C (cs.[cready_queues_index_to_C qdom prio]))) \<and> ((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> as (qdom, prio) = []); UCAST(32 signed \<rightarrow> 8) minDom \<le> a; a \<le> UCAST(32 signed \<rightarrow> 8) maxDom; UCAST(32 signed \<rightarrow> 8) seL4_MinPrio \<le> b; b \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio; sched_queue_relation' (clift s) aq (head_C (cs.[cready_queues_index_to_C a b])) (StateRelation_C.end_C (cs.[cready_queues_index_to_C a b]))\<rbrakk> \<Longrightarrow> aq = as (a, b) proof (prove)
goal:
No subgoals!