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?

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



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