Email Gateway (Aug 18 2022 at 18:26): Email Gateway (Aug 18 2022 at 18:26):From: Steve Wong <s.wong.731@gmail.com>
Hi all,
I'm trying to construct the term for "ALL x y. x = y". I know I could just
use Syntax.read_term, but what if I want to construct it term by term using
the constructor functions? I see that the term should look something like:
Const ("HOL.All", "('a => HOL.bool) => HOL.bool") $
Abs ("x", "'a",
Const ("HOL.All", "('a => HOL.bool) => HOL.bool") $
Abs ("y", "'a",
Const ("HOL.eq", "'a => 'a => HOL.bool") $ Bound 1 $ Bound 0))
Without fixing the types of x and y, HOLogic.mk_eq (Bound 0, Bound 1) gives
an error, because it can't find the type of Bound terms. I was just thinking
to create the mk_eq term first, then wrap it inside a mk_all and itself
inside another mk_all. Is there a better way to go about this?
Thanks a lot in advance.
Steve
Email Gateway (Aug 18 2022 at 18:26):From: Thomas Sewell <Thomas.Sewell@nicta.com.au>
Hello Steve.
HOLogic.eq_const might be able to help you. You need to supply it the
type, which is expected.
For instance
ML {* let val T = @{typ 'a} in
HOLogic.mk_all ("x", T, HOLogic.mk_all ("y", T, HOLogic.eq_const T
$ Bound 1 $ Bound 0)) end
*}
Or the slightly shorter
ML {* let val T = @{typ 'a} in
HOLogic.list_all ([("x", T), ("y", T)], HOLogic.eq_const T $ Bound
1 $ Bound 0) end
*}
There are usually many different ways to do things.
Here is another one, which may come as something of a surprise:
ML {* let val T = @{typ 'a} in
HOLogic.mk_all ("x", T, HOLogic.mk_all ("y", T, HOLogic.eq_const T
$ Free ("x", T) $ Free ("y", T))) end
*}
A number of the functions that construct lambda-terms call absfree,
which will captrue Free variables with the same name and type as the
variable being bound. It happens that mk_all calls this, but list_all
doesn't. Obviously.
As for whether there's a better way to go about this, well, the example
is too limited. Usually you don't use ML to build any single thing,
rather to encode a recipe for producing many terms, theorems, etc.
If you really do just want to produce this term once, you might as well
just quote it with @{term "ALL x y. x = y"}. Otherwise it depends what
you parameters really are. If you want to produce this term for various
types T, for instance, you could use the code above. In more complex
cases, you tend to end up tearing apart your input terms and thinking
carefully about which parts you can be certain are type-carrying. This
is not a lot of fun. The approach of using Free variables to represent
Bound variables whenever the Abs is not yet closed may help sometimes,
but requires some additional machinery for picking them at the right
time and making sure their names are fresh.
Yours,
Thomas.
Last updated: Apr 26 2024 at 08:19 UTC