theory ArchVSpace_AI

lemma asid_low_high_bits:
  "\<lbrakk> x && mask asid_low_bits = y && mask asid_low_bits;
    ucast (asid_high_bits_of x) = (ucast (asid_high_bits_of y)::word32);
    x \<le> 2 ^ asid_bits - 1; y \<le> 2 ^ asid_bits - 1 \<rbrakk>
  \<Longrightarrow> x = y" apply (rule word_eqI) apply (simp add: upper_bits_unset_is_l2p_32 [symmetric] bang_eq nth_ucast word_size) apply (clarsimp simp: asid_high_bits_of_def nth_ucast nth_shiftr) apply (simp add: asid_high_bits_def asid_bits_def asid_low_bits_def word_bits_def) subgoal premises prems[rule_format] for n apply (cases "n < 10") using prems(1) apply fastforce apply (cases "n < 17") using prems(2)[where n="n - 10"] apply fastforce using prems(3-) by (simp add: linorder_not_less) done

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

goal (2 subgoals):
 1. n < 10 \<Longrightarrow> x !! n = y !! n
 2. \<not> n < 10 \<Longrightarrow> x !! n = y !! n proof (prove)
goal (1 subgoal):
 1. \<not> n < 10 \<Longrightarrow> x !! n = y !! n proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<not> n < 10; n < 17\<rbrakk> \<Longrightarrow> x !! n = y !! n
 2. \<lbrakk>\<not> n < 10; \<not> n < 17\<rbrakk> \<Longrightarrow> x !! n = y !! n proof (prove)
using this:
(n - 10 < 32 \<and> n - 10 < 7 \<and> x !! (10 + (n - 10))) = (n - 10 < 32 \<and> n - 10 < 7 \<and> y !! (10 + (n - 10)))

goal (2 subgoals):
 1. \<lbrakk>\<not> n < 10; n < 17\<rbrakk> \<Longrightarrow> x !! n = y !! n
 2. \<lbrakk>\<not> n < 10; \<not> n < 17\<rbrakk> \<Longrightarrow> x !! n = y !! n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> n < 10; \<not> n < 17\<rbrakk> \<Longrightarrow> x !! n = y !! n proof (prove)
using this:
\<lbrakk>17 \<le> ?n'; ?n' < 32\<rbrakk> \<Longrightarrow> \<not> x !! ?n'
\<lbrakk>17 \<le> ?n'; ?n' < 32\<rbrakk> \<Longrightarrow> \<not> y !! ?n'
n < 32

goal (1 subgoal):
 1. \<lbrakk>\<not> n < 10; \<not> n < 17\<rbrakk> \<Longrightarrow> x !! n = y !! n proof (prove)
goal:
No subgoals!