theory Untyped_AI

lemma caps_overlap_reserved_def2:
  "caps_overlap_reserved S =
   (\<lambda>s. (\<forall>cap \<in> ran (null_filter (caps_of_state s)).
           is_untyped_cap cap \<longrightarrow> usable_untyped_range cap \<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,b)" in spec) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. caps_overlap_reserved S = (\<lambda>s. \<forall>cap\<in>ran (null_filter (caps_of_state s)). is_untyped_cap cap \<longrightarrow> usable_untyped_range cap \<inter> S = {}) proof (prove)
goal (1 subgoal):
 1. \<And>s. caps_overlap_reserved S s = (\<forall>cap\<in>ran (null_filter (caps_of_state s)). is_untyped_cap cap \<longrightarrow> usable_untyped_range cap \<inter> S = {}) proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>cap\<in>ran (caps_of_state s). is_untyped_cap cap \<longrightarrow> usable_untyped_range cap \<inter> S = {}) = (\<forall>cap\<in>ran (null_filter (caps_of_state s)). is_untyped_cap cap \<longrightarrow> usable_untyped_range cap \<inter> S = {}) proof (prove)
goal (2 subgoals):
 1. \<And>s cap. \<lbrakk>\<forall>cap\<in>ran (caps_of_state s). is_untyped_cap cap \<longrightarrow> usable_untyped_range cap \<inter> S = {}; cap \<in> ran (null_filter (caps_of_state s)); is_untyped_cap cap\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 2. \<And>s cap. \<lbrakk>\<forall>cap\<in>ran (null_filter (caps_of_state s)). is_untyped_cap cap \<longrightarrow> usable_untyped_range cap \<inter> S = {}; cap \<in> ran (caps_of_state s); is_untyped_cap cap\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {} proof (prove)
goal (4 subgoals):
 1. \<And>s cap. \<lbrakk>cap \<in> ran (null_filter (caps_of_state s)); is_untyped_cap cap\<rbrakk> \<Longrightarrow> is_untyped_cap (?cap7 s cap)
 2. \<And>s cap. \<lbrakk>cap \<in> ran (null_filter (caps_of_state s)); is_untyped_cap cap; usable_untyped_range (?cap7 s cap) \<inter> S = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 3. \<And>s cap. \<lbrakk>cap \<in> ran (null_filter (caps_of_state s)); is_untyped_cap cap; ?cap7 s cap \<notin> ran (caps_of_state s)\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 4. \<And>s cap. \<lbrakk>\<forall>cap\<in>ran (null_filter (caps_of_state s)). is_untyped_cap cap \<longrightarrow> usable_untyped_range cap \<inter> S = {}; cap \<in> ran (caps_of_state s); is_untyped_cap cap\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {} proof (prove)
goal (3 subgoals):
 1. \<And>s cap. \<lbrakk>cap \<in> ran (null_filter (caps_of_state s)); is_untyped_cap cap; usable_untyped_range cap \<inter> S = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 2. \<And>s cap. \<lbrakk>cap \<in> ran (null_filter (caps_of_state s)); is_untyped_cap cap; cap \<notin> ran (caps_of_state s)\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 3. \<And>s cap. \<lbrakk>\<forall>cap\<in>ran (null_filter (caps_of_state s)). is_untyped_cap cap \<longrightarrow> usable_untyped_range cap \<inter> S = {}; cap \<in> ran (caps_of_state s); is_untyped_cap cap\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {} proof (prove)
goal (2 subgoals):
 1. \<And>s cap. \<lbrakk>cap \<in> ran (null_filter (caps_of_state s)); is_untyped_cap cap; cap \<notin> ran (caps_of_state s)\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 2. \<And>s cap. \<lbrakk>\<forall>cap\<in>ran (null_filter (caps_of_state s)). is_untyped_cap cap \<longrightarrow> usable_untyped_range cap \<inter> S = {}; cap \<in> ran (caps_of_state s); is_untyped_cap cap\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {} proof (prove)
goal (1 subgoal):
 1. \<And>s cap. \<lbrakk>\<forall>cap\<in>ran (null_filter (caps_of_state s)). is_untyped_cap cap \<longrightarrow> usable_untyped_range cap \<inter> S = {}; cap \<in> ran (caps_of_state s); is_untyped_cap cap\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {} proof (prove)
goal (3 subgoals):
 1. \<And>s cap. \<lbrakk>cap \<in> ran (caps_of_state s); is_untyped_cap cap\<rbrakk> \<Longrightarrow> is_untyped_cap (?cap23 s cap)
 2. \<And>s cap. \<lbrakk>cap \<in> ran (caps_of_state s); is_untyped_cap cap; usable_untyped_range (?cap23 s cap) \<inter> S = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 3. \<And>s cap. \<lbrakk>cap \<in> ran (caps_of_state s); is_untyped_cap cap; ?cap23 s cap \<notin> ran (null_filter (caps_of_state s))\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {} proof (prove)
goal (2 subgoals):
 1. \<And>s cap. \<lbrakk>cap \<in> ran (caps_of_state s); is_untyped_cap cap; usable_untyped_range cap \<inter> S = {}\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {}
 2. \<And>s cap. \<lbrakk>cap \<in> ran (caps_of_state s); is_untyped_cap cap; cap \<notin> ran (null_filter (caps_of_state s))\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {} proof (prove)
goal (1 subgoal):
 1. \<And>s cap. \<lbrakk>cap \<in> ran (caps_of_state s); is_untyped_cap cap; cap \<notin> ran (null_filter (caps_of_state s))\<rbrakk> \<Longrightarrow> usable_untyped_range cap \<inter> S = {} proof (prove)
goal (1 subgoal):
 1. \<And>s a b dev r bits f. \<lbrakk>\<forall>a. caps_of_state s a = Some NullCap \<or> caps_of_state s a \<noteq> Some (UntypedCap dev r bits f); caps_of_state s (a, b) = Some (UntypedCap dev r bits f); f < 2 ^ bits\<rbrakk> \<Longrightarrow> {r + word_of_nat f..r + 2 ^ bits - 1} \<inter> S = {} proof (prove)
goal (1 subgoal):
 1. \<And>s a b dev r bits f. \<lbrakk>caps_of_state s (a, b) = Some (UntypedCap dev r bits f); f < 2 ^ bits; caps_of_state s (a, b) = Some NullCap \<or> caps_of_state s (a, b) \<noteq> Some (UntypedCap dev r bits f)\<rbrakk> \<Longrightarrow> {r + word_of_nat f..r + 2 ^ bits - 1} \<inter> S = {} proof (prove)
goal:
No subgoals!