theory Recycle_C

lemma cpspace_relation_ep_update_ep2:
  "\<lbrakk> ko_at' (ep :: endpoint) epptr s;
      cmap_relation (map_to_eps (ksPSpace s))
           (cslift t) ep_Ptr (cendpoint_relation (cslift t));
      cendpoint_relation (cslift t') ep' endpoint;
      (cslift t' :: tcb_C ptr \<rightharpoonup> tcb_C) = cslift t \<rbrakk>
     \<Longrightarrow> cmap_relation (map_to_eps ((ksPSpace s)(epptr \<mapsto> KOEndpoint ep')))
          ((cslift t)(ep_Ptr epptr \<mapsto> endpoint))
          ep_Ptr (cendpoint_relation (cslift t'))" apply (rule cmap_relationE1, assumption, erule ko_at_projectKO_opt) apply (rule_tac P="\<lambda>a. cmap_relation a b c d" for b c d in rsubst,
                   erule cmap_relation_upd_relI, assumption+) apply simp+ apply (rule ext, simp add: map_comp_def projectKO_opt_ep split: if_split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at' ep epptr s; cmap_relation (map_to_eps (ksPSpace s)) (cslift t) ep_Ptr (cendpoint_relation (cslift t)); cendpoint_relation (cslift t') ep' endpoint; cslift t' = cslift t\<rbrakk> \<Longrightarrow> cmap_relation (map_to_eps ((ksPSpace s)(epptr \<mapsto> KOEndpoint ep'))) ((cslift t)(ep_Ptr epptr \<mapsto> endpoint)) ep_Ptr (cendpoint_relation (cslift t')) proof (prove)
goal (1 subgoal):
 1. \<And>y'. \<lbrakk>ko_at' ep epptr s; cmap_relation (map_to_eps (ksPSpace s)) (cslift t) ep_Ptr (cendpoint_relation (cslift t)); cendpoint_relation (cslift t') ep' endpoint; cslift t' = cslift t; map_to_eps (ksPSpace s) epptr = Some ep; cendpoint_relation (cslift t) ep y'; cslift t (ep_Ptr epptr) = Some y'\<rbrakk> \<Longrightarrow> cmap_relation (map_to_eps ((ksPSpace s)(epptr \<mapsto> KOEndpoint ep'))) ((cslift t)(ep_Ptr epptr \<mapsto> endpoint)) ep_Ptr (cendpoint_relation (cslift t')) proof (prove)
goal (3 subgoals):
 1. \<And>y' x ov ov'. \<lbrakk>ko_at' ep epptr s; cendpoint_relation (cslift t') ep' endpoint; cslift t' = cslift t; map_to_eps (ksPSpace s) epptr = Some ep; cendpoint_relation (cslift t) ep y'; cslift t (ep_Ptr epptr) = Some y'; x \<noteq> epptr; map_to_eps (ksPSpace s) x = Some ov; cslift t (ep_Ptr x) = Some ov'; cendpoint_relation (cslift t) ov ov'\<rbrakk> \<Longrightarrow> cendpoint_relation (cslift t') ov ov'
 2. \<And>y'. \<lbrakk>ko_at' ep epptr s; cendpoint_relation (cslift t') ep' endpoint; cslift t' = cslift t; map_to_eps (ksPSpace s) epptr = Some ep; cendpoint_relation (cslift t) ep y'; cslift t (ep_Ptr epptr) = Some y'\<rbrakk> \<Longrightarrow> inj ep_Ptr
 3. \<And>y'. \<lbrakk>ko_at' ep epptr s; cmap_relation (map_to_eps (ksPSpace s)) (cslift t) ep_Ptr (cendpoint_relation (cslift t)); cendpoint_relation (cslift t') ep' endpoint; cslift t' = cslift t; map_to_eps (ksPSpace s) epptr = Some ep; cendpoint_relation (cslift t) ep y'; cslift t (ep_Ptr epptr) = Some y'\<rbrakk> \<Longrightarrow> (map_to_eps (ksPSpace s))(epptr \<mapsto> ep') = map_to_eps ((ksPSpace s)(epptr \<mapsto> KOEndpoint ep')) proof (prove)
goal (1 subgoal):
 1. \<And>y'. \<lbrakk>ko_at' ep epptr s; cmap_relation (map_to_eps (ksPSpace s)) (cslift t) ep_Ptr (cendpoint_relation (cslift t)); cendpoint_relation (cslift t) ep' endpoint; cslift t' = cslift t; map_to_eps (ksPSpace s) epptr = Some ep; cendpoint_relation (cslift t) ep y'; cslift t (ep_Ptr epptr) = Some y'\<rbrakk> \<Longrightarrow> (map_to_eps (ksPSpace s))(epptr \<mapsto> ep') = map_to_eps ((ksPSpace s)(epptr \<mapsto> KOEndpoint ep')) proof (prove)
goal:
No subgoals!