theory TcbQueue_C

lemma tcb_queue_relation_restrict0:
  "set queue \<subseteq> S \<Longrightarrow> tcb_queue_relation getNext getPrev mp queue qprev qhead =
  tcb_queue_relation getNext getPrev (restrict_map mp (tcb_ptr_to_ctcb_ptr ` S)) queue qprev qhead" proof (induct queue arbitrary: S qprev qhead) case Nil thus ?case by simp next case (Cons tcb tcbs S' qprev' qhead') thus ?case using Cons by auto qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set queue \<subseteq> S \<Longrightarrow> tcb_queue_relation getNext getPrev mp queue qprev qhead = tcb_queue_relation getNext getPrev (mp|\<^bsub>(tcb_ptr_to_ctcb_ptr ` S)\<^esub>) queue qprev qhead proof (state)
goal (2 subgoals):
 1. \<And>S qprev qhead. set [] \<subseteq> S \<Longrightarrow> tcb_queue_relation getNext getPrev mp [] qprev qhead = tcb_queue_relation getNext getPrev (mp|\<^bsub>(tcb_ptr_to_ctcb_ptr ` S)\<^esub>) [] qprev qhead
 2. \<And>x1 queue S qprev qhead. \<lbrakk>\<And>S qprev qhead. set queue \<subseteq> S \<Longrightarrow> tcb_queue_relation getNext getPrev mp queue qprev qhead = tcb_queue_relation getNext getPrev (mp|\<^bsub>(tcb_ptr_to_ctcb_ptr ` S)\<^esub>) queue qprev qhead; set (x1 # queue) \<subseteq> S\<rbrakk> \<Longrightarrow> tcb_queue_relation getNext getPrev mp (x1 # queue) qprev qhead = tcb_queue_relation getNext getPrev (mp|\<^bsub>(tcb_ptr_to_ctcb_ptr ` S)\<^esub>) (x1 # queue) qprev qhead proof (state)
this:
set [] \<subseteq> S

goal (2 subgoals):
 1. \<And>S qprev qhead. set [] \<subseteq> S \<Longrightarrow> tcb_queue_relation getNext getPrev mp [] qprev qhead = tcb_queue_relation getNext getPrev (mp|\<^bsub>(tcb_ptr_to_ctcb_ptr ` S)\<^esub>) [] qprev qhead
 2. \<And>x1 queue S qprev qhead. \<lbrakk>\<And>S qprev qhead. set queue \<subseteq> S \<Longrightarrow> tcb_queue_relation getNext getPrev mp queue qprev qhead = tcb_queue_relation getNext getPrev (mp|\<^bsub>(tcb_ptr_to_ctcb_ptr ` S)\<^esub>) queue qprev qhead; set (x1 # queue) \<subseteq> S\<rbrakk> \<Longrightarrow> tcb_queue_relation getNext getPrev mp (x1 # queue) qprev qhead = tcb_queue_relation getNext getPrev (mp|\<^bsub>(tcb_ptr_to_ctcb_ptr ` S)\<^esub>) (x1 # queue) qprev qhead proof (prove)
using this:
set [] \<subseteq> S

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

goal (1 subgoal):
 1. \<And>x1 queue S qprev qhead. \<lbrakk>\<And>S qprev qhead. set queue \<subseteq> S \<Longrightarrow> tcb_queue_relation getNext getPrev mp queue qprev qhead = tcb_queue_relation getNext getPrev (mp|\<^bsub>(tcb_ptr_to_ctcb_ptr ` S)\<^esub>) queue qprev qhead; set (x1 # queue) \<subseteq> S\<rbrakk> \<Longrightarrow> tcb_queue_relation getNext getPrev mp (x1 # queue) qprev qhead = tcb_queue_relation getNext getPrev (mp|\<^bsub>(tcb_ptr_to_ctcb_ptr ` S)\<^esub>) (x1 # queue) qprev qhead proof (state)
goal (1 subgoal):
 1. \<And>x1 queue S qprev qhead. \<lbrakk>\<And>S qprev qhead. set queue \<subseteq> S \<Longrightarrow> tcb_queue_relation getNext getPrev mp queue qprev qhead = tcb_queue_relation getNext getPrev (mp|\<^bsub>(tcb_ptr_to_ctcb_ptr ` S)\<^esub>) queue qprev qhead; set (x1 # queue) \<subseteq> S\<rbrakk> \<Longrightarrow> tcb_queue_relation getNext getPrev mp (x1 # queue) qprev qhead = tcb_queue_relation getNext getPrev (mp|\<^bsub>(tcb_ptr_to_ctcb_ptr ` S)\<^esub>) (x1 # queue) qprev qhead proof (state)
this:
set tcbs \<subseteq> ?S \<Longrightarrow> tcb_queue_relation getNext getPrev mp tcbs ?qprev ?qhead = tcb_queue_relation getNext getPrev (mp|\<^bsub>(tcb_ptr_to_ctcb_ptr ` ?S)\<^esub>) tcbs ?qprev ?qhead
set (tcb # tcbs) \<subseteq> S'

goal (1 subgoal):
 1. \<And>x1 queue S qprev qhead. \<lbrakk>\<And>S qprev qhead. set queue \<subseteq> S \<Longrightarrow> tcb_queue_relation getNext getPrev mp queue qprev qhead = tcb_queue_relation getNext getPrev (mp|\<^bsub>(tcb_ptr_to_ctcb_ptr ` S)\<^esub>) queue qprev qhead; set (x1 # queue) \<subseteq> S\<rbrakk> \<Longrightarrow> tcb_queue_relation getNext getPrev mp (x1 # queue) qprev qhead = tcb_queue_relation getNext getPrev (mp|\<^bsub>(tcb_ptr_to_ctcb_ptr ` S)\<^esub>) (x1 # queue) qprev qhead proof (prove)
using this:
set tcbs \<subseteq> ?S \<Longrightarrow> tcb_queue_relation getNext getPrev mp tcbs ?qprev ?qhead = tcb_queue_relation getNext getPrev (mp|\<^bsub>(tcb_ptr_to_ctcb_ptr ` ?S)\<^esub>) tcbs ?qprev ?qhead
set (tcb # tcbs) \<subseteq> S'

goal (1 subgoal):
 1. tcb_queue_relation getNext getPrev mp (tcb # tcbs) qprev' qhead' = tcb_queue_relation getNext getPrev (mp|\<^bsub>(tcb_ptr_to_ctcb_ptr ` S')\<^esub>) (tcb # tcbs) qprev' qhead' proof (prove)
using this:
set tcbs \<subseteq> ?S \<Longrightarrow> tcb_queue_relation getNext getPrev mp tcbs ?qprev ?qhead = tcb_queue_relation getNext getPrev (mp|\<^bsub>(tcb_ptr_to_ctcb_ptr ` ?S)\<^esub>) tcbs ?qprev ?qhead
set (tcb # tcbs) \<subseteq> S'
set tcbs \<subseteq> ?S \<Longrightarrow> tcb_queue_relation getNext getPrev mp tcbs ?qprev ?qhead = tcb_queue_relation getNext getPrev (mp|\<^bsub>(tcb_ptr_to_ctcb_ptr ` ?S)\<^esub>) tcbs ?qprev ?qhead
set (tcb # tcbs) \<subseteq> S'

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

goal:
No subgoals!