Email Gateway (Aug 22 2022 at 09:38): Email Gateway (Aug 22 2022 at 09:38):From: Viorel Preoteasa <viorel.preoteasa@aalto.fi>
Hello,
I am interested in using Isabelle to simplify a formula based on a
specific theory.
If I would use the Isabelle/jEdit interface I would create a dummy theory
theory MySimp imports BaseTheory
begin
lemma "expression to simplify = A"
apply simp
At this point the result that I am interested is
the left hand-side of the current goal.
How can this be done programmatically? Should I use
"isabelle_process" or "isabelle console"?
Best regards,
Viorel Preoteasa
Email Gateway (Aug 22 2022 at 09:38):From: Lars Hupel <hupel@in.tum.de>
How can this be done programmatically? Should I use
"isabelle_process" or "isabelle console"?
First of all, there's 'Simplifier.rewrite':
ML‹Simplifier.rewrite @{context} @{cterm "rev []"}›
... which results in
val it = "rev [] ≡ []": thm
This should be an easy-enough interface to perform just what you need.
Second, there's the question how to invoke just this bit. I think
'isabelle console' is out – quoting from the system manual:
"Interaction works via the raw ML toplevel loop: this is neither
Isabelle/Isar nor Isabelle/ML within the usual formal context. Some
useful ML commands at this stage are cd, pwd, use, use_thy, use_thys."
'isabelle_process' is even more low-level.
In which environment do you intend to invoke the simplifier? In some
program of yours? Via bash? Something else? Repeatedly, or just one-off?
Cheers
Lars
smime.p7s
Email Gateway (Aug 22 2022 at 09:38):From: Viorel Preoteasa <viorel.preoteasa@aalto.fi>
On 04/09/2015 04:46 PM, Lars Hupel wrote:
How can this be done programmatically? Should I use
"isabelle_process" or "isabelle console"?
First of all, there's 'Simplifier.rewrite':ML‹Simplifier.rewrite @{context} @{cterm "rev []"}›
The function Simplifier.rewrite seem to be available in isabelle_process,
but I don't know how to get the context, and the term in the right
form. The actual simplifying command contains also
some lemmas that I do not necessarily want as simplification
rules.
I noticed also that there is a function for parsing terms, but it also
requires a context parameter. It seems that what I should do is:
context = ...
T = Simplifier.rewrite context (Syntax.parse_term context "...")
result = Syntax.string_of_term context (the right hand side term of T)
... which results in
val it = "rev [] ≡ []": thm
This should be an easy-enough interface to perform just what you need.
Second, there's the question how to invoke just this bit. I think
'isabelle console' is out – quoting from the system manual:"Interaction works via the raw ML toplevel loop: this is neither
Isabelle/Isar nor Isabelle/ML within the usual formal context. Some
useful ML commands at this stage are cd, pwd, use, use_thy, use_thys."'isabelle_process' is even more low-level.
In which environment do you intend to invoke the simplifier? In some
program of yours? Via bash? Something else? Repeatedly, or just one-off?
I need to perform this operation from within a Python program.
I use Python to produce some terms based on some specification,
and I need them simplified using Isabelle. The terms are using
definitions from the supporting theory.
Viorel
Email Gateway (Aug 22 2022 at 09:38):From: Lars Hupel <hupel@in.tum.de>
Second, there's the question how to invoke just this bit. I think
'isabelle console' is out – quoting from the system manual:
This assessment was wrong. It is possible with 'isabelle console':
$ bin/isabelle console
val commit = fn: unit -> bool
val it = (): unit
ML> val thy = Thy_Info.get_theory "Main";
val thy = ...: theory
From there on, you can obtain a context:
ML> val ctxt = Proof_Context.init_global thy;
val ctxt = <context>: Proof.context
Now you can read a term (not just parse!):
ML> val t = Syntax.read_term ctxt "rev []";
val t =
Const ("List.rev", "'a List.list => 'a List.list") $
Const ("List.list.Nil", "'a List.list"): term
... and rewrite:
ML> Simplifier.rewrite ctxt (cterm_of thy t) |> Thm.rhs_of;
val it = "[]": cterm
Does that help?
Cheers
Lars
Email Gateway (Aug 22 2022 at 09:38):From: Lars Noschinski <noschinl@in.tum.de>
Lars has already written something about how to acquire a context.
Depending on what you do with the terms in your program, it might be a
good idea to use the YXML format to pass terms between Isabelle and your
program. There have been some discussions on that subject in the past.
Email Gateway (Aug 22 2022 at 09:38):From: Lars Hupel <hupel@in.tum.de>
If you are free to choose the language of your tool, may I suggest to
consider Java or Scala: For the JVM, there is the possibility to
communicate with the prover in a canonical way (i.e.
starting/stopping/sending messages to the prover can be done with
regular function calls, instead of performing low-level process
operations and I/O).
Email Gateway (Aug 22 2022 at 09:38):From: Viorel Preoteasa <viorel.preoteasa@aalto.fi>
Thank you Lars,
This is exactly what I need. I tested it with both
isabelle console and isabelle_process, and it works
in the same way.
Best regards,
Viorel
Email Gateway (Aug 22 2022 at 09:38):From: Viorel Preoteasa <viorel.preoteasa@aalto.fi>
This is a good point. Thank you. We will use the simplified
expressions to generate some other Isabelle file, so for this
purpose we do not need the xml format.
Best regards,
Viorel
Email Gateway (Aug 22 2022 at 09:39):From: Makarius <makarius@sketis.net>
For me a console is a device where a human is sitting to connect to the
computer. A tty is something similar, but from the Unix world (actually a
brand name of a particular device).
"Programmatically" probably refers to batch mode, so the raw
isabelle_process is the most elementary way to do it.
The examples so far on this thread where using the cold and naked toplevel
of the underlying ML system -- working there is possible, but might become
a bit awkward. Isabelle/ML normally runs within the Isabelle environment,
e.g. with a theory that is loaded via use_thy from outside.
Much more possibilities of "programmatic" use of Isabelle are thinkable,
e.g. taling to Isabelle/Scala as already explained by Lars Hupel. In may
applications one might even want to talk directly within the PIDE to the
Isabelle process, depending on user interaction result.
There are many possiblities beyond 1970-TTY-mode. It all depends on the
application what is the best way.
Makarius
Email Gateway (Aug 22 2022 at 09:39):From: Makarius <makarius@sketis.net>
Generating Isabelle sources sounds a bit odd. Depending on the actual
application, it might be easier to put the "programmatic" part into
Isabelle itself, as a small Isabelle/ML tool that reads the input and
drives the system in the intended way, then outputs the results somewhere
else. But you did not explain the intention so far.
Makarius
Email Gateway (Aug 22 2022 at 09:39):From: Viorel Preoteasa <viorel.preoteasa@aalto.fi>
On 04/09/2015 11:17 PM, Makarius wrote:
On Thu, 9 Apr 2015, Viorel Preoteasa wrote:
How can this be done programmatically? Should I use
"isabelle_process" or "isabelle console"?For me a console is a device where a human is sitting to connect to
the computer. A tty is something similar, but from the Unix world
(actually a brand name of a particular device).
Here, I just meant the option "console" available for the bin/isabelle
command. Ideally I would need an API
available in Python which does what I need: Simplifies a term based on a
specific theory. I understand
now that this API is available for Scala, and of course for SML, so in
the future I may use Scala.
On the other hand, even if using SML, getting started with it does not
seem easy. I tried to find the right
functions for this job before posting the question to the mailing list.
"Programmatically" probably refers to batch mode, so the raw
isabelle_process is the most elementary way to do it.
You are right, maybe batch mode is more appropriate term.
Thank you,
Viorel
Email Gateway (Aug 22 2022 at 09:39):From: Makarius <makarius@sketis.net>
Do you mean SML as a language, or Isabelle/ML as a language + library?
Getting started with Standard ML should be easy, using resources on the
web or text books.
Getting started with Isabelle/ML should be easy as well, since the
Isabelle Prover IDE allows to explore whatever you see, down to its actual
definition. Tools are defined in Isabelle/ML, so the standard PIDE
control-hover-click over Isar commands, methods, attributes etc. will show
the relevant ML definitions.
Reading and understanding that needs some practice and some guidance,
though. The "implementation" provides many explanations of many things,
but it is not a quick-and-dirty HOWTO guide.
Depending on what you ultimately want to achieve, some decent Isabelle/ML
could work out easier and more robust than tinkering with scripting
languages, processes, generated sources etc.
Makarius
Email Gateway (Aug 22 2022 at 09:39):From: Viorel Preoteasa <viorel.preoteasa@aalto.fi>
On 04/10/2015 11:58 AM, Makarius wrote:
On Fri, 10 Apr 2015, Viorel Preoteasa wrote:
Ideally I would need an API available in Python which does what I
need: Simplifies a term based on a specific theory. I understand now
that this API is available for Scala, and of course for SML, so in
the future I may use Scala.On the other hand, even if using SML, getting started with it does
not seem easy. I tried to find the right functions for this job
before posting the question to the mailing list.Do you mean SML as a language, or Isabelle/ML as a language + library?
I mean Isabelle/ML as a language + library.Getting started with Standard ML should be easy, using resources on
the web or text books.Getting started with Isabelle/ML should be easy as well, since the
Isabelle Prover IDE allows to explore whatever you see, down to its
actual definition. Tools are defined in Isabelle/ML, so the standard
PIDE control-hover-click over Isar commands, methods, attributes etc.
will show the relevant ML definitions.
Getting started was a bit difficult because I could not find an example
which
was self contained and small.
After asking on the mailing list, the answer by Lars, was very helpful
(ML‹Simplifier.rewrite @{context} @{cterm "rev []"}›), but it was working
within an Isabelle theory only, and not as standalone Isabelle/ML program.
The final Isabelle/ML program which does what I need is the following:
use_thy "AutoSimp";
val thy = Thy_Info.get_theory "AutoSimp";
fun term_to_string ctxt t =
let
val ctxt' = Config.put show_markup false ctxt;
in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
val ctxt = Proof_Context.init_global thy;
val t = Syntax.read_term ctxt "rel (ExampleA0) (si_f) (d,so_f)";
val simp_term_a = Simplifier.rewrite ctxt (cterm_of thy t) |> Thm.rhs_of;
val simp_term_b = term_of simp_term_a;
val result = term_to_string ctxt simp_term_b;
writeln result;
It is conceptually very simple, but figuring out all these functions
was not that simple. I could do it only with the help of the answers
from the mailing list.
For example figuring out how to use Syntax.string_of_term was also
not easy. I found this way of using Syntax.string_of_term in an old message
for the mailing list. I do not understand it fully, but it seems it does
what
I need.
It is not clear to me if it is better to use this program as such or embed
as ML{...} into a theory file. In the end I am only interested in the
string from the variable result.
Reading and understanding that needs some practice and some guidance,
though. The "implementation" provides many explanations of many
things, but it is not a quick-and-dirty HOWTO guide.
The main problem was getting started.Depending on what you ultimately want to achieve, some decent
Isabelle/ML could work out easier and more robust than tinkering with
scripting languages, processes, generated sources etc.
My use case is very simple now, and it is mainly exploratory. Using
Scala can be a good
solution, however Python is also a convenient language. Isabelle/ML can
also be a
solution, but the problem remains the same, figuring out the right
functions for
solving the problem.
Passing strings from one program to another does not seem such a big
problem,
and Python has a simple API for working with external programs.
By the way, how is the communication between Scala and Isabelle/ML done?
I assume it is also by having the Isabelle/ML process running in the
background,
and by sending and receiving strings via pipes.
Viorel
Email Gateway (Aug 22 2022 at 09:39):From: Lars Hupel <hupel@in.tum.de>
That's almost correct. Communication between the processes works via
sockets these days, and the strings which are passed back and forth are
actually represent XML documents. Both Isabelle/Scala and Isabelle/ML
offer combinators for encoding (and decoding) arbitrary data to (and
from) XML.
The major advantage in using Isabelle/Scala is that someone else takes
care of implementing resource control, session management, thread
pooling, ... and offer a nice high-level API for that. Using this API is
much more robust as compared to forking out processes by hand,
especially for serious applications.
Cheers
Lars
Email Gateway (Aug 22 2022 at 09:40):From: Makarius <makarius@sketis.net>
On Fri, 10 Apr 2015, Viorel Preoteasa wrote:
After asking on the mailing list, the answer by Lars, was very helpful
(ML‹Simplifier.rewrite @{context} @{cterm "rev []"}›), but it was working
within an Isabelle theory only, and not as standalone Isabelle/ML program.
Isabelle/ML always runs in such a formal context, i.e. inside a theory or
a more deeply nested context that is built up by other means. In such a
situation the ML antiquotation @{context} provides the all-important
context at compile time. When you implement your own tools, say a command
or proof method, you get the context at runtime from the system
infrastructure -- that is in fact the normal situation.
The final Isabelle/ML program which does what I need is the following:
use_thy "AutoSimp";
val thy = Thy_Info.get_theory "AutoSimp";
fun term_to_string ctxt t =
let
val ctxt' = Config.put show_markup false ctxt;
in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;val ctxt = Proof_Context.init_global thy;
val t = Syntax.read_term ctxt "rel (ExampleA0) (si_f) (d,so_f)";
val simp_term_a = Simplifier.rewrite ctxt (cterm_of thy t) |> Thm.rhs_of;
val simp_term_b = term_of simp_term_a;
val result = term_to_string ctxt simp_term_b;
writeln result;
This is not an Isabelle/ML program, but raw SML outside of the Isabelle
environment. You won't get very far for non-trivial things. E.g. the
whole Isabelle/HOL modules and tools are not accessible -- in fact the
accessibility of Isabelle/Pure outside the normal Isabelle environment is
merely an artifact of bootstrapping.
As the system manual points out, use_thy is the main thing you can do in
this raw ML bootstrap environment, i.e. to get into some theory context to
do the actual work.
It is not clear to me if it is better to use this program as such or embed
as ML{...} into a theory file. In the end I am only interested in the
string from the variable result.
ML {...} is always better, unless there is a very special situation.
ML_file is the same and useful for bigger text files, also with more
support in the editor.
Scala can be a good solution, however Python is also a convenient
language. Isabelle/ML can also be a solution, but the problem remains
the same, figuring out the right functions for solving the problem.
Many years ago, I was considering Python as Isabelle system programming
language, but it later became Scala. Today, you can do a fair amount of
system programming both in Isabelle/Scala and Isabelle/ML, and it is
initially hard to tell which side is better for an application. There are
also applications on both sides, which requires some bilingual fluency.
But the Isabelle/Scala and Isabelle/ML conventions and libraries are as
close to each other as feasible.
E.g. there is Isabelle_System.bash to invoke an external process running a
shell script both in Isabelle/ML and Isabelle/Scala.
Passing strings from one program to another does not seem such a big
problem, and Python has a simple API for working with external programs.By the way, how is the communication between Scala and Isabelle/ML done?
I assume it is also by having the Isabelle/ML process running in the
background, and by sending and receiving strings via pipes.
That is a very crude model, and the reality with something that actually
works robustly and efficiently came out a bit different than I anticipated
7 or 8 years ago. My ITP 2014 paper has a small section on PIDE
architecture and protocol layers:
http://www4.in.tum.de/~wenzelm/papers/itp-pide.pdf -- another version of
that aspect is explained here for Coq (!) http://arxiv.org/abs/1304.6626
So Isabelle/PIDE solves that prover connectivity problem. It just needs
to be reused. The usual errors and mistakes don't have to be repeated.
Makarius
Last updated: Apr 24 2024 at 16:18 UTC