theory Retype_C

lemma tcb_queue_update_other:
  "\<lbrakk> ctcb_ptr_to_tcb_ptr p \<notin> set tcbs \<rbrakk> \<Longrightarrow>
  tcb_queue_relation next prev (mp(p \<mapsto> v)) tcbs qe qh =
  tcb_queue_relation next prev mp tcbs qe qh" apply (induct tcbs arbitrary: qh qe) apply simp apply (rename_tac a tcbs qh qe) apply simp apply (subgoal_tac "p \<noteq> tcb_ptr_to_ctcb_ptr a") apply (simp cong: conj_cong) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ctcb_ptr_to_tcb_ptr p \<notin> set tcbs \<Longrightarrow> tcb_queue_relation next prev (mp(p \<mapsto> v)) tcbs qe qh = tcb_queue_relation next prev mp tcbs qe qh proof (prove)
goal (2 subgoals):
 1. \<And>qh qe. ctcb_ptr_to_tcb_ptr p \<notin> set [] \<Longrightarrow> tcb_queue_relation next prev (mp(p \<mapsto> v)) [] qe qh = tcb_queue_relation next prev mp [] qe qh
 2. \<And>x1 tcbs qh qe. \<lbrakk>\<And>qh qe. ctcb_ptr_to_tcb_ptr p \<notin> set tcbs \<Longrightarrow> tcb_queue_relation next prev (mp(p \<mapsto> v)) tcbs qe qh = tcb_queue_relation next prev mp tcbs qe qh; ctcb_ptr_to_tcb_ptr p \<notin> set (x1 # tcbs)\<rbrakk> \<Longrightarrow> tcb_queue_relation next prev (mp(p \<mapsto> v)) (x1 # tcbs) qe qh = tcb_queue_relation next prev mp (x1 # tcbs) qe qh proof (prove)
goal (1 subgoal):
 1. \<And>x1 tcbs qh qe. \<lbrakk>\<And>qh qe. ctcb_ptr_to_tcb_ptr p \<notin> set tcbs \<Longrightarrow> tcb_queue_relation next prev (mp(p \<mapsto> v)) tcbs qe qh = tcb_queue_relation next prev mp tcbs qe qh; ctcb_ptr_to_tcb_ptr p \<notin> set (x1 # tcbs)\<rbrakk> \<Longrightarrow> tcb_queue_relation next prev (mp(p \<mapsto> v)) (x1 # tcbs) qe qh = tcb_queue_relation next prev mp (x1 # tcbs) qe qh proof (prove)
goal (1 subgoal):
 1. \<And>a tcbs qh qe. \<lbrakk>\<And>qh qe. ctcb_ptr_to_tcb_ptr p \<notin> set tcbs \<Longrightarrow> tcb_queue_relation next prev (mp(p \<mapsto> v)) tcbs qe qh = tcb_queue_relation next prev mp tcbs qe qh; ctcb_ptr_to_tcb_ptr p \<notin> set (a # tcbs)\<rbrakk> \<Longrightarrow> tcb_queue_relation next prev (mp(p \<mapsto> v)) (a # tcbs) qe qh = tcb_queue_relation next prev mp (a # tcbs) qe qh proof (prove)
goal (1 subgoal):
 1. \<And>a tcbs qh qe. \<lbrakk>\<And>qh qe. tcb_queue_relation next prev (mp(p \<mapsto> v)) tcbs qe qh = tcb_queue_relation next prev mp tcbs qe qh; ctcb_ptr_to_tcb_ptr p \<noteq> a \<and> ctcb_ptr_to_tcb_ptr p \<notin> set tcbs\<rbrakk> \<Longrightarrow> (qh = tcb_ptr_to_ctcb_ptr a \<and> (\<exists>tcb. (if qh = p then Some v else mp qh) = Some tcb \<and> prev tcb = qe \<and> tcb_queue_relation next prev mp tcbs qh (next tcb))) = (qh = tcb_ptr_to_ctcb_ptr a \<and> (\<exists>tcb. mp qh = Some tcb \<and> prev tcb = qe \<and> tcb_queue_relation next prev mp tcbs qh (next tcb))) proof (prove)
goal (2 subgoals):
 1. \<And>a tcbs qh qe. \<lbrakk>\<And>qh qe. tcb_queue_relation next prev (mp(p \<mapsto> v)) tcbs qe qh = tcb_queue_relation next prev mp tcbs qe qh; ctcb_ptr_to_tcb_ptr p \<noteq> a \<and> ctcb_ptr_to_tcb_ptr p \<notin> set tcbs; p \<noteq> tcb_ptr_to_ctcb_ptr a\<rbrakk> \<Longrightarrow> (qh = tcb_ptr_to_ctcb_ptr a \<and> (\<exists>tcb. (if qh = p then Some v else mp qh) = Some tcb \<and> prev tcb = qe \<and> tcb_queue_relation next prev mp tcbs qh (next tcb))) = (qh = tcb_ptr_to_ctcb_ptr a \<and> (\<exists>tcb. mp qh = Some tcb \<and> prev tcb = qe \<and> tcb_queue_relation next prev mp tcbs qh (next tcb)))
 2. \<And>a tcbs qh qe. \<lbrakk>\<And>qh qe. tcb_queue_relation next prev (mp(p \<mapsto> v)) tcbs qe qh = tcb_queue_relation next prev mp tcbs qe qh; ctcb_ptr_to_tcb_ptr p \<noteq> a \<and> ctcb_ptr_to_tcb_ptr p \<notin> set tcbs\<rbrakk> \<Longrightarrow> p \<noteq> tcb_ptr_to_ctcb_ptr a proof (prove)
goal (1 subgoal):
 1. \<And>a tcbs qh qe. \<lbrakk>\<And>qh qe. tcb_queue_relation next prev (mp(p \<mapsto> v)) tcbs qe qh = tcb_queue_relation next prev mp tcbs qe qh; ctcb_ptr_to_tcb_ptr p \<noteq> a \<and> ctcb_ptr_to_tcb_ptr p \<notin> set tcbs\<rbrakk> \<Longrightarrow> p \<noteq> tcb_ptr_to_ctcb_ptr a proof (prove)
goal:
No subgoals!