theory Untyped_AI

lemma range_cover_bound':
  fixes ptr :: "'a :: len word"
  assumes cover: "range_cover ptr sz sbit n"
  assumes le : "x < n"
  shows "unat (ptr + of_nat x * 2 ^ sbit) + 2 ^ sbit  \<le> 2 ^ len_of TYPE('a)" proof - have l: "unat (ptr && ~~ mask sz) + 2^ sz \<le> 2^ len_of TYPE('a)" using cover apply - apply (rule le_diff_conv2[THEN iffD1]) apply (simp add: range_cover_def) apply (rule unat_le_helper) apply (subst p2_minus) apply (erule range_cover.sz) apply (rule neg_mask_mono_le) apply (simp add: mask_def) done have n: "unat ((ptr && mask sz) + of_nat x * 2 ^ sbit) + 2^sbit \<le> 2 ^ sz" apply (rule le_trans[OF _ range_cover.range_cover_compare_bound[OF cover]]) apply (rule le_trans[where j = "(x+1) * 2^sbit + unat (ptr && mask sz)"]) apply clarsimp apply (rule le_trans[OF unat_plus_gt]) using le apply (simp add: range_cover.unat_of_nat_shift[OF cover]) apply simp using le apply (case_tac n,simp+) done show ?thesis using cover le apply - apply (frule iffD1[OF meta_eq_to_obj_eq[OF range_cover_def]]) apply (clarsimp) apply (frule range_cover_le[where n=x]) apply simp apply (subst word_plus_and_or_coroll2[symmetric,where w = "mask sz"]) apply (subst add.commute) apply (subst add.assoc) apply (subst unat_plus_simple[THEN iffD1]) apply (rule is_aligned_no_wrap') apply (rule is_aligned_neg_mask[OF le_refl]) apply (simp add: range_cover_def) apply (simp add: word_less_nat_alt) apply (rule le_less_trans[OF unat_plus_gt]) apply (erule range_cover.range_cover_compare[OF cover]) apply (subst add.assoc) apply (rule le_trans[OF _ l]) apply simp apply (simp add: n) done qed

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

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

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

goal (2 subgoals):
 1. unat (ptr && mask sz) + unat (word_of_nat x * 2 ^ sbit) \<le> x * 2 ^ sbit + unat (ptr && mask sz)
 2. (x + 1) * 2 ^ sbit + unat (ptr && mask sz) \<le> n * 2 ^ sbit + unat (ptr && mask sz) proof (prove)
goal (1 subgoal):
 1. (x + 1) * 2 ^ sbit + unat (ptr && mask sz) \<le> n * 2 ^ sbit + unat (ptr && mask sz) proof (prove)
goal (1 subgoal):
 1. 2 ^ sbit + x * 2 ^ sbit \<le> n * 2 ^ sbit proof (prove)
using this:
x < n

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

goal (1 subgoal):
 1. unat (ptr + word_of_nat x * 2 ^ sbit) + 2 ^ sbit \<le> 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. unat (ptr + word_of_nat x * 2 ^ sbit) + 2 ^ sbit \<le> 2 ^ LENGTH('a) proof (prove)
using this:
range_cover ptr sz sbit n
x < n

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

goal:
No subgoals!