theory Detype_R

lemma descendants_range_in'_def2:
  "descendants_range_in' S p = (\<lambda>m. \<forall>p'\<in>descendants_of' p (null_filter' m).
  \<forall>c n. (null_filter' m) p' = Some (CTE c n) \<longrightarrow> capRange c \<inter> S = {})" apply (clarsimp simp:descendants_range_in'_def
                  split:if_splits) apply (rule ext) apply (rule subst[OF null_filter_descendants_of']) apply simp apply (rule iffI) apply (clarsimp simp:null_filter'_def)+ apply (drule(1) bspec) apply (elim allE impE ballE) apply (rule ccontr) apply (clarsimp split:if_splits simp:descendants_of'_def) apply (erule(1) subtree_not_Null) apply fastforce apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. descendants_range_in' S p = (\<lambda>m. \<forall>p'\<in>descendants_of' p (null_filter' m). \<forall>c n. null_filter' m p' = Some (CTE c n) \<longrightarrow> capRange c \<inter> S = {}) proof (prove)
goal (1 subgoal):
 1. (\<lambda>m. \<forall>p'\<in>descendants_of' p m. \<forall>c. (\<exists>n. m p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}) = (\<lambda>m. \<forall>p'\<in>descendants_of' p (null_filter' m). \<forall>c. (\<exists>n. null_filter' m p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}) proof (prove)
goal (1 subgoal):
 1. \<And>m. (\<forall>p'\<in>descendants_of' p m. \<forall>c. (\<exists>n. m p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}) = (\<forall>p'\<in>descendants_of' p (null_filter' m). \<forall>c. (\<exists>n. null_filter' m p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}) proof (prove)
goal (2 subgoals):
 1. \<And>m. null_filter' (?xs11 m) = null_filter' (null_filter' m)
 2. \<And>m. (\<forall>p'\<in>descendants_of' p m. \<forall>c. (\<exists>n. m p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}) = (\<forall>p'\<in>descendants_of' p (?xs11 m). \<forall>c. (\<exists>n. null_filter' m p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}) proof (prove)
goal (1 subgoal):
 1. \<And>m. (\<forall>p'\<in>descendants_of' p m. \<forall>c. (\<exists>n. m p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}) = (\<forall>p'\<in>descendants_of' p m. \<forall>c. (\<exists>n. null_filter' m p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}) proof (prove)
goal (2 subgoals):
 1. \<And>m. \<forall>p'\<in>descendants_of' p m. \<forall>c. (\<exists>n. m p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {} \<Longrightarrow> \<forall>p'\<in>descendants_of' p m. \<forall>c. (\<exists>n. null_filter' m p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}
 2. \<And>m. \<forall>p'\<in>descendants_of' p m. \<forall>c. (\<exists>n. null_filter' m p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {} \<Longrightarrow> \<forall>p'\<in>descendants_of' p m. \<forall>c. (\<exists>n. m p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {} proof (prove)
goal (1 subgoal):
 1. \<And>m p' c n. \<lbrakk>\<forall>p'\<in>descendants_of' p m. \<forall>c. (\<exists>n. (if m p' = Some (CTE capability.NullCap nullMDBNode) then None else m p') = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}; p' \<in> descendants_of' p m; m p' = Some (CTE c n)\<rbrakk> \<Longrightarrow> capRange c \<inter> S = {} proof (prove)
goal (1 subgoal):
 1. \<And>m p' c n. \<lbrakk>p' \<in> descendants_of' p m; m p' = Some (CTE c n); \<forall>c. (\<exists>n. (if m p' = Some (CTE capability.NullCap nullMDBNode) then None else m p') = Some (CTE c n)) \<longrightarrow> capRange c \<inter> S = {}\<rbrakk> \<Longrightarrow> capRange c \<inter> S = {} proof (prove)
goal (2 subgoals):
 1. \<And>m p' c n. \<lbrakk>p' \<in> descendants_of' p m; m p' = Some (CTE c n)\<rbrakk> \<Longrightarrow> \<exists>na. (if m p' = Some (CTE capability.NullCap nullMDBNode) then None else m p') = Some (CTE (?c35 m p' c n) na)
 2. \<And>m p' c n. \<lbrakk>p' \<in> descendants_of' p m; m p' = Some (CTE c n); capRange (?c35 m p' c n) \<inter> S = {}\<rbrakk> \<Longrightarrow> capRange c \<inter> S = {} proof (prove)
goal (2 subgoals):
 1. \<And>m p' c n. \<lbrakk>p' \<in> descendants_of' p m; m p' = Some (CTE c n); \<nexists>na. (if m p' = Some (CTE capability.NullCap nullMDBNode) then None else m p') = Some (CTE (?c35 m p' c n) na)\<rbrakk> \<Longrightarrow> False
 2. \<And>m p' c n. \<lbrakk>p' \<in> descendants_of' p m; m p' = Some (CTE c n); capRange (?c35 m p' c n) \<inter> S = {}\<rbrakk> \<Longrightarrow> capRange c \<inter> S = {} proof (prove)
goal (3 subgoals):
 1. \<And>m p'. \<lbrakk>m \<turnstile> p \<rightarrow> p'; m p' = Some (CTE capability.NullCap nullMDBNode)\<rbrakk> \<Longrightarrow> False
 2. \<And>m p' c n. \<lbrakk>m \<turnstile> p \<rightarrow> p'; m p' = Some (CTE c n); c = capability.NullCap \<longrightarrow> n \<noteq> nullMDBNode; c \<noteq> ?c35 m p' c n\<rbrakk> \<Longrightarrow> False
 3. \<And>m p' c n. \<lbrakk>p' \<in> descendants_of' p m; m p' = Some (CTE c n); capRange (?c35 m p' c n) \<inter> S = {}\<rbrakk> \<Longrightarrow> capRange c \<inter> S = {} proof (prove)
goal (2 subgoals):
 1. \<And>m p' c n. \<lbrakk>m \<turnstile> p \<rightarrow> p'; m p' = Some (CTE c n); c = capability.NullCap \<longrightarrow> n \<noteq> nullMDBNode; c \<noteq> ?c35 m p' c n\<rbrakk> \<Longrightarrow> False
 2. \<And>m p' c n. \<lbrakk>p' \<in> descendants_of' p m; m p' = Some (CTE c n); capRange (?c35 m p' c n) \<inter> S = {}\<rbrakk> \<Longrightarrow> capRange c \<inter> S = {} proof (prove)
goal (1 subgoal):
 1. \<And>m p' c n. \<lbrakk>p' \<in> descendants_of' p m; m p' = Some (CTE c n); capRange c \<inter> S = {}\<rbrakk> \<Longrightarrow> capRange c \<inter> S = {} proof (prove)
goal:
No subgoals!