theory Untyped_AI

lemma range_cover_subset':
  "\<lbrakk>range_cover ptr sz sbit n; n \<noteq> 0\<rbrakk>
  \<Longrightarrow> {ptr ..ptr + of_nat n * 2 ^ sbit - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2^ sz - 1}" apply clarsimp apply (frule range_cover_cell_subset[OF _ of_nat_mono_maybe,where y1 = "(n - 1)"]) apply (drule range_cover.range_cover_n_less) apply (simp add:word_bits_def) apply simp apply (clarsimp simp:range_cover_def) apply (erule impE) apply (clarsimp simp:p_assoc_help) apply (rule is_aligned_no_wrap'[OF is_aligned_add_multI[OF _ le_refl refl ]]) apply (fastforce simp:range_cover_def)+ apply (clarsimp) apply (subst (asm) add.assoc) apply (subst (asm) distrib_right[where b = "1::'a::len word",simplified,symmetric]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz sbit n; n \<noteq> 0\<rbrakk> \<Longrightarrow> {ptr..ptr + word_of_nat n * 2 ^ sbit - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz sbit n; 0 < n; ptr \<le> ptr + word_of_nat n * 2 ^ sbit - 1\<rbrakk> \<Longrightarrow> ptr + word_of_nat n * 2 ^ sbit - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>range_cover ptr sz sbit n; 0 < n; ptr \<le> ptr + word_of_nat n * 2 ^ sbit - 1\<rbrakk> \<Longrightarrow> n < 2 ^ LENGTH('a)
 2. \<lbrakk>range_cover ptr sz sbit n; 0 < n; ptr \<le> ptr + word_of_nat n * 2 ^ sbit - 1\<rbrakk> \<Longrightarrow> n - 1 < n
 3. \<lbrakk>range_cover ptr sz sbit n; 0 < n; ptr \<le> ptr + word_of_nat n * 2 ^ sbit - 1; {ptr + word_of_nat (n - 1) * 2 ^ sbit..ptr + word_of_nat (n - 1) * 2 ^ sbit + 2 ^ sbit - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> ptr + word_of_nat n * 2 ^ sbit - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < n; ptr \<le> ptr + word_of_nat n * 2 ^ sbit - 1; n < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> n < 2 ^ LENGTH('a)
 2. \<lbrakk>range_cover ptr sz sbit n; 0 < n; ptr \<le> ptr + word_of_nat n * 2 ^ sbit - 1\<rbrakk> \<Longrightarrow> n - 1 < n
 3. \<lbrakk>range_cover ptr sz sbit n; 0 < n; ptr \<le> ptr + word_of_nat n * 2 ^ sbit - 1; {ptr + word_of_nat (n - 1) * 2 ^ sbit..ptr + word_of_nat (n - 1) * 2 ^ sbit + 2 ^ sbit - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> ptr + word_of_nat n * 2 ^ sbit - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>range_cover ptr sz sbit n; 0 < n; ptr \<le> ptr + word_of_nat n * 2 ^ sbit - 1\<rbrakk> \<Longrightarrow> n - 1 < n
 2. \<lbrakk>range_cover ptr sz sbit n; 0 < n; ptr \<le> ptr + word_of_nat n * 2 ^ sbit - 1; {ptr + word_of_nat (n - 1) * 2 ^ sbit..ptr + word_of_nat (n - 1) * 2 ^ sbit + 2 ^ sbit - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> ptr + word_of_nat n * 2 ^ sbit - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz sbit n; 0 < n; ptr \<le> ptr + word_of_nat n * 2 ^ sbit - 1; {ptr + word_of_nat (n - 1) * 2 ^ sbit..ptr + word_of_nat (n - 1) * 2 ^ sbit + 2 ^ sbit - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> ptr + word_of_nat n * 2 ^ sbit - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; ptr \<le> ptr + word_of_nat n * 2 ^ sbit - 1; ptr + (word_of_nat n - 1) * 2 ^ sbit \<le> ptr + (word_of_nat n - 1) * 2 ^ sbit + 2 ^ sbit - 1 \<longrightarrow> ptr \<le> ptr + (word_of_nat n - 1) * 2 ^ sbit \<and> ptr + (word_of_nat n - 1) * 2 ^ sbit + 2 ^ sbit - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1; is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; n + unat (ptr && mask sz >> sbit) \<le> 2 ^ (sz - sbit)\<rbrakk> \<Longrightarrow> ptr + word_of_nat n * 2 ^ sbit - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < n; ptr \<le> ptr + word_of_nat n * 2 ^ sbit - 1; is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; n + unat (ptr && mask sz >> sbit) \<le> 2 ^ (sz - sbit)\<rbrakk> \<Longrightarrow> ptr + (word_of_nat n - 1) * 2 ^ sbit \<le> ptr + (word_of_nat n - 1) * 2 ^ sbit + 2 ^ sbit - 1
 2. \<lbrakk>0 < n; ptr \<le> ptr + word_of_nat n * 2 ^ sbit - 1; is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; n + unat (ptr && mask sz >> sbit) \<le> 2 ^ (sz - sbit); ptr \<le> ptr + (word_of_nat n - 1) * 2 ^ sbit \<and> ptr + (word_of_nat n - 1) * 2 ^ sbit + 2 ^ sbit - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr + word_of_nat n * 2 ^ sbit - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < n; ptr \<le> ptr + word_of_nat n * 2 ^ sbit - 1; is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; n + unat (ptr && mask sz >> sbit) \<le> 2 ^ (sz - sbit)\<rbrakk> \<Longrightarrow> ptr + (word_of_nat n - 1) * 2 ^ sbit \<le> ptr + (word_of_nat n - 1) * 2 ^ sbit + (2 ^ sbit - 1)
 2. \<lbrakk>0 < n; ptr \<le> ptr + word_of_nat n * 2 ^ sbit - 1; is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; n + unat (ptr && mask sz >> sbit) \<le> 2 ^ (sz - sbit); ptr \<le> ptr + (word_of_nat n - 1) * 2 ^ sbit \<and> ptr + (word_of_nat n - 1) * 2 ^ sbit + 2 ^ sbit - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr + word_of_nat n * 2 ^ sbit - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>0 < n; ptr \<le> ptr + word_of_nat n * 2 ^ sbit - 1; is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; n + unat (ptr && mask sz >> sbit) \<le> 2 ^ (sz - sbit)\<rbrakk> \<Longrightarrow> is_aligned ptr sbit
 2. \<lbrakk>0 < n; ptr \<le> ptr + word_of_nat n * 2 ^ sbit - 1; is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; n + unat (ptr && mask sz >> sbit) \<le> 2 ^ (sz - sbit)\<rbrakk> \<Longrightarrow> 2 ^ sbit - 1 < 2 ^ sbit
 3. \<lbrakk>0 < n; ptr \<le> ptr + word_of_nat n * 2 ^ sbit - 1; is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; n + unat (ptr && mask sz >> sbit) \<le> 2 ^ (sz - sbit); ptr \<le> ptr + (word_of_nat n - 1) * 2 ^ sbit \<and> ptr + (word_of_nat n - 1) * 2 ^ sbit + 2 ^ sbit - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr + word_of_nat n * 2 ^ sbit - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; ptr \<le> ptr + word_of_nat n * 2 ^ sbit - 1; is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; n + unat (ptr && mask sz >> sbit) \<le> 2 ^ (sz - sbit); ptr \<le> ptr + (word_of_nat n - 1) * 2 ^ sbit \<and> ptr + (word_of_nat n - 1) * 2 ^ sbit + 2 ^ sbit - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr + word_of_nat n * 2 ^ sbit - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; ptr \<le> ptr + word_of_nat n * 2 ^ sbit - 1; is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; n + unat (ptr && mask sz >> sbit) \<le> 2 ^ (sz - sbit); ptr \<le> ptr + (word_of_nat n - 1) * 2 ^ sbit; ptr + (word_of_nat n - 1) * 2 ^ sbit + 2 ^ sbit - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr + word_of_nat n * 2 ^ sbit - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; ptr \<le> ptr + word_of_nat n * 2 ^ sbit - 1; is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; n + unat (ptr && mask sz >> sbit) \<le> 2 ^ (sz - sbit); ptr \<le> ptr + (word_of_nat n - 1) * 2 ^ sbit; ptr + ((word_of_nat n - 1) * 2 ^ sbit + 2 ^ sbit) - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr + word_of_nat n * 2 ^ sbit - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; ptr \<le> ptr + word_of_nat n * 2 ^ sbit - 1; is_aligned ptr sbit; sz < LENGTH('a); sbit \<le> sz; n + unat (ptr && mask sz >> sbit) \<le> 2 ^ (sz - sbit); ptr \<le> ptr + (word_of_nat n - 1) * 2 ^ sbit; ptr + (word_of_nat n - 1 + 1) * 2 ^ sbit - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr + word_of_nat n * 2 ^ sbit - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal:
No subgoals!