aarch64 ainvs+refine: remove unused dom_ucast_eq

The old version of dom_ucast_eq in AInvs is not useful, because the
necessary constants are not available yet in AInvs.

Signed-off-by: Gerwin Klein <[email protected]>

proof/invariant-abstract/AARCH64/ArchArch_AI.thy

@@ -78,56 +78,10 @@ lemma check_vp_inv: "\<lbrace>P\<rbrace> check_vp_alignment sz w \<lbrace>\<lamb
   apply simp
   done
 
-
 lemma p2_low_bits_max:
   "(2 ^ asid_low_bits - 1) = (max_word :: asid_low_index)"
   by (simp add: asid_low_bits_def)
 
-lemma dom_ucast_eq:
-  "is_aligned y asid_low_bits \<Longrightarrow>
-   (- dom (\<lambda>a::asid_low_index. p (ucast a :: machine_word)) \<inter> {x. ucast x + (y::AARCH64_A.asid) \<noteq> 0} = {}) =
-   (- dom p \<inter> {x. x \<le> 2 ^ asid_low_bits - 1 \<and> x + ucast 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: mask_2pm1[symmetric] ucast_ucast_mask2 is_down is_aligned_mask)
-   apply (frule and_mask_eq_iff_le_mask[THEN iffD2])
-   apply (simp add: asid_low_bits_def)
-   apply (erule notE)
-   apply (subst word_plus_and_or_coroll)
-    apply word_eqI_solve
-   apply (subst (asm) word_plus_and_or_coroll; word_bitwise, clarsimp simp: word_size)
-  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 conjI)
-   apply (rule word_less_sub_1)
-   apply (rule order_less_le_trans)
-    apply (rule ucast_less, simp)
-   apply (simp add: asid_low_bits_def)
-  apply clarsimp
-  apply (erule notE)
-  apply (simp add: is_aligned_mask asid_low_bits_def)
-  apply (subst word_plus_and_or_coroll)
-   apply word_eqI_solve
-  apply (subst (asm) word_plus_and_or_coroll)
-   apply (word_bitwise, clarsimp simp: word_size)
-  apply (word_bitwise)
-  done
-
-
 lemma asid_high_bits_max_word:
   "(2 ^ asid_high_bits - 1) = (max_word :: asid_high_index)"
   by (simp add: asid_high_bits_def)

proof/refine/AARCH64/Arch_R.thy

@@ -937,7 +937,7 @@ lemma decodeARMVSpaceInvocation_corres[corres]:
   apply clarsimp
   done
 
-lemma dom_ucast_eq: (* FIXME AARCH64: remove the one in AInvs; doesn't have abs_asid_entry yet *)
+lemma dom_ucast_eq:
   "is_aligned y asid_low_bits \<Longrightarrow>
    (- dom (\<lambda>a::asid_low_index. map_option abs_asid_entry (p (ucast a :: machine_word))) \<inter>
      {x. ucast x + (y::AARCH64_A.asid) \<noteq> 0} = {}) =