theory CNodeInv_AI

lemma nat_to_cref_replicate_Zombie:
  "\<And>zb n (s::'state_ext state) p m.
    \<lbrakk> nat_to_cref (zombie_cte_bits zb) n = replicate (zombie_cte_bits zb) False;
        s \<turnstile> cap.Zombie p zb m; n < m \<rbrakk>
      \<Longrightarrow> n = 0" apply (subgoal_tac "unat (of_bl (nat_to_cref (zombie_cte_bits zb) n)) = 0") apply (subst(asm) unat_of_bl_nat_to_cref) apply (drule valid_Zombie_n_less_cte_bits, simp) apply (erule zombie_cte_bits_less) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>zb n s p m. \<lbrakk>nat_to_cref (zombie_cte_bits zb) n = replicate (zombie_cte_bits zb) False; s \<turnstile> Zombie p zb m; n < m\<rbrakk> \<Longrightarrow> n = 0 proof (prove)
goal (2 subgoals):
 1. \<And>zb n s p m. \<lbrakk>nat_to_cref (zombie_cte_bits zb) n = replicate (zombie_cte_bits zb) False; s \<turnstile> Zombie p zb m; n < m; unat (of_bl (nat_to_cref (zombie_cte_bits zb) n)) = 0\<rbrakk> \<Longrightarrow> n = 0
 2. \<And>zb n s p m. \<lbrakk>nat_to_cref (zombie_cte_bits zb) n = replicate (zombie_cte_bits zb) False; s \<turnstile> Zombie p zb m; n < m\<rbrakk> \<Longrightarrow> unat (of_bl (nat_to_cref (zombie_cte_bits zb) n)) = 0 proof (prove)
goal (4 subgoals):
 1. \<And>zb n s p m. \<lbrakk>nat_to_cref (zombie_cte_bits zb) n = replicate (zombie_cte_bits zb) False; s \<turnstile> Zombie p zb m; n < m\<rbrakk> \<Longrightarrow> n < 2 ^ zombie_cte_bits zb
 2. \<And>zb n s p m. \<lbrakk>nat_to_cref (zombie_cte_bits zb) n = replicate (zombie_cte_bits zb) False; s \<turnstile> Zombie p zb m; n < m\<rbrakk> \<Longrightarrow> zombie_cte_bits zb < word_bits
 3. \<And>zb n s p m. \<lbrakk>nat_to_cref (zombie_cte_bits zb) n = replicate (zombie_cte_bits zb) False; s \<turnstile> Zombie p zb m; n < m; n = 0\<rbrakk> \<Longrightarrow> n = 0
 4. \<And>zb n s p m. \<lbrakk>nat_to_cref (zombie_cte_bits zb) n = replicate (zombie_cte_bits zb) False; s \<turnstile> Zombie p zb m; n < m\<rbrakk> \<Longrightarrow> unat (of_bl (nat_to_cref (zombie_cte_bits zb) n)) = 0 proof (prove)
goal (3 subgoals):
 1. \<And>zb n s p m. \<lbrakk>nat_to_cref (zombie_cte_bits zb) n = replicate (zombie_cte_bits zb) False; s \<turnstile> Zombie p zb m; n < m\<rbrakk> \<Longrightarrow> zombie_cte_bits zb < word_bits
 2. \<And>zb n s p m. \<lbrakk>nat_to_cref (zombie_cte_bits zb) n = replicate (zombie_cte_bits zb) False; s \<turnstile> Zombie p zb m; n < m; n = 0\<rbrakk> \<Longrightarrow> n = 0
 3. \<And>zb n s p m. \<lbrakk>nat_to_cref (zombie_cte_bits zb) n = replicate (zombie_cte_bits zb) False; s \<turnstile> Zombie p zb m; n < m\<rbrakk> \<Longrightarrow> unat (of_bl (nat_to_cref (zombie_cte_bits zb) n)) = 0 proof (prove)
goal (2 subgoals):
 1. \<And>zb n s p m. \<lbrakk>nat_to_cref (zombie_cte_bits zb) n = replicate (zombie_cte_bits zb) False; s \<turnstile> Zombie p zb m; n < m; n = 0\<rbrakk> \<Longrightarrow> n = 0
 2. \<And>zb n s p m. \<lbrakk>nat_to_cref (zombie_cte_bits zb) n = replicate (zombie_cte_bits zb) False; s \<turnstile> Zombie p zb m; n < m\<rbrakk> \<Longrightarrow> unat (of_bl (nat_to_cref (zombie_cte_bits zb) n)) = 0 proof (prove)
goal (1 subgoal):
 1. \<And>zb n s p m. \<lbrakk>nat_to_cref (zombie_cte_bits zb) n = replicate (zombie_cte_bits zb) False; s \<turnstile> Zombie p zb m; n < m\<rbrakk> \<Longrightarrow> unat (of_bl (nat_to_cref (zombie_cte_bits zb) n)) = 0 proof (prove)
goal:
No subgoals!