theory Retype_AI

lemma unat_of_nat_n_shift:
  "gbits \<le> sbit \<Longrightarrow> unat (((of_nat n):: 'a :: len word) << gbits) = (n * 2^ gbits)" apply (simp add:shiftl_t2n field_simps) apply (subst mult.commute) apply (subst unat_mult_power_lem) apply (case_tac "gbits = sbit") apply (rule le_less_trans[OF range_cover_n_le(2)]) apply clarsimp apply (rule diff_less_mono) apply (rule sz) apply (rule sz) apply (rule le_less_trans[OF range_cover_n_le(1)]) apply clarsimp apply (rule diff_less_mono2) apply simp using sz apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. gbits \<le> sbit \<Longrightarrow> unat (word_of_nat n << gbits) = n * 2 ^ gbits proof (prove)
goal (1 subgoal):
 1. gbits \<le> sbit \<Longrightarrow> unat (word_of_nat n * 2 ^ gbits) = n * 2 ^ gbits proof (prove)
goal (1 subgoal):
 1. gbits \<le> sbit \<Longrightarrow> unat (2 ^ gbits * word_of_nat n) = n * 2 ^ gbits proof (prove)
goal (2 subgoals):
 1. gbits \<le> sbit \<Longrightarrow> n < 2 ^ (LENGTH('a) - gbits)
 2. gbits \<le> sbit \<Longrightarrow> 2 ^ gbits * n = n * 2 ^ gbits proof (prove)
goal (3 subgoals):
 1. \<lbrakk>gbits \<le> sbit; gbits = sbit\<rbrakk> \<Longrightarrow> n < 2 ^ (LENGTH('a) - gbits)
 2. \<lbrakk>gbits \<le> sbit; gbits \<noteq> sbit\<rbrakk> \<Longrightarrow> n < 2 ^ (LENGTH('a) - gbits)
 3. gbits \<le> sbit \<Longrightarrow> 2 ^ gbits * n = n * 2 ^ gbits proof (prove)
goal (3 subgoals):
 1. \<lbrakk>gbits \<le> sbit; gbits = sbit\<rbrakk> \<Longrightarrow> 2 ^ (sz - sbit) < 2 ^ (LENGTH('a) - gbits)
 2. \<lbrakk>gbits \<le> sbit; gbits \<noteq> sbit\<rbrakk> \<Longrightarrow> n < 2 ^ (LENGTH('a) - gbits)
 3. gbits \<le> sbit \<Longrightarrow> 2 ^ gbits * n = n * 2 ^ gbits proof (prove)
goal (3 subgoals):
 1. gbits = sbit \<Longrightarrow> sz - sbit < LENGTH('a) - sbit
 2. \<lbrakk>gbits \<le> sbit; gbits \<noteq> sbit\<rbrakk> \<Longrightarrow> n < 2 ^ (LENGTH('a) - gbits)
 3. gbits \<le> sbit \<Longrightarrow> 2 ^ gbits * n = n * 2 ^ gbits proof (prove)
goal (4 subgoals):
 1. gbits = sbit \<Longrightarrow> sz < LENGTH('a)
 2. gbits = sbit \<Longrightarrow> sbit \<le> sz
 3. \<lbrakk>gbits \<le> sbit; gbits \<noteq> sbit\<rbrakk> \<Longrightarrow> n < 2 ^ (LENGTH('a) - gbits)
 4. gbits \<le> sbit \<Longrightarrow> 2 ^ gbits * n = n * 2 ^ gbits proof (prove)
goal (3 subgoals):
 1. gbits = sbit \<Longrightarrow> sbit \<le> sz
 2. \<lbrakk>gbits \<le> sbit; gbits \<noteq> sbit\<rbrakk> \<Longrightarrow> n < 2 ^ (LENGTH('a) - gbits)
 3. gbits \<le> sbit \<Longrightarrow> 2 ^ gbits * n = n * 2 ^ gbits proof (prove)
goal (2 subgoals):
 1. \<lbrakk>gbits \<le> sbit; gbits \<noteq> sbit\<rbrakk> \<Longrightarrow> n < 2 ^ (LENGTH('a) - gbits)
 2. gbits \<le> sbit \<Longrightarrow> 2 ^ gbits * n = n * 2 ^ gbits proof (prove)
goal (2 subgoals):
 1. \<lbrakk>gbits \<le> sbit; gbits \<noteq> sbit\<rbrakk> \<Longrightarrow> 2 ^ (LENGTH('a) - sbit) < 2 ^ (LENGTH('a) - gbits)
 2. gbits \<le> sbit \<Longrightarrow> 2 ^ gbits * n = n * 2 ^ gbits proof (prove)
goal (2 subgoals):
 1. \<lbrakk>gbits \<le> sbit; gbits \<noteq> sbit\<rbrakk> \<Longrightarrow> LENGTH('a) - sbit < LENGTH('a) - gbits
 2. gbits \<le> sbit \<Longrightarrow> 2 ^ gbits * n = n * 2 ^ gbits proof (prove)
goal (3 subgoals):
 1. \<lbrakk>gbits \<le> sbit; gbits \<noteq> sbit\<rbrakk> \<Longrightarrow> gbits < sbit
 2. \<lbrakk>gbits \<le> sbit; gbits \<noteq> sbit\<rbrakk> \<Longrightarrow> gbits < LENGTH('a)
 3. gbits \<le> sbit \<Longrightarrow> 2 ^ gbits * n = n * 2 ^ gbits proof (prove)
goal (2 subgoals):
 1. \<lbrakk>gbits \<le> sbit; gbits \<noteq> sbit\<rbrakk> \<Longrightarrow> gbits < LENGTH('a)
 2. gbits \<le> sbit \<Longrightarrow> 2 ^ gbits * n = n * 2 ^ gbits proof (prove)
using this:
sz < LENGTH('a)
sbit \<le> sz
n + unat (ptr && mask sz >> sbit) \<le> 2 ^ (sz - sbit)

goal (2 subgoals):
 1. \<lbrakk>gbits \<le> sbit; gbits \<noteq> sbit\<rbrakk> \<Longrightarrow> gbits < LENGTH('a)
 2. gbits \<le> sbit \<Longrightarrow> 2 ^ gbits * n = n * 2 ^ gbits proof (prove)
goal (1 subgoal):
 1. gbits \<le> sbit \<Longrightarrow> 2 ^ gbits * n = n * 2 ^ gbits proof (prove)
goal:
No subgoals!