theory CNodeInv_R

lemma caps_contained_subrange:
  "\<lbrakk> caps_contained' m; m sl = Some (CTE cap n'); capRange cap' \<subseteq> capRange cap; \<not>isUntypedCap cap; \<not> isUntypedCap cap' \<rbrakk>
  \<Longrightarrow> caps_contained' (modify_map m sl (cteCap_update (%_. cap')))" apply (simp add: caps_contained'_def modify_map_apply notUntypedRange) apply clarsimp apply (erule_tac x=p in allE) apply (erule_tac x=sl in allE) apply simp apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_contained' m; m sl = Some (CTE cap n'); capRange cap' \<subseteq> capRange cap; \<not> isUntypedCap cap; \<not> isUntypedCap cap'\<rbrakk> \<Longrightarrow> caps_contained' (modify_map m sl (cteCap_update (\<lambda>_. cap'))) proof (prove)
goal (1 subgoal):
 1. \<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); m sl = Some (CTE cap n'); capRange cap' \<subseteq> capRange cap; \<not> isUntypedCap cap; \<not> isUntypedCap cap'\<rbrakk> \<Longrightarrow> \<forall>p. p \<noteq> sl \<longrightarrow> (\<forall>c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> capRange cap' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange cap' \<subseteq> untypedRange c) proof (prove)
goal (1 subgoal):
 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); m sl = Some (CTE cap n'); capRange cap' \<subseteq> capRange cap; \<not> isUntypedCap cap; \<not> isUntypedCap cap'; p \<noteq> sl; m p = Some (CTE c n); capRange cap' \<inter> untypedRange c \<noteq> {}; x \<in> capRange cap'\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (1 subgoal):
 1. \<And>p c n x. \<lbrakk>m sl = Some (CTE cap n'); capRange cap' \<subseteq> capRange cap; \<not> isUntypedCap cap; \<not> isUntypedCap cap'; p \<noteq> sl; m p = Some (CTE c n); capRange cap' \<inter> untypedRange c \<noteq> {}; x \<in> capRange cap'; \<forall>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> x \<in> untypedRange c proof (prove)
goal (1 subgoal):
 1. \<And>p c n x. \<lbrakk>m sl = Some (CTE cap n'); capRange cap' \<subseteq> capRange cap; \<not> isUntypedCap cap; \<not> isUntypedCap cap'; p \<noteq> sl; m p = Some (CTE c n); capRange cap' \<inter> untypedRange c \<noteq> {}; x \<in> capRange cap'; \<forall>c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m sl = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (1 subgoal):
 1. \<And>p c n x. \<lbrakk>m sl = Some (CTE cap n'); capRange cap' \<subseteq> capRange cap; \<not> isUntypedCap cap; \<not> isUntypedCap cap'; p \<noteq> sl; m p = Some (CTE c n); capRange cap' \<inter> untypedRange c \<noteq> {}; x \<in> capRange cap'; capRange cap \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange cap \<subseteq> untypedRange c\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal:
No subgoals!