theory Finalise_C

lemma ep_queue_relation_shift:
  "(option_map2 tcbEPNext_C (cslift s')
         = option_map2 tcbEPNext_C (cslift s)
    \<and> option_map2 tcbEPPrev_C (cslift s')
         = option_map2 tcbEPPrev_C (cslift s))
     \<longrightarrow> ep_queue_relation (cslift s') ts qPrev qHead
          = ep_queue_relation (cslift s) ts qPrev qHead" apply clarsimp apply (induct ts arbitrary: qPrev qHead) apply simp apply simp apply (simp add: option_map2_def fun_eq_iff
                   map_option_case) apply (drule_tac x=qHead in spec)+ apply (clarsimp split: option.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. option_map2 tcbEPNext_C (cslift s') = option_map2 tcbEPNext_C (cslift s) \<and> option_map2 tcbEPPrev_C (cslift s') = option_map2 tcbEPPrev_C (cslift s) \<longrightarrow> ep_queue_relation (cslift s') ts qPrev qHead = ep_queue_relation (cslift s) ts qPrev qHead proof (prove)
goal (1 subgoal):
 1. \<lbrakk>option_map2 tcbEPNext_C (cslift s') = option_map2 tcbEPNext_C (cslift s); option_map2 tcbEPPrev_C (cslift s') = option_map2 tcbEPPrev_C (cslift s)\<rbrakk> \<Longrightarrow> ep_queue_relation (cslift s') ts qPrev qHead = ep_queue_relation (cslift s) ts qPrev qHead proof (prove)
goal (2 subgoals):
 1. \<And>qPrev qHead. \<lbrakk>option_map2 tcbEPNext_C (cslift s') = option_map2 tcbEPNext_C (cslift s); option_map2 tcbEPPrev_C (cslift s') = option_map2 tcbEPPrev_C (cslift s)\<rbrakk> \<Longrightarrow> ep_queue_relation (cslift s') [] qPrev qHead = ep_queue_relation (cslift s) [] qPrev qHead
 2. \<And>x1 ts qPrev qHead. \<lbrakk>\<And>qPrev qHead. \<lbrakk>option_map2 tcbEPNext_C (cslift s') = option_map2 tcbEPNext_C (cslift s); option_map2 tcbEPPrev_C (cslift s') = option_map2 tcbEPPrev_C (cslift s)\<rbrakk> \<Longrightarrow> ep_queue_relation (cslift s') ts qPrev qHead = ep_queue_relation (cslift s) ts qPrev qHead; option_map2 tcbEPNext_C (cslift s') = option_map2 tcbEPNext_C (cslift s); option_map2 tcbEPPrev_C (cslift s') = option_map2 tcbEPPrev_C (cslift s)\<rbrakk> \<Longrightarrow> ep_queue_relation (cslift s') (x1 # ts) qPrev qHead = ep_queue_relation (cslift s) (x1 # ts) qPrev qHead proof (prove)
goal (1 subgoal):
 1. \<And>x1 ts qPrev qHead. \<lbrakk>\<And>qPrev qHead. \<lbrakk>option_map2 tcbEPNext_C (cslift s') = option_map2 tcbEPNext_C (cslift s); option_map2 tcbEPPrev_C (cslift s') = option_map2 tcbEPPrev_C (cslift s)\<rbrakk> \<Longrightarrow> ep_queue_relation (cslift s') ts qPrev qHead = ep_queue_relation (cslift s) ts qPrev qHead; option_map2 tcbEPNext_C (cslift s') = option_map2 tcbEPNext_C (cslift s); option_map2 tcbEPPrev_C (cslift s') = option_map2 tcbEPPrev_C (cslift s)\<rbrakk> \<Longrightarrow> ep_queue_relation (cslift s') (x1 # ts) qPrev qHead = ep_queue_relation (cslift s) (x1 # ts) qPrev qHead proof (prove)
goal (1 subgoal):
 1. \<And>x1 ts qPrev qHead. \<lbrakk>\<And>qPrev qHead. ep_queue_relation (cslift s') ts qPrev qHead = ep_queue_relation (cslift s) ts qPrev qHead; option_map2 tcbEPNext_C (cslift s') = option_map2 tcbEPNext_C (cslift s); option_map2 tcbEPPrev_C (cslift s') = option_map2 tcbEPPrev_C (cslift s)\<rbrakk> \<Longrightarrow> (qHead = tcb_ptr_to_ctcb_ptr x1 \<and> (\<exists>tcb. cslift s' qHead = Some tcb \<and> tcbEPPrev_C tcb = qPrev \<and> ep_queue_relation (cslift s) ts qHead (tcbEPNext_C tcb))) = (qHead = tcb_ptr_to_ctcb_ptr x1 \<and> (\<exists>tcb. cslift s qHead = Some tcb \<and> tcbEPPrev_C tcb = qPrev \<and> ep_queue_relation (cslift s) ts qHead (tcbEPNext_C tcb))) proof (prove)
goal (1 subgoal):
 1. \<And>x1 ts qPrev qHead. \<lbrakk>\<And>qPrev qHead. ep_queue_relation (cslift s') ts qPrev qHead = ep_queue_relation (cslift s) ts qPrev qHead; \<forall>x. (case cslift s' x of None \<Rightarrow> None | Some x \<Rightarrow> Some (tcbEPNext_C x)) = (case cslift s x of None \<Rightarrow> None | Some x \<Rightarrow> Some (tcbEPNext_C x)); \<forall>x. (case cslift s' x of None \<Rightarrow> None | Some x \<Rightarrow> Some (tcbEPPrev_C x)) = (case cslift s x of None \<Rightarrow> None | Some x \<Rightarrow> Some (tcbEPPrev_C x))\<rbrakk> \<Longrightarrow> (qHead = tcb_ptr_to_ctcb_ptr x1 \<and> (\<exists>tcb. cslift s' qHead = Some tcb \<and> tcbEPPrev_C tcb = qPrev \<and> ep_queue_relation (cslift s) ts qHead (tcbEPNext_C tcb))) = (qHead = tcb_ptr_to_ctcb_ptr x1 \<and> (\<exists>tcb. cslift s qHead = Some tcb \<and> tcbEPPrev_C tcb = qPrev \<and> ep_queue_relation (cslift s) ts qHead (tcbEPNext_C tcb))) proof (prove)
goal (1 subgoal):
 1. \<And>x1 ts qPrev qHead. \<lbrakk>\<And>qPrev qHead. ep_queue_relation (cslift s') ts qPrev qHead = ep_queue_relation (cslift s) ts qPrev qHead; (case cslift s' qHead of None \<Rightarrow> None | Some x \<Rightarrow> Some (tcbEPNext_C x)) = (case cslift s qHead of None \<Rightarrow> None | Some x \<Rightarrow> Some (tcbEPNext_C x)); (case cslift s' qHead of None \<Rightarrow> None | Some x \<Rightarrow> Some (tcbEPPrev_C x)) = (case cslift s qHead of None \<Rightarrow> None | Some x \<Rightarrow> Some (tcbEPPrev_C x))\<rbrakk> \<Longrightarrow> (qHead = tcb_ptr_to_ctcb_ptr x1 \<and> (\<exists>tcb. cslift s' qHead = Some tcb \<and> tcbEPPrev_C tcb = qPrev \<and> ep_queue_relation (cslift s) ts qHead (tcbEPNext_C tcb))) = (qHead = tcb_ptr_to_ctcb_ptr x1 \<and> (\<exists>tcb. cslift s qHead = Some tcb \<and> tcbEPPrev_C tcb = qPrev \<and> ep_queue_relation (cslift s) ts qHead (tcbEPNext_C tcb))) proof (prove)
goal:
No subgoals!