theory IpcCancel_C

lemma cpspace_relation_ep_update_an_ep:
  fixes ep :: "endpoint"
  defines "qs \<equiv> if (isSendEP ep \<or> isRecvEP ep) then set (epQueue ep) else {}"
  assumes koat: "ko_at' ep epptr s"
  and      cp: "cmap_relation (map_to_eps (ksPSpace s)) (cslift t) Ptr (cendpoint_relation mp)"
  and     rel: "cendpoint_relation mp' ep' endpoint"
  and    mpeq: "(mp' |` (- S)) = (mp |` (- S))"
  and     pal: "pspace_aligned' s" "pspace_distinct' s"
  and  others: "\<And>epptr' ep'. \<lbrakk> ko_at' ep' epptr' s; epptr' \<noteq> epptr; ep' \<noteq> IdleEP \<rbrakk>
                                 \<Longrightarrow> set (epQueue ep') \<inter> (ctcb_ptr_to_tcb_ptr ` S) = {}"
  shows "cmap_relation (map_to_eps ((ksPSpace s)(epptr \<mapsto> KOEndpoint ep')))
           ((cslift t)(Ptr epptr \<mapsto> endpoint)) Ptr (cendpoint_relation mp')" using cp koat pal rel unfolding cmap_relation_def apply - apply (clarsimp elim!: obj_atE' simp: map_comp_update projectKO_opts_defs) apply (drule (1) bspec [OF _ domI]) apply simp apply (erule cendpoint_relation_ep_queue[OF _ mpeq]) apply (erule(4) others[OF map_to_ko_atI]) done

(* 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 (prove)
using this:
cmap_relation (map_to_eps (ksPSpace s)) (cslift t) ep_Ptr (cendpoint_relation mp)
ko_at' ep epptr s
pspace_aligned' s
pspace_distinct' s
cendpoint_relation mp' ep' endpoint

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:
ep_Ptr ` dom (map_to_eps (ksPSpace s)) = dom (cslift t) \<and> (\<forall>x\<in>dom (map_to_eps (ksPSpace s)). cendpoint_relation mp (the (map_to_eps (ksPSpace s) x)) (the (cslift t (ep_Ptr x))))
ko_at' ep epptr s
pspace_aligned' s
pspace_distinct' s
cendpoint_relation mp' ep' endpoint

goal (1 subgoal):
 1. ep_Ptr ` dom (map_to_eps ((ksPSpace s)(epptr \<mapsto> KOEndpoint ep'))) = dom ((cslift t)(ep_Ptr epptr \<mapsto> endpoint)) \<and> (\<forall>x\<in>dom (map_to_eps ((ksPSpace s)(epptr \<mapsto> KOEndpoint ep'))). cendpoint_relation mp' (the (map_to_eps ((ksPSpace s)(epptr \<mapsto> KOEndpoint ep')) x)) (the (((cslift t)(ep_Ptr epptr \<mapsto> endpoint)) (ep_Ptr x)))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ep_Ptr ` dom (map_to_eps (ksPSpace s)) = dom (cslift t) \<and> (\<forall>x\<in>dom (map_to_eps (ksPSpace s)). cendpoint_relation mp (the (map_to_eps (ksPSpace s) x)) (the (cslift t (ep_Ptr x)))); ko_at' ep epptr s; pspace_aligned' s; pspace_distinct' s; cendpoint_relation mp' ep' endpoint\<rbrakk> \<Longrightarrow> ep_Ptr ` dom (map_to_eps ((ksPSpace s)(epptr \<mapsto> KOEndpoint ep'))) = dom ((cslift t)(ep_Ptr epptr \<mapsto> endpoint)) \<and> (\<forall>x\<in>dom (map_to_eps ((ksPSpace s)(epptr \<mapsto> KOEndpoint ep'))). cendpoint_relation mp' (the (map_to_eps ((ksPSpace s)(epptr \<mapsto> KOEndpoint ep')) x)) (the (((cslift t)(ep_Ptr epptr \<mapsto> endpoint)) (ep_Ptr x)))) proof (prove)
goal (1 subgoal):
 1. \<And>ko x y. \<lbrakk>pspace_aligned' s; pspace_distinct' s; cendpoint_relation mp' ep' endpoint; ksPSpace s epptr = Some ko; is_aligned epptr (objBitsKO ko); fst (projectKO ko s) = {(ep, s)}; ps_clear epptr (objBitsKO ko) s; map_to_eps (ksPSpace s) x = Some y; ep_Ptr ` dom (map_to_eps (ksPSpace s)) = dom (cslift t); \<forall>x\<in>dom (map_to_eps (ksPSpace s)). cendpoint_relation mp (the (map_to_eps (ksPSpace s) x)) (the (cslift t (ep_Ptr x))); x \<noteq> epptr\<rbrakk> \<Longrightarrow> cendpoint_relation mp' y (the (cslift t (ep_Ptr x))) proof (prove)
goal (1 subgoal):
 1. \<And>ko x y. \<lbrakk>pspace_aligned' s; pspace_distinct' s; cendpoint_relation mp' ep' endpoint; ksPSpace s epptr = Some ko; is_aligned epptr (objBitsKO ko); fst (projectKO ko s) = {(ep, s)}; ps_clear epptr (objBitsKO ko) s; map_to_eps (ksPSpace s) x = Some y; ep_Ptr ` dom (map_to_eps (ksPSpace s)) = dom (cslift t); x \<noteq> epptr; cendpoint_relation mp (the (map_to_eps (ksPSpace s) x)) (the (cslift t (ep_Ptr x)))\<rbrakk> \<Longrightarrow> cendpoint_relation mp' y (the (cslift t (ep_Ptr x))) proof (prove)
goal (1 subgoal):
 1. \<And>ko x y. \<lbrakk>pspace_aligned' s; pspace_distinct' s; cendpoint_relation mp' ep' endpoint; ksPSpace s epptr = Some ko; is_aligned epptr (objBitsKO ko); fst (projectKO ko s) = {(ep, s)}; ps_clear epptr (objBitsKO ko) s; map_to_eps (ksPSpace s) x = Some y; ep_Ptr ` dom (map_to_eps (ksPSpace s)) = dom (cslift t); x \<noteq> epptr; cendpoint_relation mp y (the (cslift t (ep_Ptr x)))\<rbrakk> \<Longrightarrow> cendpoint_relation mp' y (the (cslift t (ep_Ptr x))) proof (prove)
goal (1 subgoal):
 1. \<And>ko x y. \<lbrakk>pspace_aligned' s; pspace_distinct' s; cendpoint_relation mp' ep' endpoint; ksPSpace s epptr = Some ko; is_aligned epptr (objBitsKO ko); fst (projectKO ko s) = {(ep, s)}; ps_clear epptr (objBitsKO ko) s; map_to_eps (ksPSpace s) x = Some y; ep_Ptr ` dom (map_to_eps (ksPSpace s)) = dom (cslift t); x \<noteq> epptr; y \<noteq> Structures_H.endpoint.IdleEP\<rbrakk> \<Longrightarrow> set (epQueue y) \<inter> ctcb_ptr_to_tcb_ptr ` S = {} proof (prove)
goal:
No subgoals!