theory Untyped_R

lemma caps_overlap_reserved'_def2:
  "caps_overlap_reserved' S =
   (\<lambda>s. (\<forall>cte \<in> ran (null_filter' (ctes_of s)).
        isUntypedCap (cteCap cte) \<longrightarrow>
        usableUntypedRange (cteCap cte) \<inter> S = {}))" apply (rule ext) apply (clarsimp simp:caps_overlap_reserved'_def) apply (intro iffI ballI impI) apply (elim ballE impE) apply simp apply simp apply (simp add:ran_def null_filter'_def split:if_split_asm option.splits) apply (elim ballE impE) apply simp apply simp apply (clarsimp simp: ran_def null_filter'_def is_cap_simps
                  simp del: split_paired_All split_paired_Ex split: if_splits) apply (drule_tac x = a in spec) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. caps_overlap_reserved' S = (\<lambda>s. \<forall>cte\<in>ran (null_filter' (ctes_of s)). isUntypedCap (cteCap cte) \<longrightarrow> usableUntypedRange (cteCap cte) \<inter> S = {}) proof (prove)
goal (1 subgoal):
 1. \<And>s. caps_overlap_reserved' S s = (\<forall>cte\<in>ran (null_filter' (ctes_of s)). isUntypedCap (cteCap cte) \<longrightarrow> usableUntypedRange (cteCap cte) \<inter> S = {}) proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>cte\<in>ran (ctes_of s). isUntypedCap (cteCap cte) \<longrightarrow> usableUntypedRange (cteCap cte) \<inter> S = {}) = (\<forall>cte\<in>ran (null_filter' (ctes_of s)). isUntypedCap (cteCap cte) \<longrightarrow> usableUntypedRange (cteCap cte) \<inter> S = {}) proof (prove)
goal (2 subgoals):
 1. \<And>s cte. \<lbrakk>\<forall>cte\<in>ran (ctes_of s). isUntypedCap (cteCap cte) \<longrightarrow> usableUntypedRange (cteCap cte) \<inter> S = {}; cte \<in> ran (null_filter' (ctes_of s)); isUntypedCap (cteCap cte)\<rbrakk> \<Longrightarrow> usableUntypedRange (cteCap cte) \<inter> S = {}
 2. \<And>s cte. \<lbrakk>\<forall>cte\<in>ran (null_filter' (ctes_of s)). isUntypedCap (cteCap cte) \<longrightarrow> usableUntypedRange (cteCap cte) \<inter> S = {}; cte \<in> ran (ctes_of s); isUntypedCap (cteCap cte)\<rbrakk> \<Longrightarrow> usableUntypedRange (cteCap cte) \<inter> S = {} proof (prove)
goal (4 subgoals):
 1. \<And>s cte. \<lbrakk>cte \<in> ran (null_filter' (ctes_of s)); isUntypedCap (cteCap cte)\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap (?cte7 s cte))
 2. \<And>s cte. \<lbrakk>cte \<in> ran (null_filter' (ctes_of s)); isUntypedCap (cteCap cte); usableUntypedRange (cteCap (?cte7 s cte)) \<inter> S = {}\<rbrakk> \<Longrightarrow> usableUntypedRange (cteCap cte) \<inter> S = {}
 3. \<And>s cte. \<lbrakk>cte \<in> ran (null_filter' (ctes_of s)); isUntypedCap (cteCap cte); ?cte7 s cte \<notin> ran (ctes_of s)\<rbrakk> \<Longrightarrow> usableUntypedRange (cteCap cte) \<inter> S = {}
 4. \<And>s cte. \<lbrakk>\<forall>cte\<in>ran (null_filter' (ctes_of s)). isUntypedCap (cteCap cte) \<longrightarrow> usableUntypedRange (cteCap cte) \<inter> S = {}; cte \<in> ran (ctes_of s); isUntypedCap (cteCap cte)\<rbrakk> \<Longrightarrow> usableUntypedRange (cteCap cte) \<inter> S = {} proof (prove)
goal (3 subgoals):
 1. \<And>s cte. \<lbrakk>cte \<in> ran (null_filter' (ctes_of s)); isUntypedCap (cteCap cte); usableUntypedRange (cteCap cte) \<inter> S = {}\<rbrakk> \<Longrightarrow> usableUntypedRange (cteCap cte) \<inter> S = {}
 2. \<And>s cte. \<lbrakk>cte \<in> ran (null_filter' (ctes_of s)); isUntypedCap (cteCap cte); cte \<notin> ran (ctes_of s)\<rbrakk> \<Longrightarrow> usableUntypedRange (cteCap cte) \<inter> S = {}
 3. \<And>s cte. \<lbrakk>\<forall>cte\<in>ran (null_filter' (ctes_of s)). isUntypedCap (cteCap cte) \<longrightarrow> usableUntypedRange (cteCap cte) \<inter> S = {}; cte \<in> ran (ctes_of s); isUntypedCap (cteCap cte)\<rbrakk> \<Longrightarrow> usableUntypedRange (cteCap cte) \<inter> S = {} proof (prove)
goal (2 subgoals):
 1. \<And>s cte. \<lbrakk>cte \<in> ran (null_filter' (ctes_of s)); isUntypedCap (cteCap cte); cte \<notin> ran (ctes_of s)\<rbrakk> \<Longrightarrow> usableUntypedRange (cteCap cte) \<inter> S = {}
 2. \<And>s cte. \<lbrakk>\<forall>cte\<in>ran (null_filter' (ctes_of s)). isUntypedCap (cteCap cte) \<longrightarrow> usableUntypedRange (cteCap cte) \<inter> S = {}; cte \<in> ran (ctes_of s); isUntypedCap (cteCap cte)\<rbrakk> \<Longrightarrow> usableUntypedRange (cteCap cte) \<inter> S = {} proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>\<forall>cte\<in>ran (null_filter' (ctes_of s)). isUntypedCap (cteCap cte) \<longrightarrow> usableUntypedRange (cteCap cte) \<inter> S = {}; cte \<in> ran (ctes_of s); isUntypedCap (cteCap cte)\<rbrakk> \<Longrightarrow> usableUntypedRange (cteCap cte) \<inter> S = {} proof (prove)
goal (3 subgoals):
 1. \<And>s cte. \<lbrakk>cte \<in> ran (ctes_of s); isUntypedCap (cteCap cte)\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap (?cte19 s cte))
 2. \<And>s cte. \<lbrakk>cte \<in> ran (ctes_of s); isUntypedCap (cteCap cte); usableUntypedRange (cteCap (?cte19 s cte)) \<inter> S = {}\<rbrakk> \<Longrightarrow> usableUntypedRange (cteCap cte) \<inter> S = {}
 3. \<And>s cte. \<lbrakk>cte \<in> ran (ctes_of s); isUntypedCap (cteCap cte); ?cte19 s cte \<notin> ran (null_filter' (ctes_of s))\<rbrakk> \<Longrightarrow> usableUntypedRange (cteCap cte) \<inter> S = {} proof (prove)
goal (2 subgoals):
 1. \<And>s cte. \<lbrakk>cte \<in> ran (ctes_of s); isUntypedCap (cteCap cte); usableUntypedRange (cteCap cte) \<inter> S = {}\<rbrakk> \<Longrightarrow> usableUntypedRange (cteCap cte) \<inter> S = {}
 2. \<And>s cte. \<lbrakk>cte \<in> ran (ctes_of s); isUntypedCap (cteCap cte); cte \<notin> ran (null_filter' (ctes_of s))\<rbrakk> \<Longrightarrow> usableUntypedRange (cteCap cte) \<inter> S = {} proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>cte \<in> ran (ctes_of s); isUntypedCap (cteCap cte); cte \<notin> ran (null_filter' (ctes_of s))\<rbrakk> \<Longrightarrow> usableUntypedRange (cteCap cte) \<inter> S = {} proof (prove)
goal (1 subgoal):
 1. \<And>s cte a. \<lbrakk>\<forall>a. ctes_of s a = Some (CTE capability.NullCap nullMDBNode) \<or> ctes_of s a \<noteq> Some cte; isUntypedCap (cteCap cte); ctes_of s a = Some cte\<rbrakk> \<Longrightarrow> usableUntypedRange (cteCap cte) \<inter> S = {} proof (prove)
goal (1 subgoal):
 1. \<And>s cte a. \<lbrakk>isUntypedCap (cteCap cte); ctes_of s a = Some cte; ctes_of s a = Some (CTE capability.NullCap nullMDBNode) \<or> ctes_of s a \<noteq> Some cte\<rbrakk> \<Longrightarrow> usableUntypedRange (cteCap cte) \<inter> S = {} proof (prove)
goal:
No subgoals!