theory Retype_AI

lemma range_cover_not_zero_shift:
  "\<lbrakk>n \<noteq> 0; range_cover (ptr :: 'a :: len word) sz bits n; gbits \<le> bits\<rbrakk>
   \<Longrightarrow> ((of_nat n) :: 'a :: len word) << gbits \<noteq> 0" apply (rule word_shift_nonzero[where m = "sz-gbits"]) prefer 2 apply (clarsimp simp:range_cover_def) apply (clarsimp simp:word_le_nat_alt) apply (subst unat_power_lower) apply (rule less_le_trans[OF diff_less_Suc]) apply (simp add:range_cover_def) apply (simp add:range_cover.unat_of_nat_n) apply (erule le_trans[OF range_cover.range_cover_n_le(2)]) apply (rule power_increasing) apply simp+ using range_cover_not_zero apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<noteq> 0; range_cover ptr sz bits n; gbits \<le> bits\<rbrakk> \<Longrightarrow> word_of_nat n << gbits \<noteq> 0 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>n \<noteq> 0; range_cover ptr sz bits n; gbits \<le> bits\<rbrakk> \<Longrightarrow> word_of_nat n \<le> 2 ^ (sz - gbits)
 2. \<lbrakk>n \<noteq> 0; range_cover ptr sz bits n; gbits \<le> bits\<rbrakk> \<Longrightarrow> sz - gbits + gbits < LENGTH('a)
 3. \<lbrakk>n \<noteq> 0; range_cover ptr sz bits n; gbits \<le> bits\<rbrakk> \<Longrightarrow> word_of_nat n \<noteq> 0 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>n \<noteq> 0; range_cover ptr sz bits n; gbits \<le> bits\<rbrakk> \<Longrightarrow> sz - gbits + gbits < LENGTH('a)
 2. \<lbrakk>n \<noteq> 0; range_cover ptr sz bits n; gbits \<le> bits\<rbrakk> \<Longrightarrow> word_of_nat n \<le> 2 ^ (sz - gbits)
 3. \<lbrakk>n \<noteq> 0; range_cover ptr sz bits n; gbits \<le> bits\<rbrakk> \<Longrightarrow> word_of_nat n \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<noteq> 0; range_cover ptr sz bits n; gbits \<le> bits\<rbrakk> \<Longrightarrow> word_of_nat n \<le> 2 ^ (sz - gbits)
 2. \<lbrakk>n \<noteq> 0; range_cover ptr sz bits n; gbits \<le> bits\<rbrakk> \<Longrightarrow> word_of_nat n \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < n; range_cover ptr sz bits n; gbits \<le> bits\<rbrakk> \<Longrightarrow> unat (word_of_nat n) \<le> unat (2 ^ (sz - gbits))
 2. \<lbrakk>n \<noteq> 0; range_cover ptr sz bits n; gbits \<le> bits\<rbrakk> \<Longrightarrow> word_of_nat n \<noteq> 0 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < n; range_cover ptr sz bits n; gbits \<le> bits\<rbrakk> \<Longrightarrow> sz - gbits < LENGTH('a)
 2. \<lbrakk>0 < n; range_cover ptr sz bits n; gbits \<le> bits\<rbrakk> \<Longrightarrow> unat (word_of_nat n) \<le> 2 ^ (sz - gbits)
 3. \<lbrakk>n \<noteq> 0; range_cover ptr sz bits n; gbits \<le> bits\<rbrakk> \<Longrightarrow> word_of_nat n \<noteq> 0 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < n; range_cover ptr sz bits n; gbits \<le> bits\<rbrakk> \<Longrightarrow> Suc sz \<le> LENGTH('a)
 2. \<lbrakk>0 < n; range_cover ptr sz bits n; gbits \<le> bits\<rbrakk> \<Longrightarrow> unat (word_of_nat n) \<le> 2 ^ (sz - gbits)
 3. \<lbrakk>n \<noteq> 0; range_cover ptr sz bits n; gbits \<le> bits\<rbrakk> \<Longrightarrow> word_of_nat n \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < n; range_cover ptr sz bits n; gbits \<le> bits\<rbrakk> \<Longrightarrow> unat (word_of_nat n) \<le> 2 ^ (sz - gbits)
 2. \<lbrakk>n \<noteq> 0; range_cover ptr sz bits n; gbits \<le> bits\<rbrakk> \<Longrightarrow> word_of_nat n \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < n; range_cover ptr sz bits n; gbits \<le> bits\<rbrakk> \<Longrightarrow> n \<le> 2 ^ (sz - gbits)
 2. \<lbrakk>n \<noteq> 0; range_cover ptr sz bits n; gbits \<le> bits\<rbrakk> \<Longrightarrow> word_of_nat n \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < n; gbits \<le> bits\<rbrakk> \<Longrightarrow> 2 ^ (sz - bits) \<le> 2 ^ (sz - gbits)
 2. \<lbrakk>n \<noteq> 0; range_cover ptr sz bits n; gbits \<le> bits\<rbrakk> \<Longrightarrow> word_of_nat n \<noteq> 0 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < n; gbits \<le> bits\<rbrakk> \<Longrightarrow> sz - bits \<le> sz - gbits
 2. \<lbrakk>0 < n; gbits \<le> bits\<rbrakk> \<Longrightarrow> 1 \<le> 2
 3. \<lbrakk>n \<noteq> 0; range_cover ptr sz bits n; gbits \<le> bits\<rbrakk> \<Longrightarrow> word_of_nat n \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; range_cover ptr sz bits n; gbits \<le> bits\<rbrakk> \<Longrightarrow> word_of_nat n \<noteq> 0 proof (prove)
using this:
\<lbrakk>?n \<noteq> 0; range_cover ?ptr ?sz ?bits ?n\<rbrakk> \<Longrightarrow> word_of_nat ?n \<noteq> 0

goal (1 subgoal):
 1. \<lbrakk>0 < n; range_cover ptr sz bits n; gbits \<le> bits\<rbrakk> \<Longrightarrow> word_of_nat n \<noteq> 0 proof (prove)
goal:
No subgoals!