theory ArchVSpace_AI

lemma ex_asid_high_bits_plus:
  "asid \<le> mask asid_bits \<Longrightarrow> \<exists>x \<le> 2^asid_low_bits - 1. asid = (ucast (asid_high_bits_of asid) << asid_low_bits) + x" apply (rule_tac x="asid && mask asid_low_bits" in exI) apply (rule conjI) apply (simp add: mask_def) apply (rule word_and_le1) apply (subst (asm) mask_def) apply (simp add: upper_bits_unset_is_l2p_32 [symmetric]) apply (subst word_plus_and_or_coroll; word_eqI) apply (clarsimp simp: asid_high_bits_of_def asid_low_bits_def word_bits_def asid_bits_def) apply (rule iffI) prefer 2 apply fastforce apply (clarsimp simp: linorder_not_less) by (metis add_One_commute add_diff_inverse_nat le_add1 less_diff_conv2 less_imp_diff_less
            numeral_plus_numeral semiring_norm(10) semiring_norm(2) semiring_norm(3)
            semiring_norm(4) semiring_norm(9))

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. asid \<le> mask local.asid_bits \<Longrightarrow> \<exists>x\<le>2 ^ local.asid_low_bits - 1. asid = (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) << local.asid_low_bits) + x proof (prove)
goal (1 subgoal):
 1. asid \<le> mask local.asid_bits \<Longrightarrow> asid && mask local.asid_low_bits \<le> 2 ^ local.asid_low_bits - 1 \<and> asid = (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) << local.asid_low_bits) + (asid && mask local.asid_low_bits) proof (prove)
goal (2 subgoals):
 1. asid \<le> mask local.asid_bits \<Longrightarrow> asid && mask local.asid_low_bits \<le> 2 ^ local.asid_low_bits - 1
 2. asid \<le> mask local.asid_bits \<Longrightarrow> asid = (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) << local.asid_low_bits) + (asid && mask local.asid_low_bits) proof (prove)
goal (2 subgoals):
 1. asid < 2 ^ local.asid_bits \<Longrightarrow> asid && 2 ^ local.asid_low_bits - 1 \<le> 2 ^ local.asid_low_bits - 1
 2. asid \<le> mask local.asid_bits \<Longrightarrow> asid = (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) << local.asid_low_bits) + (asid && mask local.asid_low_bits) proof (prove)
goal (1 subgoal):
 1. asid \<le> mask local.asid_bits \<Longrightarrow> asid = (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) << local.asid_low_bits) + (asid && mask local.asid_low_bits) proof (prove)
goal (1 subgoal):
 1. asid \<le> (1 << local.asid_bits) - 1 \<Longrightarrow> asid = (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) << local.asid_low_bits) + (asid && mask local.asid_low_bits) proof (prove)
goal (1 subgoal):
 1. \<forall>n'\<ge>local.asid_bits. n' < word_bits \<longrightarrow> \<not> asid !! n' \<Longrightarrow> asid = (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid) << local.asid_low_bits) + (asid && mask local.asid_low_bits) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>n'\<ge>local.asid_bits. n' < word_bits \<longrightarrow> \<not> asid !! n'; n < 32\<rbrakk> \<Longrightarrow> asid !! n = (local.asid_low_bits \<le> n \<and> n - local.asid_low_bits < 32 \<and> asid_high_bits_of asid !! (n - local.asid_low_bits) \<or> asid !! n \<and> n < local.asid_low_bits) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>n'\<ge>17. n' < 32 \<longrightarrow> \<not> asid !! n'; n < 32\<rbrakk> \<Longrightarrow> asid !! n = (10 \<le> n \<and> n - 10 < 32 \<and> n - 10 < 7 \<and> asid !! (10 + (n - 10)) \<or> asid !! n \<and> n < 10) proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>\<forall>n'\<ge>17. n' < 32 \<longrightarrow> \<not> asid !! n'; n < 32; asid !! n\<rbrakk> \<Longrightarrow> 10 \<le> n \<and> n - 10 < 32 \<and> n - 10 < 7 \<and> asid !! (10 + (n - 10)) \<or> asid !! n \<and> n < 10
 2. \<And>n. \<lbrakk>\<forall>n'\<ge>17. n' < 32 \<longrightarrow> \<not> asid !! n'; n < 32; 10 \<le> n \<and> n - 10 < 32 \<and> n - 10 < 7 \<and> asid !! (10 + (n - 10)) \<or> asid !! n \<and> n < 10\<rbrakk> \<Longrightarrow> asid !! n proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>\<forall>n'\<ge>17. n' < 32 \<longrightarrow> \<not> asid !! n'; n < 32; 10 \<le> n \<and> n - 10 < 32 \<and> n - 10 < 7 \<and> asid !! (10 + (n - 10)) \<or> asid !! n \<and> n < 10\<rbrakk> \<Longrightarrow> asid !! n
 2. \<And>n. \<lbrakk>\<forall>n'\<ge>17. n' < 32 \<longrightarrow> \<not> asid !! n'; n < 32; asid !! n\<rbrakk> \<Longrightarrow> 10 \<le> n \<and> n - 10 < 32 \<and> n - 10 < 7 \<and> asid !! (10 + (n - 10)) \<or> asid !! n \<and> n < 10 proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>n'\<ge>17. n' < 32 \<longrightarrow> \<not> asid !! n'; n < 32; asid !! n\<rbrakk> \<Longrightarrow> 10 \<le> n \<and> n - 10 < 32 \<and> n - 10 < 7 \<and> asid !! (10 + (n - 10)) \<or> asid !! n \<and> n < 10 proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<forall>n'\<ge>17. n' < 32 \<longrightarrow> \<not> asid !! n'; n < 32; asid !! n; 10 \<le> n\<rbrakk> \<Longrightarrow> n - 10 < 32 \<and> n - 10 < 7