Re: [isabelle] Creating Theorems in ML

Hi Florian,

Thank you for your reply. Let me try to give some more context.

So far, I managed to create a locale, and inside this locale a theorem using

# Goal.prove ctxt vars asms prop auto_tac
# where prop =  @{prop "A ⟹ (A⟹B) ⟹ (B⟹P) ⟹ P"}

print_theorems shows:

# MyL.foo_0: MyL ?st ⟹ ?A ⟹ (?A ⟹ ?B) ⟹ (?B ⟹ ?P) ⟹ ?P

which seems good to me, and which is what I want to acheive.

Now, I'd like to use my own datatype in this lemma e.g.

# datatype MyT = MyType string
# lemma foobar : "MyType t ∈ st ⟹ A ⟹ (A⟹B) ⟹ (B⟹P) ⟹ P

Which works well from within a Theory, but I want to create this lemma from my ML code using the datatype MyT  which has been defined in a Theory file.

# Goal.prove ctxt vars asms prop auto_tac
# where prop =  @{prop "MyType t ∈ st ⟹ A ⟹ (A⟹B) ⟹ (B⟹P) ⟹ P"}

Which results in an error: Illegal fixed variable: "MyType"

Is the use of the antiquotations @{prop } actually the right way to achieve this?

 -- Reto

Reto Achermann
PhD Student, ETH Zurich

On 2019-03-02 10:46:20+01:00 Florian Haftmann wrote:

Hi Reto,

> thanks a lot for your pointers. I've managed to create a few theorems -- with the sorry goal for now.
> When I try to construct a datatype defined in HOL, I've got an undefined constant error in ML.
> What's the best approach in defining data types for the interoperability between HOL and ML?
> How can they be referred to directly?
> Scratch.thy:
>  datatype Foo = Bar string
> myml.ML:
>  ? Scratch.Bar "hello"

I have no idea what your overall application is, but I would infer from
your question »as it is« that it aims towards how to interface between
code generated from HOL and Isabelle/ML.

There is already substantial support for that use case, see particulary
the antiquotations @{code …} and various @{computation* …}.  See the
tutorial on code generation for details.

Note that if you are interested to generate native Isabelle/ML strings
you should adhere to type String.literal rather than string (the details
are delicate due to different notions of »string« in different target

Hope this helps in the next steps,

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