proof: proof updates for value_type _def -> _val

Rename _def into _val occurrences for value_type name. Does not make
full use of value_type _def theorems yet.

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

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

@@ -456,31 +456,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 =
@@ -505,7 +505,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"

proof/refine/AARCH64/ADT_H.thy

@@ -745,7 +745,7 @@ proof -
          apply (rule ucast_leq_mask)
          apply (clarsimp simp: bit_simps)
         apply (clarsimp simp: pte_relation_def ucast_ucast_mask ge_mask_eq vs_index_bits_def)
-        apply (case_tac "vs off"; simp add: ucast_leq_mask ppn_len_def)
+        apply (case_tac "vs off"; simp add: ucast_leq_mask ppn_len_val)
 
       (* NormalPT_T is an exact duplicate of the VSRootPT_T case, but I don't see any good way
          to factor out the commonality *)
@@ -815,7 +815,7 @@ proof -
        apply (rule ucast_leq_mask)
        apply (clarsimp simp: bit_simps)
       apply (clarsimp simp: pte_relation_def ucast_ucast_mask ge_mask_eq vs_index_bits_def)
-      apply (case_tac "vs off"; simp add: ucast_leq_mask ppn_len_def)
+      apply (case_tac "vs off"; simp add: ucast_leq_mask ppn_len_val)
 
      apply (in_case "DataPage ?p ?sz")
      apply (clarsimp split: if_splits)