Email Gateway (Aug 22 2022 at 15:19): Email Gateway (Aug 22 2022 at 15:19):From: Moussa Bah <bah.demba@gmail.com>
Hi everyone,
I am new in Isabelle and I would like to implement a proposed proof
technique in it but I don't know where I have to add my code. I am looking
for help.
many thanks,
Moussa
Email Gateway (Aug 22 2022 at 15:19):From: Lawrence Paulson <lp15@cam.ac.uk>
Isabelle is not the best basis for adding your own code, because the underlying formal system is quite elaborate and the APIs are extensive. You haven't stated, incidentally, whether you want to extend Isabelle/HOL (and therefore higher-order logic), or another built-in logic, or Pure Isabelle (some formalism of your own).
You might consider HOL4, an implementation of higher-order logic where coding is fairly straightforward.
Larry Paulson
Email Gateway (Aug 22 2022 at 15:19):From: Makarius <makarius@sketis.net>
Isabelle/jEdit is a fully-featured IDE that supports development of
tools in Isabelle/ML, although most users apply it most of the time to
develop theory libraries.
To implement anything yourself, you should study how others have done
that before. E.g. pick a tool that you think is close to what you want
to do (lets say the "blast" proof method), and use C-mouse-hover-click
technique described in the Isabelle/jEdit manual to get to its
definition. This will usually lead to some ML_file or ML commands that
incorporate the new Isabelle language element.
Note that in order to browse Isabelle/ML sources of tools in
Isabelle/HOL, you need to do this with "isabelle jedit -l Pure", i.e. in
a session that does not yet contain Isabelle/HOL. In contrast, tools in
other sessions (e.g. src/HOL/Library) require the default HOL image.
It is also possible to browse Isabelle/Pure sources with full IDE
annotations by opening src/Pure/ROOT.ML in Isabelle/jEdit. Here the
level of sophistication is usually much higher than plain user-space
tools from elsewhere, but looking at the core implementation also helps
to understand how things are done properly.
Some further background information on Isabelle/ML is available in the
"implementation" manual.
Makarius
Last updated: Apr 26 2024 at 12:28 UTC