Re: [isabelle] Constructing terms in ML



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.

On 27/09/11 09:04, Steve Wong wrote:
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






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.