theory CSpace_R

lemma ex_nonz_cap_not_global':
  "\<lbrakk>ex_nonz_cap_to' t s; valid_objs' s; valid_global_refs' s\<rbrakk> \<Longrightarrow>
   t \<notin> global_refs' s" apply (clarsimp simp: ex_nonz_cap_to'_def cte_wp_at_ctes_of) apply (frule(1) valid_global_refsD') apply clarsimp apply (drule orthD1, erule (1) subsetD) apply (subgoal_tac "s \<turnstile>' cteCap cte") apply (fastforce simp: valid_cap'_def capRange_def capAligned_def
                         is_aligned_no_overflow
                  split: cte.split_asm capability.split_asm) apply (case_tac cte) apply (clarsimp simp: ctes_of_valid_cap') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ex_nonz_cap_to' t s; valid_objs' s; valid_global_refs' s\<rbrakk> \<Longrightarrow> t \<notin> global_refs' s proof (prove)
goal (1 subgoal):
 1. \<And>cref cte. \<lbrakk>valid_objs' s; valid_global_refs' s; ctes_of s cref = Some cte; t \<in> zobj_refs' (cteCap cte); t \<in> global_refs' s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cref cte. \<lbrakk>valid_objs' s; valid_global_refs' s; ctes_of s cref = Some cte; t \<in> zobj_refs' (cteCap cte); t \<in> global_refs' s; kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s \<subseteq> kernel_data_refs\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cref cte. \<lbrakk>valid_objs' s; valid_global_refs' s; ctes_of s cref = Some cte; t \<in> zobj_refs' (cteCap cte); t \<in> global_refs' s; kernel_data_refs \<inter> capRange (cteCap cte) = {}; global_refs' s \<subseteq> kernel_data_refs\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cref cte. \<lbrakk>valid_objs' s; valid_global_refs' s; ctes_of s cref = Some cte; t \<in> zobj_refs' (cteCap cte); t \<in> global_refs' s; global_refs' s \<subseteq> kernel_data_refs; t \<notin> capRange (cteCap cte)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>cref cte. \<lbrakk>valid_objs' s; valid_global_refs' s; ctes_of s cref = Some cte; t \<in> zobj_refs' (cteCap cte); t \<in> global_refs' s; global_refs' s \<subseteq> kernel_data_refs; t \<notin> capRange (cteCap cte); valid_cap' (cteCap cte) s\<rbrakk> \<Longrightarrow> False
 2. \<And>cref cte. \<lbrakk>valid_objs' s; valid_global_refs' s; ctes_of s cref = Some cte; t \<in> zobj_refs' (cteCap cte); t \<in> global_refs' s; global_refs' s \<subseteq> kernel_data_refs; t \<notin> capRange (cteCap cte)\<rbrakk> \<Longrightarrow> valid_cap' (cteCap cte) s proof (prove)
goal (1 subgoal):
 1. \<And>cref cte. \<lbrakk>valid_objs' s; valid_global_refs' s; ctes_of s cref = Some cte; t \<in> zobj_refs' (cteCap cte); t \<in> global_refs' s; global_refs' s \<subseteq> kernel_data_refs; t \<notin> capRange (cteCap cte)\<rbrakk> \<Longrightarrow> valid_cap' (cteCap cte) s proof (prove)
goal (1 subgoal):
 1. \<And>cref cte x1 x2. \<lbrakk>valid_objs' s; valid_global_refs' s; ctes_of s cref = Some cte; t \<in> zobj_refs' (cteCap cte); t \<in> global_refs' s; global_refs' s \<subseteq> kernel_data_refs; t \<notin> capRange (cteCap cte); cte = CTE x1 x2\<rbrakk> \<Longrightarrow> valid_cap' (cteCap cte) s proof (prove)
goal:
No subgoals!