Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Creating Theorems in ML

view this post on Zulip Email Gateway (Aug 22 2022 at 19:06):

From: Achermann Reto <reto.achermann@inf.ethz.ch>
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

view this post on Zulip Email Gateway (Aug 22 2022 at 19:16):

From: Achermann Reto <reto.achermann@inf.ethz.ch>
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

view this post on Zulip Email Gateway (Aug 22 2022 at 19:16):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Reto,

I have no idea what your overall application is, but I would infer from
your question »as it is« that it aims towards how to interface between
code generated from HOL and Isabelle/ML.

There is already substantial support for that use case, see particulary
the antiquotations @{code …} and various @{computation* …}. See the
tutorial on code generation for details.

Note that if you are interested to generate native Isabelle/ML strings
you should adhere to type String.literal rather than string (the details
are delicate due to different notions of »string« in different target
languages).

Hope this helps in the next steps,
Florian
signature.asc

view this post on Zulip Email Gateway (Aug 22 2022 at 19:17):

From: Achermann Reto <reto.achermann@inf.ethz.ch>
Hi Florian,

Thank you for your reply. Let me try to give some more context.

So far, I managed to create a locale, and inside this locale a theorem using

Goal.prove ctxt vars asms prop auto_tac

where prop = @{prop "A ⟹ (A⟹B) ⟹ (B⟹P) ⟹ P"}

print_theorems shows:

MyL.foo_0: MyL ?st ⟹ ?A ⟹ (?A ⟹ ?B) ⟹ (?B ⟹ ?P) ⟹ ?P

which seems good to me, and which is what I want to acheive.

Now, I'd like to use my own datatype in this lemma e.g.

datatype MyT = MyType string

lemma foobar : "MyType t ∈ st ⟹ A ⟹ (A⟹B) ⟹ (B⟹P) ⟹ P

Which works well from within a Theory, but I want to create this lemma from my ML code using the datatype MyT which has been defined in a Theory file.

Goal.prove ctxt vars asms prop auto_tac

where prop = @{prop "MyType t ∈ st ⟹ A ⟹ (A⟹B) ⟹ (B⟹P) ⟹ P"}

Which results in an error: Illegal fixed variable: "MyType"

Is the use of the antiquotations @{prop } actually the right way to achieve this?

Thanks,
-- Reto

view this post on Zulip Email Gateway (Aug 22 2022 at 19:18):

From: Thomas Sewell <sewell@chalmers.se>
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.

view this post on Zulip Email Gateway (Aug 22 2022 at 19:18):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Reto,

note that antiquotations are resolved statically when processing an
Isabelle/ML block, hence I guess the issue is that you make a reference
to a symbol which is not yet present when the Isabelle/ML is parsed.

I do not know what your application context is, but if you are plumbing
Isabelle/ML pieces in a theory file (which is usually a good starting
point for experimentation), it is sufficient to have the antiquotation
in question in a separate Isabelle/ML block.

Cheers,
Florian
signature.asc

view this post on Zulip Email Gateway (Aug 22 2022 at 19:18):

From: Achermann Reto <reto.achermann@inf.ethz.ch>
Hi Florian,

Thank you for your e-mail.

I think you the issue you pointed out might be the cause of the problem. I managed to get something going by separating the process into multiple steps. Creating a locale and proving theorems at the same time, while referring to locale state seem to have caused some issues there.

In the end, Syntax.read_props was also helpful to create the props.

-- Reto

Last updated: Apr 25 2024 at 04:18 UTC