theory TcbQueue_C

lemma tcb_queue_relation'_cong:
  assumes queuec: "queue = queue'"
  and        qhc: "qhead = qhead'"
  and        qpc: "qend = qend'"
  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 qhead qend =
  tcb_queue_relation' getNext getPrev mp' queue' qhead' qend'" (is "?LHS = ?RHS") proof - have "?LHS = tcb_queue_relation' getNext getPrev (mp |` (tcb_ptr_to_ctcb_ptr ` set queue')) queue' qhead' qend'" by (clarsimp simp add: queuec qpc qhc tcb_queue_relation'_def , subst tcb_queue_relation_restrict, rule refl) also have "\<dots> = tcb_queue_relation' getNext getPrev (mp' |` (tcb_ptr_to_ctcb_ptr ` set queue')) queue' qhead' qend'" by (simp add: mpc cong: restrict_map_cong) also have "\<dots> = ?RHS" by (simp add: tcb_queue_relation'_def 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 qhead qend = tcb_queue_relation' getNext getPrev mp' queue' qhead' qend' proof (state)
goal (1 subgoal):
 1. tcb_queue_relation' getNext getPrev mp queue qhead qend = tcb_queue_relation' getNext getPrev mp' queue' qhead' qend' proof (prove)
goal (1 subgoal):
 1. tcb_queue_relation' getNext getPrev mp queue qhead qend = tcb_queue_relation' getNext getPrev (mp|\<^bsub>(tcb_ptr_to_ctcb_ptr ` set queue')\<^esub>) queue' qhead' qend' proof (state)
this:
tcb_queue_relation' getNext getPrev mp queue qhead qend = tcb_queue_relation' getNext getPrev (mp|\<^bsub>(tcb_ptr_to_ctcb_ptr ` set queue')\<^esub>) queue' qhead' qend'

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

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

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

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

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

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

goal:
No subgoals!