Programmatic access to Isabelle theories · General

I'm currently working on a project and I'm a bit lost in all the different documentation and functionality of Isabelle. I've created a Java application that uses Isabelle as one of its subcomponents. Now, I've reached a point where I would need some access to contents of theory files within the Java environment, namely I want to create a Theorem class with methods like Theorem.getProposition() and Theorem.getRequirements() or something similar. I'm not interested in altering proofs or anything like that, it would essentially be a read-only operation.

There are several approaches I have thought about and I don't know which one to follow further. The "simplest" one would probably be to just read from .thy-files directly, without even opening them in Isabelle, but I'm not particularly fond of that. Isabelle/Scala would be the natural choice due to it being JVM-compatible, but as far as I can tell after looking through the mailing list's archives, it does not seem to be up to the task. Isabelle/ML might be better suited, but after some experimentation I have not yet been able to achieve what I want and don't really know how to go on. Isabelle/MMT might be worth a look as well, but I have not been able to build that.

I know my question might be a bit broad, but I'm happy about any pointer or hint you can give me. Thanks in advance!

Manuel Eberl (Mar 18 2021 at 12:12):

I think you can interface with Isabelle/ML through Isabelle/Scala. But you should ask this on the mailing list, I think Makarius is the best (perhaps the only) person who can really answer this, and I don't think he reads Zulip.

Manuel Eberl (Mar 18 2021 at 12:13):

There was the libisabelle project by Lars Hupel as well that did things like that from Scala, but I don't know what its current status is.

Lukas Stevens (Mar 18 2021 at 12:14):

Fabian Richter (Apr 17 2021 at 12:53):

Sorry for the late reply, I've been tinkering with Isabelle/ML and scala-isabelle and gotten pretty far with that. I'm now facing a slightly more specific problem. I'm able to extract objects of ML-type "typ" from my theories and now want to work on those by extracting their signatures. When using Isabelle/jEdit, "typ"-objects are displayed in a nicely readable form, similar to the way their signatures are defined (eg. 'val x =
"(?'a set ⇒ (?'a × ?'a) set list ⇒ ?'a set × ?'a set × ?'a set)
⇒ (?'a set ⇒ (?'a × ?'a) set list ⇒ ?'a set × ?'a set × ?'a set)
⇒ ?'a set ⇒ (?'a × ?'a) set list ⇒ ?'a set × ?'a set × ?'a set":
typ'). Is there a way to retrieve this representation as a string instead of a typ object using Isabelle/ML?

I've been searching through Isabelle documentation and the ML sources, but only been able to retrieve different representations containing much less information about the actual signatures. Again, any pointers are very appreciated!

Lukas Stevens (Apr 17 2021 at 13:25):

Your first stop should be Syntax.pretty_term. Then you have to convert the pretty printing type into a string.

Lukas Stevens (Apr 17 2021 at 13:26):

Fabian Richter (Apr 17 2021 at 16:09):

thanks for the reply! I've been playing around with this, and it is not working as I hoped. The following lays out my current approach and its intermediate results:

fun sequential_composition :: "'a Electoral_Module ⇒ 'a Electoral_Module ⇒
'a Electoral_Module" where
[...]

"x = "(?'a set ⇒ (?'a × ?'a) set list ⇒ ?'a set × ?'a set × ?'a set)
⇒ (?'a set ⇒ (?'a × ?'a) set list ⇒ ?'a set × ?'a set × ?'a set)
⇒ ?'a set ⇒ (?'a × ?'a) set list ⇒ ?'a set × ?'a set × ?'a set":
typ"

val x_pretty = Syntax.pretty_typ @{context} x
==> "(?'a set ⇒ (?'a × ?'a) set list ⇒ ?'a set × ?'a set × ?'a set)
⇒ (?'a set ⇒ (?'a × ?'a) set list ⇒ ?'a set × ?'a set × ?'a set)
⇒ ?'a set ⇒ (?'a × ?'a) set list ⇒ ?'a set × ?'a set × ?'a set":
Pretty.T

val x_pretty_string = Pretty.string_of x_pretty
==> "<markup>": string (in Isabelle/jEdit)
==> (?'a, ?'b,
?'c) tuple_isomorphism.tuple_isomorphism_IITN_tuple_isomorphism itself
\<Rightarrow> typerep (in my Java application after going through scala-isabelle)

This last string I receive is significantly different from the one I see within the Pretty.T and Isabelle/jEdit. Is this part of the markup done by Pretty.string_of, or might it even be scala-isabelle working differently than I think?

Lukas Stevens (Apr 17 2021 at 16:49):

Hm, I played around with it a bit and I am not sure how to get the string directly without the surrounding markup. You should probably ask Makarius/the mailing list.

Lukas Stevens (Apr 17 2021 at 16:51):

It's probably also kind of dangerous to use the string representation. It should probably be encoded in YXML or something and then decoded on the Scala side again.

Fabian Richter (Apr 17 2021 at 17:42):

I think I've "solved" my problem for now. I've built my own type_to_string function, preserving the tree-like structure of typs as a bracket-expression within the string.

fun typ_to_string (x: Basic_Term.typ): string = case x of
    Type x => "(" ^ (fst x) ^ String.concat (map (typ_to_string) (snd x)) ^ ")"
  |  _ => ""

While this does feel rather hacky, is limited to a very special case and the output is not particularly appealing to the eye, I think it fits my purposes for now, especially as I've been stuck on this for quite some time. Thanks again, and in case I come up with something better, I'll update the thread for future reference.

Fabian Richter (Apr 17 2021 at 19:48):

Okay, wow, that's a bit embarrassing. There was a bug in my Java code mismatching types and their signatures, so everything was wrong, but looked just about right enough that I wasn't suspicious. I haven't yet been able to check for sure, but I heavily suppose Syntax.pretty_typ would indeed work for me and my weird workaround is unnecessary. I'll look into using a more robust encoding in the future, but I'm pretty happy that my prototypical implementation can at least serve as a proof-of-concept for now.

Stream: General

Topic: Programmatic access to Isabelle theories

Fabian Richter (Mar 18 2021 at 12:02):