theory ArchArch_AI

lemma shiftr_irrelevant:
  "x < 2 ^ asid_low_bits \<Longrightarrow> is_aligned (y :: word32) asid_low_bits \<Longrightarrow>
    x + y >> asid_low_bits = y >> asid_low_bits" apply (subst word_plus_and_or_coroll) apply (rule word_eqI) apply (clarsimp simp: is_aligned_nth) apply (drule(1) nth_bounded) apply (simp add: asid_low_bits_def word_bits_def) apply simp apply (rule word_eqI) apply (simp add: nth_shiftr) apply safe apply (drule(1) nth_bounded) apply (simp add: asid_low_bits_def word_bits_def) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < 2 ^ local.asid_low_bits; is_aligned y local.asid_low_bits\<rbrakk> \<Longrightarrow> x + y >> local.asid_low_bits = y >> local.asid_low_bits proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x < 2 ^ local.asid_low_bits; is_aligned y local.asid_low_bits\<rbrakk> \<Longrightarrow> x && y = 0
 2. \<lbrakk>x < 2 ^ local.asid_low_bits; is_aligned y local.asid_low_bits\<rbrakk> \<Longrightarrow> x || y >> local.asid_low_bits = y >> local.asid_low_bits proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>x < 2 ^ local.asid_low_bits; is_aligned y local.asid_low_bits\<rbrakk> \<Longrightarrow> n < size (x && y) \<longrightarrow> (x && y) !! n = 0 !! n
 2. \<lbrakk>x < 2 ^ local.asid_low_bits; is_aligned y local.asid_low_bits\<rbrakk> \<Longrightarrow> x || y >> local.asid_low_bits = y >> local.asid_low_bits proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>x < 2 ^ local.asid_low_bits; \<forall>n<local.asid_low_bits. \<not> y !! n; n < size (x && y); x !! n; y !! n\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>x < 2 ^ local.asid_low_bits; is_aligned y local.asid_low_bits\<rbrakk> \<Longrightarrow> x || y >> local.asid_low_bits = y >> local.asid_low_bits proof (prove)
goal (3 subgoals):
 1. \<And>n. \<lbrakk>x < 2 ^ local.asid_low_bits; \<forall>n<local.asid_low_bits. \<not> y !! n; n < size (x && y); y !! n\<rbrakk> \<Longrightarrow> local.asid_low_bits \<le> LENGTH(32)
 2. \<And>n. \<lbrakk>x < 2 ^ local.asid_low_bits; \<forall>n<local.asid_low_bits. \<not> y !! n; n < size (x && y); y !! n; n < local.asid_low_bits\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>x < 2 ^ local.asid_low_bits; is_aligned y local.asid_low_bits\<rbrakk> \<Longrightarrow> x || y >> local.asid_low_bits = y >> local.asid_low_bits proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>x < 2 ^ local.asid_low_bits; \<forall>n<local.asid_low_bits. \<not> y !! n; n < size (x && y); y !! n; n < local.asid_low_bits\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>x < 2 ^ local.asid_low_bits; is_aligned y local.asid_low_bits\<rbrakk> \<Longrightarrow> x || y >> local.asid_low_bits = y >> local.asid_low_bits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < 2 ^ local.asid_low_bits; is_aligned y local.asid_low_bits\<rbrakk> \<Longrightarrow> x || y >> local.asid_low_bits = y >> local.asid_low_bits proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>x < 2 ^ local.asid_low_bits; is_aligned y local.asid_low_bits\<rbrakk> \<Longrightarrow> n < size (x || y >> local.asid_low_bits) \<longrightarrow> (x || y >> local.asid_low_bits) !! n = (y >> local.asid_low_bits) !! n proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>x < 2 ^ local.asid_low_bits; is_aligned y local.asid_low_bits\<rbrakk> \<Longrightarrow> n < size (x || y >> local.asid_low_bits) \<longrightarrow> (x !! (local.asid_low_bits + n) \<or> y !! (local.asid_low_bits + n)) = y !! (local.asid_low_bits + n) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>x < 2 ^ local.asid_low_bits; is_aligned y local.asid_low_bits; n < size (x || y >> local.asid_low_bits); x !! (local.asid_low_bits + n)\<rbrakk> \<Longrightarrow> y !! (local.asid_low_bits + n) proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>x < 2 ^ local.asid_low_bits; is_aligned y local.asid_low_bits; n < size (x || y >> local.asid_low_bits)\<rbrakk> \<Longrightarrow> local.asid_low_bits \<le> LENGTH(32)
 2. \<And>n. \<lbrakk>x < 2 ^ local.asid_low_bits; is_aligned y local.asid_low_bits; n < size (x || y >> local.asid_low_bits); local.asid_low_bits + n < local.asid_low_bits\<rbrakk> \<Longrightarrow> y !! (local.asid_low_bits + n) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>x < 2 ^ local.asid_low_bits; is_aligned y local.asid_low_bits; n < size (x || y >> local.asid_low_bits); local.asid_low_bits + n < local.asid_low_bits\<rbrakk> \<Longrightarrow> y !! (local.asid_low_bits + n) proof (prove)
goal:
No subgoals!