theory Untyped_R

lemma caps_no_overlap''_def2:
  "caps_no_overlap'' ptr sz =
   (\<lambda>s. \<forall>cte\<in>ran (null_filter' (ctes_of s)).
            untypedRange (cteCap cte) \<inter>
            {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow>
            {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq>
            untypedRange (cteCap cte))" apply (intro ext iffI) apply (clarsimp simp:caps_no_overlap''_def null_filter'_def ran_def) apply (drule_tac x = cte in spec) apply fastforce apply (clarsimp simp:caps_no_overlap''_def null_filter'_def) apply (case_tac "cte = CTE capability.NullCap nullMDBNode") apply clarsimp apply (drule_tac x = cte in  bspec) apply (clarsimp simp:ran_def) apply (rule_tac x= a in exI) apply clarsimp apply clarsimp apply (erule subsetD) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. caps_no_overlap'' ptr sz = (\<lambda>s. \<forall>cte\<in>ran (null_filter' (ctes_of s)). untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte)) proof (prove)
goal (2 subgoals):
 1. \<And>s. caps_no_overlap'' ptr sz s \<Longrightarrow> \<forall>cte\<in>ran (null_filter' (ctes_of s)). untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte)
 2. \<And>s. \<forall>cte\<in>ran (null_filter' (ctes_of s)). untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte) \<Longrightarrow> caps_no_overlap'' ptr sz s proof (prove)
goal (2 subgoals):
 1. \<And>s cte a x. \<lbrakk>\<forall>cte. (\<exists>a. ctes_of s a = Some cte) \<longrightarrow> untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte); cte \<noteq> CTE capability.NullCap nullMDBNode; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s a = Some cte; ptr \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> x \<in> untypedRange (cteCap cte)
 2. \<And>s. \<forall>cte\<in>ran (null_filter' (ctes_of s)). untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte) \<Longrightarrow> caps_no_overlap'' ptr sz s proof (prove)
goal (2 subgoals):
 1. \<And>s cte a x. \<lbrakk>cte \<noteq> CTE capability.NullCap nullMDBNode; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ctes_of s a = Some cte; ptr \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; (\<exists>a. ctes_of s a = Some cte) \<longrightarrow> untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte)\<rbrakk> \<Longrightarrow> x \<in> untypedRange (cteCap cte)
 2. \<And>s. \<forall>cte\<in>ran (null_filter' (ctes_of s)). untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte) \<Longrightarrow> caps_no_overlap'' ptr sz s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>cte\<in>ran (null_filter' (ctes_of s)). untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte) \<Longrightarrow> caps_no_overlap'' ptr sz s proof (prove)
goal (1 subgoal):
 1. \<And>s cte x. \<lbrakk>\<forall>cte\<in>ran (\<lambda>x. if ctes_of s x = Some (CTE capability.NullCap nullMDBNode) then None else ctes_of s x). untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte); cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> x \<in> untypedRange (cteCap cte) proof (prove)
goal (2 subgoals):
 1. \<And>s cte x. \<lbrakk>\<forall>cte\<in>ran (\<lambda>x. if ctes_of s x = Some (CTE capability.NullCap nullMDBNode) then None else ctes_of s x). untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte); cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; cte = CTE capability.NullCap nullMDBNode\<rbrakk> \<Longrightarrow> x \<in> untypedRange (cteCap cte)
 2. \<And>s cte x. \<lbrakk>\<forall>cte\<in>ran (\<lambda>x. if ctes_of s x = Some (CTE capability.NullCap nullMDBNode) then None else ctes_of s x). untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte); cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; cte \<noteq> CTE capability.NullCap nullMDBNode\<rbrakk> \<Longrightarrow> x \<in> untypedRange (cteCap cte) proof (prove)
goal (1 subgoal):
 1. \<And>s cte x. \<lbrakk>\<forall>cte\<in>ran (\<lambda>x. if ctes_of s x = Some (CTE capability.NullCap nullMDBNode) then None else ctes_of s x). untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte); cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; cte \<noteq> CTE capability.NullCap nullMDBNode\<rbrakk> \<Longrightarrow> x \<in> untypedRange (cteCap cte) proof (prove)
goal (2 subgoals):
 1. \<And>s cte x. \<lbrakk>cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; cte \<noteq> CTE capability.NullCap nullMDBNode\<rbrakk> \<Longrightarrow> cte \<in> ran (\<lambda>x. if ctes_of s x = Some (CTE capability.NullCap nullMDBNode) then None else ctes_of s x)
 2. \<And>s cte x. \<lbrakk>cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; cte \<noteq> CTE capability.NullCap nullMDBNode; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte)\<rbrakk> \<Longrightarrow> x \<in> untypedRange (cteCap cte) proof (prove)
goal (2 subgoals):
 1. \<And>s cte x a. \<lbrakk>untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; cte \<noteq> CTE capability.NullCap nullMDBNode; ctes_of s a = Some cte\<rbrakk> \<Longrightarrow> \<exists>a. ctes_of s a \<noteq> Some (CTE capability.NullCap nullMDBNode) \<and> (ctes_of s a \<noteq> Some (CTE capability.NullCap nullMDBNode) \<longrightarrow> ctes_of s a = Some cte)
 2. \<And>s cte x. \<lbrakk>cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; cte \<noteq> CTE capability.NullCap nullMDBNode; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte)\<rbrakk> \<Longrightarrow> x \<in> untypedRange (cteCap cte) proof (prove)
goal (2 subgoals):
 1. \<And>s cte x a. \<lbrakk>untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; cte \<noteq> CTE capability.NullCap nullMDBNode; ctes_of s a = Some cte\<rbrakk> \<Longrightarrow> ctes_of s a \<noteq> Some (CTE capability.NullCap nullMDBNode) \<and> (ctes_of s a \<noteq> Some (CTE capability.NullCap nullMDBNode) \<longrightarrow> ctes_of s a = Some cte)
 2. \<And>s cte x. \<lbrakk>cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; cte \<noteq> CTE capability.NullCap nullMDBNode; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte)\<rbrakk> \<Longrightarrow> x \<in> untypedRange (cteCap cte) proof (prove)
goal (1 subgoal):
 1. \<And>s cte x. \<lbrakk>cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; cte \<noteq> CTE capability.NullCap nullMDBNode; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte)\<rbrakk> \<Longrightarrow> x \<in> untypedRange (cteCap cte) proof (prove)
goal (1 subgoal):
 1. \<And>s cte x. \<lbrakk>cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; cte \<noteq> CTE capability.NullCap nullMDBNode; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte)\<rbrakk> \<Longrightarrow> x \<in> untypedRange (cteCap cte) proof (prove)
goal (1 subgoal):
 1. \<And>s cte x. \<lbrakk>cte \<in> ran (ctes_of s); untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ptr \<le> x; x \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; cte \<noteq> CTE capability.NullCap nullMDBNode\<rbrakk> \<Longrightarrow> x \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal:
No subgoals!