lib: produce _def and _val thes in value_type

Produce a _def theorem for the value type that provides direct symbolic
access to the right-hand side of the value_type definition. This avoids
having to unfold those terms in subsequent proofs.

The numeric value as as term is still available as <type-name>_val.

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

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 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 =
+(* 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_def 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_def 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 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