theory TcbQueue_C

lemma tcb_queue_relation_cong:
  assumes queuec: "queue = queue'"
  and        qpc: "qprev = qprev'"
  and        qhc: "qhead = qhead'"
  and        mpc: "\<And>p. p \<in> tcb_ptr_to_ctcb_ptr ` set queue' \<Longrightarrow> mp p = mp' p"
  shows "tcb_queue_relation getNext getPrev mp queue qprev qhead =
  tcb_queue_relation getNext getPrev mp' queue' qprev' qhead'" (is "?LHS = ?RHS") proof - have "?LHS = tcb_queue_relation getNext getPrev (mp |` (tcb_ptr_to_ctcb_ptr ` set queue')) queue' qprev' qhead'" by (simp add: queuec qpc qhc, subst tcb_queue_relation_restrict, rule refl) also have "\<dots> = tcb_queue_relation getNext getPrev (mp' |` (tcb_ptr_to_ctcb_ptr ` set queue')) queue' qprev' qhead'" by (simp add: mpc cong: restrict_map_cong) also have "\<dots> = ?RHS" by (simp add: tcb_queue_relation_restrict [symmetric]) finally show ?thesis . qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_queue_relation getNext getPrev mp queue qprev qhead = tcb_queue_relation getNext getPrev mp' queue' qprev' qhead' proof (state)
goal (1 subgoal):
 1. tcb_queue_relation getNext getPrev mp queue qprev qhead = tcb_queue_relation getNext getPrev mp' queue' qprev' qhead' proof (prove)
goal (1 subgoal):
 1. tcb_queue_relation getNext getPrev mp queue qprev qhead = tcb_queue_relation getNext getPrev (mp|\<^bsub>(tcb_ptr_to_ctcb_ptr ` set queue')\<^esub>) queue' qprev' qhead' proof (state)
this:
tcb_queue_relation getNext getPrev mp queue qprev qhead = tcb_queue_relation getNext getPrev (mp|\<^bsub>(tcb_ptr_to_ctcb_ptr ` set queue')\<^esub>) queue' qprev' qhead'

goal (1 subgoal):
 1. tcb_queue_relation getNext getPrev mp queue qprev qhead = tcb_queue_relation getNext getPrev mp' queue' qprev' qhead' proof (state)
this:
tcb_queue_relation getNext getPrev mp queue qprev qhead = tcb_queue_relation getNext getPrev (mp|\<^bsub>(tcb_ptr_to_ctcb_ptr ` set queue')\<^esub>) queue' qprev' qhead'

goal (1 subgoal):
 1. tcb_queue_relation getNext getPrev mp queue qprev qhead = tcb_queue_relation getNext getPrev mp' queue' qprev' qhead' proof (prove)
goal (1 subgoal):
 1. tcb_queue_relation getNext getPrev (mp|\<^bsub>(tcb_ptr_to_ctcb_ptr ` set queue')\<^esub>) queue' qprev' qhead' = tcb_queue_relation getNext getPrev (mp'|\<^bsub>(tcb_ptr_to_ctcb_ptr ` set queue')\<^esub>) queue' qprev' qhead' proof (state)
this:
tcb_queue_relation getNext getPrev (mp|\<^bsub>(tcb_ptr_to_ctcb_ptr ` set queue')\<^esub>) queue' qprev' qhead' = tcb_queue_relation getNext getPrev (mp'|\<^bsub>(tcb_ptr_to_ctcb_ptr ` set queue')\<^esub>) queue' qprev' qhead'

goal (1 subgoal):
 1. tcb_queue_relation getNext getPrev mp queue qprev qhead = tcb_queue_relation getNext getPrev mp' queue' qprev' qhead' proof (state)
this:
tcb_queue_relation getNext getPrev (mp|\<^bsub>(tcb_ptr_to_ctcb_ptr ` set queue')\<^esub>) queue' qprev' qhead' = tcb_queue_relation getNext getPrev (mp'|\<^bsub>(tcb_ptr_to_ctcb_ptr ` set queue')\<^esub>) queue' qprev' qhead'

goal (1 subgoal):
 1. tcb_queue_relation getNext getPrev mp queue qprev qhead = tcb_queue_relation getNext getPrev mp' queue' qprev' qhead' proof (prove)
goal (1 subgoal):
 1. tcb_queue_relation getNext getPrev (mp'|\<^bsub>(tcb_ptr_to_ctcb_ptr ` set queue')\<^esub>) queue' qprev' qhead' = tcb_queue_relation getNext getPrev mp' queue' qprev' qhead' proof (state)
this:
tcb_queue_relation getNext getPrev (mp'|\<^bsub>(tcb_ptr_to_ctcb_ptr ` set queue')\<^esub>) queue' qprev' qhead' = tcb_queue_relation getNext getPrev mp' queue' qprev' qhead'

goal (1 subgoal):
 1. tcb_queue_relation getNext getPrev mp queue qprev qhead = tcb_queue_relation getNext getPrev mp' queue' qprev' qhead' proof (chain)
picking this:
tcb_queue_relation getNext getPrev mp queue qprev qhead = tcb_queue_relation getNext getPrev mp' queue' qprev' qhead' proof (prove)
using this:
tcb_queue_relation getNext getPrev mp queue qprev qhead = tcb_queue_relation getNext getPrev mp' queue' qprev' qhead'

goal (1 subgoal):
 1. tcb_queue_relation getNext getPrev mp queue qprev qhead = tcb_queue_relation getNext getPrev mp' queue' qprev' qhead' proof (state)
this:
tcb_queue_relation getNext getPrev mp queue qprev qhead = tcb_queue_relation getNext getPrev mp' queue' qprev' qhead'

goal:
No subgoals!