theory Retype_AI

lemma range_cover_compare_bound:
 "n * 2 ^ sbit + unat (ptr && mask sz) \<le> 2 ^ sz" proof - have mask_before_neg_mask: "(ptr && mask sz) && ~~ mask sbit = ptr && mask sz" using aligned sz by (simp add:mask_twice is_aligned_mask mask_out_sub_mask min_def) show ?thesis using aligned sz apply (drule_tac i = "a +b" for a b in Nat.mult_le_mono[where k = "2^sbit",OF _ le_refl]) apply (subst (asm) add_mult_distrib) apply (clarsimp simp: power_add[symmetric]) apply (subst (asm) unat_shiftl_absorb[where p = "sz - sbit"]) apply (rule less_imp_le) apply (rule shiftr_less_t2n) apply (rule less_le_trans) apply (rule and_mask_less') apply (simp add:word_bits_def) apply (rule two_power_increasing) apply simp apply (simp add:word_bits_def field_simps) apply simp apply (subst (asm) mult.commute[where b = "2^sbit"],
         subst (asm) shiftl_t2n[symmetric]) apply (subst (asm) and_not_mask[symmetric]) apply (simp add:mask_before_neg_mask) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n * 2 ^ sbit + unat (ptr && mask sz) \<le> 2 ^ sz proof (state)
goal (1 subgoal):
 1. n * 2 ^ sbit + unat (ptr && mask sz) \<le> 2 ^ sz proof (prove)
goal (1 subgoal):
 1. (ptr && mask sz) && ~~ mask sbit = ptr && mask sz proof (prove)
using this:
is_aligned ptr sbit
sz < LENGTH('a)
sbit \<le> sz
n + unat (ptr && mask sz >> sbit) \<le> 2 ^ (sz - sbit)

goal (1 subgoal):
 1. (ptr && mask sz) && ~~ mask sbit = ptr && mask sz proof (state)
this:
(ptr && mask sz) && ~~ mask sbit = ptr && mask sz

goal (1 subgoal):
 1. n * 2 ^ sbit + unat (ptr && mask sz) \<le> 2 ^ sz proof (prove)
goal (1 subgoal):
 1. n * 2 ^ sbit + unat (ptr && mask sz) \<le> 2 ^ sz proof (prove)
using this:
is_aligned ptr sbit
sz < LENGTH('a)
sbit \<le> sz
n + unat (ptr && mask sz >> sbit) \<le> 2 ^ (sz - sbit)

goal (1 subgoal):
 1. n * 2 ^ sbit + unat (ptr && mask sz) \<le> 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; (n + unat (ptr && mask sz >> sbit)) * 2 ^ sbit \<le> 2 ^ (sz - sbit) * 2 ^ sbit\<rbrakk> \<Longrightarrow> n * 2 ^ sbit + unat (ptr && mask sz) \<le> 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; n * 2 ^ sbit + unat (ptr && mask sz >> sbit) * 2 ^ sbit \<le> 2 ^ (sz - sbit) * 2 ^ sbit\<rbrakk> \<Longrightarrow> n * 2 ^ sbit + unat (ptr && mask sz) \<le> 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; n * 2 ^ sbit + unat (ptr && mask sz >> sbit) * 2 ^ sbit \<le> 2 ^ sz\<rbrakk> \<Longrightarrow> n * 2 ^ sbit + unat (ptr && mask sz) \<le> 2 ^ sz proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz\<rbrakk> \<Longrightarrow> ptr && mask sz >> sbit \<le> 2 ^ (sz - sbit)
 2. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz\<rbrakk> \<Longrightarrow> sz - sbit + sbit < LENGTH('a)
 3. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; n * 2 ^ sbit + unat ((ptr && mask sz >> sbit) * 2 ^ sbit) \<le> 2 ^ sz\<rbrakk> \<Longrightarrow> n * 2 ^ sbit + unat (ptr && mask sz) \<le> 2 ^ sz proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz\<rbrakk> \<Longrightarrow> ptr && mask sz >> sbit < 2 ^ (sz - sbit)
 2. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz\<rbrakk> \<Longrightarrow> sz - sbit + sbit < LENGTH('a)
 3. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; n * 2 ^ sbit + unat ((ptr && mask sz >> sbit) * 2 ^ sbit) \<le> 2 ^ sz\<rbrakk> \<Longrightarrow> n * 2 ^ sbit + unat (ptr && mask sz) \<le> 2 ^ sz proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz\<rbrakk> \<Longrightarrow> ptr && mask sz < 2 ^ (sbit + (sz - sbit))
 2. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz\<rbrakk> \<Longrightarrow> sz - sbit + sbit < LENGTH('a)
 3. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; n * 2 ^ sbit + unat ((ptr && mask sz >> sbit) * 2 ^ sbit) \<le> 2 ^ sz\<rbrakk> \<Longrightarrow> n * 2 ^ sbit + unat (ptr && mask sz) \<le> 2 ^ sz proof (prove)
goal (4 subgoals):
 1. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz\<rbrakk> \<Longrightarrow> ptr && mask sz < ?y17
 2. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz\<rbrakk> \<Longrightarrow> ?y17 \<le> 2 ^ (sbit + (sz - sbit))
 3. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz\<rbrakk> \<Longrightarrow> sz - sbit + sbit < LENGTH('a)
 4. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; n * 2 ^ sbit + unat ((ptr && mask sz >> sbit) * 2 ^ sbit) \<le> 2 ^ sz\<rbrakk> \<Longrightarrow> n * 2 ^ sbit + unat (ptr && mask sz) \<le> 2 ^ sz proof (prove)
goal (4 subgoals):
 1. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz\<rbrakk> \<Longrightarrow> sz < LENGTH('a)
 2. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz\<rbrakk> \<Longrightarrow> 2 ^ sz \<le> 2 ^ (sbit + (sz - sbit))
 3. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz\<rbrakk> \<Longrightarrow> sz - sbit + sbit < LENGTH('a)
 4. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; n * 2 ^ sbit + unat ((ptr && mask sz >> sbit) * 2 ^ sbit) \<le> 2 ^ sz\<rbrakk> \<Longrightarrow> n * 2 ^ sbit + unat (ptr && mask sz) \<le> 2 ^ sz proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz\<rbrakk> \<Longrightarrow> 2 ^ sz \<le> 2 ^ (sbit + (sz - sbit))
 2. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz\<rbrakk> \<Longrightarrow> sz - sbit + sbit < LENGTH('a)
 3. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; n * 2 ^ sbit + unat ((ptr && mask sz >> sbit) * 2 ^ sbit) \<le> 2 ^ sz\<rbrakk> \<Longrightarrow> n * 2 ^ sbit + unat (ptr && mask sz) \<le> 2 ^ sz proof (prove)
goal (4 subgoals):
 1. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz\<rbrakk> \<Longrightarrow> sz \<le> sbit + (sz - sbit)
 2. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz\<rbrakk> \<Longrightarrow> sbit + (sz - sbit) < LENGTH('a)
 3. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz\<rbrakk> \<Longrightarrow> sz - sbit + sbit < LENGTH('a)
 4. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; n * 2 ^ sbit + unat ((ptr && mask sz >> sbit) * 2 ^ sbit) \<le> 2 ^ sz\<rbrakk> \<Longrightarrow> n * 2 ^ sbit + unat (ptr && mask sz) \<le> 2 ^ sz proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz\<rbrakk> \<Longrightarrow> sbit + (sz - sbit) < LENGTH('a)
 2. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz\<rbrakk> \<Longrightarrow> sz - sbit + sbit < LENGTH('a)
 3. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; n * 2 ^ sbit + unat ((ptr && mask sz >> sbit) * 2 ^ sbit) \<le> 2 ^ sz\<rbrakk> \<Longrightarrow> n * 2 ^ sbit + unat (ptr && mask sz) \<le> 2 ^ sz proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz\<rbrakk> \<Longrightarrow> sz - sbit + sbit < LENGTH('a)
 2. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; n * 2 ^ sbit + unat ((ptr && mask sz >> sbit) * 2 ^ sbit) \<le> 2 ^ sz\<rbrakk> \<Longrightarrow> n * 2 ^ sbit + unat (ptr && mask sz) \<le> 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; n * 2 ^ sbit + unat ((ptr && mask sz >> sbit) * 2 ^ sbit) \<le> 2 ^ sz\<rbrakk> \<Longrightarrow> n * 2 ^ sbit + unat (ptr && mask sz) \<le> 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; n * 2 ^ sbit + unat (ptr && mask sz >> sbit << sbit) \<le> 2 ^ sz\<rbrakk> \<Longrightarrow> n * 2 ^ sbit + unat (ptr && mask sz) \<le> 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; n * 2 ^ sbit + unat ((ptr && mask sz) && ~~ mask sbit) \<le> 2 ^ sz\<rbrakk> \<Longrightarrow> n * 2 ^ sbit + unat (ptr && mask sz) \<le> 2 ^ sz proof (prove)
goal:
No subgoals! proof (state)
this:
n * 2 ^ sbit + unat (ptr && mask sz) \<le> 2 ^ sz

goal:
No subgoals!