theory ADT_H

lemma unaligned_page_offsets_helper:
  "\<lbrakk>is_aligned y (pageBitsForSize vmpage_size); n\<noteq>0;
    n < 2 ^ (pageBitsForSize vmpage_size - pageBits)\<rbrakk>
   \<Longrightarrow> \<not> is_aligned (y + n * 2 ^ pageBits :: word32) (pageBitsForSize vmpage_size)" apply (simp (no_asm_simp) add: is_aligned_mask) apply (simp add: mask_add_aligned) apply (cut_tac mask_eq_iff_w2p [of "pageBitsForSize vmpage_size" "n * 2 ^ pageBits"]) prefer 2 apply (case_tac vmpage_size, simp_all add: pageBits_def word_size) apply (cut_tac word_power_nonzero_32[of n pageBits];
         simp add: word_bits_conv pageBits_def) prefer 2 apply (case_tac vmpage_size, simp_all add: pageBits_def word_size) apply (frule less_trans[of n _ "0x100000"], simp+)+ apply clarsimp apply (case_tac vmpage_size, simp_all add: pageBits_def) apply (frule_tac i=n and k="0x1000" in word_mult_less_mono1, simp+)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned y (pageBitsForSize vmpage_size); n \<noteq> 0; n < 2 ^ (pageBitsForSize vmpage_size - pageBits)\<rbrakk> \<Longrightarrow> \<not> is_aligned (y + n * 2 ^ pageBits) (pageBitsForSize vmpage_size) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned y (pageBitsForSize vmpage_size); n \<noteq> 0; n < 2 ^ (pageBitsForSize vmpage_size - pageBits)\<rbrakk> \<Longrightarrow> y + n * 2 ^ pageBits && mask (pageBitsForSize vmpage_size) \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned y (pageBitsForSize vmpage_size); n \<noteq> 0; n < 2 ^ (pageBitsForSize vmpage_size - pageBits)\<rbrakk> \<Longrightarrow> n * 2 ^ pageBits && mask (pageBitsForSize vmpage_size) \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned y (pageBitsForSize vmpage_size); n \<noteq> 0; n < 2 ^ (pageBitsForSize vmpage_size - pageBits); (n * 2 ^ pageBits && mask (pageBitsForSize vmpage_size) = n * 2 ^ pageBits) = (n * 2 ^ pageBits < 2 ^ pageBitsForSize vmpage_size)\<rbrakk> \<Longrightarrow> n * 2 ^ pageBits && mask (pageBitsForSize vmpage_size) \<noteq> 0
 2. \<lbrakk>is_aligned y (pageBitsForSize vmpage_size); n \<noteq> 0; n < 2 ^ (pageBitsForSize vmpage_size - pageBits)\<rbrakk> \<Longrightarrow> pageBitsForSize vmpage_size < size (n * 2 ^ pageBits) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned y (pageBitsForSize vmpage_size); n \<noteq> 0; n < 2 ^ (pageBitsForSize vmpage_size - pageBits)\<rbrakk> \<Longrightarrow> pageBitsForSize vmpage_size < size (n * 2 ^ pageBits)
 2. \<lbrakk>is_aligned y (pageBitsForSize vmpage_size); n \<noteq> 0; n < 2 ^ (pageBitsForSize vmpage_size - pageBits); (n * 2 ^ pageBits && mask (pageBitsForSize vmpage_size) = n * 2 ^ pageBits) = (n * 2 ^ pageBits < 2 ^ pageBitsForSize vmpage_size)\<rbrakk> \<Longrightarrow> n * 2 ^ pageBits && mask (pageBitsForSize vmpage_size) \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned y (pageBitsForSize vmpage_size); n \<noteq> 0; n < 2 ^ (pageBitsForSize vmpage_size - 12); (n * 0x1000 && mask (pageBitsForSize vmpage_size) = n * 0x1000) = (n * 0x1000 < 2 ^ pageBitsForSize vmpage_size)\<rbrakk> \<Longrightarrow> n * 0x1000 && mask (pageBitsForSize vmpage_size) \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned y (pageBitsForSize vmpage_size); n \<noteq> 0; n < 2 ^ (pageBitsForSize vmpage_size - 12); (n * 0x1000 && mask (pageBitsForSize vmpage_size) = n * 0x1000) = (n * 0x1000 < 2 ^ pageBitsForSize vmpage_size); n * 0x1000 \<noteq> 0\<rbrakk> \<Longrightarrow> n * 0x1000 && mask (pageBitsForSize vmpage_size) \<noteq> 0
 2. \<lbrakk>is_aligned y (pageBitsForSize vmpage_size); n \<noteq> 0; n < 2 ^ (pageBitsForSize vmpage_size - 12); (n * 0x1000 && mask (pageBitsForSize vmpage_size) = n * 0x1000) = (n * 0x1000 < 2 ^ pageBitsForSize vmpage_size)\<rbrakk> \<Longrightarrow> n < 0x100000 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned y (pageBitsForSize vmpage_size); n \<noteq> 0; n < 2 ^ (pageBitsForSize vmpage_size - 12); (n * 0x1000 && mask (pageBitsForSize vmpage_size) = n * 0x1000) = (n * 0x1000 < 2 ^ pageBitsForSize vmpage_size)\<rbrakk> \<Longrightarrow> n < 0x100000
 2. \<lbrakk>is_aligned y (pageBitsForSize vmpage_size); n \<noteq> 0; n < 2 ^ (pageBitsForSize vmpage_size - 12); (n * 0x1000 && mask (pageBitsForSize vmpage_size) = n * 0x1000) = (n * 0x1000 < 2 ^ pageBitsForSize vmpage_size); n * 0x1000 \<noteq> 0\<rbrakk> \<Longrightarrow> n * 0x1000 && mask (pageBitsForSize vmpage_size) \<noteq> 0 proof (prove)
goal (4 subgoals):
 1. \<lbrakk>is_aligned y 16; n \<noteq> 0; n < 0x10; (n * 0x1000 && mask 16 = n * 0x1000) = (n * 0x1000 < 0x10000); vmpage_size = ARMLargePage\<rbrakk> \<Longrightarrow> n < 0x100000
 2. \<lbrakk>is_aligned y 20; n \<noteq> 0; n < 0x100; (n * 0x1000 && mask 20 = n * 0x1000) = (n * 0x1000 < 0x100000); vmpage_size = ARMSection\<rbrakk> \<Longrightarrow> n < 0x100000
 3. \<lbrakk>is_aligned y 24; n \<noteq> 0; n < 0x1000; (n * 0x1000 && mask 24 = n * 0x1000) = (n * 0x1000 < 0x1000000); vmpage_size = ARMSuperSection\<rbrakk> \<Longrightarrow> n < 0x100000
 4. \<lbrakk>is_aligned y (pageBitsForSize vmpage_size); n \<noteq> 0; n < 2 ^ (pageBitsForSize vmpage_size - 12); (n * 0x1000 && mask (pageBitsForSize vmpage_size) = n * 0x1000) = (n * 0x1000 < 2 ^ pageBitsForSize vmpage_size); n * 0x1000 \<noteq> 0\<rbrakk> \<Longrightarrow> n * 0x1000 && mask (pageBitsForSize vmpage_size) \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned y (pageBitsForSize vmpage_size); n \<noteq> 0; n < 2 ^ (pageBitsForSize vmpage_size - 12); (n * 0x1000 && mask (pageBitsForSize vmpage_size) = n * 0x1000) = (n * 0x1000 < 2 ^ pageBitsForSize vmpage_size); n * 0x1000 \<noteq> 0\<rbrakk> \<Longrightarrow> n * 0x1000 && mask (pageBitsForSize vmpage_size) \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned y (pageBitsForSize vmpage_size); n \<noteq> 0; n < 2 ^ (pageBitsForSize vmpage_size - 12); \<not> n * 0x1000 < 2 ^ pageBitsForSize vmpage_size; n * 0x1000 \<noteq> 0; n * 0x1000 && mask (pageBitsForSize vmpage_size) = 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned y 16; n \<noteq> 0; n < 0x10; \<not> n * 0x1000 < 0x10000; n * 0x1000 \<noteq> 0; n * 0x1000 && mask 16 = 0; vmpage_size = ARMLargePage\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>is_aligned y 20; n \<noteq> 0; n < 0x100; \<not> n * 0x1000 < 0x100000; n * 0x1000 \<noteq> 0; n * 0x1000 && mask 20 = 0; vmpage_size = ARMSection\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>is_aligned y 24; n \<noteq> 0; n < 0x1000; \<not> n * 0x1000 < 0x1000000; n * 0x1000 \<noteq> 0; n * 0x1000 && mask 24 = 0; vmpage_size = ARMSuperSection\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!