[isabelle] Constructing terms in ML



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.