theory Retype_AI

lemma range_cover_compare:
  assumes pointer:"p < n"
  shows "unat (ptr && mask sz) + unat (((of_nat p) :: 'a :: len word) * 2 ^ sbit) < 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) have absolute_compare:"n * 2 ^ sbit + unat (ptr && mask sz) \<le> 2 ^ sz" by (rule range_cover_compare_bound) have no_overflow_n:"n * 2^sbit < 2^len_of TYPE('a)" using aligned sz apply (clarsimp dest!:add_leD1) apply (rule le_less_trans) apply (drule Nat.mult_le_mono[where i = n and k = "2^sbit",OF _ le_refl]) apply (clarsimp simp: power_add[symmetric]) apply (assumption) apply clarsimp done have no_overflow_p:"p * 2^sbit < 2^len_of TYPE('a)" apply (rule le_less_trans[OF _ no_overflow_n]) apply (simp add:pointer less_imp_le) done show ?thesis apply (rule less_le_trans[OF _ absolute_compare]) apply (subst add.commute) apply clarsimp apply (case_tac "p = 0") apply (insert pointer) apply (clarsimp simp: range_cover_def pointer) apply (simp add:unat_word_ariths) apply (rule le_less_trans[OF mod_less_eq_dividend]) apply (rule less_le_trans[OF mult_less_mono1[where j = n]]) apply (cut_tac no_overflow_p) apply (drule multi_lessD[OF no_overflow_p],simp) apply (clarsimp simp:unat_of_nat word_bits_def) using sz apply (simp add:unat_gt_0 range_cover_def) apply (rule mult_le_mono2) apply (rule unat_le_helper) apply simp done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat (ptr && mask sz) + unat (word_of_nat p * 2 ^ sbit) < 2 ^ sz proof (state)
goal (1 subgoal):
 1. unat (ptr && mask sz) + unat (word_of_nat p * 2 ^ sbit) < 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. unat (ptr && mask sz) + unat (word_of_nat p * 2 ^ sbit) < 2 ^ sz proof (prove)
goal (1 subgoal):
 1. n * 2 ^ sbit + unat (ptr && mask sz) \<le> 2 ^ sz proof (state)
this:
n * 2 ^ sbit + unat (ptr && mask sz) \<le> 2 ^ sz

goal (1 subgoal):
 1. unat (ptr && mask sz) + unat (word_of_nat p * 2 ^ sbit) < 2 ^ sz proof (prove)
goal (1 subgoal):
 1. n * 2 ^ sbit < 2 ^ LENGTH('a) 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 < 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; n \<le> 2 ^ (sz - sbit)\<rbrakk> \<Longrightarrow> n * 2 ^ sbit < 2 ^ LENGTH('a) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; n \<le> 2 ^ (sz - sbit)\<rbrakk> \<Longrightarrow> n * 2 ^ sbit \<le> ?y5
 2. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; n \<le> 2 ^ (sz - sbit)\<rbrakk> \<Longrightarrow> ?y5 < 2 ^ LENGTH('a) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; n * 2 ^ sbit \<le> 2 ^ (sz - sbit) * 2 ^ sbit\<rbrakk> \<Longrightarrow> n * 2 ^ sbit \<le> ?y5
 2. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; n \<le> 2 ^ (sz - sbit)\<rbrakk> \<Longrightarrow> ?y5 < 2 ^ LENGTH('a) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; n * 2 ^ sbit \<le> 2 ^ sz\<rbrakk> \<Longrightarrow> n * 2 ^ sbit \<le> ?y5
 2. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; n \<le> 2 ^ (sz - sbit)\<rbrakk> \<Longrightarrow> ?y5 < 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; n \<le> 2 ^ (sz - sbit)\<rbrakk> \<Longrightarrow> 2 ^ sz < 2 ^ LENGTH('a) proof (prove)
goal:
No subgoals! proof (state)
this:
n * 2 ^ sbit < 2 ^ LENGTH('a)

goal (1 subgoal):
 1. unat (ptr && mask sz) + unat (word_of_nat p * 2 ^ sbit) < 2 ^ sz proof (prove)
goal (1 subgoal):
 1. p * 2 ^ sbit < 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. p * 2 ^ sbit \<le> n * 2 ^ sbit proof (prove)
goal:
No subgoals! proof (state)
this:
p * 2 ^ sbit < 2 ^ LENGTH('a)

goal (1 subgoal):
 1. unat (ptr && mask sz) + unat (word_of_nat p * 2 ^ sbit) < 2 ^ sz proof (prove)
goal (1 subgoal):
 1. unat (ptr && mask sz) + unat (word_of_nat p * 2 ^ sbit) < 2 ^ sz proof (prove)
goal (1 subgoal):
 1. unat (ptr && mask sz) + unat (word_of_nat p * 2 ^ sbit) < n * 2 ^ sbit + unat (ptr && mask sz) proof (prove)
goal (1 subgoal):
 1. unat (word_of_nat p * 2 ^ sbit) + unat (ptr && mask sz) < n * 2 ^ sbit + unat (ptr && mask sz) proof (prove)
goal (1 subgoal):
 1. unat (word_of_nat p * 2 ^ sbit) < n * 2 ^ sbit proof (prove)
goal (2 subgoals):
 1. p = 0 \<Longrightarrow> unat (word_of_nat p * 2 ^ sbit) < n * 2 ^ sbit
 2. p \<noteq> 0 \<Longrightarrow> unat (word_of_nat p * 2 ^ sbit) < n * 2 ^ sbit proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p = 0; p < n\<rbrakk> \<Longrightarrow> unat (word_of_nat p * 2 ^ sbit) < n * 2 ^ sbit
 2. \<lbrakk>p \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> unat (word_of_nat p * 2 ^ sbit) < n * 2 ^ sbit proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<noteq> 0; p < n\<rbrakk> \<Longrightarrow> unat (word_of_nat p * 2 ^ sbit) < n * 2 ^ sbit proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < p; p < n\<rbrakk> \<Longrightarrow> unat (word_of_nat p) * unat (2 ^ sbit) mod 2 ^ LENGTH('a) < n * 2 ^ sbit proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < p; p < n\<rbrakk> \<Longrightarrow> unat (word_of_nat p) * unat (2 ^ sbit) < n * 2 ^ sbit proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < p; p < n\<rbrakk> \<Longrightarrow> unat (word_of_nat p) < n
 2. \<lbrakk>0 < p; p < n\<rbrakk> \<Longrightarrow> 0 < unat (2 ^ sbit)
 3. \<lbrakk>0 < p; p < n\<rbrakk> \<Longrightarrow> n * unat (2 ^ sbit) \<le> n * 2 ^ sbit proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < p; p < n; p * 2 ^ sbit < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> unat (word_of_nat p) < n
 2. \<lbrakk>0 < p; p < n\<rbrakk> \<Longrightarrow> 0 < unat (2 ^ sbit)
 3. \<lbrakk>0 < p; p < n\<rbrakk> \<Longrightarrow> n * unat (2 ^ sbit) \<le> n * 2 ^ sbit proof (prove)
goal (3 subgoals):
 1. \<lbrakk>p < n; p * 2 ^ sbit < 2 ^ LENGTH('a); p < 2 ^ LENGTH('a) \<and> 2 ^ sbit < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> unat (word_of_nat p) < n
 2. \<lbrakk>0 < p; p < n\<rbrakk> \<Longrightarrow> 0 < unat (2 ^ sbit)
 3. \<lbrakk>0 < p; p < n\<rbrakk> \<Longrightarrow> n * unat (2 ^ sbit) \<le> n * 2 ^ sbit proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < p; p < n\<rbrakk> \<Longrightarrow> 0 < unat (2 ^ sbit)
 2. \<lbrakk>0 < p; p < n\<rbrakk> \<Longrightarrow> n * unat (2 ^ sbit) \<le> n * 2 ^ sbit 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>0 < p; p < n\<rbrakk> \<Longrightarrow> 0 < unat (2 ^ sbit)
 2. \<lbrakk>0 < p; p < n\<rbrakk> \<Longrightarrow> n * unat (2 ^ sbit) \<le> n * 2 ^ sbit proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < p; p < n\<rbrakk> \<Longrightarrow> n * unat (2 ^ sbit) \<le> n * 2 ^ sbit proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < p; p < n\<rbrakk> \<Longrightarrow> unat (2 ^ sbit) \<le> 2 ^ sbit proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < p; p < n\<rbrakk> \<Longrightarrow> 2 ^ sbit \<le> word_of_nat (2 ^ sbit) proof (prove)
goal:
No subgoals! proof (state)
this:
unat (ptr && mask sz) + unat (word_of_nat p * 2 ^ sbit) < 2 ^ sz

goal:
No subgoals!