produce _def and _val theorems in value_type

lib/Value_Type.thy

@@ -10,7 +10,7 @@ keywords "value_type" :: thy_decl
 begin
 
 (*
-   Define a type synonym from a term that evaluates to a numeral.
+   Define a type synonym from a term of type nat or int that evaluates to a (positive) numeral.
 
    Examples:
 
@@ -41,6 +41,8 @@ fun force_nat_numeral (Const (@{const_name numeral}, Type ("fun", [num, _])) $ n
   | force_nat_numeral (Const (@{const_name "Groups.zero"}, _)) = @{term "0::nat"}
   | force_nat_numeral t = raise TERM ("force_nat_numeral: number expected", [t])
 
+fun cast_to_nat t = if type_of t = @{typ int} then @{term nat} $ t else t
+
 fun make_type binding v lthy =
   let
     val n = case get_term_numeral v of
@@ -51,12 +53,31 @@ fun make_type binding v lthy =
     lthy |> Typedecl.abbrev (binding, [], Mixfix.NoSyn) typ |> #2
   end
 
-fun make_def binding v lthy =
+(* Copied from method eval in HOL.thy: *)
+fun eval_tac ctxt =
+  let val conv = Code_Runtime.dynamic_holds_conv
+  in
+    CONVERSION (Conv.params_conv ~1 (Conv.concl_conv ~1 o conv) ctxt) THEN'
+    resolve_tac ctxt [TrueI]
+  end
+
+(* This produces two theorems: one symbolic _def theorem and one numeric _val theorem.
+   The _def theorem is a definition, via Specification.definition.
+   The _val theorem is proved from that definition using "eval_tac" via the code generator. *)
+fun make_defs binding t v lthy =
   let
+    val t = cast_to_nat t
     val mk_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq
-    val def_t = mk_eq (Free (Binding.name_of binding, @{typ nat}), force_nat_numeral v)
+    val def_t = mk_eq (Free (Binding.name_of binding, @{typ nat}), t)
+    val ((_, (_, def_thm)), lthy') =
+          lthy |> Specification.definition NONE [] [] (Binding.empty_atts, def_t)
+    val eq_t = mk_eq (t, force_nat_numeral v)
+    val eq_thm =
+          Goal.prove lthy' [] [] eq_t (fn {context = ctxt, prems = _} => eval_tac ctxt 1)
+    val thm = @{thm trans} OF [def_thm, eq_thm]
+    val val_binding = Binding.map_name (fn n => n ^ "_val") binding |> Binding.reset_pos
   in
-    lthy |> Specification.definition NONE [] [] (Binding.empty_atts, def_t) |> #2
+    Local_Theory.note ((val_binding, []), [thm]) lthy' |> #2
   end
 
 in
@@ -68,7 +89,7 @@ fun value_type_cmd no_def binding t lthy =
   in
     lthy
     |> make_type binding v
-    |> (if no_def then I else make_def binding v)
+    |> (if no_def then I else make_defs binding t' v)
   end
 
 val no_def_option =
@@ -86,20 +107,22 @@ end
 \<close>
 
 (*
-Potential extension idea for the future:
+Potential extension ideas for the future:
 
-It may be possible to generalise this command to non-numeral types -- as long as the RHS can
-be interpreted as some nat n, we can in theory always define a type with n elements, and instantiate
-that type into class finite. Might have to present a goal to the user that RHS evaluates > 0 in nat.
+* It may be possible to generalise this command to non-numeral types -- as long as the RHS can
+  be interpreted as some nat n, we can in theory always define a type with n elements, and
+  instantiate that type into class finite. Might have to present a goal to the user that RHS
+  evaluates > 0 in nat.
 
-There are a few wrinkles with that, because currently you can use any type on the RHS without
-complications. Requiring nat for the RHS term would not be great, because we often have word there.
-We could add coercion to nat for word and int, though, that would cover all current use cases.
+  The benefit of defining a new type instead of a type synonym for a numeral type is that type
+  checking is now more meaningful and we do get some abstraction over the actual value, which would
+  help make proofs more generic.
 
-The benefit of defining a new type instead of a type synonym for a numeral type is that type
-checking is now more meaningful and we do get some abstraction over the actual value, which would
-help make proofs more generic.
-*)
+  The disadvantage of a non-numeral type is that it is not equal to the types that come out of the
+  C parser.
 
+* We could add more automatic casts from known types to nat (e.g. from word). But it's relatively
+  low overhead to provide the cast as a user.
+*)
 
 end

lib/test/Value_Type_Test.thy

@@ -5,11 +5,13 @@
  *)
 
 theory Value_Type_Test
-imports Lib.Value_Type
+  imports
+    Lib.Value_Type
+    "Word_Lib.WordSetup"
 begin
 
 (*
-   Define a type synonym from a term that evaluates to a numeral.
+   Define a type synonym from a term of type nat or int that evaluates to a positive numeral.
 *)
 
 definition num_domains :: int where
@@ -18,31 +20,51 @@ definition num_domains :: int where
 definition num_prio :: int where
   "num_prio = 256"
 
-text \<open>The RHS does not have to be of type nat, it just has to evaluate to any numeral:\<close>
+text \<open>
+  The RHS has to be of type @{typ nat} or @{typ int}. @{typ int} will be automatically cast to
+  @{term nat}:\<close>
 value_type num_queues = "num_prio * num_domains"
 
 text \<open>This produces a type of the specified size and a constant of type nat:\<close>
 typ num_queues
 term num_queues
-thm num_queues_def
 
-text \<open>You can leave out the constant definition, and just define the type:\<close>
+text \<open>You get a symbolic definition theorem:\<close>
+lemma "num_queues = nat (num_prio * num_domains)"
+  by (rule num_queues_def)
+
+text \<open>And a numeric value theorem:\<close>
+lemma "num_queues = 4096"
+  by (rule num_queues_val)
+
+
+text \<open>You can leave out the constant definitions, and just define the type:\<close>
 value_type (no_def) num_something = "10 * num_domains"
 
 typ num_something
 
 
+text \<open>
+  If the value on the rhs is not of type @{typ nat}, it can still be cast to @{typ nat} manually:\<close>
+definition some_word :: "8 word" where
+  "some_word \<equiv> 0xFF"
+
+value_type word_val = "unat (some_word && 0xF0)"
+
+lemma "word_val = (0xF0::nat)"
+  by (rule word_val_val)
+
+
 text \<open>
   @{command value_type} uses @{command value} in the background, so all of this also works in
   anonymous local contexts, provided they don't have assumptions (so that @{command value} can
   produce code)
 
-  Example:
-\<close>
+  Example:\<close>
 context
 begin
 
-definition X::int where "X = 10"
+definition X::nat where "X = 10"
 
 value_type x_t = X
 

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

@@ -94,7 +94,7 @@ abbreviation
   vcpu_vppi_masked_C_Ptr :: "addr \<Rightarrow> (machine_word[1]) ptr" where "vcpu_vppi_masked_C_Ptr \<equiv> Ptr"
 
 declare seL4_VCPUReg_Num_def[code]
-value_type num_vcpu_regs = seL4_VCPUReg_Num
+value_type num_vcpu_regs = "unat seL4_VCPUReg_Num"
 
 abbreviation
   vcpuregs_C_Ptr :: "addr \<Rightarrow> (machine_word[num_vcpu_regs]) ptr" where "vcpuregs_C_Ptr \<equiv> Ptr"
@@ -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';