theory SR_lemmas_C

lemma cpspace_cte_relation_upd_capI:
  assumes cr: "cmap_relation (map_to_ctes am) (clift cm) Ptr ccte_relation"
  and   cof: "map_to_ctes am dest = Some cte"
  and   cl:  "clift cm (Ptr dest) = Some cte'"
  and   cc:  "ccap_relation capl cap"
  shows "cmap_relation ((map_to_ctes am)(dest \<mapsto>  (cteCap_update (\<lambda>_. capl) cte)))
  ((clift cm)(Ptr dest \<mapsto> cte_C.cap_C_update (\<lambda>_. cap) cte')) Ptr ccte_relation" using cr cof cl cc apply - apply (frule (2) cmap_relation_relI) apply (erule (2) cmap_relation_updI) apply (clarsimp elim!: ccap_relationE simp: map_comp_Some_iff ccte_relation_def) apply (subst (asm) map_option_Some_eq2) apply clarsimp apply (simp add: c_valid_cte_def cl_valid_cte_def) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cmap_relation ((map_to_ctes am)(dest \<mapsto> cteCap_update (\<lambda>_. capl) cte)) ((clift cm)(cte_Ptr dest \<mapsto> cte_C.cap_C_update (\<lambda>_. cap) cte')) cte_Ptr ccte_relation proof (prove)
using this:
cmap_relation (map_to_ctes am) (clift cm) cte_Ptr ccte_relation
map_to_ctes am dest = Some cte
clift cm (cte_Ptr dest) = Some cte'
ccap_relation capl cap

goal (1 subgoal):
 1. cmap_relation ((map_to_ctes am)(dest \<mapsto> cteCap_update (\<lambda>_. capl) cte)) ((clift cm)(cte_Ptr dest \<mapsto> cte_C.cap_C_update (\<lambda>_. cap) cte')) cte_Ptr ccte_relation proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cmap_relation (map_to_ctes am) (clift cm) cte_Ptr ccte_relation; map_to_ctes am dest = Some cte; clift cm (cte_Ptr dest) = Some cte'; ccap_relation capl cap\<rbrakk> \<Longrightarrow> cmap_relation ((map_to_ctes am)(dest \<mapsto> cteCap_update (\<lambda>_. capl) cte)) ((clift cm)(cte_Ptr dest \<mapsto> cte_C.cap_C_update (\<lambda>_. cap) cte')) cte_Ptr ccte_relation proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cmap_relation (map_to_ctes am) (clift cm) cte_Ptr ccte_relation; map_to_ctes am dest = Some cte; clift cm (cte_Ptr dest) = Some cte'; ccap_relation capl cap; ccte_relation cte cte'\<rbrakk> \<Longrightarrow> cmap_relation ((map_to_ctes am)(dest \<mapsto> cteCap_update (\<lambda>_. capl) cte)) ((clift cm)(cte_Ptr dest \<mapsto> cte_C.cap_C_update (\<lambda>_. cap) cte')) cte_Ptr ccte_relation proof (prove)
goal (2 subgoals):
 1. \<lbrakk>map_to_ctes am dest = Some cte; clift cm (cte_Ptr dest) = Some cte'; ccap_relation capl cap; ccte_relation cte cte'\<rbrakk> \<Longrightarrow> ccte_relation (cteCap_update (\<lambda>_. capl) cte) (cte_C.cap_C_update (\<lambda>_. cap) cte')
 2. \<lbrakk>map_to_ctes am dest = Some cte; clift cm (cte_Ptr dest) = Some cte'; ccap_relation capl cap; ccte_relation cte cte'\<rbrakk> \<Longrightarrow> inj cte_Ptr proof (prove)
goal (2 subgoals):
 1. \<And>vl. \<lbrakk>map_to_ctes am dest = map_option cte_to_H (cte_lift cte'); clift cm (cte_Ptr dest) = Some cte'; cap_lift cap = Some vl; c_valid_cap cap; capl = cap_to_H vl; Some cte = map_option cte_to_H (cte_lift cte'); c_valid_cte cte'\<rbrakk> \<Longrightarrow> Some (cteCap_update (\<lambda>_. cap_to_H vl) cte) = map_option cte_to_H (cte_lift (cte_C.cap_C_update (\<lambda>_. cap) cte')) \<and> c_valid_cte (cte_C.cap_C_update (\<lambda>_. cap) cte')
 2. \<lbrakk>map_to_ctes am dest = Some cte; clift cm (cte_Ptr dest) = Some cte'; ccap_relation capl cap; ccte_relation cte cte'\<rbrakk> \<Longrightarrow> inj cte_Ptr proof (prove)
goal (2 subgoals):
 1. \<And>vl. \<lbrakk>map_to_ctes am dest = map_option cte_to_H (cte_lift cte'); clift cm (cte_Ptr dest) = Some cte'; cap_lift cap = Some vl; c_valid_cap cap; capl = cap_to_H vl; \<exists>z. cte_lift cte' = Some z \<and> cte_to_H z = cte; c_valid_cte cte'\<rbrakk> \<Longrightarrow> Some (cteCap_update (\<lambda>_. cap_to_H vl) cte) = map_option cte_to_H (cte_lift (cte_C.cap_C_update (\<lambda>_. cap) cte')) \<and> c_valid_cte (cte_C.cap_C_update (\<lambda>_. cap) cte')
 2. \<lbrakk>map_to_ctes am dest = Some cte; clift cm (cte_Ptr dest) = Some cte'; ccap_relation capl cap; ccte_relation cte cte'\<rbrakk> \<Longrightarrow> inj cte_Ptr proof (prove)
goal (2 subgoals):
 1. \<And>vl z. \<lbrakk>map_to_ctes am dest = Some (cte_to_H z); clift cm (cte_Ptr dest) = Some cte'; cap_lift cap = Some vl; c_valid_cap cap; capl = cap_to_H vl; c_valid_cte cte'; cte_lift cte' = Some z; cte = cte_to_H z\<rbrakk> \<Longrightarrow> c_valid_cte (cte_C.cap_C_update (\<lambda>_. cap) cte')
 2. \<lbrakk>map_to_ctes am dest = Some cte; clift cm (cte_Ptr dest) = Some cte'; ccap_relation capl cap; ccte_relation cte cte'\<rbrakk> \<Longrightarrow> inj cte_Ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>map_to_ctes am dest = Some cte; clift cm (cte_Ptr dest) = Some cte'; ccap_relation capl cap; ccte_relation cte cte'\<rbrakk> \<Longrightarrow> inj cte_Ptr proof (prove)
goal:
No subgoals!