theory ArchAcc_AI

lemma vptr_shifting_helper_magic:
  "(x = 0) \<or> (x < 2 ^ 4 \<and> vmsz_aligned (vptr::word32) ARMSuperSection)
   \<Longrightarrow> (x << 2) + (vptr >> 20 << 2) = ((vptr + (x << 20)) >> 20 << 2)" apply (erule disjE, simp_all) apply (clarsimp simp: vmsz_aligned_def) apply (subst is_aligned_add_or, assumption) apply (rule shiftl_less_t2n) apply simp apply simp apply (simp add: shiftl_over_or_dist shiftr_over_or_dist) apply (subst shiftl_shiftr_id) apply (simp add: word_bits_def) apply (simp add: word_bits_def) apply unat_arith apply (subst field_simps, rule is_aligned_add_or[where n=6]) apply (intro is_aligned_shiftl is_aligned_shiftr) apply simp apply (rule shiftl_less_t2n, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x = 0 \<or> x < 2 ^ 4 \<and> vmsz_aligned vptr ARMSuperSection \<Longrightarrow> (x << 2) + (vptr >> 20 << 2) = vptr + (x << 20) >> 20 << 2 proof (prove)
goal (1 subgoal):
 1. x < 0x10 \<and> vmsz_aligned vptr ARMSuperSection \<Longrightarrow> (x << 2) + (vptr >> 20 << 2) = vptr + (x << 20) >> 20 << 2 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < 0x10; is_aligned vptr 24\<rbrakk> \<Longrightarrow> (x << 2) + (vptr >> 20 << 2) = vptr + (x << 20) >> 20 << 2 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x < 0x10; is_aligned vptr 24\<rbrakk> \<Longrightarrow> x << 20 < 2 ^ 24
 2. \<lbrakk>x < 0x10; is_aligned vptr 24\<rbrakk> \<Longrightarrow> (x << 2) + (vptr >> 20 << 2) = vptr || (x << 20) >> 20 << 2 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>x < 0x10; is_aligned vptr 24\<rbrakk> \<Longrightarrow> x < 2 ^ (24 - 20)
 2. \<lbrakk>x < 0x10; is_aligned vptr 24\<rbrakk> \<Longrightarrow> 24 < LENGTH(32)
 3. \<lbrakk>x < 0x10; is_aligned vptr 24\<rbrakk> \<Longrightarrow> (x << 2) + (vptr >> 20 << 2) = vptr || (x << 20) >> 20 << 2 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x < 0x10; is_aligned vptr 24\<rbrakk> \<Longrightarrow> 24 < LENGTH(32)
 2. \<lbrakk>x < 0x10; is_aligned vptr 24\<rbrakk> \<Longrightarrow> (x << 2) + (vptr >> 20 << 2) = vptr || (x << 20) >> 20 << 2 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < 0x10; is_aligned vptr 24\<rbrakk> \<Longrightarrow> (x << 2) + (vptr >> 20 << 2) = vptr || (x << 20) >> 20 << 2 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < 0x10; is_aligned vptr 24\<rbrakk> \<Longrightarrow> (x << 2) + (vptr >> 20 << 2) = (vptr >> 20 << 2) || (x << 20 >> 20 << 2) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>x < 0x10; is_aligned vptr 24\<rbrakk> \<Longrightarrow> 20 < LENGTH(32)
 2. \<lbrakk>x < 0x10; is_aligned vptr 24\<rbrakk> \<Longrightarrow> x < 2 ^ (LENGTH(32) - 20)
 3. \<lbrakk>x < 0x10; is_aligned vptr 24\<rbrakk> \<Longrightarrow> (x << 2) + (vptr >> 20 << 2) = (vptr >> 20 << 2) || (x << 2) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x < 0x10; is_aligned vptr 24\<rbrakk> \<Longrightarrow> x < 2 ^ (LENGTH(32) - 20)
 2. \<lbrakk>x < 0x10; is_aligned vptr 24\<rbrakk> \<Longrightarrow> (x << 2) + (vptr >> 20 << 2) = (vptr >> 20 << 2) || (x << 2) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x < 0x10; is_aligned vptr 24\<rbrakk> \<Longrightarrow> x < 0x1000
 2. \<lbrakk>x < 0x10; is_aligned vptr 24\<rbrakk> \<Longrightarrow> (x << 2) + (vptr >> 20 << 2) = (vptr >> 20 << 2) || (x << 2) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < 0x10; is_aligned vptr 24\<rbrakk> \<Longrightarrow> (x << 2) + (vptr >> 20 << 2) = (vptr >> 20 << 2) || (x << 2) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x < 0x10; is_aligned vptr 24\<rbrakk> \<Longrightarrow> is_aligned (vptr >> 20 << 2) 6
 2. \<lbrakk>x < 0x10; is_aligned vptr 24\<rbrakk> \<Longrightarrow> x << 2 < 2 ^ 6 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x < 0x10; is_aligned vptr 24\<rbrakk> \<Longrightarrow> is_aligned vptr (6 - 2 + 20)
 2. \<lbrakk>x < 0x10; is_aligned vptr 24\<rbrakk> \<Longrightarrow> x << 2 < 2 ^ 6 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < 0x10; is_aligned vptr 24\<rbrakk> \<Longrightarrow> x << 2 < 2 ^ 6 proof (prove)
goal:
No subgoals!