Email Gateway (Mar 11 2021 at 07:47): Email Gateway (Mar 11 2021 at 07:47):From: Jaap Boender <jaapb@kerguelen.org>
Hi list,
I've been playing around with ML and the Cookbook, trying to learn how to
write a definitional package. It's working out reasonably well, but I've got
two problems I'd like to ask for help on:
1) At some point, I need to create an application of the form "s t", where tye
types of both s and t contain type variables. So I can't just get the terms
and use $, I need to unify the types first. At the moment, I'm doing it like
follows (this code is fragile and not very nice, of course, but it's a first
attempt):
fun add_is_valid t thy =
let
val Const (is_valid_c, tiv) = Proof_Context.read_term_pattern @{context} t
val (no_wrap_c, Type ("fun", [tnw1, tnw2])) = Consts.the_const
(Proof_Context.consts_of @{context}) @{const_name is_valid_imp_no_wrap}
val (tenv, _) = Sign.typ_unify @{theory} (tnw1, tiv) (Vartab.empty, 0)
val tnw1' = Envir.norm_type tenv tnw1
val tiv' = Envir.norm_type tenv tiv
and then I can use (Const (no_wrap_c, tnw1' --> tnw2) $ Const (is_valid_c,
tiv')) for the term I need.
This works, but I have the feeling it's needlessly complicated. Is there an
easier way to do this?
2) After using Goal.prove to create a proof of the term created above, I'd
like to add it to the local theory; currently I'm doing this:
Local_Theory.note (((Binding.name (t ^ "_no_wrap")), []), [nw_proof])
which works, but then when I try to find the lemma, it turns out to have the
name
is_valid_int_element_record_C_no_wrapkind=factlocal.is_valid_int_element_record_C_no_wrap
which isn't very useful. What am I doing wrong? The problem also occurs if I
do other things, like using the @binding antiquotation.
(I am still using Isabelle2020, if that makes any difference).
Thanks in advance for any advice!
Jaap Boender
Email Gateway (Mar 13 2021 at 10:26):From: Thomas Sewell <tals4@cam.ac.uk>
Hello.
In partial answer to 1, yes, that's all a bit complicated. You shouldn't
need
to parse the term and then modify that. If it really is a constant, it's
typical
to construct polymorphic constant applications using something like
Const (@{const_name myconst}, ty) $ x $ y
where ty is computed from the types of x and y. There are a lot of
examples of
this floating around in the sources.
Erm, your question 2 is simpler, it looks like the string t you're using
to create
the name is the wrong string for this purpose.
Best regards,
Thomas.
Email Gateway (Mar 13 2021 at 11:16):From: Peter Lammich <lammich@in.tum.de>
On Sat, 2021-03-13 at 10:25 +0000, Thomas Sewell wrote:
Hello.
In partial answer to 1, yes, that's all a bit complicated. You
shouldn't
need
to parse the term and then modify that. If it really is a constant,
it's
typical
to construct polymorphic constant applications using something likeConst (@{const_name myconst}, ty) $ x $ y
A quite general solution is, e.g., in
https://www.isa-afp.org/browser_info/current/AFP/Automatic_Refinement/Mk_Term_Antiquot.html
You basically write @{mk_term "myconst ?x ?y"}, where the ?x and ?y
must be ML-variables in scope. This will do all type-computation for
you, or inform you that it's not possible (for more complex things than
just function application)
If there's interest, I'm open for suggestions how to improve on the
slightly hacky workaround to use schematic variables to map on ML
identifiers.
Last updated: Jul 15 2022 at 23:21 UTC