theory IpcCancel_C

lemma cpspace_relation_ep_update_ep':
  fixes ep :: "endpoint" and ep' :: "endpoint"
    and epptr :: "word32" and s :: "kernel_state"
  defines "qs \<equiv> if (isSendEP ep' \<or> isRecvEP ep') then set (epQueue ep') else {}"
  defines "s' \<equiv> s\<lparr>ksPSpace := (ksPSpace s)(epptr \<mapsto> KOEndpoint ep')\<rparr>"
  assumes koat: "ko_at' ep epptr s"
  and       vp: "valid_pspace' s"
  and      cp: "cmap_relation (map_to_eps (ksPSpace s)) (cslift t) Ptr (cendpoint_relation mp)"
  and      srs: "sym_refs (state_refs_of' s')"
  and     rel: "cendpoint_relation mp' ep' endpoint"
  and    mpeq: "(mp' |` (- (tcb_ptr_to_ctcb_ptr ` qs))) = (mp |` (- (tcb_ptr_to_ctcb_ptr ` qs)))"
  shows "cmap_relation (map_to_eps ((ksPSpace s)(epptr \<mapsto> KOEndpoint ep')))
           ((cslift t)(Ptr epptr \<mapsto> endpoint)) Ptr (cendpoint_relation mp')" proof - from koat have koat': "ko_at' ep' epptr s'" by (clarsimp simp: obj_at'_def s'_def objBitsKO_def ps_clear_def projectKOs) from koat have koat'': "\<And>ep'' epptr'. \<lbrakk> ko_at' ep'' epptr' s; epptr' \<noteq> epptr \<rbrakk>
              \<Longrightarrow> ko_at' ep'' epptr' s'" by (clarsimp simp: obj_at'_def s'_def objBitsKO_def ps_clear_def projectKOs) show ?thesis using vp ep_ep_disjoint[OF srs koat'' koat' endpoint_not_idle_cases] apply (intro cpspace_relation_ep_update_an_ep[OF koat cp rel mpeq]) apply clarsimp+ apply (clarsimp simp add: qs_def image_image simp del: imp_disjL) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cmap_relation (map_to_eps ((ksPSpace s)(epptr \<mapsto> KOEndpoint ep'))) ((cslift t)(ep_Ptr epptr \<mapsto> endpoint)) ep_Ptr (cendpoint_relation mp') proof (state)
goal (1 subgoal):
 1. cmap_relation (map_to_eps ((ksPSpace s)(epptr \<mapsto> KOEndpoint ep'))) ((cslift t)(ep_Ptr epptr \<mapsto> endpoint)) ep_Ptr (cendpoint_relation mp') proof (chain)
picking this:
ko_at' ep epptr s proof (prove)
using this:
ko_at' ep epptr s

goal (1 subgoal):
 1. ko_at' ep' epptr s' proof (state)
this:
ko_at' ep' epptr s'

goal (1 subgoal):
 1. cmap_relation (map_to_eps ((ksPSpace s)(epptr \<mapsto> KOEndpoint ep'))) ((cslift t)(ep_Ptr epptr \<mapsto> endpoint)) ep_Ptr (cendpoint_relation mp') proof (chain)
picking this:
ko_at' ep epptr s proof (prove)
using this:
ko_at' ep epptr s

goal (1 subgoal):
 1. \<And>ep'' epptr'. \<lbrakk>ko_at' ep'' epptr' s; epptr' \<noteq> epptr\<rbrakk> \<Longrightarrow> ko_at' ep'' epptr' s' proof (state)
this:
\<lbrakk>ko_at' ?ep''1 ?epptr'1 s; ?epptr'1 \<noteq> epptr\<rbrakk> \<Longrightarrow> ko_at' ?ep''1 ?epptr'1 s'

goal (1 subgoal):
 1. cmap_relation (map_to_eps ((ksPSpace s)(epptr \<mapsto> KOEndpoint ep'))) ((cslift t)(ep_Ptr epptr \<mapsto> endpoint)) ep_Ptr (cendpoint_relation mp') proof (prove)
goal (1 subgoal):
 1. cmap_relation (map_to_eps ((ksPSpace s)(epptr \<mapsto> KOEndpoint ep'))) ((cslift t)(ep_Ptr epptr \<mapsto> endpoint)) ep_Ptr (cendpoint_relation mp') proof (prove)
using this:
valid_pspace' s
\<lbrakk>ko_at' ?ep ?epptr s; ?epptr \<noteq> epptr; ?ep \<noteq> Structures_H.endpoint.IdleEP; isSendEP ep' \<or> isRecvEP ep'; epptr \<noteq> ?epptr\<rbrakk> \<Longrightarrow> set (epQueue ?ep) \<inter> set (epQueue ep') = {}

goal (1 subgoal):
 1. cmap_relation (map_to_eps ((ksPSpace s)(epptr \<mapsto> KOEndpoint ep'))) ((cslift t)(ep_Ptr epptr \<mapsto> endpoint)) ep_Ptr (cendpoint_relation mp') proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_pspace' s; \<And>ep epptra. \<lbrakk>ko_at' ep epptra s; epptra \<noteq> epptr; ep \<noteq> Structures_H.endpoint.IdleEP; isSendEP ep' \<or> isRecvEP ep'; epptr \<noteq> epptra\<rbrakk> \<Longrightarrow> set (epQueue ep) \<inter> set (epQueue ep') = {}\<rbrakk> \<Longrightarrow> pspace_aligned' s
 2. \<lbrakk>valid_pspace' s; \<And>ep epptra. \<lbrakk>ko_at' ep epptra s; epptra \<noteq> epptr; ep \<noteq> Structures_H.endpoint.IdleEP; isSendEP ep' \<or> isRecvEP ep'; epptr \<noteq> epptra\<rbrakk> \<Longrightarrow> set (epQueue ep) \<inter> set (epQueue ep') = {}\<rbrakk> \<Longrightarrow> pspace_distinct' s
 3. \<And>epptr' ep'a. \<lbrakk>valid_pspace' s; \<And>ep epptra. \<lbrakk>ko_at' ep epptra s; epptra \<noteq> epptr; ep \<noteq> Structures_H.endpoint.IdleEP; isSendEP ep' \<or> isRecvEP ep'; epptr \<noteq> epptra\<rbrakk> \<Longrightarrow> set (epQueue ep) \<inter> set (epQueue ep') = {}; ko_at' ep'a epptr' s; epptr' \<noteq> epptr; ep'a \<noteq> Structures_H.endpoint.IdleEP\<rbrakk> \<Longrightarrow> set (epQueue ep'a) \<inter> ctcb_ptr_to_tcb_ptr ` tcb_ptr_to_ctcb_ptr ` qs = {} proof (prove)
goal (1 subgoal):
 1. \<And>epptr' ep'a. \<lbrakk>valid_pspace' s; \<And>ep epptra. \<lbrakk>ko_at' ep epptra s; ep \<noteq> Structures_H.endpoint.IdleEP; isSendEP ep' \<or> isRecvEP ep'; epptr \<noteq> epptra\<rbrakk> \<Longrightarrow> set (epQueue ep) \<inter> set (epQueue ep') = {}; ko_at' ep'a epptr' s; epptr' \<noteq> epptr; ep'a \<noteq> Structures_H.endpoint.IdleEP\<rbrakk> \<Longrightarrow> set (epQueue ep'a) \<inter> ctcb_ptr_to_tcb_ptr ` tcb_ptr_to_ctcb_ptr ` qs = {} proof (prove)
goal:
No subgoals! proof (state)
this:
cmap_relation (map_to_eps ((ksPSpace s)(epptr \<mapsto> KOEndpoint ep'))) ((cslift t)(ep_Ptr epptr \<mapsto> endpoint)) ep_Ptr (cendpoint_relation mp')

goal:
No subgoals!