theory ArchLevityCatch_AI

lemma asid_high_bits_of_add:
  "\<lbrakk>is_aligned w asid_low_bits; x \<le> 2 ^ asid_low_bits - 1\<rbrakk>
   \<Longrightarrow> asid_high_bits_of (w + x) = asid_high_bits_of w" apply (rule word_eqI) apply (simp add: word_size asid_high_bits_of_def is_aligned_nth) apply (drule le2p_bits_unset_32, simp add: asid_low_bits_def) apply (subst word_plus_and_or_coroll) apply (rule word_eqI) apply (clarsimp simp: word_size) apply (case_tac "na < asid_low_bits") apply (simp add: asid_low_bits_def linorder_not_less word_bits_def) apply (auto dest: test_bit_size
              simp: asid_low_bits_def word_bits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned w local.asid_low_bits; x \<le> 2 ^ local.asid_low_bits - 1\<rbrakk> \<Longrightarrow> asid_high_bits_of (w + x) = asid_high_bits_of w proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>is_aligned w local.asid_low_bits; x \<le> 2 ^ local.asid_low_bits - 1\<rbrakk> \<Longrightarrow> n < size (asid_high_bits_of (w + x)) \<longrightarrow> asid_high_bits_of (w + x) !! n = asid_high_bits_of w !! n proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>n<local.asid_low_bits. \<not> w !! n; x \<le> 2 ^ local.asid_low_bits - 1\<rbrakk> \<Longrightarrow> n < 7 \<longrightarrow> (w + x) !! (local.asid_low_bits + n) = w !! (local.asid_low_bits + n) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>n<10. \<not> w !! n; \<forall>n'\<ge>10. n' < word_bits \<longrightarrow> \<not> x !! n'\<rbrakk> \<Longrightarrow> n < 7 \<longrightarrow> (w + x) !! (10 + n) = w !! (10 + n) proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>\<forall>n<10. \<not> w !! n; \<forall>n'\<ge>10. n' < word_bits \<longrightarrow> \<not> x !! n'\<rbrakk> \<Longrightarrow> w && x = 0
 2. \<And>n. \<lbrakk>\<forall>n<10. \<not> w !! n; \<forall>n'\<ge>10. n' < word_bits \<longrightarrow> \<not> x !! n'\<rbrakk> \<Longrightarrow> n < 7 \<longrightarrow> (w || x) !! (10 + n) = w !! (10 + n) proof (prove)
goal (2 subgoals):
 1. \<And>n na. \<lbrakk>\<forall>n<10. \<not> w !! n; \<forall>n'\<ge>10. n' < word_bits \<longrightarrow> \<not> x !! n'\<rbrakk> \<Longrightarrow> na < size (w && x) \<longrightarrow> (w && x) !! na = 0 !! na
 2. \<And>n. \<lbrakk>\<forall>n<10. \<not> w !! n; \<forall>n'\<ge>10. n' < word_bits \<longrightarrow> \<not> x !! n'\<rbrakk> \<Longrightarrow> n < 7 \<longrightarrow> (w || x) !! (10 + n) = w !! (10 + n) proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>\<forall>n<10. \<not> w !! n; \<forall>n'\<ge>10. n' < word_bits \<longrightarrow> \<not> x !! n'; na < 32; w !! na; x !! na\<rbrakk> \<Longrightarrow> False
 2. \<And>n. \<lbrakk>\<forall>n<10. \<not> w !! n; \<forall>n'\<ge>10. n' < word_bits \<longrightarrow> \<not> x !! n'\<rbrakk> \<Longrightarrow> n < 7 \<longrightarrow> (w || x) !! (10 + n) = w !! (10 + n) proof (prove)
goal (3 subgoals):
 1. \<And>na. \<lbrakk>\<forall>n<10. \<not> w !! n; \<forall>n'\<ge>10. n' < word_bits \<longrightarrow> \<not> x !! n'; na < 32; w !! na; x !! na; na < local.asid_low_bits\<rbrakk> \<Longrightarrow> False
 2. \<And>na. \<lbrakk>\<forall>n<10. \<not> w !! n; \<forall>n'\<ge>10. n' < word_bits \<longrightarrow> \<not> x !! n'; na < 32; w !! na; x !! na; \<not> na < local.asid_low_bits\<rbrakk> \<Longrightarrow> False
 3. \<And>n. \<lbrakk>\<forall>n<10. \<not> w !! n; \<forall>n'\<ge>10. n' < word_bits \<longrightarrow> \<not> x !! n'\<rbrakk> \<Longrightarrow> n < 7 \<longrightarrow> (w || x) !! (10 + n) = w !! (10 + n) proof (prove)
goal (2 subgoals):
 1. \<And>na. \<lbrakk>\<forall>n<10. \<not> w !! n; \<forall>n'\<ge>10. n' < word_bits \<longrightarrow> \<not> x !! n'; na < 32; w !! na; x !! na; \<not> na < local.asid_low_bits\<rbrakk> \<Longrightarrow> False
 2. \<And>n. \<lbrakk>\<forall>n<10. \<not> w !! n; \<forall>n'\<ge>10. n' < word_bits \<longrightarrow> \<not> x !! n'\<rbrakk> \<Longrightarrow> n < 7 \<longrightarrow> (w || x) !! (10 + n) = w !! (10 + n) proof (prove)
goal:
No subgoals!