theory ArchArch_AI

lemma dom_ucast_eq_7:
  "(- dom (\<lambda>a::7 \<comment> \<open>asid_high_bits\<close> word. p (ucast a::word32)) \<inter> {x. x \<le> 2 ^ asid_high_bits - 1} = {}) =
   (- dom p \<inter> {x. x \<le> 2 ^ asid_high_bits - 1} = {})" apply safe apply clarsimp apply (rule ccontr) apply (erule_tac x="ucast x" in in_emptyE) apply (clarsimp simp: asid_high_bits_max_word) 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_high_bits_def) apply simp apply (clarsimp simp: asid_high_bits_max_word) 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_high_bits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (- dom (\<lambda>a. p (UCAST(7 \<rightarrow> 32) a)) \<inter> {x. x \<le> 2 ^ local.asid_high_bits - 1} = {}) = (- dom p \<inter> {x. x \<le> 2 ^ local.asid_high_bits - 1} = {}) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>- dom (\<lambda>a. p (UCAST(7 \<rightarrow> 32) a)) \<inter> {x. x \<le> 2 ^ local.asid_high_bits - 1} = {}; x \<notin> {}; x \<le> 2 ^ local.asid_high_bits - 1\<rbrakk> \<Longrightarrow> \<exists>y. p x = Some y
 2. \<And>x. \<lbrakk>- dom p \<inter> {x. x \<le> 2 ^ local.asid_high_bits - 1} = {}; x \<notin> {}; x \<le> 2 ^ local.asid_high_bits - 1\<rbrakk> \<Longrightarrow> \<exists>y. p (UCAST(7 \<rightarrow> 32) x) = Some y proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>- dom (\<lambda>a. p (UCAST(7 \<rightarrow> 32) a)) \<inter> {x. x \<le> 2 ^ local.asid_high_bits - 1} = {}; x \<le> 2 ^ local.asid_high_bits - 1\<rbrakk> \<Longrightarrow> \<exists>y. p x = Some y
 2. \<And>x. \<lbrakk>- dom p \<inter> {x. x \<le> 2 ^ local.asid_high_bits - 1} = {}; x \<notin> {}; x \<le> 2 ^ local.asid_high_bits - 1\<rbrakk> \<Longrightarrow> \<exists>y. p (UCAST(7 \<rightarrow> 32) x) = Some y proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>- dom (\<lambda>a. p (UCAST(7 \<rightarrow> 32) a)) \<inter> {x. x \<le> 2 ^ local.asid_high_bits - 1} = {}; x \<le> 2 ^ local.asid_high_bits - 1; \<nexists>y. p x = Some y\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>- dom p \<inter> {x. x \<le> 2 ^ local.asid_high_bits - 1} = {}; x \<notin> {}; x \<le> 2 ^ local.asid_high_bits - 1\<rbrakk> \<Longrightarrow> \<exists>y. p (UCAST(7 \<rightarrow> 32) x) = Some y proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x \<le> 2 ^ local.asid_high_bits - 1; \<nexists>y. p x = Some y\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 7) x \<in> - dom (\<lambda>a. p (UCAST(7 \<rightarrow> 32) a)) \<inter> {x. x \<le> 2 ^ local.asid_high_bits - 1}
 2. \<And>x. \<lbrakk>- dom p \<inter> {x. x \<le> 2 ^ local.asid_high_bits - 1} = {}; x \<notin> {}; x \<le> 2 ^ local.asid_high_bits - 1\<rbrakk> \<Longrightarrow> \<exists>y. p (UCAST(7 \<rightarrow> 32) x) = Some y proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<le> 2 ^ local.asid_high_bits - 1; p x = None; p (UCAST(7 \<rightarrow> 32) (UCAST(32 \<rightarrow> 7) x)) = Some y\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>- dom p \<inter> {x. x \<le> 2 ^ local.asid_high_bits - 1} = {}; x \<notin> {}; x \<le> 2 ^ local.asid_high_bits - 1\<rbrakk> \<Longrightarrow> \<exists>y. p (UCAST(7 \<rightarrow> 32) x) = Some y proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<le> 2 ^ local.asid_high_bits - 1; p x = None; p (x && mask 7) = Some y\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>- dom p \<inter> {x. x \<le> 2 ^ local.asid_high_bits - 1} = {}; x \<notin> {}; x \<le> 2 ^ local.asid_high_bits - 1\<rbrakk> \<Longrightarrow> \<exists>y. p (UCAST(7 \<rightarrow> 32) x) = Some y proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>x \<le> 2 ^ local.asid_high_bits - 1; p x = None\<rbrakk> \<Longrightarrow> x < 2 ^ 7
 2. \<And>x y. \<lbrakk>x \<le> 2 ^ local.asid_high_bits - 1; p x = None; p x = Some y\<rbrakk> \<Longrightarrow> False
 3. \<And>x. \<lbrakk>- dom p \<inter> {x. x \<le> 2 ^ local.asid_high_bits - 1} = {}; x \<notin> {}; x \<le> 2 ^ local.asid_high_bits - 1\<rbrakk> \<Longrightarrow> \<exists>y. p (UCAST(7 \<rightarrow> 32) x) = Some y proof (prove)
goal (4 subgoals):
 1. \<And>x y. \<lbrakk>x \<le> 2 ^ local.asid_high_bits - 1; p x = None\<rbrakk> \<Longrightarrow> 7 < LENGTH(32)
 2. \<And>x y. \<lbrakk>x \<le> 2 ^ local.asid_high_bits - 1; p x = None\<rbrakk> \<Longrightarrow> x \<le> 2 ^ 7 - 1
 3. \<And>x y. \<lbrakk>x \<le> 2 ^ local.asid_high_bits - 1; p x = None; p x = Some y\<rbrakk> \<Longrightarrow> False
 4. \<And>x. \<lbrakk>- dom p \<inter> {x. x \<le> 2 ^ local.asid_high_bits - 1} = {}; x \<notin> {}; x \<le> 2 ^ local.asid_high_bits - 1\<rbrakk> \<Longrightarrow> \<exists>y. p (UCAST(7 \<rightarrow> 32) x) = Some y proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>x \<le> 2 ^ local.asid_high_bits - 1; p x = None\<rbrakk> \<Longrightarrow> x \<le> 2 ^ 7 - 1
 2. \<And>x y. \<lbrakk>x \<le> 2 ^ local.asid_high_bits - 1; p x = None; p x = Some y\<rbrakk> \<Longrightarrow> False
 3. \<And>x. \<lbrakk>- dom p \<inter> {x. x \<le> 2 ^ local.asid_high_bits - 1} = {}; x \<notin> {}; x \<le> 2 ^ local.asid_high_bits - 1\<rbrakk> \<Longrightarrow> \<exists>y. p (UCAST(7 \<rightarrow> 32) x) = Some y proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<le> 2 ^ local.asid_high_bits - 1; p x = None; p x = Some y\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>- dom p \<inter> {x. x \<le> 2 ^ local.asid_high_bits - 1} = {}; x \<notin> {}; x \<le> 2 ^ local.asid_high_bits - 1\<rbrakk> \<Longrightarrow> \<exists>y. p (UCAST(7 \<rightarrow> 32) x) = Some y proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>- dom p \<inter> {x. x \<le> 2 ^ local.asid_high_bits - 1} = {}; x \<notin> {}; x \<le> 2 ^ local.asid_high_bits - 1\<rbrakk> \<Longrightarrow> \<exists>y. p (UCAST(7 \<rightarrow> 32) x) = Some y proof (prove)
goal (1 subgoal):
 1. \<And>x. - dom p \<inter> {x. x \<le> 2 ^ local.asid_high_bits - 1} = {} \<Longrightarrow> \<exists>y. p (UCAST(7 \<rightarrow> 32) x) = Some y proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>- dom p \<inter> {x. x \<le> 2 ^ local.asid_high_bits - 1} = {}; \<nexists>y. p (UCAST(7 \<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_high_bits - 1} = {}; p (UCAST(7 \<rightarrow> 32) x) = None\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x. p (UCAST(7 \<rightarrow> 32) x) = None \<Longrightarrow> UCAST(7 \<rightarrow> 32) x \<in> - dom p \<inter> {x. x \<le> 2 ^ local.asid_high_bits - 1} proof (prove)
goal (1 subgoal):
 1. \<And>x. p (UCAST(7 \<rightarrow> 32) x) = None \<Longrightarrow> UCAST(7 \<rightarrow> 32) x \<notin> dom p \<and> UCAST(7 \<rightarrow> 32) x \<le> 2 ^ local.asid_high_bits - 1 proof (prove)
goal (1 subgoal):
 1. \<And>x. p (UCAST(7 \<rightarrow> 32) x) = None \<Longrightarrow> UCAST(7 \<rightarrow> 32) x \<le> 2 ^ local.asid_high_bits - 1 proof (prove)
goal (1 subgoal):
 1. \<And>x. p (UCAST(7 \<rightarrow> 32) x) = None \<Longrightarrow> UCAST(7 \<rightarrow> 32) x < 2 ^ local.asid_high_bits proof (prove)
goal (2 subgoals):
 1. \<And>x. p (UCAST(7 \<rightarrow> 32) x) = None \<Longrightarrow> UCAST(7 \<rightarrow> 32) x < ?y54 x
 2. \<And>x. p (UCAST(7 \<rightarrow> 32) x) = None \<Longrightarrow> ?y54 x \<le> 2 ^ local.asid_high_bits proof (prove)
goal (1 subgoal):
 1. \<And>x. p (UCAST(7 \<rightarrow> 32) x) = None \<Longrightarrow> 2 ^ LENGTH(7) \<le> 2 ^ local.asid_high_bits proof (prove)
goal:
No subgoals!