Re: [isabelle] 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



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