proof: updates for value_type _def -> _val

Rename occurrences of _def to _val for value_type-generated names. Does
not make full use of value_type _def theorems yet.

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

proof/crefine/AARCH64/ADT_C.thy

@@ -613,7 +613,7 @@ lemma carch_state_to_H_correct:
     using valid
     apply (simp add: valid_arch_state'_def)
     apply fastforce
-   apply (clarsimp simp: mask_def vmid_bits_def)
+   apply (clarsimp simp: mask_def vmid_bits_val)
   apply (rule conjI)
   using valid rel
    apply (simp add: ccur_vcpu_to_H_correct)

proof/crefine/AARCH64/ArchMove_C.thy

@@ -715,7 +715,7 @@ lemma asid_pool_at_ko':
   apply (case_tac asidpool, auto)[1]
   done
 
-(* FIXME AARCH64: move; also add vmid_bits_def to relevant bit defs *)
+(* FIXME AARCH64: move; also add vmid_bits_val to relevant bit defs *)
 value_type vmid_bits = "size (0::vmid)"
 
 (* end of move to Refine/AInvs *)

proof/crefine/AARCH64/IpcCancel_C.thy

@@ -29,7 +29,7 @@ proof -
 qed
 
 lemmas cready_queues_index_to_C_in_range =
-  cready_queues_index_to_C_in_range'[simplified num_tcb_queues_def]
+  cready_queues_index_to_C_in_range'[simplified num_tcb_queues_val]
 
 lemma cready_queues_index_to_C_inj:
   "\<lbrakk> cready_queues_index_to_C qdom prio = cready_queues_index_to_C qdom' prio';

proof/crefine/AARCH64/Retype_C.thy

@@ -1961,7 +1961,7 @@ lemma createObjects_ccorres_pte_pt:
     (\<sigma>\<lparr>ksPSpace := ?ks \<sigma>\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := ?ks' x\<rparr>\<rparr>) \<in> rf_sr")
 proof (intro impI allI)
   define array_len where "array_len \<equiv> pt_array_len"
-  note array_len_def = pt_array_len_def array_len_def
+  note array_len_def = pt_array_len_val array_len_def
 
   fix \<sigma> x
   let ?thesis = "(\<sigma>\<lparr>ksPSpace := ?ks \<sigma>\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := ?ks' x\<rparr>\<rparr>) \<in> rf_sr"
@@ -2130,7 +2130,7 @@ lemma createObjects_ccorres_pte_vs:
     (\<sigma>\<lparr>ksPSpace := ?ks \<sigma>\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := ?ks' x\<rparr>\<rparr>) \<in> rf_sr")
 proof (intro impI allI)
   define array_len where "array_len \<equiv> vs_array_len"
-  note array_len_def = vs_array_len_def array_len_def
+  note array_len_def = vs_array_len_val array_len_def
 
   fix \<sigma> x
   let ?thesis = "(\<sigma>\<lparr>ksPSpace := ?ks \<sigma>\<rparr>, x\<lparr>globals := globals x\<lparr>t_hrs_' := ?ks' x\<rparr>\<rparr>) \<in> rf_sr"

proof/crefine/AARCH64/VSpace_C.thy

@@ -1155,7 +1155,7 @@ lemma invalidateASIDEntry_ccorres:
           apply (erule array_relation_update)
             apply word_eqI_solve
            apply (clarsimp simp: asidInvalid_def)
-          apply (simp add: mask_def vmid_bits_def unat_max_word)
+          apply (simp add: mask_def vmid_bits_val unat_max_word)
          apply (rule ccorres_return_Skip)
         apply ceqv
        apply (ctac add: invalidateASID_ccorres)
@@ -1185,7 +1185,7 @@ lemma invalidateVMIDEntry_ccorres:
   apply (simp flip: fun_upd_apply)
   apply (erule array_relation_update, rule refl)
    apply (simp (no_asm) add: asidInvalid_def)
-  apply (simp (no_asm) add: mask_def vmid_bits_def unat_max_word)
+  apply (simp (no_asm) add: mask_def vmid_bits_val unat_max_word)
   done
 
 crunches invalidateVMIDEntry, invalidateASID
@@ -1233,7 +1233,7 @@ lemma findFreeHWASID_ccorres:
               apply (simp add: throwError_def return_def split: if_split)
               apply (clarsimp simp: returnOk_def return_def inr_rrel_def rf_sr_armKSNextVMID)
               apply (drule rf_sr_armKSVMIDTable_rel')
-              apply (clarsimp simp: array_relation_def vmid_bits_def mask_def)
+              apply (clarsimp simp: array_relation_def vmid_bits_val mask_def)
               apply (erule_tac x="armKSNextASID_' (globals s) + word_of_nat (length ys)" in allE)
               apply (clarsimp simp: valid_arch_state'_def ran_def)
               apply ((rule conjI, uint_arith, simp add: take_bit_nat_def unsigned_of_nat, clarsimp)+)[1]
@@ -1316,7 +1316,7 @@ lemma findFreeHWASID_ccorres:
      apply (drule rf_sr_armKSVMIDTable_rel')
      apply (clarsimp simp: array_relation_def)
      apply (erule_tac x="armKSNextASID_' (globals s')" in allE, erule impE)
-      apply (simp add: vmid_bits_def mask_def)
+      apply (simp add: vmid_bits_val mask_def)
      apply simp
     apply (fold mapME_def)
     apply (wp mapME_wp')
@@ -1357,7 +1357,7 @@ lemma storeHWASID_ccorres:
                               cmachine_state_relation_def carch_state_relation_def carch_globals_def
                         simp del: fun_upd_apply)
         apply (erule array_relation_update, rule refl, simp)
-        apply (simp add: mask_def vmid_bits_def unat_max_word)
+        apply (simp add: mask_def vmid_bits_val unat_max_word)
        apply wp
       apply (clarsimp simp: guard_is_UNIV_def split: if_splits)
       apply (clarsimp simp: zero_sle_ucast_up is_down word_sless_alt sint_ucast_eq_uint)

proof/crefine/AARCH64/Wellformed_C.thy

@@ -497,31 +497,31 @@ lemma maxDom_sgt_0_maxDomain:
 
 lemma num_domains_calculation:
   "num_domains = numDomains"
-  unfolding num_domains_def by eval
+  unfolding num_domains_val by eval
 
 private lemma num_domains_card_explicit:
   "num_domains = CARD(num_domains)"
-  by (simp add: num_domains_def)
+  by (simp add: num_domains_val)
 
 lemmas num_domains_index_updates =
-  index_update[where 'b=num_domains, folded num_domains_card_explicit num_domains_def,
+  index_update[where 'b=num_domains, folded num_domains_card_explicit num_domains_val,
                simplified num_domains_calculation]
-  index_update2[where 'b=num_domains, folded num_domains_card_explicit num_domains_def,
+  index_update2[where 'b=num_domains, folded num_domains_card_explicit num_domains_val,
                 simplified num_domains_calculation]
 
 (* C ArrayGuards will throw these at us and there is no way to avoid a proof of being less than a
    specific number expressed as a word, so we must introduce these. However, being explicit means
    lack of discipline can lead to a violation. *)
-lemma numDomains_less_numeric_explicit[simplified num_domains_def One_nat_def]:
+lemma numDomains_less_numeric_explicit[simplified num_domains_val One_nat_def]:
   "x < Kernel_Config.numDomains \<Longrightarrow> x < num_domains"
   by (simp add: num_domains_calculation)
 
-lemma numDomains_less_unat_ucast_explicit[simplified num_domains_def]:
+lemma numDomains_less_unat_ucast_explicit[simplified num_domains_val]:
   "unat x < Kernel_Config.numDomains \<Longrightarrow> (ucast (x::domain) :: machine_word) < of_nat num_domains"
   apply (rule word_less_nat_alt[THEN iffD2])
   apply transfer
   apply simp
-  apply (drule numDomains_less_numeric_explicit, simp add: num_domains_def)
+  apply (drule numDomains_less_numeric_explicit, simp add: num_domains_val)
   done
 
 lemmas maxDomain_le_unat_ucast_explicit =
@@ -546,7 +546,7 @@ value_type num_tcb_queues = "numDomains * numPriorities"
 
 lemma num_tcb_queues_calculation:
   "num_tcb_queues = numDomains * numPriorities"
-  unfolding num_tcb_queues_def by eval
+  unfolding num_tcb_queues_val by eval
 
 
 (* Input abbreviations for API object types *)

proof/crefine/ARM/IpcCancel_C.thy

@@ -30,7 +30,7 @@ proof -
 qed
 
 lemmas cready_queues_index_to_C_in_range =
-  cready_queues_index_to_C_in_range'[simplified num_tcb_queues_def]
+  cready_queues_index_to_C_in_range'[simplified num_tcb_queues_val]
 
 lemma cready_queues_index_to_C_inj:
   "\<lbrakk> cready_queues_index_to_C qdom prio = cready_queues_index_to_C qdom' prio';

proof/crefine/ARM/Wellformed_C.thy

@@ -426,31 +426,31 @@ lemma maxDom_sgt_0_maxDomain:
 
 lemma num_domains_calculation:
   "num_domains = numDomains"
-  unfolding num_domains_def by eval
+  unfolding num_domains_val by eval
 
 private lemma num_domains_card_explicit:
   "num_domains = CARD(num_domains)"
-  by (simp add: num_domains_def)
+  by (simp add: num_domains_val)
 
 lemmas num_domains_index_updates =
-  index_update[where 'b=num_domains, folded num_domains_card_explicit num_domains_def,
+  index_update[where 'b=num_domains, folded num_domains_card_explicit num_domains_val,
                simplified num_domains_calculation]
-  index_update2[where 'b=num_domains, folded num_domains_card_explicit num_domains_def,
+  index_update2[where 'b=num_domains, folded num_domains_card_explicit num_domains_val,
                 simplified num_domains_calculation]
 
 (* C ArrayGuards will throw these at us and there is no way to avoid a proof of being less than a
    specific number expressed as a word, so we must introduce these. However, being explicit means
    lack of discipline can lead to a violation. *)
-lemma numDomains_less_numeric_explicit[simplified num_domains_def One_nat_def]:
+lemma numDomains_less_numeric_explicit[simplified num_domains_val One_nat_def]:
   "x < Kernel_Config.numDomains \<Longrightarrow> x < num_domains"
   by (simp add: num_domains_calculation)
 
-lemma numDomains_less_unat_ucast_explicit[simplified num_domains_def]:
+lemma numDomains_less_unat_ucast_explicit[simplified num_domains_val]:
   "unat x < Kernel_Config.numDomains \<Longrightarrow> (ucast (x::domain) :: machine_word) < of_nat num_domains"
   apply (rule word_less_nat_alt[THEN iffD2])
   apply transfer
   apply simp
-  apply (drule numDomains_less_numeric_explicit, simp add: num_domains_def)
+  apply (drule numDomains_less_numeric_explicit, simp add: num_domains_val)
   done
 
 lemmas maxDomain_le_unat_ucast_explicit =
@@ -475,7 +475,7 @@ value_type num_tcb_queues = "numDomains * numPriorities"
 
 lemma num_tcb_queues_calculation:
   "num_tcb_queues = numDomains * numPriorities"
-  unfolding num_tcb_queues_def by eval
+  unfolding num_tcb_queues_val by eval
 
 
 abbreviation(input)

proof/crefine/ARM_HYP/IpcCancel_C.thy

@@ -30,7 +30,7 @@ proof -
 qed
 
 lemmas cready_queues_index_to_C_in_range =
-  cready_queues_index_to_C_in_range'[simplified num_tcb_queues_def]
+  cready_queues_index_to_C_in_range'[simplified num_tcb_queues_val]
 
 lemma cready_queues_index_to_C_inj:
   "\<lbrakk> cready_queues_index_to_C qdom prio = cready_queues_index_to_C qdom' prio';

proof/crefine/ARM_HYP/Wellformed_C.thy

@@ -461,31 +461,31 @@ lemma maxDom_sgt_0_maxDomain:
 
 lemma num_domains_calculation:
   "num_domains = numDomains"
-  unfolding num_domains_def by eval
+  unfolding num_domains_val by eval
 
 private lemma num_domains_card_explicit:
   "num_domains = CARD(num_domains)"
-  by (simp add: num_domains_def)
+  by (simp add: num_domains_val)
 
 lemmas num_domains_index_updates =
-  index_update[where 'b=num_domains, folded num_domains_card_explicit num_domains_def,
+  index_update[where 'b=num_domains, folded num_domains_card_explicit num_domains_val,
                simplified num_domains_calculation]
-  index_update2[where 'b=num_domains, folded num_domains_card_explicit num_domains_def,
+  index_update2[where 'b=num_domains, folded num_domains_card_explicit num_domains_val,
                 simplified num_domains_calculation]
 
 (* C ArrayGuards will throw these at us and there is no way to avoid a proof of being less than a
    specific number expressed as a word, so we must introduce these. However, being explicit means
    lack of discipline can lead to a violation. *)
-lemma numDomains_less_numeric_explicit[simplified num_domains_def One_nat_def]:
+lemma numDomains_less_numeric_explicit[simplified num_domains_val One_nat_def]:
   "x < Kernel_Config.numDomains \<Longrightarrow> x < num_domains"
   by (simp add: num_domains_calculation)
 
-lemma numDomains_less_unat_ucast_explicit[simplified num_domains_def]:
+lemma numDomains_less_unat_ucast_explicit[simplified num_domains_val]:
   "unat x < Kernel_Config.numDomains \<Longrightarrow> (ucast (x::domain) :: machine_word) < of_nat num_domains"
   apply (rule word_less_nat_alt[THEN iffD2])
   apply transfer
   apply simp
-  apply (drule numDomains_less_numeric_explicit, simp add: num_domains_def)
+  apply (drule numDomains_less_numeric_explicit, simp add: num_domains_val)
   done
 
 lemmas maxDomain_le_unat_ucast_explicit =
@@ -510,7 +510,7 @@ value_type num_tcb_queues = "numDomains * numPriorities"
 
 lemma num_tcb_queues_calculation:
   "num_tcb_queues = numDomains * numPriorities"
-  unfolding num_tcb_queues_def by eval
+  unfolding num_tcb_queues_val by eval
 
 
 (* Input abbreviations for API object types *)

proof/crefine/RISCV64/IpcCancel_C.thy

@@ -29,7 +29,7 @@ proof -
 qed
 
 lemmas cready_queues_index_to_C_in_range =
-  cready_queues_index_to_C_in_range'[simplified num_tcb_queues_def]
+  cready_queues_index_to_C_in_range'[simplified num_tcb_queues_val]
 
 lemma cready_queues_index_to_C_inj:
   "\<lbrakk> cready_queues_index_to_C qdom prio = cready_queues_index_to_C qdom' prio';

proof/crefine/RISCV64/Wellformed_C.thy

@@ -429,31 +429,31 @@ lemma maxDom_sgt_0_maxDomain:
 
 lemma num_domains_calculation:
   "num_domains = numDomains"
-  unfolding num_domains_def by eval
+  unfolding num_domains_val by eval
 
 private lemma num_domains_card_explicit:
   "num_domains = CARD(num_domains)"
-  by (simp add: num_domains_def)
+  by (simp add: num_domains_val)
 
 lemmas num_domains_index_updates =
-  index_update[where 'b=num_domains, folded num_domains_card_explicit num_domains_def,
+  index_update[where 'b=num_domains, folded num_domains_card_explicit num_domains_val,
                simplified num_domains_calculation]
-  index_update2[where 'b=num_domains, folded num_domains_card_explicit num_domains_def,
+  index_update2[where 'b=num_domains, folded num_domains_card_explicit num_domains_val,
                 simplified num_domains_calculation]
 
 (* C ArrayGuards will throw these at us and there is no way to avoid a proof of being less than a
    specific number expressed as a word, so we must introduce these. However, being explicit means
    lack of discipline can lead to a violation. *)
-lemma numDomains_less_numeric_explicit[simplified num_domains_def One_nat_def]:
+lemma numDomains_less_numeric_explicit[simplified num_domains_val One_nat_def]:
   "x < Kernel_Config.numDomains \<Longrightarrow> x < num_domains"
   by (simp add: num_domains_calculation)
 
-lemma numDomains_less_unat_ucast_explicit[simplified num_domains_def]:
+lemma numDomains_less_unat_ucast_explicit[simplified num_domains_val]:
   "unat x < Kernel_Config.numDomains \<Longrightarrow> (ucast (x::domain) :: machine_word) < of_nat num_domains"
   apply (rule word_less_nat_alt[THEN iffD2])
   apply transfer
   apply simp
-  apply (drule numDomains_less_numeric_explicit, simp add: num_domains_def)
+  apply (drule numDomains_less_numeric_explicit, simp add: num_domains_val)
   done
 
 lemmas maxDomain_le_unat_ucast_explicit =
@@ -478,7 +478,7 @@ value_type num_tcb_queues = "numDomains * numPriorities"
 
 lemma num_tcb_queues_calculation:
   "num_tcb_queues = numDomains * numPriorities"
-  unfolding num_tcb_queues_def by eval
+  unfolding num_tcb_queues_val by eval
 
 
 (* Input abbreviations for API object types *)

proof/crefine/X64/IpcCancel_C.thy

@@ -28,7 +28,7 @@ proof -
 qed
 
 lemmas cready_queues_index_to_C_in_range =
-  cready_queues_index_to_C_in_range'[simplified num_tcb_queues_def]
+  cready_queues_index_to_C_in_range'[simplified num_tcb_queues_val]
 
 lemma cready_queues_index_to_C_inj:
   "\<lbrakk> cready_queues_index_to_C qdom prio = cready_queues_index_to_C qdom' prio';

proof/crefine/X64/Wellformed_C.thy

@@ -472,31 +472,31 @@ lemma maxDom_sgt_0_maxDomain:
 
 lemma num_domains_calculation:
   "num_domains = numDomains"
-  unfolding num_domains_def by eval
+  unfolding num_domains_val by eval
 
 private lemma num_domains_card_explicit:
   "num_domains = CARD(num_domains)"
-  by (simp add: num_domains_def)
+  by (simp add: num_domains_val)
 
 lemmas num_domains_index_updates =
-  index_update[where 'b=num_domains, folded num_domains_card_explicit num_domains_def,
+  index_update[where 'b=num_domains, folded num_domains_card_explicit num_domains_val,
                simplified num_domains_calculation]
-  index_update2[where 'b=num_domains, folded num_domains_card_explicit num_domains_def,
+  index_update2[where 'b=num_domains, folded num_domains_card_explicit num_domains_val,
                 simplified num_domains_calculation]
 
 (* C ArrayGuards will throw these at us and there is no way to avoid a proof of being less than a
    specific number expressed as a word, so we must introduce these. However, being explicit means
    lack of discipline can lead to a violation. *)
-lemma numDomains_less_numeric_explicit[simplified num_domains_def One_nat_def]:
+lemma numDomains_less_numeric_explicit[simplified num_domains_val One_nat_def]:
   "x < Kernel_Config.numDomains \<Longrightarrow> x < num_domains"
   by (simp add: num_domains_calculation)
 
-lemma numDomains_less_unat_ucast_explicit[simplified num_domains_def]:
+lemma numDomains_less_unat_ucast_explicit[simplified num_domains_val]:
   "unat x < Kernel_Config.numDomains \<Longrightarrow> (ucast (x::domain) :: machine_word) < of_nat num_domains"
   apply (rule word_less_nat_alt[THEN iffD2])
   apply transfer
   apply simp
-  apply (drule numDomains_less_numeric_explicit, simp add: num_domains_def)
+  apply (drule numDomains_less_numeric_explicit, simp add: num_domains_val)
   done
 
 lemmas maxDomain_le_unat_ucast_explicit =
@@ -521,7 +521,7 @@ value_type num_tcb_queues = "numDomains * numPriorities"
 
 lemma num_tcb_queues_calculation:
   "num_tcb_queues = numDomains * numPriorities"
-  unfolding num_tcb_queues_def by eval
+  unfolding num_tcb_queues_val by eval
 
 
 (* Input abbreviations for API object types *)

proof/invariant-abstract/AARCH64/ArchInvariants_AI.thy

@@ -2403,7 +2403,7 @@ lemma pptrTop_ucast_ppn:
    ucast (ucast (p >> pageBits)::ppn) = p >> pageBits"
   apply (drule below_pptrTop_ipa_size)
   apply word_eqI
-  using ppn_len_def'[unfolded ppn_len_def]
+  using ppn_len_def'[unfolded ppn_len_val]
   by (fastforce dest: bit_imp_le_length)
 
 lemma kernel_window_range_addrFromPPtr:
@@ -2470,7 +2470,7 @@ lemma pt_slot_offset_pt_range:
 
 lemma ucast_ucast_ppn:
   "ucast (ucast ptr::ppn) = ptr && mask ppn_len" for ptr::obj_ref
-  by (simp add: ucast_ucast_mask ppn_len_def)
+  by (simp add: ucast_ucast_mask ppn_len_val)
 
 lemma pte_base_addr_PageTablePTE[simp]:
   "pte_base_addr (PageTablePTE ppn) = paddr_from_ppn ppn"