From 00e95065de55eb6e539844b3e01b2b8ea179227e Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Fri, 27 Oct 2023 09:27:31 +1100 Subject: [PATCH] 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 _val. Signed-off-by: Gerwin Klein --- lib/Value_Type.thy | 55 +++++++++++++++++++++++++----------- lib/test/Value_Type_Test.thy | 38 +++++++++++++++++++------ 2 files changed, 69 insertions(+), 24 deletions(-) diff --git a/lib/Value_Type.thy b/lib/Value_Type.thy index e01ec193ff..e5f4d6a079 100644 --- a/lib/Value_Type.thy +++ b/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 \ (* -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 diff --git a/lib/test/Value_Type_Test.thy b/lib/test/Value_Type_Test.thy index 36636c97d6..cf8fba32c8 100644 --- a/lib/test/Value_Type_Test.thy +++ b/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 \The RHS does not have to be of type nat, it just has to evaluate to any numeral:\ +text \ + The RHS has to be of type @{typ nat} or @{typ int}. @{typ int} will be automatically cast to + @{term nat}:\ value_type num_queues = "num_prio * num_domains" text \This produces a type of the specified size and a constant of type nat:\ typ num_queues term num_queues -thm num_queues_def -text \You can leave out the constant definition, and just define the type:\ +text \You get a symbolic definition theorem:\ +lemma "num_queues = nat (num_prio * num_domains)" + by (rule num_queues_def) + +text \And a numeric value theorem:\ +lemma "num_queues = 4096" + by (rule num_queues_val) + + +text \You can leave out the constant definitions, and just define the type:\ value_type (no_def) num_something = "10 * num_domains" typ num_something +text \ + If the value on the rhs is not of type @{typ nat}, it can still be cast to @{typ nat} manually:\ +definition some_word :: "8 word" where + "some_word \ 0xFF" + +value_type word_val = "unat (some_word && 0xF0)" + +lemma "word_val = (0xF0::nat)" + by (rule word_val_val) + + text \ @{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: -\ + Example:\ context begin -definition X::int where "X = 10" +definition X::nat where "X = 10" value_type x_t = X