theory TcbQueue_C

lemma cpspace_relation_ntfn_update_ntfn:
  fixes ntfn :: "Structures_H.notification"
  defines "qs \<equiv> if isWaitingNtfn (ntfnObj ntfn) then set (ntfnQueue (ntfnObj ntfn)) else {}"
  assumes koat: "ko_at' ntfn ntfnptr s"
  and     invs: "invs' s"
  and      cp: "cpspace_ntfn_relation (ksPSpace s) (t_hrs_' (globals t))"
  and     rel: "cnotification_relation (cslift t') ntfn' notification"
  and    mpeq: "(cslift t' |` (- (tcb_ptr_to_ctcb_ptr ` qs))) = (cslift t |` (- (tcb_ptr_to_ctcb_ptr ` qs)))"
  shows "cmap_relation (map_to_ntfns ((ksPSpace s)(ntfnptr \<mapsto> KONotification ntfn')))
           ((cslift t)(Ptr ntfnptr \<mapsto> notification)) Ptr (cnotification_relation (cslift t'))" using koat invs cp rel apply - apply (subst map_comp_update) apply (simp add: projectKO_opts_defs) apply (frule ko_at_projectKO_opt) apply (rule cmap_relationE1, assumption+) apply (erule (3) cmap_relation_upd_relI) apply (erule (1) cnotification_relation_ntfn_queue [OF _ invs_sym' koat]) apply (erule (1) map_to_ko_atI') apply (fold qs_def, rule mpeq) apply assumption apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cmap_relation (map_to_ntfns ((ksPSpace s)(ntfnptr \<mapsto> KONotification ntfn'))) ((cslift t)(ntfn_Ptr ntfnptr \<mapsto> notification)) ntfn_Ptr (cnotification_relation (cslift t')) proof (prove)
using this:
ko_at' ntfn ntfnptr s
invs' s
cmap_relation (map_to_ntfns (ksPSpace s)) (cslift t) ntfn_Ptr (cnotification_relation (cslift t))
cnotification_relation (cslift t') ntfn' notification

goal (1 subgoal):
 1. cmap_relation (map_to_ntfns ((ksPSpace s)(ntfnptr \<mapsto> KONotification ntfn'))) ((cslift t)(ntfn_Ptr ntfnptr \<mapsto> notification)) ntfn_Ptr (cnotification_relation (cslift t')) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at' ntfn ntfnptr s; invs' s; cmap_relation (map_to_ntfns (ksPSpace s)) (cslift t) ntfn_Ptr (cnotification_relation (cslift t)); cnotification_relation (cslift t') ntfn' notification\<rbrakk> \<Longrightarrow> cmap_relation (map_to_ntfns ((ksPSpace s)(ntfnptr \<mapsto> KONotification ntfn'))) ((cslift t)(ntfn_Ptr ntfnptr \<mapsto> notification)) ntfn_Ptr (cnotification_relation (cslift t')) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at' ntfn ntfnptr s; invs' s; cmap_relation (map_to_ntfns (ksPSpace s)) (cslift t) ntfn_Ptr (cnotification_relation (cslift t)); cnotification_relation (cslift t') ntfn' notification\<rbrakk> \<Longrightarrow> cmap_relation ((map_to_ntfns (ksPSpace s))(ntfnptr := projectKO_opt (KONotification ntfn'))) ((cslift t)(ntfn_Ptr ntfnptr \<mapsto> notification)) ntfn_Ptr (cnotification_relation (cslift t')) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at' ntfn ntfnptr s; invs' s; cmap_relation (map_to_ntfns (ksPSpace s)) (cslift t) ntfn_Ptr (cnotification_relation (cslift t)); cnotification_relation (cslift t') ntfn' notification\<rbrakk> \<Longrightarrow> cmap_relation ((map_to_ntfns (ksPSpace s))(ntfnptr \<mapsto> ntfn')) ((cslift t)(ntfn_Ptr ntfnptr \<mapsto> notification)) ntfn_Ptr (cnotification_relation (cslift t')) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at' ntfn ntfnptr s; invs' s; cmap_relation (map_to_ntfns (ksPSpace s)) (cslift t) ntfn_Ptr (cnotification_relation (cslift t)); cnotification_relation (cslift t') ntfn' notification; map_to_ntfns (ksPSpace s) ntfnptr = Some ntfn\<rbrakk> \<Longrightarrow> cmap_relation ((map_to_ntfns (ksPSpace s))(ntfnptr \<mapsto> ntfn')) ((cslift t)(ntfn_Ptr ntfnptr \<mapsto> notification)) ntfn_Ptr (cnotification_relation (cslift t')) proof (prove)
goal (1 subgoal):
 1. \<And>y'. \<lbrakk>ko_at' ntfn ntfnptr s; invs' s; cmap_relation (map_to_ntfns (ksPSpace s)) (cslift t) ntfn_Ptr (cnotification_relation (cslift t)); cnotification_relation (cslift t') ntfn' notification; map_to_ntfns (ksPSpace s) ntfnptr = Some ntfn; map_to_ntfns (ksPSpace s) ntfnptr = Some ntfn; cnotification_relation (cslift t) ntfn y'; cslift t (ntfn_Ptr ntfnptr) = Some y'\<rbrakk> \<Longrightarrow> cmap_relation ((map_to_ntfns (ksPSpace s))(ntfnptr \<mapsto> ntfn')) ((cslift t)(ntfn_Ptr ntfnptr \<mapsto> notification)) ntfn_Ptr (cnotification_relation (cslift t')) proof (prove)
goal (2 subgoals):
 1. \<And>y' x ov ov'. \<lbrakk>ko_at' ntfn ntfnptr s; invs' s; cnotification_relation (cslift t') ntfn' notification; map_to_ntfns (ksPSpace s) ntfnptr = Some ntfn; map_to_ntfns (ksPSpace s) ntfnptr = Some ntfn; cnotification_relation (cslift t) ntfn y'; cslift t (ntfn_Ptr ntfnptr) = Some y'; x \<noteq> ntfnptr; map_to_ntfns (ksPSpace s) x = Some ov; cslift t (ntfn_Ptr x) = Some ov'; cnotification_relation (cslift t) ov ov'\<rbrakk> \<Longrightarrow> cnotification_relation (cslift t') ov ov'
 2. \<And>y'. \<lbrakk>ko_at' ntfn ntfnptr s; invs' s; cnotification_relation (cslift t') ntfn' notification; map_to_ntfns (ksPSpace s) ntfnptr = Some ntfn; map_to_ntfns (ksPSpace s) ntfnptr = Some ntfn; cnotification_relation (cslift t) ntfn y'; cslift t (ntfn_Ptr ntfnptr) = Some y'\<rbrakk> \<Longrightarrow> inj ntfn_Ptr proof (prove)
goal (4 subgoals):
 1. \<And>y' x ov ov'. \<lbrakk>ko_at' ntfn ntfnptr s; invs' s; cnotification_relation (cslift t') ntfn' notification; map_to_ntfns (ksPSpace s) ntfnptr = Some ntfn; map_to_ntfns (ksPSpace s) ntfnptr = Some ntfn; cnotification_relation (cslift t) ntfn y'; cslift t (ntfn_Ptr ntfnptr) = Some y'; x \<noteq> ntfnptr; map_to_ntfns (ksPSpace s) x = Some ov; cslift t (ntfn_Ptr x) = Some ov'\<rbrakk> \<Longrightarrow> ko_at' ov (?ntfnptr'16 y' x ov ov') s
 2. \<And>y' x ov ov'. \<lbrakk>ko_at' ntfn ntfnptr s; invs' s; cnotification_relation (cslift t') ntfn' notification; map_to_ntfns (ksPSpace s) ntfnptr = Some ntfn; map_to_ntfns (ksPSpace s) ntfnptr = Some ntfn; cnotification_relation (cslift t) ntfn y'; cslift t (ntfn_Ptr ntfnptr) = Some y'; x \<noteq> ntfnptr; map_to_ntfns (ksPSpace s) x = Some ov; cslift t (ntfn_Ptr x) = Some ov'\<rbrakk> \<Longrightarrow> cslift t'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` (if isWaitingNtfn (ntfnObj ntfn) then set (ntfnQueue (ntfnObj ntfn)) else {}))\<^esub> = cslift t|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` (if isWaitingNtfn (ntfnObj ntfn) then set (ntfnQueue (ntfnObj ntfn)) else {}))\<^esub>
 3. \<And>y' x ov ov'. \<lbrakk>ko_at' ntfn ntfnptr s; invs' s; cnotification_relation (cslift t') ntfn' notification; map_to_ntfns (ksPSpace s) ntfnptr = Some ntfn; map_to_ntfns (ksPSpace s) ntfnptr = Some ntfn; cnotification_relation (cslift t) ntfn y'; cslift t (ntfn_Ptr ntfnptr) = Some y'; x \<noteq> ntfnptr; map_to_ntfns (ksPSpace s) x = Some ov; cslift t (ntfn_Ptr x) = Some ov'\<rbrakk> \<Longrightarrow> ?ntfnptr'16 y' x ov ov' \<noteq> ntfnptr
 4. \<And>y'. \<lbrakk>ko_at' ntfn ntfnptr s; invs' s; cnotification_relation (cslift t') ntfn' notification; map_to_ntfns (ksPSpace s) ntfnptr = Some ntfn; map_to_ntfns (ksPSpace s) ntfnptr = Some ntfn; cnotification_relation (cslift t) ntfn y'; cslift t (ntfn_Ptr ntfnptr) = Some y'\<rbrakk> \<Longrightarrow> inj ntfn_Ptr proof (prove)
goal (3 subgoals):
 1. \<And>y' x ov ov'. \<lbrakk>ko_at' ntfn ntfnptr s; invs' s; cnotification_relation (cslift t') ntfn' notification; map_to_ntfns (ksPSpace s) ntfnptr = Some ntfn; map_to_ntfns (ksPSpace s) ntfnptr = Some ntfn; cnotification_relation (cslift t) ntfn y'; cslift t (ntfn_Ptr ntfnptr) = Some y'; x \<noteq> ntfnptr; map_to_ntfns (ksPSpace s) x = Some ov; cslift t (ntfn_Ptr x) = Some ov'\<rbrakk> \<Longrightarrow> cslift t'|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` (if isWaitingNtfn (ntfnObj ntfn) then set (ntfnQueue (ntfnObj ntfn)) else {}))\<^esub> = cslift t|\<^bsub>(- tcb_ptr_to_ctcb_ptr ` (if isWaitingNtfn (ntfnObj ntfn) then set (ntfnQueue (ntfnObj ntfn)) else {}))\<^esub>
 2. \<And>y' x ov ov'. \<lbrakk>ko_at' ntfn ntfnptr s; invs' s; cnotification_relation (cslift t') ntfn' notification; map_to_ntfns (ksPSpace s) ntfnptr = Some ntfn; map_to_ntfns (ksPSpace s) ntfnptr = Some ntfn; cnotification_relation (cslift t) ntfn y'; cslift t (ntfn_Ptr ntfnptr) = Some y'; x \<noteq> ntfnptr; map_to_ntfns (ksPSpace s) x = Some ov; cslift t (ntfn_Ptr x) = Some ov'\<rbrakk> \<Longrightarrow> x \<noteq> ntfnptr
 3. \<And>y'. \<lbrakk>ko_at' ntfn ntfnptr s; invs' s; cnotification_relation (cslift t') ntfn' notification; map_to_ntfns (ksPSpace s) ntfnptr = Some ntfn; map_to_ntfns (ksPSpace s) ntfnptr = Some ntfn; cnotification_relation (cslift t) ntfn y'; cslift t (ntfn_Ptr ntfnptr) = Some y'\<rbrakk> \<Longrightarrow> inj ntfn_Ptr proof (prove)
goal (2 subgoals):
 1. \<And>y' x ov ov'. \<lbrakk>ko_at' ntfn ntfnptr s; invs' s; cnotification_relation (cslift t') ntfn' notification; map_to_ntfns (ksPSpace s) ntfnptr = Some ntfn; map_to_ntfns (ksPSpace s) ntfnptr = Some ntfn; cnotification_relation (cslift t) ntfn y'; cslift t (ntfn_Ptr ntfnptr) = Some y'; x \<noteq> ntfnptr; map_to_ntfns (ksPSpace s) x = Some ov; cslift t (ntfn_Ptr x) = Some ov'\<rbrakk> \<Longrightarrow> x \<noteq> ntfnptr
 2. \<And>y'. \<lbrakk>ko_at' ntfn ntfnptr s; invs' s; cnotification_relation (cslift t') ntfn' notification; map_to_ntfns (ksPSpace s) ntfnptr = Some ntfn; map_to_ntfns (ksPSpace s) ntfnptr = Some ntfn; cnotification_relation (cslift t) ntfn y'; cslift t (ntfn_Ptr ntfnptr) = Some y'\<rbrakk> \<Longrightarrow> inj ntfn_Ptr proof (prove)
goal (1 subgoal):
 1. \<And>y'. \<lbrakk>ko_at' ntfn ntfnptr s; invs' s; cnotification_relation (cslift t') ntfn' notification; map_to_ntfns (ksPSpace s) ntfnptr = Some ntfn; map_to_ntfns (ksPSpace s) ntfnptr = Some ntfn; cnotification_relation (cslift t) ntfn y'; cslift t (ntfn_Ptr ntfnptr) = Some y'\<rbrakk> \<Longrightarrow> inj ntfn_Ptr proof (prove)
goal:
No subgoals!