theory CSpace_R

lemma parent_untyped_must_not_usable:
  "\<lbrakk>ptr \<noteq> src; m ptr = Some (CTE ccap node');
    untypedRange ccap = untypedRange src_cap; capAligned src_cap;
    isUntypedCap src_cap \<rbrakk>
   \<Longrightarrow> usableUntypedRange ccap = {}" using untyped_inc src apply (clarsimp simp:untyped_inc'_def) apply (erule_tac x = ptr in allE) apply (erule_tac x = src in allE) apply clarsimp apply (subgoal_tac "isUntypedCap ccap") apply clarsimp apply (drule_tac p = ptr in untyped_no_parent) apply (simp add:descendants_of'_def) apply (drule (1) aligned_untypedRange_non_empty) apply (case_tac ccap,simp_all add:isCap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr \<noteq> src; m ptr = Some (CTE ccap node'); untypedRange ccap = untypedRange src_cap; capAligned src_cap; isUntypedCap src_cap\<rbrakk> \<Longrightarrow> usableUntypedRange ccap = {} proof (prove)
using this:
untyped_inc' m
m src = Some (CTE src_cap src_node)

goal (1 subgoal):
 1. \<lbrakk>ptr \<noteq> src; m ptr = Some (CTE ccap node'); untypedRange ccap = untypedRange src_cap; capAligned src_cap; isUntypedCap src_cap\<rbrakk> \<Longrightarrow> usableUntypedRange ccap = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr \<noteq> src; m ptr = Some (CTE ccap node'); untypedRange ccap = untypedRange src_cap; capAligned src_cap; isUntypedCap src_cap; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> isUntypedCap c' \<longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> p \<in> descendants_of' p' m \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' p m \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' p m \<and> usableUntypedRange c = {} \<or> p \<in> descendants_of' p' m \<and> usableUntypedRange c' = {} \<or> p = p')); m src = Some (CTE src_cap src_node)\<rbrakk> \<Longrightarrow> usableUntypedRange ccap = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr \<noteq> src; m ptr = Some (CTE ccap node'); untypedRange ccap = untypedRange src_cap; capAligned src_cap; isUntypedCap src_cap; m src = Some (CTE src_cap src_node); \<forall>p' c. (\<exists>n. m ptr = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> isUntypedCap c' \<longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> ptr \<in> descendants_of' p' m \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> p' \<in> descendants_of' ptr m \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> p' \<in> descendants_of' ptr m \<and> usableUntypedRange c = {} \<or> ptr \<in> descendants_of' p' m \<and> usableUntypedRange c' = {} \<or> ptr = p'))\<rbrakk> \<Longrightarrow> usableUntypedRange ccap = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr \<noteq> src; m ptr = Some (CTE ccap node'); untypedRange ccap = untypedRange src_cap; capAligned src_cap; isUntypedCap src_cap; m src = Some (CTE src_cap src_node); \<forall>c. (\<exists>n. m ptr = Some (CTE c n)) \<longrightarrow> isUntypedCap c \<longrightarrow> (\<forall>c'. (\<exists>n'. m src = Some (CTE c' n')) \<longrightarrow> isUntypedCap c' \<longrightarrow> (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> (untypedRange c \<subset> untypedRange c' \<longrightarrow> ptr \<in> descendants_of' src m \<and> untypedRange c \<inter> usableUntypedRange c' = {}) \<and> (untypedRange c' \<subset> untypedRange c \<longrightarrow> src \<in> descendants_of' ptr m \<and> untypedRange c' \<inter> usableUntypedRange c = {}) \<and> (untypedRange c = untypedRange c' \<longrightarrow> src \<in> descendants_of' ptr m \<and> usableUntypedRange c = {} \<or> ptr \<in> descendants_of' src m \<and> usableUntypedRange c' = {} \<or> ptr = src))\<rbrakk> \<Longrightarrow> usableUntypedRange ccap = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr \<noteq> src; m ptr = Some (CTE ccap node'); untypedRange ccap = untypedRange src_cap; capAligned src_cap; isUntypedCap src_cap; m src = Some (CTE src_cap src_node); isUntypedCap ccap \<longrightarrow> src \<in> descendants_of' ptr m \<and> usableUntypedRange ccap = {} \<or> ptr \<in> descendants_of' src m \<and> usableUntypedRange src_cap = {}\<rbrakk> \<Longrightarrow> usableUntypedRange ccap = {} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ptr \<noteq> src; m ptr = Some (CTE ccap node'); untypedRange ccap = untypedRange src_cap; capAligned src_cap; isUntypedCap src_cap; m src = Some (CTE src_cap src_node); isUntypedCap ccap \<longrightarrow> src \<in> descendants_of' ptr m \<and> usableUntypedRange ccap = {} \<or> ptr \<in> descendants_of' src m \<and> usableUntypedRange src_cap = {}; isUntypedCap ccap\<rbrakk> \<Longrightarrow> usableUntypedRange ccap = {}
 2. \<lbrakk>ptr \<noteq> src; m ptr = Some (CTE ccap node'); untypedRange ccap = untypedRange src_cap; capAligned src_cap; isUntypedCap src_cap; m src = Some (CTE src_cap src_node); isUntypedCap ccap \<longrightarrow> src \<in> descendants_of' ptr m \<and> usableUntypedRange ccap = {} \<or> ptr \<in> descendants_of' src m \<and> usableUntypedRange src_cap = {}\<rbrakk> \<Longrightarrow> isUntypedCap ccap proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ptr \<noteq> src; m ptr = Some (CTE ccap node'); untypedRange ccap = untypedRange src_cap; capAligned src_cap; isUntypedCap src_cap; m src = Some (CTE src_cap src_node); src \<in> descendants_of' ptr m \<and> usableUntypedRange ccap = {} \<or> ptr \<in> descendants_of' src m \<and> usableUntypedRange src_cap = {}; isUntypedCap ccap\<rbrakk> \<Longrightarrow> usableUntypedRange ccap = {}
 2. \<lbrakk>ptr \<noteq> src; m ptr = Some (CTE ccap node'); untypedRange ccap = untypedRange src_cap; capAligned src_cap; isUntypedCap src_cap; m src = Some (CTE src_cap src_node); isUntypedCap ccap \<longrightarrow> src \<in> descendants_of' ptr m \<and> usableUntypedRange ccap = {} \<or> ptr \<in> descendants_of' src m \<and> usableUntypedRange src_cap = {}\<rbrakk> \<Longrightarrow> isUntypedCap ccap proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ptr \<noteq> src; m ptr = Some (CTE ccap node'); untypedRange ccap = untypedRange src_cap; capAligned src_cap; m src = Some (CTE src_cap src_node); src \<in> descendants_of' ptr m \<and> usableUntypedRange ccap = {} \<or> ptr \<in> descendants_of' src m \<and> usableUntypedRange src_cap = {}; isUntypedCap ccap; \<not> m \<turnstile> src \<rightarrow> ptr\<rbrakk> \<Longrightarrow> usableUntypedRange ccap = {}
 2. \<lbrakk>ptr \<noteq> src; m ptr = Some (CTE ccap node'); untypedRange ccap = untypedRange src_cap; capAligned src_cap; isUntypedCap src_cap; m src = Some (CTE src_cap src_node); isUntypedCap ccap \<longrightarrow> src \<in> descendants_of' ptr m \<and> usableUntypedRange ccap = {} \<or> ptr \<in> descendants_of' src m \<and> usableUntypedRange src_cap = {}\<rbrakk> \<Longrightarrow> isUntypedCap ccap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr \<noteq> src; m ptr = Some (CTE ccap node'); untypedRange ccap = untypedRange src_cap; capAligned src_cap; isUntypedCap src_cap; m src = Some (CTE src_cap src_node); isUntypedCap ccap \<longrightarrow> src \<in> descendants_of' ptr m \<and> usableUntypedRange ccap = {} \<or> ptr \<in> descendants_of' src m \<and> usableUntypedRange src_cap = {}\<rbrakk> \<Longrightarrow> isUntypedCap ccap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr \<noteq> src; m ptr = Some (CTE ccap node'); untypedRange ccap = untypedRange src_cap; isUntypedCap src_cap; m src = Some (CTE src_cap src_node); isUntypedCap ccap \<longrightarrow> src \<in> descendants_of' ptr m \<and> usableUntypedRange ccap = {} \<or> ptr \<in> descendants_of' src m \<and> usableUntypedRange src_cap = {}; untypedRange src_cap \<noteq> {}\<rbrakk> \<Longrightarrow> isUntypedCap ccap proof (prove)
goal:
No subgoals!