theory CSpace_I

lemma caps_contained_no_overlap:
  "\<lbrakk> caps_no_overlap' m (capRange cap); caps_contained' m\<rbrakk>
    \<Longrightarrow> caps_contained' (m(p \<mapsto> CTE cap n))" apply (clarsimp simp add: caps_contained'_def) apply (rule conjI) apply clarsimp apply (rule conjI, clarsimp dest!: capRange_untyped) apply clarsimp apply (simp add: caps_no_overlap'_def) apply (erule_tac x=p' in allE, erule allE, erule impE, erule exI) apply (frule capRange_untyped) apply (clarsimp simp add: isCap_simps) apply clarsimp apply (simp add: caps_no_overlap'_def) apply (erule_tac x=pa in allE, erule allE, erule impE, erule exI) apply (frule capRange_untyped) apply (clarsimp simp: isCap_simps) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_no_overlap' m (capRange cap); caps_contained' m\<rbrakk> \<Longrightarrow> caps_contained' (m(p \<mapsto> CTE cap n)) proof (prove)
goal (1 subgoal):
 1. \<And>pa. \<lbrakk>caps_no_overlap' m (capRange cap); \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c)\<rbrakk> \<Longrightarrow> (pa = p \<longrightarrow> (\<forall>p'. (p' = p \<longrightarrow> \<not> isUntypedCap cap \<longrightarrow> capRange cap \<inter> untypedRange cap \<noteq> {} \<longrightarrow> capRange cap \<subseteq> untypedRange cap) \<and> (p' \<noteq> p \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange cap \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange cap)))) \<and> (pa \<noteq> p \<longrightarrow> (\<forall>c. (\<exists>n. m pa = Some (CTE c n)) \<longrightarrow> \<not> isUntypedCap cap \<longrightarrow> capRange cap \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange cap \<subseteq> untypedRange c)) proof (prove)
goal (2 subgoals):
 1. \<And>pa. \<lbrakk>caps_no_overlap' m (capRange cap); \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c)\<rbrakk> \<Longrightarrow> pa = p \<longrightarrow> (\<forall>p'. (p' = p \<longrightarrow> \<not> isUntypedCap cap \<longrightarrow> capRange cap \<inter> untypedRange cap \<noteq> {} \<longrightarrow> capRange cap \<subseteq> untypedRange cap) \<and> (p' \<noteq> p \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange cap \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange cap)))
 2. \<And>pa. \<lbrakk>caps_no_overlap' m (capRange cap); \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c)\<rbrakk> \<Longrightarrow> pa \<noteq> p \<longrightarrow> (\<forall>c. (\<exists>n. m pa = Some (CTE c n)) \<longrightarrow> \<not> isUntypedCap cap \<longrightarrow> capRange cap \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange cap \<subseteq> untypedRange c) proof (prove)
goal (2 subgoals):
 1. \<And>p'. \<lbrakk>caps_no_overlap' m (capRange cap); \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c)\<rbrakk> \<Longrightarrow> (p' = p \<longrightarrow> \<not> isUntypedCap cap \<longrightarrow> capRange cap \<inter> untypedRange cap \<noteq> {} \<longrightarrow> capRange cap \<subseteq> untypedRange cap) \<and> (p' \<noteq> p \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange cap \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange cap))
 2. \<And>pa. \<lbrakk>caps_no_overlap' m (capRange cap); \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c)\<rbrakk> \<Longrightarrow> pa \<noteq> p \<longrightarrow> (\<forall>c. (\<exists>n. m pa = Some (CTE c n)) \<longrightarrow> \<not> isUntypedCap cap \<longrightarrow> capRange cap \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange cap \<subseteq> untypedRange c) proof (prove)
goal (2 subgoals):
 1. \<And>p'. \<lbrakk>caps_no_overlap' m (capRange cap); \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c)\<rbrakk> \<Longrightarrow> p' \<noteq> p \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange cap \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange cap)
 2. \<And>pa. \<lbrakk>caps_no_overlap' m (capRange cap); \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c)\<rbrakk> \<Longrightarrow> pa \<noteq> p \<longrightarrow> (\<forall>c. (\<exists>n. m pa = Some (CTE c n)) \<longrightarrow> \<not> isUntypedCap cap \<longrightarrow> capRange cap \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange cap \<subseteq> untypedRange c) proof (prove)
goal (2 subgoals):
 1. \<And>p' c' n' x. \<lbrakk>caps_no_overlap' m (capRange cap); \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); p' \<noteq> p; m p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange cap \<noteq> {}; x \<in> capRange c'\<rbrakk> \<Longrightarrow> x \<in> untypedRange cap
 2. \<And>pa. \<lbrakk>caps_no_overlap' m (capRange cap); \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c)\<rbrakk> \<Longrightarrow> pa \<noteq> p \<longrightarrow> (\<forall>c. (\<exists>n. m pa = Some (CTE c n)) \<longrightarrow> \<not> isUntypedCap cap \<longrightarrow> capRange cap \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange cap \<subseteq> untypedRange c) proof (prove)
goal (2 subgoals):
 1. \<And>p' c' n' x. \<lbrakk>\<forall>p c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> capRange c \<inter> capRange cap = {}; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); p' \<noteq> p; m p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange cap \<noteq> {}; x \<in> capRange c'\<rbrakk> \<Longrightarrow> x \<in> untypedRange cap
 2. \<And>pa. \<lbrakk>caps_no_overlap' m (capRange cap); \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c)\<rbrakk> \<Longrightarrow> pa \<noteq> p \<longrightarrow> (\<forall>c. (\<exists>n. m pa = Some (CTE c n)) \<longrightarrow> \<not> isUntypedCap cap \<longrightarrow> capRange cap \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange cap \<subseteq> untypedRange c) proof (prove)
goal (2 subgoals):
 1. \<And>p' c' n' x. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); p' \<noteq> p; m p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange cap \<noteq> {}; x \<in> capRange c'; capRange c' \<inter> capRange cap = {}\<rbrakk> \<Longrightarrow> x \<in> untypedRange cap
 2. \<And>pa. \<lbrakk>caps_no_overlap' m (capRange cap); \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c)\<rbrakk> \<Longrightarrow> pa \<noteq> p \<longrightarrow> (\<forall>c. (\<exists>n. m pa = Some (CTE c n)) \<longrightarrow> \<not> isUntypedCap cap \<longrightarrow> capRange cap \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange cap \<subseteq> untypedRange c) proof (prove)
goal (2 subgoals):
 1. \<And>p' c' n' x. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); p' \<noteq> p; m p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange cap \<noteq> {}; x \<in> capRange c'; capRange c' \<inter> capRange cap = {}; isUntypedCap cap\<rbrakk> \<Longrightarrow> x \<in> untypedRange cap
 2. \<And>pa. \<lbrakk>caps_no_overlap' m (capRange cap); \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c)\<rbrakk> \<Longrightarrow> pa \<noteq> p \<longrightarrow> (\<forall>c. (\<exists>n. m pa = Some (CTE c n)) \<longrightarrow> \<not> isUntypedCap cap \<longrightarrow> capRange cap \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange cap \<subseteq> untypedRange c) proof (prove)
goal (1 subgoal):
 1. \<And>pa. \<lbrakk>caps_no_overlap' m (capRange cap); \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c)\<rbrakk> \<Longrightarrow> pa \<noteq> p \<longrightarrow> (\<forall>c. (\<exists>n. m pa = Some (CTE c n)) \<longrightarrow> \<not> isUntypedCap cap \<longrightarrow> capRange cap \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange cap \<subseteq> untypedRange c) proof (prove)
goal (1 subgoal):
 1. \<And>pa c n x. \<lbrakk>caps_no_overlap' m (capRange cap); \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); pa \<noteq> p; m pa = Some (CTE c n); \<not> isUntypedCap cap; capRange cap \<inter> untypedRange c \<noteq> {}; x \<in> capRange cap\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (1 subgoal):
 1. \<And>pa c n x. \<lbrakk>\<forall>p c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> capRange c \<inter> capRange cap = {}; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); pa \<noteq> p; m pa = Some (CTE c n); \<not> isUntypedCap cap; capRange cap \<inter> untypedRange c \<noteq> {}; x \<in> capRange cap\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (1 subgoal):
 1. \<And>pa c n x. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); pa \<noteq> p; m pa = Some (CTE c n); \<not> isUntypedCap cap; capRange cap \<inter> untypedRange c \<noteq> {}; x \<in> capRange cap; capRange c \<inter> capRange cap = {}\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (1 subgoal):
 1. \<And>pa c n x. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); pa \<noteq> p; m pa = Some (CTE c n); \<not> isUntypedCap cap; capRange cap \<inter> untypedRange c \<noteq> {}; x \<in> capRange cap; capRange c \<inter> capRange cap = {}; isUntypedCap c\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (1 subgoal):
 1. \<And>pa n x d v0 v1 f. \<lbrakk>\<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> (\<forall>d v0 v1 f. c' \<noteq> capability.UntypedCap d v0 v1 f) \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); pa \<noteq> p; m pa = Some (CTE (capability.UntypedCap d v0 v1 f) n); \<forall>d v0 v1 f. cap \<noteq> capability.UntypedCap d v0 v1 f; capRange cap \<inter> {v0..v0 + 2 ^ v1 - 1} \<noteq> {}; x \<in> capRange cap; {v0..v0 + 2 ^ v1 - 1} \<inter> capRange cap = {}\<rbrakk> \<Longrightarrow> v0 \<le> x \<and> x \<le> v0 + 2 ^ v1 - 1 proof (prove)
goal:
No subgoals!