theory IpcCancel_C

lemma tcb_queue_relation_append:
  "\<lbrakk> tcb_queue_relation tn tp mp queue qprev qhead; queue \<noteq> [];
     qend' \<notin> tcb_ptr_to_ctcb_ptr ` set queue; mp qend' = Some tcb;
     queue = queue' @ [ctcb_ptr_to_tcb_ptr qend]; distinct queue;
     \<forall>x \<in> set queue. tcb_ptr_to_ctcb_ptr x \<noteq> NULL; qend' \<noteq> NULL;
     \<And>v f g. tn (tn_update f v) = f (tn v) \<and> tp (tp_update g v) = g (tp v)
                \<and> tn (tp_update f v) = tn v \<and> tp (tn_update g v) = tp v \<rbrakk>
    \<Longrightarrow> tcb_queue_relation tn tp
          (mp (qend \<mapsto> tn_update (\<lambda>_. qend') (the (mp qend)),
               qend' \<mapsto> tn_update (\<lambda>_. NULL) (tp_update (\<lambda>_. qend) tcb)))
          (queue @ [ctcb_ptr_to_tcb_ptr qend']) qprev qhead" using [[hypsubst_thin = true]] apply clarsimp apply (induct queue' arbitrary: qprev qhead) apply clarsimp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_queue_relation tn tp mp queue qprev qhead; queue \<noteq> []; qend' \<notin> tcb_ptr_to_ctcb_ptr ` set queue; mp qend' = Some tcb; queue = queue' @ [ctcb_ptr_to_tcb_ptr qend]; distinct queue; \<forall>x\<in>set queue. tcb_ptr_to_ctcb_ptr x \<noteq> NULL; qend' \<noteq> NULL; \<And>v f g. tn (tn_update f v) = f (tn v) \<and> tp (tp_update g v) = g (tp v) \<and> tn (tp_update f v) = tn v \<and> tp (tn_update g v) = tp v\<rbrakk> \<Longrightarrow> tcb_queue_relation tn tp (mp(qend \<mapsto> tn_update (\<lambda>_. qend') (the (mp qend)), qend' \<mapsto> tn_update (\<lambda>_. NULL) (tp_update (\<lambda>_. qend) tcb))) (queue @ [ctcb_ptr_to_tcb_ptr qend']) qprev qhead proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_queue_relation tn tp mp queue qprev qhead; queue \<noteq> []; qend' \<notin> tcb_ptr_to_ctcb_ptr ` set queue; mp qend' = Some tcb; queue = queue' @ [ctcb_ptr_to_tcb_ptr qend]; distinct queue; \<forall>x\<in>set queue. tcb_ptr_to_ctcb_ptr x \<noteq> NULL; qend' \<noteq> NULL; \<And>v f g. tn (tn_update f v) = f (tn v) \<and> tp (tp_update g v) = g (tp v) \<and> tn (tp_update f v) = tn v \<and> tp (tn_update g v) = tp v\<rbrakk> \<Longrightarrow> tcb_queue_relation tn tp (mp(qend \<mapsto> tn_update (\<lambda>_. qend') (the (mp qend)), qend' \<mapsto> tn_update (\<lambda>_. NULL) (tp_update (\<lambda>_. qend) tcb))) (queue @ [ctcb_ptr_to_tcb_ptr qend']) qprev qhead proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_queue_relation tn tp mp (queue' @ [ctcb_ptr_to_tcb_ptr qend]) qprev qhead; mp qend' = Some tcb; qend' \<noteq> NULL; \<And>v f g. tn (tn_update f v) = f (tn v) \<and> tp (tp_update g v) = g (tp v) \<and> tn (tp_update f v) = tn v \<and> tp (tn_update g v) = tp v; qend' \<noteq> qend; qend' \<notin> tcb_ptr_to_ctcb_ptr ` set queue'; distinct queue'; ctcb_ptr_to_tcb_ptr qend \<notin> set queue'; qend \<noteq> NULL; \<forall>x\<in>set queue'. tcb_ptr_to_ctcb_ptr x \<noteq> NULL\<rbrakk> \<Longrightarrow> tcb_queue_relation tn tp (mp(qend \<mapsto> tn_update (\<lambda>_. qend') (the (mp qend)), qend' \<mapsto> tn_update (\<lambda>_. NULL) (tp_update (\<lambda>_. qend) tcb))) (queue' @ [ctcb_ptr_to_tcb_ptr qend, ctcb_ptr_to_tcb_ptr qend']) qprev qhead proof (prove)
goal (2 subgoals):
 1. \<And>qprev qhead. \<lbrakk>tcb_queue_relation tn tp mp ([] @ [ctcb_ptr_to_tcb_ptr qend]) qprev qhead; mp qend' = Some tcb; qend' \<noteq> NULL; \<And>v f g. tn (tn_update f v) = f (tn v) \<and> tp (tp_update g v) = g (tp v) \<and> tn (tp_update f v) = tn v \<and> tp (tn_update g v) = tp v; qend' \<noteq> qend; qend' \<notin> tcb_ptr_to_ctcb_ptr ` set []; distinct []; ctcb_ptr_to_tcb_ptr qend \<notin> set []; qend \<noteq> NULL; \<forall>x\<in>set []. tcb_ptr_to_ctcb_ptr x \<noteq> NULL\<rbrakk> \<Longrightarrow> tcb_queue_relation tn tp (mp(qend \<mapsto> tn_update (\<lambda>_. qend') (the (mp qend)), qend' \<mapsto> tn_update (\<lambda>_. NULL) (tp_update (\<lambda>_. qend) tcb))) ([] @ [ctcb_ptr_to_tcb_ptr qend, ctcb_ptr_to_tcb_ptr qend']) qprev qhead
 2. \<And>x1 queue' qprev qhead. \<lbrakk>\<And>qprev qhead. \<lbrakk>tcb_queue_relation tn tp mp (queue' @ [ctcb_ptr_to_tcb_ptr qend]) qprev qhead; mp qend' = Some tcb; qend' \<noteq> NULL; \<And>v f g. tn (tn_update f v) = f (tn v) \<and> tp (tp_update g v) = g (tp v) \<and> tn (tp_update f v) = tn v \<and> tp (tn_update g v) = tp v; qend' \<noteq> qend; qend' \<notin> tcb_ptr_to_ctcb_ptr ` set queue'; distinct queue'; ctcb_ptr_to_tcb_ptr qend \<notin> set queue'; qend \<noteq> NULL; \<forall>x\<in>set queue'. tcb_ptr_to_ctcb_ptr x \<noteq> NULL\<rbrakk> \<Longrightarrow> tcb_queue_relation tn tp (mp(qend \<mapsto> tn_update (\<lambda>_. qend') (the (mp qend)), qend' \<mapsto> tn_update (\<lambda>_. NULL) (tp_update (\<lambda>_. qend) tcb))) (queue' @ [ctcb_ptr_to_tcb_ptr qend, ctcb_ptr_to_tcb_ptr qend']) qprev qhead; tcb_queue_relation tn tp mp ((x1 # queue') @ [ctcb_ptr_to_tcb_ptr qend]) qprev qhead; mp qend' = Some tcb; qend' \<noteq> NULL; \<And>v f g. tn (tn_update f v) = f (tn v) \<and> tp (tp_update g v) = g (tp v) \<and> tn (tp_update f v) = tn v \<and> tp (tn_update g v) = tp v; qend' \<noteq> qend; qend' \<notin> tcb_ptr_to_ctcb_ptr ` set (x1 # queue'); distinct (x1 # queue'); ctcb_ptr_to_tcb_ptr qend \<notin> set (x1 # queue'); qend \<noteq> NULL; \<forall>x\<in>set (x1 # queue'). tcb_ptr_to_ctcb_ptr x \<noteq> NULL\<rbrakk> \<Longrightarrow> tcb_queue_relation tn tp (mp(qend \<mapsto> tn_update (\<lambda>_. qend') (the (mp qend)), qend' \<mapsto> tn_update (\<lambda>_. NULL) (tp_update (\<lambda>_. qend) tcb))) ((x1 # queue') @ [ctcb_ptr_to_tcb_ptr qend, ctcb_ptr_to_tcb_ptr qend']) qprev qhead proof (prove)
goal (1 subgoal):
 1. \<And>x1 queue' qprev qhead. \<lbrakk>\<And>qprev qhead. \<lbrakk>tcb_queue_relation tn tp mp (queue' @ [ctcb_ptr_to_tcb_ptr qend]) qprev qhead; mp qend' = Some tcb; qend' \<noteq> NULL; \<And>v f g. tn (tn_update f v) = f (tn v) \<and> tp (tp_update g v) = g (tp v) \<and> tn (tp_update f v) = tn v \<and> tp (tn_update g v) = tp v; qend' \<noteq> qend; qend' \<notin> tcb_ptr_to_ctcb_ptr ` set queue'; distinct queue'; ctcb_ptr_to_tcb_ptr qend \<notin> set queue'; qend \<noteq> NULL; \<forall>x\<in>set queue'. tcb_ptr_to_ctcb_ptr x \<noteq> NULL\<rbrakk> \<Longrightarrow> tcb_queue_relation tn tp (mp(qend \<mapsto> tn_update (\<lambda>_. qend') (the (mp qend)), qend' \<mapsto> tn_update (\<lambda>_. NULL) (tp_update (\<lambda>_. qend) tcb))) (queue' @ [ctcb_ptr_to_tcb_ptr qend, ctcb_ptr_to_tcb_ptr qend']) qprev qhead; tcb_queue_relation tn tp mp ((x1 # queue') @ [ctcb_ptr_to_tcb_ptr qend]) qprev qhead; mp qend' = Some tcb; qend' \<noteq> NULL; \<And>v f g. tn (tn_update f v) = f (tn v) \<and> tp (tp_update g v) = g (tp v) \<and> tn (tp_update f v) = tn v \<and> tp (tn_update g v) = tp v; qend' \<noteq> qend; qend' \<notin> tcb_ptr_to_ctcb_ptr ` set (x1 # queue'); distinct (x1 # queue'); ctcb_ptr_to_tcb_ptr qend \<notin> set (x1 # queue'); qend \<noteq> NULL; \<forall>x\<in>set (x1 # queue'). tcb_ptr_to_ctcb_ptr x \<noteq> NULL\<rbrakk> \<Longrightarrow> tcb_queue_relation tn tp (mp(qend \<mapsto> tn_update (\<lambda>_. qend') (the (mp qend)), qend' \<mapsto> tn_update (\<lambda>_. NULL) (tp_update (\<lambda>_. qend) tcb))) ((x1 # queue') @ [ctcb_ptr_to_tcb_ptr qend, ctcb_ptr_to_tcb_ptr qend']) qprev qhead proof (prove)
goal:
No subgoals!