theory CNodeInv_R

lemma ex_Zombie_to:
  "\<lbrakk> ctes_of s p = Some cte; cteCap cte = Zombie p' b n;
       n \<noteq> 0; valid_objs' s \<rbrakk>
      \<Longrightarrow> ex_cte_cap_to' p' s" apply (simp add: ex_cte_cap_to'_def cte_wp_at_ctes_of) apply (intro exI, rule conjI, assumption) apply (simp add: image_def) apply (rule bexI[where x=0]) apply simp apply simp apply (frule(1) ctes_of_valid') apply (drule of_nat_mono_maybe[rotated, where 'a=32]) apply (simp only: word_bits_len_of) apply (erule valid_cap'_handy_bits) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s p = Some cte; cteCap cte = capability.Zombie p' b n; n \<noteq> 0; valid_objs' s\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) p' s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s p = Some cte; cteCap cte = capability.Zombie p' b n; 0 < n; valid_objs' s\<rbrakk> \<Longrightarrow> \<exists>cref cte. ctes_of s cref = Some cte \<and> p' \<in> cte_refs' (cteCap cte) (irq_node' s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s p = Some cte; cteCap cte = capability.Zombie p' b n; 0 < n; valid_objs' s\<rbrakk> \<Longrightarrow> p' \<in> cte_refs' (cteCap cte) (irq_node' s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s p = Some cte; cteCap cte = capability.Zombie p' b n; 0 < n; valid_objs' s\<rbrakk> \<Longrightarrow> \<exists>x\<in>{0..<word_of_nat n}. x * 2 ^ cteSizeBits = 0 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ctes_of s p = Some cte; cteCap cte = capability.Zombie p' b n; 0 < n; valid_objs' s\<rbrakk> \<Longrightarrow> 0 * 2 ^ cteSizeBits = 0
 2. \<lbrakk>ctes_of s p = Some cte; cteCap cte = capability.Zombie p' b n; 0 < n; valid_objs' s\<rbrakk> \<Longrightarrow> 0 \<in> {0..<word_of_nat n} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s p = Some cte; cteCap cte = capability.Zombie p' b n; 0 < n; valid_objs' s\<rbrakk> \<Longrightarrow> 0 \<in> {0..<word_of_nat n} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s p = Some cte; cteCap cte = capability.Zombie p' b n; 0 < n; valid_objs' s\<rbrakk> \<Longrightarrow> 0 < word_of_nat n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s p = Some cte; cteCap cte = capability.Zombie p' b n; 0 < n; valid_objs' s; valid_cap' (cteCap cte) s\<rbrakk> \<Longrightarrow> 0 < word_of_nat n proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ctes_of s p = Some cte; cteCap cte = capability.Zombie p' b n; valid_objs' s; valid_cap' (cteCap cte) s\<rbrakk> \<Longrightarrow> n < 2 ^ LENGTH(32)
 2. \<lbrakk>ctes_of s p = Some cte; cteCap cte = capability.Zombie p' b n; valid_objs' s; valid_cap' (cteCap cte) s; word_of_nat 0 < word_of_nat n\<rbrakk> \<Longrightarrow> 0 < word_of_nat n proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ctes_of s p = Some cte; cteCap cte = capability.Zombie p' b n; valid_objs' s; valid_cap' (capability.Zombie p' b n) s\<rbrakk> \<Longrightarrow> n < 2 ^ word_bits
 2. \<lbrakk>ctes_of s p = Some cte; cteCap cte = capability.Zombie p' b n; valid_objs' s; valid_cap' (cteCap cte) s; word_of_nat 0 < word_of_nat n\<rbrakk> \<Longrightarrow> 0 < word_of_nat n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s p = Some cte; cteCap cte = capability.Zombie p' b n; valid_objs' s; valid_cap' (cteCap cte) s; word_of_nat 0 < word_of_nat n\<rbrakk> \<Longrightarrow> 0 < word_of_nat n proof (prove)
goal:
No subgoals!