theory ArchVSpaceEntries_AI

lemma shift_0x3C_set:
  "\<lbrakk> is_aligned p 6; 8 \<le> bits; bits < 32; len_of TYPE('a) = bits - 2 \<rbrakk> \<Longrightarrow>
   (\<lambda>x. ucast (x + p && mask bits >> 2) :: ('a :: len) word) ` set [0 :: word32 , 4 .e. 0x3C]
        = {x. x && ~~ mask 4 = ucast (p && mask bits >> 2)}" apply (clarsimp simp: upto_enum_step_def word_shift_by_2 image_image) apply (subst image_cong[where N="{x. x < 2 ^ 4}"]) apply (safe, simp_all)[1] apply (drule plus_one_helper2, simp_all)[1] apply (drule word_le_minus_one_leq, simp_all)[1] apply (rule_tac f="\<lambda>x. ucast (x && mask bits >> 2)" in arg_cong) apply (rule trans[OF add.commute is_aligned_add_or], assumption) apply (rule shiftl_less_t2n, simp_all)[1] apply safe apply (frule upper_bits_unset_is_l2p_32[THEN iffD2, rotated]) apply (simp add: word_bits_conv) apply (rule word_eqI) apply (simp add: word_ops_nth_size word_size nth_ucast nth_shiftr
                    nth_shiftl neg_mask_test_bit
                    word_bits_conv) apply (safe, simp_all add: is_aligned_nth)[1] apply (rule_tac x="ucast x && mask 4" in image_eqI) apply (rule word_eqI[rule_format]) apply (drule_tac x=n in word_eqD) apply (simp add: word_ops_nth_size word_size nth_ucast nth_shiftr
                    nth_shiftl) apply (safe, simp_all) apply (rule order_less_le_trans, rule and_mask_less_size) apply (simp_all add: word_size) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p 6; 8 \<le> bits; bits < 32; LENGTH('a) = bits - 2\<rbrakk> \<Longrightarrow> (\<lambda>x. UCAST(32 \<rightarrow> 'a) (x + p && mask bits >> 2)) ` set [0 , 4 .e. 0x3C] = {x. x && ~~ mask 4 = UCAST(32 \<rightarrow> 'a) (p && mask bits >> 2)} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p 6; 8 \<le> bits; bits < 32; LENGTH('a) = bits - 2\<rbrakk> \<Longrightarrow> (\<lambda>x. UCAST(32 \<rightarrow> 'a) ((x << 2) + p && mask bits >> 2)) ` {x. x \<le> 0xF} = {x. x && ~~ mask 4 = UCAST(32 \<rightarrow> 'a) (p && mask bits >> 2)} proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned p 6; 8 \<le> bits; bits < 32; LENGTH('a) = bits - 2\<rbrakk> \<Longrightarrow> {x. x \<le> 0xF} = {x. x < 2 ^ 4}
 2. \<And>x. \<lbrakk>is_aligned p 6; 8 \<le> bits; bits < 32; LENGTH('a) = bits - 2; x \<in> {x. x < 2 ^ 4}\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 'a) ((x << 2) + p && mask bits >> 2) = ?g36 x
 3. \<lbrakk>is_aligned p 6; 8 \<le> bits; bits < 32; LENGTH('a) = bits - 2\<rbrakk> \<Longrightarrow> ?g36 ` {x. x < 2 ^ 4} = {x. x && ~~ mask 4 = UCAST(32 \<rightarrow> 'a) (p && mask bits >> 2)} proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>is_aligned p 6; 8 \<le> bits; bits < 32; LENGTH('a) = bits - 2; x \<le> 0xF\<rbrakk> \<Longrightarrow> x < 0x10
 2. \<And>x. \<lbrakk>is_aligned p 6; 8 \<le> bits; bits < 32; LENGTH('a) = bits - 2; x < 0x10\<rbrakk> \<Longrightarrow> x \<le> 0xF
 3. \<And>x. \<lbrakk>is_aligned p 6; 8 \<le> bits; bits < 32; LENGTH('a) = bits - 2; x \<in> {x. x < 2 ^ 4}\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 'a) ((x << 2) + p && mask bits >> 2) = ?g36 x
 4. \<lbrakk>is_aligned p 6; 8 \<le> bits; bits < 32; LENGTH('a) = bits - 2\<rbrakk> \<Longrightarrow> ?g36 ` {x. x < 2 ^ 4} = {x. x && ~~ mask 4 = UCAST(32 \<rightarrow> 'a) (p && mask bits >> 2)} proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>is_aligned p 6; 8 \<le> bits; bits < 32; LENGTH('a) = bits - 2; x < 0x10\<rbrakk> \<Longrightarrow> x \<le> 0xF
 2. \<And>x. \<lbrakk>is_aligned p 6; 8 \<le> bits; bits < 32; LENGTH('a) = bits - 2; x \<in> {x. x < 2 ^ 4}\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 'a) ((x << 2) + p && mask bits >> 2) = ?g36 x
 3. \<lbrakk>is_aligned p 6; 8 \<le> bits; bits < 32; LENGTH('a) = bits - 2\<rbrakk> \<Longrightarrow> ?g36 ` {x. x < 2 ^ 4} = {x. x && ~~ mask 4 = UCAST(32 \<rightarrow> 'a) (p && mask bits >> 2)} proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>is_aligned p 6; 8 \<le> bits; bits < 32; LENGTH('a) = bits - 2; x \<in> {x. x < 2 ^ 4}\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 'a) ((x << 2) + p && mask bits >> 2) = ?g36 x
 2. \<lbrakk>is_aligned p 6; 8 \<le> bits; bits < 32; LENGTH('a) = bits - 2\<rbrakk> \<Longrightarrow> ?g36 ` {x. x < 2 ^ 4} = {x. x && ~~ mask 4 = UCAST(32 \<rightarrow> 'a) (p && mask bits >> 2)} proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>is_aligned p 6; 8 \<le> bits; bits < 32; LENGTH('a) = bits - 2; x \<in> {x. x < 2 ^ 4}\<rbrakk> \<Longrightarrow> (x << 2) + p = ?y55 x
 2. \<lbrakk>is_aligned p 6; 8 \<le> bits; bits < 32; LENGTH('a) = bits - 2\<rbrakk> \<Longrightarrow> (\<lambda>x. UCAST(32 \<rightarrow> 'a) (?y55 x && mask bits >> 2)) ` {x. x < 2 ^ 4} = {x. x && ~~ mask 4 = UCAST(32 \<rightarrow> 'a) (p && mask bits >> 2)} proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>is_aligned p 6; 8 \<le> bits; bits < 32; LENGTH('a) = bits - 2; x \<in> {x. x < 2 ^ 4}\<rbrakk> \<Longrightarrow> x << 2 < 2 ^ 6
 2. \<lbrakk>is_aligned p 6; 8 \<le> bits; bits < 32; LENGTH('a) = bits - 2\<rbrakk> \<Longrightarrow> (\<lambda>x. UCAST(32 \<rightarrow> 'a) ((p || (x << 2)) && mask bits >> 2)) ` {x. x < 2 ^ 4} = {x. x && ~~ mask 4 = UCAST(32 \<rightarrow> 'a) (p && mask bits >> 2)} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p 6; 8 \<le> bits; bits < 32; LENGTH('a) = bits - 2\<rbrakk> \<Longrightarrow> (\<lambda>x. UCAST(32 \<rightarrow> 'a) ((p || (x << 2)) && mask bits >> 2)) ` {x. x < 2 ^ 4} = {x. x && ~~ mask 4 = UCAST(32 \<rightarrow> 'a) (p && mask bits >> 2)} proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>is_aligned p 6; 8 \<le> bits; bits < 32; LENGTH('a) = bits - 2; xa < 2 ^ 4\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 'a) ((p || (xa << 2)) && mask bits >> 2) && ~~ mask 4 = UCAST(32 \<rightarrow> 'a) (p && mask bits >> 2)
 2. \<And>x. \<lbrakk>is_aligned p 6; 8 \<le> bits; bits < 32; LENGTH('a) = bits - 2; x && ~~ mask 4 = UCAST(32 \<rightarrow> 'a) (p && mask bits >> 2)\<rbrakk> \<Longrightarrow> x \<in> (\<lambda>x. UCAST(32 \<rightarrow> 'a) ((p || (x << 2)) && mask bits >> 2)) ` {x. x < 2 ^ 4} proof (prove)
goal (3 subgoals):
 1. \<And>x xa. \<lbrakk>is_aligned p 6; 8 \<le> bits; bits < 32; LENGTH('a) = bits - 2; xa < 2 ^ 4\<rbrakk> \<Longrightarrow> 4 < word_bits
 2. \<And>x xa. \<lbrakk>is_aligned p 6; 8 \<le> bits; bits < 32; LENGTH('a) = bits - 2; xa < 2 ^ 4; \<forall>n'\<ge>4. n' < word_bits \<longrightarrow> \<not> xa !! n'\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 'a) ((p || (xa << 2)) && mask bits >> 2) && ~~ mask 4 = UCAST(32 \<rightarrow> 'a) (p && mask bits >> 2)
 3. \<And>x. \<lbrakk>is_aligned p 6; 8 \<le> bits; bits < 32; LENGTH('a) = bits - 2; x && ~~ mask 4 = UCAST(32 \<rightarrow> 'a) (p && mask bits >> 2)\<rbrakk> \<Longrightarrow> x \<in> (\<lambda>x. UCAST(32 \<rightarrow> 'a) ((p || (x << 2)) && mask bits >> 2)) ` {x. x < 2 ^ 4} proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrakk>is_aligned p 6; 8 \<le> bits; bits < 32; LENGTH('a) = bits - 2; xa < 2 ^ 4; \<forall>n'\<ge>4. n' < word_bits \<longrightarrow> \<not> xa !! n'\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 'a) ((p || (xa << 2)) && mask bits >> 2) && ~~ mask 4 = UCAST(32 \<rightarrow> 'a) (p && mask bits >> 2)
 2. \<And>x. \<lbrakk>is_aligned p 6; 8 \<le> bits; bits < 32; LENGTH('a) = bits - 2; x && ~~ mask 4 = UCAST(32 \<rightarrow> 'a) (p && mask bits >> 2)\<rbrakk> \<Longrightarrow> x \<in> (\<lambda>x. UCAST(32 \<rightarrow> 'a) ((p || (x << 2)) && mask bits >> 2)) ` {x. x < 2 ^ 4} proof (prove)
goal (2 subgoals):
 1. \<And>x xa n. \<lbrakk>is_aligned p 6; 8 \<le> bits; bits < 32; LENGTH('a) = bits - 2; xa < 2 ^ 4; \<forall>n'\<ge>4. n' < word_bits \<longrightarrow> \<not> xa !! n'\<rbrakk> \<Longrightarrow> n < size (UCAST(32 \<rightarrow> 'a) ((p || (xa << 2)) && mask bits >> 2) && ~~ mask 4) \<longrightarrow> (UCAST(32 \<rightarrow> 'a) ((p || (xa << 2)) && mask bits >> 2) && ~~ mask 4) !! n = UCAST(32 \<rightarrow> 'a) (p && mask bits >> 2) !! n
 2. \<And>x. \<lbrakk>is_aligned p 6; 8 \<le> bits; bits < 32; LENGTH('a) = bits - 2; x && ~~ mask 4 = UCAST(32 \<rightarrow> 'a) (p && mask bits >> 2)\<rbrakk> \<Longrightarrow> x \<in> (\<lambda>x. UCAST(32 \<rightarrow> 'a) ((p || (x << 2)) && mask bits >> 2)) ` {x. x < 2 ^ 4} proof (prove)
goal (2 subgoals):
 1. \<And>xa n. \<lbrakk>is_aligned p 6; 8 \<le> bits; bits < 32; LENGTH('a) = bits - 2; xa < 0x10; \<forall>n'\<ge>4. n' < 32 \<longrightarrow> \<not> xa !! n'\<rbrakk> \<Longrightarrow> n < bits - 2 \<longrightarrow> ((p !! Suc (Suc n) \<or> n < 30 \<and> xa !! n) \<and> Suc (Suc n) < bits \<and> \<not> n < 4) = (p !! Suc (Suc n) \<and> Suc (Suc n) < bits)
 2. \<And>x. \<lbrakk>is_aligned p 6; 8 \<le> bits; bits < 32; LENGTH('a) = bits - 2; x && ~~ mask 4 = UCAST(32 \<rightarrow> 'a) (p && mask bits >> 2)\<rbrakk> \<Longrightarrow> x \<in> (\<lambda>x. UCAST(32 \<rightarrow> 'a) ((p || (x << 2)) && mask bits >> 2)) ` {x. x < 2 ^ 4} proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_aligned p 6; 8 \<le> bits; bits < 32; LENGTH('a) = bits - 2; x && ~~ mask 4 = UCAST(32 \<rightarrow> 'a) (p && mask bits >> 2)\<rbrakk> \<Longrightarrow> x \<in> (\<lambda>x. UCAST(32 \<rightarrow> 'a) ((p || (x << 2)) && mask bits >> 2)) ` {x. x < 2 ^ 4} proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>is_aligned p 6; 8 \<le> bits; bits < 32; LENGTH('a) = bits - 2; x && ~~ mask 4 = UCAST(32 \<rightarrow> 'a) (p && mask bits >> 2)\<rbrakk> \<Longrightarrow> x = UCAST(32 \<rightarrow> 'a) ((p || (UCAST('a \<rightarrow> 32) x && mask 4 << 2)) && mask bits >> 2)
 2. \<And>x. \<lbrakk>is_aligned p 6; 8 \<le> bits; bits < 32; LENGTH('a) = bits - 2; x && ~~ mask 4 = UCAST(32 \<rightarrow> 'a) (p && mask bits >> 2)\<rbrakk> \<Longrightarrow> UCAST('a \<rightarrow> 32) x && mask 4 \<in> {x. x < 2 ^ 4} proof (prove)
goal (2 subgoals):
 1. \<And>x n. \<lbrakk>is_aligned p 6; 8 \<le> bits; bits < 32; LENGTH('a) = bits - 2; x && ~~ mask 4 = UCAST(32 \<rightarrow> 'a) (p && mask bits >> 2); n < size x\<rbrakk> \<Longrightarrow> x !! n = UCAST(32 \<rightarrow> 'a) ((p || (UCAST('a \<rightarrow> 32) x && mask 4 << 2)) && mask bits >> 2) !! n
 2. \<And>x. \<lbrakk>is_aligned p 6; 8 \<le> bits; bits < 32; LENGTH('a) = bits - 2; x && ~~ mask 4 = UCAST(32 \<rightarrow> 'a) (p && mask bits >> 2)\<rbrakk> \<Longrightarrow> UCAST('a \<rightarrow> 32) x && mask 4 \<in> {x. x < 2 ^ 4} proof (prove)
goal (2 subgoals):
 1. \<And>x n. \<lbrakk>is_aligned p 6; 8 \<le> bits; bits < 32; LENGTH('a) = bits - 2; n < size x; (x && ~~ mask 4) !! n = UCAST(32 \<rightarrow> 'a) (p && mask bits >> 2) !! n\<rbrakk> \<Longrightarrow> x !! n = UCAST(32 \<rightarrow> 'a) ((p || (UCAST('a \<rightarrow> 32) x && mask 4 << 2)) && mask bits >> 2) !! n
 2. \<And>x. \<lbrakk>is_aligned p 6; 8 \<le> bits; bits < 32; LENGTH('a) = bits - 2; x && ~~ mask 4 = UCAST(32 \<rightarrow> 'a) (p && mask bits >> 2)\<rbrakk> \<Longrightarrow> UCAST('a \<rightarrow> 32) x && mask 4 \<in> {x. x < 2 ^ 4} proof (prove)
goal (2 subgoals):
 1. \<And>x n. \<lbrakk>is_aligned p 6; 8 \<le> bits; bits < 32; LENGTH('a) = bits - 2; n < bits - 2; (x !! n \<and> \<not> n < 4) = (p !! Suc (Suc n) \<and> Suc (Suc n) < bits)\<rbrakk> \<Longrightarrow> x !! n = ((p !! Suc (Suc n) \<or> n < 30 \<and> n < 32 \<and> x !! n \<and> n < 4) \<and> Suc (Suc n) < bits)
 2. \<And>x. \<lbrakk>is_aligned p 6; 8 \<le> bits; bits < 32; LENGTH('a) = bits - 2; x && ~~ mask 4 = UCAST(32 \<rightarrow> 'a) (p && mask bits >> 2)\<rbrakk> \<Longrightarrow> UCAST('a \<rightarrow> 32) x && mask 4 \<in> {x. x < 2 ^ 4} proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>is_aligned p 6; 8 \<le> bits; bits < 32; LENGTH('a) = bits - 2; x && ~~ mask 4 = UCAST(32 \<rightarrow> 'a) (p && mask bits >> 2)\<rbrakk> \<Longrightarrow> UCAST('a \<rightarrow> 32) x && mask 4 < 0x10 proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>is_aligned p 6; 8 \<le> bits; bits < 32; LENGTH('a) = bits - 2; x && ~~ mask 4 = UCAST(32 \<rightarrow> 'a) (p && mask bits >> 2)\<rbrakk> \<Longrightarrow> 4 < size (UCAST('a \<rightarrow> 32) x)
 2. \<And>x. \<lbrakk>is_aligned p 6; 8 \<le> bits; bits < 32; LENGTH('a) = bits - 2; x && ~~ mask 4 = UCAST(32 \<rightarrow> 'a) (p && mask bits >> 2)\<rbrakk> \<Longrightarrow> 2 ^ 4 \<le> 0x10 proof (prove)
goal:
No subgoals!