theory ArchArch_AI

lemma dom_ucast_eq:
  "(- dom (\<lambda>a::asid_low_index. p (ucast a::machine_word)) \<inter> {x. ucast x + y \<noteq> 0} = {}) =
   (- dom p \<inter> {x. x \<le> 2 ^ asid_low_bits - 1 \<and> x + y \<noteq> 0} = {})" apply safe apply clarsimp apply (rule ccontr) apply (erule_tac x="ucast x" in in_emptyE) apply (clarsimp simp: p2_low_bits_max) apply (rule conjI) apply (clarsimp simp: ucast_ucast_mask) apply (subst (asm) less_mask_eq) apply (rule word_less_sub_le [THEN iffD1]) apply (simp add: word_bits_def) apply (simp add: asid_low_bits_def) apply simp apply (clarsimp simp: ucast_ucast_mask) apply (subst (asm) less_mask_eq) apply (rule word_less_sub_le [THEN iffD1]) apply (simp add: word_bits_def) apply (simp add: asid_low_bits_def) apply simp apply (clarsimp simp: p2_low_bits_max) apply (rule ccontr) apply simp apply (erule_tac x="ucast x" in in_emptyE) apply clarsimp apply (rule conjI, blast) apply (rule word_less_sub_1) apply (rule order_less_le_trans) apply (rule ucast_less, simp) apply (simp add: asid_low_bits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (- dom (\<lambda>a. p (UCAST(10 \<rightarrow> 32) a)) \<inter> {x. UCAST(10 \<rightarrow> 32) x + y \<noteq> 0} = {}) = (- dom p \<inter> {x. x \<le> 2 ^ local.asid_low_bits - 1 \<and> x + y \<noteq> 0} = {}) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>- dom (\<lambda>a. p (UCAST(10 \<rightarrow> 32) a)) \<inter> {x. UCAST(10 \<rightarrow> 32) x + y \<noteq> 0} = {}; x \<notin> {}; x \<le> 2 ^ local.asid_low_bits - 1; x + y \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>y. p x = Some y
 2. \<And>x. \<lbrakk>- dom p \<inter> {x. x \<le> 2 ^ local.asid_low_bits - 1 \<and> x + y \<noteq> 0} = {}; x \<notin> {}; UCAST(10 \<rightarrow> 32) x + y \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>y. p (UCAST(10 \<rightarrow> 32) x) = Some y proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>- dom (\<lambda>a. p (UCAST(10 \<rightarrow> 32) a)) \<inter> {x. UCAST(10 \<rightarrow> 32) x + y \<noteq> 0} = {}; x \<le> 2 ^ local.asid_low_bits - 1; x + y \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>y. p x = Some y
 2. \<And>x. \<lbrakk>- dom p \<inter> {x. x \<le> 2 ^ local.asid_low_bits - 1 \<and> x + y \<noteq> 0} = {}; x \<notin> {}; UCAST(10 \<rightarrow> 32) x + y \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>y. p (UCAST(10 \<rightarrow> 32) x) = Some y proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>- dom (\<lambda>a. p (UCAST(10 \<rightarrow> 32) a)) \<inter> {x. UCAST(10 \<rightarrow> 32) x + y \<noteq> 0} = {}; x \<le> 2 ^ local.asid_low_bits - 1; x + y \<noteq> 0; \<nexists>y. p x = Some y\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>- dom p \<inter> {x. x \<le> 2 ^ local.asid_low_bits - 1 \<and> x + y \<noteq> 0} = {}; x \<notin> {}; UCAST(10 \<rightarrow> 32) x + y \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>y. p (UCAST(10 \<rightarrow> 32) x) = Some y proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; x + y \<noteq> 0; \<nexists>y. p x = Some y\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 10) x \<in> - dom (\<lambda>a. p (UCAST(10 \<rightarrow> 32) a)) \<inter> {x. UCAST(10 \<rightarrow> 32) x + y \<noteq> 0}
 2. \<And>x. \<lbrakk>- dom p \<inter> {x. x \<le> 2 ^ local.asid_low_bits - 1 \<and> x + y \<noteq> 0} = {}; x \<notin> {}; UCAST(10 \<rightarrow> 32) x + y \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>y. p (UCAST(10 \<rightarrow> 32) x) = Some y proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; x + y \<noteq> 0; p x = None\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 10) x \<notin> dom (\<lambda>a. p (UCAST(10 \<rightarrow> 32) a)) \<and> UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x) + y \<noteq> 0
 2. \<And>x. \<lbrakk>- dom p \<inter> {x. x \<le> 2 ^ local.asid_low_bits - 1 \<and> x + y \<noteq> 0} = {}; x \<notin> {}; UCAST(10 \<rightarrow> 32) x + y \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>y. p (UCAST(10 \<rightarrow> 32) x) = Some y proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; x + y \<noteq> 0; p x = None\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 10) x \<notin> dom (\<lambda>a. p (UCAST(10 \<rightarrow> 32) a))
 2. \<And>x. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; x + y \<noteq> 0; p x = None\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x) + y \<noteq> 0
 3. \<And>x. \<lbrakk>- dom p \<inter> {x. x \<le> 2 ^ local.asid_low_bits - 1 \<and> x + y \<noteq> 0} = {}; x \<notin> {}; UCAST(10 \<rightarrow> 32) x + y \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>y. p (UCAST(10 \<rightarrow> 32) x) = Some y proof (prove)
goal (3 subgoals):
 1. \<And>x ya. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; x + y \<noteq> 0; p x = None; p (x && mask 10) = Some ya\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; x + y \<noteq> 0; p x = None\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x) + y \<noteq> 0
 3. \<And>x. \<lbrakk>- dom p \<inter> {x. x \<le> 2 ^ local.asid_low_bits - 1 \<and> x + y \<noteq> 0} = {}; x \<notin> {}; UCAST(10 \<rightarrow> 32) x + y \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>y. p (UCAST(10 \<rightarrow> 32) x) = Some y proof (prove)
goal (4 subgoals):
 1. \<And>x ya. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; x + y \<noteq> 0; p x = None\<rbrakk> \<Longrightarrow> x < 2 ^ 10
 2. \<And>x ya. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; x + y \<noteq> 0; p x = None; p x = Some ya\<rbrakk> \<Longrightarrow> False
 3. \<And>x. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; x + y \<noteq> 0; p x = None\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x) + y \<noteq> 0
 4. \<And>x. \<lbrakk>- dom p \<inter> {x. x \<le> 2 ^ local.asid_low_bits - 1 \<and> x + y \<noteq> 0} = {}; x \<notin> {}; UCAST(10 \<rightarrow> 32) x + y \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>y. p (UCAST(10 \<rightarrow> 32) x) = Some y proof (prove)
goal (5 subgoals):
 1. \<And>x ya. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; x + y \<noteq> 0; p x = None\<rbrakk> \<Longrightarrow> 10 < LENGTH(32)
 2. \<And>x ya. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; x + y \<noteq> 0; p x = None\<rbrakk> \<Longrightarrow> x \<le> 2 ^ 10 - 1
 3. \<And>x ya. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; x + y \<noteq> 0; p x = None; p x = Some ya\<rbrakk> \<Longrightarrow> False
 4. \<And>x. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; x + y \<noteq> 0; p x = None\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x) + y \<noteq> 0
 5. \<And>x. \<lbrakk>- dom p \<inter> {x. x \<le> 2 ^ local.asid_low_bits - 1 \<and> x + y \<noteq> 0} = {}; x \<notin> {}; UCAST(10 \<rightarrow> 32) x + y \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>y. p (UCAST(10 \<rightarrow> 32) x) = Some y proof (prove)
goal (4 subgoals):
 1. \<And>x ya. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; x + y \<noteq> 0; p x = None\<rbrakk> \<Longrightarrow> x \<le> 2 ^ 10 - 1
 2. \<And>x ya. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; x + y \<noteq> 0; p x = None; p x = Some ya\<rbrakk> \<Longrightarrow> False
 3. \<And>x. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; x + y \<noteq> 0; p x = None\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x) + y \<noteq> 0
 4. \<And>x. \<lbrakk>- dom p \<inter> {x. x \<le> 2 ^ local.asid_low_bits - 1 \<and> x + y \<noteq> 0} = {}; x \<notin> {}; UCAST(10 \<rightarrow> 32) x + y \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>y. p (UCAST(10 \<rightarrow> 32) x) = Some y proof (prove)
goal (3 subgoals):
 1. \<And>x ya. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; x + y \<noteq> 0; p x = None; p x = Some ya\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; x + y \<noteq> 0; p x = None\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x) + y \<noteq> 0
 3. \<And>x. \<lbrakk>- dom p \<inter> {x. x \<le> 2 ^ local.asid_low_bits - 1 \<and> x + y \<noteq> 0} = {}; x \<notin> {}; UCAST(10 \<rightarrow> 32) x + y \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>y. p (UCAST(10 \<rightarrow> 32) x) = Some y proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; x + y \<noteq> 0; p x = None\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) (UCAST(32 \<rightarrow> 10) x) + y \<noteq> 0
 2. \<And>x. \<lbrakk>- dom p \<inter> {x. x \<le> 2 ^ local.asid_low_bits - 1 \<and> x + y \<noteq> 0} = {}; x \<notin> {}; UCAST(10 \<rightarrow> 32) x + y \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>y. p (UCAST(10 \<rightarrow> 32) x) = Some y proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; x + y \<noteq> 0; p x = None; (x && mask 10) + y = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>- dom p \<inter> {x. x \<le> 2 ^ local.asid_low_bits - 1 \<and> x + y \<noteq> 0} = {}; x \<notin> {}; UCAST(10 \<rightarrow> 32) x + y \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>y. p (UCAST(10 \<rightarrow> 32) x) = Some y proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; x + y \<noteq> 0; p x = None\<rbrakk> \<Longrightarrow> x < 2 ^ 10
 2. \<And>x. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; x + y \<noteq> 0; p x = None; x + y = 0\<rbrakk> \<Longrightarrow> False
 3. \<And>x. \<lbrakk>- dom p \<inter> {x. x \<le> 2 ^ local.asid_low_bits - 1 \<and> x + y \<noteq> 0} = {}; x \<notin> {}; UCAST(10 \<rightarrow> 32) x + y \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>y. p (UCAST(10 \<rightarrow> 32) x) = Some y proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; x + y \<noteq> 0; p x = None\<rbrakk> \<Longrightarrow> 10 < LENGTH(32)
 2. \<And>x. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; x + y \<noteq> 0; p x = None\<rbrakk> \<Longrightarrow> x \<le> 2 ^ 10 - 1
 3. \<And>x. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; x + y \<noteq> 0; p x = None; x + y = 0\<rbrakk> \<Longrightarrow> False
 4. \<And>x. \<lbrakk>- dom p \<inter> {x. x \<le> 2 ^ local.asid_low_bits - 1 \<and> x + y \<noteq> 0} = {}; x \<notin> {}; UCAST(10 \<rightarrow> 32) x + y \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>y. p (UCAST(10 \<rightarrow> 32) x) = Some y proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; x + y \<noteq> 0; p x = None\<rbrakk> \<Longrightarrow> x \<le> 2 ^ 10 - 1
 2. \<And>x. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; x + y \<noteq> 0; p x = None; x + y = 0\<rbrakk> \<Longrightarrow> False
 3. \<And>x. \<lbrakk>- dom p \<inter> {x. x \<le> 2 ^ local.asid_low_bits - 1 \<and> x + y \<noteq> 0} = {}; x \<notin> {}; UCAST(10 \<rightarrow> 32) x + y \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>y. p (UCAST(10 \<rightarrow> 32) x) = Some y proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x \<le> 2 ^ local.asid_low_bits - 1; x + y \<noteq> 0; p x = None; x + y = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>- dom p \<inter> {x. x \<le> 2 ^ local.asid_low_bits - 1 \<and> x + y \<noteq> 0} = {}; x \<notin> {}; UCAST(10 \<rightarrow> 32) x + y \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>y. p (UCAST(10 \<rightarrow> 32) x) = Some y proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>- dom p \<inter> {x. x \<le> 2 ^ local.asid_low_bits - 1 \<and> x + y \<noteq> 0} = {}; x \<notin> {}; UCAST(10 \<rightarrow> 32) x + y \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>y. p (UCAST(10 \<rightarrow> 32) x) = Some y proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>- dom p \<inter> {x. x \<le> 2 ^ local.asid_low_bits - 1 \<and> x + y \<noteq> 0} = {}; UCAST(10 \<rightarrow> 32) x + y \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>y. p (UCAST(10 \<rightarrow> 32) x) = Some y proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>- dom p \<inter> {x. x \<le> 2 ^ local.asid_low_bits - 1 \<and> x + y \<noteq> 0} = {}; UCAST(10 \<rightarrow> 32) x + y \<noteq> 0; \<nexists>y. p (UCAST(10 \<rightarrow> 32) x) = Some y\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>- dom p \<inter> {x. x \<le> 2 ^ local.asid_low_bits - 1 \<and> x + y \<noteq> 0} = {}; UCAST(10 \<rightarrow> 32) x + y \<noteq> 0; p (UCAST(10 \<rightarrow> 32) x) = None\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>UCAST(10 \<rightarrow> 32) x + y \<noteq> 0; p (UCAST(10 \<rightarrow> 32) x) = None\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) x \<in> - dom p \<inter> {x. x \<le> 2 ^ local.asid_low_bits - 1 \<and> x + y \<noteq> 0} proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>UCAST(10 \<rightarrow> 32) x + y \<noteq> 0; p (UCAST(10 \<rightarrow> 32) x) = None\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) x \<notin> dom p \<and> UCAST(10 \<rightarrow> 32) x \<le> 2 ^ local.asid_low_bits - 1 proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>UCAST(10 \<rightarrow> 32) x + y \<noteq> 0; p (UCAST(10 \<rightarrow> 32) x) = None\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) x \<le> 2 ^ local.asid_low_bits - 1 proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>UCAST(10 \<rightarrow> 32) x + y \<noteq> 0; p (UCAST(10 \<rightarrow> 32) x) = None\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) x < 2 ^ local.asid_low_bits proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>UCAST(10 \<rightarrow> 32) x + y \<noteq> 0; p (UCAST(10 \<rightarrow> 32) x) = None\<rbrakk> \<Longrightarrow> UCAST(10 \<rightarrow> 32) x < ?y68 x
 2. \<And>x. \<lbrakk>UCAST(10 \<rightarrow> 32) x + y \<noteq> 0; p (UCAST(10 \<rightarrow> 32) x) = None\<rbrakk> \<Longrightarrow> ?y68 x \<le> 2 ^ local.asid_low_bits proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>UCAST(10 \<rightarrow> 32) x + y \<noteq> 0; p (UCAST(10 \<rightarrow> 32) x) = None\<rbrakk> \<Longrightarrow> 2 ^ LENGTH(10) \<le> 2 ^ local.asid_low_bits proof (prove)
goal:
No subgoals!