Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Accessing ML terms in Isabelle theory

Email Gateway (Aug 22 2022 at 10:23):

From: Iulia Dragomir <iulia.dragomir@aalto.fi>
Dear all,

I would like to ask if and how it is possible to refer in an Isabelle
theory to an ML defined term. For example, I have the following theory:

theory Test imports Main
begin

definition "A a b = a + b"

ML {*
val t1 = "a + b";
val t2 = @{cterm "a+b"};
val t3 = @{term "a + b"};
*}

lemma "A a b = ???"
sorry

end

Particularly, how can I use one of the three t's as the right hand-side
member of the lemma? And which t - string t1, cterm t2 or term t3 -
should be used in this case?

Thanks.

Best regards,
Iulia Dragomir

Email Gateway (Aug 22 2022 at 10:24):

From: Lars Hupel <hupel@in.tum.de>
Dear Iulia,

I would like to ask if and how it is possible to refer in an Isabelle
theory to an ML defined term. For example, I have the following theory:

there has been a thread on this mailing list recently:

<https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-June/msg00076.html>

The bottom line is: It's possible; but to make it work correctly, some
more thought is required. You can find an early prototype here:

<https://github.com/larsrh/purely-experimental>

Have a look at the file "Splice_Examples.thy".

Cheers
Lars

Last updated: Apr 25 2024 at 08:20 UTC