theory CSpace1_R

lemma descendants_of_eq':
  assumes "cte_at p s"
  assumes "cte_at src s"
  assumes "cdt_relation (swp cte_at s) (cdt s) m'"
  assumes "valid_mdb s"
  assumes "valid_objs s" "pspace_aligned s" "pspace_distinct s"
  shows "(cte_map src \<in> descendants_of' (cte_map p) m') = (src \<in> descendants_of p (cdt s))" using assms apply (simp add: cdt_relation_def del: split_paired_All) apply (rule iffI) prefer 2 apply (auto simp del: split_paired_All)[1] apply (erule_tac x=p in allE) apply simp apply (drule sym) apply clarsimp apply (frule (1) descendants_of_cte_at) apply (drule (5) cte_map_inj_eq) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (cte_map src \<in> descendants_of' (cte_map p) m') = (src \<in> descendants_of p (cdt s)) proof (prove)
using this:
cte_wp_at (\<lambda>_. True) p s
cte_wp_at (\<lambda>_. True) src s
cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) m'
valid_mdb s
valid_objs s
pspace_aligned s
pspace_distinct s

goal (1 subgoal):
 1. (cte_map src \<in> descendants_of' (cte_map p) m') = (src \<in> descendants_of p (cdt s)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_wp_at (\<lambda>_. True) src s; \<forall>c. cte_wp_at (\<lambda>_. True) c s \<longrightarrow> cte_map ` descendants_of c (cdt s) = descendants_of' (cte_map c) m'; valid_mdb s; valid_objs s; pspace_aligned s; pspace_distinct s\<rbrakk> \<Longrightarrow> (cte_map src \<in> descendants_of' (cte_map p) m') = (src \<in> descendants_of p (cdt s)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_wp_at (\<lambda>_. True) src s; \<forall>c. cte_wp_at (\<lambda>_. True) c s \<longrightarrow> cte_map ` descendants_of c (cdt s) = descendants_of' (cte_map c) m'; valid_mdb s; valid_objs s; pspace_aligned s; pspace_distinct s; cte_map src \<in> descendants_of' (cte_map p) m'\<rbrakk> \<Longrightarrow> src \<in> descendants_of p (cdt s)
 2. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_wp_at (\<lambda>_. True) src s; \<forall>c. cte_wp_at (\<lambda>_. True) c s \<longrightarrow> cte_map ` descendants_of c (cdt s) = descendants_of' (cte_map c) m'; valid_mdb s; valid_objs s; pspace_aligned s; pspace_distinct s; src \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> cte_map src \<in> descendants_of' (cte_map p) m' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_wp_at (\<lambda>_. True) src s; \<forall>c. cte_wp_at (\<lambda>_. True) c s \<longrightarrow> cte_map ` descendants_of c (cdt s) = descendants_of' (cte_map c) m'; valid_mdb s; valid_objs s; pspace_aligned s; pspace_distinct s; src \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> cte_map src \<in> descendants_of' (cte_map p) m'
 2. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_wp_at (\<lambda>_. True) src s; \<forall>c. cte_wp_at (\<lambda>_. True) c s \<longrightarrow> cte_map ` descendants_of c (cdt s) = descendants_of' (cte_map c) m'; valid_mdb s; valid_objs s; pspace_aligned s; pspace_distinct s; cte_map src \<in> descendants_of' (cte_map p) m'\<rbrakk> \<Longrightarrow> src \<in> descendants_of p (cdt s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_wp_at (\<lambda>_. True) src s; \<forall>c. cte_wp_at (\<lambda>_. True) c s \<longrightarrow> cte_map ` descendants_of c (cdt s) = descendants_of' (cte_map c) m'; valid_mdb s; valid_objs s; pspace_aligned s; pspace_distinct s; cte_map src \<in> descendants_of' (cte_map p) m'\<rbrakk> \<Longrightarrow> src \<in> descendants_of p (cdt s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_wp_at (\<lambda>_. True) src s; valid_mdb s; valid_objs s; pspace_aligned s; pspace_distinct s; cte_map src \<in> descendants_of' (cte_map p) m'; cte_wp_at (\<lambda>_. True) p s \<longrightarrow> cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) m'\<rbrakk> \<Longrightarrow> src \<in> descendants_of p (cdt s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_wp_at (\<lambda>_. True) src s; valid_mdb s; valid_objs s; pspace_aligned s; pspace_distinct s; cte_map src \<in> descendants_of' (cte_map p) m'; cte_map ` descendants_of p (cdt s) = descendants_of' (cte_map p) m'\<rbrakk> \<Longrightarrow> src \<in> descendants_of p (cdt s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_wp_at (\<lambda>_. True) src s; valid_mdb s; valid_objs s; pspace_aligned s; pspace_distinct s; cte_map src \<in> descendants_of' (cte_map p) m'; descendants_of' (cte_map p) m' = cte_map ` descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> src \<in> descendants_of p (cdt s) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_wp_at (\<lambda>_. True) src s; valid_mdb s; valid_objs s; pspace_aligned s; pspace_distinct s; descendants_of' (cte_map p) m' = cte_map ` descendants_of p (cdt s); cte_map src = cte_map (a, b); (a, b) \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> src \<in> descendants_of p (cdt s) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_wp_at (\<lambda>_. True) src s; valid_mdb s; valid_objs s; pspace_aligned s; pspace_distinct s; descendants_of' (cte_map p) m' = cte_map ` descendants_of p (cdt s); cte_map src = cte_map (a, b); (a, b) \<in> descendants_of p (cdt s); cte_wp_at (\<lambda>_. True) (a, b) s\<rbrakk> \<Longrightarrow> src \<in> descendants_of p (cdt s) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_wp_at (\<lambda>_. True) src s; valid_mdb s; valid_objs s; pspace_aligned s; pspace_distinct s; descendants_of' (cte_map p) m' = cte_map ` descendants_of p (cdt s); (a, b) \<in> descendants_of p (cdt s); cte_wp_at (\<lambda>_. True) (a, b) s; src = (a, b)\<rbrakk> \<Longrightarrow> src \<in> descendants_of p (cdt s) proof (prove)
goal:
No subgoals!