theory Delete_C

lemma valid_cap_capZombieNumber_unats:
  "\<lbrakk> s \<turnstile>' cap; isZombie cap \<rbrakk>
       \<Longrightarrow> capZombieNumber cap \<in> unats 32" apply (clarsimp simp: valid_cap'_def isCap_simps
                 split: zombie_type.split_asm) apply (simp add: unats_def) apply (clarsimp simp only: unats_def mem_simps) apply (erule order_le_less_trans) apply (rule power_strict_increasing) apply (simp add: word_bits_conv) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_cap' cap s; isZombie cap\<rbrakk> \<Longrightarrow> capZombieNumber cap \<in> unats 32 proof (prove)
goal (2 subgoals):
 1. \<And>v0 v2. \<lbrakk>cap = capability.Zombie v0 ZombieTCB v2; capAligned (capability.Zombie v0 ZombieTCB v2); v2 \<le> 5; tcbBlockSizeBits < word_bits; tcb_at' v0 s\<rbrakk> \<Longrightarrow> v2 \<in> unats 32
 2. \<And>v0 v1 v2 x2. \<lbrakk>cap = capability.Zombie v0 (ZombieCNode x2) v2; capAligned (capability.Zombie v0 (ZombieCNode x2) v2); v1 = ZombieCNode x2; v2 \<le> 2 ^ x2 \<and> objBits undefined + x2 < word_bits \<and> 0 < x2 \<and> (\<forall>addr. real_cte_at' (v0 + 2 ^ cteSizeBits * (addr && mask x2)) s)\<rbrakk> \<Longrightarrow> v2 \<in> unats 32 proof (prove)
goal (1 subgoal):
 1. \<And>v0 v1 v2 x2. \<lbrakk>cap = capability.Zombie v0 (ZombieCNode x2) v2; capAligned (capability.Zombie v0 (ZombieCNode x2) v2); v1 = ZombieCNode x2; v2 \<le> 2 ^ x2 \<and> objBits undefined + x2 < word_bits \<and> 0 < x2 \<and> (\<forall>addr. real_cte_at' (v0 + 2 ^ cteSizeBits * (addr && mask x2)) s)\<rbrakk> \<Longrightarrow> v2 \<in> unats 32 proof (prove)
goal (1 subgoal):
 1. \<And>v0 v1 v2 x2. \<lbrakk>cap = capability.Zombie v0 (ZombieCNode x2) v2; capAligned (capability.Zombie v0 (ZombieCNode x2) v2); v2 \<le> 2 ^ x2; objBits undefined + x2 < word_bits; 0 < x2; \<forall>addr. real_cte_at' (v0 + 2 ^ cteSizeBits * (addr && mask x2)) s\<rbrakk> \<Longrightarrow> v2 < 2 ^ 32 proof (prove)
goal (1 subgoal):
 1. \<And>v0 v1 v2 x2. \<lbrakk>cap = capability.Zombie v0 (ZombieCNode x2) v2; capAligned (capability.Zombie v0 (ZombieCNode x2) v2); objBits undefined + x2 < word_bits; 0 < x2; \<forall>addr. real_cte_at' (v0 + 2 ^ cteSizeBits * (addr && mask x2)) s\<rbrakk> \<Longrightarrow> 2 ^ x2 < 2 ^ 32 proof (prove)
goal (2 subgoals):
 1. \<And>v0 v1 v2 x2. \<lbrakk>cap = capability.Zombie v0 (ZombieCNode x2) v2; capAligned (capability.Zombie v0 (ZombieCNode x2) v2); objBits undefined + x2 < word_bits; 0 < x2; \<forall>addr. real_cte_at' (v0 + 2 ^ cteSizeBits * (addr && mask x2)) s\<rbrakk> \<Longrightarrow> x2 < 32
 2. \<And>v0 v1 v2 x2. \<lbrakk>cap = capability.Zombie v0 (ZombieCNode x2) v2; capAligned (capability.Zombie v0 (ZombieCNode x2) v2); objBits undefined + x2 < word_bits; 0 < x2; \<forall>addr. real_cte_at' (v0 + 2 ^ cteSizeBits * (addr && mask x2)) s\<rbrakk> \<Longrightarrow> 1 < 2 proof (prove)
goal (1 subgoal):
 1. \<And>v0 v1 v2 x2. \<lbrakk>cap = capability.Zombie v0 (ZombieCNode x2) v2; capAligned (capability.Zombie v0 (ZombieCNode x2) v2); objBits undefined + x2 < word_bits; 0 < x2; \<forall>addr. real_cte_at' (v0 + 2 ^ cteSizeBits * (addr && mask x2)) s\<rbrakk> \<Longrightarrow> 1 < 2 proof (prove)
goal:
No subgoals!