theory CSpace_R

lemma setCTE_corres:
  "cap_relation cap (cteCap cte) \<Longrightarrow>
   corres_underlying {(s, s'). pspace_relations (ekheap (s)) (kheap s) (ksPSpace s')} False True dc
      (pspace_distinct and pspace_aligned and valid_objs and cte_at p)
      (pspace_aligned' and pspace_distinct' and cte_at' (cte_map p))
      (set_cap cap p)
      (setCTE (cte_map p) cte)" apply (rule corres_no_failI) apply (rule no_fail_pre, wp) apply simp apply clarsimp apply (drule(8) set_cap_not_quite_corres_prequel) apply simp apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_relation cap (cteCap cte) \<Longrightarrow> corres_underlying {(s, s'). pspace_relations (ekheap s) (kheap s) (ksPSpace s')} False True dc (pspace_distinct and pspace_aligned and valid_objs and cte_wp_at (\<lambda>_. True) p) (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p)) (set_cap cap p) (setCTE (cte_map p) cte) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cap_relation cap (cteCap cte); True\<rbrakk> \<Longrightarrow> no_fail (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p)) (setCTE (cte_map p) cte)
 2. cap_relation cap (cteCap cte) \<Longrightarrow> \<forall>(s, s')\<in>{(s, s'). pspace_relations (ekheap s) (kheap s) (ksPSpace s')}. (pspace_distinct and pspace_aligned and valid_objs and cte_wp_at (\<lambda>_. True) p) s \<and> (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p)) s' \<longrightarrow> (\<forall>(r', t')\<in>fst (setCTE (cte_map p) cte s'). \<exists>(r, t)\<in>fst (set_cap cap p s). (t, t') \<in> {(s, s'). pspace_relations (ekheap s) (kheap s) (ksPSpace s')} \<and> dc r r') proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>cap_relation cap (cteCap cte); True; (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p)) s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (cte_map p) s
 2. cap_relation cap (cteCap cte) \<Longrightarrow> \<forall>(s, s')\<in>{(s, s'). pspace_relations (ekheap s) (kheap s) (ksPSpace s')}. (pspace_distinct and pspace_aligned and valid_objs and cte_wp_at (\<lambda>_. True) p) s \<and> (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p)) s' \<longrightarrow> (\<forall>(r', t')\<in>fst (setCTE (cte_map p) cte s'). \<exists>(r, t)\<in>fst (set_cap cap p s). (t, t') \<in> {(s, s'). pspace_relations (ekheap s) (kheap s) (ksPSpace s')} \<and> dc r r') proof (prove)
goal (1 subgoal):
 1. cap_relation cap (cteCap cte) \<Longrightarrow> \<forall>(s, s')\<in>{(s, s'). pspace_relations (ekheap s) (kheap s) (ksPSpace s')}. (pspace_distinct and pspace_aligned and valid_objs and cte_wp_at (\<lambda>_. True) p) s \<and> (pspace_aligned' and pspace_distinct' and cte_wp_at' (\<lambda>_. True) (cte_map p)) s' \<longrightarrow> (\<forall>(r', t')\<in>fst (setCTE (cte_map p) cte s'). \<exists>(r, t)\<in>fst (set_cap cap p s). (t, t') \<in> {(s, s'). pspace_relations (ekheap s) (kheap s) (ksPSpace s')} \<and> dc r r') proof (prove)
goal (1 subgoal):
 1. \<And>a b ba. \<lbrakk>cap_relation cap (cteCap cte); pspace_relations (ekheap a) (kheap a) (ksPSpace b); ((), ba) \<in> fst (setCTE (cte_map p) cte b); pspace_distinct a; pspace_aligned a; valid_objs a; cte_wp_at (\<lambda>_. True) p a; pspace_aligned' b; pspace_distinct' b; cte_wp_at' (\<lambda>_. True) (cte_map p) b\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (set_cap cap p a). case x of (r, t) \<Rightarrow> pspace_relations (ekheap t) (kheap t) (ksPSpace ba) proof (prove)
goal (2 subgoals):
 1. \<And>a b ba. \<lbrakk>cap_relation cap (cteCap cte); ((), ba) \<in> fst (setCTE (cte_map p) cte b); pspace_distinct a; pspace_aligned a; valid_objs a; cte_wp_at (\<lambda>_. True) p a; pspace_aligned' b; pspace_distinct' b; cte_wp_at' (\<lambda>_. True) (cte_map p) b\<rbrakk> \<Longrightarrow> cte_map p = cte_map p
 2. \<And>a b ba. \<lbrakk>cap_relation cap (cteCap cte); ((), ba) \<in> fst (setCTE (cte_map p) cte b); pspace_distinct a; pspace_aligned a; valid_objs a; cte_wp_at (\<lambda>_. True) p a; pspace_aligned' b; pspace_distinct' b; cte_wp_at' (\<lambda>_. True) (cte_map p) b; \<exists>t. ((), t) \<in> fst (set_cap cap p a) \<and> pspace_relations (ekheap t) (kheap t) (ksPSpace ba)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (set_cap cap p a). case x of (r, t) \<Rightarrow> pspace_relations (ekheap t) (kheap t) (ksPSpace ba) proof (prove)
goal (1 subgoal):
 1. \<And>a b ba. \<lbrakk>cap_relation cap (cteCap cte); ((), ba) \<in> fst (setCTE (cte_map p) cte b); pspace_distinct a; pspace_aligned a; valid_objs a; cte_wp_at (\<lambda>_. True) p a; pspace_aligned' b; pspace_distinct' b; cte_wp_at' (\<lambda>_. True) (cte_map p) b; \<exists>t. ((), t) \<in> fst (set_cap cap p a) \<and> pspace_relations (ekheap t) (kheap t) (ksPSpace ba)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (set_cap cap p a). case x of (r, t) \<Rightarrow> pspace_relations (ekheap t) (kheap t) (ksPSpace ba) proof (prove)
goal:
No subgoals!