Re: [isabelle] Creating Theorems in ML

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?

 datatype Foo = Bar string

 ? Scratch.Bar "hello"


-- Reto

Reto Achermann
PhD Student, ETH Zurich

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.



From: cl-isabelle-users-bounces at <cl-isabelle-users-bounces at> on behalf of Achermann Reto <reto.achermann at>
Sent: Thursday, February 28, 2019 12:39:42 PM
To: isabelle-users at
Subject: [isabelle] Creating Theorems in ML

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"

lemma foo:
  "A ==> (A ==> B) ==> B"


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.

-- Reto

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