theory Untyped_AI

lemma range_cover_idx_compare:
  "\<lbrakk>range_cover ptr sz sbit n;
    unat ((ptr && mask sz) + of_nat n * 2 ^ sbit) < 2 ^ sz;
    ptr \<noteq> ptr && ~~ mask sz; idx \<le> 2 ^ sz; idx \<le> unat (ptr && mask sz)\<rbrakk>
   \<Longrightarrow> (ptr && ~~ mask sz) + of_nat idx \<le> ptr + (of_nat n << sbit)" apply (subst not_less[symmetric]) apply (subst word_plus_and_or_coroll2[symmetric,where w = "mask sz" and t = ptr]) apply (subst add.commute) apply (simp add: not_less) apply (subst add.assoc) apply (rule word_add_le_mono2) apply (rule order_trans[OF word_of_nat_le]) apply simp apply (erule range_cover.range_cover_base_le) apply (subst unat_plus_simple[THEN iffD1]) apply (erule range_cover.range_cover_base_le) apply (subst unat_add_lem[THEN iffD1,symmetric]) apply (frule range_cover.unat_of_nat_shift[OF _ le_refl le_refl]) apply (simp add: shiftl_t2n field_simps del: add.commute add.assoc) apply (rule le_less_trans) apply (subst add.commute) apply (erule range_cover.range_cover_compare_bound) apply (simp add: range_cover_def) apply (rule less_diff_conv[THEN iffD1]) apply (rule less_le_trans) apply (simp add: shiftl_t2n field_simps) apply (subst le_diff_conv2) apply (rule less_imp_le[OF unat_lt2p]) apply (subst add.commute) apply (subst unat_power_lower[where 'a='a, symmetric]) apply (simp add: range_cover_def) apply (rule is_aligned_no_wrap_le[OF is_aligned_neg_mask[OF le_refl]]) apply (simp add: range_cover_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz sbit n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ sbit) < 2 ^ sz; ptr \<noteq> ptr && ~~ mask sz; idx \<le> 2 ^ sz; idx \<le> unat (ptr && mask sz)\<rbrakk> \<Longrightarrow> (ptr && ~~ mask sz) + word_of_nat idx \<le> ptr + (word_of_nat n << sbit) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz sbit n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ sbit) < 2 ^ sz; ptr \<noteq> ptr && ~~ mask sz; idx \<le> 2 ^ sz; idx \<le> unat (ptr && mask sz)\<rbrakk> \<Longrightarrow> \<not> ptr + (word_of_nat n << sbit) < (ptr && ~~ mask sz) + word_of_nat idx proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz sbit n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ sbit) < 2 ^ sz; ptr \<noteq> ptr && ~~ mask sz; idx \<le> 2 ^ sz; idx \<le> unat (ptr && mask sz)\<rbrakk> \<Longrightarrow> \<not> (ptr && mask sz) + (ptr && ~~ mask sz) + (word_of_nat n << sbit) < (ptr && ~~ mask sz) + word_of_nat idx proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz sbit n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ sbit) < 2 ^ sz; ptr \<noteq> ptr && ~~ mask sz; idx \<le> 2 ^ sz; idx \<le> unat (ptr && mask sz)\<rbrakk> \<Longrightarrow> \<not> (ptr && ~~ mask sz) + (ptr && mask sz) + (word_of_nat n << sbit) < (ptr && ~~ mask sz) + word_of_nat idx proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz sbit n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ sbit) < 2 ^ sz; ptr \<noteq> ptr && ~~ mask sz; idx \<le> 2 ^ sz; idx \<le> unat (ptr && mask sz)\<rbrakk> \<Longrightarrow> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + (ptr && mask sz) + (word_of_nat n << sbit) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz sbit n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ sbit) < 2 ^ sz; ptr \<noteq> ptr && ~~ mask sz; idx \<le> 2 ^ sz; idx \<le> unat (ptr && mask sz)\<rbrakk> \<Longrightarrow> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + ((ptr && mask sz) + (word_of_nat n << sbit)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>range_cover ptr sz sbit n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ sbit) < 2 ^ sz; ptr \<noteq> ptr && ~~ mask sz; idx \<le> 2 ^ sz; idx \<le> unat (ptr && mask sz)\<rbrakk> \<Longrightarrow> word_of_nat idx \<le> (ptr && mask sz) + (word_of_nat n << sbit)
 2. \<lbrakk>range_cover ptr sz sbit n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ sbit) < 2 ^ sz; ptr \<noteq> ptr && ~~ mask sz; idx \<le> 2 ^ sz; idx \<le> unat (ptr && mask sz)\<rbrakk> \<Longrightarrow> unat ((ptr && mask sz) + (word_of_nat n << sbit)) + unat (ptr && ~~ mask sz) < 2 ^ LENGTH('a) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>range_cover ptr sz sbit n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ sbit) < 2 ^ sz; ptr \<noteq> ptr && ~~ mask sz; idx \<le> 2 ^ sz; idx \<le> unat (ptr && mask sz)\<rbrakk> \<Longrightarrow> idx \<le> unat ?y3
 2. \<lbrakk>range_cover ptr sz sbit n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ sbit) < 2 ^ sz; ptr \<noteq> ptr && ~~ mask sz; idx \<le> 2 ^ sz; idx \<le> unat (ptr && mask sz)\<rbrakk> \<Longrightarrow> ?y3 \<le> (ptr && mask sz) + (word_of_nat n << sbit)
 3. \<lbrakk>range_cover ptr sz sbit n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ sbit) < 2 ^ sz; ptr \<noteq> ptr && ~~ mask sz; idx \<le> 2 ^ sz; idx \<le> unat (ptr && mask sz)\<rbrakk> \<Longrightarrow> unat ((ptr && mask sz) + (word_of_nat n << sbit)) + unat (ptr && ~~ mask sz) < 2 ^ LENGTH('a) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>range_cover ptr sz sbit n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ sbit) < 2 ^ sz; ptr \<noteq> ptr && ~~ mask sz; idx \<le> 2 ^ sz; idx \<le> unat (ptr && mask sz)\<rbrakk> \<Longrightarrow> ptr && mask sz \<le> (ptr && mask sz) + (word_of_nat n << sbit)
 2. \<lbrakk>range_cover ptr sz sbit n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ sbit) < 2 ^ sz; ptr \<noteq> ptr && ~~ mask sz; idx \<le> 2 ^ sz; idx \<le> unat (ptr && mask sz)\<rbrakk> \<Longrightarrow> unat ((ptr && mask sz) + (word_of_nat n << sbit)) + unat (ptr && ~~ mask sz) < 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz sbit n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ sbit) < 2 ^ sz; ptr \<noteq> ptr && ~~ mask sz; idx \<le> 2 ^ sz; idx \<le> unat (ptr && mask sz)\<rbrakk> \<Longrightarrow> unat ((ptr && mask sz) + (word_of_nat n << sbit)) + unat (ptr && ~~ mask sz) < 2 ^ LENGTH('a) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>range_cover ptr sz sbit n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ sbit) < 2 ^ sz; ptr \<noteq> ptr && ~~ mask sz; idx \<le> 2 ^ sz; idx \<le> unat (ptr && mask sz)\<rbrakk> \<Longrightarrow> ptr && mask sz \<le> (ptr && mask sz) + (word_of_nat n << sbit)
 2. \<lbrakk>range_cover ptr sz sbit n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ sbit) < 2 ^ sz; ptr \<noteq> ptr && ~~ mask sz; idx \<le> 2 ^ sz; idx \<le> unat (ptr && mask sz)\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + unat (word_of_nat n << sbit) + unat (ptr && ~~ mask sz) < 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz sbit n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ sbit) < 2 ^ sz; ptr \<noteq> ptr && ~~ mask sz; idx \<le> 2 ^ sz; idx \<le> unat (ptr && mask sz)\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + unat (word_of_nat n << sbit) + unat (ptr && ~~ mask sz) < 2 ^ LENGTH('a) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>range_cover ptr sz sbit n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ sbit) < 2 ^ sz; ptr \<noteq> ptr && ~~ mask sz; idx \<le> 2 ^ sz; idx \<le> unat (ptr && mask sz)\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + unat (word_of_nat n << sbit) < 2 ^ LENGTH('a)
 2. \<lbrakk>range_cover ptr sz sbit n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ sbit) < 2 ^ sz; ptr \<noteq> ptr && ~~ mask sz; idx \<le> 2 ^ sz; idx \<le> unat (ptr && mask sz)\<rbrakk> \<Longrightarrow> unat ((ptr && mask sz) + (word_of_nat n << sbit)) + unat (ptr && ~~ mask sz) < 2 ^ LENGTH('a) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>range_cover ptr sz sbit n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ sbit) < 2 ^ sz; ptr \<noteq> ptr && ~~ mask sz; idx \<le> 2 ^ sz; idx \<le> unat (ptr && mask sz); unat (word_of_nat n * 2 ^ sbit) = n * 2 ^ sbit\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + unat (word_of_nat n << sbit) < 2 ^ LENGTH('a)
 2. \<lbrakk>range_cover ptr sz sbit n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ sbit) < 2 ^ sz; ptr \<noteq> ptr && ~~ mask sz; idx \<le> 2 ^ sz; idx \<le> unat (ptr && mask sz)\<rbrakk> \<Longrightarrow> unat ((ptr && mask sz) + (word_of_nat n << sbit)) + unat (ptr && ~~ mask sz) < 2 ^ LENGTH('a) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>range_cover ptr sz sbit n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ sbit) < 2 ^ sz; ptr \<noteq> ptr && ~~ mask sz; idx \<le> 2 ^ sz; idx \<le> unat (ptr && mask sz); unat (word_of_nat n * 2 ^ sbit) = n * 2 ^ sbit\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + n * 2 ^ sbit < 2 ^ LENGTH('a)
 2. \<lbrakk>range_cover ptr sz sbit n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ sbit) < 2 ^ sz; ptr \<noteq> ptr && ~~ mask sz; idx \<le> 2 ^ sz; idx \<le> unat (ptr && mask sz)\<rbrakk> \<Longrightarrow> unat ((ptr && mask sz) + (word_of_nat n << sbit)) + unat (ptr && ~~ mask sz) < 2 ^ LENGTH('a) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>range_cover ptr sz sbit n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ sbit) < 2 ^ sz; ptr \<noteq> ptr && ~~ mask sz; idx \<le> 2 ^ sz; idx \<le> unat (ptr && mask sz); unat (word_of_nat n * 2 ^ sbit) = n * 2 ^ sbit\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + n * 2 ^ sbit \<le> ?y11
 2. \<lbrakk>range_cover ptr sz sbit n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ sbit) < 2 ^ sz; ptr \<noteq> ptr && ~~ mask sz; idx \<le> 2 ^ sz; idx \<le> unat (ptr && mask sz); unat (word_of_nat n * 2 ^ sbit) = n * 2 ^ sbit\<rbrakk> \<Longrightarrow> ?y11 < 2 ^ LENGTH('a)
 3. \<lbrakk>range_cover ptr sz sbit n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ sbit) < 2 ^ sz; ptr \<noteq> ptr && ~~ mask sz; idx \<le> 2 ^ sz; idx \<le> unat (ptr && mask sz)\<rbrakk> \<Longrightarrow> unat ((ptr && mask sz) + (word_of_nat n << sbit)) + unat (ptr && ~~ mask sz) < 2 ^ LENGTH('a) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>range_cover ptr sz sbit n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ sbit) < 2 ^ sz; ptr \<noteq> ptr && ~~ mask sz; idx \<le> 2 ^ sz; idx \<le> unat (ptr && mask sz); unat (word_of_nat n * 2 ^ sbit) = n * 2 ^ sbit\<rbrakk> \<Longrightarrow> n * 2 ^ sbit + unat (ptr && mask sz) \<le> ?y11
 2. \<lbrakk>range_cover ptr sz sbit n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ sbit) < 2 ^ sz; ptr \<noteq> ptr && ~~ mask sz; idx \<le> 2 ^ sz; idx \<le> unat (ptr && mask sz); unat (word_of_nat n * 2 ^ sbit) = n * 2 ^ sbit\<rbrakk> \<Longrightarrow> ?y11 < 2 ^ LENGTH('a)
 3. \<lbrakk>range_cover ptr sz sbit n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ sbit) < 2 ^ sz; ptr \<noteq> ptr && ~~ mask sz; idx \<le> 2 ^ sz; idx \<le> unat (ptr && mask sz)\<rbrakk> \<Longrightarrow> unat ((ptr && mask sz) + (word_of_nat n << sbit)) + unat (ptr && ~~ mask sz) < 2 ^ LENGTH('a) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>range_cover ptr sz sbit n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ sbit) < 2 ^ sz; ptr \<noteq> ptr && ~~ mask sz; idx \<le> 2 ^ sz; idx \<le> unat (ptr && mask sz); unat (word_of_nat n * 2 ^ sbit) = n * 2 ^ sbit\<rbrakk> \<Longrightarrow> 2 ^ sz < 2 ^ LENGTH('a)
 2. \<lbrakk>range_cover ptr sz sbit n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ sbit) < 2 ^ sz; ptr \<noteq> ptr && ~~ mask sz; idx \<le> 2 ^ sz; idx \<le> unat (ptr && mask sz)\<rbrakk> \<Longrightarrow> unat ((ptr && mask sz) + (word_of_nat n << sbit)) + unat (ptr && ~~ mask sz) < 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz sbit n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ sbit) < 2 ^ sz; ptr \<noteq> ptr && ~~ mask sz; idx \<le> 2 ^ sz; idx \<le> unat (ptr && mask sz)\<rbrakk> \<Longrightarrow> unat ((ptr && mask sz) + (word_of_nat n << sbit)) + unat (ptr && ~~ mask sz) < 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz sbit n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ sbit) < 2 ^ sz; ptr \<noteq> ptr && ~~ mask sz; idx \<le> 2 ^ sz; idx \<le> unat (ptr && mask sz)\<rbrakk> \<Longrightarrow> unat ((ptr && mask sz) + (word_of_nat n << sbit)) < 2 ^ LENGTH('a) - unat (ptr && ~~ mask sz) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>range_cover ptr sz sbit n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ sbit) < 2 ^ sz; ptr \<noteq> ptr && ~~ mask sz; idx \<le> 2 ^ sz; idx \<le> unat (ptr && mask sz)\<rbrakk> \<Longrightarrow> unat ((ptr && mask sz) + (word_of_nat n << sbit)) < ?y21
 2. \<lbrakk>range_cover ptr sz sbit n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ sbit) < 2 ^ sz; ptr \<noteq> ptr && ~~ mask sz; idx \<le> 2 ^ sz; idx \<le> unat (ptr && mask sz)\<rbrakk> \<Longrightarrow> ?y21 \<le> 2 ^ LENGTH('a) - unat (ptr && ~~ mask sz) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz sbit n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ sbit) < 2 ^ sz; ptr \<noteq> ptr && ~~ mask sz; idx \<le> 2 ^ sz; idx \<le> unat (ptr && mask sz)\<rbrakk> \<Longrightarrow> 2 ^ sz \<le> 2 ^ LENGTH('a) - unat (ptr && ~~ mask sz) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>range_cover ptr sz sbit n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ sbit) < 2 ^ sz; ptr \<noteq> ptr && ~~ mask sz; idx \<le> 2 ^ sz; idx \<le> unat (ptr && mask sz)\<rbrakk> \<Longrightarrow> unat (ptr && ~~ mask sz) \<le> 2 ^ LENGTH('a)
 2. \<lbrakk>range_cover ptr sz sbit n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ sbit) < 2 ^ sz; ptr \<noteq> ptr && ~~ mask sz; idx \<le> 2 ^ sz; idx \<le> unat (ptr && mask sz)\<rbrakk> \<Longrightarrow> 2 ^ sz + unat (ptr && ~~ mask sz) \<le> 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz sbit n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ sbit) < 2 ^ sz; ptr \<noteq> ptr && ~~ mask sz; idx \<le> 2 ^ sz; idx \<le> unat (ptr && mask sz)\<rbrakk> \<Longrightarrow> 2 ^ sz + unat (ptr && ~~ mask sz) \<le> 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz sbit n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ sbit) < 2 ^ sz; ptr \<noteq> ptr && ~~ mask sz; idx \<le> 2 ^ sz; idx \<le> unat (ptr && mask sz)\<rbrakk> \<Longrightarrow> unat (ptr && ~~ mask sz) + 2 ^ sz \<le> 2 ^ LENGTH('a) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>range_cover ptr sz sbit n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ sbit) < 2 ^ sz; ptr \<noteq> ptr && ~~ mask sz; idx \<le> 2 ^ sz; idx \<le> unat (ptr && mask sz)\<rbrakk> \<Longrightarrow> sz < LENGTH('a)
 2. \<lbrakk>range_cover ptr sz sbit n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ sbit) < 2 ^ sz; ptr \<noteq> ptr && ~~ mask sz; idx \<le> 2 ^ sz; idx \<le> unat (ptr && mask sz)\<rbrakk> \<Longrightarrow> unat (ptr && ~~ mask sz) + unat (2 ^ sz) \<le> 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz sbit n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ sbit) < 2 ^ sz; ptr \<noteq> ptr && ~~ mask sz; idx \<le> 2 ^ sz; idx \<le> unat (ptr && mask sz)\<rbrakk> \<Longrightarrow> unat (ptr && ~~ mask sz) + unat (2 ^ sz) \<le> 2 ^ LENGTH('a) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>range_cover ptr sz sbit n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ sbit) < 2 ^ sz; ptr \<noteq> ptr && ~~ mask sz; idx \<le> 2 ^ sz; idx \<le> unat (ptr && mask sz)\<rbrakk> \<Longrightarrow> sz < LENGTH('a)
 2. \<lbrakk>range_cover ptr sz sbit n; unat ((ptr && mask sz) + word_of_nat n * 2 ^ sbit) < 2 ^ sz; ptr \<noteq> ptr && ~~ mask sz; idx \<le> 2 ^ sz; idx \<le> unat (ptr && mask sz)\<rbrakk> \<Longrightarrow> unat (2 ^ sz) \<le> 2 ^ sz proof (prove)
goal:
No subgoals!