Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Translating from Isar to ML?


view this post on Zulip Email Gateway (Jan 19 2021 at 09:37):

From: Albert Jiang <albert594250@gmail.com>
Hi,

I'm working on a system that allows the communication between Isabelle and
outside agents. I wonder if there is an easy way to automatically translate
the proof in Isar to ML? For example, is there an automatic way that allows
the following proof

lemma bar:"(1::nat)=1"
apply (rule refl)
done

to be translated into something like this:

ML ‹
val ctxt = @{context};val bar' =
@{term "(1::nat) = 1"}
|> HOLogic.mk_Trueprop
|> Thm.cterm_of ctxt
|> Goal.init
|> Tactic.rule_by_tactic ctxt (Classical.rule_tac ctxt @{thms refl} [] 1)
|> Goal.finish ctxt
|> Thm.close_derivation ⌂
;ML_Thms.bind_thm ("bar'",bar');

?

I only got into Isar/ML recently so I'm sorry if this is a trivial question.

Many thanks,

Albert

view this post on Zulip Email Gateway (Jan 19 2021 at 11:55):

From: Makarius <makarius@sketis.net>
On 18/01/2021 22:12, Albert Jiang wrote:

I'm working on a system that allows the communication between Isabelle and
outside agents. I wonder if there is an easy way to automatically translate
the proof in Isar to ML? For example, is there an automatic way that allows
the following proof

lemma bar:"(1::nat)=1"
apply (rule refl)
done

to be translated into something like this:

ML ‹
val ctxt = @{context};val bar' =
@{term "(1::nat) = 1"}
|> HOLogic.mk_Trueprop
|> Thm.cterm_of ctxt
|> Goal.init
|> Tactic.rule_by_tactic ctxt (Classical.rule_tac ctxt @{thms refl} [] 1)
|> Goal.finish ctxt
|> Thm.close_derivation ⌂
;ML_Thms.bind_thm ("bar'",bar');

From where did you get this proposal for the translation? It is actually quite
far from the reality of how Isar really works. So the translation would break
down in nontrivial cases.

I only got into Isar/ML recently so I'm sorry if this is a trivial question.

An easy way would be to make a function that uses Isar source text and
interprets it faithfully. But what would be the purpose of that?

Just the usual meta-questions: What is your actual application? What are your
actual needs?

Makarius

view this post on Zulip Email Gateway (Jan 19 2021 at 13:41):

From: Albert Jiang <albert594250@gmail.com>
Hi Makarius,

Thank you for your answer!

The actual application is an Isabelle theorem proving environment that's
able to interact with a Python client. The client will send the
step-by-step proof as strings and receive the proof state info at each
step. I'm basing this on the scala-isabelle library and gRPC. The library
allows the compilation of ML code. So I thought if I could translate Isar
strings into ML code, the Python client can send in Isar commands line by
line. And then the commands can be translated into ML code, compiled, and
executed.

An easy way would be to make a function that uses Isar source text and
interprets it faithfully. But what would be the purpose of that?

I wonder if you could give some pointers as to how to make such a function?

Many thanks,
Albert

view this post on Zulip Email Gateway (Jan 19 2021 at 14:12):

From: Dominique Unruh <unruh@ut.ee>
Hi,

if I understand right, you want to do the following (from the python side):

* Create a new theory.
* Apply Isar commands one-by-one (where the commands are given as
strings, same as they would be in actual Isabelle source code).

* After each command, get access to the "state" of the Isar system
(which could be the toplevel theory, or the current proof state,
depending what the commands so far where).

* Inspect that state in various ways

If this is the case, then you might be interested in
https://github.com/dominique-unruh/scala-isabelle/blob/master/src/test/scala/de/unruh/isabelle/experiments/ExecuteIsar.scala

This is an experiment where I did more or less the above. This code is
uncommented and maybe a bit chaotic (it's me doing experiments, not part
of the distributed library) but I'd be happy to walk you through it on
the scala-isabelle gitter chat.

I also have code fragments that parse a method description (the ... in
apply (...)) and allow you to apply it to a goal. If you need that one,
I can have a look where I put it...

Best wishes,
Dominique.

view this post on Zulip Email Gateway (Jan 19 2021 at 14:26):

From: Albert Jiang <albert594250@gmail.com>
Hi Dominique,

On Tue, Jan 19, 2021 at 2:12 PM Dominique Unruh <unruh@ut.ee> wrote:

Hi,

if I understand right, you want to do the following (from the python side):

- Create a new theory.
- Apply Isar commands one-by-one (where the commands are given as
strings, same as they would be in actual Isabelle source code).
- After each command, get access to the "state" of the Isar system
(which could be the toplevel theory, or the current proof state, depending
what the commands so far where).
- Inspect that state in various ways

If this is the case, then you might be interested in
https://github.com/dominique-unruh/scala-isabelle/blob/master/src/test/scala/de/unruh/isabelle/experiments/ExecuteIsar.scala

Yes this is exactly what I need. Thank you for the pointer!

This is an experiment where I did more or less the above. This code is
uncommented and maybe a bit chaotic (it's me doing experiments, not part of
the distributed library) but I'd be happy to walk you through it on the
scala-isabelle gitter chat.

I also have code fragments that parse a method description (the ... in
apply (...)) and allow you to apply it to a goal. If you need that one, I
can have a look where I put it...

I'll be very grateful if you can take a look at where the relevant code
fragments are.

Best wishes,
Dominique.

Many thanks,
Albert

On 1/19/21 3:40 PM, Albert Jiang wrote:

Hi Makarius,

Thank you for your answer!

The actual application is an Isabelle theorem proving environment that's
able to interact with a Python client. The client will send the
step-by-step proof as strings and receive the proof state info at each
step. I'm basing this on the scala-isabelle library and gRPC. The library
allows the compilation of ML code. So I thought if I could translate Isar
strings into ML code, the Python client can send in Isar commands line by
line. And then the commands can be translated into ML code, compiled, and
executed.

An easy way would be to make a function that uses Isar source text and
interprets it faithfully. But what would be the purpose of that?

I wonder if you could give some pointers as to how to make such a function?

Many thanks,
Albert

On Tue, Jan 19, 2021 at 11:55 AM Makarius <makarius@sketis.net> wrote:

On 18/01/2021 22:12, Albert Jiang wrote:

I'm working on a system that allows the communication between Isabelle
and
outside agents. I wonder if there is an easy way to
automatically translate
the proof in Isar to ML? For example, is there an automatic way that
allows
the following proof

lemma bar:"(1::nat)=1"
apply (rule refl)
done

to be translated into something like this:

ML ‹
val ctxt = @{context};val bar' =
@{term "(1::nat) = 1"}
|> HOLogic.mk_Trueprop
|> Thm.cterm_of ctxt
|> Goal.init
|> Tactic.rule_by_tactic ctxt (Classical.rule_tac ctxt @{thms refl} []
1)
|> Goal.finish ctxt
|> Thm.close_derivation ⌂
;ML_Thms.bind_thm ("bar'",bar');

From where did you get this proposal for the translation? It is actually
quite
far from the reality of how Isar really works. So the translation would
break
down in nontrivial cases.

I only got into Isar/ML recently so I'm sorry if this is a trivial
question.

An easy way would be to make a function that uses Isar source text and
interprets it faithfully. But what would be the purpose of that?

Just the usual meta-questions: What is your actual application? What are
your
actual needs?

Makarius

view this post on Zulip Email Gateway (Jan 19 2021 at 15:19):

From: Makarius <makarius@sketis.net>
The scala-isabelle library falls outside my understanding of
Isabelle/Scala/PIDE --- I am the inventor of that framework.

If you want to interact with Isabelle programmatically in an official manner,
see the "system" manual chapter 4: it describes a TCP server with JSON
protocol, but it is also possible (actually easier) to work directly in
Isabelle/Scala with the Headless PIDE session. See also "isabelle
scala_project" in the "system" manual.

If not, I will merely ignore this thread and leave it to external tool
providers to sort out the problems (small ones and conceptual ones).

Makarius


Last updated: Sep 28 2021 at 19:14 UTC