theory Detype_AI

lemma valid_mdb_descendants_range_in:
  "valid_mdb s \<Longrightarrow> descendants_range_in S p s = (\<forall>p'\<in>descendants_of p (cdt s).
  \<exists>c. (null_filter (caps_of_state s)) p' = Some c \<and> cap_range c \<inter> S = {})" apply (clarsimp simp:descendants_range_in_def
                  split:if_splits) apply (intro ext iffI ballI impI) apply (frule(1) bspec) apply (frule(1) descendants_of_cte_at) apply (clarsimp simp:cte_wp_at_caps_of_state null_filter_def descendants_of_def) apply (clarsimp simp:valid_mdb_no_null) apply (drule(1) bspec) apply (clarsimp simp:cte_wp_at_caps_of_state null_filter_def cap_range_def split:if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_mdb s \<Longrightarrow> descendants_range_in S p s = (\<forall>p'\<in>descendants_of p (cdt s). \<exists>c. null_filter (caps_of_state s) p' = Some c \<and> cap_range c \<inter> S = {}) proof (prove)
goal (1 subgoal):
 1. valid_mdb s \<Longrightarrow> (\<forall>p'\<in>descendants_of p (cdt s). cte_wp_at (\<lambda>c. cap_range c \<inter> S = {}) p' s) = (\<forall>p'\<in>descendants_of p (cdt s). \<exists>c. null_filter (caps_of_state s) p' = Some c \<and> cap_range c \<inter> S = {}) proof (prove)
goal (2 subgoals):
 1. \<And>p'. \<lbrakk>valid_mdb s; \<forall>p'\<in>descendants_of p (cdt s). cte_wp_at (\<lambda>c. cap_range c \<inter> S = {}) p' s; p' \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> \<exists>c. null_filter (caps_of_state s) p' = Some c \<and> cap_range c \<inter> S = {}
 2. \<And>p'. \<lbrakk>valid_mdb s; \<forall>p'\<in>descendants_of p (cdt s). \<exists>c. null_filter (caps_of_state s) p' = Some c \<and> cap_range c \<inter> S = {}; p' \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. cap_range c \<inter> S = {}) p' s proof (prove)
goal (2 subgoals):
 1. \<And>p'. \<lbrakk>valid_mdb s; \<forall>p'\<in>descendants_of p (cdt s). cte_wp_at (\<lambda>c. cap_range c \<inter> S = {}) p' s; p' \<in> descendants_of p (cdt s); cte_wp_at (\<lambda>c. cap_range c \<inter> S = {}) p' s\<rbrakk> \<Longrightarrow> \<exists>c. null_filter (caps_of_state s) p' = Some c \<and> cap_range c \<inter> S = {}
 2. \<And>p'. \<lbrakk>valid_mdb s; \<forall>p'\<in>descendants_of p (cdt s). \<exists>c. null_filter (caps_of_state s) p' = Some c \<and> cap_range c \<inter> S = {}; p' \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. cap_range c \<inter> S = {}) p' s proof (prove)
goal (2 subgoals):
 1. \<And>p'. \<lbrakk>valid_mdb s; \<forall>p'\<in>descendants_of p (cdt s). cte_wp_at (\<lambda>c. cap_range c \<inter> S = {}) p' s; p' \<in> descendants_of p (cdt s); cte_wp_at (\<lambda>c. cap_range c \<inter> S = {}) p' s; cte_wp_at (\<lambda>_. True) p' s\<rbrakk> \<Longrightarrow> \<exists>c. null_filter (caps_of_state s) p' = Some c \<and> cap_range c \<inter> S = {}
 2. \<And>p'. \<lbrakk>valid_mdb s; \<forall>p'\<in>descendants_of p (cdt s). \<exists>c. null_filter (caps_of_state s) p' = Some c \<and> cap_range c \<inter> S = {}; p' \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. cap_range c \<inter> S = {}) p' s proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>valid_mdb s; \<forall>a b. cdt s \<Turnstile> p \<rightarrow> (a, b) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> cap_range cap \<inter> S = {}); cdt s \<Turnstile> p \<rightarrow> (a, b); cap_range NullCap \<inter> S = {}; caps_of_state s (a, b) = Some NullCap\<rbrakk> \<Longrightarrow> False
 2. \<And>p'. \<lbrakk>valid_mdb s; \<forall>p'\<in>descendants_of p (cdt s). \<exists>c. null_filter (caps_of_state s) p' = Some c \<and> cap_range c \<inter> S = {}; p' \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. cap_range c \<inter> S = {}) p' s proof (prove)
goal (1 subgoal):
 1. \<And>p'. \<lbrakk>valid_mdb s; \<forall>p'\<in>descendants_of p (cdt s). \<exists>c. null_filter (caps_of_state s) p' = Some c \<and> cap_range c \<inter> S = {}; p' \<in> descendants_of p (cdt s)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. cap_range c \<inter> S = {}) p' s proof (prove)
goal (1 subgoal):
 1. \<And>p'. \<lbrakk>valid_mdb s; p' \<in> descendants_of p (cdt s); \<exists>c. null_filter (caps_of_state s) p' = Some c \<and> cap_range c \<inter> S = {}\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. cap_range c \<inter> S = {}) p' s proof (prove)
goal:
No subgoals!