theory Detype_AI

lemma descendants_range_imply_no_descendants:
  "\<lbrakk>descendants_range cap p s;descendants_inc (cdt s) (caps_of_state s);
  is_untyped_cap cap; caps_of_state s p = Some cap;valid_objs s;valid_mdb s\<rbrakk>
  \<Longrightarrow> descendants_of p (cdt s)= {}" apply (simp add:descendants_range_def is_cap_simps descendants_inc_def del:split_paired_All) apply (elim exE) apply (rule equals0I) apply (drule(1) bspec) apply (drule spec)+ apply (erule(1) impE) apply (drule(1) descendants_of_cte_at) apply (clarsimp simp:cte_wp_at_caps_of_state simp del:split_paired_All) apply (drule(1) physical_valid_cap_not_empty_range[OF caps_of_state_valid_cap,rotated]) apply simp apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>descendants_range cap p s; descendants_inc (cdt s) (caps_of_state s); is_untyped_cap cap; caps_of_state s p = Some cap; valid_objs s; valid_mdb s\<rbrakk> \<Longrightarrow> descendants_of p (cdt s) = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>p'\<in>descendants_of p (cdt s). cte_wp_at (\<lambda>c. cap_range c \<inter> untyped_range cap = {}) p' s; \<forall>p p'. p \<in> descendants_of p' (cdt s) \<longrightarrow> cap_class (the (caps_of_state s p)) = cap_class (the (caps_of_state s p')) \<and> cap_range (the (caps_of_state s p)) \<subseteq> cap_range (the (caps_of_state s p')); \<exists>dev r bits f. cap = UntypedCap dev r bits f; caps_of_state s p = Some cap; valid_objs s; valid_mdb s\<rbrakk> \<Longrightarrow> descendants_of p (cdt s) = {} proof (prove)
goal (1 subgoal):
 1. \<And>dev r bits f. \<lbrakk>\<forall>p'\<in>descendants_of p (cdt s). cte_wp_at (\<lambda>c. cap_range c \<inter> untyped_range cap = {}) p' s; \<forall>p p'. p \<in> descendants_of p' (cdt s) \<longrightarrow> cap_class (the (caps_of_state s p)) = cap_class (the (caps_of_state s p')) \<and> cap_range (the (caps_of_state s p)) \<subseteq> cap_range (the (caps_of_state s p')); caps_of_state s p = Some cap; valid_objs s; valid_mdb s; cap = UntypedCap dev r bits f\<rbrakk> \<Longrightarrow> descendants_of p (cdt s) = {} proof (prove)
goal (1 subgoal):
 1. \<And>dev r bits f y. \<lbrakk>\<forall>p'\<in>descendants_of p (cdt s). cte_wp_at (\<lambda>c. cap_range c \<inter> untyped_range cap = {}) p' s; \<forall>p p'. p \<in> descendants_of p' (cdt s) \<longrightarrow> cap_class (the (caps_of_state s p)) = cap_class (the (caps_of_state s p')) \<and> cap_range (the (caps_of_state s p)) \<subseteq> cap_range (the (caps_of_state s p')); caps_of_state s p = Some cap; valid_objs s; valid_mdb s; cap = UntypedCap dev r bits f; y \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>dev r bits f y. \<lbrakk>\<forall>p p'. p \<in> descendants_of p' (cdt s) \<longrightarrow> cap_class (the (caps_of_state s p)) = cap_class (the (caps_of_state s p')) \<and> cap_range (the (caps_of_state s p)) \<subseteq> cap_range (the (caps_of_state s p')); caps_of_state s p = Some cap; valid_objs s; valid_mdb s; cap = UntypedCap dev r bits f; y \<in> descendants_of p (cdt s); cte_wp_at (\<lambda>c. cap_range c \<inter> untyped_range cap = {}) y s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>dev r bits f y. \<lbrakk>caps_of_state s p = Some cap; valid_objs s; valid_mdb s; cap = UntypedCap dev r bits f; y \<in> descendants_of p (cdt s); cte_wp_at (\<lambda>c. cap_range c \<inter> untyped_range cap = {}) y s; ?p15 dev r bits f y \<in> descendants_of (?p'17 dev r bits f y) (cdt s) \<longrightarrow> cap_class (the (caps_of_state s (?p15 dev r bits f y))) = cap_class (the (caps_of_state s (?p'17 dev r bits f y))) \<and> cap_range (the (caps_of_state s (?p15 dev r bits f y))) \<subseteq> cap_range (the (caps_of_state s (?p'17 dev r bits f y)))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>dev r bits f y. \<lbrakk>caps_of_state s p = Some cap; valid_objs s; valid_mdb s; cap = UntypedCap dev r bits f; y \<in> descendants_of p (cdt s); cte_wp_at (\<lambda>c. cap_range c \<inter> untyped_range cap = {}) y s; cap_class (the (caps_of_state s y)) = cap_class (the (caps_of_state s p)) \<and> cap_range (the (caps_of_state s y)) \<subseteq> cap_range (the (caps_of_state s p))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>dev r bits f y. \<lbrakk>caps_of_state s p = Some cap; valid_objs s; valid_mdb s; cap = UntypedCap dev r bits f; cte_wp_at (\<lambda>c. cap_range c \<inter> untyped_range cap = {}) y s; cap_class (the (caps_of_state s y)) = cap_class (the (caps_of_state s p)) \<and> cap_range (the (caps_of_state s y)) \<subseteq> cap_range (the (caps_of_state s p)); cte_wp_at (\<lambda>_. True) y s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>dev r bits f a b capa. \<lbrakk>caps_of_state s p = Some (UntypedCap dev r bits f); valid_objs s; valid_mdb s; cap = UntypedCap dev r bits f; cap_class capa = PhysicalClass; cap_range capa \<subseteq> {r..r + 2 ^ bits - 1}; caps_of_state s (a, b) = Some capa; cap_range capa \<inter> {r..r + 2 ^ bits - 1} = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>dev r bits f a b capa. \<lbrakk>caps_of_state s p = Some (UntypedCap dev r bits f); valid_mdb s; cap = UntypedCap dev r bits f; cap_class capa = PhysicalClass; cap_range capa \<subseteq> {r..r + 2 ^ bits - 1}; caps_of_state s (a, b) = Some capa; cap_range capa \<inter> {r..r + 2 ^ bits - 1} = {}\<rbrakk> \<Longrightarrow> caps_of_state s (?p30 dev r bits f a b capa) = Some capa
 2. \<And>dev r bits f a b capa. \<lbrakk>caps_of_state s p = Some (UntypedCap dev r bits f); valid_mdb s; cap = UntypedCap dev r bits f; cap_class capa = PhysicalClass; cap_range capa \<subseteq> {r..r + 2 ^ bits - 1}; caps_of_state s (a, b) = Some capa; cap_range capa \<inter> {r..r + 2 ^ bits - 1} = {}; cap_range capa \<noteq> {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>dev r bits f a b capa. \<lbrakk>caps_of_state s p = Some (UntypedCap dev r bits f); valid_mdb s; cap = UntypedCap dev r bits f; cap_class capa = PhysicalClass; cap_range capa \<subseteq> {r..r + 2 ^ bits - 1}; caps_of_state s (a, b) = Some capa; cap_range capa \<inter> {r..r + 2 ^ bits - 1} = {}; cap_range capa \<noteq> {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!