*To*: "florian.haftmann at informatik.tu-muenchen.de" <florian.haftmann at informatik.tu-muenchen.de>, "sewell at chalmers.se" <sewell at chalmers.se>, "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Creating Theorems in ML*From*: "Achermann Reto" <reto.achermann at inf.ethz.ch>*Date*: Sun, 3 Mar 2019 16:15:28 +0000*Accept-language*: en-US, en-GB, de-CH*In-reply-to*: <91e43df1-ee4c-f704-c599-a5471abcf839@informatik.tu-muenchen.de>*References*: <490C2E243DCFAB4881DBDBF47E7C8A3D6C8BD962@MBX117.d.ethz.ch> <89c681f1b9c2454ea3da849c278b5941@chalmers.se> <490C2E243DCFAB4881DBDBF47E7C8A3D6C8BF31F@MBX117.d.ethz.ch>, <91e43df1-ee4c-f704-c599-a5471abcf839@informatik.tu-muenchen.de>*Thread-index*: AdTPWku5hyfwV9BHSK6Mtxynb2zNsAA3fHWAACgL8fD///fNAIACD9EO*Thread-topic*: [isabelle] Creating Theorems in ML*User-agent*: Hiri/1.4.0.5

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? Thanks, -- Reto -- Reto Achermann PhD Student, ETH Zurich www.retoachermann.ch/ On 2019-03-02 10:46:20+01:00 Florian Haftmann wrote: Hi Reto, &gt; thanks a lot for your pointers. I've managed to create a few theorems -- with the sorry goal for now. &gt; &gt; When I try to construct a datatype defined in HOL, I've got an undefined constant error in ML. &gt; &gt; What's the best approach in defining data types for the interoperability between HOL and ML? &gt; How can they be referred to directly? &gt; &gt; Scratch.thy: &gt; datatype Foo = Bar string &gt; &gt; myml.ML: &gt; ? 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 languages). Hope this helps in the next steps, Florian

**Follow-Ups**:**Re: [isabelle] Creating Theorems in ML***From:*Florian Haftmann

**References**:**Re: [isabelle] Creating Theorems in ML***From:*Thomas Sewell

**Re: [isabelle] Creating Theorems in ML***From:*Achermann Reto

**Re: [isabelle] Creating Theorems in ML***From:*Florian Haftmann

- Previous by Date: Re: [isabelle] “Hilbert and Isabelle” in Spektrum der Wissenschaft (March 2019)
- Next by Date: [isabelle] Decomposing an Infinite Sum
- Previous by Thread: Re: [isabelle] Creating Theorems in ML
- Next by Thread: Re: [isabelle] Creating Theorems in ML
- Cl-isabelle-users March 2019 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list