*To*: "Achermann Reto" <reto.achermann at inf.ethz.ch>, "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Creating Theorems in ML*From*: Thomas Sewell <sewell at chalmers.se>*Date*: Fri, 1 Mar 2019 15:08:27 +0000*Accept-language*: en-US, sv-SE*In-reply-to*: <490C2E243DCFAB4881DBDBF47E7C8A3D6C8BD962@MBX117.d.ethz.ch>*References*: <490C2E243DCFAB4881DBDBF47E7C8A3D6C8BD962@MBX117.d.ethz.ch>*Thread-index*: AdTPWku53xyFaQeQR/qzG9G4/RfDsQA5UTBY*Thread-topic*: Creating Theorems in ML

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:*Achermann Reto

- Previous by Date: Re: [isabelle] “Hilbert and Isabelle” in Spektrum der Wissenschaft (March 2019)
- Next by Date: [isabelle] Trivial lemma requires syntactic fiddling
- Previous by Thread: Re: [isabelle] “Hilbert and Isabelle” in Spektrum der Wissenschaft (March 2019)
- 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