*To*: "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>, "sewell at chalmers.se" <sewell at chalmers.se>*Subject*: Re: [isabelle] Creating Theorems in ML*From*: "Achermann Reto" <reto.achermann at inf.ethz.ch>*Date*: Sat, 2 Mar 2019 09:15:06 +0000*Accept-language*: en-US, en-GB, de-CH*In-reply-to*: <89c681f1b9c2454ea3da849c278b5941@chalmers.se>*References*: <490C2E243DCFAB4881DBDBF47E7C8A3D6C8BD962@MBX117.d.ethz.ch>, <89c681f1b9c2454ea3da849c278b5941@chalmers.se>*Thread-index*: AdTPWku5hyfwV9BHSK6Mtxynb2zNsAA3fHWAACgL8fA=*Thread-topic*: Creating Theorems in ML*User-agent*: Hiri/1.4.0.5

Hi Thomas, 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" Thanks, -- Reto -- Reto Achermann PhD Student, ETH Zurich www.retoachermann.ch/ On 2019-03-01 16:08:41+01:00 Thomas Sewell wrote: Hi Reto. In some sense you've done the difficult parts first. Using the ML interface to manipulate locale elements is a bit technical, with lots of elements to understand. I think that proving a theorem should be easier. Essentially, try to make sense of Goal.prove. At its core, it takes a term (goal) to be proven and a tactic (proof procedure) to do it, and produces a theorem. Most proof methods have corresponding tactics available in ML, for instance "by auto" is connected to "Clasimp.auto_tac". The ML interface for standard tactics and composition mechanisms is mostly found in "src/Pure/tactic.ML" and "src/Pure/tactical.ML", and I find those parts of the system a little easier to find your way around than some others. Good luck with it. Cheers, Thomas. ________________________________ From: cl-isabelle-users-bounces at lists.cam.ac.uk <cl-isabelle-users-bounces at lists.cam.ac.uk> on behalf of Achermann Reto <reto.achermann at inf.ethz.ch> Sent: Thursday, February 28, 2019 12:39:42 PM To: isabelle-users at cl.cam.ac.uk Subject: [isabelle] Creating Theorems in ML Hi, We are using ML in a project where we need to create a locale in HOL from ML code. We managed to create the locale (local_theory) using Expression.add_locale_cmd including any assumptions we defined in ML. As a next step we would like to create a theorem from ML, in the end something equivalent to this should be defined in ML: locale MyLocale = fixes S::"nat set" begin lemma foo: "A ==> (A ==> B) ==> B" by(auto) end We tried using Local_Theory.note with the Goal or Thm structures, but apart from trivial True ==> True there is not much success. Moreover, the example (3.7 Theorems) in the cookbook doesn't seem to work with 'Illegal fixed variable: "P"' I'm thankful for any pointers to examples or descriptions on how to add/define a lemma/theorem inside a locale from an ML file. Thanks, -- Reto

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

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

- Previous by Date: Re: [isabelle] “Hilbert and Isabelle” in Spektrum der Wissenschaft (March 2019)
- Next by Date: Re: [isabelle] Creating Theorems in ML
- 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