Email Gateway (Jan 19 2021 at 09:37): 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
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 prooflemma bar:"(1::nat)=1"
apply (rule refl)
doneto 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
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
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.
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 waysIf 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.scalaYes 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,
AlbertOn 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 prooflemma bar:"(1::nat)=1"
apply (rule refl)
doneto 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
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: Jul 15 2022 at 23:21 UTC