Re: [isabelle] Creating cterms with automatic type inference from several distinct terms in Isabelle/ML



Dear Alexander Krauss,

Thank you for your email. Indeed, your reply pointed me in the right
direction.

It seems that there is a nearly canonical solution for my problem (without
the explicit use of the schematic type variables). The solution involves
the use of the “place-holder” type dummyT, which is defined in term.ML (I
can only assume it was defined specifically for this use case), e.g.

ML ‹
val f = Const ("HOL.eq", dummyT);
val A = @{term "A::'b"};
val q = (f $ A $ A)
  |> Syntax.check_term @{context}
  |> Thm.cterm_of @{context};
›

This method is presented in Section 3.5 in "The Isabelle Cookbook" (May 28,
2015 draft) by Christian Urban. I can hardly believe that I missed the
relevant example upon the first reading. Regretfully, I only have several
days of experience in Isabelle/ML coding, therefore, please accept my
apologies for the naive question.

Thank you



On Wed, May 1, 2019 at 2:16 PM Alexander Krauss <krauss at in.tum.de> wrote:

> Dear MLA,
>
> (re-sending as I forgot to Cc the list)
>
> Am 01.05.2019 um 01:06 schrieb mailing-list anonymous:
> > I would like to understand if there exists a canonical method for
> creating
> > cterms with automatic type inference from several distinct terms in
> > Isabelle/ML, given that some of these distinct terms are supplied by the
> > user.
>
> I there is not really a well-established canonical method, since the
> needs of tools are quite different in the details.
>
> What tools usually do is try to get to a "fully typed" stage as soon as
> possible in the outermost layers, and then work with full type
> information internally, which means that you must usually carry types
> around everywhere.
>
> What I would try is this:
>
> * Make sure you get the user-provided constants / terms in a polymorphic
> version, i.e., with schematic type variables. Here, the function
> "Variable.polymorphic" should help.
>
> * Then, construct the combined terms as you need them, and run type
> checking on this. (-> Syntax.check_terms). I think this should
> instantiate the type variables properly.
>
> * Then you should get terms on which Thm.cterm_of should work.
>
> Note that Syntax.check_terms includes several specific things like
> insertion of coercions etc. But it is the most general answer to "how do
> I check / infer types".
>
> Hope this helps.
>
> Alex
>


-- 
Please accept my apologies for posting anonymously. This is done to protect
my privacy. I can make my identity and my real contact details available
upon request in private communication under the condition that they are not
to be mentioned on the mailing list.



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