theory IpcCancel_C

lemma tcb_queue_relation_prev_next':
  "\<lbrakk> tcb_queue_relation' tn tp mp queue qhead qend; tcbp \<in> set queue; distinct queue;
       \<forall>t \<in> set queue. tcb_at' t s; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb \<rbrakk>
      \<Longrightarrow> (tn tcb \<noteq> tcb_Ptr 0 \<longrightarrow> tn tcb \<in> tcb_ptr_to_ctcb_ptr ` set queue
                       \<and> mp (tn tcb) \<noteq> None \<and> tn tcb \<noteq> tcb_ptr_to_ctcb_ptr tcbp)
        \<and> (tp tcb \<noteq> tcb_Ptr 0 \<longrightarrow> tp tcb \<in> tcb_ptr_to_ctcb_ptr ` set queue
                       \<and> mp (tp tcb) \<noteq> None \<and> tp tcb \<noteq> tcb_ptr_to_ctcb_ptr tcbp)
        \<and> (tn tcb \<noteq> tcb_Ptr 0 \<longrightarrow> tn tcb \<noteq> tp tcb)" apply (clarsimp simp: tcb_queue_relation'_def split: if_split_asm) apply (drule(1) tcb_queue_relation_prev_next, simp_all) apply (fastforce dest: tcb_at_not_NULL) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_queue_relation' tn tp mp queue qhead qend; tcbp \<in> set queue; distinct queue; \<forall>t\<in>set queue. tcb_at' t s; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb\<rbrakk> \<Longrightarrow> (tn tcb \<noteq> NULL \<longrightarrow> tn tcb \<in> tcb_ptr_to_ctcb_ptr ` set queue \<and> mp (tn tcb) \<noteq> None \<and> tn tcb \<noteq> tcb_ptr_to_ctcb_ptr tcbp) \<and> (tp tcb \<noteq> NULL \<longrightarrow> tp tcb \<in> tcb_ptr_to_ctcb_ptr ` set queue \<and> mp (tp tcb) \<noteq> None \<and> tp tcb \<noteq> tcb_ptr_to_ctcb_ptr tcbp) \<and> (tn tcb \<noteq> NULL \<longrightarrow> tn tcb \<noteq> tp tcb) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcbp \<in> set queue; distinct queue; \<forall>t\<in>set queue. tcb_at' t s; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; queue \<noteq> []; qend = tcb_ptr_to_ctcb_ptr (last queue); tcb_queue_relation tn tp mp queue NULL qhead\<rbrakk> \<Longrightarrow> (tn tcb \<noteq> NULL \<longrightarrow> tn tcb \<in> tcb_ptr_to_ctcb_ptr ` set queue \<and> (\<exists>y. mp (tn tcb) = Some y) \<and> tn tcb \<noteq> tcb_ptr_to_ctcb_ptr tcbp) \<and> (tp tcb \<noteq> NULL \<longrightarrow> tp tcb \<in> tcb_ptr_to_ctcb_ptr ` set queue \<and> (\<exists>y. mp (tp tcb) = Some y) \<and> tp tcb \<noteq> tcb_ptr_to_ctcb_ptr tcbp) \<and> (tn tcb \<noteq> NULL \<longrightarrow> tn tcb \<noteq> tp tcb) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>tcbp \<in> set queue; distinct queue; \<forall>t\<in>set queue. tcb_at' t s; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; queue \<noteq> []; qend = tcb_ptr_to_ctcb_ptr (last queue)\<rbrakk> \<Longrightarrow> ctcb_ptr_to_tcb_ptr NULL \<notin> set queue
 2. \<lbrakk>tcbp \<in> set queue; distinct queue; \<forall>t\<in>set queue. tcb_at' t s; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; queue \<noteq> []; qend = tcb_ptr_to_ctcb_ptr (last queue); (tn tcb \<noteq> NULL \<longrightarrow> tn tcb \<in> tcb_ptr_to_ctcb_ptr ` set queue \<and> (\<exists>y. mp (tn tcb) = Some y) \<and> tn tcb \<noteq> tcb_ptr_to_ctcb_ptr tcbp) \<and> (tp tcb \<noteq> NULL \<longrightarrow> (tp tcb \<in> tcb_ptr_to_ctcb_ptr ` set queue \<or> tp tcb = NULL) \<and> (\<exists>y. mp (tp tcb) = Some y) \<and> tp tcb \<noteq> tcb_ptr_to_ctcb_ptr tcbp) \<and> (tn tcb \<noteq> NULL \<longrightarrow> tn tcb \<noteq> tp tcb)\<rbrakk> \<Longrightarrow> (tn tcb \<noteq> NULL \<longrightarrow> tn tcb \<in> tcb_ptr_to_ctcb_ptr ` set queue \<and> (\<exists>y. mp (tn tcb) = Some y) \<and> tn tcb \<noteq> tcb_ptr_to_ctcb_ptr tcbp) \<and> (tp tcb \<noteq> NULL \<longrightarrow> tp tcb \<in> tcb_ptr_to_ctcb_ptr ` set queue \<and> (\<exists>y. mp (tp tcb) = Some y) \<and> tp tcb \<noteq> tcb_ptr_to_ctcb_ptr tcbp) \<and> (tn tcb \<noteq> NULL \<longrightarrow> tn tcb \<noteq> tp tcb) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcbp \<in> set queue; distinct queue; \<forall>t\<in>set queue. tcb_at' t s; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb; queue \<noteq> []; qend = tcb_ptr_to_ctcb_ptr (last queue); (tn tcb \<noteq> NULL \<longrightarrow> tn tcb \<in> tcb_ptr_to_ctcb_ptr ` set queue \<and> (\<exists>y. mp (tn tcb) = Some y) \<and> tn tcb \<noteq> tcb_ptr_to_ctcb_ptr tcbp) \<and> (tp tcb \<noteq> NULL \<longrightarrow> (tp tcb \<in> tcb_ptr_to_ctcb_ptr ` set queue \<or> tp tcb = NULL) \<and> (\<exists>y. mp (tp tcb) = Some y) \<and> tp tcb \<noteq> tcb_ptr_to_ctcb_ptr tcbp) \<and> (tn tcb \<noteq> NULL \<longrightarrow> tn tcb \<noteq> tp tcb)\<rbrakk> \<Longrightarrow> (tn tcb \<noteq> NULL \<longrightarrow> tn tcb \<in> tcb_ptr_to_ctcb_ptr ` set queue \<and> (\<exists>y. mp (tn tcb) = Some y) \<and> tn tcb \<noteq> tcb_ptr_to_ctcb_ptr tcbp) \<and> (tp tcb \<noteq> NULL \<longrightarrow> tp tcb \<in> tcb_ptr_to_ctcb_ptr ` set queue \<and> (\<exists>y. mp (tp tcb) = Some y) \<and> tp tcb \<noteq> tcb_ptr_to_ctcb_ptr tcbp) \<and> (tn tcb \<noteq> NULL \<longrightarrow> tn tcb \<noteq> tp tcb) proof (prove)
goal:
No subgoals!