ainvs: use "assms" in name for arch locales

i.e. 's/AI_asms/AI_assms/g' and same for Pre_asms
("asms" is rarely expected outside of ML code)

Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

proof/invariant-abstract/AARCH64/ArchAInvsPre.thy

@@ -82,7 +82,7 @@ lemma device_frame_in_device_region:
   by (auto simp add: pspace_respects_device_region_def dom_def device_mem_def)
 
 global_naming Arch
-named_theorems AInvsPre_asms
+named_theorems AInvsPre_assms
 
 lemma get_vspace_of_thread_asid_or_global_pt:
   "(\<exists>asid. vspace_for_asid asid s = Some (get_vspace_of_thread (kheap s) (arch_state s) t))
@@ -102,7 +102,7 @@ lemma get_page_info_gpd_kmaps:
                         table_base_pt_slot_offset[where level=max_pt_level, simplified])
   done
 
-lemma ptable_rights_imp_frame[AInvsPre_asms]:
+lemma ptable_rights_imp_frame[AInvsPre_assms]:
   assumes "valid_state s"
   shows "\<lbrakk> ptable_rights t s vptr \<noteq> {}; ptable_lift t s vptr = Some (addrFromPPtr p) \<rbrakk> \<Longrightarrow>
          in_user_frame p s \<or> in_device_frame p s"
@@ -140,7 +140,7 @@ end
 interpretation AInvsPre?: AInvsPre
 proof goal_cases
   interpret Arch .
-  case 1 show ?case by (intro_locales; (unfold_locales; fact AInvsPre_asms)?)
+  case 1 show ?case by (intro_locales; (unfold_locales; fact AInvsPre_assms)?)
 qed
 
 requalify_facts

proof/invariant-abstract/AARCH64/ArchDetype_AI.thy

@@ -11,16 +11,16 @@ begin
 
 context Arch begin global_naming AARCH64
 
-named_theorems Detype_AI_asms
+named_theorems Detype_AI_assms
 
-lemma valid_globals_irq_node[Detype_AI_asms]:
+lemma valid_globals_irq_node[Detype_AI_assms]:
     "\<lbrakk> valid_global_refs s; cte_wp_at ((=) cap) ptr s \<rbrakk>
           \<Longrightarrow> interrupt_irq_node s irq \<notin> cap_range cap"
     apply (erule(1) valid_global_refsD)
     apply (simp add: global_refs_def)
     done
 
-lemma caps_of_state_ko[Detype_AI_asms]:
+lemma caps_of_state_ko[Detype_AI_assms]:
   "valid_cap cap s
    \<Longrightarrow> is_untyped_cap cap \<or>
        cap_range cap = {} \<or>
@@ -34,7 +34,7 @@ lemma caps_of_state_ko[Detype_AI_asms]:
                     split: option.splits if_splits)+
   done
 
-lemma mapM_x_storeWord[Detype_AI_asms]:
+lemma mapM_x_storeWord[Detype_AI_assms]:
 (* FIXME: taken from Retype_C.thy and adapted wrt. the missing intvl syntax. *)
   assumes al: "is_aligned ptr word_size_bits"
   shows "mapM_x (\<lambda>x. storeWord (ptr + of_nat x * word_size) 0) [0..<n]
@@ -82,7 +82,7 @@ next
     done
 qed
 
-lemma empty_fail_freeMemory [Detype_AI_asms]: "empty_fail (freeMemory ptr bits)"
+lemma empty_fail_freeMemory [Detype_AI_assms]: "empty_fail (freeMemory ptr bits)"
   by (fastforce simp: freeMemory_def mapM_x_mapM)
 
 
@@ -108,7 +108,7 @@ lemma state_hyp_refs_of_detype:
   "state_hyp_refs_of (detype S s) = (\<lambda>x. if x \<in> S then {} else state_hyp_refs_of s x)"
   by (rule ext, simp add: state_hyp_refs_of_def detype_def)
 
-lemma valid_ioports_detype[Detype_AI_asms]:
+lemma valid_ioports_detype[Detype_AI_assms]:
   "valid_ioports s \<Longrightarrow> valid_ioports (detype (untyped_range cap) s)"
   by simp
 
@@ -118,7 +118,7 @@ interpretation Detype_AI?: Detype_AI
   proof goal_cases
   interpret Arch .
   case 1 show ?case
-  by (intro_locales; (unfold_locales; fact Detype_AI_asms)?)
+  by (intro_locales; (unfold_locales; fact Detype_AI_assms)?)
   qed
 
 context detype_locale_arch begin